Merge pull request #2754 from antlechner/antonia/ci-lazy-loading-rec-clinit

Fix lazy loading of enum static initializers

Author: antlechner

jbmc/regression/jbmc/NondetEnumArgField/Color.class

@@ -0,0 +1,5 @@
+public enum Color {
+    RED,
+    GREEN,
+    BLUE
+}

jbmc/regression/jbmc/NondetEnumArgField/Color.java

@@ -0,0 +1,11 @@
+public class MyClass {
+
+    private Color c;
+
+    public int myMethod() {
+        if (c == null)
+            return 10;
+        return 20;
+    }
+
+}

jbmc/regression/jbmc/NondetEnumArgField/MyClass.class

@@ -0,0 +1,8 @@
+public class NondetEnumArgField {
+
+    public static void test(MyClass mc) {
+        int result = mc.myMethod();
+        assert result == 10;
+    }
+
+}

jbmc/regression/jbmc/NondetEnumArgField/MyClass.java

@@ -0,0 +1,9 @@
+CORE
+NondetEnumArgField.class
+--function NondetEnumArgField.test --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+^VERIFICATION FAILED$
+--
+--
+The test checks that even when none of the enum constants are referenced in user
+code, a nondet enum (in this case, a field of an argument) is still correctly
+loaded and initialized.

jbmc/regression/jbmc/NondetEnumArgField/NondetEnumArgField.class

@@ -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/regression/jbmc/NondetEnumArgField/NondetEnumArgField.java

@@ -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/regression/jbmc/NondetEnumArgField/test.desc

@@ -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 &);