klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExprPPrinter.cpp
Go to the documentation of this file.
1 //===-- ExprPPrinter.cpp - ----------------------------------------------===//
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 #include "klee/util/PrintContext.h"
11 #include "klee/util/ExprPPrinter.h"
12 
13 #include "klee/Constraints.h"
14 
15 #include "llvm/Support/CommandLine.h"
16 #include "llvm/Support/raw_ostream.h"
17 
18 #include <map>
19 #include <vector>
20 
21 using namespace klee;
22 
23 namespace {
24  llvm::cl::opt<bool>
25  PCWidthAsArg("pc-width-as-arg", llvm::cl::init(true));
26 
27  llvm::cl::opt<bool>
28  PCAllWidths("pc-all-widths", llvm::cl::init(false));
29 
30  llvm::cl::opt<bool>
31  PCPrefixWidth("pc-prefix-width", llvm::cl::init(true));
32 
33  llvm::cl::opt<bool>
34  PCMultibyteReads("pc-multibyte-reads", llvm::cl::init(true));
35 
36  llvm::cl::opt<bool>
37  PCAllConstWidths("pc-all-const-widths", llvm::cl::init(false));
38 }
39 
40 class PPrinter : public ExprPPrinter {
41 public:
42  std::set<const Array*> usedArrays;
43 private:
44  std::map<ref<Expr>, unsigned> bindings;
45  std::map<const UpdateNode*, unsigned> updateBindings;
46  std::set< ref<Expr> > couldPrint, shouldPrint;
47  std::set<const UpdateNode*> couldPrintUpdates, shouldPrintUpdates;
48  llvm::raw_ostream &os;
49  unsigned counter;
50  unsigned updateCounter;
51  bool hasScan;
53  std::string newline;
54 
58  if (PCAllWidths)
59  return true;
60  return e->getWidth() != Expr::Bool;
61  }
62 
63  bool isVerySimple(const ref<Expr> &e) {
64  return isa<ConstantExpr>(e) || bindings.find(e)!=bindings.end();
65  }
66 
67  bool isVerySimpleUpdate(const UpdateNode *un) {
68  return !un || updateBindings.find(un)!=updateBindings.end();
69  }
70 
71 
72  // document me!
73  bool isSimple(const ref<Expr> &e) {
74  if (isVerySimple(e)) {
75  return true;
76  } else if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) {
77  return isVerySimple(re->index) && isVerySimpleUpdate(re->updates.head);
78  } else {
79  Expr *ep = e.get();
80  for (unsigned i=0; i<ep->getNumKids(); i++)
81  if (!isVerySimple(ep->getKid(i)))
82  return false;
83  return true;
84  }
85  }
86 
87  bool hasSimpleKids(const Expr *ep) {
88  for (unsigned i=0; i<ep->getNumKids(); i++)
89  if (!isSimple(ep->getKid(i)))
90  return false;
91  return true;
92  }
93 
94  void scanUpdate(const UpdateNode *un) {
95  // FIXME: This needs to be non-recursive.
96  if (un) {
97  if (couldPrintUpdates.insert(un).second) {
98  scanUpdate(un->next);
99  scan1(un->index);
100  scan1(un->value);
101  } else {
102  shouldPrintUpdates.insert(un);
103  }
104  }
105  }
106 
107  void scan1(const ref<Expr> &e) {
108  if (!isa<ConstantExpr>(e)) {
109  if (couldPrint.insert(e).second) {
110  Expr *ep = e.get();
111  for (unsigned i=0; i<ep->getNumKids(); i++)
112  scan1(ep->getKid(i));
113  if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) {
114  usedArrays.insert(re->updates.root);
115  scanUpdate(re->updates.head);
116  }
117  } else {
118  shouldPrint.insert(e);
119  }
120  }
121  }
122 
123  void printUpdateList(const UpdateList &updates, PrintContext &PC) {
124  const UpdateNode *head = updates.head;
125 
126  // Special case empty list.
127  if (!head) {
128  // FIXME: We need to do something (assert, mangle, etc.) so that printing
129  // distinct arrays with the same name doesn't fail.
130  PC << updates.root->name;
131  return;
132  }
133 
134  // FIXME: Explain this breaking policy.
135  bool openedList = false, nextShouldBreak = false;
136  unsigned outerIndent = PC.pos;
137  unsigned middleIndent = 0;
138  for (const UpdateNode *un = head; un; un = un->next) {
139  // We are done if we hit the cache.
140  std::map<const UpdateNode*, unsigned>::iterator it =
141  updateBindings.find(un);
142  if (it!=updateBindings.end()) {
143  if (openedList)
144  PC << "] @ ";
145  PC << "U" << it->second;
146  return;
147  } else if (!hasScan || shouldPrintUpdates.count(un)) {
148  if (openedList)
149  PC << "] @";
150  if (un != head)
151  PC.breakLine(outerIndent);
152  PC << "U" << updateCounter << ":";
153  updateBindings.insert(std::make_pair(un, updateCounter++));
154  openedList = nextShouldBreak = false;
155  }
156 
157  if (!openedList) {
158  openedList = 1;
159  PC << '[';
160  middleIndent = PC.pos;
161  } else {
162  PC << ',';
163  printSeparator(PC, !nextShouldBreak, middleIndent);
164  }
165  //PC << "(=";
166  //unsigned innerIndent = PC.pos;
167  print(un->index, PC);
168  //printSeparator(PC, isSimple(un->index), innerIndent);
169  PC << "=";
170  print(un->value, PC);
171  //PC << ')';
172 
173  nextShouldBreak = !(isa<ConstantExpr>(un->index) &&
174  isa<ConstantExpr>(un->value));
175  }
176 
177  if (openedList)
178  PC << ']';
179 
180  PC << " @ " << updates.root->name;
181  }
182 
184  if (!shouldPrintWidth(e))
185  return;
186 
187  if (PCWidthAsArg) {
188  PC << ' ';
189  if (PCPrefixWidth)
190  PC << 'w';
191  }
192 
193  PC << e->getWidth();
194  }
195 
196 
197  bool isReadExprAtOffset(ref<Expr> e, const ReadExpr *base, ref<Expr> offset) {
198  const ReadExpr *re = dyn_cast<ReadExpr>(e.get());
199 
200  // right now, all Reads are byte reads but some
201  // transformations might change this
202  if (!re || (re->getWidth() != Expr::Int8))
203  return false;
204 
205  // Check if the index follows the stride.
206  // FIXME: How aggressive should this be simplified. The
207  // canonicalizing builder is probably the right choice, but this
208  // is yet another area where we would really prefer it to be
209  // global or else use static methods.
210  return SubExpr::create(re->index, base->index) == offset;
211  }
212 
213 
222  const ReadExpr* hasOrderedReads(ref<Expr> e, int stride) {
223  assert(e->getKind() == Expr::Concat);
224  assert(stride == 1 || stride == -1);
225 
226  const ReadExpr *base = dyn_cast<ReadExpr>(e->getKid(0));
227 
228  // right now, all Reads are byte reads but some
229  // transformations might change this
230  if (!base || base->getWidth() != Expr::Int8)
231  return NULL;
232 
233  // Get stride expr in proper index width.
234  Expr::Width idxWidth = base->index->getWidth();
235  ref<Expr> strideExpr = ConstantExpr::alloc(stride, idxWidth);
236  ref<Expr> offset = ConstantExpr::create(0, idxWidth);
237 
238  e = e->getKid(1);
239 
240  // concat chains are unbalanced to the right
241  while (e->getKind() == Expr::Concat) {
242  offset = AddExpr::create(offset, strideExpr);
243  if (!isReadExprAtOffset(e->getKid(0), base, offset))
244  return NULL;
245 
246  e = e->getKid(1);
247  }
248 
249  offset = AddExpr::create(offset, strideExpr);
250  if (!isReadExprAtOffset(e, base, offset))
251  return NULL;
252 
253  if (stride == -1)
254  return cast<ReadExpr>(e.get());
255  else return base;
256  }
257 
258 #if 0
259  bool hasAllByteReads(const Expr *ep) {
262  switch (ep->kind) {
263  Expr::Read: {
264  // right now, all Reads are byte reads but some
265  // transformations might change this
266  return ep->getWidth() == Expr::Int8;
267  }
268  Expr::Concat: {
269  for (unsigned i=0; i<ep->getNumKids(); ++i) {
270  if (!hashAllByteReads(ep->getKid(i)))
271  return false;
272  }
273  }
274  default: return false;
275  }
276  }
277 #endif
278 
279  void printRead(const ReadExpr *re, PrintContext &PC, unsigned indent) {
280  print(re->index, PC);
281  printSeparator(PC, isVerySimple(re->index), indent);
282  printUpdateList(re->updates, PC);
283  }
284 
285  void printExtract(const ExtractExpr *ee, PrintContext &PC, unsigned indent) {
286  PC << ee->offset << ' ';
287  print(ee->expr, PC);
288  }
289 
290  void printExpr(const Expr *ep, PrintContext &PC, unsigned indent, bool printConstWidth=false) {
291  bool simple = hasSimpleKids(ep);
292 
293  print(ep->getKid(0), PC);
294  for (unsigned i=1; i<ep->getNumKids(); i++) {
295  printSeparator(PC, simple, indent);
296  print(ep->getKid(i), PC, printConstWidth);
297  }
298  }
299 
300 public:
301  PPrinter(llvm::raw_ostream &_os) : os(_os), newline("\n") {
302  reset();
303  }
304 
305  void setNewline(const std::string &_newline) {
306  newline = _newline;
307  }
308 
309  void setForceNoLineBreaks(bool _forceNoLineBreaks) {
310  forceNoLineBreaks = _forceNoLineBreaks;
311  }
312 
313  void reset() {
314  counter = 0;
315  updateCounter = 0;
316  hasScan = false;
317  forceNoLineBreaks = false;
318  bindings.clear();
319  updateBindings.clear();
320  couldPrint.clear();
321  shouldPrint.clear();
322  couldPrintUpdates.clear();
323  shouldPrintUpdates.clear();
324  }
325 
326  void scan(const ref<Expr> &e) {
327  hasScan = true;
328  scan1(e);
329  }
330 
331  void print(const ref<Expr> &e, unsigned level=0) {
332  PrintContext PC(os);
333  PC.pos = level;
334  print(e, PC);
335  }
336 
338  bool printWidth) {
339  if (e->getWidth() == Expr::Bool)
340  PC << (e->isTrue() ? "true" : "false");
341  else {
342  if (PCAllConstWidths)
343  printWidth = true;
344 
345  if (printWidth)
346  PC << "(w" << e->getWidth() << " ";
347 
348  if (e->getWidth() <= 64) {
349  PC << e->getZExtValue();
350  } else {
351  std::string S;
352  e->toString(S);
353  PC << S;
354  }
355 
356  if (printWidth)
357  PC << ")";
358  }
359  }
360 
361  void print(const ref<Expr> &e, PrintContext &PC, bool printConstWidth=false) {
362  if (ConstantExpr *CE = dyn_cast<ConstantExpr>(e))
363  printConst(CE, PC, printConstWidth);
364  else {
365  std::map<ref<Expr>, unsigned>::iterator it = bindings.find(e);
366  if (it!=bindings.end()) {
367  PC << 'N' << it->second;
368  } else {
369  if (!hasScan || shouldPrint.count(e)) {
370  PC << 'N' << counter << ':';
371  bindings.insert(std::make_pair(e, counter++));
372  }
373 
374  // Detect multibyte reads.
375  // FIXME: Hrm. One problem with doing this is that we are
376  // masking the sharing of the indices which aren't
377  // visible. Need to think if this matters... probably not
378  // because if they are offset reads then its either constant,
379  // or they are (base + offset) and base will get printed with
380  // a declaration.
381  if (PCMultibyteReads && e->getKind() == Expr::Concat) {
382  const ReadExpr *base = hasOrderedReads(e, -1);
383  int isLSB = (base != NULL);
384  if (!isLSB)
385  base = hasOrderedReads(e, 1);
386  if (base) {
387  PC << "(Read" << (isLSB ? "LSB" : "MSB");
388  printWidth(PC, e);
389  PC << ' ';
390  printRead(base, PC, PC.pos);
391  PC << ')';
392  return;
393  }
394  }
395 
396  PC << '(' << e->getKind();
397  printWidth(PC, e);
398  PC << ' ';
399 
400  // Indent at first argument and dispatch to appropriate print
401  // routine for exprs which require special handling.
402  unsigned indent = PC.pos;
403  if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) {
404  printRead(re, PC, indent);
405  } else if (const ExtractExpr *ee = dyn_cast<ExtractExpr>(e)) {
406  printExtract(ee, PC, indent);
407  } else if (e->getKind() == Expr::Concat || e->getKind() == Expr::SExt)
408  printExpr(e.get(), PC, indent, true);
409  else
410  printExpr(e.get(), PC, indent);
411  PC << ")";
412  }
413  }
414  }
415 
416  /* Public utility functions */
417 
418  void printSeparator(PrintContext &PC, bool simple, unsigned indent) {
419  if (simple || forceNoLineBreaks) {
420  PC << ' ';
421  } else {
422  PC.breakLine(indent);
423  }
424  }
425 };
426 
427 ExprPPrinter *klee::ExprPPrinter::create(llvm::raw_ostream &os) {
428  return new PPrinter(os);
429 }
430 
431 void ExprPPrinter::printOne(llvm::raw_ostream &os,
432  const char *message,
433  const ref<Expr> &e) {
434  PPrinter p(os);
435  p.scan(e);
436 
437  // FIXME: Need to figure out what to do here. Probably print as a
438  // "forward declaration" with whatever syntax we pick for that.
439  PrintContext PC(os);
440  PC << message << ": ";
441  p.print(e, PC);
442  PC.breakLine();
443 }
444 
445 void ExprPPrinter::printSingleExpr(llvm::raw_ostream &os, const ref<Expr> &e) {
446  PPrinter p(os);
447  p.scan(e);
448 
449  // FIXME: Need to figure out what to do here. Probably print as a
450  // "forward declaration" with whatever syntax we pick for that.
451  PrintContext PC(os);
452  p.print(e, PC);
453 }
454 
455 void ExprPPrinter::printConstraints(llvm::raw_ostream &os,
456  const ConstraintManager &constraints) {
457  printQuery(os, constraints, ConstantExpr::alloc(false, Expr::Bool));
458 }
459 
460 
461 void ExprPPrinter::printQuery(llvm::raw_ostream &os,
462  const ConstraintManager &constraints,
463  const ref<Expr> &q,
464  const ref<Expr> *evalExprsBegin,
465  const ref<Expr> *evalExprsEnd,
466  const Array * const *evalArraysBegin,
467  const Array * const *evalArraysEnd,
468  bool printArrayDecls) {
469  PPrinter p(os);
470 
471  for (ConstraintManager::const_iterator it = constraints.begin(),
472  ie = constraints.end(); it != ie; ++it)
473  p.scan(*it);
474  p.scan(q);
475 
476  for (const ref<Expr> *it = evalExprsBegin; it != evalExprsEnd; ++it)
477  p.scan(*it);
478 
479  PrintContext PC(os);
480 
481  // Print array declarations.
482  if (printArrayDecls) {
483  for (const Array * const* it = evalArraysBegin; it != evalArraysEnd; ++it)
484  p.usedArrays.insert(*it);
485  for (std::set<const Array*>::iterator it = p.usedArrays.begin(),
486  ie = p.usedArrays.end(); it != ie; ++it) {
487  const Array *A = *it;
488  // FIXME: Print correct name, domain, and range.
489  PC << "array " << A->name
490  << "[" << A->size << "]"
491  << " : " << "w32" << " -> " << "w8" << " = ";
492  if (A->isSymbolicArray()) {
493  PC << "symbolic";
494  } else {
495  PC << "[";
496  for (unsigned i = 0, e = A->size; i != e; ++i) {
497  if (i)
498  PC << " ";
499  PC << A->constantValues[i];
500  }
501  PC << "]";
502  }
503  PC.breakLine();
504  }
505  }
506 
507  PC << "(query [";
508 
509  // Ident at constraint list;
510  unsigned indent = PC.pos;
511  for (ConstraintManager::const_iterator it = constraints.begin(),
512  ie = constraints.end(); it != ie;) {
513  p.print(*it, PC);
514  ++it;
515  if (it != ie)
516  PC.breakLine(indent);
517  }
518  PC << ']';
519 
520  p.printSeparator(PC, constraints.empty(), indent-1);
521  p.print(q, PC);
522 
523  // Print expressions to obtain values for, if any.
524  if (evalExprsBegin != evalExprsEnd) {
525  p.printSeparator(PC, q->isFalse(), indent-1);
526  PC << '[';
527  for (const ref<Expr> *it = evalExprsBegin; it != evalExprsEnd; ++it) {
528  p.print(*it, PC, /*printConstWidth*/true);
529  if (it + 1 != evalExprsEnd)
530  PC.breakLine(indent);
531  }
532  PC << ']';
533  }
534 
535  // Print arrays to obtain values for, if any.
536  if (evalArraysBegin != evalArraysEnd) {
537  if (evalExprsBegin == evalExprsEnd)
538  PC << " []";
539 
540  PC.breakLine(indent - 1);
541  PC << '[';
542  for (const Array * const* it = evalArraysBegin; it != evalArraysEnd; ++it) {
543  PC << (*it)->name;
544  if (it + 1 != evalArraysEnd)
545  PC.breakLine(indent);
546  }
547  PC << ']';
548  }
549 
550  PC << ')';
551  PC.breakLine();
552 }
std::map< ref< Expr >, unsigned > bindings
T * get() const
Definition: Ref.h:69
bool isSymbolicArray() const
Definition: Expr.h:641
void breakLine(unsigned indent=0)
Definition: PrintContext.h:41
bool forceNoLineBreaks
void print(const ref< Expr > &e, unsigned level=0)
void scan(const ref< Expr > &e)
constraint_iterator end() const
Definition: Constraints.h:57
void toString(std::string &Res, unsigned radix=10) const
Definition: Expr.cpp:350
bool hasScan
virtual unsigned getNumKids() const =0
std::set< ref< Expr > > shouldPrint
ref< Expr > index
Definition: Expr.h:578
void reset()
unsigned size
Definition: Expr.h:605
bool isReadExprAtOffset(ref< Expr > e, const ReadExpr *base, ref< Expr > offset)
std::vector< ref< Expr > >::iterator A
Definition: ExprUtil.cpp:123
int const char * message
Definition: klee.h:68
std::set< const UpdateNode * > shouldPrintUpdates
const std::vector< ref< ConstantExpr > > constantValues
Definition: Expr.h:610
void printSeparator(PrintContext &PC, bool simple, unsigned indent)
constraints_ty::const_iterator const_iterator
Definition: Constraints.h:27
Class representing a complete list of updates into an array.
Definition: Expr.h:655
PPrinter(llvm::raw_ostream &_os)
UpdateList updates
Definition: Expr.h:687
uint64_t getZExtValue(unsigned bits=64) const
Definition: Expr.h:361
const ReadExpr * hasOrderedReads(ref< Expr > e, int stride)
unsigned offset
Definition: Expr.h:848
void printUpdateList(const UpdateList &updates, PrintContext &PC)
void printRead(const ReadExpr *re, PrintContext &PC, unsigned indent)
ref< Expr > value
Definition: Expr.h:578
Class representing symbolic expressions.
Definition: Expr.h:88
static const Width Int8
Definition: Expr.h:98
void printConst(const ref< ConstantExpr > &e, PrintContext &PC, bool printWidth)
llvm::raw_ostream & os
void scanUpdate(const UpdateNode *un)
virtual Width getWidth() const =0
bool shouldPrintWidth(ref< Expr > e)
bool empty() const
Definition: Constraints.h:48
virtual ref< Expr > getKid(unsigned i) const =0
static void printOne(llvm::raw_ostream &os, const char *message, const ref< Expr > &e)
bool isTrue() const
isTrue - Is this the true expression.
Definition: Expr.h:432
bool isVerySimple(const ref< Expr > &e)
Width getWidth() const
Definition: Expr.h:699
void setNewline(const std::string &_newline)
bool isFalse() const
isFalse - Is this the false expression.
Definition: Expr.h:1101
const UpdateNode * head
pointer to the most recent update node
Definition: Expr.h:662
bool isSimple(const ref< Expr > &e)
constraint_iterator begin() const
Definition: Constraints.h:54
bool hasSimpleKids(const Expr *ep)
std::set< const Array * > usedArrays
void printWidth(PrintContext &PC, ref< Expr > e)
const std::string name
Definition: Expr.h:603
static ref< ConstantExpr > create(uint64_t v, Width w)
Definition: Expr.h:412
unsigned Width
The type of an expression is simply its width, in bits.
Definition: Expr.h:94
void scan1(const ref< Expr > &e)
static ref< ConstantExpr > alloc(const llvm::APInt &v)
Definition: Expr.h:398
ref< Expr > expr
Definition: Expr.h:847
std::map< const UpdateNode *, unsigned > updateBindings
static void printSingleExpr(llvm::raw_ostream &os, const ref< Expr > &e)
const UpdateNode * next
Definition: Expr.h:577
void print(const ref< Expr > &e, PrintContext &PC, bool printConstWidth=false)
static ExprPPrinter * create(llvm::raw_ostream &os)
const Array * root
Definition: Expr.h:659
virtual Kind getKind() const =0
Class representing a one byte read from an array.
Definition: Expr.h:681
unsigned updateCounter
Width getWidth() const
Definition: Expr.h:340
ref< Expr > index
Definition: Expr.h:688
Class representing a byte update of an array.
Definition: Expr.h:569
static const Width Bool
Definition: Expr.h:97
void printExpr(const Expr *ep, PrintContext &PC, unsigned indent, bool printConstWidth=false)
bool isVerySimpleUpdate(const UpdateNode *un)
unsigned counter
static void printQuery(llvm::raw_ostream &os, const ConstraintManager &constraints, const ref< Expr > &q, const ref< Expr > *evalExprsBegin=0, const ref< Expr > *evalExprsEnd=0, const Array *const *evalArraysBegin=0, const Array *const *evalArraysEnd=0, bool printArrayDecls=true)
std::string newline
unsigned pos
Number of characters on the current line.
Definition: PrintContext.h:30
void printExtract(const ExtractExpr *ee, PrintContext &PC, unsigned indent)
static void printConstraints(llvm::raw_ostream &os, const ConstraintManager &constraints)
void setForceNoLineBreaks(bool _forceNoLineBreaks)