klee::AddressSpace Class Reference

#include <AddressSpace.h>

Collaboration diagram for klee::AddressSpace:

List of all members.

Public Member Functions

AddressSpace ()

AddressSpace (const AddressSpace &b)

~AddressSpace ()

bool resolveOne (uint64_t 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.

void unbindObject (const MemoryObject *mo)

Remove a binding from the address space.

const ObjectState * findObject (const MemoryObject *mo) const

Lookup a binding from a MemoryObject.

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

Obtain an ObjectState suitable for writing.

void copyOutConcretes ()

bool copyInConcretes ()

Public Attributes

MemoryMap objects

Private Member Functions

AddressSpace & operator= (const AddressSpace &)

Unsupported, use copy constructor.

Private Attributes

unsigned cowKey

Epoch counter used to control ownership of objects.

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(), and klee::ExecutionState::cloneObject().

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:

	true	The copy succeeded.
	false	The copy failed because a read-only object was modified.

Definition at line 306 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.

Here is the call 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 291 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.

Here is the call 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:

	mo	The MemoryObject to get a writeable ObjectState for.
	os	The 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 160 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::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	(	ExecutionState &	state,
		TimingSolver *	solver,
		ref< Expr >	address,
		ObjectPair &	result,
		bool &	success
	)

Resolve address to an ObjectPair in result.

Parameters:

	state	The state this address space is part of.
	solver	A solver used to determine possible locations of the address.
	address	The address to search for.
`[out]`	result	An ObjectPair this address can resolve to (when returning true).

Returns:: true iff an object was found at address.

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

bool AddressSpace::resolveOne	(	uint64_t	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::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:

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 [mutable, private]

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:

lib/Core/AddressSpace.h
lib/Core/AddressSpace.cpp


Public Member Functions
	AddressSpace ()
	AddressSpace (const AddressSpace &b)
	~AddressSpace ()
bool	resolveOne (uint64_t 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.
void	unbindObject (const MemoryObject *mo)
	Remove a binding from the address space.
const ObjectState *	findObject (const MemoryObject *mo) const
	Lookup a binding from a MemoryObject.
ObjectState *	getWriteable (const MemoryObject mo, const ObjectState os)
	Obtain an ObjectState suitable for writing.
void	copyOutConcretes ()
bool	copyInConcretes ()
Public Attributes
MemoryMap	objects
Private Member Functions
AddressSpace &	operator= (const AddressSpace &)
	Unsupported, use copy constructor.
Private Attributes
unsigned	cowKey
	Epoch counter used to control ownership of objects.