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 6cd20b1508b..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( @@ -151,6 +123,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,10 +131,10 @@ 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"); - 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 b736e71beac..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,15 +14,19 @@ /// 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. - /// \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) { } @@ -31,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 @@ -49,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_bytecode_convert_class.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_class.cpp index c6387db44e9..b2028ca88b0 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 @@ -989,6 +990,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,39 +1019,31 @@ 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_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) - { - 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; + [¶meter_name](const java_generic_parametert &replacement_param) { + return parameter_name == + 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_p != replacement_parameters.end()) - { - const std::string &replacement_parameter_full_name = - id2string(replacement_parameter_p->type_variable().get_identifier()); - - // 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); - - 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()); + + // 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); } /// Recursively find all generic type parameters of a given type and replace @@ -1136,12 +1139,13 @@ 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 - // during parsing + // during parsing bool no_this_field = std::none_of( class_type.components().begin(), class_type.components().end(), @@ -1158,7 +1162,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 = @@ -1171,14 +1175,21 @@ 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("$"); + outer_class_delimiter = outer_class_name.rfind('$'); } else { @@ -1191,19 +1202,32 @@ 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()) + // 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( 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; } } 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/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..b93060269d1 100644 --- a/jbmc/src/java_bytecode/select_pointer_type.cpp +++ b/jbmc/src/java_bytecode/select_pointer_type.cpp @@ -20,192 +20,61 @@ 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 { - 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(); + 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 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; - } - else if(pointer_type.subtype().id() == ID_struct_tag) - { - // 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 typet &array_element_type = java_array_element_type(array_subtype); - if(array_element_type.id() == ID_pointer) + const optionalt specialization = + spec_map_copy.pop(parameter_name); + if(!specialization) { - 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; + // 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; } - } - } - 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; + if(!is_java_generic_parameter(*specialization)) + return *specialization; + parameter_name = to_java_generic_parameter(*specialization).get_name(); } - 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()) + auto subtype = + type_try_dynamic_cast(pointer_type.subtype()); + if(subtype != nullptr && is_java_array_tag(subtype->get_identifier())) { - return {}; - } + // 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) + return pointer_type; - const size_t index = (replacements.size() - 1) - depth; - const auto &type = replacements[index]; + const pointer_typet &new_array_type = specialize_generics( + *array_element_type, generic_parameter_specialization_map); - if(!is_java_generic_parameter(type)) - { - return type; + pointer_typet replacement_array_type = java_array_type('a'); + replacement_array_type.subtype().set(ID_element_type, new_array_type); + return replacement_array_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; + return pointer_type; } std::set 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-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp index 019a73efcb1..b29b7790924 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); @@ -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; } @@ -477,7 +472,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()); 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 00000000000..28c48051216 Binary files /dev/null and b/jbmc/unit/java_bytecode/goto_program_generics/Bar.class differ diff --git a/jbmc/unit/java_bytecode/goto_program_generics/Foo.class b/jbmc/unit/java_bytecode/goto_program_generics/Foo.class new file mode 100644 index 00000000000..ad11b6646f3 Binary files /dev/null and b/jbmc/unit/java_bytecode/goto_program_generics/Foo.class differ diff --git a/jbmc/unit/java_bytecode/goto_program_generics/KeyValue.class b/jbmc/unit/java_bytecode/goto_program_generics/KeyValue.class index d093b949329..cf2db1a9f15 100644 Binary files a/jbmc/unit/java_bytecode/goto_program_generics/KeyValue.class and b/jbmc/unit/java_bytecode/goto_program_generics/KeyValue.class differ diff --git a/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.class b/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.class index ed2b3621526..d15be56452a 100644 Binary files a/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.class and b/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.class differ diff --git a/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.java b/jbmc/unit/java_bytecode/goto_program_generics/MutuallyRecursiveGenerics.java index 55dea15389b..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; } @@ -20,10 +20,18 @@ class KeyValue { 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 136c195e97d..891911ec9c6 100644 Binary files a/jbmc/unit/java_bytecode/goto_program_generics/Outer$Inner.class and b/jbmc/unit/java_bytecode/goto_program_generics/Outer$Inner.class differ diff --git a/jbmc/unit/java_bytecode/goto_program_generics/Outer.class b/jbmc/unit/java_bytecode/goto_program_generics/Outer.class index 06ce8540988..0cb609e46b0 100644 Binary files a/jbmc/unit/java_bytecode/goto_program_generics/Outer.class and b/jbmc/unit/java_bytecode/goto_program_generics/Outer.class differ diff --git a/jbmc/unit/java_bytecode/goto_program_generics/Three.class b/jbmc/unit/java_bytecode/goto_program_generics/Three.class index 3921f569040..69350f1c8d6 100644 Binary files a/jbmc/unit/java_bytecode/goto_program_generics/Three.class and b/jbmc/unit/java_bytecode/goto_program_generics/Three.class differ 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..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 @@ -297,6 +297,106 @@ 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 = + 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 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 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 0384e7e6860..a15be1947c2 100644 Binary files a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner$GenericInnerInner.class and b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner$GenericInnerInner.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner$ShadowingGenericInner.class b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner$ShadowingGenericInner.class new file mode 100644 index 00000000000..8e388ea8185 Binary files /dev/null and b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner$ShadowingGenericInner.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner.class b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner.class index 8470c58c2d5..7cbccef8015 100644 Binary files a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner.class and b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner.class differ 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 82c05531a80..66b3f9e37f9 100644 Binary files a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$Inner$InnerInner.class and b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$Inner$InnerInner.class differ 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 f8f013c31dc..06b61f90038 100644 Binary files a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$Inner.class and b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$Inner.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$StaticInner.class b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$StaticInner.class index b7001714a64..7c3a69137cf 100644 Binary files a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$StaticInner.class and b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$StaticInner.class differ 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 0201730abf5..893ee383943 100644 Binary files a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses.class and b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses.class differ diff --git a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses.java b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses.java index f62932fcaf9..598e23b34c7 100644 --- a/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses.java +++ b/jbmc/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses.java @@ -17,6 +17,12 @@ class GenericInner { class GenericInnerInner{ } + + class ShadowingGenericInner { + U shadowedField; + } + + ShadowingGenericInner shadowingField; } static class StaticInner{ 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..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,8 +17,10 @@ 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_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") { @@ -48,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"); + } + } } } @@ -69,7 +117,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 +126,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 +137,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 +154,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 +163,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 +183,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 +199,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 +212,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 +226,29 @@ 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"}}); + } + 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"}, + }); } } } @@ -194,7 +267,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"}); } 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; 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()) {