CI lazy methods: load clinit for all enum types

Previously static initializers for enum types were only loaded for those
types that are reachable from the arguments to the entry method.
This would lead to an invariant violation when an opaque method returned
an enum type (which needs to be nondet-initialized just like arguments
to the entry method).
This commit solves this problem by moving the code for marking the
static initializers of enums as loaded from ci_lazy_methods to
ci_lazy_methods_needed, and applying it to all deterministic and
nondeterministic enums that are reachable in some way from the entry
method.
Including deterministic enums is not a problem, since we load static
initializers for all types (enums and others) whose constructor we use
anyway.

Author: antlechner

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -392,37 +392,6 @@ 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 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 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(
-  const irep_idt &class_id,
-  const symbol_tablet &symbol_table,
-  ci_lazy_methods_neededt &needed_lazy_methods)
-{
-  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);
 }
 
 /// Get places where virtual functions are called.

jbmc/src/java_bytecode/ci_lazy_methods.h

@@ -120,11 +120,6 @@ class ci_lazy_methodst:public messaget
     const namespacet &ns,
     ci_lazy_methods_neededt &needed_lazy_methods);
 
-  void add_clinit_call(
-    const irep_idt &class_id,
-    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);

jbmc/src/java_bytecode/ci_lazy_methods_needed.cpp

@@ -10,6 +10,7 @@ Author: Chris Smowton, [email protected]
 /// Context-insensitive lazy methods container
 
 #include "ci_lazy_methods.h"
+#include "java_static_initializers.h"
 
 #include <java_bytecode/select_pointer_type.h>
 #include <string>
@@ -25,6 +26,24 @@ void ci_lazy_methods_neededt::add_needed_method(
   callable_methods.insert(method_symbol_name);
 }
 
+/// For a given class id, note that its static initializer is 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
+/// because ci_lazy_methods essentially has to go through the same logic as
+/// __CPROVER_start in its initial setup, and because return values of opaque
+/// methods need to be considered in ci_lazy_methods too.
+/// \param class_id: The given class id
+/// \param symbol_table: Used to look up occurrences of static initializers
+void ci_lazy_methods_neededt::add_clinit_call(
+  const irep_idt &class_id,
+  const symbol_tablet &symbol_table)
+{
+  const irep_idt &clinit_wrapper = clinit_wrapper_name(class_id);
+  if(symbol_table.symbols.count(clinit_wrapper))
+    add_needed_method(clinit_wrapper);
+}
+
 /// Notes class `class_symbol_name` will be instantiated, or a static field
 /// belonging to it will be accessed. Also notes that its static initializer is
 /// therefore reachable.
@@ -42,6 +61,14 @@ bool ci_lazy_methods_neededt::add_needed_class(
   if(symbol_table.symbols.count(cprover_validate))
     add_needed_method(cprover_validate);
 
+  // Special case for enums. We may want to generalise this, the comment in
+  // \ref java_object_factoryt::gen_nondet_pointer_init (TG-4689).
+  namespacet ns(symbol_table);
+  const auto &class_type =
+    to_java_class_type(ns.lookup(class_symbol_name).type);
+  if(class_type.get_base("java::java.lang.Enum"))
+    add_clinit_call(class_symbol_name, symbol_table);
+
   return true;
 }
 

jbmc/src/java_bytecode/ci_lazy_methods_needed.h

@@ -35,11 +35,6 @@ 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 &);
@@ -61,6 +56,9 @@ class ci_lazy_methods_neededt
 
   const select_pointer_typet &pointer_type_selector;
 
+  void
+  add_clinit_call(const irep_idt &class_id, const symbol_tablet &symbol_table);
+
   void initialize_instantiated_classes_from_pointer(
     const pointer_typet &pointer_type,
     const namespacet &ns);