#include "klee/Expr/Expr.h"
#include "klee/Config/Version.h"
#include "klee/Expr/ExprPPrinter.h"
#include "klee/Support/OptionCategories.h"
#include "klee/Support/IntEvaluation.h"
#include "llvm/ADT/Hashing.h"
#include "llvm/ADT/StringExtras.h"
#include "llvm/Support/CommandLine.h"
#include "llvm/Support/raw_ostream.h"
#include <sstream>

Include dependency graph for Expr.cpp:

Namespaces
namespace	klee

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
llvm::cl::OptionCategory	klee::ExprCat ("Expression building and printing options", "These options impact the way expressions are build and printed.")

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Macro Definition Documentation

◆ BCREATE

#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);                                    \
}

Definition at line 993 of file Expr.cpp.

◆ BCREATE_R

#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());                            \
}

Definition at line 980 of file Expr.cpp.

◆ BINARY_EXPR_CASE

#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); \

◆ CAST_EXPR_CASE

#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); \

◆ CMPCREATE

#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);                                        \
}

Definition at line 1016 of file Expr.cpp.

◆ CMPCREATE_T

#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());                         \
  }                                                                    \
}

Definition at line 1025 of file Expr.cpp.

◆ X

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

Function Documentation

◆ AddExpr_create()

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

static

Definition at line 774 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:

◆ AddExpr_createPartial()

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

static

Definition at line 771 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:

◆ AddExpr_createPartialR()

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

static

Definition at line 751 of file Expr.cpp.

References klee::Expr::Add, klee::Expr::Bool, klee::Expr::getKid(), klee::Expr::getKind(), 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:

◆ AndExpr_create()

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

static

Definition at line 887 of file Expr.cpp.

◆ AndExpr_createPartial()

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

static

Definition at line 875 of file Expr.cpp.

Referenced by AndExpr_createPartialR().

Here is the caller graph for this function:

◆ AndExpr_createPartialR()

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

static

Definition at line 884 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:

◆ AShrExpr_create()

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

static

Definition at line 972 of file Expr.cpp.

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

Here is the call graph for this function:

◆ EqExpr_create()

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

static

Definition at line 1040 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:

◆ EqExpr_createPartial()

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

static

Definition at line 1157 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:

◆ EqExpr_createPartialR()

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

static

Definition at line 1080 of file Expr.cpp.

References klee::Expr::Add, klee::Expr::Bool, klee::ConstantExpr::create(), klee::Expr::createIsZero(), klee::Expr::Eq, EqExpr_create(), EqExpr_createPartialR(), klee::Expr::getKind(), klee::Expr::Or, klee::Expr::Read, klee::Expr::SExt, klee::Expr::Sub, klee::floats::trunc(), TryConstArrayOpt(), and klee::Expr::ZExt.

Referenced by EqExpr_createPartial(), and EqExpr_createPartialR().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ LShrExpr_create()

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

static

Definition at line 964 of file Expr.cpp.

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

Here is the call graph for this function:

◆ MulExpr_create()

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

static

Definition at line 865 of file Expr.cpp.

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

Here is the call graph for this function:

◆ MulExpr_createPartial()

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

static

Definition at line 862 of file Expr.cpp.

References MulExpr_createPartialR().

Here is the call graph for this function:

◆ MulExpr_createPartialR()

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

static

Definition at line 849 of file Expr.cpp.

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

Referenced by MulExpr_createPartial().

Here is the call graph for this function:

Here is the caller graph for this function:

◆ OrExpr_create()

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

static

Definition at line 903 of file Expr.cpp.

◆ OrExpr_createPartial()

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

static

Definition at line 891 of file Expr.cpp.

Referenced by OrExpr_createPartialR().

Here is the caller graph for this function:

◆ OrExpr_createPartialR()

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

static

Definition at line 900 of file Expr.cpp.

References OrExpr_createPartial().

Here is the call graph for this function:

◆ SDivExpr_create()

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

static

Definition at line 932 of file Expr.cpp.

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

Here is the call graph for this function:

◆ ShlExpr_create()

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

static

Definition at line 956 of file Expr.cpp.

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

Here is the call graph for this function:

◆ SleExpr_create()

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

static

Definition at line 1205 of file Expr.cpp.

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

Here is the call graph for this function:

◆ SltExpr_create()

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

static

Definition at line 1197 of file Expr.cpp.

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

Here is the call graph for this function:

◆ SRemExpr_create()

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

static

Definition at line 948 of file Expr.cpp.

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

Here is the call graph for this function:

◆ SubExpr_create()

static ref< Expr > SubExpr_create	(	Expr *	l,
		Expr *	r
	)

static

Definition at line 822 of file Expr.cpp.

References klee::Expr::Add, klee::ConstantExpr::alloc(), 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:

◆ SubExpr_createPartial()

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

static

Definition at line 817 of file Expr.cpp.

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

Here is the call graph for this function:

◆ SubExpr_createPartialR()

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

static

Definition at line 799 of file Expr.cpp.

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

Here is the call graph for this function:

◆ TryConstArrayOpt()

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 1053 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.