Merge pull request #1651 from thk123/bugfix/TG-1157/store-generic-info-in-specialized-class

[TG-1157] Store generic info in specialised class

Author: Thomas Kiley

src/java_bytecode/generate_java_generic_type.cpp

@@ -42,8 +42,8 @@ symbolt generate_java_generic_typet::operator()(
   const java_generic_class_typet &generic_class_definition =
     to_java_generic_class_type(to_java_class_type(pointer_subtype));
 
-  const irep_idt new_tag =
-    build_generic_tag(existing_generic_type, generic_class_definition);
+  const irep_idt generic_name =
+    build_generic_name(existing_generic_type, generic_class_definition);
   struct_union_typet::componentst replacement_components =
     generic_class_definition.components();
 
@@ -73,8 +73,12 @@ symbolt generate_java_generic_typet::operator()(
     pre_modification_size==after_modification_size,
     "All components in the original class should be in the new class");
 
-  const java_specialized_generic_class_typet new_java_class =
-    construct_specialised_generic_type(new_tag, replacement_components);
+  const java_specialized_generic_class_typet new_java_class{
+    generic_name,
+    generic_class_definition.get_tag(),
+    replacement_components,
+    existing_generic_type.generic_type_arguments()};
+
   const type_symbolt &class_symbol =
     build_symbol_from_specialised_class(new_java_class);
 
@@ -86,7 +90,7 @@ symbolt generate_java_generic_typet::operator()(
                       << " already exists" << messaget::eom;
   }
 
-  const auto expected_symbol="java::"+id2string(new_tag);
+  const auto expected_symbol="java::"+id2string(generic_name);
   auto symbol=symbol_table.lookup(expected_symbol);
   INVARIANT(symbol, "New class not created");
   return *symbol;
@@ -184,7 +188,7 @@ typet generate_java_generic_typet::substitute_type(
 /// \param existing_generic_type The type we want to concretise
 /// \param original_class
 /// \return A tag for the new generic we want a unique tag for.
-irep_idt generate_java_generic_typet::build_generic_tag(
+irep_idt generate_java_generic_typet::build_generic_name(
   const java_generic_typet &existing_generic_type,
   const java_class_typet &original_class) const
 {
@@ -227,19 +231,6 @@ irep_idt generate_java_generic_typet::build_generic_tag(
   return new_tag_buffer.str();
 }
 
-/// Build the specialised version of the specific class, with the specified
-/// parameters and name.
-/// \param new_tag: The new name for the class (like Generic<java::Float>)
-/// \param new_components: The specialised components
-/// \return The newly constructed class.
-java_specialized_generic_class_typet
-generate_java_generic_typet::construct_specialised_generic_type(
-  const irep_idt &new_tag,
-  const struct_typet::componentst &new_components) const
-{
-  return java_specialized_generic_class_typet{new_tag, new_components};
-}
-
 /// Construct the symbol to be moved into the symbol table
 /// \param specialised_class: The newly constructed specialised class
 /// \return The symbol to add to the symbol table

src/java_bytecode/generate_java_generic_type.h

@@ -17,14 +17,13 @@
 class generate_java_generic_typet
 {
 public:
-  generate_java_generic_typet(
-    message_handlert &message_handler);
+  explicit generate_java_generic_typet(message_handlert &message_handler);
 
   symbolt operator()(
     const java_generic_typet &existing_generic_type,
     symbol_tablet &symbol_table) const;
 private:
-  irep_idt build_generic_tag(
+  irep_idt build_generic_name(
     const java_generic_typet &existing_generic_type,
     const java_class_typet &original_class) const;
 
@@ -33,10 +32,6 @@ class generate_java_generic_typet
     const java_generic_class_typet &replacement_type,
     const java_generic_typet &generic_reference) const;
 
-  java_specialized_generic_class_typet construct_specialised_generic_type(
-    const irep_idt &new_tag,
-    const struct_typet::componentst &new_components) const;
-
   type_symbolt build_symbol_from_specialised_class(
     const java_class_typet &specialised_class) const;
 

src/java_bytecode/java_types.h

@@ -442,23 +442,41 @@ void get_dependencies_from_generic_parameters(
 class java_specialized_generic_class_typet : public java_class_typet
 {
 public:
+  typedef std::vector<reference_typet> generic_type_argumentst;
+
   /// Build the specialised version of the specific class, with the specified
   /// parameters and name.
-  /// \param new_tag: The new name for the class (like Generic<java::Float>)
+  /// \param generic_name: The new name for the class
+  ///   (like Generic<java::Float>)
+  /// \param tag: The name for the original class (like java::Generic)
   /// \param new_components: The specialised components
   /// \return The newly constructed class.
   java_specialized_generic_class_typet(
-    const irep_idt &new_tag,
-    const struct_typet::componentst &new_components)
+    const irep_idt &generic_name,
+    const irep_idt &tag,
+    const struct_typet::componentst &new_components,
+    const generic_type_argumentst &specialised_parameters)
   {
     set(ID_C_specialized_generic_java_class, true);
-    // We are specialising the logic - so we don't want to be marked as generic
-    set(ID_C_java_generics_class_type, false);
-    set(ID_name, "java::" + id2string(new_tag));
-    set(ID_base_name, id2string(new_tag));
+    set(ID_name, "java::" + id2string(generic_name));
+    set(ID_base_name, id2string(generic_name));
     components() = new_components;
-    const std::string &class_tag = id2string(new_tag);
-    set_tag(class_tag.substr(0, class_tag.find('<')));
+    set_tag(tag);
+
+    generic_type_arguments() = specialised_parameters;
+  }
+
+  /// \return vector of type variables
+  const generic_type_argumentst &generic_type_arguments() const
+  {
+    return (const generic_type_argumentst &)(find(ID_type_variables).get_sub());
+  }
+
+private:
+  /// \return vector of type variables
+  generic_type_argumentst &generic_type_arguments()
+  {
+    return (generic_type_argumentst &)(add(ID_type_variables).get_sub());
   }
 };