diff --git a/jbmc/src/java_bytecode/java_types.h b/jbmc/src/java_bytecode/java_types.h index c0b0eb75b86..55e48d28f4d 100644 --- a/jbmc/src/java_bytecode/java_types.h +++ b/jbmc/src/java_bytecode/java_types.h @@ -407,21 +407,21 @@ bool equal_java_types(const typet &type1, const typet &type2); /// Class to hold a Java generic type parameter (also called type variable), /// e.g., `T` in `List`. /// The bound can specify type requirements. -class java_generic_parametert:public reference_typet +class java_generic_parameter_tagt : public struct_tag_typet { public: typedef struct_tag_typet type_variablet; - java_generic_parametert( + java_generic_parameter_tagt( const irep_idt &_type_var_name, const struct_tag_typet &_bound) - : reference_typet(java_reference_type(_bound)) + : struct_tag_typet(_bound) { set(ID_C_java_generic_parameter, true); type_variables().push_back(struct_tag_typet(_type_var_name)); } - /// \return the type variable as symbol type + /// \return the type variable as struct tag type const type_variablet &type_variable() const { PRECONDITION(!type_variables().empty()); @@ -431,7 +431,7 @@ class java_generic_parametert:public reference_typet type_variablet &type_variable_ref() { PRECONDITION(!type_variables().empty()); - return const_cast(type_variables().front()); + return type_variables().front(); } const irep_idt get_name() const @@ -452,13 +452,72 @@ class java_generic_parametert:public reference_typet } }; +/// 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 tag type +inline bool is_java_generic_parameter_tag(const typet &type) +{ + return type.get_bool(ID_C_java_generic_parameter); +} + +/// \param type: source type +/// \return cast of type into a java_generic_parametert +inline const java_generic_parameter_tagt & +to_java_generic_parameter_tag(const typet &type) +{ + PRECONDITION(is_java_generic_parameter_tag(type)); + return static_cast(type); +} + +/// \param type: source type +/// \return cast of type into a java_generic_parameter_tag +inline java_generic_parameter_tagt &to_java_generic_parameter_tag(typet &type) +{ + PRECONDITION(is_java_generic_parameter_tag(type)); + return static_cast(type); +} + +/// Reference that points to a java_generic_parameter_tagt. All information is +/// stored on the underlying tag. +class java_generic_parametert : public reference_typet +{ +public: + typedef struct_tag_typet type_variablet; + + java_generic_parametert( + const irep_idt &_type_var_name, + const struct_tag_typet &_bound) + : reference_typet(java_reference_type( + java_generic_parameter_tagt(_type_var_name, _bound))) + { + } + + /// \return the type variable as symbol type + const type_variablet &type_variable() const + { + return to_java_generic_parameter_tag(subtype()).type_variable(); + } + + type_variablet &type_variable_ref() + { + return to_java_generic_parameter_tag(subtype()).type_variable_ref(); + } + + const irep_idt get_name() const + { + return to_java_generic_parameter_tag(subtype()).get_name(); + } +}; + /// 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 type.get_bool(ID_C_java_generic_parameter); + return type.id() == ID_pointer && + is_java_generic_parameter_tag(type.subtype()); } /// \param type: source type @@ -493,36 +552,92 @@ inline java_generic_parametert &to_java_generic_parameter(typet &type) /// - in `HashMap, V>` it would contain two elements, the first of /// type `java_generic_typet` and the second of type /// `java_generic_parametert`. +class java_generic_struct_tag_typet : public struct_tag_typet +{ +public: + typedef std::vector generic_typest; + + explicit java_generic_struct_tag_typet(const struct_tag_typet &type) + : struct_tag_typet(type) + { + set(ID_C_java_generic_symbol, true); + } + + java_generic_struct_tag_typet( + const struct_tag_typet &type, + const std::string &base_ref, + const std::string &class_name_prefix); + + const generic_typest &generic_types() const + { + return (const generic_typest &)(find(ID_generic_types).get_sub()); + } + + generic_typest &generic_types() + { + return (generic_typest &)(add(ID_generic_types).get_sub()); + } + + optionalt + generic_type_index(const java_generic_parametert &type) const; +}; + +/// \param type: the type to check +/// \return true if the type is a symbol type with generics +inline bool is_java_generic_struct_tag_type(const typet &type) +{ + return type.get_bool(ID_C_java_generic_symbol); +} + +/// \param type: the type to convert +/// \return the converted type +inline const java_generic_struct_tag_typet & +to_java_generic_struct_tag_type(const typet &type) +{ + PRECONDITION(is_java_generic_struct_tag_type(type)); + return static_cast(type); +} + +/// \param type: the type to convert +/// \return the converted type +inline java_generic_struct_tag_typet & +to_java_generic_struct_tag_type(typet &type) +{ + PRECONDITION(is_java_generic_struct_tag_type(type)); + return static_cast(type); +} + +/// Reference that points to a java_generic_struct_tag_typet. All information is +/// stored on the underlying tag. class java_generic_typet:public reference_typet { public: - typedef std::vector generic_type_argumentst; + typedef java_generic_struct_tag_typet::generic_typest generic_type_argumentst; - explicit java_generic_typet(const typet &_type): - reference_typet(java_reference_type(_type)) + explicit java_generic_typet(const typet &_type) + : reference_typet(java_reference_type( + java_generic_struct_tag_typet(to_struct_tag_type(_type)))) { - set(ID_C_java_generic_type, true); } /// \return vector of type variables const generic_type_argumentst &generic_type_arguments() const { - return (const generic_type_argumentst &)( - find(ID_type_variables).get_sub()); + return to_java_generic_struct_tag_type(subtype()).generic_types(); } /// \return vector of type variables generic_type_argumentst &generic_type_arguments() { - return (generic_type_argumentst &)( - add(ID_type_variables).get_sub()); + return to_java_generic_struct_tag_type(subtype()).generic_types(); } }; template <> inline bool can_cast_type(const typet &type) { - return is_reference(type) && type.get_bool(ID_C_java_generic_type); + return is_reference(type) && + type.subtype().get_bool(ID_C_java_generic_symbol); } /// \param type: the type to check @@ -761,58 +876,6 @@ void get_dependencies_from_generic_parameters( const typet &, std::set &); -/// Type for a generic symbol, extends struct_tag_typet with a -/// vector of java generic types. -/// This is used to store the type of generic superclasses and interfaces. -class java_generic_struct_tag_typet : public struct_tag_typet -{ -public: - typedef std::vector generic_typest; - - java_generic_struct_tag_typet( - const struct_tag_typet &type, - const std::string &base_ref, - const std::string &class_name_prefix); - - const generic_typest &generic_types() const - { - return (const generic_typest &)(find(ID_generic_types).get_sub()); - } - - generic_typest &generic_types() - { - return (generic_typest &)(add(ID_generic_types).get_sub()); - } - - optionalt - generic_type_index(const java_generic_parametert &type) const; -}; - -/// \param type: the type to check -/// \return true if the type is a symbol type with generics -inline bool is_java_generic_struct_tag_type(const typet &type) -{ - return type.get_bool(ID_C_java_generic_symbol); -} - -/// \param type: the type to convert -/// \return the converted type -inline const java_generic_struct_tag_typet & -to_java_generic_struct_tag_type(const typet &type) -{ - PRECONDITION(is_java_generic_struct_tag_type(type)); - return static_cast(type); -} - -/// \param type: the type to convert -/// \return the converted type -inline java_generic_struct_tag_typet & -to_java_generic_struct_tag_type(typet &type) -{ - PRECONDITION(is_java_generic_struct_tag_type(type)); - return static_cast(type); -} - /// Take a signature string and remove everything in angle brackets allowing for /// the type to be parsed normally, for example /// `java.util.HashSet` will be turned into diff --git a/jbmc/unit/java-testing-utils/require_type.cpp b/jbmc/unit/java-testing-utils/require_type.cpp index 818299aafaa..52b02439eff 100644 --- a/jbmc/unit/java-testing-utils/require_type.cpp +++ b/jbmc/unit/java-testing-utils/require_type.cpp @@ -140,7 +140,9 @@ bool require_java_generic_type_argument_expectation( case require_type::type_argument_kindt::Inst: { REQUIRE(!is_java_generic_parameter(type_argument)); - REQUIRE(type_argument.subtype() == struct_tag_typet(expected.description)); + REQUIRE( + to_struct_tag_type(type_argument.subtype()).get_identifier() == + expected.description); return true; } } diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index c02d9a6935e..17554082981 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -649,11 +649,10 @@ IREP_ID_ONE(switch_case_number) IREP_ID_ONE(java_array_access) IREP_ID_ONE(java_member_access) IREP_ID_TWO(C_java_generic_parameter, #java_generic_parameter) -IREP_ID_TWO(C_java_generic_type, #java_generic_type) IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type) IREP_ID_TWO(C_java_implicitly_generic_class_type, #java_implicitly_generic_class_type) IREP_ID_TWO(C_java_generic_symbol, #java_generic_symbol) -IREP_ID_TWO(generic_types, #generic_types) +IREP_ID_ONE(generic_types) IREP_ID_TWO(implicit_generic_types, #implicit_generic_types) IREP_ID_ONE(type_variables) IREP_ID_TWO(java_lambda_method_handle_index, lambda_method_handle_index)