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

#include <STPBuilder.h>

Collaboration diagram for klee::STPBuilder:

Public Member Functions

 STPBuilder (::VC _vc, bool _optimizeDivides=true)
 
 ~STPBuilder ()
 
ExprHandle getTrue ()
 
ExprHandle getFalse ()
 
ExprHandle getTempVar (Expr::Width w)
 
ExprHandle getInitialRead (const Array *os, unsigned index)
 
ExprHandle construct (ref< Expr > e)
 

Private Member Functions

ExprHandle bvOne (unsigned width)
 
ExprHandle bvZero (unsigned width)
 
ExprHandle bvMinusOne (unsigned width)
 
ExprHandle bvConst32 (unsigned width, uint32_t value)
 
ExprHandle bvConst64 (unsigned width, uint64_t value)
 
ExprHandle bvZExtConst (unsigned width, uint64_t value)
 
ExprHandle bvSExtConst (unsigned width, uint64_t value)
 
ExprHandle bvBoolExtract (ExprHandle expr, int bit)
 
ExprHandle bvExtract (ExprHandle expr, unsigned top, unsigned bottom)
 
ExprHandle eqExpr (ExprHandle a, ExprHandle b)
 
ExprHandle bvLeftShift (ExprHandle expr, unsigned shift)
 
ExprHandle bvRightShift (ExprHandle expr, unsigned shift)
 
ExprHandle bvVarLeftShift (ExprHandle expr, ExprHandle shift)
 
ExprHandle bvVarRightShift (ExprHandle expr, ExprHandle shift)
 
ExprHandle bvVarArithRightShift (ExprHandle expr, ExprHandle shift)
 
ExprHandle constructAShrByConstant (ExprHandle expr, unsigned shift, ExprHandle isSigned)
 
ExprHandle constructMulByConstant (ExprHandle expr, unsigned width, uint64_t x)
 
ExprHandle constructUDivByConstant (ExprHandle expr_n, unsigned width, uint64_t d)
 
ExprHandle constructSDivByConstant (ExprHandle expr_n, unsigned width, uint64_t d)
 
::VCExpr getInitialArray (const Array *os)
 
::VCExpr getArrayForUpdate (const Array *root, const UpdateNode *un)
 
ExprHandle constructActual (ref< Expr > e, int *width_out)
 
ExprHandle construct (ref< Expr > e, int *width_out)
 
::VCExpr buildVar (const char *name, unsigned width)
 
::VCExpr buildArray (const char *name, unsigned indexWidth, unsigned valueWidth)
 

Private Attributes

::VC vc
 
ExprHandle tempVars [4]
 
ExprHashMap< std::pair
< ExprHandle, unsigned > > 
constructed
 
bool optimizeDivides
 
STPArrayExprHash _arr_hash
 

Detailed Description

Definition at line 69 of file STPBuilder.h.

Constructor & Destructor Documentation

STPBuilder::STPBuilder ( ::VC  _vc,
bool  _optimizeDivides = true 
)

Definition at line 80 of file STPBuilder.cpp.

References buildVar(), and tempVars.

Here is the call graph for this function:

STPBuilder::~STPBuilder ( )

Definition at line 89 of file STPBuilder.cpp.

Member Function Documentation

VCExpr STPBuilder::buildArray ( const char *  name,
unsigned  indexWidth,
unsigned  valueWidth 
)
private

Definition at line 107 of file STPBuilder.cpp.

References vc, and vc_DeleteExpr().

Referenced by getInitialArray().

Here is the call graph for this function:

Here is the caller graph for this function:

VCExpr STPBuilder::buildVar ( const char *  name,
unsigned  width 
)
private

Definition at line 99 of file STPBuilder.cpp.

References vc, and vc_DeleteExpr().

Referenced by STPBuilder().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::bvBoolExtract ( ExprHandle  expr,
int  bit 
)
private

Definition at line 165 of file STPBuilder.cpp.

References bvExtract(), bvOne(), and vc.

Referenced by bvVarArithRightShift(), constructActual(), and constructSDivByConstant().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::bvConst32 ( unsigned  width,
uint32_t  value 
)
private

Definition at line 144 of file STPBuilder.cpp.

References vc.

Referenced by bvVarArithRightShift(), bvVarLeftShift(), bvVarRightShift(), constructActual(), constructSDivByConstant(), constructUDivByConstant(), and getInitialRead().

Here is the caller graph for this function:

ExprHandle STPBuilder::bvConst64 ( unsigned  width,
uint64_t  value 
)
private

Definition at line 147 of file STPBuilder.cpp.

References vc.

Referenced by bvSExtConst(), bvZExtConst(), and constructActual().

Here is the caller graph for this function:

ExprHandle STPBuilder::bvExtract ( ExprHandle  expr,
unsigned  top,
unsigned  bottom 
)
private

Definition at line 168 of file STPBuilder.cpp.

References vc.

Referenced by bvBoolExtract(), bvLeftShift(), bvRightShift(), constructActual(), and constructAShrByConstant().

Here is the caller graph for this function:

ExprHandle STPBuilder::bvLeftShift ( ExprHandle  expr,
unsigned  shift 
)
private

Definition at line 191 of file STPBuilder.cpp.

References bvExtract(), bvZero(), and vc.

Referenced by bvVarLeftShift(), constructActual(), and constructMulByConstant().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::bvMinusOne ( unsigned  width)
private

Definition at line 141 of file STPBuilder.cpp.

References bvSExtConst().

Referenced by constructActual(), constructAShrByConstant(), and constructSDivByConstant().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::bvOne ( unsigned  width)
private

Definition at line 135 of file STPBuilder.cpp.

References bvZExtConst().

Referenced by bvBoolExtract(), and constructActual().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::bvRightShift ( ExprHandle  expr,
unsigned  shift 
)
private

Definition at line 176 of file STPBuilder.cpp.

References bvExtract(), bvZero(), and vc.

Referenced by bvVarRightShift(), constructActual(), and constructAShrByConstant().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::bvSExtConst ( unsigned  width,
uint64_t  value 
)
private

Definition at line 159 of file STPBuilder.cpp.

References bvConst64(), and vc.

Referenced by bvMinusOne().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::bvVarArithRightShift ( ExprHandle  expr,
ExprHandle  shift 
)
private

Definition at line 250 of file STPBuilder.cpp.

References bvBoolExtract(), bvConst32(), bvZero(), constructAShrByConstant(), eqExpr(), and vc.

Referenced by constructActual().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::bvVarLeftShift ( ExprHandle  expr,
ExprHandle  shift 
)
private

Definition at line 208 of file STPBuilder.cpp.

References bvConst32(), bvLeftShift(), bvZero(), eqExpr(), and vc.

Referenced by constructActual().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::bvVarRightShift ( ExprHandle  expr,
ExprHandle  shift 
)
private

Definition at line 229 of file STPBuilder.cpp.

References bvConst32(), bvRightShift(), bvZero(), eqExpr(), and vc.

Referenced by constructActual(), constructSDivByConstant(), and constructUDivByConstant().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::bvZero ( unsigned  width)
private

Definition at line 138 of file STPBuilder.cpp.

References bvZExtConst().

Referenced by bvLeftShift(), bvRightShift(), bvVarArithRightShift(), bvVarLeftShift(), bvVarRightShift(), constructActual(), constructAShrByConstant(), constructMulByConstant(), constructSDivByConstant(), and constructUDivByConstant().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::bvZExtConst ( unsigned  width,
uint64_t  value 
)
private

Definition at line 150 of file STPBuilder.cpp.

References bvConst64(), and vc.

Referenced by bvOne(), and bvZero().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::construct ( ref< Expr e,
int *  width_out 
)
private

if *width_out!=1 then result is a bitvector, otherwise it is a bool

Definition at line 491 of file STPBuilder.cpp.

References constructActual(), and constructed.

Referenced by construct(), constructActual(), getArrayForUpdate(), and getInitialArray().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle klee::STPBuilder::construct ( ref< Expr e)
inline

Definition at line 126 of file STPBuilder.h.

References construct(), and constructed.

Here is the call graph for this function:

ExprHandle STPBuilder::constructActual ( ref< Expr e,
int *  width_out 
)
private

if *width_out!=1 then result is a bitvector, otherwise it is a bool

Definition at line 514 of file STPBuilder.cpp.

References klee::Expr::Add, klee::Expr::And, klee::Expr::AShr, bvBoolExtract(), bvConst32(), bvConst64(), bvExtract(), bvLeftShift(), bvMinusOne(), bvOne(), bvRightShift(), bvVarArithRightShift(), bvVarLeftShift(), bvVarRightShift(), bvZero(), klee::Expr::Concat, klee::SelectExpr::cond, klee::Expr::Constant, construct(), constructAShrByConstant(), constructMulByConstant(), constructSDivByConstant(), constructUDivByConstant(), klee::Expr::Eq, klee::ExtractExpr::expr, klee::NotExpr::expr, klee::Expr::Extract, klee::SelectExpr::falseExpr, getArrayForUpdate(), getFalse(), klee::ConcatExpr::getKid(), klee::Expr::getKind(), klee::ConcatExpr::getNumKids(), klee::Array::getRange(), getTrue(), klee::ConstantExpr::getWidth(), klee::ConcatExpr::getWidth(), klee::ExtractExpr::getWidth(), klee::CastExpr::getWidth(), klee::ConstantExpr::getZExtValue(), klee::UpdateList::head, klee::ReadExpr::index, klee::bits64::indexOfSingleBit(), klee::bits64::isPowerOfTwo(), klee::ConstantExpr::isTrue(), klee::Expr::LShr, klee::Expr::Mul, klee::floats::ne(), klee::Expr::Ne, klee::Expr::Not, klee::Expr::NotOptimized, klee::ExtractExpr::offset, optimizeDivides, klee::Expr::Or, klee::stats::queryConstructs, klee::Expr::Read, klee::UpdateList::root, klee::Expr::SDiv, klee::Expr::Select, klee::Expr::SExt, klee::Expr::Sge, klee::Expr::Sgt, klee::Expr::Shl, klee::Expr::Sle, klee::Expr::Slt, klee::NotOptimizedExpr::src, klee::CastExpr::src, klee::Expr::SRem, klee::Expr::Sub, klee::SelectExpr::trueExpr, klee::Expr::UDiv, klee::Expr::Uge, klee::Expr::Ugt, klee::Expr::Ule, klee::Expr::Ult, klee::ReadExpr::updates, klee::Expr::URem, vc, klee::Expr::Xor, and klee::Expr::ZExt.

Referenced by construct().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::constructAShrByConstant ( ExprHandle  expr,
unsigned  shift,
ExprHandle  isSigned 
)
private

Definition at line 279 of file STPBuilder.cpp.

References bvExtract(), bvMinusOne(), bvRightShift(), bvZero(), and vc.

Referenced by bvVarArithRightShift(), and constructActual().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::constructMulByConstant ( ExprHandle  expr,
unsigned  width,
uint64_t  x 
)
private

Definition at line 298 of file STPBuilder.cpp.

References add, bvLeftShift(), bvZero(), klee::ComputeMultConstants64(), klee::floats::sub(), klee::bits64::truncateToNBits(), and vc.

Referenced by constructActual(), constructSDivByConstant(), and constructUDivByConstant().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::constructSDivByConstant ( ExprHandle  expr_n,
unsigned  width,
uint64_t  d 
)
private

Definition at line 388 of file STPBuilder.cpp.

References bvBoolExtract(), bvConst32(), bvMinusOne(), bvVarRightShift(), bvZero(), klee::ComputeSDivConstants32(), constructMulByConstant(), and vc.

Referenced by constructActual().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::constructUDivByConstant ( ExprHandle  expr_n,
unsigned  width,
uint64_t  d 
)
private

Definition at line 351 of file STPBuilder.cpp.

References bvConst32(), bvVarRightShift(), bvZero(), klee::ComputeUDivConstants32(), constructMulByConstant(), and vc.

Referenced by constructActual().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::eqExpr ( ExprHandle  a,
ExprHandle  b 
)
private

Definition at line 171 of file STPBuilder.cpp.

References vc.

Referenced by bvVarArithRightShift(), bvVarLeftShift(), and bvVarRightShift().

Here is the caller graph for this function:

VCExpr STPBuilder::getArrayForUpdate ( const Array root,
const UpdateNode un 
)
private

Definition at line 466 of file STPBuilder.cpp.

References _arr_hash, construct(), getInitialArray(), klee::ArrayExprHash< T >::hashUpdateNodeExpr(), klee::UpdateNode::index, klee::ArrayExprHash< T >::lookupUpdateNodeExpr(), klee::UpdateNode::next, klee::UpdateNode::value, and vc.

Referenced by constructActual().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::getFalse ( )

Definition at line 132 of file STPBuilder.cpp.

References vc.

Referenced by constructActual().

Here is the caller graph for this function:

VCExpr STPBuilder::getInitialArray ( const Array os)
private
ExprHandle STPBuilder::getInitialRead ( const Array os,
unsigned  index 
)

Definition at line 462 of file STPBuilder.cpp.

References bvConst32(), getInitialArray(), and vc.

Referenced by runAndGetCex(), and runAndGetCexForked().

Here is the call graph for this function:

Here is the caller graph for this function:

ExprHandle STPBuilder::getTempVar ( Expr::Width  w)
ExprHandle STPBuilder::getTrue ( )

Definition at line 129 of file STPBuilder.cpp.

References vc.

Referenced by constructActual().

Here is the caller graph for this function:

Member Data Documentation

STPArrayExprHash klee::STPBuilder::_arr_hash
private

Definition at line 79 of file STPBuilder.h.

Referenced by getArrayForUpdate(), and getInitialArray().

ExprHashMap< std::pair<ExprHandle, unsigned> > klee::STPBuilder::constructed
private

Definition at line 72 of file STPBuilder.h.

Referenced by construct().

bool klee::STPBuilder::optimizeDivides
private

optimizeDivides - Rewrite division and reminders by constants into multiplies and shifts. STP should probably handle this for use.

Definition at line 77 of file STPBuilder.h.

Referenced by constructActual().

ExprHandle klee::STPBuilder::tempVars[4]
private

Definition at line 71 of file STPBuilder.h.

Referenced by getTempVar(), and STPBuilder().


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