diff options
Diffstat (limited to 'include')
| -rw-r--r-- | include/klee/Config/config.h.in | 9 | ||||
| -rw-r--r-- | include/klee/ExecutionState.h | 4 | ||||
| -rw-r--r-- | include/klee/Expr.h | 61 | ||||
| -rw-r--r-- | include/klee/Internal/ADT/TreeStream.h | 1 | ||||
| -rw-r--r-- | include/klee/Internal/Module/KModule.h | 7 | ||||
| -rw-r--r-- | include/klee/Internal/System/MemoryUsage.h | 21 | ||||
| -rw-r--r-- | include/klee/Interpreter.h | 6 | ||||
| -rw-r--r-- | include/klee/util/ArrayExprHash.h | 2 | ||||
| -rw-r--r-- | include/klee/util/Assignment.h | 7 | ||||
| -rw-r--r-- | include/klee/util/ExprPPrinter.h | 14 | ||||
| -rw-r--r-- | include/klee/util/ExprRangeEvaluator.h | 2 | ||||
| -rw-r--r-- | include/klee/util/ExprSMTLIBLetPrinter.h | 104 | ||||
| -rw-r--r-- | include/klee/util/ExprSMTLIBPrinter.h | 592 | ||||
| -rw-r--r-- | include/klee/util/PrintContext.h | 16 | ||||
| -rw-r--r-- | include/klee/util/Ref.h | 12 |
15 files changed, 479 insertions, 379 deletions
diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in index 0a94de8f..5e49e35d 100644 --- a/include/klee/Config/config.h.in +++ b/include/klee/Config/config.h.in @@ -12,6 +12,9 @@ /* Define to 1 if you have the `stp' library (-lstp). */ #undef HAVE_LIBSTP +/* Define if mallinfo() is available on this platform. */ +#undef HAVE_MALLINFO + /* Define to 1 if you have the <memory.h> header file. */ #undef HAVE_MEMORY_H @@ -45,9 +48,6 @@ /* Define to 1 if you have the <unistd.h> header file. */ #undef HAVE_UNISTD_H -/* Path to KLEE's uClibc */ -#undef KLEE_UCLIBC - /* LLVM version is release (instead of development) */ #undef LLVM_IS_RELEASE @@ -81,6 +81,9 @@ /* Define to 1 if you have the ANSI C header files. */ #undef STDC_HEADERS +/* klee-uclibc is supported */ +#undef SUPPORT_KLEE_UCLIBC + /* Supporting metaSMT API */ #undef SUPPORT_METASMT diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h index 720488cc..824fbed5 100644 --- a/include/klee/ExecutionState.h +++ b/include/klee/ExecutionState.h @@ -32,7 +32,7 @@ namespace klee { class PTreeNode; struct InstructionInfo; -std::ostream &operator<<(std::ostream &os, const MemoryMap &mm); +llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const MemoryMap &mm); struct StackFrame { KInstIterator caller; @@ -137,7 +137,7 @@ public: } bool merge(const ExecutionState &b); - void dumpStack(std::ostream &out) const; + void dumpStack(llvm::raw_ostream &out) const; }; } diff --git a/include/klee/Expr.h b/include/klee/Expr.h index 4bebd521..c78cd690 100644 --- a/include/klee/Expr.h +++ b/include/klee/Expr.h @@ -17,13 +17,15 @@ #include "llvm/ADT/APFloat.h" #include "llvm/ADT/DenseSet.h" #include "llvm/ADT/SmallVector.h" +#include "llvm/Support/raw_ostream.h" +#include <sstream> #include <set> #include <vector> -#include <iosfwd> // FIXME: Remove this!!! namespace llvm { class Type; + class raw_ostream; } namespace klee { @@ -181,7 +183,7 @@ public: virtual unsigned getNumKids() const = 0; virtual ref<Expr> getKid(unsigned i) const = 0; - virtual void print(std::ostream &os) const; + virtual void print(llvm::raw_ostream &os) const; /// dump - Print the expression to stderr. void dump() const; @@ -197,8 +199,10 @@ public: typedef llvm::DenseSet<std::pair<const Expr *, const Expr *> > ExprEquivSet; int compare(const Expr &b, ExprEquivSet &equivs) const; int compare(const Expr &b) const { - ExprEquivSet equivs; - return compare(b, equivs); + static ExprEquivSet equivs; + int r = compare(b, equivs); + equivs.clear(); + return r; } virtual int compareContents(const Expr &b) const { return 0; } @@ -219,8 +223,8 @@ public: /* Static utility methods */ - static void printKind(std::ostream &os, Kind k); - static void printWidth(std::ostream &os, Expr::Width w); + static void printKind(llvm::raw_ostream &os, Kind k); + static void printWidth(llvm::raw_ostream &os, Expr::Width w); /// returns the smallest number of bytes in which the given width fits static inline unsigned getMinBytesForWidth(Width w) { @@ -289,15 +293,34 @@ inline bool operator>=(const Expr &lhs, const Expr &rhs) { // Printing operators -inline std::ostream &operator<<(std::ostream &os, const Expr &e) { +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const Expr &e) { e.print(os); return os; } -inline std::ostream &operator<<(std::ostream &os, const Expr::Kind kind) { +// XXX the following macro is to work around the ExprTest unit test compile error +#ifndef LLVM_29_UNITTEST +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const Expr::Kind kind) { Expr::printKind(os, kind); return os; } +#endif + +inline std::stringstream &operator<<(std::stringstream &os, const Expr &e) { + std::string str; + llvm::raw_string_ostream TmpStr(str); + e.print(TmpStr); + os << TmpStr.str(); + return os; +} + +inline std::stringstream &operator<<(std::stringstream &os, const Expr::Kind kind) { + std::string str; + llvm::raw_string_ostream TmpStr(str); + Expr::printKind(TmpStr, kind); + os << TmpStr.str(); + return os; +} // Terminal Exprs @@ -585,7 +608,9 @@ public: /// a symbolic array. If non-empty, this size of this array is equivalent to /// the array size. const std::vector< ref<ConstantExpr> > constantValues; - + + Expr::Width domain, range; + public: /// Array - Construct a new array object. /// @@ -596,9 +621,11 @@ public: /// distinguished once printed. Array(const std::string &_name, uint64_t _size, const ref<ConstantExpr> *constantValuesBegin = 0, - const ref<ConstantExpr> *constantValuesEnd = 0) + const ref<ConstantExpr> *constantValuesEnd = 0, + Expr::Width _domain = Expr::Int32, Expr::Width _range = Expr::Int8) : name(_name), size(_size), - constantValues(constantValuesBegin, constantValuesEnd) { + constantValues(constantValuesBegin, constantValuesEnd), + domain(_domain), range(_range) { assert((isSymbolicArray() || constantValues.size() == size) && "Invalid size for constant array!"); computeHash(); @@ -614,8 +641,8 @@ public: bool isSymbolicArray() const { return constantValues.empty(); } bool isConstantArray() const { return !isSymbolicArray(); } - Expr::Width getDomain() const { return Expr::Int32; } - Expr::Width getRange() const { return Expr::Int8; } + Expr::Width getDomain() const { return domain; } + Expr::Width getRange() const { return range; } unsigned computeHash(); unsigned hash() const { return hashValue; } @@ -669,15 +696,15 @@ public: static ref<Expr> create(const UpdateList &updates, ref<Expr> i); - Width getWidth() const { return Expr::Int8; } + Width getWidth() const { assert(updates.root); return updates.root->getRange(); } Kind getKind() const { return Read; } unsigned getNumKids() const { return numKids; } - ref<Expr> getKid(unsigned i) const { return !i ? index : 0; } + ref<Expr> getKid(unsigned i) const { return !i ? index : 0; } int compareContents(const Expr &b) const; - virtual ref<Expr> rebuild(ref<Expr> kids[]) const { + virtual ref<Expr> rebuild(ref<Expr> kids[]) const { return create(updates, kids[0]); } @@ -685,7 +712,7 @@ public: private: ReadExpr(const UpdateList &_updates, const ref<Expr> &_index) : - updates(_updates), index(_index) {} + updates(_updates), index(_index) { assert(updates.root); } public: static bool classof(const Expr *E) { diff --git a/include/klee/Internal/ADT/TreeStream.h b/include/klee/Internal/ADT/TreeStream.h index 63e49dbb..1494aa76 100644 --- a/include/klee/Internal/ADT/TreeStream.h +++ b/include/klee/Internal/ADT/TreeStream.h @@ -11,7 +11,6 @@ #define __UTIL_TREESTREAM_H__ #include <string> -#include <iostream> #include <vector> namespace klee { diff --git a/include/klee/Internal/Module/KModule.h b/include/klee/Internal/Module/KModule.h index 86be131b..80672b5e 100644 --- a/include/klee/Internal/Module/KModule.h +++ b/include/klee/Internal/Module/KModule.h @@ -110,6 +110,13 @@ namespace klee { Cell *constantTable; + // Functions which are part of KLEE runtime + std::set<const llvm::Function*> internalFunctions; + + private: + // Mark function with functionName as part of the KLEE runtime + void addInternalFunction(const char* functionName); + public: KModule(llvm::Module *_module); ~KModule(); diff --git a/include/klee/Internal/System/MemoryUsage.h b/include/klee/Internal/System/MemoryUsage.h new file mode 100644 index 00000000..e8e5d769 --- /dev/null +++ b/include/klee/Internal/System/MemoryUsage.h @@ -0,0 +1,21 @@ +//===-- MemoryUsage.h -------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_UTIL_MEMORYUSAGE_H +#define KLEE_UTIL_MEMORYUSAGE_H + +#include <cstddef> + +namespace klee { + namespace util { + size_t GetTotalMallocUsage(); + } +} + +#endif diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h index e93284d6..abd454b1 100644 --- a/include/klee/Interpreter.h +++ b/include/klee/Interpreter.h @@ -19,6 +19,8 @@ struct KTest; namespace llvm { class Function; class Module; +class raw_ostream; +class raw_fd_ostream; } namespace klee { @@ -31,10 +33,10 @@ public: InterpreterHandler() {} virtual ~InterpreterHandler() {} - virtual std::ostream &getInfoStream() const = 0; + virtual llvm::raw_ostream &getInfoStream() const = 0; virtual std::string getOutputFilename(const std::string &filename) = 0; - virtual std::ostream *openOutputFile(const std::string &filename) = 0; + virtual llvm::raw_fd_ostream *openOutputFile(const std::string &filename) = 0; virtual void incPathsExplored() = 0; diff --git a/include/klee/util/ArrayExprHash.h b/include/klee/util/ArrayExprHash.h index 9a527bcd..1e5ffc2e 100644 --- a/include/klee/util/ArrayExprHash.h +++ b/include/klee/util/ArrayExprHash.h @@ -132,4 +132,4 @@ void ArrayExprHash<T>::hashUpdateNodeExpr(const UpdateNode* un, T& exp) } -#endif \ No newline at end of file +#endif diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h index 838d03bd..63df4b65 100644 --- a/include/klee/util/Assignment.h +++ b/include/klee/util/Assignment.h @@ -67,15 +67,16 @@ namespace klee { inline ref<Expr> Assignment::evaluate(const Array *array, unsigned index) const { + assert(array); bindings_ty::const_iterator it = bindings.find(array); if (it!=bindings.end() && index<it->second.size()) { - return ConstantExpr::alloc(it->second[index], Expr::Int8); + return ConstantExpr::alloc(it->second[index], array->getRange()); } else { if (allowFreeValues) { return ReadExpr::create(UpdateList(array, 0), - ConstantExpr::alloc(index, Expr::Int32)); + ConstantExpr::alloc(index, array->getDomain())); } else { - return ConstantExpr::alloc(0, Expr::Int8); + return ConstantExpr::alloc(0, array->getRange()); } } } diff --git a/include/klee/util/ExprPPrinter.h b/include/klee/util/ExprPPrinter.h index 4d1930d8..622b0e80 100644 --- a/include/klee/util/ExprPPrinter.h +++ b/include/klee/util/ExprPPrinter.h @@ -12,6 +12,9 @@ #include "klee/Expr.h" +namespace llvm { + class raw_ostream; +} namespace klee { class ConstraintManager; @@ -20,11 +23,12 @@ namespace klee { ExprPPrinter() {} public: - static ExprPPrinter *create(std::ostream &os); + static ExprPPrinter *create(llvm::raw_ostream &os); virtual ~ExprPPrinter() {} virtual void setNewline(const std::string &newline) = 0; + virtual void setForceNoLineBreaks(bool forceNoLineBreaks) = 0; virtual void reset() = 0; virtual void scan(const ref<Expr> &e) = 0; virtual void print(const ref<Expr> &e, unsigned indent=0) = 0; @@ -44,7 +48,7 @@ namespace klee { /// printOne - Pretty print a single expression prefixed by a /// message and followed by a line break. - static void printOne(std::ostream &os, const char *message, + static void printOne(llvm::raw_ostream &os, const char *message, const ref<Expr> &e); /// printSingleExpr - Pretty print a single expression. @@ -54,12 +58,12 @@ namespace klee { /// Note that if the output stream is not positioned at the /// beginning of a line then printing will not resume at the /// correct position following any output line breaks. - static void printSingleExpr(std::ostream &os, const ref<Expr> &e); + static void printSingleExpr(llvm::raw_ostream &os, const ref<Expr> &e); - static void printConstraints(std::ostream &os, + static void printConstraints(llvm::raw_ostream &os, const ConstraintManager &constraints); - static void printQuery(std::ostream &os, + static void printQuery(llvm::raw_ostream &os, const ConstraintManager &constraints, const ref<Expr> &q, const ref<Expr> *evalExprsBegin = 0, diff --git a/include/klee/util/ExprRangeEvaluator.h b/include/klee/util/ExprRangeEvaluator.h index 34b85520..fea30b5b 100644 --- a/include/klee/util/ExprRangeEvaluator.h +++ b/include/klee/util/ExprRangeEvaluator.h @@ -102,7 +102,7 @@ T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) { const ReadExpr *re = cast<ReadExpr>(e); T index = evaluate(re->index); - assert(re->getWidth()==Expr::Int8 && "unexpected multibyte read"); + assert(re->updates.root && re->getWidth() == re->updates.root->range && "unexpected multibyte read"); return evalRead(re->updates, index); } 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..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 diff --git a/include/klee/util/PrintContext.h b/include/klee/util/PrintContext.h index a9e91925..6b1ef77a 100644 --- a/include/klee/util/PrintContext.h +++ b/include/klee/util/PrintContext.h @@ -1,14 +1,14 @@ #ifndef PRINTCONTEXT_H_ #define PRINTCONTEXT_H_ -#include <ostream> +#include "klee/Expr.h" +#include "llvm/Support/raw_ostream.h" #include <sstream> #include <string> #include <stack> -#include <iomanip> /// PrintContext - Helper class for pretty printing. -/// It provides a basic wrapper around std::ostream that keeps track of +/// It provides a basic wrapper around llvm::raw_ostream that keeps track of /// how many characters have been used on the current line. /// /// It also provides an optional way keeping track of the various levels of indentation @@ -16,8 +16,7 @@ /// \sa breakLineI() , \sa pushIndent(), \sa popIndent() class PrintContext { private: - std::ostream &os; - std::stringstream ss; + llvm::raw_ostream &os; std::string newline; ///This is used to keep track of the stack of indentations used by @@ -30,7 +29,7 @@ public: /// Number of characters on the current line. unsigned pos; - PrintContext(std::ostream &_os) : os(_os), newline("\n"), indentStack(), pos() + PrintContext(llvm::raw_ostream &_os) : os(_os), newline("\n"), indentStack(), pos() { indentStack.push(pos); } @@ -42,7 +41,7 @@ public: void breakLine(unsigned indent=0) { os << newline; if (indent) - os << std::setw(indent) << ' '; + os.indent(indent) << ' '; pos = indent; } @@ -79,7 +78,8 @@ public: template <typename T> PrintContext &operator<<(T elt) { - ss.str(""); + std::string str; + llvm::raw_string_ostream ss(str); ss << elt; write(ss.str()); return *this; diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h index d14de471..c77149aa 100644 --- a/include/klee/util/Ref.h +++ b/include/klee/util/Ref.h @@ -20,6 +20,10 @@ using llvm::dyn_cast_or_null; #include <assert.h> #include <iosfwd> // FIXME: Remove this!!! +namespace llvm { + class raw_ostream; +} + namespace klee { template<class T> @@ -107,7 +111,13 @@ public: }; template<class T> -inline std::ostream &operator<<(std::ostream &os, const ref<T> &e) { +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const ref<T> &e) { + os << *e; + return os; +} + +template<class T> +inline std::stringstream &operator<<(std::stringstream &os, const ref<T> &e) { os << *e; return os; } |