From 2f9ee7aef7854adc050f274da1ac24b0c56a840b Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 7 Nov 2017 14:41:23 +0000 Subject: [PATCH 1/7] Temp checkin adding tests for specalising an array --- .../generate_java_generic_type.cpp | 72 ++++++++++++++---- ...ic_field_array_instantiation$generic.class | Bin 550 -> 746 bytes .../generic_field_array_instantiation.class | Bin 506 -> 822 bytes .../generic_field_array_instantiation.java | 7 ++ 4 files changed, 65 insertions(+), 14 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..8157ea10e0b 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 @@ -17,6 +17,7 @@ #include #include #include +#include /// Helper function to specalise a generic class from a named component of a /// named class @@ -179,27 +180,27 @@ 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= + 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. - const irep_idt test_class= + const irep_idt test_class = "java::generic_field_array_instantiation$generic"; GIVEN("A generic type instantiated with an array type") { - symbol_tablet new_symbol_table= + 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= + const symbolt &harness_symbol = new_symbol_table.lookup_ref(harness_class); - const struct_typet::componentt &harness_component= + const struct_typet::componentt &harness_component = require_type::require_component( to_struct_type(harness_symbol.type), "f"); @@ -211,24 +212,67 @@ SCENARIO( // Test the specialized class REQUIRE(new_symbol_table.has_symbol(test_class)); - const symbolt test_class_symbol= + 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(); + 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(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")); + + GIVEN("Specialising a generic class with an array field") + { + const irep_idt &inner_class = "genericArray"; + + specialise_generic_from_component( + harness_class, "genericArrayField", new_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); + const struct_typet::componentt &field_component= + require_type::require_component( + to_struct_type(test_class_symbol.type), + "arrayField"); + const typet &test_field_type=field_component.type(); + + std::cout << test_field_type.pretty() << std::endl; + + std::cout << "Hello world" << std::endl; + } + } } +// +//SCENARIO("Specialising a generic class with a generic field ") +//{ +// const irep_idt harness_class = +// "java::generic_field_array_instantiation"; +// GIVEN("A generic type with a generic array field") +// { +// symbol_tablet new_symbol_table= +// load_java_class( +// "generic_field_array_instantiation", +// "./java_bytecode/generate_concrete_generic_type"); +// +// +// } +//} 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 zdy8kg_dO_L6cP{K5+V`^2tf~#Ts(x%q!T-gJuov7{47s`2S31% z5^IKW0fodvy{=bVS9SH<`^zhUGwh`i!={NX6WbxxIFmzrtQ7M>?P z6T1X63LwysaMF%wZ>Xd_=!qb$r?lq_?JMCcM;}BHHA1SRMq2n2R}#)=&#d3J$KpX$ zZJ|fimhA|?*5GP};06l6eT4kaAzDFWgwxsY3uosGn*U6x|Ji1;uC($SgxFEJONcj} z0gs<;D=n`k_kHQ!h`!C1Lff%~-4(71cw~(GcgiE|Pw#~LO?RA$Ysr=h${kK!OeJ{K z3<@X`N>if=x$h-h_s7!m36-g7pWBcAQ+ehDlwk1RL?|hwL6~P|Aj7zTMMfZt+?PGi z8owfnj7#jRh8##7KZBmwU|^Xs$!4&uFlItMfmN)9{`C+yI0jtEK%6DPy2U{tJ delta 195 zcmW-ZO%B0u5J%s%+CNq5+scBKvK3)%B~Bqy(xmA^Ptx=x-H=!~fCD&;g&5tunfIHI zoBOdhukYgttQdRP^bG^U&@d9rB}$`fd=mV9s@*O*W?7U8au$|FDYHDuibUqcTh?}q zb`e-x3G+i3GsV(xD8W!iXjJAYoA^q7gWf0uwMpgREbd5IjXO$L { T gf; } + class genericArray { + T [] arrayField; + } + generic f; + Float [] af; + + genericArray genericArrayField; } From f1098dc5dfb8956c002266f8a68e422eab3df7e1 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 7 Nov 2017 15:53:25 +0000 Subject: [PATCH 2/7] Renaming to_java_generic_class_type to remove spurious s --- src/java_bytecode/generate_java_generic_type.cpp | 2 +- src/java_bytecode/java_types.h | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index d5747657ee6..057f1a3f811 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -49,7 +49,7 @@ symbolt generate_java_generic_typet::operator()( if(is_java_generic_parameter(component.type())) { auto replacement_type_param= - to_java_generics_class_type(replacement_type); + 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_types.h b/src/java_bytecode/java_types.h index 740d347feb7..d00cc93e51d 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -284,7 +284,7 @@ inline bool is_java_generics_class_type(const typet &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( +inline const java_generics_class_typet &to_java_generic_class_type( const java_class_typet &type) { PRECONDITION(is_java_generics_class_type(type)); @@ -340,7 +340,7 @@ inline const typet &java_generics_class_type_bound( { PRECONDITION(is_java_generics_class_type(t)); const java_generics_class_typet &type= - to_java_generics_class_type(to_java_class_type(t)); + to_java_generic_class_type(to_java_class_type(t)); const std::vector &gen_types=type.generic_types(); PRECONDITION(index Date: Tue, 7 Nov 2017 15:56:56 +0000 Subject: [PATCH 3/7] Unit utility for symbol types --- unit/testing-utils/require_type.cpp | 17 +++++++++++++++++ unit/testing-utils/require_type.h | 3 +++ 2 files changed, 20 insertions(+) diff --git a/unit/testing-utils/require_type.cpp b/unit/testing-utils/require_type.cpp index 78b51b53762..472ae2f74ad 100644 --- a/unit/testing-utils/require_type.cpp +++ b/unit/testing-utils/require_type.cpp @@ -289,3 +289,20 @@ 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 6d61f7d325b..e25cd6b86d4 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 b0c4cfa81021dcfcc404c5ad6515c031ef4a8913 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 7 Nov 2017 17:19:14 +0000 Subject: [PATCH 4/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 | 93 +++++++++++++------ .../generate_java_generic_type.h | 5 + .../generate_java_generic_type.cpp | 84 +++++++++-------- 3 files changed, 117 insertions(+), 65 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 057f1a3f811..fc82d0a40da 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 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); - - INVARIANT( - results.has_value(), - "generic component type not found"); - - if(results) - { - component.type()= - existing_generic_type.generic_type_variables()[*results]; - } - } + auto replace_type_for_generic_field = + [&](struct_union_typet::componentt &component) { + + component.type() = substitute_type( + component.type(), + to_java_generic_class_type(replacement_type), + existing_generic_type); + return component; }; @@ -98,6 +80,65 @@ 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_generics_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..397dba9b368 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_generics_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 8157ea10e0b..2ccd2e0af58 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 @@ -17,7 +17,6 @@ #include #include #include -#include /// Helper function to specalise a generic class from a named component of a /// named class @@ -231,48 +230,55 @@ SCENARIO( require_type::require_pointer( java_array_element_type(test_field_array), symbol_typet("java::java.lang.Float")); + } +} - GIVEN("Specialising a generic class with an array field") - { - const irep_idt &inner_class = "genericArray"; +SCENARIO("generate_java_generic_type with a generic array field") +{ + 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); - - 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); - const struct_typet::componentt &field_component= - require_type::require_component( - to_struct_type(test_class_symbol.type), - "arrayField"); - const typet &test_field_type=field_component.type(); - - std::cout << test_field_type.pretty() << std::endl; - - std::cout << "Hello world" << std::endl; + 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")); + } + } } - } } -// -//SCENARIO("Specialising a generic class with a generic field ") -//{ -// const irep_idt harness_class = -// "java::generic_field_array_instantiation"; -// GIVEN("A generic type with a generic array field") -// { -// symbol_tablet new_symbol_table= -// load_java_class( -// "generic_field_array_instantiation", -// "./java_bytecode/generate_concrete_generic_type"); -// -// -// } -//} From 3d37cb535a3004ae993b9b4b11077a6ebeba01b9 Mon Sep 17 00:00:00 2001 From: thk123 Date: Tue, 7 Nov 2017 18:45:40 +0000 Subject: [PATCH 5/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 | 67 +++++++++++++++---- .../generate_java_generic_type.cpp | 15 ++++- .../generic_field_array_instantiation.java | 2 + 3 files changed, 69 insertions(+), 15 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index fc82d0a40da..736e2fe3de2 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -118,22 +118,61 @@ typet generate_java_generic_typet::substitute_type( } } else if( - parameter_type.id() == ID_pointer && - parameter_type.subtype().id() == ID_symbol) + 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 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; + 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; 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 2ccd2e0af58..3190a7599fe 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 @@ -260,9 +260,9 @@ SCENARIO("generate_java_generic_type with a generic array field") 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"); @@ -278,6 +278,19 @@ SCENARIO("generate_java_generic_type with a generic array field") 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 65cdebfeab1..1f2a28da5a1 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 2cedb22d4b5aba6e7fceca2cee31ac258e06057d Mon Sep 17 00:00:00 2001 From: thk123 Date: Wed, 8 Nov 2017 12:52:46 +0000 Subject: [PATCH 6/7] Hacked version of generate_java_generic_type --- .../generate_java_generic_type.cpp | 44 ++++++++++++++++--- 1 file changed, 38 insertions(+), 6 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 736e2fe3de2..482eab55062 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -69,12 +69,44 @@ symbolt generate_java_generic_typet::operator()( "All components in the original class should be in the new class"); const auto expected_symbol="java::"+id2string(new_tag); - - generate_class_stub( - new_tag, - symbol_table, - message_handler, - replacement_components); +// +// generate_class_stub( +// new_tag, +// symbol_table, +// message_handler, +// replacement_components); + + // inlined the generate_class_stub for now + { + java_class_typet specialised_class; + specialised_class.set_tag(replacement_type.get_tag()); + specialised_class.set(ID_base_name, new_tag); + + // produce class symbol + symbolt new_symbol; + new_symbol.base_name = new_tag; + new_symbol.pretty_name = new_tag; + new_symbol.name = "java::" + id2string(new_tag); + specialised_class.set(ID_name, new_symbol.name); + new_symbol.type = specialised_class; + new_symbol.mode = ID_java; + new_symbol.is_type = true; + + std::pair res = symbol_table.insert(std::move(new_symbol)); + + if(! res.second) + { + messaget message(message_handler); + message.warning() << + "stub class symbol " << + new_symbol.name << + " already exists" << messaget::eom; + } + else + { + java_add_components_to_class(res.first, replacement_components); + } + } auto symbol=symbol_table.lookup(expected_symbol); INVARIANT(symbol, "New class not created"); return *symbol; From b481bea9c57b45581745953d18d23090a25ed72c Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Fri, 10 Nov 2017 13:48:06 +0000 Subject: [PATCH 7/7] Added the specialised java generic class type. --- .../generate_java_generic_type.cpp | 11 ++++---- src/java_bytecode/java_types.h | 25 +++++++++++++++++++ src/util/irep_ids.def | 1 + 3 files changed, 31 insertions(+), 6 deletions(-) diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index 482eab55062..3f13ef974ce 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -78,8 +78,9 @@ symbolt generate_java_generic_typet::operator()( // inlined the generate_class_stub for now { - java_class_typet specialised_class; + java_specialised_generic_class_typet specialised_class; specialised_class.set_tag(replacement_type.get_tag()); + // NOTE: the tag absolutely has to be BasicGeneric specialised_class.set(ID_base_name, new_tag); // produce class symbol @@ -94,13 +95,11 @@ symbolt generate_java_generic_typet::operator()( std::pair res = symbol_table.insert(std::move(new_symbol)); - if(! res.second) + if(!res.second) { messaget message(message_handler); - message.warning() << - "stub class symbol " << - new_symbol.name << - " already exists" << messaget::eom; + message.warning() << "stub class symbol " << new_symbol.name + << " already exists" << messaget::eom; } else { diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index d00cc93e51d..e4ec1ad791a 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -403,4 +403,29 @@ inline const optionalt java_generics_get_index_for_subtype( return std::distance(gen_types.cbegin(), iter); } +class java_specialised_generic_class_typet : public java_class_typet +{ + // note the constryctor could take the components and construct it itself + // note vector of generic parameter of symbol type +public: + // TODO: to be defined more appropriately. + java_specialised_generic_class_typet() + { + set(ID_C_specialised_generic_java_class, true); + } +}; + +inline const bool java_is_specialised_generic_class_type(const typet &type) +{ + return type.get_bool(ID_C_specialised_generic_java_class); +} + +inline java_specialised_generic_class_typet + to_java_specialised_class_typet(const typet &type) +{ + INVARIANT(java_is_specialised_generic_class_type(type), + "Tried to convert a type that was not a specialised generic java class"); + return static_cast(type); +} + #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 005124d0ea7..7b43b224177 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -833,6 +833,7 @@ IREP_ID_TWO(C_java_generic_type, #java_generic_type) IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type) IREP_ID_TWO(generic_types, #generic_types) IREP_ID_TWO(type_variables, #type_variables) +IREP_ID_TWO(C_specialised_generic_java_class, #specialised_class) IREP_ID_ONE(havoc_object) IREP_ID_TWO(overflow_shl, overflow-shl)