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)

8 files changed, 119 insertions, 42 deletions

diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h
index ceb07864..69b29865 100644
--- a/include/klee/ExecutionState.h
+++ b/include/klee/ExecutionState.h
@@ -13,6 +13,7 @@
 #include "klee/Constraints.h"
 #include "klee/Expr.h"
 #include "klee/Internal/ADT/TreeStream.h"
+#include "klee/Internal/System/Time.h"
 #include "klee/MergeHandler.h"
 
 // FIXME: We do not want to be exposing these? :(
@@ -101,7 +102,7 @@ public:
   /// Statistics and information
 
   /// @brief Costs for all queries issued for this state, in seconds
-  mutable double queryCost;
+  mutable time::Span queryCost;
 
   /// @brief Weight assigned for importance of this state.  Can be
   /// used for searchers to decide what paths to explore
diff --git a/include/klee/IncompleteSolver.h b/include/klee/IncompleteSolver.h
index f589e3b3..25b6cc68 100644
--- a/include/klee/IncompleteSolver.h
+++ b/include/klee/IncompleteSolver.h
@@ -103,7 +103,7 @@ public:
                             bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
   char *getConstraintLog(const Query&);
-  void setCoreSolverTimeout(double timeout);
+  void setCoreSolverTimeout(time::Span timeout);
 };
 
 }
diff --git a/include/klee/Internal/Support/Timer.h b/include/klee/Internal/Support/Timer.h
index d80ccb31..4cbd3f68 100644
--- a/include/klee/Internal/Support/Timer.h
+++ b/include/klee/Internal/Support/Timer.h
@@ -10,25 +10,17 @@
 #ifndef KLEE_TIMER_H
 #define KLEE_TIMER_H
 
-#include <stdint.h>
-
-#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
-#include <llvm/Support/Chrono.h>
-#endif
+#include "klee/Internal/System/Time.h"
 
 namespace klee {
   class WallTimer {
-#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
-    llvm::sys::TimePoint<> start;
-#else
-    uint64_t startMicroseconds;
-#endif
+    time::Point start;
     
   public:
     WallTimer();
 
-    /// check - Return the delta since the timer was created, in microseconds.
-    uint64_t check();
+    /// check - Return the delta since the timer was created
+    time::Span check();
   };
 }
 
diff --git a/include/klee/Internal/System/Time.h b/include/klee/Internal/System/Time.h
index 12522c86..9c021ddc 100644
--- a/include/klee/Internal/System/Time.h
+++ b/include/klee/Internal/System/Time.h
@@ -10,31 +10,108 @@
 #ifndef KLEE_UTIL_TIME_H
 #define KLEE_UTIL_TIME_H
 
-#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
-#include <chrono>
+#include "llvm/Support/raw_ostream.h"
 
-#include "llvm/Support/Chrono.h"
-#else
-#include "llvm/Support/TimeValue.h"
-#endif
+#include <chrono>
+#include <string>
+#include <sys/time.h>
 
 namespace klee {
-  namespace util {
+  namespace time {
 
-    /// Seconds spent by this process in user mode.
-    double getUserTime();
+    /// The klee::time namespace offers various functions to measure the time (`getWallTime`)
+    /// and to get timing information for the current KLEE process (`getUserTime`).
+    /// This implementation is based on `std::chrono` and uses time points and time spans.
+    /// For KLEE statistics, spans are converted to µs and stored in `uint64_t`.
 
-    /// Wall time in seconds.
-    double getWallTime();
+    struct Point;
+    struct Span;
 
-    /// Wall time as TimeValue object.
-#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0)
-    double durationToDouble(std::chrono::nanoseconds dur);
-    llvm::sys::TimePoint<> getWallTimeVal();
-#else
-    llvm::sys::TimeValue getWallTimeVal();
-#endif
-  }
-}
+    /// Returns information about clock
+    std::string getClockInfo();
+
+    /// Returns time spent by this process in user mode
+    Span getUserTime();
+
+    /// Returns point in time using a monotonic steady clock
+    Point getWallTime();
+
+    struct Point {
+      using SteadyTimePoint = std::chrono::steady_clock::time_point;
+
+      SteadyTimePoint point;
+
+      // ctors
+      Point() = default;
+      explicit Point(SteadyTimePoint p): point(p) {};
+
+      // operators
+      Point& operator+=(const Span&);
+      Point& operator-=(const Span&);
+    };
+
+    // operators
+    Point operator+(const Point&, const Span&);
+    Point operator+(const Span&, const Point&);
+    Point operator-(const Point&, const Span&);
+    Span operator-(const Point&, const Point&);
+    bool operator==(const Point&, const Point&);
+    bool operator!=(const Point&, const Point&);
+    bool operator<(const Point&, const Point&);
+    bool operator<=(const Point&, const Point&);
+    bool operator>(const Point&, const Point&);
+    bool operator>=(const Point&, const Point&);
+
+    namespace { using Duration = std::chrono::steady_clock::duration; }
+
+    struct Span {
+      Duration duration = Duration::zero();
+
+      // ctors
+      Span() = default;
+      explicit Span(const Duration &d): duration(d) {}
+      explicit Span(const std::string &s);
+
+      // operators
+      Span& operator=(const Duration&);
+      Span& operator+=(const Span&);
+      Span& operator-=(const Span&);
+      Span& operator*=(const Duration::rep&);
+
+      // conversions
+      explicit operator Duration() const;
+      explicit operator bool() const;
+      explicit operator timeval() const;
+
+      std::uint64_t toMicroseconds() const;
+      double toSeconds() const;
+      std::tuple<std::uint32_t, std::uint8_t, std::uint8_t> toHMS() const; // hours, minutes, seconds
+    };
+
+    Span operator+(const Span&, const Span&);
+    Span operator-(const Span&, const Span&);
+    Span operator*(const Span&, const Duration::rep&);
+    Span operator/(const Span&, const Duration::rep&);
+    Span operator*(const Duration::rep&, const Span&);
+    bool operator==(const Span&, const Span&);
+    bool operator<=(const Span&, const Span&);
+    bool operator>=(const Span&, const Span&);
+    bool operator<(const Span&, const Span&);
+    bool operator>(const Span&, const Span&);
+
+    /// Span -> "X.Ys"
+    std::ostream& operator<<(std::ostream&, Span);
+    llvm::raw_ostream& operator<<(llvm::raw_ostream&, Span);
+
+    /// time spans
+    Span hours(std::uint16_t);
+    Span minutes(std::uint16_t);
+    Span seconds(std::uint64_t);
+    Span milliseconds(std::uint64_t);
+    Span microseconds(std::uint64_t);
+    Span nanoseconds(std::uint64_t);
+
+  } // time
+} // klee
 
 #endif
diff --git a/include/klee/Solver.h b/include/klee/Solver.h
index c2a8ef1e..1aaf555d 100644
--- a/include/klee/Solver.h
+++ b/include/klee/Solver.h
@@ -12,6 +12,7 @@
 
 #include "klee/Expr.h"
 #include "klee/SolverCmdLine.h"
+#include "klee/Internal/System/Time.h"
 
 #include <vector>
 
@@ -200,7 +201,7 @@ namespace klee {
     virtual std::pair< ref<Expr>, ref<Expr> > getRange(const Query&);
     
     virtual char *getConstraintLog(const Query& query);
-    virtual void setCoreSolverTimeout(double timeout);
+    virtual void setCoreSolverTimeout(time::Span timeout);
   };
 
   /* *** */
@@ -251,12 +252,14 @@ namespace klee {
   /// createKQueryLoggingSolver - Create a solver which will forward all queries
   /// after writing them to the given path in .kquery format.
   Solver *createKQueryLoggingSolver(Solver *s, std::string path,
-                                int minQueryTimeToLog);
+                                    time::Span minQueryTimeToLog,
+                                    bool logTimedOut);
 
   /// createSMTLIBLoggingSolver - Create a solver which will forward all queries
   /// after writing them to the given path in .smt2 format.
   Solver *createSMTLIBLoggingSolver(Solver *s, std::string path,
-                                    int minQueryTimeToLog);
+                                    time::Span minQueryTimeToLog,
+                                    bool logTimedOut);
 
 
   /// createDummySolver - Create a dummy solver implementation which always
diff --git a/include/klee/SolverCmdLine.h b/include/klee/SolverCmdLine.h
index 19e5fae6..82302208 100644
--- a/include/klee/SolverCmdLine.h
+++ b/include/klee/SolverCmdLine.h
@@ -32,9 +32,11 @@ extern llvm::cl::opt<bool> UseIndependentSolver;
 
 extern llvm::cl::opt<bool> DebugValidateSolver;
 
-extern llvm::cl::opt<int> MinQueryTimeToLog;
+extern llvm::cl::opt<std::string> MinQueryTimeToLog;
 
-extern llvm::cl::opt<double> MaxCoreSolverTime;
+extern llvm::cl::opt<bool> LogTimedOutQueries;
+
+extern llvm::cl::opt<std::string> MaxCoreSolverTime;
 
 extern llvm::cl::opt<bool> UseForkedCoreSolver;
 
diff --git a/include/klee/SolverImpl.h b/include/klee/SolverImpl.h
index 615f20c5..6ea06e2a 100644
--- a/include/klee/SolverImpl.h
+++ b/include/klee/SolverImpl.h
@@ -10,6 +10,7 @@
 #ifndef KLEE_SOLVERIMPL_H
 #define KLEE_SOLVERIMPL_H
 
+#include "klee/Internal/System/Time.h"
 #include "Solver.h"
 
 #include <vector>
@@ -105,7 +106,7 @@ namespace klee {
         return(NULL);
     }
 
-    virtual void setCoreSolverTimeout(double timeout) {};
+    virtual void setCoreSolverTimeout(time::Span timeout) {};
 };
 
 }
diff --git a/include/klee/TimerStatIncrementer.h b/include/klee/TimerStatIncrementer.h
index a351f96b..483d161a 100644
--- a/include/klee/TimerStatIncrementer.h
+++ b/include/klee/TimerStatIncrementer.h
@@ -22,10 +22,11 @@ namespace klee {
   public:
     TimerStatIncrementer(Statistic &_statistic) : statistic(_statistic) {}
     ~TimerStatIncrementer() {
-      statistic += timer.check(); 
+      // record microseconds
+      statistic += timer.check().toMicroseconds();
     }
 
-    uint64_t check() { return timer.check(); }
+    time::Span check() { return timer.check(); }
   };
 }