Rework CexCacheSolver and add cache to validity cores

UnitTestBot · Mar 8, 2023 · 08103b3 · 08103b3
1 parent 0e17d13
commit 08103b3
Show file tree

Hide file tree

Showing 5 changed files with 236 additions and 213 deletions.
diff --git a/include/klee/Solver/Solver.h b/include/klee/Solver/Solver.h
@@ -138,8 +138,7 @@ namespace klee {
       return false;
     }
 
-    virtual bool tryGetInitialValues(
-        std::map<const Array *, SparseStorage<unsigned char>> &values) const {
+    virtual bool tryGetInitialValues(Assignment::bindings_ty &values) const {
       return false;
     }
 
@@ -151,9 +150,15 @@ namespace klee {
 
     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 {
@@ -183,40 +188,42 @@ namespace klee {
       const ValidResponse &vb = static_cast<const ValidResponse &>(b);
       return result == vb.result;
     }
+
+    bool lessThen(const SolverResponse &b) const {
+      if (b.getResponseKind() != ResponseKind::Valid)
+        return true;
+      const ValidResponse &vb = static_cast<const ValidResponse &>(b);
+      return std::set<ref<Expr>>(result.constraints.begin(),
+                                 result.constraints.end()) <
+             std::set<ref<Expr>>(vb.result.constraints.begin(),
+                                 vb.result.constraints.end());
+    }
+
+    void dump() {}
   };
 
   class InvalidResponse : public SolverResponse {
   private:
-    std::map<const Array *, SparseStorage<unsigned char>> result;
+    Assignment result;
 
   public:
     InvalidResponse(const std::vector<const Array *> &objects,
-                    const std::vector<SparseStorage<unsigned char>> &values) {
-      std::vector<SparseStorage<unsigned char>>::const_iterator values_it =
-          values.begin();
-
-      for (std::vector<const Array *>::const_iterator i = objects.begin(),
-                                                      e = objects.end();
-           i != e; ++i, ++values_it) {
-        result[*i] = *values_it;
-      }
-    }
+                    std::vector<SparseStorage<unsigned char>> &values)
+        : result(Assignment(objects, values)) {}
 
-    InvalidResponse(const std::map<const Array *, SparseStorage<unsigned char>>
-                        &initialValues)
+    InvalidResponse(Assignment::bindings_ty &initialValues)
         : result(initialValues) {}
 
     bool tryGetInitialValuesFor(
         const std::vector<const Array *> &objects,
         std::vector<SparseStorage<unsigned char>> &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<ConstantExpr> constantSize =
-              dyn_cast<ConstantExpr>(resultAssignment.evaluate(object->size));
+              dyn_cast<ConstantExpr>(result.evaluate(object->size));
           assert(constantSize);
           values.push_back(
               SparseStorage<unsigned char>(constantSize->getZExtValue(), 0));
@@ -225,22 +232,21 @@ namespace klee {
       return true;
     }
 
-    bool tryGetInitialValues(
-        std::map<const Array *, SparseStorage<unsigned char>> &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<const Array *> objects) const {
       std::vector<SparseStorage<unsigned char>> values;
-      assert(tryGetInitialValuesFor(objects, values));
+      tryGetInitialValuesFor(objects, values);
       return Assignment(objects, values, true);
     }
 
     Assignment initialValues() const {
-      std::map<const Array *, SparseStorage<unsigned char>> values;
-      assert(tryGetInitialValues(values));
+      Assignment::bindings_ty values;
+      tryGetInitialValues(values);
       return Assignment(values, true);
     }
 
@@ -255,8 +261,25 @@ namespace klee {
       if (b.getResponseKind() != ResponseKind::Invalid)
         return false;
       const InvalidResponse &ib = static_cast<const InvalidResponse &>(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<const InvalidResponse &>(b);
+      return result.bindings < ib.result.bindings;
+    }
+
+    bool satisfies(std::set<ref<Expr>> &key) {
+      return result.satisfies(key.begin(), key.end());
+    }
+
+    ref<Expr> evaluate(ref<Expr> &e) { return result.evaluate(e); }
+
+    void dump() { result.dump(); }
+
+    ref<Expr> evaluate(ref<Expr> e) { return (result.evaluate(e)); }
   };
 
   class Solver {

diff --git a/include/klee/Solver/SolverImpl.h b/include/klee/Solver/SolverImpl.h
@@ -10,8 +10,9 @@
 #ifndef KLEE_SOLVERIMPL_H
 #define KLEE_SOLVERIMPL_H
 
-#include "klee/System/Time.h"
 #include "Solver.h"
+#include "klee/Expr/ExprUtil.h"
+#include "klee/System/Time.h"
 
 #include <vector>