From 0b5a5c384d7d0d328a632ced37ca0ffcf4a5d8e4 Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 26 Jan 2018 14:13:52 +0000 Subject: [PATCH 1/2] Rename test case Validate referred to the old name for cproverNondetInitialize, cproverNondetValidate. --- .../{NondetInitValidate => NondetInit}/Test.class | Bin .../{NondetInitValidate => NondetInit}/Test.java | 0 .../{NondetInitValidate => NondetInit}/test.desc | 0 .../test_lazy.desc | 0 4 files changed, 0 insertions(+), 0 deletions(-) rename regression/cbmc-java/{NondetInitValidate => NondetInit}/Test.class (100%) rename regression/cbmc-java/{NondetInitValidate => NondetInit}/Test.java (100%) rename regression/cbmc-java/{NondetInitValidate => NondetInit}/test.desc (100%) rename regression/cbmc-java/{NondetInitValidate => NondetInit}/test_lazy.desc (100%) diff --git a/regression/cbmc-java/NondetInitValidate/Test.class b/regression/cbmc-java/NondetInit/Test.class similarity index 100% rename from regression/cbmc-java/NondetInitValidate/Test.class rename to regression/cbmc-java/NondetInit/Test.class diff --git a/regression/cbmc-java/NondetInitValidate/Test.java b/regression/cbmc-java/NondetInit/Test.java similarity index 100% rename from regression/cbmc-java/NondetInitValidate/Test.java rename to regression/cbmc-java/NondetInit/Test.java diff --git a/regression/cbmc-java/NondetInitValidate/test.desc b/regression/cbmc-java/NondetInit/test.desc similarity index 100% rename from regression/cbmc-java/NondetInitValidate/test.desc rename to regression/cbmc-java/NondetInit/test.desc diff --git a/regression/cbmc-java/NondetInitValidate/test_lazy.desc b/regression/cbmc-java/NondetInit/test_lazy.desc similarity index 100% rename from regression/cbmc-java/NondetInitValidate/test_lazy.desc rename to regression/cbmc-java/NondetInit/test_lazy.desc From 5669d9b7bf2855e3294c731b925fe2e742f8043d Mon Sep 17 00:00:00 2001 From: Chris Smowton Date: Fri, 26 Jan 2018 13:51:00 +0000 Subject: [PATCH 2/2] Java: run nondet-initialize method *after* initialization Previously this method was run after each supertype of a relevant type was initialised, e.g. if MyClass <: MySupertype <: Object, then MyClass.cproverNondetInitialize would get run after my inner Object was set up, then again after MySupertype was set up, then one more time after the whole class was set up. Now it will only run after the whole initialisation is complete. This fixes a bug where array members could have inconsistent length and data field values because they had not been initialised yet, leading to an assertion failure during nondetInitialize, and also has the desirable side-effect that an initialiser will still be run when creating a subtype. --- regression/cbmc-java/NondetInit2/Test.class | Bin 0 -> 452 bytes regression/cbmc-java/NondetInit2/Test.java | 16 +++++++++++++ regression/cbmc-java/NondetInit2/test.desc | 5 ++++ .../cbmc-java/NondetInit3/Subclass.class | Bin 0 -> 174 bytes regression/cbmc-java/NondetInit3/Test.class | Bin 0 -> 729 bytes regression/cbmc-java/NondetInit3/Test.java | 22 ++++++++++++++++++ regression/cbmc-java/NondetInit3/test.desc | 5 ++++ src/java_bytecode/java_object_factory.cpp | 10 ++++---- 8 files changed, 53 insertions(+), 5 deletions(-) create mode 100644 regression/cbmc-java/NondetInit2/Test.class create mode 100644 regression/cbmc-java/NondetInit2/Test.java create mode 100644 regression/cbmc-java/NondetInit2/test.desc create mode 100644 regression/cbmc-java/NondetInit3/Subclass.class create mode 100644 regression/cbmc-java/NondetInit3/Test.class create mode 100644 regression/cbmc-java/NondetInit3/Test.java create mode 100644 regression/cbmc-java/NondetInit3/test.desc diff --git a/regression/cbmc-java/NondetInit2/Test.class b/regression/cbmc-java/NondetInit2/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..323039fe3ae1ffab233ecbfe08ed08b4781e0bbd GIT binary patch literal 452 zcmZXPu}{K46vn@6uhiB8RZu`ad>x^-}ml&-~0agTmv}Au?q|P4mb)fia4-wXrshn3Z)o~hZaNTGK!=0 zidd~aVBpPUBpLGUD3+b&Y$#P<45vg&;anvvsX9qKl4*s|>!@gQc4t)NOQ%UiV~Du)I-y%@R^uJ)l^zVc zbY?bCw|alAZThNPPaAJAzToR?&7WcO7jW|frUs@z>S`NfW0TuXE7Pnhkt`_|jN&zI XjU4jir$bbzwDZ3JIl?{(2KIgd5SU8* literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NondetInit2/Test.java b/regression/cbmc-java/NondetInit2/Test.java new file mode 100644 index 00000000000..8f81787947a --- /dev/null +++ b/regression/cbmc-java/NondetInit2/Test.java @@ -0,0 +1,16 @@ +import org.cprover.CProver; + +class Test { + + int[] arr; + + void cproverNondetInitialize() { + CProver.assume(arr != null && arr.length == 1); + // The following access should now be legal: + arr[0] = 100; + } + + public static void main(Test nondetInput) { + } + +} diff --git a/regression/cbmc-java/NondetInit2/test.desc b/regression/cbmc-java/NondetInit2/test.desc new file mode 100644 index 00000000000..d75e7538e9b --- /dev/null +++ b/regression/cbmc-java/NondetInit2/test.desc @@ -0,0 +1,5 @@ +CORE +Test.class + +^VERIFICATION SUCCESSFUL$ + diff --git a/regression/cbmc-java/NondetInit3/Subclass.class b/regression/cbmc-java/NondetInit3/Subclass.class new file mode 100644 index 0000000000000000000000000000000000000000..ff6f1ffb00111e1d4689a261397bc350e10f1591 GIT binary patch literal 174 zcmX^0Z`VEs1_l!bUM>b^1}=66ZgvJ9Mg}&U%)HDJJ4Oa(4b3n{1{UZ1lvG9rexJ;| zRKL>Pq|~C2#H1Xc2v=}^X;E^jTPBFZ8IoFDqL-CemdL}v!obSNz!6-Ul$?`TTnsb; xB*&n@zy!1f1Q>xBs0K*00a>y@8YIH1wVi=+BUqXpNV0(ig@GgokjKQp2>?fgc7=&l-O`N!Hnzo?{Erpb}kOo99y-^S-fK(~8NU4wrC&yk@E{R>)P7nN) zUf{-=4^aeCxN+b|A!e<79M=2p>)F|7cK`nSIR>zg`!;N>7g4~5jT_k1)y*PqVZ%b* zMjq=Hwrt$SwuK!5(~V;RW-TvDo%qaOr8aa+aD-jK=cIi2SFI5kEw3#y%vz| z$X5bOogh?4qhVjgCt55}_0HqyLd8c>=&SUQdjfY5yyu_AZt8mPUb^QKr5w6J$abUC z9re8d4}Pef3kTj{a+KYTMzN<}1lqWGqLTE%nS0?nSVGys0vrpw4({NtgGH1qGz4l| z&>FbmY3u1U$@4gl7*J{h3wsWlxF=AaE06nU%1fC(iceb;{#N@{mV?PjHX4#ZHhLN0 z6qoVm9&H^!V9i%a5G#LnI76o+{@}IsQ0GI~d?JH`_&~X)$+?moOa*~uR-2p!=Unp& z;xh|@6@K$s(`2;zv>A!2^smk! g_cJ44d8P0j#mfoYSID`?G}{EmAq-!WW(KbR2Sl%ey#N3J literal 0 HcmV?d00001 diff --git a/regression/cbmc-java/NondetInit3/Test.java b/regression/cbmc-java/NondetInit3/Test.java new file mode 100644 index 00000000000..edcea5419ca --- /dev/null +++ b/regression/cbmc-java/NondetInit3/Test.java @@ -0,0 +1,22 @@ +import org.cprover.CProver; + +class Test { + + int[] arr; + + void cproverNondetInitialize() { + CProver.assume(arr != null && arr.length == 1); + // The following access should now be legal: + arr[0] = 100; + } + + public static void main(Subclass nondetInput) { + // The condition enforced by cproverNondetInitialize should hold + // even though the parameter is a subtype of Test, not directly an + // instance of Test itself. + assert nondetInput.arr.length == 1; + } + +} + +class Subclass extends Test { } diff --git a/regression/cbmc-java/NondetInit3/test.desc b/regression/cbmc-java/NondetInit3/test.desc new file mode 100644 index 00000000000..d75e7538e9b --- /dev/null +++ b/regression/cbmc-java/NondetInit3/test.desc @@ -0,0 +1,5 @@ +CORE +Test.class + +^VERIFICATION SUCCESSFUL$ + diff --git a/src/java_bytecode/java_object_factory.cpp b/src/java_bytecode/java_object_factory.cpp index c44eaeb7edf..a1706cde435 100644 --- a/src/java_bytecode/java_object_factory.cpp +++ b/src/java_bytecode/java_object_factory.cpp @@ -1076,16 +1076,16 @@ void java_object_factoryt::gen_nondet_struct_init( } } - // If .cproverValidate() can be found in the + // If .cproverNondetInitialize() can be found in the // symbol table, we add a call: // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - // expr.cproverValidate(); + // expr.cproverNondetInitialize(); // ~~~~~~~~~~~~~~~~~~~~~~~~~~~~ - const irep_idt validate_method_name = - "java::" + id2string(class_identifier) + ".cproverNondetInitialize:()V"; + const irep_idt init_method_name = + "java::" + id2string(struct_tag) + ".cproverNondetInitialize:()V"; - if(const auto func = symbol_table.lookup(validate_method_name)) + if(const auto func = symbol_table.lookup(init_method_name)) { const code_typet &type = to_code_type(func->type); code_function_callt fun_call;