diff options
author | Timotej Kapus <tk1713@ic.ac.uk> | 2019-10-17 15:58:26 +0100 |
---|---|---|
committer | Cristian Cadar <c.cadar@imperial.ac.uk> | 2020-06-29 22:24:53 +0100 |
commit | d591cba305cb86ee8c520b7ff427651d8f9e0f31 (patch) | |
tree | 234eacb760b85d4c21daebfa879731f7ba9f37c3 /lib | |
parent | 1d357591bd80e7157d29009691d632eddff971f5 (diff) | |
download | klee-d591cba305cb86ee8c520b7ff427651d8f9e0f31.tar.gz |
Enable subsets for RandomPathSearcher
Diffstat (limited to 'lib')
-rw-r--r-- | lib/Core/ExecutionState.cpp | 1 | ||||
-rw-r--r-- | lib/Core/ExecutionState.h | 7 | ||||
-rw-r--r-- | lib/Core/Executor.h | 3 | ||||
-rw-r--r-- | lib/Core/PTree.cpp | 27 | ||||
-rw-r--r-- | lib/Core/PTree.h | 26 | ||||
-rw-r--r-- | lib/Core/Searcher.cpp | 64 | ||||
-rw-r--r-- | lib/Core/Searcher.h | 26 | ||||
-rw-r--r-- | lib/Core/UserSearcher.cpp | 12 |
8 files changed, 134 insertions, 32 deletions
diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 7b600003..14d596fc 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -105,7 +105,6 @@ ExecutionState::ExecutionState(const ExecutionState& state): pathOS(state.pathOS), symPathOS(state.symPathOS), coveredLines(state.coveredLines), - ptreeNode(state.ptreeNode), symbolics(state.symbolics), arrayNames(state.arrayNames), openMergeStack(state.openMergeStack), diff --git a/lib/Core/ExecutionState.h b/lib/Core/ExecutionState.h index e7332472..f1b09644 100644 --- a/lib/Core/ExecutionState.h +++ b/lib/Core/ExecutionState.h @@ -111,7 +111,8 @@ public: std::map<const std::string *, std::set<std::uint32_t>> coveredLines; /// @brief Pointer to the process tree of the current state - PTreeNode *ptreeNode; + /// Copies of ExecutionState should not copy ptreeNode + PTreeNode *ptreeNode = nullptr; /// @brief Ordered list of symbolics: used to generate test cases. // @@ -144,6 +145,10 @@ public: bool forkDisabled; public: + #ifdef KLEE_UNITTEST + // provide this function only in the context of unittests + ExecutionState(){} + #endif // only to create the initial state explicit ExecutionState(KFunction *kf); // XXX total hack, just used to make a state so solver can diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index d27fa503..31882cd4 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -16,6 +16,7 @@ #define KLEE_EXECUTOR_H #include "ExecutionState.h" +#include "UserSearcher.h" #include "klee/Core/Interpreter.h" #include "klee/Expr/ArrayCache.h" @@ -84,12 +85,12 @@ namespace klee { /// removedStates, and haltExecution, among others. class Executor : public Interpreter { - friend class RandomPathSearcher; friend class OwningSearcher; friend class WeightedRandomSearcher; friend class SpecialFunctionHandler; friend class StatsTracker; friend class MergeHandler; + friend klee::Searcher *klee::constructUserSearcher(Executor &executor); public: typedef std::pair<ExecutionState*,ExecutionState*> StatePair; diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp index 2962e3c2..244e8520 100644 --- a/lib/Core/PTree.cpp +++ b/lib/Core/PTree.cpp @@ -14,20 +14,29 @@ #include "klee/Expr/Expr.h" #include "klee/Expr/ExprPPrinter.h" +#include <bitset> #include <vector> using namespace klee; -PTree::PTree(ExecutionState *initialState) { - root = new PTreeNode(nullptr, initialState); - initialState->ptreeNode = root; +PTree::PTree(ExecutionState *initialState) + : root(PTreeNodePtr(new PTreeNode(nullptr, initialState))) { + initialState->ptreeNode = root.getPointer(); } void PTree::attach(PTreeNode *node, ExecutionState *leftState, ExecutionState *rightState) { assert(node && !node->left.getPointer() && !node->right.getPointer()); + assert(node == rightState->ptreeNode && + "Attach assumes the right state is the current state"); node->state = nullptr; node->left = PTreeNodePtr(new PTreeNode(node, leftState)); - node->right = PTreeNodePtr(new PTreeNode(node, rightState)); + // The current node inherits the tag + uint8_t currentNodeTag = root.getInt(); + if (node->parent) + currentNodeTag = node->parent->left.getPointer() == node + ? node->parent->left.getInt() + : node->parent->right.getInt(); + node->right = PTreeNodePtr(new PTreeNode(node, rightState), currentNodeTag); } void PTree::remove(PTreeNode *n) { @@ -58,7 +67,7 @@ void PTree::dump(llvm::raw_ostream &os) { os << "\tnode [style=\"filled\",width=.1,height=.1,fontname=\"Terminus\"]\n"; os << "\tedge [arrowsize=.3]\n"; std::vector<const PTreeNode*> stack; - stack.push_back(root); + stack.push_back(root.getPointer()); while (!stack.empty()) { const PTreeNode *n = stack.back(); stack.pop_back(); @@ -67,11 +76,15 @@ void PTree::dump(llvm::raw_ostream &os) { os << ",fillcolor=green"; os << "];\n"; if (n->left.getPointer()) { - os << "\tn" << n << " -> n" << n->left.getPointer() << ";\n"; + os << "\tn" << n << " -> n" << n->left.getPointer(); + os << " [label=0b" + << std::bitset<PtrBitCount>(n->left.getInt()).to_string() << "];\n"; stack.push_back(n->left.getPointer()); } if (n->right.getPointer()) { - os << "\tn" << n << " -> n" << n->right.getPointer() << ";\n"; + os << "\tn" << n << " -> n" << n->right.getPointer(); + os << " [label=0b" + << std::bitset<PtrBitCount>(n->right.getInt()).to_string() << "];\n"; stack.push_back(n->right.getPointer()); } } diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h index 115ea83f..b1b6e9fc 100644 --- a/lib/Core/PTree.h +++ b/lib/Core/PTree.h @@ -11,13 +11,19 @@ #define KLEE_PTREE_H #include "klee/Expr/Expr.h" +#include "klee/Support/ErrorHandling.h" #include "llvm/ADT/PointerIntPair.h" namespace klee { class ExecutionState; class PTreeNode; - using PTreeNodePtr = llvm::PointerIntPair<PTreeNode*,3,uint8_t>; - + /* PTreeNodePtr is used by the Random Path Searcher object to efficiently + record which PTreeNode belongs to it. PTree is a global structure that + captures all states, whereas a Random Path Searcher might only care about + a subset. The integer part of PTreeNodePtr is a bitmask (a "tag") of which + Random Path Searchers PTreeNode belongs to. */ + constexpr int PtrBitCount = 3; + using PTreeNodePtr = llvm::PointerIntPair<PTreeNode *, PtrBitCount, uint8_t>; class PTreeNode { public: @@ -33,14 +39,26 @@ namespace klee { }; class PTree { + // Number of registered ID + int registeredIds = 0; + public: - PTreeNode * root = nullptr; + PTreeNodePtr root; explicit PTree(ExecutionState *initialState); ~PTree() = default; - static void attach(PTreeNode *node, ExecutionState *leftState, ExecutionState *rightState); + void attach(PTreeNode *node, ExecutionState *leftState, + ExecutionState *rightState); static void remove(PTreeNode *node); void dump(llvm::raw_ostream &os); + std::uint8_t getNextId() { + std::uint8_t id = 1 << registeredIds++; + if (registeredIds > PtrBitCount) { + klee_error("PTree cannot support more than %d RandomPathSearchers", + PtrBitCount); + } + return id; + } }; } diff --git a/lib/Core/Searcher.cpp b/lib/Core/Searcher.cpp index 27a92b49..6b7e9e49 100644 --- a/lib/Core/Searcher.cpp +++ b/lib/Core/Searcher.cpp @@ -259,21 +259,29 @@ bool WeightedRandomSearcher::empty() { return states->empty(); } -/// -RandomPathSearcher::RandomPathSearcher(Executor &_executor) - : executor(_executor) { -} +RandomPathSearcher::RandomPathSearcher(PTree &_processTree) + : processTree(_processTree), idBitMask(_processTree.getNextId()) {} RandomPathSearcher::~RandomPathSearcher() { } +// Check if n is a valid pointer and a node belonging to us +#define IS_OUR_NODE_VALID(n) \ + (((n).getPointer() != nullptr) && (((n).getInt() & idBitMask) != 0)) ExecutionState &RandomPathSearcher::selectState() { unsigned flips=0, bits=0; - PTreeNode *n = executor.processTree->root; + assert(processTree.root.getInt() & idBitMask && + "Root should belong to the searcher"); + PTreeNode *n = processTree.root.getPointer(); while (!n->state) { - if (!n->left.getPointer()) { + if (!IS_OUR_NODE_VALID(n->left)) { + assert(IS_OUR_NODE_VALID(n->right) && + "Both left and right nodes invalid"); + assert(n != n->right.getPointer()); n = n->right.getPointer(); - } else if (!n->right.getPointer()) { + } else if (!IS_OUR_NODE_VALID(n->right)) { + assert(IS_OUR_NODE_VALID(n->left) && "Both right and left nodes invalid"); + assert(n != n->left.getPointer()); n = n->left.getPointer(); } else { if (bits==0) { @@ -281,7 +289,7 @@ ExecutionState &RandomPathSearcher::selectState() { bits = 32; } --bits; - n = (flips&(1<<bits)) ? n->left.getPointer() : n->right.getPointer(); + n = ((flips & (1 << bits)) ? n->left : n->right).getPointer(); } } @@ -292,10 +300,46 @@ void RandomPathSearcher::update(ExecutionState *current, const std::vector<ExecutionState *> &addedStates, const std::vector<ExecutionState *> &removedStates) { + for (auto es : addedStates) { + PTreeNode *pnode = es->ptreeNode, *parent = pnode->parent; + PTreeNodePtr *childPtr; + + childPtr = parent ? ((parent->left.getPointer() == pnode) ? &parent->left + : &parent->right) + : &processTree.root; + while (pnode && !IS_OUR_NODE_VALID(*childPtr)) { + childPtr->setInt(childPtr->getInt() | idBitMask); + pnode = parent; + if (pnode) + parent = pnode->parent; + + childPtr = parent + ? ((parent->left.getPointer() == pnode) ? &parent->left + : &parent->right) + : &processTree.root; + } + } + + for (auto es : removedStates) { + PTreeNode *pnode = es->ptreeNode, *parent = pnode->parent; + + while (pnode && !IS_OUR_NODE_VALID(pnode->left) && + !IS_OUR_NODE_VALID(pnode->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"); + childPtr->setInt(childPtr->getInt() & ~idBitMask); + pnode = parent; + if (pnode) + parent = pnode->parent; + } + } } -bool RandomPathSearcher::empty() { - return executor.states.empty(); +bool RandomPathSearcher::empty() { + return !IS_OUR_NODE_VALID(processTree.root); } /// diff --git a/lib/Core/Searcher.h b/lib/Core/Searcher.h index b369057b..baeafd84 100644 --- a/lib/Core/Searcher.h +++ b/lib/Core/Searcher.h @@ -10,6 +10,7 @@ #ifndef KLEE_SEARCHER_H #define KLEE_SEARCHER_H +#include "PTree.h" #include "klee/System/Time.h" #include "llvm/Support/CommandLine.h" @@ -170,11 +171,32 @@ namespace klee { } }; + /* RandomPathSearcher performs a random walk of the PTree to + select a state. PTree is a global data structure, however + a searcher can sometimes only select from a subset of all states + (depending on the update calls). + + To support this RandomPathSearcher has a subgraph view of PTree, in that it + only + walks the PTreeNodes that it "owns". Ownership is stored in the + getInt method of PTreeNodePtr class (which hides it in the pointer itself). + + The current implementation of PTreeNodePtr supports only 3 instances of the + RandomPathSearcher. This is because current PTreeNodePtr implementation + conforms to C++ and only steals the last 3 alligment bits. This restriction + could be relaxed slightly by an architecture specific implementation of + PTreeNodePtr, that also steals the top bits of the pointer. + + The ownership bits are maintained in the update method. + */ class RandomPathSearcher : public Searcher { - Executor &executor; + PTree &processTree; + + // Unique bitmask of this searcher + const uint8_t idBitMask; public: - RandomPathSearcher(Executor &_executor); + RandomPathSearcher(PTree &processTree); ~RandomPathSearcher(); ExecutionState &selectState(); diff --git a/lib/Core/UserSearcher.cpp b/lib/Core/UserSearcher.cpp index 8dc32a40..42d6b334 100644 --- a/lib/Core/UserSearcher.cpp +++ b/lib/Core/UserSearcher.cpp @@ -104,14 +104,15 @@ bool klee::userSearcherRequiresMD2U() { std::find(CoreSearch.begin(), CoreSearch.end(), Searcher::NURS_QC) != CoreSearch.end()); } - -Searcher *getNewSearcher(Searcher::CoreSearchType type, Executor &executor) { +Searcher *getNewSearcher(Searcher::CoreSearchType type, PTree &processTree) { Searcher *searcher = NULL; switch (type) { case Searcher::DFS: searcher = new DFSSearcher(); break; case Searcher::BFS: searcher = new BFSSearcher(); break; case Searcher::RandomState: searcher = new RandomSearcher(); break; - case Searcher::RandomPath: searcher = new RandomPathSearcher(executor); break; + case Searcher::RandomPath: + searcher = new RandomPathSearcher(processTree); + break; case Searcher::NURS_CovNew: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::CoveringNew); break; case Searcher::NURS_MD2U: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::MinDistToUncovered); break; case Searcher::NURS_Depth: searcher = new WeightedRandomSearcher(WeightedRandomSearcher::Depth); break; @@ -126,14 +127,13 @@ Searcher *getNewSearcher(Searcher::CoreSearchType type, Executor &executor) { Searcher *klee::constructUserSearcher(Executor &executor) { - Searcher *searcher = getNewSearcher(CoreSearch[0], executor); - + Searcher *searcher = getNewSearcher(CoreSearch[0], *executor.processTree); if (CoreSearch.size() > 1) { std::vector<Searcher *> s; s.push_back(searcher); for (unsigned i = 1; i < CoreSearch.size(); i++) - s.push_back(getNewSearcher(CoreSearch[i], executor)); + s.push_back(getNewSearcher(CoreSearch[i], *executor.processTree)); searcher = new InterleavedSearcher(s); } |