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

#include <Expr.h>

Inheritance diagram for klee::ConstantExpr:
Collaboration diagram for klee::ConstantExpr:

Public Member Functions

 ~ConstantExpr ()
 
Width getWidth () const
 
Kind getKind () const
 
unsigned getNumKids () const
 
ref< ExprgetKid (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< Exprrebuild (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< ConstantExprConcat (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprExtract (unsigned offset, Width W)
 
ref< ConstantExprZExt (Width W)
 
ref< ConstantExprSExt (Width W)
 
ref< ConstantExprAdd (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprSub (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprMul (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprUDiv (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprSDiv (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprURem (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprSRem (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprAnd (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprOr (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprXor (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprShl (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprLShr (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprAShr (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprEq (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprNe (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprUlt (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprUle (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprUgt (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprUge (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprSlt (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprSle (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprSgt (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprSge (const ref< ConstantExpr > &RHS)
 
ref< ConstantExprNeg ()
 
ref< ConstantExprNot ()
 
- 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...
 
int compare (const Expr &b, ExprEquivSet &equivs) const
 
int compare (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< ExprfromMemory (void *address, Width w)
 
static ref< ConstantExpralloc (const llvm::APInt &v)
 
static ref< ConstantExpralloc (const llvm::APFloat &f)
 
static ref< ConstantExpralloc (uint64_t v, Width w)
 
static ref< ConstantExprcreate (uint64_t v, Width w)
 
static bool classof (const Expr *E)
 
static bool classof (const ConstantExpr *)
 
- 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 = Constant
 
static const unsigned numKids = 0
 
- 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

 ConstantExpr (const llvm::APInt &v)
 

Private Attributes

llvm::APInt value
 

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

Definition at line 327 of file Expr.h.

Constructor & Destructor Documentation

klee::ConstantExpr::ConstantExpr ( const llvm::APInt &  v)
inlineprivate

Definition at line 335 of file Expr.h.

Referenced by alloc().

Here is the caller graph for this function:

klee::ConstantExpr::~ConstantExpr ( )
inline

Definition at line 338 of file Expr.h.

Member Function Documentation

ref< ConstantExpr > ConstantExpr::Add ( const ref< ConstantExpr > &  RHS)

Definition at line 376 of file Expr.cpp.

References alloc(), and value.

Referenced by klee::Executor::computeOffsets(), and klee::Executor::evalConstantExpr().

Here is the call graph for this function:

Here is the caller graph for this function:

static ref<ConstantExpr> klee::ConstantExpr::alloc ( const llvm::APInt &  v)
inlinestatic

Definition at line 398 of file Expr.h.

References ConstantExpr().

Referenced by Add(), klee::Executor::addConstraint(), alloc(), And(), AShr(), klee::ImpliedValue::checkForImpliedValues(), ValidatingSolver::computeInitialValues(), klee::Executor::computeOffsets(), Concat(), create(), klee::Expr::createTempRead(), Eq(), EqExpr_create(), klee::Executor::evalConstant(), klee::Executor::evalConstantExpr(), klee::ExprEvaluator::evalRead(), klee::Assignment::evaluate(), klee::Executor::executeAlloc(), klee::Executor::executeInstruction(), Extract(), klee::ExprBuilder::False(), fromMemory(), klee::MemoryObject::getBoundsCheckOffset(), klee::expr::SMTParser::GetConstExpr(), klee::Executor::getConstraintLog(), STPSolverImpl::getConstraintLog(), klee::ImpliedValue::getImpliedValues(), klee::STPBuilder::getInitialArray(), CexPossibleEvaluator::getInitialValue(), CexExactEvaluator::getInitialValue(), klee::TimingSolver::getInitialValues(), klee::Executor::getSymbolicSolution(), PPrinter::hasOrderedReads(), LShr(), klee::ExecutionState::merge(), Mul(), Ne(), Neg(), Not(), Or(), klee::SeedInfo::patchSeed(), klee::ExprPPrinter::printConstraints(), CexData::propogatePossibleValues(), 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().

Here is the call graph for this function:

static ref<ConstantExpr> klee::ConstantExpr::alloc ( const llvm::APFloat &  f)
inlinestatic

Definition at line 404 of file Expr.h.

References alloc().

Here is the call graph for this function:

static ref<ConstantExpr> klee::ConstantExpr::alloc ( uint64_t  v,
Width  w 
)
inlinestatic

Definition at line 408 of file Expr.h.

References alloc().

Here is the call graph for this function:

ref< ConstantExpr > ConstantExpr::And ( const ref< ConstantExpr > &  RHS)

Definition at line 408 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

ref< ConstantExpr > ConstantExpr::AShr ( const ref< ConstantExpr > &  RHS)

Definition at line 428 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

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

Definition at line 418 of file Expr.h.

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

Here is the call graph for this function:

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

Definition at line 421 of file Expr.h.

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

Reimplemented from klee::Expr.

Definition at line 379 of file Expr.h.

References getWidth(), and value.

Here is the call graph for this function:

unsigned ConstantExpr::computeHash ( )
virtual

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

Reimplemented from klee::Expr.

Definition at line 179 of file Expr.cpp.

ref< ConstantExpr > ConstantExpr::Concat ( const ref< ConstantExpr > &  RHS)

Definition at line 354 of file Expr.cpp.

References alloc(), getWidth(), and value.

Here is the call graph for this function:

ref< ConstantExpr > ConstantExpr::Eq ( const ref< ConstantExpr > &  RHS)

Definition at line 436 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

ref< ConstantExpr > ConstantExpr::Extract ( unsigned  offset,
Width  W 
)

Definition at line 364 of file Expr.cpp.

References alloc().

Referenced by klee::ImpliedValue::getImpliedValues().

Here is the call graph for this function:

Here is the caller graph for this function:

ref< Expr > ConstantExpr::fromMemory ( void *  address,
Width  w 
)
static

Definition at line 320 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().

Here is the call graph for this function:

Here is the caller graph for this function:

const llvm::APInt& klee::ConstantExpr::getAPValue ( ) const
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 350 of file Expr.h.

References value.

Referenced by klee::Executor::executeInstruction(), isAllOnes(), and isZero().

Here is the caller graph for this function:

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

Implements klee::Expr.

Definition at line 344 of file Expr.h.

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

Implements klee::Expr.

Definition at line 341 of file Expr.h.

References klee::Expr::Constant.

uint64_t klee::ConstantExpr::getLimitedValue ( uint64_t  Limit = ~0ULL) const
inline

getLimitedValue - If this value is smaller than the specified limit, return it, otherwise return the limit value.

Definition at line 368 of file Expr.h.

References value.

Referenced by isOne(), and ValueRange::ValueRange().

Here is the caller graph for this function:

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

Implements klee::Expr.

Definition at line 343 of file Expr.h.

uint64_t klee::ConstantExpr::getZExtValue ( unsigned  bits = 64) const
inline

getZExtValue - Returns the constant value zero extended to the return type of this method.

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

References getWidth(), and value.

Referenced by klee::Executor::computeOffsets(), klee::STPBuilder::constructActual(), klee::Executor::executeInstruction(), klee::Executor::getAddressInfo(), klee::ObjectState::getUpdates(), klee::SeedInfo::patchSeed(), PPrinter::printConst(), klee::AddressSpace::resolve(), and klee::AddressSpace::resolveOne().

Here is the call graph for this function:

Here is the caller graph for this function:

bool klee::ConstantExpr::isAllOnes ( ) const
inline

isAllOnes - Is this constant all ones.

Definition at line 442 of file Expr.h.

References getAPValue().

Referenced by AndExpr_createPartial(), and OrExpr_createPartial().

Here is the call graph for this function:

Here is the caller graph for this function:

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

isFalse - Is this the false expression.

Definition at line 437 of file Expr.h.

References klee::Expr::Bool, getWidth(), and value.

Here is the call graph for this function:

bool klee::ConstantExpr::isOne ( ) const
inline

isOne - Is this a constant one.

Definition at line 429 of file Expr.h.

References getLimitedValue().

Referenced by MulExpr_createPartialR().

Here is the call graph for this function:

Here is the caller graph for this function:

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

isTrue - Is this the true expression.

Definition at line 432 of file Expr.h.

References klee::Expr::Bool, getWidth(), and value.

Referenced by klee::Executor::branch(), klee::STPBuilder::constructActual(), EqExpr_createPartialR(), klee::Executor::fork(), klee::ImpliedValue::getImpliedValues(), and PPrinter::printConst().

Here is the call graph for this function:

Here is the caller graph for this function:

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

isZero - Is this a constant zero.

Definition at line 426 of file Expr.h.

References getAPValue().

Referenced by AddExpr_createPartialR(), AndExpr_createPartial(), klee::ImpliedValue::getImpliedValues(), MulExpr_createPartialR(), OrExpr_createPartial(), and XorExpr_createPartialR().

Here is the call graph for this function:

Here is the caller graph for this function:

ref< ConstantExpr > ConstantExpr::LShr ( const ref< ConstantExpr > &  RHS)

Definition at line 424 of file Expr.cpp.

References alloc(), and value.

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

Here is the call graph for this function:

Here is the caller graph for this function:

ref< ConstantExpr > ConstantExpr::Mul ( const ref< ConstantExpr > &  RHS)

Definition at line 388 of file Expr.cpp.

References alloc(), and value.

Referenced by klee::Executor::computeOffsets(), and klee::Executor::evalConstantExpr().

Here is the call graph for this function:

Here is the caller graph for this function:

ref< ConstantExpr > ConstantExpr::Ne ( const ref< ConstantExpr > &  RHS)

Definition at line 440 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

ref< ConstantExpr > ConstantExpr::Neg ( )

Definition at line 380 of file Expr.cpp.

References alloc().

Here is the call graph for this function:

ref< ConstantExpr > ConstantExpr::Not ( )

Definition at line 432 of file Expr.cpp.

References alloc().

Referenced by klee::ImpliedValue::getImpliedValues().

Here is the call graph for this function:

Here is the caller graph for this function:

ref< ConstantExpr > ConstantExpr::Or ( const ref< ConstantExpr > &  RHS)

Definition at line 412 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

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

Implements klee::Expr.

Definition at line 388 of file Expr.h.

ref< ConstantExpr > ConstantExpr::SDiv ( const ref< ConstantExpr > &  RHS)

Definition at line 396 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

ref< ConstantExpr > ConstantExpr::SExt ( Width  W)

Definition at line 372 of file Expr.cpp.

References alloc().

Referenced by EqExpr_createPartialR().

Here is the call graph for this function:

Here is the caller graph for this function:

ref< ConstantExpr > ConstantExpr::Sge ( const ref< ConstantExpr > &  RHS)

Definition at line 472 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

ref< ConstantExpr > ConstantExpr::Sgt ( const ref< ConstantExpr > &  RHS)

Definition at line 468 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

ref< ConstantExpr > ConstantExpr::Shl ( const ref< ConstantExpr > &  RHS)

Definition at line 420 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

ref< ConstantExpr > ConstantExpr::Sle ( const ref< ConstantExpr > &  RHS)

Definition at line 464 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

ref< ConstantExpr > ConstantExpr::Slt ( const ref< ConstantExpr > &  RHS)

Definition at line 460 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

ref< ConstantExpr > ConstantExpr::SRem ( const ref< ConstantExpr > &  RHS)

Definition at line 404 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

ref< ConstantExpr > ConstantExpr::Sub ( const ref< ConstantExpr > &  RHS)

Definition at line 384 of file Expr.cpp.

References alloc(), and value.

Referenced by klee::ImpliedValue::getImpliedValues().

Here is the call graph for this function:

Here is the caller graph for this function:

void ConstantExpr::toMemory ( void *  address)

Definition at line 335 of file Expr.cpp.

References klee::Expr::Bool, klee::Expr::Fl80, klee::Expr::Int16, klee::Expr::Int32, klee::Expr::Int64, and klee::Expr::Int8.

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

Here is the caller graph for this function:

void ConstantExpr::toString ( std::string &  Res,
unsigned  radix = 10 
) const

toString - Return the constant value as a string

Parameters
Resspecifies the string for the result to be placed in
radixspecifies the base (e.g. 2,10,16). The default is base 10

Definition at line 350 of file Expr.cpp.

Referenced by PPrinter::printConst().

Here is the caller graph for this function:

ref< ConstantExpr > ConstantExpr::UDiv ( const ref< ConstantExpr > &  RHS)

Definition at line 392 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

ref< ConstantExpr > ConstantExpr::Uge ( const ref< ConstantExpr > &  RHS)

Definition at line 456 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

ref< ConstantExpr > ConstantExpr::Ugt ( const ref< ConstantExpr > &  RHS)

Definition at line 452 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

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

Here is the call graph for this function:

Here is the caller graph for this function:

ref< ConstantExpr > ConstantExpr::Ule ( const ref< ConstantExpr > &  RHS)

Definition at line 448 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

ref< ConstantExpr > ConstantExpr::Ult ( const ref< ConstantExpr > &  RHS)

Definition at line 444 of file Expr.cpp.

References alloc(), klee::Expr::Bool, and value.

Here is the call graph for this function:

ref< ConstantExpr > ConstantExpr::URem ( const ref< ConstantExpr > &  RHS)

Definition at line 400 of file Expr.cpp.

References alloc(), and value.

Here is the call graph for this function:

ref< ConstantExpr > ConstantExpr::Xor ( const ref< ConstantExpr > &  RHS)

Definition at line 416 of file Expr.cpp.

References alloc(), and value.

Referenced by klee::ImpliedValue::getImpliedValues().

Here is the call graph for this function:

Here is the caller graph for this function:

ref< ConstantExpr > ConstantExpr::ZExt ( Width  W)

Definition at line 368 of file Expr.cpp.

References alloc().

Referenced by EqExpr_createPartialR(), klee::Executor::evalConstantExpr(), and klee::Executor::initializeGlobalObject().

Here is the call graph for this function:

Here is the caller graph for this function:

Member Data Documentation

const Kind klee::ConstantExpr::kind = Constant
static

Definition at line 329 of file Expr.h.

const unsigned klee::ConstantExpr::numKids = 0
static

Definition at line 330 of file Expr.h.

llvm::APInt klee::ConstantExpr::value
private

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