klee::Expr Class Reference

Class representing symbolic expressions. More...

#include <Expr.h>

Inheritance diagram for klee::Expr:

List of all members.

Classes

struct CreateArg

Public Types

enum Kind {
  InvalidKind = -1, Constant = 0, NotOptimized, Read = NotOptimized+2,
  Select, Concat, Extract, ZExt,
  SExt, 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.

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 (std::ostream &os) const

virtual unsigned hash () const

Returns the pre-computed hash of the current expression.

virtual unsigned computeHash ()

int compare (const Expr &b) const

Returns 0 iff b is structuraly equivalent to *this.

virtual int compareContents (const Expr &b) const

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

bool isZero () const

isZero - Is this a constant zero.

bool isTrue () const

isTrue - Is this the true expression.

bool isFalse () const

isFalse - Is this the false expression.

Static Public Member Functions

static void printKind (std::ostream &os, Kind k)

static void printWidth (std::ostream &os, Expr::Width w)

static Width getWidthForLLVMType (const llvm::Type *type)

static unsigned getMinBytesForWidth (Width w)

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

static ref< Expr > createCoerceToPointerType (ref< Expr > e)

static ref< Expr > createNot (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< Expr > 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

unsigned refCount

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

Protected Attributes

unsigned hashValue

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:

No Expr has all constant arguments.
Booleans:
1. Boolean not is written as (false == ?)
2. Ne, Ugt, Uge, Sgt, Sge are not used
3. The only acceptable operations with boolean arguments are And, Or, Xor, Eq, as well as SExt, ZExt, Select and NotOptimized.
4. The only boolean operation which may involve a constant is boolean not (== false).
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, ?).
Chains are unbalanced to the right

Steps required for adding an expr:

Add case to printKind
Add to ExprVisitor
Add to IVC (implied value concretization) if possible

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

Definition at line 85 of file Expr.h.

Member Typedef Documentation

typedef unsigned klee::Expr::Width

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

Definition at line 91 of file Expr.h.

Member Enumeration Documentation

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
Add
Sub
Mul
UDiv
SDiv
URem
SRem
And
Or
Xor
Shl
LShr
AShr
Eq
Ne
Ult	Not used in canonical form.
Ule
Ugt
Uge	Not used in canonical form.
Slt	Not used in canonical form.
Sle
Sgt
Sge	Not used in canonical form.
LastKind	Not used in canonical form.
CastKindFirst
CastKindLast
BinaryKindFirst
BinaryKindLast
CmpKindFirst
CmpKindLast

Definition at line 101 of file Expr.h.

Constructor & Destructor Documentation

klee::Expr::Expr ( ) [inline]

Definition at line 172 of file Expr.h.

References count.

virtual klee::Expr::~Expr ( ) [inline, virtual]

Definition at line 173 of file Expr.h.

References count.

Member Function Documentation

static bool klee::Expr::classof ( const Expr * ) [inline, static]

Reimplemented in klee::ConstantExpr, klee::BinaryExpr, klee::CmpExpr, klee::NotOptimizedExpr, klee::ReadExpr, klee::SelectExpr, klee::ConcatExpr, klee::ExtractExpr, and klee::CastExpr.

Definition at line 240 of file Expr.h.

int Expr::compare ( const Expr & b ) const

Returns 0 iff b is structuraly equivalent to *this.

Definition at line 87 of file Expr.cpp.

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

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

Here is the call graph for this function:

Here is the caller graph for this function:

virtual int klee::Expr::compareContents ( const Expr & b ) const [inline, virtual]

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

Definition at line 192 of file Expr.h.

Referenced by compare().

Here is the caller graph for this function:

unsigned Expr::computeHash ( ) [virtual]

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

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

Definition at line 154 of file Expr.cpp.

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

Here is the call graph for this function:

ref< Expr > Expr::createCoerceToPointerType ( ref< Expr > e ) [static]

Definition at line 310 of file Expr.cpp.

References kMachinePointerType.

Referenced by klee::Executor::bindInstructionConstants(), klee::Executor::evalConstantExpr(), and klee::Executor::executeInstruction().

Here is the caller graph for this function:

ref< Expr > Expr::createFromKind	(	Kind	k,
		std::vector< CreateArg >	args
	)			`[static]`

Definition at line 192 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:

ref< Expr > Expr::createImplies	(	ref< Expr >	hyp,
		ref< Expr >	conc
	)			`[static]`

Definition at line 302 of file Expr.cpp.

References createNot().

Here is the call graph for this function:

ref< Expr > Expr::createIsZero ( ref< Expr > e ) [static]

Definition at line 306 of file Expr.cpp.

References klee::ConstantExpr::create().

Referenced by createNot(), and klee::Executor::executeFree().

Here is the call graph for this function:

Here is the caller graph for this function:

ref< Expr > Expr::createNot ( ref< Expr > e ) [static]

Definition at line 314 of file Expr.cpp.

References createIsZero().

Referenced by klee::SelectExpr::create(), createImplies(), EqExpr_createPartialR(), klee::Executor::executeInstruction(), klee::Executor::fork(), klee::Executor::getSymbolicSolution(), LShrExpr_create(), klee::TimingSolver::mustBeFalse(), klee::Query::negateExpr(), and ShlExpr_create().

Here is the call graph for this function:

Here is the caller graph for this function:

ref< Expr > Expr::createPointer ( uint64_t v ) [static]

Definition at line 318 of file Expr.cpp.

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

Referenced by klee::Executor::bindInstructionConstants(), klee::Executor::evalConstantExpr(), klee::Executor::executeFree(), klee::Executor::executeInstruction(), and klee::Executor::initializeGlobals().

Here is the call graph for this function:

Here is the caller graph for this function:

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 40 of file Expr.cpp.

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

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

Here is the call graph for this function:

Here is the caller graph for this function:

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

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

Referenced by AddExpr_create(), AddExpr_createPartialR(), compare(), computeHash(), klee::ExprRangeEvaluator< T >::evaluate(), klee::findReads(), PPrinter::hasSimpleKids(), PPrinter::isSimple(), PPrinter::printExpr(), PPrinter::scan1(), SubExpr_create(), SubExpr_createPartialR(), and klee::ExprVisitor::visitActual().

Here is the caller graph for this function:

virtual Kind klee::Expr::getKind ( ) const [pure virtual]

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

Referenced by AddExpr_create(), AddExpr_createPartialR(), klee::CastExpr::classof(), klee::ExtractExpr::classof(), klee::ConcatExpr::classof(), klee::SelectExpr::classof(), klee::ReadExpr::classof(), klee::NotOptimizedExpr::classof(), klee::CmpExpr::classof(), klee::BinaryExpr::classof(), klee::ConstantExpr::classof(), compare(), computeHash(), EqExpr_createPartialR(), SubExpr_create(), SubExpr_createPartialR(), and klee::ExprVisitor::visitActual().

Here is the caller graph for this function:

static unsigned klee::Expr::getMinBytesForWidth ( Width w ) [inline, static]

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

Definition at line 216 of file Expr.h.

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

Here is the caller graph for this function:

virtual unsigned klee::Expr::getNumKids ( ) const [pure virtual]

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

Referenced by compare(), computeHash(), klee::ExprRangeEvaluator< T >::evaluate(), klee::findReads(), PPrinter::hasSimpleKids(), PPrinter::isSimple(), PPrinter::printExpr(), PPrinter::scan1(), and klee::ExprVisitor::visitActual().

Here is the caller graph for this function:

virtual Width klee::Expr::getWidth ( ) const [pure virtual]

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

Referenced by _getImpliedValue(), AddExpr_create(), CexData::forceExprToRange(), MulExpr_create(), and SubExpr_create().

Here is the caller graph for this function:

Expr::Width Expr::getWidthForLLVMType ( const llvm::Type * type ) [static]

Definition at line 279 of file Expr.cpp.

References Int32, Int64, and kMachinePointerType.

Referenced by klee::Executor::evalConstantExpr(), klee::Executor::executeInstruction(), and klee::Executor::executeMemoryOperation().

Here is the caller graph for this function:

virtual unsigned klee::Expr::hash ( ) const [inline, virtual]

Returns the pre-computed hash of the current expression.

Definition at line 184 of file Expr.h.

References hashValue.

bool klee::Expr::isFalse ( ) const [inline]

isFalse - Is this the false expression.

Definition at line 910 of file Expr.h.

References Bool.

bool klee::Expr::isTrue ( ) const [inline]

isTrue - Is this the true expression.

Definition at line 903 of file Expr.h.

References Bool.

static bool klee::Expr::isValidKidWidth	(	unsigned	kid,
		Width	w
	)			`[inline, static]`

Reimplemented in klee::SelectExpr.

Definition at line 237 of file Expr.h.

bool klee::Expr::isZero ( ) const [inline]

isZero - Is this a constant zero.

Definition at line 897 of file Expr.h.

static bool klee::Expr::needsResultType ( ) [inline, static]

Reimplemented in klee::CastExpr.

Definition at line 238 of file Expr.h.

void Expr::print ( std::ostream & os ) const [virtual]

Definition at line 322 of file Expr.cpp.

References klee::ExprPPrinter::printSingleExpr().

Referenced by klee::operator<<().

Here is the call graph for this function:

Here is the caller graph for this function:

void Expr::printKind	(	std::ostream &	os,
		Kind	k
	)			`[static]`

Definition at line 108 of file Expr.cpp.

References Add, And, AShr, Concat, Constant, Eq, Extract, LShr, Mul, Ne, 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::operator<<().

Here is the caller graph for this function:

void Expr::printWidth	(	std::ostream &	os,
		Expr::Width	w
	)			`[static]`

Definition at line 268 of file Expr.cpp.

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

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

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

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

Here is the caller graph for this function:

Member Data Documentation

const Width klee::Expr::Bool = 1 [static]

Definition at line 94 of file Expr.h.

Referenced by klee::Executor::addConstraint(), AddExpr_create(), AddExpr_createPartialR(), AShrExpr_create(), klee::SelectExpr::create(), createTempRead(), EqExpr_create(), EqExpr_createPartialR(), klee::Solver::evaluate(), klee::Executor::executeInstruction(), klee::ConstantExpr::fromMemory(), klee::MemoryObject::getBoundsCheckOffset(), klee::Executor::getConstraintLog(), klee::TimingSolver::getInitialValues(), klee::Executor::getSymbolicSolution(), klee::CmpExpr::getWidth(), isFalse(), isTrue(), klee::SelectExpr::isValidKidWidth(), LShrExpr_create(), klee::ExecutionState::merge(), MulExpr_create(), MulExpr_createPartialR(), klee::Solver::mustBeTrue(), klee::ExprPPrinter::printConstraints(), printWidth(), klee::ObjectState::read(), klee::ObjectState::read1(), SDivExpr_create(), ShlExpr_create(), klee::ConstraintManager::simplifyExpr(), SRemExpr_create(), SubExpr_create(), SubExpr_createPartialR(), klee::ConstantExpr::toMemory(), TryConstArrayOpt(), UDivExpr_create(), URemExpr_create(), klee::Query::withFalse(), klee::ObjectState::write(), and XorExpr_createPartialR().

unsigned Expr::count = 0 [static]

Definition at line 87 of file Expr.h.

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

unsigned klee::Expr::hashValue [protected]

Definition at line 169 of file Expr.h.

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

const Width klee::Expr::Int16 = 16 [static]

Definition at line 96 of file Expr.h.

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

const Width klee::Expr::Int32 = 32 [static]

Definition at line 97 of file Expr.h.

Referenced by createTempRead(), klee::ExprEvaluator::evalRead(), klee::Assignment::evaluate(), klee::Executor::executeAlloc(), klee::ConstantExpr::fromMemory(), klee::STPBuilder::getTempVar(), getWidthForLLVMType(), klee::SeedInfo::patchSeed(), printWidth(), klee::ObjectState::read(), klee::ConstantExpr::toMemory(), and klee::ObjectState::write().

const Width klee::Expr::Int64 = 64 [static]

Definition at line 98 of file Expr.h.

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

const Width klee::Expr::InvalidWidth = 0 [static]

Definition at line 93 of file Expr.h.

Referenced by klee::Expr::Expr::CreateArg::isWidth().

const unsigned klee::Expr::MAGIC_HASH_CONSTANT = 39 [static]

Definition at line 88 of file Expr.h.

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

unsigned klee::Expr::refCount

Definition at line 166 of file Expr.h.

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

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


Classes
struct	CreateArg
Public Types
enum	Kind { InvalidKind = -1, Constant = 0, NotOptimized, Read = NotOptimized+2, Select, Concat, Extract, ZExt, SExt, 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.
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 (std::ostream &os) const
virtual unsigned	hash () const
	Returns the pre-computed hash of the current expression.
virtual unsigned	computeHash ()
int	compare (const Expr &b) const
	Returns 0 iff b is structuraly equivalent to *this.
virtual int	compareContents (const Expr &b) const
virtual ref< Expr >	rebuild (ref< Expr > kids[]) const =0
bool	isZero () const
	isZero - Is this a constant zero.
bool	isTrue () const
	isTrue - Is this the true expression.
bool	isFalse () const
	isFalse - Is this the false expression.
Static Public Member Functions
static void	printKind (std::ostream &os, Kind k)
static void	printWidth (std::ostream &os, Expr::Width w)
static Width	getWidthForLLVMType (const llvm::Type *type)
static unsigned	getMinBytesForWidth (Width w)
	returns the smallest number of bytes in which the given width fits
static ref< Expr >	createCoerceToPointerType (ref< Expr > e)
static ref< Expr >	createNot (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< Expr >	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
unsigned	refCount
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
Protected Attributes
unsigned	hashValue