diff options
Diffstat (limited to 'src/parser/input.cpp')
-rw-r--r-- | src/parser/input.cpp | 253 |
1 files changed, 189 insertions, 64 deletions
diff --git a/src/parser/input.cpp b/src/parser/input.cpp index fd1a4cbd6..5df017f16 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -1,7 +1,7 @@ /********************* */ /** input.cpp - ** Original author: dejan - ** Major contributors: mdeters, cconway + ** Original author: cconway + ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) @@ -10,113 +10,176 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** Parser implementation. + ** A super-class for ANTLR-generated input language parsers **/ -#include <stdint.h> +#include <limits.h> +#include <antlr3.h> #include "input.h" +#include "bounded_token_buffer.h" +#include "bounded_token_factory.h" +#include "memory_mapped_input_buffer.h" #include "parser_exception.h" -#include "parser_options.h" -#include "parser_state.h" +#include "parser.h" + #include "expr/command.h" -#include "expr/expr.h" +#include "expr/type.h" #include "parser/cvc/cvc_input.h" #include "parser/smt/smt_input.h" #include "util/output.h" #include "util/Assert.h" using namespace std; +using namespace CVC4; +using namespace CVC4::parser; +using namespace CVC4::kind; namespace CVC4 { namespace parser { -bool Input::done() const { - return d_parserState->done(); +AntlrInputStream::AntlrInputStream(std::string name, pANTLR3_INPUT_STREAM input) : + d_name(name), + d_input(input) { } -void Input::disableChecks() { - d_parserState->disableChecks(); +AntlrInputStream::~AntlrInputStream() { + d_input->free(d_input); } -void Input::enableChecks() { - d_parserState->enableChecks(); +pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const { + return d_input; } -Command* Input::parseNextCommand() throw(ParserException) { - Debug("parser") << "parseNextCommand()" << std::endl; - Command* cmd = NULL; - if(!done()) { - try { - cmd = doParseCommand(); - if(cmd == NULL) { - d_parserState->setDone(); - } - } catch(ParserException& e) { - d_parserState->setDone(); - throw; - } +const std::string AntlrInputStream::getName() const { + return d_name; +} + +AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap) { + if( useMmap ) { + return new AntlrInputStream( name, MemoryMappedInputBufferNew(name) ); + } else { + return new AntlrInputStream( name, antlr3AsciiFileStreamNew((pANTLR3_UINT8) name.c_str()) ); } - Debug("parser") << "parseNextCommand() => " << cmd << std::endl; - return cmd; -} - -Expr Input::parseNextExpression() throw(ParserException) { - Debug("parser") << "parseNextExpression()" << std::endl; - Expr result; - if(!done()) { - try { - result = doParseExpr(); - if(result.isNull()) - d_parserState->setDone(); - } catch(ParserException& e) { - d_parserState->setDone(); - throw; +/* + if( d_inputStream == NULL ) { + throw ParserException("Couldn't open file: " + filename); } +*/ +} + +AntlrInputStream* AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name) /*throw (InputStreamException) */{ + char* inputStr = strdup(input.c_str()); + char* nameStr = strdup(name.c_str()); +/* + if( inputStr==NULL || nameStr==NULL ) { + throw InputStreamException("Couldn't initialize string input: '" + input + "'"); } - Debug("parser") << "parseNextExpression() => " << result << std::endl; - return result; +*/ + return new AntlrInputStream( name, + antlr3NewAsciiStringInPlaceStream( + (pANTLR3_UINT8)inputStr,input.size(), + (pANTLR3_UINT8)nameStr) ); +} + + +Input::Input(AntlrInputStream *inputStream, unsigned int lookahead) : + d_lookahead(lookahead), + d_lexer(NULL), + d_parser(NULL), + d_tokenStream(NULL), + d_inputStream( inputStream ) { + +/* + if( useMmap ) { + d_inputStream = MemoryMappedInputBufferNew(filename); + } else { + d_inputStream = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename.c_str()); + } +*/ +/* + if( d_inputStream == NULL ) { + throw ParserException("Couldn't open file: " + filename); + } +*/ +} + +/* +AntlrParser::AntlrParser(ExprManager* exprManager, std::istream& input, const std::string& name, unsigned int lookahead) + Parser(exprManager,name), + d_lookahead(lookahead) { + } +*/ + +/* +Input::Input(ExprManager* exprManager, const std::string& input, const std::string& name, unsigned int lookahead) : + Input(exprManager,name), + d_lookahead(lookahead), + d_lexer(NULL), + d_parser(NULL), + d_tokenStream(NULL) { + + char* inputStr = strdup(input.c_str()); + char* nameStr = strdup(name.c_str()); + if( inputStr==NULL || nameStr==NULL ) { + throw ParserException("Couldn't initialize string input: '" + input + "'"); + } + d_inputStream = antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8)inputStr,input.size(),(pANTLR3_UINT8)nameStr); + if( d_inputStream == NULL ) { + throw ParserException("Couldn't create input stream for string: '" + input + "'"); + } -Input::Input(ExprManager* exprManager, const std::string& filename) { - d_parserState = new ParserState(exprManager,filename,this); } +*/ Input::~Input() { - delete d_parserState; + d_tokenStream->free(d_tokenStream); + delete d_inputStream; } -Input* Input::newFileInput(ExprManager* em, InputLanguage lang, - const std::string& filename, bool useMmap) { +AntlrInputStream *Input::getInputStream() { + return d_inputStream; +} - Input* input = 0; +pANTLR3_COMMON_TOKEN_STREAM Input::getTokenStream() { + return d_tokenStream; +} - switch(lang) { - case LANG_CVC4: - input = new CvcInput(em,filename,useMmap); - break; - case LANG_SMTLIB: - input = new SmtInput(em,filename,useMmap); - break; +void Input::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) { + pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super); + AlwaysAssert(lexer!=NULL); + Parser *parser = (Parser*)(lexer->super); + AlwaysAssert(parser!=NULL); + Input *input = parser->getInput(); + AlwaysAssert(input!=NULL); - default: - Unhandled(lang); - } + // Call the error display routine + input->parseError("Error finding next token."); +} - return input; +Input* Input::newFileInput(InputLanguage lang, + const std::string& filename, bool useMmap) { + AntlrInputStream *inputStream = AntlrInputStream::newFileInputStream(filename,useMmap); + return newInput(lang,inputStream); } -Input* Input::newStringInput(ExprManager* em, InputLanguage lang, +Input* Input::newStringInput(InputLanguage lang, const std::string& str, const std::string& name) { - Input* input = 0; + AntlrInputStream *inputStream = AntlrInputStream::newStringInputStream(str,name); + return newInput(lang,inputStream); +} + +Input* Input::newInput(InputLanguage lang, AntlrInputStream *inputStream) { + Input* input; switch(lang) { case LANG_CVC4: { - input = new CvcInput(em,str,name); + input = new CvcInput(inputStream); break; } case LANG_SMTLIB: - input = new SmtInput(em,str,name); + input = new SmtInput(inputStream); break; default: @@ -125,5 +188,67 @@ Input* Input::newStringInput(ExprManager* em, InputLanguage lang, return input; } + +void Input::parseError(const std::string& message) + throw (ParserException) { + Debug("parser") << "Throwing exception: " + << d_inputStream->getName() << ":" + << d_lexer->getLine(d_lexer) << "." + << d_lexer->getCharPositionInLine(d_lexer) << ": " + << message << endl; + throw ParserException(message, d_inputStream->getName(), + d_lexer->getLine(d_lexer), + d_lexer->getCharPositionInLine(d_lexer)); +} + + +void Input::setAntlr3Lexer(pANTLR3_LEXER pLexer) { + d_lexer = pLexer; + + pANTLR3_TOKEN_FACTORY pTokenFactory = d_lexer->rec->state->tokFactory; + if( pTokenFactory != NULL ) { + pTokenFactory->close(pTokenFactory); + } + + /* 2*lookahead should be sufficient, but we give ourselves some breathing room. */ + pTokenFactory = BoundedTokenFactoryNew(d_inputStream->getAntlr3InputStream(), 2*d_lookahead); + if( pTokenFactory == NULL ) { + throw ParserException("Couldn't create token factory."); + } + d_lexer->rec->state->tokFactory = pTokenFactory; + + pBOUNDED_TOKEN_BUFFER buffer = BoundedTokenBufferSourceNew(d_lookahead, d_lexer->rec->state->tokSource); + if( buffer == NULL ) { + throw ParserException("Couldn't create token buffer."); + } + + d_tokenStream = buffer->commonTstream; + + // Override default lexer error reporting + d_lexer->rec->reportError = &lexerError; +} + +void Input::setParser(Parser *parser) { + // ANTLR isn't using super in the lexer or the parser, AFAICT. + // We could also use @lexer/parser::context to add a field to the generated + // objects, but then it would have to be declared separately in every + // language's grammar and we'd have to in the address of the field anyway. + d_lexer->super = parser; + d_parser->super = parser; + +} + +void Input::setAntlr3Parser(pANTLR3_PARSER pParser) { + d_parser = pParser; +// d_parser->rec->match = &match; + d_parser->rec->reportError = &reportError; + /* Don't try to recover from a parse error. */ + // [chris 4/5/2010] Not clear on why this cast is necessary, but I get an error if I remove it. + d_parser->rec->recoverFromMismatchedToken = + (void* (*)(ANTLR3_BASE_RECOGNIZER_struct*, ANTLR3_UINT32, ANTLR3_BITSET_LIST_struct*)) + d_parser->rec->mismatch; +} + + }/* CVC4::parser namespace */ }/* CVC4 namespace */ |