JVM write permissions

examples/java/get.saw

@@ -9,7 +9,7 @@ jvm_verify c "get" [] false
     j <- jvm_fresh_var "j" java_int;
     jvm_precond {{ j <= 3 }};
     jvm_execute_func [this, a, jvm_term j];
-    // TODO: Update spec to say `a` is modified but not specified
+    jvm_modifies_array a;
     jvm_return (jvm_term {{ j }});
   }
   abc;

intTests/test_jvm_modifies/Makefile

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

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

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!";

intTests/test_jvm_modifies/test.sh

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

intTests/test_jvm_setup_errors/Test.java

@@ -1,6 +1,7 @@
 class Test
 {
     long val;
+    static long counter;
 
     long get () {
         return val;
@@ -14,4 +15,8 @@ boolean lessThan (Test t) {
     static long lookup (long arr[], int idx) {
         return arr[idx];
     }
+    static long next () {
+        counter = counter + 1;
+        return counter;
+    }
 }

intTests/test_jvm_setup_errors/test.saw

@@ -120,6 +120,94 @@ check_fails test "get"
     jvm_return (jvm_term val);
   };
 
+print "jvm_modifies_field in pre-state section";
+check_fails test "get"
+  do {
+    this <- jvm_alloc_object "Test";
+    val <- jvm_fresh_var "val" java_long;
+    jvm_modifies_field this "val";
+    jvm_execute_func [this];
+    jvm_return (jvm_term val);
+  };
+
+print "Working spec for method 'next'";
+jvm_verify test "next" [] false
+  do {
+    ctr <- jvm_fresh_var "ctr" java_long;
+    jvm_static_field_is "counter" (jvm_term ctr);
+    jvm_execute_func [];
+    let ctr' = {{ ctr + 1 }};
+    jvm_static_field_is "counter" (jvm_term ctr');
+    jvm_return (jvm_term ctr');
+  } z3;
+
+print "jvm_static_field_is with non-monomorphic type";
+check_fails test "next"
+  do {
+    let ctr = {{ 0 }};
+    jvm_static_field_is "counter" (jvm_term ctr);
+    jvm_execute_func [];
+    let ctr' = {{ 1 }};
+    jvm_static_field_is "counter" (jvm_term ctr');
+    jvm_return (jvm_term ctr');
+  };
+
+print "jvm_static_field_is with non-jvm type";
+check_fails test "next"
+  do {
+    let ctr = {{ 0 : Integer }};
+    jvm_static_field_is "counter" (jvm_term ctr);
+    jvm_execute_func [];
+    let ctr' = {{ ctr + 1 }};
+    jvm_static_field_is "counter" (jvm_term ctr');
+    jvm_return (jvm_term ctr');
+  };
+
+print "jvm_static_field_is with wrong type";
+check_fails test "next"
+  do {
+    let ctr = {{ 0 : [32] }};
+    jvm_static_field_is "counter" (jvm_term ctr);
+    jvm_execute_func [];
+    let ctr' = {{ ctr + 1 }};
+    jvm_static_field_is "counter" (jvm_term ctr');
+    jvm_return (jvm_term ctr');
+  };
+
+print "jvm_static_field_is with non-existent field name";
+check_fails test "next"
+  do {
+    ctr <- jvm_fresh_var "ctr" java_long;
+    jvm_static_field_is "count" (jvm_term ctr);
+    jvm_execute_func [];
+    let ctr' = {{ ctr + 1 }};
+    jvm_static_field_is "count" (jvm_term ctr');
+    jvm_return (jvm_term ctr');
+  };
+
+print "jvm_static_field_is with previous jvm_static_field_is on same field";
+check_fails test "next"
+  do {
+    ctr <- jvm_fresh_var "ctr" java_long;
+    jvm_static_field_is "counter" (jvm_term ctr);
+    jvm_static_field_is "counter" (jvm_term ctr);
+    jvm_execute_func [];
+    let ctr' = {{ ctr + 1 }};
+    jvm_static_field_is "counter" (jvm_term ctr');
+    jvm_return (jvm_term ctr');
+  };
+
+print "jvm_modifies_static_field in pre-state section";
+check_fails test "next"
+  do {
+    ctr <- jvm_fresh_var "ctr" java_long;
+    jvm_modifies_static_field "counter";
+    jvm_execute_func [];
+    let ctr' = {{ ctr + 1 }};
+    jvm_static_field_is "counter" (jvm_term ctr');
+    jvm_return (jvm_term ctr');
+  };
+
 print "Working spec for method 'lookup'";
 jvm_verify test "lookup" [] false
   do {
@@ -233,6 +321,17 @@ check_fails test "lookup"
     jvm_return (jvm_term x);
   };
 
+print "jvm_modifies_elem in pre-state section";
+check_fails test "lookup"
+  do {
+    arr <- jvm_alloc_array 8 java_long;
+    let idx = {{ 2 : [32] }};
+    x <- jvm_fresh_var "x" java_long;
+    jvm_modifies_elem arr 2;
+    jvm_execute_func [arr, jvm_term idx];
+    jvm_return (jvm_term x);
+  };
+
 print "Working spec for method 'lookup' (jvm_array_is)";
 jvm_verify test "lookup" [] false
   do {
@@ -356,6 +455,17 @@ check_fails test "lookup"
     jvm_return (jvm_term {{ xs @ idx }});
   };
 
+print "jvm_modifies_array in pre-state section";
+check_fails test "lookup"
+  do {
+    arr <- jvm_alloc_array 8 java_long;
+    let idx = {{ 2 : [32] }};
+    x <- jvm_fresh_var "x" java_long;
+    jvm_modifies_array arr;
+    jvm_execute_func [arr, jvm_term idx];
+    jvm_return (jvm_term x);
+  };
+
 print "Working spec for method 'set'";
 jvm_verify test "set" [] false
   do {

intTests/test_jvm_unsound/test.saw

@@ -86,5 +86,6 @@ jvm_verify c "test_b" [set_ov_2] false
 fails (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;
+fails (jvm_verify c "set" [] false set_spec_2 z3);
+
+print "Done.";