//===-- Expr.cpp ----------------------------------------------------------===// // // The KLEE Symbolic Virtual Machine // // This file is distributed under the University of Illinois Open Source // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// #include "klee/Expr.h" #include "klee/Machine.h" #include "llvm/Type.h" #include "llvm/DerivedTypes.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/Streams.h" // FIXME: We shouldn't need this once fast constant support moves into // Core. If we need to do arithmetic, we probably want to use APInt. #include "klee/Internal/Support/IntEvaluation.h" #include "klee/util/ExprPPrinter.h" #include using namespace klee; using namespace llvm; namespace { cl::opt ConstArrayOpt("const-array-opt", cl::init(false), cl::desc("Enable various optimizations involving all-constant arrays.")); } /***/ unsigned Expr::count = 0; ref Expr::createTempRead(const Array *array, Expr::Width w) { UpdateList ul(array, 0); switch (w) { default: assert(0 && "invalid width"); case Expr::Bool: return ZExtExpr::create(ReadExpr::create(ul, ConstantExpr::alloc(0,kMachinePointerType)), Expr::Bool); case Expr::Int8: return ReadExpr::create(ul, ConstantExpr::alloc(0,kMachinePointerType)); case Expr::Int16: return ConcatExpr::create(ReadExpr::create(ul, ConstantExpr::alloc(1,kMachinePointerType)), ReadExpr::create(ul, ConstantExpr::alloc(0,kMachinePointerType))); case Expr::Int32: return ConcatExpr::create4(ReadExpr::create(ul, ConstantExpr::alloc(3,kMachinePointerType)), ReadExpr::create(ul, ConstantExpr::alloc(2,kMachinePointerType)), ReadExpr::create(ul, ConstantExpr::alloc(1,kMachinePointerType)), ReadExpr::create(ul, ConstantExpr::alloc(0,kMachinePointerType))); case Expr::Int64: return ConcatExpr::create8(ReadExpr::create(ul, ConstantExpr::alloc(7,kMachinePointerType)), ReadExpr::create(ul, ConstantExpr::alloc(6,kMachinePointerType)), ReadExpr::create(ul, ConstantExpr::alloc(5,kMachinePointerType)), ReadExpr::create(ul, ConstantExpr::alloc(4,kMachinePointerType)), ReadExpr::create(ul, ConstantExpr::alloc(3,kMachinePointerType)), ReadExpr::create(ul, ConstantExpr::alloc(2,kMachinePointerType)), ReadExpr::create(ul, ConstantExpr::alloc(1,kMachinePointerType)), ReadExpr::create(ul, ConstantExpr::alloc(0,kMachinePointerType))); } } // returns 0 if b is structurally equal to *this int Expr::compare(const Expr &b) const { if (this == &b) return 0; Kind ak = getKind(), bk = b.getKind(); if (ak!=bk) return (ak < bk) ? -1 : 1; if (hashValue != b.hashValue) return (hashValue < b.hashValue) ? -1 : 1; if (int res = compareContents(b)) return res; unsigned aN = getNumKids(); for (unsigned i=0; ihash() * Expr::MAGIC_HASH_CONSTANT; } hashValue = res; return hashValue; } unsigned ConstantExpr::computeHash() { hashValue = value.getHashValue() ^ (getWidth() * MAGIC_HASH_CONSTANT); return hashValue; } unsigned CastExpr::computeHash() { unsigned res = getWidth() * Expr::MAGIC_HASH_CONSTANT; hashValue = res ^ src->hash() * Expr::MAGIC_HASH_CONSTANT; return hashValue; } unsigned ExtractExpr::computeHash() { unsigned res = offset * Expr::MAGIC_HASH_CONSTANT; res ^= getWidth() * Expr::MAGIC_HASH_CONSTANT; hashValue = res ^ expr->hash() * Expr::MAGIC_HASH_CONSTANT; return hashValue; } unsigned ReadExpr::computeHash() { unsigned res = index->hash() * Expr::MAGIC_HASH_CONSTANT; res ^= updates.hash(); hashValue = res; return hashValue; } ref Expr::createFromKind(Kind k, std::vector args) { unsigned numArgs = args.size(); (void) numArgs; switch(k) { case Constant: case Extract: case Read: default: assert(0 && "invalid kind"); case NotOptimized: assert(numArgs == 1 && args[0].isExpr() && "invalid args array for given opcode"); return NotOptimizedExpr::create(args[0].expr); case Select: assert(numArgs == 3 && args[0].isExpr() && args[1].isExpr() && args[2].isExpr() && "invalid args array for Select opcode"); return SelectExpr::create(args[0].expr, args[1].expr, args[2].expr); case Concat: { assert(numArgs == 2 && args[0].isExpr() && args[1].isExpr() && "invalid args array for Concat opcode"); return ConcatExpr::create(args[0].expr, args[1].expr); } #define CAST_EXPR_CASE(T) \ 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); \ #define BINARY_EXPR_CASE(T) \ 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(ZExt); CAST_EXPR_CASE(SExt); BINARY_EXPR_CASE(Add); BINARY_EXPR_CASE(Sub); BINARY_EXPR_CASE(Mul); BINARY_EXPR_CASE(UDiv); BINARY_EXPR_CASE(SDiv); BINARY_EXPR_CASE(URem); BINARY_EXPR_CASE(SRem); BINARY_EXPR_CASE(And); BINARY_EXPR_CASE(Or); BINARY_EXPR_CASE(Xor); BINARY_EXPR_CASE(Shl); BINARY_EXPR_CASE(LShr); BINARY_EXPR_CASE(AShr); BINARY_EXPR_CASE(Eq); BINARY_EXPR_CASE(Ne); BINARY_EXPR_CASE(Ult); BINARY_EXPR_CASE(Ule); BINARY_EXPR_CASE(Ugt); BINARY_EXPR_CASE(Uge); BINARY_EXPR_CASE(Slt); BINARY_EXPR_CASE(Sle); BINARY_EXPR_CASE(Sgt); BINARY_EXPR_CASE(Sge); } } void Expr::printWidth(std::ostream &os, Width width) { switch(width) { case Expr::Bool: os << "Expr::Bool"; break; case Expr::Int8: os << "Expr::Int8"; break; case Expr::Int16: os << "Expr::Int16"; break; case Expr::Int32: os << "Expr::Int32"; break; case Expr::Int64: os << "Expr::Int64"; break; default: os << ""; } } Expr::Width Expr::getWidthForLLVMType(const llvm::Type *t) { switch (t->getTypeID()) { case llvm::Type::IntegerTyID: return cast(t)->getBitWidth(); case llvm::Type::FloatTyID: return Expr::Int32; case llvm::Type::DoubleTyID: return Expr::Int64; case llvm::Type::X86_FP80TyID: return 80; case llvm::Type::PointerTyID: return kMachinePointerType; default: cerr << "non-primitive type argument to Expr::getTypeForLLVMType()\n"; abort(); } } ref Expr::createImplies(ref hyp, ref conc) { return OrExpr::create(Expr::createNot(hyp), conc); } ref Expr::createIsZero(ref e) { return EqExpr::create(e, ConstantExpr::create(0, e->getWidth())); } ref Expr::createCoerceToPointerType(ref e) { return ZExtExpr::create(e, kMachinePointerType); } ref Expr::createNot(ref e) { return createIsZero(e); } ref Expr::createPointer(uint64_t v) { return ConstantExpr::create(v, kMachinePointerType); } void Expr::print(std::ostream &os) const { ExprPPrinter::printSingleExpr(os, (Expr*)this); } /***/ ref ConstantExpr::fromMemory(void *address, Width width) { switch (width) { default: assert(0 && "invalid type"); case Expr::Bool: return ConstantExpr::create(*(( uint8_t*) address), width); case Expr::Int8: return ConstantExpr::create(*(( uint8_t*) address), width); case Expr::Int16: return ConstantExpr::create(*((uint16_t*) address), width); case Expr::Int32: return ConstantExpr::create(*((uint32_t*) address), width); case Expr::Int64: return ConstantExpr::create(*((uint64_t*) address), width); // FIXME: Should support long double, at least. } } void ConstantExpr::toMemory(void *address) { switch (getWidth()) { default: assert(0 && "invalid type"); case Expr::Bool: *(( uint8_t*) address) = getZExtValue(1); break; case Expr::Int8: *(( uint8_t*) address) = getZExtValue(8); break; case Expr::Int16: *((uint16_t*) address) = getZExtValue(16); break; case Expr::Int32: *((uint32_t*) address) = getZExtValue(32); break; case Expr::Int64: *((uint64_t*) address) = getZExtValue(64); break; // FIXME: Should support long double, at least. } } void ConstantExpr::toString(std::string &Res) const { Res = value.toString(10, false); } ref ConstantExpr::Concat(const ref &RHS) { Expr::Width W = getWidth() + RHS->getWidth(); APInt Tmp(value); Tmp.zext(W); Tmp <<= RHS->getWidth(); Tmp |= APInt(RHS->value).zext(W); return ConstantExpr::alloc(Tmp); } ref ConstantExpr::Extract(unsigned Offset, Width W) { return ConstantExpr::alloc(APInt(value.ashr(Offset)).zextOrTrunc(W)); } ref ConstantExpr::ZExt(Width W) { return ConstantExpr::alloc(APInt(value).zextOrTrunc(W)); } ref ConstantExpr::SExt(Width W) { return ConstantExpr::alloc(APInt(value).sextOrTrunc(W)); } ref ConstantExpr::Add(const ref &RHS) { return ConstantExpr::alloc(value + RHS->value); } ref ConstantExpr::Neg() { return ConstantExpr::alloc(-value); } ref ConstantExpr::Sub(const ref &RHS) { return ConstantExpr::alloc(value - RHS->value); } ref ConstantExpr::Mul(const ref &RHS) { return ConstantExpr::alloc(value * RHS->value); } ref ConstantExpr::UDiv(const ref &RHS) { return ConstantExpr::alloc(value.udiv(RHS->value)); } ref ConstantExpr::SDiv(const ref &RHS) { return ConstantExpr::alloc(value.sdiv(RHS->value)); } ref ConstantExpr::URem(const ref &RHS) { return ConstantExpr::alloc(value.urem(RHS->value)); } ref ConstantExpr::SRem(const ref &RHS) { return ConstantExpr::alloc(value.srem(RHS->value)); } ref ConstantExpr::And(const ref &RHS) { return ConstantExpr::alloc(value & RHS->value); } ref ConstantExpr::Or(const ref &RHS) { return ConstantExpr::alloc(value | RHS->value); } ref ConstantExpr::Xor(const ref &RHS) { return ConstantExpr::alloc(value ^ RHS->value); } ref ConstantExpr::Shl(const ref &RHS) { return ConstantExpr::alloc(value.shl(RHS->value)); } ref ConstantExpr::LShr(const ref &RHS) { return ConstantExpr::alloc(value.lshr(RHS->value)); } ref ConstantExpr::AShr(const ref &RHS) { return ConstantExpr::alloc(value.ashr(RHS->value)); } ref ConstantExpr::Not() { return ConstantExpr::alloc(value == 0, Expr::Bool); } ref ConstantExpr::Eq(const ref &RHS) { return ConstantExpr::alloc(value == RHS->value, Expr::Bool); } ref ConstantExpr::Ne(const ref &RHS) { return ConstantExpr::alloc(value != RHS->value, Expr::Bool); } ref ConstantExpr::Ult(const ref &RHS) { return ConstantExpr::alloc(value.ult(RHS->value), Expr::Bool); } ref ConstantExpr::Ule(const ref &RHS) { return ConstantExpr::alloc(value.ule(RHS->value), Expr::Bool); } ref ConstantExpr::Ugt(const ref &RHS) { return ConstantExpr::alloc(value.ugt(RHS->value), Expr::Bool); } ref ConstantExpr::Uge(const ref &RHS) { return ConstantExpr::alloc(value.uge(RHS->value), Expr::Bool); } ref ConstantExpr::Slt(const ref &RHS) { return ConstantExpr::alloc(value.slt(RHS->value), Expr::Bool); } ref ConstantExpr::Sle(const ref &RHS) { return ConstantExpr::alloc(value.sle(RHS->value), Expr::Bool); } ref ConstantExpr::Sgt(const ref &RHS) { return ConstantExpr::alloc(value.sgt(RHS->value), Expr::Bool); } ref ConstantExpr::Sge(const ref &RHS) { return ConstantExpr::alloc(value.sge(RHS->value), Expr::Bool); } /***/ ref NotOptimizedExpr::create(ref src) { return NotOptimizedExpr::alloc(src); } /***/ extern "C" void vc_DeleteExpr(void*); Array::~Array() { // FIXME: This shouldn't be necessary. if (stpInitialArray) { ::vc_DeleteExpr(stpInitialArray); stpInitialArray = 0; } } /***/ ref ReadExpr::create(const UpdateList &ul, ref index) { // rollback index when possible... // XXX this doesn't really belong here... there are basically two // cases, one is rebuild, where we want to optimistically try various // optimizations when the index has changed, and the other is // initial creation, where we expect the ObjectState to have constructed // a smart UpdateList so it is not worth rescanning. const UpdateNode *un = ul.head; for (; un; un=un->next) { ref cond = EqExpr::create(index, un->index); if (ConstantExpr *CE = dyn_cast(cond)) { if (CE->isTrue()) return un->value; } else { break; } } return ReadExpr::alloc(ul, index); } int ReadExpr::compareContents(const Expr &b) const { return updates.compare(static_cast(b).updates); } ref SelectExpr::create(ref c, ref t, ref f) { Expr::Width kt = t->getWidth(); assert(c->getWidth()==Bool && "type mismatch"); assert(kt==f->getWidth() && "type mismatch"); if (ConstantExpr *CE = dyn_cast(c)) { return CE->isTrue() ? t : f; } else if (t==f) { return t; } else if (kt==Expr::Bool) { // c ? t : f <=> (c and t) or (not c and f) if (ConstantExpr *CE = dyn_cast(t)) { if (CE->isTrue()) { return OrExpr::create(c, f); } else { return AndExpr::create(Expr::createNot(c), f); } } else if (ConstantExpr *CE = dyn_cast(f)) { if (CE->isTrue()) { return OrExpr::create(Expr::createNot(c), t); } else { return AndExpr::create(c, t); } } } return SelectExpr::alloc(c, t, f); } /***/ ref ConcatExpr::create(const ref &l, const ref &r) { Expr::Width w = l->getWidth() + r->getWidth(); // Fold concatenation of constants. // // FIXME: concat 0 x -> zext x ? if (ConstantExpr *lCE = dyn_cast(l)) if (ConstantExpr *rCE = dyn_cast(r)) return lCE->Concat(rCE); // Merge contiguous Extracts if (ExtractExpr *ee_left = dyn_cast(l)) { if (ExtractExpr *ee_right = dyn_cast(r)) { if (ee_left->expr == ee_right->expr && ee_right->offset + ee_right->width == ee_left->offset) { return ExtractExpr::create(ee_left->expr, ee_right->offset, w); } } } return ConcatExpr::alloc(l, r); } /// Shortcut to concat N kids. The chain returned is unbalanced to the right ref ConcatExpr::createN(unsigned n_kids, const ref kids[]) { assert(n_kids > 0); if (n_kids == 1) return kids[0]; ref r = ConcatExpr::create(kids[n_kids-2], kids[n_kids-1]); for (int i=n_kids-3; i>=0; i--) r = ConcatExpr::create(kids[i], r); return r; } /// Shortcut to concat 4 kids. The chain returned is unbalanced to the right ref ConcatExpr::create4(const ref &kid1, const ref &kid2, const ref &kid3, const ref &kid4) { return ConcatExpr::create(kid1, ConcatExpr::create(kid2, ConcatExpr::create(kid3, kid4))); } /// Shortcut to concat 8 kids. The chain returned is unbalanced to the right ref ConcatExpr::create8(const ref &kid1, const ref &kid2, const ref &kid3, const ref &kid4, const ref &kid5, const ref &kid6, const ref &kid7, const ref &kid8) { return ConcatExpr::create(kid1, ConcatExpr::create(kid2, ConcatExpr::create(kid3, ConcatExpr::create(kid4, ConcatExpr::create4(kid5, kid6, kid7, kid8))))); } /***/ ref ExtractExpr::create(ref expr, unsigned off, Width w) { unsigned kw = expr->getWidth(); assert(w > 0 && off + w <= kw && "invalid extract"); if (w == kw) { return expr; } else if (ConstantExpr *CE = dyn_cast(expr)) { return CE->Extract(off, w); } else { // Extract(Concat) if (ConcatExpr *ce = dyn_cast(expr)) { // if the extract skips the right side of the concat if (off >= ce->getRight()->getWidth()) return ExtractExpr::create(ce->getLeft(), off - ce->getRight()->getWidth(), w); // if the extract skips the left side of the concat if (off + w <= ce->getRight()->getWidth()) return ExtractExpr::create(ce->getRight(), off, w); // E(C(x,y)) = C(E(x), E(y)) return ConcatExpr::create(ExtractExpr::create(ce->getKid(0), 0, w - ce->getKid(1)->getWidth() + off), ExtractExpr::create(ce->getKid(1), off, ce->getKid(1)->getWidth() - off)); } } return ExtractExpr::alloc(expr, off, w); } /***/ ref ZExtExpr::create(const ref &e, Width w) { unsigned kBits = e->getWidth(); if (w == kBits) { return e; } else if (w < kBits) { // trunc return ExtractExpr::create(e, 0, w); } else if (ConstantExpr *CE = dyn_cast(e)) { return CE->ZExt(w); } else { return ZExtExpr::alloc(e, w); } } ref SExtExpr::create(const ref &e, Width w) { unsigned kBits = e->getWidth(); if (w == kBits) { return e; } else if (w < kBits) { // trunc return ExtractExpr::create(e, 0, w); } else if (ConstantExpr *CE = dyn_cast(e)) { return CE->SExt(w); } else { return SExtExpr::alloc(e, w); } } /***/ static ref AndExpr_create(Expr *l, Expr *r); static ref XorExpr_create(Expr *l, Expr *r); static ref EqExpr_createPartial(Expr *l, const ref &cr); static ref AndExpr_createPartialR(const ref &cl, Expr *r); static ref SubExpr_createPartialR(const ref &cl, Expr *r); static ref XorExpr_createPartialR(const ref &cl, Expr *r); static ref AddExpr_createPartialR(const ref &cl, Expr *r) { Expr::Width type = cl->getWidth(); if (type==Expr::Bool) { return XorExpr_createPartialR(cl, r); } else if (cl->isZero()) { return r; } else { Expr::Kind rk = r->getKind(); if (rk==Expr::Add && isa(r->getKid(0))) { // A + (B+c) == (A+B) + c return AddExpr::create(AddExpr::create(cl, r->getKid(0)), r->getKid(1)); } else if (rk==Expr::Sub && isa(r->getKid(0))) { // A + (B-c) == (A+B) - c return SubExpr::create(AddExpr::create(cl, r->getKid(0)), r->getKid(1)); } else { return AddExpr::alloc(cl, r); } } } static ref AddExpr_createPartial(Expr *l, const ref &cr) { return AddExpr_createPartialR(cr, l); } static ref AddExpr_create(Expr *l, Expr *r) { Expr::Width type = l->getWidth(); if (type == Expr::Bool) { return XorExpr_create(l, r); } else { Expr::Kind lk = l->getKind(), rk = r->getKind(); if (lk==Expr::Add && isa(l->getKid(0))) { // (k+a)+b = k+(a+b) return AddExpr::create(l->getKid(0), AddExpr::create(l->getKid(1), r)); } else if (lk==Expr::Sub && isa(l->getKid(0))) { // (k-a)+b = k+(b-a) return AddExpr::create(l->getKid(0), SubExpr::create(r, l->getKid(1))); } else if (rk==Expr::Add && isa(r->getKid(0))) { // a + (k+b) = k+(a+b) return AddExpr::create(r->getKid(0), AddExpr::create(l, r->getKid(1))); } else if (rk==Expr::Sub && isa(r->getKid(0))) { // a + (k-b) = k+(a-b) return AddExpr::create(r->getKid(0), SubExpr::create(l, r->getKid(1))); } else { return AddExpr::alloc(l, r); } } } static ref SubExpr_createPartialR(const ref &cl, Expr *r) { Expr::Width type = cl->getWidth(); if (type==Expr::Bool) { return XorExpr_createPartialR(cl, r); } else { Expr::Kind rk = r->getKind(); if (rk==Expr::Add && isa(r->getKid(0))) { // A - (B+c) == (A-B) - c return SubExpr::create(SubExpr::create(cl, r->getKid(0)), r->getKid(1)); } else if (rk==Expr::Sub && isa(r->getKid(0))) { // A - (B-c) == (A-B) + c return AddExpr::create(SubExpr::create(cl, r->getKid(0)), r->getKid(1)); } else { return SubExpr::alloc(cl, r); } } } static ref SubExpr_createPartial(Expr *l, const ref &cr) { // l - c => l + (-c) return AddExpr_createPartial(l, ConstantExpr::alloc(0, cr->getWidth())->Sub(cr)); } static ref SubExpr_create(Expr *l, Expr *r) { Expr::Width type = l->getWidth(); if (type == Expr::Bool) { return XorExpr_create(l, r); } else if (*l==*r) { return ConstantExpr::alloc(0, type); } else { Expr::Kind lk = l->getKind(), rk = r->getKind(); if (lk==Expr::Add && isa(l->getKid(0))) { // (k+a)-b = k+(a-b) return AddExpr::create(l->getKid(0), SubExpr::create(l->getKid(1), r)); } else if (lk==Expr::Sub && isa(l->getKid(0))) { // (k-a)-b = k-(a+b) return SubExpr::create(l->getKid(0), AddExpr::create(l->getKid(1), r)); } else if (rk==Expr::Add && isa(r->getKid(0))) { // a - (k+b) = (a-c) - k return SubExpr::create(SubExpr::create(l, r->getKid(1)), r->getKid(0)); } else if (rk==Expr::Sub && isa(r->getKid(0))) { // a - (k-b) = (a+b) - k return SubExpr::create(AddExpr::create(l, r->getKid(1)), r->getKid(0)); } else { return SubExpr::alloc(l, r); } } } static ref MulExpr_createPartialR(const ref &cl, Expr *r) { Expr::Width type = cl->getWidth(); if (type == Expr::Bool) { return AndExpr_createPartialR(cl, r); } else if (cl->isOne()) { return r; } else if (cl->isZero()) { return cl; } else { return MulExpr::alloc(cl, r); } } static ref MulExpr_createPartial(Expr *l, const ref &cr) { return MulExpr_createPartialR(cr, l); } static ref MulExpr_create(Expr *l, Expr *r) { Expr::Width type = l->getWidth(); if (type == Expr::Bool) { return AndExpr::alloc(l, r); } else { return MulExpr::alloc(l, r); } } static ref AndExpr_createPartial(Expr *l, const ref &cr) { if (cr->isAllOnes()) { return l; } else if (cr->isZero()) { return cr; } else { return AndExpr::alloc(l, cr); } } static ref AndExpr_createPartialR(const ref &cl, Expr *r) { return AndExpr_createPartial(r, cl); } static ref AndExpr_create(Expr *l, Expr *r) { return AndExpr::alloc(l, r); } static ref OrExpr_createPartial(Expr *l, const ref &cr) { if (cr->isAllOnes()) { return cr; } else if (cr->isZero()) { return l; } else { return OrExpr::alloc(l, cr); } } static ref OrExpr_createPartialR(const ref &cl, Expr *r) { return OrExpr_createPartial(r, cl); } static ref OrExpr_create(Expr *l, Expr *r) { return OrExpr::alloc(l, r); } static ref XorExpr_createPartialR(const ref &cl, Expr *r) { if (cl->isZero()) { return r; } else if (cl->getWidth() == Expr::Bool) { return EqExpr_createPartial(r, ConstantExpr::create(0, Expr::Bool)); } else { return XorExpr::alloc(cl, r); } } static ref XorExpr_createPartial(Expr *l, const ref &cr) { return XorExpr_createPartialR(cr, l); } static ref XorExpr_create(Expr *l, Expr *r) { return XorExpr::alloc(l, r); } static ref UDivExpr_create(const ref &l, const ref &r) { if (l->getWidth() == Expr::Bool) { // r must be 1 return l; } else{ return UDivExpr::alloc(l, r); } } static ref SDivExpr_create(const ref &l, const ref &r) { if (l->getWidth() == Expr::Bool) { // r must be 1 return l; } else{ return SDivExpr::alloc(l, r); } } static ref URemExpr_create(const ref &l, const ref &r) { if (l->getWidth() == Expr::Bool) { // r must be 1 return ConstantExpr::create(0, Expr::Bool); } else{ return URemExpr::alloc(l, r); } } static ref SRemExpr_create(const ref &l, const ref &r) { if (l->getWidth() == Expr::Bool) { // r must be 1 return ConstantExpr::create(0, Expr::Bool); } else{ return SRemExpr::alloc(l, r); } } static ref ShlExpr_create(const ref &l, const ref &r) { if (l->getWidth() == Expr::Bool) { // l & !r return AndExpr::create(l, Expr::createNot(r)); } else{ return ShlExpr::alloc(l, r); } } static ref LShrExpr_create(const ref &l, const ref &r) { if (l->getWidth() == Expr::Bool) { // l & !r return AndExpr::create(l, Expr::createNot(r)); } else{ return LShrExpr::alloc(l, r); } } static ref AShrExpr_create(const ref &l, const ref &r) { if (l->getWidth() == Expr::Bool) { // l return l; } else{ return AShrExpr::alloc(l, r); } } #define BCREATE_R(_e_op, _op, partialL, partialR) \ ref _e_op ::create(const ref &l, const ref &r) { \ assert(l->getWidth()==r->getWidth() && "type mismatch"); \ if (ConstantExpr *cl = dyn_cast(l)) { \ if (ConstantExpr *cr = dyn_cast(r)) \ return cl->_op(cr); \ return _e_op ## _createPartialR(cl, r.get()); \ } else if (ConstantExpr *cr = dyn_cast(r)) { \ return _e_op ## _createPartial(l.get(), cr); \ } \ return _e_op ## _create(l.get(), r.get()); \ } #define BCREATE(_e_op, _op) \ ref _e_op ::create(const ref &l, const ref &r) { \ assert(l->getWidth()==r->getWidth() && "type mismatch"); \ if (ConstantExpr *cl = dyn_cast(l)) \ if (ConstantExpr *cr = dyn_cast(r)) \ return cl->_op(cr); \ return _e_op ## _create(l, r); \ } BCREATE_R(AddExpr, Add, AddExpr_createPartial, AddExpr_createPartialR) BCREATE_R(SubExpr, Sub, SubExpr_createPartial, SubExpr_createPartialR) BCREATE_R(MulExpr, Mul, MulExpr_createPartial, MulExpr_createPartialR) BCREATE_R(AndExpr, And, AndExpr_createPartial, AndExpr_createPartialR) BCREATE_R(OrExpr, Or, OrExpr_createPartial, OrExpr_createPartialR) BCREATE_R(XorExpr, Xor, XorExpr_createPartial, XorExpr_createPartialR) BCREATE(UDivExpr, UDiv) BCREATE(SDivExpr, SDiv) BCREATE(URemExpr, URem) BCREATE(SRemExpr, SRem) BCREATE(ShlExpr, Shl) BCREATE(LShrExpr, LShr) BCREATE(AShrExpr, AShr) #define CMPCREATE(_e_op, _op) \ ref _e_op ::create(const ref &l, const ref &r) { \ assert(l->getWidth()==r->getWidth() && "type mismatch"); \ if (ConstantExpr *cl = dyn_cast(l)) \ if (ConstantExpr *cr = dyn_cast(r)) \ return cl->_op(cr); \ return _e_op ## _create(l, r); \ } #define CMPCREATE_T(_e_op, _op, _reflexive_e_op, partialL, partialR) \ ref _e_op ::create(const ref &l, const ref &r) { \ assert(l->getWidth()==r->getWidth() && "type mismatch"); \ if (ConstantExpr *cl = dyn_cast(l)) { \ if (ConstantExpr *cr = dyn_cast(r)) \ return cl->_op(cr); \ return partialR(cl, r.get()); \ } else if (ConstantExpr *cr = dyn_cast(r)) { \ return partialL(l.get(), cr); \ } else { \ return _e_op ## _create(l.get(), r.get()); \ } \ } static ref EqExpr_create(const ref &l, const ref &r) { if (l == r) { return ConstantExpr::alloc(1, Expr::Bool); } else { return EqExpr::alloc(l, r); } } /// 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. static ref TryConstArrayOpt(const ref &cl, ReadExpr *rd) { if (rd->updates.root->isSymbolicArray() || rd->updates.getSize()) return EqExpr_create(cl, rd); // Number of positions in the array that contain value ct. unsigned numMatches = 0; // for now, just assume standard "flushing" of a concrete array, // where the concrete array has one update for each index, in order ref res = ConstantExpr::alloc(0, Expr::Bool); for (unsigned i = 0, e = rd->updates.root->size; i != e; ++i) { if (cl == rd->updates.root->constantValues[i]) { // Arbitrary maximum on the size of disjunction. if (++numMatches > 100) return EqExpr_create(cl, rd); ref mayBe = EqExpr::create(rd->index, ConstantExpr::alloc(i, rd->index->getWidth())); res = OrExpr::create(res, mayBe); } } return res; } static ref EqExpr_createPartialR(const ref &cl, Expr *r) { Expr::Width width = cl->getWidth(); Expr::Kind rk = r->getKind(); if (width == Expr::Bool) { if (cl->isTrue()) { return r; } else { // 0 == ... if (rk == Expr::Eq) { const EqExpr *ree = cast(r); // eliminate double negation if (ConstantExpr *CE = dyn_cast(ree->left)) { // 0 == (0 == A) => A if (CE->getWidth() == Expr::Bool && CE->isFalse()) return ree->right; } } else if (rk == Expr::Or) { const OrExpr *roe = cast(r); // transform not(or(a,b)) to and(not a, not b) return AndExpr::create(Expr::createNot(roe->left), Expr::createNot(roe->right)); } } } else if (rk == Expr::SExt) { // (sext(a,T)==c) == (a==c) const SExtExpr *see = cast(r); Expr::Width fromBits = see->src->getWidth(); ref trunc = cl->ZExt(fromBits); // pathological check, make sure it is possible to // sext to this value *from any value* if (cl == trunc->SExt(width)) { return EqExpr::create(see->src, trunc); } else { return ConstantExpr::create(0, Expr::Bool); } } else if (rk == Expr::ZExt) { // (zext(a,T)==c) == (a==c) const ZExtExpr *zee = cast(r); Expr::Width fromBits = zee->src->getWidth(); ref trunc = cl->ZExt(fromBits); // pathological check, make sure it is possible to // zext to this value *from any value* if (cl == trunc->ZExt(width)) { return EqExpr::create(zee->src, trunc); } else { return ConstantExpr::create(0, Expr::Bool); } } else if (rk==Expr::Add) { const AddExpr *ae = cast(r); if (isa(ae->left)) { // c0 = c1 + b => c0 - c1 = b return EqExpr_createPartialR(cast(SubExpr::create(cl, ae->left)), ae->right.get()); } } else if (rk==Expr::Sub) { const SubExpr *se = cast(r); if (isa(se->left)) { // c0 = c1 - b => c1 - c0 = b return EqExpr_createPartialR(cast(SubExpr::create(se->left, cl)), se->right.get()); } } else if (rk == Expr::Read && ConstArrayOpt) { return TryConstArrayOpt(cl, static_cast(r)); } return EqExpr_create(cl, r); } static ref EqExpr_createPartial(Expr *l, const ref &cr) { return EqExpr_createPartialR(cr, l); } ref NeExpr::create(const ref &l, const ref &r) { return EqExpr::create(ConstantExpr::create(0, Expr::Bool), EqExpr::create(l, r)); } ref UgtExpr::create(const ref &l, const ref &r) { return UltExpr::create(r, l); } ref UgeExpr::create(const ref &l, const ref &r) { return UleExpr::create(r, l); } ref SgtExpr::create(const ref &l, const ref &r) { return SltExpr::create(r, l); } ref SgeExpr::create(const ref &l, const ref &r) { return SleExpr::create(r, l); } static ref UltExpr_create(const ref &l, const ref &r) { Expr::Width t = l->getWidth(); if (t == Expr::Bool) { // !l && r return AndExpr::create(Expr::createNot(l), r); } else { return UltExpr::alloc(l, r); } } static ref UleExpr_create(const ref &l, const ref &r) { if (l->getWidth() == Expr::Bool) { // !(l && !r) return OrExpr::create(Expr::createNot(l), r); } else { return UleExpr::alloc(l, r); } } static ref SltExpr_create(const ref &l, const ref &r) { if (l->getWidth() == Expr::Bool) { // l && !r return AndExpr::create(l, Expr::createNot(r)); } else { return SltExpr::alloc(l, r); } } static ref SleExpr_create(const ref &l, const ref &r) { if (l->getWidth() == Expr::Bool) { // !(!l && r) return OrExpr::create(l, Expr::createNot(r)); } else { return SleExpr::alloc(l, r); } } CMPCREATE_T(EqExpr, Eq, EqExpr, EqExpr_createPartial, EqExpr_createPartialR) CMPCREATE(UltExpr, Ult) CMPCREATE(UleExpr, Ule) CMPCREATE(SltExpr, Slt) CMPCREATE(SleExpr, Sle)