{-|
Copyright        : (c) Galois, Inc. 2025
Maintainer       : Langston Barrett <langston@galois.com>
-}

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeOperators #-}

module Lang.Crucible.Debug
  ( debugger
  , bareDebuggerExt
  , bareDebugger
  , Inps.defaultDebuggerInputs
  , Outps.defaultDebuggerOutputs
  , Arg.Arg(..)
  , AType.ArgTypeRepr(..)
  , type AType.Breakpoint
  , type AType.Exactly
  , type AType.Function
  , type AType.Int
  , type AType.Path
  , type AType.Text
  , Cmd.Command(Base, Ext)
  , Cmd.CommandExt(..)
  , Cmd.voidExts
  , Cmds.execStateSimState
  , Ctxt.EvalResult(..)
  , Ctxt.Context(..)
  , Ctxt.CommandImpl(..)
  , Ctxt.ExtImpl(..)
  , Ctxt.voidImpl
  , Resp.Response(Ok, UserError, XResponse)
  , Resp.UserError(NotApplicable)
  , Resp.NotApplicable(DoneSimulating, NotYetSimulating)
  , Resp.ResponseExt
  , type Rgx.Regex
  , type Rgx.Empty
  , type Rgx.Lit
  , type (Rgx.:|)
  , type Rgx.Then
  , type Rgx.Star
  , Rgx.Match(..)
  , Rgx.RegexRepr(..)
  , Trace.Trace
  , Trace.TraceEntry(..)
  , Trace.latest
  , IntrinsicPrinters(..)
  ) where

import Control.Applicative qualified as Applicative
import Control.Lens qualified as Lens
import Control.Monad qualified as Monad
import Data.IORef qualified as IORef
import Data.Maybe qualified as Maybe
import Data.Parameterized.Map qualified as MapF
import Data.Parameterized.Nonce qualified as Nonce
import Data.Parameterized.Some (Some(Some))
import Data.Set qualified as Set
import Data.Text (Text)
import Data.Void (Void)
import Lang.Crucible.Backend qualified as C
import Lang.Crucible.Backend.Simple qualified as C
import Lang.Crucible.CFG.Extension qualified as C
import Lang.Crucible.Debug.Arg qualified as Arg
import Lang.Crucible.Debug.Arg.Type qualified as AType
import Lang.Crucible.Debug.Breakpoint qualified as Break
import Lang.Crucible.Debug.Command qualified as Cmd
import Lang.Crucible.Debug.Commands qualified as Cmds
import Lang.Crucible.Debug.Complete qualified as Complete
import Lang.Crucible.Debug.Complete (CompletionT)
import Lang.Crucible.Debug.Context (Context, DebuggerState)
import Lang.Crucible.Debug.Context qualified as Ctxt
import Lang.Crucible.Debug.Eval (EvalResult)
import Lang.Crucible.Debug.Eval qualified as Eval
import Lang.Crucible.Debug.Inputs (Inputs)
import Lang.Crucible.Debug.Inputs qualified as Inps
import Lang.Crucible.Debug.Outputs (Outputs)
import Lang.Crucible.Debug.Outputs qualified as Outps
import Lang.Crucible.Debug.Regex qualified as Rgx
import Lang.Crucible.Debug.Response qualified as Resp
import Lang.Crucible.Debug.Response (Response)
import Lang.Crucible.Debug.Statement (Statement)
import Lang.Crucible.Debug.Style qualified as Style
import Lang.Crucible.Debug.Style (StyleT)
import Lang.Crucible.Debug.Trace qualified as Trace
import Lang.Crucible.FunctionHandle qualified as C
import Lang.Crucible.Pretty (IntrinsicPrinters(..))
import Lang.Crucible.Simulator.CallFrame qualified as C
import Lang.Crucible.Simulator.EvalStmt qualified as C
import Lang.Crucible.Simulator.ExecutionTree qualified as C
import Lang.Crucible.Simulator qualified as C
import Lang.Crucible.Syntax.Concrete qualified as C
import Lang.Crucible.Types qualified as C
import Prettyprinter qualified as PP
import System.Exit qualified as Exit
import System.IO (stdout)
import What4.Expr qualified as W4
import What4.Interface qualified as W4

-- Useful for debugging
_printState :: C.ExecState p sym ext rtp -> Text
_printState :: forall p sym ext rtp. ExecState p sym ext rtp -> Text
_printState =
  \case
    C.AbortState {} -> Text
"AbortState"
    C.CallState {} -> Text
"CallState"
    C.TailCallState {} -> Text
"TailCallState"
    C.ReturnState {} -> Text
"ReturnState"
    C.ResultState {} -> Text
"ResultState"
    C.InitialState {} -> Text
"InitialState"
    C.OverrideState {} -> Text
"OverrideState"
    C.RunningState {} -> Text
"RunningState"
    C.SymbolicBranchState {} -> Text
"SymbolicBranchState"
    C.BranchMergeState {} -> Text
"BranchMergeState"
    C.ControlTransferState {} -> Text
"ControlTransferState"
    C.UnwindCallState {} -> Text
"UnwindCallState"

stepState ::
  Context cExt p sym ext t ->
  C.ExecState p sym ext rtp ->
  IO DebuggerState
stepState :: forall cExt p sym ext (t :: CrucibleType) rtp.
Context cExt p sym ext t
-> ExecState p sym ext rtp -> IO DebuggerState
stepState Context cExt p sym ext t
ctx =
  \case
    C.AbortState {} ->
      if Context cExt p sym ext t -> Bool
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> Bool
Ctxt.dbgStopOnAbort Context cExt p sym ext t
ctx
      then DebuggerState -> IO DebuggerState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DebuggerState
Ctxt.Stopped
      else DebuggerState -> IO DebuggerState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DebuggerState
initState
    C.CallState ReturnHandler ret p sym ext rtp f a
_retHandler ResolvedCall p sym ext ret
frm SimState p sym ext rtp f a
_st -> do
      C.SomeHandle FnHandle args ret
hdl <- SomeHandle -> IO SomeHandle
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ResolvedCall p sym ext ret -> SomeHandle
forall p sym ext (ret :: CrucibleType).
ResolvedCall p sym ext ret -> SomeHandle
C.resolvedCallHandle ResolvedCall p sym ext ret
frm)
      FnHandle args ret -> IO DebuggerState
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> IO DebuggerState
stepCall FnHandle args ret
hdl
    C.TailCallState ValueFromValue p sym ext rtp ret
_vfv ResolvedCall p sym ext ret
frm SimState p sym ext rtp f a
_st -> do
      C.SomeHandle FnHandle args ret
hdl <- SomeHandle -> IO SomeHandle
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ResolvedCall p sym ext ret -> SomeHandle
forall p sym ext (ret :: CrucibleType).
ResolvedCall p sym ext ret -> SomeHandle
C.resolvedCallHandle ResolvedCall p sym ext ret
frm)
      FnHandle args ret -> IO DebuggerState
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> IO DebuggerState
stepCall FnHandle args ret
hdl
    C.ReturnState FunctionName
_fnm ValueFromValue p sym ext rtp ret
_vfv RegEntry sym ret
_ret SimState p sym ext rtp f a
_st ->
      case DebuggerState
initState of
        Ctxt.Running RunningState
Ctxt.Finish -> DebuggerState -> IO DebuggerState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DebuggerState
Ctxt.Stopped
        DebuggerState
_ -> DebuggerState -> IO DebuggerState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DebuggerState
initState
    C.RunningState (C.RunBlockEnd Some (BlockID blocks)
_) SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
simState -> do
      let fr :: CallFrame sym ext blocks r args
fr = SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
simState 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
Lens.^. 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 :: * -> *).
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
      C.CallFrame { _frameCFG :: ()
C._frameCFG = CFG ext blocks initialArgs r
cfg, _frameBlockID :: forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args -> Some (BlockID blocks)
C._frameBlockID = Some (BlockID blocks)
blkId } <- CallFrame sym ext blocks r args
-> IO (CallFrame sym ext blocks r args)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CallFrame sym ext blocks r args
fr
      let ent :: TraceEntry ext
ent = CFG ext blocks initialArgs r
-> Some (BlockID blocks) -> TraceEntry ext
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> Some (BlockID blocks) -> TraceEntry ext
Trace.TraceEntry CFG ext blocks initialArgs r
cfg Some (BlockID blocks)
blkId
      Trace ext -> TraceEntry ext -> IO ()
forall ext. Trace ext -> TraceEntry ext -> IO ()
Trace.append (Context cExt p sym ext t -> Trace ext
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> Trace ext
Ctxt.dbgTrace Context cExt p sym ext t
ctx) TraceEntry ext
ent
      DebuggerState -> IO DebuggerState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DebuggerState
initState

    -- Nothing to do for these...
    C.InitialState {} -> DebuggerState -> IO DebuggerState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DebuggerState
initState
    C.OverrideState {} -> DebuggerState -> IO DebuggerState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DebuggerState
initState
    C.ResultState {} -> DebuggerState -> IO DebuggerState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DebuggerState
initState
    C.RunningState {} -> DebuggerState -> IO DebuggerState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DebuggerState
initState
    C.SymbolicBranchState {} -> DebuggerState -> IO DebuggerState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DebuggerState
initState

    -- These are mostly implementation details...
    C.BranchMergeState {} -> DebuggerState -> IO DebuggerState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DebuggerState
initState
    C.ControlTransferState {} -> DebuggerState -> IO DebuggerState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DebuggerState
initState
    C.UnwindCallState {} -> DebuggerState -> IO DebuggerState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DebuggerState
initState
  where
    initState :: DebuggerState
initState = Context cExt p sym ext t -> DebuggerState
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> DebuggerState
Ctxt.dbgState Context cExt p sym ext t
ctx

    stepCall :: C.FnHandle args ret ->  IO DebuggerState
    stepCall :: forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> IO DebuggerState
stepCall FnHandle args ret
hdl = do
      let b :: Breakpoint
b = FunctionName -> Breakpoint
Break.BreakFunction (FnHandle args ret -> FunctionName
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
C.handleName FnHandle args ret
hdl)
      if Breakpoint -> Set Breakpoint -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Breakpoint
b (Context cExt p sym ext t -> Set Breakpoint
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> Set Breakpoint
Ctxt.dbgBreakpoints Context cExt p sym ext t
ctx)
      then DebuggerState -> IO DebuggerState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DebuggerState
Ctxt.Stopped
      else DebuggerState -> IO DebuggerState
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure DebuggerState
initState

mergeResults ::
  C.ExecutionFeatureResult p sym ext ret ->
  C.ExecutionFeatureResult p sym ext ret ->
  C.ExecutionFeatureResult p sym ext ret
mergeResults :: forall p sym ext ret.
ExecutionFeatureResult p sym ext ret
-> ExecutionFeatureResult p sym ext ret
-> ExecutionFeatureResult p sym ext ret
mergeResults ExecutionFeatureResult p sym ext ret
old ExecutionFeatureResult p sym ext ret
new =
  case ExecutionFeatureResult p sym ext ret
old of
    ExecutionFeatureResult p sym ext ret
C.ExecutionFeatureNoChange -> ExecutionFeatureResult p sym ext ret
new
    ExecutionFeatureResult p sym ext ret
_ ->
      case ExecutionFeatureResult p sym ext ret
new of
        ExecutionFeatureResult p sym ext ret
C.ExecutionFeatureNoChange -> ExecutionFeatureResult p sym ext ret
old
        ExecutionFeatureResult p sym ext ret
_ -> ExecutionFeatureResult p sym ext ret
new

resultState ::
  C.ExecutionFeatureResult p sym ext ret ->
  Maybe (C.ExecState p sym ext ret)
resultState :: forall p sym ext ret.
ExecutionFeatureResult p sym ext ret
-> Maybe (ExecState p sym ext ret)
resultState =
  \case
    ExecutionFeatureResult p sym ext ret
C.ExecutionFeatureNoChange -> Maybe (ExecState p sym ext ret)
forall a. Maybe a
Nothing
    C.ExecutionFeatureModifiedState ExecState p sym ext ret
s -> ExecState p sym ext ret -> Maybe (ExecState p sym ext ret)
forall a. a -> Maybe a
Just ExecState p sym ext ret
s
    C.ExecutionFeatureNewState ExecState p sym ext ret
s -> ExecState p sym ext ret -> Maybe (ExecState p sym ext ret)
forall a. a -> Maybe a
Just ExecState p sym ext ret
s

stopped ::
  (sym ~ W4.ExprBuilder s st fs) =>
  C.IsSymInterface sym =>
  C.IsSyntaxExtension ext =>
  (?parserHooks :: C.ParserHooks ext) =>
  PP.Pretty cExt =>
  W4.IsExpr (W4.SymExpr sym) =>
  Context cExt p sym ext t ->
  C.ExecState p sym ext (C.RegEntry sym t) ->
  IO (EvalResult cExt p sym ext t)
stopped :: forall sym s (st :: * -> *) fs ext cExt p (t :: CrucibleType).
(sym ~ ExprBuilder s st fs, IsSymInterface sym,
 IsSyntaxExtension ext, ?parserHooks::ParserHooks ext, Pretty cExt,
 IsExpr (SymExpr sym)) =>
Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> IO (EvalResult cExt p sym ext t)
stopped Context cExt p sym ext t
ctx0 ExecState p sym ext (RegEntry sym t)
execState0 = Context cExt p (ExprBuilder s st fs) ext t
-> ExecState
     p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
-> ExecutionFeatureResult
     p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
-> IO (EvalResult cExt p (ExprBuilder s st fs) ext t)
forall {s} {st :: * -> *} {fs} {ext} {cExt} {p}
       {t :: CrucibleType}.
(IsInterpretedFloatExprBuilder (ExprBuilder s st fs),
 IsSyntaxExtension ext, ?parserHooks::ParserHooks ext,
 Pretty cExt) =>
Context cExt p (ExprBuilder s st fs) ext t
-> ExecState
     p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
-> ExecutionFeatureResult
     p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
-> IO (EvalResult cExt p (ExprBuilder s st fs) ext t)
go Context cExt p sym ext t
Context cExt p (ExprBuilder s st fs) ext t
ctx0 ExecState p sym ext (RegEntry sym t)
ExecState
  p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
execState0 ExecutionFeatureResult
  p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNoChange
  where
    go :: Context cExt p (ExprBuilder s st fs) ext t
-> ExecState
     p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
-> ExecutionFeatureResult
     p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
-> IO (EvalResult cExt p (ExprBuilder s st fs) ext t)
go Context cExt p (ExprBuilder s st fs) ext t
c0 ExecState
  p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
s0 ExecutionFeatureResult
  p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
r = do
      let cEnv :: CompletionEnv cExt
cEnv = Context cExt p (ExprBuilder s st fs) ext t
-> ExecState
     p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
-> CompletionEnv cExt
forall cExt p sym ext (t :: CrucibleType) r.
Context cExt p sym ext t
-> ExecState p sym ext r -> CompletionEnv cExt
Ctxt.toCompletionEnv Context cExt p (ExprBuilder s st fs) ext t
c0 ExecState
  p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
s0
      let sEnv :: StyleEnv cExt
sEnv = Context cExt p (ExprBuilder s st fs) ext t
-> ExecState
     p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
-> StyleEnv cExt
forall cExt p sym ext (t :: CrucibleType) r.
Context cExt p sym ext t -> ExecState p sym ext r -> StyleEnv cExt
Ctxt.toStyleEnv Context cExt p (ExprBuilder s st fs) ext t
c0 ExecState
  p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
s0
      Statement cExt
stmt <- StyleEnv cExt
-> StyleT cExt IO (Statement cExt) -> IO (Statement cExt)
forall cExt (m :: * -> *) a.
StyleEnv cExt -> StyleT cExt m a -> m a
Style.runStyleM StyleEnv cExt
sEnv (CompletionEnv cExt
-> CompletionT cExt (StyleT cExt IO) (Statement cExt)
-> StyleT cExt IO (Statement cExt)
forall cExt (m :: * -> *) a.
CompletionEnv cExt -> CompletionT cExt m a -> m a
Complete.runCompletionM CompletionEnv cExt
cEnv (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
-> CompletionT cExt (StyleT cExt IO) (Statement cExt)
forall (m :: * -> *) a. Inputs m a -> m a
Inps.recv (Context cExt p (ExprBuilder s st fs) ext t
-> Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t
-> Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
Ctxt.dbgInputs Context cExt p (ExprBuilder s st fs) ext t
c0)))
      EvalResult cExt p (ExprBuilder s st fs) ext t
result0 <- Context cExt p (ExprBuilder s st fs) ext t
-> ExecState
     p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
-> Statement cExt
-> IO (EvalResult cExt p (ExprBuilder s st fs) ext t)
forall sym s (st :: * -> *) fs ext cExt p (t :: CrucibleType).
(sym ~ ExprBuilder s st fs, IsSymInterface sym,
 IsSyntaxExtension ext, ?parserHooks::ParserHooks ext, Pretty cExt,
 IsExpr (SymExpr sym)) =>
Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Statement cExt
-> IO (EvalResult cExt p sym ext t)
Eval.eval Context cExt p (ExprBuilder s st fs) ext t
c0 ExecState
  p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
s0 Statement cExt
stmt
      let featResult :: ExecutionFeatureResult
  p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
featResult = ExecutionFeatureResult
  p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
-> ExecutionFeatureResult
     p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
-> ExecutionFeatureResult
     p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
forall p sym ext ret.
ExecutionFeatureResult p sym ext ret
-> ExecutionFeatureResult p sym ext ret
-> ExecutionFeatureResult p sym ext ret
mergeResults ExecutionFeatureResult
  p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
r (EvalResult cExt p (ExprBuilder s st fs) ext t
-> ExecutionFeatureResult
     p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
forall cExt p sym ext (t :: CrucibleType).
EvalResult cExt p sym ext t
-> ExecutionFeatureResult p sym ext (RegEntry sym t)
Eval.evalFeatureResult EvalResult cExt p (ExprBuilder s st fs) ext t
result0)
      let result :: EvalResult cExt p (ExprBuilder s st fs) ext t
result = EvalResult cExt p (ExprBuilder s st fs) ext t
result0 { Eval.evalFeatureResult = featResult }
      let s :: ExecState
  p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
s = ExecState
  p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
-> Maybe
     (ExecState
        p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t))
-> ExecState
     p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
forall a. a -> Maybe a -> a
Maybe.fromMaybe ExecState
  p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
s0 (ExecutionFeatureResult
  p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
-> Maybe
     (ExecState
        p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t))
forall p sym ext ret.
ExecutionFeatureResult p sym ext ret
-> Maybe (ExecState p sym ext ret)
resultState ExecutionFeatureResult
  p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
featResult)
      let c :: Context cExt p (ExprBuilder s st fs) ext t
c = EvalResult cExt p (ExprBuilder s st fs) ext t
-> Context cExt p (ExprBuilder s st fs) ext t
forall cExt p sym ext (t :: CrucibleType).
EvalResult cExt p sym ext t -> Context cExt p sym ext t
Eval.evalCtx EvalResult cExt p (ExprBuilder s st fs) ext t
result
      Outputs IO (Response cExt) -> Response cExt -> IO ()
forall (m :: * -> *) a. Outputs m a -> a -> m ()
Outps.send (Context cExt p (ExprBuilder s st fs) ext t
-> Outputs IO (Response cExt)
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> Outputs IO (Response cExt)
Ctxt.dbgOutputs Context cExt p (ExprBuilder s st fs) ext t
c) (EvalResult cExt p (ExprBuilder s st fs) ext t -> Response cExt
forall cExt p sym ext (t :: CrucibleType).
EvalResult cExt p sym ext t -> Response cExt
Eval.evalResp EvalResult cExt p (ExprBuilder s st fs) ext t
result)
      case Context cExt p (ExprBuilder s st fs) ext t -> DebuggerState
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> DebuggerState
Ctxt.dbgState Context cExt p (ExprBuilder s st fs) ext t
c of
        DebuggerState
Ctxt.Quit -> EvalResult cExt p (ExprBuilder s st fs) ext t
-> IO (EvalResult cExt p (ExprBuilder s st fs) ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure EvalResult cExt p (ExprBuilder s st fs) ext t
result
        Ctxt.Running {} -> EvalResult cExt p (ExprBuilder s st fs) ext t
-> IO (EvalResult cExt p (ExprBuilder s st fs) ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure EvalResult cExt p (ExprBuilder s st fs) ext t
result
        DebuggerState
Ctxt.Stopped -> Context cExt p (ExprBuilder s st fs) ext t
-> ExecState
     p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
-> ExecutionFeatureResult
     p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
-> IO (EvalResult cExt p (ExprBuilder s st fs) ext t)
go Context cExt p (ExprBuilder s st fs) ext t
c ExecState
  p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
s ExecutionFeatureResult
  p (ExprBuilder s st fs) ext (RegEntry (ExprBuilder s st fs) t)
featResult

dispatch ::
  (sym ~ W4.ExprBuilder s st fs) =>
  C.IsSymInterface sym =>
  C.IsSyntaxExtension ext =>
  W4.IsExpr (W4.SymExpr sym) =>
  (?parserHooks :: C.ParserHooks ext) =>
  PP.Pretty cExt =>
  Context cExt p sym ext t ->
  C.ExecState p sym ext (C.RegEntry sym t) ->
  IO (Context cExt p sym ext t, C.ExecutionFeatureResult p sym ext (C.RegEntry sym t))
dispatch :: forall sym s (st :: * -> *) fs ext cExt p (t :: CrucibleType).
(sym ~ ExprBuilder s st fs, IsSymInterface sym,
 IsSyntaxExtension ext, IsExpr (SymExpr sym),
 ?parserHooks::ParserHooks ext, Pretty cExt) =>
Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> IO
     (Context cExt p sym ext t,
      ExecutionFeatureResult p sym ext (RegEntry sym t))
dispatch Context cExt p sym ext t
ctx0 ExecState p sym ext (RegEntry sym t)
execState =
  case Context cExt p sym ext t -> DebuggerState
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> DebuggerState
Ctxt.dbgState Context cExt p sym ext t
ctx0 of
    DebuggerState
Ctxt.Quit ->
      (Context cExt p sym ext t,
 ExecutionFeatureResult p sym ext (RegEntry sym t))
-> IO
     (Context cExt p sym ext t,
      ExecutionFeatureResult p sym ext (RegEntry sym t))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t
ctx0, ExecutionFeatureResult p sym ext (RegEntry sym t)
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNoChange)
    Ctxt.Running {} | C.ResultState {} <- ExecState p sym ext (RegEntry sym t)
execState -> do
      let ctx :: Context cExt p sym ext t
ctx = Context cExt p sym ext t
ctx0 { Ctxt.dbgState = Ctxt.Stopped }
      Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> IO
     (Context cExt p sym ext t,
      ExecutionFeatureResult p sym ext (RegEntry sym t))
forall sym s (st :: * -> *) fs ext cExt p (t :: CrucibleType).
(sym ~ ExprBuilder s st fs, IsSymInterface sym,
 IsSyntaxExtension ext, IsExpr (SymExpr sym),
 ?parserHooks::ParserHooks ext, Pretty cExt) =>
Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> IO
     (Context cExt p sym ext t,
      ExecutionFeatureResult p sym ext (RegEntry sym t))
dispatch Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState
    Ctxt.Running (Ctxt.Step Int
i) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
1 -> do
      let ctx :: Context cExt p sym ext t
ctx = Context cExt p sym ext t
ctx0 { Ctxt.dbgState = Ctxt.Stopped }
      Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> IO
     (Context cExt p sym ext t,
      ExecutionFeatureResult p sym ext (RegEntry sym t))
forall sym s (st :: * -> *) fs ext cExt p (t :: CrucibleType).
(sym ~ ExprBuilder s st fs, IsSymInterface sym,
 IsSyntaxExtension ext, IsExpr (SymExpr sym),
 ?parserHooks::ParserHooks ext, Pretty cExt) =>
Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> IO
     (Context cExt p sym ext t,
      ExecutionFeatureResult p sym ext (RegEntry sym t))
dispatch Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState
    Ctxt.Running (Ctxt.Step Int
i) -> do
      let ctx :: Context cExt p sym ext t
ctx = Context cExt p sym ext t
ctx0 { Ctxt.dbgState = Ctxt.Running (Ctxt.Step (i - 1)) }
      DebuggerState
state <- Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t) -> IO DebuggerState
forall cExt p sym ext (t :: CrucibleType) rtp.
Context cExt p sym ext t
-> ExecState p sym ext rtp -> IO DebuggerState
stepState Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState
      let ctx' :: Context cExt p sym ext t
ctx' = Context cExt p sym ext t
ctx0 { Ctxt.dbgState = state }
      (Context cExt p sym ext t,
 ExecutionFeatureResult p sym ext (RegEntry sym t))
-> IO
     (Context cExt p sym ext t,
      ExecutionFeatureResult p sym ext (RegEntry sym t))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t
ctx', ExecutionFeatureResult p sym ext (RegEntry sym t)
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNoChange)
    Ctxt.Running {} -> do
      DebuggerState
state <- Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t) -> IO DebuggerState
forall cExt p sym ext (t :: CrucibleType) rtp.
Context cExt p sym ext t
-> ExecState p sym ext rtp -> IO DebuggerState
stepState Context cExt p sym ext t
ctx0 ExecState p sym ext (RegEntry sym t)
execState
      let ctx :: Context cExt p sym ext t
ctx = Context cExt p sym ext t
ctx0 { Ctxt.dbgState = state }
      (Context cExt p sym ext t,
 ExecutionFeatureResult p sym ext (RegEntry sym t))
-> IO
     (Context cExt p sym ext t,
      ExecutionFeatureResult p sym ext (RegEntry sym t))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t
ctx, ExecutionFeatureResult p sym ext (RegEntry sym t)
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNoChange)
    DebuggerState
Ctxt.Stopped -> do
      EvalResult cExt p sym ext t
result <- Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> IO (EvalResult cExt p sym ext t)
forall sym s (st :: * -> *) fs ext cExt p (t :: CrucibleType).
(sym ~ ExprBuilder s st fs, IsSymInterface sym,
 IsSyntaxExtension ext, ?parserHooks::ParserHooks ext, Pretty cExt,
 IsExpr (SymExpr sym)) =>
Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> IO (EvalResult cExt p sym ext t)
stopped Context cExt p sym ext t
ctx0 ExecState p sym ext (RegEntry sym t)
execState
      (Context cExt p sym ext t,
 ExecutionFeatureResult p sym ext (RegEntry sym t))
-> IO
     (Context cExt p sym ext t,
      ExecutionFeatureResult p sym ext (RegEntry sym t))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (EvalResult cExt p sym ext t -> Context cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
EvalResult cExt p sym ext t -> Context cExt p sym ext t
Eval.evalCtx EvalResult cExt p sym ext t
result, EvalResult cExt p sym ext t
-> ExecutionFeatureResult p sym ext (RegEntry sym t)
forall cExt p sym ext (t :: CrucibleType).
EvalResult cExt p sym ext t
-> ExecutionFeatureResult p sym ext (RegEntry sym t)
Eval.evalFeatureResult EvalResult cExt p sym ext t
result)

debugger ::
  (sym ~ W4.ExprBuilder s st fs) =>
  C.IsSymInterface sym =>
  C.IsSyntaxExtension ext =>
  W4.IsExpr (W4.SymExpr sym) =>
  (?parserHooks :: C.ParserHooks ext) =>
  PP.Pretty cExt =>
  Cmd.CommandExt cExt ->
  Ctxt.ExtImpl cExt p sym ext t ->
  IntrinsicPrinters sym ->
  Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt) ->
  Outputs IO (Response cExt) ->
  C.TypeRepr t ->
  IO (C.ExecutionFeature p sym ext (C.RegEntry sym t))
debugger :: forall sym s (st :: * -> *) fs ext cExt p (t :: CrucibleType).
(sym ~ ExprBuilder s st fs, IsSymInterface sym,
 IsSyntaxExtension ext, IsExpr (SymExpr sym),
 ?parserHooks::ParserHooks ext, Pretty cExt) =>
CommandExt cExt
-> ExtImpl cExt p sym ext t
-> IntrinsicPrinters sym
-> Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
-> Outputs IO (Response cExt)
-> TypeRepr t
-> IO (ExecutionFeature p sym ext (RegEntry sym t))
debugger CommandExt cExt
cExt ExtImpl cExt p sym ext t
impl IntrinsicPrinters sym
iFns Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
ins Outputs IO (Response cExt)
outs TypeRepr t
rTy = do
  IORef (Context cExt p sym ext t)
ctxRef <- Context cExt p sym ext t -> IO (IORef (Context cExt p sym ext t))
forall a. a -> IO (IORef a)
IORef.newIORef (Context cExt p sym ext t -> IO (IORef (Context cExt p sym ext t)))
-> IO (Context cExt p sym ext t)
-> IO (IORef (Context cExt p sym ext t))
forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
=<< CommandExt cExt
-> ExtImpl cExt p sym ext t
-> IntrinsicPrinters sym
-> Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
-> Outputs IO (Response cExt)
-> TypeRepr t
-> IO (Context cExt p sym ext t)
forall sym cExt p ext (t :: CrucibleType).
IsExpr (SymExpr sym) =>
CommandExt cExt
-> ExtImpl cExt p sym ext t
-> IntrinsicPrinters sym
-> Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
-> Outputs IO (Response cExt)
-> TypeRepr t
-> IO (Context cExt p sym ext t)
Ctxt.initCtx CommandExt cExt
cExt ExtImpl cExt p sym ext t
impl IntrinsicPrinters sym
iFns Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
ins Outputs IO (Response cExt)
outs TypeRepr t
rTy
  ExecutionFeature p sym ext (RegEntry sym t)
-> IO (ExecutionFeature p sym ext (RegEntry sym t))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExecutionFeature p sym ext (RegEntry sym t)
 -> IO (ExecutionFeature p sym ext (RegEntry sym t)))
-> ExecutionFeature p sym ext (RegEntry sym t)
-> IO (ExecutionFeature p sym ext (RegEntry sym t))
forall a b. (a -> b) -> a -> b
$
    (ExecState p sym ext (RegEntry sym t)
 -> IO (ExecutionFeatureResult p sym ext (RegEntry sym t)))
-> ExecutionFeature p sym ext (RegEntry sym t)
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 (RegEntry sym t)
  -> IO (ExecutionFeatureResult p sym ext (RegEntry sym t)))
 -> ExecutionFeature p sym ext (RegEntry sym t))
-> (ExecState p sym ext (RegEntry sym t)
    -> IO (ExecutionFeatureResult p sym ext (RegEntry sym t)))
-> ExecutionFeature p sym ext (RegEntry sym t)
forall a b. (a -> b) -> a -> b
$ \ExecState p sym ext (RegEntry sym t)
execState -> do
      Context cExt p sym ext t
ctx0 <- IORef (Context cExt p sym ext t) -> IO (Context cExt p sym ext t)
forall a. IORef a -> IO a
IORef.readIORef IORef (Context cExt p sym ext t)
ctxRef
      (Context cExt p sym ext t
ctx, ExecutionFeatureResult p sym ext (RegEntry sym t)
featResult) <- Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> IO
     (Context cExt p sym ext t,
      ExecutionFeatureResult p sym ext (RegEntry sym t))
forall sym s (st :: * -> *) fs ext cExt p (t :: CrucibleType).
(sym ~ ExprBuilder s st fs, IsSymInterface sym,
 IsSyntaxExtension ext, IsExpr (SymExpr sym),
 ?parserHooks::ParserHooks ext, Pretty cExt) =>
Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> IO
     (Context cExt p sym ext t,
      ExecutionFeatureResult p sym ext (RegEntry sym t))
dispatch Context cExt p sym ext t
ctx0 ExecState p sym ext (RegEntry sym t)
execState
      IORef (Context cExt p sym ext t)
-> Context cExt p sym ext t -> IO ()
forall a. IORef a -> a -> IO ()
IORef.writeIORef IORef (Context cExt p sym ext t)
ctxRef Context cExt p sym ext t
ctx
      ExecutionFeatureResult p sym ext (RegEntry sym t)
-> IO (ExecutionFeatureResult p sym ext (RegEntry sym t))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ExecutionFeatureResult p sym ext (RegEntry sym t)
featResult

-- | Like 'bareDebugger', but with a syntax extension
bareDebuggerExt ::
  C.IsSyntaxExtension ext =>
  (?parserHooks :: C.ParserHooks ext) =>
  PP.Pretty cExt =>
  Cmd.CommandExt cExt ->
  (forall p sym t. C.IsSymInterface sym => Ctxt.ExtImpl cExt p sym ext t) ->
  (forall p sym. C.IsSymInterface sym => C.ExtensionImpl p sym ext) ->
  Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt) ->
  Outputs IO (Response cExt) ->
  (Text -> IO ()) ->
  IO ()
bareDebuggerExt :: forall ext cExt.
(IsSyntaxExtension ext, ?parserHooks::ParserHooks ext,
 Pretty cExt) =>
CommandExt cExt
-> (forall p sym (t :: CrucibleType).
    IsSymInterface sym =>
    ExtImpl cExt p sym ext t)
-> (forall p sym. IsSymInterface sym => ExtensionImpl p sym ext)
-> Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
-> Outputs IO (Response cExt)
-> (Text -> IO ())
-> IO ()
bareDebuggerExt CommandExt cExt
cExts forall p sym (t :: CrucibleType).
IsSymInterface sym =>
ExtImpl cExt p sym ext t
cEval forall p sym. IsSymInterface sym => ExtensionImpl p sym ext
extImpl Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
inps Outputs IO (Response cExt)
outps Text -> IO ()
logger = do
  Some NonceGenerator IO x
nonceGen <- IO (Some (NonceGenerator IO))
Nonce.newIONonceGenerator
  HandleAllocator
ha <- IO HandleAllocator
C.newHandleAllocator
  ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)
sym <- FloatModeRepr 'FloatIEEE
-> EmptyExprBuilderState x
-> NonceGenerator IO x
-> IO (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
forall (fm :: FloatMode) (st :: * -> *) t.
FloatModeRepr fm
-> st t -> NonceGenerator IO t -> IO (ExprBuilder t st (Flags fm))
W4.newExprBuilder FloatModeRepr 'FloatIEEE
W4.FloatIEEERepr EmptyExprBuilderState x
forall t. EmptyExprBuilderState t
W4.EmptyExprBuilderState NonceGenerator IO x
nonceGen
  SimpleBackend x EmptyExprBuilderState (Flags 'FloatIEEE)
bak <- ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)
-> IO (SimpleBackend x EmptyExprBuilderState (Flags 'FloatIEEE))
forall t (st :: * -> *) fs.
ExprBuilder t st fs -> IO (SimpleBackend t st fs)
C.newSimpleBackend ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)
sym
  let retType :: TypeRepr 'UnitType
retType = TypeRepr 'UnitType
C.UnitRepr
  let fns :: FunctionBindings p sym ext
fns = FnHandleMap (FnState p sym ext) -> FunctionBindings p sym ext
forall p sym ext.
FnHandleMap (FnState p sym ext) -> FunctionBindings p sym ext
C.FnBindings FnHandleMap (FnState p sym ext)
forall (f :: Ctx CrucibleType -> CrucibleType -> *). FnHandleMap f
C.emptyHandleMap
  let simCtx :: SimContext
  () (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)) ext
simCtx = SimpleBackend x EmptyExprBuilderState (Flags 'FloatIEEE)
-> IntrinsicTypes
     (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
-> HandleAllocator
-> Handle
-> FunctionBindings
     () (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)) ext
-> ExtensionImpl
     () (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)) ext
-> ()
-> SimContext
     () (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)) ext
forall sym bak personality ext.
IsSymBackend sym bak =>
bak
-> IntrinsicTypes sym
-> HandleAllocator
-> Handle
-> FunctionBindings personality sym ext
-> ExtensionImpl personality sym ext
-> personality
-> SimContext personality sym ext
C.initSimContext SimpleBackend x EmptyExprBuilderState (Flags 'FloatIEEE)
bak IntrinsicTypes
  (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
forall sym. IntrinsicTypes sym
C.emptyIntrinsicTypes HandleAllocator
ha Handle
stdout FunctionBindings
  () (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)) ext
forall {p} {sym} {ext}. FunctionBindings p sym ext
fns ExtensionImpl
  () (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)) ext
forall p sym. IsSymInterface sym => ExtensionImpl p sym ext
extImpl ()
  let ov :: ExecCont p sym ext rtp (OverrideLang 'UnitType) ('Just args)
ov = TypeRepr 'UnitType
-> OverrideSim
     p sym ext rtp args 'UnitType (RegValue sym 'UnitType)
-> ExecCont p sym ext rtp (OverrideLang 'UnitType) ('Just args)
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 'UnitType
retType (OverrideSim p sym ext rtp args 'UnitType (RegValue sym 'UnitType)
 -> ExecCont p sym ext rtp (OverrideLang 'UnitType) ('Just args))
-> OverrideSim
     p sym ext rtp args 'UnitType (RegValue sym 'UnitType)
-> ExecCont p sym ext rtp (OverrideLang 'UnitType) ('Just args)
forall a b. (a -> b) -> a -> b
$ () -> OverrideSim p sym ext rtp args 'UnitType ()
forall a. a -> OverrideSim p sym ext rtp args 'UnitType a
forall (m :: * -> *) a. Monad m => a -> m a
return ()
  let simSt :: ExecState
  ()
  (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
  ext
  (RegEntry
     (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)) 'UnitType)
simSt  = SimContext
  () (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)) ext
-> SymGlobalState
     (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
-> AbortHandler
     ()
     (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
     ext
     (RegEntry
        (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)) 'UnitType)
-> TypeRepr 'UnitType
-> ExecCont
     ()
     (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
     ext
     (RegEntry
        (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)) 'UnitType)
     (OverrideLang 'UnitType)
     ('Just EmptyCtx)
-> ExecState
     ()
     (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
     ext
     (RegEntry
        (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)) 'UnitType)
forall p sym ext rtp (ret :: CrucibleType).
(rtp ~ RegEntry sym ret) =>
SimContext p sym ext
-> SymGlobalState sym
-> AbortHandler p sym ext (RegEntry sym ret)
-> TypeRepr ret
-> ExecCont
     p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
-> ExecState p sym ext rtp
C.InitialState SimContext
  () (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)) ext
simCtx SymGlobalState
  (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
forall sym. SymGlobalState sym
C.emptyGlobals AbortHandler
  ()
  (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
  ext
  (RegEntry
     (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)) 'UnitType)
forall sym p ext rtp.
IsSymInterface sym =>
AbortHandler p sym ext rtp
C.defaultAbortHandler TypeRepr 'UnitType
retType ExecCont
  ()
  (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
  ext
  (RegEntry
     (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)) 'UnitType)
  (OverrideLang 'UnitType)
  ('Just EmptyCtx)
forall {p} {sym} {ext} {rtp} {args :: Ctx CrucibleType}.
ExecCont p sym ext rtp (OverrideLang 'UnitType) ('Just args)
ov
  ExecutionFeature
  ()
  (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
  ext
  (RegEntry
     (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)) 'UnitType)
dbgr <- do
    let iFns :: IntrinsicPrinters sym
iFns = MapF SymbolRepr (IntrinsicPrettyFn sym) -> IntrinsicPrinters sym
forall sym.
MapF SymbolRepr (IntrinsicPrettyFn sym) -> IntrinsicPrinters sym
IntrinsicPrinters MapF SymbolRepr (IntrinsicPrettyFn sym)
forall {v} (k :: v -> *) (a :: v -> *). MapF k a
MapF.empty
    CommandExt cExt
-> ExtImpl
     cExt
     ()
     (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
     ext
     'UnitType
-> IntrinsicPrinters
     (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
-> Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
-> Outputs IO (Response cExt)
-> TypeRepr 'UnitType
-> IO
     (ExecutionFeature
        ()
        (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
        ext
        (RegEntry
           (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
           'UnitType))
forall sym s (st :: * -> *) fs ext cExt p (t :: CrucibleType).
(sym ~ ExprBuilder s st fs, IsSymInterface sym,
 IsSyntaxExtension ext, IsExpr (SymExpr sym),
 ?parserHooks::ParserHooks ext, Pretty cExt) =>
CommandExt cExt
-> ExtImpl cExt p sym ext t
-> IntrinsicPrinters sym
-> Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
-> Outputs IO (Response cExt)
-> TypeRepr t
-> IO (ExecutionFeature p sym ext (RegEntry sym t))
debugger CommandExt cExt
cExts ExtImpl
  cExt
  ()
  (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
  ext
  'UnitType
forall p sym (t :: CrucibleType).
IsSymInterface sym =>
ExtImpl cExt p sym ext t
cEval IntrinsicPrinters
  (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
forall {sym}. IntrinsicPrinters sym
iFns Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
inps Outputs IO (Response cExt)
outps TypeRepr 'UnitType
retType
  IO
  (ExecResult
     ()
     (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
     ext
     (RegEntry
        (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
        'UnitType))
-> IO ()
forall (f :: * -> *) a. Functor f => f a -> f ()
Monad.void (IO
   (ExecResult
      ()
      (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
      ext
      (RegEntry
         (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
         'UnitType))
 -> IO ())
-> IO
     (ExecResult
        ()
        (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
        ext
        (RegEntry
           (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
           'UnitType))
-> IO ()
forall a b. (a -> b) -> a -> b
$ [ExecutionFeature
   ()
   (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
   ext
   (RegEntry
      (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
      'UnitType)]
-> ExecState
     ()
     (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
     ext
     (RegEntry
        (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)) 'UnitType)
-> IO
     (ExecResult
        ()
        (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
        ext
        (RegEntry
           (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
           'UnitType))
forall p sym ext rtp.
(IsSymInterface sym, IsSyntaxExtension ext) =>
[ExecutionFeature p sym ext rtp]
-> ExecState p sym ext rtp -> IO (ExecResult p sym ext rtp)
C.executeCrucible [ExecutionFeature
  ()
  (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
  ext
  (RegEntry
     (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)) 'UnitType)
dbgr] ExecState
  ()
  (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
  ext
  (RegEntry
     (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE)) 'UnitType)
simSt
  SimpleBackend x EmptyExprBuilderState (Flags 'FloatIEEE)
-> IO
     (Maybe
        (Goals
           (CrucibleAssumptions
              (SymExpr (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))))
           (LabeledPred
              (SymExpr
                 (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
                 BaseBoolType)
              SimError)))
forall sym bak.
IsSymBackend sym bak =>
bak -> IO (ProofObligations sym)
C.getProofObligations SimpleBackend x EmptyExprBuilderState (Flags 'FloatIEEE)
bak IO
  (Maybe
     (Goals
        (CrucibleAssumptions
           (SymExpr (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))))
        (LabeledPred
           (SymExpr
              (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
              BaseBoolType)
           SimError)))
-> (Maybe
      (Goals
         (CrucibleAssumptions
            (SymExpr (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))))
         (LabeledPred
            (SymExpr
               (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
               BaseBoolType)
            SimError))
    -> IO ())
-> IO ()
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe
  (Goals
     (CrucibleAssumptions
        (SymExpr (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))))
     (LabeledPred
        (SymExpr
           (ExprBuilder x EmptyExprBuilderState (Flags 'FloatIEEE))
           BaseBoolType)
        SimError))
Nothing -> () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    Just {} -> do
      Text -> IO ()
logger Text
"There were unhandled proof obligations! Try `prove` and `clear`."
      IO ()
forall a. IO a
Exit.exitFailure

-- | Start a debugger instance in an empty Crucible program.
--
-- The Crucible program simply returns the unit value. The idea is to use the
-- @Load@ and @Call@ commands to actually run some Crucible CFG(s).
--
-- Proves obligations using Z3.
bareDebugger ::
  Inputs (CompletionT Void (StyleT Void IO)) (Statement Void) ->
  Outputs IO (Response Void) ->
  (Text -> IO ()) ->
  IO ()
bareDebugger :: Inputs (CompletionT Void (StyleT Void IO)) (Statement Void)
-> Outputs IO (Response Void) -> (Text -> IO ()) -> IO ()
bareDebugger Inputs (CompletionT Void (StyleT Void IO)) (Statement Void)
inps Outputs IO (Response Void)
outps Text -> IO ()
logger =
  let ?parserHooks = (forall (m :: * -> *). MonadSyntax Atomic m => m (Some TypeRepr))
-> (forall s (m :: * -> *).
    (MonadSyntax Atomic m, MonadWriter [Posd (Stmt () s)] m,
     MonadState (SyntaxState s) m, MonadIO m, IsSyntaxExtension (),
     ?parserHooks::ParserHooks ()) =>
    m (Some (Atom s)))
-> ParserHooks ()
forall ext.
(forall (m :: * -> *). MonadSyntax Atomic m => m (Some TypeRepr))
-> (forall s (m :: * -> *).
    (MonadSyntax Atomic m, MonadWriter [Posd (Stmt ext s)] m,
     MonadState (SyntaxState s) m, MonadIO m, IsSyntaxExtension ext,
     ?parserHooks::ParserHooks ext) =>
    m (Some (Atom s)))
-> ParserHooks ext
C.ParserHooks m (Some TypeRepr)
forall a. m a
forall (f :: * -> *) a. Alternative f => f a
forall (m :: * -> *). MonadSyntax Atomic m => m (Some TypeRepr)
Applicative.empty m (Some (Atom s))
forall a. m a
forall s (m :: * -> *).
(MonadSyntax Atomic m, MonadWriter [Posd (Stmt () s)] m,
 MonadState (SyntaxState s) m, MonadIO m, IsSyntaxExtension (),
 ?parserHooks::ParserHooks ()) =>
m (Some (Atom s))
forall (f :: * -> *) a. Alternative f => f a
Applicative.empty in
  CommandExt Void
-> (forall p sym (t :: CrucibleType).
    IsSymInterface sym =>
    ExtImpl Void p sym () t)
-> (forall p sym. IsSymInterface sym => ExtensionImpl p sym ())
-> Inputs (CompletionT Void (StyleT Void IO)) (Statement Void)
-> Outputs IO (Response Void)
-> (Text -> IO ())
-> IO ()
forall ext cExt.
(IsSyntaxExtension ext, ?parserHooks::ParserHooks ext,
 Pretty cExt) =>
CommandExt cExt
-> (forall p sym (t :: CrucibleType).
    IsSymInterface sym =>
    ExtImpl cExt p sym ext t)
-> (forall p sym. IsSymInterface sym => ExtensionImpl p sym ext)
-> Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
-> Outputs IO (Response cExt)
-> (Text -> IO ())
-> IO ()
bareDebuggerExt
    CommandExt Void
Cmd.voidExts
    ExtImpl Void p sym () t
forall p sym ext (t :: CrucibleType). ExtImpl Void p sym ext t
forall p sym (t :: CrucibleType).
IsSymInterface sym =>
ExtImpl Void p sym () t
Ctxt.voidImpl
    ExtensionImpl p sym ()
forall p sym. ExtensionImpl p sym ()
forall p sym. IsSymInterface sym => ExtensionImpl p sym ()
C.emptyExtensionImpl
    Inputs (CompletionT Void (StyleT Void IO)) (Statement Void)
inps
    Outputs IO (Response Void)
outps
    Text -> IO ()
logger