CI lazy methods: load clinit for all param types

We load static initializers for all types of parameters of the entry
function(s). This is necessary for the new nondet-initialization of
enums, and also consistent with the Java language specification, which
says that static initializers should be run on object initialization.

Author: antlechner

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -382,6 +382,8 @@ void ci_lazy_methodst::initialize_instantiated_classes(
       if(param.type().id()==ID_pointer)
       {
         const pointer_typet &original_pointer=to_pointer_type(param.type());
+        add_clinit_call_for_pointer_type(
+          original_pointer, ns.get_symbol_table(), needed_lazy_methods);
         needed_lazy_methods.add_all_needed_classes(original_pointer);
       }
     }
@@ -399,6 +401,29 @@ void ci_lazy_methodst::initialize_instantiated_classes(
     needed_lazy_methods.add_needed_class("java::" + id2string(id));
 }
 
+/// Helper function for `initialize_instantiated_classes`.
+/// For a given pointer_typet that is being noted as needed in
+/// `needed_lazy_methods`, notes that its static initializer is also needed.
+/// This applies the same logic to the class of `pointer_type` that
+/// `java_bytecode_convert_methodt::get_clinit_call` applies e.g. to classes
+/// whose constructor we call in a method body. This duplication is unavoidable
+/// due to the fact that ci_lazy_methods essentially has to go through the same
+/// logic as __CPROVER_start in its initial setup.
+/// \param pointer_type: The given pointer_typet
+/// \param symbol_table: Used to look up occurrences of static initializers
+/// \param [out] needed_lazy_methods: Gets notified of any static initializers
+///   that need to be loaded
+void ci_lazy_methodst::add_clinit_call_for_pointer_type(
+  const pointer_typet &pointer_type,
+  const symbol_tablet &symbol_table,
+  ci_lazy_methods_neededt &needed_lazy_methods)
+{
+  const irep_idt &pointer_id =
+    to_symbol_type(pointer_type.subtype()).get_identifier();
+  const irep_idt &clinit_wrapper = clinit_wrapper_name(pointer_id);
+  if(symbol_table.symbols.count(clinit_wrapper))
+    needed_lazy_methods.add_needed_method(clinit_wrapper);
+}
 
 /// Get places where virtual functions are called.
 /// \param e: expression tree to search

jbmc/src/java_bytecode/ci_lazy_methods.h

@@ -120,6 +120,11 @@ class ci_lazy_methodst:public messaget
     const namespacet &ns,
     ci_lazy_methods_neededt &needed_lazy_methods);
 
+  void add_clinit_call_for_pointer_type(
+    const pointer_typet &pointer_type,
+    const symbol_tablet &symbol_table,
+    ci_lazy_methods_neededt &needed_lazy_methods);
+
   void gather_virtual_callsites(
     const exprt &e,
     std::unordered_set<exprt, irep_hash> &result);