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