From be33e6f52abdbbe017fe790355004af6d2efcd44 Mon Sep 17 00:00:00 2001 From: dim8art Date: Sun, 20 Aug 2023 16:16:19 +0300 Subject: [PATCH 1/5] Add DisjointSetUnion --- include/klee/ADT/DisjointSetUnion.h | 143 +++++++++++++++ .../klee/Expr/IndependentConstraintSetUnion.h | 46 +++++ lib/Expr/IndependentConstraintSetUnion.cpp | 166 ++++++++++++++++++ 3 files changed, 355 insertions(+) create mode 100644 include/klee/ADT/DisjointSetUnion.h create mode 100644 include/klee/Expr/IndependentConstraintSetUnion.h create mode 100644 lib/Expr/IndependentConstraintSetUnion.cpp diff --git a/include/klee/ADT/DisjointSetUnion.h b/include/klee/ADT/DisjointSetUnion.h new file mode 100644 index 0000000000..77a41353c2 --- /dev/null +++ b/include/klee/ADT/DisjointSetUnion.h @@ -0,0 +1,143 @@ +#ifndef KLEE_DISJOINEDSETUNION_H +#define KLEE_DISJOINEDSETUNION_H +#include "klee/ADT/PersistentMap.h" +#include "klee/ADT/PersistentSet.h" +#include "klee/ADT/Ref.h" +#include +#include +#include +#include + +namespace klee { + +template > +class DisjointSetUnion { +protected: + PersistentMap parent; + PersistentSet roots; + PersistentMap rank; + + PersistentSet internalStorage; + PersistentMap, CMP> disjointSets; + + ValueType find(const ValueType &v) { // findparent + assert(parent.find(v) != parent.end()); + if (v == parent.at(v)) + return v; + parent.replace({v, find(parent.at(v))}); + return parent.at(v); + } + + ValueType constFind(const ValueType &v) const { + assert(parent.find(v) != parent.end()); + ValueType v1 = parent.at(v); + if (v == v1) + return v; + return constFind(v1); + } + + void merge(ValueType a, ValueType b) { + a = find(a); + b = find(b); + if (a == b) { + return; + } + + if (rank.at(a) < rank.at(b)) { + std::swap(a, b); + } + parent.replace({b, a}); + if (rank.at(a) == rank.at(b)) { + rank.replace({a, rank.at(a) + 1}); + } + + roots.remove(b); + disjointSets.replace( + {a, SetType::merge(disjointSets.at(a), disjointSets.at(b))}); + disjointSets.replace({b, nullptr}); + } + + bool areJoined(const ValueType &i, const ValueType &j) const { + return constFind(i) == constFind(j); + } + +public: + using internalStorage_ty = PersistentSet; + using disjointSets_ty = ImmutableMap, CMP>; + using iterator = typename internalStorage_ty::iterator; + + iterator begin() const { return internalStorage.begin(); } + iterator end() const { return internalStorage.end(); } + + size_t numberOfValues() const noexcept { return internalStorage.size(); } + + size_t numberOfGroups() const noexcept { return disjointSets.size(); } + + bool empty() const noexcept { return numberOfValues() == 0; } + + ref findGroup(const ValueType &i) const { + return disjointSets.find(constFind(i))->second; + } + + ref findGroup(iterator it) const { + return disjointSets.find(constFind(*it))->second; + } + + void addValue(const ValueType value) { + if (internalStorage.find(value) != internalStorage.end()) { + return; + } + parent.insert({value, value}); + roots.insert(value); + rank.insert({value, 0}); + disjointSets.insert({value, new SetType(value)}); + + internalStorage.insert(value); + internalStorage_ty oldRoots = roots; + for (ValueType v : oldRoots) { + if (!areJoined(v, value) && + SetType::intersects(disjointSets.at(find(v)), + disjointSets.at(find(value)))) { + merge(v, value); + } + } + } + void getAllIndependentSets(std::vector> &result) const { + for (ValueType v : roots) + result.push_back(findGroup(v)); + } + + void add(const DisjointSetUnion &b) { + for (auto it : b.parent) { + parent.insert(it); + } + for (auto it : b.roots) { + roots.insert(it); + } + for (auto it : b.rank) { + rank.insert(it); + } + for (auto it : b.internalStorage) { + internalStorage.insert(it); + } + for (auto it : b.disjointSets) { + disjointSets.insert(it); + } + } + + DisjointSetUnion() {} + + DisjointSetUnion(const internalStorage_ty &is) { + for (ValueType v : is) { + addValue(v); + } + } + +public: + internalStorage_ty is() const { return internalStorage; } + + disjointSets_ty ds() const { return disjointSets; } +}; +} // namespace klee +#endif diff --git a/include/klee/Expr/IndependentConstraintSetUnion.h b/include/klee/Expr/IndependentConstraintSetUnion.h new file mode 100644 index 0000000000..3591cd5eff --- /dev/null +++ b/include/klee/Expr/IndependentConstraintSetUnion.h @@ -0,0 +1,46 @@ +#ifndef KLEE_INDEPENDENTCONSTRAINTSETUNION_H +#define KLEE_INDEPENDENTCONSTRAINTSETUNION_H + +#include "klee/Expr/Assignment.h" +#include "klee/Expr/IndependentSet.h" + +namespace klee { +class IndependentConstraintSetUnion + : public DisjointSetUnion, IndependentConstraintSet> { +public: + Assignment concretization; + +public: + ExprHashMap> concretizedExprs; + +public: + void updateConcretization(const Assignment &c); + void removeConcretization(const Assignment &remove); + void reEvaluateConcretization(const Assignment &newConcretization); + + IndependentConstraintSetUnion getConcretizedVersion() const; + IndependentConstraintSetUnion + getConcretizedVersion(const Assignment &c) const; + + IndependentConstraintSetUnion(); + IndependentConstraintSetUnion(const constraints_ty &is, + const SymcreteOrderedSet &os, + const Assignment &c); + IndependentConstraintSetUnion(ref ics); + + void + addIndependentConstraintSetUnion(const IndependentConstraintSetUnion &icsu); + + void getAllDependentConstraintSets( + ref e, + std::vector> &result) const; + void getAllIndependentConstraintSets( + ref e, + std::vector> &result) const; + + void addExpr(ref e); + void addSymcrete(ref s); +}; +} // namespace klee + +#endif diff --git a/lib/Expr/IndependentConstraintSetUnion.cpp b/lib/Expr/IndependentConstraintSetUnion.cpp new file mode 100644 index 0000000000..692e679234 --- /dev/null +++ b/lib/Expr/IndependentConstraintSetUnion.cpp @@ -0,0 +1,166 @@ +#include "klee/Expr/IndependentConstraintSetUnion.h" + +namespace klee { + +IndependentConstraintSetUnion::IndependentConstraintSetUnion() {} + +IndependentConstraintSetUnion::IndependentConstraintSetUnion( + const constraints_ty &is, const SymcreteOrderedSet &os, + const Assignment &c) { + for (ref e : is) { + addValue(e); + } + for (ref s : os) { + addSymcrete(s); + } + updateConcretization(c); +} + +IndependentConstraintSetUnion::IndependentConstraintSetUnion( + ref ics) { + for (ref e : ics->exprs) { + rank.replace({e, 0}); + internalStorage.insert(e); + disjointSets.replace({e, nullptr}); + } + + for (ref s : ics->symcretes) { + ref e = s->symcretized; + rank.replace({e, 0}); + internalStorage.insert(e); + disjointSets.replace({e, nullptr}); + } + + if (internalStorage.size() == 0) { + return; + } + + ref first = *(internalStorage.begin()); + for (ref e : internalStorage) { + parent.replace({e, first}); + } + rank.replace({first, 1}); + roots.insert(first); + disjointSets.replace({first, ics}); + concretization = ics->concretization; +} + +void IndependentConstraintSetUnion::addIndependentConstraintSetUnion( + const IndependentConstraintSetUnion &icsu) { + add(icsu); + concretization.addIndependentAssignment(icsu.concretization); +} + +void IndependentConstraintSetUnion::updateConcretization( + const Assignment &delta) { + for (ref e : roots) { + ref ics = disjointSets.at(e); + Assignment part = delta.part(ics->getSymcretes()); + ics = ics->updateConcretization(part, concretizedExprs); + disjointSets.replace({e, ics}); + } + for (auto it : delta.bindings) { + concretization.bindings.replace({it.first, it.second}); + } +} + +void IndependentConstraintSetUnion::removeConcretization( + const Assignment &remove) { + for (ref e : roots) { + ref ics = disjointSets.at(e); + Assignment part = remove.part(ics->getSymcretes()); + ics = ics->removeConcretization(part, concretizedExprs); + disjointSets.replace({e, ics}); + } + for (auto it : remove.bindings) { + concretization.bindings.remove(it.first); + } +} + +void IndependentConstraintSetUnion::reEvaluateConcretization( + const Assignment &newConcretization) { + Assignment delta; + Assignment removed; + for (const auto it : concretization) { + if (newConcretization.bindings.count(it.first) == 0) { + removed.bindings.insert(it); + } else if (newConcretization.bindings.at(it.first) != it.second) { + delta.bindings.insert(*(newConcretization.bindings.find(it.first))); + } + } + updateConcretization(delta); + removeConcretization(removed); +} + +void IndependentConstraintSetUnion::getAllIndependentConstraintSets( + ref e, + std::vector> &result) const { + ref compare = new IndependentConstraintSet(e); + for (ref r : roots) { + ref ics = disjointSets.at(r); + if (!IndependentConstraintSet::intersects(ics, compare)) { + result.push_back(ics); + } + } +} + +void IndependentConstraintSetUnion::getAllDependentConstraintSets( + ref e, + std::vector> &result) const { + ref compare = new IndependentConstraintSet(e); + for (ref r : roots) { + ref ics = disjointSets.at(r); + if (IndependentConstraintSet::intersects(ics, compare)) { + result.push_back(ics); + } + } +} + +void IndependentConstraintSetUnion::addExpr(ref e) { + addValue(e); + disjointSets.replace({find(e), disjointSets.at(find(e))->addExpr(e)}); +} + +void IndependentConstraintSetUnion::addSymcrete(ref s) { + ref value = s->symcretized; + if (internalStorage.find(value) != internalStorage.end()) { + return; + } + parent.insert({value, value}); + roots.insert(value); + rank.insert({value, 0}); + disjointSets.insert({value, new IndependentConstraintSet(s)}); + + internalStorage.insert(value); + internalStorage_ty oldRoots = roots; + for (ref v : oldRoots) { + if (!areJoined(v, value) && + IndependentConstraintSet::intersects(disjointSets.at(find(v)), + disjointSets.at(find(value)))) { + merge(v, value); + } + } + disjointSets.replace( + {find(value), disjointSets.at(find(value))->addExpr(value)}); +} + +IndependentConstraintSetUnion +IndependentConstraintSetUnion::getConcretizedVersion() const { + IndependentConstraintSetUnion icsu; + for (ref i : roots) { + ref root = disjointSets.at(i); + icsu.add(root->concretizedSets); + icsu.concretization.addIndependentAssignment(root->concretization); + } + icsu.concretizedExprs = concretizedExprs; + return icsu; +} + +IndependentConstraintSetUnion +IndependentConstraintSetUnion::getConcretizedVersion( + const Assignment &newConcretization) const { + IndependentConstraintSetUnion icsu = *this; + icsu.reEvaluateConcretization(newConcretization); + return icsu.getConcretizedVersion(); +} +} // namespace klee From c35c9f1d903a73331e6ce97ba145f3b8c2493890 Mon Sep 17 00:00:00 2001 From: dim8art Date: Sun, 20 Aug 2023 16:17:13 +0300 Subject: [PATCH 2/5] Rework IndependentSolver using persistent DSU --- include/klee/Expr/Constraints.h | 17 +- include/klee/Expr/IndependentSet.h | 111 ++++++--- lib/Expr/CMakeLists.txt | 1 + lib/Expr/Constraints.cpp | 74 +++++- lib/Expr/IndependentSet.cpp | 378 ++++++++++++++--------------- lib/Solver/IndependentSolver.cpp | 231 +++++++++--------- 6 files changed, 461 insertions(+), 351 deletions(-) diff --git a/include/klee/Expr/Constraints.h b/include/klee/Expr/Constraints.h index a14b9e191e..c65cee483f 100644 --- a/include/klee/Expr/Constraints.h +++ b/include/klee/Expr/Constraints.h @@ -16,6 +16,8 @@ #include "klee/Expr/Expr.h" #include "klee/Expr/ExprHashMap.h" #include "klee/Expr/ExprUtil.h" +#include "klee/Expr/IndependentConstraintSetUnion.h" +#include "klee/Expr/IndependentSet.h" #include "klee/Expr/Path.h" #include "klee/Expr/Symcrete.h" @@ -35,6 +37,8 @@ class ConstraintSet { public: ConstraintSet(constraints_ty cs, symcretes_ty symcretes, Assignment concretization); + ConstraintSet(ref ics); + ConstraintSet(const std::vector> &ics); ConstraintSet(); void addConstraint(ref e, const Assignment &delta); @@ -55,7 +59,8 @@ class ConstraintSet { return _constraints < b._constraints || (_constraints == b._constraints && _symcretes < b._symcretes); } - + ConstraintSet getConcretizedVersion() const; + ConstraintSet getConcretizedVersion(const Assignment &c) const; void dump() const; void print(llvm::raw_ostream &os) const; @@ -64,11 +69,21 @@ class ConstraintSet { const constraints_ty &cs() const; const symcretes_ty &symcretes() const; const Assignment &concretization() const; + const IndependentConstraintSetUnion &independentElements() const; + + void getAllIndependentConstraintsSets( + ref queryExpr, + std::vector> &result) const; + + void getAllDependentConstraintsSets( + ref queryExpr, + std::vector> &result) const; private: constraints_ty _constraints; symcretes_ty _symcretes; Assignment _concretization; + IndependentConstraintSetUnion _independentElements; }; class PathConstraints { diff --git a/include/klee/Expr/IndependentSet.h b/include/klee/Expr/IndependentSet.h index 9173d90678..ef29498f5a 100644 --- a/include/klee/Expr/IndependentSet.h +++ b/include/klee/Expr/IndependentSet.h @@ -1,9 +1,13 @@ #ifndef KLEE_INDEPENDENTSET_H #define KLEE_INDEPENDENTSET_H +#include "klee/ADT/DisjointSetUnion.h" +#include "klee/ADT/PersistentMap.h" +#include "klee/ADT/PersistentSet.h" +#include "klee/Expr/Assignment.h" #include "klee/Expr/Expr.h" #include "klee/Expr/ExprHashMap.h" -#include "klee/Solver/Solver.h" +#include "klee/Expr/Symcrete.h" #include "klee/Support/CompilerWarning.h" DISABLE_WARNING_PUSH @@ -11,8 +15,10 @@ DISABLE_WARNING_DEPRECATED_DECLARATIONS #include "llvm/Support/raw_ostream.h" DISABLE_WARNING_POP -#include +#include #include +#include +#include namespace klee { @@ -42,7 +48,7 @@ template class DenseSet { return modified; } - bool intersects(const DenseSet &b) { + bool intersects(const DenseSet &b) const { for (typename set_ty::iterator it = s.begin(), ie = s.end(); it != ie; ++it) if (b.s.count(*it)) return true; @@ -76,54 +82,89 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, return os; } -class IndependentElementSet { +class IndependentConstraintSet { +private: + using InnerSetUnion = DisjointSetUnion, IndependentConstraintSet>; + public: - typedef std::map> elements_ty; + // All containers need to become persistent to make fast copy and faster + // merge possible map from concretized to normal + typedef PersistentMap> elements_ty; elements_ty elements; // Represents individual elements of array accesses (arr[1]) - std::set - wholeObjects; // Represents symbolically accessed arrays (arr[x]) - constraints_ty exprs; // All expressions (constraints) that are associated - // with this factor - SymcreteOrderedSet symcretes; // All symcretes associated with this factor + PersistentSet + wholeObjects; // Represents symbolically accessed arrays (arr[x]) + PersistentSet> exprs; // All expressions (constraints) that are + // associated with this factor + PersistentSet> + symcretes; // All symcretes associated with this factor + + Assignment concretization; + + InnerSetUnion concretizedSets; + + ref addExpr(ref e) const; + ref + updateConcretization(const Assignment &delta, + ExprHashMap> &changedExprs) const; + ref + removeConcretization(const Assignment &delta, + ExprHashMap> &changedExprs) const; - IndependentElementSet(); - IndependentElementSet(ref e); - IndependentElementSet(ref s); - IndependentElementSet(const IndependentElementSet &ies); + void + addValuesToAssignment(const std::vector &objects, + const std::vector> &values, + Assignment &assign) const; - IndependentElementSet &operator=(const IndependentElementSet &ies); + IndependentConstraintSet(); + IndependentConstraintSet(ref e); + IndependentConstraintSet(ref s); + IndependentConstraintSet(const ref &ics); + + IndependentConstraintSet &operator=(const IndependentConstraintSet &ies); void print(llvm::raw_ostream &os) const; - // more efficient when this is the smaller set - bool intersects(const IndependentElementSet &b); + static bool intersects(ref a, + ref b); - // returns true iff set is changed by addition - bool add(const IndependentElementSet &b); + static ref + merge(ref a, + ref b); + + // Extracts which arrays are referenced from a particular independent set. + // Examines both the actual known array accesses arr[1] plus the undetermined + // accesses arr[x].Z + void calculateArrayReferences(std::vector &returnVector) const; + + SymcreteOrderedSet getSymcretes() const { + SymcreteOrderedSet a; + for (ref s : symcretes) { + a.insert(s); + } + return a; + } + + constraints_ty getConstraints() const { + constraints_ty a; + for (ref e : exprs) { + a.insert(e); + } + return a; + } + mutable class ReferenceCounter _refCount; }; +void calculateArraysInFactors( + const std::vector> &factors, + ref queryExpr, std::vector &returnVector); + inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, - const IndependentElementSet &ies) { + const IndependentConstraintSet &ies) { ies.print(os); return os; } -// Breaks down a constraint into all of it's individual pieces, returning a -// list of IndependentElementSets or the independent factors. -// -// Caller takes ownership of returned std::list. -std::list * -getAllIndependentConstraintsSets(const Query &query); - -IndependentElementSet getIndependentConstraints(const Query &query, - constraints_ty &result); - -// Extracts which arrays are referenced from a particular independent set. -// Examines both the actual known array accesses arr[1] plus the undetermined -// accesses arr[x]. -void calculateArrayReferences(const IndependentElementSet &ie, - std::vector &returnVector); } // namespace klee #endif /* KLEE_INDEPENDENTSET_H */ diff --git a/lib/Expr/CMakeLists.txt b/lib/Expr/CMakeLists.txt index b7ca4e0124..758a4ca743 100644 --- a/lib/Expr/CMakeLists.txt +++ b/lib/Expr/CMakeLists.txt @@ -22,6 +22,7 @@ add_library(kleaverExpr ExprSMTLIBPrinter.cpp ExprUtil.cpp ExprVisitor.cpp + IndependentConstraintSetUnion.cpp IndependentSet.cpp Path.cpp SourceBuilder.cpp diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index 802a75bea4..22d45d6d29 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -181,18 +181,36 @@ class ExprReplaceVisitor3 : public ExprVisitor { ConstraintSet::ConstraintSet(constraints_ty cs, symcretes_ty symcretes, Assignment concretization) - : _constraints(cs), _symcretes(symcretes), _concretization(concretization) { + : _constraints(cs), _symcretes(symcretes), _concretization(concretization), + _independentElements(_constraints, _symcretes, _concretization) {} + +ConstraintSet::ConstraintSet(ref ics) + : _constraints(ics->getConstraints()), _symcretes(ics->getSymcretes()), + _concretization(ics->concretization), _independentElements(ics) {} + +ConstraintSet::ConstraintSet( + const std::vector> &factors) { + 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); + } } -ConstraintSet::ConstraintSet() : _concretization(Assignment(true)) {} +ConstraintSet::ConstraintSet() {} void ConstraintSet::addConstraint(ref e, const Assignment &delta) { _constraints.insert(e); - + _independentElements.addExpr(e); // Update bindings for (auto i : delta.bindings) { - _concretization.bindings[i.first] = i.second; + _concretization.bindings.replace({i.first, i.second}); } + _independentElements.updateConcretization(delta); } IDType Symcrete::idCounter = 0; @@ -200,9 +218,14 @@ IDType Symcrete::idCounter = 0; void ConstraintSet::addSymcrete(ref s, const Assignment &concretization) { _symcretes.insert(s); + _independentElements.addSymcrete(s); + Assignment dependentConcretization; for (auto i : s->dependentArrays()) { - _concretization.bindings[i] = concretization.bindings.at(i); + _concretization.bindings.replace({i, concretization.bindings.at(i)}); + dependentConcretization.bindings.replace( + {i, concretization.bindings.at(i)}); } + _independentElements.updateConcretization(dependentConcretization); } bool ConstraintSet::isSymcretized(ref expr) const { @@ -217,9 +240,31 @@ bool ConstraintSet::isSymcretized(ref expr) const { void ConstraintSet::rewriteConcretization(const Assignment &a) { for (auto i : a.bindings) { if (concretization().bindings.count(i.first)) { - _concretization.bindings[i.first] = i.second; + _concretization.bindings.replace({i.first, i.second}); } } + _independentElements.updateConcretization(a); +} + +ConstraintSet ConstraintSet::getConcretizedVersion() const { + ConstraintSet cs; + cs._independentElements = _independentElements.getConcretizedVersion(); + + for (ref e : cs._independentElements.is()) { + cs._constraints.insert(e); + } + return cs; +} + +ConstraintSet ConstraintSet::getConcretizedVersion( + const Assignment &newConcretization) const { + ConstraintSet cs; + cs._independentElements = + _independentElements.getConcretizedVersion(newConcretization); + for (ref e : cs._independentElements.is()) { + cs._constraints.insert(e); + } + return cs; } void ConstraintSet::print(llvm::raw_ostream &os) const { @@ -246,6 +291,11 @@ const constraints_ty &ConstraintSet::cs() const { return _constraints; } const symcretes_ty &ConstraintSet::symcretes() const { return _symcretes; } +const IndependentConstraintSetUnion & +ConstraintSet::independentElements() const { + return _independentElements; +} + const Path &PathConstraints::path() const { return _path; } const ExprHashMap &PathConstraints::indexes() const { @@ -523,6 +573,18 @@ Simplificator::composeExprDependencies(const ExprHashMap &upper, return result; } +void ConstraintSet::getAllIndependentConstraintsSets( + ref queryExpr, + std::vector> &result) const { + _independentElements.getAllIndependentConstraintSets(queryExpr, result); +} + +void ConstraintSet::getAllDependentConstraintsSets( + ref queryExpr, + std::vector> &result) const { + _independentElements.getAllDependentConstraintSets(queryExpr, result); +} + std::vector ConstraintSet::gatherArrays() const { std::vector arrays; findObjects(_constraints.begin(), _constraints.end(), arrays); diff --git a/lib/Expr/IndependentSet.cpp b/lib/Expr/IndependentSet.cpp index d4fade9ef1..ed602599b2 100644 --- a/lib/Expr/IndependentSet.cpp +++ b/lib/Expr/IndependentSet.cpp @@ -1,6 +1,7 @@ #include "klee/Expr/IndependentSet.h" #include "klee/ADT/Ref.h" +#include "klee/Expr/Assignment.h" #include "klee/Expr/Constraints.h" #include "klee/Expr/ExprHashMap.h" #include "klee/Expr/ExprUtil.h" @@ -16,9 +17,87 @@ namespace klee { -IndependentElementSet::IndependentElementSet() {} +ref +IndependentConstraintSet::addExpr(ref e) const { + ref ics = new IndependentConstraintSet(this); + ics->concretizedSets.addValue(concretization.evaluate(e)); + return ics; +} + +ref +IndependentConstraintSet::updateConcretization( + const Assignment &delta, ExprHashMap> &concretizedExprs) const { + ref ics = new IndependentConstraintSet(this); + if (delta.bindings.size() == 0) { + return ics; + } + for (auto i : delta.bindings) { + ics->concretization.bindings.replace({i.first, i.second}); + } + InnerSetUnion DSU; + for (ref i : exprs) { + ref e = ics->concretization.evaluate(i); + concretizedExprs[i] = e; + DSU.addValue(e); + } + for (ref s : symcretes) { + DSU.addValue(EqExpr::create(ics->concretization.evaluate(s->symcretized), + s->symcretized)); + } + ics->concretizedSets = DSU; + return ics; +} -IndependentElementSet::IndependentElementSet(ref e) { +ref +IndependentConstraintSet::removeConcretization( + const Assignment &delta, ExprHashMap> &concretizedExprs) const { + ref ics = new IndependentConstraintSet(this); + if (delta.bindings.size() == 0) { + return ics; + } + for (auto i : delta.bindings) { + ics->concretization.bindings.remove(i.first); + } + InnerSetUnion DSU; + for (ref i : exprs) { + ref e = ics->concretization.evaluate(i); + concretizedExprs[i] = e; + DSU.addValue(e); + } + for (ref s : symcretes) { + DSU.addValue(EqExpr::create(ics->concretization.evaluate(s->symcretized), + s->symcretized)); + } + + ics->concretizedSets = DSU; + return ics; +} + +void IndependentConstraintSet::addValuesToAssignment( + const std::vector &objects, + const std::vector> &values, + Assignment &assign) const { + for (unsigned i = 0; i < objects.size(); i++) { + if (assign.bindings.count(objects[i])) { + SparseStorage value = assign.bindings.at(objects[i]); + assert(value.size() == values[i].size() && + "we're talking about the same array here"); + DenseSet ds = (elements.find(objects[i]))->second; + for (std::set::iterator it2 = ds.begin(); it2 != ds.end(); + it2++) { + unsigned index = *it2; + value.store(index, values[i].load(index)); + } + assign.bindings.replace({objects[i], value}); + } else { + assign.bindings.replace({objects[i], values[i]}); + } + } +} + +IndependentConstraintSet::IndependentConstraintSet() {} + +IndependentConstraintSet::IndependentConstraintSet(ref e) { exprs.insert(e); // Track all reads in the program. Determines whether reads are // concrete or symbolic. If they are symbolic, "collapses" array @@ -39,19 +118,23 @@ IndependentElementSet::IndependentElementSet(ref e) { if (ConstantExpr *CE = dyn_cast(re->index)) { // if index constant, then add to set of constraints operating // on that array (actually, don't add constraint, just set index) - DenseSet &dis = elements[array]; + DenseSet dis; + if (elements.find(array) != elements.end()) { + dis = (elements.find(array))->second; + } dis.add((unsigned)CE->getZExtValue(32)); + elements.replace({array, dis}); } else { elements_ty::iterator it2 = elements.find(array); if (it2 != elements.end()) - elements.erase(it2); + elements.remove(it2->first); wholeObjects.insert(array); } } } } -IndependentElementSet::IndependentElementSet(ref s) { +IndependentConstraintSet::IndependentConstraintSet(ref s) { symcretes.insert(s); for (Symcrete &dependentSymcrete : s->dependentSymcretes()) { @@ -93,35 +176,45 @@ IndependentElementSet::IndependentElementSet(ref s) { if (ConstantExpr *CE = dyn_cast(re->index)) { // if index constant, then add to set of constraints operating // on that array (actually, don't add constraint, just set index) - DenseSet &dis = elements[array]; + DenseSet dis; + if (elements.find(array) != elements.end()) { + dis = (elements.find(array))->second; + } dis.add((unsigned)CE->getZExtValue(32)); + elements.replace({array, dis}); } else { elements_ty::iterator it2 = elements.find(array); if (it2 != elements.end()) - elements.erase(it2); + elements.remove(it2->first); wholeObjects.insert(array); } } } } -IndependentElementSet::IndependentElementSet(const IndependentElementSet &ies) - : elements(ies.elements), wholeObjects(ies.wholeObjects), exprs(ies.exprs) { -} - -IndependentElementSet & -IndependentElementSet::operator=(const IndependentElementSet &ies) { - elements = ies.elements; - wholeObjects = ies.wholeObjects; - exprs = ies.exprs; +IndependentConstraintSet::IndependentConstraintSet( + const ref &ics) + : elements(ics->elements), wholeObjects(ics->wholeObjects), + exprs(ics->exprs), symcretes(ics->symcretes), + concretization(ics->concretization), + concretizedSets(ics->concretizedSets) {} + +IndependentConstraintSet & +IndependentConstraintSet::operator=(const IndependentConstraintSet &ics) { + elements = ics.elements; + wholeObjects = ics.wholeObjects; + exprs = ics.exprs; + symcretes = ics.symcretes; + concretization = ics.concretization; + concretizedSets = ics.concretizedSets; return *this; } -void IndependentElementSet::print(llvm::raw_ostream &os) const { +void IndependentConstraintSet::print(llvm::raw_ostream &os) const { os << "{"; bool first = true; - for (std::set::iterator it = wholeObjects.begin(), - ie = wholeObjects.end(); + for (PersistentSet::iterator it = wholeObjects.begin(), + ie = wholeObjects.end(); it != ie; ++it) { const Array *array = *it; @@ -133,7 +226,7 @@ void IndependentElementSet::print(llvm::raw_ostream &os) const { os << "MO" << array->getIdentifier(); } - for (elements_ty::const_iterator it = elements.begin(), ie = elements.end(); + for (elements_ty::iterator it = elements.begin(), ie = elements.end(); it != ie; ++it) { const Array *array = it->first; const DenseSet &dis = it->second; @@ -149,218 +242,123 @@ void IndependentElementSet::print(llvm::raw_ostream &os) const { os << "}"; } -// more efficient when this is the smaller set -bool IndependentElementSet::intersects(const IndependentElementSet &b) { +bool IndependentConstraintSet::intersects( + ref a, + ref b) { + if (a->wholeObjects.size() + a->elements.size() > + b->wholeObjects.size() + b->elements.size()) { + std::swap(a, b); + } // If there are any symbolic arrays in our query that b accesses - for (std::set::iterator it = wholeObjects.begin(), - ie = wholeObjects.end(); + for (PersistentSet::iterator it = a->wholeObjects.begin(), + ie = a->wholeObjects.end(); it != ie; ++it) { const Array *array = *it; - if (b.wholeObjects.count(array) || - b.elements.find(array) != b.elements.end()) + if (b->wholeObjects.count(array) || + b->elements.find(array) != b->elements.end()) return true; } - for (elements_ty::iterator it = elements.begin(), ie = elements.end(); + for (elements_ty::iterator it = a->elements.begin(), ie = a->elements.end(); it != ie; ++it) { const Array *array = it->first; // if the array we access is symbolic in b - if (b.wholeObjects.count(array)) + if (b->wholeObjects.count(array)) return true; - elements_ty::const_iterator it2 = b.elements.find(array); + elements_ty::iterator it2 = b->elements.find(array); // if any of the elements we access are also accessed by b - if (it2 != b.elements.end()) { - if (it->second.intersects(it2->second)) + if (it2 != b->elements.end()) { + if (it->second.intersects(it2->second)) { return true; + } } } // No need to check symcretes here, arrays must be sufficient. return false; } -// returns true iff set is changed by addition -bool IndependentElementSet::add(const IndependentElementSet &b) { - for (auto expr : b.exprs) { - exprs.insert(expr); - } +ref +IndependentConstraintSet::merge(ref A, + ref B) { + ref a = new IndependentConstraintSet(A); + ref b = new IndependentConstraintSet(B); - for (const ref &symcrete : b.symcretes) { - symcretes.insert(symcrete); + if (a->wholeObjects.size() + a->elements.size() < + b->wholeObjects.size() + b->elements.size()) { + std::swap(a, b); + } + for (ref expr : b->exprs) { + a->exprs.insert(expr); + } + for (const ref &symcrete : b->symcretes) { + a->symcretes.insert(symcrete); } - bool modified = false; - for (std::set::const_iterator it = b.wholeObjects.begin(), - ie = b.wholeObjects.end(); + for (PersistentSet::iterator it = b->wholeObjects.begin(), + ie = b->wholeObjects.end(); it != ie; ++it) { const Array *array = *it; - elements_ty::iterator it2 = elements.find(array); - if (it2 != elements.end()) { - modified = true; - elements.erase(it2); - wholeObjects.insert(array); + elements_ty::iterator it2 = a->elements.find(array); + if (it2 != a->elements.end()) { + a->elements.remove(it2->first); + a->wholeObjects.insert(array); } else { - if (!wholeObjects.count(array)) { - modified = true; - wholeObjects.insert(array); + if (!a->wholeObjects.count(array)) { + a->wholeObjects.insert(array); } } } - for (elements_ty::const_iterator it = b.elements.begin(), - ie = b.elements.end(); + for (elements_ty::iterator it = b->elements.begin(), ie = b->elements.end(); it != ie; ++it) { const Array *array = it->first; - if (!wholeObjects.count(array)) { - elements_ty::iterator it2 = elements.find(array); - if (it2 == elements.end()) { - modified = true; - elements.insert(*it); + if (!a->wholeObjects.count(array)) { + elements_ty::iterator it2 = a->elements.find(array); + if (it2 == a->elements.end()) { + a->elements.insert(*it); } else { - // Now need to see if there are any (z=?)'s - if (it2->second.add(it->second)) - modified = true; + DenseSet dis = it2->second; + dis.add(it->second); + a->elements.replace({array, dis}); } } } - return modified; + b->addValuesToAssignment(b->concretization.keys(), b->concretization.values(), + a->concretization); + a->concretizedSets.add(b->concretizedSets); + return a; } -// Breaks down a constraint into all of it's individual pieces, returning a -// list of IndependentElementSets or the independent factors. -// -// Caller takes ownership of returned std::list. -std::list * -getAllIndependentConstraintsSets(const Query &query) { - std::list *factors = - new std::list(); - ConstantExpr *CE = dyn_cast(query.expr); - if (CE) { - assert(CE && CE->isFalse() && - "the expr should always be false and " - "therefore not included in factors"); - } else { - ref neg = Expr::createIsZero(query.expr); - factors->push_back(IndependentElementSet(neg)); - } - - for (const auto &constraint : query.constraints.cs()) { - // iterate through all the previously separated constraints. Until we - // actually return, factors is treated as a queue of expressions to be - // evaluated. If the queue property isn't maintained, then the exprs - // could be returned in an order different from how they came it, negatively - // affecting later stages. - factors->push_back(IndependentElementSet(constraint)); - } - - for (const auto &symcrete : query.constraints.symcretes()) { - factors->push_back(IndependentElementSet(symcrete)); - } - - bool doneLoop = false; - do { - doneLoop = true; - std::list *done = - new std::list; - while (factors->size() > 0) { - IndependentElementSet current = factors->front(); - factors->pop_front(); - // This list represents the set of factors that are separate from current. - // Those that are not inserted into this list (queue) intersect with - // current. - std::list *keep = - new std::list; - while (factors->size() > 0) { - IndependentElementSet compare = factors->front(); - factors->pop_front(); - if (current.intersects(compare)) { - if (current.add(compare)) { - // Means that we have added (z=y)added to (x=y) - // Now need to see if there are any (z=?)'s - doneLoop = false; - } - } else { - keep->push_back(compare); - } - } - done->push_back(current); - delete factors; - factors = keep; - } - delete factors; - factors = done; - } while (!doneLoop); - - return factors; -} - -IndependentElementSet getIndependentConstraints(const Query &query, - constraints_ty &result) { - IndependentElementSet eltsClosure(query.expr); - std::vector, IndependentElementSet>> worklist; - - for (const auto &constraint : query.constraints.cs()) - worklist.push_back( - std::make_pair(constraint, IndependentElementSet(constraint))); - - for (const ref &symcrete : query.constraints.symcretes()) { - worklist.push_back( - std::make_pair(symcrete->symcretized, IndependentElementSet(symcrete))); - } - - // XXX This should be more efficient (in terms of low level copy stuff). - bool done = false; - do { - done = true; - std::vector, IndependentElementSet>> newWorklist; - for (std::vector, IndependentElementSet>>::iterator - it = worklist.begin(), - ie = worklist.end(); - it != ie; ++it) { - if (it->second.intersects(eltsClosure)) { - if (eltsClosure.add(it->second)) - done = false; - result.insert(it->first); - // Means that we have added (z=y)added to (x=y) - // Now need to see if there are any (z=?)'s - } else { - newWorklist.push_back(*it); - } - } - worklist.swap(newWorklist); - } while (!done); - - // KLEE_DEBUG( - // std::set> reqset(result.begin(), result.end()); - // errs() << "--\n"; errs() << "Q: " << query.expr << "\n"; - // errs() << "\telts: " << IndependentElementSet(query.expr) << "\n"; - // int i = 0; for (const auto &constraint - // : query.constraints) { - // errs() << "C" << i++ << ": " << constraint; - // errs() << " " - // << (reqset.count(constraint) ? "(required)" : "(independent)") - // << "\n"; - // errs() << "\telts: " << IndependentElementSet(constraint) << "\n"; - // } errs() << "elts closure: " - // << eltsClosure << "\n";); - - return eltsClosure; -} - -void calculateArrayReferences(const IndependentElementSet &ie, - std::vector &returnVector) { +void IndependentConstraintSet::calculateArrayReferences( + std::vector &returnVector) const { std::set thisSeen; - for (std::map>::const_iterator it = - ie.elements.begin(); - it != ie.elements.end(); it++) { + for (IndependentConstraintSet::elements_ty::iterator it = elements.begin(); + it != elements.end(); ++it) { thisSeen.insert(it->first); } - for (std::set::iterator it = ie.wholeObjects.begin(); - it != ie.wholeObjects.end(); it++) { - assert(*it); + for (PersistentSet::iterator it = wholeObjects.begin(); + it != wholeObjects.end(); ++it) { thisSeen.insert(*it); } for (std::set::iterator it = thisSeen.begin(); - it != thisSeen.end(); it++) { + it != thisSeen.end(); ++it) { returnVector.push_back(*it); } } +void calculateArraysInFactors( + const std::vector> &factors, + ref queryExpr, std::vector &returnVector) { + std::set returnSet; + for (ref ics : factors) { + std::vector result; + ics->calculateArrayReferences(result); + returnSet.insert(result.begin(), result.end()); + } + std::vector result; + ref queryExprSet = + new IndependentConstraintSet(queryExpr); + queryExprSet->calculateArrayReferences(result); + returnSet.insert(result.begin(), result.end()); + returnVector.insert(returnVector.begin(), returnSet.begin(), returnSet.end()); +} + } // namespace klee diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 9e0139200a..a8c7fb8ede 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -64,32 +64,23 @@ class IndependentSolver : public SolverImpl { bool IndependentSolver::computeValidity(const Query &query, PartialValidity &result) { - constraints_ty required; - IndependentElementSet eltsClosure = - getIndependentConstraints(query, required); - ConstraintSet tmp( - required, eltsClosure.symcretes, - query.constraints.concretization().part(eltsClosure.symcretes)); + std::vector> factors; + query.getAllDependentConstraintsSets(factors); + ConstraintSet tmp(factors); return solver->impl->computeValidity(query.withConstraints(tmp), result); } bool IndependentSolver::computeTruth(const Query &query, bool &isValid) { - constraints_ty required; - IndependentElementSet eltsClosure = - getIndependentConstraints(query, required); - ConstraintSet tmp( - required, eltsClosure.symcretes, - query.constraints.concretization().part(eltsClosure.symcretes)); + std::vector> factors; + query.getAllDependentConstraintsSets(factors); + ConstraintSet tmp(factors); return solver->impl->computeTruth(query.withConstraints(tmp), isValid); } bool IndependentSolver::computeValue(const Query &query, ref &result) { - constraints_ty required; - IndependentElementSet eltsClosure = - getIndependentConstraints(query, required); - ConstraintSet tmp( - required, eltsClosure.symcretes, - query.constraints.concretization().part(eltsClosure.symcretes)); + std::vector> factors; + query.getAllDependentConstraintsSets(factors); + ConstraintSet tmp(factors); return solver->impl->computeValue(query.withConstraints(tmp), result); } @@ -99,22 +90,26 @@ bool IndependentSolver::computeValue(const Query &query, ref &result) { bool assertCreatedPointEvaluatesToTrue( const Query &query, const std::vector &objects, std::vector> &values, - std::map> &retMap) { + Assignment::bindings_ty &retMap) { // _allowFreeValues is set to true so that if there are missing bytes in the // assignment we will end up with a non ConstantExpr after evaluating the // assignment and fail - Assignment assign = Assignment(objects, values, /*_allowFreeValues=*/true); + Assignment assign = Assignment(objects, values); // Add any additional bindings. // The semantics of std::map should be to not insert a (key, value) // pair if it already exists so we should continue to use the assignment // from ``objects`` and ``values``. - if (retMap.size() > 0) - assign.bindings.insert(retMap.begin(), retMap.end()); - + if (retMap.size() > 0) { + for (auto it : retMap) { + assign.bindings.insert(it); + } + } for (auto const &constraint : query.constraints.cs()) { ref ret = assign.evaluate(constraint); - + if (!isa(ret)) { + ret = ret->rebuild(); + } assert(isa(ret) && "assignment evaluation did not result in constant"); ref evaluatedConstraint = dyn_cast(ret); @@ -124,15 +119,17 @@ bool assertCreatedPointEvaluatesToTrue( } ref neg = Expr::createIsZero(query.expr); ref q = assign.evaluate(neg); + if (!isa(q)) { + q = q->rebuild(); + } assert(isa(q) && "assignment evaluation did not result in constant"); return cast(q)->isTrue(); } -bool assertCreatedPointEvaluatesToTrue( - const Query &query, - std::map> &bindings, - std::map> &retMap) { +bool assertCreatedPointEvaluatesToTrue(const Query &query, + Assignment::bindings_ty &bindings, + Assignment::bindings_ty &retMap) { std::vector objects; std::vector> values; objects.reserve(bindings.size()); @@ -151,82 +148,89 @@ bool IndependentSolver::computeInitialValues( // This is important in case we don't have any constraints but // we need initial values for requested array objects. hasSolution = true; - // FIXME: When we switch to C++11 this should be a std::unique_ptr so we don't - // need to remember to manually call delete - std::list *factors = - getAllIndependentConstraintsSets(query); + Assignment retMap; + std::vector> dependentFactors; + query.getAllDependentConstraintsSets(dependentFactors); + ConstraintSet dependentConstriants(dependentFactors); + + std::vector dependentFactorsObjects; + calculateArraysInFactors(dependentFactors, query.expr, + dependentFactorsObjects); + + if (dependentFactorsObjects.size() != 0) { + std::vector> dependentFactorsValues; + + if (!solver->impl->computeInitialValues( + query.withConstraints(dependentConstriants), + dependentFactorsObjects, dependentFactorsValues, hasSolution)) { + values.clear(); + return false; + } else if (!hasSolution) { + values.clear(); + return true; + } else { + retMap = Assignment(dependentFactorsObjects, dependentFactorsValues); + } + } + + std::vector> independentFactors; + query.getAllIndependentConstraintsSets(independentFactors); // Used to rearrange all of the answers into the correct order - std::map> retMap; - for (std::list::iterator it = factors->begin(); - it != factors->end(); ++it) { + for (ref it : independentFactors) { std::vector arraysInFactor; - calculateArrayReferences(*it, arraysInFactor); + it->calculateArrayReferences(arraysInFactor); // Going to use this as the "fresh" expression for the Query() invocation // below assert(it->exprs.size() >= 1 && "No null/empty factors"); if (arraysInFactor.size() == 0) { continue; } - ConstraintSet tmp(it->exprs, it->symcretes, - query.constraints.concretization().part(it->symcretes)); + ConstraintSet tmp(it); std::vector> tempValues; if (!solver->impl->computeInitialValues( Query(tmp, ConstantExpr::alloc(0, Expr::Bool)), arraysInFactor, tempValues, hasSolution)) { values.clear(); - delete factors; + return false; } else if (!hasSolution) { values.clear(); - delete factors; + return true; } else { assert(tempValues.size() == arraysInFactor.size() && "Should be equal number arrays and answers"); - for (unsigned i = 0; i < tempValues.size(); i++) { - if (retMap.count(arraysInFactor[i])) { - // We already have an array with some partially correct answers, - // so we need to place the answers to the new query into the right - // spot while avoiding the undetermined values also in the array - SparseStorage *tempPtr = &retMap[arraysInFactor[i]]; - assert(tempPtr->size() == tempValues[i].size() && - "we're talking about the same array here"); - klee::DenseSet *ds = &(it->elements[arraysInFactor[i]]); - for (std::set::iterator it2 = ds->begin(); it2 != ds->end(); - it2++) { - unsigned index = *it2; - tempPtr->store(index, tempValues[i].load(index)); - } - } else { - // Dump all the new values into the array - retMap[arraysInFactor[i]] = tempValues[i]; - } - } + // We already have an array with some partially correct answers, + // so we need to place the answers to the new query into the right + // spot while avoiding the undetermined values also in the array + it->addValuesToAssignment(arraysInFactor, tempValues, retMap); } } - Assignment solutionAssignment(retMap, true); for (std::vector::const_iterator it = objects.begin(); it != objects.end(); it++) { const Array *arr = *it; - if (!retMap.count(arr)) { + if (!retMap.bindings.count(arr)) { // this means we have an array that is somehow related to the // constraint, but whose values aren't actually required to // satisfy the query. ref arrayConstantSize = - dyn_cast(solutionAssignment.evaluate(arr->size)); + dyn_cast(retMap.evaluate(arr->size)); + arrayConstantSize->dump(); assert(arrayConstantSize && "Array of symbolic size had not receive value for size!"); SparseStorage ret(arrayConstantSize->getZExtValue()); values.push_back(ret); } else { - values.push_back(retMap[arr]); + values.push_back(retMap.bindings.at(arr)); } } - assert(assertCreatedPointEvaluatesToTrue(query, objects, values, retMap) && + + assert(assertCreatedPointEvaluatesToTrue(query, objects, values, + retMap.bindings) && "should satisfy the equation"); - delete factors; + return true; } @@ -234,47 +238,54 @@ bool IndependentSolver::check(const Query &query, ref &result) { // We assume the query has a solution except proven differently // This is important in case we don't have any constraints but // we need initial values for requested array objects. + // result = new ValidResponse(ValidityCore()); + Assignment retMap; + std::vector> dependentFactors; + query.getAllDependentConstraintsSets(dependentFactors); + ConstraintSet dependentConstriants(dependentFactors); + + std::vector dependentFactorsObjects; + std::vector> dependentFactorsValues; + ref dependentFactorsResult; + + calculateArraysInFactors(dependentFactors, query.expr, + dependentFactorsObjects); + + if (dependentFactorsObjects.size() != 0) { + if (!solver->impl->check(query.withConstraints(dependentConstriants), + dependentFactorsResult)) { + return false; + } else if (isa(dependentFactorsResult)) { + result = dependentFactorsResult; + return true; + } else { + bool success = dependentFactorsResult->tryGetInitialValuesFor( + dependentFactorsObjects, dependentFactorsValues); + assert(success && "Can not get initial values (Independent solver)!"); + retMap = Assignment(dependentFactorsObjects, dependentFactorsValues); + } + } - // FIXME: When we switch to C++11 this should be a std::unique_ptr so we don't - // need to remember to manually call delete - std::list *factors = - getAllIndependentConstraintsSets(query); + std::vector> independentFactors; + query.getAllIndependentConstraintsSets(independentFactors); // Used to rearrange all of the answers into the correct order - std::map> retMap; - for (std::list::iterator it = factors->begin(); - it != factors->end(); ++it) { + for (ref it : independentFactors) { std::vector arraysInFactor; - calculateArrayReferences(*it, arraysInFactor); + it->calculateArrayReferences(arraysInFactor); // Going to use this as the "fresh" expression for the Query() invocation // below assert(it->exprs.size() >= 1 && "No null/empty factors"); if (arraysInFactor.size() == 0) { continue; } - - constraints_ty factorConstraints = it->exprs; - ref factorExpr = ConstantExpr::alloc(0, Expr::Bool); - auto factorConstraintsExprIterator = - std::find(factorConstraints.begin(), factorConstraints.end(), - query.negateExpr().expr); - if (factorConstraintsExprIterator != factorConstraints.end()) { - factorConstraints.erase(factorConstraintsExprIterator); - factorExpr = query.expr; - } - ref tempResult; std::vector> tempValues; if (!solver->impl->check( - Query(ConstraintSet( - factorConstraints, it->symcretes, - query.constraints.concretization().part(it->symcretes)), - factorExpr), + Query(ConstraintSet(it), ConstantExpr::alloc(0, Expr::Bool)), tempResult)) { - delete factors; return false; } else if (isa(tempResult)) { - delete factors; result = tempResult; return true; } else { @@ -283,46 +294,28 @@ bool IndependentSolver::check(const Query &query, ref &result) { assert(success && "Can not get initial values (Independent solver)!"); assert(tempValues.size() == arraysInFactor.size() && "Should be equal number arrays and answers"); - for (unsigned i = 0; i < tempValues.size(); i++) { - if (retMap.count(arraysInFactor[i])) { - // We already have an array with some partially correct answers, - // so we need to place the answers to the new query into the right - // spot while avoiding the undetermined values also in the array - SparseStorage *tempPtr = &retMap[arraysInFactor[i]]; - assert(tempPtr->size() == tempValues[i].size() && - "we're talking about the same array here"); - klee::DenseSet *ds = &(it->elements[arraysInFactor[i]]); - for (std::set::iterator it2 = ds->begin(); it2 != ds->end(); - it2++) { - unsigned index = *it2; - tempPtr->store(index, tempValues[i].load(index)); - } - } else { - // Dump all the new values into the array - retMap[arraysInFactor[i]] = tempValues[i]; - } - } + // We already have an array with some partially correct answers, + // so we need to place the answers to the new query into the right + // spot while avoiding the undetermined values also in the array + it->addValuesToAssignment(arraysInFactor, tempValues, retMap); } } - result = new InvalidResponse(retMap); - std::map> bindings; + result = new InvalidResponse(retMap.bindings); + Assignment::bindings_ty bindings; bool success = result->tryGetInitialValues(bindings); assert(success); - assert(assertCreatedPointEvaluatesToTrue(query, bindings, retMap) && + assert(assertCreatedPointEvaluatesToTrue(query, bindings, retMap.bindings) && "should satisfy the equation"); - delete factors; + return true; } bool IndependentSolver::computeValidityCore(const Query &query, ValidityCore &validityCore, bool &isValid) { - constraints_ty required; - IndependentElementSet eltsClosure = - getIndependentConstraints(query, required); - ConstraintSet tmp( - required, eltsClosure.symcretes, - query.constraints.concretization().part(eltsClosure.symcretes)); + std::vector> factors; + query.getAllDependentConstraintsSets(factors); + ConstraintSet tmp(factors); return solver->impl->computeValidityCore(query.withConstraints(tmp), validityCore, isValid); } From d9ae5a3f1c55ca0125972f028edee0ffab366c11 Mon Sep 17 00:00:00 2001 From: dim8art Date: Sun, 20 Aug 2023 16:17:40 +0300 Subject: [PATCH 3/5] Reworking ConcretizingSolver --- lib/Solver/ConcretizingSolver.cpp | 190 ++++++++++++++++++------------ 1 file changed, 113 insertions(+), 77 deletions(-) diff --git a/lib/Solver/ConcretizingSolver.cpp b/lib/Solver/ConcretizingSolver.cpp index 36f5a81191..52ed3dbd11 100644 --- a/lib/Solver/ConcretizingSolver.cpp +++ b/lib/Solver/ConcretizingSolver.cpp @@ -55,18 +55,59 @@ class ConcretizingSolver : public SolverImpl { private: bool assertConcretization(const Query &query, const Assignment &assign) const; + bool getBrokenArrays(const Query &query, const Assignment &diff, + ref &result, + std::vector &brokenArrays); bool relaxSymcreteConstraints(const Query &query, ref &result); Query constructConcretizedQuery(const Query &, const Assignment &); + Query getConcretizedVersion(const Query &); + +private: + void reverseConcretization(ValidityCore &validityCore, + const ExprHashMap> &reverse, + ref reverseExpr); + void reverseConcretization(ref &res, + const ExprHashMap> &reverse, + ref reverseExpr); }; Query ConcretizingSolver::constructConcretizedQuery(const Query &query, const Assignment &assign) { - ConstraintSet constraints = assign.createConstraintsFromAssignment(); - for (auto e : query.constraints.cs()) { - constraints.addConstraint(e, {}); + ConstraintSet cs = query.constraints; + ref concretizedExpr = assign.evaluate(query.expr); + return Query(cs.getConcretizedVersion(assign), concretizedExpr); +} + +Query ConcretizingSolver::getConcretizedVersion(const Query &query) { + ConstraintSet cs = query.constraints; + ref concretizedExpr = cs.concretization().evaluate(query.expr); + return Query(cs.getConcretizedVersion(), concretizedExpr); +} + +void ConcretizingSolver::reverseConcretization( + ValidityCore &validityCore, const ExprHashMap> &reverse, + ref reverseExpr) { + validityCore.expr = reverseExpr; + for (auto e : reverse) { + if (validityCore.constraints.find(e.second) != + validityCore.constraints.end()) { + validityCore.constraints.erase(e.second); + validityCore.constraints.insert(e.first); + } + } +} + +void ConcretizingSolver::reverseConcretization( + ref &res, const ExprHashMap> &reverse, + ref reverseExpr) { + if (!isa(res)) { + return; } - return Query(constraints, query.expr); + ValidityCore validityCore; + res->tryGetValidityCore(validityCore); + reverseConcretization(validityCore, reverse, reverseExpr); + res = new ValidResponse(validityCore); } bool ConcretizingSolver::assertConcretization(const Query &query, @@ -80,6 +121,41 @@ bool ConcretizingSolver::assertConcretization(const Query &query, return true; } +bool ConcretizingSolver::getBrokenArrays( + const Query &query, const Assignment &assign, ref &result, + std::vector &brokenArrays) { + Query concretizedQuery = constructConcretizedQuery(query, assign); + ref CE = dyn_cast(concretizedQuery.expr); + if (CE && CE->isTrue()) { + findObjects(query.expr, brokenArrays); + result = new UnknownResponse(); + return true; + } + const ExprHashMap> &reverse = + concretizedQuery.constraints.independentElements().concretizedExprs; + ref reverseExpr = query.expr; + if (!solver->impl->check(concretizedQuery, result)) { + return false; + } + reverseConcretization(result, reverse, reverseExpr); + + /* No unsat cores were found for the query, so we can try to find new + * solution. */ + if (isa(result)) { + return true; + } + + ValidityCore validityCore; + bool success = result->tryGetValidityCore(validityCore); + assert(success); + + constraints_ty allValidityCoreConstraints = validityCore.constraints; + allValidityCoreConstraints.insert(validityCore.expr); + findObjects(allValidityCoreConstraints.begin(), + allValidityCoreConstraints.end(), brokenArrays); + return true; +} + bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query, ref &result) { if (!query.containsSizeSymcretes()) { @@ -111,28 +187,17 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query, bool wereConcretizationsRemoved = true; while (wereConcretizationsRemoved) { wereConcretizationsRemoved = false; - if (!solver->impl->check(constructConcretizedQuery(query, assignment), - result)) { + + std::vector currentlyBrokenSymcretizedArrays; + if (!getBrokenArrays(query, assignment, result, + currentlyBrokenSymcretizedArrays)) { return false; } - /* No unsat cores were found for the query, so we can try to find new - * solution. */ if (isa(result)) { break; } - ValidityCore validityCore; - bool success = result->tryGetValidityCore(validityCore); - assert(success); - - constraints_ty allValidityCoreConstraints = validityCore.constraints; - allValidityCoreConstraints.insert(validityCore.expr); - std::vector currentlyBrokenSymcretizedArrays; - findObjects(allValidityCoreConstraints.begin(), - allValidityCoreConstraints.end(), - currentlyBrokenSymcretizedArrays); - std::queue arrayQueue; std::queue addressQueue; @@ -159,9 +224,10 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query, if (arrayQueue.empty() && addressArrayPresent) { while (!addressQueue.empty()) { - assignment.bindings.erase(addressQueue.front()); + assignment.bindings.remove(addressQueue.front()); addressQueue.pop(); } + if (!solver->impl->check(constructConcretizedQuery(query, assignment), result)) { return false; @@ -175,7 +241,7 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query, while (!arrayQueue.empty()) { const Array *brokenArray = arrayQueue.front(); - assignment.bindings.erase(brokenArray); + assignment.bindings.remove(brokenArray); wereConcretizationsRemoved = true; arrayQueue.pop(); @@ -198,14 +264,15 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query, } for (const ref &symcrete : currentlyBrokenSymcretes) { - constraints_ty required; - IndependentElementSet eltsClosure = getIndependentConstraints( - Query(query.constraints, - AndExpr::create(query.expr, - Expr::createIsZero(symcrete->symcretized))), - required); - for (ref symcrete : eltsClosure.symcretes) { - currentlyBrokenSymcretes.insert(symcrete); + std::vector> factors; + Query(query.constraints, + AndExpr::create(query.expr, + Expr::createIsZero(symcrete->symcretized))) + .getAllDependentConstraintsSets(factors); + for (ref ics : factors) { + for (ref symcrete : ics->symcretes) { + currentlyBrokenSymcretes.insert(symcrete); + } } } @@ -281,7 +348,7 @@ bool ConcretizingSolver::relaxSymcreteConstraints(const Query &query, } for (unsigned idx = 0; idx < objects.size(); ++idx) { - assignment.bindings[objects[idx]] = brokenSymcretizedValues[idx]; + assignment.bindings.replace({objects[idx], brokenSymcretizedValues[idx]}); } ExprHashMap> concretizations; @@ -378,37 +445,10 @@ bool ConcretizingSolver::computeValidity( assert(assertConcretization(query, assign) && "Assignment does not contain concretization for all symcrete arrays!"); - auto concretizedQuery = constructConcretizedQuery(query, assign); - if (!solver->impl->computeValidity(concretizedQuery, queryResult, - negatedQueryResult)) { + if (!check(query, queryResult) || + !check(query.negateExpr(), negatedQueryResult)) { return false; } - - std::vector> queryResultValues, - negatedQueryResultValues; - - std::vector objects = assign.keys(); - - assert(isa(queryResult) || - isa(negatedQueryResult)); - - // *No more than one* of queryResult and negatedQueryResult is possible, - // i.e. `mustBeTrue` with values from `assign`. - // Take one which is `mustBeTrue` with symcretes from `assign` - // and try to relax them to `mayBeFalse`. This solution should be - // appropriate for the remain branch. - - if (isa(queryResult)) { - if (!relaxSymcreteConstraints(query, queryResult)) { - return false; - } - } else if (isa(negatedQueryResult)) { - if (!relaxSymcreteConstraints(query.negateExpr(), negatedQueryResult)) { - return false; - } - } else { - } - return true; } @@ -421,12 +461,15 @@ bool ConcretizingSolver::check(const Query &query, assert(assertConcretization(query, assign) && "Assignment does not contain concretization for all symcrete arrays!"); - auto concretizedQuery = constructConcretizedQuery(query, assign); - if (!solver->impl->check(concretizedQuery, result)) { - return false; - } + auto concretizedQuery = getConcretizedVersion(query); - if (isa(result)) { + ref CE = dyn_cast(concretizedQuery.expr); + if (!CE || !CE->isTrue()) { + if (!solver->impl->check(concretizedQuery, result)) { + return false; + } + } + if ((CE && CE->isTrue()) || isa(result)) { if (!relaxSymcreteConstraints(query, result)) { return false; } @@ -455,8 +498,7 @@ bool ConcretizingSolver::computeTruth(const Query &query, bool &isValid) { query.constraints.concretization().evaluate(query.expr))) { isValid = CE->isTrue(); } else { - auto concretizedQuery = constructConcretizedQuery(query, assign); - + auto concretizedQuery = getConcretizedVersion(query); if (!solver->impl->computeTruth(concretizedQuery, isValid)) { return false; } @@ -471,9 +513,7 @@ bool ConcretizingSolver::computeTruth(const Query &query, bool &isValid) { if (!relaxSymcreteConstraints(query, result)) { return false; } - if (ref resultInvalidResponse = - dyn_cast(result)) { - assign = resultInvalidResponse->initialValuesFor(assign.keys()); + if (isa(result)) { isValid = false; } } @@ -491,7 +531,7 @@ bool ConcretizingSolver::computeValidityCore(const Query &query, assert(assertConcretization(query, assign) && "Assignment does not contain concretization for all symcrete arrays!"); - Query concretizedQuery = constructConcretizedQuery(query, assign); + Query concretizedQuery = getConcretizedVersion(query); if (ref CE = dyn_cast( query.constraints.concretization().evaluate(query.expr))) { @@ -544,7 +584,7 @@ bool ConcretizingSolver::computeValue(const Query &query, ref &result) { result = expr; return true; } - auto concretizedQuery = constructConcretizedQuery(query, assign); + auto concretizedQuery = getConcretizedVersion(query); return solver->impl->computeValue(concretizedQuery, result); } @@ -560,7 +600,7 @@ bool ConcretizingSolver::computeInitialValues( assert(assertConcretization(query, assign) && "Assignment does not contain concretization for all symcrete arrays!"); - auto concretizedQuery = constructConcretizedQuery(query, assign); + auto concretizedQuery = getConcretizedVersion(query); if (!solver->impl->computeInitialValues(concretizedQuery, objects, values, hasSolution)) { return false; @@ -576,11 +616,7 @@ bool ConcretizingSolver::computeInitialValues( if (ref resultInvalidResponse = dyn_cast(result)) { hasSolution = true; - assign = resultInvalidResponse->initialValuesFor(assign.keys()); - values = std::vector>(); - return solver->impl->computeInitialValues( - constructConcretizedQuery(query, assign), objects, values, - hasSolution); + result->tryGetInitialValuesFor(objects, values); } } From bdf29c81fcef8a1e482ea04932dbbaaf87190e42 Mon Sep 17 00:00:00 2001 From: dim8art Date: Sun, 20 Aug 2023 16:18:06 +0300 Subject: [PATCH 4/5] Add persistency to Assignment --- include/klee/Expr/Assignment.h | 71 ++++++++++++++++++++++------------ lib/Expr/Assignment.cpp | 36 ++++++++++------- 2 files changed, 67 insertions(+), 40 deletions(-) diff --git a/include/klee/Expr/Assignment.h b/include/klee/Expr/Assignment.h index ad48af0baa..61376ff940 100644 --- a/include/klee/Expr/Assignment.h +++ b/include/klee/Expr/Assignment.h @@ -10,6 +10,7 @@ #ifndef KLEE_ASSIGNMENT_H #define KLEE_ASSIGNMENT_H +#include "klee/ADT/PersistentMap.h" #include "klee/ADT/SparseStorage.h" #include "klee/Expr/ExprEvaluator.h" @@ -27,9 +28,9 @@ using symcretes_ty = SymcreteOrderedSet; class Assignment { public: - typedef std::map> bindings_ty; + using bindings_ty = + PersistentMap>; - bool allowFreeValues; bindings_ty bindings; friend bool operator==(const Assignment &lhs, const Assignment &rhs) { @@ -37,14 +38,10 @@ class Assignment { } public: - Assignment(bool _allowFreeValues = false) - : allowFreeValues(_allowFreeValues) {} - Assignment(const bindings_ty &_bindings, bool _allowFreeValues = false) - : allowFreeValues(_allowFreeValues), bindings(_bindings) {} + Assignment() {} + Assignment(const bindings_ty &_bindings) : bindings(_bindings) {} Assignment(const std::vector &objects, - const std::vector> &values, - bool _allowFreeValues = false) - : allowFreeValues(_allowFreeValues) { + const std::vector> &values) { assert(objects.size() == values.size()); for (unsigned i = 0; i < values.size(); ++i) { const Array *os = objects.at(i); @@ -53,19 +50,26 @@ class Assignment { } } - ref evaluate(const Array *mo, unsigned index) const; - ref evaluate(ref e) const; - ConstraintSet createConstraintsFromAssignment() const; + void addIndependentAssignment(const Assignment &b); + + ref evaluate(const Array *mo, unsigned index, + bool allowFreeValues = true) const; + ref evaluate(ref e, bool allowFreeValues = true) const; + constraints_ty createConstraintsFromAssignment() const; template - bool satisfies(InputIterator begin, InputIterator end); + bool satisfies(InputIterator begin, InputIterator end, + bool allowFreeValues = true); + template + bool satisfiesNonBoolean(InputIterator begin, InputIterator end, + bool allowFreeValues = true); void dump() const; Assignment diffWith(const Assignment &other) const; Assignment part(const SymcreteOrderedSet &symcretes) const; - bindings_ty::const_iterator begin() const { return bindings.begin(); } - bindings_ty::const_iterator end() const { return bindings.end(); } + bindings_ty::iterator begin() const { return bindings.begin(); } + bindings_ty::iterator end() const { return bindings.end(); } bool isEmpty() { return begin() == end(); } std::vector keys() const; @@ -74,22 +78,24 @@ class Assignment { class AssignmentEvaluator : public ExprEvaluator { const Assignment &a; + bool allowFreeValues; protected: ref getInitialValue(const Array &mo, unsigned index) { - return a.evaluate(&mo, index); + return a.evaluate(&mo, index, allowFreeValues); } public: - AssignmentEvaluator(const Assignment &_a) : a(_a) {} + AssignmentEvaluator(const Assignment &_a, bool _allowFreeValues) + : a(_a), allowFreeValues(_allowFreeValues) {} }; /***/ -inline ref Assignment::evaluate(const Array *array, - unsigned index) const { +inline ref Assignment::evaluate(const Array *array, unsigned index, + bool allowFreeValues) const { assert(array); - bindings_ty::const_iterator it = bindings.find(array); + bindings_ty::iterator it = bindings.find(array); if (it != bindings.end() && index < it->second.size()) { return ConstantExpr::alloc(it->second.load(index), array->getRange()); } else { @@ -102,17 +108,32 @@ inline ref Assignment::evaluate(const Array *array, } } -inline ref Assignment::evaluate(ref e) const { - AssignmentEvaluator v(*this); +inline ref Assignment::evaluate(ref e, bool allowFreeValues) const { + AssignmentEvaluator v(*this, allowFreeValues); return v.visit(e); } template -inline bool Assignment::satisfies(InputIterator begin, InputIterator end) { - AssignmentEvaluator v(*this); - for (; begin != end; ++begin) +inline bool Assignment::satisfies(InputIterator begin, InputIterator end, + bool allowFreeValues) { + AssignmentEvaluator v(*this, allowFreeValues); + for (; begin != end; ++begin) { + assert((*begin)->getWidth() == Expr::Bool && "constraints must be boolean"); if (!v.visit(*begin)->isTrue()) return false; + } + return true; +} + +template +inline bool Assignment::satisfiesNonBoolean(InputIterator begin, + InputIterator end, + bool allowFreeValues) { + AssignmentEvaluator v(*this, allowFreeValues); + for (; begin != end; ++begin) { + if (!isa(v.visit(*begin))) + return false; + } return true; } } // namespace klee diff --git a/lib/Expr/Assignment.cpp b/lib/Expr/Assignment.cpp index d43db33870..1cc7a76e1c 100644 --- a/lib/Expr/Assignment.cpp +++ b/lib/Expr/Assignment.cpp @@ -20,8 +20,8 @@ void Assignment::dump() const { llvm::errs() << "No bindings\n"; return; } - for (bindings_ty::const_iterator i = bindings.begin(), e = bindings.end(); - i != e; ++i) { + for (bindings_ty::iterator i = bindings.begin(), e = bindings.end(); i != e; + ++i) { llvm::errs() << (*i).first->getName() << "\n["; for (int j = 0, k = (*i).second.size(); j < k; ++j) llvm::errs() << (int)(*i).second.load(j) << ","; @@ -29,8 +29,14 @@ void Assignment::dump() const { } } -ConstraintSet Assignment::createConstraintsFromAssignment() const { - ConstraintSet result; +void Assignment::addIndependentAssignment(const Assignment &b) { + for (auto it : b) { + bindings.insert(it); + } +} + +constraints_ty Assignment::createConstraintsFromAssignment() const { + constraints_ty result; for (const auto &binding : bindings) { const auto &array = binding.first; const auto &values = binding.second; @@ -41,17 +47,15 @@ ConstraintSet Assignment::createConstraintsFromAssignment() const { uint64_t arraySize = arrayConstantSize->getZExtValue(); if (arraySize <= 8 && array->getRange() == Expr::Int8) { ref e = Expr::createTempRead(array, arraySize * array->getRange()); - result.addConstraint(EqExpr::create(e, evaluate(e)), {}); + result.insert(EqExpr::create(e, evaluate(e))); } else { for (unsigned arrayIndex = 0; arrayIndex < arraySize; ++arrayIndex) { unsigned char value = values.load(arrayIndex); - result.addConstraint( - EqExpr::create( - ReadExpr::create( - UpdateList(array, 0), - ConstantExpr::alloc(arrayIndex, array->getDomain())), - ConstantExpr::alloc(value, array->getRange())), - {}); + result.insert(EqExpr::create( + ReadExpr::create( + UpdateList(array, 0), + ConstantExpr::alloc(arrayIndex, array->getDomain())), + ConstantExpr::alloc(value, array->getRange()))); } } } @@ -59,7 +63,7 @@ ConstraintSet Assignment::createConstraintsFromAssignment() const { } Assignment Assignment::diffWith(const Assignment &other) const { - Assignment diffAssignment(allowFreeValues); + Assignment diffAssignment; for (const auto &it : other) { if (bindings.count(it.first) == 0 || bindings.at(it.first) != it.second) { diffAssignment.bindings.insert(it); @@ -87,10 +91,12 @@ std::vector> Assignment::values() const { } Assignment Assignment::part(const SymcreteOrderedSet &symcretes) const { - Assignment ret(allowFreeValues); + Assignment ret; for (auto symcrete : symcretes) { for (auto array : symcrete->dependentArrays()) { - ret.bindings.insert({array, bindings.at(array)}); + if (bindings.find(array) != bindings.end()) { + ret.bindings.insert({array, bindings.at(array)}); + } } } return ret; From e319a6f4e004f5bceaeed6c48fc5dc1ee3db8d61 Mon Sep 17 00:00:00 2001 From: dim8art Date: Sun, 20 Aug 2023 17:24:21 +0300 Subject: [PATCH 5/5] Rework solver chain + small refactoring changes --- include/klee/ADT/ImmutableMap.h | 27 +++++++++++ include/klee/ADT/PersistentMap.h | 4 ++ include/klee/Expr/Expr.h | 7 +++ include/klee/Solver/SolverUtil.h | 30 +++++++++--- lib/Core/Executor.cpp | 42 +++++++++------- lib/Core/SeedInfo.cpp | 8 ++- lib/Core/SeedInfo.h | 3 +- lib/Solver/AssignmentValidatingSolver.cpp | 8 ++- lib/Solver/CachingSolver.cpp | 1 - lib/Solver/CexCachingSolver.cpp | 59 ++++++++++++++++------- lib/Solver/ConstructSolverChain.cpp | 9 ++++ lib/Solver/FastCexSolver.cpp | 1 - lib/Solver/QueryLoggingSolver.cpp | 17 +++---- lib/Solver/Solver.cpp | 2 +- lib/Solver/ValidatingSolver.cpp | 5 +- lib/Solver/Z3Solver.cpp | 4 -- test/Expr/Evaluate.kquery | 2 +- test/Feature/DanglingConcreteReadExpr.c | 2 +- test/Solver/CexCacheValidityCoresCheck.c | 4 +- tools/kleaver/main.cpp | 11 ++--- unittests/Assignment/AssignmentTest.cpp | 2 +- unittests/Expr/ArrayExprTest.cpp | 3 +- 22 files changed, 168 insertions(+), 83 deletions(-) diff --git a/include/klee/ADT/ImmutableMap.h b/include/klee/ADT/ImmutableMap.h index d79a4d5790..44cacedc33 100644 --- a/include/klee/ADT/ImmutableMap.h +++ b/include/klee/ADT/ImmutableMap.h @@ -44,6 +44,32 @@ template > class ImmutableMap { return *this; } + bool operator==(const ImmutableMap &b) const { + if (size() != b.size()) { + return false; + } + for (iterator it1 = begin(), it2 = b.begin(); + it1 != end() && it2 != b.end(); ++it1, ++it2) { + if (*it1 != *it2) + return false; + } + return true; + } + + bool operator<(const ImmutableMap &b) const { + if (size() != b.size()) { + return size() < b.size(); + } + for (iterator it1 = begin(), it2 = b.begin(); + it1 != end() && it2 != b.end(); ++it1, ++it2) { + if (*it1 < *it2) + return true; + if (*it1 > *it2) + return false; + } + return false; + } + bool empty() const { return elts.empty(); } size_t count(const key_type &key) const { return elts.count(key); } const value_type *lookup(const key_type &key) const { @@ -80,6 +106,7 @@ template > class ImmutableMap { return elts.upper_bound(key); } + const D &at(const key_type &key) const { return find(key)->second; } static size_t getAllocated() { return Tree::allocated; } }; diff --git a/include/klee/ADT/PersistentMap.h b/include/klee/ADT/PersistentMap.h index bfec1824a0..dabc5495db 100644 --- a/include/klee/ADT/PersistentMap.h +++ b/include/klee/ADT/PersistentMap.h @@ -37,6 +37,8 @@ template > class PersistentMap { elts = b.elts; return *this; } + bool operator==(const PersistentMap &b) const { return elts == b.elts; } + bool operator<(const PersistentMap &b) const { return elts < b.elts; } bool empty() const { return elts.empty(); } size_t count(const key_type &key) const { return elts.count(key); } @@ -77,6 +79,8 @@ template > class PersistentMap { return *lookup(key); } } + + const D &at(const key_type &key) const { return elts.at(key); } }; } // namespace klee diff --git a/include/klee/Expr/Expr.h b/include/klee/Expr/Expr.h index 8e258b8f56..ab6826e25d 100644 --- a/include/klee/Expr/Expr.h +++ b/include/klee/Expr/Expr.h @@ -328,6 +328,13 @@ class Expr { // Given an array of new kids return a copy of the expression // but using those children. virtual ref rebuild(ref kids[/* getNumKids() */]) const = 0; + virtual ref rebuild() const { + ref kids[getNumKids()]; + for (unsigned i = 0; i < getNumKids(); ++i) { + kids[i] = getKid(i); + } + return rebuild(kids); + } /// isZero - Is this a constant zero. bool isZero() const; diff --git a/include/klee/Solver/SolverUtil.h b/include/klee/Solver/SolverUtil.h index d61c188cc0..d55f372de1 100644 --- a/include/klee/Solver/SolverUtil.h +++ b/include/klee/Solver/SolverUtil.h @@ -5,6 +5,7 @@ #include "klee/Expr/Constraints.h" #include "klee/Expr/Expr.h" #include "klee/Expr/ExprHashMap.h" +#include "klee/Expr/IndependentSet.h" #include "klee/System/Time.h" namespace klee { @@ -80,6 +81,16 @@ struct Query { (lhs.constraints == rhs.constraints && lhs.expr < rhs.expr); } + void getAllIndependentConstraintsSets( + std::vector> &result) const { + constraints.getAllIndependentConstraintsSets(expr, result); + } + + void getAllDependentConstraintsSets( + std::vector> &result) const { + constraints.getAllDependentConstraintsSets(expr, result); + } + /// Dump query void dump() const; }; @@ -239,20 +250,20 @@ class InvalidResponse : public SolverResponse { } bool tryGetInitialValues(Assignment::bindings_ty &values) const { - values.insert(result.bindings.begin(), result.bindings.end()); + values = result.bindings; return true; } Assignment initialValuesFor(const std::vector objects) const { std::vector> values; tryGetInitialValuesFor(objects, values); - return Assignment(objects, values, true); + return Assignment(objects, values); } Assignment initialValues() const { Assignment::bindings_ty values; tryGetInitialValues(values); - return Assignment(values, true); + return Assignment(values); } ResponseKind getResponseKind() const { return Invalid; }; @@ -276,15 +287,20 @@ class InvalidResponse : public SolverResponse { return result.bindings < ib.result.bindings; } - bool satisfies(std::set> &key) { - return result.satisfies(key.begin(), key.end()); + bool satisfies(const std::set> &key, bool allowFreeValues = true) { + return result.satisfies(key.begin(), key.end(), allowFreeValues); } - ref evaluate(ref &e) { return result.evaluate(e); } + bool satisfiesNonBoolean(const std::set> &key, + bool allowFreeValues = true) { + return result.satisfiesNonBoolean(key.begin(), key.end(), allowFreeValues); + } void dump() { result.dump(); } - ref evaluate(ref e) { return (result.evaluate(e)); } + ref evaluate(ref e, bool allowFreeValues = true) { + return (result.evaluate(e, allowFreeValues)); + } }; class UnknownResponse : public SolverResponse { diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 064935305d..8bc362391d 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -1145,7 +1145,7 @@ Executor::StatePair Executor::fork(ExecutionState ¤t, ref condition, success = solver->mayBeFalse(current.constraints.cs(), condition, mayBeFalse, current.queryMetaData); } - if (success && !mayBeFalse) + if (!success || !mayBeFalse) terminateEverything = true; else res = PartialValidity::MayBeFalse; @@ -1154,7 +1154,7 @@ Executor::StatePair Executor::fork(ExecutionState ¤t, ref condition, bool mayBeTrue; success = solver->mayBeTrue(current.constraints.cs(), condition, mayBeTrue, current.queryMetaData); - if (success && !mayBeTrue) + if (!success || !mayBeTrue) terminateEverything = true; else res = PartialValidity::MayBeTrue; @@ -5419,18 +5419,19 @@ MemoryObject *Executor::allocate(ExecutionState &state, ref size, std::vector> symbolicSizesTerms = { ZExtExpr::create(size, pointerWidthInBits)}; - constraints_ty required; - IndependentElementSet eltsClosure = getIndependentConstraints( - Query(state.constraints.cs(), ZExtExpr::create(size, pointerWidthInBits)), - required); + std::vector> factors; + Query(state.constraints.cs(), ZExtExpr::create(size, pointerWidthInBits)) + .getAllDependentConstraintsSets(factors); + /* Collect dependent size symcretes. */ - for (ref symcrete : eltsClosure.symcretes) { - if (isa(symcrete)) { - symbolicSizesTerms.push_back( - ZExtExpr::create(symcrete->symcretized, pointerWidthInBits)); + for (ref ics : factors) { + for (ref symcrete : ics->symcretes) { + if (isa(symcrete)) { + symbolicSizesTerms.push_back( + ZExtExpr::create(symcrete->symcretized, pointerWidthInBits)); + } } } - ref symbolicSizesSum = createNonOverflowingSumExpr(symbolicSizesTerms); std::vector objects; @@ -5441,7 +5442,7 @@ MemoryObject *Executor::allocate(ExecutionState &state, ref size, return nullptr; } - Assignment assignment(objects, values, true); + Assignment assignment(objects, values); uint64_t sizeMemoryObject = cast(assignment.evaluate(size))->getZExtValue(); @@ -5471,7 +5472,8 @@ MemoryObject *Executor::allocate(ExecutionState &state, ref size, state.addPointerResolution(addressExpr, mo); } - assignment.bindings[addressArray] = sparseBytesFromValue(mo->address); + assignment.bindings.replace( + {addressArray, sparseBytesFromValue(mo->address)}); state.constraints.addSymcrete(sizeSymcrete, assignment); state.constraints.addSymcrete(addressSymcrete, assignment); @@ -6428,8 +6430,8 @@ void Executor::executeMakeSymbolic(ExecutionState &state, if (!obj) { if (ZeroSeedExtension) { - si.assignment.bindings[array] = - SparseStorage(mo->size, 0); + si.assignment.bindings.replace( + {array, SparseStorage(mo->size, 0)}); } else if (!AllowSeedExtension) { terminateStateOnUserError(state, "ran out of inputs during seeding"); @@ -6449,14 +6451,18 @@ void Executor::executeMakeSymbolic(ExecutionState &state, terminateStateOnUserError(state, msg.str()); break; } else { - SparseStorage &values = - si.assignment.bindings[array]; + SparseStorage values; + if (si.assignment.bindings.find(array) != + si.assignment.bindings.end()) { + values = si.assignment.bindings.at(array); + } values.resize(std::min(mo->size, obj->numBytes)); values.store(0, obj->bytes, obj->bytes + std::min(obj->numBytes, mo->size)); if (ZeroSeedExtension) { values.resize(mo->size); } + si.assignment.bindings.replace({array, values}); } } } @@ -7077,7 +7083,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, KTest &res) { o->pointers = nullptr; } - Assignment model = Assignment(objects, values, true); + Assignment model = Assignment(objects, values); for (auto binding : state.constraints.cs().concretization().bindings) { model.bindings.insert(binding); } diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp index 143baae61e..bea2a646a8 100644 --- a/lib/Core/SeedInfo.cpp +++ b/lib/Core/SeedInfo.cpp @@ -107,7 +107,9 @@ void SeedInfo::patchSeed(const ExecutionState &state, ref condition, solver->getValue(required, read, value, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void)success; - it2->second.store(i, value->getZExtValue(8)); + auto s = it2->second; + s.store(i, value->getZExtValue(8)); + assignment.bindings.replace({it2->first, s}); required.addConstraint( EqExpr::create( read, ConstantExpr::alloc(it2->second.load(i), Expr::Int8)), @@ -151,7 +153,9 @@ void SeedInfo::patchSeed(const ExecutionState &state, ref condition, solver->getValue(required, read, value, state.queryMetaData); assert(success && "FIXME: Unhandled solver failure"); (void)success; - it->second.store(i, value->getZExtValue(8)); + auto s = it->second; + s.store(i, value->getZExtValue(8)); + assignment.bindings.replace({it->first, s}); required.addConstraint( EqExpr::create(read, ConstantExpr::alloc(it->second.load(i), Expr::Int8)), diff --git a/lib/Core/SeedInfo.h b/lib/Core/SeedInfo.h index a513665fdb..ee84133bc3 100644 --- a/lib/Core/SeedInfo.h +++ b/lib/Core/SeedInfo.h @@ -32,8 +32,7 @@ class SeedInfo { std::set used; public: - explicit SeedInfo(KTest *_input) - : assignment(true), input(_input), inputPosition(0) {} + explicit SeedInfo(KTest *_input) : input(_input), inputPosition(0) {} KTestObject *getNextInput(const MemoryObject *mo, bool byName); diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp index dde0f1a23d..4df43ae869 100644 --- a/lib/Solver/AssignmentValidatingSolver.cpp +++ b/lib/Solver/AssignmentValidatingSolver.cpp @@ -65,9 +65,8 @@ void AssignmentValidatingSolver::validateAssigment( std::vector> &values) { // Use `_allowFreeValues` so that if we are missing an assignment // we can't compute a constant and flag this as a problem. - Assignment assignment(objects, values, /*_allowFreeValues=*/true); + Assignment assignment(objects, values); // Check computed assignment satisfies query - assert(!query.containsSymcretes()); for (const auto &constraint : query.constraints.cs()) { ref constraintEvaluated = assignment.evaluate(constraint); ConstantExpr *CE = dyn_cast(constraintEvaluated); @@ -143,7 +142,6 @@ bool AssignmentValidatingSolver::check(const Query &query, } ExprHashSet expressions; - assert(!query.containsSymcretes()); expressions.insert(query.constraints.cs().begin(), query.constraints.cs().end()); expressions.insert(query.expr); @@ -170,10 +168,10 @@ void AssignmentValidatingSolver::dumpAssignmentQuery( const Query &query, const Assignment &assignment) { // Create a Query that is augmented with constraints that // enforce the given assignment. - auto constraints = assignment.createConstraintsFromAssignment(); + auto constraints = + ConstraintSet(assignment.createConstraintsFromAssignment(), {}, {}); // Add Constraints from `query` - assert(!query.containsSymcretes()); for (const auto &constraint : query.constraints.cs()) constraints.addConstraint(constraint, {}); diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index de43695d5e..dbd9dbf39a 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -53,7 +53,6 @@ class CachingSolver : public SolverImpl { unsigned operator()(const CacheEntry &ce) const { unsigned result = ce.query->hash(); - assert(ce.constraints.symcretes().empty()); for (auto const &constraint : ce.constraints.cs()) { result ^= constraint->hash(); } diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index da3303359d..2e26971040 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -127,12 +127,23 @@ struct isInvalidResponse { }; struct isValidOrSatisfyingResponse { - KeyType &key; - - isValidOrSatisfyingResponse(KeyType &_key) : key(_key) {} + KeyType booleanKey; + KeyType nonBooleanKey; + isValidOrSatisfyingResponse(KeyType &_key) { + for (auto i : _key) { + if (i->getWidth() == Expr::Bool) { + booleanKey.insert(i); + } else { + nonBooleanKey.insert(i); + } + } + } bool operator()(ref a) const { - return isa(a) || cast(a)->satisfies(key); + return isa(a) || + (isa(a) && + cast(a)->satisfies(booleanKey) && + cast(a)->satisfiesNonBoolean(nonBooleanKey)); } }; @@ -215,8 +226,10 @@ bool CexCachingSolver::searchForResponse(KeyType &key, /// an unsatisfiable query). \return True if a cached result was found. bool CexCachingSolver::lookupResponse(const Query &query, KeyType &key, ref &result) { - assert(!query.containsSymcretes()); key = KeyType(query.constraints.cs().begin(), query.constraints.cs().end()); + for (ref s : query.constraints.symcretes()) { + key.insert(s->symcretized); + } ref neg = Expr::createIsZero(query.expr); if (ConstantExpr *CE = dyn_cast(neg)) { if (CE->isFalse()) { @@ -240,8 +253,9 @@ bool CexCachingSolver::lookupResponse(const Query &query, KeyType &key, bool CexCachingSolver::getResponse(const Query &query, ref &result) { KeyType key; - if (lookupResponse(query, key, result)) + if (lookupResponse(query, key, result)) { return true; + } if (!solver->impl->check(query, result)) { return false; @@ -264,14 +278,15 @@ bool CexCachingSolver::getResponse(const Query &query, } ValidityCore resultCore; - if (CexCacheValidityCores && result->tryGetValidityCore(resultCore)) { + if (CexCacheValidityCores && isa(result)) { + result->tryGetValidityCore(resultCore); KeyType resultCoreConstarints(resultCore.constraints.begin(), resultCore.constraints.end()); ref neg = Expr::createIsZero(query.expr); resultCoreConstarints.insert(neg); cache.insert(resultCoreConstarints, result); - cache.insert(key, result); - } else { + } + if (isa(result) || isa(result)) { cache.insert(key, result); } @@ -290,7 +305,7 @@ bool CexCachingSolver::computeValidity(const Query &query, return false; assert(isa(a) && "computeValidity() must have assignment"); - ref q = cast(a)->evaluate(query.expr); + ref q = cast(a)->evaluate(query.expr, false); if (!isa(q) && solver->impl->computeValue(query, q)) return false; @@ -301,13 +316,23 @@ bool CexCachingSolver::computeValidity(const Query &query, if (cast(q)->isTrue()) { if (!getResponse(query, a)) return false; - result = - isa(a) ? PValidity::MustBeTrue : PValidity::TrueOrFalse; + if (isa(a)) { + result = PValidity::MustBeTrue; + } else if (isa(a)) { + result = PValidity::TrueOrFalse; + } else { + result = PValidity::MayBeTrue; + } } else { if (!getResponse(query.negateExpr(), a)) return false; - result = - isa(a) ? PValidity::MustBeFalse : PValidity::TrueOrFalse; + if (isa(a)) { + result = PValidity::MustBeFalse; + } else if (isa(a)) { + result = PValidity::TrueOrFalse; + } else { + result = PValidity::MayBeFalse; + } } return true; @@ -334,7 +359,7 @@ bool CexCachingSolver::computeTruth(const Query &query, bool &isValid) { if (!getResponse(query, a)) return false; - isValid = isa(a); + isValid = !isa(a); return true; } @@ -346,7 +371,7 @@ bool CexCachingSolver::computeValue(const Query &query, ref &result) { if (!getResponse(query.withFalse(), a)) return false; assert(isa(a) && "computeValue() must have assignment"); - result = cast(a)->evaluate(query.expr); + result = cast(a)->evaluate(query.expr, false); if (!isa(result) && solver->impl->computeValue(query, result)) return false; @@ -365,7 +390,7 @@ bool CexCachingSolver::computeInitialValues( return false; hasSolution = isa(a); - if (isa(a)) + if (!hasSolution) return true; // FIXME: We should use smarter assignment for result so we don't diff --git a/lib/Solver/ConstructSolverChain.cpp b/lib/Solver/ConstructSolverChain.cpp index a8eb1e2fe7..f8c9c8d522 100644 --- a/lib/Solver/ConstructSolverChain.cpp +++ b/lib/Solver/ConstructSolverChain.cpp @@ -73,6 +73,15 @@ std::unique_ptr constructSolverChain( if (UseConcretizingSolver) solver = createConcretizingSolver(std::move(solver), addressGenerator); + if (UseCexCache && UseConcretizingSolver) + solver = createCexCachingSolver(std::move(solver)); + + if (UseBranchCache && UseConcretizingSolver) + solver = createCachingSolver(std::move(solver)); + + if (UseIndependentSolver && UseConcretizingSolver) + solver = createIndependentSolver(std::move(solver)); + if (DebugValidateSolver) solver = createValidatingSolver(std::move(solver), rawCoreSolver, false); diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 3ba7904ac4..3276b3d1be 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -1088,7 +1088,6 @@ FastCexSolver::~FastCexSolver() {} /// \return - True if the propogation was able to prove validity or invalidity. static bool propagateValues(const Query &query, CexData &cd, bool checkExpr, bool &isValid) { - assert(!query.containsSymcretes()); for (const auto &constraint : query.constraints.cs()) { cd.propagatePossibleValue(constraint, 1); cd.propagateExactValue(constraint, 1); diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index e35ca0daaa..0bbd631805 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -193,11 +193,11 @@ bool QueryLoggingSolver::computeInitialValues( new InvalidResponse(allObjects, allValues); success = invalidResponse->tryGetInitialValuesFor(objects, values); assert(success); - Assignment allSolutionAssignment(allObjects, allValues, true); + Assignment allSolutionAssignment(allObjects, allValues); std::vector>::iterator values_it = values.begin(); - Assignment solutionAssignment(objects, values, true); + Assignment solutionAssignment(objects, values); for (std::vector::const_iterator i = objects.begin(), e = objects.end(); i != e; ++i, ++values_it) { @@ -241,13 +241,12 @@ bool QueryLoggingSolver::check(const Query &query, logBuffer << queryCommentSign << " Solvable: " << (hasSolution ? "true" : "false") << "\n"; if (hasSolution) { - std::map> initialValues; + Assignment::bindings_ty initialValues; result->tryGetInitialValues(initialValues); - Assignment solutionAssignment(initialValues, true); + Assignment solutionAssignment(initialValues); - for (std::map>::const_iterator - i = initialValues.begin(), - e = initialValues.end(); + for (Assignment::bindings_ty::iterator i = initialValues.begin(), + e = initialValues.end(); i != e; ++i) { const Array *array = i->first; const SparseStorage &data = i->second; @@ -271,7 +270,7 @@ bool QueryLoggingSolver::check(const Query &query, result->tryGetValidityCore(validityCore); logBuffer << queryCommentSign << " ValidityCore:\n"; - printQuery(Query(ConstraintSet(validityCore.constraints, {}, {true}), + printQuery(Query(ConstraintSet(validityCore.constraints, {}, {}), validityCore.expr)); } } @@ -300,7 +299,7 @@ bool QueryLoggingSolver::computeValidityCore(const Query &query, if (isValid) { logBuffer << queryCommentSign << " ValidityCore:\n"; - printQuery(Query(ConstraintSet(validityCore.constraints, {}, {true}), + printQuery(Query(ConstraintSet(validityCore.constraints, {}, {}), validityCore.expr)); } diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index ec30aa9b19..d45e071d61 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -335,5 +335,5 @@ void Query::dump() const { } void ValidityCore::dump() const { - Query(ConstraintSet(constraints, {}, {true}), expr).dump(); + Query(ConstraintSet(constraints, {}, {}), expr).dump(); } diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp index ddae26f2e3..65069e32bb 100644 --- a/lib/Solver/ValidatingSolver.cpp +++ b/lib/Solver/ValidatingSolver.cpp @@ -95,7 +95,6 @@ bool ValidatingSolver::computeInitialValues( const Query &query, const std::vector &objects, std::vector> &values, bool &hasSolution) { bool answer; - assert(!query.containsSymcretes()); if (!solver->impl->computeInitialValues(query, objects, values, hasSolution)) return false; @@ -104,7 +103,7 @@ bool ValidatingSolver::computeInitialValues( // Assert the bindings as constraints, and verify that the // conjunction of the actual constraints is satisfiable. ConstraintSet bindings; - Assignment solutionAssignment(objects, values, true); + Assignment solutionAssignment(objects, values); for (unsigned i = 0; i != values.size(); ++i) { const Array *array = objects[i]; @@ -159,7 +158,7 @@ bool ValidatingSolver::check(const Query &query, ref &result) { // conjunction of the actual constraints is satisfiable. ConstraintSet bindings; - std::map> initialValues; + Assignment::bindings_ty initialValues; cast(result)->tryGetInitialValues(initialValues); Assignment solutionAssignment(initialValues); for (auto &arrayValues : initialValues) { diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 3a92ae7fe1..755f47ee92 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -217,7 +217,6 @@ char *Z3SolverImpl::getConstraintLog(const Query &query) { break; } ConstantArrayFinder constant_arrays_in_query; - assert(!query.containsSymcretes()); for (auto const &constraint : query.constraints.cs()) { assumptions.push_back(temp_builder->construct(constraint)); constant_arrays_in_query.visit(constraint); @@ -309,7 +308,6 @@ bool Z3SolverImpl::computeInitialValues( bool Z3SolverImpl::check(const Query &query, ref &result) { ExprHashSet expressions; - assert(!query.containsSymcretes()); expressions.insert(query.constraints.cs().begin(), query.constraints.cs().end()); expressions.insert(query.expr); @@ -347,8 +345,6 @@ bool Z3SolverImpl::internalRunSolver( std::vector> *values, ValidityCore *validityCore, bool &hasSolution) { - assert(!query.containsSymcretes()); - if (ProduceUnsatCore && validityCore) { enableUnsatCore(); } else { diff --git a/test/Expr/Evaluate.kquery b/test/Expr/Evaluate.kquery index 6738c872eb..e6b0d1e1a4 100644 --- a/test/Expr/Evaluate.kquery +++ b/test/Expr/Evaluate.kquery @@ -1,4 +1,4 @@ -# RUN: %kleaver -evaluate %s > %t.log +# RUN: %kleaver -evaluate --use-concretizing-solver=false %s > %t.log arr01 : (array (w64 4) (makeSymbolic arr0 0)) arr12 : (array (w64 8) (makeSymbolic arr1 0)) diff --git a/test/Feature/DanglingConcreteReadExpr.c b/test/Feature/DanglingConcreteReadExpr.c index 4f4dd6cc23..d41d19e1c5 100644 --- a/test/Feature/DanglingConcreteReadExpr.c +++ b/test/Feature/DanglingConcreteReadExpr.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --optimize=false --output-dir=%t.klee-out %t1.bc +// RUN: %klee --optimize=false --use-cex-cache=false --output-dir=%t.klee-out %t1.bc // RUN: grep "total queries = 2" %t.klee-out/info #include diff --git a/test/Solver/CexCacheValidityCoresCheck.c b/test/Solver/CexCacheValidityCoresCheck.c index 26ba133d63..0e48f6f24f 100644 --- a/test/Solver/CexCacheValidityCoresCheck.c +++ b/test/Solver/CexCacheValidityCoresCheck.c @@ -30,6 +30,6 @@ int main(int argc, char **argv) { } } // CHECK-CACHE-ON: QCexCacheHits,SolverQueries -// CHECK-CACHE-ON: 1461,202 +// CHECK-CACHE-ON: 1460,202 // CHECK-CACHE-OFF: QCexCacheHits,SolverQueries -// CHECK-CACHE-OFF: 1011,652 +// CHECK-CACHE-OFF: 1010,652 diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 441e7ffacf..a56ab4c7fb 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -228,9 +228,8 @@ static bool EvaluateInputAST(const char *Filename, const llvm::MemoryBuffer *MB, for (auto i : QC->Constraints) { constraints.insert(i); } - if (S->mustBeTrue( - Query(ConstraintSet(constraints, {}, {true}), QC->Query), - result)) { + if (S->mustBeTrue(Query(ConstraintSet(constraints, {}, {}), QC->Query), + result)) { llvm::outs() << (result ? "VALID" : "INVALID"); } else { llvm::outs() << "FAIL (reason: " @@ -251,7 +250,7 @@ static bool EvaluateInputAST(const char *Filename, const llvm::MemoryBuffer *MB, constraints.insert(i); } if (S->getValue( - Query(ConstraintSet(constraints, {}, {true}), QC->Values[0]), + Query(ConstraintSet(constraints, {}, {}), QC->Values[0]), result)) { llvm::outs() << "INVALID\n"; llvm::outs() << "\tExpr 0:\t" << result; @@ -270,7 +269,7 @@ static bool EvaluateInputAST(const char *Filename, const llvm::MemoryBuffer *MB, } if (S->getInitialValues( - Query(ConstraintSet(constraints, {}, {true}), QC->Query), + Query(ConstraintSet(constraints, {}, {}), QC->Query), QC->Objects, result)) { llvm::outs() << "INVALID\n"; Assignment solutionAssugnment(QC->Objects, result); @@ -383,7 +382,7 @@ static bool printInputAsSMTLIBv2(const char *Filename, constraints.insert(i); } - ConstraintSet constraintM(constraints, {}, {true}); + ConstraintSet constraintM(constraints, {}, {}); Query query(constraintM, QC->Query); printer.setQuery(query); diff --git a/unittests/Assignment/AssignmentTest.cpp b/unittests/Assignment/AssignmentTest.cpp index f7906ef73b..410a4ce357 100644 --- a/unittests/Assignment/AssignmentTest.cpp +++ b/unittests/Assignment/AssignmentTest.cpp @@ -27,7 +27,7 @@ TEST(AssignmentTest, FoldNotOptimized) { values.push_back(value); // We want to simplify to a constant so allow free values so // if the assignment is incomplete we don't get back a constant. - Assignment assignment(objects, values, /*_allowFreeValues=*/true); + Assignment assignment(objects, values); // Now make an expression that reads from the array at position // zero. diff --git a/unittests/Expr/ArrayExprTest.cpp b/unittests/Expr/ArrayExprTest.cpp index 866e6d3fd7..68b6948612 100644 --- a/unittests/Expr/ArrayExprTest.cpp +++ b/unittests/Expr/ArrayExprTest.cpp @@ -65,8 +65,7 @@ TEST(ArrayExprTest, HashCollisions) { SparseStorage value({6, 0, 0, 0}); std::vector> values = {value}; std::vector assigmentArrays = {symArray}; - auto a = std::make_unique(assigmentArrays, values, - /*_allowFreeValues=*/true); + auto a = std::make_unique(assigmentArrays, values); EXPECT_NE(a->evaluate(updatedRead), a->evaluate(firstRead)); EXPECT_EQ(a->evaluate(updatedRead), getConstant(42, Expr::Int8));