klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee::Expr Class Referenceabstract

Class representing symbolic expressions. More...

#include <Expr.h>

Inheritance diagram for klee::Expr:

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,
  Not, 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...
 
typedef llvm::DenseSet
< std::pair< const Expr
*, const Expr * > > 
ExprEquivSet
 Returns 0 iff b is structuraly equivalent to *this. More...
 

Public Member Functions

 Expr ()
 
virtual ~Expr ()
 
virtual Kind getKind () const =0
 
virtual Width getWidth () const =0
 
virtual unsigned getNumKids () const =0
 
virtual ref< ExprgetKid (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, ExprEquivSet &equivs) const
 
int compare (const Expr &b) const
 
virtual int compareContents (const Expr &b) const
 
virtual ref< Exprrebuild (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< ExprcreateSExtToPointerWidth (ref< Expr > e)
 
static ref< ExprcreateZExtToPointerWidth (ref< Expr > e)
 
static ref< ExprcreateImplies (ref< Expr > hyp, ref< Expr > conc)
 
static ref< ExprcreateIsZero (ref< Expr > e)
 
static ref< ExprcreateTempRead (const Array *array, Expr::Width w)
 
static ref< ConstantExprcreatePointer (uint64_t v)
 
static ref< ExprcreateFromKind (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
 
static const Width Fl80 = 80
 

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:

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

Member Typedef Documentation

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

Returns 0 iff b is structuraly equivalent to *this.

Definition at line 199 of file Expr.h.

typedef unsigned klee::Expr::Width

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

Definition at line 94 of file Expr.h.

Member Enumeration Documentation

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

Constructor & Destructor Documentation

klee::Expr::Expr ( )
inline

Definition at line 177 of file Expr.h.

References count.

virtual klee::Expr::~Expr ( )
inlinevirtual

Definition at line 178 of file Expr.h.

References count.

Member Function Documentation

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

Definition at line 254 of file Expr.h.

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

Definition at line 87 of file Expr.cpp.

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

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

Here is the call graph for this function:

Here is the caller graph for this function:

int klee::Expr::compare ( const Expr b) const
inline

Definition at line 201 of file Expr.h.

References compare().

Here is the call graph for this function:

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

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

Definition at line 207 of file Expr.h.

unsigned Expr::computeHash ( )
virtual

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

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

Definition at line 166 of file Expr.cpp.

References MAGIC_HASH_CONSTANT.

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

Here is the caller graph for this function:

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

Definition at line 213 of file Expr.cpp.

References BINARY_EXPR_CASE, CAST_EXPR_CASE, klee::NotOptimizedExpr::create(), klee::SelectExpr::create(), and klee::ConcatExpr::create().

Here is the call graph for this function:

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

Definition at line 301 of file Expr.cpp.

References createIsZero().

Here is the call graph for this function:

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

Definition at line 51 of file Context.cpp.

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

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

Here is the call graph for this function:

Here is the caller graph for this function:

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

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

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::ReadExpr::create(), klee::ConcatExpr::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:

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

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

void Expr::dump ( ) const

dump - Print the expression to stderr.

Definition at line 313 of file Expr.cpp.

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

Here is the caller graph for this function:

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

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

Definition at line 230 of file Expr.h.

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

Here is the caller graph for this function:

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

Returns the pre-computed hash of the current expression.

Definition at line 192 of file Expr.h.

References hashValue.

Referenced by klee::UpdateNode::computeHash(), klee::util::ExprHash::operator()(), and CachingSolver::CacheEntryHash::operator()().

Here is the caller graph for this function:

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

isFalse - Is this the false expression.

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

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

isTrue - Is this the true expression.

Definition at line 1094 of file Expr.h.

References Bool, and getWidth().

Referenced by propogateValues(), and klee::Assignment::satisfies().

Here is the call graph for this function:

Here is the caller graph for this function:

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

Definition at line 251 of file Expr.h.

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

isZero - Is this a constant zero.

Definition at line 1088 of file Expr.h.

References isZero().

Referenced by isZero().

Here is the call graph for this function:

Here is the caller graph for this function:

static bool klee::Expr::needsResultType ( )
inlinestatic

Definition at line 252 of file Expr.h.

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

Definition at line 309 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 ( llvm::raw_ostream &  os,
Kind  k 
)
static

Definition at line 119 of file Expr.cpp.

References X.

Referenced by klee::operator<<().

Here is the caller graph for this function:

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

Definition at line 289 of file Expr.cpp.

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

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

Member Data Documentation

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

Definition at line 97 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(), STPSolverImpl::getConstraintLog(), klee::ImpliedValue::getImpliedValues(), 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::ExprSMTLIBPrinter::printCastToSort(), PPrinter::printConst(), klee::ExprPPrinter::printConstraints(), printWidth(), CexData::propogateExactValues(), CexData::propogatePossibleValues(), klee::ObjectState::read(), SDivExpr_create(), klee::ConstantExpr::Sge(), klee::ConstantExpr::Sgt(), ShlExpr_create(), PPrinter::shouldPrintWidth(), 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().

unsigned Expr::count = 0
static

Definition at line 90 of file Expr.h.

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

const Width klee::Expr::Fl80 = 80
static

Definition at line 102 of file Expr.h.

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

unsigned klee::Expr::hashValue
protected

Definition at line 174 of file Expr.h.

Referenced by compare(), and hash().

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

Definition at line 96 of file Expr.h.

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

unsigned klee::Expr::refCount

Definition at line 171 of file Expr.h.


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