klee
|
#include <Expr.h>
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 |
![]() | |
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 bool | classof (const Expr *E) |
static bool | classof (const NonConstantExpr *) |
![]() | |
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 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 | |
![]() | |
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... | |
![]() | |
class ReferenceCounter | _refCount |
Required by klee::ref-managed objects. More... | |
![]() | |
unsigned | hashValue |
Children of a concat expression can have arbitrary widths.
Kid 0 is the left kid, kid 1 is the right kid.
Definition at line 715 of file Expr.h.
References klee::Expr::getWidth(), and width.
Referenced by alloc().
|
inlinestatic |
Definition at line 683 of file Expr.h.
References klee::Expr::computeHash(), and ConcatExpr().
Referenced by create().
|
inlinestatic |
|
inlinestatic |
Definition at line 720 of file Expr.h.
References klee::Expr::Concat, and klee::Expr::getKind().
|
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.
[in] | b | Expr to compare this to. |
this
is <
b
ignoring kid expressions.this
is >
b
ignoring kid expressions.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.
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().
|
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().
|
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().
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().
Implements klee::Expr.
Definition at line 697 of file Expr.h.
Referenced by klee::ImpliedValue::getImpliedValues(), klee::ArrayExprHelper::hasOrderedReads(), CexData::propogatePossibleValues(), and klee::IndexTransformationExprVisitor::visitConcat().
|
inlinevirtual |
|
inlinevirtual |
|
inlinevirtual |
Implements klee::Expr.
Definition at line 691 of file Expr.h.
References width.
Referenced by klee::IndexTransformationExprVisitor::visitConcat(), and klee::ArrayReadExprVisitor::visitConcat().
Implements klee::Expr.
Definition at line 712 of file Expr.h.
References create().
|
static |
Definition at line 676 of file Expr.h.
Referenced by getNumKids().
Definition at line 680 of file Expr.h.
Referenced by getKid(), and getRight().
|
private |
Definition at line 679 of file Expr.h.
Referenced by compareContents(), ConcatExpr(), and getWidth().