diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index bcabd9f48d6..2b5badb381b 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -11,7 +11,6 @@ #include #include - generate_java_generic_typet::generate_java_generic_typet( message_handlert &message_handler): message_handler(message_handler) @@ -33,41 +32,26 @@ 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), + "Generic references type must be a generic class"); - const java_class_typet &replacement_type= - to_java_class_type(pointer_subtype); - const irep_idt new_tag=build_generic_tag( - existing_generic_type, replacement_type); - struct_union_typet::componentst replacement_components= - replacement_type.components(); + 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); + struct_union_typet::componentst replacement_components = + generic_class_definition.components(); // Small auxiliary function, to perform the inplace // modification of the generic fields. - auto replace_type_for_generic_field= - [&](struct_union_typet::componentt &component) - { - if(is_java_generic_parameter(component.type())) - { - auto replacement_type_param= - to_java_generics_class_type(replacement_type); - - auto component_identifier= - to_java_generic_parameter(component.type()).type_variable() - .get_identifier(); - - optionalt results=java_generics_get_index_for_subtype( - replacement_type_param, component_identifier); + auto replace_type_for_generic_field = + [&](struct_union_typet::componentt &component) { - INVARIANT( - results.has_value(), - "generic component type not found"); + component.type() = substitute_type( + component.type(), generic_class_definition, existing_generic_type); - if(results) - { - component.type()= - existing_generic_type.generic_type_variables()[*results]; - } - } return component; }; @@ -79,8 +63,8 @@ symbolt generate_java_generic_typet::operator()( replacement_components.end(), replace_type_for_generic_field); - std::size_t after_modification_size= - replacement_type.components().size(); + std::size_t after_modification_size = + generic_class_definition.components().size(); INVARIANT( pre_modification_size==after_modification_size, @@ -98,6 +82,95 @@ symbolt generate_java_generic_typet::operator()( return *symbol; } +/// For a given type, if the type contains a Java generic parameter, we look +/// that parameter up and return the relevant type. This works recursively on +/// arrays so that T [] is converted to RelevantType []. +/// \param parameter_type: The type under consideration +/// \param generic_class: The generic class that the \p parameter_type +/// belongs to (e.g. the type of a component of the class). This is used to +/// look up the mapping from name of generic parameter to its index. +/// \param generic_reference: The instantiated version of the generic class +/// used to look up the instantiated type. This is expected to be fully +/// instantiated. +/// \return A newly constructed type with generic parameters replaced, or if +/// 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_generic_typet &generic_reference) const +{ + if(is_java_generic_parameter(parameter_type)) + { + auto component_identifier = to_java_generic_parameter(parameter_type) + .type_variable() + .get_identifier(); + + optionalt results = + java_generics_get_index_for_subtype(generic_class, component_identifier); + + INVARIANT(results.has_value(), "generic component type not found"); + return generic_reference.generic_type_variables()[*results]; + } + else if(parameter_type.id() == ID_pointer) + { + if(is_java_generic_type(parameter_type)) + { + const java_generic_typet &generic_type = + to_java_generic_type(parameter_type); + + java_generic_typet::generic_type_variablest replaced_type_variables; + + // Swap each parameter + std::transform( + generic_type.generic_type_variables().begin(), + generic_type.generic_type_variables().end(), + std::back_inserter(replaced_type_variables), + [&](const java_generic_parametert &generic_param) + -> java_generic_parametert { + const typet &replacement_type = + substitute_type(generic_param, generic_class, generic_reference); + + // This code will be simplified when references aren't considered to + // be generic parameters + if(is_java_generic_parameter(replacement_type)) + { + return to_java_generic_parameter(replacement_type); + } + else + { + INVARIANT( + is_reference(replacement_type), + "All generic parameters should be references"); + return java_generic_inst_parametert( + to_symbol_type(replacement_type.subtype())); + } + }); + + java_generic_typet new_type = generic_type; + new_type.generic_type_variables() = replaced_type_variables; + return new_type; + } + else if(parameter_type.subtype().id() == ID_symbol) + { + const symbol_typet &array_subtype = + to_symbol_type(parameter_type.subtype()); + if(is_java_array_tag(array_subtype.get_identifier())) + { + 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); + + typet replacement_array_type = java_array_type('a'); + replacement_array_type.subtype().set(ID_C_element_type, new_array_type); + return replacement_array_type; + } + } + } + return parameter_type; +} + /// Build a unique tag for the generic to be instantiated. /// \param existing_generic_type The type we want to concretise /// \param original_class diff --git a/src/java_bytecode/generate_java_generic_type.h b/src/java_bytecode/generate_java_generic_type.h index c171976e5c7..601c32ca7a6 100644 --- a/src/java_bytecode/generate_java_generic_type.h +++ b/src/java_bytecode/generate_java_generic_type.h @@ -28,6 +28,11 @@ class generate_java_generic_typet const java_generic_typet &existing_generic_type, const java_class_typet &original_class) const; + typet substitute_type( + const typet ¶meter_type, + const java_generic_class_typet &replacement_type, + const java_generic_typet &generic_reference) const; + message_handlert &message_handler; }; diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 0b0b71a1d09..b84978b2020 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -97,7 +97,7 @@ void java_bytecode_convert_classt::convert(const classt &c) java_class_typet class_type; if(c.signature.has_value() && c.signature.value()[0]=='<') { - java_generics_class_typet generic_class_type; + java_generic_class_typet generic_class_type; #ifdef DEBUG std::cout << "INFO: found generic class signature " << c.signature.value() diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 740d347feb7..cd4aa45813d 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -254,12 +254,12 @@ inline java_generic_typet &to_java_generic_type(typet &type) /// vector of java_generic_type variables. /// /// For example, a class definition `class MyGenericClass` -class java_generics_class_typet:public java_class_typet +class java_generic_class_typet : public java_class_typet { public: typedef std::vector generic_typest; - java_generics_class_typet() + java_generic_class_typet() { set(ID_C_java_generics_class_type, true); } @@ -277,27 +277,27 @@ class java_generics_class_typet:public java_class_typet /// \param type: the type to check /// \return true if type is a java class type with generics -inline bool is_java_generics_class_type(const typet &type) +inline bool is_java_generic_class_type(const typet &type) { return type.get_bool(ID_C_java_generics_class_type); } /// \param type: the type to check /// \return cast of type to java_generics_class_typet -inline const java_generics_class_typet &to_java_generics_class_type( - const java_class_typet &type) +inline const java_generic_class_typet & +to_java_generic_class_type(const java_class_typet &type) { - PRECONDITION(is_java_generics_class_type(type)); - return static_cast(type); + PRECONDITION(is_java_generic_class_type(type)); + return static_cast(type); } /// \param type: source type /// \return cast of type into a java class type with generics -inline java_generics_class_typet &to_java_generics_class_type( - java_class_typet &type) +inline java_generic_class_typet & +to_java_generic_class_type(java_class_typet &type) { - PRECONDITION(is_java_generics_class_type(type)); - return static_cast(type); + PRECONDITION(is_java_generic_class_type(type)); + return static_cast(type); } /// Access information of instantiated type params of java instantiated type. @@ -318,9 +318,8 @@ inline const typet &java_generic_get_inst_type( /// \param index: the index of the type variable /// \param type: the type from which to extract the type variable /// \return the name of the generic type variable of t at the given index -inline const irep_idt &java_generics_class_type_var( - size_t index, - const java_generics_class_typet &type) +inline const irep_idt & +java_generic_class_type_var(size_t index, const java_generic_class_typet &type) { const std::vector &gen_types=type.generic_types(); @@ -334,13 +333,11 @@ inline const irep_idt &java_generics_class_type_var( /// \param index: the index of the type variable /// \param t: the type from which to extract the type bound /// \return the type of the bound of the type variable -inline const typet &java_generics_class_type_bound( - size_t index, - const typet &t) +inline const typet &java_generic_class_type_bound(size_t index, const typet &t) { - PRECONDITION(is_java_generics_class_type(t)); - const java_generics_class_typet &type= - to_java_generics_class_type(to_java_class_type(t)); + PRECONDITION(is_java_generic_class_type(t)); + const java_generic_class_typet &type = + to_java_generic_class_type(to_java_class_type(t)); const std::vector &gen_types=type.generic_types(); PRECONDITION(index java_generics_get_index_for_subtype( - const java_generics_class_typet &t, + const java_generic_class_typet &t, const irep_idt &identifier) { const std::vector &gen_types= 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 2c746a37c83..1e7d52981a2 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 @@ -179,8 +179,7 @@ SCENARIO( // We have a 'harness' class who's only purpose is to contain a reference // to the generic class so that we can test the specialization of that generic // class - const irep_idt harness_class= - "java::generic_field_array_instantiation"; + const irep_idt harness_class = "java::generic_field_array_instantiation"; // We want to test that the specialized/instantiated class has it's field // type updated, so find the specialized class, not the generic class. @@ -190,20 +189,16 @@ SCENARIO( GIVEN("A generic type instantiated with an array type") { - symbol_tablet new_symbol_table= - load_java_class( - "generic_field_array_instantiation", - "./java_bytecode/generate_concrete_generic_type"); + symbol_tablet new_symbol_table = load_java_class( + "generic_field_array_instantiation", + "./java_bytecode/generate_concrete_generic_type"); // Ensure the class has been specialized REQUIRE(new_symbol_table.has_symbol(harness_class)); - const symbolt &harness_symbol= - new_symbol_table.lookup_ref(harness_class); + const symbolt &harness_symbol = new_symbol_table.lookup_ref(harness_class); - const struct_typet::componentt &harness_component= - require_type::require_component( - to_struct_type(harness_symbol.type), - "f"); + const struct_typet::componentt &harness_component = + require_type::require_component(to_struct_type(harness_symbol.type), "f"); ui_message_handlert message_handler; generate_java_generic_typet instantiate_generic_type(message_handler); @@ -212,25 +207,22 @@ SCENARIO( // Test the specialized class REQUIRE(new_symbol_table.has_symbol(test_class)); - const symbolt test_class_symbol= - new_symbol_table.lookup_ref(test_class); + const symbolt test_class_symbol = new_symbol_table.lookup_ref(test_class); - REQUIRE(test_class_symbol.type.id()==ID_struct); - const struct_typet::componentt &field_component= + REQUIRE(test_class_symbol.type.id() == ID_struct); + const struct_typet::componentt &field_component = require_type::require_component( - to_struct_type(test_class_symbol.type), - "gf"); - const typet &test_field_type=field_component.type(); + to_struct_type(test_class_symbol.type), "gf"); + const typet &test_field_type = field_component.type(); - REQUIRE(test_field_type.id()==ID_pointer); - REQUIRE(test_field_type.subtype().id()==ID_symbol); - const symbol_typet test_field_array= + REQUIRE(test_field_type.id() == ID_pointer); + REQUIRE(test_field_type.subtype().id() == ID_symbol); + const symbol_typet test_field_array = to_symbol_type(test_field_type.subtype()); - REQUIRE(test_field_array.get_identifier()=="java::array[reference]"); - const pointer_typet &element_type= - require_type::require_pointer( - java_array_element_type(test_field_array), - symbol_typet("java::java.lang.Float")); + REQUIRE(test_field_array.get_identifier() == "java::array[reference]"); + const pointer_typet &element_type = require_type::require_pointer( + java_array_element_type(test_field_array), + symbol_typet("java::java.lang.Float")); // check for other specialized classes, in particular different symbol ids // for arrays with different element types @@ -270,3 +262,136 @@ SCENARIO( } } } + +SCENARIO( + "generate_java_generic_type with a generic array field", + "[core][java_bytecode][generate_java_generic_type]") +{ + const irep_idt harness_class = "java::generic_field_array_instantiation"; + GIVEN("A generic class with a field of type T []") + { + symbol_tablet new_symbol_table = load_java_class( + "generic_field_array_instantiation", + "./java_bytecode/generate_concrete_generic_type"); + + const irep_idt inner_class = "genericArray"; + + WHEN("We specialise that class from a reference to it") + { + 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) + + ""; + REQUIRE(new_symbol_table.has_symbol(specialised_class_name)); + + const symbolt test_class_symbol = + new_symbol_table.lookup_ref(specialised_class_name); + + REQUIRE(test_class_symbol.type.id() == ID_struct); + THEN("The array field should be specialised to be an array of floats") + { + const struct_typet::componentt &field_component = + require_type::require_component( + to_struct_type(test_class_symbol.type), "arrayField"); + + const pointer_typet &component_pointer_type = + require_type::require_pointer(field_component.type(), {}); + + const symbol_typet &pointer_subtype = require_type::require_symbol( + component_pointer_type.subtype(), "java::array[reference]"); + + const typet &array_type = java_array_element_type(pointer_subtype); + + require_type::require_pointer( + array_type, symbol_typet("java::java.lang.Float")); + } + + THEN( + "The generic class field should be specialised to be a generic " + "class with the appropriate type") + { + const struct_typet::componentt &field_component = + require_type::require_component( + to_struct_type(test_class_symbol.type), "genericClassField"); + + require_type::require_java_generic_type( + field_component.type(), + {{require_type::type_parameter_kindt::Inst, + "java::java.lang.Float"}}); + } + } + } + WHEN( + "We specialise the class with an array we should have appropriate types") + { + 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; + + REQUIRE(new_symbol_table.has_symbol(specialised_class_name)); + + const symbolt test_class_symbol = + new_symbol_table.lookup_ref(specialised_class_name); + + REQUIRE(test_class_symbol.type.id() == ID_struct); + THEN("The array field should be specialised to be an array of floats") + { + const struct_typet::componentt &field_component = + require_type::require_component( + to_struct_type(test_class_symbol.type), "arrayField"); + + const pointer_typet &component_pointer_type = + require_type::require_pointer(field_component.type(), {}); + + const symbol_typet &pointer_subtype = require_type::require_symbol( + component_pointer_type.subtype(), "java::array[reference]"); + + const typet &array_type = java_array_element_type(pointer_subtype); + + require_type::require_pointer( + array_type, symbol_typet("java::array[reference]")); + + const typet &array_subtype = + java_array_element_type(to_symbol_type(array_type.subtype())); + + require_type::require_pointer( + array_subtype, symbol_typet("java::java.lang.Float")); + } + + THEN( + "The generic class field should be specialised to be a generic " + "class with the appropriate type") + { + const struct_typet::componentt &field_component = + require_type::require_component( + to_struct_type(test_class_symbol.type), "genericClassField"); + + const java_generic_typet ¶m_type = + require_type::require_java_generic_type( + field_component.type(), + {{require_type::type_parameter_kindt::Inst, + "java::array[reference]"}}); + + const typet &array_type = java_array_element_type( + to_symbol_type(param_type.generic_type_variables()[0].subtype())); + require_type::require_pointer( + array_type, symbol_typet("java::java.lang.Float")); + } + } + } + } +} diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$generic.class b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$generic.class index b7056a5e522..694991b2962 100644 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$generic.class and b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$generic.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$genericArray.class b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$genericArray.class new file mode 100644 index 00000000000..184f8383980 Binary files /dev/null and b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$genericArray.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.class b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.class index 409016e9bf3..45f98be34c7 100644 Binary files a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.class and b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.class differ diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.java b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.java index 524c0108b09..c24758d2ef0 100644 --- a/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.java +++ b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.java @@ -4,9 +4,18 @@ class generic { T gf; } + class genericArray { + T [] arrayField; + + generic genericClassField; + } + generic f; generic g; generic h; generic i; Float [] af; + + genericArray genericArrayField; + genericArray genericArrayArrayField; } diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp index 8e0111869c9..c79b6f4f87b 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_bounded_generic_inner_classes.cpp @@ -32,7 +32,7 @@ SCENARIO( THEN("The symbol type should be generic") { const symbolt &class_symbol = new_symbol_table.lookup_ref(inner_name); - const java_generics_class_typet &java_generics_class_type = + const java_generic_class_typet &java_generic_class_type = require_type::require_java_generic_class( class_symbol.type, {inner_name + "::E"}); @@ -56,7 +56,7 @@ SCENARIO( { const symbolt &class_symbol = new_symbol_table.lookup_ref(boundedinner_name); - const java_generics_class_typet &java_generics_class_type = + const java_generic_class_typet &java_generic_class_type = require_type::require_java_generic_class( class_symbol.type, {boundedinner_name + "::NUM"}); @@ -96,7 +96,7 @@ SCENARIO( const symbolt &class_symbol = new_symbol_table.lookup_ref(doubleboundedinner_name); // TODO the symbol should be generic - TG-1349 - // const java_generics_class_typet &java_generics_class_type = + // const java_generic_class_typet &java_generic_class_type = // require_type::require_java_generic_class( // class_symbol.type, {doubleboundedinner_name + "::T"}); @@ -125,7 +125,7 @@ SCENARIO( { const symbolt &class_symbol = new_symbol_table.lookup_ref(twoelementinner_name); - const java_generics_class_typet &java_generics_class_type = + const java_generic_class_typet &java_generic_class_type = require_type::require_java_generic_class( class_symbol.type, {twoelementinner_name + "::K", twoelementinner_name + "::V"}); diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp index 2c4b698879d..1f83a68d6f7 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp @@ -44,7 +44,7 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(class_prefix)); const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); - const java_generics_class_typet &derived_class_type = + const java_generic_class_typet &derived_class_type = require_type::require_java_generic_class( derived_symbol.type, {class_prefix + "::T"}); diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp index ac054de5e5e..5d35cd08131 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_array_class.cpp @@ -21,7 +21,7 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(class_prefix)); const symbolt &class_symbol = new_symbol_table.lookup_ref(class_prefix); - const java_generics_class_typet &java_generic_class = + const java_generic_class_typet &java_generic_class = require_type::require_java_generic_class( class_symbol.type, {class_prefix + "::T"}); diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp index 3487a4e4e3e..46103893048 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class.cpp @@ -26,7 +26,7 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(class_prefix)); const symbolt &class_symbol = new_symbol_table.lookup_ref(class_prefix); - const java_generics_class_typet &java_generics_class = + const java_generic_class_typet &java_generic_class = require_type::require_java_generic_class( class_symbol.type, {class_prefix + "::T"}); @@ -79,7 +79,7 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(class_prefix)); const symbolt &class_symbol = new_symbol_table.lookup_ref(class_prefix); - const java_generics_class_typet &java_generics_class = + const java_generic_class_typet &java_generic_class = require_type::require_java_generic_class( class_symbol.type, {class_prefix + "::T", class_prefix + "::U"}); diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp index 47bbcd2c2e9..b04b5dfbd83 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_generic_inner_classes.cpp @@ -25,7 +25,7 @@ SCENARIO( { REQUIRE(new_symbol_table.has_symbol(class_prefix)); const symbolt &class_symbol = new_symbol_table.lookup_ref(class_prefix); - const java_generics_class_typet &java_generic_class = + const java_generic_class_typet &java_generic_class = require_type::require_java_generic_class( class_symbol.type, {class_prefix + "::T"}); diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp index d1108be3952..21b2be51eee 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_fields.cpp @@ -26,7 +26,7 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(class_prefix)); const symbolt &class_symbol = new_symbol_table.lookup_ref(class_prefix); - const java_generics_class_typet &java_generics_class_type = + const java_generic_class_typet &java_generic_class_type = require_type::require_java_generic_class( class_symbol.type, {class_prefix + "::T", class_prefix + "::S"}); diff --git a/unit/testing-utils/generic_utils.cpp b/unit/testing-utils/generic_utils.cpp index 57c9cc20145..c0582378ef6 100644 --- a/unit/testing-utils/generic_utils.cpp +++ b/unit/testing-utils/generic_utils.cpp @@ -8,6 +8,7 @@ #include #include +#include #include "generic_utils.h" #include "catch.hpp" #include "require_type.h" @@ -29,6 +30,10 @@ void generic_utils::specialise_generic( example_type.generic_type_variables().end(), is_java_generic_inst_parameter)); + namespacet ns(new_symbol_table); + const typet &class_type = ns.follow(example_type.subtype()); + REQUIRE(is_java_generic_class_type(class_type)); + // Generate the specialised version. ui_message_handlert message_handler; generate_java_generic_typet instantiate_generic_type(message_handler); diff --git a/unit/testing-utils/require_type.cpp b/unit/testing-utils/require_type.cpp index 78b51b53762..8c338d29629 100644 --- a/unit/testing-utils/require_type.cpp +++ b/unit/testing-utils/require_type.cpp @@ -234,15 +234,15 @@ class_typet require_complete_class(const typet &class_type) /// Verify that a class is a complete, valid java generic class. /// \param class_type: the class /// \return: A reference to the java generic class type. -java_generics_class_typet +java_generic_class_typet require_type::require_java_generic_class(const typet &class_type) { const class_typet &class_class_type = require_complete_class(class_type); java_class_typet java_class_type = to_java_class_type(class_class_type); - REQUIRE(is_java_generics_class_type(java_class_type)); - java_generics_class_typet java_generic_class_type = - to_java_generics_class_type(java_class_type); + REQUIRE(is_java_generic_class_type(java_class_type)); + java_generic_class_typet java_generic_class_type = + to_java_generic_class_type(java_class_type); return java_generic_class_type; } @@ -252,14 +252,14 @@ require_type::require_java_generic_class(const typet &class_type) /// \param class_type: the class /// \param type_variables: vector of type variables /// \return: A reference to the java generic class type. -java_generics_class_typet require_type::require_java_generic_class( +java_generic_class_typet require_type::require_java_generic_class( const typet &class_type, const std::initializer_list &type_variables) { - const java_generics_class_typet java_generic_class_type = + const java_generic_class_typet java_generic_class_type = require_type::require_java_generic_class(class_type); - const java_generics_class_typet::generic_typest &generic_type_vars = + const java_generic_class_typet::generic_typest &generic_type_vars = java_generic_class_type.generic_types(); REQUIRE(generic_type_vars.size() == type_variables.size()); REQUIRE( @@ -285,7 +285,23 @@ require_type::require_java_non_generic_class(const typet &class_type) const class_typet &class_class_type = require_complete_class(class_type); java_class_typet java_class_type = to_java_class_type(class_class_type); - REQUIRE(!is_java_generics_class_type(java_class_type)); + REQUIRE(!is_java_generic_class_type(java_class_type)); return java_class_type; } + +/// Verify a given type is a symbol type, optionally with a specific identifier +/// \param type: The type to check +/// \param identifier: The identifier the symbol type should have +/// \return The cast version of the input type +const symbol_typet & +require_type::require_symbol(const typet &type, const irep_idt &identifier) +{ + REQUIRE(type.id() == ID_symbol); + const symbol_typet &result = to_symbol_type(type); + if(identifier != "") + { + REQUIRE(result.get_identifier() == identifier); + } + return result; +} diff --git a/unit/testing-utils/require_type.h b/unit/testing-utils/require_type.h index 6d61f7d325b..d2fb0504077 100644 --- a/unit/testing-utils/require_type.h +++ b/unit/testing-utils/require_type.h @@ -25,6 +25,9 @@ namespace require_type pointer_typet require_pointer(const typet &type, const optionalt &subtype); +const symbol_typet & +require_symbol(const typet &type, const irep_idt &identifier = ""); + struct_typet::componentt require_component( const struct_typet &struct_type, const irep_idt &component_name); @@ -67,9 +70,9 @@ const typet &require_java_non_generic_type( const typet &type, const optionalt &expect_subtype); -java_generics_class_typet require_java_generic_class(const typet &class_type); +java_generic_class_typet require_java_generic_class(const typet &class_type); -java_generics_class_typet require_java_generic_class( +java_generic_class_typet require_java_generic_class( const typet &class_type, const std::initializer_list &type_variables);