From 57988fc581c1b91d1d1fe5b18a015e40a8dcb460 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Wed, 16 May 2018 12:06:49 +0100 Subject: [PATCH] Fix String type initialisation when --refine-strings is not active Previously this would incorrectly leave a branch on which the object was not initialised at all. Now it is always initialised, falling back to conventional initialisation when string-specific init is not possible. --- .../NondetCharSequence.class | Bin 0 -> 768 bytes .../NondetCharSequence.java | 10 ++++++ .../cbmc-java/NondetCharSequence/test.desc | 8 +++++ .../cbmc-java/NondetString/NondetString.class | Bin 0 -> 738 bytes .../cbmc-java/NondetString/NondetString.java | 10 ++++++ regression/cbmc-java/NondetString/test.desc | 8 +++++ .../NondetStringBuffer.class | Bin 0 -> 768 bytes .../NondetStringBuffer.java | 10 ++++++ .../cbmc-java/NondetStringBuffer/test.desc | 8 +++++ .../NondetStringBuilder.class | Bin 0 -> 773 bytes .../NondetStringBuilder.java | 10 ++++++ .../cbmc-java/NondetStringBuilder/test.desc | 8 +++++ src/java_bytecode/java_object_factory.cpp | 31 +++++++++++------- 13 files changed, 91 insertions(+), 12 deletions(-) create mode 100644 regression/cbmc-java/NondetCharSequence/NondetCharSequence.class create mode 100644 regression/cbmc-java/NondetCharSequence/NondetCharSequence.java create mode 100644 regression/cbmc-java/NondetCharSequence/test.desc create mode 100644 regression/cbmc-java/NondetString/NondetString.class create mode 100644 regression/cbmc-java/NondetString/NondetString.java create mode 100644 regression/cbmc-java/NondetString/test.desc create mode 100644 regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.class create mode 100644 regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.java create mode 100644 regression/cbmc-java/NondetStringBuffer/test.desc create mode 100644 regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.class create mode 100644 regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.java create mode 100644 regression/cbmc-java/NondetStringBuilder/test.desc diff --git a/regression/cbmc-java/NondetCharSequence/NondetCharSequence.class b/regression/cbmc-java/NondetCharSequence/NondetCharSequence.class new file mode 100644 index 0000000000000000000000000000000000000000..b4af31db09374bd8184688f6e08e34cc2f3de4e9 GIT binary patch literal 768 zcmZuuO>fgc5Pcgv*~E35G;Pz+@{!UOk|5QW-lz~Lz=aTyQWeqL#$GjBT)V98ir^;8^ZoYVzFamV#9U0MAw(XM=~QV+}1GFvIH4I8r@n>KFYHbd?IS~e`q zkd?{ngFiEQq;;sN$7z0!ri~Wb43$aUv%#TsW14EH4;=SchbK}yo#)xfFc)OQc%kB9 zFY$dEPqXz``xnJDp7MmS);Vc0!RsA9W7W zq{yL@(V1_bgPl>3Lz(`C?9xDmV*3Jsc~mJYVqsh?2%Q$MeL(Ijj3;klj!IF<=jAIoiLV!(WrzejNd ZZl1z4-oc#qos#5{v+t+fU7;k0mEU*Npd|nR literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NondetCharSequence/NondetCharSequence.java b/regression/cbmc-java/NondetCharSequence/NondetCharSequence.java new file mode 100644 index 00000000000..eb8200154c6 --- /dev/null +++ b/regression/cbmc-java/NondetCharSequence/NondetCharSequence.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetCharSequence +{ + static void main() + { + CharSequence x = CProver.nondetWithNull(); + assert x == null || x instanceof CharSequence; + } +} diff --git a/regression/cbmc-java/NondetCharSequence/test.desc b/regression/cbmc-java/NondetCharSequence/test.desc new file mode 100644 index 00000000000..baaa60614e5 --- /dev/null +++ b/regression/cbmc-java/NondetCharSequence/test.desc @@ -0,0 +1,8 @@ +CORE +NondetCharSequence.class + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetString/NondetString.class b/regression/cbmc-java/NondetString/NondetString.class new file mode 100644 index 0000000000000000000000000000000000000000..1e93b74e30fa7e1aa96648f6533e8d0cc879e7e8 GIT binary patch literal 738 zcmZWmOK;Oa5dJoHvWe?9kCqTx9w`(^f`l)as?b$INA=1SmRiC za23}$HW-#SM3P9IsyIp>s6>oI88EP2hSHXbRC<@e>U4J)?0y_bhU!2?ayUI0OTBHH z85)Dw7vYZ3%A8M&cDkn$hNZzUjslsEQmvxN9YQ$}DkA(>W^P{`2`?1U#LMp&N2%~% zJ`sl*4k>3SZ~5V=5@!@owJ#qj!&{$+zHP8vxLD-4?&1b+GSvRXci~`xp>KU9{=_D)g?b)-oO_v*;tYAWq6Wii~2hcMSH1 zk^-vqFJ(mwHOk$S2Gr4@QyI(ou%K=;y#4`&udp7!g*`*F_Z^MiH&`<)d_wWXF-l(y zu$2KXW&E5}l}TGAC*WAc3eHhqGb3R?(dIZ$U9FsMGb01)4gMbG8Myr#w)GD7|GEuG P5e4_2ad&|Z1+4xClS!1v literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NondetString/NondetString.java b/regression/cbmc-java/NondetString/NondetString.java new file mode 100644 index 00000000000..e2c14ae76f7 --- /dev/null +++ b/regression/cbmc-java/NondetString/NondetString.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetString +{ + static void main() + { + String x = CProver.nondetWithNull(); + assert x == null || x instanceof String; + } +} diff --git a/regression/cbmc-java/NondetString/test.desc b/regression/cbmc-java/NondetString/test.desc new file mode 100644 index 00000000000..6756c4a7630 --- /dev/null +++ b/regression/cbmc-java/NondetString/test.desc @@ -0,0 +1,8 @@ +CORE +NondetString.class + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.class b/regression/cbmc-java/NondetStringBuffer/NondetStringBuffer.class new file mode 100644 index 0000000000000000000000000000000000000000..4a2de67ab40cd612ec068bee8a31477f47cfb8ae GIT binary patch literal 768 zcmZuuO>fgc5Pcgv*~E35G%aap`ADJAB$et*Z&U~fa3KVwR7Lc*vA5|K*RIxf)!&jo zz!{Jz0*Q|c2YwSmjNOtT!ol8|-8b*OnfdYS<7WU{*sxH-iiIn<%5kj(j_Vu^3wf+? ztXjB%n;dHl3u_{Zq>fb>L=ROY2EOzd*d9Y+TLmh<%V0EHy9{P0^dv*Ms{+|ejs{Zi zq+o_>H*|%+E3``Ui%T;;P!Ypow-*MUjQg=x!SF${zc2M2;yMy4AeB>wdiPMA2*($} z(D?^7+mD6&>Zv%+IH?PU;_RouHJmm>t$EWp>aZg4{OKfgc5PcIn-Nbd9G;Pzg{YtOwX3yL@mul- zI0F(zAn|eGz;8l`v0D-Zrf}R2v(!HL$EuMuLz~C4pnb-Fi_@c z3MN##ktc&4X>^*OUfRi?jtR@%UKIK&=_f{q!@DCL_{!X5vID6@mU&57?e5DX*$!kl zZ2t|L>nGBC@kkzKtUL#yueL4MTWIXjir(M*}5W0~vyKpflaK*({TqCUfN6m$U zS*Dpj-}&v!ePbfSPMx73&~VX2i%^~xJ|65VFX4j74BOtJiH?+Mcb;S?VLr?pd8U)S z-Y5tNOO56q7Mv8bMWrcWC*U0ss=kV~QU0Vcb|)F}121S7bzX6iS5M_yItoV?e>^)_ zlcP4D#Am*B40_E$4kiB2WS17o9J?m~ETF_9r<2`a;U_E>TdyH!98!D}@ zu*R7Ei2UsOBj?^ur(5MDhqYfKC8Es$ literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.java b/regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.java new file mode 100644 index 00000000000..feec3c3ac6b --- /dev/null +++ b/regression/cbmc-java/NondetStringBuilder/NondetStringBuilder.java @@ -0,0 +1,10 @@ +import org.cprover.CProver; + +class NondetStringBuilder +{ + static void main() + { + StringBuilder x = CProver.nondetWithNull(); + assert x == null || x instanceof StringBuilder; + } +} diff --git a/regression/cbmc-java/NondetStringBuilder/test.desc b/regression/cbmc-java/NondetStringBuilder/test.desc new file mode 100644 index 00000000000..6aa68c42d41 --- /dev/null +++ b/regression/cbmc-java/NondetStringBuilder/test.desc @@ -0,0 +1,8 @@ +CORE +NondetStringBuilder.class + +^VERIFICATION SUCCESSFUL$ +^EXIT=0$ +^SIGNAL=0$ +-- +^warning: ignoring diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index 4bd9380547f..6e9617cb109 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -841,20 +841,27 @@ void java_object_factoryt::gen_nondet_pointer_init( // and asign to `expr` the address of such object code_blockt non_null_inst; - if( - java_string_library_preprocesst::implements_java_char_sequence_pointer( - expr.type())) + // 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())) { - 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); + 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); } - else + + if(!string_init_succeeded) { gen_pointer_target_init( non_null_inst,