diff options
Diffstat (limited to 'lib/Expr')
| -rw-r--r-- | lib/Expr/ExprSMTLIBLetPrinter.cpp | 232 | ||||
| -rw-r--r-- | lib/Expr/ExprSMTLIBPrinter.cpp | 150 |
2 files changed, 123 insertions, 259 deletions
diff --git a/lib/Expr/ExprSMTLIBLetPrinter.cpp b/lib/Expr/ExprSMTLIBLetPrinter.cpp deleted file mode 100644 index d4243452..00000000 --- a/lib/Expr/ExprSMTLIBLetPrinter.cpp +++ /dev/null @@ -1,232 +0,0 @@ -//===-- ExprSMTLIBLetPrinter.cpp ------------------------------------------*- -//C++ -*-===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#include "llvm/Support/raw_ostream.h" -#include "llvm/Support/CommandLine.h" -#include "klee/util/ExprSMTLIBLetPrinter.h" - -namespace ExprSMTLIBOptions { -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)); -} - -namespace klee { -const char ExprSMTLIBLetPrinter::BINDING_PREFIX[] = "?B"; - -ExprSMTLIBLetPrinter::ExprSMTLIBLetPrinter() - : bindings(), firstEO(), twoOrMoreEO(), disablePrintedAbbreviations(false) { -} - -void ExprSMTLIBLetPrinter::generateOutput() { - if (p == NULL || query == NULL || o == NULL) { - llvm::errs() << "Can't print SMTLIBv2. Output or query bad!\n"; - return; - } - - generateBindings(); - - if (isHumanReadable()) - printNotice(); - printOptions(); - printSetLogic(); - printArrayDeclarations(); - printLetExpression(); - printAction(); - printExit(); -} - -void ExprSMTLIBLetPrinter::scan(const ref<Expr> &e) { - if (isa<ConstantExpr>(e)) - return; // we don't need to scan simple constants - - if (firstEO.insert(e).second) { - // We've not seen this expression before - - if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) { - - // Attempt to insert array and if array wasn't present before do more - // things - if (usedArrays.insert(re->updates.root).second) { - - // check if the array is constant - if (re->updates.root->isConstantArray()) - haveConstantArray = true; - - // scan the update list - scanUpdates(re->updates.head); - } - } - - // recurse into the children - Expr *ep = e.get(); - for (unsigned int i = 0; i < ep->getNumKids(); i++) - scan(ep->getKid(i)); - } else { - /* We must of seen the expression before. Add it to - * the set of twoOrMoreOccurances. We don't need to - * check if the insertion fails. - */ - twoOrMoreEO.insert(e); - } -} - -void ExprSMTLIBLetPrinter::generateBindings() { - // Assign a number to each binding that will be used - unsigned int counter = 0; - for (std::set<ref<Expr> >::const_iterator i = twoOrMoreEO.begin(); - i != twoOrMoreEO.end(); ++i) { - bindings.insert(std::make_pair(*i, counter)); - ++counter; - } -} - -void ExprSMTLIBLetPrinter::printExpression( - const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort) { - std::map<const ref<Expr>, unsigned int>::const_iterator i = bindings.find(e); - - if (disablePrintedAbbreviations || i == bindings.end()) { - /*There is no abbreviation for this expression so print it normally. - * Do this by using the parent method. - */ - ExprSMTLIBPrinter::printExpression(e, expectedSort); - } else { - // Use binding name e.g. "?B1" - - /* Handle the corner case where the expectedSort - * doesn't match the sort of the abbreviation. Not really very efficient - * (calls bindings.find() twice), - * we'll cast and call ourself again but with the correct expectedSort. - */ - if (getSort(e) != expectedSort) { - printCastToSort(e, expectedSort); - return; - } - - // No casting is needed in this depth of recursion, just print the - // abbreviation - *p << BINDING_PREFIX << i->second; - } -} - -void ExprSMTLIBLetPrinter::reset() { - // Let parent clean up first - ExprSMTLIBPrinter::reset(); - - firstEO.clear(); - twoOrMoreEO.clear(); - bindings.clear(); -} - -void ExprSMTLIBLetPrinter::printLetExpression() { - *p << "(assert"; - p->pushIndent(); - printSeperator(); - - if (bindings.size() != 0) { - // Only print let expression if we have bindings to use. - *p << "(let"; - p->pushIndent(); - printSeperator(); - *p << "( "; - p->pushIndent(); - - // Print each binding - for (std::map<const ref<Expr>, unsigned int>::const_iterator i = - bindings.begin(); - i != bindings.end(); ++i) { - printSeperator(); - *p << "(" << BINDING_PREFIX << i->second << " "; - p->pushIndent(); - - // Disable abbreviations so none are used here. - disablePrintedAbbreviations = true; - - // We can abbreviate SORT_BOOL or SORT_BITVECTOR in let expressions - printExpression(i->first, getSort(i->first)); - - p->popIndent(); - printSeperator(); - *p << ")"; - } - - p->popIndent(); - printSeperator(); - *p << ")"; - printSeperator(); - - // Re-enable printing abbreviations. - disablePrintedAbbreviations = false; - } - - // print out Expressions with abbreviations. - unsigned int numberOfItems = query->constraints.size() + 1; //+1 for query - unsigned int itemsLeft = numberOfItems; - std::vector<ref<Expr> >::const_iterator constraint = - query->constraints.begin(); - - /* Produce nested (and () () statements. If the constraint set - * is empty then we will only print the "queryAssert". - */ - for (; itemsLeft != 0; --itemsLeft) { - if (itemsLeft >= 2) { - *p << "(and"; - p->pushIndent(); - printSeperator(); - printExpression(*constraint, - SORT_BOOL); // We must and together bool expressions - printSeperator(); - ++constraint; - continue; - } else { - // must have 1 item left (i.e. the "queryAssert") - if (isHumanReadable()) { - *p << "; query"; - p->breakLineI(); - } - printExpression(queryAssert, - SORT_BOOL); // The query must be a bool expression - } - } - - /* Produce closing brackets for nested "and statements". - * Number of "nested ands" = numberOfItems -1 - */ - itemsLeft = numberOfItems - 1; - for (; itemsLeft != 0; --itemsLeft) { - p->popIndent(); - printSeperator(); - *p << ")"; - } - - if (bindings.size() != 0) { - // end let expression - p->popIndent(); - printSeperator(); - *p << ")"; - printSeperator(); - } - - // end assert - p->popIndent(); - printSeperator(); - *p << ")"; - p->breakLineI(); -} - -ExprSMTLIBPrinter *createSMTLIBPrinter() { - if (ExprSMTLIBOptions::useLetExpressions) - return new ExprSMTLIBLetPrinter(); - else - return new ExprSMTLIBPrinter(); -} -} diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index bbb82d0d..fb7e270e 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -31,6 +31,19 @@ llvm::cl::opt<bool> humanReadableSMTLIB( llvm::cl::desc( "Enables generated SMT-LIBv2 files to be human readable (default=off)"), llvm::cl::init(false)); + +llvm::cl::opt<klee::ExprSMTLIBPrinter::AbbreviationMode> abbreviationMode( + "smtlib-abbreviation-mode", + llvm::cl::desc( + "Choose abbreviation mode to use in SMT-LIBv2 files (default=let)"), + llvm::cl::values(clEnumValN(klee::ExprSMTLIBPrinter::ABBR_NONE, "none", + "Do not abbreviate"), + clEnumValN(klee::ExprSMTLIBPrinter::ABBR_LET, "let", + "Abbreviate with let"), + clEnumValN(klee::ExprSMTLIBPrinter::ABBR_NAMED, "named", + "Abbreviate with :named annotations"), + clEnumValEnd), + llvm::cl::init(klee::ExprSMTLIBPrinter::ABBR_LET)); } namespace klee { @@ -41,6 +54,7 @@ ExprSMTLIBPrinter::ExprSMTLIBPrinter() humanReadable(ExprSMTLIBOptions::humanReadableSMTLIB), smtlibBoolOptions(), arraysToCallGetValueOn(NULL) { setConstantDisplayMode(ExprSMTLIBOptions::argConstantDisplayMode); + setAbbreviationMode(ExprSMTLIBOptions::abbreviationMode); } ExprSMTLIBPrinter::~ExprSMTLIBPrinter() { @@ -60,10 +74,11 @@ void ExprSMTLIBPrinter::setQuery(const Query &q) { query = &q; reset(); // clear the data structures scanAll(); - negateQueryExpression(); } void ExprSMTLIBPrinter::reset() { + bindings.clear(); + seenExprs.clear(); usedArrays.clear(); haveConstantArray = false; @@ -154,6 +169,41 @@ void ExprSMTLIBPrinter::printExpression( return; } + switch (abbrMode) { + case ABBR_NONE: + break; + + case ABBR_LET: { + BindingMap::iterator i = bindings.find(e); + if (i != bindings.end()) { + *p << "?B" << i->second; + return; + } + break; + } + + case ABBR_NAMED: { + BindingMap::iterator i = bindings.find(e); + if (i != bindings.end()) { + if (i->second > 0) { + *p << "(! "; + printFullExpression(e, expectedSort); + *p << " :named ?B" << i->second << ")"; + i->second = -i->second; + } else { + *p << "?B" << -i->second; + } + return; + } + break; + } + } + + printFullExpression(e, expectedSort); +} + +void ExprSMTLIBPrinter::printFullExpression( + const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort) { switch (e->getKind()) { case Expr::Constant: printConstant(cast<ConstantExpr>(e)); @@ -431,7 +481,7 @@ void ExprSMTLIBPrinter::generateOutput() { printSetLogic(); printArrayDeclarations(); printConstraints(); - printQuery(); + printQueryExpr(); printAction(); printExit(); } @@ -576,24 +626,32 @@ void ExprSMTLIBPrinter::scan(const ref<Expr> &e) { if (isa<ConstantExpr>(e)) return; // we don't need to scan simple constants - if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) { + if (seenExprs.insert(e).second) { + // We've not seen this expression before + + if (const ReadExpr *re = dyn_cast<ReadExpr>(e)) { - // Attempt to insert array and if array wasn't present before do more things - if (usedArrays.insert(re->updates.root).second) { + // Attempt to insert array and if array wasn't present before do more things + if (usedArrays.insert(re->updates.root).second) { - // check if the array is constant - if (re->updates.root->isConstantArray()) - haveConstantArray = true; + // check if the array is constant + if (re->updates.root->isConstantArray()) + haveConstantArray = true; - // scan the update list - scanUpdates(re->updates.head); + // scan the update list + scanUpdates(re->updates.head); + } } - } - // recurse into the children - Expr *ep = e.get(); - for (unsigned int i = 0; i < ep->getNumKids(); i++) - scan(ep->getKid(i)); + // recurse into the children + Expr *ep = e.get(); + for (unsigned int i = 0; i < ep->getNumKids(); i++) + scan(ep->getKid(i)); + } else { + // Add the expression to the binding map. The semantics of std::map::insert + // are such that it will not be inserted twice. + bindings.insert(std::make_pair(e, bindings.size()+1)); + } } void ExprSMTLIBPrinter::scanUpdates(const UpdateNode *un) { @@ -637,18 +695,52 @@ void ExprSMTLIBPrinter::printOptions() { } } -void ExprSMTLIBPrinter::printQuery() { - if (humanReadable) { - *p << "; Query from solver turned into an assert"; - p->breakLineI(); - } - +void ExprSMTLIBPrinter::printAssert(const ref<Expr> &e) { p->pushIndent(); *p << "(assert"; p->pushIndent(); printSeperator(); - printExpression(queryAssert, SORT_BOOL); + if (abbrMode == ABBR_LET && bindings.size() != 0) { + // Only print let expression if we have bindings to use. + *p << "(let"; + p->pushIndent(); + printSeperator(); + *p << "( "; + p->pushIndent(); + + // Disable abbreviations so none are used here. + abbrMode = ABBR_NONE; + + // Print each binding + for (BindingMap::const_iterator i = bindings.begin(); i != bindings.end(); + ++i) { + printSeperator(); + *p << "(?B" << i->second << " "; + p->pushIndent(); + + // We can abbreviate SORT_BOOL or SORT_BITVECTOR in let expressions + printExpression(i->first, getSort(i->first)); + + p->popIndent(); + printSeperator(); + *p << ")"; + } + + // Re-enable printing abbreviations. + abbrMode = ABBR_LET; + + p->popIndent(); + printSeperator(); + *p << ")"; + printSeperator(); + + printExpression(e, SORT_BOOL); + + *p << ")"; + } else { + printExpression(e, SORT_BOOL); + } p->popIndent(); printSeperator(); @@ -657,6 +749,15 @@ void ExprSMTLIBPrinter::printQuery() { p->breakLineI(); } +void ExprSMTLIBPrinter::printQueryExpr() { + if (humanReadable) { + *p << "; Query from solver turned into an assert"; + p->breakLineI(); + } + ref<Expr> queryAssert = Expr::createIsZero(query->expr); + printAssert(queryAssert); +} + ExprSMTLIBPrinter::SMTLIB_SORT ExprSMTLIBPrinter::getSort(const ref<Expr> &e) { switch (e->getKind()) { case Expr::NotOptimized: @@ -831,11 +932,6 @@ void ExprSMTLIBPrinter::printLogicalOrBitVectorExpr( *p << ")"; } -void ExprSMTLIBPrinter::negateQueryExpression() { - // Negating the query - queryAssert = Expr::createIsZero(query->expr); -} - bool ExprSMTLIBPrinter::setSMTLIBboolOption(SMTLIBboolOptions option, SMTLIBboolValues value) { std::pair<std::map<SMTLIBboolOptions, bool>::iterator, bool> thePair; |