From 808a6ad1d1d9d32a3bf5dd24cf1d915d5d889ae9 Mon Sep 17 00:00:00 2001 From: thk123 Date: Mon, 4 Sep 2017 14:35:43 +0100 Subject: [PATCH 1/2] Created basic class for creating new java instantiations of classes --- src/java_bytecode/Makefile | 1 + .../generate_java_generic_type.cpp | 92 +++++++++++++++++++ .../generate_java_generic_type.h | 36 ++++++++ .../generate_java_generic_type.cpp | 50 ++++++++++ 4 files changed, 179 insertions(+) create mode 100644 src/java_bytecode/generate_java_generic_type.cpp create mode 100644 src/java_bytecode/generate_java_generic_type.h create mode 100644 unit/java_bytecode/generate_java_generic_type.cpp diff --git a/src/java_bytecode/Makefile b/src/java_bytecode/Makefile index 06a7d55757e..61e0e474b42 100644 --- a/src/java_bytecode/Makefile +++ b/src/java_bytecode/Makefile @@ -25,6 +25,7 @@ SRC = bytecode_info.cpp \ java_string_library_preprocess.cpp \ java_types.cpp \ java_utils.cpp \ + generate_java_generic_type.cpp \ mz_zip_archive.cpp \ select_pointer_type.cpp \ # Empty last line diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp new file mode 100644 index 00000000000..a3cb564c9b0 --- /dev/null +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -0,0 +1,92 @@ +/*******************************************************************\ + + Module: MODULE NAME + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ +#include "generate_java_generic_type.h" +#include +#include +#include + +#include +#include + +generate_java_generic_typet::generate_java_generic_typet( + symbol_tablet &symbol_table, + message_handlert &message_handler): + symbol_table(symbol_table), + message_handler(message_handler) +{} + +symbolt generate_java_generic_typet::operator()( + const java_type_with_generic_typet &existing_generic_type) +{ + namespacet ns(symbol_table); + + const typet &pointer_subtype=ns.follow(existing_generic_type.subtype()); + + INVARIANT( + pointer_subtype.id()==ID_struct, "Only pointers to classes in java"); + + const java_class_typet &java_class=to_java_class_type(pointer_subtype); + + java_class_typet replacement_type=java_class; + replacement_type.components().clear(); + + const irep_idt new_tag=build_generic_tag(existing_generic_type, java_class); + replacement_type.set_tag(new_tag); + + for(const struct_union_typet::componentt &component_type : + java_class.components()) + { + if(!is_java_generic_type(component_type.type())) + { + replacement_type.components().push_back(component_type); + continue; + } + + INVARIANT( + existing_generic_type.type_parameters.size()==1, + "Must have a type parameter"); + + struct_union_typet::componentt replacement_comp=component_type; + replacement_comp.type()=existing_generic_type.type_parameters[0]; + + replacement_type.components().push_back(replacement_comp); + + } + INVARIANT( + replacement_type.components().size()==java_class.components().size(), + "All components in the original class should be in the new class"); + + generate_class_stub(new_tag, symbol_table, message_handler); + INVARIANT(symbol_table.has_symbol("java::"+id2string(new_tag)), "New class not created"); + return symbol_table.lookup("java::"+id2string(new_tag)); +} + +irep_idt generate_java_generic_typet::build_generic_tag( + const java_type_with_generic_typet &existing_generic_type, + const java_class_typet &original_class) +{ + std::ostringstream new_tag_buffer; + new_tag_buffer << original_class.get_tag(); + new_tag_buffer << "<"; + bool first=true; + for(const typet ¶m : existing_generic_type.type_parameters) + { + if(!first) + new_tag_buffer << ", "; + first=false; + + INVARIANT( + is_java_inst_generic_type(param), + "Only create full concretized generic types"); + new_tag_buffer << param.subtype().get(ID_identifier); + } + + new_tag_buffer << ">"; + + return new_tag_buffer.str(); +} diff --git a/src/java_bytecode/generate_java_generic_type.h b/src/java_bytecode/generate_java_generic_type.h new file mode 100644 index 00000000000..03cf81a17d6 --- /dev/null +++ b/src/java_bytecode/generate_java_generic_type.h @@ -0,0 +1,36 @@ +/*******************************************************************\ + + Module: MODULE NAME + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ +#ifndef GENERATE_JAVA_GENERIC_TYPE_H +#define GENERATE_JAVA_GENERIC_TYPE_H + +#include +#include +#include +#include + +class generate_java_generic_typet +{ +public: + generate_java_generic_typet( + symbol_tablet &symbol_table, + message_handlert &message_handler); + + symbolt operator()( + const java_type_with_generic_typet &existing_generic_type); +private: + irep_idt build_generic_tag( + const java_type_with_generic_typet &existing_generic_type, + const java_class_typet &original_class); + + symbol_tablet &symbol_table; + + message_handlert &message_handler; + +}; + +#endif // GENERATE_JAVA_GENERIC_TYPE_H diff --git a/unit/java_bytecode/generate_java_generic_type.cpp b/unit/java_bytecode/generate_java_generic_type.cpp new file mode 100644 index 00000000000..a868d86b182 --- /dev/null +++ b/unit/java_bytecode/generate_java_generic_type.cpp @@ -0,0 +1,50 @@ +/*******************************************************************\ + + Module: Unit tests for generating new type with generic parameters + substitued for concrete types + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include + +#include + +#include +#include + +SCENARIO( + "generate_java_generic_type", + "[CORE][java_bytecode][generate_java_generic_type") +{ + GIVEN("A generic java type and a concrete substitution") + { + symbol_tablet symbol_table; + + + null_message_handlert message_handler; + generate_java_generic_typet type_generator(symbol_table, message_handler); + + + const reference_typet &boxed_integer_type=to_reference_type(java_type_from_string("Ljava/lang/Integer;")); + + java_type_with_generic_typet generic_type; + generic_type.type_parameters.push_back(java_inst_generic_typet(boxed_integer_type)); + + struct_typet base_class; + base_class.components().push_back(struct_union_typet::componentt("a", java_generic_typet("T"))); + base_class.set_tag("UserClass"); + + generic_type.subtype()=base_class; + + const symbolt &new_symbol=type_generator(generic_type); + REQUIRE(new_symbol.is_type); + + + + REQUIRE(new_symbol.base_name=="UserClass"); + REQUIRE(new_symbol.type.id()==ID_pointer); + + } +} From d735cc54e42faff7fe73f5199094afda3df47a5f Mon Sep 17 00:00:00 2001 From: Fotis Koutoulakis Date: Tue, 19 Sep 2017 17:10:19 +0100 Subject: [PATCH 2/2] Added support for concretising a generic and adding it into the symbol table. --- .../generics$bound_element.class | Bin 0 -> 892 bytes .../generics_symtab1/generics$element.class | Bin 0 -> 573 bytes .../cbmc-java/generics_symtab1/generics.class | Bin 0 -> 1032 bytes .../cbmc-java/generics_symtab1/generics.java | 31 ++++ .../cbmc-java/generics_symtab1/test.desc | 8 + .../generate_java_generic_type.cpp | 159 ++++++++++++----- .../generate_java_generic_type.h | 24 +-- .../java_bytecode_convert_class.cpp | 3 +- .../java_bytecode_instrument.cpp | 3 +- src/java_bytecode/java_bytecode_language.cpp | 19 +- src/java_bytecode/java_types.h | 28 +++ src/java_bytecode/java_utils.cpp | 23 ++- src/java_bytecode/java_utils.h | 11 +- .../generate_java_generic_type.cpp | 162 ++++++++++++++++++ .../generic_two_fields$bound_element.class | Bin 0 -> 699 bytes .../generic_two_fields.class | Bin 0 -> 495 bytes .../generic_two_fields.java | 11 ++ .../generic_two_instances$element.class | Bin 0 -> 664 bytes .../generic_two_instances.class | Bin 0 -> 581 bytes .../generic_two_instances.java | 8 + .../generic_two_parameters$KeyValuePair.class | Bin 0 -> 743 bytes .../generic_two_parameters.class | Bin 0 -> 1009 bytes .../generic_two_parameters.java | 22 +++ .../generic_unknown_field$G.class | Bin 0 -> 738 bytes .../generic_unknown_field$element.class | Bin 0 -> 664 bytes .../generic_unknown_field.class | Bin 0 -> 405 bytes .../generic_unknown_field.java | 9 + .../generate_java_generic_type.cpp | 50 ------ .../generics05$igeneric05.class | Bin 0 -> 856 bytes 29 files changed, 462 insertions(+), 109 deletions(-) create mode 100644 regression/cbmc-java/generics_symtab1/generics$bound_element.class create mode 100644 regression/cbmc-java/generics_symtab1/generics$element.class create mode 100644 regression/cbmc-java/generics_symtab1/generics.class create mode 100644 regression/cbmc-java/generics_symtab1/generics.java create mode 100644 regression/cbmc-java/generics_symtab1/test.desc create mode 100644 unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp create mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_two_fields$bound_element.class create mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_two_fields.class create mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_two_fields.java create mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_two_instances$element.class create mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_two_instances.class create mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_two_instances.java create mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters$KeyValuePair.class create mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters.class create mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters.java create mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field$G.class create mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field$element.class create mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field.class create mode 100644 unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field.java delete mode 100644 unit/java_bytecode/generate_java_generic_type.cpp create mode 100644 unit/java_bytecode/java_bytecode_parse_generics/generics05$igeneric05.class diff --git a/regression/cbmc-java/generics_symtab1/generics$bound_element.class b/regression/cbmc-java/generics_symtab1/generics$bound_element.class new file mode 100644 index 0000000000000000000000000000000000000000..8076c290e12a9de020c7afdf303b3f7c5adbd307 GIT binary patch literal 892 zcmZ`%U2oGs5S)u+yD?51LJ8%wKm#~IqCD^fQ6y9e2`Ln$mOk);ob(!8xejt1B>ojh zAS5360sJV$>|IhfDm>WU+nt@Ao%8QMKYsyuf=&%p+zH^~u0&ft?)kW{P}QkEQD_d1 z<4^H+8fW9}-Py@d=g$;sd&xM9i&?G}-2L6RubA_S56QIsSRojUb*A%VG?i>G$&#Y4 zP>;%V=YaG(lS6i|4U$Y--u-x(GSeJPMsa!&=ZT!>$*Pc(WH^~+hwnw1&I*O_WyVQ6 zX*`{3mN!mEw3mR?(OPEx{Bgm&`JbMiS*y=hb)>K!b^hgpA9d#2tFgl6=sZSNRorSN zGC(hs8 z6dL6%T5bg=5;ZG}4&3JLyZj|8e8>mZ%&FFB$Rx%NpAdCcRvEn^Qm{ey;diL+4^+My z%o^VwF(5~S@0La3BG!2#-muXw#-YIlthG$-3O0xq_UEh!hui%I=L-V|C2?SgZL>Qk zF6ksAbXNXVM%QqCPWz5uv!IA}O2L82)@i`%8PVRUXb(4xB{Ib>BsD8qYBh?r^KMe9 Ujc#F+=n9R!#BV@E6>T(uzpNdiDgXcg literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/generics_symtab1/generics$element.class b/regression/cbmc-java/generics_symtab1/generics$element.class new file mode 100644 index 0000000000000000000000000000000000000000..34cb36e36b49a205496b9dd54785cf9216aaf601 GIT binary patch literal 573 zcmZWmO;5r=5PeH4g;Jze1;6FM0WlE|o|JGQn3yzb0^z>Y4K68*X^V+J%Y!lT;1BRe z8E27dl*8`Mym|BHV?RFM-T|DUnumdH8zy!v>{-}nFhwXP44yyckGvUjHEP}r$0A5B z81g+iQaqVOg2Cu_3CSk+GOnF6*#1Z;5y>FdXiF-Yv>A%^U-)Q1;+^Ro<(7P@#Pw`4 z6j7fKLqa@%8t`zyBdPrbXlii=OLrtx!r)vfs?iB~9199~KjO6og=&}oDm^`pb4G+dhaGk$|6 zB{h;5pZxo));RKkcNtK(i6KIFnMkT+-*bQHq~ zB4@zFeH{-J^UxsjNJmM>V}WR+GjR4_%eFj}PG7*RI*#maw5?uG_5^f~2sD%_kf^mJ zJ?v&LbuP3lVASoFWAz7JDUiRwtx`L%j;&(ba$3cz)0ZvTEw3>)Sg{?uzb4>MXLbd& zjm|!^%+zd0ZVwI{vir(vw28!Oou<{^wYs+Yo`PEcolUV}uO<_Uw*v8WHS?c(Bpt3Q z*Epls(6m`b`x<28=WBg9a_g;lg;LXyi`t6T`&RS)mUT2%$_wI+P-wj~=r-j`TXht5 z%NNvSOe`QSFzbSD0fj#?@f1rYR`HDDJdbnNU}6q2fw_OCtP(s|vFtA7#?O4~rw9)bNq$5mcY?ro7@zVdh^UjfG^qNw5#qkUUnfra zi>#f%GS!r5ty0H2H7IS_NqtY-Ca&WK)fsq!n;e3VOo7>A@Z%2s<3uK0%H!tA-6a=+ e_=R;H%Q{v_rV06w!3@tBtsn<+X^fee1^xi|W7(tt literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/generics_symtab1/generics.java b/regression/cbmc-java/generics_symtab1/generics.java new file mode 100644 index 00000000000..0a0af41c63a --- /dev/null +++ b/regression/cbmc-java/generics_symtab1/generics.java @@ -0,0 +1,31 @@ +public class generics { + + class element { + E elem; + } + + class bound_element { + NUM elem; + NUM f() { + return elem; + } + void g(NUM e) { + elem=e; + } + } + + bound_element belem; + + Integer f(int n) { + + element e=new element<>(); + e.elem=n; + bound_element be=new bound_element<>(); + belem=new bound_element<>(); + be.elem=new Integer(n+1); + if(n>0) + return e.elem; + else + return be.elem; + } +} diff --git a/regression/cbmc-java/generics_symtab1/test.desc b/regression/cbmc-java/generics_symtab1/test.desc new file mode 100644 index 00000000000..fe6b3693bf3 --- /dev/null +++ b/regression/cbmc-java/generics_symtab1/test.desc @@ -0,0 +1,8 @@ +CORE +generics.class +--show-symbol-table +^EXIT=0$ +^SIGNAL=0$ +^Type........: struct generics\$bound_element\ \{ +__CPROVER_string \@class_identifier; boolean \@lock; struct java.lang.Object \@java.lang.Object; struct java.lang.Integer \*elem; struct generics \*this\$0; \}$ +-- diff --git a/src/java_bytecode/generate_java_generic_type.cpp b/src/java_bytecode/generate_java_generic_type.cpp index a3cb564c9b0..6c6cbc4e1c8 100644 --- a/src/java_bytecode/generate_java_generic_type.cpp +++ b/src/java_bytecode/generate_java_generic_type.cpp @@ -1,6 +1,7 @@ /*******************************************************************\ - Module: MODULE NAME + Module: Generate Java Generic Type - Instantiate a generic class with + concrete type information. Author: DiffBlue Limited. All rights reserved. @@ -10,18 +11,21 @@ #include #include -#include -#include generate_java_generic_typet::generate_java_generic_typet( - symbol_tablet &symbol_table, message_handlert &message_handler): - symbol_table(symbol_table), message_handler(message_handler) {} +/// Generate a concrete instantiation of a generic type. +/// \param existing_generic_type The type to be concretised +/// \param symbol_table The symbol table that the concrete type will be +/// inserted into. +/// \return The symbol as it was retrieved from the symbol table after +/// it has been inserted into. symbolt generate_java_generic_typet::operator()( - const java_type_with_generic_typet &existing_generic_type) + const java_generic_typet &existing_generic_type, + symbol_tablet &symbol_table) const { namespacet ns(symbol_table); @@ -30,58 +34,90 @@ symbolt generate_java_generic_typet::operator()( INVARIANT( pointer_subtype.id()==ID_struct, "Only pointers to classes in java"); - const java_class_typet &java_class=to_java_class_type(pointer_subtype); - - java_class_typet replacement_type=java_class; - replacement_type.components().clear(); - - const irep_idt new_tag=build_generic_tag(existing_generic_type, java_class); - replacement_type.set_tag(new_tag); - - for(const struct_union_typet::componentt &component_type : - java_class.components()) - { - if(!is_java_generic_type(component_type.type())) + const java_class_typet &replacement_type= + to_java_class_type(pointer_subtype); + const irep_idt new_tag=build_generic_tag( + existing_generic_type, replacement_type); + struct_union_typet::componentst replacement_components= + replacement_type.components(); + + // Small auxiliary function, to perform the inplace + // modification of the generic fields. + auto replace_type_for_generic_field= + [&](struct_union_typet::componentt &component) { - replacement_type.components().push_back(component_type); - continue; - } + if(is_java_generic_parameter(component.type())) + { + auto replacement_type_param= + to_java_generics_class_type(replacement_type); + + auto component_identifier= + to_java_generic_parameter(component.type()).type_variable() + .get_identifier(); + + optionalt results=java_generics_get_index_for_subtype( + replacement_type_param, component_identifier); + + INVARIANT( + results.has_value(), + "generic component type not found"); + + if(results) + { + component.type()= + existing_generic_type.generic_type_variables()[*results]; + } + } + return component; + }; + + std::size_t pre_modification_size=to_java_class_type( + ns.follow(existing_generic_type.subtype())).components().size(); + + std::for_each( + replacement_components.begin(), + replacement_components.end(), + replace_type_for_generic_field); + + std::size_t after_modification_size= + replacement_type.components().size(); - INVARIANT( - existing_generic_type.type_parameters.size()==1, - "Must have a type parameter"); - - struct_union_typet::componentt replacement_comp=component_type; - replacement_comp.type()=existing_generic_type.type_parameters[0]; - - replacement_type.components().push_back(replacement_comp); - - } INVARIANT( - replacement_type.components().size()==java_class.components().size(), + pre_modification_size==after_modification_size, "All components in the original class should be in the new class"); - generate_class_stub(new_tag, symbol_table, message_handler); - INVARIANT(symbol_table.has_symbol("java::"+id2string(new_tag)), "New class not created"); - return symbol_table.lookup("java::"+id2string(new_tag)); + const auto expected_symbol="java::"+id2string(new_tag); + + generate_class_stub( + new_tag, + symbol_table, + message_handler, + replacement_components); + auto symbol=symbol_table.lookup(expected_symbol); + INVARIANT(symbol, "New class not created"); + return *symbol; } +/// Build a unique tag for the generic to be instantiated. +/// \param existing_generic_type The type we want to concretise +/// \param original_class +/// \return A tag for the new generic we want a unique tag for. irep_idt generate_java_generic_typet::build_generic_tag( - const java_type_with_generic_typet &existing_generic_type, - const java_class_typet &original_class) + const java_generic_typet &existing_generic_type, + const java_class_typet &original_class) const { std::ostringstream new_tag_buffer; new_tag_buffer << original_class.get_tag(); new_tag_buffer << "<"; bool first=true; - for(const typet ¶m : existing_generic_type.type_parameters) + for(const typet ¶m : existing_generic_type.generic_type_variables()) { if(!first) - new_tag_buffer << ", "; + new_tag_buffer << ","; first=false; INVARIANT( - is_java_inst_generic_type(param), + is_java_generic_inst_parameter(param), "Only create full concretized generic types"); new_tag_buffer << param.subtype().get(ID_identifier); } @@ -90,3 +126,46 @@ irep_idt generate_java_generic_typet::build_generic_tag( return new_tag_buffer.str(); } + + +/// Activate the generic instantiation code. +/// \param message_handler +/// \param symbol_table The symbol table so far. +void +instantiate_generics( + message_handlert &message_handler, + symbol_tablet &symbol_table) +{ + generate_java_generic_typet instantiate_generic_type(message_handler); + // check out the symbols in the symbol table at this point to see if we + // have a a generic type in. + for(const auto &symbol : symbol_table.symbols) + { + if(symbol.second.type.id()==ID_struct) + { + auto symbol_struct=to_struct_type(symbol.second.type); + auto &components=symbol_struct.components(); + + for(const auto &component : components) + { + if(is_java_generic_type(component.type())) + { + const auto &type_vars=to_java_generic_type(component.type()). + generic_type_variables(); + + // Before we can instantiate a generic component, we need + // its type variables to be instantiated parameters + if(all_of(type_vars.cbegin(), type_vars.cend(), + [](const typet &type) + { + return is_java_generic_inst_parameter(type); + })) + { + instantiate_generic_type( + to_java_generic_type(component.type()), symbol_table); + } + } + } + } + } +} diff --git a/src/java_bytecode/generate_java_generic_type.h b/src/java_bytecode/generate_java_generic_type.h index 03cf81a17d6..6ba48378a31 100644 --- a/src/java_bytecode/generate_java_generic_type.h +++ b/src/java_bytecode/generate_java_generic_type.h @@ -1,12 +1,13 @@ /*******************************************************************\ - Module: MODULE NAME + Module: Generate Java Generic Type - Instantiate a generic class with + concrete type information. Author: DiffBlue Limited. All rights reserved. \*******************************************************************/ -#ifndef GENERATE_JAVA_GENERIC_TYPE_H -#define GENERATE_JAVA_GENERIC_TYPE_H +#ifndef CPROVER_JAVA_BYTECODE_GENERATE_JAVA_GENERIC_TYPE_H +#define CPROVER_JAVA_BYTECODE_GENERATE_JAVA_GENERIC_TYPE_H #include #include @@ -17,20 +18,21 @@ class generate_java_generic_typet { public: generate_java_generic_typet( - symbol_tablet &symbol_table, message_handlert &message_handler); symbolt operator()( - const java_type_with_generic_typet &existing_generic_type); + const java_generic_typet &existing_generic_type, + symbol_tablet &symbol_table) const; private: irep_idt build_generic_tag( - const java_type_with_generic_typet &existing_generic_type, - const java_class_typet &original_class); - - symbol_tablet &symbol_table; + const java_generic_typet &existing_generic_type, + const java_class_typet &original_class) const; message_handlert &message_handler; - }; -#endif // GENERATE_JAVA_GENERIC_TYPE_H +void instantiate_generics( + message_handlert &message_handler, + symbol_tablet &symbol_table); + +#endif // CPROVER_JAVA_BYTECODE_GENERATE_JAVA_GENERIC_TYPE_H diff --git a/src/java_bytecode/java_bytecode_convert_class.cpp b/src/java_bytecode/java_bytecode_convert_class.cpp index 8f038c92440..9270e1fa0cd 100644 --- a/src/java_bytecode/java_bytecode_convert_class.cpp +++ b/src/java_bytecode/java_bytecode_convert_class.cpp @@ -63,7 +63,8 @@ class java_bytecode_convert_classt:public messaget generate_class_stub( parse_tree.parsed_class.name, symbol_table, - get_message_handler()); + get_message_handler(), + struct_union_typet::componentst{}); } typedef java_bytecode_parse_treet::classt classt; diff --git a/src/java_bytecode/java_bytecode_instrument.cpp b/src/java_bytecode/java_bytecode_instrument.cpp index 31c18fab721..66f62e6ff78 100644 --- a/src/java_bytecode/java_bytecode_instrument.cpp +++ b/src/java_bytecode/java_bytecode_instrument.cpp @@ -100,7 +100,8 @@ codet java_bytecode_instrumentt::throw_exception( generate_class_stub( exc_name, symbol_table, - get_message_handler()); + get_message_handler(), + struct_union_typet::componentst{}); } pointer_typet exc_ptr_type= diff --git a/src/java_bytecode/java_bytecode_language.cpp b/src/java_bytecode/java_bytecode_language.cpp index cd6210bdb8f..a4b15d8b963 100644 --- a/src/java_bytecode/java_bytecode_language.cpp +++ b/src/java_bytecode/java_bytecode_language.cpp @@ -30,6 +30,7 @@ Author: Daniel Kroening, kroening@kroening.com #include "java_class_loader.h" #include "java_utils.h" #include +#include #include "expr2java.h" @@ -238,11 +239,21 @@ bool java_bytecode_languaget::typecheck( get_message_handler()); // now typecheck all - if(java_bytecode_typecheck( - symbol_table, get_message_handler(), string_refinement_enabled)) - return true; + bool res=java_bytecode_typecheck( + symbol_table, get_message_handler(), string_refinement_enabled); + // NOTE (FOTIS): There is some unintuitive logic here, where + // java_bytecode_check will return TRUE if typechecking failed, and FALSE + // if everything went well... + if(res) + { + // there is no point in continuing to concretise + // the generic types if typechecking failed. + return res; + } - return false; + instantiate_generics(get_message_handler(), symbol_table); + + return res; } bool java_bytecode_languaget::generate_support_functions( diff --git a/src/java_bytecode/java_types.h b/src/java_bytecode/java_types.h index e4c370157e0..b2ba6b7777d 100644 --- a/src/java_bytecode/java_types.h +++ b/src/java_bytecode/java_types.h @@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com #define CPROVER_JAVA_BYTECODE_JAVA_TYPES_H #include +#include + #include #include #include @@ -379,4 +381,30 @@ inline typet java_type_from_string_with_exception( } } +/// Get the index in the subtypes array for a given component. +/// \param t The type we search for the subtypes in. +/// \param identifier The string identifier of the type of the component. +/// \return Optional with the size if the identifier was found. +inline const optionalt java_generics_get_index_for_subtype( + const java_generics_class_typet &t, + const irep_idt &identifier) +{ + const std::vector &gen_types=t.generic_types(); + + const auto iter = std::find_if( + gen_types.cbegin(), + gen_types.cend(), + [&identifier](const java_generic_parametert &ref) + { + return ref.type_variable().get_identifier()==identifier; + }); + + if(iter==gen_types.cend()) + { + return {}; + } + + return std::distance(gen_types.cbegin(), iter); +} + #endif // CPROVER_JAVA_BYTECODE_JAVA_TYPES_H diff --git a/src/java_bytecode/java_utils.cpp b/src/java_bytecode/java_utils.cpp index 6521f9903d6..8f366c324e3 100644 --- a/src/java_bytecode/java_utils.cpp +++ b/src/java_bytecode/java_utils.cpp @@ -67,7 +67,8 @@ const std::string java_class_to_package(const std::string &canonical_classname) void generate_class_stub( const irep_idt &class_name, symbol_tablet &symbol_table, - message_handlert &message_handler) + message_handlert &message_handler, + const struct_union_typet::componentst &componentst) { class_typet class_type; @@ -100,6 +101,7 @@ void generate_class_stub( { // create the class identifier etc java_root_class(res.first); + java_add_components_to_class(res.first, componentst); } } @@ -230,3 +232,22 @@ size_t find_closing_delimiter( // did not find corresponding closing '>' return std::string::npos; } + +/// Add the components in components_to_add to the class denoted by +/// class symbol. +/// \param class_symbol The symbol representing the class we want to modify. +/// \param components_to_add The vector with the components we want to add. +void java_add_components_to_class( + symbolt &class_symbol, + const struct_union_typet::componentst &components_to_add) +{ + PRECONDITION(class_symbol.is_type); + PRECONDITION(class_symbol.type.id()==ID_struct); + struct_typet &struct_type=to_struct_type(class_symbol.type); + struct_typet::componentst &components=struct_type.components(); + + for(const struct_union_typet::componentt &component : components_to_add) + { + components.push_back(component); + } +} diff --git a/src/java_bytecode/java_utils.h b/src/java_bytecode/java_utils.h index 9428494db93..774bb350572 100644 --- a/src/java_bytecode/java_utils.h +++ b/src/java_bytecode/java_utils.h @@ -18,7 +18,8 @@ bool java_is_array_type(const typet &type); void generate_class_stub( const irep_idt &class_name, symbol_tablet &symbol_table, - message_handlert &message_handler); + message_handlert &message_handler, + const struct_union_typet::componentst &componentst); /// Returns the number of JVM local variables (slots) taken by a local variable /// that, when translated to goto, has type \p t. @@ -66,6 +67,14 @@ irep_idt resolve_friendly_method_name( /// \param type: expected result type (typically expr.type().subtype()) dereference_exprt checked_dereference(const exprt &expr, const typet &type); +/// Add the components in components_to_add to the class denoted +/// by class symbol. +/// \param class_symbol The symbol representing the class we want to modify. +/// \param components_to_add The vector with the components we want to add. +void java_add_components_to_class( + symbolt &class_symbol, + const struct_union_typet::componentst &components_to_add); + size_t find_closing_delimiter( const std::string &src, size_t position, diff --git a/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp new file mode 100644 index 00000000000..7ea813cc4d9 --- /dev/null +++ b/unit/java_bytecode/generate_concrete_generic_type/generate_java_generic_type.cpp @@ -0,0 +1,162 @@ +/*******************************************************************\ + + Module: Unit tests for generating new type with generic parameters + substitued for concrete types + + Author: DiffBlue Limited. All rights reserved. + +\*******************************************************************/ + +#include +#include + +#include + +#include + + +SCENARIO( + "generate_java_generic_type_from_file", + "[core][java_bytecode][generate_java_generic_type]") +{ + auto expected_symbol= + "java::generic_two_fields$bound_element"; + + GIVEN("A generic java type with two generic fields and a concrete " + "substitution") + { + symbol_tablet new_symbol_table= + load_java_class("generic_two_fields", + "./java_bytecode/generate_concrete_generic_type"); + + REQUIRE(new_symbol_table.has_symbol(expected_symbol)); + THEN("The class should contain two instantiated fields.") + { + const auto &class_symbol=new_symbol_table.lookup( + "java::generic_two_fields$bound_element"); + const typet &symbol_type=class_symbol->type; + + REQUIRE(symbol_type.id()==ID_struct); + class_typet class_type=to_class_type(symbol_type); + REQUIRE(class_type.is_class()); + + REQUIRE(class_type.has_component("first")); + const auto &first_component=class_type.get_component("first"); + REQUIRE(is_java_generic_inst_parameter(first_component.type())); + REQUIRE(first_component.type().id()==ID_pointer); + REQUIRE(first_component.type().subtype().id()==ID_symbol); + REQUIRE(to_symbol_type( + first_component.type().subtype()).get_identifier()== + "java::java.lang.Integer"); + REQUIRE(class_type.has_component("second")); + const auto &second_component=class_type.get_component("second"); + REQUIRE(is_java_generic_inst_parameter(second_component.type())); + REQUIRE(second_component.type().id()==ID_pointer); + REQUIRE(second_component.type().subtype().id()==ID_symbol); + REQUIRE(to_symbol_type( + second_component.type().subtype()).get_identifier()== + "java::java.lang.Integer"); + } + } +} + + +SCENARIO( + "generate_java_generic_type_from_file_two_params", + "[core][java_bytecode][generate_java_generic_type]") +{ + auto expected_symbol= + "java::generic_two_parameters$KeyValuePair" + ""; + + GIVEN("A generic java type with two generic parameters, like a Hashtable") + { + symbol_tablet new_symbol_table= + load_java_class("generic_two_parameters", + "./java_bytecode/generate_concrete_generic_type"); + + REQUIRE(new_symbol_table.has_symbol( + "java::generic_two_parameters$KeyValuePair")); + THEN("The class should have two subtypes in the vector of the types of " + "the generic components.") + { + const auto &class_symbol=new_symbol_table.lookup( + expected_symbol); + const typet &symbol_type=class_symbol->type; + + REQUIRE(symbol_type.id()==ID_struct); + class_typet class_type=to_class_type(symbol_type); + REQUIRE(class_type.is_class()); + + REQUIRE(class_type.has_component("key")); + const auto &first_component=class_type.get_component("key"); + REQUIRE(is_java_generic_inst_parameter(first_component.type())); + REQUIRE(class_type.has_component("value")); + const auto &second_component=class_type.get_component("value"); + REQUIRE(is_java_generic_inst_parameter(second_component.type())); + } + } +} + + +SCENARIO( + "generate_java_generic_type_from_file_uninstantiated_param", + "[core][java_bytecode][generate_java_generic_type]") +{ + GIVEN("A generic java type with a field that refers to another generic with" + " an uninstantiated parameter.") + { + symbol_tablet new_symbol_table= + load_java_class("generic_unknown_field", + "./java_bytecode/generate_concrete_generic_type"); + + // It's illegal to create an instantiation of a field that refers + // to a (still) uninstantiated generic class, so this is checking that + // this hasn't happened. + REQUIRE_FALSE(new_symbol_table.has_symbol + ("java::generic_unknown_field$element")); + } +} + + +SCENARIO( + "generate_java_generic_type_from_file_two_instances", + "[core][java_bytecode][generate_java_generic_type]") +{ + // After we have loaded the class and converted the generics, + // the presence of these two symbols in the symbol table is + // proof enough that we did the work we needed to do correctly. + auto first_expected_symbol= + "java::generic_two_instances$element"; + auto second_expected_symbol= + "java::generic_two_instances$element"; + + GIVEN("A generic java type with a field that refers to another generic with" + " an uninstantiated parameter.") + { + symbol_tablet new_symbol_table= + load_java_class("generic_two_instances", + "./java_bytecode/generate_concrete_generic_type"); + + REQUIRE(new_symbol_table.has_symbol(first_expected_symbol)); + auto first_symbol=new_symbol_table.lookup(first_expected_symbol); + REQUIRE(first_symbol->type.id()==ID_struct); + auto first_symbol_type= + to_struct_type(first_symbol->type).components()[3].type(); + REQUIRE(first_symbol_type.id()==ID_pointer); + REQUIRE(first_symbol_type.subtype().id()==ID_symbol); + REQUIRE(to_symbol_type(first_symbol_type.subtype()).get_identifier()== + "java::java.lang.Boolean"); + + REQUIRE(new_symbol_table.has_symbol(second_expected_symbol)); + auto second_symbol=new_symbol_table.lookup(second_expected_symbol); + REQUIRE(second_symbol->type.id()==ID_struct); + auto second_symbol_type= + to_struct_type(second_symbol->type).components()[3].type(); + REQUIRE(second_symbol_type.id()==ID_pointer); + REQUIRE(second_symbol_type.subtype().id()==ID_symbol); + REQUIRE(to_symbol_type(second_symbol_type.subtype()).get_identifier()== + "java::java.lang.Integer"); + } +} diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_two_fields$bound_element.class b/unit/java_bytecode/generate_concrete_generic_type/generic_two_fields$bound_element.class new file mode 100644 index 0000000000000000000000000000000000000000..0e61e55d0dea065a0a62964d01ce3c42dd73a3d1 GIT binary patch literal 699 zcmah{%T5A85UgQQWL*_e!MA8Q04CzWlM*f_CMNhud|b)0j5ubUHM@((&+=eQJoo{A zl(7ahN-*&-JzYK3T|GVX{_*+-UNT&XaM1+tAB_uj4guI^Ni zySFVF?g^yNR7bmUHd)G}0FGkyq~S4#Tr$PjBv ztGF(ZFa1R*UkW7mgEmV~HI$Zp(Q~)uGm>otp6g$_p)&X@m^6X{6Rn`D+fC`qTdCQ( zbEv7l@4HbXdA#w5SaBeQz2ye$Ki++7l>g1H_2y7#kxGpd*&Uu+{a5IubtAo)Wcw`W zhMqi7=6d0voMWWBJz9H f1m@^FJ)X_89Fg_aK_2r&2`pfy$LB4uj4bd8Mnk7< literal 0 HcmV?d00001 diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_two_fields.class b/unit/java_bytecode/generate_concrete_generic_type/generic_two_fields.class new file mode 100644 index 0000000000000000000000000000000000000000..5d14a465aaf2fc9af840739223d64c194b918e84 GIT binary patch literal 495 zcmah_O-sW-5Ph3AjjgGzwOWrV9<&E@5j?c?QVT2f3K(z$>;)0)z0EVGO< z0Xr}ifipiM##Ok?Uy|jcqIi{^Z?%pDnsXItnHMPu-2B@x_Sf=Rda=}zH`6&ql#V8> z(ikhP@`*t0;&LHSpC&8T>-b93U9kx$eUL%SNY76~882k2O#TDb^C!h?_y3sA(ye(? zq#@lZ(?6*G=*n#5VizvUSIYw3-<9u!HHCbzlPYifFgS(9M+XEy2RrPW99d{_B+M|j qZAQE@2khY+#A`{}W7}ZZG { + NUM first; + NUM second; + } + + bound_element belem; +} diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_two_instances$element.class b/unit/java_bytecode/generate_concrete_generic_type/generic_two_instances$element.class new file mode 100644 index 0000000000000000000000000000000000000000..3229b26a8326ae4ab6b3afdfedf403cc75933b23 GIT binary patch literal 664 zcmaJ;O;5r=5Pb{PN~uy&Kv9GP2gF1?cv8ZJ#KeTC2@O}W)D12vi)o9-pXI@rc<=}K zql~i%2c>%0-I>`p@6E@@=i57gQ&dt&V%LI!qKSPIB?d$IV$6{3jQ9g@_*@Me*MpJp zqH~5+R}K}Arh#Bcx-LalqdOT^PZ$cFp->`_UO#%A^rZ?Tt~?QHNK+~qwHS)EKQMC2E=9M&&^XbS2{6L`;?rn2m^u5sS30-X-oqBzu7}~As?j^N*y>?yoRJ6jCe#{ zX|rDWk0BFnD4;kWQX49*%t)Yoc0LoRjH7$LsOc(AH|f%&_)dBuXWDM$%Wx)RmEl#g zVjdJfzFT}hpJ-2`H1_FQWg~ipnp|d&YhVl80-ZvJKx-|)t+ybb^*<`4ehZ8fl=$nw z7O=1Z7Cc8b+xjou;0m(k?3)}p?6XYu;sxTFgA!V7Yk5*&hvTo7D%#l1>wCHFFbA-i JSK*#2@Cl)umY@It literal 0 HcmV?d00001 diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_two_instances.java b/unit/java_bytecode/generate_concrete_generic_type/generic_two_instances.java new file mode 100644 index 00000000000..48144b5ecaf --- /dev/null +++ b/unit/java_bytecode/generate_concrete_generic_type/generic_two_instances.java @@ -0,0 +1,8 @@ +class generic_two_instances { + class element { + T elem; + } + + element bool_element; + element int_element; +} diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters$KeyValuePair.class b/unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters$KeyValuePair.class new file mode 100644 index 0000000000000000000000000000000000000000..8c4e5674b68c64a89a6fa4994461bb71e705fa64 GIT binary patch literal 743 zcma)4%T59@6g_27WE=%i@qrIiOnk)0!j%vJ<%YbId!F>`duP># zs)c!h_=T?fGVBD3v`UGQp*!hyddMXj4zG1Pw=XbTt}9;!x^@}fw=QpGAe$;wLECT& z+Sg%GAhYooY10*m9<{Ehn<#5vopzd46;x!^V)uiXjKpXrSjGDv(PDyoLQ_#88 z0pW?yB91)SZY!Ry|B)}(e~T5Szh~&)er4JDk3fNQskr$fg$jkz;qNiJ17gMBGy(gf z)d_0qSev#pg9o~6Udh2I90y~_#;_u=HkkUYO@ZXk_vMprn8~LHUq_ZdCCX1@aSdS@ z0x^0KjL^pWu$@erdKeX4V;JY2pm$DgguA`9{Rpx3gvbMtg(R&}Gg=e0=?@lCm?k2> gr^dSIJ3XGwvl$}mvw~U75k)YMsUDx5U=fqRJ8HeQtN;K2 literal 0 HcmV?d00001 diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters.class b/unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters.class new file mode 100644 index 0000000000000000000000000000000000000000..2527db386759c91ac8add3793ffa91cf4399cdc1 GIT binary patch literal 1009 zcma)5T~8B16g|_g-EJ3wf<^HQg-T0>BH~98JNPdh7|)b%#A_~na;vT@{5^+vyQ0gGXnO4?L*8l$3QPMS z_~0FMxX;@n5Po-Mw79~MuFICogPt!KtpBOmv5xo&FFV|AmFs~o-Bx8JQgs8-5`JZu zpi?{2mBB7UyijaVV|(5^BAK?ND_-^5P2s=cO@|^`%d@%D;J#G;Aeac=OPc1|B`pzr z;;`r14D*HJ2>+lX21dZSao~RE0(`0-aQpZr?}TKeKZ8;CdcG~5OV!bh$=YqG$xY1T zD#P;Rlrec#>Lx?-g>W3t#6xVEc!X^ekFmutJJfNYnu#ZP$}lth5RF5#*1Qg>k(*39 zR#Iyo2|J(}3YSTzE+c*{`bzmBRa8g1YA5P#)eecSP#x9w;%;f8Foi*vZV80Kg}=|+(pS!Fs^PIB!V*yk{1f%a4wq)R8;j1q7ii{#NbxJkPz z{)l)8xA_yXw*(NkO4-C2k|q5+QfJUgU!a{s|BAHs2^sQ|=P*vQnNzAwK=CXR6JQ{X z45o=`ftt>fwN8yH?p%aF;7(%|x58m=(>K*u6qzII4n=gZKkDaPqN=;($8e9Z6h0%{ H#1-Hl@AB%M literal 0 HcmV?d00001 diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters.java b/unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters.java new file mode 100644 index 00000000000..0f5bed55482 --- /dev/null +++ b/unit/java_bytecode/generate_concrete_generic_type/generic_two_parameters.java @@ -0,0 +1,22 @@ +class generic_two_parameters { + class KeyValuePair { + K key; + V value; + } + + KeyValuePair bomb; + + public String func() { + KeyValuePair e = new KeyValuePair(); + e.key = "Hello"; + e.value = 5; + if (e.value >= 4) + { + return e.key; + } + else + { + return "Oops"; + } + } +} diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field$G.class b/unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field$G.class new file mode 100644 index 0000000000000000000000000000000000000000..39888ab1dbc0313dbadc8cd262d7bd3be8dc6cd9 GIT binary patch literal 738 zcmaKq%TB^T6o&tyNChh(3JA(Y?E*0o7p{b`A(5C6HG!}t1qK`}gDFMhW4SOUE_?tV z%6MAAL@h36=KQDMxy91MUFwS_&`OTLFFbNb7?bZ7gBPo zW*XBepEBecLrz-sIx~4ICl9hS5ZvtRbH2J^Y?3u+G^#AEft5vR2NWi`kQ~iV? z>CHPxMMz;+8PbI%%we0sUz_x)Y@{J1znqP`+-ezJlRUA;q-U6I!xE03JN-^s23BWC zc_-EDR66l9_VI2JpIsKTxL2XlI%|xKd!u9;a#*_Rj(E>5SO2;gLe0s{>hW{ober~^ z@v)OhgNAhtVeF~cr-6BrI^8JxyDme<8~*;)O2L_7+>=6{9*dvejgQs}f}oaNwHA#! zEs@P=g%P1MO4c=z4jU>SJ%bfr;CmvaV1xF6%lZ%_JMl$f6LC_+yV+>!WNR)LqHjr3 Z%Dmz>QlxxHW0lSrSpj6AxBb5Pb{C$#Kew0*WFO6o`pfSSg_)F)_KQ351p`u;SveXO26KKg+_HSoj0{ zQN~$>LP3k2osT#3=Huh@?H#}gN(n@&9+vJG{w{lWGX2>~1p@c8{-B8^r?@@Jcq;LlsQkO~w4TgN>56nS_ zXq(=Es-_&N#AP_{3BS#IE_u?9*XM4B`%>F8XH3&F7`j)X0tV|s5qs0+lZl`}aXC|Y zhNrHwKg&Md&r6s8Pp#9~4a%?7+oy{wYAm`K%$67WeQ_@JIQgY(I?~Iwkbr3+iG2e_ zhQd=0outmzGDR}`je?C$vIsw|#;`@YuBAOTGW17hj9KK!ieMY*X_OkrE;fKK DdrzSq literal 0 HcmV?d00001 diff --git a/unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field.class b/unit/java_bytecode/generate_concrete_generic_type/generic_unknown_field.class new file mode 100644 index 0000000000000000000000000000000000000000..73db45376b9a53d426d4f37e50632ae73abb1191 GIT binary patch literal 405 zcmZvY&q~8U5XQf0)2_y7YqSOg!Gj0&U@qPiF9nMb^q}-wHtATmrW?o~eJ)Re2Oq$P z5+_kSWnpH%{pQCkvtQpIp8(Dgxah)H*iqP37!eewykc7tyc=sdAE&w~xKP+5(1g&x zG}e??gzoXll;DiBITHqvv3y&tV$L6QoQmT|S)$Xa&P{#)GoA9u6oepJu#7gztg_EG zd$qGi!|D8j;NE9dp76D)N9?y!XG{H}J*>kej9Ll8ux7$k+eLU6FFBEI4qDNp|80Zz z{sf2U$QRXzB;;AC8=^v~wbMI&2fc~tz?0l>Ov0vU?-#%p22Fq1 { + element ref; + } + + class element { + T elem; + } +} diff --git a/unit/java_bytecode/generate_java_generic_type.cpp b/unit/java_bytecode/generate_java_generic_type.cpp deleted file mode 100644 index a868d86b182..00000000000 --- a/unit/java_bytecode/generate_java_generic_type.cpp +++ /dev/null @@ -1,50 +0,0 @@ -/*******************************************************************\ - - Module: Unit tests for generating new type with generic parameters - substitued for concrete types - - Author: DiffBlue Limited. All rights reserved. - -\*******************************************************************/ - -#include - -#include - -#include -#include - -SCENARIO( - "generate_java_generic_type", - "[CORE][java_bytecode][generate_java_generic_type") -{ - GIVEN("A generic java type and a concrete substitution") - { - symbol_tablet symbol_table; - - - null_message_handlert message_handler; - generate_java_generic_typet type_generator(symbol_table, message_handler); - - - const reference_typet &boxed_integer_type=to_reference_type(java_type_from_string("Ljava/lang/Integer;")); - - java_type_with_generic_typet generic_type; - generic_type.type_parameters.push_back(java_inst_generic_typet(boxed_integer_type)); - - struct_typet base_class; - base_class.components().push_back(struct_union_typet::componentt("a", java_generic_typet("T"))); - base_class.set_tag("UserClass"); - - generic_type.subtype()=base_class; - - const symbolt &new_symbol=type_generator(generic_type); - REQUIRE(new_symbol.is_type); - - - - REQUIRE(new_symbol.base_name=="UserClass"); - REQUIRE(new_symbol.type.id()==ID_pointer); - - } -} diff --git a/unit/java_bytecode/java_bytecode_parse_generics/generics05$igeneric05.class b/unit/java_bytecode/java_bytecode_parse_generics/generics05$igeneric05.class new file mode 100644 index 0000000000000000000000000000000000000000..179141a38e28b24502ec84b87aeb9cb023cdafb4 GIT binary patch literal 856 zcmZuwO>fgc6r9axV_YXBv_OH<(g1D{O%C)zqg*P1kRm{;<@+Wq=~l);&WFU$LZU+A zzz^U@A?7&=2_y&G`}WPwyxI5s>-UeJ0AAp@gghQPDBwU=hb271Q4#eb9xLR+sg4w? z-77uS%}B?C=DXgN>5tD8N*8tz>+vKp3fUm!PGNj$NA;G%PIq8pli2>KxmdJL1<?LG5!1N7bf1+ly~40 zD}mn*U#`PC>sz#UF`OiQ^UBISl$Td}B5iST1Fnm0JaJLPRuNBK_}Eg|UjSE{u;N>x z@_$#^NMA~;Z8%AD0fzyH9FhVjC&Pzw;2@-tQ>jQH=~}TGkC`%~_e2WTX*|1zYJ5lL zE2Atbd>4oTkvI9?ouN?04kO}IHui>VH^n*3-Dbq`!Cj(-{o|b76ZUN58^5pEO5R^34|}N(QJPgDIZ=|@_E^cn<2|y?+}_6nW;58wEq(=&=YLa!`U5k_ BtSJBh literal 0 HcmV?d00001