From bbeff5faacc19b4ca2c1a6ff8c908e13343c29a4 Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Sat, 19 Aug 2023 16:50:53 -0400 Subject: [PATCH 1/2] Mir.Intrinsics: Don't pass SimState when SymGlobalState/IntrinsicTypes will suffice This makes it possible to call into the `crucible-mir` memory model without needing access to a full-blown `SimState`, which is sometimes not available in SAW contexts. Fixes #1105. --- crucible-mir/src/Mir/Intrinsics.hs | 160 +++++++++++++++-------------- 1 file changed, 84 insertions(+), 76 deletions(-) diff --git a/crucible-mir/src/Mir/Intrinsics.hs b/crucible-mir/src/Mir/Intrinsics.hs index 5cbaea065..4b40a11bb 100644 --- a/crucible-mir/src/Mir/Intrinsics.hs +++ b/crucible-mir/src/Mir/Intrinsics.hs @@ -1124,38 +1124,35 @@ newConstMirRef sym tpr v = MirReferenceMux $ toFancyMuxTree sym $ MirReference (Const_RefRoot tpr v) Empty_RefPath readRefRoot :: (IsSymBackend sym bak) => - SimState p sym ext rtp f a -> bak -> + SymGlobalState sym -> MirReferenceRoot sym tp -> MuxLeafT sym IO (RegValue sym tp) -readRefRoot s bak (RefCell_RefRoot rc) = - leafReadPartExpr bak (lookupRef rc (s ^. stateTree . actFrame . gpGlobals)) readBeforeWriteMsg -readRefRoot s _bak (GlobalVar_RefRoot gv) = - case lookupGlobal gv (s ^. stateTree . actFrame . gpGlobals) of +readRefRoot bak gs (RefCell_RefRoot rc) = + leafReadPartExpr bak (lookupRef rc gs) readBeforeWriteMsg +readRefRoot _bak gs (GlobalVar_RefRoot gv) = + case lookupGlobal gv gs of Just x -> return x Nothing -> leafAbort readBeforeWriteMsg readRefRoot _ _ (Const_RefRoot _ v) = return v -writeRefRoot :: forall p sym bak ext rtp f a tp. +writeRefRoot :: forall sym bak tp. (IsSymBackend sym bak) => - SimState p sym ext rtp f a -> bak -> + SymGlobalState sym -> + IntrinsicTypes sym -> MirReferenceRoot sym tp -> RegValue sym tp -> - MuxLeafT sym IO (SimState p sym ext rtp f a) -writeRefRoot s bak (RefCell_RefRoot rc) v = do + MuxLeafT sym IO (SymGlobalState sym) +writeRefRoot bak gs iTypes (RefCell_RefRoot rc) v = do let sym = backendGetSym bak - let iTypes = ctxIntrinsicTypes $ s^.stateContext - let gs = s ^. stateTree . actFrame . gpGlobals let tpr = refType rc let f p a b = liftIO $ muxRegForType sym iTypes tpr p a b let oldv = lookupRef rc gs newv <- leafUpdatePartExpr bak f v oldv - return $ s & stateTree . actFrame . gpGlobals %~ updateRef rc newv -writeRefRoot s bak (GlobalVar_RefRoot gv) v = do + return $ updateRef rc newv gs +writeRefRoot bak gs iTypes (GlobalVar_RefRoot gv) v = do let sym = backendGetSym bak - let iTypes = ctxIntrinsicTypes $ s^.stateContext - let gs = s ^. stateTree . actFrame . gpGlobals let tpr = globalType gv p <- leafPredicate newv <- case lookupGlobal gv gs of @@ -1165,71 +1162,71 @@ writeRefRoot s bak (GlobalVar_RefRoot gv) v = do Nothing -> leafAbort $ ReadBeforeWriteSimError $ "attempted conditional write to uninitialized global " ++ show gv ++ " of type " ++ show tpr - return $ s & stateTree . actFrame . gpGlobals %~ insertGlobal gv newv -writeRefRoot _s _bak (Const_RefRoot tpr _) _ = + return $ insertGlobal gv newv gs +writeRefRoot _bak _gs _iTypes (Const_RefRoot tpr _) _ = leafAbort $ GenericSimError $ "Cannot write to Const_RefRoot (of type " ++ show tpr ++ ")" dropRefRoot :: (IsSymBackend sym bak) => - SimState p sym ext rtp f a -> bak -> + SymGlobalState sym -> MirReferenceRoot sym tp -> - MuxLeafT sym IO (SimState p sym ext rtp f a) -dropRefRoot s bak (RefCell_RefRoot rc) = do - let gs = s ^. stateTree . actFrame . gpGlobals + MuxLeafT sym IO (SymGlobalState sym) +dropRefRoot bak gs (RefCell_RefRoot rc) = do let oldv = lookupRef rc gs newv <- leafClearPartExpr bak oldv - return $ s & stateTree . actFrame . gpGlobals %~ updateRef rc newv -dropRefRoot _ _bak (GlobalVar_RefRoot gv) = + return $ updateRef rc newv gs +dropRefRoot _bak _gs (GlobalVar_RefRoot gv) = leafAbort $ GenericSimError $ "Cannot drop global variable " ++ show gv -dropRefRoot _ _bak (Const_RefRoot tpr _) = +dropRefRoot _bak _gs (Const_RefRoot tpr _) = leafAbort $ GenericSimError $ "Cannot drop Const_RefRoot (of type " ++ show tpr ++ ")" readMirRefLeaf :: (IsSymBackend sym bak) => - SimState p sym ext rtp f a -> bak -> + SymGlobalState sym -> + IntrinsicTypes sym -> MirReference sym tp -> MuxLeafT sym IO (RegValue sym tp) -readMirRefLeaf s bak (MirReference r path) = do - let iTypes = ctxIntrinsicTypes $ s^.stateContext - v <- readRefRoot s bak r +readMirRefLeaf bak gs iTypes (MirReference r path) = do + v <- readRefRoot bak gs r v' <- readRefPath bak iTypes v path return v' -readMirRefLeaf _ _ (MirReference_Integer _ _) = +readMirRefLeaf _ _ _ (MirReference_Integer _ _) = leafAbort $ GenericSimError $ "attempted to dereference the result of an integer-to-pointer cast" writeMirRefLeaf :: (IsSymBackend sym bak) => - SimState p sym ext rtp f a -> bak -> + SymGlobalState sym -> + IntrinsicTypes sym -> MirReference sym tp -> RegValue sym tp -> - MuxLeafT sym IO (SimState p sym ext rtp f a) -writeMirRefLeaf s bak (MirReference root Empty_RefPath) val = writeRefRoot s bak root val -writeMirRefLeaf s bak (MirReference root path) val = do - let iTypes = ctxIntrinsicTypes $ s^.stateContext - x <- readRefRoot s bak root + MuxLeafT sym IO (SymGlobalState sym) +writeMirRefLeaf bak gs iTypes (MirReference root Empty_RefPath) val = + writeRefRoot bak gs iTypes root val +writeMirRefLeaf bak gs iTypes (MirReference root path) val = do + x <- readRefRoot bak gs root x' <- writeRefPath bak iTypes x path val - writeRefRoot s bak root x' -writeMirRefLeaf _ _bak (MirReference_Integer _ _) _ = + writeRefRoot bak gs iTypes root x' +writeMirRefLeaf _ _bak _iTypes (MirReference_Integer _ _) _ = leafAbort $ GenericSimError $ "attempted to write to the result of an integer-to-pointer cast" dropMirRefLeaf :: (IsSymBackend sym bak) => - SimState p sym ext rtp f a -> bak -> + SymGlobalState sym -> MirReference sym tp -> - MuxLeafT sym IO (SimState p sym ext rtp f a) -dropMirRefLeaf s bak (MirReference root Empty_RefPath) = dropRefRoot s bak root -dropMirRefLeaf _ _bak (MirReference _ _) = + MuxLeafT sym IO (SymGlobalState sym) +dropMirRefLeaf bak gs (MirReference root Empty_RefPath) = dropRefRoot bak gs root +dropMirRefLeaf _bak _gs (MirReference _ _) = leafAbort $ GenericSimError $ "attempted to drop an interior reference (non-empty ref path)" -dropMirRefLeaf _ _bak (MirReference_Integer _ _) = +dropMirRefLeaf _bak _gs (MirReference_Integer _ _) = leafAbort $ GenericSimError $ "attempted to drop the result of an integer-to-pointer cast" @@ -1611,13 +1608,14 @@ mirRef_peelIndexIO _sym _ _ = do mirRef_indexAndLenLeaf :: (IsSymBackend sym bak) => bak -> - SimState p sym ext rtp f a -> + SymGlobalState sym -> + IntrinsicTypes sym -> MirReference sym tp -> MuxLeafT sym IO (RegValue sym UsizeType, RegValue sym UsizeType) -mirRef_indexAndLenLeaf bak s (MirReference root (Index_RefPath _tpr' path idx)) = do +mirRef_indexAndLenLeaf bak gs iTypes (MirReference root (Index_RefPath _tpr' path idx)) = do let sym = backendGetSym bak let parent = MirReference root path - parentVec <- readMirRefLeaf s bak parent + parentVec <- readMirRefLeaf bak gs iTypes parent lenInt <- case parentVec of MirVector_Vector v -> return $ V.length v MirVector_PartialVector pv -> return $ V.length pv @@ -1625,12 +1623,12 @@ mirRef_indexAndLenLeaf bak s (MirReference root (Index_RefPath _tpr' path idx)) "can't compute allocation length for MirVector_Array, which is unbounded" len <- liftIO $ bvLit sym knownNat $ BV.mkBV knownNat $ fromIntegral lenInt return (idx, len) -mirRef_indexAndLenLeaf bak _ (MirReference _ _) = do +mirRef_indexAndLenLeaf bak _ _ (MirReference _ _) = do let sym = backendGetSym bak idx <- liftIO $ bvLit sym knownNat $ BV.mkBV knownNat 0 len <- liftIO $ bvLit sym knownNat $ BV.mkBV knownNat 1 return (idx, len) -mirRef_indexAndLenLeaf bak _ (MirReference_Integer _ _) = do +mirRef_indexAndLenLeaf bak _ _ (MirReference_Integer _ _) = do let sym = backendGetSym bak -- No offset of `MirReference_Integer` is dereferenceable, so `len` is -- zero. @@ -1640,13 +1638,14 @@ mirRef_indexAndLenLeaf bak _ (MirReference_Integer _ _) = do mirRef_indexAndLenIO :: (IsSymBackend sym bak) => bak -> - SimState p sym ext rtp f a -> + SymGlobalState sym -> + IntrinsicTypes sym -> MirReferenceMux sym tp -> IO (PartExpr (Pred sym) (RegValue sym UsizeType, RegValue sym UsizeType)) -mirRef_indexAndLenIO bak s (MirReferenceMux ref) = do +mirRef_indexAndLenIO bak gs iTypes (MirReferenceMux ref) = do let sym = backendGetSym bak readPartialFancyMuxTree bak - (mirRef_indexAndLenLeaf bak s) + (mirRef_indexAndLenLeaf bak gs iTypes) (\c (tIdx, tLen) (eIdx, eLen) -> do idx <- baseTypeIte sym c tIdx eIdx len <- baseTypeIte sym c tLen eLen @@ -1661,7 +1660,9 @@ mirRef_indexAndLenSim :: mirRef_indexAndLenSim ref = do ovrWithBackend $ \bak -> do s <- get - liftIO $ mirRef_indexAndLenIO bak s ref + let gs = s^.stateTree.actFrame.gpGlobals + let iTypes = ctxIntrinsicTypes $ s^.stateContext + liftIO $ mirRef_indexAndLenIO bak gs iTypes ref execMirStmt :: forall p sym. IsSymInterface sym => EvalStmtFunc p sym MIR @@ -1685,11 +1686,11 @@ execMirStmt stmt s = withBackend ctx $ \bak -> return (mkRef r, s) MirReadRef tpr (regValue -> MirReferenceMux ref) -> - readOnly s $ readFancyMuxTree' bak (readMirRefLeaf s bak) (mux tpr) ref + readOnly s $ readFancyMuxTree' bak (readMirRefLeaf bak gs iTypes) (mux tpr) ref MirWriteRef (regValue -> MirReferenceMux ref) (regValue -> x) -> - writeOnly $ foldFancyMuxTree bak (\s' ref' -> writeMirRefLeaf s' bak ref' x) s ref + writeOnly s $ foldFancyMuxTree bak (\gs' ref' -> writeMirRefLeaf bak gs' iTypes ref' x) gs ref MirDropRef (regValue -> MirReferenceMux ref) -> - writeOnly $ foldFancyMuxTree bak (\s' ref' -> dropMirRefLeaf s' bak ref') s ref + writeOnly s $ foldFancyMuxTree bak (\gs' ref' -> dropMirRefLeaf bak gs' ref') gs ref MirSubanyRef tp (regValue -> ref) -> readOnly s $ modifyRefMux bak (subanyMirRefLeaf tp) ref MirSubfieldRef ctx0 (regValue -> ref) idx -> @@ -1770,6 +1771,7 @@ execMirStmt stmt s = withBackend ctx $ \bak -> let pv' = V.generate (fromInteger newLen) getter return (MirVector_PartialVector pv', s) where + gs = s^.stateTree.actFrame.gpGlobals ctx = s^.stateContext iTypes = ctxIntrinsicTypes ctx sym = ctx^.ctxSymInterface @@ -1786,9 +1788,14 @@ execMirStmt stmt s = withBackend ctx $ \bak -> IO (b, SimState p sym ext rtp f a) readOnly s' act = act >>= \x -> return (x, s') - writeOnly :: IO (SimState p sym ext rtp f a) -> + writeOnly :: + SimState p sym ext rtp f a -> + IO (SymGlobalState sym) -> IO ((), SimState p sym ext rtp f a) - writeOnly act = act >>= \s' -> return ((), s') + writeOnly s0 act = do + gs' <- act + let s1 = s0 & stateTree.actFrame.gpGlobals .~ gs' + return ((), s1) modifyRefMux :: IsSymBackend sym bak => bak -> @@ -1824,18 +1831,16 @@ readRefMuxSim tpr' f (MirReferenceMux ref) = let iTypes = ctxIntrinsicTypes ctx liftIO $ readFancyMuxTree' bak f (muxRegForType sym iTypes tpr') ref -readRefMuxIO :: IsSymInterface sym => - sym -> - SimState p sym ext rtp f a -> +readRefMuxIO :: + IsSymBackend sym bak => + bak -> + IntrinsicTypes sym -> TypeRepr tp' -> (MirReference sym tp -> MuxLeafT sym IO (RegValue sym tp')) -> MirReferenceMux sym tp -> IO (RegValue sym tp') -readRefMuxIO sym s tpr' f (MirReferenceMux ref) = - let ctx = s ^. stateContext - iTypes = ctxIntrinsicTypes ctx - in withBackend ctx $ \bak -> - readFancyMuxTree' bak f (muxRegForType sym iTypes tpr') ref +readRefMuxIO bak iTypes tpr' f (MirReferenceMux ref) = + readFancyMuxTree' bak f (muxRegForType (backendGetSym bak) iTypes tpr') ref modifyRefMuxSim :: IsSymInterface sym => (MirReference sym tp -> MuxLeafT sym IO (MirReference sym tp')) -> @@ -1852,21 +1857,22 @@ readMirRefSim :: IsSymInterface sym => TypeRepr tp -> MirReferenceMux sym tp -> OverrideSim m sym MIR rtp args ret (RegValue sym tp) readMirRefSim tpr ref = - do sym <- getSymInterface - s <- get - liftIO $ readMirRefIO sym s tpr ref + ovrWithBackend $ \bak -> + do s <- get + let gs = s^.stateTree.actFrame.gpGlobals + let iTypes = ctxIntrinsicTypes $ s^.stateContext + liftIO $ readMirRefIO bak gs iTypes tpr ref readMirRefIO :: - IsSymInterface sym => - sym -> - SimState p sym ext rtp f a -> + IsSymBackend sym bak => + bak -> + SymGlobalState sym -> + IntrinsicTypes sym -> TypeRepr tp -> MirReferenceMux sym tp -> IO (RegValue sym tp) -readMirRefIO sym s tpr ref = - let ctx = s ^. stateContext - in withBackend ctx $ \bak -> - readRefMuxIO sym s tpr (readMirRefLeaf s bak) ref +readMirRefIO bak gs iTypes tpr ref = + readRefMuxIO bak iTypes tpr (readMirRefLeaf bak gs iTypes) ref writeMirRefSim :: IsSymInterface sym => @@ -1876,9 +1882,11 @@ writeMirRefSim :: OverrideSim m sym MIR rtp args ret () writeMirRefSim _tpr (MirReferenceMux ref) x = do s <- get + let gs0 = s^.stateTree.actFrame.gpGlobals + let iTypes = ctxIntrinsicTypes $ s^.stateContext ovrWithBackend $ \bak -> do - s' <- liftIO $ foldFancyMuxTree bak (\s' ref' -> writeMirRefLeaf s' bak ref' x) s ref - put s' + gs1 <- liftIO $ foldFancyMuxTree bak (\gs' ref' -> writeMirRefLeaf bak gs' iTypes ref' x) gs0 ref + put $ s & stateTree.actFrame.gpGlobals .~ gs1 subindexMirRefSim :: IsSymInterface sym => TypeRepr tp -> MirReferenceMux sym (MirVectorType tp) -> RegValue sym UsizeType -> From 75836c9b3ef86406e2eeb77bdc96b3d2752dad7e Mon Sep 17 00:00:00 2001 From: Ryan Scott Date: Tue, 22 Aug 2023 15:17:26 -0400 Subject: [PATCH 2/2] Mir.Intrinsics: Provide more IO wrappers around memory model functionality MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Much of the memory model–related functionality in `Mir.Intrinsics` is defined in terms of `FancyMuxTree`s, which are somewhat clunky to manipulate outside of `crucible-mir`. `Mir.Intrinsics` does provide some wrapper functions to encapsulate the `FancyMuxTree` manipulation, but these typically live in the `OverrideSim` monad, which is more specific than we want for SAW's needs. This patch adds `IO` wrappers alongside the `OverrideSim` wrappers to make it more straightforward to use them in SAW. --- crucible-mir/src/Mir/Intrinsics.hs | 93 +++++++++++++++++++++++------- 1 file changed, 72 insertions(+), 21 deletions(-) diff --git a/crucible-mir/src/Mir/Intrinsics.hs b/crucible-mir/src/Mir/Intrinsics.hs index 4b40a11bb..962de25bd 100644 --- a/crucible-mir/src/Mir/Intrinsics.hs +++ b/crucible-mir/src/Mir/Intrinsics.hs @@ -1373,6 +1373,19 @@ mirRef_eqIO bak (MirReferenceMux r1) (MirReferenceMux r2) = let sym = backendGetSym bak in zipFancyMuxTrees' bak (mirRef_eqLeaf sym) (itePred sym) r1 r2 +mirVector_uninitIO :: + IsSymBackend sym bak => + bak -> + RegValue sym UsizeType -> + IO (MirVector sym tp) +mirVector_uninitIO bak lenSym = do + len <- case asBV lenSym of + Just x -> return (BV.asUnsigned x) + Nothing -> addFailedAssertion bak $ Unsupported callStack $ + "Attempted to allocate vector of symbolic length" + let pv = V.replicate (fromInteger len) Unassigned + return (MirVector_PartialVector pv) + -- | An ordinary `MirReferencePath sym tp tp''` is represented "inside-out": to -- turn `tp` into `tp''`, we first use a subsidiary `MirReferencePath` to turn @@ -1669,9 +1682,8 @@ execMirStmt :: forall p sym. IsSymInterface sym => EvalStmtFunc p sym MIR execMirStmt stmt s = withBackend ctx $ \bak -> case stmt of MirNewRef tp -> - do r <- freshRefCell halloc tp - let r' = MirReference (RefCell_RefRoot r) Empty_RefPath - return (mkRef r', s) + do r <- newMirRefIO sym halloc tp + return (r, s) MirIntegerToRef tp (regValue -> i) -> do let r' = MirReference_Integer tp i @@ -1748,12 +1760,8 @@ execMirStmt stmt s = withBackend ctx $ \bak -> return (val, s) MirVector_Uninit _tp (regValue -> lenSym) -> do - len <- case asBV lenSym of - Just x -> return (BV.asUnsigned x) - Nothing -> addFailedAssertion bak $ Unsupported callStack $ - "Attempted to allocate vector of symbolic length" - let pv = V.replicate (fromInteger len) Unassigned - return (MirVector_PartialVector pv, s) + pv <- mirVector_uninitIO bak lenSym + return (pv, s) MirVector_FromVector _tp (regValue -> v) -> return (MirVector_Vector v, s) MirVector_FromArray _tp (regValue -> a) -> @@ -1801,11 +1809,10 @@ execMirStmt stmt s = withBackend ctx $ \bak -> bak -> (MirReference sym tp -> MuxLeafT sym IO (MirReference sym tp')) -> MirReferenceMux sym tp -> IO (MirReferenceMux sym tp') - modifyRefMux bak f (MirReferenceMux ref) = - MirReferenceMux <$> mapFancyMuxTree bak (muxRef' sym iTypes) f ref + modifyRefMux bak = modifyRefMuxIO bak iTypes --- MirReferenceType manipulation within the OverrideSim monad. These are +-- MirReferenceType manipulation within the OverrideSim and IO monads. These are -- useful for implementing overrides that work with MirReferences. newMirRefSim :: IsSymInterface sym => @@ -1815,7 +1822,16 @@ newMirRefSim tpr = do sym <- getSymInterface s <- get let halloc = simHandleAllocator $ s ^. stateContext - rc <- liftIO $ freshRefCell halloc tpr + liftIO $ newMirRefIO sym halloc tpr + +newMirRefIO :: + IsSymInterface sym => + sym -> + HandleAllocator -> + TypeRepr tp -> + IO (MirReferenceMux sym tp) +newMirRefIO sym halloc tpr = do + rc <- freshRefCell halloc tpr let ref = MirReference (RefCell_RefRoot rc) Empty_RefPath return $ MirReferenceMux $ toFancyMuxTree sym ref @@ -1824,12 +1840,11 @@ readRefMuxSim :: IsSymInterface sym => (MirReference sym tp -> MuxLeafT sym IO (RegValue sym tp')) -> MirReferenceMux sym tp -> OverrideSim m sym MIR rtp args ret (RegValue sym tp') -readRefMuxSim tpr' f (MirReferenceMux ref) = +readRefMuxSim tpr' f ref = ovrWithBackend $ \bak -> do - let sym = backendGetSym bak ctx <- getContext let iTypes = ctxIntrinsicTypes ctx - liftIO $ readFancyMuxTree' bak f (muxRegForType sym iTypes tpr') ref + liftIO $ readRefMuxIO bak iTypes tpr' f ref readRefMuxIO :: IsSymBackend sym bak => @@ -1846,12 +1861,22 @@ modifyRefMuxSim :: IsSymInterface sym => (MirReference sym tp -> MuxLeafT sym IO (MirReference sym tp')) -> MirReferenceMux sym tp -> OverrideSim m sym MIR rtp args ret (MirReferenceMux sym tp') -modifyRefMuxSim f (MirReferenceMux ref) = +modifyRefMuxSim f ref = ovrWithBackend $ \bak -> do - let sym = backendGetSym bak ctx <- getContext let iTypes = ctxIntrinsicTypes ctx - liftIO $ MirReferenceMux <$> mapFancyMuxTree bak (muxRef' sym iTypes) f ref + liftIO $ modifyRefMuxIO bak iTypes f ref + +modifyRefMuxIO :: + IsSymBackend sym bak => + bak -> + IntrinsicTypes sym -> + (MirReference sym tp -> MuxLeafT sym IO (MirReference sym tp')) -> + MirReferenceMux sym tp -> + IO (MirReferenceMux sym tp') +modifyRefMuxIO bak iTypes f (MirReferenceMux ref) = do + let sym = backendGetSym bak + MirReferenceMux <$> mapFancyMuxTree bak (muxRef' sym iTypes) f ref readMirRefSim :: IsSymInterface sym => TypeRepr tp -> MirReferenceMux sym tp -> @@ -1880,20 +1905,46 @@ writeMirRefSim :: MirReferenceMux sym tp -> RegValue sym tp -> OverrideSim m sym MIR rtp args ret () -writeMirRefSim _tpr (MirReferenceMux ref) x = do +writeMirRefSim _tpr ref x = do s <- get let gs0 = s^.stateTree.actFrame.gpGlobals let iTypes = ctxIntrinsicTypes $ s^.stateContext ovrWithBackend $ \bak -> do - gs1 <- liftIO $ foldFancyMuxTree bak (\gs' ref' -> writeMirRefLeaf bak gs' iTypes ref' x) gs0 ref + gs1 <- liftIO $ writeMirRefIO bak gs0 iTypes ref x put $ s & stateTree.actFrame.gpGlobals .~ gs1 +writeMirRefIO :: + IsSymBackend sym bak => + bak -> + SymGlobalState sym -> + IntrinsicTypes sym -> + MirReferenceMux sym tp -> + RegValue sym tp -> + IO (SymGlobalState sym) +writeMirRefIO bak gs iTypes (MirReferenceMux ref) x = + foldFancyMuxTree + bak + (\gs' ref' -> writeMirRefLeaf bak gs' iTypes ref' x) + gs + ref + subindexMirRefSim :: IsSymInterface sym => TypeRepr tp -> MirReferenceMux sym (MirVectorType tp) -> RegValue sym UsizeType -> OverrideSim m sym MIR rtp args ret (MirReferenceMux sym tp) subindexMirRefSim tpr ref idx = do modifyRefMuxSim (\ref' -> subindexMirRefLeaf tpr ref' idx) ref +subindexMirRefIO :: + IsSymBackend sym bak => + bak -> + IntrinsicTypes sym -> + TypeRepr tp -> + MirReferenceMux sym (MirVectorType tp) -> + RegValue sym UsizeType -> + IO (MirReferenceMux sym tp) +subindexMirRefIO bak iTypes tpr ref x = + modifyRefMuxIO bak iTypes (\ref' -> subindexMirRefLeaf tpr ref' x) ref + mirRef_offsetSim :: IsSymInterface sym => TypeRepr tp -> MirReferenceMux sym tp -> RegValue sym IsizeType -> OverrideSim m sym MIR rtp args ret (MirReferenceMux sym tp)