klee
|
#include <Expr.h>
Public Member Functions | |
~ConstantExpr () | |
Width | getWidth () const |
Kind | getKind () const |
unsigned | getNumKids () const |
ref< Expr > | getKid (unsigned i) const |
const llvm::APInt & | getAPValue () const |
uint64_t | getZExtValue (unsigned bits=64) const |
uint64_t | getLimitedValue (uint64_t Limit=~0ULL) const |
void | toString (std::string &Res, unsigned radix=10) const |
int | compareContents (const Expr &b) const |
virtual ref< Expr > | rebuild (ref< Expr > kids[]) const |
virtual unsigned | computeHash () |
void | toMemory (void *address) |
bool | isZero () const |
isZero - Is this a constant zero. More... | |
bool | isOne () const |
isOne - Is this a constant one. More... | |
bool | isTrue () const |
isTrue - Is this the true expression. More... | |
bool | isFalse () const |
isFalse - Is this the false expression. More... | |
bool | isAllOnes () const |
isAllOnes - Is this constant all ones. More... | |
ref< ConstantExpr > | Concat (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | Extract (unsigned offset, Width W) |
ref< ConstantExpr > | ZExt (Width W) |
ref< ConstantExpr > | SExt (Width W) |
ref< ConstantExpr > | Add (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | Sub (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | Mul (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | UDiv (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | SDiv (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | URem (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | SRem (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | And (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | Or (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | Xor (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | Shl (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | LShr (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | AShr (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | Eq (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | Ne (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | Ult (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | Ule (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | Ugt (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | Uge (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | Slt (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | Sle (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | Sgt (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | Sge (const ref< ConstantExpr > &RHS) |
ref< ConstantExpr > | Neg () |
ref< ConstantExpr > | Not () |
![]() | |
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 > | fromMemory (void *address, Width w) |
static ref< ConstantExpr > | alloc (const llvm::APInt &v) |
static ref< ConstantExpr > | alloc (const llvm::APFloat &f) |
static ref< ConstantExpr > | alloc (uint64_t v, Width w) |
static ref< ConstantExpr > | create (uint64_t v, Width w) |
static bool | classof (const Expr *E) |
static bool | classof (const ConstantExpr *) |
![]() | |
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 = Constant |
static const unsigned | numKids = 0 |
![]() | |
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 | |
ConstantExpr (const llvm::APInt &v) | |
Private Attributes | |
llvm::APInt | value |
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... | |
virtual int | compareContents (const Expr &b) const =0 |
![]() | |
unsigned | hashValue |
|
inlineprivate |
ref< ConstantExpr > ConstantExpr::Add | ( | const ref< ConstantExpr > & | RHS | ) |
|
inlinestatic |
|
inlinestatic |
Definition at line 1065 of file Expr.h.
Referenced by Add(), klee::Executor::addConstraint(), And(), AShr(), klee::ExprOptimizer::computeIndexes(), klee::ValidatingSolver::computeInitialValues(), klee::Executor::computeOffsets(), klee::Executor::computeOffsetsSeqTy(), Concat(), klee::Assignment::createConstraintsFromAssignment(), klee::Expr::createTempRead(), Eq(), EqExpr_create(), klee::Executor::evalConstant(), klee::Executor::evalConstantExpr(), klee::ExprEvaluator::evalRead(), klee::Assignment::evaluate(), klee::Executor::executeAlloc(), klee::Executor::executeCall(), klee::Executor::executeInstruction(), Extract(), klee::ExprBuilder::False(), fromMemory(), klee::MemoryObject::getBoundsCheckOffset(), klee::Executor::getConstraintLog(), klee::TimingSolver::getInitialValues(), klee::Executor::getSymbolicSolution(), klee::ArrayExprHelper::hasOrderedReads(), klee::AssignmentGenerator::hasOrderedReads(), LShr(), klee::ExecutionState::merge(), Mul(), Ne(), Neg(), Not(), Or(), klee::SeedInfo::patchSeed(), klee::ExprPPrinter::printConstraints(), klee::ExprRewriter::rewrite(), klee::Executor::runFunctionAsMain(), SDiv(), SExt(), Sge(), Sgt(), Shl(), klee::ConstraintManager::simplifyExpr(), Sle(), Slt(), SRem(), Sub(), SubExpr_create(), SubExpr_createPartial(), klee::ExprBuilder::True(), TryConstArrayOpt(), UDiv(), Uge(), Ugt(), Ule(), Ult(), URem(), klee::Query::withFalse(), Xor(), and ZExt().
|
inlinestatic |
ref< ConstantExpr > ConstantExpr::And | ( | const ref< ConstantExpr > & | RHS | ) |
ref< ConstantExpr > ConstantExpr::AShr | ( | const ref< ConstantExpr > & | RHS | ) |
|
inlinestatic |
|
inlinestatic |
Definition at line 1087 of file Expr.h.
References klee::Expr::Constant, and klee::Expr::getKind().
|
inlinevirtual |
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 1046 of file Expr.h.
References getWidth(), and value.
|
virtual |
(Re)computes the hash of the current expression. Returns the hash value.
Reimplemented from klee::Expr.
Definition at line 195 of file Expr.cpp.
References getWidth(), klee::Expr::hashValue, klee::Expr::MAGIC_HASH_CONSTANT, and value.
ref< ConstantExpr > ConstantExpr::Concat | ( | const ref< ConstantExpr > & | RHS | ) |
Definition at line 377 of file Expr.cpp.
References alloc(), getWidth(), and value.
|
inlinestatic |
Definition at line 1079 of file Expr.h.
References klee::bits64::truncateToNBits().
Referenced by klee::ExprOptimizer::buildMixedSelectExpr(), klee::Executor::callExternalFunction(), klee::Expr::createIsZero(), klee::Expr::createPointer(), EqExpr_createPartialR(), klee::Executor::evalConstant(), klee::Executor::executeCall(), klee::Executor::executeInstruction(), klee::ObjectState::flushRangeForRead(), klee::ObjectState::flushRangeForWrite(), fromMemory(), klee::MemoryObject::getBaseExpr(), klee::Executor::getEhTypeidFor(), klee::Solver::getRange(), klee::ExprOptimizer::getSelectOptExpr(), klee::MemoryObject::getSizeExpr(), klee::ObjectState::getUpdates(), klee::ArrayExprHelper::hasOrderedReads(), klee::AssignmentGenerator::hasOrderedReads(), klee::ExprOptimizer::optimizeExpr(), klee::ExprSMTLIBPrinter::printAShrExpr(), klee::ObjectState::read(), klee::ObjectState::read8(), klee::ExprRewriter::rewrite(), SRemExpr_create(), URemExpr_create(), klee::ObjectState::write(), and XorExpr_createPartialR().
ref< ConstantExpr > ConstantExpr::Eq | ( | const ref< ConstantExpr > & | RHS | ) |
Definition at line 459 of file Expr.cpp.
References alloc(), klee::Expr::Bool, and value.
ref< ConstantExpr > ConstantExpr::Extract | ( | unsigned | offset, |
Width | W | ||
) |
Definition at line 337 of file Expr.cpp.
References alloc(), klee::Expr::Bool, create(), klee::Expr::Int16, klee::Expr::Int32, klee::Expr::Int64, and klee::Expr::Int8.
Referenced by klee::Executor::callExternalFunction().
|
inline |
getAPValue - Return the arbitrary precision value directly.
Clients should generally not use the APInt value directly and instead use native ConstantExpr APIs.
Definition at line 1019 of file Expr.h.
Referenced by klee::AssignmentGenerator::getIndexedValue().
Implements klee::Expr.
|
inlinevirtual |
Implements klee::Expr.
|
inline |
|
inlinevirtual |
Implements klee::Expr.
|
inlinevirtual |
Implements klee::Expr.
Definition at line 1009 of file Expr.h.
Referenced by compareContents(), computeHash(), Concat(), and toMemory().
|
inline |
getZExtValue - Returns the constant value zero extended to the return type of this method.
bits | - optional parameter that can be used to check that the number of bits used by this constant is <= to the parameter value. This is useful for checking that type casts won't truncate useful bits. |
Example: unit8_t byte= (unit8_t) constant->getZExtValue(8);
Definition at line 1030 of file Expr.h.
Referenced by klee::Executor::callExternalFunction(), klee::Executor::executeInstruction(), klee::ObjectState::getUpdates(), and toMemory().
|
inline |
|
inline |
isFalse - Is this the false expression.
Definition at line 1104 of file Expr.h.
References klee::Expr::Bool.
Referenced by klee::AssignmentValidatingSolver::computeInitialValues(), and getAllIndependentConstraintsSets().
|
inline |
|
inline |
isTrue - Is this the true expression.
Definition at line 1099 of file Expr.h.
References klee::Expr::Bool.
Referenced by klee::AssignmentValidatingSolver::computeInitialValues().
|
inline |
ref< ConstantExpr > ConstantExpr::LShr | ( | const ref< ConstantExpr > & | RHS | ) |
ref< ConstantExpr > ConstantExpr::Mul | ( | const ref< ConstantExpr > & | RHS | ) |
ref< ConstantExpr > ConstantExpr::Ne | ( | const ref< ConstantExpr > & | RHS | ) |
Definition at line 463 of file Expr.cpp.
References alloc(), klee::Expr::Bool, and value.
ref< ConstantExpr > ConstantExpr::Neg | ( | ) |
ref< ConstantExpr > ConstantExpr::Not | ( | ) |
ref< ConstantExpr > ConstantExpr::Or | ( | const ref< ConstantExpr > & | RHS | ) |
Implements klee::Expr.
ref< ConstantExpr > ConstantExpr::SDiv | ( | const ref< ConstantExpr > & | RHS | ) |
ref< ConstantExpr > ConstantExpr::SExt | ( | Width | W | ) |
Definition at line 395 of file Expr.cpp.
References alloc(), and value.
Referenced by klee::Executor::computeOffsetsSeqTy().
ref< ConstantExpr > ConstantExpr::Sge | ( | const ref< ConstantExpr > & | RHS | ) |
Definition at line 495 of file Expr.cpp.
References alloc(), klee::Expr::Bool, and value.
ref< ConstantExpr > ConstantExpr::Sgt | ( | const ref< ConstantExpr > & | RHS | ) |
Definition at line 491 of file Expr.cpp.
References alloc(), klee::Expr::Bool, and value.
ref< ConstantExpr > ConstantExpr::Shl | ( | const ref< ConstantExpr > & | RHS | ) |
ref< ConstantExpr > ConstantExpr::Sle | ( | const ref< ConstantExpr > & | RHS | ) |
Definition at line 487 of file Expr.cpp.
References alloc(), klee::Expr::Bool, and value.
ref< ConstantExpr > ConstantExpr::Slt | ( | const ref< ConstantExpr > & | RHS | ) |
Definition at line 483 of file Expr.cpp.
References alloc(), klee::Expr::Bool, and value.
ref< ConstantExpr > ConstantExpr::SRem | ( | const ref< ConstantExpr > & | RHS | ) |
ref< ConstantExpr > ConstantExpr::Sub | ( | const ref< ConstantExpr > & | RHS | ) |
void ConstantExpr::toMemory | ( | void * | address | ) |
Definition at line 354 of file Expr.cpp.
References klee::Expr::Bool, klee::Expr::Fl80, getWidth(), getZExtValue(), klee::Expr::Int16, klee::Expr::Int32, klee::Expr::Int64, klee::Expr::Int8, and value.
void ConstantExpr::toString | ( | std::string & | Res, |
unsigned | radix = 10 |
||
) | const |
ref< ConstantExpr > ConstantExpr::UDiv | ( | const ref< ConstantExpr > & | RHS | ) |
ref< ConstantExpr > ConstantExpr::Uge | ( | const ref< ConstantExpr > & | RHS | ) |
Definition at line 479 of file Expr.cpp.
References alloc(), klee::Expr::Bool, and value.
ref< ConstantExpr > ConstantExpr::Ugt | ( | const ref< ConstantExpr > & | RHS | ) |
Definition at line 475 of file Expr.cpp.
References alloc(), klee::Expr::Bool, and value.
ref< ConstantExpr > ConstantExpr::Ule | ( | const ref< ConstantExpr > & | RHS | ) |
Definition at line 471 of file Expr.cpp.
References alloc(), klee::Expr::Bool, and value.
ref< ConstantExpr > ConstantExpr::Ult | ( | const ref< ConstantExpr > & | RHS | ) |
Definition at line 467 of file Expr.cpp.
References alloc(), klee::Expr::Bool, and value.
ref< ConstantExpr > ConstantExpr::URem | ( | const ref< ConstantExpr > & | RHS | ) |
ref< ConstantExpr > ConstantExpr::Xor | ( | const ref< ConstantExpr > & | RHS | ) |
ref< ConstantExpr > ConstantExpr::ZExt | ( | Width | W | ) |
|
private |
Definition at line 1002 of file Expr.h.
Referenced by Add(), And(), AShr(), compareContents(), computeHash(), Concat(), Eq(), Extract(), LShr(), Mul(), Ne(), Neg(), Not(), Or(), SDiv(), SExt(), Sge(), Sgt(), Shl(), Sle(), Slt(), SRem(), Sub(), toMemory(), toString(), UDiv(), Uge(), Ugt(), Ule(), Ult(), URem(), Xor(), and ZExt().