factor out pool for JARs into jar_poolt

Author: 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, kroening@kroening.com
+
+\*******************************************************************/
+
+#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, kroening@kroening.com
+
+\*******************************************************************/
+
+#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