1 /********************* */
2 /*! \file antlr_input.h
4 ** Original author: cconway
5 ** Major contributors: none
6 ** Minor contributors (to current version): mdeters, dejan
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief Base for ANTLR parser classes.
16 ** Base for ANTLR parser classes.
19 #include "cvc4parser_private.h"
21 #ifndef __CVC4__PARSER__ANTLR_INPUT_H
22 #define __CVC4__PARSER__ANTLR_INPUT_H
31 #include "bounded_token_buffer.h"
32 #include "parser_exception.h"
35 #include "util/Assert.h"
36 #include "util/bitvector.h"
37 #include "util/integer.h"
38 #include "util/rational.h"
48 /** Wrapper around an ANTLR3 input stream. */
49 class AntlrInputStream
: public InputStream
{
50 pANTLR3_INPUT_STREAM d_input
;
52 AntlrInputStream(std::string name
,
53 pANTLR3_INPUT_STREAM input
,
54 bool fileIsTemporary
= false);
56 /* This is private and unimplemented, because you should never use it. */
57 AntlrInputStream(const AntlrInputStream
& inputStream
);
59 /* This is private and unimplemented, because you should never use it. */
60 AntlrInputStream
& operator=(const AntlrInputStream
& inputStream
);
64 virtual ~AntlrInputStream();
66 pANTLR3_INPUT_STREAM
getAntlr3InputStream() const;
68 /** Create a file input.
70 * @param name the path of the file to read
71 * @param useMmap <code>true</code> if the input should use memory-mapped I/O; otherwise, the
72 * input will use the standard ANTLR3 I/O implementation.
74 static AntlrInputStream
* newFileInputStream(const std::string
& name
,
76 throw (InputStreamException
, AssertionException
);
78 /** Create an input from an istream. */
79 static AntlrInputStream
* newStreamInputStream(std::istream
& input
,
80 const std::string
& name
)
81 throw (InputStreamException
, AssertionException
);
83 /** Create a string input.
85 * @param input the string to read
86 * @param name the "filename" to use when reporting errors
88 static AntlrInputStream
* newStringInputStream(const std::string
& input
,
89 const std::string
& name
)
90 throw (InputStreamException
, AssertionException
);
96 * An input to be parsed. The static factory methods in this class (e.g.,
97 * <code>newFileInput</code>, <code>newStringInput</code>) create a parser
98 * for the given input language and attach it to an input source of the
101 class AntlrInput
: public Input
{
102 /** The token lookahead used to lex and parse the input. This should usually be equal to
103 * <code>K</code> for an LL(k) grammar. */
104 unsigned int d_lookahead
;
106 /** The ANTLR3 lexer associated with this input. This will be <code>NULL</code> initially. It
107 * must be set by a call to <code>setLexer</code>, preferably in the subclass constructor. */
108 pANTLR3_LEXER d_lexer
;
110 /** The ANTLR3 parser associated with this input. This will be <code>NULL</code> initially. It
111 * must be set by a call to <code>setParser</code>, preferably in the subclass constructor.
112 * The <code>super</code> field of <code>d_parser</code> will be set to <code>this</code> and
113 * <code>reportError</code> will be set to <code>Input::reportError</code>. */
114 pANTLR3_PARSER d_parser
;
116 /** The ANTLR3 input stream associated with this input. */
117 pANTLR3_INPUT_STREAM d_antlr3InputStream
;
119 /** The ANTLR3 bounded token buffer associated with this input.
120 * We only need this so we can free it on exit.
121 * This is set by <code>setLexer</code>.
122 * NOTE: We assume that we <em>can</em> free it on exit. No sharing! */
123 pBOUNDED_TOKEN_BUFFER d_tokenBuffer
;
125 /** Turns an ANTLR3 exception into a message for the user and calls <code>parseError</code>. */
126 static void reportError(pANTLR3_BASE_RECOGNIZER recognizer
);
128 /** Builds a message for a lexer error and calls <code>parseError</code>. */
129 static void lexerError(pANTLR3_BASE_RECOGNIZER recognizer
);
131 /** Returns the next available lexer token from the current input stream. */
132 static pANTLR3_COMMON_TOKEN
133 nextTokenStr (pANTLR3_TOKEN_SOURCE toksource
);
135 /* Since we own d_tokenStream and it needs to be freed, we need to prevent
136 * copy construction and assignment.
138 AntlrInput(const AntlrInput
& input
);
139 AntlrInput
& operator=(const AntlrInput
& input
);
143 /** Destructor. Frees the token stream and closes the input. */
144 virtual ~AntlrInput();
146 /** Create an input for the given AntlrInputStream. NOTE: the new Input
147 * will take ownership of the input stream and delete it at destruction time.
149 * @param lang the input language
150 * @param inputStream the input stream
153 static AntlrInput
* newInput(InputLanguage lang
, AntlrInputStream
& inputStream
);
155 /** Retrieve the text associated with a token. */
156 static std::string
tokenText(pANTLR3_COMMON_TOKEN token
);
158 /** Retrieve a substring of the text associated with a token.
160 * @param token the token
161 * @param index the index of the starting character of the substring
162 * @param n the size of the substring. If <code>n</code> is 0, then all of the
163 * characters up to the end of the token text will be included. If <code>n</code>
164 * would make the substring span past the end of the token text, only those
165 * characters up to the end of the token text will be included.
167 static std::string
tokenTextSubstr(pANTLR3_COMMON_TOKEN token
, size_t index
, size_t n
= 0);
169 /** Retrieve an unsigned from the text of a token */
170 static unsigned tokenToUnsigned( pANTLR3_COMMON_TOKEN token
);
172 /** Retrieve an Integer from the text of a token */
173 static Integer
tokenToInteger( pANTLR3_COMMON_TOKEN token
);
175 /** Retrieve a Rational from the text of a token */
176 static Rational
tokenToRational(pANTLR3_COMMON_TOKEN token
);
178 /** Get a bitvector constant from the text of the number and the size token */
179 static BitVector
tokenToBitvector(pANTLR3_COMMON_TOKEN number
, pANTLR3_COMMON_TOKEN size
);
181 std::string
getUnparsedText();
184 /** Create an input. This input takes ownership of the given input stream,
185 * and will delete it at destruction time.
187 * @param inputStream the input stream to use
188 * @param lookahead the lookahead needed to parse the input (i.e., k for
191 AntlrInput(AntlrInputStream
& inputStream
, unsigned int lookahead
);
193 /** Retrieve the token stream for this parser. Must not be called before
194 * <code>setLexer()</code>. */
195 pANTLR3_COMMON_TOKEN_STREAM
getTokenStream();
198 * Throws a <code>ParserException</code> with the given message.
200 void parseError(const std::string
& msg
)
201 throw (ParserException
, AssertionException
);
203 /** Set the ANTLR3 lexer for this input. */
204 void setAntlr3Lexer(pANTLR3_LEXER pLexer
);
206 /** Set the ANTLR3 parser implementation for this input. */
207 void setAntlr3Parser(pANTLR3_PARSER pParser
);
209 /** Set the Parser object for this input. */
210 virtual void setParser(Parser
& parser
);
213 inline std::string
AntlrInput::getUnparsedText() {
214 const char *base
= (const char *)d_antlr3InputStream
->data
;
215 const char *cur
= (const char *)d_antlr3InputStream
->nextChar
;
217 return std::string(cur
, d_antlr3InputStream
->sizeBuf
- (cur
- base
));
221 inline std::string
AntlrInput::tokenText(pANTLR3_COMMON_TOKEN token
) {
222 if( token
->type
== ANTLR3_TOKEN_EOF
) {
226 ANTLR3_MARKER start
= token
->getStartIndex(token
);
227 ANTLR3_MARKER end
= token
->getStopIndex(token
);
228 /* start and end are boundary pointers. The text is a string
229 * of (end-start+1) bytes beginning at start. */
230 std::string
txt( (const char *)start
, end
-start
+1 );
231 Debug("parser-extra") << "tokenText: start=" << start
<< std::endl
232 << "end=" << end
<< std::endl
233 << "txt='" << txt
<< "'" << std::endl
;
237 inline std::string
AntlrInput::tokenTextSubstr(pANTLR3_COMMON_TOKEN token
,
240 ANTLR3_MARKER start
= token
->getStartIndex(token
);
241 ANTLR3_MARKER end
= token
->getStopIndex(token
);
242 Assert( start
< end
);
243 if( index
> (size_t) end
- start
) {
244 std::stringstream ss
;
245 ss
<< "Out-of-bounds substring index: " << index
;
246 throw std::invalid_argument(ss
.str());
249 if( n
==0 || n
>= (size_t) end
- start
) {
250 return std::string( (const char *)start
, end
-start
+1 );
252 return std::string( (const char *)start
, n
);
256 inline unsigned AntlrInput::tokenToUnsigned(pANTLR3_COMMON_TOKEN token
) {
258 std::stringstream ss
;
259 ss
<< tokenText(token
);
264 inline Integer
AntlrInput::tokenToInteger(pANTLR3_COMMON_TOKEN token
) {
265 return Integer( tokenText(token
) );
268 inline Rational
AntlrInput::tokenToRational(pANTLR3_COMMON_TOKEN token
) {
269 return Rational::fromDecimal( tokenText(token
) );
272 inline BitVector
AntlrInput::tokenToBitvector(pANTLR3_COMMON_TOKEN number
, pANTLR3_COMMON_TOKEN size
) {
273 std::string number_str
= tokenTextSubstr(number
, 2);
274 return BitVector(tokenToUnsigned(size
), Integer(number_str
));
277 }/* CVC4::parser namespace */
278 }/* CVC4 namespace */
280 #endif /* __CVC4__PARSER__ANTLR_INPUT_H */