[TG-1190] Parse generic information of outer classes

src/java_bytecode/java_bytecode_convert_class.cpp

@@ -517,3 +517,163 @@ bool java_bytecode_convert_class(
 
   return true;
 }
+
+/// For a given generic type parameter, check if there is a parameter in the
+/// given vector of replacement parameters with a matching name. If yes,
+/// replace the identifier of the parameter at hand by the identifier of
+/// the matching parameter.
+/// Example: if \p parameter has identifier `java::Outer$Inner::T` and
+/// there is a replacement parameter with identifier `java::Outer::T`, the
+/// identifier of \p parameter gets set to `java::Outer::T`.
+/// \param parameter
+/// \param replacement_parameters vector of generic parameters (only viable
+///   ones, i.e., only those that can actually appear here such as generic
+///   parameters of outer classes of the class specified by the prefix of \p
+///   parameter identifier)
+static void find_and_replace_parameter(
+  java_generic_parametert &parameter,
+  const std::vector<java_generic_parametert> &replacement_parameters)
+{
+  // get the name of the parameter, e.g., `T` from `java::Class::T`
+  const std::string &parameter_full_name =
+    as_string(parameter.type_variable_ref().get_identifier());
+  const std::string &parameter_name =
+    parameter_full_name.substr(parameter_full_name.rfind("::") + 2);
+
+  // check if there is a replacement parameter with the same name
+  const auto replacement_parameter_p = std::find_if(
+    replacement_parameters.begin(),
+    replacement_parameters.end(),
+    [&parameter_name](const java_generic_parametert &replacement_param)
+    {
+      const std::string &replacement_parameter_full_name =
+        as_string(replacement_param.type_variable().get_identifier());
+      return parameter_name.compare(
+               replacement_parameter_full_name.substr(
+                 replacement_parameter_full_name.rfind("::") + 2)) == 0;
+    });
+
+  // if a replacement parameter was found, update the identifier
+  if(replacement_parameter_p != replacement_parameters.end())
+  {
+    const std::string &replacement_parameter_full_name =
+      as_string(replacement_parameter_p->type_variable().get_identifier());
+
+    // the replacement parameter is a viable one, i.e., it comes from an outer
+    // class
+    PRECONDITION(
+      parameter_full_name.substr(0, parameter_full_name.rfind("::"))
+        .compare(
+          replacement_parameter_full_name.substr(
+            0, replacement_parameter_full_name.rfind("::"))) > 0);
+
+    parameter.type_variable_ref().set_identifier(
+      replacement_parameter_full_name);
+  }
+}
+
+/// Recursively find all generic type parameters of a given type and replace
+/// their identifiers if matching replacement parameter exist.
+/// Example: class `Outer<T>` has an inner class `Inner` that has a field
+/// `t` of type `Generic<T>`. This function ensures that the parameter points to
+/// `java::Outer::T` instead of `java::Outer$Inner::T`.
+/// \param type
+/// \param replacement_parameters
+static void find_and_replace_parameters(
+  typet &type,
+  const std::vector<java_generic_parametert> &replacement_parameters)
+{
+  if(is_java_generic_parameter(type))
+  {
+    find_and_replace_parameter(
+      to_java_generic_parameter(type), replacement_parameters);
+  }
+  else if(is_java_generic_type(type))
+  {
+    java_generic_typet &generic_type = to_java_generic_type(type);
+    std::vector<reference_typet> &arguments =
+      generic_type.generic_type_arguments();
+    for(auto &argument : arguments)
+    {
+      find_and_replace_parameters(argument, replacement_parameters);
+    }
+  }
+}
+
+/// Checks if the class is implicitly generic, i.e., it is an inner class of
+/// any generic class. All uses of the implicit generic type parameters within
+/// the inner class are updated to point to the type parameters of the
+/// corresponding outer classes.
+/// \param class_name
+/// \param symbol_table
+void mark_java_implicitly_generic_class_type(
+  const irep_idt &class_name,
+  symbol_tablet &symbol_table)
+{
+  const std::string qualified_class_name = "java::" + id2string(class_name);
+  PRECONDITION(symbol_table.has_symbol(qualified_class_name));
+  symbolt &class_symbol = symbol_table.get_writeable_ref(qualified_class_name);
+  java_class_typet &class_type = to_java_class_type(class_symbol.type);
+
+  // the class must be an inner non-static class, i.e., have a field this$*
+  // TODO this should be simplified once static inner classes are marked
+  // during parsing
+  bool no_this_field = std::none_of(
+    class_type.components().begin(),
+    class_type.components().end(),
+    [](const struct_union_typet::componentt &component)
+    {
+      return id2string(component.get_name()).substr(0, 5) == "this$";
+    });
+  if(no_this_field)
+  {
+    return;
+  }
+
+  // create a vector of all generic type parameters of all outer classes, in
+  // the order from the outer-most inwards
+  std::vector<java_generic_parametert> implicit_generic_type_parameters;
+  std::string::size_type outer_class_delimiter =
+    qualified_class_name.rfind("$");
+  while(outer_class_delimiter != std::string::npos)
+  {
+    std::string outer_class_name =
+      qualified_class_name.substr(0, outer_class_delimiter);
+    if(symbol_table.has_symbol(outer_class_name))
+    {
+      const symbolt &outer_class_symbol =
+        symbol_table.lookup_ref(outer_class_name);
+      const java_class_typet &outer_class_type =
+        to_java_class_type(outer_class_symbol.type);
+      if(is_java_generic_class_type(outer_class_type))
+      {
+        const auto &outer_generic_type_parameters =
+          to_java_generic_class_type(outer_class_type).generic_types();
+        implicit_generic_type_parameters.insert(
+          implicit_generic_type_parameters.begin(),
+          outer_generic_type_parameters.begin(),
+          outer_generic_type_parameters.end());
+      }
+      outer_class_delimiter = outer_class_name.rfind("$");
+    }
+    else
+    {
+      throw missing_outer_class_symbol_exceptiont(
+        outer_class_name, qualified_class_name);
+    }
+  }
+
+  // if there are any implicit generic type parameters, mark the class
+  // implicitly generic and update identifiers of type parameters used in fields
+  if(!implicit_generic_type_parameters.empty())
+  {
+    class_symbol.type = java_implicitly_generic_class_typet(
+      class_type, implicit_generic_type_parameters);
+
+    for(auto &field : class_type.components())
+    {
+      find_and_replace_parameters(
+        field.type(), implicit_generic_type_parameters);
+    }
+  }
+}

src/java_bytecode/java_bytecode_convert_class.h

@@ -28,4 +28,22 @@ bool java_bytecode_convert_class(
   lazy_methods_modet,
   java_string_library_preprocesst &string_preprocess);
 
+void mark_java_implicitly_generic_class_type(
+  const irep_idt &class_name,
+  symbol_tablet &symbol_table);
+
+/// An exception that is raised checking whether a class is implicitly
+/// generic if a symbol for an outer class is missing
+class missing_outer_class_symbol_exceptiont : public std::logic_error
+{
+public:
+  explicit missing_outer_class_symbol_exceptiont(
+    const std::string &outer,
+    const std::string &inner)
+    : std::logic_error(
+        "Missing outer class symbol: " + outer + ", for class " + inner)
+  {
+  }
+};
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H

src/java_bytecode/java_bytecode_language.cpp

@@ -209,6 +209,26 @@ bool java_bytecode_languaget::typecheck(
       return true;
   }
 
+  // find and mark all implicitly generic class types
+  // this can only be done once all the class symbols have been created
+  for(const auto &c : java_class_loader.class_map)
+  {
+    if(c.second.parsed_class.name.empty())
+      continue;
+    try
+    {
+      mark_java_implicitly_generic_class_type(
+        c.second.parsed_class.name, symbol_table);
+    }
+    catch(missing_outer_class_symbol_exceptiont &)
+    {
+      messaget::warning()
+        << "Not marking class " << c.first
+        << " implicitly generic due to missing outer class symbols"
+        << messaget::eom;
+    }
+  }
+
   // Now incrementally elaborate methods
   // that are reachable from this entry point.
   if(lazy_methods_mode==LAZY_METHODS_MODE_CONTEXT_INSENSITIVE)

src/java_bytecode/java_types.h

@@ -110,6 +110,12 @@ class java_generic_parametert:public reference_typet
     return type_variables().front();
   }
 
+  type_variablet &type_variable_ref()
+  {
+    PRECONDITION(!type_variables().empty());
+    return const_cast<type_variablet &>(type_variables().front());
+  }
+
 private:
   typedef std::vector<type_variablet> type_variablest;
   const type_variablest &type_variables() const
@@ -313,6 +319,65 @@ inline const typet &java_generic_class_type_bound(size_t index, const typet &t)
   return gen_type.subtype();
 }
 
+/// Type to hold a Java class that is implicitly generic, e.g., an inner
+/// class of a generic outer class or a derived class of a generic base
+/// class. Extends the java class type.
+class java_implicitly_generic_class_typet : public java_class_typet
+{
+public:
+  typedef std::vector<java_generic_parametert> implicit_generic_typest;
+
+  explicit java_implicitly_generic_class_typet(
+    const java_class_typet &class_type,
+    const implicit_generic_typest &generic_types)
+    : java_class_typet(class_type)
+  {
+    set(ID_C_java_implicitly_generic_class_type, true);
+    for(const auto &type : generic_types)
+    {
+      implicit_generic_types().push_back(type);
+    }
+  }
+
+  const implicit_generic_typest &implicit_generic_types() const
+  {
+    return (
+      const implicit_generic_typest
+        &)(find(ID_implicit_generic_types).get_sub());
+  }
+
+  implicit_generic_typest &implicit_generic_types()
+  {
+    return (
+      implicit_generic_typest &)(add(ID_implicit_generic_types).get_sub());
+  }
+};
+
+/// \param type: the type to check
+/// \return true if type is a implicitly generic java class type
+inline bool is_java_implicitly_generic_class_type(const typet &type)
+{
+  return type.get_bool(ID_C_java_implicitly_generic_class_type);
+}
+
+/// \param type: the type to check
+/// \return cast of type to java_generics_class_typet
+inline const java_implicitly_generic_class_typet &
+to_java_implicitly_generic_class_type(const java_class_typet &type)
+{
+  PRECONDITION(is_java_implicitly_generic_class_type(type));
+  return static_cast<const java_implicitly_generic_class_typet &>(type);
+}
+
+/// \param type: source type
+/// \return cast of type into a java class type with generics
+inline java_implicitly_generic_class_typet &
+to_java_implicitly_generic_class_type(java_class_typet &type)
+{
+  PRECONDITION(is_java_implicitly_generic_class_type(type));
+  return static_cast<java_implicitly_generic_class_typet &>(type);
+}
+
 /// An exception that is raised for unsupported class signature.
 /// Currently we do not parse multiple bounds.
 class unsupported_java_class_signature_exceptiont:public std::logic_error

src/util/irep_ids.def

@@ -831,7 +831,9 @@ IREP_ID_TWO(C_java_generic_parameter, #java_generic_parameter)
 IREP_ID_TWO(C_java_generic_type, #java_generic_type)
 IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type)
 IREP_ID_TWO(C_specialized_generic_java_class, #specialized_generic_java_class)
+IREP_ID_TWO(C_java_implicitly_generic_class_type, #java_implicitly_generic_class_type)
 IREP_ID_TWO(generic_types, #generic_types)
+IREP_ID_TWO(implicit_generic_types, #implicit_generic_types)
 IREP_ID_TWO(type_variables, #type_variables)
 IREP_ID_ONE(havoc_object)
 IREP_ID_TWO(overflow_shl, overflow-shl)

unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses.java

@@ -0,0 +1,29 @@
+class GenericClassWithInnerClasses<T>
+{
+  class Inner {
+    T t1;
+    Generic<T> t2;
+
+    class InnerInner {
+      T tt1;
+      Generic<Generic<T>> tt2;
+    }
+  }
+
+  class GenericInner<U> {
+    T gt1;
+    GenericTwoParam<T,U> gt2;
+
+    class GenericInnerInner<V>{
+
+    }
+  }
+
+  static class StaticInner<U>{
+    U st;
+  }
+
+  Inner f1;
+  Inner.InnerInner f2;
+  GenericInner<Integer> f3;
+}