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 component_identifier=
-          to_java_generic_parameter(component.type()).type_variable()
-            .get_identifier();
-
-        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];
-        }
-      }
+  auto replace_type_for_generic_field =
+    [&](struct_union_typet::componentt &component) {
+
+      component.type() = substitute_type(
+        component.type(),
+        to_java_generic_class_type(replacement_type),
+        existing_generic_type);
+
       return component;
     };
 
@@ -98,6 +80,65 @@ 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_generics_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_generics_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

@@ -17,7 +17,6 @@
 #include <testing-utils/require_type.h>
 #include <testing-utils/generic_utils.h>
 #include <util/ui_message.h>
-#include <iostream>
 
 /// Helper function to specalise a generic class from a named component of a
 /// named class
@@ -231,48 +230,55 @@ SCENARIO(
       require_type::require_pointer(
         java_array_element_type(test_field_array),
         symbol_typet("java::java.lang.Float"));
+  }
+}
 
-    GIVEN("Specialising a generic class with an array field")
-    {
-      const irep_idt &inner_class = "genericArray";
+SCENARIO("generate_java_generic_type with a generic array field")
+{
+  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);
-
-      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);
-
-      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 typet &test_field_type=field_component.type();
-
-      std::cout << test_field_type.pretty() << std::endl;
-
-      std::cout << "Hello world" << std::endl;
+      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"));
+        }
+      }
     }
-
   }
 }
-//
-//SCENARIO("Specialising a generic class with a generic field ")
-//{
-//  const irep_idt harness_class =
-//    "java::generic_field_array_instantiation";
-//  GIVEN("A generic type with a generic array field")
-//  {
-//    symbol_tablet new_symbol_table=
-//      load_java_class(
-//        "generic_field_array_instantiation",
-//        "./java_bytecode/generate_concrete_generic_type");
-//
-//
-//  }
-//}