From ba05f187d01b14ac4c54cab0eb306c1b044529df Mon Sep 17 00:00:00 2001 From: svorenova Date: Thu, 23 Nov 2017 11:39:28 +0000 Subject: [PATCH 1/2] Introducing a new type for implicitly generic classes Non-static inner classes of generic outer classes are marked as implicitly generic and a vector of implicit generic type parameters is stored. The identifiers of the implicit generic type parameters used in the inner classes are updated to point to the outer class. --- .../java_bytecode_convert_class.cpp | 160 ++++++++++++++++++ .../java_bytecode_convert_class.h | 18 ++ src/java_bytecode/java_bytecode_language.cpp | 20 +++ src/java_bytecode/java_types.h | 65 +++++++ src/util/irep_ids.def | 2 + 5 files changed, 265 insertions(+) diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 42d3992081d..4c2e640ff9e 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -517,3 +517,163 @@ bool java_bytecode_convert_class( return true; } + +/// For a given generic type parameter, check if there is a parameter in the +/// given vector of replacement parameters with a matching name. If yes, +/// replace the identifier of the parameter at hand by the identifier of +/// the matching parameter. +/// Example: if \p parameter has identifier `java::Outer$Inner::T` and +/// there is a replacement parameter with identifier `java::Outer::T`, the +/// identifier of \p parameter gets set to `java::Outer::T`. +/// \param parameter +/// \param replacement_parameters vector of generic parameters (only viable +/// ones, i.e., only those that can actually appear here such as generic +/// parameters of outer classes of the class specified by the prefix of \p +/// parameter identifier) +static void find_and_replace_parameter( + java_generic_parametert ¶meter, + const std::vector &replacement_parameters) +{ + // get the name of the parameter, e.g., `T` from `java::Class::T` + const std::string ¶meter_full_name = + as_string(parameter.type_variable_ref().get_identifier()); + const std::string ¶meter_name = + parameter_full_name.substr(parameter_full_name.rfind("::") + 2); + + // check if there is a replacement parameter with the same name + const auto replacement_parameter_p = std::find_if( + replacement_parameters.begin(), + replacement_parameters.end(), + [¶meter_name](const java_generic_parametert &replacement_param) + { + const std::string &replacement_parameter_full_name = + as_string(replacement_param.type_variable().get_identifier()); + return parameter_name.compare( + replacement_parameter_full_name.substr( + replacement_parameter_full_name.rfind("::") + 2)) == 0; + }); + + // if a replacement parameter was found, update the identifier + if(replacement_parameter_p != replacement_parameters.end()) + { + const std::string &replacement_parameter_full_name = + as_string(replacement_parameter_p->type_variable().get_identifier()); + + // the replacement parameter is a viable one, i.e., it comes from an outer + // class + PRECONDITION( + parameter_full_name.substr(0, parameter_full_name.rfind("::")) + .compare( + replacement_parameter_full_name.substr( + 0, replacement_parameter_full_name.rfind("::"))) > 0); + + parameter.type_variable_ref().set_identifier( + replacement_parameter_full_name); + } +} + +/// Recursively find all generic type parameters of a given type and replace +/// their identifiers if matching replacement parameter exist. +/// Example: class `Outer` has an inner class `Inner` that has a field +/// `t` of type `Generic`. This function ensures that the parameter points to +/// `java::Outer::T` instead of `java::Outer$Inner::T`. +/// \param type +/// \param replacement_parameters +static void find_and_replace_parameters( + typet &type, + const std::vector &replacement_parameters) +{ + if(is_java_generic_parameter(type)) + { + find_and_replace_parameter( + to_java_generic_parameter(type), replacement_parameters); + } + else if(is_java_generic_type(type)) + { + java_generic_typet &generic_type = to_java_generic_type(type); + std::vector &arguments = + generic_type.generic_type_arguments(); + for(auto &argument : arguments) + { + find_and_replace_parameters(argument, replacement_parameters); + } + } +} + +/// Checks if the class is implicitly generic, i.e., it is an inner class of +/// any generic class. All uses of the implicit generic type parameters within +/// the inner class are updated to point to the type parameters of the +/// corresponding outer classes. +/// \param class_name +/// \param symbol_table +void mark_java_implicitly_generic_class_type( + const irep_idt &class_name, + symbol_tablet &symbol_table) +{ + const std::string qualified_class_name = "java::" + id2string(class_name); + PRECONDITION(symbol_table.has_symbol(qualified_class_name)); + symbolt &class_symbol = symbol_table.get_writeable_ref(qualified_class_name); + java_class_typet &class_type = to_java_class_type(class_symbol.type); + + // the class must be an inner non-static class, i.e., have a field this$* + // TODO this should be simplified once static inner classes are marked + // during parsing + bool no_this_field = std::none_of( + class_type.components().begin(), + class_type.components().end(), + [](const struct_union_typet::componentt &component) + { + return id2string(component.get_name()).substr(0, 5) == "this$"; + }); + if(no_this_field) + { + return; + } + + // create a vector of all generic type parameters of all outer classes, in + // the order from the outer-most inwards + std::vector implicit_generic_type_parameters; + std::string::size_type outer_class_delimiter = + qualified_class_name.rfind("$"); + while(outer_class_delimiter != std::string::npos) + { + std::string outer_class_name = + qualified_class_name.substr(0, outer_class_delimiter); + if(symbol_table.has_symbol(outer_class_name)) + { + const symbolt &outer_class_symbol = + symbol_table.lookup_ref(outer_class_name); + const java_class_typet &outer_class_type = + to_java_class_type(outer_class_symbol.type); + if(is_java_generic_class_type(outer_class_type)) + { + const auto &outer_generic_type_parameters = + to_java_generic_class_type(outer_class_type).generic_types(); + implicit_generic_type_parameters.insert( + implicit_generic_type_parameters.begin(), + outer_generic_type_parameters.begin(), + outer_generic_type_parameters.end()); + } + outer_class_delimiter = outer_class_name.rfind("$"); + } + else + { + throw missing_outer_class_symbol_exceptiont( + outer_class_name, qualified_class_name); + } + } + + // if there are any implicit generic type parameters, mark the class + // implicitly generic and update identifiers of type parameters used in fields + if(!implicit_generic_type_parameters.empty()) + { + class_symbol.type = java_implicitly_generic_class_typet( + class_type, implicit_generic_type_parameters); + + for(auto &field : class_type.components()) + { + find_and_replace_parameters( + field.type(), implicit_generic_type_parameters); + } + } +} diff --git a/src/java_bytecode/java_bytecode_convert_class.h b/src/java_bytecode/java_bytecode_convert_class.h index 490372adf9d..6f87db44baa 100644 --- a/src/java_bytecode/java_bytecode_convert_class.h +++ b/src/java_bytecode/java_bytecode_convert_class.h @@ -28,4 +28,22 @@ bool java_bytecode_convert_class( lazy_methods_modet, java_string_library_preprocesst &string_preprocess); +void mark_java_implicitly_generic_class_type( + const irep_idt &class_name, + symbol_tablet &symbol_table); + +/// An exception that is raised checking whether a class is implicitly +/// generic if a symbol for an outer class is missing +class missing_outer_class_symbol_exceptiont : public std::logic_error +{ +public: + explicit missing_outer_class_symbol_exceptiont( + const std::string &outer, + const std::string &inner) + : std::logic_error( + "Missing outer class symbol: " + outer + ", for class " + inner) + { + } +}; + #endif // CPROVER_JAVA_BYTECODE_JAVA_BYTECODE_CONVERT_CLASS_H diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index a275cfa6ec3..26914f08522 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -209,6 +209,26 @@ bool java_bytecode_languaget::typecheck( return true; } + // find and mark all implicitly generic class types + // this can only be done once all the class symbols have been created + for(const auto &c : java_class_loader.class_map) + { + if(c.second.parsed_class.name.empty()) + continue; + try + { + mark_java_implicitly_generic_class_type( + c.second.parsed_class.name, symbol_table); + } + catch(missing_outer_class_symbol_exceptiont &) + { + messaget::warning() + << "Not marking class " << c.first + << " implicitly generic due to missing outer class symbols" + << messaget::eom; + } + } + // Now incrementally elaborate methods // that are reachable from this entry point. if(lazy_methods_mode==LAZY_METHODS_MODE_CONTEXT_INSENSITIVE) diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index d25d49bcefa..d52fa713de6 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -110,6 +110,12 @@ class java_generic_parametert:public reference_typet return type_variables().front(); } + type_variablet &type_variable_ref() + { + PRECONDITION(!type_variables().empty()); + return const_cast(type_variables().front()); + } + private: typedef std::vector type_variablest; const type_variablest &type_variables() const @@ -313,6 +319,65 @@ inline const typet &java_generic_class_type_bound(size_t index, const typet &t) return gen_type.subtype(); } +/// Type to hold a Java class that is implicitly generic, e.g., an inner +/// class of a generic outer class or a derived class of a generic base +/// class. Extends the java class type. +class java_implicitly_generic_class_typet : public java_class_typet +{ +public: + typedef std::vector implicit_generic_typest; + + explicit java_implicitly_generic_class_typet( + const java_class_typet &class_type, + const implicit_generic_typest &generic_types) + : java_class_typet(class_type) + { + set(ID_C_java_implicitly_generic_class_type, true); + for(const auto &type : generic_types) + { + implicit_generic_types().push_back(type); + } + } + + const implicit_generic_typest &implicit_generic_types() const + { + return ( + const implicit_generic_typest + &)(find(ID_implicit_generic_types).get_sub()); + } + + implicit_generic_typest &implicit_generic_types() + { + return ( + implicit_generic_typest &)(add(ID_implicit_generic_types).get_sub()); + } +}; + +/// \param type: the type to check +/// \return true if type is a implicitly generic java class type +inline bool is_java_implicitly_generic_class_type(const typet &type) +{ + return type.get_bool(ID_C_java_implicitly_generic_class_type); +} + +/// \param type: the type to check +/// \return cast of type to java_generics_class_typet +inline const java_implicitly_generic_class_typet & +to_java_implicitly_generic_class_type(const java_class_typet &type) +{ + PRECONDITION(is_java_implicitly_generic_class_type(type)); + return static_cast(type); +} + +/// \param type: source type +/// \return cast of type into a java class type with generics +inline java_implicitly_generic_class_typet & +to_java_implicitly_generic_class_type(java_class_typet &type) +{ + PRECONDITION(is_java_implicitly_generic_class_type(type)); + return static_cast(type); +} + /// An exception that is raised for unsupported class signature. /// Currently we do not parse multiple bounds. class unsupported_java_class_signature_exceptiont:public std::logic_error diff --git a/src/util/irep_ids.def b/src/util/irep_ids.def index 2a25ab2d250..e2e3c30885e 100644 --- a/src/util/irep_ids.def +++ b/src/util/irep_ids.def @@ -831,7 +831,9 @@ IREP_ID_TWO(C_java_generic_parameter, #java_generic_parameter) IREP_ID_TWO(C_java_generic_type, #java_generic_type) IREP_ID_TWO(C_java_generics_class_type, #java_generics_class_type) IREP_ID_TWO(C_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(generic_types, #generic_types) +IREP_ID_TWO(implicit_generic_types, #implicit_generic_types) IREP_ID_TWO(type_variables, #type_variables) IREP_ID_ONE(havoc_object) IREP_ID_TWO(overflow_shl, overflow-shl) From 01633621a4428e8ebd41f4f0cec4c4190e7c7006 Mon Sep 17 00:00:00 2001 From: svorenova Date: Wed, 22 Nov 2017 11:21:08 +0000 Subject: [PATCH 2/2] Adding a unit test for implicitly generic classes --- ...asses$GenericInner$GenericInnerInner.class | Bin 0 -> 848 bytes ...icClassWithInnerClasses$GenericInner.class | Bin 0 -> 900 bytes ...assWithInnerClasses$Inner$InnerInner.class | Bin 0 -> 821 bytes .../GenericClassWithInnerClasses$Inner.class | Bin 0 -> 774 bytes ...ricClassWithInnerClasses$StaticInner.class | Bin 0 -> 616 bytes .../GenericClassWithInnerClasses.class | Bin 0 -> 1111 bytes .../GenericClassWithInnerClasses.java | 29 +++ ...parse_generic_class_with_inner_classes.cpp | 219 ++++++++++++++++++ .../parse_signature_descriptor_mismatch.cpp | 5 +- unit/testing-utils/require_type.cpp | 48 ++++ unit/testing-utils/require_type.h | 7 + 11 files changed, 305 insertions(+), 3 deletions(-) create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner$GenericInnerInner.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$Inner$InnerInner.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$Inner.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$StaticInner.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses.class create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses.java create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp diff --git a/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner$GenericInnerInner.class b/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner$GenericInnerInner.class new file mode 100644 index 0000000000000000000000000000000000000000..0384e7e68604b6b3082c9c79816064343a8d97f9 GIT binary patch literal 848 zcmb7CO-sW-5PjR$#@1-ls`aaCg&z6=ErKT#b15i7P@%D&(-_(6XS0!DIdpyt?n$>^g)w&F+_UPVW$Qj&ot|kvX z$2YB>OH9ES*_PY2d@gWArbPb?`FQ!L|FgvlPjw%r(-Df(^`0MpYZ`NfHPck}X1pKG zyq#gf5}Mgnb*hu;@V;jS6Q9ml)w-v~(0a03uI2Sx*S(=*2de&;V#szz6W?~uxwxC7 zd2iDcf-;tnk&(p#gE}vI>Mo{0bg#;6e-aKEY71*JB&*_~OY<^Nrcq7N)G|d8oePit zELO5JrB43U)b66*o#0ISi WY*LP}TUaJrATNy)q%a~41^5PEc<9Ce literal 0 HcmV?d00001 diff --git a/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner.class b/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$GenericInner.class new file mode 100644 index 0000000000000000000000000000000000000000..8470c58c2d5c54d205061ac84e64f5c14b22fd8a GIT binary patch literal 900 zcma)4(M}ps5IuL7va($&qEg#Zm6kT3iQ1;V2;qgKO%u|ZxZ39n-M}TVm}SxUSw0vO zAN&A6%JkgrVnCZsANJ0inRCz1%$>XYn_B>1@G%1u>o!u@uu!t_PQdx*`Cgzp-+daw z$TkOZJod&G-U}?v5@MFw4L=FwTYY&ZcL&n%?*44|y-rvY$Q-GzFT+XT37D?S2+5x* z(~5Q6^Ur+xx)GrnGW=qt}y7E=n5GYlWsnrvK zRCDy3l`XcE@BNqz+g{+x_JEOmYt)g06B#It<6ue`A+VjOTb>;d>nY4DU7SwU_7i1v z?~R>Vt$I9)O8xlY>8Kk|Ljv~EXcBb1uS&O6ipBmpxE=j=4suv>kVo0V2Z3tRg}F8b za*y9$p!VO_=d`9fRnhNLOwzz6*EhvYHu+^>L*O|*0}jtDUOeE%Tuyh!sNk2!GVKbz zLvjsTdu#g&V(S{lC6S3$p6Q62MS*_dFAFcRMnrz3#)YNtL_C|h*F%b0NBP#3KnJ^Br#`W-o}E!ilR+HrgH7wd8LLIT$YY&*M2?P z5u{GlW#C2a&?l{0B|`ER@ydZ8_@Sy3nT+G|XF%pIKS6JFrCPa78%u(o!+=KwuJL;f zuhsHff?RycAm=K&`nsPpiB>ABKt;QP)%<@Btepvxd(8{hJycPFf7HII`C-+oHHc&? z&AQh(^FpQb4=|}q6*%TXV+5stT-B*CE;IXG`u;YS-|i|^)*UMvk&cb^oYQ7Ito!>) z*S+}B^j|ww)X(R_McTzMmIWK#*qy4s)GkQ>e197`!P4I<9E!Z|_e?h`7C3iFj-bWW zgI)-1MhW!Mrr><${pqy+38KO^j12tW$H6J1qJM jX5$j_nc*xz+~OXk?Ex%poFET>z!YWMAqcS49ZMAxyrv1=35W|JAkJ7T(iZnLrIFcF*KQ_feJ zh?cAHjvz)Ye( z>{x@A z(*{f|8c1MAL!OWeDws4%Fn>Q0VgLWSN%i!t)q;PSsh}!k_#=h*PpLej&_S4Iq`=^L z0kN+*Zkqlfm?a(wEb+R`=$f?(uX<_k8B}_K^2Cvf6`mtft0KubIZtJpKN5lXaE2J literal 0 HcmV?d00001 diff --git a/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$StaticInner.class b/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses$StaticInner.class new file mode 100644 index 0000000000000000000000000000000000000000..b7001714a64c7b36b5b5dc447ecd0538a27f02eb GIT binary patch literal 616 zcma)3%TB^T6g|@dg;E8p;&Y)13uIw8uCyUBBpQ=O7X@4obpk_bG3{XDXSp(Q;RpCp z#@mWXk%YLIIrp6Vp85QG{{V1?0~0zL26heXF=&Zmu)PU?=1$0?k#jekh(KL1RD3y# zxSGX+LGSfRDY-I|szbDOGGHilrw`<-c`_2Wv&W%`dwdv@VtdnohXWqVl+VS28q0*C z>MO2fa1%u$X0S5shCE3GIosZ~AYBHTaxc|5?{DT(X`04jmzSsCPR_rpxU^P>O10en z`SKHVmL&$$pU&byT*-9N<5lCHrf+JYjEaGM>ai*|zZygR?{6?1uFA#{H2PD3(J7!v zSRzYk z>Z{>U4_&+`@?CQ!CAcUFrc$oc{UGof>3Xa=HQ{--f)^)M!EDp?d=-uYEht+hwN|TI zKN#zr?nf78K_LcWBdAylBs~*5E^}yAWLhST$1Yh0)+ zRp~3gS2^}W-P1v}&N|aI(;%n$;zbo`q#L?wpAIQg7Q+W^*OWspY03X39I#gA%4H+U=(!pHxuo7 z({^PJqIneY0;_^G8&R7Z^PQ?g3=7G{*n{ literal 0 HcmV?d00001 diff --git a/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses.java b/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses.java new file mode 100644 index 00000000000..f62932fcaf9 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/GenericClassWithInnerClasses.java @@ -0,0 +1,29 @@ +class GenericClassWithInnerClasses +{ + class Inner { + T t1; + Generic t2; + + class InnerInner { + T tt1; + Generic> tt2; + } + } + + class GenericInner { + T gt1; + GenericTwoParam gt2; + + class GenericInnerInner{ + + } + } + + static class StaticInner{ + U st; + } + + Inner f1; + Inner.InnerInner f2; + GenericInner f3; +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp new file mode 100644 index 00000000000..d74d4f2ba44 --- /dev/null +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_generic_class_with_inner_classes.cpp @@ -0,0 +1,219 @@ +/*******************************************************************\ + + Module: Unit tests for parsing generic classes + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include +#include +#include + +SCENARIO( + "parse_generic_class_with_inner_classes", + "[core][java_bytecode][java_bytecode_parse_generics]") +{ + const symbol_tablet &new_symbol_table = load_java_class( + "GenericClassWithInnerClasses", + "./java_bytecode/java_bytecode_parse_generics"); + + std::string outer_class_prefix = "java::GenericClassWithInnerClasses"; + + WHEN("Generic outer class has fields which are objects of the inner classes") + { + REQUIRE(new_symbol_table.has_symbol(outer_class_prefix)); + const symbolt &class_symbol = + new_symbol_table.lookup_ref(outer_class_prefix); + const java_generic_class_typet &generic_class = + require_type::require_java_generic_class( + class_symbol.type, {outer_class_prefix + "::T"}); + THEN("There is a field f1 of generic type with correct arguments") + { + const auto &field = require_type::require_component(generic_class, "f1"); + require_type::require_pointer( + field.type(), symbol_typet(outer_class_prefix + "$Inner")); + require_type::require_java_generic_type( + field.type(), + {{require_type::type_argument_kindt::Var, outer_class_prefix + "::T"}}); + } + THEN("There is a field f2 of generic type with correct arguments") + { + const auto &field = require_type::require_component(generic_class, "f2"); + require_type::require_pointer( + field.type(), symbol_typet(outer_class_prefix + "$Inner$InnerInner")); + require_type::require_java_generic_type( + field.type(), + {{require_type::type_argument_kindt::Var, outer_class_prefix + "::T"}}); + } + THEN("There is a field f3 of generic type with correct arguments") + { + const auto &field = require_type::require_component(generic_class, "f3"); + require_type::require_pointer( + field.type(), symbol_typet(outer_class_prefix + "$GenericInner")); + require_type::require_java_generic_type( + field.type(), + {{require_type::type_argument_kindt::Var, outer_class_prefix + "::T"}, + {require_type::type_argument_kindt::Inst, "java::java.lang.Integer"}}); + } + } + + WHEN("Inner class of a generic outer class is parsed") + { + std::string inner_class_prefix = outer_class_prefix + "$Inner"; + REQUIRE(new_symbol_table.has_symbol(inner_class_prefix)); + const symbolt &class_symbol = + new_symbol_table.lookup_ref(inner_class_prefix); + + THEN("It has correct implicit generic types") + { + const java_implicitly_generic_class_typet &java_class = + require_type::require_java_implicitly_generic_class( + class_symbol.type, {outer_class_prefix + "::T"}); + + THEN( + "There is a field t1 which is the generic parameter of the outer " + "class") + { + const auto &field = require_type::require_component(java_class, "t1"); + require_type::require_java_generic_parameter( + field.type(), outer_class_prefix + "::T"); + } + THEN( + "There is a field t2 of generic type with the generic " + "parameter of the outer class") + { + const auto &field = require_type::require_component(java_class, "t2"); + require_type::require_pointer( + field.type(), symbol_typet("java::Generic")); + require_type::require_java_generic_type( + field.type(), + {{require_type::type_argument_kindt::Var, + outer_class_prefix + "::T"}}); + } + } + } + + WHEN("Inner class of an inner class of a generic outer class is parsed") + { + std::string inner_inner_class_prefix = + outer_class_prefix + "$Inner$InnerInner"; + REQUIRE(new_symbol_table.has_symbol(inner_inner_class_prefix)); + const symbolt &class_symbol = + new_symbol_table.lookup_ref(inner_inner_class_prefix); + + THEN("It has correct implicit generic types") + { + const java_implicitly_generic_class_typet &java_class = + require_type::require_java_implicitly_generic_class( + class_symbol.type, {outer_class_prefix + "::T"}); + + THEN( + "There is a field tt1 which is the generic parameter of the outer " + "class") + { + const auto &field = require_type::require_component(java_class, "tt1"); + require_type::require_java_generic_parameter( + field.type(), outer_class_prefix + "::T"); + } + THEN( + "There is a field tt2 of nested generic type with the generic " + "parameter of the outer class") + { + const auto &field = require_type::require_component(java_class, "tt2"); + require_type::require_pointer( + field.type(), symbol_typet("java::Generic")); + const java_generic_typet &generic_field = + require_type::require_java_generic_type( + field.type(), + {{require_type::type_argument_kindt::Inst, "java::Generic"}}); + + const typet &type_argument = + generic_field.generic_type_arguments().at(0); + const java_generic_typet generic_type_argument = + require_type::require_java_generic_type( + type_argument, + {{require_type::type_argument_kindt::Var, + outer_class_prefix + "::T"}}); + } + } + } + + WHEN("Generic inner class of a generic outer class is parsed") + { + std::string generic_inner_class_prefix = + outer_class_prefix + "$GenericInner"; + REQUIRE(new_symbol_table.has_symbol(generic_inner_class_prefix)); + const symbolt &class_symbol = + new_symbol_table.lookup_ref(generic_inner_class_prefix); + + THEN("It has correct generic types and implicit generic types") + { + require_type::require_java_implicitly_generic_class( + class_symbol.type, {outer_class_prefix + "::T"}); + const java_generic_class_typet &generic_class = + require_type::require_java_generic_class( + class_symbol.type, {generic_inner_class_prefix + "::U"}); + + THEN( + "There is a field gt1 which is the generic parameter of the outer " + "class") + { + const auto &field = + require_type::require_component(generic_class, "gt1"); + require_type::require_java_generic_parameter( + field.type(), outer_class_prefix + "::T"); + } + THEN( + "There is a field gt2 of generic type with the generic " + "parameter of the outer class") + { + const auto &field = + require_type::require_component(generic_class, "gt2"); + require_type::require_pointer( + field.type(), symbol_typet("java::GenericTwoParam")); + require_type::require_java_generic_type( + field.type(), + {{require_type::type_argument_kindt::Var, + outer_class_prefix + "::T"}, + {require_type::type_argument_kindt::Var, + generic_inner_class_prefix + "::U"}}); + } + } + } + + WHEN( + "A generic inner class of a generic inner class of a generic outer class " + "is parsed") + { + std::string generic_inner_inner_class_prefix = + outer_class_prefix + "$GenericInner$GenericInnerInner"; + REQUIRE(new_symbol_table.has_symbol(generic_inner_inner_class_prefix)); + const symbolt &class_symbol = + new_symbol_table.lookup_ref(generic_inner_inner_class_prefix); + + THEN("It has correct generic types and implicit generic types") + { + require_type::require_java_implicitly_generic_class( + class_symbol.type, + {outer_class_prefix + "::T", outer_class_prefix + "$GenericInner::U"}); + require_type::require_java_generic_class( + class_symbol.type, {generic_inner_inner_class_prefix + "::V"}); + } + } + + WHEN("A static generic inner class of a generic class is parsed") + { + std::string static_inner_class_prefix = outer_class_prefix + "$StaticInner"; + REQUIRE(new_symbol_table.has_symbol(static_inner_class_prefix)); + const symbolt &class_symbol = + new_symbol_table.lookup_ref(static_inner_class_prefix); + + THEN("It has correct generic types and no implicit generic types") + { + REQUIRE(!is_java_implicitly_generic_class_type(class_symbol.type)); + require_type::require_java_generic_class( + class_symbol.type, {static_inner_class_prefix + "::U"}); + } + } +} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp b/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp index cb6b6289502..ee2bbf373ee 100644 --- a/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp +++ b/unit/java_bytecode/java_bytecode_parse_generics/parse_signature_descriptor_mismatch.cpp @@ -28,7 +28,7 @@ SCENARIO( const symbolt &inner_symbol = new_symbol_table.lookup_ref(inner_prefix); const class_typet &inner_class_type = - require_type::require_java_non_generic_class(inner_symbol.type); + require_type::require_java_implicitly_generic_class(inner_symbol.type); } THEN( @@ -63,8 +63,7 @@ SCENARIO( const symbolt &inner_enum_symbol = new_symbol_table.lookup_ref(inner_enum_prefix); - const class_typet &inner_enum_class_type = - require_type::require_java_non_generic_class(inner_enum_symbol.type); + require_type::require_java_non_generic_class(inner_enum_symbol.type); } THEN( diff --git a/unit/testing-utils/require_type.cpp b/unit/testing-utils/require_type.cpp index 597b3c034e0..0ddc11100ca 100644 --- a/unit/testing-utils/require_type.cpp +++ b/unit/testing-utils/require_type.cpp @@ -270,6 +270,53 @@ java_generic_class_typet require_type::require_java_generic_class( return java_generic_class_type; } +/// Verify that a class is a complete, valid java implicitly generic class. +/// \param class_type: the class +/// \return: A reference to the java generic class type. +java_implicitly_generic_class_typet +require_type::require_java_implicitly_generic_class(const typet &class_type) +{ + const class_typet &class_class_type = require_complete_class(class_type); + java_class_typet java_class_type = to_java_class_type(class_class_type); + + REQUIRE(is_java_implicitly_generic_class_type(java_class_type)); + java_implicitly_generic_class_typet java_implicitly_generic_class_type = + to_java_implicitly_generic_class_type(java_class_type); + + return java_implicitly_generic_class_type; +} + +/// Verify that a class is a complete, valid java generic class with the +/// specified list of variables. +/// \param class_type: the class +/// \param type_variables: vector of type variables +/// \return: A reference to the java generic class type. +java_implicitly_generic_class_typet +require_type::require_java_implicitly_generic_class( + const typet &class_type, + const std::initializer_list &implicit_type_variables) +{ + const java_implicitly_generic_class_typet java_implicitly_generic_class_type = + require_type::require_java_implicitly_generic_class(class_type); + + const java_implicitly_generic_class_typet::implicit_generic_typest + &implicit_generic_type_vars = + java_implicitly_generic_class_type.implicit_generic_types(); + REQUIRE(implicit_generic_type_vars.size() == implicit_type_variables.size()); + REQUIRE( + std::equal( + implicit_type_variables.begin(), + implicit_type_variables.end(), + implicit_generic_type_vars.begin(), + [](const irep_idt &type_var_name, const java_generic_parametert ¶m) + { + REQUIRE(is_java_generic_parameter(param)); + return param.type_variable().get_identifier() == type_var_name; + })); + + return java_implicitly_generic_class_type; +} + /// Verify that a class is a complete, valid nongeneric java class /// \param class_type: the class /// \return: A reference to the java generic class type. @@ -280,6 +327,7 @@ require_type::require_java_non_generic_class(const typet &class_type) java_class_typet java_class_type = to_java_class_type(class_class_type); REQUIRE(!is_java_generic_class_type(java_class_type)); + REQUIRE(!is_java_implicitly_generic_class_type(java_class_type)); return java_class_type; } diff --git a/unit/testing-utils/require_type.h b/unit/testing-utils/require_type.h index bf9da4c2bfb..eb13fed9614 100644 --- a/unit/testing-utils/require_type.h +++ b/unit/testing-utils/require_type.h @@ -76,6 +76,13 @@ java_generic_class_typet require_java_generic_class( const typet &class_type, const std::initializer_list &type_parameters); +java_implicitly_generic_class_typet +require_java_implicitly_generic_class(const typet &class_type); + +java_implicitly_generic_class_typet require_java_implicitly_generic_class( + const typet &class_type, + const std::initializer_list &implicit_type_variables); + java_class_typet require_java_non_generic_class(const typet &class_type); }