content: -----------------------------------------------------------------------
  -- |
  -- Module           : Lang.Crucible.Simulator.Operations
  -- Description      : Basic operations on execution trees
  -- Copyright        : (c) Galois, Inc 2014-2018
  -- License          : BSD3
  -- Maintainer       : Joe Hendrix <jhendrix@galois.com>
  -- Stability        : provisional
  --
  -- Operations corresponding to basic control-flow events on
  -- simulator execution trees.
  ------------------------------------------------------------------------
  
  {-# LANGUAGE ConstraintKinds #-}
  {-# LANGUAGE DataKinds #-}
  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE FlexibleInstances #-}
  {-# LANGUAGE GADTs #-}
  {-# LANGUAGE KindSignatures #-}
  {-# LANGUAGE LambdaCase #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  {-# LANGUAGE OverloadedStrings #-}
  {-# LANGUAGE PatternGuards #-}
  {-# LANGUAGE PolyKinds #-}
  {-# LANGUAGE RankNTypes #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE TypeApplications #-}
  {-# LANGUAGE TypeFamilies #-}
  {-# LANGUAGE TypeOperators #-}
  {-# LANGUAGE ViewPatterns #-}
  {-# OPTIONS_GHC -fprint-explicit-kinds -Wall #-}
  module Lang.Crucible.Simulator.Operations
    ( -- * Control-flow operations
      continue
    , jumpToBlock
    , conditionalBranch
    , variantCases
    , returnValue
    , callFunction
    , tailCallFunction
    , runOverride
    , runAbortHandler
    , runErrorHandler
    , runGenericErrorHandler
    , performIntraFrameMerge
    , performIntraFrameSplit
    , performFunctionCall
    , performTailCall
    , performReturn
    , performControlTransfer
    , resumeFrame
    , resumeValueFromValueAbort
    , overrideSymbolicBranch
  
      -- * Resolving calls
    , ResolvedCall(..)
    , UnresolvableFunction(..)
    , resolveCall
    , resolvedCallName
  
      -- * Abort handlers
    , abortExecAndLog
    , abortExec
    , defaultAbortHandler
  
      -- * Call tree manipulations
    , pushCallFrame
    , replaceTailFrame
    , isSingleCont
    , unwindContext
    , extractCurrentPath
    , asContFrame
    , forgetPostdomFrame
    ) where
  
  import Prelude hiding (pred)
  
  import qualified Control.Exception as Ex
  import           Control.Lens
  import           Control.Monad (when, void)
  import           Control.Monad.IO.Class (MonadIO(..))
  import           Control.Monad.Reader (ReaderT(..), withReaderT)
  import           Control.Monad.Trans.Class (MonadTrans(..))
  import           Data.Maybe (fromMaybe)
  import           Data.List (isPrefixOf)
  import qualified Data.Parameterized.Context as Ctx
  import           Data.Parameterized.Some
  import qualified Data.Vector as V
  import           Data.Type.Equality hiding (sym)
  import           System.IO
  import qualified Prettyprinter as PP
  
  import           What4.Config
  import           What4.Interface
  import           What4.FunctionName
  import           What4.ProgramLoc
  
  import           Lang.Crucible.Backend
  import           Lang.Crucible.CFG.Core
  import           Lang.Crucible.CFG.Extension
  import           Lang.Crucible.FunctionHandle
  import           Lang.Crucible.Panic(panic)
  import           Lang.Crucible.Simulator.CallFrame
  import           Lang.Crucible.Simulator.ExecutionTree
  import           Lang.Crucible.Simulator.GlobalState
  import           Lang.Crucible.Simulator.Intrinsics
  import           Lang.Crucible.Simulator.RegMap
  import           Lang.Crucible.Simulator.SimError
  
  ---------------------------------------------------------------------
  -- Intermediate state branching/merging
  
  -- | Merge two globals together.
  mergeGlobalPair ::
    MuxFn p v ->
    MuxFn p (SymGlobalState sym) ->
    MuxFn p (GlobalPair sym v)
  mergeGlobalPair merge_fn global_fn c x y =
    GlobalPair <$> merge_fn  c (x^.gpValue) (y^.gpValue)
               <*> global_fn c (x^.gpGlobals) (y^.gpGlobals)
  
  mergeAbortedResult ::
    ProgramLoc {- ^ Program location of control-flow branching -} ->
    Pred sym {- ^ Branch predicate -} ->
    AbortedResult sym ext ->
    AbortedResult sym ext ->
    AbortedResult sym ext
  mergeAbortedResult _ _ ae@(AbortedExit {}) _ = ae
  mergeAbortedResult _ _ _ ae@(AbortedExit {}) = ae
  mergeAbortedResult loc pred q r = AbortedBranch loc pred q r
  
  mergePartialAndAbortedResult ::
    IsExprBuilder sym =>
    sym ->
    ProgramLoc {- ^ Program location of control-flow branching -} ->
    Pred sym {- ^ This needs to hold to avoid the aborted result -} ->
    PartialResult sym ext v ->
    AbortedResult sym ext ->
    IO (PartialResult sym ext v)
  mergePartialAndAbortedResult sym loc pred ar r = do
    case ar of
      TotalRes gp -> return $! PartialRes loc pred gp r
      PartialRes loc' d gp q ->
        do e <- andPred sym pred d
           return $! PartialRes loc' e gp (mergeAbortedResult loc pred q r)
  
  
  mergeCrucibleFrame ::
    IsSymInterface sym =>
    sym ->
    IntrinsicTypes sym ->
    CrucibleBranchTarget f args {- ^ Target of branch -} ->
    MuxFn (Pred sym) (SimFrame sym ext f args)
  mergeCrucibleFrame sym muxFns tgt p x0 y0 =
    case tgt of
      BlockTarget _b_id -> do
        let x = fromCallFrame x0
        let y = fromCallFrame y0
        z <- mergeRegs sym muxFns p (x^.frameRegs) (y^.frameRegs)
        pure $! MF (x & frameRegs .~ z)
      ReturnTarget -> do
        let x = fromReturnFrame x0
        let y = fromReturnFrame y0
        RF (x0^.frameFunctionName) <$> muxRegEntry sym muxFns p x y
  
  
  mergePartialResult ::
    IsSymInterface sym =>
    SimState p sym ext root f args ->
    CrucibleBranchTarget f args ->
    MuxFn (Pred sym) (PartialResultFrame sym ext f args)
  mergePartialResult s tgt pred x y =
    let sym       = s^.stateSymInterface
        iteFns    = s^.stateIntrinsicTypes
        merge_val = mergeCrucibleFrame sym iteFns tgt
        merge_fn  = mergeGlobalPair merge_val (globalMuxFn sym iteFns)
    in
    case x of
      TotalRes cx ->
        case y of
          TotalRes cy ->
            TotalRes <$> merge_fn pred cx cy
  
          PartialRes loc py cy fy ->
            PartialRes loc <$> orPred sym pred py
                           <*> merge_fn pred cx cy
                           <*> pure fy
  
      PartialRes loc px cx fx ->
        case y of
          TotalRes cy ->
            do pc <- notPred sym pred
               PartialRes loc <$> orPred sym pc px
                              <*> merge_fn pred cx cy
                              <*> pure fx
  
          PartialRes loc' py cy fy ->
            PartialRes loc' <$> itePred sym pred px py
                            <*> merge_fn pred cx cy
                            <*> pure (AbortedBranch loc' pred fx fy)
  
  forgetPostdomFrame ::
    PausedFrame p sym ext rtp g ->
    PausedFrame p sym ext rtp g
  forgetPostdomFrame (PausedFrame frm cont loc) = PausedFrame frm (f cont) loc
    where
    f (CheckMergeResumption jmp) = ContinueResumption jmp
    f x = x
  
  
  pushPausedFrame ::
    IsSymInterface sym =>
    PausedFrame p sym ext rtp g ->
    ReaderT (SimState p sym ext rtp f ma) IO (PausedFrame p sym ext rtp g)
  pushPausedFrame (PausedFrame frm res loc) =
    do sym <- view stateSymInterface
       iTypes <- view stateIntrinsicTypes
       frm' <- lift (frm & traverseOf (partialValue.gpGlobals) (globalPushBranch sym iTypes))
       res' <- lift (pushControlResumption sym iTypes res)
       return (PausedFrame frm' res' loc)
  
  pushControlResumption ::
    IsSymInterface sym =>
    sym ->
    IntrinsicTypes sym ->
    ControlResumption p sym ext rtp g ->
    IO (ControlResumption p sym ext rtp g)
  pushControlResumption sym iTypes res =
    case res of
      ContinueResumption jmp ->
        ContinueResumption <$> pushResolvedJump sym iTypes jmp
      CheckMergeResumption jmp ->
        CheckMergeResumption <$> pushResolvedJump sym iTypes jmp
      SwitchResumption ps ->
        SwitchResumption <$> (traverse._2) (pushResolvedJump sym iTypes) ps
      OverrideResumption k args ->
        OverrideResumption k <$> pushBranchRegs sym iTypes args
  
  pushResolvedJump ::
    IsSymInterface sym =>
    sym ->
    IntrinsicTypes sym ->
    ResolvedJump sym branches ->
    IO (ResolvedJump sym branches)
  pushResolvedJump sym iTypes (ResolvedJump block_id args) =
    ResolvedJump block_id <$> pushBranchRegs sym iTypes args
  
  
  abortCrucibleFrame ::
    IsSymInterface sym =>
    sym ->
    IntrinsicTypes sym ->
    CrucibleBranchTarget f a' ->
    SimFrame sym ext f a' ->
    IO (SimFrame sym ext f a')
  abortCrucibleFrame sym intrinsicFns (BlockTarget _) (MF x') =
    do r' <- abortBranchRegs sym intrinsicFns (x'^.frameRegs)
       return $! MF (x' & frameRegs .~ r')
  
  abortCrucibleFrame sym intrinsicFns ReturnTarget (RF nm x') =
    RF nm <$> abortBranchRegEntry sym intrinsicFns x'
  
  
  abortPartialResult ::
    IsSymInterface sym =>
    SimState p sym ext r f args ->
    CrucibleBranchTarget f a' ->
    PartialResultFrame sym ext f a' ->
    IO (PartialResultFrame sym ext f a')
  abortPartialResult s tgt pr =
    let sym                    = s^.stateSymInterface
        muxFns                 = s^.stateIntrinsicTypes
        abtGp (GlobalPair v g) = GlobalPair <$> abortCrucibleFrame sym muxFns tgt v
                                            <*> globalAbortBranch sym muxFns g
    in partialValue abtGp pr
  
  
  ------------------------------------------------------------------------
  -- resolveCall
  
  -- | This exception is thrown if a 'FnHandle' cannot be resolved to
  --   a callable function.  This usually indicates a programming error,
  --   but might also be used to allow on-demand function loading.
  --
  --   The 'ProgramLoc' argument references the call site for the unresolved
  --   function call.
  --
  --   The @['SomeFrame']@ argument is the active call stack at the time of
  --   the exception.
  data UnresolvableFunction where
    UnresolvableFunction ::
      !(ProgramLoc) ->
      [SomeFrame (SimFrame sym ext)] ->
      !(FnHandle args ret) ->
      UnresolvableFunction
  
  instance Ex.Exception UnresolvableFunction
  instance Show UnresolvableFunction where
    show (UnresolvableFunction loc callStack h) =
      let name = show $ handleName h
      in unlines $
           if "llvm" `isPrefixOf` name
           then [ "Encountered unresolved LLVM intrinsic '" ++ name ++ "'"
                , "Please report this on the following issue:"
                , "https://github.com/GaloisInc/crucible/issues/73"
                ] ++ [ show (ppExceptionContext callStack) ]
           else [ "Could not resolve function: " ++ name
                , "Called at: " ++ show (PP.pretty (plSourceLoc loc))
                ] ++ [ show (ppExceptionContext callStack) ]
  
  
  -- | Utility function that packs the tail of a collection of arguments
  --   into a vector of ANY type values for passing to varargs functions.
  packVarargs ::
    CtxRepr addlArgs ->
    RegMap sym (args <+> addlArgs) ->
    RegMap sym (args ::> VectorType AnyType)
  
  packVarargs = go mempty
   where
   go ::
    V.Vector (AnyValue sym) ->
    CtxRepr addlArgs ->
    RegMap sym (args <+> addlArgs) ->
    RegMap sym (args ::> VectorType AnyType)
  
   go v (addl Ctx.:> tp) (unconsReg -> (args, x)) =
     go (V.cons (AnyValue tp (regValue x)) v) addl args
  
   go v Ctx.Empty args =
     assignReg knownRepr v args
  
  -- | Given a set of function bindings, a function-
  --   value (which is possibly a closure) and a
  --   collection of arguments, resolve the identity
  --   of the function to call, and set it up to be called.
  --
  --   Will throw an 'UnresolvableFunction' exception if
  --   the underlying function handle is not found in the
  --   'FunctionBindings' map.
  resolveCall ::
    FunctionBindings p sym ext {- ^ Map from function handles to semantics -} ->
    FnVal sym args ret {- ^ Function handle and any closure variables -} ->
    RegMap sym args {- ^ Arguments to the function -} ->
    ProgramLoc {- ^ Location of the call -} ->
    [SomeFrame (SimFrame sym ext)] {-^ current call stack (for exceptions) -} ->
    ResolvedCall p sym ext ret
  resolveCall bindings c0 args loc callStack =
    case c0 of
      ClosureFnVal c tp v -> do
        resolveCall bindings c (assignReg tp v args) loc callStack
  
      VarargsFnVal h addlTypes ->
        resolveCall bindings (HandleFnVal h) (packVarargs addlTypes args) loc callStack
  
      HandleFnVal h -> do
        case lookupHandleMap h (fnBindings bindings) of
          Nothing -> Ex.throw (UnresolvableFunction loc callStack h)
          Just (UseOverride o) -> do
            let f = OverrideFrame { _override = overrideName o
                                  , _overrideHandle = SomeHandle h
                                  , _overrideRegMap = args
                                  }
             in OverrideCall o f
          Just (UseCFG g pdInfo) -> do
            CrucibleCall (cfgEntryBlockID g) (mkCallFrame g pdInfo args)
  
  
  resolvedCallName :: ResolvedCall p sym ext ret -> FunctionName
  resolvedCallName (OverrideCall _ f) = f^.override
  resolvedCallName (CrucibleCall _ f) = case frameHandle f of SomeHandle h -> handleName h
  
  ---------------------------------------------------------------------
  -- Control-flow operations
  
  -- | Immediately transtition to an 'OverrideState'.  On the next
  --   execution step, the simulator will execute the given override.
  runOverride ::
    Override p sym ext args ret {- ^ Override to execute -} ->
    ExecCont p sym ext rtp (OverrideLang ret) ('Just args)
  runOverride o = ReaderT (return . OverrideState o)
  
  -- | Immediately transition to a 'RunningState'.  On the next
  --   execution step, the simulator will interpret the next basic
  --   block.
  continue :: RunningStateInfo blocks a -> ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just a)
  continue rtgt = ReaderT (return . RunningState rtgt)
  
  -- | Immediately transition to an 'AbortState'.  On the next
  --   execution step, the simulator will unwind the 'SimState'
  --   and resolve the abort.
  runAbortHandler ::
    AbortExecReason {- ^ Description of the abort condition -} ->
    SimState p sym ext rtp f args {- ^ Simulator state prior to the abort -} ->
    IO (ExecState p sym ext rtp)
  runAbortHandler rsn s = return (AbortState rsn s)
  
  -- | Abort the current thread of execution with an error.
  --   This adds a proof obligation that requires the current
  --   execution path to be infeasible, and unwids to the
  --   nearest branch point to resume.
  runErrorHandler ::
    SimErrorReason {- ^ Description of the error -} ->
    SimState p sym ext rtp f args {- ^ Simulator state prior to the abort -} ->
    IO (ExecState p sym ext rtp)
  runErrorHandler msg st =
    let ctx = st^.stateContext
        sym = ctx^.ctxSymInterface
     in withBackend ctx $ \bak ->
        do loc <- getCurrentProgramLoc sym
           let err = SimError loc msg
           addProofObligation bak (LabeledPred (falsePred sym) err)
           return (AbortState (AssertionFailure err) st)
  
  -- | Abort the current thread of execution with an error.
  --   This adds a proof obligation that requires the current
  --   execution path to be infeasible, and unwids to the
  --   nearest branch point to resume.
  runGenericErrorHandler ::
    String {- ^ Generic description of the error condition -} ->
    SimState p sym ext rtp f args {- ^ Simulator state prior to the abort -} ->
    IO (ExecState p sym ext rtp)
  runGenericErrorHandler msg st = runErrorHandler (GenericSimError msg) st
  
  -- | Transfer control to the given resolved jump, after first
  --   checking for any pending symbolic merges at the destination
  --   of the jump.
  jumpToBlock ::
    IsSymInterface sym =>
    ResolvedJump sym blocks {- ^ Jump target and arguments -} ->
    ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just a)
  jumpToBlock jmp = ReaderT $ return . ControlTransferState (CheckMergeResumption jmp)
  {-# INLINE jumpToBlock #-}
  
  performControlTransfer ::
    IsSymInterface sym =>
    ControlResumption p sym ext rtp f ->
    ExecCont p sym ext rtp f ('Just a)
  performControlTransfer res =
    case res of
      ContinueResumption (ResolvedJump block_id args) ->
        withReaderT
          (stateCrucibleFrame %~ setFrameBlock block_id args)
          (continue (RunBlockStart block_id))
      CheckMergeResumption (ResolvedJump block_id args) ->
        withReaderT
          (stateCrucibleFrame %~ setFrameBlock block_id args)
          (checkForIntraFrameMerge (BlockTarget block_id))
      SwitchResumption cs ->
        variantCases cs
      OverrideResumption k args ->
        withReaderT
          (stateOverrideFrame.overrideRegMap .~ args)
          k
  
  -- | Perform a conditional branch on the given predicate.
  --   If the predicate is symbolic, this will record a symbolic
  --   branch state.
  conditionalBranch ::
    (IsSymInterface sym, IsSyntaxExtension ext) =>
    Pred sym {- ^ Predicate to branch on -} ->
    ResolvedJump sym blocks {- ^ True branch -} ->
    ResolvedJump sym blocks {- ^ False branch -} ->
    ExecCont p sym ext rtp (CrucibleLang blocks ret) ('Just ctx)
  conditionalBranch p xjmp yjmp = do
    top_frame <- view (stateTree.actFrame)
    Some pd <- return (top_frame^.crucibleTopFrame.framePostdom)
  
    x_frame <- cruciblePausedFrame xjmp top_frame pd
    y_frame <- cruciblePausedFrame yjmp top_frame pd
  
    intra_branch p x_frame y_frame pd
  
  -- | Execute the next branch of a sequence of branch cases.
  --   These arise from the implementation of the 'VariantElim'
  --   construct.  The predicates are expected to be mutually
  --   disjoint.  However, the construct still has well defined
  --   semantics even in the case where they overlap; in this case,
  --   the first branch with a true 'Pred' is taken.  In other words,
  --   each branch assumes the negation of all the predicates of branches
  --   appearing before it.
  --
  --   In the final default case (corresponding to an empty list of branches),
  --   a 'VariantOptionsExhausted' abort will be executed.
  variantCases ::
    IsSymInterface sym =>
    [(Pred sym, ResolvedJump sym blocks)] {- ^ Variant branches to execute -} ->
    ExecCont p sym ext rtp (CrucibleLang blocks r) ('Just ctx)
  
  variantCases [] =
    do fm <- view stateCrucibleFrame
       let loc = frameProgramLoc fm
       let rsn = VariantOptionsExhausted loc
       abortExec rsn
  
  variantCases ((p,jmp) : cs) =
    do top_frame <- view (stateTree.actFrame)
       Some pd <- return (top_frame^.crucibleTopFrame.framePostdom)
  
       x_frame <- cruciblePausedFrame jmp top_frame pd
       let y_frame = PausedFrame (TotalRes top_frame) (SwitchResumption cs) Nothing
  
       intra_branch p x_frame y_frame pd
  
  -- | Return a value from current Crucible execution.
  returnValue :: forall p sym ext rtp f args.
    RegEntry sym (FrameRetType f) {- ^ return value -} ->
    ExecCont p sym ext rtp f args
  returnValue arg =
    do nm <- view (stateTree.actFrame.gpValue.frameFunctionName)
       withReaderT
         (stateTree.actFrame.gpValue .~ RF nm arg)
         (checkForIntraFrameMerge ReturnTarget)
  
  
  callFunction ::
    IsExprBuilder sym =>
    FnVal sym args ret {- ^ Function handle and any closure variables -} ->
    RegMap sym args {- ^ Arguments to the function -} ->
    ReturnHandler ret p sym ext rtp f a {- ^ How to modify the caller's scope with the return value -} ->
    ProgramLoc {-^ location of call -} ->
    ExecCont p sym ext rtp f a
  callFunction fn args retHandler loc =
    do bindings <- view (stateContext.functionBindings)
       callStack <- view (stateTree . to activeFrames)
       let rcall = resolveCall bindings fn args loc callStack
       ReaderT $ return . CallState retHandler rcall
  
  tailCallFunction ::
    FrameRetType f ~ ret =>
    FnVal sym args ret {- ^ Function handle and any closure variables -} ->
    RegMap sym args {- ^ Arguments to the function -} ->
    ValueFromValue p sym ext rtp ret ->
    ProgramLoc {-^ location of call -} ->
    ExecCont p sym ext rtp f a
  tailCallFunction fn args vfv loc =
    do bindings <- view (stateContext.functionBindings)
       callStack <- view (stateTree . to activeFrames)
       let rcall = resolveCall bindings fn args loc callStack
       ReaderT $ return . TailCallState vfv rcall
  
  
  -- | Immediately transition to the 'BranchMergeState'.
  --   On the next simulator step, this will checks for the
  --   opportunity to merge within a frame.
  --
  --   This should be called everytime the current control flow location
  --   changes to a potential merge point.
  checkForIntraFrameMerge ::
    CrucibleBranchTarget f args
      {- ^ The location of the block we are transferring to -} ->
    ExecCont p sym ext root f args
  
  checkForIntraFrameMerge tgt =
    ReaderT $ return . BranchMergeState tgt
  
  
  assumeInNewFrame ::
    IsSymBackend sym bak =>
    bak ->
    Assumption sym ->
    IO FrameIdentifier
  assumeInNewFrame bak asm =
    do frm <- pushAssumptionFrame bak
       Ex.try @Ex.SomeException (addAssumption bak asm) >>= \case
         Left ex ->
           do void $ popAssumptionFrame bak frm
              Ex.throw ex
         Right () -> return frm
  
  -- | Perform a single instance of path merging at a join point.
  --   This will resume an alternate branch, if it is pending,
  --   or merge result values if a completed branch has alread reached
  --   this point. If there are no pending merge points at this location,
  --   continue executing by transfering control to the given target.
  performIntraFrameMerge ::
    IsSymInterface sym =>
    CrucibleBranchTarget f args
      {- ^ The location of the block we are transferring to -} ->
    ExecCont p sym ext root f args
  
  performIntraFrameMerge tgt = do
    ActiveTree ctx0 er <- view stateTree
    simCtx <- view stateContext
    sym <- view stateSymInterface
    withBackend simCtx $ \bak ->
      case ctx0 of
        VFFBranch ctx assume_frame loc pred other_branch tgt'
  
          -- Did we get to our merge point (i.e., we are finished with this branch)
          | Just Refl <- testEquality tgt tgt' ->
            case other_branch of
  
              -- We still have some more work to do, reactivate the other, postponed branch
              VFFActivePath next ->
                do pathAssumes      <- liftIO $ popAssumptionFrame bak assume_frame
                   pnot             <- liftIO $ notPred sym pred
                   new_assume_frame <-
                      liftIO $ assumeInNewFrame bak (BranchCondition loc (pausedLoc next) pnot)
  
                   -- The current branch is done
                   let new_other = VFFCompletePath pathAssumes er
                   resumeFrame next (VFFBranch ctx new_assume_frame loc pnot new_other tgt)
  
              -- We are done with both branches, pop-off back to the outer context.
              VFFCompletePath otherAssumes other ->
                do ar <- ReaderT $ \s ->
                     mergePartialResult s tgt pred er other
  
                   -- Merge the assumptions from each branch and add to the
                   -- current assumption frame
                   pathAssumes <- liftIO $ popAssumptionFrame bak assume_frame
  
                   liftIO $ addAssumptions bak
                     =<< mergeAssumptions sym pred pathAssumes otherAssumes
  
                   -- Check for more potential merge targets.
                   withReaderT
                     (stateTree .~ ActiveTree ctx ar)
                     (checkForIntraFrameMerge tgt)
  
        -- Since the other branch aborted before it got to the merge point,
        -- we merge-in the partiality on our current path and keep going.
        VFFPartial ctx loc pred ar needsAborting ->
          do er'  <- case needsAborting of
                       NoNeedToAbort    -> return er
                       NeedsToBeAborted -> ReaderT $ \s -> abortPartialResult s tgt er
             er'' <- liftIO $
               mergePartialAndAbortedResult sym loc pred er' ar
             withReaderT
               (stateTree .~ ActiveTree ctx er'')
               (checkForIntraFrameMerge tgt)
  
        -- There are no pending merges to deal with.  Instead, complete
        -- the transfer of control by either transitioning into an ordinary
        -- running state, or by returning a value to the calling context.
        _ -> case tgt of
               BlockTarget bid ->
                 continue (RunPostBranchMerge bid)
               ReturnTarget ->
                 handleSimReturn
                   (er^.partialValue.gpValue.frameFunctionName)
                   (returnContext ctx0)
                   (er^.partialValue.gpValue.to fromReturnFrame)
  
  ---------------------------------------------------------------------
  -- Abort handling
  
  -- | The default abort handler calls `abortExecAndLog`.
  defaultAbortHandler :: IsSymInterface sym => AbortHandler p sym ext rtp
  defaultAbortHandler = AH abortExecAndLog
  
  -- | Abort the current execution and roll back to the nearest
  --   symbolic branch point.  When verbosity is 3 or more, a message
  --   will be logged indicating the reason for the abort.
  --
  --   The default abort handler calls this function.
  abortExecAndLog ::
    IsSymInterface sym =>
    AbortExecReason ->
    ExecCont p sym ext rtp f args
  abortExecAndLog rsn = do
    t   <- view stateTree
    cfg <- view stateConfiguration
    ctx <- view stateContext
    v <- liftIO (getOpt =<< getOptionSetting verbosity cfg)
    when (v >= 3) $ do
      let frames = activeFrames t
      let msg = PP.vcat [ ppAbortExecReason rsn
                        , PP.indent 2 (ppExceptionContext frames) ]
      -- Print error message.
      liftIO (hPrint (printHandle ctx) msg)
  
    -- Switch to new frame.
    abortExec rsn
  
  
  -- | Abort the current execution and roll back to the nearest
  --   symbolic branch point.
  abortExec ::
    IsSymInterface sym =>
    AbortExecReason ->
    ExecCont p sym ext rtp f args
  abortExec rsn = do
    ActiveTree ctx ar0 <- view stateTree
    resumeValueFromFrameAbort ctx $
      -- Get aborted result from active result.
      case ar0 of
        TotalRes e -> AbortedExec rsn e
        PartialRes loc pred ex ar1 ->
          AbortedBranch loc pred (AbortedExec rsn ex) ar1
  
  
  ------------------------------------------------------------------------
  -- Internal operations
  
  -- | Resolve the fact that the current branch aborted.
  resumeValueFromFrameAbort ::
    IsSymInterface sym =>
    ValueFromFrame p sym ext r f ->
    AbortedResult sym ext {- ^ The execution that is being aborted. -} ->
    ExecCont p sym ext r g args
  resumeValueFromFrameAbort ctx0 ar0 = do
    simCtx <- view stateContext
    sym <- view stateSymInterface
    withBackend simCtx $ \bak ->
      case ctx0 of
  
        -- This is the first abort.
        VFFBranch ctx assume_frame loc pred other_branch tgt ->
          do pnot <- liftIO $ notPred sym pred
             let nextCtx = VFFPartial ctx loc pnot ar0 NeedsToBeAborted
  
             -- Reset the backend path state
             _assumes <- liftIO $ popAssumptionFrame bak assume_frame
  
             case other_branch of
  
               -- We have some more work to do.
               VFFActivePath n ->
                 do liftIO $ addAssumption bak (BranchCondition loc (pausedLoc n) pnot)
                    resumeFrame n nextCtx
  
               -- The other branch had finished successfully;
               -- Since this one aborted, then the other one is really the only
               -- viable option we have, and so we commit to it.
               VFFCompletePath otherAssumes er ->
                 do -- We are committed to the other path,
                    -- assume all of its suspended assumptions
                    liftIO $ addAssumptions bak otherAssumes
  
                    -- check for further merges, then continue onward.
                    withReaderT
                      (stateTree .~ ActiveTree nextCtx er)
                      (checkForIntraFrameMerge tgt)
  
        -- Both branches aborted
        VFFPartial ctx loc pred ay _ ->
          resumeValueFromFrameAbort ctx $ AbortedBranch loc pred ar0 ay
  
        VFFEnd ctx ->
          ReaderT $ return . UnwindCallState ctx ar0
  
  -- | Run rest of execution given a value from value context and an aborted
  -- result.
  resumeValueFromValueAbort ::
    IsSymInterface sym =>
    ValueFromValue p sym ext r ret' ->
    AbortedResult sym ext ->
    ExecCont p sym ext r f a
  resumeValueFromValueAbort ctx0 ar0 =
    case ctx0 of
      VFVCall ctx frm _rh ->
        do ActiveTree _oldFrm er <- view stateTree
           withReaderT
             (stateTree .~ ActiveTree ctx (er & partialValue.gpValue .~ frm))
             (resumeValueFromFrameAbort ctx ar0)
      VFVPartial ctx loc pred ay -> do
        resumeValueFromValueAbort ctx (AbortedBranch loc pred ar0 ay)
      VFVEnd ->
        do res <- view stateContext
           return $! ResultState $ AbortedResult res ar0
  
  -- | Resume a paused frame.
  resumeFrame ::
    IsSymInterface sym =>
    PausedFrame p sym ext rtp f ->
    ValueFromFrame p sym ext rtp f ->
    ExecCont p sym ext rtp g ba
  resumeFrame (PausedFrame frm cont toLoc) ctx =
   do case toLoc of
        Nothing -> return ()
        Just l  ->
          do sym <- view stateSymInterface
             liftIO $ setCurrentProgramLoc sym l
      withReaderT
        (stateTree .~ ActiveTree ctx frm)
        (ReaderT $ return . ControlTransferState cont)
  {-# INLINABLE resumeFrame #-}
  
  
  -- | Transition immediately to a @ReturnState@.  We are done with all
  --   intercall merges, and are ready to resmue execution in the caller's
  --   context.
  handleSimReturn ::
    IsSymInterface sym =>
    FunctionName {- ^ Name of the function we are returning from -} ->
    ValueFromValue p sym ext r ret {- ^ Context to return to. -} ->
    RegEntry sym ret {- ^ Value that is being returned. -} ->
    ExecCont p sym ext r f a
  handleSimReturn fnName vfv return_value =
    ReaderT $ return . ReturnState fnName vfv return_value
  
  
  -- | Resolve the return value, and begin executing in the caller's context again.
  performReturn ::
    IsSymInterface sym =>
    FunctionName {- ^ Name of the function we are returning from -} ->
    ValueFromValue p sym ext r ret {- ^ Context to return to. -} ->
    RegEntry sym ret {- ^ Value that is being returned. -} ->
    ExecCont p sym ext r f a
  performReturn fnName ctx0 v = do
    case ctx0 of
      VFVCall ctx (MF f) (ReturnToCrucible tpr rest) ->
        do ActiveTree _oldctx pres <- view stateTree
           let f' = extendFrame tpr (regValue v) rest f
           withReaderT
             (stateTree .~ ActiveTree ctx (pres & partialValue . gpValue .~ MF f'))
             (continue (RunReturnFrom fnName))
  
      VFVCall ctx _ TailReturnToCrucible ->
        do ActiveTree _oldctx pres <- view stateTree
           withReaderT
             (stateTree .~ ActiveTree ctx (pres & partialValue . gpValue .~ RF fnName v))
             (returnValue v)
  
      VFVCall ctx (OF f) (ReturnToOverride k) ->
        do ActiveTree _oldctx pres <- view stateTree
           withReaderT
             (stateTree .~ ActiveTree ctx (pres & partialValue . gpValue .~ OF f))
             (ReaderT (k v))
  
      VFVPartial ctx loc pred r ->
        do sym <- view stateSymInterface
           ActiveTree oldctx pres <- view stateTree
           newPres <- liftIO $
             mergePartialAndAbortedResult sym loc pred pres r
           withReaderT
              (stateTree .~ ActiveTree oldctx newPres)
              (performReturn fnName ctx v)
  
      VFVEnd ->
        do simctx <- view stateContext
           ActiveTree _oldctx pres <- view stateTree
           return $! ResultState $ FinishedResult simctx (pres & partialValue . gpValue .~ v)
  
  cruciblePausedFrame ::
    ResolvedJump sym b ->
    GlobalPair sym (SimFrame sym ext (CrucibleLang b r) ('Just a)) ->
    CrucibleBranchTarget (CrucibleLang b r) pd_args {- ^ postdominator target -} ->
    ReaderT (SimState p sym ext rtp (CrucibleLang b z) ('Just dc_args)) IO
            (PausedFrame p sym ext rtp' (CrucibleLang b r))
  cruciblePausedFrame jmp@(ResolvedJump x_id _) top_frame pd =
    do let res = case testEquality pd (BlockTarget x_id) of
                   Just Refl -> CheckMergeResumption jmp
                   Nothing   -> ContinueResumption jmp
       loc <- getTgtLoc x_id
       return $ PausedFrame (TotalRes top_frame) res (Just loc)
  
  overrideSymbolicBranch ::
    IsSymInterface sym =>
    Pred sym ->
  
    RegMap sym then_args ->
    ExecCont p sym ext rtp (OverrideLang r) ('Just then_args) {- ^ if branch -} ->
    Maybe Position {- ^ optional if branch location -} ->
  
    RegMap sym else_args ->
    ExecCont p sym ext rtp (OverrideLang r) ('Just else_args) {- ^ else branch -} ->
    Maybe Position {- ^ optional else branch location -} ->
  
    ExecCont p sym ext rtp (OverrideLang r) ('Just args)
  overrideSymbolicBranch p thn_args thn thn_pos els_args els els_pos =
    do top_frm <- view (stateTree.actFrame)
       let fnm     = top_frm^.gpValue.overrideSimFrame.override
       let thn_loc = mkProgramLoc fnm <$> thn_pos
       let els_loc = mkProgramLoc fnm <$> els_pos
       let thn_frm = PausedFrame (TotalRes top_frm) (OverrideResumption thn thn_args) thn_loc
       let els_frm = PausedFrame (TotalRes top_frm) (OverrideResumption els els_args) els_loc
       intra_branch p thn_frm els_frm ReturnTarget
  
  getTgtLoc ::
    BlockID b y ->
    ReaderT (SimState p sym ext r (CrucibleLang b a) ('Just dc_args)) IO ProgramLoc
  getTgtLoc (BlockID i) =
     do blocks <- view (stateCrucibleFrame . to frameBlockMap)
        return $ blockLoc (blocks Ctx.! i)
  
  -- | Return the context of the current top frame.
  asContFrame ::
    ActiveTree     p sym ext ret f args ->
    ValueFromFrame p sym ext ret f
  asContFrame (ActiveTree ctx active_res) =
    case active_res of
      TotalRes{} -> ctx
      PartialRes loc pred _ex ar -> VFFPartial ctx loc pred ar NoNeedToAbort
  
  
  -- | Return assertion where predicate equals a constant
  predEqConst :: IsExprBuilder sym => sym -> Pred sym -> Bool -> IO (Pred sym)
  predEqConst _   p True  = return p
  predEqConst sym p False = notPred sym p
  
  -- | Branch with a merge point inside this frame.
  intra_branch ::
    IsSymInterface sym =>
    Pred sym
    {- ^ Branch condition branch -} ->
  
    PausedFrame p sym ext rtp f
    {- ^ true branch. -} ->
  
    PausedFrame p sym ext rtp f
    {- ^ false branch. -} ->
  
    CrucibleBranchTarget f (args :: Maybe (Ctx CrucibleType))
    {- ^ Postdominator merge point, where both branches meet again. -} ->
  
    ExecCont p sym ext rtp f ('Just dc_args)
  
  intra_branch p t_label f_label tgt = do
    ctx <- asContFrame <$> view stateTree
    simCtx <- view stateContext
    sym <- view stateSymInterface
    withBackend simCtx $ \bak ->
      case asConstantPred p of
        Nothing ->
          ReaderT $ return . SymbolicBranchState p t_label f_label tgt
  
        Just chosen_branch ->
          do p' <- liftIO $ predEqConst sym p chosen_branch
             let a_frame = if chosen_branch then t_label else f_label
             loc <- liftIO $ getCurrentProgramLoc sym
             liftIO $ addAssumption bak (BranchCondition loc (pausedLoc a_frame) p')
             resumeFrame a_frame ctx
  {-# INLINABLE intra_branch #-}
  
  -- | Branch with a merge point inside this frame.
  performIntraFrameSplit ::
    IsSymInterface sym =>
    Pred sym
    {- ^ Branch condition -} ->
  
    PausedFrame p sym ext rtp f
    {- ^ active branch. -} ->
  
    PausedFrame p sym ext rtp f
    {- ^ other branch. -} ->
  
    CrucibleBranchTarget f (args :: Maybe (Ctx CrucibleType))
    {- ^ Postdominator merge point, where both branches meet again. -} ->
  
    ExecCont p sym ext rtp f ('Just dc_args)
  performIntraFrameSplit p a_frame o_frame tgt =
    do ctx <- asContFrame <$> view stateTree
       simCtx <- view stateContext
       sym <- view stateSymInterface
       loc <- liftIO $ getCurrentProgramLoc sym
       a_frame' <- pushPausedFrame a_frame
       o_frame' <- pushPausedFrame o_frame
  
       assume_frame <- withBackend simCtx $ \bak ->
         liftIO $ assumeInNewFrame bak (BranchCondition loc (pausedLoc a_frame') p)
  
       -- Create context for paused frame.
       let todo = VFFActivePath o_frame'
           ctx' = VFFBranch ctx assume_frame loc p todo tgt
  
       -- Start a_state (where branch pred is p)
       resumeFrame a_frame' ctx'
  
  performFunctionCall ::
    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
  performFunctionCall retHandler frm =
    do sym <- view stateSymInterface
       case frm of
         OverrideCall o f ->
           -- Eventually, locations should be nested. However, for now,
           -- while they're not, it's useful for the location of an
           -- override to be the location of its call site, so we don't
           -- change it here.
           withReaderT
             (stateTree %~ pushCallFrame retHandler (OF f))
             (runOverride o)
         CrucibleCall entryID f -> do
           let loc = mkProgramLoc (resolvedCallName frm) (OtherPos "<function entry>")
           liftIO $ setCurrentProgramLoc sym loc
           withReaderT
             (stateTree %~ pushCallFrame retHandler (MF f))
             (continue (RunBlockStart entryID))
  
  performTailCall ::
    IsSymInterface sym =>
    ValueFromValue p sym ext rtp ret ->
    ResolvedCall p sym ext ret ->
    ExecCont p sym ext rtp f a
  performTailCall vfv frm =
    do sym <- view stateSymInterface
       let loc = mkProgramLoc (resolvedCallName frm) (OtherPos "<function entry>")
       liftIO $ setCurrentProgramLoc sym loc
       case frm of
         OverrideCall o f ->
           withReaderT
             (stateTree %~ swapCallFrame vfv (OF f))
             (runOverride o)
         CrucibleCall entryID f ->
           withReaderT
             (stateTree %~ swapCallFrame vfv (MF f))
             (continue (RunBlockStart entryID))
  
  ------------------------------------------------------------------------
  -- Context tree manipulations
  
  -- | Returns true if tree contains a single non-aborted execution.
  isSingleCont :: ValueFromFrame p sym ext root a -> Bool
  isSingleCont c0 =
    case c0 of
      VFFBranch{} -> False
      VFFPartial c _ _ _ _ -> isSingleCont c
      VFFEnd vfv -> isSingleVFV vfv
  
  isSingleVFV :: ValueFromValue p sym ext r a -> Bool
  isSingleVFV c0 = do
    case c0 of
      VFVCall c _ _ -> isSingleCont c
      VFVPartial c _ _ _ -> isSingleVFV c
      VFVEnd -> True
  
  -- | Attempt to unwind a frame context into a value context.
  --   This succeeds only if there are no pending symbolic
  --   merges.
  unwindContext ::
    ValueFromFrame p sym ext root f ->
    Maybe (ValueFromValue p sym ext root (FrameRetType f))
  unwindContext c0 =
      case c0 of
        VFFBranch{} -> Nothing
        VFFPartial _ _ _ _ NeedsToBeAborted -> Nothing
        VFFPartial d loc pred ar NoNeedToAbort ->
          (\d' -> VFVPartial d' loc pred ar) <$> unwindContext d
        VFFEnd vfv -> return vfv
  
  -- | Get the context for when returning (assumes no
  -- intra-procedural merges are possible).
  returnContext ::
    ValueFromFrame ctx sym ext root f ->
    ValueFromValue ctx sym ext root (FrameRetType f)
  returnContext c0 =
    fromMaybe
      (panic "ExecutionTree.returnContext"
        [ "Unexpected attempt to exit function before all intra-procedural merges are complete."
        , "The call stack was:"
        , show (PP.pretty c0)
        ])
      (unwindContext c0)
  
  -- | Replace the given frame with a new frame.  Succeeds
  --   only if there are no pending symbolic merge points.
  replaceTailFrame :: forall p sym ext a b c args args'.
    FrameRetType a ~ FrameRetType c =>
    ActiveTree p sym ext b a args ->
    SimFrame sym ext c args' ->
    Maybe (ActiveTree p sym ext b c args')
  replaceTailFrame t@(ActiveTree c _) f = do
      vfv <- unwindContext c
      return $ swapCallFrame vfv f t
  
  swapCallFrame ::
    ValueFromValue p sym ext rtp (FrameRetType f') ->
    SimFrame sym ext f' args' ->
    ActiveTree p sym ext rtp f args ->
    ActiveTree p sym ext rtp f' args'
  swapCallFrame vfv frm (ActiveTree _ er) =
    ActiveTree (VFFEnd vfv) (er & partialValue . gpValue .~ frm)
  
  
  pushCallFrame ::
    ReturnHandler (FrameRetType a) p sym ext r f old_args
      {- ^ What to do with the result of the function -} ->
  
    SimFrame sym ext a args
      {- ^ The code to run -} ->
  
    ActiveTree p sym ext r f old_args ->
    ActiveTree p sym ext r a args
  pushCallFrame rh f' (ActiveTree ctx er) =
      ActiveTree (VFFEnd (VFVCall ctx old_frame rh)) er'
    where
    old_frame = er ^. partialValue ^. gpValue
    er'       = er &  partialValue  . gpValue .~ f'
  
  
  -- | Create a tree that contains just a single path with no branches.
  --
  -- All branch conditions are converted to assertions.
  extractCurrentPath ::
    ActiveTree p sym ext ret f args ->
    ActiveTree p sym ext ret f args
  extractCurrentPath t =
    ActiveTree (vffSingleContext (t^.actContext))
               (TotalRes (t^.actFrame))
  
  vffSingleContext ::
    ValueFromFrame p sym ext ret f ->
    ValueFromFrame p sym ext ret f
  vffSingleContext ctx0 =
    case ctx0 of
      VFFBranch ctx _ _ _ _ _ -> vffSingleContext ctx
      VFFPartial ctx _ _ _ _  -> vffSingleContext ctx
      VFFEnd ctx              -> VFFEnd (vfvSingleContext ctx)
  
  vfvSingleContext ::
    ValueFromValue p sym ext root top_ret ->
    ValueFromValue p sym ext root top_ret
  vfvSingleContext ctx0 =
    case ctx0 of
      VFVCall ctx f h         -> VFVCall (vffSingleContext ctx) f h
      VFVPartial ctx _ _ _    -> vfvSingleContext ctx
      VFVEnd                  -> VFVEnd
  
  
  ------------------------------------------------------------------------
  -- branchConditions
  
  -- -- | Return all branch conditions along path to this node.
  -- branchConditions :: ActiveTree ctx sym ext ret f args -> [Pred sym]
  -- branchConditions t =
  --   case t^.actResult of
  --     TotalRes _ -> vffBranchConditions (t^.actContext)
  --     PartialRes p _ _ -> p : vffBranchConditions (t^.actContext)
  
  -- vffBranchConditions :: ValueFromFrame p sym ext ret f
  --                     -> [Pred sym]
  -- vffBranchConditions ctx0 =
  --   case ctx0 of
  --     VFFBranch   ctx _ _ p _ _  -> p : vffBranchConditions ctx
  --     VFFPartial  ctx p _ _      -> p : vffBranchConditions ctx
  --     VFFEnd  ctx -> vfvBranchConditions ctx
  
  -- vfvBranchConditions :: ValueFromValue p sym ext root top_ret
  --                     -> [Pred sym]
  -- vfvBranchConditions ctx0 =
  --   case ctx0 of
  --     VFVCall     ctx _ _      -> vffBranchConditions ctx
  --     VFVPartial  ctx p _      -> p : vfvBranchConditions ctx
  --     VFVEnd                   -> []
  