From 4d67b075643eac6870e4f791dead97f2a2073056 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Fri, 5 Feb 2021 11:24:02 -0800 Subject: [PATCH] Add regression tests for jvm_verify soundness bugs (issue #900). Currently these tests are configured as known failures; the tests will need to be updated when the bugs are fixed. --- intTests/test_jvm_unsound/Makefile | 2 + intTests/test_jvm_unsound/Test.class | Bin 0 -> 580 bytes intTests/test_jvm_unsound/Test.java | 18 ++++++ intTests/test_jvm_unsound/test.saw | 91 +++++++++++++++++++++++++++ intTests/test_jvm_unsound/test.sh | 1 + 5 files changed, 112 insertions(+) create mode 100644 intTests/test_jvm_unsound/Makefile create mode 100644 intTests/test_jvm_unsound/Test.class create mode 100644 intTests/test_jvm_unsound/Test.java create mode 100644 intTests/test_jvm_unsound/test.saw create mode 100644 intTests/test_jvm_unsound/test.sh diff --git a/intTests/test_jvm_unsound/Makefile b/intTests/test_jvm_unsound/Makefile new file mode 100644 index 0000000000..94675b9b1f --- /dev/null +++ b/intTests/test_jvm_unsound/Makefile @@ -0,0 +1,2 @@ +%.class: %.java + javac -g $< diff --git a/intTests/test_jvm_unsound/Test.class b/intTests/test_jvm_unsound/Test.class new file mode 100644 index 0000000000000000000000000000000000000000..2ab6aefa515206263eb9923a23a5dbe83ece69c1 GIT binary patch literal 580 zcmZ9H%TB^j5QhKLmX;nWASzz!ZHZmT#+}AQO-M+HE+lMCi;b2bBv6bG<;HvB!Uyo7 zjQ?qyN?go+=9`)CpU*D<2iTD?v2LS)4W(R3wP|6?!nT0$DQ!w1U>-%IC_Wa@8+$zg z<7|8#3RF7LC_JCt1>vOY2Sa9RopIkE_WVht;w)*zx6zc0PB)y!hh$8{n2bhSp~M3# zF$-5*r*hnw##}2e$FoU4Y(6znL$66IXbav4#1kD23)E(k6e!bo(gsveWhB&MYBk(q zw?-@77igaQ2K|pvhR%w`bww_=6H-0x&PeKvC05k|%UH>nCmGZB+;o3NkCMrF oiJv)hI6KGLIj)}LPBWZLaNaBQ|GWx$)j6Kbd4K1vCO5480^Th_7XSbN literal 0 HcmV?d00001 diff --git a/intTests/test_jvm_unsound/Test.java b/intTests/test_jvm_unsound/Test.java new file mode 100644 index 0000000000..0b19b4a3e9 --- /dev/null +++ b/intTests/test_jvm_unsound/Test.java @@ -0,0 +1,18 @@ +class Test +{ + static int a; + int b; + + public void set(int x) { + a = x; + b = x; + } + public int test_a(int x) { + set(x); + return a; + } + public int test_b(int x) { + set(x); + return b; + } +} diff --git a/intTests/test_jvm_unsound/test.saw b/intTests/test_jvm_unsound/test.saw new file mode 100644 index 0000000000..a8588a3830 --- /dev/null +++ b/intTests/test_jvm_unsound/test.saw @@ -0,0 +1,91 @@ +// This is a regression test for saw-script issue #900; it tests whether +// `jvm_verify` will successfully verify a spec that does not specify a +// new value for a field, when the method actually does modify that +// field. For soundness of compositional verification, it is required +// that such a verification will fail. +// https://github.com/GaloisInc/saw-script/issues/900 + +enable_experimental; +c <- java_load_class "Test"; + +let set_spec_1 = + do { + this <- jvm_alloc_object "Test"; + x <- jvm_fresh_var "x" java_int; + jvm_execute_func [this, jvm_term x]; + jvm_field_is this "b" (jvm_term x); + }; + +let set_spec_2 = + do { + this <- jvm_alloc_object "Test"; + x <- jvm_fresh_var "x" java_int; + jvm_execute_func [this, jvm_term x]; + jvm_static_field_is "a" (jvm_term x); + }; + +set_ov_1 <- jvm_unsafe_assume_spec c "set" set_spec_1; +set_ov_2 <- jvm_unsafe_assume_spec c "set" set_spec_2; + +let one = jvm_term {{ 1:[32] }}; +let two = jvm_term {{ 2:[32] }}; + +// A correct spec for test_a. +jvm_verify c "test_a" [] false + do { + this <- jvm_alloc_object "Test"; + jvm_static_field_is "a" one; + jvm_execute_func [this, two]; + jvm_static_field_is "a" two; + jvm_field_is this "b" two; + jvm_return two; + } + z3; + +// An incorrect spec for test_a, which can be proven using the bogus +// spec set_ov_1. +jvm_verify c "test_a" [set_ov_1] false + do { + this <- jvm_alloc_object "Test"; + jvm_static_field_is "a" one; + jvm_execute_func [this, two]; + jvm_static_field_is "a" one; + jvm_field_is this "b" two; + jvm_return one; + } + z3; + +// A correct spec for test_b. +jvm_verify c "test_b" [] false + do { + this <- jvm_alloc_object "Test"; + jvm_static_field_is "a" one; + jvm_field_is this "b" one; + jvm_execute_func [this, two]; + jvm_static_field_is "a" two; + jvm_field_is this "b" two; + jvm_return two; + } + z3; + +// An incorrect spec for test_b, which can be proven using the bogus +// spec set_ov_2. +jvm_verify c "test_b" [set_ov_2] false + do { + this <- jvm_alloc_object "Test"; + jvm_static_field_is "a" one; + jvm_field_is this "b" one; + jvm_execute_func [this, two]; + jvm_static_field_is "a" two; + jvm_field_is this "b" one; + jvm_return one; + } + z3; + +// It should be impossible to verify the bogus set_spec_1. +// FIXME: this should fail +jvm_verify c "set" [] false set_spec_1 z3; + +// It should be impossible to verify the bogus set_spec_2. +// FIXME: this should fail +jvm_verify c "set" [] false set_spec_2 z3; diff --git a/intTests/test_jvm_unsound/test.sh b/intTests/test_jvm_unsound/test.sh new file mode 100644 index 0000000000..0b864017cd --- /dev/null +++ b/intTests/test_jvm_unsound/test.sh @@ -0,0 +1 @@ +$SAW test.saw