diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 00f45eb8ec9..d94c6c0e638 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -11,6 +11,20 @@ #include #include +/// Strip the package name from a java type, for the type to be +/// pretty printed (java::java.lang.Integer -> Integer). +/// \param fqn_java_type The java type we want to pretty print. +/// \return The pretty printed type if there was a match of the +// qualifiers, or the type as it was passed otherwise. +static std::string pretty_print_java_type(const std::string &fqn_java_type) +{ + const std::string java_lang("java::java.lang."); + const std::string package_name(java_class_to_package(fqn_java_type) + "."); + if(package_name == java_lang) + return fqn_java_type.substr(java_lang.length()); + return fqn_java_type; +} + generate_java_generic_typet::generate_java_generic_typet( message_handlert &message_handler): message_handler(message_handler) @@ -70,8 +84,8 @@ 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_class_typet &new_java_class = construct_specialised_generic_type( - generic_class_definition, new_tag, replacement_components); + const java_specialized_generic_class_typet new_java_class = + construct_specialised_generic_type(new_tag, replacement_components); const type_symbolt &class_symbol = build_symbol_from_specialised_class(new_java_class); @@ -193,14 +207,14 @@ irep_idt generate_java_generic_typet::build_generic_tag( .generic_type_arguments()) { if(!first) - new_tag_buffer << ","; + new_tag_buffer << ", "; first=false; INVARIANT( !is_java_generic_parameter(type_argument), "Only create full concretized generic types"); const irep_idt &id(id2string(type_argument.subtype().get(ID_identifier))); - new_tag_buffer << id2string(id); + new_tag_buffer << pretty_print_java_type(id2string(id)); if(is_java_array_tag(id)) { const typet &element_type = @@ -224,25 +238,17 @@ 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 +/// Build the specialised 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) /// \param new_components: The specialised components /// \return The newly constructed class. -java_class_typet +java_specialized_generic_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; + return java_specialized_generic_class_typet{new_tag, new_components}; } /// Construct the symbol to be moved into the symbol table diff --git a/src/java_bytecode/generate_java_generic_type.h b/src/java_bytecode/generate_java_generic_type.h index f7e7656abc7..5c01756f1b2 100644 --- a/src/java_bytecode/generate_java_generic_type.h +++ b/src/java_bytecode/generate_java_generic_type.h @@ -33,8 +33,7 @@ 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, + java_specialized_generic_class_typet construct_specialised_generic_type( const irep_idt &new_tag, const struct_typet::componentst &new_components) const; diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 3c4df0ade38..1957880ee19 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -374,4 +374,55 @@ void get_dependencies_from_generic_parameters( const typet &, std::set &); +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 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) + { + 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)); + components() = new_components; + const std::string &class_tag = id2string(new_tag); + set_tag(class_tag.substr(0, class_tag.find('<'))); + } +}; + +inline bool is_java_specialized_generic_class_type(const typet &type) +{ + return type.get_bool(ID_C_specialized_generic_java_class); +} + +inline bool is_java_specialized_generic_class_type(typet &type) +{ + return type.get_bool(ID_C_specialized_generic_java_class); +} + +inline java_specialized_generic_class_typet +to_java_specialized_generic_class_type(const typet &type) +{ + INVARIANT( + is_java_specialized_generic_class_type(type), + "Tried to convert a type that was not a specialised generic java class"); + return static_cast(type); +} + +inline java_specialized_generic_class_typet +to_java_specialized_generic_class_type(typet &type) +{ + INVARIANT( + is_java_specialized_generic_class_type(type), + "Tried to convert a type that was not a specialised generic java class"); + return static_cast(type); +} + #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 810e2f4b260..2a25ab2d250 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -830,6 +830,7 @@ IREP_ID_ONE(integer_dereference) IREP_ID_TWO(C_java_generic_parameter, #java_generic_parameter) 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(C_specialized_generic_java_class, #specialized_generic_java_class) IREP_ID_TWO(generic_types, #generic_types) IREP_ID_TWO(type_variables, #type_variables) IREP_ID_ONE(havoc_object) diff --git a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp index 7fb1a1a2519..de216862376 100644 --- a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp +++ b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp @@ -40,8 +40,7 @@ SCENARIO( "generate_java_generic_type_from_file", "[core][java_bytecode][generate_java_generic_type]") { - auto expected_symbol= - "java::generic_two_fields$bound_element"; + auto expected_symbol = "java::generic_two_fields$bound_element"; GIVEN("A generic java type with two generic fields and a concrete " "substitution") @@ -56,8 +55,8 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(expected_symbol)); THEN("The class should contain two instantiated fields.") { - const auto &class_symbol=new_symbol_table.lookup( - "java::generic_two_fields$bound_element"); + const auto &class_symbol = new_symbol_table.lookup( + "java::generic_two_fields$bound_element"); const typet &symbol_type=class_symbol->type; REQUIRE(symbol_type.id()==ID_struct); @@ -89,10 +88,8 @@ SCENARIO( "generate_java_generic_type_from_file_two_params", "[core][java_bytecode][generate_java_generic_type]") { - auto expected_symbol= - "java::generic_two_parameters$KeyValuePair" - ""; + auto expected_symbol = + "java::generic_two_parameters$KeyValuePair"; GIVEN("A generic java type with two generic parameters, like a Hashtable") { @@ -133,10 +130,8 @@ SCENARIO( // After we have loaded the class and converted the generics, // the presence of these two symbols in the symbol table is // proof enough that we did the work we needed to do correctly. - auto first_expected_symbol= - "java::generic_two_instances$element"; - auto second_expected_symbol= - "java::generic_two_instances$element"; + auto first_expected_symbol = "java::generic_two_instances$element"; + auto second_expected_symbol = "java::generic_two_instances$element"; GIVEN("A generic java type with a field that refers to another generic with" " an uninstantiated parameter.") @@ -284,9 +279,8 @@ SCENARIO( "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) + - ""; + const irep_idt specialised_class_name = + id2string(harness_class) + "$" + id2string(inner_class) + ""; REQUIRE(new_symbol_table.has_symbol(specialised_class_name)); const symbolt test_class_symbol =