content: -----------------------------------------------------------------------
  -- |
  -- 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 C.CFG{..} breakpoint_name arg_types ret_type override all_breakpoints =
    case Bimap.lookup breakpoint_name cfgBreakpoints of
      Just (Some breakpoint_block_id)
        | breakpoint_block <- C.getBlock breakpoint_block_id cfgBlockMap
        , Just Refl <- testEquality (C.blockInputs breakpoint_block) arg_types ->
          return $ C.ExecutionFeature $ \case
            C.RunningState (C.RunPostBranchMerge block_id) state
              | frame <- state ^. C.stateCrucibleFrame
              , C.SomeHandle cfgHandle == C.frameHandle frame
              , Just Refl <- testEquality
                  (fmapFC C.blockInputs cfgBlockMap)
                  (fmapFC C.blockInputs $ C.frameBlockMap frame)
              , Just Refl <- testEquality breakpoint_block_id block_id
              , Just Refl <- testEquality ret_type (C.frameReturnType frame) -> do
                let override_frame = C.OF $ C.OverrideFrame
                      { _override = W.functionNameFromText $
                          C.breakpointNameText breakpoint_name
                      , _overrideHandle = C.frameHandle frame
                      , _overrideRegMap = state ^.
                          C.stateCrucibleFrame . C.frameRegs
                      }
                result_state <- runReaderT (C.runOverrideSim ret_type override) $
                  state & C.stateTree %~
                    C.pushCallFrame C.TailReturnToCrucible override_frame
                return $ C.ExecutionFeatureNewState result_state
            C.CallState return_handler (C.CrucibleCall block_id frame) state
              | Just breakpoints <- HashMap.lookup
                  (C.frameHandle frame)
                  all_breakpoints -> do
                let result_frame = C.setFrameBreakpointPostdomInfo
                      breakpoints
                      frame
                result_state <- runReaderT
                  (C.performFunctionCall
                    return_handler
                    (C.CrucibleCall block_id result_frame))
                  state
                return $ C.ExecutionFeatureNewState result_state
            C.TailCallState value_from_value (C.CrucibleCall block_id frame) state
              | Just breakpoints <- HashMap.lookup
                  (C.frameHandle frame)
                  all_breakpoints -> do
                let result_frame = C.setFrameBreakpointPostdomInfo
                      breakpoints
                      frame
                result_state <- runReaderT
                  (C.performTailCall
                    value_from_value
                    (C.CrucibleCall block_id result_frame))
                  state
                return $ C.ExecutionFeatureNewState result_state
            _ -> return C.ExecutionFeatureNoChange
      _ -> fail $ "unexpected breakpoint: " ++ show breakpoint_name
  