From: Andres Noetzli Date: Mon, 28 Feb 2022 19:21:16 +0000 (-0800) Subject: Remove broken/unused `--mmap` option (#8178) X-Git-Tag: cvc5-1.0.0~365 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6b459fe9160bd8fc4f94fde7ccd6c7fae116c178;p=cvc5.git Remove broken/unused `--mmap` option (#8178) Fixes #2705. This commit removes the broken and unused --mmap option. Given that we are planning to change to a different parser at some point, it is not worth attempting to fix the option. --- diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp index 1b33f5ac6..49ddfbc29 100644 --- a/src/main/driver_unified.cpp +++ b/src/main/driver_unified.cpp @@ -214,9 +214,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr& solver) else { parser->setInput( - Input::newFileInput(solver->getOption("input-language"), - filename, - solver->getOptionInfo("mmap").boolValue())); + Input::newFileInput(solver->getOption("input-language"), filename)); } bool interrupted = false; diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml index 5552a677d..254c99486 100644 --- a/src/options/parser_options.toml +++ b/src/options/parser_options.toml @@ -8,13 +8,6 @@ name = "Parser" type = "bool" help = "be less tolerant of non-conforming inputs" -[[option]] - name = "memoryMap" - category = "regular" - long = "mmap" - type = "bool" - help = "memory map file input" - [[option]] name = "semanticChecks" long = "semantic-checks" diff --git a/src/parser/CMakeLists.txt b/src/parser/CMakeLists.txt index bfa577304..bed109695 100644 --- a/src/parser/CMakeLists.txt +++ b/src/parser/CMakeLists.txt @@ -35,8 +35,6 @@ set(libcvc5parser_src_files input.h line_buffer.cpp line_buffer.h - memory_mapped_input_buffer.cpp - memory_mapped_input_buffer.h parse_op.cpp parse_op.h parser.cpp diff --git a/src/parser/antlr_input.cpp b/src/parser/antlr_input.cpp index 236eb534c..1402ed7bb 100644 --- a/src/parser/antlr_input.cpp +++ b/src/parser/antlr_input.cpp @@ -24,7 +24,6 @@ #include "parser/bounded_token_buffer.h" #include "parser/bounded_token_factory.h" #include "parser/input.h" -#include "parser/memory_mapped_input_buffer.h" #include "parser/parser.h" #include "parser/parser_exception.h" #include "parser/smt2/smt2_input.h" @@ -127,24 +126,11 @@ 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) { -#ifdef _WIN32 - if(useMmap) { - useMmap = false; - } -#endif - pANTLR3_INPUT_STREAM input = NULL; - if(useMmap) { - input = MemoryMappedInputBufferNew(name); - } else { - input = newAntlr3FileStream(name); - } - if(input == NULL) { + pANTLR3_INPUT_STREAM input = newAntlr3FileStream(name); + if (input == nullptr) + { throw InputStreamException("Couldn't open file: " + name); } return new AntlrInputStream(name, input, false, NULL, NULL); diff --git a/src/parser/antlr_input.h b/src/parser/antlr_input.h index 7799d279d..10306822e 100644 --- a/src/parser/antlr_input.h +++ b/src/parser/antlr_input.h @@ -69,11 +69,8 @@ public: /** Create a file input. * * @param name the path of the file to read - * @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); /** Create an input from an istream. */ static AntlrInputStream* newStreamInputStream(std::istream& input, diff --git a/src/parser/input.cpp b/src/parser/input.cpp index 0fb44b4a9..237c97bdd 100644 --- a/src/parser/input.cpp +++ b/src/parser/input.cpp @@ -50,12 +50,10 @@ InputStream *Input::getInputStream() { return d_inputStream; } -Input* Input::newFileInput(const std::string& lang, - const std::string& filename, - bool useMmap) +Input* Input::newFileInput(const std::string& lang, const std::string& filename) { - AntlrInputStream *inputStream = - AntlrInputStream::newFileInputStream(filename, useMmap); + AntlrInputStream* inputStream = + AntlrInputStream::newFileInputStream(filename); return AntlrInput::newInput(lang, *inputStream); } diff --git a/src/parser/input.h b/src/parser/input.h index 7d7254339..ab732e300 100644 --- a/src/parser/input.h +++ b/src/parser/input.h @@ -98,11 +98,9 @@ class CVC5_EXPORT Input * * @param lang the input language * @param filename the input filename - * @param useMmap true if the parser should use memory-mapped I/O (default: false) */ static Input* newFileInput(const std::string& lang, - const std::string& filename, - bool useMmap = false); + const std::string& filename); /** Create an input for the given stream. * diff --git a/src/parser/memory_mapped_input_buffer.cpp b/src/parser/memory_mapped_input_buffer.cpp deleted file mode 100644 index 44e85bc90..000000000 --- a/src/parser/memory_mapped_input_buffer.cpp +++ /dev/null @@ -1,134 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Christopher L. Conway, Morgan Deters, Tim King - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * [[ Add file-specific comments here ]]. - * - * [[ Add file-specific comments here ]] - */ - -#include -#include - -#include - -#ifndef _WIN32 - -#include -#include -#include - -#endif /* _WIN32 */ - -#include "base/exception.h" -#include "parser/memory_mapped_input_buffer.h" - -namespace cvc5 { -namespace parser { - -extern "C" { - -#ifdef _WIN32 - -pANTLR3_INPUT_STREAM MemoryMappedInputBufferNew(const std::string& filename) { - return 0; -} - -#else /* ! _WIN32 */ - -static ANTLR3_UINT32 -MemoryMapFile(pANTLR3_INPUT_STREAM input, const std::string& filename); - -void -UnmapFile(pANTLR3_INPUT_STREAM input); - -pANTLR3_INPUT_STREAM MemoryMappedInputBufferNew(const std::string& filename) { - // Pointer to the input stream we are going to create - // - pANTLR3_INPUT_STREAM input; - ANTLR3_UINT32 status; - - // Allocate memory for the input stream structure - // - input = (pANTLR3_INPUT_STREAM) ANTLR3_CALLOC(1, sizeof(ANTLR3_INPUT_STREAM)); - - if(input == NULL) { - return NULL; - } - - // Structure was allocated correctly, now we can read the file. - // - status = MemoryMapFile(input, filename); - - // Call the common 8 bit ASCII input stream handler - // Initializer type thingy doobry function. - // -#ifdef CVC5_ANTLR3_OLD_INPUT_STREAM - antlr3AsciiSetupStream(input, ANTLR3_CHARSTREAM); -#else /* CVC5_ANTLR3_OLD_INPUT_STREAM */ - antlr38BitSetupStream(input); -#endif /* CVC5_ANTLR3_OLD_INPUT_STREAM */ - - // Now we can set up the file name - // - input->istream->streamName - = input->strFactory->newStr(input->strFactory, - (uint8_t*) filename.c_str()); - input->fileName = input->istream->streamName; - input->free = UnmapFile; - - if(status != ANTLR3_SUCCESS) { - input->close(input); - return NULL; - } - - return input; -} - -static ANTLR3_UINT32 MemoryMapFile(pANTLR3_INPUT_STREAM input, - const std::string& filename) { - errno = 0; - struct stat st; - if(stat(filename.c_str(), &st) == -1) { - return ANTLR3_ERR_NOFILE; - } - - input->sizeBuf = st.st_size; - - int fd = open(filename.c_str(), O_RDONLY); - if(fd == -1) { - return ANTLR3_ERR_NOFILE; - } - - input->data = mmap(0, input->sizeBuf, PROT_READ, MAP_PRIVATE, fd, 0); - errno = 0; - close(fd); - if(intptr_t(input->data) == -1) { - return ANTLR3_ERR_NOMEM; - } - - return ANTLR3_SUCCESS; -} - -/* This is a bit shady. antlr3AsciiSetupStream has free and close as aliases. - * We need to unmap the file somewhere, so we install this function as free and - * call the default version of close to de-allocate everything else. */ -void UnmapFile(pANTLR3_INPUT_STREAM input) { - munmap((void*) input->data, input->sizeBuf); - input->close(input); -} - -#endif /* _WIN32 */ - -}/* extern "C" */ - -} // namespace parser -} // namespace cvc5 diff --git a/src/parser/memory_mapped_input_buffer.h b/src/parser/memory_mapped_input_buffer.h deleted file mode 100644 index a420eccbf..000000000 --- a/src/parser/memory_mapped_input_buffer.h +++ /dev/null @@ -1,41 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Mathias Preiner, Christopher L. Conway - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * ANTLR input buffer from a memory-mapped file. - */ - -#include "cvc5parser_private.h" - -#ifndef CVC5__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H -#define CVC5__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H - -#include -#include - -namespace cvc5 { -namespace parser { - -#ifdef __cplusplus -extern "C" { -#endif - -pANTLR3_INPUT_STREAM -MemoryMappedInputBufferNew(const std::string& filename); - -#ifdef __cplusplus -}/* extern "C" */ -#endif - -} // namespace parser -} // namespace cvc5 - -#endif /* CVC5__PARSER__MEMORY_MAPPED_INPUT_BUFFER_H */ diff --git a/test/unit/parser/parser_builder_black.cpp b/test/unit/parser/parser_builder_black.cpp index d68f5f5db..97e6406f8 100644 --- a/test/unit/parser/parser_builder_black.cpp +++ b/test/unit/parser/parser_builder_black.cpp @@ -78,7 +78,7 @@ TEST_F(TestParseBlackParserBuilder, empty_file_input) std::unique_ptr parser(ParserBuilder(&d_solver, d_symman.get(), false) .withInputLanguage("LANG_SMTLIB_V2_6") .build()); - parser->setInput(Input::newFileInput("LANG_SMTLIB_V2_6", filename, false)); + parser->setInput(Input::newFileInput("LANG_SMTLIB_V2_6", filename)); checkEmptyInput(parser.get()); remove(filename); @@ -96,7 +96,7 @@ TEST_F(TestParseBlackParserBuilder, simple_file_input) std::unique_ptr parser(ParserBuilder(&d_solver, d_symman.get(), false) .withInputLanguage("LANG_SMTLIB_V2_6") .build()); - parser->setInput(Input::newFileInput("LANG_SMTLIB_V2_6", filename, false)); + parser->setInput(Input::newFileInput("LANG_SMTLIB_V2_6", filename)); checkInput(parser.get(), "(set-logic ALL)\n"); remove(filename);