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

@@ -146,7 +146,8 @@ class java_object_factoryt
     code_blockt &assignments,
     const std::string &basename_prefix,
     const exprt &min_length_expr,
-    const exprt &max_length_expr);
+    const exprt &max_length_expr,
+    bool include_max);
 
   void gen_method_call(
     code_blockt &assignments,
@@ -384,67 +385,95 @@ void java_object_factoryt::gen_pointer_target_init(
   size_t depth,
   update_in_placet update_in_place)
 {
-  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);
-  }
-  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);
+      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 symbolt &values = ns.lookup(id2string(class_name) + ".$VALUES");
+
+      // 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()));
+      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()),
+        length_expr,
+        false);
+
+      // Index array using pointer arithmetic
+      plus_exprt plus(enum_array_expr, index_expr, enum_array_expr.type());
+      const dereference_exprt arraycellref(
+        plus_exprt(enum_array_expr, index_expr, enum_array_expr.type()),
+        enum_array_expr.type().subtype());
+      code_assignt enum_assign(expr, typecast_exprt(arraycellref, expr.type()));
+      assignments.add(enum_assign);
+      return;
     }
+  }
 
-    // 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);
+  // 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);
 }
 
 /// Recursion-set entry owner class. If a recursion-set entry is added
@@ -1207,20 +1236,25 @@ void java_object_factoryt::gen_nondet_init(
   }
 }
 
-/// Nondeterministically initializes an int i in the range min <= i <= max,
+/// Nondeterministically initializes an int i in the range min <= i <= max (if
+/// `include_max` is true) or min <= i < max (if `include_max` is false),
 /// where min is the integer represented by `min_value_expr` and max is the
 /// integer represented by `max_value_expr`.
 /// \param [out] assignments: A code block that the initializing assignments
 ///   will be appended to.
 /// \param basename_prefix: Used for naming the newly created symbol.
 /// \param min_value_expr: Represents the minimum value for the integer.
 /// \param max_value_expr: Represents the maximum value for the integer.
+/// \param include_max: true if the maximum value should be included in the
+///   range, false otherwise (i.e. if the maximum value for the integer is
+///   max_value_expr - 1).
 /// \return A symbol expression for the resulting integer.
 const symbol_exprt java_object_factoryt::gen_nondet_int_init(
   code_blockt &assignments,
   const std::string &basename_prefix,
   const exprt &min_value_expr,
-  const exprt &max_value_expr)
+  const exprt &max_value_expr,
+  bool include_max)
 {
   // Allocate a new symbol for the int
   const symbolt &int_symbol = get_fresh_aux_symbol(
@@ -1237,7 +1271,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
@@ -1250,7 +1284,8 @@ const symbol_exprt java_object_factoryt::gen_nondet_int_init(
   const auto min_assume_expr =
     binary_relation_exprt(int_symbol_expr, ID_ge, min_value_expr);
   const auto max_assume_expr =
-    binary_relation_exprt(int_symbol_expr, ID_le, max_value_expr);
+    include_max ? binary_relation_exprt(int_symbol_expr, ID_le, max_value_expr)
+                : binary_relation_exprt(int_symbol_expr, ID_lt, max_value_expr);
   assignments.add(code_assumet(min_assume_expr));
   assignments.add(code_assumet(max_assume_expr));
 
@@ -1280,7 +1315,8 @@ void java_object_factoryt::allocate_nondet_length_array(
     assignments,
     "nondet_array_length",
     from_integer(0, java_int_type()),
-    max_length_expr);
+    max_length_expr,
+    true);
 
   side_effect_exprt java_new_array(ID_java_new_array, lhs.type());
   java_new_array.copy_to_operands(length_sym_expr);