Move nondet enum initialization to new function

Author: antlechner

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -107,6 +107,12 @@ class java_object_factoryt
     update_in_placet,
     const source_locationt &location);
 
+  void gen_nondet_enum_init(
+    code_blockt &assignments,
+    const exprt &expr,
+    const java_class_typet &java_class_type,
+    const source_locationt &location);
+
   void gen_nondet_init(
     code_blockt &assignments,
     const exprt &expr,
@@ -408,46 +414,7 @@ void java_object_factoryt::gen_pointer_target_init(
     }
     if(target_class_type.get_base("java::java.lang.Enum"))
     {
-      // 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);
-
-      // 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);
+      gen_nondet_enum_init(assignments, expr, target_class_type, location);
       return;
     }
   }
@@ -1492,6 +1459,51 @@ void java_object_factoryt::gen_nondet_array_init(
   assignments.move_to_operands(init_done_label);
 }
 
+/// 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().
+void 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");
+  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);
+
+  // 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);
+  code_assignt enum_assign(expr, typecast_exprt(arraycellref, expr.type()));
+  assignments.add(enum_assign);
+}
+
 /// Add code_declt instructions to `init_code` for every non-static symbol
 /// in `symbols_created`
 /// \param symbols_created: list of symbols