#include <Expr.h>

Inheritance diagram for klee::ConcatExpr:

Collaboration diagram for klee::ConcatExpr:

[legend]

Public Member Functions
Width	getWidth () const

Kind	getKind () const

ref< Expr >	getLeft () const

ref< Expr >	getRight () const

unsigned	getNumKids () const

ref< Expr >	getKid (unsigned i) const

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

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 >	alloc (const ref< Expr > &l, const ref< Expr > &r)

static ref< Expr >	create (const ref< Expr > &l, const ref< Expr > &r)

static ref< Expr >	createN (unsigned nKids, const ref< Expr > kids[])
	Shortcuts to create larger concats. The chain returned is unbalanced to the right. More...

static ref< Expr >	create4 (const ref< Expr > &kid1, const ref< Expr > &kid2, const ref< Expr > &kid3, const ref< Expr > &kid4)
	Shortcut to concat 4 kids. The chain returned is unbalanced to the right. More...

static ref< Expr >	create8 (const ref< Expr > &kid1, const ref< Expr > &kid2, const ref< Expr > &kid3, const ref< Expr > &kid4, const ref< Expr > &kid5, const ref< Expr > &kid6, const ref< Expr > &kid7, const ref< Expr > &kid8)
	Shortcut to concat 8 kids. The chain returned is unbalanced to the right. More...

static bool	classof (const Expr *E)

static bool	classof (const ConcatExpr *)

Static Public Member Functions inherited from klee::NonConstantExpr
static bool	classof (const Expr *E)

static bool	classof (const NonConstantExpr *)

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 = Concat

static const unsigned	numKids = 2

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

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

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

Private Member Functions
	ConcatExpr (const ref< Expr > &l, const ref< Expr > &r)

Private Attributes
Width	width

ref< Expr >	left

ref< Expr >	right

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...

Protected Attributes inherited from klee::Expr
unsigned	hashValue

Detailed Description

Children of a concat expression can have arbitrary widths.
Kid 0 is the left kid, kid 1 is the right kid.

Definition at line 673 of file Expr.h.

Constructor & Destructor Documentation

◆ ConcatExpr()

klee::ConcatExpr::ConcatExpr	(	const ref< Expr > &	l,
		const ref< Expr > &	r
	)

inlineprivate

Definition at line 715 of file Expr.h.

References klee::Expr::getWidth(), and width.

Referenced by alloc().

Here is the call graph for this function:

Here is the caller graph for this function:

Member Function Documentation

◆ alloc()

static ref< Expr > klee::ConcatExpr::alloc	(	const ref< Expr > &	l,
		const ref< Expr > &	r
	)

inlinestatic

Definition at line 683 of file Expr.h.

References klee::Expr::computeHash(), and ConcatExpr().

Referenced by create().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ classof() [1/2]

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

inlinestatic

Definition at line 723 of file Expr.h.

◆ classof() [2/2]

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

inlinestatic

Definition at line 720 of file Expr.h.

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

Here is the call graph for this function:

◆ compareContents()

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

inlineprotectedvirtual

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 726 of file Expr.h.

References width.

◆ create()

ref< Expr > ConcatExpr::create	(	const ref< Expr > &	l,
		const ref< Expr > &	r
	)

static

Definition at line 623 of file Expr.cpp.

References alloc(), klee::ExtractExpr::create(), and klee::Expr::getWidth().

Referenced by klee::ExtractExpr::create(), create4(), create8(), klee::Expr::createFromKind(), createN(), klee::Expr::createTempRead(), klee::Executor::executeCall(), klee::Executor::executeInstruction(), klee::ObjectState::read(), and rebuild().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ create4()

ref< Expr > ConcatExpr::create4	(	const ref< Expr > &	kid1,
		const ref< Expr > &	kid2,
		const ref< Expr > &	kid3,
		const ref< Expr > &	kid4
	)

static

Shortcut to concat 4 kids. The chain returned is unbalanced to the right.

Definition at line 659 of file Expr.cpp.

References create().

Referenced by create8(), and klee::Expr::createTempRead().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ create8()

ref< Expr > ConcatExpr::create8	(	const ref< Expr > &	kid1,
		const ref< Expr > &	kid2,
		const ref< Expr > &	kid3,
		const ref< Expr > &	kid4,
		const ref< Expr > &	kid5,
		const ref< Expr > &	kid6,
		const ref< Expr > &	kid7,
		const ref< Expr > &	kid8
	)

static

Shortcut to concat 8 kids. The chain returned is unbalanced to the right.

Definition at line 665 of file Expr.cpp.

References create(), and create4().

Referenced by klee::Expr::createTempRead().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ createN()

ref< Expr > ConcatExpr::createN	(	unsigned	nKids,
		const ref< Expr >	kids[]
	)

static

Shortcuts to create larger concats. The chain returned is unbalanced to the right.

Shortcut to concat N kids. The chain returned is unbalanced to the right.

Definition at line 647 of file Expr.cpp.

References create().

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

Here is the call graph for this function:

Here is the caller graph for this function:

◆ getKid()

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

inlinevirtual

Implements klee::Expr.

Definition at line 697 of file Expr.h.

References left, and right.

Referenced by klee::ImpliedValue::getImpliedValues(), klee::ArrayExprHelper::hasOrderedReads(), CexData::propogatePossibleValues(), and klee::IndexTransformationExprVisitor::visitConcat().

Here is the caller graph for this function:

◆ getKind()

Kind klee::ConcatExpr::getKind ( ) const

inlinevirtual

Implements klee::Expr.

Definition at line 692 of file Expr.h.

References kind.

◆ getLeft()

ref< Expr > klee::ConcatExpr::getLeft ( ) const

inline

Definition at line 693 of file Expr.h.

References left.

◆ getNumKids()

unsigned klee::ConcatExpr::getNumKids ( ) const

inlinevirtual

Implements klee::Expr.

Definition at line 696 of file Expr.h.

References numKids.

◆ getRight()

ref< Expr > klee::ConcatExpr::getRight ( ) const

inline

Definition at line 694 of file Expr.h.

References right.

◆ getWidth()

Width klee::ConcatExpr::getWidth ( ) const

inlinevirtual

Implements klee::Expr.

Definition at line 691 of file Expr.h.

References width.

Referenced by klee::IndexTransformationExprVisitor::visitConcat(), and klee::ArrayReadExprVisitor::visitConcat().

Here is the caller graph for this function:

◆ rebuild()

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

inlinevirtual

Implements klee::Expr.

Definition at line 712 of file Expr.h.

References create().

Here is the call graph for this function:

Member Data Documentation

◆ kind

const Kind klee::ConcatExpr::kind = Concat

static

Definition at line 675 of file Expr.h.

Referenced by getKind().

◆ left

ref<Expr> klee::ConcatExpr::left

private

Definition at line 680 of file Expr.h.

Referenced by getKid(), and getLeft().

◆ numKids

const unsigned klee::ConcatExpr::numKids = 2

static

Definition at line 676 of file Expr.h.

Referenced by getNumKids().

◆ right

ref<Expr> klee::ConcatExpr::right

private

Definition at line 680 of file Expr.h.

Referenced by getKid(), and getRight().

◆ width

Width klee::ConcatExpr::width

private

Definition at line 679 of file Expr.h.

Referenced by compareContents(), ConcatExpr(), and getWidth().

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

Protected Member Functions

Private Member Functions

Private Attributes

Additional Inherited Members

Detailed Description

Constructor & Destructor Documentation

◆ ConcatExpr()

Member Function Documentation

◆ alloc()

◆ classof() [1/2]

◆ classof() [2/2]

◆ compareContents()

◆ create()

◆ create4()

◆ create8()

◆ createN()

◆ getKid()

◆ getKind()

◆ getLeft()

◆ getNumKids()

◆ getRight()

◆ getWidth()

◆ rebuild()

Member Data Documentation

◆ kind

◆ left

◆ numKids

◆ right

◆ width