From 05239e9bdf31d848ff073334d26a790de5412e03 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 13 May 2021 09:49:33 -0700 Subject: [PATCH] Always parse streams with line buffer (#6532) When cvc5 was compiled in competition mode (but not for the application track), then it had a special behavior when reading from stdin. When it received input from stdin, it would read all of stdin and then parse the input as a string because it assumed that the full input is directly available on stdin. However, the non-application tracks of SMT-COMP do not use stdin anymore. They pass a filename to the solver. This special case is not used as a result. Usually, cvc5 parses from stdin using the line buffer, so this commit makes it so that this is always the case, which simplifies the code. --- src/main/driver_unified.cpp | 8 ----- src/parser/antlr_input.cpp | 58 +++-------------------------------- src/parser/antlr_input.h | 3 +- src/parser/input.cpp | 7 ++--- src/parser/input.h | 3 +- src/parser/parser_builder.cpp | 10 ------ src/parser/parser_builder.h | 4 --- 7 files changed, 10 insertions(+), 83 deletions(-) diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 9b0ea4759..f27bf03f0 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -263,11 +263,7 @@ int runCvc5(int argc, char* argv[], Options& opts) opts); if( inputFromStdin ) { -#if defined(CVC5_COMPETITION_MODE) && !defined(CVC5_SMTCOMP_APPLICATION_TRACK) parserBuilder.withStreamInput(cin); -#else /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */ - parserBuilder.withLineBufferedStreamInput(cin); -#endif /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */ } vector< vector > allCommands; @@ -419,11 +415,7 @@ int runCvc5(int argc, char* argv[], Options& opts) opts); if( inputFromStdin ) { -#if defined(CVC5_COMPETITION_MODE) && !defined(CVC5_SMTCOMP_APPLICATION_TRACK) parserBuilder.withStreamInput(cin); -#else /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */ - parserBuilder.withLineBufferedStreamInput(cin); -#endif /* CVC5_COMPETITION_MODE && !CVC5_SMTCOMP_APPLICATION_TRACK */ } std::unique_ptr parser(parserBuilder.build()); diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index de90ee14b..73d1b89b5 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -16,7 +16,7 @@ #include "parser/antlr_input.h" #include -#include +#include #include "base/check.h" #include "base/output.h" @@ -152,61 +152,13 @@ AntlrInputStream::newFileInputStream(const std::string& name, return new AntlrInputStream(name, input, false, NULL, NULL); } - -AntlrInputStream* -AntlrInputStream::newStreamInputStream(std::istream& input, - const std::string& name, - bool lineBuffered) +AntlrInputStream* AntlrInputStream::newStreamInputStream( + std::istream& input, const std::string& name) { pANTLR3_INPUT_STREAM inputStream = NULL; pANTLR3_UINT8 inputStringCopy = NULL; - LineBuffer* line_buffer = NULL; - - if(lineBuffered) { - line_buffer = new LineBuffer(&input); - inputStream = newAntlr3BufferedStream(input, name, line_buffer); - } else { - - // Since these are all NULL on entry, realloc will be called - char *basep = NULL, *boundp = NULL, *cp = NULL; - /* 64KB seems like a reasonable default size. */ - size_t bufSize = 0x10000; - - /* Keep going until we can't go no more. */ - while( !input.eof() && !input.fail() ) { - - if( cp == boundp ) { - /* We ran out of room in the buffer. Realloc at double the size. */ - ptrdiff_t offset = cp - basep; - basep = (char *) realloc(basep, bufSize); - if( basep == NULL ) { - throw InputStreamException("Failed buffering input stream: " + name); - } - cp = basep + offset; - boundp = basep + bufSize; - bufSize *= 2; - } - - /* Read as much as we have room for. */ - input.read( cp, boundp - cp ); - cp += input.gcount(); - } - - /* Make sure the fail bit didn't get set. */ - if( !input.eof() ) { - throw InputStreamException("Stream input failed: " + name); - } - ptrdiff_t offset = cp - basep; - Assert(offset >= 0); - Assert(offset <= std::numeric_limits::max()); - inputStringCopy = (pANTLR3_UINT8)basep; - inputStream = newAntrl3InPlaceStream(inputStringCopy, (uint32_t) offset, name); - } - - if( inputStream == NULL ) { - throw InputStreamException("Couldn't initialize input: " + name); - } - + LineBuffer* line_buffer = new LineBuffer(&input); + inputStream = newAntlr3BufferedStream(input, name, line_buffer); return new AntlrInputStream(name, inputStream, false, inputStringCopy, line_buffer); } diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 5fcf853cc..c74962188 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -77,8 +77,7 @@ public: /** Create an input from an istream. */ static AntlrInputStream* newStreamInputStream(std::istream& input, - const std::string& name, - bool lineBuffered = false); + const std::string& name); /** Create a string input. * NOTE: the new AntlrInputStream will take ownership of input over diff --git a/src/parser/input.cpp b/src/parser/input.cpp index cfb418fbe..4c88978de 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -62,11 +62,10 @@ Input* Input::newFileInput(InputLanguage lang, Input* Input::newStreamInput(InputLanguage lang, std::istream& input, - const std::string& name, - bool lineBuffered) + const std::string& name) { - AntlrInputStream *inputStream = - AntlrInputStream::newStreamInputStream(input, name, lineBuffered); + AntlrInputStream* inputStream = + AntlrInputStream::newStreamInputStream(input, name); return AntlrInput::newInput(lang, *inputStream); } diff --git a/src/parser/input.h b/src/parser/input.h index 47453e367..1821bc034 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -115,8 +115,7 @@ class CVC5_EXPORT Input */ static Input* newStreamInput(InputLanguage lang, std::istream& input, - const std::string& name, - bool lineBuffered = false); + const std::string& name); /** Create an input for the given string * diff --git a/src/parser/parser_builder.cpp b/src/parser/parser_builder.cpp index ad3b69f7e..220edb9d5 100644 --- a/src/parser/parser_builder.cpp +++ b/src/parser/parser_builder.cpp @@ -75,10 +75,6 @@ Parser* ParserBuilder::build() case FILE_INPUT: input = Input::newFileInput(d_lang, d_filename, d_mmap); break; - case LINE_BUFFERED_STREAM_INPUT: - Assert(d_streamInput != NULL); - input = Input::newStreamInput(d_lang, *d_streamInput, d_filename, true); - break; case STREAM_INPUT: Assert(d_streamInput != NULL); input = Input::newStreamInput(d_lang, *d_streamInput, d_filename); @@ -204,12 +200,6 @@ ParserBuilder& ParserBuilder::withStreamInput(std::istream& input) { return *this; } -ParserBuilder& ParserBuilder::withLineBufferedStreamInput(std::istream& input) { - d_inputType = LINE_BUFFERED_STREAM_INPUT; - d_streamInput = &input; - return *this; -} - ParserBuilder& ParserBuilder::withStringInput(const std::string& input) { d_inputType = STRING_INPUT; d_stringInput = input; diff --git a/src/parser/parser_builder.h b/src/parser/parser_builder.h index 5d73fedfa..b43da3548 100644 --- a/src/parser/parser_builder.h +++ b/src/parser/parser_builder.h @@ -46,7 +46,6 @@ class CVC5_EXPORT ParserBuilder { enum InputType { FILE_INPUT, - LINE_BUFFERED_STREAM_INPUT, STREAM_INPUT, STRING_INPUT }; @@ -177,9 +176,6 @@ class CVC5_EXPORT ParserBuilder /** Set the parser to use the given stream for its input. */ ParserBuilder& withStreamInput(std::istream& input); - /** Set the parser to use the given stream for its input. */ - ParserBuilder& withLineBufferedStreamInput(std::istream& input); - /** Set the parser to use the given string for its input. */ ParserBuilder& withStringInput(const std::string& input); -- 2.30.2