ExecutorTimers: move dumpStates/dumpPTree into Executor

* creates two new methods: dumpStates, dumpPTree

3 files changed, 76 insertions, 63 deletions

diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 5590af41..85cb8e8d 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -405,6 +405,10 @@ namespace klee {
   RNG theRNG;
 }
 
+// XXX hack
+extern "C" unsigned dumpStates, dumpPTree;
+unsigned dumpStates = 0, dumpPTree = 0;
+
 const char *Executor::TerminateReasonNames[] = {
   [ Abort ] = "abort",
   [ Assert ] = "assert",
@@ -2904,6 +2908,8 @@ void Executor::run(ExecutionState &initialState) {
 
       executeInstruction(state, ki);
       processTimers(&state, maxInstructionTime * numSeeds);
+      if (::dumpStates) dumpStates();
+      if (::dumpPTree) dumpPTree();
       updateStates(&state);
 
       if ((stats::instructions % 1000) == 0) {
@@ -2958,6 +2964,8 @@ void Executor::run(ExecutionState &initialState) {
 
     executeInstruction(state, ki);
     processTimers(&state, maxInstructionTime);
+    if (::dumpStates) dumpStates();
+    if (::dumpPTree) dumpPTree();
 
     checkMemoryUsage();
 
@@ -4082,6 +4090,67 @@ int *Executor::getErrnoLocation(const ExecutionState &state) const {
 #endif
 }
 
+
+void Executor::dumpPTree() {
+  if (!::dumpPTree) return;
+
+  char name[32];
+  snprintf(name, sizeof(name),"ptree%08d.dot", (int) stats::instructions);
+  auto os = interpreterHandler->openOutputFile(name);
+  if (os) {
+    processTree->dump(*os);
+  }
+
+  ::dumpPTree = 0;
+}
+
+void Executor::dumpStates() {
+  if (!::dumpStates) return;
+
+  auto os = interpreterHandler->openOutputFile("states.txt");
+
+  if (os) {
+    for (ExecutionState *es : states) {
+      *os << "(" << es << ",";
+      *os << "[";
+      auto next = es->stack.begin();
+      ++next;
+      for (auto sfIt = es->stack.begin(), sf_ie = es->stack.end();
+           sfIt != sf_ie; ++sfIt) {
+        *os << "('" << sfIt->kf->function->getName().str() << "',";
+        if (next == es->stack.end()) {
+          *os << es->prevPC->info->line << "), ";
+        } else {
+          *os << next->caller->info->line << "), ";
+          ++next;
+        }
+      }
+      *os << "], ";
+
+      StackFrame &sf = es->stack.back();
+      uint64_t md2u = computeMinDistToUncovered(es->pc,
+                                                sf.minDistToUncoveredOnReturn);
+      uint64_t icnt = theStatisticManager->getIndexedValue(stats::instructions,
+                                                           es->pc->info->id);
+      uint64_t cpicnt = sf.callPathNode->statistics.getValue(stats::instructions);
+
+      *os << "{";
+      *os << "'depth' : " << es->depth << ", ";
+      *os << "'weight' : " << es->weight << ", ";
+      *os << "'queryCost' : " << es->queryCost << ", ";
+      *os << "'coveredNew' : " << es->coveredNew << ", ";
+      *os << "'instsSinceCovNew' : " << es->instsSinceCovNew << ", ";
+      *os << "'md2u' : " << md2u << ", ";
+      *os << "'icnt' : " << icnt << ", ";
+      *os << "'CPicnt' : " << cpicnt << ", ";
+      *os << "}";
+      *os << ")\n";
+    }
+  }
+
+  ::dumpStates = 0;
+}
+
 ///
 
 Interpreter *Interpreter::create(LLVMContext &ctx, const InterpreterOptions &opts,
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index e2aab56c..851a52ec 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -479,6 +479,10 @@ private:
   void printDebugInstructions(ExecutionState &state);
   void doDumpStates();
 
+  /// Only for debug purposes; enable via debugger or klee-control
+  void dumpStates();
+  void dumpPTree();
+
 public:
   Executor(llvm::LLVMContext &ctx, const InterpreterOptions &opts,
       InterpreterHandler *ie);
diff --git a/lib/Core/ExecutorTimers.cpp b/lib/Core/ExecutorTimers.cpp
index e1d6684d..81ab7651 100644
--- a/lib/Core/ExecutorTimers.cpp
+++ b/lib/Core/ExecutorTimers.cpp
@@ -62,10 +62,6 @@ public:
 static const time::Span kMilliSecondsPerTick(time::milliseconds(100));
 static volatile unsigned timerTicks = 0;
 
-// XXX hack
-extern "C" unsigned dumpStates, dumpPTree;
-unsigned dumpStates = 0, dumpPTree = 0;
-
 static void onAlarm(int) {
   ++timerTicks;
 }
@@ -114,63 +110,7 @@ void Executor::processTimers(ExecutionState *current,
     ticks = 1;
   }
 
-  if (ticks || dumpPTree || dumpStates) {
-    if (dumpPTree) {
-      char name[32];
-      snprintf(name, sizeof(name), "ptree%08d.dot", (int) stats::instructions);
-      auto os = interpreterHandler->openOutputFile(name);
-      if (os) {
-        processTree->dump(*os);
-      }
-
-      dumpPTree = 0;
-    }
-
-    if (dumpStates) {
-      auto os = interpreterHandler->openOutputFile("states.txt");
-
-      if (os) {
-        for (ExecutionState *es : states) {
-          *os << "(" << es << ",";
-          *os << "[";
-          auto next = es->stack.begin();
-          ++next;
-          for (auto sfIt = es->stack.begin(), sf_ie = es->stack.end();
-               sfIt != sf_ie; ++sfIt) {
-            *os << "('" << sfIt->kf->function->getName().str() << "',";
-            if (next == es->stack.end()) {
-              *os << es->prevPC->info->line << "), ";
-            } else {
-              *os << next->caller->info->line << "), ";
-              ++next;
-            }
-          }
-          *os << "], ";
-
-          StackFrame &sf = es->stack.back();
-          uint64_t md2u = computeMinDistToUncovered(es->pc,
-                                                    sf.minDistToUncoveredOnReturn);
-          uint64_t icnt = theStatisticManager->getIndexedValue(stats::instructions,
-                                                               es->pc->info->id);
-          uint64_t cpicnt = sf.callPathNode->statistics.getValue(stats::instructions);
-
-          *os << "{";
-          *os << "'depth' : " << es->depth << ", ";
-          *os << "'weight' : " << es->weight << ", ";
-          *os << "'queryCost' : " << es->queryCost << ", ";
-          *os << "'coveredNew' : " << es->coveredNew << ", ";
-          *os << "'instsSinceCovNew' : " << es->instsSinceCovNew << ", ";
-          *os << "'md2u' : " << md2u << ", ";
-          *os << "'icnt' : " << icnt << ", ";
-          *os << "'CPicnt' : " << cpicnt << ", ";
-          *os << "}";
-          *os << ")\n";
-        }
-      }
-
-      dumpStates = 0;
-    }
-
+  if (ticks) {
     if (maxInstTime && current &&
         std::find(removedStates.begin(), removedStates.end(), current) ==
             removedStates.end()) {
@@ -183,10 +123,10 @@ void Executor::processTimers(ExecutionState *current,
     if (!timers.empty()) {
       auto time = time::getWallTime();
 
-      for (std::vector<TimerInfo*>::iterator it = timers.begin(), 
+      for (std::vector<TimerInfo*>::iterator it = timers.begin(),
              ie = timers.end(); it != ie; ++it) {
         TimerInfo *ti = *it;
-        
+
         if (time >= ti->nextFireTime) {
           ti->timer->run();
           ti->nextFireTime = time + ti->rate;