klee::ArrayCache Class Reference

Provides an interface for creating and destroying Array objects. More...

#include <ArrayCache.h>

Public Member Functions

 ArrayCache ()
 ~ArrayCache ()
const ArrayCreateArray (const std::string &_name, uint64_t _size, const ref< ConstantExpr > *constantValuesBegin=0, const ref< ConstantExpr > *constantValuesEnd=0, Expr::Width _domain=Expr::Int32, Expr::Width _range=Expr::Int8)
 Create an Array object. More...

Private Types

typedef std::unordered_set< const Array *, klee::ArrayHashFn, klee::EquivArrayCmpFnArrayHashMap
typedef std::vector< const Array * > ArrayPtrVec

Private Attributes

ArrayHashMap cachedSymbolicArrays
ArrayPtrVec concreteArrays

Detailed Description

Provides an interface for creating and destroying Array objects.

Definition at line 31 of file ArrayCache.h.

Member Typedef Documentation

◆ ArrayHashMap

typedef std::unordered_set<const Array *, klee::ArrayHashFn, klee::EquivArrayCmpFn> klee::ArrayCache::ArrayHashMap

Definition at line 65 of file ArrayCache.h.

◆ ArrayPtrVec

typedef std::vector<const Array *> klee::ArrayCache::ArrayPtrVec

Definition at line 67 of file ArrayCache.h.

Constructor & Destructor Documentation

◆ ArrayCache()

klee::ArrayCache::ArrayCache ( )

Definition at line 33 of file ArrayCache.h.

◆ ~ArrayCache()

klee::ArrayCache::~ArrayCache ( )

Definition at line 5 of file ArrayCache.cpp.

References cachedSymbolicArrays, and concreteArrays.

Member Function Documentation

◆ CreateArray()

const Array * klee::ArrayCache::CreateArray ( const std::string &  _name,
uint64_t  _size,
const ref< ConstantExpr > *  constantValuesBegin = 0,
const ref< ConstantExpr > *  constantValuesEnd = 0,
Expr::Width  _domain = Expr::Int32,
Expr::Width  _range = Expr::Int8 

Create an Array object.

Symbolic Arrays are cached so that only one instance exists. This provides a limited form of "alpha-renaming". Constant arrays are not cached.

This class retains ownership of Array object so that upon destruction of this object all allocated Array objects are deleted.

_nameThe name of the array
_sizeThe size of the array in bytes
constantValuesBeginA pointer to the beginning of a block of for symbolic arrays.
constantValuesEndA pointer +1 pass the end of a block of memory that contains a ref<ConstantExpr>. This should be NULL for a symbolic array.
_domainThe size of the domain (i.e. the bitvector used to index the array)
_rangeThe size of range (i.e. the bitvector that is indexed to)

Definition at line 20 of file ArrayCache.cpp.

References cachedSymbolicArrays, concreteArrays, klee::Array::isConstantArray(), and klee::Array::isSymbolicArray().

Referenced by klee::Executor::executeMakeSymbolic(), klee::ObjectState::getUpdates(), klee::ObjectState::ObjectState(), and klee::Executor::replaceReadWithSymbolic().

Here is the call graph for this function:
Here is the caller graph for this function:

Member Data Documentation

◆ cachedSymbolicArrays

ArrayHashMap klee::ArrayCache::cachedSymbolicArrays

Definition at line 66 of file ArrayCache.h.

Referenced by CreateArray(), and ~ArrayCache().

◆ concreteArrays

ArrayPtrVec klee::ArrayCache::concreteArrays

Definition at line 68 of file ArrayCache.h.

Referenced by CreateArray(), and ~ArrayCache().

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