From d773e3f762affd7189d34fbd6d1e7e0e5af3f712 Mon Sep 17 00:00:00 2001 From: Frank Busse Date: Wed, 11 Sep 2019 21:19:24 +0100 Subject: refactor PTree: remove split(), add attach() method --- lib/Core/Executor.cpp | 21 +++++---------------- lib/Core/Executor.h | 2 +- lib/Core/PTree.cpp | 35 +++++++++++++++++++---------------- lib/Core/PTree.h | 36 ++++++++++++++---------------------- lib/Core/Searcher.cpp | 6 +++--- 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> &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 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 ¤t, ref condition, bool isInternal) { } } - current.ptreeNode->data = 0; - std::pair 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(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 timers; - PTree *processTree; + std::unique_ptr 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 -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 stack; + std::vector 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 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 -- cgit 1.4.1