From f075399cac6b402346e9f94af424c678c255ee4f Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Tue, 18 May 2021 18:06:01 -0700
Subject: [PATCH] Add new regression test for jvm_modifies declarations.

---
 intTests/test_jvm_modifies/Makefile   |   2 +
 intTests/test_jvm_modifies/Test.class | Bin 0 -> 920 bytes
 intTests/test_jvm_modifies/Test.java  |  31 +++++
 intTests/test_jvm_modifies/test.saw   | 170 ++++++++++++++++++++++++++
 intTests/test_jvm_modifies/test.sh    |   1 +
 5 files changed, 204 insertions(+)
 create mode 100644 intTests/test_jvm_modifies/Makefile
 create mode 100644 intTests/test_jvm_modifies/Test.class
 create mode 100644 intTests/test_jvm_modifies/Test.java
 create mode 100644 intTests/test_jvm_modifies/test.saw
 create mode 100644 intTests/test_jvm_modifies/test.sh

diff --git a/intTests/test_jvm_modifies/Makefile b/intTests/test_jvm_modifies/Makefile
new file mode 100644
index 0000000000..94675b9b1f
--- /dev/null
+++ b/intTests/test_jvm_modifies/Makefile
@@ -0,0 +1,2 @@
+%.class: %.java
+	javac -g $<
diff --git a/intTests/test_jvm_modifies/Test.class b/intTests/test_jvm_modifies/Test.class
new file mode 100644
index 0000000000000000000000000000000000000000..e01192f456b0baa996f7499ccc28810a6afd9354
GIT binary patch
literal 920
zcma)&OHUJF6o%igop!EVENFo#SV6R%g^ib;gbjhDSYZKS<HoP;1csE>lp^|{+!#<3
z7yJNzl<_^x<bx1MSe*A<=6ugNb1wh=y#VkIkp~ygTsT-1SrU2fQI<tsh`h8>vr$)2
zn%1PXX&r^!Cnm*}q@Rpd74o(Eo`SVD=*9{Yt)w4sogB5};jV7?SShsz9o^g0!$k6|
zXpIh%V=`L1@$u+AU+Zr7wL+oRY}RGaH`@2K{3dm8`So<DzetyOmajbP-p=4;*oik1
z8RrV|)uH~X1598tfCoQ7AToyW08da3FeehCOtiEsOv-~sPxtp5+wH@+GeVUIaCxab
zjR>kE6nY4VYSTCY3Xd2y=oNh-`UCZoK@KHq@v5jW#W+YCFpbB|Agiz<k3X<m2DwrA
z3%RiJ`3I8};L*$M0=E%JHElEy7c<;SCcBtrB;EYI47{0vo$w6#JGf)8_%GL7$8a6P
zbqtpm%eWu8g)Hnx=di4B`wn!82b#Kp_6^!MXy2eK2ECr4?I^7LM&bGr=_$)MkhVeE
h25B4Q{5{CxZRFg8kqh@A?c2!t2O<@o@`^cB{{yMJQdR%}

literal 0
HcmV?d00001

diff --git a/intTests/test_jvm_modifies/Test.java b/intTests/test_jvm_modifies/Test.java
new file mode 100644
index 0000000000..260213dd14
--- /dev/null
+++ b/intTests/test_jvm_modifies/Test.java
@@ -0,0 +1,31 @@
+class Test
+{
+    int a;
+    static int b;
+    int[] c;
+
+    int add1 (int x, int y) {
+        a = x;
+        return x + y;
+    }
+
+    int add2 (int x, int y) {
+        b = x;
+        return x + y;
+    }
+
+    int add3 (int x, int y) {
+        c[1] = x;
+        return x + y;
+    }
+
+    int wrap1 (int x, int y) {
+        return add1 (x, y);
+    }
+    int wrap2 (int x, int y) {
+        return add2 (x, y);
+    }
+    int wrap3 (int x, int y) {
+        return add3 (x, y);
+    }
+}
diff --git a/intTests/test_jvm_modifies/test.saw b/intTests/test_jvm_modifies/test.saw
new file mode 100644
index 0000000000..5a35f7e1a8
--- /dev/null
+++ b/intTests/test_jvm_modifies/test.saw
@@ -0,0 +1,170 @@
+enable_experimental;
+c <- java_load_class "Test";
+
+////////////////////////////////////////////////////////////////////////////////
+// Specs with missing side effects
+
+print "Verification fails for add1 spec with missing side effect.";
+fails (
+  jvm_verify c "add1" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    x <- jvm_fresh_var "x" java_int;
+    y <- jvm_fresh_var "y" java_int;
+    jvm_execute_func [this, jvm_term x, jvm_term y];
+    jvm_return (jvm_term {{ x + y }});
+  } z3
+  );
+
+print "Verification fails for add2 spec with missing side effect.";
+fails (
+  jvm_verify c "add2" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    x <- jvm_fresh_var "x" java_int;
+    y <- jvm_fresh_var "y" java_int;
+    jvm_execute_func [this, jvm_term x, jvm_term y];
+    jvm_return (jvm_term {{ x + y }});
+  } z3
+  );
+
+print "Verification fails for add3 spec with missing side effect.";
+fails (
+  jvm_verify c "add3" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    arr <- jvm_alloc_array 2 java_int;
+    jvm_field_is this "c" arr;
+    x <- jvm_fresh_var "x" java_int;
+    y <- jvm_fresh_var "y" java_int;
+    jvm_execute_func [this, jvm_term x, jvm_term y];
+    jvm_return (jvm_term {{ x + y }});
+  } z3
+  );
+
+////////////////////////////////////////////////////////////////////////////////
+// Full specifications with side effects
+
+let spec1 =
+  do {
+    this <- jvm_alloc_object "Test";
+    x <- jvm_fresh_var "x" java_int;
+    y <- jvm_fresh_var "y" java_int;
+    jvm_execute_func [this, jvm_term x, jvm_term y];
+    jvm_field_is this "a" (jvm_term x);
+    jvm_return (jvm_term {{ x + y }});
+  };
+
+let spec2 =
+  do {
+    this <- jvm_alloc_object "Test";
+    x <- jvm_fresh_var "x" java_int;
+    y <- jvm_fresh_var "y" java_int;
+    jvm_execute_func [this, jvm_term x, jvm_term y];
+    jvm_static_field_is "b" (jvm_term x);
+    jvm_return (jvm_term {{ x + y }});
+  };
+
+let spec3 =
+  do {
+    this <- jvm_alloc_object "Test";
+    arr <- jvm_alloc_array 2 java_int;
+    jvm_field_is this "c" arr;
+    x <- jvm_fresh_var "x" java_int;
+    y <- jvm_fresh_var "y" java_int;
+    jvm_execute_func [this, jvm_term x, jvm_term y];
+    jvm_elem_is arr 1 (jvm_term x);
+    jvm_return (jvm_term {{ x + y }});
+  };
+
+print "Verification succeeds for complete add1 spec.";
+add1_full <- jvm_verify c "add1" [] false spec1 z3;
+
+print "Verification succeeds for complete add2 spec.";
+add2_full <- jvm_verify c "add2" [] false spec2 z3;
+
+print "Verification succeeds for complete add3 spec.";
+add3_full <- jvm_verify c "add3" [] false spec3 z3;
+
+////////////////////////////////////////////////////////////////////////////////
+// Partial specifications with jvm_modifies
+
+print "Verification succeeds for partial add1 spec (jvm_modifies_field).";
+add1_part <-
+  jvm_verify c "add1" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    x <- jvm_fresh_var "x" java_int;
+    y <- jvm_fresh_var "y" java_int;
+    jvm_execute_func [this, jvm_term x, jvm_term y];
+    jvm_modifies_field this "a";
+    jvm_return (jvm_term {{ x + y }});
+  } z3;
+
+print "Verification succeeds for partial add2 spec (jvm_modifies_static_field).";
+add2_part <-
+  jvm_verify c "add2" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    x <- jvm_fresh_var "x" java_int;
+    y <- jvm_fresh_var "y" java_int;
+    jvm_execute_func [this, jvm_term x, jvm_term y];
+    jvm_modifies_static_field "b";
+    jvm_return (jvm_term {{ x + y }});
+  } z3;
+
+print "Verification succeeds for partial add3 spec (jvm_modifies_elem).";
+add3_part <-
+  jvm_verify c "add3" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    arr <- jvm_alloc_array 2 java_int;
+    jvm_field_is this "c" arr;
+    x <- jvm_fresh_var "x" java_int;
+    y <- jvm_fresh_var "y" java_int;
+    jvm_execute_func [this, jvm_term x, jvm_term y];
+    jvm_modifies_elem arr 1;
+    jvm_return (jvm_term {{ x + y }});
+  } z3;
+
+print "Verification succeeds for partial add3 spec (jvm_modifies_array).";
+add3_part_a <-
+  jvm_verify c "add3" [] false
+  do {
+    this <- jvm_alloc_object "Test";
+    arr <- jvm_alloc_array 2 java_int;
+    jvm_field_is this "c" arr;
+    x <- jvm_fresh_var "x" java_int;
+    y <- jvm_fresh_var "y" java_int;
+    jvm_execute_func [this, jvm_term x, jvm_term y];
+    jvm_modifies_array arr;
+    jvm_return (jvm_term {{ x + y }});
+  } z3;
+
+////////////////////////////////////////////////////////////////////////////////
+// Compositional verification with full specs
+
+print "Compositional verification succeeds with full add1 spec.";
+wrap1_full <- jvm_verify c "wrap1" [add1_full] false spec1 z3;
+
+print "Compositional verification succeeds with full add1 spec.";
+wrap2_full <- jvm_verify c "wrap2" [add2_full] false spec2 z3;
+
+print "Compositional verification succeeds with full add1 spec.";
+wrap3_full <- jvm_verify c "wrap3" [add3_full] false spec3 z3;
+
+////////////////////////////////////////////////////////////////////////////////
+// Compositional verification with partial specs
+
+// TODO: Improve misleading "Ill-formed value for type int" error message.
+
+print "Compositional verification fails with partial add1 spec.";
+fails (jvm_verify c "wrap1" [add1_part] false spec1 z3);
+
+print "Compositional verification fails with partial add2 spec.";
+fails (jvm_verify c "wrap2" [add2_part] false spec2 z3);
+
+print "Compositional verification fails with partial add3 spec.";
+fails (jvm_verify c "wrap3" [add3_part] false spec3 z3);
+
+print "DONE!";
diff --git a/intTests/test_jvm_modifies/test.sh b/intTests/test_jvm_modifies/test.sh
new file mode 100644
index 0000000000..0b864017cd
--- /dev/null
+++ b/intTests/test_jvm_modifies/test.sh
@@ -0,0 +1 @@
+$SAW test.saw