klee
|
#include <Searcher.h>
Public Types | |
enum | WeightType : std::uint8_t { Depth , RP , QueryCost , InstCount , CPInstCount , MinDistToUncovered , CoveringNew } |
![]() | |
enum | CoreSearchType : std::uint8_t { DFS , BFS , RandomState , RandomPath , NURS_CovNew , NURS_MD2U , NURS_Depth , NURS_RP , NURS_ICnt , NURS_CPICnt , NURS_QC } |
Public Member Functions | |
WeightedRandomSearcher (WeightType type, RNG &rng) | |
~WeightedRandomSearcher () 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... | |
![]() | |
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 Member Functions | |
double | getWeight (ExecutionState *) |
Private Attributes | |
std::unique_ptr< DiscretePDF< ExecutionState *, ExecutionStateIDCompare > > | states |
RNG & | theRNG |
WeightType | type |
bool | updateWeights |
The base class for all weighted searchers. Uses DiscretePDF as underlying data structure.
Definition at line 125 of file Searcher.h.
enum klee::WeightedRandomSearcher::WeightType : std::uint8_t |
Enumerator | |
---|---|
Depth | |
RP | |
QueryCost | |
InstCount | |
CPInstCount | |
MinDistToUncovered | |
CoveringNew |
Definition at line 127 of file Searcher.h.
WeightedRandomSearcher::WeightedRandomSearcher | ( | WeightType | type, |
RNG & | rng | ||
) |
type | The WeightType that determines the underlying heuristic. |
RNG | A random number generator. |
Definition at line 150 of file Searcher.cpp.
References CoveringNew, CPInstCount, Depth, InstCount, MinDistToUncovered, QueryCost, RP, type, and updateWeights.
|
overridedefault |
|
overridevirtual |
Implements klee::Searcher.
Definition at line 235 of file Searcher.cpp.
References states.
|
private |
Definition at line 176 of file Searcher.cpp.
References klee::StackFrame::callPathNode, klee::computeMinDistToUncovered(), CoveringNew, CPInstCount, klee::ExecutionState::depth, Depth, klee::StatisticManager::getIndexedValue(), klee::StatisticRecord::getValue(), klee::InstructionInfo::id, klee::KInstruction::info, InstCount, klee::stats::instructions, klee::ExecutionState::instsSinceCovNew, MinDistToUncovered, klee::ExecutionState::pc, klee::SolverQueryMetaData::queryCost, QueryCost, klee::ExecutionState::queryMetaData, RP, klee::ExecutionState::stack, klee::CallPathNode::statistics, klee::theStatisticManager, klee::time::Span::toSeconds(), and type.
Referenced by update().
|
overridevirtual |
Prints name of searcher as a klee_message()
.
Implements klee::Searcher.
Definition at line 239 of file Searcher.cpp.
References CoveringNew, CPInstCount, Depth, InstCount, MinDistToUncovered, QueryCost, RP, and type.
|
overridevirtual |
Selects a state for further exploration.
Implements klee::Searcher.
Definition at line 172 of file Searcher.cpp.
References klee::RNG::getDoubleL(), states, and theRNG.
|
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 217 of file Searcher.cpp.
References getWeight(), states, and updateWeights.
|
private |
Definition at line 138 of file Searcher.h.
Referenced by empty(), selectState(), and update().
|
private |
Definition at line 139 of file Searcher.h.
Referenced by selectState().
|
private |
Definition at line 140 of file Searcher.h.
Referenced by getWeight(), printName(), and WeightedRandomSearcher().
|
private |
Definition at line 141 of file Searcher.h.
Referenced by update(), and WeightedRandomSearcher().