diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index e6302f82dcd..fa1dbc19636 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -27,6 +27,7 @@ Author: Daniel Kroening, kroening@kroening.com #include #include +#include class java_bytecode_convert_classt:public messaget { @@ -85,6 +86,83 @@ class java_bytecode_convert_classt:public messaget static void add_array_types(symbol_tablet &symbol_table); }; +/// Auxiliary function to extract the generic superclass reference from the +/// class signature. If the signature is empty or the superclass is not generic +/// it returns empty. +/// Example: +/// - class: A extends B implements C, D +/// - signature: B;LC;LD; +/// - returned superclass reference: B; +/// \param signature Signature of the class +/// \return Reference of the generic superclass, or empty if the superclass +/// is not generic +static optionalt +extract_generic_superclass_reference(const optionalt &signature) +{ + if(signature.has_value()) + { + // skip the (potential) list of generic parameters at the beginning of the + // signature + const size_t start = + signature.value().front() == '<' + ? find_closing_delimiter(signature.value(), 0, '<', '>') + 1 + : 0; + + // extract the superclass reference + const size_t end = + find_closing_semi_colon_for_reference_type(signature.value(), start); + const std::string superclass_ref = + signature.value().substr(start, (end - start) + 1); + + // if the superclass is generic then the reference is of form + // Lsuperclass-name; + if(has_suffix(superclass_ref, ">;")) + return superclass_ref; + } + return {}; +} + +/// Auxiliary function to extract the generic interface reference of an +/// interface with the specified name from the class signature. If the +/// signature is empty or the interface is not generic it returns empty. +/// Example: +/// - class: A extends B implements C, D +/// - signature: B;LC;LD; +/// - returned interface reference for C: LC; +/// - returned interface reference for D: LD; +/// \param signature Signature of the class +/// \param interface_name The interface name +/// \return Reference of the generic interface, or empty if the interface +/// is not generic +static optionalt extract_generic_interface_reference( + const optionalt &signature, + const std::string &interface_name) +{ + if(signature.has_value()) + { + // skip the (potential) list of generic parameters at the beginning of the + // signature + size_t start = + signature.value().front() == '<' + ? find_closing_delimiter(signature.value(), 0, '<', '>') + 1 + : 0; + + // skip the superclass reference (if there is at least one interface + // reference in the signature, then there is a superclass reference) + start = + find_closing_semi_colon_for_reference_type(signature.value(), start) + 1; + + start = signature.value().find("L" + interface_name + "<", start); + if(start != std::string::npos) + { + const size_t &end = + find_closing_semi_colon_for_reference_type(signature.value(), start); + return signature.value().substr(start, (end - start) + 1); + } + } + return {}; +} + void java_bytecode_convert_classt::convert(const classt &c) { std::string qualified_classname="java::"+id2string(c.name); @@ -145,10 +223,26 @@ void java_bytecode_convert_classt::convert(const classt &c) if(!c.extends.empty()) { - symbol_typet base("java::"+id2string(c.extends)); - class_type.add_base(base); + const symbol_typet base("java::" + id2string(c.extends)); + + // if the superclass is generic then the class has the superclass reference + // including the generic info in its signature + // e.g., signature for class 'A' that extends + // 'Generic' is 'LGeneric;' + const optionalt &superclass_ref = + extract_generic_superclass_reference(c.signature); + if(superclass_ref.has_value()) + { + const java_generic_symbol_typet generic_base( + base, superclass_ref.value(), qualified_classname); + class_type.add_base(generic_base); + } + else + { + class_type.add_base(base); + } class_typet::componentt base_class_field; - base_class_field.type()=base; + base_class_field.type() = class_type.bases().at(0).type(); base_class_field.set_name("@"+id2string(c.extends)); base_class_field.set_base_name("@"+id2string(c.extends)); base_class_field.set_pretty_name("@"+id2string(c.extends)); @@ -158,8 +252,24 @@ void java_bytecode_convert_classt::convert(const classt &c) // interfaces are recorded as bases for(const auto &interface : c.implements) { - symbol_typet base("java::"+id2string(interface)); - class_type.add_base(base); + const symbol_typet base("java::" + id2string(interface)); + + // if the interface is generic then the class has the interface reference + // including the generic info in its signature + // e.g., signature for class 'A implements GenericInterface' is + // 'Ljava/lang/Object;LGenericInterface;' + const optionalt interface_ref = + extract_generic_interface_reference(c.signature, id2string(interface)); + if(interface_ref.has_value()) + { + const java_generic_symbol_typet generic_base( + base, interface_ref.value(), qualified_classname); + class_type.add_base(generic_base); + } + else + { + class_type.add_base(base); + } } // produce class symbol @@ -598,6 +708,15 @@ static void find_and_replace_parameters( find_and_replace_parameters(argument, replacement_parameters); } } + else if(is_java_generic_symbol_type(type)) + { + java_generic_symbol_typet &generic_base = to_java_generic_symbol_type(type); + std::vector &gen_types = generic_base.generic_types(); + for(auto &gen_type : gen_types) + { + find_and_replace_parameters(gen_type, replacement_parameters); + } + } } /// Checks if the class is implicitly generic, i.e., it is an inner class of @@ -675,5 +794,11 @@ void mark_java_implicitly_generic_class_type( find_and_replace_parameters( field.type(), implicit_generic_type_parameters); } + + for(auto &base : class_type.bases()) + { + find_and_replace_parameters( + base.type(), implicit_generic_type_parameters); + } } } diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index 925640e5a09..043eb5abca8 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -522,6 +522,65 @@ to_java_specialized_generic_class_type(typet &type) return static_cast(type); } +/// Type for a generic symbol, extends symbol_typet with a +/// vector of java generic types. +/// This is used to store the type of generic superclasses and interfaces. +class java_generic_symbol_typet : public symbol_typet +{ +public: + typedef std::vector generic_typest; + + java_generic_symbol_typet( + const symbol_typet &type, + const std::string &base_ref, + const std::string &class_name_prefix) + : symbol_typet(type) + { + set(ID_C_java_generic_symbol, true); + const typet &base_type = java_type_from_string(base_ref, class_name_prefix); + PRECONDITION(is_java_generic_type(base_type)); + const java_generic_typet gen_base_type = to_java_generic_type(base_type); + generic_types().insert( + generic_types().end(), + gen_base_type.generic_type_arguments().begin(), + gen_base_type.generic_type_arguments().end()); + } + + 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()); + } +}; + +/// \param type: the type to check +/// \return true if the type is a symbol type with generics +inline bool is_java_generic_symbol_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_symbol_typet & +to_java_generic_symbol_type(const typet &type) +{ + PRECONDITION(is_java_generic_symbol_type(type)); + return static_cast(type); +} + +/// \param type: the type to convert +/// \return the converted type +inline java_generic_symbol_typet &to_java_generic_symbol_type(typet &type) +{ + PRECONDITION(is_java_generic_symbol_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/src/util/irep_ids.def b/src/util/irep_ids.def index 0b134e536c6..8fc363886d1 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -832,6 +832,7 @@ IREP_ID_TWO(C_java_generic_type, #java_generic_type) IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type) IREP_ID_TWO(C_specialized_generic_java_class, #specialized_generic_java_class) 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_TWO(implicit_generic_types, #implicit_generic_types) IREP_ID_TWO(type_variables, #type_variables) diff --git a/unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClass$InnerClass.class b/unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClass$InnerClass.class new file mode 100644 index 00000000000..f3595751537 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClass$InnerClass.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClass$InnerClassGeneric.class b/unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClass$InnerClassGeneric.class new file mode 100644 index 00000000000..09cf119f8b2 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClass$InnerClassGeneric.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClass.class b/unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClass.class new file mode 100644 index 00000000000..55b7569f8cf Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClass.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClassGeneric$InnerClass.class b/unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClassGeneric$InnerClass.class new file mode 100644 index 00000000000..4070754058f Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClassGeneric$InnerClass.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClassGeneric.class b/unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClassGeneric.class new file mode 100644 index 00000000000..94e68d33065 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClassGeneric.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericInst.class b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericInst.class index f5a72b7d0a5..9b796c9b9a4 100644 Binary files a/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericInst.class and b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericInst.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericInst.java b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericInst.java deleted file mode 100644 index b2a41911694..00000000000 --- a/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericInst.java +++ /dev/null @@ -1,4 +0,0 @@ -class DerivedGenericInst extends Generic -{ - -} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericInst2.class b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericInst2.class new file mode 100644 index 00000000000..d9f9cd5c25e Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericInst2.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericMixed1.class b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericMixed1.class new file mode 100644 index 00000000000..8b0a137c161 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericMixed1.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericMixed2.class b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericMixed2.class new file mode 100644 index 00000000000..e191040cc9d Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericMixed2.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericUninst.class b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericUninst.class index 437daa77f9c..67929447c97 100644 Binary files a/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericUninst.class and b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericUninst.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericUninst.java b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericUninst.java deleted file mode 100644 index 88dcb1c9250..00000000000 --- a/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericUninst.java +++ /dev/null @@ -1,4 +0,0 @@ -class DerivedGenericUninst extends Generic -{ - -} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenerics.class b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenerics.class new file mode 100644 index 00000000000..bd6fb9644fe Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenerics.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenerics.java b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenerics.java new file mode 100644 index 00000000000..6492f0d49dc --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenerics.java @@ -0,0 +1,171 @@ +public class DerivedGenerics { + DerivedGenericInst new1; + DerivedGenericInst2 new2; + DerivedGenericUninst new3; + DerivedGenericMixed1 new4; + DerivedGenericMixed2 new5; + ContainsInnerClass new6; + ContainsInnerClassGeneric new7; + ThreeHierarchy new8; + ImplementsInterfaceGenericSpecialised new9; + ImplementsInterfaceGenericUnspec new10; + ImplementsMultipleInterfaces new11; + ExtendsAndImplements new12; + ExtendsAndImplementsGeneric new13; + ExtendsAndImplementsSameInterface new14; + ExtendsAndImplementsSameInterface2 new15; + ExtendsAndImplementsSameInterfaceGeneric new16; +} + +class DerivedGenericInst extends Generic +{ + // This class is to test instantiating a non-generic subclass of a generic class + // with the base class having only one type parameter. +} + +class DerivedGenericInst2 extends +GenericTwoParam +{ + // This class is to test instantiating a non-generic subclass of a generic class + // with the base class having two type parameters. +} + +class DerivedGenericUninst extends Generic +{ + T newField; + + // This class is to test instantiating a generic subclass of a generic class + // with the base class having only one parameter, but the type parameter is + // not specialised. +} + +class DerivedGenericMixed1 extends Generic +{ + T newField; + + // This class is to test instantiating a generic subclass of a generic class + // with the base class having only one type parameter. +} + +class DerivedGenericMixed2 extends GenericTwoParam +{ + T newField; + + // This class is to test instantiating a generic subclass of a generic class + // with the base class having two type parameters, where one is specialised + // and the other is not. +} + +class ContainsInnerClass { + + InnerClass ic; + InnerClassGeneric icg; + + // This class is to test inner classes that extend generic types. + class InnerClass extends Generic { + } + + class InnerClassGeneric extends Generic { + } +} + +class ContainsInnerClassGeneric { + + InnerClass ic; + + // This class is to test inner classes that extend generic types when the + // outer class in generic. + class InnerClass extends Generic { + } +} + +class ThreeHierarchy extends DerivedGenericMixed2 { + + // This class extends a specialised class that extends another generic + // class. + +} + +class ImplementsInterfaceGenericSpecialised implements InterfaceGeneric + { + + public Integer someMethod() { + return 0; + } + +} + +class ImplementsInterfaceGenericUnspec implements InterfaceGeneric { + + public E someMethod() { + return null; + } + +} + +class ImplementsMultipleInterfaces implements +InterfaceGeneric, Interface +{ + + public Integer someMethod() { + return 0; + } + + public int getX() { + return 0; + } +} + +class ExtendsAndImplements extends Generic implements Interface, +InterfaceGeneric +{ + public Integer someMethod() { + return 0; + } + + public int getX() { + return 0; + } +} + +class ExtendsAndImplementsGeneric extends GenericTwoParam +implements Interface, +InterfaceGeneric +{ + T f; + + public T someMethod() { + return f; + } + + public int getX() { + return 0; + } +} + +class ExtendsAndImplementsSameInterface extends Generic +implements InterfaceGeneric +{ + public Integer someMethod() { + return 0; + } +} + +class ExtendsAndImplementsSameInterface2 extends +Generic> +implements InterfaceGeneric +{ + public Integer someMethod() { + return 0; + } +} + +class ExtendsAndImplementsSameInterfaceGeneric extends +Generic implements InterfaceGeneric +{ + T f; + + public T someMethod() { + return f; + } +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplements.class b/unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplements.class new file mode 100644 index 00000000000..28afaa564af Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplements.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplementsGeneric.class b/unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplementsGeneric.class new file mode 100644 index 00000000000..13f542bf41e Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplementsGeneric.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplementsSameInterface.class b/unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplementsSameInterface.class new file mode 100644 index 00000000000..b1ec684caa6 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplementsSameInterface.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplementsSameInterface2.class b/unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplementsSameInterface2.class new file mode 100644 index 00000000000..d2483f17236 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplementsSameInterface2.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplementsSameInterfaceGeneric.class b/unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplementsSameInterfaceGeneric.class new file mode 100644 index 00000000000..9ac0eba44d3 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplementsSameInterfaceGeneric.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/ImplementsInterfaceGenericSpecialised.class b/unit/java_bytecode/java_bytecode_parse_generics/ImplementsInterfaceGenericSpecialised.class new file mode 100644 index 00000000000..ea90de3f1fc Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/ImplementsInterfaceGenericSpecialised.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/ImplementsInterfaceGenericUnspec.class b/unit/java_bytecode/java_bytecode_parse_generics/ImplementsInterfaceGenericUnspec.class new file mode 100644 index 00000000000..2703a52e1aa Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/ImplementsInterfaceGenericUnspec.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/ImplementsMultipleInterfaces.class b/unit/java_bytecode/java_bytecode_parse_generics/ImplementsMultipleInterfaces.class new file mode 100644 index 00000000000..44e8a5bd84d Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/ImplementsMultipleInterfaces.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/Int.class b/unit/java_bytecode/java_bytecode_parse_generics/Int.class new file mode 100644 index 00000000000..981b3756769 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/Int.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/InterfaceGeneric.class b/unit/java_bytecode/java_bytecode_parse_generics/InterfaceGeneric.class new file mode 100644 index 00000000000..ab013e24537 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/InterfaceGeneric.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/InterfaceGeneric.java b/unit/java_bytecode/java_bytecode_parse_generics/InterfaceGeneric.java new file mode 100644 index 00000000000..cda3cfe57a4 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/InterfaceGeneric.java @@ -0,0 +1,4 @@ +interface InterfaceGeneric +{ + E someMethod(); +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/NotGeneric.class b/unit/java_bytecode/java_bytecode_parse_generics/NotGeneric.class new file mode 100644 index 00000000000..a478117ccf6 Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/NotGeneric.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/ThreeHierarchy.class b/unit/java_bytecode/java_bytecode_parse_generics/ThreeHierarchy.class new file mode 100644 index 00000000000..a3d28e0886d Binary files /dev/null and b/unit/java_bytecode/java_bytecode_parse_generics/ThreeHierarchy.class differ diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp index 1f83a68d6f7..6c00ae92065 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_derived_generic_class.cpp @@ -11,11 +11,11 @@ #include SCENARIO( - "parse_derived_generic_class_inst", + "parse_derived_generic_class", "[core][java_bytecode][java_bytecode_parse_generics]") { const symbol_tablet &new_symbol_table = load_java_class( - "DerivedGenericInst", "./java_bytecode/java_bytecode_parse_generics"); + "DerivedGenerics", "./java_bytecode/java_bytecode_parse_generics"); THEN("There should be a symbol for the DerivedGenericInst class") { @@ -26,17 +26,44 @@ SCENARIO( const class_typet &derived_class_type = require_type::require_java_non_generic_class(derived_symbol.type); - // TODO: Currently we do not support extracting information - // about the base classes generic information - issue TG-1287 + THEN("The base for superclass has the correct generic type information") + { + REQUIRE(derived_class_type.bases().size() == 1); + const typet &base_type = derived_class_type.bases().at(0).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::Generic", + {{require_type::type_argument_kindt::Inst, + "java::Interface_Implementation"}}); + } + + // TODO: Check that specialised superclass is created. TG-1419 } -} -SCENARIO( - "parse_derived_generic_class_uninst", - "[core][java_bytecode][java_bytecode_parse_generics]") -{ - const symbol_tablet &new_symbol_table = load_java_class( - "DerivedGenericUninst", "./java_bytecode/java_bytecode_parse_generics"); + THEN("There should be a symbol for the DerivedGenericInst2 class") + { + std::string class_prefix = "java::DerivedGenericInst2"; + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); + + const class_typet &derived_class_type = + require_type::require_java_non_generic_class(derived_symbol.type); + + THEN("The base for superclass has the correct generic type information") + { + REQUIRE(derived_class_type.bases().size() == 1); + const typet &base_type = derived_class_type.bases().at(0).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::GenericTwoParam", + {{require_type::type_argument_kindt::Inst, + "java::Interface_Implementation"}, + {require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}}); + } + + // TODO: Check that specialised superclass is created. TG-1419 + } THEN("There should be a symbol for the DerivedGenericUninst class") { @@ -44,11 +71,492 @@ SCENARIO( REQUIRE(new_symbol_table.has_symbol(class_prefix)); const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); - const java_generic_class_typet &derived_class_type = - require_type::require_java_generic_class( - derived_symbol.type, {class_prefix + "::T"}); - // TODO: Currently we do not support extracting information - // about the base classes generic information - issue TG-1287 + const class_typet &derived_class_type = + require_type::require_java_generic_class(derived_symbol.type); + + THEN("The base for superclasss has the correct generic type information") + { + REQUIRE(derived_class_type.bases().size() == 1); + const typet &base_type = derived_class_type.bases().at(0).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::Generic", + {{require_type::type_argument_kindt::Var, + "java::DerivedGenericUninst::T"}}); + } + + // TODO: Check that specialised superclass is created. TG-1418 + } + + THEN("There should be a symbol for the DerivedGenericMixed1 class") + { + std::string class_prefix = "java::DerivedGenericMixed1"; + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); + + const class_typet &derived_class_type = + require_type::require_java_generic_class(derived_symbol.type); + + THEN("The base for superclass has the correct generic type information") + { + REQUIRE(derived_class_type.bases().size() == 1); + const typet &base_type = derived_class_type.bases().at(0).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::Generic", + {{require_type::type_argument_kindt::Inst, + "java::Interface_Implementation"}}); + } + + // TODO: Check that specialised superclass is created. TG-1418, TG-1419 + } + + THEN("There should be a symbol for the DerivedGenericMixed2 class") + { + std::string class_prefix = "java::DerivedGenericMixed2"; + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); + + const class_typet &derived_class_type = + require_type::require_java_generic_class(derived_symbol.type); + + THEN("The base for superclass has the correct generic type information") + { + REQUIRE(derived_class_type.bases().size() == 1); + const typet &base_type = derived_class_type.bases().at(0).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::GenericTwoParam", + {{require_type::type_argument_kindt::Var, + "java::DerivedGenericMixed2::T"}, + {require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}}); + } + + // TODO: Check that specialised superclass is created. TG-1418, TG-1419 + } + + THEN("There should be a symbol for the ContainsInnerClass$InnerClass class") + { + std::string class_prefix = "java::ContainsInnerClass$InnerClass"; + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); + + const class_typet &derived_class_type = + require_type::require_java_non_generic_class(derived_symbol.type); + + THEN("The base for superclass has the correct generic type information") + { + REQUIRE(derived_class_type.bases().size() == 1); + const typet &base_type = derived_class_type.bases().at(0).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::Generic", + {{require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}}); + } + + // TODO: Check that specialised superclass is created. TG-1418, TG-1419 + } + + THEN( + "There should be a symbol for the ContainsInnerClass$InnerClassGeneric " + "class") + { + std::string class_prefix = "java::ContainsInnerClass$InnerClassGeneric"; + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); + + const class_typet &derived_class_type = + require_type::require_java_generic_class(derived_symbol.type); + + THEN("The base for superclass has the correct generic type information") + { + REQUIRE(derived_class_type.bases().size() == 1); + const typet &base_type = derived_class_type.bases().at(0).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::Generic", + {{require_type::type_argument_kindt::Var, + "java::ContainsInnerClass$InnerClassGeneric::T"}}); + } + + // TODO: Check that specialised superclass is created. TG-1418, TG-1419 + } + + THEN( + "There should be a symbol for the ContainsInnerClassGeneric$InnerClass" + "class") + { + std::string class_prefix = "java::ContainsInnerClassGeneric$InnerClass"; + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); + + const class_typet &derived_class_type = + require_type::require_java_implicitly_generic_class( + derived_symbol.type, {"java::ContainsInnerClassGeneric::T"}); + + THEN("The base for superclass has the correct generic type information") + { + REQUIRE(derived_class_type.bases().size() == 1); + const typet &base_type = derived_class_type.bases().at(0).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::Generic", + {{require_type::type_argument_kindt::Var, + "java::ContainsInnerClassGeneric::T"}}); + } + + // TODO: Check that specialised superclass is created. TG-1418, TG-1419 + } + + THEN("There should be a symbol for the ThreeHierarchy class") + { + std::string class_prefix = "java::ThreeHierarchy"; + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); + + const class_typet &derived_class_type = + require_type::require_java_non_generic_class(derived_symbol.type); + + THEN("The base for superclass has the correct generic type information") + { + REQUIRE(derived_class_type.bases().size() == 1); + const typet &base_type = derived_class_type.bases().at(0).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::DerivedGenericMixed2", + {{require_type::type_argument_kindt::Inst, "java::java.lang.String"}}); + } + + // TODO: Check that specialised superclass is created. TG-1418, TG-1419 + } + + THEN( + "There should be a symbol for the ImplementsInterfaceGenericSpecialised " + "class") + { + std::string class_prefix = "java::ImplementsInterfaceGenericSpecialised"; + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); + + const class_typet &derived_class_type = + require_type::require_java_non_generic_class(derived_symbol.type); + + THEN("The bases have the correct generic type information") + { + REQUIRE(derived_class_type.bases().size() == 2); + + THEN("The superclass is correct") + { + const typet &base_type = derived_class_type.bases().at(0).type(); + require_type::require_symbol(base_type, "java::java.lang.Object"); + } + THEN("The second interface is correct") + { + const typet &base_type = derived_class_type.bases().at(1).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::InterfaceGeneric", + {{require_type::type_argument_kindt::Inst, + "java::java.lang.Integer"}}); + } + } + + // TODO: Check that specialised superclass is created. TG-1418, TG-1419 + } + + THEN( + "There should be a symbol for the ImplementsInterfaceGenericUnspec class") + { + std::string class_prefix = "java::ImplementsInterfaceGenericUnspec"; + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); + + const class_typet &derived_class_type = + require_type::require_java_generic_class(derived_symbol.type); + + THEN("The bases have the correct generic type information") + { + REQUIRE(derived_class_type.bases().size() == 2); + + THEN("The superclass is correct") + { + const typet &base_type = derived_class_type.bases().at(0).type(); + require_type::require_symbol(base_type, "java::java.lang.Object"); + } + THEN("The second interface is correct") + { + const typet &base_type = derived_class_type.bases().at(1).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::InterfaceGeneric", + {{require_type::type_argument_kindt::Var, + "java::ImplementsInterfaceGenericUnspec::E"}}); + } + } + + // TODO: Check that specialised superclass is created. TG-1418, TG-1419 + } + + THEN( + "There should be a symbol for the " + "ImplementsMultipleInterfaces class") + { + std::string class_prefix = "java::ImplementsMultipleInterfaces"; + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); + + const class_typet &derived_class_type = + require_type::require_java_non_generic_class(derived_symbol.type); + + THEN("The bases have the correct generic type information") + { + REQUIRE(derived_class_type.bases().size() == 3); + + THEN("The superclass is correct") + { + const typet &base_type = derived_class_type.bases().at(0).type(); + require_type::require_symbol(base_type, "java::java.lang.Object"); + } + THEN("The second interface is correct") + { + const typet &base_type = derived_class_type.bases().at(1).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::InterfaceGeneric", + {{require_type::type_argument_kindt::Inst, + "java::java.lang.Integer"}}); + } + THEN("The first interface is correct") + { + const typet &base_type = derived_class_type.bases().at(2).type(); + require_type::require_symbol(base_type, "java::Interface"); + } + } + + // TODO: Check that specialised superclass is created. TG-1418, TG-1419 + } + + THEN( + "There should be a symbol for the " + "ExtendsAndImplements class") + { + std::string class_prefix = "java::ExtendsAndImplements"; + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); + + const class_typet &derived_class_type = + require_type::require_java_non_generic_class(derived_symbol.type); + + THEN("The bases have the correct generic type information") + { + REQUIRE(derived_class_type.bases().size() == 3); + + THEN("The superclass is correct") + { + const typet &base_type = derived_class_type.bases().at(0).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::Generic", + {{require_type::type_argument_kindt::Inst, + "java::java.lang.Integer"}}); + } + THEN("The first interface is correct") + { + const typet &base_type = derived_class_type.bases().at(1).type(); + require_type::require_symbol(base_type, "java::Interface"); + } + THEN("The second interface is correct") + { + const typet &base_type = derived_class_type.bases().at(2).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::InterfaceGeneric", + {{require_type::type_argument_kindt::Inst, + "java::java.lang.Integer"}}); + } + } + + // TODO: Check that specialised superclass is created. TG-1418, TG-1419 + } + + THEN( + "There should be a symbol for the " + "ExtendsAndImplementsGeneric class") + { + std::string class_prefix = "java::ExtendsAndImplementsGeneric"; + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); + + const class_typet &derived_class_type = + require_type::require_java_generic_class(derived_symbol.type); + + THEN("The bases have the correct generic type information") + { + REQUIRE(derived_class_type.bases().size() == 3); + + THEN("The superclass is correct") + { + const typet &base_type = derived_class_type.bases().at(0).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::GenericTwoParam", + {{require_type::type_argument_kindt::Var, + "java::ExtendsAndImplementsGeneric::T"}, + {require_type::type_argument_kindt::Inst, + "java::java.lang.Integer"}}); + } + THEN("The first interface is correct") + { + const typet &base_type = derived_class_type.bases().at(1).type(); + require_type::require_symbol(base_type, "java::Interface"); + } + THEN("The second interface is correct") + { + const typet &base_type = derived_class_type.bases().at(2).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::InterfaceGeneric", + {{require_type::type_argument_kindt::Var, + "java::ExtendsAndImplementsGeneric::T"}}); + } + } + + // TODO: Check that specialised superclass is created. TG-1418, TG-1419 + } + + THEN( + "There should be a symbol for the " + "ExtendsAndImplementsSameInterface class") + { + std::string class_prefix = "java::ExtendsAndImplementsSameInterface"; + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); + + const class_typet &derived_class_type = + require_type::require_java_non_generic_class(derived_symbol.type); + + THEN("The bases have the correct generic type information") + { + REQUIRE(derived_class_type.bases().size() == 2); + + THEN("The superclass is correct") + { + const typet &base_type = derived_class_type.bases().at(0).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::Generic", + {{require_type::type_argument_kindt::Inst, + "java::InterfaceGeneric"}}); + } + THEN("The interface is correct") + { + const typet &base_type = derived_class_type.bases().at(1).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::InterfaceGeneric", + {{require_type::type_argument_kindt::Inst, + "java::java.lang.Integer"}}); + } + } + + // TODO: Check that specialised superclass is created. TG-1418, TG-1419 + } + + THEN( + "There should be a symbol for the " + "ExtendsAndImplementsSameInterface2 class") + { + std::string class_prefix = "java::ExtendsAndImplementsSameInterface2"; + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); + + const class_typet &derived_class_type = + require_type::require_java_non_generic_class(derived_symbol.type); + + THEN("The bases have the correct generic type information") + { + REQUIRE(derived_class_type.bases().size() == 2); + + THEN("The superclass is correct") + { + const typet &base_type = derived_class_type.bases().at(0).type(); + const java_generic_symbol_typet &superclass_type = + require_type::require_java_generic_symbol_type( + base_type, + "java::Generic", + {{require_type::type_argument_kindt::Inst, + "java::InterfaceGeneric"}}); + + const typet &type_argument = superclass_type.generic_types().at(0); + require_type::require_java_generic_type( + type_argument, + {{require_type::type_argument_kindt::Inst, + "java::java.lang.String"}}); + } + THEN("The interface is correct") + { + const typet &base_type = derived_class_type.bases().at(1).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::InterfaceGeneric", + {{require_type::type_argument_kindt::Inst, + "java::java.lang.Integer"}}); + } + } + + // TODO: Check that specialised superclass is created. TG-1418, TG-1419 + } + + THEN( + "There should be a symbol for the " + "ExtendsAndImplementsSameInterfaceGeneric class") + { + std::string class_prefix = "java::ExtendsAndImplementsSameInterfaceGeneric"; + REQUIRE(new_symbol_table.has_symbol(class_prefix)); + + const symbolt &derived_symbol = new_symbol_table.lookup_ref(class_prefix); + + const class_typet &derived_class_type = + require_type::require_java_generic_class(derived_symbol.type); + + THEN("The bases have the correct generic type information") + { + REQUIRE(derived_class_type.bases().size() == 2); + + THEN("The superclass is correct") + { + const typet &base_type = derived_class_type.bases().at(0).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::Generic", + {{require_type::type_argument_kindt::Inst, + "java::InterfaceGeneric"}}); + } + THEN("The interface is correct") + { + const typet &base_type = derived_class_type.bases().at(1).type(); + require_type::require_java_generic_symbol_type( + base_type, + "java::InterfaceGeneric", + {{require_type::type_argument_kindt::Var, + "java::ExtendsAndImplementsSameInterfaceGeneric::T"}}); + } + } + + // TODO: Check that specialised superclass is created. TG-1418, TG-1419 } } diff --git a/unit/testing-utils/require_type.cpp b/unit/testing-utils/require_type.cpp index 0ddc11100ca..b849402483f 100644 --- a/unit/testing-utils/require_type.cpp +++ b/unit/testing-utils/require_type.cpp @@ -347,3 +347,50 @@ require_type::require_symbol(const typet &type, const irep_idt &identifier) } return result; } + +/// Verify a given type is a java generic symbol type +/// \param type The type to check +/// \param identifier The identifier to match +/// \return The type, cast to a java_generic_symbol_typet +java_generic_symbol_typet require_type::require_java_generic_symbol_type( + const typet &type, + const std::string &identifier) +{ + symbol_typet symbol_type = require_symbol(type, identifier); + REQUIRE(is_java_generic_symbol_type(type)); + return to_java_generic_symbol_type(type); +} + +/// Verify a given type is a java generic symbol type, checking +/// that it's associated type arguments match a given set of identifiers. +/// Expected usage is something like this: +/// +/// require_java_generic_symbol_type(type, "java::Generic", +/// {{require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}, +/// {require_type::type_argument_kindt::Var, "T"}}) +/// +/// \param type The type to check +/// \param identifier The identifier to match +/// \param type_expectations A set of type argument kinds and identifiers +/// which should be expected as the type arguments of the given generic type +/// \return The given type, cast to a java_generic_symbol_typet +java_generic_symbol_typet require_type::require_java_generic_symbol_type( + const typet &type, + const std::string &identifier, + const require_type::expected_type_argumentst &type_expectations) +{ + const java_generic_symbol_typet &generic_base_type = + require_java_generic_symbol_type(type, identifier); + + const java_generic_typet::generic_type_argumentst &generic_type_arguments = + generic_base_type.generic_types(); + REQUIRE(generic_type_arguments.size() == type_expectations.size()); + REQUIRE( + std::equal( + generic_type_arguments.begin(), + generic_type_arguments.end(), + type_expectations.begin(), + require_java_generic_type_argument_expectation)); + + return generic_base_type; +} diff --git a/unit/testing-utils/require_type.h b/unit/testing-utils/require_type.h index eb13fed9614..d49c02743a1 100644 --- a/unit/testing-utils/require_type.h +++ b/unit/testing-utils/require_type.h @@ -84,6 +84,15 @@ java_implicitly_generic_class_typet require_java_implicitly_generic_class( const std::initializer_list &implicit_type_variables); java_class_typet require_java_non_generic_class(const typet &class_type); + +java_generic_symbol_typet require_java_generic_symbol_type( + const typet &type, + const std::string &identifier); + +java_generic_symbol_typet require_java_generic_symbol_type( + const typet &type, + const std::string &identifier, + const require_type::expected_type_argumentst &type_expectations); } #endif // CPROVER_TESTING_UTILS_REQUIRE_TYPE_H