 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
82.4% |
56 / 68 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
100.0% |
68 / 68 |
| |
|
Line Coverage: |
86.1% |
118 / 137 |
| |
 |
|
 |
1 : #include "klee/Expr.h"
2 : #include "klee/util/ExprVisitor.h"
3 :
4 : #include "llvm/Support/CommandLine.h"
5 :
6 : namespace {
7 : llvm::cl::opt<bool>
8 104: UseVisitorHash("use-visitor-hash",
9 : llvm::cl::desc("Use hash-consing during expr visitation."),
10 104: llvm::cl::init(true));
11 : }
12 :
13 : using namespace klee;
14 :
15 1460771: ref<Expr> ExprVisitor::visit(const ref<Expr> &e) {
1460771: branch 0 taken
0: branch 1 not taken
713030: branch 2 taken
747741: branch 3 taken
713030: branch 4 taken
747741: branch 5 taken
16 2921542: if (!UseVisitorHash || e.isConstant()) {
17 713030: return visitActual(e);
18 : } else {
19 747741: visited_ty::iterator it = visited.find(e);
20 :
193098: branch 0 taken
554643: branch 1 taken
21 1495482: if (it!=visited.end()) {
22 386196: return it->second;
23 : } else {
24 554643: ref<Expr> res = visitActual(e);
25 1663929: visited.insert(std::make_pair(e, res));
26 1109286: return res;
27 : }
28 : }
29 : }
30 :
31 1267673: ref<Expr> ExprVisitor::visitActual(const ref<Expr> &e) {
713030: branch 0 taken
554643: branch 1 taken
32 1267673: if (e.isConstant()) {
33 713030: return e;
34 : } else {
35 554643: Expr &ep = *e.get();
36 :
37 554643: Action res = visitExpr(ep);
0: branch 0 not taken
277: branch 1 taken
554366: branch 2 taken
38 554643: switch(res.kind) {
39 : case Action::DoChildren:
40 : // continue with normal action
41 : break;
42 : case Action::SkipChildren:
43 0: return e;
44 : case Action::ChangeTo:
45 277: return res.argument;
46 : }
47 :
2039: branch 1 taken
74153: branch 2 taken
15: branch 3 taken
37508: branch 4 taken
1604: branch 5 taken
3852: branch 6 taken
916: branch 7 taken
8080: branch 8 taken
556: branch 9 taken
2721: branch 10 taken
17: branch 11 taken
40: branch 12 taken
16: branch 13 taken
16: branch 14 taken
9519: branch 15 taken
131096: branch 16 taken
116: branch 17 taken
146: branch 18 taken
169: branch 19 taken
80: branch 20 taken
271172: branch 21 taken
0: branch 22 not taken
5751: branch 23 taken
3719: branch 24 taken
0: branch 25 not taken
0: branch 26 not taken
777: branch 27 taken
288: branch 28 taken
0: branch 29 not taken
0: branch 30 not taken
0: branch 31 not taken
48 554366: switch(ep.getKind()) {
49 2039: case Expr::NotOptimized: res = visitNotOptimized(static_cast<NotOptimizedExpr&>(ep)); break;
50 74153: case Expr::Read: res = visitRead(static_cast<ReadExpr&>(ep)); break;
51 15: case Expr::Select: res = visitSelect(static_cast<SelectExpr&>(ep)); break;
52 37508: case Expr::Concat: res = visitConcat(static_cast<ConcatExpr&>(ep)); break;
53 1604: case Expr::Extract: res = visitExtract(static_cast<ExtractExpr&>(ep)); break;
54 3852: case Expr::ZExt: res = visitZExt(static_cast<ZExtExpr&>(ep)); break;
55 916: case Expr::SExt: res = visitSExt(static_cast<SExtExpr&>(ep)); break;
56 8080: case Expr::Add: res = visitAdd(static_cast<AddExpr&>(ep)); break;
57 556: case Expr::Sub: res = visitSub(static_cast<SubExpr&>(ep)); break;
58 2721: case Expr::Mul: res = visitMul(static_cast<MulExpr&>(ep)); break;
59 17: case Expr::UDiv: res = visitUDiv(static_cast<UDivExpr&>(ep)); break;
60 40: case Expr::SDiv: res = visitSDiv(static_cast<SDivExpr&>(ep)); break;
61 16: case Expr::URem: res = visitURem(static_cast<URemExpr&>(ep)); break;
62 16: case Expr::SRem: res = visitSRem(static_cast<SRemExpr&>(ep)); break;
63 9519: case Expr::And: res = visitAnd(static_cast<AndExpr&>(ep)); break;
64 131096: case Expr::Or: res = visitOr(static_cast<OrExpr&>(ep)); break;
65 116: case Expr::Xor: res = visitXor(static_cast<XorExpr&>(ep)); break;
66 146: case Expr::Shl: res = visitShl(static_cast<ShlExpr&>(ep)); break;
67 169: case Expr::LShr: res = visitLShr(static_cast<LShrExpr&>(ep)); break;
68 80: case Expr::AShr: res = visitAShr(static_cast<AShrExpr&>(ep)); break;
69 271172: case Expr::Eq: res = visitEq(static_cast<EqExpr&>(ep)); break;
70 0: case Expr::Ne: res = visitNe(static_cast<NeExpr&>(ep)); break;
71 5751: case Expr::Ult: res = visitUlt(static_cast<UltExpr&>(ep)); break;
72 3719: case Expr::Ule: res = visitUle(static_cast<UleExpr&>(ep)); break;
73 0: case Expr::Ugt: res = visitUgt(static_cast<UgtExpr&>(ep)); break;
74 0: case Expr::Uge: res = visitUge(static_cast<UgeExpr&>(ep)); break;
75 777: case Expr::Slt: res = visitSlt(static_cast<SltExpr&>(ep)); break;
76 288: case Expr::Sle: res = visitSle(static_cast<SleExpr&>(ep)); break;
77 0: case Expr::Sgt: res = visitSgt(static_cast<SgtExpr&>(ep)); break;
78 0: case Expr::Sge: res = visitSge(static_cast<SgeExpr&>(ep)); break;
79 : case Expr::Constant:
80 : default:
81 0: assert(0 && "invalid expression kind");
82 : }
83 :
533612: branch 0 taken
0: branch 1 not taken
20754: branch 2 taken
0: branch 3 not taken
84 554366: switch(res.kind) {
85 : case Action::DoChildren: {
86 533612: bool rebuild = false;
4268896: branch 0 taken
533612: branch 1 taken
87 4802508: ref<Expr> e(&ep), kids[8];
88 533612: unsigned count = ep.getNumKids();
1005421: branch 1 taken
533612: branch 2 taken
89 1539033: for (unsigned i=0; i<count; i++) {
90 1005421: ref<Expr> kid = ep.getKid(i);
91 1005421: kids[i] = visit(kid);
101940: branch 0 taken
903481: branch 1 taken
92 2010842: if (kids[i] != kid)
93 101940: rebuild = true;
94 : }
86037: branch 0 taken
447575: branch 1 taken
95 533612: if (rebuild) {
96 86037: e = ep.rebuild(kids);
4925: branch 0 taken
81112: branch 1 taken
97 86037: if (recursive)
98 4925: e = visit(e);
99 : }
448113: branch 0 taken
85499: branch 1 taken
100 533612: if (!e.isConstant()) {
101 448113: res = visitExprPost(*e.get());
2281: branch 0 taken
445832: branch 1 taken
102 448113: if (res.kind==Action::ChangeTo)
103 2281: e = res.argument;
104 : }
4268896: branch 0 taken
533612: branch 1 taken
105 1067224: return e;
106 : }
107 : case Action::SkipChildren:
108 0: return e;
109 : case Action::ChangeTo:
110 20754: return res.argument;
111 : default:
112 0: assert(0 && "invalid kind");
113 : }
114 : }
115 : }
116 :
117 207225: ExprVisitor::Action ExprVisitor::visitExpr(const Expr&) {
118 207225: return Action::doChildren();
119 : }
120 :
121 64519: ExprVisitor::Action ExprVisitor::visitExprPost(const Expr&) {
122 64519: return Action::skipChildren();
123 : }
124 :
125 2039: ExprVisitor::Action ExprVisitor::visitNotOptimized(const NotOptimizedExpr&) {
126 2039: return Action::doChildren();
127 : }
128 :
129 38459: ExprVisitor::Action ExprVisitor::visitRead(const ReadExpr&) {
130 38459: return Action::doChildren();
131 : }
132 :
133 15: ExprVisitor::Action ExprVisitor::visitSelect(const SelectExpr&) {
134 15: return Action::doChildren();
135 : }
136 :
137 37508: ExprVisitor::Action ExprVisitor::visitConcat(const ConcatExpr&) {
138 37508: return Action::doChildren();
139 : }
140 :
141 1604: ExprVisitor::Action ExprVisitor::visitExtract(const ExtractExpr&) {
142 1604: return Action::doChildren();
143 : }
144 :
145 3852: ExprVisitor::Action ExprVisitor::visitZExt(const ZExtExpr&) {
146 3852: return Action::doChildren();
147 : }
148 :
149 916: ExprVisitor::Action ExprVisitor::visitSExt(const SExtExpr&) {
150 916: return Action::doChildren();
151 : }
152 :
153 8080: ExprVisitor::Action ExprVisitor::visitAdd(const AddExpr&) {
154 8080: return Action::doChildren();
155 : }
156 :
157 556: ExprVisitor::Action ExprVisitor::visitSub(const SubExpr&) {
158 556: return Action::doChildren();
159 : }
160 :
161 2721: ExprVisitor::Action ExprVisitor::visitMul(const MulExpr&) {
162 2721: return Action::doChildren();
163 : }
164 :
165 17: ExprVisitor::Action ExprVisitor::visitUDiv(const UDivExpr&) {
166 17: return Action::doChildren();
167 : }
168 :
169 32: ExprVisitor::Action ExprVisitor::visitSDiv(const SDivExpr&) {
170 32: return Action::doChildren();
171 : }
172 :
173 16: ExprVisitor::Action ExprVisitor::visitURem(const URemExpr&) {
174 16: return Action::doChildren();
175 : }
176 :
177 16: ExprVisitor::Action ExprVisitor::visitSRem(const SRemExpr&) {
178 16: return Action::doChildren();
179 : }
180 :
181 9519: ExprVisitor::Action ExprVisitor::visitAnd(const AndExpr&) {
182 9519: return Action::doChildren();
183 : }
184 :
185 131096: ExprVisitor::Action ExprVisitor::visitOr(const OrExpr&) {
186 131096: return Action::doChildren();
187 : }
188 :
189 116: ExprVisitor::Action ExprVisitor::visitXor(const XorExpr&) {
190 116: return Action::doChildren();
191 : }
192 :
193 146: ExprVisitor::Action ExprVisitor::visitShl(const ShlExpr&) {
194 146: return Action::doChildren();
195 : }
196 :
197 169: ExprVisitor::Action ExprVisitor::visitLShr(const LShrExpr&) {
198 169: return Action::doChildren();
199 : }
200 :
201 80: ExprVisitor::Action ExprVisitor::visitAShr(const AShrExpr&) {
202 80: return Action::doChildren();
203 : }
204 :
205 271172: ExprVisitor::Action ExprVisitor::visitEq(const EqExpr&) {
206 271172: return Action::doChildren();
207 : }
208 :
209 0: ExprVisitor::Action ExprVisitor::visitNe(const NeExpr&) {
210 0: return Action::doChildren();
211 : }
212 :
213 5751: ExprVisitor::Action ExprVisitor::visitUlt(const UltExpr&) {
214 5751: return Action::doChildren();
215 : }
216 :
217 3719: ExprVisitor::Action ExprVisitor::visitUle(const UleExpr&) {
218 3719: return Action::doChildren();
219 : }
220 :
221 0: ExprVisitor::Action ExprVisitor::visitUgt(const UgtExpr&) {
222 0: return Action::doChildren();
223 : }
224 :
225 0: ExprVisitor::Action ExprVisitor::visitUge(const UgeExpr&) {
226 0: return Action::doChildren();
227 : }
228 :
229 777: ExprVisitor::Action ExprVisitor::visitSlt(const SltExpr&) {
230 777: return Action::doChildren();
231 : }
232 :
233 288: ExprVisitor::Action ExprVisitor::visitSle(const SleExpr&) {
234 288: return Action::doChildren();
235 : }
236 :
237 0: ExprVisitor::Action ExprVisitor::visitSgt(const SgtExpr&) {
238 0: return Action::doChildren();
239 : }
240 :
241 0: ExprVisitor::Action ExprVisitor::visitSge(const SgeExpr&) {
242 0: return Action::doChildren();
104: branch 0 taken
0: branch 1 not taken
104: branch 2 taken
0: branch 3 not taken
243 208: }
244 :
Generated: 2009-05-17 22:47 by zcov