From 8a0f1af7500e10dadd97300f242424917d2e9902 Mon Sep 17 00:00:00 2001
From: Martin Nowack <m.nowack@imperial.ac.uk>
Date: Mon, 1 Apr 2019 14:08:43 +0100
Subject: Use constraint sets and separate metadata for timing solver
 invocation

Decouple ExecutionState from TimingSolver

Instead of providing an execution state to the timing solver use a set of
constraints and an additional object for metadata.

Fixes:
* correct accounting of metadata to a specific state
* accounting of all solver invocations (e.g. solver-getRange was not
accounted)
* allows to invoke the solver without a state (avoids costly copying of
states/constraints)
---
 lib/Core/TimingSolver.h | 78 ++++++++++++++++++++++++++-----------------------
 1 file changed, 41 insertions(+), 37 deletions(-)

(limited to 'lib/Core/TimingSolver.h')

diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index 9470bd31..1f179e54 100644
--- a/lib/Core/TimingSolver.h
+++ b/lib/Core/TimingSolver.h
@@ -19,54 +19,58 @@
 #include <vector>
 
 namespace klee {
-  class ExecutionState;
-  class Solver;  
-
-  /// TimingSolver - A simple class which wraps a solver and handles
-  /// tracking the statistics that we care about.
-  class TimingSolver {
-  public:
-    std::unique_ptr<Solver> solver;
-    bool simplifyExprs;
-
-  public:
-    /// TimingSolver - Construct a new timing solver.
-    ///
-    /// \param _simplifyExprs - Whether expressions should be
-    /// simplified (via the constraint manager interface) prior to
-    /// querying.
-    TimingSolver(Solver *_solver, bool _simplifyExprs = true) 
+class ConstraintSet;
+class Solver;
+
+/// TimingSolver - A simple class which wraps a solver and handles
+/// tracking the statistics that we care about.
+class TimingSolver {
+public:
+  std::unique_ptr<Solver> solver;
+  bool simplifyExprs;
+
+public:
+  /// TimingSolver - Construct a new timing solver.
+  ///
+  /// \param _simplifyExprs - Whether expressions should be
+  /// simplified (via the constraint manager interface) prior to
+  /// querying.
+  TimingSolver(Solver *_solver, bool _simplifyExprs = true)
       : solver(_solver), simplifyExprs(_simplifyExprs) {}
 
-    void setTimeout(time::Span t) {
-      solver->setCoreSolverTimeout(t);
-    }
-    
-    char *getConstraintLog(const Query& query) {
-      return solver->getConstraintLog(query);
-    }
+  void setTimeout(time::Span t) { solver->setCoreSolverTimeout(t); }
 
-    bool evaluate(const ExecutionState&, ref<Expr>, Solver::Validity &result);
+  char *getConstraintLog(const Query &query) {
+    return solver->getConstraintLog(query);
+  }
 
-    bool mustBeTrue(const ExecutionState&, ref<Expr>, bool &result);
+  bool evaluate(const ConstraintSet &, ref<Expr>, Solver::Validity &result,
+                SolverQueryMetaData &metaData);
 
-    bool mustBeFalse(const ExecutionState&, ref<Expr>, bool &result);
+  bool mustBeTrue(const ConstraintSet &, ref<Expr>, bool &result,
+                  SolverQueryMetaData &metaData);
 
-    bool mayBeTrue(const ExecutionState&, ref<Expr>, bool &result);
+  bool mustBeFalse(const ConstraintSet &, ref<Expr>, bool &result,
+                   SolverQueryMetaData &metaData);
 
-    bool mayBeFalse(const ExecutionState&, ref<Expr>, bool &result);
+  bool mayBeTrue(const ConstraintSet &, ref<Expr>, bool &result,
+                 SolverQueryMetaData &metaData);
 
-    bool getValue(const ExecutionState &, ref<Expr> expr, 
-                  ref<ConstantExpr> &result);
+  bool mayBeFalse(const ConstraintSet &, ref<Expr>, bool &result,
+                  SolverQueryMetaData &metaData);
 
-    bool getInitialValues(const ExecutionState&, 
-                          const std::vector<const Array*> &objects,
-                          std::vector< std::vector<unsigned char> > &result);
+  bool getValue(const ConstraintSet &, ref<Expr> expr,
+                ref<ConstantExpr> &result, SolverQueryMetaData &metaData);
 
-    std::pair< ref<Expr>, ref<Expr> >
-    getRange(const ExecutionState&, ref<Expr> query);
-  };
+  bool getInitialValues(const ConstraintSet &,
+                        const std::vector<const Array *> &objects,
+                        std::vector<std::vector<unsigned char>> &result,
+                        SolverQueryMetaData &metaData);
 
+  std::pair<ref<Expr>, ref<Expr>> getRange(const ConstraintSet &,
+                                           ref<Expr> query,
+                                           SolverQueryMetaData &metaData);
+};
 }
 
 #endif /* KLEE_TIMINGSOLVER_H */
-- 
cgit 1.4.1