Nondet-init enums by assigning them to a constant

Rather than nondet-initializing each field (String name and int ordinal)
of an enum, we assign it to be equal to one of the constant values
stored in the $VALUES array of the corresponding type.

Author: antlechner

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -394,65 +394,103 @@ void java_object_factoryt::gen_pointer_target_init(
   update_in_placet update_in_place,
   const source_locationt &location)
 {
-  PRECONDITION(expr.type().id()==ID_pointer);
-  PRECONDITION(update_in_place!=update_in_placet::MAY_UPDATE_IN_PLACE);
+  PRECONDITION(expr.type().id() == ID_pointer);
+  PRECONDITION(update_in_place != update_in_placet::MAY_UPDATE_IN_PLACE);
 
-  if(target_type.id()==ID_struct &&
-     has_prefix(
-       id2string(to_struct_type(target_type).get_tag()),
-       "java::array["))
-  {
-    gen_nondet_array_init(
-      assignments, expr, depth + 1, update_in_place, location);
-  }
-  else
+  if(target_type.id() == ID_struct)
   {
-    // obtain a target pointer to initialize; if in MUST_UPDATE_IN_PLACE mode we
-    // initialize the fields of the object pointed by `expr`; if in
-    // NO_UPDATE_IN_PLACE then we allocate a new object, get a pointer to it
-    // (return value of `allocate_object`), emit a statement of the form
-    // `<expr> := address-of(<new-object>)` and recursively initialize such new
-    // object.
-    exprt target;
-    if(update_in_place==update_in_placet::NO_UPDATE_IN_PLACE)
+    const auto &target_class_type = to_java_class_type(target_type);
+    if(has_prefix(id2string(target_class_type.get_tag()), "java::array["))
     {
-      target=allocate_object(
-        assignments,
-        expr,
-        target_type,
-        alloc_type);
-      INVARIANT(
-        target.type().id()==ID_pointer,
-        "Pointer-typed expression expected");
+      gen_nondet_array_init(
+        assignments, expr, depth + 1, update_in_place, location);
+      return;
     }
-    else
+    if(target_class_type.get_base("java::java.lang.Enum"))
     {
-      target=expr;
-    }
+      // We nondet-initialize enums to be equal to one of the constants defined
+      // for their type:
+      // 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().
+
+      const irep_idt &class_name = target_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");
+      const symbolt &values = ns.lookup(values_name);
+
+      // Access members (length and data) of $VALUES array
+      dereference_exprt deref_expr(values.symbol_expr());
+      const auto &deref_struct_type =
+        to_struct_type(ns.follow(deref_expr.type()));
+      PRECONDITION(is_valid_java_array(deref_struct_type));
+      const auto &comps = deref_struct_type.components();
+      const member_exprt length_expr(deref_expr, "length", comps[1].type());
+      const member_exprt enum_array_expr =
+        member_exprt(deref_expr, "data", comps[2].type());
+
+      const symbol_exprt &index_expr = gen_nondet_int_init(
+        assignments,
+        "enum_index_init",
+        from_integer(0, java_int_type()),
+        minus_exprt(length_expr, from_integer(1, java_int_type())),
+        location);
 
-    // we dereference the pointer and initialize the resulting object using a
-    // recursive call
-    exprt init_expr;
-    if(target.id()==ID_address_of)
-      init_expr=target.op0();
-    else
-    {
-      init_expr=
-        dereference_exprt(target, target.type().subtype());
+      // Generate statement using pointer arithmetic to access array element:
+      // expr = (expr.type())*(enum_array_expr + index_expr);
+      plus_exprt plus(enum_array_expr, index_expr);
+      const dereference_exprt arraycellref(
+        plus, enum_array_expr.type().subtype());
+      code_assignt enum_assign(expr, typecast_exprt(arraycellref, expr.type()));
+      assignments.add(enum_assign);
+      return;
     }
-    gen_nondet_init(
-      assignments,
-      init_expr,
-      false, // is_sub
-      "",    // class_identifier
-      false, // skip_classid
-      alloc_type,
-      false,
-      typet(),
-      depth + 1,
-      update_in_place,
-      location);
   }
+
+  // obtain a target pointer to initialize; if in MUST_UPDATE_IN_PLACE mode we
+  // initialize the fields of the object pointed by `expr`; if in
+  // NO_UPDATE_IN_PLACE then we allocate a new object, get a pointer to it
+  // (return value of `allocate_object`), emit a statement of the form
+  // `<expr> := address-of(<new-object>)` and recursively initialize such new
+  // object.
+  exprt target;
+  if(update_in_place == update_in_placet::NO_UPDATE_IN_PLACE)
+  {
+    target = allocate_object(assignments, expr, target_type, alloc_type);
+    INVARIANT(
+      target.type().id() == ID_pointer, "Pointer-typed expression expected");
+  }
+  else
+  {
+    target = expr;
+  }
+
+  // we dereference the pointer and initialize the resulting object using a
+  // recursive call
+  exprt init_expr;
+  if(target.id() == ID_address_of)
+    init_expr = target.op0();
+  else
+  {
+    init_expr = dereference_exprt(target, target.type().subtype());
+  }
+  gen_nondet_init(
+    assignments,
+    init_expr,
+    false, // is_sub
+    "",    // class_identifier
+    false, // skip_classid
+    alloc_type,
+    false,   // override
+    typet(), // override type immaterial
+    depth + 1,
+    update_in_place,
+    location);
 }
 
 /// Recursion-set entry owner class. If a recursion-set entry is added
@@ -1258,7 +1296,7 @@ const symbol_exprt java_object_factoryt::gen_nondet_int_init(
   gen_nondet_init(
     assignments,
     int_symbol_expr,
-    false,                   // is_sub
+    false, // is_sub
     irep_idt(),
     false,                   // skip_classid
     allocation_typet::LOCAL, // immaterial, type is primitive