Make explicit type parameters shadow implicit ones with the same names

Fixes problem where outer class type parameters take precedence over inner class ones

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");
+        }
+      }
     }
   }