Extend the specialisation code to handle generic fields

Previously we didn't handle generic fields when we were doing
specialisation, meaning they were missed. This resolves this and adds a
unit test to demonstrate it.

Author: thk123

src/java_bytecode/generate_java_generic_type.cpp

@@ -118,22 +118,61 @@ typet generate_java_generic_typet::substitute_type(
     }
   }
   else if(
-    parameter_type.id() == ID_pointer &&
-    parameter_type.subtype().id() == ID_symbol)
+    parameter_type.id() == ID_pointer)
   {
-    const symbol_typet &array_subtype =
-      to_symbol_type(parameter_type.subtype());
-    if(is_java_array_tag(array_subtype.get_identifier()))
+    if(is_java_generic_type(parameter_type))
     {
-      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;
+      const java_generic_typet &generic_type =
+        to_java_generic_type(parameter_type);
+
+      java_generic_typet::generic_type_variablest replaced_type_variables;
+
+      // Swap each parameter
+      std::transform(
+        generic_type.generic_type_variables().begin(),
+        generic_type.generic_type_variables().end(),
+        std::back_inserter(replaced_type_variables),
+        [&](const java_generic_parametert &generic_param)
+          -> java_generic_parametert {
+            const typet &replacement_type =
+              substitute_type(generic_param, generic_class, generic_reference);
+
+            // This code will be simplified when references aren't considered to
+            // be generic parameters
+            if(is_java_generic_parameter(replacement_type))
+            {
+              return to_java_generic_parameter(replacement_type);
+            }
+            else
+            {
+              INVARIANT(
+                is_reference(replacement_type),
+                "All generic parameters should be references");
+              return java_generic_inst_parametert(
+                to_symbol_type(replacement_type.subtype()));
+            }
+          });
+
+      java_generic_typet new_type=generic_type;
+      new_type.generic_type_variables()=replaced_type_variables;
+      return new_type;
+    }
+    else if(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;

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

@@ -260,9 +260,9 @@ SCENARIO("generate_java_generic_type with a generic array field")
         const symbolt test_class_symbol =
           new_symbol_table.lookup_ref(specialised_class_name);
 
+        REQUIRE(test_class_symbol.type.id() == ID_struct);
         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");
@@ -278,6 +278,19 @@ SCENARIO("generate_java_generic_type with a generic array field")
           require_type::require_pointer(
             array_type, symbol_typet("java::java.lang.Float"));
         }
+
+        THEN("The generic class field should be specialised to be a generic "
+               "class with the appropriate type")
+        {
+          const struct_typet::componentt &field_component =
+            require_type::require_component(
+              to_struct_type(test_class_symbol.type), "genericClassField");
+
+          require_type::require_java_generic_type(
+            field_component.type(),
+            {{require_type::type_parameter_kindt::Inst,"java::java.lang.Float"}});
+        }
+
       }
     }
   }

unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.java

@@ -6,6 +6,8 @@ class generic<T> {
 
     class genericArray<T> {
         T [] arrayField;
+
+        generic<T> genericClassField;
     }
 
     generic<Float []> f;