diff options
Diffstat (limited to 'include/klee/util/ExprSMTLIBPrinter.h')
| -rw-r--r-- | include/klee/util/ExprSMTLIBPrinter.h | 107 |
1 files changed, 72 insertions, 35 deletions
diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h index 8b072242..6b0d260a 100644 --- a/include/klee/util/ExprSMTLIBPrinter.h +++ b/include/klee/util/ExprSMTLIBPrinter.h @@ -30,8 +30,7 @@ namespace klee { /// 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. +/// This printer abbreviates expressions according to its abbreviation mode. /// /// It is intended to be used as follows /// -# Create instance of this class @@ -83,7 +82,7 @@ public: 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 + ///< uninterpreted functions }; /// Different SMTLIBv2 options that have a boolean value that can be set @@ -100,7 +99,7 @@ public: 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) + ///< output) }; enum ConstantDisplayMode { @@ -109,6 +108,14 @@ public: DECIMAL ///< Display bit vector constants in Decimal e.g. (_ bv45 8) }; + /// How to abbreviate repeatedly mentioned expressions. Some solvers do not + /// understand all of them, hence the flexibility. + enum AbbreviationMode { + ABBR_NONE, ///< Do not abbreviate. + ABBR_LET, ///< Abbreviate with let. + ABBR_NAMED ///< Abbreviate with :named annotations. + }; + /// Different supported SMTLIBv2 sorts (a.k.a type) in QF_AUFBV enum SMTLIB_SORT { SORT_BITVECTOR, SORT_BOOL }; @@ -119,6 +126,8 @@ public: ConstantDisplayMode getConstantDisplayMode() { return cdm; } + void setAbbreviationMode(AbbreviationMode am) { abbrMode = am; } + /// Create a new printer that will print a query in the SMTLIBv2 language. ExprSMTLIBPrinter(); @@ -131,7 +140,7 @@ public: /// the SMTLIBv2 (get-value ()) command). void setQuery(const Query &q); - virtual ~ExprSMTLIBPrinter(); + ~ExprSMTLIBPrinter(); /// Print the query to the llvm::raw_ostream /// setOutput() and setQuery() must be called before calling this. @@ -150,7 +159,7 @@ public: /// is made that uses the PRODUCE_MODELS before calling setArrayValuesToGet() /// then the setSMTLIBboolOption() /// call will be ineffective. - virtual void generateOutput(); + void generateOutput(); /// Set which SMTLIBv2 logic to use. /// This only affects what logic is used in the (set-logic <logic>) command. @@ -204,6 +213,21 @@ protected: /// Contains the arrays found during scans std::set<const Array *> usedArrays; + /// Set of expressions seen during scan. + std::set<ref<Expr> > seenExprs; + + typedef std::map<const ref<Expr>, int> BindingMap; + + /// Let expression binding number map. Under the :named abbreviation mode, + /// negative binding numbers indicate that the abbreviation has already been + /// emitted, so it may be used. + BindingMap bindings; + + /// An ordered list of expression bindings. + /// Exprs in BindingMap at index i depend on Exprs in BindingMap at i-1. + /// Exprs in orderedBindings[0] have no dependencies. + std::vector<BindingMap> orderedBindings; + /// Output stream to write to llvm::raw_ostream *o; @@ -217,36 +241,40 @@ protected: void printCastToSort(const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT sort); // Resets various internal objects for a new query - virtual void reset(); + void reset(); // Scan all constraints and the query - virtual void scanAll(); + void scanAll(); // Print an initial SMTLIBv2 comment before anything else is printed - virtual void printNotice(); + void printNotice(); // Print SMTLIBv2 options e.g. (set-option :option-name <value>) command - virtual void printOptions(); + void printOptions(); // Print SMTLIBv2 logic to use e.g. (set-logic QF_ABV) - virtual void printSetLogic(); + void printSetLogic(); // Print SMTLIBv2 assertions for constant arrays - virtual void printArrayDeclarations(); + void printArrayDeclarations(); + + // Print SMTLIBv2 for the query optimised for human readability + void printHumanReadableQuery(); - // Print SMTLIBv2 for all constraints in the query - virtual void printConstraints(); + // Print SMTLIBv2 for the query optimised for minimal query size. + // This does not imply ABBR_LET or ABBR_NAMED (although it would be wise + // to use them to minimise the query size further) + void printMachineReadableQuery(); - // Print SMTLIBv2 assert statement for the negated query expression - virtual void printQuery(); + void printQueryInSingleAssert(); /// Print the SMTLIBv2 command to check satisfiability and also optionally /// request for values /// \sa setArrayValuesToGet() - virtual void printAction(); + void printAction(); /// Print the SMTLIBv2 command to exit - virtual void printExit(); + void printExit(); /// Print a Constant in the format specified by the current "Constant Display /// Mode" @@ -256,13 +284,18 @@ protected: /// \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); + /// \param abbrMode the abbreviation mode to use for this expression + void printExpression(const ref<Expr> &e, 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); + void scan(const ref<Expr> &e); + + /// Scan bindings for expression intra-dependencies. The result is written + /// to the orderedBindings vector that is later used for nested expression + /// printing in the let abbreviation mode. + void scanBindingExprDeps(); /* Rules of recursion for "Special Expression handlers" and *printSortArgsExpr() @@ -280,15 +313,15 @@ protected: */ // 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, + void printReadExpr(const ref<ReadExpr> &e); + void printExtractExpr(const ref<ExtractExpr> &e); + void printCastExpr(const ref<CastExpr> &e); + void printNotEqualExpr(const ref<NeExpr> &e); + 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, + void printSortArgsExpr(const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT s); /// For the set of operators that come in two sorts (e.g. (and () ()) (bvand @@ -296,21 +329,21 @@ protected: /// 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, + void printLogicalOrBitVectorExpr(const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT s); /// Recursively prints updatesNodes - virtual void printUpdatesAndArray(const UpdateNode *un, const Array *root); + 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); + const char *getSMTLIBKeyword(const ref<Expr> &e); - virtual void printSeperator(); + void printSeperator(); /// Helper function for scan() that scans the expressions of an update node - virtual void scanUpdates(const UpdateNode *un); + void scanUpdates(const UpdateNode *un); /// Helper printer class PrintContext *p; @@ -330,18 +363,22 @@ private: // 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); + /// Print expression without top-level abbreviations + void printFullExpression(const ref<Expr> &e, SMTLIB_SORT expectedSort); + + /// Print an assert statement for the given expr. + void printAssert(const ref<Expr> &e); + // Pointer to a vector of Arrays. These will be used for the (get-value () ) // call. const std::vector<const Array *> *arraysToCallGetValueOn; ConstantDisplayMode cdm; + AbbreviationMode abbrMode; }; } |