diff options
Diffstat (limited to 'include/expr')
| -rw-r--r-- | include/expr/Lexer.h | 121 | ||||
| -rw-r--r-- | include/expr/Parser.h | 237 |
2 files changed, 0 insertions, 358 deletions
diff --git a/include/expr/Lexer.h b/include/expr/Lexer.h deleted file mode 100644 index 14ae7f85..00000000 --- a/include/expr/Lexer.h +++ /dev/null @@ -1,121 +0,0 @@ -//===-- Lexer.h -------------------------------------------------*- C++ -*-===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#ifndef KLEE_LEXER_H -#define KLEE_LEXER_H - -#include <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._]* - KWArray, ///< 'array' - KWFalse, ///< 'false' - KWQuery, ///< 'query' - KWReserved, ///< fp[0-9]+([.].*)?, i[0-9]+ - KWSymbolic, ///< 'symbolic' - KWTrue, ///< 'true' - KWWidth, ///< w[0-9]+ - LBrace, ///< '{' - LParen, ///< '(' - LSquare, ///< '[' - Number, ///< [+-]?[0-9][a-zA-Z0-9_]+ - RBrace, ///< '}' - RParen, ///< ')' - RSquare, ///< ']' - Semicolon, ///< ';' - Unknown, ///< <other> - - KWKindFirst=KWArray, - KWKindLast=KWWidth - }; - - Kind kind; /// The token kind. - const char *start; /// The beginning of the token string. - unsigned length; /// The length of the token. - unsigned line; /// The line number of the start of this token. - unsigned column; /// The column number at the start of - /// this token. - - /// getKindName - The name of this token's kind. - const char *getKindName() const; - - /// getString - The string spanned by this token. This is not - /// particularly efficient, use start and length when reasonable. - std::string getString() const { return std::string(start, length); } - - /// isKeyword - True if this token is a keyword. - bool isKeyword() const { - return kind >= KWKindFirst && kind <= KWKindLast; - } - - // dump - Dump the token to stderr. - void dump(); - - Token() : kind(Unknown), start(nullptr) {} - }; - - /// Lexer - Interface for lexing tokens from a .kquery language file. - class Lexer { - const char *BufferPos; /// The current lexer position. - const char *BufferEnd; /// The buffer end position. - unsigned LineNumber; /// The current line. - unsigned ColumnNumber; /// The current column. - - /// GetNextChar - Eat a character or -1 from the stream. - int GetNextChar(); - - /// PeekNextChar - Return the next character without consuming it - /// from the stream. This does not perform newline - /// canonicalization. - int PeekNextChar(); - - /// SetTokenKind - Set the token kind and length (using the - /// token's start pointer, which must have been initialized). - Token &SetTokenKind(Token &Result, Token::Kind k); - - /// SetTokenKind - Set an identifiers token kind. This has the - /// same requirements as SetTokenKind and additionally takes care - /// of keyword recognition. - Token &SetIdentifierTokenKind(Token &Result); - - void SkipToEndOfLine(); - - /// LexNumber - Lex a number which does not have a base specifier. - Token &LexNumber(Token &Result); - - /// LexIdentifier - Lex an identifier. - Token &LexIdentifier(Token &Result); - - public: - explicit Lexer(const llvm::MemoryBuffer *_buf); - ~Lexer(); - - /// Lex - Return the next token from the file or EOF continually - /// when the end of the file is reached. The input argument is - /// used as the result, for convenience. - Token &Lex(Token &Result); - }; -} -} - -#endif /* KLEE_LEXER_H */ diff --git a/include/expr/Parser.h b/include/expr/Parser.h deleted file mode 100644 index 6a34b8d0..00000000 --- a/include/expr/Parser.h +++ /dev/null @@ -1,237 +0,0 @@ -//===-- Parser.h ------------------------------------------------*- C++ -*-===// -// -// The KLEE Symbolic Virtual Machine -// -// This file is distributed under the University of Illinois Open Source -// License. See LICENSE.TXT for details. -// -//===----------------------------------------------------------------------===// - -#ifndef KLEE_PARSER_H -#define KLEE_PARSER_H - -#include "klee/Expr.h" - -#include <vector> -#include <string> - -namespace llvm { - class MemoryBuffer; -} - -namespace klee { - class ExprBuilder; - -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: - enum DeclKind { - ArrayDeclKind, - ExprVarDeclKind, - VersionVarDeclKind, - QueryCommandDeclKind, - - DeclKindLast = QueryCommandDeclKind, - VarDeclKindFirst = ExprVarDeclKind, - VarDeclKindLast = VersionVarDeclKind, - CommandDeclKindFirst = QueryCommandDeclKind, - CommandDeclKindLast = QueryCommandDeclKind - }; - - private: - DeclKind Kind; - - public: - Decl(DeclKind _Kind); - virtual ~Decl() {} - - /// getKind - Get the decl kind. - DeclKind getKind() const { return Kind; } - - /// dump - Dump the AST node to stderr. - virtual void dump() = 0; - - static bool classof(const Decl *) { return true; } - }; - - /// ArrayDecl - Array declarations. - /// - /// For example: - /// array obj[] : w32 -> w8 = symbolic - /// array obj[32] : w32 -> w8 = [ ... ] - class ArrayDecl : public Decl { - public: - /// Name - The name of this array. - const Identifier *Name; - - /// Domain - The width of indices. - const unsigned Domain; - - /// Range - The width of array contents. - const unsigned Range; - - /// Root - The root array object defined by this decl. - const Array *Root; - - public: - ArrayDecl(const Identifier *_Name, uint64_t _Size, - unsigned _Domain, unsigned _Range, - const Array *_Root) - : Decl(ArrayDeclKind), Name(_Name), - Domain(_Domain), Range(_Range), - Root(_Root) { - } - - virtual void dump(); - - static bool classof(const Decl *D) { - return D->getKind() == Decl::ArrayDeclKind; - } - static bool classof(const ArrayDecl *) { return true; } - }; - - /// VarDecl - Variable declarations, used to associate names to - /// expressions or array versions outside of expressions. - /// - /// For example: - // FIXME: What syntax are we going to use for this? We need it. - class VarDecl : public Decl { - public: - const Identifier *Name; - - static bool classof(const Decl *D) { - return (Decl::VarDeclKindFirst <= D->getKind() && - D->getKind() <= Decl::VarDeclKindLast); - } - static bool classof(const VarDecl *) { return true; } - }; - - /// ExprVarDecl - Expression variable declarations. - class ExprVarDecl : public VarDecl { - public: - ExprHandle Value; - - static bool classof(const Decl *D) { - return D->getKind() == Decl::ExprVarDeclKind; - } - static bool classof(const ExprVarDecl *) { return true; } - }; - - /// VersionVarDecl - Array version variable declarations. - class VersionVarDecl : public VarDecl { - public: - VersionHandle Value; - - static bool classof(const Decl *D) { - return D->getKind() == Decl::VersionVarDeclKind; - } - static bool classof(const VersionVarDecl *) { return true; } - }; - - /// CommandDecl - Base class for language commands. - class CommandDecl : public Decl { - public: - CommandDecl(DeclKind _Kind) : Decl(_Kind) {} - - static bool classof(const Decl *D) { - return (Decl::CommandDeclKindFirst <= D->getKind() && - D->getKind() <= Decl::CommandDeclKindLast); - } - static bool classof(const CommandDecl *) { return true; } - }; - - /// QueryCommand - Query commands. - /// - /// (query [ ... constraints ... ] expression) - /// (query [ ... constraints ... ] expression values) - /// (query [ ... constraints ... ] expression values objects) - class QueryCommand : public CommandDecl { - public: - // FIXME: One issue with STP... should we require the FE to - // guarantee that these are consistent? That is a cornerstone of - // being able to do independence. We may want this as a flag, if - // we are to interface with things like SMT. - - /// Constraints - The list of constraints to assume for this - /// expression. - const std::vector<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<const Array*> Objects; - - public: - QueryCommand(const std::vector<ExprHandle> &_Constraints, - ExprHandle _Query, - const std::vector<ExprHandle> &_Values, - const std::vector<const Array*> &_Objects - ) - : CommandDecl(QueryCommandDeclKind), - Constraints(_Constraints), - Query(_Query), - Values(_Values), - Objects(_Objects) {} - - virtual void dump(); - - static bool classof(const Decl *D) { - return D->getKind() == QueryCommandDeclKind; - } - static bool classof(const QueryCommand *) { return true; } - }; - - /// Parser - Public interface for parsing a .kquery language file. - class Parser { - protected: - Parser(); - public: - virtual ~Parser(); - - /// SetMaxErrors - Suppress anything beyond the first N errors. - virtual void SetMaxErrors(unsigned N) = 0; - - /// GetNumErrors - Return the number of encountered errors. - virtual unsigned GetNumErrors() const = 0; - - /// ParseTopLevelDecl - Parse and return a top level declaration, - /// which the caller assumes ownership of. - /// - /// \return NULL indicates the end of the file has been reached. - virtual Decl *ParseTopLevelDecl() = 0; - - /// CreateParser - Create a parser implementation for the given - /// MemoryBuffer. - /// - /// \arg Name - The name to use in diagnostic messages. - /// \arg MB - The input data. - /// \arg Builder - The expression builder to use for constructing - /// expressions. - static Parser *Create(const std::string Name, const llvm::MemoryBuffer *MB, - ExprBuilder *Builder, bool ClearArrayAfterQuery); - }; -} -} - -#endif /* KLEE_PARSER_H */ |