Nondet-initialize enums to be equal to a constant of the same type

jbmc/regression/jbmc/NondetEnumArg/Color.java

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

jbmc/regression/jbmc/NondetEnumArg/NondetEnumArg.java

@@ -0,0 +1,46 @@
+public class NondetEnumArg {
+
+    public static void canChooseSomeConstant(Color c) {
+        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(Color c) {
+        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(Color c) {
+        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(Color c) {
+        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/NondetEnumArg/test_some_constant.desc

@@ -0,0 +1,10 @@
+CORE
+NondetEnumArg.class
+--function NondetEnumArg.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
+correspond to those of an enum constant of the same type.

jbmc/regression/jbmc/NondetEnumArg/test_specific_constant1.desc

@@ -0,0 +1,7 @@
+CORE
+NondetEnumArg.class
+--function NondetEnumArg.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/NondetEnumArg/test_specific_constant2.desc

@@ -0,0 +1,7 @@
+CORE
+NondetEnumArg.class
+--function NondetEnumArg.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/NondetEnumArg/test_specific_constant3.desc

@@ -0,0 +1,7 @@
+CORE
+NondetEnumArg.class
+--function NondetEnumArg.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

@@ -381,7 +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());
+        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);
       }
     }
@@ -399,6 +409,29 @@ void ci_lazy_methodst::initialize_instantiated_classes(
     needed_lazy_methods.add_needed_class("java::" + id2string(id));
 }
 
+/// 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
+/// `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 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,
+  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);
+  if(symbol_table.symbols.count(clinit_wrapper))
+    needed_lazy_methods.add_needed_method(clinit_wrapper);
+}
 
 /// Get places where virtual functions are called.
 /// \param e: expression tree to search

jbmc/src/java_bytecode/ci_lazy_methods.h

@@ -120,6 +120,11 @@ 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,
+    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);