Merge pull request #3259 from romainbrenguier/bugfix/allocate-nondet-char-array

Allocate nondet char array

Author: romainbrenguier

jbmc/src/java_bytecode/java_object_factory.cpp

@@ -526,18 +526,6 @@ static mp_integer max_value(const typet &type)
   UNREACHABLE;
 }
 
-/// Create code allocating object of size `size` and assigning it to `lhs`
-/// \param lhs : pointer which will be allocated
-/// \param size : size of the object
-/// \return code allocation object and assigning `lhs`
-static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
-{
-  side_effect_exprt alloc(ID_allocate, lhs.type(), lhs.source_location());
-  alloc.copy_to_operands(size);
-  alloc.copy_to_operands(false_exprt());
-  return code_assignt(lhs, alloc);
-}
-
 /// Check if a structure is a nondeterministic String structure, and if it is
 /// initialize its length and data fields.
 /// \param struct_expr [out]: struct that we may initialize
@@ -648,25 +636,8 @@ bool initialize_nondet_string_fields(
       code_assumet(binary_relation_exprt(length_expr, ID_le, max_length)));
   }
 
-  // char (*array_data_init)[INFINITY];
-  const typet data_ptr_type = pointer_type(
-    array_typet(java_char_type(), infinity_exprt(java_int_type())));
-
-  symbolt &data_pointer_sym = get_fresh_aux_symbol(
-    data_ptr_type, "", "string_data_pointer", loc, ID_java, symbol_table);
-  const auto data_pointer = data_pointer_sym.symbol_expr();
-  code.add(code_declt(data_pointer));
-
-  // Dynamic allocation: `data array = allocate char[INFINITY]`
-  code.add(make_allocate_code(data_pointer, infinity_exprt(java_int_type())));
-
-  // `data_expr` is `*data_pointer`
-  // data_expr = nondet(char[INFINITY]) // we use infinity for variable size
-  const dereference_exprt data_expr(data_pointer);
-  const exprt nondet_array =
+  const exprt data_expr =
     make_nondet_infinite_char_array(symbol_table, loc, function_id, code);
-  code.add(code_assignt(data_expr, nondet_array));
-
   struct_expr.operands()[struct_type.component_number("length")] = length_expr;
 
   const address_of_exprt array_pointer(

jbmc/src/java_bytecode/java_string_library_preprocess.cpp

@@ -617,6 +617,18 @@ codet java_string_library_preprocesst::code_return_function_application(
   return code_returnt(fun_app);
 }
 
+/// Create code allocating object of size `size` and assigning it to `lhs`
+/// \param lhs : pointer which will be allocated
+/// \param size : size of the object
+/// \return code allocation object and assigning `lhs`
+static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size)
+{
+  side_effect_exprt alloc(ID_allocate, lhs.type(), lhs.source_location());
+  alloc.add_to_operands(size);
+  alloc.add_to_operands(false_exprt());
+  return code_assignt(lhs, alloc);
+}
+
 /// Declare a fresh symbol of type array of character with infinite size.
 /// \param symbol_table: the symbol table
 /// \param loc: source location
@@ -632,17 +644,20 @@ exprt make_nondet_infinite_char_array(
   const array_typet array_type(
     java_char_type(), infinity_exprt(java_int_type()));
   const symbolt data_sym = get_fresh_aux_symbol(
-    array_type,
+    pointer_type(array_type),
     id2string(function_id),
-    "nondet_infinite_array",
+    "nondet_infinite_array_pointer",
     loc,
     ID_java,
     symbol_table);
-  const symbol_exprt data_expr = data_sym.symbol_expr();
-  code.add(code_declt(data_expr), loc);
-  const side_effect_expr_nondett nondet_data(data_expr.type(), loc);
-  code.add(code_assignt(data_expr, nondet_data), loc);
-  return data_expr;
+
+  const symbol_exprt data_pointer = data_sym.symbol_expr();
+  code.add(code_declt(data_pointer));
+  code.add(make_allocate_code(data_pointer, array_type.size()));
+  const exprt nondet_data = side_effect_expr_nondett(array_type, loc);
+  const exprt data = dereference_exprt(data_pointer, array_type);
+  code.add(code_assignt(data, nondet_data), loc);
+  return data;
 }
 
 /// Add a call to a primitive of the string solver, letting it know that

jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp

@@ -84,22 +84,20 @@ SCENARIO(
           "tmp_object_factory = NONDET(int);",
           CPROVER_PREFIX "assume(tmp_object_factory >= 0);",
           CPROVER_PREFIX "assume(tmp_object_factory <= 20);",
-          "char (*string_data_pointer)[INFINITY()];",
-          "string_data_pointer = "
+          "char (*nondet_infinite_array_pointer)[INFINITY()];",
+          "nondet_infinite_array_pointer = "
             "ALLOCATE(char [INFINITY()], INFINITY(), false);",
-          "char nondet_infinite_array[INFINITY()];",
-          "nondet_infinite_array = NONDET(char [INFINITY()]);",
-          "*string_data_pointer = nondet_infinite_array;",
+          "*nondet_infinite_array_pointer = NONDET(char [INFINITY()]);",
           "int return_array;",
           "return_array = cprover_associate_array_to_pointer_func"
-            "(*string_data_pointer, *string_data_pointer);",
+            "(*nondet_infinite_array_pointer, *nondet_infinite_array_pointer);",
           "int return_array;",
           "return_array = cprover_associate_length_to_array_func"
-            "(*string_data_pointer, tmp_object_factory);",
+            "(*nondet_infinite_array_pointer, tmp_object_factory);",
           "arg = { [email protected]={ .@class_identifier"
             "=\"java::java.lang.String\" },"
             " .length=tmp_object_factory, "
-            ".data=*string_data_pointer };"};
+            ".data=*nondet_infinite_array_pointer };"};
         // clang-format on
 
         for(std::size_t i = 0;