Make explicit type parameters shadow implicit ones with the same names

Fixes problem where outer class type parameters take precedence over inner class ones
Previously field would be given the type of the argument assigned to A::T, not B::T.
class A<T> { class B<T> { T field; } }?

Author: NathanJPhillips

jbmc/src/java_bytecode/java_bytecode_convert_class.cpp

@@ -1205,6 +1205,17 @@ void mark_java_implicitly_generic_class_type(
     java_implicitly_generic_class_typet new_class_type(
       class_type, implicit_generic_type_parameters);
 
+    // Prepend existing parameters so choose those above any inherited
+    if(is_java_generic_class_type(class_type))
+    {
+      const java_generic_class_typet::generic_typest &class_type_params =
+        to_java_generic_class_type(class_type).generic_types();
+      implicit_generic_type_parameters.insert(
+        implicit_generic_type_parameters.begin(),
+        class_type_params.begin(),
+        class_type_params.end());
+    }
+
     for(auto &field : new_class_type.components())
     {
       find_and_replace_parameters(

jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.java

@@ -3,7 +3,7 @@ class Inner<U> {
     Outer<V, K, U> o;
     U u;
   }
-  Inner<U> inner;
+  Inner<V> inner;
   K key;
   V value;
 }

jbmc/unit/java_bytecode/goto_program_generics/Outer.class

@@ -298,6 +298,45 @@ SCENARIO(
       }
     }
 
+    THEN(
+      "The Object has a field `example3` of type `Outer<Boolean, Byte, Short>`")
+    {
+      const auto &example3_field =
+        require_goto_statements::require_struct_component_assignment(
+          tmp_object_name,
+          {},
+          "example3",
+          "java::Outer",
+          {},
+          entry_point_code,
+          symbol_table);
+
+      THEN("`example3` has field `inner` of type `Inner<Byte>`")
+      {
+        const auto &inner_field =
+          require_goto_statements::require_struct_component_assignment(
+            example3_field,
+            {},
+            "inner",
+            "java::Outer$Inner",
+            {},
+            entry_point_code,
+            symbol_table);
+
+        THEN("`inner` has a field `u` of type `Byte`")
+        {
+          require_goto_statements::require_struct_component_assignment(
+            inner_field,
+            {},
+            "u",
+            "java::java.lang.Byte",
+            {},
+            entry_point_code,
+            symbol_table);
+        }
+      }
+    }
+
     THEN("The Object has a field `testFoo` of type `Foo<Long>`")
     {
       const auto &testFoo_field =

jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp

@@ -17,6 +17,12 @@ class GenericInner<U> {
     class GenericInnerInner<V>{
 
     }
+
+    class ShadowingGenericInner<U> {
+      U shadowedField;
+    }
+
+    ShadowingGenericInner<String> shadowingField;
   }
 
   static class StaticInner<U>{

jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner$GenericInnerInner.class

@@ -17,6 +17,7 @@ SCENARIO(
   const symbol_tablet &new_symbol_table = load_java_class(
     "GenericClassWithInnerClasses",
     "./java_bytecode/java_bytecode_parse_generics");
+  namespacet ns{new_symbol_table};
 
   std::string outer_class_name = "GenericClassWithInnerClasses";
   std::string outer_class_prefix = "java::" + outer_class_name;
@@ -49,13 +50,59 @@ SCENARIO(
     }
     THEN("There is a field f3 of generic type with correct arguments")
     {
+      std::string inner_class_prefix = outer_class_prefix + "$GenericInner";
       const auto &field = require_type::require_component(generic_class, "f3");
-      require_type::require_pointer_to_tag(
-        field.type(), outer_class_prefix + "$GenericInner");
-      require_type::require_java_generic_type(
-        field.type(),
-        {{require_type::type_argument_kindt::Var, outer_class_prefix + "::T"},
-         {require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}});
+      const auto &field_type =
+        require_type::require_pointer_to_tag(field.type(), inner_class_prefix);
+      java_generic_struct_tag_typet inner_class_tag =
+        require_type::require_java_generic_struct_tag_type(
+          field_type.subtype(),
+          inner_class_prefix,
+          {
+            {require_type::type_argument_kindt::Var,
+             outer_class_prefix + "::T"},
+            {require_type::type_argument_kindt::Inst,
+             "java::java.lang.Integer"},
+          });
+      const java_generic_class_typet &inner_class =
+        require_type::require_complete_java_generic_class(
+          ns.follow_tag(inner_class_tag), {inner_class_prefix + "::U"});
+      THEN(
+        "There is a field shadowingField of generic type with correct "
+        "arguments")
+      {
+        std::string shadowing_inner_class_prefix =
+          inner_class_prefix + "$ShadowingGenericInner";
+        const auto &shadowing_field =
+          require_type::require_component(inner_class, "shadowingField");
+        const auto &shadowing_field_type = require_type::require_pointer_to_tag(
+          shadowing_field.type(), shadowing_inner_class_prefix);
+        java_generic_struct_tag_typet shadowing_inner_class_tag =
+          require_type::require_java_generic_struct_tag_type(
+            shadowing_field_type.subtype(),
+            shadowing_inner_class_prefix,
+            {
+              {require_type::type_argument_kindt::Var,
+               inner_class_prefix + "::" + outer_class_name + "::T"},
+              {require_type::type_argument_kindt::Var,
+               inner_class_prefix + "::U"},
+              {require_type::type_argument_kindt::Inst,
+               "java::java.lang.String"},
+            });
+        const java_generic_class_typet &shadowing_inner_class =
+          require_type::require_complete_java_generic_class(
+            ns.follow_tag(shadowing_inner_class_tag),
+            {shadowing_inner_class_prefix + "::U"});
+        THEN(
+          "There is a field shadowedField which is the generic parameter of "
+          "the inner class")
+        {
+          const auto &shadowed_field = require_type::require_component(
+            shadowing_inner_class, "shadowedField");
+          require_type::require_java_generic_parameter(
+            shadowed_field.type(), shadowing_inner_class_prefix + "::U");
+        }
+      }
     }
   }
 
@@ -183,6 +230,26 @@ SCENARIO(
            {require_type::type_argument_kindt::Var,
             generic_inner_class_prefix + "::U"}});
       }
+      THEN(
+        "There is a field shadowingField of generic type with a generic "
+        "type argument of String")
+      {
+        std::string shadowing_inner_class_prefix =
+          generic_inner_class_prefix + "$ShadowingGenericInner";
+        const auto &field =
+          require_type::require_component(generic_class, "shadowingField");
+        require_type::require_pointer_to_tag(
+          field.type(), shadowing_inner_class_prefix);
+        require_type::require_java_generic_type(
+          field.type(),
+          {
+            {require_type::type_argument_kindt::Var,
+             generic_inner_class_prefix + "::" + outer_class_name + "::T"},
+            {require_type::type_argument_kindt::Var,
+             generic_inner_class_prefix + "::U"},
+            {require_type::type_argument_kindt::Inst, "java::java.lang.String"},
+          });
+      }
     }
   }