From 3caf3e985e4f35ac6ac04f61b92f11d2569550c6 Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Fri, 24 Nov 2017 16:58:27 +0000 Subject: Base time API upon std::chrono This should not change the behaviour of KLEE and mimics the old API. - functions moved from util into time namespace - uses time points and time spans instead of double - CLI arguments now have the form "3h5min8us" Changed command line parameters: - batch-time (double to string) - istats-write-interval (double to string) - max-instruction-time (double to string) - max-solver-time (double to string) - max-time (double to string) - min-query-time-to-log (double to string) - seed-time (double to string) - stats-write-interval (double to string) - uncovered-update-interval (double to string) - added: log-timed-out-queries (replaces negative max-solver-time) --- include/klee/ExecutionState.h | 3 +- include/klee/IncompleteSolver.h | 2 +- include/klee/Internal/Support/Timer.h | 16 ++--- include/klee/Internal/System/Time.h | 117 ++++++++++++++++++++++++++++------ include/klee/Solver.h | 9 ++- include/klee/SolverCmdLine.h | 6 +- include/klee/SolverImpl.h | 3 +- include/klee/TimerStatIncrementer.h | 5 +- 8 files changed, 119 insertions(+), 42 deletions(-) (limited to 'include') 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 - -#if LLVM_VERSION_CODE >= LLVM_VERSION(4, 0) -#include -#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 +#include "llvm/Support/raw_ostream.h" -#include "llvm/Support/Chrono.h" -#else -#include "llvm/Support/TimeValue.h" -#endif +#include +#include +#include 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 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 @@ -200,7 +201,7 @@ namespace klee { virtual std::pair< ref, ref > 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 UseIndependentSolver; extern llvm::cl::opt DebugValidateSolver; -extern llvm::cl::opt MinQueryTimeToLog; +extern llvm::cl::opt MinQueryTimeToLog; -extern llvm::cl::opt MaxCoreSolverTime; +extern llvm::cl::opt LogTimedOutQueries; + +extern llvm::cl::opt MaxCoreSolverTime; extern llvm::cl::opt 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 @@ -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(); } }; } -- cgit 1.4.1