diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index 81f4ad08f8..d8290576a4 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/jbmc/src/java_bytecode/java_class_loader.cpp @@ -88,17 +88,16 @@ void java_class_loadert::add_classpath_entry(const std::string &path) /// \return optional value of parse tree, empty if class cannot be loaded optionalt java_class_loadert::get_class_from_jar( const irep_idt &class_name, - const std::string &jar_file, - const jar_indext &jar_index) + const std::string &jar_file) { - auto jar_index_it = jar_index.find(class_name); - if(jar_index_it == jar_index.end()) + auto classes = read_jar_file(jar_file); + if(!classes.has_value()) return {}; debug() << "Getting class `" << class_name << "' from JAR " << jar_file << eom; - auto data = jar_pool(jar_file).get_entry(jar_index_it->second); + auto data = jar_pool(jar_file).get_entry(class_name_to_jar_file(class_name)); if(!data.has_value()) return {}; @@ -137,7 +136,7 @@ java_class_loadert::get_parse_tree( PRECONDITION(parse_trees.empty()); // do we refuse to load? - if(!class_loader_limit.load_class_file(class_name_to_file(class_name))) + if(!class_loader_limit.load_class_file(class_name_to_jar_file(class_name))) { debug() << "not loading " << class_name << " because of limit" << eom; java_bytecode_parse_treet parse_tree; @@ -153,11 +152,8 @@ java_class_loadert::get_parse_tree( { case classpath_entryt::JAR: { - jar_index_optcreft index = read_jar_file(cp_entry.path); - if(!index) - continue; optionalt parse_tree = - get_class_from_jar(class_name, cp_entry.path, *index); + get_class_from_jar(class_name, cp_entry.path); if(parse_tree) parse_trees.emplace_back(std::move(*parse_tree)); } @@ -166,7 +162,7 @@ java_class_loadert::get_parse_tree( case classpath_entryt::DIRECTORY: { // Look in the given directory - const std::string class_file = class_name_to_file(class_name); + const std::string class_file = class_name_to_os_file(class_name); const std::string full_path = #ifdef _WIN32 cp_entry.path + '\\' + class_file; @@ -243,33 +239,24 @@ java_class_loadert::get_parse_tree( std::vector java_class_loadert::load_entire_jar( const std::string &jar_path) { - jar_index_optcreft jar_index = read_jar_file(jar_path); - if(!jar_index) + auto classes = read_jar_file(jar_path); + if(!classes.has_value()) return {}; classpath_entries.push_front( classpath_entryt(classpath_entryt::JAR, jar_path)); - std::vector classes; - - for(const auto &e : jar_index->get()) - { - operator()(e.first); - classes.push_back(e.first); - } + for(const auto &c : *classes) + operator()(c); classpath_entries.pop_front(); - return classes; + return *classes; } -java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file( - const std::string &jar_path) +optionalt> +java_class_loadert::read_jar_file(const std::string &jar_path) { - auto existing_it = jars_by_path.find(jar_path); - if(existing_it != jars_by_path.end()) - return std::cref(existing_it->second); - std::vector filenames; try { @@ -278,13 +265,13 @@ java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file( catch(const std::runtime_error &) { error() << "failed to open JAR file `" << jar_path << "'" << eom; - return jar_index_optcreft(); + return {}; } debug() << "Adding JAR file `" << jar_path << "'" << eom; // Create a new entry in the map and initialize using the list of file names // that are in jar_filet - jar_indext &jar_index = jars_by_path[jar_path]; + std::vector classes; for(auto &file_name : filenames) { if(has_suffix(file_name, ".class")) @@ -293,10 +280,10 @@ java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file( << "Found class file " << file_name << " in JAR `" << jar_path << "'" << eom; irep_idt class_name=file_to_class_name(file_name); - jar_index[class_name] = file_name; + classes.push_back(class_name); } } - return std::cref(jar_index); + return classes; } /// Convert a file name to the class name. Java interprets folders as packages, @@ -336,7 +323,27 @@ std::string java_class_loadert::file_to_class_name(const std::string &file) /// file_to_class_name. /// \param class_name: the name of the class /// \return the class name converted to file name -std::string java_class_loadert::class_name_to_file(const irep_idt &class_name) +std::string +java_class_loadert::class_name_to_jar_file(const irep_idt &class_name) +{ + std::string result = id2string(class_name); + + // dots (package name separators) to slash + for(std::string::iterator it = result.begin(); it != result.end(); it++) + if(*it == '.') + *it = '/'; + + // add .class suffix + result += ".class"; + + return result; +} + +/// Convert a class name to a file name, with OS-dependent syntax +/// \param class_name: the name of the class +/// \return the class name converted to file name +std::string +java_class_loadert::class_name_to_os_file(const irep_idt &class_name) { std::string result=id2string(class_name); diff --git a/jbmc/src/java_bytecode/java_class_loader.h b/jbmc/src/java_bytecode/java_class_loader.h index f1eaf1b7ff..5eccca936c 100644 --- a/jbmc/src/java_bytecode/java_class_loader.h +++ b/jbmc/src/java_bytecode/java_class_loader.h @@ -27,10 +27,6 @@ Author: Daniel Kroening, kroening@kroening.com class java_class_loadert:public messaget { public: - /// A map associating logical class names with the name of the .class file - /// implementing it for all classes inside a single JAR file - typedef std::map jar_indext; - /// A list of parse trees supporting overlay classes typedef std::list parse_tree_with_overlayst; /// A map from class names to list of parse tree where multiple entries can @@ -95,14 +91,11 @@ public: void add_classpath_entry(const std::string &); static std::string file_to_class_name(const std::string &); - static std::string class_name_to_file(const irep_idt &); + static std::string class_name_to_os_file(const irep_idt &); + static std::string class_name_to_jar_file(const irep_idt &); std::vector load_entire_jar(const std::string &jar_path); - const jar_indext &get_jar_index(const std::string &jar_path) - { - return jars_by_path.at(jar_path); - } /// Map from class names to the bytecode parse trees fixed_keys_map_wrappert get_class_with_overlays_map() @@ -146,22 +139,13 @@ private: std::vector java_load_classes; get_extra_class_refs_functiont get_extra_class_refs; - /// The jar_indext for each jar file we've read - std::map jars_by_path; - /// Map from class names to the bytecode parse trees parse_tree_with_overridest_mapt class_map; - typedef optionalt> - jar_index_optcreft; + optionalt> read_jar_file(const std::string &jar_path); - jar_index_optcreft read_jar_file( - const std::string &jar_path); - - optionalt get_class_from_jar( - const irep_idt &class_name, - const std::string &jar_file, - const jar_indext &jar_index); + optionalt + get_class_from_jar(const irep_idt &class_name, const std::string &jar_file); }; #endif // CPROVER_JAVA_BYTECODE_JAVA_CLASS_LOADER_H