1 /********************* */
2 /*! \file antlr_input.cpp
4 ** Original author: Christopher L. Conway
5 ** Major contributors: Morgan Deters
6 ** Minor contributors (to current version): Francois Bobot
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief A super-class for ANTLR-generated input language parsers.
14 ** A super-class for ANTLR-generated input language parsers
21 #include "parser/antlr_input.h"
22 #include "parser/input.h"
23 #include "parser/bounded_token_buffer.h"
24 #include "parser/bounded_token_factory.h"
25 #include "parser/antlr_line_buffered_input.h"
26 #include "parser/memory_mapped_input_buffer.h"
27 #include "parser/parser_exception.h"
28 #include "parser/parser.h"
30 #include "expr/command.h"
31 #include "expr/type.h"
32 #include "parser/cvc/cvc_input.h"
33 #include "parser/smt1/smt1_input.h"
34 #include "parser/smt2/smt2_input.h"
35 #include "parser/tptp/tptp_input.h"
36 #include "util/output.h"
40 using namespace CVC4::parser
;
41 using namespace CVC4::kind
;
46 AntlrInputStream::AntlrInputStream(std::string name
,
47 pANTLR3_INPUT_STREAM input
,
48 bool fileIsTemporary
) :
49 InputStream(name
,fileIsTemporary
),
51 assert( input
!= NULL
);
54 AntlrInputStream::~AntlrInputStream() {
55 d_input
->free(d_input
);
58 pANTLR3_INPUT_STREAM
AntlrInputStream::getAntlr3InputStream() const {
63 AntlrInputStream::newFileInputStream(const std::string
& name
,
65 throw (InputStreamException
) {
71 pANTLR3_INPUT_STREAM input
= NULL
;
73 input
= MemoryMappedInputBufferNew(name
);
75 // libantlr3c v3.2 isn't source-compatible with v3.4
76 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
77 input
= antlr3AsciiFileStreamNew((pANTLR3_UINT8
) name
.c_str());
78 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
79 input
= antlr3FileStreamNew((pANTLR3_UINT8
) name
.c_str(), ANTLR3_ENC_8BIT
);
80 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
83 throw InputStreamException("Couldn't open file: " + name
);
85 return new AntlrInputStream( name
, input
);
89 AntlrInputStream::newStreamInputStream(std::istream
& input
,
90 const std::string
& name
,
92 throw (InputStreamException
) {
94 pANTLR3_INPUT_STREAM inputStream
= NULL
;
97 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
99 antlr3LineBufferedStreamNew(input
,
101 (pANTLR3_UINT8
) strdup(name
.c_str()));
102 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
104 antlr3LineBufferedStreamNew(input
,
106 (pANTLR3_UINT8
) strdup(name
.c_str()));
107 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
110 // Since these are all NULL on entry, realloc will be called
111 char *basep
= NULL
, *boundp
= NULL
, *cp
= NULL
;
112 /* 64KB seems like a reasonable default size. */
113 size_t bufSize
= 0x10000;
115 /* Keep going until we can't go no more. */
116 while( !input
.eof() && !input
.fail() ) {
119 /* We ran out of room in the buffer. Realloc at double the size. */
120 ptrdiff_t offset
= cp
- basep
;
121 basep
= (char *) realloc(basep
, bufSize
);
122 if( basep
== NULL
) {
123 throw InputStreamException("Failed buffering input stream: " + name
);
126 boundp
= basep
+ bufSize
;
130 /* Read as much as we have room for. */
131 input
.read( cp
, boundp
- cp
);
132 cp
+= input
.gcount();
135 /* Make sure the fail bit didn't get set. */
137 throw InputStreamException("Stream input failed: " + name
);
140 /* Create an ANTLR input backed by the buffer. */
141 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
143 antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8
) basep
,
145 (pANTLR3_UINT8
) strdup(name
.c_str()));
146 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
148 antlr3StringStreamNew((pANTLR3_UINT8
) basep
,
151 (pANTLR3_UINT8
) strdup(name
.c_str()));
152 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
156 if( inputStream
== NULL
) {
157 throw InputStreamException("Couldn't initialize input: " + name
);
160 return new AntlrInputStream( name
, inputStream
);
165 AntlrInputStream::newStringInputStream(const std::string
& input
,
166 const std::string
& name
)
167 throw (InputStreamException
) {
168 char* inputStr
= strdup(input
.c_str());
169 char* nameStr
= strdup(name
.c_str());
170 assert( inputStr
!=NULL
&& nameStr
!=NULL
);
171 #ifdef CVC4_ANTLR3_OLD_INPUT_STREAM
172 pANTLR3_INPUT_STREAM inputStream
=
173 antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8
) inputStr
,
175 (pANTLR3_UINT8
) nameStr
);
176 #else /* CVC4_ANTLR3_OLD_INPUT_STREAM */
177 pANTLR3_INPUT_STREAM inputStream
=
178 antlr3StringStreamNew((pANTLR3_UINT8
) inputStr
,
181 (pANTLR3_UINT8
) nameStr
);
182 #endif /* CVC4_ANTLR3_OLD_INPUT_STREAM */
183 if( inputStream
==NULL
) {
184 throw InputStreamException("Couldn't initialize string input: '" + input
+ "'");
186 return new AntlrInputStream( name
, inputStream
);
189 AntlrInput
* AntlrInput::newInput(InputLanguage lang
, AntlrInputStream
& inputStream
) {
190 using namespace language::input
;
196 input
= new CvcInput(inputStream
);
200 input
= new Smt1Input(inputStream
);
204 input
= new Smt2Input(inputStream
);
208 input
= new TptpInput(inputStream
);
212 std::stringstream ss
;
213 ss
<< "internal error: unhandled language " << lang
<< " in AntlrInput::newInput";
214 throw InputStreamException(ss
.str());
220 AntlrInput::AntlrInput(AntlrInputStream
& inputStream
, unsigned int lookahead
) :
222 d_lookahead(lookahead
),
225 d_antlr3InputStream( inputStream
.getAntlr3InputStream() ),
226 d_tokenBuffer(NULL
) {
230 AntlrParser::AntlrParser(ExprManager* exprManager, std::istream& input, const std::string& name, unsigned int lookahead)
231 Parser(exprManager,name),
232 d_lookahead(lookahead) {
238 AntlrInput::Input(ExprManager* exprManager, const std::string& input, const std::string& name, unsigned int lookahead) :
239 Input(exprManager,name),
240 d_lookahead(lookahead),
243 d_tokenStream(NULL) {
245 char* inputStr = strdup(input.c_str());
246 char* nameStr = strdup(name.c_str());
247 if( inputStr==NULL || nameStr==NULL ) {
248 throw ParserException("Couldn't initialize string input: '" + input + "'");
250 d_inputStream = antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8)inputStr,input.size(),(pANTLR3_UINT8)nameStr);
251 if( d_inputStream == NULL ) {
252 throw ParserException("Couldn't create input stream for string: '" + input + "'");
258 AntlrInput::~AntlrInput() {
259 BoundedTokenBufferFree(d_tokenBuffer
);
262 pANTLR3_COMMON_TOKEN_STREAM
AntlrInput::getTokenStream() {
263 return d_tokenBuffer
->commonTstream
;
266 void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer
) {
267 pANTLR3_LEXER lexer
= (pANTLR3_LEXER
)(recognizer
->super
);
269 Parser
*parser
= (Parser
*)(lexer
->super
);
270 assert(parser
!=NULL
);
271 AntlrInput
*input
= (AntlrInput
*) parser
->getInput();
274 /* Call the error display routine *if* there's not already a
275 * parse error pending. If a parser error is pending, this
276 * error is probably less important, so we just drop it. */
277 if( input
->d_parser
->rec
->state
->error
== ANTLR3_FALSE
) {
278 input
->parseError("Error finding next token.");
282 void AntlrInput::warning(const std::string
& message
) {
283 Warning() << getInputStream()->getName() << ':' << d_lexer
->getLine(d_lexer
) << '.' << d_lexer
->getCharPositionInLine(d_lexer
) << ": " << message
<< endl
;
286 void AntlrInput::parseError(const std::string
& message
, bool eofException
)
287 throw (ParserException
) {
288 Debug("parser") << "Throwing exception: "
289 << getInputStream()->getName() << ":"
290 << d_lexer
->getLine(d_lexer
) << "."
291 << d_lexer
->getCharPositionInLine(d_lexer
) << ": "
294 throw ParserEndOfFileException(message
, getInputStream()->getName(),
295 d_lexer
->getLine(d_lexer
),
296 d_lexer
->getCharPositionInLine(d_lexer
));
298 throw ParserException(message
, getInputStream()->getName(),
299 d_lexer
->getLine(d_lexer
),
300 d_lexer
->getCharPositionInLine(d_lexer
));
305 void AntlrInput::setAntlr3Lexer(pANTLR3_LEXER pLexer
) {
308 pANTLR3_TOKEN_FACTORY pTokenFactory
= d_lexer
->rec
->state
->tokFactory
;
309 if( pTokenFactory
!= NULL
) {
310 pTokenFactory
->close(pTokenFactory
);
313 /* 2*lookahead should be sufficient, but we give ourselves some breathing room. */
314 pTokenFactory
= BoundedTokenFactoryNew(d_antlr3InputStream
, 2*d_lookahead
);
315 if( pTokenFactory
== NULL
) {
316 throw InputStreamException("Couldn't create token factory.");
318 d_lexer
->rec
->state
->tokFactory
= pTokenFactory
;
320 pBOUNDED_TOKEN_BUFFER buffer
= BoundedTokenBufferSourceNew(d_lookahead
, d_lexer
->rec
->state
->tokSource
);
321 if( buffer
== NULL
) {
322 throw InputStreamException("Couldn't create token buffer.");
325 d_tokenBuffer
= buffer
;
327 // Override default lexer error reporting
328 d_lexer
->rec
->reportError
= &lexerError
;
329 // Override default nextToken function, just to prevent exceptions escaping.
330 d_lexer
->rec
->state
->tokSource
->nextToken
= &nextToken
;
333 void AntlrInput::setParser(Parser
& parser
) {
334 // ANTLR isn't using super in the lexer or the parser, AFAICT.
335 // We could also use @lexer/parser::context to add a field to the generated
336 // objects, but then it would have to be declared separately in every
337 // language's grammar and we'd have to in the address of the field anyway.
338 d_lexer
->super
= &parser
;
339 d_parser
->super
= &parser
;
342 void AntlrInput::setAntlr3Parser(pANTLR3_PARSER pParser
) {
344 // d_parser->rec->match = &match;
345 d_parser
->rec
->reportError
= &reportError
;
346 /* Don't try to recover from a parse error. */
347 // [chris 4/5/2010] Not clear on why this cast is necessary, but I get an error if I remove it.
348 d_parser
->rec
->recoverFromMismatchedToken
=
349 (void* (*)(ANTLR3_BASE_RECOGNIZER_struct
*, ANTLR3_UINT32
, ANTLR3_BITSET_LIST_struct
*))
350 d_parser
->rec
->mismatch
;
353 }/* CVC4::parser namespace */
354 }/* CVC4 namespace */