1 //===-- ExprSMTLIBPrinter.h ------------------------------------------*- C++ 2 //-*-===// 3 // 4 // The KLEE Symbolic Virtual Machine 5 // 6 // This file is distributed under the University of Illinois Open Source 7 // License. See LICENSE.TXT for details. 8 // 9 //===----------------------------------------------------------------------===// 10 11 #ifndef KLEE_EXPRSMTLIBPRINTER_H 12 #define KLEE_EXPRSMTLIBPRINTER_H 13 14 #include "klee/Expr/Constraints.h" 15 #include "klee/Expr/Expr.h" 16 #include "klee/Solver/Solver.h" 17 #include "klee/Support/PrintContext.h" 18 19 #include <map> 20 #include <set> 21 #include <string> 22 23 namespace llvm { 24 class raw_ostream; 25 } 26 27 namespace klee { 28 29 /// Base Class for SMTLIBv2 printer for KLEE Queries. It uses the QF_ABV logic. 30 /// Note however the logic can be 31 /// set to QF_AUFBV because some solvers (e.g. STP) complain if this logic is 32 /// set to QF_ABV. 33 /// 34 /// This printer abbreviates expressions according to its abbreviation mode. 35 /// 36 /// It is intended to be used as follows 37 /// -# Create instance of this class 38 /// -# Set output ( setOutput() ) 39 /// -# Set query to print ( setQuery() ) 40 /// -# Set options using the methods prefixed with the word "set". 41 /// -# Call generateOutput() 42 /// 43 /// The class can then be used again on another query ( setQuery() ). 44 /// The options set are persistent across queries (apart from 45 /// setArrayValuesToGet() and PRODUCE_MODELS). 46 /// 47 /// 48 /// Note that in KLEE at the lowest level the solver checks for validity of the 49 /// query, i.e. 50 /// 51 /// \f[ \forall X constraints(X) \to query(X) \f] 52 /// 53 /// Where \f$X\f$ is some assignment, \f$constraints(X)\f$ are the constraints 54 /// in the query and \f$query(X)\f$ is the query expression. 55 /// If the above formula is true the query is said to be **valid**, otherwise it 56 /// is 57 /// **invalid**. 58 /// 59 /// The SMTLIBv2 language works in terms of satisfiability rather than validity 60 /// so instead 61 /// this class must ask the equivalent query but in terms of satisfiability 62 /// which is: 63 /// 64 /// \f[ \lnot \exists X constraints(X) \land \lnot query(X) \f] 65 /// 66 /// The printed SMTLIBv2 query actually asks the following: 67 /// 68 /// \f[ \exists X constraints(X) \land \lnot query(X) \f] 69 /// Hence the printed SMTLIBv2 query will just assert the constraints and the 70 /// negation 71 /// of the query expression. 72 /// 73 /// If a SMTLIBv2 solver says the printed query is satisfiable the then original 74 /// query passed to this class was **invalid** and if a SMTLIBv2 solver says the 75 /// printed 76 /// query is unsatisfiable then the original query passed to this class was 77 /// **valid**. 78 /// 79 class ExprSMTLIBPrinter { 80 public: 81 /// Different SMTLIBv2 logics supported by this class 82 /// \sa setLogic() 83 enum SMTLIBv2Logic { 84 QF_ABV, ///< Logic using Theory of Arrays and Theory of Bitvectors 85 QF_AUFBV ///< Logic using Theory of Arrays and Theory of Bitvectors and has 86 ///< uninterpreted functions 87 }; 88 89 /// Different SMTLIBv2 options that have a boolean value that can be set 90 /// \sa setSMTLIBboolOption 91 enum SMTLIBboolOptions { 92 PRINT_SUCCESS, ///< print-success SMTLIBv2 option 93 PRODUCE_MODELS, ///< produce-models SMTLIBv2 option 94 INTERACTIVE_MODE ///< interactive-mode SMTLIBv2 option 95 }; 96 97 /// Different SMTLIBv2 bool option values 98 /// \sa setSMTLIBboolOption 99 enum SMTLIBboolValues { 100 OPTION_TRUE, ///< Set option to true 101 OPTION_FALSE, ///< Set option to false 102 OPTION_DEFAULT ///< Use solver's defaults (the option will not be set in 103 ///< output) 104 }; 105 106 enum ConstantDisplayMode { 107 BINARY, ///< Display bit vector constants in binary e.g. #b00101101 108 HEX, ///< Display bit vector constants in Hexidecimal e.g.#x2D 109 DECIMAL ///< Display bit vector constants in Decimal e.g. (_ bv45 8) 110 }; 111 112 /// How to abbreviate repeatedly mentioned expressions. Some solvers do not 113 /// understand all of them, hence the flexibility. 114 enum AbbreviationMode { 115 ABBR_NONE, ///< Do not abbreviate. 116 ABBR_LET, ///< Abbreviate with let. 117 ABBR_NAMED ///< Abbreviate with :named annotations. 118 }; 119 120 /// Different supported SMTLIBv2 sorts (a.k.a type) in QF_AUFBV 121 enum SMTLIB_SORT { SORT_BITVECTOR, SORT_BOOL }; 122 123 /// Allows the way Constant bitvectors are printed to be changed. 124 /// This setting is persistent across queries. 125 /// \return true if setting the mode was successful 126 bool setConstantDisplayMode(ConstantDisplayMode cdm); 127 getConstantDisplayMode()128 ConstantDisplayMode getConstantDisplayMode() { return cdm; } 129 setAbbreviationMode(AbbreviationMode am)130 void setAbbreviationMode(AbbreviationMode am) { abbrMode = am; } 131 132 /// Create a new printer that will print a query in the SMTLIBv2 language. 133 ExprSMTLIBPrinter(); 134 135 /// Set the output stream that will be printed to. 136 /// This call is persistent across queries. 137 void setOutput(llvm::raw_ostream &output); 138 139 /// Set the query to print. This will setArrayValuesToGet() 140 /// to none (i.e. no array values will be requested using 141 /// the SMTLIBv2 (get-value ()) command). 142 void setQuery(const Query &q); 143 144 ~ExprSMTLIBPrinter(); 145 146 /// Print the query to the llvm::raw_ostream 147 /// setOutput() and setQuery() must be called before calling this. 148 /// 149 /// All options should be set before calling this. 150 /// \sa setConstantDisplayMode 151 /// \sa setLogic() 152 /// \sa setHumanReadable 153 /// \sa setSMTLIBboolOption 154 /// \sa setArrayValuesToGet 155 /// 156 /// Mostly it does not matter what order the options are set in. However 157 /// calling 158 /// setArrayValuesToGet() implies PRODUCE_MODELS is set so, if a call to 159 /// setSMTLIBboolOption() 160 /// is made that uses the PRODUCE_MODELS before calling setArrayValuesToGet() 161 /// then the setSMTLIBboolOption() 162 /// call will be ineffective. 163 void generateOutput(); 164 165 /// Set which SMTLIBv2 logic to use. 166 /// This only affects what logic is used in the (set-logic <logic>) command. 167 /// The rest of the printed SMTLIBv2 commands are the same regardless of the 168 /// logic used. 169 /// 170 /// \return true if setting logic was successful. 171 bool setLogic(SMTLIBv2Logic l); 172 173 /// Sets how readable the printed SMTLIBv2 commands are. 174 /// \param hr If set to true the printed commands are made more human 175 /// readable. 176 /// 177 /// The printed commands are made human readable by... 178 /// - Indenting and line breaking. 179 /// - Adding comments 180 void setHumanReadable(bool hr); 181 182 /// Set SMTLIB options. 183 /// These options will be printed when generateOutput() is called via 184 /// the SMTLIBv2 command (set-option :option-name <value>) 185 /// 186 /// By default no options will be printed so the SMTLIBv2 solver will use 187 /// its default values for all options. 188 /// 189 /// \return true if option was successfully set. 190 /// 191 /// The options set are persistent across calls to setQuery() apart from the 192 /// PRODUCE_MODELS option which this printer may automatically set/unset. 193 bool setSMTLIBboolOption(SMTLIBboolOptions option, SMTLIBboolValues value); 194 195 /// Set the array names that the SMTLIBv2 solver will be asked to determine. 196 /// Calling this method implies the PRODUCE_MODELS option is true and will 197 /// change 198 /// any previously set value. 199 /// 200 /// If no call is made to this function before 201 /// ExprSMTLIBPrinter::generateOutput() then 202 /// the solver will only be asked to check satisfiability. 203 /// 204 /// If the passed vector is not empty then the values of those arrays will be 205 /// requested 206 /// via (get-value ()) SMTLIBv2 command in the output stream in the same order 207 /// as vector. 208 void setArrayValuesToGet(const std::vector<const Array *> &a); 209 210 /// \return True if human readable mode is switched on 211 bool isHumanReadable(); 212 213 protected: 214 /// Contains the arrays found during scans 215 std::set<const Array *> usedArrays; 216 217 /// Set of expressions seen during scan. 218 std::set<ref<Expr> > seenExprs; 219 220 typedef std::map<const ref<Expr>, int> BindingMap; 221 222 /// Let expression binding number map. Under the :named abbreviation mode, 223 /// negative binding numbers indicate that the abbreviation has already been 224 /// emitted, so it may be used. 225 BindingMap bindings; 226 227 /// An ordered list of expression bindings. 228 /// Exprs in BindingMap at index i depend on Exprs in BindingMap at i-1. 229 /// Exprs in orderedBindings[0] have no dependencies. 230 std::vector<BindingMap> orderedBindings; 231 232 /// Output stream to write to 233 llvm::raw_ostream *o; 234 235 /// The query to print 236 const Query *query; 237 238 /// Determine the SMTLIBv2 sort of the expression 239 SMTLIB_SORT getSort(const ref<Expr> &e); 240 241 /// Print an expression but cast it to a particular SMTLIBv2 sort first. 242 void printCastToSort(const ref<Expr> &e, ExprSMTLIBPrinter::SMTLIB_SORT sort); 243 244 // Resets various internal objects for a new query 245 void reset(); 246 247 // Scan all constraints and the query 248 void scanAll(); 249 250 // Print an initial SMTLIBv2 comment before anything else is printed 251 void printNotice(); 252 253 // Print SMTLIBv2 options e.g. (set-option :option-name <value>) command 254 void printOptions(); 255 256 // Print SMTLIBv2 logic to use e.g. (set-logic QF_ABV) 257 void printSetLogic(); 258 259 // Print SMTLIBv2 assertions for constant arrays 260 void printArrayDeclarations(); 261 262 // Print SMTLIBv2 for the query optimised for human readability 263 void printHumanReadableQuery(); 264 265 // Print SMTLIBv2 for the query optimised for minimal query size. 266 // This does not imply ABBR_LET or ABBR_NAMED (although it would be wise 267 // to use them to minimise the query size further) 268 void printMachineReadableQuery(); 269 270 void printQueryInSingleAssert(); 271 272 /// Print the SMTLIBv2 command to check satisfiability and also optionally 273 /// request for values 274 /// \sa setArrayValuesToGet() 275 void printAction(); 276 277 /// Print the SMTLIBv2 command to exit 278 void printExit(); 279 280 /// Print a Constant in the format specified by the current "Constant Display 281 /// Mode" 282 void printConstant(const ref<ConstantExpr> &e); 283 284 /// Recursively print expression 285 /// \param e is the expression to print 286 /// \param expectedSort is the sort we want. If "e" is not of the right type a 287 /// cast will be performed. 288 /// \param abbrMode the abbreviation mode to use for this expression 289 void printExpression(const ref<Expr> &e, SMTLIB_SORT expectedSort); 290 291 /// Scan Expression recursively for Arrays in expressions. Found arrays are 292 /// added to 293 /// the usedArrays vector. 294 void scan(const ref<Expr> &e); 295 296 /// Scan bindings for expression intra-dependencies. The result is written 297 /// to the orderedBindings vector that is later used for nested expression 298 /// printing in the let abbreviation mode. 299 void scanBindingExprDeps(); 300 301 /* Rules of recursion for "Special Expression handlers" and 302 *printSortArgsExpr() 303 * 304 * 1. The parent of the recursion will have created an indent level for you so 305 *you don't need to add another initially. 306 * 2. You do not need to add a line break (via printSeperator() ) at the end, 307 *the parent caller will handle that. 308 * 3. The effect of a single recursive call should not affect the depth of the 309 *indent stack (nor the contents 310 * of the indent stack prior to the call). I.e. After executing a single 311 *recursive call the indent stack 312 * should have the same size and contents as before executing the recursive 313 *call. 314 */ 315 316 // Special Expression handlers 317 void printReadExpr(const ref<ReadExpr> &e); 318 void printExtractExpr(const ref<ExtractExpr> &e); 319 void printCastExpr(const ref<CastExpr> &e); 320 void printNotEqualExpr(const ref<NeExpr> &e); 321 void printSelectExpr(const ref<SelectExpr> &e, 322 ExprSMTLIBPrinter::SMTLIB_SORT s); 323 void printAShrExpr(const ref<AShrExpr> &e); 324 325 // For the set of operators that take sort "s" arguments 326 void printSortArgsExpr(const ref<Expr> &e, 327 ExprSMTLIBPrinter::SMTLIB_SORT s); 328 329 /// For the set of operators that come in two sorts (e.g. (and () ()) (bvand 330 /// () ()) ) 331 /// These are and,xor,or,not 332 /// \param e the Expression to print 333 /// \param s the sort of the expression we want 334 void printLogicalOrBitVectorExpr(const ref<Expr> &e, 335 ExprSMTLIBPrinter::SMTLIB_SORT s); 336 337 /// Recursively prints updatesNodes 338 void printUpdatesAndArray(const UpdateNode *un, const Array *root); 339 340 /// This method does the translation between Expr classes and SMTLIBv2 341 /// keywords 342 /// \return A C-string of the SMTLIBv2 keyword 343 const char *getSMTLIBKeyword(const ref<Expr> &e); 344 345 void printSeperator(); 346 347 /// Helper function for scan() that scans the expressions of an update node 348 void scanUpdates(const UpdateNode *un); 349 350 /// Helper printer class 351 PrintContext *p; 352 353 /// This contains the query from the solver but negated for our purposes. 354 /// \sa negateQueryExpression() 355 ref<Expr> queryAssert; 356 357 /// Indicates if there were any constant arrays founds during a scan() 358 bool haveConstantArray; 359 360 private: 361 SMTLIBv2Logic logicToUse; 362 363 volatile bool humanReadable; 364 365 // Map of enabled SMTLIB Options 366 std::map<SMTLIBboolOptions, bool> smtlibBoolOptions; 367 368 // Print a SMTLIBv2 option as a C-string 369 const char * 370 getSMTLIBOptionString(ExprSMTLIBPrinter::SMTLIBboolOptions option); 371 372 /// Print expression without top-level abbreviations 373 void printFullExpression(const ref<Expr> &e, SMTLIB_SORT expectedSort); 374 375 /// Print an assert statement for the given expr. 376 void printAssert(const ref<Expr> &e); 377 378 // Pointer to a vector of Arrays. These will be used for the (get-value () ) 379 // call. 380 const std::vector<const Array *> *arraysToCallGetValueOn; 381 382 ConstantDisplayMode cdm; 383 AbbreviationMode abbrMode; 384 }; 385 } 386 387 #endif /* KLEE_EXPRSMTLIBPRINTER_H */ 388