From b005f024294cde55c31904ae397e795c8082185b Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 24 Jul 2019 14:37:26 +0100 Subject: [PATCH 01/19] Indent TODO continuation lines --- jbmc/src/java_bytecode/java_bytecode_convert_class.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index c6387db44e9..8a5f2cd03ee 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -1141,7 +1141,7 @@ void mark_java_implicitly_generic_class_type( // the class must be an inner non-static class, i.e., have a field this$* // TODO this should be simplified once static inner classes are marked - // during parsing + // during parsing bool no_this_field = std::none_of( class_type.components().begin(), class_type.components().end(), From fed9fd8ef5456c59f6ccb5d1dd518f7a09cddade Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 24 Jul 2019 14:24:01 +0100 Subject: [PATCH 02/19] Remove prefix underscore --- .../generic_parameter_specialization_map_keys.h | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h index b736e71beac..691c07f2f38 100644 --- a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h +++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h @@ -18,12 +18,10 @@ class generic_parameter_specialization_map_keyst public: /// Initialize a generic-parameter-specialization-map entry owner operating /// on a given map. Initially it does not own any map entry. - /// \param _generic_parameter_specialization_map: map to operate on. + /// \param generic_parameter_specialization_map: map to operate on. explicit generic_parameter_specialization_map_keyst( - generic_parameter_specialization_mapt - &_generic_parameter_specialization_map) - : generic_parameter_specialization_map( - _generic_parameter_specialization_map) + generic_parameter_specialization_mapt &generic_parameter_specialization_map) + : generic_parameter_specialization_map(generic_parameter_specialization_map) { } From bbf403ed4733bd90b9215fe50a6c7bbad73ef615 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 24 Jul 2019 13:52:28 +0100 Subject: [PATCH 03/19] Remove const modifier that doesn't do anything --- jbmc/unit/java-testing-utils/require_type.cpp | 2 +- jbmc/unit/java-testing-utils/require_type.h | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp index 019a73efcb1..7b6a8847b53 100644 --- a/jbmc/unit/java-testing-utils/require_type.cpp +++ b/jbmc/unit/java-testing-utils/require_type.cpp @@ -477,7 +477,7 @@ require_type::require_struct_tag(const typet &type, const irep_idt &identifier) return result; } -const pointer_typet +pointer_typet require_type::require_pointer_to_tag(const typet &type, const irep_idt &tag) { const auto pointer_type = require_type::require_pointer(type, {}); diff --git a/jbmc/unit/java-testing-utils/require_type.h b/jbmc/unit/java-testing-utils/require_type.h index d0d8912453f..d24b1274e42 100644 --- a/jbmc/unit/java-testing-utils/require_type.h +++ b/jbmc/unit/java-testing-utils/require_type.h @@ -28,7 +28,7 @@ require_pointer(const typet &type, const optionalt &subtype); const struct_tag_typet & require_struct_tag(const typet &type, const irep_idt &identifier = ""); -const pointer_typet require_pointer_to_tag( +pointer_typet require_pointer_to_tag( const typet &type, const irep_idt &identifier = irep_idt()); From a483c86884f200c3112634058e6226ce72d5a767 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 24 Jul 2019 13:52:03 +0100 Subject: [PATCH 04/19] Remove duplicated brackets --- jbmc/unit/java-testing-utils/require_type.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp index 7b6a8847b53..536101e5bad 100644 --- a/jbmc/unit/java-testing-utils/require_type.cpp +++ b/jbmc/unit/java-testing-utils/require_type.cpp @@ -147,7 +147,7 @@ bool require_java_generic_type_argument_expectation( { case require_type::type_argument_kindt::Var: { - REQUIRE(is_java_generic_parameter((type_argument))); + REQUIRE(is_java_generic_parameter(type_argument)); java_generic_parametert parameter = to_java_generic_parameter(type_argument); REQUIRE(parameter.type_variable().get_identifier() == expected.description); From 7aa6d2309e8fd5f6fc78c43114419b4e19b6c3fb Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 24 Jul 2019 18:37:52 +0100 Subject: [PATCH 05/19] Spacing Add space between pre-checks and action Remove space between abbreviations and their usage --- .../java_bytecode/generic_parameter_specialization_map_keys.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp index 6cd20b1508b..c845c3cde9a 100644 --- a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp +++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp @@ -151,6 +151,7 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol( { return; } + const java_generic_struct_tag_typet &generic_symbol = to_java_generic_struct_tag_type(struct_tag_type); @@ -158,7 +159,6 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol( get_all_generic_parameters(symbol_struct); const java_generic_typet::generic_type_argumentst &type_args = generic_symbol.generic_types(); - INVARIANT( type_args.size() == generic_parameters.size(), "All generic parameters of the superclass need to be concretized"); From 871994ed77a4c9f9007c7c73ef9a46febb8404ab Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Thu, 25 Jul 2019 15:53:29 +0100 Subject: [PATCH 06/19] Fix indentation --- .../java_bytecode_parse_generics/DerivedGenerics.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenerics.java b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenerics.java index 14aa3ecef53..bf899408f29 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenerics.java +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenerics.java @@ -15,9 +15,9 @@ public class DerivedGenerics { ExtendsAndImplementsSameInterface new14; ExtendsAndImplementsSameInterface2 new15; ExtendsAndImplementsSameInterfaceGeneric new16; - GenericBase.ExtendImplicit new17; - GenericBase.ExtendImplicitAndExplicit new18; - GenericBase2.ExtendImplicitAndExplicit new19; + GenericBase.ExtendImplicit new17; + GenericBase.ExtendImplicitAndExplicit new18; + GenericBase2.ExtendImplicitAndExplicit new19; } class DerivedGenericInst extends Generic From 541e667c5f078748fe0772e3d9afeedf962f086b Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 24 Jul 2019 14:36:57 +0100 Subject: [PATCH 07/19] Use std::next to allow variable that isn't changed to be const --- src/util/simplify_expr_int.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp index cd4aed6d928..0f66c76b3df 100644 --- a/src/util/simplify_expr_int.cpp +++ b/src/util/simplify_expr_int.cpp @@ -415,8 +415,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_plus(const plus_exprt &expr) // we only merge neighboring constants! Forall_expr(it, new_operands) { - exprt::operandst::iterator next=it; - next++; + const exprt::operandst::iterator next = std::next(it); if(next != new_operands.end()) { From 1981bddbdd022cc59f0e68e566a7cfcbab7626bf Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 24 Jul 2019 14:37:54 +0100 Subject: [PATCH 08/19] Use faster character version of rfind --- jbmc/src/java_bytecode/java_bytecode_convert_class.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 8a5f2cd03ee..9b4662179f1 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -1158,7 +1158,7 @@ void mark_java_implicitly_generic_class_type( // the order from the outer-most inwards std::vector implicit_generic_type_parameters; std::string::size_type outer_class_delimiter = - qualified_class_name.rfind("$"); + qualified_class_name.rfind('$'); while(outer_class_delimiter != std::string::npos) { std::string outer_class_name = @@ -1178,7 +1178,7 @@ void mark_java_implicitly_generic_class_type( outer_generic_type_parameters.begin(), outer_generic_type_parameters.end()); } - outer_class_delimiter = outer_class_name.rfind("$"); + outer_class_delimiter = outer_class_name.rfind('$'); } else { From fabd8636c9edcc9c8517ee96367a170926bbf6cb Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 24 Jul 2019 14:29:05 +0100 Subject: [PATCH 09/19] Rename replacement_parameter_it --- jbmc/src/java_bytecode/java_bytecode_convert_class.cpp | 9 ++++----- 1 file changed, 4 insertions(+), 5 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 9b4662179f1..6769659d652 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -1012,11 +1012,10 @@ static void find_and_replace_parameter( parameter_full_name.substr(parameter_full_name.rfind("::") + 2); // check if there is a replacement parameter with the same name - const auto replacement_parameter_p = std::find_if( + const auto replacement_parameter_it = std::find_if( replacement_parameters.begin(), replacement_parameters.end(), - [¶meter_name](const java_generic_parametert &replacement_param) - { + [¶meter_name](const java_generic_parametert &replacement_param) { const std::string &replacement_parameter_full_name = id2string(replacement_param.type_variable().get_identifier()); return parameter_name.compare( @@ -1025,10 +1024,10 @@ static void find_and_replace_parameter( }); // if a replacement parameter was found, update the identifier - if(replacement_parameter_p != replacement_parameters.end()) + if(replacement_parameter_it != replacement_parameters.end()) { const std::string &replacement_parameter_full_name = - id2string(replacement_parameter_p->type_variable().get_identifier()); + id2string(replacement_parameter_it->type_variable().get_identifier()); // the replacement parameter is a viable one, i.e., it comes from an outer // class From db37e0f3b18a36137c7f251ed16f45a8b94471b2 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 24 Jul 2019 14:32:34 +0100 Subject: [PATCH 10/19] Use == instead of compare == 0 --- jbmc/src/java_bytecode/java_bytecode_convert_class.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 6769659d652..d530071b5bf 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -1018,9 +1018,9 @@ static void find_and_replace_parameter( [¶meter_name](const java_generic_parametert &replacement_param) { const std::string &replacement_parameter_full_name = id2string(replacement_param.type_variable().get_identifier()); - return parameter_name.compare( - replacement_parameter_full_name.substr( - replacement_parameter_full_name.rfind("::") + 2)) == 0; + return parameter_name == + replacement_parameter_full_name.substr( + replacement_parameter_full_name.rfind("::") + 2); }); // if a replacement parameter was found, update the identifier From 2939616ee70ea3cb83ea52cba6425024636ca6a7 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 24 Jul 2019 14:28:21 +0100 Subject: [PATCH 11/19] Extract get_final_name_component/get_without_final_name_component --- .../java_bytecode_convert_class.cpp | 27 ++++++++++++------- 1 file changed, 17 insertions(+), 10 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index d530071b5bf..368ae4db74f 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -989,6 +989,16 @@ bool java_bytecode_convert_class( return true; } +static std::string get_final_name_component(const std::string &name) +{ + return name.substr(name.rfind("::") + 2); +} + +static std::string get_without_final_name_component(const std::string &name) +{ + return name.substr(0, name.rfind("::")); +} + /// For a given generic type parameter, check if there is a parameter in the /// given vector of replacement parameters with a matching name. If yes, /// replace the identifier of the parameter at hand by the identifier of @@ -1008,19 +1018,17 @@ static void find_and_replace_parameter( // get the name of the parameter, e.g., `T` from `java::Class::T` const std::string ¶meter_full_name = id2string(parameter.type_variable_ref().get_identifier()); - const std::string ¶meter_name = - parameter_full_name.substr(parameter_full_name.rfind("::") + 2); + const std::string parameter_name = + get_final_name_component(parameter_full_name); // check if there is a replacement parameter with the same name const auto replacement_parameter_it = std::find_if( replacement_parameters.begin(), replacement_parameters.end(), [¶meter_name](const java_generic_parametert &replacement_param) { - const std::string &replacement_parameter_full_name = - id2string(replacement_param.type_variable().get_identifier()); return parameter_name == - replacement_parameter_full_name.substr( - replacement_parameter_full_name.rfind("::") + 2); + get_final_name_component( + id2string(replacement_param.type_variable().get_identifier())); }); // if a replacement parameter was found, update the identifier @@ -1032,10 +1040,9 @@ static void find_and_replace_parameter( // the replacement parameter is a viable one, i.e., it comes from an outer // class PRECONDITION( - parameter_full_name.substr(0, parameter_full_name.rfind("::")) - .compare( - replacement_parameter_full_name.substr( - 0, replacement_parameter_full_name.rfind("::"))) > 0); + get_without_final_name_component(parameter_full_name) + .compare(get_without_final_name_component( + replacement_parameter_full_name)) > 0); parameter.type_variable_ref().set_identifier( replacement_parameter_full_name); From b0319b8759f4fdc78e3ebba8909fd75137d37ece Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 24 Jul 2019 14:36:16 +0100 Subject: [PATCH 12/19] Update class type before assigning to class_symbol.type Previously the code relied on the fact that class_type is a reference to class_symbol.type and so after a new type got copied assigned into class_symbol.type, class_type became a reference to the new value. --- .../src/java_bytecode/java_bytecode_convert_class.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index 368ae4db74f..da1ca4add51 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -1142,8 +1142,9 @@ void mark_java_implicitly_generic_class_type( { const std::string qualified_class_name = "java::" + id2string(class_name); PRECONDITION(symbol_table.has_symbol(qualified_class_name)); + // This will have its type changed symbolt &class_symbol = symbol_table.get_writeable_ref(qualified_class_name); - java_class_typet &class_type = to_java_class_type(class_symbol.type); + const java_class_typet &class_type = to_java_class_type(class_symbol.type); // the class must be an inner non-static class, i.e., have a field this$* // TODO this should be simplified once static inner classes are marked @@ -1197,19 +1198,21 @@ void mark_java_implicitly_generic_class_type( // implicitly generic and update identifiers of type parameters used in fields if(!implicit_generic_type_parameters.empty()) { - class_symbol.type = java_implicitly_generic_class_typet( + java_implicitly_generic_class_typet new_class_type( class_type, implicit_generic_type_parameters); - for(auto &field : class_type.components()) + for(auto &field : new_class_type.components()) { find_and_replace_parameters( field.type(), implicit_generic_type_parameters); } - for(auto &base : class_type.bases()) + for(auto &base : new_class_type.bases()) { find_and_replace_parameters( base.type(), implicit_generic_type_parameters); } + + class_symbol.type = new_class_type; } } From a1e35d8df339c35c4a68016f958a1e082a5df26e Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Tue, 16 Jul 2019 19:29:46 +0100 Subject: [PATCH 13/19] Validate config is initialised when a member_offset_expr is constructed This will save time hunting for the cause of problems when unit tests don't initialise the config. --- src/util/pointer_offset_size.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp index 67529f1ec07..bae960a1021 100644 --- a/src/util/pointer_offset_size.cpp +++ b/src/util/pointer_offset_size.cpp @@ -241,6 +241,7 @@ optionalt member_offset_expr( const irep_idt &member, const namespacet &ns) { + PRECONDITION(size_type().get_width() != 0); exprt result=from_integer(0, size_type()); std::size_t bit_field_bits=0; From e513d0242b713734776a73b694b63bc078528d00 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Fri, 19 Jul 2019 18:46:48 +0100 Subject: [PATCH 14/19] Give separate REQUIRE statements for each element in list This will produce better error messages when tests fail. --- jbmc/unit/java-testing-utils/require_type.cpp | 19 +++++++------------ 1 file changed, 7 insertions(+), 12 deletions(-) diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp index 536101e5bad..b29b7790924 100644 --- a/jbmc/unit/java-testing-utils/require_type.cpp +++ b/jbmc/unit/java-testing-utils/require_type.cpp @@ -392,18 +392,13 @@ require_type::require_java_implicitly_generic_class( &implicit_generic_type_vars = java_implicitly_generic_class_type.implicit_generic_types(); REQUIRE(implicit_generic_type_vars.size() == implicit_type_variables.size()); - REQUIRE( - std::equal( - implicit_type_variables.begin(), - implicit_type_variables.end(), - implicit_generic_type_vars.begin(), - []( - const irep_idt &type_var_name, - const java_generic_parametert ¶m) { //NOLINT - REQUIRE(is_java_generic_parameter(param)); - return param.type_variable().get_identifier() == type_var_name; - })); - + auto param = implicit_generic_type_vars.begin(); + auto type_var_name = implicit_type_variables.begin(); + for(; param != implicit_generic_type_vars.end(); ++param, ++type_var_name) + { + REQUIRE(is_java_generic_parameter(*param)); + REQUIRE(param->type_variable().get_identifier() == *type_var_name); + } return java_implicitly_generic_class_type; } From 3ca75107188ff7b155da0b59a339615fd070ff79 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Mon, 15 Jul 2019 11:56:54 +0100 Subject: [PATCH 15/19] Use type_try_dynamic_cast --- jbmc/src/java_bytecode/java_types.h | 12 +++++- .../src/java_bytecode/select_pointer_type.cpp | 38 +++++++++---------- 2 files changed, 30 insertions(+), 20 deletions(-) diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index 024eaeec24c..aaea1be12e0 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -735,13 +735,23 @@ class java_generic_parametert : public reference_typet } }; +/// Check whether a reference to a typet is a Java generic parameter/variable, +/// e.g., `T` in `List`. +/// \param base: Source type. +/// \return True if \p type is a generic Java parameter type +template <> +inline bool can_cast_type(const typet &base) +{ + return is_reference(base) && is_java_generic_parameter_tag(base.subtype()); +} + /// Checks whether the type is a java generic parameter/variable, e.g., `T` in /// `List`. /// \param type: the type to check /// \return true if type is a generic Java parameter type inline bool is_java_generic_parameter(const typet &type) { - return is_reference(type) && is_java_generic_parameter_tag(type.subtype()); + return can_cast_type(type); } /// \param type: source type diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp index a8a615dc2ea..d8ec521eca1 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.cpp +++ b/jbmc/src/java_bytecode/select_pointer_type.cpp @@ -42,11 +42,10 @@ pointer_typet select_pointer_typet::specialize_generics( &generic_parameter_specialization_map, generic_parameter_recursion_trackingt &visited_nodes) const { - if(is_java_generic_parameter(pointer_type)) + auto parameter = type_try_dynamic_cast(pointer_type); + if(parameter != nullptr) { - const java_generic_parametert ¶meter = - to_java_generic_parameter(pointer_type); - const irep_idt ¶meter_name = parameter.get_name(); + const irep_idt ¶meter_name = parameter->get_name(); // avoid infinite recursion by looking at each generic argument from // previous assignments @@ -82,26 +81,27 @@ pointer_typet select_pointer_typet::specialize_generics( visited_nodes.erase(parameter_name); return returned_type; } - else if(pointer_type.subtype().id() == ID_struct_tag) + + auto subtype = + type_try_dynamic_cast(pointer_type.subtype()); + if(subtype != nullptr && is_java_array_tag(subtype->get_identifier())) { // if the pointer is an array, recursively specialize its element type - const auto &array_subtype = to_struct_tag_type(pointer_type.subtype()); - if(is_java_array_tag(array_subtype.get_identifier())) + const auto *array_element_type = + type_try_dynamic_cast(java_array_element_type(*subtype)); + if(array_element_type != nullptr) { - const typet &array_element_type = java_array_element_type(array_subtype); - if(array_element_type.id() == ID_pointer) - { - const pointer_typet &new_array_type = specialize_generics( - to_pointer_type(array_element_type), - generic_parameter_specialization_map, - visited_nodes); - - pointer_typet replacement_array_type = java_array_type('a'); - replacement_array_type.subtype().set(ID_element_type, new_array_type); - return replacement_array_type; - } + const pointer_typet &new_array_type = specialize_generics( + *array_element_type, + generic_parameter_specialization_map, + visited_nodes); + + pointer_typet replacement_array_type = java_array_type('a'); + replacement_array_type.subtype().set(ID_element_type, new_array_type); + return replacement_array_type; } } + return pointer_type; } From 75cbba1a329bf32140dad4138115f884df746351 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 24 Jul 2019 14:31:03 +0100 Subject: [PATCH 16/19] Invert the iterator check to reduce cognitive load caused by extended block scope --- .../java_bytecode_convert_class.cpp | 30 +++++++++---------- .../src/java_bytecode/select_pointer_type.cpp | 20 ++++++------- 2 files changed, 23 insertions(+), 27 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index da1ca4add51..c2c9be8114d 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -1030,23 +1030,21 @@ static void find_and_replace_parameter( get_final_name_component( id2string(replacement_param.type_variable().get_identifier())); }); + if(replacement_parameter_it == replacement_parameters.end()) + return; - // if a replacement parameter was found, update the identifier - if(replacement_parameter_it != replacement_parameters.end()) - { - const std::string &replacement_parameter_full_name = - id2string(replacement_parameter_it->type_variable().get_identifier()); - - // the replacement parameter is a viable one, i.e., it comes from an outer - // class - PRECONDITION( - get_without_final_name_component(parameter_full_name) - .compare(get_without_final_name_component( - replacement_parameter_full_name)) > 0); - - parameter.type_variable_ref().set_identifier( - replacement_parameter_full_name); - } + // A replacement parameter was found, update the identifier + const std::string &replacement_parameter_full_name = + id2string(replacement_parameter_it->type_variable().get_identifier()); + + // the replacement parameter is a viable one, i.e., it comes from an outer + // class + PRECONDITION( + get_without_final_name_component(parameter_full_name) + .compare( + get_without_final_name_component(replacement_parameter_full_name)) > 0); + + parameter.type_variable_ref().set_identifier(replacement_parameter_full_name); } /// Recursively find all generic type parameters of a given type and replace diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp index d8ec521eca1..dc659aaefca 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.cpp +++ b/jbmc/src/java_bytecode/select_pointer_type.cpp @@ -89,17 +89,15 @@ pointer_typet select_pointer_typet::specialize_generics( // if the pointer is an array, recursively specialize its element type const auto *array_element_type = type_try_dynamic_cast(java_array_element_type(*subtype)); - if(array_element_type != nullptr) - { - const pointer_typet &new_array_type = specialize_generics( - *array_element_type, - generic_parameter_specialization_map, - visited_nodes); - - pointer_typet replacement_array_type = java_array_type('a'); - replacement_array_type.subtype().set(ID_element_type, new_array_type); - return replacement_array_type; - } + if(array_element_type == nullptr) + return pointer_type; + + const pointer_typet &new_array_type = specialize_generics( + *array_element_type, generic_parameter_specialization_map, visited_nodes); + + pointer_typet replacement_array_type = java_array_type('a'); + replacement_array_type.subtype().set(ID_element_type, new_array_type); + return replacement_array_type; } return pointer_type; From de5b6e90ea599bb3ac5afec779bcfee3ea4f7180 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Thu, 11 Jul 2019 16:10:45 +0100 Subject: [PATCH 17/19] Change data storage for generic_parameter_specialization_mapt This fixes the problem where we tried to unwind stacks in step that are not related, e.g. when a third generic class refers to two mutually recursive generic classes Instead stacks are created per scope (generic context) and unwound individually Also fixes problem where self-recursion isn't handled properly Add test that would have triggered invariant in get_recursively_instantiated_type --- jbmc/src/java_bytecode/Makefile | 1 + jbmc/src/java_bytecode/README.md | 6 +- .../generic_parameter_specialization_map.cpp | 67 +++++++ .../generic_parameter_specialization_map.h | 141 ++++++++++++++ ...eric_parameter_specialization_map_keys.cpp | 79 +++----- ...eneric_parameter_specialization_map_keys.h | 32 +--- .../src/java_bytecode/java_object_factory.cpp | 6 +- .../src/java_bytecode/select_pointer_type.cpp | 175 +++--------------- jbmc/src/java_bytecode/select_pointer_type.h | 28 ++- .../goto_program_generics/Bar.class | Bin 0 -> 308 bytes .../goto_program_generics/Foo.class | Bin 0 -> 355 bytes .../goto_program_generics/KeyValue.class | Bin 562 -> 473 bytes .../MutuallyRecursiveGenerics.class | Bin 671 -> 637 bytes .../MutuallyRecursiveGenerics.java | 8 + .../goto_program_generics/Outer$Inner.class | Bin 613 -> 466 bytes .../goto_program_generics/Outer.class | Bin 634 -> 514 bytes .../goto_program_generics/Three.class | Bin 597 -> 508 bytes .../mutually_recursive_generics.cpp | 61 ++++++ 18 files changed, 352 insertions(+), 252 deletions(-) create mode 100644 jbmc/src/java_bytecode/generic_parameter_specialization_map.cpp create mode 100644 jbmc/src/java_bytecode/generic_parameter_specialization_map.h create mode 100644 jbmc/unit/java_bytecode/goto_program_generics/Bar.class create mode 100644 jbmc/unit/java_bytecode/goto_program_generics/Foo.class diff --git a/jbmc/src/java_bytecode/Makefile b/jbmc/src/java_bytecode/Makefile index 0cfc14ed5b1..4cfb97b35fd 100644 --- a/jbmc/src/java_bytecode/Makefile +++ b/jbmc/src/java_bytecode/Makefile @@ -5,6 +5,7 @@ SRC = assignments_from_json.cpp \ ci_lazy_methods_needed.cpp \ convert_java_nondet.cpp \ expr2java.cpp \ + generic_parameter_specialization_map.cpp \ generic_parameter_specialization_map_keys.cpp \ jar_file.cpp \ jar_pool.cpp \ diff --git a/jbmc/src/java_bytecode/README.md b/jbmc/src/java_bytecode/README.md index fd04a7c0586..675a57b691e 100644 --- a/jbmc/src/java_bytecode/README.md +++ b/jbmc/src/java_bytecode/README.md @@ -76,11 +76,7 @@ types so we keep a stack of types for each parameter. We use the map in \ref select_pointer_typet::specialize_generics to retrieve the concrete type of generic parameters such as `MyGeneric::T` and of -arrays of generic parameters such as `MyGeneric::T[]`. Special attention -is paid to breaking infinite recursion when searching the map, e.g., -`MyGeneric::T` being specialized with `MyGeneric::U` and vice versa, for an -example of such a recursion see -\ref select_pointer_typet::get_recursively_instantiated_type. More complicated +arrays of generic parameters such as `MyGeneric::T[]`. More complicated generic types such as `MyGeneric` are specialized indirectly within \ref java_object_factoryt. Their concrete types are already stored in the map and are retrieved when needed, e.g., to initialize their fields. diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map.cpp b/jbmc/src/java_bytecode/generic_parameter_specialization_map.cpp new file mode 100644 index 00000000000..39033edf2ad --- /dev/null +++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map.cpp @@ -0,0 +1,67 @@ +/// Author: Diffblue Ltd. + +#include "generic_parameter_specialization_map.h" + +std::size_t generic_parameter_specialization_mapt::insert( + const std::vector ¶meters, + std::vector types) +{ + PRECONDITION(!parameters.empty()); + const auto first_param_it = + param_to_container.find(parameters.front().get_name()); + std::size_t container_index; + if(first_param_it == param_to_container.end()) + { + container_index = container_to_specializations.size(); + container_to_specializations.emplace_back(); + std::size_t param_index = 0; + for(const java_generic_parametert ¶meter : parameters) + { + const auto result = param_to_container.emplace( + parameter.get_name(), container_paramt{container_index, param_index++}); + INVARIANT( + result.second, "Some type parameters are already mapped but not all"); + } + } + else + { + container_index = first_param_it->second.container_index; + std::size_t param_index = 0; + for(const java_generic_parametert ¶meter : parameters) + { + const auto param_it = param_to_container.find(parameter.get_name()); + INVARIANT( + param_it != param_to_container.end(), + "Some type parameters are already mapped but not all"); + INVARIANT( + param_it->second.container_index == container_index, + "Not all type parameters are assigned to same container"); + INVARIANT( + param_it->second.param_index == param_index, + "Type parameters have been encountered in two different orders"); + ++param_index; + } + } + container_to_specializations[container_index].push(std::move(types)); + return container_index; +} + +void generic_parameter_specialization_mapt::pop(std::size_t container_index) +{ + container_to_specializations.at(container_index).pop(); +} + +optionalt +generic_parameter_specialization_mapt::pop(const irep_idt ¶meter_name) +{ + const auto types_it = param_to_container.find(parameter_name); + if(types_it == param_to_container.end()) + return {}; + std::stack> &stack = + container_to_specializations.at(types_it->second.container_index); + if(stack.empty()) + return {}; + reference_typet result = stack.top().at(types_it->second.param_index); + stack.pop(); + return result; +} diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map.h b/jbmc/src/java_bytecode/generic_parameter_specialization_map.h new file mode 100644 index 00000000000..914dca2758b --- /dev/null +++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map.h @@ -0,0 +1,141 @@ +/// Author: Diffblue Ltd. + +#ifndef CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_H +#define CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_H + +#include +#include + +#include + +#include "expr2java.h" +#include "java_types.h" + +/// A map from generic type parameters to their specializations (type arguments) +/// We need to map from the names of parameters to the container (class or +/// method) that contains them as well as the particular specialization of that +/// parameter. However we do not need the name of the container, merely the full +/// set of specializations for the parameters of that container. +/// We store a stack of specializations for each container for a particular +/// context. Finding the value for a type parameter is a matter of following +/// the specialization for that parameter, unwinding the stack of its container +/// as you do so and repeating until one reaches a non-generic type. +class generic_parameter_specialization_mapt +{ +private: + /// The index of the container and the type parameter inside that container + struct container_paramt + { + std::size_t container_index; + std::size_t param_index; + }; + /// A map from parameter names to container_paramt instances + std::unordered_map param_to_container; + /// The list of containers and, for each one, the stack of lists of + /// specializations + std::vector>> + container_to_specializations; + +public: + /// Insert a specialization for each type parameters of a container + /// \param parameters: The type parameters + /// \param types: The type arguments + /// \returns: The index of the added container + std::size_t insert( + const std::vector ¶meters, + std::vector types); + + /// Pop the top of the specialization stack for a given container + /// \param container_index: The index of the container to pop + void pop(std::size_t container_index); + + /// Pop the top of the specialization stack for the container associated with + /// a given type parameter + /// \param parameter_name: The name of the type parameter + /// \returns: The specialization for the given type parameter, if there was + /// one before the pop, or an empty optionalt if the stack was empty + optionalt pop(const irep_idt ¶meter_name); + + /// A wrapper for a generic_parameter_specialization_mapt and a namespacet + /// that can be output to a stream + struct printert + { + const generic_parameter_specialization_mapt ↦ + const namespacet &ns; + + printert( + const generic_parameter_specialization_mapt &map, + const namespacet &ns) + : map(map), ns(ns) + { + } + }; + + template + friend ostreamt &operator<<(ostreamt &stm, const printert &map); +}; + +/// Output a generic_parameter_specialization_mapt wrapped in a +/// generic_parameter_specialization_mapt::printert to a stream +/// \tparam ostreamt: The type of stream to output to (not restricted to be +/// derived from std::ostream) +/// \param stm: The stream to output to +/// \param map: The generic_parameter_specialization_mapt printer to output +/// \returns: A reference to the stream passed in +template +ostreamt &operator<<( + ostreamt &stm, + const generic_parameter_specialization_mapt::printert &map) +{ + if(map.map.container_to_specializations.empty()) + stm << "empty map"; + else + stm << "map:\n"; + std::vector> container_to_params( + map.map.container_to_specializations.size()); + for(const auto &elt : map.map.param_to_container) + { + std::vector ¶ms = + container_to_params[elt.second.container_index]; + if(params.size() < elt.second.param_index + 1) + params.resize(elt.second.param_index + 1); + params[elt.second.param_index] = elt.first; + } + const namespacet &ns = map.ns; + for(std::size_t index = 0; index < container_to_params.size(); ++index) + { + stm << "<"; + join_strings( + stm, + container_to_params.at(index).begin(), + container_to_params.at(index).end(), + ", "); + stm << ">: "; + std::stack> stack = + map.map.container_to_specializations.at(index); + while(!stack.empty()) + { + stm << "<"; + join_strings( + stm, + stack.top().begin(), + stack.top().end(), + ", ", + [&ns](const reference_typet &pointer_type) { + if(is_java_generic_parameter(pointer_type)) + { + return id2string( + to_java_generic_parameter(pointer_type).get_name()); + } + else + return type2java(pointer_type, ns); + }); + stm << ">, "; + stack.pop(); + } + stm << "\n"; + } + return stm; +} + +#endif // CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_H diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp index c845c3cde9a..4aa16ffd813 100644 --- a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp +++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.cpp @@ -35,51 +35,18 @@ get_all_generic_parameters(const typet &type) return generic_parameters; } -/// Add pairs to the controlled map. Own the keys and pop from their stack -/// on destruction; otherwise do nothing. -/// \param parameters: generic parameters that are the keys of the pairs to add -/// \param types: a type to add for each parameter -void generic_parameter_specialization_map_keyst::insert_pairs( - const std::vector ¶meters, - const std::vector &types) -{ - INVARIANT(erase_keys.empty(), "insert_pairs should only be called once"); - - for(const auto &pair : make_range(parameters).zip(types)) - { - // Only add the pair if the type is not the parameter itself, e.g., - // pair.first = pair.second = java::A::T. This can happen for example - // when initializing a pointer to an implicitly generic Java class type - // in gen_nondet_init and would result in a loop when the map is used - // to look up the type of the parameter. - if( - !(is_java_generic_parameter(pair.second) && - to_java_generic_parameter(pair.second).get_name() == - pair.first.get_name())) - { - const irep_idt &key = pair.first.get_name(); - const auto map_it = generic_parameter_specialization_map - .emplace(key, std::vector{}) - .first; - map_it->second.push_back(pair.second); - - // We added something; pop it when this - // generic_parameter_specialization_map_keyst is destroyed - erase_keys.push_back(key); - } - } -} - -/// Add a pair of a parameter and its types for each generic parameter of the -/// given generic pointer type to the controlled map. Own the keys and pop -/// from their stack on destruction; otherwise do nothing. +/// Add the parameters and their types for each generic parameter of the +/// given generic pointer type to the map. +/// Own the keys and pop from their stack on destruction. /// \param pointer_type: pointer type to get the specialized generic types from /// \param pointer_subtype_struct: struct type to which the generic pointer /// points, must be generic if the pointer is generic -void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer( +void generic_parameter_specialization_map_keyst::insert( const pointer_typet &pointer_type, const typet &pointer_subtype_struct) { + // Use a fresh generic_parameter_specialization_map_keyst for each scope + PRECONDITION(!container_id); if(!is_java_generic_type(pointer_type)) return; // The supplied type must be the full type of the pointer's subtype @@ -91,7 +58,7 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer( // - an incomplete class or // - a class that is neither generic nor implicitly generic (this // may be due to unsupported class signature) - // then ignore the generic types in the pointer and do not add any pairs. + // then ignore the generic types in the pointer and do not add an entry. // TODO TG-1996 should decide how mocking and generics should work // together. Currently an incomplete class is never marked as generic. If // this changes in TG-1996 then the condition below should be updated. @@ -115,34 +82,39 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_pointer( type_args.size() == generic_parameters.size(), "All generic parameters of the pointer type need to be specified"); - insert_pairs(generic_parameters, type_args); + container_id = + generic_parameter_specialization_map.insert(generic_parameters, type_args); } -/// Add a pair of a parameter and its types for each generic parameter of the -/// given generic symbol type to the controlled map. This function is used -/// for generic bases (superclass or interfaces) where the reference to it is -/// in the form of a symbol rather than a pointer (as opposed to the function -/// insert_pairs_for_pointer). Own the keys and pop from their stack -/// on destruction; otherwise do nothing. +/// Add the parameters and their types for each generic parameter of the +/// given generic symbol type to the map. +/// This function is used for generic bases (superclass or interfaces) where +/// the reference to it is in the form of a symbol rather than a pointer. +/// Own the keys and pop from their stack on destruction. /// \param struct_tag_type: symbol type to get the specialized generic types /// from /// \param symbol_struct: struct type of the symbol type, must be generic if /// the symbol is generic -void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol( +void generic_parameter_specialization_map_keyst::insert( const struct_tag_typet &struct_tag_type, const typet &symbol_struct) { + // Use a fresh generic_parameter_specialization_map_keyst for each scope + PRECONDITION(!container_id); + if(!is_java_generic_struct_tag_type(struct_tag_type)) + return; + // The supplied type must be the full type of the pointer's subtype + PRECONDITION( + struct_tag_type.get(ID_identifier) == symbol_struct.get(ID_name)); + // If the struct is: // - an incomplete class or // - a class that is neither generic nor implicitly generic (this // may be due to unsupported class signature) - // then ignore the generic types in the struct_tag_type and do not add any - // pairs. + // then ignore the generic types in the struct and do not add an entry. // TODO TG-1996 should decide how mocking and generics should work // together. Currently an incomplete class is never marked as generic. If // this changes in TG-1996 then the condition below should be updated. - if(!is_java_generic_struct_tag_type(struct_tag_type)) - return; if(to_java_class_type(symbol_struct).get_is_stub()) return; if( @@ -163,5 +135,6 @@ void generic_parameter_specialization_map_keyst::insert_pairs_for_symbol( type_args.size() == generic_parameters.size(), "All generic parameters of the superclass need to be concretized"); - insert_pairs(generic_parameters, type_args); + container_id = + generic_parameter_specialization_map.insert(generic_parameters, type_args); } diff --git a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h index 691c07f2f38..70e4d36dd15 100644 --- a/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h +++ b/jbmc/src/java_bytecode/generic_parameter_specialization_map_keys.h @@ -1,4 +1,3 @@ - /// Author: Diffblue Ltd. #ifndef CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H @@ -15,6 +14,12 @@ /// on leaving that scope. class generic_parameter_specialization_map_keyst { +private: + /// Generic parameter specialization map to modify + generic_parameter_specialization_mapt &generic_parameter_specialization_map; + /// Key of the container to pop on destruction + optionalt container_id; + public: /// Initialize a generic-parameter-specialization-map entry owner operating /// on a given map. Initially it does not own any map entry. @@ -29,15 +34,8 @@ class generic_parameter_specialization_map_keyst /// controlled map. ~generic_parameter_specialization_map_keyst() { - for(const auto key : erase_keys) - { - const auto map_it = generic_parameter_specialization_map.find(key); - PRECONDITION(map_it != generic_parameter_specialization_map.end()); - std::vector &val = map_it->second; - val.pop_back(); - if(val.empty()) - generic_parameter_specialization_map.erase(map_it); - } + if(container_id) + generic_parameter_specialization_map.pop(*container_id); } // Objects of these class cannot be copied in any way - delete the copy @@ -47,21 +45,11 @@ class generic_parameter_specialization_map_keyst generic_parameter_specialization_map_keyst & operator=(const generic_parameter_specialization_map_keyst &) = delete; - void insert_pairs_for_pointer( + void insert( const pointer_typet &pointer_type, const typet &pointer_subtype_struct); - void - insert_pairs_for_symbol(const struct_tag_typet &, const typet &symbol_struct); - -private: - /// Generic parameter specialization map to modify - generic_parameter_specialization_mapt &generic_parameter_specialization_map; - /// Keys of the entries to pop on destruction - std::vector erase_keys; - void insert_pairs( - const std::vector ¶meters, - const std::vector &types); + void insert(const struct_tag_typet &, const typet &symbol_struct); }; #endif // CPROVER_JAVA_BYTECODE_GENERIC_PARAMETER_SPECIALIZATION_MAP_KEYS_H diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 394d0ed816b..bc62934f148 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -495,7 +495,7 @@ void java_object_factoryt::gen_nondet_pointer_init( generic_parameter_specialization_map_keyst generic_parameter_specialization_map_keys( generic_parameter_specialization_map); - generic_parameter_specialization_map_keys.insert_pairs_for_pointer( + generic_parameter_specialization_map_keys.insert( replacement_pointer_type, ns.follow(replacement_pointer_type.subtype())); const symbol_exprt real_pointer_symbol = gen_nondet_subtype_pointer_init( @@ -1007,7 +1007,7 @@ void java_object_factoryt::gen_nondet_init( generic_parameter_specialization_map_keyst generic_parameter_specialization_map_keys( generic_parameter_specialization_map); - generic_parameter_specialization_map_keys.insert_pairs_for_pointer( + generic_parameter_specialization_map_keys.insert( pointer_type, ns.follow(pointer_type.subtype())); gen_nondet_pointer_init( @@ -1034,7 +1034,7 @@ void java_object_factoryt::gen_nondet_init( const typet &symbol = override_type.has_value() ? *override_type : expr.type(); PRECONDITION(symbol.id() == ID_struct_tag); - generic_parameter_specialization_map_keys.insert_pairs_for_symbol( + generic_parameter_specialization_map_keys.insert( to_struct_tag_type(symbol), struct_type); } diff --git a/jbmc/src/java_bytecode/select_pointer_type.cpp b/jbmc/src/java_bytecode/select_pointer_type.cpp index dc659aaefca..b93060269d1 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.cpp +++ b/jbmc/src/java_bytecode/select_pointer_type.cpp @@ -20,66 +20,40 @@ pointer_typet select_pointer_typet::convert_pointer_type( &generic_parameter_specialization_map, const namespacet &) const { - // if we have a map of generic parameters -> types and the pointer is - // a generic parameter, specialize it with concrete types - if(!generic_parameter_specialization_map.empty()) - { - generic_parameter_recursion_trackingt visited; - const auto &type = specialize_generics( - pointer_type, generic_parameter_specialization_map, visited); - INVARIANT(visited.empty(), "recursion stack must be empty here"); - return type; - } - else - { - return pointer_type; - } + return specialize_generics( + pointer_type, generic_parameter_specialization_map); } pointer_typet select_pointer_typet::specialize_generics( const pointer_typet &pointer_type, const generic_parameter_specialization_mapt - &generic_parameter_specialization_map, - generic_parameter_recursion_trackingt &visited_nodes) const + &generic_parameter_specialization_map) const { auto parameter = type_try_dynamic_cast(pointer_type); if(parameter != nullptr) { - const irep_idt ¶meter_name = parameter->get_name(); + irep_idt parameter_name = parameter->get_name(); - // avoid infinite recursion by looking at each generic argument from - // previous assignments - if(visited_nodes.count(parameter_name) != 0) + // Make a local copy of the specialization map to unwind + generic_parameter_specialization_mapt spec_map_copy = + generic_parameter_specialization_map; + while(true) { - const optionalt result = get_recursively_instantiated_type( - parameter_name, generic_parameter_specialization_map); - return result.has_value() ? result.value() : pointer_type; - } - - const auto specialization = - generic_parameter_specialization_map.find(parameter_name); - if(specialization == generic_parameter_specialization_map.end()) - { - // this means that the generic pointer_type has not been specialized - // in the current context (e.g., the method under test is generic); - // we return the pointer_type itself which is basically a pointer to - // its upper bound - return pointer_type; + const optionalt specialization = + spec_map_copy.pop(parameter_name); + if(!specialization) + { + // This means that the generic pointer_type has not been specialized + // in the current context (e.g., the method under test is generic); + // we return the pointer_type itself which is a pointer to its upper + // bound + return pointer_type; + } + + if(!is_java_generic_parameter(*specialization)) + return *specialization; + parameter_name = to_java_generic_parameter(*specialization).get_name(); } - const pointer_typet &type = specialization->second.back(); - - // generic parameters can be adopted from outer classes or superclasses so - // we may need to search for the concrete type recursively - if(!is_java_generic_parameter(type)) - return type; - - visited_nodes.insert(parameter_name); - const auto returned_type = specialize_generics( - to_java_generic_parameter(type), - generic_parameter_specialization_map, - visited_nodes); - visited_nodes.erase(parameter_name); - return returned_type; } auto subtype = @@ -93,7 +67,7 @@ pointer_typet select_pointer_typet::specialize_generics( return pointer_type; const pointer_typet &new_array_type = specialize_generics( - *array_element_type, generic_parameter_specialization_map, visited_nodes); + *array_element_type, generic_parameter_specialization_map); pointer_typet replacement_array_type = java_array_type('a'); replacement_array_type.subtype().set(ID_element_type, new_array_type); @@ -103,109 +77,6 @@ pointer_typet select_pointer_typet::specialize_generics( return pointer_type; } -/// Return the first concrete type instantiation if any such exists. This method -/// is only to be called when \ref select_pointer_typet::specialize_generics -/// cannot find an instantiation due to a loop in its recursion. -/// -/// Example: -/// `class MyGeneric { MyGeneric gen; T t;}` -/// For example, when instantiating `MyGeneric my` we need to -/// resolve the type of `my.gen.t`. The map would in this context contain -/// - T -> (Integer, U) -/// - U -> (String, T) -/// -/// Note that the top of the stacks for T and U create a recursion T -> U, -/// U-> T. We want to break it and specialize `T my.gen.t` to `String my.gen.t`. -/// \param parameter_name: The name of the generic parameter type we want to -/// have instantiated -/// \param generic_parameter_specialization_map: Map of type names to -/// specialization stack -/// \return The first instantiated type for the generic type or nothing if no -/// such instantiation exists. -optionalt -select_pointer_typet::get_recursively_instantiated_type( - const irep_idt ¶meter_name, - const generic_parameter_specialization_mapt - &generic_parameter_specialization_map) const -{ - generic_parameter_recursion_trackingt visited; - const size_t max_depth = - generic_parameter_specialization_map.find(parameter_name)->second.size(); - - irep_idt current_parameter = parameter_name; - for(size_t depth = 0; depth < max_depth; depth++) - { - const auto retval = get_recursively_instantiated_type( - current_parameter, generic_parameter_specialization_map, visited, depth); - if(retval.has_value()) - { - CHECK_RETURN(!is_java_generic_parameter(*retval)); - return retval; - } - CHECK_RETURN(visited.empty()); - - const auto &entry = - generic_parameter_specialization_map.find(current_parameter) - ->second.back(); - current_parameter = to_java_generic_parameter(entry).get_name(); - } - return {}; -} - -/// See get_recursively instantiated_type, the additional parameters just track -/// the recursion to prevent visiting the same depth again and specify which -/// stack depth is analyzed. -/// \param parameter_name: The name of the generic parameter type we want to -/// have instantiated -/// \param generic_parameter_specialization_map: Map of type names to -/// specialization stack -/// \param visited: Tracks the visited parameter names -/// \param depth: Stack depth to analyze -/// \return if this type is not a generic type, it is returned as a valid -/// instantiation, if nothing can be found at the given depth, en empty -/// optional is returned -optionalt -select_pointer_typet::get_recursively_instantiated_type( - const irep_idt ¶meter_name, - const generic_parameter_specialization_mapt - &generic_parameter_specialization_map, - generic_parameter_recursion_trackingt &visited, - const size_t depth) const -{ - const auto &val = generic_parameter_specialization_map.find(parameter_name); - INVARIANT( - val != generic_parameter_specialization_map.end(), - "generic parameter must be a key in map"); - - const auto &replacements = val->second; - - INVARIANT( - depth < replacements.size(), "cannot access elements outside stack"); - - // Check if there is a recursion loop, if yes return with nothing found - if(visited.find(parameter_name) != visited.end()) - { - return {}; - } - - const size_t index = (replacements.size() - 1) - depth; - const auto &type = replacements[index]; - - if(!is_java_generic_parameter(type)) - { - return type; - } - - visited.insert(parameter_name); - const auto inst_val = get_recursively_instantiated_type( - to_java_generic_parameter(type).get_name(), - generic_parameter_specialization_map, - visited, - depth); - visited.erase(parameter_name); - return inst_val; -} - std::set select_pointer_typet::get_parameter_alternative_types( const irep_idt &, diff --git a/jbmc/src/java_bytecode/select_pointer_type.h b/jbmc/src/java_bytecode/select_pointer_type.h index bc4df621080..02ff9ef06d2 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.h +++ b/jbmc/src/java_bytecode/select_pointer_type.h @@ -11,6 +11,7 @@ Author: Diffblue Ltd. /// \file /// Handle selection of correct pointer type (for example changing abstract /// classes to concrete versions). +#include "generic_parameter_specialization_map.h" #include "java_types.h" #include @@ -19,23 +20,10 @@ Author: Diffblue Ltd. #include #include -typedef std::unordered_map> - generic_parameter_specialization_mapt; -typedef std::set generic_parameter_recursion_trackingt; - class namespacet; class select_pointer_typet { - optionalt get_recursively_instantiated_type( - const irep_idt &, - const generic_parameter_specialization_mapt &, - generic_parameter_recursion_trackingt &, - const size_t) const; - optionalt get_recursively_instantiated_type( - const irep_idt ¶meter_name, - const generic_parameter_specialization_mapt &visited) const; - public: virtual ~select_pointer_typet() = default; @@ -78,18 +66,24 @@ class select_pointer_typet /// - generic type: T[] /// - map: T -> U; U -> String /// - result: String[] + /// Example 2: + /// `class MyGeneric { MyGeneric gen; T t;}` + /// When instantiating `MyGeneric my` we need to resolve the + /// type of `my.gen.t`. The map would in this context contain + /// - T -> (Integer, U) + /// - U -> (String, T) + /// + /// Note that the top of the stacks for T and U create a recursion T -> U, + /// U-> T. We break it and specialize `T my.gen.t` to `String my.gen.t`. /// \param pointer_type: The pointer to be specialized /// \param generic_parameter_specialization_map: Map of types for all /// generic parameters in the current scope - /// \param visited_nodes: Set of parameter names already considered in - /// recursion, used to avoid infinite recursion /// \return Pointer type where generic parameters are replaced with /// specialized types (if set in the current scope) pointer_typet specialize_generics( const pointer_typet &pointer_type, const generic_parameter_specialization_mapt - &generic_parameter_specialization_map, - generic_parameter_recursion_trackingt &visited_nodes) const; + &generic_parameter_specialization_map) const; }; #endif // CPROVER_JAVA_BYTECODE_SELECT_POINTER_TYPE_H diff --git a/jbmc/unit/java_bytecode/goto_program_generics/Bar.class b/jbmc/unit/java_bytecode/goto_program_generics/Bar.class new file mode 100644 index 0000000000000000000000000000000000000000..28c480512165e1cc5554207d1a9d653fa93a930f GIT binary patch literal 308 zcmZXPF;BxV5QX2RO+rJVg%yDq3ju>)~1BsR4}IO0g^aTKRk2iSHLjIej33G+S52D#N76sF-c>x& zZSLgGH(u5C=8-G!R(j31Y}n~)bV}0xi4Y2Gczw$?W`7rjTfcqBxXZu z!7y2JU$R~B2$_=rW~C;3EDT+GZXrWDfPX3$+S&XR?rzm>D6XR zylHX$ta3KjQ`5|y+_~DRqIiAOxwA{N(zm+Q*5u2J=B6ID(c|)IRS5?Fuf!=@{4$6@ u8$NjNS_Q-{bpLcnh9-)2hwPZOas2al$Qy}Zm)KdGM~wT8>0>~*g}om%_ec@| literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/goto_program_generics/KeyValue.class b/jbmc/unit/java_bytecode/goto_program_generics/KeyValue.class index d093b9493294bc8edb2cfcbce204f3f5dd9dd7a0..cf2db1a9f1573958e11a11acd89bd3a5940ff738 100644 GIT binary patch delta 81 zcmdnQa+6u~)W2Q(7#J8#7$mtEm>I;_8N}HcBqoZko%sE^fh+?f5Hc{ZYHep=+z4ba YG6(@lHn5-|0~3(N03?MOM8LEt0JL8Vu>b%7 delta 164 zcmcb~yop8h)W2Q(7#J8#7-YB@m>DG58Kl@5q$i55)f4i`PfpAUODxJvOv*_O0TGN0 zEF~G4#f%JMsB)DBsS|g<3vpy%1VRP|R;}#}j2nRrW(FZ3$p#h_WDo|jc_0cHL>O3s VJW&)8b|8-ls2W6yF^Gd{2>^@n92)=t diff --git a/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.class b/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.class index ed2b36215260644dd843a70e930ff028a7701c03..d15be56452a911ce7aaa4eef858d436c658b6151 100644 GIT binary patch delta 186 zcmbQw`j=&cETcMmNosM4TYf$x1FH{^vSwru2hlb@S&3zd`ZH0qTdFhiS70hl$l&?JvpDzgqe?lfATU$3r6P2_ZbcAnHU%tfFcZx3<5xwK9FVv z(yUtB85lPL8B7d { K key; V value; } +class Foo { + Bar bar; + T t; +} +class Bar { + Foo foo; +} class MutuallyRecursiveGenerics { KeyValue example1; Three example2; Outer example3; + Foo testFoo; void f() { } } diff --git a/jbmc/unit/java_bytecode/goto_program_generics/Outer$Inner.class b/jbmc/unit/java_bytecode/goto_program_generics/Outer$Inner.class index 136c195e97df665129f992026280d4aea55b80a8..891911ec9c622da9c9689632821a8e8168ae06d5 100644 GIT binary patch delta 134 zcmaFLa*0{$)W2Q(7#J8#7-Tsam>ER47+4rY*%`#y8Kfpkbxf9HOc0W0XOLlJ;Px*q zNi9 XG6;cbVFpPc%>|TYW)NeLU|;|M>IoBX delta 304 zcmcb_{FFuN)W2Q(7#J8#7?d~}m>HzG7+4r&*cs&58RREQb<_*_TQge4YbCMM;i zhJXl029}bH%wk3cR?ob=)FMU(9x&~klUQ7w3KZt`@h>e&Em8rCS~D_;p&C(H05e7w zqR=M9+d3r7IwaKEP7kcd2E+tv)UXMixHMKsft^8-k%1e@(8=12NyPySOhCxMz@??V zm4Q)fI|I{3Adi_r07$YiFak*?20ff$?3=9k=4ANW-%nah}3=-@NlI#pp6D77xR$%<*Aj`lAgbWOff$?3=9k=3<_Kf%nUN@46^JDa_kK96D76;3HjtFC+37D7G)+T<)nsy z2u22$l8nq^Mh12t|I(7wB5OtlF;rER1u&ID5G6Jt-qs;u)*+$RcGeS5{YY_SU<5)2 z23D=@42&Cr3}yylAjt+6WMmKlvUwm17(^MwfIM*&5eXoVnSm2XGBHRpNP%f-pl${R NE}$+JpeQQ?0|2{OCno>^ diff --git a/jbmc/unit/java_bytecode/goto_program_generics/Three.class b/jbmc/unit/java_bytecode/goto_program_generics/Three.class index 3921f56904040ddb6fe635f50d0223fb88357d6e..69350f1c8d614a63ba079c59962348cf0a58a602 100644 GIT binary patch delta 82 zcmcc0@`qXU)W2Q(7#J8#7^Jxvm>DG486?>mq$Y~4-}sY*(Lk1g5eOL=Shcn@Fm41g Z7#T!>BpXHzm8D!WQWG9NQ*Aw!|PfpAUODxJvOv*_O0TGN0 zEF~G4#f%JMsB)DBsT=q5Gln=aFajY11FP0{2F8s*1~Y>QkYoc3axsVk**p*h3}Otd WK%O{?2q%!o1XK+oB^V^Zv=jiCD;v51 diff --git a/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp index 3638af5d509..096a2dbb25f 100644 --- a/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp +++ b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp @@ -297,6 +297,67 @@ SCENARIO( } } } + + THEN("The Object has a field `testFoo` of type `Foo`") + { + const auto &testFoo_field = + require_goto_statements::require_struct_component_assignment( + tmp_object_name, + {}, + "testFoo", + "java::Foo", + {}, + entry_point_code, + symbol_table); + + THEN("Object 'testFoo' has field 't' of type `Long`") + { + require_goto_statements::require_struct_component_assignment( + testFoo_field, + {}, + "t", + "java::java.lang.Long", + {}, + entry_point_code, + symbol_table); + } + + THEN("`testFoo` has field bar") + { + const auto &bar_field = + require_goto_statements::require_struct_component_assignment( + testFoo_field, + {}, + "bar", + "java::Bar", + {}, + entry_point_code, + symbol_table); + THEN("`bar` has field foo") + { + const auto &foo_field = + require_goto_statements::require_struct_component_assignment( + bar_field, + {}, + "foo", + "java::Foo", + {}, + entry_point_code, + symbol_table); + THEN("'foo' has field 't' of type `Long`") + { + require_goto_statements::require_struct_component_assignment( + foo_field, + {}, + "t", + "java::java.lang.Long", + {}, + entry_point_code, + symbol_table); + } + } + } + } } // TODO: add test for TG-3828 From 8fe86eef5191e5bacb8a983a7e95152d8b4052de Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Thu, 18 Jul 2019 17:27:43 +0100 Subject: [PATCH 18/19] Change naming of implicit type parameters for inner classes Previously they duplicated the names for the type parameters of the outer classes --- .../java_bytecode_convert_class.cpp | 30 ++++++++++------- .../parse_derived_generic_class.cpp | 22 +++++++++---- ...parse_generic_class_with_inner_classes.cpp | 32 ++++++++++++------- 3 files changed, 53 insertions(+), 31 deletions(-) diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index c2c9be8114d..b42d1e97c96 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -25,6 +25,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include #include +#include #include #include @@ -1037,12 +1038,10 @@ static void find_and_replace_parameter( const std::string &replacement_parameter_full_name = id2string(replacement_parameter_it->type_variable().get_identifier()); - // the replacement parameter is a viable one, i.e., it comes from an outer - // class - PRECONDITION( - get_without_final_name_component(parameter_full_name) - .compare( - get_without_final_name_component(replacement_parameter_full_name)) > 0); + // Check the replacement parameter comes from an outer class + PRECONDITION(has_prefix( + replacement_parameter_full_name, + get_without_final_name_component(parameter_full_name))); parameter.type_variable_ref().set_identifier(replacement_parameter_full_name); } @@ -1176,12 +1175,19 @@ void mark_java_implicitly_generic_class_type( to_java_class_type(outer_class_symbol.type); if(is_java_generic_class_type(outer_class_type)) { - const auto &outer_generic_type_parameters = - to_java_generic_class_type(outer_class_type).generic_types(); - implicit_generic_type_parameters.insert( - implicit_generic_type_parameters.begin(), - outer_generic_type_parameters.begin(), - outer_generic_type_parameters.end()); + for(const java_generic_parametert &outer_generic_type_parameter : + to_java_generic_class_type(outer_class_type).generic_types()) + { + // Create a new generic type parameter with name in the form: + // java::Outer$Inner::Outer::T + irep_idt identifier = qualified_class_name + "::" + + id2string(strip_java_namespace_prefix( + outer_generic_type_parameter.get_name())); + java_generic_parameter_tagt bound = to_java_generic_parameter_tag( + outer_generic_type_parameter.subtype()); + bound.type_variable_ref().set_identifier(identifier); + implicit_generic_type_parameters.emplace_back(identifier, bound); + } } outer_class_delimiter = outer_class_name.rfind('$'); } diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp index b0a57720564..c16540bbe02 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp @@ -187,7 +187,9 @@ SCENARIO( const class_typet &derived_class_type = require_type::require_complete_java_implicitly_generic_class( - derived_symbol.type, {"java::ContainsInnerClassGeneric::T"}); + derived_symbol.type, + {"java::ContainsInnerClassGeneric$InnerClass::" + "ContainsInnerClassGeneric::T"}); THEN("The base for superclass has the correct generic type information") { @@ -197,7 +199,8 @@ SCENARIO( base_type, "java::Generic", {{require_type::type_argument_kindt::Var, - "java::ContainsInnerClassGeneric::T"}}); + "java::ContainsInnerClassGeneric$InnerClass::" + "ContainsInnerClassGeneric::T"}}); } } @@ -552,7 +555,8 @@ SCENARIO( require_type::require_java_generic_struct_tag_type( base_type, "java::GenericBase$ImplicitGeneric", - {{require_type::type_argument_kindt::Var, "java::GenericBase::T"}}); + {{require_type::type_argument_kindt::Var, + "java::GenericBase$ExtendImplicit::GenericBase::T"}}); } } @@ -573,7 +577,8 @@ SCENARIO( require_type::require_java_generic_struct_tag_type( base_type, "java::GenericBase$ImplicitAndExplicitGeneric", - {{require_type::type_argument_kindt::Var, "java::GenericBase::T"}, + {{require_type::type_argument_kindt::Var, + "java::GenericBase$ExtendImplicitAndExplicit::GenericBase::T"}, {require_type::type_argument_kindt::Var, "java::GenericBase$ExtendImplicitAndExplicit::S"}}); } @@ -596,9 +601,12 @@ SCENARIO( require_type::require_java_generic_struct_tag_type( base_type, "java::GenericBase2$ImplicitAndExplicitGeneric", - {{require_type::type_argument_kindt::Var, "java::GenericBase2::T"}, - {require_type::type_argument_kindt::Var, "java::GenericBase2::S"}, - {require_type::type_argument_kindt::Var, "java::GenericBase2::S"}}); + {{require_type::type_argument_kindt::Var, + "java::GenericBase2$ExtendImplicitAndExplicit::GenericBase2::T"}, + {require_type::type_argument_kindt::Var, + "java::GenericBase2$ExtendImplicitAndExplicit::GenericBase2::S"}, + {require_type::type_argument_kindt::Var, + "java::GenericBase2$ExtendImplicitAndExplicit::GenericBase2::S"}}); } } } diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp index 313ed682723..4d135ff4121 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp @@ -18,7 +18,8 @@ SCENARIO( "GenericClassWithInnerClasses", "./java_bytecode/java_bytecode_parse_generics"); - std::string outer_class_prefix = "java::GenericClassWithInnerClasses"; + std::string outer_class_name = "GenericClassWithInnerClasses"; + std::string outer_class_prefix = "java::" + outer_class_name; WHEN("Generic outer class has fields which are objects of the inner classes") { @@ -69,7 +70,8 @@ SCENARIO( { const java_implicitly_generic_class_typet &java_class = require_type::require_complete_java_implicitly_generic_class( - class_symbol.type, {outer_class_prefix + "::T"}); + class_symbol.type, + {inner_class_prefix + "::" + outer_class_name + "::T"}); THEN( "There is a field t1 which is the generic parameter of the outer " @@ -77,7 +79,7 @@ SCENARIO( { const auto &field = require_type::require_component(java_class, "t1"); require_type::require_java_generic_parameter( - field.type(), outer_class_prefix + "::T"); + field.type(), inner_class_prefix + "::" + outer_class_name + "::T"); } THEN( "There is a field t2 of generic type with the generic " @@ -88,7 +90,7 @@ SCENARIO( require_type::require_java_generic_type( field.type(), {{require_type::type_argument_kindt::Var, - outer_class_prefix + "::T"}}); + inner_class_prefix + "::" + outer_class_name + "::T"}}); } } } @@ -105,7 +107,8 @@ SCENARIO( { const java_implicitly_generic_class_typet &java_class = require_type::require_complete_java_implicitly_generic_class( - class_symbol.type, {outer_class_prefix + "::T"}); + class_symbol.type, + {inner_inner_class_prefix + "::" + outer_class_name + "::T"}); THEN( "There is a field tt1 which is the generic parameter of the outer " @@ -113,7 +116,8 @@ SCENARIO( { const auto &field = require_type::require_component(java_class, "tt1"); require_type::require_java_generic_parameter( - field.type(), outer_class_prefix + "::T"); + field.type(), + inner_inner_class_prefix + "::" + outer_class_name + "::T"); } THEN( "There is a field tt2 of nested generic type with the generic " @@ -132,7 +136,7 @@ SCENARIO( require_type::require_java_generic_type( type_argument, {{require_type::type_argument_kindt::Var, - outer_class_prefix + "::T"}}); + inner_inner_class_prefix + "::" + outer_class_name + "::T"}}); } } } @@ -148,7 +152,8 @@ SCENARIO( THEN("It has correct generic types and implicit generic types") { require_type::require_complete_java_implicitly_generic_class( - class_symbol.type, {outer_class_prefix + "::T"}); + class_symbol.type, + {generic_inner_class_prefix + "::" + outer_class_name + "::T"}); const java_generic_class_typet &generic_class = require_type::require_complete_java_generic_class( class_symbol.type, {generic_inner_class_prefix + "::U"}); @@ -160,7 +165,8 @@ SCENARIO( const auto &field = require_type::require_component(generic_class, "gt1"); require_type::require_java_generic_parameter( - field.type(), outer_class_prefix + "::T"); + field.type(), + generic_inner_class_prefix + "::" + outer_class_name + "::T"); } THEN( "There is a field gt2 of generic type with the generic " @@ -173,9 +179,9 @@ SCENARIO( require_type::require_java_generic_type( field.type(), {{require_type::type_argument_kindt::Var, - outer_class_prefix + "::T"}, + generic_inner_class_prefix + "::" + outer_class_name + "::T"}, {require_type::type_argument_kindt::Var, - generic_inner_class_prefix + "::U"}}); + generic_inner_class_prefix + "::U"}}); } } } @@ -194,7 +200,9 @@ SCENARIO( { require_type::require_complete_java_implicitly_generic_class( class_symbol.type, - {outer_class_prefix + "::T", outer_class_prefix + "$GenericInner::U"}); + {generic_inner_inner_class_prefix + "::" + outer_class_name + + "$GenericInner::U", + generic_inner_inner_class_prefix + "::" + outer_class_name + "::T"}); require_type::require_complete_java_generic_class( class_symbol.type, {generic_inner_inner_class_prefix + "::V"}); } From 186adb8aee29a624594d63fdf7ea824f7aa65753 Mon Sep 17 00:00:00 2001 From: Nathan Phillips Date: Wed, 24 Jul 2019 13:54:38 +0100 Subject: [PATCH 19/19] Make explicit type parameters shadow implicit ones with the same names Fixes problem where outer class type parameters take precedence over inner class ones Previously field would be given the type of the argument assigned to A::T, not B::T. class A { class B { T field; } }? --- .../java_bytecode_convert_class.cpp | 11 +++ .../MutuallyRecursiveGenerics.java | 2 +- .../goto_program_generics/Outer.class | Bin 514 -> 514 bytes .../mutually_recursive_generics.cpp | 39 +++++++++ ...asses$GenericInner$GenericInnerInner.class | Bin 848 -> 606 bytes ...s$GenericInner$ShadowingGenericInner.class | Bin 0 -> 673 bytes ...icClassWithInnerClasses$GenericInner.class | Bin 900 -> 999 bytes ...assWithInnerClasses$Inner$InnerInner.class | Bin 821 -> 617 bytes .../GenericClassWithInnerClasses$Inner.class | Bin 774 -> 592 bytes ...ricClassWithInnerClasses$StaticInner.class | Bin 616 -> 432 bytes .../GenericClassWithInnerClasses.class | Bin 1111 -> 951 bytes .../GenericClassWithInnerClasses.java | 6 ++ ...parse_generic_class_with_inner_classes.cpp | 79 ++++++++++++++++-- 13 files changed, 130 insertions(+), 7 deletions(-) create mode 100644 jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner$ShadowingGenericInner.class diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index b42d1e97c96..b2028ca88b0 100644 --- a/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp @@ -1205,6 +1205,17 @@ void mark_java_implicitly_generic_class_type( java_implicitly_generic_class_typet new_class_type( class_type, implicit_generic_type_parameters); + // Prepend existing parameters so choose those above any inherited + if(is_java_generic_class_type(class_type)) + { + const java_generic_class_typet::generic_typest &class_type_params = + to_java_generic_class_type(class_type).generic_types(); + implicit_generic_type_parameters.insert( + implicit_generic_type_parameters.begin(), + class_type_params.begin(), + class_type_params.end()); + } + for(auto &field : new_class_type.components()) { find_and_replace_parameters( diff --git a/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.java b/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.java index db4b677067c..ecf3a607944 100644 --- a/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.java +++ b/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.java @@ -3,7 +3,7 @@ class Inner { Outer o; U u; } - Inner inner; + Inner inner; K key; V value; } diff --git a/jbmc/unit/java_bytecode/goto_program_generics/Outer.class b/jbmc/unit/java_bytecode/goto_program_generics/Outer.class index 4f54020f3888a271f0b47dea250fa6b67f57a889..0cb609e46b01b2038221c3b235525f6e4447e0e5 100644 GIT binary patch delta 12 TcmZo-X=0g><9`U=kw$8U6$p delta 12 TcmZo-X=0g><L~U=kw$8TkYj diff --git a/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp index 096a2dbb25f..12937b8d43d 100644 --- a/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp +++ b/jbmc/unit/java_bytecode/goto_program_generics/mutually_recursive_generics.cpp @@ -298,6 +298,45 @@ SCENARIO( } } + THEN( + "The Object has a field `example3` of type `Outer`") + { + const auto &example3_field = + require_goto_statements::require_struct_component_assignment( + tmp_object_name, + {}, + "example3", + "java::Outer", + {}, + entry_point_code, + symbol_table); + + THEN("`example3` has field `inner` of type `Inner`") + { + const auto &inner_field = + require_goto_statements::require_struct_component_assignment( + example3_field, + {}, + "inner", + "java::Outer$Inner", + {}, + entry_point_code, + symbol_table); + + THEN("`inner` has a field `u` of type `Byte`") + { + require_goto_statements::require_struct_component_assignment( + inner_field, + {}, + "u", + "java::java.lang.Byte", + {}, + entry_point_code, + symbol_table); + } + } + } + THEN("The Object has a field `testFoo` of type `Foo`") { const auto &testFoo_field = diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner$GenericInnerInner.class b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner$GenericInnerInner.class index 0384e7e68604b6b3082c9c79816064343a8d97f9..a15be1947c29106b1ffa4c072c2958a50947795a 100644 GIT binary patch delta 153 zcmcb>c8^8v)W2Q(7#J8#7^FEFm>Gn)7+4sD*%?IG8N?VF*h(@oi&YHS86+mEEu1`` zF`rR#GCz~U#K$6&{h5SWq!<}ACpKtK?q_oIRbpTQLIwsdE$yugj9S|nm^K1=j10U$ qk_|{RFbD#T=L6DA4EziNU|NuY14s)2Mc5d`8Q6hrW*|$HfdK%*j}>45 delta 333 zcmcb|a)C|l)W2Q(7#J8#7!)`em>DFv7+4r2*%_qR8KfB**h(@oi&YHS8DuA_Ei@GJ z$xlwq2}>->Oiap24FM613@jiej0}SAsd=eInaQ4cKnhGSGT2V6*P5KnC?spm$RLKQ zx3U1H-)CaItiDZ1h_#&_vJo~Rp=cstLv2FBtnI8P9xY^%V`Q+N*q{kCUu1GOqcEfV z0)N+f#Noi}gi&F;+3+xyEafD`Pe5Jz4|0vj4OHEa{ozAdcDgS6U8Iu;?<8H;;S zcZ55tUk}D|7@QGOT{Ut=F!dxM-s>}y3~c2Wk2UNPj0@>XPYo|!Hta^Wff$?3=9k=4C)iPj3q^bGZIts%QN%R-Ba^Yi!zfv^MDjPgUUqfN+G^t zn50`~YEB9xgX3gJMlC57ta_{&8RCJ`vXhrGifia$Rbu0ll~|UjpOcuEt{+@d1hjPG z`qIh!8DscF8N_%P#2HlC8PpgVG$-ztnHff$?3=9k=3~Cd(j3-8vPi|u@kQMUDPfpAUODxJvOv*_O0TGN0EF~G4 z#f%Kv6CY~HS~D_;p{l7YfT=T`_)vDT6Qekz_2e&%aeM*{f;Vm<)Y{I#v=PW-W)KCEY+$v#3}QgG7(^9=ID-U`2UHI>jgdhT$mU^SGyw~V lGe`kxW~dXS8DxMwCI(rcK_DxcfHDdUtUxw9kj25k004q(Ek^(V diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$Inner$InnerInner.class b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$Inner$InnerInner.class index 82c05531a808ca66bdf5c70c2b968a1e65ca303c..66b3f9e37f9ed4f40a16d2dbf7b0679500ab2062 100644 GIT binary patch delta 137 zcmdnW_L4>F)W2Q(7#J8#7!)`em>I;m7+4r2*cl|*8Kfslr7_A*Z0wo5gVBOfZt_P) zBSx;t;!N@^@{9~h6VED5j$ul3RbpTQLIwsdE$yugj9S|nm^K1=j0_?`k_|{RFt7vV dMS(OEgBSxpkQM^6co}3E_<(F?AWMpY0RTvW6XpN_ delta 294 zcmaFKvXxEh)W2Q(7#J8#7*shKm>Fcb7+4tO*cs&685AZ;r7){G2dsG2GZU>Z#(o{<%| z2??>b(*tXRkYJ|uWNt<)7G*{T-HB(FfClkSZevCfjnjg5g^INzz8JS8AO4k7(^A2mH_gA>KS+#1c36AKsFCp9T!ke3dmz( bkOq@74E#V^2*~GUP-Nf(vYCM_aRvqek`g%L diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$Inner.class b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$Inner.class index f8f013c31dc7a0a8a9a14ca8532aabf6ef0e8143..06b61f90038acfbc54339a7b3a9d6161d46b0313 100644 GIT binary patch delta 149 zcmZo;yTD>{>ff$?3=9k=3<{hK%nTA-3@i+i>6C$YFV zwV0hjcB0AI$(@WA>~ic3@{9~hlbDnyzhYeJs>HwqgbWN^TH0F~7`3)DFl_|#7#T!? mBpZ-s09wGrAO@tF7{q}h3=Bd*7Bhns11pft4rFmKFaQ9)#1@+X delta 271 zcmcb>(#B?T>ff$?3=9k=462+A%nY(z3@i+C>6C$YFV zwV0hjX`;zlIU%3?Kxl83frGL?()cO_pIyWE7oT$EZ88U3T(n#z+TQ z21X!cU|`kS&cL`4$Y5mP29j)GK^dTCHXx6Qfro(?O!F}a18FXxEE9tOgAfA;0Fm_$ AVE_OC delta 219 zcmdnM{DMXF)W2Q(7#J8#7^Jxvm>I;_86?;lBqxf7NeTJnCnx5FB^G5SCgr4tfCxqg zmXeIj;)y@xnY4T+UeJ)UW@HdURaRL5Q>qVA!DbT@YHepdF*BJ_YT{Yl$>NNWDUJ+` zK*+$rsS)WyUg&cMgO0RSqTCtLsk diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses.class b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses.class index 0201730abf52c73e38ea0abf9e0a8fecf2edaab7..893ee3839437772183b7c67356b851ecbaa1384f 100644 GIT binary patch delta 119 zcmcc4v7KGw)W2Q(7#J8#7*x3!m>J~Q8RXd+6xbOQCrZc*D={+gxTof&7G)-T<^d^o z2IYxf#f&N&_enEu4rOX%G>~Or1VRP|R;}#}j2nRrMg}P$$p#i=1RBT-HDW8C2LARM{ESCQ8T)t1~k2xTof&7G)-T<^d^o z291ec#f+L8_enF#3i;$GC+37D7G)+T<)nsy2u22$l8nq^Mh3Y_jIy%Uj0|F^YAOq0 z>XaujDluAbzRuXe7~;sl2!sp_tXkU{7&ihL%nVXMk_{}#$RG`5^FS0Z$S}wPd2%Qs X@<1Ll122$dVo+dE1k*~B` { class GenericInnerInner{ } + + class ShadowingGenericInner { + U shadowedField; + } + + ShadowingGenericInner shadowingField; } static class StaticInner{ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp index 4d135ff4121..81bf5374810 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp @@ -17,6 +17,7 @@ SCENARIO( const symbol_tablet &new_symbol_table = load_java_class( "GenericClassWithInnerClasses", "./java_bytecode/java_bytecode_parse_generics"); + namespacet ns{new_symbol_table}; std::string outer_class_name = "GenericClassWithInnerClasses"; std::string outer_class_prefix = "java::" + outer_class_name; @@ -49,13 +50,59 @@ SCENARIO( } THEN("There is a field f3 of generic type with correct arguments") { + std::string inner_class_prefix = outer_class_prefix + "$GenericInner"; const auto &field = require_type::require_component(generic_class, "f3"); - require_type::require_pointer_to_tag( - field.type(), outer_class_prefix + "$GenericInner"); - require_type::require_java_generic_type( - field.type(), - {{require_type::type_argument_kindt::Var, outer_class_prefix + "::T"}, - {require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}}); + const auto &field_type = + require_type::require_pointer_to_tag(field.type(), inner_class_prefix); + java_generic_struct_tag_typet inner_class_tag = + require_type::require_java_generic_struct_tag_type( + field_type.subtype(), + inner_class_prefix, + { + {require_type::type_argument_kindt::Var, + outer_class_prefix + "::T"}, + {require_type::type_argument_kindt::Inst, + "java::java.lang.Integer"}, + }); + const java_generic_class_typet &inner_class = + require_type::require_complete_java_generic_class( + ns.follow_tag(inner_class_tag), {inner_class_prefix + "::U"}); + THEN( + "There is a field shadowingField of generic type with correct " + "arguments") + { + std::string shadowing_inner_class_prefix = + inner_class_prefix + "$ShadowingGenericInner"; + const auto &shadowing_field = + require_type::require_component(inner_class, "shadowingField"); + const auto &shadowing_field_type = require_type::require_pointer_to_tag( + shadowing_field.type(), shadowing_inner_class_prefix); + java_generic_struct_tag_typet shadowing_inner_class_tag = + require_type::require_java_generic_struct_tag_type( + shadowing_field_type.subtype(), + shadowing_inner_class_prefix, + { + {require_type::type_argument_kindt::Var, + inner_class_prefix + "::" + outer_class_name + "::T"}, + {require_type::type_argument_kindt::Var, + inner_class_prefix + "::U"}, + {require_type::type_argument_kindt::Inst, + "java::java.lang.String"}, + }); + const java_generic_class_typet &shadowing_inner_class = + require_type::require_complete_java_generic_class( + ns.follow_tag(shadowing_inner_class_tag), + {shadowing_inner_class_prefix + "::U"}); + THEN( + "There is a field shadowedField which is the generic parameter of " + "the inner class") + { + const auto &shadowed_field = require_type::require_component( + shadowing_inner_class, "shadowedField"); + require_type::require_java_generic_parameter( + shadowed_field.type(), shadowing_inner_class_prefix + "::U"); + } + } } } @@ -183,6 +230,26 @@ SCENARIO( {require_type::type_argument_kindt::Var, generic_inner_class_prefix + "::U"}}); } + THEN( + "There is a field shadowingField of generic type with a generic " + "type argument of String") + { + std::string shadowing_inner_class_prefix = + generic_inner_class_prefix + "$ShadowingGenericInner"; + const auto &field = + require_type::require_component(generic_class, "shadowingField"); + require_type::require_pointer_to_tag( + field.type(), shadowing_inner_class_prefix); + require_type::require_java_generic_type( + field.type(), + { + {require_type::type_argument_kindt::Var, + generic_inner_class_prefix + "::" + outer_class_name + "::T"}, + {require_type::type_argument_kindt::Var, + generic_inner_class_prefix + "::U"}, + {require_type::type_argument_kindt::Inst, "java::java.lang.String"}, + }); + } } }