Merge pull request #3124 from antlechner/stub-return-enum

Load static initializers for enum types returned by opaque methods

Author: antlechner

jbmc/regression/jbmc/NondetEnumOpaqueReturn/Color.class

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

jbmc/regression/jbmc/NondetEnumOpaqueReturn/Color.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/NondetEnumOpaqueReturn.class

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

jbmc/regression/jbmc/NondetEnumOpaqueReturn/NondetEnumOpaqueReturn.java

@@ -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/Opaque.java

@@ -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_some_constant.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_constant1.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/regression/jbmc/NondetEnumOpaqueReturn/test_specific_constant2.desc

@@ -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.