-----------------------------------------------------------------------
-- |
-- Module           : Lang.Crucible.Simulator.Cut
-- Description      : Support for symbolic execution cuts
-- 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
-- cutpoints.
-----------------------------------------------------------------------
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE RecordWildCards #-}
module Lang.Crucible.Simulator.Cut
  ( cutAndReturn
  ) where

import           Control.Monad.Reader
import qualified Data.Bimap as Bimap
import           Data.Function ((&))
import           Data.HashMap.Strict (HashMap)
import qualified Data.HashMap.Strict as HashMap
import           Lens.Micro ((^.), (%~))

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 cutpoint.
--   The override summarizes the execution from the cutpoint
--   to the return from the function (similar to a tail call).
--   This feature requires a map from each function handle
--   to the list of cutpoints in the respective function with this
--   execution feature.
cutAndReturn ::
  (C.IsSymInterface sym, C.IsSyntaxExtension ext) =>
  C.CFG ext blocks init ret ->
  C.CutpointName ->
  Ctx.Assignment C.TypeRepr args ->
  C.TypeRepr ret ->
  C.OverrideSim p sym ext rtp args ret (C.RegValue sym ret) ->
  HashMap C.SomeHandle [C.CutpointName] ->
  IO (C.ExecutionFeature p sym ext rtp)
cutAndReturn :: 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
-> CutpointName
-> Assignment TypeRepr args
-> TypeRepr ret
-> OverrideSim p sym ext rtp args ret (RegValue sym ret)
-> HashMap SomeHandle [CutpointName]
-> IO (ExecutionFeature p sym ext rtp)
cutAndReturn C.CFG{Bimap CutpointName (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
cfgCutpoints :: Bimap CutpointName (Some (BlockID blocks))
cfgCutpoints :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret
-> Bimap CutpointName (Some (BlockID blocks))
cfgEntryBlockID :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockID blocks init
cfgBlockMap :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> BlockMap ext blocks ret
cfgHandle :: forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> FnHandle init ret
..} CutpointName
cutpoint_name Assignment TypeRepr args
arg_types TypeRepr ret
ret_type OverrideSim p sym ext rtp args ret (RegValue sym ret)
override HashMap SomeHandle [CutpointName]
all_cutpoints =
  case CutpointName
-> Bimap CutpointName (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 CutpointName
cutpoint_name Bimap CutpointName (Some (BlockID blocks))
cfgCutpoints of
    Just (Some BlockID blocks x
cutpoint_block_id)
      | Block ext blocks ret x
cutpoint_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
cutpoint_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
cutpoint_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
cutpoint_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
$
                        CutpointName -> Text
C.cutpointNameText CutpointName
cutpoint_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 [CutpointName]
cutpoints <- SomeHandle
-> HashMap SomeHandle [CutpointName] -> Maybe [CutpointName]
forall k v. 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 [CutpointName]
all_cutpoints -> do
              let result_frame :: CallFrame sym ext blocks ret args
result_frame = [CutpointName]
-> CallFrame sym ext blocks ret args
-> CallFrame sym ext blocks ret args
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType).
[CutpointName]
-> CallFrame sym ext blocks ret ctx
-> CallFrame sym ext blocks ret ctx
C.setFrameCutpointPostdomInfo
                    [CutpointName]
cutpoints
                    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 [CutpointName]
cutpoints <- SomeHandle
-> HashMap SomeHandle [CutpointName] -> Maybe [CutpointName]
forall k v. 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 [CutpointName]
all_cutpoints -> do
              let result_frame :: CallFrame sym ext blocks ret args
result_frame = [CutpointName]
-> CallFrame sym ext blocks ret args
-> CallFrame sym ext blocks ret args
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (ctx :: Ctx CrucibleType).
[CutpointName]
-> CallFrame sym ext blocks ret ctx
-> CallFrame sym ext blocks ret ctx
C.setFrameCutpointPostdomInfo
                    [CutpointName]
cutpoints
                    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 cutpoint: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ CutpointName -> String
forall a. Show a => a -> String
show CutpointName
cutpoint_name