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

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE ImplicitParams #-}
{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE TypeOperators #-}

module Lang.Crucible.Debug.Eval
  ( Ctxt.EvalResult(..)
  , eval
  ) where

import Control.Lens qualified as Lens
import Data.Maybe qualified as Maybe
import Data.Set qualified as Set
import Data.Text qualified as Text
import Lang.Crucible.Backend qualified as C
import Lang.Crucible.CFG.Extension qualified as C
import Lang.Crucible.Debug.Arg qualified as Arg
import Lang.Crucible.Debug.Breakpoint (Breakpoint(BreakFunction))
import Lang.Crucible.Debug.Command.Base qualified as BCmd
import Lang.Crucible.Debug.Command qualified as Cmd
import Lang.Crucible.Debug.Commands qualified as Cmds
import Lang.Crucible.Debug.Context (Context)
import Lang.Crucible.Debug.Context qualified as Ctxt
import Lang.Crucible.Debug.Regex qualified as Rgx
import Lang.Crucible.Debug.Response qualified as Resp
import Lang.Crucible.Debug.Statement qualified as Stmt
import Lang.Crucible.Debug.Statement (Statement)
import Lang.Crucible.Debug.Trace qualified as Trace
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 Prettyprinter qualified as PP
import What4.Expr.Builder qualified as W4
import What4.Interface qualified as W4

runCmd ::
  Context cExt p sym ext t ->
  C.ExecState p sym ext (C.RegEntry sym t) ->
  Ctxt.RunningState ->
  IO (Ctxt.EvalResult cExt p sym ext t)
runCmd :: forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> RunningState
-> IO (EvalResult cExt p sym ext t)
runCmd Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState RunningState
runState =
  case ExecState p sym ext (RegEntry sym t)
execState of
    C.ResultState {} ->
      let resp :: Response cExt
resp = UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (NotApplicable -> UserError cExt
forall cExt. NotApplicable -> UserError cExt
Resp.NotApplicable NotApplicable
Resp.DoneSimulating) in
      EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = resp }
    ExecState p sym ext (RegEntry sym t)
_ -> EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalCtx = ctx { Ctxt.dbgState = Ctxt.Running runState  } }

-- | Helper, not exported
def :: Context cExt p sym ext t -> Ctxt.EvalResult cExt p sym ext t
def :: forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx = Context cExt p sym ext t
-> ExecutionFeatureResult p sym ext (RegEntry sym t)
-> Response cExt
-> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t
-> ExecutionFeatureResult p sym ext (RegEntry sym t)
-> Response cExt
-> EvalResult cExt p sym ext t
Ctxt.EvalResult 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 Response cExt
forall {cExt}. Response cExt
Resp.Ok

baseImpl ::
  (sym ~ W4.ExprBuilder s st fs) =>
  C.IsSymInterface sym =>
  C.IsSyntaxExtension ext =>
  (?parserHooks :: C.ParserHooks ext) =>
  PP.Pretty cExt =>
  W4.IsExpr (W4.SymExpr sym) =>
  BCmd.BaseCommand ->
  Ctxt.CommandImpl cExt p sym ext t
baseImpl :: 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)) =>
BaseCommand -> CommandImpl cExt p sym ext t
baseImpl =
  \case
    BaseCommand
BCmd.Backtrace ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr Empty
Ctxt.implRegex = RegexRepr ArgTypeRepr Empty
BCmd.rBacktrace
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) Empty
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState Match (Arg cExt) Empty
Rgx.MEmpty -> do
          Response cExt
resp <- ExecState p sym ext (RegEntry sym t) -> IO (Response cExt)
forall p sym ext r cExt.
ExecState p sym ext r -> IO (Response cExt)
Cmds.backtrace ExecState p sym ext (RegEntry sym t)
execState
          EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = resp }
      }

    BaseCommand
BCmd.Block ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr Empty
Ctxt.implRegex = RegexRepr ArgTypeRepr Empty
BCmd.rBlock
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) Empty
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState Match (Arg cExt) Empty
Rgx.MEmpty -> do
          Response cExt
resp <- Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t) -> IO (Response cExt)
forall ext sym cExt p (t :: CrucibleType) r.
(IsSyntaxExtension ext, IsExpr (SymExpr sym)) =>
Context cExt p sym ext t
-> ExecState p sym ext r -> IO (Response cExt)
Cmds.block Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState
          EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = resp }
      }

    BaseCommand
BCmd.Break ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr Function
Ctxt.implRegex = RegexRepr ArgTypeRepr Function
BCmd.rBreak
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) Function
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
_execState (Rgx.MLit (Arg.AFunction FunctionName
fNm)) -> do
          let bs :: Set Breakpoint
bs = Breakpoint -> Set Breakpoint -> Set Breakpoint
forall a. Ord a => a -> Set a -> Set a
Set.insert (FunctionName -> Breakpoint
BreakFunction FunctionName
fNm) (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)
          EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalCtx = ctx { Ctxt.dbgBreakpoints = bs } }
      }

    BaseCommand
BCmd.Call ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr Function
Ctxt.implRegex = RegexRepr ArgTypeRepr Function
BCmd.rCall
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) Function
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState (Rgx.MLit (Arg.AFunction FunctionName
fNm)) -> do
          (ExecutionFeatureResult p sym ext (RegEntry sym t)
featRes, Response cExt
resp) <- ExecState p sym ext (RegEntry sym t)
-> TypeRepr t
-> FunctionName
-> IO
     (ExecutionFeatureResult p sym ext (RegEntry sym t), Response cExt)
forall sym ext p (t :: CrucibleType) cExt.
(IsSymInterface sym, IsSyntaxExtension ext) =>
ExecState p sym ext (RegEntry sym t)
-> TypeRepr t
-> FunctionName
-> IO
     (ExecutionFeatureResult p sym ext (RegEntry sym t), Response cExt)
Cmds.call ExecState p sym ext (RegEntry sym t)
execState (Context cExt p sym ext t -> TypeRepr t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> TypeRepr t
Ctxt.dbgRetTy Context cExt p sym ext t
ctx) FunctionName
fNm
          EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalFeatureResult = featRes, Ctxt.evalResp = resp }
      }

    BaseCommand
BCmd.Cfg ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr (Empty :| Function)
Ctxt.implRegex = RegexRepr ArgTypeRepr (Empty :| Function)
BCmd.rCfg
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) (Empty :| Function)
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState Match (Arg cExt) (Empty :| Function)
m ->
          case Match (Arg cExt) (Empty :| Function)
m of
            Rgx.MLeft Match (Arg cExt) l
Rgx.MEmpty -> do
              Response cExt
resp <- ExecState p sym ext (RegEntry sym t)
-> Maybe FunctionName -> IO (Response cExt)
forall ext p sym r cExt.
IsSyntaxExtension ext =>
ExecState p sym ext r -> Maybe FunctionName -> IO (Response cExt)
Cmds.cfg ExecState p sym ext (RegEntry sym t)
execState Maybe FunctionName
forall a. Maybe a
Nothing
              EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = resp }
            Rgx.MRight (Rgx.MLit (Arg.AFunction FunctionName
fNm)) -> do
              (ExecutionFeatureResult p sym ext (RegEntry sym t)
featRes, Response cExt
resp) <- ExecState p sym ext (RegEntry sym t)
-> TypeRepr t
-> FunctionName
-> IO
     (ExecutionFeatureResult p sym ext (RegEntry sym t), Response cExt)
forall sym ext p (t :: CrucibleType) cExt.
(IsSymInterface sym, IsSyntaxExtension ext) =>
ExecState p sym ext (RegEntry sym t)
-> TypeRepr t
-> FunctionName
-> IO
     (ExecutionFeatureResult p sym ext (RegEntry sym t), Response cExt)
Cmds.call ExecState p sym ext (RegEntry sym t)
execState (Context cExt p sym ext t -> TypeRepr t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> TypeRepr t
Ctxt.dbgRetTy Context cExt p sym ext t
ctx) FunctionName
fNm
              EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalFeatureResult = featRes, Ctxt.evalResp = resp }
      }

    BaseCommand
BCmd.Clear ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr Empty
Ctxt.implRegex = RegexRepr ArgTypeRepr Empty
BCmd.rClear
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) Empty
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState Match (Arg cExt) Empty
Rgx.MEmpty ->
          SimContext p sym ext
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (EvalResult cExt p sym ext t))
-> IO (EvalResult cExt p sym ext t)
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
C.withBackend (ExecState p sym ext (RegEntry sym t) -> SimContext p sym ext
forall p sym ext r. ExecState p sym ext r -> SimContext p sym ext
C.execStateContext ExecState p sym ext (RegEntry sym t)
execState) ((forall {bak}.
  IsSymBackend sym bak =>
  bak -> IO (EvalResult cExt p sym ext t))
 -> IO (EvalResult cExt p sym ext t))
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (EvalResult cExt p sym ext t))
-> IO (EvalResult cExt p sym ext t)
forall a b. (a -> b) -> a -> b
$ \bak
bak -> do
            Int
n <- Maybe
  (Goals
     (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
     (LabeledPred
        (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError))
-> Int
forall a. Maybe a -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (Maybe
   (Goals
      (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
      (LabeledPred
         (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError))
 -> Int)
-> IO
     (Maybe
        (Goals
           (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
           (LabeledPred
              (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError)))
-> IO Int
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> bak
-> IO
     (Maybe
        (Goals
           (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
           (LabeledPred
              (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError)))
forall sym bak.
IsSymBackend sym bak =>
bak -> IO (ProofObligations sym)
C.getProofObligations bak
bak
            bak -> IO ()
forall sym bak. IsSymBackend sym bak => bak -> IO ()
C.clearProofObligations bak
bak
            EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = Resp.Clear n }
      }

    BaseCommand
BCmd.Comment ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr (Star Text)
Ctxt.implRegex = RegexRepr ArgTypeRepr (Star Text)
BCmd.rComment
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) (Star Text)
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
_execState (Rgx.MStar [Match (Arg cExt) r1]
_) -> EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx)
      }

    BaseCommand
BCmd.Delete ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr Breakpoint
Ctxt.implRegex = RegexRepr ArgTypeRepr Breakpoint
BCmd.rDelete
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) Breakpoint
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
_execState (Rgx.MLit (Arg.ABreakpoint bp :: Breakpoint
bp@(BreakFunction FunctionName
fNm))) -> do
          let bs0 :: Set Breakpoint
bs0 = 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
          let wasElem :: Bool
wasElem = Breakpoint -> Set Breakpoint -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member Breakpoint
bp Set Breakpoint
bs0
          let bs :: Set Breakpoint
bs = Breakpoint -> Set Breakpoint -> Set Breakpoint
forall a. Ord a => a -> Set a -> Set a
Set.delete Breakpoint
bp Set Breakpoint
bs0
          EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx)
            { Ctxt.evalCtx = ctx { Ctxt.dbgBreakpoints = bs }
            , Ctxt.evalResp = Resp.Delete fNm wasElem
            }
      }

    BaseCommand
BCmd.Done ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr Empty
Ctxt.implRegex = RegexRepr ArgTypeRepr Empty
BCmd.rDone
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) Empty
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState Match (Arg cExt) Empty
Rgx.MEmpty -> do
          case ExecState p sym ext (RegEntry sym t)
execState of
            C.ResultState {} ->
              EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalCtx = ctx { Ctxt.dbgState = Ctxt.Quit } }
            ExecState p sym ext (RegEntry sym t)
_ ->
              let resp :: Response cExt
resp = UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (NotApplicable -> UserError cExt
forall cExt. NotApplicable -> UserError cExt
Resp.NotApplicable NotApplicable
Resp.NotDone) in
              EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = resp }
      }

    BaseCommand
BCmd.Frame ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr Empty
Ctxt.implRegex = RegexRepr ArgTypeRepr Empty
BCmd.rFrame
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) Empty
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState Match (Arg cExt) Empty
Rgx.MEmpty -> do
          Response cExt
resp <- Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t) -> IO (Response cExt)
forall ext sym cExt p (t :: CrucibleType) r.
(IsSyntaxExtension ext, IsExpr (SymExpr sym)) =>
Context cExt p sym ext t
-> ExecState p sym ext r -> IO (Response cExt)
Cmds.frame Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState
          EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = resp }
      }

    BaseCommand
BCmd.Finish ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr Empty
Ctxt.implRegex = RegexRepr ArgTypeRepr Empty
BCmd.rFinish
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) Empty
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState Match (Arg cExt) Empty
Rgx.MEmpty ->
          Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> RunningState
-> IO (EvalResult cExt p sym ext t)
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> RunningState
-> IO (EvalResult cExt p sym ext t)
runCmd Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState RunningState
Ctxt.Finish
      }

    BaseCommand
BCmd.Help ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr (Empty :| Command)
Ctxt.implRegex = RegexRepr ArgTypeRepr (Empty :| Command)
BCmd.rHelp
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) (Empty :| Command)
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
_execState Match (Arg cExt) (Empty :| Command)
m ->
        case Match (Arg cExt) (Empty :| Command)
m of
          Rgx.MLeft Match (Arg cExt) l
Rgx.MEmpty ->
            EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = Cmds.help (Ctxt.dbgCommandExt ctx) Nothing }
          Rgx.MRight (Rgx.MLit (Arg.ACommand Command cExt
cmd)) ->
            EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = Cmds.help (Ctxt.dbgCommandExt ctx) (Just cmd) }

      }

    BaseCommand
BCmd.Load ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr Path
Ctxt.implRegex = RegexRepr ArgTypeRepr Path
BCmd.rLoad
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) Path
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState (Rgx.MLit (Arg.APath Text
path)) -> do
          (ExecutionFeatureResult p sym ext (RegEntry sym t)
featRes, Response cExt
resp) <- ExecState p sym ext (RegEntry sym t)
-> FilePath
-> IO
     (ExecutionFeatureResult p sym ext (RegEntry sym t), Response cExt)
forall ext p sym r cExt.
(IsSyntaxExtension ext, ?parserHooks::ParserHooks ext) =>
ExecState p sym ext r
-> FilePath
-> IO (ExecutionFeatureResult p sym ext r, Response cExt)
Cmds.load ExecState p sym ext (RegEntry sym t)
execState (Text -> FilePath
Text.unpack Text
path)
          EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalFeatureResult = featRes, Ctxt.evalResp = resp }
      }

    BaseCommand
BCmd.Location ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr Empty
Ctxt.implRegex = RegexRepr ArgTypeRepr Empty
BCmd.rLocation
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) Empty
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState Match (Arg cExt) Empty
Rgx.MEmpty -> do
          let stateCtx :: SimContext p sym ext
stateCtx = ExecState p sym ext (RegEntry sym t) -> SimContext p sym ext
forall p sym ext r. ExecState p sym ext r -> SimContext p sym ext
C.execStateContext ExecState p sym ext (RegEntry sym t)
execState
          let sym :: sym
sym = SimContext p sym ext
stateCtx SimContext p sym ext
-> Getting sym (SimContext p sym ext) sym -> sym
forall s a. s -> Getting a s a -> a
Lens.^. Getting sym (SimContext p sym ext) sym
forall p sym ext (f :: * -> *).
(Contravariant f, Functor f) =>
(sym -> f sym) -> SimContext p sym ext -> f (SimContext p sym ext)
C.ctxSymInterface
          ProgramLoc
loc <- sym -> IO ProgramLoc
forall sym. IsExprBuilder sym => sym -> IO ProgramLoc
W4.getCurrentProgramLoc sym
sym
          EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = Resp.Location loc }
      }

    BaseCommand
BCmd.Obligation ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr Empty
Ctxt.implRegex = RegexRepr ArgTypeRepr Empty
BCmd.rObligation
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) Empty
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState Match (Arg cExt) Empty
Rgx.MEmpty ->
          SimContext p sym ext
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (EvalResult cExt p sym ext t))
-> IO (EvalResult cExt p sym ext t)
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
C.withBackend (ExecState p sym ext (RegEntry sym t) -> SimContext p sym ext
forall p sym ext r. ExecState p sym ext r -> SimContext p sym ext
C.execStateContext ExecState p sym ext (RegEntry sym t)
execState) ((forall {bak}.
  IsSymBackend sym bak =>
  bak -> IO (EvalResult cExt p sym ext t))
 -> IO (EvalResult cExt p sym ext t))
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (EvalResult cExt p sym ext t))
-> IO (EvalResult cExt p sym ext t)
forall a b. (a -> b) -> a -> b
$ \bak
bak -> do
          Maybe
  (Goals
     (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
     (LabeledPred
        (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError))
obls <- bak
-> IO
     (Maybe
        (Goals
           (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
           (LabeledPred
              (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError)))
forall sym bak.
IsSymBackend sym bak =>
bak -> IO (ProofObligations sym)
C.getProofObligations bak
bak
          let goals :: [ProofGoal
   (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
   (LabeledPred
      (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError)]
goals = [ProofGoal
   (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
   (LabeledPred
      (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError)]
-> Maybe
     [ProofGoal
        (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
        (LabeledPred
           (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError)]
-> [ProofGoal
      (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
      (LabeledPred
         (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError)]
forall a. a -> Maybe a -> a
Maybe.fromMaybe [] (Goals
  (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
  (LabeledPred (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError)
-> [ProofGoal
      (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
      (LabeledPred
         (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError)]
forall asmp goal.
Monoid asmp =>
Goals asmp goal -> [ProofGoal asmp goal]
C.goalsToList (Goals
   (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
   (LabeledPred (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError)
 -> [ProofGoal
       (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
       (LabeledPred
          (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError)])
-> Maybe
     (Goals
        (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
        (LabeledPred
           (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError))
-> Maybe
     [ProofGoal
        (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
        (LabeledPred
           (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError)]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe
  (Goals
     (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
     (LabeledPred
        (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError))
obls)
          let sym :: ExprBuilder s st fs
sym = bak -> ExprBuilder s st fs
forall sym bak. HasSymInterface sym bak => bak -> sym
C.backendGetSym bak
bak
          [Doc Void]
prettyGoals <- (ProofGoal
   (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
   (LabeledPred (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError)
 -> IO (Doc Void))
-> [ProofGoal
      (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
      (LabeledPred
         (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError)]
-> IO [Doc Void]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (ExprBuilder s st fs
-> ProofGoal
     (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
     (LabeledPred (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError)
-> IO (Doc Void)
forall sym ann.
IsExprBuilder sym =>
sym -> ProofObligation sym -> IO (Doc ann)
C.ppProofObligation ExprBuilder s st fs
sym) [ProofGoal
   (CrucibleAssumptions (SymExpr (ExprBuilder s st fs)))
   (LabeledPred
      (SymExpr (ExprBuilder s st fs) BaseBoolType) SimError)]
goals
          EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = Resp.Obligation prettyGoals }
      }

    BaseCommand
BCmd.PathCondition ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr Empty
Ctxt.implRegex = RegexRepr ArgTypeRepr Empty
BCmd.rPathCondition
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) Empty
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState Match (Arg cExt) Empty
Rgx.MEmpty ->
          SimContext p sym ext
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (EvalResult cExt p sym ext t))
-> IO (EvalResult cExt p sym ext t)
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
C.withBackend (ExecState p sym ext (RegEntry sym t) -> SimContext p sym ext
forall p sym ext r. ExecState p sym ext r -> SimContext p sym ext
C.execStateContext ExecState p sym ext (RegEntry sym t)
execState) ((forall {bak}.
  IsSymBackend sym bak =>
  bak -> IO (EvalResult cExt p sym ext t))
 -> IO (EvalResult cExt p sym ext t))
-> (forall {bak}.
    IsSymBackend sym bak =>
    bak -> IO (EvalResult cExt p sym ext t))
-> IO (EvalResult cExt p sym ext t)
forall a b. (a -> b) -> a -> b
$ \bak
bak -> do
            Doc Void
pathCond <- SymExpr (ExprBuilder s st fs) BaseBoolType -> Doc Void
forall (tp :: BaseType) ann.
SymExpr (ExprBuilder s st fs) tp -> Doc ann
forall (e :: BaseType -> *) (tp :: BaseType) ann.
IsExpr e =>
e tp -> Doc ann
W4.printSymExpr (SymExpr (ExprBuilder s st fs) BaseBoolType -> Doc Void)
-> IO (SymExpr (ExprBuilder s st fs) BaseBoolType) -> IO (Doc Void)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> bak -> IO (SymExpr (ExprBuilder s st fs) BaseBoolType)
forall sym bak. IsSymBackend sym bak => bak -> IO (Pred sym)
C.getPathCondition bak
bak
            EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = Resp.PathCondition pathCond }
      }

    BaseCommand
BCmd.Prove ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr Empty
Ctxt.implRegex = RegexRepr ArgTypeRepr Empty
BCmd.rProve
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) Empty
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState Match (Arg cExt) Empty
Rgx.MEmpty -> do
          Response cExt
resp <- SimContext p sym ext
-> (forall bak. IsSymBackend sym bak => bak -> IO (Response cExt))
-> IO (Response cExt)
forall personality sym ext a.
SimContext personality sym ext
-> (forall bak. IsSymBackend sym bak => bak -> a) -> a
C.withBackend (ExecState p sym ext (RegEntry sym t) -> SimContext p sym ext
forall p sym ext r. ExecState p sym ext r -> SimContext p sym ext
C.execStateContext ExecState p sym ext (RegEntry sym t)
execState) bak -> IO (Response cExt)
forall bak. IsSymBackend sym bak => bak -> IO (Response cExt)
forall sym t (st :: * -> *) fs bak cExt.
(sym ~ ExprBuilder t st fs, IsSymBackend sym bak) =>
bak -> IO (Response cExt)
Cmds.prove
          EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = resp }
      }

    BaseCommand
BCmd.Quit ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr Empty
Ctxt.implRegex = RegexRepr ArgTypeRepr Empty
BCmd.rQuit
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) Empty
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
_execState Match (Arg cExt) Empty
Rgx.MEmpty ->
          EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalCtx = ctx { Ctxt.dbgState = Ctxt.Quit } }
      }

    BaseCommand
BCmd.Register ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr (Star Int)
Ctxt.implRegex = RegexRepr ArgTypeRepr (Star Int)
BCmd.rRegister
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) (Star Int)
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState (Rgx.MStar [Match (Arg cExt) r1]
ints) -> do
          let ints' :: [Int]
ints' = (Match (Arg cExt) r1 -> Int) -> [Match (Arg cExt) r1] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (\(Rgx.MLit (Arg.AInt Int
i)) -> Int
i) [Match (Arg cExt) r1]
ints
          Response cExt
resp <- Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> [Int]
-> IO (Response cExt)
forall p sym ext r (t :: CrucibleType) cExt.
IsExpr (SymExpr sym) =>
Context cExt p sym ext t
-> ExecState p sym ext r -> [Int] -> IO (Response cExt)
Cmds.reg Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState [Int]
ints'
          EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = resp }
      }

    BaseCommand
BCmd.Run ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr Empty
Ctxt.implRegex = RegexRepr ArgTypeRepr Empty
BCmd.rRun
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) Empty
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState Match (Arg cExt) Empty
Rgx.MEmpty ->
          Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> RunningState
-> IO (EvalResult cExt p sym ext t)
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> RunningState
-> IO (EvalResult cExt p sym ext t)
runCmd Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState RunningState
Ctxt.Run
      }

    BaseCommand
BCmd.Secret ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr SecretRegex
Ctxt.implRegex = RegexRepr ArgTypeRepr SecretRegex
BCmd.rSecret
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) SecretRegex
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState Match (Arg cExt) SecretRegex
m -> do
          Response cExt
resp <- Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) SecretRegex
-> IO (Response cExt)
forall cExt p sym ext (t :: CrucibleType) r.
Pretty cExt =>
Context cExt p sym ext t
-> ExecState p sym ext r
-> Match (Arg cExt) SecretRegex
-> IO (Response cExt)
Cmds.secret Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState Match (Arg cExt) SecretRegex
m
          EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = resp }
      }

    BaseCommand
BCmd.Step ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr (Empty :| Int)
Ctxt.implRegex = RegexRepr ArgTypeRepr (Empty :| Int)
BCmd.rStep
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) (Empty :| Int)
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState Match (Arg cExt) (Empty :| Int)
m -> do
          let n :: Int
n =
                case Match (Arg cExt) (Empty :| Int)
m of
                  Rgx.MLeft Match (Arg cExt) l
Rgx.MEmpty -> Int
1
                  Rgx.MRight (Rgx.MLit (Arg.AInt Int
i)) -> Int
i
          Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> RunningState
-> IO (EvalResult cExt p sym ext t)
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> RunningState
-> IO (EvalResult cExt p sym ext t)
runCmd Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState (Int -> RunningState
Ctxt.Step Int
n)
      }

    BaseCommand
BCmd.Source ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr Path
Ctxt.implRegex = RegexRepr ArgTypeRepr Path
BCmd.rSource
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) Path
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
_execState (Rgx.MLit (Arg.APath Text
path)) -> do
          Either
  IOException
  (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt))
r <- Context cExt p sym ext t
-> FilePath
-> IO
     (Either
        IOException
        (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)))
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t
-> FilePath
-> IO
     (Either
        IOException
        (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)))
Cmds.source Context cExt p sym ext t
ctx (Text -> FilePath
Text.unpack Text
path)
          case Either
  IOException
  (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt))
r of
            Left IOException
ioErr -> EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = Resp.IOError ioErr }
            Right Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
inputs -> EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalCtx = ctx { Ctxt.dbgInputs = inputs } }
      }

    BaseCommand
BCmd.Trace ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr (Empty :| Int)
Ctxt.implRegex = RegexRepr ArgTypeRepr (Empty :| Int)
BCmd.rTrace
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) (Empty :| Int)
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
_execState Match (Arg cExt) (Empty :| Int)
m -> do
          let n :: Int
n =
                case Match (Arg cExt) (Empty :| Int)
m of
                  Rgx.MLeft Match (Arg cExt) l
Rgx.MEmpty -> Int
2
                  Rgx.MRight (Rgx.MLit (Arg.AInt Int
i)) -> Int
i
          [TraceEntry ext]
ents <- [TraceEntry ext] -> [TraceEntry ext]
forall a. [a] -> [a]
reverse ([TraceEntry ext] -> [TraceEntry ext])
-> IO [TraceEntry ext] -> IO [TraceEntry ext]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Trace ext -> Int -> IO [TraceEntry ext]
forall ext. Trace ext -> Int -> IO [TraceEntry ext]
Trace.latest (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) Int
n
          EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = Resp.Trace (map PP.pretty ents) }
      }

    BaseCommand
BCmd.Usage ->
      Ctxt.CommandImpl
      { implRegex :: RegexRepr ArgTypeRepr Command
Ctxt.implRegex = RegexRepr ArgTypeRepr Command
BCmd.rUsage
      , implBody :: Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) Command
-> IO (EvalResult cExt p sym ext t)
Ctxt.implBody = \Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
_execState (Rgx.MLit (Arg.ACommand Command cExt
cmd)) ->
          EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = Resp.Usage (Cmds.usage (Ctxt.dbgCommandExt ctx) cmd) }
      }

cmdImpl ::
  (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 ->
  Cmd.Command cExt ->
  Ctxt.CommandImpl cExt p sym ext t
cmdImpl :: 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
-> Command cExt -> CommandImpl cExt p sym ext t
cmdImpl Context cExt p sym ext t
ctx Command cExt
cmd =
  case Command cExt
cmd of
    Cmd.Base BaseCommand
bCmd -> BaseCommand -> CommandImpl 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)) =>
BaseCommand -> CommandImpl cExt p sym ext t
baseImpl BaseCommand
bCmd
    Cmd.Ext cExt
xCmd -> ExtImpl cExt p sym ext t -> cExt -> CommandImpl cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
ExtImpl cExt p sym ext t -> cExt -> CommandImpl cExt p sym ext t
Ctxt.getExtImpl (Context cExt p sym ext t -> ExtImpl cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> ExtImpl cExt p sym ext t
Ctxt.dbgExtImpl Context cExt p sym ext t
ctx) cExt
xCmd

eval ::
  (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) ->
  Statement cExt ->
  IO (Ctxt.EvalResult cExt p sym ext t)
eval :: 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 Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState Statement cExt
stmt =
  let args :: [Text]
args = Statement cExt -> [Text]
forall cExt. Statement cExt -> [Text]
Stmt.stmtArgs Statement cExt
stmt in
  let argError :: MatchError Text ArgParseError -> EvalResult cExt p sym ext t
argError MatchError Text ArgParseError
err = (Context cExt p sym ext t -> EvalResult cExt p sym ext t
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> EvalResult cExt p sym ext t
def Context cExt p sym ext t
ctx) { Ctxt.evalResp = Resp.UserError (Resp.ArgError (Stmt.stmtCmd stmt) err) } in
  case Context cExt p sym ext t
-> Command cExt -> CommandImpl 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
-> Command cExt -> CommandImpl cExt p sym ext t
cmdImpl Context cExt p sym ext t
ctx (Statement cExt -> Command cExt
forall cExt. Statement cExt -> Command cExt
Stmt.stmtCmd Statement cExt
stmt) of
    Ctxt.CommandImpl { implRegex :: ()
Ctxt.implRegex = RegexRepr ArgTypeRepr r
r, implBody :: ()
Ctxt.implBody = Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) r
-> IO (EvalResult cExt p sym ext t)
f } ->
      case RegexRepr (ArgParser cExt) r
-> [Text]
-> Either (MatchError Text ArgParseError) (Match (Arg cExt) r)
forall (r :: Regex ArgType) cExt.
RegexRepr (ArgParser cExt) r
-> [Text]
-> Either (MatchError Text ArgParseError) (Match (Arg cExt) r)
Arg.match (CommandExt cExt
-> RegexRepr ArgTypeRepr r -> RegexRepr (ArgParser cExt) r
forall cExt (r :: Regex ArgType).
CommandExt cExt
-> RegexRepr ArgTypeRepr r -> RegexRepr (ArgParser cExt) r
Arg.convert (Context cExt p sym ext t -> CommandExt cExt
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> CommandExt cExt
Ctxt.dbgCommandExt Context cExt p sym ext t
ctx) RegexRepr ArgTypeRepr r
r) [Text]
args of
        Left MatchError Text ArgParseError
e -> EvalResult cExt p sym ext t -> IO (EvalResult cExt p sym ext t)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (MatchError Text ArgParseError -> EvalResult cExt p sym ext t
argError MatchError Text ArgParseError
e)
        Right Match (Arg cExt) r
m -> Context cExt p sym ext t
-> ExecState p sym ext (RegEntry sym t)
-> Match (Arg cExt) r
-> IO (EvalResult cExt p sym ext t)
f Context cExt p sym ext t
ctx ExecState p sym ext (RegEntry sym t)
execState Match (Arg cExt) r
m