diff options
Diffstat (limited to 'lib/Expr/ExprSMTLIBPrinter.cpp')
| -rw-r--r-- | lib/Expr/ExprSMTLIBPrinter.cpp | 348 |
1 files changed, 288 insertions, 60 deletions
diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index bbb82d0d..c4a6876e 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -8,8 +8,11 @@ //===----------------------------------------------------------------------===// #include "llvm/Support/Casting.h" #include "llvm/Support/CommandLine.h" +#include "llvm/Support/ErrorHandling.h" #include "klee/util/ExprSMTLIBPrinter.h" +#include <stack> + namespace ExprSMTLIBOptions { // Command line options llvm::cl::opt<klee::ExprSMTLIBPrinter::ConstantDisplayMode> @@ -31,6 +34,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 +57,7 @@ ExprSMTLIBPrinter::ExprSMTLIBPrinter() humanReadable(ExprSMTLIBOptions::humanReadableSMTLIB), smtlibBoolOptions(), arraysToCallGetValueOn(NULL) { setConstantDisplayMode(ExprSMTLIBOptions::argConstantDisplayMode); + setAbbreviationMode(ExprSMTLIBOptions::abbreviationMode); } ExprSMTLIBPrinter::~ExprSMTLIBPrinter() { @@ -60,10 +77,12 @@ void ExprSMTLIBPrinter::setQuery(const Query &q) { query = &q; reset(); // clear the data structures scanAll(); - negateQueryExpression(); } void ExprSMTLIBPrinter::reset() { + bindings.clear(); + orderedBindings.clear(); + seenExprs.clear(); usedArrays.clear(); haveConstantArray = false; @@ -141,8 +160,7 @@ void ExprSMTLIBPrinter::printConstant(const ref<ConstantExpr> &e) { break; default: - llvm::errs() << "ExprSMTLIBPrinter::printConstant() : Unexpected Constant " - "display mode\n"; + llvm_unreachable("Unexpected constant display mode"); } } @@ -154,6 +172,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)); @@ -188,7 +241,7 @@ void ExprSMTLIBPrinter::printExpression( case Expr::Eq: /* The "=" operator is special in that it can take any sort but we must - * enforce that both arguments are the same type. We do this a lazy way + * enforce that both arguments are the same sort. We do this in a lazy way * by enforcing the second argument is of the same type as the first. */ printSortArgsExpr(e, getSort(e->getKid(0))); @@ -201,8 +254,8 @@ void ExprSMTLIBPrinter::printExpression( case Expr::Not: /* These operators have a bitvector version and a bool version. * For these operators only (e.g. wouldn't apply to bvult) if the expected - * sort the - * expression is T then that implies the arguments are also of type T. + * sort of the expression is T then that implies the arguments are also of + * type T. */ printLogicalOrBitVectorExpr(e, expectedSort); @@ -254,7 +307,7 @@ void ExprSMTLIBPrinter::printExtractExpr(const ref<ExtractExpr> &e) { } void ExprSMTLIBPrinter::printCastExpr(const ref<CastExpr> &e) { - /* sign_extend and zero_extend behave slightly unusually in SMTLIBv2 + /* sign_extend and zero_extend behave slightly unusually in SMTLIBv2, * instead of specifying of what bit-width we would like to extend to * we specify how many bits to add to the child expression * @@ -376,7 +429,7 @@ const char *ExprSMTLIBPrinter::getSMTLIBKeyword(const ref<Expr> &e) { return "bvsge"; default: - return "<error>"; + llvm_unreachable("Conversion from Expr to SMTLIB keyword failed"); } } @@ -416,6 +469,10 @@ void ExprSMTLIBPrinter::scanAll() { // Scan the query too scan(query->expr); + + // Scan bindings for expression intra-dependencies + if (abbrMode == ABBR_LET) + scanBindingExprDeps(); } void ExprSMTLIBPrinter::generateOutput() { @@ -430,8 +487,12 @@ void ExprSMTLIBPrinter::generateOutput() { printOptions(); printSetLogic(); printArrayDeclarations(); - printConstraints(); - printQuery(); + + if (humanReadable) + printHumanReadableQuery(); + else + printMachineReadableQuery(); + printAction(); printExit(); } @@ -520,32 +581,57 @@ void ExprSMTLIBPrinter::printArrayDeclarations() { } } -void ExprSMTLIBPrinter::printConstraints() { - if (humanReadable) - *o << "; Constraints\n"; +void ExprSMTLIBPrinter::printHumanReadableQuery() { + assert(humanReadable && "method must be called in humanReadable mode"); + *o << "; Constraints\n"; - // Generate assert statements for each constraint - for (ConstraintManager::const_iterator i = query->constraints.begin(); - i != query->constraints.end(); i++) { - *p << "(assert "; - p->pushIndent(); - printSeperator(); + if (abbrMode != ABBR_LET) { + // Generate assert statements for each constraint + for (ConstraintManager::const_iterator i = query->constraints.begin(); + i != query->constraints.end(); i++) { + printAssert(*i); + } - // recurse into Expression - printExpression(*i, SORT_BOOL); + *o << "; QueryExpr\n"; - p->popIndent(); - printSeperator(); - *p << ")"; - p->breakLineI(); + // We negate the Query Expr because in KLEE queries are solved + // in terms of validity, but SMT-LIB works in terms of satisfiability + ref<Expr> queryAssert = Expr::createIsZero(query->expr); + printAssert(queryAssert); + } else { + // let bindings are only scoped within a single (assert ...) so + // the entire query must be printed within a single assert + *o << "; Constraints and QueryExpr\n"; + printQueryInSingleAssert(); } } +void ExprSMTLIBPrinter::printMachineReadableQuery() { + assert(!humanReadable && "method should not be called in humanReadable mode"); + printQueryInSingleAssert(); +} + + +void ExprSMTLIBPrinter::printQueryInSingleAssert() { + // We negate the Query Expr because in KLEE queries are solved + // in terms of validity, but SMT-LIB works in terms of satisfiability + ref<Expr> queryAssert = Expr::createIsZero(query->expr); + + // Print constraints inside the main query to reuse the Expr bindings + for (std::vector<ref<Expr> >::const_iterator i = query->constraints.begin(), + e = query->constraints.end(); + i != e; ++i) { + queryAssert = AndExpr::create(queryAssert, *i); + } + + // print just a single (assert ...) containing entire query + printAssert(queryAssert); +} void ExprSMTLIBPrinter::printAction() { // Ask solver to check for satisfiability *o << "(check-sat)\n"; - /* If we has arrays to find the values of then we'll + /* If we have arrays to find the values of then we'll * ask the solver for the value of each bitvector in each array */ if (arraysToCallGetValueOn != NULL && !arraysToCallGetValueOn->empty()) { @@ -567,33 +653,129 @@ void ExprSMTLIBPrinter::printAction() { } void ExprSMTLIBPrinter::scan(const ref<Expr> &e) { - if (e.isNull()) { - llvm::errs() << "ExprSMTLIBPrinter::scan() : Found NULL expression!" - << "\n"; - return; - } + assert(!(e.isNull()) && "found NULL expression"); 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) { + if (usedArrays.insert(re->updates.root).second) { + // Array was not recorded before - // 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)); + } 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)); } +} - // recurse into the children - Expr *ep = e.get(); - for (unsigned int i = 0; i < ep->getNumKids(); i++) - scan(ep->getKid(i)); +void ExprSMTLIBPrinter::scanBindingExprDeps() { + if (!bindings.size()) + return; + + // Mutual dependency storage + typedef std::map<const ref<Expr>, std::set<ref<Expr> > > ExprDepMap; + + // A map from binding Expr (need abbreviating) "e" to the set of binding Expr + // that are sub expressions of "e" (i.e. "e" uses these sub expressions). + // usesSubExprMap[a].count(b) == 1 means that binding Expr "a" uses + // sub Expr "b" (also a binding Expr). + // One can think of this map representing the "depends on" edges + // in a "dependency graph" where nodes are binding Expr roots + ExprDepMap usesSubExprMap; + + // A map from Binding Expr "e" to the set of binding Expr that use "e" + // subExprOfMap[a].count(b) == 1 means that binding Expr "a" is a sub Expr + // of binding Expr "b". + // One can think of this map as representing the edges in the previously + // mentioned "dependency graph" except the direction of the edges + // have been reversed + ExprDepMap subExprOfMap; + + // Working queue holding expressions with no dependencies + std::vector<ref<Expr> > nonDepBindings; + + // Iterate over bindings and collect dependencies + for (BindingMap::const_iterator it = bindings.begin(); + it != bindings.end(); ++it) { + std::stack<ref<Expr> > childQueue; + childQueue.push(it->first); + // Non-recursive expression parsing + while (childQueue.size()) { + Expr *ep = childQueue.top().get(); + childQueue.pop(); + for (unsigned i = 0; i < ep->getNumKids(); ++i) { + ref<Expr> e = ep->getKid(i); + if (isa<ConstantExpr>(e)) + continue; + // Are there any dependencies in the bindings? + if (bindings.count(e)) { + usesSubExprMap[it->first].insert(e); + subExprOfMap[e].insert(it->first); + } else { + childQueue.push(e); + } + } + } + // Store expressions with zero deps + if (!usesSubExprMap.count(it->first)) + nonDepBindings.push_back(it->first); + } + assert(nonDepBindings.size() && "there must be expr bindings with no deps"); + + // Unroll the dependency tree starting with zero-dep expressions + // and redefine bindings + unsigned counter = 1; + // nonDepBindings always holds expressions with no dependencies + while (nonDepBindings.size()) { + BindingMap levelExprs; + std::vector<ref<Expr> > tmp(nonDepBindings); + nonDepBindings.clear(); + for (std::vector<ref<Expr> >::const_iterator nonDepExprIt = tmp.begin(); + nonDepExprIt != tmp.end(); ++nonDepExprIt) { + // Save to the level expression bindings + levelExprs.insert(std::make_pair(*nonDepExprIt, counter++)); + // Who is dependent on me? + ExprDepMap::iterator depsIt = subExprOfMap.find(*nonDepExprIt); + if (depsIt != subExprOfMap.end()) { + for (std::set<ref<Expr> >::iterator exprIt = depsIt->second.begin(); + exprIt != depsIt->second.end(); ) { + // Erase dependency + ExprDepMap::iterator subExprIt = usesSubExprMap.find(*exprIt); + assert(subExprIt != usesSubExprMap.end()); + assert(subExprIt->second.count(*nonDepExprIt)); + subExprIt->second.erase(*nonDepExprIt); + // If the expression *exprIt does not have any + // dependencies anymore, add it to the queue + if (!subExprIt->second.size()) { + nonDepBindings.push_back(*exprIt); + depsIt->second.erase(exprIt++); + } else { + ++exprIt; + } + } + } + } + // Store level bindings + orderedBindings.push_back(levelExprs); + } } void ExprSMTLIBPrinter::scanUpdates(const UpdateNode *un) { @@ -637,18 +819,69 @@ 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 && orderedBindings.size() != 0) { + // Only print let expression if we have bindings to use. + *p << "(let"; + p->pushIndent(); + printSeperator(); + *p << "("; + p->pushIndent(); + + // Clear original bindings, we'll be using orderedBindings + // to print nested let expressions + bindings.clear(); + + // Print each binding on its level + for (unsigned i = 0; i < orderedBindings.size(); ++i) { + BindingMap levelBindings = orderedBindings[i]; + for (BindingMap::const_iterator j = levelBindings.begin(); + j != levelBindings.end(); ++j) { + printSeperator(); + *p << "(?B" << j->second; + p->pushIndent(); + printSeperator(); + + // We can abbreviate SORT_BOOL or SORT_BITVECTOR in let expressions + printExpression(j->first, getSort(j->first)); + + p->popIndent(); + printSeperator(); + *p << ")"; + } + p->popIndent(); + printSeperator(); + *p << ")"; + printSeperator(); + + // Add nested let expressions (if any) + if (i < orderedBindings.size()-1) { + *p << "(let"; + p->pushIndent(); + printSeperator(); + *p << "("; + p->pushIndent(); + } + // Insert current level bindings so that they can be used + // in the next level during expression printing + bindings.insert(levelBindings.begin(), levelBindings.end()); + } + + printExpression(e, SORT_BOOL); + + for (unsigned i = 0; i < orderedBindings.size(); ++i) { + p->popIndent(); + printSeperator(); + *p << ")"; + } + } else { + printExpression(e, SORT_BOOL); + } p->popIndent(); printSeperator(); @@ -713,9 +946,9 @@ void ExprSMTLIBPrinter::printCastToSort(const ref<Expr> &e, *p << ")"; break; case SORT_BOOL: { - /* We make the assumption (might be wrong) that any bitvector whos unsigned - *decimal value is - * is zero is interpreted as "false", otherwise it is true. + /* We make the assumption (might be wrong) that any bitvector whose unsigned + * decimal value is is zero is interpreted as "false", otherwise it is + * true. * * This may not be the interpretation we actually want! */ @@ -743,7 +976,7 @@ void ExprSMTLIBPrinter::printCastToSort(const ref<Expr> &e, } break; default: - assert(0 && "Unsupported cast!"); + llvm_unreachable("Unsupported cast"); } } @@ -814,7 +1047,7 @@ void ExprSMTLIBPrinter::printLogicalOrBitVectorExpr( *p << ((s == SORT_BITVECTOR) ? "bvxor" : "xor"); break; default: - *p << "ERROR"; // this shouldn't happen + llvm_unreachable("Conversion from Expr to SMTLIB keyword failed"); } *p << " "; @@ -831,11 +1064,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; |