Fix lazy loading of enum static initializers

Rather than calling clinit_wrapper on every parameter to the entry
method that is an enum, we should first load all the classes that may
be needed before we enter the entry method, and then call
clinit_wrapper on all of those which are enums. For example, the case of
an enum field of an argument to the entry method would have previously
hit an invariant violation.

Author: antlechner

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -382,16 +382,6 @@ void ci_lazy_methodst::initialize_instantiated_classes(
       if(param.type().id()==ID_pointer)
       {
         const pointer_typet &original_pointer = to_pointer_type(param.type());
-        const auto &original_type = ns.follow(original_pointer.subtype());
-        // Special case for enums. We may want to generalise this, see TG-4689
-        // and the comment in java_object_factoryt::gen_nondet_pointer_init.
-        if(
-          can_cast_type<java_class_typet>(original_type) &&
-          to_java_class_type(original_type).get_base("java::java.lang.Enum"))
-        {
-          add_clinit_call_for_pointer_type(
-            original_pointer, ns.get_symbol_table(), needed_lazy_methods);
-        }
         needed_lazy_methods.add_all_needed_classes(original_pointer);
       }
     }
@@ -407,28 +397,35 @@ void ci_lazy_methodst::initialize_instantiated_classes(
   // As in class_loader, ensure these classes stay available
   for(const auto &id : extra_instantiated_classes)
     needed_lazy_methods.add_needed_class("java::" + id2string(id));
+
+  // Special case for enums. We may want to generalise this, see TG-4689
+  // and the comment in java_object_factoryt::gen_nondet_pointer_init.
+  for(const auto &found_class : needed_lazy_methods.get_instantiated_classes())
+  {
+    const auto &class_type = to_java_class_type(ns.lookup(found_class).type);
+    if(class_type.get_base("java::java.lang.Enum"))
+      add_clinit_call(found_class, ns.get_symbol_table(), needed_lazy_methods);
+  }
 }
 
 /// 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
+/// For a given class id 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 given class 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 class_id: The given class id
 /// \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,
+void ci_lazy_methodst::add_clinit_call(
+  const irep_idt &class_id,
   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);
+  const irep_idt &clinit_wrapper = clinit_wrapper_name(class_id);
   if(symbol_table.symbols.count(clinit_wrapper))
     needed_lazy_methods.add_needed_method(clinit_wrapper);
 }

jbmc/src/java_bytecode/ci_lazy_methods.h

@@ -120,8 +120,8 @@ 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,
+  void add_clinit_call(
+    const irep_idt &class_id,
     const symbol_tablet &symbol_table,
     ci_lazy_methods_neededt &needed_lazy_methods);
 

jbmc/src/java_bytecode/ci_lazy_methods_needed.h

@@ -34,6 +34,11 @@ class ci_lazy_methods_neededt
       pointer_type_selector(pointer_type_selector)
   {}
 
+  std::unordered_set<irep_idt> get_instantiated_classes()
+  {
+    return instantiated_classes;
+  }
+
   void add_needed_method(const irep_idt &);
   // Returns true if new
   bool add_needed_class(const irep_idt &);