[TG-1403] Correctly specialise classes with generic arrays or generic types

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)
@@ -33,41 +32,26 @@ symbolt generate_java_generic_typet::operator()(
 
   INVARIANT(
     pointer_subtype.id()==ID_struct, "Only pointers to classes in java");
+  INVARIANT(
+    is_java_generic_class_type(pointer_subtype),
+    "Generic references type must be a generic class");
 
-  const java_class_typet &replacement_type=
-    to_java_class_type(pointer_subtype);
-  const irep_idt new_tag=build_generic_tag(
-    existing_generic_type, replacement_type);
-  struct_union_typet::componentst replacement_components=
-    replacement_type.components();
+  const java_generic_class_typet &generic_class_definition =
+    to_java_generic_class_type(to_java_class_type(pointer_subtype));
+
+  const irep_idt new_tag =
+    build_generic_tag(existing_generic_type, generic_class_definition);
+  struct_union_typet::componentst replacement_components =
+    generic_class_definition.components();
 
   // 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_generics_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);
+  auto replace_type_for_generic_field =
+    [&](struct_union_typet::componentt &component) {
 
-        INVARIANT(
-          results.has_value(),
-          "generic component type not found");
+      component.type() = substitute_type(
+        component.type(), generic_class_definition, existing_generic_type);
 
-        if(results)
-        {
-          component.type()=
-            existing_generic_type.generic_type_variables()[*results];
-        }
-      }
       return component;
     };
 
@@ -79,8 +63,8 @@ symbolt generate_java_generic_typet::operator()(
     replacement_components.end(),
     replace_type_for_generic_field);
 
-  std::size_t after_modification_size=
-    replacement_type.components().size();
+  std::size_t after_modification_size =
+    generic_class_definition.components().size();
 
   INVARIANT(
     pre_modification_size==after_modification_size,
@@ -98,6 +82,95 @@ 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");
+    return generic_reference.generic_type_variables()[*results];
+  }
+  else if(parameter_type.id() == ID_pointer)
+  {
+    if(is_java_generic_type(parameter_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;
+}
+
 /// 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;
 };
 

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -97,7 +97,7 @@ void java_bytecode_convert_classt::convert(const classt &c)
   java_class_typet class_type;
   if(c.signature.has_value() && c.signature.value()[0]=='<')
   {
-    java_generics_class_typet generic_class_type;
+    java_generic_class_typet generic_class_type;
 #ifdef DEBUG
     std::cout << "INFO: found generic class signature "
               << c.signature.value()

src/java_bytecode/java_types.h

@@ -254,12 +254,12 @@ inline java_generic_typet &to_java_generic_type(typet &type)
 /// vector of java_generic_type variables.
 ///
 /// For example, a class definition `class MyGenericClass<T>`
-class java_generics_class_typet:public java_class_typet
+class java_generic_class_typet : public java_class_typet
 {
  public:
   typedef std::vector<java_generic_parametert> generic_typest;
 
-  java_generics_class_typet()
+  java_generic_class_typet()
   {
     set(ID_C_java_generics_class_type, true);
   }
@@ -277,27 +277,27 @@ class java_generics_class_typet:public java_class_typet
 
 /// \param type: the type to check
 /// \return true if type is a java class type with generics
-inline bool is_java_generics_class_type(const typet &type)
+inline bool is_java_generic_class_type(const typet &type)
 {
   return type.get_bool(ID_C_java_generics_class_type);
 }
 
 /// \param type: the type to check
 /// \return cast of type to java_generics_class_typet
-inline const java_generics_class_typet &to_java_generics_class_type(
-  const java_class_typet &type)
+inline const java_generic_class_typet &
+to_java_generic_class_type(const java_class_typet &type)
 {
-  PRECONDITION(is_java_generics_class_type(type));
-  return static_cast<const java_generics_class_typet &>(type);
+  PRECONDITION(is_java_generic_class_type(type));
+  return static_cast<const java_generic_class_typet &>(type);
 }
 
 /// \param type: source type
 /// \return cast of type into a java class type with generics
-inline java_generics_class_typet &to_java_generics_class_type(
-  java_class_typet &type)
+inline java_generic_class_typet &
+to_java_generic_class_type(java_class_typet &type)
 {
-  PRECONDITION(is_java_generics_class_type(type));
-  return static_cast<java_generics_class_typet &>(type);
+  PRECONDITION(is_java_generic_class_type(type));
+  return static_cast<java_generic_class_typet &>(type);
 }
 
 /// Access information of instantiated type params of java instantiated type.
@@ -318,9 +318,8 @@ inline const typet &java_generic_get_inst_type(
 /// \param index: the index of the type variable
 /// \param type: the type from which to extract the type variable
 /// \return the name of the generic type variable of t at the given index
-inline const irep_idt &java_generics_class_type_var(
-  size_t index,
-  const java_generics_class_typet &type)
+inline const irep_idt &
+java_generic_class_type_var(size_t index, const java_generic_class_typet &type)
 {
   const std::vector<java_generic_parametert> &gen_types=type.generic_types();
 
@@ -334,13 +333,11 @@ inline const irep_idt &java_generics_class_type_var(
 /// \param index: the index of the type variable
 /// \param t: the type from which to extract the type bound
 /// \return the type of the bound of the type variable
-inline const typet &java_generics_class_type_bound(
-  size_t index,
-  const typet &t)
+inline const typet &java_generic_class_type_bound(size_t index, const typet &t)
 {
-  PRECONDITION(is_java_generics_class_type(t));
-  const java_generics_class_typet &type=
-    to_java_generics_class_type(to_java_class_type(t));
+  PRECONDITION(is_java_generic_class_type(t));
+  const java_generic_class_typet &type =
+    to_java_generic_class_type(to_java_class_type(t));
   const std::vector<java_generic_parametert> &gen_types=type.generic_types();
 
   PRECONDITION(index<gen_types.size());
@@ -381,7 +378,7 @@ inline typet java_type_from_string_with_exception(
 /// \param identifier The string identifier of the type of the component.
 /// \return Optional with the size if the identifier was found.
 inline const optionalt<size_t> java_generics_get_index_for_subtype(
-  const java_generics_class_typet &t,
+  const java_generic_class_typet &t,
   const irep_idt &identifier)
 {
   const std::vector<java_generic_parametert> &gen_types=