From 8e7b6e7cdf2c66a40f7ba27d527a74f05e635c87 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Mon, 25 Jun 2018 18:23:20 +0100 Subject: [PATCH] Java object factory: initialize AbstractStringBuilder-derived types correctly These are currently initialized as if they are directly derived from Object, which causes a crash due to the type inconsistency between StringBuilder { AbstractStringBuilder { Object { } } } and StringBuilder { Object { } } With this change they are initialised more like normal types, which has the side-effect that any fields they possess that are *not* special-cased by `initialize_nondet_string_fields` are nondet-initialized as for any other type. I add a test verifying this new behaviour, and a simpler test checking that Builder and Buffer are usable as nondet arguments at all. --- .../NondetStringBuilderAndBuffer/Test.class | Bin 0 -> 285 bytes .../NondetStringBuilderAndBuffer/Test.java | 7 + .../java/lang/AbstractStringBuilder.class | Bin 0 -> 256 bytes .../java/lang/AbstractStringBuilder.java | 5 + .../java/lang/CharSequence.class | Bin 0 -> 115 bytes .../java/lang/CharSequence.java | 5 + .../java/lang/String.class | Bin 0 -> 226 bytes .../java/lang/String.java | 5 + .../java/lang/StringBuffer.class | Bin 0 -> 223 bytes .../java/lang/StringBuffer.java | 5 + .../java/lang/StringBuilder.class | Bin 0 -> 225 bytes .../java/lang/StringBuilder.java | 5 + .../NondetStringBuilderAndBuffer/test.desc | 12 + .../StringModelsWithFields/Test.class | Bin 0 -> 1083 bytes .../StringModelsWithFields/Test.java | 36 +++ .../StringModelsWithFields/java/lang/A.class | Bin 0 -> 218 bytes .../StringModelsWithFields/java/lang/A.java | 8 + .../java/lang/AbstractStringBuilder.class | Bin 0 -> 290 bytes .../java/lang/AbstractStringBuilder.java | 7 + .../java/lang/CharSequence.class | Bin 0 -> 115 bytes .../java/lang/CharSequence.java | 5 + .../java/lang/String.class | Bin 0 -> 254 bytes .../java/lang/String.java | 7 + .../java/lang/StringBuffer.class | Bin 0 -> 239 bytes .../java/lang/StringBuffer.java | 7 + .../java/lang/StringBuilder.class | Bin 0 -> 241 bytes .../java/lang/StringBuilder.java | 7 + .../StringModelsWithFields/test.desc | 14 + .../src/java_bytecode/java_object_factory.cpp | 296 ++++++++---------- jbmc/src/java_bytecode/java_object_factory.h | 8 - .../gen_nondet_string_init.cpp | 16 +- 31 files changed, 277 insertions(+), 178 deletions(-) create mode 100644 jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/Test.class create mode 100644 jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/Test.java create mode 100644 jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/AbstractStringBuilder.class create mode 100644 jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/AbstractStringBuilder.java create mode 100644 jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/CharSequence.class create mode 100644 jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/CharSequence.java create mode 100644 jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/String.class create mode 100644 jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/String.java create mode 100644 jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuffer.class create mode 100644 jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuffer.java create mode 100644 jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuilder.class create mode 100644 jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuilder.java create mode 100644 jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/test.desc create mode 100644 jbmc/regression/jbmc-strings/StringModelsWithFields/Test.class create mode 100644 jbmc/regression/jbmc-strings/StringModelsWithFields/Test.java create mode 100644 jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/A.class create mode 100644 jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/A.java create mode 100644 jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/AbstractStringBuilder.class create mode 100644 jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/AbstractStringBuilder.java create mode 100644 jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/CharSequence.class create mode 100644 jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/CharSequence.java create mode 100644 jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/String.class create mode 100644 jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/String.java create mode 100644 jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuffer.class create mode 100644 jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuffer.java create mode 100644 jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuilder.class create mode 100644 jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuilder.java create mode 100644 jbmc/regression/jbmc-strings/StringModelsWithFields/test.desc diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/Test.class b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..ced41ac19a37f055658a772d23487477201d7b44 GIT binary patch literal 285 zcmZvWJrBW96o%j1PpZ^vFxbk#(v28MOv2E{-g4VqsY>eB|1wDoet;h(&Sj8@lic(1 zo;T0AkLT?UAb{sUhijv0qs3rNL?PsqLHGL`24jBQaRzTG3cjii2`{5K$w{#!Kgk0% zfxq0x=XjLIMK%g$DT-`XiG0V)@t;MSlCHo`c&y4TUkC-OM+6%xj0*!MomB!u`%7LY zd%l(EL8ITQ&_Fhrlr5UNR2fxsa0R literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/Test.java b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/Test.java new file mode 100644 index 00000000000..36bef70d308 --- /dev/null +++ b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/Test.java @@ -0,0 +1,7 @@ +public class Test { + + public static void testme(StringBuilder builder, StringBuffer buffer) { + + } + +} diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/AbstractStringBuilder.class b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/AbstractStringBuilder.class new file mode 100644 index 0000000000000000000000000000000000000000..63f44f994ceb3547db288371c323c979451e8893 GIT binary patch literal 256 zcmX^0Z`VEs1_l!bel7-P25xo+9(D#^b_PC11~!|_yv!0iMh0dL%`ip=7U%qwR7M7V zpUk{eztY^K)S{5Yq#U3KS8#r5QF5wVCWs^Dm{eR+l$cx+TvC*om+n-WnUj)Qq?eUg zmdL}v%D~3RAP-{e=OpH(>tj{R$RL1F;h&V1nq0!jAchcf&PXf@PAx1=%}Y*YP-I{N tx*F&>pcfc{5NHFCWC!wO!F&b=R;}#}j2pqy96%Bz%>dTI38a}AxBvlGIbQ$( literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/AbstractStringBuilder.java b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/AbstractStringBuilder.java new file mode 100644 index 00000000000..13b25b4c809 --- /dev/null +++ b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/AbstractStringBuilder.java @@ -0,0 +1,5 @@ +package java.lang; + +public class AbstractStringBuilder implements CharSequence { + +} diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/CharSequence.class b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/CharSequence.class new file mode 100644 index 0000000000000000000000000000000000000000..9b3497435fd3f03109435adac1fb55e8cb84c8bf GIT binary patch literal 115 zcmX^0Z`VEs1_l!bc6J6 zswPfY7D^}cR9uA%3vGr$UHh5PiT^eKq+OKCxMUdqx`LA^LV2mAjwQx0=r1}?PcjNx aNyv$f8V*>qJJ_wUJA}23W~58mfc*h>mn};G literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/String.java b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/String.java new file mode 100644 index 00000000000..e9d95981d63 --- /dev/null +++ b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/String.java @@ -0,0 +1,5 @@ +package java.lang; + +public class String implements CharSequence { + +} diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuffer.class b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuffer.class new file mode 100644 index 0000000000000000000000000000000000000000..1c6cddabe11dd5ed9db1a05065a86ed82d244cd6 GIT binary patch literal 223 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDj7+g}6nV0TVnwFMYq?eUgmdL}v!obSNAO>RV z=OpH(>mw^+WROQlI3^XB6eT8?z!YTWq@)%xC^9esodp7nKnOGpNU{NWvS2;~1FP0{ Z2F8tGX?7sV1{7uhYG7pG0MbkhoB%>^FP;DZ literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuffer.java b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuffer.java new file mode 100644 index 00000000000..5031f40a7c7 --- /dev/null +++ b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuffer.java @@ -0,0 +1,5 @@ +package java.lang; + +public class StringBuffer extends AbstractStringBuilder { + +} diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuilder.class b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuilder.class new file mode 100644 index 0000000000000000000000000000000000000000..9830cfebf49205b428644113bacf297848fa048a GIT binary patch literal 225 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBDj6kJl2nV0TVnwgW5TBMhiSeD4cz{0@F$RG}4 z>*plqrR$@pVPud;$T%hymlP!?m!PO%P-I{NIt&CDfe>gKkYoe$WWjs}23D=@42&DW V((FKz4Jgb2)WFEV0i>B2I04{PFnRz0 literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuilder.java b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuilder.java new file mode 100644 index 00000000000..0fd6a6f0160 --- /dev/null +++ b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/java/lang/StringBuilder.java @@ -0,0 +1,5 @@ +package java.lang; + +public class StringBuilder extends AbstractStringBuilder { + +} diff --git a/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/test.desc b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/test.desc new file mode 100644 index 00000000000..4d82786d6ef --- /dev/null +++ b/jbmc/regression/jbmc-strings/NondetStringBuilderAndBuffer/test.desc @@ -0,0 +1,12 @@ +CORE +Test.class +--function Test.testme +^EXIT=0$ +^SIGNAL=0$ +^VERIFICATION SUCCESSFUL$ +-- +type mismatch +-- +Before cbmc#2472 this would assume that StringBuilder's direct parent was +java.lang.Object, causing a type mismatch when --refine-strings was not in use +(which at the time would assume that parent-child relationship) diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/Test.class b/jbmc/regression/jbmc-strings/StringModelsWithFields/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..ecc310248ef9d3870b7f93be6b95ef26d2783a02 GIT binary patch literal 1083 zcmZ{iOK%cU6vzJ;rVNiu3zP!B`?6BN;sc-5T1q8pg1Ts9((VSBlBpETFf{rZ+^eZE zsd3@Ll}fC!iH4Z4=+3xt;X?fyCdP9qk6Lh&bLP(foO{o?zcagkK70faL(&c(#%yq7 z+y*C3+Taq-g9+hINwr}>1cH{?W!gZG$e6Uji;#@4jEEim7?W{Y#*~bxj59LM+Hnr& zWyBZ;$CYwf)eWswEYE9YB~wsy3~YtLGOZOgV}`*ToV>#zB}+M#VIZv))mxSIjH)k* zWXdztvawE!R4~1!Y$(x!Qp`se4P7hd=PFtur|R(@fz{PsdR&xpE*eVq?oH)hvx0Rx zTWI!TUo2JhteVn9W!n-}o)R@V4&gAz1zhB~gv%UPaFrvDX^v}{;kb?fhaUk3|9@I! z2y`Ne7LpsfUeXzSolxsuqJ0L}!2pA!BPAHzov($Wq2|RVNwh6vmLq|=f6lm_SyQtH z;a3R4K4ytHX&Mb{pVmB1MDCL43&A`wT)TN)xwgc6R^no?O95^V;4 zMe6tws^fdOj&G4FOm%z-Rbj4UH(Z5O$7dl{(Pw>*_j^l=M}G7SuPDpvh3)ZEY*D5| z+QO4J;G6J-YH)7Cv4j5QZ47+c6T>yQy2MBg?t|ixC{lx`OBY?$FxaJwHhbvp`htV0 z!C`_3032z8rx3mkLidnpyrAd~vH6M<_=!>SfCKVxC|FA?EnA( literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/Test.java b/jbmc/regression/jbmc-strings/StringModelsWithFields/Test.java new file mode 100644 index 00000000000..7bb9f7676ef --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringModelsWithFields/Test.java @@ -0,0 +1,36 @@ +public class Test { + + public static void testme(StringBuilder builder, StringBuffer buffer, String str) { + + // In this test the versions of String, StringBuilder and + // StringBuffer.class supplied have fields beyond the expected situation + // of either no fields at all (without --refine-strings) or only 'length' + // and 'data' (with --refine-strings). We check they have been nondet- + // initialized as expected by making sure we can reach the final + // 'assert false'. + + if(str != null && + builder != null && + buffer != null && + str.a != null && + builder.i != null && + buffer.i != null && + str.a.x >= 5 && + str.a.y <= -10.0f && + builder.d >= 100.0 && + buffer.b == true) { + + assert builder instanceof StringBuilder; + assert buffer instanceof StringBuffer; + assert str instanceof String; + + assert str.a instanceof A; + assert builder.i instanceof Integer; + assert buffer.i instanceof Integer; + + assert false; + } + + } + +} diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/A.class b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/A.class new file mode 100644 index 0000000000000000000000000000000000000000..f620ab4db78d31ad96844e8df120b21ffd46a5cd GIT binary patch literal 218 zcmYL@!3u(45QJwlwbarcphLInke7}TNFW4Jhobwh{lqV(AR6^poq`TMKo1qIUOLRo ze!DR2=lgmCm}6i;L*ImJ!Xwa)wPxK}A;DOvOqEN5Hl7>_?Nxq~1b3q{xvegdEDj<{ zd1LMKs)%K%YA}LXBCf(g2VH_)&weVhvmX$=KkcGK#wA8*@dse%e&{@L1I#9=u3)y9 XhMdHyPoJPibGF%yW~s3|OfB?&*S#VT literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/A.java b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/A.java new file mode 100644 index 00000000000..7a001f56696 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/A.java @@ -0,0 +1,8 @@ +package java.lang; + +public class A { + + public int x; + public float y; + +} diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/AbstractStringBuilder.class b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/AbstractStringBuilder.class new file mode 100644 index 0000000000000000000000000000000000000000..aecd1092a9a93f33a42c49a4badd0582b4fe462f GIT binary patch literal 290 zcmZus%WA?<5Iy4~(bQI@;G$5(UE4+7bY~H)AQVIwDeiBQA>NQ)>FtgG)s^6)AJC5~ zon(_u7xOr0&b)qp&))!^FbvSdrH?BgeIEk?X~Ok7Q%5z;l}V?s#&ODaM)01s(QZy? z-resAt>qzMLVv9dZ;JPb?VE~nVS?~b*qB$k1UHN5(^(a}&{=KLmqOPCj@J%v`S`#Vz0j=losc`B)BW3 zK{@VGED#g literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/String.java b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/String.java new file mode 100644 index 00000000000..5f9cd4b405c --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/String.java @@ -0,0 +1,7 @@ +package java.lang; + +public class String implements CharSequence { + + public A a; + +} diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuffer.class b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuffer.class new file mode 100644 index 0000000000000000000000000000000000000000..7d574b934be9143a496ae1fc64ad5991c79c5ed7 GIT binary patch literal 239 zcmYjLO%K6P5S*o2-;Il#h#L-E97Te}NnD77+iUyUJgGK$TK~&Q;@}7PQDWN=4!b+E zGrO7R>;3>Rfn7xrbqfs(O#(Sw2ZA|OkxFKSVt=qF7|Ym`1beL_xk*os)H~sXys2*E zRJ(GeGSb>6T1CMk^?j*FM{yB#n6L=#439$*1>=7Uq5Bi&&N=Y5 i6%3RdB!NL#lqr_DNvDn?2 zo!Mm`&)Xfq7)>8V)I8KZGzb)PEeY;KX=SH`Vt=qFIEyTngyvdlxyg^AG&>Qdyz#eL zZX&r-Z_?UYqjWOQRT@h(I*7BV!G%X?zj2TXodka#LieZ4!jm;3vVRWrP~d<7=YoUM e7x7o-WoDg^0+fbV(B&gnxVyXtA96&V1yo-UmoZ5I literal 0 HcmV?d00001 diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuilder.java b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuilder.java new file mode 100644 index 00000000000..b9cc96a321b --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringModelsWithFields/java/lang/StringBuilder.java @@ -0,0 +1,7 @@ +package java.lang; + +public class StringBuilder extends AbstractStringBuilder { + + public double d; + +} diff --git a/jbmc/regression/jbmc-strings/StringModelsWithFields/test.desc b/jbmc/regression/jbmc-strings/StringModelsWithFields/test.desc new file mode 100644 index 00000000000..caba6e8ac88 --- /dev/null +++ b/jbmc/regression/jbmc-strings/StringModelsWithFields/test.desc @@ -0,0 +1,14 @@ +CORE +Test.class +--function Test.testme +^EXIT=10$ +^SIGNAL=0$ +assertion at file Test.java line 23 .* SUCCESS +assertion at file Test.java line 24 .* SUCCESS +assertion at file Test.java line 25 .* SUCCESS +assertion at file Test.java line 27 .* SUCCESS +assertion at file Test.java line 28 .* SUCCESS +assertion at file Test.java line 29 .* SUCCESS +assertion at file Test.java line 31 .* FAILURE +-- +type mismatch diff --git a/jbmc/src/java_bytecode/java_object_factory.cpp b/jbmc/src/java_bytecode/java_object_factory.cpp index bba09f713f9..565a4b59f97 100644 --- a/jbmc/src/java_bytecode/java_object_factory.cpp +++ b/jbmc/src/java_bytecode/java_object_factory.cpp @@ -510,17 +510,22 @@ static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size) return code_assignt(lhs, alloc); } -/// Initialize a nondeterministic String structure -/// \param obj: struct to initialize, must have been declared using -/// code of the form: -/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ -/// struct java.lang.String { struct \@java.lang.Object; -/// int length; char *data; } tmp_object_factory$1; -/// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +/// Check if a structure is a nondeterministic String structure, and if it is +/// initialize its length and data fields. +/// \param struct_expr [out]: struct that we may initialize +/// \param code: block to add pre-requisite declarations (e.g. to allocate a +/// data array) /// \param max_nondet_string_length: maximum length of strings to initialize /// \param loc: location in the source +/// \param function_id: function ID to associate with auxiliary variables /// \param symbol_table: the symbol table -/// \return code for initialization of the strings +/// \param printable: if true, the nondet string must consist of printable +/// characters only +/// \return true if struct_expr's length and data fields have been set up, +/// false if we took no action because struct_expr wasn't a CharSequence +/// or didn't have the necessary fields. +/// +/// The code produced is of the form: /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ /// int tmp_object_factory$1; /// tmp_object_factory$1 = NONDET(int); @@ -535,169 +540,125 @@ static codet make_allocate_code(const symbol_exprt &lhs, const exprt &size) /// *string_data_pointer, *string_data_pointer); /// cprover_associate_length_to_array_func( /// *string_data_pointer, tmp_object_factory); -/// arg = { .@java.lang.Object={ -/// .@class_identifier=\"java::java.lang.String\" }, +/// +/// struct_expr is then adjusted to set /// .length=tmp_object_factory, -/// .data=*string_data_pointer }; +/// .data=*string_data_pointer /// ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ /// Unit tests in `unit/java_bytecode/java_object_factory/` ensure /// it is the case. -codet initialize_nondet_string_struct( - const exprt &obj, +bool initialize_nondet_string_fields( + struct_exprt &struct_expr, + code_blockt &code, const std::size_t &max_nondet_string_length, const source_locationt &loc, const irep_idt &function_id, symbol_table_baset &symbol_table, bool printable) { - PRECONDITION( - java_string_library_preprocesst::implements_java_char_sequence(obj.type())); + if(!java_string_library_preprocesst::implements_java_char_sequence( + struct_expr.type())) + { + return false; + } - const namespacet ns(symbol_table); - code_blockt code; + namespacet ns(symbol_table); + + const struct_typet &struct_type = + to_struct_type(ns.follow(struct_expr.type())); + + // In case the type for String was not added to the symbol table, + // (typically when string refinement is not activated), `struct_type` + // just contains the standard Object fields (or may have some other model + // entirely), and in particular has no length and data fields. + if(!struct_type.has_component("length") || !struct_type.has_component("data")) + return false; - // `obj` is `*expr` - const struct_typet &struct_type = to_struct_type(ns.follow(obj.type())); - // @clsid = java::java.lang.String or similar. // We allow type StringBuffer and StringBuilder to be initialized // in the same way has String, because they have the same structure and // are treated in the same way by CBMC. + // Note that CharSequence cannot be used as classid because it's abstract, // so it is replaced by String. // \todo allow StringBuffer and StringBuilder as classid for Charsequence - const irep_idt &class_id = - struct_type.get_tag() == "java.lang.CharSequence" - ? "java::java.lang.String" - : "java::" + id2string(struct_type.get_tag()); + if(struct_type.get_tag() == "java.lang.CharSequence") + { + set_class_identifier( + struct_expr, ns, symbol_typet("java::java.lang.String")); + } - const symbol_typet jlo_symbol("java::java.lang.Object"); - const struct_typet &jlo_type = to_struct_type(ns.follow(jlo_symbol)); - struct_exprt jlo_init(jlo_symbol); - java_root_class_init(jlo_init, jlo_type, class_id); + // OK, this is a String type with the expected fields -- add code to `code` + // to set up pre-requisite variables and assign them in `struct_expr`. - struct_exprt struct_expr(obj.type()); - struct_expr.copy_to_operands(jlo_init); + /// \todo Refactor with make_nondet_string_expr + // length_expr = nondet(int); + const symbolt length_sym = get_fresh_aux_symbol( + java_int_type(), + id2string(function_id), + "tmp_object_factory", + loc, + ID_java, + symbol_table); + const symbol_exprt length_expr = length_sym.symbol_expr(); + const side_effect_expr_nondett nondet_length(length_expr.type()); + code.add(code_declt(length_expr)); + code.add(code_assignt(length_expr, nondet_length)); - // In case the type for string was not added to the symbol table, - // (typically when string refinement is not activated), `struct_type` - // just contains the standard Object field and no length and data fields. - if(struct_type.has_component("length")) - { - /// \todo Refactor with make_nondet_string_expr - // length_expr = nondet(int); - const symbolt length_sym = get_fresh_aux_symbol( - java_int_type(), - id2string(function_id), - "tmp_object_factory", - loc, - ID_java, - symbol_table); - const symbol_exprt length_expr = length_sym.symbol_expr(); - const side_effect_expr_nondett nondet_length(length_expr.type()); - code.add(code_declt(length_expr)); - code.add(code_assignt(length_expr, nondet_length)); + // assume (length_expr >= 0); + code.add( + code_assumet( + binary_relation_exprt( + length_expr, ID_ge, from_integer(0, java_int_type())))); - // assume (length_expr >= 0); + // assume (length_expr <= max_input_length) + if(max_nondet_string_length <= max_value(length_expr.type())) + { + exprt max_length = + from_integer(max_nondet_string_length, length_expr.type()); code.add( - code_assumet( - binary_relation_exprt( - length_expr, ID_ge, from_integer(0, java_int_type())))); - - // assume (length_expr <= max_input_length) - if(max_nondet_string_length <= max_value(length_expr.type())) - { - exprt max_length = - from_integer(max_nondet_string_length, length_expr.type()); - code.add( - code_assumet(binary_relation_exprt(length_expr, ID_le, max_length))); - } + code_assumet(binary_relation_exprt(length_expr, ID_le, max_length))); + } - // char (*array_data_init)[INFINITY]; - const typet data_ptr_type = pointer_type( - array_typet(java_char_type(), infinity_exprt(java_int_type()))); + // char (*array_data_init)[INFINITY]; + const typet data_ptr_type = pointer_type( + array_typet(java_char_type(), infinity_exprt(java_int_type()))); - symbolt &data_pointer_sym = get_fresh_aux_symbol( - data_ptr_type, "", "string_data_pointer", loc, ID_java, symbol_table); - const auto data_pointer = data_pointer_sym.symbol_expr(); - code.add(code_declt(data_pointer)); + symbolt &data_pointer_sym = get_fresh_aux_symbol( + data_ptr_type, "", "string_data_pointer", loc, ID_java, symbol_table); + const auto data_pointer = data_pointer_sym.symbol_expr(); + code.add(code_declt(data_pointer)); - // Dynamic allocation: `data array = allocate char[INFINITY]` - code.add(make_allocate_code(data_pointer, infinity_exprt(java_int_type()))); + // Dynamic allocation: `data array = allocate char[INFINITY]` + code.add(make_allocate_code(data_pointer, infinity_exprt(java_int_type()))); - // `data_expr` is `*data_pointer` - // data_expr = nondet(char[INFINITY]) // we use infinity for variable size - const dereference_exprt data_expr(data_pointer); - const exprt nondet_array = - make_nondet_infinite_char_array(symbol_table, loc, function_id, code); - code.add(code_assignt(data_expr, nondet_array)); + // `data_expr` is `*data_pointer` + // data_expr = nondet(char[INFINITY]) // we use infinity for variable size + const dereference_exprt data_expr(data_pointer); + const exprt nondet_array = + make_nondet_infinite_char_array(symbol_table, loc, function_id, code); + code.add(code_assignt(data_expr, nondet_array)); - struct_expr.copy_to_operands(length_expr); + struct_expr.operands()[struct_type.component_number("length")] = length_expr; - const address_of_exprt array_pointer( - index_exprt(data_expr, from_integer(0, java_int_type()))); + const address_of_exprt array_pointer( + index_exprt(data_expr, from_integer(0, java_int_type()))); - add_pointer_to_array_association( - array_pointer, data_expr, symbol_table, loc, code); + add_pointer_to_array_association( + array_pointer, data_expr, symbol_table, loc, code); - add_array_to_length_association( - data_expr, length_expr, symbol_table, loc, code); + add_array_to_length_association( + data_expr, length_expr, symbol_table, loc, code); - struct_expr.copy_to_operands(array_pointer); + struct_expr.operands()[struct_type.component_number("data")] = array_pointer; - // Printable ASCII characters are between ' ' and '~'. - if(printable) - { - add_character_set_constraint( - array_pointer, length_expr, " -~", symbol_table, loc, code); - } + // Printable ASCII characters are between ' ' and '~'. + if(printable) + { + add_character_set_constraint( + array_pointer, length_expr, " -~", symbol_table, loc, code); } - // tmp_object = struct_expr; - code.add(code_assignt(obj, struct_expr)); - return code; -} - -/// Add code for the initialization of a string using a nondeterministic -/// content and association of its address to the pointer `expr`. -/// \param expr: pointer to be affected -/// \param max_nondet_string_length: maximum length of strings to initialize -/// \param printable: Boolean, true to force content to be printable -/// \param symbol_table: the symbol table -/// \param loc: location in the source -/// \param [out] code: code block in which initialization code is added -/// \return false if code was added, true to signal an error when the given -/// object does not implement CharSequence or does not have data and -/// length fields, in which case it should be initialized another way. -static bool add_nondet_string_pointer_initialization( - const exprt &expr, - const std::size_t &max_nondet_string_length, - bool printable, - symbol_table_baset &symbol_table, - const source_locationt &loc, - const irep_idt &function_id, - code_blockt &code) -{ - const namespacet ns(symbol_table); - const dereference_exprt obj(expr, expr.type().subtype()); - const struct_typet &struct_type = - to_struct_type(ns.follow(to_symbol_type(obj.type()))); - - // if no String model is loaded then we cannot construct a String object - if(struct_type.get_bool(ID_incomplete_class)) - return true; - - const exprt malloc_site = allocate_dynamic_object_with_decl( - expr, symbol_table, loc, function_id, code); - - code.add( - initialize_nondet_string_struct( - dereference_exprt(malloc_site, struct_type), - max_nondet_string_length, - loc, - function_id, - symbol_table, - printable)); - return false; + return true; } /// Initializes a pointer \p expr of type \p pointer_type to a primitive-typed @@ -831,35 +792,13 @@ void java_object_factoryt::gen_nondet_pointer_init( // and asign to `expr` the address of such object code_blockt non_null_inst; - // Note string-type-specific initialization might fail, e.g. if java.lang.CharSequence does not - // have the expected fields (typically this happens if --refine-strings was not passed). In this - // case we fall back to normal pointer target init. - bool string_init_succeeded = false; - - if(java_string_library_preprocesst::implements_java_char_sequence_pointer( - expr.type())) - { - string_init_succeeded = - !add_nondet_string_pointer_initialization( - expr, - object_factory_parameters.max_nondet_string_length, - object_factory_parameters.string_printable, - symbol_table, - loc, - object_factory_parameters.function_id, - assignments); - } - - if(!string_init_succeeded) - { - gen_pointer_target_init( - non_null_inst, - expr, - subtype, - alloc_type, - depth, - update_in_placet::NO_UPDATE_IN_PLACE); - } + gen_pointer_target_init( + non_null_inst, + expr, + subtype, + alloc_type, + depth, + update_in_placet::NO_UPDATE_IN_PLACE); auto set_null_inst=get_null_assignment(expr, pointer_type); @@ -1030,6 +969,8 @@ void java_object_factoryt::gen_nondet_struct_init( // case they will set `skip_classid` // * Not if we're re-initializing an existing object (i.e. update_in_place) + bool skip_special_string_fields = false; + if(!is_sub && !skip_classid && update_in_place != update_in_placet::MUST_UPDATE_IN_PLACE) @@ -1042,15 +983,28 @@ void java_object_factoryt::gen_nondet_struct_init( // This code mirrors the `remove_java_new` pass: null_message_handlert nullout; - exprt zero_object= + exprt initial_object = zero_initializer( struct_type, source_locationt(), ns, nullout); irep_idt qualified_clsid = "java::" + id2string(class_identifier); set_class_identifier( - to_struct_expr(zero_object), ns, symbol_typet(qualified_clsid)); + to_struct_expr(initial_object), ns, symbol_typet(qualified_clsid)); + + // If the initialised type is a special-cased String type (one with length + // and data fields introduced by string-library preprocessing), initialise + // those fields with nondet values: + skip_special_string_fields = + initialize_nondet_string_fields( + to_struct_expr(initial_object), + assignments, + object_factory_parameters.max_nondet_string_length, + loc, + object_factory_parameters.function_id, + symbol_table, + object_factory_parameters.string_printable); assignments.copy_to_operands( - code_assignt(expr, zero_object)); + code_assignt(expr, initial_object)); } for(const auto &component : components) @@ -1076,6 +1030,12 @@ void java_object_factoryt::gen_nondet_struct_init( code.add_source_location() = loc; assignments.copy_to_operands(code); } + else if(skip_special_string_fields && (name == "length" || name == "data")) + { + // In this case these were set up by initialise_nondet_string_fields + // above. + continue; + } else { INVARIANT(!name.empty(), "Each component of a struct must have a name"); diff --git a/jbmc/src/java_bytecode/java_object_factory.h b/jbmc/src/java_bytecode/java_object_factory.h index a1ce6bb51d6..d174d4e4ae2 100644 --- a/jbmc/src/java_bytecode/java_object_factory.h +++ b/jbmc/src/java_bytecode/java_object_factory.h @@ -150,12 +150,4 @@ exprt allocate_dynamic_object_with_decl( const irep_idt &function_id, code_blockt &output_code); -codet initialize_nondet_string_struct( - const exprt &obj, - const std::size_t &max_nondet_string_length, - const source_locationt &loc, - const irep_idt &function_id, - symbol_table_baset &symbol_table, - bool printable); - #endif // CPROVER_JAVA_BYTECODE_JAVA_OBJECT_FACTORY_H diff --git a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp index 032348e8ed6..53cc0e7f5ef 100644 --- a/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp +++ b/jbmc/unit/java_bytecode/java_object_factory/gen_nondet_string_init.cpp @@ -46,10 +46,22 @@ SCENARIO( symbol_typet java_string_type("java::java.lang.String"); symbol_exprt expr("arg", java_string_type); + object_factory_parameterst object_factory_parameters; + object_factory_parameters.max_nondet_string_length = 20; + object_factory_parameters.function_id = "test"; + WHEN("Initialisation code for a string is generated") { - const codet code = initialize_nondet_string_struct( - expr, 20, loc, "test", symbol_table, false); + code_blockt code; + gen_nondet_init( + expr, + code, + symbol_table, + loc, + false, + allocation_typet::DYNAMIC, + object_factory_parameters, + update_in_placet::NO_UPDATE_IN_PLACE); THEN("Code is produced") {