diff options
| -rw-r--r-- | include/klee/util/ExprSMTLIBLetPrinter.h | 104 | ||||
| -rw-r--r-- | include/klee/util/ExprSMTLIBPrinter.h | 587 | ||||
| -rw-r--r-- | lib/Expr/ExprSMTLIBLetPrinter.cpp | 442 | ||||
| -rw-r--r-- | lib/Expr/ExprSMTLIBPrinter.cpp | 1711 | ||||
| -rw-r--r-- | test/Expr/print-smt.smt2.good | 22 |
5 files changed, 1429 insertions, 1437 deletions
diff --git a/include/klee/util/ExprSMTLIBLetPrinter.h b/include/klee/util/ExprSMTLIBLetPrinter.h index 56c8f008..dd97e0d5 100644 --- a/include/klee/util/ExprSMTLIBLetPrinter.h +++ b/include/klee/util/ExprSMTLIBLetPrinter.h @@ -1,4 +1,5 @@ -//===-- ExprSMTLIBLetPrinter.h ------------------------------------------*- C++ -*-===// +//===-- ExprSMTLIBLetPrinter.h ------------------------------------------*- C++ +//-*-===// // // The KLEE Symbolic Virtual Machine // @@ -11,63 +12,62 @@ #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(); +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(); - private: - ///Let expression binding number map. - std::map<const ref<Expr>,unsigned int> bindings; +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(); - /* 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; +private: + /// Let expression binding number map. + std::map<const ref<Expr>, unsigned int> bindings; - ///This is the prefix string used for all abbreviations in (let) expressions. - static const char BINDING_PREFIX[]; + /* 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 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; + /// 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(); +/// 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 index 83f48eb6..42f38007 100644 --- a/include/klee/util/ExprSMTLIBPrinter.h +++ b/include/klee/util/ExprSMTLIBPrinter.h @@ -1,4 +1,5 @@ -//===-- ExprSMTLIBPrinter.h ------------------------------------------*- C++ -*-===// +//===-- ExprSMTLIBPrinter.h ------------------------------------------*- C++ +//-*-===// // // The KLEE Symbolic Virtual Machine // @@ -21,302 +22,324 @@ namespace klee { - ///Base Class for SMTLIBv2 printer for KLEE Queries. 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. +/// Base Class for SMTLIBv2 printer for KLEE Queries. 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). +/// +/// +/// Note that in KLEE at the lowest level the solver checks for validity of the +/// query, i.e. +/// +/// \f[ \forall X constraints(X) \to query(X) \f] +/// +/// Where \f$X\f$ is some assignment, \f$constraints(X)\f$ are the constraints +/// in the query and \f$query(X)\f$ is the query expression. +/// If the above formula is true the query is said to be **valid**, otherwise it +/// is +/// **invalid**. +/// +/// The SMTLIBv2 language works in terms of satisfiability rather than validity +/// so instead +/// this class must ask the equivalent query but in terms of satisfiability +/// which is: +/// +/// \f[ \lnot \exists X constraints(X) \land \lnot query(X) \f] +/// +/// The printed SMTLIBv2 query actually asks the following: +/// +/// \f[ \exists X constraints(X) \land \lnot query(X) \f] +/// Hence the printed SMTLIBv2 query will just assert the constraints and the +/// negation +/// of the query expression. +/// +/// If a SMTLIBv2 solver says the printed query is satisfiable the then original +/// query passed to this class was **invalid** and if a SMTLIBv2 solver says the +/// printed +/// query is unsatisfiable then the original query passed to this class was +/// **valid**. +/// +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. /// - ///This printer does not abbreviate expressions. The printer ExprSMTLIBLetPrinter does though. + /// All options should be set before calling this. + /// \sa setConstantDisplayMode + /// \sa setLogic() + /// \sa setHumanReadable + /// \sa setSMTLIBboolOption + /// \sa setArrayValuesToGet /// - /// 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() + /// 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. /// - ///The class can then be used again on another query ( setQuery() ). - ///The options set are persistent across queries (apart from setArrayValuesToGet() and PRODUCE_MODELS). - /// - /// - ///Note that in KLEE at the lowest level the solver checks for validity of the query, i.e. - /// - /// \f[ \forall X constraints(X) \to query(X) \f] - /// - /// Where \f$X\f$ is some assignment, \f$constraints(X)\f$ are the constraints - /// in the query and \f$query(X)\f$ is the query expression. - /// If the above formula is true the query is said to be **valid**, otherwise it is - /// **invalid**. + /// \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 SMTLIBv2 language works in terms of satisfiability rather than validity so instead - /// this class must ask the equivalent query but in terms of satisfiability which is: + /// 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>) /// - /// \f[ \lnot \exists X constraints(X) \land \lnot query(X) \f] + /// By default no options will be printed so the SMTLIBv2 solver will use + /// its default values for all options. /// - /// The printed SMTLIBv2 query actually asks the following: + /// \return true if option was successfully set. /// - /// \f[ \exists X constraints(X) \land \lnot query(X) \f] - /// Hence the printed SMTLIBv2 query will just assert the constraints and the negation - /// of the query expression. + /// 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 a SMTLIBv2 solver says the printed query is satisfiable the then original - /// query passed to this class was **invalid** and if a SMTLIBv2 solver says the printed - /// query is unsatisfiable then the original query passed to this class was **valid**. + /// If no call is made to this function before + /// ExprSMTLIBPrinter::generateOutput() then + /// the solver will only be asked to check satisfiability. /// - 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 negated query expression - 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 negateQueryExpression() - 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 negateQueryExpression(); - - //Print a SMTLIBv2 option as a C-string - const char* getSMTLIBOptionString(ExprSMTLIBPrinter::SMTLIBboolOptions option); + /// 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(); - //Pointer to a vector of Arrays. These will be used for the (get-value () ) call. - const std::vector<const Array*> * arraysToCallGetValueOn; + // Print SMTLIBv2 for all constraints in the query + virtual void printConstraints(); - ConstantDisplayMode cdm; + // Print SMTLIBv2 assert statement for the negated query expression + 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 negateQueryExpression() + 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 negateQueryExpression(); + + // 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 index 7225704e..6a88ab5d 100644 --- a/lib/Expr/ExprSMTLIBLetPrinter.cpp +++ b/lib/Expr/ExprSMTLIBLetPrinter.cpp @@ -1,4 +1,5 @@ -//===-- ExprSMTLIBLetPrinter.cpp ------------------------------------------*- C++ -*-===// +//===-- ExprSMTLIBLetPrinter.cpp ------------------------------------------*- +//C++ -*-===// // // The KLEE Symbolic Virtual Machine // @@ -13,237 +14,220 @@ 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 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(); - } +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 index 9e97a4e0..c32b5bf9 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -1,4 +1,5 @@ -//===-- ExprSMTLIBPrinter.cpp ------------------------------------------*- C++ -*-===// +//===-- ExprSMTLIBPrinter.cpp ------------------------------------------*- C++ +//-*-===// // // The KLEE Symbolic Virtual Machine // @@ -14,893 +15,877 @@ 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) +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(); + negateQueryExpression(); +} + +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; +} + +namespace { + +struct ArrayPtrsByName { + bool operator()(const Array *a1, const Array *a2) const { + return a1->name < a2->name; + } +}; + +} + +void ExprSMTLIBPrinter::printArrayDeclarations() { + // Assume scan() has been called + if (humanReadable) + *o << "; Array declarations" << endl; + + // Declare arrays in a deterministic order. + std::vector<const Array *> sortedArrays(usedArrays.begin(), usedArrays.end()); + std::sort(sortedArrays.begin(), sortedArrays.end(), ArrayPtrsByName()); + for (std::vector<const Array *>::iterator it = sortedArrays.begin(); + it != sortedArrays.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 (std::vector<const Array *>::iterator it = sortedArrays.begin(); + it != sortedArrays.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; +} - 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 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(); + } -namespace klee -{ + p->pushIndent(); + *p << "(assert"; + p->pushIndent(); + printSeperator(); - ExprSMTLIBPrinter::ExprSMTLIBPrinter() : - usedArrays(), o(NULL), query(NULL), p(NULL), haveConstantArray(false), logicToUse(QF_AUFBV), - humanReadable(ExprSMTLIBOptions::humanReadableSMTLIB), smtlibBoolOptions(), arraysToCallGetValueOn(NULL) - { - setConstantDisplayMode(ExprSMTLIBOptions::argConstantDisplayMode); - } + printExpression(queryAssert, SORT_BOOL); - ExprSMTLIBPrinter::~ExprSMTLIBPrinter() - { - if(p!=NULL) - delete p; - } + p->popIndent(); + printSeperator(); + *p << ")"; + p->popIndent(); + p->breakLineI(); +} - void ExprSMTLIBPrinter::setOutput(std::ostream& output) - { - o = &output; - if(p!=NULL) - delete p; +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); +} - p = new PrintContext(output); - } +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 - void ExprSMTLIBPrinter::setQuery(const Query& q) - { - query = &q; - reset(); // clear the data structures - scanAll(); - negateQueryExpression(); - } + *p << "(" << getSMTLIBKeyword(e) << " "; + p->pushIndent(); // add indent for recursive call - void ExprSMTLIBPrinter::reset() - { - usedArrays.clear(); - haveConstantArray=false; + // The condition + printSeperator(); + printExpression(e->getKid(0), SORT_BOOL); - /* 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); + /* This operator is special in that the remaining children + * can be of any sort. + */ - arraysToCallGetValueOn=NULL; + // if true + printSeperator(); + printExpression(e->getKid(1), s); + // if false + printSeperator(); + printExpression(e->getKid(2), s); - } - - bool ExprSMTLIBPrinter::isHumanReadable() - { - return humanReadable; - } + p->popIndent(); // pop indent added for recursive call + printSeperator(); + *p << ")"; +} - bool ExprSMTLIBPrinter::setConstantDisplayMode(ConstantDisplayMode cdm) - { - if(cdm > DECIMAL) - return false; +void ExprSMTLIBPrinter::printSortArgsExpr(const ref<Expr> &e, + ExprSMTLIBPrinter::SMTLIB_SORT s) { + *p << "(" << getSMTLIBKeyword(e) << " "; + p->pushIndent(); // add indent for recursive call - this->cdm = cdm; - return true; - } + // 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); + } - 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::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; - 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"; - } + 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::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; + 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"; + } +} +} diff --git a/test/Expr/print-smt.smt2.good b/test/Expr/print-smt.smt2.good index cca282af..7b2002b9 100644 --- a/test/Expr/print-smt.smt2.good +++ b/test/Expr/print-smt.smt2.good @@ -859,9 +859,9 @@ ;SMTLIBv2 Query 72 (set-option :produce-models true) (set-logic QF_AUFBV ) -(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) (declare-fun const_arr2 () (Array (_ BitVec 32) (_ BitVec 8) ) ) (declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) ) +(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) (assert (= (select const_arr2 (_ bv0 32) ) (_ bv121 8) ) ) (assert (= (select const_arr2 (_ bv1 32) ) (_ bv101 8) ) ) (assert (= (select const_arr2 (_ bv2 32) ) (_ bv115 8) ) ) @@ -881,8 +881,8 @@ ;SMTLIBv2 Query 73 (set-option :produce-models true) (set-logic QF_AUFBV ) -(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) (declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) ) +(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) (assert (let ( (?B0 ((_ extract 31 0) (bvadd (_ bv18446744073709533360 64) (bvmul (_ bv4 64) ((_ sign_extend 32) (concat (select unnamed_1 (_ bv3 32) ) (concat (select unnamed_1 (_ bv2 32) ) (concat (select unnamed_1 (_ bv1 32) ) (select unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) ) (?B1 (bvadd (_ bv18446744073709533360 64) (bvmul (_ bv4 64) ((_ sign_extend 32) (concat (select unnamed_1 (_ bv3 32) ) (concat (select unnamed_1 (_ bv2 32) ) (concat (select unnamed_1 (_ bv1 32) ) (select unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (?B2 (bvmul (_ bv4 64) ((_ sign_extend 32) (concat (select unnamed_1 (_ bv3 32) ) (concat (select unnamed_1 (_ bv2 32) ) (concat (select unnamed_1 (_ bv1 32) ) (select unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (and (= false (bvult ?B2 (_ bv13 64) ) ) (and (= false (bvult (bvadd (_ bv31312 64) ?B2 ) (_ bv1 64) ) ) (and (= false (bvult (bvadd (_ bv31760 64) ?B2 ) (_ bv13 64) ) ) (and (= false (bvult (bvadd (_ bv111120 64) ?B2 ) (_ bv1 64) ) ) (and (bvult ?B1 (_ bv1 64) ) (= false (= (concat (select unnamed (_ bv3 32) ) (concat (select unnamed (_ bv2 32) ) (concat (select unnamed (_ bv1 32) ) (select unnamed (_ bv0 32) ) ) ) ) (concat (select unnamed (bvadd (_ bv3 32) ?B0 ) ) (concat (select unnamed (bvadd (_ bv2 32) ?B0 ) ) (concat (select unnamed (bvadd (_ bv1 32) ?B0 ) ) (select unnamed ?B0 ) ) ) ) ) ) ) ) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) @@ -898,9 +898,9 @@ ;SMTLIBv2 Query 74 (set-option :produce-models true) (set-logic QF_AUFBV ) -(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) ) (declare-fun const_arr5 () (Array (_ BitVec 32) (_ BitVec 8) ) ) +(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) ) +(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) (assert (= (select const_arr5 (_ bv0 32) ) (_ bv171 8) ) ) (assert (= (select const_arr5 (_ bv1 32) ) (_ bv171 8) ) ) (assert (= (select const_arr5 (_ bv2 32) ) (_ bv171 8) ) ) @@ -920,9 +920,9 @@ ;SMTLIBv2 Query 75 (set-option :produce-models true) (set-logic QF_AUFBV ) -(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) ) (declare-fun const_arr1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) +(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) ) +(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) (assert (= (select const_arr1 (_ bv0 32) ) (_ bv12 8) ) ) (assert (= (select const_arr1 (_ bv1 32) ) (_ bv0 8) ) ) (assert (= (select const_arr1 (_ bv2 32) ) (_ bv0 8) ) ) @@ -954,9 +954,9 @@ ;SMTLIBv2 Query 76 (set-option :produce-models true) (set-logic QF_AUFBV ) -(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) ) (declare-fun const_arr4 () (Array (_ BitVec 32) (_ BitVec 8) ) ) +(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) ) +(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) (assert (= (select const_arr4 (_ bv0 32) ) (_ bv171 8) ) ) (assert (= (select const_arr4 (_ bv1 32) ) (_ bv171 8) ) ) (assert (= (select const_arr4 (_ bv2 32) ) (_ bv171 8) ) ) @@ -976,9 +976,9 @@ ;SMTLIBv2 Query 77 (set-option :produce-models true) (set-logic QF_AUFBV ) -(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) -(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) ) (declare-fun const_arr3 () (Array (_ BitVec 32) (_ BitVec 8) ) ) +(declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) ) +(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) (assert (= (select const_arr3 (_ bv0 32) ) (_ bv12 8) ) ) (assert (= (select const_arr3 (_ bv1 32) ) (_ bv0 8) ) ) (assert (= (select const_arr3 (_ bv2 32) ) (_ bv0 8) ) ) @@ -1010,8 +1010,8 @@ ;SMTLIBv2 Query 78 (set-option :produce-models true) (set-logic QF_AUFBV ) -(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) (declare-fun unnamed () (Array (_ BitVec 32) (_ BitVec 8) ) ) +(declare-fun unnamed_1 () (Array (_ BitVec 32) (_ BitVec 8) ) ) (assert (let ( (?B0 ((_ extract 31 0) (bvadd (_ bv18446744073709532800 64) (bvmul (_ bv4 64) ((_ sign_extend 32) (concat (select unnamed_1 (_ bv3 32) ) (concat (select unnamed_1 (_ bv2 32) ) (concat (select unnamed_1 (_ bv1 32) ) (select unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) ) (?B1 (bvadd (_ bv18446744073709532800 64) (bvmul (_ bv4 64) ((_ sign_extend 32) (concat (select unnamed_1 (_ bv3 32) ) (concat (select unnamed_1 (_ bv2 32) ) (concat (select unnamed_1 (_ bv1 32) ) (select unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (?B2 (bvmul (_ bv4 64) ((_ sign_extend 32) (concat (select unnamed_1 (_ bv3 32) ) (concat (select unnamed_1 (_ bv2 32) ) (concat (select unnamed_1 (_ bv1 32) ) (select unnamed_1 (_ bv0 32) ) ) ) ) ) ) ) ) (and (= false (bvult ?B2 (_ bv13 64) ) ) (and (= false (bvult (bvadd (_ bv31312 64) ?B2 ) (_ bv1 64) ) ) (and (= false (bvult (bvadd (_ bv31760 64) ?B2 ) (_ bv13 64) ) ) (and (= false (bvult (bvadd (_ bv111120 64) ?B2 ) (_ bv1 64) ) ) (and (= false (bvult (bvadd (_ bv18446744073709533360 64) ?B2 ) (_ bv1 64) ) ) (and (= false (bvult (bvadd (_ bv18446744073709533328 64) ?B2 ) (_ bv1 64) ) ) (and (bvult ?B1 (_ bv1 64) ) (= (concat (select unnamed (_ bv3 32) ) (concat (select unnamed (_ bv2 32) ) (concat (select unnamed (_ bv1 32) ) (select unnamed (_ bv0 32) ) ) ) ) (concat (select unnamed_1 (bvadd (_ bv3 32) ?B0 ) ) (concat (select unnamed_1 (bvadd (_ bv2 32) ?B0 ) ) (concat (select unnamed_1 (bvadd (_ bv1 32) ?B0 ) ) (select unnamed_1 ?B0 ) ) ) ) ) ) ) ) ) ) ) ) ) ) (check-sat) (get-value ( (select unnamed_1 (_ bv0 32) ) ) ) |