TG-1318 Mgudemann/feature/support arrays in generic parameters

src/java_bytecode/generate_java_generic_type.cpp

@@ -119,7 +119,24 @@ irep_idt generate_java_generic_typet::build_generic_tag(
     INVARIANT(
       is_java_generic_inst_parameter(param),
       "Only create full concretized generic types");
-    new_tag_buffer << param.subtype().get(ID_identifier);
+    const irep_idt &id(id2string(param.subtype().get(ID_identifier)));
+    new_tag_buffer << id2string(id);
+    if(is_java_array_tag(id))
+    {
+      const typet &element_type =
+        java_array_element_type(to_symbol_type(param.subtype()));
+
+      // If this is an array of references then we will specialize its
+      // identifier using the type of the objects in the array. Else, there can
+      // be a problem with the same symbols for different instantiations using
+      // arrays with different types.
+      if(element_type.id() == ID_pointer)
+      {
+        const symbol_typet element_symbol =
+          to_symbol_type(element_type.subtype());
+        new_tag_buffer << "of_" << id2string(element_symbol.get_identifier());
+      }
+    }
   }
 
   new_tag_buffer << ">";

src/java_bytecode/java_utils.cpp

@@ -21,11 +21,9 @@ Author: Daniel Kroening, [email protected]
 
 bool java_is_array_type(const typet &type)
 {
-  if(type.id()!=ID_struct)
+  if(type.id() != ID_struct)
     return false;
-  return has_prefix(id2string(
-    to_struct_type(type).get_tag()),
-                    "java::array[");
+  return is_java_array_tag(to_struct_type(type).get_tag());
 }
 
 unsigned java_local_variable_slots(const typet &t)

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

@@ -184,8 +184,9 @@ SCENARIO(
 
   // We want to test that the specialized/instantiated class has it's field
   // type updated, so find the specialized class, not the generic class.
-  const irep_idt test_class=
-    "java::generic_field_array_instantiation$generic<java::array[reference]>";
+  const irep_idt test_class =
+    "java::generic_field_array_instantiation$generic<java::array[reference]"
+    "of_java::java.lang.Float>";
 
   GIVEN("A generic type instantiated with an array type")
   {
@@ -230,5 +231,42 @@ SCENARIO(
       require_type::require_pointer(
         java_array_element_type(test_field_array),
         symbol_typet("java::java.lang.Float"));
+
+    // check for other specialized classes, in particular different symbol ids
+    // for arrays with different element types
+    GIVEN("A generic type instantiated with different array types")
+    {
+      const irep_idt test_class_integer =
+        "java::generic_field_array_instantiation$generic<java::array[reference]"
+        "of_"
+        "java::java.lang.Integer>";
+
+      const irep_idt test_class_int =
+        "java::generic_field_array_instantiation$generic<java::array[int]>";
+
+      const irep_idt test_class_float =
+        "java::generic_field_array_instantiation$generic<java::array[float]>";
+
+      const struct_typet::componentt &component_g =
+        require_type::require_component(
+          to_struct_type(harness_symbol.type), "g");
+      instantiate_generic_type(
+        to_java_generic_type(component_g.type()), new_symbol_table);
+      REQUIRE(new_symbol_table.has_symbol(test_class_integer));
+
+      const struct_typet::componentt &component_h =
+        require_type::require_component(
+          to_struct_type(harness_symbol.type), "h");
+      instantiate_generic_type(
+        to_java_generic_type(component_h.type()), new_symbol_table);
+      REQUIRE(new_symbol_table.has_symbol(test_class_int));
+
+      const struct_typet::componentt &component_i =
+        require_type::require_component(
+          to_struct_type(harness_symbol.type), "i");
+      instantiate_generic_type(
+        to_java_generic_type(component_i.type()), new_symbol_table);
+      REQUIRE(new_symbol_table.has_symbol(test_class_float));
+    }
   }
 }

unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.java

@@ -5,7 +5,8 @@ class generic<T> {
     }
 
     generic<Float []> f;
+    generic<Integer []> g;
+    generic<int []> h;
+    generic<float []> i;
     Float [] af;
 }
-
-