klee::Expr Class Reference

Class representing symbolic expressions. More...

#include <Expr.h>

Inheritance diagram for klee::Expr:

Collaboration diagram for klee::Expr:

Classes
struct	CreateArg

Public Types
enum	Kind {   InvalidKind = -1 , Constant = 0 , NotOptimized , Read =NotOptimized+2 ,   Select , Concat , Extract , ZExt ,   SExt , Not , Add , Sub ,   Mul , UDiv , SDiv , URem ,   SRem , And , Or , Xor ,   Shl , LShr , AShr , Eq ,   Ne , Ult , Ule , Ugt ,   Uge , Slt , Sle , Sgt ,   Sge , LastKind =Sge , CastKindFirst =ZExt , CastKindLast =SExt ,   BinaryKindFirst =Add , BinaryKindLast =Sge , CmpKindFirst =Eq , CmpKindLast =Sge }
typedef unsigned	Width
	The type of an expression is simply its width, in bits. More...

Public Member Functions
	Expr ()
virtual	~Expr ()
virtual Kind	getKind () const =0
virtual Width	getWidth () const =0
virtual unsigned	getNumKids () const =0
virtual ref< Expr >	getKid (unsigned i) const =0
virtual void	print (llvm::raw_ostream &os) const
void	dump () const
	dump - Print the expression to stderr. More...
virtual unsigned	hash () const
	Returns the pre-computed hash of the current expression. More...
virtual unsigned	computeHash ()
int	compare (const Expr &b) const
virtual ref< Expr >	rebuild (ref< Expr > kids[]) const =0
bool	isZero () const
	isZero - Is this a constant zero. More...
bool	isTrue () const
	isTrue - Is this the true expression. More...
bool	isFalse () const
	isFalse - Is this the false expression. More...

Static Public Member Functions
static void	printKind (llvm::raw_ostream &os, Kind k)
static void	printWidth (llvm::raw_ostream &os, Expr::Width w)
static unsigned	getMinBytesForWidth (Width w)
	returns the smallest number of bytes in which the given width fits More...
static ref< Expr >	createSExtToPointerWidth (ref< Expr > e)
static ref< Expr >	createZExtToPointerWidth (ref< Expr > e)
static ref< Expr >	createImplies (ref< Expr > hyp, ref< Expr > conc)
static ref< Expr >	createIsZero (ref< Expr > e)
static ref< Expr >	createTempRead (const Array *array, Expr::Width w)
static ref< ConstantExpr >	createPointer (uint64_t v)
static ref< Expr >	createFromKind (Kind k, std::vector< CreateArg > args)
static bool	isValidKidWidth (unsigned kid, Width w)
static bool	needsResultType ()
static bool	classof (const Expr *)

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

Static Public Attributes
static unsigned	count = 0
static const unsigned	MAGIC_HASH_CONSTANT = 39
static const Width	InvalidWidth = 0
static const Width	Bool = 1
static const Width	Int8 = 8
static const Width	Int16 = 16
static const Width	Int32 = 32
static const Width	Int64 = 64
static const Width	Fl80 = 80

Protected Member Functions
virtual int	compareContents (const Expr &b) const =0

Protected Attributes
unsigned	hashValue

Private Types
typedef llvm::DenseSet< std::pair< const Expr *, const Expr * > >	ExprEquivSet

Private Member Functions
int	compare (const Expr &b, ExprEquivSet &equivs) const

Detailed Description

Class representing symbolic expressions.

Expression canonicalization: we define certain rules for canonicalization rules for Exprs in order to simplify code that pattern matches Exprs (since the number of forms are reduced), to open up further chances for optimization, and to increase similarity for caching and other purposes.

The general rules are:

1. No Expr has all constant arguments.

2. Booleans:

   1. Ne, Ugt, Uge, Sgt, Sge are not used
   2. The only acceptable operations with boolean arguments are Not And, Or, Xor, Eq, as well as SExt, ZExt, Select and NotOptimized.
   3. The only boolean operation which may involve a constant is boolean not (== false).

3. Linear Formulas:

   1. For any subtree representing a linear formula, a constant term must be on the LHS of the root node of the subtree. In particular, in a BinaryExpr a constant must always be on the LHS. For example, subtraction by a constant c is written as add(-c, ?).

4. Chains are unbalanced to the right

Steps required for adding an expr:

1. Add case to printKind
2. Add to ExprVisitor
3. Add to IVC (implied value concretization) if possible

Todo: Shouldn't bool Xor just be written as not equal?

Definition at line 91 of file Expr.h.

Member Typedef Documentation

ExprEquivSet

typedef llvm::DenseSet<std::pair<const Expr *, const Expr *> > klee::Expr::ExprEquivSet

private

Definition at line 289 of file Expr.h.

Width

typedef unsigned klee::Expr::Width

The type of an expression is simply its width, in bits.

Definition at line 97 of file Expr.h.

Member Enumeration Documentation

Kind

enum klee::Expr::Kind

Enumerator
InvalidKind
Constant
NotOptimized	Prevents optimization below the given expression. Used for testing: make equality constraints that KLEE will not use to optimize to concretes.
Read
Select
Concat
Extract
ZExt
SExt
Not
Add
Sub
Mul
UDiv
SDiv
URem
SRem
And
Or
Xor
Shl
LShr
AShr
Eq
Ne	Not used in canonical form.
Ult
Ule
Ugt	Not used in canonical form.
Uge	Not used in canonical form.
Slt
Sle
Sgt	Not used in canonical form.
Sge	Not used in canonical form.
LastKind
CastKindFirst
CastKindLast
BinaryKindFirst
BinaryKindLast
CmpKindFirst
CmpKindLast

Definition at line 108 of file Expr.h.

Constructor & Destructor Documentation

Expr()

klee::Expr::Expr ( )

inline

Definition at line 207 of file Expr.h.

References count.

~Expr()

virtual klee::Expr::~Expr ( )

inlinevirtual

Definition at line 208 of file Expr.h.

References count.

Member Function Documentation

classof()

static bool klee::Expr::classof ( const Expr *  )

inlinestatic

Definition at line 286 of file Expr.h.

compare() [1/2]

int Expr::compare

(

const Expr &

b

)

const

Compares b to this Expr for structural equivalence.

This method effectively defines a total order over all Expr.

Parameters

[in]

b

Expr to compare this to.

Returns

One of the following values:

• -1 iff this is < b
• 0 iff this is structurally equivalent to b
• 1 iff this is > b

< and > are binary relations that express the total order.

Definition at line 95 of file Expr.cpp.

References compare().

Referenced by compare(), klee::operator<(), and klee::operator==().

Here is the call graph for this function:

Here is the caller graph for this function:

compare() [2/2]

int Expr::compare ( const Expr &  b, ExprEquivSet &  equivs  ) const

private

Definition at line 103 of file Expr.cpp.

References compare(), compareContents(), getKid(), getKind(), getNumKids(), and hashValue.

Here is the call graph for this function:

compareContents()

virtual int klee::Expr::compareContents ( const Expr &  b ) const

protectedpure virtual

Compares b to this Expr and determines how they are ordered (ignoring their kid expressions - i.e. those returned by getKid()).

Typically this requires comparing internal attributes of the Expr.

Implementations can assume that b and this are of the same kind.

This method effectively defines a partial order over Expr of the same kind (partial because kid Expr are not compared).

This method should not be called directly. Instead compare() should be used.

Parameters

[in]

b

Expr to compare this to.

Returns

One of the following values:

• -1 if this is < b ignoring kid expressions.
• 1 if this is > b ignoring kid expressions.
• 0 if this and b are not ordered.

< and > are binary relations that express the partial order.

Implemented in klee::NotOptimizedExpr, klee::ReadExpr, klee::SelectExpr, klee::ConcatExpr, klee::ExtractExpr, klee::NotExpr, klee::CastExpr, and klee::ConstantExpr.

Referenced by compare().

Here is the caller graph for this function:

computeHash()

unsigned Expr::computeHash ( )

virtual

(Re)computes the hash of the current expression. Returns the hash value.

Reimplemented in klee::ReadExpr, klee::ExtractExpr, klee::NotExpr, klee::CastExpr, and klee::ConstantExpr.

Definition at line 182 of file Expr.cpp.

References getKid(), getKind(), getNumKids(), hash(), hashValue, and MAGIC_HASH_CONSTANT.

Referenced by klee::SelectExpr::alloc(), klee::NotExpr::alloc(), klee::ExtractExpr::alloc(), klee::ConcatExpr::alloc(), klee::NotOptimizedExpr::alloc(), and klee::ReadExpr::alloc().

Here is the call graph for this function:

Here is the caller graph for this function:

createFromKind()

ref< Expr > Expr::createFromKind ( Kind  k, std::vector< CreateArg >  args  )

static

Definition at line 230 of file Expr.cpp.

References Add, And, AShr, BINARY_EXPR_CASE, CAST_EXPR_CASE, Concat, Constant, klee::ConcatExpr::create(), klee::SelectExpr::create(), klee::NotOptimizedExpr::create(), Eq, Extract, LShr, Mul, Ne, NotOptimized, Or, Read, SDiv, Select, SExt, Sge, Sgt, Shl, Sle, Slt, SRem, Sub, UDiv, Uge, Ugt, Ule, Ult, URem, Xor, and ZExt.

Here is the call graph for this function:

createImplies()

ref< Expr > Expr::createImplies ( ref< Expr >  hyp, ref< Expr >  conc  )

static

Definition at line 318 of file Expr.cpp.

References createIsZero().

Here is the call graph for this function:

createIsZero()

ref< Expr > Expr::createIsZero ( ref< Expr >  e )

static

Definition at line 322 of file Expr.cpp.

References klee::ConstantExpr::create(), and getWidth().

Referenced by klee::ValidatingSolver::computeInitialValues(), klee::SelectExpr::create(), createImplies(), EqExpr_createPartialR(), klee::Executor::executeFree(), klee::Executor::executeInstruction(), klee::Executor::fork(), klee::Executor::getSymbolicSolution(), LShrExpr_create(), klee::TimingSolver::mustBeFalse(), klee::Query::negateExpr(), klee::ExprSMTLIBPrinter::printHumanReadableQuery(), klee::ExprSMTLIBPrinter::printQueryInSingleAssert(), ShlExpr_create(), SleExpr_create(), SltExpr_create(), UleExpr_create(), and UltExpr_create().

Here is the call graph for this function:

Here is the caller graph for this function:

createPointer()

ref< ConstantExpr > Expr::createPointer ( uint64_t  v )

static

Definition at line 46 of file Context.cpp.

References klee::ConstantExpr::create(), and klee::Context::get().

Referenced by klee::Executor::allocateGlobalObjects(), klee::Executor::evalConstant(), klee::Executor::executeFree(), klee::Executor::executeInstruction(), and klee::Executor::runFunctionAsMain().

Here is the call graph for this function:

Here is the caller graph for this function:

createSExtToPointerWidth()

ref< Expr > Expr::createSExtToPointerWidth ( ref< Expr >  e )

static

Definition at line 38 of file Context.cpp.

References klee::Context::get().

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

Here is the call graph for this function:

Here is the caller graph for this function:

createTempRead()

ref< Expr > Expr::createTempRead ( const Array *  array, Expr::Width  w  )

static

Create a little endian read of the given type at offset 0 of the given object.

Definition at line 49 of file Expr.cpp.

References klee::ConstantExpr::alloc(), Bool, klee::ConcatExpr::create(), klee::ReadExpr::create(), klee::ConcatExpr::create4(), klee::ConcatExpr::create8(), Int16, Int32, Int64, and Int8.

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

Here is the call graph for this function:

Here is the caller graph for this function:

createZExtToPointerWidth()

ref< Expr > Expr::createZExtToPointerWidth ( ref< Expr >  e )

static

Definition at line 42 of file Context.cpp.

References klee::Context::get().

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

Here is the call graph for this function:

Here is the caller graph for this function:

dump()

void Expr::dump

(

)

const

dump - Print the expression to stderr.

Definition at line 330 of file Expr.cpp.

References print().

Referenced by klee::Query::dump().

Here is the call graph for this function:

Here is the caller graph for this function:

getKid()

virtual ref< Expr > klee::Expr::getKid ( unsigned  i ) const

pure virtual

Implemented in klee::BinaryExpr, klee::NotOptimizedExpr, klee::ReadExpr, klee::SelectExpr, klee::ConcatExpr, klee::ExtractExpr, klee::NotExpr, klee::CastExpr, and klee::ConstantExpr.

Referenced by AddExpr_create(), AddExpr_createPartialR(), compare(), computeHash(), klee::ExprRangeEvaluator< T >::evaluate(), klee::findReads(), klee::ExprSMTLIBPrinter::getSort(), klee::ArrayExprHelper::hasOrderedReads(), klee::AssignmentGenerator::hasOrderedReads(), PPrinter::hasOrderedReads(), PPrinter::hasSimpleKids(), klee::AssignmentGenerator::helperGenerateAssignment(), PPrinter::isSimple(), PPrinter::printExpr(), klee::ExprSMTLIBPrinter::printFullExpression(), klee::ExprSMTLIBPrinter::printLogicalOrBitVectorExpr(), klee::ExprSMTLIBPrinter::printSortArgsExpr(), CexData::propogateExactValues(), CexData::propogatePossibleValues(), klee::ExprSMTLIBPrinter::scan(), PPrinter::scan1(), klee::ExprSMTLIBPrinter::scanBindingExprDeps(), SubExpr_create(), SubExpr_createPartialR(), klee::ExprVisitor::visitActual(), and klee::ExprEvaluator::visitExpr().

Here is the caller graph for this function:

getKind()

virtual Kind klee::Expr::getKind ( ) const

pure virtual

Implemented in klee::NotOptimizedExpr, klee::ReadExpr, klee::SelectExpr, klee::ConcatExpr, klee::ExtractExpr, klee::NotExpr, and klee::ConstantExpr.

Referenced by klee::ConstraintManager::addConstraintInternal(), AddExpr_create(), AddExpr_createPartialR(), klee::NonConstantExpr::classof(), klee::BinaryExpr::classof(), klee::CmpExpr::classof(), klee::NotOptimizedExpr::classof(), klee::ReadExpr::classof(), klee::SelectExpr::classof(), klee::ConcatExpr::classof(), klee::ExtractExpr::classof(), klee::NotExpr::classof(), klee::CastExpr::classof(), klee::ConstantExpr::classof(), compare(), computeHash(), klee::AssignmentGenerator::createExtendExpr(), EqExpr_createPartialR(), klee::ExprRangeEvaluator< T >::evaluate(), klee::ImpliedValue::getImpliedValues(), klee::ExprSMTLIBPrinter::getSMTLIBKeyword(), klee::ExprSMTLIBPrinter::getSort(), klee::ArrayExprHelper::hasOrderedReads(), klee::AssignmentGenerator::hasOrderedReads(), PPrinter::hasOrderedReads(), klee::AssignmentGenerator::helperGenerateAssignment(), PPrinter::print(), klee::ExprSMTLIBPrinter::printFullExpression(), klee::ExprSMTLIBPrinter::printLogicalOrBitVectorExpr(), CexData::propogateExactValues(), CexData::propogatePossibleValues(), SubExpr_create(), SubExpr_createPartialR(), klee::ExprVisitor::visitActual(), and klee::ExprEvaluator::visitExprPost().

Here is the caller graph for this function:

getMinBytesForWidth()

static unsigned klee::Expr::getMinBytesForWidth ( Width  w )

inlinestatic

returns the smallest number of bytes in which the given width fits

Definition at line 262 of file Expr.h.

Referenced by klee::Executor::executeCall(), klee::Executor::executeMemoryOperation(), and klee::Executor::replaceReadWithSymbolic().

Here is the caller graph for this function:

getNumKids()

virtual unsigned klee::Expr::getNumKids ( ) const

pure virtual

Implemented in klee::BinaryExpr, klee::NotOptimizedExpr, klee::ReadExpr, klee::SelectExpr, klee::ConcatExpr, klee::ExtractExpr, klee::NotExpr, klee::CastExpr, and klee::ConstantExpr.

Referenced by compare(), computeHash(), klee::ExprRangeEvaluator< T >::evaluate(), klee::findReads(), PPrinter::hasSimpleKids(), PPrinter::isSimple(), PPrinter::printExpr(), klee::ExprSMTLIBPrinter::printLogicalOrBitVectorExpr(), klee::ExprSMTLIBPrinter::printSortArgsExpr(), klee::ExprSMTLIBPrinter::scan(), PPrinter::scan1(), klee::ExprSMTLIBPrinter::scanBindingExprDeps(), klee::ExprVisitor::visitActual(), and klee::ExprEvaluator::visitExpr().

Here is the caller graph for this function:

getWidth()

virtual Width klee::Expr::getWidth ( ) const

pure virtual

Implemented in klee::CmpExpr, klee::NotOptimizedExpr, klee::ReadExpr, klee::SelectExpr, klee::ConcatExpr, klee::ExtractExpr, klee::NotExpr, klee::CastExpr, and klee::ConstantExpr.

Referenced by AddExpr_create(), AShrExpr_create(), klee::ExprOptimizer::buildConstantSelectExpr(), klee::ExprOptimizer::buildMixedSelectExpr(), klee::ConcatExpr::ConcatExpr(), klee::ConcatExpr::create(), klee::SelectExpr::create(), klee::ExtractExpr::create(), klee::AssignmentGenerator::createExtendExpr(), klee::AssignmentGenerator::createExtractExpr(), createIsZero(), klee::Executor::evalConstant(), klee::Solver::evaluate(), klee::ExprRangeEvaluator< T >::evaluate(), klee::Executor::executeCall(), klee::Executor::executeInstruction(), klee::Executor::executeMemoryOperation(), klee::UpdateList::extend(), klee::AssignmentGenerator::generatePartialAssignment(), klee::ImpliedValue::getImpliedValues(), klee::Solver::getRange(), klee::ExprSMTLIBPrinter::getSort(), klee::NotOptimizedExpr::getWidth(), klee::SelectExpr::getWidth(), klee::NotExpr::getWidth(), klee::ArrayExprHelper::hasOrderedReads(), klee::AssignmentGenerator::hasOrderedReads(), PPrinter::hasOrderedReads(), klee::AssignmentGenerator::helperGenerateAssignment(), isFalse(), isTrue(), LShrExpr_create(), MulExpr_create(), klee::Solver::mustBeTrue(), klee::ExprSMTLIBPrinter::printCastToSort(), PPrinter::printWidth(), CexData::propogateExactValues(), CexData::propogatePossibleValues(), klee::Executor::replaceReadWithSymbolic(), SDivExpr_create(), ShlExpr_create(), PPrinter::shouldPrintWidth(), SleExpr_create(), SltExpr_create(), SRemExpr_create(), SubExpr_create(), TryConstArrayOpt(), UDivExpr_create(), UleExpr_create(), UltExpr_create(), URemExpr_create(), and klee::ObjectState::write().

hash()

virtual unsigned klee::Expr::hash ( ) const

inlinevirtual

Returns the pre-computed hash of the current expression.

Definition at line 222 of file Expr.h.

References hashValue.

Referenced by computeHash(), klee::UpdateNode::computeHash(), klee::ReadExpr::computeHash(), klee::ExtractExpr::computeHash(), klee::NotExpr::computeHash(), klee::CastExpr::computeHash(), CachingSolver::CacheEntryHash::operator()(), klee::util::ExprHash::operator()(), klee::ConstantArrayExprVisitor::visitConcat(), and klee::ConstantArrayExprVisitor::visitRead().

Here is the caller graph for this function:

isFalse()

bool klee::Expr::isFalse ( ) const

inline

isFalse - Is this the false expression.

Definition at line 1163 of file Expr.h.

References Bool, and getWidth().

Referenced by klee::ExprPPrinter::printQuery(), and propogateValues().

Here is the call graph for this function:

Here is the caller graph for this function:

isTrue()

bool klee::Expr::isTrue ( ) const

inline

isTrue - Is this the true expression.

Definition at line 1156 of file Expr.h.

References Bool, and getWidth().

Referenced by klee::ExprOptimizer::computeIndexes(), klee::Executor::executeCall(), propogateValues(), and klee::Assignment::satisfies().

Here is the call graph for this function:

Here is the caller graph for this function:

isValidKidWidth()

static bool klee::Expr::isValidKidWidth ( unsigned  kid, Width  w  )

inlinestatic

Definition at line 283 of file Expr.h.

isZero()

bool klee::Expr::isZero ( ) const

inline

isZero - Is this a constant zero.

Definition at line 1150 of file Expr.h.

Referenced by klee::Executor::executeInstruction(), and klee::AssignmentGenerator::helperGenerateAssignment().

Here is the caller graph for this function:

needsResultType()

static bool klee::Expr::needsResultType ( )

inlinestatic

Definition at line 284 of file Expr.h.

print()

void Expr::print ( llvm::raw_ostream &  os ) const

virtual

Definition at line 326 of file Expr.cpp.

References klee::ExprPPrinter::printSingleExpr().

Referenced by dump(), and klee::operator<<().

Here is the call graph for this function:

Here is the caller graph for this function:

printKind()

void Expr::printKind ( llvm::raw_ostream &  os, Kind  k  )

static

Definition at line 135 of file Expr.cpp.

References Add, And, AShr, Concat, Constant, Eq, Extract, LShr, Mul, Ne, Not, NotOptimized, Or, Read, SDiv, Select, SExt, Sge, Sgt, Shl, Sle, Slt, SRem, Sub, UDiv, Uge, Ugt, Ule, Ult, URem, X, Xor, and ZExt.

Referenced by klee::AssignmentGenerator::helperGenerateAssignment(), and klee::operator<<().

Here is the caller graph for this function:

printWidth()

void Expr::printWidth ( llvm::raw_ostream &  os, Expr::Width  w  )

static

Definition at line 306 of file Expr.cpp.

References Bool, Fl80, Int16, Int32, Int64, and Int8.

rebuild()

virtual ref< Expr > klee::Expr::rebuild ( ref< Expr >  kids[] ) const

pure virtual

Implemented in klee::NotOptimizedExpr, klee::ReadExpr, klee::SelectExpr, klee::ConcatExpr, klee::ExtractExpr, klee::NotExpr, and klee::ConstantExpr.

Referenced by klee::ExprEvaluator::protectedDivOperation(), klee::ExprVisitor::visitActual(), and klee::ExprEvaluator::visitExpr().

Here is the caller graph for this function:

Member Data Documentation

_refCount

class ReferenceCounter klee::Expr::_refCount

Required by klee::ref-managed objects.

Definition at line 177 of file Expr.h.

Bool

const Width klee::Expr::Bool = 1

static

Definition at line 100 of file Expr.h.

Referenced by klee::Executor::addConstraint(), AddExpr_create(), AddExpr_createPartialR(), AShrExpr_create(), klee::SelectExpr::create(), createTempRead(), klee::ConstantExpr::Eq(), EqExpr_create(), EqExpr_createPartialR(), klee::Solver::evaluate(), klee::Executor::executeInstruction(), klee::ExprBuilder::False(), klee::ConstantExpr::fromMemory(), klee::MemoryObject::getBoundsCheckOffset(), klee::Executor::getConstraintLog(), klee::TimingSolver::getInitialValues(), klee::ExprSMTLIBPrinter::getSort(), klee::Executor::getSymbolicSolution(), klee::CmpExpr::getWidth(), isFalse(), klee::ConstantExpr::isFalse(), isTrue(), klee::ConstantExpr::isTrue(), klee::SelectExpr::isValidKidWidth(), LShrExpr_create(), klee::ExecutionState::merge(), MulExpr_create(), MulExpr_createPartialR(), klee::Solver::mustBeTrue(), klee::ConstantExpr::Ne(), klee::ExprOptimizer::optimizeExpr(), klee::ExprSMTLIBPrinter::printCastToSort(), klee::ExprPPrinter::printConstraints(), printWidth(), klee::ObjectState::read(), SDivExpr_create(), klee::ConstantExpr::Sge(), klee::ConstantExpr::Sgt(), ShlExpr_create(), klee::ConstraintManager::simplifyExpr(), klee::ConstantExpr::Sle(), SleExpr_create(), klee::ConstantExpr::Slt(), SltExpr_create(), SRemExpr_create(), SubExpr_create(), SubExpr_createPartialR(), klee::ConstantExpr::toMemory(), klee::ExprBuilder::True(), TryConstArrayOpt(), UDivExpr_create(), klee::ConstantExpr::Uge(), klee::ConstantExpr::Ugt(), klee::ConstantExpr::Ule(), UleExpr_create(), klee::ConstantExpr::Ult(), UltExpr_create(), URemExpr_create(), klee::Query::withFalse(), klee::ObjectState::write(), and XorExpr_createPartialR().

count

unsigned Expr::count = 0

static

Definition at line 93 of file Expr.h.

Referenced by Expr(), and ~Expr().

Fl80

const Width klee::Expr::Fl80 = 80

static

Definition at line 105 of file Expr.h.

Referenced by klee::Executor::callExternalFunction(), fpWidthToSemantics(), printWidth(), and klee::ConstantExpr::toMemory().

hashValue

unsigned klee::Expr::hashValue

protected

Definition at line 180 of file Expr.h.

Referenced by compare(), computeHash(), klee::ReadExpr::computeHash(), klee::ExtractExpr::computeHash(), klee::NotExpr::computeHash(), klee::CastExpr::computeHash(), klee::ConstantExpr::computeHash(), and hash().

Int16

const Width klee::Expr::Int16 = 16

static

Definition at line 102 of file Expr.h.

Referenced by createTempRead(), klee::ConstantExpr::fromMemory(), printWidth(), klee::ConstantExpr::toMemory(), and klee::ObjectState::write().

Int32

const Width klee::Expr::Int32 = 32

static

Definition at line 103 of file Expr.h.

Referenced by klee::ExprOptimizer::buildConstantSelectExpr(), klee::ExprRewriter::concatenateOrExpr(), createTempRead(), klee::Executor::executeCall(), klee::Executor::executeInstruction(), klee::ObjectState::flushRangeForRead(), klee::ObjectState::flushRangeForWrite(), fpWidthToSemantics(), klee::ConstantExpr::fromMemory(), klee::Executor::getEhTypeidFor(), klee::SeedInfo::patchSeed(), printWidth(), klee::ObjectState::read(), klee::ObjectState::read8(), klee::Executor::runFunctionAsMain(), klee::ConstantExpr::toMemory(), klee::ObjectState::write(), and klee::ObjectState::write8().

Int64

const Width klee::Expr::Int64 = 64

static

Definition at line 104 of file Expr.h.

Referenced by klee::Executor::callExternalFunction(), createTempRead(), klee::Executor::executeCall(), klee::Executor::executeInstruction(), fpWidthToSemantics(), klee::ConstantExpr::fromMemory(), printWidth(), klee::ConstantExpr::toMemory(), and klee::ObjectState::write().

Int8

const Width klee::Expr::Int8 = 8

static

Definition at line 101 of file Expr.h.

Referenced by createTempRead(), klee::ObjectState::flushRangeForRead(), klee::ObjectState::flushRangeForWrite(), klee::ConstantExpr::fromMemory(), klee::AssignmentGenerator::getByteValue(), klee::ExprOptimizer::getSelectOptExpr(), klee::ObjectState::getUpdates(), klee::IndexTransformationExprVisitor::getWidth(), klee::ArrayExprHelper::hasOrderedReads(), klee::AssignmentGenerator::hasOrderedReads(), klee::ArrayExprHelper::isReadExprAtOffset(), klee::AssignmentGenerator::isReadExprAtOffset(), klee::SeedInfo::patchSeed(), printWidth(), klee::ObjectState::read8(), klee::ConstantExpr::toMemory(), and klee::ObjectState::write().

InvalidWidth

const Width klee::Expr::InvalidWidth = 0

static

Definition at line 99 of file Expr.h.

Referenced by klee::IndexTransformationExprVisitor::getWidth(), klee::Expr::CreateArg::isWidth(), and klee::IndexTransformationExprVisitor::visitConcat().

MAGIC_HASH_CONSTANT

const unsigned klee::Expr::MAGIC_HASH_CONSTANT = 39

static

Definition at line 94 of file Expr.h.

Referenced by computeHash(), klee::Array::computeHash(), klee::ReadExpr::computeHash(), klee::ExtractExpr::computeHash(), klee::NotExpr::computeHash(), klee::CastExpr::computeHash(), klee::ConstantExpr::computeHash(), and klee::UpdateList::hash().

---

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

• /Users/cristic/klee/include/klee/Expr/Expr.h
• /Users/cristic/klee/lib/Core/Context.cpp
• /Users/cristic/klee/lib/Expr/Expr.cpp