diff options
Diffstat (limited to 'include/klee/Expr/Parser')
| -rw-r--r-- | include/klee/Expr/Parser/Lexer.h | 121 | ||||
| -rw-r--r-- | include/klee/Expr/Parser/Parser.h | 237 |
2 files changed, 358 insertions, 0 deletions
diff --git a/include/klee/Expr/Parser/Lexer.h b/include/klee/Expr/Parser/Lexer.h new file mode 100644 index 00000000..14ae7f85 --- /dev/null +++ b/include/klee/Expr/Parser/Lexer.h @@ -0,0 +1,121 @@ +//===-- Lexer.h -------------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_LEXER_H +#define KLEE_LEXER_H + +#include <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/klee/Expr/Parser/Parser.h b/include/klee/Expr/Parser/Parser.h new file mode 100644 index 00000000..c1888e26 --- /dev/null +++ b/include/klee/Expr/Parser/Parser.h @@ -0,0 +1,237 @@ +//===-- Parser.h ------------------------------------------------*- C++ -*-===// +// +// The KLEE Symbolic Virtual Machine +// +// This file is distributed under the University of Illinois Open Source +// License. See LICENSE.TXT for details. +// +//===----------------------------------------------------------------------===// + +#ifndef KLEE_PARSER_H +#define KLEE_PARSER_H + +#include "klee/Expr/Expr.h" + +#include <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 */ |