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)

1 files changed, 15 insertions, 13 deletions

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();