diff options
48 files changed, 735 insertions, 385 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(); } }; } 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 diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 3ce414a2..3ac13adb 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -216,8 +216,9 @@ static bool EvaluateInputAST(const char *Filename, Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse); if (CoreSolverToUse != DUMMY_SOLVER) { - if (0 != MaxCoreSolverTime) { - coreSolver->setCoreSolverTimeout(MaxCoreSolverTime); + const time::Span maxCoreSolverTime(MaxCoreSolverTime); + if (maxCoreSolverTime) { + coreSolver->setCoreSolverTimeout(maxCoreSolverTime); } } diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 0cbeaa96..50848bad 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -58,6 +58,7 @@ #include <sys/wait.h> #include <cerrno> +#include <ctime> #include <fstream> #include <iomanip> #include <iterator> @@ -213,7 +214,7 @@ namespace { cl::init(0)); } -extern cl::opt<double> MaxTime; +extern cl::opt<std::string> MaxTime; /***/ @@ -409,7 +410,7 @@ void KleeHandler::processTestCase(const ExecutionState &state, if (!success) klee_warning("unable to get symbolic solution, losing test case"); - double start_time = util::getWallTime(); + const auto start_time = time::getWallTime(); unsigned id = ++m_numTotalTests; @@ -515,10 +516,10 @@ void KleeHandler::processTestCase(const ExecutionState &state, m_interpreter->setHaltExecution(true); if (WriteTestInfo) { - double elapsed_time = util::getWallTime() - start_time; + time::Span elapsed_time(time::getWallTime() - start_time); auto f = openTestFile("info", id); if (f) - *f << "Time to generate test case: " << elapsed_time << "s\n"; + *f << "Time to generate test case: " << elapsed_time << '\n'; } } @@ -940,21 +941,6 @@ static void halt_via_gdb(int pid) { perror("system"); } -// returns the end of the string put in buf -static char *format_tdiff(char *buf, long seconds) -{ - assert(seconds >= 0); - - long minutes = seconds / 60; seconds %= 60; - long hours = minutes / 60; minutes %= 60; - long days = hours / 24; hours %= 24; - - buf = strrchr(buf, '\0'); - if (days > 0) buf += sprintf(buf, "%ld days, ", days); - buf += sprintf(buf, "%02ld:%02ld:%02ld", hours, minutes, seconds); - return buf; -} - #ifndef SUPPORT_KLEE_UCLIBC static void linkWithUclibc(StringRef libDir, @@ -1080,7 +1066,7 @@ int main(int argc, char **argv, char **envp) { #endif if (Watchdog) { - if (MaxTime==0) { + if (MaxTime.empty()) { klee_error("--watchdog used without --max-time"); } @@ -1092,7 +1078,8 @@ int main(int argc, char **argv, char **envp) { fflush(stderr); sys::SetInterruptFunction(interrupt_handle_watchdog); - double nextStep = util::getWallTime() + MaxTime*1.1; + const time::Span maxTime(MaxTime); + auto nextStep = time::getWallTime() + maxTime + (maxTime / 10); int level = 0; // Simple stupid code... @@ -1114,7 +1101,7 @@ int main(int argc, char **argv, char **envp) { } else if (res==pid && WIFEXITED(status)) { return WEXITSTATUS(status); } else { - double time = util::getWallTime(); + auto time = time::getWallTime(); if (time > nextStep) { ++level; @@ -1136,7 +1123,8 @@ int main(int argc, char **argv, char **envp) { // Ideally this triggers a dump, which may take a while, // so try and give the process extra time to clean up. - nextStep = util::getWallTime() + std::max(15., MaxTime*.1); + auto max = std::max(time::seconds(15), maxTime / 10); + nextStep = time::getWallTime() + max; } } } @@ -1293,12 +1281,16 @@ int main(int argc, char **argv, char **envp) { interpreter->setReplayPath(&replayPath); } - char buf[256]; - time_t t[2]; - t[0] = time(NULL); - strftime(buf, sizeof(buf), "Started: %Y-%m-%d %H:%M:%S\n", localtime(&t[0])); - handler->getInfoStream() << buf; - handler->getInfoStream().flush(); + + auto startTime = std::time(nullptr); + { // output clock info and start time + std::stringstream startInfo; + startInfo << time::getClockInfo() + << "Started: " + << std::put_time(std::localtime(&startTime), "%Y-%m-%d %H:%M:%S") << '\n'; + handler->getInfoStream() << startInfo.str(); + handler->getInfoStream().flush(); + } if (!ReplayKTestDir.empty() || !ReplayKTestFile.empty()) { assert(SeedOutFile.empty()); @@ -1396,13 +1388,24 @@ int main(int argc, char **argv, char **envp) { } } - t[1] = time(NULL); - strftime(buf, sizeof(buf), "Finished: %Y-%m-%d %H:%M:%S\n", localtime(&t[1])); - handler->getInfoStream() << buf; - - strcpy(buf, "Elapsed: "); - strcpy(format_tdiff(buf, t[1] - t[0]), "\n"); - handler->getInfoStream() << buf; + auto endTime = std::time(nullptr); + { // output end and elapsed time + std::uint32_t h; + std::uint8_t m, s; + std::tie(h,m,s) = time::seconds(endTime - startTime).toHMS(); + std::stringstream endInfo; + endInfo << "Finished: " + << std::put_time(std::localtime(&endTime), "%Y-%m-%d %H:%M:%S") << '\n' + << "Elapsed: " + << std::setfill('0') << std::setw(2) << h + << ':' + << std::setfill('0') << std::setw(2) << +m + << ':' + << std::setfill('0') << std::setw(2) << +s + << '\n'; + handler->getInfoStream() << endInfo.str(); + handler->getInfoStream().flush(); + } // Free all the args. for (unsigned i=0; i<InputArgv.size()+1; i++) diff --git a/unittests/CMakeLists.txt b/unittests/CMakeLists.txt index 00d4cbfa..d6e58183 100644 --- a/unittests/CMakeLists.txt +++ b/unittests/CMakeLists.txt @@ -86,6 +86,7 @@ add_subdirectory(Ref) add_subdirectory(Solver) add_subdirectory(TreeStream) add_subdirectory(DiscretePDF) +add_subdirectory(Time) # Set up lit configuration set (UNIT_TEST_EXE_SUFFIX "Test") diff --git a/unittests/Time/CMakeLists.txt b/unittests/Time/CMakeLists.txt new file mode 100644 index 00000000..6a860582 --- /dev/null +++ b/unittests/Time/CMakeLists.txt @@ -0,0 +1,3 @@ +add_klee_unit_test(TimeTest + TimeTest.cpp) +target_link_libraries(TimeTest PRIVATE kleeSupport) diff --git a/unittests/Time/TimeTest.cpp b/unittests/Time/TimeTest.cpp new file mode 100644 index 00000000..9caa14fd --- /dev/null +++ b/unittests/Time/TimeTest.cpp @@ -0,0 +1,165 @@ +#include "klee/Internal/System/Time.h" +#include "gtest/gtest.h" +#include "gtest/gtest-death-test.h" + +#include <cerrno> +#include <sstream> + + +int finished = 0; + +using namespace klee; + + +TEST(TimeTest, TimingFunctions) { + auto t = time::getClockInfo(); + ASSERT_STRNE(t.c_str(), ""); + + auto p0 = time::getWallTime(); + auto p1 = time::getWallTime(); + ASSERT_GT(p0, time::Point()); + ASSERT_GT(p1, time::Point()); + ASSERT_LE(p0, p1); + + time::getUserTime(); +} + + +TEST(TimeTest, TimeParserNewFormat) { + // valid + errno = 0; + auto s0 = time::Span(""); + ASSERT_EQ(s0, time::Span()); + ASSERT_EQ(errno, 0); + + s0 = time::Span("3h10min"); + ASSERT_EQ(s0, time::minutes(190)); + s0 = time::Span("5min5min"); + ASSERT_EQ(s0, time::seconds(600)); + s0 = time::Span("3us"); + ASSERT_EQ(s0, time::microseconds(3)); + s0 = time::Span("1h1min1s1ms1us1ns"); + ASSERT_EQ(s0, time::nanoseconds(3661001001001)); + s0 = time::Span("1min1min"); + ASSERT_EQ(s0, time::minutes(2)); + + // invalid + ASSERT_EXIT(time::Span("h"), ::testing::ExitedWithCode(1), "Illegal number format: h"); + ASSERT_EXIT(time::Span("-5min"), ::testing::ExitedWithCode(1), "Illegal number format: -5min"); + ASSERT_EXIT(time::Span("3.5h"), ::testing::ExitedWithCode(1), "Illegal number format: 3.5h"); + ASSERT_EXIT(time::Span("3mi"), ::testing::ExitedWithCode(1), "Illegal number format: 3mi"); +} + + +TEST(TimeTest, TimeParserOldFormat) { + // valid + errno = 0; + + auto s0 = time::Span("20"); + ASSERT_EQ(s0, time::seconds(20)); + s0 = time::Span("3.5"); + ASSERT_EQ(s0, time::milliseconds(3500)); + s0 = time::Span("0.0"); + ASSERT_EQ(s0, time::Span()); + s0 = time::Span("0"); + ASSERT_EQ(s0, time::Span()); + + ASSERT_EQ(errno, 0); + + // invalid + ASSERT_EXIT(time::Span("-3.5"), ::testing::ExitedWithCode(1), "Illegal number format: -3.5"); + ASSERT_EXIT(time::Span("NAN"), ::testing::ExitedWithCode(1), "Illegal number format: NAN"); + ASSERT_EXIT(time::Span("INF"), ::testing::ExitedWithCode(1), "Illegal number format: INF"); + ASSERT_EXIT(time::Span("foo"), ::testing::ExitedWithCode(1), "Illegal number format: foo"); +} + + +TEST(TimeTest, TimeArithmeticAndComparisons) { + auto h = time::hours(1); + auto min = time::minutes(1); + auto sec = time::seconds(1); + auto ms = time::milliseconds(1); + auto us = time::microseconds(1); + auto ns = time::nanoseconds(1); + + ASSERT_GT(h, min); + ASSERT_GT(min, sec); + ASSERT_GT(sec, ms); + ASSERT_GT(ms, us); + ASSERT_GT(us, ns); + + ASSERT_LT(min, h); + ASSERT_LT(sec, min); + ASSERT_LT(ms, sec); + ASSERT_LT(us, ms); + ASSERT_LT(ns, us); + + ASSERT_GE(h, min); + ASSERT_LE(min, h); + + auto sec2 = time::seconds(1); + ASSERT_EQ(sec, sec2); + sec2 += time::nanoseconds(1); + ASSERT_LT(sec, sec2); + + auto op0 = time::seconds(1); + auto op1 = op0 / 1000; + ASSERT_EQ(op1, ms); + op0 = time::nanoseconds(3); + op1 = op0 * 1000; + ASSERT_EQ(op1, 3*us); + + op0 = (time::seconds(10) + time::minutes(1) - time::milliseconds(10000)) * 60; + ASSERT_EQ(op0, h); + + auto p1 = time::getWallTime(); + auto p2 = p1; + p1 += time::seconds(10); + p2 -= time::seconds(15); + ASSERT_EQ(p1 - p2, time::seconds(25)); + + auto s = time::minutes(3); + p1 = s + p2; + ASSERT_NE(p1, p2); + ASSERT_LT(p2, p1); + p1 = p1 - s; + ASSERT_EQ(p1, p2); + + s = time::minutes(5); + s -= time::minutes(4); + ASSERT_EQ(s, time::seconds(60)); +} + + +TEST(TimeTest, TimeConversions) { + auto t = time::Span("3h14min1s"); + auto d = t.toSeconds(); + ASSERT_EQ(d, 11641.0); + + std::uint32_t h; + std::uint8_t m, s; + std::tie(h, m, s) = t.toHMS(); + ASSERT_EQ(h, 3u); + ASSERT_EQ(m, 14u); + ASSERT_EQ(s, 1u); + + ASSERT_TRUE((bool)t); + ASSERT_FALSE((bool)time::Span()); + + auto us = t.toMicroseconds(); + ASSERT_EQ(us, 11641000000u); + + t += time::microseconds(42); + auto v = (timeval)t; + ASSERT_EQ(v.tv_sec, 11641); + ASSERT_EQ(v.tv_usec, 42); + + t = std::chrono::seconds(1); + ASSERT_EQ(t, time::seconds(1)); + auto u = (std::chrono::steady_clock::duration)t; + ASSERT_EQ(u, std::chrono::seconds(1)); + + std::ostringstream os; + os << time::Span("2.5"); + ASSERT_EQ(os.str(), "2.5s"); +} |