Draft: Support ghost values in all language backends

Still TODO:

* Once the MIR backend supports overrides, the MIR backend needs to call the
  `executeGhost` function from `executeCond`, similarly to how the LLVM and
  JVM backends do currently.
* Add a MIR test case demonstrating that it works.

Fixes #1929.

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

@@ -649,8 +649,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

@@ -3144,14 +3144,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
 

saw-remote-api/CHANGELOG.md

@@ -25,6 +25,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
 

saw-remote-api/python/CHANGELOG.md

@@ -29,6 +29,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/src/SAWServer/JVMCrucibleSetup.hs

@@ -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/src/SAWServer/JVMVerify.hs

@@ -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/src/SAWServer/MIRCrucibleSetup.hs

@@ -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/MIRVerify.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_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

src/SAWScript/Builtins.hs

@@ -27,6 +27,7 @@ import Data.Functor
 import Control.Applicative
 import Data.Monoid
 #endif
+import Control.Lens (view)
 import Control.Monad.Except (MonadError(..))
 import Control.Monad.State
 import qualified Control.Exception as Ex
@@ -132,7 +133,8 @@ import SAWScript.Value (ProofScript, printOutLnTop, AIGNetwork)
 import SAWScript.SolverCache
 import SAWScript.SolverVersions
 
-import SAWScript.Crucible.Common.MethodSpec (ppTypedTermType)
+import qualified SAWScript.Crucible.Common.MethodSpec as MS
+import SAWScript.Crucible.Common.Setup.Type (addCondition, croTags)
 import SAWScript.Prover.Util(checkBooleanSchema)
 import SAWScript.Prover.SolverStats
 import qualified SAWScript.Prover.SBV as Prover
@@ -158,7 +160,7 @@ definePrim name (TypedTerm (TypedTermSchema schema) rhs) =
 definePrim _name (TypedTerm tp _) =
   fail $ unlines
     [ "Expected term with Cryptol schema type, but got"
-    , show (ppTypedTermType tp)
+    , show (MS.ppTypedTermType tp)
     ]
 
 sbvUninterpreted :: String -> Term -> TopLevel Uninterp
@@ -696,7 +698,7 @@ term_type tt =
     TypedTermSchema sch -> pure sch
     tp -> fail $ unlines
             [ "Term does not have a Cryptol type"
-            , show (ppTypedTermType tp)
+            , show (MS.ppTypedTermType tp)
             ]
 
 goal_eval :: [String] -> ProofScript ()
@@ -2474,3 +2476,18 @@ declare_ghost_state name =
   do allocator <- getHandleAlloc
      global <- liftIO (freshGlobalVar allocator (Text.pack name) knownRepr)
      return (SV.VGhostVar global)
+
+ghost_value ::
+  MS.GhostGlobal ->
+  TypedTerm ->
+  SV.CrucibleSetup ext ()
+ghost_value ghost val =
+  do loc <- SV.getW4Position "ghost_value"
+     tags <- view croTags
+     let md = MS.ConditionMetadata
+              { MS.conditionLoc = loc
+              , MS.conditionTags = tags
+              , MS.conditionType = "ghost value"
+              , MS.conditionContext = ""
+              }
+     addCondition (MS.SetupCond_Ghost md ghost val)