quick fix #8428 jbmc array unsoundness

Author: lks9

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -1143,17 +1143,16 @@ static void allocate_nondet_length_array(
   const allocate_local_symbolt &allocate_local_symbol,
   const source_locationt &location)
 {
-  const auto &length_sym_expr = generate_nondet_int(
-    from_integer(0, java_int_type()),
-    max_length_expr,
+  const auto &length_sym_expr = gen_positive_nondet_int(
     "nondet_array_length",
+    java_int_type(),
     location,
     allocate_local_symbol,
     assignments);
 
   side_effect_exprt java_new_array(ID_java_new_array, lhs.type(), location);
   java_new_array.copy_to_operands(length_sym_expr);
-  java_new_array.set(ID_length_upper_bound, max_length_expr);
+  //java_new_array.set(ID_length_upper_bound, max_length_expr);
   to_type_with_subtype(java_new_array.type())
     .subtype()
     .set(ID_element_type, element_type);

jbmc/src/java_bytecode/nondet.cpp

@@ -88,6 +88,34 @@ symbol_exprt generate_nondet_int(
     instructions);
 }
 
+symbol_exprt gen_positive_nondet_int(
+  const std::string &basename_prefix,
+  const typet &int_type,
+  const source_locationt &source_location,
+  const allocate_local_symbolt &alocate_local_symbol,
+  code_blockt &instructions)
+{
+  const exprt min_value_expr = from_integer(0, int_type);
+
+  // Declare a symbol for the non deterministic integer.
+  const symbol_exprt &nondet_symbol =
+    alocate_local_symbol(int_type, basename_prefix);
+  instructions.add(code_frontend_declt(nondet_symbol));
+
+  // Assign the symbol any non deterministic integer value.
+  //   int_type name_prefix::nondet_int = NONDET(int_type)
+  instructions.add(code_frontend_assignt(
+    nondet_symbol, side_effect_expr_nondett(int_type, source_location)));
+
+  // Constrain the non deterministic integer with a lower bound of `min_value`.
+  //   ASSUME(name_prefix::nondet_int >= min_value)
+  instructions.add(
+    code_assumet(binary_predicate_exprt(nondet_symbol, ID_ge, min_value_expr)));
+
+  return nondet_symbol;
+}
+
+
 code_blockt generate_nondet_switch(
   const irep_idt &name_prefix,
   const alternate_casest &switch_cases,

jbmc/src/java_bytecode/nondet.h

@@ -79,6 +79,28 @@ symbol_exprt generate_nondet_int(
   allocate_objectst &allocate_objects,
   code_blockt &instructions);
 
+/// Gets a fresh nondet choice in range >= 0. GOTO generated
+/// resembles:
+/// ```
+/// int_type name_prefix::nondet_int = NONDET(int_type)
+/// ASSUME(name_prefix::nondet_int >= 0)
+/// ```
+/// \param basename_prefix: Basename prefix for the fresh symbol name generated.
+/// \param int_type: The type of the int used to non-deterministically choose
+///   one of the switch cases.
+/// \param source_location: The location to mark the generated int with.
+/// \param allocate_local_symbol: Handles allocation of new objects.
+/// \param [out] instructions: Output instructions are written to
+///   'instructions'. These declare, nondet-initialise and range-constrain (with
+///   assume statements) a fresh integer.
+/// \return Returns a symbol expression for the resulting integer.
+symbol_exprt gen_positive_nondet_int(
+  const std::string &basename_prefix,
+  const typet &int_type,
+  const source_locationt &source_location,
+  const allocate_local_symbolt &alocate_local_symbol,
+  code_blockt &instructions);
+
 typedef std::vector<codet> alternate_casest;
 
 /// Pick nondeterministically between imperative actions 'switch_cases'.