Restrict new clinit_wrapper calls to enum types

Calling clinit_wrapper on all nondet-initialized types has a noticeable
impact on performance, so for now we are only doing this for enums, and
we will re-evaluate the behavior for other types in the future.

Author: antlechner

jbmc/src/java_bytecode/ci_lazy_methods.cpp

@@ -381,9 +381,17 @@ 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);
+        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);
       }
     }

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -785,18 +785,28 @@ void java_object_factoryt::gen_nondet_pointer_init(
   // (This can currently happen for some cases of #exception_value)
   bool must_be_null = subtype == empty_typet();
 
-  // If we may be about to initialize a non-null object, always run the
+  // If we may be about to initialize a non-null enum type, always run the
   // clinit_wrapper of its class first.
+  // TODO: TG-4689 we may want to do this for all types, not just enums, as
+  // described in the Java language specification:
+  // https://docs.oracle.com/javase/specs/jls/se8/html/jls-8.html#jls-8.7
+  // https://docs.oracle.com/javase/specs/jls/se8/html/jls-12.html#jls-12.4.1
+  // But we would have to put this behavior behind an option as it would have an
+  // impact on running times.
   // Note that it would be more consistent with the behaviour of the JVM to only
   // run clinit_wrapper if we are about to initialize an object of which we know
   // for sure that it is not null on any following branch. However, adding this
-  // case in gen_nondet_struct_init would slow symex down too much.
-  if(!must_be_null)
+  // case in gen_nondet_struct_init would slow symex down too much, so if we
+  // decide to do this for all types, we should do it here.
+  if(can_cast_type<java_class_typet>(subtype))
   {
-    const java_class_typet &class_type = to_java_class_type(subtype);
-    const irep_idt &class_name = class_type.get_name();
-    const irep_idt class_clinit = clinit_wrapper_name(class_name);
-    gen_method_call_if_present(assignments, expr, class_clinit);
+    const java_class_typet &class_type=to_java_class_type(subtype);
+    if(class_type.get_base("java::java.lang.Enum") && !must_be_null)
+    {
+      const irep_idt &class_name=class_type.get_name();
+      const irep_idt class_clinit=clinit_wrapper_name(class_name);
+      gen_method_call_if_present(assignments, expr, class_clinit);
+    }
   }
 
   code_blockt new_object_assignments;