aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/Core
diff options
context:
space:
mode:
authorTimotej Kapus <tk1713@ic.ac.uk>2019-10-17 15:58:26 +0100
committerCristian Cadar <c.cadar@imperial.ac.uk>2020-06-29 22:24:53 +0100
commitd591cba305cb86ee8c520b7ff427651d8f9e0f31 (patch)
tree234eacb760b85d4c21daebfa879731f7ba9f37c3 /lib/Core
parent1d357591bd80e7157d29009691d632eddff971f5 (diff)
downloadklee-d591cba305cb86ee8c520b7ff427651d8f9e0f31.tar.gz
Enable subsets for RandomPathSearcher
Diffstat (limited to 'lib/Core')
-rw-r--r--lib/Core/ExecutionState.cpp1
-rw-r--r--lib/Core/ExecutionState.h7
-rw-r--r--lib/Core/Executor.h3
-rw-r--r--lib/Core/PTree.cpp27
-rw-r--r--lib/Core/PTree.h26
-rw-r--r--lib/Core/Searcher.cpp64
-rw-r--r--lib/Core/Searcher.h26
-rw-r--r--lib/Core/UserSearcher.cpp12
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);
}