klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Expr.h
Go to the documentation of this file.
1 //===-- Expr.h --------------------------------------------------*- C++ -*-===//
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 #ifndef KLEE_EXPR_H
11 #define KLEE_EXPR_H
12 
13 #include "klee/util/Bits.h"
14 #include "klee/util/Ref.h"
15 
16 #include "llvm/ADT/APInt.h"
17 #include "llvm/ADT/APFloat.h"
18 #include "llvm/ADT/DenseSet.h"
19 #include "llvm/ADT/SmallVector.h"
20 #include "llvm/Support/raw_ostream.h"
21 
22 #include <sstream>
23 #include <set>
24 #include <vector>
25 
26 namespace llvm {
27  class Type;
28  class raw_ostream;
29 }
30 
31 namespace klee {
32 
33 class Array;
34 class ConstantExpr;
35 class ObjectState;
36 
37 template<class T> class ref;
38 
39 
41 
88 class Expr {
89 public:
90  static unsigned count;
91  static const unsigned MAGIC_HASH_CONSTANT = 39;
92 
94  typedef unsigned Width;
95 
96  static const Width InvalidWidth = 0;
97  static const Width Bool = 1;
98  static const Width Int8 = 8;
99  static const Width Int16 = 16;
100  static const Width Int32 = 32;
101  static const Width Int64 = 64;
102  static const Width Fl80 = 80;
103 
104 
105  enum Kind {
107 
108  // Primitive
109 
110  Constant = 0,
111 
112  // Special
113 
118 
124 
125  // Casting,
128 
129  // All subsequent kinds are binary.
130 
131  // Arithmetic
139 
140  // Bit
143  Or,
148 
149  // Compare
150  Eq,
151  Ne,
154  Ugt,
155  Uge,
158  Sgt,
159  Sge,
160 
162 
169  };
170 
171  unsigned refCount;
172 
173 protected:
174  unsigned hashValue;
175 
176 public:
177  Expr() : refCount(0) { Expr::count++; }
178  virtual ~Expr() { Expr::count--; }
179 
180  virtual Kind getKind() const = 0;
181  virtual Width getWidth() const = 0;
182 
183  virtual unsigned getNumKids() const = 0;
184  virtual ref<Expr> getKid(unsigned i) const = 0;
185 
186  virtual void print(llvm::raw_ostream &os) const;
187 
189  void dump() const;
190 
192  virtual unsigned hash() const { return hashValue; }
193 
196  virtual unsigned computeHash();
197 
199  typedef llvm::DenseSet<std::pair<const Expr *, const Expr *> > ExprEquivSet;
200  int compare(const Expr &b, ExprEquivSet &equivs) const;
201  int compare(const Expr &b) const {
202  static ExprEquivSet equivs;
203  int r = compare(b, equivs);
204  equivs.clear();
205  return r;
206  }
207  virtual int compareContents(const Expr &b) const { return 0; }
208 
209  // Given an array of new kids return a copy of the expression
210  // but using those children.
211  virtual ref<Expr> rebuild(ref<Expr> kids[/* getNumKids() */]) const = 0;
212 
213  //
214 
216  bool isZero() const;
217 
219  bool isTrue() const;
220 
222  bool isFalse() const;
223 
224  /* Static utility methods */
225 
226  static void printKind(llvm::raw_ostream &os, Kind k);
227  static void printWidth(llvm::raw_ostream &os, Expr::Width w);
228 
230  static inline unsigned getMinBytesForWidth(Width w) {
231  return (w + 7) / 8;
232  }
233 
234  /* Kind utilities */
235 
236  /* Utility creation functions */
239  static ref<Expr> createImplies(ref<Expr> hyp, ref<Expr> conc);
240  static ref<Expr> createIsZero(ref<Expr> e);
241 
244  static ref<Expr> createTempRead(const Array *array, Expr::Width w);
245 
246  static ref<ConstantExpr> createPointer(uint64_t v);
247 
248  struct CreateArg;
249  static ref<Expr> createFromKind(Kind k, std::vector<CreateArg> args);
250 
251  static bool isValidKidWidth(unsigned kid, Width w) { return true; }
252  static bool needsResultType() { return false; }
253 
254  static bool classof(const Expr *) { return true; }
255 };
256 
260 
261  CreateArg(Width w = Bool) : expr(0), width(w) {}
263 
264  bool isExpr() { return !isWidth(); }
265  bool isWidth() { return width != Expr::InvalidWidth; }
266 };
267 
268 // Comparison operators
269 
270 inline bool operator==(const Expr &lhs, const Expr &rhs) {
271  return lhs.compare(rhs) == 0;
272 }
273 
274 inline bool operator<(const Expr &lhs, const Expr &rhs) {
275  return lhs.compare(rhs) < 0;
276 }
277 
278 inline bool operator!=(const Expr &lhs, const Expr &rhs) {
279  return !(lhs == rhs);
280 }
281 
282 inline bool operator>(const Expr &lhs, const Expr &rhs) {
283  return rhs < lhs;
284 }
285 
286 inline bool operator<=(const Expr &lhs, const Expr &rhs) {
287  return !(lhs > rhs);
288 }
289 
290 inline bool operator>=(const Expr &lhs, const Expr &rhs) {
291  return !(lhs < rhs);
292 }
293 
294 // Printing operators
295 
296 inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const Expr &e) {
297  e.print(os);
298  return os;
299 }
300 
301 // XXX the following macro is to work around the ExprTest unit test compile error
302 #ifndef LLVM_29_UNITTEST
303 inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const Expr::Kind kind) {
304  Expr::printKind(os, kind);
305  return os;
306 }
307 #endif
308 
309 inline std::stringstream &operator<<(std::stringstream &os, const Expr &e) {
310  std::string str;
311  llvm::raw_string_ostream TmpStr(str);
312  e.print(TmpStr);
313  os << TmpStr.str();
314  return os;
315 }
316 
317 inline std::stringstream &operator<<(std::stringstream &os, const Expr::Kind kind) {
318  std::string str;
319  llvm::raw_string_ostream TmpStr(str);
320  Expr::printKind(TmpStr, kind);
321  os << TmpStr.str();
322  return os;
323 }
324 
325 // Terminal Exprs
326 
327 class ConstantExpr : public Expr {
328 public:
329  static const Kind kind = Constant;
330  static const unsigned numKids = 0;
331 
332 private:
333  llvm::APInt value;
334 
335  ConstantExpr(const llvm::APInt &v) : value(v) {}
336 
337 public:
339 
340  Width getWidth() const { return value.getBitWidth(); }
341  Kind getKind() const { return Constant; }
342 
343  unsigned getNumKids() const { return 0; }
344  ref<Expr> getKid(unsigned i) const { return 0; }
345 
350  const llvm::APInt &getAPValue() const { return value; }
351 
361  uint64_t getZExtValue(unsigned bits = 64) const {
362  assert(getWidth() <= bits && "Value may be out of range!");
363  return value.getZExtValue();
364  }
365 
368  uint64_t getLimitedValue(uint64_t Limit = ~0ULL) const {
369  return value.getLimitedValue(Limit);
370  }
371 
375  void toString(std::string &Res, unsigned radix=10) const;
376 
377 
378 
379  int compareContents(const Expr &b) const {
380  const ConstantExpr &cb = static_cast<const ConstantExpr&>(b);
381  if (getWidth() != cb.getWidth())
382  return getWidth() < cb.getWidth() ? -1 : 1;
383  if (value == cb.value)
384  return 0;
385  return value.ult(cb.value) ? -1 : 1;
386  }
387 
388  virtual ref<Expr> rebuild(ref<Expr> kids[]) const {
389  assert(0 && "rebuild() on ConstantExpr");
390  return const_cast<ConstantExpr*>(this);
391  }
392 
393  virtual unsigned computeHash();
394 
395  static ref<Expr> fromMemory(void *address, Width w);
396  void toMemory(void *address);
397 
398  static ref<ConstantExpr> alloc(const llvm::APInt &v) {
400  r->computeHash();
401  return r;
402  }
403 
404  static ref<ConstantExpr> alloc(const llvm::APFloat &f) {
405  return alloc(f.bitcastToAPInt());
406  }
407 
408  static ref<ConstantExpr> alloc(uint64_t v, Width w) {
409  return alloc(llvm::APInt(w, v));
410  }
411 
412  static ref<ConstantExpr> create(uint64_t v, Width w) {
413  assert(v == bits64::truncateToNBits(v, w) &&
414  "invalid constant");
415  return alloc(v, w);
416  }
417 
418  static bool classof(const Expr *E) {
419  return E->getKind() == Expr::Constant;
420  }
421  static bool classof(const ConstantExpr *) { return true; }
422 
423  /* Utility Functions */
424 
426  bool isZero() const { return getAPValue().isMinValue(); }
427 
429  bool isOne() const { return getLimitedValue() == 1; }
430 
432  bool isTrue() const {
433  return (getWidth() == Expr::Bool && value.getBoolValue()==true);
434  }
435 
437  bool isFalse() const {
438  return (getWidth() == Expr::Bool && value.getBoolValue()==false);
439  }
440 
442  bool isAllOnes() const { return getAPValue().isAllOnesValue(); }
443 
444  /* Constant Operations */
445 
447  ref<ConstantExpr> Extract(unsigned offset, Width W);
463 
464  // Comparisons return a constant expression of width 1.
465 
476 
479 };
480 
481 
482 // Utility classes
483 
484 class NonConstantExpr : public Expr {
485 public:
486  static bool classof(const Expr *E) {
487  return E->getKind() != Expr::Constant;
488  }
489  static bool classof(const NonConstantExpr *) { return true; }
490 };
491 
492 class BinaryExpr : public NonConstantExpr {
493 public:
495 
496 public:
497  unsigned getNumKids() const { return 2; }
498  ref<Expr> getKid(unsigned i) const {
499  if(i == 0)
500  return left;
501  if(i == 1)
502  return right;
503  return 0;
504  }
505 
506 protected:
507  BinaryExpr(const ref<Expr> &l, const ref<Expr> &r) : left(l), right(r) {}
508 
509 public:
510  static bool classof(const Expr *E) {
511  Kind k = E->getKind();
512  return Expr::BinaryKindFirst <= k && k <= Expr::BinaryKindLast;
513  }
514  static bool classof(const BinaryExpr *) { return true; }
515 };
516 
517 
518 class CmpExpr : public BinaryExpr {
519 
520 protected:
522 
523 public:
524  Width getWidth() const { return Bool; }
525 
526  static bool classof(const Expr *E) {
527  Kind k = E->getKind();
528  return Expr::CmpKindFirst <= k && k <= Expr::CmpKindLast;
529  }
530  static bool classof(const CmpExpr *) { return true; }
531 };
532 
533 // Special
534 
536 public:
537  static const Kind kind = NotOptimized;
538  static const unsigned numKids = 1;
540 
541  static ref<Expr> alloc(const ref<Expr> &src) {
542  ref<Expr> r(new NotOptimizedExpr(src));
543  r->computeHash();
544  return r;
545  }
546 
547  static ref<Expr> create(ref<Expr> src);
548 
549  Width getWidth() const { return src->getWidth(); }
550  Kind getKind() const { return NotOptimized; }
551 
552  unsigned getNumKids() const { return 1; }
553  ref<Expr> getKid(unsigned i) const { return src; }
554 
555  virtual ref<Expr> rebuild(ref<Expr> kids[]) const { return create(kids[0]); }
556 
557 private:
558  NotOptimizedExpr(const ref<Expr> &_src) : src(_src) {}
559 
560 public:
561  static bool classof(const Expr *E) {
562  return E->getKind() == Expr::NotOptimized;
563  }
564  static bool classof(const NotOptimizedExpr *) { return true; }
565 };
566 
567 
569 class UpdateNode {
570  friend class UpdateList;
571 
572  mutable unsigned refCount;
573  // cache instead of recalc
574  unsigned hashValue;
575 
576 public:
577  const UpdateNode *next;
579 
580 private:
582  unsigned size;
583 
584 public:
585  UpdateNode(const UpdateNode *_next,
586  const ref<Expr> &_index,
587  const ref<Expr> &_value);
588 
589  unsigned getSize() const { return size; }
590 
591  int compare(const UpdateNode &b) const;
592  unsigned hash() const { return hashValue; }
593 
594 private:
596  ~UpdateNode();
597 
598  unsigned computeHash();
599 };
600 
601 class Array {
602 public:
603  const std::string name;
604  // FIXME: Not 64-bit clean.
605  unsigned size;
606 
610  const std::vector< ref<ConstantExpr> > constantValues;
611 
613 
614 public:
622  Array(const std::string &_name, uint64_t _size,
623  const ref<ConstantExpr> *constantValuesBegin = 0,
624  const ref<ConstantExpr> *constantValuesEnd = 0,
625  Expr::Width _domain = Expr::Int32, Expr::Width _range = Expr::Int8)
626  : name(_name), size(_size),
627  constantValues(constantValuesBegin, constantValuesEnd),
628  domain(_domain), range(_range) {
629  assert((isSymbolicArray() || constantValues.size() == size) &&
630  "Invalid size for constant array!");
631  computeHash();
632 #ifndef NDEBUG
633  for (const ref<ConstantExpr> *it = constantValuesBegin;
634  it != constantValuesEnd; ++it)
635  assert((*it)->getWidth() == getRange() &&
636  "Invalid initial constant value!");
637 #endif
638  }
639  ~Array();
640 
641  bool isSymbolicArray() const { return constantValues.empty(); }
642  bool isConstantArray() const { return !isSymbolicArray(); }
643 
644  Expr::Width getDomain() const { return domain; }
645  Expr::Width getRange() const { return range; }
646 
647  unsigned computeHash();
648  unsigned hash() const { return hashValue; }
649 
650 private:
651  unsigned hashValue;
652 };
653 
655 class UpdateList {
656  friend class ReadExpr; // for default constructor
657 
658 public:
659  const Array *root;
660 
662  const UpdateNode *head;
663 
664 public:
665  UpdateList(const Array *_root, const UpdateNode *_head);
666  UpdateList(const UpdateList &b);
667  ~UpdateList();
668 
669  UpdateList &operator=(const UpdateList &b);
670 
672  unsigned getSize() const { return (head ? head->getSize() : 0); }
673 
674  void extend(const ref<Expr> &index, const ref<Expr> &value);
675 
676  int compare(const UpdateList &b) const;
677  unsigned hash() const;
678 };
679 
681 class ReadExpr : public NonConstantExpr {
682 public:
683  static const Kind kind = Read;
684  static const unsigned numKids = 1;
685 
686 public:
689 
690 public:
691  static ref<Expr> alloc(const UpdateList &updates, const ref<Expr> &index) {
692  ref<Expr> r(new ReadExpr(updates, index));
693  r->computeHash();
694  return r;
695  }
696 
697  static ref<Expr> create(const UpdateList &updates, ref<Expr> i);
698 
699  Width getWidth() const { assert(updates.root); return updates.root->getRange(); }
700  Kind getKind() const { return Read; }
701 
702  unsigned getNumKids() const { return numKids; }
703  ref<Expr> getKid(unsigned i) const { return !i ? index : 0; }
704 
705  int compareContents(const Expr &b) const;
706 
707  virtual ref<Expr> rebuild(ref<Expr> kids[]) const {
708  return create(updates, kids[0]);
709  }
710 
711  virtual unsigned computeHash();
712 
713 private:
714  ReadExpr(const UpdateList &_updates, const ref<Expr> &_index) :
715  updates(_updates), index(_index) { assert(updates.root); }
716 
717 public:
718  static bool classof(const Expr *E) {
719  return E->getKind() == Expr::Read;
720  }
721  static bool classof(const ReadExpr *) { return true; }
722 };
723 
724 
726 class SelectExpr : public NonConstantExpr {
727 public:
728  static const Kind kind = Select;
729  static const unsigned numKids = 3;
730 
731 public:
733 
734 public:
735  static ref<Expr> alloc(const ref<Expr> &c, const ref<Expr> &t,
736  const ref<Expr> &f) {
737  ref<Expr> r(new SelectExpr(c, t, f));
738  r->computeHash();
739  return r;
740  }
741 
742  static ref<Expr> create(ref<Expr> c, ref<Expr> t, ref<Expr> f);
743 
744  Width getWidth() const { return trueExpr->getWidth(); }
745  Kind getKind() const { return Select; }
746 
747  unsigned getNumKids() const { return numKids; }
748  ref<Expr> getKid(unsigned i) const {
749  switch(i) {
750  case 0: return cond;
751  case 1: return trueExpr;
752  case 2: return falseExpr;
753  default: return 0;
754  }
755  }
756 
757  static bool isValidKidWidth(unsigned kid, Width w) {
758  if (kid == 0)
759  return w == Bool;
760  else
761  return true;
762  }
763 
764  virtual ref<Expr> rebuild(ref<Expr> kids[]) const {
765  return create(kids[0], kids[1], kids[2]);
766  }
767 
768 private:
769  SelectExpr(const ref<Expr> &c, const ref<Expr> &t, const ref<Expr> &f)
770  : cond(c), trueExpr(t), falseExpr(f) {}
771 
772 public:
773  static bool classof(const Expr *E) {
774  return E->getKind() == Expr::Select;
775  }
776  static bool classof(const SelectExpr *) { return true; }
777 };
778 
779 
783 class ConcatExpr : public NonConstantExpr {
784 public:
785  static const Kind kind = Concat;
786  static const unsigned numKids = 2;
787 
788 private:
791 
792 public:
793  static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) {
794  ref<Expr> c(new ConcatExpr(l, r));
795  c->computeHash();
796  return c;
797  }
798 
799  static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r);
800 
801  Width getWidth() const { return width; }
802  Kind getKind() const { return kind; }
803  ref<Expr> getLeft() const { return left; }
804  ref<Expr> getRight() const { return right; }
805 
806  unsigned getNumKids() const { return numKids; }
807  ref<Expr> getKid(unsigned i) const {
808  if (i == 0) return left;
809  else if (i == 1) return right;
810  else return NULL;
811  }
812 
814  static ref<Expr> createN(unsigned nKids, const ref<Expr> kids[]);
815  static ref<Expr> create4(const ref<Expr> &kid1, const ref<Expr> &kid2,
816  const ref<Expr> &kid3, const ref<Expr> &kid4);
817  static ref<Expr> create8(const ref<Expr> &kid1, const ref<Expr> &kid2,
818  const ref<Expr> &kid3, const ref<Expr> &kid4,
819  const ref<Expr> &kid5, const ref<Expr> &kid6,
820  const ref<Expr> &kid7, const ref<Expr> &kid8);
821 
822  virtual ref<Expr> rebuild(ref<Expr> kids[]) const { return create(kids[0], kids[1]); }
823 
824 private:
825  ConcatExpr(const ref<Expr> &l, const ref<Expr> &r) : left(l), right(r) {
826  width = l->getWidth() + r->getWidth();
827  }
828 
829 public:
830  static bool classof(const Expr *E) {
831  return E->getKind() == Expr::Concat;
832  }
833  static bool classof(const ConcatExpr *) { return true; }
834 };
835 
836 
841 class ExtractExpr : public NonConstantExpr {
842 public:
843  static const Kind kind = Extract;
844  static const unsigned numKids = 1;
845 
846 public:
848  unsigned offset;
850 
851 public:
852  static ref<Expr> alloc(const ref<Expr> &e, unsigned o, Width w) {
853  ref<Expr> r(new ExtractExpr(e, o, w));
854  r->computeHash();
855  return r;
856  }
857 
859  static ref<Expr> create(ref<Expr> e, unsigned bitOff, Width w);
860 
861  Width getWidth() const { return width; }
862  Kind getKind() const { return Extract; }
863 
864  unsigned getNumKids() const { return numKids; }
865  ref<Expr> getKid(unsigned i) const { return expr; }
866 
867  int compareContents(const Expr &b) const {
868  const ExtractExpr &eb = static_cast<const ExtractExpr&>(b);
869  if (offset != eb.offset) return offset < eb.offset ? -1 : 1;
870  if (width != eb.width) return width < eb.width ? -1 : 1;
871  return 0;
872  }
873 
874  virtual ref<Expr> rebuild(ref<Expr> kids[]) const {
875  return create(kids[0], offset, width);
876  }
877 
878  virtual unsigned computeHash();
879 
880 private:
881  ExtractExpr(const ref<Expr> &e, unsigned b, Width w)
882  : expr(e),offset(b),width(w) {}
883 
884 public:
885  static bool classof(const Expr *E) {
886  return E->getKind() == Expr::Extract;
887  }
888  static bool classof(const ExtractExpr *) { return true; }
889 };
890 
891 
895 class NotExpr : public NonConstantExpr {
896 public:
897  static const Kind kind = Not;
898  static const unsigned numKids = 1;
899 
901 
902 public:
903  static ref<Expr> alloc(const ref<Expr> &e) {
904  ref<Expr> r(new NotExpr(e));
905  r->computeHash();
906  return r;
907  }
908 
909  static ref<Expr> create(const ref<Expr> &e);
910 
911  Width getWidth() const { return expr->getWidth(); }
912  Kind getKind() const { return Not; }
913 
914  unsigned getNumKids() const { return numKids; }
915  ref<Expr> getKid(unsigned i) const { return expr; }
916 
917  int compareContents(const Expr &b) const {
918  const NotExpr &eb = static_cast<const NotExpr&>(b);
919  if (expr != eb.expr) return expr < eb.expr ? -1 : 1;
920  return 0;
921  }
922 
923  virtual ref<Expr> rebuild(ref<Expr> kids[]) const {
924  return create(kids[0]);
925  }
926 
927  virtual unsigned computeHash();
928 
929 public:
930  static bool classof(const Expr *E) {
931  return E->getKind() == Expr::Not;
932  }
933  static bool classof(const NotExpr *) { return true; }
934 
935 private:
936  NotExpr(const ref<Expr> &e) : expr(e) {}
937 };
938 
939 
940 
941 // Casting
942 
943 class CastExpr : public NonConstantExpr {
944 public:
947 
948 public:
949  CastExpr(const ref<Expr> &e, Width w) : src(e), width(w) {}
950 
951  Width getWidth() const { return width; }
952 
953  unsigned getNumKids() const { return 1; }
954  ref<Expr> getKid(unsigned i) const { return (i==0) ? src : 0; }
955 
956  static bool needsResultType() { return true; }
957 
958  int compareContents(const Expr &b) const {
959  const CastExpr &eb = static_cast<const CastExpr&>(b);
960  if (width != eb.width) return width < eb.width ? -1 : 1;
961  return 0;
962  }
963 
964  virtual unsigned computeHash();
965 
966  static bool classof(const Expr *E) {
967  Expr::Kind k = E->getKind();
968  return Expr::CastKindFirst <= k && k <= Expr::CastKindLast;
969  }
970  static bool classof(const CastExpr *) { return true; }
971 };
972 
973 #define CAST_EXPR_CLASS(_class_kind) \
974 class _class_kind ## Expr : public CastExpr { \
975 public: \
976  static const Kind kind = _class_kind; \
977  static const unsigned numKids = 1; \
978 public: \
979  _class_kind ## Expr(ref<Expr> e, Width w) : CastExpr(e,w) {} \
980  static ref<Expr> alloc(const ref<Expr> &e, Width w) { \
981  ref<Expr> r(new _class_kind ## Expr(e, w)); \
982  r->computeHash(); \
983  return r; \
984  } \
985  static ref<Expr> create(const ref<Expr> &e, Width w); \
986  Kind getKind() const { return _class_kind; } \
987  virtual ref<Expr> rebuild(ref<Expr> kids[]) const { \
988  return create(kids[0], width); \
989  } \
990  \
991  static bool classof(const Expr *E) { \
992  return E->getKind() == Expr::_class_kind; \
993  } \
994  static bool classof(const _class_kind ## Expr *) { \
995  return true; \
996  } \
997 }; \
998 
999 CAST_EXPR_CLASS(SExt)
1000 CAST_EXPR_CLASS(ZExt)
1001 
1002 // Arithmetic/Bit Exprs
1003 
1004 #define ARITHMETIC_EXPR_CLASS(_class_kind) \
1005 class _class_kind ## Expr : public BinaryExpr { \
1006 public: \
1007  static const Kind kind = _class_kind; \
1008  static const unsigned numKids = 2; \
1009 public: \
1010  _class_kind ## Expr(const ref<Expr> &l, \
1011  const ref<Expr> &r) : BinaryExpr(l,r) {} \
1012  static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) { \
1013  ref<Expr> res(new _class_kind ## Expr (l, r)); \
1014  res->computeHash(); \
1015  return res; \
1016  } \
1017  static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r); \
1018  Width getWidth() const { return left->getWidth(); } \
1019  Kind getKind() const { return _class_kind; } \
1020  virtual ref<Expr> rebuild(ref<Expr> kids[]) const { \
1021  return create(kids[0], kids[1]); \
1022  } \
1023  \
1024  static bool classof(const Expr *E) { \
1025  return E->getKind() == Expr::_class_kind; \
1026  } \
1027  static bool classof(const _class_kind ## Expr *) { \
1028  return true; \
1029  } \
1030 }; \
1031 
1045 
1046 // Comparison Exprs
1047 
1048 #define COMPARISON_EXPR_CLASS(_class_kind) \
1049 class _class_kind ## Expr : public CmpExpr { \
1050 public: \
1051  static const Kind kind = _class_kind; \
1052  static const unsigned numKids = 2; \
1053 public: \
1054  _class_kind ## Expr(const ref<Expr> &l, \
1055  const ref<Expr> &r) : CmpExpr(l,r) {} \
1056  static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) { \
1057  ref<Expr> res(new _class_kind ## Expr (l, r)); \
1058  res->computeHash(); \
1059  return res; \
1060  } \
1061  static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r); \
1062  Kind getKind() const { return _class_kind; } \
1063  virtual ref<Expr> rebuild(ref<Expr> kids[]) const { \
1064  return create(kids[0], kids[1]); \
1065  } \
1066  \
1067  static bool classof(const Expr *E) { \
1068  return E->getKind() == Expr::_class_kind; \
1069  } \
1070  static bool classof(const _class_kind ## Expr *) { \
1071  return true; \
1072  } \
1073 }; \
1074 
1085 
1086 // Implementations
1087 
1088 inline bool Expr::isZero() const {
1089  if (const ConstantExpr *CE = dyn_cast<ConstantExpr>(this))
1090  return CE->isZero();
1091  return false;
1092 }
1093 
1094 inline bool Expr::isTrue() const {
1095  assert(getWidth() == Expr::Bool && "Invalid isTrue() call!");
1096  if (const ConstantExpr *CE = dyn_cast<ConstantExpr>(this))
1097  return CE->isTrue();
1098  return false;
1099 }
1100 
1101 inline bool Expr::isFalse() const {
1102  assert(getWidth() == Expr::Bool && "Invalid isFalse() call!");
1103  if (const ConstantExpr *CE = dyn_cast<ConstantExpr>(this))
1104  return CE->isFalse();
1105  return false;
1106 }
1107 
1108 } // End klee namespace
1109 
1110 #endif
ref< Expr > getKid(unsigned i) const
Definition: Expr.h:553
bool isFalse() const
isFalse - Is this the false expression.
Definition: Expr.h:437
virtual int compareContents(const Expr &b) const
Definition: Expr.h:207
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
ConcatExpr(const ref< Expr > &l, const ref< Expr > &r)
Definition: Expr.h:825
unsigned hashValue
Definition: Expr.h:174
static bool classof(const ConstantExpr *)
Definition: Expr.h:421
virtual unsigned computeHash()
Definition: Expr.cpp:201
unsigned hashValue
Definition: Expr.h:651
void extend(const ref< Expr > &index, const ref< Expr > &value)
Definition: Updates.cpp:90
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
unsigned hash() const
Definition: Updates.cpp:128
virtual ref< Expr > rebuild(ref< Expr > kids[]) const
Definition: Expr.h:923
ref< ConstantExpr > URem(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:400
ref< ConstantExpr > Ne(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:440
unsigned getNumKids() const
Definition: Expr.h:953
ReadExpr(const UpdateList &_updates, const ref< Expr > &_index)
Definition: Expr.h:714
ref< Expr > left
Definition: Expr.h:494
static bool classof(const NotOptimizedExpr *)
Definition: Expr.h:564
static bool classof(const Expr *E)
Definition: Expr.h:885
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
static bool isValidKidWidth(unsigned kid, Width w)
Definition: Expr.h:251
virtual ref< Expr > rebuild(ref< Expr > kids[]) const =0
bool operator>(const Expr &lhs, const Expr &rhs)
Definition: Expr.h:282
Not used in canonical form.
Definition: Expr.h:151
Width width
Definition: Expr.h:789
virtual unsigned getNumKids() const =0
static bool classof(const ConcatExpr *)
Definition: Expr.h:833
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
ref< ConstantExpr > Or(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:412
static bool classof(const Expr *E)
Definition: Expr.h:510
ref< ConstantExpr > SDiv(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:396
ref< ConstantExpr > SRem(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:404
virtual ref< Expr > rebuild(ref< Expr > kids[]) const
Definition: Expr.h:764
NotOptimizedExpr(const ref< Expr > &_src)
Definition: Expr.h:558
unsigned size
Definition: Expr.h:605
#define ARITHMETIC_EXPR_CLASS(_class_kind)
Definition: Expr.h:1004
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
ref< Expr > trueExpr
Definition: Expr.h:732
ref< Expr > expr
Definition: Expr.h:900
static const Kind kind
Definition: Expr.h:843
UpdateList(const Array *_root, const UpdateNode *_head)
Definition: Updates.cpp:59
static bool classof(const Expr *E)
Definition: Expr.h:930
ref< ConstantExpr > Mul(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:388
static bool classof(const SelectExpr *)
Definition: Expr.h:776
int compareContents(const Expr &b) const
Definition: Expr.cpp:523
llvm::raw_ostream & operator<<(llvm::raw_ostream &os, const MemoryMap &mm)
static ref< Expr > create(ref< Expr > c, ref< Expr > t, ref< Expr > f)
Definition: Expr.cpp:527
static const Kind kind
Definition: Expr.h:785
ref< ConstantExpr > Not()
Definition: Expr.cpp:432
ConstantExpr(const llvm::APInt &v)
Definition: Expr.h:335
bool isOne() const
isOne - Is this a constant one.
Definition: Expr.h:429
static const Width Fl80
Definition: Expr.h:102
ref< Expr > getKid(unsigned i) const
Definition: Expr.h:865
NotExpr(const ref< Expr > &e)
Definition: Expr.h:936
static const unsigned numKids
Definition: Expr.h:898
static bool classof(const Expr *)
Definition: Expr.h:254
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
int compare(const Expr &b) const
Definition: Expr.h:201
static bool needsResultType()
Definition: Expr.h:252
const std::vector< ref< ConstantExpr > > constantValues
Definition: Expr.h:610
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< ConstantExpr > alloc(uint64_t v, Width w)
Definition: Expr.h:408
static const Kind kind
Definition: Expr.h:728
Kind getKind() const
Definition: Expr.h:802
ref< ConstantExpr > And(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:408
unsigned refCount
Definition: Expr.h:171
virtual unsigned hash() const
Returns the pre-computed hash of the current expression.
Definition: Expr.h:192
Class representing a complete list of updates into an array.
Definition: Expr.h:655
static bool classof(const BinaryExpr *)
Definition: Expr.h:514
static const Kind kind
Definition: Expr.h:897
unsigned getNumKids() const
Definition: Expr.h:343
virtual ref< Expr > rebuild(ref< Expr > kids[]) const
Definition: Expr.h:822
static const unsigned numKids
Definition: Expr.h:844
UpdateList updates
Definition: Expr.h:687
Not used in canonical form.
Definition: Expr.h:155
uint64_t getZExtValue(unsigned bits=64) const
Definition: Expr.h:361
static bool classof(const Expr *E)
Definition: Expr.h:561
bool isZero() const
isZero - Is this a constant zero.
Definition: Expr.h:1088
static bool classof(const NonConstantExpr *)
Definition: Expr.h:489
static const unsigned numKids
Definition: Expr.h:729
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
Expr::Width range
Definition: Expr.h:612
Class representing an if-then-else expression.
Definition: Expr.h:726
static bool classof(const Expr *E)
Definition: Expr.h:718
#define COMPARISON_EXPR_CLASS(_class_kind)
Definition: Expr.h:1048
unsigned offset
Definition: Expr.h:848
virtual ref< Expr > rebuild(ref< Expr > kids[]) const
Definition: Expr.h:555
Width getWidth() const
Definition: Expr.h:801
ref< Expr > value
Definition: Expr.h:578
unsigned getNumKids() const
Definition: Expr.h:497
bool operator!=(const Expr &lhs, const Expr &rhs)
Definition: Expr.h:278
Not used in canonical form.
Definition: Expr.h:154
static const Width Int32
Definition: Expr.h:100
Class representing symbolic expressions.
Definition: Expr.h:88
uint64_t getLimitedValue(uint64_t Limit=~0ULL) const
Definition: Expr.h:368
static const unsigned numKids
Definition: Expr.h:684
static const Width Int8
Definition: Expr.h:98
bool isAllOnes() const
isAllOnes - Is this constant all ones.
Definition: Expr.h:442
unsigned hash() const
Definition: Expr.h:592
Not used in canonical form.
Definition: Expr.h:158
#define CAST_EXPR_CLASS(_class_kind)
Definition: Expr.h:973
unsigned getNumKids() const
Definition: Expr.h:747
ref< Expr > src
Definition: Expr.h:945
virtual Width getWidth() const =0
unsigned getNumKids() const
Definition: Expr.h:702
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 bool classof(const Expr *E)
Definition: Expr.h:526
virtual ref< Expr > getKid(unsigned i) const =0
BinaryExpr(const ref< Expr > &l, const ref< Expr > &r)
Definition: Expr.h:507
ref< Expr > src
Definition: Expr.h:539
static ref< ConstantExpr > createPointer(uint64_t v)
Definition: Context.cpp:51
static const Width Int64
Definition: Expr.h:101
static ref< Expr > createFromKind(Kind k, std::vector< CreateArg > args)
Definition: Expr.cpp:213
unsigned hashValue
Definition: Expr.h:574
static ref< Expr > createZExtToPointerWidth(ref< Expr > e)
Definition: Context.cpp:47
int compareContents(const Expr &b) const
Definition: Expr.h:917
Kind getKind() const
Definition: Expr.h:912
bool isTrue() const
isTrue - Is this the true expression.
Definition: Expr.h:432
ref< ConstantExpr > Sle(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:464
CastExpr(const ref< Expr > &e, Width w)
Definition: Expr.h:949
Width getWidth() const
Definition: Expr.h:699
ref< ConstantExpr > Ule(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:448
static const unsigned numKids
Definition: Expr.h:330
virtual unsigned computeHash()
Definition: Expr.cpp:194
UpdateList & operator=(const UpdateList &b)
Definition: Updates.cpp:82
bool isFalse() const
isFalse - Is this the false expression.
Definition: Expr.h:1101
Kind getKind() const
Definition: Expr.h:745
Width getWidth() const
Definition: Expr.h:861
int compareContents(const Expr &b) const
Definition: Expr.h:958
static bool classof(const NotExpr *)
Definition: Expr.h:933
static ref< Expr > createTempRead(const Array *array, Expr::Width w)
Definition: Expr.cpp:40
static ref< Expr > createIsZero(ref< Expr > e)
Definition: Expr.cpp:305
static bool needsResultType()
Definition: Expr.h:956
bool operator<=(const Expr &lhs, const Expr &rhs)
Definition: Expr.h:286
ref< ConstantExpr > Sgt(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:468
virtual ref< Expr > rebuild(ref< Expr > kids[]) const
Definition: Expr.h:707
Width getWidth() const
Definition: Expr.h:911
unsigned hash() const
Definition: Expr.h:648
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
virtual unsigned computeHash()
Definition: Expr.cpp:188
ref< Expr > getKid(unsigned i) const
Definition: Expr.h:498
Width getWidth() const
Definition: Expr.h:549
int compare(const Expr &b, ExprEquivSet &equivs) const
Definition: Expr.cpp:87
static const Kind kind
Definition: Expr.h:329
static unsigned count
Definition: Expr.h:90
unsigned getNumKids() const
Definition: Expr.h:864
ref< Expr > left
Definition: Expr.h:790
static bool classof(const Expr *E)
Definition: Expr.h:773
static ref< Expr > alloc(const ref< Expr > &e)
Definition: Expr.h:903
Expr()
Definition: Expr.h:177
int compareContents(const Expr &b) const
Definition: Expr.h:379
bool isTrue() const
isTrue - Is this the true expression.
Definition: Expr.h:1094
virtual unsigned computeHash()
Definition: Expr.cpp:166
static bool isValidKidWidth(unsigned kid, Width w)
Definition: Expr.h:757
const std::string name
Definition: Expr.h:603
bool operator==(const Expr &lhs, const Expr &rhs)
Definition: Expr.h:270
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
Array(const std::string &_name, uint64_t _size, const ref< ConstantExpr > *constantValuesBegin=0, const ref< ConstantExpr > *constantValuesEnd=0, Expr::Width _domain=Expr::Int32, Expr::Width _range=Expr::Int8)
Definition: Expr.h:622
static ref< ConstantExpr > alloc(const llvm::APFloat &f)
Definition: Expr.h:404
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 > create(ref< Expr > src)
Definition: Expr.cpp:478
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:398
static const unsigned numKids
Definition: Expr.h:538
Kind getKind() const
Definition: Expr.h:700
static bool classof(const Expr *E)
Definition: Expr.h:830
ref< Expr > expr
Definition: Expr.h:847
Expr::Width domain
Definition: Expr.h:612
CreateArg(ref< Expr > e)
Definition: Expr.h:262
unsigned getSize() const
Definition: Expr.h:589
ref< ConstantExpr > Ugt(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:452
static unsigned getMinBytesForWidth(Width w)
returns the smallest number of bytes in which the given width fits
Definition: Expr.h:230
Expr::Width getRange() const
Definition: Expr.h:645
virtual ref< Expr > rebuild(ref< Expr > kids[]) const
Definition: Expr.h:874
virtual unsigned computeHash()
Definition: Expr.cpp:179
static bool classof(const CmpExpr *)
Definition: Expr.h:530
ref< Expr > right
Definition: Expr.h:494
static const Kind kind
Definition: Expr.h:537
int compareContents(const Expr &b) const
Definition: Expr.h:867
static bool classof(const Expr *E)
Definition: Expr.h:486
const UpdateNode * next
Definition: Expr.h:577
Kind getKind() const
Definition: Expr.h:862
ref< ConstantExpr > Shl(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:420
CmpExpr(ref< Expr > l, ref< Expr > r)
Definition: Expr.h:521
static ref< Expr > createImplies(ref< Expr > hyp, ref< Expr > conc)
Definition: Expr.cpp:301
bool isConstantArray() const
Definition: Expr.h:642
static const unsigned numKids
Definition: Expr.h:786
bool operator<(const Expr &lhs, const Expr &rhs)
Definition: Expr.h:274
Expr::Width getDomain() const
Definition: Expr.h:644
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
unsigned size
size of this update sequence, including this update
Definition: Expr.h:582
const Array * root
Definition: Expr.h:659
Width width
Definition: Expr.h:946
virtual Kind getKind() const =0
static bool classof(const ReadExpr *)
Definition: Expr.h:721
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
Kind getKind() const
Definition: Expr.h:341
Width getWidth() const
Definition: Expr.h:340
ref< ConstantExpr > LShr(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:424
Width getWidth() const
Definition: Expr.h:524
unsigned computeHash()
Definition: Expr.cpp:489
ref< Expr > index
Definition: Expr.h:688
static ref< Expr > createSExtToPointerWidth(ref< Expr > e)
Definition: Context.cpp:43
Class representing a byte update of an array.
Definition: Expr.h:569
unsigned getNumKids() const
Definition: Expr.h:806
ref< ConstantExpr > SExt(Width W)
Definition: Expr.cpp:372
ref< Expr > cond
Definition: Expr.h:732
bool operator>=(const Expr &lhs, const Expr &rhs)
Definition: Expr.h:290
void dump() const
dump - Print the expression to stderr.
Definition: Expr.cpp:313
ref< Expr > right
Definition: Expr.h:790
static ref< Expr > alloc(const ref< Expr > &c, const ref< Expr > &t, const ref< Expr > &f)
Definition: Expr.h:735
virtual ~Expr()
Definition: Expr.h:178
static bool classof(const Expr *E)
Definition: Expr.h:418
static const Width Bool
Definition: Expr.h:97
virtual ref< Expr > rebuild(ref< Expr > kids[]) const
Definition: Expr.h:388
Not used in canonical form.
Definition: Expr.h:159
ref< Expr > getKid(unsigned i) const
Definition: Expr.h:748
ref< ConstantExpr > Concat(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:354
uint64_t truncateToNBits(uint64_t x, unsigned N)
Definition: Bits.h:71
ref< Expr > getKid(unsigned i) const
Definition: Expr.h:915
ref< Expr > getKid(unsigned i) const
Definition: Expr.h:703
ref< ConstantExpr > ZExt(Width W)
Definition: Expr.cpp:368
ref< Expr > expr
Definition: Expr.h:258
SelectExpr(const ref< Expr > &c, const ref< Expr > &t, const ref< Expr > &f)
Definition: Expr.h:769
ExtractExpr(const ref< Expr > &e, unsigned b, Width w)
Definition: Expr.h:881
void toMemory(void *address)
Definition: Expr.cpp:335
unsigned computeHash()
Definition: Updates.cpp:50
ref< ConstantExpr > Sge(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:472
static ref< Expr > create(const ref< Expr > &e)
Definition: Expr.cpp:640
ref< Expr > getRight() const
Definition: Expr.h:804
static ref< Expr > fromMemory(void *address, Width w)
Definition: Expr.cpp:320
int compare(const UpdateList &b) const
Definition: Updates.cpp:102
static const Width InvalidWidth
Definition: Expr.h:96
unsigned refCount
Definition: Expr.h:572
unsigned getNumKids() const
Definition: Expr.h:914
static bool classof(const Expr *E)
Definition: Expr.h:966
Width getWidth() const
Definition: Expr.h:744
ref< Expr > falseExpr
Definition: Expr.h:732
CreateArg(Width w=Bool)
Definition: Expr.h:261
ref< ConstantExpr > Slt(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:460
Width width
Definition: Expr.h:849
static bool classof(const ExtractExpr *)
Definition: Expr.h:888
virtual unsigned computeHash()
Definition: Expr.cpp:208
ref< Expr > getKid(unsigned i) const
Definition: Expr.h:807
static ref< Expr > alloc(const ref< Expr > &e, unsigned o, Width w)
Definition: Expr.h:852
static const Kind kind
Definition: Expr.h:683
Kind getKind() const
Definition: Expr.h:550
ref< Expr > getLeft() const
Definition: Expr.h:803
int compare(const UpdateNode &b) const
Definition: Updates.cpp:44
ref< Expr > getKid(unsigned i) const
Definition: Expr.h:954
ref< ConstantExpr > Add(const ref< ConstantExpr > &RHS)
Definition: Expr.cpp:376
const llvm::APInt & getAPValue() const
Definition: Expr.h:350
Width getWidth() const
Definition: Expr.h:951
unsigned getNumKids() const
Definition: Expr.h:552
ref< Expr > getKid(unsigned i) const
Definition: Expr.h:344
static bool classof(const CastExpr *)
Definition: Expr.h:970