From 3fa027c696c27edcb063f905185b6305d90b792a Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Mon, 13 Nov 2023 10:02:56 -0500 Subject: [PATCH] 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 https://github.com/GaloisInc/crucible/issues/1128 as a reminder to generalize `jvmSimContext` upstream. --- .../test_mir_ghost_symbolic_branch/Makefile | 13 ++++++++++ .../test.linked-mir.json | 1 + .../test_mir_ghost_symbolic_branch/test.rs | 10 ++++++++ .../test_mir_ghost_symbolic_branch/test.saw | 24 +++++++++++++++++++ .../test_mir_ghost_symbolic_branch/test.sh | 3 +++ src/SAWScript/Crucible/JVM/Builtins.hs | 8 ++++++- src/SAWScript/Crucible/JVM/MethodSpecIR.hs | 16 +++++++++++++ src/SAWScript/Crucible/LLVM/MethodSpecIR.hs | 4 +++- src/SAWScript/Crucible/MIR/Builtins.hs | 2 +- src/SAWScript/Crucible/MIR/MethodSpecIR.hs | 20 ++++++++++++++++ src/SAWScript/Crucible/MIR/Override.hs | 8 +++---- .../Crucible/MIR/ResolveSetupValue.hs | 7 +++--- 12 files changed, 106 insertions(+), 10 deletions(-) create mode 100644 intTests/test_mir_ghost_symbolic_branch/Makefile create mode 100644 intTests/test_mir_ghost_symbolic_branch/test.linked-mir.json create mode 100644 intTests/test_mir_ghost_symbolic_branch/test.rs create mode 100644 intTests/test_mir_ghost_symbolic_branch/test.saw create mode 100755 intTests/test_mir_ghost_symbolic_branch/test.sh diff --git a/intTests/test_mir_ghost_symbolic_branch/Makefile b/intTests/test_mir_ghost_symbolic_branch/Makefile new file mode 100644 index 0000000000..bc6297ae15 --- /dev/null +++ b/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 diff --git a/intTests/test_mir_ghost_symbolic_branch/test.linked-mir.json b/intTests/test_mir_ghost_symbolic_branch/test.linked-mir.json new file mode 100644 index 0000000000..deea148368 --- /dev/null +++ b/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"]} \ No newline at end of file diff --git a/intTests/test_mir_ghost_symbolic_branch/test.rs b/intTests/test_mir_ghost_symbolic_branch/test.rs new file mode 100644 index 0000000000..6a3d06e7fd --- /dev/null +++ b/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) + } +} diff --git a/intTests/test_mir_ghost_symbolic_branch/test.saw b/intTests/test_mir_ghost_symbolic_branch/test.saw new file mode 100644 index 0000000000..e35b0652cc --- /dev/null +++ b/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; diff --git a/intTests/test_mir_ghost_symbolic_branch/test.sh b/intTests/test_mir_ghost_symbolic_branch/test.sh new file mode 100755 index 0000000000..2315cc233c --- /dev/null +++ b/intTests/test_mir_ghost_symbolic_branch/test.sh @@ -0,0 +1,3 @@ +set -e + +$SAW test.saw diff --git a/src/SAWScript/Crucible/JVM/Builtins.hs b/src/SAWScript/Crucible/JVM/Builtins.hs index c4e9b3ae80..f2a55d93b4 100644 --- a/src/SAWScript/Crucible/JVM/Builtins.hs +++ b/src/SAWScript/Crucible/JVM/Builtins.hs @@ -673,7 +673,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 = diff --git a/src/SAWScript/Crucible/JVM/MethodSpecIR.hs b/src/SAWScript/Crucible/JVM/MethodSpecIR.hs index bc9e40a9f6..1e3cd413f8 100644 --- a/src/SAWScript/Crucible/JVM/MethodSpecIR.hs +++ b/src/SAWScript/Crucible/JVM/MethodSpecIR.hs @@ -53,9 +53,13 @@ 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 @@ -63,6 +67,8 @@ 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 -------------------------------------------------------------------------------- diff --git a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs b/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs index d64181171e..f627d36508 100644 --- a/src/SAWScript/Crucible/LLVM/MethodSpecIR.hs +++ b/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 diff --git a/src/SAWScript/Crucible/MIR/Builtins.hs b/src/SAWScript/Crucible/MIR/Builtins.hs index fdead987dd..c81a39546d 100644 --- a/src/SAWScript/Crucible/MIR/Builtins.hs +++ b/src/SAWScript/Crucible/MIR/Builtins.hs @@ -1260,7 +1260,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 diff --git a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs b/src/SAWScript/Crucible/MIR/MethodSpecIR.hs index b66b3cc02a..c52292ea43 100644 --- a/src/SAWScript/Crucible/MIR/MethodSpecIR.hs +++ b/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 diff --git a/src/SAWScript/Crucible/MIR/Override.hs b/src/SAWScript/Crucible/MIR/Override.hs index 11826af349..0cee024cc5 100644 --- a/src/SAWScript/Crucible/MIR/Override.hs +++ b/src/SAWScript/Crucible/MIR/Override.hs @@ -980,10 +980,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. @@ -1173,6 +1175,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 @@ -1181,9 +1184,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 diff --git a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs b/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs index 1426e62f02..4727199da3 100644 --- a/src/SAWScript/Crucible/MIR/ResolveSetupValue.hs +++ b/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