klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee::Executor Class Reference

#include <Executor.h>

Inheritance diagram for klee::Executor:
Collaboration diagram for klee::Executor:

Classes

class  Timer
 
class  TimerInfo
 

Public Types

typedef std::pair
< ExecutionState
*, ExecutionState * > 
StatePair
 
- Public Types inherited from klee::Interpreter
enum  LogType { STP, KQUERY, SMTLIB2 }
 

Public Member Functions

 Executor (const InterpreterOptions &opts, InterpreterHandler *ie)
 
virtual ~Executor ()
 
const InterpreterHandlergetHandler ()
 
ref< klee::ConstantExprevalConstant (const 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, Interpreter::LogType logFormat=Interpreter::STP)
 
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)
 
Expr::Width getWidthForLLVMType (LLVM_TYPE_Q llvm::Type *type) const
 
- Public Member Functions inherited from klee::Interpreter
virtual ~Interpreter ()
 

Private Types

typedef std::vector< std::pair
< std::pair< const
MemoryObject *, const
ObjectState * >
, ExecutionState * > > 
ExactResolutionList
 

Private Member Functions

llvm::Function * getTargetFunction (llvm::Value *calledVal, ExecutionState &state)
 
void executeInstruction (ExecutionState &state, KInstruction *ki)
 
void printFileLine (ExecutionState &state, KInstruction *ki)
 
void run (ExecutionState &initialState)
 
MemoryObjectaddExternalObject (ExecutionState &state, void *addr, unsigned size, bool isReadOnly)
 
void initializeGlobalObject (ExecutionState &state, ObjectState *os, const 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)
 
ObjectStatebindObjectInState (ExecutionState &state, const MemoryObject *mo, bool isLocal, const Array *array=0)
 
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, const std::string &name)
 
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< ExprreplaceReadWithSymbolic (ExecutionState &state, ref< Expr > e)
 
const Celleval (KInstruction *ki, unsigned index, ExecutionState &state) const
 
CellgetArgumentCell (ExecutionState &state, KFunction *kf, unsigned index)
 
CellgetDestCell (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< klee::ConstantExprevalConstantExpr (const llvm::ConstantExpr *ce)
 
ref< ExprtoUnique (const ExecutionState &state, ref< Expr > &e)
 
ref< klee::ConstantExprtoConstant (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. More...
 
const InstructionInfogetLastNonKleeInternalInstruction (const ExecutionState &state, llvm::Instruction **lastInstruction)
 
void terminateState (ExecutionState &state)
 
void terminateStateEarly (ExecutionState &state, const llvm::Twine &message)
 
void terminateStateOnExit (ExecutionState &state)
 
void terminateStateOnError (ExecutionState &state, const llvm::Twine &message, const char *suffix, const llvm::Twine &longMessage="")
 
void terminateStateOnExecError (ExecutionState &state, const llvm::Twine &message, const llvm::Twine &info="")
 
void bindModuleConstants ()
 bindModuleConstants - Initialize the module constant table. More...
 
template<typename TypeIt >
void computeOffsets (KGEPInstruction *kgepi, TypeIt ib, TypeIt ie)
 
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

KModulekmodule
 
InterpreterHandlerinterpreterHandler
 
Searchersearcher
 
ExternalDispatcherexternalDispatcher
 
TimingSolversolver
 
MemoryManagermemory
 
std::set< ExecutionState * > states
 
StatsTrackerstatsTracker
 
TreeStreamWriterpathWriter
 
TreeStreamWritersymPathWriter
 
SpecialFunctionHandlerspecialFunctionHandler
 
std::vector< TimerInfo * > timers
 
PTreeprocessTree
 
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. More...
 
std::map< const
llvm::GlobalValue *, ref
< ConstantExpr > > 
globalAddresses
 
std::set< uint64_t > legalFunctions
 
const struct KTestreplayOut
 
const std::vector< bool > * replayPath
 When non-null a list of branch decisions to be used for replay. More...
 
unsigned replayPosition
 
const std::vector< struct
KTest * > * 
usingSeeds
 
bool atMemoryLimit
 
bool inhibitForking
 Disables forking, set by client. More...
 
bool haltExecution
 
bool ivcEnabled
 
double coreSolverTimeout
 

Friends

class BumpMergingSearcher
 
class MergingSearcher
 
class RandomPathSearcher
 
class OwningSearcher
 
class WeightedRandomSearcher
 
class SpecialFunctionHandler
 
class StatsTracker
 

Additional Inherited Members

- Static Public Member Functions inherited from klee::Interpreter
static Interpretercreate (const InterpreterOptions &_interpreterOpts, InterpreterHandler *ih)
 
- Protected Member Functions inherited from klee::Interpreter
 Interpreter (const InterpreterOptions &_interpreterOpts)
 
- Protected Attributes inherited from klee::Interpreter
const InterpreterOptions interpreterOpts
 

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 79 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 222 of file Executor.h.

Definition at line 98 of file Executor.h.

Constructor & Destructor Documentation

Executor::~Executor ( )
virtual

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 propagation of implied values, validity checks, and seed patching.

Definition at line 956 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 449 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
timerThe timer object to run on firings.
rateThe approximate delay (in seconds) between firings.

Definition at line 107 of file ExecutorTimers.cpp.

Referenced by 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 1074 of file Executor.cpp.

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

Referenced by executeCall(), and runFunctionAsMain().

Here is the call graph for this function:

Here is the caller graph for this function:

void Executor::bindInstructionConstants ( KInstruction KI)
private

bindInstructionConstants - Initialize any necessary per instruction constant values.

Definition at line 2475 of file Executor.cpp.

References computeOffsets(), klee::ev_type_begin(), klee::ev_type_end(), klee::gep_type_begin(), klee::gep_type_end(), klee::KGEPInstruction::indices, klee::KInstruction::inst, klee::iv_type_begin(), and klee::iv_type_end().

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 1069 of file Executor.cpp.

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

Referenced by callExternalFunction(), 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 2489 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,
const Array array = 0 
)
private

Definition at line 2942 of file Executor.cpp.

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

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

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 642 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(), klee::ConstantExpr::isTrue(), 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:

template<typename TypeIt >
void Executor::computeOffsets ( KGEPInstruction kgepi,
TypeIt  ib,
TypeIt  ie 
)
private
void Executor::doImpliedValueConcretization ( ExecutionState state,
ref< Expr e,
ref< ConstantExpr value 
)
private
const Cell & Executor::eval ( KInstruction ki,
unsigned  index,
ExecutionState state 
) const
private

Definition at line 1050 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< klee::ConstantExpr > Executor::evalConstant ( const llvm::Constant *  c)
ref< ConstantExpr > klee::Executor::evalConstantExpr ( const llvm::ConstantExpr *  ce)
private
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
isLocalFlag to indicate if the object should be automatically deallocated on function return (this also makes it illegal to free directly).
targetValue at which to bind the base address of the new object.
reallocFromIf 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 2959 of file Executor.cpp.

References klee::ExecutionState::addressSpace, klee::ConstantExpr::alloc(), klee::MemoryManager::allocate(), bindLocal(), bindObjectInState(), fork(), klee::Context::get(), klee::MemoryObject::getBaseExpr(), klee::ObjectState::getObject(), klee::Context::getPointerWidth(), klee::TimingSolver::getValue(), klee::ConstantExpr::getWidth(), klee::ObjectState::initializeToRandom(), klee::ObjectState::initializeToZero(), klee::KInstruction::inst, klee::klee_message(), klee::ConstantExpr::LShr(), klee::TimingSolver::mayBeTrue(), memory, klee::TimingSolver::mustBeTrue(), klee::ExecutionState::prevPC, klee::ExprPPrinter::printOne(), klee::ObjectState::read8(), klee::ObjectState::size, solver, terminateStateOnError(), toUnique(), klee::ConstantExpr::Ugt(), 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 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 3069 of file Executor.cpp.

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

Here is the call 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 1130 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
Executor::StatePair Executor::fork ( ExecutionState current,
ref< Expr condition,
bool  isInternal 
)
private
std::string Executor::getAddressInfo ( ExecutionState state,
ref< Expr address 
) const
private
Cell& klee::Executor::getArgumentCell ( ExecutionState state,
KFunction kf,
unsigned  index 
)
inlineprivate

Definition at line 301 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:

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

Implements klee::Interpreter.

Definition at line 3528 of file Executor.cpp.

References klee::ExecutionState::coveredLines.

Cell& klee::Executor::getDestCell ( ExecutionState state,
KInstruction target 
)
inlineprivate

Definition at line 307 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 401 of file Executor.h.

References interpreterHandler.

Referenced by klee::constructUserSearcher().

Here is the caller graph for this function:

const InstructionInfo & Executor::getLastNonKleeInternalInstruction ( const ExecutionState state,
llvm::Instruction **  lastInstruction 
)
private
unsigned Executor::getPathStreamID ( const ExecutionState state)
virtual

Implements klee::Interpreter.

Definition at line 3439 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 3444 of file Executor.cpp.

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

Here is the call graph for this function:

Function * Executor::getTargetFunction ( llvm::Value *  calledVal,
ExecutionState state 
)
private

Compute the true target of a function call, resolving LLVM and KLEE aliases and bitcasts.

Definition at line 1368 of file Executor.cpp.

References klee::ExecutionState::getFnAlias(), kmodule, and klee::KModule::module.

Referenced by executeInstruction().

Here is the call graph for this function:

Here is the caller graph for this function:

Expr::Width Executor::getWidthForLLVMType ( LLVM_TYPE_Q llvm::Type *  type) const

Definition at line 3567 of file Executor.cpp.

References kmodule, and klee::KModule::targetData.

Referenced by callExternalFunction(), evalConstant(), executeInstruction(), and executeMemoryOperation().

Here is the caller graph for this function:

void klee::Executor::handlePointsToObj ( ExecutionState state,
KInstruction target,
const std::vector< ref< Expr > > &  arguments 
)
private
void Executor::initializeGlobalObject ( ExecutionState state,
ObjectState os,
const llvm::Constant *  c,
unsigned  offset 
)
private

Definition at line 397 of file Executor.cpp.

References evalConstant(), klee::ConstantExpr::getWidth(), kmodule, klee::KModule::targetData, klee::ObjectState::write(), klee::ObjectState::write8(), and klee::ConstantExpr::ZExt().

Referenced by initializeGlobals().

Here is the call graph for this function:

Here is the caller graph for this function:

void Executor::initTimers ( )
private

Definition at line 88 of file ExecutorTimers.cpp.

References 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 1358 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:

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

Definition at line 3103 of file Executor.cpp.

References klee::ExecutionState::addressSpace, 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:

virtual void klee::Executor::setHaltExecution ( bool  value)
inlinevirtual

Implements klee::Interpreter.

Definition at line 441 of file Executor.h.

References haltExecution.

virtual void klee::Executor::setInhibitForking ( bool  value)
inlinevirtual

Implements klee::Interpreter.

Definition at line 445 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 347 of file Executor.cpp.

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

Here is the call graph for this function:

virtual void klee::Executor::setPathWriter ( TreeStreamWriter tsw)
inlinevirtual

Implements klee::Interpreter.

Definition at line 408 of file Executor.h.

References pathWriter.

virtual void klee::Executor::setReplayOut ( const struct KTest out)
inlinevirtual

Implements klee::Interpreter.

Definition at line 415 of file Executor.h.

References replayOut, replayPath, and replayPosition.

virtual void klee::Executor::setReplayPath ( const std::vector< bool > *  path)
inlinevirtual

Implements klee::Interpreter.

Definition at line 421 of file Executor.h.

References replayOut, replayPath, and replayPosition.

virtual void klee::Executor::setSymbolicPathWriter ( TreeStreamWriter tsw)
inlinevirtual

Implements klee::Interpreter.

Definition at line 411 of file Executor.h.

References symPathWriter.

void Executor::stepInstruction ( ExecutionState state)
private

Definition at line 1173 of file Executor.cpp.

References haltExecution, klee::KInstruction::inst, 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::terminateStateEarly ( ExecutionState state,
const llvm::Twine &  message 
)
private

Definition at line 2720 of file Executor.cpp.

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

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

Here is the call graph for this function:

Here is the caller graph for this function:

void Executor::terminateStateOnError ( ExecutionState state,
const llvm::Twine &  message,
const char *  suffix,
const llvm::Twine &  longMessage = "" 
)
private
void klee::Executor::terminateStateOnExecError ( ExecutionState state,
const llvm::Twine &  message,
const llvm::Twine &  info = "" 
)
inlineprivate

Definition at line 363 of file Executor.h.

References terminateStateOnError().

Referenced by callExternalFunction(), executeCall(), executeInstruction(), and klee::SpecialFunctionHandler::handle().

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 2729 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
purposeAn identify string to printed in case of concretization.

Definition at line 1102 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 1079 of file Executor.cpp.

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

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

Here is the call graph for this function:

Here is the caller graph for this function:

void Executor::transferToBasicBlock ( llvm::BasicBlock *  dst,
llvm::BasicBlock *  src,
ExecutionState state 
)
private
void Executor::updateStates ( ExecutionState current)
private

Definition at line 2417 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)
inlinevirtual

Implements klee::Interpreter.

Definition at line 430 of file Executor.h.

References usingSeeds.

Friends And Related Function Documentation

friend class BumpMergingSearcher
friend

Definition at line 80 of file Executor.h.

friend class MergingSearcher
friend

Definition at line 81 of file Executor.h.

friend class OwningSearcher
friend

Definition at line 83 of file Executor.h.

friend class RandomPathSearcher
friend

Definition at line 82 of file Executor.h.

friend class SpecialFunctionHandler
friend

Definition at line 85 of file Executor.h.

Referenced by setModule().

friend class StatsTracker
friend

Definition at line 86 of file Executor.h.

Referenced by setModule().

friend class WeightedRandomSearcher
friend

Definition at line 84 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 121 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 163 of file Executor.h.

Referenced by fork(), and run().

double klee::Executor::coreSolverTimeout
private

The maximum time to allow for a single core solver query. (e.g. for a single STP query)

Definition at line 178 of file Executor.h.

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

ExternalDispatcher* klee::Executor::externalDispatcher
private

Definition at line 107 of file Executor.h.

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

std::map<const llvm::GlobalValue*, ref<ConstantExpr> > 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 142 of file Executor.h.

Referenced by evalConstant(), initializeGlobals(), and runFunctionAsMain().

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

Map of globals to their representative memory object.

Definition at line 138 of file Executor.h.

Referenced by initializeGlobals(), and runFunctionAsMain().

bool klee::Executor::haltExecution
private

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

Definition at line 170 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 166 of file Executor.h.

Referenced by fork(), and setInhibitForking().

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 174 of file Executor.h.

Referenced by addConstraint().

std::set<uint64_t> klee::Executor::legalFunctions
private

The set of legal function addresses, used to validate function pointers. We use the actual Function* address as the function address.

Definition at line 146 of file Executor.h.

Referenced by executeInstruction(), and initializeGlobals().

MemoryManager* klee::Executor::memory
private
TreeStreamWriter* klee::Executor::pathWriter
private

Definition at line 112 of file Executor.h.

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

PTree* klee::Executor::processTree
private
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 126 of file Executor.h.

Referenced by terminateState(), and updateStates().

const struct KTest* klee::Executor::replayOut
private

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

Definition at line 150 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 152 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 155 of file Executor.h.

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

Searcher* klee::Executor::searcher
private

Definition at line 105 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 135 of file Executor.h.

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

SpecialFunctionHandler* klee::Executor::specialFunctionHandler
private

Definition at line 113 of file Executor.h.

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

StatsTracker* klee::Executor::statsTracker
private
TreeStreamWriter * klee::Executor::symPathWriter
private
std::vector<TimerInfo*> klee::Executor::timers
private

Definition at line 114 of file Executor.h.

Referenced by ~Executor().

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 159 of file Executor.h.

Referenced by run(), and useSeeds().


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