aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/klee/Internal/Support/Timer.h79
-rw-r--r--include/klee/TimerStatIncrementer.h12
-rw-r--r--lib/Core/AddressSpace.cpp4
-rw-r--r--lib/Core/CMakeLists.txt1
-rw-r--r--lib/Core/Executor.cpp49
-rw-r--r--lib/Core/Executor.h21
-rw-r--r--lib/Core/ExecutorTimerInfo.h42
-rw-r--r--lib/Core/ExecutorTimers.cpp108
-rw-r--r--lib/Core/StatsTracker.cpp46
-rw-r--r--lib/Core/TimingSolver.cpp8
-rw-r--r--lib/Support/Timer.cpp69
11 files changed, 189 insertions, 250 deletions
diff --git a/include/klee/Internal/Support/Timer.h b/include/klee/Internal/Support/Timer.h
index 65079a06..30b1b758 100644
--- a/include/klee/Internal/Support/Timer.h
+++ b/include/klee/Internal/Support/Timer.h
@@ -12,16 +12,85 @@
#include "klee/Internal/System/Time.h"
+#include "llvm/ADT/SmallVector.h"
+
+#include <functional>
+#include <memory>
+
namespace klee {
+
+ /**
+ * A WallTimer stores its creation time.
+ */
class WallTimer {
- time::Point start;
-
+ const time::Point start;
public:
WallTimer();
- /// check - Return the delta since the timer was created
- time::Span check();
+ /// Return the delta since the timer was created
+ time::Span delta() const;
+ };
+
+
+ /**
+ * A Timer repeatedly executes a `callback` after a specified `interval`.
+ * An object of this class is _passive_ and only keeps track of the next invocation time.
+ * _Passive_ means, that it has to be `invoke`d by an external caller with the current time.
+ * Only when the time span between the current time and the last invocation exceeds the
+ * specified `interval`, the `callback` will be executed.
+ * Multiple timers are typically managed by a TimerGroup.
+ */
+ class Timer {
+ /// Approximate interval between callback invocations.
+ time::Span interval;
+ /// Wall time for next invocation.
+ time::Point nextInvocationTime;
+ /// The event callback.
+ std::function<void()> run;
+ public:
+ /// \param interval The time span between callback invocations.
+ /// \param callback The event callback.
+ Timer(const time::Span &interval, std::function<void()> &&callback);
+
+ /// Return specified `interval` between invocations.
+ time::Span getInterval() const;
+ /// Execute `callback` if invocation time exceeded.
+ void invoke(const time::Point &currentTime);
+ /// Set new invocation time to `currentTime + interval`.
+ void reset(const time::Point &currentTime);
+ };
+
+
+ /**
+ * A TimerGroup manages multiple timers.
+ *
+ * TimerGroup simplifies the handling of multiple Timer objects by offering a unifying
+ * Timer-like interface. Additionally, it serves as a barrier and prevents timers from
+ * being invoked too often by defining a minimum invocation interval (MI).
+ * All registered timer intervals should be larger than MI and also be multiples of MI.
+ * Similar to Timer, a TimerGroup is _passive_ and needs to be `invoke`d by an external
+ * caller.
+ */
+ class TimerGroup {
+ /// Registered timers.
+ llvm::SmallVector<std::unique_ptr<Timer>, 4> timers;
+ /// Timer that invokes all registered timers after minimum interval.
+ Timer invocationTimer;
+ /// Time of last `invoke` call.
+ time::Point currentTime;
+ public:
+ /// \param minInterval The minimum interval between invocations of registered timers.
+ explicit TimerGroup(const time::Span &minInterval);
+
+ /// Add a timer to be executed periodically.
+ ///
+ /// \param timer The timer object to register.
+ void add(std::unique_ptr<Timer> timer);
+ /// Invoke registered timers with current time only if minimum interval exceeded.
+ void invoke();
+ /// Reset all timers.
+ void reset();
};
-}
+} // klee
#endif /* KLEE_TIMER_H */
diff --git a/include/klee/TimerStatIncrementer.h b/include/klee/TimerStatIncrementer.h
index f494b9d1..c467c82b 100644
--- a/include/klee/TimerStatIncrementer.h
+++ b/include/klee/TimerStatIncrementer.h
@@ -14,19 +14,23 @@
#include "klee/Internal/Support/Timer.h"
namespace klee {
+
+ /**
+ * A TimerStatIncrementer adds its lifetime to a specified Statistic.
+ */
class TimerStatIncrementer {
private:
- WallTimer timer;
+ const WallTimer timer;
Statistic &statistic;
public:
- TimerStatIncrementer(Statistic &_statistic) : statistic(_statistic) {}
+ explicit TimerStatIncrementer(Statistic &statistic) : statistic(statistic) {}
~TimerStatIncrementer() {
// record microseconds
- statistic += timer.check().toMicroseconds();
+ statistic += timer.delta().toMicroseconds();
}
- time::Span check() { return timer.check(); }
+ time::Span delta() const { return timer.delta(); }
};
}
diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp
index 1a88e4ec..12e74c77 100644
--- a/lib/Core/AddressSpace.cpp
+++ b/lib/Core/AddressSpace.cpp
@@ -237,7 +237,7 @@ bool AddressSpace::resolve(ExecutionState &state, TimingSolver *solver,
while (oi != begin) {
--oi;
const MemoryObject *mo = oi->first;
- if (timeout && timeout < timer.check())
+ if (timeout && timeout < timer.delta())
return true;
int incomplete =
@@ -256,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 && timeout < timer.check())
+ if (timeout && timeout < timer.delta())
return true;
bool mustBeTrue;
diff --git a/lib/Core/CMakeLists.txt b/lib/Core/CMakeLists.txt
index 72e9bc31..de52cd11 100644
--- a/lib/Core/CMakeLists.txt
+++ b/lib/Core/CMakeLists.txt
@@ -14,7 +14,6 @@ klee_add_component(kleeCore
CoreStats.cpp
ExecutionState.cpp
Executor.cpp
- ExecutorTimers.cpp
ExecutorUtil.cpp
ExternalDispatcher.cpp
ImpliedValue.cpp
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 1ba6d9bf..655d6005 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -12,7 +12,6 @@
#include "../Expr/ArrayExprOptimizer.h"
#include "Context.h"
#include "CoreStats.h"
-#include "ExecutorTimerInfo.h"
#include "ExternalDispatcher.h"
#include "ImpliedValue.h"
#include "Memory.h"
@@ -104,6 +103,13 @@ cl::OptionCategory
cl::OptionCategory TestGenCat("Test generation options",
"These options impact test generation.");
+
+cl::opt<std::string> MaxTime(
+ "max-time",
+ cl::desc("Halt execution after the specified duration. "
+ "Set to 0s to disable (default=0s)"),
+ cl::init("0s"),
+ cl::cat(TerminationCat));
} // namespace klee
namespace {
@@ -314,12 +320,6 @@ cl::opt<unsigned> RuntimeMaxStackFrames(
cl::init(8192),
cl::cat(TerminationCat));
-cl::opt<std::string> MaxInstructionTime(
- "max-instruction-time",
- cl::desc("Allow a single instruction to take only this much time. Enables "
- "--use-forked-solver. Set to 0s to disable (default=0s)"),
- cl::cat(TerminationCat));
-
cl::opt<double> MaxStaticForkPct(
"max-static-fork-pct", cl::init(1.),
cl::desc("Maximum percentage spent by an instruction forking out of the "
@@ -347,6 +347,13 @@ cl::opt<double> MaxStaticCPSolvePct(
"instructions (default=1.0 (always))"),
cl::cat(TerminationCat));
+cl::opt<std::string> TimerInterval(
+ "timer-interval",
+ cl::desc("Minimum interval to check timers. "
+ "Affects -max-time, -istats-write-interval, -stats-write-interval, and -uncovered-update-interval (default=1s)"),
+ cl::init("1s"),
+ cl::cat(TerminationCat));
+
/*** Debugging options ***/
@@ -425,22 +432,25 @@ const char *Executor::TerminateReasonNames[] = {
[ Unhandled ] = "xxx",
};
+
Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
InterpreterHandler *ih)
: Interpreter(opts), interpreterHandler(ih), searcher(0),
externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0),
- pathWriter(0), symPathWriter(0), specialFunctionHandler(0),
+ pathWriter(0), symPathWriter(0), specialFunctionHandler(0), timers{time::Span(TimerInterval)},
replayKTest(0), replayPath(0), usingSeeds(0),
atMemoryLimit(false), inhibitForking(false), haltExecution(false),
ivcEnabled(false), debugLogBuffer(debugBufferString) {
- const time::Span maxCoreSolverTime(MaxCoreSolverTime);
- maxInstructionTime = time::Span(MaxInstructionTime);
- coreSolverTimeout = maxCoreSolverTime && maxInstructionTime ?
- std::min(maxCoreSolverTime, maxInstructionTime)
- : std::max(maxCoreSolverTime, maxInstructionTime);
+ const time::Span maxTime{MaxTime};
+ if (maxTime) timers.add(
+ std::move(std::make_unique<Timer>(maxTime, [&]{
+ klee_message("HaltTimer invoked");
+ setHaltExecution(true);
+ })));
+ coreSolverTimeout = time::Span{MaxCoreSolverTime};
if (coreSolverTimeout) UseForkedCoreSolver = true;
Solver *coreSolver = klee::createCoreSolver(CoreSolverToUse);
if (!coreSolver) {
@@ -554,10 +564,6 @@ Executor::~Executor() {
delete specialFunctionHandler;
delete statsTracker;
delete solver;
- while(!timers.empty()) {
- delete timers.back();
- timers.pop_back();
- }
}
/***/
@@ -2865,9 +2871,8 @@ void Executor::doDumpStates() {
void Executor::run(ExecutionState &initialState) {
bindModuleConstants();
- // Delay init till now so that ticks don't accrue during
- // optimization and such.
- initTimers();
+ // Delay init till now so that ticks don't accrue during optimization and such.
+ timers.reset();
states.insert(&initialState);
@@ -2898,7 +2903,7 @@ void Executor::run(ExecutionState &initialState) {
stepInstruction(state);
executeInstruction(state, ki);
- processTimers(&state, maxInstructionTime * numSeeds);
+ timers.invoke();
if (::dumpStates) dumpStates();
if (::dumpPTree) dumpPTree();
updateStates(&state);
@@ -2954,7 +2959,7 @@ void Executor::run(ExecutionState &initialState) {
stepInstruction(state);
executeInstruction(state, ki);
- processTimers(&state, maxInstructionTime);
+ timers.invoke();
if (::dumpStates) dumpStates();
if (::dumpPTree) dumpPTree();
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 84231720..f6e58a6b 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -92,15 +92,6 @@ class Executor : public Interpreter {
friend class MergingSearcher;
public:
- class Timer {
- public:
- Timer() = default;
- virtual ~Timer() = default;
-
- /// The event callback.
- virtual void run() = 0;
- };
-
typedef std::pair<ExecutionState*,ExecutionState*> StatePair;
enum TerminateReason {
@@ -122,8 +113,6 @@ public:
private:
static const char *TerminateReasonNames[];
- class TimerInfo;
-
std::unique_ptr<KModule> kmodule;
InterpreterHandler *interpreterHandler;
Searcher *searcher;
@@ -135,7 +124,7 @@ private:
StatsTracker *statsTracker;
TreeStreamWriter *pathWriter, *symPathWriter;
SpecialFunctionHandler *specialFunctionHandler;
- std::vector<TimerInfo*> timers;
+ TimerGroup timers;
std::unique_ptr<PTree> processTree;
/// Keeps track of all currently ongoing merges.
@@ -460,14 +449,6 @@ private:
ref<Expr> e,
ref<ConstantExpr> value);
- /// Add a timer to be executed periodically.
- ///
- /// \param timer The timer object to run on firings.
- /// \param rate The approximate delay (in seconds) between firings.
- void addTimer(Timer *timer, time::Span rate);
-
- void initTimers();
- 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
deleted file mode 100644
index 66ba5c2e..00000000
--- a/lib/Core/ExecutorTimerInfo.h
+++ /dev/null
@@ -1,42 +0,0 @@
-//===-- ExecutorTimerInfo.h -------------------------------------*- C++ -*-===//
-//
-// The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-//
-// Class to wrap information for a timer.
-//
-//===----------------------------------------------------------------------===//
-
-#ifndef KLEE_EXECUTORTIMERINFO_H
-#define KLEE_EXECUTORTIMERINFO_H
-
-#include "klee/Internal/System/Time.h"
-
-namespace klee {
-
-class Executor::TimerInfo {
-public:
- Timer *timer;
-
- /// Approximate delay per timer firing.
- time::Span rate;
- /// Wall time for next firing.
- time::Point nextFireTime;
-
-public:
- TimerInfo(Timer *_timer, time::Span _rate)
- : timer(_timer),
- rate(_rate),
- nextFireTime(time::getWallTime() + rate) {}
- ~TimerInfo() { delete timer; }
-};
-
-
-}
-
-
-#endif /* KLEE_EXECUTORTIMERINFO_H */
diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp
index 8ebe5aed..e69de29b 100644
--- a/lib/Core/ExecutorTimers.cpp
+++ b/lib/Core/ExecutorTimers.cpp
@@ -1,108 +0,0 @@
-//===-- ExecutorTimers.cpp ------------------------------------------------===//
-//
-// The KLEE Symbolic Virtual Machine
-//
-// This file is distributed under the University of Illinois Open Source
-// License. See LICENSE.TXT for details.
-//
-//===----------------------------------------------------------------------===//
-
-#include "CoreStats.h"
-#include "Executor.h"
-#include "ExecutorTimerInfo.h"
-#include "PTree.h"
-#include "StatsTracker.h"
-
-#include "klee/ExecutionState.h"
-#include "klee/Internal/Module/InstructionInfoTable.h"
-#include "klee/Internal/Module/KInstruction.h"
-#include "klee/Internal/Module/KModule.h"
-#include "klee/Internal/Support/ErrorHandling.h"
-#include "klee/Internal/System/Time.h"
-#include "klee/OptionCategories.h"
-
-#include "llvm/IR/Function.h"
-#include "llvm/Support/CommandLine.h"
-
-#include <math.h>
-#include <signal.h>
-#include <string>
-#include <sys/time.h>
-#include <unistd.h>
-
-using namespace llvm;
-using namespace klee;
-
-namespace klee {
-cl::opt<std::string>
- MaxTime("max-time",
- cl::desc("Halt execution after the specified number of seconds. "
- "Set to 0s to disable (default=0s)"),
- cl::init("0s"),
- cl::cat(TerminationCat));
-
-cl::opt<std::string>
- TimerInterval("timer-interval",
- cl::desc("Minimum interval to check timers (default=1s)"),
- cl::init("1s"),
- cl::cat(TerminationCat)); // StatsCat?
-}
-
-///
-
-class HaltTimer : public Executor::Timer {
- Executor *executor;
-
-public:
- HaltTimer(Executor *_executor) : executor(_executor) {}
- ~HaltTimer() {}
-
- void run() {
- klee_message("HaltTimer invoked");
- executor->setHaltExecution(true);
- }
-};
-
-///
-
-void Executor::initTimers() {
- const time::Span maxTime(MaxTime);
- if (maxTime) {
- addTimer(new HaltTimer(this), maxTime);
- }
-}
-
-///
-
-void Executor::addTimer(Timer *timer, time::Span rate) {
- timers.push_back(new TimerInfo(timer, rate));
-}
-
-void Executor::processTimers(ExecutionState *current,
- time::Span maxInstTime) {
- const static time::Span minInterval(TimerInterval);
- static time::Point lastCheckedTime;
- const auto currentTime = time::getWallTime();
- const auto duration = currentTime - lastCheckedTime;
-
- if (duration < minInterval) return;
-
- // check max instruction time
- if (maxInstTime && current &&
- std::find(removedStates.begin(), removedStates.end(), current) == removedStates.end() &&
- duration > maxInstTime) {
- klee_warning("max-instruction-time exceeded: %.2fs", duration.toSeconds());
- terminateStateEarly(*current, "max-instruction-time exceeded");
- }
-
-
- // check timers
- for (auto &timerInfo : timers) {
- if (currentTime >= timerInfo->nextFireTime) {
- timerInfo->timer->run();
- timerInfo->nextFireTime = currentTime + timerInfo->rate;
- }
- }
-
- lastCheckedTime = currentTime;
-}
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 259a8d98..5eac2cf2 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -122,40 +122,6 @@ bool StatsTracker::useIStats() {
return OutputIStats;
}
-namespace klee {
- class WriteIStatsTimer : public Executor::Timer {
- StatsTracker *statsTracker;
-
- public:
- WriteIStatsTimer(StatsTracker *_statsTracker) : statsTracker(_statsTracker) {}
- ~WriteIStatsTimer() {}
-
- void run() { statsTracker->writeIStats(); }
- };
-
- class WriteStatsTimer : public Executor::Timer {
- StatsTracker *statsTracker;
-
- public:
- WriteStatsTimer(StatsTracker *_statsTracker) : statsTracker(_statsTracker) {}
- ~WriteStatsTimer() {}
-
- void run() { statsTracker->writeStatsLine(); }
- };
-
- class UpdateReachableTimer : public Executor::Timer {
- StatsTracker *statsTracker;
-
- public:
- UpdateReachableTimer(StatsTracker *_statsTracker) : statsTracker(_statsTracker) {}
-
- void run() { statsTracker->computeReachableUncovered(); }
- };
-
-}
-
-//
-
/// Check for special cases where we statically know an instruction is
/// uncoverable. Currently the case is an unreachable instruction
/// following a noreturn call; the instruction is really only there to
@@ -297,20 +263,26 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
writeStatsLine();
if (statsWriteInterval)
- executor.addTimer(new WriteStatsTimer(this), statsWriteInterval);
+ executor.timers.add(std::move(std::make_unique<Timer>(statsWriteInterval, [&]{
+ writeStatsLine();
+ })));
}
// Add timer to calculate uncovered instructions if needed by the solver
if (updateMinDistToUncovered) {
computeReachableUncovered();
- executor.addTimer(new UpdateReachableTimer(this), time::Span(UncoveredUpdateInterval));
+ executor.timers.add(std::move(std::make_unique<Timer>(time::Span{UncoveredUpdateInterval}, [&]{
+ computeReachableUncovered();
+ })));
}
if (OutputIStats) {
istatsFile = executor.interpreterHandler->openOutputFile("run.istats");
if (istatsFile) {
if (iStatsWriteInterval)
- executor.addTimer(new WriteIStatsTimer(this), iStatsWriteInterval);
+ executor.timers.add(std::move(std::make_unique<Timer>(iStatsWriteInterval, [&]{
+ writeIStats();
+ })));
} else {
klee_error("Unable to open instruction level stats file (run.istats).");
}
diff --git a/lib/Core/TimingSolver.cpp b/lib/Core/TimingSolver.cpp
index 81ebf098..0bd2fe57 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();
+ state.queryCost += timer.delta();
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();
+ state.queryCost += timer.delta();
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();
+ state.queryCost += timer.delta();
return success;
}
@@ -120,7 +120,7 @@ TimingSolver::getInitialValues(const ExecutionState& state,
ConstantExpr::alloc(0, Expr::Bool)),
objects, result);
- state.queryCost += timer.check();
+ state.queryCost += timer.delta();
return success;
}
diff --git a/lib/Support/Timer.cpp b/lib/Support/Timer.cpp
index 4e52feb5..8a0b4ecc 100644
--- a/lib/Support/Timer.cpp
+++ b/lib/Support/Timer.cpp
@@ -7,16 +7,75 @@
//
//===----------------------------------------------------------------------===//
-#include "klee/Config/Version.h"
+#include "klee/Internal/Support/ErrorHandling.h"
#include "klee/Internal/Support/Timer.h"
#include "klee/Internal/System/Time.h"
+
using namespace klee;
-WallTimer::WallTimer() {
- start = time::getWallTime();
+
+// WallTimer
+
+WallTimer::WallTimer() : start{time::getWallTime()} {}
+
+time::Span WallTimer::delta() const {
+ return {time::getWallTime() - start};
+}
+
+
+// Timer
+
+Timer::Timer(const time::Span &interval, std::function<void()> &&callback) :
+ interval{interval}, nextInvocationTime{time::getWallTime() + interval}, run{std::move(callback)} {};
+
+time::Span Timer::getInterval() const {
+ return interval;
+};
+
+void Timer::invoke(const time::Point &currentTime) {
+ if (currentTime < nextInvocationTime) return;
+
+ run();
+ nextInvocationTime = currentTime + interval;
+};
+
+void Timer::reset(const time::Point &currentTime) {
+ nextInvocationTime = currentTime + interval;
+};
+
+
+// TimerGroup
+
+TimerGroup::TimerGroup(const time::Span &minInterval) :
+ invocationTimer{
+ minInterval,
+ [&]{
+ // invoke timers
+ for (auto &timer : timers)
+ timer->invoke(currentTime);
+ }
+ } {};
+
+void TimerGroup::add(std::unique_ptr<klee::Timer> timer) {
+ const auto &interval = timer->getInterval();
+ const auto &minInterval = invocationTimer.getInterval();
+ if (interval < minInterval)
+ klee_warning("Timer interval below minimum timer interval (-timer-interval)");
+ if (interval.toMicroseconds() % minInterval.toMicroseconds())
+ klee_warning("Timer interval not a multiple of timer interval (-timer-interval)");
+
+ timers.emplace_back(std::move(timer));
+}
+
+void TimerGroup::invoke() {
+ currentTime = time::getWallTime();
+ invocationTimer.invoke(currentTime);
}
-time::Span WallTimer::check() {
- return time::Span(time::getWallTime() - start);
+void TimerGroup::reset() {
+ currentTime = time::getWallTime();
+ invocationTimer.reset(currentTime);
+ for (auto &timer : timers)
+ timer->reset(currentTime);
}
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-14 14:38:31 +0000