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 1b33f5ac6774d49299ed6460f023cdbd680f80e4..49ddfbc29d072c55471a86b625fa8dce6143f1ed 100644 (file)
--- 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<api::Solver>& 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 5552a677d29ad2a9e7b6d81ad2c0dca81aae28c4..254c994867f78a7f605ef9d86d2f2ac148a0dcd5 100644 (file)
--- 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 bfa577304d8e33f112cc6f994b21a7f420035c4f..bed10969560b21061be04720a7ca37bec48b9829 100644 (file)
--- 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 236eb534c7b0facf8634d73fe917cae1f60861b3..1402ed7bb11e02d63429169020c364667ed0ac27 100644 (file)
--- 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 7799d279dbea8cdbe2e10e5e2457fe2bd79ec8be..10306822e85e2b14747007f0e319282857f0b231 100644 (file)
--- 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 <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);
 
   /** 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 0fb44b4a9e268586c4113f22a89120a022916267..237c97bdde962f0f7bf25b0d48409f3a9221921b 100644 (file)
--- 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 7d7254339d8e0d18de9369f1068dfcf3828dc689..ab732e3000c98681e4b25df9537fa5eb6b626856 100644 (file)
--- 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 (file)
index 44e85bc..0000000
--- 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 <fcntl.h>
-#include <stdio.h>
-
-#include <antlr3input.h>
-
-#ifndef _WIN32
-
-#include <cerrno>
-#include <sys/mman.h>
-#include <sys/stat.h>
-
-#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 (file)
index a420ecc..0000000
--- 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 <antlr3input.h>
-#include <string>
-
-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 d68f5f5db3f3b73478a00eb9589704cc7580b6e2..97e6406f8ffb96c9296a2b7c19e33698e0c135ee 100644 (file)
--- 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> 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> 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);