about summary refs log tree commit diff homepage
path: root/include/expr/Parser.h
diff options
context:
space:
mode:
Diffstat (limited to 'include/expr/Parser.h')
-rw-r--r--include/expr/Parser.h237
1 files changed, 0 insertions, 237 deletions
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 */