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

#include <Memory.h>

Collaboration diagram for klee::ObjectState:

Public Member Functions

 ObjectState (const MemoryObject *mo)
 
 ObjectState (const MemoryObject *mo, const Array *array)
 
 ObjectState (const ObjectState &os)
 
 ~ObjectState ()
 
const MemoryObjectgetObject () const
 
void setReadOnly (bool ro)
 
void initializeToZero ()
 
void initializeToRandom ()
 
ref< Exprread (ref< Expr > offset, Expr::Width width) const
 
ref< Exprread (unsigned offset, Expr::Width width) const
 
ref< Exprread8 (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)
 

Public Attributes

unsigned size
 
bool readOnly
 

Private Member Functions

const UpdateListgetUpdates () const
 
void makeConcrete ()
 
void makeSymbolic ()
 
ref< Exprread8 (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
 
bool isByteFlushed (unsigned offset) const
 
bool isByteKnownSymbolic (unsigned offset) const
 
void markByteConcrete (unsigned offset)
 
void markByteSymbolic (unsigned offset)
 
void markByteFlushed (unsigned offset)
 
void markByteUnflushed (unsigned offset)
 
void setKnownSymbolic (unsigned offset, Expr *value)
 
void print ()
 

Private Attributes

unsigned copyOnWriteOwner
 
unsigned refCount
 
const MemoryObjectobject
 
uint8_t * concreteStore
 
BitArrayconcreteMask
 
BitArrayflushMask
 
ref< Expr > * knownSymbolics
 
UpdateList updates
 

Friends

class AddressSpace
 
class ObjectHolder
 

Detailed Description

Definition at line 148 of file Memory.h.

Constructor & Destructor Documentation

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 101 of file Memory.cpp.

References concreteStore, klee::MemoryObject::refCount, size, and updates.

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

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

Definition at line 123 of file Memory.cpp.

References concreteStore, makeSymbolic(), klee::MemoryObject::refCount, and size.

Here is the call graph for this function:

ObjectState::ObjectState ( const ObjectState os)

Definition at line 139 of file Memory.cpp.

References concreteStore, knownSymbolics, readOnly, and size.

ObjectState::~ObjectState ( )

Member Function Documentation

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

Definition at line 280 of file Memory.cpp.

References size.

Referenced by read8(), and write8().

Here is the caller graph for this function:

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

Definition at line 287 of file Memory.cpp.

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

Referenced by read8().

Here is the call graph for this function:

Here is the caller graph for this function:

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

Definition at line 307 of file Memory.cpp.

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

Referenced by write8().

Here is the call graph for this function:

Here is the caller graph for this function:

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

Definition at line 188 of file Memory.h.

References object.

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

Here is the caller graph for this function:

const UpdateList & ObjectState::getUpdates ( ) const
private

Definition at line 182 of file Memory.cpp.

References klee::ConstantExpr::create(), klee::UpdateNode::getSize(), klee::ConstantExpr::getZExtValue(), klee::UpdateList::head, klee::UpdateNode::index, klee::Expr::Int8, klee::UpdateNode::next, klee::UpdateList::root, size, updates, and klee::UpdateNode::value.

Referenced by read8().

Here is the call graph for this function:

Here is the caller graph for this function:

void ObjectState::initializeToRandom ( )

Definition at line 264 of file Memory.cpp.

References concreteStore, makeConcrete(), and size.

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

Here is the call graph for this function:

Here is the caller graph for this function:

void ObjectState::initializeToZero ( )

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

bool ObjectState::isByteConcrete ( unsigned  offset) const
private

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

bool ObjectState::isByteFlushed ( unsigned  offset) const
private

Definition at line 341 of file Memory.cpp.

References flushMask, 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:

bool ObjectState::isByteKnownSymbolic ( unsigned  offset) const
private

Definition at line 345 of file Memory.cpp.

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

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

Here is the call graph for this function:

Here is the caller graph for this function:

void ObjectState::makeConcrete ( )
private

Definition at line 238 of file Memory.cpp.

References concreteMask, flushMask, and knownSymbolics.

Referenced by initializeToRandom(), and initializeToZero().

Here is the caller graph for this function:

void ObjectState::makeSymbolic ( )
private

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

void ObjectState::markByteConcrete ( unsigned  offset)
private

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

void ObjectState::markByteFlushed ( unsigned  offset)
private

Definition at line 365 of file Memory.cpp.

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

Referenced by makeSymbolic().

Here is the call graph for this function:

Here is the caller graph for this function:

void ObjectState::markByteSymbolic ( unsigned  offset)
private

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

void ObjectState::markByteUnflushed ( unsigned  offset)
private

Definition at line 360 of file Memory.cpp.

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

Referenced by write8().

Here is the call graph for this function:

Here is the caller graph for this function:

void ObjectState::print ( )
private

Definition at line 586 of file Memory.cpp.

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

Here is the call graph for this function:

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

Definition at line 457 of file Memory.cpp.

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

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

Here is the call graph for this function:

Here is the caller graph for this function:

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

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

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

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

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

Definition at line 373 of file Memory.cpp.

References knownSymbolics, and size.

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

Here is the caller graph for this function:

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

Definition at line 190 of file Memory.h.

References readOnly.

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

Here is the caller graph for this function:

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

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

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

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

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

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

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

Definition at line 426 of file Memory.cpp.

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

Here is the call graph for this function:

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

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

Friends And Related Function Documentation

friend class AddressSpace
friend

Definition at line 150 of file Memory.h.

friend class ObjectHolder
friend

Definition at line 153 of file Memory.h.

Member Data Documentation

BitArray* klee::ObjectState::concreteMask
private
unsigned klee::ObjectState::copyOnWriteOwner
private

Definition at line 151 of file Memory.h.

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

BitArray* klee::ObjectState::flushMask
mutableprivate
ref<Expr>* klee::ObjectState::knownSymbolics
private
const MemoryObject* klee::ObjectState::object
private

Definition at line 156 of file Memory.h.

Referenced by getObject(), and ~ObjectState().

unsigned klee::ObjectState::refCount
private
UpdateList klee::ObjectState::updates
mutableprivate

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