 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
18.0% |
29 / 161 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
28.0% |
45 / 161 |
| |
|
Line Coverage: |
85.8% |
157 / 183 |
| |
 |
|
 |
1 : //===- Expr.h - --*- C++ -*-===//
2 :
3 : #ifndef KLEE_EXPR_H
4 : #define KLEE_EXPR_H
5 :
6 : #include "Machine.h"
7 : #include "klee/util/Bits.h"
8 :
9 : #include "llvm/Support/Streams.h"
10 : #include "llvm/ADT/SmallVector.h"
11 :
12 : #include <set>
13 : #include <vector>
14 :
15 : namespace llvm {
16 : class Type;
17 : }
18 :
19 : namespace klee {
20 : namespace serialize {
21 : class access;
22 : }
23 :
24 : class ConstantExpr;
25 : class ObjectState;
26 : class MemoryObject;
27 :
28 : template<class T> class ref;
29 :
30 :
31 : /// Class representing symbolic expressions.
32 : /**
33 :
34 : <b>Expression canonicalization</b>: we define certain rules for
35 : canonicalization rules for Exprs in order to simplify code that
36 : pattern matches Exprs (since the number of forms are reduced), to open
37 : up further chances for optimization, and to increase similarity for
38 : caching and other purposes.
39 :
40 : The general rules are:
41 : <ol>
42 : <li> No Expr has all constant arguments.</li>
43 :
44 : <li> Booleans:
45 : <ol type="a">
46 : <li> Boolean not is written as <tt>(false == ?)</tt> </li>
47 : <li> \c Ne, \c Ugt, \c Uge, \c Sgt, \c Sge are not used </li>
48 : <li> The only acceptable operations with boolean arguments are \c And,
49 : \c Or, \c Xor, \c Eq, as well as \c SExt, \c ZExt,
50 : \c Select and \c NotOptimized. </li>
51 : <li> The only boolean operation which may involve a constant is boolean not (<tt>== false</tt>). </li>
52 : </ol>
53 : </li>
54 :
55 : <li> Linear Formulas:
56 : <ol type="a">
57 : <li> For any subtree representing a linear formula, a constant
58 : term must be on the LHS of the root node of the subtree. In particular,
59 : in a BinaryExpr a constant must always be on the LHS. For example, subtraction
60 : by a constant c is written as <tt>add(-c, ?)</tt>. </li>
61 : </ol>
62 : </li>
63 :
64 :
65 : <li> Chains are unbalanced to the right </li>
66 :
67 : </ol>
68 :
69 :
70 : <b>Steps required for adding an expr</b>:
71 : -# Add case to printKind
72 : -# Add to ExprVisitor
73 : -# Add to IVC (implied value concretization) if possible
74 :
75 : Todo: Shouldn't bool \c Xor just be written as not equal?
76 :
77 : */
78 :
79 : class Expr {
80 : public:
81 : static unsigned count;
82 : static const unsigned MAGIC_HASH_CONSTANT = 39;
83 :
84 : /// The type of an expression is simply its width, in bits.
85 : typedef unsigned Width;
86 :
87 : static const Width InvalidWidth = 0;
88 : static const Width Bool = 1;
89 : static const Width Int8 = 8;
90 : static const Width Int16 = 16;
91 : static const Width Int32 = 32;
92 : static const Width Int64 = 64;
93 :
94 :
95 : enum Kind {
96 : InvalidKind = -1,
97 :
98 : // Primitive
99 :
100 : Constant = 0,
101 :
102 : // Special
103 :
104 : /// Prevents optimization below the given expression. Used for
105 : /// testing: make equality constraints that KLEE will not use to
106 : /// optimize to concretes.
107 : NotOptimized,
108 :
109 : //// Skip old varexpr, just for deserialization, purge at some point
110 : Read=NotOptimized+2,
111 : Select,
112 : Concat,
113 : Extract,
114 :
115 : // Casting,
116 :
117 : ZExt,
118 : SExt,
119 :
120 : // Arithmetic
121 : Add,
122 : Sub,
123 : Mul,
124 : UDiv,
125 : SDiv,
126 : URem,
127 : SRem,
128 :
129 : // Bit
130 : And,
131 : Or,
132 : Xor,
133 : Shl,
134 : LShr,
135 : AShr,
136 :
137 : // Compare
138 : Eq,
139 : Ne, /// Not used in canonical form
140 : Ult,
141 : Ule,
142 : Ugt, /// Not used in canonical form
143 : Uge, /// Not used in canonical form
144 : Slt,
145 : Sle,
146 : Sgt, /// Not used in canonical form
147 : Sge, /// Not used in canonical form
148 :
149 : LastKind=Sge
150 : };
151 :
152 : unsigned refCount;
153 :
154 : protected:
155 : unsigned hashValue;
156 :
157 : public:
158 63349: Expr() : refCount(0) { Expr::count++; }
0: branch 0 not taken
63349: branch 1 taken
0: branch 3 not taken
0: branch 4 not taken
0: branch 6 not taken
0: branch 7 not taken
159 63349: virtual ~Expr() { Expr::count--; }
160 :
161 : virtual Kind getKind() const = 0;
162 : virtual Width getWidth() const = 0;
163 :
164 : virtual unsigned getNumKids() const = 0;
165 : virtual ref<Expr> getKid(unsigned i) const = 0;
166 :
167 : virtual void print(std::ostream &os) const;
168 :
169 : /// Returns the pre-computed hash of the current expression
170 2561309: virtual unsigned hash() const { return hashValue; }
171 :
172 : /// (Re)computes the hash of the current expression.
173 : /// Returns the hash value.
174 : virtual unsigned computeHash();
175 :
176 : static unsigned hashConstant(uint64_t val, Width w) {
177 45159: return val ^ (w * MAGIC_HASH_CONSTANT);
178 : }
179 :
180 : /// Returns 0 iff b is structuraly equivalent to *this
181 : int compare(const Expr &b) const;
182 957189: virtual int compareContents(const Expr &b) const { return 0; }
183 :
184 : // Given an array of new kids return a copy of the expression
185 : // but using those children.
186 : virtual ref<Expr> rebuild(ref<Expr> kids[/* getNumKids() */]) const = 0;
187 :
188 : ///
189 :
190 : uint64_t getConstantValue() const;
191 :
192 : /* Static utility methods */
193 :
194 : static void printKind(std::ostream &os, Kind k);
195 : static void printWidth(std::ostream &os, Expr::Width w);
196 : static Width getWidthForLLVMType(const llvm::Type *type);
197 :
198 : /// returns the smallest number of bytes in which the given width fits
199 : static inline unsigned getMinBytesForWidth(Width w) {
200 3407229: return (w + 7) / 8;
201 : }
202 :
203 : /* Kind utilities */
204 :
205 : /* Utility creation functions */
206 : static ref<Expr> createCoerceToPointerType(ref<Expr> e);
207 : static ref<Expr> createNot(ref<Expr> e);
208 : static ref<Expr> createImplies(ref<Expr> hyp, ref<Expr> conc);
209 : static ref<Expr> createIsZero(ref<Expr> e);
210 :
211 : /// Create a little endian read of the given type at offset 0 of the
212 : /// given object.
213 : static ref<Expr> createTempRead(const MemoryObject *mo, Expr::Width w);
214 :
215 : static ref<Expr> createPointer(uint64_t v);
216 :
217 : // do not use
218 : static Expr *createConstant(uint64_t val, Width w);
219 :
220 : struct CreateArg;
221 : static ref<Expr> createFromKind(Kind k, std::vector<CreateArg> args);
222 :
223 1002: static bool isValidKidWidth(unsigned kid, Width w) { return true; }
224 942: static bool needsResultType() { return false; }
225 : };
226 : // END class Expr
227 :
228 :
229 :
230 : #include "klee/util/Ref.h"
231 :
232 24777: struct Expr::CreateArg {
233 : ref<Expr> expr;
234 : Width width;
235 :
236 180: CreateArg(Width w = Bool) : expr(0, Expr::Bool), width(w) {}
237 4068: CreateArg(ref<Expr> e) : expr(e), width(Expr::InvalidWidth) {}
238 :
239 2976: bool isExpr() { return !isWidth(); }
240 3156: bool isWidth() { return width != Expr::InvalidWidth; }
241 : };
242 :
243 : // Comparison operators
244 :
245 : inline bool operator==(const Expr &lhs, const Expr &rhs) {
246 689428: return lhs.compare(rhs) == 0;
247 : }
248 :
249 : inline bool operator<(const Expr &lhs, const Expr &rhs) {
250 : return lhs.compare(rhs) < 0;
251 : }
252 :
253 : inline bool operator!=(const Expr &lhs, const Expr &rhs) {
254 : return !(lhs == rhs);
255 : }
256 :
257 : inline bool operator>(const Expr &lhs, const Expr &rhs) {
258 : return rhs < lhs;
259 : }
260 :
261 : inline bool operator<=(const Expr &lhs, const Expr &rhs) {
262 : return !(lhs > rhs);
263 : }
264 :
265 : inline bool operator>=(const Expr &lhs, const Expr &rhs) {
266 : return !(lhs < rhs);
267 : }
268 :
269 : // Printing operators
270 :
271 : inline std::ostream &operator<<(std::ostream &os, const Expr &e) {
272 206: e.print(os);
273 206: return os;
274 : }
275 :
276 : inline std::ostream &operator<<(std::ostream &os, const Expr::Kind kind) {
277 2525: Expr::printKind(os, kind);
278 2525: return os;
279 : }
280 :
281 : // Terminal Exprs
282 :
283 : class ConstantExpr : public Expr {
284 : public:
285 : static const Kind kind = Constant;
286 : static const unsigned numKids = 0;
287 :
288 : public:
289 : union {
290 : uint64_t asUInt64;
291 : };
292 : Width width;
293 :
294 : public:
643: branch 1 taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
295 643: ~ConstantExpr() {};
296 : // should change the code to make this private
297 1286: ConstantExpr(uint64_t v, Width w) : asUInt64(v), width(w) {}
298 :
299 0: Width getWidth() const { return width; }
300 0: Kind getKind() const { return Constant; }
301 :
302 0: unsigned getNumKids() const { return 0; }
303 0: ref<Expr> getKid(unsigned i) const { return 0; }
304 :
305 0: int compareContents(const Expr &b) const {
306 0: const ConstantExpr &cb = static_cast<const ConstantExpr&>(b);
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
307 0: if (width != cb.width) return width < cb.width ? -1 : 1;
0: branch 0 not taken
0: branch 1 not taken
308 0: if (asUInt64 < cb.asUInt64) {
309 0: return -1;
0: branch 0 not taken
0: branch 1 not taken
310 0: } else if (asUInt64 > cb.asUInt64) {
311 0: return 1;
312 : } else {
313 0: return 0;
314 : }
315 : }
316 :
317 0: virtual ref<Expr> rebuild(ref<Expr> kids[]) const {
318 0: assert(0 && "rebuild() on ConstantExpr");
319 : }
320 :
321 : virtual unsigned computeHash();
322 :
323 : static ref<ConstantExpr> fromMemory(void *address, Width w);
324 : void toMemory(void *address);
325 :
326 : static ref<ConstantExpr> alloc(uint64_t v, Width w) {
327 : // constructs an "optimized" ConstantExpr
328 28927411: return ref<ConstantExpr>(v, w);
329 : }
330 :
331 28927411: static ref<ConstantExpr> create(uint64_t v, Width w) {
332 : assert(v == bits64::truncateToNBits(v, w) &&
0: branch 0 not taken
28927411: branch 1 taken
333 28927411: "invalid constant");
334 28927411: return alloc(v, w);
335 : }
336 : };
337 :
338 :
339 : // Utility classes
340 :
0: branch 9 not taken
0: branch 10 not taken
0: branch 15 not taken
0: branch 16 not taken
341 26964: class BinaryExpr : public Expr {
342 : public:
343 : ref<Expr> left, right;
344 :
345 : public:
346 832623: unsigned getNumKids() const { return 2; }
347 1472694: ref<Expr> getKid(unsigned i) const {
736976: branch 0 taken
735718: branch 1 taken
348 1472694: if(i == 0)
349 736976: return left;
735718: branch 0 taken
0: branch 1 not taken
350 735718: if(i == 1)
351 735718: return right;
352 0: return 0;
353 : }
354 :
355 : protected:
356 107856: BinaryExpr(const ref<Expr> &l, const ref<Expr> &r) : left(l), right(r) {}
357 : BinaryExpr() {}
358 :
359 : private:
360 : friend class serialize::access;
361 : template<typename Archive>
362 1759: void save(Archive &ar) const {
363 3518: ar & left;
364 3518: ar & right;
365 1759: }
366 : template<typename Archive>
367 : void load(Archive &ar, unsigned version) {
368 : ar & left;
369 : ar & right;
370 : }
371 : };
372 :
373 :
0: branch 1 not taken
20018: branch 2 taken
0: branch 5 not taken
0: branch 6 not taken
0: branch 9 not taken
0: branch 10 not taken
374 20018: class CmpExpr : public BinaryExpr {
375 :
376 : protected:
377 20018: CmpExpr(ref<Expr> l, ref<Expr> r) : BinaryExpr(l,r) {}
378 : CmpExpr() {}
379 :
380 : public:
381 59640: Width getWidth() const { return Bool; }
382 : };
383 :
384 : // Special
385 :
1020: branch 2 taken
0: branch 3 not taken
0: branch 7 not taken
0: branch 8 not taken
386 1020: class NotOptimizedExpr : public Expr {
387 : public:
388 : static const Kind kind = NotOptimized;
389 : static const unsigned numKids = 1;
390 : ref<Expr> src;
391 :
392 : static ref<Expr> alloc(const ref<Expr> &src) {
393 2040: ref<Expr> r(new NotOptimizedExpr(src));
394 1020: r.computeHash();
395 : return r;
396 : }
397 :
398 : static ref<Expr> create(ref<Expr> src);
399 :
400 2: Width getWidth() const { return src.getWidth(); }
401 1487527: Kind getKind() const { return NotOptimized; }
402 :
403 5103: unsigned getNumKids() const { return 1; }
404 4083: ref<Expr> getKid(unsigned i) const { return src; }
405 :
406 2: virtual ref<Expr> rebuild(ref<Expr> kids[]) const { return create(kids[0]); }
407 :
408 : private:
409 2040: NotOptimizedExpr(const ref<Expr> &_src) : src(_src) {}
410 :
411 : friend class serialize::access;
412 : NotOptimizedExpr() {}
413 : template<typename Archive>
414 : void save(Archive &ar) const {
415 0: ar & src;
416 : }
417 : template<typename Archive>
418 : void load(Archive &ar, unsigned) {
419 : ar & src;
420 : }
421 : };
422 :
423 :
424 : /// Class representing a byte update of an array.
425 : class UpdateNode {
426 : friend class UpdateList;
427 : friend class STPBuilder; // for setting STPArray
428 :
429 : mutable unsigned refCount;
430 : // gross
431 : mutable void *stpArray;
432 : // cache instead of recalc
433 : unsigned hashValue;
434 :
435 : public:
436 : const UpdateNode *next;
437 : ref<Expr> index, value;
438 :
439 : private:
440 : /// size of this update sequence, including this update
441 : unsigned size;
442 :
443 : public:
444 : UpdateNode(const UpdateNode *_next,
445 : const ref<Expr> &_index,
446 : const ref<Expr> &_value);
447 :
448 56112: unsigned getSize() const { return size; }
449 :
450 : int compare(const UpdateNode &b) const;
451 9722: unsigned hash() const { return hashValue; }
452 :
453 : private:
454 : UpdateNode() : refCount(0), stpArray(0) {}
455 : ~UpdateNode();
456 :
457 : unsigned computeHash();
458 :
459 : friend class serialize::access;
460 : template<class Archive>
461 : void save(Archive &ar) const {
462 406: ar & next;
463 406: ar & size;
464 812: ar & index;
465 812: ar & value;
466 : }
467 : template<class Archive>
468 : void load(Archive &ar, unsigned version) {
469 : ar & const_cast<UpdateNode*&>(next);
470 : ar & size;
471 : ar & index;
472 : ar & value;
473 : if (next)
474 : next->refCount++;
475 : computeHash();
476 : }
477 : };
478 :
479 :
480 : /// Class representing a complete list of updates into an array.
481 : /** The main trick is the isRooted bit, which enables important optimizations.
482 : ...
483 : */
484 : class UpdateList {
485 : friend class ReadExpr; // for default constructor
486 :
487 : public:
488 : // should remove this dependency
489 : const MemoryObject *root;
490 :
491 : /// pointer to the most recent update node
492 : const UpdateNode *head;
493 :
494 : // shouldn't this be part of the ReadExpr?
495 : bool isRooted;
496 :
497 : public:
498 : UpdateList(const MemoryObject *_root, bool isRooted, const UpdateNode *_head);
499 : UpdateList(const UpdateList &b);
500 : ~UpdateList();
501 :
502 : UpdateList &operator=(const UpdateList &b);
503 :
504 : /// size of this update list
14036: branch 0 taken
1178573: branch 1 taken
14036: branch 2 taken
1178573: branch 3 taken
14020: branch 4 taken
1178573: branch 5 taken
14020: branch 6 taken
1178573: branch 7 taken
505 2441330: unsigned getSize() const { return (head ? head->getSize() : 0); }
506 :
507 : void extend(const ref<Expr> &index, const ref<Expr> &value);
508 :
509 : int compare(const UpdateList &b) const;
510 : unsigned hash() const;
511 :
512 : private:
513 : UpdateList() {}
514 :
515 : friend class serialize::access;
516 : template<class Archive>
517 : void save(Archive &ar) const {
518 69: ar & root;
519 69: ar & head;
520 69: ar & isRooted;
521 : }
522 : template<class Archive>
523 : void load(Archive &ar, unsigned version) {
524 : ar & const_cast<MemoryObject*&>(root);
525 : ar & const_cast<UpdateNode*&>(head);
526 : if (version>1) {
527 : ar & isRooted;
528 : } else {
529 : isRooted = true; // conservative
530 : }
531 : if (head)
532 : head->refCount++;
533 : }
534 : };
535 :
536 : /// Class representing a one byte read from an array.
5512: branch 3 taken
537 5512: class ReadExpr : public Expr {
538 : public:
539 : static const Kind kind = Read;
540 : static const unsigned numKids = 1;
541 :
542 : public:
543 : UpdateList updates;
544 : ref<Expr> index;
545 :
546 : public:
547 273: static ref<Expr> alloc(const UpdateList &updates, const ref<Expr> &index) {
548 11024: ref<Expr> r(new ReadExpr(updates, index));
549 5512: r.computeHash();
550 : return r;
551 : }
552 :
553 : static ref<Expr> create(const UpdateList &updates, ref<Expr> i);
554 :
555 22833: Width getWidth() const { return Expr::Int8; }
556 5889803: Kind getKind() const { return Read; }
557 :
558 1248358: unsigned getNumKids() const { return numKids; }
559 2439772: ref<Expr> getKid(unsigned i) const { return !i ? index : 0; }
560 :
561 : int compareContents(const Expr &b) const;
562 :
563 82: virtual ref<Expr> rebuild(ref<Expr> kids[]) const {
564 164: return create(updates, kids[0]);
565 : }
566 :
567 : virtual unsigned computeHash();
568 :
569 : private:
570 : ReadExpr(const UpdateList &_updates, const ref<Expr> &_index) :
571 11024: updates(_updates), index(_index) {}
572 : ReadExpr() {}
573 :
574 : friend class serialize::access;
575 : template<class Archive>
576 : void save(Archive &ar) const {
577 138: ar & updates;
578 138: ar & index;
579 : }
580 : template<class Archive>
581 : void load(Archive &ar, unsigned version) {
582 : ar & updates;
583 : ar & index;
584 : }
585 : };
586 :
587 :
588 : /// Class representing an if-then-else expression.
0: branch 4 not taken
0: branch 5 not taken
0: branch 11 not taken
0: branch 12 not taken
589 425: class SelectExpr : public Expr {
590 : public:
591 : static const Kind kind = Select;
592 : static const unsigned numKids = 3;
593 :
594 : public:
595 : ref<Expr> cond, trueExpr, falseExpr;
596 :
597 : public:
598 : static ref<Expr> alloc(const ref<Expr> &c, const ref<Expr> &t, const ref<Expr> &f) {
599 850: ref<Expr> r(new SelectExpr(c, t, f));
600 425: r.computeHash();
601 : return r;
602 : }
603 :
604 : static ref<Expr> create(ref<Expr> c, ref<Expr> t, ref<Expr> f);
605 :
606 3270: Width getWidth() const { return trueExpr.getWidth(); }
607 1723: Kind getKind() const { return Select; }
608 :
609 500: unsigned getNumKids() const { return numKids; }
610 1365: ref<Expr> getKid(unsigned i) const {
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
611 1365: switch(i) {
612 455: case 0: return cond;
613 455: case 1: return trueExpr;
614 455: case 2: return falseExpr;
615 0: default: return 0;
616 : }
617 : }
618 :
619 : static bool isValidKidWidth(unsigned kid, Width w) {
25: branch 0 taken
10: branch 1 taken
620 35: if (kid == 0)
621 25: return w == Bool;
622 : else
623 10: return true;
624 : }
625 :
626 0: virtual ref<Expr> rebuild(ref<Expr> kids[]) const {
627 0: return create(kids[0], kids[1], kids[2]);
628 : }
629 :
630 : private:
631 : SelectExpr(const ref<Expr> &c, const ref<Expr> &t, const ref<Expr> &f)
632 1700: : cond(c), trueExpr(t), falseExpr(f) {}
633 : SelectExpr() {}
634 :
635 : friend class serialize::access;
636 : template<typename Archive>
637 : void save(Archive &ar) const {
638 0: ar & cond & trueExpr & falseExpr;
639 : }
640 : template<typename Archive>
641 : void load(Archive &ar, unsigned) {
642 : ar & cond & trueExpr & falseExpr;
643 : }
644 : };
645 :
646 :
647 : /** Children of a concat expression can have arbitrary widths.
648 : Kid 0 is the left kid, kid 1 is the right kid.
649 : */
650 3336: class ConcatExpr : public Expr {
651 : public:
652 : static const Kind kind = Concat;
653 : static const unsigned numKids = 2;
654 :
655 : private:
656 : Width width;
657 : ref<Expr> left, right;
658 :
659 : public:
660 : static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) {
661 6672: ref<Expr> c(new ConcatExpr(l, r));
662 3336: c.computeHash();
663 : return c;
664 : }
665 :
666 : static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r);
667 :
668 35533: Width getWidth() const { return width; }
669 4405895: Kind getKind() const { return kind; }
670 126: ref<Expr> getLeft() const { return left; }
671 1029: ref<Expr> getRight() const { return right; }
672 :
673 1042837: unsigned getNumKids() const { return numKids; }
674 3672581: ref<Expr> getKid(unsigned i) const {
675 3672581: if (i == 0) return left;
676 1836100: else if (i == 1) return right;
677 0: else return NULL;
678 : }
679 :
680 : /// Shortcuts to create larger concats. The chain returned is unbalanced to the right
681 : static ref<Expr> createN(unsigned nKids, const ref<Expr> kids[]);
682 : static ref<Expr> create4(const ref<Expr> &kid1, const ref<Expr> &kid2,
683 : const ref<Expr> &kid3, const ref<Expr> &kid4);
684 : static ref<Expr> create8(const ref<Expr> &kid1, const ref<Expr> &kid2,
685 : const ref<Expr> &kid3, const ref<Expr> &kid4,
686 : const ref<Expr> &kid5, const ref<Expr> &kid6,
687 : const ref<Expr> &kid7, const ref<Expr> &kid8);
688 :
689 8221: virtual ref<Expr> rebuild(ref<Expr> kids[]) const { return create(kids[0], kids[1]); }
690 :
691 :
692 : /* These will be eliminated */
693 508: bool is2ByteConcat() const { return false; }
694 508: bool is4ByteConcat() const { return false; }
695 508: bool is8ByteConcat() const { return false; }
696 :
697 : private:
698 10008: ConcatExpr(const ref<Expr> &l, const ref<Expr> &r) : left(l), right(r) {
699 3336: width = l.getWidth() + r.getWidth();
700 : }
701 : ConcatExpr() {}
702 :
703 : friend class serialize::access;
704 : template<typename Archive>
705 : void save(Archive &ar) const {
706 10: ar & left;
707 10: ar & right;
708 : }
709 :
710 : template<typename Archive>
711 : void load(Archive &ar, unsigned) {
712 : ar & left;
713 : ar & right;
714 : width = left.getWidth() + right.getWidth();
715 : }
716 : };
717 :
718 :
719 : /** This class represents an extract from expression {\tt expr}, at
720 : bit offset {\tt offset} of width {\tt width}. Bit 0 is the right most
721 : bit of the expression.
722 : */
723 24125: class ExtractExpr : public Expr {
724 : public:
725 : static const Kind kind = Extract;
726 : static const unsigned numKids = 1;
727 :
728 : public:
729 : ref<Expr> expr;
730 : unsigned offset;
731 : Width width;
732 :
733 : public:
734 : static ref<Expr> alloc(const ref<Expr> &e, unsigned o, Width w) {
735 48250: ref<Expr> r(new ExtractExpr(e, o, w));
736 24125: r.computeHash();
737 : return r;
738 : }
739 :
740 : /// Creates an ExtractExpr with the given bit offset and width
741 : static ref<Expr> create(ref<Expr> e, unsigned bitOff, Width w);
742 :
743 : /// Creates an ExtractExpr with the given byte offset and width
744 : static ref<Expr> createByteOff(ref<Expr> e, unsigned byteOff, Width w=Expr::Int8);
745 :
746 54217: Width getWidth() const { return width; }
747 171036: Kind getKind() const { return Extract; }
748 :
749 9946: unsigned getNumKids() const { return numKids; }
750 13308: ref<Expr> getKid(unsigned i) const { return expr; }
751 :
752 5022: int compareContents(const Expr &b) const {
753 5022: const ExtractExpr &eb = static_cast<const ExtractExpr&>(b);
754 5022: if (offset != eb.offset) return offset < eb.offset ? -1 : 1;
755 5022: if (width != eb.width) return width < eb.width ? -1 : 1;
756 5022: return 0;
757 : }
758 :
759 520: virtual ref<Expr> rebuild(ref<Expr> kids[]) const {
760 1040: return create(kids[0], offset, width);
761 : }
762 :
763 : virtual unsigned computeHash();
764 :
765 : private:
766 72375: ExtractExpr(const ref<Expr> &e, unsigned b, Width w) : expr(e),offset(b),width(w) {}
767 :
768 : friend class serialize::access;
769 : ExtractExpr() {}
770 : template<typename Archive>
771 : void save(Archive &ar) const {
772 42: ar & expr;
773 21: ar & offset;
774 21: ar & (unsigned) width;
775 : }
776 : template<typename Archive>
777 : void load(Archive &ar, unsigned) {
778 : unsigned w;
779 : ar & expr;
780 : ar & offset;
781 : ar & w;
782 : width = (Expr::Width) w;
783 : }
784 : };
785 :
786 :
787 : // Casting
788 :
0: branch 2 not taken
8: branch 3 taken
789 1324: class CastExpr : public Expr {
790 : public:
791 : ref<Expr> src;
792 : Width width;
793 :
794 : public:
795 3972: CastExpr(const ref<Expr> &e, Width w) : src(e), width(w) {}
796 :
797 45411: Width getWidth() const { return width; }
798 :
799 34072: unsigned getNumKids() const { return 1; }
24: branch 0 taken
0: branch 1 not taken
800 50160: ref<Expr> getKid(unsigned i) const { return (i==0) ? src : 0; }
801 :
802 140: static bool needsResultType() { return true; }
803 :
804 20488: int compareContents(const Expr &b) const {
805 20488: const CastExpr &eb = static_cast<const CastExpr&>(b);
0: branch 0 not taken
0: branch 1 not taken
0: branch 2 not taken
0: branch 3 not taken
806 20488: if (width != eb.width) return width < eb.width ? -1 : 1;
807 20488: return 0;
808 : }
809 :
810 : virtual unsigned computeHash();
811 :
812 : public:
813 : // sorry, too lazy to manual friend with all children
814 : CastExpr() {}
815 : private:
816 : friend class serialize::access;
817 : template<typename Archive>
818 87: void save(Archive &ar) const {
819 174: ar & src;
820 87: ar & (unsigned) width;
821 87: }
822 : template<typename Archive>
823 : void load(Archive &ar, unsigned version) {
824 : unsigned w;
825 : ar & src;
826 : ar & w;
827 : width = (Expr::Width) w;
828 : }
829 : };
830 :
831 : #define CAST_EXPR_CLASS(_class_kind) \
832 : class _class_kind ## Expr : public CastExpr { \
833 : public: \
834 : static const Kind kind = _class_kind; \
835 : static const unsigned numKids = 1; \
836 : public: \
837 : _class_kind ## Expr() {} \
838 : public: \
839 : _class_kind ## Expr(ref<Expr> e, Width w) : CastExpr(e,w) {} \
840 : static ref<Expr> alloc(const ref<Expr> &e, Width w) { \
841 : ref<Expr> r(new _class_kind ## Expr(e, w)); \
842 : r.computeHash(); \
843 : return r; \
844 : } \
845 : static ref<Expr> create(const ref<Expr> &e, Width w); \
846 : Kind getKind() const { return _class_kind; } \
847 : virtual ref<Expr> rebuild(ref<Expr> kids[]) const { \
848 : return create(kids[0], width); \
849 : } \
850 : }; \
851 :
8: branch 1 taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
852 40844: CAST_EXPR_CLASS(SExt)
0: branch 1 not taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
853 162872: CAST_EXPR_CLASS(ZExt)
854 :
855 : // Arithmetic/Bit Exprs
856 :
857 : #define ARITHMETIC_EXPR_CLASS(_class_kind) \
858 : class _class_kind ## Expr : public BinaryExpr { \
859 : public: \
860 : static const Kind kind = _class_kind; \
861 : static const unsigned numKids = 2; \
862 : public: \
863 : _class_kind ## Expr() {} \
864 : public: \
865 : _class_kind ## Expr(const ref<Expr> &l, const ref<Expr> &r) : BinaryExpr(l,r) {} \
866 : static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) { \
867 : ref<Expr> res(new _class_kind ## Expr (l, r)); \
868 : res.computeHash(); \
869 : return res; \
870 : } \
871 : static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r); \
872 : Width getWidth() const { return left.getWidth(); } \
873 : Kind getKind() const { return _class_kind; } \
874 : virtual ref<Expr> rebuild(ref<Expr> kids[]) const { \
875 : return create(kids[0], kids[1]); \
876 : } \
877 : }; \
878 :
37: branch 2 taken
0: branch 3 not taken
0: branch 6 not taken
0: branch 7 not taken
879 213181: ARITHMETIC_EXPR_CLASS(Add)
0: branch 2 not taken
0: branch 3 not taken
0: branch 6 not taken
0: branch 7 not taken
880 7372: ARITHMETIC_EXPR_CLASS(Sub)
17: branch 2 taken
0: branch 3 not taken
0: branch 6 not taken
0: branch 7 not taken
881 162148: ARITHMETIC_EXPR_CLASS(Mul)
0: branch 2 not taken
0: branch 3 not taken
0: branch 6 not taken
0: branch 7 not taken
882 420: ARITHMETIC_EXPR_CLASS(UDiv)
0: branch 2 not taken
0: branch 3 not taken
0: branch 6 not taken
0: branch 7 not taken
883 633: ARITHMETIC_EXPR_CLASS(SDiv)
0: branch 2 not taken
0: branch 3 not taken
0: branch 6 not taken
0: branch 7 not taken
884 341: ARITHMETIC_EXPR_CLASS(URem)
0: branch 2 not taken
0: branch 3 not taken
0: branch 6 not taken
0: branch 7 not taken
885 327: ARITHMETIC_EXPR_CLASS(SRem)
27: branch 2 taken
0: branch 3 not taken
0: branch 6 not taken
0: branch 7 not taken
886 279377: ARITHMETIC_EXPR_CLASS(And)
3: branch 2 taken
0: branch 3 not taken
0: branch 6 not taken
0: branch 7 not taken
887 1798690: ARITHMETIC_EXPR_CLASS(Or)
0: branch 2 not taken
0: branch 3 not taken
0: branch 6 not taken
0: branch 7 not taken
888 2355: ARITHMETIC_EXPR_CLASS(Xor)
889 2758: ARITHMETIC_EXPR_CLASS(Shl)
0: branch 2 not taken
0: branch 3 not taken
0: branch 6 not taken
0: branch 7 not taken
890 3101: ARITHMETIC_EXPR_CLASS(LShr)
0: branch 2 not taken
0: branch 3 not taken
0: branch 6 not taken
0: branch 7 not taken
891 1807: ARITHMETIC_EXPR_CLASS(AShr)
892 :
893 : // Comparison Exprs
894 :
895 : #define COMPARISON_EXPR_CLASS(_class_kind) \
896 : class _class_kind ## Expr : public CmpExpr { \
897 : public: \
898 : static const Kind kind = _class_kind; \
899 : static const unsigned numKids = 2; \
900 : public: \
901 : _class_kind ## Expr() {} \
902 : public: \
903 : _class_kind ## Expr(const ref<Expr> &l, const ref<Expr> &r) : CmpExpr(l,r) {} \
904 : static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) { \
905 : ref<Expr> res(new _class_kind ## Expr (l, r)); \
906 : res.computeHash(); \
907 : return res; \
908 : } \
909 : static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r); \
910 : Kind getKind() const { return _class_kind; } \
911 : virtual ref<Expr> rebuild(ref<Expr> kids[]) const { \
912 : return create(kids[0], kids[1]); \
913 : } \
914 : }; \
915 :
101: branch 1 taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
916 17021242: COMPARISON_EXPR_CLASS(Eq)
0: branch 1 not taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
917 0: COMPARISON_EXPR_CLASS(Ne)
48: branch 1 taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
918 312583: COMPARISON_EXPR_CLASS(Ult)
0: branch 1 not taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
919 272834: COMPARISON_EXPR_CLASS(Ule)
0: branch 1 not taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
920 0: COMPARISON_EXPR_CLASS(Ugt)
0: branch 1 not taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
921 0: COMPARISON_EXPR_CLASS(Uge)
5: branch 1 taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
922 138165: COMPARISON_EXPR_CLASS(Slt)
0: branch 1 not taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
923 27432: COMPARISON_EXPR_CLASS(Sle)
0: branch 1 not taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
924 0: COMPARISON_EXPR_CLASS(Sgt)
0: branch 1 not taken
0: branch 2 not taken
0: branch 5 not taken
0: branch 6 not taken
925 0: COMPARISON_EXPR_CLASS(Sge)
926 :
927 : } // End klee namespace
928 :
929 : #endif
Generated: 2009-05-17 22:47 by zcov