Skip to content

Commit

Permalink
Generalization tool
Browse files Browse the repository at this point in the history
  • Loading branch information
@manasij7479
manasij7479 committed Dec 1, 2020
1 parent 6b7a271 commit 63c8fc3
Show file tree
Hide file tree
Showing 9 changed files with 305 additions and 45 deletions.
7 changes: 6 additions & 1 deletion CMakeLists.txt
View file
Original file line number Diff line number Diff line change
Expand Up @@ -295,6 +295,10 @@ add_executable(souper-check
tools/souper-check.cpp
)

add_executable(generalize
tools/generalize.cpp
)

add_executable(souper-interpret
tools/souper-interpret.cpp
)
Expand Down Expand Up @@ -362,7 +366,7 @@ configure_file(
)

foreach(target souper internal-solver-test lexer-test parser-test souper-check count-insts
souper2llvm souper-interpret
souper2llvm souper-interpret generalize
souperExtractor souperInfer souperInst souperKVStore souperParser
souperSMTLIB2 souperTool souperPass souperPassProfileAll kleeExpr
souperCodegen)
Expand Down Expand Up @@ -400,6 +404,7 @@ target_link_libraries(internal-solver-test souperSMTLIB2)
target_link_libraries(lexer-test souperParser)
target_link_libraries(parser-test souperParser)
target_link_libraries(souper-check souperTool souperExtractor souperKVStore souperSMTLIB2 souperParser ${HIREDIS_LIBRARY} ${ALIVE_LIBRARY} ${Z3_LIBRARY})
target_link_libraries(generalize souperTool souperExtractor souperKVStore souperSMTLIB2 souperParser ${HIREDIS_LIBRARY} ${ALIVE_LIBRARY} ${Z3_LIBRARY})
target_link_libraries(souper-interpret souperTool souperExtractor souperKVStore souperSMTLIB2 souperParser ${HIREDIS_LIBRARY} ${ALIVE_LIBRARY} ${Z3_LIBRARY})
target_link_libraries(clang-souper souperClangTool souperExtractor souperKVStore souperParser souperSMTLIB2 souperTool kleeExpr ${CLANG_LIBS} ${LLVM_LIBS} ${LLVM_LDFLAGS} ${HIREDIS_LIBRARY} ${ALIVE_LIBRARY} ${Z3_LIBRARY})
target_link_libraries(count-insts souperParser)
Expand Down
10 changes: 8 additions & 2 deletions include/souper/Extractor/Solver.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,6 +44,12 @@ class Solver {
InstMapping Mapping, bool &IsValid,
std::vector<std::pair<Inst *, llvm::APInt>> *Model) = 0;

virtual std::error_code
isSatisfiable(llvm::StringRef Query, bool &Result,
unsigned NumModels,
std::vector<llvm::APInt> *Models,
unsigned Timeout = 0) = 0;

virtual std::string getName() = 0;

virtual
Expand Down Expand Up @@ -90,8 +96,8 @@ class Solver {
virtual
std::error_code abstractPrecondition(const BlockPCs &BPCs,
const std::vector<InstMapping> &PCs,
InstMapping &Mapping, InstContext &IC,
bool &FoundWeakest) = 0;
InstMapping &Mapping, InstContext &IC, bool &FoundWeakest,
std::vector<std::map<Inst *, llvm::KnownBits>> &Results) = 0;
};

std::unique_ptr<Solver> createBaseSolver(
Expand Down
2 changes: 1 addition & 1 deletion include/souper/Infer/Preconditions.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,7 +9,7 @@ class SMTLIBSolver;
class Solver;
std::vector<std::map<Inst *, llvm::KnownBits>>
inferAbstractKBPreconditions(SynthesisContext &SC, Inst *RHS,
SMTLIBSolver *SMTSolver, Solver *S, bool &FoundWeakest);
Solver *S, bool &FoundWeakest);
}

#endif // SOUPER_PRECONDITIONS_H
66 changes: 30 additions & 36 deletions lib/Extractor/Solver.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -265,39 +265,12 @@ class BaseSolver : public Solver {

std::error_code abstractPrecondition(const BlockPCs &BPCs,
const std::vector<InstMapping> &PCs,
InstMapping &Mapping, InstContext &IC,
bool &FoundWeakest) override {
InstMapping &Mapping, InstContext &IC, bool &FoundWeakest,
std::vector<std::map<Inst *, llvm::KnownBits>> &Results) override {
SynthesisContext SC{IC, SMTSolver.get(), Mapping.LHS, /*LHSUB*/nullptr, PCs,
BPCs, /*CheckAllGuesses=*/false, Timeout};

std::vector<std::map<Inst *, llvm::KnownBits>> Results =
inferAbstractKBPreconditions(SC, Mapping.RHS, SMTSolver.get(), this, FoundWeakest);

ReplacementContext RC;
auto LHSStr = RC.printInst(Mapping.LHS, llvm::outs(), true);
llvm::outs() << "infer " << LHSStr << "\n";
auto RHSStr = RC.printInst(Mapping.RHS, llvm::outs(), true);
llvm::outs() << "result " << RHSStr << "\n";
for (size_t i = 0; i < Results.size(); ++i) {
for (auto It = Results[i].begin(); It != Results[i].end(); ++It) {
auto &&P = *It;
std::string dummy;
llvm::raw_string_ostream str(dummy);
auto VarStr = RC.printInst(P.first, str, false);
llvm::outs() << VarStr << " -> " << Inst::getKnownBitsString(P.second.Zero, P.second.One);

auto Next = It;
Next++;
if (Next != Results[i].end()) {
llvm::outs() << " (and) ";
}
}
if (i == Results.size() - 1) {
llvm::outs() << "\n";
} else {
llvm::outs() << "\n(or)\n";
}
}
Results = inferAbstractKBPreconditions(SC, Mapping.RHS, this, FoundWeakest);
return {};
}

Expand Down Expand Up @@ -461,6 +434,13 @@ class BaseSolver : public Solver {
return EC;
}

std::error_code isSatisfiable(llvm::StringRef Query, bool &Result,
unsigned NumModels,
std::vector<llvm::APInt> *Models,
unsigned Timeout = 0) override {
return SMTSolver->isSatisfiable(Query, Result, NumModels, Models, Timeout);
}

std::error_code isValid(InstContext &IC, const BlockPCs &BPCs,
const std::vector<InstMapping> &PCs,
InstMapping Mapping, bool &IsValid,
Expand Down Expand Up @@ -717,6 +697,13 @@ class MemCachingSolver : public Solver {
}
}

std::error_code isSatisfiable(llvm::StringRef Query, bool &Result,
unsigned NumModels,
std::vector<llvm::APInt> *Models,
unsigned Timeout = 0) override {
return UnderlyingSolver->isSatisfiable(Query, Result, NumModels, Models, Timeout);
}

std::string getName() override {
return UnderlyingSolver->getName() + " + internal cache";
}
Expand Down Expand Up @@ -745,9 +732,9 @@ class MemCachingSolver : public Solver {

std::error_code abstractPrecondition(const BlockPCs &BPCs,
const std::vector<InstMapping> &PCs,
InstMapping &Mapping, InstContext &IC,
bool &FoundWeakest) override {
return UnderlyingSolver->abstractPrecondition(BPCs, PCs, Mapping, IC, FoundWeakest);
InstMapping &Mapping, InstContext &IC, bool &FoundWeakest,
std::vector<std::map<Inst *, llvm::KnownBits>> &Results) override {
return UnderlyingSolver->abstractPrecondition(BPCs, PCs, Mapping, IC, FoundWeakest, Results);
}

std::error_code knownBits(const BlockPCs &BPCs,
Expand Down Expand Up @@ -847,6 +834,13 @@ class ExternalCachingSolver : public Solver {
return UnderlyingSolver->constantRange(BPCs, PCs, LHS, IC);
}

std::error_code isSatisfiable(llvm::StringRef Query, bool &Result,
unsigned NumModels,
std::vector<llvm::APInt> *Models,
unsigned Timeout = 0) override {
return UnderlyingSolver->isSatisfiable(Query, Result, NumModels, Models, Timeout);
}

std::error_code isValid(InstContext &IC, const BlockPCs &BPCs,
const std::vector<InstMapping> &PCs,
InstMapping Mapping, bool &IsValid,
Expand Down Expand Up @@ -885,9 +879,9 @@ class ExternalCachingSolver : public Solver {

std::error_code abstractPrecondition(const BlockPCs &BPCs,
const std::vector<InstMapping> &PCs,
InstMapping &Mapping, InstContext &IC,
bool &FoundWeakest) override {
return UnderlyingSolver->abstractPrecondition(BPCs, PCs, Mapping, IC, FoundWeakest);
InstMapping &Mapping, InstContext &IC, bool &FoundWeakest,
std::vector<std::map<Inst *, llvm::KnownBits>> &Results) override {
return UnderlyingSolver->abstractPrecondition(BPCs, PCs, Mapping, IC, FoundWeakest, Results);
}

std::error_code knownBits(const BlockPCs &BPCs,
Expand Down
9 changes: 6 additions & 3 deletions lib/Infer/Preconditions.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ using llvm::APInt;
namespace souper {
std::vector<std::map<Inst *, llvm::KnownBits>>
inferAbstractKBPreconditions(SynthesisContext &SC, Inst *RHS,
SMTLIBSolver *SMTSolver, Solver *S, bool &FoundWeakest) {
Solver *S, bool &FoundWeakest) {
InstMapping Mapping(SC.LHS, RHS);
bool Valid;
if (DebugLevel >= 3) {
Expand All @@ -20,7 +20,10 @@ std::vector<std::map<Inst *, llvm::KnownBits>>
}
std::vector<InstMapping> PCCopy = SC.PCs;
if (Valid) {
llvm::outs() << "Already valid.\n";
FoundWeakest = true;
if (DebugLevel > 1) {
llvm::errs() << "Already valid.\n";
}
return {};
}

Expand Down Expand Up @@ -97,7 +100,7 @@ std::vector<std::map<Inst *, llvm::KnownBits>>
&ModelInsts, Precondition, true);


SMTSolver->isSatisfiable(Query, FoundWeakest, ModelInsts.size(),
S->isSatisfiable(Query, FoundWeakest, ModelInsts.size(),
&ModelVals, SC.Timeout);

std::map<Inst *, llvm::KnownBits> Known;
Expand Down
42 changes: 42 additions & 0 deletions test/Generalize/fixit.opt
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,42 @@
; REQUIRES: solver, synthesis
; RUN: %generalize -fixit %s | %souper-check > %t
; RUN: %FileCheck %s < %t

%x:i8 = var
%y:i8 = var
%z = add %x, %y
%t = add %z, 42
%u = sub %t, %y
infer %u
%v = add %x, 42
result %v
;CHECK: LGTM

%x:i8 = var
%y:i8 = var
%t = add %x, 42
%u = sub %t, %y
infer %u
%v = add %x, 42
result %v
;CHECK: LGTM

%x:i8 = var
%y:i8 = var
%t = and %x, 137
%u = xor %t, %y
infer %u
%v = or %x, %y
result %v
;CHECK: LGTM
;CHECK-NEXT: LGTM

%x:i8 = var
%y:i8 = var
%t = or %x, 42
%u = and %t, %y
infer %u
%v = and %x, %y
result %v
;CHECK: LGTM
;CHECK-NEXT: LGTM
22 changes: 22 additions & 0 deletions test/Generalize/leaf.opt
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,22 @@
; REQUIRES: solver, synthesis
; RUN: %generalize -remove-leaf %s | %souper-check > %t
; RUN: %FileCheck %s < %t

%x:i8 = var
%y:i8 = var
%masked = and %x, 3
%and = and %masked, %y
%foo = lshr %and, 2
infer %and
result 0:i8
; CHECK: LGTM
; CHECK: LGTM

%x:i8 = var
%y:i8 = var
%a = and %x, 15
%b = and %y, 240
%foo = or %a, %b
infer %foo
result 0:i8
; CHECK: LGTM
Loading

0 comments on commit 63c8fc3

Please sign in to comment.