diff options
Diffstat (limited to 'include/expr')
| -rw-r--r-- | include/expr/Lexer.h | 114 | ||||
| -rw-r--r-- | include/expr/Parser.h | 178 |
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 |