Merge pull request #1958 from GaloisInc/T1929

Support ghost values in all language backends

Author: mergify[bot]

CHANGES.md

@@ -17,6 +17,13 @@
   generating LLVM setup scripts for Cryptol FFI functions with the
   `llvm_ffi_setup` command. For more information, see the [manual](https://github.com/GaloisInc/saw-script/blob/master/doc/manual/manual.md#verifying-cryptol-ffi-functions).
 
+* Ghost state is now supported with the JVM and MIR language backends:
+  * The `llvm_declare_ghost_state` command is now deprecated in favor of the
+    new `declare_ghost_state` command, as nothing about this command is
+    LLVM-specific.
+  * Add `jvm_ghost_value` and `mir_ghost_value` commands in addition to the
+    existing `llvm_ghost_value` command.
+
 # Version 1.0 -- 2023-06-26
 
 ## New Features

crucible-mir-comp/src/Mir/Compositional/Builder.hs

@@ -641,8 +641,8 @@ substMethodSpec sc sm ms = do
         MS.SetupCond_Equal loc <$> goSetupValue sv1 <*> goSetupValue sv2
     goSetupCondition (MS.SetupCond_Pred loc tt) =
         MS.SetupCond_Pred loc <$> goTypedTerm tt
-    goSetupCondition (MS.SetupCond_Ghost b loc gg tt) =
-        MS.SetupCond_Ghost b loc gg <$> goTypedTerm tt
+    goSetupCondition (MS.SetupCond_Ghost loc gg tt) =
+        MS.SetupCond_Ghost loc gg <$> goTypedTerm tt
 
     goSetupSlice (MirSetupSliceRaw ref len) =
       MirSetupSliceRaw <$> goSetupValue ref <*> goSetupValue len

crucible-mir-comp/src/Mir/Compositional/Override.hs

@@ -581,7 +581,7 @@ condTerm sc (MS.SetupCond_Pred md tt) = do
     sub <- use MS.termSub
     t' <- liftIO $ SAW.scInstantiateExt sc sub $ SAW.ttTerm tt
     return (md, t')
-condTerm _ (MS.SetupCond_Ghost _ _ _ _) = do
+condTerm _ (MS.SetupCond_Ghost _ _ _) = do
     error $ "learnCond: SetupCond_Ghost is not supported"
 
 

doc/manual/manual.md

@@ -3541,18 +3541,19 @@ thought of as additional global state that is visible only to the
 verifier. Ghost state with a given name can be declared at the top level
 with the following function:
 
-* `llvm_declare_ghost_state : String -> TopLevel Ghost`
+* `declare_ghost_state : String -> TopLevel Ghost`
 
 Ghost state variables do not initially have any particluar type, and can
 store data of any type. Given an existing ghost variable the following
-function can be used to specify its value:
+functions can be used to specify its value:
 
 * `llvm_ghost_value : Ghost -> Term -> LLVMSetup ()`
+* `jvm_ghost_value  : Ghost -> Term -> JVMSetup  ()`
+* `mir_ghost_value  : Ghost -> Term -> MIRSetup  ()`
 
-Currently, this function can only be used for LLVM verification, though
-that will likely be generalized in the future. It can be used in either
-the pre state or the post state, to specify the value of ghost state
-either before or after the execution of the function, respectively.
+These can be used in either the pre state or the post state, to specify the
+value of ghost state either before or after the execution of the function,
+respectively.
 
 ## An Extended Example
 

doc/manual/manual.pdf

@@ -16,7 +16,7 @@ let example_spec counter : CrucibleSetup () = do {
 };
 
 let main : TopLevel () = do {
-    counter <- llvm_declare_ghost_state "ctr";
+    counter <- declare_ghost_state "ctr";
 
     m <- llvm_load_module "simple.bc";
     next <- llvm_unsafe_assume_spec m "next" (next_spec counter);

examples/ghost/ghost.saw

@@ -26,7 +26,7 @@ let f_spec (counter : Ghost) : CrucibleSetup () = do {
 };
 
 let main : TopLevel () = do {
-  counter <- llvm_declare_ghost_state "counter";
+  counter <- declare_ghost_state "counter";
   m <- llvm_load_module "test.bc";
   get_and_increment_ov <-
     llvm_unsafe_assume_spec m "get_and_increment" (get_and_increment_spec counter);

intTests/test_ghost/test.saw

@@ -25,7 +25,7 @@ let g_spec : CrucibleSetup () = do {
 };
 
 let main : TopLevel () = do {
-  x <- llvm_declare_ghost_state "x";
+  x <- declare_ghost_state "x";
   m <- llvm_load_module "test.bc";
   f_lt_ov <- llvm_unsafe_assume_spec m "f" (f_lt_spec x);
   f_ge_ov <- llvm_unsafe_assume_spec m "f" (f_ge_spec x);

intTests/test_ghost_branch_00/test.saw

@@ -28,7 +28,7 @@ let h_spec : CrucibleSetup () = do {
 };
 
 let main : TopLevel () = do {
-  x <- llvm_declare_ghost_state "x";
+  x <- declare_ghost_state "x";
   m <- llvm_load_module "test.bc";
   get_ov <- llvm_unsafe_assume_spec m "get" (get_spec x);
   f_ov <- llvm_unsafe_assume_spec m "f" (f_spec x);

intTests/test_ghost_branch_01/test.saw

@@ -21,7 +21,7 @@ let g_spec : CrucibleSetup () = do {
 };
 
 let main : TopLevel () = do {
-  x <- llvm_declare_ghost_state "x";
+  x <- declare_ghost_state "x";
   m <- llvm_load_module "test.bc";
   f_lt_ov <- llvm_unsafe_assume_spec m "f" (f_lt_spec x);
   f_ge_ov <- llvm_unsafe_assume_spec m "f" (f_ge_spec x);

intTests/test_ghost_branch_02/test.saw

@@ -28,7 +28,7 @@ let h_spec : CrucibleSetup () = do {
 };
 
 let main : TopLevel () = do {
-  x <- llvm_declare_ghost_state "x";
+  x <- declare_ghost_state "x";
   m <- llvm_load_module "test.bc";
   get_ov <- llvm_unsafe_assume_spec m "get" (get_spec x);
   f_ov <- llvm_unsafe_assume_spec m "f" (f_spec x);

intTests/test_ghost_branch_03/test.saw

@@ -23,7 +23,7 @@ let h_spec : CrucibleSetup () = do {
 };
 
 let main : TopLevel () = do {
-  x <- llvm_declare_ghost_state "x";
+  x <- declare_ghost_state "x";
   m <- llvm_load_module "test.bc";
   f_ov <- llvm_unsafe_assume_spec m "f" (f_spec x);
   // This spec should probably use a different variable, but doesn't:

intTests/test_ghost_types_00/test.saw

@@ -0,0 +1,13 @@
+all: test.linked-mir.json
+
+test.linked-mir.json: test.rs
+	saw-rustc $<
+	$(MAKE) remove-unused-build-artifacts
+
+.PHONY: remove-unused-build-artifacts
+remove-unused-build-artifacts:
+	rm -f test libtest.mir libtest.rlib
+
+.PHONY: clean
+clean: remove-unused-build-artifacts
+	rm -f test.linked-mir.json

intTests/test_mir_ghost/Makefile

@@ -0,0 +1,9 @@
+pub fn next() -> u32 {
+    unimplemented!("This should be overridden")
+}
+
+pub fn example() -> u32 {
+    next();
+    next();
+    next()
+}

intTests/test_mir_ghost/test.linked-mir.json

@@ -0,0 +1,28 @@
+enable_experimental;
+
+let next_spec counter = do {
+  n <- mir_fresh_var "n" mir_u32;
+  mir_ghost_value counter n;
+
+  mir_execute_func [];
+
+  mir_ghost_value counter {{n+1}};
+  mir_return (mir_term {{n}});
+};
+
+let example_spec counter = do {
+  n <- mir_fresh_var "nm" mir_u32;
+  mir_precond {{n < 2}};
+  mir_ghost_value counter n;
+
+  mir_execute_func [];
+
+  mir_ghost_value counter {{n+3}};
+  mir_return (mir_term {{n+2}});
+};
+
+counter <- declare_ghost_state "ctr";
+m <- mir_load_module "test.linked-mir.json";
+
+next <- mir_unsafe_assume_spec m "test::next" (next_spec counter);
+mir_verify m "test::example" [next] false (example_spec counter) z3;

intTests/test_mir_ghost/test.rs

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

intTests/test_mir_ghost/test.saw

@@ -0,0 +1,13 @@
+all: test.linked-mir.json
+
+test.linked-mir.json: test.rs
+	saw-rustc $<
+	$(MAKE) remove-unused-build-artifacts
+
+.PHONY: remove-unused-build-artifacts
+remove-unused-build-artifacts:
+	rm -f test libtest.mir libtest.rlib
+
+.PHONY: clean
+clean: remove-unused-build-artifacts
+	rm -f test.linked-mir.json

intTests/test_mir_ghost/test.sh

@@ -0,0 +1 @@
+{"fns":[{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::bool"}],"body":{"blocks":[{"block":{"data":[{"kind":"Assign","lhs":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"}},"pos":"test.rs:5:8: 5:9","rhs":{"kind":"Use","usevar":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::bool"}},"kind":"Copy"}}}],"terminator":{"discr":{"data":{"data":[],"var":{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"}},"kind":"Move"},"discr_span":"test.rs:5:8: 5:9 !test.rs:5:8: 5:9","kind":"SwitchInt","pos":"test.rs:5:8: 5:9 !test.rs:5:8: 5:9","switch_ty":"ty::bool","targets":["bb2","bb1"],"values":["0"]}},"blockid":"bb0"},{"block":{"data":[],"terminator":{"args":[{"data":{"rendered":{"kind":"uint","size":4,"val":"27"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::140cf1f14525dfe1"},"kind":"Constant"},"kind":"Call","pos":"test.rs:6:9: 6:14"}},"blockid":"bb1"},{"block":{"data":[],"terminator":{"args":[{"data":{"rendered":{"kind":"uint","size":4,"val":"42"},"ty":"ty::u32"},"kind":"Constant"}],"cleanup":null,"destination":[{"data":[],"var":{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}},"bb3"],"from_hir_call":true,"func":{"data":{"rendered":{"kind":"zst"},"ty":"ty::FnDef::140cf1f14525dfe1"},"kind":"Constant"},"kind":"Call","pos":"test.rs:8:9: 8:14"}},"blockid":"bb2"},{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:10:2: 10:2"}},"blockid":"bb3"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"},{"is_zst":false,"mut":{"kind":"Mut"},"name":"_2","ty":"ty::bool"}]},"name":"test/2c9d3c4c::g","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null},{"abi":{"kind":"Rust"},"args":[{"is_zst":false,"mut":{"kind":"Not"},"name":"_1","ty":"ty::u32"}],"body":{"blocks":[{"block":{"data":[],"terminator":{"kind":"Return","pos":"test.rs:2:21: 2:21"}},"blockid":"bb0"}],"vars":[{"is_zst":true,"mut":{"kind":"Mut"},"name":"_0","ty":"ty::Tuple::e93222e871854c41"}]},"name":"test/2c9d3c4c::f","return_ty":"ty::Tuple::e93222e871854c41","spread_arg":null}],"adts":[],"statics":[],"vtables":[],"traits":[],"intrinsics":[{"inst":{"def_id":"test/2c9d3c4c::g","kind":"Item","substs":[]},"name":"test/2c9d3c4c::g"},{"inst":{"def_id":"test/2c9d3c4c::f","kind":"Item","substs":[]},"name":"test/2c9d3c4c::f"}],"tys":[{"name":"ty::bool","ty":{"kind":"Bool"}},{"name":"ty::Tuple::e93222e871854c41","ty":{"kind":"Tuple","tys":[]}},{"name":"ty::FnDef::140cf1f14525dfe1","ty":{"defid":"test/2c9d3c4c::f","kind":"FnDef"}},{"name":"ty::u32","ty":{"kind":"Uint","uintkind":{"kind":"U32"}}}],"roots":["test/2c9d3c4c::f","test/2c9d3c4c::g"]}

intTests/test_mir_ghost_symbolic_branch/Makefile

@@ -0,0 +1,10 @@
+// Meant to be overridden
+pub fn f(_x: u32) {}
+
+pub fn g(b: bool) {
+    if b {
+        f(27)
+    } else {
+        f(42)
+    }
+}

intTests/test_mir_ghost_symbolic_branch/test.linked-mir.json

@@ -0,0 +1,24 @@
+enable_experimental;
+
+m <- mir_load_module "test.linked-mir.json";
+
+g <- declare_ghost_state "g";
+
+let f_spec = do {
+    x <- mir_fresh_var "x" mir_u32;
+
+    mir_execute_func [mir_term x];
+
+    mir_ghost_value g x;
+};
+
+let g_spec = do {
+    b <- mir_fresh_var "b" mir_bool;
+
+    mir_execute_func [mir_term b];
+
+    mir_ghost_value g ({{ if b then 27 else 42 : [32] }});
+};
+
+f_ov <- mir_unsafe_assume_spec m "test::f" f_spec;
+mir_verify m "test::g" [f_ov] false g_spec z3;

intTests/test_mir_ghost_symbolic_branch/test.rs

@@ -0,0 +1,3 @@
+set -e
+
+$SAW test.saw

intTests/test_mir_ghost_symbolic_branch/test.saw

@@ -35,6 +35,8 @@
 * Add `"slice"` and `"slice range"` `setup value`s representing slices in MIR
   verification. Attempting to use these in LLVM or JVM verification will raise
   an error.
+* The `SAW/create ghost variable` command and the associated
+  `ghost variable value` value are now supported with JVM and MIR verification.
 
 ## 1.0.0 -- 2023-06-26
 

intTests/test_mir_ghost_symbolic_branch/test.sh

@@ -38,6 +38,8 @@
   variable. This function is currently only supported with LLVM and MIR
   verification, and using this function with JVM verification will raise an
   error.
+* The `create_ghost_variable()` and `ghost_value()` functions are now supported
+  with JVM and MIR verification.
 
 ## 1.0.1 -- YYYY-MM-DD
 

saw-remote-api/CHANGELOG.md

@@ -0,0 +1,9 @@
+pub fn next() -> u32 {
+    unimplemented!("This should be overridden")
+}
+
+pub fn example() -> u32 {
+    next();
+    next();
+    next()
+}

saw-remote-api/python/CHANGELOG.md

@@ -0,0 +1,53 @@
+import unittest
+from pathlib import Path
+
+from saw_client import *
+from saw_client.crucible import cry_f
+from saw_client.mir import Contract, GhostVariable, u32
+
+
+class NextContract(Contract):
+    def __init__(self, counter: GhostVariable) -> None:
+        super().__init__()
+        self.counter = counter
+
+    def specification(self) -> None:
+        n = self.fresh_var(u32, 'n')
+        self.ghost_value(self.counter, n)
+
+        self.execute_func()
+
+        self.ghost_value(self.counter, cry_f('{n} + 1'))
+        self.returns(n)
+
+
+class ExampleContract(Contract):
+    def __init__(self, counter: GhostVariable) -> None:
+        super().__init__()
+        self.counter = counter
+
+    def specification(self) -> None:
+        n = self.fresh_var(u32, 'n')
+        self.precondition_f('{n} < 2')
+        self.ghost_value(self.counter, n)
+
+        self.execute_func()
+        self.ghost_value(self.counter, cry_f('{n} + 3'))
+        self.returns_f('{n} + 2')
+
+
+class MIRGhostTest(unittest.TestCase):
+    def test_mir_ghost(self):
+        connect(reset_server=True)
+        if __name__ == "__main__": view(LogResults())
+        json_name = str(Path('tests', 'saw', 'test-files', 'mir_ghost.linked-mir.json'))
+        mod = mir_load_module(json_name)
+
+        counter = create_ghost_variable('ctr');
+        next_ov = mir_assume(mod, 'mir_ghost::next', NextContract(counter))
+        example_result = mir_verify(mod, 'mir_ghost::example', ExampleContract(counter), lemmas=[next_ov])
+        self.assertIs(example_result.is_success(), True)
+
+
+if __name__ == "__main__":
+    unittest.main()

saw-remote-api/python/tests/saw/test-files/mir_ghost.linked-mir.json

@@ -26,7 +26,7 @@ import qualified Data.Map as Map
 import qualified Cryptol.Parser.AST as P
 import Cryptol.Utils.Ident (mkIdent)
 import qualified Lang.Crucible.JVM as CJ
-import SAWScript.Crucible.Common.MethodSpec as MS (SetupValue(..))
+import qualified SAWScript.Crucible.Common.MethodSpec as MS
 import SAWScript.Crucible.JVM.Builtins
     ( jvm_alloc_array,
       jvm_alloc_object,
@@ -35,6 +35,7 @@ import SAWScript.Crucible.JVM.Builtins
       jvm_static_field_is,
       jvm_execute_func,
       jvm_fresh_var,
+      jvm_ghost_value,
       jvm_postcond,
       jvm_precond,
       jvm_return )
@@ -56,10 +57,11 @@ import SAWServer
 import SAWServer.Data.Contract
     ( PointsTo(PointsTo),
       PointsToBitfield,
+      GhostValue(GhostValue),
       Allocated(Allocated),
       ContractVar(ContractVar),
-      Contract(preVars, preConds, preAllocated, prePointsTos, prePointsToBitfields,
-               argumentVals, postVars, postConds, postAllocated, postPointsTos, postPointsToBitfields,
+      Contract(preVars, preConds, preAllocated, preGhostValues, prePointsTos, prePointsToBitfields,
+               argumentVals, postVars, postConds, postAllocated, postGhostValues, postPointsTos, postPointsToBitfields,
                returnVal) )
 import SAWServer.Data.SetupValue ()
 import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCExp)
@@ -82,28 +84,29 @@ instance Doc.DescribedMethod StartJVMSetupParams OK where
     ]
   resultFieldDescription = []
 
-newtype ServerSetupVal = Val (SetupValue CJ.JVM)
+newtype ServerSetupVal = Val (MS.SetupValue CJ.JVM)
 
 compileJVMContract ::
   (FilePath -> IO ByteString) ->
   BuiltinContext ->
+  Map ServerName MS.GhostGlobal ->
   CryptolEnv ->
   Contract JavaType (P.Expr P.PName) ->
   JVMSetupM ()
-compileJVMContract fileReader bic cenv0 c =
+compileJVMContract fileReader bic ghostEnv cenv0 c =
   do allocsPre <- mapM setupAlloc (preAllocated c)
      (envPre, cenvPre) <- setupState allocsPre (Map.empty, cenv0) (preVars c)
      mapM_ (\p -> getTypedTerm cenvPre p >>= jvm_precond) (preConds c)
      mapM_ (setupPointsTo (envPre, cenvPre)) (prePointsTos c)
      mapM_ setupPointsToBitfields (prePointsToBitfields c)
-     --mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c)
+     mapM_ (setupGhostValue ghostEnv cenvPre) (preGhostValues c)
      traverse (getSetupVal (envPre, cenvPre)) (argumentVals c) >>= jvm_execute_func
      allocsPost <- mapM setupAlloc (postAllocated c)
      (envPost, cenvPost) <- setupState (allocsPre ++ allocsPost) (envPre, cenvPre) (postVars c)
      mapM_ (\p -> getTypedTerm cenvPost p >>= jvm_postcond) (postConds c)
      mapM_ (setupPointsTo (envPost, cenvPost)) (postPointsTos c)
      mapM_ setupPointsToBitfields (postPointsToBitfields c)
-     --mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c)
+     mapM_ (setupGhostValue ghostEnv cenvPost) (postGhostValues c)
      case returnVal c of
        Just v -> getSetupVal (envPost, cenvPost) v >>= jvm_return
        Nothing -> return ()
@@ -149,7 +152,10 @@ compileJVMContract fileReader bic cenv0 c =
     setupPointsToBitfields _ =
       JVMSetupM $ fail "Points-to-bitfield not supported in JVM API."
 
-    --setupGhostValue _ _ _ = fail "Ghost values not supported yet in JVM API."
+    setupGhostValue genv cenv (GhostValue serverName e) =
+      do g <- resolve genv serverName
+         t <- getTypedTerm cenv e
+         jvm_ghost_value g t
 
     resolve :: Map ServerName a -> ServerName -> JVMSetupM a
     resolve env name =