From 2fc6f099d5c5dba5e502dee5fa9ba0eedf36c396 Mon Sep 17 00:00:00 2001
From: Chris Smowton <chris@smowton.net>
Date: Fri, 29 Jul 2016 15:41:47 +0100
Subject: [PATCH] Preserve true array type in Java -> GOTO conversion. Fixes
 #184.

Previously all object array allocations became a generic void** when
a Java-new operator was lowered into a CPP-new one. Now the type is
preserved and is therefore available in the symbol table to build an
appropriate source-level type during testcase generation.
---
 src/goto-programs/builtin_functions.cpp | 37 +++++++++++++++++++++++--
 1 file changed, 34 insertions(+), 3 deletions(-)

diff --git a/src/goto-programs/builtin_functions.cpp b/src/goto-programs/builtin_functions.cpp
index d5e27615d3d..63eb18ec549 100644
--- a/src/goto-programs/builtin_functions.cpp
+++ b/src/goto-programs/builtin_functions.cpp
@@ -830,10 +830,41 @@ void goto_convertt::do_java_new_array(
     deref,
     struct_type.components()[2].get_name(),
     struct_type.components()[2].type());
-  side_effect_exprt data_cpp_new_expr(ID_cpp_new_array, data.type());
+
+  // Allocate a (struct realtype**) instead of a (void**) if possible.
+  const irept &given_element_type=object_type.find(ID_C_element_type);
+  typet allocate_data_type;
+  exprt cast_data_member;
+  if(given_element_type.is_not_nil())
+  {
+    allocate_data_type=
+      pointer_typet(static_cast<const typet &>(given_element_type));
+  }
+  else
+    allocate_data_type=data.type();
+
+  side_effect_exprt data_cpp_new_expr(ID_cpp_new_array, allocate_data_type);
   data_cpp_new_expr.set(ID_size, rhs.op0());
+
+  // Must directly assign the new array to a temporary
+  // because goto-symex will notice `x=side_effect_exprt` but not
+  // `x=typecast_exprt(side_effect_exprt(...))`
+  symbol_exprt new_array_data_symbol=
+    new_tmp_symbol(
+      data_cpp_new_expr.type(),
+      "new_array_data",
+      dest,
+      location)
+    .symbol_expr();
+  goto_programt::targett t_p2=dest.add_instruction(ASSIGN);
+  t_p2->code=code_assignt(new_array_data_symbol, data_cpp_new_expr);
+  t_p2->source_location=location;
+
   goto_programt::targett t_p=dest.add_instruction(ASSIGN);
-  t_p->code=code_assignt(data, data_cpp_new_expr);
+  exprt cast_cpp_new=new_array_data_symbol;
+  if(cast_cpp_new.type()!=data.type())
+    cast_cpp_new=typecast_exprt(cast_cpp_new, data.type());
+  t_p->code=code_assignt(data, cast_cpp_new);
   t_p->source_location=location;
 
   // zero-initialize the data
@@ -846,7 +877,7 @@ void goto_convertt::do_java_new_array(
         ns,
         get_message_handler());
     codet array_set(ID_array_set);
-    array_set.copy_to_operands(data, zero_element);
+    array_set.copy_to_operands(new_array_data_symbol, zero_element);
     goto_programt::targett t_d=dest.add_instruction(OTHER);
     t_d->code=array_set;
     t_d->source_location=location;