Make failed nondet Enum assignment non-fatal

Previously we always expected an Enum type's VALUES array to be present if it may be created in a
stub method. However while this is easy for a front-end to ensure when the Enum is a direct return
type or member of a stub return type, there are other cases where the object factory can end up
building a nondet Enum, such as generic type substitution and usage-inferred stub return types.
Until (if ever) ci-lazy-methods can precisely mimic the object factory's behaviour, we're better
off tolerating the case where the VALUES array remains missing than killing the entire run.

Author: smowton

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -104,7 +104,7 @@ class java_object_factoryt
     update_in_placet,
     const source_locationt &location);
 
-  void gen_nondet_enum_init(
+  bool gen_nondet_enum_init(
     code_blockt &assignments,
     const exprt &expr,
     const java_class_typet &java_class_type,
@@ -263,8 +263,8 @@ void java_object_factoryt::gen_pointer_target_init(
     }
     if(target_class_type.get_base("java::java.lang.Enum"))
     {
-      gen_nondet_enum_init(assignments, expr, target_class_type, location);
-      return;
+      if(gen_nondet_enum_init(assignments, expr, target_class_type, location))
+        return;
     }
   }
 
@@ -1435,20 +1435,25 @@ void java_object_factoryt::gen_nondet_array_init(
 ///     int i = nondet(int);
 ///     assume(0 < = i < $VALUES.length);
 ///     expr = $VALUES[i];
-/// where $VALUES is a variable generated by the Java compiler that stores
-/// the array that is returned by Enum.values().
-void java_object_factoryt::gen_nondet_enum_init(
+/// where $VALUES is a variable generated by the Java compiler and which gives
+/// the possible values of a particular enum subtype (this is the same array
+/// that is returned by Enum.values()).
+/// This may fail if the $VALUES static field is not present. Ensuring that
+/// field is in the symbol table when this method may be applicable is the
+/// driver program's responsibility: for example, \ref ci_lazy_methods.cpp makes
+/// some effort to retain this field when a stub method might refer to it.
+/// \return true on success
+bool java_object_factoryt::gen_nondet_enum_init(
   code_blockt &assignments,
   const exprt &expr,
   const java_class_typet &java_class_type,
   const source_locationt &location)
 {
   const irep_idt &class_name = java_class_type.get_name();
   const irep_idt values_name = id2string(class_name) + ".$VALUES";
-  INVARIANT(
-    ns.get_symbol_table().has_symbol(values_name),
-    "The $VALUES array (populated by clinit_wrapper) should be in the "
-    "symbol table");
+  if(!ns.get_symbol_table().has_symbol(values_name))
+    return false;
+
   const symbolt &values = ns.lookup(values_name);
 
   // Access members (length and data) of $VALUES array
@@ -1473,6 +1478,8 @@ void java_object_factoryt::gen_nondet_enum_init(
   const dereference_exprt arraycellref(plus);
   code_assignt enum_assign(expr, typecast_exprt(arraycellref, expr.type()));
   assignments.add(enum_assign);
+
+  return true;
 }
 
 static void assert_type_consistency(const code_blockt &assignments)