Merge pull request diffblue#2765 from diffblue/jar_pool

factor out jar pool class

Author: Daniel Kroening

jbmc/src/java_bytecode/Makefile

@@ -6,6 +6,7 @@ SRC = bytecode_info.cpp \
       expr2java.cpp \
       generic_parameter_specialization_map_keys.cpp \
       jar_file.cpp \
+      jar_pool.cpp \
       java_bytecode_convert_class.cpp \
       java_bytecode_convert_method.cpp \
       java_bytecode_concurrency_instrumentation.cpp \

jbmc/src/java_bytecode/jar_pool.cpp

@@ -0,0 +1,39 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#include "jar_pool.h"
+#include "jar_file.h"
+
+jar_filet &jar_poolt::operator()(const std::string &file_name)
+{
+  const auto it = m_archives.find(file_name);
+  if(it == m_archives.end())
+  {
+    // VS: Can't construct in place
+    auto file = jar_filet(file_name);
+    return m_archives.emplace(file_name, std::move(file)).first->second;
+  }
+  else
+    return it->second;
+}
+
+jar_filet &jar_poolt::add_jar(
+  const std::string &buffer_name,
+  const void *pmem,
+  size_t size)
+{
+  const auto it = m_archives.find(buffer_name);
+  if(it == m_archives.end())
+  {
+    // VS: Can't construct in place
+    auto file = jar_filet(pmem, size);
+    return m_archives.emplace(buffer_name, std::move(file)).first->second;
+  }
+  else
+    return it->second;
+}

jbmc/src/java_bytecode/jar_pool.h

@@ -0,0 +1,40 @@
+/*******************************************************************\
+
+Module:
+
+Author: Daniel Kroening, [email protected]
+
+\*******************************************************************/
+
+#ifndef CPROVER_JAVA_BYTECODE_JAR_POOL_H
+#define CPROVER_JAVA_BYTECODE_JAR_POOL_H
+
+#include <map>
+#include <string>
+
+class jar_filet;
+
+/// A chache for jar_filet objects, by file name
+class jar_poolt
+{
+public:
+  /// Load jar archive or retrieve from cache if already loaded
+  /// \param jar_path name of the file
+  // Throws an exception if the file does not exist
+  jar_filet &operator()(const std::string &jar_path);
+
+  /// Add a jar archive or retrieve from cache if already added
+  /// \param buffer_name name of the original file
+  /// \param pmem memory pointer to the contents of the file
+  /// \param size size of the memory buffer
+  /// Note that this mocks the existence of a file which may
+  /// or may not exist since  the actual data bis retrieved from memory.
+  jar_filet &
+  add_jar(const std::string &buffer_name, const void *pmem, size_t size);
+
+protected:
+  /// Jar files that have been loaded
+  std::map<std::string, jar_filet> m_archives;
+};
+
+#endif // CPROVER_JAVA_BYTECODE_JAVA_CLASS_LOADER_H

jbmc/src/java_bytecode/java_class_loader.cpp

@@ -252,7 +252,7 @@ java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file(
   std::vector<std::string> filenames;
   try
   {
-    filenames = this->jar_pool(jar_path).filenames();
+    filenames = jar_pool(jar_path).filenames();
   }
   catch(const std::runtime_error &)
   {
@@ -325,33 +325,3 @@ std::string java_class_loadert::class_name_to_file(const irep_idt &class_name)
 
   return result;
 }
-
-jar_filet &java_class_loadert::jar_pool(
-  const std::string &file_name)
-{
-  const auto it=m_archives.find(file_name);
-  if(it==m_archives.end())
-  {
-    // VS: Can't construct in place
-    auto file = jar_filet(file_name);
-    return m_archives.emplace(file_name, std::move(file)).first->second;
-  }
-  else
-    return it->second;
-}
-
-jar_filet &java_class_loadert::jar_pool(
-  const std::string &buffer_name,
-  const void *pmem,
-  size_t size)
-{
-  const auto it=m_archives.find(buffer_name);
-  if(it==m_archives.end())
-  {
-    // VS: Can't construct in place
-    auto file = jar_filet(pmem, size);
-    return m_archives.emplace(buffer_name, std::move(file)).first->second;
-  }
-  else
-    return it->second;
-}

jbmc/src/java_bytecode/java_class_loader.h

@@ -17,9 +17,10 @@ Author: Daniel Kroening, [email protected]
 #include <util/message.h>
 #include <util/fixed_keys_map_wrapper.h>
 
+#include "jar_file.h"
+#include "jar_pool.h"
 #include "java_bytecode_parse_tree.h"
 #include "java_class_loader_limit.h"
-#include "jar_file.h"
 
 class java_class_loadert:public messaget
 {
@@ -99,20 +100,8 @@ class java_class_loadert:public messaget
     return class_map.at(class_name).front();
   }
 
-  /// Load jar archive or retrieve from cache if already loaded
-  /// \param filename name of the file
-  jar_filet &jar_pool(const std::string &filename);
-
-  /// Load jar archive or retrieve from cache if already loaded
-  /// \param buffer_name name of the original file
-  /// \param pmem memory pointer to the contents of the file
-  /// \param size size of the memory buffer
-  /// Note that this mocks the existence of a file which may
-  /// or may not exist since  the actual data bis retrieved from memory.
-  jar_filet &jar_pool(
-    const std::string &buffer_name,
-    const void *pmem,
-    size_t size);
+  /// a cache for jar_filet, by path name
+  jar_poolt jar_pool;
 
 private:
   /// Either a regular expression matching files that will be allowed to be
@@ -134,8 +123,6 @@ class java_class_loadert:public messaget
   /// The jar_indext for each jar file we've read
   std::map<std::string, jar_indext> jars_by_path;
 
-  /// Jar files that have been loaded
-  std::map<std::string, jar_filet> m_archives;
   /// Map from class names to the bytecode parse trees
   parse_tree_with_overridest_mapt class_map;