about summary refs log tree commit diff homepage
path: root/lib/Core/Searcher.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/Searcher.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/Searcher.cpp')
-rw-r--r--lib/Core/Searcher.cpp23
1 files changed, 13 insertions, 10 deletions
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index bf98ebc7..1c57eb4e 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -261,15 +261,18 @@ void WeightedRandomSearcher::printName(llvm::raw_ostream &os) {
 #define IS_OUR_NODE_VALID(n)                                                   \
   (((n).getPointer() != nullptr) && (((n).getInt() & idBitMask) != 0))
 
-RandomPathSearcher::RandomPathSearcher(PTree &processTree, RNG &rng)
-  : processTree{processTree},
-    theRNG{rng},
-    idBitMask{processTree.getNextId()} {};
+RandomPathSearcher::RandomPathSearcher(InMemoryPTree *processTree, RNG &rng)
+    : processTree{processTree}, theRNG{rng},
+      idBitMask{
+          static_cast<uint8_t>(processTree ? processTree->getNextId() : 0)} {
+
+  assert(processTree);
+};
 
 ExecutionState &RandomPathSearcher::selectState() {
   unsigned flips=0, bits=0;
-  assert(processTree.root.getInt() & idBitMask && "Root should belong to the searcher");
-  PTreeNode *n = processTree.root.getPointer();
+  assert(processTree->root.getInt() & idBitMask && "Root should belong to the searcher");
+  PTreeNode *n = processTree->root.getPointer();
   while (!n->state) {
     if (!IS_OUR_NODE_VALID(n->left)) {
       assert(IS_OUR_NODE_VALID(n->right) && "Both left and right nodes invalid");
@@ -302,7 +305,7 @@ void RandomPathSearcher::update(ExecutionState *current,
 
     childPtr = parent ? ((parent->left.getPointer() == pnode) ? &parent->left
                                                               : &parent->right)
-                      : &processTree.root;
+                      : &processTree->root;
     while (pnode && !IS_OUR_NODE_VALID(*childPtr)) {
       childPtr->setInt(childPtr->getInt() | idBitMask);
       pnode = parent;
@@ -312,7 +315,7 @@ void RandomPathSearcher::update(ExecutionState *current,
       childPtr = parent
                      ? ((parent->left.getPointer() == pnode) ? &parent->left
                                                              : &parent->right)
-                     : &processTree.root;
+                     : &processTree->root;
     }
   }
 
@@ -325,7 +328,7 @@ void RandomPathSearcher::update(ExecutionState *current,
       auto childPtr =
           parent ? ((parent->left.getPointer() == pnode) ? &parent->left
                                                          : &parent->right)
-                 : &processTree.root;
+                 : &processTree->root;
       assert(IS_OUR_NODE_VALID(*childPtr) && "Removing pTree child not ours");
       childPtr->setInt(childPtr->getInt() & ~idBitMask);
       pnode = parent;
@@ -336,7 +339,7 @@ void RandomPathSearcher::update(ExecutionState *current,
 }
 
 bool RandomPathSearcher::empty() {
-  return !IS_OUR_NODE_VALID(processTree.root);
+  return !IS_OUR_NODE_VALID(processTree->root);
 }
 
 void RandomPathSearcher::printName(llvm::raw_ostream &os) {