Add force loading parameter --java-load-class

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.

src/java_bytecode/ci_lazy_methods.cpp

@@ -17,20 +17,33 @@
 
 #include <goto-programs/resolve_concrete_function_call.h>
 
-
+/// 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<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> &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

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> &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<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> &extra_needed_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"))
+  {
+    for(const auto &c : cmd.get_values("java-load-class"))
+      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

@@ -21,15 +21,16 @@ Author: Daniel Kroening, [email protected]
 
 #include <java_bytecode/select_pointer_type.h>
 
-#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<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,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<irep_idt> &classes)
+{
+  for(const auto &id : classes)
+    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(const 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