ExecutionState representing a path under exploration. More...

#include <ExecutionState.h>

Collaboration diagram for klee::ExecutionState:

[legend]

Public Types
using	stack_ty = std::vector< StackFrame >

Public Member Functions
	ExecutionState (KFunction *kf)

ExecutionState &	operator= (const ExecutionState &)=delete

	ExecutionState (ExecutionState &&) noexcept=delete

ExecutionState &	operator= (ExecutionState &&) noexcept=delete

	~ExecutionState ()

ExecutionState *	branch ()

void	pushFrame (KInstIterator caller, KFunction *kf)

void	popFrame ()

void	addSymbolic (const MemoryObject mo, const Array array)

void	addConstraint (ref< Expr > e)

void	addCexPreference (const ref< Expr > &cond)

bool	merge (const ExecutionState &b)

void	dumpStack (llvm::raw_ostream &out) const

std::uint32_t	getID () const

void	setID ()

Public Attributes
KInstIterator	pc
	Pointer to instruction to be executed after the current instruction. More...

KInstIterator	prevPC
	Pointer to instruction which is currently executed. More...

stack_ty	stack
	Stack representing the current instruction stream. More...

std::uint32_t	incomingBBIndex
	Remember from which Basic Block control flow arrived (i.e. to select the right phi values) More...

std::uint32_t	depth = 0
	Exploration depth, i.e., number of times KLEE branched for this state. More...

AddressSpace	addressSpace
	Address space used by this state (e.g. Global and Heap) More...

ConstraintSet	constraints
	Constraints collected so far. More...

SolverQueryMetaData	queryMetaData
	Statistics and information. More...

TreeOStream	pathOS
	History of complete path: represents branches taken to reach/create this state (both concrete and symbolic) More...

TreeOStream	symPathOS
	History of symbolic path: represents symbolic branches taken to reach/create this state. More...

std::map< const std::string *, std::set< std::uint32_t > >	coveredLines
	Set containing which lines in which files are covered by this state. More...

PTreeNode *	ptreeNode = nullptr
	Pointer to the process tree of the current state Copies of ExecutionState should not copy ptreeNode. More...

std::vector< std::pair< ref< const MemoryObject >, const Array * > >	symbolics
	Ordered list of symbolics: used to generate test cases. More...

ImmutableSet< ref< Expr > >	cexPreferences
	A set of boolean expressions the user has requested be true of a counterexample. More...

std::set< std::string >	arrayNames
	Set of used array names for this state. Used to avoid collisions. More...

std::vector< ref< MergeHandler > >	openMergeStack
	The objects handling the klee_open_merge calls this state ran through. More...

std::uint64_t	steppedInstructions = 0
	The numbers of times this state has run through Executor::stepInstruction. More...

std::uint32_t	instsSinceCovNew = 0
	Counts how many instructions were executed since the last new instruction was covered. More...

std::unique_ptr< UnwindingInformation >	unwindingInformation
	Keep track of unwinding state while unwinding, otherwise empty. More...

std::uint32_t	id = 0
	the state id More...

bool	coveredNew = false
	Whether a new instruction was covered in this state. More...

bool	forkDisabled = false
	Disables forking for this state. Set by user code. More...

Static Public Attributes
static std::uint32_t	nextID = 1
	the global state counter More...

Private Member Functions
	ExecutionState (const ExecutionState &state)

Detailed Description

ExecutionState representing a path under exploration.

Definition at line 147 of file ExecutionState.h.

Member Typedef Documentation

◆ stack_ty

using klee::ExecutionState::stack_ty = std::vector<StackFrame>

Definition at line 157 of file ExecutionState.h.

Constructor & Destructor Documentation

◆ ExecutionState() [1/3]

ExecutionState::ExecutionState ( const ExecutionState & state )

private

Definition at line 87 of file ExecutionState.cpp.

References openMergeStack.

Referenced by branch().

Here is the caller graph for this function:

◆ ExecutionState() [2/3]

ExecutionState::ExecutionState ( KFunction * kf )

explicit

Definition at line 73 of file ExecutionState.cpp.

References pushFrame(), and setID().

Here is the call graph for this function:

◆ ExecutionState() [3/3]

klee::ExecutionState::ExecutionState ( ExecutionState && )

deletenoexcept

◆ ~ExecutionState()

ExecutionState::~ExecutionState ( )

Definition at line 79 of file ExecutionState.cpp.

References openMergeStack, popFrame(), and stack.

Here is the call graph for this function:

Member Function Documentation

◆ addCexPreference()

void ExecutionState::addCexPreference ( const ref< Expr > & cond )

Definition at line 356 of file ExecutionState.cpp.

References cexPreferences.

◆ addConstraint()

void ExecutionState::addConstraint ( ref< Expr > e )

Definition at line 351 of file ExecutionState.cpp.

References klee::ConstraintManager::addConstraint(), and constraints.

Referenced by klee::Executor::addConstraint(), and klee::Executor::replaceReadWithSymbolic().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ addSymbolic()

void ExecutionState::addSymbolic	(	const MemoryObject *	mo,
		const Array *	array
	)

Definition at line 135 of file ExecutionState.cpp.

References symbolics.

Referenced by klee::Executor::executeMakeSymbolic().

Here is the caller graph for this function:

◆ branch()

ExecutionState * ExecutionState::branch ( )

Definition at line 113 of file ExecutionState.cpp.

References depth, and ExecutionState().

Referenced by klee::Executor::branch(), and klee::Executor::fork().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ dumpStack()

void ExecutionState::dumpStack ( llvm::raw_ostream & out ) const

Definition at line 317 of file ExecutionState.cpp.

References klee::InstructionInfo::assemblyLine, klee::StackFrame::caller, klee::InstructionInfo::file, klee::KFunction::function, klee::KFunction::getArgRegister(), klee::KInstruction::info, klee::StackFrame::kf, klee::InstructionInfo::line, klee::StackFrame::locals, prevPC, stack, and klee::Cell::value.

Referenced by klee::Executor::terminateStateOnError().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getID()

std::uint32_t klee::ExecutionState::getID ( ) const

inline

Definition at line 272 of file ExecutionState.h.

References id.

Referenced by klee::ExecutionStateIDCompare::operator()(), klee::Executor::printDebugInstructions(), and klee::Executor::terminateStateOnError().

Here is the caller graph for this function:

◆ merge()

bool ExecutionState::merge ( const ExecutionState & b )

◆ operator=() [1/2]

ExecutionState & klee::ExecutionState::operator= ( const ExecutionState & )

delete

◆ operator=() [2/2]

ExecutionState & klee::ExecutionState::operator= ( ExecutionState && )

deletenoexcept

◆ popFrame()

void ExecutionState::popFrame ( )

Definition at line 128 of file ExecutionState.cpp.

References addressSpace, klee::StackFrame::allocas, stack, and klee::AddressSpace::unbindObject().

Referenced by klee::Executor::executeInstruction(), klee::Executor::unwindToNextLandingpad(), and ~ExecutionState().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ pushFrame()

void ExecutionState::pushFrame	(	KInstIterator	caller,
		KFunction *	kf
	)

Definition at line 124 of file ExecutionState.cpp.

References stack.

Referenced by klee::Executor::executeCall(), ExecutionState(), and klee::Executor::unwindToNextLandingpad().

Here is the caller graph for this function:

◆ setID()

void klee::ExecutionState::setID ( )

inline

Definition at line 273 of file ExecutionState.h.

References nextID.

Referenced by ExecutionState().

Here is the caller graph for this function:

Member Data Documentation

◆ addressSpace

AddressSpace klee::ExecutionState::addressSpace

Address space used by this state (e.g. Global and Heap)

Definition at line 181 of file ExecutionState.h.

Referenced by klee::Executor::bindObjectInState(), klee::Executor::callExternalFunction(), klee::Executor::doImpliedValueConcretization(), klee::Executor::executeAlloc(), klee::Executor::executeCall(), klee::Executor::executeInstruction(), klee::Executor::executeMemoryOperation(), klee::Executor::getAddressInfo(), klee::Executor::initializeGlobalObjects(), merge(), popFrame(), klee::SpecialFunctionHandler::readStringAtAddress(), and klee::Executor::resolveExact().

◆ arrayNames

std::set<std::string> klee::ExecutionState::arrayNames

Set of used array names for this state. Used to avoid collisions.

Definition at line 216 of file ExecutionState.h.

Referenced by klee::Executor::executeMakeSymbolic().

◆ cexPreferences

ImmutableSet<ref<Expr> > klee::ExecutionState::cexPreferences

A set of boolean expressions the user has requested be true of a counterexample.

Definition at line 213 of file ExecutionState.h.

Referenced by addCexPreference(), and klee::Executor::getSymbolicSolution().

◆ constraints

ConstraintSet klee::ExecutionState::constraints

◆ coveredLines

std::map<const std::string *, std::set<std::uint32_t> > klee::ExecutionState::coveredLines

Set containing which lines in which files are covered by this state.

Definition at line 200 of file ExecutionState.h.

Referenced by klee::Executor::fork(), klee::Executor::getCoveredLines(), and klee::StatsTracker::stepInstruction().

◆ coveredNew

bool klee::ExecutionState::coveredNew = false

Whether a new instruction was covered in this state.

Definition at line 238 of file ExecutionState.h.

Referenced by klee::Executor::fork(), klee::StatsTracker::markBranchVisited(), shouldWriteTest(), and klee::StatsTracker::stepInstruction().

◆ depth

std::uint32_t klee::ExecutionState::depth = 0

Exploration depth, i.e., number of times KLEE branched for this state.

Definition at line 178 of file ExecutionState.h.

Referenced by branch(), and klee::WeightedRandomSearcher::getWeight().

◆ forkDisabled

bool klee::ExecutionState::forkDisabled = false

Disables forking for this state. Set by user code.

Definition at line 241 of file ExecutionState.h.

Referenced by klee::Executor::branchingPermitted(), and klee::Executor::fork().

◆ id

std::uint32_t klee::ExecutionState::id = 0

the state id

Definition at line 235 of file ExecutionState.h.

Referenced by getID().

◆ incomingBBIndex

std::uint32_t klee::ExecutionState::incomingBBIndex

Remember from which Basic Block control flow arrived (i.e. to select the right phi values)

Definition at line 173 of file ExecutionState.h.

Referenced by klee::Executor::executeInstruction(), and klee::Executor::transferToBasicBlock().

◆ instsSinceCovNew

std::uint32_t klee::ExecutionState::instsSinceCovNew = 0

Counts how many instructions were executed since the last new instruction was covered.

Definition at line 226 of file ExecutionState.h.

Referenced by klee::WeightedRandomSearcher::getWeight(), klee::StatsTracker::markBranchVisited(), and klee::StatsTracker::stepInstruction().

◆ nextID

std::uint32_t ExecutionState::nextID = 1

static

the global state counter

Definition at line 232 of file ExecutionState.h.

Referenced by setID().

◆ openMergeStack

std::vector<ref<MergeHandler> > klee::ExecutionState::openMergeStack

The objects handling the klee_open_merge calls this state ran through.

Definition at line 219 of file ExecutionState.h.

Referenced by ExecutionState(), and ~ExecutionState().

◆ pathOS

TreeOStream klee::ExecutionState::pathOS

History of complete path: represents branches taken to reach/create this state (both concrete and symbolic)

Definition at line 193 of file ExecutionState.h.

Referenced by klee::Executor::fork(), klee::Executor::getPathStreamID(), and klee::Executor::runFunctionAsMain().

◆ pc

KInstIterator klee::ExecutionState::pc

◆ prevPC

KInstIterator klee::ExecutionState::prevPC

Pointer to instruction which is currently executed.

Definition at line 166 of file ExecutionState.h.

Referenced by dumpStack(), klee::Executor::executeAlloc(), klee::Executor::executeCall(), klee::Executor::executeMemoryOperation(), klee::Executor::fork(), klee::Executor::getLastNonKleeInternalInstruction(), klee::Executor::maxStaticPctChecks(), klee::Executor::stepInstruction(), klee::Executor::terminateState(), and klee::Executor::unwindToNextLandingpad().

◆ ptreeNode

PTreeNode* klee::ExecutionState::ptreeNode = nullptr

Pointer to the process tree of the current state Copies of ExecutionState should not copy ptreeNode.

Definition at line 204 of file ExecutionState.h.

Referenced by klee::PTree::attach(), klee::Executor::branch(), klee::Executor::fork(), klee::PTree::PTree(), klee::PTreeNode::PTreeNode(), klee::Executor::terminateState(), and klee::Executor::updateStates().

◆ queryMetaData

SolverQueryMetaData klee::ExecutionState::queryMetaData

mutable

Statistics and information.

Metadata utilized and collected by solvers for this state

Definition at line 189 of file ExecutionState.h.

◆ stack

stack_ty klee::ExecutionState::stack

◆ steppedInstructions

std::uint64_t klee::ExecutionState::steppedInstructions = 0

The numbers of times this state has run through Executor::stepInstruction.

Definition at line 222 of file ExecutionState.h.

Referenced by klee::MergeHandler::getInstructionDistance(), and klee::Executor::stepInstruction().

◆ symbolics

std::vector<std::pair<ref<const MemoryObject>, const Array *> > klee::ExecutionState::symbolics

Ordered list of symbolics: used to generate test cases.

Definition at line 209 of file ExecutionState.h.

Referenced by addSymbolic(), klee::Executor::getSymbolicSolution(), and merge().

◆ symPathOS

TreeOStream klee::ExecutionState::symPathOS

History of symbolic path: represents symbolic branches taken to reach/create this state.

Definition at line 197 of file ExecutionState.h.

Referenced by klee::Executor::fork(), klee::Executor::getSymbolicPathStreamID(), and klee::Executor::runFunctionAsMain().

◆ unwindingInformation

std::unique_ptr<UnwindingInformation> klee::ExecutionState::unwindingInformation

Keep track of unwinding state while unwinding, otherwise empty.

Definition at line 229 of file ExecutionState.h.

Referenced by klee::Executor::executeInstruction(), and klee::Executor::unwindToNextLandingpad().

The documentation for this class was generated from the following files:

/Users/cristic/klee/lib/Core/ExecutionState.h
/Users/cristic/klee/lib/Core/ExecutionState.cpp

Public Types

Public Member Functions

Public Attributes

Static Public Attributes

Private Member Functions

Detailed Description

Member Typedef Documentation

◆ stack_ty

Constructor & Destructor Documentation

◆ ExecutionState() [1/3]

◆ ExecutionState() [2/3]

◆ ExecutionState() [3/3]

◆ ~ExecutionState()

Member Function Documentation

◆ addCexPreference()

◆ addConstraint()

◆ addSymbolic()

◆ branch()

◆ dumpStack()

◆ getID()

◆ merge()

◆ operator=() [1/2]

◆ operator=() [2/2]

◆ popFrame()

◆ pushFrame()

◆ setID()

Member Data Documentation

◆ addressSpace

◆ arrayNames

◆ cexPreferences

◆ constraints

◆ coveredLines

◆ coveredNew

◆ depth

◆ forkDisabled

◆ id

◆ incomingBBIndex

◆ instsSinceCovNew

◆ nextID

◆ openMergeStack

◆ pathOS

◆ pc

◆ prevPC

◆ ptreeNode

◆ queryMetaData

◆ stack

◆ steppedInstructions

◆ symbolics

◆ symPathOS

◆ unwindingInformation