diff options
Diffstat (limited to 'lib/Expr/ExprSMTLIBPrinter.cpp')
| -rw-r--r-- | lib/Expr/ExprSMTLIBPrinter.cpp | 96 |
1 files changed, 53 insertions, 43 deletions
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index c32b5bf9..bbb82d0d 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -1,5 +1,4 @@ -//===-- ExprSMTLIBPrinter.cpp ------------------------------------------*- C++ -//-*-===// +//===-- ExprSMTLIBPrinter.cpp -----------------------------------*- C++ -*-===// // // The KLEE Symbolic Virtual Machine // @@ -7,14 +6,10 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// -#include <iostream> - #include "llvm/Support/Casting.h" #include "llvm/Support/CommandLine.h" #include "klee/util/ExprSMTLIBPrinter.h" -using namespace std; - namespace ExprSMTLIBOptions { // Command line options llvm::cl::opt<klee::ExprSMTLIBPrinter::ConstantDisplayMode> @@ -53,7 +48,7 @@ ExprSMTLIBPrinter::~ExprSMTLIBPrinter() { delete p; } -void ExprSMTLIBPrinter::setOutput(std::ostream &output) { +void ExprSMTLIBPrinter::setOutput(llvm::raw_ostream &output) { o = &output; if (p != NULL) delete p; @@ -146,8 +141,8 @@ void ExprSMTLIBPrinter::printConstant(const ref<ConstantExpr> &e) { break; default: - std::cerr << "ExprSMTLIBPrinter::printConstant() : Unexpected Constant " - "display mode" << std::endl; + llvm::errs() << "ExprSMTLIBPrinter::printConstant() : Unexpected Constant " + "display mode\n"; } } @@ -425,8 +420,8 @@ void ExprSMTLIBPrinter::scanAll() { void ExprSMTLIBPrinter::generateOutput() { if (p == NULL || query == NULL || o == NULL) { - std::cerr << "ExprSMTLIBPrinter::generateOutput() Can't print SMTLIBv2. " - "Output or query bad!" << std::endl; + llvm::errs() << "ExprSMTLIBPrinter::generateOutput() Can't print SMTLIBv2. " + "Output or query bad!\n"; return; } @@ -451,7 +446,7 @@ void ExprSMTLIBPrinter::printSetLogic() { *o << "QF_AUFBV"; break; } - *o << " )" << std::endl; + *o << " )\n"; } namespace { @@ -467,7 +462,7 @@ struct ArrayPtrsByName { void ExprSMTLIBPrinter::printArrayDeclarations() { // Assume scan() has been called if (humanReadable) - *o << "; Array declarations" << endl; + *o << "; Array declarations\n"; // Declare arrays in a deterministic order. std::vector<const Array *> sortedArrays(usedArrays.begin(), usedArrays.end()); @@ -478,13 +473,13 @@ void ExprSMTLIBPrinter::printArrayDeclarations() { "(Array (_ BitVec " << (*it)->getDomain() << ") " "(_ BitVec " << (*it)->getRange() << ") ) )" - << endl; + << "\n"; } // Set array values for constant values if (haveConstantArray) { if (humanReadable) - *o << "; Constant Array Definitions" << endl; + *o << "; Constant Array Definitions\n"; const Array *array; @@ -497,7 +492,7 @@ void ExprSMTLIBPrinter::printArrayDeclarations() { /*loop over elements in the array and generate an assert statement for each one */ - for (vector<ref<ConstantExpr> >::const_iterator + for (std::vector<ref<ConstantExpr> >::const_iterator ce = array->constantValues.begin(); ce != array->constantValues.end(); ce++, byteIndex++) { *p << "(assert ("; @@ -527,7 +522,7 @@ void ExprSMTLIBPrinter::printArrayDeclarations() { void ExprSMTLIBPrinter::printConstraints() { if (humanReadable) - *o << "; Constraints" << endl; + *o << "; Constraints\n"; // Generate assert statements for each constraint for (ConstraintManager::const_iterator i = query->constraints.begin(); @@ -548,7 +543,7 @@ void ExprSMTLIBPrinter::printConstraints() { void ExprSMTLIBPrinter::printAction() { // Ask solver to check for satisfiability - *o << "(check-sat)" << endl; + *o << "(check-sat)\n"; /* If we has arrays to find the values of then we'll * ask the solver for the value of each bitvector in each array @@ -558,14 +553,14 @@ void ExprSMTLIBPrinter::printAction() { const Array *theArray = 0; // loop over the array names - for (vector<const Array *>::const_iterator it = + for (std::vector<const Array *>::const_iterator it = arraysToCallGetValueOn->begin(); it != arraysToCallGetValueOn->end(); it++) { theArray = *it; // Loop over the array indices for (unsigned int index = 0; index < theArray->size; ++index) { *o << "(get-value ( (select " << (**it).name << " (_ bv" << index << " " - << theArray->getDomain() << ") ) ) )" << endl; + << theArray->getDomain() << ") ) ) )\n"; } } } @@ -573,8 +568,8 @@ void ExprSMTLIBPrinter::printAction() { void ExprSMTLIBPrinter::scan(const ref<Expr> &e) { if (e.isNull()) { - std::cerr << "ExprSMTLIBPrinter::scan() : Found NULL expression!" - << std::endl; + llvm::errs() << "ExprSMTLIBPrinter::scan() : Found NULL expression!" + << "\n"; return; } @@ -609,7 +604,7 @@ void ExprSMTLIBPrinter::scanUpdates(const UpdateNode *un) { } } -void ExprSMTLIBPrinter::printExit() { *o << "(exit)" << endl; } +void ExprSMTLIBPrinter::printExit() { *o << "(exit)\n"; } bool ExprSMTLIBPrinter::setLogic(SMTLIBv2Logic l) { if (l > QF_AUFBV) @@ -627,7 +622,7 @@ void ExprSMTLIBPrinter::printSeperator() { } void ExprSMTLIBPrinter::printNotice() { - *o << "; This file conforms to SMTLIBv2 and was generated by KLEE" << endl; + *o << "; This file conforms to SMTLIBv2 and was generated by KLEE\n"; } void ExprSMTLIBPrinter::setHumanReadable(bool hr) { humanReadable = hr; } @@ -638,7 +633,7 @@ void ExprSMTLIBPrinter::printOptions() { smtlibBoolOptions.begin(); i != smtlibBoolOptions.end(); i++) { *o << "(set-option :" << getSMTLIBOptionString(i->first) << " " - << ((i->second) ? "true" : "false") << ")" << endl; + << ((i->second) ? "true" : "false") << ")\n"; } } @@ -663,23 +658,36 @@ void ExprSMTLIBPrinter::printQuery() { } ExprSMTLIBPrinter::SMTLIB_SORT ExprSMTLIBPrinter::getSort(const ref<Expr> &e) { - /* We could handle every operator in a large switch statement, - * but this seems more elegant. - */ + switch (e->getKind()) { + case Expr::NotOptimized: + return getSort(e->getKid(0)); - if (e->getKind() == Expr::Extract) { - /* This is a special corner case. In most cases if a node in the expression - * tree - * is of width 1 it should be considered as SORT_BOOL. However it is - * possible to - * perform an extract operation on a SORT_BITVECTOR and produce a - * SORT_BITVECTOR of length 1. - * The ((_ extract i j) () ) operation in SMTLIBv2 always produces - * SORT_BITVECTOR - */ + // The relational operators are bools. + case Expr::Eq: + case Expr::Ne: + case Expr::Slt: + case Expr::Sle: + case Expr::Sgt: + case Expr::Sge: + case Expr::Ult: + case Expr::Ule: + case Expr::Ugt: + case Expr::Uge: + return SORT_BOOL; + + // These may be bitvectors or bools depending on their width (see + // printConstant and printLogicalOrBitVectorExpr). + case Expr::Constant: + case Expr::And: + case Expr::Not: + case Expr::Or: + case Expr::Xor: + return e->getWidth() == Expr::Bool ? SORT_BOOL : SORT_BITVECTOR; + + // Everything else is a bitvector. + default: return SORT_BITVECTOR; - } else - return (e->getWidth() == Expr::Bool) ? (SORT_BOOL) : (SORT_BITVECTOR); + } } void ExprSMTLIBPrinter::printCastToSort(const ref<Expr> &e, @@ -729,8 +737,9 @@ void ExprSMTLIBPrinter::printCastToSort(const ref<Expr> &e, *p << ")"; if (bitWidth != Expr::Bool) - std::cerr << "ExprSMTLIBPrinter : Warning. Casting a bitvector (length " - << bitWidth << ") to bool!" << std::endl; + llvm::errs() + << "ExprSMTLIBPrinter : Warning. Casting a bitvector (length " + << bitWidth << ") to bool!\n"; } break; default: @@ -870,7 +879,8 @@ ExprSMTLIBPrinter::setArrayValuesToGet(const std::vector<const Array *> &a) { * that the solver knows what to do when we ask for the values of arrays * that don't feature in our query! */ - for (vector<const Array *>::const_iterator i = a.begin(); i != a.end(); ++i) { + for (std::vector<const Array *>::const_iterator i = a.begin(); i != a.end(); + ++i) { usedArrays.insert(*i); } } |