Merge pull request #1300 from GaloisInc/jvm-current

Mark `jvm_*` commands as "Current" instead of "Experimental".

CHANGES.md

@@ -1,3 +1,25 @@
+# Unreleased version
+
+## New Features
+
+Several improvements have been made to JVM verification:
+
+* For method specs that do not specify a final value for a field or
+  array element, it is now enforced that the method must leave that
+  field or element unmodified. This ensures soundness of the resulting
+  override for use in compositional verification.
+
+* New JVM setup commands have been introduced for writing partial
+  specifications: `jvm_modifies_field`, `jvm_modifies_static_field`,
+  `jvm_modifies_elem`, and `jvm_modifies_array`. Used in the
+  post-condition section of a spec, these declare that the field or
+  array in question may be modified by the method in an unspecified
+  manner.
+
+* All `jvm_` functions have all been promoted from "experimental" to
+  "current" status, so that `enable_experimental` is no longer
+  necessary for JVM verification.
+
 # Version 0.8
 
 ## New Features

doc/tutorial/code/java_add.saw

@@ -1,4 +1,3 @@
-enable_experimental;
 let add_spec = do {
     x <- jvm_fresh_var "x" java_int;
     y <- jvm_fresh_var "y" java_int;

examples/java/alloc.saw

@@ -1,5 +1,3 @@
-enable_experimental;
-
 c <- java_load_class "Alloc";
 
 jvm_verify c "alloc" [] false

examples/java/arrayfield.saw

@@ -1,5 +1,3 @@
-enable_experimental;
-
 c <- java_load_class "ArrayField";
 
 jvm_verify c "init" [] false

examples/java/arrays.saw

@@ -1,5 +1,3 @@
-enable_experimental;
-
 c <- java_load_class "ArrayTest";
 
 copy_ms <-

examples/java/branchsat.saw

@@ -1,5 +1,3 @@
-enable_experimental;
-
 c <- java_load_class "BranchTest";
 
 // FIXME: make this terminate with the symbolic precondition

examples/java/bytearray.saw

@@ -1,4 +1,3 @@
-enable_experimental;
 c <- java_load_class "ByteArray";
 
 jvm_verify c "id" [] false

examples/java/classtype.saw

@@ -1,5 +1,3 @@
-enable_experimental;
-
 c <- java_load_class "ClassType";
 
 jvm_verify c "id" [] false

examples/java/fields.saw

@@ -1,5 +1,3 @@
-enable_experimental;
-
 c <- java_load_class "Fields";
 
 ms_setx <-

examples/java/get.saw

@@ -1,5 +1,3 @@
-enable_experimental;
-
 c <- java_load_class "Get";
 
 jvm_verify c "get" [] false

examples/java/java_add.saw

@@ -1,5 +1,3 @@
-enable_experimental;
-
 c <- java_load_class "Add";
 
 let {{

examples/java/java_types.saw

@@ -1,4 +1,3 @@
-enable_experimental;
 set_base 16;
 
 c <- java_load_class "JavaTypes";

examples/java/return.saw

@@ -1,5 +1,3 @@
-enable_experimental;
-
 c <- java_load_class "Return";
 
 let fill_spec =

examples/java/staticfield.saw

@@ -1,5 +1,3 @@
-enable_experimental;
-
 c <- java_load_class "sfield.StaticField";
 
 ms_setx <-

intTests/test0001/javamd5test.saw

@@ -1,4 +1,3 @@
-enable_experimental;
 import "../../deps/cryptol-specs/Primitive/Keyless/Hash/MD5.cry";
 
 let md5_spec = do {

intTests/test0023_java_assert_false/test.saw

@@ -1,4 +1,3 @@
-enable_experimental;
 c <- java_load_class "Test0023";
 fails (
   jvm_verify c "id" [] false

intTests/test_crucible_jvm/arr_crucible.java

@@ -1,4 +1,3 @@
-enable_experimental;
 a <- java_load_class "Arr";
 
 print "**Extracting main";

intTests/test_crucible_jvm/arr_crucible.saw

@@ -1,4 +1,3 @@
-enable_experimental;
 j <- java_load_class "Dyn";
 a <- java_load_class "Arr";
 

intTests/test_crucible_jvm/dyn_crucible.saw

@@ -1,4 +1,3 @@
-enable_experimental;
 obj   <- java_load_class "java.lang.Object";
 iface <- java_load_class "Iface";
 

intTests/test_crucible_jvm/ffs_crucible.saw

@@ -1,4 +1,3 @@
-enable_experimental;
 print "Extracting reference term";
 j <- java_load_class "FFS";
 ffs_ref <- jvm_extract j "ffs_ref";

intTests/test_crucible_jvm/obj_crucible.saw

@@ -1,4 +1,3 @@
-enable_experimental;
 print "**loading TestStr";
 str <- java_load_class "java/lang/String";
 teststr <- java_load_class "TestStr";

intTests/test_crucible_jvm/stat_crucible.saw

@@ -1,4 +1,3 @@
-enable_experimental;
 print "**Extracting reference term";
 j <- java_load_class "Stat";
 f_ref <- jvm_extract j "f_ref";

intTests/test_crucible_jvm/statdyn_crucible.saw

@@ -1,4 +1,3 @@
-enable_experimental;
 jdyn <- java_load_class "Dyn";
 jstat <- java_load_class "Stat";
 

intTests/test_crucible_jvm/sub_crucible.saw

@@ -1,4 +1,3 @@
-enable_experimental;
 obj <- java_load_class "java.lang.Object";
 dyn <- java_load_class "Dyn";
 ifc <- java_load_class "Iface";

intTests/test_crucible_jvm/teststr_crucible.saw

@@ -1,4 +1,3 @@
-enable_experimental;
 print "**loading TestStr";
 str <- java_load_class "java/lang/String";
 t <- java_load_class "java/lang/Throwable";

intTests/test_issue108/refarray.saw

@@ -1,4 +1,3 @@
-enable_experimental;
 Test_class <- java_load_class "RefArray";
 let test1_spec : JVMSetup() = do {
   x <- jvm_fresh_var "x" java_int;

intTests/test_jvm_method_names/test.saw

@@ -1,4 +1,3 @@
-enable_experimental;
 c <- java_load_class "Test";
 print c;
 

intTests/test_jvm_modifies/test.saw

@@ -1,4 +1,3 @@
-enable_experimental;
 c <- java_load_class "Test";
 
 ////////////////////////////////////////////////////////////////////////////////

intTests/test_jvm_setup_errors/test.saw

@@ -15,7 +15,6 @@ saw-script.
 
 */
 
-enable_experimental;
 test <- java_load_class "Test";
 
 print test;

intTests/test_jvm_small_types/test.saw

@@ -1,4 +1,3 @@
-enable_experimental;
 c <- java_load_class "Test";
 
 jvm_verify c "addBoolean" [] false

intTests/test_jvm_static_fields/test.saw

@@ -1,4 +1,3 @@
-enable_experimental;
 a <- java_load_class "A";
 print a;
 b <- java_load_class "B";

intTests/test_jvm_unsound/test.saw

@@ -5,7 +5,6 @@
 // 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 =

src/SAWScript/Interpreter.hs

@@ -2668,14 +2668,14 @@ primitives = Map.fromList
 
   , prim "jvm_fresh_var" "String -> JavaType -> JVMSetup Term"
     (pureVal jvm_fresh_var)
-    Experimental
+    Current
     [ "Create a fresh variable for use within a JVM specification. The"
     , "name is used only for pretty-printing."
     ]
 
   , prim "jvm_alloc_object" "String -> JVMSetup JVMValue"
     (pureVal jvm_alloc_object)
-    Experimental
+    Current
     [ "Declare that an instance of the given class should be allocated in a"
     , "JVM specification. Before `jvm_execute_func`, this states that the"
     , "method expects the object to be allocated before it runs. After"
@@ -2685,7 +2685,7 @@ primitives = Map.fromList
 
   , prim "jvm_alloc_array" "Int -> JavaType -> JVMSetup JVMValue"
     (pureVal jvm_alloc_array)
-    Experimental
+    Current
     [ "Declare that an array of the given size and element type should be"
     , "allocated in a JVM specification. Before `jvm_execute_func`, this"
     , "states that the method expects the array to be allocated before it"
@@ -2697,7 +2697,7 @@ primitives = Map.fromList
 
   , prim "jvm_modifies_field" "JVMValue -> String -> JVMSetup ()"
     (pureVal jvm_modifies_field)
-    Experimental
+    Current
     [ "Declare that the indicated object (first argument) has a field"
     , "(second argument) containing an unspecified value."
     , ""
@@ -2709,7 +2709,7 @@ primitives = Map.fromList
 
   , prim "jvm_modifies_static_field" "String -> JVMSetup ()"
     (pureVal jvm_modifies_static_field)
-    Experimental
+    Current
     [ "Declare that the named static field contains an unspecified"
     , "value."
     , ""
@@ -2721,7 +2721,7 @@ primitives = Map.fromList
 
   , prim "jvm_modifies_elem" "JVMValue -> Int -> JVMSetup ()"
     (pureVal jvm_modifies_elem)
-    Experimental
+    Current
     [ "Declare that the indicated array (first argument) has an element"
     , "(second argument) containing an unspecified value."
     , ""
@@ -2733,7 +2733,7 @@ primitives = Map.fromList
 
   , prim "jvm_modifies_array" "JVMValue -> JVMSetup ()"
     (pureVal jvm_modifies_array)
-    Experimental
+    Current
     [ "Declare that the indicated array's elements contain unspecified"
     , "values."
     , ""
@@ -2745,7 +2745,7 @@ primitives = Map.fromList
 
   , prim "jvm_field_is" "JVMValue -> String -> JVMValue -> JVMSetup ()"
     (pureVal jvm_field_is)
-    Experimental
+    Current
     [ "Declare that the indicated object (first argument) has a field"
     , "(second argument) containing the given value (third argument)."
     , ""
@@ -2757,7 +2757,7 @@ primitives = Map.fromList
 
   , prim "jvm_static_field_is" "String -> JVMValue -> JVMSetup ()"
     (pureVal jvm_static_field_is)
-    Experimental
+    Current
     [ "Declare that the named static field contains the given value."
     , "By default the field name is assumed to belong to the same class"
     , "as the method being specified. Static fields belonging to other"
@@ -2772,7 +2772,7 @@ primitives = Map.fromList
 
   , prim "jvm_elem_is" "JVMValue -> Int -> JVMValue -> JVMSetup ()"
     (pureVal jvm_elem_is)
-    Experimental
+    Current
     [ "Declare that the indicated array (first argument) has an element"
     , "(second argument) containing the given value (third argument)."
     , ""
@@ -2784,7 +2784,7 @@ primitives = Map.fromList
 
   , prim "jvm_array_is" "JVMValue -> Term -> JVMSetup ()"
     (pureVal jvm_array_is)
-    Experimental
+    Current
     [ "Declare that the indicated array reference (first argument) contains"
     , "the given sequence of values (second argument)."
     , ""
@@ -2796,21 +2796,21 @@ primitives = Map.fromList
 
   , prim "jvm_precond" "Term -> JVMSetup ()"
     (pureVal jvm_precond)
-    Experimental
+    Current
     [ "State that the given predicate is a pre-condition on execution of the"
     , "method being verified."
     ]
 
   , prim "jvm_postcond" "Term -> JVMSetup ()"
     (pureVal jvm_postcond)
-    Experimental
+    Current
     [ "State that the given predicate is a post-condition of execution of the"
     , "method being verified."
     ]
 
   , prim "jvm_execute_func" "[JVMValue] -> JVMSetup ()"
     (pureVal jvm_execute_func)
-    Experimental
+    Current
     [ "Specify the given list of values as the arguments of the method."
     ,  ""
     , "The jvm_execute_func statement also serves to separate the pre-state"
@@ -2822,15 +2822,15 @@ primitives = Map.fromList
 
   , prim "jvm_return" "JVMValue -> JVMSetup ()"
     (pureVal jvm_return)
-    Experimental
+    Current
     [ "Specify the given value as the return value of the method. A"
     , "jvm_return statement is required if and only if the method"
     , "has a non-void return type." ]
 
   , prim "jvm_verify"
     "JavaClass -> String -> [JVMSpec] -> Bool -> JVMSetup () -> ProofScript () -> TopLevel JVMSpec"
     (pureVal jvm_verify)
-    Experimental
+    Current
     [ "Verify the JVM method named by the second parameter in the class"
     , "specified by the first. The third parameter lists the JVMSpec values"
     , "returned by previous calls to use as overrides. The fourth (Bool)"
@@ -2843,21 +2843,21 @@ primitives = Map.fromList
   , prim "jvm_unsafe_assume_spec"
     "JavaClass -> String -> JVMSetup () -> TopLevel JVMSpec"
     (pureVal jvm_unsafe_assume_spec)
-    Experimental
+    Current
     [ "Return a JVMSpec corresponding to a JVMSetup block, as would be"
     , "returned by jvm_verify but without performing any verification."
     ]
 
   , prim "jvm_null"
     "JVMValue"
     (pureVal (CMS.SetupNull () :: CMS.SetupValue CJ.JVM))
-    Experimental
+    Current
     [ "A JVMValue representing a null pointer value." ]
 
   , prim "jvm_term"
     "Term -> JVMValue"
     (pureVal (CMS.SetupTerm :: TypedTerm -> CMS.SetupValue CJ.JVM))
-    Experimental
+    Current
     [ "Construct a `JVMValue` from a `Term`." ]
 
     ---------------------------------------------------------------------