diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/main/main.cpp | 52 | ||||
-rw-r--r-- | src/parser/antlr_input.cpp | 58 | ||||
-rw-r--r-- | src/parser/antlr_input.h | 14 | ||||
-rw-r--r-- | src/parser/input.cpp | 12 | ||||
-rw-r--r-- | src/parser/input.h | 31 | ||||
-rw-r--r-- | src/parser/parser_builder.cpp | 44 | ||||
-rw-r--r-- | src/parser/parser_builder.h | 48 | ||||
-rw-r--r-- | src/parser/smt2/smt2.cpp | 2 |
8 files changed, 210 insertions, 51 deletions
diff --git a/src/main/main.cpp b/src/main/main.cpp index 6be992479..5150d32f9 100644 --- a/src/main/main.cpp +++ b/src/main/main.cpp @@ -95,11 +95,6 @@ int runCvc4(int argc, char* argv[]) { cout << unitbuf; #endif - /* NOTE: ANTLR3 doesn't support input from stdin */ - if(firstArgIndex >= argc) { - throw Exception("No input file specified."); - } - // We only accept one input file if(argc > firstArgIndex + 1) { throw Exception("Too many input files specified."); @@ -112,19 +107,26 @@ int runCvc4(int argc, char* argv[]) { SmtEngine smt(&exprMgr, &options); // If no file supplied we read from standard input - // bool inputFromStdin = firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); + bool inputFromStdin = + firstArgIndex >= argc || !strcmp("-", argv[firstArgIndex]); // Auto-detect input language by filename extension - if(/*!inputFromStdin && */options.lang == parser::LANG_AUTO) { - const char* filename = argv[firstArgIndex]; - unsigned len = strlen(filename); - if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { - options.lang = parser::LANG_SMTLIB_V2; - } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) { - options.lang = parser::LANG_SMTLIB; - } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) - || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { + const char* filename = inputFromStdin ? "<stdin>" : argv[firstArgIndex]; + + if(options.lang == parser::LANG_AUTO) { + if( inputFromStdin ) { + // We can't do any fancy detection on stdin options.lang = parser::LANG_CVC4; + } else { + unsigned len = strlen(filename); + if(len >= 5 && !strcmp(".smt2", filename + len - 5)) { + options.lang = parser::LANG_SMTLIB_V2; + } else if(len >= 4 && !strcmp(".smt", filename + len - 4)) { + options.lang = parser::LANG_SMTLIB; + } else if(( len >= 4 && !strcmp(".cvc", filename + len - 4) ) + || ( len >= 5 && !strcmp(".cvc4", filename + len - 5) )) { + options.lang = parser::LANG_CVC4; + } } } @@ -149,15 +151,19 @@ int runCvc4(int argc, char* argv[]) { } } - /* TODO: Hack ANTLR3 to support input from streams */ - ParserBuilder parserBuilder(options.lang, argv[firstArgIndex]); - - Parser *parser = - parserBuilder.withExprManager(exprMgr) + ParserBuilder parserBuilder = + ParserBuilder(exprMgr, filename) + .withInputLanguage(options.lang) .withMmap(options.memoryMap) - .withChecks(options.semanticChecks && !Configuration::isMuzzledBuild() ) - .withStrictMode( options.strictParsing ) - .build(); + .withChecks(options.semanticChecks && + !Configuration::isMuzzledBuild() ) + .withStrictMode( options.strictParsing ); + + if( inputFromStdin ) { + parserBuilder.withStreamInput(cin); + } + + Parser *parser = parserBuilder.build(); // Parse and execute commands until we are done Command* cmd; diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 300b181a6..9d75dd31f 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -40,8 +40,10 @@ using namespace CVC4::kind; namespace CVC4 { namespace parser { -AntlrInputStream::AntlrInputStream(std::string name, pANTLR3_INPUT_STREAM input) : - InputStream(name), +AntlrInputStream::AntlrInputStream(std::string name, + pANTLR3_INPUT_STREAM input, + bool fileIsTemporary) : + InputStream(name,fileIsTemporary), d_input(input) { AlwaysAssert( input != NULL ); } @@ -54,7 +56,9 @@ pANTLR3_INPUT_STREAM AntlrInputStream::getAntlr3InputStream() const { return d_input; } -AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, bool useMmap) +AntlrInputStream* +AntlrInputStream::newFileInputStream(const std::string& name, + bool useMmap) throw (InputStreamException) { pANTLR3_INPUT_STREAM input = NULL; if( useMmap ) { @@ -68,7 +72,53 @@ AntlrInputStream* AntlrInputStream::newFileInputStream(const std::string& name, return new AntlrInputStream( name, input ); } -AntlrInputStream* AntlrInputStream::newStringInputStream(const std::string& input, const std::string& name) +AntlrInputStream* +AntlrInputStream::newStreamInputStream(std::istream& input, + const std::string& name) + throw (InputStreamException) { + // // TODO: make this more portable + // char *filename = strdup("/tmp/streaminput.XXXXXX"); + // int fd = mkstemp(filename); + // if( fd == -1 ) { + // throw InputStreamException("Couldn't create temporary for stream input: " + name); + // } + + // // We don't want to use the temp file directly, so first close it + // close(fd); + + // // Make a FIFO with our reserved temporary name + // int fd = mkfifo(filename, s_IRUSR); + + // // Just stuff everything from the istream into the FIFO + // char buf[4096]; + // while( !input.eof() && !input.fail() ) { + // input.read( buf, sizeof(buf) ); + // write( fd, buf, input.gcount() ); + // } + + // if( !input.eof() ) { + // throw InputStreamException("Stream input failed: " + name); + // } + + // // Now create the ANTLR stream + // pANTLR3_INPUT_STREAM input = antlr3AsciiFileStreamNew((pANTLR3_UINT8) filename); + + // if( input == NULL ) { + // throw InputStreamException("Couldn't create stream input: " + name); + // } + + // // Create the stream with fileIsTemporary = true + // return new AntlrInputStream( name, input, true ); + + stringstream ss( ios_base::out ); + ss << input.rdbuf(); + return newStringInputStream( ss.str(), name ); +} + + +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()); diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 27337c35f..642dc9654 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -47,7 +47,9 @@ namespace parser { class AntlrInputStream : public InputStream { pANTLR3_INPUT_STREAM d_input; - AntlrInputStream(std::string name,pANTLR3_INPUT_STREAM input); + AntlrInputStream(std::string name, + pANTLR3_INPUT_STREAM input, + bool fileIsTemporary = false); /* This is private and unimplemented, because you should never use it. */ AntlrInputStream(const AntlrInputStream& inputStream); @@ -67,18 +69,22 @@ public: * @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) + static AntlrInputStream* newFileInputStream(const std::string& name, + bool useMmap = false) throw (InputStreamException); /** Create an input from an istream. */ - // AntlrInputStream newInputStream(std::istream& input, const std::string& name); + static AntlrInputStream* newStreamInputStream(std::istream& input, + const std::string& name) + throw (InputStreamException); /** 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) + static AntlrInputStream* newStringInputStream(const std::string& input, + const std::string& name) throw (InputStreamException); }; diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 9ee167897..a900765b5 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -55,7 +55,17 @@ Input* Input::newFileInput(InputLanguage lang, const std::string& filename, bool useMmap) throw (InputStreamException) { - AntlrInputStream *inputStream = AntlrInputStream::newFileInputStream(filename,useMmap); + AntlrInputStream *inputStream = + AntlrInputStream::newFileInputStream(filename,useMmap); + return AntlrInput::newInput(lang,*inputStream); +} + +Input* Input::newStreamInput(InputLanguage lang, + std::istream& input, + const std::string& name) + throw (InputStreamException) { + AntlrInputStream *inputStream = + AntlrInputStream::newStreamInputStream(input,name); return AntlrInput::newInput(lang,*inputStream); } diff --git a/src/parser/input.h b/src/parser/input.h index ccae2d84b..926ebe156 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -20,6 +20,7 @@ #include <iostream> #include <string> +#include <stdio.h> #include <vector> #include "expr/expr.h" @@ -49,17 +50,26 @@ class InputStream { /** The name of this input stream. */ std::string d_name; + /** Indicates whether the input file is a temporary that we should + * delete on exit. */ + bool d_fileIsTemporary; + protected: /** Initialize the input stream with a name. */ - InputStream(std::string name) : - d_name(name) { + InputStream(std::string name, bool isTemporary=false) : + d_name(name), + d_fileIsTemporary(isTemporary) { } public: - /** Do-nothing destructor. */ - virtual ~InputStream() { } + /** Destructor. */ + virtual ~InputStream() { + if( d_fileIsTemporary ) { + remove(d_name.c_str()); + } + } /** Get the name of this input stream. */ const std::string getName() const; @@ -92,7 +102,9 @@ class CVC4_PUBLIC Input { * @param filename the input filename * @param useMmap true if the parser should use memory-mapped I/O (default: false) */ - static Input* newFileInput(InputLanguage lang, const std::string& filename, bool useMmap=false) + static Input* newFileInput(InputLanguage lang, + const std::string& filename, + bool useMmap=false) throw (InputStreamException); /** Create an input for the given stream. @@ -101,7 +113,10 @@ class CVC4_PUBLIC Input { * @param input the input stream * @param name the name of the stream, for use in error messages */ - //static Parser* newStreamInput(InputLanguage lang, std::istream& input, const std::string& name); + static Input* newStreamInput(InputLanguage lang, + std::istream& input, + const std::string& name) + throw (InputStreamException); /** Create an input for the given string * @@ -109,7 +124,9 @@ class CVC4_PUBLIC Input { * @param input the input string * @param name the name of the stream, for use in error messages */ - static Input* newStringInput(InputLanguage lang, const std::string& input, const std::string& name) + static Input* newStringInput(InputLanguage lang, + const std::string& input, + const std::string& name) throw (InputStreamException); public: diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index b2bb15a6a..a9b3c461d 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -52,31 +52,37 @@ public: } };*/ -ParserBuilder::ParserBuilder(InputLanguage lang, const std::string& filename) : +ParserBuilder::ParserBuilder(ExprManager& exprManager, const std::string& filename) : d_inputType(FILE_INPUT), - d_lang(lang), + d_lang(LANG_AUTO), d_filename(filename), - d_exprManager(NULL), + d_streamInput(NULL), + d_exprManager(exprManager), d_checksEnabled(true), d_strictMode(false), d_mmap(false) { } -Parser *ParserBuilder::build() throw (InputStreamException) { +Parser *ParserBuilder::build() throw (InputStreamException,AssertionException) { Input *input; switch( d_inputType ) { case FILE_INPUT: input = Input::newFileInput(d_lang,d_filename,d_mmap); break; + case STREAM_INPUT: + AlwaysAssert( d_streamInput != NULL, + "Uninitialized stream input in ParserBuilder::build()" ); + input = Input::newStreamInput(d_lang,*d_streamInput,d_filename); + break; case STRING_INPUT: input = Input::newStringInput(d_lang,d_stringInput,d_filename); break; } switch(d_lang) { case LANG_SMTLIB_V2: - return new Smt2(d_exprManager, input, d_strictMode); + return new Smt2(&d_exprManager, input, d_strictMode); default: - return new Parser(d_exprManager, input, d_strictMode); + return new Parser(&d_exprManager, input, d_strictMode); } } @@ -115,6 +121,27 @@ ParserBuilder& ParserBuilder::withChecks(bool flag) { return *this; } +ParserBuilder& ParserBuilder::withExprManager(ExprManager& exprManager) { + d_exprManager = exprManager; + return *this; +} + +ParserBuilder& ParserBuilder::withFileInput() { + d_inputType = FILE_INPUT; + return *this; +} + +ParserBuilder& ParserBuilder::withFilename(const std::string& filename) { + d_filename = filename; + return *this; +} + +ParserBuilder& ParserBuilder::withInputLanguage(InputLanguage lang) { + d_lang = lang; + return *this; +} + + ParserBuilder& ParserBuilder::withMmap(bool flag) { d_mmap = flag; return *this; @@ -125,8 +152,9 @@ ParserBuilder& ParserBuilder::withStrictMode(bool flag) { return *this; } -ParserBuilder& ParserBuilder::withExprManager(ExprManager& exprManager) { - d_exprManager = &exprManager; +ParserBuilder& ParserBuilder::withStreamInput(std::istream& input) { + d_inputType = STREAM_INPUT; + d_streamInput = &input; return *this; } diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index d0b8b7bb2..92b44a82d 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -45,9 +45,15 @@ public: class Parser; +/** + * A builder for input language parsers. <code>build()</code> can be + * called any number of times on an instance and will generate a fresh + * parser each time. + */ class CVC4_PUBLIC ParserBuilder { enum InputType { FILE_INPUT, + STREAM_INPUT, STRING_INPUT }; @@ -63,8 +69,11 @@ class CVC4_PUBLIC ParserBuilder { /** The string input, if any. */ std::string d_stringInput; + /** The stream input, if any. */ + std::istream *d_streamInput; + /** The expression manager */ - ExprManager *d_exprManager; + ExprManager& d_exprManager; /** Should semantic checks be enabled during parsing? */ bool d_checksEnabled; @@ -76,12 +85,43 @@ class CVC4_PUBLIC ParserBuilder { bool d_mmap; public: - ParserBuilder(InputLanguage lang, const std::string& filename); - Parser *build() throw (InputStreamException); + + /** Create a parser builder using the given ExprManager and filename. */ + ParserBuilder(ExprManager& exprManager, const std::string& filename); + + /** Build the parser, using the current settings. */ + Parser *build() throw (InputStreamException,AssertionException); + + /** Should semantic checks be enabled in the parser? (Default: yes) */ ParserBuilder& withChecks(bool flag = true); + + /** Set the ExprManager to use with the parser. */ + ParserBuilder& withExprManager(ExprManager& exprManager); + + /** Set the parser to read a file for its input. (Default) */ + ParserBuilder& withFileInput(); + + /** Set the filename for use by the parser. If file input is used, + * this file will be opened and read by the parser. Otherwise, the + * filename string (possibly a non-existent path) will only be used + * in error messages. */ + ParserBuilder& withFilename(const std::string& filename); + + /** Set the input language to be used by the parser. (Default: + LANG_AUTO). */ + ParserBuilder& withInputLanguage(InputLanguage lang); + + /** Should the parser memory-map its input? This is only relevant if + * the parser will have a file input. (Default: no) */ ParserBuilder& withMmap(bool flag = true); + + /** Should the parser use strict mode? (Default: no) */ ParserBuilder& withStrictMode(bool flag = true); - ParserBuilder& withExprManager(ExprManager& exprManager); + + /** Set the parser to use the given stream for its input. */ + ParserBuilder& withStreamInput(std::istream& input); + + /** Set the parser to use the given string for its input. */ ParserBuilder& withStringInput(const std::string& input); }; diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index d76d8ba38..f6089382c 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -145,6 +145,8 @@ void Smt2::setLogic(const std::string& name) { case AUFNIRA: case QF_AUFBV: case QF_AUFLIA: + case QF_AX: + case QF_BV: Unhandled(name); } } |