diff options
Diffstat (limited to 'include')
| -rw-r--r-- | include/klee/util/ArrayExprHash.h | 3 | ||||
| -rw-r--r-- | include/klee/util/ExprHashMap.h | 3 | ||||
| -rw-r--r-- | include/klee/util/ExprSMTLIBLetPrinter.h | 73 | ||||
| -rw-r--r-- | include/klee/util/ExprSMTLIBPrinter.h | 107 |
4 files changed, 78 insertions, 108 deletions
diff --git a/include/klee/util/ArrayExprHash.h b/include/klee/util/ArrayExprHash.h index 646ffd0c..da3b1d2b 100644 --- a/include/klee/util/ArrayExprHash.h +++ b/include/klee/util/ArrayExprHash.h @@ -140,4 +140,7 @@ void ArrayExprHash<T>::hashUpdateNodeExpr(const UpdateNode* un, T& exp) } +#undef unordered_map +#undef unordered_set + #endif diff --git a/include/klee/util/ExprHashMap.h b/include/klee/util/ExprHashMap.h index 867ad001..88086e7c 100644 --- a/include/klee/util/ExprHashMap.h +++ b/include/klee/util/ExprHashMap.h @@ -56,4 +56,7 @@ namespace klee { } +#undef unordered_map +#undef unordered_set + #endif diff --git a/include/klee/util/ExprSMTLIBLetPrinter.h b/include/klee/util/ExprSMTLIBLetPrinter.h deleted file mode 100644 index dd97e0d5..00000000 --- a/include/klee/util/ExprSMTLIBLetPrinter.h +++ /dev/null @@ -1,73 +0,0 @@ -//===-- ExprSMTLIBLetPrinter.h ------------------------------------------*- C++ -//-*-===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#include "ExprSMTLIBPrinter.h" -#ifndef EXPRSMTLETPRINTER_H_ -#define EXPRSMTLETPRINTER_H_ - -namespace klee { -/// This printer behaves like ExprSMTLIBPrinter except that it will abbreviate -/// expressions -/// using the (let) SMT-LIBv2 command. Expression trees that appear two or more -/// times in the Query -/// passed to setQuery() will be abbreviated. -/// -/// This class should be used just like ExprSMTLIBPrinter. -class ExprSMTLIBLetPrinter : public ExprSMTLIBPrinter { -public: - ExprSMTLIBLetPrinter(); - virtual ~ExprSMTLIBLetPrinter() {} - virtual void generateOutput(); - -protected: - virtual void scan(const ref<Expr> &e); - virtual void reset(); - virtual void generateBindings(); - void printExpression(const ref<Expr> &e, - ExprSMTLIBPrinter::SMTLIB_SORT expectedSort); - void printLetExpression(); - -private: - /// Let expression binding number map. - std::map<const ref<Expr>, unsigned int> bindings; - - /* These are effectively expression counters. - * firstEO - first Occurrence of expression contains - * all expressions that occur once. It is - * only used to help us fill twoOrMoreOE - * - * twoOrMoreEO - Contains occur all expressions that - * that occur two or more times. These - * are the expressions that will be - * abbreviated by using (let () ()) expressions. - * - * - * - */ - std::set<ref<Expr> > firstEO, twoOrMoreEO; - - /// This is the prefix string used for all abbreviations in (let) expressions. - static const char BINDING_PREFIX[]; - - /* This is needed during un-abbreviated printing. - * Because we have overloaded printExpression() - * the parent will call it and will abbreviate - * when we don't want it to. This bool allows us - * to switch it on/off easily. - */ - bool disablePrintedAbbreviations; -}; - -/// Create a SMT-LIBv2 printer based on command line options -/// The caller is responsible for deleting the printer -ExprSMTLIBPrinter *createSMTLIBPrinter(); -} - -#endif /* EXPRSMTLETPRINTER_H_ */ diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h 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; }; } |