klee
Public Member Functions | Public Attributes | Private Member Functions | Private Attributes | Friends | List of all members
klee::Array Class Reference

#include <Expr.h>

Public Member Functions

bool isSymbolicArray () const
 
bool isConstantArray () const
 
const std::string getName () const
 
unsigned getSize () const
 
Expr::Width getDomain () const
 
Expr::Width getRange () const
 
unsigned computeHash ()
 ComputeHash must take into account the name, the size, the domain, and the range. More...
 
unsigned hash () const
 

Public Attributes

const std::string name
 
const unsigned size
 
const Expr::Width domain
 
const Expr::Width range
 
const std::vector< ref< ConstantExpr > > constantValues
 

Private Member Functions

 Array (const Array &array)
 
Array & operator= (const Array &array)
 
 ~Array ()
 
 Array (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)
 

Private Attributes

unsigned hashValue
 

Friends

class ArrayCache
 

Detailed Description

Definition at line 483 of file Expr.h.

Constructor & Destructor Documentation

◆ Array() [1/2]

klee::Array::Array ( const Array &  array)
private

◆ ~Array()

Array::~Array ( )
private

Definition at line 525 of file Expr.cpp.

◆ Array() [2/2]

Array::Array ( 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 
)
private

Array - Construct a new array object.

Parameters
_name- The name for this array. Names should generally be unique across an application, but this is not necessary for correctness, except when printing expressions. When expressions are printed the output will not parse correctly since two arrays with the same name cannot be distinguished once printed.

Definition at line 507 of file Expr.cpp.

References computeHash(), constantValues, getRange(), isSymbolicArray(), and size.

Here is the call graph for this function:

Member Function Documentation

◆ computeHash()

unsigned Array::computeHash ( )

ComputeHash must take into account the name, the size, the domain, and the range.

Definition at line 528 of file Expr.cpp.

References hashValue, klee::Expr::MAGIC_HASH_CONSTANT, name, and size.

Referenced by Array().

Here is the caller graph for this function:

◆ getDomain()

Expr::Width klee::Array::getDomain ( ) const
inline

Definition at line 529 of file Expr.h.

References domain.

Referenced by klee::ExprOptimizer::computeIndexes(), FastCexSolver::computeInitialValues(), klee::ValidatingSolver::computeInitialValues(), klee::ExprEvaluator::evalRead(), klee::Assignment::evaluate(), klee::UpdateList::extend(), CexPossibleEvaluator::getInitialValue(), CexExactEvaluator::getInitialValue(), klee::ExprSMTLIBPrinter::printAction(), and klee::ExprSMTLIBPrinter::printArrayDeclarations().

Here is the caller graph for this function:

◆ getName()

const std::string klee::Array::getName ( ) const
inline

Definition at line 527 of file Expr.h.

References name.

◆ getRange()

Expr::Width klee::Array::getRange ( ) const
inline

Definition at line 530 of file Expr.h.

References range.

Referenced by Array(), klee::ValidatingSolver::computeInitialValues(), klee::Assignment::evaluate(), klee::UpdateList::extend(), CexPossibleEvaluator::getInitialValue(), CexExactEvaluator::getInitialValue(), and klee::ReadExpr::getWidth().

Here is the caller graph for this function:

◆ getSize()

unsigned klee::Array::getSize ( ) const
inline

Definition at line 528 of file Expr.h.

References size.

◆ hash()

unsigned klee::Array::hash ( ) const
inline

Definition at line 534 of file Expr.h.

References hashValue.

Referenced by klee::ArrayHashFn::operator()(), and klee::IndexTransformationExprVisitor::visitConcat().

Here is the caller graph for this function:

◆ isConstantArray()

bool klee::Array::isConstantArray ( ) const
inline

Definition at line 525 of file Expr.h.

References isSymbolicArray().

Referenced by klee::ExprOptimizer::computeIndexes(), klee::ReadExpr::create(), klee::ArrayCache::CreateArray(), klee::ExprEvaluator::evalRead(), CexRangeEvaluator::getInitialReadRange(), IndependentElementSet::IndependentElementSet(), klee::ExprSMTLIBPrinter::printArrayDeclarations(), CexData::propogateExactValues(), klee::ConstantArrayExprVisitor::visitConcat(), klee::ConstantArrayExprVisitor::visitRead(), klee::IndexCompatibilityExprVisitor::visitRead(), and klee::ConstantArrayFinder::visitRead().

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

◆ isSymbolicArray()

bool klee::Array::isSymbolicArray ( ) const
inline

Definition at line 524 of file Expr.h.

References constantValues.

Referenced by Array(), klee::ArrayCache::CreateArray(), klee::expr::ArrayDecl::dump(), klee::AssignmentGenerator::helperGenerateAssignment(), klee::ArrayReadExprVisitor::inspectRead(), isConstantArray(), TryConstArrayOpt(), klee::ConstantArrayExprVisitor::visitRead(), and klee::SymbolicObjectFinder::visitRead().

Here is the caller graph for this function:

◆ operator=()

Array & klee::Array::operator= ( const Array &  array)
private

Friends And Related Function Documentation

◆ ArrayCache

friend class ArrayCache
friend

Definition at line 535 of file Expr.h.

Member Data Documentation

◆ constantValues

const std::vector<ref<ConstantExpr> > klee::Array::constantValues

constantValues - The constant initial values for this array, or empty for a symbolic array. If non-empty, this size of this array is equivalent to the array size.

Definition at line 498 of file Expr.h.

Referenced by Array(), klee::ExprOptimizer::computeIndexes(), klee::ReadExpr::create(), klee::expr::ArrayDecl::dump(), klee::ExprEvaluator::evalRead(), CexRangeEvaluator::getInitialReadRange(), isSymbolicArray(), klee::ExprSMTLIBPrinter::printArrayDeclarations(), CexData::propogateExactValues(), and TryConstArrayOpt().

◆ domain

const Expr::Width klee::Array::domain

Domain is how many bits can be used to access the array [32 bits] Range is the size (in bits) of the number stored there (array of bytes -> 8)

Definition at line 493 of file Expr.h.

Referenced by getDomain().

◆ hashValue

unsigned klee::Array::hashValue
private

Definition at line 501 of file Expr.h.

Referenced by computeHash(), and hash().

◆ name

const std::string klee::Array::name

Definition at line 486 of file Expr.h.

Referenced by klee::UpdateList::compare(), computeHash(), QueryLoggingSolver::computeInitialValues(), klee::expr::ArrayDecl::dump(), getName(), klee::UpdateList::hash(), klee::EquivArrayCmpFn::operator()(), IndependentElementSet::print(), klee::ExprSMTLIBPrinter::printArrayDeclarations(), PPrinter::printUpdateList(), and klee::ExprSMTLIBPrinter::printUpdatesAndArray().

◆ range

const Expr::Width klee::Array::range

Definition at line 493 of file Expr.h.

Referenced by klee::ExprOptimizer::computeIndexes(), klee::ExprRangeEvaluator< T >::evaluate(), and getRange().

◆ size

const unsigned klee::Array::size

Definition at line 489 of file Expr.h.

Referenced by Array(), klee::ImpliedValue::checkForImpliedValues(), computeHash(), CexCachingSolver::computeInitialValues(), FastCexSolver::computeInitialValues(), klee::ValidatingSolver::computeInitialValues(), IndependentSolver::computeInitialValues(), QueryLoggingSolver::computeInitialValues(), klee::ReadExpr::create(), klee::expr::ArrayDecl::dump(), CexRangeEvaluator::getInitialReadRange(), CexPossibleEvaluator::getInitialValue(), CexExactEvaluator::getInitialValue(), getSize(), klee::AssignmentGenerator::helperGenerateAssignment(), klee::EquivArrayCmpFn::operator()(), klee::SeedInfo::patchSeed(), klee::ExprSMTLIBPrinter::printAction(), KQueryLoggingSolver::printQuery(), klee::ExprRewriter::rewrite(), and TryConstArrayOpt().

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