From 7d041f04dbdf43ee5fd0587a9ca359835d37708e Mon Sep 17 00:00:00 2001 From: svorenova Date: Tue, 14 Nov 2017 16:30:18 +0000 Subject: [PATCH 1/4] Defining a new type for generic bases --- src/java_bytecode/java_types.h | 59 ++++++++++++++++++++++++++++++++++ src/util/irep_ids.def | 1 + 2 files changed, 60 insertions(+) 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) From 6d691d7b18a48e3ea7973d0c9d88cd5c16fff105 Mon Sep 17 00:00:00 2001 From: svorenova Date: Fri, 19 Jan 2018 17:03:37 +0000 Subject: [PATCH 2/4] Parsing generic bases' information into the class symbol --- .../java_bytecode_convert_class.cpp | 120 +++++++++++++++++- 1 file changed, 115 insertions(+), 5 deletions(-) diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index e6302f82dcd..7ac6b176aef 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 From 54df3a1d635c626d4371a89da3f3d616e1d208d6 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 24 Jan 2018 11:36:06 +0000 Subject: [PATCH 3/4] Correcting generic parameters in bases for implicitly generic classes If the superclass or interface uses a generic parameter inherited from an outer class, make sure that the parameter for the base points to the parameter of the outer class. --- src/java_bytecode/java_bytecode_convert_class.cpp | 15 +++++++++++++++ 1 file changed, 15 insertions(+) diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 7ac6b176aef..fa1dbc19636 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -708,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 @@ -785,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); + } } } From 50dcec80d7f0ff8ab4d48b62a324388783466f42 Mon Sep 17 00:00:00 2001 From: Jeannie Moulton Date: Mon, 22 Jan 2018 15:19:58 +0000 Subject: [PATCH 4/4] Adding unit tests for extracting generic bases' info --- .../ContainsInnerClass$InnerClass.class | Bin 0 -> 501 bytes ...ContainsInnerClass$InnerClassGeneric.class | Bin 0 -> 617 bytes .../ContainsInnerClass.class | Bin 0 -> 608 bytes ...ContainsInnerClassGeneric$InnerClass.class | Bin 0 -> 609 bytes .../ContainsInnerClassGeneric.class | Bin 0 -> 625 bytes .../DerivedGenericInst.class | Bin 330 -> 327 bytes .../DerivedGenericInst.java | 4 - .../DerivedGenericInst2.class | Bin 0 -> 364 bytes .../DerivedGenericMixed1.class | Bin 0 -> 480 bytes .../DerivedGenericMixed2.class | Bin 0 -> 492 bytes .../DerivedGenericUninst.class | Bin 408 -> 457 bytes .../DerivedGenericUninst.java | 4 - .../DerivedGenerics.class | Bin 0 -> 1297 bytes .../DerivedGenerics.java | 171 ++++++ .../ExtendsAndImplements.class | Bin 0 -> 746 bytes .../ExtendsAndImplementsGeneric.class | Bin 0 -> 811 bytes .../ExtendsAndImplementsSameInterface.class | Bin 0 -> 672 bytes .../ExtendsAndImplementsSameInterface2.class | Bin 0 -> 694 bytes ...ndsAndImplementsSameInterfaceGeneric.class | Bin 0 -> 713 bytes ...mplementsInterfaceGenericSpecialised.class | Bin 0 -> 678 bytes .../ImplementsInterfaceGenericUnspec.class | Bin 0 -> 627 bytes .../ImplementsMultipleInterfaces.class | Bin 0 -> 759 bytes .../java_bytecode_parse_generics/Int.class | Bin 0 -> 99 bytes .../InterfaceGeneric.class | Bin 0 -> 236 bytes .../InterfaceGeneric.java | 4 + .../NotGeneric.class | Bin 0 -> 280 bytes .../ThreeHierarchy.class | Bin 0 -> 337 bytes .../parse_derived_generic_class.cpp | 540 +++++++++++++++++- unit/testing-utils/require_type.cpp | 47 ++ unit/testing-utils/require_type.h | 9 + 30 files changed, 755 insertions(+), 24 deletions(-) create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClass$InnerClass.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClass$InnerClassGeneric.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClass.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClassGeneric$InnerClass.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/ContainsInnerClassGeneric.class delete mode 100644 unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericInst.java create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericInst2.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericMixed1.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericMixed2.class delete mode 100644 unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericUninst.java create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/DerivedGenerics.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/DerivedGenerics.java create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplements.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplementsGeneric.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplementsSameInterface.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplementsSameInterface2.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/ExtendsAndImplementsSameInterfaceGeneric.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/ImplementsInterfaceGenericSpecialised.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/ImplementsInterfaceGenericUnspec.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/ImplementsMultipleInterfaces.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/Int.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/InterfaceGeneric.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/InterfaceGeneric.java create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/NotGeneric.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/ThreeHierarchy.class 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 0000000000000000000000000000000000000000..f359575153715ce447748ac5cf1d6ee9ccb51ac4 GIT binary patch literal 501 zcmZutO-sW-5Ph4*#>QxCjjbQ}ap<8|upYd%1SFyqf|p9~+jOZbaRW)(|K&jh5B>mu zlsFp$5n7hrnYZuFykWk7KED9m;JAhgTpK3#Ewn8hFjTW=nRc!j+`x}j#-&O}N{Pge zc$yA~A4(-NkD=XNC%Bj}n0`DH4D~=N@wj-MisXq;Bl>9uamb?yPo&1hr>PAY?9zq7 zDS;sFY>iW=l+aYQv79TOEfR7$4ITsyEW=^&!k4@saW(IcR3_#k8F(bN$MGTw#l6%s zxpyR8idj*UUg;VK8>l+4aA@I(;be6a|Lhs8qL`u5)eC5@>Tyn+Hfias(a_CxM%Th7 z#TsQE3_5__yL<=heZY7lWWc7knrm;dMS1H_1qXFPq|dvNGa7^p?4p^+J?!MHW?I+= FegP)ta|Zwb literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..09cf119f8b2cfb3b70c16b08a99286c7fbc000a1 GIT binary patch literal 617 zcma)3%TB^T6g@+cO0Dt`!Dr%v7=%PzxDvt!qA_XIgogc4COD){O<-a`7PjjxuzcRFKyVapI*}fbr9!`BKz1p@ftqGs; zrpwj1c{iL0Cv0`BgmfNa^u4L?h$|VjTk268Gcigq!C4e? z|IS3KMI$aQhvArZnWnX}d_LlcG`c$0NoGmAM~V($)Elp0^*5wm$kJfYn~AYKY>;05 oLBT|hEW*dx81kf>G0q@aAWK7$-W0Y`iscTrNE(FEu!~LL8+<*M1poj5 literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..55b7569f8cfbbf89d86e392f197aeb040aebd02b GIT binary patch literal 608 zcma)3O;5r=6r2ZzN=5k)za@GgMm^YzCm~!g8k0s38175i)FpMBw1xlW$;5*{z#nCN z+YoDlAs+hPbavi!`u6kd{R6-i+761?v$1dEz{Vk=aj&(E2cbxkJIP4-glf*o#KsZ9 z$r(byXpX%>q*I}Ek{@+)*d-K|9}rGg>lWW+d1a^qEz(&m3D^G`>UmQ!7j7tY;11JR z>7d(ZqjFDamG(Kn+4+cI4WbEK);y)d0 ze5>FJRN!z0)=>pvgHZvSj9`LsZ!mJX8>V#e271jTO|IpP>|%?t8D;@m*v`&(vbxI} PpvjgNKPARC_ch=f=V_Zm literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..4070754058fd911c147007a0cb289431c3f42a91 GIT binary patch literal 609 zcmaKp!A`-^K%&#(6n0GBw#J+{9g+qpH_@Dykf}!U2JRJ(9gIleo z- zfw%A{@>)fIRKB9=Eafy|g4Rqdg^dklZCI#TIAU;8r~0RP1}mw-VAP{2R#QL2Dczw- z*U5^-$SP9wTG*tRBXx%iJpgYsU%?u0$h=TyfYX|d**>;NSAHniC{RXxT#cbf+KxF+ ZafdPkC0aAsMLCXp$W!FR7&yQ-@C{M|lmh?& literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..94e68d33065a68494202353135a17bb98e0d7e42 GIT binary patch literal 625 zcmZ`$O;5r=5PjPM6+}Tq6uEF91~q|;Cre07jUP#)2O926+2E40HEkjBXL&O5;1BRe z8K(^ftLb5P=DmGyW-|Nv_5K0i0<98s92z(>&@^z&P`X!21eV9ckfFQ*f}kc{h7;TJ zRm7zVH;=c1JksrK7?Ytmk~77lWgr;NvrPlXF^9dBvoMfKMneX@dpc&wS^ku2RBWll z!*VeZfx{;rF*VzFxi{v4jPaVxMNg7uZDn_)*&1o*%kz)Boo!17C2x1&T-tNK;(d>+ zS^se|7j9$@|5LQgk-rRFaU({iSm6)!V753s9Wo)C&(9GN^L-lVjhEAsZ*B77- zjXoD(bPQ}!EK;VSlrYqn;tnxa6k|>P><#Rd5*@pA7ZUOg70P2N2~foz#afElC#0`S R*Kt5dLxbE%8s!M(fp4(=o{j(j literal 0 HcmV?d00001 diff --git a/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericInst.class b/unit/java_bytecode/java_bytecode_parse_generics/DerivedGenericInst.class index f5a72b7d0a53047cca6ec461c1a51b33562ba53a..9b796c9b9a49b05ca886a2f886e838f9bd38bb90 100644 GIT binary patch delta 32 mcmX@bbew6zW&shG)S}F?)D-vBJRl>vc;c~mMv=*Cj4A-ko(q`( delta 35 pcmX@kbc$)hW?^xc)S}F?)D-vBJRl?4Gq1R0;^BBk#>vWzDgg8n46y(J 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 0000000000000000000000000000000000000000..d9f9cd5c25ef88170e0e6d9265290a3f14c8d350 GIT binary patch literal 364 zcmZ8dK}*9h6#lYxt*h1P)QcyN>cN6|>llKf6oLpFyGqu@8fjBW)A_r05tu$&W7xz*V$WmR~%Y>mnQMnejF{Hod>*DmidK5;K zBc5t2&9lhlQ(C?ivXt5it16xFSFsdvA#@(Qo?Mz_Oyj~y)tF4)Dd*>K^UC_dX(D*& zF&u2xT08Wne+F=Z4*i5%j5aAL`-Ec3j_I9$fUO905K#16@)%o$qrV395w`X1Hb&TK G^X@Ob3Rb=V literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..8b0a137c161c9e05e2775306f269132df64f4436 GIT binary patch literal 480 zcmZutO;5r=6rAO&fGCQH2QMC#gT%y>G);^KLsIoX!__S96PJ`NDGTb)@?_${AK;HN zzLt6*c-Vb2vv1x`-uKVv7k~>KR*^^3!hwaBKv~mEPf-{MG~9_?%1$WtxbrZYkZ-yI zm4O;-X%;aF4;)ajzU%%Zsf~wC}WlIOe~mZ zH5X{PHx#QS1-GOb_;>1+f^#0;S~tDT{)|WeI&4nlu&rx*mz(JwHydxeeQhXyl0H55 zr?Zfzq>VHx(y6;Th!(L=J(a|6t|yzHB}=KHjLOE_Dz$)>eS>4_fMNueFcZYH+Tana**1bQZAUPAL z^wdDhWMW9b@;qjWj?yaWFg!Ty3*;~3kZUzpX}X(?d@`Q&BWCJu9LT6IjY{!?%qNd( zEYNhX$fzlW*Q7ZKZq+k|Z5D4X54}A74DS6q;jp6)kDWW->8ksVyO8&0@q;vSl(zqB zyU_^^$YcuDUOX`YbyaG;vFvVqoG!*j8I_gV+&TaM&r{e(j`s`*K6w;47CFnIlrb#D tvC7N^$F!$#^akERa8ARC`#26Vk@>0v)GE;L>7#W0ovJ%S@^>Y&Q z()In5vQm>vtQi?NgEQ0f5=%;pQW+VTLqe=4icXuj-9$>nCABECEH%YFH4n&0F4hBS zC4w8HCswgeSUB 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 0000000000000000000000000000000000000000..bd6fb9644fe7cebff9f16a5f997dbeacfe621e24 GIT binary patch literal 1297 zcmah}+j0^?5IsYg!Andu7fnJm1cIoQRH`iEg{n<_Aj$i%JHn)vA+PG6?Chu?pG{sK@!c?uKQO`(*+D~7ldUkeNw>ri;|QaB%l zq6fRGe7)C2iwyG-XfcF$8L~t0sgm9B$(n2^t~;J!*oq|WTj%_e=UuKE`Kr>QA-uhV zFmvhu%t!J{I0eFUL)p5(^=vimN!92lqoWSDX<~w7L?$baNLCI8R%t8E>7Z3b6RWt~ z_rtzlGb}`);be)FzZo4-^bNy|b<*^N_#}nLJ-hiWEcljT-Kw@OT+tFrQ$t#KU$`y8 zinR-2OYTZvI24cwUic2f%7}oi%VSA5G;FHSUM*cqaMW?Nq$d0Q1p_lgTCuG4 z{z?nw`0tc6I7*K|OSTwE7!1`UqLo>Vql^|yojltvC)RB8yL1sdG8&-HU*Yb+y1e+R$}{o+WF1d>P@eG8MIa`YU- zZIWr+>Dzb7o~EcCK1=o-?vVsCnD6_uWZ%aF<9~=pMlaxTA73QT5}p|UQ|c!8tYFpX zH9Rx=Io6Hdz$R%%UpgMi7i8s)4J2|uz`m0shL 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 0000000000000000000000000000000000000000..28afaa564af54985a9d949b1be2bbe99bb502e0a GIT binary patch literal 746 zcmaJ;%TDV+3_X*k4U_-{%KHtQf)L%X10f-}_o`BONFc;^nwS!lPEax}NG$jv7O(-t zf)C)M5KgHo=#5y+*yHi>Ikw+FUf%$0U^$O0Ci0lXR30X#EzDS$wJ>L4ULd#SD_?I5 zWJ)Wi0_JY$k-(tiD>`V@s}!BcYQT|UCv;_SDkDF6w}Ym>@MD27=g*BM<;6S7tJJRo zs*}?3ra(Rp>$Fe$BJ>1CODoQ$Y|3&VRjpi6nrakrl362t*5a=S6n`WgRxioboYQ;k z*Ob(ah?N{U|432fyIU#cwl|%ma&#_T`sV(MV4cTdBXa4lpLAN>Sz{Nhcc!1oVu<^{$>7x*?6JcQvk qc#UnsY-H}ckaypZ#usg2hiON;X;+_+>84H7Y@pbp7{yr2j(-B!t&?E@ literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..13f542bf41eb4fd656e2a17236dda615c6235200 GIT binary patch literal 811 zcma)4O;6iE5Pj=7xCv=P!$(VjLUT$uz@;aMBB9b&kxW|&3-!9Ohu|n)BYQ*3nHvXw z35QlfLgK&=;73)=1~*CoAugUbvv1zK+4ar8t7`xsQ7yv8VgWfUIe712*};l~4+3Ie zpyGDrkzDUd)mi`E?vk%J1q!=iM@ijJNFe8VT$yNuD%4F*YxO+=`%@h7S=kL0ed|YU zN<7)_ai!wMzU=MEBs6(ewDm!l3M{#we```fx}}0vbl9Valuo~rq9pWr#@u-C@!|je z>Qjvk_SfX@Vj4%ZL;4^N1ZHaW$M(wC>Vs|U4(XqRU0MRN;cYx5H{Hyb_bdJ(6B(H~ zBea&%)S-k&y9Orv(x(xaH4n}0#{I;nFQK`knQdP9h=Pohu9+7oVG^Yh9J~-%c;cS; z((f7L=NdW?m>S}Yh82Ez8y51IfZ!j3M{q1KvQXqRn8{pu$!LqC;pA5@A^tMR;T3=H z8c$GWY^Y4Y6kcSDjsNCtZ7OiaidAu8B3%6~9rV;=E literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..b1ec684caa6ac234574c27edca68b416aa18f7ee GIT binary patch literal 672 zcmah`%TB^j5IvWI)rty;?|0k)3)#4XkPuNrQgwlGe`yD(X>Uzih~MGD@6e4J7k+>r zWt<{05lCFzd7R9dIdkXp>-_`3G4>3kuwq~pYX*{7*Ri2vQ^%ITOx00NR1?q&#T$X- ziEop@lIbYA?0anru4UV0Bxm}TbZ=zf#Q6wJMm;AKI5bc1BT{x)S9a68bIBtWg)Qk( zQ$-YXq(v10BlJDGps45D0xN~0c`FC9>`K)w$7Nj#xG4VzziQu-6)`;5a=J=J{eYD; z%yUu{I9ApCZ9hUPwaNrmoie8u%W3)jz@jrJ-Y(zZh6A!keZr$yTN*lMb!?}xgWWV1 zu_SQt@1_F!sEa^mT%bU9VrwQ0q}!*fj=*Z6IqhGt&sR%Eg<% zKxQZONMOiOnvR-5jiM7-^BEa&LRb2yGEzz00W;=Y#RALD-jyNk#oOAe1eZPqq)l9v z0adi2s4iVv-xRRpFrY&+=btX5`YoN=7d1a+4N$o!aqQQac9= zy%uJ3n8SPygBTK6`hR=@t5ZfG->q6;_)B(24ij3^Z_;sHV7yrQ?X$4RyUc=j$V*Q1 zWn~=ou~%X%*k)HBAnw>n!REK84PK+4{oH#3+X0S5G6}!m$mvI3NWhHOzElkZ&m@%i=+;1~xf#IT)26gvub73?Y4XJBoHtlr}zUg~q%Dc!bu z!VJm`$%fsLJQ#X{A!-=pBr3MFgDQnup~(Y1N%UUpPVreuF!rE(77UxhXD%6rOET!Tc=fe(((|EljCU z=T$^(#TM>HsfR|VpvCxu(P-qM4l-58~3;nZqnxl0VgVt JP2xnb^#uhUp^^Xq literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..ea90de3f1fc65c6f2fff25a9ee46061c19d94f18 GIT binary patch literal 678 zcma)3%T5A85UgQ=)fE*Le7`P6^dJ{6Mq^?$8j@8H7!nU2hNXoe`!M_9yY!;QgCF2W z8GB)kxN`6?)7_P->FVi^&$o8~``9p$L)pMQ77S#usAEaTvW^vj{E>21cr2h*b{YcN zQ?Eq=)24FiDsr0S-^ixT$gJsE(r!p!#dQK^!;T6Bw#}OJV3R{`7}VU5{CjE91-axa ztNuWilC}z{btqs2o9(t}uuVRbO26>yW|ypx;qkg^yE2S? zc5^T!ObBMW^U)CJ`|;!0L*0vfi_TR%R_TmQ_NbM(4fbL~1?U*lv0A_y)(e=zw7}NC zMieOiOf)dYP}-Tm%nvKECZPAE9ntl@zSwUYyUT%h#!J=suuHDSIjeFM9CN!b z5Ko+BVDO#qgSVLAyf7eeoa9QxQ}O*vti2-hm=fRp6&FufTuh61pP{A2qdI3W({C}0 Ixqd8t0XUJ9ZU6uP literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..2703a52e1aa70190e16f82c0612f90271c8f4173 GIT binary patch literal 627 zcmaix&rZTX5XQePe=3NAh^RN>MeraOPeN*pq9Lhz0J(3=ic8upX$y&Or6&^)K7bEp zoCP!p2M#+s^X<%UXLr87KRyAR;V_E?_Dqyb?3*}XNH?XDvBi+6)_M%dtDr9!^0rjs ze(XCU>~hB=rDz8(_j){(I-ZNk_*q5_M|RsEdBPVej@l{~;S+botxzJA?xTuE!fh~= z{{vn|zmVg#)y;0JVG$x51-`fw@pI5;C{=6rkWYBs<7!ZUaE8K-DJRpB1I6QUNIj>j zHL7H|XtvH*bFEd$Uhe+y=1wpUU2!AzSCp>lVH44xzc4!0ZRC(bnxV4pCm0ILU6ZtY zFDfu-P&5yknn8=;6q)2*($2JU@(%V!P68Wb^)cWeLpC={Ko*UH8K!HQVS+=tGYbMD+fe}DZ3@D-nm$YZmJEo>KIV#mU+g^w2YEbI#uPL;28 zQy^D6z7sIdf-VWHILfE1c+jEnR(3q@l%2qp-kl6pQm0K*KdMMz&uI_7do&Dv3YB|0gZZ!2Jek50Z#O|4x^%9RDJv~z4XK;bqc4e3 z8w*&paA4yQM>bYa64-rjVu8|hz_B%MWxeqH0yST5HeyG#v0k z^Dt0=#k)57uvPF-oHaNKj`{iv#7|BPEb(0!HT$qRx5of1;{#W`c9i&jL(aXz_>mz8 ubIGeHr{vEZ6J;a!lwn3QOk*rt`o^+rS=stCa#`7Vo()t+66>gr;>JIK=9vco literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..981b37567691f5230675dc73e18e503c34aa31cc GIT binary patch literal 99 zcmX^0Z`VEs1_l!bc6J6vST8HF tERm6c*)y+%kwE~&(a%ZDOV{^L%1TWxVPjxmWMBds2LeD$c zhK;Kgrdm5pA)pn(`K3k4scxA$K>ebgc_pbu zX^F|H?x}gHMVZNZAPX581klBSLg-FmV_;xpU;?@yNV709Ff*_K`K&-569XF%Ls;w# I9AFVn02YWklK=n! literal 0 HcmV?d00001 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 0000000000000000000000000000000000000000..a478117ccf678143d90f098c8cb40879244df9dd GIT binary patch literal 280 zcmYL@y>7xl5QJyJKj4_3ARd4+Nr9VG0nrd8Lb6B!qCeY9ION!pF}xQQQi?nP4~4P^ zmMHFS_M4g2oiD$C0AA7aP)El_*To~jUTaPh0?i1{SZBJN5b96QD}pu66DD**o$-AC z6LGOrQ7WVt=CMjws?cVxpjB@4j^Ky$y!_;h3muOL-Xh-@F@I>&>%R*cJB3OFL=D)NQh~L_fWhAqKlQb-2DGUr^ 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