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.

4 files changed, 29 insertions, 23 deletions

diff --git a/include/klee/Internal/System/Time.h b/include/klee/Internal/System/Time.h
index 5229c8c9..14d23536 100644
--- a/include/klee/Internal/System/Time.h
+++ b/include/klee/Internal/System/Time.h
@@ -10,10 +10,19 @@
 #ifndef KLEE_UTIL_TIME_H
 #define KLEE_UTIL_TIME_H
 
+#include <llvm/Support/TimeValue.h>
+
 namespace klee {
   namespace util {
+
+    /// Seconds spent by this process in user mode.
     double getUserTime();
+
+    /// Wall time in seconds.
     double getWallTime();
+
+    /// Wall time as TimeValue object.
+    llvm::sys::TimeValue getWallTimeVal();
   }
 }
 
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.;
diff --git a/lib/Support/Time.cpp b/lib/Support/Time.cpp
index 909e07da..be5eaf18 100644
--- a/lib/Support/Time.cpp
+++ b/lib/Support/Time.cpp
@@ -10,6 +10,7 @@
 #include "klee/Config/Version.h"
 #include "klee/Internal/System/Time.h"
 
+#include "llvm/Support/TimeValue.h"
 #include "llvm/Support/Process.h"
 
 using namespace llvm;
@@ -22,7 +23,10 @@ double util::getUserTime() {
 }
 
 double util::getWallTime() {
-  sys::TimeValue now(0,0),user(0,0),sys(0,0);
-  sys::Process::GetTimeUsage(now,user,sys);
-  return (now.seconds() + (double) now.nanoseconds() * 1e-9);
+  sys::TimeValue now = getWallTimeVal();
+  return (now.seconds() + ((double) now.nanoseconds() * 1e-9));
+}
+
+sys::TimeValue util::getWallTimeVal() {
+  return sys::TimeValue::now();
 }
diff --git a/lib/Support/Timer.cpp b/lib/Support/Timer.cpp
index c61a90a3..da969810 100644
--- a/lib/Support/Timer.cpp
+++ b/lib/Support/Timer.cpp
@@ -10,19 +10,15 @@
 #include "klee/Config/Version.h"
 #include "klee/Internal/Support/Timer.h"
 
-#include "llvm/Support/Process.h"
+#include "klee/Internal/System/Time.h"
 
 using namespace klee;
 using namespace llvm;
 
 WallTimer::WallTimer() {
-  sys::TimeValue now(0,0),user(0,0),sys(0,0);
-  sys::Process::GetTimeUsage(now,user,sys);
-  startMicroseconds = now.usec();
+  startMicroseconds = util::getWallTimeVal().usec();
 }
 
 uint64_t WallTimer::check() {
-  sys::TimeValue now(0,0),user(0,0),sys(0,0);
-  sys::Process::GetTimeUsage(now,user,sys);
-  return now.usec() - startMicroseconds;
+  return util::getWallTimeVal().usec() - startMicroseconds;
 }