Skip to content

Commit

Permalink
Add lazy calculation of constraint dsu
Browse files Browse the repository at this point in the history
  • Loading branch information
@dim8art @misonijnik
dim8art authored and misonijnik committed Nov 22, 2023
1 parent a731677 commit 096ccf3
Show file tree
Hide file tree
Showing 5 changed files with 102 additions and 43 deletions.
5 changes: 4 additions & 1 deletion include/klee/Expr/Constraints.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -43,6 +43,7 @@ class ConstraintSet {
const std::vector<ref<const IndependentConstraintSet>> &ics);
explicit ConstraintSet(constraints_ty cs);
explicit ConstraintSet();
void fork();

void addConstraint(ref<Expr> e, const Assignment &delta);
void addSymcrete(ref<Symcrete> s, const Assignment &concretization);
Expand Down Expand Up @@ -90,7 +91,7 @@ class ConstraintSet {
constraints_ty _constraints;
symcretes_ty _symcretes;
Assignment _concretization;
IndependentConstraintSetUnion _independentElements;
std::shared_ptr<IndependentConstraintSetUnion> _independentElements;
};

class PathConstraints {
Expand All @@ -100,6 +101,8 @@ class PathConstraints {

void advancePath(KInstruction *ki);
void advancePath(const Path &path);
void fork();

ExprHashSet addConstraint(ref<Expr> e, const Assignment &delta,
Path::PathIndex currIndex);
ExprHashSet addConstraint(ref<Expr> e, const Assignment &delta);
Expand Down
19 changes: 11 additions & 8 deletions include/klee/Expr/IndependentConstraintSetUnion.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -12,18 +12,22 @@ class IndependentConstraintSetUnion
ExprOrSymcreteHash, ExprOrSymcreteCmp> {
public:
Assignment concretization;
std::vector<ref<ExprOrSymcrete>> constraintQueue;
Assignment updateQueue;
Assignment removeQueue;

public:
ExprHashMap<ref<Expr>> concretizedExprs;

public:
void updateConcretization(const Assignment &c);
void updateConcretization(const Assignment &delta);
void removeConcretization(const Assignment &remove);
void calculateUpdateConcretizationQueue();
void calculateRemoveConcretizationQueue();
void reEvaluateConcretization(const Assignment &newConcretization);

IndependentConstraintSetUnion getConcretizedVersion() const;
IndependentConstraintSetUnion
getConcretizedVersion(const Assignment &c) const;
IndependentConstraintSetUnion getConcretizedVersion();
IndependentConstraintSetUnion getConcretizedVersion(const Assignment &c);

IndependentConstraintSetUnion();
IndependentConstraintSetUnion(const constraints_ty &is,
Expand All @@ -35,14 +39,13 @@ class IndependentConstraintSetUnion
addIndependentConstraintSetUnion(const IndependentConstraintSetUnion &icsu);

void getAllDependentConstraintSets(
ref<Expr> e,
std::vector<ref<const IndependentConstraintSet>> &result) const;
ref<Expr> e, std::vector<ref<const IndependentConstraintSet>> &result);
void getAllIndependentConstraintSets(
ref<Expr> e,
std::vector<ref<const IndependentConstraintSet>> &result) const;
ref<Expr> e, std::vector<ref<const IndependentConstraintSet>> &result);

void addExpr(ref<Expr> e);
void addSymcrete(ref<Symcrete> s);
void calculateQueue();
};
} // namespace klee

Expand Down
1 change: 1 addition & 0 deletions lib/Core/ExecutionState.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -180,6 +180,7 @@ ExecutionState::ExecutionState(const ExecutionState &state)
gepExprBases(state.gepExprBases), prevTargets_(state.prevTargets_),
targets_(state.targets_), prevHistory_(state.prevHistory_),
history_(state.history_), isTargeted_(state.isTargeted_) {
constraints.fork();
queryMetaData.id = state.id;
}

Expand Down
53 changes: 33 additions & 20 deletions lib/Expr/Constraints.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -183,52 +183,62 @@ class ExprReplaceVisitor3 : public ExprVisitor {
ConstraintSet::ConstraintSet(constraints_ty cs, symcretes_ty symcretes,
Assignment concretization)
: _constraints(cs), _symcretes(symcretes), _concretization(concretization),
_independentElements(_constraints, _symcretes, _concretization) {}
_independentElements(new IndependentConstraintSetUnion(
_constraints, _symcretes, _concretization)) {}

ConstraintSet::ConstraintSet(ref<const IndependentConstraintSet> ics)
: _constraints(ics->getConstraints()), _symcretes(ics->getSymcretes()),
_concretization(ics->concretization), _independentElements(ics) {}
_concretization(ics->concretization),
_independentElements(new IndependentConstraintSetUnion(ics)) {}

ConstraintSet::ConstraintSet(
const std::vector<ref<const IndependentConstraintSet>> &factors) {
const std::vector<ref<const IndependentConstraintSet>> &factors)
: _independentElements(new IndependentConstraintSetUnion(
_constraints, _symcretes, _concretization)) {
for (auto ics : factors) {
constraints_ty constraints = ics->getConstraints();
SymcreteOrderedSet symcretes = ics->getSymcretes();
IndependentConstraintSetUnion icsu(ics);
_constraints.insert(constraints.begin(), constraints.end());
_symcretes.insert(symcretes.begin(), symcretes.end());
_concretization.addIndependentAssignment(ics->concretization);
_independentElements.addIndependentConstraintSetUnion(icsu);
_independentElements->addIndependentConstraintSetUnion(icsu);
}
}

ConstraintSet::ConstraintSet(constraints_ty cs) : ConstraintSet(cs, {}, {}) {}

ConstraintSet::ConstraintSet() {}
ConstraintSet::ConstraintSet()
: _independentElements(new IndependentConstraintSetUnion()) {}

void ConstraintSet::fork() {
_independentElements = std::make_shared<IndependentConstraintSetUnion>(
IndependentConstraintSetUnion(*_independentElements));
}

void ConstraintSet::addConstraint(ref<Expr> e, const Assignment &delta) {
_constraints.insert(e);
// Update bindings
for (auto &i : delta.bindings) {
_concretization.bindings.replace({i.first, i.second});
}
_independentElements.updateConcretization(delta);
_independentElements.addExpr(e);
_independentElements->updateConcretization(delta);
_independentElements->addExpr(e);
}

IDType Symcrete::idCounter = 0;

void ConstraintSet::addSymcrete(ref<Symcrete> s,
const Assignment &concretization) {
_symcretes.insert(s);
_independentElements.addSymcrete(s);
_independentElements->addSymcrete(s);
Assignment dependentConcretization;
for (auto i : s->dependentArrays()) {
_concretization.bindings.replace({i, concretization.bindings.at(i)});
dependentConcretization.bindings.replace(
{i, concretization.bindings.at(i)});
}
_independentElements.updateConcretization(dependentConcretization);
_independentElements->updateConcretization(dependentConcretization);
}

bool ConstraintSet::isSymcretized(ref<Expr> expr) const {
Expand All @@ -246,14 +256,15 @@ void ConstraintSet::rewriteConcretization(const Assignment &a) {
_concretization.bindings.replace({i.first, i.second});
}
}
_independentElements.updateConcretization(a);
_independentElements->updateConcretization(a);
}

ConstraintSet ConstraintSet::getConcretizedVersion() const {
ConstraintSet cs;
cs._independentElements = _independentElements.getConcretizedVersion();
cs._independentElements = std::make_shared<IndependentConstraintSetUnion>(
_independentElements->getConcretizedVersion());

for (auto &e : cs._independentElements.is()) {
for (auto &e : cs._independentElements->is()) {
if (isa<ExprOrSymcrete::left>(e)) {
cs._constraints.insert(cast<ExprOrSymcrete::left>(e)->value());
}
Expand All @@ -264,9 +275,9 @@ ConstraintSet ConstraintSet::getConcretizedVersion() const {
ConstraintSet ConstraintSet::getConcretizedVersion(
const Assignment &newConcretization) const {
ConstraintSet cs;
cs._independentElements =
_independentElements.getConcretizedVersion(newConcretization);
for (auto &e : cs._independentElements.is()) {
cs._independentElements = std::make_shared<IndependentConstraintSetUnion>(
_independentElements->getConcretizedVersion(newConcretization));
for (auto &e : cs._independentElements->is()) {
cs._constraints.insert(cast<ExprOrSymcrete::left>(e)->value());
}
return cs;
Expand All @@ -292,8 +303,8 @@ void ConstraintSet::dump() const { this->print(llvm::errs()); }

void ConstraintSet::changeCS(constraints_ty &cs) {
_constraints = cs;
_independentElements =
IndependentConstraintSetUnion(_constraints, _symcretes, _concretization);
_independentElements = std::make_shared<IndependentConstraintSetUnion>(
IndependentConstraintSetUnion(_constraints, _symcretes, _concretization));
}

const constraints_ty &ConstraintSet::cs() const { return _constraints; }
Expand All @@ -302,7 +313,7 @@ const symcretes_ty &ConstraintSet::symcretes() const { return _symcretes; }

const IndependentConstraintSetUnion &
ConstraintSet::independentElements() const {
return _independentElements;
return *_independentElements;
}

const Path &PathConstraints::path() const { return _path; }
Expand Down Expand Up @@ -330,6 +341,8 @@ PathConstraints::orderedCS() const {

void PathConstraints::advancePath(KInstruction *ki) { _path.advance(ki); }

void PathConstraints::fork() { constraints.fork(); }

ExprHashSet PathConstraints::addConstraint(ref<Expr> e, const Assignment &delta,
Path::PathIndex currIndex) {
auto expr = Simplificator::simplifyExpr(constraints, e);
Expand Down Expand Up @@ -560,13 +573,13 @@ Simplificator::composeExprDependencies(const ExprHashMap<ExprHashSet> &upper,
void ConstraintSet::getAllIndependentConstraintsSets(
ref<Expr> queryExpr,
std::vector<ref<const IndependentConstraintSet>> &result) const {
_independentElements.getAllIndependentConstraintSets(queryExpr, result);
_independentElements->getAllIndependentConstraintSets(queryExpr, result);
}

void ConstraintSet::getAllDependentConstraintsSets(
ref<Expr> queryExpr,
std::vector<ref<const IndependentConstraintSet>> &result) const {
_independentElements.getAllDependentConstraintSets(queryExpr, result);
_independentElements->getAllDependentConstraintSets(queryExpr, result);
}

std::vector<const Array *> ConstraintSet::gatherArrays() const {
Expand Down
67 changes: 53 additions & 14 deletions lib/Expr/IndependentConstraintSetUnion.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -49,30 +49,48 @@ void IndependentConstraintSetUnion::addIndependentConstraintSetUnion(
const IndependentConstraintSetUnion &icsu) {
add(icsu);
concretization.addIndependentAssignment(icsu.concretization);
updateQueue.addIndependentAssignment(icsu.updateQueue);
removeQueue.addIndependentAssignment(icsu.removeQueue);
constraintQueue.insert(constraintQueue.begin(), icsu.constraintQueue.begin(),
icsu.constraintQueue.end());
}

void IndependentConstraintSetUnion::updateConcretization(
const Assignment &delta) {
for (auto &it : delta.bindings) {
updateQueue.bindings.replace({it.first, it.second});
removeQueue.bindings.remove(it.first);
}
}

void IndependentConstraintSetUnion::removeConcretization(
const Assignment &remove) {
for (auto &it : remove.bindings) {
removeQueue.bindings.replace({it.first, it.second});
updateQueue.bindings.remove(it.first);
}
}

void IndependentConstraintSetUnion::calculateUpdateConcretizationQueue() {
for (auto &e : roots) {
ref<const IndependentConstraintSet> ics = disjointSets.at(e);
Assignment part = delta.part(ics->getSymcretes());
Assignment part = updateQueue.part(ics->getSymcretes());
ics = ics->updateConcretization(part, concretizedExprs);
disjointSets.insert_or_assign(e, ics);
}
for (auto &it : delta.bindings) {
for (auto &it : updateQueue.bindings) {
concretization.bindings.replace({it.first, it.second});
}
}

void IndependentConstraintSetUnion::removeConcretization(
const Assignment &remove) {
void IndependentConstraintSetUnion::calculateRemoveConcretizationQueue() {
for (auto &e : roots) {
ref<const IndependentConstraintSet> ics = disjointSets.at(e);
Assignment part = remove.part(ics->getSymcretes());
Assignment part = removeQueue.part(ics->getSymcretes());
ics = ics->removeConcretization(part, concretizedExprs);
disjointSets.insert_or_assign(e, ics);
}
for (auto &it : remove.bindings) {
for (auto &it : removeQueue.bindings) {
concretization.bindings.remove(it.first);
}
}
Expand All @@ -93,8 +111,8 @@ void IndependentConstraintSetUnion::reEvaluateConcretization(
}

void IndependentConstraintSetUnion::getAllIndependentConstraintSets(
ref<Expr> e,
std::vector<ref<const IndependentConstraintSet>> &result) const {
ref<Expr> e, std::vector<ref<const IndependentConstraintSet>> &result) {
calculateQueue();
ref<const IndependentConstraintSet> compare =
new IndependentConstraintSet(new ExprOrSymcrete::left(e));
for (auto &r : roots) {
Expand All @@ -106,8 +124,8 @@ void IndependentConstraintSetUnion::getAllIndependentConstraintSets(
}

void IndependentConstraintSetUnion::getAllDependentConstraintSets(
ref<Expr> e,
std::vector<ref<const IndependentConstraintSet>> &result) const {
ref<Expr> e, std::vector<ref<const IndependentConstraintSet>> &result) {
calculateQueue();
ref<const IndependentConstraintSet> compare =
new IndependentConstraintSet(new ExprOrSymcrete::left(e));
for (auto &r : roots) {
Expand All @@ -119,15 +137,16 @@ void IndependentConstraintSetUnion::getAllDependentConstraintSets(
}

void IndependentConstraintSetUnion::addExpr(ref<Expr> e) {
addValue(new ExprOrSymcrete::left(e));
constraintQueue.push_back(new ExprOrSymcrete::left(e));
}

void IndependentConstraintSetUnion::addSymcrete(ref<Symcrete> s) {
addValue(new ExprOrSymcrete::right(s));
constraintQueue.push_back(new ExprOrSymcrete::right(s));
}

IndependentConstraintSetUnion
IndependentConstraintSetUnion::getConcretizedVersion() const {
IndependentConstraintSetUnion::getConcretizedVersion() {
calculateQueue();
IndependentConstraintSetUnion icsu;
for (auto &i : roots) {
ref<const IndependentConstraintSet> root = disjointSets.at(i);
Expand All @@ -141,14 +160,34 @@ IndependentConstraintSetUnion::getConcretizedVersion() const {
icsu.concretization.addIndependentAssignment(root->concretization);
}
icsu.concretizedExprs = concretizedExprs;
icsu.calculateQueue();
return icsu;
}

IndependentConstraintSetUnion
IndependentConstraintSetUnion::getConcretizedVersion(
const Assignment &newConcretization) const {
const Assignment &newConcretization) {
calculateQueue();
IndependentConstraintSetUnion icsu = *this;
icsu.reEvaluateConcretization(newConcretization);
icsu.calculateQueue();
return icsu.getConcretizedVersion();
}

void IndependentConstraintSetUnion::calculateQueue() {
calculateUpdateConcretizationQueue();
calculateRemoveConcretizationQueue();
while (!constraintQueue.empty()) {
addValue(constraintQueue[constraintQueue.size() - 1]);
constraintQueue.pop_back();
}
calculateUpdateConcretizationQueue();
calculateRemoveConcretizationQueue();
// Calculations are done twice for constraints already in dsu and for newly
// added constraints. Because IndependentSet update and remove concretization
// functions work only with difference between new and old concretization, no
// extra work is done
removeQueue.bindings = Assignment::bindings_ty();
updateQueue.bindings = Assignment::bindings_ty();
}
} // namespace klee

0 comments on commit 096ccf3

Please sign in to comment.