diff --git a/src/java_bytecode/ci_lazy_methods.cpp b/src/java_bytecode/ci_lazy_methods.cpp index 6fb16600d92..14e51502868 100644 --- a/src/java_bytecode/ci_lazy_methods.cpp +++ b/src/java_bytecode/ci_lazy_methods.cpp @@ -17,20 +17,33 @@ #include - +/// Constructor for lazy-method loading +/// \param symbol_table: the symbol table to use +/// \param main_class: identifier of the entry point / main class +/// \param main_jar_classes: specify main class of jar if \p main_class is empty +/// \param lazy_methods_extra_entry_points: entry point functions to use +/// \param java_class_loader: the Java class loader to use +/// \param extra_needed_classes: list of class identifiers which are considered +/// to be required and therefore their methods should not be removed via +/// `lazy-methods`. Example of use: `ArrayList` as general implementation for +/// `List` interface. +/// \param pointer_type_selector: selector to handle correct pointer types +/// \param message_handler: the message handler to use for output ci_lazy_methodst::ci_lazy_methodst( const symbol_tablet &symbol_table, const irep_idt &main_class, const std::vector &main_jar_classes, const std::vector &lazy_methods_extra_entry_points, java_class_loadert &java_class_loader, + const std::vector &extra_needed_classes, const select_pointer_typet &pointer_type_selector, - message_handlert &message_handler): - messaget(message_handler), + message_handlert &message_handler) + : messaget(message_handler), main_class(main_class), main_jar_classes(main_jar_classes), lazy_methods_extra_entry_points(lazy_methods_extra_entry_points), java_class_loader(java_class_loader), + extra_needed_classes(extra_needed_classes), pointer_type_selector(pointer_type_selector) { // build the class hierarchy @@ -279,6 +292,10 @@ void ci_lazy_methodst::initialize_needed_classes( lazy_methods.add_needed_class("java::java.lang.String"); lazy_methods.add_needed_class("java::java.lang.Class"); lazy_methods.add_needed_class("java::java.lang.Object"); + + // As in class_loader, ensure these classes stay available + for(const auto &id : extra_needed_classes) + lazy_methods.add_needed_class("java::" + id2string(id)); } /// Build up list of methods for types for a pointer and any types it diff --git a/src/java_bytecode/ci_lazy_methods.h b/src/java_bytecode/ci_lazy_methods.h index f910abf2bb8..5c5d2aca51c 100644 --- a/src/java_bytecode/ci_lazy_methods.h +++ b/src/java_bytecode/ci_lazy_methods.h @@ -48,6 +48,7 @@ class ci_lazy_methodst:public messaget const std::vector &main_jar_classes, const std::vector &lazy_methods_extra_entry_points, java_class_loadert &java_class_loader, + const std::vector &extra_needed_classes, const select_pointer_typet &pointer_type_selector, message_handlert &message_handler); @@ -111,6 +112,7 @@ class ci_lazy_methodst:public messaget std::vector main_jar_classes; std::vector lazy_methods_extra_entry_points; java_class_loadert &java_class_loader; + const std::vector &extra_needed_classes; const select_pointer_typet &pointer_type_selector; }; diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index 26914f08522..c949b54f211 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -61,6 +61,12 @@ void java_bytecode_languaget::get_language_options(const cmdlinet &cmd) else lazy_methods_mode=LAZY_METHODS_MODE_EAGER; + if(cmd.isset("java-load-class")) + { + for(const auto &c : cmd.get_values("java-load-class")) + java_load_classes.push_back(c); + } + const std::list &extra_entry_points= cmd.get_values("lazy-methods-extra-entry-point"); lazy_methods_extra_entry_points.insert( @@ -128,6 +134,7 @@ bool java_bytecode_languaget::parse( PRECONDITION(language_options_initialized); 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); // look at extension if(has_suffix(path, ".class")) @@ -323,6 +330,7 @@ bool java_bytecode_languaget::do_ci_lazy_method_conversion( main_jar_classes, lazy_methods_extra_entry_points, java_class_loader, + java_load_classes, get_pointer_type_selector(), get_message_handler()); diff --git a/src/java_bytecode/java_bytecode_language.h b/src/java_bytecode/java_bytecode_language.h index f10fee616e5..d8999572942 100644 --- a/src/java_bytecode/java_bytecode_language.h +++ b/src/java_bytecode/java_bytecode_language.h @@ -21,15 +21,16 @@ Author: Daniel Kroening, kroening@kroening.com #include -#define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \ - "(java-assume-inputs-non-null)" \ - "(java-throw-runtime-exceptions)" \ - "(java-max-input-array-length):" \ - "(java-max-input-tree-depth):" \ - "(java-max-vla-length):" \ - "(java-cp-include-files):" \ - "(lazy-methods)" \ - "(lazy-methods-extra-entry-point):" +#define JAVA_BYTECODE_LANGUAGE_OPTIONS /*NOLINT*/ \ + "(java-assume-inputs-non-null)" \ + "(java-throw-runtime-exceptions)" \ + "(java-max-input-array-length):" \ + "(java-max-input-tree-depth):" \ + "(java-max-vla-length):" \ + "(java-cp-include-files):" \ + "(lazy-methods)" \ + "(lazy-methods-extra-entry-point):" \ + "(java-load-class):" #define JAVA_BYTECODE_LANGUAGE_OPTIONS_HELP /*NOLINT*/ \ " --java-assume-inputs-non-null never initialize reference-typed parameter to the\n" \ @@ -177,6 +178,9 @@ class java_bytecode_languaget:public languaget java_string_library_preprocesst string_preprocess; std::string java_cp_include_files; + // list of classes to force load even without reference from the entry point + std::vector java_load_classes; + private: const std::unique_ptr pointer_type_selector; }; diff --git a/src/java_bytecode/java_class_loader.cpp b/src/java_bytecode/java_class_loader.cpp index bb945ddcc10..b3039e9bd69 100644 --- a/src/java_bytecode/java_class_loader.cpp +++ b/src/java_bytecode/java_class_loader.cpp @@ -36,6 +36,10 @@ java_bytecode_parse_treet &java_class_loadert::operator()( queue.push("java.lang.Throwable"); queue.push(class_name); + // Require user provided classes to be loaded even without explicit reference + for(const auto &id : java_load_classes) + queue.push(id); + java_class_loader_limitt class_loader_limit( get_message_handler(), java_cp_include_files); @@ -278,3 +282,12 @@ jar_filet &java_class_loadert::jar_pool( else return it->second; } + +/// Adds the list of classes to the load queue, forcing them to be loaded even +/// without explicit reference +/// \param classes: list of class identifiers +void java_class_loadert::add_load_classes(const std::vector &classes) +{ + for(const auto &id : classes) + java_load_classes.push_back(id); +} diff --git a/src/java_bytecode/java_class_loader.h b/src/java_bytecode/java_class_loader.h index fe8f8e3dd77..82e624bbacc 100644 --- a/src/java_bytecode/java_class_loader.h +++ b/src/java_bytecode/java_class_loader.h @@ -26,6 +26,7 @@ class java_class_loadert:public messaget java_bytecode_parse_treet &operator()(const irep_idt &); void set_java_cp_include_files(std::string &); + void add_load_classes(const std::vector &); static std::string file_to_class_name(const std::string &); static std::string class_name_to_file(const irep_idt &); @@ -94,6 +95,7 @@ class java_class_loadert:public messaget std::string java_cp_include_files; private: std::map m_archives; + std::vector java_load_classes; }; #endif // CPROVER_JAVA_BYTECODE_JAVA_CLASS_LOADER_H