klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
ExprSMTLIBPrinter.cpp
Go to the documentation of this file.
1 //===-- ExprSMTLIBPrinter.cpp -----------------------------------*- C++ -*-===//
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 #include "llvm/Support/Casting.h"
10 #include "llvm/Support/CommandLine.h"
12 
13 namespace ExprSMTLIBOptions {
14 // Command line options
15 llvm::cl::opt<klee::ExprSMTLIBPrinter::ConstantDisplayMode>
17  "smtlib-display-constants",
18  llvm::cl::desc("Sets how bitvector constants are written in generated "
19  "SMT-LIBv2 files (default=dec)"),
20  llvm::cl::values(clEnumValN(klee::ExprSMTLIBPrinter::BINARY, "bin",
21  "Use binary form (e.g. #b00101101)"),
22  clEnumValN(klee::ExprSMTLIBPrinter::HEX, "hex",
23  "Use Hexadecimal form (e.g. #x2D)"),
24  clEnumValN(klee::ExprSMTLIBPrinter::DECIMAL, "dec",
25  "Use decimal form (e.g. (_ bv45 8) )"),
26  clEnumValEnd),
27  llvm::cl::init(klee::ExprSMTLIBPrinter::DECIMAL));
28 
29 llvm::cl::opt<bool> humanReadableSMTLIB(
30  "smtlib-human-readable",
31  llvm::cl::desc(
32  "Enables generated SMT-LIBv2 files to be human readable (default=off)"),
33  llvm::cl::init(false));
34 }
35 
36 namespace klee {
37 
39  : usedArrays(), o(NULL), query(NULL), p(NULL), haveConstantArray(false),
40  logicToUse(QF_AUFBV),
41  humanReadable(ExprSMTLIBOptions::humanReadableSMTLIB),
42  smtlibBoolOptions(), arraysToCallGetValueOn(NULL) {
44 }
45 
47  if (p != NULL)
48  delete p;
49 }
50 
51 void ExprSMTLIBPrinter::setOutput(llvm::raw_ostream &output) {
52  o = &output;
53  if (p != NULL)
54  delete p;
55 
56  p = new PrintContext(output);
57 }
58 
60  query = &q;
61  reset(); // clear the data structures
62  scanAll();
64 }
65 
67  usedArrays.clear();
68  haveConstantArray = false;
69 
70  /* Clear the PRODUCE_MODELS option if it was automatically set.
71  * We need to do this because the next query might not need the
72  * (get-value) SMT-LIBv2 command.
73  */
74  if (arraysToCallGetValueOn != NULL)
76 
78 }
79 
81 
83  if (cdm > DECIMAL)
84  return false;
85 
86  this->cdm = cdm;
87  return true;
88 }
89 
91  /* Handle simple boolean constants */
92 
93  if (e->isTrue()) {
94  *p << "true";
95  return;
96  }
97 
98  if (e->isFalse()) {
99  *p << "false";
100  return;
101  }
102 
103  /* Handle bitvector constants */
104 
105  std::string value;
106 
107  /* SMTLIBv2 deduces the bit-width (should be 8-bits in our case)
108  * from the length of the string (e.g. zero is #b00000000). LLVM
109  * doesn't know about this so we need to pad the printed output
110  * with the appropriate number of zeros (zeroPad)
111  */
112  unsigned int zeroPad = 0;
113 
114  switch (cdm) {
115  case BINARY:
116  e->toString(value, 2);
117  *p << "#b";
118 
119  zeroPad = e->getWidth() - value.length();
120 
121  for (unsigned int count = 0; count < zeroPad; count++)
122  *p << "0";
123 
124  *p << value;
125  break;
126 
127  case HEX:
128  e->toString(value, 16);
129  *p << "#x";
130 
131  zeroPad = (e->getWidth() / 4) - value.length();
132  for (unsigned int count = 0; count < zeroPad; count++)
133  *p << "0";
134 
135  *p << value;
136  break;
137 
138  case DECIMAL:
139  e->toString(value, 10);
140  *p << "(_ bv" << value << " " << e->getWidth() << ")";
141  break;
142 
143  default:
144  llvm::errs() << "ExprSMTLIBPrinter::printConstant() : Unexpected Constant "
145  "display mode\n";
146  }
147 }
148 
150  const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort) {
151  // check if casting might be necessary
152  if (getSort(e) != expectedSort) {
153  printCastToSort(e, expectedSort);
154  return;
155  }
156 
157  switch (e->getKind()) {
158  case Expr::Constant:
159  printConstant(cast<ConstantExpr>(e));
160  return; // base case
161 
162  case Expr::NotOptimized:
163  // skip to child
164  printExpression(e->getKid(0), expectedSort);
165  return;
166 
167  case Expr::Read:
168  printReadExpr(cast<ReadExpr>(e));
169  return;
170 
171  case Expr::Extract:
172  printExtractExpr(cast<ExtractExpr>(e));
173  return;
174 
175  case Expr::SExt:
176  case Expr::ZExt:
177  printCastExpr(cast<CastExpr>(e));
178  return;
179 
180  case Expr::Ne:
181  printNotEqualExpr(cast<NeExpr>(e));
182  return;
183 
184  case Expr::Select:
185  // the if-then-else expression.
186  printSelectExpr(cast<SelectExpr>(e), expectedSort);
187  return;
188 
189  case Expr::Eq:
190  /* The "=" operator is special in that it can take any sort but we must
191  * enforce that both arguments are the same type. We do this a lazy way
192  * by enforcing the second argument is of the same type as the first.
193  */
194  printSortArgsExpr(e, getSort(e->getKid(0)));
195 
196  return;
197 
198  case Expr::And:
199  case Expr::Or:
200  case Expr::Xor:
201  case Expr::Not:
202  /* These operators have a bitvector version and a bool version.
203  * For these operators only (e.g. wouldn't apply to bvult) if the expected
204  * sort the
205  * expression is T then that implies the arguments are also of type T.
206  */
207  printLogicalOrBitVectorExpr(e, expectedSort);
208 
209  return;
210 
211  default:
212  /* The remaining operators (Add,Sub...,Ult,Ule,..)
213  * Expect SORT_BITVECTOR arguments
214  */
216  return;
217  }
218 }
219 
221  *p << "(" << getSMTLIBKeyword(e) << " ";
222  p->pushIndent();
223 
224  printSeperator();
225 
226  // print array with updates recursively
227  printUpdatesAndArray(e->updates.head, e->updates.root);
228 
229  // print index
230  printSeperator();
231  printExpression(e->index, SORT_BITVECTOR);
232 
233  p->popIndent();
234  printSeperator();
235  *p << ")";
236 }
237 
239  unsigned int lowIndex = e->offset;
240  unsigned int highIndex = lowIndex + e->width - 1;
241 
242  *p << "((_ " << getSMTLIBKeyword(e) << " " << highIndex << " " << lowIndex
243  << ") ";
244 
245  p->pushIndent(); // add indent for recursive call
246  printSeperator();
247 
248  // recurse
249  printExpression(e->getKid(0), SORT_BITVECTOR);
250 
251  p->popIndent(); // pop indent added for the recursive call
252  printSeperator();
253  *p << ")";
254 }
255 
257  /* sign_extend and zero_extend behave slightly unusually in SMTLIBv2
258  * instead of specifying of what bit-width we would like to extend to
259  * we specify how many bits to add to the child expression
260  *
261  * e.g
262  * ((_ sign_extend 64) (_ bv5 32))
263  *
264  * gives a (_ BitVec 96) instead of (_ BitVec 64)
265  *
266  * So we must work out how many bits we need to add.
267  *
268  * (e->width) is the desired number of bits
269  * (e->src->getWidth()) is the number of bits in the child
270  */
271  unsigned int numExtraBits = (e->width) - (e->src->getWidth());
272 
273  *p << "((_ " << getSMTLIBKeyword(e) << " " << numExtraBits << ") ";
274 
275  p->pushIndent(); // add indent for recursive call
276  printSeperator();
277 
278  // recurse
280 
281  p->popIndent(); // pop indent added for recursive call
282  printSeperator();
283 
284  *p << ")";
285 }
286 
288  *p << "(not (";
289  p->pushIndent();
290  *p << "="
291  << " ";
292  p->pushIndent();
293  printSeperator();
294 
295  /* The "=" operators allows both sorts. We assume
296  * that the second argument sort should be forced to be the same sort as the
297  * first argument
298  */
299  SMTLIB_SORT s = getSort(e->getKid(0));
300 
301  printExpression(e->getKid(0), s);
302  printSeperator();
303  printExpression(e->getKid(1), s);
304  p->popIndent();
305  printSeperator();
306 
307  *p << ")";
308  p->popIndent();
309  printSeperator();
310  *p << ")";
311 }
312 
314 
315  switch (e->getKind()) {
316  case Expr::Read:
317  return "select";
318  case Expr::Select:
319  return "ite";
320  case Expr::Concat:
321  return "concat";
322  case Expr::Extract:
323  return "extract";
324  case Expr::ZExt:
325  return "zero_extend";
326  case Expr::SExt:
327  return "sign_extend";
328 
329  case Expr::Add:
330  return "bvadd";
331  case Expr::Sub:
332  return "bvsub";
333  case Expr::Mul:
334  return "bvmul";
335  case Expr::UDiv:
336  return "bvudiv";
337  case Expr::SDiv:
338  return "bvsdiv";
339  case Expr::URem:
340  return "bvurem";
341  case Expr::SRem:
342  return "bvsrem";
343 
344  /* And, Xor, Not and Or are not handled here because there different versions
345  * for different sorts. See printLogicalOrBitVectorExpr()
346  */
347 
348  case Expr::Shl:
349  return "bvshl";
350  case Expr::LShr:
351  return "bvlshr";
352  case Expr::AShr:
353  return "bvashr";
354 
355  case Expr::Eq:
356  return "=";
357 
358  // Not Equal does not exist directly in SMTLIBv2
359 
360  case Expr::Ult:
361  return "bvult";
362  case Expr::Ule:
363  return "bvule";
364  case Expr::Ugt:
365  return "bvugt";
366  case Expr::Uge:
367  return "bvuge";
368 
369  case Expr::Slt:
370  return "bvslt";
371  case Expr::Sle:
372  return "bvsle";
373  case Expr::Sgt:
374  return "bvsgt";
375  case Expr::Sge:
376  return "bvsge";
377 
378  default:
379  return "<error>";
380  }
381 }
382 
384  const Array *root) {
385  if (un != NULL) {
386  *p << "(store ";
387  p->pushIndent();
388  printSeperator();
389 
390  // recurse to get the array or update that this store operations applies to
391  printUpdatesAndArray(un->next, root);
392 
393  printSeperator();
394 
395  // print index
397  printSeperator();
398 
399  // print value that is assigned to this index of the array
401 
402  p->popIndent();
403  printSeperator();
404  *p << ")";
405  } else {
406  // The base case of the recursion
407  *p << root->name;
408  }
409 }
410 
412  // perform scan of all expressions
414  i != query->constraints.end(); i++)
415  scan(*i);
416 
417  // Scan the query too
418  scan(query->expr);
419 }
420 
422  if (p == NULL || query == NULL || o == NULL) {
423  llvm::errs() << "ExprSMTLIBPrinter::generateOutput() Can't print SMTLIBv2. "
424  "Output or query bad!\n";
425  return;
426  }
427 
428  if (humanReadable)
429  printNotice();
430  printOptions();
431  printSetLogic();
434  printQuery();
435  printAction();
436  printExit();
437 }
438 
440  *o << "(set-logic ";
441  switch (logicToUse) {
442  case QF_ABV:
443  *o << "QF_ABV";
444  break;
445  case QF_AUFBV:
446  *o << "QF_AUFBV";
447  break;
448  }
449  *o << " )\n";
450 }
451 
452 namespace {
453 
454 struct ArrayPtrsByName {
455  bool operator()(const Array *a1, const Array *a2) const {
456  return a1->name < a2->name;
457  }
458 };
459 
460 }
461 
463  // Assume scan() has been called
464  if (humanReadable)
465  *o << "; Array declarations\n";
466 
467  // Declare arrays in a deterministic order.
468  std::vector<const Array *> sortedArrays(usedArrays.begin(), usedArrays.end());
469  std::sort(sortedArrays.begin(), sortedArrays.end(), ArrayPtrsByName());
470  for (std::vector<const Array *>::iterator it = sortedArrays.begin();
471  it != sortedArrays.end(); it++) {
472  *o << "(declare-fun " << (*it)->name << " () "
473  "(Array (_ BitVec "
474  << (*it)->getDomain() << ") "
475  "(_ BitVec " << (*it)->getRange() << ") ) )"
476  << "\n";
477  }
478 
479  // Set array values for constant values
480  if (haveConstantArray) {
481  if (humanReadable)
482  *o << "; Constant Array Definitions\n";
483 
484  const Array *array;
485 
486  // loop over found arrays
487  for (std::vector<const Array *>::iterator it = sortedArrays.begin();
488  it != sortedArrays.end(); it++) {
489  array = *it;
490  int byteIndex = 0;
491  if (array->isConstantArray()) {
492  /*loop over elements in the array and generate an assert statement
493  for each one
494  */
495  for (std::vector<ref<ConstantExpr> >::const_iterator
496  ce = array->constantValues.begin();
497  ce != array->constantValues.end(); ce++, byteIndex++) {
498  *p << "(assert (";
499  p->pushIndent();
500  *p << "= ";
501  p->pushIndent();
502  printSeperator();
503 
504  *p << "(select " << array->name << " (_ bv" << byteIndex << " "
505  << array->getDomain() << ") )";
506  printSeperator();
507  printConstant((*ce));
508 
509  p->popIndent();
510  printSeperator();
511  *p << ")";
512  p->popIndent();
513  printSeperator();
514  *p << ")";
515 
516  p->breakLineI();
517  }
518  }
519  }
520  }
521 }
522 
524  if (humanReadable)
525  *o << "; Constraints\n";
526 
527  // Generate assert statements for each constraint
529  i != query->constraints.end(); i++) {
530  *p << "(assert ";
531  p->pushIndent();
532  printSeperator();
533 
534  // recurse into Expression
536 
537  p->popIndent();
538  printSeperator();
539  *p << ")";
540  p->breakLineI();
541  }
542 }
543 
545  // Ask solver to check for satisfiability
546  *o << "(check-sat)\n";
547 
548  /* If we has arrays to find the values of then we'll
549  * ask the solver for the value of each bitvector in each array
550  */
551  if (arraysToCallGetValueOn != NULL && !arraysToCallGetValueOn->empty()) {
552 
553  const Array *theArray = 0;
554 
555  // loop over the array names
556  for (std::vector<const Array *>::const_iterator it =
557  arraysToCallGetValueOn->begin();
558  it != arraysToCallGetValueOn->end(); it++) {
559  theArray = *it;
560  // Loop over the array indices
561  for (unsigned int index = 0; index < theArray->size; ++index) {
562  *o << "(get-value ( (select " << (**it).name << " (_ bv" << index << " "
563  << theArray->getDomain() << ") ) ) )\n";
564  }
565  }
566  }
567 }
568 
570  if (e.isNull()) {
571  llvm::errs() << "ExprSMTLIBPrinter::scan() : Found NULL expression!"
572  << "\n";
573  return;
574  }
575 
576  if (isa<ConstantExpr>(e))
577  return; // we don't need to scan simple constants
578 
579  if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) {
580 
581  // Attempt to insert array and if array wasn't present before do more things
582  if (usedArrays.insert(re->updates.root).second) {
583 
584  // check if the array is constant
585  if (re->updates.root->isConstantArray())
586  haveConstantArray = true;
587 
588  // scan the update list
589  scanUpdates(re->updates.head);
590  }
591  }
592 
593  // recurse into the children
594  Expr *ep = e.get();
595  for (unsigned int i = 0; i < ep->getNumKids(); i++)
596  scan(ep->getKid(i));
597 }
598 
600  while (un != NULL) {
601  scan(un->index);
602  scan(un->value);
603  un = un->next;
604  }
605 }
606 
607 void ExprSMTLIBPrinter::printExit() { *o << "(exit)\n"; }
608 
610  if (l > QF_AUFBV)
611  return false;
612 
613  logicToUse = l;
614  return true;
615 }
616 
618  if (humanReadable)
619  p->breakLineI();
620  else
621  p->write(" ");
622 }
623 
625  *o << "; This file conforms to SMTLIBv2 and was generated by KLEE\n";
626 }
627 
629 
631  // Print out SMTLIBv2 boolean options
632  for (std::map<SMTLIBboolOptions, bool>::const_iterator i =
633  smtlibBoolOptions.begin();
634  i != smtlibBoolOptions.end(); i++) {
635  *o << "(set-option :" << getSMTLIBOptionString(i->first) << " "
636  << ((i->second) ? "true" : "false") << ")\n";
637  }
638 }
639 
641  if (humanReadable) {
642  *p << "; Query from solver turned into an assert";
643  p->breakLineI();
644  }
645 
646  p->pushIndent();
647  *p << "(assert";
648  p->pushIndent();
649  printSeperator();
650 
652 
653  p->popIndent();
654  printSeperator();
655  *p << ")";
656  p->popIndent();
657  p->breakLineI();
658 }
659 
661  switch (e->getKind()) {
662  case Expr::NotOptimized:
663  return getSort(e->getKid(0));
664 
665  // The relational operators are bools.
666  case Expr::Eq:
667  case Expr::Ne:
668  case Expr::Slt:
669  case Expr::Sle:
670  case Expr::Sgt:
671  case Expr::Sge:
672  case Expr::Ult:
673  case Expr::Ule:
674  case Expr::Ugt:
675  case Expr::Uge:
676  return SORT_BOOL;
677 
678  // These may be bitvectors or bools depending on their width (see
679  // printConstant and printLogicalOrBitVectorExpr).
680  case Expr::Constant:
681  case Expr::And:
682  case Expr::Not:
683  case Expr::Or:
684  case Expr::Xor:
685  return e->getWidth() == Expr::Bool ? SORT_BOOL : SORT_BITVECTOR;
686 
687  // Everything else is a bitvector.
688  default:
689  return SORT_BITVECTOR;
690  }
691 }
692 
695  switch (sort) {
696  case SORT_BITVECTOR:
697  if (humanReadable) {
698  p->breakLineI();
699  *p << ";Performing implicit bool to bitvector cast";
700  p->breakLine();
701  }
702  // We assume the e is a bool that we need to cast to a bitvector sort.
703  *p << "(ite";
704  p->pushIndent();
705  printSeperator();
707  printSeperator();
708  *p << "(_ bv1 1)";
709  printSeperator(); // printing the "true" bitvector
710  *p << "(_ bv0 1)";
711  p->popIndent();
712  printSeperator(); // printing the "false" bitvector
713  *p << ")";
714  break;
715  case SORT_BOOL: {
716  /* We make the assumption (might be wrong) that any bitvector whos unsigned
717  *decimal value is
718  * is zero is interpreted as "false", otherwise it is true.
719  *
720  * This may not be the interpretation we actually want!
721  */
722  Expr::Width bitWidth = e->getWidth();
723  if (humanReadable) {
724  p->breakLineI();
725  *p << ";Performing implicit bitvector to bool cast";
726  p->breakLine();
727  }
728  *p << "(bvugt";
729  p->pushIndent();
730  printSeperator();
731  // We assume is e is a bitvector
733  printSeperator();
734  *p << "(_ bv0 " << bitWidth << ")";
735  p->popIndent();
736  printSeperator(); // Zero bitvector of required width
737  *p << ")";
738 
739  if (bitWidth != Expr::Bool)
740  llvm::errs()
741  << "ExprSMTLIBPrinter : Warning. Casting a bitvector (length "
742  << bitWidth << ") to bool!\n";
743 
744  } break;
745  default:
746  assert(0 && "Unsupported cast!");
747  }
748 }
749 
752  // This is the if-then-else expression
753 
754  *p << "(" << getSMTLIBKeyword(e) << " ";
755  p->pushIndent(); // add indent for recursive call
756 
757  // The condition
758  printSeperator();
759  printExpression(e->getKid(0), SORT_BOOL);
760 
761  /* This operator is special in that the remaining children
762  * can be of any sort.
763  */
764 
765  // if true
766  printSeperator();
767  printExpression(e->getKid(1), s);
768 
769  // if false
770  printSeperator();
771  printExpression(e->getKid(2), s);
772 
773  p->popIndent(); // pop indent added for recursive call
774  printSeperator();
775  *p << ")";
776 }
777 
780  *p << "(" << getSMTLIBKeyword(e) << " ";
781  p->pushIndent(); // add indent for recursive call
782 
783  // loop over children and recurse into each expecting they are of sort "s"
784  for (unsigned int i = 0; i < e->getNumKids(); i++) {
785  printSeperator();
786  printExpression(e->getKid(i), s);
787  }
788 
789  p->popIndent(); // pop indent added for recursive call
790  printSeperator();
791  *p << ")";
792 }
793 
796  /* For these operators it is the case that the expected sort is the same as
797  * the sorts
798  * of the arguments.
799  */
800 
801  *p << "(";
802  switch (e->getKind()) {
803  case Expr::And:
804  *p << ((s == SORT_BITVECTOR) ? "bvand" : "and");
805  break;
806  case Expr::Not:
807  *p << ((s == SORT_BITVECTOR) ? "bvnot" : "not");
808  break;
809  case Expr::Or:
810  *p << ((s == SORT_BITVECTOR) ? "bvor" : "or");
811  break;
812 
813  case Expr::Xor:
814  *p << ((s == SORT_BITVECTOR) ? "bvxor" : "xor");
815  break;
816  default:
817  *p << "ERROR"; // this shouldn't happen
818  }
819  *p << " ";
820 
821  p->pushIndent(); // add indent for recursive call
822 
823  // loop over children and recurse into each expecting they are of sort "s"
824  for (unsigned int i = 0; i < e->getNumKids(); i++) {
825  printSeperator();
826  printExpression(e->getKid(i), s);
827  }
828 
829  p->popIndent(); // pop indent added for recursive call
830  printSeperator();
831  *p << ")";
832 }
833 
835  // Negating the query
837 }
838 
840  SMTLIBboolValues value) {
841  std::pair<std::map<SMTLIBboolOptions, bool>::iterator, bool> thePair;
842  bool theValue = (value == OPTION_TRUE) ? true : false;
843 
844  switch (option) {
845  case PRINT_SUCCESS:
846  case PRODUCE_MODELS:
847  case INTERACTIVE_MODE:
848  thePair = smtlibBoolOptions.insert(
849  std::pair<SMTLIBboolOptions, bool>(option, theValue));
850 
851  if (value == OPTION_DEFAULT) {
852  // we should unset (by removing from map) this option so the solver uses
853  // its default
854  smtlibBoolOptions.erase(thePair.first);
855  return true;
856  }
857 
858  if (!thePair.second) {
859  // option was already present so modify instead.
860  thePair.first->second = value;
861  }
862  return true;
863  default:
864  return false;
865  }
866 }
867 
868 void
869 ExprSMTLIBPrinter::setArrayValuesToGet(const std::vector<const Array *> &a) {
871 
872  // This option must be set in order to use the SMTLIBv2 command (get-value ()
873  // )
874  if (!a.empty())
876 
877  /* There is a risk that users will ask about array values that aren't
878  * even in the query. We should add them to the usedArrays list and hope
879  * that the solver knows what to do when we ask for the values of arrays
880  * that don't feature in our query!
881  */
882  for (std::vector<const Array *>::const_iterator i = a.begin(); i != a.end();
883  ++i) {
884  usedArrays.insert(*i);
885  }
886 }
887 
890  switch (option) {
891  case PRINT_SUCCESS:
892  return "print-success";
893  case PRODUCE_MODELS:
894  return "produce-models";
895  case INTERACTIVE_MODE:
896  return "interactive-mode";
897  default:
898  return "unknown-option";
899  }
900 }
901 }
T * get() const
Definition: Ref.h:69
virtual void printLogicalOrBitVectorExpr(const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT s)
void breakLine(unsigned indent=0)
Definition: PrintContext.h:41
PrintContext & popIndent()
Definition: PrintContext.h:66
constraint_iterator end() const
Definition: Constraints.h:57
virtual void printExit()
Print the SMTLIBv2 command to exit.
ExprSMTLIBPrinter()
Create a new printer that will print a query in the SMTLIBv2 language.
PrintContext & pushIndent()
Definition: PrintContext.h:58
void setQuery(const Query &q)
Not used in canonical form.
Definition: Expr.h:151
virtual unsigned getNumKids() const =0
virtual void printReadExpr(const ref< ReadExpr > &e)
ref< Expr > index
Definition: Expr.h:578
std::map< SMTLIBboolOptions, bool > smtlibBoolOptions
unsigned size
Definition: Expr.h:605
virtual void printNotEqualExpr(const ref< NeExpr > &e)
ref< Expr > expr
Definition: Solver.h:25
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()
const std::vector< ref< ConstantExpr > > constantValues
Definition: Expr.h:610
constraints_ty::const_iterator const_iterator
Definition: Constraints.h:27
void write(const std::string &s)
Definition: PrintContext.h:74
Not used in canonical form.
Definition: Expr.h:155
Display bit vector constants in Decimal e.g. (_ bv45 8)
ref< Expr > value
Definition: Expr.h:578
Not used in canonical form.
Definition: Expr.h:154
Class representing symbolic expressions.
Definition: Expr.h:88
Display bit vector constants in Hexidecimal e.g.#x2D.
Not used in canonical form.
Definition: Expr.h:158
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 Width getWidth() const =0
virtual ref< Expr > getKid(unsigned i) const =0
bool isNull() const
Definition: Ref.h:99
virtual void printSortArgsExpr(const ref< Expr > &e, ExprSMTLIBPrinter::SMTLIB_SORT s)
virtual void scan(const ref< Expr > &e)
static ref< Expr > createIsZero(ref< Expr > e)
Definition: Expr.cpp:305
const ConstraintManager & constraints
Definition: Solver.h:24
llvm::cl::opt< klee::ExprSMTLIBPrinter::ConstantDisplayMode > argConstantDisplayMode("smtlib-display-constants", llvm::cl::desc("Sets how bitvector constants are written in generated ""SMT-LIBv2 files (default=dec)"), llvm::cl::values(clEnumValN(klee::ExprSMTLIBPrinter::BINARY,"bin","Use binary form (e.g. #b00101101)"), clEnumValN(klee::ExprSMTLIBPrinter::HEX,"hex","Use Hexadecimal form (e.g. #x2D)"), clEnumValN(klee::ExprSMTLIBPrinter::DECIMAL,"dec","Use decimal form (e.g. (_ bv45 8) )"), clEnumValEnd), llvm::cl::init(klee::ExprSMTLIBPrinter::DECIMAL))
constraint_iterator begin() const
Definition: Constraints.h:54
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
const std::string name
Definition: Expr.h:603
virtual void scanUpdates(const UpdateNode *un)
Helper function for scan() that scans the expressions of an update node.
PrintContext & breakLineI()
Definition: PrintContext.h:50
unsigned Width
The type of an expression is simply its width, in bits.
Definition: Expr.h:94
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)
const UpdateNode * next
Definition: Expr.h:577
bool isConstantArray() const
Definition: Expr.h:642
Expr::Width getDomain() const
Definition: Expr.h:644
virtual Kind getKind() const =0
Class representing a one byte read from an array.
Definition: Expr.h:681
llvm::cl::opt< bool > humanReadableSMTLIB("smtlib-human-readable", llvm::cl::desc("Enables generated SMT-LIBv2 files to be human readable (default=off)"), llvm::cl::init(false))
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.
static const Width Bool
Definition: Expr.h:97
Not used in canonical form.
Definition: Expr.h:159
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.