handle freeze in alive double-check

include/souper/Inst/Inst.h

@@ -185,6 +185,7 @@ struct Inst : llvm::FoldingSetNode {
   std::vector<llvm::ConstantRange> RangeRefinement;
   int nReservedConsts = -1;
   int nHoles = -1;
+  bool IsBorder = false;
 };
 
 /// A mapping from an Inst to a replacement. This may either represent a

lib/Infer/EnumerativeSynthesis.cpp

@@ -34,7 +34,7 @@ using namespace souper;
 using namespace llvm;
 
 static const std::vector<Inst::Kind> UnaryOperators = {
-  Inst::CtPop, Inst::BSwap, Inst::BitReverse, Inst::Cttz, Inst::Ctlz, Inst::Freeze
+  Inst::CtPop, Inst::BSwap, Inst::BitReverse, Inst::Cttz, Inst::Ctlz
 };
 
 static const std::vector<Inst::Kind> BinaryOperators = {
@@ -207,10 +207,6 @@ bool getGuesses(const std::vector<Inst *> &Inputs,
     unaryExclList.push_back(Inst::BitReverse);
   }
 
-  // disable generating freeze of freeze
-  if (unaryHoleUsers.size() == 1 && unaryHoleUsers[0]->K == Inst::Freeze)
-    unaryExclList.push_back(Inst::Freeze);
-
   std::vector<Inst *> PartialGuesses;
 
   std::vector<Inst *> Comps(Inputs.begin(), Inputs.end());
@@ -231,9 +227,6 @@ bool getGuesses(const std::vector<Inst *> &Inputs,
     if (std::find(unaryExclList.begin(), unaryExclList.end(), K) != unaryExclList.end())
       continue;
 
-    if (K != Inst::Freeze && Width <= 1)
-      continue;
-
     for (auto Comp : Comps) {
       if (K == Inst::BSwap && Width % 16 != 0)
         continue;
@@ -727,6 +720,51 @@ bool isBigQuerySat(SynthesisContext &SC,
   return BigQueryIsSat;
 }
 
+// if B == NULL, insert freeze to each border, otherwise replace all (freeze B) with B
+static Inst *FreezeCopy(Inst *I, InstContext &IC,
+                        std::map<Inst *, Inst *> &InstCache,
+                        std::map<Block *, Block *> &BlockCache,
+                        Inst *B) {
+
+  if (InstCache.count(I))
+    return InstCache.at(I);
+
+  std::vector<Inst *> Ops;
+  for (auto const &Op : I->Ops) {
+    Ops.push_back(FreezeCopy(Op, IC, InstCache, BlockCache, B));
+  }
+
+  Inst *Copy = 0;
+  if (!B && I->IsBorder) {
+    // explicitly forbid cloning the parameter of freeze
+    Copy = IC.getInst(Inst::Freeze, I->Width, { I }, I->DemandedBits, I->Available);
+  } else if (I->K == Inst::Freeze) {
+    if (I->Ops[0] == B) {
+      Copy = Ops[0];
+    } else {
+      // ditto
+      Copy = IC.getInst(Inst::Freeze, I->Width, { I->Ops[0] }, I->DemandedBits, I->Available);
+    }
+  } else if (I->K == Inst::Var) {
+    Copy = I;
+  } else if (I->K == Inst::Phi) {
+    if (!BlockCache.count(I->B)) {
+      auto BlockCopy = IC.createBlock(I->B->Preds);
+      BlockCache[I->B] = BlockCopy;
+      Copy = IC.getPhi(BlockCopy, Ops, I->DemandedBits);
+    } else {
+      Copy = IC.getPhi(BlockCache.at(I->B), Ops, I->DemandedBits);
+    }
+  } else if (I->K == Inst::Const || I->K == Inst::UntypedConst) {
+    Copy = I;
+  } else {
+    Copy = IC.getInst(I->K, I->Width, Ops, I->DemandedBits, I->Available);
+  }
+  assert(Copy);
+  InstCache[I] = Copy;
+  return Copy;
+}
+
 std::error_code synthesizeWithKLEE(SynthesisContext &SC, std::vector<Inst *> &RHSs,
                                    const std::vector<souper::Inst *> &Guesses) {
   std::error_code EC;
@@ -788,13 +826,48 @@ std::error_code synthesizeWithKLEE(SynthesisContext &SC, std::vector<Inst *> &RH
 
     if (DoubleCheckWithAlive) {
       if (!isTransformationValid(SC.LHS, RHS, SC.PCs, SC.IC)) {
-        llvm::errs() << "Transformation proved wrong by alive.\n";
-        ReplacementContext RC;
-        auto str = RC.printInst(SC.LHS, llvm::errs(), /*printNames=*/true);
-        llvm::errs() << "infer " << str << "\n";
-        str = RC.printInst(RHS, llvm::errs(), /*printNames=*/true);
-        llvm::errs() << "result " << str << "\n";
-        RHS = nullptr;
+        std::map<Inst *, Inst *> InstCache;
+        std::map<Block *, Block *> BlockCache;
+
+        Inst *F = FreezeCopy(RHS, SC.IC, InstCache, BlockCache, nullptr);
+
+        if (!isTransformationValid(SC.LHS, F, SC.PCs, SC.IC)) {
+          llvm::errs() << "Error: transformation proved wrong by alive, even with freeze inserted in border\n\n";
+          ReplacementContext RC;
+          RC.printInst(SC.LHS, llvm::errs(), /*printNames=*/true);
+          llvm::errs() << "\n=>\n\n";
+          RC.printInst(RHS, llvm::errs(), /*printNames=*/true);
+          llvm::errs() << "\n; RHS after inserting freeze \n\n";
+          RC.printInst(F, llvm::errs(), /*printNames=*/true);
+          RHS = nullptr;
+          return EC;
+        }
+
+        // Get border insts
+        std::set<Inst *> Visited;
+        std::vector<Inst *> Borders;
+        std::queue<Inst *> Q;
+        Q.push(RHS);
+        while (!Q.empty()) {
+          Inst *I = Q.front();
+          Q.pop();
+          if (I->IsBorder)
+            Borders.push_back(I);
+          if (Visited.insert(I).second)
+            for (auto Op : I->orderedOps())
+              Q.push(Op);
+        }
+        // Remove freezes
+        for (auto Border : Borders) {
+          auto I = F;
+          InstCache.clear();
+          BlockCache.clear();
+          F = FreezeCopy(F, SC.IC, InstCache, BlockCache, Border);
+          if (!isTransformationValid(SC.LHS, F, SC.PCs, SC.IC)) {
+            F = I;
+          }
+        }
+        RHS = F;
       }
     }
     if (RHS) {

lib/Inst/Inst.cpp

@@ -1084,6 +1084,7 @@ void souper::findCands(Inst *Root, std::vector<Inst *> &Guesses,
             I->K == Inst::SSubWithOverflow || I->K == Inst::USubWithOverflow ||
             I->K == Inst::SMulWithOverflow || I->K == Inst::UMulWithOverflow)
           continue;
+        I->IsBorder = true;
         Guesses.emplace_back(I);
         if (Guesses.size() >= Max)
           return;

test/Infer/double-check-freeze-removal-1.opt

@@ -0,0 +1,15 @@
+; REQUIRES: solver, solver-model
+
+; RUN: %souper-check %solver -infer-rhs -souper-infer-iN=false -souper-enumerative-synthesis -souper-double-check %s > %t1
+; RUN: %FileCheck %s < %t1
+
+; CHECK: %5:i1 = freeze %3
+; CHECK: %6:i1 = or %1, %5
+
+
+%0:i8 = var ; 0
+%1:i1 = eq 0:i8, %0
+%2:i8 = var ; 1
+%3:i1 = eq 0:i8, %2
+%4:i1 = select %1, 1:i1, %3
+infer %4

test/Infer/double-check-freeze-removal-2.opt

@@ -0,0 +1,14 @@
+; REQUIRES: solver, solver-model
+
+; RUN: %souper-check %solver -infer-rhs -souper-infer-iN=false -souper-enumerative-synthesis -souper-double-check %s > %t1
+; RUN: %FileCheck %s < %t1
+
+; CHECK: %5:i1 = freeze %1
+; CHECK: %6:i1 = or %3, %5
+
+%0:i8 = var ; 0
+%1:i1 = eq 0:i8, %0
+%2:i8 = var ; 1
+%3:i1 = eq 0:i8, %2
+%4:i1 = select %3, 1:i1, %1
+infer %4

test/Infer/double-check-freeze-removal-3.opt

@@ -0,0 +1,15 @@
+; REQUIRES: solver, solver-model
+
+; RUN: %souper-check %solver -infer-rhs -souper-infer-iN=false -souper-enumerative-synthesis -souper-double-check %s > %t1
+; RUN: %FileCheck %s < %t1
+
+; CHECK: %6:i1 = freeze %2
+; CHECK: %7:i1 = or %4, %6
+
+%0:i1 = var ; 0
+%1:i1 = var ; 1
+%2:i1 = and %0, %1
+%3:i8 = var ; 2
+%4:i1 = eq 0:i8, %3
+%5:i1 = select %4, 1:i1, %2
+infer %5

test/Infer/double-check-freeze-removal-4.opt

@@ -0,0 +1,23 @@
+; REQUIRES: solver, solver-model, long-duration-synthesis
+
+; RUN: %souper-check %solver -infer-rhs -souper-infer-iN=false -souper-enumerative-synthesis -souper-double-check -souper-enumerative-synthesis-num-instructions=2 -souper-check-all-guesses %s > %t1
+; RUN: %FileCheck %s < %t1
+
+; CHECK: %0:i1 = var
+; CHECK: %1:i1 = var
+; CHECK: %2:i1 = freeze %1
+; CHECK: %3:i1 = var
+; CHECK: %4:i1 = freeze %3
+; CHECK: %5:i1 = and %2, %4
+; CHECK: %6:i1 = or %0, %5
+; CHECK: result %6
+
+%0:i1 = var
+%1:i1 = var
+; make cost model happy
+%2:i1 = eq %0, 1:i1
+%3:i1 = eq %1, 1:i1
+%4:i1 = and %2, %3
+%5:i1 = var
+%6:i1 = select %5, 1:i1, %4
+infer %6

test/Infer/multiple-rhs1.opt

@@ -5,8 +5,6 @@
 ; RUN: %FileCheck %s < %t2
 
 ; CHECK: result %0
-; CHECK: %1:i8 = freeze %0
-; CHECK-NEXT: result %1
 
 %0:i8 = var
 %1:i8 = add 1:i8, %0

test/Infer/syn-double-insts/syn-freeze-or.opt

@@ -1,7 +1,8 @@
-; REQUIRES: solver, synthesis
+; REQUIRES: solver, synthesis, unsupported
 ; RUN: %souper-check -infer-rhs -souper-enumerative-synthesis -souper-use-alive -souper-enumerative-synthesis-num-instructions=2 -souper-dataflow-pruning %solver %s > %t1
 ; RUN: %FileCheck %s < %t1
 
+; No longer supported, freeze synthesis is now handled by alive double-check
 ; synthesis freeze
 ; takes about a minute