klee
|
#include <Executor.h>
Public Types | |
typedef std::pair< ExecutionState *, ExecutionState * > | StatePair |
![]() | |
enum | LogType { STP , KQUERY , SMTLIB2 } |
Public Member Functions | |
Executor (llvm::LLVMContext &ctx, const InterpreterOptions &opts, InterpreterHandler *ie) | |
virtual | ~Executor () |
const InterpreterHandler & | getHandler () |
void | setPathWriter (TreeStreamWriter *tsw) override |
void | setSymbolicPathWriter (TreeStreamWriter *tsw) override |
void | setReplayKTest (const struct KTest *out) override |
void | setReplayPath (const std::vector< bool > *path) override |
llvm::Module * | setModule (std::vector< std::unique_ptr< llvm::Module > > &modules, const ModuleOptions &opts) override |
void | useSeeds (const std::vector< struct KTest * > *seeds) override |
void | runFunctionAsMain (llvm::Function *f, int argc, char **argv, char **envp) override |
void | setHaltExecution (bool value) override |
void | setInhibitForking (bool value) override |
void | prepareForEarlyExit () override |
unsigned | getPathStreamID (const ExecutionState &state) override |
unsigned | getSymbolicPathStreamID (const ExecutionState &state) override |
void | getConstraintLog (const ExecutionState &state, std::string &res, Interpreter::LogType logFormat=Interpreter::STP) override |
bool | getSymbolicSolution (const ExecutionState &state, std::vector< std::pair< std::string, std::vector< unsigned char > > > &res) override |
void | getCoveredLines (const ExecutionState &state, std::map< const std::string *, std::set< unsigned > > &res) override |
Expr::Width | getWidthForLLVMType (llvm::Type *type) const |
size_t | getAllocationAlignment (const llvm::Value *allocSite) const |
int * | getErrnoLocation (const ExecutionState &state) const |
Returns the errno location in memory of the state. More... | |
MergingSearcher * | getMergingSearcher () const |
void | setMergingSearcher (MergingSearcher *ms) |
![]() | |
virtual | ~Interpreter () |
virtual llvm::Module * | setModule (std::vector< std::unique_ptr< llvm::Module > > &modules, const ModuleOptions &opts)=0 |
virtual void | setPathWriter (TreeStreamWriter *tsw)=0 |
virtual void | setSymbolicPathWriter (TreeStreamWriter *tsw)=0 |
virtual void | setReplayKTest (const struct KTest *out)=0 |
virtual void | setReplayPath (const std::vector< bool > *path)=0 |
virtual void | useSeeds (const std::vector< struct KTest * > *seeds)=0 |
virtual void | runFunctionAsMain (llvm::Function *f, int argc, char **argv, char **envp)=0 |
virtual void | setHaltExecution (bool value)=0 |
virtual void | setInhibitForking (bool value)=0 |
virtual void | prepareForEarlyExit ()=0 |
virtual unsigned | getPathStreamID (const ExecutionState &state)=0 |
virtual unsigned | getSymbolicPathStreamID (const ExecutionState &state)=0 |
virtual void | getConstraintLog (const ExecutionState &state, std::string &res, LogType logFormat=STP)=0 |
virtual bool | getSymbolicSolution (const ExecutionState &state, std::vector< std::pair< std::string, std::vector< unsigned char > > > &res)=0 |
virtual void | getCoveredLines (const ExecutionState &state, std::map< const std::string *, std::set< unsigned > > &res)=0 |
Public Attributes | |
RNG | theRNG |
The random number generator. More... | |
Private Types | |
typedef std::vector< std::pair< std::pair< const MemoryObject *, const ObjectState * >, ExecutionState * > > | ExactResolutionList |
Private Member Functions | |
ref< ConstantExpr > | getEhTypeidFor (ref< Expr > type_info) |
Return the typeid corresponding to a certain type_info More... | |
llvm::Function * | getTargetFunction (llvm::Value *calledVal, ExecutionState &state) |
void | executeInstruction (ExecutionState &state, KInstruction *ki) |
void | run (ExecutionState &initialState) |
MemoryObject * | addExternalObject (ExecutionState &state, void *addr, unsigned size, bool isReadOnly) |
void | initializeGlobalAlias (const llvm::Constant *c) |
void | initializeGlobalObject (ExecutionState &state, ObjectState *os, const llvm::Constant *c, unsigned offset) |
void | initializeGlobals (ExecutionState &state) |
void | allocateGlobalObjects (ExecutionState &state) |
void | initializeGlobalAliases () |
void | initializeGlobalObjects (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, 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, size_t allocationAlignment=0) |
void | executeFree (ExecutionState &state, ref< Expr > address, KInstruction *target=0) |
MemoryObject * | serializeLandingpad (ExecutionState &state, const llvm::LandingPadInst &lpi, bool &stateTerminated) |
void | unwindToNextLandingpad (ExecutionState &state) |
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, BranchType reason) |
StatePair | fork (ExecutionState ¤t, ref< Expr > condition, bool isInternal, BranchType reason) |
ref< Expr > | maxStaticPctChecks (ExecutionState ¤t, ref< Expr > condition) |
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< klee::ConstantExpr > | evalConstantExpr (const llvm::ConstantExpr *c, const KInstruction *ki=NULL) |
ref< klee::ConstantExpr > | evalConstant (const llvm::Constant *c, const KInstruction *ki=NULL) |
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. More... | |
const InstructionInfo & | getLastNonKleeInternalInstruction (const ExecutionState &state, llvm::Instruction **lastInstruction) |
void | terminateState (ExecutionState &state) |
Remove state from queue and delete state. More... | |
void | terminateStateOnExit (ExecutionState &state) |
void | terminateStateEarly (ExecutionState &state, const llvm::Twine &message, StateTerminationType terminationType) |
void | terminateStateOnError (ExecutionState &state, const llvm::Twine &message, StateTerminationType terminationType, const llvm::Twine &longMessage="", const char *suffix=nullptr) |
void | terminateStateOnExecError (ExecutionState &state, const llvm::Twine &message, const llvm::Twine &info="") |
void | terminateStateOnSolverError (ExecutionState &state, const llvm::Twine &message) |
void | terminateStateOnUserError (ExecutionState &state, const llvm::Twine &message) |
void | bindModuleConstants () |
bindModuleConstants - Initialize the module constant table. More... | |
template<typename SqType , typename TypeIt > | |
void | computeOffsetsSeqTy (KGEPInstruction *kgepi, ref< ConstantExpr > &constantOffset, uint64_t index, const TypeIt it) |
template<typename TypeIt > | |
void | computeOffsets (KGEPInstruction *kgepi, TypeIt ib, TypeIt ie) |
void | bindInstructionConstants (KInstruction *KI) |
void | doImpliedValueConcretization (ExecutionState &state, ref< Expr > e, ref< ConstantExpr > value) |
bool | checkMemoryUsage () |
bool | branchingPermitted (const ExecutionState &state) const |
check if branching/forking is allowed More... | |
void | printDebugInstructions (ExecutionState &state) |
void | doDumpStates () |
void | dumpStates () |
Only for debug purposes; enable via debugger or klee-control. More... | |
void | dumpPTree () |
Private Attributes | |
std::unique_ptr< KModule > | kmodule |
InterpreterHandler * | interpreterHandler |
Searcher * | searcher |
ExternalDispatcher * | externalDispatcher |
TimingSolver * | solver |
MemoryManager * | memory |
std::set< ExecutionState *, ExecutionStateIDCompare > | states |
StatsTracker * | statsTracker |
TreeStreamWriter * | pathWriter |
TreeStreamWriter * | symPathWriter |
SpecialFunctionHandler * | specialFunctionHandler |
TimerGroup | timers |
std::unique_ptr< PTree > | processTree |
std::vector< ExecutionState * > | addedStates |
std::vector< 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::unordered_map< std::uint64_t, llvm::Function * > | legalFunctions |
const struct KTest * | replayKTest |
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 |
time::Span | coreSolverTimeout |
time::Span | maxInstructionTime |
Maximum time to allow for a single instruction. More... | |
ArrayCache | arrayCache |
Assumes ownership of the created array objects. More... | |
std::unique_ptr< llvm::raw_ostream > | debugInstFile |
File to print executed instructions to. More... | |
std::string | debugBufferString |
llvm::raw_string_ostream | debugLogBuffer |
ExprOptimizer | optimizer |
Optimizes expressions. More... | |
MergingSearcher * | mergingSearcher = nullptr |
std::vector< ref< Expr > > | eh_typeids |
Typeids used during exception handling. More... | |
Friends | |
class | OwningSearcher |
class | WeightedRandomSearcher |
class | SpecialFunctionHandler |
class | StatsTracker |
class | MergeHandler |
klee::Searcher * | klee::constructUserSearcher (Executor &executor) |
Additional Inherited Members | |
![]() | |
static Interpreter * | create (llvm::LLVMContext &ctx, const InterpreterOptions &_interpreterOpts, InterpreterHandler *ih) |
![]() | |
Interpreter (const InterpreterOptions &_interpreterOpts) | |
![]() | |
const InterpreterOptions | interpreterOpts |
Definition at line 92 of file Executor.h.
|
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).
results[out] | A list of ((MemoryObject,ObjectState), state) pairs for each object the given address can point to the beginning of. |
Definition at line 258 of file Executor.h.
typedef std::pair<ExecutionState*,ExecutionState*> klee::Executor::StatePair |
Definition at line 101 of file Executor.h.
Executor::Executor | ( | llvm::LLVMContext & | ctx, |
const InterpreterOptions & | opts, | ||
InterpreterHandler * | ie | ||
) |
Definition at line 436 of file Executor.cpp.
References klee::TimerGroup::add(), klee::ALL_QUERIES_KQUERY_FILE_NAME, klee::ALL_QUERIES_SMT2_FILE_NAME, arrayCache, klee::constructSolverChain(), coreSolverTimeout, klee::CoreSolverToUse, klee::createCoreSolver(), debugInstFile, klee::InterpreterHandler::getOutputFilename(), klee::initializeSearchOptions(), interpreterHandler, klee::klee_error(), klee::klee_message(), klee::klee_open_output_file(), klee::MaxCoreSolverTime, klee::MaxTime, memory, setHaltExecution(), solver, klee::SOLVER_QUERIES_KQUERY_FILE_NAME, klee::SOLVER_QUERIES_SMT2_FILE_NAME, timers, klee::UseForkedCoreSolver, and klee::StatsTracker::useIStats().
|
virtual |
Definition at line 562 of file Executor.cpp.
References externalDispatcher, memory, solver, specialFunctionHandler, and statsTracker.
|
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 1194 of file Executor.cpp.
References klee::ExecutionState::addConstraint(), klee::ConstantExpr::alloc(), klee::Expr::Bool, klee::ExecutionState::constraints, doImpliedValueConcretization(), ivcEnabled, klee::klee_warning(), klee::TimingSolver::mustBeFalse(), klee::ExecutionState::queryMetaData, seedMap, and solver.
Referenced by branch(), fork(), maxStaticPctChecks(), and toConstant().
|
private |
Definition at line 618 of file Executor.cpp.
References klee::MemoryManager::allocateFixed(), bindObjectInState(), memory, klee::ObjectState::setReadOnly(), and klee::ObjectState::write8().
Referenced by allocateGlobalObjects().
|
private |
Definition at line 648 of file Executor.cpp.
References addExternalObject(), klee::MemoryManager::allocate(), klee::Expr::createPointer(), externalDispatcher, getAllocationAlignment(), klee::MemoryObject::getBaseExpr(), getErrnoLocation(), globalAddresses, globalObjects, klee::MemoryObject::isUserSpecified, klee::klee_error(), klee::klee_warning(), kmodule, legalFunctions, memory, and klee::ExternalDispatcher::resolveSymbol().
Referenced by initializeGlobals().
|
private |
Definition at line 1253 of file Executor.cpp.
References getArgumentCell(), and klee::Cell::value.
Referenced by executeCall(), runFunctionAsMain(), and unwindToNextLandingpad().
|
private |
bindInstructionConstants - Initialize any necessary per instruction constant values.
Definition at line 3358 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().
|
private |
Definition at line 1248 of file Executor.cpp.
References getDestCell(), and klee::Cell::value.
Referenced by callExternalFunction(), executeAlloc(), executeCall(), executeFree(), executeGetValue(), executeInstruction(), and executeMemoryOperation().
|
private |
bindModuleConstants - Initialize the module constant table.
Definition at line 3373 of file Executor.cpp.
References bindInstructionConstants(), evalConstant(), klee::KFunction::instructions, kmodule, klee::KFunction::numInstructions, and klee::Cell::value.
Referenced by run().
|
private |
Definition at line 3938 of file Executor.cpp.
References klee::ExecutionState::addressSpace, klee::AddressSpace::bindObject(), and klee::ExecutionState::stack.
Referenced by addExternalObject(), executeAlloc(), executeCall(), executeMakeSymbolic(), initializeGlobalObjects(), runFunctionAsMain(), and serializeLandingpad().
|
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 include NULL pointers for states which were unable to be created.
Definition at line 864 of file Executor.cpp.
References addConstraint(), addedStates, klee::ExecutionState::branch(), branchingPermitted(), klee::ExecutionState::constraints, klee::stats::forks, klee::stats::forkTime, klee::RNG::getInt32(), klee::TimingSolver::getValue(), processTree, klee::ExecutionState::ptreeNode, klee::ExecutionState::queryMetaData, seedMap, solver, terminateStateEarly(), and theRNG.
Referenced by executeGetValue(), executeInstruction(), and fork().
|
private |
check if branching/forking is allowed
Definition at line 843 of file Executor.cpp.
References atMemoryLimit, klee::ExecutionState::forkDisabled, klee::stats::forks, inhibitForking, and klee::klee_warning_once().
Referenced by branch(), and fork().
|
private |
Definition at line 3781 of file Executor.cpp.
References klee::ExecutionState::addressSpace, bindLocal(), klee::ExecutionState::constraints, klee::AddressSpace::copyInConcrete(), klee::AddressSpace::copyInConcretes(), klee::AddressSpace::copyOutConcretes(), klee::ConstantExpr::create(), klee::ExternalDispatcher::executeCall(), externalDispatcher, klee::Expr::Fl80, klee::ConstantExpr::fromMemory(), klee::Context::get(), getErrnoLocation(), klee::ExternalDispatcher::getLastErrno(), klee::Context::getPointerWidth(), klee::KInstruction::getSourceLocation(), klee::TimingSolver::getValue(), getWidthForLLVMType(), klee::ConstantExpr::getZExtValue(), klee::SpecialFunctionHandler::handle(), klee::KInstruction::inst, klee::Expr::Int64, klee::klee_error(), klee::klee_warning(), klee::klee_warning_once(), okExternals(), klee::ExprOptimizer::optimizeExpr(), optimizer, klee::ExecutionState::pc, klee::ExecutionState::queryMetaData, klee::AddressSpace::resolveOne(), klee::ExternalDispatcher::setLastErrno(), solver, specialFunctionHandler, terminateStateOnError(), terminateStateOnExecError(), terminateStateOnUserError(), and toUnique().
Referenced by executeCall().
|
private |
check memory usage and terminate states when over threshold of -max-memory + 100MB
Definition at line 3388 of file Executor.cpp.
References atMemoryLimit, klee::RNG::getInt32(), klee::util::GetTotalMallocUsage(), klee::MemoryManager::getUsedDeterministicSize(), klee::stats::instructions, klee::klee_warning(), memory, states, terminateStateEarly(), and theRNG.
Referenced by run().
|
private |
Definition at line 3334 of file Executor.cpp.
References klee::ConstantExpr::alloc(), klee::Context::get(), kmodule, and klee::KGEPInstruction::offset.
Referenced by bindInstructionConstants().
|
private |
Definition at line 3315 of file Executor.cpp.
References klee::ConstantExpr::alloc(), evalConstant(), klee::Context::get(), klee::KGEPInstruction::indices, kmodule, and klee::ConstantExpr::SExt().
|
private |
Definition at line 3430 of file Executor.cpp.
References klee::InterpreterHandler::incPathsExplored(), interpreterHandler, klee::klee_message(), states, terminateStateEarly(), and updateStates().
Referenced by run().
|
private |
Definition at line 4550 of file Executor.cpp.
References klee::ExecutionState::addressSpace, klee::ImpliedValue::checkForImpliedValues(), klee::AddressSpace::findObject(), klee::ImpliedValue::getImpliedValues(), klee::AddressSpace::getWriteable(), klee::ReadExpr::index, klee::ObjectState::readOnly, solver, klee::TimingSolver::solver, and klee::ObjectState::write().
Referenced by addConstraint().
|
private |
Definition at line 4677 of file Executor.cpp.
References dumpPTree(), klee::stats::instructions, interpreterHandler, klee::InterpreterHandler::openOutputFile(), and processTree.
Referenced by dumpPTree(), and run().
|
private |
Only for debug purposes; enable via debugger or klee-control.
Definition at line 4690 of file Executor.cpp.
References klee::StackFrame::callPathNode, klee::computeMinDistToUncovered(), dumpStates(), klee::StatisticManager::getIndexedValue(), klee::StatisticRecord::getValue(), klee::Statistic::id, klee::stats::instructions, interpreterHandler, klee::StackFrame::minDistToUncoveredOnReturn, klee::InterpreterHandler::openOutputFile(), states, klee::CallPathNode::statistics, and klee::theStatisticManager.
Referenced by dumpStates(), and run().
|
private |
Definition at line 1229 of file Executor.cpp.
References kmodule, klee::StackFrame::locals, klee::KInstruction::operands, and klee::ExecutionState::stack.
Referenced by executeCall(), and executeInstruction().
|
private |
Evaluates an LLVM constant. The optional argument ki is the instruction where this constant was encountered, or NULL if not applicable/unavailable.
Definition at line 35 of file ExecutorUtil.cpp.
References klee::ConstantExpr::alloc(), klee::ConstantExpr::create(), klee::ConcatExpr::createN(), klee::Expr::createPointer(), evalConstant(), evalConstantExpr(), klee::Context::get(), klee::KInstruction::getSourceLocation(), klee::Expr::getWidth(), getWidthForLLVMType(), globalAddresses, klee::KInstruction::inst, klee::KConstant::ki, klee::klee_error(), klee::klee_warning_once(), and kmodule.
Referenced by bindModuleConstants(), computeOffsetsSeqTy(), evalConstant(), evalConstantExpr(), executeInstruction(), initializeGlobalAlias(), and initializeGlobalObject().
|
private |
Evaluates an LLVM constant expression. The optional argument ki is the instruction where this constant was encountered, or NULL if not applicable/unavailable.
Definition at line 138 of file ExecutorUtil.cpp.
References klee::ConstantExpr::alloc(), evalConstant(), klee::gep_type_begin(), klee::gep_type_end(), klee::Context::get(), klee::Context::getPointerWidth(), klee::KInstruction::getSourceLocation(), getWidthForLLVMType(), klee::klee_error(), and kmodule.
Referenced by evalConstant().
|
private |
Allocate and bind a new object in a particular state. NOTE: This function may fork.
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. |
allocationAlignment | If non-zero, the given alignment is used. Otherwise, the alignment is deduced via Executor::getAllocationAlignment |
Definition at line 3955 of file Executor.cpp.
References klee::ExecutionState::addressSpace, klee::ConstantExpr::alloc(), klee::MemoryManager::allocate(), bindLocal(), bindObjectInState(), klee::ExecutionState::constraints, executeAlloc(), fork(), klee::Context::get(), getAllocationAlignment(), klee::MemoryObject::getBaseExpr(), klee::ObjectState::getObject(), klee::Context::getPointerWidth(), klee::TimingSolver::getValue(), klee::ObjectState::initializeToRandom(), klee::ObjectState::initializeToZero(), klee::KInstruction::inst, klee::klee_message(), klee::TimingSolver::mayBeTrue(), memory, klee::TimingSolver::mustBeTrue(), klee::ExprOptimizer::optimizeExpr(), optimizer, klee::ExecutionState::prevPC, klee::ExprPPrinter::printOne(), klee::ExecutionState::queryMetaData, klee::ObjectState::read8(), klee::ObjectState::size, solver, terminateStateOnError(), toUnique(), klee::AddressSpace::unbindObject(), and klee::ObjectState::write().
Referenced by executeAlloc(), and executeInstruction().
|
private |
Definition at line 1657 of file Executor.cpp.
References klee::MemoryObject::address, klee::ExecutionState::addressSpace, klee::ConstantExpr::alloc(), klee::MemoryManager::allocate(), bindArgument(), bindLocal(), bindObjectInState(), callExternalFunction(), klee::ConcatExpr::create(), klee::SelectExpr::create(), klee::ExtractExpr::create(), klee::ConstantExpr::create(), eval(), executeMemoryOperation(), fpWidthToSemantics(), klee::StatsTracker::framePushed(), klee::Context::get(), klee::MemoryObject::getBaseExpr(), getEhTypeidFor(), klee::Expr::getMinBytesForWidth(), klee::Context::getPointerWidth(), klee::Expr::getWidth(), klee::KInstruction::inst, klee::KFunction::instructions, klee::Expr::Int32, klee::Expr::Int64, klee::Expr::isTrue(), klee::klee_warning(), klee::klee_warning_once(), kmodule, memory, klee::ExecutionState::pc, klee::ExecutionState::prevPC, klee::ExecutionState::pushFrame(), klee::ObjectState::read8(), klee::AddressSpace::resolveOne(), klee::ObjectState::size, klee::ExecutionState::stack, statsTracker, terminateStateEarly(), terminateStateOnExecError(), terminateStateOnUserError(), toConstant(), transferToBasicBlock(), klee::Cell::value, klee::StackFrame::varargs, and klee::ObjectState::write().
Referenced by executeInstruction().
|
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 4076 of file Executor.cpp.
References bindLocal(), klee::Expr::createIsZero(), klee::Expr::createPointer(), fork(), getAddressInfo(), klee::MemoryObject::isGlobal, klee::MemoryObject::isLocal, klee::ExprOptimizer::optimizeExpr(), optimizer, resolveExact(), and terminateStateOnError().
|
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 1314 of file Executor.cpp.
References bindLocal(), branch(), klee::ExecutionState::constraints, klee::TimingSolver::getValue(), klee::ExprOptimizer::optimizeExpr(), optimizer, klee::ExecutionState::queryMetaData, seedMap, klee::ConstraintManager::simplifyExpr(), and solver.
|
private |
Definition at line 2045 of file Executor.cpp.
References __attribute__(), klee::ExecutionState::addressSpace, klee::ConstantExpr::alloc(), bindLocal(), klee::Expr::Bool, branch(), klee::ExecutionState::constraints, klee::ConcatExpr::create(), klee::SelectExpr::create(), klee::ExtractExpr::create(), klee::ConstantExpr::create(), klee::Expr::createIsZero(), klee::ConcatExpr::createN(), klee::Expr::createPointer(), klee::Expr::createSExtToPointerWidth(), klee::Expr::createZExtToPointerWidth(), eval(), evalConstant(), executeAlloc(), executeCall(), executeMemoryOperation(), fork(), fpWidthToSemantics(), klee::StatsTracker::framePopped(), klee::Context::get(), klee::Context::getPointerWidth(), getTargetFunction(), klee::TimingSolver::getValue(), klee::Expr::getWidth(), getWidthForLLVMType(), klee::ConstantExpr::getZExtValue(), klee::ExecutionState::incomingBBIndex, klee::KGEPInstruction::indices, klee::KInstruction::inst, klee::Expr::Int32, klee::Expr::Int64, klee::Expr::isZero(), klee::klee_warning(), klee::klee_warning_once(), kmodule, legalFunctions, klee::StatsTracker::markBranchVisited(), klee::TimingSolver::mayBeTrue(), klee::KGEPInstruction::offset, klee::ExprOptimizer::optimizeExpr(), optimizer, klee::ExecutionState::pc, klee::ExecutionState::popFrame(), klee::ExecutionState::queryMetaData, solver, klee::ExecutionState::stack, statsTracker, terminateStateOnError(), terminateStateOnExecError(), terminateStateOnExit(), toConstant(), toUnique(), transferToBasicBlock(), klee::AddressSpace::unbindObject(), klee::ExecutionState::unwindingInformation, unwindToNextLandingpad(), and klee::Cell::value.
Referenced by run().
|
private |
Definition at line 4268 of file Executor.cpp.
References klee::ExecutionState::addSymbolic(), arrayCache, klee::ExecutionState::arrayNames, klee::SeedInfo::assignment, klee::Assignment::bindings, bindObjectInState(), KTestObject::bytes, klee::ArrayCache::CreateArray(), klee::SeedInfo::getNextInput(), KTestObject::name, klee::MemoryObject::name, KTestObject::numBytes, KTest::numObjects, KTest::objects, replayKTest, replayPosition, seedMap, klee::MemoryObject::size, terminateStateOnUserError(), and klee::ObjectState::write8().
|
private |
Definition at line 4141 of file Executor.cpp.
References klee::ExecutionState::addressSpace, bindLocal(), klee::ExecutionState::constraints, coreSolverTimeout, fork(), getAddressInfo(), klee::MemoryObject::getBoundsCheckOffset(), klee::MemoryObject::getBoundsCheckPointer(), klee::Expr::getMinBytesForWidth(), klee::MemoryObject::getOffsetExpr(), klee::Expr::getWidth(), getWidthForLLVMType(), klee::AddressSpace::getWriteable(), klee::KInstruction::inst, klee::Interpreter::interpreterOpts, klee::Interpreter::InterpreterOptions::MakeConcreteSymbolic, klee::TimingSolver::mustBeTrue(), klee::ExprOptimizer::optimizeExpr(), optimizer, klee::ExecutionState::pc, klee::ExecutionState::prevPC, klee::ExecutionState::queryMetaData, klee::ObjectState::read(), klee::ObjectState::readOnly, replaceReadWithSymbolic(), klee::AddressSpace::resolve(), klee::AddressSpace::resolveOne(), klee::TimingSolver::setTimeout(), klee::ConstraintManager::simplifyExpr(), klee::MemoryObject::size, solver, terminateStateOnError(), terminateStateOnSolverError(), toConstant(), and klee::ObjectState::write().
Referenced by executeCall(), and executeInstruction().
|
private |
Fork current and return states in which condition holds / does not hold, respectively. One of the states is necessarily the current state, and one of the states may be null.
Definition at line 1003 of file Executor.cpp.
References addConstraint(), addedStates, klee::ExecutionState::branch(), branch(), branchingPermitted(), klee::ExecutionState::constraints, coreSolverTimeout, klee::ExecutionState::coveredLines, klee::ExecutionState::coveredNew, klee::Expr::createIsZero(), klee::TimingSolver::evaluate(), klee::Solver::False, klee::ExecutionState::forkDisabled, klee::stats::forks, klee::stats::forkTime, klee::RNG::getBool(), klee::TimingSolver::getValue(), maxStaticPctChecks(), klee::TreeStreamWriter::open(), klee::ExecutionState::pathOS, pathWriter, klee::ExecutionState::pc, klee::ExecutionState::prevPC, processTree, klee::ExecutionState::ptreeNode, klee::ExecutionState::queryMetaData, replayKTest, replayPath, replayPosition, seedMap, klee::TimingSolver::setTimeout(), solver, klee::ExecutionState::symPathOS, symPathWriter, terminateStateEarly(), terminateStateOnSolverError(), theRNG, klee::Solver::True, and klee::Solver::Unknown.
Referenced by executeAlloc(), executeFree(), executeInstruction(), executeMemoryOperation(), and resolveExact().
|
private |
Get textual information regarding a memory address.
Definition at line 3543 of file Executor.cpp.
References klee::MemoryObject::address, klee::ExecutionState::addressSpace, klee::ImmutableMap< K, D, CMP >::begin(), klee::ExecutionState::constraints, klee::ImmutableMap< K, D, CMP >::end(), klee::MemoryObject::getAllocInfo(), klee::TimingSolver::getRange(), klee::TimingSolver::getValue(), klee::AddressSpace::objects, klee::ExecutionState::queryMetaData, klee::MemoryObject::size, solver, and klee::ImmutableMap< K, D, CMP >::upper_bound().
Referenced by executeFree(), executeMemoryOperation(), and resolveExact().
size_t Executor::getAllocationAlignment | ( | const llvm::Value * | allocSite | ) | const |
Definition at line 4588 of file Executor.cpp.
References klee::getDirectCallTarget(), klee::bits64::isPowerOfTwo(), klee::klee_warning_once(), and kmodule.
Referenced by allocateGlobalObjects(), and executeAlloc().
|
inlineprivate |
Definition at line 356 of file Executor.h.
References klee::KFunction::getArgRegister(), and klee::ExecutionState::stack.
Referenced by bindArgument().
|
overridevirtual |
Implements klee::Interpreter.
Definition at line 4460 of file Executor.cpp.
References klee::ConstantExpr::alloc(), klee::Expr::Bool, klee::ExecutionState::constraints, klee::ExprSMTLIBPrinter::generateOutput(), klee::TimingSolver::getConstraintLog(), klee::klee_warning(), klee::Interpreter::KQUERY, klee::ExprPPrinter::printConstraints(), klee::ExprSMTLIBPrinter::setOutput(), klee::ExprSMTLIBPrinter::setQuery(), klee::Interpreter::SMTLIB2, solver, and klee::Interpreter::STP.
|
overridevirtual |
Implements klee::Interpreter.
Definition at line 4545 of file Executor.cpp.
References klee::ExecutionState::coveredLines.
|
inlineprivate |
Definition at line 362 of file Executor.h.
References klee::KInstruction::dest, and klee::ExecutionState::stack.
Referenced by bindLocal().
|
private |
Return the typeid corresponding to a certain type_info
Definition at line 1641 of file Executor.cpp.
References klee::ConstantExpr::create(), eh_typeids, and klee::Expr::Int32.
Referenced by executeCall().
int * Executor::getErrnoLocation | ( | const ExecutionState & | state | ) | const |
Returns the errno location in memory of the state.
Returns the errno location in memory.
Definition at line 4667 of file Executor.cpp.
Referenced by allocateGlobalObjects(), and callExternalFunction().
|
inline |
Definition at line 487 of file Executor.h.
References interpreterHandler.
Referenced by klee::constructUserSearcher().
|
private |
Definition at line 3665 of file Executor.cpp.
References klee::KInstruction::info, klee::KInstruction::inst, kmodule, klee::ExecutionState::prevPC, and klee::ExecutionState::stack.
Referenced by terminateStateOnError().
|
inline |
Definition at line 552 of file Executor.h.
References mergingSearcher.
|
overridevirtual |
Implements klee::Interpreter.
Definition at line 4450 of file Executor.cpp.
References klee::TreeOStream::getID(), klee::ExecutionState::pathOS, and pathWriter.
|
overridevirtual |
Implements klee::Interpreter.
Definition at line 4455 of file Executor.cpp.
References klee::TreeOStream::getID(), klee::ExecutionState::symPathOS, and symPathWriter.
|
overridevirtual |
Implements klee::Interpreter.
Definition at line 4494 of file Executor.cpp.
References klee::ConstraintManager::addConstraint(), klee::ConstantExpr::alloc(), klee::Expr::Bool, klee::ExecutionState::cexPreferences, klee::ExecutionState::constraints, coreSolverTimeout, klee::Expr::createIsZero(), klee::TimingSolver::getInitialValues(), klee::klee_warning(), klee::TimingSolver::mustBeTrue(), klee::ExprPPrinter::printQuery(), klee::ExecutionState::queryMetaData, klee::TimingSolver::setTimeout(), solver, and klee::ExecutionState::symbolics.
|
private |
Compute the true target of a function call, resolving LLVM aliases and bitcasts.
Definition at line 2017 of file Executor.cpp.
Referenced by executeInstruction().
Expr::Width Executor::getWidthForLLVMType | ( | llvm::Type * | type | ) | const |
Definition at line 4584 of file Executor.cpp.
References kmodule.
Referenced by callExternalFunction(), evalConstant(), evalConstantExpr(), executeInstruction(), and executeMemoryOperation().
|
private |
Definition at line 758 of file Executor.cpp.
References evalConstant(), globalAddresses, and initializeGlobalAlias().
Referenced by initializeGlobalAlias(), and initializeGlobalAliases().
|
private |
Definition at line 789 of file Executor.cpp.
References initializeGlobalAlias(), and kmodule.
Referenced by initializeGlobals().
|
private |
Definition at line 572 of file Executor.cpp.
References evalConstant(), initializeGlobalObject(), kmodule, klee::ObjectState::write(), and klee::ObjectState::write8().
Referenced by initializeGlobalObject(), and initializeGlobalObjects().
|
private |
Definition at line 796 of file Executor.cpp.
References klee::ExecutionState::addressSpace, bindObjectInState(), klee::AddressSpace::copyOutConcretes(), externalDispatcher, globalObjects, initializeGlobalObject(), klee::ObjectState::initializeToRandom(), klee::klee_error(), kmodule, klee::ExternalDispatcher::resolveSymbol(), klee::MemoryObject::size, and klee::ObjectState::write8().
Referenced by initializeGlobals().
|
private |
Definition at line 634 of file Executor.cpp.
References allocateGlobalObjects(), initializeGlobalAliases(), and initializeGlobalObjects().
Referenced by runFunctionAsMain().
|
private |
Definition at line 947 of file Executor.cpp.
References addConstraint(), klee::ExecutionState::constraints, klee::stats::forks, klee::StatisticManager::getIndex(), klee::StatisticManager::getIndexedValue(), klee::KInstruction::getSourceLocation(), klee::TimingSolver::getValue(), klee::StatisticRecord::getValue(), klee::klee_warning_once(), klee::ExecutionState::prevPC, klee::ExecutionState::queryMetaData, solver, klee::stats::solverTime, klee::ExecutionState::stack, klee::CallPathNode::statistics, and klee::theStatisticManager.
Referenced by fork().
|
overridevirtual |
Implements klee::Interpreter.
Definition at line 4659 of file Executor.cpp.
References klee::StatsTracker::done(), and statsTracker.
|
private |
Definition at line 1361 of file Executor.cpp.
References klee::InstructionInfo::assemblyLine, debugBufferString, debugLogBuffer, klee::ExecutionState::getID(), klee::KInstruction::getSourceLocation(), klee::KInstruction::info, klee::KInstruction::inst, and klee::ExecutionState::pc.
Referenced by stepInstruction().
|
private |
Definition at line 3911 of file Executor.cpp.
References klee::ExecutionState::addConstraint(), arrayCache, klee::NotOptimizedExpr::create(), klee::ArrayCache::CreateArray(), klee::Expr::createTempRead(), klee::floats::eq(), klee::Expr::getMinBytesForWidth(), klee::Expr::getWidth(), klee::Interpreter::interpreterOpts, klee::Interpreter::InterpreterOptions::MakeConcreteSymbolic, replayKTest, and replayPath.
Referenced by executeMemoryOperation().
|
private |
Definition at line 4110 of file Executor.cpp.
References klee::ExecutionState::addressSpace, fork(), getAddressInfo(), klee::ExprOptimizer::optimizeExpr(), optimizer, klee::AddressSpace::resolve(), solver, and terminateStateOnError().
Referenced by executeFree().
|
private |
Definition at line 3442 of file Executor.cpp.
References bindModuleConstants(), checkMemoryUsage(), klee::constructUserSearcher(), doDumpStates(), dumpPTree(), dumpStates(), executeInstruction(), klee::time::getWallTime(), haltExecution, klee::stats::instructions, klee::TimerGroup::invoke(), klee::klee_message(), klee::klee_warning(), klee::ExecutionState::pc, klee::TimerGroup::reset(), searcher, klee::time::seconds(), seedMap, klee::Searcher::selectState(), states, stepInstruction(), timers, klee::Searcher::update(), updateStates(), and usingSeeds.
Referenced by runFunctionAsMain().
|
overridevirtual |
Implements klee::Interpreter.
Definition at line 4344 of file Executor.cpp.
References klee::MemoryObject::address, klee::ConstantExpr::alloc(), klee::MemoryManager::allocate(), bindArgument(), bindObjectInState(), klee::Expr::createPointer(), klee::StatsTracker::done(), klee::StatsTracker::framePushed(), klee::Context::get(), klee::MemoryObject::getBaseExpr(), klee::Context::getPointerWidth(), globalAddresses, globalObjects, initializeGlobals(), klee::KInstruction::inst, klee::Expr::Int32, klee::klee_error(), kmodule, memory, klee::TreeStreamWriter::open(), klee::ExecutionState::pathOS, pathWriter, klee::ExecutionState::pc, processTree, run(), statsTracker, klee::ExecutionState::symPathOS, symPathWriter, klee::ObjectState::write(), and klee::ObjectState::write8().
|
private |
Serialize a landingpad instruction so it can be handled by the libcxxabi-runtime
Definition at line 1429 of file Executor.cpp.
References klee::MemoryManager::allocate(), bindObjectInState(), globalAddresses, memory, terminateStateOnExecError(), and klee::ObjectState::write8().
Referenced by unwindToNextLandingpad().
|
inlineoverridevirtual |
Implements klee::Interpreter.
Definition at line 521 of file Executor.h.
References haltExecution.
Referenced by Executor().
|
inlineoverridevirtual |
|
inline |
Definition at line 553 of file Executor.h.
References mergingSearcher.
Referenced by klee::constructUserSearcher().
|
overridevirtual |
Register the module to be executed.
modules | A list of modules that should form the final module |
Implements klee::Interpreter.
Definition at line 499 of file Executor.cpp.
References klee::SpecialFunctionHandler::bind(), klee::Interpreter::ModuleOptions::EntryPoint, klee::InterpreterHandler::getOutputFilename(), klee::Context::initialize(), interpreterHandler, klee::klee_error(), kmodule, klee::Interpreter::ModuleOptions::LibraryDir, klee::loadFile(), klee::Interpreter::ModuleOptions::OptSuffix, klee::SpecialFunctionHandler::prepare(), SpecialFunctionHandler, specialFunctionHandler, StatsTracker, statsTracker, klee::userSearcherRequiresMD2U(), and klee::StatsTracker::useStatistics().
|
inlineoverridevirtual |
|
inlineoverridevirtual |
Implements klee::Interpreter.
Definition at line 497 of file Executor.h.
References replayKTest, replayPath, and replayPosition.
|
inlineoverridevirtual |
Implements klee::Interpreter.
Definition at line 503 of file Executor.h.
References replayKTest, replayPath, and replayPosition.
|
inlineoverridevirtual |
|
private |
Definition at line 1402 of file Executor.cpp.
References haltExecution, klee::stats::instructions, klee::ExecutionState::pc, klee::ExecutionState::prevPC, printDebugInstructions(), statsTracker, klee::StatsTracker::stepInstruction(), and klee::ExecutionState::steppedInstructions.
Referenced by run().
|
private |
Remove state from queue and delete state.
Definition at line 3596 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, removedStates, replayKTest, replayPosition, and seedMap.
Referenced by terminateStateEarly(), terminateStateOnError(), and terminateStateOnExit().
|
private |
Call exit handler and terminate state early (e.g. due to state merging or memory pressure)
Definition at line 3648 of file Executor.cpp.
References interpreterHandler, message, klee::InterpreterHandler::processTestCase(), seedMap, shouldWriteTest(), terminateState(), and terminationTypeFileExtension().
Referenced by klee::MergeHandler::addClosedState(), branch(), checkMemoryUsage(), doDumpStates(), executeCall(), and fork().
|
private |
Call error handler and terminate state in case of program errors (e.g. free()ing globals, out-of-bound accesses)
Definition at line 3713 of file Executor.cpp.
References klee::InstructionInfo::assemblyLine, klee::ExecutionState::dumpStack(), klee::floats::ext(), klee::InstructionInfo::file, klee::ExecutionState::getID(), getLastNonKleeInternalInstruction(), haltExecution, interpreterHandler, klee::klee_message(), klee::InstructionInfo::line, message, klee::InterpreterHandler::processTestCase(), shouldExitOn(), suffix, terminateState(), and terminationTypeFileExtension().
Referenced by callExternalFunction(), executeAlloc(), executeFree(), executeInstruction(), executeMemoryOperation(), resolveExact(), terminateStateOnExecError(), terminateStateOnSolverError(), and terminateStateOnUserError().
|
private |
Call error handler and terminate state in case of execution errors (things that should not be possible, like illegal instruction or unlowered intrinsic, or unsupported intrinsics, like inline assembly)
Definition at line 3761 of file Executor.cpp.
References message, and terminateStateOnError().
Referenced by callExternalFunction(), executeCall(), executeInstruction(), klee::SpecialFunctionHandler::handle(), serializeLandingpad(), and unwindToNextLandingpad().
|
private |
Call exit handler and terminate state normally (end of execution path)
Definition at line 3638 of file Executor.cpp.
References klee::InterpreterHandler::incPathsCompleted(), interpreterHandler, klee::InterpreterHandler::processTestCase(), seedMap, shouldWriteTest(), terminateState(), and terminationTypeFileExtension().
Referenced by executeInstruction().
|
private |
Call error handler and terminate state in case of solver errors (solver error or timeout)
Definition at line 3767 of file Executor.cpp.
References message, and terminateStateOnError().
Referenced by executeMemoryOperation(), and fork().
|
private |
Call error handler and terminate state for user errors (e.g. wrong usage of klee.h API)
Definition at line 3661 of file Executor.cpp.
References message, and terminateStateOnError().
Referenced by callExternalFunction(), executeCall(), executeMakeSymbolic(), and klee::SpecialFunctionHandler::readStringAtAddress().
|
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.
purpose | An identify string to printed in case of concretization. |
Definition at line 1285 of file Executor.cpp.
References addConstraint(), klee::ExecutionState::constraints, klee::TimingSolver::getValue(), klee::klee_warning(), klee::klee_warning_once(), klee::ExecutionState::pc, klee::ExecutionState::queryMetaData, klee::ConstraintManager::simplifyExpr(), and solver.
Referenced by executeCall(), executeInstruction(), and executeMemoryOperation().
|
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 1258 of file Executor.cpp.
References klee::ExecutionState::constraints, coreSolverTimeout, klee::TimingSolver::getValue(), klee::TimingSolver::mustBeTrue(), klee::ExprOptimizer::optimizeExpr(), optimizer, klee::ExecutionState::queryMetaData, klee::TimingSolver::setTimeout(), and solver.
Referenced by callExternalFunction(), executeAlloc(), executeInstruction(), and klee::SpecialFunctionHandler::readStringAtAddress().
|
private |
Definition at line 1991 of file Executor.cpp.
References klee::KFunction::basicBlockEntry, klee::ExecutionState::incomingBBIndex, klee::KInstruction::inst, klee::KFunction::instructions, klee::ExecutionState::pc, and klee::ExecutionState::stack.
Referenced by executeCall(), executeInstruction(), and unwindToNextLandingpad().
|
private |
Unwind the given state until it hits a landingpad. This is used for exception handling.
Definition at line 1532 of file Executor.cpp.
References bindArgument(), klee::StatsTracker::framePopped(), klee::StatsTracker::framePushed(), klee::MemoryObject::getBaseExpr(), klee::MemoryObject::getSizeExpr(), klee::KFunction::instructions, kmodule, klee::ExecutionState::pc, klee::ExecutionState::popFrame(), klee::ExecutionState::prevPC, klee::ExecutionState::pushFrame(), serializeLandingpad(), klee::ExecutionState::stack, statsTracker, terminateStateOnExecError(), transferToBasicBlock(), and klee::ExecutionState::unwindingInformation.
Referenced by executeInstruction().
|
private |
Definition at line 3289 of file Executor.cpp.
References addedStates, processTree, klee::ExecutionState::ptreeNode, removedStates, searcher, seedMap, states, and klee::Searcher::update().
Referenced by doDumpStates(), and run().
|
inlineoverridevirtual |
|
friend |
|
friend |
Definition at line 97 of file Executor.h.
|
friend |
Definition at line 93 of file Executor.h.
|
friend |
Definition at line 95 of file Executor.h.
Referenced by setModule().
|
friend |
Definition at line 96 of file Executor.h.
Referenced by setModule().
|
friend |
Definition at line 94 of file Executor.h.
|
private |
Used to track states that have been added during the current instructions step.
Definition at line 125 of file Executor.h.
Referenced by branch(), fork(), terminateState(), and updateStates().
|
private |
Assumes ownership of the created array objects.
Definition at line 190 of file Executor.h.
Referenced by executeMakeSymbolic(), Executor(), and replaceReadWithSymbolic().
|
private |
Disables forking, instead a random path is chosen. Enabled as needed to control memory usage.
Definition at line 169 of file Executor.h.
Referenced by branchingPermitted(), and checkMemoryUsage().
|
private |
The maximum time to allow for a single core solver query. (e.g. for a single STP query)
Definition at line 184 of file Executor.h.
Referenced by executeMemoryOperation(), Executor(), fork(), getSymbolicSolution(), and toUnique().
|
private |
Definition at line 196 of file Executor.h.
Referenced by printDebugInstructions().
|
private |
File to print executed instructions to.
Definition at line 193 of file Executor.h.
Referenced by Executor().
|
private |
Definition at line 199 of file Executor.h.
Referenced by printDebugInstructions().
Typeids used during exception handling.
Definition at line 209 of file Executor.h.
Referenced by getEhTypeidFor().
|
private |
Definition at line 111 of file Executor.h.
Referenced by allocateGlobalObjects(), callExternalFunction(), initializeGlobalObjects(), and ~Executor().
|
private |
Map of globals to their bound address. This also includes globals that have no representative object (i.e. functions).
Definition at line 146 of file Executor.h.
Referenced by allocateGlobalObjects(), evalConstant(), initializeGlobalAlias(), runFunctionAsMain(), and serializeLandingpad().
|
private |
Map of globals to their representative memory object.
Definition at line 142 of file Executor.h.
Referenced by allocateGlobalObjects(), initializeGlobalObjects(), and runFunctionAsMain().
|
private |
Signals the executor to halt execution at the next instruction step.
Definition at line 176 of file Executor.h.
Referenced by run(), setHaltExecution(), stepInstruction(), and terminateStateOnError().
|
private |
Disables forking, set by client.
Definition at line 172 of file Executor.h.
Referenced by branchingPermitted(), and setInhibitForking().
|
private |
Definition at line 108 of file Executor.h.
Referenced by doDumpStates(), dumpPTree(), dumpStates(), Executor(), getHandler(), setModule(), klee::StatsTracker::StatsTracker(), terminateState(), terminateStateEarly(), terminateStateOnError(), and terminateStateOnExit().
|
private |
Whether implied-value concretization is enabled. Currently false, it is buggy (it needs to validate its writes).
Definition at line 180 of file Executor.h.
Referenced by addConstraint().
|
private |
Definition at line 107 of file Executor.h.
Referenced by allocateGlobalObjects(), klee::SpecialFunctionHandler::bind(), bindModuleConstants(), computeOffsets(), computeOffsetsSeqTy(), klee::StatsTracker::computeReachableUncovered(), eval(), evalConstant(), evalConstantExpr(), executeCall(), executeInstruction(), getAllocationAlignment(), getLastNonKleeInternalInstruction(), getWidthForLLVMType(), initializeGlobalAliases(), initializeGlobalObject(), initializeGlobalObjects(), klee::SpecialFunctionHandler::prepare(), runFunctionAsMain(), setModule(), klee::StatsTracker::StatsTracker(), unwindToNextLandingpad(), and klee::StatsTracker::writeIStats().
|
private |
Map of legal function addresses to the corresponding Function. Used to validate and dereference function pointers.
Definition at line 150 of file Executor.h.
Referenced by allocateGlobalObjects(), and executeInstruction().
|
private |
Maximum time to allow for a single instruction.
Definition at line 187 of file Executor.h.
|
private |
Definition at line 113 of file Executor.h.
Referenced by addExternalObject(), allocateGlobalObjects(), checkMemoryUsage(), executeAlloc(), executeCall(), Executor(), runFunctionAsMain(), serializeLandingpad(), klee::StatsTracker::writeStatsLine(), and ~Executor().
|
private |
Points to the merging searcher of the searcher chain, nullptr
if merging is disabled
Definition at line 206 of file Executor.h.
Referenced by klee::MergeHandler::addClosedState(), getMergingSearcher(), klee::MergeHandler::getPrioritizeState(), klee::MergeHandler::MergeHandler(), klee::MergeHandler::releaseStates(), setMergingSearcher(), and klee::MergeHandler::~MergeHandler().
|
private |
Optimizes expressions.
Definition at line 202 of file Executor.h.
Referenced by callExternalFunction(), executeAlloc(), executeFree(), executeGetValue(), executeInstruction(), executeMemoryOperation(), resolveExact(), and toUnique().
|
private |
Definition at line 116 of file Executor.h.
Referenced by fork(), getPathStreamID(), runFunctionAsMain(), and setPathWriter().
|
private |
Definition at line 119 of file Executor.h.
Referenced by branch(), klee::constructUserSearcher(), dumpPTree(), fork(), runFunctionAsMain(), terminateState(), and updateStates().
|
private |
Used to track states that have been removed during the current instructions step.
Definition at line 130 of file Executor.h.
Referenced by terminateState(), and updateStates().
|
private |
When non-null the bindings that will be used for calls to klee_make_symbolic in order replay.
Definition at line 154 of file Executor.h.
Referenced by executeMakeSymbolic(), fork(), replaceReadWithSymbolic(), setReplayKTest(), setReplayPath(), and terminateState().
|
private |
When non-null a list of branch decisions to be used for replay.
Definition at line 157 of file Executor.h.
Referenced by fork(), replaceReadWithSymbolic(), setReplayKTest(), and setReplayPath().
|
private |
The index into the current replayKTest or replayPath object.
Definition at line 161 of file Executor.h.
Referenced by executeMakeSymbolic(), fork(), setReplayKTest(), setReplayPath(), and terminateState().
|
private |
Definition at line 109 of file Executor.h.
Referenced by run(), and updateStates().
|
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 139 of file Executor.h.
Referenced by addConstraint(), branch(), executeGetValue(), executeMakeSymbolic(), fork(), run(), terminateState(), terminateStateEarly(), terminateStateOnExit(), and updateStates().
|
private |
Definition at line 112 of file Executor.h.
Referenced by addConstraint(), branch(), callExternalFunction(), doImpliedValueConcretization(), executeAlloc(), executeGetValue(), executeInstruction(), executeMemoryOperation(), Executor(), fork(), getAddressInfo(), getConstraintLog(), getSymbolicSolution(), maxStaticPctChecks(), resolveExact(), toConstant(), toUnique(), and ~Executor().
|
private |
Definition at line 117 of file Executor.h.
Referenced by callExternalFunction(), setModule(), and ~Executor().
|
private |
Definition at line 114 of file Executor.h.
Referenced by checkMemoryUsage(), klee::StatsTracker::computeReachableUncovered(), doDumpStates(), dumpStates(), run(), updateStates(), klee::StatsTracker::updateStateStatistics(), and klee::StatsTracker::writeStatsLine().
|
private |
Definition at line 115 of file Executor.h.
Referenced by executeCall(), executeInstruction(), prepareForEarlyExit(), runFunctionAsMain(), setModule(), stepInstruction(), unwindToNextLandingpad(), and ~Executor().
|
private |
Definition at line 116 of file Executor.h.
Referenced by fork(), getSymbolicPathStreamID(), runFunctionAsMain(), and setSymbolicPathWriter().
RNG klee::Executor::theRNG |
The random number generator.
Definition at line 104 of file Executor.h.
Referenced by branch(), checkMemoryUsage(), klee::constructUserSearcher(), and fork().
|
private |
Definition at line 118 of file Executor.h.
Referenced by Executor(), run(), and klee::StatsTracker::StatsTracker().
|
private |
When non-null a list of "seed" inputs which will be used to drive execution.
Definition at line 165 of file Executor.h.
Referenced by run(), and useSeeds().