Skip to content
This repository was archived by the owner on Oct 30, 2025. It is now read-only.

Commit c438add

Browse files
zhengyang92zhengyang92
committed
alive double check freeze removal
1 parent 5b78c3d commit c438add

9 files changed

Lines changed: 159 additions & 18 deletions

File tree

‎include/souper/Inst/Inst.h‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -185,6 +185,7 @@ struct Inst : llvm::FoldingSetNode {
185185
std::vector<llvm::ConstantRange> RangeRefinement;
186186
int nReservedConsts = -1;
187187
int nHoles = -1;
188+
bool IsBorder = false;
188189
};
189190

190191
/// A mapping from an Inst to a replacement. This may either represent a

‎lib/Infer/EnumerativeSynthesis.cpp‎

Lines changed: 88 additions & 15 deletions
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ using namespace souper;
3434
using namespace llvm;
3535

3636
static const std::vector<Inst::Kind> UnaryOperators = {
37-
Inst::CtPop, Inst::BSwap, Inst::BitReverse, Inst::Cttz, Inst::Ctlz, Inst::Freeze
37+
Inst::CtPop, Inst::BSwap, Inst::BitReverse, Inst::Cttz, Inst::Ctlz
3838
};
3939

4040
static const std::vector<Inst::Kind> BinaryOperators = {
@@ -207,10 +207,6 @@ bool getGuesses(const std::vector<Inst *> &Inputs,
207207
unaryExclList.push_back(Inst::BitReverse);
208208
}
209209

210-
// disable generating freeze of freeze
211-
if (unaryHoleUsers.size() == 1 && unaryHoleUsers[0]->K == Inst::Freeze)
212-
unaryExclList.push_back(Inst::Freeze);
213-
214210
std::vector<Inst *> PartialGuesses;
215211

216212
std::vector<Inst *> Comps(Inputs.begin(), Inputs.end());
@@ -231,9 +227,6 @@ bool getGuesses(const std::vector<Inst *> &Inputs,
231227
if (std::find(unaryExclList.begin(), unaryExclList.end(), K) != unaryExclList.end())
232228
continue;
233229

234-
if (K != Inst::Freeze && Width <= 1)
235-
continue;
236-
237230
for (auto Comp : Comps) {
238231
if (K == Inst::BSwap && Width % 16 != 0)
239232
continue;
@@ -727,6 +720,51 @@ bool isBigQuerySat(SynthesisContext &SC,
727720
return BigQueryIsSat;
728721
}
729722

723+
// if B == NULL, insert freeze to each border, otherwise replace all (freeze B) with B
724+
static Inst *FreezeCopy(Inst *I, InstContext &IC,
725+
std::map<Inst *, Inst *> &InstCache,
726+
std::map<Block *, Block *> &BlockCache,
727+
Inst *B) {
728+
729+
if (InstCache.count(I))
730+
return InstCache.at(I);
731+
732+
std::vector<Inst *> Ops;
733+
for (auto const &Op : I->Ops) {
734+
Ops.push_back(FreezeCopy(Op, IC, InstCache, BlockCache, B));
735+
}
736+
737+
Inst *Copy = 0;
738+
if (!B && I->IsBorder) {
739+
// explicitly forbid cloning the parameter of freeze
740+
Copy = IC.getInst(Inst::Freeze, I->Width, { I }, I->DemandedBits, I->Available);
741+
} else if (I->K == Inst::Freeze) {
742+
if (I->Ops[0] == B) {
743+
Copy = Ops[0];
744+
} else {
745+
// ditto
746+
Copy = IC.getInst(Inst::Freeze, I->Width, { I->Ops[0] }, I->DemandedBits, I->Available);
747+
}
748+
} else if (I->K == Inst::Var) {
749+
Copy = I;
750+
} else if (I->K == Inst::Phi) {
751+
if (!BlockCache.count(I->B)) {
752+
auto BlockCopy = IC.createBlock(I->B->Preds);
753+
BlockCache[I->B] = BlockCopy;
754+
Copy = IC.getPhi(BlockCopy, Ops, I->DemandedBits);
755+
} else {
756+
Copy = IC.getPhi(BlockCache.at(I->B), Ops, I->DemandedBits);
757+
}
758+
} else if (I->K == Inst::Const || I->K == Inst::UntypedConst) {
759+
Copy = I;
760+
} else {
761+
Copy = IC.getInst(I->K, I->Width, Ops, I->DemandedBits, I->Available);
762+
}
763+
assert(Copy);
764+
InstCache[I] = Copy;
765+
return Copy;
766+
}
767+
730768
std::error_code synthesizeWithKLEE(SynthesisContext &SC, std::vector<Inst *> &RHSs,
731769
const std::vector<souper::Inst *> &Guesses) {
732770
std::error_code EC;
@@ -788,13 +826,48 @@ std::error_code synthesizeWithKLEE(SynthesisContext &SC, std::vector<Inst *> &RH
788826

789827
if (DoubleCheckWithAlive) {
790828
if (!isTransformationValid(SC.LHS, RHS, SC.PCs, SC.IC)) {
791-
llvm::errs() << "Transformation proved wrong by alive.\n";
792-
ReplacementContext RC;
793-
auto str = RC.printInst(SC.LHS, llvm::errs(), /*printNames=*/true);
794-
llvm::errs() << "infer " << str << "\n";
795-
str = RC.printInst(RHS, llvm::errs(), /*printNames=*/true);
796-
llvm::errs() << "result " << str << "\n";
797-
RHS = nullptr;
829+
std::map<Inst *, Inst *> InstCache;
830+
std::map<Block *, Block *> BlockCache;
831+
832+
Inst *F = FreezeCopy(RHS, SC.IC, InstCache, BlockCache, nullptr);
833+
834+
if (!isTransformationValid(SC.LHS, F, SC.PCs, SC.IC)) {
835+
llvm::errs() << "Error: transformation proved wrong by alive, even with freeze inserted in border\n\n";
836+
ReplacementContext RC;
837+
RC.printInst(SC.LHS, llvm::errs(), /*printNames=*/true);
838+
llvm::errs() << "\n=>\n\n";
839+
RC.printInst(RHS, llvm::errs(), /*printNames=*/true);
840+
llvm::errs() << "\n; RHS after inserting freeze \n\n";
841+
RC.printInst(F, llvm::errs(), /*printNames=*/true);
842+
RHS = nullptr;
843+
return EC;
844+
}
845+
846+
// Get border insts
847+
std::set<Inst *> Visited;
848+
std::vector<Inst *> Borders;
849+
std::queue<Inst *> Q;
850+
Q.push(RHS);
851+
while (!Q.empty()) {
852+
Inst *I = Q.front();
853+
Q.pop();
854+
if (I->IsBorder)
855+
Borders.push_back(I);
856+
if (Visited.insert(I).second)
857+
for (auto Op : I->orderedOps())
858+
Q.push(Op);
859+
}
860+
// Remove freezes
861+
for (auto Border : Borders) {
862+
auto I = F;
863+
InstCache.clear();
864+
BlockCache.clear();
865+
F = FreezeCopy(F, SC.IC, InstCache, BlockCache, Border);
866+
if (!isTransformationValid(SC.LHS, F, SC.PCs, SC.IC)) {
867+
F = I;
868+
}
869+
}
870+
RHS = F;
798871
}
799872
}
800873
if (RHS) {

‎lib/Inst/Inst.cpp‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1084,6 +1084,7 @@ void souper::findCands(Inst *Root, std::vector<Inst *> &Guesses,
10841084
I->K == Inst::SSubWithOverflow || I->K == Inst::USubWithOverflow ||
10851085
I->K == Inst::SMulWithOverflow || I->K == Inst::UMulWithOverflow)
10861086
continue;
1087+
I->IsBorder = true;
10871088
Guesses.emplace_back(I);
10881089
if (Guesses.size() >= Max)
10891090
return;

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

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
; REQUIRES: solver, solver-model
2+
3+
; RUN: %souper-check %solver -infer-rhs -souper-infer-iN=false -souper-enumerative-synthesis -souper-double-check %s > %t1
4+
; RUN: %FileCheck %s < %t1
5+
6+
; CHECK: %5:i1 = freeze %3
7+
; CHECK: %6:i1 = or %1, %5
8+
9+
10+
%0:i8 = var ; 0
11+
%1:i1 = eq 0:i8, %0
12+
%2:i8 = var ; 1
13+
%3:i1 = eq 0:i8, %2
14+
%4:i1 = select %1, 1:i1, %3
15+
infer %4

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

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,14 @@
1+
; REQUIRES: solver, solver-model
2+
3+
; RUN: %souper-check %solver -infer-rhs -souper-infer-iN=false -souper-enumerative-synthesis -souper-double-check %s > %t1
4+
; RUN: %FileCheck %s < %t1
5+
6+
; CHECK: %5:i1 = freeze %1
7+
; CHECK: %6:i1 = or %3, %5
8+
9+
%0:i8 = var ; 0
10+
%1:i1 = eq 0:i8, %0
11+
%2:i8 = var ; 1
12+
%3:i1 = eq 0:i8, %2
13+
%4:i1 = select %3, 1:i1, %1
14+
infer %4

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

Lines changed: 15 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
; REQUIRES: solver, solver-model
2+
3+
; RUN: %souper-check %solver -infer-rhs -souper-infer-iN=false -souper-enumerative-synthesis -souper-double-check %s > %t1
4+
; RUN: %FileCheck %s < %t1
5+
6+
; CHECK: %6:i1 = freeze %2
7+
; CHECK: %7:i1 = or %4, %6
8+
9+
%0:i1 = var ; 0
10+
%1:i1 = var ; 1
11+
%2:i1 = and %0, %1
12+
%3:i8 = var ; 2
13+
%4:i1 = eq 0:i8, %3
14+
%5:i1 = select %4, 1:i1, %2
15+
infer %5

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

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
; REQUIRES: solver, solver-model, long-duration-synthesis
2+
3+
; 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
4+
; RUN: %FileCheck %s < %t1
5+
6+
; CHECK: %0:i1 = var
7+
; CHECK: %1:i1 = var
8+
; CHECK: %2:i1 = freeze %1
9+
; CHECK: %3:i1 = var
10+
; CHECK: %4:i1 = freeze %3
11+
; CHECK: %5:i1 = and %2, %4
12+
; CHECK: %6:i1 = or %0, %5
13+
; CHECK: result %6
14+
15+
%0:i1 = var
16+
%1:i1 = var
17+
; make cost model happy
18+
%2:i1 = eq %0, 1:i1
19+
%3:i1 = eq %1, 1:i1
20+
%4:i1 = and %2, %3
21+
%5:i1 = var
22+
%6:i1 = select %5, 1:i1, %4
23+
infer %6

‎test/Infer/multiple-rhs1.opt‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,8 +5,6 @@
55
; RUN: %FileCheck %s < %t2
66

77
; CHECK: result %0
8-
; CHECK: %1:i8 = freeze %0
9-
; CHECK-NEXT: result %1
108

119
%0:i8 = var
1210
%1:i8 = add 1:i8, %0

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

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,8 @@
1-
; REQUIRES: solver, synthesis
1+
; REQUIRES: solver, synthesis, unsupported
22
; RUN: %souper-check -infer-rhs -souper-enumerative-synthesis -souper-use-alive -souper-enumerative-synthesis-num-instructions=2 -souper-dataflow-pruning %solver %s > %t1
33
; RUN: %FileCheck %s < %t1
44

5+
; No longer supported, freeze synthesis is now handled by alive double-check
56
; synthesis freeze
67
; takes about a minute
78

0 commit comments

Comments
 (0)