klee::MergingSearcher Class Reference

#include <Searcher.h>

Inheritance diagram for klee::MergingSearcher:

Collaboration diagram for klee::MergingSearcher:

Public Member Functions
	MergingSearcher (Searcher *baseSearcher)
	~MergingSearcher () override=default
void	pauseState (ExecutionState &state)
void	continueState (ExecutionState &state)
	Continue a paused state. More...
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...

Public Attributes
std::set< ExecutionState * >	inCloseMerge
std::vector< MergeHandler * >	mergeGroups

Private Attributes
std::unique_ptr< Searcher >	baseSearcher
std::vector< ExecutionState * >	pausedStates
	States that have been paused by the 'pauseState' function. More...

Friends
class	MergeHandler

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

Definition at line 198 of file Searcher.h.

Constructor & Destructor Documentation

MergingSearcher()

MergingSearcher::MergingSearcher ( Searcher *  baseSearcher )

explicit

Parameters

baseSearcher

The underlying searcher (takes ownership).

Definition at line 345 of file Searcher.cpp.

~MergingSearcher()

klee::MergingSearcher::~MergingSearcher ( )

overridedefault

Member Function Documentation

continueState()

void MergingSearcher::continueState

(

ExecutionState &

state

)

Continue a paused state.

Definition at line 354 of file Searcher.cpp.

References baseSearcher, and pausedStates.

Referenced by klee::MergeHandler::releaseStates().

Here is the caller graph for this function:

empty()

bool MergingSearcher::empty ( )

overridevirtual

Returns

True if no state left for exploration, False otherwise

Implements klee::Searcher.

Definition at line 400 of file Searcher.cpp.

References baseSearcher.

pauseState()

void MergingSearcher::pauseState

(

ExecutionState &

state

)

Remove state from the searcher chain, while keeping it in the executor. This is used here to 'freeze' a state while it is waiting for other states in its merge group to reach the same instruction.

Definition at line 348 of file Searcher.cpp.

References baseSearcher, and pausedStates.

Referenced by klee::MergeHandler::addClosedState().

Here is the caller graph for this function:

printName()

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

overridevirtual

Prints name of searcher as a klee_message().

Implements klee::Searcher.

Definition at line 404 of file Searcher.cpp.

selectState()

ExecutionState & MergingSearcher::selectState ( )

overridevirtual

Selects a state for further exploration.

Returns

The selected state.

Implements klee::Searcher.

Definition at line 361 of file Searcher.cpp.

References baseSearcher, klee::DebugLogIncompleteMerge, mergeGroups, and klee::UseIncompleteMerge.

update()

void MergingSearcher::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 390 of file Searcher.cpp.

References baseSearcher, and pausedStates.

Friends And Related Function Documentation

MergeHandler

friend class MergeHandler

friend

Definition at line 199 of file Searcher.h.

Member Data Documentation

baseSearcher

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

private

Definition at line 203 of file Searcher.h.

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

inCloseMerge

std::set<ExecutionState *> klee::MergingSearcher::inCloseMerge

ExecutionStates currently paused from scheduling because they are waiting to be merged in a klee_close_merge instruction

Definition at line 215 of file Searcher.h.

Referenced by klee::MergeHandler::addClosedState(), klee::MergeHandler::getPrioritizeState(), and klee::MergeHandler::releaseStates().

mergeGroups

std::vector<MergeHandler *> klee::MergingSearcher::mergeGroups

Keeps track of all currently ongoing merges. An ongoing merge is a set of states (stored in a MergeHandler object) which branched from a single state which ran into a klee_open_merge(), and not all states in the set have reached the corresponding klee_close_merge() yet.

Definition at line 222 of file Searcher.h.

Referenced by klee::MergeHandler::MergeHandler(), selectState(), and klee::MergeHandler::~MergeHandler().

pausedStates

std::vector<ExecutionState*> klee::MergingSearcher::pausedStates

private

States that have been paused by the 'pauseState' function.

Definition at line 206 of file Searcher.h.

Referenced by continueState(), pauseState(), 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