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

#include <AddressSpace.h>

Collaboration diagram for klee::AddressSpace:

Public Member Functions

 AddressSpace ()
 
 AddressSpace (const AddressSpace &b)
 
 ~AddressSpace ()
 
bool resolveOne (const ref< ConstantExpr > &address, ObjectPair &result)
 
bool resolveOne (ExecutionState &state, TimingSolver *solver, ref< Expr > address, ObjectPair &result, bool &success)
 
bool resolve (ExecutionState &state, TimingSolver *solver, ref< Expr > address, ResolutionList &rl, unsigned maxResolutions=0, double timeout=0.)
 
void bindObject (const MemoryObject *mo, ObjectState *os)
 Add a binding to the address space. More...
 
void unbindObject (const MemoryObject *mo)
 Remove a binding from the address space. More...
 
const ObjectStatefindObject (const MemoryObject *mo) const
 Lookup a binding from a MemoryObject. More...
 
ObjectStategetWriteable (const MemoryObject *mo, const ObjectState *os)
 Obtain an ObjectState suitable for writing. More...
 
void copyOutConcretes ()
 
bool copyInConcretes ()
 

Public Attributes

MemoryMap objects
 

Private Member Functions

AddressSpaceoperator= (const AddressSpace &)
 Unsupported, use copy constructor. More...
 

Private Attributes

unsigned cowKey
 Epoch counter used to control ownership of objects. More...
 

Detailed Description

Definition at line 36 of file AddressSpace.h.

Constructor & Destructor Documentation

klee::AddressSpace::AddressSpace ( )
inline

Definition at line 55 of file AddressSpace.h.

klee::AddressSpace::AddressSpace ( const AddressSpace b)
inline

Definition at line 56 of file AddressSpace.h.

klee::AddressSpace::~AddressSpace ( )
inline

Definition at line 57 of file AddressSpace.h.

Member Function Documentation

void AddressSpace::bindObject ( const MemoryObject mo,
ObjectState os 
)

Add a binding to the address space.

Definition at line 22 of file AddressSpace.cpp.

References klee::ObjectState::copyOnWriteOwner, cowKey, objects, and klee::ImmutableMap< K, D, CMP >::replace().

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

Here is the call graph for this function:

Here is the caller graph for this function:

bool AddressSpace::copyInConcretes ( )

Copy the concrete values of all managed ObjectStates back from the actual system memory location they were allocated at. ObjectStates will only be written to (and thus, potentially copied) if the memory values are different from the current concrete values.

Return values
trueThe copy succeeded.
falseThe copy failed because a read-only object was modified.

Definition at line 307 of file AddressSpace.cpp.

References klee::MemoryObject::address, klee::ImmutableMap< K, D, CMP >::begin(), klee::ObjectState::concreteStore, klee::ImmutableMap< K, D, CMP >::end(), getWriteable(), klee::MemoryObject::isUserSpecified, objects, klee::ObjectState::readOnly, and klee::MemoryObject::size.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void AddressSpace::copyOutConcretes ( )

Copy the concrete values of all managed ObjectStates into the actual system memory location they were allocated at.

Definition at line 292 of file AddressSpace.cpp.

References klee::MemoryObject::address, klee::ImmutableMap< K, D, CMP >::begin(), klee::ObjectState::concreteStore, klee::ImmutableMap< K, D, CMP >::end(), klee::MemoryObject::isUserSpecified, objects, klee::ObjectState::readOnly, and klee::MemoryObject::size.

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

Here is the call graph for this function:

Here is the caller graph for this function:

const ObjectState * AddressSpace::findObject ( const MemoryObject mo) const

Lookup a binding from a MemoryObject.

Definition at line 32 of file AddressSpace.cpp.

References klee::ImmutableMap< K, D, CMP >::lookup(), and objects.

Referenced by klee::Executor::doImpliedValueConcretization(), klee::Executor::initializeGlobals(), and klee::ExecutionState::merge().

Here is the call graph for this function:

Here is the caller graph for this function:

ObjectState * AddressSpace::getWriteable ( const MemoryObject mo,
const ObjectState os 
)

Obtain an ObjectState suitable for writing.

This returns a writeable object state, creating a new copy of the given ObjectState if necessary. If the address space owns the ObjectState then this routine effectively just strips the const qualifier it.

Parameters
moThe MemoryObject to get a writeable ObjectState for.
osThe current binding of the MemoryObject.
Returns
A writeable ObjectState (os or a copy).

Definition at line 38 of file AddressSpace.cpp.

References klee::ObjectState::copyOnWriteOwner, cowKey, objects, klee::ObjectState::readOnly, and klee::ImmutableMap< K, D, CMP >::replace().

Referenced by copyInConcretes(), klee::Executor::doImpliedValueConcretization(), klee::Executor::executeMemoryOperation(), klee::Executor::initializeGlobals(), and klee::ExecutionState::merge().

Here is the call graph for this function:

Here is the caller graph for this function:

AddressSpace& klee::AddressSpace::operator= ( const AddressSpace )
private

Unsupported, use copy constructor.

bool AddressSpace::resolve ( ExecutionState state,
TimingSolver solver,
ref< Expr address,
ResolutionList rl,
unsigned  maxResolutions = 0,
double  timeout = 0. 
)

Resolve address to a list of ObjectPairs it can point to. If maxResolutions is non-zero then no more than that many pairs will be returned.

Returns
true iff the resolution is incomplete (maxResolutions is non-zero and the search terminated early, or a query timed out).

Definition at line 161 of file AddressSpace.cpp.

References klee::ImmutableMap< K, D, CMP >::begin(), klee::TimerStatIncrementer::check(), klee::ImmutableMap< K, D, CMP >::end(), klee::MemoryObject::getBaseExpr(), klee::MemoryObject::getBoundsCheckPointer(), klee::TimingSolver::getValue(), klee::ConstantExpr::getZExtValue(), klee::TimingSolver::mayBeTrue(), klee::TimingSolver::mustBeTrue(), objects, resolveOne(), klee::stats::resolveTime, and klee::ImmutableMap< K, D, CMP >::upper_bound().

Referenced by klee::Executor::executeMemoryOperation(), and klee::Executor::resolveExact().

Here is the call graph for this function:

Here is the caller graph for this function:

bool AddressSpace::resolveOne ( const ref< ConstantExpr > &  address,
ObjectPair result 
)

Resolve address to an ObjectPair in result.

Returns
true iff an object was found.

Definition at line 54 of file AddressSpace.cpp.

References klee::MemoryObject::address, klee::ConstantExpr::getZExtValue(), klee::ImmutableMap< K, D, CMP >::lookup_previous(), objects, and klee::MemoryObject::size.

Referenced by klee::Executor::executeMemoryOperation(), klee::SpecialFunctionHandler::readStringAtAddress(), resolve(), and resolveOne().

Here is the call graph for this function:

Here is the caller graph for this function:

bool AddressSpace::resolveOne ( ExecutionState state,
TimingSolver solver,
ref< Expr address,
ObjectPair result,
bool &  success 
)

Resolve address to an ObjectPair in result.

Parameters
stateThe state this address space is part of.
solverA solver used to determine possible locations of the address.
addressThe address to search for.
[out]resultAn ObjectPair this address can resolve to (when returning true).
Returns
true iff an object was found at address.

Definition at line 71 of file AddressSpace.cpp.

References klee::MemoryObject::address, klee::ImmutableMap< K, D, CMP >::begin(), klee::ImmutableMap< K, D, CMP >::end(), klee::MemoryObject::getBaseExpr(), klee::MemoryObject::getBoundsCheckPointer(), klee::TimingSolver::getValue(), klee::ConstantExpr::getZExtValue(), klee::ImmutableMap< K, D, CMP >::lookup_previous(), klee::TimingSolver::mayBeTrue(), klee::TimingSolver::mustBeTrue(), objects, resolveOne(), klee::stats::resolveTime, klee::MemoryObject::size, and klee::ImmutableMap< K, D, CMP >::upper_bound().

Here is the call graph for this function:

void AddressSpace::unbindObject ( const MemoryObject mo)

Remove a binding from the address space.

Definition at line 28 of file AddressSpace.cpp.

References objects, and klee::ImmutableMap< K, D, CMP >::remove().

Referenced by klee::Executor::executeAlloc(), and klee::ExecutionState::popFrame().

Here is the call graph for this function:

Here is the caller graph for this function:

Member Data Documentation

unsigned klee::AddressSpace::cowKey
mutableprivate

Epoch counter used to control ownership of objects.

Definition at line 39 of file AddressSpace.h.

Referenced by bindObject(), and getWriteable().

MemoryMap klee::AddressSpace::objects

The MemoryObject -> ObjectState map that constitutes the address space.

The set of objects where o->copyOnWriteOwner == cowKey are the objects that we own.

Invariant
forall o in objects, o->copyOnWriteOwner <= cowKey

Definition at line 52 of file AddressSpace.h.

Referenced by bindObject(), copyInConcretes(), copyOutConcretes(), findObject(), klee::Executor::getAddressInfo(), getWriteable(), klee::ExecutionState::merge(), resolve(), resolveOne(), and unbindObject().


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