Merge pull request #1251 from LAJW/refactor/jar_file

Refactor, fix and document jar_filet class

Author: peterschrammel

src/java_bytecode/Makefile

@@ -25,6 +25,7 @@ SRC = bytecode_info.cpp \
       java_string_library_preprocess.cpp \
       java_types.cpp \
       java_utils.cpp \
+      mz_zip_archive.cpp \
       select_pointer_type.cpp \
       # Empty last line
 

src/java_bytecode/jar_file.cpp

@@ -1,144 +1,100 @@
 /*******************************************************************\
 
-Module:
+Module: Jar file reader
 
-Author: Daniel Kroening, [email protected]
+Author: Diffblue Ltd
 
 \*******************************************************************/
 
 #include "jar_file.h"
-
-#include <cstring>
-#include <unordered_set>
-
-#include <json/json_parser.h>
+#include <cctype>
 #include <util/suffix.h>
 #include <util/invariant.h>
+#include "java_class_loader_limit.h"
 
-void jar_filet::open(
-  java_class_loader_limitt &class_loader_limit,
-  const std::string &filename)
+jar_filet::jar_filet(
+  java_class_loader_limitt &limit,
+  const std::string &filename):
+  m_zip_archive(filename)
 {
-  if(!mz_ok)
+  const size_t file_count=m_zip_archive.get_num_files();
+  for(size_t index=0; index<file_count; index++)
   {
-    memset(&zip, 0, sizeof(zip));
-    mz_bool mz_open=mz_zip_reader_init_file(&zip, filename.c_str(), 0);
-    mz_ok=mz_open==MZ_TRUE;
+    const auto filename=m_zip_archive.get_filename(index);
+    if(!has_suffix(filename, ".class") || limit.load_class_file(filename))
+      m_name_to_index.emplace(filename, index);
   }
+}
 
-  if(mz_ok)
-  {
-    std::size_t number_of_files=
-      mz_zip_reader_get_num_files(&zip);
-
-    for(std::size_t i=0; i<number_of_files; i++)
-    {
-      // get the length of the filename, including the trailing \0
-      mz_uint filename_length=mz_zip_reader_get_filename(&zip, i, nullptr, 0);
-      std::vector<char> filename_char(filename_length+1);
-      INVARIANT(filename_length>=1, "buffer size must include trailing \\0");
+// VS: No default move constructors or assigns
 
-      // read and convert to std::string
-      mz_uint filename_len=
-        mz_zip_reader_get_filename(
-          &zip, i, filename_char.data(), filename_length);
-      INVARIANT(
-        filename_length==filename_len,
-        "buffer size was incorrectly pre-computed");
-      std::string file_name(filename_char.data());
-#if DEBUG
-      debug()
-        << "jar_filet.open: idx " << i
-        << " len " << filename_len
-        << " filename '" << std::string(filename_char.data()) << "'" << eom;
-#endif
-      INVARIANT(file_name.size()==filename_len-1, "no \\0 found in file name");
+jar_filet::jar_filet(jar_filet &&other):
+  m_zip_archive(std::move(other.m_zip_archive)),
+  m_name_to_index((other.m_name_to_index)) {}
 
-      // non-class files are loaded in any case
-      bool add_file=!has_suffix(file_name, ".class");
-      // load .class file only if they match regex / are in match set
-      add_file|=class_loader_limit.load_class_file(file_name);
-      if(add_file)
-      {
-        if(has_suffix(file_name, ".class"))
-          status() << "read class file " << file_name
-                   << " from " << filename << eom;
-        filtered_jar[file_name]=i;
-      }
-    }
-  }
+jar_filet &jar_filet::operator=(jar_filet &&other)
+{
+  m_zip_archive=std::move(other.m_zip_archive);
+  m_name_to_index=std::move(other.m_name_to_index);
+  return *this;
 }
 
-jar_filet::~jar_filet()
+std::string jar_filet::get_entry(const std::string &name)
 {
-  if(mz_ok)
+  const auto entry=m_name_to_index.find(name);
+  INVARIANT(entry!=m_name_to_index.end(), "File doesn't exist");
+  try
+  {
+    return m_zip_archive.extract(entry->second);
+  }
+  catch(const std::runtime_error &)
   {
-    mz_zip_reader_end(&zip);
-    mz_ok=false;
+    return "";
   }
 }
 
-std::string jar_filet::get_entry(const irep_idt &name)
+static bool is_space(const char ch)
 {
-  if(!mz_ok)
-    return std::string("");
-
-  std::string dest;
-
-  auto entry=filtered_jar.find(name);
-  assert(entry!=filtered_jar.end());
-
-  size_t real_index=entry->second;
-  mz_zip_archive_file_stat file_stat;
-  memset(&file_stat, 0, sizeof(file_stat));
-  mz_bool stat_ok=mz_zip_reader_file_stat(&zip, real_index, &file_stat);
-  if(stat_ok!=MZ_TRUE)
-    return std::string();
-  std::vector<char> buffer;
-  size_t bufsize=file_stat.m_uncomp_size;
-  buffer.resize(bufsize);
-  mz_bool read_ok=
-    mz_zip_reader_extract_to_mem(&zip, real_index, buffer.data(), bufsize, 0);
-  if(read_ok!=MZ_TRUE)
-    return std::string();
-
-  dest.insert(dest.end(), buffer.begin(), buffer.end());
-
-  return dest;
+  return std::isspace(ch);
 }
 
-jar_filet::manifestt jar_filet::get_manifest()
+/// Remove leading and trailing whitespace characters from string
+static std::string trim(
+  const std::string::const_iterator begin,
+  const std::string::const_iterator end)
 {
-  auto entry=filtered_jar.find("META-INF/MANIFEST.MF");
-  if(entry==filtered_jar.end())
-    return manifestt();
-
-  std::string dest=get_entry(entry->first);
-  std::istringstream in(dest);
-
-  manifestt manifest;
+  const auto out_begin=std::find_if_not(begin, end, is_space);
+  const auto out_end=std::find_if_not(
+    std::string::const_reverse_iterator(end),
+    std::string::const_reverse_iterator(out_begin),
+    is_space).base();
+  return { out_begin, out_end };
+}
 
-  std::string line;
-  while(std::getline(in, line))
+std::unordered_map<std::string, std::string> jar_filet::get_manifest()
+{
+  std::unordered_map<std::string, std::string> out;
+  const auto entry=m_name_to_index.find("META-INF/MANIFEST.MF");
+  if(entry!=m_name_to_index.end())
   {
-    std::size_t pos=line.find(':');
-    if(pos==std::string::npos)
-      continue;
-    std::string key=line.substr(0, pos);
-
-    // skip spaces
-    pos++;
-    while(pos<line.size() && line[pos]==' ') pos++;
-
-    std::string value=line.substr(pos, std::string::npos);
-
-    // trim off \r
-    if(!value.empty() && *value.rbegin()=='\r')
-      value.resize(value.size()-1);
-
-    // store
-    manifest[key]=value;
+    std::istringstream in(this->get_entry(entry->first));
+    std::string line;
+    while(std::getline(in, line))
+    {
+      const auto key_end=std::find(line.cbegin(), line.cend(), ':');
+      if(key_end!=line.cend())
+        out.emplace(
+          trim(line.cbegin(), key_end),
+          trim(std::next(key_end), line.cend()));
+    }
   }
+  return out;
+}
 
-  return manifest;
+std::vector<std::string> jar_filet::filenames() const
+{
+  std::vector<std::string> out;
+  for(const auto &pair : m_name_to_index)
+    out.emplace_back(pair.first);
+  return out;
 }

src/java_bytecode/jar_file.h

@@ -1,110 +1,48 @@
 /*******************************************************************\
 
-Module: JAR File Reading
+Module: Jar file reader
 
-Author: Daniel Kroening, [email protected]
+Author: Diffblue Ltd
 
 \*******************************************************************/
 
-/// \file
-/// JAR File Reading
-
 #ifndef CPROVER_JAVA_BYTECODE_JAR_FILE_H
 #define CPROVER_JAVA_BYTECODE_JAR_FILE_H
 
-#define _LARGEFILE64_SOURCE 1
-#include "miniz/miniz.h"
-
+#include <unordered_map>
+#include <memory>
 #include <string>
 #include <vector>
-#include <map>
-#include <regex>
-#include <util/message.h>
+#include "mz_zip_archive.h"
 
-#include "java_class_loader_limit.h"
+class java_class_loader_limitt;
 
-/// An in-memory representation of a JAR file, consisting of a handler to a zip
-/// file (field \ref zip) and a map from file names inside the zip file to the
-/// index they occupy in the root directory (field \ref filtered_jar).
-///
-/// Both fields are initialize by a call to open(). Method get_entry() reads a
-/// file from the zip and returns it.
-class jar_filet:public messaget
+/// Class representing a .jar archive
+class jar_filet final
 {
 public:
-  jar_filet():
-    mz_ok(false)
-    // `zip` will be initialized by open()
-  {
-  }
-
-  ~jar_filet();
-
-  /// Initializes \ref zip to store the JAR file pointed by \p filepath and
-  /// loads the map \ref filtered_jar with the .class names allowed by \p limit.
-  void open(java_class_loader_limitt &limit, const std::string &filepath);
-
-  /// Test for error; 'true' means we are good.
-  explicit operator bool() const { return mz_ok; }
-
-  /// Reads the \ref zip field and returns a string storing the data contained
-  /// in file \p name.
-  std::string get_entry(const irep_idt &name);
-
-  /// Maps the names of the files stored in the JAR file to the index they
-  /// occupy (starting from 0) in the JAR central directory.  Populated by
-  /// method open() above.
-  typedef std::map<irep_idt, size_t> filtered_jart;
-  filtered_jart filtered_jar;
-
-  typedef std::map<std::string, std::string> manifestt;
-  manifestt get_manifest();
-
-protected:
-  /// A handle representing the zip file
-  mz_zip_archive zip;
-
-  /// True iff the \ref zip field has been correctly initialized with a JAR file
-  bool mz_ok;
-};
-
-/// A pool of jar_filet objects, indexed by the filesystem path name used to
-/// load that jar_filet.
-///
-/// The state of the class is maintained by the field \ref file_map, a std::map
-/// associating the path of a .jar file with its in-memory representation.
-/// A call to
-///
-/// ```
-///   operator()(limit, path)
-/// ```
-///
-/// will either return a previously loaded jar_filet, if it is found in the map,
-/// or will load that file (using jar_filet::open) and return a newly created
-/// jar_filet.
-class jar_poolt:public messaget
-{
-public:
-  jar_filet &operator()(
-    java_class_loader_limitt &class_loader_limit,
-    const std::string &file_name)
-  {
-    file_mapt::iterator it=file_map.find(file_name);
-    if(it==file_map.end())
-    {
-      jar_filet &jar_file=file_map[file_name];
-      jar_file.set_message_handler(get_message_handler());
-      jar_file.open(class_loader_limit, file_name);
-      return jar_file;
-    }
-    else
-      return file_map[file_name];
-  }
-
-protected:
-  /// A map from filesystem paths to jar_filet objects
-  typedef std::map<std::string, jar_filet> file_mapt;
-  file_mapt file_map;
+  /// Open java file for reading
+  /// \param limit Object limiting number of loaded .class files
+  /// \param filename Name of the file
+  /// \throw Throws std::runtime_error if file cannot be opened
+  jar_filet(java_class_loader_limitt &limit, const std::string &filename);
+  jar_filet(const jar_filet &)=delete;
+  jar_filet &operator=(const jar_filet &)=delete;
+  jar_filet(jar_filet &&);
+  jar_filet &operator=(jar_filet &&);
+  ~jar_filet()=default;
+  /// Get contents of a file in the jar archive.
+  /// Terminates the program if file doesn't exist
+  /// \param filename Name of the file in the archive
+  std::string get_entry(const std::string &filename);
+  /// Get contents of the Manifest file in the jar archive
+  std::unordered_map<std::string, std::string> get_manifest();
+  /// Get list of filenames in the archive
+  std::vector<std::string> filenames() const;
+private:
+  mz_zip_archivet m_zip_archive;
+  /// Map of filename to the file index in the zip archive
+  std::unordered_map<std::string, size_t> m_name_to_index;
 };
 
 #endif // CPROVER_JAVA_BYTECODE_JAR_FILE_H

src/java_bytecode/java_bytecode_language.cpp

@@ -138,8 +138,7 @@ bool java_bytecode_languaget::parse(
       java_cp_include_files);
     if(config.java.main_class.empty())
     {
-      // load the .jar file and retrieve its manifest
-      jar_filet::manifestt manifest=
+      auto manifest=
         java_class_loader.jar_pool(class_loader_limit, path).get_manifest();
       std::string manifest_main_class=manifest["Main-Class"];