klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Expr.cpp File Reference
#include "klee/Expr.h"
#include "klee/Config/Version.h"
#include "llvm/ADT/Hashing.h"
#include "llvm/Support/CommandLine.h"
#include "llvm/Support/raw_ostream.h"
#include "klee/Internal/Support/IntEvaluation.h"
#include "klee/util/ExprPPrinter.h"
#include <sstream>
Include dependency graph for Expr.cpp:

Go to the source code of this file.

Macros

#define X(C)   case C: os << #C; break
 
#define CAST_EXPR_CASE(T)
 
#define BINARY_EXPR_CASE(T)
 
#define BCREATE_R(_e_op, _op, partialL, partialR)
 
#define BCREATE(_e_op, _op)
 
#define CMPCREATE(_e_op, _op)
 
#define CMPCREATE_T(_e_op, _op, _reflexive_e_op, partialL, partialR)
 

Functions

void vc_DeleteExpr (void *)
 
static ref< ExprAndExpr_create (Expr *l, Expr *r)
 
static ref< ExprXorExpr_create (Expr *l, Expr *r)
 
static ref< ExprEqExpr_createPartial (Expr *l, const ref< ConstantExpr > &cr)
 
static ref< ExprAndExpr_createPartialR (const ref< ConstantExpr > &cl, Expr *r)
 
static ref< ExprSubExpr_createPartialR (const ref< ConstantExpr > &cl, Expr *r)
 
static ref< ExprXorExpr_createPartialR (const ref< ConstantExpr > &cl, Expr *r)
 
static ref< ExprAddExpr_createPartialR (const ref< ConstantExpr > &cl, Expr *r)
 
static ref< ExprAddExpr_createPartial (Expr *l, const ref< ConstantExpr > &cr)
 
static ref< ExprAddExpr_create (Expr *l, Expr *r)
 
static ref< ExprSubExpr_createPartial (Expr *l, const ref< ConstantExpr > &cr)
 
static ref< ExprSubExpr_create (Expr *l, Expr *r)
 
static ref< ExprMulExpr_createPartialR (const ref< ConstantExpr > &cl, Expr *r)
 
static ref< ExprMulExpr_createPartial (Expr *l, const ref< ConstantExpr > &cr)
 
static ref< ExprMulExpr_create (Expr *l, Expr *r)
 
static ref< ExprAndExpr_createPartial (Expr *l, const ref< ConstantExpr > &cr)
 
static ref< ExprOrExpr_createPartial (Expr *l, const ref< ConstantExpr > &cr)
 
static ref< ExprOrExpr_createPartialR (const ref< ConstantExpr > &cl, Expr *r)
 
static ref< ExprOrExpr_create (Expr *l, Expr *r)
 
static ref< ExprXorExpr_createPartial (Expr *l, const ref< ConstantExpr > &cr)
 
static ref< ExprUDivExpr_create (const ref< Expr > &l, const ref< Expr > &r)
 
static ref< ExprSDivExpr_create (const ref< Expr > &l, const ref< Expr > &r)
 
static ref< ExprURemExpr_create (const ref< Expr > &l, const ref< Expr > &r)
 
static ref< ExprSRemExpr_create (const ref< Expr > &l, const ref< Expr > &r)
 
static ref< ExprShlExpr_create (const ref< Expr > &l, const ref< Expr > &r)
 
static ref< ExprLShrExpr_create (const ref< Expr > &l, const ref< Expr > &r)
 
static ref< ExprAShrExpr_create (const ref< Expr > &l, const ref< Expr > &r)
 
static ref< ExprEqExpr_create (const ref< Expr > &l, const ref< Expr > &r)
 
static ref< ExprTryConstArrayOpt (const ref< ConstantExpr > &cl, ReadExpr *rd)
 
static ref< ExprEqExpr_createPartialR (const ref< ConstantExpr > &cl, Expr *r)
 
static ref< ExprUltExpr_create (const ref< Expr > &l, const ref< Expr > &r)
 
static ref< ExprUleExpr_create (const ref< Expr > &l, const ref< Expr > &r)
 
static ref< ExprSltExpr_create (const ref< Expr > &l, const ref< Expr > &r)
 
static ref< ExprSleExpr_create (const ref< Expr > &l, const ref< Expr > &r)
 

Macro Definition Documentation

#define BCREATE (   _e_op,
  _op 
)
Value:
ref<Expr> _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
assert(l->getWidth()==r->getWidth() && "type mismatch"); \
if (ConstantExpr *cl = dyn_cast<ConstantExpr>(l)) \
if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) \
return cl->_op(cr); \
return _e_op ## _create(l, r); \
}
virtual Width getWidth() const =0

Definition at line 928 of file Expr.cpp.

#define BCREATE_R (   _e_op,
  _op,
  partialL,
  partialR 
)
Value:
ref<Expr> _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
assert(l->getWidth()==r->getWidth() && "type mismatch"); \
if (ConstantExpr *cl = dyn_cast<ConstantExpr>(l)) { \
if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) \
return cl->_op(cr); \
return _e_op ## _createPartialR(cl, r.get()); \
} else if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) { \
return _e_op ## _createPartial(l.get(), cr); \
} \
return _e_op ## _create(l.get(), r.get()); \
}
T * get() const
Definition: Ref.h:69
virtual Width getWidth() const =0

Definition at line 915 of file Expr.cpp.

#define BINARY_EXPR_CASE (   T)
Value:
case T: \
assert(numArgs == 2 && \
args[0].isExpr() && args[1].isExpr() && \
"invalid args array for given opcode"); \
return T ## Expr::create(args[0].expr, args[1].expr); \

Referenced by klee::Expr::createFromKind().

#define CAST_EXPR_CASE (   T)
Value:
case T: \
assert(numArgs == 2 && \
args[0].isExpr() && args[1].isWidth() && \
"invalid args array for given opcode"); \
return T ## Expr::create(args[0].expr, args[1].width); \

Referenced by klee::Expr::createFromKind().

#define CMPCREATE (   _e_op,
  _op 
)
Value:
ref<Expr> _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
assert(l->getWidth()==r->getWidth() && "type mismatch"); \
if (ConstantExpr *cl = dyn_cast<ConstantExpr>(l)) \
if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) \
return cl->_op(cr); \
return _e_op ## _create(l, r); \
}
virtual Width getWidth() const =0

Definition at line 951 of file Expr.cpp.

#define CMPCREATE_T (   _e_op,
  _op,
  _reflexive_e_op,
  partialL,
  partialR 
)
Value:
ref<Expr> _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
assert(l->getWidth()==r->getWidth() && "type mismatch"); \
if (ConstantExpr *cl = dyn_cast<ConstantExpr>(l)) { \
if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) \
return cl->_op(cr); \
return partialR(cl, r.get()); \
} else if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) { \
return partialL(l.get(), cr); \
} else { \
return _e_op ## _create(l.get(), r.get()); \
} \
}
T * get() const
Definition: Ref.h:69
virtual Width getWidth() const =0

Definition at line 960 of file Expr.cpp.

#define X (   C)    case C: os << #C; break

Referenced by klee::Expr::printKind().

Function Documentation

static ref<Expr> AddExpr_create ( Expr l,
Expr r 
)
static

Definition at line 709 of file Expr.cpp.

References klee::Expr::Add, klee::Expr::Bool, klee::Expr::getKid(), klee::Expr::getKind(), klee::Expr::getWidth(), klee::Expr::Sub, and XorExpr_create().

Here is the call graph for this function:

static ref<Expr> AddExpr_createPartial ( Expr l,
const ref< ConstantExpr > &  cr 
)
static

Definition at line 706 of file Expr.cpp.

References AddExpr_createPartialR().

Referenced by SubExpr_createPartial().

Here is the call graph for this function:

Here is the caller graph for this function:

static ref<Expr> AddExpr_createPartialR ( const ref< ConstantExpr > &  cl,
Expr r 
)
static

Definition at line 686 of file Expr.cpp.

References klee::Expr::Add, klee::Expr::Bool, klee::Expr::getKid(), klee::Expr::getKind(), klee::ConstantExpr::getWidth(), klee::ConstantExpr::isZero(), klee::Expr::Sub, and XorExpr_createPartialR().

Referenced by AddExpr_createPartial().

Here is the call graph for this function:

Here is the caller graph for this function:

static ref< Expr > AndExpr_create ( Expr l,
Expr r 
)
static

Definition at line 822 of file Expr.cpp.

static ref<Expr> AndExpr_createPartial ( Expr l,
const ref< ConstantExpr > &  cr 
)
static

Definition at line 810 of file Expr.cpp.

References klee::ConstantExpr::isAllOnes(), and klee::ConstantExpr::isZero().

Referenced by AndExpr_createPartialR().

Here is the call graph for this function:

Here is the caller graph for this function:

static ref< Expr > AndExpr_createPartialR ( const ref< ConstantExpr > &  cl,
Expr r 
)
static

Definition at line 819 of file Expr.cpp.

References AndExpr_createPartial().

Referenced by MulExpr_createPartialR().

Here is the call graph for this function:

Here is the caller graph for this function:

static ref<Expr> AShrExpr_create ( const ref< Expr > &  l,
const ref< Expr > &  r 
)
static

Definition at line 907 of file Expr.cpp.

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

Here is the call graph for this function:

static ref<Expr> EqExpr_create ( const ref< Expr > &  l,
const ref< Expr > &  r 
)
static

Definition at line 975 of file Expr.cpp.

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

Referenced by EqExpr_createPartialR(), and TryConstArrayOpt().

Here is the call graph for this function:

Here is the caller graph for this function:

static ref< Expr > EqExpr_createPartial ( Expr l,
const ref< ConstantExpr > &  cr 
)
static

Definition at line 1092 of file Expr.cpp.

References EqExpr_createPartialR().

Referenced by XorExpr_createPartialR().

Here is the call graph for this function:

Here is the caller graph for this function:

static ref<Expr> LShrExpr_create ( const ref< Expr > &  l,
const ref< Expr > &  r 
)
static

Definition at line 899 of file Expr.cpp.

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

Here is the call graph for this function:

static ref<Expr> MulExpr_create ( Expr l,
Expr r 
)
static

Definition at line 800 of file Expr.cpp.

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

Here is the call graph for this function:

static ref<Expr> MulExpr_createPartial ( Expr l,
const ref< ConstantExpr > &  cr 
)
static

Definition at line 797 of file Expr.cpp.

References MulExpr_createPartialR().

Here is the call graph for this function:

static ref<Expr> MulExpr_createPartialR ( const ref< ConstantExpr > &  cl,
Expr r 
)
static

Definition at line 784 of file Expr.cpp.

References AndExpr_createPartialR(), klee::Expr::Bool, klee::ConstantExpr::getWidth(), klee::ConstantExpr::isOne(), and klee::ConstantExpr::isZero().

Referenced by MulExpr_createPartial().

Here is the call graph for this function:

Here is the caller graph for this function:

static ref<Expr> OrExpr_create ( Expr l,
Expr r 
)
static

Definition at line 838 of file Expr.cpp.

static ref<Expr> OrExpr_createPartial ( Expr l,
const ref< ConstantExpr > &  cr 
)
static

Definition at line 826 of file Expr.cpp.

References klee::ConstantExpr::isAllOnes(), and klee::ConstantExpr::isZero().

Referenced by OrExpr_createPartialR().

Here is the call graph for this function:

Here is the caller graph for this function:

static ref<Expr> OrExpr_createPartialR ( const ref< ConstantExpr > &  cl,
Expr r 
)
static

Definition at line 835 of file Expr.cpp.

References OrExpr_createPartial().

Here is the call graph for this function:

static ref<Expr> SDivExpr_create ( const ref< Expr > &  l,
const ref< Expr > &  r 
)
static

Definition at line 867 of file Expr.cpp.

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

Here is the call graph for this function:

static ref<Expr> ShlExpr_create ( const ref< Expr > &  l,
const ref< Expr > &  r 
)
static

Definition at line 891 of file Expr.cpp.

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

Here is the call graph for this function:

static ref<Expr> SleExpr_create ( const ref< Expr > &  l,
const ref< Expr > &  r 
)
static

Definition at line 1140 of file Expr.cpp.

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

Here is the call graph for this function:

static ref<Expr> SltExpr_create ( const ref< Expr > &  l,
const ref< Expr > &  r 
)
static

Definition at line 1132 of file Expr.cpp.

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

Here is the call graph for this function:

static ref<Expr> SRemExpr_create ( const ref< Expr > &  l,
const ref< Expr > &  r 
)
static

Definition at line 883 of file Expr.cpp.

References klee::Expr::Bool, klee::ConstantExpr::create(), and klee::Expr::getWidth().

Here is the call graph for this function:

static ref<Expr> SubExpr_create ( Expr l,
Expr r 
)
static
static ref<Expr> SubExpr_createPartial ( Expr l,
const ref< ConstantExpr > &  cr 
)
static

Definition at line 752 of file Expr.cpp.

References AddExpr_createPartial(), klee::ConstantExpr::alloc(), and klee::ConstantExpr::getWidth().

Here is the call graph for this function:

static ref< Expr > SubExpr_createPartialR ( const ref< ConstantExpr > &  cl,
Expr r 
)
static

Definition at line 734 of file Expr.cpp.

References klee::Expr::Add, klee::Expr::Bool, klee::Expr::getKid(), klee::Expr::getKind(), klee::ConstantExpr::getWidth(), klee::Expr::Sub, and XorExpr_createPartialR().

Here is the call graph for this function:

static ref<Expr> TryConstArrayOpt ( const ref< ConstantExpr > &  cl,
ReadExpr rd 
)
static

Tries to optimize EqExpr cl == rd, where cl is a ConstantExpr and rd a ReadExpr. If rd is a read into an all-constant array, returns a disjunction of equalities on the index. Otherwise, returns the initial equality expression.

Definition at line 988 of file Expr.cpp.

References klee::ConstantExpr::alloc(), klee::Expr::Bool, klee::Array::constantValues, EqExpr_create(), klee::UpdateList::getSize(), klee::Expr::getWidth(), klee::ReadExpr::index, klee::Array::isSymbolicArray(), klee::UpdateList::root, klee::Array::size, and klee::ReadExpr::updates.

Referenced by EqExpr_createPartialR().

Here is the call graph for this function:

Here is the caller graph for this function:

static ref<Expr> UDivExpr_create ( const ref< Expr > &  l,
const ref< Expr > &  r 
)
static

Definition at line 859 of file Expr.cpp.

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

Here is the call graph for this function:

static ref<Expr> UleExpr_create ( const ref< Expr > &  l,
const ref< Expr > &  r 
)
static

Definition at line 1124 of file Expr.cpp.

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

Here is the call graph for this function:

static ref<Expr> UltExpr_create ( const ref< Expr > &  l,
const ref< Expr > &  r 
)
static

Definition at line 1115 of file Expr.cpp.

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

Here is the call graph for this function:

static ref<Expr> URemExpr_create ( const ref< Expr > &  l,
const ref< Expr > &  r 
)
static

Definition at line 875 of file Expr.cpp.

References klee::Expr::Bool, klee::ConstantExpr::create(), and klee::Expr::getWidth().

Here is the call graph for this function:

void vc_DeleteExpr ( void *  )
static ref< Expr > XorExpr_create ( Expr l,
Expr r 
)
static

Definition at line 855 of file Expr.cpp.

Referenced by AddExpr_create(), and SubExpr_create().

Here is the caller graph for this function:

static ref<Expr> XorExpr_createPartial ( Expr l,
const ref< ConstantExpr > &  cr 
)
static

Definition at line 852 of file Expr.cpp.

References XorExpr_createPartialR().

Here is the call graph for this function:

static ref< Expr > XorExpr_createPartialR ( const ref< ConstantExpr > &  cl,
Expr r 
)
static

Definition at line 842 of file Expr.cpp.

References klee::Expr::Bool, klee::ConstantExpr::create(), EqExpr_createPartial(), klee::ConstantExpr::getWidth(), and klee::ConstantExpr::isZero().

Referenced by AddExpr_createPartialR(), SubExpr_createPartialR(), and XorExpr_createPartial().

Here is the call graph for this function:

Here is the caller graph for this function: