From: Christopher L. Conway Date: Thu, 3 Jun 2010 22:27:16 +0000 (+0000) Subject: Implementing input from stdin (Fixes: #144) X-Git-Tag: cvc5-1.0.0~9002 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f780dd882fc343cef668d5cd9eed8f515d0e70ed;p=cvc5.git Implementing input from stdin (Fixes: #144) --- 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 ? "" : 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 true 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 #include +#include #include #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. build() 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); } } diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index 1f283f476..0597de931 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -12,6 +12,7 @@ UNIT_TESTS = \ expr/attribute_black \ expr/declaration_scope_black \ parser/parser_black \ + parser/parser_builder_black \ prop/cnf_stream_black \ context/context_black \ context/context_white \ diff --git a/test/unit/parser/parser_black.h b/test/unit/parser/parser_black.h index 6f09820c5..f6d822265 100644 --- a/test/unit/parser/parser_black.h +++ b/test/unit/parser/parser_black.h @@ -1,5 +1,5 @@ /********************* */ -/** parser_white.h +/** parser_black.h ** Original author: cconway ** Major contributors: none ** Minor contributors (to current version): dejan, mdeters @@ -10,17 +10,18 @@ ** See the file COPYING in the top-level source directory for licensing ** information. ** - ** White box testing of CVC4::parser::SmtParser. + ** Black box testing of CVC4::parser::Parser, including CVC, SMT and + ** SMT v2 inputs. **/ #include -//#include #include #include "expr/expr.h" #include "expr/expr_manager.h" #include "parser/parser.h" #include "parser/parser_builder.h" +#include "parser/parser_options.h" #include "parser/smt2/smt2.h" #include "expr/command.h" #include "util/output.h" @@ -29,8 +30,6 @@ using namespace CVC4; using namespace CVC4::parser; using namespace std; - - class ParserBlack { InputLanguage d_lang; ExprManager *d_exprManager; @@ -62,10 +61,10 @@ protected: // Debug.on("parser-extra"); // cerr << "Testing good input: <<" << goodInput << ">>" << endl; // istringstream stream(goodInputs[i]); - ParserBuilder parserBuilder(d_lang,"test"); Parser *parser = - parserBuilder.withStringInput(goodInput) - .withExprManager(*d_exprManager) + ParserBuilder(*d_exprManager,"test") + .withStringInput(goodInput) + .withInputLanguage(d_lang) .build(); TS_ASSERT( !parser->done() ); Command* cmd; @@ -88,10 +87,11 @@ protected: void tryBadInput(const string badInput, bool strictMode = false) { // cerr << "Testing bad input: '" << badInput << "'\n"; // Debug.on("parser"); - ParserBuilder parserBuilder(d_lang,"test"); + Parser *parser = - parserBuilder.withStringInput(badInput) - .withExprManager(*d_exprManager) + ParserBuilder(*d_exprManager,"test") + .withStringInput(badInput) + .withInputLanguage(d_lang) .withStrictMode(strictMode) .build(); TS_ASSERT_THROWS @@ -109,11 +109,13 @@ protected: // cerr << "Testing good expr: '" << goodExpr << "'\n"; // Debug.on("parser"); // istringstream stream(context + goodBooleanExprs[i]); - ParserBuilder parserBuilder(d_lang,"test"); + Parser *parser = - parserBuilder.withStringInput(goodExpr) - .withExprManager(*d_exprManager) + ParserBuilder(*d_exprManager,"test") + .withStringInput(goodExpr) + .withInputLanguage(d_lang) .build(); + TS_ASSERT( !parser->done() ); setupContext(*parser); TS_ASSERT( !parser->done() ); @@ -142,10 +144,11 @@ protected: // Debug.on("parser"); // Debug.on("parser-extra"); // cout << "Testing bad expr: '" << badExpr << "'\n"; - ParserBuilder parserBuilder(d_lang,"test"); + Parser *parser = - parserBuilder.withStringInput(badExpr) - .withExprManager(*d_exprManager) + ParserBuilder(*d_exprManager,"test") + .withStringInput(badExpr) + .withInputLanguage(d_lang) .withStrictMode(strictMode) .build(); setupContext(*parser); diff --git a/test/unit/parser/parser_builder_black.h b/test/unit/parser/parser_builder_black.h new file mode 100644 index 000000000..f254580af --- /dev/null +++ b/test/unit/parser/parser_builder_black.h @@ -0,0 +1,150 @@ +/********************* */ +/** parser_builder_black.h + ** Original author: cconway + ** Major contributors: none + ** Minor contributors (to current version): dejan, mdeters + ** 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. + ** + ** Black box testing of CVC4::parser::ParserBuilder. + **/ + +#include +#include +#include +#include +#include +#include +#include +#include + +#include "expr/command.h" +#include "parser/parser.h" +#include "parser/parser_builder.h" +#include "parser/parser_options.h" + +typedef __gnu_cxx::stdio_filebuf filebuf_gnu; + +using namespace CVC4; +using namespace CVC4::parser; +using namespace std; + +class ParserBuilderBlack : public CxxTest::TestSuite { + + ExprManager *d_exprManager; + + void checkEmptyInput(ParserBuilder& builder) { + Parser *parser = builder.build(); + TS_ASSERT( parser != NULL ); + + Expr e = parser->nextExpression(); + TS_ASSERT( e.isNull() ); + + delete parser; + } + + void checkTrueInput(ParserBuilder& builder) { + Parser *parser = builder.build(); + TS_ASSERT( parser != NULL ); + + Expr e = parser->nextExpression(); + TS_ASSERT_EQUALS( e, d_exprManager->mkConst(true) ); + + e = parser->nextExpression(); + TS_ASSERT( e.isNull() ); + delete parser; + } + + char* mkTemp() { + char *filename = strdup("/tmp/testinput.XXXXXX"); + int fd = mkstemp(filename); + TS_ASSERT( fd != -1 ); + close(fd); + return filename; + } + +public: + + void setUp() { + d_exprManager = new ExprManager; + } + + void tearDown() { + delete d_exprManager; + } + + void testEmptyFileInput() { + char *filename = mkTemp(); + + /* FILE *fp = tmpfile(); */ + /* filebuf_gnu fs( fd, ios_base::out ); */ + + /* ptr = tmpnam(filename); */ + /* std::fstream fs( ptr, fstream::out ); */ + /* fs.close(); */ + + checkEmptyInput( + ParserBuilder(*d_exprManager,filename) + .withInputLanguage(LANG_CVC4) + ); + + remove(filename); + // mkfifo(ptr, S_IWUSR | s_IRUSR); + } + + void testSimpleFileInput() { + char *filename = mkTemp(); + + std::fstream fs( filename, fstream::out ); + fs << "TRUE" << std::endl; + fs.close(); + + checkTrueInput( + ParserBuilder(*d_exprManager,filename) + .withInputLanguage(LANG_CVC4) + ); + + remove(filename); + } + + void testEmptyStringInput() { + checkEmptyInput( + ParserBuilder(*d_exprManager,"foo") + .withInputLanguage(LANG_CVC4) + .withStringInput("") + ); + } + + void testTrueStringInput() { + checkTrueInput( + ParserBuilder(*d_exprManager,"foo") + .withInputLanguage(LANG_CVC4) + .withStringInput("TRUE") + ); + } + + void testEmptyStreamInput() { + stringstream ss( "", ios_base::in ); + checkEmptyInput( + ParserBuilder(*d_exprManager,"foo") + .withInputLanguage(LANG_CVC4) + .withStreamInput(ss) + ); + } + + void testTrueStreamInput() { + stringstream ss( "TRUE", ios_base::in ); + checkTrueInput( + ParserBuilder(*d_exprManager,"foo") + .withInputLanguage(LANG_CVC4) + .withStreamInput(ss) + ); + } + + + +}; // class ParserBuilderBlack