From 9a7dfe93ee0cd82be26b598d676d4b9147ddce20 Mon Sep 17 00:00:00 2001
From: Manasij Mukherjee <manasij7479@gmail.com>
Date: Wed, 12 Feb 2020 16:28:49 -0700
Subject: [PATCH] Do not generate inputs when PC has PHI

---
 include/souper/Infer/Pruning.h     |  2 +-
 lib/Infer/AbstractInterpreter.cpp  |  2 +-
 lib/Infer/EnumerativeSynthesis.cpp |  2 +-
 lib/Infer/Pruning.cpp              | 23 +++++++++++++++++------
 4 files changed, 20 insertions(+), 9 deletions(-)

diff --git a/include/souper/Infer/Pruning.h b/include/souper/Infer/Pruning.h
index 8d709b8f1..06b0ac6d0 100644
--- a/include/souper/Infer/Pruning.h
+++ b/include/souper/Infer/Pruning.h
@@ -52,7 +52,7 @@ class PruningManager {
   llvm::KnownBits LHSKnownBitsNoSpec;
   InputVarInfo LHSMustDemandedBits;
   bool LHSHasPhi = false;
-
+  bool PCHasPhi = false;
   PruneFunc DataflowPrune;
   unsigned NumPruned;
   unsigned TotalGuesses;
diff --git a/lib/Infer/AbstractInterpreter.cpp b/lib/Infer/AbstractInterpreter.cpp
index e57c9215e..d10473b60 100644
--- a/lib/Infer/AbstractInterpreter.cpp
+++ b/lib/Infer/AbstractInterpreter.cpp
@@ -496,7 +496,7 @@ namespace souper {
     case Inst::Phi: {
       std::vector<llvm::KnownBits> vec;
       for (auto &Op : I->Ops) {
-        vec.emplace_back(findKnownBits(Op, CI));
+        vec.emplace_back(findKnownBits(Op, CI, UsePartialEval));
       }
       Result = mergeKnownBits(vec);
     }
diff --git a/lib/Infer/EnumerativeSynthesis.cpp b/lib/Infer/EnumerativeSynthesis.cpp
index 90ed79d5f..ba5c9af5c 100644
--- a/lib/Infer/EnumerativeSynthesis.cpp
+++ b/lib/Infer/EnumerativeSynthesis.cpp
@@ -864,7 +864,7 @@ EnumerativeSynthesis::synthesize(SMTLIBSolver *SMTSolver,
   std::vector<PruneFunc> PruneFuncs = { [&Visited](Inst *I, std::vector<Inst*> &ReservedInsts)  {
     return CountPrune(I, ReservedInsts, Visited);
   }};
-  if (EnableDataflowPruning) {
+  if (EnableDataflowPruning && BPCs.empty()) {
     DataflowPruning.init();
     PruneFuncs.push_back(DataflowPruning.getPruneFunc());
   }
diff --git a/lib/Infer/Pruning.cpp b/lib/Infer/Pruning.cpp
index faae5bbb8..d84c2bbe2 100644
--- a/lib/Infer/Pruning.cpp
+++ b/lib/Infer/Pruning.cpp
@@ -211,7 +211,7 @@ bool PruningManager::isInfeasible(souper::Inst *RHS,
       }
     }
 
-    if (LHSHasPhi) {
+    if (LHSHasPhi && !PCHasPhi) {
       auto LHSCR = LHSConstantRange[I];
       auto RHSCR = ConstantRangeAnalysis().findConstantRange(RHS, ConcreteInterpreters[I]);
       if (!RHSCR.isFullSet()) {
@@ -492,17 +492,28 @@ void PruningManager::init() {
     Ante = SC.IC.getInst(Inst::And, 1, {Ante, Eq});
   }
 
+  if (hasGivenInst(Ante, [](Inst *I){ return I->K == Inst::Phi;})) {
+    PCHasPhi = true;
+  }
+
+  if (hasGivenInst(SC.LHS, [](Inst *I){ return I->K == Inst::Phi;})) {
+    LHSHasPhi = true;
+  }
+
   findVars(Ante, InputVars);
 
-  InputVals = generateInputSets(InputVars);
+  if (!PCHasPhi) {
+    InputVals = generateInputSets(InputVars);
+  }
 
-  for (auto &&Input : InputVals) {
-    ConcreteInterpreters.emplace_back(SC.LHS, Input);
+  if (!LHSHasPhi && !PCHasPhi) {
+    for (auto &&Input : InputVals) {
+      ConcreteInterpreters.emplace_back(SC.LHS, Input);
+    }
   }
 
-  if (hasGivenInst(SC.LHS, [](Inst *I){ return I->K == Inst::Phi;})) {
+  if (LHSHasPhi) {
     // Have to abstract interpret LHS because of phi
-    LHSHasPhi = true;
     for (unsigned I = 0; I < InputVals.size(); I++) {
       LHSKnownBits.push_back(KnownBitsAnalysis().findKnownBits(SC.LHS, ConcreteInterpreters[I]));
       LHSConstantRange.push_back(ConstantRangeAnalysis().findConstantRange(SC.LHS, ConcreteInterpreters[I]));