Do not generate inputs when PC has PHI

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;

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);
     }

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());
   }

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]));