diff options
Diffstat (limited to 'include')
46 files changed, 6215 insertions, 0 deletions
diff --git a/include/expr/Lexer.h b/include/expr/Lexer.h new file mode 100644 index 00000000..4ae760a0 --- /dev/null +++ b/include/expr/Lexer.h @@ -0,0 +1,114 @@ +//===-- 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_EXPR_LEXER_H +#define KLEE_EXPR_LEXER_H + +#include <string> + +namespace llvm { + class MemoryBuffer; +} + +namespace klee { +namespace expr { + struct Token { + enum Kind { + At, /// '@' + Arrow, /// '->' + Colon, /// ':' + Comma, /// ',' + Comment, /// #[^\n]+ + EndOfFile, /// <end of file> + Equals, /// ' = ' + Identifier, /// [a-zA-Z_][a-zA-Z0-9._]* + KWFalse, /// 'false' + KWQuery, /// 'query' + KWReserved, /// fp[0-9]+([.].*)?, i[0-9]+ + KWTrue, /// 'true' + KWWidth, /// w[0-9]+ + LBrace, /// '{' + LParen, /// '(' + LSquare, /// '[' + Number, /// [+-]?[0-9][a-zA-Z0-9_]+ + RBrace, /// '}' + RParen, /// ')' + RSquare, /// ']' + Semicolon, /// ';' + Unknown /// <other> + }; + + 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 >= KWFalse && kind <= KWTrue; + } + + // dump - Dump the token to stderr. + void dump(); + }; + + /// Lexer - Interface for lexing tokens from a .pc 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 diff --git a/include/expr/Parser.h b/include/expr/Parser.h new file mode 100644 index 00000000..7634d66a --- /dev/null +++ b/include/expr/Parser.h @@ -0,0 +1,178 @@ +//===-- 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_EXPR_PARSER_H +#define KLEE_EXPR_PARSER_H + +#include "klee/Expr.h" + +#include <vector> +#include <string> + +namespace llvm { + class MemoryBuffer; +} + +namespace klee { +namespace expr { + // These are the language types we manipulate. + typedef ref<Expr> 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: + Decl(); + virtual ~Decl() {} + + /// dump - Dump the AST node to stderr. + virtual void dump() = 0; + }; + + /// ArrayDecl - Array declarations. + /// + /// For example: + /// array obj : 32 -> 8 = symbolic + /// array obj[32] : 32 -> 8 = { ... } + class ArrayDecl : public Decl { + public: + /// Name - The name of this array. + const Identifier *Name; + + /// Size - The maximum array size (or 0 if unspecified). Concrete + /// arrays always are specified with a size. + const unsigned Size; + + /// Domain - The width of indices. + const unsigned Domain; + + /// Range - The width of array contents. + const unsigned Range; + + /// Contents - The initial contents of the array. The array is + /// symbolic if no contents are specified. The contained + /// expressions are guaranteed to be constants. + const std::vector<ExprHandle> Contents; + + public: + template<typename InputIterator> + ArrayDecl(const Identifier *_Name, unsigned _Size, + unsigned _Domain, unsigned _Range, + InputIterator ContentsBegin=InputIterator(), + InputIterator ContentsEnd=InputIterator()) + : Name(_Name), Size(_Size), Domain(_Domain), Range(_Range), + Contents(ContentsBegin, ContentsEnd) {} + }; + + /// 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; + }; + + /// ExprVarDecl - Expression variable declarations. + class ExprVarDecl : public VarDecl { + public: + ExprHandle Value; + }; + + /// VersionVarDecl - Array version variable declarations. + class VersionVarDecl : public VarDecl { + public: + VersionHandle Value; + }; + + /// CommandDecl - Base class for language commands. + class CommandDecl : public Decl { + public: + const Identifier *Name; + }; + + /// 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<ExprHandle> 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<ExprHandle> Values; + + /// Objects - Symbolic arrays whose initial contents should be + /// given if the query is invalid. + const std::vector<ArrayDecl> Objects; + + public: + template<typename InputIterator> + QueryCommand(InputIterator ConstraintsBegin, + InputIterator ConstraintsEnd, + ExprHandle _Query) + : Constraints(ConstraintsBegin, ConstraintsEnd), + Query(_Query) {} + + virtual void dump(); + }; + + /// Parser - Public interface for parsing a .pc 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. + static Parser *Create(const std::string Name, + const llvm::MemoryBuffer *MB); + }; +} +} + +#endif diff --git a/include/klee/Config/config.h.in b/include/klee/Config/config.h.in new file mode 100644 index 00000000..ef41d786 --- /dev/null +++ b/include/klee/Config/config.h.in @@ -0,0 +1,64 @@ +/* include/klee/Config/config.h.in. Generated from autoconf/configure.tmp.ac by autoheader. */ + +/* Define if stplog enabled */ +#undef ENABLE_STPLOG + +/* Does the platform use __ctype_b_loc, etc. */ +#undef HAVE_CTYPE_EXTERNALS + +/* Define to 1 if you have the <inttypes.h> header file. */ +#undef HAVE_INTTYPES_H + +/* Define to 1 if you have the <memory.h> header file. */ +#undef HAVE_MEMORY_H + +/* Define to 1 if you have the <selinux/selinux.h> header file. */ +#undef HAVE_SELINUX_SELINUX_H + +/* Define to 1 if you have the <stdint.h> header file. */ +#undef HAVE_STDINT_H + +/* Define to 1 if you have the <stdlib.h> header file. */ +#undef HAVE_STDLIB_H + +/* Define to 1 if you have the <strings.h> header file. */ +#undef HAVE_STRINGS_H + +/* Define to 1 if you have the <string.h> header file. */ +#undef HAVE_STRING_H + +/* Define to 1 if you have the <sys/acl.h> header file. */ +#undef HAVE_SYS_ACL_H + +/* Define to 1 if you have the <sys/stat.h> header file. */ +#undef HAVE_SYS_STAT_H + +/* Define to 1 if you have the <sys/types.h> header file. */ +#undef HAVE_SYS_TYPES_H + +/* Define to 1 if you have the <unistd.h> header file. */ +#undef HAVE_UNISTD_H + +/* Path to KLEE's uClibc */ +#undef KLEE_UCLIBC + +/* Define to the address where bug reports for this package should be sent. */ +#undef PACKAGE_BUGREPORT + +/* Define to the full name of this package. */ +#undef PACKAGE_NAME + +/* Define to the full name and version of this package. */ +#undef PACKAGE_STRING + +/* Define to the one symbol short name of this package. */ +#undef PACKAGE_TARNAME + +/* Define to the version of this package. */ +#undef PACKAGE_VERSION + +/* Configuration for runtime libraries */ +#undef RUNTIME_CONFIGURATION + +/* Define to 1 if you have the ANSI C header files. */ +#undef STDC_HEADERS diff --git a/include/klee/Constraints.h b/include/klee/Constraints.h new file mode 100644 index 00000000..87069f89 --- /dev/null +++ b/include/klee/Constraints.h @@ -0,0 +1,79 @@ +//===-- 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: + typedef std::vector< ref<Expr> > constraints_ty; + typedef constraints_ty::iterator iterator; + typedef constraints_ty::const_iterator const_iterator; + + ConstraintManager() {} + + // create from constraints with no optimization + explicit + ConstraintManager(const std::vector< ref<Expr> > &_constraints) : + constraints(_constraints) {} + + ConstraintManager(const ConstraintManager &cs) : constraints(cs.constraints) {} + + typedef std::vector< ref<Expr> >::const_iterator constraint_iterator; + + // given a constraint which is known to be valid, attempt to + // simplify the existing constraint set + void simplifyForValidConstraint(ref<Expr> e); + + ref<Expr> simplifyExpr(ref<Expr> e) const; + + void addConstraint(ref<Expr> e); + + bool empty() const { + return constraints.empty(); + } + ref<Expr> back() const { + return constraints.back(); + } + constraint_iterator begin() const { + return constraints.begin(); + } + constraint_iterator end() const { + return constraints.end(); + } + size_t size() const { + return constraints.size(); + } + + bool operator==(const ConstraintManager &other) const { + return constraints == other.constraints; + } + +private: + std::vector< ref<Expr> > constraints; + + // returns true iff the constraints were modified + bool rewriteConstraints(ExprVisitor &visitor); + + void addConstraintInternal(ref<Expr> e); +}; + +} + +#endif /* KLEE_CONSTRAINTS_H */ diff --git a/include/klee/ExecutionState.h b/include/klee/ExecutionState.h new file mode 100644 index 00000000..09ce2a4b --- /dev/null +++ b/include/klee/ExecutionState.h @@ -0,0 +1,250 @@ +//===-- ExecutionState.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_EXECUTIONSTATE_H +#define KLEE_EXECUTIONSTATE_H + +#include "klee/Constraints.h" +#include "klee/Expr.h" +#include "klee/Internal/ADT/TreeStream.h" + +// FIXME: We do not want to be exposing these? :( +#include "../../lib/Core/AddressSpace.h" +#include "klee/Internal/Module/KInstIterator.h" + +#include <map> +#include <set> +#include <vector> + +namespace klee { + class CallPathNode; + class Cell; + class KFunction; + class KInstruction; + class MemoryObject; + class PTreeNode; + class InstructionInfo; + class ExecutionTraceEvent; + +std::ostream &operator<<(std::ostream &os, const MemoryMap &mm); + +struct StackFrame { + KInstIterator caller; + KFunction *kf; + CallPathNode *callPathNode; + + std::vector<const MemoryObject*> allocas; + Cell *locals; + + /// Minimum distance to an uncovered instruction once the function + /// returns. This is not a good place for this but is used to + /// quickly compute the context sensitive minimum distance to an + /// uncovered instruction. This value is updated by the StatsTracker + /// periodically. + unsigned minDistToUncoveredOnReturn; + + // For vararg functions: arguments not passed via parameter are + // stored (packed tightly) in a local (alloca) memory object. This + // is setup to match the way the front-end generates vaarg code (it + // does not pass vaarg through as expected). VACopy is lowered inside + // of intrinsic lowering. + MemoryObject *varargs; + + StackFrame(KInstIterator caller, KFunction *kf); + StackFrame(const StackFrame &s); + ~StackFrame(); +}; + +// FIXME: Redo execution trace stuff to use a TreeStream, there is no +// need to keep this stuff in memory as far as I can tell. + +// each state should have only one of these guys ... +class ExecutionTraceManager { +public: + ExecutionTraceManager() : hasSeenUserMain(false) {} + + void addEvent(ExecutionTraceEvent* evt); + void printAllEvents(std::ostream &os) const; + +private: + // have we seen a call to __user_main() yet? + // don't bother tracing anything until we see this, + // or else we'll get junky prologue shit + bool hasSeenUserMain; + + // ugh C++ only supports polymorphic calls thru pointers + // + // WARNING: these are NEVER FREED, because they are shared + // across different states (when states fork), so we have + // an *intentional* memory leak, but oh wellz ;) + std::vector<ExecutionTraceEvent*> events; +}; + + +class ExecutionState { +public: + typedef std::vector<StackFrame> stack_ty; + +private: + // unsupported, use copy constructor + ExecutionState &operator=(const ExecutionState&); + std::map< std::string, std::string > fnAliases; + +public: + bool fakeState; + // Are we currently underconstrained? Hack: value is size to make fake + // objects. + unsigned underConstrained; + unsigned depth; + + // pc - pointer to current instruction stream + KInstIterator pc, prevPC; + stack_ty stack; + ConstraintManager constraints; + mutable double queryCost; + double weight; + AddressSpace addressSpace; + TreeOStream pathOS, symPathOS; + unsigned instsSinceCovNew; + bool coveredNew; + + // for printing execution traces when this state terminates + ExecutionTraceManager exeTraceMgr; + + /// Disables forking, set by user code. + bool forkDisabled; + + std::map<const std::string*, std::set<unsigned> > coveredLines; + PTreeNode *ptreeNode; + + /// ordered list of symbolics: used to generate test cases. + // + // FIXME: Move to a shared list structure (not critical). + std::vector<const MemoryObject*> symbolics; + + // Used by the checkpoint/rollback methods for fake objects. + // FIXME: not freeing things on branch deletion. + MemoryMap shadowObjects; + + unsigned incomingBBIndex; + + std::string getFnAlias(std::string fn); + void addFnAlias(std::string old_fn, std::string new_fn); + void removeFnAlias(std::string fn); + +private: + ExecutionState() : fakeState(false), underConstrained(0), ptreeNode(0) {}; + +public: + ExecutionState(KFunction *kf); + + // XXX total hack, just used to make a state so solver can + // use on structure + ExecutionState(const std::vector<ref<Expr> > &assumptions); + + ~ExecutionState(); + + ExecutionState *branch(); + + void pushFrame(KInstIterator caller, KFunction *kf); + void popFrame(); + + void addSymbolic(const MemoryObject *mo) { + symbolics.push_back(mo); + } + void addConstraint(ref<Expr> e) { + constraints.addConstraint(e); + } + + // Used for checkpoint/rollback of fake objects created during tainting. + ObjectState *cloneObject(ObjectState *os, MemoryObject *mo); + + // + + bool merge(const ExecutionState &b); +}; + + +// for producing abbreviated execution traces to help visualize +// paths and diagnose bugs + +class ExecutionTraceEvent { +public: + // the location of the instruction: + std::string file; + unsigned line; + std::string funcName; + unsigned stackDepth; + + unsigned consecutiveCount; // init to 1, increase for CONSECUTIVE + // repetitions of the SAME event + + ExecutionTraceEvent() + : file("global"), line(0), funcName("global_def"), + consecutiveCount(1) {} + + ExecutionTraceEvent(ExecutionState& state, KInstruction* ki); + + virtual ~ExecutionTraceEvent() {} + + void print(std::ostream &os) const; + + // return true if it shouldn't be added to ExecutionTraceManager + // + virtual bool ignoreMe() const; + +private: + virtual void printDetails(std::ostream &os) const = 0; +}; + + +class FunctionCallTraceEvent : public ExecutionTraceEvent { +public: + std::string calleeFuncName; + + FunctionCallTraceEvent(ExecutionState& state, KInstruction* ki, + const std::string& _calleeFuncName) + : ExecutionTraceEvent(state, ki), calleeFuncName(_calleeFuncName) {} + +private: + virtual void printDetails(std::ostream &os) const { + os << "CALL " << calleeFuncName; + } + +}; + +class FunctionReturnTraceEvent : public ExecutionTraceEvent { +public: + FunctionReturnTraceEvent(ExecutionState& state, KInstruction* ki) + : ExecutionTraceEvent(state, ki) {} + +private: + virtual void printDetails(std::ostream &os) const { + os << "RETURN"; + } +}; + +class BranchTraceEvent : public ExecutionTraceEvent { +public: + bool trueTaken; // which side taken? + bool canForkGoBothWays; + + BranchTraceEvent(ExecutionState& state, KInstruction* ki, + bool _trueTaken, bool _isTwoWay) + : ExecutionTraceEvent(state, ki), + trueTaken(_trueTaken), + canForkGoBothWays(_isTwoWay) {} + +private: + virtual void printDetails(std::ostream &os) const; +}; + +} + +#endif diff --git a/include/klee/Expr.h b/include/klee/Expr.h new file mode 100644 index 00000000..d16a09bf --- /dev/null +++ b/include/klee/Expr.h @@ -0,0 +1,808 @@ +//===-- 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 "Machine.h" +#include "klee/util/Bits.h" + +#include "llvm/Support/Streams.h" +#include "llvm/ADT/SmallVector.h" + +#include <set> +#include <vector> + +namespace llvm { + class Type; +} + +namespace klee { + +class Array; +class ConstantExpr; +class ObjectState; +class MemoryObject; + +template<class T> class ref; + + +/// Class representing symbolic expressions. +/** + +<b>Expression canonicalization</b>: 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: +<ol> +<li> No Expr has all constant arguments.</li> + +<li> Booleans: + <ol type="a"> + <li> Boolean not is written as <tt>(false == ?)</tt> </li> + <li> \c Ne, \c Ugt, \c Uge, \c Sgt, \c Sge are not used </li> + <li> The only acceptable operations with boolean arguments are \c And, + \c Or, \c Xor, \c Eq, as well as \c SExt, \c ZExt, + \c Select and \c NotOptimized. </li> + <li> The only boolean operation which may involve a constant is boolean not (<tt>== false</tt>). </li> + </ol> +</li> + +<li> Linear Formulas: + <ol type="a"> + <li> 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 <tt>add(-c, ?)</tt>. </li> + </ol> +</li> + + +<li> Chains are unbalanced to the right </li> + +</ol> + + +<b>Steps required for adding an expr</b>: + -# 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; + + + 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, + + // 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 + }; + + unsigned refCount; + +protected: + unsigned hashValue; + +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<Expr> getKid(unsigned i) const = 0; + + virtual void print(std::ostream &os) 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(); + + static unsigned hashConstant(uint64_t val, Width w) { + return val ^ (w * MAGIC_HASH_CONSTANT); + } + + /// Returns 0 iff b is structuraly equivalent to *this + int compare(const Expr &b) const; + virtual int compareContents(const Expr &b) const { return 0; } + + // Given an array of new kids return a copy of the expression + // but using those children. + virtual ref<Expr> rebuild(ref<Expr> kids[/* getNumKids() */]) const = 0; + + /// + + uint64_t getConstantValue() const; + + /* Static utility methods */ + + static void printKind(std::ostream &os, Kind k); + static void printWidth(std::ostream &os, Expr::Width w); + static Width getWidthForLLVMType(const llvm::Type *type); + + /// 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<Expr> createCoerceToPointerType(ref<Expr> e); + static ref<Expr> createNot(ref<Expr> e); + static ref<Expr> createImplies(ref<Expr> hyp, ref<Expr> conc); + static ref<Expr> createIsZero(ref<Expr> e); + + /// Create a little endian read of the given type at offset 0 of the + /// given object. + static ref<Expr> createTempRead(const Array *array, Expr::Width w); + + static ref<Expr> createPointer(uint64_t v); + + // do not use + static Expr *createConstant(uint64_t val, Width w); + + struct CreateArg; + static ref<Expr> createFromKind(Kind k, std::vector<CreateArg> args); + + static bool isValidKidWidth(unsigned kid, Width w) { return true; } + static bool needsResultType() { return false; } +}; +// END class Expr + + + +#include "klee/util/Ref.h" + +struct Expr::CreateArg { + ref<Expr> expr; + Width width; + + CreateArg(Width w = Bool) : expr(0, Expr::Bool), width(w) {} + CreateArg(ref<Expr> 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 std::ostream &operator<<(std::ostream &os, const Expr &e) { + e.print(os); + return os; +} + +inline std::ostream &operator<<(std::ostream &os, const Expr::Kind kind) { + Expr::printKind(os, kind); + return os; +} + +// Terminal Exprs + +class ConstantExpr : public Expr { +public: + static const Kind kind = Constant; + static const unsigned numKids = 0; + +public: + union { + uint64_t asUInt64; + }; + Width width; + +public: + ~ConstantExpr() {}; + // should change the code to make this private + ConstantExpr(uint64_t v, Width w) : asUInt64(v), width(w) {} + + Width getWidth() const { return width; } + Kind getKind() const { return Constant; } + + unsigned getNumKids() const { return 0; } + ref<Expr> getKid(unsigned i) const { return 0; } + + int compareContents(const Expr &b) const { + const ConstantExpr &cb = static_cast<const ConstantExpr&>(b); + if (width != cb.width) return width < cb.width ? -1 : 1; + if (asUInt64 < cb.asUInt64) { + return -1; + } else if (asUInt64 > cb.asUInt64) { + return 1; + } else { + return 0; + } + } + + virtual ref<Expr> rebuild(ref<Expr> kids[]) const { + assert(0 && "rebuild() on ConstantExpr"); + } + + virtual unsigned computeHash(); + + static ref<ConstantExpr> fromMemory(void *address, Width w); + void toMemory(void *address); + + static ref<ConstantExpr> alloc(uint64_t v, Width w) { + // constructs an "optimized" ConstantExpr + return ref<ConstantExpr>(v, w); + } + + static ref<ConstantExpr> create(uint64_t v, Width w) { + assert(v == bits64::truncateToNBits(v, w) && + "invalid constant"); + return alloc(v, w); + } +}; + + +// Utility classes + +class BinaryExpr : public Expr { +public: + ref<Expr> left, right; + +public: + unsigned getNumKids() const { return 2; } + ref<Expr> getKid(unsigned i) const { + if(i == 0) + return left; + if(i == 1) + return right; + return 0; + } + +protected: + BinaryExpr(const ref<Expr> &l, const ref<Expr> &r) : left(l), right(r) {} +}; + + +class CmpExpr : public BinaryExpr { + +protected: + CmpExpr(ref<Expr> l, ref<Expr> r) : BinaryExpr(l,r) {} + +public: + Width getWidth() const { return Bool; } +}; + +// Special + +class NotOptimizedExpr : public Expr { +public: + static const Kind kind = NotOptimized; + static const unsigned numKids = 1; + ref<Expr> src; + + static ref<Expr> alloc(const ref<Expr> &src) { + ref<Expr> r(new NotOptimizedExpr(src)); + r.computeHash(); + return r; + } + + static ref<Expr> create(ref<Expr> src); + + Width getWidth() const { return src.getWidth(); } + Kind getKind() const { return NotOptimized; } + + unsigned getNumKids() const { return 1; } + ref<Expr> getKid(unsigned i) const { return src; } + + virtual ref<Expr> rebuild(ref<Expr> kids[]) const { return create(kids[0]); } + +private: + NotOptimizedExpr(const ref<Expr> &_src) : src(_src) {} +}; + + +/// Class representing a byte update of an array. +class UpdateNode { + friend class UpdateList; + friend class STPBuilder; // for setting STPArray + + mutable unsigned refCount; + // gross + mutable void *stpArray; + // cache instead of recalc + unsigned hashValue; + +public: + const UpdateNode *next; + ref<Expr> index, value; + +private: + /// size of this update sequence, including this update + unsigned size; + +public: + UpdateNode(const UpdateNode *_next, + const ref<Expr> &_index, + const ref<Expr> &_value); + + unsigned getSize() const { return size; } + + int compare(const UpdateNode &b) const; + unsigned hash() const { return hashValue; } + +private: + UpdateNode() : refCount(0), stpArray(0) {} + ~UpdateNode(); + + unsigned computeHash(); +}; + +class Array { +public: + const MemoryObject *object; + unsigned id; + unsigned size; + + // FIXME: This does not belong here. + mutable void *stpInitialArray; + +public: + // NOTE: id's ***MUST*** be unique to ensure sanity w.r.t. STP, + // which hashes different arrays with the same id to the same + // object! We should probably use the pointer for talking to STP, as + // long as we can guarantee that it won't be a "stale" reference + // once we have freed it. + Array(const MemoryObject *_object, unsigned _id, uint64_t _size) + : object(_object), id(_id), size(_size), stpInitialArray(0) {} + ~Array() { + // FIXME: This relies on caller to delete the STP array. + assert(!stpInitialArray && "Array must be deleted by caller!"); + } +}; + +/// Class representing a complete list of updates into an array. +/** The main trick is the isRooted bit, which enables important optimizations. + ... + */ +class UpdateList { + friend class ReadExpr; // for default constructor + +public: + const Array *root; + + /// pointer to the most recent update node + const UpdateNode *head; + + // shouldn't this be part of the ReadExpr? + bool isRooted; + +public: + UpdateList(const Array *_root, bool isRooted, 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<Expr> &index, const ref<Expr> &value); + + int compare(const UpdateList &b) const; + unsigned hash() const; +}; + +/// Class representing a one byte read from an array. +class ReadExpr : public Expr { +public: + static const Kind kind = Read; + static const unsigned numKids = 1; + +public: + UpdateList updates; + ref<Expr> index; + +public: + static ref<Expr> alloc(const UpdateList &updates, const ref<Expr> &index) { + ref<Expr> r(new ReadExpr(updates, index)); + r.computeHash(); + return r; + } + + static ref<Expr> create(const UpdateList &updates, ref<Expr> i); + + Width getWidth() const { return Expr::Int8; } + Kind getKind() const { return Read; } + + unsigned getNumKids() const { return numKids; } + ref<Expr> getKid(unsigned i) const { return !i ? index : 0; } + + int compareContents(const Expr &b) const; + + virtual ref<Expr> rebuild(ref<Expr> kids[]) const { + return create(updates, kids[0]); + } + + virtual unsigned computeHash(); + +private: + ReadExpr(const UpdateList &_updates, const ref<Expr> &_index) : + updates(_updates), index(_index) {} +}; + + +/// Class representing an if-then-else expression. +class SelectExpr : public Expr { +public: + static const Kind kind = Select; + static const unsigned numKids = 3; + +public: + ref<Expr> cond, trueExpr, falseExpr; + +public: + static ref<Expr> alloc(const ref<Expr> &c, const ref<Expr> &t, const ref<Expr> &f) { + ref<Expr> r(new SelectExpr(c, t, f)); + r.computeHash(); + return r; + } + + static ref<Expr> create(ref<Expr> c, ref<Expr> t, ref<Expr> f); + + Width getWidth() const { return trueExpr.getWidth(); } + Kind getKind() const { return Select; } + + unsigned getNumKids() const { return numKids; } + ref<Expr> 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<Expr> rebuild(ref<Expr> kids[]) const { + return create(kids[0], kids[1], kids[2]); + } + +private: + SelectExpr(const ref<Expr> &c, const ref<Expr> &t, const ref<Expr> &f) + : cond(c), trueExpr(t), falseExpr(f) {} +}; + + +/** Children of a concat expression can have arbitrary widths. + Kid 0 is the left kid, kid 1 is the right kid. +*/ +class ConcatExpr : public Expr { +public: + static const Kind kind = Concat; + static const unsigned numKids = 2; + +private: + Width width; + ref<Expr> left, right; + +public: + static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) { + ref<Expr> c(new ConcatExpr(l, r)); + c.computeHash(); + return c; + } + + static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r); + + Width getWidth() const { return width; } + Kind getKind() const { return kind; } + ref<Expr> getLeft() const { return left; } + ref<Expr> getRight() const { return right; } + + unsigned getNumKids() const { return numKids; } + ref<Expr> 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<Expr> createN(unsigned nKids, const ref<Expr> kids[]); + static ref<Expr> create4(const ref<Expr> &kid1, const ref<Expr> &kid2, + const ref<Expr> &kid3, const ref<Expr> &kid4); + static ref<Expr> create8(const ref<Expr> &kid1, const ref<Expr> &kid2, + const ref<Expr> &kid3, const ref<Expr> &kid4, + const ref<Expr> &kid5, const ref<Expr> &kid6, + const ref<Expr> &kid7, const ref<Expr> &kid8); + + virtual ref<Expr> rebuild(ref<Expr> kids[]) const { return create(kids[0], kids[1]); } + + + /* These will be eliminated */ + bool is2ByteConcat() const { return false; } + bool is4ByteConcat() const { return false; } + bool is8ByteConcat() const { return false; } + +private: + ConcatExpr(const ref<Expr> &l, const ref<Expr> &r) : left(l), right(r) { + width = l.getWidth() + r.getWidth(); + } +}; + + +/** 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 Expr { +public: + static const Kind kind = Extract; + static const unsigned numKids = 1; + +public: + ref<Expr> expr; + unsigned offset; + Width width; + +public: + static ref<Expr> alloc(const ref<Expr> &e, unsigned o, Width w) { + ref<Expr> r(new ExtractExpr(e, o, w)); + r.computeHash(); + return r; + } + + /// Creates an ExtractExpr with the given bit offset and width + static ref<Expr> create(ref<Expr> e, unsigned bitOff, Width w); + + /// Creates an ExtractExpr with the given byte offset and width + static ref<Expr> createByteOff(ref<Expr> e, unsigned byteOff, Width w=Expr::Int8); + + Width getWidth() const { return width; } + Kind getKind() const { return Extract; } + + unsigned getNumKids() const { return numKids; } + ref<Expr> getKid(unsigned i) const { return expr; } + + int compareContents(const Expr &b) const { + const ExtractExpr &eb = static_cast<const ExtractExpr&>(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<Expr> rebuild(ref<Expr> kids[]) const { + return create(kids[0], offset, width); + } + + virtual unsigned computeHash(); + +private: + ExtractExpr(const ref<Expr> &e, unsigned b, Width w) + : expr(e),offset(b),width(w) {} +}; + + +// Casting + +class CastExpr : public Expr { +public: + ref<Expr> src; + Width width; + +public: + CastExpr(const ref<Expr> &e, Width w) : src(e), width(w) {} + + Width getWidth() const { return width; } + + unsigned getNumKids() const { return 1; } + ref<Expr> 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<const CastExpr&>(b); + if (width != eb.width) return width < eb.width ? -1 : 1; + return 0; + } + + virtual unsigned computeHash(); +}; + +#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<Expr> e, Width w) : CastExpr(e,w) {} \ + static ref<Expr> alloc(const ref<Expr> &e, Width w) { \ + ref<Expr> r(new _class_kind ## Expr(e, w)); \ + r.computeHash(); \ + return r; \ + } \ + static ref<Expr> create(const ref<Expr> &e, Width w); \ + Kind getKind() const { return _class_kind; } \ + virtual ref<Expr> rebuild(ref<Expr> kids[]) const { \ + return create(kids[0], width); \ + } \ +}; \ + +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<Expr> &l, const ref<Expr> &r) : BinaryExpr(l,r) {} \ + static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) { \ + ref<Expr> res(new _class_kind ## Expr (l, r)); \ + res.computeHash(); \ + return res; \ + } \ + static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r); \ + Width getWidth() const { return left.getWidth(); } \ + Kind getKind() const { return _class_kind; } \ + virtual ref<Expr> rebuild(ref<Expr> kids[]) const { \ + return create(kids[0], kids[1]); \ + } \ +}; \ + +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<Expr> &l, const ref<Expr> &r) : CmpExpr(l,r) {} \ + static ref<Expr> alloc(const ref<Expr> &l, const ref<Expr> &r) { \ + ref<Expr> res(new _class_kind ## Expr (l, r)); \ + res.computeHash(); \ + return res; \ + } \ + static ref<Expr> create(const ref<Expr> &l, const ref<Expr> &r); \ + Kind getKind() const { return _class_kind; } \ + virtual ref<Expr> rebuild(ref<Expr> kids[]) const { \ + return create(kids[0], kids[1]); \ + } \ +}; \ + +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) + +} // End klee namespace + +#endif diff --git a/include/klee/IncompleteSolver.h b/include/klee/IncompleteSolver.h new file mode 100644 index 00000000..f72607b5 --- /dev/null +++ b/include/klee/IncompleteSolver.h @@ -0,0 +1,108 @@ +//===-- IncompleteSolver.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_INCOMPLETESOLVER_H +#define KLEE_INCOMPLETESOLVER_H + +#include "klee/Solver.h" +#include "klee/SolverImpl.h" + +namespace klee { + +/// IncompleteSolver - Base class for incomplete solver +/// implementations. +/// +/// Incomplete solvers are useful for implementing optimizations which +/// may quickly compute an answer, but cannot always compute the +/// correct answer. They can be used with the StagedSolver to provide +/// a complete Solver implementation. +class IncompleteSolver { +public: + /// PartialValidity - Represent a possibility incomplete query + /// validity. + enum PartialValidity { + /// The query is provably true. + MustBeTrue = 1, + + /// The query is provably false. + MustBeFalse = -1, + + /// The query is not provably false (a true assignment is known to + /// exist). + MayBeTrue = 2, + + /// The query is not provably true (a false assignment is known to + /// exist). + MayBeFalse = -2, + + /// The query is known to have both true and false assignments. + TrueOrFalse = 0, + + /// The validity of the query is unknown. + None = 3 + }; + + static PartialValidity negatePartialValidity(PartialValidity pv); + +public: + IncompleteSolver() {}; + virtual ~IncompleteSolver() {}; + + /// computeValidity - Compute a partial validity for the given query. + /// + /// The passed expression is non-constant with bool type. + /// + /// The IncompleteSolver class provides an implementation of + /// computeValidity using computeTruth. Sub-classes may override + /// this if a more efficient implementation is available. + virtual IncompleteSolver::PartialValidity computeValidity(const Query&); + + /// computeValidity - Compute a partial validity for the given query. + /// + /// The passed expression is non-constant with bool type. + virtual IncompleteSolver::PartialValidity computeTruth(const Query&) = 0; + + /// computeValue - Attempt to compute a value for the given expression. + virtual bool computeValue(const Query&, ref<Expr> &result) = 0; + + /// computeInitialValues - Attempt to compute the constant values + /// for the initial state of each given object. If a correct result + /// is not found, then the values array must be unmodified. + virtual bool computeInitialValues(const Query&, + const std::vector<const Array*> + &objects, + std::vector< std::vector<unsigned char> > + &values, + bool &hasSolution) = 0; +}; + +/// StagedSolver - Adapter class for staging an incomplete solver with +/// a complete secondary solver, to form an (optimized) complete +/// solver. +class StagedSolverImpl : public SolverImpl { +private: + IncompleteSolver *primary; + Solver *secondary; + +public: + StagedSolverImpl(IncompleteSolver *_primary, Solver *_secondary); + ~StagedSolverImpl(); + + bool computeTruth(const Query&, bool &isValid); + bool computeValidity(const Query&, Solver::Validity &result); + bool computeValue(const Query&, ref<Expr> &result); + bool computeInitialValues(const Query&, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool &hasSolution); +}; + +} + +#endif diff --git a/include/klee/Internal/ADT/BOut.h b/include/klee/Internal/ADT/BOut.h new file mode 100644 index 00000000..14aeb714 --- /dev/null +++ b/include/klee/Internal/ADT/BOut.h @@ -0,0 +1,62 @@ +//===-- BOut.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 __COMMON_BOUT_H__ +#define __COMMON_BOUT_H__ + + +#ifdef __cplusplus +extern "C" { +#endif + + typedef struct BOutObject BOutObject; + struct BOutObject { + char *name; + unsigned numBytes; + unsigned char *bytes; + }; + + typedef struct BOut BOut; + struct BOut { + /* file format version */ + unsigned version; + + unsigned numArgs; + char **args; + + unsigned symArgvs; + unsigned symArgvLen; + + unsigned numObjects; + BOutObject *objects; + }; + + + /* returns the current .bout file format version */ + unsigned bOut_getCurrentVersion(); + + /* return true iff file at path matches BOut header */ + int bOut_isBOutFile(const char *path); + + /* returns NULL on (unspecified) error */ + BOut* bOut_fromFile(const char *path); + + /* returns 1 on success, 0 on (unspecified) error */ + int bOut_toFile(BOut *, const char *path); + + /* returns total number of object bytes */ + unsigned bOut_numBytes(BOut *); + + void bOut_free(BOut *); + +#ifdef __cplusplus +} +#endif + +#endif diff --git a/include/klee/Internal/ADT/DiscretePDF.h b/include/klee/Internal/ADT/DiscretePDF.h new file mode 100644 index 00000000..bda851fa --- /dev/null +++ b/include/klee/Internal/ADT/DiscretePDF.h @@ -0,0 +1,47 @@ +//===-- DiscretePDF.h -------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +namespace klee { + template <class T> + class DiscretePDF { + // not perfectly parameterized, but float/double/int should work ok, + // although it would be better to have choose argument range from 0 + // to queryable max. + typedef double weight_type; + + public: + DiscretePDF(); + ~DiscretePDF(); + + bool empty() const; + void insert(T item, weight_type weight); + void update(T item, weight_type newWeight); + void remove(T item); + bool inTree(T item); + weight_type getWeight(T item); + + /* pick a tree element according to its + * weight. p should be in [0,1). + */ + T choose(double p); + + private: + class Node; + Node *m_root; + + Node **lookup(T item, Node **parent_out); + void split(Node *node); + void rotate(Node *node); + void lengthen(Node *node); + void propogateSumsUp(Node *n); + }; + +} + +#include "DiscretePDF.inc" diff --git a/include/klee/Internal/ADT/DiscretePDF.inc b/include/klee/Internal/ADT/DiscretePDF.inc new file mode 100644 index 00000000..1eb23629 --- /dev/null +++ b/include/klee/Internal/ADT/DiscretePDF.inc @@ -0,0 +1,342 @@ +//===- DiscretePDF.inc - --*- C++ -*-===// + +// + +namespace klee { + +template <class T> +class DiscretePDF<T>::Node +{ +private: + bool m_mark; + +public: + Node *parent, *left, *right; + T key; + weight_type weight, sumWeights; + +public: + Node(T key_, weight_type weight_, Node *parent_); + ~Node(); + + Node *sibling() { return this==parent->left?parent->right:parent->left; } + + void markRed() { m_mark = true; } + void markBlack() { m_mark = false; } + bool isBlack() { return !m_mark; } + bool leftIsBlack() { return !left || left->isBlack(); } + bool rightIsBlack() { return !right || right->isBlack(); } + void setSum() { + sumWeights = weight; + if (left) sumWeights += left->sumWeights; + if (right) sumWeights += right->sumWeights; + } +}; + + /// + +template <class T> +DiscretePDF<T>::Node::Node(T key_, weight_type weight_, Node *parent_) { + m_mark = false; + + key = key_; + weight = weight_; + sumWeights = 0; + left = right = 0; + parent = parent_; +} + +template <class T> +DiscretePDF<T>::Node::~Node() { + if (left) delete left; + if (right) delete right; +} + +// + +template <class T> +DiscretePDF<T>::DiscretePDF() { + m_root = 0; +} + +template <class T> +DiscretePDF<T>::~DiscretePDF() { + if (m_root) delete m_root; +} + +template <class T> +bool DiscretePDF<T>::empty() const { + return m_root == 0; +} + +template <class T> +void DiscretePDF<T>::insert(T item, weight_type weight) { + Node *p=0, *n=m_root; + + while (n) { + if (!n->leftIsBlack() && !n->rightIsBlack()) + split(n); + + p = n; + if (n->key==item) { + assert(0 && "insert: argument(item) already in tree"); + } else { + n = (item<n->key)?n->left:n->right; + } + } + + n = new Node(item, weight, p); + + if (!p) { + m_root = n; + } else { + if (item<p->key) { + p->left = n; + } else { + p->right = n; + } + + split(n); + } + + propogateSumsUp(n); +} + +template <class T> +void DiscretePDF<T>::remove(T item) { + Node **np = lookup(item, 0); + Node *child, *n = *np; + + if (!n) { + assert(0 && "remove: argument(item) not in tree"); + } else { + if (n->left) { + Node **leftMaxp = &n->left; + + while ((*leftMaxp)->right) + leftMaxp = &(*leftMaxp)->right; + + n->key = (*leftMaxp)->key; + n->weight = (*leftMaxp)->weight; + + np = leftMaxp; + n = *np; + } + + // node now has at most one child + + child = n->left?n->left:n->right; + *np = child; + + if (child) { + child->parent = n->parent; + + if (n->isBlack()) { + lengthen(child); + } + } + + propogateSumsUp(n->parent); + + n->left = n->right = 0; + delete n; + } +} + +template <class T> +void DiscretePDF<T>::update(T item, weight_type weight) { + Node *n = *lookup(item, 0); + + if (!n) { + assert(0 && "update: argument(item) not in tree"); + } else { + n->weight = weight; + propogateSumsUp(n); + } +} + +template <class T> +T DiscretePDF<T>::choose(double p) { + if (p<0.0 || p>=1.0) { + assert(0 && "choose: argument(p) outside valid range"); + } else if (!m_root) { + assert(0 && "choose: choose() called on empty tree"); + } else { + weight_type w = (weight_type) (m_root->sumWeights * p); + Node *n = m_root; + + while (1) { + if (n->left) { + if (w<n->left->sumWeights) { + n = n->left; + continue; + } else { + w -= n->left->sumWeights; + } + } + if (w<n->weight || !n->right) { + break; // !n->right condition shouldn't be necessary, just sanity check + } + w -= n->weight; + n = n->right; + } + + return n->key; + } +} + +template <class T> +bool DiscretePDF<T>::inTree(T item) { + Node *n = *lookup(item, 0); + + return !!n; +} + +template <class T> +typename DiscretePDF<T>::weight_type DiscretePDF<T>::getWeight(T item) { + Node *n = *lookup(item, 0); + assert(n); + return n->weight; +} + +// + +template <class T> +typename DiscretePDF<T>::Node ** +DiscretePDF<T>::lookup(T item, Node **parent_out) { + Node *n, *p=0, **np=&m_root; + + while ((n = *np)) { + if (n->key==item) { + break; + } else { + p = n; + if (item<n->key) { + np = &n->left; + } else { + np = &n->right; + } + } + } + + if (parent_out) + *parent_out = p; + return np; +} + +template <class T> +void DiscretePDF<T>::split(Node *n) { + if (n->left) n->left->markBlack(); + if (n->right) n->right->markBlack(); + + if (n->parent) { + Node *p = n->parent; + + n->markRed(); + + if (!p->isBlack()) { + p->parent->markRed(); + + // not same direction + if (!((n==p->left && p==p->parent->left) || + (n==p->right && p==p->parent->right))) { + rotate(n); + p = n; + } + + rotate(p); + p->markBlack(); + } + } +} + +template <class T> +void DiscretePDF<T>::rotate(Node *n) { + Node *p=n->parent, *pp=p->parent; + + n->parent = pp; + p->parent = n; + + if (n==p->left) { + p->left = n->right; + n->right = p; + if (p->left) p->left->parent = p; + } else { + p->right = n->left; + n->left = p; + if (p->right) p->right->parent = p; + } + + n->setSum(); + p->setSum(); + + if (!pp) { + m_root = n; + } else { + if (p==pp->left) { + pp->left = n; + } else { + pp->right = n; + } + } +} + +template <class T> +void DiscretePDF<T>::lengthen(Node *n) { + if (!n->isBlack()) { + n->markBlack(); + } else if (n->parent) { + Node *sibling = n->sibling(); + + if (sibling && !sibling->isBlack()) { + n->parent->markRed(); + sibling->markBlack(); + + rotate(sibling); // node sibling is now old sibling child, must be black + sibling = n->sibling(); + } + + // sibling is black + + if (!sibling) { + lengthen(n->parent); + } else if (sibling->leftIsBlack() && sibling->rightIsBlack()) { + if (n->parent->isBlack()) { + sibling->markRed(); + lengthen(n->parent); + } else { + sibling->markRed(); + n->parent->markBlack(); + } + } else { + if (n==n->parent->left && sibling->rightIsBlack()) { + rotate(sibling->left); // sibling->left must be red + sibling->markRed(); + sibling->parent->markBlack(); + sibling = sibling->parent; + } else if (n==n->parent->right && sibling->leftIsBlack()) { + rotate(sibling->right); // sibling->right must be red + sibling->markRed(); + sibling->parent->markBlack(); + sibling = sibling->parent; + } + + // sibling is black, and sibling's far child is red + + rotate(sibling); + if (!n->parent->isBlack()) + sibling->markRed(); + sibling->left->markBlack(); + sibling->right->markBlack(); + } + } +} + +template <class T> +void DiscretePDF<T>::propogateSumsUp(Node *n) { + for (; n; n=n->parent) + n->setSum(); +} + +} + diff --git a/include/klee/Internal/ADT/ImmutableMap.h b/include/klee/Internal/ADT/ImmutableMap.h new file mode 100644 index 00000000..c7af3786 --- /dev/null +++ b/include/klee/Internal/ADT/ImmutableMap.h @@ -0,0 +1,104 @@ +//===-- ImmutableMap.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 __UTIL_IMMUTABLEMAP_H__ +#define __UTIL_IMMUTABLEMAP_H__ + +#include <functional> + +#include "ImmutableTree.h" + +namespace klee { + template<class V, class D> + struct _Select1st { + D &operator()(V &a) const { return a.first; } + const D &operator()(const V &a) const { return a.first; } + }; + + template<class K, class D, class CMP=std::less<K> > + class ImmutableMap { + public: + typedef K key_type; + typedef std::pair<K,D> value_type; + + typedef ImmutableTree<K, value_type, _Select1st<value_type,key_type>, CMP> Tree; + typedef typename Tree::iterator iterator; + + private: + Tree elts; + + ImmutableMap(const Tree &b): elts(b) {} + + public: + ImmutableMap() {} + ImmutableMap(const ImmutableMap &b) : elts(b.elts) {} + ~ImmutableMap() {} + + ImmutableMap &operator=(const ImmutableMap &b) { elts = b.elts; return *this; } + + bool empty() const { + return elts.empty(); + } + unsigned count(const key_type &key) const { + return elts.count(key); + } + const value_type *lookup(const key_type &key) const { + return elts.lookup(key); + } + const value_type *lookup_previous(const key_type &key) const { + return elts.lookup_previous(key); + } + const value_type &min() const { + return elts.min(); + } + const value_type &max() const { + return elts.max(); + } + unsigned size() const { + return elts.size(); + } + + ImmutableMap insert(const value_type &value) const { + return elts.insert(value); + } + ImmutableMap replace(const value_type &value) const { + return elts.replace(value); + } + ImmutableMap remove(const key_type &key) const { + return elts.remove(key); + } + ImmutableMap popMin(const value_type &valueOut) const { + return elts.popMin(valueOut); + } + ImmutableMap popMax(const value_type &valueOut) const { + return elts.popMax(valueOut); + } + + iterator begin() const { + return elts.begin(); + } + iterator end() const { + return elts.end(); + } + iterator find(const key_type &key) const { + return elts.find(key); + } + iterator lower_bound(const key_type &key) const { + return elts.lower_bound(key); + } + iterator upper_bound(const key_type &key) const { + return elts.upper_bound(key); + } + + static unsigned getAllocated() { return Tree::allocated; } + }; + +} + +#endif diff --git a/include/klee/Internal/ADT/ImmutableSet.h b/include/klee/Internal/ADT/ImmutableSet.h new file mode 100644 index 00000000..0c79eb9c --- /dev/null +++ b/include/klee/Internal/ADT/ImmutableSet.h @@ -0,0 +1,101 @@ +//===-- ImmutableSet.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 __UTIL_IMMUTABLESET_H__ +#define __UTIL_IMMUTABLESET_H__ + +#include <functional> + +#include "ImmutableTree.h" + +namespace klee { + template<class T> + struct _Identity { + T &operator()(T &a) const { return a; } + const T &operator()(const T &a) const { return a; } + }; + + template<class T, class CMP=std::less<T> > + class ImmutableSet { + public: + typedef T key_type; + typedef T value_type; + + typedef ImmutableTree<T, T, _Identity<T>, CMP> Tree; + typedef typename Tree::iterator iterator; + + private: + Tree elts; + + ImmutableSet(const Tree &b): elts(b) {} + + public: + ImmutableSet() {} + ImmutableSet(const ImmutableSet &b) : elts(b.elts) {} + ~ImmutableSet() {} + + ImmutableSet &operator=(const ImmutableSet &b) { elts = b.elts; return *this; } + + bool empty() const { + return elts.empty(); + } + unsigned count(const key_type &key) const { + return elts.count(key); + } + const value_type *lookup(const key_type &key) const { + return elts.lookup(key); + } + const value_type &min() const { + return elts.min(); + } + const value_type &max() const { + return elts.max(); + } + unsigned size() { + return elts.size(); + } + + ImmutableSet insert(const value_type &value) const { + return elts.insert(value); + } + ImmutableSet replace(const value_type &value) const { + return elts.replace(value); + } + ImmutableSet remove(const key_type &key) const { + return elts.remove(key); + } + ImmutableSet popMin(const value_type &valueOut) const { + return elts.popMin(valueOut); + } + ImmutableSet popMax(const value_type &valueOut) const { + return elts.popMax(valueOut); + } + + iterator begin() const { + return elts.begin(); + } + iterator end() const { + return elts.end(); + } + iterator find(const key_type &key) const { + return elts.find(key); + } + iterator lower_bound(const key_type &key) const { + return elts.lower_bound(key); + } + iterator upper_bound(const key_type &key) const { + return elts.upper_bound(key); + } + + static unsigned getAllocated() { return Tree::allocated; } + }; + +} + +#endif diff --git a/include/klee/Internal/ADT/ImmutableTree.h b/include/klee/Internal/ADT/ImmutableTree.h new file mode 100644 index 00000000..2f294077 --- /dev/null +++ b/include/klee/Internal/ADT/ImmutableTree.h @@ -0,0 +1,619 @@ +//===-- ImmutableTree.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 __UTIL_IMMUTABLETREE_H__ +#define __UTIL_IMMUTABLETREE_H__ + +#include <cassert> +#include <vector> + +namespace klee { + template<class K, class V, class KOV, class CMP> + class ImmutableTree { + public: + static unsigned allocated; + class iterator; + + typedef K key_type; + typedef V value_type; + typedef KOV key_of_value; + typedef CMP key_compare; + + public: + ImmutableTree(); + ImmutableTree(const ImmutableTree &s); + ~ImmutableTree(); + + ImmutableTree &operator=(const ImmutableTree &s); + + bool empty() const; + + unsigned count(const key_type &key) const; // always 0 or 1 + const value_type *lookup(const key_type &key) const; + + // find the last value less than or equal to key, or null if + // no such value exists + const value_type *lookup_previous(const key_type &key) const; + + const value_type &min() const; + const value_type &max() const; + unsigned size() const; + + ImmutableTree insert(const value_type &value) const; + ImmutableTree replace(const value_type &value) const; + ImmutableTree remove(const key_type &key) const; + ImmutableTree popMin(value_type &valueOut) const; + ImmutableTree popMax(value_type &valueOut) const; + + iterator begin() const; + iterator end() const; + iterator find(const key_type &key) const; + iterator lower_bound(const key_type &key) const; + iterator upper_bound(const key_type &key) const; + + static unsigned getAllocated() { return allocated; } + + private: + class Node; + + Node *node; + ImmutableTree(Node *_node); + }; + + /***/ + + template<class K, class V, class KOV, class CMP> + class ImmutableTree<K,V,KOV,CMP>::Node { + public: + static Node terminator; + Node *left, *right; + value_type value; + unsigned height, references; + + protected: + Node(); // solely for creating the terminator node + static Node *balance(Node *left, const value_type &value, Node *right); + + public: + + Node(Node *_left, Node *_right, const value_type &_value); + ~Node(); + + void decref(); + Node *incref(); + + bool isTerminator(); + + unsigned size(); + Node *popMin(value_type &valueOut); + Node *popMax(value_type &valueOut); + Node *insert(const value_type &v); + Node *replace(const value_type &v); + Node *remove(const key_type &k); + }; + + // Should live somewhere else, this is a simple stack with maximum size. + template<typename T> + class FixedStack { + unsigned pos, max; + T *elts; + + public: + FixedStack(unsigned _max) : pos(0), + max(_max), + elts(new T[max]) {} + FixedStack(const FixedStack &b) : pos(b.pos), + max(b.max), + elts(new T[b.max]) { + std::copy(b.elts, b.elts+pos, elts); + } + ~FixedStack() { delete[] elts; } + + void push_back(const T &elt) { elts[pos++] = elt; } + void pop_back() { --pos; } + bool empty() { return pos==0; } + T &back() { return elts[pos-1]; } + + + FixedStack &operator=(const FixedStack &b) { + assert(max == b.max); + pos = b.pos; + std::copy(b.elts, b.elts+pos, elts); + return *this; + } + + bool operator==(const FixedStack &b) { + return (pos == b.pos && + std::equal(elts, elts+pos, b.elts)); + } + bool operator!=(const FixedStack &b) { return !(*this==b); } + }; + + template<class K, class V, class KOV, class CMP> + class ImmutableTree<K,V,KOV,CMP>::iterator { + friend class ImmutableTree<K,V,KOV,CMP>; + private: + Node *root; // so can back up from end + FixedStack<Node*> stack; + + public: + iterator(Node *_root, bool atBeginning) : root(_root->incref()), + stack(root->height) { + if (atBeginning) { + for (Node *n=root; !n->isTerminator(); n=n->left) + stack.push_back(n); + } + } + iterator(const iterator &i) : root(i.root->incref()), + stack(i.stack) { + } + ~iterator() { + root->decref(); + } + + iterator &operator=(const iterator &b) { + b.root->incref(); + root->decref(); + root = b.root; + stack = b.stack; + return *this; + } + + const value_type &operator*() { + Node *n = stack.back(); + return n->value; + } + + const value_type *operator->() { + Node *n = stack.back(); + return &n->value; + } + + bool operator==(const iterator &b) { + return stack==b.stack; + } + bool operator!=(const iterator &b) { + return stack!=b.stack; + } + + iterator &operator--() { + if (stack.empty()) { + for (Node *n=root; !n->isTerminator(); n=n->right) + stack.push_back(n); + } else { + Node *n = stack.back(); + if (n->left->isTerminator()) { + for (;;) { + Node *prev = n; + stack.pop_back(); + if (stack.empty()) { + break; + } else { + n = stack.back(); + if (prev==n->right) + break; + } + } + } else { + stack.push_back(n->left); + for (n=n->left->right; !n->isTerminator(); n=n->right) + stack.push_back(n); + } + } + return *this; + } + + iterator &operator++() { + assert(!stack.empty()); + Node *n = stack.back(); + if (n->right->isTerminator()) { + for (;;) { + Node *prev = n; + stack.pop_back(); + if (stack.empty()) { + break; + } else { + n = stack.back(); + if (prev==n->left) + break; + } + } + } else { + stack.push_back(n->right); + for (n=n->right->left; !n->isTerminator(); n=n->left) + stack.push_back(n); + } + return *this; + } + }; + + /***/ + + template<class K, class V, class KOV, class CMP> + typename ImmutableTree<K,V,KOV,CMP>::Node + ImmutableTree<K,V,KOV,CMP>::Node::terminator; + + template<class K, class V, class KOV, class CMP> + unsigned ImmutableTree<K,V,KOV,CMP>::allocated = 0; + + template<class K, class V, class KOV, class CMP> + ImmutableTree<K,V,KOV,CMP>::Node::Node() + : left(&terminator), + right(&terminator), + height(0), + references(3) { + assert(this==&terminator); + } + + template<class K, class V, class KOV, class CMP> + ImmutableTree<K,V,KOV,CMP>::Node::Node(Node *_left, Node *_right, const value_type &_value) + : left(_left), + right(_right), + value(_value), + height(std::max(left->height, right->height) + 1), + references(1) + { + ++allocated; + } + + template<class K, class V, class KOV, class CMP> + ImmutableTree<K,V,KOV,CMP>::Node::~Node() { + left->decref(); + right->decref(); + --allocated; + } + + template<class K, class V, class KOV, class CMP> + inline void ImmutableTree<K,V,KOV,CMP>::Node::decref() { + --references; + if (references==0) delete this; + } + + template<class K, class V, class KOV, class CMP> + inline typename ImmutableTree<K,V,KOV,CMP>::Node *ImmutableTree<K,V,KOV,CMP>::Node::incref() { + ++references; + return this; + } + + template<class K, class V, class KOV, class CMP> + inline bool ImmutableTree<K,V,KOV,CMP>::Node::isTerminator() { + return this==&terminator; + } + + /***/ + + template<class K, class V, class KOV, class CMP> + typename ImmutableTree<K,V,KOV,CMP>::Node * + ImmutableTree<K,V,KOV,CMP>::Node::balance(Node *left, const value_type &value, Node *right) { + if (left->height > right->height + 2) { + Node *ll = left->left; + Node *lr = left->right; + if (ll->height >= lr->height) { + Node *nlr = new Node(lr->incref(), right, value); + Node *res = new Node(ll->incref(), nlr, left->value); + left->decref(); + return res; + } else { + Node *lrl = lr->left; + Node *lrr = lr->right; + Node *nll = new Node(ll->incref(), lrl->incref(), left->value); + Node *nlr = new Node(lrr->incref(), right, value); + Node *res = new Node(nll, nlr, lr->value); + left->decref(); + return res; + } + } else if (right->height > left->height + 2) { + Node *rl = right->left; + Node *rr = right->right; + if (rr->height >= rl->height) { + Node *nrl = new Node(left, rl->incref(), value); + Node *res = new Node(nrl, rr->incref(), right->value); + right->decref(); + return res; + } else { + Node *rll = rl->left; + Node *rlr = rl->right; + Node *nrl = new Node(left, rll->incref(), value); + Node *nrr = new Node(rlr->incref(), rr->incref(), right->value); + Node *res = new Node(nrl, nrr, rl->value); + right->decref(); + return res; + } + } else { + return new Node(left, right, value); + } + } + + template<class K, class V, class KOV, class CMP> + unsigned ImmutableTree<K,V,KOV,CMP>::Node::size() { + if (isTerminator()) { + return 0; + } else { + return left->size() + 1 + right->size(); + } + } + + template<class K, class V, class KOV, class CMP> + typename ImmutableTree<K,V,KOV,CMP>::Node * + ImmutableTree<K,V,KOV,CMP>::Node::popMin(value_type &valueOut) { + if (left->isTerminator()) { + valueOut = value; + return right->incref(); + } else { + return balance(left->popMin(valueOut), value, right->incref()); + } + } + + template<class K, class V, class KOV, class CMP> + typename ImmutableTree<K,V,KOV,CMP>::Node * + ImmutableTree<K,V,KOV,CMP>::Node::popMax(value_type &valueOut) { + if (right->isTerminator()) { + valueOut = value; + return left->incref(); + } else { + return balance(left->incref(), value, right->popMax(valueOut)); + } + } + + template<class K, class V, class KOV, class CMP> + typename ImmutableTree<K,V,KOV,CMP>::Node * + ImmutableTree<K,V,KOV,CMP>::Node::insert(const value_type &v) { + if (isTerminator()) { + return new Node(terminator.incref(), terminator.incref(), v); + } else { + if (key_compare()(key_of_value()(v), key_of_value()(value))) { + return balance(left->insert(v), value, right->incref()); + } else if (key_compare()(key_of_value()(value), key_of_value()(v))) { + return balance(left->incref(), value, right->insert(v)); + } else { + return incref(); + } + } + } + + template<class K, class V, class KOV, class CMP> + typename ImmutableTree<K,V,KOV,CMP>::Node * + ImmutableTree<K,V,KOV,CMP>::Node::replace(const value_type &v) { + if (isTerminator()) { + return new Node(terminator.incref(), terminator.incref(), v); + } else { + if (key_compare()(key_of_value()(v), key_of_value()(value))) { + return balance(left->replace(v), value, right->incref()); + } else if (key_compare()(key_of_value()(value), key_of_value()(v))) { + return balance(left->incref(), value, right->replace(v)); + } else { + return new Node(left->incref(), right->incref(), v); + } + } + } + + template<class K, class V, class KOV, class CMP> + typename ImmutableTree<K,V,KOV,CMP>::Node * + ImmutableTree<K,V,KOV,CMP>::Node::remove(const key_type &k) { + if (isTerminator()) { + return incref(); + } else { + if (key_compare()(k, key_of_value()(value))) { + return balance(left->remove(k), value, right->incref()); + } else if (key_compare()(key_of_value()(value), k)) { + return balance(left->incref(), value, right->remove(k)); + } else { + if (left->isTerminator()) { + return right->incref(); + } else if (right->isTerminator()) { + return left->incref(); + } else { + value_type min; + Node *nr = right->popMin(min); + return balance(left->incref(), min, nr); + } + } + } + } + + /***/ + + template<class K, class V, class KOV, class CMP> + ImmutableTree<K,V,KOV,CMP>::ImmutableTree() + : node(Node::terminator.incref()) { + } + + template<class K, class V, class KOV, class CMP> + ImmutableTree<K,V,KOV,CMP>::ImmutableTree(Node *_node) + : node(_node) { + } + + template<class K, class V, class KOV, class CMP> + ImmutableTree<K,V,KOV,CMP>::ImmutableTree(const ImmutableTree &s) + : node(s.node->incref()) { + } + + template<class K, class V, class KOV, class CMP> + ImmutableTree<K,V,KOV,CMP>::~ImmutableTree() { + node->decref(); + } + + template<class K, class V, class KOV, class CMP> + ImmutableTree<K,V,KOV,CMP> &ImmutableTree<K,V,KOV,CMP>::operator=(const ImmutableTree &s) { + Node *n = s.node->incref(); + node->decref(); + node = n; + return *this; + } + + template<class K, class V, class KOV, class CMP> + bool ImmutableTree<K,V,KOV,CMP>::empty() const { + return node->isTerminator(); + } + + template<class K, class V, class KOV, class CMP> + unsigned ImmutableTree<K,V,KOV,CMP>::count(const key_type &k) const { + Node *n = node; + while (!n->isTerminator()) { + key_type key = key_of_value()(n->value); + if (key_compare()(k, key)) { + n = n->left; + } else if (key_compare()(key, k)) { + n = n->right; + } else { + return 1; + } + } + return 0; + } + + template<class K, class V, class KOV, class CMP> + const typename ImmutableTree<K,V,KOV,CMP>::value_type * + ImmutableTree<K,V,KOV,CMP>::lookup(const key_type &k) const { + Node *n = node; + while (!n->isTerminator()) { + key_type key = key_of_value()(n->value); + if (key_compare()(k, key)) { + n = n->left; + } else if (key_compare()(key, k)) { + n = n->right; + } else { + return &n->value; + } + } + return 0; + } + + template<class K, class V, class KOV, class CMP> + const typename ImmutableTree<K,V,KOV,CMP>::value_type * + ImmutableTree<K,V,KOV,CMP>::lookup_previous(const key_type &k) const { + Node *n = node; + Node *result = 0; + while (!n->isTerminator()) { + key_type key = key_of_value()(n->value); + if (key_compare()(k, key)) { + n = n->left; + } else if (key_compare()(key, k)) { + result = n; + n = n->right; + } else { + return &n->value; + } + } + return result ? &result->value : 0; + } + + template<class K, class V, class KOV, class CMP> + const typename ImmutableTree<K,V,KOV,CMP>::value_type & + ImmutableTree<K,V,KOV,CMP>::min() const { + Node *n = node; + assert(!n->isTerminator()); + while (!n->left->isTerminator()) n = n->left; + return n->value; + } + + template<class K, class V, class KOV, class CMP> + const typename ImmutableTree<K,V,KOV,CMP>::value_type & + ImmutableTree<K,V,KOV,CMP>::max() const { + Node *n = node; + assert(!n->isTerminator()); + while (!n->right->isTerminator()) n = n->right; + return n->value; + } + + template<class K, class V, class KOV, class CMP> + unsigned ImmutableTree<K,V,KOV,CMP>::size() const { + return node->size(); + } + + template<class K, class V, class KOV, class CMP> + ImmutableTree<K,V,KOV,CMP> + ImmutableTree<K,V,KOV,CMP>::insert(const value_type &value) const { + return ImmutableTree(node->insert(value)); + } + + template<class K, class V, class KOV, class CMP> + ImmutableTree<K,V,KOV,CMP> + ImmutableTree<K,V,KOV,CMP>::replace(const value_type &value) const { + return ImmutableTree(node->replace(value)); + } + + template<class K, class V, class KOV, class CMP> + ImmutableTree<K,V,KOV,CMP> + ImmutableTree<K,V,KOV,CMP>::remove(const key_type &key) const { + return ImmutableTree(node->remove(key)); + } + + template<class K, class V, class KOV, class CMP> + ImmutableTree<K,V,KOV,CMP> + ImmutableTree<K,V,KOV,CMP>::popMin(value_type &valueOut) const { + return ImmutableTree(node->popMin(valueOut)); + } + + template<class K, class V, class KOV, class CMP> + ImmutableTree<K,V,KOV,CMP> + ImmutableTree<K,V,KOV,CMP>::popMax(value_type &valueOut) const { + return ImmutableTree(node->popMax(valueOut)); + } + + template<class K, class V, class KOV, class CMP> + inline typename ImmutableTree<K,V,KOV,CMP>::iterator + ImmutableTree<K,V,KOV,CMP>::begin() const { + return iterator(node, true); + } + + template<class K, class V, class KOV, class CMP> + inline typename ImmutableTree<K,V,KOV,CMP>::iterator + ImmutableTree<K,V,KOV,CMP>::end() const { + return iterator(node, false); + } + + template<class K, class V, class KOV, class CMP> + inline typename ImmutableTree<K,V,KOV,CMP>::iterator + ImmutableTree<K,V,KOV,CMP>::find(const key_type &key) const { + iterator end(node,false), it = lower_bound(key); + if (it==end || key_compare()(key,key_of_value()(*it))) { + return end; + } else { + return it; + } + } + + template<class K, class V, class KOV, class CMP> + inline typename ImmutableTree<K,V,KOV,CMP>::iterator + ImmutableTree<K,V,KOV,CMP>::lower_bound(const key_type &k) const { + // XXX ugh this doesn't have to be so ugly does it? + iterator it(node,false); + for (Node *root=node; !root->isTerminator();) { + it.stack.push_back(root); + if (key_compare()(k, key_of_value()(root->value))) { + root = root->left; + } else if (key_compare()(key_of_value()(root->value), k)) { + root = root->right; + } else { + return it; + } + } + // it is now beginning or first element < k + if (!it.stack.empty()) { + Node *last = it.stack.back(); + if (key_compare()(key_of_value()(last->value), k)) + ++it; + } + return it; + } + + template<class K, class V, class KOV, class CMP> + typename ImmutableTree<K,V,KOV,CMP>::iterator + ImmutableTree<K,V,KOV,CMP>::upper_bound(const key_type &key) const { + iterator end(node,false),it = lower_bound(key); + if (it!=end && + !key_compare()(key,key_of_value()(*it))) // no need to loop, no duplicates + ++it; + return it; + } + +} + +#endif diff --git a/include/klee/Internal/ADT/MapOfSets.h b/include/klee/Internal/ADT/MapOfSets.h new file mode 100644 index 00000000..25c5e2b9 --- /dev/null +++ b/include/klee/Internal/ADT/MapOfSets.h @@ -0,0 +1,385 @@ +//===-- MapOfSets.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 __UTIL_MAPOFSETS_H__ +#define __UTIL_MAPOFSETS_H__ + +#include <cassert> +#include <vector> +#include <set> +#include <map> + +// This should really be broken down into TreeOfSets on top of which +// SetOfSets and MapOfSets are easily implemeted. It should also be +// parameterized on the underlying set type. Neither are hard to do, +// just not worth it at the moment. +// +// I also broke some STLish conventions because I was bored. + +namespace klee { + + /** This implements the UBTree data structure (see Hoffmann and + Koehler, "A New Method to Index and Query Sets", IJCAI 1999) */ + template<class K, class V> + class MapOfSets { + public: + class iterator; + + public: + MapOfSets(); + + void clear(); + + void insert(const std::set<K> &set, const V &value); + + V *lookup(const std::set<K> &set); + + iterator begin(); + iterator end(); + + void subsets(const std::set<K> &set, + std::vector< std::pair<std::set<K>, V> > &resultOut); + void supersets(const std::set<K> &set, + std::vector< std::pair<std::set<K>, V> > &resultOut); + + template<class Predicate> + V *findSuperset(const std::set<K> &set, const Predicate &p); + template<class Predicate> + V *findSubset(const std::set<K> &set, const Predicate &p); + + private: + class Node; + + Node root; + + template<class Iterator, class Vector> + void findSubsets(Node *n, + const std::set<K> &accum, + Iterator begin, + Iterator end, + Vector &resultsOut); + template<class Iterator, class Vector> + void findSupersets(Node *n, + const std::set<K> &accum, + Iterator begin, + Iterator end, + Vector &resultsOut); + template<class Predicate> + V *findSuperset(Node *n, + typename std::set<K>::iterator begin, + typename std::set<K>::iterator end, + const Predicate &p); + template<class Predicate> + V *findSubset(Node *n, + typename std::set<K>::iterator begin, + typename std::set<K>::iterator end, + const Predicate &p); + }; + + /***/ + + template<class K, class V> + class MapOfSets<K,V>::Node { + friend class MapOfSets<K,V>; + friend class MapOfSets<K,V>::iterator; + + public: + typedef std::map<K, Node> children_ty; + + V value; + + private: + bool isEndOfSet; + std::map<K, Node> children; + + public: + Node() : isEndOfSet(false) {} + }; + + template<class K, class V> + class MapOfSets<K,V>::iterator { + typedef std::vector< typename std::map<K, Node>::iterator > stack_ty; + friend class MapOfSets<K,V>; + private: + Node *root; + bool onEntry; + stack_ty stack; + + void step() { + if (onEntry) { + onEntry = false; + Node *n = stack.empty() ? root : &stack.back()->second; + while (!n->children.empty()) { + stack.push_back(n->children.begin()); + n = &stack.back()->second; + if (n->isEndOfSet) { + onEntry = true; + return; + } + } + } + + while (!stack.empty()) { + unsigned size = stack.size(); + Node *at = size==1 ? root : &stack[size-2]->second; + typename std::map<K,Node>::iterator &cur = stack.back(); + ++cur; + if (cur==at->children.end()) { + stack.pop_back(); + } else { + Node *n = &cur->second; + + while (!n->isEndOfSet) { + assert(!n->children.empty()); + stack.push_back(n->children.begin()); + n = &stack.back()->second; + } + + onEntry = true; + break; + } + } + } + + public: + // end() + iterator() : onEntry(false) {} + // begin() + iterator(Node *_n) : root(_n), onEntry(true) { + if (!root->isEndOfSet) + step(); + } + + const std::pair<const std::set<K>, const V> operator*() { + assert(onEntry || !stack.empty()); + std::set<K> s; + for (typename stack_ty::iterator it = stack.begin(), ie = stack.end(); + it != ie; ++it) + s.insert((*it)->first); + Node *n = stack.empty() ? root : &stack.back()->second; + return std::make_pair(s, n->value); + } + + bool operator==(const iterator &b) { + return onEntry==b.onEntry && stack==b.stack; + } + bool operator!=(const iterator &b) { + return !(*this==b); + } + + iterator &operator++() { + step(); + return *this; + } + }; + + /***/ + + template<class K, class V> + MapOfSets<K,V>::MapOfSets() {} + + template<class K, class V> + void MapOfSets<K,V>::insert(const std::set<K> &set, const V &value) { + Node *n = &root; + for (typename std::set<K>::const_iterator it = set.begin(), ie = set.end(); + it != ie; ++it) + n = &n->children.insert(std::make_pair(*it, Node())).first->second; + n->isEndOfSet = true; + n->value = value; + } + + template<class K, class V> + V *MapOfSets<K,V>::lookup(const std::set<K> &set) { + Node *n = &root; + for (typename std::set<K>::const_iterator it = set.begin(), ie = set.end(); + it != ie; ++it) { + typename Node::children_ty::iterator kit = n->children.find(*it); + if (kit==n->children.end()) { + return 0; + } else { + n = &kit->second; + } + } + if (n->isEndOfSet) { + return &n->value; + } else { + return 0; + } + } + + template<class K, class V> + typename MapOfSets<K,V>::iterator + MapOfSets<K,V>::begin() { return iterator(&root); } + + template<class K, class V> + typename MapOfSets<K,V>::iterator + MapOfSets<K,V>::end() { return iterator(); } + + template<class K, class V> + template<class Iterator, class Vector> + void MapOfSets<K,V>::findSubsets(Node *n, + const std::set<K> &accum, + Iterator begin, + Iterator end, + Vector &resultsOut) { + if (n->isEndOfSet) { + resultsOut.push_back(std::make_pair(accum, n->value)); + } + + for (Iterator it=begin; it!=end;) { + K elt = *it; + typename Node::children_ty::iterator kit = n->children.find(elt); + it++; + if (kit!=n->children.end()) { + std::set<K> nacc = accum; + nacc.insert(elt); + findSubsets(&kit->second, nacc, it, end, resultsOut); + } + } + } + + template<class K, class V> + void MapOfSets<K,V>::subsets(const std::set<K> &set, + std::vector< std::pair<std::set<K>, + V> > &resultOut) { + findSubsets(&root, std::set<K>(), set.begin(), set.end(), resultOut); + } + + template<class K, class V> + template<class Iterator, class Vector> + void MapOfSets<K,V>::findSupersets(Node *n, + const std::set<K> &accum, + Iterator begin, + Iterator end, + Vector &resultsOut) { + if (begin==end) { + if (n->isEndOfSet) + resultsOut.push_back(std::make_pair(accum, n->value)); + for (typename Node::children_ty::iterator it = n->children.begin(), + ie = n->children.end(); it != ie; ++it) { + std::set<K> nacc = accum; + nacc.insert(it->first); + findSupersets(&it->second, nacc, begin, end, resultsOut); + } + } else { + K elt = *begin; + Iterator next = begin; + ++next; + for (typename Node::children_ty::iterator it = n->children.begin(), + ie = n->children.end(); it != ie; ++it) { + std::set<K> nacc = accum; + nacc.insert(it->first); + if (elt==it->first) { + findSupersets(&it->second, nacc, next, end, resultsOut); + } else if (it->first<elt) { + findSupersets(&it->second, nacc, begin, end, resultsOut); + } else { + break; + } + } + } + } + + template<class K, class V> + void MapOfSets<K,V>::supersets(const std::set<K> &set, + std::vector< std::pair<std::set<K>, V> > &resultOut) { + findSupersets(&root, std::set<K>(), set.begin(), set.end(), resultOut); + } + + template<class K, class V> + template<class Predicate> + V *MapOfSets<K,V>::findSubset(Node *n, + typename std::set<K>::iterator begin, + typename std::set<K>::iterator end, + const Predicate &p) { + if (n->isEndOfSet && p(n->value)) { + return &n->value; + } else if (begin==end) { + return 0; + } else { + typename Node::children_ty::iterator kend = n->children.end(); + typename Node::children_ty::iterator + kbegin = n->children.lower_bound(*begin); + typename std::set<K>::iterator it = begin; + if (kbegin==kend) + return 0; + for (;;) { // kbegin!=kend && *it <= kbegin->first + while (*it < kbegin->first) { + ++it; + if (it==end) + return 0; + } + if (*it == kbegin->first) { + ++it; + V *res = findSubset(&kbegin->second, it, end, p); + if (res || it==end) + return res; + } + while (kbegin->first < *it) { + ++kbegin; + if (kbegin==kend) + return 0; + } + } + } + } + + template<class K, class V> + template<class Predicate> + V *MapOfSets<K,V>::findSuperset(Node *n, + typename std::set<K>::iterator begin, + typename std::set<K>::iterator end, + const Predicate &p) { + if (begin==end) { + if (n->isEndOfSet && p(n->value)) + return &n->value; + for (typename Node::children_ty::iterator it = n->children.begin(), + ie = n->children.end(); it != ie; ++it) { + V *res = findSuperset(&it->second, begin, end, p); + if (res) return res; + } + } else { + typename Node::children_ty::iterator kbegin = n->children.begin(); + typename Node::children_ty::iterator kmid = + n->children.lower_bound(*begin); + for (typename Node::children_ty::iterator it = n->children.begin(), + ie = n->children.end(); it != ie; ++it) { + V *res = findSuperset(&it->second, begin, end, p); + if (res) return res; + } + if (kmid!=n->children.end() && *begin==kmid->first) { + V *res = findSuperset(&kmid->second, ++begin, end, p); + if (res) return res; + } + } + return 0; + } + + template<class K, class V> + template<class Predicate> + V *MapOfSets<K,V>::findSuperset(const std::set<K> &set, const Predicate &p) { + return findSuperset(&root, set.begin(), set.end(), p); + } + + template<class K, class V> + template<class Predicate> + V *MapOfSets<K,V>::findSubset(const std::set<K> &set, const Predicate &p) { + return findSubset(&root, set.begin(), set.end(), p); + } + + template<class K, class V> + void MapOfSets<K,V>::clear() { + root.isEndOfSet = false; + root.value = V(); + root.children.clear(); + } + +} + +#endif diff --git a/include/klee/Internal/ADT/RNG.h b/include/klee/Internal/ADT/RNG.h new file mode 100644 index 00000000..b7f4906b --- /dev/null +++ b/include/klee/Internal/ADT/RNG.h @@ -0,0 +1,50 @@ +//===-- RNG.h ---------------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_UTIL_RNG_H +#define KLEE_UTIL_RNG_H + +namespace klee { + class RNG { + private: + /* Period parameters */ + static const int N = 624; + static const int M = 397; + static const unsigned int MATRIX_A = 0x9908b0dfUL; /* constant vector a */ + static const unsigned int UPPER_MASK = 0x80000000UL; /* most significant w-r bits */ + static const unsigned int LOWER_MASK = 0x7fffffffUL; /* least significant r bits */ + + private: + unsigned int mt[N]; /* the array for the state vector */ + int mti; + + public: + RNG(unsigned int seed=5489UL); + + void seed(unsigned int seed); + + /* generates a random number on [0,0xffffffff]-interval */ + unsigned int getInt32(); + /* generates a random number on [0,0x7fffffff]-interval */ + int getInt31(); + /* generates a random number on [0,1]-real-interval */ + double getDoubleLR(); + float getFloatLR(); + /* generates a random number on [0,1)-real-interval */ + double getDoubleL(); + float getFloatL(); + /* generates a random number on (0,1)-real-interval */ + double getDouble(); + float getFloat(); + /* generators a random flop */ + bool getBool(); + }; +} + +#endif diff --git a/include/klee/Internal/ADT/TreeStream.h b/include/klee/Internal/ADT/TreeStream.h new file mode 100644 index 00000000..63e49dbb --- /dev/null +++ b/include/klee/Internal/ADT/TreeStream.h @@ -0,0 +1,77 @@ +//===-- TreeStream.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 __UTIL_TREESTREAM_H__ +#define __UTIL_TREESTREAM_H__ + +#include <string> +#include <iostream> +#include <vector> + +namespace klee { + + typedef unsigned TreeStreamID; + class TreeOStream; + + class TreeStreamWriter { + static const unsigned bufferSize = 4*4096; + + friend class TreeOStream; + + private: + char buffer[bufferSize]; + unsigned lastID, bufferCount; + + std::string path; + std::ofstream *output; + unsigned ids; + + void write(TreeOStream &os, const char *s, unsigned size); + void flushBuffer(); + + public: + TreeStreamWriter(const std::string &_path); + ~TreeStreamWriter(); + + bool good(); + + TreeOStream open(); + TreeOStream open(const TreeOStream &node); + + void flush(); + + // hack, to be replace by proper stream capabilities + void readStream(TreeStreamID id, + std::vector<unsigned char> &out); + }; + + class TreeOStream { + friend class TreeStreamWriter; + + private: + TreeStreamWriter *writer; + unsigned id; + + TreeOStream(TreeStreamWriter &_writer, unsigned _id); + + public: + TreeOStream(); + ~TreeOStream(); + + unsigned getID() const; + + void write(const char *buffer, unsigned size); + + TreeOStream &operator<<(const std::string &s); + + void flush(); + }; +} + +#endif diff --git a/include/klee/Internal/Module/Cell.h b/include/klee/Internal/Module/Cell.h new file mode 100644 index 00000000..f54cd6eb --- /dev/null +++ b/include/klee/Internal/Module/Cell.h @@ -0,0 +1,23 @@ +//===-- Cell.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_CELL_H +#define KLEE_CELL_H + +#include <klee/Expr.h> + +namespace klee { + class MemoryObject; + + struct Cell { + ref<Expr> value; + }; +} + +#endif diff --git a/include/klee/Internal/Module/InstructionInfoTable.h b/include/klee/Internal/Module/InstructionInfoTable.h new file mode 100644 index 00000000..c93f5ddb --- /dev/null +++ b/include/klee/Internal/Module/InstructionInfoTable.h @@ -0,0 +1,70 @@ +//===-- InstructionInfoTable.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_LIB_INSTRUCTIONINFOTABLE_H +#define KLEE_LIB_INSTRUCTIONINFOTABLE_H + +#include <map> +#include <string> +#include <set> + +namespace llvm { + class Function; + class Instruction; + class Module; +} + +namespace klee { + + /* Stores debug information for a KInstruction */ + struct InstructionInfo { + unsigned id; + const std::string &file; + unsigned line; + unsigned assemblyLine; + + public: + InstructionInfo(unsigned _id, + const std::string &_file, + unsigned _line, + unsigned _assemblyLine) + : id(_id), + file(_file), + line(_line), + assemblyLine(_assemblyLine) { + } + }; + + class InstructionInfoTable { + struct ltstr { + bool operator()(const std::string *a, const std::string *b) const { + return *a<*b; + } + }; + + std::string dummyString; + InstructionInfo dummyInfo; + std::map<const llvm::Instruction*, InstructionInfo> infos; + std::set<const std::string *, ltstr> internedStrings; + + private: + const std::string *internString(std::string s); + + public: + InstructionInfoTable(llvm::Module *m); + ~InstructionInfoTable(); + + unsigned getMaxID() const; + const InstructionInfo &getInfo(const llvm::Instruction*) const; + const InstructionInfo &getFunctionInfo(const llvm::Function*) const; + }; + +} + +#endif diff --git a/include/klee/Internal/Module/KInstIterator.h b/include/klee/Internal/Module/KInstIterator.h new file mode 100644 index 00000000..3890cc65 --- /dev/null +++ b/include/klee/Internal/Module/KInstIterator.h @@ -0,0 +1,49 @@ +//===-- KInstIterator.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_KINSTITERATOR_H +#define KLEE_KINSTITERATOR_H + +namespace klee { + class KInstruction; + + class KInstIterator { + KInstruction **it; + + public: + KInstIterator() : it(0) {} + KInstIterator(KInstruction **_it) : it(_it) {} + KInstIterator(const KInstIterator &b) : it(b.it) {} + ~KInstIterator() {} + + KInstIterator &operator=(const KInstIterator &b) { + it = b.it; + return *this; + } + + bool operator==(const KInstIterator &b) const { + return it==b.it; + } + bool operator!=(const KInstIterator &b) const { + return !(*this == b); + } + + KInstIterator &operator++() { + ++it; + return *this; + } + + operator KInstruction*() const { return it ? *it : 0;} + operator bool() const { return it != 0; } + + KInstruction *operator ->() const { return *it; } + }; +} // End klee namespace + +#endif diff --git a/include/klee/Internal/Module/KInstruction.h b/include/klee/Internal/Module/KInstruction.h new file mode 100644 index 00000000..c91d37ab --- /dev/null +++ b/include/klee/Internal/Module/KInstruction.h @@ -0,0 +1,50 @@ +//===-- KInstruction.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_KINSTRUCTION_H +#define KLEE_KINSTRUCTION_H + +#include <vector> + +namespace llvm { + class Instruction; +} + +namespace klee { + class Executor; + struct InstructionInfo; + class KModule; + + + /// KInstruction - Intermediate instruction representation used + /// during execution. + struct KInstruction { + llvm::Instruction *inst; + const InstructionInfo *info; + + /// Value numbers for each operand. -1 is an invalid value, + /// otherwise negative numbers are indices (negated and offset by + /// 2) into the module constant table and positive numbers are + /// register indices. + int *operands; + /// Destination register index. + unsigned dest; + + public: + virtual ~KInstruction(); + }; + + struct KGEPInstruction : KInstruction { + std::vector< std::pair<unsigned, unsigned> > indices; + unsigned offset; + }; +} + +#endif + diff --git a/include/klee/Internal/Module/KModule.h b/include/klee/Internal/Module/KModule.h new file mode 100644 index 00000000..690f079d --- /dev/null +++ b/include/klee/Internal/Module/KModule.h @@ -0,0 +1,119 @@ +//===-- KModule.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_KMODULE_H +#define KLEE_KMODULE_H + +#include "klee/Interpreter.h" + +#include <map> +#include <set> +#include <vector> + +namespace llvm { + class BasicBlock; + class Constant; + class Function; + class Instruction; + class Module; + class TargetData; +} + +namespace klee { + class Cell; + class Executor; + class Expr; + class InterpreterHandler; + class InstructionInfoTable; + class KInstruction; + class KModule; + template<class T> class ref; + + struct KFunction { + llvm::Function *function; + + unsigned numArgs, numRegisters; + + unsigned numInstructions; + KInstruction **instructions; + + std::map<llvm::BasicBlock*, unsigned> basicBlockEntry; + + /// Whether instructions in this function should count as + /// "coverable" for statistics and search heuristics. + bool trackCoverage; + + private: + KFunction(const KFunction&); + KFunction &operator=(const KFunction&); + + public: + explicit KFunction(llvm::Function*, KModule *); + ~KFunction(); + + unsigned getArgRegister(unsigned index) { return index; } + }; + + + class KConstant { + public: + /// Actual LLVM constant this represents. + llvm::Constant* ct; + + /// The constant ID. + unsigned id; + + /// First instruction where this constant was encountered, or NULL + /// if not applicable/unavailable. + KInstruction *ki; + + KConstant(llvm::Constant*, unsigned, KInstruction*); + }; + + + class KModule { + public: + llvm::Module *module; + llvm::TargetData *targetData; + + // Some useful functions to know the address of + llvm::Function *dbgStopPointFn, *kleeMergeFn; + + // Our shadow versions of LLVM structures. + std::vector<KFunction*> functions; + std::map<llvm::Function*, KFunction*> functionMap; + + // Functions which escape (may be called indirectly) + // XXX change to KFunction + std::set<llvm::Function*> escapingFunctions; + + InstructionInfoTable *infos; + + std::vector<llvm::Constant*> constants; + std::map<llvm::Constant*, KConstant*> constantMap; + KConstant* getKConstant(llvm::Constant *c); + + Cell *constantTable; + + public: + KModule(llvm::Module *_module); + ~KModule(); + + /// Initialize local data structures. + // + // FIXME: ihandler should not be here + void prepare(const Interpreter::ModuleOptions &opts, + InterpreterHandler *ihandler); + + /// Return an id for the given constant, creating a new one if necessary. + unsigned getConstantID(llvm::Constant *c, KInstruction* ki); + }; +} // End klee namespace + +#endif diff --git a/include/klee/Internal/README.txt b/include/klee/Internal/README.txt new file mode 100644 index 00000000..9cedb653 --- /dev/null +++ b/include/klee/Internal/README.txt @@ -0,0 +1,3 @@ +This directory holds header files for things which are exposed as part +of the internal API of a library, but shouldn't be exposed to +externally. diff --git a/include/klee/Internal/Support/FloatEvaluation.h b/include/klee/Internal/Support/FloatEvaluation.h new file mode 100644 index 00000000..1d305374 --- /dev/null +++ b/include/klee/Internal/Support/FloatEvaluation.h @@ -0,0 +1,258 @@ +//===-- FloatEvaluation.h ---------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +// FIXME: Ditch this and use APFloat. + +#ifndef KLEE_UTIL_FLOATS_H +#define KLEE_UTIL_FLOATS_H + +#include "klee/util/Bits.h" //bits64::truncateToNBits +#include "IntEvaluation.h" //ints::sext + +#include "llvm/Support/MathExtras.h" + +namespace klee { +namespace floats { + +// ********************************** // +// *** Pack uint64_t into FP types ** // +// ********************************** // + +// interpret the 64 bits as a double instead of a uint64_t +inline double UInt64AsDouble( uint64_t bits ) { + double ret; + assert( sizeof(bits) == sizeof(ret) ); + memcpy( &ret, &bits, sizeof bits ); + return ret; +} + +// interpret the first 32 bits as a float instead of a uint64_t +inline float UInt64AsFloat( uint64_t bits ) { + uint32_t tmp = bits; // ensure that we read correct bytes + float ret; + assert( sizeof(tmp) == sizeof(ret) ); + memcpy( &ret, &tmp, sizeof tmp ); + return ret; +} + + +// ********************************** // +// *** Pack FP types into uint64_t ** // +// ********************************** // + +// interpret the 64 bits as a uint64_t instead of a double +inline uint64_t DoubleAsUInt64( double d ) { + uint64_t ret; + assert( sizeof(d) == sizeof(ret) ); + memcpy( &ret, &d, sizeof d ); + return ret; +} + +// interpret the 32 bits as a uint64_t instead of as a float (add 32 0s) +inline uint64_t FloatAsUInt64( float f ) { + uint32_t tmp; + assert( sizeof(tmp) == sizeof(f) ); + memcpy( &tmp, &f, sizeof f ); + return (uint64_t)tmp; +} + + +// ********************************** // +// ************ Constants *********** // +// ********************************** // + +const unsigned FLT_BITS = 32; +const unsigned DBL_BITS = 64; + + + +// ********************************** // +// ***** LLVM Binary Operations ***** // +// ********************************** // + +// add of l and r +inline uint64_t add(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) + UInt64AsFloat(r)), FLT_BITS); + case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) + UInt64AsDouble(r)), DBL_BITS); + default: assert(0 && "invalid floating point width"); + } +} + +// difference of l and r +inline uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) - UInt64AsFloat(r)), FLT_BITS); + case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) - UInt64AsDouble(r)), DBL_BITS); + default: assert(0 && "invalid floating point width"); + } +} + +// product of l and r +inline uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) * UInt64AsFloat(r)), FLT_BITS); + case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) * UInt64AsDouble(r)), DBL_BITS); + default: assert(0 && "invalid floating point width"); + } +} + +// signed divide of l by r +inline uint64_t div(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64(UInt64AsFloat(l) / UInt64AsFloat(r)), FLT_BITS); + case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64(UInt64AsDouble(l) / UInt64AsDouble(r)), DBL_BITS); + default: assert(0 && "invalid floating point width"); + } +} + +// signed modulo of l by r +inline uint64_t mod(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64( fmod(UInt64AsFloat(l), UInt64AsFloat(r)) ), FLT_BITS); + case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64( fmod(UInt64AsDouble(l), UInt64AsDouble(r)) ), DBL_BITS); + default: assert(0 && "invalid floating point width"); + } +} + + +// ********************************** // +// *** LLVM Comparison Operations *** // +// ********************************** // + +// determine if l represents NaN +inline bool isNaN(uint64_t l, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return llvm::IsNAN( UInt64AsFloat(l) ); + case DBL_BITS: return llvm::IsNAN( UInt64AsDouble(l) ); + default: assert(0 && "invalid floating point width"); + } +} + +inline uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return UInt64AsFloat(l) == UInt64AsFloat(r); + case DBL_BITS: return UInt64AsDouble(l) == UInt64AsDouble(r); + default: assert(0 && "invalid floating point width"); + } +} + +inline uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return UInt64AsFloat(l) != UInt64AsFloat(r); + case DBL_BITS: return UInt64AsDouble(l) != UInt64AsDouble(r); + default: assert(0 && "invalid floating point width"); + } +} + +inline uint64_t lt(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return UInt64AsFloat(l) < UInt64AsFloat(r); + case DBL_BITS: return UInt64AsDouble(l) < UInt64AsDouble(r); + default: assert(0 && "invalid floating point width"); + } +} + +inline uint64_t le(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return UInt64AsFloat(l) <= UInt64AsFloat(r); + case DBL_BITS: return UInt64AsDouble(l) <= UInt64AsDouble(r); + default: assert(0 && "invalid floating point width"); + } +} + +inline uint64_t gt(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return UInt64AsFloat(l) > UInt64AsFloat(r); + case DBL_BITS: return UInt64AsDouble(l) > UInt64AsDouble(r); + default: assert(0 && "invalid floating point width"); + } +} + +inline uint64_t ge(uint64_t l, uint64_t r, unsigned inWidth) { + switch( inWidth ) { + case FLT_BITS: return UInt64AsFloat(l) >= UInt64AsFloat(r); + case DBL_BITS: return UInt64AsDouble(l) >= UInt64AsDouble(r); + default: assert(0 && "invalid floating point width"); + } +} + + +// ********************************** // +// *** LLVM Conversion Operations *** // +// ********************************** // + +// truncation of l (which must be a double) to float (casts a double to a float) +inline uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth) { + // FIXME: Investigate this, should this not happen? Was a quick + // patch for busybox. + if (inWidth==64 && outWidth==64) { + return l; + } else { + assert(inWidth==64 && "can only truncate from a 64-bit double"); + assert(outWidth==32 && "can only truncate to a 32-bit float"); + float trunc = (float)UInt64AsDouble(l); + return bits64::truncateToNBits(FloatAsUInt64(trunc), outWidth); + } +} + +// extension of l (which must be a float) to double (casts a float to a double) +inline uint64_t ext(uint64_t l, unsigned outWidth, unsigned inWidth) { + // FIXME: Investigate this, should this not happen? Was a quick + // patch for busybox. + if (inWidth==64 && outWidth==64) { + return l; + } else { + assert(inWidth==32 && "can only extend from a 32-bit float"); + assert(outWidth==64 && "can only extend to a 64-bit double"); + double ext = (double)UInt64AsFloat(l); + return bits64::truncateToNBits(DoubleAsUInt64(ext), outWidth); + } +} + +// conversion of l to an unsigned integer, rounding towards zero +inline uint64_t toUnsignedInt( uint64_t l, unsigned outWidth, unsigned inWidth ) { + switch( inWidth ) { + case FLT_BITS: return bits64::truncateToNBits((uint64_t)UInt64AsFloat(l), outWidth ); + case DBL_BITS: return bits64::truncateToNBits((uint64_t)UInt64AsDouble(l), outWidth ); + default: assert(0 && "invalid floating point width"); + } +} + +// conversion of l to a signed integer, rounding towards zero +inline uint64_t toSignedInt( uint64_t l, unsigned outWidth, unsigned inWidth ) { + switch( inWidth ) { + case FLT_BITS: return bits64::truncateToNBits((int64_t)UInt64AsFloat(l), outWidth); + case DBL_BITS: return bits64::truncateToNBits((int64_t)UInt64AsDouble(l), outWidth); + default: assert(0 && "invalid floating point width"); + } +} + +// conversion of l, interpreted as an unsigned int, to a floating point number +inline uint64_t UnsignedIntToFP( uint64_t l, unsigned outWidth ) { + switch( outWidth ) { + case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64((float)l), outWidth); + case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64((double)l), outWidth); + default: assert(0 && "invalid floating point width"); + } +} + +// conversion of l, interpreted as a signed int, to a floating point number +inline uint64_t SignedIntToFP( uint64_t l, unsigned outWidth, unsigned inWidth ) { + switch( outWidth ) { + case FLT_BITS: return bits64::truncateToNBits(FloatAsUInt64((float)(int64_t)ints::sext(l, 64, inWidth)), outWidth); + case DBL_BITS: return bits64::truncateToNBits(DoubleAsUInt64((double)(int64_t)ints::sext(l,64, inWidth)), outWidth); + default: assert(0 && "invalid floating point width"); + } +} + +} // end namespace ints +} // end namespace klee + +#endif //KLEE_UTIL_FLOATS_H diff --git a/include/klee/Internal/Support/IntEvaluation.h b/include/klee/Internal/Support/IntEvaluation.h new file mode 100644 index 00000000..ed3ffc23 --- /dev/null +++ b/include/klee/Internal/Support/IntEvaluation.h @@ -0,0 +1,164 @@ +//===-- IntEvaluation.h -----------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_UTIL_INTEVALUATION_H +#define KLEE_UTIL_INTEVALUATION_H + +#include "klee/util/Bits.h" + +#define MAX_BITS (sizeof(uint64_t) * 8) + +// ASSUMPTION: invalid bits in each uint64_t are 0. the trade-off here is +// between making trunc/zext/sext fast and making operations that depend +// on the invalid bits being 0 fast. + +namespace klee { +namespace ints { + +// add of l and r +inline uint64_t add(uint64_t l, uint64_t r, unsigned inWidth) { + return bits64::truncateToNBits(l + r, inWidth); +} + +// difference of l and r +inline uint64_t sub(uint64_t l, uint64_t r, unsigned inWidth) { + return bits64::truncateToNBits(l - r, inWidth); +} + +// product of l and r +inline uint64_t mul(uint64_t l, uint64_t r, unsigned inWidth) { + return bits64::truncateToNBits(l * r, inWidth); +} + +// truncation of l to outWidth bits +inline uint64_t trunc(uint64_t l, unsigned outWidth, unsigned inWidth) { + return bits64::truncateToNBits(l, outWidth); +} + +// zero-extension of l from inWidth to outWidth bits +inline uint64_t zext(uint64_t l, unsigned outWidth, unsigned inWidth) { + return l; +} + +// sign-extension of l from inWidth to outWidth bits +inline uint64_t sext(uint64_t l, unsigned outWidth, unsigned inWidth) { + uint32_t numInvalidBits = MAX_BITS - inWidth; + return bits64::truncateToNBits(((int64_t)(l << numInvalidBits)) >> numInvalidBits, outWidth); +} + +// unsigned divide of l by r +inline uint64_t udiv(uint64_t l, uint64_t r, unsigned inWidth) { + return bits64::truncateToNBits(l / r, inWidth); +} + +// unsigned mod of l by r +inline uint64_t urem(uint64_t l, uint64_t r, unsigned inWidth) { + return bits64::truncateToNBits(l % r, inWidth); +} + +// signed divide of l by r +inline uint64_t sdiv(uint64_t l, uint64_t r, unsigned inWidth) { + // sign extend operands so that signed operation on 64-bits works correctly + int64_t sl = sext(l, MAX_BITS, inWidth); + int64_t sr = sext(r, MAX_BITS, inWidth); + return bits64::truncateToNBits(sl / sr, inWidth); +} + +// signed mod of l by r +inline uint64_t srem(uint64_t l, uint64_t r, unsigned inWidth) { + // sign extend operands so that signed operation on 64-bits works correctly + int64_t sl = sext(l, MAX_BITS, inWidth); + int64_t sr = sext(r, MAX_BITS, inWidth); + return bits64::truncateToNBits(sl % sr, inWidth); +} + +// arithmetic shift right of l by r bits +inline uint64_t ashr(uint64_t l, uint64_t shift, unsigned inWidth) { + int64_t sl = sext(l, MAX_BITS, inWidth); + return bits64::truncateToNBits(sl >> shift, inWidth); +} + +// logical shift right of l by r bits +inline uint64_t lshr(uint64_t l, uint64_t shift, unsigned inWidth) { + return l >> shift; +} + +// shift left of l by r bits +inline uint64_t shl(uint64_t l, uint64_t shift, unsigned inWidth) { + return bits64::truncateToNBits(l << shift, inWidth); +} + +// logical AND of l and r +inline uint64_t land(uint64_t l, uint64_t r, unsigned inWidth) { + return l & r; +} + +// logical OR of l and r +inline uint64_t lor(uint64_t l, uint64_t r, unsigned inWidth) { + return l | r; +} + +// logical XOR of l and r +inline uint64_t lxor(uint64_t l, uint64_t r, unsigned inWidth) { + return l ^ r; +} + +// comparison operations +inline uint64_t eq(uint64_t l, uint64_t r, unsigned inWidth) { + return l == r; +} + +inline uint64_t ne(uint64_t l, uint64_t r, unsigned inWidth) { + return l != r; +} + +inline uint64_t ult(uint64_t l, uint64_t r, unsigned inWidth) { + return l < r; +} + +inline uint64_t ule(uint64_t l, uint64_t r, unsigned inWidth) { + return l <= r; +} + +inline uint64_t ugt(uint64_t l, uint64_t r, unsigned inWidth) { + return l > r; +} + +inline uint64_t uge(uint64_t l, uint64_t r, unsigned inWidth) { + return l >= r; +} + +inline uint64_t slt(uint64_t l, uint64_t r, unsigned inWidth) { + int64_t sl = sext(l, MAX_BITS, inWidth); + int64_t sr = sext(r, MAX_BITS, inWidth); + return sl < sr; +} + +inline uint64_t sle(uint64_t l, uint64_t r, unsigned inWidth) { + int64_t sl = sext(l, MAX_BITS, inWidth); + int64_t sr = sext(r, MAX_BITS, inWidth); + return sl <= sr; +} + +inline uint64_t sgt(uint64_t l, uint64_t r, unsigned inWidth) { + int64_t sl = sext(l, MAX_BITS, inWidth); + int64_t sr = sext(r, MAX_BITS, inWidth); + return sl > sr; +} + +inline uint64_t sge(uint64_t l, uint64_t r, unsigned inWidth) { + int64_t sl = sext(l, MAX_BITS, inWidth); + int64_t sr = sext(r, MAX_BITS, inWidth); + return sl >= sr; +} + +} // end namespace ints +} // end namespace klee + +#endif diff --git a/include/klee/Internal/Support/ModuleUtil.h b/include/klee/Internal/Support/ModuleUtil.h new file mode 100644 index 00000000..6cf5fbee --- /dev/null +++ b/include/klee/Internal/Support/ModuleUtil.h @@ -0,0 +1,40 @@ +//===-- ModuleUtil.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_TRANSFORM_UTIL_H +#define KLEE_TRANSFORM_UTIL_H + +#include <string> + +namespace llvm { + class Function; + class Instruction; + class Module; +} + +namespace klee { + + /// Link a module with a specified bitcode archive. + llvm::Module *linkWithLibrary(llvm::Module *module, + const std::string &libraryName); + + /// Return the Function* target of a Call or Invoke instruction, or + /// null if it cannot be determined (should be only for indirect + /// calls, although complicated constant expressions might be + /// another possibility). + llvm::Function *getDirectCallTarget(const llvm::Instruction*); + + /// Return true iff the given Function value is used in something + /// other than a direct call (or a constant expression that + /// terminates in a direct call). + bool functionEscapes(const llvm::Function *f); + +} + +#endif diff --git a/include/klee/Internal/Support/QueryLog.h b/include/klee/Internal/Support/QueryLog.h new file mode 100644 index 00000000..b090d2d9 --- /dev/null +++ b/include/klee/Internal/Support/QueryLog.h @@ -0,0 +1,63 @@ +//===-- QueryLog.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_OPT_LOGGINGSOLVER_H +#define KLEE_OPT_LOGGINGSOLVER_H + +#include "klee/Expr.h" + +#include <vector> + +namespace klee { + struct Query; + + class QueryLogEntry { + public: + enum Type { + Validity, + Truth, + Value, + Cex + }; + + typedef std::vector< ref<Expr> > exprs_ty; + exprs_ty exprs; + + Type type; + ref<Expr> query; + unsigned instruction; + std::vector<const Array*> objects; + + public: + QueryLogEntry() : query(0,Expr::Bool) {} + QueryLogEntry(const QueryLogEntry &b); + QueryLogEntry(const Query &_query, + Type _type, + const std::vector<const Array*> *objects = 0); + }; + + class QueryLogResult { + public: + uint64_t result; + double time; + + public: + QueryLogResult() {} + QueryLogResult(bool _success, uint64_t _result, double _time) + : result(_result), time(_time) { + if (!_success) { // la la la + result = 0; + time = -1; + } + } + }; + +} + +#endif diff --git a/include/klee/Internal/Support/Timer.h b/include/klee/Internal/Support/Timer.h new file mode 100644 index 00000000..a422abd0 --- /dev/null +++ b/include/klee/Internal/Support/Timer.h @@ -0,0 +1,28 @@ +//===-- Timer.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_TIMER_H +#define KLEE_TIMER_H + +#include <stdint.h> + +namespace klee { + class WallTimer { + uint64_t startMicroseconds; + + public: + WallTimer(); + + /// check - Return the delta since the timer was created, in microseconds. + uint64_t check(); + }; +} + +#endif + diff --git a/include/klee/Internal/System/Time.h b/include/klee/Internal/System/Time.h new file mode 100644 index 00000000..5229c8c9 --- /dev/null +++ b/include/klee/Internal/System/Time.h @@ -0,0 +1,20 @@ +//===-- Time.h --------------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_UTIL_TIME_H +#define KLEE_UTIL_TIME_H + +namespace klee { + namespace util { + double getUserTime(); + double getWallTime(); + } +} + +#endif diff --git a/include/klee/Interpreter.h b/include/klee/Interpreter.h new file mode 100644 index 00000000..eca6e59e --- /dev/null +++ b/include/klee/Interpreter.h @@ -0,0 +1,149 @@ +//===-- Interpreter.h - Abstract Execution Engine Interface -----*- 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_INTERPRETER_H +#define KLEE_INTERPRETER_H + +#include <vector> +#include <string> +#include <map> +#include <set> + +struct BOut; + +namespace llvm { +class Function; +class Module; +} + +namespace klee { +class ExecutionState; +class Interpreter; +class TreeStreamWriter; + +class InterpreterHandler { +public: + InterpreterHandler() {} + virtual ~InterpreterHandler() {}; + + virtual std::ostream &getInfoStream() const = 0; + + virtual std::string getOutputFilename(const std::string &filename) = 0; + virtual std::ostream *openOutputFile(const std::string &filename) = 0; + + virtual void incPathsExplored() = 0; + + virtual void processTestCase(const ExecutionState &state, + const char *err, + const char *suffix) = 0; +}; + +class Interpreter { +public: + /// ModuleOptions - Module level options which can be set when + /// registering a module with the interpreter. + struct ModuleOptions { + std::string LibraryDir; + bool Optimize; + bool CheckDivZero; + + ModuleOptions(const std::string& _LibraryDir, + bool _Optimize, bool _CheckDivZero) + : LibraryDir(_LibraryDir), Optimize(_Optimize), + CheckDivZero(_CheckDivZero) {} + }; + + /// InterpreterOptions - Options varying the runtime behavior during + /// interpretation. + struct InterpreterOptions { + /// A frequency at which to make concrete reads return constrained + /// symbolic values. This is used to test the correctness of the + /// symbolic execution on concrete programs. + unsigned MakeConcreteSymbolic; + + InterpreterOptions() + : MakeConcreteSymbolic(false) + {} + }; + +protected: + const InterpreterOptions interpreterOpts; + + Interpreter(const InterpreterOptions &_interpreterOpts) + : interpreterOpts(_interpreterOpts) + {}; + +public: + virtual ~Interpreter() {}; + + static Interpreter *create(const InterpreterOptions &_interpreterOpts, + InterpreterHandler *ih); + + /// Register the module to be executed. + /// + /// \return The final module after it has been optimized, checks + /// inserted, and modified for interpretation. + virtual const llvm::Module * + setModule(llvm::Module *module, + const ModuleOptions &opts) = 0; + + // supply a tree stream writer which the interpreter will use + // to record the concrete path (as a stream of '0' and '1' bytes). + virtual void setPathWriter(TreeStreamWriter *tsw) = 0; + + // supply a tree stream writer which the interpreter will use + // to record the symbolic path (as a stream of '0' and '1' bytes). + virtual void setSymbolicPathWriter(TreeStreamWriter *tsw) = 0; + + // supply a test case to replay from. this can be used to drive the + // interpretation down a user specified path. use null to reset. + virtual void setReplayOut(const struct BOut *out) = 0; + + // supply a list of branch decisions specifying which direction to + // take on forks. this can be used to drive the interpretation down + // a user specified path. use null to reset. + virtual void setReplayPath(const std::vector<bool> *path) = 0; + + // supply a set of symbolic bindings that will be used as "seeds" + // for the search. use null to reset. + virtual void useSeeds(const std::vector<struct BOut *> *seeds) = 0; + + virtual void runFunctionAsMain(llvm::Function *f, + int argc, + char **argv, + char **envp) = 0; + + /*** Runtime options ***/ + + virtual void setHaltExecution(bool value) = 0; + + virtual void setInhibitForking(bool value) = 0; + + /*** State accessor methods ***/ + + virtual unsigned getPathStreamID(const ExecutionState &state) = 0; + + virtual unsigned getSymbolicPathStreamID(const ExecutionState &state) = 0; + + virtual void getConstraintLog(const ExecutionState &state, + std::string &res, + bool asCVC = false) = 0; + + virtual bool getSymbolicSolution(const ExecutionState &state, + std::vector< + std::pair<std::string, + std::vector<unsigned char> > > + &res) = 0; + + virtual void getCoveredLines(const ExecutionState &state, + std::map<const std::string*, std::set<unsigned> > &res) = 0; +}; + +} // End klee namespace + +#endif diff --git a/include/klee/Machine.h b/include/klee/Machine.h new file mode 100644 index 00000000..b8a9e9ac --- /dev/null +++ b/include/klee/Machine.h @@ -0,0 +1,28 @@ +//===-- Machine.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_MACHINE_H__ +#define __KLEE_MACHINE_H__ + +#include "klee/Expr.h" + +namespace klee { + namespace machine { + enum ByteOrder { + LSB = 0, + MSB = 1 + }; + } +} + +#define kMachineByteOrder klee::machine::LSB +#define kMachinePointerType Expr::Int32 +#define kMachinePointerSize 4 + +#endif /* __KLEE_MACHINE_H__ */ diff --git a/include/klee/Solver.h b/include/klee/Solver.h new file mode 100644 index 00000000..2d4fa044 --- /dev/null +++ b/include/klee/Solver.h @@ -0,0 +1,216 @@ +//===-- Solver.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_SOLVER_H +#define KLEE_SOLVER_H + +#include "klee/Expr.h" + +#include <vector> + +namespace klee { + class ConstraintManager; + class Expr; + class SolverImpl; + + struct Query { + public: + const ConstraintManager &constraints; + ref<Expr> expr; + + Query(const ConstraintManager& _constraints, ref<Expr> _expr) + : constraints(_constraints), expr(_expr) { + } + + /// withExpr - Return a copy of the query with the given expression. + Query withExpr(ref<Expr> _expr) const { + return Query(constraints, _expr); + } + + /// withFalse - Return a copy of the query with a false expression. + Query withFalse() const { + return Query(constraints, ref<Expr>(0, Expr::Bool)); + } + + /// negateExpr - Return a copy of the query with the expression negated. + Query negateExpr() const { + return withExpr(Expr::createNot(expr)); + } + }; + + class Solver { + // DO NOT IMPLEMENT. + Solver(const Solver&); + void operator=(const Solver&); + + public: + enum Validity { + True = 1, + False = -1, + Unknown = 0 + }; + + public: + /// validity_to_str - Return the name of given Validity enum value. + static const char *validity_to_str(Validity v); + + public: + SolverImpl *impl; + + public: + Solver(SolverImpl *_impl) : impl(_impl) {}; + ~Solver(); + + /// evaluate - Determine the full validity of an expression in particular + /// state. + //// + /// \param [out] result - The validity of the given expression (provably + /// true, provably false, or neither). + /// + /// \return True on success. + bool evaluate(const Query&, Validity &result); + + /// mustBeTrue - Determine if the expression is provably true. + /// + /// \param [out] result - On success, true iff the expresssion is provably + /// false. + /// + /// \return True on success. + bool mustBeTrue(const Query&, bool &result); + + /// mustBeFalse - Determine if the expression is provably false. + /// + /// \param [out] result - On success, true iff the expresssion is provably + /// false. + /// + /// \return True on success. + bool mustBeFalse(const Query&, bool &result); + + /// mayBeTrue - Determine if there is a valid assignment for the given state + /// in which the expression evaluates to false. + /// + /// \param [out] result - On success, true iff the expresssion is true for + /// some satisfying assignment. + /// + /// \return True on success. + bool mayBeTrue(const Query&, bool &result); + + /// mayBeFalse - Determine if there is a valid assignment for the given + /// state in which the expression evaluates to false. + /// + /// \param [out] result - On success, true iff the expresssion is false for + /// some satisfying assignment. + /// + /// \return True on success. + bool mayBeFalse(const Query&, bool &result); + + /// getValue - Compute one possible value for the given expression. + /// + /// \param [out] result - On success, a value for the expression in some + /// satisying assignment. + /// + /// \return True on success. + bool getValue(const Query&, ref<Expr> &result); + + /// getInitialValues - Compute the initial values for a list of objects. + /// + /// \param [out] result - On success, this vector will be filled in with an + /// array of bytes for each given object (with length matching the object + /// size). The bytes correspond to the initial values for the objects for + /// some satisying assignment. + /// + /// \return True on success. + /// + /// NOTE: This function returns failure if there is no satisfying + /// assignment. + // + // FIXME: This API is lame. We should probably just provide an API which + // returns an Assignment object, then clients can get out whatever values + // they want. This also allows us to optimize the representation. + bool getInitialValues(const Query&, + const std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &result); + + /// getRange - Compute a tight range of possible values for a given + /// expression. + /// + /// \return - A pair with (min, max) values for the expression. + /// + /// \post(mustBeTrue(min <= e <= max) && + /// mayBeTrue(min == e) && + /// mayBeTrue(max == e)) + // + // FIXME: This should go into a helper class, and should handle failure. + virtual std::pair< ref<Expr>, ref<Expr> > getRange(const Query&); + }; + + /// STPSolver - A complete solver based on STP. + class STPSolver : public Solver { + public: + /// STPSolver - Construct a new STPSolver. + /// + /// \param useForkedSTP - Whether STP should be run in a separate process + /// (required for using timeouts). + STPSolver(bool useForkedSTP); + + /// getConstraintLog - Return the constraint log for the given state in CVC + /// format. + char *getConstraintLog(const Query&); + + /// setTimeout - Set constraint solver timeout delay to the given value; 0 + /// is off. + void setTimeout(double timeout); + }; + + /* *** */ + + /// createValidatingSolver - Create a solver which will validate all query + /// results against an oracle, used for testing that an optimized solver has + /// the same results as an unoptimized one. This solver will assert on any + /// mismatches. + /// + /// \param s - The primary underlying solver to use. + /// \param oracle - The solver to check query results against. + Solver *createValidatingSolver(Solver *s, Solver *oracle); + + /// createCachingSolver - Create a solver which will cache the queries in + /// memory (without eviction). + /// + /// \param s - The underlying solver to use. + Solver *createCachingSolver(Solver *s); + + /// createCexCachingSolver - Create a counterexample caching solver. This is a + /// more sophisticated cache which records counterexamples for a constraint + /// set and uses subset/superset relations among constraints to try and + /// quickly find satisfying assignments. + /// + /// \param s - The underlying solver to use. + Solver *createCexCachingSolver(Solver *s); + + /// createFastCexSolver - Create a "fast counterexample solver", which tries + /// to quickly compute a satisfying assignment for a constraint set using + /// value propogation and range analysis. + /// + /// \param s - The underlying solver to use. + Solver *createFastCexSolver(Solver *s); + + /// createIndependentSolver - Create a solver which will eliminate any + /// unnecessary constraints before propogating the query to the underlying + /// solver. + /// + /// \param s - The underlying solver to use. + Solver *createIndependentSolver(Solver *s); + + /// createPCLoggingSolver - Create a solver which will forward all queries + /// after writing them to the given path in .pc format. + Solver *createPCLoggingSolver(Solver *s, std::string path); + +} + +#endif diff --git a/include/klee/SolverImpl.h b/include/klee/SolverImpl.h new file mode 100644 index 00000000..29c356be --- /dev/null +++ b/include/klee/SolverImpl.h @@ -0,0 +1,63 @@ +//===-- SolverImpl.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_SOLVERIMPL_H +#define KLEE_SOLVERIMPL_H + +#include <vector> + +namespace klee { + class Array; + class ExecutionState; + class Expr; + struct Query; + + /// SolverImpl - Abstract base clase for solver implementations. + class SolverImpl { + // DO NOT IMPLEMENT. + SolverImpl(const SolverImpl&); + void operator=(const SolverImpl&); + + public: + SolverImpl() {} + virtual ~SolverImpl(); + + /// computeValidity - Compute a full validity result for the + /// query. + /// + /// The query expression is guaranteed to be non-constant and have + /// bool type. + /// + /// SolverImpl provides a default implementation which uses + /// computeTruth. Clients should override this if a more efficient + /// implementation is available. + virtual bool computeValidity(const Query& query, Solver::Validity &result); + + /// computeTruth - Determine whether the given query is provable. + /// + /// The query expression is guaranteed to be non-constant and have + /// bool type. + virtual bool computeTruth(const Query& query, bool &isValid) = 0; + + /// computeValue - Compute a feasible value for the expression. + /// + /// The query expression is guaranteed to be non-constant. + virtual bool computeValue(const Query& query, ref<Expr> &result) = 0; + + virtual bool computeInitialValues(const Query& query, + const std::vector<const Array*> + &objects, + std::vector< std::vector<unsigned char> > + &values, + bool &hasSolution) = 0; +}; + +} + +#endif diff --git a/include/klee/Statistic.h b/include/klee/Statistic.h new file mode 100644 index 00000000..e5aef6b1 --- /dev/null +++ b/include/klee/Statistic.h @@ -0,0 +1,65 @@ +//===-- Statistic.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_STATISTIC_H +#define KLEE_STATISTIC_H + +#include <string> + +namespace klee { + class Statistic; + class StatisticManager; + class StatisticRecord; + + /// Statistic - A named statistic instance. + /// + /// The Statistic class holds information about the statistic, but + /// not the actual values. Values are managed by the global + /// StatisticManager to enable transparent support for instruction + /// level and call path level statistics. + class Statistic { + friend class StatisticManager; + friend class StatisticRecord; + + private: + unsigned id; + const std::string name; + const std::string shortName; + + public: + Statistic(const std::string &_name, + const std::string &_shortName); + ~Statistic(); + + /// getID - Get the unique statistic ID. + unsigned getID() { return id; } + + /// getName - Get the statistic name. + const std::string &getName() const { return name; } + + /// getShortName - Get the "short" statistic name, used in + /// callgrind output for example. + const std::string &getShortName() const { return shortName; } + + /// getValue - Get the current primary statistic value. + uint64_t getValue() const; + + /// operator uint64_t - Get the current primary statistic value. + operator uint64_t () const { return getValue(); } + + /// operator++ - Increment the statistic by 1. + Statistic &operator ++() { return (*this += 1); } + + /// operator+= - Increment the statistic by \arg addend. + Statistic &operator +=(const uint64_t addend); + }; +} + +#endif + diff --git a/include/klee/Statistics.h b/include/klee/Statistics.h new file mode 100644 index 00000000..20ab2528 --- /dev/null +++ b/include/klee/Statistics.h @@ -0,0 +1,154 @@ +//===-- Statistics.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_STATISTICS_H +#define KLEE_STATISTICS_H + +#include "Statistic.h" + +#include <vector> +#include <string> +#include <string.h> + +namespace klee { + class Statistic; + class StatisticRecord { + friend class StatisticManager; + + private: + uint64_t *data; + + public: + StatisticRecord(); + StatisticRecord(const StatisticRecord &s); + ~StatisticRecord() { delete[] data; } + + void zero(); + + uint64_t getValue(const Statistic &s) const; + void incrementValue(const Statistic &s, uint64_t addend) const; + StatisticRecord &operator =(const StatisticRecord &s); + StatisticRecord &operator +=(const StatisticRecord &sr); + }; + + class StatisticManager { + private: + bool enabled; + std::vector<Statistic*> stats; + uint64_t *globalStats; + uint64_t *indexedStats; + StatisticRecord *contextStats; + unsigned index; + + public: + StatisticManager(); + ~StatisticManager(); + + void useIndexedStats(unsigned totalIndices); + + StatisticRecord *getContext(); + void setContext(StatisticRecord *sr); /* null to reset */ + + void setIndex(unsigned i) { index = i; } + unsigned getIndex() { return index; } + unsigned getNumStatistics() { return stats.size(); } + Statistic &getStatistic(unsigned i) { return *stats[i]; } + + void registerStatistic(Statistic &s); + void incrementStatistic(Statistic &s, uint64_t addend); + uint64_t getValue(const Statistic &s) const; + void incrementIndexedValue(const Statistic &s, unsigned index, + uint64_t addend) const; + uint64_t getIndexedValue(const Statistic &s, unsigned index) const; + void setIndexedValue(const Statistic &s, unsigned index, uint64_t value); + int getStatisticID(const std::string &name) const; + Statistic *getStatisticByName(const std::string &name) const; + }; + + extern StatisticManager *theStatisticManager; + + inline void StatisticManager::incrementStatistic(Statistic &s, + uint64_t addend) { + if (enabled) { + globalStats[s.id] += addend; + if (indexedStats) { + indexedStats[index*stats.size() + s.id] += addend; + if (contextStats) + contextStats->data[s.id] += addend; + } + } + } + + inline StatisticRecord *StatisticManager::getContext() { + return contextStats; + } + inline void StatisticManager::setContext(StatisticRecord *sr) { + contextStats = sr; + } + + inline void StatisticRecord::zero() { + ::memset(data, 0, sizeof(*data)*theStatisticManager->getNumStatistics()); + } + + inline StatisticRecord::StatisticRecord() + : data(new uint64_t[theStatisticManager->getNumStatistics()]) { + zero(); + } + + inline StatisticRecord::StatisticRecord(const StatisticRecord &s) + : data(new uint64_t[theStatisticManager->getNumStatistics()]) { + ::memcpy(data, s.data, + sizeof(*data)*theStatisticManager->getNumStatistics()); + } + + inline StatisticRecord &StatisticRecord::operator=(const StatisticRecord &s) { + ::memcpy(data, s.data, + sizeof(*data)*theStatisticManager->getNumStatistics()); + return *this; + } + + inline void StatisticRecord::incrementValue(const Statistic &s, + uint64_t addend) const { + data[s.id] += addend; + } + inline uint64_t StatisticRecord::getValue(const Statistic &s) const { + return data[s.id]; + } + + inline StatisticRecord & + StatisticRecord::operator +=(const StatisticRecord &sr) { + unsigned nStats = theStatisticManager->getNumStatistics(); + for (unsigned i=0; i<nStats; i++) + data[i] += sr.data[i]; + return *this; + } + + inline uint64_t StatisticManager::getValue(const Statistic &s) const { + return globalStats[s.id]; + } + + inline void StatisticManager::incrementIndexedValue(const Statistic &s, + unsigned index, + uint64_t addend) const { + indexedStats[index*stats.size() + s.id] += addend; + } + + inline uint64_t StatisticManager::getIndexedValue(const Statistic &s, + unsigned index) const { + return indexedStats[index*stats.size() + s.id]; + } + + inline void StatisticManager::setIndexedValue(const Statistic &s, + unsigned index, + uint64_t value) { + indexedStats[index*stats.size() + s.id] = value; + } +} + +#endif diff --git a/include/klee/TimerStatIncrementer.h b/include/klee/TimerStatIncrementer.h new file mode 100644 index 00000000..35495d8b --- /dev/null +++ b/include/klee/TimerStatIncrementer.h @@ -0,0 +1,32 @@ +//===-- TimerStatIncrementer.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_TIMERSTATINCREMENTER_H +#define KLEE_TIMERSTATINCREMENTER_H + +#include "klee/Statistics.h" +#include "klee/Internal/Support/Timer.h" + +namespace klee { + class TimerStatIncrementer { + private: + WallTimer timer; + Statistic &statistic; + + public: + TimerStatIncrementer(Statistic &_statistic) : statistic(_statistic) {} + ~TimerStatIncrementer() { + statistic += timer.check(); + }; + + uint64_t check() { return timer.check(); } + }; +} + +#endif diff --git a/include/klee/klee.h b/include/klee/klee.h new file mode 100644 index 00000000..698a61c4 --- /dev/null +++ b/include/klee/klee.h @@ -0,0 +1,120 @@ +//===-- klee.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_H__ +#define __KLEE_H__ + +#ifdef __cplusplus +extern "C" { +#endif + + /* Add an accesible memory object at a user specified location. It + is the users responsibility to make sure that these memory + objects do not overlap. These memory objects will also + (obviously) not correctly interact with external function + calls. */ + void klee_define_fixed_object(void *addr, unsigned nbytes); + + /* make the contents of the object pointed to by addr symbolic. addr + * should always be the start of the object and nbytes must be its + * entire size. name is an optional name (can be the empty string) + */ + void klee_make_symbolic_name(void *addr, unsigned nbytes, + const char *name); + + void klee_make_symbolic(void *addr, unsigned nbytes); + + /* Return symbolic value in the (signed) interval [begin,end) */ + int klee_range(int begin, int end, const char *name); + + /* Return a symbolic integer */ + int klee_int(const char *name); + + void *klee_malloc_n(unsigned nelems, unsigned size, unsigned alignment); + + /* terminate the state without generating a test file */ + __attribute__((noreturn)) + void klee_silent_exit(int status); + + __attribute__((noreturn)) + void klee_abort(void); + + /** Report an error and terminate the state. */ + __attribute__((noreturn)) + void klee_report_error(const char *file, + int line, + const char *message, + const char *suffix); + + /* called by checking code to get size of memory. */ + unsigned klee_get_obj_size(void *ptr); + + /* print the tree associated w/ a given expression. */ + void klee_print_expr(const char *msg, ...); + + /* NB: this *does not* fork n times and return [0,n) in children. + * It makes n be symbolic and returns: caller must compare N times. + */ + unsigned klee_choose(unsigned n); + + /* special klee assert macro. this assert should be used when path consistency + * across platforms is desired (e.g., in tests). + * NB: __assert_fail is a klee "special" function + */ +# define klee_assert(expr) \ + ((expr) \ + ? (void) (0) \ + : __assert_fail (#expr, __FILE__, __LINE__, __PRETTY_FUNCTION__)) \ + + /* Return true if the given value is symbolic (represented by an + * expression) in the current state. This is primarily for debugging + * and writing tests but can also be used to enable prints in replay + * mode. + */ + unsigned klee_is_symbolic(unsigned n); + + + /* The following intrinsics are primarily intended for internal use + and may have peculiar semantics. */ + + void klee_assume(unsigned condition); + void klee_warning(const char *message); + void klee_warning_once(const char *message); + void klee_prefer_cex(void *object, unsigned condition); + void klee_mark_global(void *object); + + /* Return a possible constant value for the input expression. This + allows programs to forcibly concretize values on their own. */ + unsigned klee_get_value(unsigned expr); + + /* Ensure that memory in the range [address, address+size) is + accessible to the program. If some byte in the range is not + accessible an error will be generated and the state + terminated. + + The current implementation requires both address and size to be + constants and that the range lie within a single object. */ + void klee_check_memory_access(const void *address, unsigned size); + + /* Enable/disable forking. */ + void klee_set_forking(unsigned enable); + + /* klee_alias_function("foo", "bar") will replace, at runtime (on + the current path and all paths spawned on the current path), all + calls to foo() by calls to bar(). foo() and bar() have to exist + and have identical types. Use klee_alias_function("foo", "foo") + to undo. Be aware that some special functions, such as exit(), + may not always work. */ + void klee_alias_function(const char* fn_name, const char* new_fn_name); + +#ifdef __cplusplus +} +#endif + +#endif /* __KLEE_H__ */ diff --git a/include/klee/util/Assignment.h b/include/klee/util/Assignment.h new file mode 100644 index 00000000..19f89a03 --- /dev/null +++ b/include/klee/util/Assignment.h @@ -0,0 +1,100 @@ +//===-- 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_UTIL_ASSIGNMENT_H +#define KLEE_UTIL_ASSIGNMENT_H + +#include <map> + +#include "klee/util/ExprEvaluator.h" + +// FIXME: Rename? + +namespace klee { + class Array; + + class Assignment { + public: + typedef std::map<const Array*, std::vector<unsigned char> > bindings_ty; + + bool allowFreeValues; + bindings_ty bindings; + + public: + Assignment(bool _allowFreeValues=false) + : allowFreeValues(_allowFreeValues) {} + Assignment(std::vector<const Array*> &objects, + std::vector< std::vector<unsigned char> > &values, + bool _allowFreeValues=false) + : allowFreeValues(_allowFreeValues){ + std::vector< std::vector<unsigned char> >::iterator valIt = + values.begin(); + for (std::vector<const Array*>::iterator it = objects.begin(), + ie = objects.end(); it != ie; ++it) { + const Array *os = *it; + std::vector<unsigned char> &arr = *valIt; + bindings.insert(std::make_pair(os, arr)); + ++valIt; + } + } + + ref<Expr> evaluate(const Array *mo, unsigned index) const; + ref<Expr> evaluate(ref<Expr> e); + + template<typename InputIterator> + bool satisfies(InputIterator begin, InputIterator end); + }; + + class AssignmentEvaluator : public ExprEvaluator { + const Assignment &a; + + protected: + ref<Expr> getInitialValue(const Array &mo, unsigned index) { + return a.evaluate(&mo, index); + } + + public: + AssignmentEvaluator(const Assignment &_a) : a(_a) {} + }; + + /***/ + + inline ref<Expr> Assignment::evaluate(const Array *array, + unsigned index) const { + bindings_ty::const_iterator it = bindings.find(array); + if (it!=bindings.end() && index<it->second.size()) { + return ref<Expr>(it->second[index], Expr::Int8); + } else { + if (allowFreeValues) { + return ReadExpr::create(UpdateList(array, true, 0), + ref<Expr>(index, Expr::Int32)); + } else { + return ref<Expr>(0, Expr::Int8); + } + } + } + + inline ref<Expr> Assignment::evaluate(ref<Expr> e) { + AssignmentEvaluator v(*this); + return v.visit(e); + } + + template<typename InputIterator> + inline bool Assignment::satisfies(InputIterator begin, InputIterator end) { + AssignmentEvaluator v(*this); + for (; begin!=end; ++begin) { + ref<Expr> res = v.visit(*begin); + if (!res.isConstant() || !res.getConstantValue()) + return false; + } + return true; + } +} + +#endif diff --git a/include/klee/util/BitArray.h b/include/klee/util/BitArray.h new file mode 100644 index 00000000..6f887600 --- /dev/null +++ b/include/klee/util/BitArray.h @@ -0,0 +1,42 @@ +//===-- BitArray.h ----------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_UTIL_BITARRAY_H +#define KLEE_UTIL_BITARRAY_H + +namespace klee { + + // XXX would be nice not to have + // two allocations here for allocated + // BitArrays +class BitArray { +private: + uint32_t *bits; + +protected: + static uint32_t length(unsigned size) { return (size+31)/32; } + +public: + BitArray(unsigned size, bool value = false) : bits(new uint32_t[length(size)]) { + memset(bits, value?0xFF:0, sizeof(*bits)*length(size)); + } + BitArray(const BitArray &b, unsigned size) : bits(new uint32_t[length(size)]) { + memcpy(bits, b.bits, sizeof(*bits)*length(size)); + } + ~BitArray() { delete[] bits; } + + bool get(unsigned idx) { return (bool) ((bits[idx/32]>>(idx&0x1F))&1); } + void set(unsigned idx) { bits[idx/32] |= 1<<(idx&0x1F); } + void unset(unsigned idx) { bits[idx/32] &= ~(1<<(idx&0x1F)); } + void set(unsigned idx, bool value) { if (value) set(idx); else unset(idx); } +}; + +} // End klee namespace + +#endif diff --git a/include/klee/util/Bits.h b/include/klee/util/Bits.h new file mode 100644 index 00000000..ffbda09e --- /dev/null +++ b/include/klee/util/Bits.h @@ -0,0 +1,102 @@ +//===-- Bits.h --------------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_UTIL_BITS_H +#define KLEE_UTIL_BITS_H + +#include "llvm/Support/DataTypes.h" + +namespace klee { + namespace bits32 { + // @pre(0 <= N <= 32) + // @post(retval = max([truncateToNBits(i,N) for i in naturals()])) + inline unsigned maxValueOfNBits(unsigned N) { + if (N==0) + return 0; + return ((unsigned) -1) >> (32 - N); + } + + // @pre(0 < N <= 32) + inline unsigned truncateToNBits(unsigned x, unsigned N) { + return x&(((unsigned) -1) >> (32 - N)); + } + + inline unsigned withoutRightmostBit(unsigned x) { + return x&(x-1); + } + + inline unsigned isolateRightmostBit(unsigned x) { + return x&-x; + } + + inline unsigned isPowerOfTwo(unsigned x) { + if (x==0) return 0; + return !(x&(x-1)); + } + + // @pre(withoutRightmostBit(x) == 0) + // @post((1 << retval) == x) + inline unsigned indexOfSingleBit(unsigned x) { + unsigned res = 0; + if (x&0xFFFF0000) res += 16; + if (x&0xFF00FF00) res += 8; + if (x&0xF0F0F0F0) res += 4; + if (x&0xCCCCCCCC) res += 2; + if (x&0xAAAAAAAA) res += 1; + return res; + } + + inline unsigned indexOfRightmostBit(unsigned x) { + return indexOfSingleBit(isolateRightmostBit(x)); + } + } + + namespace bits64 { + // @pre(0 <= N <= 32) + // @post(retval = max([truncateToNBits(i,N) for i in naturals()])) + inline uint64_t maxValueOfNBits(unsigned N) { + if (N==0) + return 0; + return ((uint64_t) (int64_t) -1) >> (64 - N); + } + + // @pre(0 < N <= 64) + inline uint64_t truncateToNBits(uint64_t x, unsigned N) { + return x&(((uint64_t) (int64_t) -1) >> (64 - N)); + } + + inline uint64_t withoutRightmostBit(uint64_t x) { + return x&(x-1); + } + + inline uint64_t isolateRightmostBit(uint64_t x) { + return x&-x; + } + + inline uint64_t isPowerOfTwo(uint64_t x) { + if (x==0) return 0; + return !(x&(x-1)); + } + + // @pre((x&(x-1)) == 0) + // @post((1 << retval) == x) + inline unsigned indexOfSingleBit(uint64_t x) { + unsigned res = bits32::indexOfSingleBit((unsigned) (x | (x>>32))); + if (x&((uint64_t) 0xFFFFFFFF << 32)) + res += 32; + return res; + } + + inline uint64_t indexOfRightmostBit(uint64_t x) { + return indexOfSingleBit(isolateRightmostBit(x)); + } + } +} // End klee namespace + +#endif diff --git a/include/klee/util/ExprEvaluator.h b/include/klee/util/ExprEvaluator.h new file mode 100644 index 00000000..be98942d --- /dev/null +++ b/include/klee/util/ExprEvaluator.h @@ -0,0 +1,39 @@ +//===-- 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 protectedDivOperation(const BinaryExpr &e); + Action visitUDiv(const UDivExpr &e); + Action visitSDiv(const SDivExpr &e); + Action visitURem(const URemExpr &e); + Action visitSRem(const SRemExpr &e); + + public: + ExprEvaluator() {} + + // override to implement evaluation, this function is called to + // get the initial value for a symbolic byte. if the value is + // unknown then the user can simply return a ReadExpr at version 0 + // of this MemoryObject. + virtual ref<Expr> getInitialValue(const Array& os, unsigned index) = 0; + }; +} + +#endif diff --git a/include/klee/util/ExprHashMap.h b/include/klee/util/ExprHashMap.h new file mode 100644 index 00000000..d9f95bff --- /dev/null +++ b/include/klee/util/ExprHashMap.h @@ -0,0 +1,48 @@ +//===-- 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 <tr1/unordered_map> +#include <tr1/unordered_set> + +namespace klee { + + namespace util { + struct ExprHash { + unsigned operator()(const ref<Expr> e) const { + return e.hash(); + } + }; + + struct ExprCmp { + bool operator()(const ref<Expr> &a, const ref<Expr> &b) const { + return a==b; + } + }; + } + + template<class T> + class ExprHashMap : + + public std::tr1::unordered_map<ref<Expr>, + T, + klee::util::ExprHash, + klee::util::ExprCmp> { + }; + + typedef std::tr1::unordered_set<ref<Expr>, + klee::util::ExprHash, + klee::util::ExprCmp> ExprHashSet; + +} + +#endif diff --git a/include/klee/util/ExprPPrinter.h b/include/klee/util/ExprPPrinter.h new file mode 100644 index 00000000..a1961e2b --- /dev/null +++ b/include/klee/util/ExprPPrinter.h @@ -0,0 +1,58 @@ +//===-- 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 klee { + class ConstraintManager; + + class ExprPPrinter { + protected: + ExprPPrinter() {} + + public: + static ExprPPrinter *create(std::ostream &os); + + virtual ~ExprPPrinter() {} + + virtual void setNewline(const std::string &newline) = 0; + virtual void reset() = 0; + virtual void scan(const ref<Expr> &e) = 0; + virtual void print(const ref<Expr> &e, unsigned indent=0) = 0; + + // utility methods + + template<class Container> + void scan(Container c) { + scan(c.begin(), c.end()); + } + + template<class InputIterator> + void scan(InputIterator it, InputIterator end) { + for (; it!=end; ++it) + scan(*it); + } + + static void printOne(std::ostream &os, const char *message, + const ref<Expr> &e); + + static void printConstraints(std::ostream &os, + const ConstraintManager &constraints); + + static void printQuery(std::ostream &os, + const ConstraintManager &constraints, + const ref<Expr> &q); + }; + +} + +#endif diff --git a/include/klee/util/ExprRangeEvaluator.h b/include/klee/util/ExprRangeEvaluator.h new file mode 100644 index 00000000..3729b5c2 --- /dev/null +++ b/include/klee/util/ExprRangeEvaluator.h @@ -0,0 +1,283 @@ +//===-- 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 T> +class ExprRangeEvaluator { +protected: + virtual T getInitialReadRange(const Array &os, T index) = 0; + + T evalRead(const UpdateList &ul, T index); + +public: + ExprRangeEvaluator() {} + virtual ~ExprRangeEvaluator() {} + + T evaluate(const ref<Expr> &e); +}; + +template<class T> +T ExprRangeEvaluator<T>::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<class T> +T ExprRangeEvaluator<T>::evaluate(const ref<Expr> &e) { + switch (e.getKind()) { + case Expr::Constant: + return T(e.getConstantValue()); + + case Expr::NotOptimized: + break; + + case Expr::Read: { + const ReadExpr *re = static_ref_cast<const ReadExpr>(e); + T index = evaluate(re->index); + + assert(re->getWidth()==Expr::Int8 && "unexpected multibyte read"); + + return evalRead(re->updates, index); + } + + case Expr::Select: { + const SelectExpr *se = static_ref_cast<const SelectExpr>(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; i<ep->getNumKids(); i++) + res = res.concat(evaluate(ep->getKid(i)),8); + return res; + } + + // Arithmetic + + case Expr::Add: { + const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e); + unsigned width = be->left.getWidth(); + return evaluate(be->left).add(evaluate(be->right), width); + } + case Expr::Sub: { + const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e); + unsigned width = be->left.getWidth(); + return evaluate(be->left).sub(evaluate(be->right), width); + } + case Expr::Mul: { + const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e); + unsigned width = be->left.getWidth(); + return evaluate(be->left).mul(evaluate(be->right), width); + } + case Expr::UDiv: { + const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e); + unsigned width = be->left.getWidth(); + return evaluate(be->left).udiv(evaluate(be->right), width); + } + case Expr::SDiv: { + const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e); + unsigned width = be->left.getWidth(); + return evaluate(be->left).sdiv(evaluate(be->right), width); + } + case Expr::URem: { + const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e); + unsigned width = be->left.getWidth(); + return evaluate(be->left).urem(evaluate(be->right), width); + } + case Expr::SRem: { + const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e); + unsigned width = be->left.getWidth(); + return evaluate(be->left).srem(evaluate(be->right), width); + } + + // Binary + + case Expr::And: { + const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e); + return evaluate(be->left).binaryAnd(evaluate(be->right)); + } + case Expr::Or: { + const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e); + return evaluate(be->left).binaryOr(evaluate(be->right)); + } + case Expr::Xor: { + const BinaryExpr *be = static_ref_cast<const BinaryExpr>(e); + return evaluate(be->left).binaryXor(evaluate(be->right)); + } + case Expr::Shl: { + // BinaryExpr *be = static_ref_cast<BinaryExpr>(e); + // unsigned width = be->left.getWidth(); + // return evaluate(be->left).shl(evaluate(be->right), width); + break; + } + case Expr::LShr: { + // BinaryExpr *be = static_ref_cast<BinaryExpr>(e); + // unsigned width = be->left.getWidth(); + // return evaluate(be->left).lshr(evaluate(be->right), width); + break; + } + case Expr::AShr: { + // BinaryExpr *be = static_ref_cast<BinaryExpr>(e); + // unsigned width = be->left.getWidth(); + // return evaluate(be->left).ashr(evaluate(be->right), width); + break; + } + + // Comparison + + case Expr::Eq: { + const BinaryExpr *be = static_ref_cast<const BinaryExpr>(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 = static_ref_cast<const BinaryExpr>(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 = static_ref_cast<const BinaryExpr>(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 = static_ref_cast<const BinaryExpr>(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 = static_ref_cast<const BinaryExpr>(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 diff --git a/include/klee/util/ExprUtil.h b/include/klee/util/ExprUtil.h new file mode 100644 index 00000000..a81c299f --- /dev/null +++ b/include/klee/util/ExprUtil.h @@ -0,0 +1,43 @@ +//===-- 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 <vector> + +namespace klee { + class Array; + class Expr; + class ReadExpr; + template<typename T> 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<Expr> e, + bool visitUpdates, + std::vector< ref<ReadExpr> > &result); + + /// Return a list of all unique symbolic objects referenced by the given + /// expression. + void findSymbolicObjects(ref<Expr> e, + std::vector<const Array*> &results); + + /// Return a list of all unique symbolic objects referenced by the + /// given expression range. + template<typename InputIterator> + void findSymbolicObjects(InputIterator begin, + InputIterator end, + std::vector<const Array*> &results); + +} + +#endif diff --git a/include/klee/util/ExprVisitor.h b/include/klee/util/ExprVisitor.h new file mode 100644 index 00000000..8f8617e3 --- /dev/null +++ b/include/klee/util/ExprVisitor.h @@ -0,0 +1,95 @@ +//===-- 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(0,Expr::Bool) {} + Action(Kind _kind, const ref<Expr> &_argument) + : kind(_kind), argument(_argument) {} + + friend class ExprVisitor; + + public: + Kind kind; + ref<Expr> argument; + + static Action changeTo(const ref<Expr> &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 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<Expr> > visited_ty; + visited_ty visited; + bool recursive; + + ref<Expr> visitActual(const ref<Expr> &e); + + public: + // apply the visitor to the expression and return a possibly + // modified new expression. + ref<Expr> visit(const ref<Expr> &e); + }; + +} + +#endif diff --git a/include/klee/util/Ref.h b/include/klee/util/Ref.h new file mode 100644 index 00000000..a70b09cf --- /dev/null +++ b/include/klee/util/Ref.h @@ -0,0 +1,303 @@ +//===-- Ref.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_REF_H +#define KLEE_REF_H + +#include <assert.h> + +class Expr; +class BinaryExpr; +class CastExpr; +class CmpExpr; + +class ConstantExpr; +class ReadExpr; +class UpdateNode; +class NotOptimizedExpr; +class ReadExpr; +class SelectExpr; +class ConcatExpr; +class ExtractExpr; +class ZExtExpr; +class SExtExpr; +class AddExpr; +class SubExpr; +class MulExpr; +class UDivExpr; +class SDivExpr; +class URemExpr; +class SRemExpr; +class AndExpr; +class OrExpr; +class XorExpr; +class ShlExpr; +class LShrExpr; +class AShrExpr; +class EqExpr; +class NeExpr; +class UltExpr; +class UleExpr; +class UgtExpr; +class UgeExpr; +class SltExpr; +class SleExpr; +class SgtExpr; +class SgeExpr; +class KModule; + + class ExprVisitor; + class StackFrame; + class ObjectState; + +template<class T> +class ref { +public: + // default constructor: create a NULL reference + ref() : constantWidth(Expr::InvalidWidth) { + contents.ptr = 0; + } + +private: + // if NotConstant, not this ref is not a constant. + // otherwise, it's the width of the constant. + Expr::Width constantWidth; + static const Expr::Width NotConstant = (Expr::Width) 0; + + union { + T *ptr; + uint64_t val; + } contents; + + void inc() { + if (constantWidth == NotConstant && + contents.ptr) { + contents.ptr->refCount++; + } + } + + void dec() { + if (constantWidth == NotConstant && + contents.ptr && + --contents.ptr->refCount == 0) { + delete contents.ptr; + } + } + + friend class ExprVisitor; + friend class Cell; + friend class ObjectState; + friend class KModule; + +public: + template<class U> friend class ref; + template<class U> friend U* dyn_ref_cast(ref &src); + template<class U> friend const U* dyn_ref_cast(const ref &src); + template<class U> friend U* static_ref_cast(ref &src); + template<class U> friend const U* static_ref_cast(const ref &src); + + // constructor from pointer + ref(T *p) : constantWidth(NotConstant) { + contents.ptr = p; + inc(); + } + + // construct from constant + ref(uint64_t val, Expr::Width w) : constantWidth(w) { + contents.val = val; + } + + // normal copy constructor + ref (const ref<T> &r) + : constantWidth(r.constantWidth), contents(r.contents) { + inc(); + } + + // conversion constructor + template<class U> + ref (const ref<U> &r) { + constantWidth = r.constantWidth; + contents.val = r.contents.val; + inc(); + } + + // pointer operations + T *get () { + // demand(constantWidth == NotConstant, "deref of constant"); + + // allocate + if (constantWidth != NotConstant) { + contents.ptr = dynamic_cast<T*>(Expr::createConstant(contents.val, constantWidth)); + assert(contents.ptr && "error with lazy constant initialization"); + constantWidth = NotConstant; + + inc(); + } + return contents.ptr; + } + + T *get () const { + assert(constantWidth == NotConstant && "deref of constant"); + return contents.ptr; + } + + // method calls for the constant optimization + bool isConstant() const { + if (constantWidth != NotConstant) { + return true; + } else if (contents.ptr) { + return contents.ptr->getKind() == Expr::Constant; + } else { + return false; // should never happen, but nice check + } + } + + uint64_t getConstantValue() const { + if (constantWidth) { + return contents.val; + } else { + return contents.ptr->getConstantValue(); + } + } + + unsigned hash() const { + if (constantWidth) { + return Expr::hashConstant(contents.val, constantWidth); + } else { + return contents.ptr->hash(); + } + } + + unsigned computeHash() const { + if (isConstant()) { + return Expr::hashConstant(contents.val, constantWidth); + } else { + return contents.ptr->computeHash(); + } + } + + void rehash() const { + if (!isConstant()) + contents.ptr->computeHash(); + } + + Expr::Width getWidth() const { + if (constantWidth != NotConstant) + return constantWidth; + return contents.ptr->getWidth(); + } + + Expr::Kind getKind() const { + if (constantWidth != NotConstant) + return Expr::Constant; + return contents.ptr->getKind(); + } + + unsigned getNumKids() const { + if (constantWidth != NotConstant) + return 0; + return contents.ptr->getNumKids(); + } + + ref<Expr> getKid(unsigned k) { + if (constantWidth != NotConstant) + return 0; + return contents.ptr->getKid(k); + } + + ~ref () { dec (); } + + /* The copy assignment operator must also explicitly be defined, + * despite a redundant template. */ + ref<T> &operator= (const ref<T> &r) { + dec(); + constantWidth = r.constantWidth; + contents.val = r.contents.val; + inc(); + + return *this; + } + + template<class U> ref<T> &operator= (const ref<U> &r) { + dec(); + constantWidth = r.constantWidth; + contents.val = r.contents.val; + inc(); + + return *this; + } + + bool isNull() const { return !constantWidth && !contents.ptr; } + + // assumes non-null arguments + int compare(const ref &rhs) const { + Expr::Kind ak = getKind(), bk = rhs.getKind(); + if (ak!=bk) + return (ak < bk) ? -1 : 1; + if (ak==Expr::Constant) { + Expr::Width at = getWidth(), bt = rhs.getWidth(); + if (at!=bt) + return (at < bt) ? -1 : 1; + uint64_t av = getConstantValue(), bv = rhs.getConstantValue(); + if (av<bv) { + return -1; + } else if (av>bv) { + return 1; + } else { + return 0; + } + } else { + return get()->compare(*rhs.get()); + } + } + + // assumes non-null arguments + bool operator<(const ref &rhs) const { return compare(rhs)<0; } + bool operator==(const ref &rhs) const { return compare(rhs)==0; } + bool operator!=(const ref &rhs) const { return compare(rhs)!=0; } +}; + + +template<class T> +inline std::ostream &operator<<(std::ostream &os, const ref<T> &e) { + if (e.isConstant()) { + os << e.getConstantValue(); + } else { + os << *e.get(); + } + return os; +} + +template<class U> +U* dyn_ref_cast(ref<Expr> &src) { + if (src.constantWidth != ref<Expr>::NotConstant) + return 0; + + return dynamic_cast<U*>(src.contents.ptr); +} + +template<class U> +const U* dyn_ref_cast(const ref<Expr> &src) { + if (src.constantWidth != ref<Expr>::NotConstant) + return 0; + + return dynamic_cast<const U*>(src.contents.ptr); +} + +template<class U> +U* static_ref_cast(ref<Expr> &src) { + return static_cast<U*>(src.contents.ptr); +} + +template<class U> +const U* static_ref_cast(const ref<Expr> &src) { + return static_cast<const U*>(src.contents.ptr); +} + +#endif /* KLEE_REF_H */ |