diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index d5747657ee6..3f13ef974ce 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_generics_class_type(replacement_type); - - auto component_identifier= - to_java_generic_parameter(component.type()).type_variable() - .get_identifier(); + auto replace_type_for_generic_field = + [&](struct_union_typet::componentt &component) { - optionalt results=java_generics_get_index_for_subtype( - replacement_type_param, component_identifier); + component.type() = substitute_type( + component.type(), + to_java_generic_class_type(replacement_type), + existing_generic_type); - INVARIANT( - results.has_value(), - "generic component type not found"); - - if(results) - { - component.type()= - existing_generic_type.generic_type_variables()[*results]; - } - } return component; }; @@ -87,17 +69,146 @@ 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_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 + 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; } +/// 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) + { + 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..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/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 740d347feb7..e4ec1ad791a 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 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) 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..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 @@ -179,27 +179,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 +211,87 @@ 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")); } } + +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); + 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"}}); + } + + } + } + } +} 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.class b/unit/java_bytecode/generate_concrete_generic_type/generic_field_array_instantiation.class index 67141fda96a..094157ad89d 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 c5266feeedb..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 @@ -4,8 +4,17 @@ class generic { T gf; } + class genericArray { + T [] arrayField; + + generic genericClassField; + } + generic f; + Float [] af; + + genericArray genericArrayField; } 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);