Merge pull request diffblue#1778 from peterschrammel/java-array-is-object

Java arrays are instanceof Object

Author: peterschrammel

regression/cbmc-java/instanceof1/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 instanceof1.class
 
 ^EXIT=0$

regression/cbmc-java/instanceof3/test.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 instanceof3.class
 
 ^EXIT=0$

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -487,39 +487,41 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     if(symbol_table.has_symbol(symbol_type_identifier))
       return;
 
-    struct_typet struct_type;
+    class_typet class_type;
     // we have the base class, java.lang.Object, length and data
     // of appropriate type
-    struct_type.set_tag(symbol_type_identifier);
-
-    struct_type.components().reserve(3);
-    struct_typet::componentt
-      comp0("@java.lang.Object", symbol_typet("java::java.lang.Object"));
-    comp0.set_pretty_name("@java.lang.Object");
-    comp0.set_base_name("@java.lang.Object");
-    struct_type.components().push_back(comp0);
-
-    struct_typet::componentt comp1("length", java_int_type());
-    comp1.set_pretty_name("length");
-    comp1.set_base_name("length");
-    struct_type.components().push_back(comp1);
-
-    struct_typet::componentt
-      comp2("data", java_reference_type(java_type_from_char(l)));
-    comp2.set_pretty_name("data");
-    comp2.set_base_name("data");
-    struct_type.components().push_back(comp2);
+    class_type.set_tag(symbol_type_identifier);
+
+    class_type.components().reserve(3);
+    class_typet::componentt base_class_component(
+      "@java.lang.Object", symbol_typet("java::java.lang.Object"));
+    base_class_component.set_pretty_name("@java.lang.Object");
+    base_class_component.set_base_name("@java.lang.Object");
+    class_type.components().push_back(base_class_component);
+
+    class_typet::componentt length_component("length", java_int_type());
+    length_component.set_pretty_name("length");
+    length_component.set_base_name("length");
+    class_type.components().push_back(length_component);
+
+    class_typet::componentt data_component(
+      "data", java_reference_type(java_type_from_char(l)));
+    data_component.set_pretty_name("data");
+    data_component.set_base_name("data");
+    class_type.components().push_back(data_component);
+
+    class_type.add_base(symbol_typet("java::java.lang.Object"));
 
     INVARIANT(
-      is_valid_java_array(struct_type),
+      is_valid_java_array(class_type),
       "Constructed a new type representing a Java Array "
       "object that doesn't match expectations");
 
     symbolt symbol;
     symbol.name=symbol_type_identifier;
     symbol.base_name=symbol_type.get(ID_C_base_name);
     symbol.is_type=true;
-    symbol.type=struct_type;
+    symbol.type = class_type;
     symbol_table.add(symbol);
 
     // Also provide a clone method:
@@ -566,14 +568,16 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
       java_reference_type(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());
+    member_exprt old_length(
+      old_array, length_component.get_name(), length_component.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());
+    member_exprt old_data(
+      old_array, data_component.get_name(), data_component.type());
+    member_exprt new_data(
+      new_array, data_component.get_name(), data_component.type());
 
     /*
       // TODO use this instead of a loop.
@@ -592,7 +596,7 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     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.type = length_component.type();
     index_symbol.mode=ID_java;
     symbol_table.add(index_symbol);
     const auto &index_symexpr=index_symbol.symbol_expr();
@@ -623,7 +627,8 @@ void java_bytecode_convert_classt::add_array_types(symbol_tablet &symbol_table)
     // End for-loop
     clone_body.move_to_operands(copy_loop);
 
-    member_exprt new_base_class(new_array, comp0.get_name(), comp0.type());
+    member_exprt new_base_class(
+      new_array, base_class_component.get_name(), base_class_component.type());
     address_of_exprt retval(new_base_class);
     code_returnt return_inst(retval);
     clone_body.move_to_operands(return_inst);