diff options
author | Emil Rakadjiev <emil.rakadjiev.bf@hitachi.com> | 2015-03-09 18:52:11 +0900 |
---|---|---|
committer | Emil Rakadjiev <emil.rakadjiev.bf@hitachi.com> | 2015-03-13 11:37:37 +0900 |
commit | 78946863d6d44475bb3363e07587fedb053d65d5 (patch) | |
tree | 6c2ce971840fad337f5107364381298054c999ec /lib/Core/TimingSolver.cpp | |
parent | d9b5b92cb1627edce7d476f8fd4328f5ee6f3bc8 (diff) | |
download | klee-78946863d6d44475bb3363e07587fedb053d65d5.tar.gz |
Timestamp improvements.
Replaced inefficient llvm::sys::Process::GetTimeUsage() with TimeValue::now(), because in many cases only the wall clock time is needed, not the user and sys times (which are significantly more expensive to get). Updated TimingSolver and WallTimer accordingly.
Diffstat (limited to 'lib/Core/TimingSolver.cpp')
-rw-r--r-- | lib/Core/TimingSolver.cpp | 23 |
1 files changed, 10 insertions, 13 deletions
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp index 037b23f3..b70bcbef 100644 --- a/lib/Core/TimingSolver.cpp +++ b/lib/Core/TimingSolver.cpp @@ -13,10 +13,11 @@ #include "klee/ExecutionState.h" #include "klee/Solver.h" #include "klee/Statistics.h" +#include "klee/Internal/System/Time.h" #include "CoreStats.h" -#include "llvm/Support/Process.h" +#include "llvm/Support/TimeValue.h" using namespace klee; using namespace llvm; @@ -31,15 +32,14 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr, return true; } - sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0); - sys::Process::GetTimeUsage(now,user,sys); + sys::TimeValue now = util::getWallTimeVal(); if (simplifyExprs) expr = state.constraints.simplifyExpr(expr); bool success = solver->evaluate(Query(state.constraints, expr), result); - sys::Process::GetTimeUsage(delta,user,sys); + sys::TimeValue delta = util::getWallTimeVal(); delta -= now; stats::solverTime += delta.usec(); state.queryCost += delta.usec()/1000000.; @@ -55,15 +55,14 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr, return true; } - sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0); - sys::Process::GetTimeUsage(now,user,sys); + sys::TimeValue now = util::getWallTimeVal(); if (simplifyExprs) expr = state.constraints.simplifyExpr(expr); bool success = solver->mustBeTrue(Query(state.constraints, expr), result); - sys::Process::GetTimeUsage(delta,user,sys); + sys::TimeValue delta = util::getWallTimeVal(); delta -= now; stats::solverTime += delta.usec(); state.queryCost += delta.usec()/1000000.; @@ -102,15 +101,14 @@ bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr, return true; } - sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0); - sys::Process::GetTimeUsage(now,user,sys); + sys::TimeValue now = util::getWallTimeVal(); if (simplifyExprs) expr = state.constraints.simplifyExpr(expr); bool success = solver->getValue(Query(state.constraints, expr), result); - sys::Process::GetTimeUsage(delta,user,sys); + sys::TimeValue delta = util::getWallTimeVal(); delta -= now; stats::solverTime += delta.usec(); state.queryCost += delta.usec()/1000000.; @@ -127,14 +125,13 @@ TimingSolver::getInitialValues(const ExecutionState& state, if (objects.empty()) return true; - sys::TimeValue now(0,0),user(0,0),delta(0,0),sys(0,0); - sys::Process::GetTimeUsage(now,user,sys); + sys::TimeValue now = util::getWallTimeVal(); bool success = solver->getInitialValues(Query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)), objects, result); - sys::Process::GetTimeUsage(delta,user,sys); + sys::TimeValue delta = util::getWallTimeVal(); delta -= now; stats::solverTime += delta.usec(); state.queryCost += delta.usec()/1000000.; |