From 5dbd48c6cceb35aef7f3f2119d460d8f3a7dc03b Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 20 Aug 2018 13:50:52 +0100 Subject: [PATCH 1/3] unify jar list and classpath --- .../java_bytecode/java_bytecode_language.cpp | 8 +++++- .../java_bytecode/java_bytecode_language.h | 7 ++--- jbmc/src/java_bytecode/java_class_loader.cpp | 26 +++++++------------ jbmc/src/java_bytecode/java_class_loader.h | 18 ++++++++----- 4 files changed, 32 insertions(+), 27 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_language.cpp b/jbmc/src/java_bytecode/java_bytecode_language.cpp index e72ad355529..ba0a347c236 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_language.cpp @@ -185,6 +185,12 @@ bool java_bytecode_languaget::parse( const std::string &path) { PRECONDITION(language_options_initialized); + + java_class_loader.clear_classpath(); + + for(const auto &p : config.java.classpath) + java_class_loader.add_classpath_entry(p); + java_class_loader.set_message_handler(get_message_handler()); java_class_loader.set_java_cp_include_files(java_cp_include_files); java_class_loader.add_load_classes(java_load_classes); @@ -232,7 +238,7 @@ bool java_bytecode_languaget::parse( main_jar_classes.push_back(kv.first); } else - java_class_loader.add_jar_file(path); + java_class_loader.add_classpath_entry(path); } else UNREACHABLE; diff --git a/jbmc/src/java_bytecode/java_bytecode_language.h b/jbmc/src/java_bytecode/java_bytecode_language.h index 20885ed689c..e25e4fc21b4 100644 --- a/jbmc/src/java_bytecode/java_bytecode_language.h +++ b/jbmc/src/java_bytecode/java_bytecode_language.h @@ -123,13 +123,14 @@ class java_bytecode_languaget:public languaget lazy_methods_mode(lazy_methods_modet::LAZY_METHODS_MODE_EAGER), string_refinement_enabled(false), pointer_type_selector(std::move(pointer_type_selector)) - {} + { + } java_bytecode_languaget(): java_bytecode_languaget( std::unique_ptr(new select_pointer_typet())) - {} - + { + } bool from_expr( const exprt &expr, diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index 562527ba552..41a6ad2672a 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/jbmc/src/java_bytecode/java_class_loader.cpp @@ -13,7 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com #include #include -#include #include "java_bytecode_parser.h" @@ -69,6 +68,11 @@ java_class_loadert::parse_tree_with_overlayst &java_class_loadert::operator()( return class_map.at(class_name); } +void java_class_loadert::add_classpath_entry(const std::string &path) +{ + classpath_entries.push_back(path); +} + optionalt java_class_loadert::get_class_from_jar( const irep_idt &class_name, const std::string &jar_file, @@ -124,20 +128,8 @@ java_class_loadert::get_parse_tree( return parse_trees; } - // First add all given JAR files - for(const auto &jar_file : jar_files) - { - jar_index_optcreft index = read_jar_file(jar_file); - if(!index) - continue; - optionalt parse_tree = - get_class_from_jar(class_name, jar_file, *index); - if(parse_tree) - parse_trees.emplace_back(std::move(*parse_tree)); - } - - // Then add everything on the class path - for(const auto &cp_entry : config.java.classpath) + // Rummage through the class path + for(const auto &cp_entry : classpath_entries) { if(has_suffix(cp_entry, ".jar")) { @@ -234,12 +226,12 @@ void java_class_loadert::load_entire_jar( if(!jar_index) return; - jar_files.push_front(jar_path); + classpath_entries.push_front(jar_path); for(const auto &e : jar_index->get()) operator()(e.first); - jar_files.pop_front(); + classpath_entries.pop_front(); } java_class_loadert::jar_index_optcreft java_class_loadert::read_jar_file( diff --git a/jbmc/src/java_bytecode/java_class_loader.h b/jbmc/src/java_bytecode/java_class_loader.h index 61125c9e904..fb7bca5d15f 100644 --- a/jbmc/src/java_bytecode/java_class_loader.h +++ b/jbmc/src/java_bytecode/java_class_loader.h @@ -74,11 +74,19 @@ class java_class_loadert:public messaget for(const auto &id : classes) java_load_classes.push_back(id); } - void add_jar_file(const std::string &f) + + /// Clear all classpath entries + void clear_classpath() { - jar_files.push_back(f); + classpath_entries.clear(); } + /// Appends an entry to the class path, used for loading classes. The + /// argument may be + /// 1) The name of a directory, used for searching for .class files + /// 2) The name of a JAR file + 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 &); @@ -111,10 +119,8 @@ class java_class_loadert:public messaget /// information. std::string java_cp_include_files; - /// List of filesystem paths to .jar files that will be used, in the given - /// order, to find and load a class, provided its name (see \ref - /// get_parse_tree). - std::list jar_files; + /// List of entries in the classpath + std::list classpath_entries; /// Classes to be explicitly loaded std::vector java_load_classes; From ba7e06ff8b271b9fa0189ed401e5181128f36c5c Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Mon, 20 Aug 2018 14:13:58 +0100 Subject: [PATCH 2/3] precompute the category of the classpath entry --- jbmc/src/java_bytecode/java_class_loader.cpp | 73 ++++++++++++-------- jbmc/src/java_bytecode/java_class_loader.h | 15 +++- 2 files changed, 57 insertions(+), 31 deletions(-) diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index 41a6ad2672a..16122fbec90 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/jbmc/src/java_bytecode/java_class_loader.cpp @@ -70,7 +70,15 @@ java_class_loadert::parse_tree_with_overlayst &java_class_loadert::operator()( void java_class_loadert::add_classpath_entry(const std::string &path) { - classpath_entries.push_back(path); + if(has_suffix(path, ".jar")) + { + classpath_entries.push_back(classpath_entryt(classpath_entryt::JAR, path)); + } + else + { + classpath_entries.push_back( + classpath_entryt(classpath_entryt::DIRECTORY, path)); + } } optionalt java_class_loadert::get_class_from_jar( @@ -131,40 +139,44 @@ java_class_loadert::get_parse_tree( // Rummage through the class path for(const auto &cp_entry : classpath_entries) { - if(has_suffix(cp_entry, ".jar")) - { - jar_index_optcreft index = read_jar_file(cp_entry); - if(!index) - continue; - optionalt parse_tree = - get_class_from_jar(class_name, cp_entry, *index); - if(parse_tree) - parse_trees.emplace_back(std::move(*parse_tree)); - } - else + switch(cp_entry.kind) { - // Look in the given directory - const std::string class_file = class_name_to_file(class_name); - const std::string full_path = - #ifdef _WIN32 - cp_entry + '\\' + class_file; - #else - cp_entry + '/' + class_file; - #endif - - if(!class_loader_limit.load_class_file(class_file)) - continue; - - if(std::ifstream(full_path)) + case classpath_entryt::JAR: { - debug() - << "Getting class `" << class_name << "' from file " << full_path - << eom; + jar_index_optcreft index = read_jar_file(cp_entry.path); + if(!index) + continue; optionalt parse_tree = - java_bytecode_parse(full_path, get_message_handler()); + get_class_from_jar(class_name, cp_entry.path, *index); if(parse_tree) parse_trees.emplace_back(std::move(*parse_tree)); } + break; + + case classpath_entryt::DIRECTORY: + { + // Look in the given directory + const std::string class_file = class_name_to_file(class_name); + const std::string full_path = +#ifdef _WIN32 + cp_entry.path + '\\' + class_file; +#else + cp_entry.path + '/' + class_file; +#endif + + if(!class_loader_limit.load_class_file(class_file)) + continue; + + if(std::ifstream(full_path)) + { + debug() << "Getting class `" << class_name << "' from file " + << full_path << eom; + optionalt parse_tree = + java_bytecode_parse(full_path, get_message_handler()); + if(parse_tree) + parse_trees.emplace_back(std::move(*parse_tree)); + } + } } } @@ -226,7 +238,8 @@ void java_class_loadert::load_entire_jar( if(!jar_index) return; - classpath_entries.push_front(jar_path); + classpath_entries.push_front( + classpath_entryt(classpath_entryt::JAR, jar_path)); for(const auto &e : jar_index->get()) operator()(e.first); diff --git a/jbmc/src/java_bytecode/java_class_loader.h b/jbmc/src/java_bytecode/java_class_loader.h index fb7bca5d15f..8e83c2601ad 100644 --- a/jbmc/src/java_bytecode/java_class_loader.h +++ b/jbmc/src/java_bytecode/java_class_loader.h @@ -119,8 +119,21 @@ class java_class_loadert:public messaget /// information. std::string java_cp_include_files; + /// An entry in the classpath + struct classpath_entryt + { + using kindt = enum { JAR, DIRECTORY }; + kindt kind; + std::string path; + + classpath_entryt(kindt _kind, const std::string &_path) + : kind(_kind), path(_path) + { + } + }; + /// List of entries in the classpath - std::list classpath_entries; + std::list classpath_entries; /// Classes to be explicitly loaded std::vector java_load_classes; From 53b3c4a5f4e95dc80997d34f84c79f19130fc6a2 Mon Sep 17 00:00:00 2001 From: Daniel Kroening Date: Tue, 21 Aug 2018 12:16:33 +0100 Subject: [PATCH 3/3] remove redundant class loader limit test --- jbmc/src/java_bytecode/java_class_loader.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/jbmc/src/java_bytecode/java_class_loader.cpp b/jbmc/src/java_bytecode/java_class_loader.cpp index 16122fbec90..c035a327126 100644 --- a/jbmc/src/java_bytecode/java_class_loader.cpp +++ b/jbmc/src/java_bytecode/java_class_loader.cpp @@ -164,9 +164,6 @@ java_class_loadert::get_parse_tree( cp_entry.path + '/' + class_file; #endif - if(!class_loader_limit.load_class_file(class_file)) - continue; - if(std::ifstream(full_path)) { debug() << "Getting class `" << class_name << "' from file "