diff --git a/jbmc/regression/jbmc/multidimensional-array-object-factory/My.class b/jbmc/regression/jbmc/multidimensional-array-object-factory/My.class new file mode 100644 index 0000000000..47f58a8831 Binary files /dev/null and b/jbmc/regression/jbmc/multidimensional-array-object-factory/My.class differ diff --git a/jbmc/regression/jbmc/multidimensional-array-object-factory/My.java b/jbmc/regression/jbmc/multidimensional-array-object-factory/My.java new file mode 100644 index 0000000000..2a18d3347c --- /dev/null +++ b/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; + } +} diff --git a/jbmc/regression/jbmc/multidimensional-array-object-factory/test.desc b/jbmc/regression/jbmc/multidimensional-array-object-factory/test.desc new file mode 100644 index 0000000000..5ce4fe5e39 --- /dev/null +++ b/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. diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index d25cc7032e..82582767cd 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/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));