src/parser/antlr_input.cpp

   1 /*********************                                                        */
   2 /** input.cpp
   3  ** Original author: cconway
   4  ** Major contributors: none
   5  ** Minor contributors (to current version): none
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   8  ** Courant Institute of Mathematical Sciences
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  ** A super-class for ANTLR-generated input language parsers
  14  **/
  15
  16 #include <limits.h>
  17 #include <antlr3.h>
  18
  19 #include "antlr_input.h"
  20 #include "input.h"
  21 #include "bounded_token_buffer.h"
  22 #include "bounded_token_factory.h"
  23 #include "memory_mapped_input_buffer.h"
  24 #include "parser_exception.h"
  25 #include "parser.h"
  26
  27 #include "expr/command.h"
  28 #include "expr/type.h"
  29 #include "parser/cvc/cvc_input.h"
  30 #include "parser/smt/smt_input.h"
  31 #include "parser/smt2/smt2_input.h"
  32 #include "util/output.h"
  33 #include "util/Assert.h"
  34
  35 using namespace std;
  36 using namespace CVC4;
  37 using namespace CVC4::parser;
  38 using namespace CVC4::kind;
  39
  40 namespace CVC4 {
  41 namespace parser {
  42
  43 AntlrInputStream::AntlrInputStream(std::string name, pANTLR3_INPUT_STREAM input) :
  44   InputStream(name),
  45   d_input(input) {
  46 }
  47
  48 AntlrInputStream::~AntlrInputStream() {
  49   d_input->free(d_input);
  50 }
  51
  52 pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const {
  53   return d_input;
  54 }
  55
  56 AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap) {
  57   if( useMmap ) {
  58     return new AntlrInputStream( name, MemoryMappedInputBufferNew(name) );
  59   } else {
  60     return new AntlrInputStream( name, antlr3AsciiFileStreamNew((pANTLR3_UINT8) name.c_str()) );
  61   }
  62 /*
  63     if( d_inputStream == NULL ) {
  64       throw ParserException("Couldn't open file: " + filename);
  65     }
  66 */
  67 }
  68
  69 AntlrInputStream* AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name) /*throw (InputStreamException) */{
  70   char* inputStr = strdup(input.c_str());
  71   char* nameStr = strdup(name.c_str());
  72 /*
  73   if( inputStr==NULL || nameStr==NULL ) {
  74     throw InputStreamException("Couldn't initialize string input: '" + input + "'");
  75   }
  76 */
  77   return new AntlrInputStream( name,
  78                                antlr3NewAsciiStringInPlaceStream(
  79                                   (pANTLR3_UINT8)inputStr,input.size(),
  80                                   (pANTLR3_UINT8)nameStr) );
  81 }
  82
  83 AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream *inputStream) {
  84   AntlrInput* input;
  85
  86   switch(lang) {
  87   case LANG_CVC4: {
  88     input = new CvcInput(inputStream);
  89     break;
  90   }
  91   case LANG_SMTLIB:
  92     input = new SmtInput(inputStream);
  93     break;
  94
  95   case LANG_SMTLIB_V2:
  96     input = new Smt2Input(inputStream);
  97     break;
  98
  99   default:
 100     Unhandled(lang);
 101   }
 102   return input;
 103 }
 104
 105 AntlrInput::AntlrInput(AntlrInputStream *inputStream, unsigned int lookahead) :
 106     Input(inputStream),
 107     d_lookahead(lookahead),
 108     d_lexer(NULL),
 109     d_parser(NULL),
 110     d_antlr3InputStream( inputStream->getAntlr3InputStream() ),
 111     d_tokenStream(NULL) {
 112 }
 113
 114 /*
 115 AntlrParser::AntlrParser(ExprManager* exprManager, std::istream& input, const std::string& name, unsigned int lookahead)
 116   Parser(exprManager,name),
 117   d_lookahead(lookahead) {
 118
 119 }
 120 */
 121
 122 /*
 123 AntlrInput::Input(ExprManager* exprManager, const std::string& input, const std::string& name, unsigned int lookahead) :
 124   Input(exprManager,name),
 125   d_lookahead(lookahead),
 126   d_lexer(NULL),
 127   d_parser(NULL),
 128   d_tokenStream(NULL) {
 129
 130   char* inputStr = strdup(input.c_str());
 131   char* nameStr = strdup(name.c_str());
 132   if( inputStr==NULL || nameStr==NULL ) {
 133     throw ParserException("Couldn't initialize string input: '" + input + "'");
 134   }
 135   d_inputStream = antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8)inputStr,input.size(),(pANTLR3_UINT8)nameStr);
 136   if( d_inputStream == NULL ) {
 137     throw ParserException("Couldn't create input stream for string: '" + input + "'");
 138   }
 139
 140 }
 141 */
 142
 143 AntlrInput::~AntlrInput() {
 144   d_tokenStream->free(d_tokenStream);
 145 }
 146
 147 pANTLR3_COMMON_TOKEN_STREAM AntlrInput::getTokenStream() {
 148   return d_tokenStream;
 149 }
 150
 151 void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) {
 152   pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super);
 153   AlwaysAssert(lexer!=NULL);
 154   Parser *parser = (Parser*)(lexer->super);
 155   AlwaysAssert(parser!=NULL);
 156   AntlrInput *input = (AntlrInput*) parser->getInput();
 157   AlwaysAssert(input!=NULL);
 158
 159   // Call the error display routine
 160   input->parseError("Error finding next token.");
 161 }
 162
 163 void AntlrInput::parseError(const std::string& message)
 164     throw (ParserException) {
 165   Debug("parser") << "Throwing exception: "
 166       << getInputStream()->getName() << ":"
 167       << d_lexer->getLine(d_lexer) << "."
 168       << d_lexer->getCharPositionInLine(d_lexer) << ": "
 169       << message << endl;
 170   throw ParserException(message, getInputStream()->getName(),
 171                         d_lexer->getLine(d_lexer),
 172                         d_lexer->getCharPositionInLine(d_lexer));
 173 }
 174
 175
 176 void AntlrInput::setAntlr3Lexer(pANTLR3_LEXER pLexer) {
 177   d_lexer = pLexer;
 178
 179   pANTLR3_TOKEN_FACTORY pTokenFactory = d_lexer->rec->state->tokFactory;
 180   if( pTokenFactory != NULL ) {
 181     pTokenFactory->close(pTokenFactory);
 182   }
 183
 184   /* 2*lookahead should be sufficient, but we give ourselves some breathing room. */
 185   pTokenFactory = BoundedTokenFactoryNew(d_antlr3InputStream, 2*d_lookahead);
 186   if( pTokenFactory == NULL ) {
 187     throw ParserException("Couldn't create token factory.");
 188   }
 189   d_lexer->rec->state->tokFactory = pTokenFactory;
 190
 191   pBOUNDED_TOKEN_BUFFER buffer = BoundedTokenBufferSourceNew(d_lookahead, d_lexer->rec->state->tokSource);
 192   if( buffer == NULL ) {
 193     throw ParserException("Couldn't create token buffer.");
 194   }
 195
 196   d_tokenStream = buffer->commonTstream;
 197
 198   // Override default lexer error reporting
 199   d_lexer->rec->reportError = &lexerError;
 200 }
 201
 202 void AntlrInput::setParser(Parser *parser) {
 203   // ANTLR isn't using super in the lexer or the parser, AFAICT.
 204   // We could also use @lexer/parser::context to add a field to the generated
 205   // objects, but then it would have to be declared separately in every
 206   // language's grammar and we'd have to in the address of the field anyway.
 207   d_lexer->super = parser;
 208   d_parser->super = parser;
 209
 210 }
 211
 212 void AntlrInput::setAntlr3Parser(pANTLR3_PARSER pParser) {
 213   d_parser = pParser;
 214 //  d_parser->rec->match = &match;
 215   d_parser->rec->reportError = &reportError;
 216   /* Don't try to recover from a parse error. */
 217   // [chris 4/5/2010] Not clear on why this cast is necessary, but I get an error if I remove it.
 218   d_parser->rec->recoverFromMismatchedToken =
 219       (void* (*)(ANTLR3_BASE_RECOGNIZER_struct*, ANTLR3_UINT32, ANTLR3_BITSET_LIST_struct*))
 220       d_parser->rec->mismatch;
 221 }
 222
 223
 224 }/* CVC4::parser namespace */
 225 }/* CVC4 namespace */