Make symbolic branching work with JVM/MIR ghost state

This is not entirely straightforward to do for the JVM backend, as the
`jvmSimContext` function (`crucible-jvm`'s API function for constructing a
`SimContext`) does not support adding additional intrinsic types, including the
intrinsic type needed to support SAW ghost state. For the time being, I have
simply inlined the implementation of `jvmSimContext` as needed, and I have
opened GaloisInc/crucible#1128 as a reminder to
generalize `jvmSimContext` upstream.

intTests/test_mir_ghost_symbolic_branch/Makefile

@@ -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_symbolic_branch/test.linked-mir.json

@@ -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/test.rs

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

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

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

src/SAWScript/Crucible/JVM/Builtins.hs

@@ -670,7 +670,13 @@ verifySimulate opts cc pfs mspec args assumes top_loc lemmas globals _checkSat m
      regmap <- prepareArgs (Crucible.handleArgTypes h) (map snd args)
      res <-
        do let feats = pfs
-          let simctx = CJ.jvmSimContext bak halloc stdout jc verbosity SAWCruciblePersonality
+          -- TODO: Use crucible-jvm's jvmSimContext here (instead of manually
+          -- calling mkDelayedBindings/initSimContext), once
+          -- https://github.com/GaloisInc/crucible/issues/1128 has been fixed
+          -- upstream.
+          let bindings = CJ.mkDelayedBindings jc verbosity
+          let simctx = Crucible.initSimContext bak intrinsics halloc stdout
+                         bindings CJ.jvmExtensionImpl SAWCruciblePersonality
           let simSt = Crucible.InitialState simctx globals Crucible.defaultAbortHandler (Crucible.handleReturnType h)
           let fnCall = Crucible.regValue <$> Crucible.callFnVal (Crucible.HandleFnVal h) regmap
           let overrideSim =

src/SAWScript/Crucible/JVM/MethodSpecIR.hs

@@ -53,16 +53,22 @@ module SAWScript.Crucible.JVM.MethodSpecIR
 
   , initialDefCrucibleMethodSpecIR
   , initialCrucibleSetupState
+
+  , intrinsics
   ) where
 
 import           Control.Lens
+import qualified Data.Parameterized.Map as MapF
+import           Data.Parameterized.SymbolRepr (SymbolRepr, knownSymbol)
 import qualified Prettyprinter as PPL
 
 -- what4
 import           What4.ProgramLoc (ProgramLoc)
 
 -- crucible-jvm
 import qualified Lang.Crucible.JVM as CJ
+import qualified Lang.Crucible.Simulator.Intrinsics as CS
+  (IntrinsicMuxFn(IntrinsicMuxFn))
 import qualified Lang.JVM.Codebase as CB
 
 -- jvm-parser
@@ -184,6 +190,16 @@ initialCrucibleSetupState cc (cls, method) loc =
       (J.className cls)
       method
       loc
+--------------------------------------------------------------------------------
+
+-- | The default JVM intrinsics extended with the 'MS.GhostValue' intrinsic,
+-- which powers ghost state.
+intrinsics :: MapF.MapF SymbolRepr (CS.IntrinsicMuxFn Sym)
+intrinsics =
+  MapF.insert
+    (knownSymbol :: SymbolRepr MS.GhostValue)
+    CS.IntrinsicMuxFn
+    CJ.jvmIntrinsicTypes
 
 --------------------------------------------------------------------------------
 

src/SAWScript/Crucible/LLVM/MethodSpecIR.hs

@@ -222,8 +222,10 @@ instance PPL.Pretty (LLVMPointsToValue arch) where
       MS.ppTypedTerm arr PPL.<+> PPL.pretty "[" PPL.<+> MS.ppTypedTerm sz PPL.<+> PPL.pretty "]"
 
 --------------------------------------------------------------------------------
--- ** ???
+-- ** SAW LLVM intrinsics
 
+-- | The default LLVM intrinsics extended with the 'MS.GhostValue' intrinsic,
+-- which powers ghost state.
 intrinsics :: MapF.MapF Crucible.SymbolRepr (Crucible.IntrinsicMuxFn Sym)
 intrinsics =
   MapF.insert

src/SAWScript/Crucible/MIR/Builtins.hs

@@ -1210,7 +1210,7 @@ setupCrucibleContext rm =
                             (Crucible.UseCFG cfg (Crucible.postdomInfo cfg))) $
                     Map.elems cfgMap
      let simctx0 = Crucible.initSimContext bak
-                     Mir.mirIntrinsicTypes halloc stdout
+                     intrinsics halloc stdout
                      bindings Mir.mirExtImpl
                      SAWCruciblePersonality
      let globals0 = Crucible.emptyGlobals

src/SAWScript/Crucible/MIR/MethodSpecIR.hs

@@ -17,6 +17,7 @@ module SAWScript.Crucible.MIR.MethodSpecIR
   , mccSymGlobalState
   , mccStaticInitializerMap
   , mccHandleAllocator
+  , mccIntrinsicTypes
   , mccWithBackend
   , mccSym
 
@@ -53,13 +54,20 @@ module SAWScript.Crucible.MIR.MethodSpecIR
     -- * Initial CrucibleSetupMethodSpec
   , initialDefCrucibleMethodSpecIR
   , initialCrucibleSetupState
+
+    -- * Intrinsics
+  , intrinsics
   ) where
 
 import Control.Lens (Getter, Iso', Lens', (^.), iso, to)
+import qualified Data.Parameterized.Map as MapF
+import Data.Parameterized.SymbolRepr (SymbolRepr, knownSymbol)
 import qualified Prettyprinter as PP
 
 import Lang.Crucible.FunctionHandle (HandleAllocator)
 import Lang.Crucible.Simulator (SimContext(..))
+import Lang.Crucible.Simulator.Intrinsics
+  (IntrinsicMuxFn(IntrinsicMuxFn), IntrinsicTypes)
 import Mir.Generator
 import Mir.Intrinsics
 import qualified Mir.Mir as M
@@ -73,6 +81,9 @@ import           SAWScript.Crucible.MIR.Setup.Value
 mccHandleAllocator :: Getter MIRCrucibleContext HandleAllocator
 mccHandleAllocator = mccSimContext . to simHandleAllocator
 
+mccIntrinsicTypes :: Getter MIRCrucibleContext (IntrinsicTypes Sym)
+mccIntrinsicTypes = mccSimContext . to ctxIntrinsicTypes
+
 mccWithBackend ::
   MIRCrucibleContext ->
   (forall solver. OnlineSolver solver => Backend solver -> a) ->
@@ -127,3 +138,12 @@ initialCrucibleSetupState cc fn loc =
       (cc ^. mccRustModule ^. rmCS)
       fn
       loc
+
+-- | The default MIR intrinsics extended with the 'MS.GhostValue' intrinsic,
+-- which powers ghost state.
+intrinsics :: MapF.MapF SymbolRepr (IntrinsicMuxFn Sym)
+intrinsics =
+  MapF.insert
+    (knownSymbol :: SymbolRepr MS.GhostValue)
+    IntrinsicMuxFn
+    mirIntrinsicTypes

src/SAWScript/Crucible/MIR/Override.hs

@@ -965,10 +965,12 @@ learnPointsTo opts sc cc spec prepost (MirPointsTo md reference referents) =
                  ]
      let innerShp = tyToShapeEq col referenceInnerMirTy referenceInnerTpr
      referentVal <- firstPointsToReferent referents
-     v <- liftIO $ Mir.readMirRefIO bak globals Mir.mirIntrinsicTypes
+     v <- liftIO $ Mir.readMirRefIO bak globals iTypes
        referenceInnerTpr referenceVal
      matchArg opts sc cc spec prepost md (MIRVal innerShp v)
        referenceInnerMirTy referentVal
+  where
+    iTypes = cc ^. mccIntrinsicTypes
 
 -- | Process a "mir_precond" statement from the precondition
 -- section of the CrucibleSetup block.
@@ -1158,6 +1160,7 @@ matchArg opts sc cc cs prepost md actual expectedTy expected =
   where
     colState = cc ^. mccRustModule . Mir.rmCS
     col      = colState ^. Mir.collection
+    iTypes   = cc ^. mccIntrinsicTypes
     tyenv    = MS.csAllocations cs
     nameEnv  = MS.csTypeNames cs
 
@@ -1166,9 +1169,6 @@ matchArg opts sc cc cs prepost md actual expectedTy expected =
               mkStructuralMismatch opts cc sc cs actual expected expectedTy
     notEq = notEqual prepost opts loc cc sc cs expected actual
 
-    iTypes :: Crucible.IntrinsicTypes Sym
-    iTypes = Mir.mirIntrinsicTypes
-
 -- | For each points-to statement read the memory value through the
 -- given pointer (lhs) and match the value against the given pattern
 -- (rhs).  Statements are processed in dependency order: a points-to

src/SAWScript/Crucible/MIR/ResolveSetupValue.hs

@@ -422,7 +422,7 @@ resolveSetupVal mcc env tyenv nameEnv val =
   where
     cs  = mcc ^. mccRustModule . Mir.rmCS
     col = cs ^. Mir.collection
-    iTypes = Mir.mirIntrinsicTypes
+    iTypes = mcc ^. mccIntrinsicTypes
 
     usizeBvLit :: Sym -> Int -> IO (W4.SymBV Sym Mir.SizeBits)
     usizeBvLit sym = W4.bvLit sym W4.knownNat . BV.mkBV W4.knownNat . toInteger
@@ -967,7 +967,7 @@ doAlloc cc globals (Some ma) =
   do let col = cc ^. mccRustModule ^. Mir.rmCS ^. Mir.collection
      let halloc = cc^.mccHandleAllocator
      let sym = backendGetSym bak
-     let iTypes = Mir.mirIntrinsicTypes
+     let iTypes = cc^.mccIntrinsicTypes
      Some tpr <- pure $ Mir.tyToRepr col (ma^.maMirType)
 
      -- Create an uninitialized `MirVector_PartialVector` of length 1 and
@@ -1026,8 +1026,9 @@ doPointsTo mspec cc env globals (MirPointsTo _ reference referents) =
                 , "Reference type: " ++ show referenceInnerTy
                 , "Referent type:  " ++ show (shapeType referentShp)
                 ]
-    Mir.writeMirRefIO bak globals Mir.mirIntrinsicTypes referenceVal referentVal
+    Mir.writeMirRefIO bak globals iTypes referenceVal referentVal
   where
+    iTypes = cc ^. mccIntrinsicTypes
     tyenv = MS.csAllocations mspec
     nameEnv = mspec ^. MS.csPreState . MS.csVarTypeNames