{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.Simulator.CallFrame
(
CrucibleBranchTarget(..)
, ppBranchTarget
, CallFrame(..)
, mkCallFrame
, mkBlockFrame
, framePostdomMap
, frameBlockMap
, frameHandle
, frameReturnType
, frameBlockID
, frameRegs
, frameStmts
, framePostdom
, frameProgramLoc
, setFrameBlock
, setFrameBreakpointPostdomInfo
, extendFrame
, updateFrame
, mergeCallFrame
, SomeHandle(..)
, SimFrame(..)
, CrucibleLang
, OverrideLang
, FrameRetType
, OverrideFrame(..)
, override
, overrideHandle
, overrideRegMap
, overrideSimFrame
, crucibleSimFrame
, fromCallFrame
, fromReturnFrame
, frameFunctionName
) where
import Control.Lens
import Data.Kind
import qualified Data.Parameterized.Context as Ctx
import What4.FunctionName
import What4.Interface ( Pred )
import What4.ProgramLoc ( ProgramLoc )
import Lang.Crucible.Analysis.Postdom
import Lang.Crucible.CFG.Core
import Lang.Crucible.FunctionHandle
import Lang.Crucible.Simulator.Intrinsics
import Lang.Crucible.Simulator.RegMap
import Lang.Crucible.Backend
data CrucibleBranchTarget f (args :: Maybe (Ctx CrucibleType)) where
BlockTarget ::
!(BlockID blocks args) ->
CrucibleBranchTarget (CrucibleLang blocks r) ('Just args)
ReturnTarget ::
CrucibleBranchTarget f 'Nothing
instance TestEquality (CrucibleBranchTarget f) where
testEquality :: forall (a :: Maybe (Ctx CrucibleType))
(b :: Maybe (Ctx CrucibleType)).
CrucibleBranchTarget f a
-> CrucibleBranchTarget f b -> Maybe (a :~: b)
testEquality (BlockTarget BlockID blocks args
x) (BlockTarget BlockID blocks args
y) =
case BlockID blocks args -> BlockID blocks args -> Maybe (args :~: args)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx CrucibleType) (b :: Ctx CrucibleType).
BlockID blocks a -> BlockID blocks b -> Maybe (a :~: b)
testEquality BlockID blocks args
x BlockID blocks args
BlockID blocks args
y of
Just args :~: args
Refl -> (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
Maybe (args :~: args)
Nothing -> Maybe (a :~: b)
forall a. Maybe a
Nothing
testEquality CrucibleBranchTarget f a
ReturnTarget CrucibleBranchTarget f b
ReturnTarget = (a :~: b) -> Maybe (a :~: b)
forall a. a -> Maybe a
Just a :~: a
a :~: b
forall {k} (a :: k). a :~: a
Refl
testEquality CrucibleBranchTarget f a
_ CrucibleBranchTarget f b
_ = Maybe (a :~: b)
forall a. Maybe a
Nothing
ppBranchTarget :: CrucibleBranchTarget f args -> String
ppBranchTarget :: forall f (args :: Maybe (Ctx CrucibleType)).
CrucibleBranchTarget f args -> String
ppBranchTarget (BlockTarget BlockID blocks args
b) = String
"merge: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BlockID blocks args -> String
forall a. Show a => a -> String
show BlockID blocks args
b
ppBranchTarget CrucibleBranchTarget f args
ReturnTarget = String
"return"
data CallFrame sym ext blocks ret args
= forall initialArgs.
CallFrame
{ ()
_frameCFG :: CFG ext blocks initialArgs ret
, forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args -> CFGPostdom blocks
_framePostdomMap :: !(CFGPostdom blocks)
, forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args -> Some (BlockID blocks)
_frameBlockID :: !(Some (BlockID blocks))
, forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args -> RegMap sym args
_frameRegs :: !(RegMap sym args)
, forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args -> StmtSeq ext blocks ret args
_frameStmts :: !(StmtSeq ext blocks ret args)
, forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args
-> Some (CrucibleBranchTarget (CrucibleLang blocks ret))
_framePostdom :: !(Some (CrucibleBranchTarget (CrucibleLang blocks ret)))
}
frameBlockMap :: CallFrame sym ext blocks ret ctx -> BlockMap ext blocks ret
frameBlockMap :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> BlockMap ext blocks ret
frameBlockMap CallFrame { _frameCFG :: ()
_frameCFG = CFG ext blocks initialArgs ret
g } = CFG ext blocks initialArgs ret -> BlockMap ext blocks ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap CFG ext blocks initialArgs ret
g
frameHandle :: CallFrame sym ext blocks ret ctx -> SomeHandle
frameHandle :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> SomeHandle
frameHandle CallFrame { _frameCFG :: ()
_frameCFG = CFG ext blocks initialArgs ret
g } = FnHandle initialArgs ret -> SomeHandle
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> SomeHandle
SomeHandle (CFG ext blocks initialArgs ret -> FnHandle initialArgs ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> FnHandle init ret
cfgHandle CFG ext blocks initialArgs ret
g)
frameReturnType :: CallFrame sym ext blocks ret ctx -> TypeRepr ret
frameReturnType :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> TypeRepr ret
frameReturnType CallFrame { _frameCFG :: ()
_frameCFG = CFG ext blocks initialArgs ret
g } = CFG ext blocks initialArgs ret -> TypeRepr ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> TypeRepr ret
cfgReturnType CFG ext blocks initialArgs ret
g
framePostdomMap :: Simple Lens (CallFrame sym ext blocks ret ctx) (CFGPostdom blocks)
framePostdomMap :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType)
(f :: Type -> Type).
Functor f =>
(CFGPostdom blocks -> f (CFGPostdom blocks))
-> CallFrame sym ext blocks ret ctx
-> f (CallFrame sym ext blocks ret ctx)
framePostdomMap = (CallFrame sym ext blocks ret ctx -> CFGPostdom blocks)
-> (CallFrame sym ext blocks ret ctx
-> CFGPostdom blocks -> CallFrame sym ext blocks ret ctx)
-> Lens
(CallFrame sym ext blocks ret ctx)
(CallFrame sym ext blocks ret ctx)
(CFGPostdom blocks)
(CFGPostdom blocks)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens CallFrame sym ext blocks ret ctx -> CFGPostdom blocks
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args -> CFGPostdom blocks
_framePostdomMap (\CallFrame sym ext blocks ret ctx
s CFGPostdom blocks
x -> CallFrame sym ext blocks ret ctx
s{ _framePostdomMap = x })
frameBlockID :: Simple Lens (CallFrame sym ext blocks ret ctx) (Some (BlockID blocks))
frameBlockID :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType)
(f :: Type -> Type).
Functor f =>
(Some (BlockID blocks) -> f (Some (BlockID blocks)))
-> CallFrame sym ext blocks ret ctx
-> f (CallFrame sym ext blocks ret ctx)
frameBlockID = (CallFrame sym ext blocks ret ctx -> Some (BlockID blocks))
-> (CallFrame sym ext blocks ret ctx
-> Some (BlockID blocks) -> CallFrame sym ext blocks ret ctx)
-> Lens
(CallFrame sym ext blocks ret ctx)
(CallFrame sym ext blocks ret ctx)
(Some (BlockID blocks))
(Some (BlockID blocks))
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens CallFrame sym ext blocks ret ctx -> Some (BlockID blocks)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args -> Some (BlockID blocks)
_frameBlockID (\CallFrame sym ext blocks ret ctx
s Some (BlockID blocks)
v -> CallFrame sym ext blocks ret ctx
s { _frameBlockID = v })
frameStmts :: Simple Lens (CallFrame sym ext blocks ret ctx) (StmtSeq ext blocks ret ctx)
frameStmts :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType)
(f :: Type -> Type).
Functor f =>
(StmtSeq ext blocks ret ctx -> f (StmtSeq ext blocks ret ctx))
-> CallFrame sym ext blocks ret ctx
-> f (CallFrame sym ext blocks ret ctx)
frameStmts = (CallFrame sym ext blocks ret ctx -> StmtSeq ext blocks ret ctx)
-> (CallFrame sym ext blocks ret ctx
-> StmtSeq ext blocks ret ctx -> CallFrame sym ext blocks ret ctx)
-> Lens
(CallFrame sym ext blocks ret ctx)
(CallFrame sym ext blocks ret ctx)
(StmtSeq ext blocks ret ctx)
(StmtSeq ext blocks ret ctx)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens CallFrame sym ext blocks ret ctx -> StmtSeq ext blocks ret ctx
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args -> StmtSeq ext blocks ret args
_frameStmts (\CallFrame sym ext blocks ret ctx
s StmtSeq ext blocks ret ctx
v -> CallFrame sym ext blocks ret ctx
s { _frameStmts = v })
{-# INLINE frameStmts #-}
frameRegs :: Simple Lens (CallFrame sym ext blocks ret args) (RegMap sym args)
frameRegs :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (args :: Ctx CrucibleType)
(f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args))
-> CallFrame sym ext blocks ret args
-> f (CallFrame sym ext blocks ret args)
frameRegs = (CallFrame sym ext blocks ret args -> RegMap sym args)
-> (CallFrame sym ext blocks ret args
-> RegMap sym args -> CallFrame sym ext blocks ret args)
-> Lens
(CallFrame sym ext blocks ret args)
(CallFrame sym ext blocks ret args)
(RegMap sym args)
(RegMap sym args)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens CallFrame sym ext blocks ret args -> RegMap sym args
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args -> RegMap sym args
_frameRegs (\CallFrame sym ext blocks ret args
s RegMap sym args
v -> CallFrame sym ext blocks ret args
s { _frameRegs = v })
framePostdom :: Simple Lens (CallFrame sym ext blocks ret ctx) (Some (CrucibleBranchTarget (CrucibleLang blocks ret)))
framePostdom :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType)
(f :: Type -> Type).
Functor f =>
(Some (CrucibleBranchTarget (CrucibleLang blocks ret))
-> f (Some (CrucibleBranchTarget (CrucibleLang blocks ret))))
-> CallFrame sym ext blocks ret ctx
-> f (CallFrame sym ext blocks ret ctx)
framePostdom = (CallFrame sym ext blocks ret ctx
-> Some (CrucibleBranchTarget (CrucibleLang blocks ret)))
-> (CallFrame sym ext blocks ret ctx
-> Some (CrucibleBranchTarget (CrucibleLang blocks ret))
-> CallFrame sym ext blocks ret ctx)
-> Lens
(CallFrame sym ext blocks ret ctx)
(CallFrame sym ext blocks ret ctx)
(Some (CrucibleBranchTarget (CrucibleLang blocks ret)))
(Some (CrucibleBranchTarget (CrucibleLang blocks ret)))
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens CallFrame sym ext blocks ret ctx
-> Some (CrucibleBranchTarget (CrucibleLang blocks ret))
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args
-> Some (CrucibleBranchTarget (CrucibleLang blocks ret))
_framePostdom (\CallFrame sym ext blocks ret ctx
s Some (CrucibleBranchTarget (CrucibleLang blocks ret))
v -> CallFrame sym ext blocks ret ctx
s { _framePostdom = v })
mkCallFrame :: CFG ext blocks init ret
-> CFGPostdom blocks
-> RegMap sym init
-> CallFrame sym ext blocks ret init
mkCallFrame :: forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType) sym.
CFG ext blocks init ret
-> CFGPostdom blocks
-> RegMap sym init
-> CallFrame sym ext blocks ret init
mkCallFrame CFG ext blocks init ret
g = CFG ext blocks init ret
-> BlockID blocks init
-> CFGPostdom blocks
-> RegMap sym init
-> CallFrame sym ext blocks ret init
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType)
(args :: Ctx CrucibleType) sym.
CFG ext blocks init ret
-> BlockID blocks args
-> CFGPostdom blocks
-> RegMap sym args
-> CallFrame sym ext blocks ret args
mkBlockFrame CFG ext blocks init ret
g (CFG ext blocks init ret -> BlockID blocks init
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockID blocks init
cfgEntryBlockID CFG ext blocks init ret
g)
mkBlockFrame ::
CFG ext blocks init ret ->
BlockID blocks args ->
CFGPostdom blocks ->
RegMap sym args ->
CallFrame sym ext blocks ret args
mkBlockFrame :: forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType)
(args :: Ctx CrucibleType) sym.
CFG ext blocks init ret
-> BlockID blocks args
-> CFGPostdom blocks
-> RegMap sym args
-> CallFrame sym ext blocks ret args
mkBlockFrame CFG ext blocks init ret
g bid :: BlockID blocks args
bid@(BlockID Index blocks args
block_id) CFGPostdom blocks
pdInfo RegMap sym args
args = do
let b :: Block ext blocks ret args
b = CFG ext blocks init ret -> BlockMap ext blocks ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
(init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgBlockMap CFG ext blocks init ret
g BlockMap ext blocks ret
-> Index blocks args -> Block ext blocks ret args
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index blocks args
block_id
let pds :: [Some (BlockID blocks)]
pds = Const [Some (BlockID blocks)] args -> [Some (BlockID blocks)]
forall {k} a (b :: k). Const a b -> a
getConst (Const [Some (BlockID blocks)] args -> [Some (BlockID blocks)])
-> Const [Some (BlockID blocks)] args -> [Some (BlockID blocks)]
forall a b. (a -> b) -> a -> b
$ CFGPostdom blocks
pdInfo CFGPostdom blocks
-> Index blocks args -> Const [Some (BlockID blocks)] args
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index blocks args
block_id
CallFrame { _frameCFG :: CFG ext blocks init ret
_frameCFG = CFG ext blocks init ret
g
, _framePostdomMap :: CFGPostdom blocks
_framePostdomMap = CFGPostdom blocks
pdInfo
, _frameBlockID :: Some (BlockID blocks)
_frameBlockID = BlockID blocks args -> Some (BlockID blocks)
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some BlockID blocks args
bid
, _frameRegs :: RegMap sym args
_frameRegs = RegMap sym args
args
, _frameStmts :: StmtSeq ext blocks ret args
_frameStmts = Block ext blocks ret args
bBlock ext blocks ret args
-> Getting
(StmtSeq ext blocks ret args)
(Block ext blocks ret args)
(StmtSeq ext blocks ret args)
-> StmtSeq ext blocks ret args
forall s a. s -> Getting a s a -> a
^.Getting
(StmtSeq ext blocks ret args)
(Block ext blocks ret args)
(StmtSeq ext blocks ret args)
forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType)
(c :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(StmtSeq ext b r c -> f (StmtSeq ext b r c))
-> Block ext b r c -> f (Block ext b r c)
blockStmts
, _framePostdom :: Some (CrucibleBranchTarget (CrucibleLang blocks ret))
_framePostdom = [Some (BlockID blocks)]
-> Some (CrucibleBranchTarget (CrucibleLang blocks ret))
forall (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
[Some (BlockID blocks)]
-> Some (CrucibleBranchTarget (CrucibleLang blocks ret))
mkFramePostdom [Some (BlockID blocks)]
pds
}
mkFramePostdom :: [Some (BlockID blocks)] -> Some (CrucibleBranchTarget (CrucibleLang blocks ret))
mkFramePostdom :: forall (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType).
[Some (BlockID blocks)]
-> Some (CrucibleBranchTarget (CrucibleLang blocks ret))
mkFramePostdom [] = CrucibleBranchTarget (CrucibleLang blocks ret) 'Nothing
-> Some (CrucibleBranchTarget (CrucibleLang blocks ret))
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some CrucibleBranchTarget (CrucibleLang blocks ret) 'Nothing
forall f. CrucibleBranchTarget f 'Nothing
ReturnTarget
mkFramePostdom (Some BlockID blocks x
i:[Some (BlockID blocks)]
_) = CrucibleBranchTarget (CrucibleLang blocks ret) ('Just x)
-> Some (CrucibleBranchTarget (CrucibleLang blocks ret))
forall k (f :: k -> Type) (x :: k). f x -> Some f
Some (BlockID blocks x
-> CrucibleBranchTarget (CrucibleLang blocks ret) ('Just x)
forall (blocks :: Ctx (Ctx CrucibleType)) (ret :: Ctx CrucibleType)
(args :: CrucibleType).
BlockID blocks ret
-> CrucibleBranchTarget (CrucibleLang blocks args) ('Just ret)
BlockTarget BlockID blocks x
i)
frameProgramLoc :: CallFrame sym ext blocks ret ctx -> ProgramLoc
frameProgramLoc :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> ProgramLoc
frameProgramLoc CallFrame sym ext blocks ret ctx
cf = StmtSeq ext blocks ret ctx -> ProgramLoc
forall ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType)
(ctx :: Ctx CrucibleType).
StmtSeq ext b r ctx -> ProgramLoc
firstStmtLoc (CallFrame sym ext blocks ret ctx
cfCallFrame sym ext blocks ret ctx
-> Getting
(StmtSeq ext blocks ret ctx)
(CallFrame sym ext blocks ret ctx)
(StmtSeq ext blocks ret ctx)
-> StmtSeq ext blocks ret ctx
forall s a. s -> Getting a s a -> a
^.Getting
(StmtSeq ext blocks ret ctx)
(CallFrame sym ext blocks ret ctx)
(StmtSeq ext blocks ret ctx)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType)
(f :: Type -> Type).
Functor f =>
(StmtSeq ext blocks ret ctx -> f (StmtSeq ext blocks ret ctx))
-> CallFrame sym ext blocks ret ctx
-> f (CallFrame sym ext blocks ret ctx)
frameStmts)
setFrameBlock :: BlockID blocks args
-> RegMap sym args
-> CallFrame sym ext blocks ret ctx
-> CallFrame sym ext blocks ret args
setFrameBlock :: forall (blocks :: Ctx (Ctx CrucibleType))
(args :: Ctx CrucibleType) sym ext (ret :: CrucibleType)
(ctx :: Ctx CrucibleType).
BlockID blocks args
-> RegMap sym args
-> CallFrame sym ext blocks ret ctx
-> CallFrame sym ext blocks ret args
setFrameBlock bid :: BlockID blocks args
bid@(BlockID Index blocks args
block_id) RegMap sym args
args CallFrame sym ext blocks ret ctx
f = CallFrame sym ext blocks ret args
f'
where b :: Block ext blocks ret args
b = CallFrame sym ext blocks ret ctx -> BlockMap ext blocks ret
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> BlockMap ext blocks ret
frameBlockMap CallFrame sym ext blocks ret ctx
f BlockMap ext blocks ret
-> Index blocks args -> Block ext blocks ret args
forall {k} (f :: k -> Type) (ctx :: Ctx k) (tp :: k).
Assignment f ctx -> Index ctx tp -> f tp
Ctx.! Index blocks args
block_id
pds :: [Some (BlockID blocks)]
pds = Const [Some (BlockID blocks)] args -> [Some (BlockID blocks)]
forall {k} a (b :: k). Const a b -> a
getConst (Const [Some (BlockID blocks)] args -> [Some (BlockID blocks)])
-> Const [Some (BlockID blocks)] args -> [Some (BlockID blocks)]
forall a b. (a -> b) -> a -> b
$ (CallFrame sym ext blocks ret ctx
fCallFrame sym ext blocks ret ctx
-> Getting
(Const [Some (BlockID blocks)] args)
(CallFrame sym ext blocks ret ctx)
(Const [Some (BlockID blocks)] args)
-> Const [Some (BlockID blocks)] args
forall s a. s -> Getting a s a -> a
^.(CFGPostdom blocks
-> Const (Const [Some (BlockID blocks)] args) (CFGPostdom blocks))
-> CallFrame sym ext blocks ret ctx
-> Const
(Const [Some (BlockID blocks)] args)
(CallFrame sym ext blocks ret ctx)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType)
(f :: Type -> Type).
Functor f =>
(CFGPostdom blocks -> f (CFGPostdom blocks))
-> CallFrame sym ext blocks ret ctx
-> f (CallFrame sym ext blocks ret ctx)
framePostdomMap((CFGPostdom blocks
-> Const (Const [Some (BlockID blocks)] args) (CFGPostdom blocks))
-> CallFrame sym ext blocks ret ctx
-> Const
(Const [Some (BlockID blocks)] args)
(CallFrame sym ext blocks ret ctx))
-> ((Const [Some (BlockID blocks)] args
-> Const
(Const [Some (BlockID blocks)] args)
(Const [Some (BlockID blocks)] args))
-> CFGPostdom blocks
-> Const (Const [Some (BlockID blocks)] args) (CFGPostdom blocks))
-> Getting
(Const [Some (BlockID blocks)] args)
(CallFrame sym ext blocks ret ctx)
(Const [Some (BlockID blocks)] args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
.IndexF (CFGPostdom blocks) args
-> Traversal'
(CFGPostdom blocks) (IxValueF (CFGPostdom blocks) args)
forall k m (x :: k).
IxedF k m =>
IndexF m x -> Traversal' m (IxValueF m x)
forall (x :: Ctx CrucibleType).
IndexF (CFGPostdom blocks) x
-> Traversal' (CFGPostdom blocks) (IxValueF (CFGPostdom blocks) x)
ixF IndexF (CFGPostdom blocks) args
Index blocks args
block_id)
f' :: CallFrame sym ext blocks ret args
f' = CallFrame sym ext blocks ret ctx
f { _frameBlockID = Some bid
, _frameRegs = args
, _frameStmts = b^.blockStmts
, _framePostdom = mkFramePostdom pds
}
setFrameBreakpointPostdomInfo ::
[BreakpointName] ->
CallFrame sym ext blocks ret ctx ->
CallFrame sym ext blocks ret ctx
setFrameBreakpointPostdomInfo :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType).
[BreakpointName]
-> CallFrame sym ext blocks ret ctx
-> CallFrame sym ext blocks ret ctx
setFrameBreakpointPostdomInfo [BreakpointName]
breakpoints CallFrame sym ext blocks ret ctx
f = case CallFrame sym ext blocks ret ctx
f of
CallFrame{ _frameCFG :: ()
_frameCFG = CFG ext blocks initialArgs ret
g, _frameBlockID :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args -> Some (BlockID blocks)
_frameBlockID = Some (BlockID Index blocks x
block_id) } -> do
let pdInfo :: CFGPostdom blocks
pdInfo = CFG ext blocks initialArgs ret
-> [BreakpointName] -> CFGPostdom blocks
forall ext (b :: Ctx (Ctx CrucibleType)) (i :: Ctx CrucibleType)
(r :: CrucibleType).
CFG ext b i r -> [BreakpointName] -> CFGPostdom b
breakpointPostdomInfo CFG ext blocks initialArgs ret
g [BreakpointName]
breakpoints
CallFrame sym ext blocks ret ctx
f { _framePostdomMap = pdInfo
, _framePostdom = mkFramePostdom (getConst $ pdInfo Ctx.! block_id)
}
updateFrame :: RegMap sym ctx'
-> BlockID blocks ctx
-> StmtSeq ext blocks ret ctx'
-> CallFrame sym ext blocks ret ctx
-> CallFrame sym ext blocks ret ctx'
updateFrame :: forall sym (ctx' :: Ctx CrucibleType)
(blocks :: Ctx (Ctx CrucibleType)) (ctx :: Ctx CrucibleType) ext
(ret :: CrucibleType).
RegMap sym ctx'
-> BlockID blocks ctx
-> StmtSeq ext blocks ret ctx'
-> CallFrame sym ext blocks ret ctx
-> CallFrame sym ext blocks ret ctx'
updateFrame RegMap sym ctx'
r BlockID blocks ctx
b StmtSeq ext blocks ret ctx'
s CallFrame sym ext blocks ret ctx
f = CallFrame sym ext blocks ret ctx
f { _frameBlockID = Some b, _frameRegs = r, _frameStmts = s }
extendFrame :: TypeRepr tp
-> RegValue sym tp
-> StmtSeq ext blocks ret (ctx ::> tp)
-> CallFrame sym ext blocks ret ctx
-> CallFrame sym ext blocks ret (ctx ::> tp)
extendFrame :: forall (tp :: CrucibleType) sym ext
(blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
(ctx :: Ctx CrucibleType).
TypeRepr tp
-> RegValue sym tp
-> StmtSeq ext blocks ret (ctx ::> tp)
-> CallFrame sym ext blocks ret ctx
-> CallFrame sym ext blocks ret (ctx ::> tp)
extendFrame TypeRepr tp
tp RegValue sym tp
v StmtSeq ext blocks ret (ctx ::> tp)
s CallFrame sym ext blocks ret ctx
f = CallFrame sym ext blocks ret ctx
f { _frameRegs = assignReg tp v (_frameRegs f)
, _frameStmts = s
}
mergeCallFrame :: IsSymInterface sym
=> sym
-> IntrinsicTypes sym
-> MuxFn (Pred sym) (CallFrame sym ext blocks ret args)
mergeCallFrame :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (args :: Ctx CrucibleType).
IsSymInterface sym =>
sym
-> IntrinsicTypes sym
-> MuxFn (Pred sym) (CallFrame sym ext blocks ret args)
mergeCallFrame sym
s IntrinsicTypes sym
iteFns Pred sym
p CallFrame sym ext blocks ret args
xcf CallFrame sym ext blocks ret args
ycf = do
RegMap sym args
r <- sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (RegMap sym args)
forall sym (ctx :: Ctx CrucibleType).
IsSymInterface sym =>
sym -> IntrinsicTypes sym -> MuxFn (Pred sym) (RegMap sym ctx)
mergeRegs sym
s IntrinsicTypes sym
iteFns Pred sym
p (CallFrame sym ext blocks ret args -> RegMap sym args
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args -> RegMap sym args
_frameRegs CallFrame sym ext blocks ret args
xcf) (CallFrame sym ext blocks ret args -> RegMap sym args
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args -> RegMap sym args
_frameRegs CallFrame sym ext blocks ret args
ycf)
CallFrame sym ext blocks ret args
-> IO (CallFrame sym ext blocks ret args)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (CallFrame sym ext blocks ret args
-> IO (CallFrame sym ext blocks ret args))
-> CallFrame sym ext blocks ret args
-> IO (CallFrame sym ext blocks ret args)
forall a b. (a -> b) -> a -> b
$ CallFrame sym ext blocks ret args
xcf { _frameRegs = r }
data CrucibleLang (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
data OverrideLang (ret :: CrucibleType)
data OverrideFrame sym (ret :: CrucibleType) args
= OverrideFrame { forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType).
OverrideFrame sym ret args -> FunctionName
_override :: !FunctionName
, forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType).
OverrideFrame sym ret args -> SomeHandle
_overrideHandle :: !SomeHandle
, forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType).
OverrideFrame sym ret args -> RegMap sym args
_overrideRegMap :: !(RegMap sym args)
}
override :: Simple Lens (OverrideFrame sym ret args) FunctionName
override :: forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType)
(f :: Type -> Type).
Functor f =>
(FunctionName -> f FunctionName)
-> OverrideFrame sym ret args -> f (OverrideFrame sym ret args)
override = (OverrideFrame sym ret args -> FunctionName)
-> (OverrideFrame sym ret args
-> FunctionName -> OverrideFrame sym ret args)
-> Lens
(OverrideFrame sym ret args)
(OverrideFrame sym ret args)
FunctionName
FunctionName
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens OverrideFrame sym ret args -> FunctionName
forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType).
OverrideFrame sym ret args -> FunctionName
_override (\OverrideFrame sym ret args
o FunctionName
x -> OverrideFrame sym ret args
o{ _override = x })
overrideHandle :: Simple Lens (OverrideFrame sym ret args) SomeHandle
overrideHandle :: forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType)
(f :: Type -> Type).
Functor f =>
(SomeHandle -> f SomeHandle)
-> OverrideFrame sym ret args -> f (OverrideFrame sym ret args)
overrideHandle = (OverrideFrame sym ret args -> SomeHandle)
-> (OverrideFrame sym ret args
-> SomeHandle -> OverrideFrame sym ret args)
-> Lens
(OverrideFrame sym ret args)
(OverrideFrame sym ret args)
SomeHandle
SomeHandle
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens OverrideFrame sym ret args -> SomeHandle
forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType).
OverrideFrame sym ret args -> SomeHandle
_overrideHandle (\OverrideFrame sym ret args
o SomeHandle
x -> OverrideFrame sym ret args
o { _overrideHandle = x })
overrideRegMap :: Lens (OverrideFrame sym ret args) (OverrideFrame sym ret args')
(RegMap sym args) (RegMap sym args')
overrideRegMap :: forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType)
(args' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(RegMap sym args -> f (RegMap sym args'))
-> OverrideFrame sym ret args -> f (OverrideFrame sym ret args')
overrideRegMap = (OverrideFrame sym ret args -> RegMap sym args)
-> (OverrideFrame sym ret args
-> RegMap sym args' -> OverrideFrame sym ret args')
-> Lens
(OverrideFrame sym ret args)
(OverrideFrame sym ret args')
(RegMap sym args)
(RegMap sym args')
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens OverrideFrame sym ret args -> RegMap sym args
forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType).
OverrideFrame sym ret args -> RegMap sym args
_overrideRegMap (\OverrideFrame sym ret args
o RegMap sym args'
x -> OverrideFrame sym ret args
o{ _overrideRegMap = x })
type family FrameRetType (f :: Type) :: CrucibleType where
FrameRetType (CrucibleLang b r) = r
FrameRetType (OverrideLang r) = r
data SimFrame sym ext l (args :: Maybe (Ctx CrucibleType)) where
OF :: !(OverrideFrame sym ret args)
-> SimFrame sym ext (OverrideLang ret) ('Just args)
MF :: !(CallFrame sym ext blocks ret args)
-> SimFrame sym ext (CrucibleLang blocks ret) ('Just args)
RF :: !FunctionName
-> !(RegEntry sym (FrameRetType f))
-> SimFrame sym ext f 'Nothing
overrideSimFrame :: Lens (SimFrame sym ext (OverrideLang r) ('Just args))
(SimFrame sym ext (OverrideLang r') ('Just args'))
(OverrideFrame sym r args)
(OverrideFrame sym r' args')
overrideSimFrame :: forall sym ext (r :: CrucibleType) (args :: Ctx CrucibleType)
(r' :: CrucibleType) (args' :: Ctx CrucibleType)
(f :: Type -> Type).
Functor f =>
(OverrideFrame sym r args -> f (OverrideFrame sym r' args'))
-> SimFrame sym ext (OverrideLang r) ('Just args)
-> f (SimFrame sym ext (OverrideLang r') ('Just args'))
overrideSimFrame OverrideFrame sym r args -> f (OverrideFrame sym r' args')
f (OF OverrideFrame sym ret args
g) = OverrideFrame sym r' args'
-> SimFrame sym ext (OverrideLang r') ('Just args')
forall sym (blocks :: CrucibleType) (ret :: Ctx CrucibleType) ext.
OverrideFrame sym blocks ret
-> SimFrame sym ext (OverrideLang blocks) ('Just ret)
OF (OverrideFrame sym r' args'
-> SimFrame sym ext (OverrideLang r') ('Just args'))
-> f (OverrideFrame sym r' args')
-> f (SimFrame sym ext (OverrideLang r') ('Just args'))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> OverrideFrame sym r args -> f (OverrideFrame sym r' args')
f OverrideFrame sym r args
OverrideFrame sym ret args
g
crucibleSimFrame :: Lens (SimFrame sym ext (CrucibleLang blocks r) ('Just args))
(SimFrame sym ext (CrucibleLang blocks' r') ('Just args'))
(CallFrame sym ext blocks r args)
(CallFrame sym ext blocks' r' args')
crucibleSimFrame :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(r :: CrucibleType) (args :: Ctx CrucibleType)
(blocks' :: Ctx (Ctx CrucibleType)) (r' :: CrucibleType)
(args' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r args
-> f (CallFrame sym ext blocks' r' args'))
-> SimFrame sym ext (CrucibleLang blocks r) ('Just args)
-> f (SimFrame sym ext (CrucibleLang blocks' r') ('Just args'))
crucibleSimFrame CallFrame sym ext blocks r args
-> f (CallFrame sym ext blocks' r' args')
f (MF CallFrame sym ext blocks ret args
c) = CallFrame sym ext blocks' r' args'
-> SimFrame sym ext (CrucibleLang blocks' r') ('Just args')
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args
-> SimFrame sym ext (CrucibleLang blocks ret) ('Just args)
MF (CallFrame sym ext blocks' r' args'
-> SimFrame sym ext (CrucibleLang blocks' r') ('Just args'))
-> f (CallFrame sym ext blocks' r' args')
-> f (SimFrame sym ext (CrucibleLang blocks' r') ('Just args'))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> CallFrame sym ext blocks r args
-> f (CallFrame sym ext blocks' r' args')
f CallFrame sym ext blocks r args
CallFrame sym ext blocks ret args
c
fromCallFrame :: SimFrame sym ext (CrucibleLang b r) ('Just a)
-> CallFrame sym ext b r a
fromCallFrame :: forall sym ext (b :: Ctx (Ctx CrucibleType)) (r :: CrucibleType)
(a :: Ctx CrucibleType).
SimFrame sym ext (CrucibleLang b r) ('Just a)
-> CallFrame sym ext b r a
fromCallFrame (MF CallFrame sym ext blocks ret args
x) = CallFrame sym ext b r a
CallFrame sym ext blocks ret args
x
fromReturnFrame :: SimFrame sym ext f 'Nothing
-> RegEntry sym (FrameRetType f)
fromReturnFrame :: forall sym ext f.
SimFrame sym ext f 'Nothing -> RegEntry sym (FrameRetType f)
fromReturnFrame (RF FunctionName
_ RegEntry sym (FrameRetType f)
x) = RegEntry sym (FrameRetType f)
x
frameFunctionName :: Getter (SimFrame sym ext f a) FunctionName
frameFunctionName :: forall sym ext f (a :: Maybe (Ctx CrucibleType))
(f :: Type -> Type).
(Contravariant f, Functor f) =>
(FunctionName -> f FunctionName)
-> SimFrame sym ext f a -> f (SimFrame sym ext f a)
frameFunctionName = (SimFrame sym ext f a -> FunctionName)
-> Optic' (->) f (SimFrame sym ext f a) FunctionName
forall (p :: Type -> Type -> Type) (f :: Type -> Type) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
to ((SimFrame sym ext f a -> FunctionName)
-> Optic' (->) f (SimFrame sym ext f a) FunctionName)
-> (SimFrame sym ext f a -> FunctionName)
-> Optic' (->) f (SimFrame sym ext f a) FunctionName
forall a b. (a -> b) -> a -> b
$ \case
OF OverrideFrame sym ret args
f -> OverrideFrame sym ret args
fOverrideFrame sym ret args
-> Getting FunctionName (OverrideFrame sym ret args) FunctionName
-> FunctionName
forall s a. s -> Getting a s a -> a
^.Getting FunctionName (OverrideFrame sym ret args) FunctionName
forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType)
(f :: Type -> Type).
Functor f =>
(FunctionName -> f FunctionName)
-> OverrideFrame sym ret args -> f (OverrideFrame sym ret args)
override
MF CallFrame sym ext blocks ret args
f -> case CallFrame sym ext blocks ret args -> SomeHandle
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
(ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> SomeHandle
frameHandle CallFrame sym ext blocks ret args
f of SomeHandle FnHandle args ret
h -> FnHandle args ret -> FunctionName
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
handleName FnHandle args ret
h
RF FunctionName
n RegEntry sym (FrameRetType f)
_ -> FunctionName
n