--- /dev/null
+/********************* */
+/** input.cpp
+ ** 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** A super-class for ANTLR-generated input language parsers
+ **/
+
+#include <limits.h>
+#include <antlr3.h>
+
+#include "antlr_input.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.h"
+
+#include "expr/command.h"
+#include "expr/type.h"
+#include "parser/cvc/cvc_input.h"
+#include "parser/smt/smt_input.h"
+#include "parser/smt2/smt2_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 {
+
+AntlrInputStream::AntlrInputStream(std::string name, pANTLR3_INPUT_STREAM input) :
+ InputStream(name),
+ d_input(input) {
+}
+
+AntlrInputStream::~AntlrInputStream() {
+ d_input->free(d_input);
+}
+
+pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const {
+ return d_input;
+}
+
+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()) );
+ }
+/*
+ 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 + "'");
+ }
+*/
+ return new AntlrInputStream( name,
+ antlr3NewAsciiStringInPlaceStream(
+ (pANTLR3_UINT8)inputStr,input.size(),
+ (pANTLR3_UINT8)nameStr) );
+}
+
+AntlrInput* AntlrInput::newInput(InputLanguage lang, AntlrInputStream *inputStream) {
+ AntlrInput* input;
+
+ switch(lang) {
+ case LANG_CVC4: {
+ input = new CvcInput(inputStream);
+ break;
+ }
+ case LANG_SMTLIB:
+ input = new SmtInput(inputStream);
+ break;
+
+ case LANG_SMTLIB_V2:
+ input = new Smt2Input(inputStream);
+ break;
+
+ default:
+ Unhandled(lang);
+ }
+ return input;
+}
+
+AntlrInput::AntlrInput(AntlrInputStream *inputStream, unsigned int lookahead) :
+ Input(inputStream),
+ d_lookahead(lookahead),
+ d_lexer(NULL),
+ d_parser(NULL),
+ d_antlr3InputStream( inputStream->getAntlr3InputStream() ),
+ d_tokenStream(NULL) {
+}
+
+/*
+AntlrParser::AntlrParser(ExprManager* exprManager, std::istream& input, const std::string& name, unsigned int lookahead)
+ Parser(exprManager,name),
+ d_lookahead(lookahead) {
+
+}
+*/
+
+/*
+AntlrInput::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 + "'");
+ }
+
+}
+*/
+
+AntlrInput::~AntlrInput() {
+ d_tokenStream->free(d_tokenStream);
+}
+
+pANTLR3_COMMON_TOKEN_STREAM AntlrInput::getTokenStream() {
+ return d_tokenStream;
+}
+
+void AntlrInput::lexerError(pANTLR3_BASE_RECOGNIZER recognizer) {
+ pANTLR3_LEXER lexer = (pANTLR3_LEXER)(recognizer->super);
+ AlwaysAssert(lexer!=NULL);
+ Parser *parser = (Parser*)(lexer->super);
+ AlwaysAssert(parser!=NULL);
+ AntlrInput *input = (AntlrInput*) parser->getInput();
+ AlwaysAssert(input!=NULL);
+
+ // Call the error display routine
+ input->parseError("Error finding next token.");
+}
+
+void AntlrInput::parseError(const std::string& message)
+ throw (ParserException) {
+ Debug("parser") << "Throwing exception: "
+ << getInputStream()->getName() << ":"
+ << d_lexer->getLine(d_lexer) << "."
+ << d_lexer->getCharPositionInLine(d_lexer) << ": "
+ << message << endl;
+ throw ParserException(message, getInputStream()->getName(),
+ d_lexer->getLine(d_lexer),
+ d_lexer->getCharPositionInLine(d_lexer));
+}
+
+
+void AntlrInput::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_antlr3InputStream, 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 AntlrInput::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 AntlrInput::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 */
--- /dev/null
+/********************* */
+/** input.h
+ ** 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)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.
+ **
+ ** Base for ANTLR parser classes.
+ **/
+
+#include "cvc4parser_private.h"
+
+#ifndef __CVC4__PARSER__ANTLR_INPUT_H
+#define __CVC4__PARSER__ANTLR_INPUT_H
+
+#include <antlr3.h>
+#include <iostream>
+#include <string>
+#include <vector>
+
+#include "input.h"
+#include "parser_options.h"
+#include "parser_exception.h"
+#include "expr/expr.h"
+#include "expr/expr_manager.h"
+#include "util/Assert.h"
+
+namespace CVC4 {
+
+class Command;
+class Type;
+class FunctionType;
+
+namespace parser {
+
+/** Wrapper around an ANTLR3 input stream. */
+class AntlrInputStream : public InputStream {
+ pANTLR3_INPUT_STREAM d_input;
+
+ AntlrInputStream(std::string name,pANTLR3_INPUT_STREAM input);
+
+ /* This is private and unimplemented, because you should never use it. */
+ AntlrInputStream(const AntlrInputStream& inputStream);
+
+ /* This is private and unimplemented, because you should never use it. */
+ AntlrInputStream& operator=(const AntlrInputStream& inputStream);
+
+public:
+
+ virtual ~AntlrInputStream();
+
+ pANTLR3_INPUT_STREAM getAntlr3InputStream() const;
+
+ /** Create a file input.
+ *
+ * @param filename the path of the file to read
+ * @param useMmap <code>true</code> if the input should use memory-mapped I/O; otherwise, the
+ * input will use the standard ANTLR3 I/O implementation.
+ */
+ static AntlrInputStream* newFileInputStream(const std::string& name, bool useMmap = false);
+
+ /** Create an input from an istream. */
+ // AntlrInputStream newInputStream(std::istream& input, const std::string& name);
+
+ /** Create a string input.
+ *
+ * @param input the string to read
+ * @param name the "filename" to use when reporting errors
+ */
+ static AntlrInputStream* newStringInputStream(const std::string& input, const std::string& name);
+};
+
+class Parser;
+
+/**
+ * An input to be parsed. The static factory methods in this class (e.g.,
+ * <code>newFileInput</code>, <code>newStringInput</code>) create a parser
+ * for the given input language and attach it to an input source of the
+ * appropriate type.
+ */
+class AntlrInput : public Input{
+ /** The token lookahead used to lex and parse the input. This should usually be equal to
+ * <code>K</code> for an LL(k) grammar. */
+ unsigned int d_lookahead;
+
+ /** The ANTLR3 lexer associated with this input. This will be <code>NULL</code> initially. It
+ * must be set by a call to <code>setLexer</code>, preferably in the subclass constructor. */
+ pANTLR3_LEXER d_lexer;
+
+ /** The ANTLR3 parser associated with this input. This will be <code>NULL</code> initially. It
+ * must be set by a call to <code>setParser</code>, preferably in the subclass constructor.
+ * The <code>super</code> field of <code>d_parser</code> will be set to <code>this</code> and
+ * <code>reportError</code> will be set to <code>Input::reportError</code>. */
+ pANTLR3_PARSER d_parser;
+
+ /** The ANTLR3 input stream associated with this input. */
+ pANTLR3_INPUT_STREAM d_antlr3InputStream;
+
+ /** The ANTLR3 token stream associated with this input. We only need this so we can free it on exit.
+ * This is set by <code>setLexer</code>.
+ * NOTE: We assume that we <em>can</em> free it on exit. No sharing! */
+ pANTLR3_COMMON_TOKEN_STREAM d_tokenStream;
+
+ /** Turns an ANTLR3 exception into a message for the user and calls <code>parseError</code>. */
+ static void reportError(pANTLR3_BASE_RECOGNIZER recognizer);
+
+ /** Builds a message for a lexer error and calls <code>parseError</code>. */
+ static void lexerError(pANTLR3_BASE_RECOGNIZER recognizer);
+
+ /* Since we own d_tokenStream and it needs to be freed, we need to prevent
+ * copy construction and assignment.
+ */
+ AntlrInput(const AntlrInput& input);
+ AntlrInput& operator=(const AntlrInput& input);
+
+public:
+
+ /** Destructor. Frees the token stream and closes the input. */
+ virtual ~AntlrInput();
+
+ /** Create an input for the given AntlrInputStream. NOTE: the new Input
+ * will take ownership of the input stream and delete it at destruction time.
+ *
+ * @param lang the input language
+ * @param inputStream the input stream
+ *
+ * */
+ static AntlrInput* newInput(InputLanguage lang, AntlrInputStream *inputStream);
+
+ /** Retrieve the text associated with a token. */
+ inline static std::string tokenText(pANTLR3_COMMON_TOKEN token);
+ /** Retrieve an Integer from the text of a token */
+ inline static Integer tokenToInteger( pANTLR3_COMMON_TOKEN token );
+ /** Retrieve a Rational from the text of a token */
+ inline static Rational tokenToRational(pANTLR3_COMMON_TOKEN token);
+
+protected:
+ /** Create an input. This input takes ownership of the given input stream,
+ * and will delete it at destruction time.
+ *
+ * @param inputStream the input stream to use
+ * @param lookahead the lookahead needed to parse the input (i.e., k for
+ * an LL(k) grammar)
+ */
+ AntlrInput(AntlrInputStream *inputStream, unsigned int lookahead);
+
+ /** Retrieve the token stream for this parser. Must not be called before
+ * <code>setLexer()</code>. */
+ pANTLR3_COMMON_TOKEN_STREAM getTokenStream();
+
+ /**
+ * Throws a <code>ParserException</code> with the given message.
+ */
+ void parseError(const std::string& msg) throw (ParserException);
+
+ /** Set the ANTLR3 lexer for this input. */
+ void setAntlr3Lexer(pANTLR3_LEXER pLexer);
+
+ /** Set the ANTLR3 parser implementation for this input. */
+ void setAntlr3Parser(pANTLR3_PARSER pParser);
+
+ /** Set the Parser object for this input. */
+ void setParser(Parser *parser);
+};
+
+std::string AntlrInput::tokenText(pANTLR3_COMMON_TOKEN token) {
+ ANTLR3_MARKER start = token->getStartIndex(token);
+ ANTLR3_MARKER end = token->getStopIndex(token);
+ /* start and end are boundary pointers. The text is a string
+ * of (end-start+1) bytes beginning at start. */
+ std::string txt( (const char *)start, end-start+1 );
+ Debug("parser-extra") << "tokenText: start=" << start << std::endl
+ << "end=" << end << std::endl
+ << "txt='" << txt << "'" << std::endl;
+ return txt;
+}
+
+Integer AntlrInput::tokenToInteger(pANTLR3_COMMON_TOKEN token) {
+ Integer i( tokenText(token) );
+ return i;
+}
+
+Rational AntlrInput::tokenToRational(pANTLR3_COMMON_TOKEN token) {
+ Rational r( tokenText(token) );
+ return r;
+}
+
+}/* CVC4::parser namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__PARSER__ANTLR_INPUT_H */
projects / cvc5.git / commitdiff