Load static initializers for enum types returned by opaque methods

jbmc/regression/jbmc/NondetEnumOpaqueReturn/Color.java

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

jbmc/regression/jbmc/NondetEnumOpaqueReturn/NondetEnumOpaqueReturn.java

@@ -0,0 +1,54 @@
+public class NondetEnumOpaqueReturn {
+
+  public static void canChooseSomeConstant() {
+    Opaque o = new Opaque();
+    Color c = o.getC();
+    if (c == null)
+      return;
+    assert c != null;
+    boolean isRed = c.name().startsWith("RED") && c.name().length() == 3
+      && c.ordinal() == 0;
+    boolean isGreen = c.name().startsWith("GREEN") && c.name().length() == 5
+      && c.ordinal() == 1;
+    boolean isBlue = c.name().startsWith("BLUE") && c.name().length() == 4
+      && c.ordinal() == 2;
+    assert (isRed || isGreen || isBlue);
+  }
+
+  public static void canChooseRed() {
+    Opaque o = new Opaque();
+    Color c = o.getC();
+    if (c == null)
+      return;
+    boolean isGreen = c.name().startsWith("GREEN") && c.name().length() == 5
+      && c.ordinal() == 1;
+    boolean isBlue = c.name().startsWith("BLUE") && c.name().length() == 4
+      && c.ordinal() == 2;
+    assert (isGreen || isBlue);
+  }
+
+  public static void canChooseGreen() {
+    Opaque o = new Opaque();
+    Color c = o.getC();
+    if (c == null)
+      return;
+    boolean isRed = c.name().startsWith("RED") && c.name().length() == 3
+      && c.ordinal() == 0;
+    boolean isBlue = c.name().startsWith("BLUE") && c.name().length() == 4
+      && c.ordinal() == 2;
+    assert (isRed || isBlue);
+  }
+
+  public static void canChooseBlue() {
+    Opaque o = new Opaque();
+    Color c = o.getC();
+    if (c == null)
+      return;
+    boolean isRed = c.name().startsWith("RED") && c.name().length() == 3
+      && c.ordinal() == 0;
+    boolean isGreen = c.name().startsWith("GREEN") && c.name().length() == 5
+      && c.ordinal() == 1;
+    assert (isRed || isGreen);
+  }
+
+}

jbmc/regression/jbmc/NondetEnumOpaqueReturn/Opaque.java

@@ -0,0 +1,9 @@
+public class Opaque {
+
+  Color c;
+
+  public Color getC() {
+    return c;
+  }
+
+}

jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_some_constant.desc

@@ -0,0 +1,11 @@
+CORE
+NondetEnumOpaqueReturn.class
+--function NondetEnumOpaqueReturn.canChooseSomeConstant --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+The test checks that the name and ordinal fields of nondet-initialized enums
+which have been returned by an opaque method correspond to those of an enum
+constant of the same type.

jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant1.desc

@@ -0,0 +1,7 @@
+CORE
+NondetEnumOpaqueReturn.class
+--function NondetEnumOpaqueReturn.canChooseRed --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+^VERIFICATION FAILED$
+--
+--
+Test 1 of 3 to check that any of the enum constants can be chosen.

jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant2.desc

@@ -0,0 +1,7 @@
+CORE
+NondetEnumOpaqueReturn.class
+--function NondetEnumOpaqueReturn.canChooseGreen --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+^VERIFICATION FAILED$
+--
+--
+Test 2 of 3 to check that any of the enum constants can be chosen.

jbmc/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant3.desc

@@ -0,0 +1,7 @@
+CORE
+NondetEnumOpaqueReturn.class
+--function NondetEnumOpaqueReturn.canChooseBlue --cp `../../../../scripts/format_classpath.sh . ../../../src/java_bytecode/library/core-models.jar`
+^VERIFICATION FAILED$
+--
+--
+Test 3 of 3 to check that any of the enum constants can be chosen.

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