Parser.h

Go to the documentation of this file.

//===-- 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;
  
  struct Identifier {
    const std::string Name;
 
  public:
    Identifier(const std::string _Name) : Name(_Name) {}
  };
 
  // FIXME: Do we have a use for tracking source locations?
 
  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() {}
 
    DeclKind getKind() const { return Kind; }
 
    virtual void dump() = 0;
 
    static bool classof(const Decl *) { return true; }
  };
 
  class ArrayDecl : public Decl {
  public:
    const Identifier *Name;
 
    const unsigned Domain;
 
    const unsigned Range;
 
    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; }
  };
 
  // 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; }
  };
 
  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; }
  };
 
  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; }
  };
 
  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; }
  };
 
  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.
 
    const std::vector<ExprHandle> Constraints;
    
    ExprHandle Query;
 
    const std::vector<ExprHandle> Values;
 
    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; }
  };
  
  class Parser {
  protected:
    Parser();
  public:
    virtual ~Parser();
 
    virtual void SetMaxErrors(unsigned N) = 0;
    
    virtual unsigned GetNumErrors() const = 0;
 
    virtual Decl *ParseTopLevelDecl() = 0;
 
    static Parser *Create(const std::string Name, const llvm::MemoryBuffer *MB,
                          ExprBuilder *Builder, bool ClearArrayAfterQuery);
  };
}
}
 
#endif /* KLEE_PARSER_H */