-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Simulator.CallFrame
-- Description      : Data structure for call frames in the simulator
-- Copyright        : (c) Galois, Inc 2014
-- License          : BSD3
-- Maintainer       : Joe Hendrix <jhendrix@galois.com>
-- Stability        : provisional
--
-- Call frames are used to record information about suspended stack
-- frames when functions are called.
------------------------------------------------------------------------

{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
module Lang.Crucible.Simulator.CallFrame
  ( -- * CrucibleBranchTarget
    CrucibleBranchTarget(..)
  , ppBranchTarget
    -- * Call frame
  , CallFrame(..)
  , mkCallFrame
  , mkBlockFrame
  , framePostdomMap
  , frameBlockMap
  , frameHandle
  , frameReturnType
  , frameBlockID
  , frameRegs
  , frameStmts
  , framePostdom
  , frameProgramLoc
  , setFrameBlock
  , setFrameBreakpointPostdomInfo
  , extendFrame
  , updateFrame
  , mergeCallFrame
    -- * SomeHandle
  , SomeHandle(..)
    -- * Simulator frames
  , 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


------------------------------------------------------------------------
-- CrucibleBranchTarget

-- | A 'CrucibleBranchTarget' identifies a program location that is a
--   potential join point.  Each label is a merge point, and there is
--   an additional implicit join point at function returns.
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"


------------------------------------------------------------------------
-- CallFrame

-- | A call frame for a crucible block.
data CallFrame sym ext blocks ret args
   = forall initialArgs.
     CallFrame
     { ()
_frameCFG        :: CFG ext blocks initialArgs ret
       -- ^ Handle to control flow graph for the current frame.
     , forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args -> CFGPostdom blocks
_framePostdomMap :: !(CFGPostdom blocks)
       -- ^ Post-dominator map for control flow graph associated with this
       -- function.
     , 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 })

-- | List of statements to execute next.
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 })

-- | List of statements to execute next.
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 })

-- | Create a new call frame.
mkCallFrame :: CFG ext blocks init ret
               -- ^ Control flow graph
            -> CFGPostdom blocks
               -- ^ Post dominator information.
            -> RegMap sym init
               -- ^ Initial arguments
            -> 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)

-- | Create a new call frame.
mkBlockFrame ::
  CFG ext blocks init ret {- ^  Control flow graph -} ->
  BlockID blocks args {- ^ Entry point -} ->
  CFGPostdom blocks {- ^ Post dominator information -} ->
  RegMap sym args {- ^ Initial arguments -} ->
  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)


-- | Return program location associated with frame.
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 }

-- | Extend frame with new register.
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 }


------------------------------------------------------------------------
-- CrucibleLang

-- | Nominal type for identifying override frames.
data CrucibleLang (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)

------------------------------------------------------------------------
-- OverrideLang

-- | Nominal type for identifying override frames.
data OverrideLang (ret :: CrucibleType)

------------------------------------------------------------------------
-- OverrideFrame

-- | Frame in call to override.
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)
                     -- ^ Arguments to override.
                   }

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 })

------------------------------------------------------------------------
-- SimFrame

{- An alternate idea we could try to save a few indirections...
type family SimFrame sym ext l args :: * where
  SimFrame sym ext (OverrideLang ret)        ('Just args) = OverrideFrame sym ret args
  SimFrame sym ext (CrucibleLang blocks ret) ('Just args) = CallFrame sym ext blocks ret args
  SimFrame sym ext (CrucibleLang blocks ret) ('Nothing)   = RegEntry sym ret
-}

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
  -- | Custom code to execute, typically for "overrides"
  OF :: !(OverrideFrame sym ret args)
     -> SimFrame sym ext (OverrideLang ret) ('Just args)

  -- | We are executing some Crucible instructions
  MF :: !(CallFrame sym ext blocks ret args)
     -> SimFrame sym ext (CrucibleLang blocks ret) ('Just args)

  -- | We should return this value.
  RF :: !FunctionName {- Function we are returning from -}
     -> !(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