klee::WeightedRandomSearcher Class Reference

#include <Searcher.h>

Inheritance diagram for klee::WeightedRandomSearcher:

Collaboration diagram for klee::WeightedRandomSearcher:

Public Types
enum	WeightType : std::uint8_t {   Depth , RP , QueryCost , InstCount ,   CPInstCount , MinDistToUncovered , CoveringNew }
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 }

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...
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 Member Functions
double	getWeight (ExecutionState *)

Private Attributes
std::unique_ptr< DiscretePDF< ExecutionState *, ExecutionStateIDCompare > >	states
RNG &	theRNG
WeightType	type
bool	updateWeights

Detailed Description

The base class for all weighted searchers. Uses DiscretePDF as underlying data structure.

Definition at line 125 of file Searcher.h.

Member Enumeration Documentation

WeightType

enum klee::WeightedRandomSearcher::WeightType : std::uint8_t

Enumerator
Depth
RP
QueryCost
InstCount
CPInstCount
MinDistToUncovered
CoveringNew

Definition at line 127 of file Searcher.h.

Constructor & Destructor Documentation

WeightedRandomSearcher()

WeightedRandomSearcher::WeightedRandomSearcher	(	WeightType	type,
		RNG &	rng
	)

Parameters

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.

~WeightedRandomSearcher()

klee::WeightedRandomSearcher::~WeightedRandomSearcher ( )

overridedefault

Member Function Documentation

empty()

bool WeightedRandomSearcher::empty ( )

overridevirtual

Returns

True if no state left for exploration, False otherwise

Implements klee::Searcher.

Definition at line 235 of file Searcher.cpp.

References states.

getWeight()

double WeightedRandomSearcher::getWeight ( ExecutionState *  es )

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().

Here is the call graph for this function:

Here is the caller graph for this function:

printName()

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

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.

selectState()

ExecutionState & WeightedRandomSearcher::selectState ( )

overridevirtual

Selects a state for further exploration.

Returns

The selected state.

Implements klee::Searcher.

Definition at line 172 of file Searcher.cpp.

References klee::RNG::getDoubleL(), states, and theRNG.

Here is the call graph for this function:

update()

void WeightedRandomSearcher::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 217 of file Searcher.cpp.

References getWeight(), states, and updateWeights.

Here is the call graph for this function:

Member Data Documentation

states

std::unique_ptr<DiscretePDF<ExecutionState*, ExecutionStateIDCompare> > klee::WeightedRandomSearcher::states

private

Definition at line 138 of file Searcher.h.

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

theRNG

RNG& klee::WeightedRandomSearcher::theRNG

private

Definition at line 139 of file Searcher.h.

Referenced by selectState().

type

WeightType klee::WeightedRandomSearcher::type

private

Definition at line 140 of file Searcher.h.

Referenced by getWeight(), printName(), and WeightedRandomSearcher().

updateWeights

bool klee::WeightedRandomSearcher::updateWeights

private

Definition at line 141 of file Searcher.h.

Referenced by update(), and WeightedRandomSearcher().

---

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