 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
73.7% |
28 / 38 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
89.5% |
34 / 38 |
| |
|
Line Coverage: |
94.9% |
56 / 59 |
| |
 |
|
 |
1 : /* -*- mode: c++; c-basic-offset: 2; -*- */
2 :
3 : #include "klee/Constraints.h"
4 :
5 : #include "klee/util/ExprPPrinter.h"
6 : #include "klee/util/ExprVisitor.h"
7 :
8 : #include "klee/Internal/FIXME/sugar.h"
9 :
10 : #include <iostream>
11 : #include <map>
12 :
13 : using namespace klee;
14 :
0: branch 3 not taken
0: branch 4 not taken
0: branch 9 not taken
2032: branch 10 taken
15 2032: class ExprReplaceVisitor : public ExprVisitor {
16 : private:
17 : ref<Expr> src, dst;
18 :
19 : public:
20 4064: ExprReplaceVisitor(ref<Expr> _src, ref<Expr> _dst) : src(_src), dst(_dst) {}
21 :
22 347418: Action visitExpr(const Expr &e) {
277: branch 1 taken
347141: branch 2 taken
23 694836: if (e == *src.get()) {
24 277: return Action::changeTo(dst);
25 : } else {
26 347141: return Action::doChildren();
27 : }
28 : }
29 :
30 340594: Action visitExprPost(const Expr &e) {
0: branch 1 not taken
340594: branch 2 taken
31 681188: if (e == *src.get()) {
32 0: return Action::changeTo(dst);
33 : } else {
34 340594: return Action::doChildren();
35 : }
36 : }
37 : };
38 :
0: branch 1 not taken
0: branch 2 not taken
0: branch 5 not taken
5673: branch 6 taken
39 5673: class ExprReplaceVisitor2 : public ExprVisitor {
40 : private:
41 : const std::map< ref<Expr>, ref<Expr> > &replacements;
42 :
43 : public:
44 : ExprReplaceVisitor2(const std::map< ref<Expr>, ref<Expr> > &_replacements)
45 : : ExprVisitor(true),
46 5673: replacements(_replacements) {}
47 :
48 43000: Action visitExprPost(const Expr &e) {
49 129000: let(it, replacements.find(ref<Expr>((Expr*) &e)));
2281: branch 0 taken
40719: branch 1 taken
50 86000: if (it!=replacements.end()) {
51 4562: return Action::changeTo(it->second);
52 : } else {
53 40719: return Action::doChildren();
54 : }
55 : }
56 : };
57 :
58 2032: bool ConstraintManager::rewriteConstraints(ExprVisitor &visitor) {
59 : std::vector< ref<Expr> > old;
60 2032: bool changed = false;
61 :
62 2032: constraints.swap(old);
32443: branch 1 taken
2032: branch 2 taken
63 68950: foreach(it, old.begin(), old.end()) {
64 32443: ref<Expr> &ce = *it;
65 32443: ref<Expr> e = visitor.visit(ce);
66 :
3079: branch 0 taken
29364: branch 1 taken
67 32443: if (e!=ce) {
68 3079: addConstraintInternal(e); // enable further reductions
69 3079: changed = true;
70 : } else {
71 29364: constraints.push_back(ce);
72 : }
73 : }
74 :
75 2032: return changed;
76 : }
77 :
78 0: void ConstraintManager::simplifyForValidConstraint(ref<Expr> e) {
79 : // XXX
80 0: }
81 :
82 5675: ref<Expr> ConstraintManager::simplifyExpr(ref<Expr> e) const {
2: branch 0 taken
5673: branch 1 taken
83 5675: if (e.isConstant())
84 2: return e;
85 :
86 : std::map< ref<Expr>, ref<Expr> > equalities;
87 :
38763: branch 0 taken
5673: branch 1 taken
88 61455: foreach(it, constraints.begin(), constraints.end()) {
36126: branch 0 taken
2637: branch 1 taken
89 38763: if (const EqExpr *ee = dyn_ref_cast<EqExpr>(*it)) {
36124: branch 0 taken
2: branch 1 taken
90 72252: if (ee->left.isConstant()) {
91 : equalities.insert(std::make_pair(ee->right,
92 144496: ee->left));
93 : } else {
94 : equalities.insert(std::make_pair(*it,
95 4: ref<Expr>(1,Expr::Bool)));
96 : }
97 : } else {
98 : equalities.insert(std::make_pair(*it,
99 5274: ref<Expr>(1,Expr::Bool)));
100 : }
101 : }
102 :
103 11346: return ExprReplaceVisitor2(equalities).visit(e);
104 : }
105 :
106 7062: void ConstraintManager::addConstraintInternal(ref<Expr> e) {
107 : // rewrite any known equalities
108 :
109 : // XXX should profile the effects of this and the overhead.
110 : // traversing the constraints looking for equalities is hardly the
111 : // slowest thing we do, but it is probably nicer to have a
112 : // ConstraintSet ADT which efficiently remembers obvious patterns
113 : // (byte-constant comparison).
114 :
3091: branch 0 taken
768: branch 1 taken
2033: branch 2 taken
1170: branch 3 taken
115 7062: switch (e.getKind()) {
116 : case Expr::Constant:
0: branch 0 not taken
3091: branch 1 taken
117 3091: assert(e.getConstantValue() && "attempt to add invalid (false) constraint");
118 : break;
119 :
120 : // split to enable finer grained independence and other optimizations
121 : case Expr::And: {
122 768: BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
123 1536: addConstraintInternal(be->left);
124 1536: addConstraintInternal(be->right);
125 768: break;
126 : }
127 :
128 : case Expr::Eq: {
129 2033: BinaryExpr *be = static_ref_cast<BinaryExpr>(e);
2032: branch 0 taken
1: branch 1 taken
130 4066: if (be->left.isConstant()) {
131 6096: ExprReplaceVisitor visitor(be->right, be->left);
132 2032: rewriteConstraints(visitor);
133 : }
134 2033: constraints.push_back(e);
135 2033: break;
136 : }
137 :
138 : default:
139 1170: constraints.push_back(e);
140 : break;
141 : }
142 7062: }
143 :
144 2447: void ConstraintManager::addConstraint(ref<Expr> e) {
145 2447: e = simplifyExpr(e);
146 2447: addConstraintInternal(e);
104: branch 0 taken
0: branch 1 not taken
104: branch 2 taken
0: branch 3 not taken
147 2655: }
Generated: 2009-05-17 22:47 by zcov