klee
|
#include <Searcher.h>
Public Member Functions | |
RandomPathSearcher (PTree &processTree, RNG &rng) | |
~RandomPathSearcher () override=default | |
ExecutionState & | selectState () override |
void | update (ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates) override |
bool | empty () override |
void | printName (llvm::raw_ostream &os) override |
Prints name of searcher as a klee_message() . More... | |
![]() | |
virtual | ~Searcher ()=default |
virtual ExecutionState & | selectState ()=0 |
virtual void | update (ExecutionState *current, const std::vector< ExecutionState * > &addedStates, const std::vector< ExecutionState * > &removedStates)=0 |
virtual bool | empty ()=0 |
virtual void | printName (llvm::raw_ostream &os)=0 |
Prints name of searcher as a klee_message() . More... | |
Private Attributes | |
PTree & | processTree |
RNG & | theRNG |
const uint8_t | idBitMask |
Additional Inherited Members | |
![]() | |
enum | CoreSearchType : std::uint8_t { DFS , BFS , RandomState , RandomPath , NURS_CovNew , NURS_MD2U , NURS_Depth , NURS_RP , NURS_ICnt , NURS_CPICnt , NURS_QC } |
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 the PTreeNodePtr class (which hides it in the pointer itself).
The current implementation of PTreeNodePtr supports only 3 instances of the RandomPathSearcher. This is because the current PTreeNodePtr implementation conforms to C++ and only steals the last 3 alignment 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.
Definition at line 174 of file Searcher.h.
processTree | The process tree. |
RNG | A random number generator. |
Definition at line 260 of file Searcher.cpp.
|
overridedefault |
|
overridevirtual |
Implements klee::Searcher.
Definition at line 334 of file Searcher.cpp.
References IS_OUR_NODE_VALID, processTree, and klee::PTree::root.
|
overridevirtual |
Prints name of searcher as a klee_message()
.
Implements klee::Searcher.
Definition at line 338 of file Searcher.cpp.
|
overridevirtual |
Selects a state for further exploration.
Implements klee::Searcher.
Definition at line 265 of file Searcher.cpp.
References klee::RNG::getInt32(), idBitMask, IS_OUR_NODE_VALID, klee::PTreeNode::left, processTree, klee::PTreeNode::right, klee::PTree::root, klee::PTreeNode::state, and theRNG.
|
overridevirtual |
Notifies searcher about new or deleted states.
current | The currently selected state for exploration. |
addedStates | The newly branched states with current as common ancestor. |
removedStates | The states that will be terminated. |
Implements klee::Searcher.
Definition at line 291 of file Searcher.cpp.
References idBitMask, IS_OUR_NODE_VALID, klee::PTreeNode::left, klee::PTreeNode::parent, processTree, klee::PTreeNode::right, and klee::PTree::root.
|
private |
Definition at line 179 of file Searcher.h.
Referenced by selectState(), and update().
|
private |
Definition at line 175 of file Searcher.h.
Referenced by empty(), selectState(), and update().
|
private |
Definition at line 176 of file Searcher.h.
Referenced by selectState().