#include <Expr.h>

Inheritance diagram for klee::ConstantExpr:

Collaboration diagram for klee::ConstantExpr:

Public Member Functions
	~ConstantExpr ()

Width	getWidth () const

Kind	getKind () const

unsigned	getNumKids () const

ref< Expr >	getKid (unsigned i) const

const llvm::APInt &	getAPValue () const

uint64_t	getZExtValue (unsigned bits=64) const

uint64_t	getLimitedValue (uint64_t Limit=~0ULL) const

void	toString (std::string &Res, unsigned radix=10) const

int	compareContents (const Expr &b) const

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

virtual unsigned	computeHash ()

void	toMemory (void *address)

bool	isZero () const
	isZero - Is this a constant zero. More...

bool	isOne () const
	isOne - Is this a constant one. More...

bool	isTrue () const
	isTrue - Is this the true expression. More...

bool	isFalse () const
	isFalse - Is this the false expression. More...

bool	isAllOnes () const
	isAllOnes - Is this constant all ones. More...

ref< ConstantExpr >	Concat (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	Extract (unsigned offset, Width W)

ref< ConstantExpr >	ZExt (Width W)

ref< ConstantExpr >	SExt (Width W)

ref< ConstantExpr >	Add (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	Sub (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	Mul (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	UDiv (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	SDiv (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	URem (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	SRem (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	And (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	Or (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	Xor (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	Shl (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	LShr (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	AShr (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	Eq (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	Ne (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	Ult (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	Ule (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	Ugt (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	Uge (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	Slt (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	Sle (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	Sgt (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	Sge (const ref< ConstantExpr > &RHS)

ref< ConstantExpr >	Neg ()

ref< ConstantExpr >	Not ()

Public Member Functions inherited from klee::Expr
	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 ref< Expr >	fromMemory (void *address, Width w)

static ref< ConstantExpr >	alloc (const llvm::APInt &v)

static ref< ConstantExpr >	alloc (const llvm::APFloat &f)

static ref< ConstantExpr >	alloc (uint64_t v, Width w)

static ref< ConstantExpr >	create (uint64_t v, Width w)

static bool	classof (const Expr *E)

static bool	classof (const ConstantExpr *)

Static Public Member Functions inherited from klee::Expr
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 *)

Static Public Attributes
static const Kind	kind = Constant

static const unsigned	numKids = 0

Static Public Attributes inherited from klee::Expr
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

Private Member Functions
	ConstantExpr (const llvm::APInt &v)

Private Attributes
llvm::APInt	value

Additional Inherited Members
Public Types inherited from klee::Expr
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 Attributes inherited from klee::Expr
class ReferenceCounter	_refCount
	Required by klee::ref-managed objects. More...

virtual int	compareContents (const Expr &b) const =0

Protected Attributes inherited from klee::Expr
unsigned	hashValue

Detailed Description

Definition at line 996 of file Expr.h.

Constructor & Destructor Documentation

◆ ConstantExpr()

klee::ConstantExpr::ConstantExpr ( const llvm::APInt & v )

inlineprivate

Definition at line 1004 of file Expr.h.

◆ ~ConstantExpr()

klee::ConstantExpr::~ConstantExpr ( )

inline

Definition at line 1007 of file Expr.h.

Member Function Documentation

◆ Add()

ref< ConstantExpr > ConstantExpr::Add ( const ref< ConstantExpr > & RHS )

Definition at line 399 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

◆ alloc() [1/3]

static ref< ConstantExpr > klee::ConstantExpr::alloc ( const llvm::APFloat & f )

inlinestatic

Definition at line 1071 of file Expr.h.

◆ alloc() [2/3]

static ref< ConstantExpr > klee::ConstantExpr::alloc ( const llvm::APInt & v )

inlinestatic

Definition at line 1065 of file Expr.h.

◆ alloc() [3/3]

static ref< ConstantExpr > klee::ConstantExpr::alloc	(	uint64_t	v,
		Width	w
	)

inlinestatic

Definition at line 1075 of file Expr.h.

◆ And()

ref< ConstantExpr > ConstantExpr::And ( const ref< ConstantExpr > & RHS )

Definition at line 431 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

◆ AShr()

ref< ConstantExpr > ConstantExpr::AShr ( const ref< ConstantExpr > & RHS )

Definition at line 451 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

◆ classof() [1/2]

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

inlinestatic

Definition at line 1088 of file Expr.h.

◆ classof() [2/2]

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

inlinestatic

Definition at line 1087 of file Expr.h.

References klee::Expr::Constant, and klee::Expr::getKind().

Here is the call graph for this function:

◆ compareContents()

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

inlinevirtual

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.

Implements klee::Expr.

Definition at line 1046 of file Expr.h.

References getWidth(), and value.

Here is the call graph for this function:

◆ computeHash()

unsigned ConstantExpr::computeHash ( )

virtual

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

Reimplemented from klee::Expr.

Definition at line 195 of file Expr.cpp.

References getWidth(), klee::Expr::hashValue, klee::Expr::MAGIC_HASH_CONSTANT, and value.

Here is the call graph for this function:

◆ Concat()

ref< ConstantExpr > ConstantExpr::Concat ( const ref< ConstantExpr > & RHS )

Definition at line 377 of file Expr.cpp.

References alloc(), getWidth(), and value.

Here is the call graph for this function:

◆ create()

static ref< ConstantExpr > klee::ConstantExpr::create	(	uint64_t	v,
		Width	w
	)

inlinestatic

Definition at line 1079 of file Expr.h.

References klee::bits64::truncateToNBits().

Referenced by klee::ExprOptimizer::buildMixedSelectExpr(), klee::Executor::callExternalFunction(), klee::Expr::createIsZero(), klee::Expr::createPointer(), EqExpr_createPartialR(), klee::Executor::evalConstant(), klee::Executor::executeCall(), klee::Executor::executeInstruction(), klee::ObjectState::flushRangeForRead(), klee::ObjectState::flushRangeForWrite(), fromMemory(), klee::MemoryObject::getBaseExpr(), klee::Executor::getEhTypeidFor(), klee::Solver::getRange(), klee::ExprOptimizer::getSelectOptExpr(), klee::MemoryObject::getSizeExpr(), klee::ObjectState::getUpdates(), klee::ArrayExprHelper::hasOrderedReads(), klee::AssignmentGenerator::hasOrderedReads(), klee::ExprOptimizer::optimizeExpr(), klee::ExprSMTLIBPrinter::printAShrExpr(), klee::ObjectState::read(), klee::ObjectState::read8(), klee::ExprRewriter::rewrite(), SRemExpr_create(), URemExpr_create(), klee::ObjectState::write(), and XorExpr_createPartialR().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Eq()

ref< ConstantExpr > ConstantExpr::Eq ( const ref< ConstantExpr > & RHS )

Definition at line 459 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

◆ Extract()

ref< ConstantExpr > ConstantExpr::Extract	(	unsigned	offset,
		Width	W
	)

Definition at line 387 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

◆ fromMemory()

ref< Expr > ConstantExpr::fromMemory	(	void *	address,
		Width	w
	)

static

Definition at line 337 of file Expr.cpp.

References alloc(), klee::Expr::Bool, create(), klee::Expr::Int16, klee::Expr::Int32, klee::Expr::Int64, and klee::Expr::Int8.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getAPValue()

const llvm::APInt & klee::ConstantExpr::getAPValue ( ) const

inline

getAPValue - Return the arbitrary precision value directly.

Clients should generally not use the APInt value directly and instead use native ConstantExpr APIs.

Definition at line 1019 of file Expr.h.

Referenced by klee::AssignmentGenerator::getIndexedValue().

Here is the caller graph for this function:

◆ getKid()

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

inlinevirtual

Implements klee::Expr.

Definition at line 1013 of file Expr.h.

◆ getKind()

Kind klee::ConstantExpr::getKind ( ) const

inlinevirtual

Implements klee::Expr.

Definition at line 1010 of file Expr.h.

◆ getLimitedValue()

uint64_t klee::ConstantExpr::getLimitedValue ( uint64_t Limit = ~0ULL ) const

inline

getLimitedValue - If this value is smaller than the specified limit, return it, otherwise return the limit value.

Definition at line 1037 of file Expr.h.

◆ getNumKids()

unsigned klee::ConstantExpr::getNumKids ( ) const

inlinevirtual

Implements klee::Expr.

Definition at line 1012 of file Expr.h.

◆ getWidth()

Width klee::ConstantExpr::getWidth ( ) const

inlinevirtual

Implements klee::Expr.

Definition at line 1009 of file Expr.h.

Referenced by compareContents(), computeHash(), Concat(), and toMemory().

Here is the caller graph for this function:

◆ getZExtValue()

uint64_t klee::ConstantExpr::getZExtValue ( unsigned bits = 64 ) const

inline

getZExtValue - Returns the constant value zero extended to the return type of this method.

Parameters

bits	- optional parameter that can be used to check that the number of bits used by this constant is <= to the parameter value. This is useful for checking that type casts won't truncate useful bits.

Example: unit8_t byte= (unit8_t) constant->getZExtValue(8);

Definition at line 1030 of file Expr.h.

Referenced by klee::Executor::callExternalFunction(), klee::Executor::executeInstruction(), klee::ObjectState::getUpdates(), and toMemory().

Here is the caller graph for this function:

◆ isAllOnes()

bool klee::ConstantExpr::isAllOnes ( ) const

inline

isAllOnes - Is this constant all ones.

Definition at line 1109 of file Expr.h.

◆ isFalse()

bool klee::ConstantExpr::isFalse ( ) const

inline

isFalse - Is this the false expression.

Definition at line 1104 of file Expr.h.

References klee::Expr::Bool.

Referenced by klee::AssignmentValidatingSolver::computeInitialValues(), and getAllIndependentConstraintsSets().

Here is the caller graph for this function:

◆ isOne()

bool klee::ConstantExpr::isOne ( ) const

inline

isOne - Is this a constant one.

Definition at line 1096 of file Expr.h.

◆ isTrue()

bool klee::ConstantExpr::isTrue ( ) const

inline

isTrue - Is this the true expression.

Definition at line 1099 of file Expr.h.

References klee::Expr::Bool.

Referenced by klee::AssignmentValidatingSolver::computeInitialValues().

Here is the caller graph for this function:

◆ isZero()

bool klee::ConstantExpr::isZero ( ) const

inline

isZero - Is this a constant zero.

Definition at line 1093 of file Expr.h.

◆ LShr()

ref< ConstantExpr > ConstantExpr::LShr ( const ref< ConstantExpr > & RHS )

Definition at line 447 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

◆ Mul()

ref< ConstantExpr > ConstantExpr::Mul ( const ref< ConstantExpr > & RHS )

Definition at line 411 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

◆ Ne()

ref< ConstantExpr > ConstantExpr::Ne ( const ref< ConstantExpr > & RHS )

Definition at line 463 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

◆ Neg()

ref< ConstantExpr > ConstantExpr::Neg ( )

Definition at line 403 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

◆ Not()

ref< ConstantExpr > ConstantExpr::Not ( )

Definition at line 455 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

◆ Or()

ref< ConstantExpr > ConstantExpr::Or ( const ref< ConstantExpr > & RHS )

Definition at line 435 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

◆ rebuild()

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

inlinevirtual

Implements klee::Expr.

Definition at line 1055 of file Expr.h.

◆ SDiv()

ref< ConstantExpr > ConstantExpr::SDiv ( const ref< ConstantExpr > & RHS )

Definition at line 419 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

◆ SExt()

ref< ConstantExpr > ConstantExpr::SExt ( Width W )

Definition at line 395 of file Expr.cpp.

References alloc(), and value.

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ Sge()

ref< ConstantExpr > ConstantExpr::Sge ( const ref< ConstantExpr > & RHS )

Definition at line 495 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

◆ Sgt()

ref< ConstantExpr > ConstantExpr::Sgt ( const ref< ConstantExpr > & RHS )

Definition at line 491 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

◆ Shl()

ref< ConstantExpr > ConstantExpr::Shl ( const ref< ConstantExpr > & RHS )

Definition at line 443 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

◆ Sle()

ref< ConstantExpr > ConstantExpr::Sle ( const ref< ConstantExpr > & RHS )

Definition at line 487 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

◆ Slt()

ref< ConstantExpr > ConstantExpr::Slt ( const ref< ConstantExpr > & RHS )

Definition at line 483 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

◆ SRem()

ref< ConstantExpr > ConstantExpr::SRem ( const ref< ConstantExpr > & RHS )

Definition at line 427 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

◆ Sub()

ref< ConstantExpr > ConstantExpr::Sub ( const ref< ConstantExpr > & RHS )

Definition at line 407 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

◆ toMemory()

void ConstantExpr::toMemory ( void * address )

Definition at line 354 of file Expr.cpp.

References klee::Expr::Bool, klee::Expr::Fl80, getWidth(), getZExtValue(), klee::Expr::Int16, klee::Expr::Int32, klee::Expr::Int64, klee::Expr::Int8, and value.

Here is the call graph for this function:

◆ toString()

void ConstantExpr::toString	(	std::string &	Res,
		unsigned	radix = `10`
	)		const

toString - Return the constant value as a string

Parameters

Res	specifies the string for the result to be placed in
radix	specifies the base (e.g. 2,10,16). The default is base 10

Definition at line 369 of file Expr.cpp.

References value.

◆ UDiv()

ref< ConstantExpr > ConstantExpr::UDiv ( const ref< ConstantExpr > & RHS )

Definition at line 415 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

◆ Uge()

ref< ConstantExpr > ConstantExpr::Uge ( const ref< ConstantExpr > & RHS )

Definition at line 479 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

◆ Ugt()

ref< ConstantExpr > ConstantExpr::Ugt ( const ref< ConstantExpr > & RHS )

Definition at line 475 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

◆ Ule()

ref< ConstantExpr > ConstantExpr::Ule ( const ref< ConstantExpr > & RHS )

Definition at line 471 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

◆ Ult()

ref< ConstantExpr > ConstantExpr::Ult ( const ref< ConstantExpr > & RHS )

Definition at line 467 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

◆ URem()

ref< ConstantExpr > ConstantExpr::URem ( const ref< ConstantExpr > & RHS )

Definition at line 423 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

◆ Xor()

ref< ConstantExpr > ConstantExpr::Xor ( const ref< ConstantExpr > & RHS )

Definition at line 439 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

◆ ZExt()

ref< ConstantExpr > ConstantExpr::ZExt ( Width W )

Definition at line 391 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

Member Data Documentation

◆ kind

const Kind klee::ConstantExpr::kind = Constant

static

Definition at line 998 of file Expr.h.

◆ numKids

const unsigned klee::ConstantExpr::numKids = 0

static

Definition at line 999 of file Expr.h.

◆ value

llvm::APInt klee::ConstantExpr::value

private

Definition at line 1002 of file Expr.h.

Referenced by Add(), And(), AShr(), compareContents(), computeHash(), Concat(), Eq(), Extract(), LShr(), Mul(), Ne(), Neg(), Not(), Or(), SDiv(), SExt(), Sge(), Sgt(), Shl(), Sle(), Slt(), SRem(), Sub(), toMemory(), toString(), UDiv(), Uge(), Ugt(), Ule(), Ult(), URem(), Xor(), and ZExt().

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

/Users/cristic/klee/include/klee/Expr/Expr.h
/Users/cristic/klee/lib/Expr/Expr.cpp

Public Member Functions

Static Public Member Functions

Static Public Attributes

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ ConstantExpr()

◆ ~ConstantExpr()

Member Function Documentation

◆ Add()

◆ alloc() [1/3]

◆ alloc() [2/3]

◆ alloc() [3/3]

◆ And()

◆ AShr()

◆ classof() [1/2]

◆ classof() [2/2]

◆ compareContents()

◆ computeHash()

◆ Concat()

◆ create()

◆ Eq()

◆ Extract()

◆ fromMemory()

◆ getAPValue()

◆ getKid()

◆ getKind()

◆ getLimitedValue()

◆ getNumKids()

◆ getWidth()

◆ getZExtValue()

◆ isAllOnes()

◆ isFalse()

◆ isOne()

◆ isTrue()

◆ isZero()

◆ LShr()

◆ Mul()

◆ Ne()

◆ Neg()

◆ Not()

◆ Or()

◆ rebuild()

◆ SDiv()

◆ SExt()

◆ Sge()

◆ Sgt()

◆ Shl()

◆ Sle()

◆ Slt()

◆ SRem()

◆ Sub()

◆ toMemory()

◆ toString()

◆ UDiv()

◆ Uge()

◆ Ugt()

◆ Ule()

◆ Ult()

◆ URem()

◆ Xor()

◆ ZExt()

Member Data Documentation

◆ kind

◆ numKids

◆ value