From 604828f30104981ca822b95d6e210eb14a23cc75 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Sat, 23 Sep 2023 00:17:25 +0400 Subject: [PATCH 1/5] [fix] Improve `IndependentConstraintSetUnion` --- include/klee/ADT/DisjointSetUnion.h | 29 +++- include/klee/ADT/Either.h | 142 ++++++++++++++++++ .../klee/Expr/IndependentConstraintSetUnion.h | 7 +- include/klee/Expr/IndependentSet.h | 15 +- lib/Core/ExecutionState.h | 2 +- lib/Expr/Constraints.cpp | 12 +- lib/Expr/IndependentConstraintSetUnion.cpp | 74 ++++----- lib/Expr/IndependentSet.cpp | 109 ++++++++------ 8 files changed, 289 insertions(+), 101 deletions(-) create mode 100644 include/klee/ADT/Either.h diff --git a/include/klee/ADT/DisjointSetUnion.h b/include/klee/ADT/DisjointSetUnion.h index 77a41353c2..b479ca0765 100644 --- a/include/klee/ADT/DisjointSetUnion.h +++ b/include/klee/ADT/DisjointSetUnion.h @@ -1,14 +1,27 @@ #ifndef KLEE_DISJOINEDSETUNION_H #define KLEE_DISJOINEDSETUNION_H + +#include "klee/ADT/Either.h" #include "klee/ADT/PersistentMap.h" #include "klee/ADT/PersistentSet.h" #include "klee/ADT/Ref.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/Symcrete.h" + +#include "klee/Support/CompilerWarning.h" +DISABLE_WARNING_PUSH +DISABLE_WARNING_DEPRECATED_DECLARATIONS +#include "llvm/Support/raw_ostream.h" +DISABLE_WARNING_POP + +#include #include #include #include #include namespace klee { +using ExprEitherSymcrete = either; template > @@ -55,7 +68,7 @@ class DisjointSetUnion { roots.remove(b); disjointSets.replace( {a, SetType::merge(disjointSets.at(a), disjointSets.at(b))}); - disjointSets.replace({b, nullptr}); + disjointSets.remove(b); } bool areJoined(const ValueType &i, const ValueType &j) const { @@ -109,6 +122,8 @@ class DisjointSetUnion { } void add(const DisjointSetUnion &b) { + internalStorage_ty oldRoots = roots; + internalStorage_ty newRoots = b.roots; for (auto it : b.parent) { parent.insert(it); } @@ -124,6 +139,15 @@ class DisjointSetUnion { for (auto it : b.disjointSets) { disjointSets.insert(it); } + for (ValueType nv : newRoots) { + for (ValueType ov : oldRoots) { + if (!areJoined(ov, nv) && + SetType::intersects(disjointSets.at(find(ov)), + disjointSets.at(find(nv)))) { + merge(ov, nv); + } + } + } } DisjointSetUnion() {} @@ -140,4 +164,5 @@ class DisjointSetUnion { disjointSets_ty ds() const { return disjointSets; } }; } // namespace klee -#endif + +#endif /* KLEE_DISJOINEDSETUNION_H */ diff --git a/include/klee/ADT/Either.h b/include/klee/ADT/Either.h new file mode 100644 index 0000000000..cc01bf761e --- /dev/null +++ b/include/klee/ADT/Either.h @@ -0,0 +1,142 @@ +//===-- Either.h ------------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_EITHER_H +#define KLEE_EITHER_H + +#include "klee/ADT/Ref.h" + +#include "klee/Support/Casting.h" + +#include + +namespace llvm { +class raw_ostream; +} // namespace llvm + +namespace klee { + +template class either_left; +template class either_right; + +template class either { +protected: + friend class ref>; + friend class ref>; + + /// @brief Required by klee::ref-managed objects + class ReferenceCounter _refCount; + +public: + using left = either_left; + using right = either_right; + + enum class EitherKind { Left, Right }; + + virtual ~either() {} + virtual EitherKind getKind() const = 0; + + static bool classof(const either *) { return true; } + // virtual unsigned hash() = 0; + virtual int compare(const either &b) = 0; + virtual bool equals(const either &b) = 0; +}; + +template class either_left : public either { +protected: + friend class ref>; + friend class ref>; + +private: + ref value_; + +public: + either_left(ref leftValue) : value_(leftValue){}; + + ref value() const { return value_; } + operator ref const() { return value_; } + + virtual typename either::EitherKind getKind() const override { + return either::EitherKind::Left; + } + + static bool classof(const either *S) { + return S->getKind() == either::EitherKind::Left; + } + static bool classof(const either_left *) { return true; } + + // virtual unsigned hash() override { return value_->hash(); }; + virtual int compare(const either &b) override { + if (b.getKind() != getKind()) { + return b.getKind() < getKind() ? -1 : 1; + } + const either_left &el = static_cast &>(b); + if (el.value() != value()) { + return el.value() < value() ? -1 : 1; + } + return 0; + } + + virtual bool equals(const either &b) override { + if (b.getKind() != getKind()) { + return false; + } + const either_left &el = static_cast &>(b); + return el.value() == value(); + } +}; + +template class either_right : public either { +protected: + friend class ref>; + friend class ref>; + +private: + ref value_; + +public: + either_right(ref rightValue) : value_(rightValue){}; + + ref value() const { return value_; } + operator ref const() { return value_; } + + virtual typename either::EitherKind getKind() const override { + return either::EitherKind::Right; + } + + static bool classof(const either *S) { + return S->getKind() == either::EitherKind::Right; + } + static bool classof(const either_right *) { return true; } + + // virtual unsigned hash() override { return value_->hash(); }; + virtual int compare(const either &b) override { + if (b.getKind() != getKind()) { + return b.getKind() < getKind() ? -1 : 1; + } + const either_right &el = + static_cast &>(b); + if (el.value() != value()) { + return el.value() < value() ? -1 : 1; + } + return 0; + } + + virtual bool equals(const either &b) override { + if (b.getKind() != getKind()) { + return false; + } + const either_right &el = + static_cast &>(b); + return el.value() == value(); + } +}; +} // end namespace klee + +#endif /* KLEE_EITHER_H */ diff --git a/include/klee/Expr/IndependentConstraintSetUnion.h b/include/klee/Expr/IndependentConstraintSetUnion.h index 3591cd5eff..4ec9e11c5a 100644 --- a/include/klee/Expr/IndependentConstraintSetUnion.h +++ b/include/klee/Expr/IndependentConstraintSetUnion.h @@ -1,12 +1,15 @@ #ifndef KLEE_INDEPENDENTCONSTRAINTSETUNION_H #define KLEE_INDEPENDENTCONSTRAINTSETUNION_H +#include "klee/ADT/Either.h" + #include "klee/Expr/Assignment.h" #include "klee/Expr/IndependentSet.h" namespace klee { class IndependentConstraintSetUnion - : public DisjointSetUnion, IndependentConstraintSet> { + : public DisjointSetUnion, + IndependentConstraintSet> { public: Assignment concretization; @@ -43,4 +46,4 @@ class IndependentConstraintSetUnion }; } // namespace klee -#endif +#endif /* KLEE_INDEPENDENTCONSTRAINTSETUNION_H */ diff --git a/include/klee/Expr/IndependentSet.h b/include/klee/Expr/IndependentSet.h index ef29498f5a..a0878ea6c2 100644 --- a/include/klee/Expr/IndependentSet.h +++ b/include/klee/Expr/IndependentSet.h @@ -2,6 +2,7 @@ #define KLEE_INDEPENDENTSET_H #include "klee/ADT/DisjointSetUnion.h" +#include "klee/ADT/Either.h" #include "klee/ADT/PersistentMap.h" #include "klee/ADT/PersistentSet.h" #include "klee/Expr/Assignment.h" @@ -21,6 +22,7 @@ DISABLE_WARNING_POP #include namespace klee { +using ExprEitherSymcrete = either; template class DenseSet { typedef std::set set_ty; @@ -84,7 +86,11 @@ inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, class IndependentConstraintSet { private: - using InnerSetUnion = DisjointSetUnion, IndependentConstraintSet>; + using InnerSetUnion = + DisjointSetUnion, IndependentConstraintSet>; + + void initIndependentConstraintSet(ref e); + void initIndependentConstraintSet(ref s); public: // All containers need to become persistent to make fast copy and faster @@ -117,11 +123,8 @@ class IndependentConstraintSet { Assignment &assign) const; IndependentConstraintSet(); - IndependentConstraintSet(ref e); - IndependentConstraintSet(ref s); - IndependentConstraintSet(const ref &ics); - - IndependentConstraintSet &operator=(const IndependentConstraintSet &ies); + explicit IndependentConstraintSet(ref v); + IndependentConstraintSet(const IndependentConstraintSet &ics); void print(llvm::raw_ostream &os) const; diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index a13b963de7..be63b654bc 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -228,7 +228,7 @@ struct Symbolic { struct MemorySubobject { ref address; unsigned size; - MemorySubobject(ref address, unsigned size) + explicit MemorySubobject(ref address, unsigned size) : address(address), size(size) {} MemorySubobject &operator=(const MemorySubobject &other) = default; }; diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index a1612e9c74..11efeed2b1 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -207,12 +207,12 @@ 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.replace({i.first, i.second}); } _independentElements.updateConcretization(delta); + _independentElements.addExpr(e); } IDType Symcrete::idCounter = 0; @@ -252,8 +252,10 @@ ConstraintSet ConstraintSet::getConcretizedVersion() const { ConstraintSet cs; cs._independentElements = _independentElements.getConcretizedVersion(); - for (ref e : cs._independentElements.is()) { - cs._constraints.insert(e); + for (auto &e : cs._independentElements.is()) { + if (isa(e)) { + cs._constraints.insert(cast(e)->value()); + } } return cs; } @@ -263,8 +265,8 @@ ConstraintSet ConstraintSet::getConcretizedVersion( ConstraintSet cs; cs._independentElements = _independentElements.getConcretizedVersion(newConcretization); - for (ref e : cs._independentElements.is()) { - cs._constraints.insert(e); + for (auto &e : cs._independentElements.is()) { + cs._constraints.insert(cast(e)->value()); } return cs; } diff --git a/lib/Expr/IndependentConstraintSetUnion.cpp b/lib/Expr/IndependentConstraintSetUnion.cpp index 3ec73081cb..01358e2623 100644 --- a/lib/Expr/IndependentConstraintSetUnion.cpp +++ b/lib/Expr/IndependentConstraintSetUnion.cpp @@ -8,7 +8,7 @@ IndependentConstraintSetUnion::IndependentConstraintSetUnion( const constraints_ty &is, const SymcreteOrderedSet &os, const Assignment &c) { for (ref e : is) { - addValue(e); + addExpr(e); } for (ref s : os) { addSymcrete(s); @@ -18,25 +18,25 @@ IndependentConstraintSetUnion::IndependentConstraintSetUnion( IndependentConstraintSetUnion::IndependentConstraintSetUnion( ref ics) { - for (ref e : ics->exprs) { - rank.replace({e, 0}); - internalStorage.insert(e); - disjointSets.replace({e, nullptr}); + auto exprs = ics->exprs; + for (ref e : exprs) { + auto v = ref(new ExprEitherSymcrete::left(e)); + rank.replace({v, 0}); + internalStorage.insert(v); } for (ref s : ics->symcretes) { - ref e = s->symcretized; - rank.replace({e, 0}); - internalStorage.insert(e); - disjointSets.replace({e, nullptr}); + auto v = ref(new ExprEitherSymcrete::right(s)); + rank.replace({v, 0}); + internalStorage.insert(v); } if (internalStorage.size() == 0) { return; } - ref first = *(internalStorage.begin()); - for (ref e : internalStorage) { + auto &first = *(internalStorage.begin()); + for (auto &e : internalStorage) { parent.replace({e, first}); } rank.replace({first, 1}); @@ -53,26 +53,26 @@ void IndependentConstraintSetUnion::addIndependentConstraintSetUnion( void IndependentConstraintSetUnion::updateConcretization( const Assignment &delta) { - for (ref e : roots) { + for (auto &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) { + for (auto &it : delta.bindings) { concretization.bindings.replace({it.first, it.second}); } } void IndependentConstraintSetUnion::removeConcretization( const Assignment &remove) { - for (ref e : roots) { + for (auto &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) { + for (auto &it : remove.bindings) { concretization.bindings.remove(it.first); } } @@ -95,8 +95,9 @@ void IndependentConstraintSetUnion::reEvaluateConcretization( void IndependentConstraintSetUnion::getAllIndependentConstraintSets( ref e, std::vector> &result) const { - ref compare = new IndependentConstraintSet(e); - for (ref r : roots) { + ref compare = + new IndependentConstraintSet(new ExprEitherSymcrete::left(e)); + for (auto &r : roots) { ref ics = disjointSets.at(r); if (!IndependentConstraintSet::intersects(ics, compare)) { result.push_back(ics); @@ -107,8 +108,9 @@ void IndependentConstraintSetUnion::getAllIndependentConstraintSets( void IndependentConstraintSetUnion::getAllDependentConstraintSets( ref e, std::vector> &result) const { - ref compare = new IndependentConstraintSet(e); - for (ref r : roots) { + ref compare = + new IndependentConstraintSet(new ExprEitherSymcrete::left(e)); + for (auto &r : roots) { ref ics = disjointSets.at(r); if (IndependentConstraintSet::intersects(ics, compare)) { result.push_back(ics); @@ -117,39 +119,25 @@ void IndependentConstraintSetUnion::getAllDependentConstraintSets( } void IndependentConstraintSetUnion::addExpr(ref e) { - addValue(e); - disjointSets.replace({find(e), disjointSets.at(find(e))->addExpr(e)}); + addValue(new ExprEitherSymcrete::left(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)}); + addValue(new ExprEitherSymcrete::right(s)); } IndependentConstraintSetUnion IndependentConstraintSetUnion::getConcretizedVersion() const { IndependentConstraintSetUnion icsu; - for (ref i : roots) { + for (auto &i : roots) { ref root = disjointSets.at(i); - icsu.add(root->concretizedSets); + if (root->concretization.bindings.empty()) { + for (ref expr : root->exprs) { + icsu.addValue(new ExprEitherSymcrete::left(expr)); + } + } else { + icsu.add(root->concretizedSets); + } icsu.concretization.addIndependentAssignment(root->concretization); } icsu.concretizedExprs = concretizedExprs; diff --git a/lib/Expr/IndependentSet.cpp b/lib/Expr/IndependentSet.cpp index ed602599b2..3acca539c9 100644 --- a/lib/Expr/IndependentSet.cpp +++ b/lib/Expr/IndependentSet.cpp @@ -16,18 +16,10 @@ #include namespace klee { - -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); + ref ics = new IndependentConstraintSet(*this); if (delta.bindings.size() == 0) { return ics; } @@ -37,12 +29,21 @@ IndependentConstraintSet::updateConcretization( InnerSetUnion DSU; for (ref i : exprs) { ref e = ics->concretization.evaluate(i); + if (auto ce = dyn_cast(e)) { + assert(ce->isTrue() && "Attempt to add invalid constraint"); + continue; + } concretizedExprs[i] = e; - DSU.addValue(e); + DSU.addValue(new ExprEitherSymcrete::left(e)); } for (ref s : symcretes) { - DSU.addValue(EqExpr::create(ics->concretization.evaluate(s->symcretized), - s->symcretized)); + ref e = EqExpr::create(ics->concretization.evaluate(s->symcretized), + s->symcretized); + if (auto ce = dyn_cast(e)) { + assert(ce->isTrue() && "Attempt to add invalid constraint"); + continue; + } + DSU.addValue(new ExprEitherSymcrete::left(e)); } ics->concretizedSets = DSU; return ics; @@ -51,7 +52,7 @@ IndependentConstraintSet::updateConcretization( ref IndependentConstraintSet::removeConcretization( const Assignment &delta, ExprHashMap> &concretizedExprs) const { - ref ics = new IndependentConstraintSet(this); + ref ics = new IndependentConstraintSet(*this); if (delta.bindings.size() == 0) { return ics; } @@ -61,12 +62,21 @@ IndependentConstraintSet::removeConcretization( InnerSetUnion DSU; for (ref i : exprs) { ref e = ics->concretization.evaluate(i); + if (auto ce = dyn_cast(e)) { + assert(ce->isTrue() && "Attempt to add invalid constraint"); + continue; + } concretizedExprs[i] = e; - DSU.addValue(e); + DSU.addValue(new ExprEitherSymcrete::left(e)); } for (ref s : symcretes) { - DSU.addValue(EqExpr::create(ics->concretization.evaluate(s->symcretized), - s->symcretized)); + ref e = EqExpr::create(ics->concretization.evaluate(s->symcretized), + s->symcretized); + if (auto ce = dyn_cast(e)) { + assert(ce->isTrue() && "Attempt to add invalid constraint"); + continue; + } + DSU.addValue(new ExprEitherSymcrete::left(e)); } ics->concretizedSets = DSU; @@ -97,7 +107,15 @@ void IndependentConstraintSet::addValuesToAssignment( IndependentConstraintSet::IndependentConstraintSet() {} -IndependentConstraintSet::IndependentConstraintSet(ref e) { +IndependentConstraintSet::IndependentConstraintSet(ref v) { + if (isa(v)) { + initIndependentConstraintSet(cast(v)->value()); + } else { + initIndependentConstraintSet(cast(v)->value()); + } +} + +void IndependentConstraintSet::initIndependentConstraintSet(ref e) { exprs.insert(e); // Track all reads in the program. Determines whether reads are // concrete or symbolic. If they are symbolic, "collapses" array @@ -134,13 +152,9 @@ IndependentConstraintSet::IndependentConstraintSet(ref e) { } } -IndependentConstraintSet::IndependentConstraintSet(ref s) { +void IndependentConstraintSet::initIndependentConstraintSet(ref s) { symcretes.insert(s); - for (Symcrete &dependentSymcrete : s->dependentSymcretes()) { - symcretes.insert(ref(&dependentSymcrete)); - } - // Track all reads in the program. Determines whether reads are // concrete or symbolic. If they are symbolic, "collapses" array // by adding it to wholeObjects. Otherwise, creates a mapping of @@ -193,22 +207,10 @@ IndependentConstraintSet::IndependentConstraintSet(ref s) { } 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; -} + const IndependentConstraintSet &ics) + : elements(ics.elements), wholeObjects(ics.wholeObjects), exprs(ics.exprs), + symcretes(ics.symcretes), concretization(ics.concretization), + concretizedSets(ics.concretizedSets) {} void IndependentConstraintSet::print(llvm::raw_ostream &os) const { os << "{"; @@ -279,8 +281,8 @@ bool IndependentConstraintSet::intersects( ref IndependentConstraintSet::merge(ref A, ref B) { - ref a = new IndependentConstraintSet(A); - ref b = new IndependentConstraintSet(B); + ref a = new IndependentConstraintSet(*A); + ref b = new IndependentConstraintSet(*B); if (a->wholeObjects.size() + a->elements.size() < b->wholeObjects.size() + b->elements.size()) { @@ -323,7 +325,30 @@ IndependentConstraintSet::merge(ref A, } b->addValuesToAssignment(b->concretization.keys(), b->concretization.values(), a->concretization); - a->concretizedSets.add(b->concretizedSets); + + if (!a->concretization.bindings.empty()) { + InnerSetUnion DSU; + for (ref i : a->exprs) { + ref e = a->concretization.evaluate(i); + if (auto ce = dyn_cast(e)) { + assert(ce->isTrue() && "Attempt to add invalid constraint"); + continue; + } + DSU.addValue(new ExprEitherSymcrete::left(e)); + } + for (ref s : a->symcretes) { + ref e = EqExpr::create(a->concretization.evaluate(s->symcretized), + s->symcretized); + if (auto ce = dyn_cast(e)) { + assert(ce->isTrue() && "Attempt to add invalid constraint"); + continue; + } + DSU.addValue(new ExprEitherSymcrete::left(e)); + } + + a->concretizedSets = DSU; + } + return a; } @@ -355,7 +380,7 @@ void calculateArraysInFactors( } std::vector result; ref queryExprSet = - new IndependentConstraintSet(queryExpr); + new IndependentConstraintSet(new ExprEitherSymcrete::left(queryExpr)); queryExprSet->calculateArrayReferences(result); returnSet.insert(result.begin(), result.end()); returnVector.insert(returnVector.begin(), returnSet.begin(), returnSet.end()); From 16b5bcbe493cb27faba8ef19ab727246513b8777 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Mon, 25 Sep 2023 16:21:57 +0400 Subject: [PATCH 2/5] [feat] Add optimization in case all constraints are dependent --- lib/Solver/IndependentSolver.cpp | 21 +++++++++++++++------ 1 file changed, 15 insertions(+), 6 deletions(-) diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 50e518fb59..67c0309335 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -152,6 +152,14 @@ bool IndependentSolver::computeInitialValues( Assignment retMap; std::vector> dependentFactors; query.getAllDependentConstraintsSets(dependentFactors); + std::vector> independentFactors; + query.getAllIndependentConstraintsSets(independentFactors); + + if (independentFactors.size() == 0 && dependentFactors.size() == 1) { + return solver->impl->computeInitialValues(query, objects, values, + hasSolution); + } + ConstraintSet dependentConstriants(dependentFactors); std::vector dependentFactorsObjects; @@ -174,9 +182,6 @@ bool IndependentSolver::computeInitialValues( } } - std::vector> independentFactors; - query.getAllIndependentConstraintsSets(independentFactors); - // Used to rearrange all of the answers into the correct order for (ref it : independentFactors) { std::vector arraysInFactor; @@ -242,6 +247,13 @@ bool IndependentSolver::check(const Query &query, ref &result) { Assignment retMap; std::vector> dependentFactors; query.getAllDependentConstraintsSets(dependentFactors); + std::vector> independentFactors; + query.getAllIndependentConstraintsSets(independentFactors); + + if (independentFactors.size() == 0 && dependentFactors.size() == 1) { + return solver->impl->check(query, result); + } + ConstraintSet dependentConstriants(dependentFactors); std::vector dependentFactorsObjects; @@ -266,9 +278,6 @@ bool IndependentSolver::check(const Query &query, ref &result) { } } - std::vector> independentFactors; - query.getAllIndependentConstraintsSets(independentFactors); - // Used to rearrange all of the answers into the correct order for (ref it : independentFactors) { std::vector arraysInFactor; From 2703a8207eb0cabbc050d07a6975ec00ee5ad555 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Fri, 29 Sep 2023 13:17:40 +0400 Subject: [PATCH 3/5] [fix] Rebuild constraint dsu after constraints simplification --- include/klee/Expr/Constraints.h | 1 + lib/Core/CXXTypeSystem/CXXTypeManager.cpp | 6 ++++-- lib/Expr/Constraints.cpp | 19 ++++++++++++++----- 3 files changed, 19 insertions(+), 7 deletions(-) diff --git a/include/klee/Expr/Constraints.h b/include/klee/Expr/Constraints.h index a87cd0ce3c..d6f47e3d94 100644 --- a/include/klee/Expr/Constraints.h +++ b/include/klee/Expr/Constraints.h @@ -152,6 +152,7 @@ class Simplificator { struct SetResult { constraints_ty simplified; ExprHashMap dependency; + bool wasSimplified; }; public: diff --git a/lib/Core/CXXTypeSystem/CXXTypeManager.cpp b/lib/Core/CXXTypeSystem/CXXTypeManager.cpp index a171e65a9d..1df8091e9c 100644 --- a/lib/Core/CXXTypeSystem/CXXTypeManager.cpp +++ b/lib/Core/CXXTypeSystem/CXXTypeManager.cpp @@ -201,8 +201,10 @@ static ref getComplexPointerRestrictions( restrictions.addConstraint(innerAlignmentRequirement, {}); } - auto simplified = Simplificator::simplify(restrictions.cs()).simplified; - restrictions.changeCS(simplified); + auto simplified = Simplificator::simplify(restrictions.cs()); + if (simplified.wasSimplified) { + restrictions.changeCS(simplified.simplified); + } for (auto restriction : restrictions.cs()) { if (resultCondition.isNull()) { resultCondition = restriction; diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index 11efeed2b1..f14d612379 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -15,6 +15,7 @@ #include "klee/Expr/ExprHashMap.h" #include "klee/Expr/ExprUtil.h" #include "klee/Expr/ExprVisitor.h" +#include "klee/Expr/IndependentSet.h" #include "klee/Expr/Path.h" #include "klee/Expr/Symcrete.h" #include "klee/Module/KModule.h" @@ -289,7 +290,11 @@ void ConstraintSet::print(llvm::raw_ostream &os) const { void ConstraintSet::dump() const { this->print(llvm::errs()); } -void ConstraintSet::changeCS(constraints_ty &cs) { _constraints = cs; } +void ConstraintSet::changeCS(constraints_ty &cs) { + _constraints = cs; + _independentElements = + IndependentConstraintSetUnion(_constraints, _symcretes, _concretization); +} const constraints_ty &ConstraintSet::cs() const { return _constraints; } @@ -355,10 +360,12 @@ ExprHashSet PathConstraints::addConstraint(ref e, const Assignment &delta, if (RewriteEqualities != RewriteEqualitiesPolicy::None) { auto simplified = Simplificator::simplify(constraints.cs(), RewriteEqualities); - constraints.changeCS(simplified.simplified); + if (simplified.wasSimplified) { + constraints.changeCS(simplified.simplified); - _simplificationMap = Simplificator::composeExprDependencies( - _simplificationMap, simplified.dependency); + _simplificationMap = Simplificator::composeExprDependencies( + _simplificationMap, simplified.dependency); + } } return added; @@ -463,6 +470,7 @@ Simplificator::simplify(const constraints_ty &constraints, dependencies.insert({constraint, {constraint}}); } + bool actuallyChanged = false; bool changed = true; while (changed) { changed = false; @@ -495,6 +503,7 @@ Simplificator::simplify(const constraints_ty &constraints, currentDependencies[part].insert(constraint); } if (constraint != simplifiedConstraint || andsSplit.size() > 1) { + actuallyChanged = true; changed = true; } } @@ -508,7 +517,7 @@ Simplificator::simplify(const constraints_ty &constraints, simplified.erase(ConstantExpr::createTrue()); dependencies.erase(ConstantExpr::createTrue()); - return {simplified, dependencies}; + return {simplified, dependencies, actuallyChanged}; } Simplificator::Replacements From fa319a61a2e54ed0edab04865febeb2242cc1448 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Wed, 27 Sep 2023 14:13:44 +0400 Subject: [PATCH 4/5] [fix] Fix MemorySubobject warning --- lib/Core/ExecutionState.h | 1 - 1 file changed, 1 deletion(-) diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index be63b654bc..a40c6a0982 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -230,7 +230,6 @@ struct MemorySubobject { unsigned size; explicit MemorySubobject(ref address, unsigned size) : address(address), size(size) {} - MemorySubobject &operator=(const MemorySubobject &other) = default; }; struct MemorySubobjectHash { From 3c4a8fcacf68e125b1d5820d34048ba7c7ae97c0 Mon Sep 17 00:00:00 2001 From: Aleksandr Misonizhnik Date: Wed, 27 Sep 2023 14:13:25 +0400 Subject: [PATCH 5/5] [fix] Fix `CachingSolver` --- lib/Solver/CachingSolver.cpp | 14 +++----------- 1 file changed, 3 insertions(+), 11 deletions(-) diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index a84b686474..0bf904a60a 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -223,19 +223,11 @@ bool CachingSolver::computeValidity(const Query &query, if (!solver->impl->computeValidity(query, result)) return false; - switch (result) { - case PValidity::MustBeTrue: - cachedResult = PValidity::MustBeTrue; - break; - case PValidity::MustBeFalse: - cachedResult = PValidity::MustBeFalse; - break; - default: - cachedResult = PValidity::TrueOrFalse; - break; - } + cachedResult = result; + assert(cachedResult != PValidity::None); cacheInsert(query, cachedResult); + return true; }