diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 1cc35143fa9..56733460bae 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/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) -/// \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 diff --git a/src/java_bytecode/generate_java_generic_type.h b/src/java_bytecode/generate_java_generic_type.h index 5c01756f1b2..3e93faf0896 100644 --- a/src/java_bytecode/generate_java_generic_type.h +++ b/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; diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index d52fa713de6..9e617323067 100644 --- a/src/java_bytecode/java_types.h +++ b/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 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) + /// \param generic_name: The new name for the class + /// (like Generic) + /// \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()); } };