src/parser/antlr_input.cpp

   1 /*********************                                                        */
   2 /*! \file antlr_input.cpp
   3  ** \verbatim
   4  ** Original author: cconway
   5  ** Major contributors: none
   6  ** Minor contributors (to current version): mdeters
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  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
  13  **
  14  ** \brief A super-class for ANTLR-generated input language parsers.
  15  **
  16  ** A super-class for ANTLR-generated input language parsers
  17  **/
  18
  19 #include <limits.h>
  20 #include <antlr3.h>
  21 #include <stdint.h>
  22
  23 #include "antlr_input.h"
  24 #include "input.h"
  25 #include "bounded_token_buffer.h"
  26 #include "bounded_token_factory.h"
  27 #include "memory_mapped_input_buffer.h"
  28 #include "parser_exception.h"
  29 #include "parser.h"
  30
  31 #include "expr/command.h"
  32 #include "expr/type.h"
  33 #include "parser/cvc/cvc_input.h"
  34 #include "parser/smt/smt_input.h"
  35 #include "parser/smt2/smt2_input.h"
  36 #include "util/output.h"
  37 #include "util/Assert.h"
  38
  39 using namespace std;
  40 using namespace CVC4;
  41 using namespace CVC4::parser;
  42 using namespace CVC4::kind;
  43
  44 namespace CVC4 {
  45 namespace parser {
  46
  47 AntlrInputStream::AntlrInputStream(std::string name,
  48                                    pANTLR3_INPUT_STREAM input,
  49                                    bool fileIsTemporary) :
  50   InputStream(name,fileIsTemporary),
  51   d_input(input) {
  52   AlwaysAssert( input != NULL );
  53 }
  54
  55 AntlrInputStream::~AntlrInputStream() {
  56   d_input->free(d_input);
  57 }
  58
  59 pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const {
  60   return d_input;
  61 }
  62
  63 AntlrInputStream*
  64 AntlrInputStream::newFileInputStream(const std::string& name,
  65                                      bool useMmap)
  66   throw (InputStreamException, AssertionException) {
  67   pANTLR3_INPUT_STREAM input = NULL;
  68   if( useMmap ) {
  69     input = MemoryMappedInputBufferNew(name);
  70   } else {
  71     input = antlr3AsciiFileStreamNew((pANTLR3_UINT8) name.c_str());
  72   }
  73   if( input == NULL ) {
  74     throw InputStreamException("Couldn't open file: " + name);
  75   }
  76   return new AntlrInputStream( name, input );
  77 }
  78
  79 AntlrInputStream*
  80 AntlrInputStream::newStreamInputStream(std::istream& input,
  81                                        const std::string& name)
  82   throw (InputStreamException, AssertionException) {
  83
  84   // Since these are all NULL on entry, realloc will be called
  85   char *basep = NULL, *boundp = NULL, *cp = NULL;
  86   /* 64KB seems like a reasonable default size. */
  87   size_t bufSize = 0x10000;
  88
  89   /* Keep going until we can't go no more. */
  90   while( !input.eof() && !input.fail() ) {
  91
  92     if( cp == boundp ) {
  93       /* We ran out of room in the buffer. Realloc at double the size. */
  94       ptrdiff_t offset = cp - basep;
  95       basep = (char *) realloc(basep, bufSize);
  96       if( basep == NULL ) {
  97         throw InputStreamException("Failed buffering input stream: " + name);
  98       }
  99       cp = basep + offset;
 100       boundp = basep + bufSize;
 101       bufSize *= 2;
 102     }
 103
 104     /* Read as much as we have room for. */
 105     input.read( cp, boundp - cp );
 106     cp += input.gcount();
 107   }
 108
 109   /* Make sure the fail bit didn't get set. */
 110   if( !input.eof() ) {
 111     throw InputStreamException("Stream input failed: " + name);
 112   }
 113
 114   /* Create an ANTLR input backed by the buffer. */
 115   pANTLR3_INPUT_STREAM inputStream =
 116       antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8) basep,
 117                                         cp - basep,
 118                                         (pANTLR3_UINT8) strdup(name.c_str()));
 119   if( inputStream==NULL ) {
 120     throw InputStreamException("Couldn't initialize input: " + name);
 121   }
 122   return new AntlrInputStream( name, inputStream );
 123 }
 124
 125
 126 AntlrInputStream*
 127 AntlrInputStream::newStringInputStream(const std::string& input,
 128                                        const std::string& name)
 129   throw (InputStreamException, AssertionException) {
 130   char* inputStr = strdup(input.c_str());
 131   char* nameStr = strdup(name.c_str());
 132   AlwaysAssert( inputStr!=NULL && nameStr!=NULL );
 133   pANTLR3_INPUT_STREAM inputStream =
 134       antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8) inputStr,
 135                                         input.size(),
 136                                         (pANTLR3_UINT8) nameStr);
 137   if( inputStream==NULL ) {
 138     throw InputStreamException("Couldn't initialize string input: '" + input + "'");
 139   }
 140   return new AntlrInputStream( name, inputStream );
 141 }
 142
 143 AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream& inputStream) {
 144   using namespace language::input;
 145
 146   AntlrInput* input;
 147
 148   switch(lang) {
 149   case LANG_CVC4: {
 150     input = new CvcInput(inputStream);
 151     break;
 152   }
 153   case LANG_SMTLIB:
 154     input = new SmtInput(inputStream);
 155     break;
 156
 157   case LANG_SMTLIB_V2:
 158     input = new Smt2Input(inputStream);
 159     break;
 160
 161   default:
 162     Unhandled(lang);
 163   }
 164
 165   return input;
 166 }
 167
 168 AntlrInput::AntlrInput(AntlrInputStream& inputStream, unsigned int lookahead) :
 169     Input(inputStream),
 170     d_lookahead(lookahead),
 171     d_lexer(NULL),
 172     d_parser(NULL),
 173     d_antlr3InputStream( inputStream.getAntlr3InputStream() ),
 174     d_tokenBuffer(NULL) {
 175 }
 176
 177 /*
 178 AntlrParser::AntlrParser(ExprManager* exprManager, std::istream& input, const std::string& name, unsigned int lookahead)
 179   Parser(exprManager,name),
 180   d_lookahead(lookahead) {
 181
 182 }
 183 */
 184
 185 /*
 186 AntlrInput::Input(ExprManager* exprManager, const std::string& input, const std::string& name, unsigned int lookahead) :
 187   Input(exprManager,name),
 188   d_lookahead(lookahead),
 189   d_lexer(NULL),
 190   d_parser(NULL),
 191   d_tokenStream(NULL) {
 192
 193   char* inputStr = strdup(input.c_str());
 194   char* nameStr = strdup(name.c_str());
 195   if( inputStr==NULL || nameStr==NULL ) {
 196     throw ParserException("Couldn't initialize string input: '" + input + "'");
 197   }
 198   d_inputStream = antlr3NewAsciiStringInPlaceStream((pANTLR3_UINT8)inputStr,input.size(),(pANTLR3_UINT8)nameStr);
 199   if( d_inputStream == NULL ) {
 200     throw ParserException("Couldn't create input stream for string: '" + input + "'");
 201   }
 202
 203 }
 204 */
 205
 206 AntlrInput::~AntlrInput() {
 207   BoundedTokenBufferFree(d_tokenBuffer);
 208 }
 209
 210 pANTLR3_COMMON_TOKEN_STREAM AntlrInput::getTokenStream() {
 211   return d_tokenBuffer->commonTstream;
 212 }
 213
 214 void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) {
 215   pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super);
 216   AlwaysAssert(lexer!=NULL);
 217   Parser *parser = (Parser*)(lexer->super);
 218   AlwaysAssert(parser!=NULL);
 219   AntlrInput *input = (AntlrInput*) parser->getInput();
 220   AlwaysAssert(input!=NULL);
 221
 222   /* Call the error display routine *if* there's not already a
 223    * parse error pending.  If a parser error is pending, this
 224    * error is probably less important, so we just drop it. */
 225   if( input->d_parser->rec->state->error == ANTLR3_FALSE ) {
 226     input->parseError("Error finding next token.");
 227   }
 228 }
 229
 230 void AntlrInput::parseError(const std::string& message)
 231   throw (ParserException, AssertionException) {
 232   Debug("parser") << "Throwing exception: "
 233       << getInputStream()->getName() << ":"
 234       << d_lexer->getLine(d_lexer) << "."
 235       << d_lexer->getCharPositionInLine(d_lexer) << ": "
 236       << message << endl;
 237   throw ParserException(message, getInputStream()->getName(),
 238                         d_lexer->getLine(d_lexer),
 239                         d_lexer->getCharPositionInLine(d_lexer));
 240 }
 241
 242
 243 void AntlrInput::setAntlr3Lexer(pANTLR3_LEXER pLexer) {
 244   d_lexer = pLexer;
 245
 246   pANTLR3_TOKEN_FACTORY pTokenFactory = d_lexer->rec->state->tokFactory;
 247   if( pTokenFactory != NULL ) {
 248     pTokenFactory->close(pTokenFactory);
 249   }
 250
 251   /* 2*lookahead should be sufficient, but we give ourselves some breathing room. */
 252   pTokenFactory = BoundedTokenFactoryNew(d_antlr3InputStream, 2*d_lookahead);
 253   if( pTokenFactory == NULL ) {
 254     throw ParserException("Couldn't create token factory.");
 255   }
 256   d_lexer->rec->state->tokFactory = pTokenFactory;
 257
 258   pBOUNDED_TOKEN_BUFFER buffer = BoundedTokenBufferSourceNew(d_lookahead, d_lexer->rec->state->tokSource);
 259   if( buffer == NULL ) {
 260     throw ParserException("Couldn't create token buffer.");
 261   }
 262
 263   d_tokenBuffer = buffer;
 264
 265   // Override default lexer error reporting
 266   d_lexer->rec->reportError = &lexerError;
 267   // Override default nextToken function, just to prevent exceptions escaping.
 268   d_lexer->rec->state->tokSource->nextToken = &nextTokenStr;
 269 }
 270
 271 void AntlrInput::setParser(Parser& parser) {
 272   // ANTLR isn't using super in the lexer or the parser, AFAICT.
 273   // We could also use @lexer/parser::context to add a field to the generated
 274   // objects, but then it would have to be declared separately in every
 275   // language's grammar and we'd have to in the address of the field anyway.
 276   d_lexer->super = &parser;
 277   d_parser->super = &parser;
 278 }
 279
 280 void AntlrInput::setAntlr3Parser(pANTLR3_PARSER pParser) {
 281   d_parser = pParser;
 282 //  d_parser->rec->match = &match;
 283   d_parser->rec->reportError = &reportError;
 284   /* Don't try to recover from a parse error. */
 285   // [chris 4/5/2010] Not clear on why this cast is necessary, but I get an error if I remove it.
 286   d_parser->rec->recoverFromMismatchedToken =
 287       (void* (*)(ANTLR3_BASE_RECOGNIZER_struct*, ANTLR3_UINT32, ANTLR3_BITSET_LIST_struct*))
 288       d_parser->rec->mismatch;
 289 }
 290
 291
 292 }/* CVC4::parser namespace */
 293 }/* CVC4 namespace */