Make given_length_expr argument non-optional

This simplifies the logic in assign_array_from_json and makes its
specification simpler.

Author: romainbrenguier

jbmc/src/java_bytecode/assignments_from_json.cpp

@@ -458,55 +458,42 @@ static symbol_exprt nondet_length(
 
 /// One of the cases in the recursive algorithm: the case where \p expr
 /// represents an array.
-/// The length of the array is given by a symbol: \p given_length_expr if it is
-/// specified (this will be the case when there are two or more reference-equal
-/// arrays), or a fresh symbol otherwise.
-/// If \p given_length_expr is specified, we assume that an array with this
-/// symbol as its length has already been allocated and that \p expr has been
-/// assigned to it.
-/// Either way, the length symbol stores a nondet integer, and we add
-/// constraints on this: if "nondetLength" is specified in \p json, then the
-/// number of elements specified in \p json should be the minimum length of the
-/// array. Otherwise the number of elements should be the exact length of the
-/// array.
+/// The length of the array is given by symbol \p given_length_expr.
+/// We assume that an array with this symbol as its length has already been
+/// allocated and that \p expr has been assigned to it.
+/// We add constraints on the length: if "nondetLength" is specified in \p json,
+/// then the number of elements specified in \p json should be less than or
+/// equal to the length of the array. Otherwise the number of elements should be
+/// the exact length of the array.
 /// For the assignment of the array elements, see
 /// \ref assign_array_data_component_from_json.
 /// For the overall algorithm, see \ref assign_from_json_rec.
 static void assign_array_from_json(
   const exprt &expr,
   const jsont &json,
-  const optionalt<symbol_exprt> &given_length_expr,
+  const exprt &given_length_expr,
   const optionalt<std::string> &type_from_array,
   object_creation_infot &info)
 {
   PRECONDITION(is_java_array_type(expr.type()));
   const auto &element_type =
     java_array_element_type(to_struct_tag_type(expr.type().subtype()));
-
-  const exprt length_expr = [&] {
-    if(given_length_expr)
-      return *given_length_expr;
-    const symbol_exprt length =
-      nondet_length(info.allocate_objects, info.block, info.loc);
-    allocate_array(expr, length, info);
-    return length;
-  }();
   const json_arrayt json_array = get_untyped_array(json, element_type);
   const auto number_of_elements =
     from_integer(json_array.size(), java_int_type());
   info.block.add(code_assumet{
-    binary_predicate_exprt{length_expr, ID_ge, number_of_elements}});
+    binary_predicate_exprt{given_length_expr, ID_ge, number_of_elements}});
   if(has_nondet_length(json))
   {
     info.block.add(code_assumet{binary_predicate_exprt{
-      length_expr,
+      given_length_expr,
       ID_le,
       from_integer(info.max_user_array_length, java_int_type())}});
   }
   else
   {
     info.block.add(code_assumet{
-      binary_predicate_exprt{length_expr, ID_le, number_of_elements}});
+      binary_predicate_exprt{given_length_expr, ID_le, number_of_elements}});
   }
   assign_array_data_component_from_json(expr, json, type_from_array, info);
 }
@@ -784,8 +771,10 @@ static void assign_reference_from_json(
   {
     if(is_java_array_type(expr.type()))
     {
+      INVARIANT(
+        reference.array_length, "an array reference should store its length");
       assign_array_from_json(
-        reference.expr, json, reference.array_length, type_from_array, info);
+        reference.expr, json, *reference.array_length, type_from_array, info);
     }
     else
       assign_struct_from_json(dereference_exprt(reference.expr), json, info);
@@ -823,7 +812,12 @@ void assign_from_json_rec(
       assign_reference_from_json(expr, json, type_from_array, info);
     }
     else if(is_java_array_type(expr.type()))
-      assign_array_from_json(expr, json, {}, type_from_array, info);
+    {
+      const exprt length =
+        nondet_length(info.allocate_objects, info.block, info.loc);
+      allocate_array(expr, length, info);
+      assign_array_from_json(expr, json, length, type_from_array, info);
+    }
     else if(
       const auto runtime_type =
         ::runtime_type(json, type_from_array, info.symbol_table))