Merge pull request #673 from jirislaby/llvm40_WallTimer

Core: TimingSolver, use WallTimer

1 files changed, 9 insertions, 23 deletions

diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index b70bcbef..3b66f641 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -13,12 +13,10 @@
 #include "klee/ExecutionState.h"
 #include "klee/Solver.h"
 #include "klee/Statistics.h"
-#include "klee/Internal/System/Time.h"
+#include "klee/TimerStatIncrementer.h"
 
 #include "CoreStats.h"
 
-#include "llvm/Support/TimeValue.h"
-
 using namespace klee;
 using namespace llvm;
 
@@ -32,17 +30,14 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
     return true;
   }
 
-  sys::TimeValue now = util::getWallTimeVal();
+  TimerStatIncrementer timer(stats::solverTime);
 
   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.;
+  state.queryCost += timer.check() / 1e6;
 
   return success;
 }
@@ -55,17 +50,14 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr,
     return true;
   }
 
-  sys::TimeValue now = util::getWallTimeVal();
+  TimerStatIncrementer timer(stats::solverTime);
 
   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.;
+  state.queryCost += timer.check() / 1e6;
 
   return success;
 }
@@ -101,17 +93,14 @@ bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr,
     return true;
   }
   
-  sys::TimeValue now = util::getWallTimeVal();
+  TimerStatIncrementer timer(stats::solverTime);
 
   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.;
+  state.queryCost += timer.check() / 1e6;
 
   return success;
 }
@@ -125,16 +114,13 @@ TimingSolver::getInitialValues(const ExecutionState& state,
   if (objects.empty())
     return true;
 
-  sys::TimeValue now = util::getWallTimeVal();
+  TimerStatIncrementer timer(stats::solverTime);
 
   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.;
+  state.queryCost += timer.check() / 1e6;
   
   return success;
 }