Base time API upon std::chrono

This should not change the behaviour of KLEE and mimics the old API.

- functions moved from util into time namespace
- uses time points and time spans instead of double
- CLI arguments now have the form "3h5min8us"

Changed command line parameters:
- batch-time (double to string)
- istats-write-interval (double to string)
- max-instruction-time (double to string)
- max-solver-time (double to string)
- max-time (double to string)
- min-query-time-to-log (double to string)
- seed-time (double to string)
- stats-write-interval (double to string)
- uncovered-update-interval (double to string)
- added: log-timed-out-queries (replaces negative max-solver-time)

14 files changed, 140 insertions, 155 deletions

diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp
index 0f5a2bb7..fdf9c905 100644
--- a/lib/Core/AddressSpace.cpp
+++ b/lib/Core/AddressSpace.cpp
@@ -196,7 +196,7 @@ int AddressSpace::checkPointerInObject(ExecutionState &state,
 
 bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
                            ref<Expr> p, ResolutionList &rl,
-                           unsigned maxResolutions, double timeout) const {
+                           unsigned maxResolutions, time::Span timeout) const {
   if (ConstantExpr *CE = dyn_cast<ConstantExpr>(p)) {
     ObjectPair res;
     if (resolveOne(CE, res))
@@ -204,7 +204,6 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
     return false;
   } else {
     TimerStatIncrementer timer(stats::resolveTime);
-    uint64_t timeout_us = (uint64_t) (timeout * 1000000.);
 
     // XXX in general this isn't exactly what we want... for
     // a multiple resolution case (or for example, a \in {b,c,0})
@@ -238,7 +237,7 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
     while (oi != begin) {
       --oi;
       const MemoryObject *mo = oi->first;
-      if (timeout_us && timeout_us < timer.check())
+      if (timeout && timeout < timer.check())
         return true;
 
       int incomplete =
@@ -257,7 +256,7 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
     // search forwards
     for (oi = start; oi != end; ++oi) {
       const MemoryObject *mo = oi->first;
-      if (timeout_us && timeout_us < timer.check())
+      if (timeout && timeout < timer.check())
         return true;
 
       bool mustBeTrue;
diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h
index 57c0e472..2554a5b1 100644
--- a/lib/Core/AddressSpace.h
+++ b/lib/Core/AddressSpace.h
@@ -14,6 +14,7 @@
 
 #include "klee/Expr.h"
 #include "klee/Internal/ADT/ImmutableMap.h"
+#include "klee/Internal/System/Time.h"
 
 namespace klee {
   class ExecutionState;
@@ -61,7 +62,7 @@ namespace klee {
     ///
     /// \invariant forall o in objects, o->copyOnWriteOwner <= cowKey
     MemoryMap objects;
-    
+
     AddressSpace() : cowKey(1) {}
     AddressSpace(const AddressSpace &b) : cowKey(++b.cowKey), objects(b.objects) { }
     ~AddressSpace() {}
@@ -97,7 +98,7 @@ namespace klee {
                  ref<Expr> p,
                  ResolutionList &rl, 
                  unsigned maxResolutions=0,
-                 double timeout=0.) const;
+                 time::Span timeout=time::Span()) const;
 
     /***/
 
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp
index 00e372e4..9ba163da 100644
--- a/lib/Core/ExecutionState.cpp
+++ b/lib/Core/ExecutionState.cpp
@@ -66,7 +66,6 @@ ExecutionState::ExecutionState(KFunction *kf) :
     pc(kf->instructions),
     prevPC(pc),
 
-    queryCost(0.), 
     weight(1),
     depth(0),
 
@@ -79,7 +78,7 @@ ExecutionState::ExecutionState(KFunction *kf) :
 }
 
 ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions)
-    : constraints(assumptions), queryCost(0.), ptreeNode(0) {}
+    : constraints(assumptions), ptreeNode(0) {}
 
 ExecutionState::~ExecutionState() {
   for (unsigned int i=0; i<symbolics.size(); i++)
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 2e5b864c..ddf11929 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -244,15 +244,13 @@ namespace {
 		      cl::init(1.),
 		      cl::desc("(default=1.0)"));
 
-  cl::opt<double>
+  cl::opt<std::string>
   MaxInstructionTime("max-instruction-time",
-                     cl::desc("Only allow a single instruction to take this much time (default=0s (off)). Enables --use-forked-solver"),
-                     cl::init(0));
+                     cl::desc("Allow a single instruction to take only this much time (default=0s (off)). Enables --use-forked-solver"));
   
-  cl::opt<double>
+  cl::opt<std::string>
   SeedTime("seed-time",
-           cl::desc("Amount of time to dedicate to seeds, before normal search (default=0 (off))"),
-           cl::init(0));
+           cl::desc("Amount of time to dedicate to seeds, before normal search (default=0s (off))"));
   
   cl::list<Executor::TerminateReason>
   ExitOnErrorType("exit-on-error-type",
@@ -328,11 +326,14 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
       pathWriter(0), symPathWriter(0), specialFunctionHandler(0),
       processTree(0), replayKTest(0), replayPath(0), usingSeeds(0),
       atMemoryLimit(false), inhibitForking(false), haltExecution(false),
-      ivcEnabled(false),
-      coreSolverTimeout(MaxCoreSolverTime != 0 && MaxInstructionTime != 0
-                            ? std::min(MaxCoreSolverTime, MaxInstructionTime)
-                            : std::max(MaxCoreSolverTime, MaxInstructionTime)),
-      debugLogBuffer(debugBufferString) {
+      ivcEnabled(false), debugLogBuffer(debugBufferString) {
+
+
+  const time::Span maxCoreSolverTime(MaxCoreSolverTime);
+  maxInstructionTime = time::Span(MaxInstructionTime);
+  coreSolverTimeout = maxCoreSolverTime && maxInstructionTime ?
+                      std::min(maxCoreSolverTime, maxInstructionTime)
+                    : std::max(maxCoreSolverTime, maxInstructionTime);
 
   if (coreSolverTimeout) UseForkedCoreSolver = true;
   Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse);
@@ -779,7 +780,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
   if (!isSeeding && !isa<ConstantExpr>(condition) && 
       (MaxStaticForkPct!=1. || MaxStaticSolvePct != 1. ||
        MaxStaticCPForkPct!=1. || MaxStaticCPSolvePct != 1.) &&
-      statsTracker->elapsed() > 60.) {
+      statsTracker->elapsed() > time::seconds(60)) {
     StatisticManager &sm = *theStatisticManager;
     CallPathNode *cpn = current.stack.back().callPathNode;
     if ((MaxStaticForkPct<1. &&
@@ -803,12 +804,12 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
     }
   }
 
-  double timeout = coreSolverTimeout;
+  time::Span timeout = coreSolverTimeout;
   if (isSeeding)
     timeout *= it->second.size();
   solver->setTimeout(timeout);
   bool success = solver->evaluate(current, condition, res);
-  solver->setTimeout(0);
+  solver->setTimeout(time::Span());
   if (!success) {
     current.pc = current.prevPC;
     terminateStateEarly(current, "Query timed out (fork).");
@@ -1076,7 +1077,7 @@ ref<Expr> Executor::toUnique(const ExecutionState &state,
       if (solver->mustBeTrue(state, cond, isTrue) && isTrue)
         result = value;
     }
-    solver->setTimeout(0);
+    solver->setTimeout(time::Span());
   }
   
   return result;
@@ -2774,7 +2775,7 @@ void Executor::run(ExecutionState &initialState) {
       v.push_back(SeedInfo(*it));
 
     int lastNumSeeds = usingSeeds->size()+10;
-    double lastTime, startTime = lastTime = util::getWallTime();
+    time::Point lastTime, startTime = lastTime = time::getWallTime();
     ExecutionState *lastState = 0;
     while (!seedMap.empty()) {
       if (haltExecution) {
@@ -2793,7 +2794,7 @@ void Executor::run(ExecutionState &initialState) {
       stepInstruction(state);
 
       executeInstruction(state, ki);
-      processTimers(&state, MaxInstructionTime * numSeeds);
+      processTimers(&state, maxInstructionTime * numSeeds);
       updateStates(&state);
 
       if ((stats::instructions % 1000) == 0) {
@@ -2804,13 +2805,14 @@ void Executor::run(ExecutionState &initialState) {
           numSeeds += it->second.size();
           numStates++;
         }
-        double time = util::getWallTime();
-        if (SeedTime>0. && time > startTime + SeedTime) {
+        const auto time = time::getWallTime();
+        const time::Span seedTime(SeedTime);
+        if (seedTime && time > startTime + seedTime) {
           klee_warning("seed time expired, %d seeds remain over %d states",
                        numSeeds, numStates);
           break;
         } else if (numSeeds<=lastNumSeeds-10 ||
-                   time >= lastTime+10) {
+                   time - lastTime >= time::seconds(10)) {
           lastTime = time;
           lastNumSeeds = numSeeds;          
           klee_message("%d seeds remaining over: %d states", 
@@ -2846,7 +2848,7 @@ void Executor::run(ExecutionState &initialState) {
     stepInstruction(state);
 
     executeInstruction(state, ki);
-    processTimers(&state, MaxInstructionTime);
+    processTimers(&state, maxInstructionTime);
 
     checkMemoryUsage();
 
@@ -3457,7 +3459,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
     address = toConstant(state, address, "resolveOne failure");
     success = state.addressSpace.resolveOne(cast<ConstantExpr>(address), op);
   }
-  solver->setTimeout(0);
+  solver->setTimeout(time::Span());
 
   if (success) {
     const MemoryObject *mo = op.first;
@@ -3473,7 +3475,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
     bool inBounds;
     solver->setTimeout(coreSolverTimeout);
     bool success = solver->mustBeTrue(state, check, inBounds);
-    solver->setTimeout(0);
+    solver->setTimeout(time::Span());
     if (!success) {
       state.pc = state.prevPC;
       terminateStateEarly(state, "Query timed out (bounds check).");
@@ -3511,7 +3513,7 @@ void Executor::executeMemoryOperation(ExecutionState &state,
   solver->setTimeout(coreSolverTimeout);
   bool incomplete = state.addressSpace.resolve(state, solver, address, rl,
                                                0, coreSolverTimeout);
-  solver->setTimeout(0);
+  solver->setTimeout(time::Span());
   
   // XXX there is some query wasteage here. who cares?
   ExecutionState *unbound = &state;
@@ -3827,7 +3829,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state,
   for (unsigned i = 0; i != state.symbolics.size(); ++i)
     objects.push_back(state.symbolics[i].second);
   bool success = solver->getInitialValues(tmp, objects, values);
-  solver->setTimeout(0);
+  solver->setTimeout(time::Span());
   if (!success) {
     klee_warning("unable to compute initial values (invalid constraints?)!");
     ExprPPrinter::printQuery(llvm::errs(), state.constraints,
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 3643c3f4..180c9140 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -20,6 +20,7 @@
 #include "klee/Internal/Module/Cell.h"
 #include "klee/Internal/Module/KInstruction.h"
 #include "klee/Internal/Module/KModule.h"
+#include "klee/Internal/System/Time.h"
 #include "klee/util/ArrayCache.h"
 #include "llvm/Support/raw_ostream.h"
 
@@ -216,7 +217,10 @@ private:
 
   /// The maximum time to allow for a single core solver query.
   /// (e.g. for a single STP query)
-  double coreSolverTimeout;
+  time::Span coreSolverTimeout;
+
+  /// Maximum time to allow for a single instruction.
+  time::Span maxInstructionTime;
 
   /// Assumes ownership of the created array objects
   ArrayCache arrayCache;
@@ -461,11 +465,10 @@ private:
   ///
   /// \param timer The timer object to run on firings.
   /// \param rate The approximate delay (in seconds) between firings.
-  void addTimer(Timer *timer, double rate);
+  void addTimer(Timer *timer, time::Span rate);
 
   void initTimers();
-  void processTimers(ExecutionState *current,
-                     double maxInstTime);
+  void processTimers(ExecutionState *current, time::Span maxInstTime);
   void checkMemoryUsage();
   void printDebugInstructions(ExecutionState &state);
   void doDumpStates();
diff --git a/lib/Core/ExecutorTimerInfo.h b/lib/Core/ExecutorTimerInfo.h
index 60977b74..9127fb68 100644
--- a/lib/Core/ExecutorTimerInfo.h
+++ b/lib/Core/ExecutorTimerInfo.h
@@ -23,15 +23,15 @@ public:
   Timer *timer;
 
   /// Approximate delay per timer firing.
-  double rate;
+  time::Span rate;
   /// Wall time for next firing.
-  double nextFireTime;
+  time::Point nextFireTime;
 
 public:
-  TimerInfo(Timer *_timer, double _rate)
+  TimerInfo(Timer *_timer, time::Span _rate)
     : timer(_timer),
       rate(_rate),
-      nextFireTime(util::getWallTime() + rate) {}
+      nextFireTime(time::getWallTime() + rate) {}
   ~TimerInfo() { delete timer; }
 };
 
diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp
index a3c13530..de24d75d 100644
--- a/lib/Core/ExecutorTimers.cpp
+++ b/lib/Core/ExecutorTimers.cpp
@@ -23,6 +23,7 @@
 #include "llvm/IR/Function.h"
 #include "llvm/Support/CommandLine.h"
 
+#include <string>
 #include <unistd.h>
 #include <signal.h>
 #include <sys/time.h>
@@ -32,10 +33,9 @@
 using namespace llvm;
 using namespace klee;
 
-cl::opt<double>
+cl::opt<std::string>
 MaxTime("max-time",
-        cl::desc("Halt execution after the specified number of seconds (default=0 (off))"),
-        cl::init(0));
+        cl::desc("Halt execution after the specified number of seconds (default=0s (off))"));
 
 ///
 
@@ -54,7 +54,7 @@ public:
 
 ///
 
-static const double kSecondsPerTick = .1;
+static const time::Span kMilliSecondsPerTick(time::milliseconds(100));
 static volatile unsigned timerTicks = 0;
 
 // XXX hack
@@ -67,15 +67,11 @@ static void onAlarm(int) {
 
 // oooogalay
 static void setupHandler() {
-  struct itimerval t;
-  struct timeval tv;
-  
-  tv.tv_sec = (long) kSecondsPerTick;
-  tv.tv_usec = (long) (fmod(kSecondsPerTick, 1.)*1000000);
-  
+  itimerval t{};
+  timeval tv = static_cast<timeval>(kMilliSecondsPerTick);
   t.it_interval = t.it_value = tv;
-  
-  ::setitimer(ITIMER_REAL, &t, 0);
+
+  ::setitimer(ITIMER_REAL, &t, nullptr);
   ::signal(SIGALRM, onAlarm);
 }
 
@@ -87,8 +83,9 @@ void Executor::initTimers() {
     setupHandler();
   }
 
-  if (MaxTime) {
-    addTimer(new HaltTimer(this), MaxTime.getValue());
+  const time::Span maxTime(MaxTime);
+  if (maxTime) {
+    addTimer(new HaltTimer(this), maxTime);
   }
 }
 
@@ -98,12 +95,12 @@ Executor::Timer::Timer() {}
 
 Executor::Timer::~Timer() {}
 
-void Executor::addTimer(Timer *timer, double rate) {
+void Executor::addTimer(Timer *timer, time::Span rate) {
   timers.push_back(new TimerInfo(timer, rate));
 }
 
 void Executor::processTimers(ExecutionState *current,
-                             double maxInstTime) {
+                             time::Span maxInstTime) {
   static unsigned callsWithoutCheck = 0;
   unsigned ticks = timerTicks;
 
@@ -169,18 +166,17 @@ void Executor::processTimers(ExecutionState *current,
       dumpStates = 0;
     }
 
-    if (maxInstTime > 0 && current &&
+    if (maxInstTime && current &&
         std::find(removedStates.begin(), removedStates.end(), current) ==
             removedStates.end()) {
-      if (timerTicks*kSecondsPerTick > maxInstTime) {
-        klee_warning("max-instruction-time exceeded: %.2fs",
-                     timerTicks*kSecondsPerTick);
+      if (timerTicks*kMilliSecondsPerTick > maxInstTime) {
+        klee_warning("max-instruction-time exceeded: %.2fs", (timerTicks * kMilliSecondsPerTick).toSeconds());
         terminateStateEarly(*current, "max-instruction-time exceeded");
       }
     }
 
     if (!timers.empty()) {
-      double time = util::getWallTime();
+      auto time = time::getWallTime();
 
       for (std::vector<TimerInfo*>::iterator it = timers.begin(), 
              ie = timers.end(); it != ie; ++it) {
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 0c1f4316..cce83d23 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -214,7 +214,7 @@ double WeightedRandomSearcher::getWeight(ExecutionState *es) {
     return inv;
   }
   case QueryCost:
-    return (es->queryCost < .1) ? 1. : 1./es->queryCost;
+    return (es->queryCost.toSeconds() < .1) ? 1. : 1./ es->queryCost.toSeconds();
   case CoveringNew:
   case MinDistToUncovered: {
     uint64_t md2u = computeMinDistToUncovered(es->pc,
@@ -337,7 +337,7 @@ ExecutionState& MergingSearcher::selectState() {
 ///
 
 BatchingSearcher::BatchingSearcher(Searcher *_baseSearcher,
-                                   double _timeBudget,
+                                   time::Span _timeBudget,
                                    unsigned _instructionBudget) 
   : baseSearcher(_baseSearcher),
     timeBudget(_timeBudget),
@@ -352,18 +352,19 @@ BatchingSearcher::~BatchingSearcher() {
 
 ExecutionState &BatchingSearcher::selectState() {
   if (!lastState || 
-      (util::getWallTime()-lastStartTime)>timeBudget ||
-      (stats::instructions-lastStartInstructions)>instructionBudget) {
+      (time::getWallTime() - lastStartTime) > timeBudget ||
+      (stats::instructions - lastStartInstructions) > instructionBudget) {
     if (lastState) {
-      double delta = util::getWallTime()-lastStartTime;
-      if (delta>timeBudget*1.1) {
-        klee_message("increased time budget from %f to %f\n", timeBudget,
-                     delta);
+      time::Span delta = time::getWallTime() - lastStartTime;
+      auto t = timeBudget;
+      t *= 1.1;
+      if (delta > t) {
+        klee_message("increased time budget from %f to %f\n", timeBudget.toSeconds(), delta.toSeconds());
         timeBudget = delta;
       }
     }
     lastState = &baseSearcher->selectState();
-    lastStartTime = util::getWallTime();
+    lastStartTime = time::getWallTime();
     lastStartInstructions = stats::instructions;
     return *lastState;
   } else {
@@ -385,7 +386,7 @@ BatchingSearcher::update(ExecutionState *current,
 
 IterativeDeepeningTimeSearcher::IterativeDeepeningTimeSearcher(Searcher *_baseSearcher)
   : baseSearcher(_baseSearcher),
-    time(1.) {
+    time(time::seconds(1)) {
 }
 
 IterativeDeepeningTimeSearcher::~IterativeDeepeningTimeSearcher() {
@@ -394,14 +395,15 @@ IterativeDeepeningTimeSearcher::~IterativeDeepeningTimeSearcher() {
 
 ExecutionState &IterativeDeepeningTimeSearcher::selectState() {
   ExecutionState &res = baseSearcher->selectState();
-  startTime = util::getWallTime();
+  startTime = time::getWallTime();
   return res;
 }
 
 void IterativeDeepeningTimeSearcher::update(
     ExecutionState *current, const std::vector<ExecutionState *> &addedStates,
     const std::vector<ExecutionState *> &removedStates) {
-  double elapsed = util::getWallTime() - startTime;
+
+  const auto elapsed = time::getWallTime() - startTime;
 
   if (!removedStates.empty()) {
     std::vector<ExecutionState *> alt = removedStates;
@@ -431,7 +433,7 @@ void IterativeDeepeningTimeSearcher::update(
 
   if (baseSearcher->empty()) {
     time *= 2;
-    klee_message("increased time budget to %f\n", time);
+    klee_message("increased time budget to %f\n", time.toSeconds());
     std::vector<ExecutionState *> ps(pausedStates.begin(), pausedStates.end());
     baseSearcher->update(0, ps, std::vector<ExecutionState *>());
     pausedStates.clear();
diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h
index 47026410..dc0e12a4 100644
--- a/lib/Core/Searcher.h
+++ b/lib/Core/Searcher.h
@@ -10,11 +10,14 @@
 #ifndef KLEE_SEARCHER_H
 #define KLEE_SEARCHER_H
 
+#include "klee/Internal/System/Time.h"
+
 #include "llvm/Support/raw_ostream.h"
-#include <vector>
-#include <set>
+
 #include <map>
 #include <queue>
+#include <set>
+#include <vector>
 
 namespace llvm {
   class BasicBlock;
@@ -208,16 +211,16 @@ namespace klee {
 
   class BatchingSearcher : public Searcher {
     Searcher *baseSearcher;
-    double timeBudget;
+    time::Span timeBudget;
     unsigned instructionBudget;
 
     ExecutionState *lastState;
-    double lastStartTime;
+    time::Point lastStartTime;
     unsigned lastStartInstructions;
 
   public:
     BatchingSearcher(Searcher *baseSearcher, 
-                     double _timeBudget,
+                     time::Span _timeBudget,
                      unsigned _instructionBudget);
     ~BatchingSearcher();
 
@@ -237,7 +240,8 @@ namespace klee {
 
   class IterativeDeepeningTimeSearcher : public Searcher {
     Searcher *baseSearcher;
-    double time, startTime;
+    time::Point startTime;
+    time::Span time;
     std::set<ExecutionState*> pausedStates;
 
   public:
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index dee14e61..5ad0f174 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -17,7 +17,6 @@
 #include "klee/Internal/Module/KInstruction.h"
 #include "klee/Internal/Support/ModuleUtil.h"
 #include "klee/Internal/System/MemoryUsage.h"
-#include "klee/Internal/System/Time.h"
 #include "klee/Internal/Support/ErrorHandling.h"
 #include "klee/SolverStats.h"
 
@@ -71,20 +70,20 @@ namespace {
 	       cl::init(true),
                cl::desc("Write instruction level statistics in callgrind format (default=on)"));
 
-  cl::opt<double>
+  cl::opt<std::string>
   StatsWriteInterval("stats-write-interval",
-                     cl::init(1.),
-		     cl::desc("Approximate number of seconds between stats writes (default=1.0s)"));
+                     cl::init("1s"),
+                     cl::desc("Approximate time between stats writes (default=1s)"));
 
   cl::opt<unsigned> StatsWriteAfterInstructions(
       "stats-write-after-instructions", cl::init(0),
       cl::desc("Write statistics after each n instructions, 0 to disable "
                "(default=0)"));
 
-  cl::opt<double>
+  cl::opt<std::string>
   IStatsWriteInterval("istats-write-interval",
-		      cl::init(10.),
-                      cl::desc("Approximate number of seconds between istats writes (default: 10.0s)"));
+                      cl::init("10s"),
+                      cl::desc("Approximate number of seconds between istats writes (default=10s)"));
 
   cl::opt<unsigned> IStatsWriteAfterInstructions(
       "istats-write-after-instructions", cl::init(0),
@@ -92,10 +91,10 @@ namespace {
                "(default=0)"));
 
   // XXX I really would like to have dynamic rate control for something like this.
-  cl::opt<double>
+  cl::opt<std::string>
   UncoveredUpdateInterval("uncovered-update-interval",
-                          cl::init(30.),
-			  cl::desc("(default=30.0s)"));
+                          cl::init("30s"),
+                          cl::desc("(default=30s)"));
   
   cl::opt<bool>
   UseCallPaths("use-call-paths",
@@ -176,18 +175,20 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
                            bool _updateMinDistToUncovered)
   : executor(_executor),
     objectFilename(_objectFilename),
-    startWallTime(util::getWallTime()),
+    startWallTime(time::getWallTime()),
     numBranches(0),
     fullBranches(0),
     partialBranches(0),
     updateMinDistToUncovered(_updateMinDistToUncovered) {
 
-  if (StatsWriteAfterInstructions > 0 && StatsWriteInterval > 0)
+  const time::Span statsWriteInterval(StatsWriteInterval);
+  if (StatsWriteAfterInstructions > 0 && statsWriteInterval)
     klee_error("Both options --stats-write-interval and "
                "--stats-write-after-instructions cannot be enabled at the same "
                "time.");
 
-  if (IStatsWriteAfterInstructions > 0 && IStatsWriteInterval > 0)
+  const time::Span iStatsWriteInterval(IStatsWriteInterval);
+  if (IStatsWriteAfterInstructions > 0 && iStatsWriteInterval)
     klee_error(
         "Both options --istats-write-interval and "
         "--istats-write-after-instructions cannot be enabled at the same "
@@ -245,8 +246,8 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
       writeStatsHeader();
       writeStatsLine();
 
-      if (StatsWriteInterval > 0)
-        executor.addTimer(new WriteStatsTimer(this), StatsWriteInterval);
+      if (statsWriteInterval)
+        executor.addTimer(new WriteStatsTimer(this), statsWriteInterval);
     } else {
       klee_error("Unable to open statistics trace file (run.stats).");
     }
@@ -255,14 +256,14 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
   // Add timer to calculate uncovered instructions if needed by the solver
   if (updateMinDistToUncovered) {
     computeReachableUncovered();
-    executor.addTimer(new UpdateReachableTimer(this), UncoveredUpdateInterval);
+    executor.addTimer(new UpdateReachableTimer(this), time::Span(UncoveredUpdateInterval));
   }
 
   if (OutputIStats) {
     istatsFile = executor.interpreterHandler->openOutputFile("run.istats");
     if (istatsFile) {
-      if (IStatsWriteInterval > 0)
-        executor.addTimer(new WriteIStatsTimer(this), IStatsWriteInterval);
+      if (iStatsWriteInterval)
+        executor.addTimer(new WriteIStatsTimer(this), iStatsWriteInterval);
     } else {
       klee_error("Unable to open instruction level stats file (run.istats).");
     }
@@ -284,45 +285,21 @@ void StatsTracker::done() {
 void StatsTracker::stepInstruction(ExecutionState &es) {
   if (OutputIStats) {
     if (TrackInstructionTime) {
-#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
-      static sys::TimePoint<> lastNowTime;
-      static std::chrono::nanoseconds lastUserTime(0);
+      static time::Point lastNowTime(time::getWallTime());
+      static time::Span lastUserTime;
 
-      if (lastUserTime.count() == 0) {
-        std::chrono::nanoseconds sys;
-        sys::Process::GetTimeUsage(lastNowTime, lastUserTime, sys);
+      if (!lastUserTime) {
+        lastUserTime = time::getUserTime();
       } else {
-        sys::TimePoint<> now;
-        std::chrono::nanoseconds user, sys;
-
-        sys::Process::GetTimeUsage(now, user, sys);
-
-        auto delta =
-          std::chrono::duration_cast<std::chrono::microseconds>(user - lastUserTime);
-        auto deltaNow =
-          std::chrono::duration_cast<std::chrono::microseconds>(now - lastNowTime);
-        stats::instructionTime += delta.count();
-        stats::instructionRealTime += deltaNow.count();
+        const auto now = time::getWallTime();
+        const auto user = time::getUserTime();
+        const auto delta = user - lastUserTime;
+        const auto deltaNow = now - lastNowTime;
+        stats::instructionTime += delta.toMicroseconds();
+        stats::instructionRealTime += deltaNow.toMicroseconds();
         lastUserTime = user;
         lastNowTime = now;
       }
-#else
-      static sys::TimeValue lastNowTime(0,0),lastUserTime(0,0);
-    
-      if (lastUserTime.seconds()==0 && lastUserTime.nanoseconds()==0) {
-        sys::TimeValue sys(0,0);
-        sys::Process::GetTimeUsage(lastNowTime,lastUserTime,sys);
-      } else {
-        sys::TimeValue now(0,0),user(0,0),sys(0,0);
-        sys::Process::GetTimeUsage(now,user,sys);
-        sys::TimeValue delta = user - lastUserTime;
-        sys::TimeValue deltaNow = now - lastNowTime;
-        stats::instructionTime += delta.usec();
-        stats::instructionRealTime += deltaNow.usec();
-        lastUserTime = user;
-        lastNowTime = now;
-      }
-#endif
     }
 
     Instruction *inst = es.pc->inst;
@@ -447,8 +424,8 @@ void StatsTracker::writeStatsHeader() {
   statsFile->flush();
 }
 
-double StatsTracker::elapsed() {
-  return util::getWallTime() - startWallTime;
+time::Span StatsTracker::elapsed() {
+  return time::getWallTime() - startWallTime;
 }
 
 void StatsTracker::writeStatsLine() {
@@ -456,24 +433,24 @@ void StatsTracker::writeStatsLine() {
              << "," << fullBranches
              << "," << partialBranches
              << "," << numBranches
-             << "," << util::getUserTime()
+             << "," << time::getUserTime().toSeconds()
              << "," << executor.states.size()
              << "," << util::GetTotalMallocUsage() + executor.memory->getUsedDeterministicSize()
              << "," << stats::queries
              << "," << stats::queryConstructs
              << "," << 0 // was numObjects
-             << "," << elapsed()
+             << "," << elapsed().toSeconds()
              << "," << stats::coveredInstructions
              << "," << stats::uncoveredInstructions
-             << "," << stats::queryTime / 1000000.
-             << "," << stats::solverTime / 1000000.
-             << "," << stats::cexCacheTime / 1000000.
-             << "," << stats::forkTime / 1000000.
-             << "," << stats::resolveTime / 1000000.
+             << "," << time::microseconds(stats::queryTime).toSeconds()
+             << "," << time::microseconds(stats::solverTime).toSeconds()
+             << "," << time::microseconds(stats::cexCacheTime).toSeconds()
+             << "," << time::microseconds(stats::forkTime).toSeconds()
+             << "," << time::microseconds(stats::resolveTime).toSeconds()
              << "," << stats::queryCexCacheMisses
              << "," << stats::queryCexCacheHits
 #ifdef KLEE_ARRAY_DEBUG
-             << "," << stats::arrayHashTime / 1000000.
+             << "," << time::microseconds(stats::arrayHashTime).toSeconds()
 #endif
              << ")\n";
   statsFile->flush();
diff --git a/lib/Core/StatsTracker.h b/lib/Core/StatsTracker.h
index e352bb91..88e4cf30 100644
--- a/lib/Core/StatsTracker.h
+++ b/lib/Core/StatsTracker.h
@@ -11,6 +11,7 @@
 #define KLEE_STATSTRACKER_H
 
 #include "CallPathManager.h"
+#include "klee/Internal/System/Time.h"
 
 #include <memory>
 #include <set>
@@ -38,7 +39,7 @@ namespace klee {
     std::string objectFilename;
 
     std::unique_ptr<llvm::raw_fd_ostream> statsFile, istatsFile;
-    double startWallTime;
+    time::Point startWallTime;
 
     unsigned numBranches;
     unsigned fullBranches, partialBranches;
@@ -81,8 +82,8 @@ namespace klee {
     // about to be stepped
     void stepInstruction(ExecutionState &es);
 
-    /// Return time in seconds since execution start.
-    double elapsed();
+    /// Return duration since execution start.
+    time::Span elapsed();
 
     void computeReachableUncovered();
   };
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index 3b66f641..0f69509a 100644
--- a/lib/Core/TimingSolver.cpp
+++ b/lib/Core/TimingSolver.cpp
@@ -37,7 +37,7 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr,
 
   bool success = solver->evaluate(Query(state.constraints, expr), result);
 
-  state.queryCost += timer.check() / 1e6;
+  state.queryCost += timer.check();
 
   return success;
 }
@@ -57,7 +57,7 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr,
 
   bool success = solver->mustBeTrue(Query(state.constraints, expr), result);
 
-  state.queryCost += timer.check() / 1e6;
+  state.queryCost += timer.check();
 
   return success;
 }
@@ -100,7 +100,7 @@ bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr,
 
   bool success = solver->getValue(Query(state.constraints, expr), result);
 
-  state.queryCost += timer.check() / 1e6;
+  state.queryCost += timer.check();
 
   return success;
 }
@@ -120,7 +120,7 @@ TimingSolver::getInitialValues(const ExecutionState& state,
                                                 ConstantExpr::alloc(0, Expr::Bool)), 
                                           objects, result);
   
-  state.queryCost += timer.check() / 1e6;
+  state.queryCost += timer.check();
   
   return success;
 }
diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h
index c98dd881..08ed0de2 100644
--- a/lib/Core/TimingSolver.h
+++ b/lib/Core/TimingSolver.h
@@ -12,6 +12,7 @@
 
 #include "klee/Expr.h"
 #include "klee/Solver.h"
+#include "klee/Internal/System/Time.h"
 
 #include <vector>
 
@@ -38,7 +39,7 @@ namespace klee {
       delete solver;
     }
 
-    void setTimeout(double t) {
+    void setTimeout(time::Span t) {
       solver->setCoreSolverTimeout(t);
     }
     
diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp
index aa90c401..934cef54 100644
--- a/lib/Core/UserSearcher.cpp
+++ b/lib/Core/UserSearcher.cpp
@@ -51,10 +51,10 @@ namespace {
                     cl::desc("Number of instructions to batch when using --use-batching-search"),
                     cl::init(10000));
   
-  cl::opt<double>
+  cl::opt<std::string>
   BatchTime("batch-time",
-            cl::desc("Amount of time to batch when using --use-batching-search"),
-            cl::init(5.0));
+            cl::desc("Amount of time to batch when using --use-batching-search (default=5s)"),
+            cl::init("5s"));
 
 }
 
@@ -120,7 +120,7 @@ Searcher *klee::constructUserSearcher(Executor &executor) {
   }
 
   if (UseBatchingSearch) {
-    searcher = new BatchingSearcher(searcher, BatchTime, BatchInstructions);
+    searcher = new BatchingSearcher(searcher, time::Span(BatchTime), BatchInstructions);
   }
 
   if (UseMerge && UseIncompleteMerge) {