From 3caf3e985e4f35ac6ac04f61b92f11d2569550c6 Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Fri, 24 Nov 2017 16:58:27 +0000 Subject: 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) --- lib/Basic/CmdLineOptions.cpp | 29 +++++++++++++++++++---------- lib/Basic/ConstructSolverChain.cpp | 15 +++++++-------- 2 files changed, 26 insertions(+), 18 deletions(-) (limited to 'lib/Basic') 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 UseFastCexSolver("use-fast-cex-solver", cl::init(false), @@ -47,19 +56,19 @@ cl::opt DebugValidateSolver("debug-validate-solver", cl::init(false)); -cl::opt +cl::opt 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 +LogTimedOutQueries("log-timed-out-queries", + cl::init(true), + cl::desc("Log queries that timed out. (default=true).")); -cl::opt +cl::opt 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 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()); } -- cgit 1.4.1