Java object factory: allocate fixed length arrays

This replaces the variable-length arrays produced by the Java object
factory with fixed-length ones annotated with a variable length member.
This allows the backend to use the much cheaper fixed-length array lowering
rather than the full variable-length array theory, while retaining the
ability for the effective length to vary. In effect this creates a bounded-
length array construct.

Fixes diffblue#746

Author: smowton

src/goto-programs/builtin_functions.cpp

@@ -824,7 +824,17 @@ void goto_convertt::do_java_new_array(
     struct_type.components()[2].get_name(),
     struct_type.components()[2].type());
   side_effect_exprt data_cpp_new_expr(ID_cpp_new_array, data.type());
-  data_cpp_new_expr.set(ID_size, rhs.op0());
+
+  // The instruction may specify a (hopefully small) upper bound on the
+  // array size, in which case we allocate a fixed-length array that may
+  // be larger than the `length` member rather than use a true variable-
+  // length array, which produces a more complex formula in the current
+  // backend.
+  const irept size_bound=rhs.find(ID_length_upper_bound);
+  if(size_bound.is_nil())
+    data_cpp_new_expr.set(ID_size, rhs.op0());
+  else
+    data_cpp_new_expr.set(ID_size, size_bound);
   goto_programt::targett t_p=dest.add_instruction(ASSIGN);
   t_p->code=code_assignt(data, data_cpp_new_expr);
   t_p->source_location=location;

src/java_bytecode/java_object_factory.cpp

@@ -386,6 +386,7 @@ void java_object_factoryt::gen_nondet_array_init(
 
   side_effect_exprt java_new_array(ID_java_new_array, expr.type());
   java_new_array.copy_to_operands(length_sym_expr);
+  java_new_array.set(ID_length_upper_bound, max_length_expr);
   java_new_array.type().subtype().set(ID_C_element_type, element_type);
   codet assign=code_assignt(expr, java_new_array);
   assign.add_source_location()=loc;

src/util/irep_ids.def

@@ -741,6 +741,7 @@ IREP_ID_ONE(java_instanceof)
 IREP_ID_ONE(java_super_method_call)
 IREP_ID_ONE(java_enum_static_unwind)
 IREP_ID_ONE(push_catch)
+IREP_ID_ONE(length_upper_bound)
 IREP_ID_ONE(string_constraint)
 IREP_ID_ONE(string_not_contains_constraint)
 IREP_ID_ONE(cprover_char_literal_func)