about summary refs log tree commit diff homepage
path: root/lib/Core/Executor.cpp
diff options
context:
space:
mode:
authorFrank Busse <bb0xfb@gmail.com>2023-03-24 21:14:02 +0000
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2024-01-12 12:00:35 +0000
commit19b6ae578b0658115d15848604a28434845bb3e3 (patch)
tree31d52545929760ad725385bd1cdc1153b710fc75 /lib/Core/Executor.cpp
parentfc83f06b17221bf5ef20e30d9da1ccff927beb17 (diff)
downloadklee-19b6ae578b0658115d15848604a28434845bb3e3.tar.gz
new: persistent ptree (-write-ptree) and klee-ptree
Introduce three different kinds of process trees:
1. Noop: does nothing (e.g. no allocations for DFS)
2. InMemory: same behaviour as before (e.g. RandomPathSearcher)
3. Persistent: similar to InMemory but writes nodes to ptree.db
     and tracks information such as branch type, termination
     type or source location (asm) in nodes. Enabled with
     -write-ptree

ptree.db files can be analysed/plotted with the new "klee-ptree"
tool.
Diffstat (limited to 'lib/Core/Executor.cpp')
-rw-r--r--lib/Core/Executor.cpp23
1 files changed, 15 insertions, 8 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index b4da6a08..8f70540c 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -3639,14 +3639,15 @@ std::string Executor::getAddressInfo(ExecutionState &state,
   return info.str();
 }
 
-
-void Executor::terminateState(ExecutionState &state) {
+void Executor::terminateState(ExecutionState &state,
+                              StateTerminationType reason) {
   if (replayKTest && replayPosition!=replayKTest->numObjects) {
     klee_warning_once(replayKTest,
                       "replay did not consume all objects in test input.");
   }
 
   interpreterHandler->incPathsExplored();
+  processTree->setTerminationType(state, reason);
 
   std::vector<ExecutionState *>::iterator it =
       std::find(addedStates.begin(), addedStates.end(), &state);
@@ -3690,7 +3691,7 @@ void Executor::terminateStateOnExit(ExecutionState &state) {
         terminationTypeFileExtension(StateTerminationType::Exit).c_str());
 
   interpreterHandler->incPathsCompleted();
-  terminateState(state);
+  terminateState(state, StateTerminationType::Exit);
 }
 
 void Executor::terminateStateEarly(ExecutionState &state, const Twine &message,
@@ -3707,7 +3708,7 @@ void Executor::terminateStateEarly(ExecutionState &state, const Twine &message,
         terminationTypeFileExtension(reason).c_str());
   }
 
-  terminateState(state);
+  terminateState(state, reason);
 }
 
 void Executor::terminateStateEarlyAlgorithm(ExecutionState &state,
@@ -3815,7 +3816,7 @@ void Executor::terminateStateOnError(ExecutionState &state,
     interpreterHandler->processTestCase(state, msg.str().c_str(), file_suffix);
   }
 
-  terminateState(state);
+  terminateState(state, terminationType);
 
   if (shouldExitOn(terminationType))
     haltExecution = true;
@@ -3848,9 +3849,14 @@ void Executor::terminateStateOnSolverError(ExecutionState &state,
 }
 
 void Executor::terminateStateOnUserError(ExecutionState &state,
-                                         const llvm::Twine &message) {
+                                         const llvm::Twine &message,
+                                         bool writeErr) {
   ++stats::terminationUserError;
-  terminateStateOnError(state, message, StateTerminationType::User, "");
+  if (writeErr) {
+    terminateStateOnError(state, message, StateTerminationType::User, "");
+  } else {
+    terminateState(state, StateTerminationType::User);
+  }
 }
 
 // XXX shoot me
@@ -4601,7 +4607,8 @@ void Executor::runFunctionAsMain(Function *f,
   
   initializeGlobals(*state);
 
-  processTree = std::make_unique<PTree>(state);
+  processTree = createPTree(*state, userSearcherRequiresInMemoryPTree(),
+                            *interpreterHandler);
   run(*state);
   processTree = nullptr;