ExecutorTimers: refactor and move to support lib

- moves timer handling from Executor into support lib
- introduces TimerGroup, removes TimerInfo/WriteStatsTimer/UpdateReachableTimer/WriteIStatsTimer classes
- removes ExecutorTimers.cpp and ExecutorTimerInfo.h
- removes -max-instruction-time flag (see #1114)

9 files changed, 107 insertions, 241 deletions

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);
 }