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)

2 files changed, 82 insertions, 9 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(); }
   };
 }