From 21a33fa142a658b41c75e1b0f671fc8d78279cb2 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 7 Nov 2017 15:53:25 +0000 Subject: [PATCH 1/7] Renaming to_java_generic_class_type to remove spurious s --- .../generate_java_generic_type.cpp | 4 +- .../java_bytecode_convert_class.cpp | 2 +- src/java_bytecode/java_types.h | 39 +++++++++---------- .../parse_bounded_generic_inner_classes.cpp | 8 ++-- .../parse_derived_generic_class.cpp | 2 +- .../parse_generic_array_class.cpp | 2 +- .../parse_generic_class.cpp | 4 +- ...neric_class_with_generic_inner_classes.cpp | 2 +- .../parse_generic_fields.cpp | 2 +- unit/testing-utils/require_type.cpp | 16 ++++---- unit/testing-utils/require_type.h | 4 +- 11 files changed, 41 insertions(+), 44 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index bcabd9f48d6..7483523cf4d 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -48,8 +48,8 @@ symbolt generate_java_generic_typet::operator()( { if(is_java_generic_parameter(component.type())) { - auto replacement_type_param= - to_java_generics_class_type(replacement_type); + auto replacement_type_param = + to_java_generic_class_type(replacement_type); auto component_identifier= to_java_generic_parameter(component.type()).type_variable() 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/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/require_type.cpp b/unit/testing-utils/require_type.cpp index 78b51b53762..73e546c2e99 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,7 @@ 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; } diff --git a/unit/testing-utils/require_type.h b/unit/testing-utils/require_type.h index 6d61f7d325b..29c2e9d6c9d 100644 --- a/unit/testing-utils/require_type.h +++ b/unit/testing-utils/require_type.h @@ -67,9 +67,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); From f60d8c80b3fcd3a30d6869508cbfbbb6a265fc2c Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 7 Nov 2017 15:56:56 +0000 Subject: [PATCH 2/7] Unit utility for symbol types --- unit/testing-utils/require_type.cpp | 16 ++++++++++++++++ unit/testing-utils/require_type.h | 3 +++ 2 files changed, 19 insertions(+) diff --git a/unit/testing-utils/require_type.cpp b/unit/testing-utils/require_type.cpp index 73e546c2e99..8c338d29629 100644 --- a/unit/testing-utils/require_type.cpp +++ b/unit/testing-utils/require_type.cpp @@ -289,3 +289,19 @@ require_type::require_java_non_generic_class(const typet &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 29c2e9d6c9d..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); From 1ccbf83356bf6a3c6ded95fc3aed884e5c91f6f7 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 7 Nov 2017 14:41:23 +0000 Subject: [PATCH 3/7] Correctly handle generic classes that have a array field Previously we only converted types that were precisely a generic parameter. Now we deal with the case where the array is T type'd. --- .../generate_java_generic_type.cpp | 88 +++++++++++----- .../generate_java_generic_type.h | 5 + .../generate_java_generic_type.cpp | 98 +++++++++++++----- ...ic_field_array_instantiation$generic.class | Bin 550 -> 746 bytes ...eld_array_instantiation$genericArray.class | Bin 0 -> 974 bytes .../generic_field_array_instantiation.class | Bin 823 -> 1050 bytes .../generic_field_array_instantiation.java | 6 ++ 7 files changed, 146 insertions(+), 51 deletions(-) create mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation$genericArray.class diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 7483523cf4d..9dcc6eeb074 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) @@ -43,31 +42,14 @@ symbolt generate_java_generic_typet::operator()( // 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_generic_class_type(replacement_type); + auto replace_type_for_generic_field = + [&](struct_union_typet::componentt &component) { - auto component_identifier= - to_java_generic_parameter(component.type()).type_variable() - .get_identifier(); + component.type() = substitute_type( + component.type(), + to_java_generic_class_type(replacement_type), + existing_generic_type); - optionalt results=java_generics_get_index_for_subtype( - replacement_type_param, component_identifier); - - INVARIANT( - results.has_value(), - "generic component type not found"); - - if(results) - { - component.type()= - existing_generic_type.generic_type_variables()[*results]; - } - } return component; }; @@ -98,6 +80,64 @@ 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"); + + if(results) + { + return generic_reference.generic_type_variables()[*results]; + } + else + { + return parameter_type; + } + } + else if( + parameter_type.id() == ID_pointer && + 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/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..c386f452d8b 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,55 @@ 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); + + THEN("The array field should be specialised to be an array of floats") + { + 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), "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")); + } + } + } + } +} 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 b7056a5e522af6c9b024a55648bbb36504d3e855..694991b296232ba2d5248935750dbf0ebde2a804 100644 GIT binary patch delta 246 zcmZ3+@`_dJ)W2Q(7#J8#7!)`em>DFw7+4sj*coKl8Du9)t&kG($xlwq2}>->Oiap2 z4FM613@jxXnZ=W%7^RuCeI^?+YRXwNGKirntSo>jHUKMOvk3{YwzHmiAd5wgok4!G z9;4pmQpTL(00t%?WMJUZ(%#CzsI{GeX(N!w%)kdE*%%nXYuXD69w{^8Q6g&6HtdZn3iA=0@5J0%nZ^Df(#4*MTIBn delta 124 zcmaFGx{O8Y)W2Q(7#J8#7^FEFm>Gn)7+4sD*%?IH86+l3t(aWMn86~+&LB1UE~DPW zdyYBXw;mqv?g4D0l7)*OIb`tD!=i^Jft(Bid9|;VeC{OXiB5G`-V#_&=URA88y(dJ zD%BzIt4Az+uXn=wCmPzQzy0&J3YxO*Q#0A-{6w->WzphrNE#QTy7KSxJ4s4Ldq{OrVfQ5oHf6 z0voBUS4j#K-p-%E>d-y}+^T)6#Z(4L{0JHT376{=M!?zS&A}-5EIz-;E_$|fo%b_MC4(|0_#bLDyJ znRwkNHnsA7$2YMjFlUDG@u>vwQpjba9WB?g>?Dgrb$&NX6<3xQ5-X6MrvL2Z=r^pu)B zx4A%G1)Z_G2`*PfD3Qzrk0o!1lgW5y7N(n;Ea{H2!X|b;co+zj;iJ0WeNNv@;bPTs z@2VFya3pARX50O!hPw{#ml_oaHo2TamAU1)MsIuGp?5v+(fgk3^Z^c;Tp#?5c}&Hn ef$(Y#S(WV*X2f#*e^=p@R5)V^+(NKHg}@&MEG!`a 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..dd7a88599a7 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,15 @@ class generic { T gf; } + class genericArray { + T [] arrayField; + } + generic f; generic g; generic h; generic i; Float [] af; + + genericArray genericArrayField; } From a01a0f23a4bedba38e9f462e79da096b8fc77cf1 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 7 Nov 2017 18:45:40 +0000 Subject: [PATCH 4/7] Extend the specialisation code to handle generic fields Previously we didn't handle generic fields when we were doing specialisation, meaning they were missed. This resolves this and adds a unit test to demonstrate it. --- .../generate_java_generic_type.cpp | 63 +++++++++++++++---- .../generate_java_generic_type.cpp | 16 ++++- .../generic_field_array_instantiation.java | 2 + 3 files changed, 68 insertions(+), 13 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 9dcc6eeb074..89d6c325dc9 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -117,22 +117,61 @@ typet generate_java_generic_typet::substitute_type( return parameter_type; } } - else if( - parameter_type.id() == ID_pointer && - parameter_type.subtype().id() == ID_symbol) + else if(parameter_type.id() == ID_pointer) { - const symbol_typet &array_subtype = - to_symbol_type(parameter_type.subtype()); - if(is_java_array_tag(array_subtype.get_identifier())) + if(is_java_generic_type(parameter_type)) { - const typet &array_element_type = java_array_element_type(array_subtype); + 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); + 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; + 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; 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 c386f452d8b..f3784993c37 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 @@ -292,9 +292,9 @@ SCENARIO( 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") { - 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), "arrayField"); @@ -310,6 +310,20 @@ SCENARIO( 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"}}); + } } } } 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 dd7a88599a7..9bc4a2a7d28 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 @@ -6,6 +6,8 @@ class generic { class genericArray { T [] arrayField; + + generic genericClassField; } generic f; From 6e06fbdaf9b2be52a2b751e29dcd44c3c539a704 Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 8 Nov 2017 18:26:43 +0000 Subject: [PATCH 5/7] Extending tests to deal with specialising with arrays when array fields --- .../generate_java_generic_type.cpp | 67 ++++++++++++++++++ .../generic_field_array_instantiation.class | Bin 1050 -> 1162 bytes .../generic_field_array_instantiation.java | 1 + 3 files changed, 68 insertions(+) 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 f3784993c37..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 @@ -326,5 +326,72 @@ SCENARIO( } } } + 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.class b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.class index 2e1dfd92d1c5aaf1f04a4ff66eb585d97b37d70d..45f98be34c777a3b916b99272c22f60f203b66c5 100644 GIT binary patch delta 217 zcmW-aI|{;36h!B~`10bXvWU_6N&IV}jg6%sR&KyDXpn%2q{|lULOLr~Afys3T!0&K z7vkj=bMDMAaBtSN=zM;!H-H7kB^c-_^c4mQ!_@I;lrO*J+Q;x5#?gKi$3dd8iNe!? zu-;}fVX8o19JKV<$BU$ enp}g`W>&P9=)mJ7;A?hy15`N|SdzWsYXN^A-XH=1 delta 160 zcmeC;oW&t=>ff$?3=9k=3~F2q%nXX`3`*<_%Ipj(6D1TFRX18bXPn%?w17>5L6VU{ zadIEC;$(N`N=CNH2bm)i7#SEDfD%Ab3TT2pkY)tZtXkU{7&ihLObpUMk_{}#$RGn` j^FS0Z$TG-*<>kSo0#FSDgAh { Float [] af; genericArray genericArrayField; + genericArray genericArrayArrayField; } From ffa104cbebfbff58b84dfde89f04fb241ce1a752 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 9 Nov 2017 13:44:00 +0000 Subject: [PATCH 6/7] Enforce condition that generic references must refer to generic classes We require that all generic references refer to generic classes Also pulled out the conversion out of the loop and gave the variable a more logical name Added check for generic utils function --- .../generate_java_generic_type.cpp | 24 ++++++++++--------- unit/testing-utils/generic_utils.cpp | 5 ++++ 2 files changed, 18 insertions(+), 11 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 89d6c325dc9..2012368f51f 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -32,13 +32,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), + "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 &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 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. @@ -46,9 +50,7 @@ symbolt generate_java_generic_typet::operator()( [&](struct_union_typet::componentt &component) { component.type() = substitute_type( - component.type(), - to_java_generic_class_type(replacement_type), - existing_generic_type); + component.type(), generic_class_definition, existing_generic_type); return component; }; @@ -61,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, 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); From 0f98cb45549b2c2a88bb374290a59a1765e88a13 Mon Sep 17 00:00:00 2001 From: thk123 Date: Thu, 9 Nov 2017 14:33:59 +0000 Subject: [PATCH 7/7] Removed redundant if statement --- src/java_bytecode/generate_java_generic_type.cpp | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 2012368f51f..2b5badb381b 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -109,15 +109,7 @@ typet generate_java_generic_typet::substitute_type( java_generics_get_index_for_subtype(generic_class, component_identifier); INVARIANT(results.has_value(), "generic component type not found"); - - if(results) - { - return generic_reference.generic_type_variables()[*results]; - } - else - { - return parameter_type; - } + return generic_reference.generic_type_variables()[*results]; } else if(parameter_type.id() == ID_pointer) {