diff --git a/jbmc/src/java_bytecode/Makefile b/jbmc/src/java_bytecode/Makefile index c3964a40375..5d4e734a0e5 100644 --- a/jbmc/src/java_bytecode/Makefile +++ b/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 \ diff --git a/jbmc/src/java_bytecode/jar_pool.cpp b/jbmc/src/java_bytecode/jar_pool.cpp new file mode 100644 index 00000000000..5e72ffb0454 --- /dev/null +++ b/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; +} diff --git a/jbmc/src/java_bytecode/jar_pool.h b/jbmc/src/java_bytecode/jar_pool.h new file mode 100644 index 00000000000..2216688bb80 --- /dev/null +++ b/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 +#include + +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 m_archives; +}; + +#endif // CPROVER_JAVA_BYTECODE_JAVA_CLASS_LOADER_H diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index 215e6739f9b..562527ba552 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/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 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; -} diff --git a/jbmc/src/java_bytecode/java_class_loader.h b/jbmc/src/java_bytecode/java_class_loader.h index ed389a4d03b..61125c9e904 100644 --- a/jbmc/src/java_bytecode/java_class_loader.h +++ b/jbmc/src/java_bytecode/java_class_loader.h @@ -17,9 +17,10 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#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 jars_by_path; - /// Jar files that have been loaded - std::map m_archives; /// Map from class names to the bytecode parse trees parse_tree_with_overridest_mapt class_map;