klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
klee::ConcatExpr Class Reference

#include <Expr.h>

Inheritance diagram for klee::ConcatExpr:
Collaboration diagram for klee::ConcatExpr:

Public Member Functions

Width getWidth () const
 
Kind getKind () const
 
ref< ExprgetLeft () const
 
ref< ExprgetRight () const
 
unsigned getNumKids () const
 
ref< ExprgetKid (unsigned i) const
 
virtual ref< Exprrebuild (ref< Expr > kids[]) const
 
- Public Member Functions inherited from klee::Expr
 Expr ()
 
virtual ~Expr ()
 
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
 
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< Expralloc (const ref< Expr > &l, const ref< Expr > &r)
 
static ref< Exprcreate (const ref< Expr > &l, const ref< Expr > &r)
 
static ref< ExprcreateN (unsigned nKids, const ref< Expr > kids[])
 Shortcuts to create larger concats. The chain returned is unbalanced to the right. More...
 
static ref< Exprcreate4 (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< Exprcreate8 (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< 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 *)
 

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
 

Private Member Functions

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

Private Attributes

Width width
 
ref< Exprleft
 
ref< Exprright
 

Additional Inherited Members

- Public Types inherited from klee::Expr
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 Attributes inherited from klee::Expr
unsigned refCount
 
- 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 783 of file Expr.h.

Constructor & Destructor Documentation

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

Definition at line 825 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

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

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

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

Definition at line 830 of file Expr.h.

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

Here is the call graph for this function:

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

Definition at line 833 of file Expr.h.

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

Definition at line 558 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::executeInstruction(), klee::ObjectState::read(), and rebuild().

Here is the call graph for this function:

Here is the caller graph for this function:

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 594 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:

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 600 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:

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

References create().

Referenced by klee::expr::SMTParser::DeclareExpr(), and klee::Executor::evalConstant().

Here is the call graph for this function:

Here is the caller graph for this function:

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

Implements klee::Expr.

Definition at line 807 of file Expr.h.

References left, and right.

Referenced by klee::STPBuilder::constructActual(), klee::ImpliedValue::getImpliedValues(), and CexData::propogatePossibleValues().

Here is the caller graph for this function:

Kind klee::ConcatExpr::getKind ( ) const
inlinevirtual

Implements klee::Expr.

Definition at line 802 of file Expr.h.

References kind.

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

Definition at line 803 of file Expr.h.

References left.

unsigned klee::ConcatExpr::getNumKids ( ) const
inlinevirtual

Implements klee::Expr.

Definition at line 806 of file Expr.h.

References numKids.

Referenced by klee::STPBuilder::constructActual().

Here is the caller graph for this function:

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

Definition at line 804 of file Expr.h.

References right.

Width klee::ConcatExpr::getWidth ( ) const
inlinevirtual

Implements klee::Expr.

Definition at line 801 of file Expr.h.

References width.

Referenced by klee::STPBuilder::constructActual().

Here is the caller graph for this function:

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

Implements klee::Expr.

Definition at line 822 of file Expr.h.

References create().

Here is the call graph for this function:

Member Data Documentation

const Kind klee::ConcatExpr::kind = Concat
static

Definition at line 785 of file Expr.h.

Referenced by getKind().

ref<Expr> klee::ConcatExpr::left
private

Definition at line 790 of file Expr.h.

Referenced by getKid(), and getLeft().

const unsigned klee::ConcatExpr::numKids = 2
static

Definition at line 786 of file Expr.h.

Referenced by getNumKids().

ref<Expr> klee::ConcatExpr::right
private

Definition at line 790 of file Expr.h.

Referenced by getKid(), and getRight().

Width klee::ConcatExpr::width
private

Definition at line 789 of file Expr.h.

Referenced by ConcatExpr(), and getWidth().


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