1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
|
//===-- 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_EXPR_PARSER_H
#define KLEE_EXPR_PARSER_H
#include "klee/Expr.h"
#include <vector>
#include <string>
namespace llvm {
class MemoryBuffer;
}
namespace klee {
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:
Decl();
virtual ~Decl() {}
/// dump - Dump the AST node to stderr.
virtual void dump() = 0;
};
/// ArrayDecl - Array declarations.
///
/// For example:
/// array obj : 32 -> 8 = symbolic
/// array obj[32] : 32 -> 8 = { ... }
class ArrayDecl : public Decl {
public:
/// Name - The name of this array.
const Identifier *Name;
/// Size - The maximum array size (or 0 if unspecified). Concrete
/// arrays always are specified with a size.
const unsigned Size;
/// Domain - The width of indices.
const unsigned Domain;
/// Range - The width of array contents.
const unsigned Range;
/// Contents - The initial contents of the array. The array is
/// symbolic if no contents are specified. The contained
/// expressions are guaranteed to be constants.
const std::vector<ExprHandle> Contents;
public:
template<typename InputIterator>
ArrayDecl(const Identifier *_Name, unsigned _Size,
unsigned _Domain, unsigned _Range,
InputIterator ContentsBegin=InputIterator(),
InputIterator ContentsEnd=InputIterator())
: Name(_Name), Size(_Size), Domain(_Domain), Range(_Range),
Contents(ContentsBegin, ContentsEnd) {}
};
/// 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;
};
/// ExprVarDecl - Expression variable declarations.
class ExprVarDecl : public VarDecl {
public:
ExprHandle Value;
};
/// VersionVarDecl - Array version variable declarations.
class VersionVarDecl : public VarDecl {
public:
VersionHandle Value;
};
/// CommandDecl - Base class for language commands.
class CommandDecl : public Decl {
public:
const Identifier *Name;
};
/// 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<ArrayDecl> Objects;
public:
template<typename InputIterator>
QueryCommand(InputIterator ConstraintsBegin,
InputIterator ConstraintsEnd,
ExprHandle _Query)
: Constraints(ConstraintsBegin, ConstraintsEnd),
Query(_Query) {}
virtual void dump();
};
/// Parser - Public interface for parsing a .pc 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.
static Parser *Create(const std::string Name,
const llvm::MemoryBuffer *MB);
};
}
}
#endif
|
