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.

Author: Brian Huffman

intTests/test_jvm_unsound/Makefile

@@ -0,0 +1,2 @@
+%.class: %.java
+	javac -g $<

intTests/test_jvm_unsound/Test.class

@@ -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;
+    }
+}

intTests/test_jvm_unsound/Test.java

@@ -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;

intTests/test_jvm_unsound/test.saw

@@ -0,0 +1 @@
+$SAW test.saw