klee::RandomPathSearcher Class Reference

#include <Searcher.h>

Inheritance diagram for klee::RandomPathSearcher:

Collaboration diagram for klee::RandomPathSearcher:

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...
Public Member Functions inherited from klee::Searcher
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
Public Types inherited from klee::Searcher
enum	CoreSearchType : std::uint8_t {   DFS , BFS , RandomState , RandomPath ,   NURS_CovNew , NURS_MD2U , NURS_Depth , NURS_RP ,   NURS_ICnt , NURS_CPICnt , NURS_QC }

Detailed Description

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.

Constructor & Destructor Documentation

RandomPathSearcher()

RandomPathSearcher::RandomPathSearcher	(	PTree &	processTree,
		RNG &	rng
	)

Parameters

processTree	The process tree.
RNG	A random number generator.

Definition at line 260 of file Searcher.cpp.

~RandomPathSearcher()

klee::RandomPathSearcher::~RandomPathSearcher ( )

overridedefault

Member Function Documentation

empty()

bool RandomPathSearcher::empty ( )

overridevirtual

Returns

True if no state left for exploration, False otherwise

Implements klee::Searcher.

Definition at line 334 of file Searcher.cpp.

References IS_OUR_NODE_VALID, processTree, and klee::PTree::root.

printName()

void RandomPathSearcher::printName ( llvm::raw_ostream &  os )

overridevirtual

Prints name of searcher as a klee_message().

Implements klee::Searcher.

Definition at line 338 of file Searcher.cpp.

selectState()

ExecutionState & RandomPathSearcher::selectState ( )

overridevirtual

Selects a state for further exploration.

Returns

The selected state.

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.

Here is the call graph for this function:

update()

void RandomPathSearcher::update ( ExecutionState *  current, const std::vector< ExecutionState * > &  addedStates, const std::vector< ExecutionState * > &  removedStates  )

overridevirtual

Notifies searcher about new or deleted states.

Parameters

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.

Member Data Documentation

idBitMask

const uint8_t klee::RandomPathSearcher::idBitMask

private

Definition at line 179 of file Searcher.h.

Referenced by selectState(), and update().

processTree

PTree& klee::RandomPathSearcher::processTree

private

Definition at line 175 of file Searcher.h.

Referenced by empty(), selectState(), and update().

theRNG

RNG& klee::RandomPathSearcher::theRNG

private

Definition at line 176 of file Searcher.h.

Referenced by selectState().

---

The documentation for this class was generated from the following files:

• /Users/cristic/klee/lib/Core/Searcher.h
• /Users/cristic/klee/lib/Core/Searcher.cpp