Add force loading parameter --java-load-class-list

This parameter force loads the specified classes and prevents their methods from
being removed by lazy-methods. This allows to add classes that provide an
implementations for interfaces, where the classes themselves are not referenced.

Author: Matthias Güdemann

src/java_bytecode/ci_lazy_methods.cpp

@@ -24,13 +24,15 @@ ci_lazy_methodst::ci_lazy_methodst(
   const std::vector<irep_idt> &main_jar_classes,
   const std::vector<irep_idt> &lazy_methods_extra_entry_points,
   java_class_loadert &java_class_loader,
+  const std::vector<irep_idt> &java_load_classes,
   const select_pointer_typet &pointer_type_selector,
   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),
+    java_load_classes(java_load_classes),
     pointer_type_selector(pointer_type_selector)
 {
   // build the class hierarchy
@@ -279,6 +281,14 @@ 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
+  std::for_each(
+    java_load_classes.begin(),
+    java_load_classes.end(),
+    [&](const irep_idt &id) {
+      lazy_methods.add_needed_class("java::" + id2string(id));
+    });
 }
 
 /// Build up list of methods for types for a pointer and any types it

src/java_bytecode/ci_lazy_methods.h

@@ -48,6 +48,7 @@ class ci_lazy_methodst:public messaget
     const std::vector<irep_idt> &main_jar_classes,
     const std::vector<irep_idt> &lazy_methods_extra_entry_points,
     java_class_loadert &java_class_loader,
+    const std::vector<irep_idt> &java_load_classes,
     const select_pointer_typet &pointer_type_selector,
     message_handlert &message_handler);
 
@@ -111,6 +112,7 @@ class ci_lazy_methodst:public messaget
   std::vector<irep_idt> main_jar_classes;
   std::vector<irep_idt> lazy_methods_extra_entry_points;
   java_class_loadert &java_class_loader;
+  const std::vector<irep_idt> &java_load_classes;
   const select_pointer_typet &pointer_type_selector;
 };
 

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-list"))
+  {
+    for(const auto &c : cmd.get_values("java-load-class-list"))
+      java_load_classes.push_back(c);
+  }
+
   const std::list<std::string> &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());
 

src/java_bytecode/java_bytecode_language.h

@@ -29,7 +29,8 @@ Author: Daniel Kroening, [email protected]
   "(java-max-vla-length):"                        \
   "(java-cp-include-files):"                      \
   "(lazy-methods)"                                \
-  "(lazy-methods-extra-entry-point):"
+  "(lazy-methods-extra-entry-point):"             \
+  "(java-load-class-list):"
 
 #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<irep_idt> java_load_classes;
+
 private:
   const std::unique_ptr<const select_pointer_typet> pointer_type_selector;
 };

src/java_bytecode/java_class_loader.cpp

@@ -36,6 +36,12 @@ java_bytecode_parse_treet &java_class_loadert::operator()(
   queue.push("java.lang.Throwable");
   queue.push(class_name);
 
+  // Require often used library classes that implement widely used interfaces
+  std::for_each(
+    java_load_classes.begin(),
+    java_load_classes.end(),
+    [&](const irep_idt &id) { queue.push(id); });
+
   java_class_loader_limitt class_loader_limit(
     get_message_handler(), java_cp_include_files);
 
@@ -278,3 +284,13 @@ 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(std::vector<irep_idt> &classes)
+{
+  std::for_each(classes.begin(), classes.end(), [&](const irep_idt &id) {
+    java_load_classes.push_back(id);
+  });
+}

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(std::vector<irep_idt> &);
 
   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<std::string, jar_filet> m_archives;
+  std::vector<irep_idt> java_load_classes;
 };
 
 #endif // CPROVER_JAVA_BYTECODE_JAVA_CLASS_LOADER_H