Initial KLEE checkin.

 - Lots more tweaks, documentation, and web page content is needed,
   but this should compile & work on OS X & Linux.


git-svn-id: https://llvm.org/svn/llvm-project/klee/trunk@72205 91177308-0d34-0410-b5e6-96231b3b80d8

2 files changed, 292 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