klee
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros Pages
Parser.h
Go to the documentation of this file.
1 //===-- Parser.h ------------------------------------------------*- C++ -*-===//
2 //
3 // The KLEE Symbolic Virtual Machine
4 //
5 // This file is distributed under the University of Illinois Open Source
6 // License. See LICENSE.TXT for details.
7 //
8 //===----------------------------------------------------------------------===//
9 
10 #ifndef KLEE_EXPR_PARSER_H
11 #define KLEE_EXPR_PARSER_H
12 
13 #include "klee/Expr.h"
14 
15 #include <vector>
16 #include <string>
17 
18 namespace llvm {
19  class MemoryBuffer;
20 }
21 
22 namespace klee {
23  class ExprBuilder;
24 
25 namespace expr {
26  // These are the language types we manipulate.
29 
31  struct Identifier {
32  const std::string Name;
33 
34  public:
35  Identifier(const std::string _Name) : Name(_Name) {}
36  };
37 
38  // FIXME: Do we have a use for tracking source locations?
39 
41  class Decl {
42  public:
43  enum DeclKind {
48 
54  };
55 
56  private:
58 
59  public:
60  Decl(DeclKind _Kind);
61  virtual ~Decl() {}
62 
64  DeclKind getKind() const { return Kind; }
65 
67  virtual void dump() = 0;
68 
69  static bool classof(const Decl *) { return true; }
70  };
71 
77  class ArrayDecl : public Decl {
78  public:
80  const Identifier *Name;
81 
83  const unsigned Domain;
84 
86  const unsigned Range;
87 
89  const Array *Root;
90 
91  public:
92  ArrayDecl(const Identifier *_Name, uint64_t _Size,
93  unsigned _Domain, unsigned _Range,
94  const Array *_Root)
95  : Decl(ArrayDeclKind), Name(_Name),
96  Domain(_Domain), Range(_Range),
97  Root(_Root) {
98  }
99 
100  virtual void dump();
101 
102  static bool classof(const Decl *D) {
103  return D->getKind() == Decl::ArrayDeclKind;
104  }
105  static bool classof(const ArrayDecl *) { return true; }
106  };
107 
112  // FIXME: What syntax are we going to use for this? We need it.
113  class VarDecl : public Decl {
114  public:
115  const Identifier *Name;
116 
117  static bool classof(const Decl *D) {
118  return (Decl::VarDeclKindFirst <= D->getKind() &&
120  }
121  static bool classof(const VarDecl *) { return true; }
122  };
123 
125  class ExprVarDecl : public VarDecl {
126  public:
128 
129  static bool classof(const Decl *D) {
130  return D->getKind() == Decl::ExprVarDeclKind;
131  }
132  static bool classof(const ExprVarDecl *) { return true; }
133  };
134 
136  class VersionVarDecl : public VarDecl {
137  public:
139 
140  static bool classof(const Decl *D) {
141  return D->getKind() == Decl::VersionVarDeclKind;
142  }
143  static bool classof(const VersionVarDecl *) { return true; }
144  };
145 
147  class CommandDecl : public Decl {
148  public:
149  CommandDecl(DeclKind _Kind) : Decl(_Kind) {}
150 
151  static bool classof(const Decl *D) {
152  return (Decl::CommandDeclKindFirst <= D->getKind() &&
154  }
155  static bool classof(const CommandDecl *) { return true; }
156  };
157 
163  class QueryCommand : public CommandDecl {
164  public:
165  // FIXME: One issue with STP... should we require the FE to
166  // guarantee that these are consistent? That is a cornerstone of
167  // being able to do independence. We may want this as a flag, if
168  // we are to interface with things like SMT.
169 
172  const std::vector<ExprHandle> Constraints;
173 
176 
179  const std::vector<ExprHandle> Values;
180 
183  const std::vector<const Array*> Objects;
184 
185  public:
186  QueryCommand(const std::vector<ExprHandle> &_Constraints,
187  ExprHandle _Query,
188  const std::vector<ExprHandle> &_Values,
189  const std::vector<const Array*> &_Objects
190  )
192  Constraints(_Constraints),
193  Query(_Query),
194  Values(_Values),
195  Objects(_Objects) {}
196 
197  virtual void dump();
198 
199  static bool classof(const Decl *D) {
200  return D->getKind() == QueryCommandDeclKind;
201  }
202  static bool classof(const QueryCommand *) { return true; }
203  };
204 
206  class Parser {
207  protected:
208  Parser();
209  public:
210  virtual ~Parser();
211 
213  virtual void SetMaxErrors(unsigned N) = 0;
214 
216  virtual unsigned GetNumErrors() const = 0;
217 
222  virtual Decl *ParseTopLevelDecl() = 0;
223 
231  static Parser *Create(const std::string Name,
232  const llvm::MemoryBuffer *MB,
233  ExprBuilder *Builder);
234  };
235 }
236 }
237 
238 #endif
const unsigned Domain
Domain - The width of indices.
Definition: Parser.h:83
CommandDecl(DeclKind _Kind)
Definition: Parser.h:149
ExprHandle Value
Definition: Parser.h:127
VersionVarDecl - Array version variable declarations.
Definition: Parser.h:136
const Identifier * Name
Name - The name of this array.
Definition: Parser.h:80
static bool classof(const VarDecl *)
Definition: Parser.h:121
const std::vector< const Array * > Objects
Definition: Parser.h:183
CommandDecl - Base class for language commands.
Definition: Parser.h:147
static bool classof(const Decl *D)
Definition: Parser.h:102
const std::vector< ExprHandle > Constraints
Definition: Parser.h:172
ExprBuilder - Base expression builder class.
Definition: ExprBuilder.h:17
static bool classof(const Decl *D)
Definition: Parser.h:140
Identifier(const std::string _Name)
Definition: Parser.h:35
static bool classof(const ArrayDecl *)
Definition: Parser.h:105
const unsigned Range
Range - The width of array contents.
Definition: Parser.h:86
Class representing a complete list of updates into an array.
Definition: Expr.h:655
QueryCommand(const std::vector< ExprHandle > &_Constraints, ExprHandle _Query, const std::vector< ExprHandle > &_Values, const std::vector< const Array * > &_Objects)
Definition: Parser.h:186
const Array * Root
Root - The root array object defined by this decl.
Definition: Parser.h:89
virtual void dump()
dump - Dump the AST node to stderr.
Definition: Parser.cpp:1583
DeclKind Kind
Definition: Parser.h:57
static bool classof(const Decl *D)
Definition: Parser.h:199
ExprHandle Query
Query - The expression being queried.
Definition: Parser.h:175
ArrayDecl(const Identifier *_Name, uint64_t _Size, unsigned _Domain, unsigned _Range, const Array *_Root)
Definition: Parser.h:92
const std::string Name
Definition: Parser.h:32
Decl - Base class for top level declarations.
Definition: Parser.h:41
UpdateList VersionHandle
Definition: Parser.h:28
static Parser * Create(const std::string Name, const llvm::MemoryBuffer *MB, ExprBuilder *Builder)
Definition: Parser.cpp:1608
virtual ~Parser()
Definition: Parser.cpp:1605
virtual void dump()=0
dump - Dump the AST node to stderr.
static bool classof(const Decl *D)
Definition: Parser.h:117
static bool classof(const ExprVarDecl *)
Definition: Parser.h:132
ref< Expr > ExprHandle
Definition: Parser.h:27
VersionHandle Value
Definition: Parser.h:138
virtual void SetMaxErrors(unsigned N)=0
SetMaxErrors - Suppress anything beyond the first N errors.
Identifier - Wrapper for a uniqued string.
Definition: Parser.h:31
virtual void dump()
dump - Dump the AST node to stderr.
Definition: Parser.cpp:1565
virtual unsigned GetNumErrors() const =0
GetNumErrors - Return the number of encountered errors.
static bool classof(const Decl *D)
Definition: Parser.h:151
Decl(DeclKind _Kind)
Definition: Parser.cpp:1563
DeclKind getKind() const
getKind - Get the decl kind.
Definition: Parser.h:64
ExprVarDecl - Expression variable declarations.
Definition: Parser.h:125
static bool classof(const Decl *D)
Definition: Parser.h:129
Parser - Public interface for parsing a .pc language file.
Definition: Parser.h:206
static bool classof(const VersionVarDecl *)
Definition: Parser.h:143
static bool classof(const Decl *)
Definition: Parser.h:69
virtual ~Decl()
Definition: Parser.h:61
static bool classof(const CommandDecl *)
Definition: Parser.h:155
static bool classof(const QueryCommand *)
Definition: Parser.h:202
virtual Decl * ParseTopLevelDecl()=0
const std::vector< ExprHandle > Values
Definition: Parser.h:179
const Identifier * Name
Definition: Parser.h:115