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

first cut at providing synthesis with 'big components' from the LHS #326

Closed
regehr wants to merge 1 commit into from
Closed

first cut at providing synthesis with 'big components' from the LHS #326

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
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
3 changes: 3 additions & 0 deletions include/souper/Infer/InstSynthesis.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -132,6 +132,9 @@ class InstSynthesis {
const BlockPCs &BPCs,
const std::vector<InstMapping> &PCs,
Inst *TargetLHS, Inst *&RHS,
const std::vector<Inst *> &Copies,
const std::vector<InstMapping> &PCsCopy,
const BlockPCs &BPCsCopy,
InstContext &IC, unsigned Timeout);

private:
Expand Down
18 changes: 17 additions & 1 deletion lib/Extractor/Solver.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -206,8 +206,24 @@ class BaseSolver : public Solver {
}

if (InferInsts && SMTSolver->supportsModels()) {
std::vector<Inst *> LHSComps;
findCands(LHS, LHSComps, IC, MaxNops);

std::vector<Inst *> Copies;
std::vector<InstMapping> PCsCopy;
BlockPCs BPCsCopy;
for (auto I : LHSComps) {
// separate sub-expressions by copying vars
std::map<Inst *, Inst *> InstCache;
std::map<Block *, Block *> BlockCache;
Copies.push_back(getInstCopy(I, IC, InstCache, BlockCache));
separateBlockPCs(BPCs, BPCsCopy, InstCache, BlockCache, IC);
separatePCs(PCs, PCsCopy, InstCache, BlockCache, IC);
Copy link
Contributor

@rsas rsas May 8, 2018

Choose a reason for hiding this comment

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

The synthesis engine doesn't take PCs/BPCs into account that are attached to the component library (RHS). Now, if a candidate from LHS has a PC/PBC, I should consider this during synthesis. This makes things a bit more complex. Maybe we can start without PC/BPC support first.

Copy link
Contributor Author

@regehr regehr May 9, 2018

Choose a reason for hiding this comment

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

Yes, just ignore for now.

I think the correct thing to do with pc/blockpc is to ignore them for almost all purposes (cost functions etc.) but to allow them to put constraints on the LHS, which should make synthesis work more often.

}

InstSynthesis IS;
EC = IS.synthesize(SMTSolver.get(), BPCs, PCs, LHS, RHS, IC, Timeout);
EC = IS.synthesize(SMTSolver.get(), BPCs, PCs, LHS, RHS,
Copies, PCsCopy, BPCsCopy, IC, Timeout);
Copy link
Contributor

@rsas rsas May 8, 2018

Choose a reason for hiding this comment

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

There is no need to make copies, the only thing I need are the LHSComps.

Copy link
Contributor Author

@regehr regehr May 9, 2018

Choose a reason for hiding this comment

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

Wait, really? But we need copies for nop synthesis, what's different here?

Copy link
Contributor

@rsas rsas May 11, 2018

Choose a reason for hiding this comment

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

The necessary replacements are performed in the synthesis engine in a special way that is different from the nop synthesis.

if (EC || RHS)
return EC;
}
Expand Down
3 changes: 3 additions & 0 deletions lib/Infer/InstSynthesis.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -59,6 +59,9 @@ std::error_code InstSynthesis::synthesize(SMTLIBSolver *SMTSolver,
const BlockPCs &BPCs,
const std::vector<InstMapping> &PCs,
Inst *TargetLHS, Inst *&RHS,
const std::vector<Inst *> &Copies,
const std::vector<InstMapping> &PCsCopy,
const BlockPCs &BPCsCopy,
InstContext &IC, unsigned Timeout) {
std::error_code EC;

Expand Down