klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExprSMTLIBLetPrinter.cpp
Go to the documentation of this file.
1 //===-- ExprSMTLIBLetPrinter.cpp ------------------------------------------*-
2 //C++ -*-===//
3 //
4 // The KLEE Symbolic Virtual Machine
5 //
6 // This file is distributed under the University of Illinois Open Source
7 // License. See LICENSE.TXT for details.
8 //
9 //===----------------------------------------------------------------------===//
10 
11 #include "llvm/Support/raw_ostream.h"
12 #include "llvm/Support/CommandLine.h"
14 
15 namespace ExprSMTLIBOptions {
16 llvm::cl::opt<bool>
17 useLetExpressions("smtlib-use-let-expressions",
18  llvm::cl::desc("Enables generated SMT-LIBv2 files to use "
19  "(let) expressions (default=on)"),
20  llvm::cl::init(true));
21 }
22 
23 namespace klee {
24 const char ExprSMTLIBLetPrinter::BINDING_PREFIX[] = "?B";
25 
27  : bindings(), firstEO(), twoOrMoreEO(), disablePrintedAbbreviations(false) {
28 }
29 
31  if (p == NULL || query == NULL || o == NULL) {
32  llvm::errs() << "Can't print SMTLIBv2. Output or query bad!\n";
33  return;
34  }
35 
37 
38  if (isHumanReadable())
39  printNotice();
40  printOptions();
41  printSetLogic();
44  printAction();
45  printExit();
46 }
47 
49  if (isa<ConstantExpr>(e))
50  return; // we don't need to scan simple constants
51 
52  if (firstEO.insert(e).second) {
53  // We've not seen this expression before
54 
55  if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) {
56 
57  // Attempt to insert array and if array wasn't present before do more
58  // things
59  if (usedArrays.insert(re->updates.root).second) {
60 
61  // check if the array is constant
62  if (re->updates.root->isConstantArray())
63  haveConstantArray = true;
64 
65  // scan the update list
66  scanUpdates(re->updates.head);
67  }
68  }
69 
70  // recurse into the children
71  Expr *ep = e.get();
72  for (unsigned int i = 0; i < ep->getNumKids(); i++)
73  scan(ep->getKid(i));
74  } else {
75  /* We must of seen the expression before. Add it to
76  * the set of twoOrMoreOccurances. We don't need to
77  * check if the insertion fails.
78  */
79  twoOrMoreEO.insert(e);
80  }
81 }
82 
84  // Assign a number to each binding that will be used
85  unsigned int counter = 0;
86  for (std::set<ref<Expr> >::const_iterator i = twoOrMoreEO.begin();
87  i != twoOrMoreEO.end(); ++i) {
88  bindings.insert(std::make_pair(*i, counter));
89  ++counter;
90  }
91 }
92 
94  const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort) {
95  std::map<const ref<Expr>, unsigned int>::const_iterator i = bindings.find(e);
96 
97  if (disablePrintedAbbreviations || i == bindings.end()) {
98  /*There is no abbreviation for this expression so print it normally.
99  * Do this by using the parent method.
100  */
101  ExprSMTLIBPrinter::printExpression(e, expectedSort);
102  } else {
103  // Use binding name e.g. "?B1"
104 
105  /* Handle the corner case where the expectedSort
106  * doesn't match the sort of the abbreviation. Not really very efficient
107  * (calls bindings.find() twice),
108  * we'll cast and call ourself again but with the correct expectedSort.
109  */
110  if (getSort(e) != expectedSort) {
111  printCastToSort(e, expectedSort);
112  return;
113  }
114 
115  // No casting is needed in this depth of recursion, just print the
116  // abbreviation
117  *p << BINDING_PREFIX << i->second;
118  }
119 }
120 
122  // Let parent clean up first
124 
125  firstEO.clear();
126  twoOrMoreEO.clear();
127  bindings.clear();
128 }
129 
131  *p << "(assert";
132  p->pushIndent();
133  printSeperator();
134 
135  if (bindings.size() != 0) {
136  // Only print let expression if we have bindings to use.
137  *p << "(let";
138  p->pushIndent();
139  printSeperator();
140  *p << "( ";
141  p->pushIndent();
142 
143  // Print each binding
144  for (std::map<const ref<Expr>, unsigned int>::const_iterator i =
145  bindings.begin();
146  i != bindings.end(); ++i) {
147  printSeperator();
148  *p << "(" << BINDING_PREFIX << i->second << " ";
149  p->pushIndent();
150 
151  // Disable abbreviations so none are used here.
153 
154  // We can abbreviate SORT_BOOL or SORT_BITVECTOR in let expressions
155  printExpression(i->first, getSort(i->first));
156 
157  p->popIndent();
158  printSeperator();
159  *p << ")";
160  }
161 
162  p->popIndent();
163  printSeperator();
164  *p << ")";
165  printSeperator();
166 
167  // Re-enable printing abbreviations.
169  }
170 
171  // print out Expressions with abbreviations.
172  unsigned int numberOfItems = query->constraints.size() + 1; //+1 for query
173  unsigned int itemsLeft = numberOfItems;
174  std::vector<ref<Expr> >::const_iterator constraint =
176 
177  /* Produce nested (and () () statements. If the constraint set
178  * is empty then we will only print the "queryAssert".
179  */
180  for (; itemsLeft != 0; --itemsLeft) {
181  if (itemsLeft >= 2) {
182  *p << "(and";
183  p->pushIndent();
184  printSeperator();
185  printExpression(*constraint,
186  SORT_BOOL); // We must and together bool expressions
187  printSeperator();
188  ++constraint;
189  continue;
190  } else {
191  // must have 1 item left (i.e. the "queryAssert")
192  if (isHumanReadable()) {
193  *p << "; query";
194  p->breakLineI();
195  }
197  SORT_BOOL); // The query must be a bool expression
198  }
199  }
200 
201  /* Produce closing brackets for nested "and statements".
202  * Number of "nested ands" = numberOfItems -1
203  */
204  itemsLeft = numberOfItems - 1;
205  for (; itemsLeft != 0; --itemsLeft) {
206  p->popIndent();
207  printSeperator();
208  *p << ")";
209  }
210 
211  if (bindings.size() != 0) {
212  // end let expression
213  p->popIndent();
214  printSeperator();
215  *p << ")";
216  printSeperator();
217  }
218 
219  // end assert
220  p->popIndent();
221  printSeperator();
222  *p << ")";
223  p->breakLineI();
224 }
225 
228  return new ExprSMTLIBLetPrinter();
229  else
230  return new ExprSMTLIBPrinter();
231 }
232 }
T * get() const
Definition: Ref.h:69
PrintContext & popIndent()
Definition: PrintContext.h:66
virtual void printExit()
Print the SMTLIBv2 command to exit.
PrintContext & pushIndent()
Definition: PrintContext.h:58
virtual unsigned getNumKids() const =0
ExprSMTLIBPrinter * createSMTLIBPrinter()
SMTLIB_SORT
Different supported SMTLIBv2 sorts (a.k.a type) in QF_AUFBV.
virtual void printArrayDeclarations()
bool haveConstantArray
Indicates if there were any constant arrays founds during a scan()
void printExpression(const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort)
std::map< const ref< Expr >, unsigned int > bindings
Let expression binding number map.
Class representing symbolic expressions.
Definition: Expr.h:88
std::set< ref< Expr > > firstEO
void printCastToSort(const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT sort)
Print an expression but cast it to a particular SMTLIBv2 sort first.
size_t size() const
Definition: Constraints.h:60
SMTLIB_SORT getSort(const ref< Expr > &e)
Determine the SMTLIBv2 sort of the expression.
virtual ref< Expr > getKid(unsigned i) const =0
const ConstraintManager & constraints
Definition: Solver.h:24
constraint_iterator begin() const
Definition: Constraints.h:54
PrintContext * p
Helper printer class.
llvm::raw_ostream * o
Output stream to write to.
virtual void scanUpdates(const UpdateNode *un)
Helper function for scan() that scans the expressions of an update node.
PrintContext & breakLineI()
Definition: PrintContext.h:50
virtual void printExpression(const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort)
Class representing a one byte read from an array.
Definition: Expr.h:681
static const char BINDING_PREFIX[]
This is the prefix string used for all abbreviations in (let) expressions.
const Query * query
The query to print.
llvm::cl::opt< bool > useLetExpressions("smtlib-use-let-expressions", llvm::cl::desc("Enables generated SMT-LIBv2 files to use ""(let) expressions (default=on)"), llvm::cl::init(true))
std::set< ref< Expr > > twoOrMoreEO
virtual void scan(const ref< Expr > &e)
std::set< const Array * > usedArrays
Contains the arrays found during scans.