[TG-1157] Add specialised java generic class type.

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)
@@ -43,31 +42,14 @@ symbolt generate_java_generic_typet::operator()(
 
   // 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();
+  auto replace_type_for_generic_field =
+    [&](struct_union_typet::componentt &component) {
 
-        optionalt<size_t> results=java_generics_get_index_for_subtype(
-          replacement_type_param, component_identifier);
+      component.type() = substitute_type(
+        component.type(),
+        to_java_generic_class_type(replacement_type),
+        existing_generic_type);
 
-        INVARIANT(
-          results.has_value(),
-          "generic component type not found");
-
-        if(results)
-        {
-          component.type()=
-            existing_generic_type.generic_type_variables()[*results];
-        }
-      }
       return component;
     };
 
@@ -87,17 +69,146 @@ symbolt generate_java_generic_typet::operator()(
     "All components in the original class should be in the new class");
 
   const auto expected_symbol="java::"+id2string(new_tag);
-
-  generate_class_stub(
-    new_tag,
-    symbol_table,
-    message_handler,
-    replacement_components);
+//
+//  generate_class_stub(
+//    new_tag,
+//    symbol_table,
+//    message_handler,
+//    replacement_components);
+
+  // inlined the generate_class_stub for now
+  {
+    java_specialised_generic_class_typet specialised_class;
+    specialised_class.set_tag(replacement_type.get_tag());
+    // NOTE: the tag absolutely has to be BasicGeneric
+    specialised_class.set(ID_base_name, new_tag);
+
+    // produce class symbol
+    symbolt new_symbol;
+    new_symbol.base_name = new_tag;
+    new_symbol.pretty_name = new_tag;
+    new_symbol.name = "java::" + id2string(new_tag);
+    specialised_class.set(ID_name, new_symbol.name);
+    new_symbol.type = specialised_class;
+    new_symbol.mode = ID_java;
+    new_symbol.is_type = true;
+
+    std::pair<symbolt &, bool> res = symbol_table.insert(std::move(new_symbol));
+
+    if(!res.second)
+    {
+      messaget message(message_handler);
+      message.warning() << "stub class symbol " << new_symbol.name
+                        << " already exists" << messaget::eom;
+    }
+    else
+    {
+      java_add_components_to_class(res.first, replacement_components);
+    }
+  }
   auto symbol=symbol_table.lookup(expected_symbol);
   INVARIANT(symbol, "New class not created");
   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_generics_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");
+
+    if(results)
+    {
+      return generic_reference.generic_type_variables()[*results];
+    }
+    else
+    {
+      return parameter_type;
+    }
+  }
+  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_generics_class_typet &replacement_type,
+    const java_generic_typet &generic_reference) const;
+
   message_handlert &message_handler;
 };
 

src/java_bytecode/java_types.h

@@ -284,7 +284,7 @@ inline bool is_java_generics_class_type(const typet &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(
+inline const java_generics_class_typet &to_java_generic_class_type(
   const java_class_typet &type)
 {
   PRECONDITION(is_java_generics_class_type(type));
@@ -340,7 +340,7 @@ inline const typet &java_generics_class_type_bound(
 {
   PRECONDITION(is_java_generics_class_type(t));
   const java_generics_class_typet &type=
-    to_java_generics_class_type(to_java_class_type(t));
+    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());
@@ -403,4 +403,29 @@ inline const optionalt<size_t> java_generics_get_index_for_subtype(
   return std::distance(gen_types.cbegin(), iter);
 }
 
+class java_specialised_generic_class_typet : public java_class_typet
+{
+  // note the constryctor could take the components and construct it itself
+  // note vector of generic parameter of symbol type
+public:
+  // TODO: to be defined more appropriately.
+  java_specialised_generic_class_typet()
+  {
+    set(ID_C_specialised_generic_java_class, true);
+  }
+};
+
+inline const bool java_is_specialised_generic_class_type(const typet &type)
+{
+  return type.get_bool(ID_C_specialised_generic_java_class);
+}
+
+inline java_specialised_generic_class_typet
+  to_java_specialised_class_typet(const typet &type)
+{
+  INVARIANT(java_is_specialised_generic_class_type(type),
+    "Tried to convert a type that was not a specialised generic java class");
+  return static_cast<const java_specialised_generic_class_typet &>(type);
+}
+
 #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H

src/util/irep_ids.def

@@ -833,6 +833,7 @@ 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(generic_types, #generic_types)
 IREP_ID_TWO(type_variables, #type_variables)
+IREP_ID_TWO(C_specialised_generic_java_class, #specialised_class)
 IREP_ID_ONE(havoc_object)
 IREP_ID_TWO(overflow_shl, overflow-shl)
 

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

@@ -179,27 +179,27 @@ SCENARIO(
   // We have a 'harness' class who's only purpose is to contain a reference
   // to the generic class so that we can test the specialization of that generic
   // class
-  const irep_idt harness_class=
+  const irep_idt harness_class =
     "java::generic_field_array_instantiation";
 
   // We want to test that the specialized/instantiated class has it's field
   // type updated, so find the specialized class, not the generic class.
-  const irep_idt test_class=
+  const irep_idt test_class =
     "java::generic_field_array_instantiation$generic<java::array[reference]>";
 
   GIVEN("A generic type instantiated with an array type")
   {
-    symbol_tablet new_symbol_table=
+    symbol_tablet new_symbol_table =
       load_java_class(
         "generic_field_array_instantiation",
         "./java_bytecode/generate_concrete_generic_type");
 
     // Ensure the class has been specialized
     REQUIRE(new_symbol_table.has_symbol(harness_class));
-    const symbolt &harness_symbol=
+    const symbolt &harness_symbol =
       new_symbol_table.lookup_ref(harness_class);
 
-    const struct_typet::componentt &harness_component=
+    const struct_typet::componentt &harness_component =
       require_type::require_component(
         to_struct_type(harness_symbol.type),
         "f");
@@ -211,24 +211,87 @@ SCENARIO(
 
     // Test the specialized class
     REQUIRE(new_symbol_table.has_symbol(test_class));
-    const symbolt test_class_symbol=
+    const symbolt test_class_symbol =
       new_symbol_table.lookup_ref(test_class);
 
-    REQUIRE(test_class_symbol.type.id()==ID_struct);
-    const struct_typet::componentt &field_component=
+    REQUIRE(test_class_symbol.type.id() == ID_struct);
+    const struct_typet::componentt &field_component =
       require_type::require_component(
         to_struct_type(test_class_symbol.type),
         "gf");
-    const typet &test_field_type=field_component.type();
+    const typet &test_field_type = field_component.type();
 
-    REQUIRE(test_field_type.id()==ID_pointer);
-    REQUIRE(test_field_type.subtype().id()==ID_symbol);
-    const symbol_typet test_field_array=
+    REQUIRE(test_field_type.id() == ID_pointer);
+    REQUIRE(test_field_type.subtype().id() == ID_symbol);
+    const symbol_typet test_field_array =
       to_symbol_type(test_field_type.subtype());
-    REQUIRE(test_field_array.get_identifier()=="java::array[reference]");
-    const pointer_typet &element_type=
+    REQUIRE(test_field_array.get_identifier() == "java::array[reference]");
+    const pointer_typet &element_type =
       require_type::require_pointer(
         java_array_element_type(test_field_array),
         symbol_typet("java::java.lang.Float"));
   }
 }
+
+SCENARIO("generate_java_generic_type with a generic array field")
+{
+  const irep_idt harness_class = "java::generic_field_array_instantiation";
+  GIVEN("A generic class with a field of type T []")
+  {
+    symbol_tablet new_symbol_table = load_java_class(
+      "generic_field_array_instantiation",
+      "./java_bytecode/generate_concrete_generic_type");
+
+    const irep_idt &inner_class = "genericArray";
+
+    WHEN("We specialise that class from a reference to it")
+    {
+      specialise_generic_from_component(
+        harness_class, "genericArrayField", new_symbol_table);
+      THEN(
+        "There should be a specialised version of the class in the symbol "
+        "table")
+      {
+        const irep_idt &specialised_class_name = id2string(harness_class) +
+                                                 "$" + id2string(inner_class) +
+                                                 "<java::java.lang.Float>";
+        REQUIRE(new_symbol_table.has_symbol(specialised_class_name));
+
+        const symbolt test_class_symbol =
+          new_symbol_table.lookup_ref(specialised_class_name);
+
+        REQUIRE(test_class_symbol.type.id() == ID_struct);
+        THEN("The array field should be specialised to be an array of floats")
+        {
+          const struct_typet::componentt &field_component =
+            require_type::require_component(
+              to_struct_type(test_class_symbol.type), "arrayField");
+
+          const pointer_typet &component_pointer_type =
+            require_type::require_pointer(field_component.type(), {});
+
+          const symbol_typet &pointer_subtype = require_type::require_symbol(
+            component_pointer_type.subtype(), "java::array[reference]");
+
+          const typet &array_type = java_array_element_type(pointer_subtype);
+
+          require_type::require_pointer(
+            array_type, symbol_typet("java::java.lang.Float"));
+        }
+
+        THEN("The generic class field should be specialised to be a generic "
+               "class with the appropriate type")
+        {
+          const struct_typet::componentt &field_component =
+            require_type::require_component(
+              to_struct_type(test_class_symbol.type), "genericClassField");
+
+          require_type::require_java_generic_type(
+            field_component.type(),
+            {{require_type::type_parameter_kindt::Inst,"java::java.lang.Float"}});
+        }
+
+      }
+    }
+  }
+}