Merge pull request #1615 from romainbrenguier/bugfix/string-allocation#TG1619

Fix problem with string data allocation TG-1612

Author: romainbrenguier

src/java_bytecode/java_object_factory.cpp

@@ -511,6 +511,19 @@ 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);
+  alloc.copy_to_operands(size);
+  alloc.copy_to_operands(false_exprt());
+  alloc.type() = lhs.type();
+  return code_assignt(lhs, alloc);
+}
+
 /// Initialize a nondeterministic String structure
 /// \param obj: struct to initialize, must have been declared using
 ///   code of the form:
@@ -527,15 +540,19 @@ static mp_integer max_value(const typet &type)
 /// tmp_object_factory$1 = NONDET(int);
 /// __CPROVER_assume(tmp_object_factory$1 >= 0);
 /// __CPROVER_assume(tmp_object_factory$1 <= max_nondet_string_length);
+/// char (*string_data_pointer)[INFINITY()];
+/// string_data_pointer = ALLOCATE(char [INFINITY()], INFINITY(), false);
 /// char nondet_infinite_array$2[INFINITY()];
 /// nondet_infinite_array$2 = NONDET(char [INFINITY()]);
-/// cprover_associate_array_to_pointer_func
-///   (nondet_infinite_array$2, &nondet_infinite_array$2[0]);
-/// prover_associate_length_to_array_func
-///   (nondet_infinite_array$2, tmp_object_factory$1);
-/// arg = { .\@java.lang.Object={ .\@class_identifier="java.lang.String",
-///   .\@lock=false }, .length=tmp_object_factory$1,
-///   .data=nondet_infinite_array$2 };
+/// *string_data_pointer = nondet_infinite_array$2;
+/// cprover_associate_array_to_pointer_func(
+///   *string_data_pointer, *string_data_pointer);
+/// cprover_associate_length_to_array_func(
+///   *string_data_pointer, tmp_object_factory);
+/// arg = { [email protected]={
+///   .@class_identifier=\"java::java.lang.String\", .@lock=false },
+///   .length=tmp_object_factory,
+///   .data=*string_data_pointer };
 /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 /// Unit tests in `unit/java_bytecode/java_object_factory/` ensure
 /// it is the case.
@@ -570,6 +587,7 @@ codet initialize_nondet_string_struct(
   // just contains the standard Object field and no length and data fields.
   if(struct_type.has_component("length"))
   {
+    /// \todo Refactor with make_nondet_string_expr
     // length_expr = nondet(int);
     const symbolt length_sym =
       new_tmp_symbol(symbol_table, loc, java_int_type());
@@ -593,21 +611,38 @@ codet initialize_nondet_string_struct(
         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
-    exprt data_expr = make_nondet_infinite_char_array(symbol_table, loc, code);
+    const dereference_exprt data_expr(data_pointer);
+    const exprt nondet_array =
+      make_nondet_infinite_char_array(symbol_table, loc, code);
+    code.add(code_assignt(data_expr, nondet_array));
 
     struct_expr.copy_to_operands(length_expr);
 
     const address_of_exprt array_pointer(
       index_exprt(data_expr, from_integer(0, java_int_type())));
-    struct_expr.copy_to_operands(array_pointer);
 
     add_pointer_to_array_association(
       array_pointer, data_expr, symbol_table, loc, code);
 
     add_array_to_length_association(
       data_expr, length_expr, symbol_table, loc, code);
 
+    struct_expr.copy_to_operands(array_pointer);
+
     // Printable ASCII characters are between ' ' and '~'.
     if(printable)
     {

src/java_bytecode/java_string_library_preprocess.cpp

@@ -519,6 +519,7 @@ refined_string_exprt java_string_library_preprocesst::make_nondet_string_expr(
   symbol_table_baset &symbol_table,
   code_blockt &code)
 {
+  /// \todo refactor with initialize_nonddet_string_struct
   const refined_string_exprt str = decl_string_expr(loc, symbol_table, code);
 
   side_effect_expr_nondett nondet_length(str.length().type());
@@ -1695,14 +1696,6 @@ codet java_string_library_preprocesst::make_init_from_array_code(
   /// \todo this assumes the array to be constant between all calls to
   /// string primitives, which may not be true in general.
   refined_string_exprt string_arg = to_string_expr(args[1]);
-  add_pointer_to_array_association(
-    string_arg.content(),
-    dereference_exprt(
-      string_arg.content(),
-      array_typet(java_char_type(), infinity_exprt(java_int_type()))),
-    symbol_table,
-    loc,
-    code);
 
   // The third argument is `count`, whereas the third argument of substring
   // is `end` which corresponds to `offset+count`

src/solvers/refinement/string_constraint_generator_main.cpp

@@ -270,7 +270,10 @@ exprt string_constraint_generatort::associate_array_to_pointer(
 
   /// \todo We should use a function for inserting the correspondance
   /// between array and pointers.
-  arrays_of_pointers_.insert(std::make_pair(pointer_expr, array_expr));
+  const auto it_bool =
+    arrays_of_pointers_.insert(std::make_pair(pointer_expr, array_expr));
+  INVARIANT(
+    it_bool.second, "should not associate two arrays to the same pointer");
   add_default_axioms(to_array_string_expr(array_expr));
   return from_integer(0, f.type());
 }

unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp

@@ -70,18 +70,22 @@ SCENARIO(
           "tmp_object_factory = NONDET(int);",
           "__CPROVER_assume(tmp_object_factory >= 0);",
           "__CPROVER_assume(tmp_object_factory <= 20);",
+          "char (*string_data_pointer)[INFINITY()];",
+          "string_data_pointer = "
+            "ALLOCATE(char [INFINITY()], INFINITY(), false);",
           "char nondet_infinite_array[INFINITY()];",
           "nondet_infinite_array = NONDET(char [INFINITY()]);",
+          "*string_data_pointer = nondet_infinite_array;",
           "int return_array;",
           "return_array = cprover_associate_array_to_pointer_func"
-          "(nondet_infinite_array, nondet_infinite_array);",
+            "(*string_data_pointer, *string_data_pointer);",
           "int return_array;",
           "return_array = cprover_associate_length_to_array_func"
-          "(nondet_infinite_array, tmp_object_factory);",
+            "(*string_data_pointer, tmp_object_factory);",
           "arg = { [email protected]={ .@class_identifier"
-          "=\"java::java.lang.String\", .@lock=false },"
-          " .length=tmp_object_factory, "
-          ".data=nondet_infinite_array };"};
+            "=\"java::java.lang.String\", .@lock=false },"
+            " .length=tmp_object_factory, "
+            ".data=*string_data_pointer };"};
 
         for(std::size_t i = 0;
             i < code_string.size() && i < reference_code.size();