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)

1 files changed, 42 insertions, 39 deletions

diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index cc0afff8..fc31e72d 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -23,8 +23,9 @@ using namespace llvm;
 
 /***/
 
-bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
-                            Solver::Validity &result) {
+bool TimingSolver::evaluate(const ConstraintSet &constraints, ref<Expr> expr,
+                            Solver::Validity &result,
+                            SolverQueryMetaData &metaData) {
   // Fast path, to avoid timer and OS overhead.
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
     result = CE->isTrue() ? Solver::True : Solver::False;
@@ -34,17 +35,17 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
   TimerStatIncrementer timer(stats::solverTime);
 
   if (simplifyExprs)
-    expr = ConstraintManager::simplifyExpr(state.constraints, expr);
+    expr = ConstraintManager::simplifyExpr(constraints, expr);
 
-  bool success = solver->evaluate(Query(state.constraints, expr), result);
+  bool success = solver->evaluate(Query(constraints, expr), result);
 
-  state.queryCost += timer.delta();
+  metaData.queryCost += timer.delta();
 
   return success;
 }
 
-bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr, 
-                              bool &result) {
+bool TimingSolver::mustBeTrue(const ConstraintSet &constraints, ref<Expr> expr,
+                              bool &result, SolverQueryMetaData &metaData) {
   // Fast path, to avoid timer and OS overhead.
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
     result = CE->isTrue() ? true : false;
@@ -54,40 +55,41 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr,
   TimerStatIncrementer timer(stats::solverTime);
 
   if (simplifyExprs)
-    expr = ConstraintManager::simplifyExpr(state.constraints, expr);
+    expr = ConstraintManager::simplifyExpr(constraints, expr);
 
-  bool success = solver->mustBeTrue(Query(state.constraints, expr), result);
+  bool success = solver->mustBeTrue(Query(constraints, expr), result);
 
-  state.queryCost += timer.delta();
+  metaData.queryCost += timer.delta();
 
   return success;
 }
 
-bool TimingSolver::mustBeFalse(const ExecutionState& state, ref<Expr> expr,
-                               bool &result) {
-  return mustBeTrue(state, Expr::createIsZero(expr), result);
+bool TimingSolver::mustBeFalse(const ConstraintSet &constraints, ref<Expr> expr,
+                               bool &result, SolverQueryMetaData &metaData) {
+  return mustBeTrue(constraints, Expr::createIsZero(expr), result, metaData);
 }
 
-bool TimingSolver::mayBeTrue(const ExecutionState& state, ref<Expr> expr, 
-                             bool &result) {
+bool TimingSolver::mayBeTrue(const ConstraintSet &constraints, ref<Expr> expr,
+                             bool &result, SolverQueryMetaData &metaData) {
   bool res;
-  if (!mustBeFalse(state, expr, res))
+  if (!mustBeFalse(constraints, expr, res, metaData))
     return false;
   result = !res;
   return true;
 }
 
-bool TimingSolver::mayBeFalse(const ExecutionState& state, ref<Expr> expr, 
-                              bool &result) {
+bool TimingSolver::mayBeFalse(const ConstraintSet &constraints, ref<Expr> expr,
+                              bool &result, SolverQueryMetaData &metaData) {
   bool res;
-  if (!mustBeTrue(state, expr, res))
+  if (!mustBeTrue(constraints, expr, res, metaData))
     return false;
   result = !res;
   return true;
 }
 
-bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr, 
-                            ref<ConstantExpr> &result) {
+bool TimingSolver::getValue(const ConstraintSet &constraints, ref<Expr> expr,
+                            ref<ConstantExpr> &result,
+                            SolverQueryMetaData &metaData) {
   // Fast path, to avoid timer and OS overhead.
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
     result = CE;
@@ -97,36 +99,37 @@ bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr,
   TimerStatIncrementer timer(stats::solverTime);
 
   if (simplifyExprs)
-    expr = ConstraintManager::simplifyExpr(state.constraints, expr);
+    expr = ConstraintManager::simplifyExpr(constraints, expr);
 
-  bool success = solver->getValue(Query(state.constraints, expr), result);
+  bool success = solver->getValue(Query(constraints, expr), result);
 
-  state.queryCost += timer.delta();
+  metaData.queryCost += timer.delta();
 
   return success;
 }
 
-bool 
-TimingSolver::getInitialValues(const ExecutionState& state, 
-                               const std::vector<const Array*>
-                                 &objects,
-                               std::vector< std::vector<unsigned char> >
-                                 &result) {
+bool TimingSolver::getInitialValues(
+    const ConstraintSet &constraints, const std::vector<const Array *> &objects,
+    std::vector<std::vector<unsigned char>> &result,
+    SolverQueryMetaData &metaData) {
   if (objects.empty())
     return true;
 
   TimerStatIncrementer timer(stats::solverTime);
 
-  bool success = solver->getInitialValues(Query(state.constraints,
-                                                ConstantExpr::alloc(0, Expr::Bool)), 
-                                          objects, result);
-  
-  state.queryCost += timer.delta();
-  
+  bool success = solver->getInitialValues(
+      Query(constraints, ConstantExpr::alloc(0, Expr::Bool)), objects, result);
+
+  metaData.queryCost += timer.delta();
+
   return success;
 }
 
-std::pair< ref<Expr>, ref<Expr> >
-TimingSolver::getRange(const ExecutionState& state, ref<Expr> expr) {
-  return solver->getRange(Query(state.constraints, expr));
+std::pair<ref<Expr>, ref<Expr>>
+TimingSolver::getRange(const ConstraintSet &constraints, ref<Expr> expr,
+                       SolverQueryMetaData &metaData) {
+  TimerStatIncrementer timer(stats::solverTime);
+  auto result = solver->getRange(Query(constraints, expr));
+  metaData.queryCost += timer.delta();
+  return result;
 }