about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--lib/Core/Executor.cpp21
-rw-r--r--lib/Core/Executor.h2
-rw-r--r--lib/Core/PTree.cpp35
-rw-r--r--lib/Core/PTree.h36
-rw-r--r--lib/Core/Searcher.cpp6
5 files changed, 42 insertions, 58 deletions
diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 56753bb1..1ba6d9bf 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -430,7 +430,7 @@ Executor::Executor(LLVMContext &ctx, const InterpreterOptions &opts,
     : Interpreter(opts), interpreterHandler(ih), searcher(0),
       externalDispatcher(new ExternalDispatcher(ctx)), statsTracker(0),
       pathWriter(0), symPathWriter(0), specialFunctionHandler(0),
-      processTree(0), replayKTest(0), replayPath(0), usingSeeds(0),
+      replayKTest(0), replayPath(0), usingSeeds(0),
       atMemoryLimit(false), inhibitForking(false), haltExecution(false),
       ivcEnabled(false), debugLogBuffer(debugBufferString) {
 
@@ -551,7 +551,6 @@ Executor::setModule(std::vector<std::unique_ptr<llvm::Module>> &modules,
 Executor::~Executor() {
   delete memory;
   delete externalDispatcher;
-  delete processTree;
   delete specialFunctionHandler;
   delete statsTracker;
   delete solver;
@@ -825,11 +824,7 @@ void Executor::branch(ExecutionState &state,
       ExecutionState *ns = es->branch();
       addedStates.push_back(ns);
       result.push_back(ns);
-      es->ptreeNode->data = 0;
-      std::pair<PTree::Node*,PTree::Node*> res = 
-        processTree->split(es->ptreeNode, ns, es);
-      ns->ptreeNode = res.first;
-      es->ptreeNode = res.second;
+      processTree->attach(es->ptreeNode, ns, es);
     }
   }
 
@@ -1077,11 +1072,7 @@ Executor::fork(ExecutionState &current, ref<Expr> condition, bool isInternal) {
       }
     }
 
-    current.ptreeNode->data = 0;
-    std::pair<PTree::Node*, PTree::Node*> res =
-      processTree->split(current.ptreeNode, falseState, trueState);
-    falseState->ptreeNode = res.first;
-    trueState->ptreeNode = res.second;
+    processTree->attach(current.ptreeNode, falseState, trueState);
 
     if (pathWriter) {
       // Need to update the pathOS.id field of falseState, otherwise the same id
@@ -3847,11 +3838,9 @@ void Executor::runFunctionAsMain(Function *f,
   
   initializeGlobals(*state);
 
-  processTree = new PTree(state);
-  state->ptreeNode = processTree->root;
+  processTree = std::make_unique<PTree>(state);
   run(*state);
-  delete processTree;
-  processTree = 0;
+  processTree = nullptr;
 
   // hack to clear memory objects
   delete memory;
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index 851a52ec..c3111713 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -136,7 +136,7 @@ private:
   TreeStreamWriter *pathWriter, *symPathWriter;
   SpecialFunctionHandler *specialFunctionHandler;
   std::vector<TimerInfo*> timers;
-  PTree *processTree;
+  std::unique_ptr<PTree> processTree;
 
   /// Keeps track of all currently ongoing merges.
   /// An ongoing merge is a set of states which branched from a single state
diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp
index 67a6e967..9747e814 100644
--- a/lib/Core/PTree.cpp
+++ b/lib/Core/PTree.cpp
@@ -9,6 +9,7 @@
 
 #include "PTree.h"
 
+#include "klee/ExecutionState.h"
 #include "klee/Expr/Expr.h"
 #include "klee/Expr/ExprPPrinter.h"
 
@@ -16,22 +17,23 @@
 
 using namespace klee;
 
-PTree::PTree(const data_type &root) : root(new Node(nullptr, root)) {}
+PTree::PTree(ExecutionState *initialState) {
+  root = new PTreeNode(nullptr, initialState);
+  initialState->ptreeNode = root;
+}
+
+void PTree::attach(PTreeNode *node, ExecutionState *leftState, ExecutionState *rightState) {
+  assert(node && !node->left && !node->right);
 
-std::pair<PTreeNode*, PTreeNode*>
-PTree::split(Node *n, 
-             const data_type &leftData, 
-             const data_type &rightData) {
-  assert(n && !n->left && !n->right);
-  n->left = new Node(n, leftData);
-  n->right = new Node(n, rightData);
-  return std::make_pair(n->left, n->right);
+  node->state = nullptr;
+  node->left = new PTreeNode(node, leftState);
+  node->right = new PTreeNode(node, rightState);
 }
 
-void PTree::remove(Node *n) {
+void PTree::remove(PTreeNode *n) {
   assert(!n->left && !n->right);
   do {
-    Node *p = n->parent;
+    PTreeNode *p = n->parent;
     if (p) {
       if (n == p->left) {
         p->left = nullptr;
@@ -55,13 +57,13 @@ void PTree::dump(llvm::raw_ostream &os) {
   os << "\tcenter = \"true\";\n";
   os << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n";
   os << "\tedge [arrowsize=.3]\n";
-  std::vector<PTree::Node*> stack;
+  std::vector<const PTreeNode*> stack;
   stack.push_back(root);
   while (!stack.empty()) {
-    PTree::Node *n = stack.back();
+    const PTreeNode *n = stack.back();
     stack.pop_back();
     os << "\tn" << n << " [shape=diamond";
-    if (n->data)
+    if (n->state)
       os << ",fillcolor=green";
     os << "];\n";
     if (n->left) {
@@ -77,6 +79,7 @@ void PTree::dump(llvm::raw_ostream &os) {
   delete pp;
 }
 
-PTreeNode::PTreeNode(PTreeNode * parent, ExecutionState * data)
-  : parent{parent}, data{data} {}
+PTreeNode::PTreeNode(PTreeNode *parent, ExecutionState *state) : parent{parent}, state{state} {
+  state->ptreeNode = this;
+}
 
diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h
index 7618e86e..6456b57f 100644
--- a/lib/Core/PTree.h
+++ b/lib/Core/PTree.h
@@ -15,36 +15,28 @@
 namespace klee {
   class ExecutionState;
 
-  class PTree { 
-    typedef ExecutionState* data_type;
-
-  public:
-    typedef class PTreeNode Node;
-    Node *root;
-
-    explicit PTree(const data_type &_root);
-    ~PTree() = default;
-    
-    std::pair<Node*,Node*> split(Node *n,
-                                 const data_type &leftData,
-                                 const data_type &rightData);
-    void remove(Node *n);
-
-    void dump(llvm::raw_ostream &os);
-  };
-
   class PTreeNode {
-    friend class PTree;
   public:
     PTreeNode *parent = nullptr;
     PTreeNode *left = nullptr;
     PTreeNode *right = nullptr;
-    ExecutionState *data = nullptr;
+    ExecutionState *state = nullptr;
 
-  private:
-    PTreeNode(PTreeNode * parent, ExecutionState * data);
+    PTreeNode(const PTreeNode&) = delete;
+    PTreeNode(PTreeNode *parent, ExecutionState *state);
     ~PTreeNode() = default;
   };
+
+  class PTree {
+  public:
+    PTreeNode * root = nullptr;
+    explicit PTree(ExecutionState *initialState);
+    ~PTree() = default;
+
+    static void attach(PTreeNode *node, ExecutionState *leftState, ExecutionState *rightState);
+    static void remove(PTreeNode *node);
+    void dump(llvm::raw_ostream &os);
+  };
 }
 
 #endif /* KLEE_PTREE_H */
diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp
index 49f6e52b..8d35b7ef 100644
--- a/lib/Core/Searcher.cpp
+++ b/lib/Core/Searcher.cpp
@@ -264,8 +264,8 @@ RandomPathSearcher::~RandomPathSearcher() {
 
 ExecutionState &RandomPathSearcher::selectState() {
   unsigned flips=0, bits=0;
-  PTree::Node *n = executor.processTree->root;
-  while (!n->data) {
+  PTreeNode *n = executor.processTree->root;
+  while (!n->state) {
     if (!n->left) {
       n = n->right;
     } else if (!n->right) {
@@ -280,7 +280,7 @@ ExecutionState &RandomPathSearcher::selectState() {
     }
   }
 
-  return *n->data;
+  return *n->state;
 }
 
 void
generated by cgit-pink 1.4.1 (git 2.36.1) at 2024-11-11 09:35:48 +0000