diff options
| author | Frank Busse <bb0xfb@gmail.com> | 2023-03-24 21:14:02 +0000 |
|---|---|---|
| committer | MartinNowack <2443641+MartinNowack@users.noreply.github.com> | 2024-01-12 12:00:35 +0000 |
| commit | 19b6ae578b0658115d15848604a28434845bb3e3 (patch) | |
| tree | 31d52545929760ad725385bd1cdc1153b710fc75 /lib/Core/Searcher.cpp | |
| parent | fc83f06b17221bf5ef20e30d9da1ccff927beb17 (diff) | |
| download | klee-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.cpp | 23 |
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) { |
