Fix multinewarray

* Always init subarrays with correct type, rather than trying to use a member of (void**)data to do init.
* Use a for-loop, not array-set, for zero init. This is how C memset gets implemented anyhow, and array_set depends on the symex pass lowering the array to a static global object, which is likely not to happen for subarrays.

Author: smowton

src/goto-programs/builtin_functions.cpp

@@ -6,6 +6,7 @@ Author: Daniel Kroening, [email protected]
 
 \*******************************************************************/
 
+#include <iostream>
 #include <cassert>
 
 #include <util/i2string.h>
@@ -675,7 +676,7 @@ void goto_convertt::do_java_new_array(
 {
   if(lhs.is_nil())
     throw "do_java_new_array without lhs is yet to be implemented";
-    
+
   source_locationt location=rhs.source_location();
 
   assert(rhs.operands().size()>=1); // one per dimension
@@ -718,7 +719,7 @@ void goto_convertt::do_java_new_array(
 
   // Allocate a (struct realtype**) instead of a (void**) if possible,
   // to avoid confusing the trace due to dynamic type aliasing.
-  const irept& given_element_type=rhs.find(ID_C_element_type);
+  const irept& given_element_type=object_type.find(ID_C_element_type);
   typet allocate_data_type;
   exprt cast_data_member;
   if(given_element_type!=get_nil_irep())
@@ -745,22 +746,16 @@ void goto_convertt::do_java_new_array(
   t_p->code=code_assignt(data,cast_cpp_new);
   t_p->source_location=location;
 
-  // zero-initialize the data
+  // zero-initialize the data, or create subarrays if specified:
   if(!rhs.get_bool("skip_initialise"))
-  {
-    exprt zero_element=gen_zero(data.type().subtype());
-    codet array_set(ID_array_set);
-    array_set.copy_to_operands(data, zero_element);
-    goto_programt::targett t_d=dest.add_instruction(OTHER);
-    t_d->code=array_set;
-    t_d->source_location=location;
-  }
-
-  if(rhs.operands().size()>=2)
   {
     // produce
-    // for(int i=0; i<size; i++) tmp[i]=java_new(dim-1);
+    // for(int i=0; i<size; i++) { init=java_new(dim-1); tmp[i]=init; }
+    // or init=0 if this is the last dimension.
     // This will be converted recursively.
+
+    // Since reference arrays carry void*, init using a local variable
+    // before assigning to the array.
 
     goto_programt tmp;
 
@@ -769,21 +764,38 @@ void goto_convertt::do_java_new_array(
 
     code_fort for_loop;
 
-    side_effect_exprt sub_java_new=rhs;
-    sub_java_new.operands().erase(sub_java_new.operands().begin());
-    
     side_effect_exprt inc(ID_assign);
     inc.operands().resize(2);
     inc.op0()=tmp_i;
     inc.op1()=plus_exprt(tmp_i, gen_one(tmp_i.type()));
 
-    dereference_exprt deref_expr(plus_exprt(data, tmp_i), data.type().subtype());
-    
     for_loop.init()=code_assignt(tmp_i, gen_zero(tmp_i.type()));
     for_loop.cond()=binary_relation_exprt(tmp_i, ID_lt, rhs.op0());
     for_loop.iter()=inc;
-    for_loop.body()=code_skipt();
-    for_loop.body()=code_assignt(deref_expr, sub_java_new);
+
+    code_blockt for_body;
+    dereference_exprt deref_expr(plus_exprt(data, tmp_i), data.type().subtype());
+    
+    if(rhs.operands().size() >= 2)
+    {
+      side_effect_exprt sub_java_new=rhs;
+      sub_java_new.operands().erase(sub_java_new.operands().begin());
+      sub_java_new.type()=static_cast<const typet &>(given_element_type);
+      exprt next_array_init=
+        new_tmp_symbol(sub_java_new.type(), "multiarray_init", tmp, location).symbol_expr();
+      for_body.copy_to_operands(code_assignt(next_array_init, sub_java_new));
+
+      if(deref_expr.type()!=next_array_init.type())
+        next_array_init=typecast_exprt(next_array_init, deref_expr.type());
+      for_body.copy_to_operands(code_assignt(deref_expr, next_array_init));
+    }
+    else
+    {
+      exprt zero_element=gen_zero(deref_expr.type());
+      for_body.copy_to_operands(code_assignt(deref_expr,zero_element));
+    }
+      
+    for_loop.body()=for_body;
 
     convert(for_loop, tmp);
     dest.destructive_append(tmp);

src/java_bytecode/java_bytecode_convert.cpp

@@ -1448,16 +1448,15 @@ codet java_bytecode_convertt::convert_instructions(
     }
     else if(statement=="multianewarray")
     {
-      // The first argument is the type, the second argument is the dimension.
+      // The first argument is the type, the second argument is the number of dimensions.
       // The size of each dimension is on the stack.
       irep_idt number=to_constant_expr(arg1).get_value();
       unsigned dimension=safe_c_str2unsigned(number.c_str());
 
       op=pop(dimension);
       assert(results.size()==1);
 
-      // arg0.type()
-      const pointer_typet ref_type=java_array_type('a');
+      const pointer_typet ref_type=pointer_typet(arg0.type());
 
       side_effect_exprt java_new_array(ID_java_new_array, ref_type);
       java_new_array.operands()=op;

src/java_bytecode/java_object_factory.cpp

@@ -310,7 +310,7 @@ void gen_nondet_array_init(const exprt &expr,
   side_effect_exprt java_new_array(ID_java_new_array,expr.type());
   java_new_array.copy_to_operands(length_sym_expr);
   java_new_array.set("skip_initialise",true);
-  java_new_array.set(ID_C_element_type,element_type);
+  java_new_array.type().subtype().set(ID_C_element_type,element_type);
   init_code.copy_to_operands(code_assignt(expr,java_new_array));
 
   exprt init_array_expr=member_exprt(dereference_exprt(expr, expr.type().subtype()),