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

Multiple RHS Support #367

Open
zhengyang92 wants to merge 2 commits into
base: main
Choose a base branch
from
Open

Multiple RHS Support #367

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
63506cd
Multiple RHS Support
zhengyang92 Oct 10, 2018
fe011e0
remote redundant variable ValidRHS
zhengyang92 Oct 10, 2018
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
6 changes: 3 additions & 3 deletions include/souper/Extractor/Solver.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,11 +30,11 @@ class Solver {
public:
virtual ~Solver();
virtual std::error_code
infer(const BlockPCs &BPCs, const std::vector<InstMapping> &PCs,
Inst *LHS, Inst *&RHS, InstContext &IC) = 0;
infer(const BlockPCs &BPCs, const std::vector<InstMapping> &PCs,
Inst *LHS, std::vector<Inst *> &RHSs, InstContext &IC) = 0;
virtual std::error_code
isValid(InstContext &IC, const BlockPCs &BPCs,
const std::vector<InstMapping> &PCs,
const std::vector<InstMapping> &PCs,
InstMapping Mapping, bool &IsValid,
std::vector<std::pair<Inst *, llvm::APInt>> *Model) = 0;
virtual std::string getName() = 0;
Expand Down
2 changes: 1 addition & 1 deletion include/souper/Infer/ExhaustiveSynthesis.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@ class ExhaustiveSynthesis {
std::error_code synthesize(SMTLIBSolver *SMTSolver,
const BlockPCs &BPCs,
const std::vector<InstMapping> &PCs,
Inst *TargetLHS, Inst *&RHS,
Inst *TargetLHS, std::vector<Inst *> &RHS,
InstContext &IC, unsigned Timeout);

};
Expand Down
46 changes: 26 additions & 20 deletions lib/Extractor/Solver.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,7 +75,8 @@ class BaseSolver : public Solver {

std::error_code infer(const BlockPCs &BPCs,
const std::vector<InstMapping> &PCs,
Inst *LHS, Inst *&RHS, InstContext &IC) override {
Inst *LHS, std::vector<Inst *> &RHSs,
InstContext &IC) override {
std::error_code EC;

/*
Expand Down Expand Up @@ -103,7 +104,7 @@ class BaseSolver : public Solver {
if (EC)
return EC;
if (!IsSat) {
RHS = I;
RHSs.emplace_back(I);
Copy link
Contributor

@regehr regehr Oct 10, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

do you want to return here, or try to find more RHSs?

Copy link
Contributor Author

@zhengyang92 zhengyang92 Oct 10, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

These are both constant synthesis, why we wants to collect multiple RHSs if a constant fit the LHS

Copy link
Contributor

@regehr regehr Oct 10, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

well, it depends on why we want multiple RHSs. for manasij's purposes a constant is always good, but for building a cost model I'd like as many alternatives as possible

Copy link
Contributor Author

@zhengyang92 zhengyang92 Oct 10, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

ping me if you need this.

return EC;
}
}
Expand Down Expand Up @@ -142,7 +143,7 @@ class BaseSolver : public Solver {
if (EC)
return EC;
if (!IsSat) {
RHS = Const;
RHSs.emplace_back(Const);
Copy link
Contributor

@regehr regehr Oct 10, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

same

return EC;
}
}
Expand Down Expand Up @@ -188,7 +189,7 @@ class BaseSolver : public Solver {
if (EC)
return EC;
if (!SmallQueryIsSat) {
RHS = I;
RHSs.emplace_back(I);
break;
}
}
Expand All @@ -214,18 +215,21 @@ class BaseSolver : public Solver {
if(SMTSolver->supportsModels()) {
if (EnableExhaustiveSynthesis) {
ExhaustiveSynthesis ES;
EC = ES.synthesize(SMTSolver.get(), BPCs, PCs, LHS, RHS, IC, Timeout);
if (EC || RHS)
EC = ES.synthesize(SMTSolver.get(), BPCs, PCs, LHS, RHSs,
Copy link
Contributor

@regehr regehr Oct 10, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

did you intend to change this line? was it too long?

Copy link
Contributor Author

@zhengyang92 zhengyang92 Oct 10, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

RHS is changed to RHSs, and it is too long so I wrapped.

IC, Timeout);
if (EC || !RHSs.empty())
return EC;
} else if (InferInsts) {
InstSynthesis IS;
Inst *RHS;
EC = IS.synthesize(SMTSolver.get(), BPCs, PCs, LHS, RHS, IC, Timeout);
RHSs.emplace_back(RHS);
if (EC || RHS)
return EC;
}
}

RHS = 0;
RHSs.clear();
return EC;
}

Expand Down Expand Up @@ -281,16 +285,17 @@ class MemCachingSolver : public Solver {

std::error_code infer(const BlockPCs &BPCs,
const std::vector<InstMapping> &PCs,
Inst *LHS, Inst *&RHS, InstContext &IC) override {
Inst *LHS, std::vector<Inst *> &RHSs,
InstContext &IC) override {
ReplacementContext Context;
std::string Repl = GetReplacementLHSString(BPCs, PCs, LHS, Context);
const auto &ent = InferCache.find(Repl);
if (ent == InferCache.end()) {
++MemMissesInfer;
std::error_code EC = UnderlyingSolver->infer(BPCs, PCs, LHS, RHS, IC);
std::error_code EC = UnderlyingSolver->infer(BPCs, PCs, LHS, RHSs, IC);
std::string RHSStr;
if (!EC && RHS) {
RHSStr = GetReplacementRHSString(RHS, Context);
if (!EC && !RHSs.empty()) {
RHSStr = GetReplacementRHSString(RHSs.front(), Context);
Copy link
Contributor

@regehr regehr Oct 10, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

seems weird to take the first element here, is this a placeholder for something different?

Copy link
Contributor Author

@zhengyang92 zhengyang92 Oct 10, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This PR does not support cache dumping yet, so only print the first RHS in the list. I'll add support for cache dumping soon.

Copy link
Contributor

@regehr regehr Oct 10, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I'd say don't do the caching part of this yet, until we're sure we want it

Copy link
Contributor Author

@zhengyang92 zhengyang92 Oct 10, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Agreed.

Copy link
Contributor

@manasij7479 manasij7479 Oct 10, 2018

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Sounds good, should be possible to prototype without caching.

}
InferCache.emplace(Repl, std::make_pair(EC, RHSStr));
return EC;
Expand All @@ -299,12 +304,12 @@ class MemCachingSolver : public Solver {
std::string ES;
StringRef S = ent->second.second;
if (S == "") {
RHS = 0;
RHSs.clear();
} else {
ParsedReplacement R = ParseReplacementRHS(IC, "<cache>", S, Context, ES);
if (ES != "")
return std::make_error_code(std::errc::protocol_error);
RHS = R.Mapping.RHS;
RHSs.emplace_back(R.Mapping.RHS);
}
return ent->second.first;
}
Expand Down Expand Up @@ -351,7 +356,8 @@ class ExternalCachingSolver : public Solver {

std::error_code infer(const BlockPCs &BPCs,
const std::vector<InstMapping> &PCs,
Inst *LHS, Inst *&RHS, InstContext &IC) override {
Inst *LHS, std::vector<Inst *> &RHSs,
InstContext &IC) override {
ReplacementContext Context;
std::string LHSStr = GetReplacementLHSString(BPCs, PCs, LHS, Context);
if (LHSStr.length() > MaxLHSSize)
Expand All @@ -360,26 +366,26 @@ class ExternalCachingSolver : public Solver {
if (KV->hGet(LHSStr, "result", S)) {
++ExternalHits;
if (S == "") {
RHS = 0;
RHSs.clear();
} else {
std::string ES;
ParsedReplacement R = ParseReplacementRHS(IC, "<cache>", S, Context, ES);
if (ES != "")
return std::make_error_code(std::errc::protocol_error);
RHS = R.Mapping.RHS;
RHSs.emplace_back(R.Mapping.RHS);
}
return std::error_code();
} else {
++ExternalMisses;
if (NoInfer) {
RHS = 0;
RHSs.clear();
KV->hSet(LHSStr, "result", "");
return std::error_code();
}
std::error_code EC = UnderlyingSolver->infer(BPCs, PCs, LHS, RHS, IC);
std::error_code EC = UnderlyingSolver->infer(BPCs, PCs, LHS, RHSs, IC);
std::string RHSStr;
if (!EC && RHS) {
RHSStr = GetReplacementRHSString(RHS, Context);
if (!EC && !RHSs.empty()) {
RHSStr = GetReplacementRHSString(RHSs.front(), Context);
}
KV->hSet(LHSStr, "result", RHSStr);
return EC;
Expand Down
8 changes: 5 additions & 3 deletions lib/Infer/ExhaustiveSynthesis.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,7 @@
static const unsigned MaxTries = 30;
static const unsigned MaxInputSpecializationTries = 2;
static const unsigned MaxLHSCands = 15;
static const unsigned MaxRHS = 1;

using namespace souper;
using namespace llvm;
Expand Down Expand Up @@ -361,7 +362,7 @@ std::error_code
ExhaustiveSynthesis::synthesize(SMTLIBSolver *SMTSolver,
const BlockPCs &BPCs,
const std::vector<InstMapping> &PCs,
Inst *LHS, Inst *&RHS,
Inst *LHS, std::vector<Inst *> &RHSs,
InstContext &IC, unsigned Timeout) {
std::vector<Inst *> Inputs;
findCands(LHS, Inputs, /*WidthMustMatch=*/false, /*FilterVars=*/false, MaxLHSCands);
Expand Down Expand Up @@ -581,8 +582,9 @@ ExhaustiveSynthesis::synthesize(SMTLIBSolver *SMTSolver,
llvm::errs() << "second query is UNSAT-- works for all values of this constant\n";
llvm::errs() << Tries << " tries were made for synthesizing constants\n";
}
RHS = I2;
return EC;
RHSs.emplace_back(I2);
if (RHSs.size() >= MaxRHS)
return EC;
}
}
if (DebugLevel > 2)
Expand Down
4 changes: 3 additions & 1 deletion lib/Pass/Pass.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -399,16 +399,18 @@ struct SouperPass : public ModulePass {
Changed = true;
continue;
}
std::vector<Inst *> RHSs;
if (std::error_code EC =
S->infer(Cand.BPCs, Cand.PCs, Cand.Mapping.LHS,
Cand.Mapping.RHS, IC)) {
RHSs, IC)) {
if (EC == std::errc::timed_out ||
EC == std::errc::value_too_large) {
continue;
} else {
report_fatal_error("Unable to query solver: " + EC.message() + "\n");
}
}
Cand.Mapping.RHS = RHSs.empty() ? 0 : RHSs.front();
if (!Cand.Mapping.RHS)
continue;

Expand Down
16 changes: 8 additions & 8 deletions lib/Tool/CandidateMapUtils.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -83,16 +83,16 @@ bool SolveCandidateMap(llvm::raw_ostream &OS, CandidateMap &M,
Cand.PCs, Cand.Mapping.LHS, Context), HField, 1);
}

Inst *RHS;
std::vector<Inst *> RHSs;
if (std::error_code EC =
S->infer(Cand.BPCs, Cand.PCs, Cand.Mapping.LHS, RHS, IC)) {
S->infer(Cand.BPCs, Cand.PCs, Cand.Mapping.LHS, RHSs, IC)) {
llvm::errs() << "Unable to query solver: " << EC.message() << '\n';
return false;
}
if (RHS) {
if (!RHSs.empty()) {
OS << '\n';
OS << "; Static profile " << Profile[I] << '\n';
Cand.Mapping.RHS = RHS;
Cand.Mapping.RHS = RHSs.front();
Cand.printFunction(OS);
Cand.print(OS);
}
Expand Down Expand Up @@ -121,14 +121,14 @@ bool CheckCandidateMap(llvm::Module &Mod, CandidateMap &M, Solver *S,

bool OK = true;
for (auto &Cand : M) {
Inst *RHS;
std::vector<Inst *> RHSs;
if (std::error_code EC =
S->infer(Cand.BPCs, Cand.PCs, Cand.Mapping.LHS, RHS, IC)) {
S->infer(Cand.BPCs, Cand.PCs, Cand.Mapping.LHS, RHSs, IC)) {
llvm::errs() << "Unable to query solver: " << EC.message() << '\n';
return false;
}
if (RHS) {
Cand.Mapping.RHS = RHS;
if (!RHSs.empty()) {
Cand.Mapping.RHS = RHSs.front();
if (Cand.Mapping.RHS->K != Inst::Const) {
llvm::errs() << "found replacement:\n";
Cand.printFunction(llvm::errs());
Expand Down
4 changes: 3 additions & 1 deletion tools/souper-check.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -83,12 +83,14 @@ int SolveInst(const MemoryBufferRef &MB, Solver *S) {
OldCost = cost(Rep.Mapping.RHS);
Rep.Mapping.RHS = 0;
}
std::vector<Inst *> RHSs;
if (std::error_code EC = S->infer(Rep.BPCs, Rep.PCs, Rep.Mapping.LHS,
Rep.Mapping.RHS, IC)) {
RHSs, IC)) {
llvm::errs() << EC.message() << '\n';
Ret = 1;
++Error;
}
Rep.Mapping.RHS = RHSs.empty() ? 0 : RHSs.front();
if (Rep.Mapping.RHS) {
++Success;
if (ReInferRHS) {
Expand Down