diff --git a/include/klee/Solver/SolverImpl.h b/include/klee/Solver/SolverImpl.h index bd5937ed11e..3e24a16ed7f 100644 --- a/include/klee/Solver/SolverImpl.h +++ b/include/klee/Solver/SolverImpl.h @@ -22,7 +22,7 @@ class ExecutionState; class Expr; struct Query; -/// SolverImpl - Abstract base clase for solver implementations. +/// SolverImpl - Abstract base class for solver implementations. class SolverImpl { public: SolverImpl() = default; diff --git a/include/klee/Solver/SolverUtil.h b/include/klee/Solver/SolverUtil.h index d61c188cc0b..c1fdb2832c6 100644 --- a/include/klee/Solver/SolverUtil.h +++ b/include/klee/Solver/SolverUtil.h @@ -220,6 +220,8 @@ class InvalidResponse : public SolverResponse { InvalidResponse(Assignment::bindings_ty &initialValues) : result(initialValues) {} + explicit InvalidResponse() : result() {} + bool tryGetInitialValuesFor( const std::vector &objects, std::vector> &values) const { diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index da3303359de..bdbc73a4dbc 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -286,17 +286,9 @@ bool CexCachingSolver::computeValidity(const Query &query, PartialValidity &result) { TimerStatIncrementer t(stats::cexCacheTime); ref a; - if (!getResponse(query.withFalse(), a)) + ref q; + if (!computeValue(query, q)) return false; - assert(isa(a) && "computeValidity() must have assignment"); - - ref q = cast(a)->evaluate(query.expr); - - if (!isa(q) && solver->impl->computeValue(query, q)) - return false; - - assert(isa(q) && - "assignment evaluation did not result in constant"); if (cast(q)->isTrue()) { if (!getResponse(query, a)) @@ -343,8 +335,12 @@ bool CexCachingSolver::computeValue(const Query &query, ref &result) { TimerStatIncrementer t(stats::cexCacheTime); ref a; - if (!getResponse(query.withFalse(), a)) - return false; + if (!query.constraints.cs().empty()) { + if (!getResponse(query.withFalse(), a)) + return false; + } else { + a = new InvalidResponse(); + } assert(isa(a) && "computeValue() must have assignment"); result = cast(a)->evaluate(query.expr); diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 9e0139200a8..b7fe116123c 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -147,14 +147,20 @@ bool assertCreatedPointEvaluatesToTrue( bool IndependentSolver::computeInitialValues( const Query &query, const std::vector &objects, std::vector> &values, bool &hasSolution) { - // 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. - 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); + if (factors->size() == 1) { + delete factors; + return solver->impl->computeInitialValues(query, objects, values, + hasSolution); + } + + // 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. + hasSolution = true; // Used to rearrange all of the answers into the correct order std::map> retMap; @@ -164,16 +170,17 @@ bool IndependentSolver::computeInitialValues( calculateArrayReferences(*it, arraysInFactor); // Going to use this as the "fresh" expression for the Query() invocation // below - assert(it->exprs.size() >= 1 && "No null/empty factors"); + constraints_ty factorConstraints = it->exprs; + assert(factorConstraints.size() >= 1 && "No null/empty factors"); if (arraysInFactor.size() == 0) { continue; } - ConstraintSet tmp(it->exprs, it->symcretes, + ConstraintSet tmp(factorConstraints, it->symcretes, query.constraints.concretization().part(it->symcretes)); + ref factorExpr = ConstantExpr::alloc(0, Expr::Bool); std::vector> tempValues; if (!solver->impl->computeInitialValues( - Query(tmp, ConstantExpr::alloc(0, Expr::Bool)), arraysInFactor, - tempValues, hasSolution)) { + Query(tmp, factorExpr), arraysInFactor, tempValues, hasSolution)) { values.clear(); delete factors; return false; @@ -248,12 +255,13 @@ bool IndependentSolver::check(const Query &query, ref &result) { calculateArrayReferences(*it, arraysInFactor); // Going to use this as the "fresh" expression for the Query() invocation // below - assert(it->exprs.size() >= 1 && "No null/empty factors"); + constraints_ty factorConstraints = it->exprs; + assert(factorConstraints.size() >= 1 && "No null/empty factors"); if (arraysInFactor.size() == 0) { continue; } - - constraints_ty factorConstraints = it->exprs; + ConstraintSet tmp(factorConstraints, it->symcretes, + query.constraints.concretization().part(it->symcretes)); ref factorExpr = ConstantExpr::alloc(0, Expr::Bool); auto factorConstraintsExprIterator = std::find(factorConstraints.begin(), factorConstraints.end(), @@ -265,12 +273,7 @@ bool IndependentSolver::check(const Query &query, ref &result) { ref tempResult; std::vector> tempValues; - if (!solver->impl->check( - Query(ConstraintSet( - factorConstraints, it->symcretes, - query.constraints.concretization().part(it->symcretes)), - factorExpr), - tempResult)) { + if (!solver->impl->check(Query(tmp, factorExpr), tempResult)) { delete factors; return false; } else if (isa(tempResult)) { diff --git a/test/Feature/DanglingConcreteReadExpr.c b/test/Feature/DanglingConcreteReadExpr.c index 4f4dd6cc23d..1f8a5a347aa 100644 --- a/test/Feature/DanglingConcreteReadExpr.c +++ b/test/Feature/DanglingConcreteReadExpr.c @@ -1,7 +1,7 @@ // 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: grep "total queries = 2" %t.klee-out/info +// RUN: grep "total queries = 1" %t.klee-out/info #include @@ -12,7 +12,7 @@ int main() { y = x; - // should be exactly two queries (prove x is/is not 10) + // should be exactly one query (prove x is 10) // eventually should be 0 when we have fast solver if (x == 10) { assert(y == 10); diff --git a/test/Solver/CexCacheValidityCoresCheck.c b/test/Solver/CexCacheValidityCoresCheck.c index 26ba133d635..0e48f6f24fe 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/test/Solver/CrosscheckCoreStpZ3.c b/test/Solver/CrosscheckCoreStpZ3.c index 9847d8a69ba..471f7d40e3e 100644 --- a/test/Solver/CrosscheckCoreStpZ3.c +++ b/test/Solver/CrosscheckCoreStpZ3.c @@ -2,9 +2,9 @@ // REQUIRES: z3 // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --solver-backend=stp --use-forked-solver=false --debug-crosscheck-core-solver=z3 %t1.bc +// RUN: %klee --output-dir=%t.klee-out --solver-backend=stp --use-forked-solver=false --debug-crosscheck-core-solver=z3 %t1.bc 2>&1 | FileCheck %s #include "ExerciseSolver.c.inc" -// CHECK: KLEE: done: completed paths = 15 -// CHECK: KLEE: done: partially completed paths = 0 +// CHECK: KLEE: done: completed paths = 9 +// CHECK: KLEE: done: partially completed paths = 5 diff --git a/test/Solver/DummySolver.c b/test/Solver/DummySolver.c index f6fe3671be2..51c35e936fb 100644 --- a/test/Solver/DummySolver.c +++ b/test/Solver/DummySolver.c @@ -1,6 +1,6 @@ // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --solver-backend=dummy %t1.bc +// RUN: %klee --output-dir=%t.klee-out --solver-backend=dummy %t1.bc 2>&1 | FileCheck %s #include "ExerciseSolver.c.inc" diff --git a/test/Solver/ValidatingSolver.c b/test/Solver/ValidatingSolver.c index 86799a85f21..d492ff92646 100644 --- a/test/Solver/ValidatingSolver.c +++ b/test/Solver/ValidatingSolver.c @@ -1,8 +1,8 @@ // RUN: %clang %s -emit-llvm %O0opt -c -o %t1.bc // RUN: rm -rf %t.klee-out -// RUN: %klee --output-dir=%t.klee-out --debug-validate-solver --debug-assignment-validating-solver %t1.bc +// RUN: %klee --output-dir=%t.klee-out --debug-validate-solver --debug-assignment-validating-solver %t1.bc 2>&1 | FileCheck %s #include "ExerciseSolver.c.inc" -// CHECK: KLEE: done: completed paths = 15 -// CHECK: KLEE: done: partially completed paths = 0 \ No newline at end of file +// CHECK: KLEE: done: completed paths = 9 +// CHECK: KLEE: done: partially completed paths = 5 \ No newline at end of file