Support ghost values in all language backends

This patch:

* Factors out the machinery needed to track ghost state into
  into the `SAWScript.Crucible.Common.Override` and `SAWScript.Builtins`
  modules. Nothing about ghost state is specific to any language backend, so it
  deserves to live in a non-LLVM–specific location.
* Adds `jvm_ghost_value` and `mir_ghost_value` commands, which behave exactly
  like the LLVM backend's `llvm_ghost_value` command does, but for the JVM and
  MIR backends, respectively.
* Adds a `test_mir_ghost` test case in SAWScript and the remote API to ensure
  that everything works as expected.

Fixes #1929.

Author: RyanGlScott

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 languaage 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

@@ -640,8 +640,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
 
     goTypedTerm tt = do
         term' <- goTerm $ SAW.ttTerm tt

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

@@ -571,7 +571,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

@@ -3142,14 +3142,15 @@ with the following function:
 
 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

@@ -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

@@ -27,6 +27,8 @@
 * The API for `"struct"` `setup value`s now has a `"MIR ADT"` field. For
   MIR verification, this field is required. For LLVM and JVM verification,
   this field must be `null`, or else an error will be raised.
+* 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/test.sh

@@ -30,6 +30,8 @@
 * Add a `proclaim_f` function. This behaves like the `proclaim` function, except
   that it takes a `cry_f`-style format string as an argument. That is,
   `proclaim_f(...)` is equivalent to `proclaim(cry_f(...))`.
+* 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 =

saw-remote-api/python/tests/saw/test-files/mir_ghost.rs

@@ -9,6 +9,7 @@ module SAWServer.JVMVerify
 
 import Prelude hiding (mod)
 import Control.Lens
+import qualified Data.Map as Map
 
 import SAWScript.Crucible.JVM.Builtins
     ( jvm_unsafe_assume_spec, jvm_verify )
@@ -26,6 +27,7 @@ import SAWServer
       pushTask,
       dropTask,
       setServerVal,
+      getGhosts,
       getJVMClass,
       getJVMMethodSpecIR )
 import SAWServer.CryptolExpression (getCryptolExpr)
@@ -51,7 +53,8 @@ jvmVerifyAssume mode (VerifyParams className fun lemmaNames checkSat contract sc
             let bic = view sawBIC state
                 cenv = rwCryptol (view sawTopLevelRW state)
             fileReader <- Argo.getFileReader
-            setup <- compileJVMContract fileReader bic cenv <$> traverse getCryptolExpr contract
+            ghostEnv <- Map.fromList <$> getGhosts
+            setup <- compileJVMContract fileReader bic ghostEnv cenv <$> traverse getCryptolExpr contract
             res <- case mode of
               VerifyContract -> do
                 lemmas <- mapM getJVMMethodSpecIR lemmaNames

saw-remote-api/python/tests/saw/test_mir_ghost.py

@@ -30,6 +30,7 @@ import SAWScript.Crucible.MIR.Builtins
       mir_alloc_mut,
       mir_fresh_var,
       mir_execute_func,
+      mir_ghost_value,
       mir_load_module,
       mir_points_to,
       mir_postcond,
@@ -55,10 +56,11 @@ import SAWServer.CryptolExpression (CryptolModuleException(..), getTypedTermOfCE
 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.MIRType (JSONMIRType, mirType)
 import SAWServer.Exceptions ( notAtTopLevel )
@@ -71,24 +73,25 @@ newtype ServerSetupVal = Val (MS.SetupValue MIR)
 compileMIRContract ::
   (FilePath -> IO ByteString) ->
   BuiltinContext ->
+  Map ServerName MS.GhostGlobal ->
   CryptolEnv ->
   SAWEnv ->
   Contract JSONMIRType (P.Expr P.PName) ->
   MIRSetupM ()
-compileMIRContract fileReader bic cenv0 sawenv c =
+compileMIRContract fileReader bic ghostEnv cenv0 sawenv c =
   do allocsPre <- mapM setupAlloc (preAllocated c)
      (envPre, cenvPre) <- setupState allocsPre (Map.empty, cenv0) (preVars c)
      mapM_ (\p -> getTypedTerm cenvPre p >>= mir_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) >>= mir_execute_func
      allocsPost <- mapM setupAlloc (postAllocated c)
      (envPost, cenvPost) <- setupState (allocsPre ++ allocsPost) (envPre, cenvPre) (postVars c)
      mapM_ (\p -> getTypedTerm cenvPost p >>= mir_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 >>= mir_return
        Nothing -> return ()
@@ -133,7 +136,10 @@ compileMIRContract fileReader bic cenv0 sawenv c =
     setupPointsToBitfields _ =
       MIRSetupM $ fail "Points-to-bitfield not supported in the MIR API."
 
-    --setupGhostValue _ _ _ = fail "Ghost values not supported yet in the MIR API."
+    setupGhostValue genv cenv (GhostValue serverName e) =
+      do g <- resolve genv serverName
+         t <- getTypedTerm cenv e
+         mir_ghost_value g t
 
     resolve :: Map ServerName a -> ServerName -> MIRSetupM a
     resolve env name =

saw-remote-api/src/SAWServer/JVMCrucibleSetup.hs

@@ -9,6 +9,7 @@ module SAWServer.MIRVerify
 
 import Prelude hiding (mod)
 import Control.Lens
+import qualified Data.Map as Map
 
 import SAWScript.Crucible.MIR.Builtins
     ( mir_unsafe_assume_spec, mir_verify )
@@ -26,6 +27,7 @@ import SAWServer
       pushTask,
       dropTask,
       setServerVal,
+      getGhosts,
       getMIRModule,
       getMIRMethodSpecIR )
 import SAWServer.CryptolExpression (getCryptolExpr)
@@ -53,7 +55,8 @@ mirVerifyAssume mode (VerifyParams modName fun lemmaNames checkSat contract scri
                 cenv = rwCryptol (view sawTopLevelRW state)
                 sawenv = view sawEnv state
             fileReader <- Argo.getFileReader
-            setup <- compileMIRContract fileReader bic cenv sawenv <$>
+            ghostEnv <- Map.fromList <$> getGhosts
+            setup <- compileMIRContract fileReader bic ghostEnv cenv sawenv <$>
                      traverse getCryptolExpr contract
             res <- case mode of
               VerifyContract -> do