-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Simulator.Breakpoint
-- Description      : Support for symbolic execution breakpoints
-- Copyright        : (c) Galois, Inc 2019
-- License          : BSD3
-- Maintainer       : Andrei Stefanescu <andrei@galois.com>
-- Stability        : provisional
--
-- This module provides execution features for changing the state on
-- breakpoints.
-----------------------------------------------------------------------
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RecordWildCards #-}
module Lang.Crucible.Simulator.Breakpoint
  ( breakAndReturn
  ) where

import           Control.Lens
import           Control.Monad.Reader
import qualified Data.Bimap as Bimap
import           Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HashMap

import           Data.Parameterized.Classes
import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.Some
import           Data.Parameterized.TraversableFC

import qualified Lang.Crucible.Backend as C
import qualified Lang.Crucible.CFG.Core as C
import qualified Lang.Crucible.CFG.Expr as C
import qualified Lang.Crucible.Simulator.CallFrame as C
import qualified Lang.Crucible.Simulator.EvalStmt as C
import qualified Lang.Crucible.Simulator.ExecutionTree as C
import qualified Lang.Crucible.Simulator.Operations as C
import qualified Lang.Crucible.Simulator.OverrideSim as C
import qualified Lang.Crucible.Simulator.RegValue as C
import qualified What4.FunctionName as W

-- | This execution feature registers an override for a breakpoint.
--   The override summarizes the execution from the breakpoint
--   to the return from the function (similar to a tail call).
--   This feature requires a map from each function handle
--   to the list of breakpoints in the respective function with this
--   execution feature.
breakAndReturn ::
  (C.IsSymInterface sym, C.IsSyntaxExtension ext) =>
  C.CFG ext blocks init ret ->
  C.BreakpointName ->
  Ctx.Assignment C.TypeRepr args ->
  C.TypeRepr ret ->
  C.OverrideSim p sym ext rtp args ret (C.RegValue sym ret) ->
  HashMap C.SomeHandle [C.BreakpointName] ->
  IO (C.ExecutionFeature p sym ext rtp)
breakAndReturn :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType)
       (args :: Ctx CrucibleType) p rtp.
(IsSymInterface sym, IsSyntaxExtension ext) =>
CFG ext blocks init ret
-> BreakpointName
-> Assignment TypeRepr args
-> TypeRepr ret
-> OverrideSim p sym ext rtp args ret (RegValue sym ret)
-> HashMap SomeHandle [BreakpointName]
-> IO (ExecutionFeature p sym ext rtp)
breakAndReturn C.CFG{Bimap BreakpointName (Some (BlockID blocks))
BlockMap ext blocks ret
FnHandle init ret
BlockID blocks init
cfgHandle :: FnHandle init ret
cfgBlockMap :: BlockMap ext blocks ret
cfgEntryBlockID :: BlockID blocks init
cfgBreakpoints :: Bimap BreakpointName (Some (BlockID blocks))
cfgHandle :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> FnHandle init ret
cfgBlockMap :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgEntryBlockID :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockID blocks init
cfgBreakpoints :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> Bimap BreakpointName (Some (BlockID blocks))
..} BreakpointName
breakpoint_name Assignment TypeRepr args
arg_types TypeRepr ret
ret_type OverrideSim p sym ext rtp args ret (RegValue sym ret)
override HashMap SomeHandle [BreakpointName]
all_breakpoints =
  case BreakpointName
-> Bimap BreakpointName (Some (BlockID blocks))
-> Maybe (Some (BlockID blocks))
forall a b (m :: Type -> Type).
(Ord a, Ord b, MonadThrow m) =>
a -> Bimap a b -> m b
Bimap.lookup BreakpointName
breakpoint_name Bimap BreakpointName (Some (BlockID blocks))
cfgBreakpoints of
    Just (Some BlockID blocks x
breakpoint_block_id)
      | Block ext blocks ret x
breakpoint_block <- BlockID blocks x
-> BlockMap ext blocks ret -> Block ext blocks ret x
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) ext (ret :: CrucibleType).
BlockID blocks args
-> BlockMap ext blocks ret -> Block ext blocks ret args
C.getBlock BlockID blocks x
breakpoint_block_id BlockMap ext blocks ret
cfgBlockMap
      , Just x :~: args
Refl <- Assignment TypeRepr x
-> Assignment TypeRepr args -> Maybe (x :~: 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).
Assignment TypeRepr a -> Assignment TypeRepr b -> Maybe (a :~: b)
testEquality (Block ext blocks ret x -> Assignment TypeRepr x
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
C.blockInputs Block ext blocks ret x
breakpoint_block) Assignment TypeRepr args
arg_types ->
        ExecutionFeature p sym ext rtp
-> IO (ExecutionFeature p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecutionFeature p sym ext rtp
 -> IO (ExecutionFeature p sym ext rtp))
-> ExecutionFeature p sym ext rtp
-> IO (ExecutionFeature p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ (ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
forall p sym ext rtp.
(ExecState p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
C.ExecutionFeature ((ExecState p sym ext rtp
  -> IO (ExecutionFeatureResult p sym ext rtp))
 -> ExecutionFeature p sym ext rtp)
-> (ExecState p sym ext rtp
    -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeature p sym ext rtp
forall a b. (a -> b) -> a -> b
$ \case
          C.RunningState (C.RunPostBranchMerge BlockID blocks args
block_id) SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
state
            | CallFrame sym ext blocks r args
frame <- SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
state SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Getting
     (CallFrame sym ext blocks r args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     (CallFrame sym ext blocks r args)
-> CallFrame sym ext blocks r args
forall s a. s -> Getting a s a -> a
^. Getting
  (CallFrame sym ext blocks r args)
  (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
  (CallFrame sym ext blocks r args)
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
C.stateCrucibleFrame
            , FnHandle init ret -> SomeHandle
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> SomeHandle
C.SomeHandle FnHandle init ret
cfgHandle SomeHandle -> SomeHandle -> Bool
forall a. Eq a => a -> a -> Bool
== CallFrame sym ext blocks r args -> SomeHandle
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> SomeHandle
C.frameHandle CallFrame sym ext blocks r args
frame
            , Just blocks :~: blocks
Refl <- Assignment (Assignment TypeRepr) blocks
-> Assignment (Assignment TypeRepr) blocks
-> Maybe (blocks :~: blocks)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: Ctx (Ctx CrucibleType)) (b :: Ctx (Ctx CrucibleType)).
Assignment (Assignment TypeRepr) a
-> Assignment (Assignment TypeRepr) b -> Maybe (a :~: b)
testEquality
                ((forall (x :: Ctx CrucibleType).
 Block ext blocks ret x -> Assignment TypeRepr x)
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment (Block ext blocks ret) x
   -> Assignment (Assignment TypeRepr) x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: Ctx CrucibleType -> Type)
       (g :: Ctx CrucibleType -> Type).
(forall (x :: Ctx CrucibleType). f x -> g x)
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment f x -> Assignment g x
fmapFC Block ext blocks ret x -> CtxRepr x
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
forall (x :: Ctx CrucibleType).
Block ext blocks ret x -> Assignment TypeRepr x
C.blockInputs BlockMap ext blocks ret
cfgBlockMap)
                ((forall (x :: Ctx CrucibleType).
 Block ext blocks r x -> Assignment TypeRepr x)
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment (Block ext blocks r) x
   -> Assignment (Assignment TypeRepr) x
forall k l (t :: (k -> Type) -> l -> Type) (f :: k -> Type)
       (g :: k -> Type).
FunctorFC t =>
(forall (x :: k). f x -> g x) -> forall (x :: l). t f x -> t g x
forall (f :: Ctx CrucibleType -> Type)
       (g :: Ctx CrucibleType -> Type).
(forall (x :: Ctx CrucibleType). f x -> g x)
-> forall (x :: Ctx (Ctx CrucibleType)).
   Assignment f x -> Assignment g x
fmapFC Block ext blocks r x -> CtxRepr x
forall ext (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType)
       (ctx :: Ctx CrucibleType).
Block ext blocks ret ctx -> CtxRepr ctx
forall (x :: Ctx CrucibleType).
Block ext blocks r x -> Assignment TypeRepr x
C.blockInputs (Assignment (Block ext blocks r) blocks
 -> Assignment (Assignment TypeRepr) blocks)
-> Assignment (Block ext blocks r) blocks
-> Assignment (Assignment TypeRepr) blocks
forall a b. (a -> b) -> a -> b
$ CallFrame sym ext blocks r args
-> Assignment (Block ext blocks r) blocks
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> BlockMap ext blocks ret
C.frameBlockMap CallFrame sym ext blocks r args
frame)
            , Just x :~: args
Refl <- BlockID blocks x -> BlockID blocks args -> Maybe (x :~: 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 x
breakpoint_block_id BlockID blocks args
BlockID blocks args
block_id
            , Just ret :~: r
Refl <- TypeRepr ret -> TypeRepr r -> Maybe (ret :~: r)
forall {k} (f :: k -> Type) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
forall (a :: CrucibleType) (b :: CrucibleType).
TypeRepr a -> TypeRepr b -> Maybe (a :~: b)
testEquality TypeRepr ret
ret_type (CallFrame sym ext blocks r args -> TypeRepr r
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> TypeRepr ret
C.frameReturnType CallFrame sym ext blocks r args
frame) -> do
              let override_frame :: SimFrame sym ext (OverrideLang ret) ('Just args)
override_frame = OverrideFrame sym ret args
-> SimFrame sym ext (OverrideLang ret) ('Just args)
forall sym (ret :: CrucibleType) (args1 :: Ctx CrucibleType) ext.
OverrideFrame sym ret args1
-> SimFrame sym ext (OverrideLang ret) ('Just args1)
C.OF (OverrideFrame sym ret args
 -> SimFrame sym ext (OverrideLang ret) ('Just args))
-> OverrideFrame sym ret args
-> SimFrame sym ext (OverrideLang ret) ('Just args)
forall a b. (a -> b) -> a -> b
$ C.OverrideFrame
                    { _override :: FunctionName
_override = Text -> FunctionName
W.functionNameFromText (Text -> FunctionName) -> Text -> FunctionName
forall a b. (a -> b) -> a -> b
$
                        BreakpointName -> Text
C.breakpointNameText BreakpointName
breakpoint_name
                    , _overrideHandle :: SomeHandle
_overrideHandle = CallFrame sym ext blocks r args -> SomeHandle
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType).
CallFrame sym ext blocks ret ctx -> SomeHandle
C.frameHandle CallFrame sym ext blocks r args
frame
                    , _overrideRegMap :: RegMap sym args
_overrideRegMap = SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
state SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Getting
     (RegMap sym args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     (RegMap sym args)
-> RegMap sym args
forall s a. s -> Getting a s a -> a
^.
                        (CallFrame sym ext blocks r args
 -> Const (RegMap sym args) (CallFrame sym ext blocks r args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Const
     (RegMap sym args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (a :: Ctx CrucibleType)
       (a' :: Ctx CrucibleType) (f :: Type -> Type).
Functor f =>
(CallFrame sym ext blocks r a -> f (CallFrame sym ext blocks r a'))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just a)
-> f (SimState p sym ext rtp (CrucibleLang blocks r) ('Just a'))
C.stateCrucibleFrame ((CallFrame sym ext blocks r args
  -> Const (RegMap sym args) (CallFrame sym ext blocks r args))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Const
      (RegMap sym args)
      (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)))
-> ((RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
    -> CallFrame sym ext blocks r args
    -> Const (RegMap sym args) (CallFrame sym ext blocks r args))
-> Getting
     (RegMap sym args)
     (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args))
     (RegMap sym args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RegMap sym args -> Const (RegMap sym args) (RegMap sym args))
-> CallFrame sym ext blocks r args
-> Const (RegMap sym args) (CallFrame sym ext blocks r args)
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)
C.frameRegs
                    }
              ExecState p sym ext rtp
result_state <- ReaderT
  (SimState p sym ext rtp (OverrideLang ret) ('Just args))
  IO
  (ExecState p sym ext rtp)
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> IO (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT (TypeRepr ret
-> OverrideSim p sym ext rtp args ret (RegValue sym ret)
-> ReaderT
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
     IO
     (ExecState p sym ext rtp)
forall (tp :: CrucibleType) p sym ext rtp
       (args :: Ctx CrucibleType).
TypeRepr tp
-> OverrideSim p sym ext rtp args tp (RegValue sym tp)
-> ExecCont p sym ext rtp (OverrideLang tp) ('Just args)
C.runOverrideSim TypeRepr ret
ret_type OverrideSim p sym ext rtp args ret (RegValue sym ret)
override) (SimState p sym ext rtp (OverrideLang ret) ('Just args)
 -> IO (ExecState p sym ext rtp))
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> IO (ExecState p sym ext rtp)
forall a b. (a -> b) -> a -> b
$
                SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
state SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> (SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
    -> SimState p sym ext rtp (OverrideLang ret) ('Just args))
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
forall a b. a -> (a -> b) -> b
& (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Identity
      (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> Identity
     (SimState p sym ext rtp (OverrideLang ret) ('Just args))
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: Type -> Type).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
C.stateTree ((ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)
  -> Identity
       (ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)))
 -> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
 -> Identity
      (SimState p sym ext rtp (OverrideLang ret) ('Just args)))
-> (ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)
    -> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args))
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
%~
                  ReturnHandler
  (FrameRetType (OverrideLang ret))
  p
  sym
  ext
  rtp
  (CrucibleLang blocks r)
  ('Just args)
-> SimFrame sym ext (OverrideLang ret) ('Just args)
-> ActiveTree p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ActiveTree p sym ext rtp (OverrideLang ret) ('Just args)
forall a p sym ext r f (old_args :: Maybe (Ctx CrucibleType))
       (args :: Maybe (Ctx CrucibleType)).
ReturnHandler (FrameRetType a) p sym ext r f old_args
-> SimFrame sym ext a args
-> ActiveTree p sym ext r f old_args
-> ActiveTree p sym ext r a args
C.pushCallFrame ReturnHandler
  ret p sym ext rtp (CrucibleLang blocks r) ('Just args)
ReturnHandler
  (FrameRetType (OverrideLang ret))
  p
  sym
  ext
  rtp
  (CrucibleLang blocks r)
  ('Just args)
forall (ret :: CrucibleType) (r :: CrucibleType) p sym ext root
       (blocks :: Ctx (Ctx CrucibleType))
       (args :: Maybe (Ctx CrucibleType)).
(ret ~ r) =>
ReturnHandler ret p sym ext root (CrucibleLang blocks r) args
C.TailReturnToCrucible SimFrame sym ext (OverrideLang ret) ('Just args)
SimFrame sym ext (OverrideLang ret) ('Just args)
override_frame
              ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecutionFeatureResult p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNewState ExecState p sym ext rtp
result_state
          C.CallState ReturnHandler ret p sym ext rtp f a
return_handler (C.CrucibleCall BlockID blocks args
block_id CallFrame sym ext blocks ret args
frame) SimState p sym ext rtp f a
state
            | Just [BreakpointName]
breakpoints <- SomeHandle
-> HashMap SomeHandle [BreakpointName] -> Maybe [BreakpointName]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup
                (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
C.frameHandle CallFrame sym ext blocks ret args
frame)
                HashMap SomeHandle [BreakpointName]
all_breakpoints -> do
              let result_frame :: CallFrame sym ext blocks ret args
result_frame = [BreakpointName]
-> CallFrame sym ext blocks ret args
-> CallFrame sym ext blocks ret args
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
C.setFrameBreakpointPostdomInfo
                    [BreakpointName]
breakpoints
                    CallFrame sym ext blocks ret args
frame
              ExecState p sym ext rtp
result_state <- ReaderT (SimState p sym ext rtp f a) IO (ExecState p sym ext rtp)
-> SimState p sym ext rtp f a -> IO (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT
                (ReturnHandler ret p sym ext rtp f a
-> ResolvedCall p sym ext ret
-> ReaderT
     (SimState p sym ext rtp f a) IO (ExecState p sym ext rtp)
forall sym (ret :: CrucibleType) p ext rtp outer_frame
       (outer_args :: Maybe (Ctx CrucibleType)).
IsSymInterface sym =>
ReturnHandler ret p sym ext rtp outer_frame outer_args
-> ResolvedCall p sym ext ret
-> ExecCont p sym ext rtp outer_frame outer_args
C.performFunctionCall
                  ReturnHandler ret p sym ext rtp f a
return_handler
                  (BlockID blocks args
-> CallFrame sym ext blocks ret args -> ResolvedCall p sym ext ret
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) sym ext (ret :: CrucibleType) p.
BlockID blocks args
-> CallFrame sym ext blocks ret args -> ResolvedCall p sym ext ret
C.CrucibleCall BlockID blocks args
block_id CallFrame sym ext blocks ret args
result_frame))
                SimState p sym ext rtp f a
state
              ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecutionFeatureResult p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNewState ExecState p sym ext rtp
result_state
          C.TailCallState ValueFromValue p sym ext rtp ret
value_from_value (C.CrucibleCall BlockID blocks args
block_id CallFrame sym ext blocks ret args
frame) SimState p sym ext rtp f a
state
            | Just [BreakpointName]
breakpoints <- SomeHandle
-> HashMap SomeHandle [BreakpointName] -> Maybe [BreakpointName]
forall k v. (Eq k, Hashable k) => k -> HashMap k v -> Maybe v
HashMap.lookup
                (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
C.frameHandle CallFrame sym ext blocks ret args
frame)
                HashMap SomeHandle [BreakpointName]
all_breakpoints -> do
              let result_frame :: CallFrame sym ext blocks ret args
result_frame = [BreakpointName]
-> CallFrame sym ext blocks ret args
-> CallFrame sym ext blocks ret args
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
C.setFrameBreakpointPostdomInfo
                    [BreakpointName]
breakpoints
                    CallFrame sym ext blocks ret args
frame
              ExecState p sym ext rtp
result_state <- ReaderT (SimState p sym ext rtp f a) IO (ExecState p sym ext rtp)
-> SimState p sym ext rtp f a -> IO (ExecState p sym ext rtp)
forall r (m :: Type -> Type) a. ReaderT r m a -> r -> m a
runReaderT
                (ValueFromValue p sym ext rtp ret
-> ResolvedCall p sym ext ret
-> ReaderT
     (SimState p sym ext rtp f a) IO (ExecState p sym ext rtp)
forall sym p ext rtp (ret :: CrucibleType) f
       (a :: Maybe (Ctx CrucibleType)).
IsSymInterface sym =>
ValueFromValue p sym ext rtp ret
-> ResolvedCall p sym ext ret -> ExecCont p sym ext rtp f a
C.performTailCall
                  ValueFromValue p sym ext rtp ret
value_from_value
                  (BlockID blocks args
-> CallFrame sym ext blocks ret args -> ResolvedCall p sym ext ret
forall (blocks :: Ctx (Ctx CrucibleType))
       (args :: Ctx CrucibleType) sym ext (ret :: CrucibleType) p.
BlockID blocks args
-> CallFrame sym ext blocks ret args -> ResolvedCall p sym ext ret
C.CrucibleCall BlockID blocks args
block_id CallFrame sym ext blocks ret args
result_frame))
                SimState p sym ext rtp f a
state
              ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (ExecutionFeatureResult p sym ext rtp
 -> IO (ExecutionFeatureResult p sym ext rtp))
-> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNewState ExecState p sym ext rtp
result_state
          ExecState p sym ext rtp
_ -> ExecutionFeatureResult p sym ext rtp
-> IO (ExecutionFeatureResult p sym ext rtp)
forall a. a -> IO a
forall (m :: Type -> Type) a. Monad m => a -> m a
return ExecutionFeatureResult p sym ext rtp
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNoChange
    Maybe (Some (BlockID blocks))
_ -> String -> IO (ExecutionFeature p sym ext rtp)
forall a. String -> IO a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String -> IO (ExecutionFeature p sym ext rtp))
-> String -> IO (ExecutionFeature p sym ext rtp)
forall a b. (a -> b) -> a -> b
$ String
"unexpected breakpoint: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ BreakpointName -> String
forall a. Show a => a -> String
show BreakpointName
breakpoint_name