 |
|
 |
|
| Files: |
1 |
|
Branches Taken: |
84.8% |
139 / 164 |
| Generated: |
2009-05-17 22:47 |
|
Branches Executed: |
100.0% |
164 / 164 |
| |
|
Line Coverage: |
94.4% |
235 / 249 |
| |
 |
|
 |
1 : #include "klee/util/ExprPPrinter.h"
2 :
3 : #include "klee/Constraints.h"
4 : // FIXME: This should not be here.
5 : #include "klee/Memory.h"
6 :
7 : #include "llvm/Support/CommandLine.h"
8 :
9 : #include <map>
10 : #include <vector>
11 : #include <iostream>
12 : #include <sstream>
13 : #include <iomanip>
14 :
15 : #include "klee/Internal/FIXME/sugar.h"
16 :
17 : using namespace klee;
18 :
19 : namespace {
20 : llvm::cl::opt<bool>
21 216: PCWidthAsArg("pc-width-as-arg", llvm::cl::init(true));
22 :
23 : llvm::cl::opt<bool>
24 216: PCAllWidths("pc-all-widths", llvm::cl::init(false));
25 :
26 : llvm::cl::opt<bool>
27 216: PCPrefixWidth("pc-prefix-width", llvm::cl::init(true));
28 :
29 : llvm::cl::opt<bool>
30 216: PCMultibyteReads("pc-multibyte-reads", llvm::cl::init(true));
31 :
32 : llvm::cl::opt<bool>
33 216: PCAllConstWidths("pc-all-const-widths", llvm::cl::init(false));
34 : }
35 :
36 : /// PrintContext - Helper class for storing extra information for
37 : /// the pretty printer.
38 270: class PrintContext {
39 : private:
40 : std::ostream &os;
41 : std::stringstream ss;
42 : std::string newline;
43 :
44 : public:
45 : /// Number of characters on the current line.
46 : unsigned pos;
47 :
48 : public:
49 1080: PrintContext(std::ostream &_os) : os(_os), newline("\n"), pos(0) {}
50 :
51 : void setNewline(const std::string &_newline) {
52 : newline = _newline;
53 : }
54 :
55 1758: void breakLine(unsigned indent=0) {
56 1758: os << newline;
1488: branch 0 taken
270: branch 1 taken
57 1758: if (indent)
58 4464: os << std::setw(indent) << ' ';
59 1758: pos = indent;
60 1758: }
61 :
62 : /// write - Output a string to the stream and update the
63 : /// position. The stream should not have any newlines.
64 : void write(const std::string &s) {
65 28438: os << s;
66 56876: pos += s.length();
67 : }
68 :
69 : template <typename T>
70 23085: PrintContext &operator<<(T elt) {
71 56876: ss.str("");
72 28438: ss << elt;
73 56876: write(ss.str());
74 28438: return *this;
75 : }
76 : };
77 :
1: branch 1 taken
0: branch 2 not taken
0: branch 5 not taken
270: branch 6 taken
78 2168: class PPrinter : public ExprPPrinter {
79 : std::map<ref<Expr>, unsigned> bindings;
80 : std::map<const UpdateNode*, unsigned> updateBindings;
81 : std::set< ref<Expr> > couldPrint, shouldPrint;
82 : std::set<const UpdateNode*> couldPrintUpdates, shouldPrintUpdates;
83 : std::ostream &os;
84 : unsigned counter;
85 : unsigned updateCounter;
86 : bool hasScan;
87 : std::string newline;
88 :
89 : /// shouldPrintWidth - Predicate for whether this expression should
90 : /// be printed with its width.
91 : bool shouldPrintWidth(ref<Expr> e) {
0: branch 0 not taken
3090: branch 1 taken
92 3090: if (PCAllWidths)
93 0: return true;
94 3090: return e.getWidth() != Expr::Bool;
95 : }
96 :
97 5848: bool isVerySimple(const ref<Expr> &e) {
3520: branch 1 taken
2328: branch 2 taken
359: branch 4 taken
3161: branch 5 taken
98 12888: return e.isConstant() || bindings.find(e)!=bindings.end();
99 : }
100 :
101 : bool isVerySimpleUpdate(const UpdateNode *un) {
58: branch 0 taken
651: branch 1 taken
38: branch 2 taken
20: branch 3 taken
102 825: return !un || updateBindings.find(un)!=updateBindings.end();
103 : }
104 :
105 :
106 : // document me!
107 : bool isSimple(const ref<Expr> &e) {
797: branch 1 taken
1949: branch 2 taken
108 2746: if (isVerySimple(e)) {
109 797: return true;
735: branch 1 taken
1214: branch 2 taken
110 1949: } else if (const ReadExpr *re = dyn_ref_cast<ReadExpr>(e)) {
709: branch 1 taken
26: branch 2 taken
689: branch 3 taken
20: branch 4 taken
111 1444: return isVerySimple(re->index) && isVerySimpleUpdate(re->updates.head);
112 : } else {
113 1214: Expr *ep = e.get();
1410: branch 1 taken
54: branch 2 taken
114 1464: for (unsigned i=0; i<ep->getNumKids(); i++)
1160: branch 3 taken
250: branch 4 taken
115 1410: if (!isVerySimple(ep->getKid(i)))
116 1160: return false;
117 54: return true;
118 : }
119 : }
120 :
121 : bool hasSimpleKids(const Expr *ep) {
2746: branch 1 taken
520: branch 2 taken
122 3266: for (unsigned i=0; i<ep->getNumKids(); i++)
1206: branch 2 taken
1540: branch 3 taken
123 5492: if (!isSimple(ep->getKid(i)))
124 1206: return false;
125 520: return true;
126 : }
127 :
128 1891: void scanUpdate(const UpdateNode *un) {
811: branch 0 taken
1080: branch 1 taken
129 1891: if (un) {
712: branch 1 taken
99: branch 2 taken
130 811: if (couldPrintUpdates.insert(un).second) {
131 712: scanUpdate(un->next);
132 712: scan1(un->index);
133 712: scan1(un->value);
134 : } else {
135 99: shouldPrintUpdates.insert(un);
136 : }
137 : }
138 1891: }
139 :
140 7709: void scan1(const ref<Expr> &e) {
4284: branch 1 taken
3425: branch 2 taken
141 7709: if (!e.isConstant()) {
3547: branch 0 taken
737: branch 1 taken
142 8568: if (couldPrint.insert(e).second) {
143 3547: Expr *ep = e.get();
5833: branch 1 taken
3547: branch 2 taken
144 9380: for (unsigned i=0; i<ep->getNumKids(); i++)
145 5833: scan1(ep->getKid(i));
1179: branch 1 taken
2368: branch 2 taken
146 3547: if (const ReadExpr *re = dyn_ref_cast<ReadExpr>(e))
147 1179: scanUpdate(re->updates.head);
148 : } else {
149 737: shouldPrint.insert(e);
150 : }
151 : }
152 7709: }
153 :
154 957: void printUpdateList(const UpdateList &updates, PrintContext &PC) {
155 957: const UpdateNode *head = updates.head;
156 :
157 : // Special case empty list.
852: branch 0 taken
105: branch 1 taken
158 957: if (!head) {
852: branch 0 taken
0: branch 1 not taken
159 852: if (updates.isRooted) {
160 852: PC << "arr" << updates.root->id;
161 : } else {
162 0: PC << "[]";
163 : }
164 : return;
165 : }
166 :
167 : // FIXME: Explain this breaking policy.
168 105: bool openedList = false, nextShouldBreak = false;
169 105: unsigned outerIndent = PC.pos;
170 105: unsigned middleIndent = 0;
790: branch 0 taken
27: branch 1 taken
171 817: for (const UpdateNode *un = head; un; un = un->next) {
172 : // We are done if we hit the cache.
173 790: let(it, updateBindings.find(un));
78: branch 0 taken
712: branch 1 taken
174 1580: if (it!=updateBindings.end()) {
0: branch 0 not taken
78: branch 1 taken
175 78: if (openedList)
176 0: PC << "] @ ";
177 : PC << "U" << it->second;
178 78: return;
712: branch 0 taken
0: branch 1 not taken
31: branch 2 taken
681: branch 3 taken
31: branch 4 taken
681: branch 5 taken
179 1424: } else if (!hasScan || shouldPrintUpdates.count(un)) {
6: branch 0 taken
25: branch 1 taken
180 31: if (openedList)
181 6: PC << "] @";
6: branch 0 taken
25: branch 1 taken
182 31: if (un != head)
183 6: PC.breakLine(outerIndent);
184 31: PC << "U" << updateCounter << ":";
185 62: updateBindings.insert(std::make_pair(un, updateCounter++));
186 31: openedList = nextShouldBreak = false;
187 : }
188 :
33: branch 0 taken
679: branch 1 taken
189 712: if (!openedList) {
190 33: openedList = 1;
191 33: PC << '[';
192 33: middleIndent = PC.pos;
193 : } else {
194 679: PC << ',';
195 679: printSeparator(PC, !nextShouldBreak, middleIndent);
196 : }
197 : //PC << "(=";
198 : //unsigned innerIndent = PC.pos;
199 712: print(un->index, PC);
200 : //printSeparator(PC, isSimple(un->index), innerIndent);
201 712: PC << "=";
202 712: print(un->value, PC);
203 : //PC << ')';
204 :
636: branch 1 taken
76: branch 2 taken
0: branch 4 not taken
636: branch 5 taken
205 712: nextShouldBreak = !(un->index.isConstant() && un->value.isConstant());
206 : }
207 :
27: branch 0 taken
0: branch 1 not taken
208 27: if (openedList)
209 27: PC << ']';
210 :
12: branch 0 taken
15: branch 1 taken
211 27: if (updates.isRooted)
212 12: PC << " @ arr" << updates.root->id;
213 : }
214 :
215 3090: void printWidth(PrintContext &PC, ref<Expr> e) {
1443: branch 1 taken
1647: branch 2 taken
216 3090: if (!shouldPrintWidth(e))
217 1443: return;
218 :
1647: branch 0 taken
0: branch 1 not taken
219 1647: if (PCWidthAsArg) {
220 1647: PC << ' ';
1647: branch 0 taken
0: branch 1 not taken
221 1647: if (PCPrefixWidth)
222 1647: PC << 'w';
223 : }
224 :
225 1647: PC << e.getWidth();
226 : }
227 :
228 : /// hasOrderedReads - True iff all children are reads with
229 : /// consecutive offsets according to the given \arg stride.
230 444: bool hasOrderedReads(const Expr *ep, int stride) {
231 444: const ReadExpr *base = dyn_ref_cast<ReadExpr>(ep->getKid(0));
0: branch 0 not taken
444: branch 1 taken
232 444: if (!base)
233 0: return false;
234 :
235 : // Get stride expr in proper index width.
236 444: Expr::Width idxWidth = base->index.getWidth();
237 444: ref<Expr> strideExpr(stride, idxWidth), offset(0, idxWidth);
444: branch 1 taken
222: branch 2 taken
238 666: for (unsigned i=1; i<ep->getNumKids(); ++i) {
239 444: const ReadExpr *re = dyn_ref_cast<ReadExpr>(ep->getKid(i));
0: branch 0 not taken
444: branch 1 taken
240 444: if (!re)
241 0: return false;
242 :
243 : // Check if the index follows the stride.
244 : // FIXME: How aggressive should this be simplified. The
245 : // canonicalizing builder is probably the right choice, but this
246 : // is yet another area where we would really prefer it to be
247 : // global or else use static methods.
248 888: offset = AddExpr::create(offset, strideExpr);
222: branch 2 taken
222: branch 3 taken
249 888: if (SubExpr::create(re->index, base->index) != offset)
250 222: return false;
251 : }
252 :
253 222: return true;
254 : }
255 :
256 : /// hasAllByteReads - True iff all children are byte level reads.
257 : bool hasAllByteReads(const Expr *ep) {
1395: branch 1 taken
222: branch 2 taken
258 1617: for (unsigned i=0; i<ep->getNumKids(); ++i) {
259 1395: const ReadExpr *re = dyn_ref_cast<ReadExpr>(ep->getKid(i));
918: branch 0 taken
477: branch 1 taken
0: branch 3 not taken
918: branch 4 taken
477: branch 5 taken
918: branch 6 taken
260 1395: if (!re || re->getWidth() != Expr::Int8)
261 477: return false;
262 : }
263 222: return true;
264 : }
265 :
266 957: void printRead(const ReadExpr *re, PrintContext &PC, unsigned indent) {
267 957: print(re->index, PC);
268 957: printSeparator(PC, isVerySimple(re->index), indent);
269 957: printUpdateList(re->updates, PC);
270 957: }
271 :
272 : void printExtract(const ExtractExpr *ee, PrintContext &PC, unsigned indent) {
273 64: PC << ee->offset << ' ';
274 64: print(ee->expr, PC);
275 : }
276 :
277 1726: void printExpr(const Expr *ep, PrintContext &PC, unsigned indent, bool printConstWidth=false) {
278 1726: bool simple = hasSimpleKids(ep);
279 :
280 1726: print(ep->getKid(0), PC);
1708: branch 1 taken
1726: branch 2 taken
281 3434: for (unsigned i=1; i<ep->getNumKids(); i++) {
282 1708: printSeparator(PC, simple, indent);
283 1708: print(ep->getKid(i), PC, printConstWidth);
284 : }
285 1726: }
286 :
287 : public:
288 2439: PPrinter(std::ostream &_os) : os(_os), newline("\n") {
289 271: reset();
290 271: }
291 :
292 0: void setNewline(const std::string &_newline) {
293 0: newline = _newline;
294 0: }
295 :
296 271: void reset() {
297 271: counter = 0;
298 271: updateCounter = 0;
299 271: hasScan = false;
300 271: bindings.clear();
301 271: updateBindings.clear();
302 271: couldPrint.clear();
303 271: shouldPrint.clear();
304 271: couldPrintUpdates.clear();
305 271: shouldPrintUpdates.clear();
306 271: }
307 :
308 452: void scan(const ref<Expr> &e) {
309 452: hasScan = true;
310 452: scan1(e);
311 452: }
312 :
313 0: void print(const ref<Expr> &e, unsigned level=0) {
314 0: PrintContext PC(os);
315 0: PC.pos = level;
316 0: print(e, PC);
317 0: }
318 :
319 2860: void printConst(const ref<Expr> &e, PrintContext &PC, bool printWidth) {
0: branch 1 not taken
2860: branch 2 taken
320 2860: assert(e.isConstant());
321 :
32: branch 1 taken
2828: branch 2 taken
322 2860: if (e.getWidth() == Expr::Bool)
0: branch 0 not taken
32: branch 1 taken
323 32: PC << (e.getConstantValue() ? "true" : "false");
324 : else {
0: branch 0 not taken
2828: branch 1 taken
325 2828: if (PCAllConstWidths)
326 0: printWidth = true;
327 :
13: branch 0 taken
2815: branch 1 taken
328 2828: if (printWidth)
329 13: PC << "(w" << e.getWidth() << " ";
330 :
331 : PC << e.getConstantValue();
332 :
13: branch 0 taken
2815: branch 1 taken
333 2828: if (printWidth)
334 13: PC << ")";
335 : }
336 2860: }
337 :
338 6674: void print(const ref<Expr> &e, PrintContext &PC, bool printConstWidth=false) {
2860: branch 1 taken
3814: branch 2 taken
339 6674: if (e.isConstant())
340 2860: printConst(e, PC, printConstWidth);
341 : else {
342 3814: let(it, bindings.find(e));
724: branch 0 taken
3090: branch 1 taken
343 7628: if (it!=bindings.end()) {
344 724: PC << 'N' << it->second;
345 : } else {
3090: branch 0 taken
0: branch 1 not taken
299: branch 2 taken
2791: branch 3 taken
299: branch 4 taken
2791: branch 5 taken
346 6180: if (!hasScan || shouldPrint.count(e)) {
347 299: PC << 'N' << counter << ':';
348 1495: bindings.insert(std::make_pair(e, counter++));
349 : }
350 :
351 : // Detect Not.
352 : // FIXME: This should be in common code.
714: branch 0 taken
2376: branch 1 taken
353 3090: if (const EqExpr *ee = dyn_ref_cast<EqExpr>(e)) {
343: branch 1 taken
371: branch 2 taken
354 1428: if (ee->left == ref<Expr>(false, Expr::Bool)) {
355 343: PC << "(Not";
356 343: printWidth(PC, e);
357 343: PC << ' ';
358 : // FIXME: This is a boom if right is a constant.
359 343: print(ee->right, PC);
360 343: PC << ')';
361 343: return;
362 : }
363 : }
364 :
365 : // Detect multibyte reads.
366 : // FIXME: Hrm. One problem with doing this is that we are
367 : // masking the sharing of the indices which aren't
368 : // visible. Need to think if this matters... probably not
369 : // because if they are offset reads then its either constant,
370 : // or they are (base + offset) and base will get printed with
371 : // a declaration.
2747: branch 0 taken
0: branch 1 not taken
699: branch 3 taken
2048: branch 4 taken
699: branch 5 taken
2048: branch 6 taken
372 2747: if (PCMultibyteReads && e.getKind() == Expr::Concat) {
373 699: const Expr *ep = e.get();
222: branch 0 taken
477: branch 1 taken
374 699: if (hasAllByteReads(ep)) {
375 222: bool isMSB = hasOrderedReads(ep, 1);
222: branch 0 taken
0: branch 1 not taken
222: branch 3 taken
0: branch 4 not taken
222: branch 5 taken
0: branch 6 not taken
376 222: if (isMSB || hasOrderedReads(ep, -1)) {
0: branch 0 not taken
222: branch 1 taken
377 222: PC << "(Read" << (isMSB ? "MSB" : "LSB");
378 222: printWidth(PC, e);
379 222: PC << ' ';
0: branch 0 not taken
222: branch 1 taken
380 222: unsigned firstIdx = isMSB ? 0 : ep->getNumKids()-1;
381 : printRead(static_ref_cast<ReadExpr>(ep->getKid(firstIdx)),
382 444: PC, PC.pos);
383 222: PC << ')';
384 222: return;
385 : }
386 : }
387 : }
388 :
389 2525: PC << '(' << e.getKind();
390 2525: printWidth(PC, e);
391 2525: PC << ' ';
392 :
393 : // Indent at first argument and dispatch to appropriate print
394 : // routine for exprs which require special handling.
395 2525: unsigned indent = PC.pos;
735: branch 1 taken
1790: branch 2 taken
396 2525: if (const ReadExpr *re = dyn_ref_cast<ReadExpr>(e)) {
397 735: printRead(re, PC, indent);
64: branch 0 taken
1726: branch 1 taken
398 1790: } else if (const ExtractExpr *ee = dyn_ref_cast<ExtractExpr>(e)) {
399 : printExtract(ee, PC, indent);
1249: branch 1 taken
477: branch 2 taken
16: branch 4 taken
1233: branch 5 taken
493: branch 6 taken
1233: branch 7 taken
400 1726: } else if (e.getKind() == Expr::Concat || e.getKind() == Expr::SExt)
401 493: printExpr(e.get(), PC, indent, true);
402 : else
403 1233: printExpr(e.get(), PC, indent);
404 2525: PC << ")";
405 : }
406 : }
407 : }
408 :
409 : /* Public utility functions */
410 :
411 3408: void printSeparator(PrintContext &PC, bool simple, unsigned indent) {
2057: branch 0 taken
1351: branch 1 taken
412 3408: if (simple) {
413 2057: PC << ' ';
414 : } else {
415 1351: PC.breakLine(indent);
416 : }
417 3408: }
418 : };
419 :
420 1: ExprPPrinter *klee::ExprPPrinter::create(std::ostream &os) {
421 1: return new PPrinter(os);
422 : }
423 :
424 : void ExprPPrinter::printOne(std::ostream &os,
425 : const char *message,
426 206: const ref<Expr> &e) {
427 206: PPrinter p(os);
428 206: p.scan(e);
429 :
430 : // FIXME: Need to figure out what to do here. Probably print as a
431 : // "forward declaration" with whatever syntax we pick for that.
432 206: PrintContext PC(os);
433 206: PC << message << ": ";
434 206: p.print(e, PC);
435 206: PC.breakLine();
436 206: }
437 :
438 : void ExprPPrinter::printConstraints(std::ostream &os,
439 29: const ConstraintManager &constraints) {
440 29: printQuery(os, constraints, ref<Expr>(false, Expr::Bool));
441 29: }
442 :
443 : void ExprPPrinter::printQuery(std::ostream &os,
444 : const ConstraintManager &constraints,
445 64: const ref<Expr> &q) {
446 64: PPrinter p(os);
447 :
182: branch 0 taken
64: branch 1 taken
448 246: for (ConstraintManager::const_iterator it = constraints.begin(),
449 : ie = constraints.end(); it != ie; ++it)
450 182: p.scan(*it);
451 64: p.scan(q);
452 :
453 64: PrintContext PC(os);
454 64: PC << "(query [";
455 :
456 : // Ident at constraint list;
457 64: unsigned indent = PC.pos;
182: branch 0 taken
64: branch 1 taken
458 246: for (ConstraintManager::const_iterator it = constraints.begin(),
459 : ie = constraints.end(); it != ie;) {
460 182: p.print(*it, PC);
461 : ++it;
131: branch 0 taken
51: branch 1 taken
462 182: if (it != ie)
463 131: PC.breakLine(indent);
464 : }
465 64: PC << ']';
466 :
467 128: p.printSeparator(PC, constraints.empty(), indent-1);
468 64: p.print(q, PC);
469 :
470 64: PC << ')';
471 64: PC.breakLine();
108: branch 0 taken
0: branch 1 not taken
108: branch 2 taken
0: branch 3 not taken
472 388: }
Generated: 2009-05-17 22:47 by zcov