diff options
Diffstat (limited to 'include/klee/util/ExprSMTLIBPrinter.h')
| -rw-r--r-- | include/klee/util/ExprSMTLIBPrinter.h | 592 |
1 files changed, 309 insertions, 283 deletions
diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h index 83f48eb6..8b072242 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 // @@ -10,7 +11,6 @@ #ifndef KLEE_EXPRSMTLIBPRINTER_H #define KLEE_EXPRSMTLIBPRINTER_H -#include <ostream> #include <string> #include <set> #include <map> @@ -19,304 +19,330 @@ #include <klee/util/PrintContext.h> #include <klee/Solver.h> +namespace llvm { +class raw_ostream; +} + 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. - /// - ///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() +/// 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(llvm::raw_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 llvm::raw_ostream + /// setOutput() and setQuery() must be called before calling this. /// - ///The class can then be used again on another query ( setQuery() ). - ///The options set are persistent across queries (apart from setArrayValuesToGet() and PRODUCE_MODELS). + /// 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. /// - ///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 + llvm::raw_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 |