From 731028161a6aa973a001bb7ae45c124f06a6f20b Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 4 Dec 2017 18:12:43 +0000 Subject: [PATCH 1/3] Tidying of java_specialized_generic_class_typet Named the tag more intuitively (since it is not used as the tag). Added explicit on single parameter constructor. --- src/java_bytecode/generate_java_generic_type.h | 3 +-- src/java_bytecode/java_types.h | 11 +++++------ 2 files changed, 6 insertions(+), 8 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.h b/src/java_bytecode/generate_java_generic_type.h index 5c01756f1b2..84f8a467a31 100644 --- a/src/java_bytecode/generate_java_generic_type.h +++ b/src/java_bytecode/generate_java_generic_type.h @@ -17,8 +17,7 @@ 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, diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index d52fa713de6..c5f6849e919 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -444,18 +444,17 @@ class java_specialized_generic_class_typet : public java_class_typet public: /// 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 new_components: The specialised components /// \return The newly constructed class. java_specialized_generic_class_typet( - const irep_idt &new_tag, + const irep_idt &generic_name, const struct_typet::componentst &new_components) { 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('<'))); From 58f8482048fa76be9d0ab5b7971ea78980e208fc Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 4 Dec 2017 18:13:45 +0000 Subject: [PATCH 2/3] Add the generic type arguments to the specalised type This is useful information when trying to output this type without muddying the waters by labeling it as a generic type (which it isn't) --- .../generate_java_generic_type.cpp | 21 +++++----------- .../generate_java_generic_type.h | 4 --- src/java_bytecode/java_types.h | 25 ++++++++++++++++--- 3 files changed, 28 insertions(+), 22 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 1cc35143fa9..454e88d130f 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -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{ + new_tag, + 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); @@ -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 84f8a467a31..aad1a86d325 100644 --- a/src/java_bytecode/generate_java_generic_type.h +++ b/src/java_bytecode/generate_java_generic_type.h @@ -32,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 c5f6849e919..9e617323067 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -442,22 +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 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 &generic_name, - const struct_typet::componentst &new_components) + const irep_idt &tag, + const struct_typet::componentst &new_components, + const generic_type_argumentst &specialised_parameters) { set(ID_C_specialized_generic_java_class, true); 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()); } }; From 3a4652554329a689a3d8c43e7311f6633358aca3 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 6 Dec 2017 10:41:50 +0000 Subject: [PATCH 3/3] Renaming generic_tag to generic_name since not a tag --- src/java_bytecode/generate_java_generic_type.cpp | 10 +++++----- src/java_bytecode/generate_java_generic_type.h | 2 +- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 454e88d130f..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(); @@ -74,7 +74,7 @@ symbolt generate_java_generic_typet::operator()( "All components in the original class should be in the new class"); const java_specialized_generic_class_typet new_java_class{ - new_tag, + generic_name, generic_class_definition.get_tag(), replacement_components, existing_generic_type.generic_type_arguments()}; @@ -90,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; @@ -188,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 { diff --git a/src/java_bytecode/generate_java_generic_type.h b/src/java_bytecode/generate_java_generic_type.h index aad1a86d325..3e93faf0896 100644 --- a/src/java_bytecode/generate_java_generic_type.h +++ b/src/java_bytecode/generate_java_generic_type.h @@ -23,7 +23,7 @@ class generate_java_generic_typet 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;