diff options
Diffstat (limited to 'lib')
35 files changed, 405 insertions, 305 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()); } diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp index 0f5a2bb7..fdf9c905 100644 --- a/lib/Core/AddressSpace.cpp +++ b/lib/Core/AddressSpace.cpp @@ -196,7 +196,7 @@ int AddressSpace::checkPointerInObject(ExecutionState &state, bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver, ref<Expr> p, ResolutionList &rl, - unsigned maxResolutions, double timeout) const { + unsigned maxResolutions, time::Span timeout) const { if (ConstantExpr *CE = dyn_cast<ConstantExpr>(p)) { ObjectPair res; if (resolveOne(CE, res)) @@ -204,7 +204,6 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver, return false; } else { TimerStatIncrementer timer(stats::resolveTime); - uint64_t timeout_us = (uint64_t) (timeout * 1000000.); // XXX in general this isn't exactly what we want... for // a multiple resolution case (or for example, a \in {b,c,0}) @@ -238,7 +237,7 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver, while (oi != begin) { --oi; const MemoryObject *mo = oi->first; - if (timeout_us && timeout_us < timer.check()) + if (timeout && timeout < timer.check()) return true; int incomplete = @@ -257,7 +256,7 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver, // search forwards for (oi = start; oi != end; ++oi) { const MemoryObject *mo = oi->first; - if (timeout_us && timeout_us < timer.check()) + if (timeout && timeout < timer.check()) return true; bool mustBeTrue; diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h index 57c0e472..2554a5b1 100644 --- a/lib/Core/AddressSpace.h +++ b/lib/Core/AddressSpace.h @@ -14,6 +14,7 @@ #include "klee/Expr.h" #include "klee/Internal/ADT/ImmutableMap.h" +#include "klee/Internal/System/Time.h" namespace klee { class ExecutionState; @@ -61,7 +62,7 @@ namespace klee { /// /// \invariant forall o in objects, o->copyOnWriteOwner <= cowKey MemoryMap objects; - + AddressSpace() : cowKey(1) {} AddressSpace(const AddressSpace &b) : cowKey(++b.cowKey), objects(b.objects) { } ~AddressSpace() {} @@ -97,7 +98,7 @@ namespace klee { ref<Expr> p, ResolutionList &rl, unsigned maxResolutions=0, - double timeout=0.) const; + time::Span timeout=time::Span()) const; /***/ diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 00e372e4..9ba163da 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -66,7 +66,6 @@ ExecutionState::ExecutionState(KFunction *kf) : pc(kf->instructions), prevPC(pc), - queryCost(0.), weight(1), depth(0), @@ -79,7 +78,7 @@ ExecutionState::ExecutionState(KFunction *kf) : } ExecutionState::ExecutionState(const std::vector<ref<Expr> > &assumptions) - : constraints(assumptions), queryCost(0.), ptreeNode(0) {} + : constraints(assumptions), ptreeNode(0) {} ExecutionState::~ExecutionState() { for (unsigned int i=0; i<symbolics.size(); i++) diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 2e5b864c..ddf11929 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -244,15 +244,13 @@ namespace { cl::init(1.), cl::desc("(default=1.0)")); - cl::opt<double> + cl::opt<std::string> MaxInstructionTime("max-instruction-time", - cl::desc("Only allow a single instruction to take this much time (default=0s (off)). Enables --use-forked-solver"), - cl::init(0)); + cl::desc("Allow a single instruction to take only this much time (default=0s (off)). Enables --use-forked-solver")); - cl::opt<double> + cl::opt<std::string> SeedTime("seed-time", - cl::desc("Amount of time to dedicate to seeds, before normal search (default=0 (off))"), - cl::init(0)); + cl::desc("Amount of time to dedicate to seeds, before normal search (default=0s (off))")); cl::list<Executor::TerminateReason> ExitOnErrorType("exit-on-error-type", @@ -328,11 +326,14 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts, pathWriter(0), symPathWriter(0), specialFunctionHandler(0), processTree(0), replayKTest(0), replayPath(0), usingSeeds(0), atMemoryLimit(false), inhibitForking(false), haltExecution(false), - ivcEnabled(false), - coreSolverTimeout(MaxCoreSolverTime != 0 && MaxInstructionTime != 0 - ? std::min(MaxCoreSolverTime, MaxInstructionTime) - : std::max(MaxCoreSolverTime, MaxInstructionTime)), - debugLogBuffer(debugBufferString) { + ivcEnabled(false), debugLogBuffer(debugBufferString) { + + + const time::Span maxCoreSolverTime(MaxCoreSolverTime); + maxInstructionTime = time::Span(MaxInstructionTime); + coreSolverTimeout = maxCoreSolverTime && maxInstructionTime ? + std::min(maxCoreSolverTime, maxInstructionTime) + : std::max(maxCoreSolverTime, maxInstructionTime); if (coreSolverTimeout) UseForkedCoreSolver = true; Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse); @@ -779,7 +780,7 @@ Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { if (!isSeeding && !isa<ConstantExpr>(condition) && (MaxStaticForkPct!=1. || MaxStaticSolvePct != 1. || MaxStaticCPForkPct!=1. || MaxStaticCPSolvePct != 1.) && - statsTracker->elapsed() > 60.) { + statsTracker->elapsed() > time::seconds(60)) { StatisticManager &sm = *theStatisticManager; CallPathNode *cpn = current.stack.back().callPathNode; if ((MaxStaticForkPct<1. && @@ -803,12 +804,12 @@ Executor::fork(ExecutionState ¤t, ref<Expr> condition, bool isInternal) { } } - double timeout = coreSolverTimeout; + time::Span timeout = coreSolverTimeout; if (isSeeding) timeout *= it->second.size(); solver->setTimeout(timeout); bool success = solver->evaluate(current, condition, res); - solver->setTimeout(0); + solver->setTimeout(time::Span()); if (!success) { current.pc = current.prevPC; terminateStateEarly(current, "Query timed out (fork)."); @@ -1076,7 +1077,7 @@ ref<Expr> Executor::toUnique(const ExecutionState &state, if (solver->mustBeTrue(state, cond, isTrue) && isTrue) result = value; } - solver->setTimeout(0); + solver->setTimeout(time::Span()); } return result; @@ -2774,7 +2775,7 @@ void Executor::run(ExecutionState &initialState) { v.push_back(SeedInfo(*it)); int lastNumSeeds = usingSeeds->size()+10; - double lastTime, startTime = lastTime = util::getWallTime(); + time::Point lastTime, startTime = lastTime = time::getWallTime(); ExecutionState *lastState = 0; while (!seedMap.empty()) { if (haltExecution) { @@ -2793,7 +2794,7 @@ void Executor::run(ExecutionState &initialState) { stepInstruction(state); executeInstruction(state, ki); - processTimers(&state, MaxInstructionTime * numSeeds); + processTimers(&state, maxInstructionTime * numSeeds); updateStates(&state); if ((stats::instructions % 1000) == 0) { @@ -2804,13 +2805,14 @@ void Executor::run(ExecutionState &initialState) { numSeeds += it->second.size(); numStates++; } - double time = util::getWallTime(); - if (SeedTime>0. && time > startTime + SeedTime) { + const auto time = time::getWallTime(); + const time::Span seedTime(SeedTime); + if (seedTime && time > startTime + seedTime) { klee_warning("seed time expired, %d seeds remain over %d states", numSeeds, numStates); break; } else if (numSeeds<=lastNumSeeds-10 || - time >= lastTime+10) { + time - lastTime >= time::seconds(10)) { lastTime = time; lastNumSeeds = numSeeds; klee_message("%d seeds remaining over: %d states", @@ -2846,7 +2848,7 @@ void Executor::run(ExecutionState &initialState) { stepInstruction(state); executeInstruction(state, ki); - processTimers(&state, MaxInstructionTime); + processTimers(&state, maxInstructionTime); checkMemoryUsage(); @@ -3457,7 +3459,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, address = toConstant(state, address, "resolveOne failure"); success = state.addressSpace.resolveOne(cast<ConstantExpr>(address), op); } - solver->setTimeout(0); + solver->setTimeout(time::Span()); if (success) { const MemoryObject *mo = op.first; @@ -3473,7 +3475,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, bool inBounds; solver->setTimeout(coreSolverTimeout); bool success = solver->mustBeTrue(state, check, inBounds); - solver->setTimeout(0); + solver->setTimeout(time::Span()); if (!success) { state.pc = state.prevPC; terminateStateEarly(state, "Query timed out (bounds check)."); @@ -3511,7 +3513,7 @@ void Executor::executeMemoryOperation(ExecutionState &state, solver->setTimeout(coreSolverTimeout); bool incomplete = state.addressSpace.resolve(state, solver, address, rl, 0, coreSolverTimeout); - solver->setTimeout(0); + solver->setTimeout(time::Span()); // XXX there is some query wasteage here. who cares? ExecutionState *unbound = &state; @@ -3827,7 +3829,7 @@ bool Executor::getSymbolicSolution(const ExecutionState &state, for (unsigned i = 0; i != state.symbolics.size(); ++i) objects.push_back(state.symbolics[i].second); bool success = solver->getInitialValues(tmp, objects, values); - solver->setTimeout(0); + solver->setTimeout(time::Span()); if (!success) { klee_warning("unable to compute initial values (invalid constraints?)!"); ExprPPrinter::printQuery(llvm::errs(), state.constraints, diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index 3643c3f4..180c9140 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -20,6 +20,7 @@ #include "klee/Internal/Module/Cell.h" #include "klee/Internal/Module/KInstruction.h" #include "klee/Internal/Module/KModule.h" +#include "klee/Internal/System/Time.h" #include "klee/util/ArrayCache.h" #include "llvm/Support/raw_ostream.h" @@ -216,7 +217,10 @@ private: /// The maximum time to allow for a single core solver query. /// (e.g. for a single STP query) - double coreSolverTimeout; + time::Span coreSolverTimeout; + + /// Maximum time to allow for a single instruction. + time::Span maxInstructionTime; /// Assumes ownership of the created array objects ArrayCache arrayCache; @@ -461,11 +465,10 @@ private: /// /// \param timer The timer object to run on firings. /// \param rate The approximate delay (in seconds) between firings. - void addTimer(Timer *timer, double rate); + void addTimer(Timer *timer, time::Span rate); void initTimers(); - void processTimers(ExecutionState *current, - double maxInstTime); + void processTimers(ExecutionState *current, time::Span maxInstTime); void checkMemoryUsage(); void printDebugInstructions(ExecutionState &state); void doDumpStates(); diff --git a/lib/Core/ExecutorTimerInfo.h b/lib/Core/ExecutorTimerInfo.h index 60977b74..9127fb68 100644 --- a/lib/Core/ExecutorTimerInfo.h +++ b/lib/Core/ExecutorTimerInfo.h @@ -23,15 +23,15 @@ public: Timer *timer; /// Approximate delay per timer firing. - double rate; + time::Span rate; /// Wall time for next firing. - double nextFireTime; + time::Point nextFireTime; public: - TimerInfo(Timer *_timer, double _rate) + TimerInfo(Timer *_timer, time::Span _rate) : timer(_timer), rate(_rate), - nextFireTime(util::getWallTime() + rate) {} + nextFireTime(time::getWallTime() + rate) {} ~TimerInfo() { delete timer; } }; diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp index a3c13530..de24d75d 100644 --- a/lib/Core/ExecutorTimers.cpp +++ b/lib/Core/ExecutorTimers.cpp @@ -23,6 +23,7 @@ #include "llvm/IR/Function.h" #include "llvm/Support/CommandLine.h" +#include <string> #include <unistd.h> #include <signal.h> #include <sys/time.h> @@ -32,10 +33,9 @@ using namespace llvm; using namespace klee; -cl::opt<double> +cl::opt<std::string> MaxTime("max-time", - cl::desc("Halt execution after the specified number of seconds (default=0 (off))"), - cl::init(0)); + cl::desc("Halt execution after the specified number of seconds (default=0s (off))")); /// @@ -54,7 +54,7 @@ public: /// -static const double kSecondsPerTick = .1; +static const time::Span kMilliSecondsPerTick(time::milliseconds(100)); static volatile unsigned timerTicks = 0; // XXX hack @@ -67,15 +67,11 @@ static void onAlarm(int) { // oooogalay static void setupHandler() { - struct itimerval t; - struct timeval tv; - - tv.tv_sec = (long) kSecondsPerTick; - tv.tv_usec = (long) (fmod(kSecondsPerTick, 1.)*1000000); - + itimerval t{}; + timeval tv = static_cast<timeval>(kMilliSecondsPerTick); t.it_interval = t.it_value = tv; - - ::setitimer(ITIMER_REAL, &t, 0); + + ::setitimer(ITIMER_REAL, &t, nullptr); ::signal(SIGALRM, onAlarm); } @@ -87,8 +83,9 @@ void Executor::initTimers() { setupHandler(); } - if (MaxTime) { - addTimer(new HaltTimer(this), MaxTime.getValue()); + const time::Span maxTime(MaxTime); + if (maxTime) { + addTimer(new HaltTimer(this), maxTime); } } @@ -98,12 +95,12 @@ Executor::Timer::Timer() {} Executor::Timer::~Timer() {} -void Executor::addTimer(Timer *timer, double rate) { +void Executor::addTimer(Timer *timer, time::Span rate) { timers.push_back(new TimerInfo(timer, rate)); } void Executor::processTimers(ExecutionState *current, - double maxInstTime) { + time::Span maxInstTime) { static unsigned callsWithoutCheck = 0; unsigned ticks = timerTicks; @@ -169,18 +166,17 @@ void Executor::processTimers(ExecutionState *current, dumpStates = 0; } - if (maxInstTime > 0 && current && + if (maxInstTime && current && std::find(removedStates.begin(), removedStates.end(), current) == removedStates.end()) { - if (timerTicks*kSecondsPerTick > maxInstTime) { - klee_warning("max-instruction-time exceeded: %.2fs", - timerTicks*kSecondsPerTick); + if (timerTicks*kMilliSecondsPerTick > maxInstTime) { + klee_warning("max-instruction-time exceeded: %.2fs", (timerTicks * kMilliSecondsPerTick).toSeconds()); terminateStateEarly(*current, "max-instruction-time exceeded"); } } if (!timers.empty()) { - double time = util::getWallTime(); + auto time = time::getWallTime(); for (std::vector<TimerInfo*>::iterator it = timers.begin(), ie = timers.end(); it != ie; ++it) { 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(); diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index 47026410..dc0e12a4 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -10,11 +10,14 @@ #ifndef KLEE_SEARCHER_H #define KLEE_SEARCHER_H +#include "klee/Internal/System/Time.h" + #include "llvm/Support/raw_ostream.h" -#include <vector> -#include <set> + #include <map> #include <queue> +#include <set> +#include <vector> namespace llvm { class BasicBlock; @@ -208,16 +211,16 @@ namespace klee { class BatchingSearcher : public Searcher { Searcher *baseSearcher; - double timeBudget; + time::Span timeBudget; unsigned instructionBudget; ExecutionState *lastState; - double lastStartTime; + time::Point lastStartTime; unsigned lastStartInstructions; public: BatchingSearcher(Searcher *baseSearcher, - double _timeBudget, + time::Span _timeBudget, unsigned _instructionBudget); ~BatchingSearcher(); @@ -237,7 +240,8 @@ namespace klee { class IterativeDeepeningTimeSearcher : public Searcher { Searcher *baseSearcher; - double time, startTime; + time::Point startTime; + time::Span time; std::set<ExecutionState*> pausedStates; public: diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp index dee14e61..5ad0f174 100644 --- a/lib/Core/StatsTracker.cpp +++ b/lib/Core/StatsTracker.cpp @@ -17,7 +17,6 @@ #include "klee/Internal/Module/KInstruction.h" #include "klee/Internal/Support/ModuleUtil.h" #include "klee/Internal/System/MemoryUsage.h" -#include "klee/Internal/System/Time.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/SolverStats.h" @@ -71,20 +70,20 @@ namespace { cl::init(true), cl::desc("Write instruction level statistics in callgrind format (default=on)")); - cl::opt<double> + cl::opt<std::string> StatsWriteInterval("stats-write-interval", - cl::init(1.), - cl::desc("Approximate number of seconds between stats writes (default=1.0s)")); + cl::init("1s"), + cl::desc("Approximate time between stats writes (default=1s)")); cl::opt<unsigned> StatsWriteAfterInstructions( "stats-write-after-instructions", cl::init(0), cl::desc("Write statistics after each n instructions, 0 to disable " "(default=0)")); - cl::opt<double> + cl::opt<std::string> IStatsWriteInterval("istats-write-interval", - cl::init(10.), - cl::desc("Approximate number of seconds between istats writes (default: 10.0s)")); + cl::init("10s"), + cl::desc("Approximate number of seconds between istats writes (default=10s)")); cl::opt<unsigned> IStatsWriteAfterInstructions( "istats-write-after-instructions", cl::init(0), @@ -92,10 +91,10 @@ namespace { "(default=0)")); // XXX I really would like to have dynamic rate control for something like this. - cl::opt<double> + cl::opt<std::string> UncoveredUpdateInterval("uncovered-update-interval", - cl::init(30.), - cl::desc("(default=30.0s)")); + cl::init("30s"), + cl::desc("(default=30s)")); cl::opt<bool> UseCallPaths("use-call-paths", @@ -176,18 +175,20 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename, bool _updateMinDistToUncovered) : executor(_executor), objectFilename(_objectFilename), - startWallTime(util::getWallTime()), + startWallTime(time::getWallTime()), numBranches(0), fullBranches(0), partialBranches(0), updateMinDistToUncovered(_updateMinDistToUncovered) { - if (StatsWriteAfterInstructions > 0 && StatsWriteInterval > 0) + const time::Span statsWriteInterval(StatsWriteInterval); + if (StatsWriteAfterInstructions > 0 && statsWriteInterval) klee_error("Both options --stats-write-interval and " "--stats-write-after-instructions cannot be enabled at the same " "time."); - if (IStatsWriteAfterInstructions > 0 && IStatsWriteInterval > 0) + const time::Span iStatsWriteInterval(IStatsWriteInterval); + if (IStatsWriteAfterInstructions > 0 && iStatsWriteInterval) klee_error( "Both options --istats-write-interval and " "--istats-write-after-instructions cannot be enabled at the same " @@ -245,8 +246,8 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename, writeStatsHeader(); writeStatsLine(); - if (StatsWriteInterval > 0) - executor.addTimer(new WriteStatsTimer(this), StatsWriteInterval); + if (statsWriteInterval) + executor.addTimer(new WriteStatsTimer(this), statsWriteInterval); } else { klee_error("Unable to open statistics trace file (run.stats)."); } @@ -255,14 +256,14 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename, // Add timer to calculate uncovered instructions if needed by the solver if (updateMinDistToUncovered) { computeReachableUncovered(); - executor.addTimer(new UpdateReachableTimer(this), UncoveredUpdateInterval); + executor.addTimer(new UpdateReachableTimer(this), time::Span(UncoveredUpdateInterval)); } if (OutputIStats) { istatsFile = executor.interpreterHandler->openOutputFile("run.istats"); if (istatsFile) { - if (IStatsWriteInterval > 0) - executor.addTimer(new WriteIStatsTimer(this), IStatsWriteInterval); + if (iStatsWriteInterval) + executor.addTimer(new WriteIStatsTimer(this), iStatsWriteInterval); } else { klee_error("Unable to open instruction level stats file (run.istats)."); } @@ -284,45 +285,21 @@ void StatsTracker::done() { void StatsTracker::stepInstruction(ExecutionState &es) { if (OutputIStats) { if (TrackInstructionTime) { -#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0) - static sys::TimePoint<> lastNowTime; - static std::chrono::nanoseconds lastUserTime(0); + static time::Point lastNowTime(time::getWallTime()); + static time::Span lastUserTime; - if (lastUserTime.count() == 0) { - std::chrono::nanoseconds sys; - sys::Process::GetTimeUsage(lastNowTime, lastUserTime, sys); + if (!lastUserTime) { + lastUserTime = time::getUserTime(); } else { - sys::TimePoint<> now; - std::chrono::nanoseconds user, sys; - - sys::Process::GetTimeUsage(now, user, sys); - - auto delta = - std::chrono::duration_cast<std::chrono::microseconds>(user - lastUserTime); - auto deltaNow = - std::chrono::duration_cast<std::chrono::microseconds>(now - lastNowTime); - stats::instructionTime += delta.count(); - stats::instructionRealTime += deltaNow.count(); + const auto now = time::getWallTime(); + const auto user = time::getUserTime(); + const auto delta = user - lastUserTime; + const auto deltaNow = now - lastNowTime; + stats::instructionTime += delta.toMicroseconds(); + stats::instructionRealTime += deltaNow.toMicroseconds(); lastUserTime = user; lastNowTime = now; } -#else - static sys::TimeValue lastNowTime(0,0),lastUserTime(0,0); - - if (lastUserTime.seconds()==0 && lastUserTime.nanoseconds()==0) { - sys::TimeValue sys(0,0); - sys::Process::GetTimeUsage(lastNowTime,lastUserTime,sys); - } else { - sys::TimeValue now(0,0),user(0,0),sys(0,0); - sys::Process::GetTimeUsage(now,user,sys); - sys::TimeValue delta = user - lastUserTime; - sys::TimeValue deltaNow = now - lastNowTime; - stats::instructionTime += delta.usec(); - stats::instructionRealTime += deltaNow.usec(); - lastUserTime = user; - lastNowTime = now; - } -#endif } Instruction *inst = es.pc->inst; @@ -447,8 +424,8 @@ void StatsTracker::writeStatsHeader() { statsFile->flush(); } -double StatsTracker::elapsed() { - return util::getWallTime() - startWallTime; +time::Span StatsTracker::elapsed() { + return time::getWallTime() - startWallTime; } void StatsTracker::writeStatsLine() { @@ -456,24 +433,24 @@ void StatsTracker::writeStatsLine() { << "," << fullBranches << "," << partialBranches << "," << numBranches - << "," << util::getUserTime() + << "," << time::getUserTime().toSeconds() << "," << executor.states.size() << "," << util::GetTotalMallocUsage() + executor.memory->getUsedDeterministicSize() << "," << stats::queries << "," << stats::queryConstructs << "," << 0 // was numObjects - << "," << elapsed() + << "," << elapsed().toSeconds() << "," << stats::coveredInstructions << "," << stats::uncoveredInstructions - << "," << stats::queryTime / 1000000. - << "," << stats::solverTime / 1000000. - << "," << stats::cexCacheTime / 1000000. - << "," << stats::forkTime / 1000000. - << "," << stats::resolveTime / 1000000. + << "," << time::microseconds(stats::queryTime).toSeconds() + << "," << time::microseconds(stats::solverTime).toSeconds() + << "," << time::microseconds(stats::cexCacheTime).toSeconds() + << "," << time::microseconds(stats::forkTime).toSeconds() + << "," << time::microseconds(stats::resolveTime).toSeconds() << "," << stats::queryCexCacheMisses << "," << stats::queryCexCacheHits #ifdef KLEE_ARRAY_DEBUG - << "," << stats::arrayHashTime / 1000000. + << "," << time::microseconds(stats::arrayHashTime).toSeconds() #endif << ")\n"; statsFile->flush(); diff --git a/lib/Core/StatsTracker.h b/lib/Core/StatsTracker.h index e352bb91..88e4cf30 100644 --- a/lib/Core/StatsTracker.h +++ b/lib/Core/StatsTracker.h @@ -11,6 +11,7 @@ #define KLEE_STATSTRACKER_H #include "CallPathManager.h" +#include "klee/Internal/System/Time.h" #include <memory> #include <set> @@ -38,7 +39,7 @@ namespace klee { std::string objectFilename; std::unique_ptr<llvm::raw_fd_ostream> statsFile, istatsFile; - double startWallTime; + time::Point startWallTime; unsigned numBranches; unsigned fullBranches, partialBranches; @@ -81,8 +82,8 @@ namespace klee { // about to be stepped void stepInstruction(ExecutionState &es); - /// Return time in seconds since execution start. - double elapsed(); + /// Return duration since execution start. + time::Span elapsed(); void computeReachableUncovered(); }; diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp index 3b66f641..0f69509a 100644 --- a/lib/Core/TimingSolver.cpp +++ b/lib/Core/TimingSolver.cpp @@ -37,7 +37,7 @@ bool TimingSolver::evaluate(const ExecutionState& state, ref<Expr> expr, bool success = solver->evaluate(Query(state.constraints, expr), result); - state.queryCost += timer.check() / 1e6; + state.queryCost += timer.check(); return success; } @@ -57,7 +57,7 @@ bool TimingSolver::mustBeTrue(const ExecutionState& state, ref<Expr> expr, bool success = solver->mustBeTrue(Query(state.constraints, expr), result); - state.queryCost += timer.check() / 1e6; + state.queryCost += timer.check(); return success; } @@ -100,7 +100,7 @@ bool TimingSolver::getValue(const ExecutionState& state, ref<Expr> expr, bool success = solver->getValue(Query(state.constraints, expr), result); - state.queryCost += timer.check() / 1e6; + state.queryCost += timer.check(); return success; } @@ -120,7 +120,7 @@ TimingSolver::getInitialValues(const ExecutionState& state, ConstantExpr::alloc(0, Expr::Bool)), objects, result); - state.queryCost += timer.check() / 1e6; + state.queryCost += timer.check(); return success; } diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h index c98dd881..08ed0de2 100644 --- a/lib/Core/TimingSolver.h +++ b/lib/Core/TimingSolver.h @@ -12,6 +12,7 @@ #include "klee/Expr.h" #include "klee/Solver.h" +#include "klee/Internal/System/Time.h" #include <vector> @@ -38,7 +39,7 @@ namespace klee { delete solver; } - void setTimeout(double t) { + void setTimeout(time::Span t) { solver->setCoreSolverTimeout(t); } diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index aa90c401..934cef54 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -51,10 +51,10 @@ namespace { cl::desc("Number of instructions to batch when using --use-batching-search"), cl::init(10000)); - cl::opt<double> + cl::opt<std::string> BatchTime("batch-time", - cl::desc("Amount of time to batch when using --use-batching-search"), - cl::init(5.0)); + cl::desc("Amount of time to batch when using --use-batching-search (default=5s)"), + cl::init("5s")); } @@ -120,7 +120,7 @@ Searcher *klee::constructUserSearcher(Executor &executor) { } if (UseBatchingSearch) { - searcher = new BatchingSearcher(searcher, BatchTime, BatchInstructions); + searcher = new BatchingSearcher(searcher, time::Span(BatchTime), BatchInstructions); } if (UseMerge && UseIncompleteMerge) { diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp index a4d97f54..82702dbf 100644 --- a/lib/Solver/AssignmentValidatingSolver.cpp +++ b/lib/Solver/AssignmentValidatingSolver.cpp @@ -32,7 +32,7 @@ public: bool &hasSolution); SolverRunStatus getOperationStatusCode(); char *getConstraintLog(const Query &); - void setCoreSolverTimeout(double timeout); + void setCoreSolverTimeout(time::Span timeout); }; // TODO: use computeInitialValues for all queries for more stress testing @@ -148,7 +148,7 @@ char *AssignmentValidatingSolver::getConstraintLog(const Query &query) { return solver->impl->getConstraintLog(query); } -void AssignmentValidatingSolver::setCoreSolverTimeout(double timeout) { +void AssignmentValidatingSolver::setCoreSolverTimeout(time::Span timeout) { return solver->impl->setCoreSolverTimeout(timeout); } diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index 1a6dce52..be46621b 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -93,7 +93,7 @@ public: } SolverRunStatus getOperationStatusCode(); char *getConstraintLog(const Query&); - void setCoreSolverTimeout(double timeout); + void setCoreSolverTimeout(time::Span timeout); }; /** @returns the canonical version of the given query. The reference @@ -257,7 +257,7 @@ char *CachingSolver::getConstraintLog(const Query& query) { return solver->impl->getConstraintLog(query); } -void CachingSolver::setCoreSolverTimeout(double timeout) { +void CachingSolver::setCoreSolverTimeout(time::Span timeout) { solver->impl->setCoreSolverTimeout(timeout); } diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index 8627b2ac..f4ee009c 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -91,7 +91,7 @@ public: bool &hasSolution); SolverRunStatus getOperationStatusCode(); char *getConstraintLog(const Query& query); - void setCoreSolverTimeout(double timeout); + void setCoreSolverTimeout(time::Span timeout); }; /// @@ -371,7 +371,7 @@ char *CexCachingSolver::getConstraintLog(const Query& query) { return solver->impl->getConstraintLog(query); } -void CexCachingSolver::setCoreSolverTimeout(double timeout) { +void CexCachingSolver::setCoreSolverTimeout(time::Span timeout) { solver->impl->setCoreSolverTimeout(timeout); } diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp index dc2c9fd4..72fe2a95 100644 --- a/lib/Solver/IncompleteSolver.cpp +++ b/lib/Solver/IncompleteSolver.cpp @@ -143,7 +143,7 @@ char *StagedSolverImpl::getConstraintLog(const Query& query) { return secondary->impl->getConstraintLog(query); } -void StagedSolverImpl::setCoreSolverTimeout(double timeout) { +void StagedSolverImpl::setCoreSolverTimeout(time::Span timeout) { secondary->impl->setCoreSolverTimeout(timeout); } diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 3594fecf..19a0d745 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -408,7 +408,7 @@ public: bool &hasSolution); SolverRunStatus getOperationStatusCode(); char *getConstraintLog(const Query&); - void setCoreSolverTimeout(double timeout); + void setCoreSolverTimeout(time::Span timeout); }; bool IndependentSolver::computeValidity(const Query& query, @@ -555,7 +555,7 @@ char *IndependentSolver::getConstraintLog(const Query& query) { return solver->impl->getConstraintLog(query); } -void IndependentSolver::setCoreSolverTimeout(double timeout) { +void IndependentSolver::setCoreSolverTimeout(time::Span timeout) { solver->impl->setCoreSolverTimeout(timeout); } diff --git a/lib/Solver/KQueryLoggingSolver.cpp b/lib/Solver/KQueryLoggingSolver.cpp index 8dc98ac5..0c2ac6dd 100644 --- a/lib/Solver/KQueryLoggingSolver.cpp +++ b/lib/Solver/KQueryLoggingSolver.cpp @@ -11,6 +11,7 @@ #include "klee/Expr.h" #include "klee/util/ExprPPrinter.h" +#include "klee/Internal/System/Time.h" using namespace klee; @@ -49,8 +50,8 @@ private : } public: - KQueryLoggingSolver(Solver *_solver, std::string path, int queryTimeToLog) - : QueryLoggingSolver(_solver, path, "#", queryTimeToLog), + KQueryLoggingSolver(Solver *_solver, std::string path, time::Span queryTimeToLog, bool logTimedOut) + : QueryLoggingSolver(_solver, path, "#", queryTimeToLog, logTimedOut), printer(ExprPPrinter::create(logBuffer)) { } @@ -62,7 +63,7 @@ public: /// Solver *klee::createKQueryLoggingSolver(Solver *_solver, std::string path, - int minQueryTimeToLog) { - return new Solver(new KQueryLoggingSolver(_solver, path, minQueryTimeToLog)); + time::Span minQueryTimeToLog, bool logTimedOut) { + return new Solver(new KQueryLoggingSolver(_solver, path, minQueryTimeToLog, logTimedOut)); } diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index 695c408b..b58319c2 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -77,7 +77,7 @@ private: SolverContext _meta_solver; MetaSMTSolver<SolverContext> *_solver; MetaSMTBuilder<SolverContext> *_builder; - double _timeout; + time::Span _timeout; bool _useForked; SolverRunStatus _runStatusCode; @@ -87,7 +87,7 @@ public: virtual ~MetaSMTSolverImpl(); char *getConstraintLog(const Query &); - void setCoreSolverTimeout(double timeout) { _timeout = timeout; } + void setCoreSolverTimeout(time::Span timeout) { _timeout = timeout; } bool computeTruth(const Query &, bool &isValid); bool computeValue(const Query &, ref<Expr> &result); @@ -106,7 +106,7 @@ public: runAndGetCexForked(const Query &query, const std::vector<const Array *> &objects, std::vector<std::vector<unsigned char> > &values, - bool &hasSolution, double timeout); + bool &hasSolution, time::Span timeout); SolverRunStatus getOperationStatusCode(); @@ -118,7 +118,7 @@ MetaSMTSolverImpl<SolverContext>::MetaSMTSolverImpl( MetaSMTSolver<SolverContext> *solver, bool useForked, bool optimizeDivides) : _solver(solver), _builder(new MetaSMTBuilder<SolverContext>( _meta_solver, optimizeDivides)), - _timeout(0.0), _useForked(useForked) { + _useForked(useForked) { assert(_solver && "unable to create MetaSMTSolver"); assert(_builder && "unable to create MetaSMTBuilder"); @@ -273,7 +273,7 @@ SolverImpl::SolverRunStatus MetaSMTSolverImpl<SolverContext>::runAndGetCexForked( const Query &query, const std::vector<const Array *> &objects, std::vector<std::vector<unsigned char> > &values, bool &hasSolution, - double timeout) { + time::Span timeout) { unsigned char *pos = shared_memory_ptr; unsigned sum = 0; for (std::vector<const Array *>::const_iterator it = objects.begin(), @@ -298,7 +298,7 @@ MetaSMTSolverImpl<SolverContext>::runAndGetCexForked( if (timeout) { ::alarm(0); /* Turn off alarm so we can safely set signal handler */ ::signal(SIGALRM, metaSMTTimeoutHandler); - ::alarm(std::max(1, (int)timeout)); + ::alarm(std::max(1u, static_cast<unsigned>(timeout.toSeconds()))); } // assert constraints as we are in a child process @@ -419,7 +419,7 @@ char *MetaSMTSolver<SolverContext>::getConstraintLog(const Query &query) { } template <typename SolverContext> -void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(double timeout) { +void MetaSMTSolver<SolverContext>::setCoreSolverTimeout(time::Span timeout) { impl->setCoreSolverTimeout(timeout); } diff --git a/lib/Solver/MetaSMTSolver.h b/lib/Solver/MetaSMTSolver.h index 60d72383..9fa93719 100644 --- a/lib/Solver/MetaSMTSolver.h +++ b/lib/Solver/MetaSMTSolver.h @@ -21,7 +21,7 @@ public: virtual ~MetaSMTSolver(); virtual char *getConstraintLog(const Query &); - virtual void setCoreSolverTimeout(double timeout); + virtual void setCoreSolverTimeout(time::Span timeout); }; /// createMetaSMTSolver - Create a solver using the metaSMT backend set by diff --git a/lib/Solver/QueryLoggingSolver.cpp b/lib/Solver/QueryLoggingSolver.cpp index 0fb145d7..9001b5c1 100644 --- a/lib/Solver/QueryLoggingSolver.cpp +++ b/lib/Solver/QueryLoggingSolver.cpp @@ -13,8 +13,6 @@ #include "klee/Internal/Support/FileHandling.h" #include "klee/Internal/System/Time.h" -using namespace klee::util; - namespace { llvm::cl::opt<bool> DumpPartialQueryiesEarly( "log-partial-queries-early", llvm::cl::init(false), @@ -29,9 +27,10 @@ llvm::cl::opt<bool> CreateCompressedQueryLog( QueryLoggingSolver::QueryLoggingSolver(Solver *_solver, std::string path, const std::string &commentSign, - int queryTimeToLog) + time::Span queryTimeToLog, + bool logTimedOut) : solver(_solver), BufferString(""), logBuffer(BufferString), queryCount(0), - minQueryTimeToLog(queryTimeToLog), startTime(0.0f), lastQueryTime(0.0f), + minQueryTimeToLog(queryTimeToLog), logTimedOutQueries(logTimedOut), queryCommentSign(commentSign) { std::string error; #ifdef HAVE_ZLIB_H @@ -79,13 +78,13 @@ void QueryLoggingSolver::startQuery(const Query &query, const char *typeName, if (DumpPartialQueryiesEarly) { flushBufferConditionally(true); } - startTime = getWallTime(); + startTime = time::getWallTime(); } void QueryLoggingSolver::finishQuery(bool success) { - lastQueryTime = getWallTime() - startTime; + lastQueryDuration = time::getWallTime() - startTime; logBuffer << queryCommentSign << " " << (success ? "OK" : "FAIL") << " -- " - << "Elapsed: " << lastQueryTime << "\n"; + << "Elapsed: " << lastQueryDuration << "\n"; if (false == success) { logBuffer << queryCommentSign << " Failure reason: " @@ -95,21 +94,13 @@ void QueryLoggingSolver::finishQuery(bool success) { } void QueryLoggingSolver::flushBuffer() { - bool writeToFile = false; - - if ((0 == minQueryTimeToLog) || - (static_cast<int>(lastQueryTime * 1000) > minQueryTimeToLog)) { - // we either do not limit logging queries or the query time - // is larger than threshold (in ms) - - if ((minQueryTimeToLog >= 0) || - (SOLVER_RUN_STATUS_TIMEOUT == - (solver->impl->getOperationStatusCode()))) { - // we do additional check here to log only timeouts in case - // user specified negative value for minQueryTimeToLog param - writeToFile = true; - } - } + // we either do not limit logging queries + // or the query time is larger than threshold + // or we log a timed out query + bool writeToFile = (!minQueryTimeToLog) + || (lastQueryDuration > minQueryTimeToLog) + || (logTimedOutQueries && + (SOLVER_RUN_STATUS_TIMEOUT == solver->impl->getOperationStatusCode())); flushBufferConditionally(writeToFile); } @@ -218,6 +209,6 @@ char *QueryLoggingSolver::getConstraintLog(const Query &query) { return solver->impl->getConstraintLog(query); } -void QueryLoggingSolver::setCoreSolverTimeout(double timeout) { +void QueryLoggingSolver::setCoreSolverTimeout(time::Span timeout) { solver->impl->setCoreSolverTimeout(timeout); } 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 */ diff --git a/lib/Solver/SMTLIBLoggingSolver.cpp b/lib/Solver/SMTLIBLoggingSolver.cpp index 2f3e97da..f734ac38 100644 --- a/lib/Solver/SMTLIBLoggingSolver.cpp +++ b/lib/Solver/SMTLIBLoggingSolver.cpp @@ -43,9 +43,10 @@ class SMTLIBLoggingSolver : public QueryLoggingSolver public: SMTLIBLoggingSolver(Solver *_solver, - std::string path, - int queryTimeToLog) - : QueryLoggingSolver(_solver, path, ";", queryTimeToLog) + std::string path, + time::Span queryTimeToLog, + bool logTimedOut) + : QueryLoggingSolver(_solver, path, ";", queryTimeToLog, logTimedOut) { //Setup the printer printer.setOutput(logBuffer); @@ -54,7 +55,7 @@ class SMTLIBLoggingSolver : public QueryLoggingSolver Solver* klee::createSMTLIBLoggingSolver(Solver *_solver, std::string path, - int minQueryTimeToLog) + time::Span minQueryTimeToLog, bool logTimedOut) { - return new Solver(new SMTLIBLoggingSolver(_solver, path, minQueryTimeToLog)); + return new Solver(new SMTLIBLoggingSolver(_solver, path, minQueryTimeToLog, logTimedOut)); } diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index d1b8cbdc..6081ff95 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -65,7 +65,7 @@ class STPSolverImpl : public SolverImpl { private: VC vc; STPBuilder *builder; - double timeout; + time::Span timeout; bool useForkedSTP; SolverRunStatus runStatusCode; @@ -74,7 +74,7 @@ public: ~STPSolverImpl(); char *getConstraintLog(const Query &); - void setCoreSolverTimeout(double _timeout) { timeout = _timeout; } + void setCoreSolverTimeout(time::Span timeout) { this->timeout = timeout; } bool computeTruth(const Query &, bool &isValid); bool computeValue(const Query &, ref<Expr> &result); @@ -87,7 +87,7 @@ public: STPSolverImpl::STPSolverImpl(bool _useForkedSTP, bool _optimizeDivides) : vc(vc_createValidityChecker()), - builder(new STPBuilder(vc, _optimizeDivides)), timeout(0.0), + builder(new STPBuilder(vc, _optimizeDivides)), useForkedSTP(_useForkedSTP), runStatusCode(SOLVER_RUN_STATUS_FAILURE) { assert(vc && "unable to create validity checker"); assert(builder && "unable to create STPBuilder"); @@ -219,7 +219,7 @@ static SolverImpl::SolverRunStatus runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q, const std::vector<const Array *> &objects, std::vector<std::vector<unsigned char> > &values, - bool &hasSolution, double timeout) { + bool &hasSolution, time::Span timeout) { unsigned char *pos = shared_memory_ptr; unsigned sum = 0; for (std::vector<const Array *>::const_iterator it = objects.begin(), @@ -243,7 +243,7 @@ runAndGetCexForked(::VC vc, STPBuilder *builder, ::VCExpr q, if (timeout) { ::alarm(0); /* Turn off alarm so we can safely set signal handler */ ::signal(SIGALRM, stpTimeoutHandler); - ::alarm(std::max(1, (int)timeout)); + ::alarm(std::max(1u, static_cast<unsigned>(timeout.toSeconds()))); } unsigned res = vc_query(vc, q); if (!res) { @@ -326,7 +326,6 @@ bool STPSolverImpl::computeInitialValues( const Query &query, const std::vector<const Array *> &objects, std::vector<std::vector<unsigned char> > &values, bool &hasSolution) { runStatusCode = SOLVER_RUN_STATUS_FAILURE; - TimerStatIncrementer t(stats::queryTime); vc_push(vc); @@ -383,7 +382,7 @@ char *STPSolver::getConstraintLog(const Query &query) { return impl->getConstraintLog(query); } -void STPSolver::setCoreSolverTimeout(double timeout) { +void STPSolver::setCoreSolverTimeout(time::Span timeout) { impl->setCoreSolverTimeout(timeout); } } diff --git a/lib/Solver/STPSolver.h b/lib/Solver/STPSolver.h index cb68ed91..70b9aa12 100644 --- a/lib/Solver/STPSolver.h +++ b/lib/Solver/STPSolver.h @@ -32,7 +32,7 @@ public: /// setCoreSolverTimeout - Set constraint solver timeout delay to the given /// value; 0 /// is off. - virtual void setCoreSolverTimeout(double timeout); + virtual void setCoreSolverTimeout(time::Span timeout); }; } diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 3434d2ae..4f7458c5 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -29,7 +29,7 @@ char *Solver::getConstraintLog(const Query& query) { return impl->getConstraintLog(query); } -void Solver::setCoreSolverTimeout(double timeout) { +void Solver::setCoreSolverTimeout(time::Span timeout) { impl->setCoreSolverTimeout(timeout); } diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp index ef79b563..40a7c9e0 100644 --- a/lib/Solver/ValidatingSolver.cpp +++ b/lib/Solver/ValidatingSolver.cpp @@ -31,7 +31,7 @@ public: bool &hasSolution); SolverRunStatus getOperationStatusCode(); char *getConstraintLog(const Query &); - void setCoreSolverTimeout(double timeout); + void setCoreSolverTimeout(time::Span timeout); }; bool ValidatingSolver::computeTruth(const Query &query, bool &isValid) { @@ -132,7 +132,7 @@ char *ValidatingSolver::getConstraintLog(const Query &query) { return solver->impl->getConstraintLog(query); } -void ValidatingSolver::setCoreSolverTimeout(double timeout) { +void ValidatingSolver::setCoreSolverTimeout(time::Span timeout) { solver->impl->setCoreSolverTimeout(timeout); } diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index f127de9b..5efda6b6 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -47,7 +47,7 @@ namespace klee { class Z3SolverImpl : public SolverImpl { private: Z3Builder *builder; - double timeout; + time::Span timeout; SolverRunStatus runStatusCode; std::unique_ptr<llvm::raw_fd_ostream> dumpedQueriesFile; ::Z3_params solverParameters; @@ -65,12 +65,11 @@ public: ~Z3SolverImpl(); char *getConstraintLog(const Query &); - void setCoreSolverTimeout(double _timeout) { - assert(_timeout >= 0.0 && "timeout must be >= 0"); + void setCoreSolverTimeout(time::Span _timeout) { timeout = _timeout; - unsigned int timeoutInMilliSeconds = (unsigned int)((timeout * 1000) + 0.5); - if (timeoutInMilliSeconds == 0) + auto timeoutInMilliSeconds = static_cast<unsigned>((timeout.toMicroseconds() / 1000)); + if (!timeoutInMilliSeconds) timeoutInMilliSeconds = UINT_MAX; Z3_params_set_uint(builder->ctx, solverParameters, timeoutParamStrSymbol, timeoutInMilliSeconds); @@ -96,7 +95,7 @@ Z3SolverImpl::Z3SolverImpl() /*z3LogInteractionFileArg=*/Z3LogInteractionFile.size() > 0 ? Z3LogInteractionFile.c_str() : NULL)), - timeout(0.0), runStatusCode(SOLVER_RUN_STATUS_FAILURE) { + runStatusCode(SOLVER_RUN_STATUS_FAILURE) { assert(builder && "unable to create Z3Builder"); solverParameters = Z3_mk_params(builder->ctx); Z3_params_inc_ref(builder->ctx, solverParameters); @@ -134,7 +133,7 @@ char *Z3Solver::getConstraintLog(const Query &query) { return impl->getConstraintLog(query); } -void Z3Solver::setCoreSolverTimeout(double timeout) { +void Z3Solver::setCoreSolverTimeout(time::Span timeout) { impl->setCoreSolverTimeout(timeout); } diff --git a/lib/Solver/Z3Solver.h b/lib/Solver/Z3Solver.h index 105c7c75..bed74b88 100644 --- a/lib/Solver/Z3Solver.h +++ b/lib/Solver/Z3Solver.h @@ -27,7 +27,7 @@ public: /// setCoreSolverTimeout - Set constraint solver timeout delay to the given /// value; 0 /// is off. - virtual void setCoreSolverTimeout(double timeout); + virtual void setCoreSolverTimeout(time::Span timeout); }; } diff --git a/lib/Support/Time.cpp b/lib/Support/Time.cpp index f508e6fa..7cd9659b 100644 --- a/lib/Support/Time.cpp +++ b/lib/Support/Time.cpp @@ -7,58 +7,193 @@ // //===----------------------------------------------------------------------===// -#include "klee/Config/Version.h" +#include "klee/Internal/Support/ErrorHandling.h" #include "klee/Internal/System/Time.h" -#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0) -#include <chrono> -#include <llvm/Support/Chrono.h> -#else -#include "llvm/Support/TimeValue.h" -#endif +#include <cstdint> +#include <regex> +#include <sstream> +#include <tuple> +#include <sys/resource.h> -#include "llvm/Support/Process.h" -using namespace llvm; using namespace klee; -#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0) -double util::durationToDouble(std::chrono::nanoseconds dur) -{ - return dur.count() / 1e9; + +/* Why std::chrono: + * - C++11 + * - separation between time points and durations + * - good performance on Linux and macOS (similar to gettimeofday) + * and not: + * - clock_gettime(CLOCK_MONOTONIC_COARSE): software clock, Linux-specific + * - clock_gettime(CLOCK_MONOTONIC): slowest on macOS, C-like API + * - gettimeofday: C-like API, non-monotonic + * + * TODO: add time literals with C++14 + */ + +// === Point === + +// operators +time::Point& time::Point::operator+=(const time::Span &span) { point += span.duration; return *this; } +time::Point& time::Point::operator-=(const time::Span &span) { point -= span.duration; return *this; } + +time::Point time::operator+(const time::Point &point, const time::Span &span) { return time::Point(point.point + span.duration); } +time::Point time::operator+(const time::Span &span, const time::Point &point) { return time::Point(point.point + span.duration); } +time::Point time::operator-(const time::Point &point, const time::Span &span) { return time::Point(point.point - span.duration); } +time::Span time::operator-(const time::Point &lhs, const time::Point &rhs) { return time::Span(lhs.point - rhs.point); } +bool time::operator==(const time::Point &lhs, const time::Point &rhs) { return lhs.point == rhs.point; } +bool time::operator!=(const time::Point &lhs, const time::Point &rhs) { return lhs.point != rhs.point; } +bool time::operator<(const time::Point &lhs, const time::Point &rhs) { return lhs.point < rhs.point; } +bool time::operator<=(const time::Point &lhs, const time::Point &rhs) { return lhs.point <= rhs.point; } +bool time::operator>(const time::Point &lhs, const time::Point &rhs) { return lhs.point > rhs.point; } +bool time::operator>=(const time::Point &lhs, const time::Point &rhs) { return lhs.point >= rhs.point; } + + +// === Span === + +// ctors +/// returns span from string in old (X.Y) and new (3h4min) format +time::Span::Span(const std::string &s) { + if (s.empty()) return; + + std::regex re("^([0-9]*\\.?[0-9]+)|((([0-9]+)(h|min|s|ms|us|ns))+)$", std::regex::extended); + std::regex nre("([0-9]+)(h|min|s|ms|us|ns)", std::regex::extended); + std::smatch match; + std::string submatch; + + // error + if (!std::regex_match(s, match, re)) goto error; + + // old (double) format + submatch = match[1].str(); + if (match[1].matched) { + errno = 0; + auto value = std::stod(submatch); + if (errno) goto error; + + std::chrono::duration<double> d(value); + duration = std::chrono::duration_cast<std::chrono::microseconds>(d); + } + + // new (string) format + submatch = match[2].str(); + for (std::smatch m; std::regex_search(submatch, m, nre); submatch = m.suffix()) { + errno = 0; + const auto value = std::stoull(m[1]); + if (errno) goto error; + + Duration d; + if (m[2] == "h") d = std::chrono::hours(value); + else if (m[2] == "min") d = std::chrono::minutes(value); + else if (m[2] == "s") d = std::chrono::seconds(value); + else if (m[2] == "ms") d = std::chrono::milliseconds(value); + else if (m[2] == "us") d = std::chrono::microseconds(value); + else if (m[2] == "ns") d = std::chrono::nanoseconds(value); + else goto error; + + duration += d; + } + + return; + +error: + klee_error("Illegal number format: %s", s.c_str()); } -double util::getUserTime() { - sys::TimePoint<> now; - std::chrono::nanoseconds user, sys; +// operators +time::Span& time::Span::operator=(const time::Duration &d) { duration = d; return *this; }; +time::Span& time::Span::operator+=(const time::Span &other) { duration += other.duration; return *this; } +time::Span& time::Span::operator-=(const time::Span &other) { duration -= other.duration; return *this; } +time::Span& time::Span::operator*=(const time::Duration::rep &rep) { duration *= rep; return *this; } + +time::Span time::operator+(const time::Span &lhs, const time::Span &rhs) { return time::Span(lhs.duration + rhs.duration); } +time::Span time::operator-(const time::Span &lhs, const time::Span &rhs) { return time::Span(lhs.duration - rhs.duration); } +time::Span time::operator*(const time::Span &span, const time::Duration::rep &rep) { return time::Span(span.duration * rep); } +time::Span time::operator*(const time::Duration::rep &rep, const time::Span &span) { return time::Span(span.duration * rep); } +time::Span time::operator/(const time::Span &span, const time::Duration::rep &rep) { return time::Span(span.duration / rep); } +bool time::operator==(const time::Span &lhs, const time::Span &rhs) { return lhs.duration == rhs.duration; } +bool time::operator<=(const time::Span &lhs, const time::Span &rhs) { return lhs.duration <= rhs.duration; } +bool time::operator>=(const time::Span &lhs, const time::Span &rhs) { return lhs.duration >= rhs.duration; } +bool time::operator<(const time::Span &lhs, const time::Span &rhs) { return lhs.duration < rhs.duration; } +bool time::operator>(const time::Span &lhs, const time::Span &rhs) { return lhs.duration > rhs.duration; } + +std::ostream& time::operator<<(std::ostream &stream, time::Span span) { return stream << span.toSeconds() << 's'; } +llvm::raw_ostream& time::operator<<(llvm::raw_ostream &stream, time::Span span) { return stream << span.toSeconds() << 's'; } + - sys::Process::GetTimeUsage(now, user, sys); +// units +time::Span time::hours(std::uint16_t ticks) { return time::Span(std::chrono::hours(ticks)); } +time::Span time::minutes(std::uint16_t ticks) { return time::Span(std::chrono::minutes(ticks)); } +time::Span time::seconds(std::uint64_t ticks) { return time::Span(std::chrono::seconds(ticks)); } +time::Span time::milliseconds(std::uint64_t ticks) { return time::Span(std::chrono::milliseconds(ticks)); } +time::Span time::microseconds(std::uint64_t ticks) { return time::Span(std::chrono::microseconds(ticks)); } +time::Span time::nanoseconds(std::uint64_t ticks) { return time::Span(std::chrono::nanoseconds(ticks)); } - return durationToDouble(user); + +// conversions +time::Span::operator time::Duration() const { return duration; } + +time::Span::operator bool() const { return duration.count() != 0; } + +time::Span::operator timeval() const { + timeval tv{}; + const auto secs = std::chrono::duration_cast<std::chrono::seconds>(duration); + const auto usecs = std::chrono::duration_cast<std::chrono::microseconds>(duration - secs); + tv.tv_sec = secs.count(); + tv.tv_usec = usecs.count(); + return tv; } -double util::getWallTime() { - return durationToDouble(getWallTimeVal().time_since_epoch()); +std::uint64_t time::Span::toMicroseconds() const { + return (std::uint64_t)std::chrono::duration_cast<std::chrono::microseconds>(duration).count(); } -sys::TimePoint<> util::getWallTimeVal() { - return std::chrono::system_clock::now(); +double time::Span::toSeconds() const { + return std::chrono::duration_cast<std::chrono::nanoseconds>(duration).count() / (double)1000000000; } -#else -double util::getUserTime() { - sys::TimeValue now(0,0),user(0,0),sys(0,0); - sys::Process::GetTimeUsage(now,user,sys); - return (user.seconds() + (double) user.nanoseconds() * 1e-9); +std::tuple<std::uint32_t, std::uint8_t, std::uint8_t> time::Span::toHMS() const { + auto d = duration; + const auto h = std::chrono::duration_cast<std::chrono::hours>(d); + const auto m = std::chrono::duration_cast<std::chrono::minutes>(d -= h); + const auto s = std::chrono::duration_cast<std::chrono::seconds>(d -= m); + + return std::make_tuple((std::uint32_t) h.count(), (std::uint8_t) m.count(), (std::uint8_t) s.count()); } -double util::getWallTime() { - sys::TimeValue now = getWallTimeVal(); - return (now.seconds() + ((double) now.nanoseconds() * 1e-9)); + +// methods +/// Returns information about clock +std::string time::getClockInfo() { + std::stringstream buffer; + buffer << "Using monotonic steady clock with " + << std::chrono::steady_clock::period::num + << '/' + << std::chrono::steady_clock::period::den + << "s resolution\n"; + return buffer.str(); } -sys::TimeValue util::getWallTimeVal() { - return sys::TimeValue::now(); + +/// Returns time spent by this process in user mode +time::Span time::getUserTime() { + rusage usage{}; + auto ret = ::getrusage(RUSAGE_SELF, &usage); + + if (ret) { + klee_warning("getrusage returned with error, return (0,0)"); + return {}; + } else { + return time::seconds(static_cast<std::uint64_t>(usage.ru_utime.tv_sec)) + + time::microseconds(static_cast<std::uint64_t>(usage.ru_utime.tv_usec)); + } } -#endif + + +/// Returns point in time using a monotonic steady clock +time::Point time::getWallTime() { + return time::Point(std::chrono::steady_clock::now()); +} + diff --git a/lib/Support/Timer.cpp b/lib/Support/Timer.cpp index 0e727bb4..4e52feb5 100644 --- a/lib/Support/Timer.cpp +++ b/lib/Support/Timer.cpp @@ -9,32 +9,14 @@ #include "klee/Config/Version.h" #include "klee/Internal/Support/Timer.h" - #include "klee/Internal/System/Time.h" using namespace klee; -using namespace llvm; - -#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0) WallTimer::WallTimer() { - start = util::getWallTimeVal(); + start = time::getWallTime(); } -uint64_t WallTimer::check() { - auto now = util::getWallTimeVal(); - return std::chrono::duration_cast<std::chrono::microseconds>(now - - start).count(); +time::Span WallTimer::check() { + return time::Span(time::getWallTime() - start); } - -#else - -WallTimer::WallTimer() { - startMicroseconds = util::getWallTimeVal().usec(); -} - -uint64_t WallTimer::check() { - return util::getWallTimeVal().usec() - startMicroseconds; -} - -#endif |