Add feature to dump statistics after n instructions

Add -stats-write-after-instructions and -istats-write-after-instructions
to update each statistic after n steps.

Furthermore, the metric "minimal distance to uncovered state" is now
updated independently if statistics are enabled or not.
This metric is needed i.e. by weighted random searchers directed towards
uncovered instructions.

Remove some dead code.

2 files changed, 54 insertions, 22 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 49b022f8..f23fb3c0 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -364,7 +364,7 @@ const Module *Executor::setModule(llvm::Module *module,
   kmodule->prepare(opts, interpreterHandler);
   specialFunctionHandler->bind();
 
-  if (StatsTracker::useStatistics()) {
+  if (StatsTracker::useStatistics() || userSearcherRequiresMD2U()) {
     statsTracker = 
       new StatsTracker(*this,
                        interpreterHandler->getOutputFilename("assembly.ll"),
diff --git a/lib/Core/StatsTracker.cpp b/lib/Core/StatsTracker.cpp
index 5e77172e..26890e50 100644
--- a/lib/Core/StatsTracker.cpp
+++ b/lib/Core/StatsTracker.cpp
@@ -86,17 +86,20 @@ namespace {
                      cl::init(1.),
 		     cl::desc("Approximate number of seconds between stats writes (default=1.0s)"));
 
+  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>
   IStatsWriteInterval("istats-write-interval",
 		      cl::init(10.),
                       cl::desc("Approximate number of seconds between istats writes (default: 10.0s)"));
 
-  /*
-  cl::opt<double>
-  BranchCovCountsWriteInterval("branch-cov-counts-write-interval",
-                     cl::desc("Approximate number of seconds between run.branches writes (default: 5.0s)"),
-                     cl::init(5.));
-  */
+  cl::opt<unsigned> IStatsWriteAfterInstructions(
+      "istats-write-after-instructions", cl::init(0),
+      cl::desc("Write istats after each n instructions, 0 to disable "
+               "(default=0)"));
 
   // XXX I really would like to have dynamic rate control for something like this.
   cl::opt<double>
@@ -185,6 +188,18 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
     fullBranches(0),
     partialBranches(0),
     updateMinDistToUncovered(_updateMinDistToUncovered) {
+
+  if (StatsWriteAfterInstructions > 0 && StatsWriteInterval > 0)
+    klee_error("Both options --stats-write-interval and "
+               "--stats-write-after-instructions cannot be enabled at the same "
+               "time.");
+
+  if (IStatsWriteAfterInstructions > 0 && IStatsWriteInterval > 0)
+    klee_error(
+        "Both options --istats-write-interval and "
+        "--istats-write-after-instructions cannot be enabled at the same "
+        "time.");
+
   KModule *km = executor.kmodule;
 
   if (!sys::path::is_absolute(objectFilename)) {
@@ -235,19 +250,22 @@ StatsTracker::StatsTracker(Executor &_executor, std::string _objectFilename,
     writeStatsHeader();
     writeStatsLine();
 
-    executor.addTimer(new WriteStatsTimer(this), StatsWriteInterval);
+    if (StatsWriteInterval > 0)
+      executor.addTimer(new WriteStatsTimer(this), StatsWriteInterval);
+  }
 
-    if (updateMinDistToUncovered) {
-      computeReachableUncovered();
-      executor.addTimer(new UpdateReachableTimer(this), UncoveredUpdateInterval);
-    }
+  // Add timer to calculate uncovered instructions if needed by the solver
+  if (updateMinDistToUncovered) {
+    computeReachableUncovered();
+    executor.addTimer(new UpdateReachableTimer(this), UncoveredUpdateInterval);
   }
 
   if (OutputIStats) {
     istatsFile = executor.interpreterHandler->openOutputFile("run.istats");
     assert(istatsFile && "unable to open istats file");
 
-    executor.addTimer(new WriteIStatsTimer(this), IStatsWriteInterval);
+    if (IStatsWriteInterval > 0)
+      executor.addTimer(new WriteIStatsTimer(this), IStatsWriteInterval);
   }
 }
 
@@ -261,8 +279,12 @@ StatsTracker::~StatsTracker() {
 void StatsTracker::done() {
   if (statsFile)
     writeStatsLine();
-  if (OutputIStats)
+
+  if (OutputIStats) {
+    if (updateMinDistToUncovered)
+      computeReachableUncovered();
     writeIStats();
+  }
 }
 
 void StatsTracker::stepInstruction(ExecutionState &es) {
@@ -310,6 +332,14 @@ void StatsTracker::stepInstruction(ExecutionState &es) {
       }
     }
   }
+
+  if (statsFile && StatsWriteAfterInstructions &&
+      stats::instructions % StatsWriteAfterInstructions.getValue() == 0)
+    writeStatsLine();
+
+  if (istatsFile && IStatsWriteAfterInstructions &&
+      stats::instructions % IStatsWriteAfterInstructions.getValue() == 0)
+    writeIStats();
 }
 
 ///
@@ -327,15 +357,17 @@ void StatsTracker::framePushed(ExecutionState &es, StackFrame *parentFrame) {
       sf.callPathNode = cp;
       cp->count++;
     }
+  }
 
-    if (updateMinDistToUncovered) {
-      uint64_t minDistAtRA = 0;
-      if (parentFrame)
-        minDistAtRA = parentFrame->minDistToUncoveredOnReturn;
-      
-      sf.minDistToUncoveredOnReturn = sf.caller ?
-        computeMinDistToUncovered(sf.caller, minDistAtRA) : 0;
-    }
+  if (updateMinDistToUncovered) {
+    StackFrame &sf = es.stack.back();
+
+    uint64_t minDistAtRA = 0;
+    if (parentFrame)
+      minDistAtRA = parentFrame->minDistToUncoveredOnReturn;
+
+    sf.minDistToUncoveredOnReturn =
+        sf.caller ? computeMinDistToUncovered(sf.caller, minDistAtRA) : 0;
   }
 }