From c438addfb2b21c4d242d965200a7d2e99f4bf4aa Mon Sep 17 00:00:00 2001 From: Zhengyang Liu Date: Mon, 20 Apr 2020 20:20:52 -0600 Subject: [PATCH] alive double check freeze removal --- include/souper/Inst/Inst.h | 1 + lib/Infer/EnumerativeSynthesis.cpp | 103 +++++++++++++++--- lib/Inst/Inst.cpp | 1 + test/Infer/double-check-freeze-removal-1.opt | 15 +++ test/Infer/double-check-freeze-removal-2.opt | 14 +++ test/Infer/double-check-freeze-removal-3.opt | 15 +++ test/Infer/double-check-freeze-removal-4.opt | 23 ++++ test/Infer/multiple-rhs1.opt | 2 - test/Infer/syn-double-insts/syn-freeze-or.opt | 3 +- 9 files changed, 159 insertions(+), 18 deletions(-) create mode 100644 test/Infer/double-check-freeze-removal-1.opt create mode 100644 test/Infer/double-check-freeze-removal-2.opt create mode 100644 test/Infer/double-check-freeze-removal-3.opt create mode 100644 test/Infer/double-check-freeze-removal-4.opt diff --git a/include/souper/Inst/Inst.h b/include/souper/Inst/Inst.h index 2941978aa..e906ef006 100644 --- a/include/souper/Inst/Inst.h +++ b/include/souper/Inst/Inst.h @@ -185,6 +185,7 @@ struct Inst : llvm::FoldingSetNode { std::vector RangeRefinement; int nReservedConsts = -1; int nHoles = -1; + bool IsBorder = false; }; /// A mapping from an Inst to a replacement. This may either represent a diff --git a/lib/Infer/EnumerativeSynthesis.cpp b/lib/Infer/EnumerativeSynthesis.cpp index 21c9b9f4d..823c9edfe 100644 --- a/lib/Infer/EnumerativeSynthesis.cpp +++ b/lib/Infer/EnumerativeSynthesis.cpp @@ -34,7 +34,7 @@ using namespace souper; using namespace llvm; static const std::vector 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 BinaryOperators = { @@ -207,10 +207,6 @@ bool getGuesses(const std::vector &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 PartialGuesses; std::vector Comps(Inputs.begin(), Inputs.end()); @@ -231,9 +227,6 @@ bool getGuesses(const std::vector &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 &InstCache, + std::map &BlockCache, + Inst *B) { + + if (InstCache.count(I)) + return InstCache.at(I); + + std::vector 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 &RHSs, const std::vector &Guesses) { std::error_code EC; @@ -788,13 +826,48 @@ std::error_code synthesizeWithKLEE(SynthesisContext &SC, std::vector &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 InstCache; + std::map 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 Visited; + std::vector Borders; + std::queue 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) { diff --git a/lib/Inst/Inst.cpp b/lib/Inst/Inst.cpp index 407d7d65d..9f0701d83 100644 --- a/lib/Inst/Inst.cpp +++ b/lib/Inst/Inst.cpp @@ -1084,6 +1084,7 @@ void souper::findCands(Inst *Root, std::vector &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; diff --git a/test/Infer/double-check-freeze-removal-1.opt b/test/Infer/double-check-freeze-removal-1.opt new file mode 100644 index 000000000..9230302fc --- /dev/null +++ b/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 diff --git a/test/Infer/double-check-freeze-removal-2.opt b/test/Infer/double-check-freeze-removal-2.opt new file mode 100644 index 000000000..a4093b1f3 --- /dev/null +++ b/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 diff --git a/test/Infer/double-check-freeze-removal-3.opt b/test/Infer/double-check-freeze-removal-3.opt new file mode 100644 index 000000000..0a42a1c65 --- /dev/null +++ b/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 diff --git a/test/Infer/double-check-freeze-removal-4.opt b/test/Infer/double-check-freeze-removal-4.opt new file mode 100644 index 000000000..cf589416b --- /dev/null +++ b/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 diff --git a/test/Infer/multiple-rhs1.opt b/test/Infer/multiple-rhs1.opt index 96eaf8cb0..1bd90c8b7 100644 --- a/test/Infer/multiple-rhs1.opt +++ b/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 diff --git a/test/Infer/syn-double-insts/syn-freeze-or.opt b/test/Infer/syn-double-insts/syn-freeze-or.opt index 1194d36b6..6930d11e2 100644 --- a/test/Infer/syn-double-insts/syn-freeze-or.opt +++ b/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