Correctly handle generic classes that have a array field

Previously we only converted types that were precisely a generic
parameter. Now we deal with the case where the array is T type'd.

Author: thk123

src/java_bytecode/generate_java_generic_type.cpp

@@ -11,7 +11,6 @@
 #include <java_bytecode/java_types.h>
 #include <java_bytecode/java_utils.h>
 
-
 generate_java_generic_typet::generate_java_generic_typet(
   message_handlert &message_handler):
     message_handler(message_handler)
@@ -43,31 +42,14 @@ symbolt generate_java_generic_typet::operator()(
 
   // Small auxiliary function, to perform the inplace
   // modification of the generic fields.
-  auto replace_type_for_generic_field=
-    [&](struct_union_typet::componentt &component)
-    {
-      if(is_java_generic_parameter(component.type()))
-      {
-        auto replacement_type_param =
-          to_java_generic_class_type(replacement_type);
+  auto replace_type_for_generic_field =
+    [&](struct_union_typet::componentt &component) {
 
-        auto component_identifier=
-          to_java_generic_parameter(component.type()).type_variable()
-            .get_identifier();
+      component.type() = substitute_type(
+        component.type(),
+        to_java_generic_class_type(replacement_type),
+        existing_generic_type);
 
-        optionalt<size_t> results=java_generics_get_index_for_subtype(
-          replacement_type_param, component_identifier);
-
-        INVARIANT(
-          results.has_value(),
-          "generic component type not found");
-
-        if(results)
-        {
-          component.type()=
-            existing_generic_type.generic_type_variables()[*results];
-        }
-      }
       return component;
     };
 
@@ -98,6 +80,64 @@ symbolt generate_java_generic_typet::operator()(
   return *symbol;
 }
 
+/// For a given type, if the type contains a Java generic parameter, we look
+/// that parameter up and return the relevant type. This works recursively on
+/// arrays so that T [] is converted to RelevantType [].
+/// \param parameter_type: The type under consideration
+/// \param generic_class: The generic class that the \p parameter_type
+/// belongs to (e.g. the type of a component of the class). This is used to
+/// look up the mapping from name of generic parameter to its index.
+/// \param generic_reference: The instantiated version of the generic class
+/// used to look up the instantiated type. This is expected to be fully
+/// instantiated.
+/// \return A newly constructed type with generic parameters replaced, or if
+/// there are none to replace, the original type.
+typet generate_java_generic_typet::substitute_type(
+  const typet &parameter_type,
+  const java_generic_class_typet &generic_class,
+  const java_generic_typet &generic_reference) const
+{
+  if(is_java_generic_parameter(parameter_type))
+  {
+    auto component_identifier = to_java_generic_parameter(parameter_type)
+                                  .type_variable()
+                                  .get_identifier();
+
+    optionalt<size_t> results =
+      java_generics_get_index_for_subtype(generic_class, component_identifier);
+
+    INVARIANT(results.has_value(), "generic component type not found");
+
+    if(results)
+    {
+      return generic_reference.generic_type_variables()[*results];
+    }
+    else
+    {
+      return parameter_type;
+    }
+  }
+  else if(
+    parameter_type.id() == ID_pointer &&
+    parameter_type.subtype().id() == ID_symbol)
+  {
+    const symbol_typet &array_subtype =
+      to_symbol_type(parameter_type.subtype());
+    if(is_java_array_tag(array_subtype.get_identifier()))
+    {
+      const typet &array_element_type = java_array_element_type(array_subtype);
+
+      const typet &new_array_type =
+        substitute_type(array_element_type, generic_class, generic_reference);
+
+      typet replacement_array_type = java_array_type('a');
+      replacement_array_type.subtype().set(ID_C_element_type, new_array_type);
+      return replacement_array_type;
+    }
+  }
+  return parameter_type;
+}
+
 /// Build a unique tag for the generic to be instantiated.
 /// \param existing_generic_type The type we want to concretise
 /// \param original_class

src/java_bytecode/generate_java_generic_type.h

@@ -28,6 +28,11 @@ class generate_java_generic_typet
     const java_generic_typet &existing_generic_type,
     const java_class_typet &original_class) const;
 
+  typet substitute_type(
+    const typet &parameter_type,
+    const java_generic_class_typet &replacement_type,
+    const java_generic_typet &generic_reference) const;
+
   message_handlert &message_handler;
 };
 

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

@@ -179,8 +179,7 @@ SCENARIO(
   // We have a 'harness' class who's only purpose is to contain a reference
   // to the generic class so that we can test the specialization of that generic
   // class
-  const irep_idt harness_class=
-    "java::generic_field_array_instantiation";
+  const irep_idt harness_class = "java::generic_field_array_instantiation";
 
   // We want to test that the specialized/instantiated class has it's field
   // type updated, so find the specialized class, not the generic class.
@@ -190,20 +189,16 @@ SCENARIO(
 
   GIVEN("A generic type instantiated with an array type")
   {
-    symbol_tablet new_symbol_table=
-      load_java_class(
-        "generic_field_array_instantiation",
-        "./java_bytecode/generate_concrete_generic_type");
+    symbol_tablet new_symbol_table = load_java_class(
+      "generic_field_array_instantiation",
+      "./java_bytecode/generate_concrete_generic_type");
 
     // Ensure the class has been specialized
     REQUIRE(new_symbol_table.has_symbol(harness_class));
-    const symbolt &harness_symbol=
-      new_symbol_table.lookup_ref(harness_class);
+    const symbolt &harness_symbol = new_symbol_table.lookup_ref(harness_class);
 
-    const struct_typet::componentt &harness_component=
-      require_type::require_component(
-        to_struct_type(harness_symbol.type),
-        "f");
+    const struct_typet::componentt &harness_component =
+      require_type::require_component(to_struct_type(harness_symbol.type), "f");
 
     ui_message_handlert message_handler;
     generate_java_generic_typet instantiate_generic_type(message_handler);
@@ -212,25 +207,22 @@ SCENARIO(
 
     // Test the specialized class
     REQUIRE(new_symbol_table.has_symbol(test_class));
-    const symbolt test_class_symbol=
-      new_symbol_table.lookup_ref(test_class);
+    const symbolt test_class_symbol = new_symbol_table.lookup_ref(test_class);
 
-    REQUIRE(test_class_symbol.type.id()==ID_struct);
-    const struct_typet::componentt &field_component=
+    REQUIRE(test_class_symbol.type.id() == ID_struct);
+    const struct_typet::componentt &field_component =
       require_type::require_component(
-        to_struct_type(test_class_symbol.type),
-        "gf");
-    const typet &test_field_type=field_component.type();
+        to_struct_type(test_class_symbol.type), "gf");
+    const typet &test_field_type = field_component.type();
 
-    REQUIRE(test_field_type.id()==ID_pointer);
-    REQUIRE(test_field_type.subtype().id()==ID_symbol);
-    const symbol_typet test_field_array=
+    REQUIRE(test_field_type.id() == ID_pointer);
+    REQUIRE(test_field_type.subtype().id() == ID_symbol);
+    const symbol_typet test_field_array =
       to_symbol_type(test_field_type.subtype());
-    REQUIRE(test_field_array.get_identifier()=="java::array[reference]");
-    const pointer_typet &element_type=
-      require_type::require_pointer(
-        java_array_element_type(test_field_array),
-        symbol_typet("java::java.lang.Float"));
+    REQUIRE(test_field_array.get_identifier() == "java::array[reference]");
+    const pointer_typet &element_type = 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
@@ -270,3 +262,55 @@ SCENARIO(
     }
   }
 }
+
+SCENARIO(
+  "generate_java_generic_type with a generic array field",
+  "[core][java_bytecode][generate_java_generic_type]")
+{
+  const irep_idt harness_class = "java::generic_field_array_instantiation";
+  GIVEN("A generic class with a field of type T []")
+  {
+    symbol_tablet new_symbol_table = load_java_class(
+      "generic_field_array_instantiation",
+      "./java_bytecode/generate_concrete_generic_type");
+
+    const irep_idt inner_class = "genericArray";
+
+    WHEN("We specialise that class from a reference to it")
+    {
+      specialise_generic_from_component(
+        harness_class, "genericArrayField", new_symbol_table);
+      THEN(
+        "There should be a specialised version of the class in the symbol "
+        "table")
+      {
+        const irep_idt specialised_class_name = id2string(harness_class) + "$" +
+                                                id2string(inner_class) +
+                                                "<java::java.lang.Float>";
+        REQUIRE(new_symbol_table.has_symbol(specialised_class_name));
+
+        const symbolt test_class_symbol =
+          new_symbol_table.lookup_ref(specialised_class_name);
+
+        THEN("The array field should be specialised to be an array of floats")
+        {
+          REQUIRE(test_class_symbol.type.id() == ID_struct);
+          const struct_typet::componentt &field_component =
+            require_type::require_component(
+              to_struct_type(test_class_symbol.type), "arrayField");
+
+          const pointer_typet &component_pointer_type =
+            require_type::require_pointer(field_component.type(), {});
+
+          const symbol_typet &pointer_subtype = require_type::require_symbol(
+            component_pointer_type.subtype(), "java::array[reference]");
+
+          const typet &array_type = java_array_element_type(pointer_subtype);
+
+          require_type::require_pointer(
+            array_type, symbol_typet("java::java.lang.Float"));
+        }
+      }
+    }
+  }
+}

unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$generic.class

@@ -4,9 +4,15 @@ class generic<T> {
         T gf;
     }
 
+    class genericArray<T> {
+        T [] arrayField;
+    }
+
     generic<Float []> f;
     generic<Integer []> g;
     generic<int []> h;
     generic<float []> i;
     Float [] af;
+
+    genericArray<Float> genericArrayField;
 }