#include <AddressSpace.h>

Collaboration diagram for klee::AddressSpace:

[legend]

Public Member Functions
	AddressSpace ()

	AddressSpace (const AddressSpace &b)

	~AddressSpace ()

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

bool	resolveOne (ExecutionState &state, TimingSolver *solver, ref< Expr > address, ObjectPair &result, bool &success) const

bool	resolve (ExecutionState &state, TimingSolver *solver, ref< Expr > p, ResolutionList &rl, unsigned maxResolutions=0, time::Span timeout=time::Span()) const

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 ObjectState *	findObject (const MemoryObject *mo) const
	Lookup a binding from a MemoryObject. More...

ObjectState *	getWriteable (const MemoryObject mo, const ObjectState os)
	Obtain an ObjectState suitable for writing. More...

void	copyOutConcretes ()

bool	copyInConcretes ()

bool	copyInConcrete (const MemoryObject mo, const ObjectState os, uint64_t src_address)

Public Attributes
MemoryMap	objects

Private Member Functions
AddressSpace &	operator= (const AddressSpace &)
	Unsupported, use copy constructor. More...

int	checkPointerInObject (ExecutionState &state, TimingSolver *solver, ref< Expr > p, const ObjectPair &op, ResolutionList &rl, unsigned maxResolutions) const

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

Detailed Description

Definition at line 38 of file AddressSpace.h.

Constructor & Destructor Documentation

◆ AddressSpace() [1/2]

klee::AddressSpace::AddressSpace ( )

inline

Definition at line 67 of file AddressSpace.h.

◆ AddressSpace() [2/2]

klee::AddressSpace::AddressSpace ( const AddressSpace & b )

inline

Definition at line 68 of file AddressSpace.h.

◆ ~AddressSpace()

klee::AddressSpace::~AddressSpace ( )

inline

Definition at line 69 of file AddressSpace.h.

Member Function Documentation

◆ bindObject()

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

Add a binding to the address space.

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

◆ checkPointerInObject()

int AddressSpace::checkPointerInObject	(	ExecutionState &	state,
		TimingSolver *	solver,
		ref< Expr >	p,
		const ObjectPair &	op,
		ResolutionList &	rl,
		unsigned	maxResolutions
	)		const

private

Check if pointer p can point to the memory object in the given object pair. If so, add it to the given resolution list.

Returns: 1 iff the resolution is incomplete (maxResolutions is non-zero and it was reached, or a query timed out), 0 iff the resolution is complete (p can only point to the given memory object), and 2 otherwise.

Definition at line 171 of file AddressSpace.cpp.

References klee::ExecutionState::constraints, klee::MemoryObject::getBoundsCheckPointer(), klee::TimingSolver::mayBeTrue(), klee::TimingSolver::mustBeTrue(), and klee::ExecutionState::queryMetaData.

Referenced by resolve().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ copyInConcrete()

bool AddressSpace::copyInConcrete	(	const MemoryObject *	mo,
		const ObjectState *	os,
		uint64_t	src_address
	)

Updates the memory object with the raw memory from the address

Parameters

mo	The MemoryObject to update
os	The associated memory state containing the actual data
src_address	the address to copy from

Returns

Definition at line 330 of file AddressSpace.cpp.

References klee::ObjectState::concreteStore, getWriteable(), klee::ObjectState::readOnly, and klee::MemoryObject::size.

Referenced by klee::Executor::callExternalFunction(), and copyInConcretes().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ copyInConcretes()

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 315 of file AddressSpace.cpp.

References klee::MemoryObject::address, copyInConcrete(), klee::MemoryObject::isUserSpecified, and objects.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ copyOutConcretes()

void AddressSpace::copyOutConcretes ( )

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

Definition at line 300 of file AddressSpace.cpp.

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

Referenced by klee::Executor::callExternalFunction(), and klee::Executor::initializeGlobalObjects().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ findObject()

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

Lookup a binding from a MemoryObject.

Definition at line 35 of file AddressSpace.cpp.

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

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getWriteable()

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 40 of file AddressSpace.cpp.

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

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ operator=()

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

private

Unsupported, use copy constructor.

◆ resolve()

bool AddressSpace::resolve	(	ExecutionState &	state,
		TimingSolver *	solver,
		ref< Expr >	p,
		ResolutionList &	rl,
		unsigned	maxResolutions = `0`,
		time::Span	timeout = `time::Span()`
	)		const

Resolve pointer p 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 it was reached, or a query timed out).

Definition at line 207 of file AddressSpace.cpp.

References klee::ImmutableMap< K, D, CMP >::begin(), checkPointerInObject(), klee::ExecutionState::constraints, klee::TimerStatIncrementer::delta(), klee::ImmutableMap< K, D, CMP >::end(), klee::MemoryObject::getBaseExpr(), klee::TimingSolver::getValue(), klee::TimingSolver::mustBeTrue(), objects, klee::ExecutionState::queryMetaData, 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:

◆ resolveOne() [1/2]

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

Resolve address to an ObjectPair in result.

Returns: true iff an object was found.

Definition at line 57 of file AddressSpace.cpp.

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

Referenced by klee::Executor::callExternalFunction(), klee::Executor::executeCall(), 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:

◆ resolveOne() [2/2]

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

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 77 of file AddressSpace.cpp.

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

Here is the call graph for this function:

◆ unbindObject()

void AddressSpace::unbindObject ( const MemoryObject * mo )

Remove a binding from the address space.

Definition at line 31 of file AddressSpace.cpp.

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

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

Here is the call graph for this function:

Here is the caller graph for this function:

Member Data Documentation

◆ cowKey

unsigned klee::AddressSpace::cowKey

mutableprivate

Epoch counter used to control ownership of objects.

Definition at line 41 of file AddressSpace.h.

Referenced by bindObject(), and getWriteable().

◆ objects

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 65 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:

/Users/cristic/klee/lib/Core/AddressSpace.h
/Users/cristic/klee/lib/Core/AddressSpace.cpp

Public Member Functions

Public Attributes

Private Member Functions

Private Attributes

Detailed Description

Constructor & Destructor Documentation

◆ AddressSpace() [1/2]

◆ AddressSpace() [2/2]

◆ ~AddressSpace()

Member Function Documentation

◆ bindObject()

◆ checkPointerInObject()

◆ copyInConcrete()

◆ copyInConcretes()

◆ copyOutConcretes()

◆ findObject()

◆ getWriteable()

◆ operator=()

◆ resolve()

◆ resolveOne() [1/2]

◆ resolveOne() [2/2]

◆ unbindObject()

Member Data Documentation

◆ cowKey

◆ objects