klee
|
#include <Searcher.h>
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... | |
![]() | |
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 | |
![]() | |
enum | CoreSearchType : std::uint8_t { DFS , BFS , RandomState , RandomPath , NURS_CovNew , NURS_MD2U , NURS_Depth , NURS_RP , NURS_ICnt , NURS_CPICnt , NURS_QC } |
Definition at line 198 of file Searcher.h.
|
explicit |
baseSearcher | The underlying searcher (takes ownership). |
Definition at line 345 of file Searcher.cpp.
|
overridedefault |
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().
|
overridevirtual |
Implements klee::Searcher.
Definition at line 400 of file Searcher.cpp.
References baseSearcher.
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().
|
overridevirtual |
Prints name of searcher as a klee_message()
.
Implements klee::Searcher.
Definition at line 404 of file Searcher.cpp.
|
overridevirtual |
Selects a state for further exploration.
Implements klee::Searcher.
Definition at line 361 of file Searcher.cpp.
References baseSearcher, klee::DebugLogIncompleteMerge, mergeGroups, and klee::UseIncompleteMerge.
|
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 390 of file Searcher.cpp.
References baseSearcher, and pausedStates.
|
friend |
Definition at line 199 of file Searcher.h.
|
private |
Definition at line 203 of file Searcher.h.
Referenced by continueState(), empty(), pauseState(), selectState(), and update().
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().
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().
|
private |
States that have been paused by the 'pauseState' function.
Definition at line 206 of file Searcher.h.
Referenced by continueState(), pauseState(), and update().