Constructed class to mimic the original class in all but name of symbol

When the tag was wrong it causes issues in calling methods and meant the
real time type information would not be handled correctly.

As the components on the new class have been moved, accessing the
components by index no longer works. Instead access the components by
name (and made use of other helper functions)

Author: thk123

src/java_bytecode/generate_java_generic_type.cpp

@@ -70,13 +70,20 @@ 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 auto expected_symbol="java::"+id2string(new_tag);
+  const java_class_typet &new_java_class = construct_specialised_generic_type(
+    generic_class_definition, new_tag, replacement_components);
+  const type_symbolt &class_symbol =
+    build_symbol_from_specialised_class(new_java_class);
+
+  std::pair<symbolt &, bool> res = symbol_table.insert(std::move(class_symbol));
+  if(!res.second)
+  {
+    messaget message(message_handler);
+    message.warning() << "stub class symbol " << class_symbol.name
+                      << " already exists" << messaget::eom;
+  }
 
-  generate_class_stub(
-    new_tag,
-    symbol_table,
-    message_handler,
-    replacement_components);
+  const auto expected_symbol="java::"+id2string(new_tag);
   auto symbol=symbol_table.lookup(expected_symbol);
   INVARIANT(symbol, "New class not created");
   return *symbol;
@@ -216,3 +223,38 @@ irep_idt generate_java_generic_typet::build_generic_tag(
 
   return new_tag_buffer.str();
 }
+
+/// Build the specalised version of the specific class, with the specified
+/// parameters and name.
+/// \param generic_class_definition: The generic class we are specialising
+/// \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_class_typet
+generate_java_generic_typet::construct_specialised_generic_type(
+  const java_generic_class_typet &generic_class_definition,
+  const irep_idt &new_tag,
+  const struct_typet::componentst &new_components) const
+{
+  java_class_typet specialised_class = generic_class_definition;
+  // We are specialising the logic - so we don't want to be marked as generic
+  specialised_class.set(ID_C_java_generics_class_type, false);
+  specialised_class.set(ID_name, "java::" + id2string(new_tag));
+  specialised_class.set(ID_base_name, new_tag);
+  specialised_class.components() = new_components;
+  return specialised_class;
+}
+
+/// 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
+type_symbolt generate_java_generic_typet::build_symbol_from_specialised_class(
+  const java_class_typet &specialised_class) const
+{
+  type_symbolt new_symbol(specialised_class);
+  new_symbol.base_name = specialised_class.get(ID_base_name);
+  new_symbol.pretty_name = specialised_class.get(ID_base_name);
+  new_symbol.name = specialised_class.get(ID_name);
+  new_symbol.mode = ID_java;
+  return new_symbol;
+}

src/java_bytecode/generate_java_generic_type.h

@@ -33,6 +33,14 @@ class generate_java_generic_typet
     const java_generic_class_typet &replacement_type,
     const java_generic_typet &generic_reference) const;
 
+  java_class_typet construct_specialised_generic_type(
+    const java_generic_class_typet &generic_class_definition,
+    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;
+
   message_handlert &message_handler;
 };
 

unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp

@@ -153,22 +153,22 @@ SCENARIO(
     REQUIRE(new_symbol_table.has_symbol(first_expected_symbol));
     auto first_symbol=new_symbol_table.lookup(first_expected_symbol);
     REQUIRE(first_symbol->type.id()==ID_struct);
-    auto first_symbol_type=
-      to_struct_type(first_symbol->type).components()[3].type();
-    REQUIRE(first_symbol_type.id()==ID_pointer);
-    REQUIRE(first_symbol_type.subtype().id()==ID_symbol);
-    REQUIRE(to_symbol_type(first_symbol_type.subtype()).get_identifier()==
-      "java::java.lang.Boolean");
+    const struct_union_typet::componentt &component =
+      require_type::require_component(
+        to_struct_type(first_symbol->type), "elem");
+    auto first_symbol_type=component.type();
+    require_type::require_pointer(
+      first_symbol_type, symbol_typet("java::java.lang.Boolean"));
 
     REQUIRE(new_symbol_table.has_symbol(second_expected_symbol));
     auto second_symbol=new_symbol_table.lookup(second_expected_symbol);
     REQUIRE(second_symbol->type.id()==ID_struct);
-    auto second_symbol_type=
-      to_struct_type(second_symbol->type).components()[3].type();
-    REQUIRE(second_symbol_type.id()==ID_pointer);
-    REQUIRE(second_symbol_type.subtype().id()==ID_symbol);
-    REQUIRE(to_symbol_type(second_symbol_type.subtype()).get_identifier()==
-            "java::java.lang.Integer");
+    const struct_union_typet::componentt &second_component =
+      require_type::require_component(
+        to_struct_type(second_symbol->type), "elem");
+    auto second_symbol_type=second_component.type();
+    require_type::require_pointer(
+      second_symbol_type, symbol_typet("java::java.lang.Integer"));
   }
 }