From 198f12674184160274de14efa20b75bf201f78a4 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 18 May 2021 19:34:07 -0700 Subject: [PATCH 1/3] Mark `jvm_*` commands as "Current" instead of "Experimental". --- src/SAWScript/Interpreter.hs | 38 ++++++++++++++++++------------------ 1 file changed, 19 insertions(+), 19 deletions(-) diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs index d9c33d7e26..aa44660ece 100644 --- a/src/SAWScript/Interpreter.hs +++ b/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,7 +2822,7 @@ 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." ] @@ -2830,7 +2830,7 @@ primitives = Map.fromList , 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,7 +2843,7 @@ 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." ] @@ -2851,13 +2851,13 @@ primitives = Map.fromList , 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`." ] --------------------------------------------------------------------- From 1f709c4e39163395709cdb5d7c3adc53443e60c3 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Tue, 18 May 2021 19:48:40 -0700 Subject: [PATCH 2/3] Remove now-unnecessary uses of `enable_experimental`. --- doc/tutorial/code/java_add.saw | 1 - examples/java/alloc.saw | 2 -- examples/java/arrayfield.saw | 2 -- examples/java/arrays.saw | 2 -- examples/java/branchsat.saw | 2 -- examples/java/bytearray.saw | 1 - examples/java/classtype.saw | 2 -- examples/java/fields.saw | 2 -- examples/java/get.saw | 2 -- examples/java/java_add.saw | 2 -- examples/java/java_types.saw | 1 - examples/java/return.saw | 2 -- examples/java/staticfield.saw | 2 -- intTests/test0001/javamd5test.saw | 1 - intTests/test0023_java_assert_false/test.saw | 1 - intTests/test_crucible_jvm/arr_crucible.java | 1 - intTests/test_crucible_jvm/arr_crucible.saw | 1 - intTests/test_crucible_jvm/dyn_crucible.saw | 1 - intTests/test_crucible_jvm/ffs_crucible.saw | 1 - intTests/test_crucible_jvm/obj_crucible.saw | 1 - intTests/test_crucible_jvm/stat_crucible.saw | 1 - intTests/test_crucible_jvm/statdyn_crucible.saw | 1 - intTests/test_crucible_jvm/sub_crucible.saw | 1 - intTests/test_crucible_jvm/teststr_crucible.saw | 1 - intTests/test_issue108/refarray.saw | 1 - intTests/test_jvm_method_names/test.saw | 1 - intTests/test_jvm_modifies/test.saw | 1 - intTests/test_jvm_setup_errors/test.saw | 1 - intTests/test_jvm_small_types/test.saw | 1 - intTests/test_jvm_static_fields/test.saw | 1 - intTests/test_jvm_unsound/test.saw | 1 - 31 files changed, 41 deletions(-) diff --git a/doc/tutorial/code/java_add.saw b/doc/tutorial/code/java_add.saw index 3a5dedaafa..394fcb77aa 100644 --- a/doc/tutorial/code/java_add.saw +++ b/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; diff --git a/examples/java/alloc.saw b/examples/java/alloc.saw index b6c0f62c0b..1e007f481b 100644 --- a/examples/java/alloc.saw +++ b/examples/java/alloc.saw @@ -1,5 +1,3 @@ -enable_experimental; - c <- java_load_class "Alloc"; jvm_verify c "alloc" [] false diff --git a/examples/java/arrayfield.saw b/examples/java/arrayfield.saw index e3db4b0b3f..02853e9bb3 100644 --- a/examples/java/arrayfield.saw +++ b/examples/java/arrayfield.saw @@ -1,5 +1,3 @@ -enable_experimental; - c <- java_load_class "ArrayField"; jvm_verify c "init" [] false diff --git a/examples/java/arrays.saw b/examples/java/arrays.saw index 8dd55f78ab..a4c9d8e056 100644 --- a/examples/java/arrays.saw +++ b/examples/java/arrays.saw @@ -1,5 +1,3 @@ -enable_experimental; - c <- java_load_class "ArrayTest"; copy_ms <- diff --git a/examples/java/branchsat.saw b/examples/java/branchsat.saw index 03b3dcc420..db1e812e34 100644 --- a/examples/java/branchsat.saw +++ b/examples/java/branchsat.saw @@ -1,5 +1,3 @@ -enable_experimental; - c <- java_load_class "BranchTest"; // FIXME: make this terminate with the symbolic precondition diff --git a/examples/java/bytearray.saw b/examples/java/bytearray.saw index c0b435ef7a..bb0da2cc71 100644 --- a/examples/java/bytearray.saw +++ b/examples/java/bytearray.saw @@ -1,4 +1,3 @@ -enable_experimental; c <- java_load_class "ByteArray"; jvm_verify c "id" [] false diff --git a/examples/java/classtype.saw b/examples/java/classtype.saw index e236e3e17d..e95f9f8656 100644 --- a/examples/java/classtype.saw +++ b/examples/java/classtype.saw @@ -1,5 +1,3 @@ -enable_experimental; - c <- java_load_class "ClassType"; jvm_verify c "id" [] false diff --git a/examples/java/fields.saw b/examples/java/fields.saw index 63724a3f49..9b090bbbee 100644 --- a/examples/java/fields.saw +++ b/examples/java/fields.saw @@ -1,5 +1,3 @@ -enable_experimental; - c <- java_load_class "Fields"; ms_setx <- diff --git a/examples/java/get.saw b/examples/java/get.saw index aaae7633a6..afd3b562bd 100644 --- a/examples/java/get.saw +++ b/examples/java/get.saw @@ -1,5 +1,3 @@ -enable_experimental; - c <- java_load_class "Get"; jvm_verify c "get" [] false diff --git a/examples/java/java_add.saw b/examples/java/java_add.saw index fa0eaa53ff..03e16501e4 100644 --- a/examples/java/java_add.saw +++ b/examples/java/java_add.saw @@ -1,5 +1,3 @@ -enable_experimental; - c <- java_load_class "Add"; let {{ diff --git a/examples/java/java_types.saw b/examples/java/java_types.saw index cbb0cfa31d..a4b754acd7 100644 --- a/examples/java/java_types.saw +++ b/examples/java/java_types.saw @@ -1,4 +1,3 @@ -enable_experimental; set_base 16; c <- java_load_class "JavaTypes"; diff --git a/examples/java/return.saw b/examples/java/return.saw index 07f4321531..e91b973483 100644 --- a/examples/java/return.saw +++ b/examples/java/return.saw @@ -1,5 +1,3 @@ -enable_experimental; - c <- java_load_class "Return"; let fill_spec = diff --git a/examples/java/staticfield.saw b/examples/java/staticfield.saw index 10c51850e2..3b859c4cc9 100644 --- a/examples/java/staticfield.saw +++ b/examples/java/staticfield.saw @@ -1,5 +1,3 @@ -enable_experimental; - c <- java_load_class "sfield.StaticField"; ms_setx <- diff --git a/intTests/test0001/javamd5test.saw b/intTests/test0001/javamd5test.saw index fc781a4751..c378236409 100644 --- a/intTests/test0001/javamd5test.saw +++ b/intTests/test0001/javamd5test.saw @@ -1,4 +1,3 @@ -enable_experimental; import "../../deps/cryptol-specs/Primitive/Keyless/Hash/MD5.cry"; let md5_spec = do { diff --git a/intTests/test0023_java_assert_false/test.saw b/intTests/test0023_java_assert_false/test.saw index 40ab1fa675..c3e5eca871 100644 --- a/intTests/test0023_java_assert_false/test.saw +++ b/intTests/test0023_java_assert_false/test.saw @@ -1,4 +1,3 @@ -enable_experimental; c <- java_load_class "Test0023"; fails ( jvm_verify c "id" [] false diff --git a/intTests/test_crucible_jvm/arr_crucible.java b/intTests/test_crucible_jvm/arr_crucible.java index 308c05090e..0cc3525bd0 100644 --- a/intTests/test_crucible_jvm/arr_crucible.java +++ b/intTests/test_crucible_jvm/arr_crucible.java @@ -1,4 +1,3 @@ -enable_experimental; a <- java_load_class "Arr"; print "**Extracting main"; diff --git a/intTests/test_crucible_jvm/arr_crucible.saw b/intTests/test_crucible_jvm/arr_crucible.saw index 006fe70281..3a420314d4 100644 --- a/intTests/test_crucible_jvm/arr_crucible.saw +++ b/intTests/test_crucible_jvm/arr_crucible.saw @@ -1,4 +1,3 @@ -enable_experimental; j <- java_load_class "Dyn"; a <- java_load_class "Arr"; diff --git a/intTests/test_crucible_jvm/dyn_crucible.saw b/intTests/test_crucible_jvm/dyn_crucible.saw index 73d3ac6131..01bc2f37bf 100644 --- a/intTests/test_crucible_jvm/dyn_crucible.saw +++ b/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"; diff --git a/intTests/test_crucible_jvm/ffs_crucible.saw b/intTests/test_crucible_jvm/ffs_crucible.saw index add2e23d4a..8bc440848f 100644 --- a/intTests/test_crucible_jvm/ffs_crucible.saw +++ b/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"; diff --git a/intTests/test_crucible_jvm/obj_crucible.saw b/intTests/test_crucible_jvm/obj_crucible.saw index d5b54a5945..08d8a701f1 100644 --- a/intTests/test_crucible_jvm/obj_crucible.saw +++ b/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"; diff --git a/intTests/test_crucible_jvm/stat_crucible.saw b/intTests/test_crucible_jvm/stat_crucible.saw index 3f776c0541..c6494a64b8 100644 --- a/intTests/test_crucible_jvm/stat_crucible.saw +++ b/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"; diff --git a/intTests/test_crucible_jvm/statdyn_crucible.saw b/intTests/test_crucible_jvm/statdyn_crucible.saw index bba88007fa..6d13ea11e5 100644 --- a/intTests/test_crucible_jvm/statdyn_crucible.saw +++ b/intTests/test_crucible_jvm/statdyn_crucible.saw @@ -1,4 +1,3 @@ -enable_experimental; jdyn <- java_load_class "Dyn"; jstat <- java_load_class "Stat"; diff --git a/intTests/test_crucible_jvm/sub_crucible.saw b/intTests/test_crucible_jvm/sub_crucible.saw index 58879b5224..43bf4ee3d6 100644 --- a/intTests/test_crucible_jvm/sub_crucible.saw +++ b/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"; diff --git a/intTests/test_crucible_jvm/teststr_crucible.saw b/intTests/test_crucible_jvm/teststr_crucible.saw index d3bba388a1..ba927609ec 100644 --- a/intTests/test_crucible_jvm/teststr_crucible.saw +++ b/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"; diff --git a/intTests/test_issue108/refarray.saw b/intTests/test_issue108/refarray.saw index 64ef0b354e..718f174108 100644 --- a/intTests/test_issue108/refarray.saw +++ b/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; diff --git a/intTests/test_jvm_method_names/test.saw b/intTests/test_jvm_method_names/test.saw index c4e114ce8f..513e13525a 100644 --- a/intTests/test_jvm_method_names/test.saw +++ b/intTests/test_jvm_method_names/test.saw @@ -1,4 +1,3 @@ -enable_experimental; c <- java_load_class "Test"; print c; diff --git a/intTests/test_jvm_modifies/test.saw b/intTests/test_jvm_modifies/test.saw index 5a35f7e1a8..2000b05bd7 100644 --- a/intTests/test_jvm_modifies/test.saw +++ b/intTests/test_jvm_modifies/test.saw @@ -1,4 +1,3 @@ -enable_experimental; c <- java_load_class "Test"; //////////////////////////////////////////////////////////////////////////////// diff --git a/intTests/test_jvm_setup_errors/test.saw b/intTests/test_jvm_setup_errors/test.saw index d92bae4392..bebe6929a8 100644 --- a/intTests/test_jvm_setup_errors/test.saw +++ b/intTests/test_jvm_setup_errors/test.saw @@ -15,7 +15,6 @@ saw-script. */ -enable_experimental; test <- java_load_class "Test"; print test; diff --git a/intTests/test_jvm_small_types/test.saw b/intTests/test_jvm_small_types/test.saw index b6a3700bef..86cb876794 100644 --- a/intTests/test_jvm_small_types/test.saw +++ b/intTests/test_jvm_small_types/test.saw @@ -1,4 +1,3 @@ -enable_experimental; c <- java_load_class "Test"; jvm_verify c "addBoolean" [] false diff --git a/intTests/test_jvm_static_fields/test.saw b/intTests/test_jvm_static_fields/test.saw index 14bdaa709a..d15a56fe48 100644 --- a/intTests/test_jvm_static_fields/test.saw +++ b/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"; diff --git a/intTests/test_jvm_unsound/test.saw b/intTests/test_jvm_unsound/test.saw index 636fa2a8f8..64a0041ef7 100644 --- a/intTests/test_jvm_unsound/test.saw +++ 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 = From 0cf8400c5eef78b79e21d737acb8640dad74ff05 Mon Sep 17 00:00:00 2001 From: Brian Huffman Date: Wed, 19 May 2021 09:47:16 -0700 Subject: [PATCH 3/3] Add notes to CHANGES.md related to new JVM verification commands. --- CHANGES.md | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index ac1e300239..16cd1ea2e6 100644 --- a/CHANGES.md +++ b/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