about summary refs log tree commit diff homepage
path: root/lib/Core/Searcher.cpp
diff options
context:
space:
mode:
authorCristian Cadar <c.cadar@imperial.ac.uk>2023-12-22 18:22:02 +0200
committerMartinNowack <2443641+MartinNowack@users.noreply.github.com>2024-01-12 12:00:35 +0000
commit3fa03d12d28658694f2bf2085e8634cc267e3f16 (patch)
treec775b6d770c98ca310e9caf50c36016f99b81891 /lib/Core/Searcher.cpp
parent2c8b74cc858793c94e5476b5765e93ee23738702 (diff)
downloadklee-3fa03d12d28658694f2bf2085e8634cc267e3f16.tar.gz
Renamed PTree to ExecutionTree (and similar)
Diffstat (limited to 'lib/Core/Searcher.cpp')
-rw-r--r--lib/Core/Searcher.cpp64
1 files changed, 32 insertions, 32 deletions
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 1c57eb4e..e94511ea 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -11,9 +11,9 @@
 
 #include "CoreStats.h"
 #include "ExecutionState.h"
+#include "ExecutionTree.h"
 #include "Executor.h"
 #include "MergeHandler.h"
-#include "PTree.h"
 #include "StatsTracker.h"
 
 #include "klee/ADT/DiscretePDF.h"
@@ -261,18 +261,17 @@ void WeightedRandomSearcher::printName(llvm::raw_ostream &os) {
 #define IS_OUR_NODE_VALID(n)                                                   \
   (((n).getPointer() != nullptr) && (((n).getInt() & idBitMask) != 0))
 
-RandomPathSearcher::RandomPathSearcher(InMemoryPTree *processTree, RNG &rng)
-    : processTree{processTree}, theRNG{rng},
-      idBitMask{
-          static_cast<uint8_t>(processTree ? processTree->getNextId() : 0)} {
-
-  assert(processTree);
+RandomPathSearcher::RandomPathSearcher(InMemoryExecutionTree *executionTree, RNG &rng)
+    : executionTree{executionTree}, theRNG{rng},
+      idBitMask{static_cast<uint8_t>(executionTree ? executionTree->getNextId() : 0)} {
+  assert(executionTree);
 };
 
 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(executionTree->root.getInt() & idBitMask &&
+         "Root should belong to the searcher");
+  ExecutionTreeNode *n = executionTree->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");
@@ -300,46 +299,47 @@ void RandomPathSearcher::update(ExecutionState *current,
                                 const std::vector<ExecutionState *> &removedStates) {
   // insert states
   for (auto es : addedStates) {
-    PTreeNode *pnode = es->ptreeNode, *parent = pnode->parent;
-    PTreeNodePtr *childPtr;
+    ExecutionTreeNode *etnode = es->executionTreeNode, *parent = etnode->parent;
+    ExecutionTreeNodePtr *childPtr;
 
-    childPtr = parent ? ((parent->left.getPointer() == pnode) ? &parent->left
-                                                              : &parent->right)
-                      : &processTree->root;
-    while (pnode && !IS_OUR_NODE_VALID(*childPtr)) {
+    childPtr = parent ? ((parent->left.getPointer() == etnode) ? &parent->left
+                                                               : &parent->right)
+                      : &executionTree->root;
+    while (etnode && !IS_OUR_NODE_VALID(*childPtr)) {
       childPtr->setInt(childPtr->getInt() | idBitMask);
-      pnode = parent;
-      if (pnode)
-        parent = pnode->parent;
+      etnode = parent;
+      if (etnode)
+        parent = etnode->parent;
 
       childPtr = parent
-                     ? ((parent->left.getPointer() == pnode) ? &parent->left
-                                                             : &parent->right)
-                     : &processTree->root;
+                     ? ((parent->left.getPointer() == etnode) ? &parent->left
+                                                              : &parent->right)
+                     : &executionTree->root;
     }
   }
 
   // remove states
   for (auto es : removedStates) {
-    PTreeNode *pnode = es->ptreeNode, *parent = pnode->parent;
+    ExecutionTreeNode *etnode = es->executionTreeNode, *parent = etnode->parent;
 
-    while (pnode && !IS_OUR_NODE_VALID(pnode->left) &&
-           !IS_OUR_NODE_VALID(pnode->right)) {
+    while (etnode && !IS_OUR_NODE_VALID(etnode->left) &&
+           !IS_OUR_NODE_VALID(etnode->right)) {
       auto childPtr =
-          parent ? ((parent->left.getPointer() == pnode) ? &parent->left
-                                                         : &parent->right)
-                 : &processTree->root;
-      assert(IS_OUR_NODE_VALID(*childPtr) && "Removing pTree child not ours");
+          parent ? ((parent->left.getPointer() == etnode) ? &parent->left
+                                                          : &parent->right)
+                 : &executionTree->root;
+      assert(IS_OUR_NODE_VALID(*childPtr) &&
+             "Removing executionTree child not ours");
       childPtr->setInt(childPtr->getInt() & ~idBitMask);
-      pnode = parent;
-      if (pnode)
-        parent = pnode->parent;
+      etnode = parent;
+      if (etnode)
+        parent = etnode->parent;
     }
   }
 }
 
 bool RandomPathSearcher::empty() {
-  return !IS_OUR_NODE_VALID(processTree->root);
+  return !IS_OUR_NODE_VALID(executionTree->root);
 }
 
 void RandomPathSearcher::printName(llvm::raw_ostream &os) {