File 0003-Core-TimingSolver-use-WallTimer.patch of Package klee

Overview Repositories Revisions Requests Users Attributes Meta

File 0003-Core-TimingSolver-use-WallTimer.patch of Package klee (Revision f8ebdb80b86b8738197a7c593552a392)

Currently displaying revision f8ebdb80b86b8738197a7c593552a392 , Show latest

From: Jiri Slaby <jirislaby@gmail.com>
Date: Wed, 7 Jun 2017 16:50:27 +0200
Subject: Core: TimingSolver, use WallTimer
Patch-mainline: no

Do not opencode what we already have in WallTimer. This simplifies the
code a lot and makes transition to LLVM 4.0 a lot easier.

We also introduce a helper to update the times.

Signed-off-by: Jiri Slaby <jirislaby@gmail.com>
---
 lib/Core/TimingSolver.cpp | 38 +++++++++++++++-----------------------
 lib/Core/TimingSolver.h   |  3 +++
 2 files changed, 18 insertions(+), 23 deletions(-)

diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index b70bcbefcddc..77451111b676 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -13,17 +13,21 @@
 #include "klee/ExecutionState.h"
 #include "klee/Solver.h"
 #include "klee/Statistics.h"
-#include "klee/Internal/System/Time.h"
+#include "klee/Internal/Support/Timer.h"
 
 #include "CoreStats.h"
 
-#include "llvm/Support/TimeValue.h"
-
 using namespace klee;
 using namespace llvm;
 
 /***/
 
+void TimingSolver::updateTimes(const ExecutionState& state, uint64_t usec)
+{
+  stats::solverTime += usec;
+  state.queryCost += usec / 1e6;
+}
+
 bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
                             Solver::Validity &result) {
   // Fast path, to avoid timer and OS overhead.
@@ -32,17 +36,14 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
     return true;
   }
 
-  sys::TimeValue now = util::getWallTimeVal();
+  WallTimer timer;
 
   if (simplifyExprs)
     expr = state.constraints.simplifyExpr(expr);
 
   bool success = solver->evaluate(Query(state.constraints, expr), result);
 
-  sys::TimeValue delta = util::getWallTimeVal();
-  delta -= now;
-  stats::solverTime += delta.usec();
-  state.queryCost += delta.usec()/1000000.;
+  updateTimes(state, timer.check());
 
   return success;
 }
@@ -55,17 +56,14 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr,
     return true;
   }
 
-  sys::TimeValue now = util::getWallTimeVal();
+  WallTimer timer;
 
   if (simplifyExprs)
     expr = state.constraints.simplifyExpr(expr);
 
   bool success = solver->mustBeTrue(Query(state.constraints, expr), result);
 
-  sys::TimeValue delta = util::getWallTimeVal();
-  delta -= now;
-  stats::solverTime += delta.usec();
-  state.queryCost += delta.usec()/1000000.;
+  updateTimes(state, timer.check());
 
   return success;
 }
@@ -101,17 +99,14 @@ bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr,
     return true;
   }
   
-  sys::TimeValue now = util::getWallTimeVal();
+  WallTimer timer;
 
   if (simplifyExprs)
     expr = state.constraints.simplifyExpr(expr);
 
   bool success = solver->getValue(Query(state.constraints, expr), result);
 
-  sys::TimeValue delta = util::getWallTimeVal();
-  delta -= now;
-  stats::solverTime += delta.usec();
-  state.queryCost += delta.usec()/1000000.;
+  updateTimes(state, timer.check());
 
   return success;
 }
@@ -125,16 +120,13 @@ TimingSolver::getInitialValues(const ExecutionState& state,
   if (objects.empty())
     return true;
 
-  sys::TimeValue now = util::getWallTimeVal();
+  WallTimer timer;
 
   bool success = solver->getInitialValues(Query(state.constraints,
                                                 ConstantExpr::alloc(0, Expr::Bool)), 
                                           objects, result);
   
-  sys::TimeValue delta = util::getWallTimeVal();
-  delta -= now;
-  stats::solverTime += delta.usec();
-  state.queryCost += delta.usec()/1000000.;
+  updateTimes(state, timer.check());
   
   return success;
 }
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index c98dd881b841..c1c229b08fc0 100644
--- a/lib/Core/TimingSolver.h
+++ b/lib/Core/TimingSolver.h
@@ -26,6 +26,9 @@ namespace klee {
     Solver *solver;
     bool simplifyExprs;
 
+  private:
+    void updateTimes(const ExecutionState& state, uint64_t usec);
+
   public:
     /// TimingSolver - Construct a new timing solver.
     ///
-- 
2.13.1

Places

File 0003-Core-TimingSolver-use-WallTimer.patch of Package klee (Revision f8ebdb80b86b8738197a7c593552a392)

Places