Switch from custom file / path routines to Boost-filesystem

For the time being this means building boost-fs and boost-system at
configure time; as of C++17 these functions will be in libstdc++.

Author: smowton

src/CMakeLists.txt

@@ -61,6 +61,7 @@ macro(generic_includes name)
         ${CBMC_SOURCE_DIR}
         ${CMAKE_CURRENT_BINARY_DIR}
         ${CMAKE_CURRENT_SOURCE_DIR}
+        ${boost_include_include_dir}
     )
 endmacro(generic_includes)
 

src/cbmc/CMakeLists.txt

@@ -24,6 +24,9 @@ target_link_libraries(cbmc-lib
     solvers
     util
     xml
+
+    boost_filesystem
+    boost_system
 )
 
 add_if_library(cbmc-lib bv_refinement)

src/goto-analyzer/CMakeLists.txt

@@ -19,6 +19,9 @@ target_link_libraries(goto-analyzer-lib
     json
     assembler
     util
+
+    boost_filesystem
+    boost_system
 )
 
 add_if_library(goto-analyzer-lib java_bytecode)

src/goto-instrument/CMakeLists.txt

@@ -10,6 +10,8 @@ add_library(goto-instrument-lib ${sources})
 
 generic_includes(goto-instrument-lib)
 
+
+
 target_link_libraries(goto-instrument-lib
     ansi-c
     cpp
@@ -25,6 +27,9 @@ target_link_libraries(goto-instrument-lib
     util
     json
     solvers
+
+    boost_filesystem
+    boost_system
 )
 
 add_if_library(goto-instrument-lib java_bytecode)

src/goto-instrument/goto_instrument_parse_options.cpp

@@ -15,6 +15,8 @@ Author: Daniel Kroening, [email protected]
 #include <iostream>
 #include <memory>
 
+#include <boost/filesystem.hpp>
+
 #include <util/config.h>
 #include <util/string2int.h>
 #include <util/unicode.h>
@@ -136,15 +138,15 @@ int goto_instrument_parse_optionst::doit()
     // Here we only early-check for requirements and we handle the option later.
     const std::string out_json_file_pathname=
       cmdline.get_value("save-code-statistics");
-    if(fileutl_is_directory(out_json_file_pathname))
+    if(boost::filesystem::is_directory(out_json_file_pathname))
     {
       error() << "The path-name '" << out_json_file_pathname
               << "'passed to the option '--save-code-statistics' "
                 "represents an existing directory."
               << eom;
       return 12;
     }
-    if(fileutl_parse_extension_in_pathname(out_json_file_pathname)!=".json")
+    if(boost::filesystem::path(out_json_file_pathname).extension() != ".json")
     {
       error() << "The file of the path-name '" << out_json_file_pathname
               << "'passed to the option '--save-code-statistics' does "
@@ -790,11 +792,11 @@ int goto_instrument_parse_optionst::doit()
       stats.extend(goto_model);
       const std::string out_json_file_pathname=
         cmdline.get_value("save-code-statistics");
-      INVARIANT(!fileutl_is_directory(out_json_file_pathname),
+      INVARIANT(!boost::filesystem::is_directory(out_json_file_pathname),
                 "The early check passed so the JSON file indeed should not be "
                   " a directory.");
       INVARIANT(
-        fileutl_parse_extension_in_pathname(out_json_file_pathname)==".json",
+        boost::filesystem::path(out_json_file_pathname).extension() == ".json",
         "The early check passed so the JSON file indeed should have "
           "'.json' extension.");
       std::ofstream ofile(out_json_file_pathname);

src/jbmc/CMakeLists.txt

@@ -25,6 +25,9 @@ target_link_libraries(jbmc-lib
     solvers
     util
     xml
+
+    boost_filesystem
+    boost_system
 )
 
 add_if_library(jbmc-lib bv_refinement)

src/util/file_util.cpp

@@ -156,226 +156,6 @@ std::string concat_dir_file(
 #endif
 }
 
-static std::string::size_type fileutl_parse_last_dir_pos(
-  std::string const &file_pathname)
-{
-  auto found = file_pathname.find_last_of("/\\");
-  if(found == std::string::npos)
-    return 0;
-  else
-    return found + 1;
-}
-
-bool fileutl_file_exists(std::string const &pathname)
-{
-  std::ifstream f{pathname, std::ios::binary};
-  return f.good();
-}
-
-bool fileutl_is_directory(std::string const &pathname)
-{
-  if(!fileutl_file_exists(pathname))
-    return false;
-# if defined(WIN32)
-  return PathIsDirectory(pathname.c_str());
-# elif defined(__linux__) || defined(__APPLE__)
-  struct stat buf;
-  stat(pathname.c_str(), &buf);
-  return S_ISDIR(buf.st_mode);
-# else
-#   error "Unsuported platform."
-# endif
-}
-
-uint64_t fileutl_file_size(std::string const &file_pathname)
-{
-  std::ifstream f{file_pathname, std::ios::binary};
-  std::streampos const begin = f.tellg();
-  f.seekg(0ULL, std::ios::end);
-  std::streampos const end = f.tellg();
-  return end - begin;
-}
-
-std::string fileutl_parse_name_in_pathname(std::string const &file_pathname)
-{
-  return file_pathname.substr(fileutl_parse_last_dir_pos(file_pathname));
-}
-
-std::string fileutl_parse_extension_in_pathname(const std::string &pathname)
-{
-  const std::size_t idx=pathname.find_last_of('.');
-# if defined(WIN32)
-  const std::size_t fwd_slash_idx=pathname.find_last_of('/');
-  const std::size_t bwd_slash_idx=pathname.find_last_of('\\');
-  const std::size_t slash_idx=
-    fwd_slash_idx==std::string::npos ? bwd_slash_idx :
-    bwd_slash_idx==std::string::npos ? fwd_slash_idx :
-      std::max(fwd_slash_idx, bwd_slash_idx);
-# elif defined(__linux__) || defined(__APPLE__)
-  const std::size_t slash_idx=pathname.find_last_of('/');
-# else
-#   error "Unsuported platform."
-# endif
-  return
-    idx==std::string::npos || (slash_idx!=std::string::npos && idx<slash_idx) ?
-      std::string() : pathname.substr(idx);
-}
-
-std::string fileutl_parse_path_in_pathname(std::string const &file_pathname)
-{
-  return file_pathname.substr(0U, fileutl_parse_last_dir_pos(file_pathname));
-}
-
-std::string fileutl_remove_extension(std::string const &filename)
-{
-  return filename.substr(0U, filename.find_last_of('.'));
-}
-
-void fileutl_create_directory(std::string const &pathname)
-{
-# if defined(WIN32)
-  char path_sep='\\';
-#else
-  char path_sep='/';
-#endif
-  std::size_t search_from=0;
-  while(search_from!=std::string::npos)
-  {
-    // Search from after the previous path separator, incidentally
-    // skipping trying to create '/' if an absolute path is given
-    search_from=pathname.find(path_sep, search_from+1);
-    std::string truncated_pathname=pathname.substr(0, search_from);
-#if defined(WIN32)
-    _mkdir(truncated_pathname.c_str());
-#else
-    mkdir(truncated_pathname.c_str(), 0777);
-#endif
-    // Ignore return-- regardless of why we can't create a
-    // path prefix, we might as well keep trying down to more
-    // specific paths.
-  }
-}
-
-std::string fileutl_concatenate_file_paths(
-  std::string const &left_path,
-  std::string const &right_path)
-{
-  if(left_path.empty())
-    return right_path;
-  if(right_path.empty())
-    return left_path;
-  return left_path + "/" + right_path;
-}
-
-std::string fileutl_absolute_path(std::string const &path)
-{
-#if defined(WIN32)
-  DWORD buffer_length = GetFullPathName(path.c_str(), 0, nullptr, nullptr);
-  std::vector<char> buffer(buffer_length);
-  DWORD actual_length =
-    GetFullPathName(path.c_str(), buffer_length, &(buffer[0]), nullptr);
-  if(actual_length != buffer_length - 1)
-    throw "fileutl_absolute_path: GetFullPathName failed";
-  return std::string(&(buffer[0]));
-#else
-  char *absolute = realpath(path.c_str(), nullptr);
-  if(absolute==NULL)
-  {
-    std::string error=std::strerror(errno);
-    throw std::ios::failure("Could not resolve absolute path ("+error+")");
-  }
-  std::string ret(absolute);
-  free(absolute);
-  return ret;
-#endif
-}
-
-std::string fileutl_normalise_path(std::string const &path)
-{
-  std::string result = path;
-  std::replace(result.begin(), result.end(), '\\', '/');
-  std::string::size_type pos = 0ULL;
-  while((pos = result.find("//", 0)) != std::string::npos)
-    result.replace(pos, 2, "/");
-  while((pos = result.find("/./", 0)) != std::string::npos)
-    result.replace(pos, 3, "/");
-  while((pos = result.find("/../", 0)) != std::string::npos)
-  {
-    assert(pos != 0ULL);
-    const std::string::size_type prev_pos = result.rfind("/", pos-1ULL);
-    if(prev_pos == std::string::npos)
-      break;
-    result.replace(prev_pos, pos - prev_pos + 4ULL, "/");
-  }
-  return result;
-}
-
-void fileutl_split_pathname(
-  std::string const &pathname,
-  std::vector<std::string> &output)
-{
-  std::istringstream istr(fileutl_normalise_path(pathname));
-  std::string token;
-  while(std::getline(istr, token, '/'))
-    output.push_back(token);
-}
-
-std::string fileutl_join_path_parts(std::vector<std::string> const &parts)
-{
-  if(parts.empty())
-    return "";
-  std::string result = parts.at(0);
-  for(uint64_t i = 1ULL; i < parts.size(); ++i)
-  {
-    result.push_back('/');
-    result.append(parts.at(i));
-  }
-  return result;
-}
-
-std::string fileutl_get_common_prefix(
-  std::string const &pathname1,
-  std::string const &pathname2)
-{
-  std::vector<std::string>  split1;
-  fileutl_split_pathname(pathname1, split1);
-
-  std::vector<std::string>  split2;
-  fileutl_split_pathname(pathname2, split2);
-
-  std::vector<std::string>  common_split;
-  for(uint64_t i = 0ULL, size = std::min(split1.size(), split2.size());
-      i < size && split1.at(i) == split2.at(i);
-      ++i)
-    common_split.push_back(split1.at(i));
-
-  std::string const result = fileutl_join_path_parts(common_split);
-  return result;
-}
-
-std::string fileutl_get_relative_path(
-  std::string const &pathname,
-  std::string const &directory)
-{
-  std::vector<std::string>  split1;
-  fileutl_split_pathname(pathname, split1);
-  std::reverse(split1.begin(), split1.end());
-
-  std::vector<std::string>  split2;
-  fileutl_split_pathname(directory, split2);
-  std::reverse(split2.begin(), split2.end());
-
-  while(!split1.empty() && !split2.empty() && split1.back() == split2.back())
-  {
-    split1.pop_back();
-    split2.pop_back();
-  }
-
-  std::reverse(split1.begin(), split1.end());
-  std::string const result = fileutl_join_path_parts(split1);
-  return result;
-}
-
 /// Replaces invalid characters in a file name using a hard-coded list of
 /// replacements.
 /// This is not designed to operate on path names and will replace folder

src/util/file_util.h

@@ -11,59 +11,13 @@ Author: Daniel Kroening, [email protected]
 #define CPROVER_UTIL_FILE_UTIL_H
 
 #include <string>
-#include <vector>
-#include <cstdint>
-#include <iosfwd>
 
 void delete_directory(const std::string &path);
 
 std::string get_current_working_directory();
 
-std::string concat_dir_file(
-  const std::string &directory,
-  const std::string &file_name);
-
-/// These functions provide us disc-related functionality, like manipulation
-/// with disc paths (concatenation/splitting), checking for existence of files,
-/// etc.
-
-bool fileutl_file_exists(std::string const &pathname);
-
-bool fileutl_is_directory(std::string const &pathname);
-
-uint64_t fileutl_file_size(std::string const &file_pathname);
-
-std::string fileutl_parse_name_in_pathname(std::string const &file_pathname);
-
-std::string fileutl_parse_extension_in_pathname(const std::string &pathname);
-
-std::string fileutl_parse_path_in_pathname(std::string const &file_pathname);
-
-std::string fileutl_remove_extension(std::string const &filename);
-
-void fileutl_create_directory(std::string const &pathname);
-
-std::string fileutl_concatenate_file_paths(
-  std::string const &left_path,
-  std::string const &right_path);
-
-std::string fileutl_absolute_path(std::string const &path);
-
-std::string fileutl_normalise_path(std::string const &path);
-
-void fileutl_split_pathname(
-  std::string const &pathname,
-  std::vector<std::string>& output);
-
-std::string fileutl_join_path_parts(std::vector<std::string> const &parts);
-
-std::string fileutl_get_common_prefix(
-  std::string const &pathname1,
-  std::string const &pathname2);
-
-std::string fileutl_get_relative_path(
-  std::string const &pathname,
-  std::string const &directory);
+std::string concat_dir_file(const std::string &directory,
+                            const std::string &file_name);
 
 std::string make_valid_filename(std::string filename);