ExecutorTimers: move dumpStates/dumpPTree into Executor

* creates two new methods: dumpStates, dumpPTree

1 files changed, 69 insertions, 0 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,