Implement Java array.clone (#774)

This simply duplicates the contents of an array. Regrettably it uses
a loop to do so at this point because if we use ARRAY_COPY the backend
dies when it can't conclusively establish that the actual parameters have
like type. Some sort of copy-type-from intrinsic would do this, but is
more effort than is sensible to make right now.

Author: smowton

regression/cbmc-java/enum1/test.desc

@@ -1,7 +1,8 @@
 CORE
 enum1.class
 --java-unwind-enum-static --unwind 3
-^EXIT=10$
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
 ^SIGNAL=0$
 ^Unwinding loop java::enum1.<clinit>:\(\)V.0 iteration 5 \(6 max\) file enum1.java line 6 function java::enum1.<clinit>:\(\)V bytecode_index 78 thread 0$
 --

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -19,6 +19,7 @@ Author: Daniel Kroening, [email protected]
 #include "java_bytecode_convert_method.h"
 #include "java_bytecode_language.h"
 
+#include <util/arith_tools.h>
 #include <util/namespace.h>
 #include <util/std_expr.h>
 
@@ -311,6 +312,122 @@ void java_bytecode_convert_classt::add_array_types()
     symbol.is_type=true;
     symbol.type=struct_type;
     symbol_table.add(symbol);
+
+    // Also provide a clone method:
+    // ----------------------------
+
+    const irep_idt clone_name=
+      id2string(symbol_type.get_identifier())+".clone:()Ljava/lang/Object;";
+    code_typet clone_type;
+    clone_type.return_type()=
+      pointer_typet(symbol_typet("java::java.lang.Object"));
+    code_typet::parametert this_param;
+    this_param.set_identifier(id2string(clone_name)+"::this");
+    this_param.set_base_name("this");
+    this_param.set_this();
+    this_param.type()=pointer_typet(symbol_type);
+    clone_type.parameters().push_back(this_param);
+
+    parameter_symbolt this_symbol;
+    this_symbol.name=this_param.get_identifier();
+    this_symbol.base_name=this_param.get_base_name();
+    this_symbol.pretty_name=this_symbol.base_name;
+    this_symbol.type=this_param.type();
+    this_symbol.mode=ID_java;
+    symbol_table.add(this_symbol);
+
+    const irep_idt local_name=
+      id2string(clone_name)+"::cloned_array";
+    auxiliary_symbolt local_symbol;
+    local_symbol.name=local_name;
+    local_symbol.base_name="cloned_array";
+    local_symbol.pretty_name=local_symbol.base_name;
+    local_symbol.type=pointer_typet(symbol_type);
+    local_symbol.mode=ID_java;
+    symbol_table.add(local_symbol);
+    const auto &local_symexpr=local_symbol.symbol_expr();
+
+    code_blockt clone_body;
+
+    code_declt declare_cloned(local_symexpr);
+    clone_body.move_to_operands(declare_cloned);
+
+    side_effect_exprt java_new_array(
+      ID_java_new_array,
+      pointer_typet(symbol_type));
+    dereference_exprt old_array(this_symbol.symbol_expr(), symbol_type);
+    dereference_exprt new_array(local_symexpr, symbol_type);
+    member_exprt old_length(old_array, comp1.get_name(), comp1.type());
+    java_new_array.copy_to_operands(old_length);
+    code_assignt create_blank(local_symexpr, java_new_array);
+    clone_body.move_to_operands(create_blank);
+
+
+    member_exprt old_data(old_array, comp2.get_name(), comp2.type());
+    member_exprt new_data(new_array, comp2.get_name(), comp2.type());
+
+    /*
+      // TODO use this instead of a loop.
+    codet array_copy;
+    array_copy.set_statement(ID_array_copy);
+    array_copy.move_to_operands(new_data);
+    array_copy.move_to_operands(old_data);
+    clone_body.move_to_operands(array_copy);
+    */
+
+    // Begin for-loop to replace:
+
+    const irep_idt index_name=
+      id2string(clone_name)+"::index";
+    auxiliary_symbolt index_symbol;
+    index_symbol.name=index_name;
+    index_symbol.base_name="index";
+    index_symbol.pretty_name=index_symbol.base_name;
+    index_symbol.type=comp1.type();
+    index_symbol.mode=ID_java;
+    symbol_table.add(index_symbol);
+    const auto &index_symexpr=index_symbol.symbol_expr();
+
+    code_declt declare_index(index_symexpr);
+    clone_body.move_to_operands(declare_index);
+
+    code_fort copy_loop;
+
+    copy_loop.init()=
+      code_assignt(index_symexpr, from_integer(0, index_symexpr.type()));
+    copy_loop.cond()=
+      binary_relation_exprt(index_symexpr, ID_lt, old_length);
+
+    side_effect_exprt inc(ID_assign);
+    inc.operands().resize(2);
+    inc.op0()=index_symexpr;
+    inc.op1()=plus_exprt(index_symexpr, from_integer(1, index_symexpr.type()));
+    copy_loop.iter()=inc;
+
+    dereference_exprt old_cell(
+      plus_exprt(old_data, index_symexpr), old_data.type().subtype());
+    dereference_exprt new_cell(
+      plus_exprt(new_data, index_symexpr), new_data.type().subtype());
+    code_assignt copy_cell(new_cell, old_cell);
+    copy_loop.body()=copy_cell;
+
+    // End for-loop
+    clone_body.move_to_operands(copy_loop);
+
+    member_exprt new_base_class(new_array, comp0.get_name(), comp0.type());
+    address_of_exprt retval(new_base_class);
+    code_returnt return_inst(retval);
+    clone_body.move_to_operands(return_inst);
+
+    symbolt clone_symbol;
+    clone_symbol.name=clone_name;
+    clone_symbol.pretty_name=
+      id2string(symbol_type.get_identifier())+".clone:()";
+    clone_symbol.base_name="clone";
+    clone_symbol.type=clone_type;
+    clone_symbol.value=clone_body;
+    clone_symbol.mode=ID_java;
+    symbol_table.add(clone_symbol);
   }
 }