From 714a633b64629c35009f66646ebe23e2d76e16bc Mon Sep 17 00:00:00 2001
From: Manasij Mukherjee <manasij7479@gmail.com>
Date: Tue, 19 Feb 2019 20:35:29 -0700
Subject: [PATCH] Introduce pruning in the constant synthesis loop

---
 lib/Infer/ExhaustiveSynthesis.cpp | 59 ++++++++++++++++++-------------
 1 file changed, 35 insertions(+), 24 deletions(-)

diff --git a/lib/Infer/ExhaustiveSynthesis.cpp b/lib/Infer/ExhaustiveSynthesis.cpp
index 29894edf6..09945c5e4 100644
--- a/lib/Infer/ExhaustiveSynthesis.cpp
+++ b/lib/Infer/ExhaustiveSynthesis.cpp
@@ -631,35 +631,14 @@ bool isBigQuerySat(SynthesisContext &SC,
   return BigQueryIsSat;
 }
 
-void generateAndSortGuesses(InstContext &IC, Inst *LHS,
-                            std::vector<Inst *> &Guesses) {
-  std::vector<Inst *> Inputs;
-  findCands(LHS, Inputs, /*WidthMustMatch=*/false, /*FilterVars=*/false, MaxLHSCands);
-  if (DebugLevel > 1)
-    llvm::errs() << "got " << Inputs.size() << " candidates from LHS\n";
-
+void generateAndSortGuesses(InstContext &IC, Inst *LHS, const std::vector<Inst *> Inputs,
+                            std::vector<Inst *> &Guesses, PruneFunc PruneCallback) {
   int LHSCost = souper::cost(LHS, /*IgnoreDepsWithExternalUses=*/true);
 
   int TooExpensive = 0;
 
-  dataflow::DataflowPruningManager DataflowPruning
-    (LHS, Inputs, DebugLevel);
-  // Cheaper tests go first
-  std::vector<PruneFunc> PruneFuncs = {CostPrune};
-  if (EnableDataflowPruning) {
-    PruneFuncs.push_back(DataflowPruning.getPruneFunc());
-  }
-  auto PruneCallback = MkPruneFunc(PruneFuncs);
-  // TODO(zhengyangl): Refactor the syntactic pruning into a
-  // prune function here, between Cost and Dataflow
-  // TODO(manasij7479) : If RHS is concrete, evaluate both sides
-  // TODO(regehr?) : Solver assisted pruning (should be the last component)
-
   getGuesses(Guesses, Inputs, LHS->Width,
              LHSCost, IC, nullptr, nullptr, TooExpensive, PruneCallback);
-  if (DebugLevel >= 1) {
-    DataflowPruning.printStats(llvm::outs());
-  }
 
   // add nops guesses separately
   for (auto I : Inputs) {
@@ -822,7 +801,29 @@ ExhaustiveSynthesis::synthesize(SMTLIBSolver *SMTSolver,
 
   std::vector<Inst *> Guesses;
   std::error_code EC;
-  generateAndSortGuesses(IC, LHS, Guesses);
+
+  std::vector<Inst *> Inputs;
+  findCands(LHS, Inputs, /*WidthMustMatch=*/false, /*FilterVars=*/false, MaxLHSCands);
+  if (DebugLevel > 1)
+    llvm::errs() << "got " << Inputs.size() << " candidates from LHS\n";
+
+  dataflow::DataflowPruningManager DataflowPruning
+    (LHS, Inputs, DebugLevel);
+  // Cheaper tests go first
+  std::vector<PruneFunc> PruneFuncs = {CostPrune};
+  if (EnableDataflowPruning) {
+    PruneFuncs.push_back(DataflowPruning.getPruneFunc());
+  }
+  auto PruneCallback = MkPruneFunc(PruneFuncs);
+  // TODO(zhengyangl): Refactor the syntactic pruning into a
+  // prune function here, between Cost and Dataflow
+  // TODO(manasij7479) : If RHS is concrete, evaluate both sides
+  // TODO(regehr?) : Solver assisted pruning (should be the last component)
+
+  generateAndSortGuesses(IC, LHS, Inputs, Guesses, PruneCallback);
+  if (DebugLevel >= 1) {
+    DataflowPruning.printStats(llvm::outs());
+  }
 
   if (Guesses.empty()) {
     return EC;
@@ -883,6 +884,16 @@ ExhaustiveSynthesis::synthesize(SMTLIBSolver *SMTSolver,
       // TODO Utilize this for the mysterious constant synthesis 'loop'
     }
 
+    // Avoids calling isConcreteCandidateSat
+    std::vector<Inst *> Empty;
+    if (!PruneCallback(ConcreteRHS, Empty)) {
+      if (DebugLevel > 3)
+        llvm::errs() << "Constant proved infeasible with inequivalence checks\n";
+      Tries++;
+      if (GuessHasConstant && Tries < MaxTries)
+        goto again; // TODO: Remove goto.
+    }
+
     bool SecondSmallQueryIsSat;
     EC = isConcreteCandidateSat(SC, ConstMap, ConcreteRHS, SecondSmallQueryIsSat);
     if (EC) {