Merge pull request #4523 from smowton/smowton/feature/use-temporary-to-init-multidimensional-array

Use temporary variable to initialise array cells

jbmc/regression/jbmc/multidimensional-array-object-factory/My.java

@@ -0,0 +1,8 @@
+public class My {
+    public int func(int[][] inta) {
+        if (inta[0][0] == 500) { 
+            return 1; 
+        }
+        return 0;
+    }
+}

jbmc/regression/jbmc/multidimensional-array-object-factory/test.desc

@@ -0,0 +1,14 @@
+CORE
+My.class
+--function My.func --unwind 3 --max-nondet-array-length 10 --show-vcc
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring
+\$object
+invalid_object
+--
+This checks that no \$object or invalid_object references are generated when creating a multidimensional
+array (required for My.func's input parameter, which is an int[][]). Both of the unwanted terms are used
+by goto-symex to describe the result of a failed or unknown pointer dereference, and the object factory's
+initialisation code should be clear enough that this is never necessary.

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1205,6 +1205,29 @@ void java_object_factoryt::array_loop_init_code(
     plus_exprt(array_init_symexpr, counter_expr, array_init_symexpr.type()),
     array_init_symexpr.type().subtype());
 
+  bool new_item_is_primitive = arraycellref.type().id() != ID_pointer;
+
+  // Use a temporary to initialise a new, or update an existing, non-primitive.
+  // This makes it clearer that in a sequence like
+  // `new_array_item->x = y; new_array_item->z = w;` that all the
+  // `new_array_item` references must alias, cf. the harder-to-analyse
+  // `some_expr[idx]->x = y; some_expr[idx]->z = w;`
+  exprt init_expr;
+  if(new_item_is_primitive)
+  {
+    init_expr = arraycellref;
+  }
+  else
+  {
+    init_expr = allocate_objects.allocate_automatic_local_object(
+      arraycellref.type(), "new_array_item");
+
+    // If we're updating an existing array item, read the existing object that
+    // we (may) alter:
+    if(update_in_place != update_in_placet::NO_UPDATE_IN_PLACE)
+      assignments.add(code_assignt(init_expr, arraycellref));
+  }
+
   // MUST_UPDATE_IN_PLACE only applies to this object.
   // If this is a pointer to another object, offer the chance
   // to leave it alone by setting MAY_UPDATE_IN_PLACE instead.
@@ -1214,9 +1237,9 @@ void java_object_factoryt::array_loop_init_code(
     update_in_place;
   gen_nondet_init(
     assignments,
-    arraycellref,
-    false,      // is_sub
-    false,      // skip_classid
+    init_expr,
+    false, // is_sub
+    false, // skip_classid
     // These are variable in number, so use dynamic allocator:
     lifetimet::DYNAMIC,
     element_type, // override
@@ -1224,6 +1247,13 @@ void java_object_factoryt::array_loop_init_code(
     child_update_in_place,
     location);
 
+  if(!new_item_is_primitive)
+  {
+    // We used a temporary variable to update or initialise an array item;
+    // now write it into the array:
+    assignments.add(code_assignt(arraycellref, init_expr));
+  }
+
   exprt java_one=from_integer(1, java_int_type());
   code_assignt incr(counter_expr, plus_exprt(counter_expr, java_one));