Refactor array access into a separate function

This does not save many lines of code, but the way we access Java arrays
using pointer arithmetic can be a bit confusing and it makes sense to
abstract it away and keep the documentation of why we do things this way
in one place.

Author: antlechner

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1200,10 +1200,10 @@ void java_object_factoryt::array_loop_init_code(
     assignments.add(std::move(max_test));
   }
 
-  const dereference_exprt arraycellref{
-    plus_exprt{array_init_symexpr, counter_expr}};
+  const dereference_exprt element_at_counter =
+    element_at_pointer_array_index(array_init_symexpr, counter_expr);
 
-  bool new_item_is_primitive = arraycellref.type().id() != ID_pointer;
+  bool new_item_is_primitive = element_at_counter.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
@@ -1213,17 +1213,17 @@ void java_object_factoryt::array_loop_init_code(
   exprt init_expr;
   if(new_item_is_primitive)
   {
-    init_expr = arraycellref;
+    init_expr = element_at_counter;
   }
   else
   {
     init_expr = allocate_objects.allocate_automatic_local_object(
-      arraycellref.type(), "new_array_item");
+      element_at_counter.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));
+      assignments.add(code_assignt(init_expr, element_at_counter));
   }
 
   // MUST_UPDATE_IN_PLACE only applies to this object.
@@ -1249,7 +1249,7 @@ void java_object_factoryt::array_loop_init_code(
   {
     // 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));
+    assignments.add(code_assignt(element_at_counter, init_expr));
   }
 
   exprt java_one=from_integer(1, java_int_type());
@@ -1389,11 +1389,9 @@ bool java_object_factoryt::gen_nondet_enum_init(
     allocate_objects,
     assignments);
 
-  // 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()));
+  const dereference_exprt element_at_index =
+    element_at_pointer_array_index(enum_array_expr, index_expr);
+  code_assignt enum_assign(expr, typecast_exprt(element_at_index, expr.type()));
   assignments.add(enum_assign);
 
   return true;

jbmc/src/java_bytecode/java_utils.cpp

@@ -191,6 +191,12 @@ dereference_exprt checked_dereference(const exprt &expr)
   return result;
 }
 
+dereference_exprt
+element_at_pointer_array_index(const exprt &pointer, const exprt &index)
+{
+  return dereference_exprt{plus_exprt{pointer, index}};
+}
+
 /// Finds the corresponding closing delimiter to the given opening delimiter. It
 /// is assumed that \p open_pos points to the opening delimiter \p open_char in
 /// the \p src string. The depth of nesting is counted to identify the correct

jbmc/src/java_bytecode/java_utils.h

@@ -81,6 +81,20 @@ irep_idt resolve_friendly_method_name(
 /// \param expr: expression to dereference and check
 dereference_exprt checked_dereference(const exprt &expr);
 
+/// Generate statement using pointer arithmetic to access the element at the
+/// given index of a pointer array:
+/// `*(pointer + index)`
+/// In JBMC, an array is generally represented as a pointer to its first
+/// element. This is because we cannot know the type of an array of
+/// nondeterministic length, as the length is part of any array type. But we do
+/// know the type of the first element of the array, so we work with that
+/// instead.
+/// \param pointer: pointer to the first element of an array
+/// \param index: index of the element to access
+/// \return expression representing the (index)'th element of the array
+dereference_exprt
+element_at_pointer_array_index(const exprt &pointer, const exprt &index);
+
 /// Add the components in components_to_add to the class denoted
 /// by class symbol.
 /// \param class_symbol: The symbol representing the class we want to modify.