klee
Public Member Functions | Private Member Functions | Private Attributes | List of all members
klee::STPBuilder Class Reference

#include <STPBuilder.h>

Collaboration diagram for klee::STPBuilder:
Collaboration graph
[legend]

Public Member Functions

 STPBuilder (::VC _vc, bool _optimizeDivides=true)
 
 ~STPBuilder ()
 
ExprHandle getTrue ()
 
ExprHandle getFalse ()
 
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 extractPartialShiftValue (ExprHandle shift, unsigned width, unsigned &shiftBits)
 
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
 
ExprHashMap< std::pair< ExprHandle, unsigned > > constructed
 
bool optimizeDivides
 
STPArrayExprHash _arr_hash
 

Detailed Description

Definition at line 65 of file STPBuilder.h.

Constructor & Destructor Documentation

◆ STPBuilder()

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

◆ ~STPBuilder()

klee::STPBuilder::~STPBuilder ( )

Member Function Documentation

◆ buildArray()

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

◆ buildVar()

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

◆ bvBoolExtract()

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

◆ bvConst32()

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

◆ bvConst64()

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

◆ bvExtract()

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

◆ bvLeftShift()

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

◆ bvMinusOne()

ExprHandle klee::STPBuilder::bvMinusOne ( unsigned  width)
private

◆ bvOne()

ExprHandle klee::STPBuilder::bvOne ( unsigned  width)
private

◆ bvRightShift()

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

◆ bvSExtConst()

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

◆ bvVarArithRightShift()

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

◆ bvVarLeftShift()

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

◆ bvVarRightShift()

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

◆ bvZero()

ExprHandle klee::STPBuilder::bvZero ( unsigned  width)
private

◆ bvZExtConst()

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

◆ construct() [1/2]

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

Definition at line 122 of file STPBuilder.h.

References construct(), and constructed.

Here is the call graph for this function:

◆ construct() [2/2]

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

Referenced by construct().

Here is the caller graph for this function:

◆ constructActual()

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

◆ constructAShrByConstant()

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

◆ constructMulByConstant()

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

◆ constructSDivByConstant()

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

◆ constructUDivByConstant()

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

◆ eqExpr()

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

◆ extractPartialShiftValue()

ExprHandle klee::STPBuilder::extractPartialShiftValue ( ExprHandle  shift,
unsigned  width,
unsigned &  shiftBits 
)
private

◆ getArrayForUpdate()

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

◆ getFalse()

ExprHandle klee::STPBuilder::getFalse ( )

◆ getInitialArray()

::VCExpr klee::STPBuilder::getInitialArray ( const Array *  os)
private

◆ getInitialRead()

ExprHandle klee::STPBuilder::getInitialRead ( const Array *  os,
unsigned  index 
)

◆ getTrue()

ExprHandle klee::STPBuilder::getTrue ( )

Member Data Documentation

◆ _arr_hash

STPArrayExprHash klee::STPBuilder::_arr_hash
private

Definition at line 74 of file STPBuilder.h.

◆ constructed

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

Definition at line 67 of file STPBuilder.h.

Referenced by construct().

◆ optimizeDivides

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 72 of file STPBuilder.h.

◆ vc

::VC klee::STPBuilder::vc
private

Definition at line 66 of file STPBuilder.h.

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