diff --git a/include/klee/Expr/Assignment.h b/include/klee/Expr/Assignment.h index f72bb581b7..bb86172a60 100644 --- a/include/klee/Expr/Assignment.h +++ b/include/klee/Expr/Assignment.h @@ -25,6 +25,7 @@ class ConstraintSet; typedef std::set, SymcreteLess> SymcreteOrderedSet; using symcretes_ty = SymcreteOrderedSet; +typedef std::function)> ExprPredicate; class Assignment { public: @@ -57,11 +58,14 @@ class Assignment { ref evaluate(ref e, bool allowFreeValues = true) const; constraints_ty createConstraintsFromAssignment() const; + template + bool satisfies(InputIterator begin, InputIterator end, + ExprPredicate predicate, bool allowFreeValues = true); template bool satisfies(InputIterator begin, InputIterator end, bool allowFreeValues = true); template - bool satisfiesNonBoolean(InputIterator begin, InputIterator end, + bool satisfiesOrConstant(InputIterator begin, InputIterator end, bool allowFreeValues = true); void dump() const; @@ -115,28 +119,43 @@ inline ref Assignment::evaluate(ref e, bool allowFreeValues) const { return v.visit(e); } +struct isTrueBoolean { + bool operator()(ref e) const { + return e->getWidth() == Expr::Bool && e->isTrue(); + } +}; + +struct isTrueBooleanOrConstantNotBoolean { + bool operator()(ref e) const { + return (e->getWidth() == Expr::Bool && e->isTrue()) || + ((isa(e) && e->getWidth() != Expr::Bool)); + } +}; + template inline bool Assignment::satisfies(InputIterator begin, InputIterator end, + ExprPredicate predicate, bool allowFreeValues) { AssignmentEvaluator v(*this, allowFreeValues); for (; begin != end; ++begin) { - assert((*begin)->getWidth() == Expr::Bool && "constraints must be boolean"); - if (!v.visit(*begin)->isTrue()) + if (!predicate(v.visit(*begin))) return false; } return true; } template -inline bool Assignment::satisfiesNonBoolean(InputIterator begin, +inline bool Assignment::satisfies(InputIterator begin, InputIterator end, + bool allowFreeValues) { + return satisfies(begin, end, isTrueBoolean(), allowFreeValues); +} + +template +inline bool Assignment::satisfiesOrConstant(InputIterator begin, InputIterator end, bool allowFreeValues) { - AssignmentEvaluator v(*this, allowFreeValues); - for (; begin != end; ++begin) { - if (!isa(v.visit(*begin))) - return false; - } - return true; + return satisfies(begin, end, isTrueBooleanOrConstantNotBoolean(), + allowFreeValues); } } // namespace klee diff --git a/include/klee/Solver/SolverUtil.h b/include/klee/Solver/SolverUtil.h index ffd3849c62..9be7d0f2d2 100644 --- a/include/klee/Solver/SolverUtil.h +++ b/include/klee/Solver/SolverUtil.h @@ -299,26 +299,12 @@ class InvalidResponse : public SolverResponse { } bool satisfies(const std::set> &key, bool allowFreeValues = true) { - std::set> booleanKey; - std::set> nonBooleanKey; - - for (auto i : key) { - if (i->getWidth() == Expr::Bool) { - booleanKey.insert(i); - } else { - nonBooleanKey.insert(i); - } - } - - return result.satisfies(booleanKey.begin(), booleanKey.end(), - allowFreeValues) && - result.satisfiesNonBoolean(nonBooleanKey.begin(), - nonBooleanKey.end(), allowFreeValues); + return result.satisfies(key.begin(), key.end(), allowFreeValues); } - bool satisfiesNonBoolean(const std::set> &key, + bool satisfiesOrConstant(const std::set> &key, bool allowFreeValues = true) { - return result.satisfiesNonBoolean(key.begin(), key.end(), allowFreeValues); + return result.satisfiesOrConstant(key.begin(), key.end(), allowFreeValues); } void dump() { result.dump(); } diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index ddb5861c88..74144a0697 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -169,16 +169,6 @@ bool CexCachingSolver::searchForResponse(KeyType &key, return true; } - KeyType booleanKey; - KeyType nonBooleanKey; - for (auto i : key) { - if (i->getWidth() == Expr::Bool) { - booleanKey.insert(i); - } else { - nonBooleanKey.insert(i); - } - } - // Otherwise, iterate through the set of current solver responses to see if // one of them satisfies the query. for (responseTable_ty::iterator it = responseTable.begin(), @@ -186,8 +176,7 @@ bool CexCachingSolver::searchForResponse(KeyType &key, it != ie; ++it) { ref a = *it; if (isa(a) && - cast(a)->satisfies(booleanKey) && - cast(a)->satisfiesNonBoolean(nonBooleanKey)) { + cast(a)->satisfiesOrConstant(key)) { result = a; return true; } @@ -272,17 +261,7 @@ bool CexCachingSolver::getResponse(const Query &query, } if (DebugCexCacheCheckBinding) { - KeyType booleanKey; - KeyType nonBooleanKey; - for (auto i : key) { - if (i->getWidth() == Expr::Bool) { - booleanKey.insert(i); - } else { - nonBooleanKey.insert(i); - } - } - if (!cast(result)->satisfies(booleanKey) || - !cast(result)->satisfiesNonBoolean(nonBooleanKey)) { + if (!cast(result)->satisfiesOrConstant(key)) { query.dump(); result->dump(); klee_error("Generated assignment doesn't match query");