TG-1212 Bugfix/add generic type args to dependencies

regression/cbmc-java/generics_type_param/GenericFields.java

@@ -0,0 +1,25 @@
+class IWrapper {
+    public int i;
+}
+
+class FWrapper {
+}
+
+class AWrapper {
+}
+
+class SimpleWrapper<T> {
+}
+
+public class GenericFields
+{
+  class SimpleGenericField  {
+    // IWrapper field; // for this to work, uncomment this line
+    SimpleWrapper<IWrapper> field_input;
+    public void foo() {
+    }
+    SimpleWrapper<IWrapper> f(SimpleWrapper<FWrapper> s, SimpleWrapper<AWrapper []> a) {
+      return new SimpleWrapper<>();
+    }
+  }
+}

regression/cbmc-java/generics_type_param/test.desc

@@ -0,0 +1,8 @@
+CORE
+GenericFields$SimpleGenericField.class
+--cover location --function GenericFields\$SimpleGenericField.foo --verbosity 10
+^EXIT=0$
+^SIGNAL=0$
+Reading class AWrapper
+Reading class FWrapper
+Reading class IWrapper

src/java_bytecode/java_bytecode_convert_method.cpp

@@ -116,15 +116,6 @@ static bool operator==(const irep_idt &what, const patternt &pattern)
   return pattern==what;
 }
 
-static irep_idt strip_java_namespace_prefix(const irep_idt to_strip)
-{
-  const std::string to_strip_str=id2string(to_strip);
-  const std::string prefix="java::";
-
-  PRECONDITION(has_prefix(to_strip_str, prefix));
-  return to_strip_str.substr(prefix.size(), std::string::npos);
-}
-
 // name contains <init> or <clinit>
 bool java_bytecode_convert_methodt::is_constructor(
   const class_typet::methodt &method)

src/java_bytecode/java_bytecode_parser.cpp

@@ -343,6 +343,11 @@ void java_bytecode_parsert::get_class_refs()
         field.descriptor,
         field.signature,
         "java::"+id2string(parse_tree.parsed_class.name));
+
+      // add generic type args to class refs as dependencies, same below for
+      // method types and entries from the local variable type table
+      get_dependencies_from_generic_parameters(
+        field_type, parse_tree.class_refs);
     }
     else
       field_type=java_type_from_string(field.descriptor);
@@ -359,6 +364,8 @@ void java_bytecode_parsert::get_class_refs()
         method.descriptor,
         method.signature,
         "java::"+id2string(parse_tree.parsed_class.name));
+      get_dependencies_from_generic_parameters(
+        method_type, parse_tree.class_refs);
     }
     else
       method_type=java_type_from_string(method.descriptor);
@@ -373,6 +380,8 @@ void java_bytecode_parsert::get_class_refs()
           var.descriptor,
           var.signature,
           "java::"+id2string(parse_tree.parsed_class.name));
+        get_dependencies_from_generic_parameters(
+          var_type, parse_tree.class_refs);
       }
       else
         var_type=java_type_from_string(var.descriptor);
@@ -1356,6 +1365,9 @@ void java_bytecode_parsert::rclass_attribute(classt &parsed_class)
   {
     u2 signature_index=read_u2();
     parsed_class.signature=id2string(pool_entry(signature_index).s);
+    get_dependencies_from_generic_parameters(
+      parsed_class.signature.value(),
+      parse_tree.class_refs);
   }
   else if(attribute_name=="RuntimeInvisibleAnnotations" ||
           attribute_name=="RuntimeVisibleAnnotations")

src/java_bytecode/java_types.cpp

@@ -715,3 +715,93 @@ bool is_valid_java_array(const struct_typet &type)
     length_component_valid &&
     data_component_valid;
 }
+
+void get_dependencies_from_generic_parameters_rec(
+  const typet &t,
+  std::set<irep_idt> &refs)
+{
+  // Java generic type that holds different types in its type arguments
+  if(is_java_generic_type(t))
+  {
+    for(const auto type_arg : to_java_generic_type(t).generic_type_arguments())
+      get_dependencies_from_generic_parameters_rec(type_arg, refs);
+  }
+
+  // Java reference type
+  else if(t.id() == ID_pointer)
+  {
+    get_dependencies_from_generic_parameters_rec(t.subtype(), refs);
+  }
+
+  // method type with parameters and return value
+  else if(t.id() == ID_code)
+  {
+    const code_typet &c = to_code_type(t);
+    get_dependencies_from_generic_parameters_rec(c.return_type(), refs);
+    for(const auto &param : c.parameters())
+      get_dependencies_from_generic_parameters_rec(param.type(), refs);
+  }
+
+  // symbol type
+  else if(t.id() == ID_symbol)
+  {
+    const symbol_typet &symbol_type = to_symbol_type(t);
+    const irep_idt class_name(symbol_type.get_identifier());
+    if(is_java_array_tag(class_name))
+    {
+      get_dependencies_from_generic_parameters(
+        java_array_element_type(symbol_type), refs);
+    }
+    else
+      refs.insert(strip_java_namespace_prefix(class_name));
+  }
+}
+
+/// Collect information about generic type parameters from a given
+/// signature. This is used to get information about class dependencies that
+/// must be loaded but only appear as generic type argument, not as a field
+/// reference.
+/// \param signature: the string representation of the signature to analyze
+/// \param refs [out]: the set to insert the names of the found dependencies
+void get_dependencies_from_generic_parameters(
+  const std::string &signature,
+  std::set<irep_idt> &refs)
+{
+  try
+  {
+    // class signature with bounds
+    if(signature[0] == '<')
+    {
+      const std::vector<typet> types = java_generic_type_from_string(
+        erase_type_arguments(signature), signature);
+
+      for(const auto &t : types)
+        get_dependencies_from_generic_parameters_rec(t, refs);
+    }
+
+    // class signature without bounds and without wildcards
+    else if(signature.find('*') == std::string::npos)
+    {
+      get_dependencies_from_generic_parameters_rec(
+        java_type_from_string(signature, erase_type_arguments(signature)),
+        refs);
+    }
+  }
+  catch(unsupported_java_class_signature_exceptiont &)
+  {
+    // skip for now, if we cannot parse it, we cannot detect which additional
+    // classes should be loaded as dependencies
+  }
+}
+
+/// Collect information about generic type parameters from a given type. This is
+/// used to get information about class dependencies that must be loaded but
+/// only appear as generic type argument, not as a field reference.
+/// \param t: the type to analyze
+/// \param refs [out]: the set to insert the names of the found dependencies
+void get_dependencies_from_generic_parameters(
+  const typet &t,
+  std::set<irep_idt> &refs)
+{
+  get_dependencies_from_generic_parameters_rec(t, refs);
+}

src/java_bytecode/java_types.h

@@ -11,6 +11,7 @@ Author: Daniel Kroening, [email protected]
 
 #include <util/invariant.h>
 #include <algorithm>
+#include <set>
 
 #include <util/type.h>
 #include <util/std_types.h>
@@ -366,4 +367,11 @@ inline const optionalt<size_t> java_generics_get_index_for_subtype(
   return std::distance(gen_types.cbegin(), iter);
 }
 
+void get_dependencies_from_generic_parameters(
+  const std::string &,
+  std::set<irep_idt> &);
+void get_dependencies_from_generic_parameters(
+  const typet &,
+  std::set<irep_idt> &);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H

src/java_bytecode/java_utils.cpp

@@ -293,3 +293,15 @@ exprt make_function_application(
   call.arguments()=arguments;
   return call;
 }
+
+/// Strip java:: prefix from given identifier
+/// \param to_strip: identifier from which the prefix is stripped
+/// \return the identifier without without java:: prefix
+irep_idt strip_java_namespace_prefix(const irep_idt &to_strip)
+{
+  const std::string to_strip_str=id2string(to_strip);
+  const std::string prefix="java::";
+
+  PRECONDITION(has_prefix(to_strip_str, prefix));
+  return to_strip_str.substr(prefix.size(), std::string::npos);
+}

src/java_bytecode/java_utils.h

@@ -92,4 +92,6 @@ exprt make_function_application(
   const typet &type,
   symbol_table_baset &symbol_table);
 
+irep_idt strip_java_namespace_prefix(const irep_idt &to_strip);
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_UTILS_H