diff options
author | Cristian Cadar <cristic@cs.stanford.edu> | 2012-10-24 13:10:25 +0000 |
---|---|---|
committer | Cristian Cadar <cristic@cs.stanford.edu> | 2012-10-24 13:10:25 +0000 |
commit | 07834bcfefa160dd78c8fe29f0ead71b33ab0817 (patch) | |
tree | 8463bc1412bb1d65113a0e96ae80f7c41154d6a1 | |
parent | 3cbfaee24c52c2e9a2070890e9f343fa06f4d0b8 (diff) | |
download | klee-07834bcfefa160dd78c8fe29f0ead71b33ab0817.tar.gz |
Nice patch by Dan Liew that adds support for printing queries in the
SMTLIB format (part of his MSc project work). git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@166556 91177308-0d34-0410-b5e6-96231b3b80d8
-rw-r--r-- | include/klee/util/ExprSMTLIBLetPrinter.h | 73 | ||||
-rw-r--r-- | include/klee/util/ExprSMTLIBPrinter.h | 296 | ||||
-rw-r--r-- | lib/Expr/ExprSMTLIBLetPrinter.cpp | 249 | ||||
-rw-r--r-- | lib/Expr/ExprSMTLIBPrinter.cpp | 906 |
4 files changed, 1524 insertions, 0 deletions
diff --git a/include/klee/util/ExprSMTLIBLetPrinter.h b/include/klee/util/ExprSMTLIBLetPrinter.h new file mode 100644 index 00000000..56c8f008 --- /dev/null +++ b/include/klee/util/ExprSMTLIBLetPrinter.h @@ -0,0 +1,73 @@ +//===-- ExprSMTLIBLetPrinter.h ------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#include "ExprSMTLIBPrinter.h" +#ifndef EXPRSMTLETPRINTER_H_ +#define EXPRSMTLETPRINTER_H_ + +namespace klee +{ + /// This printer behaves like ExprSMTLIBPrinter except that it will abbreviate expressions + /// using the (let) SMT-LIBv2 command. Expression trees that appear two or more times in the Query + /// passed to setQuery() will be abbreviated. + /// + /// This class should be used just like ExprSMTLIBPrinter. + class ExprSMTLIBLetPrinter : public ExprSMTLIBPrinter + { + public: + ExprSMTLIBLetPrinter(); + virtual ~ExprSMTLIBLetPrinter() { } + virtual void generateOutput(); + protected: + virtual void scan(const ref<Expr>& e); + virtual void reset(); + virtual void generateBindings(); + void printExpression(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort); + void printLetExpression(); + + private: + ///Let expression binding number map. + std::map<const ref<Expr>,unsigned int> bindings; + + /* These are effectively expression counters. + * firstEO - first Occurrence of expression contains + * all expressions that occur once. It is + * only used to help us fill twoOrMoreOE + * + * twoOrMoreEO - Contains occur all expressions that + * that occur two or more times. These + * are the expressions that will be + * abbreviated by using (let () ()) expressions. + * + * + * + */ + std::set<ref<Expr> > firstEO, twoOrMoreEO; + + ///This is the prefix string used for all abbreviations in (let) expressions. + static const char BINDING_PREFIX[]; + + /* This is needed during un-abbreviated printing. + * Because we have overloaded printExpression() + * the parent will call it and will abbreviate + * when we don't want it to. This bool allows us + * to switch it on/off easily. + */ + bool disablePrintedAbbreviations; + + + + }; + + ///Create a SMT-LIBv2 printer based on command line options + ///The caller is responsible for deleting the printer + ExprSMTLIBPrinter* createSMTLIBPrinter(); +} + +#endif /* EXPRSMTLETPRINTER_H_ */ diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h new file mode 100644 index 00000000..588d9d19 --- /dev/null +++ b/include/klee/util/ExprSMTLIBPrinter.h @@ -0,0 +1,296 @@ +//===-- ExprSMTLIBPrinter.h ------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_EXPRSMTLIBPRINTER_H +#define KLEE_EXPRSMTLIBPRINTER_H + +#include <ostream> +#include <string> +#include <set> +#include <map> +#include <klee/Constraints.h> +#include <klee/Expr.h> +#include <klee/util/PrintContext.h> +#include <klee/Solver.h> + +namespace klee { + + ///Base Class for SMTLIBv2 printer for Expr trees. It uses the QF_ABV logic. Note however the logic can be + ///set to QF_AUFBV because some solvers (e.g. STP) complain if this logic is set to QF_ABV. + /// + ///This printer does not abbreviate expressions. The printer ExprSMTLIBLetPrinter does though. + /// + /// It is intended to be used as follows + /// -# Create instance of this class + /// -# Set output ( setOutput() ) + /// -# Set query to print ( setQuery() ) + /// -# Set options using the methods prefixed with the word "set". + /// -# Call generateOutput() + /// + /// The class can then be used again on another query ( setQuery() ). + /// The options set are persistent across queries (apart from setArrayValuesToGet() and PRODUCE_MODELS) + class ExprSMTLIBPrinter + { + public: + + ///Different SMTLIBv2 logics supported by this class + /// \sa setLogic() + enum SMTLIBv2Logic + { + QF_ABV, ///< Logic using Theory of Arrays and Theory of Bitvectors + QF_AUFBV ///< Logic using Theory of Arrays and Theory of Bitvectors and has uninterpreted functions + }; + + ///Different SMTLIBv2 options that have a boolean value that can be set + /// \sa setSMTLIBboolOption + enum SMTLIBboolOptions + { + PRINT_SUCCESS, ///< print-success SMTLIBv2 option + PRODUCE_MODELS,///< produce-models SMTLIBv2 option + INTERACTIVE_MODE ///< interactive-mode SMTLIBv2 option + }; + + ///Different SMTLIBv2 bool option values + /// \sa setSMTLIBboolOption + enum SMTLIBboolValues + { + OPTION_TRUE, ///< Set option to true + OPTION_FALSE, ///< Set option to false + OPTION_DEFAULT ///< Use solver's defaults (the option will not be set in output) + }; + + enum ConstantDisplayMode + { + BINARY,///< Display bit vector constants in binary e.g. #b00101101 + HEX, ///< Display bit vector constants in Hexidecimal e.g.#x2D + DECIMAL ///< Display bit vector constants in Decimal e.g. (_ bv45 8) + }; + + ///Different supported SMTLIBv2 sorts (a.k.a type) in QF_AUFBV + enum SMTLIB_SORT + { + SORT_BITVECTOR, + SORT_BOOL + }; + + + + ///Allows the way Constant bitvectors are printed to be changed. + ///This setting is persistent across queries. + /// \return true if setting the mode was successful + bool setConstantDisplayMode(ConstantDisplayMode cdm); + + ConstantDisplayMode getConstantDisplayMode() { return cdm;} + + ///Create a new printer that will print a query in the SMTLIBv2 language. + ExprSMTLIBPrinter(); + + ///Set the output stream that will be printed to. + ///This call is persistent across queries. + void setOutput(std::ostream& output); + + ///Set the query to print. This will setArrayValuesToGet() + ///to none (i.e. no array values will be requested using + ///the SMTLIBv2 (get-value ()) command). + void setQuery(const Query& q); + + virtual ~ExprSMTLIBPrinter(); + + /// Print the query to the std::ostream + /// setOutput() and setQuery() must be called before calling this. + /// + /// All options should be set before calling this. + /// \sa setConstantDisplayMode + /// \sa setLogic() + /// \sa setHumanReadable + /// \sa setSMTLIBboolOption + /// \sa setArrayValuesToGet + /// + /// Mostly it does not matter what order the options are set in. However calling + /// setArrayValuesToGet() implies PRODUCE_MODELS is set so, if a call to setSMTLIBboolOption() + /// is made that uses the PRODUCE_MODELS before calling setArrayValuesToGet() then the setSMTLIBboolOption() + /// call will be ineffective. + virtual void generateOutput(); + + ///Set which SMTLIBv2 logic to use. + ///This only affects what logic is used in the (set-logic <logic>) command. + ///The rest of the printed SMTLIBv2 commands are the same regardless of the logic used. + /// + /// \return true if setting logic was successful. + bool setLogic(SMTLIBv2Logic l); + + ///Sets how readable the printed SMTLIBv2 commands are. + /// \param hr If set to true the printed commands are made more human readable. + /// + /// The printed commands are made human readable by... + /// - Indenting and line breaking. + /// - Adding comments + void setHumanReadable(bool hr); + + ///Set SMTLIB options. + /// These options will be printed when generateOutput() is called via + /// the SMTLIBv2 command (set-option :option-name <value>) + /// + /// By default no options will be printed so the SMTLIBv2 solver will use + /// its default values for all options. + /// + /// \return true if option was successfully set. + /// + /// The options set are persistent across calls to setQuery() apart from the + /// PRODUCE_MODELS option which this printer may automatically set/unset. + bool setSMTLIBboolOption(SMTLIBboolOptions option, SMTLIBboolValues value); + + /// Set the array names that the SMTLIBv2 solver will be asked to determine. + /// Calling this method implies the PRODUCE_MODELS option is true and will change + /// any previously set value. + /// + /// If no call is made to this function before ExprSMTLIBPrinter::generateOutput() then + /// the solver will only be asked to check satisfiability. + /// + /// If the passed vector is not empty then the values of those arrays will be requested + /// via (get-value ()) SMTLIBv2 command in the output stream in the same order as vector. + void setArrayValuesToGet(const std::vector<const Array*>& a); + + /// \return True if human readable mode is switched on + bool isHumanReadable(); + + + protected: + ///Contains the arrays found during scans + std::set<const Array*> usedArrays; + + ///Output stream to write to + std::ostream* o; + + ///The query to print + const Query* query; + + ///Determine the SMTLIBv2 sort of the expression + SMTLIB_SORT getSort(const ref<Expr>& e); + + ///Print an expression but cast it to a particular SMTLIBv2 sort first. + void printCastToSort(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT sort); + + //Resets various internal objects for a new query + virtual void reset(); + + //Scan all constraints and the query + virtual void scanAll(); + + //Print an initial SMTLIBv2 comment before anything else is printed + virtual void printNotice(); + + //Print SMTLIBv2 options e.g. (set-option :option-name <value>) command + virtual void printOptions(); + + //Print SMTLIBv2 logic to use e.g. (set-logic QF_ABV) + virtual void printSetLogic(); + + //Print SMTLIBv2 assertions for constant arrays + virtual void printArrayDeclarations(); + + //Print SMTLIBv2 for all constraints in the query + virtual void printConstraints(); + + //Print SMTLIBv2 assert statement for the "mangled" query + virtual void printQuery(); + + ///Print the SMTLIBv2 command to check satisfiability and also optionally request for values + /// \sa setArrayValuesToGet() + virtual void printAction(); + + ///Print the SMTLIBv2 command to exit + virtual void printExit(); + + ///Print a Constant in the format specified by the current "Constant Display Mode" + void printConstant(const ref<ConstantExpr>& e); + + ///Recursively print expression + /// \param e is the expression to print + /// \param expectedSort is the sort we want. If "e" is not of the right type a cast will be performed. + virtual void printExpression(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort); + + ///Scan Expression recursively for Arrays in expressions. Found arrays are added to + /// the usedArrays vector. + virtual void scan(const ref<Expr>& e); + + /* Rules of recursion for "Special Expression handlers" and printSortArgsExpr() + * + * 1. The parent of the recursion will have created an indent level for you so you don't need to add another initially. + * 2. You do not need to add a line break (via printSeperator() ) at the end, the parent caller will handle that. + * 3. The effect of a single recursive call should not affect the depth of the indent stack (nor the contents + * of the indent stack prior to the call). I.e. After executing a single recursive call the indent stack + * should have the same size and contents as before executing the recursive call. + */ + + //Special Expression handlers + virtual void printReadExpr(const ref<ReadExpr>& e); + virtual void printExtractExpr(const ref<ExtractExpr>& e); + virtual void printCastExpr(const ref<CastExpr>& e); + virtual void printNotEqualExpr(const ref<NeExpr>& e); + virtual void printSelectExpr(const ref<SelectExpr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s); + + //For the set of operators that take sort "s" arguments + virtual void printSortArgsExpr(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s); + + ///For the set of operators that come in two sorts (e.g. (and () ()) (bvand () ()) ) + ///These are and,xor,or,not + /// \param e the Expression to print + /// \param s the sort of the expression we want + virtual void printLogicalOrBitVectorExpr(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s); + + ///Recursively prints updatesNodes + virtual void printUpdatesAndArray(const UpdateNode* un, const Array* root); + + ///This method does the translation between Expr classes and SMTLIBv2 keywords + /// \return A C-string of the SMTLIBv2 keyword + virtual const char* getSMTLIBKeyword(const ref<Expr>& e); + + virtual void printSeperator(); + + ///Helper function for scan() that scans the expressions of an update node + virtual void scanUpdates(const UpdateNode* un); + + ///Helper printer class + PrintContext* p; + + ///This contains the query from the solver but negated for our purposes. + /// \sa mangleQuery() + ref<Expr> queryAssert; + + ///Indicates if there were any constant arrays founds during a scan() + bool haveConstantArray; + + + private: + SMTLIBv2Logic logicToUse; + + volatile bool humanReadable; + + //Map of enabled SMTLIB Options + std::map<SMTLIBboolOptions,bool> smtlibBoolOptions; + + ///This sets queryAssert to be the boolean negation of the original Query + void mangleQuery(); + + //Print a SMTLIBv2 option as a C-string + const char* getSMTLIBOptionString(ExprSMTLIBPrinter::SMTLIBboolOptions option); + + //Pointer to a vector of Arrays. These will be used for the (get-value () ) call. + const std::vector<const Array*> * arraysToCallGetValueOn; + + ConstantDisplayMode cdm; + + }; + + + +} + +#endif diff --git a/lib/Expr/ExprSMTLIBLetPrinter.cpp b/lib/Expr/ExprSMTLIBLetPrinter.cpp new file mode 100644 index 00000000..7225704e --- /dev/null +++ b/lib/Expr/ExprSMTLIBLetPrinter.cpp @@ -0,0 +1,249 @@ +//===-- 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 <iostream> +#include "llvm/Support/CommandLine.h" +#include "klee/util/ExprSMTLIBLetPrinter.h" + +using namespace std; + +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) + { + std::cerr << "Can't print SMTLIBv2. Output or query bad!" << std::endl; + 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(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) + { + 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(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; + 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 new file mode 100644 index 00000000..aa75629a --- /dev/null +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -0,0 +1,906 @@ +//===-- ExprSMTLIBPrinter.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 <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> 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) + + + ); + + 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) + + + ); + +} + + +namespace klee +{ + + ExprSMTLIBPrinter::ExprSMTLIBPrinter() : + usedArrays(), o(NULL), query(NULL), p(NULL), haveConstantArray(false), logicToUse(QF_AUFBV), + humanReadable(ExprSMTLIBOptions::humanReadableSMTLIB), smtlibBoolOptions(), arraysToCallGetValueOn(NULL) + { + setConstantDisplayMode(ExprSMTLIBOptions::argConstantDisplayMode); + } + + ExprSMTLIBPrinter::~ExprSMTLIBPrinter() + { + if(p!=NULL) + delete p; + } + + void ExprSMTLIBPrinter::setOutput(std::ostream& output) + { + o = &output; + if(p!=NULL) + delete p; + + p = new PrintContext(output); + } + + void ExprSMTLIBPrinter::setQuery(const Query& q) + { + query = &q; + reset(); // clear the data structures + scanAll(); + mangleQuery(); + } + + void ExprSMTLIBPrinter::reset() + { + usedArrays.clear(); + haveConstantArray=false; + + /* Clear the PRODUCE_MODELS option if it was automatically set. + * We need to do this because the next query might not need the + * (get-value) SMT-LIBv2 command. + */ + if(arraysToCallGetValueOn !=NULL) + setSMTLIBboolOption(PRODUCE_MODELS,OPTION_DEFAULT); + + arraysToCallGetValueOn=NULL; + + + } + + bool ExprSMTLIBPrinter::isHumanReadable() + { + return humanReadable; + } + + bool ExprSMTLIBPrinter::setConstantDisplayMode(ConstantDisplayMode cdm) + { + if(cdm > DECIMAL) + return false; + + this->cdm = cdm; + return true; + } + + void ExprSMTLIBPrinter::printConstant(const ref<ConstantExpr>& e) + { + /* Handle simple boolean constants */ + + if(e->isTrue()) + { + *p << "true"; + return; + } + + if(e->isFalse()) + { + *p << "false"; + return; + } + + /* Handle bitvector constants */ + + std::string value; + + /* SMTLIBv2 deduces the bit-width (should be 8-bits in our case) + * from the length of the string (e.g. zero is #b00000000). LLVM + * doesn't know about this so we need to pad the printed output + * with the appropriate number of zeros (zeroPad) + */ + unsigned int zeroPad=0; + + switch(cdm) + { + case BINARY: + e->toString(value,2); + *p << "#b"; + + zeroPad = e->getWidth() - value.length(); + + for(unsigned int count=0; count < zeroPad; count++) + *p << "0"; + + *p << value ; + break; + + case HEX: + e->toString(value,16); + *p << "#x"; + + zeroPad = (e->getWidth() / 4) - value.length(); + for(unsigned int count=0; count < zeroPad; count++) + *p << "0"; + + *p << value ; + break; + + case DECIMAL: + e->toString(value,10); + *p << "(_ bv" << value<< " " << e->getWidth() << ")"; + break; + + default: + std::cerr << "ExprSMTLIBPrinter::printConstant() : Unexpected Constant display mode" << std::endl; + } + } + + void ExprSMTLIBPrinter::printExpression(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT expectedSort) + { + //check if casting might be necessary + if(getSort(e) != expectedSort) + { + printCastToSort(e,expectedSort); + return; + } + + + switch(e->getKind()) + { + case Expr::Constant: + printConstant(cast<ConstantExpr>(e)); + return; //base case + + case Expr::NotOptimized: + //skip to child + printExpression(e->getKid(0),expectedSort); + return; + + case Expr::Read: + printReadExpr(cast<ReadExpr>(e)); + return; + + case Expr::Extract: + printExtractExpr(cast<ExtractExpr>(e)); + return; + + case Expr::SExt: + case Expr::ZExt: + printCastExpr(cast<CastExpr>(e)); + return; + + case Expr::Ne: + printNotEqualExpr(cast<NeExpr>(e)); + return; + + case Expr::Select: + //the if-then-else expression. + printSelectExpr(cast<SelectExpr>(e),expectedSort); + return; + + 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 + * by enforcing the second argument is of the same type as the first. + */ + printSortArgsExpr(e,getSort(e->getKid(0))); + + return; + + case Expr::And: + case Expr::Or: + case Expr::Xor: + 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. + */ + printLogicalOrBitVectorExpr(e,expectedSort); + + return; + + + default: + /* The remaining operators (Add,Sub...,Ult,Ule,..) + * Expect SORT_BITVECTOR arguments + */ + printSortArgsExpr(e,SORT_BITVECTOR); + return; + } + } + + void ExprSMTLIBPrinter::printReadExpr(const ref<ReadExpr>& e) + { + *p << "(" << getSMTLIBKeyword(e) << " "; + p->pushIndent(); + + printSeperator(); + + //print array with updates recursively + printUpdatesAndArray(e->updates.head,e->updates.root); + + //print index + printSeperator(); + printExpression(e->index,SORT_BITVECTOR); + + p->popIndent(); + printSeperator(); + *p << ")"; + } + + void ExprSMTLIBPrinter::printExtractExpr(const ref<ExtractExpr>& e) + { + unsigned int lowIndex= e->offset; + unsigned int highIndex= lowIndex + e->width -1; + + *p << "((_ " << getSMTLIBKeyword(e) << " " << highIndex << " " << lowIndex << ") "; + + p->pushIndent(); //add indent for recursive call + printSeperator(); + + //recurse + printExpression(e->getKid(0),SORT_BITVECTOR); + + p->popIndent(); //pop indent added for the recursive call + printSeperator(); + *p << ")"; + } + + void ExprSMTLIBPrinter::printCastExpr(const ref<CastExpr>& e) + { + /* 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 + * + * e.g + * ((_ sign_extend 64) (_ bv5 32)) + * + * gives a (_ BitVec 96) instead of (_ BitVec 64) + * + * So we must work out how many bits we need to add. + * + * (e->width) is the desired number of bits + * (e->src->getWidth()) is the number of bits in the child + */ + unsigned int numExtraBits= (e->width) - (e->src->getWidth()); + + *p << "((_ " << getSMTLIBKeyword(e) << " " << + numExtraBits << ") "; + + p->pushIndent(); //add indent for recursive call + printSeperator(); + + //recurse + printExpression(e->src,SORT_BITVECTOR); + + p->popIndent(); //pop indent added for recursive call + printSeperator(); + + *p << ")"; + } + + void ExprSMTLIBPrinter::printNotEqualExpr(const ref<NeExpr>& e) + { + *p << "(not ("; + p->pushIndent(); + *p << "=" << " "; + p->pushIndent(); + printSeperator(); + + /* The "=" operators allows both sorts. We assume + * that the second argument sort should be forced to be the same sort as the + * first argument + */ + SMTLIB_SORT s = getSort(e->getKid(0)); + + printExpression(e->getKid(0),s); + printSeperator(); + printExpression(e->getKid(1),s); + p->popIndent(); + printSeperator(); + + *p << ")"; + p->popIndent(); + printSeperator(); + *p << ")"; + } + + + const char* ExprSMTLIBPrinter::getSMTLIBKeyword(const ref<Expr>& e) + { + + switch(e->getKind()) + { + case Expr::Read: return "select"; + case Expr::Select: return "ite"; + case Expr::Concat: return "concat"; + case Expr::Extract: return "extract"; + case Expr::ZExt: return "zero_extend"; + case Expr::SExt: return "sign_extend"; + + case Expr::Add: return "bvadd"; + case Expr::Sub: return "bvsub"; + case Expr::Mul: return "bvmul"; + case Expr::UDiv: return "bvudiv"; + case Expr::SDiv: return "bvsdiv"; + case Expr::URem: return "bvurem"; + case Expr::SRem: return "bvsrem"; + + + /* And, Xor, Not and Or are not handled here because there different versions + * for different sorts. See printLogicalOrBitVectorExpr() + */ + + + case Expr::Shl: return "bvshl"; + case Expr::LShr: return "bvlshr"; + case Expr::AShr: return "bvashr"; + + case Expr::Eq: return "="; + + //Not Equal does not exist directly in SMTLIBv2 + + case Expr::Ult: return "bvult"; + case Expr::Ule: return "bvule"; + case Expr::Ugt: return "bvugt"; + case Expr::Uge: return "bvuge"; + + case Expr::Slt: return "bvslt"; + case Expr::Sle: return "bvsle"; + case Expr::Sgt: return "bvsgt"; + case Expr::Sge: return "bvsge"; + + default: + return "<error>"; + + } + } + + void ExprSMTLIBPrinter::printUpdatesAndArray(const UpdateNode* un, const Array* root) + { + if(un!=NULL) + { + *p << "(store "; + p->pushIndent(); + printSeperator(); + + //recurse to get the array or update that this store operations applies to + printUpdatesAndArray(un->next,root); + + printSeperator(); + + //print index + printExpression(un->index,SORT_BITVECTOR); + printSeperator(); + + //print value that is assigned to this index of the array + printExpression(un->value,SORT_BITVECTOR); + + p->popIndent(); + printSeperator(); + *p << ")"; + } + else + { + //The base case of the recursion + *p << root->name; + } + + } + + void ExprSMTLIBPrinter::scanAll() + { + //perform scan of all expressions + for(ConstraintManager::const_iterator i= query->constraints.begin(); i != query->constraints.end(); i++) + scan(*i); + + //Scan the query too + scan(query->expr); + } + + void ExprSMTLIBPrinter::generateOutput() + { + if(p==NULL || query == NULL || o ==NULL) + { + std::cerr << "ExprSMTLIBPrinter::generateOutput() Can't print SMTLIBv2. Output or query bad!" << std::endl; + return; + } + + if(humanReadable) printNotice(); + printOptions(); + printSetLogic(); + printArrayDeclarations(); + printConstraints(); + printQuery(); + printAction(); + printExit(); + } + + void ExprSMTLIBPrinter::printSetLogic() + { + *o << "(set-logic "; + switch(logicToUse) + { + case QF_ABV: *o << "QF_ABV"; break; + case QF_AUFBV: *o << "QF_AUFBV" ; break; + } + *o << " )" << std::endl; + } + + + void ExprSMTLIBPrinter::printArrayDeclarations() + { + //Assume scan() has been called + if(humanReadable) + *o << "; Array declarations" << endl; + + //declare arrays + for(set<const Array*>::iterator it = usedArrays.begin(); it != usedArrays.end(); it++) + { + *o << "(declare-fun " << (*it)->name << " () " + "(Array (_ BitVec " << (*it)->getDomain() << ") " + "(_ BitVec " << (*it)->getRange() << ") ) )" << endl; + } + + //Set array values for constant values + if(haveConstantArray) + { + if(humanReadable) + *o << "; Constant Array Definitions" << endl; + + const Array* array; + + //loop over found arrays + for(set<const Array*>::iterator it = usedArrays.begin(); it != usedArrays.end(); it++) + { + array= *it; + int byteIndex=0; + if(array->isConstantArray()) + { + /*loop over elements in the array and generate an assert statement + for each one + */ + for(vector< ref<ConstantExpr> >::const_iterator ce= array->constantValues.begin(); + ce != array->constantValues.end(); ce++, byteIndex++) + { + *p << "(assert ("; + p->pushIndent(); + *p << "= "; + p->pushIndent(); + printSeperator(); + + *p << "(select " << array->name << " (_ bv" << byteIndex << " " << array->getDomain() << ") )"; + printSeperator(); + printConstant((*ce)); + + p->popIndent(); + printSeperator(); + *p << ")"; + p->popIndent(); + printSeperator(); + *p << ")"; + + p->breakLineI(); + + } + } + } + } + } + + void ExprSMTLIBPrinter::printConstraints() + { + if(humanReadable) + *o << "; Constraints" << endl; + + //Generate assert statements for each constraint + for(ConstraintManager::const_iterator i= query->constraints.begin(); i != query->constraints.end(); i++) + { + *p << "(assert "; + p->pushIndent(); + printSeperator(); + + //recurse into Expression + printExpression(*i,SORT_BOOL); + + p->popIndent(); + printSeperator(); + *p << ")"; p->breakLineI(); + } + + } + + void ExprSMTLIBPrinter::printAction() + { + //Ask solver to check for satisfiability + *o << "(check-sat)" << endl; + + /* If we has 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()) + { + + const Array* theArray=0; + + //loop over the array names + for(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; + } + + } + + + } + } + + void ExprSMTLIBPrinter::scan(const ref<Expr>& e) + { + if(e.isNull()) + { + std::cerr << "ExprSMTLIBPrinter::scan() : Found NULL expression!" << std::endl; + return; + } + + if(isa<ConstantExpr>(e)) + return; //we don't need to scan simple constants + + 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)); + } + + + void ExprSMTLIBPrinter::scanUpdates(const UpdateNode* un) + { + while(un != NULL) + { + scan(un->index); + scan(un->value); + un= un->next; + } + } + + + void ExprSMTLIBPrinter::printExit() + { + *o << "(exit)" << endl; + } + + bool ExprSMTLIBPrinter::setLogic(SMTLIBv2Logic l) + { + if(l > QF_AUFBV) + return false; + + logicToUse=l; + return true; + } + + void ExprSMTLIBPrinter::printSeperator() + { + if(humanReadable) + p->breakLineI(); + else + p->write(" "); + } + + void ExprSMTLIBPrinter::printNotice() + { + *o << "; This file conforms to SMTLIBv2 and was generated by KLEE" << endl; + } + + void ExprSMTLIBPrinter::setHumanReadable(bool hr) + { + humanReadable=hr; + } + + void ExprSMTLIBPrinter::printOptions() + { + //Print out SMTLIBv2 boolean options + for(std::map<SMTLIBboolOptions,bool>::const_iterator i= smtlibBoolOptions.begin(); i!= smtlibBoolOptions.end(); i++) + { + *o << "(set-option :" << getSMTLIBOptionString(i->first) << + " " << ((i->second)?"true":"false") << ")" << endl; + } + } + + void ExprSMTLIBPrinter::printQuery() + { + if(humanReadable) + { + *p << "; Query from solver turned into an assert"; + p->breakLineI(); + } + + p->pushIndent(); + *p << "(assert"; + p->pushIndent(); + printSeperator(); + + printExpression(queryAssert,SORT_BOOL); + + p->popIndent(); + printSeperator(); + *p << ")"; + p->popIndent(); + p->breakLineI(); + } + + ExprSMTLIBPrinter::SMTLIB_SORT ExprSMTLIBPrinter::getSort(const ref<Expr>& e) + { + /* We could handle every operator in a large switch statement, + * but this seems more elegant. + */ + + 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 + */ + return SORT_BITVECTOR; + } + else + return (e->getWidth() == Expr::Bool)?(SORT_BOOL):(SORT_BITVECTOR); + } + + void ExprSMTLIBPrinter::printCastToSort(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT sort) + { + switch(sort) + { + case SORT_BITVECTOR: + if(humanReadable) + { + p->breakLineI(); *p << ";Performing implicit bool to bitvector cast"; p->breakLine(); + } + //We assume the e is a bool that we need to cast to a bitvector sort. + *p << "(ite"; p->pushIndent(); printSeperator(); + printExpression(e,SORT_BOOL); printSeperator(); + *p << "(_ bv1 1)" ; printSeperator(); //printing the "true" bitvector + *p << "(_ bv0 1)" ; p->popIndent(); printSeperator(); //printing the "false" bitvector + *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. + * + * This may not be the interpretation we actually want! + */ + Expr::Width bitWidth=e->getWidth(); + if(humanReadable) + { + p->breakLineI(); *p << ";Performing implicit bitvector to bool cast"; p->breakLine(); + } + *p << "(bvugt"; p->pushIndent(); printSeperator(); + // We assume is e is a bitvector + printExpression(e,SORT_BITVECTOR); printSeperator(); + *p << "(_ bv0 " << bitWidth << ")"; p->popIndent(); printSeperator(); //Zero bitvector of required width + *p << ")"; + + if(bitWidth!=Expr::Bool) + std::cerr << "ExprSMTLIBPrinter : Warning. Casting a bitvector (length " << bitWidth << ") to bool!" << std::endl; + + } + break; + default: + assert(0 && "Unsupported cast!"); + } + } + + void ExprSMTLIBPrinter::printSelectExpr(const ref<SelectExpr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s) + { + //This is the if-then-else expression + + *p << "(" << getSMTLIBKeyword(e) << " "; + p->pushIndent(); //add indent for recursive call + + //The condition + printSeperator(); + printExpression(e->getKid(0),SORT_BOOL); + + /* This operator is special in that the remaining children + * can be of any sort. + */ + + //if true + printSeperator(); + printExpression(e->getKid(1),s); + + //if false + printSeperator(); + printExpression(e->getKid(2),s); + + + p->popIndent(); //pop indent added for recursive call + printSeperator(); + *p << ")"; + } + + void ExprSMTLIBPrinter::printSortArgsExpr(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s) + { + *p << "(" << getSMTLIBKeyword(e) << " "; + p->pushIndent(); //add indent for recursive call + + //loop over children and recurse into each expecting they are of sort "s" + for(unsigned int i=0; i < e->getNumKids(); i++) + { + printSeperator(); + printExpression(e->getKid(i),s); + } + + p->popIndent(); //pop indent added for recursive call + printSeperator(); + *p << ")"; + } + + void ExprSMTLIBPrinter::printLogicalOrBitVectorExpr(const ref<Expr>& e, ExprSMTLIBPrinter::SMTLIB_SORT s) + { + /* For these operators it is the case that the expected sort is the same as the sorts + * of the arguments. + */ + + *p << "("; + switch(e->getKind()) + { + case Expr::And: + *p << ((s==SORT_BITVECTOR)?"bvand":"and"); + break; + case Expr::Not: + *p << ((s==SORT_BITVECTOR)?"bvnot":"not"); + break; + case Expr::Or: + *p << ((s==SORT_BITVECTOR)?"bvor":"or"); + break; + + case Expr::Xor: + *p << ((s==SORT_BITVECTOR)?"bvxor":"xor"); + break; + default: + *p << "ERROR"; // this shouldn't happen + } + *p << " "; + + p->pushIndent(); //add indent for recursive call + + //loop over children and recurse into each expecting they are of sort "s" + for(unsigned int i=0; i < e->getNumKids(); i++) + { + printSeperator(); + printExpression(e->getKid(i),s); + } + + p->popIndent(); //pop indent added for recursive call + printSeperator(); + *p << ")"; + } + + void ExprSMTLIBPrinter::mangleQuery() + { + //Negating the query + queryAssert = Expr::createIsZero(query->expr); + } + + bool ExprSMTLIBPrinter::setSMTLIBboolOption(SMTLIBboolOptions option, SMTLIBboolValues value) + { + std::pair< std::map<SMTLIBboolOptions,bool>::iterator, bool> thePair; + bool theValue= (value==OPTION_TRUE)?true:false; + + switch(option) + { + case PRINT_SUCCESS: + case PRODUCE_MODELS: + case INTERACTIVE_MODE: + thePair=smtlibBoolOptions.insert(std::pair<SMTLIBboolOptions,bool>(option,theValue)); + + if(value== OPTION_DEFAULT) + { + //we should unset (by removing from map) this option so the solver uses its default + smtlibBoolOptions.erase(thePair.first); + return true; + } + + if(!thePair.second) + { + //option was already present so modify instead. + thePair.first->second=value; + } + return true; + default: + return false; + + } + } + + void ExprSMTLIBPrinter::setArrayValuesToGet(const std::vector<const Array*>& a) + { + arraysToCallGetValueOn = &a; + + //This option must be set in order to use the SMTLIBv2 command (get-value () ) + if(!a.empty()) + setSMTLIBboolOption(PRODUCE_MODELS,OPTION_TRUE); + + /* There is a risk that users will ask about array values that aren't + * even in the query. We should add them to the usedArrays list and hope + * 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) + { + usedArrays.insert(*i); + } + + } + +const char* ExprSMTLIBPrinter::getSMTLIBOptionString(ExprSMTLIBPrinter::SMTLIBboolOptions option) +{ + switch(option) + { + case PRINT_SUCCESS: return "print-success"; + case PRODUCE_MODELS: return "produce-models"; + case INTERACTIVE_MODE: return "interactive-mode"; + default: + return "unknown-option"; + } +} + +} + + + |