[fix] Solvers performance fixes

Solvers: - Fixed CexCachingSolver so that the core solver (Z3/STP) does not get stupid queries, like `false` or `not false` - Omit complex stuff in IndependentSolver for independent sets of size 1 - Unified code of IndependentSolver Tests: - Changed total queries in `Feature/DanglingConcreteReadExpr.c` test from 2 to 1 as its first query to Z3 was `not false` - Decreased QCexCacheHits in `Solver/CexCacheValidityCoresCheck.c` test by one for the same reason - Activated tests in `test/Solver`
UnitTestBot · Sep 12, 2023 · 878abd7 · 878abd7
1 parent ede8d25
commit 878abd7
Show file tree

Hide file tree

Showing 9 changed files with 42 additions and 41 deletions.
diff --git 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
@@ -220,6 +220,8 @@ class InvalidResponse : public SolverResponse {
   InvalidResponse(Assignment::bindings_ty &initialValues)
       : result(initialValues) {}
 
+  explicit InvalidResponse() : result() {}
+
   bool tryGetInitialValuesFor(
       const std::vector<const Array *> &objects,
       std::vector<SparseStorage<unsigned char>> &values) const {

diff --git 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<SolverResponse> a;
-  if (!getResponse(query.withFalse(), a))
+  ref<Expr> q;
+  if (!computeValue(query, q))
     return false;
-  assert(isa<InvalidResponse>(a) && "computeValidity() must have assignment");
-
-  ref<Expr> q = cast<InvalidResponse>(a)->evaluate(query.expr);
-
-  if (!isa<ConstantExpr>(q) && solver->impl->computeValue(query, q))
-    return false;
-
-  assert(isa<ConstantExpr>(q) &&
-         "assignment evaluation did not result in constant");
 
   if (cast<ConstantExpr>(q)->isTrue()) {
     if (!getResponse(query, a))
@@ -343,8 +335,12 @@ bool CexCachingSolver::computeValue(const Query &query, ref<Expr> &result) {
   TimerStatIncrementer t(stats::cexCacheTime);
 
   ref<SolverResponse> 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<InvalidResponse>(a) && "computeValue() must have assignment");
   result = cast<InvalidResponse>(a)->evaluate(query.expr);
 

diff --git 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<const Array *> &objects,
     std::vector<SparseStorage<unsigned char>> &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<IndependentElementSet> *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<const Array *, SparseStorage<unsigned char>> 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<Expr> factorExpr = ConstantExpr::alloc(0, Expr::Bool);
     std::vector<SparseStorage<unsigned char>> 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<SolverResponse> &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<Expr> 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<SolverResponse> &result) {
 
     ref<SolverResponse> tempResult;
     std::vector<SparseStorage<unsigned char>> 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<ValidResponse>(tempResult)) {

diff --git 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 <assert.h>
 
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
+// CHECK: KLEE: done: completed paths = 9
+// CHECK: KLEE: done: partially completed paths = 5