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, 9 insertions, 10 deletions

diff --git a/lib/Solver/QueryLoggingSolver.h b/lib/Solver/QueryLoggingSolver.h
index 4da3c129..75faf3a3 100644
--- a/lib/Solver/QueryLoggingSolver.h
+++ b/lib/Solver/QueryLoggingSolver.h
@@ -13,6 +13,8 @@
 
 #include "klee/Solver.h"
 #include "klee/SolverImpl.h"
+#include "klee/Internal/System/Time.h"
+
 #include "llvm/Support/raw_ostream.h"
 
 using namespace klee;
@@ -31,13 +33,10 @@ protected:
   // @brief buffer to store logs before flushing to file
   llvm::raw_string_ostream logBuffer;
   unsigned queryCount;
-  int minQueryTimeToLog; // we log to file only those queries
-                         // which take longer than the specified time (ms);
-                         // if this param is negative, log only those queries
-                         // on which the solver has timed out
-
-  double startTime;
-  double lastQueryTime;
+  time::Span minQueryTimeToLog; // we log to file only those queries which take longer than the specified time
+  bool logTimedOutQueries = false;
+  time::Point startTime;
+  time::Span lastQueryDuration;
   const std::string queryCommentSign; // sign representing commented lines
                                       // in given a query format
 
@@ -57,8 +56,8 @@ protected:
   void flushBufferConditionally(bool writeToFile);
 
 public:
-  QueryLoggingSolver(Solver *_solver, std::string path,
-                     const std::string &commentSign, int queryTimeToLog);
+  QueryLoggingSolver(Solver *_solver, std::string path, const std::string &commentSign,
+                     time::Span queryTimeToLog, bool logTimedOut);
 
   virtual ~QueryLoggingSolver();
 
@@ -72,7 +71,7 @@ public:
                             bool &hasSolution);
   SolverRunStatus getOperationStatusCode();
   char *getConstraintLog(const Query &);
-  void setCoreSolverTimeout(double timeout);
+  void setCoreSolverTimeout(time::Span timeout);
 };
 
 #endif /* KLEE_QUERYLOGGINGSOLVER_H */