From 9b3c98850572f0729afe97ffde16d05a7e6e691b Mon Sep 17 00:00:00 2001 From: Cristian Cadar Date: Thu, 25 Jul 2019 22:22:55 +0100 Subject: Consolidated Expr-related include files into a single include/klee/Expr directory. This improves the organization of the code, and also makes it easier to reuse Expr outside KLEE. --- include/expr/Lexer.h | 121 --- include/expr/Parser.h | 237 ------ include/klee/Constraints.h | 72 -- include/klee/ExecutionState.h | 4 +- include/klee/Expr.h | 1174 ----------------------------- include/klee/Expr/ArrayCache.h | 81 ++ include/klee/Expr/ArrayExprHash.h | 139 ++++ include/klee/Expr/Assignment.h | 99 +++ include/klee/Expr/Constraints.h | 72 ++ include/klee/Expr/Expr.h | 1174 +++++++++++++++++++++++++++++ include/klee/Expr/ExprBuilder.h | 91 +++ include/klee/Expr/ExprEvaluator.h | 42 ++ include/klee/Expr/ExprHashMap.h | 62 ++ include/klee/Expr/ExprPPrinter.h | 78 ++ include/klee/Expr/ExprRangeEvaluator.h | 285 +++++++ include/klee/Expr/ExprSMTLIBPrinter.h | 387 ++++++++++ include/klee/Expr/ExprUtil.h | 52 ++ include/klee/Expr/ExprVisitor.h | 98 +++ include/klee/Expr/Parser/Lexer.h | 121 +++ include/klee/Expr/Parser/Parser.h | 237 ++++++ include/klee/ExprBuilder.h | 91 --- include/klee/Internal/Module/Cell.h | 2 +- include/klee/Solver.h | 2 +- include/klee/util/ArrayCache.h | 81 -- include/klee/util/ArrayExprHash.h | 139 ---- include/klee/util/Assignment.h | 101 --- include/klee/util/ExprEvaluator.h | 42 -- include/klee/util/ExprHashMap.h | 62 -- include/klee/util/ExprPPrinter.h | 78 -- include/klee/util/ExprRangeEvaluator.h | 285 ------- include/klee/util/ExprSMTLIBPrinter.h | 386 ---------- include/klee/util/ExprUtil.h | 51 -- include/klee/util/ExprVisitor.h | 98 --- include/klee/util/PrintContext.h | 4 +- lib/Core/AddressSpace.cpp | 2 +- lib/Core/AddressSpace.h | 2 +- lib/Core/Context.cpp | 2 +- lib/Core/Context.h | 2 +- lib/Core/ExecutionState.cpp | 2 +- lib/Core/Executor.cpp | 10 +- lib/Core/Executor.h | 7 +- lib/Core/ExecutorUtil.cpp | 8 +- lib/Core/ImpliedValue.cpp | 11 +- lib/Core/ImpliedValue.h | 2 +- lib/Core/Memory.cpp | 5 +- lib/Core/Memory.h | 5 +- lib/Core/MemoryManager.cpp | 5 +- lib/Core/PTree.cpp | 6 +- lib/Core/PTree.h | 2 +- lib/Core/SeedInfo.cpp | 4 +- lib/Core/SeedInfo.h | 2 +- lib/Core/TimingSolver.h | 2 +- lib/Expr/ArrayCache.cpp | 2 +- lib/Expr/ArrayExprOptimizer.cpp | 4 +- lib/Expr/ArrayExprOptimizer.h | 2 +- lib/Expr/ArrayExprRewriter.h | 2 +- lib/Expr/ArrayExprVisitor.h | 4 +- lib/Expr/Assigment.cpp | 4 +- lib/Expr/AssignmentGenerator.cpp | 13 +- lib/Expr/AssignmentGenerator.h | 6 +- lib/Expr/Constraints.cpp | 6 +- lib/Expr/Expr.cpp | 4 +- lib/Expr/ExprBuilder.cpp | 2 +- lib/Expr/ExprEvaluator.cpp | 2 +- lib/Expr/ExprPPrinter.cpp | 4 +- lib/Expr/ExprSMTLIBPrinter.cpp | 2 +- lib/Expr/ExprUtil.cpp | 10 +- lib/Expr/ExprVisitor.cpp | 5 +- lib/Expr/Lexer.cpp | 2 +- lib/Expr/Parser.cpp | 14 +- lib/Expr/Updates.cpp | 4 +- lib/Solver/AssignmentValidatingSolver.cpp | 6 +- lib/Solver/CachingSolver.cpp | 4 +- lib/Solver/CexCachingSolver.cpp | 10 +- lib/Solver/FastCexSolver.cpp | 20 +- lib/Solver/IncompleteSolver.cpp | 2 +- lib/Solver/IndependentSolver.cpp | 16 +- lib/Solver/KQueryLoggingSolver.cpp | 6 +- lib/Solver/MetaSMTBuilder.h | 18 +- lib/Solver/MetaSMTSolver.cpp | 13 +- lib/Solver/SMTLIBLoggingSolver.cpp | 3 +- lib/Solver/STPBuilder.cpp | 4 +- lib/Solver/STPBuilder.h | 4 +- lib/Solver/STPSolver.cpp | 12 +- lib/Solver/Solver.cpp | 3 +- lib/Solver/ValidatingSolver.cpp | 4 +- lib/Solver/Z3Builder.cpp | 2 +- lib/Solver/Z3Builder.h | 5 +- lib/Solver/Z3Solver.cpp | 9 +- tools/kleaver/main.cpp | 17 +- tools/klee/main.cpp | 2 +- unittests/Assignment/AssignmentTest.cpp | 6 +- unittests/Expr/ExprTest.cpp | 4 +- unittests/Solver/SolverTest.cpp | 12 +- 94 files changed, 3203 insertions(+), 3198 deletions(-) delete mode 100644 include/expr/Lexer.h delete mode 100644 include/expr/Parser.h delete mode 100644 include/klee/Constraints.h delete mode 100644 include/klee/Expr.h create mode 100644 include/klee/Expr/ArrayCache.h create mode 100644 include/klee/Expr/ArrayExprHash.h create mode 100644 include/klee/Expr/Assignment.h create mode 100644 include/klee/Expr/Constraints.h create mode 100644 include/klee/Expr/Expr.h create mode 100644 include/klee/Expr/ExprBuilder.h create mode 100644 include/klee/Expr/ExprEvaluator.h create mode 100644 include/klee/Expr/ExprHashMap.h create mode 100644 include/klee/Expr/ExprPPrinter.h create mode 100644 include/klee/Expr/ExprRangeEvaluator.h create mode 100644 include/klee/Expr/ExprSMTLIBPrinter.h create mode 100644 include/klee/Expr/ExprUtil.h create mode 100644 include/klee/Expr/ExprVisitor.h create mode 100644 include/klee/Expr/Parser/Lexer.h create mode 100644 include/klee/Expr/Parser/Parser.h delete mode 100644 include/klee/ExprBuilder.h delete mode 100644 include/klee/util/ArrayCache.h delete mode 100644 include/klee/util/ArrayExprHash.h delete mode 100644 include/klee/util/Assignment.h delete mode 100644 include/klee/util/ExprEvaluator.h delete mode 100644 include/klee/util/ExprHashMap.h delete mode 100644 include/klee/util/ExprPPrinter.h delete mode 100644 include/klee/util/ExprRangeEvaluator.h delete mode 100644 include/klee/util/ExprSMTLIBPrinter.h delete mode 100644 include/klee/util/ExprUtil.h delete mode 100644 include/klee/util/ExprVisitor.h diff --git a/include/expr/Lexer.h b/include/expr/Lexer.h deleted file mode 100644 index 14ae7f85..00000000 --- a/include/expr/Lexer.h +++ /dev/null @@ -1,121 +0,0 @@ -//===-- Lexer.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_LEXER_H -#define KLEE_LEXER_H - -#include - -namespace llvm { - class MemoryBuffer; -} - -namespace klee { -namespace expr { - struct Token { - enum Kind { - At, ///< '@' - Arrow, ///< '->' - Colon, ///< ':' - Comma, ///< ',' - Comment, ///< #[^\n]+ - EndOfFile, ///< - Equals, ///< ' = ' - Identifier, ///< [a-zA-Z_][a-zA-Z0-9._]* - KWArray, ///< 'array' - KWFalse, ///< 'false' - KWQuery, ///< 'query' - KWReserved, ///< fp[0-9]+([.].*)?, i[0-9]+ - KWSymbolic, ///< 'symbolic' - KWTrue, ///< 'true' - KWWidth, ///< w[0-9]+ - LBrace, ///< '{' - LParen, ///< '(' - LSquare, ///< '[' - Number, ///< [+-]?[0-9][a-zA-Z0-9_]+ - RBrace, ///< '}' - RParen, ///< ')' - RSquare, ///< ']' - Semicolon, ///< ';' - Unknown, ///< - - KWKindFirst=KWArray, - KWKindLast=KWWidth - }; - - Kind kind; /// The token kind. - const char *start; /// The beginning of the token string. - unsigned length; /// The length of the token. - unsigned line; /// The line number of the start of this token. - unsigned column; /// The column number at the start of - /// this token. - - /// getKindName - The name of this token's kind. - const char *getKindName() const; - - /// getString - The string spanned by this token. This is not - /// particularly efficient, use start and length when reasonable. - std::string getString() const { return std::string(start, length); } - - /// isKeyword - True if this token is a keyword. - bool isKeyword() const { - return kind >= KWKindFirst && kind <= KWKindLast; - } - - // dump - Dump the token to stderr. - void dump(); - - Token() : kind(Unknown), start(nullptr) {} - }; - - /// Lexer - Interface for lexing tokens from a .kquery language file. - class Lexer { - const char *BufferPos; /// The current lexer position. - const char *BufferEnd; /// The buffer end position. - unsigned LineNumber; /// The current line. - unsigned ColumnNumber; /// The current column. - - /// GetNextChar - Eat a character or -1 from the stream. - int GetNextChar(); - - /// PeekNextChar - Return the next character without consuming it - /// from the stream. This does not perform newline - /// canonicalization. - int PeekNextChar(); - - /// SetTokenKind - Set the token kind and length (using the - /// token's start pointer, which must have been initialized). - Token &SetTokenKind(Token &Result, Token::Kind k); - - /// SetTokenKind - Set an identifiers token kind. This has the - /// same requirements as SetTokenKind and additionally takes care - /// of keyword recognition. - Token &SetIdentifierTokenKind(Token &Result); - - void SkipToEndOfLine(); - - /// LexNumber - Lex a number which does not have a base specifier. - Token &LexNumber(Token &Result); - - /// LexIdentifier - Lex an identifier. - Token &LexIdentifier(Token &Result); - - public: - explicit Lexer(const llvm::MemoryBuffer *_buf); - ~Lexer(); - - /// Lex - Return the next token from the file or EOF continually - /// when the end of the file is reached. The input argument is - /// used as the result, for convenience. - Token &Lex(Token &Result); - }; -} -} - -#endif /* KLEE_LEXER_H */ diff --git a/include/expr/Parser.h b/include/expr/Parser.h deleted file mode 100644 index 6a34b8d0..00000000 --- a/include/expr/Parser.h +++ /dev/null @@ -1,237 +0,0 @@ -//===-- Parser.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_PARSER_H -#define KLEE_PARSER_H - -#include "klee/Expr.h" - -#include -#include - -namespace llvm { - class MemoryBuffer; -} - -namespace klee { - class ExprBuilder; - -namespace expr { - // These are the language types we manipulate. - typedef ref ExprHandle; - typedef UpdateList VersionHandle; - - /// Identifier - Wrapper for a uniqued string. - struct Identifier { - const std::string Name; - - public: - Identifier(const std::string _Name) : Name(_Name) {} - }; - - // FIXME: Do we have a use for tracking source locations? - - /// Decl - Base class for top level declarations. - class Decl { - public: - enum DeclKind { - ArrayDeclKind, - ExprVarDeclKind, - VersionVarDeclKind, - QueryCommandDeclKind, - - DeclKindLast = QueryCommandDeclKind, - VarDeclKindFirst = ExprVarDeclKind, - VarDeclKindLast = VersionVarDeclKind, - CommandDeclKindFirst = QueryCommandDeclKind, - CommandDeclKindLast = QueryCommandDeclKind - }; - - private: - DeclKind Kind; - - public: - Decl(DeclKind _Kind); - virtual ~Decl() {} - - /// getKind - Get the decl kind. - DeclKind getKind() const { return Kind; } - - /// dump - Dump the AST node to stderr. - virtual void dump() = 0; - - static bool classof(const Decl *) { return true; } - }; - - /// ArrayDecl - Array declarations. - /// - /// For example: - /// array obj[] : w32 -> w8 = symbolic - /// array obj[32] : w32 -> w8 = [ ... ] - class ArrayDecl : public Decl { - public: - /// Name - The name of this array. - const Identifier *Name; - - /// Domain - The width of indices. - const unsigned Domain; - - /// Range - The width of array contents. - const unsigned Range; - - /// Root - The root array object defined by this decl. - const Array *Root; - - public: - ArrayDecl(const Identifier *_Name, uint64_t _Size, - unsigned _Domain, unsigned _Range, - const Array *_Root) - : Decl(ArrayDeclKind), Name(_Name), - Domain(_Domain), Range(_Range), - Root(_Root) { - } - - virtual void dump(); - - static bool classof(const Decl *D) { - return D->getKind() == Decl::ArrayDeclKind; - } - static bool classof(const ArrayDecl *) { return true; } - }; - - /// VarDecl - Variable declarations, used to associate names to - /// expressions or array versions outside of expressions. - /// - /// For example: - // FIXME: What syntax are we going to use for this? We need it. - class VarDecl : public Decl { - public: - const Identifier *Name; - - static bool classof(const Decl *D) { - return (Decl::VarDeclKindFirst <= D->getKind() && - D->getKind() <= Decl::VarDeclKindLast); - } - static bool classof(const VarDecl *) { return true; } - }; - - /// ExprVarDecl - Expression variable declarations. - class ExprVarDecl : public VarDecl { - public: - ExprHandle Value; - - static bool classof(const Decl *D) { - return D->getKind() == Decl::ExprVarDeclKind; - } - static bool classof(const ExprVarDecl *) { return true; } - }; - - /// VersionVarDecl - Array version variable declarations. - class VersionVarDecl : public VarDecl { - public: - VersionHandle Value; - - static bool classof(const Decl *D) { - return D->getKind() == Decl::VersionVarDeclKind; - } - static bool classof(const VersionVarDecl *) { return true; } - }; - - /// CommandDecl - Base class for language commands. - class CommandDecl : public Decl { - public: - CommandDecl(DeclKind _Kind) : Decl(_Kind) {} - - static bool classof(const Decl *D) { - return (Decl::CommandDeclKindFirst <= D->getKind() && - D->getKind() <= Decl::CommandDeclKindLast); - } - static bool classof(const CommandDecl *) { return true; } - }; - - /// QueryCommand - Query commands. - /// - /// (query [ ... constraints ... ] expression) - /// (query [ ... constraints ... ] expression values) - /// (query [ ... constraints ... ] expression values objects) - class QueryCommand : public CommandDecl { - public: - // FIXME: One issue with STP... should we require the FE to - // guarantee that these are consistent? That is a cornerstone of - // being able to do independence. We may want this as a flag, if - // we are to interface with things like SMT. - - /// Constraints - The list of constraints to assume for this - /// expression. - const std::vector Constraints; - - /// Query - The expression being queried. - ExprHandle Query; - - /// Values - The expressions for which counterexamples should be - /// given if the query is invalid. - const std::vector Values; - - /// Objects - Symbolic arrays whose initial contents should be - /// given if the query is invalid. - const std::vector Objects; - - public: - QueryCommand(const std::vector &_Constraints, - ExprHandle _Query, - const std::vector &_Values, - const std::vector &_Objects - ) - : CommandDecl(QueryCommandDeclKind), - Constraints(_Constraints), - Query(_Query), - Values(_Values), - Objects(_Objects) {} - - virtual void dump(); - - static bool classof(const Decl *D) { - return D->getKind() == QueryCommandDeclKind; - } - static bool classof(const QueryCommand *) { return true; } - }; - - /// Parser - Public interface for parsing a .kquery language file. - class Parser { - protected: - Parser(); - public: - virtual ~Parser(); - - /// SetMaxErrors - Suppress anything beyond the first N errors. - virtual void SetMaxErrors(unsigned N) = 0; - - /// GetNumErrors - Return the number of encountered errors. - virtual unsigned GetNumErrors() const = 0; - - /// ParseTopLevelDecl - Parse and return a top level declaration, - /// which the caller assumes ownership of. - /// - /// \return NULL indicates the end of the file has been reached. - virtual Decl *ParseTopLevelDecl() = 0; - - /// CreateParser - Create a parser implementation for the given - /// MemoryBuffer. - /// - /// \arg Name - The name to use in diagnostic messages. - /// \arg MB - The input data. - /// \arg Builder - The expression builder to use for constructing - /// expressions. - static Parser *Create(const std::string Name, const llvm::MemoryBuffer *MB, - ExprBuilder *Builder, bool ClearArrayAfterQuery); - }; -} -} - -#endif /* KLEE_PARSER_H */ diff --git a/include/klee/Constraints.h b/include/klee/Constraints.h deleted file mode 100644 index 08077293..00000000 --- a/include/klee/Constraints.h +++ /dev/null @@ -1,72 +0,0 @@ -//===-- Constraints.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_CONSTRAINTS_H -#define KLEE_CONSTRAINTS_H - -#include "klee/Expr.h" - -// FIXME: Currently we use ConstraintManager for two things: to pass -// sets of constraints around, and to optimize constraints. We should -// move the first usage into a separate data structure -// (ConstraintSet?) which ConstraintManager could embed if it likes. -namespace klee { - -class ExprVisitor; - -class ConstraintManager { -public: - using constraints_ty = std::vector>; - using iterator = constraints_ty::iterator; - using const_iterator = constraints_ty::const_iterator; - - ConstraintManager() = default; - ConstraintManager(const ConstraintManager &cs) = default; - ConstraintManager &operator=(const ConstraintManager &cs) = default; - ConstraintManager(ConstraintManager &&cs) = default; - ConstraintManager &operator=(ConstraintManager &&cs) = default; - - // create from constraints with no optimization - explicit ConstraintManager(const std::vector> &_constraints) - : constraints(_constraints) {} - - // given a constraint which is known to be valid, attempt to - // simplify the existing constraint set - void simplifyForValidConstraint(ref e); - - ref simplifyExpr(ref e) const; - - void addConstraint(ref e); - - bool empty() const noexcept { return constraints.empty(); } - ref back() const { return constraints.back(); } - const_iterator begin() const { return constraints.cbegin(); } - const_iterator end() const { return constraints.cend(); } - std::size_t size() const noexcept { return constraints.size(); } - - bool operator==(const ConstraintManager &other) const { - return constraints == other.constraints; - } - - bool operator!=(const ConstraintManager &other) const { - return constraints != other.constraints; - } - -private: - std::vector> constraints; - - // returns true iff the constraints were modified - bool rewriteConstraints(ExprVisitor &visitor); - - void addConstraintInternal(ref e); -}; - -} // namespace klee - -#endif /* KLEE_CONSTRAINTS_H */ diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h index e2c6bffe..891e6f06 100644 --- a/include/klee/ExecutionState.h +++ b/include/klee/ExecutionState.h @@ -10,8 +10,8 @@ #ifndef KLEE_EXECUTIONSTATE_H #define KLEE_EXECUTIONSTATE_H -#include "klee/Constraints.h" -#include "klee/Expr.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" #include "klee/Internal/ADT/TreeStream.h" #include "klee/Internal/System/Time.h" #include "klee/MergeHandler.h" diff --git a/include/klee/Expr.h b/include/klee/Expr.h deleted file mode 100644 index d4e4f7fa..00000000 --- a/include/klee/Expr.h +++ /dev/null @@ -1,1174 +0,0 @@ -//===-- Expr.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_EXPR_H -#define KLEE_EXPR_H - -#include "klee/util/Bits.h" -#include "klee/util/Ref.h" - -#include "llvm/ADT/APFloat.h" -#include "llvm/ADT/APInt.h" -#include "llvm/ADT/DenseSet.h" -#include "llvm/ADT/SmallVector.h" -#include "llvm/Support/CommandLine.h" -#include "llvm/Support/raw_ostream.h" - -#include -#include -#include -#include - -namespace llvm { - class Type; - class raw_ostream; -} - -namespace klee { - -class Array; -class ArrayCache; -class ConstantExpr; -class ObjectState; - -template class ref; - -extern llvm::cl::OptionCategory ExprCat; - -/// Class representing symbolic expressions. -/** - -Expression canonicalization: we define certain rules for -canonicalization rules for Exprs in order to simplify code that -pattern matches Exprs (since the number of forms are reduced), to open -up further chances for optimization, and to increase similarity for -caching and other purposes. - -The general rules are: -
    -
  1. No Expr has all constant arguments.
    2. - -
  2. Booleans: -
      -
    1. \c Ne, \c Ugt, \c Uge, \c Sgt, \c Sge are not used
      2. -
    2. The only acceptable operations with boolean arguments are - \c Not \c And, \c Or, \c Xor, \c Eq, - as well as \c SExt, \c ZExt, - \c Select and \c NotOptimized.
      3. -
    3. The only boolean operation which may involve a constant is boolean not (== false).
      4. -
    -
    3. - -
  3. Linear Formulas: -
      -
    1. For any subtree representing a linear formula, a constant - term must be on the LHS of the root node of the subtree. In particular, - in a BinaryExpr a constant must always be on the LHS. For example, subtraction - by a constant c is written as add(-c, ?).
      2. -
    -
    4. - - -
  4. Chains are unbalanced to the right
    5. - -
- - -Steps required for adding an expr: - -# Add case to printKind - -# Add to ExprVisitor - -# Add to IVC (implied value concretization) if possible - -Todo: Shouldn't bool \c Xor just be written as not equal? - -*/ - -class Expr { -public: - static unsigned count; - static const unsigned MAGIC_HASH_CONSTANT = 39; - - /// The type of an expression is simply its width, in bits. - typedef unsigned Width; - - static const Width InvalidWidth = 0; - static const Width Bool = 1; - static const Width Int8 = 8; - static const Width Int16 = 16; - static const Width Int32 = 32; - static const Width Int64 = 64; - static const Width Fl80 = 80; - - - enum Kind { - InvalidKind = -1, - - // Primitive - - Constant = 0, - - // Special - - /// Prevents optimization below the given expression. Used for - /// testing: make equality constraints that KLEE will not use to - /// optimize to concretes. - NotOptimized, - - //// Skip old varexpr, just for deserialization, purge at some point - Read=NotOptimized+2, - Select, - Concat, - Extract, - - // Casting, - ZExt, - SExt, - - // Bit - Not, - - // All subsequent kinds are binary. - - // Arithmetic - Add, - Sub, - Mul, - UDiv, - SDiv, - URem, - SRem, - - // Bit - And, - Or, - Xor, - Shl, - LShr, - AShr, - - // Compare - Eq, - Ne, ///< Not used in canonical form - Ult, - Ule, - Ugt, ///< Not used in canonical form - Uge, ///< Not used in canonical form - Slt, - Sle, - Sgt, ///< Not used in canonical form - Sge, ///< Not used in canonical form - - LastKind=Sge, - - CastKindFirst=ZExt, - CastKindLast=SExt, - BinaryKindFirst=Add, - BinaryKindLast=Sge, - CmpKindFirst=Eq, - CmpKindLast=Sge - }; - - unsigned refCount; - -protected: - unsigned hashValue; - - /// Compares `b` to `this` Expr and determines how they are ordered - /// (ignoring their kid expressions - i.e. those returned by `getKid()`). - /// - /// Typically this requires comparing internal attributes of the Expr. - /// - /// Implementations can assume that `b` and `this` are of the same kind. - /// - /// This method effectively defines a partial order over Expr of the same - /// kind (partial because kid Expr are not compared). - /// - /// This method should not be called directly. Instead `compare()` should - /// be used. - /// - /// \param [in] b Expr to compare `this` to. - /// - /// \return One of the following values: - /// - /// * -1 if `this` is `<` `b` ignoring kid expressions. - /// * 1 if `this` is `>` `b` ignoring kid expressions. - /// * 0 if `this` and `b` are not ordered. - /// - /// `<` and `>` are binary relations that express the partial order. - virtual int compareContents(const Expr &b) const = 0; - -public: - Expr() : refCount(0) { Expr::count++; } - virtual ~Expr() { Expr::count--; } - - virtual Kind getKind() const = 0; - virtual Width getWidth() const = 0; - - virtual unsigned getNumKids() const = 0; - virtual ref getKid(unsigned i) const = 0; - - virtual void print(llvm::raw_ostream &os) const; - - /// dump - Print the expression to stderr. - void dump() const; - - /// Returns the pre-computed hash of the current expression - virtual unsigned hash() const { return hashValue; } - - /// (Re)computes the hash of the current expression. - /// Returns the hash value. - virtual unsigned computeHash(); - - /// Compares `b` to `this` Expr for structural equivalence. - /// - /// This method effectively defines a total order over all Expr. - /// - /// \param [in] b Expr to compare `this` to. - /// - /// \return One of the following values: - /// - /// * -1 iff `this` is `<` `b` - /// * 0 iff `this` is structurally equivalent to `b` - /// * 1 iff `this` is `>` `b` - /// - /// `<` and `>` are binary relations that express the total order. - int compare(const Expr &b) const; - - // Given an array of new kids return a copy of the expression - // but using those children. - virtual ref rebuild(ref kids[/* getNumKids() */]) const = 0; - - /// isZero - Is this a constant zero. - bool isZero() const; - - /// isTrue - Is this the true expression. - bool isTrue() const; - - /// isFalse - Is this the false expression. - bool isFalse() const; - - /* Static utility methods */ - - 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) { - return (w + 7) / 8; - } - - /* Kind utilities */ - - /* Utility creation functions */ - static ref createSExtToPointerWidth(ref e); - static ref createZExtToPointerWidth(ref e); - static ref createImplies(ref hyp, ref conc); - static ref createIsZero(ref e); - - /// Create a little endian read of the given type at offset 0 of the - /// given object. - static ref createTempRead(const Array *array, Expr::Width w); - - static ref createPointer(uint64_t v); - - struct CreateArg; - static ref createFromKind(Kind k, std::vector args); - - static bool isValidKidWidth(unsigned kid, Width w) { return true; } - static bool needsResultType() { return false; } - - static bool classof(const Expr *) { return true; } - -private: - typedef llvm::DenseSet > ExprEquivSet; - int compare(const Expr &b, ExprEquivSet &equivs) const; -}; - -struct Expr::CreateArg { - ref expr; - Width width; - - CreateArg(Width w = Bool) : expr(0), width(w) {} - CreateArg(ref e) : expr(e), width(Expr::InvalidWidth) {} - - bool isExpr() { return !isWidth(); } - bool isWidth() { return width != Expr::InvalidWidth; } -}; - -// Comparison operators - -inline bool operator==(const Expr &lhs, const Expr &rhs) { - return lhs.compare(rhs) == 0; -} - -inline bool operator<(const Expr &lhs, const Expr &rhs) { - return lhs.compare(rhs) < 0; -} - -inline bool operator!=(const Expr &lhs, const Expr &rhs) { - return !(lhs == rhs); -} - -inline bool operator>(const Expr &lhs, const Expr &rhs) { - return rhs < lhs; -} - -inline bool operator<=(const Expr &lhs, const Expr &rhs) { - return !(lhs > rhs); -} - -inline bool operator>=(const Expr &lhs, const Expr &rhs) { - return !(lhs < rhs); -} - -// Printing operators - -inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const Expr &e) { - e.print(os); - return os; -} - -inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const Expr::Kind kind) { - Expr::printKind(os, kind); - return os; -} - -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; -} - -// Utility classes - -class NonConstantExpr : public Expr { -public: - static bool classof(const Expr *E) { - return E->getKind() != Expr::Constant; - } - static bool classof(const NonConstantExpr *) { return true; } -}; - -class BinaryExpr : public NonConstantExpr { -public: - ref left, right; - -public: - unsigned getNumKids() const { return 2; } - ref getKid(unsigned i) const { - if(i == 0) - return left; - if(i == 1) - return right; - return 0; - } - -protected: - BinaryExpr(const ref &l, const ref &r) : left(l), right(r) {} - -public: - static bool classof(const Expr *E) { - Kind k = E->getKind(); - return Expr::BinaryKindFirst <= k && k <= Expr::BinaryKindLast; - } - static bool classof(const BinaryExpr *) { return true; } -}; - - -class CmpExpr : public BinaryExpr { - -protected: - CmpExpr(ref l, ref r) : BinaryExpr(l,r) {} - -public: - Width getWidth() const { return Bool; } - - static bool classof(const Expr *E) { - Kind k = E->getKind(); - return Expr::CmpKindFirst <= k && k <= Expr::CmpKindLast; - } - static bool classof(const CmpExpr *) { return true; } -}; - -// Special - -class NotOptimizedExpr : public NonConstantExpr { -public: - static const Kind kind = NotOptimized; - static const unsigned numKids = 1; - ref src; - - static ref alloc(const ref &src) { - ref r(new NotOptimizedExpr(src)); - r->computeHash(); - return r; - } - - static ref create(ref src); - - Width getWidth() const { return src->getWidth(); } - Kind getKind() const { return NotOptimized; } - - unsigned getNumKids() const { return 1; } - ref getKid(unsigned i) const { return src; } - - virtual ref rebuild(ref kids[]) const { return create(kids[0]); } - -private: - NotOptimizedExpr(const ref &_src) : src(_src) {} - -protected: - virtual int compareContents(const Expr &b) const { - // No attributes to compare. - return 0; - } - -public: - static bool classof(const Expr *E) { - return E->getKind() == Expr::NotOptimized; - } - static bool classof(const NotOptimizedExpr *) { return true; } -}; - - -/// Class representing a byte update of an array. -class UpdateNode { - friend class UpdateList; - - mutable unsigned refCount; - // cache instead of recalc - unsigned hashValue; - -public: - const UpdateNode *next; - ref index, value; - -private: - /// size of this update sequence, including this update - unsigned size; - -public: - UpdateNode(const UpdateNode *_next, - const ref &_index, - const ref &_value); - - unsigned getSize() const { return size; } - - int compare(const UpdateNode &b) const; - unsigned hash() const { return hashValue; } - -private: - UpdateNode() : refCount(0) {} - ~UpdateNode(); - - unsigned computeHash(); -}; - -class Array { -public: - // Name of the array - const std::string name; - - // FIXME: Not 64-bit clean. - const unsigned size; - - /// Domain is how many bits can be used to access the array [32 bits] - /// Range is the size (in bits) of the number stored there (array of bytes -> 8) - const Expr::Width domain, range; - - /// constantValues - The constant initial values for this array, or empty for - /// a symbolic array. If non-empty, this size of this array is equivalent to - /// the array size. - const std::vector > constantValues; - -private: - unsigned hashValue; - - // FIXME: Make =delete when we switch to C++11 - Array(const Array& array); - - // FIXME: Make =delete when we switch to C++11 - Array& operator =(const Array& array); - - ~Array(); - - /// Array - Construct a new array object. - /// - /// \param _name - The name for this array. Names should generally be unique - /// across an application, but this is not necessary for correctness, except - /// when printing expressions. When expressions are printed the output will - /// not parse correctly since two arrays with the same name cannot be - /// distinguished once printed. - Array(const std::string &_name, uint64_t _size, - const ref *constantValuesBegin = 0, - const ref *constantValuesEnd = 0, - Expr::Width _domain = Expr::Int32, Expr::Width _range = Expr::Int8); - -public: - bool isSymbolicArray() const { return constantValues.empty(); } - bool isConstantArray() const { return !isSymbolicArray(); } - - const std::string getName() const { return name; } - unsigned getSize() const { return size; } - Expr::Width getDomain() const { return domain; } - Expr::Width getRange() const { return range; } - - /// ComputeHash must take into account the name, the size, the domain, and the range - unsigned computeHash(); - unsigned hash() const { return hashValue; } - friend class ArrayCache; -}; - -/// Class representing a complete list of updates into an array. -class UpdateList { - friend class ReadExpr; // for default constructor - -public: - const Array *root; - - /// pointer to the most recent update node - const UpdateNode *head; - -public: - UpdateList(const Array *_root, const UpdateNode *_head); - UpdateList(const UpdateList &b); - ~UpdateList(); - - UpdateList &operator=(const UpdateList &b); - - /// size of this update list - unsigned getSize() const { return (head ? head->getSize() : 0); } - - void extend(const ref &index, const ref &value); - - int compare(const UpdateList &b) const; - unsigned hash() const; -private: - void tryFreeNodes(); -}; - -/// Class representing a one byte read from an array. -class ReadExpr : public NonConstantExpr { -public: - static const Kind kind = Read; - static const unsigned numKids = 1; - -public: - UpdateList updates; - ref index; - -public: - static ref alloc(const UpdateList &updates, const ref &index) { - ref r(new ReadExpr(updates, index)); - r->computeHash(); - return r; - } - - static ref create(const UpdateList &updates, ref i); - - Width getWidth() const { assert(updates.root); return updates.root->getRange(); } - Kind getKind() const { return Read; } - - unsigned getNumKids() const { return numKids; } - ref getKid(unsigned i) const { return !i ? index : 0; } - - int compareContents(const Expr &b) const; - - virtual ref rebuild(ref kids[]) const { - return create(updates, kids[0]); - } - - virtual unsigned computeHash(); - -private: - ReadExpr(const UpdateList &_updates, const ref &_index) : - updates(_updates), index(_index) { assert(updates.root); } - -public: - static bool classof(const Expr *E) { - return E->getKind() == Expr::Read; - } - static bool classof(const ReadExpr *) { return true; } -}; - - -/// Class representing an if-then-else expression. -class SelectExpr : public NonConstantExpr { -public: - static const Kind kind = Select; - static const unsigned numKids = 3; - -public: - ref cond, trueExpr, falseExpr; - -public: - static ref alloc(const ref &c, const ref &t, - const ref &f) { - ref r(new SelectExpr(c, t, f)); - r->computeHash(); - return r; - } - - static ref create(ref c, ref t, ref f); - - Width getWidth() const { return trueExpr->getWidth(); } - Kind getKind() const { return Select; } - - unsigned getNumKids() const { return numKids; } - ref getKid(unsigned i) const { - switch(i) { - case 0: return cond; - case 1: return trueExpr; - case 2: return falseExpr; - default: return 0; - } - } - - static bool isValidKidWidth(unsigned kid, Width w) { - if (kid == 0) - return w == Bool; - else - return true; - } - - virtual ref rebuild(ref kids[]) const { - return create(kids[0], kids[1], kids[2]); - } - -private: - SelectExpr(const ref &c, const ref &t, const ref &f) - : cond(c), trueExpr(t), falseExpr(f) {} - -public: - static bool classof(const Expr *E) { - return E->getKind() == Expr::Select; - } - static bool classof(const SelectExpr *) { return true; } - -protected: - virtual int compareContents(const Expr &b) const { - // No attributes to compare. - return 0; - } -}; - - -/** Children of a concat expression can have arbitrary widths. - Kid 0 is the left kid, kid 1 is the right kid. -*/ -class ConcatExpr : public NonConstantExpr { -public: - static const Kind kind = Concat; - static const unsigned numKids = 2; - -private: - Width width; - ref left, right; - -public: - static ref alloc(const ref &l, const ref &r) { - ref c(new ConcatExpr(l, r)); - c->computeHash(); - return c; - } - - static ref create(const ref &l, const ref &r); - - Width getWidth() const { return width; } - Kind getKind() const { return kind; } - ref getLeft() const { return left; } - ref getRight() const { return right; } - - unsigned getNumKids() const { return numKids; } - ref getKid(unsigned i) const { - if (i == 0) return left; - else if (i == 1) return right; - else return NULL; - } - - /// Shortcuts to create larger concats. The chain returned is unbalanced to the right - static ref createN(unsigned nKids, const ref kids[]); - static ref create4(const ref &kid1, const ref &kid2, - const ref &kid3, const ref &kid4); - static ref create8(const ref &kid1, const ref &kid2, - const ref &kid3, const ref &kid4, - const ref &kid5, const ref &kid6, - const ref &kid7, const ref &kid8); - - virtual ref rebuild(ref kids[]) const { return create(kids[0], kids[1]); } - -private: - ConcatExpr(const ref &l, const ref &r) : left(l), right(r) { - width = l->getWidth() + r->getWidth(); - } - -public: - static bool classof(const Expr *E) { - return E->getKind() == Expr::Concat; - } - static bool classof(const ConcatExpr *) { return true; } - -protected: - virtual int compareContents(const Expr &b) const { - const ConcatExpr &eb = static_cast(b); - if (width != eb.width) - return width < eb.width ? -1 : 1; - return 0; - } -}; - - -/** This class represents an extract from expression {\tt expr}, at - bit offset {\tt offset} of width {\tt width}. Bit 0 is the right most - bit of the expression. - */ -class ExtractExpr : public NonConstantExpr { -public: - static const Kind kind = Extract; - static const unsigned numKids = 1; - -public: - ref expr; - unsigned offset; - Width width; - -public: - static ref alloc(const ref &e, unsigned o, Width w) { - ref r(new ExtractExpr(e, o, w)); - r->computeHash(); - return r; - } - - /// Creates an ExtractExpr with the given bit offset and width - static ref create(ref e, unsigned bitOff, Width w); - - Width getWidth() const { return width; } - Kind getKind() const { return Extract; } - - unsigned getNumKids() const { return numKids; } - ref getKid(unsigned i) const { return expr; } - - int compareContents(const Expr &b) const { - const ExtractExpr &eb = static_cast(b); - if (offset != eb.offset) return offset < eb.offset ? -1 : 1; - if (width != eb.width) return width < eb.width ? -1 : 1; - return 0; - } - - virtual ref rebuild(ref kids[]) const { - return create(kids[0], offset, width); - } - - virtual unsigned computeHash(); - -private: - ExtractExpr(const ref &e, unsigned b, Width w) - : expr(e),offset(b),width(w) {} - -public: - static bool classof(const Expr *E) { - return E->getKind() == Expr::Extract; - } - static bool classof(const ExtractExpr *) { return true; } -}; - - -/** - Bitwise Not -*/ -class NotExpr : public NonConstantExpr { -public: - static const Kind kind = Not; - static const unsigned numKids = 1; - - ref expr; - -public: - static ref alloc(const ref &e) { - ref r(new NotExpr(e)); - r->computeHash(); - return r; - } - - static ref create(const ref &e); - - Width getWidth() const { return expr->getWidth(); } - Kind getKind() const { return Not; } - - unsigned getNumKids() const { return numKids; } - ref getKid(unsigned i) const { return expr; } - - virtual ref rebuild(ref kids[]) const { - return create(kids[0]); - } - - virtual unsigned computeHash(); - -public: - static bool classof(const Expr *E) { - return E->getKind() == Expr::Not; - } - static bool classof(const NotExpr *) { return true; } - -private: - NotExpr(const ref &e) : expr(e) {} - -protected: - virtual int compareContents(const Expr &b) const { - // No attributes to compare. - return 0; - } -}; - - - -// Casting - -class CastExpr : public NonConstantExpr { -public: - ref src; - Width width; - -public: - CastExpr(const ref &e, Width w) : src(e), width(w) {} - - Width getWidth() const { return width; } - - unsigned getNumKids() const { return 1; } - ref getKid(unsigned i) const { return (i==0) ? src : 0; } - - static bool needsResultType() { return true; } - - int compareContents(const Expr &b) const { - const CastExpr &eb = static_cast(b); - if (width != eb.width) return width < eb.width ? -1 : 1; - return 0; - } - - virtual unsigned computeHash(); - - static bool classof(const Expr *E) { - Expr::Kind k = E->getKind(); - return Expr::CastKindFirst <= k && k <= Expr::CastKindLast; - } - static bool classof(const CastExpr *) { return true; } -}; - -#define CAST_EXPR_CLASS(_class_kind) \ -class _class_kind ## Expr : public CastExpr { \ -public: \ - static const Kind kind = _class_kind; \ - static const unsigned numKids = 1; \ -public: \ - _class_kind ## Expr(ref e, Width w) : CastExpr(e,w) {} \ - static ref alloc(const ref &e, Width w) { \ - ref r(new _class_kind ## Expr(e, w)); \ - r->computeHash(); \ - return r; \ - } \ - static ref create(const ref &e, Width w); \ - Kind getKind() const { return _class_kind; } \ - virtual ref rebuild(ref kids[]) const { \ - return create(kids[0], width); \ - } \ - \ - static bool classof(const Expr *E) { \ - return E->getKind() == Expr::_class_kind; \ - } \ - static bool classof(const _class_kind ## Expr *) { \ - return true; \ - } \ -}; \ - -CAST_EXPR_CLASS(SExt) -CAST_EXPR_CLASS(ZExt) - -// Arithmetic/Bit Exprs - -#define ARITHMETIC_EXPR_CLASS(_class_kind) \ - class _class_kind##Expr : public BinaryExpr { \ - public: \ - static const Kind kind = _class_kind; \ - static const unsigned numKids = 2; \ - \ - public: \ - _class_kind##Expr(const ref &l, const ref &r) \ - : BinaryExpr(l, r) {} \ - static ref alloc(const ref &l, const ref &r) { \ - ref res(new _class_kind##Expr(l, r)); \ - res->computeHash(); \ - return res; \ - } \ - static ref create(const ref &l, const ref &r); \ - Width getWidth() const { return left->getWidth(); } \ - Kind getKind() const { return _class_kind; } \ - virtual ref rebuild(ref kids[]) const { \ - return create(kids[0], kids[1]); \ - } \ - \ - static bool classof(const Expr *E) { \ - return E->getKind() == Expr::_class_kind; \ - } \ - static bool classof(const _class_kind##Expr *) { return true; } \ - \ - protected: \ - virtual int compareContents(const Expr &b) const { \ - /* No attributes to compare.*/ \ - return 0; \ - } \ - }; - -ARITHMETIC_EXPR_CLASS(Add) -ARITHMETIC_EXPR_CLASS(Sub) -ARITHMETIC_EXPR_CLASS(Mul) -ARITHMETIC_EXPR_CLASS(UDiv) -ARITHMETIC_EXPR_CLASS(SDiv) -ARITHMETIC_EXPR_CLASS(URem) -ARITHMETIC_EXPR_CLASS(SRem) -ARITHMETIC_EXPR_CLASS(And) -ARITHMETIC_EXPR_CLASS(Or) -ARITHMETIC_EXPR_CLASS(Xor) -ARITHMETIC_EXPR_CLASS(Shl) -ARITHMETIC_EXPR_CLASS(LShr) -ARITHMETIC_EXPR_CLASS(AShr) - -// Comparison Exprs - -#define COMPARISON_EXPR_CLASS(_class_kind) \ - class _class_kind##Expr : public CmpExpr { \ - public: \ - static const Kind kind = _class_kind; \ - static const unsigned numKids = 2; \ - \ - public: \ - _class_kind##Expr(const ref &l, const ref &r) \ - : CmpExpr(l, r) {} \ - static ref alloc(const ref &l, const ref &r) { \ - ref res(new _class_kind##Expr(l, r)); \ - res->computeHash(); \ - return res; \ - } \ - static ref create(const ref &l, const ref &r); \ - Kind getKind() const { return _class_kind; } \ - virtual ref rebuild(ref kids[]) const { \ - return create(kids[0], kids[1]); \ - } \ - \ - static bool classof(const Expr *E) { \ - return E->getKind() == Expr::_class_kind; \ - } \ - static bool classof(const _class_kind##Expr *) { return true; } \ - \ - protected: \ - virtual int compareContents(const Expr &b) const { \ - /* No attributes to compare. */ \ - return 0; \ - } \ - }; - -COMPARISON_EXPR_CLASS(Eq) -COMPARISON_EXPR_CLASS(Ne) -COMPARISON_EXPR_CLASS(Ult) -COMPARISON_EXPR_CLASS(Ule) -COMPARISON_EXPR_CLASS(Ugt) -COMPARISON_EXPR_CLASS(Uge) -COMPARISON_EXPR_CLASS(Slt) -COMPARISON_EXPR_CLASS(Sle) -COMPARISON_EXPR_CLASS(Sgt) -COMPARISON_EXPR_CLASS(Sge) - -// Terminal Exprs - -class ConstantExpr : public Expr { -public: - static const Kind kind = Constant; - static const unsigned numKids = 0; - -private: - llvm::APInt value; - - ConstantExpr(const llvm::APInt &v) : value(v) {} - -public: - ~ConstantExpr() {} - - Width getWidth() const { return value.getBitWidth(); } - Kind getKind() const { return Constant; } - - unsigned getNumKids() const { return 0; } - ref getKid(unsigned i) const { return 0; } - - /// getAPValue - Return the arbitrary precision value directly. - /// - /// Clients should generally not use the APInt value directly and instead use - /// native ConstantExpr APIs. - const llvm::APInt &getAPValue() const { return value; } - - /// getZExtValue - Returns the constant value zero extended to the - /// return type of this method. - /// - ///\param bits - optional parameter that can be used to check that the - /// number of bits used by this constant is <= to the parameter - /// value. This is useful for checking that type casts won't truncate - /// useful bits. - /// - /// Example: unit8_t byte= (unit8_t) constant->getZExtValue(8); - uint64_t getZExtValue(unsigned bits = 64) const { - assert(getWidth() <= bits && "Value may be out of range!"); - return value.getZExtValue(); - } - - /// getLimitedValue - If this value is smaller than the specified limit, - /// return it, otherwise return the limit value. - uint64_t getLimitedValue(uint64_t Limit = ~0ULL) const { - return value.getLimitedValue(Limit); - } - - /// toString - Return the constant value as a string - /// \param Res specifies the string for the result to be placed in - /// \param radix specifies the base (e.g. 2,10,16). The default is base 10 - void toString(std::string &Res, unsigned radix = 10) const; - - int compareContents(const Expr &b) const { - const ConstantExpr &cb = static_cast(b); - if (getWidth() != cb.getWidth()) - return getWidth() < cb.getWidth() ? -1 : 1; - if (value == cb.value) - return 0; - return value.ult(cb.value) ? -1 : 1; - } - - virtual ref rebuild(ref kids[]) const { - assert(0 && "rebuild() on ConstantExpr"); - return const_cast(this); - } - - virtual unsigned computeHash(); - - static ref fromMemory(void *address, Width w); - void toMemory(void *address); - - static ref alloc(const llvm::APInt &v) { - ref r(new ConstantExpr(v)); - r->computeHash(); - return r; - } - - static ref alloc(const llvm::APFloat &f) { - return alloc(f.bitcastToAPInt()); - } - - static ref alloc(uint64_t v, Width w) { - return alloc(llvm::APInt(w, v)); - } - - static ref create(uint64_t v, Width w) { -#ifndef NDEBUG - if (w <= 64) - assert(v == bits64::truncateToNBits(v, w) && "invalid constant"); -#endif - return alloc(v, w); - } - - static bool classof(const Expr *E) { return E->getKind() == Expr::Constant; } - static bool classof(const ConstantExpr *) { return true; } - - /* Utility Functions */ - - /// isZero - Is this a constant zero. - bool isZero() const { return getAPValue().isMinValue(); } - - /// isOne - Is this a constant one. - bool isOne() const { return getLimitedValue() == 1; } - - /// isTrue - Is this the true expression. - bool isTrue() const { - return (getWidth() == Expr::Bool && value.getBoolValue() == true); - } - - /// isFalse - Is this the false expression. - bool isFalse() const { - return (getWidth() == Expr::Bool && value.getBoolValue() == false); - } - - /// isAllOnes - Is this constant all ones. - bool isAllOnes() const { return getAPValue().isAllOnesValue(); } - - /* Constant Operations */ - - ref Concat(const ref &RHS); - ref Extract(unsigned offset, Width W); - ref ZExt(Width W); - ref SExt(Width W); - ref Add(const ref &RHS); - ref Sub(const ref &RHS); - ref Mul(const ref &RHS); - ref UDiv(const ref &RHS); - ref SDiv(const ref &RHS); - ref URem(const ref &RHS); - ref SRem(const ref &RHS); - ref And(const ref &RHS); - ref Or(const ref &RHS); - ref Xor(const ref &RHS); - ref Shl(const ref &RHS); - ref LShr(const ref &RHS); - ref AShr(const ref &RHS); - - // Comparisons return a constant expression of width 1. - - ref Eq(const ref &RHS); - ref Ne(const ref &RHS); - ref Ult(const ref &RHS); - ref Ule(const ref &RHS); - ref Ugt(const ref &RHS); - ref Uge(const ref &RHS); - ref Slt(const ref &RHS); - ref Sle(const ref &RHS); - ref Sgt(const ref &RHS); - ref Sge(const ref &RHS); - - ref Neg(); - ref Not(); -}; - -// Implementations - -inline bool Expr::isZero() const { - if (const ConstantExpr *CE = dyn_cast(this)) - return CE->isZero(); - return false; -} - -inline bool Expr::isTrue() const { - assert(getWidth() == Expr::Bool && "Invalid isTrue() call!"); - if (const ConstantExpr *CE = dyn_cast(this)) - return CE->isTrue(); - return false; -} - -inline bool Expr::isFalse() const { - assert(getWidth() == Expr::Bool && "Invalid isFalse() call!"); - if (const ConstantExpr *CE = dyn_cast(this)) - return CE->isFalse(); - return false; -} - -} // End klee namespace - -#endif /* KLEE_EXPR_H */ diff --git a/include/klee/Expr/ArrayCache.h b/include/klee/Expr/ArrayCache.h new file mode 100644 index 00000000..09eddf49 --- /dev/null +++ b/include/klee/Expr/ArrayCache.h @@ -0,0 +1,81 @@ +//===-- ArrayCache.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_ARRAYCACHE_H +#define KLEE_ARRAYCACHE_H + +#include "klee/Expr/Expr.h" +#include "klee/Expr/ArrayExprHash.h" // For klee::ArrayHashFn + +// FIXME: Remove this hack when we switch to C++11 +#ifdef _LIBCPP_VERSION +#include +#define unordered_set std::unordered_set +#else +#include +#define unordered_set std::tr1::unordered_set +#endif + +#include +#include + +namespace klee { + +struct EquivArrayCmpFn { + bool operator()(const Array *array1, const Array *array2) const { + if (array1 == NULL || array2 == NULL) + return false; + return (array1->size == array2->size) && (array1->name == array2->name); + } +}; + +/// Provides an interface for creating and destroying Array objects. +class ArrayCache { +public: + ArrayCache() {} + ~ArrayCache(); + /// Create an Array object. + // + /// Symbolic Arrays are cached so that only one instance exists. This + /// provides a limited form of "alpha-renaming". Constant arrays are not + /// cached. + /// + /// This class retains ownership of Array object so that upon destruction + /// of this object all allocated Array objects are deleted. + /// + /// \param _name The name of the array + /// \param _size The size of the array in bytes + /// \param constantValuesBegin A pointer to the beginning of a block of + // memory that constains a ``ref`` (i.e. concrete values + // for the //array). This should be NULL for symbolic arrays. + /// for symbolic arrays. + /// \param constantValuesEnd A pointer +1 pass the end of a block of memory + /// that contains a ``ref``. This should be NULL for a + /// symbolic array. + /// \param _domain The size of the domain (i.e. the bitvector used to index + /// the array) + /// \param _range The size of range (i.e. the bitvector that is indexed to) + const Array *CreateArray(const std::string &_name, uint64_t _size, + const ref *constantValuesBegin = 0, + const ref *constantValuesEnd = 0, + Expr::Width _domain = Expr::Int32, + Expr::Width _range = Expr::Int8); + +private: + typedef unordered_set ArrayHashMap; + ArrayHashMap cachedSymbolicArrays; + typedef std::vector ArrayPtrVec; + ArrayPtrVec concreteArrays; +}; +} + +#undef unordered_set + +#endif /* KLEE_ARRAYCACHE_H */ diff --git a/include/klee/Expr/ArrayExprHash.h b/include/klee/Expr/ArrayExprHash.h new file mode 100644 index 00000000..04660fe0 --- /dev/null +++ b/include/klee/Expr/ArrayExprHash.h @@ -0,0 +1,139 @@ +//===-- ArrayExprHash.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_ARRAYEXPRHASH_H +#define KLEE_ARRAYEXPRHASH_H + +#include "klee/Expr/Expr.h" +#include "klee/TimerStatIncrementer.h" +#include "klee/SolverStats.h" + +#include + +#include + +namespace klee { + +struct ArrayHashFn { + unsigned operator()(const Array* array) const { + return(array ? array->hash() : 0); + } +}; + +struct ArrayCmpFn { + bool operator()(const Array* array1, const Array* array2) const { + return(array1 == array2); + } +}; + +struct UpdateNodeHashFn { + unsigned operator()(const UpdateNode* un) const { + return(un ? un->hash() : 0); + } +}; + +struct UpdateNodeCmpFn { + bool operator()(const UpdateNode* un1, const UpdateNode* un2) const { + return(un1 == un2); + } +}; + +template +class ArrayExprHash { +public: + + ArrayExprHash() {}; + // Note: Extend the class and overload the destructor if the objects of type T + // that are to be hashed need to be explicitly destroyed + // As an example, see class STPArrayExprHash + virtual ~ArrayExprHash() {}; + + bool lookupArrayExpr(const Array* array, T& exp) const; + void hashArrayExpr(const Array* array, T& exp); + + bool lookupUpdateNodeExpr(const UpdateNode* un, T& exp) const; + void hashUpdateNodeExpr(const UpdateNode* un, T& exp); + +protected: + typedef std::unordered_map ArrayHash; + typedef typename ArrayHash::iterator ArrayHashIter; + typedef typename ArrayHash::const_iterator ArrayHashConstIter; + + typedef std::unordered_map UpdateNodeHash; + typedef typename UpdateNodeHash::iterator UpdateNodeHashIter; + typedef typename UpdateNodeHash::const_iterator UpdateNodeHashConstIter; + + ArrayHash _array_hash; + UpdateNodeHash _update_node_hash; +}; + + +template +bool ArrayExprHash::lookupArrayExpr(const Array* array, T& exp) const { + bool res = false; + +#ifdef KLEE_ARRAY_DEBUG + TimerStatIncrementer t(stats::arrayHashTime); +#endif + + assert(array); + ArrayHashConstIter it = _array_hash.find(array); + if (it != _array_hash.end()) { + exp = it->second; + res = true; + } + return res; +} + +template +void ArrayExprHash::hashArrayExpr(const Array* array, T& exp) { + +#ifdef KLEE_ARRAY_DEBUG + TimerStatIncrementer t(stats::arrayHashTime); +#endif + + assert(array); + _array_hash[array] = exp; +} + +template +bool ArrayExprHash::lookupUpdateNodeExpr(const UpdateNode* un, T& exp) const +{ + bool res = false; + +#ifdef KLEE_ARRAY_DEBUG + TimerStatIncrementer t(stats::arrayHashTime); +#endif + + assert(un); + UpdateNodeHashConstIter it = _update_node_hash.find(un); + if (it != _update_node_hash.end()) { + exp = it->second; + res = true; + } + return res; +} + +template +void ArrayExprHash::hashUpdateNodeExpr(const UpdateNode* un, T& exp) +{ +#ifdef KLEE_ARRAY_DEBUG + TimerStatIncrementer t(stats::arrayHashTime); +#endif + + assert(un); + _update_node_hash[un] = exp; +} + +} + +#undef unordered_map +#undef unordered_set + +#endif /* KLEE_ARRAYEXPRHASH_H */ diff --git a/include/klee/Expr/Assignment.h b/include/klee/Expr/Assignment.h new file mode 100644 index 00000000..ead459a9 --- /dev/null +++ b/include/klee/Expr/Assignment.h @@ -0,0 +1,99 @@ +//===-- Assignment.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_ASSIGNMENT_H +#define KLEE_ASSIGNMENT_H + +#include "klee/Expr/ExprEvaluator.h" + +#include + +namespace klee { + class Array; + + class Assignment { + public: + typedef std::map > bindings_ty; + + bool allowFreeValues; + bindings_ty bindings; + + public: + Assignment(bool _allowFreeValues=false) + : allowFreeValues(_allowFreeValues) {} + Assignment(const std::vector &objects, + std::vector< std::vector > &values, + bool _allowFreeValues=false) + : allowFreeValues(_allowFreeValues){ + std::vector< std::vector >::iterator valIt = + values.begin(); + for (std::vector::const_iterator it = objects.begin(), + ie = objects.end(); it != ie; ++it) { + const Array *os = *it; + std::vector &arr = *valIt; + bindings.insert(std::make_pair(os, arr)); + ++valIt; + } + } + + ref evaluate(const Array *mo, unsigned index) const; + ref evaluate(ref e); + void createConstraintsFromAssignment(std::vector > &out) const; + + template + bool satisfies(InputIterator begin, InputIterator end); + void dump(); + }; + + class AssignmentEvaluator : public ExprEvaluator { + const Assignment &a; + + protected: + ref getInitialValue(const Array &mo, unsigned index) { + return a.evaluate(&mo, index); + } + + public: + AssignmentEvaluator(const Assignment &_a) : a(_a) {} + }; + + /***/ + + inline ref Assignment::evaluate(const Array *array, + unsigned index) const { + assert(array); + bindings_ty::const_iterator it = bindings.find(array); + if (it!=bindings.end() && indexsecond.size()) { + return ConstantExpr::alloc(it->second[index], array->getRange()); + } else { + if (allowFreeValues) { + return ReadExpr::create(UpdateList(array, 0), + ConstantExpr::alloc(index, array->getDomain())); + } else { + return ConstantExpr::alloc(0, array->getRange()); + } + } + } + + inline ref Assignment::evaluate(ref e) { + AssignmentEvaluator v(*this); + return v.visit(e); + } + + template + inline bool Assignment::satisfies(InputIterator begin, InputIterator end) { + AssignmentEvaluator v(*this); + for (; begin!=end; ++begin) + if (!v.visit(*begin)->isTrue()) + return false; + return true; + } +} + +#endif /* KLEE_ASSIGNMENT_H */ diff --git a/include/klee/Expr/Constraints.h b/include/klee/Expr/Constraints.h new file mode 100644 index 00000000..b9bf3464 --- /dev/null +++ b/include/klee/Expr/Constraints.h @@ -0,0 +1,72 @@ +//===-- Constraints.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_CONSTRAINTS_H +#define KLEE_CONSTRAINTS_H + +#include "klee/Expr/Expr.h" + +// FIXME: Currently we use ConstraintManager for two things: to pass +// sets of constraints around, and to optimize constraints. We should +// move the first usage into a separate data structure +// (ConstraintSet?) which ConstraintManager could embed if it likes. +namespace klee { + +class ExprVisitor; + +class ConstraintManager { +public: + using constraints_ty = std::vector>; + using iterator = constraints_ty::iterator; + using const_iterator = constraints_ty::const_iterator; + + ConstraintManager() = default; + ConstraintManager(const ConstraintManager &cs) = default; + ConstraintManager &operator=(const ConstraintManager &cs) = default; + ConstraintManager(ConstraintManager &&cs) = default; + ConstraintManager &operator=(ConstraintManager &&cs) = default; + + // create from constraints with no optimization + explicit ConstraintManager(const std::vector> &_constraints) + : constraints(_constraints) {} + + // given a constraint which is known to be valid, attempt to + // simplify the existing constraint set + void simplifyForValidConstraint(ref e); + + ref simplifyExpr(ref e) const; + + void addConstraint(ref e); + + bool empty() const noexcept { return constraints.empty(); } + ref back() const { return constraints.back(); } + const_iterator begin() const { return constraints.cbegin(); } + const_iterator end() const { return constraints.cend(); } + std::size_t size() const noexcept { return constraints.size(); } + + bool operator==(const ConstraintManager &other) const { + return constraints == other.constraints; + } + + bool operator!=(const ConstraintManager &other) const { + return constraints != other.constraints; + } + +private: + std::vector> constraints; + + // returns true iff the constraints were modified + bool rewriteConstraints(ExprVisitor &visitor); + + void addConstraintInternal(ref e); +}; + +} // namespace klee + +#endif /* KLEE_CONSTRAINTS_H */ diff --git a/include/klee/Expr/Expr.h b/include/klee/Expr/Expr.h new file mode 100644 index 00000000..d4e4f7fa --- /dev/null +++ b/include/klee/Expr/Expr.h @@ -0,0 +1,1174 @@ +//===-- Expr.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_EXPR_H +#define KLEE_EXPR_H + +#include "klee/util/Bits.h" +#include "klee/util/Ref.h" + +#include "llvm/ADT/APFloat.h" +#include "llvm/ADT/APInt.h" +#include "llvm/ADT/DenseSet.h" +#include "llvm/ADT/SmallVector.h" +#include "llvm/Support/CommandLine.h" +#include "llvm/Support/raw_ostream.h" + +#include +#include +#include +#include + +namespace llvm { + class Type; + class raw_ostream; +} + +namespace klee { + +class Array; +class ArrayCache; +class ConstantExpr; +class ObjectState; + +template class ref; + +extern llvm::cl::OptionCategory ExprCat; + +/// Class representing symbolic expressions. +/** + +Expression canonicalization: we define certain rules for +canonicalization rules for Exprs in order to simplify code that +pattern matches Exprs (since the number of forms are reduced), to open +up further chances for optimization, and to increase similarity for +caching and other purposes. + +The general rules are: +
    +
  1. No Expr has all constant arguments.
    2. + +
  2. Booleans: +
      +
    1. \c Ne, \c Ugt, \c Uge, \c Sgt, \c Sge are not used
      2. +
    2. The only acceptable operations with boolean arguments are + \c Not \c And, \c Or, \c Xor, \c Eq, + as well as \c SExt, \c ZExt, + \c Select and \c NotOptimized.
      3. +
    3. The only boolean operation which may involve a constant is boolean not (== false).
      4. +
    +
    3. + +
  3. Linear Formulas: +
      +
    1. For any subtree representing a linear formula, a constant + term must be on the LHS of the root node of the subtree. In particular, + in a BinaryExpr a constant must always be on the LHS. For example, subtraction + by a constant c is written as add(-c, ?).
      2. +
    +
    4. + + +
  4. Chains are unbalanced to the right
    5. + +
+ + +Steps required for adding an expr: + -# Add case to printKind + -# Add to ExprVisitor + -# Add to IVC (implied value concretization) if possible + +Todo: Shouldn't bool \c Xor just be written as not equal? + +*/ + +class Expr { +public: + static unsigned count; + static const unsigned MAGIC_HASH_CONSTANT = 39; + + /// The type of an expression is simply its width, in bits. + typedef unsigned Width; + + static const Width InvalidWidth = 0; + static const Width Bool = 1; + static const Width Int8 = 8; + static const Width Int16 = 16; + static const Width Int32 = 32; + static const Width Int64 = 64; + static const Width Fl80 = 80; + + + enum Kind { + InvalidKind = -1, + + // Primitive + + Constant = 0, + + // Special + + /// Prevents optimization below the given expression. Used for + /// testing: make equality constraints that KLEE will not use to + /// optimize to concretes. + NotOptimized, + + //// Skip old varexpr, just for deserialization, purge at some point + Read=NotOptimized+2, + Select, + Concat, + Extract, + + // Casting, + ZExt, + SExt, + + // Bit + Not, + + // All subsequent kinds are binary. + + // Arithmetic + Add, + Sub, + Mul, + UDiv, + SDiv, + URem, + SRem, + + // Bit + And, + Or, + Xor, + Shl, + LShr, + AShr, + + // Compare + Eq, + Ne, ///< Not used in canonical form + Ult, + Ule, + Ugt, ///< Not used in canonical form + Uge, ///< Not used in canonical form + Slt, + Sle, + Sgt, ///< Not used in canonical form + Sge, ///< Not used in canonical form + + LastKind=Sge, + + CastKindFirst=ZExt, + CastKindLast=SExt, + BinaryKindFirst=Add, + BinaryKindLast=Sge, + CmpKindFirst=Eq, + CmpKindLast=Sge + }; + + unsigned refCount; + +protected: + unsigned hashValue; + + /// Compares `b` to `this` Expr and determines how they are ordered + /// (ignoring their kid expressions - i.e. those returned by `getKid()`). + /// + /// Typically this requires comparing internal attributes of the Expr. + /// + /// Implementations can assume that `b` and `this` are of the same kind. + /// + /// This method effectively defines a partial order over Expr of the same + /// kind (partial because kid Expr are not compared). + /// + /// This method should not be called directly. Instead `compare()` should + /// be used. + /// + /// \param [in] b Expr to compare `this` to. + /// + /// \return One of the following values: + /// + /// * -1 if `this` is `<` `b` ignoring kid expressions. + /// * 1 if `this` is `>` `b` ignoring kid expressions. + /// * 0 if `this` and `b` are not ordered. + /// + /// `<` and `>` are binary relations that express the partial order. + virtual int compareContents(const Expr &b) const = 0; + +public: + Expr() : refCount(0) { Expr::count++; } + virtual ~Expr() { Expr::count--; } + + virtual Kind getKind() const = 0; + virtual Width getWidth() const = 0; + + virtual unsigned getNumKids() const = 0; + virtual ref getKid(unsigned i) const = 0; + + virtual void print(llvm::raw_ostream &os) const; + + /// dump - Print the expression to stderr. + void dump() const; + + /// Returns the pre-computed hash of the current expression + virtual unsigned hash() const { return hashValue; } + + /// (Re)computes the hash of the current expression. + /// Returns the hash value. + virtual unsigned computeHash(); + + /// Compares `b` to `this` Expr for structural equivalence. + /// + /// This method effectively defines a total order over all Expr. + /// + /// \param [in] b Expr to compare `this` to. + /// + /// \return One of the following values: + /// + /// * -1 iff `this` is `<` `b` + /// * 0 iff `this` is structurally equivalent to `b` + /// * 1 iff `this` is `>` `b` + /// + /// `<` and `>` are binary relations that express the total order. + int compare(const Expr &b) const; + + // Given an array of new kids return a copy of the expression + // but using those children. + virtual ref rebuild(ref kids[/* getNumKids() */]) const = 0; + + /// isZero - Is this a constant zero. + bool isZero() const; + + /// isTrue - Is this the true expression. + bool isTrue() const; + + /// isFalse - Is this the false expression. + bool isFalse() const; + + /* Static utility methods */ + + 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) { + return (w + 7) / 8; + } + + /* Kind utilities */ + + /* Utility creation functions */ + static ref createSExtToPointerWidth(ref e); + static ref createZExtToPointerWidth(ref e); + static ref createImplies(ref hyp, ref conc); + static ref createIsZero(ref e); + + /// Create a little endian read of the given type at offset 0 of the + /// given object. + static ref createTempRead(const Array *array, Expr::Width w); + + static ref createPointer(uint64_t v); + + struct CreateArg; + static ref createFromKind(Kind k, std::vector args); + + static bool isValidKidWidth(unsigned kid, Width w) { return true; } + static bool needsResultType() { return false; } + + static bool classof(const Expr *) { return true; } + +private: + typedef llvm::DenseSet > ExprEquivSet; + int compare(const Expr &b, ExprEquivSet &equivs) const; +}; + +struct Expr::CreateArg { + ref expr; + Width width; + + CreateArg(Width w = Bool) : expr(0), width(w) {} + CreateArg(ref e) : expr(e), width(Expr::InvalidWidth) {} + + bool isExpr() { return !isWidth(); } + bool isWidth() { return width != Expr::InvalidWidth; } +}; + +// Comparison operators + +inline bool operator==(const Expr &lhs, const Expr &rhs) { + return lhs.compare(rhs) == 0; +} + +inline bool operator<(const Expr &lhs, const Expr &rhs) { + return lhs.compare(rhs) < 0; +} + +inline bool operator!=(const Expr &lhs, const Expr &rhs) { + return !(lhs == rhs); +} + +inline bool operator>(const Expr &lhs, const Expr &rhs) { + return rhs < lhs; +} + +inline bool operator<=(const Expr &lhs, const Expr &rhs) { + return !(lhs > rhs); +} + +inline bool operator>=(const Expr &lhs, const Expr &rhs) { + return !(lhs < rhs); +} + +// Printing operators + +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const Expr &e) { + e.print(os); + return os; +} + +inline llvm::raw_ostream &operator<<(llvm::raw_ostream &os, const Expr::Kind kind) { + Expr::printKind(os, kind); + return os; +} + +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; +} + +// Utility classes + +class NonConstantExpr : public Expr { +public: + static bool classof(const Expr *E) { + return E->getKind() != Expr::Constant; + } + static bool classof(const NonConstantExpr *) { return true; } +}; + +class BinaryExpr : public NonConstantExpr { +public: + ref left, right; + +public: + unsigned getNumKids() const { return 2; } + ref getKid(unsigned i) const { + if(i == 0) + return left; + if(i == 1) + return right; + return 0; + } + +protected: + BinaryExpr(const ref &l, const ref &r) : left(l), right(r) {} + +public: + static bool classof(const Expr *E) { + Kind k = E->getKind(); + return Expr::BinaryKindFirst <= k && k <= Expr::BinaryKindLast; + } + static bool classof(const BinaryExpr *) { return true; } +}; + + +class CmpExpr : public BinaryExpr { + +protected: + CmpExpr(ref l, ref r) : BinaryExpr(l,r) {} + +public: + Width getWidth() const { return Bool; } + + static bool classof(const Expr *E) { + Kind k = E->getKind(); + return Expr::CmpKindFirst <= k && k <= Expr::CmpKindLast; + } + static bool classof(const CmpExpr *) { return true; } +}; + +// Special + +class NotOptimizedExpr : public NonConstantExpr { +public: + static const Kind kind = NotOptimized; + static const unsigned numKids = 1; + ref src; + + static ref alloc(const ref &src) { + ref r(new NotOptimizedExpr(src)); + r->computeHash(); + return r; + } + + static ref create(ref src); + + Width getWidth() const { return src->getWidth(); } + Kind getKind() const { return NotOptimized; } + + unsigned getNumKids() const { return 1; } + ref getKid(unsigned i) const { return src; } + + virtual ref rebuild(ref kids[]) const { return create(kids[0]); } + +private: + NotOptimizedExpr(const ref &_src) : src(_src) {} + +protected: + virtual int compareContents(const Expr &b) const { + // No attributes to compare. + return 0; + } + +public: + static bool classof(const Expr *E) { + return E->getKind() == Expr::NotOptimized; + } + static bool classof(const NotOptimizedExpr *) { return true; } +}; + + +/// Class representing a byte update of an array. +class UpdateNode { + friend class UpdateList; + + mutable unsigned refCount; + // cache instead of recalc + unsigned hashValue; + +public: + const UpdateNode *next; + ref index, value; + +private: + /// size of this update sequence, including this update + unsigned size; + +public: + UpdateNode(const UpdateNode *_next, + const ref &_index, + const ref &_value); + + unsigned getSize() const { return size; } + + int compare(const UpdateNode &b) const; + unsigned hash() const { return hashValue; } + +private: + UpdateNode() : refCount(0) {} + ~UpdateNode(); + + unsigned computeHash(); +}; + +class Array { +public: + // Name of the array + const std::string name; + + // FIXME: Not 64-bit clean. + const unsigned size; + + /// Domain is how many bits can be used to access the array [32 bits] + /// Range is the size (in bits) of the number stored there (array of bytes -> 8) + const Expr::Width domain, range; + + /// constantValues - The constant initial values for this array, or empty for + /// a symbolic array. If non-empty, this size of this array is equivalent to + /// the array size. + const std::vector > constantValues; + +private: + unsigned hashValue; + + // FIXME: Make =delete when we switch to C++11 + Array(const Array& array); + + // FIXME: Make =delete when we switch to C++11 + Array& operator =(const Array& array); + + ~Array(); + + /// Array - Construct a new array object. + /// + /// \param _name - The name for this array. Names should generally be unique + /// across an application, but this is not necessary for correctness, except + /// when printing expressions. When expressions are printed the output will + /// not parse correctly since two arrays with the same name cannot be + /// distinguished once printed. + Array(const std::string &_name, uint64_t _size, + const ref *constantValuesBegin = 0, + const ref *constantValuesEnd = 0, + Expr::Width _domain = Expr::Int32, Expr::Width _range = Expr::Int8); + +public: + bool isSymbolicArray() const { return constantValues.empty(); } + bool isConstantArray() const { return !isSymbolicArray(); } + + const std::string getName() const { return name; } + unsigned getSize() const { return size; } + Expr::Width getDomain() const { return domain; } + Expr::Width getRange() const { return range; } + + /// ComputeHash must take into account the name, the size, the domain, and the range + unsigned computeHash(); + unsigned hash() const { return hashValue; } + friend class ArrayCache; +}; + +/// Class representing a complete list of updates into an array. +class UpdateList { + friend class ReadExpr; // for default constructor + +public: + const Array *root; + + /// pointer to the most recent update node + const UpdateNode *head; + +public: + UpdateList(const Array *_root, const UpdateNode *_head); + UpdateList(const UpdateList &b); + ~UpdateList(); + + UpdateList &operator=(const UpdateList &b); + + /// size of this update list + unsigned getSize() const { return (head ? head->getSize() : 0); } + + void extend(const ref &index, const ref &value); + + int compare(const UpdateList &b) const; + unsigned hash() const; +private: + void tryFreeNodes(); +}; + +/// Class representing a one byte read from an array. +class ReadExpr : public NonConstantExpr { +public: + static const Kind kind = Read; + static const unsigned numKids = 1; + +public: + UpdateList updates; + ref index; + +public: + static ref alloc(const UpdateList &updates, const ref &index) { + ref r(new ReadExpr(updates, index)); + r->computeHash(); + return r; + } + + static ref create(const UpdateList &updates, ref i); + + Width getWidth() const { assert(updates.root); return updates.root->getRange(); } + Kind getKind() const { return Read; } + + unsigned getNumKids() const { return numKids; } + ref getKid(unsigned i) const { return !i ? index : 0; } + + int compareContents(const Expr &b) const; + + virtual ref rebuild(ref kids[]) const { + return create(updates, kids[0]); + } + + virtual unsigned computeHash(); + +private: + ReadExpr(const UpdateList &_updates, const ref &_index) : + updates(_updates), index(_index) { assert(updates.root); } + +public: + static bool classof(const Expr *E) { + return E->getKind() == Expr::Read; + } + static bool classof(const ReadExpr *) { return true; } +}; + + +/// Class representing an if-then-else expression. +class SelectExpr : public NonConstantExpr { +public: + static const Kind kind = Select; + static const unsigned numKids = 3; + +public: + ref cond, trueExpr, falseExpr; + +public: + static ref alloc(const ref &c, const ref &t, + const ref &f) { + ref r(new SelectExpr(c, t, f)); + r->computeHash(); + return r; + } + + static ref create(ref c, ref t, ref f); + + Width getWidth() const { return trueExpr->getWidth(); } + Kind getKind() const { return Select; } + + unsigned getNumKids() const { return numKids; } + ref getKid(unsigned i) const { + switch(i) { + case 0: return cond; + case 1: return trueExpr; + case 2: return falseExpr; + default: return 0; + } + } + + static bool isValidKidWidth(unsigned kid, Width w) { + if (kid == 0) + return w == Bool; + else + return true; + } + + virtual ref rebuild(ref kids[]) const { + return create(kids[0], kids[1], kids[2]); + } + +private: + SelectExpr(const ref &c, const ref &t, const ref &f) + : cond(c), trueExpr(t), falseExpr(f) {} + +public: + static bool classof(const Expr *E) { + return E->getKind() == Expr::Select; + } + static bool classof(const SelectExpr *) { return true; } + +protected: + virtual int compareContents(const Expr &b) const { + // No attributes to compare. + return 0; + } +}; + + +/** Children of a concat expression can have arbitrary widths. + Kid 0 is the left kid, kid 1 is the right kid. +*/ +class ConcatExpr : public NonConstantExpr { +public: + static const Kind kind = Concat; + static const unsigned numKids = 2; + +private: + Width width; + ref left, right; + +public: + static ref alloc(const ref &l, const ref &r) { + ref c(new ConcatExpr(l, r)); + c->computeHash(); + return c; + } + + static ref create(const ref &l, const ref &r); + + Width getWidth() const { return width; } + Kind getKind() const { return kind; } + ref getLeft() const { return left; } + ref getRight() const { return right; } + + unsigned getNumKids() const { return numKids; } + ref getKid(unsigned i) const { + if (i == 0) return left; + else if (i == 1) return right; + else return NULL; + } + + /// Shortcuts to create larger concats. The chain returned is unbalanced to the right + static ref createN(unsigned nKids, const ref kids[]); + static ref create4(const ref &kid1, const ref &kid2, + const ref &kid3, const ref &kid4); + static ref create8(const ref &kid1, const ref &kid2, + const ref &kid3, const ref &kid4, + const ref &kid5, const ref &kid6, + const ref &kid7, const ref &kid8); + + virtual ref rebuild(ref kids[]) const { return create(kids[0], kids[1]); } + +private: + ConcatExpr(const ref &l, const ref &r) : left(l), right(r) { + width = l->getWidth() + r->getWidth(); + } + +public: + static bool classof(const Expr *E) { + return E->getKind() == Expr::Concat; + } + static bool classof(const ConcatExpr *) { return true; } + +protected: + virtual int compareContents(const Expr &b) const { + const ConcatExpr &eb = static_cast(b); + if (width != eb.width) + return width < eb.width ? -1 : 1; + return 0; + } +}; + + +/** This class represents an extract from expression {\tt expr}, at + bit offset {\tt offset} of width {\tt width}. Bit 0 is the right most + bit of the expression. + */ +class ExtractExpr : public NonConstantExpr { +public: + static const Kind kind = Extract; + static const unsigned numKids = 1; + +public: + ref expr; + unsigned offset; + Width width; + +public: + static ref alloc(const ref &e, unsigned o, Width w) { + ref r(new ExtractExpr(e, o, w)); + r->computeHash(); + return r; + } + + /// Creates an ExtractExpr with the given bit offset and width + static ref create(ref e, unsigned bitOff, Width w); + + Width getWidth() const { return width; } + Kind getKind() const { return Extract; } + + unsigned getNumKids() const { return numKids; } + ref getKid(unsigned i) const { return expr; } + + int compareContents(const Expr &b) const { + const ExtractExpr &eb = static_cast(b); + if (offset != eb.offset) return offset < eb.offset ? -1 : 1; + if (width != eb.width) return width < eb.width ? -1 : 1; + return 0; + } + + virtual ref rebuild(ref kids[]) const { + return create(kids[0], offset, width); + } + + virtual unsigned computeHash(); + +private: + ExtractExpr(const ref &e, unsigned b, Width w) + : expr(e),offset(b),width(w) {} + +public: + static bool classof(const Expr *E) { + return E->getKind() == Expr::Extract; + } + static bool classof(const ExtractExpr *) { return true; } +}; + + +/** + Bitwise Not +*/ +class NotExpr : public NonConstantExpr { +public: + static const Kind kind = Not; + static const unsigned numKids = 1; + + ref expr; + +public: + static ref alloc(const ref &e) { + ref r(new NotExpr(e)); + r->computeHash(); + return r; + } + + static ref create(const ref &e); + + Width getWidth() const { return expr->getWidth(); } + Kind getKind() const { return Not; } + + unsigned getNumKids() const { return numKids; } + ref getKid(unsigned i) const { return expr; } + + virtual ref rebuild(ref kids[]) const { + return create(kids[0]); + } + + virtual unsigned computeHash(); + +public: + static bool classof(const Expr *E) { + return E->getKind() == Expr::Not; + } + static bool classof(const NotExpr *) { return true; } + +private: + NotExpr(const ref &e) : expr(e) {} + +protected: + virtual int compareContents(const Expr &b) const { + // No attributes to compare. + return 0; + } +}; + + + +// Casting + +class CastExpr : public NonConstantExpr { +public: + ref src; + Width width; + +public: + CastExpr(const ref &e, Width w) : src(e), width(w) {} + + Width getWidth() const { return width; } + + unsigned getNumKids() const { return 1; } + ref getKid(unsigned i) const { return (i==0) ? src : 0; } + + static bool needsResultType() { return true; } + + int compareContents(const Expr &b) const { + const CastExpr &eb = static_cast(b); + if (width != eb.width) return width < eb.width ? -1 : 1; + return 0; + } + + virtual unsigned computeHash(); + + static bool classof(const Expr *E) { + Expr::Kind k = E->getKind(); + return Expr::CastKindFirst <= k && k <= Expr::CastKindLast; + } + static bool classof(const CastExpr *) { return true; } +}; + +#define CAST_EXPR_CLASS(_class_kind) \ +class _class_kind ## Expr : public CastExpr { \ +public: \ + static const Kind kind = _class_kind; \ + static const unsigned numKids = 1; \ +public: \ + _class_kind ## Expr(ref e, Width w) : CastExpr(e,w) {} \ + static ref alloc(const ref &e, Width w) { \ + ref r(new _class_kind ## Expr(e, w)); \ + r->computeHash(); \ + return r; \ + } \ + static ref create(const ref &e, Width w); \ + Kind getKind() const { return _class_kind; } \ + virtual ref rebuild(ref kids[]) const { \ + return create(kids[0], width); \ + } \ + \ + static bool classof(const Expr *E) { \ + return E->getKind() == Expr::_class_kind; \ + } \ + static bool classof(const _class_kind ## Expr *) { \ + return true; \ + } \ +}; \ + +CAST_EXPR_CLASS(SExt) +CAST_EXPR_CLASS(ZExt) + +// Arithmetic/Bit Exprs + +#define ARITHMETIC_EXPR_CLASS(_class_kind) \ + class _class_kind##Expr : public BinaryExpr { \ + public: \ + static const Kind kind = _class_kind; \ + static const unsigned numKids = 2; \ + \ + public: \ + _class_kind##Expr(const ref &l, const ref &r) \ + : BinaryExpr(l, r) {} \ + static ref alloc(const ref &l, const ref &r) { \ + ref res(new _class_kind##Expr(l, r)); \ + res->computeHash(); \ + return res; \ + } \ + static ref create(const ref &l, const ref &r); \ + Width getWidth() const { return left->getWidth(); } \ + Kind getKind() const { return _class_kind; } \ + virtual ref rebuild(ref kids[]) const { \ + return create(kids[0], kids[1]); \ + } \ + \ + static bool classof(const Expr *E) { \ + return E->getKind() == Expr::_class_kind; \ + } \ + static bool classof(const _class_kind##Expr *) { return true; } \ + \ + protected: \ + virtual int compareContents(const Expr &b) const { \ + /* No attributes to compare.*/ \ + return 0; \ + } \ + }; + +ARITHMETIC_EXPR_CLASS(Add) +ARITHMETIC_EXPR_CLASS(Sub) +ARITHMETIC_EXPR_CLASS(Mul) +ARITHMETIC_EXPR_CLASS(UDiv) +ARITHMETIC_EXPR_CLASS(SDiv) +ARITHMETIC_EXPR_CLASS(URem) +ARITHMETIC_EXPR_CLASS(SRem) +ARITHMETIC_EXPR_CLASS(And) +ARITHMETIC_EXPR_CLASS(Or) +ARITHMETIC_EXPR_CLASS(Xor) +ARITHMETIC_EXPR_CLASS(Shl) +ARITHMETIC_EXPR_CLASS(LShr) +ARITHMETIC_EXPR_CLASS(AShr) + +// Comparison Exprs + +#define COMPARISON_EXPR_CLASS(_class_kind) \ + class _class_kind##Expr : public CmpExpr { \ + public: \ + static const Kind kind = _class_kind; \ + static const unsigned numKids = 2; \ + \ + public: \ + _class_kind##Expr(const ref &l, const ref &r) \ + : CmpExpr(l, r) {} \ + static ref alloc(const ref &l, const ref &r) { \ + ref res(new _class_kind##Expr(l, r)); \ + res->computeHash(); \ + return res; \ + } \ + static ref create(const ref &l, const ref &r); \ + Kind getKind() const { return _class_kind; } \ + virtual ref rebuild(ref kids[]) const { \ + return create(kids[0], kids[1]); \ + } \ + \ + static bool classof(const Expr *E) { \ + return E->getKind() == Expr::_class_kind; \ + } \ + static bool classof(const _class_kind##Expr *) { return true; } \ + \ + protected: \ + virtual int compareContents(const Expr &b) const { \ + /* No attributes to compare. */ \ + return 0; \ + } \ + }; + +COMPARISON_EXPR_CLASS(Eq) +COMPARISON_EXPR_CLASS(Ne) +COMPARISON_EXPR_CLASS(Ult) +COMPARISON_EXPR_CLASS(Ule) +COMPARISON_EXPR_CLASS(Ugt) +COMPARISON_EXPR_CLASS(Uge) +COMPARISON_EXPR_CLASS(Slt) +COMPARISON_EXPR_CLASS(Sle) +COMPARISON_EXPR_CLASS(Sgt) +COMPARISON_EXPR_CLASS(Sge) + +// Terminal Exprs + +class ConstantExpr : public Expr { +public: + static const Kind kind = Constant; + static const unsigned numKids = 0; + +private: + llvm::APInt value; + + ConstantExpr(const llvm::APInt &v) : value(v) {} + +public: + ~ConstantExpr() {} + + Width getWidth() const { return value.getBitWidth(); } + Kind getKind() const { return Constant; } + + unsigned getNumKids() const { return 0; } + ref getKid(unsigned i) const { return 0; } + + /// getAPValue - Return the arbitrary precision value directly. + /// + /// Clients should generally not use the APInt value directly and instead use + /// native ConstantExpr APIs. + const llvm::APInt &getAPValue() const { return value; } + + /// getZExtValue - Returns the constant value zero extended to the + /// return type of this method. + /// + ///\param bits - optional parameter that can be used to check that the + /// number of bits used by this constant is <= to the parameter + /// value. This is useful for checking that type casts won't truncate + /// useful bits. + /// + /// Example: unit8_t byte= (unit8_t) constant->getZExtValue(8); + uint64_t getZExtValue(unsigned bits = 64) const { + assert(getWidth() <= bits && "Value may be out of range!"); + return value.getZExtValue(); + } + + /// getLimitedValue - If this value is smaller than the specified limit, + /// return it, otherwise return the limit value. + uint64_t getLimitedValue(uint64_t Limit = ~0ULL) const { + return value.getLimitedValue(Limit); + } + + /// toString - Return the constant value as a string + /// \param Res specifies the string for the result to be placed in + /// \param radix specifies the base (e.g. 2,10,16). The default is base 10 + void toString(std::string &Res, unsigned radix = 10) const; + + int compareContents(const Expr &b) const { + const ConstantExpr &cb = static_cast(b); + if (getWidth() != cb.getWidth()) + return getWidth() < cb.getWidth() ? -1 : 1; + if (value == cb.value) + return 0; + return value.ult(cb.value) ? -1 : 1; + } + + virtual ref rebuild(ref kids[]) const { + assert(0 && "rebuild() on ConstantExpr"); + return const_cast(this); + } + + virtual unsigned computeHash(); + + static ref fromMemory(void *address, Width w); + void toMemory(void *address); + + static ref alloc(const llvm::APInt &v) { + ref r(new ConstantExpr(v)); + r->computeHash(); + return r; + } + + static ref alloc(const llvm::APFloat &f) { + return alloc(f.bitcastToAPInt()); + } + + static ref alloc(uint64_t v, Width w) { + return alloc(llvm::APInt(w, v)); + } + + static ref create(uint64_t v, Width w) { +#ifndef NDEBUG + if (w <= 64) + assert(v == bits64::truncateToNBits(v, w) && "invalid constant"); +#endif + return alloc(v, w); + } + + static bool classof(const Expr *E) { return E->getKind() == Expr::Constant; } + static bool classof(const ConstantExpr *) { return true; } + + /* Utility Functions */ + + /// isZero - Is this a constant zero. + bool isZero() const { return getAPValue().isMinValue(); } + + /// isOne - Is this a constant one. + bool isOne() const { return getLimitedValue() == 1; } + + /// isTrue - Is this the true expression. + bool isTrue() const { + return (getWidth() == Expr::Bool && value.getBoolValue() == true); + } + + /// isFalse - Is this the false expression. + bool isFalse() const { + return (getWidth() == Expr::Bool && value.getBoolValue() == false); + } + + /// isAllOnes - Is this constant all ones. + bool isAllOnes() const { return getAPValue().isAllOnesValue(); } + + /* Constant Operations */ + + ref Concat(const ref &RHS); + ref Extract(unsigned offset, Width W); + ref ZExt(Width W); + ref SExt(Width W); + ref Add(const ref &RHS); + ref Sub(const ref &RHS); + ref Mul(const ref &RHS); + ref UDiv(const ref &RHS); + ref SDiv(const ref &RHS); + ref URem(const ref &RHS); + ref SRem(const ref &RHS); + ref And(const ref &RHS); + ref Or(const ref &RHS); + ref Xor(const ref &RHS); + ref Shl(const ref &RHS); + ref LShr(const ref &RHS); + ref AShr(const ref &RHS); + + // Comparisons return a constant expression of width 1. + + ref Eq(const ref &RHS); + ref Ne(const ref &RHS); + ref Ult(const ref &RHS); + ref Ule(const ref &RHS); + ref Ugt(const ref &RHS); + ref Uge(const ref &RHS); + ref Slt(const ref &RHS); + ref Sle(const ref &RHS); + ref Sgt(const ref &RHS); + ref Sge(const ref &RHS); + + ref Neg(); + ref Not(); +}; + +// Implementations + +inline bool Expr::isZero() const { + if (const ConstantExpr *CE = dyn_cast(this)) + return CE->isZero(); + return false; +} + +inline bool Expr::isTrue() const { + assert(getWidth() == Expr::Bool && "Invalid isTrue() call!"); + if (const ConstantExpr *CE = dyn_cast(this)) + return CE->isTrue(); + return false; +} + +inline bool Expr::isFalse() const { + assert(getWidth() == Expr::Bool && "Invalid isFalse() call!"); + if (const ConstantExpr *CE = dyn_cast(this)) + return CE->isFalse(); + return false; +} + +} // End klee namespace + +#endif /* KLEE_EXPR_H */ diff --git a/include/klee/Expr/ExprBuilder.h b/include/klee/Expr/ExprBuilder.h new file mode 100644 index 00000000..4a2c5cf4 --- /dev/null +++ b/include/klee/Expr/ExprBuilder.h @@ -0,0 +1,91 @@ +//===-- ExprBuilder.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_EXPRBUILDER_H +#define KLEE_EXPRBUILDER_H + +#include "Expr.h" + +namespace klee { + /// ExprBuilder - Base expression builder class. + class ExprBuilder { + protected: + ExprBuilder(); + + public: + virtual ~ExprBuilder(); + + // Expressions + + virtual ref Constant(const llvm::APInt &Value) = 0; + virtual ref NotOptimized(const ref &Index) = 0; + virtual ref Read(const UpdateList &Updates, + const ref &Index) = 0; + virtual ref Select(const ref &Cond, + const ref &LHS, const ref &RHS) = 0; + virtual ref Concat(const ref &LHS, const ref &RHS) = 0; + virtual ref Extract(const ref &LHS, + unsigned Offset, Expr::Width W) = 0; + virtual ref ZExt(const ref &LHS, Expr::Width W) = 0; + virtual ref SExt(const ref &LHS, Expr::Width W) = 0; + virtual ref Add(const ref &LHS, const ref &RHS) = 0; + virtual ref Sub(const ref &LHS, const ref &RHS) = 0; + virtual ref Mul(const ref &LHS, const ref &RHS) = 0; + virtual ref UDiv(const ref &LHS, const ref &RHS) = 0; + virtual ref SDiv(const ref &LHS, const ref &RHS) = 0; + virtual ref URem(const ref &LHS, const ref &RHS) = 0; + virtual ref SRem(const ref &LHS, const ref &RHS) = 0; + virtual ref Not(const ref &LHS) = 0; + virtual ref And(const ref &LHS, const ref &RHS) = 0; + virtual ref Or(const ref &LHS, const ref &RHS) = 0; + virtual ref Xor(const ref &LHS, const ref &RHS) = 0; + virtual ref Shl(const ref &LHS, const ref &RHS) = 0; + virtual ref LShr(const ref &LHS, const ref &RHS) = 0; + virtual ref AShr(const ref &LHS, const ref &RHS) = 0; + virtual ref Eq(const ref &LHS, const ref &RHS) = 0; + virtual ref Ne(const ref &LHS, const ref &RHS) = 0; + virtual ref Ult(const ref &LHS, const ref &RHS) = 0; + virtual ref Ule(const ref &LHS, const ref &RHS) = 0; + virtual ref Ugt(const ref &LHS, const ref &RHS) = 0; + virtual ref Uge(const ref &LHS, const ref &RHS) = 0; + virtual ref Slt(const ref &LHS, const ref &RHS) = 0; + virtual ref Sle(const ref &LHS, const ref &RHS) = 0; + virtual ref Sgt(const ref &LHS, const ref &RHS) = 0; + virtual ref Sge(const ref &LHS, const ref &RHS) = 0; + + // Utility functions + + ref False() { return ConstantExpr::alloc(0, Expr::Bool); } + + ref True() { return ConstantExpr::alloc(1, Expr::Bool); } + + ref Constant(uint64_t Value, Expr::Width W) { + return Constant(llvm::APInt(W, Value)); + } + }; + + /// createDefaultExprBuilder - Create an expression builder which does no + /// folding. + ExprBuilder *createDefaultExprBuilder(); + + /// createConstantFoldingExprBuilder - Create an expression builder which + /// folds constant expressions. + /// + /// Base - The base builder to use when constructing expressions. + ExprBuilder *createConstantFoldingExprBuilder(ExprBuilder *Base); + + /// createSimplifyingExprBuilder - Create an expression builder which attemps + /// to fold redundant expressions and normalize expressions for improved + /// caching. + /// + /// Base - The base builder to use when constructing expressions. + ExprBuilder *createSimplifyingExprBuilder(ExprBuilder *Base); +} + +#endif /* KLEE_EXPRBUILDER_H */ diff --git a/include/klee/Expr/ExprEvaluator.h b/include/klee/Expr/ExprEvaluator.h new file mode 100644 index 00000000..e0368203 --- /dev/null +++ b/include/klee/Expr/ExprEvaluator.h @@ -0,0 +1,42 @@ +//===-- ExprEvaluator.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_EXPREVALUATOR_H +#define KLEE_EXPREVALUATOR_H + +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprVisitor.h" + +namespace klee { + class ExprEvaluator : public ExprVisitor { + protected: + Action evalRead(const UpdateList &ul, unsigned index); + Action visitRead(const ReadExpr &re); + Action visitExpr(const Expr &e); + + Action protectedDivOperation(const BinaryExpr &e); + Action visitUDiv(const UDivExpr &e); + Action visitSDiv(const SDivExpr &e); + Action visitURem(const URemExpr &e); + Action visitSRem(const SRemExpr &e); + Action visitExprPost(const Expr& e); + + public: + ExprEvaluator() {} + + /// getInitialValue - Return the initial value for a symbolic byte. + /// + /// This will only be called for constant arrays if the index is + /// out-of-bounds. If the value is unknown then the user should return a + /// ReadExpr at the initial version of this array. + virtual ref getInitialValue(const Array& os, unsigned index) = 0; + }; +} + +#endif /* KLEE_EXPREVALUATOR_H */ diff --git a/include/klee/Expr/ExprHashMap.h b/include/klee/Expr/ExprHashMap.h new file mode 100644 index 00000000..2b0b3bda --- /dev/null +++ b/include/klee/Expr/ExprHashMap.h @@ -0,0 +1,62 @@ +//===-- ExprHashMap.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_EXPRHASHMAP_H +#define KLEE_EXPRHASHMAP_H + +#include "klee/Expr/Expr.h" + +#include +#ifdef _LIBCPP_VERSION +#include +#include +#define unordered_map std::unordered_map +#define unordered_set std::unordered_set +#else +#include +#include +#define unordered_map std::tr1::unordered_map +#define unordered_set std::tr1::unordered_set +#endif + +namespace klee { + + namespace util { + struct ExprHash { + unsigned operator()(const ref e) const { + return e->hash(); + } + }; + + struct ExprCmp { + bool operator()(const ref &a, const ref &b) const { + return a==b; + } + }; + } + + template + class ExprHashMap : + + public unordered_map, + T, + klee::util::ExprHash, + klee::util::ExprCmp> { + }; + + typedef unordered_set, + klee::util::ExprHash, + klee::util::ExprCmp> ExprHashSet; + +} + +#undef unordered_map +#undef unordered_set + +#endif /* KLEE_EXPRHASHMAP_H */ diff --git a/include/klee/Expr/ExprPPrinter.h b/include/klee/Expr/ExprPPrinter.h new file mode 100644 index 00000000..7541c132 --- /dev/null +++ b/include/klee/Expr/ExprPPrinter.h @@ -0,0 +1,78 @@ +//===-- ExprPPrinter.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_EXPRPPRINTER_H +#define KLEE_EXPRPPRINTER_H + +#include "klee/Expr/Expr.h" + +namespace llvm { + class raw_ostream; +} +namespace klee { + class ConstraintManager; + + class ExprPPrinter { + protected: + ExprPPrinter() {} + + public: + 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 &e) = 0; + virtual void print(const ref &e, unsigned indent=0) = 0; + + // utility methods + + template + void scan(Container c) { + scan(c.begin(), c.end()); + } + + template + void scan(InputIterator it, InputIterator end) { + for (; it!=end; ++it) + scan(*it); + } + + /// printOne - Pretty print a single expression prefixed by a + /// message and followed by a line break. + static void printOne(llvm::raw_ostream &os, const char *message, + const ref &e); + + /// printSingleExpr - Pretty print a single expression. + /// + /// The expression will not be followed by a line break. + /// + /// 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(llvm::raw_ostream &os, const ref &e); + + static void printConstraints(llvm::raw_ostream &os, + const ConstraintManager &constraints); + + static void printQuery(llvm::raw_ostream &os, + const ConstraintManager &constraints, + const ref &q, + const ref *evalExprsBegin = 0, + const ref *evalExprsEnd = 0, + const Array * const* evalArraysBegin = 0, + const Array * const* evalArraysEnd = 0, + bool printArrayDecls = true); + }; + +} + +#endif /* KLEE_EXPRPPRINTER_H */ diff --git a/include/klee/Expr/ExprRangeEvaluator.h b/include/klee/Expr/ExprRangeEvaluator.h new file mode 100644 index 00000000..4d212764 --- /dev/null +++ b/include/klee/Expr/ExprRangeEvaluator.h @@ -0,0 +1,285 @@ +//===-- ExprRangeEvaluator.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_EXPRRANGEEVALUATOR_H +#define KLEE_EXPRRANGEEVALUATOR_H + +#include "klee/Expr/Expr.h" +#include "klee/util/Bits.h" + +namespace klee { + +/* +class ValueType { +public: + ValueType(); // empty range + ValueType(uint64_t value); + ValueType(uint64_t min, uint64_t max); + + bool mustEqual(const uint64_t b); + bool mustEqual(const ValueType &b); + bool mayEqual(const uint64_t b); + bool mayEqual(const ValueType &b); + + bool isFullRange(unsigned width); + + ValueType set_union(ValueType &); + ValueType set_intersection(ValueType &); + ValueType set_difference(ValueType &); + + ValueType binaryAnd(ValueType &); + ValueType binaryOr(ValueType &); + ValueType binaryXor(ValueType &); + ValueType concat(ValueType &, unsigned width); + ValueType add(ValueType &, unsigned width); + ValueType sub(ValueType &, unsigned width); + ValueType mul(ValueType &, unsigned width); + ValueType udiv(ValueType &, unsigned width); + ValueType sdiv(ValueType &, unsigned width); + ValueType urem(ValueType &, unsigned width); + ValueType srem(ValueType &, unsigned width); + + uint64_t min(); + uint64_t max(); + int64_t minSigned(unsigned width); + int64_t maxSigned(unsigned width); +} +*/ + +template +class ExprRangeEvaluator { +protected: + /// getInitialReadRange - Return a range for the initial value of the given + /// array (which may be constant), for the given range of indices. + virtual T getInitialReadRange(const Array &os, T index) = 0; + + T evalRead(const UpdateList &ul, T index); + +public: + ExprRangeEvaluator() {} + virtual ~ExprRangeEvaluator() {} + + T evaluate(const ref &e); +}; + +template +T ExprRangeEvaluator::evalRead(const UpdateList &ul, + T index) { + T res; + + for (const UpdateNode *un=ul.head; un; un=un->next) { + T ui = evaluate(un->index); + + if (ui.mustEqual(index)) { + return res.set_union(evaluate(un->value)); + } else if (ui.mayEqual(index)) { + res = res.set_union(evaluate(un->value)); + if (res.isFullRange(8)) { + return res; + } + } + } + + return res.set_union(getInitialReadRange(*ul.root, index)); +} + +template +T ExprRangeEvaluator::evaluate(const ref &e) { + switch (e->getKind()) { + case Expr::Constant: + return T(cast(e)); + + case Expr::NotOptimized: + break; + + case Expr::Read: { + const ReadExpr *re = cast(e); + T index = evaluate(re->index); + + assert(re->updates.root && re->getWidth() == re->updates.root->range && "unexpected multibyte read"); + + return evalRead(re->updates, index); + } + + case Expr::Select: { + const SelectExpr *se = cast(e); + T cond = evaluate(se->cond); + + if (cond.mustEqual(1)) { + return evaluate(se->trueExpr); + } else if (cond.mustEqual(0)) { + return evaluate(se->falseExpr); + } else { + return evaluate(se->trueExpr).set_union(evaluate(se->falseExpr)); + } + } + + // XXX these should be unrolled to ensure nice inline + case Expr::Concat: { + const Expr *ep = e.get(); + T res(0); + for (unsigned i=0; igetNumKids(); i++) + res = res.concat(evaluate(ep->getKid(i)),8); + return res; + } + + // Arithmetic + + case Expr::Add: { + const BinaryExpr *be = cast(e); + unsigned width = be->left->getWidth(); + return evaluate(be->left).add(evaluate(be->right), width); + } + case Expr::Sub: { + const BinaryExpr *be = cast(e); + unsigned width = be->left->getWidth(); + return evaluate(be->left).sub(evaluate(be->right), width); + } + case Expr::Mul: { + const BinaryExpr *be = cast(e); + unsigned width = be->left->getWidth(); + return evaluate(be->left).mul(evaluate(be->right), width); + } + case Expr::UDiv: { + const BinaryExpr *be = cast(e); + unsigned width = be->left->getWidth(); + return evaluate(be->left).udiv(evaluate(be->right), width); + } + case Expr::SDiv: { + const BinaryExpr *be = cast(e); + unsigned width = be->left->getWidth(); + return evaluate(be->left).sdiv(evaluate(be->right), width); + } + case Expr::URem: { + const BinaryExpr *be = cast(e); + unsigned width = be->left->getWidth(); + return evaluate(be->left).urem(evaluate(be->right), width); + } + case Expr::SRem: { + const BinaryExpr *be = cast(e); + unsigned width = be->left->getWidth(); + return evaluate(be->left).srem(evaluate(be->right), width); + } + + // Binary + + case Expr::And: { + const BinaryExpr *be = cast(e); + return evaluate(be->left).binaryAnd(evaluate(be->right)); + } + case Expr::Or: { + const BinaryExpr *be = cast(e); + return evaluate(be->left).binaryOr(evaluate(be->right)); + } + case Expr::Xor: { + const BinaryExpr *be = cast(e); + return evaluate(be->left).binaryXor(evaluate(be->right)); + } + case Expr::Shl: { + // BinaryExpr *be = cast(e); + // unsigned width = be->left->getWidth(); + // return evaluate(be->left).shl(evaluate(be->right), width); + break; + } + case Expr::LShr: { + // BinaryExpr *be = cast(e); + // unsigned width = be->left->getWidth(); + // return evaluate(be->left).lshr(evaluate(be->right), width); + break; + } + case Expr::AShr: { + // BinaryExpr *be = cast(e); + // unsigned width = be->left->getWidth(); + // return evaluate(be->left).ashr(evaluate(be->right), width); + break; + } + + // Comparison + + case Expr::Eq: { + const BinaryExpr *be = cast(e); + T left = evaluate(be->left); + T right = evaluate(be->right); + + if (left.mustEqual(right)) { + return T(1); + } else if (!left.mayEqual(right)) { + return T(0); + } + break; + } + + case Expr::Ult: { + const BinaryExpr *be = cast(e); + T left = evaluate(be->left); + T right = evaluate(be->right); + + if (left.max() < right.min()) { + return T(1); + } else if (left.min() >= right.max()) { + return T(0); + } + break; + } + case Expr::Ule: { + const BinaryExpr *be = cast(e); + T left = evaluate(be->left); + T right = evaluate(be->right); + + if (left.max() <= right.min()) { + return T(1); + } else if (left.min() > right.max()) { + return T(0); + } + break; + } + case Expr::Slt: { + const BinaryExpr *be = cast(e); + T left = evaluate(be->left); + T right = evaluate(be->right); + unsigned bits = be->left->getWidth(); + + if (left.maxSigned(bits) < right.minSigned(bits)) { + return T(1); + } else if (left.minSigned(bits) >= right.maxSigned(bits)) { + return T(0); + } + break; + } + case Expr::Sle: { + const BinaryExpr *be = cast(e); + T left = evaluate(be->left); + T right = evaluate(be->right); + unsigned bits = be->left->getWidth(); + + if (left.maxSigned(bits) <= right.minSigned(bits)) { + return T(1); + } else if (left.minSigned(bits) > right.maxSigned(bits)) { + return T(0); + } + break; + } + + case Expr::Ne: + case Expr::Ugt: + case Expr::Uge: + case Expr::Sgt: + case Expr::Sge: + assert(0 && "invalid expressions (uncanonicalized)"); + + default: + break; + } + + return T(0, bits64::maxValueOfNBits(e->getWidth())); +} + +} + +#endif /* KLEE_EXPRRANGEEVALUATOR_H */ diff --git a/include/klee/Expr/ExprSMTLIBPrinter.h b/include/klee/Expr/ExprSMTLIBPrinter.h new file mode 100644 index 00000000..b042bfeb --- /dev/null +++ b/include/klee/Expr/ExprSMTLIBPrinter.h @@ -0,0 +1,387 @@ +//===-- ExprSMTLIBPrinter.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_EXPRSMTLIBPRINTER_H +#define KLEE_EXPRSMTLIBPRINTER_H + +#include +#include +#include +#include + +#include +#include +#include + +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 abbreviates expressions according to its abbreviation mode. +/// +/// 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) + }; + + /// 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 }; + + /// 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; } + + void setAbbreviationMode(AbbreviationMode am) { abbrMode = am; } + + /// 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); + + ~ExprSMTLIBPrinter(); + + /// Print the query to the llvm::raw_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. + void generateOutput(); + + /// Set which SMTLIBv2 logic to use. + /// This only affects what logic is used in the (set-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 ) + /// + /// 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 &a); + + /// \return True if human readable mode is switched on + bool isHumanReadable(); + +protected: + /// Contains the arrays found during scans + std::set usedArrays; + + /// Set of expressions seen during scan. + std::set > seenExprs; + + typedef std::map, 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 orderedBindings; + + /// 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 &e); + + /// Print an expression but cast it to a particular SMTLIBv2 sort first. + void printCastToSort(const ref &e, ExprSMTLIBPrinter::SMTLIB_SORT sort); + + // Resets various internal objects for a new query + void reset(); + + // Scan all constraints and the query + void scanAll(); + + // Print an initial SMTLIBv2 comment before anything else is printed + void printNotice(); + + // Print SMTLIBv2 options e.g. (set-option :option-name ) command + void printOptions(); + + // Print SMTLIBv2 logic to use e.g. (set-logic QF_ABV) + void printSetLogic(); + + // Print SMTLIBv2 assertions for constant arrays + void printArrayDeclarations(); + + // Print SMTLIBv2 for the query optimised for human readability + void printHumanReadableQuery(); + + // 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(); + + void printQueryInSingleAssert(); + + /// Print the SMTLIBv2 command to check satisfiability and also optionally + /// request for values + /// \sa setArrayValuesToGet() + void printAction(); + + /// Print the SMTLIBv2 command to exit + void printExit(); + + /// Print a Constant in the format specified by the current "Constant Display + /// Mode" + void printConstant(const ref &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. + /// \param abbrMode the abbreviation mode to use for this expression + void printExpression(const ref &e, SMTLIB_SORT expectedSort); + + /// Scan Expression recursively for Arrays in expressions. Found arrays are + /// added to + /// the usedArrays vector. + void scan(const ref &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() + * + * 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 + void printReadExpr(const ref &e); + void printExtractExpr(const ref &e); + void printCastExpr(const ref &e); + void printNotEqualExpr(const ref &e); + void printSelectExpr(const ref &e, + ExprSMTLIBPrinter::SMTLIB_SORT s); + void printAShrExpr(const ref &e); + + // For the set of operators that take sort "s" arguments + void printSortArgsExpr(const ref &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 + void printLogicalOrBitVectorExpr(const ref &e, + ExprSMTLIBPrinter::SMTLIB_SORT s); + + /// Recursively prints updatesNodes + 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 + const char *getSMTLIBKeyword(const ref &e); + + void printSeperator(); + + /// Helper function for scan() that scans the expressions of an update node + 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 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; + + // Print a SMTLIBv2 option as a C-string + const char * + getSMTLIBOptionString(ExprSMTLIBPrinter::SMTLIBboolOptions option); + + /// Print expression without top-level abbreviations + void printFullExpression(const ref &e, SMTLIB_SORT expectedSort); + + /// Print an assert statement for the given expr. + void printAssert(const ref &e); + + // Pointer to a vector of Arrays. These will be used for the (get-value () ) + // call. + const std::vector *arraysToCallGetValueOn; + + ConstantDisplayMode cdm; + AbbreviationMode abbrMode; +}; +} + +#endif /* KLEE_EXPRSMTLIBPRINTER_H */ diff --git a/include/klee/Expr/ExprUtil.h b/include/klee/Expr/ExprUtil.h new file mode 100644 index 00000000..c6b2c2d7 --- /dev/null +++ b/include/klee/Expr/ExprUtil.h @@ -0,0 +1,52 @@ +//===-- ExprUtil.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_EXPRUTIL_H +#define KLEE_EXPRUTIL_H + +#include "klee/Expr/ExprVisitor.h" + +#include + +namespace klee { + class Array; + class Expr; + class ReadExpr; + template class ref; + + /// Find all ReadExprs used in the expression DAG. If visitUpdates + /// is true then this will including those reachable by traversing + /// update lists. Note that this may be slow and return a large + /// number of results. + void findReads(ref e, + bool visitUpdates, + std::vector< ref > &result); + + /// Return a list of all unique symbolic objects referenced by the given + /// expression. + void findSymbolicObjects(ref e, + std::vector &results); + + /// Return a list of all unique symbolic objects referenced by the + /// given expression range. + template + void findSymbolicObjects(InputIterator begin, + InputIterator end, + std::vector &results); + + class ConstantArrayFinder : public ExprVisitor { + protected: + ExprVisitor::Action visitRead(const ReadExpr &re); + + public: + std::set results; + }; +} + +#endif /* KLEE_EXPRUTIL_H */ diff --git a/include/klee/Expr/ExprVisitor.h b/include/klee/Expr/ExprVisitor.h new file mode 100644 index 00000000..03d4d77d --- /dev/null +++ b/include/klee/Expr/ExprVisitor.h @@ -0,0 +1,98 @@ +//===-- ExprVisitor.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_EXPRVISITOR_H +#define KLEE_EXPRVISITOR_H + +#include "ExprHashMap.h" + +namespace klee { + class ExprVisitor { + protected: + // typed variant, but non-virtual for efficiency + class Action { + public: + enum Kind { SkipChildren, DoChildren, ChangeTo }; + + private: + // Action() {} + Action(Kind _kind) + : kind(_kind), argument(ConstantExpr::alloc(0, Expr::Bool)) {} + Action(Kind _kind, const ref &_argument) + : kind(_kind), argument(_argument) {} + + friend class ExprVisitor; + + public: + Kind kind; + ref argument; + + static Action changeTo(const ref &expr) { + return Action(ChangeTo,expr); + } + static Action doChildren() { return Action(DoChildren); } + static Action skipChildren() { return Action(SkipChildren); } + }; + + protected: + explicit + ExprVisitor(bool _recursive=false) : recursive(_recursive) {} + virtual ~ExprVisitor() {} + + virtual Action visitExpr(const Expr&); + virtual Action visitExprPost(const Expr&); + + virtual Action visitNotOptimized(const NotOptimizedExpr&); + virtual Action visitRead(const ReadExpr&); + virtual Action visitSelect(const SelectExpr&); + virtual Action visitConcat(const ConcatExpr&); + virtual Action visitExtract(const ExtractExpr&); + virtual Action visitZExt(const ZExtExpr&); + virtual Action visitSExt(const SExtExpr&); + virtual Action visitAdd(const AddExpr&); + virtual Action visitSub(const SubExpr&); + virtual Action visitMul(const MulExpr&); + virtual Action visitUDiv(const UDivExpr&); + virtual Action visitSDiv(const SDivExpr&); + virtual Action visitURem(const URemExpr&); + virtual Action visitSRem(const SRemExpr&); + virtual Action visitNot(const NotExpr&); + virtual Action visitAnd(const AndExpr&); + virtual Action visitOr(const OrExpr&); + virtual Action visitXor(const XorExpr&); + virtual Action visitShl(const ShlExpr&); + virtual Action visitLShr(const LShrExpr&); + virtual Action visitAShr(const AShrExpr&); + virtual Action visitEq(const EqExpr&); + virtual Action visitNe(const NeExpr&); + virtual Action visitUlt(const UltExpr&); + virtual Action visitUle(const UleExpr&); + virtual Action visitUgt(const UgtExpr&); + virtual Action visitUge(const UgeExpr&); + virtual Action visitSlt(const SltExpr&); + virtual Action visitSle(const SleExpr&); + virtual Action visitSgt(const SgtExpr&); + virtual Action visitSge(const SgeExpr&); + + private: + typedef ExprHashMap< ref > visited_ty; + visited_ty visited; + bool recursive; + + ref visitActual(const ref &e); + + public: + // apply the visitor to the expression and return a possibly + // modified new expression. + ref visit(const ref &e); + }; + +} + +#endif /* KLEE_EXPRVISITOR_H */ diff --git a/include/klee/Expr/Parser/Lexer.h b/include/klee/Expr/Parser/Lexer.h new file mode 100644 index 00000000..14ae7f85 --- /dev/null +++ b/include/klee/Expr/Parser/Lexer.h @@ -0,0 +1,121 @@ +//===-- Lexer.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_LEXER_H +#define KLEE_LEXER_H + +#include + +namespace llvm { + class MemoryBuffer; +} + +namespace klee { +namespace expr { + struct Token { + enum Kind { + At, ///< '@' + Arrow, ///< '->' + Colon, ///< ':' + Comma, ///< ',' + Comment, ///< #[^\n]+ + EndOfFile, ///< + Equals, ///< ' = ' + Identifier, ///< [a-zA-Z_][a-zA-Z0-9._]* + KWArray, ///< 'array' + KWFalse, ///< 'false' + KWQuery, ///< 'query' + KWReserved, ///< fp[0-9]+([.].*)?, i[0-9]+ + KWSymbolic, ///< 'symbolic' + KWTrue, ///< 'true' + KWWidth, ///< w[0-9]+ + LBrace, ///< '{' + LParen, ///< '(' + LSquare, ///< '[' + Number, ///< [+-]?[0-9][a-zA-Z0-9_]+ + RBrace, ///< '}' + RParen, ///< ')' + RSquare, ///< ']' + Semicolon, ///< ';' + Unknown, ///< + + KWKindFirst=KWArray, + KWKindLast=KWWidth + }; + + Kind kind; /// The token kind. + const char *start; /// The beginning of the token string. + unsigned length; /// The length of the token. + unsigned line; /// The line number of the start of this token. + unsigned column; /// The column number at the start of + /// this token. + + /// getKindName - The name of this token's kind. + const char *getKindName() const; + + /// getString - The string spanned by this token. This is not + /// particularly efficient, use start and length when reasonable. + std::string getString() const { return std::string(start, length); } + + /// isKeyword - True if this token is a keyword. + bool isKeyword() const { + return kind >= KWKindFirst && kind <= KWKindLast; + } + + // dump - Dump the token to stderr. + void dump(); + + Token() : kind(Unknown), start(nullptr) {} + }; + + /// Lexer - Interface for lexing tokens from a .kquery language file. + class Lexer { + const char *BufferPos; /// The current lexer position. + const char *BufferEnd; /// The buffer end position. + unsigned LineNumber; /// The current line. + unsigned ColumnNumber; /// The current column. + + /// GetNextChar - Eat a character or -1 from the stream. + int GetNextChar(); + + /// PeekNextChar - Return the next character without consuming it + /// from the stream. This does not perform newline + /// canonicalization. + int PeekNextChar(); + + /// SetTokenKind - Set the token kind and length (using the + /// token's start pointer, which must have been initialized). + Token &SetTokenKind(Token &Result, Token::Kind k); + + /// SetTokenKind - Set an identifiers token kind. This has the + /// same requirements as SetTokenKind and additionally takes care + /// of keyword recognition. + Token &SetIdentifierTokenKind(Token &Result); + + void SkipToEndOfLine(); + + /// LexNumber - Lex a number which does not have a base specifier. + Token &LexNumber(Token &Result); + + /// LexIdentifier - Lex an identifier. + Token &LexIdentifier(Token &Result); + + public: + explicit Lexer(const llvm::MemoryBuffer *_buf); + ~Lexer(); + + /// Lex - Return the next token from the file or EOF continually + /// when the end of the file is reached. The input argument is + /// used as the result, for convenience. + Token &Lex(Token &Result); + }; +} +} + +#endif /* KLEE_LEXER_H */ diff --git a/include/klee/Expr/Parser/Parser.h b/include/klee/Expr/Parser/Parser.h new file mode 100644 index 00000000..c1888e26 --- /dev/null +++ b/include/klee/Expr/Parser/Parser.h @@ -0,0 +1,237 @@ +//===-- Parser.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_PARSER_H +#define KLEE_PARSER_H + +#include "klee/Expr/Expr.h" + +#include +#include + +namespace llvm { + class MemoryBuffer; +} + +namespace klee { + class ExprBuilder; + +namespace expr { + // These are the language types we manipulate. + typedef ref ExprHandle; + typedef UpdateList VersionHandle; + + /// Identifier - Wrapper for a uniqued string. + struct Identifier { + const std::string Name; + + public: + Identifier(const std::string _Name) : Name(_Name) {} + }; + + // FIXME: Do we have a use for tracking source locations? + + /// Decl - Base class for top level declarations. + class Decl { + public: + enum DeclKind { + ArrayDeclKind, + ExprVarDeclKind, + VersionVarDeclKind, + QueryCommandDeclKind, + + DeclKindLast = QueryCommandDeclKind, + VarDeclKindFirst = ExprVarDeclKind, + VarDeclKindLast = VersionVarDeclKind, + CommandDeclKindFirst = QueryCommandDeclKind, + CommandDeclKindLast = QueryCommandDeclKind + }; + + private: + DeclKind Kind; + + public: + Decl(DeclKind _Kind); + virtual ~Decl() {} + + /// getKind - Get the decl kind. + DeclKind getKind() const { return Kind; } + + /// dump - Dump the AST node to stderr. + virtual void dump() = 0; + + static bool classof(const Decl *) { return true; } + }; + + /// ArrayDecl - Array declarations. + /// + /// For example: + /// array obj[] : w32 -> w8 = symbolic + /// array obj[32] : w32 -> w8 = [ ... ] + class ArrayDecl : public Decl { + public: + /// Name - The name of this array. + const Identifier *Name; + + /// Domain - The width of indices. + const unsigned Domain; + + /// Range - The width of array contents. + const unsigned Range; + + /// Root - The root array object defined by this decl. + const Array *Root; + + public: + ArrayDecl(const Identifier *_Name, uint64_t _Size, + unsigned _Domain, unsigned _Range, + const Array *_Root) + : Decl(ArrayDeclKind), Name(_Name), + Domain(_Domain), Range(_Range), + Root(_Root) { + } + + virtual void dump(); + + static bool classof(const Decl *D) { + return D->getKind() == Decl::ArrayDeclKind; + } + static bool classof(const ArrayDecl *) { return true; } + }; + + /// VarDecl - Variable declarations, used to associate names to + /// expressions or array versions outside of expressions. + /// + /// For example: + // FIXME: What syntax are we going to use for this? We need it. + class VarDecl : public Decl { + public: + const Identifier *Name; + + static bool classof(const Decl *D) { + return (Decl::VarDeclKindFirst <= D->getKind() && + D->getKind() <= Decl::VarDeclKindLast); + } + static bool classof(const VarDecl *) { return true; } + }; + + /// ExprVarDecl - Expression variable declarations. + class ExprVarDecl : public VarDecl { + public: + ExprHandle Value; + + static bool classof(const Decl *D) { + return D->getKind() == Decl::ExprVarDeclKind; + } + static bool classof(const ExprVarDecl *) { return true; } + }; + + /// VersionVarDecl - Array version variable declarations. + class VersionVarDecl : public VarDecl { + public: + VersionHandle Value; + + static bool classof(const Decl *D) { + return D->getKind() == Decl::VersionVarDeclKind; + } + static bool classof(const VersionVarDecl *) { return true; } + }; + + /// CommandDecl - Base class for language commands. + class CommandDecl : public Decl { + public: + CommandDecl(DeclKind _Kind) : Decl(_Kind) {} + + static bool classof(const Decl *D) { + return (Decl::CommandDeclKindFirst <= D->getKind() && + D->getKind() <= Decl::CommandDeclKindLast); + } + static bool classof(const CommandDecl *) { return true; } + }; + + /// QueryCommand - Query commands. + /// + /// (query [ ... constraints ... ] expression) + /// (query [ ... constraints ... ] expression values) + /// (query [ ... constraints ... ] expression values objects) + class QueryCommand : public CommandDecl { + public: + // FIXME: One issue with STP... should we require the FE to + // guarantee that these are consistent? That is a cornerstone of + // being able to do independence. We may want this as a flag, if + // we are to interface with things like SMT. + + /// Constraints - The list of constraints to assume for this + /// expression. + const std::vector Constraints; + + /// Query - The expression being queried. + ExprHandle Query; + + /// Values - The expressions for which counterexamples should be + /// given if the query is invalid. + const std::vector Values; + + /// Objects - Symbolic arrays whose initial contents should be + /// given if the query is invalid. + const std::vector Objects; + + public: + QueryCommand(const std::vector &_Constraints, + ExprHandle _Query, + const std::vector &_Values, + const std::vector &_Objects + ) + : CommandDecl(QueryCommandDeclKind), + Constraints(_Constraints), + Query(_Query), + Values(_Values), + Objects(_Objects) {} + + virtual void dump(); + + static bool classof(const Decl *D) { + return D->getKind() == QueryCommandDeclKind; + } + static bool classof(const QueryCommand *) { return true; } + }; + + /// Parser - Public interface for parsing a .kquery language file. + class Parser { + protected: + Parser(); + public: + virtual ~Parser(); + + /// SetMaxErrors - Suppress anything beyond the first N errors. + virtual void SetMaxErrors(unsigned N) = 0; + + /// GetNumErrors - Return the number of encountered errors. + virtual unsigned GetNumErrors() const = 0; + + /// ParseTopLevelDecl - Parse and return a top level declaration, + /// which the caller assumes ownership of. + /// + /// \return NULL indicates the end of the file has been reached. + virtual Decl *ParseTopLevelDecl() = 0; + + /// CreateParser - Create a parser implementation for the given + /// MemoryBuffer. + /// + /// \arg Name - The name to use in diagnostic messages. + /// \arg MB - The input data. + /// \arg Builder - The expression builder to use for constructing + /// expressions. + static Parser *Create(const std::string Name, const llvm::MemoryBuffer *MB, + ExprBuilder *Builder, bool ClearArrayAfterQuery); + }; +} +} + +#endif /* KLEE_PARSER_H */ diff --git a/include/klee/ExprBuilder.h b/include/klee/ExprBuilder.h deleted file mode 100644 index 4a2c5cf4..00000000 --- a/include/klee/ExprBuilder.h +++ /dev/null @@ -1,91 +0,0 @@ -//===-- ExprBuilder.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_EXPRBUILDER_H -#define KLEE_EXPRBUILDER_H - -#include "Expr.h" - -namespace klee { - /// ExprBuilder - Base expression builder class. - class ExprBuilder { - protected: - ExprBuilder(); - - public: - virtual ~ExprBuilder(); - - // Expressions - - virtual ref Constant(const llvm::APInt &Value) = 0; - virtual ref NotOptimized(const ref &Index) = 0; - virtual ref Read(const UpdateList &Updates, - const ref &Index) = 0; - virtual ref Select(const ref &Cond, - const ref &LHS, const ref &RHS) = 0; - virtual ref Concat(const ref &LHS, const ref &RHS) = 0; - virtual ref Extract(const ref &LHS, - unsigned Offset, Expr::Width W) = 0; - virtual ref ZExt(const ref &LHS, Expr::Width W) = 0; - virtual ref SExt(const ref &LHS, Expr::Width W) = 0; - virtual ref Add(const ref &LHS, const ref &RHS) = 0; - virtual ref Sub(const ref &LHS, const ref &RHS) = 0; - virtual ref Mul(const ref &LHS, const ref &RHS) = 0; - virtual ref UDiv(const ref &LHS, const ref &RHS) = 0; - virtual ref SDiv(const ref &LHS, const ref &RHS) = 0; - virtual ref URem(const ref &LHS, const ref &RHS) = 0; - virtual ref SRem(const ref &LHS, const ref &RHS) = 0; - virtual ref Not(const ref &LHS) = 0; - virtual ref And(const ref &LHS, const ref &RHS) = 0; - virtual ref Or(const ref &LHS, const ref &RHS) = 0; - virtual ref Xor(const ref &LHS, const ref &RHS) = 0; - virtual ref Shl(const ref &LHS, const ref &RHS) = 0; - virtual ref LShr(const ref &LHS, const ref &RHS) = 0; - virtual ref AShr(const ref &LHS, const ref &RHS) = 0; - virtual ref Eq(const ref &LHS, const ref &RHS) = 0; - virtual ref Ne(const ref &LHS, const ref &RHS) = 0; - virtual ref Ult(const ref &LHS, const ref &RHS) = 0; - virtual ref Ule(const ref &LHS, const ref &RHS) = 0; - virtual ref Ugt(const ref &LHS, const ref &RHS) = 0; - virtual ref Uge(const ref &LHS, const ref &RHS) = 0; - virtual ref Slt(const ref &LHS, const ref &RHS) = 0; - virtual ref Sle(const ref &LHS, const ref &RHS) = 0; - virtual ref Sgt(const ref &LHS, const ref &RHS) = 0; - virtual ref Sge(const ref &LHS, const ref &RHS) = 0; - - // Utility functions - - ref False() { return ConstantExpr::alloc(0, Expr::Bool); } - - ref True() { return ConstantExpr::alloc(1, Expr::Bool); } - - ref Constant(uint64_t Value, Expr::Width W) { - return Constant(llvm::APInt(W, Value)); - } - }; - - /// createDefaultExprBuilder - Create an expression builder which does no - /// folding. - ExprBuilder *createDefaultExprBuilder(); - - /// createConstantFoldingExprBuilder - Create an expression builder which - /// folds constant expressions. - /// - /// Base - The base builder to use when constructing expressions. - ExprBuilder *createConstantFoldingExprBuilder(ExprBuilder *Base); - - /// createSimplifyingExprBuilder - Create an expression builder which attemps - /// to fold redundant expressions and normalize expressions for improved - /// caching. - /// - /// Base - The base builder to use when constructing expressions. - ExprBuilder *createSimplifyingExprBuilder(ExprBuilder *Base); -} - -#endif /* KLEE_EXPRBUILDER_H */ diff --git a/include/klee/Internal/Module/Cell.h b/include/klee/Internal/Module/Cell.h index 691c1c89..abdce3f6 100644 --- a/include/klee/Internal/Module/Cell.h +++ b/include/klee/Internal/Module/Cell.h @@ -10,7 +10,7 @@ #ifndef KLEE_CELL_H #define KLEE_CELL_H -#include +#include namespace klee { class MemoryObject; diff --git a/include/klee/Solver.h b/include/klee/Solver.h index 476fb732..f320a5b6 100644 --- a/include/klee/Solver.h +++ b/include/klee/Solver.h @@ -10,7 +10,7 @@ #ifndef KLEE_SOLVER_H #define KLEE_SOLVER_H -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/SolverCmdLine.h" #include "klee/Internal/System/Time.h" diff --git a/include/klee/util/ArrayCache.h b/include/klee/util/ArrayCache.h deleted file mode 100644 index bec6e15a..00000000 --- a/include/klee/util/ArrayCache.h +++ /dev/null @@ -1,81 +0,0 @@ -//===-- ArrayCache.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_ARRAYCACHE_H -#define KLEE_ARRAYCACHE_H - -#include "klee/Expr.h" -#include "klee/util/ArrayExprHash.h" // For klee::ArrayHashFn - -// FIXME: Remove this hack when we switch to C++11 -#ifdef _LIBCPP_VERSION -#include -#define unordered_set std::unordered_set -#else -#include -#define unordered_set std::tr1::unordered_set -#endif - -#include -#include - -namespace klee { - -struct EquivArrayCmpFn { - bool operator()(const Array *array1, const Array *array2) const { - if (array1 == NULL || array2 == NULL) - return false; - return (array1->size == array2->size) && (array1->name == array2->name); - } -}; - -/// Provides an interface for creating and destroying Array objects. -class ArrayCache { -public: - ArrayCache() {} - ~ArrayCache(); - /// Create an Array object. - // - /// Symbolic Arrays are cached so that only one instance exists. This - /// provides a limited form of "alpha-renaming". Constant arrays are not - /// cached. - /// - /// This class retains ownership of Array object so that upon destruction - /// of this object all allocated Array objects are deleted. - /// - /// \param _name The name of the array - /// \param _size The size of the array in bytes - /// \param constantValuesBegin A pointer to the beginning of a block of - // memory that constains a ``ref`` (i.e. concrete values - // for the //array). This should be NULL for symbolic arrays. - /// for symbolic arrays. - /// \param constantValuesEnd A pointer +1 pass the end of a block of memory - /// that contains a ``ref``. This should be NULL for a - /// symbolic array. - /// \param _domain The size of the domain (i.e. the bitvector used to index - /// the array) - /// \param _range The size of range (i.e. the bitvector that is indexed to) - const Array *CreateArray(const std::string &_name, uint64_t _size, - const ref *constantValuesBegin = 0, - const ref *constantValuesEnd = 0, - Expr::Width _domain = Expr::Int32, - Expr::Width _range = Expr::Int8); - -private: - typedef unordered_set ArrayHashMap; - ArrayHashMap cachedSymbolicArrays; - typedef std::vector ArrayPtrVec; - ArrayPtrVec concreteArrays; -}; -} - -#undef unordered_set - -#endif /* KLEE_ARRAYCACHE_H */ diff --git a/include/klee/util/ArrayExprHash.h b/include/klee/util/ArrayExprHash.h deleted file mode 100644 index 05cb8692..00000000 --- a/include/klee/util/ArrayExprHash.h +++ /dev/null @@ -1,139 +0,0 @@ -//===-- ArrayExprHash.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_ARRAYEXPRHASH_H -#define KLEE_ARRAYEXPRHASH_H - -#include "klee/Expr.h" -#include "klee/TimerStatIncrementer.h" -#include "klee/SolverStats.h" - -#include - -#include - -namespace klee { - -struct ArrayHashFn { - unsigned operator()(const Array* array) const { - return(array ? array->hash() : 0); - } -}; - -struct ArrayCmpFn { - bool operator()(const Array* array1, const Array* array2) const { - return(array1 == array2); - } -}; - -struct UpdateNodeHashFn { - unsigned operator()(const UpdateNode* un) const { - return(un ? un->hash() : 0); - } -}; - -struct UpdateNodeCmpFn { - bool operator()(const UpdateNode* un1, const UpdateNode* un2) const { - return(un1 == un2); - } -}; - -template -class ArrayExprHash { -public: - - ArrayExprHash() {}; - // Note: Extend the class and overload the destructor if the objects of type T - // that are to be hashed need to be explicitly destroyed - // As an example, see class STPArrayExprHash - virtual ~ArrayExprHash() {}; - - bool lookupArrayExpr(const Array* array, T& exp) const; - void hashArrayExpr(const Array* array, T& exp); - - bool lookupUpdateNodeExpr(const UpdateNode* un, T& exp) const; - void hashUpdateNodeExpr(const UpdateNode* un, T& exp); - -protected: - typedef std::unordered_map ArrayHash; - typedef typename ArrayHash::iterator ArrayHashIter; - typedef typename ArrayHash::const_iterator ArrayHashConstIter; - - typedef std::unordered_map UpdateNodeHash; - typedef typename UpdateNodeHash::iterator UpdateNodeHashIter; - typedef typename UpdateNodeHash::const_iterator UpdateNodeHashConstIter; - - ArrayHash _array_hash; - UpdateNodeHash _update_node_hash; -}; - - -template -bool ArrayExprHash::lookupArrayExpr(const Array* array, T& exp) const { - bool res = false; - -#ifdef KLEE_ARRAY_DEBUG - TimerStatIncrementer t(stats::arrayHashTime); -#endif - - assert(array); - ArrayHashConstIter it = _array_hash.find(array); - if (it != _array_hash.end()) { - exp = it->second; - res = true; - } - return res; -} - -template -void ArrayExprHash::hashArrayExpr(const Array* array, T& exp) { - -#ifdef KLEE_ARRAY_DEBUG - TimerStatIncrementer t(stats::arrayHashTime); -#endif - - assert(array); - _array_hash[array] = exp; -} - -template -bool ArrayExprHash::lookupUpdateNodeExpr(const UpdateNode* un, T& exp) const -{ - bool res = false; - -#ifdef KLEE_ARRAY_DEBUG - TimerStatIncrementer t(stats::arrayHashTime); -#endif - - assert(un); - UpdateNodeHashConstIter it = _update_node_hash.find(un); - if (it != _update_node_hash.end()) { - exp = it->second; - res = true; - } - return res; -} - -template -void ArrayExprHash::hashUpdateNodeExpr(const UpdateNode* un, T& exp) -{ -#ifdef KLEE_ARRAY_DEBUG - TimerStatIncrementer t(stats::arrayHashTime); -#endif - - assert(un); - _update_node_hash[un] = exp; -} - -} - -#undef unordered_map -#undef unordered_set - -#endif /* KLEE_ARRAYEXPRHASH_H */ diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h deleted file mode 100644 index 8d082791..00000000 --- a/include/klee/util/Assignment.h +++ /dev/null @@ -1,101 +0,0 @@ -//===-- Assignment.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_ASSIGNMENT_H -#define KLEE_ASSIGNMENT_H - -#include - -#include "klee/util/ExprEvaluator.h" - -// FIXME: Rename? - -namespace klee { - class Array; - - class Assignment { - public: - typedef std::map > bindings_ty; - - bool allowFreeValues; - bindings_ty bindings; - - public: - Assignment(bool _allowFreeValues=false) - : allowFreeValues(_allowFreeValues) {} - Assignment(const std::vector &objects, - std::vector< std::vector > &values, - bool _allowFreeValues=false) - : allowFreeValues(_allowFreeValues){ - std::vector< std::vector >::iterator valIt = - values.begin(); - for (std::vector::const_iterator it = objects.begin(), - ie = objects.end(); it != ie; ++it) { - const Array *os = *it; - std::vector &arr = *valIt; - bindings.insert(std::make_pair(os, arr)); - ++valIt; - } - } - - ref evaluate(const Array *mo, unsigned index) const; - ref evaluate(ref e); - void createConstraintsFromAssignment(std::vector > &out) const; - - template - bool satisfies(InputIterator begin, InputIterator end); - void dump(); - }; - - class AssignmentEvaluator : public ExprEvaluator { - const Assignment &a; - - protected: - ref getInitialValue(const Array &mo, unsigned index) { - return a.evaluate(&mo, index); - } - - public: - AssignmentEvaluator(const Assignment &_a) : a(_a) {} - }; - - /***/ - - inline ref Assignment::evaluate(const Array *array, - unsigned index) const { - assert(array); - bindings_ty::const_iterator it = bindings.find(array); - if (it!=bindings.end() && indexsecond.size()) { - return ConstantExpr::alloc(it->second[index], array->getRange()); - } else { - if (allowFreeValues) { - return ReadExpr::create(UpdateList(array, 0), - ConstantExpr::alloc(index, array->getDomain())); - } else { - return ConstantExpr::alloc(0, array->getRange()); - } - } - } - - inline ref Assignment::evaluate(ref e) { - AssignmentEvaluator v(*this); - return v.visit(e); - } - - template - inline bool Assignment::satisfies(InputIterator begin, InputIterator end) { - AssignmentEvaluator v(*this); - for (; begin!=end; ++begin) - if (!v.visit(*begin)->isTrue()) - return false; - return true; - } -} - -#endif /* KLEE_ASSIGNMENT_H */ diff --git a/include/klee/util/ExprEvaluator.h b/include/klee/util/ExprEvaluator.h deleted file mode 100644 index ed366f77..00000000 --- a/include/klee/util/ExprEvaluator.h +++ /dev/null @@ -1,42 +0,0 @@ -//===-- ExprEvaluator.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_EXPREVALUATOR_H -#define KLEE_EXPREVALUATOR_H - -#include "klee/Expr.h" -#include "klee/util/ExprVisitor.h" - -namespace klee { - class ExprEvaluator : public ExprVisitor { - protected: - Action evalRead(const UpdateList &ul, unsigned index); - Action visitRead(const ReadExpr &re); - Action visitExpr(const Expr &e); - - Action protectedDivOperation(const BinaryExpr &e); - Action visitUDiv(const UDivExpr &e); - Action visitSDiv(const SDivExpr &e); - Action visitURem(const URemExpr &e); - Action visitSRem(const SRemExpr &e); - Action visitExprPost(const Expr& e); - - public: - ExprEvaluator() {} - - /// getInitialValue - Return the initial value for a symbolic byte. - /// - /// This will only be called for constant arrays if the index is - /// out-of-bounds. If the value is unknown then the user should return a - /// ReadExpr at the initial version of this array. - virtual ref getInitialValue(const Array& os, unsigned index) = 0; - }; -} - -#endif /* KLEE_EXPREVALUATOR_H */ diff --git a/include/klee/util/ExprHashMap.h b/include/klee/util/ExprHashMap.h deleted file mode 100644 index 6477b7c9..00000000 --- a/include/klee/util/ExprHashMap.h +++ /dev/null @@ -1,62 +0,0 @@ -//===-- ExprHashMap.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_EXPRHASHMAP_H -#define KLEE_EXPRHASHMAP_H - -#include "klee/Expr.h" - -#include -#ifdef _LIBCPP_VERSION -#include -#include -#define unordered_map std::unordered_map -#define unordered_set std::unordered_set -#else -#include -#include -#define unordered_map std::tr1::unordered_map -#define unordered_set std::tr1::unordered_set -#endif - -namespace klee { - - namespace util { - struct ExprHash { - unsigned operator()(const ref e) const { - return e->hash(); - } - }; - - struct ExprCmp { - bool operator()(const ref &a, const ref &b) const { - return a==b; - } - }; - } - - template - class ExprHashMap : - - public unordered_map, - T, - klee::util::ExprHash, - klee::util::ExprCmp> { - }; - - typedef unordered_set, - klee::util::ExprHash, - klee::util::ExprCmp> ExprHashSet; - -} - -#undef unordered_map -#undef unordered_set - -#endif /* KLEE_EXPRHASHMAP_H */ diff --git a/include/klee/util/ExprPPrinter.h b/include/klee/util/ExprPPrinter.h deleted file mode 100644 index f2537750..00000000 --- a/include/klee/util/ExprPPrinter.h +++ /dev/null @@ -1,78 +0,0 @@ -//===-- ExprPPrinter.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_EXPRPPRINTER_H -#define KLEE_EXPRPPRINTER_H - -#include "klee/Expr.h" - -namespace llvm { - class raw_ostream; -} -namespace klee { - class ConstraintManager; - - class ExprPPrinter { - protected: - ExprPPrinter() {} - - public: - 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 &e) = 0; - virtual void print(const ref &e, unsigned indent=0) = 0; - - // utility methods - - template - void scan(Container c) { - scan(c.begin(), c.end()); - } - - template - void scan(InputIterator it, InputIterator end) { - for (; it!=end; ++it) - scan(*it); - } - - /// printOne - Pretty print a single expression prefixed by a - /// message and followed by a line break. - static void printOne(llvm::raw_ostream &os, const char *message, - const ref &e); - - /// printSingleExpr - Pretty print a single expression. - /// - /// The expression will not be followed by a line break. - /// - /// 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(llvm::raw_ostream &os, const ref &e); - - static void printConstraints(llvm::raw_ostream &os, - const ConstraintManager &constraints); - - static void printQuery(llvm::raw_ostream &os, - const ConstraintManager &constraints, - const ref &q, - const ref *evalExprsBegin = 0, - const ref *evalExprsEnd = 0, - const Array * const* evalArraysBegin = 0, - const Array * const* evalArraysEnd = 0, - bool printArrayDecls = true); - }; - -} - -#endif /* KLEE_EXPRPPRINTER_H */ diff --git a/include/klee/util/ExprRangeEvaluator.h b/include/klee/util/ExprRangeEvaluator.h deleted file mode 100644 index b3011827..00000000 --- a/include/klee/util/ExprRangeEvaluator.h +++ /dev/null @@ -1,285 +0,0 @@ -//===-- ExprRangeEvaluator.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_EXPRRANGEEVALUATOR_H -#define KLEE_EXPRRANGEEVALUATOR_H - -#include "klee/Expr.h" -#include "klee/util/Bits.h" - -namespace klee { - -/* -class ValueType { -public: - ValueType(); // empty range - ValueType(uint64_t value); - ValueType(uint64_t min, uint64_t max); - - bool mustEqual(const uint64_t b); - bool mustEqual(const ValueType &b); - bool mayEqual(const uint64_t b); - bool mayEqual(const ValueType &b); - - bool isFullRange(unsigned width); - - ValueType set_union(ValueType &); - ValueType set_intersection(ValueType &); - ValueType set_difference(ValueType &); - - ValueType binaryAnd(ValueType &); - ValueType binaryOr(ValueType &); - ValueType binaryXor(ValueType &); - ValueType concat(ValueType &, unsigned width); - ValueType add(ValueType &, unsigned width); - ValueType sub(ValueType &, unsigned width); - ValueType mul(ValueType &, unsigned width); - ValueType udiv(ValueType &, unsigned width); - ValueType sdiv(ValueType &, unsigned width); - ValueType urem(ValueType &, unsigned width); - ValueType srem(ValueType &, unsigned width); - - uint64_t min(); - uint64_t max(); - int64_t minSigned(unsigned width); - int64_t maxSigned(unsigned width); -} -*/ - -template -class ExprRangeEvaluator { -protected: - /// getInitialReadRange - Return a range for the initial value of the given - /// array (which may be constant), for the given range of indices. - virtual T getInitialReadRange(const Array &os, T index) = 0; - - T evalRead(const UpdateList &ul, T index); - -public: - ExprRangeEvaluator() {} - virtual ~ExprRangeEvaluator() {} - - T evaluate(const ref &e); -}; - -template -T ExprRangeEvaluator::evalRead(const UpdateList &ul, - T index) { - T res; - - for (const UpdateNode *un=ul.head; un; un=un->next) { - T ui = evaluate(un->index); - - if (ui.mustEqual(index)) { - return res.set_union(evaluate(un->value)); - } else if (ui.mayEqual(index)) { - res = res.set_union(evaluate(un->value)); - if (res.isFullRange(8)) { - return res; - } - } - } - - return res.set_union(getInitialReadRange(*ul.root, index)); -} - -template -T ExprRangeEvaluator::evaluate(const ref &e) { - switch (e->getKind()) { - case Expr::Constant: - return T(cast(e)); - - case Expr::NotOptimized: - break; - - case Expr::Read: { - const ReadExpr *re = cast(e); - T index = evaluate(re->index); - - assert(re->updates.root && re->getWidth() == re->updates.root->range && "unexpected multibyte read"); - - return evalRead(re->updates, index); - } - - case Expr::Select: { - const SelectExpr *se = cast(e); - T cond = evaluate(se->cond); - - if (cond.mustEqual(1)) { - return evaluate(se->trueExpr); - } else if (cond.mustEqual(0)) { - return evaluate(se->falseExpr); - } else { - return evaluate(se->trueExpr).set_union(evaluate(se->falseExpr)); - } - } - - // XXX these should be unrolled to ensure nice inline - case Expr::Concat: { - const Expr *ep = e.get(); - T res(0); - for (unsigned i=0; igetNumKids(); i++) - res = res.concat(evaluate(ep->getKid(i)),8); - return res; - } - - // Arithmetic - - case Expr::Add: { - const BinaryExpr *be = cast(e); - unsigned width = be->left->getWidth(); - return evaluate(be->left).add(evaluate(be->right), width); - } - case Expr::Sub: { - const BinaryExpr *be = cast(e); - unsigned width = be->left->getWidth(); - return evaluate(be->left).sub(evaluate(be->right), width); - } - case Expr::Mul: { - const BinaryExpr *be = cast(e); - unsigned width = be->left->getWidth(); - return evaluate(be->left).mul(evaluate(be->right), width); - } - case Expr::UDiv: { - const BinaryExpr *be = cast(e); - unsigned width = be->left->getWidth(); - return evaluate(be->left).udiv(evaluate(be->right), width); - } - case Expr::SDiv: { - const BinaryExpr *be = cast(e); - unsigned width = be->left->getWidth(); - return evaluate(be->left).sdiv(evaluate(be->right), width); - } - case Expr::URem: { - const BinaryExpr *be = cast(e); - unsigned width = be->left->getWidth(); - return evaluate(be->left).urem(evaluate(be->right), width); - } - case Expr::SRem: { - const BinaryExpr *be = cast(e); - unsigned width = be->left->getWidth(); - return evaluate(be->left).srem(evaluate(be->right), width); - } - - // Binary - - case Expr::And: { - const BinaryExpr *be = cast(e); - return evaluate(be->left).binaryAnd(evaluate(be->right)); - } - case Expr::Or: { - const BinaryExpr *be = cast(e); - return evaluate(be->left).binaryOr(evaluate(be->right)); - } - case Expr::Xor: { - const BinaryExpr *be = cast(e); - return evaluate(be->left).binaryXor(evaluate(be->right)); - } - case Expr::Shl: { - // BinaryExpr *be = cast(e); - // unsigned width = be->left->getWidth(); - // return evaluate(be->left).shl(evaluate(be->right), width); - break; - } - case Expr::LShr: { - // BinaryExpr *be = cast(e); - // unsigned width = be->left->getWidth(); - // return evaluate(be->left).lshr(evaluate(be->right), width); - break; - } - case Expr::AShr: { - // BinaryExpr *be = cast(e); - // unsigned width = be->left->getWidth(); - // return evaluate(be->left).ashr(evaluate(be->right), width); - break; - } - - // Comparison - - case Expr::Eq: { - const BinaryExpr *be = cast(e); - T left = evaluate(be->left); - T right = evaluate(be->right); - - if (left.mustEqual(right)) { - return T(1); - } else if (!left.mayEqual(right)) { - return T(0); - } - break; - } - - case Expr::Ult: { - const BinaryExpr *be = cast(e); - T left = evaluate(be->left); - T right = evaluate(be->right); - - if (left.max() < right.min()) { - return T(1); - } else if (left.min() >= right.max()) { - return T(0); - } - break; - } - case Expr::Ule: { - const BinaryExpr *be = cast(e); - T left = evaluate(be->left); - T right = evaluate(be->right); - - if (left.max() <= right.min()) { - return T(1); - } else if (left.min() > right.max()) { - return T(0); - } - break; - } - case Expr::Slt: { - const BinaryExpr *be = cast(e); - T left = evaluate(be->left); - T right = evaluate(be->right); - unsigned bits = be->left->getWidth(); - - if (left.maxSigned(bits) < right.minSigned(bits)) { - return T(1); - } else if (left.minSigned(bits) >= right.maxSigned(bits)) { - return T(0); - } - break; - } - case Expr::Sle: { - const BinaryExpr *be = cast(e); - T left = evaluate(be->left); - T right = evaluate(be->right); - unsigned bits = be->left->getWidth(); - - if (left.maxSigned(bits) <= right.minSigned(bits)) { - return T(1); - } else if (left.minSigned(bits) > right.maxSigned(bits)) { - return T(0); - } - break; - } - - case Expr::Ne: - case Expr::Ugt: - case Expr::Uge: - case Expr::Sgt: - case Expr::Sge: - assert(0 && "invalid expressions (uncanonicalized)"); - - default: - break; - } - - return T(0, bits64::maxValueOfNBits(e->getWidth())); -} - -} - -#endif /* KLEE_EXPRRANGEEVALUATOR_H */ diff --git a/include/klee/util/ExprSMTLIBPrinter.h b/include/klee/util/ExprSMTLIBPrinter.h deleted file mode 100644 index cf5df1c5..00000000 --- a/include/klee/util/ExprSMTLIBPrinter.h +++ /dev/null @@ -1,386 +0,0 @@ -//===-- ExprSMTLIBPrinter.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_EXPRSMTLIBPRINTER_H -#define KLEE_EXPRSMTLIBPRINTER_H - -#include -#include -#include -#include -#include -#include -#include - -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 abbreviates expressions according to its abbreviation mode. -/// -/// 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) - }; - - /// 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 }; - - /// 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; } - - void setAbbreviationMode(AbbreviationMode am) { abbrMode = am; } - - /// 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); - - ~ExprSMTLIBPrinter(); - - /// Print the query to the llvm::raw_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. - void generateOutput(); - - /// Set which SMTLIBv2 logic to use. - /// This only affects what logic is used in the (set-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 ) - /// - /// 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 &a); - - /// \return True if human readable mode is switched on - bool isHumanReadable(); - -protected: - /// Contains the arrays found during scans - std::set usedArrays; - - /// Set of expressions seen during scan. - std::set > seenExprs; - - typedef std::map, 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 orderedBindings; - - /// 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 &e); - - /// Print an expression but cast it to a particular SMTLIBv2 sort first. - void printCastToSort(const ref &e, ExprSMTLIBPrinter::SMTLIB_SORT sort); - - // Resets various internal objects for a new query - void reset(); - - // Scan all constraints and the query - void scanAll(); - - // Print an initial SMTLIBv2 comment before anything else is printed - void printNotice(); - - // Print SMTLIBv2 options e.g. (set-option :option-name ) command - void printOptions(); - - // Print SMTLIBv2 logic to use e.g. (set-logic QF_ABV) - void printSetLogic(); - - // Print SMTLIBv2 assertions for constant arrays - void printArrayDeclarations(); - - // Print SMTLIBv2 for the query optimised for human readability - void printHumanReadableQuery(); - - // 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(); - - void printQueryInSingleAssert(); - - /// Print the SMTLIBv2 command to check satisfiability and also optionally - /// request for values - /// \sa setArrayValuesToGet() - void printAction(); - - /// Print the SMTLIBv2 command to exit - void printExit(); - - /// Print a Constant in the format specified by the current "Constant Display - /// Mode" - void printConstant(const ref &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. - /// \param abbrMode the abbreviation mode to use for this expression - void printExpression(const ref &e, SMTLIB_SORT expectedSort); - - /// Scan Expression recursively for Arrays in expressions. Found arrays are - /// added to - /// the usedArrays vector. - void scan(const ref &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() - * - * 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 - void printReadExpr(const ref &e); - void printExtractExpr(const ref &e); - void printCastExpr(const ref &e); - void printNotEqualExpr(const ref &e); - void printSelectExpr(const ref &e, - ExprSMTLIBPrinter::SMTLIB_SORT s); - void printAShrExpr(const ref &e); - - // For the set of operators that take sort "s" arguments - void printSortArgsExpr(const ref &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 - void printLogicalOrBitVectorExpr(const ref &e, - ExprSMTLIBPrinter::SMTLIB_SORT s); - - /// Recursively prints updatesNodes - 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 - const char *getSMTLIBKeyword(const ref &e); - - void printSeperator(); - - /// Helper function for scan() that scans the expressions of an update node - 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 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; - - // Print a SMTLIBv2 option as a C-string - const char * - getSMTLIBOptionString(ExprSMTLIBPrinter::SMTLIBboolOptions option); - - /// Print expression without top-level abbreviations - void printFullExpression(const ref &e, SMTLIB_SORT expectedSort); - - /// Print an assert statement for the given expr. - void printAssert(const ref &e); - - // Pointer to a vector of Arrays. These will be used for the (get-value () ) - // call. - const std::vector *arraysToCallGetValueOn; - - ConstantDisplayMode cdm; - AbbreviationMode abbrMode; -}; -} - -#endif /* KLEE_EXPRSMTLIBPRINTER_H */ diff --git a/include/klee/util/ExprUtil.h b/include/klee/util/ExprUtil.h deleted file mode 100644 index 88db15f0..00000000 --- a/include/klee/util/ExprUtil.h +++ /dev/null @@ -1,51 +0,0 @@ -//===-- ExprUtil.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_EXPRUTIL_H -#define KLEE_EXPRUTIL_H - -#include "klee/util/ExprVisitor.h" -#include - -namespace klee { - class Array; - class Expr; - class ReadExpr; - template class ref; - - /// Find all ReadExprs used in the expression DAG. If visitUpdates - /// is true then this will including those reachable by traversing - /// update lists. Note that this may be slow and return a large - /// number of results. - void findReads(ref e, - bool visitUpdates, - std::vector< ref > &result); - - /// Return a list of all unique symbolic objects referenced by the given - /// expression. - void findSymbolicObjects(ref e, - std::vector &results); - - /// Return a list of all unique symbolic objects referenced by the - /// given expression range. - template - void findSymbolicObjects(InputIterator begin, - InputIterator end, - std::vector &results); - - class ConstantArrayFinder : public ExprVisitor { - protected: - ExprVisitor::Action visitRead(const ReadExpr &re); - - public: - std::set results; - }; -} - -#endif /* KLEE_EXPRUTIL_H */ diff --git a/include/klee/util/ExprVisitor.h b/include/klee/util/ExprVisitor.h deleted file mode 100644 index 03d4d77d..00000000 --- a/include/klee/util/ExprVisitor.h +++ /dev/null @@ -1,98 +0,0 @@ -//===-- ExprVisitor.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_EXPRVISITOR_H -#define KLEE_EXPRVISITOR_H - -#include "ExprHashMap.h" - -namespace klee { - class ExprVisitor { - protected: - // typed variant, but non-virtual for efficiency - class Action { - public: - enum Kind { SkipChildren, DoChildren, ChangeTo }; - - private: - // Action() {} - Action(Kind _kind) - : kind(_kind), argument(ConstantExpr::alloc(0, Expr::Bool)) {} - Action(Kind _kind, const ref &_argument) - : kind(_kind), argument(_argument) {} - - friend class ExprVisitor; - - public: - Kind kind; - ref argument; - - static Action changeTo(const ref &expr) { - return Action(ChangeTo,expr); - } - static Action doChildren() { return Action(DoChildren); } - static Action skipChildren() { return Action(SkipChildren); } - }; - - protected: - explicit - ExprVisitor(bool _recursive=false) : recursive(_recursive) {} - virtual ~ExprVisitor() {} - - virtual Action visitExpr(const Expr&); - virtual Action visitExprPost(const Expr&); - - virtual Action visitNotOptimized(const NotOptimizedExpr&); - virtual Action visitRead(const ReadExpr&); - virtual Action visitSelect(const SelectExpr&); - virtual Action visitConcat(const ConcatExpr&); - virtual Action visitExtract(const ExtractExpr&); - virtual Action visitZExt(const ZExtExpr&); - virtual Action visitSExt(const SExtExpr&); - virtual Action visitAdd(const AddExpr&); - virtual Action visitSub(const SubExpr&); - virtual Action visitMul(const MulExpr&); - virtual Action visitUDiv(const UDivExpr&); - virtual Action visitSDiv(const SDivExpr&); - virtual Action visitURem(const URemExpr&); - virtual Action visitSRem(const SRemExpr&); - virtual Action visitNot(const NotExpr&); - virtual Action visitAnd(const AndExpr&); - virtual Action visitOr(const OrExpr&); - virtual Action visitXor(const XorExpr&); - virtual Action visitShl(const ShlExpr&); - virtual Action visitLShr(const LShrExpr&); - virtual Action visitAShr(const AShrExpr&); - virtual Action visitEq(const EqExpr&); - virtual Action visitNe(const NeExpr&); - virtual Action visitUlt(const UltExpr&); - virtual Action visitUle(const UleExpr&); - virtual Action visitUgt(const UgtExpr&); - virtual Action visitUge(const UgeExpr&); - virtual Action visitSlt(const SltExpr&); - virtual Action visitSle(const SleExpr&); - virtual Action visitSgt(const SgtExpr&); - virtual Action visitSge(const SgeExpr&); - - private: - typedef ExprHashMap< ref > visited_ty; - visited_ty visited; - bool recursive; - - ref visitActual(const ref &e); - - public: - // apply the visitor to the expression and return a possibly - // modified new expression. - ref visit(const ref &e); - }; - -} - -#endif /* KLEE_EXPRVISITOR_H */ diff --git a/include/klee/util/PrintContext.h b/include/klee/util/PrintContext.h index 9deaa207..de9094da 100644 --- a/include/klee/util/PrintContext.h +++ b/include/klee/util/PrintContext.h @@ -10,8 +10,10 @@ #ifndef KLEE_PRINTCONTEXT_H #define KLEE_PRINTCONTEXT_H -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" + #include "llvm/Support/raw_ostream.h" + #include #include #include diff --git a/lib/Core/AddressSpace.cpp b/lib/Core/AddressSpace.cpp index fdf9c905..1a88e4ec 100644 --- a/lib/Core/AddressSpace.cpp +++ b/lib/Core/AddressSpace.cpp @@ -12,7 +12,7 @@ #include "Memory.h" #include "TimingSolver.h" -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/TimerStatIncrementer.h" using namespace klee; diff --git a/lib/Core/AddressSpace.h b/lib/Core/AddressSpace.h index d8ba6f36..9e7e414a 100644 --- a/lib/Core/AddressSpace.h +++ b/lib/Core/AddressSpace.h @@ -12,7 +12,7 @@ #include "ObjectHolder.h" -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/Internal/ADT/ImmutableMap.h" #include "klee/Internal/System/Time.h" diff --git a/lib/Core/Context.cpp b/lib/Core/Context.cpp index 8246e631..a74d5446 100644 --- a/lib/Core/Context.cpp +++ b/lib/Core/Context.cpp @@ -9,7 +9,7 @@ #include "Context.h" -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "llvm/IR/Type.h" #include "llvm/IR/DerivedTypes.h" diff --git a/lib/Core/Context.h b/lib/Core/Context.h index b2ea83f1..ecef646e 100644 --- a/lib/Core/Context.h +++ b/lib/Core/Context.h @@ -10,7 +10,7 @@ #ifndef KLEE_CONTEXT_H #define KLEE_CONTEXT_H -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" namespace klee { diff --git a/lib/Core/ExecutionState.cpp b/lib/Core/ExecutionState.cpp index 3bce274c..15003b0e 100644 --- a/lib/Core/ExecutionState.cpp +++ b/lib/Core/ExecutionState.cpp @@ -11,7 +11,7 @@ #include "klee/ExecutionState.h" -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/Internal/Module/Cell.h" #include "klee/Internal/Module/InstructionInfoTable.h" #include "klee/Internal/Module/KInstruction.h" diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp index 330665c0..5590af41 100644 --- a/lib/Core/Executor.cpp +++ b/lib/Core/Executor.cpp @@ -28,7 +28,11 @@ #include "klee/Common.h" #include "klee/Config/Version.h" #include "klee/ExecutionState.h" -#include "klee/Expr.h" +#include "klee/Expr/Assignment.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprPPrinter.h" +#include "klee/Expr/ExprSMTLIBPrinter.h" +#include "klee/Expr/ExprUtil.h" #include "klee/Internal/ADT/KTest.h" #include "klee/Internal/ADT/RNG.h" #include "klee/Internal/Module/Cell.h" @@ -46,10 +50,6 @@ #include "klee/SolverCmdLine.h" #include "klee/SolverStats.h" #include "klee/TimerStatIncrementer.h" -#include "klee/util/Assignment.h" -#include "klee/util/ExprPPrinter.h" -#include "klee/util/ExprSMTLIBPrinter.h" -#include "klee/util/ExprUtil.h" #include "klee/util/GetElementPtrTypeIterator.h" #include "llvm/ADT/SmallPtrSet.h" diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h index eafdc2f7..e2aab56c 100644 --- a/lib/Core/Executor.h +++ b/lib/Core/Executor.h @@ -16,17 +16,18 @@ #define KLEE_EXECUTOR_H #include "klee/ExecutionState.h" -#include "klee/Interpreter.h" +#include "klee/Expr/ArrayCache.h" #include "klee/Internal/Module/Cell.h" #include "klee/Internal/Module/KInstruction.h" #include "klee/Internal/Module/KModule.h" #include "klee/Internal/System/Time.h" -#include "klee/util/ArrayCache.h" -#include "llvm/Support/raw_ostream.h" +#include "klee/Interpreter.h" #include "llvm/ADT/Twine.h" +#include "llvm/Support/raw_ostream.h" #include "../Expr/ArrayExprOptimizer.h" + #include #include #include diff --git a/lib/Core/ExecutorUtil.cpp b/lib/Core/ExecutorUtil.cpp index 7b227eba..15125fe1 100644 --- a/lib/Core/ExecutorUtil.cpp +++ b/lib/Core/ExecutorUtil.cpp @@ -11,14 +11,12 @@ #include "Context.h" -#include "klee/Expr.h" -#include "klee/Interpreter.h" -#include "klee/Solver.h" - #include "klee/Config/Version.h" +#include "klee/Expr/Expr.h" #include "klee/Internal/Module/KModule.h" - #include "klee/Internal/Support/ErrorHandling.h" +#include "klee/Interpreter.h" +#include "klee/Solver.h" #include "llvm/IR/Constants.h" #include "llvm/IR/DataLayout.h" diff --git a/lib/Core/ImpliedValue.cpp b/lib/Core/ImpliedValue.cpp index 90000683..cc001660 100644 --- a/lib/Core/ImpliedValue.cpp +++ b/lib/Core/ImpliedValue.cpp @@ -10,13 +10,12 @@ #include "ImpliedValue.h" #include "Context.h" -#include "klee/Constraints.h" -#include "klee/Expr.h" -#include "klee/Solver.h" -// FIXME: Use APInt. -#include "klee/Internal/Support/IntEvaluation.h" -#include "klee/util/ExprUtil.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprUtil.h" +#include "klee/Internal/Support/IntEvaluation.h" // FIXME: Use APInt +#include "klee/Solver.h" #include #include diff --git a/lib/Core/ImpliedValue.h b/lib/Core/ImpliedValue.h index 2b323c01..5943e41f 100644 --- a/lib/Core/ImpliedValue.h +++ b/lib/Core/ImpliedValue.h @@ -10,7 +10,7 @@ #ifndef KLEE_IMPLIEDVALUE_H #define KLEE_IMPLIEDVALUE_H -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include diff --git a/lib/Core/Memory.cpp b/lib/Core/Memory.cpp index 9348105e..93be1f44 100644 --- a/lib/Core/Memory.cpp +++ b/lib/Core/Memory.cpp @@ -12,11 +12,12 @@ #include "Context.h" #include "MemoryManager.h" #include "ObjectHolder.h" -#include "klee/Expr.h" + +#include "klee/Expr/ArrayCache.h" +#include "klee/Expr/Expr.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/OptionCategories.h" #include "klee/Solver.h" -#include "klee/util/ArrayCache.h" #include "klee/util/BitArray.h" #include "llvm/IR/Function.h" diff --git a/lib/Core/Memory.h b/lib/Core/Memory.h index 3558c96c..dfda433c 100644 --- a/lib/Core/Memory.h +++ b/lib/Core/Memory.h @@ -12,12 +12,13 @@ #include "Context.h" #include "TimingSolver.h" -#include "klee/Expr.h" + +#include "klee/Expr/Expr.h" #include "llvm/ADT/StringExtras.h" -#include #include +#include namespace llvm { class Value; diff --git a/lib/Core/MemoryManager.cpp b/lib/Core/MemoryManager.cpp index dba90f8d..af3a2f26 100644 --- a/lib/Core/MemoryManager.cpp +++ b/lib/Core/MemoryManager.cpp @@ -7,11 +7,12 @@ // //===----------------------------------------------------------------------===// +#include "MemoryManager.h" + #include "CoreStats.h" #include "Memory.h" -#include "MemoryManager.h" -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/Internal/Support/ErrorHandling.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Core/PTree.cpp b/lib/Core/PTree.cpp index e3e38868..732dc817 100644 --- a/lib/Core/PTree.cpp +++ b/lib/Core/PTree.cpp @@ -9,15 +9,13 @@ #include "PTree.h" -#include -#include +#include +#include #include using namespace klee; - /* *** */ - PTree::PTree(const data_type &root) : root(new Node(nullptr, root)) {} std::pair diff --git a/lib/Core/PTree.h b/lib/Core/PTree.h index b13b1d67..3185203f 100644 --- a/lib/Core/PTree.h +++ b/lib/Core/PTree.h @@ -10,7 +10,7 @@ #ifndef KLEE_PTREE_H #define KLEE_PTREE_H -#include +#include namespace klee { class ExecutionState; diff --git a/lib/Core/SeedInfo.cpp b/lib/Core/SeedInfo.cpp index 90de17ff..a896197b 100644 --- a/lib/Core/SeedInfo.cpp +++ b/lib/Core/SeedInfo.cpp @@ -12,8 +12,8 @@ #include "TimingSolver.h" #include "klee/ExecutionState.h" -#include "klee/Expr.h" -#include "klee/util/ExprUtil.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprUtil.h" #include "klee/Internal/ADT/KTest.h" #include "klee/Internal/Support/ErrorHandling.h" diff --git a/lib/Core/SeedInfo.h b/lib/Core/SeedInfo.h index 0d2b6ae0..fb2d025d 100644 --- a/lib/Core/SeedInfo.h +++ b/lib/Core/SeedInfo.h @@ -10,7 +10,7 @@ #ifndef KLEE_SEEDINFO_H #define KLEE_SEEDINFO_H -#include "klee/util/Assignment.h" +#include "klee/Expr/Assignment.h" extern "C" { struct KTest; diff --git a/lib/Core/TimingSolver.h b/lib/Core/TimingSolver.h index 6951a3ad..b08073ab 100644 --- a/lib/Core/TimingSolver.h +++ b/lib/Core/TimingSolver.h @@ -10,7 +10,7 @@ #ifndef KLEE_TIMINGSOLVER_H #define KLEE_TIMINGSOLVER_H -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/Solver.h" #include "klee/Internal/System/Time.h" diff --git a/lib/Expr/ArrayCache.cpp b/lib/Expr/ArrayCache.cpp index b669f237..d4e8ee8f 100644 --- a/lib/Expr/ArrayCache.cpp +++ b/lib/Expr/ArrayCache.cpp @@ -1,4 +1,4 @@ -#include "klee/util/ArrayCache.h" +#include "klee/Expr/ArrayCache.h" namespace klee { diff --git a/lib/Expr/ArrayExprOptimizer.cpp b/lib/Expr/ArrayExprOptimizer.cpp index 43b289e2..1a48adfe 100644 --- a/lib/Expr/ArrayExprOptimizer.cpp +++ b/lib/Expr/ArrayExprOptimizer.cpp @@ -13,10 +13,10 @@ #include "AssignmentGenerator.h" #include "klee/Config/Version.h" -#include "klee/ExprBuilder.h" +#include "klee/Expr/Assignment.h" +#include "klee/Expr/ExprBuilder.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/OptionCategories.h" -#include "klee/util/Assignment.h" #include "klee/util/BitArray.h" #include diff --git a/lib/Expr/ArrayExprOptimizer.h b/lib/Expr/ArrayExprOptimizer.h index 8f6472a4..ca90931d 100644 --- a/lib/Expr/ArrayExprOptimizer.h +++ b/lib/Expr/ArrayExprOptimizer.h @@ -17,7 +17,7 @@ #include #include -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/util/Ref.h" namespace klee { diff --git a/lib/Expr/ArrayExprRewriter.h b/lib/Expr/ArrayExprRewriter.h index a0ee9f1d..098cb0a6 100644 --- a/lib/Expr/ArrayExprRewriter.h +++ b/lib/Expr/ArrayExprRewriter.h @@ -14,7 +14,7 @@ #include #include -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/util/Ref.h" namespace klee { diff --git a/lib/Expr/ArrayExprVisitor.h b/lib/Expr/ArrayExprVisitor.h index bfa75478..a6d9ae46 100644 --- a/lib/Expr/ArrayExprVisitor.h +++ b/lib/Expr/ArrayExprVisitor.h @@ -10,9 +10,9 @@ #ifndef KLEE_ARRAYEXPRVISITOR_H #define KLEE_ARRAYEXPRVISITOR_H -#include "klee/ExprBuilder.h" +#include "klee/Expr/ExprBuilder.h" +#include "klee/Expr/ExprVisitor.h" #include "klee/SolverCmdLine.h" -#include "klee/util/ExprVisitor.h" #include #include diff --git a/lib/Expr/Assigment.cpp b/lib/Expr/Assigment.cpp index d788785a..2fc569cc 100644 --- a/lib/Expr/Assigment.cpp +++ b/lib/Expr/Assigment.cpp @@ -6,7 +6,9 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// -#include "klee/util/Assignment.h" + +#include "klee/Expr/Assignment.h" + namespace klee { void Assignment::dump() { diff --git a/lib/Expr/AssignmentGenerator.cpp b/lib/Expr/AssignmentGenerator.cpp index dc744ba0..acb2dc13 100644 --- a/lib/Expr/AssignmentGenerator.cpp +++ b/lib/Expr/AssignmentGenerator.cpp @@ -9,21 +9,22 @@ #include "AssignmentGenerator.h" -#include -#include +#include "klee/Expr/Assignment.h" +#include "klee/Internal/Support/ErrorHandling.h" +#include "klee/klee.h" + #include #include #include + +#include +#include #include #include #include #include #include -#include "klee/Internal/Support/ErrorHandling.h" -#include "klee/klee.h" -#include "klee/util/Assignment.h" - using namespace klee; bool AssignmentGenerator::generatePartialAssignment(const ref &e, diff --git a/lib/Expr/AssignmentGenerator.h b/lib/Expr/AssignmentGenerator.h index 3bd940e7..173b863e 100644 --- a/lib/Expr/AssignmentGenerator.h +++ b/lib/Expr/AssignmentGenerator.h @@ -10,11 +10,11 @@ #ifndef KLEE_ASSIGNMENTGENERATOR_H #define KLEE_ASSIGNMENTGENERATOR_H -#include - -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/util/Ref.h" +#include + namespace klee { class Assignment; } /* namespace klee */ diff --git a/lib/Expr/Constraints.cpp b/lib/Expr/Constraints.cpp index e033333b..2b5adc4c 100644 --- a/lib/Expr/Constraints.cpp +++ b/lib/Expr/Constraints.cpp @@ -7,12 +7,12 @@ // //===----------------------------------------------------------------------===// -#include "klee/Constraints.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/ExprPPrinter.h" +#include "klee/Expr/ExprVisitor.h" #include "klee/Internal/Module/KModule.h" #include "klee/OptionCategories.h" -#include "klee/util/ExprPPrinter.h" -#include "klee/util/ExprVisitor.h" #include "llvm/IR/Function.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Expr/Expr.cpp b/lib/Expr/Expr.cpp index 060595d6..6b8dc95f 100644 --- a/lib/Expr/Expr.cpp +++ b/lib/Expr/Expr.cpp @@ -7,14 +7,14 @@ // //===----------------------------------------------------------------------===// -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/Config/Version.h" +#include "klee/Expr/ExprPPrinter.h" // FIXME: We shouldn't need this once fast constant support moves into // Core. If we need to do arithmetic, we probably want to use APInt. #include "klee/Internal/Support/IntEvaluation.h" #include "klee/OptionCategories.h" -#include "klee/util/ExprPPrinter.h" #include "llvm/ADT/Hashing.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Expr/ExprBuilder.cpp b/lib/Expr/ExprBuilder.cpp index d9e20e45..e1cfa2d2 100644 --- a/lib/Expr/ExprBuilder.cpp +++ b/lib/Expr/ExprBuilder.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "klee/ExprBuilder.h" +#include "klee/Expr/ExprBuilder.h" using namespace klee; diff --git a/lib/Expr/ExprEvaluator.cpp b/lib/Expr/ExprEvaluator.cpp index 6b84cd6f..f03d7669 100644 --- a/lib/Expr/ExprEvaluator.cpp +++ b/lib/Expr/ExprEvaluator.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "klee/util/ExprEvaluator.h" +#include "klee/Expr/ExprEvaluator.h" using namespace klee; diff --git a/lib/Expr/ExprPPrinter.cpp b/lib/Expr/ExprPPrinter.cpp index 114c46b4..2ccd7262 100644 --- a/lib/Expr/ExprPPrinter.cpp +++ b/lib/Expr/ExprPPrinter.cpp @@ -7,9 +7,9 @@ // //===----------------------------------------------------------------------===// -#include "klee/util/ExprPPrinter.h" +#include "klee/Expr/ExprPPrinter.h" -#include "klee/Constraints.h" +#include "klee/Expr/Constraints.h" #include "klee/OptionCategories.h" #include "klee/util/PrintContext.h" diff --git a/lib/Expr/ExprSMTLIBPrinter.cpp b/lib/Expr/ExprSMTLIBPrinter.cpp index 06186db2..b83a6af4 100644 --- a/lib/Expr/ExprSMTLIBPrinter.cpp +++ b/lib/Expr/ExprSMTLIBPrinter.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "klee/util/ExprSMTLIBPrinter.h" +#include "klee/Expr/ExprSMTLIBPrinter.h" #include "llvm/Support/Casting.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Expr/ExprUtil.cpp b/lib/Expr/ExprUtil.cpp index 2106b226..911366f3 100644 --- a/lib/Expr/ExprUtil.cpp +++ b/lib/Expr/ExprUtil.cpp @@ -7,12 +7,10 @@ // //===----------------------------------------------------------------------===// -#include "klee/util/ExprUtil.h" -#include "klee/util/ExprHashMap.h" - -#include "klee/Expr.h" - -#include "klee/util/ExprVisitor.h" +#include "klee/Expr/ExprUtil.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprHashMap.h" +#include "klee/Expr/ExprVisitor.h" #include diff --git a/lib/Expr/ExprVisitor.cpp b/lib/Expr/ExprVisitor.cpp index b99cc7e7..a3fa41d8 100644 --- a/lib/Expr/ExprVisitor.cpp +++ b/lib/Expr/ExprVisitor.cpp @@ -7,9 +7,10 @@ // //===----------------------------------------------------------------------===// -#include "klee/util/ExprVisitor.h" +#include "klee/Expr/ExprVisitor.h" + +#include "klee/Expr/Expr.h" -#include "klee/Expr.h" #include "llvm/Support/CommandLine.h" namespace { diff --git a/lib/Expr/Lexer.cpp b/lib/Expr/Lexer.cpp index e250a968..784764bb 100644 --- a/lib/Expr/Lexer.cpp +++ b/lib/Expr/Lexer.cpp @@ -7,7 +7,7 @@ // //===----------------------------------------------------------------------===// -#include "expr/Lexer.h" +#include "klee/Expr/Parser/Lexer.h" #include "llvm/Support/MemoryBuffer.h" #include "llvm/Support/raw_ostream.h" diff --git a/lib/Expr/Parser.cpp b/lib/Expr/Parser.cpp index 479ff6c2..c365002d 100644 --- a/lib/Expr/Parser.cpp +++ b/lib/Expr/Parser.cpp @@ -7,16 +7,14 @@ // //===----------------------------------------------------------------------===// -#include "expr/Parser.h" - -#include "expr/Lexer.h" - #include "klee/Config/Version.h" -#include "klee/Constraints.h" -#include "klee/ExprBuilder.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/ArrayCache.h" +#include "klee/Expr/ExprBuilder.h" +#include "klee/Expr/ExprPPrinter.h" +#include "klee/Expr/Parser/Lexer.h" +#include "klee/Expr/Parser/Parser.h" #include "klee/Solver.h" -#include "klee/util/ExprPPrinter.h" -#include "klee/util/ArrayCache.h" #include "llvm/ADT/APInt.h" #include "llvm/Support/MemoryBuffer.h" diff --git a/lib/Expr/Updates.cpp b/lib/Expr/Updates.cpp index d58a3642..7264ca89 100644 --- a/lib/Expr/Updates.cpp +++ b/lib/Expr/Updates.cpp @@ -7,14 +7,12 @@ // //===----------------------------------------------------------------------===// -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include using namespace klee; -/// - UpdateNode::UpdateNode(const UpdateNode *_next, const ref &_index, const ref &_value) diff --git a/lib/Solver/AssignmentValidatingSolver.cpp b/lib/Solver/AssignmentValidatingSolver.cpp index 82702dbf..b75f982a 100644 --- a/lib/Solver/AssignmentValidatingSolver.cpp +++ b/lib/Solver/AssignmentValidatingSolver.cpp @@ -6,10 +6,12 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// -#include "klee/util/Assignment.h" -#include "klee/Constraints.h" + +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Assignment.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" + #include namespace klee { diff --git a/lib/Solver/CachingSolver.cpp b/lib/Solver/CachingSolver.cpp index a6ca93ac..2eedc616 100644 --- a/lib/Solver/CachingSolver.cpp +++ b/lib/Solver/CachingSolver.cpp @@ -10,8 +10,8 @@ #include "klee/Solver.h" -#include "klee/Constraints.h" -#include "klee/Expr.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" #include "klee/IncompleteSolver.h" #include "klee/SolverImpl.h" diff --git a/lib/Solver/CexCachingSolver.cpp b/lib/Solver/CexCachingSolver.cpp index d2e080d9..5c181dc3 100644 --- a/lib/Solver/CexCachingSolver.cpp +++ b/lib/Solver/CexCachingSolver.cpp @@ -9,17 +9,17 @@ #include "klee/Solver.h" -#include "klee/Constraints.h" -#include "klee/Expr.h" +#include "klee/Expr/Assignment.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprUtil.h" +#include "klee/Expr/ExprVisitor.h" #include "klee/Internal/ADT/MapOfSets.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/OptionCategories.h" #include "klee/SolverImpl.h" #include "klee/SolverStats.h" #include "klee/TimerStatIncrementer.h" -#include "klee/util/Assignment.h" -#include "klee/util/ExprUtil.h" -#include "klee/util/ExprVisitor.h" #include "llvm/Support/CommandLine.h" diff --git a/lib/Solver/FastCexSolver.cpp b/lib/Solver/FastCexSolver.cpp index 5ea6c1d4..9f493cd1 100644 --- a/lib/Solver/FastCexSolver.cpp +++ b/lib/Solver/FastCexSolver.cpp @@ -10,27 +10,25 @@ #define DEBUG_TYPE "cex-solver" #include "klee/Solver.h" -#include "klee/Constraints.h" -#include "klee/Expr.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprEvaluator.h" +#include "klee/Expr/ExprRangeEvaluator.h" +#include "klee/Expr/ExprVisitor.h" #include "klee/IncompleteSolver.h" -#include "klee/util/ExprEvaluator.h" -#include "klee/util/ExprRangeEvaluator.h" -#include "klee/util/ExprVisitor.h" -// FIXME: Use APInt. #include "klee/Internal/Support/Debug.h" -#include "klee/Internal/Support/IntEvaluation.h" +#include "klee/Internal/Support/IntEvaluation.h" // FIXME: Use APInt #include "llvm/Support/raw_ostream.h" -#include + #include #include +#include #include using namespace klee; -/***/ - - // Hacker's Delight, pgs 58-63 +// Hacker's Delight, pgs 58-63 static uint64_t minOR(uint64_t a, uint64_t b, uint64_t c, uint64_t d) { uint64_t temp, m = ((uint64_t) 1)<<63; diff --git a/lib/Solver/IncompleteSolver.cpp b/lib/Solver/IncompleteSolver.cpp index 72fe2a95..e19a71e1 100644 --- a/lib/Solver/IncompleteSolver.cpp +++ b/lib/Solver/IncompleteSolver.cpp @@ -9,7 +9,7 @@ #include "klee/IncompleteSolver.h" -#include "klee/Constraints.h" +#include "klee/Expr/Constraints.h" using namespace klee; using namespace llvm; diff --git a/lib/Solver/IndependentSolver.cpp b/lib/Solver/IndependentSolver.cpp index 447e5575..12017e5c 100644 --- a/lib/Solver/IndependentSolver.cpp +++ b/lib/Solver/IndependentSolver.cpp @@ -10,19 +10,19 @@ #define DEBUG_TYPE "independent-solver" #include "klee/Solver.h" -#include "klee/Expr.h" -#include "klee/Constraints.h" -#include "klee/SolverImpl.h" +#include "klee/Expr/Assignment.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprUtil.h" #include "klee/Internal/Support/Debug.h" - -#include "klee/util/ExprUtil.h" -#include "klee/util/Assignment.h" +#include "klee/SolverImpl.h" #include "llvm/Support/raw_ostream.h" + +#include #include -#include #include -#include +#include using namespace klee; using namespace llvm; diff --git a/lib/Solver/KQueryLoggingSolver.cpp b/lib/Solver/KQueryLoggingSolver.cpp index 0c2ac6dd..27e8ad0b 100644 --- a/lib/Solver/KQueryLoggingSolver.cpp +++ b/lib/Solver/KQueryLoggingSolver.cpp @@ -9,14 +9,12 @@ #include "QueryLoggingSolver.h" -#include "klee/Expr.h" -#include "klee/util/ExprPPrinter.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprPPrinter.h" #include "klee/Internal/System/Time.h" using namespace klee; -/// - class KQueryLoggingSolver : public QueryLoggingSolver { private : diff --git a/lib/Solver/MetaSMTBuilder.h b/lib/Solver/MetaSMTBuilder.h index ffe4608d..3112495d 100644 --- a/lib/Solver/MetaSMTBuilder.h +++ b/lib/Solver/MetaSMTBuilder.h @@ -7,23 +7,17 @@ // //===----------------------------------------------------------------------===// -/* - * MetaSMTBuilder.h - * - * Created on: 8 Aug 2012 - * Author: hpalikar - */ - #ifndef KLEE_METASMTBUILDER_H #define KLEE_METASMTBUILDER_H -#include "klee/Config/config.h" -#include "klee/Expr.h" -#include "klee/util/ExprPPrinter.h" -#include "klee/util/ArrayExprHash.h" -#include "klee/util/ExprHashMap.h" #include "ConstantDivision.h" +#include "klee/Config/config.h" +#include "klee/Expr/ArrayExprHash.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprHashMap.h" +#include "klee/Expr/ExprPPrinter.h" + #ifdef ENABLE_METASMT #include "llvm/Support/CommandLine.h" diff --git a/lib/Solver/MetaSMTSolver.cpp b/lib/Solver/MetaSMTSolver.cpp index dfa78e42..c4ff1f13 100644 --- a/lib/Solver/MetaSMTSolver.cpp +++ b/lib/Solver/MetaSMTSolver.cpp @@ -7,16 +7,17 @@ // //===----------------------------------------------------------------------===// #include "klee/Config/config.h" -#ifdef ENABLE_METASMT +#ifdef ENABLE_METASMT #include "MetaSMTSolver.h" #include "MetaSMTBuilder.h" -#include "klee/Constraints.h" + +#include "klee/Expr/Assignment.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/ExprUtil.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" -#include "klee/util/Assignment.h" -#include "klee/util/ExprUtil.h" #include "llvm/Support/ErrorHandling.h" @@ -51,11 +52,11 @@ #endif #include -#include #include -#include #include #include +#include +#include static unsigned char *shared_memory_ptr; static int shared_memory_id = 0; diff --git a/lib/Solver/SMTLIBLoggingSolver.cpp b/lib/Solver/SMTLIBLoggingSolver.cpp index f734ac38..bfea5c1b 100644 --- a/lib/Solver/SMTLIBLoggingSolver.cpp +++ b/lib/Solver/SMTLIBLoggingSolver.cpp @@ -8,7 +8,8 @@ //===----------------------------------------------------------------------===// #include "QueryLoggingSolver.h" -#include "klee/util/ExprSMTLIBPrinter.h" + +#include "klee/Expr/ExprSMTLIBPrinter.h" using namespace klee; diff --git a/lib/Solver/STPBuilder.cpp b/lib/Solver/STPBuilder.cpp index 0bd5084a..645c8989 100644 --- a/lib/Solver/STPBuilder.cpp +++ b/lib/Solver/STPBuilder.cpp @@ -10,10 +10,10 @@ #ifdef ENABLE_STP #include "STPBuilder.h" -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/Solver.h" -#include "klee/util/Bits.h" #include "klee/SolverStats.h" +#include "klee/util/Bits.h" #include "ConstantDivision.h" diff --git a/lib/Solver/STPBuilder.h b/lib/Solver/STPBuilder.h index cb163384..814046fa 100644 --- a/lib/Solver/STPBuilder.h +++ b/lib/Solver/STPBuilder.h @@ -10,9 +10,9 @@ #ifndef KLEE_STPBUILDER_H #define KLEE_STPBUILDER_H -#include "klee/util/ExprHashMap.h" -#include "klee/util/ArrayExprHash.h" #include "klee/Config/config.h" +#include "klee/Expr/ArrayExprHash.h" +#include "klee/Expr/ExprHashMap.h" #include diff --git a/lib/Solver/STPSolver.cpp b/lib/Solver/STPSolver.cpp index e8b9222f..eb46b6db 100644 --- a/lib/Solver/STPSolver.cpp +++ b/lib/Solver/STPSolver.cpp @@ -9,23 +9,25 @@ #include "klee/Config/config.h" #ifdef ENABLE_STP + #include "STPBuilder.h" #include "STPSolver.h" -#include "klee/Constraints.h" + +#include "klee/Expr/Assignment.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/ExprUtil.h" +#include "klee/Internal/Support/ErrorHandling.h" #include "klee/OptionCategories.h" #include "klee/SolverImpl.h" -#include "klee/Internal/Support/ErrorHandling.h" -#include "klee/util/Assignment.h" -#include "klee/util/ExprUtil.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/Errno.h" #include -#include #include #include #include +#include namespace { diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp index 4f7458c5..6c7361dc 100644 --- a/lib/Solver/Solver.cpp +++ b/lib/Solver/Solver.cpp @@ -8,8 +8,9 @@ //===----------------------------------------------------------------------===// #include "klee/Solver.h" + +#include "klee/Expr/Constraints.h" #include "klee/SolverImpl.h" -#include "klee/Constraints.h" using namespace klee; diff --git a/lib/Solver/ValidatingSolver.cpp b/lib/Solver/ValidatingSolver.cpp index 40a7c9e0..71e6834e 100644 --- a/lib/Solver/ValidatingSolver.cpp +++ b/lib/Solver/ValidatingSolver.cpp @@ -6,9 +6,11 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// -#include "klee/Constraints.h" + +#include "klee/Expr/Constraints.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" + #include namespace klee { diff --git a/lib/Solver/Z3Builder.cpp b/lib/Solver/Z3Builder.cpp index 06b995ae..07a7b681 100644 --- a/lib/Solver/Z3Builder.cpp +++ b/lib/Solver/Z3Builder.cpp @@ -10,7 +10,7 @@ #ifdef ENABLE_Z3 #include "Z3Builder.h" -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/Solver.h" #include "klee/SolverStats.h" diff --git a/lib/Solver/Z3Builder.h b/lib/Solver/Z3Builder.h index efbf4f9a..4501ecbd 100644 --- a/lib/Solver/Z3Builder.h +++ b/lib/Solver/Z3Builder.h @@ -11,8 +11,9 @@ #define KLEE_Z3BUILDER_H #include "klee/Config/config.h" -#include "klee/util/ArrayExprHash.h" -#include "klee/util/ExprHashMap.h" +#include "klee/Expr/ArrayExprHash.h" +#include "klee/Expr/ExprHashMap.h" + #include #include diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp index 74fee290..cfcb77e7 100644 --- a/lib/Solver/Z3Solver.cpp +++ b/lib/Solver/Z3Solver.cpp @@ -6,19 +6,22 @@ // License. See LICENSE.TXT for details. // //===----------------------------------------------------------------------===// + #include "klee/Config/config.h" #include "klee/Internal/Support/ErrorHandling.h" #include "klee/Internal/Support/FileHandling.h" #include "klee/OptionCategories.h" #ifdef ENABLE_Z3 + #include "Z3Solver.h" #include "Z3Builder.h" -#include "klee/Constraints.h" + +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Assignment.h" +#include "klee/Expr/ExprUtil.h" #include "klee/Solver.h" #include "klee/SolverImpl.h" -#include "klee/util/Assignment.h" -#include "klee/util/ExprUtil.h" #include "llvm/Support/CommandLine.h" #include "llvm/Support/raw_ostream.h" diff --git a/tools/kleaver/main.cpp b/tools/kleaver/main.cpp index 9033a2b4..cc292d10 100644 --- a/tools/kleaver/main.cpp +++ b/tools/kleaver/main.cpp @@ -7,23 +7,22 @@ // //===----------------------------------------------------------------------===// -#include "expr/Lexer.h" -#include "expr/Parser.h" - #include "klee/Common.h" #include "klee/Config/Version.h" -#include "klee/Constraints.h" -#include "klee/Expr.h" -#include "klee/ExprBuilder.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" +#include "klee/Expr/ExprBuilder.h" +#include "klee/Expr/ExprPPrinter.h" +#include "klee/Expr/ExprSMTLIBPrinter.h" +#include "klee/Expr/ExprVisitor.h" +#include "klee/Expr/Parser/Lexer.h" +#include "klee/Expr/Parser/Parser.h" #include "klee/Internal/Support/PrintVersion.h" #include "klee/OptionCategories.h" #include "klee/Solver.h" #include "klee/SolverCmdLine.h" #include "klee/SolverImpl.h" #include "klee/Statistics.h" -#include "klee/util/ExprPPrinter.h" -#include "klee/util/ExprSMTLIBPrinter.h" -#include "klee/util/ExprVisitor.h" #include "llvm/ADT/StringExtras.h" #include "llvm/Support/CommandLine.h" diff --git a/tools/klee/main.cpp b/tools/klee/main.cpp index 99a9bf2a..8235c261 100644 --- a/tools/klee/main.cpp +++ b/tools/klee/main.cpp @@ -11,7 +11,7 @@ #include "klee/Config/Version.h" #include "klee/ExecutionState.h" -#include "klee/Expr.h" +#include "klee/Expr/Expr.h" #include "klee/Internal/ADT/KTest.h" #include "klee/Internal/ADT/TreeStream.h" #include "klee/Internal/Support/Debug.h" diff --git a/unittests/Assignment/AssignmentTest.cpp b/unittests/Assignment/AssignmentTest.cpp index 0eaa28f1..872d3301 100644 --- a/unittests/Assignment/AssignmentTest.cpp +++ b/unittests/Assignment/AssignmentTest.cpp @@ -1,6 +1,8 @@ -#include "klee/util/ArrayCache.h" -#include "klee/util/Assignment.h" #include "gtest/gtest.h" + +#include "klee/Expr/ArrayCache.h" +#include "klee/Expr/Assignment.h" + #include #include diff --git a/unittests/Expr/ExprTest.cpp b/unittests/Expr/ExprTest.cpp index fba15535..3a7541e9 100644 --- a/unittests/Expr/ExprTest.cpp +++ b/unittests/Expr/ExprTest.cpp @@ -10,8 +10,8 @@ #include #include "gtest/gtest.h" -#include "klee/Expr.h" -#include "klee/util/ArrayCache.h" +#include "klee/Expr/ArrayCache.h" +#include "klee/Expr/Expr.h" using namespace klee; diff --git a/unittests/Solver/SolverTest.cpp b/unittests/Solver/SolverTest.cpp index b178ced3..b15fd64b 100644 --- a/unittests/Solver/SolverTest.cpp +++ b/unittests/Solver/SolverTest.cpp @@ -7,16 +7,18 @@ // //===----------------------------------------------------------------------===// -#include #include "gtest/gtest.h" -#include "klee/SolverCmdLine.h" -#include "klee/Constraints.h" -#include "klee/Expr.h" +#include "klee/Expr/ArrayCache.h" +#include "klee/Expr/Constraints.h" +#include "klee/Expr/Expr.h" #include "klee/Solver.h" -#include "klee/util/ArrayCache.h" +#include "klee/SolverCmdLine.h" + #include "llvm/ADT/StringExtras.h" +#include + using namespace klee; namespace { -- cgit 1.4.1