From c350f6dcec853c8ab472acb7c31f9ea64f3145de Mon Sep 17 00:00:00 2001 From: Jiri Slaby Date: Wed, 7 Jun 2017 16:50:27 +0200 Subject: Core: TimingSolver, use TimerStatIncrementer Do not opencode what we already have in TimerStatIncrementer. This simplifies the code a lot and makes transition to LLVM 4.0 a lot easier. Signed-off-by: Jiri Slaby --- lib/Core/TimingSolver.cpp | 32 +++++++++----------------------- 1 file 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, 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, 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, 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; } -- cgit 1.4.1