klee::InterleavedSearcher Class Reference

#include <Searcher.h>

Inheritance diagram for klee::InterleavedSearcher:

Collaboration diagram for klee::InterleavedSearcher:

Public Member Functions
	InterleavedSearcher (const std::vector< Searcher * > &searchers)
	~InterleavedSearcher () 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
std::vector< std::unique_ptr< Searcher > >	searchers
unsigned	index {1}

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

InterleavedSearcher selects states from a set of searchers in round-robin manner. It is used for KLEE's default strategy where it switches between RandomPathSearcher and WeightedRandomSearcher with CoveringNew metric.

Definition at line 295 of file Searcher.h.

Constructor & Destructor Documentation

InterleavedSearcher()

InterleavedSearcher::InterleavedSearcher ( const std::vector< Searcher * > &  searchers )

explicit

Parameters

searchers

The underlying searchers (takes ownership).

Definition at line 524 of file Searcher.cpp.

References searchers.

~InterleavedSearcher()

klee::InterleavedSearcher::~InterleavedSearcher ( )

overridedefault

Member Function Documentation

empty()

bool InterleavedSearcher::empty ( )

overridevirtual

Returns

True if no state left for exploration, False otherwise

Implements klee::Searcher.

Definition at line 545 of file Searcher.cpp.

References searchers.

printName()

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

overridevirtual

Prints name of searcher as a klee_message().

Implements klee::Searcher.

Definition at line 549 of file Searcher.cpp.

References searchers.

selectState()

ExecutionState & InterleavedSearcher::selectState ( )

overridevirtual

Selects a state for further exploration.

Returns

The selected state.

Implements klee::Searcher.

Definition at line 530 of file Searcher.cpp.

References index, searchers, and klee::Searcher::selectState().

Here is the call graph for this function:

update()

void InterleavedSearcher::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 536 of file Searcher.cpp.

References searchers.

Member Data Documentation

index

unsigned klee::InterleavedSearcher::index {1}

private

Definition at line 297 of file Searcher.h.

Referenced by selectState().

searchers

std::vector<std::unique_ptr<Searcher> > klee::InterleavedSearcher::searchers

private

Definition at line 296 of file Searcher.h.

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

---

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