From 2ecdc0eb68ed6010e355f059bdca36d9bd20e90f Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 8 Feb 2019 17:58:44 +0000 Subject: [PATCH 1/3] Object factory: retain type tags Previously it would follow types as it went, resulting in generated objects with raw struct types. Now it only follows types locally for reference, and passes the tagged types to subroutines. --- .../src/java_bytecode/java_object_factory.cpp | 25 +++++++++++-------- .../require_goto_statements.cpp | 9 ++++--- 2 files changed, 20 insertions(+), 14 deletions(-) diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index 668a3b2cc72..599190feced 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -249,9 +249,11 @@ void java_object_factoryt::gen_pointer_target_init( PRECONDITION(expr.type().id() == ID_pointer); PRECONDITION(update_in_place != update_in_placet::MAY_UPDATE_IN_PLACE); - if(target_type.id() == ID_struct) + const typet &followed_target_type = ns.follow(target_type); + + if(followed_target_type.id() == ID_struct) { - const auto &target_class_type = to_java_class_type(target_type); + const auto &target_class_type = to_java_class_type(followed_target_type); if(has_prefix(id2string(target_class_type.get_tag()), "java::array[")) { gen_nondet_array_init( @@ -565,10 +567,11 @@ void java_object_factoryt::gen_nondet_pointer_init( // When we visit for 2nd time a type AND the maximum depth is exceeded, we set // the pointer to NULL instead of recursively initializing the struct to which // it points. - const typet &subtype=ns.follow(pointer_type.subtype()); - if(subtype.id()==ID_struct) + const typet &subtype = pointer_type.subtype(); + const typet &followed_subtype = ns.follow(subtype); + if(followed_subtype.id() == ID_struct) { - const struct_typet &struct_type=to_struct_type(subtype); + const struct_typet &struct_type = to_struct_type(followed_subtype); const irep_idt &struct_tag=struct_type.get_tag(); // If this is a recursive type of some kind AND the depth is exceeded, set @@ -604,7 +607,9 @@ void java_object_factoryt::gen_nondet_pointer_init( // decide to do this for all types, we should do it here. // Note also that this logic is mirrored in // ci_lazy_methodst::initialize_instantiated_classes. - if(const auto class_type = type_try_dynamic_cast(subtype)) + if( + const auto class_type = + type_try_dynamic_cast(followed_subtype)) { if(class_type->get_base("java::java.lang.Enum") && !must_be_null) { @@ -1024,8 +1029,8 @@ void java_object_factoryt::gen_nondet_init( update_in_placet update_in_place, const source_locationt &location) { - const typet &type = override_type.has_value() ? ns.follow(*override_type) - : ns.follow(expr.type()); + const typet &type = override_type.has_value() ? *override_type : expr.type(); + const typet &followed_type = ns.follow(type); if(type.id()==ID_pointer) { @@ -1049,9 +1054,9 @@ void java_object_factoryt::gen_nondet_init( update_in_place, location); } - else if(type.id()==ID_struct) + else if(followed_type.id() == ID_struct) { - const struct_typet struct_type=to_struct_type(type); + const struct_typet struct_type = to_struct_type(followed_type); // If we are about to initialize a generic class (as a superclass object // for a different object), add its concrete types to the map and delete diff --git a/jbmc/unit/java-testing-utils/require_goto_statements.cpp b/jbmc/unit/java-testing-utils/require_goto_statements.cpp index 4e2ef931915..7b1f24fb4f5 100644 --- a/jbmc/unit/java-testing-utils/require_goto_statements.cpp +++ b/jbmc/unit/java-testing-utils/require_goto_statements.cpp @@ -315,6 +315,8 @@ const irep_idt &require_goto_statements::require_struct_component_assignment( const std::vector &entry_point_instructions, const symbol_tablet &symbol_table) { + namespacet ns(symbol_table); + // First we need to find the assignments to the component belonging to // the structure_name object const auto &component_assignments = @@ -361,14 +363,13 @@ const irep_idt &require_goto_statements::require_struct_component_assignment( // After we have found the declaration of the final assignment's // right hand side, then we want to identify that the type // is the one we expect, e.g.: - // struct java.lang.Integer { __CPROVER_string @class_identifier; } - // tmp_object_factory$2; + // struct java.lang.Integer tmp_object_factory$2; const auto &component_declaration = require_goto_statements::require_declaration_of_name( component_tmp_name, entry_point_instructions); - REQUIRE(component_declaration.symbol().type().id() == ID_struct); + REQUIRE(component_declaration.symbol().type().id() == ID_struct_tag); const auto &component_struct = - to_struct_type(component_declaration.symbol().type()); + ns.follow_tag(to_struct_tag_type(component_declaration.symbol().type())); REQUIRE(component_struct.get(ID_name) == component_type_name); return component_tmp_name; From 7b178219179d6d11ddb715d9b751214b77ce899f Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 11 Feb 2019 17:57:56 +0000 Subject: [PATCH 2/3] Add unit test verifying that java_object_factory doesn't strip tag types Previously if asked to populate a pointer with tagged type (e.g. "Object *") then it would allocate a "struct Object { ... }", i.e. the struct_typet rather than the struct_tag_typet. This verifies that it now retains tag types. --- jbmc/unit/Makefile | 1 + .../java_bytecode/java_object_factory/A.class | Bin 0 -> 264 bytes .../java_bytecode/java_object_factory/A.java | 11 + .../java_bytecode/java_object_factory/B.class | Bin 0 -> 228 bytes .../java_bytecode/java_object_factory/C.class | Bin 0 -> 228 bytes .../java_bytecode/java_object_factory/D.class | Bin 0 -> 235 bytes .../java_bytecode/java_object_factory/E.class | Bin 0 -> 849 bytes .../java_object_factory/Generic.class | Bin 0 -> 419 bytes .../java_object_factory/HasArray.class | Bin 0 -> 269 bytes .../java_object_factory/HasArray.java | 8 + .../java_object_factory/HasEnum.class | Bin 0 -> 264 bytes .../java_object_factory/HasEnum.java | 8 + .../java_object_factory/HasGeneric.class | Bin 0 -> 458 bytes .../java_object_factory/HasGeneric.java | 16 ++ .../java_object_factory/OtherGeneric.class | Bin 0 -> 438 bytes .../java_object_factory/Root.class | Bin 0 -> 334 bytes .../java_object_factory/Root.java | 12 + .../module_dependencies.txt | 1 + .../java_object_factory/struct_tag_types.cpp | 214 ++++++++++++++++++ 19 files changed, 271 insertions(+) create mode 100644 jbmc/unit/java_bytecode/java_object_factory/A.class create mode 100644 jbmc/unit/java_bytecode/java_object_factory/A.java create mode 100644 jbmc/unit/java_bytecode/java_object_factory/B.class create mode 100644 jbmc/unit/java_bytecode/java_object_factory/C.class create mode 100644 jbmc/unit/java_bytecode/java_object_factory/D.class create mode 100644 jbmc/unit/java_bytecode/java_object_factory/E.class create mode 100644 jbmc/unit/java_bytecode/java_object_factory/Generic.class create mode 100644 jbmc/unit/java_bytecode/java_object_factory/HasArray.class create mode 100644 jbmc/unit/java_bytecode/java_object_factory/HasArray.java create mode 100644 jbmc/unit/java_bytecode/java_object_factory/HasEnum.class create mode 100644 jbmc/unit/java_bytecode/java_object_factory/HasEnum.java create mode 100644 jbmc/unit/java_bytecode/java_object_factory/HasGeneric.class create mode 100644 jbmc/unit/java_bytecode/java_object_factory/HasGeneric.java create mode 100644 jbmc/unit/java_bytecode/java_object_factory/OtherGeneric.class create mode 100644 jbmc/unit/java_bytecode/java_object_factory/Root.class create mode 100644 jbmc/unit/java_bytecode/java_object_factory/Root.java create mode 100644 jbmc/unit/java_bytecode/java_object_factory/struct_tag_types.cpp diff --git a/jbmc/unit/Makefile b/jbmc/unit/Makefile index 6c60e82cb23..a9d0d5ad840 100644 --- a/jbmc/unit/Makefile +++ b/jbmc/unit/Makefile @@ -44,6 +44,7 @@ SRC += java_bytecode/ci_lazy_methods/lazy_load_lambdas.cpp \ java_bytecode/java_bytecode_parser/parse_java_class.cpp \ java_bytecode/java_bytecode_parser/parse_java_field.cpp \ java_bytecode/java_object_factory/gen_nondet_string_init.cpp \ + java_bytecode/java_object_factory/struct_tag_types.cpp \ java_bytecode/java_replace_nondet/replace_nondet.cpp \ java_bytecode/java_string_library_preprocess/convert_exprt_to_string_exprt.cpp \ java_bytecode/java_types/erase_type_arguments.cpp \ diff --git a/jbmc/unit/java_bytecode/java_object_factory/A.class b/jbmc/unit/java_bytecode/java_object_factory/A.class new file mode 100644 index 0000000000000000000000000000000000000000..e0f4c1848c97fa74b59054ff6a3725dbda0711e4 GIT binary patch literal 264 zcmXYry>7xl5QJw9*u*%5Kwf|@p}-9t5t4&MWsw3ze>SJ&kg+9Wc&}8ED0l!K3Nh!T z*_m%O`*XdWF90TZ@zKDuhrWk_KoUVC{+QCG*3IeMcaxiHMtptS2%7U^s|8Q7$@TKM zPjtCfNybh;E>e|kRB0^#H=EVBIoM4RH~FjLSf+YmY}}2;J9Sb4+IZl(NYJw!W-9** zKa-tKD-7ZAJFxODT6CO)SF6}TvQG-BLT!zHAwM(@I;?KpbP&)7e*rwAOXB}^s&@z3 CS}8IB literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_object_factory/A.java b/jbmc/unit/java_bytecode/java_object_factory/A.java new file mode 100644 index 00000000000..b0118eb94f5 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_object_factory/A.java @@ -0,0 +1,11 @@ + +public class A { + + public B b; + public C c; + +} + +class B { } + +class C { } diff --git a/jbmc/unit/java_bytecode/java_object_factory/B.class b/jbmc/unit/java_bytecode/java_object_factory/B.class new file mode 100644 index 0000000000000000000000000000000000000000..e5654ceb07bec12b68f19c312b9e1f82aa5e7824 GIT binary patch literal 228 zcmXYr!4APt5Jm4)wNz>23oNnFjUADw#HwLIx__+~o>ZGu`7bMpg%9viVjd=$nR`#} zB=dSdo&d)19n{da(XrtXtf|UXH6zsegP340ik&2Qk;>)ja!O>m6-maV8x^U@Vo@sX z|In-s>ddE6I3YNj;!>t^sdU_$kB;IhT$rd6C?xpW2bswC!8$q0v_cOCf1-=HImp{$ g74X)iKD>i&EDYE@tuJh%!P@-=(1gQ|(E6s_5C7LDe*gdg literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_object_factory/C.class b/jbmc/unit/java_bytecode/java_object_factory/C.class new file mode 100644 index 0000000000000000000000000000000000000000..fda468de8d286af4514238d0bb7ec86f5a636580 GIT binary patch literal 228 zcmXYr%?`m(5QWd^A5|)zz!D4H*b#{|v1(Wl``fzVHq|Co-pfj2;Q>69m|G^9nRC9J zN#^}|z5q)zdX8ne6LH3*9~Ftn_M%kU z|Djo()P+x@a7J*q#kEZ2O6j=0oTTC=JeaTu6cT#c2bsu^!6r^+Qel7wf1-=HImp{) g74X)?8b3gH77aK&?HabxWbOR|Xu)MiXxAz43jq!$g8%>k literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_object_factory/D.class b/jbmc/unit/java_bytecode/java_object_factory/D.class new file mode 100644 index 0000000000000000000000000000000000000000..06526bbfa08cadfea4691ea1ebd90700e17814b1 GIT binary patch literal 235 zcmXYr!4APt5Jm4$EmbPMz!D4H*b#{kv1nKj``3EmNwvvS5}#!yvG4&tO3cF~Gjs3B zon&6`#}hyw4Hre!9Mm271be7bm5&I;c4tGdCfQaJ{7|KGaXv;;uSJwFX@*%Wl8w;H z_&>Dry*lw}I2{n&Rd&{~oGBBp&BbY~wYc^U;vzg)C=qB%Xc!+PBHabc=pf@9Efn}6 nQ^d_d-Zra%w;`qO9du(+fWy=N!ZOONyBRSP+6^0s9nZxOh~ zjE5$c*lwF}*wzf}2#EIrTD#StuMhNo6fibA2kloaS3rNQfXs;u$NoqlQ?6V@^uysB zUm)KOBLBsB(DUP$vKLasP}HNh0$0oJV|gNLp^W-9H;IF&->9f^PJ8Idup{GubEb)U zBnOo5{F_8=n?V#Ldjc!}srkIpA)(2;fb?bEpdZO(98)E&%z)YS!fEpIOzBoM9yCeJ z9*u3e!*T5SPXpF(Ka(Q{w^_T5D}0!1TXw;aY{XMVws*U{}y0;u%y1rjx1prwRp)BbD z3ac!d8OUN8E1;VoZ=EbJYXb2FsdH$b$P>6mdq!a<@k>~p^6N;csO9L@uSlOmXMSpq zf1M)s1q*Aqp>R4HVsXb^X!HO^b#v_una>KIZFiY&;5JLg9mQFPiMvWLm+8_VybiuY z?>dHd2J;kIq#=Yf;su zB$!FU#155KRm5_9IwM#&#S@?TvC{IPeo1ASh%{#s#6>3ZnJ87GJ7`tUYROgOJE>)< zGOjn;^u4{Vy@RzWj_W;DpLXV@(nE|IIe4V4q79Lm-Z?R`%e&n|7ar%{p85QWdg{55J5eS_}WF3hI8iXfHZBIrVK)74G9v^S&)T%+J)xe{FX06tXd z+z=TU&iM{=nA_jw3g8XH03C!LA`b(CwcQcyuVnU4aL1}t^@PxQe%UbnsJ4<2CaRQ+ z{ckGuTBHS&VNzwH*a)qRZ=qfPD6R^Ux!6s$7Dp}&R@Gi-@>7|s{yiAw;vjl(;Su~h zBt!Tp5xG_lp literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_object_factory/HasArray.java b/jbmc/unit/java_bytecode/java_object_factory/HasArray.java new file mode 100644 index 00000000000..6e5f5f8d215 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_object_factory/HasArray.java @@ -0,0 +1,8 @@ + +public class HasArray { + + public D[] ds; + +} + +class D { } diff --git a/jbmc/unit/java_bytecode/java_object_factory/HasEnum.class b/jbmc/unit/java_bytecode/java_object_factory/HasEnum.class new file mode 100644 index 0000000000000000000000000000000000000000..1b87ff41d4a748a91aa20fb9127c51e15b3ed87f GIT binary patch literal 264 zcmXYr%?`m(6olu{AF32@V26cn?1+sJi-rZUzpWdtRGU=my{se_9>7D1bDM5XX1>Xs z%=h>H0GOihpbpPQ*G7*(l28v;GlDf&iOLsjhod9GSf(e=yg(&#TiimK9Yh#2=?7^f z;-kov_7ybpi@FnG^nE>Ya1$r{5p~=@`thK|}EwzajEB&ZlCY?V*J1;r_ literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_object_factory/HasEnum.java b/jbmc/unit/java_bytecode/java_object_factory/HasEnum.java new file mode 100644 index 00000000000..5e2c97ab74b --- /dev/null +++ b/jbmc/unit/java_bytecode/java_object_factory/HasEnum.java @@ -0,0 +1,8 @@ + +public class HasEnum { + + public E e; + +} + +enum E { x, y, z } diff --git a/jbmc/unit/java_bytecode/java_object_factory/HasGeneric.class b/jbmc/unit/java_bytecode/java_object_factory/HasGeneric.class new file mode 100644 index 0000000000000000000000000000000000000000..dfae98673ccb49028d5441f5327b80dd00d27a50 GIT binary patch literal 458 zcmZ`#yH3ME5S-1!CdR}eybF+^A{4lxOOytQhh&k$DE---oQupwx}5nhDkKU%fR93~ z&BGu;adSJfv%9zV`u6++;0${nn%H)+<6@UUOF}2Qlv)~<4mplhriCqxBF>`a<^%F!?3pZ3m3X=TTR=J8-kXq_+a z_)$Tmw7e<9;t&n~Kk(rvq0Q(pYry4b^N);mU#Vcq}$ literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_object_factory/HasGeneric.java b/jbmc/unit/java_bytecode/java_object_factory/HasGeneric.java new file mode 100644 index 00000000000..894c7cd04f2 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_object_factory/HasGeneric.java @@ -0,0 +1,16 @@ + +public class HasGeneric { + + public Generic s; + public Generic t; + public OtherGeneric u; + +} + +class Generic { + T t; +} + +class OtherGeneric { + Generic gen; +} diff --git a/jbmc/unit/java_bytecode/java_object_factory/OtherGeneric.class b/jbmc/unit/java_bytecode/java_object_factory/OtherGeneric.class new file mode 100644 index 0000000000000000000000000000000000000000..a46150cab26d063dd8de865a913abb08a69f7f4d GIT binary patch literal 438 zcmZWl!A^rf6r2SL77=Qz_3E*Duoq84NQ{YkAoftw`+^&~4T7Oy;%9j>@!$veQN{;C z6g}*|nb~>sUiRbj?H#~5j!dXHFmPyK%Ah79V;BZEA`^v-UBXM5WW1~j!C-f~7ly7+ zkGdx_S^CsBJ6SPkSNT2JoIqycu6l?>5%MS{WgO%&PglH|n@X z{oaOQ^fwvDQ0T`1Mn}Vds!m9O(I}Kb)g7χTkCV{PF*;g?i8Vjk3~>W={_@tHf5SXIwSbATnR4x0sbiQ zCb-DC=X~KFxIe#N-vA~!Dlou)hJy@;1d@b-m|hT~1=~X0%k|Vb`5uTOhRmR@S3yDM%vIh_&WYx~MuL!pg&=vTFJFS2f#jD>AvJCjcP{14-9q1W6Y zo~-S-ta!G)Yt*gw8@Y$)OZg^Cl-S~K4+tZVs#cnL^;j=e)8QBq-vq?rC9FV-EX)n$ rVHVir$p`x`)@@Ez$Ut)T3Ho3VVaS>?_I|`#2A^ODV@`zK@U!;^ZR$E( literal 0 HcmV?d00001 diff --git a/jbmc/unit/java_bytecode/java_object_factory/Root.java b/jbmc/unit/java_bytecode/java_object_factory/Root.java new file mode 100644 index 00000000000..b1db5c85737 --- /dev/null +++ b/jbmc/unit/java_bytecode/java_object_factory/Root.java @@ -0,0 +1,12 @@ + +public class Root { + + // This one isn't used in the tests; it just references other classes + // to get them loaded. + + A a; + HasArray ha; + HasEnum he; + HasGeneric hg; + +} diff --git a/jbmc/unit/java_bytecode/java_object_factory/module_dependencies.txt b/jbmc/unit/java_bytecode/java_object_factory/module_dependencies.txt index c4380fa26bd..cbdc5447cf2 100644 --- a/jbmc/unit/java_bytecode/java_object_factory/module_dependencies.txt +++ b/jbmc/unit/java_bytecode/java_object_factory/module_dependencies.txt @@ -1,5 +1,6 @@ java_bytecode java_object_factory +java-testing-utils langapi # should go away testing-utils util diff --git a/jbmc/unit/java_bytecode/java_object_factory/struct_tag_types.cpp b/jbmc/unit/java_bytecode/java_object_factory/struct_tag_types.cpp new file mode 100644 index 00000000000..3e20cccac6e --- /dev/null +++ b/jbmc/unit/java_bytecode/java_object_factory/struct_tag_types.cpp @@ -0,0 +1,214 @@ +/*******************************************************************\ + +Module: Unit tests for Java-object-factory's treatment of tag types + +Author: Diffblue Ltd. + +\*******************************************************************/ + +#include +#include +#include +#include +#include +#include +#include + +#include + +static bool is_decl_with_struct_tag(const codet &code, const irep_idt &id) +{ + if(code.get_statement() != ID_decl) + return false; + + const typet &decl_type = to_code_decl(code).symbol().type(); + return decl_type.id() == ID_struct_tag && + to_struct_tag_type(decl_type).get_identifier() == id; +} + +static bool is_decl_of_type(const codet &code, const typet &type) +{ + return code.get_statement() == ID_decl && + to_code_decl(code).symbol().type() == type; +} + +static bool +contains(const exprt &expr, std::function predicate) +{ + return std::any_of(expr.depth_begin(), expr.depth_end(), predicate); +} + +static bool +contains(const codet &code, std::function predicate) +{ + std::vector statements = + require_goto_statements::get_all_statements(code); + return std::any_of(statements.begin(), statements.end(), predicate); +} + +static bool +contains(const typet &type, std::function predicate) +{ + if(predicate(type)) + return true; + + if(type.has_subtypes()) + { + for(const auto &subtype : to_type_with_subtypes(type).subtypes()) + { + if(contains(subtype, predicate)) + return true; + } + } + + return false; +} + +static bool contains_decl_of_type(const codet &code, const typet &type) +{ + return contains(code, [&type](const codet &subcode) { + return is_decl_of_type(subcode, type); + }); +} + +static bool contains_decl_with_struct_tag(const codet &code, const irep_idt &id) +{ + return contains(code, [&id](const codet &subcode) { + return is_decl_with_struct_tag(subcode, id); + }); +} + +static bool uses_raw_struct_types(const typet &type) +{ + return contains( + type, [](const typet &subtype) { return subtype.id() == ID_struct; }); +} + +static bool uses_raw_struct_types(const exprt &expr) +{ + return contains(expr, [](const exprt &subexpr) { + return uses_raw_struct_types(subexpr.type()); + }); +} + +code_blockt +initialise_nondet_object_of_type(const typet &type, symbol_tablet &symbol_table) +{ + code_blockt created_code; + java_object_factory_parameterst parameters; + select_pointer_typet pointer_selector; + + object_factory( + type, + "root", + created_code, + symbol_table, + parameters, + lifetimet::AUTOMATIC_LOCAL, + source_locationt(), + pointer_selector); + + return created_code; +} + +SCENARIO( + "java_object_factory_tag_types", + "[core][java_bytecode][java_object_factory]") +{ + GIVEN("Some classes with fields") + { + register_language(new_java_bytecode_language); + symbol_tablet symbol_table = + load_java_class("Root", "./java_bytecode/java_object_factory"); + + WHEN("Creating a nondet 'A' object") + { + struct_tag_typet A_type("java::A"); + struct_tag_typet B_type("java::B"); + struct_tag_typet C_type("java::C"); + + const auto a_pointer = java_reference_type(A_type); + code_blockt created_code = + initialise_nondet_object_of_type(a_pointer, symbol_table); + + THEN("An A, a B and a C object should be allocated") + { + REQUIRE(contains_decl_of_type(created_code, A_type)); + REQUIRE(contains_decl_of_type(created_code, B_type)); + REQUIRE(contains_decl_of_type(created_code, C_type)); + } + + THEN("No raw struct expressions should appear") + { + REQUIRE_FALSE(uses_raw_struct_types(created_code)); + } + } + + WHEN("Creating a nondet 'HasArray' object") + { + struct_tag_typet HasArray_type("java::HasArray"); + struct_tag_typet D_type("java::D"); + + const auto HasArray_pointer = java_reference_type(HasArray_type); + code_blockt created_code = + initialise_nondet_object_of_type(HasArray_pointer, symbol_table); + + THEN("A HasArray object should be created") + { + REQUIRE(contains_decl_of_type(created_code, HasArray_type)); + } + + THEN("No raw struct expressions should appear") + { + REQUIRE_FALSE(uses_raw_struct_types(created_code)); + } + } + + WHEN("Creating a nondet 'HasEnum' object") + { + struct_tag_typet HasEnum_type("java::HasEnum"); + struct_tag_typet E_type("java::E"); + + const auto HasEnum_pointer = java_reference_type(HasEnum_type); + code_blockt created_code = + initialise_nondet_object_of_type(HasEnum_pointer, symbol_table); + + THEN("A HasEnum object should be allocated") + { + REQUIRE(contains_decl_of_type(created_code, HasEnum_type)); + } + + THEN("No raw struct expressions should appear") + { + REQUIRE_FALSE(uses_raw_struct_types(created_code)); + } + } + + WHEN("Creating a nondet 'HasGeneric' object") + { + struct_tag_typet HasGeneric_type("java::HasGeneric"); + irep_idt generic_id = "java::Generic"; + irep_idt other_generic_id = "java::OtherGeneric"; + + const auto HasGeneric_pointer = java_reference_type(HasGeneric_type); + code_blockt created_code = + initialise_nondet_object_of_type(HasGeneric_pointer, symbol_table); + + THEN("An HasGeneric, Generic and OtherGeneric object should be allocated") + { + REQUIRE(contains_decl_of_type(created_code, HasGeneric_type)); + // These ones are just checked for a tag rather than a full type because + // the tags are decorated with generic information, and I just want to + // check they (a) are created and (b) don't use expanded types, rather + // than verifying their full structure. + REQUIRE(contains_decl_with_struct_tag(created_code, generic_id)); + REQUIRE(contains_decl_with_struct_tag(created_code, other_generic_id)); + } + + THEN("No raw struct expressions should appear") + { + REQUIRE_FALSE(uses_raw_struct_types(created_code)); + } + } + } +} From 328bc04aec7df5ffdf6489d9a4345d7709d2087d Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Tue, 12 Feb 2019 11:17:04 +0000 Subject: [PATCH 3/3] Amend generics test to expect tag types rather than plain structs --- .../generic_parameters_test.cpp | 28 +++++++++---------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp index 5d803a770d8..6ea76302000 100644 --- a/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp +++ b/jbmc/unit/java_bytecode/goto_program_generics/generic_parameters_test.cpp @@ -316,9 +316,9 @@ SCENARIO( // Trace the assignments back to the declaration of the generic type // and verify that it is what we expect. - const auto &tmp_object_struct = - to_struct_type(tmp_object_declaration.symbol().type()); - REQUIRE(tmp_object_struct.get_tag() == "Wrapper"); + const auto &tmp_object_struct_tag = + to_struct_tag_type(tmp_object_declaration.symbol().type()); + REQUIRE(tmp_object_struct_tag.get_identifier() == "java::Wrapper"); THEN("Object 'v' has field 'field' of type IWrapper") { @@ -366,9 +366,9 @@ SCENARIO( // Trace the assignments back to the declaration of the generic type // and verify that it is what we expect. - const auto &tmp_object_struct = - to_struct_type(tmp_object_declaration.symbol().type()); - REQUIRE(tmp_object_struct.get_tag() == "Wrapper"); + const auto &tmp_object_struct_tag = + to_struct_tag_type(tmp_object_declaration.symbol().type()); + REQUIRE(tmp_object_struct_tag.get_identifier() == "java::Wrapper"); THEN( "Object 'v' has field 'field' of type Object (upper bound of the " @@ -416,11 +416,11 @@ SCENARIO( // Trace the assignments back to the declaration of the generic type // and verify that it is what we expect. - const auto &tmp_object_struct = - to_struct_type(tmp_object_declaration.symbol().type()); + const auto &tmp_object_struct_tag = + to_struct_tag_type(tmp_object_declaration.symbol().type()); REQUIRE( - tmp_object_struct.get_tag() == - "GenericFields$GenericInnerOuter$Outer"); + tmp_object_struct_tag.get_identifier() == + "java::GenericFields$GenericInnerOuter$Outer"); THEN("Object 'v' has field 'field' of type InnerClass") { @@ -481,11 +481,11 @@ SCENARIO( // Trace the assignments back to the declaration of the generic type // and verify that it is what we expect. - const auto &tmp_object_struct = - to_struct_type(tmp_object_declaration.symbol().type()); + const auto &tmp_object_struct_tag = + to_struct_tag_type(tmp_object_declaration.symbol().type()); REQUIRE( - tmp_object_struct.get_tag() == - "GenericFields$GenericRewriteParameter$A"); + tmp_object_struct_tag.get_identifier() == + "java::GenericFields$GenericRewriteParameter$A"); THEN("Object 'v' has field 'value' of type Integer") {