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)

2 files changed, 26 insertions, 18 deletions

diff --git a/lib/Basic/CmdLineOptions.cpp b/lib/Basic/CmdLineOptions.cpp
index b4517d47..b071eab6 100644
--- a/lib/Basic/CmdLineOptions.cpp
+++ b/lib/Basic/CmdLineOptions.cpp
@@ -23,6 +23,15 @@ using namespace llvm;
 
 namespace klee {
 
+cl::extrahelp TimeFormatInfo(
+  "\nTime format used by KLEE's options\n"
+  "\n"
+  "  Time spans can be specified in two ways:\n"
+  "    1. As positive real numbers representing seconds, e.g. '10', '3.5' but not 'INF', 'NaN', '1e3', '-4.5s'\n"
+  "    2. As a sequence of natural numbers with specified units, e.g. '1h10min' (= '70min'), '5min10s' but not '3.5min', '8S'\n"
+  "       The following units are supported: h, min, s, ms, us, ns.\n"
+);
+
 cl::opt<bool>
 UseFastCexSolver("use-fast-cex-solver",
 		 cl::init(false),
@@ -47,19 +56,19 @@ cl::opt<bool>
 DebugValidateSolver("debug-validate-solver",
                     cl::init(false));
   
-cl::opt<int>
+cl::opt<std::string>
 MinQueryTimeToLog("min-query-time-to-log",
-                  cl::init(0),
-                  cl::value_desc("milliseconds"),
-                  cl::desc("Set time threshold (in ms) for queries logged in files. "
-                           "Only queries longer than threshold will be logged. (default=0). "
-                           "Set this param to a negative value to log timeouts only."));
+                  cl::desc("Set time threshold for queries logged in files. "
+                           "Only queries longer than threshold will be logged. (default=0s)"));
+
+cl::opt<bool>
+LogTimedOutQueries("log-timed-out-queries",
+                   cl::init(true),
+                   cl::desc("Log queries that timed out. (default=true)."));
 
-cl::opt<double>
+cl::opt<std::string>
 MaxCoreSolverTime("max-solver-time",
-                  cl::desc("Maximum amount of time for a single SMT query (default=0s (off)). Enables --use-forked-solver"),
-                  cl::init(0.0),
-                  cl::value_desc("seconds"));
+                  cl::desc("Maximum amount of time for a single SMT query (default=0s (off)). Enables --use-forked-solver"));
 
 cl::opt<bool>
 UseForkedCoreSolver("use-forked-solver",
diff --git a/lib/Basic/ConstructSolverChain.cpp b/lib/Basic/ConstructSolverChain.cpp
index 5880ad59..8341f62d 100644
--- a/lib/Basic/ConstructSolverChain.cpp
+++ b/lib/Basic/ConstructSolverChain.cpp
@@ -13,8 +13,10 @@
 #include "klee/Common.h"
 #include "klee/SolverCmdLine.h"
 #include "klee/Internal/Support/ErrorHandling.h"
+#include "klee/Internal/System/Time.h"
 #include "llvm/Support/raw_ostream.h"
 
+
 namespace klee {
 Solver *constructSolverChain(Solver *coreSolver,
                              std::string querySMT2LogPath,
@@ -22,17 +24,16 @@ Solver *constructSolverChain(Solver *coreSolver,
                              std::string queryKQueryLogPath,
                              std::string baseSolverQueryKQueryLogPath) {
   Solver *solver = coreSolver;
+  const time::Span minQueryTimeToLog(MinQueryTimeToLog);
 
   if (queryLoggingOptions.isSet(SOLVER_KQUERY)) {
-    solver = createKQueryLoggingSolver(solver, baseSolverQueryKQueryLogPath,
-                                   MinQueryTimeToLog);
+    solver = createKQueryLoggingSolver(solver, baseSolverQueryKQueryLogPath, minQueryTimeToLog, LogTimedOutQueries);
     klee_message("Logging queries that reach solver in .kquery format to %s\n",
                  baseSolverQueryKQueryLogPath.c_str());
   }
 
   if (queryLoggingOptions.isSet(SOLVER_SMTLIB)) {
-    solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath,
-                                       MinQueryTimeToLog);
+    solver = createSMTLIBLoggingSolver(solver, baseSolverQuerySMT2LogPath, minQueryTimeToLog, LogTimedOutQueries);
     klee_message("Logging queries that reach solver in .smt2 format to %s\n",
                  baseSolverQuerySMT2LogPath.c_str());
   }
@@ -56,15 +57,13 @@ Solver *constructSolverChain(Solver *coreSolver,
     solver = createValidatingSolver(solver, coreSolver);
 
   if (queryLoggingOptions.isSet(ALL_KQUERY)) {
-    solver = createKQueryLoggingSolver(solver, queryKQueryLogPath,
-                                       MinQueryTimeToLog);
+    solver = createKQueryLoggingSolver(solver, queryKQueryLogPath, minQueryTimeToLog, LogTimedOutQueries);
     klee_message("Logging all queries in .kquery format to %s\n",
                  queryKQueryLogPath.c_str());
   }
 
   if (queryLoggingOptions.isSet(ALL_SMTLIB)) {
-    solver =
-        createSMTLIBLoggingSolver(solver, querySMT2LogPath, MinQueryTimeToLog);
+    solver = createSMTLIBLoggingSolver(solver, querySMT2LogPath, minQueryTimeToLog, LogTimedOutQueries);
     klee_message("Logging all queries in .smt2 format to %s\n",
                  querySMT2LogPath.c_str());
   }