From 2a22a2e61c18348049b6e21e7e5c2b6582ae2554 Mon Sep 17 00:00:00 2001
From: Romain Brenguier <romain.brenguier@gmail.com>
Date: Wed, 22 Nov 2017 15:25:51 +0000
Subject: [PATCH] Fix allocation of infinite char arrays

Infinite char arrays used in string need to be dynamically allocated
instead of being on the stack as it used to be.
---
 src/java_bytecode/java_object_factory.cpp     | 53 +++++++++++++++----
 .../java_string_library_preprocess.cpp        |  1 +
 2 files changed, 45 insertions(+), 9 deletions(-)

diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp
index 5c05b26c295..18fe7238fba 100644
--- a/src/java_bytecode/java_object_factory.cpp
+++ b/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 = { .@java.lang.Object={
+///   .@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,14 +611,29 @@ 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);
@@ -608,6 +641,8 @@ codet initialize_nondet_string_struct(
     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)
     {
diff --git a/src/java_bytecode/java_string_library_preprocess.cpp b/src/java_bytecode/java_string_library_preprocess.cpp
index 6c040a5a759..2c6df028b9d 100644
--- a/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/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());