#include <Memory.h>

Collaboration diagram for klee::ObjectState:

[legend]

Public Member Functions
	ObjectState (const MemoryObject *mo)

	ObjectState (const MemoryObject mo, const Array array)

	ObjectState (const ObjectState &os)

	~ObjectState ()

const MemoryObject *	getObject () const

void	setReadOnly (bool ro)

void	initializeToZero ()
	Make contents all concrete and zero. More...

void	initializeToRandom ()
	Make contents all concrete and random. More...

ref< Expr >	read (ref< Expr > offset, Expr::Width width) const

ref< Expr >	read (unsigned offset, Expr::Width width) const

ref< Expr >	read8 (unsigned offset) const

void	write (unsigned offset, ref< Expr > value)

void	write (ref< Expr > offset, ref< Expr > value)

void	write8 (unsigned offset, uint8_t value)

void	write16 (unsigned offset, uint16_t value)

void	write32 (unsigned offset, uint32_t value)

void	write64 (unsigned offset, uint64_t value)

void	print () const

void	flushToConcreteStore (TimingSolver *solver, const ExecutionState &state) const

Public Attributes
unsigned	size

bool	readOnly

Private Member Functions
const UpdateList &	getUpdates () const

void	makeConcrete ()

void	makeSymbolic ()

ref< Expr >	read8 (ref< Expr > offset) const

void	write8 (unsigned offset, ref< Expr > value)

void	write8 (ref< Expr > offset, ref< Expr > value)

void	fastRangeCheckOffset (ref< Expr > offset, unsigned base_r, unsigned size_r) const

void	flushRangeForRead (unsigned rangeBase, unsigned rangeSize) const

void	flushRangeForWrite (unsigned rangeBase, unsigned rangeSize)

bool	isByteConcrete (unsigned offset) const
	isByteConcrete ==> !isByteKnownSymbolic More...

bool	isByteKnownSymbolic (unsigned offset) const
	isByteKnownSymbolic ==> !isByteConcrete More...

bool	isByteUnflushed (unsigned offset) const
	isByteUnflushed(i) => (isByteConcrete(i) \|\| isByteKnownSymbolic(i)) More...

void	markByteConcrete (unsigned offset)

void	markByteSymbolic (unsigned offset)

void	markByteFlushed (unsigned offset)

void	markByteUnflushed (unsigned offset)

void	setKnownSymbolic (unsigned offset, Expr *value)

ArrayCache *	getArrayCache () const

Private Attributes
unsigned	copyOnWriteOwner

class ReferenceCounter	_refCount
	Required by klee::ref-managed objects. More...

ref< const MemoryObject >	object

uint8_t *	concreteStore
	Holds all known concrete bytes. More...

BitArray *	concreteMask
	concreteMask[byte] is set if byte is known to be concrete More...

ref< Expr > *	knownSymbolics

BitArray *	unflushedMask

UpdateList	updates

Friends
class	AddressSpace

class	ref< ObjectState >

Detailed Description

Definition at line 163 of file Memory.h.

Constructor & Destructor Documentation

◆ ObjectState() [1/3]

ObjectState::ObjectState ( const MemoryObject * mo )

Create a new object state for the given memory object with concrete contents. The initial contents are undefined, it is the callers responsibility to initialize the object contents appropriately.

Definition at line 76 of file Memory.cpp.

References concreteStore, klee::ArrayCache::CreateArray(), getArrayCache(), size, and updates.

Here is the call graph for this function:

◆ ObjectState() [2/3]

ObjectState::ObjectState	(	const MemoryObject *	mo,
		const Array *	array
	)

Create a new object state for the given memory object with symbolic contents.

Definition at line 96 of file Memory.cpp.

References concreteStore, makeSymbolic(), and size.

Here is the call graph for this function:

◆ ObjectState() [3/3]

ObjectState::ObjectState ( const ObjectState & os )

Definition at line 110 of file Memory.cpp.

References concreteStore, knownSymbolics, readOnly, and size.

◆ ~ObjectState()

ObjectState::~ObjectState ( )

Definition at line 130 of file Memory.cpp.

References concreteMask, concreteStore, knownSymbolics, and unflushedMask.

Member Function Documentation

◆ fastRangeCheckOffset()

void ObjectState::fastRangeCheckOffset	(	ref< Expr >	offset,
		unsigned *	base_r,
		unsigned *	size_r
	)		const

private

Definition at line 254 of file Memory.cpp.

References size.

Referenced by read8(), and write8().

Here is the caller graph for this function:

◆ flushRangeForRead()

void ObjectState::flushRangeForRead	(	unsigned	rangeBase,
		unsigned	rangeSize
	)		const

private

Definition at line 261 of file Memory.cpp.

References concreteStore, klee::ConstantExpr::create(), klee::UpdateList::extend(), klee::Expr::Int32, klee::Expr::Int8, isByteConcrete(), isByteKnownSymbolic(), isByteUnflushed(), knownSymbolics, size, unflushedMask, klee::BitArray::unset(), and updates.

Referenced by read8().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ flushRangeForWrite()

void ObjectState::flushRangeForWrite	(	unsigned	rangeBase,
		unsigned	rangeSize
	)

private

Definition at line 283 of file Memory.cpp.

References concreteStore, klee::ConstantExpr::create(), klee::UpdateList::extend(), klee::Expr::Int32, klee::Expr::Int8, isByteConcrete(), isByteKnownSymbolic(), isByteUnflushed(), knownSymbolics, markByteSymbolic(), setKnownSymbolic(), size, unflushedMask, klee::BitArray::unset(), and updates.

Referenced by write8().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ flushToConcreteStore()

void ObjectState::flushToConcreteStore	(	TimingSolver *	solver,
		const ExecutionState &	state
	)		const

Definition at line 195 of file Memory.cpp.

References concreteStore, klee::ExecutionState::constraints, klee::TimingSolver::getValue(), isByteKnownSymbolic(), klee::klee_warning(), object, klee::ExecutionState::queryMetaData, read8(), and size.

Here is the call graph for this function:

◆ getArrayCache()

ArrayCache * ObjectState::getArrayCache ( ) const

private

Definition at line 137 of file Memory.cpp.

Referenced by getUpdates(), and ObjectState().

Here is the caller graph for this function:

◆ getObject()

const MemoryObject * klee::ObjectState::getObject ( ) const

inline

Definition at line 210 of file Memory.h.

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

Here is the caller graph for this function:

◆ getUpdates()

const UpdateList & ObjectState::getUpdates ( ) const

private

Definition at line 144 of file Memory.cpp.

References klee::ConstantExpr::create(), klee::ArrayCache::CreateArray(), klee::UpdateList::extend(), getArrayCache(), klee::ConstantExpr::getZExtValue(), klee::UpdateList::head, klee::Expr::Int8, klee::UpdateList::root, size, and updates.

Referenced by read8().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ initializeToRandom()

void ObjectState::initializeToRandom ( )

Make contents all concrete and random.

Definition at line 238 of file Memory.cpp.

References concreteStore, makeConcrete(), and size.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ initializeToZero()

void ObjectState::initializeToZero ( )

Make contents all concrete and zero.

Definition at line 233 of file Memory.cpp.

References concreteStore, makeConcrete(), and size.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ isByteConcrete()

bool ObjectState::isByteConcrete ( unsigned offset ) const

private

isByteConcrete ==> !isByteKnownSymbolic

Definition at line 314 of file Memory.cpp.

References concreteMask, and klee::BitArray::get().

Referenced by flushRangeForRead(), flushRangeForWrite(), print(), and read8().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ isByteKnownSymbolic()

bool ObjectState::isByteKnownSymbolic ( unsigned offset ) const

private

isByteKnownSymbolic ==> !isByteConcrete

Definition at line 322 of file Memory.cpp.

References klee::ref< T >::get(), and knownSymbolics.

Referenced by flushRangeForRead(), flushRangeForWrite(), flushToConcreteStore(), print(), and read8().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ isByteUnflushed()

bool ObjectState::isByteUnflushed ( unsigned offset ) const

private

isByteUnflushed(i) => (isByteConcrete(i) || isByteKnownSymbolic(i))

Definition at line 318 of file Memory.cpp.

References klee::BitArray::get(), and unflushedMask.

Referenced by flushRangeForRead(), flushRangeForWrite(), print(), and read8().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ makeConcrete()

void ObjectState::makeConcrete ( )

private

Definition at line 212 of file Memory.cpp.

References concreteMask, knownSymbolics, and unflushedMask.

Referenced by initializeToRandom(), and initializeToZero().

Here is the caller graph for this function:

◆ makeSymbolic()

void ObjectState::makeSymbolic ( )

private

Definition at line 221 of file Memory.cpp.

References klee::UpdateList::head, markByteFlushed(), markByteSymbolic(), setKnownSymbolic(), size, and updates.

Referenced by ObjectState().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ markByteConcrete()

void ObjectState::markByteConcrete ( unsigned offset )

private

Definition at line 326 of file Memory.cpp.

References concreteMask, and klee::BitArray::set().

Referenced by write8().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ markByteFlushed()

void ObjectState::markByteFlushed ( unsigned offset )

private

Definition at line 342 of file Memory.cpp.

References size, unflushedMask, and klee::BitArray::unset().

Referenced by makeSymbolic().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ markByteSymbolic()

void ObjectState::markByteSymbolic ( unsigned offset )

private

Definition at line 331 of file Memory.cpp.

References concreteMask, size, and klee::BitArray::unset().

Referenced by flushRangeForWrite(), makeSymbolic(), and write8().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ markByteUnflushed()

void ObjectState::markByteUnflushed ( unsigned offset )

private

Definition at line 337 of file Memory.cpp.

References klee::BitArray::set(), and unflushedMask.

Referenced by write8().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ print()

void ObjectState::print ( ) const

Definition at line 563 of file Memory.cpp.

References klee::UpdateList::head, isByteConcrete(), isByteKnownSymbolic(), isByteUnflushed(), read8(), klee::UpdateList::root, size, and updates.

Here is the call graph for this function:

◆ read() [1/2]

ref< Expr > ObjectState::read	(	ref< Expr >	offset,
		Expr::Width	width
	)		const

Definition at line 434 of file Memory.cpp.

References klee::Expr::Bool, klee::ConcatExpr::create(), klee::ExtractExpr::create(), klee::ConstantExpr::create(), klee::Context::get(), klee::Expr::Int32, klee::Context::isLittleEndian(), read(), and read8().

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ read() [2/2]

ref< Expr > ObjectState::read	(	unsigned	offset,
		Expr::Width	width
	)		const

Definition at line 461 of file Memory.cpp.

References klee::Expr::Bool, klee::ConcatExpr::create(), klee::ExtractExpr::create(), klee::Context::get(), klee::Context::isLittleEndian(), and read8().

Here is the call graph for this function:

◆ read8() [1/2]

ref< Expr > ObjectState::read8 ( ref< Expr > offset ) const

private

Definition at line 377 of file Memory.cpp.

References klee::ReadExpr::create(), fastRangeCheckOffset(), flushRangeForRead(), getUpdates(), klee::Expr::Int32, klee::klee_warning_once(), and size.

Here is the call graph for this function:

◆ read8() [2/2]

ref< Expr > ObjectState::read8 ( unsigned offset ) const

Definition at line 364 of file Memory.cpp.

References concreteStore, klee::ReadExpr::create(), klee::ConstantExpr::create(), getUpdates(), klee::Expr::Int32, klee::Expr::Int8, isByteConcrete(), isByteKnownSymbolic(), isByteUnflushed(), and knownSymbolics.

Referenced by klee::Executor::executeAlloc(), klee::Executor::executeCall(), flushToConcreteStore(), klee::ExecutionState::merge(), print(), read(), and klee::SpecialFunctionHandler::readStringAtAddress().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ setKnownSymbolic()

void ObjectState::setKnownSymbolic	(	unsigned	offset,
		Expr *	value
	)

private

Definition at line 350 of file Memory.cpp.

References knownSymbolics, and size.

Referenced by flushRangeForWrite(), makeSymbolic(), and write8().

Here is the caller graph for this function:

◆ setReadOnly()

void klee::ObjectState::setReadOnly ( bool ro )

inline

Definition at line 212 of file Memory.h.

References readOnly.

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

Here is the caller graph for this function:

◆ write() [1/2]

void ObjectState::write	(	ref< Expr >	offset,
		ref< Expr >	value
	)

Definition at line 479 of file Memory.cpp.

References klee::Expr::Bool, klee::ExtractExpr::create(), klee::ConstantExpr::create(), klee::Context::get(), klee::Expr::getWidth(), klee::Expr::Int32, klee::Expr::Int8, klee::Context::isLittleEndian(), write(), and write8().

Here is the call graph for this function:

◆ write() [2/2]

void ObjectState::write	(	unsigned	offset,
		ref< Expr >	value
	)

Definition at line 506 of file Memory.cpp.

References klee::Expr::Bool, klee::ExtractExpr::create(), klee::Context::get(), klee::Expr::getWidth(), klee::Expr::Int16, klee::Expr::Int32, klee::Expr::Int64, klee::Expr::Int8, klee::Context::isLittleEndian(), klee::bits64::isPowerOfTwo(), write16(), write32(), write64(), and write8().

Referenced by klee::Executor::doImpliedValueConcretization(), klee::Executor::executeAlloc(), klee::Executor::executeCall(), klee::Executor::executeMemoryOperation(), klee::Executor::initializeGlobalObject(), klee::ExecutionState::merge(), klee::Executor::runFunctionAsMain(), and write().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ write16()

void ObjectState::write16	(	unsigned	offset,
		uint16_t	value
	)

Definition at line 539 of file Memory.cpp.

References klee::Context::get(), klee::Context::isLittleEndian(), and write8().

Referenced by write().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ write32()

void ObjectState::write32	(	unsigned	offset,
		uint32_t	value
	)

Definition at line 547 of file Memory.cpp.

References klee::Context::get(), klee::Context::isLittleEndian(), and write8().

Referenced by write().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ write64()

void ObjectState::write64	(	unsigned	offset,
		uint64_t	value
	)

Definition at line 555 of file Memory.cpp.

References klee::Context::get(), klee::Context::isLittleEndian(), and write8().

Referenced by write().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ write8() [1/3]

void ObjectState::write8	(	ref< Expr >	offset,
		ref< Expr >	value
	)

private

Definition at line 415 of file Memory.cpp.

References klee::UpdateList::extend(), fastRangeCheckOffset(), flushRangeForWrite(), klee::Expr::Int32, klee::klee_warning_once(), size, and updates.

Here is the call graph for this function:

◆ write8() [2/3]

void ObjectState::write8	(	unsigned	offset,
		ref< Expr >	value
	)

private

Definition at line 403 of file Memory.cpp.

References klee::ref< T >::get(), markByteSymbolic(), markByteUnflushed(), setKnownSymbolic(), and write8().

Here is the call graph for this function:

◆ write8() [3/3]

void ObjectState::write8	(	unsigned	offset,
		uint8_t	value
	)

Definition at line 394 of file Memory.cpp.

References concreteStore, markByteConcrete(), markByteUnflushed(), and setKnownSymbolic().

Referenced by klee::Executor::addExternalObject(), klee::Executor::executeMakeSymbolic(), klee::Executor::initializeGlobalObject(), klee::Executor::initializeGlobalObjects(), klee::Executor::runFunctionAsMain(), klee::Executor::serializeLandingpad(), write(), write16(), write32(), write64(), and write8().

Here is the call graph for this function:

Here is the caller graph for this function:

Friends And Related Function Documentation

◆ AddressSpace

friend class AddressSpace

friend

Definition at line 165 of file Memory.h.

◆ ref< ObjectState >

friend class ref< ObjectState >

friend

Definition at line 165 of file Memory.h.

Member Data Documentation

◆ _refCount

class ReferenceCounter klee::ObjectState::_refCount

private

Required by klee::ref-managed objects.

Definition at line 171 of file Memory.h.

◆ concreteMask

BitArray* klee::ObjectState::concreteMask

private

concreteMask[byte] is set if byte is known to be concrete

Definition at line 179 of file Memory.h.

Referenced by isByteConcrete(), makeConcrete(), markByteConcrete(), markByteSymbolic(), and ~ObjectState().

◆ concreteStore

uint8_t* klee::ObjectState::concreteStore

private

Holds all known concrete bytes.

Definition at line 176 of file Memory.h.

Referenced by klee::AddressSpace::copyInConcrete(), flushRangeForRead(), flushRangeForWrite(), flushToConcreteStore(), initializeToRandom(), initializeToZero(), ObjectState(), read8(), write8(), and ~ObjectState().

◆ copyOnWriteOwner

unsigned klee::ObjectState::copyOnWriteOwner

private

Definition at line 168 of file Memory.h.

Referenced by klee::AddressSpace::bindObject(), and klee::AddressSpace::getWriteable().

◆ knownSymbolics

ref<Expr>* klee::ObjectState::knownSymbolics

private

knownSymbolics[byte] holds the symbolic expression for byte, if byte is known to be symbolic

Definition at line 183 of file Memory.h.

Referenced by flushRangeForRead(), flushRangeForWrite(), isByteKnownSymbolic(), makeConcrete(), ObjectState(), read8(), setKnownSymbolic(), and ~ObjectState().

◆ object

ref<const MemoryObject> klee::ObjectState::object

private

Definition at line 173 of file Memory.h.

Referenced by flushToConcreteStore().

◆ readOnly

bool klee::ObjectState::readOnly

Definition at line 195 of file Memory.h.

Referenced by klee::AddressSpace::copyInConcrete(), klee::Executor::doImpliedValueConcretization(), klee::Executor::executeMemoryOperation(), klee::AddressSpace::getWriteable(), klee::ExecutionState::merge(), ObjectState(), and setReadOnly().

◆ size

unsigned klee::ObjectState::size

Definition at line 193 of file Memory.h.

Referenced by klee::Executor::executeAlloc(), klee::Executor::executeCall(), fastRangeCheckOffset(), flushRangeForRead(), flushRangeForWrite(), flushToConcreteStore(), getUpdates(), initializeToRandom(), initializeToZero(), makeSymbolic(), markByteFlushed(), markByteSymbolic(), ObjectState(), print(), read8(), setKnownSymbolic(), and write8().

◆ unflushedMask

BitArray* klee::ObjectState::unflushedMask

mutableprivate

unflushedMask[byte] is set if byte is unflushed mutable because may need flushed during read of const

Definition at line 187 of file Memory.h.

Referenced by flushRangeForRead(), flushRangeForWrite(), isByteUnflushed(), makeConcrete(), markByteFlushed(), markByteUnflushed(), and ~ObjectState().

◆ updates

UpdateList klee::ObjectState::updates

mutableprivate

Definition at line 190 of file Memory.h.

Referenced by flushRangeForRead(), flushRangeForWrite(), getUpdates(), makeSymbolic(), ObjectState(), print(), and write8().

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

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

Public Member Functions

Public Attributes

Private Member Functions

Private Attributes

Friends

Detailed Description

Constructor & Destructor Documentation

◆ ObjectState() [1/3]

◆ ObjectState() [2/3]

◆ ObjectState() [3/3]

◆ ~ObjectState()

Member Function Documentation

◆ fastRangeCheckOffset()

◆ flushRangeForRead()

◆ flushRangeForWrite()

◆ flushToConcreteStore()

◆ getArrayCache()

◆ getObject()

◆ getUpdates()

◆ initializeToRandom()

◆ initializeToZero()

◆ isByteConcrete()

◆ isByteKnownSymbolic()

◆ isByteUnflushed()

◆ makeConcrete()

◆ makeSymbolic()

◆ markByteConcrete()

◆ markByteFlushed()

◆ markByteSymbolic()

◆ markByteUnflushed()

◆ print()

◆ read() [1/2]

◆ read() [2/2]

◆ read8() [1/2]

◆ read8() [2/2]

◆ setKnownSymbolic()

◆ setReadOnly()

◆ write() [1/2]

◆ write() [2/2]

◆ write16()

◆ write32()

◆ write64()

◆ write8() [1/3]

◆ write8() [2/3]

◆ write8() [3/3]

Friends And Related Function Documentation

◆ AddressSpace

◆ ref< ObjectState >

Member Data Documentation

◆ _refCount

◆ concreteMask

◆ concreteStore

◆ copyOnWriteOwner

◆ knownSymbolics

◆ object

◆ readOnly

◆ size

◆ unflushedMask

◆ updates