klee::Executor Class Reference

#include <Executor.h>

Inheritance diagram for klee::Executor:

[legend]

Collaboration diagram for klee::Executor:

[legend]

List of all members.

Classes
class	Timer
class	TimerInfo
Public Types
typedef std::pair < ExecutionState *, ExecutionState * >	StatePair
Public Member Functions
	Executor (const InterpreterOptions &opts, InterpreterHandler *ie)
virtual	~Executor ()
const InterpreterHandler &	getHandler ()
ref< Expr >	evalConstant (llvm::Constant *c)
virtual void	setPathWriter (TreeStreamWriter *tsw)
virtual void	setSymbolicPathWriter (TreeStreamWriter *tsw)
virtual void	setReplayOut (const struct KTest *out)
virtual void	setReplayPath (const std::vector< bool > *path)
virtual const llvm::Module *	setModule (llvm::Module *module, const ModuleOptions &opts)
virtual void	useSeeds (const std::vector< struct KTest * > *seeds)
virtual void	runFunctionAsMain (llvm::Function *f, int argc, char **argv, char **envp)
virtual void	setHaltExecution (bool value)
virtual void	setInhibitForking (bool value)
virtual unsigned	getPathStreamID (const ExecutionState &state)
virtual unsigned	getSymbolicPathStreamID (const ExecutionState &state)
virtual void	getConstraintLog (const ExecutionState &state, std::string &res, bool asCVC=false)
virtual bool	getSymbolicSolution (const ExecutionState &state, std::vector< std::pair< std::string, std::vector< unsigned char > > > &res)
virtual void	getCoveredLines (const ExecutionState &state, std::map< const std::string *, std::set< unsigned > > &res)
Private Types
typedef std::vector< std::pair < std::pair< const MemoryObject *, const ObjectState * > , ExecutionState * > >	ExactResolutionList
Private Member Functions
llvm::Function *	getCalledFunction (llvm::CallSite &cs, ExecutionState &state)
void	executeInstruction (ExecutionState &state, KInstruction *ki)
void	printFileLine (ExecutionState &state, KInstruction *ki)
void	run (ExecutionState &initialState)
MemoryObject *	addExternalObject (ExecutionState &state, void *addr, unsigned size, bool isReadOnly)
void	initializeGlobalObject (ExecutionState &state, ObjectState *os, llvm::Constant *c, unsigned offset)
void	initializeGlobals (ExecutionState &state)
void	stepInstruction (ExecutionState &state)
void	updateStates (ExecutionState *current)
void	transferToBasicBlock (llvm::BasicBlock *dst, llvm::BasicBlock *src, ExecutionState &state)
void	callExternalFunction (ExecutionState &state, KInstruction *target, llvm::Function *function, std::vector< ref< Expr > > &arguments)
ObjectState *	bindObjectInState (ExecutionState &state, const MemoryObject *mo, bool isLocal)
void	resolveExact (ExecutionState &state, ref< Expr > p, ExactResolutionList &results, const std::string &name)
void	executeAlloc (ExecutionState &state, ref< Expr > size, bool isLocal, KInstruction *target, bool zeroMemory=false, const ObjectState *reallocFrom=0)
void	executeFree (ExecutionState &state, ref< Expr > address, KInstruction *target=0)
void	executeCall (ExecutionState &state, KInstruction *ki, llvm::Function *f, std::vector< ref< Expr > > &arguments)
void	executeMemoryOperation (ExecutionState &state, bool isWrite, ref< Expr > address, ref< Expr > value, KInstruction *target)
void	executeMakeSymbolic (ExecutionState &state, const MemoryObject *mo)
void	branch (ExecutionState &state, const std::vector< ref< Expr > > &conditions, std::vector< ExecutionState * > &result)
StatePair	fork (ExecutionState &current, ref< Expr > condition, bool isInternal)
void	addConstraint (ExecutionState &state, ref< Expr > condition)
ref< Expr >	replaceReadWithSymbolic (ExecutionState &state, ref< Expr > e)
const Cell &	eval (KInstruction *ki, unsigned index, ExecutionState &state) const
Cell &	getArgumentCell (ExecutionState &state, KFunction *kf, unsigned index)
Cell &	getDestCell (ExecutionState &state, KInstruction *target)
void	bindLocal (KInstruction *target, ExecutionState &state, ref< Expr > value)
void	bindArgument (KFunction *kf, unsigned index, ExecutionState &state, ref< Expr > value)
ref< Expr >	evalConstantExpr (llvm::ConstantExpr *ce)
ref< Expr >	toUnique (const ExecutionState &state, ref< Expr > &e)
ref< klee::ConstantExpr >	toConstant (ExecutionState &state, ref< Expr > e, const char *purpose)
void	executeGetValue (ExecutionState &state, ref< Expr > e, KInstruction *target)
std::string	getAddressInfo (ExecutionState &state, ref< Expr > address) const
	Get textual information regarding a memory address.
void	terminateState (ExecutionState &state)
void	terminateStateEarly (ExecutionState &state, std::string message)
void	terminateStateOnExit (ExecutionState &state)
void	terminateStateOnError (ExecutionState &state, const std::string &message, const std::string &suffix, const std::string &longMessage="")
void	terminateStateOnExecError (ExecutionState &state, const std::string &message, const std::string &info="")
void	bindModuleConstants ()
	bindModuleConstants - Initialize the module constant table.
void	bindInstructionConstants (KInstruction *KI)
void	handlePointsToObj (ExecutionState &state, KInstruction *target, const std::vector< ref< Expr > > &arguments)
void	doImpliedValueConcretization (ExecutionState &state, ref< Expr > e, ref< ConstantExpr > value)
void	addTimer (Timer *timer, double rate)
void	initTimers ()
void	processTimers (ExecutionState *current, double maxInstTime)
Private Attributes
KModule *	kmodule
InterpreterHandler *	interpreterHandler
Searcher *	searcher
ExternalDispatcher *	externalDispatcher
TimingSolver *	solver
MemoryManager *	memory
std::set< ExecutionState * >	states
StatsTracker *	statsTracker
TreeStreamWriter *	pathWriter
TreeStreamWriter *	symPathWriter
SpecialFunctionHandler *	specialFunctionHandler
std::vector< TimerInfo * >	timers
PTree *	processTree
std::set< ExecutionState * >	addedStates
std::set< ExecutionState * >	removedStates
std::map< ExecutionState *, std::vector< SeedInfo > >	seedMap
std::map< const llvm::GlobalValue *, MemoryObject * >	globalObjects
	Map of globals to their representative memory object.
std::map< const llvm::GlobalValue *, ref< Expr > >	globalAddresses
std::set< void * >	legalFunctions
struct KTest *	replayOut
const std::vector< bool > *	replayPath
	When non-null a list of branch decisions to be used for replay.
unsigned	replayPosition
const std::vector< struct KTest * > *	usingSeeds
bool	atMemoryLimit
bool	inhibitForking
	Disables forking, set by client.
bool	haltExecution
bool	ivcEnabled
double	stpTimeout
	The maximum time to allow for a single stp query.
Friends
class	BumpMergingSearcher
class	MergingSearcher
class	RandomPathSearcher
class	OwningSearcher
class	WeightedRandomSearcher
class	SpecialFunctionHandler
class	StatsTracker

---

Detailed Description

Todo:

Add a context object to keep track of data only live during an instruction step. Should contain addedStates, removedStates, and haltExecution, among others.

Definition at line 71 of file Executor.h.

---

Member Typedef Documentation

typedef std::vector< std::pair<std::pair<const MemoryObject*, const ObjectState*>, ExecutionState*> > klee::Executor::ExactResolutionList [private]

Resolve a pointer to the memory objects it could point to the start of, forking execution when necessary and generating errors for pointers to invalid locations (either out of bounds or address inside the middle of objects).

Parameters:

results[out]

A list of ((MemoryObject,ObjectState), state) pairs for each object the given address can point to the beginning of.

Definition at line 212 of file Executor.h.

typedef std::pair<ExecutionState*,ExecutionState*> klee::Executor::StatePair

Definition at line 90 of file Executor.h.

---

Constructor & Destructor Documentation

Executor::Executor	(	const InterpreterOptions &	opts,
		InterpreterHandler *	ie
	)

Definition at line 300 of file Executor.cpp.

References constructSolverChain(), klee::InterpreterHandler::getOutputFilename(), interpreterHandler, memory, and solver.

Here is the call graph for this function:

Executor::~Executor

(

)

[virtual]

Definition at line 356 of file Executor.cpp.

References externalDispatcher, kmodule, memory, processTree, solver, specialFunctionHandler, and statsTracker.

---

Member Function Documentation

void Executor::addConstraint	(	ExecutionState &	state,
		ref< Expr >	condition
	)			[private]

Add the given (boolean) condition as a constraint on state. This function is a wrapper around the state's addConstraint function which also manages manages propogation of implied values, validity checks, and seed patching.

Definition at line 879 of file Executor.cpp.

References klee::ExecutionState::addConstraint(), klee::ConstantExpr::alloc(), klee::Expr::Bool, doImpliedValueConcretization(), ivcEnabled, klee::klee_warning(), klee::TimingSolver::mustBeFalse(), seedMap, and solver.

Referenced by branch(), fork(), and toConstant().

Here is the call graph for this function:

Here is the caller graph for this function:

MemoryObject * Executor::addExternalObject	(	ExecutionState &	state,
		void *	addr,
		unsigned	size,
		bool	isReadOnly
	)			[private]

Definition at line 402 of file Executor.cpp.

References klee::MemoryManager::allocateFixed(), bindObjectInState(), memory, klee::ObjectState::setReadOnly(), and klee::ObjectState::write8().

Referenced by initializeGlobals().

Here is the call graph for this function:

Here is the caller graph for this function:

void Executor::addTimer	(	Timer *	timer,
		double	rate
	)			[private]

Add a timer to be executed periodically.

Parameters:

	timer	The timer object to run on firings.
	rate	The approximate delay (in seconds) between firings.

Definition at line 118 of file ExecutorTimers.cpp.

References timers.

Referenced by initTimers(), and klee::StatsTracker::StatsTracker().

Here is the caller graph for this function:

void Executor::bindArgument	(	KFunction *	kf,
		unsigned	index,
		ExecutionState &	state,
		ref< Expr >	value
	)			[private]

Definition at line 996 of file Executor.cpp.

References getArgumentCell(), and klee::Cell::value.

Here is the call graph for this function:

void Executor::bindInstructionConstants

(

KInstruction *

KI

)

[private]

bindInstructionConstants - Initialize any necessary per instruction constant values.

Definition at line 2168 of file Executor.cpp.

References klee::Interpreter::create(), klee::Expr::createCoerceToPointerType(), klee::Expr::createPointer(), evalConstant(), klee::KGEPInstruction::indices, klee::KInstruction::inst, kmodule, klee::KGEPInstruction::offset, and klee::KModule::targetData.

Referenced by bindModuleConstants().

Here is the call graph for this function:

Here is the caller graph for this function:

void Executor::bindLocal	(	KInstruction *	target,
		ExecutionState &	state,
		ref< Expr >	value
	)			[private]

Definition at line 991 of file Executor.cpp.

References getDestCell(), and klee::Cell::value.

Referenced by executeAlloc(), executeFree(), executeGetValue(), executeInstruction(), and executeMemoryOperation().

Here is the call graph for this function:

Here is the caller graph for this function:

void Executor::bindModuleConstants

(

)

[private]

bindModuleConstants - Initialize the module constant table.

Definition at line 2204 of file Executor.cpp.

References bindInstructionConstants(), klee::KModule::constants, klee::KModule::constantTable, evalConstant(), klee::KModule::functions, klee::KFunction::instructions, kmodule, klee::KFunction::numInstructions, and klee::Cell::value.

Referenced by run().

Here is the call graph for this function:

Here is the caller graph for this function:

ObjectState * Executor::bindObjectInState	(	ExecutionState &	state,
		const MemoryObject *	mo,
		bool	isLocal
	)			[private]

Definition at line 2620 of file Executor.cpp.

References klee::ExecutionState::addressSpace, klee::AddressSpace::bindObject(), klee::MemoryObject::size, and klee::ExecutionState::stack.

Referenced by addExternalObject(), executeAlloc(), executeMakeSymbolic(), and initializeGlobals().

Here is the call graph for this function:

Here is the caller graph for this function:

void Executor::branch	(	ExecutionState &	state,
		const std::vector< ref< Expr > > &	conditions,
		std::vector< ExecutionState * > &	result
	)			[private]

Create a new state where each input condition has been added as a constraint and return the results. The input state is included as one of the results. Note that the output vector may included NULL pointers for states which were unable to be created.

Definition at line 586 of file Executor.cpp.

References addConstraint(), addedStates, klee::ExecutionState::branch(), klee::PTreeNode::data, klee::stats::forks, klee::stats::forkTime, klee::RNG::getInt32(), klee::TimingSolver::getValue(), processTree, klee::ExecutionState::ptreeNode, seedMap, solver, klee::PTree::split(), terminateState(), and klee::theRNG.

Referenced by executeGetValue(), executeInstruction(), and fork().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::Executor::callExternalFunction	(	ExecutionState &	state,
		KInstruction *	target,
		llvm::Function *	function,
		std::vector< ref< Expr > > &	arguments
	)			[private]

void Executor::doImpliedValueConcretization	(	ExecutionState &	state,
		ref< Expr >	e,
		ref< ConstantExpr >	value
	)			[private]

Definition at line 3199 of file Executor.cpp.

References klee::ExecutionState::addressSpace, klee::ImpliedValue::checkForImpliedValues(), klee::AddressSpace::findObject(), klee::ImpliedValue::getImpliedValues(), klee::AddressSpace::getWriteable(), klee::ReadExpr::index, klee::Array::object, klee::ObjectState::readOnly, klee::UpdateList::root, klee::TimingSolver::solver, solver, klee::ReadExpr::updates, and klee::ObjectState::write().

Referenced by addConstraint().

Here is the call graph for this function:

Here is the caller graph for this function:

const Cell & Executor::eval	(	KInstruction *	ki,
		unsigned	index,
		ExecutionState &	state
	)			const [private]

Definition at line 975 of file Executor.cpp.

References klee::KModule::constantTable, kmodule, klee::StackFrame::locals, klee::KInstruction::operands, and klee::ExecutionState::stack.

Referenced by executeInstruction().

Here is the caller graph for this function:

ref<Expr> klee::Executor::evalConstant

(

llvm::Constant *

c

)

Referenced by bindInstructionConstants(), bindModuleConstants(), evalConstantExpr(), executeInstruction(), and initializeGlobals().

Here is the caller graph for this function:

ref< Expr > klee::Executor::evalConstantExpr

(

llvm::ConstantExpr *

ce

)

[private]

Definition at line 37 of file ExecutorUtil.cpp.

References klee::ConstantExpr::alloc(), klee::Interpreter::create(), klee::ExtractExpr::createByteOff(), klee::Expr::createCoerceToPointerType(), klee::Expr::createPointer(), evalConstant(), klee::Expr::getWidthForLLVMType(), kMachinePointerType, kmodule, and klee::KModule::targetData.

Here is the call graph for this function:

void Executor::executeAlloc	(	ExecutionState &	state,
		ref< Expr >	size,
		bool	isLocal,
		KInstruction *	target,
		bool	zeroMemory = false,
		const ObjectState *	reallocFrom = 0
	)			[private]

Allocate and bind a new object in a particular state. NOTE: This function may fork.

Parameters:

	isLocal	Flag to indicate if the object should be automatically deallocated on function return (this also makes it illegal to free directly).
	target	Value at which to bind the base address of the new object.
	reallocFrom	If non-zero and the allocation succeeds, initialize the new object from the given one and unbind it when done (realloc semantics). The initialized bytes will be the minimum of the size of the old and new objects, with remaining bytes initialized as specified by zeroMemory.

Definition at line 2635 of file Executor.cpp.

References klee::ExecutionState::addressSpace, klee::ConstantExpr::alloc(), klee::MemoryManager::allocate(), bindLocal(), bindObjectInState(), fork(), klee::MemoryObject::getBaseExpr(), klee::ObjectState::getObject(), klee::TimingSolver::getValue(), klee::ObjectState::initializeToRandom(), klee::ObjectState::initializeToZero(), klee::Expr::Int32, klee::klee_message(), kMachinePointerType, klee::TimingSolver::mayBeTrue(), memory, klee::TimingSolver::mustBeTrue(), klee::ExecutionState::prevPC, klee::ExprPPrinter::printOne(), klee::ObjectState::read8(), klee::ObjectState::size, solver, terminateStateOnError(), toUnique(), klee::AddressSpace::unbindObject(), and klee::ObjectState::write().

Referenced by executeInstruction().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::Executor::executeCall	(	ExecutionState &	state,
		KInstruction *	ki,
		llvm::Function *	f,
		std::vector< ref< Expr > > &	arguments
	)			[private]

Referenced by executeInstruction().

Here is the caller graph for this function:

void Executor::executeFree	(	ExecutionState &	state,
		ref< Expr >	address,
		KInstruction *	target = 0
	)			[private]

Free the given address with checking for errors. If target is given it will be bound to 0 in the resulting states (this is a convenience for realloc). Note that this function can cause the state to fork and that state cannot be safely accessed afterwards.

Definition at line 2745 of file Executor.cpp.

References bindLocal(), klee::Expr::createIsZero(), klee::Expr::createPointer(), fork(), getAddressInfo(), klee::MemoryObject::isGlobal, klee::MemoryObject::isLocal, resolveExact(), and terminateStateOnError().

Referenced by executeInstruction().

Here is the call graph for this function:

Here is the caller graph for this function:

void Executor::executeGetValue	(	ExecutionState &	state,
		ref< Expr >	e,
		KInstruction *	target
	)			[private]

Bind a constant value for e to the given target. NOTE: This function may fork state if the state has multiple seeds.

Definition at line 1051 of file Executor.cpp.

References bindLocal(), branch(), klee::ExecutionState::constraints, klee::TimingSolver::getValue(), seedMap, klee::ConstraintManager::simplifyExpr(), and solver.

Here is the call graph for this function:

void Executor::executeInstruction	(	ExecutionState &	state,
		KInstruction *	ki
	)			[private]

Definition at line 1269 of file Executor.cpp.

References klee::floats::add(), klee::ExecutionTraceManager::addEvent(), klee::ConstantExpr::alloc(), bindLocal(), klee::Expr::Bool, branch(), klee::Interpreter::create(), klee::ExtractExpr::createByteOff(), klee::Expr::createCoerceToPointerType(), klee::Expr::createNot(), klee::Expr::createPointer(), klee::floats::div(), klee::ints::eq(), eval(), evalConstant(), executeAlloc(), executeCall(), executeFree(), executeMemoryOperation(), klee::ExecutionState::exeTraceMgr, klee::floats::ext(), fork(), FP_CONSTANT_BINOP, klee::StatsTracker::framePopped(), klee::floats::ge(), getCalledFunction(), klee::TimingSolver::getValue(), klee::Expr::getWidthForLLVMType(), klee::floats::gt(), klee::ExecutionState::incomingBBIndex, klee::KGEPInstruction::indices, klee::KInstruction::inst, klee::floats::isNaN(), klee::klee_warning_once(), kmodule, klee::floats::le(), legalFunctions, klee::floats::lt(), klee::StatsTracker::markBranchVisited(), klee::TimingSolver::mayBeTrue(), klee::floats::mod(), klee::floats::mul(), klee::ints::ne(), klee::KGEPInstruction::offset, klee::ExecutionState::pc, klee::ExecutionState::popFrame(), klee::floats::SignedIntToFP(), solver, klee::ExecutionState::stack, statsTracker, klee::floats::sub(), klee::KModule::targetData, terminateStateOnError(), terminateStateOnExecError(), terminateStateOnExit(), toConstant(), klee::floats::toSignedInt(), toUnique(), klee::floats::toUnsignedInt(), transferToBasicBlock(), klee::ints::trunc(), klee::floats::UnsignedIntToFP(), klee::Cell::value, and WriteTraces.

Referenced by run().

Here is the call graph for this function:

Here is the caller graph for this function:

void Executor::executeMakeSymbolic	(	ExecutionState &	state,
		const MemoryObject *	mo
	)			[private]

Definition at line 2936 of file Executor.cpp.

References klee::ExecutionState::addSymbolic(), klee::MemoryObject::array, klee::SeedInfo::assignment, klee::Assignment::bindings, bindObjectInState(), KTestObject::bytes, klee::SeedInfo::getNextInput(), klee::ObjectState::makeSymbolic(), KTestObject::name, klee::MemoryObject::name, KTestObject::numBytes, KTest::numObjects, KTest::objects, replayOut, replayPosition, seedMap, klee::MemoryObject::size, terminateStateOnError(), and klee::ObjectState::write8().

Here is the call graph for this function:

void Executor::executeMemoryOperation	(	ExecutionState &	state,
		bool	isWrite,
		ref< Expr >	address,
		ref< Expr >	value,
		KInstruction *	target
	)			[private]

Definition at line 2810 of file Executor.cpp.

References klee::ExecutionState::addressSpace, bindLocal(), klee::ExecutionState::constraints, fork(), getAddressInfo(), klee::MemoryObject::getBoundsCheckOffset(), klee::MemoryObject::getBoundsCheckPointer(), klee::Expr::getMinBytesForWidth(), klee::MemoryObject::getOffsetExpr(), klee::Expr::getWidthForLLVMType(), klee::AddressSpace::getWriteable(), klee::KInstruction::inst, klee::Interpreter::interpreterOpts, klee::Interpreter::Interpreter::InterpreterOptions::MakeConcreteSymbolic, klee::TimingSolver::mustBeTrue(), klee::ExecutionState::pc, klee::ExecutionState::prevPC, klee::ObjectState::read(), klee::ObjectState::readOnly, replaceReadWithSymbolic(), klee::AddressSpace::resolve(), klee::AddressSpace::resolveOne(), klee::TimingSolver::setTimeout(), klee::ConstraintManager::simplifyExpr(), klee::MemoryObject::size, solver, stpTimeout, terminateStateEarly(), terminateStateOnError(), toConstant(), and klee::ObjectState::write().

Referenced by executeInstruction().

Here is the call graph for this function:

Here is the caller graph for this function:

Executor::StatePair Executor::fork	(	ExecutionState &	current,
		ref< Expr >	condition,
		bool	isInternal
	)			[private]

Definition at line 660 of file Executor.cpp.

References addConstraint(), addedStates, atMemoryLimit, klee::ExecutionState::branch(), branch(), klee::ExecutionState::coveredLines, klee::ExecutionState::coveredNew, klee::Expr::createNot(), klee::PTreeNode::data, klee::StatsTracker::elapsed(), klee::TimingSolver::evaluate(), klee::Solver::False, klee::ExecutionState::forkDisabled, klee::stats::forks, klee::stats::forkTime, klee::RNG::getBool(), klee::StatisticManager::getIndex(), klee::StatisticManager::getIndexedValue(), klee::TimingSolver::getValue(), klee::StatisticRecord::getValue(), inhibitForking, klee::TreeStreamWriter::open(), klee::ExecutionState::pathOS, pathWriter, klee::ExecutionState::pc, klee::ExecutionState::prevPC, processTree, klee::ExecutionState::ptreeNode, replayOut, replayPath, replayPosition, seedMap, klee::TimingSolver::setTimeout(), solver, klee::stats::solverTime, klee::PTree::split(), klee::ExecutionState::stack, klee::CallPathNode::statistics, statsTracker, stpTimeout, klee::ExecutionState::symPathOS, symPathWriter, terminateStateEarly(), klee::theRNG, klee::theStatisticManager, klee::Solver::True, and klee::Solver::Unknown.

Referenced by executeAlloc(), executeFree(), executeInstruction(), executeMemoryOperation(), and resolveExact().

Here is the call graph for this function:

Here is the caller graph for this function:

std::string Executor::getAddressInfo	(	ExecutionState &	state,
		ref< Expr >	address
	)			const [private]

Get textual information regarding a memory address.

Definition at line 2361 of file Executor.cpp.

References klee::MemoryObject::address, klee::ExecutionState::addressSpace, klee::ImmutableMap< K, D, CMP >::begin(), klee::ImmutableMap< K, D, CMP >::end(), klee::TimingSolver::getRange(), klee::TimingSolver::getValue(), klee::AddressSpace::objects, klee::MemoryObject::size, solver, and klee::ImmutableMap< K, D, CMP >::upper_bound().

Referenced by executeFree(), executeMemoryOperation(), and resolveExact().

Here is the call graph for this function:

Here is the caller graph for this function:

Cell& klee::Executor::getArgumentCell	(	ExecutionState &	state,
		KFunction *	kf,
		unsigned	index
	)			[inline, private]

Definition at line 290 of file Executor.h.

References klee::KFunction::getArgRegister(), and klee::ExecutionState::stack.

Referenced by bindArgument().

Here is the call graph for this function:

Here is the caller graph for this function:

llvm::Function* klee::Executor::getCalledFunction	(	llvm::CallSite &	cs,
		ExecutionState &	state
	)			[private]

Referenced by executeInstruction().

Here is the caller graph for this function:

void Executor::getConstraintLog	(	const ExecutionState &	state,
		std::string &	res,
		bool	asCVC = false
	)			[virtual]

Implements klee::Interpreter.

Definition at line 3129 of file Executor.cpp.

References klee::ConstantExpr::alloc(), klee::Expr::Bool, klee::ExecutionState::constraints, klee::STPSolver::getConstraintLog(), klee::ExprPPrinter::printConstraints(), solver, and klee::TimingSolver::stpSolver.

Here is the call graph for this function:

void Executor::getCoveredLines	(	const ExecutionState &	state,
		std::map< const std::string *, std::set< unsigned > > &	res
	)			[virtual]

Implements klee::Interpreter.

Definition at line 3194 of file Executor.cpp.

References klee::ExecutionState::coveredLines.

Cell& klee::Executor::getDestCell	(	ExecutionState &	state,
		KInstruction *	target
	)			[inline, private]

Definition at line 296 of file Executor.h.

References klee::KInstruction::dest, and klee::ExecutionState::stack.

Referenced by bindLocal().

Here is the caller graph for this function:

const InterpreterHandler& klee::Executor::getHandler

(

)

[inline]

Definition at line 382 of file Executor.h.

References interpreterHandler.

Referenced by klee::constructUserSearcher().

Here is the caller graph for this function:

unsigned Executor::getPathStreamID

(

const ExecutionState &

state

)

[virtual]

Implements klee::Interpreter.

Definition at line 3119 of file Executor.cpp.

References klee::TreeOStream::getID(), klee::ExecutionState::pathOS, and pathWriter.

Here is the call graph for this function:

unsigned Executor::getSymbolicPathStreamID

(

const ExecutionState &

state

)

[virtual]

Implements klee::Interpreter.

Definition at line 3124 of file Executor.cpp.

References klee::TreeOStream::getID(), klee::ExecutionState::symPathOS, and symPathWriter.

Here is the call graph for this function:

bool Executor::getSymbolicSolution	(	const ExecutionState &	state,
		std::vector< std::pair< std::string, std::vector< unsigned char > > > &	res
	)			[virtual]

Implements klee::Interpreter.

Definition at line 3144 of file Executor.cpp.

References klee::ExecutionState::addConstraint(), klee::ConstantExpr::alloc(), klee::Expr::Bool, klee::MemoryObject::cexPreferences, klee::ExecutionState::constraints, klee::Expr::createNot(), klee::TimingSolver::getInitialValues(), klee::klee_warning(), klee::TimingSolver::mustBeTrue(), klee::ExprPPrinter::printQuery(), klee::TimingSolver::setTimeout(), solver, stpTimeout, and klee::ExecutionState::symbolics.

Here is the call graph for this function:

void klee::Executor::handlePointsToObj	(	ExecutionState &	state,
		KInstruction *	target,
		const std::vector< ref< Expr > > &	arguments
	)			[private]

void klee::Executor::initializeGlobalObject	(	ExecutionState &	state,
		ObjectState *	os,
		llvm::Constant *	c,
		unsigned	offset
	)			[private]

Referenced by initializeGlobals().

Here is the caller graph for this function:

void Executor::initializeGlobals

(

ExecutionState &

state

)

[private]

Definition at line 415 of file Executor.cpp.

References __attribute__(), addExternalObject(), klee::ExecutionState::addressSpace, klee::MemoryManager::allocate(), klee::MemoryManager::allocateFixed(), bindObjectInState(), klee::Expr::createPointer(), evalConstant(), externalDispatcher, klee::AddressSpace::findObject(), klee::MemoryObject::getBaseExpr(), klee::AddressSpace::getWriteable(), globalAddresses, globalObjects, initializeGlobalObject(), klee::ObjectState::initializeToRandom(), klee::MemoryObject::isUserSpecified, klee::klee_error(), klee::klee_message(), klee::klee_warning(), kmodule, legalFunctions, memory, klee::KModule::module, klee::ExternalDispatcher::resolveSymbol(), klee::MemoryObject::size, klee::KModule::targetData, and klee::ObjectState::write8().

Here is the call graph for this function:

void Executor::initTimers

(

)

[private]

Definition at line 82 of file ExecutorTimers.cpp.

References addTimer(), MaxTime, and setupHandler().

Referenced by run().

Here is the call graph for this function:

Here is the caller graph for this function:

void Executor::printFileLine	(	ExecutionState &	state,
		KInstruction *	ki
	)			[private]

Definition at line 1239 of file Executor.cpp.

References klee::InstructionInfo::file, klee::KInstruction::info, and klee::InstructionInfo::line.

Referenced by stepInstruction().

Here is the caller graph for this function:

void Executor::processTimers	(	ExecutionState *	current,
		double	maxInstTime
	)			[private]

Definition at line 122 of file ExecutorTimers.cpp.

References klee::StackFrame::callPathNode, klee::computeMinDistToUncovered(), klee::PTree::dump(), klee::StatisticManager::getIndexedValue(), klee::StatisticRecord::getValue(), klee::util::getWallTime(), klee::Statistic::id, klee::stats::instructions, interpreterHandler, klee::klee_warning(), klee::StackFrame::minDistToUncoveredOnReturn, klee::Executor::Executor::TimerInfo::nextFireTime, klee::InterpreterHandler::openOutputFile(), processTree, klee::Executor::Executor::TimerInfo::rate, removedStates, klee::Executor::Executor::Timer::run(), setupHandler(), klee::ExecutionState::stack, states, klee::CallPathNode::statistics, terminateStateEarly(), klee::theStatisticManager, klee::Executor::Executor::TimerInfo::timer, and timers.

Referenced by run().

Here is the call graph for this function:

Here is the caller graph for this function:

ref< Expr > Executor::replaceReadWithSymbolic	(	ExecutionState &	state,
		ref< Expr >	e
	)			[private]

Definition at line 2593 of file Executor.cpp.

References klee::ExecutionState::addConstraint(), klee::MemoryManager::allocate(), klee::MemoryObject::array, klee::Interpreter::create(), klee::Expr::createTempRead(), klee::ints::eq(), klee::Expr::getMinBytesForWidth(), klee::Interpreter::interpreterOpts, klee::Interpreter::Interpreter::InterpreterOptions::MakeConcreteSymbolic, memory, klee::ExecutionState::prevPC, replayOut, and replayPath.

Referenced by executeMemoryOperation().

Here is the call graph for this function:

Here is the caller graph for this function:

void Executor::resolveExact	(	ExecutionState &	state,
		ref< Expr >	p,
		ExactResolutionList &	results,
		const std::string &	name
	)			[private]

Definition at line 2779 of file Executor.cpp.

References klee::ExecutionState::addressSpace, klee::Interpreter::create(), fork(), getAddressInfo(), klee::AddressSpace::resolve(), solver, and terminateStateOnError().

Referenced by executeFree().

Here is the call graph for this function:

Here is the caller graph for this function:

void Executor::run

(

ExecutionState &

initialState

)

[private]

Definition at line 2219 of file Executor.cpp.

References atMemoryLimit, bindModuleConstants(), klee::constructUserSearcher(), executeInstruction(), klee::util::getWallTime(), haltExecution, initTimers(), klee::stats::instructions, klee::klee_message(), klee::klee_warning(), klee::ExecutionState::pc, processTimers(), searcher, seedMap, klee::Searcher::selectState(), states, stepInstruction(), terminateStateEarly(), klee::Searcher::update(), updateStates(), and usingSeeds.

Here is the call graph for this function:

virtual void klee::Executor::runFunctionAsMain	(	llvm::Function *	f,
		int	argc,
		char **	argv,
		char **	envp
	)			[virtual]

Implements klee::Interpreter.

virtual void klee::Executor::setHaltExecution

(

bool

value

)

[inline, virtual]

Implements klee::Interpreter.

Definition at line 422 of file Executor.h.

References haltExecution.

Referenced by HaltTimer::run().

Here is the caller graph for this function:

virtual void klee::Executor::setInhibitForking

(

bool

value

)

[inline, virtual]

Implements klee::Interpreter.

Definition at line 426 of file Executor.h.

References inhibitForking.

const Module * Executor::setModule	(	llvm::Module *	module,
		const ModuleOptions &	opts
	)			[virtual]

Register the module to be executed.

Returns:

The final module after it has been optimized, checks inserted, and modified for interpretation.

Implements klee::Interpreter.

Definition at line 334 of file Executor.cpp.

References klee::SpecialFunctionHandler::bind(), klee::InterpreterHandler::getOutputFilename(), interpreterHandler, kmodule, klee::KModule::prepare(), klee::SpecialFunctionHandler::prepare(), SpecialFunctionHandler, specialFunctionHandler, StatsTracker, statsTracker, klee::userSearcherRequiresMD2U(), and klee::StatsTracker::useStatistics().

Here is the call graph for this function:

virtual void klee::Executor::setPathWriter

(

TreeStreamWriter *

tsw

)

[inline, virtual]

Implements klee::Interpreter.

Definition at line 389 of file Executor.h.

References pathWriter.

virtual void klee::Executor::setReplayOut

(

const struct KTest *

out

)

[inline, virtual]

Implements klee::Interpreter.

Definition at line 396 of file Executor.h.

References replayOut, replayPath, and replayPosition.

virtual void klee::Executor::setReplayPath

(

const std::vector< bool > *

path

)

[inline, virtual]

Implements klee::Interpreter.

Definition at line 402 of file Executor.h.

References replayOut, replayPath, and replayPosition.

virtual void klee::Executor::setSymbolicPathWriter

(

TreeStreamWriter *

tsw

)

[inline, virtual]

Implements klee::Interpreter.

Definition at line 392 of file Executor.h.

References symPathWriter.

void Executor::stepInstruction

(

ExecutionState &

state

)

[private]

Definition at line 1094 of file Executor.cpp.

References haltExecution, klee::stats::instructions, klee::ExecutionState::pc, klee::ExecutionState::prevPC, printFileLine(), statsTracker, and klee::StatsTracker::stepInstruction().

Referenced by run().

Here is the call graph for this function:

Here is the caller graph for this function:

void Executor::terminateState

(

ExecutionState &

state

)

[private]

Definition at line 2404 of file Executor.cpp.

References addedStates, klee::InterpreterHandler::incPathsExplored(), interpreterHandler, klee::klee_warning_once(), KTest::numObjects, klee::ExecutionState::pc, klee::ExecutionState::prevPC, processTree, klee::ExecutionState::ptreeNode, klee::PTree::remove(), removedStates, replayOut, replayPosition, and seedMap.

Referenced by branch(), klee::MergingSearcher::selectState(), klee::BumpMergingSearcher::selectState(), terminateStateEarly(), terminateStateOnError(), and terminateStateOnExit().

Here is the call graph for this function:

Here is the caller graph for this function:

void Executor::terminateStateEarly	(	ExecutionState &	state,
		std::string	message
	)			[private]

Definition at line 2429 of file Executor.cpp.

References klee::ExecutionState::coveredNew, interpreterHandler, klee::InterpreterHandler::processTestCase(), seedMap, and terminateState().

Referenced by executeMemoryOperation(), fork(), processTimers(), and run().

Here is the call graph for this function:

Here is the caller graph for this function:

void Executor::terminateStateOnError	(	ExecutionState &	state,
		const std::string &	message,
		const std::string &	suffix,
		const std::string &	longMessage = ""
	)			[private]

Definition at line 2443 of file Executor.cpp.

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

Referenced by executeAlloc(), executeFree(), executeInstruction(), executeMakeSymbolic(), executeMemoryOperation(), resolveExact(), and terminateStateOnExecError().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::Executor::terminateStateOnExecError	(	ExecutionState &	state,
		const std::string &	message,
		const std::string &	info = ""
	)			[inline, private]

Definition at line 347 of file Executor.h.

References terminateStateOnError().

Referenced by executeInstruction().

Here is the call graph for this function:

Here is the caller graph for this function:

void Executor::terminateStateOnExit

(

ExecutionState &

state

)

[private]

Definition at line 2436 of file Executor.cpp.

References klee::ExecutionState::coveredNew, interpreterHandler, klee::InterpreterHandler::processTestCase(), seedMap, and terminateState().

Referenced by executeInstruction().

Here is the call graph for this function:

Here is the caller graph for this function:

ref< klee::ConstantExpr > Executor::toConstant	(	ExecutionState &	state,
		ref< Expr >	e,
		const char *	purpose
	)			[private]

Return a constant value for the given expression, forcing it to be constant in the given state by adding a constraint if necessary. Note that this function breaks completeness and should generally be avoided.

Parameters:

purpose

An identify string to printed in case of concretization.

Definition at line 1024 of file Executor.cpp.

References addConstraint(), klee::ExecutionState::constraints, klee::TimingSolver::getValue(), klee::klee_warning(), klee::klee_warning_once(), klee::ExecutionState::pc, klee::ConstraintManager::simplifyExpr(), and solver.

Referenced by executeInstruction(), and executeMemoryOperation().

Here is the call graph for this function:

Here is the caller graph for this function:

ref< Expr > Executor::toUnique	(	const ExecutionState &	state,
		ref< Expr > &	e
	)			[private]

Return a unique constant value for the given expression in the given state, if it has one (i.e. it provably only has a single value). Otherwise return the original expression.

Definition at line 1001 of file Executor.cpp.

References klee::TimingSolver::getValue(), klee::TimingSolver::mustBeTrue(), klee::TimingSolver::setTimeout(), solver, and stpTimeout.

Referenced by executeAlloc(), executeInstruction(), and klee::SpecialFunctionHandler::readStringAtAddress().

Here is the call graph for this function:

Here is the caller graph for this function:

void klee::Executor::transferToBasicBlock	(	llvm::BasicBlock *	dst,
		llvm::BasicBlock *	src,
		ExecutionState &	state
	)			[private]

Referenced by executeInstruction().

Here is the caller graph for this function:

void Executor::updateStates

(

ExecutionState *

current

)

[private]

Definition at line 2143 of file Executor.cpp.

References addedStates, processTree, klee::ExecutionState::ptreeNode, klee::PTree::remove(), removedStates, searcher, seedMap, states, and klee::Searcher::update().

Referenced by run().

Here is the call graph for this function:

Here is the caller graph for this function:

virtual void klee::Executor::useSeeds

(

const std::vector< struct KTest * > *

seeds

)

[inline, virtual]

Implements klee::Interpreter.

Definition at line 411 of file Executor.h.

References usingSeeds.

---

Friends And Related Function Documentation

friend class BumpMergingSearcher [friend]

Definition at line 72 of file Executor.h.

friend class MergingSearcher [friend]

Definition at line 73 of file Executor.h.

friend class OwningSearcher [friend]

Definition at line 75 of file Executor.h.

friend class RandomPathSearcher [friend]

Definition at line 74 of file Executor.h.

friend class SpecialFunctionHandler [friend]

Definition at line 77 of file Executor.h.

Referenced by setModule().

friend class StatsTracker [friend]

Definition at line 78 of file Executor.h.

Referenced by setModule().

friend class WeightedRandomSearcher [friend]

Definition at line 76 of file Executor.h.

---

Member Data Documentation

std::set<ExecutionState*> klee::Executor::addedStates [private]

Used to track states that have been added during the current instructions step.

Invariant:

addedStates is a subset of states.

addedStates and removedStates are disjoint.

Definition at line 113 of file Executor.h.

Referenced by branch(), fork(), terminateState(), and updateStates().

bool klee::Executor::atMemoryLimit [private]

Disables forking, instead a random path is chosen. Enabled as needed to control memory usage.

See also:

fork()

Definition at line 155 of file Executor.h.

Referenced by fork(), and run().

ExternalDispatcher* klee::Executor::externalDispatcher [private]

Definition at line 99 of file Executor.h.

Referenced by initializeGlobals(), and ~Executor().

std::map<const llvm::GlobalValue*, ref<Expr> > klee::Executor::globalAddresses [private]

Map of globals to their bound address. This also includes globals that have no representative object (i.e. functions).

Definition at line 134 of file Executor.h.

Referenced by initializeGlobals().

std::map<const llvm::GlobalValue*, MemoryObject*> klee::Executor::globalObjects [private]

Map of globals to their representative memory object.

Definition at line 130 of file Executor.h.

Referenced by initializeGlobals().

bool klee::Executor::haltExecution [private]

Signals the executor to halt execution at the next instruction step.

Definition at line 162 of file Executor.h.

Referenced by run(), setHaltExecution(), and stepInstruction().

bool klee::Executor::inhibitForking [private]

Disables forking, set by client.

See also:

setInhibitForking()

Definition at line 158 of file Executor.h.

Referenced by fork(), and setInhibitForking().

InterpreterHandler* klee::Executor::interpreterHandler [private]

Definition at line 96 of file Executor.h.

Referenced by Executor(), getHandler(), processTimers(), setModule(), klee::StatsTracker::StatsTracker(), terminateState(), terminateStateEarly(), terminateStateOnError(), and terminateStateOnExit().

bool klee::Executor::ivcEnabled [private]

Whether implied-value concretization is enabled. Currently false, it is buggy (it needs to validate its writes).

Definition at line 166 of file Executor.h.

Referenced by addConstraint().

KModule* klee::Executor::kmodule [private]

Definition at line 93 of file Executor.h.

Referenced by klee::SpecialFunctionHandler::bind(), bindInstructionConstants(), bindModuleConstants(), klee::StatsTracker::computeReachableUncovered(), eval(), evalConstantExpr(), executeInstruction(), initializeGlobals(), klee::SpecialFunctionHandler::prepare(), setModule(), klee::StatsTracker::StatsTracker(), klee::StatsTracker::writeIStats(), and ~Executor().

std::set<void*> klee::Executor::legalFunctions [private]

The set of legal function addresses, used to validate function pointers.

Definition at line 138 of file Executor.h.

Referenced by executeInstruction(), and initializeGlobals().

MemoryManager* klee::Executor::memory [private]

Definition at line 101 of file Executor.h.

Referenced by addExternalObject(), executeAlloc(), Executor(), initializeGlobals(), replaceReadWithSymbolic(), and ~Executor().

TreeStreamWriter* klee::Executor::pathWriter [private]

Definition at line 104 of file Executor.h.

Referenced by fork(), getPathStreamID(), and setPathWriter().

PTree* klee::Executor::processTree [private]

Definition at line 107 of file Executor.h.

Referenced by branch(), fork(), processTimers(), klee::RandomPathSearcher::selectState(), terminateState(), updateStates(), and ~Executor().

std::set<ExecutionState*> klee::Executor::removedStates [private]

Used to track states that have been removed during the current instructions step.

Invariant:

removedStates is a subset of states.

addedStates and removedStates are disjoint.

Definition at line 118 of file Executor.h.

Referenced by processTimers(), terminateState(), and updateStates().

struct KTest* klee::Executor::replayOut [read, private]

When non-null the bindings that will be used for calls to klee_make_symbolic in order replay.

Definition at line 142 of file Executor.h.

Referenced by executeMakeSymbolic(), fork(), replaceReadWithSymbolic(), setReplayOut(), setReplayPath(), and terminateState().

const std::vector<bool>* klee::Executor::replayPath [private]

When non-null a list of branch decisions to be used for replay.

Definition at line 144 of file Executor.h.

Referenced by fork(), replaceReadWithSymbolic(), setReplayOut(), and setReplayPath().

unsigned klee::Executor::replayPosition [private]

The index into the current replayOut or replayPath object.

Definition at line 147 of file Executor.h.

Referenced by executeMakeSymbolic(), fork(), setReplayOut(), setReplayPath(), and terminateState().

Searcher* klee::Executor::searcher [private]

Definition at line 97 of file Executor.h.

Referenced by run(), and updateStates().

std::map<ExecutionState*, std::vector<SeedInfo> > klee::Executor::seedMap [private]

When non-empty the Executor is running in "seed" mode. The states in this map will be executed in an arbitrary order (outside the normal search interface) until they terminate. When the states reach a symbolic branch then either direction that satisfies one or more seeds will be added to this map. What happens with other states (that don't satisfy the seeds) depends on as-yet-to-be-determined flags.

Definition at line 127 of file Executor.h.

Referenced by addConstraint(), branch(), executeGetValue(), executeMakeSymbolic(), fork(), run(), terminateState(), terminateStateEarly(), terminateStateOnExit(), and updateStates().

TimingSolver* klee::Executor::solver [private]

Definition at line 100 of file Executor.h.

Referenced by addConstraint(), branch(), doImpliedValueConcretization(), executeAlloc(), executeGetValue(), executeInstruction(), executeMemoryOperation(), Executor(), fork(), getAddressInfo(), getConstraintLog(), getSymbolicSolution(), klee::SpecialFunctionHandler::readStringAtAddress(), resolveExact(), toConstant(), toUnique(), and ~Executor().

SpecialFunctionHandler* klee::Executor::specialFunctionHandler [private]

Definition at line 105 of file Executor.h.

Referenced by setModule(), and ~Executor().

std::set<ExecutionState*> klee::Executor::states [private]

Definition at line 102 of file Executor.h.

Referenced by klee::StatsTracker::computeReachableUncovered(), klee::RandomPathSearcher::empty(), processTimers(), run(), updateStates(), klee::StatsTracker::updateStateStatistics(), and klee::StatsTracker::writeStatsLine().

StatsTracker* klee::Executor::statsTracker [private]

Definition at line 103 of file Executor.h.

Referenced by executeInstruction(), fork(), setModule(), stepInstruction(), and ~Executor().

double klee::Executor::stpTimeout [private]

The maximum time to allow for a single stp query.

Definition at line 169 of file Executor.h.

Referenced by executeMemoryOperation(), fork(), getSymbolicSolution(), and toUnique().

TreeStreamWriter * klee::Executor::symPathWriter [private]

Definition at line 104 of file Executor.h.

Referenced by fork(), getSymbolicPathStreamID(), and setSymbolicPathWriter().

std::vector<TimerInfo*> klee::Executor::timers [private]

Definition at line 106 of file Executor.h.

Referenced by addTimer(), and processTimers().

const std::vector<struct KTest *>* klee::Executor::usingSeeds [private]

When non-null a list of "seed" inputs which will be used to drive execution.

Definition at line 151 of file Executor.h.

Referenced by run(), and useSeeds().

---

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

• lib/Core/Executor.h
• lib/Core/Executor.cpp
• lib/Core/ExecutorTimers.cpp
• lib/Core/ExecutorUtil.cpp