[WIP] Fix bug where stats would not be updated on early exit caused by

finding a bug with the `-exit-on-error` option enabled.

4 files changed, 12 insertions, 0 deletions

diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h
index 4c428994..40f59ff1 100644
--- a/include/klee/Interpreter.h
+++ b/include/klee/Interpreter.h
@@ -138,6 +138,8 @@ public:
 
   virtual void setInhibitForking(bool value) = 0;
 
+  virtual void prepareForEarlyExit() = 0;
+
   /*** State accessor methods ***/
 
   virtual unsigned getPathStreamID(const ExecutionState &state) = 0;
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 95812dd7..1930cdc3 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -3835,6 +3835,13 @@ size_t Executor::getAllocationAlignment(const llvm::Value *allocSite) const {
          "Returned alignment must be a power of two");
   return alignment;
 }
+
+void Executor::prepareForEarlyExit() {
+  if (statsTracker) {
+    // Make sure stats get flushed out
+    statsTracker->done();
+  }
+}
 ///
 
 Interpreter *Interpreter::create(LLVMContext &ctx, const InterpreterOptions &opts,
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 7c18ae1f..c3f6e705 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -487,6 +487,8 @@ public:
     inhibitForking = value;
   }
 
+  void prepareForEarlyExit();
+
   /*** State accessor methods ***/
 
   virtual unsigned getPathStreamID(const ExecutionState &state);
diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp
index c65953d1..337d23a4 100644
--- a/tools/klee/main.cpp
+++ b/tools/klee/main.cpp
@@ -422,6 +422,7 @@ void KleeHandler::processTestCase(const ExecutionState &state,
                                   const char *errorSuffix) {
   if (errorMessage && ExitOnError) {
     llvm::errs() << "EXITING ON ERROR:\n" << errorMessage << "\n";
+    m_interpreter->prepareForEarlyExit();
     exit(1);
   }