klee::BatchingSearcher Class Reference

#include <Searcher.h>

Inheritance diagram for klee::BatchingSearcher:

Collaboration diagram for klee::BatchingSearcher:

Public Member Functions
	BatchingSearcher (Searcher *baseSearcher, time::Span timeBudget, unsigned instructionBudget)
	~BatchingSearcher () 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::unique_ptr< Searcher >	baseSearcher
time::Span	timeBudget
unsigned	instructionBudget
ExecutionState *	lastState {nullptr}
time::Point	lastStartTime
unsigned	lastStartInstructions

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

BatchingSearcher selects a state from an underlying searcher and returns that state for further exploration for a given time or a given number of instructions.

Definition at line 244 of file Searcher.h.

Constructor & Destructor Documentation

BatchingSearcher()

BatchingSearcher::BatchingSearcher	(	Searcher *	baseSearcher,
		time::Span	timeBudget,
		unsigned	instructionBudget
	)

Parameters

baseSearcher	The underlying searcher (takes ownership).
timeBudget	Time span a state gets selected before choosing a different one.
instructionBudget	Number of instructions to re-select a state for.

Definition at line 411 of file Searcher.cpp.

~BatchingSearcher()

klee::BatchingSearcher::~BatchingSearcher ( )

overridedefault

Member Function Documentation

empty()

bool BatchingSearcher::empty ( )

overridevirtual

Returns

True if no state left for exploration, False otherwise

Implements klee::Searcher.

Definition at line 450 of file Searcher.cpp.

References baseSearcher.

printName()

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

overridevirtual

Prints name of searcher as a klee_message().

Implements klee::Searcher.

Definition at line 454 of file Searcher.cpp.

References baseSearcher, instructionBudget, and timeBudget.

selectState()

ExecutionState & BatchingSearcher::selectState ( )

overridevirtual

Selects a state for further exploration.

Returns

The selected state.

Implements klee::Searcher.

Definition at line 416 of file Searcher.cpp.

References baseSearcher, klee::time::getWallTime(), instructionBudget, klee::stats::instructions, klee::klee_message(), lastStartInstructions, lastStartTime, lastState, timeBudget, and klee::time::Span::toSeconds().

Here is the call graph for this function:

update()

void BatchingSearcher::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 440 of file Searcher.cpp.

References baseSearcher, and lastState.

Member Data Documentation

baseSearcher

std::unique_ptr<Searcher> klee::BatchingSearcher::baseSearcher

private

Definition at line 245 of file Searcher.h.

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

instructionBudget

unsigned klee::BatchingSearcher::instructionBudget

private

Definition at line 247 of file Searcher.h.

Referenced by printName(), and selectState().

lastStartInstructions

unsigned klee::BatchingSearcher::lastStartInstructions

private

Definition at line 251 of file Searcher.h.

Referenced by selectState().

lastStartTime

time::Point klee::BatchingSearcher::lastStartTime

private

Definition at line 250 of file Searcher.h.

Referenced by selectState().

lastState

ExecutionState* klee::BatchingSearcher::lastState {nullptr}

private

Definition at line 249 of file Searcher.h.

Referenced by selectState(), and update().

timeBudget

time::Span klee::BatchingSearcher::timeBudget

private

Definition at line 246 of file Searcher.h.

Referenced by printName(), and 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