klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExprSMTLIBPrinter.h
Go to the documentation of this file.
1 //===-- ExprSMTLIBPrinter.h ------------------------------------------*- C++
2 //-*-===//
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 #ifndef KLEE_EXPRSMTLIBPRINTER_H
12 #define KLEE_EXPRSMTLIBPRINTER_H
13 
14 #include <string>
15 #include <set>
16 #include <map>
17 #include <klee/Constraints.h>
18 #include <klee/Expr.h>
19 #include <klee/util/PrintContext.h>
20 #include <klee/Solver.h>
21 
22 namespace llvm {
23 class raw_ostream;
24 }
25 
26 namespace klee {
27 
80 public:
86  };
88 
95  };
96 
103  };
105 
108  HEX,
110  };
111 
114 
119 
121 
124 
127  void setOutput(llvm::raw_ostream &output);
128 
132  void setQuery(const Query &q);
133 
134  virtual ~ExprSMTLIBPrinter();
135 
153  virtual void generateOutput();
154 
161  bool setLogic(SMTLIBv2Logic l);
162 
170  void setHumanReadable(bool hr);
171 
184 
198  void setArrayValuesToGet(const std::vector<const Array *> &a);
199 
201  bool isHumanReadable();
202 
203 protected:
205  std::set<const Array *> usedArrays;
206 
208  llvm::raw_ostream *o;
209 
211  const Query *query;
212 
214  SMTLIB_SORT getSort(const ref<Expr> &e);
215 
218 
219  // Resets various internal objects for a new query
220  virtual void reset();
221 
222  // Scan all constraints and the query
223  virtual void scanAll();
224 
225  // Print an initial SMTLIBv2 comment before anything else is printed
226  virtual void printNotice();
227 
228  // Print SMTLIBv2 options e.g. (set-option :option-name <value>) command
229  virtual void printOptions();
230 
231  // Print SMTLIBv2 logic to use e.g. (set-logic QF_ABV)
232  virtual void printSetLogic();
233 
234  // Print SMTLIBv2 assertions for constant arrays
235  virtual void printArrayDeclarations();
236 
237  // Print SMTLIBv2 for all constraints in the query
238  virtual void printConstraints();
239 
240  // Print SMTLIBv2 assert statement for the negated query expression
241  virtual void printQuery();
242 
246  virtual void printAction();
247 
249  virtual void printExit();
250 
253  void printConstant(const ref<ConstantExpr> &e);
254 
259  virtual void printExpression(const ref<Expr> &e,
260  ExprSMTLIBPrinter::SMTLIB_SORT expectedSort);
261 
265  virtual void scan(const ref<Expr> &e);
266 
267  /* Rules of recursion for "Special Expression handlers" and
268  *printSortArgsExpr()
269  *
270  * 1. The parent of the recursion will have created an indent level for you so
271  *you don't need to add another initially.
272  * 2. You do not need to add a line break (via printSeperator() ) at the end,
273  *the parent caller will handle that.
274  * 3. The effect of a single recursive call should not affect the depth of the
275  *indent stack (nor the contents
276  * of the indent stack prior to the call). I.e. After executing a single
277  *recursive call the indent stack
278  * should have the same size and contents as before executing the recursive
279  *call.
280  */
281 
282  // Special Expression handlers
283  virtual void printReadExpr(const ref<ReadExpr> &e);
284  virtual void printExtractExpr(const ref<ExtractExpr> &e);
285  virtual void printCastExpr(const ref<CastExpr> &e);
286  virtual void printNotEqualExpr(const ref<NeExpr> &e);
287  virtual void printSelectExpr(const ref<SelectExpr> &e,
289 
290  // For the set of operators that take sort "s" arguments
291  virtual void printSortArgsExpr(const ref<Expr> &e,
293 
299  virtual void printLogicalOrBitVectorExpr(const ref<Expr> &e,
301 
303  virtual void printUpdatesAndArray(const UpdateNode *un, const Array *root);
304 
308  virtual const char *getSMTLIBKeyword(const ref<Expr> &e);
309 
310  virtual void printSeperator();
311 
313  virtual void scanUpdates(const UpdateNode *un);
314 
317 
321 
324 
325 private:
327 
328  volatile bool humanReadable;
329 
330  // Map of enabled SMTLIB Options
331  std::map<SMTLIBboolOptions, bool> smtlibBoolOptions;
332 
334  void negateQueryExpression();
335 
336  // Print a SMTLIBv2 option as a C-string
337  const char *
339 
340  // Pointer to a vector of Arrays. These will be used for the (get-value () )
341  // call.
342  const std::vector<const Array *> *arraysToCallGetValueOn;
343 
345 };
346 }
347 
348 #endif
virtual void printLogicalOrBitVectorExpr(const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT s)
virtual void printExit()
Print the SMTLIBv2 command to exit.
ExprSMTLIBPrinter()
Create a new printer that will print a query in the SMTLIBv2 language.
void setQuery(const Query &q)
virtual void printReadExpr(const ref< ReadExpr > &e)
std::map< SMTLIBboolOptions, bool > smtlibBoolOptions
virtual void printNotEqualExpr(const ref< NeExpr > &e)
virtual void printUpdatesAndArray(const UpdateNode *un, const Array *root)
Recursively prints updatesNodes.
const char * getSMTLIBOptionString(ExprSMTLIBPrinter::SMTLIBboolOptions option)
const std::vector< const Array * > * arraysToCallGetValueOn
bool setConstantDisplayMode(ConstantDisplayMode cdm)
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()
Display bit vector constants in Decimal e.g. (_ bv45 8)
Display bit vector constants in Hexidecimal e.g.#x2D.
void printCastToSort(const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT sort)
Print an expression but cast it to a particular SMTLIBv2 sort first.
void setOutput(llvm::raw_ostream &output)
SMTLIB_SORT getSort(const ref< Expr > &e)
Determine the SMTLIBv2 sort of the expression.
virtual void printSortArgsExpr(const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT s)
virtual void scan(const ref< Expr > &e)
void negateQueryExpression()
This sets queryAssert to be the boolean negation of the original Query.
PrintContext * p
Helper printer class.
llvm::raw_ostream * o
Output stream to write to.
interactive-mode SMTLIBv2 option
ConstantDisplayMode cdm
virtual void scanUpdates(const UpdateNode *un)
Helper function for scan() that scans the expressions of an update node.
bool setLogic(SMTLIBv2Logic l)
virtual void printExpression(const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort)
virtual void printSelectExpr(const ref< SelectExpr > &e, ExprSMTLIBPrinter::SMTLIB_SORT s)
void printConstant(const ref< ConstantExpr > &e)
Display bit vector constants in binary e.g. #b00101101.
bool setSMTLIBboolOption(SMTLIBboolOptions option, SMTLIBboolValues value)
virtual void printCastExpr(const ref< CastExpr > &e)
ConstantDisplayMode getConstantDisplayMode()
void setArrayValuesToGet(const std::vector< const Array * > &a)
Class representing a byte update of an array.
Definition: Expr.h:569
Logic using Theory of Arrays and Theory of Bitvectors.
print-success SMTLIBv2 option
produce-models SMTLIBv2 option
const Query * query
The query to print.
virtual const char * getSMTLIBKeyword(const ref< Expr > &e)
virtual void printExtractExpr(const ref< ExtractExpr > &e)
std::set< const Array * > usedArrays
Contains the arrays found during scans.