diff --git a/include/klee/Solver/Solver.h b/include/klee/Solver/Solver.h index f77aed8253..4ee955b6a4 100644 --- a/include/klee/Solver/Solver.h +++ b/include/klee/Solver/Solver.h @@ -131,8 +131,7 @@ class SolverResponse { return false; } - virtual bool tryGetInitialValues( - std::map> &values) const { + virtual bool tryGetInitialValues(Assignment::bindings_ty &values) const { return false; } @@ -142,9 +141,15 @@ class SolverResponse { virtual bool equals(const SolverResponse &b) const = 0; + virtual bool lessThen(const SolverResponse &b) const = 0; + bool operator==(const SolverResponse &b) const { return equals(b); } bool operator!=(const SolverResponse &b) const { return !equals(b); } + + bool operator<(const SolverResponse &b) const { return lessThen(b); } + + virtual void dump() = 0; }; class ValidResponse : public SolverResponse { @@ -174,40 +179,42 @@ class ValidResponse : public SolverResponse { const ValidResponse &vb = static_cast(b); return result == vb.result; } + + bool lessThen(const SolverResponse &b) const { + if (b.getResponseKind() != ResponseKind::Valid) + return true; + const ValidResponse &vb = static_cast(b); + return std::set>(result.constraints.begin(), + result.constraints.end()) < + std::set>(vb.result.constraints.begin(), + vb.result.constraints.end()); + } + + void dump() { result.dump(); } }; class InvalidResponse : public SolverResponse { private: - std::map> result; + Assignment result; public: InvalidResponse(const std::vector &objects, - const std::vector> &values) { - std::vector>::const_iterator values_it = - values.begin(); - - for (std::vector::const_iterator i = objects.begin(), - e = objects.end(); - i != e; ++i, ++values_it) { - result[*i] = *values_it; - } - } + std::vector> &values) + : result(Assignment(objects, values)) {} - InvalidResponse(const std::map> - &initialValues) + InvalidResponse(Assignment::bindings_ty &initialValues) : result(initialValues) {} bool tryGetInitialValuesFor( const std::vector &objects, std::vector> &values) const { - Assignment resultAssignment(result); values.reserve(objects.size()); for (auto object : objects) { - if (result.count(object)) { - values.push_back(result.at(object)); + if (result.bindings.count(object)) { + values.push_back(result.bindings.at(object)); } else { ref constantSize = - dyn_cast(resultAssignment.evaluate(object->size)); + dyn_cast(result.evaluate(object->size)); assert(constantSize); values.push_back( SparseStorage(constantSize->getZExtValue(), 0)); @@ -216,21 +223,20 @@ class InvalidResponse : public SolverResponse { return true; } - bool tryGetInitialValues( - std::map> &values) const { - values.insert(result.begin(), result.end()); + bool tryGetInitialValues(Assignment::bindings_ty &values) const { + values.insert(result.bindings.begin(), result.bindings.end()); return true; } Assignment initialValuesFor(const std::vector objects) const { std::vector> values; - assert(tryGetInitialValuesFor(objects, values)); + tryGetInitialValuesFor(objects, values); return Assignment(objects, values, true); } Assignment initialValues() const { - std::map> values; - assert(tryGetInitialValues(values)); + Assignment::bindings_ty values; + tryGetInitialValues(values); return Assignment(values, true); } @@ -245,8 +251,25 @@ class InvalidResponse : public SolverResponse { if (b.getResponseKind() != ResponseKind::Invalid) return false; const InvalidResponse &ib = static_cast(b); - return result == ib.result; + return result.bindings == ib.result.bindings; } + + bool lessThen(const SolverResponse &b) const { + if (b.getResponseKind() != ResponseKind::Invalid) + return false; + const InvalidResponse &ib = static_cast(b); + return result.bindings < ib.result.bindings; + } + + bool satisfies(std::set> &key) { + return result.satisfies(key.begin(), key.end()); + } + + ref evaluate(ref &e) { return result.evaluate(e); } + + void dump() { result.dump(); } + + ref evaluate(ref e) { return (result.evaluate(e)); } }; class Solver { diff --git a/include/klee/Solver/SolverImpl.h b/include/klee/Solver/SolverImpl.h index ca3292b56c..a579cc6fca 100644 --- a/include/klee/Solver/SolverImpl.h +++ b/include/klee/Solver/SolverImpl.h @@ -11,6 +11,7 @@ #define KLEE_SOLVERIMPL_H #include "Solver.h" +#include "klee/Expr/ExprUtil.h" #include "klee/System/Time.h" #include diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index c10d730b7f..fdff8783cf 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -10,7 +10,6 @@ #include "klee/Solver/Solver.h" #include "klee/ADT/MapOfSets.h" -#include "klee/Expr/Assignment.h" #include "klee/Expr/Constraints.h" #include "klee/Expr/Expr.h" #include "klee/Expr/ExprUtil.h" @@ -50,38 +49,44 @@ cl::opt CexCacheExperimental( cl::desc("Optimization for validity queries (default=false)"), cl::cat(SolvingCat)); +cl::opt CexCacheValidityCores( + "cex-cache-validity-cores", cl::init(false), + cl::desc("Cache assignment and it's validity cores (default=false)"), + cl::cat(SolvingCat)); + } // namespace /// typedef std::set> KeyType; -struct AssignmentLessThan { - bool operator()(const Assignment *a, const Assignment *b) const { - return a->bindings < b->bindings; +struct ResponseComparator { + bool operator()(const ref a, + const ref b) const { + return *a < *b; } }; class CexCachingSolver : public SolverImpl { - typedef std::set assignmentsTable_ty; + typedef std::set, ResponseComparator> responseTable_ty; Solver *solver; - MapOfSets, Assignment *> cache; + MapOfSets, ref> cache; // memo table - assignmentsTable_ty assignmentsTable; + responseTable_ty responseTable; - bool searchForAssignment(KeyType &key, Assignment *&result); + bool searchForResponse(KeyType &key, ref &result); - bool lookupAssignment(const Query &query, KeyType &key, Assignment *&result); + bool lookupResponse(const Query &query, KeyType &key, + ref &result); - bool lookupAssignment(const Query &query, Assignment *&result) { + bool lookupResponse(const Query &query, ref &result) { KeyType key; - return lookupAssignment(query, key, result); + return lookupResponse(query, key, result); } - bool getAssignment(const Query &query, Assignment *&result, - ValidityCore *validityCore = nullptr); + bool getResponse(const Query &query, ref &result); public: CexCachingSolver(Solver *_solver) : solver(_solver) {} @@ -104,48 +109,51 @@ class CexCachingSolver : public SolverImpl { /// -struct NullAssignment { - bool operator()(Assignment *a) const { return !a; } +struct isValidResponse { + bool operator()(ref a) const { return isa(a); } }; -struct NonNullAssignment { - bool operator()(Assignment *a) const { return a != 0; } +struct isInvalidResponse { + bool operator()(ref a) const { + return isa(a); + } }; -struct NullOrSatisfyingAssignment { +struct isValidOrSatisfyingResponse { KeyType &key; - NullOrSatisfyingAssignment(KeyType &_key) : key(_key) {} + isValidOrSatisfyingResponse(KeyType &_key) : key(_key) {} - bool operator()(Assignment *a) const { - return !a || a->satisfies(key.begin(), key.end()); + bool operator()(ref a) const { + return isa(a) || cast(a)->satisfies(key); } }; -/// searchForAssignment - Look for a cached solution for a query. +/// searchForResponse - Look for a cached solution for a query. /// /// \param key - The query to look up. /// \param result [out] - The cached result, if the lookup is successful. This -/// is either a satisfying assignment (for a satisfiable query), or 0 (for an -/// unsatisfiable query). -/// \return - True if a cached result was found. -bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) { - Assignment *const *lookup = cache.lookup(key); +/// is either a satisfying invalid response (for a satisfiable query), or valid +/// response (for an unsatisfiable query). \return - True if a cached result was +/// found. +bool CexCachingSolver::searchForResponse(KeyType &key, + ref &result) { + const ref *lookup = cache.lookup(key); if (lookup) { result = *lookup; return true; } if (CexCacheTryAll) { - // Look for a satisfying assignment for a superset, which is trivially an - // assignment for any subset. - Assignment **lookup = 0; + // Look for a satisfying invalid response for a superset, which is trivially + // a response for any subset. + ref *lookup = 0; if (CexCacheSuperSet) - lookup = cache.findSuperset(key, NonNullAssignment()); + lookup = cache.findSuperset(key, isInvalidResponse()); // Otherwise, look for a subset which is unsatisfiable, see below. if (!lookup) - lookup = cache.findSubset(key, NullAssignment()); + lookup = cache.findSubset(key, isValidResponse()); // If either lookup succeeded, then we have a cached solution. if (lookup) { @@ -153,13 +161,13 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) { return true; } - // Otherwise, iterate through the set of current assignments to see if one - // of them satisfies the query. - for (assignmentsTable_ty::iterator it = assignmentsTable.begin(), - ie = assignmentsTable.end(); + // 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(), + ie = responseTable.end(); it != ie; ++it) { - Assignment *a = *it; - if (a->satisfies(key.begin(), key.end())) { + ref a = *it; + if (isa(a) && cast(a)->satisfies(key)) { result = a; return true; } @@ -167,19 +175,19 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) { } else { // FIXME: Which order? one is sure to be better. - // Look for a satisfying assignment for a superset, which is trivially an - // assignment for any subset. - Assignment **lookup = 0; + // Look for a satisfying invalid response for a superset, which is trivially + // a response for any subset. + ref *lookup = 0; if (CexCacheSuperSet) - lookup = cache.findSuperset(key, NonNullAssignment()); + lookup = cache.findSuperset(key, isInvalidResponse()); // Otherwise, look for a subset which is unsatisfiable -- if the subset is // unsatisfiable then no additional constraints can produce a valid - // assignment. While searching subsets, we also explicitly the solutions for - // satisfiable subsets to see if they solve the current query and return - // them if so. This is cheap and frequently succeeds. + // solver response. While searching subsets, we also explicitly the + // solutions for satisfiable subsets to see if they solve the current query + // and return them if so. This is cheap and frequently succeeds. if (!lookup) - lookup = cache.findSubset(key, NullOrSatisfyingAssignment(key)); + lookup = cache.findSubset(key, isValidOrSatisfyingResponse(key)); // If either lookup succeeded, then we have a cached solution. if (lookup) { @@ -191,21 +199,20 @@ bool CexCachingSolver::searchForAssignment(KeyType &key, Assignment *&result) { return false; } -/// lookupAssignment - Lookup a cached result for the given \arg query. +/// lookupResponse - Lookup a cached result for the given \arg query. /// /// \param query - The query to lookup. /// \param key [out] - On return, the key constructed for the query. /// \param result [out] - The cached result, if the lookup is successful. This -/// is either a satisfying assignment (for a satisfiable query), or 0 (for an -/// unsatisfiable query). -/// \return True if a cached result was found. -bool CexCachingSolver::lookupAssignment(const Query &query, KeyType &key, - Assignment *&result) { +/// is either a InvalidResponse (for a satisfiable query), or ValidResponse (for +/// an unsatisfiable query). \return True if a cached result was found. +bool CexCachingSolver::lookupResponse(const Query &query, KeyType &key, + ref &result) { key = KeyType(query.constraints.begin(), query.constraints.end()); ref neg = Expr::createIsZero(query.expr); if (ConstantExpr *CE = dyn_cast(neg)) { if (CE->isFalse()) { - result = (Assignment *)0; + result = new ValidResponse(ValidityCore()); ++stats::queryCexCacheHits; return true; } @@ -213,7 +220,7 @@ bool CexCachingSolver::lookupAssignment(const Query &query, KeyType &key, key.insert(neg); } - bool found = searchForAssignment(key, result); + bool found = searchForResponse(key, result); if (found) ++stats::queryCexCacheHits; else @@ -222,60 +229,43 @@ bool CexCachingSolver::lookupAssignment(const Query &query, KeyType &key, return found; } -bool CexCachingSolver::getAssignment(const Query &query, Assignment *&result, - ValidityCore *validityCore) { +bool CexCachingSolver::getResponse(const Query &query, + ref &result) { KeyType key; - if (lookupAssignment(query, key, result) && (result || !validityCore)) + if (lookupResponse(query, key, result)) return true; - std::vector objects; - findSymbolicObjects(key.begin(), key.end(), objects); - - std::vector> values; - ref queryResult; - bool hasSolution; - if (validityCore) { - if (!solver->impl->check(query, queryResult)) - return false; - hasSolution = isa(queryResult); - } else { - if (!solver->impl->computeInitialValues(query, objects, values, - hasSolution)) - return false; + if (!solver->impl->check(query, result)) { + return false; } - Assignment *binding; - if (hasSolution) { - if (validityCore) { - Assignment::bindings_ty bindings; - queryResult->tryGetInitialValues(bindings); - binding = new Assignment(bindings); - } else { - binding = new Assignment(objects, values); - } - - // Memoize the result. - std::pair res = - assignmentsTable.insert(binding); + if (isa(result)) { + // Memorize the result. + std::pair res = + responseTable.insert(result); if (!res.second) { - delete binding; - binding = *res.first; + result = *res.first; } if (DebugCexCacheCheckBinding) - if (!binding->satisfies(key.begin(), key.end())) { + if (!cast(result)->satisfies(key)) { query.dump(); - binding->dump(); + result->dump(); klee_error("Generated assignment doesn't match query"); } - } else { - if (validityCore) - queryResult->tryGetValidityCore(*validityCore); - binding = (Assignment *)0; } - result = binding; - cache.insert(key, binding); + ValidityCore resultCore; + if (CexCacheValidityCores && 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 { + cache.insert(key, result); + } return true; } @@ -285,20 +275,17 @@ bool CexCachingSolver::getAssignment(const Query &query, Assignment *&result, CexCachingSolver::~CexCachingSolver() { cache.clear(); delete solver; - for (assignmentsTable_ty::iterator it = assignmentsTable.begin(), - ie = assignmentsTable.end(); - it != ie; ++it) - delete *it; } bool CexCachingSolver::computeValidity(const Query &query, Solver::Validity &result) { TimerStatIncrementer t(stats::cexCacheTime); - Assignment *a; - if (!getAssignment(query.withFalse(), a)) + ref a; + if (!getResponse(query.withFalse(), a)) return false; - assert(a && "computeValidity() must have assignment"); - ref q = a->evaluate(query.expr); + assert(isa(a) && "computeValidity() must have assignment"); + + ref q = cast(a)->evaluate(query.expr); if (!isa(q) && solver->impl->computeValue(query, q)) return false; @@ -307,13 +294,13 @@ bool CexCachingSolver::computeValidity(const Query &query, "assignment evaluation did not result in constant"); if (cast(q)->isTrue()) { - if (!getAssignment(query, a)) + if (!getResponse(query, a)) return false; - result = !a ? Solver::True : Solver::Unknown; + result = isa(a) ? Solver::True : Solver::Unknown; } else { - if (!getAssignment(query.negateExpr(), a)) + if (!getResponse(query.negateExpr(), a)) return false; - result = !a ? Solver::False : Solver::Unknown; + result = isa(a) ? Solver::False : Solver::Unknown; } return true; @@ -331,16 +318,16 @@ bool CexCachingSolver::computeTruth(const Query &query, bool &isValid) { // really seem to be worth the overhead. if (CexCacheExperimental) { - Assignment *a; - if (lookupAssignment(query.negateExpr(), a) && !a) + ref a; + if (lookupResponse(query.negateExpr(), a) && isa(a)) return false; } - Assignment *a; - if (!getAssignment(query, a)) + ref a; + if (!getResponse(query, a)) return false; - isValid = !a; + isValid = isa(a); return true; } @@ -348,11 +335,11 @@ bool CexCachingSolver::computeTruth(const Query &query, bool &isValid) { bool CexCachingSolver::computeValue(const Query &query, ref &result) { TimerStatIncrementer t(stats::cexCacheTime); - Assignment *a; - if (!getAssignment(query.withFalse(), a)) + ref a; + if (!getResponse(query.withFalse(), a)) return false; - assert(a && "computeValue() must have assignment"); - result = a->evaluate(query.expr); + assert(isa(a) && "computeValue() must have assignment"); + result = cast(a)->evaluate(query.expr); if (!isa(result) && solver->impl->computeValue(query, result)) return false; @@ -366,12 +353,12 @@ bool CexCachingSolver::computeInitialValues( const Query &query, const std::vector &objects, std::vector> &values, bool &hasSolution) { TimerStatIncrementer t(stats::cexCacheTime); - Assignment *a; - if (!getAssignment(query, a)) + ref a; + if (!getResponse(query, a)) return false; - hasSolution = !!a; + hasSolution = isa(a); - if (!a) + if (isa(a)) return true; // FIXME: We should use smarter assignment for result so we don't @@ -379,10 +366,13 @@ bool CexCachingSolver::computeInitialValues( values = std::vector>(objects.size()); for (unsigned i = 0; i < objects.size(); ++i) { const Array *os = objects[i]; - Assignment::bindings_ty::iterator it = a->bindings.find(os); + Assignment::bindings_ty aBindings; + a->tryGetInitialValues(aBindings); + Assignment::bindings_ty::iterator it = aBindings.find(os); - if (it == a->bindings.end()) { - ref arrayConstantSize = a->evaluate(os->size); + if (it == aBindings.end()) { + ref arrayConstantSize = + cast(a)->evaluate(os->size); assert(arrayConstantSize && "Array of symbolic size had not receive value for size!"); values[i] = @@ -397,37 +387,7 @@ bool CexCachingSolver::computeInitialValues( bool CexCachingSolver::check(const Query &query, ref &result) { TimerStatIncrementer t(stats::cexCacheTime); - Assignment *a; - ValidityCore validityCore; - if (!getAssignment(query, a, &validityCore)) - return false; - - if (!a) { - result = new ValidResponse(validityCore); - return true; - } - - ExprHashSet expressions; - expressions.insert(query.constraints.begin(), query.constraints.end()); - expressions.insert(query.expr); - - std::vector objects; - findObjects(expressions.begin(), expressions.end(), objects); - for (unsigned i = 0; i < objects.size(); ++i) { - const Array *os = objects[i]; - Assignment::bindings_ty::iterator it = a->bindings.find(os); - ref arrayConstantSize = a->evaluate(os->size); - assert(arrayConstantSize && - "Array of symbolic size had not receive value for size!"); - if (it == a->bindings.end()) { - a->bindings[os] = - SparseStorage(arrayConstantSize->getZExtValue(), 0); - } - } - - result = new InvalidResponse(a->bindings); - - return true; + return getResponse(query, result); } bool CexCachingSolver::computeValidityCore(const Query &query, @@ -435,12 +395,13 @@ bool CexCachingSolver::computeValidityCore(const Query &query, bool &isValid) { TimerStatIncrementer t(stats::cexCacheTime); - Assignment *a; - if (!getAssignment(query, a, &validityCore)) + ref a; + if (!getResponse(query, a)) return false; - isValid = !a; - + isValid = isa(a); + if (isValid) + cast(a)->tryGetValidityCore(validityCore); return true; } diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp index e0f6545f27..3dd886ed89 100644 --- a/lib/Solver/IncompleteSolver.cpp +++ b/lib/Solver/IncompleteSolver.cpp @@ -134,6 +134,23 @@ bool StagedSolverImpl::computeInitialValues( } bool StagedSolverImpl::check(const Query &query, ref &result) { + ExprHashSet expressions; + expressions.insert(query.constraints.begin(), query.constraints.end()); + expressions.insert(query.expr); + + std::vector objects; + findSymbolicObjects(expressions.begin(), expressions.end(), objects); + std::vector> values; + + bool hasSolution; + + bool primaryResult = + primary->computeInitialValues(query, objects, values, hasSolution); + if (primaryResult && hasSolution) { + result = new InvalidResponse(objects, values); + return true; + } + return secondary->impl->check(query, result); } diff --git a/lib/Solver/SolverImpl.cpp b/lib/Solver/SolverImpl.cpp index b07075cc8c..f726d8f765 100644 --- a/lib/Solver/SolverImpl.cpp +++ b/lib/Solver/SolverImpl.cpp @@ -41,17 +41,43 @@ bool SolverImpl::computeValidity(const Query &query, } bool SolverImpl::check(const Query &query, ref &result) { - if (ProduceUnsatCore) - klee_error("check is not implemented"); - return false; + ExprHashSet expressions; + expressions.insert(query.constraints.begin(), query.constraints.end()); + expressions.insert(query.expr); + + std::vector objects; + findSymbolicObjects(expressions.begin(), expressions.end(), objects); + std::vector> values; + + bool hasSolution; + + if (!computeInitialValues(query, objects, values, hasSolution)) { + return false; + } + + if (hasSolution) { + result = new InvalidResponse(objects, values); + } else { + result = new ValidResponse(ValidityCore( + ExprHashSet(query.constraints.begin(), query.constraints.end()), + query.expr)); + } + return true; } bool SolverImpl::computeValidityCore(const Query &query, ValidityCore &validityCore, bool &isValid) { - if (ProduceUnsatCore) - klee_error("computeTruthCore is not implemented"); - return false; + if (!computeTruth(query, isValid)) { + return false; + } + + if (isValid) { + validityCore = ValidityCore( + ExprHashSet(query.constraints.begin(), query.constraints.end()), + query.expr); + } + return true; } bool SolverImpl::computeMinimalUnsignedValue(const Query &query, diff --git a/test/Solver/CexCacheValidityCoresCheck.c b/test/Solver/CexCacheValidityCoresCheck.c new file mode 100644 index 0000000000..a134d6aaef --- /dev/null +++ b/test/Solver/CexCacheValidityCoresCheck.c @@ -0,0 +1,35 @@ +// REQUIRES: z3 +// RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc +// RUN: rm -rf %t1.klee-out +// RUN: rm -rf %t2.klee-out +// RUN: %klee --output-dir=%t1.klee-out -cex-cache-validity-cores=false -solver-backend=z3 %t1.bc +// RUN: %klee --output-dir=%t2.klee-out -cex-cache-validity-cores=true -solver-backend=z3 %t1.bc +// RUN: %klee-stats --print-columns 'QCexCHits' --table-format=csv %t1.klee-out > %t1.stats +// RUN: %klee-stats --print-columns 'QCexCHits' --table-format=csv %t2.klee-out > %t2.stats +// RUN: FileCheck -check-prefix=CHECK-CACHE-OFF -input-file=%t1.stats %s +// RUN: FileCheck -check-prefix=CHECK-CACHE-ON -input-file=%t2.stats %s +#include "klee/klee.h" + +int main(int argc, char **argv) { + int a, b; + klee_make_symbolic(&a, sizeof(a), "a"); + klee_make_symbolic(&b, sizeof(b), "b"); + + for (int i = 0; i < 10; i++) { + for (int j = 0; j < 10; j++) { + if (b == a + i && b == a + j) + break; + } + } + + for (int i = 0; i < 10; i++) { + for (int j = 0; j < 10; j++) { + if (b > i && b > j && b == a + i && b == a + j) + break; + } + } +} +// CHECK-CACHE-ON: QCexCHits +// CHECK-CACHE-ON: 324 +// CHECK-CACHE-OFF: QCexCHits +// CHECK-CACHE-OFF: 273