klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Expr.cpp
Go to the documentation of this file.
1 //===-- Expr.cpp ----------------------------------------------------------===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #include "klee/Expr.h"
11 #include "klee/Config/Version.h"
12 
13 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1)
14 #include "llvm/ADT/Hashing.h"
15 #endif
16 #include "llvm/Support/CommandLine.h"
17 #include "llvm/Support/raw_ostream.h"
18 // FIXME: We shouldn't need this once fast constant support moves into
19 // Core. If we need to do arithmetic, we probably want to use APInt.
21 
22 #include "klee/util/ExprPPrinter.h"
23 
24 #include <sstream>
25 
26 using namespace klee;
27 using namespace llvm;
28 
29 namespace {
30  cl::opt<bool>
31  ConstArrayOpt("const-array-opt",
32  cl::init(false),
33  cl::desc("Enable various optimizations involving all-constant arrays."));
34 }
35 
36 /***/
37 
38 unsigned Expr::count = 0;
39 
41  UpdateList ul(array, 0);
42 
43  switch (w) {
44  default: assert(0 && "invalid width");
45  case Expr::Bool:
46  return ZExtExpr::create(ReadExpr::create(ul,
48  Expr::Bool);
49  case Expr::Int8:
50  return ReadExpr::create(ul,
52  case Expr::Int16:
55  ReadExpr::create(ul,
57  case Expr::Int32:
60  ReadExpr::create(ul,
62  ReadExpr::create(ul,
64  ReadExpr::create(ul,
66  case Expr::Int64:
69  ReadExpr::create(ul,
71  ReadExpr::create(ul,
73  ReadExpr::create(ul,
75  ReadExpr::create(ul,
77  ReadExpr::create(ul,
79  ReadExpr::create(ul,
81  ReadExpr::create(ul,
83  }
84 }
85 
86 // returns 0 if b is structurally equal to *this
87 int Expr::compare(const Expr &b, ExprEquivSet &equivs) const {
88  if (this == &b) return 0;
89 
90  const Expr *ap, *bp;
91  if (this < &b) {
92  ap = this; bp = &b;
93  } else {
94  ap = &b; bp = this;
95  }
96 
97  if (equivs.count(std::make_pair(ap, bp)))
98  return 0;
99 
100  Kind ak = getKind(), bk = b.getKind();
101  if (ak!=bk)
102  return (ak < bk) ? -1 : 1;
103 
104  if (hashValue != b.hashValue)
105  return (hashValue < b.hashValue) ? -1 : 1;
106 
107  if (int res = compareContents(b))
108  return res;
109 
110  unsigned aN = getNumKids();
111  for (unsigned i=0; i<aN; i++)
112  if (int res = getKid(i)->compare(*b.getKid(i), equivs))
113  return res;
114 
115  equivs.insert(std::make_pair(ap, bp));
116  return 0;
117 }
118 
119 void Expr::printKind(llvm::raw_ostream &os, Kind k) {
120  switch(k) {
121 #define X(C) case C: os << #C; break
122  X(Constant);
123  X(NotOptimized);
124  X(Read);
125  X(Select);
126  X(Concat);
127  X(Extract);
128  X(ZExt);
129  X(SExt);
130  X(Add);
131  X(Sub);
132  X(Mul);
133  X(UDiv);
134  X(SDiv);
135  X(URem);
136  X(SRem);
137  X(Not);
138  X(And);
139  X(Or);
140  X(Xor);
141  X(Shl);
142  X(LShr);
143  X(AShr);
144  X(Eq);
145  X(Ne);
146  X(Ult);
147  X(Ule);
148  X(Ugt);
149  X(Uge);
150  X(Slt);
151  X(Sle);
152  X(Sgt);
153  X(Sge);
154 #undef X
155  default:
156  assert(0 && "invalid kind");
157  }
158 }
159 
161 //
162 // Simple hash functions for various kinds of Exprs
163 //
165 
166 unsigned Expr::computeHash() {
167  unsigned res = getKind() * Expr::MAGIC_HASH_CONSTANT;
168 
169  int n = getNumKids();
170  for (int i = 0; i < n; i++) {
171  res <<= 1;
172  res ^= getKid(i)->hash() * Expr::MAGIC_HASH_CONSTANT;
173  }
174 
175  hashValue = res;
176  return hashValue;
177 }
178 
180 #if LLVM_VERSION_CODE >= LLVM_VERSION(3, 1)
181  hashValue = hash_value(value) ^ (getWidth() * MAGIC_HASH_CONSTANT);
182 #else
183  hashValue = value.getHashValue() ^ (getWidth() * MAGIC_HASH_CONSTANT);
184 #endif
185  return hashValue;
186 }
187 
189  unsigned res = getWidth() * Expr::MAGIC_HASH_CONSTANT;
190  hashValue = res ^ src->hash() * Expr::MAGIC_HASH_CONSTANT;
191  return hashValue;
192 }
193 
195  unsigned res = offset * Expr::MAGIC_HASH_CONSTANT;
196  res ^= getWidth() * Expr::MAGIC_HASH_CONSTANT;
197  hashValue = res ^ expr->hash() * Expr::MAGIC_HASH_CONSTANT;
198  return hashValue;
199 }
200 
202  unsigned res = index->hash() * Expr::MAGIC_HASH_CONSTANT;
203  res ^= updates.hash();
204  hashValue = res;
205  return hashValue;
206 }
207 
209  hashValue = expr->hash() * Expr::MAGIC_HASH_CONSTANT * Expr::Not;
210  return hashValue;
211 }
212 
213 ref<Expr> Expr::createFromKind(Kind k, std::vector<CreateArg> args) {
214  unsigned numArgs = args.size();
215  (void) numArgs;
216 
217  switch(k) {
218  case Constant:
219  case Extract:
220  case Read:
221  default:
222  assert(0 && "invalid kind");
223 
224  case NotOptimized:
225  assert(numArgs == 1 && args[0].isExpr() &&
226  "invalid args array for given opcode");
227  return NotOptimizedExpr::create(args[0].expr);
228 
229  case Select:
230  assert(numArgs == 3 && args[0].isExpr() &&
231  args[1].isExpr() && args[2].isExpr() &&
232  "invalid args array for Select opcode");
233  return SelectExpr::create(args[0].expr,
234  args[1].expr,
235  args[2].expr);
236 
237  case Concat: {
238  assert(numArgs == 2 && args[0].isExpr() && args[1].isExpr() &&
239  "invalid args array for Concat opcode");
240 
241  return ConcatExpr::create(args[0].expr, args[1].expr);
242  }
243 
244 #define CAST_EXPR_CASE(T) \
245  case T: \
246  assert(numArgs == 2 && \
247  args[0].isExpr() && args[1].isWidth() && \
248  "invalid args array for given opcode"); \
249  return T ## Expr::create(args[0].expr, args[1].width); \
250 
251 #define BINARY_EXPR_CASE(T) \
252  case T: \
253  assert(numArgs == 2 && \
254  args[0].isExpr() && args[1].isExpr() && \
255  "invalid args array for given opcode"); \
256  return T ## Expr::create(args[0].expr, args[1].expr); \
257 
258  CAST_EXPR_CASE(ZExt);
259  CAST_EXPR_CASE(SExt);
260 
261  BINARY_EXPR_CASE(Add);
262  BINARY_EXPR_CASE(Sub);
263  BINARY_EXPR_CASE(Mul);
264  BINARY_EXPR_CASE(UDiv);
265  BINARY_EXPR_CASE(SDiv);
266  BINARY_EXPR_CASE(URem);
267  BINARY_EXPR_CASE(SRem);
268  BINARY_EXPR_CASE(And);
269  BINARY_EXPR_CASE(Or);
270  BINARY_EXPR_CASE(Xor);
271  BINARY_EXPR_CASE(Shl);
272  BINARY_EXPR_CASE(LShr);
273  BINARY_EXPR_CASE(AShr);
274 
275  BINARY_EXPR_CASE(Eq);
276  BINARY_EXPR_CASE(Ne);
277  BINARY_EXPR_CASE(Ult);
278  BINARY_EXPR_CASE(Ule);
279  BINARY_EXPR_CASE(Ugt);
280  BINARY_EXPR_CASE(Uge);
281  BINARY_EXPR_CASE(Slt);
282  BINARY_EXPR_CASE(Sle);
283  BINARY_EXPR_CASE(Sgt);
284  BINARY_EXPR_CASE(Sge);
285  }
286 }
287 
288 
289 void Expr::printWidth(llvm::raw_ostream &os, Width width) {
290  switch(width) {
291  case Expr::Bool: os << "Expr::Bool"; break;
292  case Expr::Int8: os << "Expr::Int8"; break;
293  case Expr::Int16: os << "Expr::Int16"; break;
294  case Expr::Int32: os << "Expr::Int32"; break;
295  case Expr::Int64: os << "Expr::Int64"; break;
296  case Expr::Fl80: os << "Expr::Fl80"; break;
297  default: os << "<invalid type: " << (unsigned) width << ">";
298  }
299 }
300 
302  return OrExpr::create(Expr::createIsZero(hyp), conc);
303 }
304 
306  return EqExpr::create(e, ConstantExpr::create(0, e->getWidth()));
307 }
308 
309 void Expr::print(llvm::raw_ostream &os) const {
310  ExprPPrinter::printSingleExpr(os, const_cast<Expr*>(this));
311 }
312 
313 void Expr::dump() const {
314  this->print(errs());
315  errs() << "\n";
316 }
317 
318 /***/
319 
320 ref<Expr> ConstantExpr::fromMemory(void *address, Width width) {
321  switch (width) {
322  case Expr::Bool: return ConstantExpr::create(*(( uint8_t*) address), width);
323  case Expr::Int8: return ConstantExpr::create(*(( uint8_t*) address), width);
324  case Expr::Int16: return ConstantExpr::create(*((uint16_t*) address), width);
325  case Expr::Int32: return ConstantExpr::create(*((uint32_t*) address), width);
326  case Expr::Int64: return ConstantExpr::create(*((uint64_t*) address), width);
327  // FIXME: what about machines without x87 support?
328  default:
329  return ConstantExpr::alloc(llvm::APInt(width,
330  (width+llvm::integerPartWidth-1)/llvm::integerPartWidth,
331  (const uint64_t*)address));
332  }
333 }
334 
335 void ConstantExpr::toMemory(void *address) {
336  switch (getWidth()) {
337  default: assert(0 && "invalid type");
338  case Expr::Bool: *(( uint8_t*) address) = getZExtValue(1); break;
339  case Expr::Int8: *(( uint8_t*) address) = getZExtValue(8); break;
340  case Expr::Int16: *((uint16_t*) address) = getZExtValue(16); break;
341  case Expr::Int32: *((uint32_t*) address) = getZExtValue(32); break;
342  case Expr::Int64: *((uint64_t*) address) = getZExtValue(64); break;
343  // FIXME: what about machines without x87 support?
344  case Expr::Fl80:
345  *((long double*) address) = *(const long double*) value.getRawData();
346  break;
347  }
348 }
349 
350 void ConstantExpr::toString(std::string &Res, unsigned radix) const {
351  Res = value.toString(radix, false);
352 }
353 
355  Expr::Width W = getWidth() + RHS->getWidth();
356  APInt Tmp(value);
357  Tmp=Tmp.zext(W);
358  Tmp <<= RHS->getWidth();
359  Tmp |= APInt(RHS->value).zext(W);
360 
361  return ConstantExpr::alloc(Tmp);
362 }
363 
365  return ConstantExpr::alloc(APInt(value.ashr(Offset)).zextOrTrunc(W));
366 }
367 
369  return ConstantExpr::alloc(APInt(value).zextOrTrunc(W));
370 }
371 
373  return ConstantExpr::alloc(APInt(value).sextOrTrunc(W));
374 }
375 
377  return ConstantExpr::alloc(value + RHS->value);
378 }
379 
381  return ConstantExpr::alloc(-value);
382 }
383 
385  return ConstantExpr::alloc(value - RHS->value);
386 }
387 
389  return ConstantExpr::alloc(value * RHS->value);
390 }
391 
393  return ConstantExpr::alloc(value.udiv(RHS->value));
394 }
395 
397  return ConstantExpr::alloc(value.sdiv(RHS->value));
398 }
399 
401  return ConstantExpr::alloc(value.urem(RHS->value));
402 }
403 
405  return ConstantExpr::alloc(value.srem(RHS->value));
406 }
407 
409  return ConstantExpr::alloc(value & RHS->value);
410 }
411 
413  return ConstantExpr::alloc(value | RHS->value);
414 }
415 
417  return ConstantExpr::alloc(value ^ RHS->value);
418 }
419 
421  return ConstantExpr::alloc(value.shl(RHS->value));
422 }
423 
425  return ConstantExpr::alloc(value.lshr(RHS->value));
426 }
427 
429  return ConstantExpr::alloc(value.ashr(RHS->value));
430 }
431 
433  return ConstantExpr::alloc(~value);
434 }
435 
437  return ConstantExpr::alloc(value == RHS->value, Expr::Bool);
438 }
439 
441  return ConstantExpr::alloc(value != RHS->value, Expr::Bool);
442 }
443 
445  return ConstantExpr::alloc(value.ult(RHS->value), Expr::Bool);
446 }
447 
449  return ConstantExpr::alloc(value.ule(RHS->value), Expr::Bool);
450 }
451 
453  return ConstantExpr::alloc(value.ugt(RHS->value), Expr::Bool);
454 }
455 
457  return ConstantExpr::alloc(value.uge(RHS->value), Expr::Bool);
458 }
459 
461  return ConstantExpr::alloc(value.slt(RHS->value), Expr::Bool);
462 }
463 
465  return ConstantExpr::alloc(value.sle(RHS->value), Expr::Bool);
466 }
467 
469  return ConstantExpr::alloc(value.sgt(RHS->value), Expr::Bool);
470 }
471 
473  return ConstantExpr::alloc(value.sge(RHS->value), Expr::Bool);
474 }
475 
476 /***/
477 
479  return NotOptimizedExpr::alloc(src);
480 }
481 
482 /***/
483 
484 extern "C" void vc_DeleteExpr(void*);
485 
487 }
488 
489 unsigned Array::computeHash() {
490  unsigned res = 0;
491  for (unsigned i = 0, e = name.size(); i != e; ++i)
492  res = (res * Expr::MAGIC_HASH_CONSTANT) + name[i];
493  hashValue = res;
494  return hashValue;
495 }
496 
497 /***/
498 
500  // rollback index when possible...
501 
502  // XXX this doesn't really belong here... there are basically two
503  // cases, one is rebuild, where we want to optimistically try various
504  // optimizations when the index has changed, and the other is
505  // initial creation, where we expect the ObjectState to have constructed
506  // a smart UpdateList so it is not worth rescanning.
507 
508  const UpdateNode *un = ul.head;
509  for (; un; un=un->next) {
510  ref<Expr> cond = EqExpr::create(index, un->index);
511 
512  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(cond)) {
513  if (CE->isTrue())
514  return un->value;
515  } else {
516  break;
517  }
518  }
519 
520  return ReadExpr::alloc(ul, index);
521 }
522 
523 int ReadExpr::compareContents(const Expr &b) const {
524  return updates.compare(static_cast<const ReadExpr&>(b).updates);
525 }
526 
528  Expr::Width kt = t->getWidth();
529 
530  assert(c->getWidth()==Bool && "type mismatch");
531  assert(kt==f->getWidth() && "type mismatch");
532 
533  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(c)) {
534  return CE->isTrue() ? t : f;
535  } else if (t==f) {
536  return t;
537  } else if (kt==Expr::Bool) { // c ? t : f <=> (c and t) or (not c and f)
538  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(t)) {
539  if (CE->isTrue()) {
540  return OrExpr::create(c, f);
541  } else {
542  return AndExpr::create(Expr::createIsZero(c), f);
543  }
544  } else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(f)) {
545  if (CE->isTrue()) {
546  return OrExpr::create(Expr::createIsZero(c), t);
547  } else {
548  return AndExpr::create(c, t);
549  }
550  }
551  }
552 
553  return SelectExpr::alloc(c, t, f);
554 }
555 
556 /***/
557 
559  Expr::Width w = l->getWidth() + r->getWidth();
560 
561  // Fold concatenation of constants.
562  //
563  // FIXME: concat 0 x -> zext x ?
564  if (ConstantExpr *lCE = dyn_cast<ConstantExpr>(l))
565  if (ConstantExpr *rCE = dyn_cast<ConstantExpr>(r))
566  return lCE->Concat(rCE);
567 
568  // Merge contiguous Extracts
569  if (ExtractExpr *ee_left = dyn_cast<ExtractExpr>(l)) {
570  if (ExtractExpr *ee_right = dyn_cast<ExtractExpr>(r)) {
571  if (ee_left->expr == ee_right->expr &&
572  ee_right->offset + ee_right->width == ee_left->offset) {
573  return ExtractExpr::create(ee_left->expr, ee_right->offset, w);
574  }
575  }
576  }
577 
578  return ConcatExpr::alloc(l, r);
579 }
580 
582 ref<Expr> ConcatExpr::createN(unsigned n_kids, const ref<Expr> kids[]) {
583  assert(n_kids > 0);
584  if (n_kids == 1)
585  return kids[0];
586 
587  ref<Expr> r = ConcatExpr::create(kids[n_kids-2], kids[n_kids-1]);
588  for (int i=n_kids-3; i>=0; i--)
589  r = ConcatExpr::create(kids[i], r);
590  return r;
591 }
592 
595  const ref<Expr> &kid3, const ref<Expr> &kid4) {
596  return ConcatExpr::create(kid1, ConcatExpr::create(kid2, ConcatExpr::create(kid3, kid4)));
597 }
598 
601  const ref<Expr> &kid3, const ref<Expr> &kid4,
602  const ref<Expr> &kid5, const ref<Expr> &kid6,
603  const ref<Expr> &kid7, const ref<Expr> &kid8) {
605  ConcatExpr::create(kid4, ConcatExpr::create4(kid5, kid6, kid7, kid8)))));
606 }
607 
608 /***/
609 
611  unsigned kw = expr->getWidth();
612  assert(w > 0 && off + w <= kw && "invalid extract");
613 
614  if (w == kw) {
615  return expr;
616  } else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(expr)) {
617  return CE->Extract(off, w);
618  } else {
619  // Extract(Concat)
620  if (ConcatExpr *ce = dyn_cast<ConcatExpr>(expr)) {
621  // if the extract skips the right side of the concat
622  if (off >= ce->getRight()->getWidth())
623  return ExtractExpr::create(ce->getLeft(), off - ce->getRight()->getWidth(), w);
624 
625  // if the extract skips the left side of the concat
626  if (off + w <= ce->getRight()->getWidth())
627  return ExtractExpr::create(ce->getRight(), off, w);
628 
629  // E(C(x,y)) = C(E(x), E(y))
630  return ConcatExpr::create(ExtractExpr::create(ce->getKid(0), 0, w - ce->getKid(1)->getWidth() + off),
631  ExtractExpr::create(ce->getKid(1), off, ce->getKid(1)->getWidth() - off));
632  }
633  }
634 
635  return ExtractExpr::alloc(expr, off, w);
636 }
637 
638 /***/
639 
641  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e))
642  return CE->Not();
643 
644  return NotExpr::alloc(e);
645 }
646 
647 
648 /***/
649 
650 ref<Expr> ZExtExpr::create(const ref<Expr> &e, Width w) {
651  unsigned kBits = e->getWidth();
652  if (w == kBits) {
653  return e;
654  } else if (w < kBits) { // trunc
655  return ExtractExpr::create(e, 0, w);
656  } else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e)) {
657  return CE->ZExt(w);
658  } else {
659  return ZExtExpr::alloc(e, w);
660  }
661 }
662 
663 ref<Expr> SExtExpr::create(const ref<Expr> &e, Width w) {
664  unsigned kBits = e->getWidth();
665  if (w == kBits) {
666  return e;
667  } else if (w < kBits) { // trunc
668  return ExtractExpr::create(e, 0, w);
669  } else if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e)) {
670  return CE->SExt(w);
671  } else {
672  return SExtExpr::alloc(e, w);
673  }
674 }
675 
676 /***/
677 
678 static ref<Expr> AndExpr_create(Expr *l, Expr *r);
679 static ref<Expr> XorExpr_create(Expr *l, Expr *r);
680 
685 
687  Expr::Width type = cl->getWidth();
688 
689  if (type==Expr::Bool) {
690  return XorExpr_createPartialR(cl, r);
691  } else if (cl->isZero()) {
692  return r;
693  } else {
694  Expr::Kind rk = r->getKind();
695  if (rk==Expr::Add && isa<ConstantExpr>(r->getKid(0))) { // A + (B+c) == (A+B) + c
696  return AddExpr::create(AddExpr::create(cl, r->getKid(0)),
697  r->getKid(1));
698  } else if (rk==Expr::Sub && isa<ConstantExpr>(r->getKid(0))) { // A + (B-c) == (A+B) - c
699  return SubExpr::create(AddExpr::create(cl, r->getKid(0)),
700  r->getKid(1));
701  } else {
702  return AddExpr::alloc(cl, r);
703  }
704  }
705 }
707  return AddExpr_createPartialR(cr, l);
708 }
710  Expr::Width type = l->getWidth();
711 
712  if (type == Expr::Bool) {
713  return XorExpr_create(l, r);
714  } else {
715  Expr::Kind lk = l->getKind(), rk = r->getKind();
716  if (lk==Expr::Add && isa<ConstantExpr>(l->getKid(0))) { // (k+a)+b = k+(a+b)
717  return AddExpr::create(l->getKid(0),
718  AddExpr::create(l->getKid(1), r));
719  } else if (lk==Expr::Sub && isa<ConstantExpr>(l->getKid(0))) { // (k-a)+b = k+(b-a)
720  return AddExpr::create(l->getKid(0),
721  SubExpr::create(r, l->getKid(1)));
722  } else if (rk==Expr::Add && isa<ConstantExpr>(r->getKid(0))) { // a + (k+b) = k+(a+b)
723  return AddExpr::create(r->getKid(0),
724  AddExpr::create(l, r->getKid(1)));
725  } else if (rk==Expr::Sub && isa<ConstantExpr>(r->getKid(0))) { // a + (k-b) = k+(a-b)
726  return AddExpr::create(r->getKid(0),
727  SubExpr::create(l, r->getKid(1)));
728  } else {
729  return AddExpr::alloc(l, r);
730  }
731  }
732 }
733 
735  Expr::Width type = cl->getWidth();
736 
737  if (type==Expr::Bool) {
738  return XorExpr_createPartialR(cl, r);
739  } else {
740  Expr::Kind rk = r->getKind();
741  if (rk==Expr::Add && isa<ConstantExpr>(r->getKid(0))) { // A - (B+c) == (A-B) - c
742  return SubExpr::create(SubExpr::create(cl, r->getKid(0)),
743  r->getKid(1));
744  } else if (rk==Expr::Sub && isa<ConstantExpr>(r->getKid(0))) { // A - (B-c) == (A-B) + c
745  return AddExpr::create(SubExpr::create(cl, r->getKid(0)),
746  r->getKid(1));
747  } else {
748  return SubExpr::alloc(cl, r);
749  }
750  }
751 }
753  // l - c => l + (-c)
754  return AddExpr_createPartial(l,
755  ConstantExpr::alloc(0, cr->getWidth())->Sub(cr));
756 }
758  Expr::Width type = l->getWidth();
759 
760  if (type == Expr::Bool) {
761  return XorExpr_create(l, r);
762  } else if (*l==*r) {
763  return ConstantExpr::alloc(0, type);
764  } else {
765  Expr::Kind lk = l->getKind(), rk = r->getKind();
766  if (lk==Expr::Add && isa<ConstantExpr>(l->getKid(0))) { // (k+a)-b = k+(a-b)
767  return AddExpr::create(l->getKid(0),
768  SubExpr::create(l->getKid(1), r));
769  } else if (lk==Expr::Sub && isa<ConstantExpr>(l->getKid(0))) { // (k-a)-b = k-(a+b)
770  return SubExpr::create(l->getKid(0),
771  AddExpr::create(l->getKid(1), r));
772  } else if (rk==Expr::Add && isa<ConstantExpr>(r->getKid(0))) { // a - (k+b) = (a-c) - k
773  return SubExpr::create(SubExpr::create(l, r->getKid(1)),
774  r->getKid(0));
775  } else if (rk==Expr::Sub && isa<ConstantExpr>(r->getKid(0))) { // a - (k-b) = (a+b) - k
776  return SubExpr::create(AddExpr::create(l, r->getKid(1)),
777  r->getKid(0));
778  } else {
779  return SubExpr::alloc(l, r);
780  }
781  }
782 }
783 
785  Expr::Width type = cl->getWidth();
786 
787  if (type == Expr::Bool) {
788  return AndExpr_createPartialR(cl, r);
789  } else if (cl->isOne()) {
790  return r;
791  } else if (cl->isZero()) {
792  return cl;
793  } else {
794  return MulExpr::alloc(cl, r);
795  }
796 }
798  return MulExpr_createPartialR(cr, l);
799 }
801  Expr::Width type = l->getWidth();
802 
803  if (type == Expr::Bool) {
804  return AndExpr::alloc(l, r);
805  } else {
806  return MulExpr::alloc(l, r);
807  }
808 }
809 
811  if (cr->isAllOnes()) {
812  return l;
813  } else if (cr->isZero()) {
814  return cr;
815  } else {
816  return AndExpr::alloc(l, cr);
817  }
818 }
820  return AndExpr_createPartial(r, cl);
821 }
823  return AndExpr::alloc(l, r);
824 }
825 
827  if (cr->isAllOnes()) {
828  return cr;
829  } else if (cr->isZero()) {
830  return l;
831  } else {
832  return OrExpr::alloc(l, cr);
833  }
834 }
836  return OrExpr_createPartial(r, cl);
837 }
839  return OrExpr::alloc(l, r);
840 }
841 
843  if (cl->isZero()) {
844  return r;
845  } else if (cl->getWidth() == Expr::Bool) {
847  } else {
848  return XorExpr::alloc(cl, r);
849  }
850 }
851 
853  return XorExpr_createPartialR(cr, l);
854 }
856  return XorExpr::alloc(l, r);
857 }
858 
859 static ref<Expr> UDivExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
860  if (l->getWidth() == Expr::Bool) { // r must be 1
861  return l;
862  } else{
863  return UDivExpr::alloc(l, r);
864  }
865 }
866 
867 static ref<Expr> SDivExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
868  if (l->getWidth() == Expr::Bool) { // r must be 1
869  return l;
870  } else{
871  return SDivExpr::alloc(l, r);
872  }
873 }
874 
875 static ref<Expr> URemExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
876  if (l->getWidth() == Expr::Bool) { // r must be 1
877  return ConstantExpr::create(0, Expr::Bool);
878  } else{
879  return URemExpr::alloc(l, r);
880  }
881 }
882 
883 static ref<Expr> SRemExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
884  if (l->getWidth() == Expr::Bool) { // r must be 1
885  return ConstantExpr::create(0, Expr::Bool);
886  } else{
887  return SRemExpr::alloc(l, r);
888  }
889 }
890 
891 static ref<Expr> ShlExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
892  if (l->getWidth() == Expr::Bool) { // l & !r
893  return AndExpr::create(l, Expr::createIsZero(r));
894  } else{
895  return ShlExpr::alloc(l, r);
896  }
897 }
898 
899 static ref<Expr> LShrExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
900  if (l->getWidth() == Expr::Bool) { // l & !r
901  return AndExpr::create(l, Expr::createIsZero(r));
902  } else{
903  return LShrExpr::alloc(l, r);
904  }
905 }
906 
907 static ref<Expr> AShrExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
908  if (l->getWidth() == Expr::Bool) { // l
909  return l;
910  } else{
911  return AShrExpr::alloc(l, r);
912  }
913 }
914 
915 #define BCREATE_R(_e_op, _op, partialL, partialR) \
916 ref<Expr> _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
917  assert(l->getWidth()==r->getWidth() && "type mismatch"); \
918  if (ConstantExpr *cl = dyn_cast<ConstantExpr>(l)) { \
919  if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) \
920  return cl->_op(cr); \
921  return _e_op ## _createPartialR(cl, r.get()); \
922  } else if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) { \
923  return _e_op ## _createPartial(l.get(), cr); \
924  } \
925  return _e_op ## _create(l.get(), r.get()); \
926 }
927 
928 #define BCREATE(_e_op, _op) \
929 ref<Expr> _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
930  assert(l->getWidth()==r->getWidth() && "type mismatch"); \
931  if (ConstantExpr *cl = dyn_cast<ConstantExpr>(l)) \
932  if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) \
933  return cl->_op(cr); \
934  return _e_op ## _create(l, r); \
935 }
936 
943 BCREATE(UDivExpr, UDiv)
944 BCREATE(SDivExpr, SDiv)
945 BCREATE(URemExpr, URem)
946 BCREATE(SRemExpr, SRem)
947 BCREATE(ShlExpr, Shl)
948 BCREATE(LShrExpr, LShr)
949 BCREATE(AShrExpr, AShr)
950 
951 #define CMPCREATE(_e_op, _op) \
952 ref<Expr> _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
953  assert(l->getWidth()==r->getWidth() && "type mismatch"); \
954  if (ConstantExpr *cl = dyn_cast<ConstantExpr>(l)) \
955  if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) \
956  return cl->_op(cr); \
957  return _e_op ## _create(l, r); \
958 }
959 
960 #define CMPCREATE_T(_e_op, _op, _reflexive_e_op, partialL, partialR) \
961 ref<Expr> _e_op ::create(const ref<Expr> &l, const ref<Expr> &r) { \
962  assert(l->getWidth()==r->getWidth() && "type mismatch"); \
963  if (ConstantExpr *cl = dyn_cast<ConstantExpr>(l)) { \
964  if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) \
965  return cl->_op(cr); \
966  return partialR(cl, r.get()); \
967  } else if (ConstantExpr *cr = dyn_cast<ConstantExpr>(r)) { \
968  return partialL(l.get(), cr); \
969  } else { \
970  return _e_op ## _create(l.get(), r.get()); \
971  } \
972 }
973 
974 
975 static ref<Expr> EqExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
976  if (l == r) {
977  return ConstantExpr::alloc(1, Expr::Bool);
978  } else {
979  return EqExpr::alloc(l, r);
980  }
981 }
982 
983 
989  ReadExpr *rd) {
990  if (rd->updates.root->isSymbolicArray() || rd->updates.getSize())
991  return EqExpr_create(cl, rd);
992 
993  // Number of positions in the array that contain value ct.
994  unsigned numMatches = 0;
995 
996  // for now, just assume standard "flushing" of a concrete array,
997  // where the concrete array has one update for each index, in order
999  for (unsigned i = 0, e = rd->updates.root->size; i != e; ++i) {
1000  if (cl == rd->updates.root->constantValues[i]) {
1001  // Arbitrary maximum on the size of disjunction.
1002  if (++numMatches > 100)
1003  return EqExpr_create(cl, rd);
1004 
1005  ref<Expr> mayBe =
1006  EqExpr::create(rd->index, ConstantExpr::alloc(i,
1007  rd->index->getWidth()));
1008  res = OrExpr::create(res, mayBe);
1009  }
1010  }
1011 
1012  return res;
1013 }
1014 
1016  Expr::Width width = cl->getWidth();
1017 
1018  Expr::Kind rk = r->getKind();
1019  if (width == Expr::Bool) {
1020  if (cl->isTrue()) {
1021  return r;
1022  } else {
1023  // 0 == ...
1024 
1025  if (rk == Expr::Eq) {
1026  const EqExpr *ree = cast<EqExpr>(r);
1027 
1028  // eliminate double negation
1029  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(ree->left)) {
1030  // 0 == (0 == A) => A
1031  if (CE->getWidth() == Expr::Bool &&
1032  CE->isFalse())
1033  return ree->right;
1034  }
1035  } else if (rk == Expr::Or) {
1036  const OrExpr *roe = cast<OrExpr>(r);
1037 
1038  // transform not(or(a,b)) to and(not a, not b)
1039  return AndExpr::create(Expr::createIsZero(roe->left),
1040  Expr::createIsZero(roe->right));
1041  }
1042  }
1043  } else if (rk == Expr::SExt) {
1044  // (sext(a,T)==c) == (a==c)
1045  const SExtExpr *see = cast<SExtExpr>(r);
1046  Expr::Width fromBits = see->src->getWidth();
1047  ref<ConstantExpr> trunc = cl->ZExt(fromBits);
1048 
1049  // pathological check, make sure it is possible to
1050  // sext to this value *from any value*
1051  if (cl == trunc->SExt(width)) {
1052  return EqExpr::create(see->src, trunc);
1053  } else {
1054  return ConstantExpr::create(0, Expr::Bool);
1055  }
1056  } else if (rk == Expr::ZExt) {
1057  // (zext(a,T)==c) == (a==c)
1058  const ZExtExpr *zee = cast<ZExtExpr>(r);
1059  Expr::Width fromBits = zee->src->getWidth();
1060  ref<ConstantExpr> trunc = cl->ZExt(fromBits);
1061 
1062  // pathological check, make sure it is possible to
1063  // zext to this value *from any value*
1064  if (cl == trunc->ZExt(width)) {
1065  return EqExpr::create(zee->src, trunc);
1066  } else {
1067  return ConstantExpr::create(0, Expr::Bool);
1068  }
1069  } else if (rk==Expr::Add) {
1070  const AddExpr *ae = cast<AddExpr>(r);
1071  if (isa<ConstantExpr>(ae->left)) {
1072  // c0 = c1 + b => c0 - c1 = b
1073  return EqExpr_createPartialR(cast<ConstantExpr>(SubExpr::create(cl,
1074  ae->left)),
1075  ae->right.get());
1076  }
1077  } else if (rk==Expr::Sub) {
1078  const SubExpr *se = cast<SubExpr>(r);
1079  if (isa<ConstantExpr>(se->left)) {
1080  // c0 = c1 - b => c1 - c0 = b
1081  return EqExpr_createPartialR(cast<ConstantExpr>(SubExpr::create(se->left,
1082  cl)),
1083  se->right.get());
1084  }
1085  } else if (rk == Expr::Read && ConstArrayOpt) {
1086  return TryConstArrayOpt(cl, static_cast<ReadExpr*>(r));
1087  }
1088 
1089  return EqExpr_create(cl, r);
1090 }
1091 
1093  return EqExpr_createPartialR(cr, l);
1094 }
1095 
1096 ref<Expr> NeExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
1097  return EqExpr::create(ConstantExpr::create(0, Expr::Bool),
1098  EqExpr::create(l, r));
1099 }
1100 
1101 ref<Expr> UgtExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
1102  return UltExpr::create(r, l);
1103 }
1104 ref<Expr> UgeExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
1105  return UleExpr::create(r, l);
1106 }
1107 
1108 ref<Expr> SgtExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
1109  return SltExpr::create(r, l);
1110 }
1111 ref<Expr> SgeExpr::create(const ref<Expr> &l, const ref<Expr> &r) {
1112  return SleExpr::create(r, l);
1113 }
1114 
1115 static ref<Expr> UltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
1116  Expr::Width t = l->getWidth();
1117  if (t == Expr::Bool) { // !l && r
1118  return AndExpr::create(Expr::createIsZero(l), r);
1119  } else {
1120  return UltExpr::alloc(l, r);
1121  }
1122 }
1123 
1124 static ref<Expr> UleExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
1125  if (l->getWidth() == Expr::Bool) { // !(l && !r)
1126  return OrExpr::create(Expr::createIsZero(l), r);
1127  } else {
1128  return UleExpr::alloc(l, r);
1129  }
1130 }
1131 
1132 static ref<Expr> SltExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
1133  if (l->getWidth() == Expr::Bool) { // l && !r
1134  return AndExpr::create(l, Expr::createIsZero(r));
1135  } else {
1136  return SltExpr::alloc(l, r);
1137  }
1138 }
1139 
1140 static ref<Expr> SleExpr_create(const ref<Expr> &l, const ref<Expr> &r) {
1141  if (l->getWidth() == Expr::Bool) { // !(!l && r)
1142  return OrExpr::create(l, Expr::createIsZero(r));
1143  } else {
1144  return SleExpr::alloc(l, r);
1145  }
1146 }
1147 
1149 CMPCREATE(UltExpr, Ult)
1150 CMPCREATE(UleExpr, Ule)
1151 CMPCREATE(SltExpr, Slt)
1152 CMPCREATE(SleExpr, Sle)
static ref< Expr > URemExpr_create(const ref< Expr > &l, const ref< Expr > &r)
Definition: Expr.cpp:875
bool isSymbolicArray() const
Definition: Expr.h:641
ref< ConstantExpr > Extract(unsigned offset, Width W)
Definition: Expr.cpp:364
static ref< Expr > alloc(const ref< Expr > &src)
Definition: Expr.h:541
unsigned hashValue
Definition: Expr.h:174
static ref< Expr > XorExpr_createPartial(Expr *l, const ref< ConstantExpr > &cr)
Definition: Expr.cpp:852
virtual unsigned computeHash()
Definition: Expr.cpp:201
void toString(std::string &Res, unsigned radix=10) const
Definition: Expr.cpp:350
ref< ConstantExpr > Ult(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:444
static void printWidth(llvm::raw_ostream &os, Expr::Width w)
Definition: Expr.cpp:289
static ref< Expr > alloc(const ref< Expr > &l, const ref< Expr > &r)
Definition: Expr.h:793
ref< ConstantExpr > URem(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:400
ref< ConstantExpr > Ne(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:440
ref< ConstantExpr > Neg()
Definition: Expr.cpp:380
static const unsigned MAGIC_HASH_CONSTANT
Definition: Expr.h:91
ref< ConstantExpr > Sub(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:384
#define CMPCREATE(_e_op, _op)
Definition: Expr.cpp:951
ref< Expr > index
Definition: Expr.h:578
static ref< Expr > create(ref< Expr > e, unsigned bitOff, Width w)
Creates an ExtractExpr with the given bit offset and width.
Definition: Expr.cpp:610
static ref< Expr > SubExpr_createPartial(Expr *l, const ref< ConstantExpr > &cr)
Definition: Expr.cpp:752
ref< ConstantExpr > Or(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:412
ref< ConstantExpr > SDiv(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:396
ref< ConstantExpr > SRem(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:404
static ref< Expr > MulExpr_createPartial(Expr *l, const ref< ConstantExpr > &cr)
Definition: Expr.cpp:797
unsigned size
Definition: Expr.h:605
ref< ConstantExpr > Uge(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:456
static ref< Expr > create(const UpdateList &updates, ref< Expr > i)
Definition: Expr.cpp:499
virtual void print(llvm::raw_ostream &os) const
Definition: Expr.cpp:309
static ref< Expr > AddExpr_createPartial(Expr *l, const ref< ConstantExpr > &cr)
Definition: Expr.cpp:706
ref< ConstantExpr > Mul(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:388
static ref< Expr > AddExpr_createPartialR(const ref< ConstantExpr > &cl, Expr *r)
Definition: Expr.cpp:686
#define CAST_EXPR_CASE(T)
int compareContents(const Expr &b) const
Definition: Expr.cpp:523
static ref< Expr > create(ref< Expr > c, ref< Expr > t, ref< Expr > f)
Definition: Expr.cpp:527
ref< ConstantExpr > Not()
Definition: Expr.cpp:432
bool isOne() const
isOne - Is this a constant one.
Definition: Expr.h:429
static const Width Fl80
Definition: Expr.h:102
static ref< Expr > ShlExpr_create(const ref< Expr > &l, const ref< Expr > &r)
Definition: Expr.cpp:891
ref< ConstantExpr > Eq(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:436
ref< ConstantExpr > Xor(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:416
bool isZero() const
isZero - Is this a constant zero.
Definition: Expr.h:426
const std::vector< ref< ConstantExpr > > constantValues
Definition: Expr.h:610
static ref< Expr > SubExpr_createPartialR(const ref< ConstantExpr > &cl, Expr *r)
Definition: Expr.cpp:734
static const Width Int16
Definition: Expr.h:99
static ref< Expr > create(const ref< Expr > &l, const ref< Expr > &r)
Definition: Expr.cpp:558
static ref< Expr > AddExpr_create(Expr *l, Expr *r)
Definition: Expr.cpp:709
ref< ConstantExpr > And(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:408
Class representing a complete list of updates into an array.
Definition: Expr.h:655
UpdateList updates
Definition: Expr.h:687
#define CMPCREATE_T(_e_op, _op, _reflexive_e_op, partialL, partialR)
Definition: Expr.cpp:960
ref< ConstantExpr > UDiv(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:392
static ref< Expr > createN(unsigned nKids, const ref< Expr > kids[])
Shortcuts to create larger concats. The chain returned is unbalanced to the right.
Definition: Expr.cpp:582
ref< Expr > value
Definition: Expr.h:578
static const Width Int32
Definition: Expr.h:100
Class representing symbolic expressions.
Definition: Expr.h:88
static const Width Int8
Definition: Expr.h:98
bool isAllOnes() const
isAllOnes - Is this constant all ones.
Definition: Expr.h:442
static ref< Expr > SltExpr_create(const ref< Expr > &l, const ref< Expr > &r)
Definition: Expr.cpp:1132
virtual Width getWidth() const =0
static ref< Expr > create8(const ref< Expr > &kid1, const ref< Expr > &kid2, const ref< Expr > &kid3, const ref< Expr > &kid4, const ref< Expr > &kid5, const ref< Expr > &kid6, const ref< Expr > &kid7, const ref< Expr > &kid8)
Shortcut to concat 8 kids. The chain returned is unbalanced to the right.
Definition: Expr.cpp:600
static ref< Expr > AShrExpr_create(const ref< Expr > &l, const ref< Expr > &r)
Definition: Expr.cpp:907
virtual ref< Expr > getKid(unsigned i) const =0
static ref< Expr > XorExpr_create(Expr *l, Expr *r)
Definition: Expr.cpp:855
static ref< Expr > UleExpr_create(const ref< Expr > &l, const ref< Expr > &r)
Definition: Expr.cpp:1124
static const Width Int64
Definition: Expr.h:101
static ref< Expr > createFromKind(Kind k, std::vector< CreateArg > args)
Definition: Expr.cpp:213
static ref< Expr > SubExpr_create(Expr *l, Expr *r)
Definition: Expr.cpp:757
bool isTrue() const
isTrue - Is this the true expression.
Definition: Expr.h:432
ref< ConstantExpr > Sle(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:464
ref< ConstantExpr > Ule(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:448
static ref< Expr > MulExpr_createPartialR(const ref< ConstantExpr > &cl, Expr *r)
Definition: Expr.cpp:784
virtual unsigned computeHash()
Definition: Expr.cpp:194
uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth)
static ref< Expr > createTempRead(const Array *array, Expr::Width w)
Definition: Expr.cpp:40
static ref< Expr > EqExpr_createPartialR(const ref< ConstantExpr > &cl, Expr *r)
Definition: Expr.cpp:1015
static ref< Expr > createIsZero(ref< Expr > e)
Definition: Expr.cpp:305
ref< ConstantExpr > Sgt(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:468
const UpdateNode * head
pointer to the most recent update node
Definition: Expr.h:662
static ref< Expr > create4(const ref< Expr > &kid1, const ref< Expr > &kid2, const ref< Expr > &kid3, const ref< Expr > &kid4)
Shortcut to concat 4 kids. The chain returned is unbalanced to the right.
Definition: Expr.cpp:594
static ref< Expr > UDivExpr_create(const ref< Expr > &l, const ref< Expr > &r)
Definition: Expr.cpp:859
virtual unsigned computeHash()
Definition: Expr.cpp:188
int compare(const Expr &b, ExprEquivSet &equivs) const
Definition: Expr.cpp:87
static unsigned count
Definition: Expr.h:90
static ref< Expr > alloc(const ref< Expr > &e)
Definition: Expr.h:903
static ref< Expr > EqExpr_createPartial(Expr *l, const ref< ConstantExpr > &cr)
Definition: Expr.cpp:1092
virtual unsigned computeHash()
Definition: Expr.cpp:166
llvm::APInt value
Definition: Expr.h:333
static ref< ConstantExpr > create(uint64_t v, Width w)
Definition: Expr.h:412
static void printKind(llvm::raw_ostream &os, Kind k)
Definition: Expr.cpp:119
static ref< Expr > AndExpr_createPartialR(const ref< ConstantExpr > &cl, Expr *r)
Definition: Expr.cpp:819
unsigned Width
The type of an expression is simply its width, in bits.
Definition: Expr.h:94
ref< ConstantExpr > AShr(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:428
static ref< Expr > OrExpr_createPartialR(const ref< ConstantExpr > &cl, Expr *r)
Definition: Expr.cpp:835
static ref< Expr > UltExpr_create(const ref< Expr > &l, const ref< Expr > &r)
Definition: Expr.cpp:1115
static ref< Expr > create(ref< Expr > src)
Definition: Expr.cpp:478
static ref< Expr > OrExpr_createPartial(Expr *l, const ref< ConstantExpr > &cr)
Definition: Expr.cpp:826
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:398
#define X(C)
static ref< Expr > OrExpr_create(Expr *l, Expr *r)
Definition: Expr.cpp:838
ref< ConstantExpr > Ugt(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:452
virtual unsigned computeHash()
Definition: Expr.cpp:179
static void printSingleExpr(llvm::raw_ostream &os, const ref< Expr > &e)
const UpdateNode * next
Definition: Expr.h:577
static ref< Expr > SleExpr_create(const ref< Expr > &l, const ref< Expr > &r)
Definition: Expr.cpp:1140
ref< ConstantExpr > Shl(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:420
static ref< Expr > createImplies(ref< Expr > hyp, ref< Expr > conc)
Definition: Expr.cpp:301
llvm::DenseSet< std::pair< const Expr *, const Expr * > > ExprEquivSet
Returns 0 iff b is structuraly equivalent to *this.
Definition: Expr.h:199
unsigned getSize() const
size of this update list
Definition: Expr.h:672
const Array * root
Definition: Expr.h:659
virtual Kind getKind() const =0
static ref< Expr > LShrExpr_create(const ref< Expr > &l, const ref< Expr > &r)
Definition: Expr.cpp:899
Class representing a one byte read from an array.
Definition: Expr.h:681
static ref< Expr > alloc(const UpdateList &updates, const ref< Expr > &index)
Definition: Expr.h:691
Width getWidth() const
Definition: Expr.h:340
ref< ConstantExpr > LShr(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:424
unsigned computeHash()
Definition: Expr.cpp:489
ref< Expr > index
Definition: Expr.h:688
Class representing a byte update of an array.
Definition: Expr.h:569
ref< ConstantExpr > SExt(Width W)
Definition: Expr.cpp:372
static ref< Expr > XorExpr_createPartialR(const ref< ConstantExpr > &cl, Expr *r)
Definition: Expr.cpp:842
static ref< Expr > AndExpr_createPartial(Expr *l, const ref< ConstantExpr > &cr)
Definition: Expr.cpp:810
void dump() const
dump - Print the expression to stderr.
Definition: Expr.cpp:313
static ref< Expr > alloc(const ref< Expr > &c, const ref< Expr > &t, const ref< Expr > &f)
Definition: Expr.h:735
static const Width Bool
Definition: Expr.h:97
ref< ConstantExpr > Concat(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:354
static ref< Expr > AndExpr_create(Expr *l, Expr *r)
Definition: Expr.cpp:822
static ref< Expr > TryConstArrayOpt(const ref< ConstantExpr > &cl, ReadExpr *rd)
Definition: Expr.cpp:988
ref< ConstantExpr > ZExt(Width W)
Definition: Expr.cpp:368
void toMemory(void *address)
Definition: Expr.cpp:335
ref< ConstantExpr > Sge(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:472
static ref< Expr > create(const ref< Expr > &e)
Definition: Expr.cpp:640
#define BCREATE_R(_e_op, _op, partialL, partialR)
Definition: Expr.cpp:915
static ref< Expr > fromMemory(void *address, Width w)
Definition: Expr.cpp:320
static ref< Expr > EqExpr_create(const ref< Expr > &l, const ref< Expr > &r)
Definition: Expr.cpp:975
static ref< Expr > MulExpr_create(Expr *l, Expr *r)
Definition: Expr.cpp:800
ref< ConstantExpr > Slt(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:460
virtual unsigned computeHash()
Definition: Expr.cpp:208
static ref< Expr > SRemExpr_create(const ref< Expr > &l, const ref< Expr > &r)
Definition: Expr.cpp:883
static ref< Expr > alloc(const ref< Expr > &e, unsigned o, Width w)
Definition: Expr.h:852
void vc_DeleteExpr(void *)
#define BINARY_EXPR_CASE(T)
ref< ConstantExpr > Add(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:376
#define BCREATE(_e_op, _op)
Definition: Expr.cpp:928
static ref< Expr > SDivExpr_create(const ref< Expr > &l, const ref< Expr > &r)
Definition: Expr.cpp:867