From ef6b4af31296d2f74aa8fc4688bed7de537277af Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Tue, 7 Nov 2017 15:06:28 +0100 Subject: [PATCH 1/2] Post-fix arrays as generic types with their element type --- .../generate_java_generic_type.cpp | 19 ++++++++++++++++++- src/java_bytecode/java_utils.cpp | 6 ++---- 2 files changed, 20 insertions(+), 5 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index d5747657ee6..bcabd9f48d6 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -119,7 +119,24 @@ irep_idt generate_java_generic_typet::build_generic_tag( INVARIANT( is_java_generic_inst_parameter(param), "Only create full concretized generic types"); - new_tag_buffer << param.subtype().get(ID_identifier); + const irep_idt &id(id2string(param.subtype().get(ID_identifier))); + new_tag_buffer << id2string(id); + if(is_java_array_tag(id)) + { + const typet &element_type = + java_array_element_type(to_symbol_type(param.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()); + } + } } new_tag_buffer << ">"; diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index 8184394e3b5..e244247ca42 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -21,11 +21,9 @@ Author: Daniel Kroening, kroening@kroening.com bool java_is_array_type(const typet &type) { - if(type.id()!=ID_struct) + if(type.id() != ID_struct) return false; - return has_prefix(id2string( - to_struct_type(type).get_tag()), - "java::array["); + return is_java_array_tag(to_struct_type(type).get_tag()); } unsigned java_local_variable_slots(const typet &t) From 5be97db6ab0cb464736cb7211cff884c033d9af9 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matthias=20G=C3=BCdemann?= Date: Wed, 8 Nov 2017 10:38:56 +0100 Subject: [PATCH 2/2] Create new and adapt existing unit tests for generic array param --- .../generate_java_generic_type.cpp | 42 +++++++++++++++++- .../generic_field_array_instantiation.class | Bin 506 -> 823 bytes .../generic_field_array_instantiation.java | 5 ++- 3 files changed, 43 insertions(+), 4 deletions(-) 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 40ada0c6cf7..2c746a37c83 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 @@ -184,8 +184,9 @@ SCENARIO( // We want to test that the specialized/instantiated class has it's field // type updated, so find the specialized class, not the generic class. - const irep_idt test_class= - "java::generic_field_array_instantiation$generic"; + const irep_idt test_class = + "java::generic_field_array_instantiation$generic"; GIVEN("A generic type instantiated with an array type") { @@ -230,5 +231,42 @@ SCENARIO( 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 + GIVEN("A generic type instantiated with different array types") + { + const irep_idt test_class_integer = + "java::generic_field_array_instantiation$generic"; + + const irep_idt test_class_int = + "java::generic_field_array_instantiation$generic"; + + const irep_idt test_class_float = + "java::generic_field_array_instantiation$generic"; + + const struct_typet::componentt &component_g = + require_type::require_component( + to_struct_type(harness_symbol.type), "g"); + instantiate_generic_type( + to_java_generic_type(component_g.type()), new_symbol_table); + REQUIRE(new_symbol_table.has_symbol(test_class_integer)); + + const struct_typet::componentt &component_h = + require_type::require_component( + to_struct_type(harness_symbol.type), "h"); + instantiate_generic_type( + to_java_generic_type(component_h.type()), new_symbol_table); + REQUIRE(new_symbol_table.has_symbol(test_class_int)); + + const struct_typet::componentt &component_i = + require_type::require_component( + to_struct_type(harness_symbol.type), "i"); + instantiate_generic_type( + to_java_generic_type(component_i.type()), new_symbol_table); + REQUIRE(new_symbol_table.has_symbol(test_class_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 67141fda96ad3efeb8fc30b66662b11e256317a7..409016e9bf3decfe12fb3814ea6bde2be57119ce 100644 GIT binary patch delta 306 zcmeyxyq!(r)W2Q(7#J8#805Jam>Hzm8D!WQWZ4E&Q$$E@Ascb-}u`_TmFfwogSxgLEK$07Y&jaN1BJufve10Up z0FW<;#1{hcg&9PEB+w5GKwE&M_~iYJVyY5AF*YC%B*VlY38a}Aq<|s}Ksy;3Sb#iM G1_l5;(KHH+3#t8}AwTrk XV|XvcAp0M6R@%;54k|H5QaStp3EB { } generic f; + generic g; + generic h; + generic i; Float [] af; } - -