diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 56733460bae..77cd26f8092 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -36,16 +36,17 @@ symbolt generate_java_generic_typet::operator()( INVARIANT( pointer_subtype.id()==ID_struct, "Only pointers to classes in java"); INVARIANT( - is_java_generic_class_type(pointer_subtype), + is_java_generic_class_type(pointer_subtype) || + is_java_implicitly_generic_class_type(pointer_subtype), "Generic references type must be a generic class"); - const java_generic_class_typet &generic_class_definition = - to_java_generic_class_type(to_java_class_type(pointer_subtype)); + const java_class_typet &class_definition = + to_java_class_type(pointer_subtype); const irep_idt generic_name = - build_generic_name(existing_generic_type, generic_class_definition); + build_generic_name(existing_generic_type, class_definition); struct_union_typet::componentst replacement_components = - generic_class_definition.components(); + class_definition.components(); // Small auxiliary function, to perform the inplace // modification of the generic fields. @@ -53,7 +54,7 @@ symbolt generate_java_generic_typet::operator()( [&](struct_union_typet::componentt &component) { component.type() = substitute_type( - component.type(), generic_class_definition, existing_generic_type); + component.type(), class_definition, existing_generic_type); return component; }; @@ -66,8 +67,7 @@ symbolt generate_java_generic_typet::operator()( replacement_components.end(), replace_type_for_generic_field); - std::size_t after_modification_size = - generic_class_definition.components().size(); + std::size_t after_modification_size = class_definition.components().size(); INVARIANT( pre_modification_size==after_modification_size, @@ -75,7 +75,7 @@ symbolt generate_java_generic_typet::operator()( const java_specialized_generic_class_typet new_java_class{ generic_name, - generic_class_definition.get_tag(), + class_definition.get_tag(), replacement_components, existing_generic_type.generic_type_arguments()}; @@ -110,7 +110,7 @@ symbolt generate_java_generic_typet::operator()( /// there are none to replace, the original type. typet generate_java_generic_typet::substitute_type( const typet ¶meter_type, - const java_generic_class_typet &generic_class, + const java_class_typet &class_definition, const java_generic_typet &generic_reference) const { if(is_java_generic_parameter(parameter_type)) @@ -119,8 +119,28 @@ typet generate_java_generic_typet::substitute_type( .type_variable() .get_identifier(); - optionalt results = - java_generics_get_index_for_subtype(generic_class, component_identifier); + // see if it is a generic parameter introduced by this class + optionalt results; + if(is_java_generic_class_type(class_definition)) + { + const java_generic_class_typet &generic_class = + to_java_generic_class_type(class_definition); + + results = java_generics_get_index_for_subtype( + generic_class.generic_types(), component_identifier); + } + // see if it is an implicit generic parameter introduced by an outer class + if(!results.has_value()) + { + INVARIANT( + is_java_implicitly_generic_class_type(class_definition), + "The parameter must either be a generic type or implicit generic type"); + const java_implicitly_generic_class_typet &implicitly_generic_class = + to_java_implicitly_generic_class_type(class_definition); + results = java_generics_get_index_for_subtype( + implicitly_generic_class.implicit_generic_types(), + component_identifier); + } INVARIANT(results.has_value(), "generic component type not found"); return generic_reference.generic_type_arguments()[*results]; @@ -142,7 +162,7 @@ typet generate_java_generic_typet::substitute_type( [&](const reference_typet &generic_param) -> reference_typet { const typet &replacement_type = - substitute_type(generic_param, generic_class, generic_reference); + substitute_type(generic_param, class_definition, generic_reference); // This code will be simplified when references aren't considered to // be generic parameters @@ -172,8 +192,8 @@ typet generate_java_generic_typet::substitute_type( const typet &array_element_type = java_array_element_type(array_subtype); - const typet &new_array_type = - substitute_type(array_element_type, generic_class, generic_reference); + const typet &new_array_type = substitute_type( + array_element_type, class_definition, generic_reference); typet replacement_array_type = java_array_type('a'); replacement_array_type.subtype().set(ID_C_element_type, new_array_type); @@ -184,51 +204,173 @@ typet generate_java_generic_typet::substitute_type( return parameter_type; } -/// Build a unique tag for the generic to be instantiated. +/// Creates a name for an argument that is an array, e.g., for an array of +/// Integers it returns a string `array[reference]of_java::java.lang.Integer` +/// \param id argument of type array +/// \param generic_argument_p array reference type +/// \return name as a string +static irep_idt build_name_for_array_argument( + const irep_idt &id, + const reference_typet &generic_argument_p) +{ + PRECONDITION(is_java_array_tag(id)); + std::ostringstream name_buffer; + name_buffer << pretty_print_java_type(id2string(id)); + const typet &element_type = + java_array_element_type(to_symbol_type(generic_argument_p.subtype())); + + // If this is an array of references then we will specialize its + // identifier using the type of the objects in the array. Else, there + // can be a problem with the same symbols for different instantiations + // using arrays with different types. + if(element_type.id() == ID_pointer) + { + const symbol_typet element_symbol = to_symbol_type(element_type.subtype()); + name_buffer << "of_" + id2string(element_symbol.get_identifier()); + } + return name_buffer.str(); +} + +/// Build a generic name for a generic class, from given generic arguments. +/// For example, given a class `Class` with two generic type parameters +/// `java::Class::T` and `java::Class::U`, and two arguments +/// `java::java.lang.Integer` and `java::Outer$Inner`, the returned string is +/// ``. +/// \param generic_argument_p iterator over generic arguments +/// \param generic_type_p iterator over generic types, starts with types for +/// the given class, may continue with generic types of its inner classes +/// \param generic_types_end end of the vector of generic types +/// \param class_name name of the class for which the tag is being built +/// \return name as a string of the form `<*, *, ..., *>` +static irep_idt build_generic_name_for_class_arguments( + std::vector::const_iterator &generic_argument_p, + std::vector::const_iterator &generic_type_p, + const std::vector::const_iterator &generic_types_end, + const std::string &class_name) +{ + std::ostringstream name_buffer; + bool first = true; + std::string parameter_class_name = + (*generic_type_p).get_parameter_class_name(); + PRECONDITION(parameter_class_name == class_name); + + while(parameter_class_name == class_name) + { + if(first) + { + name_buffer << "<"; + first = false; + } + else + { + name_buffer << ", "; + } + + const irep_idt &id( + id2string((*generic_argument_p).subtype().get(ID_identifier))); + if(is_java_array_tag(id)) + { + name_buffer << build_name_for_array_argument(id, *generic_argument_p); + } + else + { + name_buffer << id2string(id); + } + + ++generic_argument_p; + ++generic_type_p; + if(generic_type_p != generic_types_end) + { + parameter_class_name = (*generic_type_p).get_parameter_class_name(); + } + else + { + break; + } + } + name_buffer << ">"; + return name_buffer.str(); +} + +/// Build a unique name for the generic to be instantiated. /// \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. +/// \return A name for the new generic we want a unique name for. irep_idt generate_java_generic_typet::build_generic_name( const java_generic_typet &existing_generic_type, const java_class_typet &original_class) const { - std::ostringstream new_tag_buffer; - new_tag_buffer << original_class.get_tag(); - new_tag_buffer << "<"; - bool first=true; - for(const typet &type_argument : existing_generic_type - .generic_type_arguments()) + std::ostringstream generic_name_buffer; + const std::string &original_class_name = original_class.get_tag().c_str(); + auto generic_argument_p = + existing_generic_type.generic_type_arguments().begin(); + + // if the original class is implicitly generic, add tags for all generic + // outer classes + // NOTE here we assume that the implicit generic types are ordered from the + // outermost outer class inwards, this is currently guaranteed by the way + // this vector is constructed in + // java_bytecode_convert_class:mark_java_implicitly_generic_class_type + if(is_java_implicitly_generic_class_type(original_class)) { - if(!first) - new_tag_buffer << ", "; - first=false; + const java_implicitly_generic_class_typet + &implicitly_generic_original_class = + to_java_implicitly_generic_class_type(original_class); 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 << pretty_print_java_type(id2string(id)); - if(is_java_array_tag(id)) + existing_generic_type.generic_type_arguments().size() >= + implicitly_generic_original_class.implicit_generic_types().size(), + "All implicit generic types must be concretised"); + auto implicit_generic_type_p = + implicitly_generic_original_class.implicit_generic_types().begin(); + const auto &implicit_generic_types_end = + implicitly_generic_original_class.implicit_generic_types().end(); + std::string current_outer_class_name; + + while(implicit_generic_type_p != implicit_generic_types_end) { - const typet &element_type = - java_array_element_type(to_symbol_type(type_argument.subtype())); - - // If this is an array of references then we will specialize its - // identifier using the type of the objects in the array. Else, there can - // be a problem with the same symbols for different instantiations using - // arrays with different types. - if(element_type.id() == ID_pointer) - { - const symbol_typet element_symbol = - to_symbol_type(element_type.subtype()); - new_tag_buffer << "of_" << id2string(element_symbol.get_identifier()); - } + current_outer_class_name = + (*implicit_generic_type_p).get_parameter_class_name(); + generic_name_buffer << current_outer_class_name; + generic_name_buffer << build_generic_name_for_class_arguments( + generic_argument_p, + implicit_generic_type_p, + implicit_generic_types_end, + current_outer_class_name); } + generic_name_buffer << original_class_name.substr( + current_outer_class_name.length(), std::string::npos); + } + else + { + generic_name_buffer << original_class_name; } - new_tag_buffer << ">"; + // if the original class is generic, add tag for the class itself + if(is_java_generic_class_type(original_class)) + { + const java_generic_class_typet &generic_original_class = + to_java_generic_class_type(original_class); - return new_tag_buffer.str(); + INVARIANT( + std::distance( + generic_argument_p, + existing_generic_type.generic_type_arguments().end()) == + static_cast(generic_original_class.generic_types().size()), + "All generic types must be concretised"); + auto generic_type_p = generic_original_class.generic_types().begin(); + + generic_name_buffer << build_generic_name_for_class_arguments( + generic_argument_p, + generic_type_p, + generic_original_class.generic_types().end(), + original_class_name); + } + + INVARIANT( + generic_argument_p == existing_generic_type.generic_type_arguments().end(), + "All type arguments must have been added to the name"); + return generic_name_buffer.str(); } /// 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 3e93faf0896..d8648639ba4 100644 --- a/src/java_bytecode/generate_java_generic_type.h +++ b/src/java_bytecode/generate_java_generic_type.h @@ -29,7 +29,7 @@ class generate_java_generic_typet typet substitute_type( const typet ¶meter_type, - const java_generic_class_typet &replacement_type, + const java_class_typet &replacement_type, const java_generic_typet &generic_reference) const; type_symbolt build_symbol_from_specialised_class( diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 9e617323067..0f0b15ed0dd 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -116,6 +116,17 @@ class java_generic_parametert:public reference_typet return const_cast(type_variables().front()); } + const std::string get_parameter_class_name() const + { + const std::string ¶meter_name = + type_variable().get_identifier().c_str(); + PRECONDITION(has_prefix(parameter_name, "java::")); + int prefix_length = std::string("java::").length(); + const std::string name = parameter_name.substr( + prefix_length, parameter_name.rfind("::") - prefix_length); + return name; + } + private: typedef std::vector type_variablest; const type_variablest &type_variables() const @@ -410,21 +421,18 @@ inline typet java_type_from_string_with_exception( /// \param identifier The string identifier of the type of the component. /// \return Optional with the size if the identifier was found. inline const optionalt java_generics_get_index_for_subtype( - const java_generic_class_typet &t, + const std::vector &gen_types, const irep_idt &identifier) { - const std::vector &gen_types= - t.generic_types(); - const auto iter = std::find_if( gen_types.cbegin(), gen_types.cend(), [&identifier](const java_generic_parametert &ref) { - return ref.type_variable().get_identifier()==identifier; + return ref.type_variable().get_identifier() == identifier; }); - if(iter==gen_types.cend()) + if(iter == gen_types.cend()) { return {}; } 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 f4b8625ceec..8155bdf3ef7 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 @@ -7,43 +7,20 @@ \*******************************************************************/ -#include -#include - #include #include #include - -#include +#include #include -#include -#include #include -/// Helper function to specalise a generic class from a named component of a -/// named class -/// \param class_name: The name of the class that has a generic component. -/// \param component_name: The name of the generic component -/// \param new_symbol_table: The symbol table to use. -void specialise_generic_from_component( - const irep_idt &class_name, - const irep_idt &component_name, - symbol_tablet &new_symbol_table) -{ - const symbolt &harness_symbol = new_symbol_table.lookup_ref(class_name); - const struct_typet::componentt &harness_component = - require_type::require_component( - to_struct_type(harness_symbol.type), component_name); - generic_utils::specialise_generic( - to_java_generic_type(harness_component.type()), new_symbol_table); -} - 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") @@ -52,14 +29,14 @@ SCENARIO( load_java_class("generic_two_fields", "./java_bytecode/generate_concrete_generic_type"); - specialise_generic_from_component( + generic_utils::specialise_generic_from_component( "java::generic_two_fields", "belem", new_symbol_table); 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"); + "java::generic_two_fields$bound_element"); const typet &symbol_type=class_symbol->type; REQUIRE(symbol_type.id()==ID_struct); @@ -92,7 +69,8 @@ SCENARIO( "[core][java_bytecode][generate_java_generic_type]") { auto expected_symbol = - "java::generic_two_parameters$KeyValuePair"; + "java::generic_two_parameters$KeyValuePair"; GIVEN("A generic java type with two generic parameters, like a Hashtable") { @@ -100,7 +78,7 @@ SCENARIO( load_java_class("generic_two_parameters", "./java_bytecode/generate_concrete_generic_type"); - specialise_generic_from_component( + generic_utils::specialise_generic_from_component( "java::generic_two_parameters", "bomb", new_symbol_table); REQUIRE(new_symbol_table.has_symbol( @@ -133,8 +111,10 @@ 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.") @@ -143,9 +123,9 @@ SCENARIO( load_java_class("generic_two_instances", "./java_bytecode/generate_concrete_generic_type"); - specialise_generic_from_component( + generic_utils::specialise_generic_from_component( "java::generic_two_instances", "bool_element", new_symbol_table); - specialise_generic_from_component( + generic_utils::specialise_generic_from_component( "java::generic_two_instances", "int_element", new_symbol_table); REQUIRE(new_symbol_table.has_symbol(first_expected_symbol)); @@ -228,8 +208,7 @@ SCENARIO( { const irep_idt test_class_integer = "java::generic_field_array_instantiation$generic"; + "of_java::java.lang.Integer>"; const irep_idt test_class_int = "java::generic_field_array_instantiation$generic"; @@ -276,14 +255,15 @@ SCENARIO( WHEN("We specialise that class from a reference to it") { - specialise_generic_from_component( + generic_utils::specialise_generic_from_component( harness_class, "genericArrayField", new_symbol_table); THEN( "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 = @@ -326,15 +306,14 @@ SCENARIO( WHEN( "We specialise the class with an array we should have appropriate types") { - specialise_generic_from_component( + generic_utils::specialise_generic_from_component( harness_class, "genericArrayArrayField", new_symbol_table); THEN( "There should be a specialised version of the class in the symbol " "table") { const std::string specialised_string = - ""; + ""; const irep_idt specialised_class_name = id2string(harness_class) + "$" + id2string(inner_class) + specialised_string; diff --git a/unit/java_bytecode/generate_concrete_generic_type/generate_outer_inner.cpp b/unit/java_bytecode/generate_concrete_generic_type/generate_outer_inner.cpp new file mode 100644 index 00000000000..d6c8b271d38 --- /dev/null +++ b/unit/java_bytecode/generate_concrete_generic_type/generate_outer_inner.cpp @@ -0,0 +1,598 @@ +/*******************************************************************\ + + Module: Unit tests for generating new type with generic parameters + substitued for concrete types + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include +#include +#include +#include + +SCENARIO("generate_outer_inner", "[core][java_bytecode][generate_outer_inner]") +{ + WHEN("Loading a class with generic and non-generic inner classes") + { + symbol_tablet new_symbol_table = load_java_class( + "generic_outer_inner", "./java_bytecode/generate_concrete_generic_type"); + const std::string &class_prefix = "java::generic_outer_inner"; + + WHEN("Its field t1 is specialised") + { + generic_utils::specialise_generic_from_component( + class_prefix, "t1", new_symbol_table); + const std::string &expected_prefix = + class_prefix + "$GenericOuter"; + THEN("The corresponding specialised class symbol is created") + { + REQUIRE(new_symbol_table.has_symbol(expected_prefix)); + const symbolt &expected_symbol = + new_symbol_table.lookup_ref(expected_prefix); + + const struct_typet class_struct = to_struct_type(expected_symbol.type); + REQUIRE(is_java_specialized_generic_class_type(class_struct)); + + THEN("It has field f1 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f1"); + require_type::require_pointer( + field.type(), symbol_typet("java::java.lang.Integer")); + } + + THEN("It has field f2 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f2"); + require_type::require_pointer( + field.type(), + symbol_typet("java::generic_outer_inner$GenericOuter$Inner")); + require_type::require_java_generic_type( + field.type(), + {{require_type::type_argument_kindt::Inst, + "java::java.lang.Integer"}}); + } + + THEN("It has field f3 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f3"); + require_type::require_pointer( + field.type(), + symbol_typet( + "java::generic_outer_inner$GenericOuter$GenericInner")); + require_type::require_java_generic_type( + field.type(), + {{require_type::type_argument_kindt::Inst, + "java::java.lang.Integer"}, + {require_type::type_argument_kindt::Inst, + "java::java.lang.String"}}); + } + + THEN("It has field this$0 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "this$0"); + require_type::require_pointer( + field.type(), symbol_typet("java::generic_outer_inner")); + } + } + } + + WHEN("Its field t2 is specialised") + { + generic_utils::specialise_generic_from_component( + class_prefix, "t2", new_symbol_table); + const std::string &expected_prefix = + class_prefix + "$GenericOuter$Inner"; + THEN("The corresponding specialised class symbol is created") + { + REQUIRE(new_symbol_table.has_symbol(expected_prefix)); + const symbolt &expected_symbol = + new_symbol_table.lookup_ref(expected_prefix); + + const struct_typet class_struct = to_struct_type(expected_symbol.type); + REQUIRE(is_java_specialized_generic_class_type(class_struct)); + + THEN("It has field f1 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f1"); + require_type::require_pointer( + field.type(), symbol_typet("java::java.lang.Integer")); + } + + THEN("It has field f2 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f2"); + require_type::require_pointer( + field.type(), symbol_typet("java::java.lang.Integer")); + } + + THEN("It has field this$1 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "this$1"); + // TODO should be java generic type - TG-1826 + } + } + } + + WHEN("Its field t2a is specialised") + { + generic_utils::specialise_generic_from_component( + class_prefix, "t2a", new_symbol_table); + const std::string &expected_prefix = + class_prefix + + "$GenericOuter$Inner"; + THEN("The corresponding specialised class symbol is created") + { + REQUIRE(new_symbol_table.has_symbol(expected_prefix)); + const symbolt &expected_symbol = + new_symbol_table.lookup_ref(expected_prefix); + + const struct_typet class_struct = to_struct_type(expected_symbol.type); + REQUIRE(is_java_specialized_generic_class_type(class_struct)); + + THEN("It has field f1 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f1"); + const symbol_typet &field_array = + to_symbol_type(field.type().subtype()); + REQUIRE(field_array.get_identifier() == "java::array[reference]"); + require_type::require_pointer( + java_array_element_type(field_array), + symbol_typet("java::java.lang.Integer")); + } + + THEN("It has field f2 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f2"); + require_type::require_pointer( + field.type(), symbol_typet("java::java.lang.Integer")); + } + + THEN("It has field this$1 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "this$1"); + // TODO should be java generic type - TG-1826 + } + } + } + + WHEN("Its field t3 is specialised") + { + generic_utils::specialise_generic_from_component( + class_prefix, "t3", new_symbol_table); + const std::string &expected_prefix = + class_prefix + "$GenericOuter$Inner$InnerInner"; + + THEN("The corresponding specialised class symbol is created") + { + REQUIRE(new_symbol_table.has_symbol(expected_prefix)); + const symbolt &expected_symbol = + new_symbol_table.lookup_ref(expected_prefix); + + const struct_typet class_struct = to_struct_type(expected_symbol.type); + REQUIRE(is_java_specialized_generic_class_type(class_struct)); + + THEN("It has field f1 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f1"); + require_type::require_pointer( + field.type(), symbol_typet("java::java.lang.String")); + } + + THEN("It has field this$2 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "this$2"); + // TODO should be java generic type - TG-1826 + } + } + } + + WHEN("Its field t3a is specialised") + { + generic_utils::specialise_generic_from_component( + class_prefix, "t3a", new_symbol_table); + const std::string &expected_prefix = class_prefix + + "$GenericOuter$Inner$" + "InnerInner"; + + THEN("The corresponding specialised class symbol is created") + { + REQUIRE(new_symbol_table.has_symbol(expected_prefix)); + const symbolt &expected_symbol = + new_symbol_table.lookup_ref(expected_prefix); + + const struct_typet class_struct = to_struct_type(expected_symbol.type); + REQUIRE(is_java_specialized_generic_class_type(class_struct)); + + THEN("It has field f1 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f1"); + const symbol_typet &field_array = + to_symbol_type(field.type().subtype()); + REQUIRE(field_array.get_identifier() == "java::array[reference]"); + require_type::require_pointer( + java_array_element_type(field_array), + symbol_typet("java::java.lang.String")); + } + + THEN("It has field this$2 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "this$2"); + // TODO should be java generic type - TG-1826 + } + } + } + + // TODO add test for field t4 once TG-1633 is done + + WHEN("Its field t5 is specialised") + { + generic_utils::specialise_generic_from_component( + class_prefix, "t5", new_symbol_table); + const std::string &expected_prefix = + class_prefix + + "$Outer$Inner$GenericInnerInner"; + + THEN("The corresponding specialised class symbol is created") + { + REQUIRE(new_symbol_table.has_symbol(expected_prefix)); + const symbolt &expected_symbol = + new_symbol_table.lookup_ref(expected_prefix); + + const struct_typet class_struct = to_struct_type(expected_symbol.type); + REQUIRE(is_java_specialized_generic_class_type(class_struct)); + + THEN("It has field f1 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f1"); + require_type::require_pointer( + field.type(), symbol_typet("java::java.lang.Integer")); + } + + THEN("It has field this$2 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "this$2"); + require_type::require_pointer( + field.type(), symbol_typet(class_prefix + "$Outer$Inner")); + } + } + } + + WHEN("Its field t6 is specialised") + { + generic_utils::specialise_generic_from_component( + class_prefix, "t6", new_symbol_table); + const std::string &expected_prefix = + class_prefix + "$Outer$GenericInner"; + + THEN("The corresponding specialised class symbol is created") + { + REQUIRE(new_symbol_table.has_symbol(expected_prefix)); + const symbolt &expected_symbol = + new_symbol_table.lookup_ref(expected_prefix); + + const struct_typet class_struct = to_struct_type(expected_symbol.type); + REQUIRE(is_java_specialized_generic_class_type(class_struct)); + + THEN("It has field f1 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f1"); + require_type::require_pointer( + field.type(), + symbol_typet( + "java::generic_outer_inner$Outer$" + "GenericInner$GenericInnerInner")); + require_type::require_java_generic_type( + field.type(), + {{require_type::type_argument_kindt::Inst, + "java::java.lang.Integer"}, + {require_type::type_argument_kindt::Inst, + "java::java.lang.String"}}); + } + + THEN("It has field this$1 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "this$1"); + require_type::require_pointer( + field.type(), symbol_typet(class_prefix + "$Outer")); + } + } + } + + WHEN("Its field t7 is specialised") + { + generic_utils::specialise_generic_from_component( + class_prefix, "t7", new_symbol_table); + const std::string &expected_prefix = + class_prefix + + "$Outer$GenericInner$InnerInner"; + + THEN("The corresponding specialised class symbol is created") + { + REQUIRE(new_symbol_table.has_symbol(expected_prefix)); + const symbolt &expected_symbol = + new_symbol_table.lookup_ref(expected_prefix); + + const struct_typet class_struct = to_struct_type(expected_symbol.type); + REQUIRE(is_java_specialized_generic_class_type(class_struct)); + + THEN("It has field f1 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f1"); + require_type::require_pointer( + field.type(), symbol_typet("java::java.lang.Integer")); + } + + THEN("It has field this$2 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "this$2"); + // TODO should be java generic type - TG-1826 + } + } + } + + WHEN("Its field t7a is specialised") + { + generic_utils::specialise_generic_from_component( + class_prefix, "t7a", new_symbol_table); + const std::string &expected_prefix = + class_prefix + + "$Outer$GenericInner$InnerInner"; + + THEN("The corresponding specialised class symbol is created") + { + REQUIRE(new_symbol_table.has_symbol(expected_prefix)); + const symbolt &expected_symbol = + new_symbol_table.lookup_ref(expected_prefix); + + const struct_typet class_struct = to_struct_type(expected_symbol.type); + REQUIRE(is_java_specialized_generic_class_type(class_struct)); + + THEN("It has field f1 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f1"); + const symbol_typet &field_array = + to_symbol_type(field.type().subtype()); + REQUIRE(field_array.get_identifier() == "java::array[reference]"); + require_type::require_pointer( + java_array_element_type(field_array), + symbol_typet("java::java.lang.Integer")); + } + + THEN("It has field this$2 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "this$2"); + // TODO should be java generic type - TG-1826 + } + } + } + + // TODO add test for field t8 once TG-1633 is done + + WHEN("Its field t9 is specialised") + { + generic_utils::specialise_generic_from_component( + class_prefix, "t9", new_symbol_table); + const std::string &expected_prefix = class_prefix + + "$Outer$TwoParamGenericInner"; + + THEN("The corresponding specialised class symbol is created") + { + REQUIRE(new_symbol_table.has_symbol(expected_prefix)); + const symbolt &expected_symbol = + new_symbol_table.lookup_ref(expected_prefix); + + const struct_typet class_struct = to_struct_type(expected_symbol.type); + REQUIRE(is_java_specialized_generic_class_type(class_struct)); + + THEN("It has field f1 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f1"); + require_type::require_pointer( + field.type(), symbol_typet("java::java.lang.Integer")); + } + + THEN("It has field f2 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f2"); + require_type::require_pointer( + field.type(), symbol_typet("java::java.lang.String")); + } + + THEN("It has field this$1 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "this$1"); + require_type::require_pointer( + field.type(), symbol_typet(class_prefix + "$Outer")); + } + } + } + + WHEN("Its field t10 is specialised") + { + generic_utils::specialise_generic_from_component( + class_prefix, "t10", new_symbol_table); + const std::string &expected_prefix = class_prefix + + "$Outer$TwoParamGenericInner$InnerInner"; + + THEN("The corresponding specialised class symbol is created") + { + REQUIRE(new_symbol_table.has_symbol(expected_prefix)); + const symbolt &expected_symbol = + new_symbol_table.lookup_ref(expected_prefix); + + const struct_typet class_struct = to_struct_type(expected_symbol.type); + REQUIRE(is_java_specialized_generic_class_type(class_struct)); + + THEN("It has field f1 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f1"); + require_type::require_pointer( + field.type(), symbol_typet("java::java.lang.Integer")); + } + + THEN("It has field f2 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f2"); + require_type::require_pointer( + field.type(), symbol_typet("java::java.lang.String")); + } + + THEN("It has field this$2 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "this$2"); + // TODO should be java generic type - TG-1826 + } + } + } + + WHEN("Its field t10a is specialised") + { + generic_utils::specialise_generic_from_component( + class_prefix, "t10a", new_symbol_table); + const std::string &expected_prefix = + class_prefix + + "$Outer$TwoParamGenericInner$InnerInner"; + + THEN("The corresponding specialised class symbol is created") + { + REQUIRE(new_symbol_table.has_symbol(expected_prefix)); + const symbolt &expected_symbol = + new_symbol_table.lookup_ref(expected_prefix); + + const struct_typet class_struct = to_struct_type(expected_symbol.type); + REQUIRE(is_java_specialized_generic_class_type(class_struct)); + + THEN("It has field f1 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f1"); + const symbol_typet &field_array = + to_symbol_type(field.type().subtype()); + REQUIRE(field_array.get_identifier() == "java::array[reference]"); + require_type::require_pointer( + java_array_element_type(field_array), + symbol_typet("java::java.lang.Integer")); + } + + THEN("It has field f2 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f2"); + const symbol_typet &field_array = + to_symbol_type(field.type().subtype()); + REQUIRE(field_array.get_identifier() == "java::array[reference]"); + require_type::require_pointer( + java_array_element_type(field_array), + symbol_typet("java::java.lang.String")); + } + + THEN("It has field this$2 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "this$2"); + // TODO should be java generic type - TG-1826 + } + } + } + + WHEN("Its field t11 is specialised") + { + generic_utils::specialise_generic_from_component( + class_prefix, "t11", new_symbol_table); + const std::string &expected_prefix = + class_prefix + "$GenericOuter"; + + THEN("The corresponding specialised class symbol is created") + { + REQUIRE(new_symbol_table.has_symbol(expected_prefix)); + const symbolt &expected_symbol = + new_symbol_table.lookup_ref(expected_prefix); + + const struct_typet class_struct = to_struct_type(expected_symbol.type); + REQUIRE(is_java_specialized_generic_class_type(class_struct)); + + THEN("It has field f1 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f1"); + require_type::require_pointer( + field.type(), symbol_typet("java::generic_outer_inner$Outer")); + } + + THEN("It has field f2 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f2"); + require_type::require_pointer( + field.type(), + symbol_typet("java::generic_outer_inner$GenericOuter$Inner")); + require_type::require_java_generic_type( + field.type(), + {{require_type::type_argument_kindt::Inst, + "java::generic_outer_inner$Outer"}}); + } + + THEN("It has field f3 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "f3"); + require_type::require_pointer( + field.type(), + symbol_typet( + "java::generic_outer_inner$GenericOuter$GenericInner")); + require_type::require_java_generic_type( + field.type(), + {{require_type::type_argument_kindt::Inst, + "java::generic_outer_inner$Outer"}, + {require_type::type_argument_kindt::Inst, + "java::java.lang.String"}}); + } + + THEN("It has field this$0 of correct type") + { + const struct_union_typet::componentt &field = + require_type::require_component(class_struct, "this$0"); + require_type::require_pointer( + field.type(), symbol_typet(class_prefix)); + } + } + } + } +} diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$GenericInner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$GenericInner.class new file mode 100644 index 00000000000..1d9fe54995c Binary files /dev/null and b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$GenericInner.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$Inner$InnerInner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$Inner$InnerInner.class new file mode 100644 index 00000000000..8f6d49bec1f Binary files /dev/null and b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$Inner$InnerInner.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$Inner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$Inner.class new file mode 100644 index 00000000000..bc9fa9be685 Binary files /dev/null and b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter$Inner.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter.class new file mode 100644 index 00000000000..be62d73f664 Binary files /dev/null and b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$GenericOuter.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner$GenericInnerInner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner$GenericInnerInner.class new file mode 100644 index 00000000000..be2037c6c88 Binary files /dev/null and b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner$GenericInnerInner.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner$InnerInner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner$InnerInner.class new file mode 100644 index 00000000000..36972ebe360 Binary files /dev/null and b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner$InnerInner.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner.class new file mode 100644 index 00000000000..2368c6b18ab Binary files /dev/null and b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$GenericInner.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner$GenericInnerInner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner$GenericInnerInner.class new file mode 100644 index 00000000000..af00787fbf9 Binary files /dev/null and b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner$GenericInnerInner.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner$InnerInner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner$InnerInner.class new file mode 100644 index 00000000000..d481c3322f3 Binary files /dev/null and b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner$InnerInner.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner.class new file mode 100644 index 00000000000..7495bb55358 Binary files /dev/null and b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$Inner.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$TwoParamGenericInner$InnerInner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$TwoParamGenericInner$InnerInner.class new file mode 100644 index 00000000000..d7e166e8c9a Binary files /dev/null and b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$TwoParamGenericInner$InnerInner.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$TwoParamGenericInner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$TwoParamGenericInner.class new file mode 100644 index 00000000000..8ce274e530c Binary files /dev/null and b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer$TwoParamGenericInner.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer.class new file mode 100644 index 00000000000..508f964ddf8 Binary files /dev/null and b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner$Outer.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner.class b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner.class new file mode 100644 index 00000000000..acf46950e1e Binary files /dev/null and b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner.java b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner.java new file mode 100644 index 00000000000..7de5a6bea30 --- /dev/null +++ b/unit/java_bytecode/generate_concrete_generic_type/generic_outer_inner.java @@ -0,0 +1,82 @@ +public class generic_outer_inner +{ + class GenericOuter + { + class Inner { + T f1; + Integer f2; + + class InnerInner { + T f1; + } + } + + class GenericInner + { + + } + + T f1; + Inner f2; + GenericInner f3; + } + + class Outer + { + class Inner + { + class GenericInnerInner + { + T f1; + } + } + + class GenericInner + { + class InnerInner + { + T f1; + } + + class GenericInnerInner + { + T f1; + U f2; + } + + GenericInnerInner f1; + } + + class TwoParamGenericInner + { + class InnerInner + { + U f1; + V f2; + } + + U f1; + V f2; + } + } + + GenericOuter t1; + GenericOuter.Inner t2; + GenericOuter.Inner t2a; + GenericOuter.Inner.InnerInner t3; + GenericOuter.Inner.InnerInner t3a; + GenericOuter.GenericInner t4; + + Outer.Inner.GenericInnerInner t5; + Outer.GenericInner t6; + Outer.GenericInner.InnerInner t7; + Outer.GenericInner.InnerInner t7a; + Outer.GenericInner.GenericInnerInner t8; + + Outer.TwoParamGenericInner t9; + Outer.TwoParamGenericInner.InnerInner t10; + Outer.TwoParamGenericInner.InnerInner t10a; + + GenericOuter t11; +} + diff --git a/unit/testing-utils/generic_utils.cpp b/unit/testing-utils/generic_utils.cpp index e15276e7bd2..caa3f8db341 100644 --- a/unit/testing-utils/generic_utils.cpp +++ b/unit/testing-utils/generic_utils.cpp @@ -32,7 +32,9 @@ void generic_utils::specialise_generic( namespacet ns(new_symbol_table); const typet &class_type = ns.follow(example_type.subtype()); - REQUIRE(is_java_generic_class_type(class_type)); + REQUIRE( + (is_java_generic_class_type(class_type) || + is_java_implicitly_generic_class_type(class_type))); // Generate the specialised version. ui_message_handlert message_handler; @@ -40,3 +42,21 @@ void generic_utils::specialise_generic( instantiate_generic_type( to_java_generic_type(example_type), new_symbol_table); } + +/// Helper function to specialise a generic class from a named component of a +/// named class +/// \param class_name: The name of the class that has a generic component. +/// \param component_name: The name of the generic component +/// \param new_symbol_table: The symbol table to use. +void generic_utils::specialise_generic_from_component( + const irep_idt &class_name, + const irep_idt &component_name, + symbol_tablet &new_symbol_table) +{ + const symbolt &harness_symbol = new_symbol_table.lookup_ref(class_name); + const struct_typet::componentt &harness_component = + require_type::require_component( + to_struct_type(harness_symbol.type), component_name); + generic_utils::specialise_generic( + to_java_generic_type(harness_component.type()), new_symbol_table); +} diff --git a/unit/testing-utils/generic_utils.h b/unit/testing-utils/generic_utils.h index 4bfc70fb4be..e0d36d7beb7 100644 --- a/unit/testing-utils/generic_utils.h +++ b/unit/testing-utils/generic_utils.h @@ -21,6 +21,11 @@ namespace generic_utils void specialise_generic( const java_generic_typet &example_type, symbol_tablet &new_symbol_table); + +void specialise_generic_from_component( + const irep_idt &class_name, + const irep_idt &component_name, + symbol_tablet &new_symbol_table); } #endif // CPROVER_TESTING_UTILS_GENERIC_UTILS_H