klee
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_PARSER_H
11#define KLEE_PARSER_H
12
13#include "klee/Expr/Expr.h"
14
15#include <vector>
16#include <string>
17
18namespace llvm {
19 class MemoryBuffer;
20}
21
22namespace klee {
23 class ExprBuilder;
24
25namespace 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:
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:
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, const llvm::MemoryBuffer *MB,
232 ExprBuilder *Builder, bool ClearArrayAfterQuery);
233 };
234}
235}
236
237#endif /* KLEE_PARSER_H */
ExprBuilder - Base expression builder class.
Definition: ExprBuilder.h:17
Class representing a complete list of updates into an array.
Definition: Expr.h:539
ArrayDecl(const Identifier *_Name, uint64_t _Size, unsigned _Domain, unsigned _Range, const Array *_Root)
Definition: Parser.h:92
const Identifier * Name
Name - The name of this array.
Definition: Parser.h:80
static bool classof(const ArrayDecl *)
Definition: Parser.h:105
const Array * Root
Root - The root array object defined by this decl.
Definition: Parser.h:89
const unsigned Domain
Domain - The width of indices.
Definition: Parser.h:83
const unsigned Range
Range - The width of array contents.
Definition: Parser.h:86
static bool classof(const Decl *D)
Definition: Parser.h:102
virtual void dump()
dump - Dump the AST node to stderr.
Definition: Parser.cpp:1606
CommandDecl - Base class for language commands.
Definition: Parser.h:147
static bool classof(const Decl *D)
Definition: Parser.h:151
CommandDecl(DeclKind _Kind)
Definition: Parser.h:149
static bool classof(const CommandDecl *)
Definition: Parser.h:155
Decl - Base class for top level declarations.
Definition: Parser.h:41
virtual ~Decl()
Definition: Parser.h:61
@ QueryCommandDeclKind
Definition: Parser.h:47
@ CommandDeclKindFirst
Definition: Parser.h:52
@ VersionVarDeclKind
Definition: Parser.h:46
@ VarDeclKindFirst
Definition: Parser.h:50
@ CommandDeclKindLast
Definition: Parser.h:53
Decl(DeclKind _Kind)
Definition: Parser.cpp:1604
DeclKind Kind
Definition: Parser.h:57
static bool classof(const Decl *)
Definition: Parser.h:69
DeclKind getKind() const
getKind - Get the decl kind.
Definition: Parser.h:64
virtual void dump()=0
dump - Dump the AST node to stderr.
ExprVarDecl - Expression variable declarations.
Definition: Parser.h:125
static bool classof(const ExprVarDecl *)
Definition: Parser.h:132
ExprHandle Value
Definition: Parser.h:127
static bool classof(const Decl *D)
Definition: Parser.h:129
Parser - Public interface for parsing a .kquery language file.
Definition: Parser.h:206
virtual ~Parser()
Definition: Parser.cpp:1645
static Parser * Create(const std::string Name, const llvm::MemoryBuffer *MB, ExprBuilder *Builder, bool ClearArrayAfterQuery)
Definition: Parser.cpp:1648
virtual unsigned GetNumErrors() const =0
GetNumErrors - Return the number of encountered errors.
virtual void SetMaxErrors(unsigned N)=0
SetMaxErrors - Suppress anything beyond the first N errors.
virtual Decl * ParseTopLevelDecl()=0
const std::vector< const Array * > Objects
Definition: Parser.h:183
virtual void dump()
dump - Dump the AST node to stderr.
Definition: Parser.cpp:1624
const std::vector< ExprHandle > Constraints
Definition: Parser.h:172
static bool classof(const QueryCommand *)
Definition: Parser.h:202
static bool classof(const Decl *D)
Definition: Parser.h:199
ExprHandle Query
Query - The expression being queried.
Definition: Parser.h:175
QueryCommand(const std::vector< ExprHandle > &_Constraints, ExprHandle _Query, const std::vector< ExprHandle > &_Values, const std::vector< const Array * > &_Objects)
Definition: Parser.h:186
const std::vector< ExprHandle > Values
Definition: Parser.h:179
static bool classof(const Decl *D)
Definition: Parser.h:117
static bool classof(const VarDecl *)
Definition: Parser.h:121
const Identifier * Name
Definition: Parser.h:115
VersionVarDecl - Array version variable declarations.
Definition: Parser.h:136
VersionHandle Value
Definition: Parser.h:138
static bool classof(const Decl *D)
Definition: Parser.h:140
static bool classof(const VersionVarDecl *)
Definition: Parser.h:143
UpdateList VersionHandle
Definition: Parser.h:28
ref< Expr > ExprHandle
Definition: Parser.h:27
Definition: main.cpp:291
Identifier - Wrapper for a uniqued string.
Definition: Parser.h:31
const std::string Name
Definition: Parser.h:32
Identifier(const std::string _Name)
Definition: Parser.h:35