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

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

module Lang.Crucible.Debug.Commands
  ( execStateSimState
  , backtrace
  , block
  , call
  , cfg
  , frame
  , help
  , load
  , prove
  , reg
  , secret
  , source
  , usage
  ) where

import Control.Exception qualified as X
import Control.Lens qualified as Lens
import Control.Monad.Except (runExceptT)
import Control.Monad.IO.Class (liftIO)
import Data.List qualified as List
import Data.Maybe qualified as Maybe
import Data.Parameterized.Classes (ixF')
import Data.Parameterized.Context qualified as Ctx
import Data.Parameterized.Nonce qualified as Nonce
import Data.Parameterized.Some (Some(Some), viewSome)
import Data.Parameterized.TraversableFC (toListFC)
import Data.Sequence qualified as Seq
import Data.Text.IO qualified as IO
import Data.Text qualified as Text
import Lang.Crucible.Analysis.Postdom qualified as C
import Lang.Crucible.Backend.Prove qualified as Prove
import Lang.Crucible.Backend qualified as C
import Lang.Crucible.CFG.Core qualified as C
import Lang.Crucible.CFG.Extension qualified as C
import Lang.Crucible.CFG.Reg qualified as C.Reg
import Lang.Crucible.CFG.SSAConversion qualified as C
import Lang.Crucible.Debug.Arg qualified as Arg
import Lang.Crucible.Debug.Command.Base qualified as BCmd
import Lang.Crucible.Debug.Command qualified as Cmd
import Lang.Crucible.Debug.Complete (CompletionT)
import Lang.Crucible.Debug.Complete qualified as Complete
import Lang.Crucible.Debug.Context (Context)
import Lang.Crucible.Debug.Context qualified as Ctxt
import Lang.Crucible.Debug.Inputs (Inputs)
import Lang.Crucible.Debug.Inputs qualified as Inps
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 qualified as Stmt
import Lang.Crucible.Debug.Statement (Statement)
import Lang.Crucible.Debug.Style qualified as Style
import Lang.Crucible.Debug.Style (StyleT)
import Lang.Crucible.FunctionHandle qualified as C
import Lang.Crucible.Pretty (ppRegVal)
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.Atoms qualified as C
import Lang.Crucible.Syntax.Concrete qualified as C
import Lang.Crucible.Syntax.SExpr qualified as C
import Lang.Crucible.Utils.Seconds qualified as Sec
import Lang.Crucible.Utils.Timeout qualified as CTO
import Prettyprinter qualified as PP
import System.Exit qualified as Exit
import Text.Megaparsec qualified as MP
import What4.Config qualified as W4
import What4.Expr.Builder qualified as W4
import What4.FunctionName qualified as W4
import What4.Interface qualified as W4
import What4.ProgramLoc qualified as W4
import What4.Solver qualified as W4

---------------------------------------------------------------------
-- Helpers, exported

execStateSimState ::
  C.ExecState p sym ext r ->
  Either Resp.NotApplicable (C.SomeSimState p sym ext r)
execStateSimState :: forall p sym ext r.
ExecState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
execStateSimState =
  \case
    C.ResultState ExecResult p sym ext r
_                  -> NotApplicable -> Either NotApplicable (SomeSimState p sym ext r)
forall a b. a -> Either a b
Left NotApplicable
Resp.DoneSimulating
    C.AbortState AbortExecReason
_ SimState p sym ext r f a
st                -> SomeSimState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
forall a b. b -> Either a b
Right (SimState p sym ext r f a -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
C.SomeSimState SimState p sym ext r f a
st)
    C.UnwindCallState ValueFromValue p sym ext r r
_ AbortedResult sym ext
_ SimState p sym ext r f a
st         -> SomeSimState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
forall a b. b -> Either a b
Right (SimState p sym ext r f a -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
C.SomeSimState SimState p sym ext r f a
st)
    C.CallState ReturnHandler ret p sym ext r f a
_ ResolvedCall p sym ext ret
_ SimState p sym ext r f a
st               -> SomeSimState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
forall a b. b -> Either a b
Right (SimState p sym ext r f a -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
C.SomeSimState SimState p sym ext r f a
st)
    C.TailCallState ValueFromValue p sym ext r ret
_ ResolvedCall p sym ext ret
_ SimState p sym ext r f a
st           -> SomeSimState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
forall a b. b -> Either a b
Right (SimState p sym ext r f a -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
C.SomeSimState SimState p sym ext r f a
st)
    C.ReturnState FunctionName
_ ValueFromValue p sym ext r ret
_ RegEntry sym ret
_ SimState p sym ext r f a
st           -> SomeSimState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
forall a b. b -> Either a b
Right (SimState p sym ext r f a -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
C.SomeSimState SimState p sym ext r f a
st)
    C.ControlTransferState ControlResumption p sym ext r f
_ SimState p sym ext r f ('Just a)
st      -> SomeSimState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
forall a b. b -> Either a b
Right (SimState p sym ext r f ('Just a) -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
C.SomeSimState SimState p sym ext r f ('Just a)
st)
    C.RunningState RunningStateInfo blocks args
_ SimState p sym ext r (CrucibleLang blocks r) ('Just args)
st              -> SomeSimState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
forall a b. b -> Either a b
Right (SimState p sym ext r (CrucibleLang blocks r) ('Just args)
-> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
C.SomeSimState SimState p sym ext r (CrucibleLang blocks r) ('Just args)
st)
    C.SymbolicBranchState Pred sym
_ PausedFrame p sym ext r f
_ PausedFrame p sym ext r f
_ CrucibleBranchTarget f postdom_args
_ SimState p sym ext r f ('Just args)
st -> SomeSimState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
forall a b. b -> Either a b
Right (SimState p sym ext r f ('Just args) -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
C.SomeSimState SimState p sym ext r f ('Just args)
st)
    C.OverrideState Override p sym ext args ret
_ SimState p sym ext r (OverrideLang ret) ('Just args)
st             -> SomeSimState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
forall a b. b -> Either a b
Right (SimState p sym ext r (OverrideLang ret) ('Just args)
-> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
C.SomeSimState SimState p sym ext r (OverrideLang ret) ('Just args)
st)
    C.BranchMergeState CrucibleBranchTarget f args
_ SimState p sym ext r f args
st          -> SomeSimState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
forall a b. b -> Either a b
Right (SimState p sym ext r f args -> SomeSimState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> SomeSimState p sym ext rtp
C.SomeSimState SimState p sym ext r f args
st)
    C.InitialState 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)
_         -> NotApplicable -> Either NotApplicable (SomeSimState p sym ext r)
forall a b. a -> Either a b
Left NotApplicable
Resp.NotYetSimulating

---------------------------------------------------------------------
-- Helpers, not exported

insertCfg ::
  C.IsSyntaxExtension ext =>
  C.Reg.CFG ext blocks init ret ->
  C.FnHandleMap (C.FnState p sym ext) ->
  C.FnHandleMap (C.FnState p sym ext)
insertCfg :: forall ext blocks (init :: Ctx CrucibleType) (ret :: CrucibleType)
       p sym.
IsSyntaxExtension ext =>
CFG ext blocks init ret
-> FnHandleMap (FnState p sym ext)
-> FnHandleMap (FnState p sym ext)
insertCfg CFG ext blocks init ret
regCFG FnHandleMap (FnState p sym ext)
hdlMap =
  case CFG ext blocks init ret -> SomeCFG ext init ret
forall ext s (init :: Ctx CrucibleType) (ret :: CrucibleType).
IsSyntaxExtension ext =>
CFG ext s init ret -> SomeCFG ext init ret
C.toSSA CFG ext blocks init ret
regCFG of
    C.SomeCFG CFG ext blocks init ret
ssaCFG ->
      FnHandle init ret
-> FnState p sym ext init ret
-> FnHandleMap (FnState p sym ext)
-> FnHandleMap (FnState p sym ext)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (f :: Ctx CrucibleType -> CrucibleType -> *).
FnHandle args ret -> f args ret -> FnHandleMap f -> FnHandleMap f
C.insertHandleMap
        (CFG ext blocks init ret -> FnHandle init ret
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType).
CFG ext blocks init ret -> FnHandle init ret
C.cfgHandle CFG ext blocks init ret
ssaCFG)
        (CFG ext blocks init ret
-> CFGPostdom blocks -> FnState p sym ext init ret
forall p sym ext (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)).
CFG ext blocks args ret
-> CFGPostdom blocks -> FnState p sym ext args ret
C.UseCFG CFG ext blocks init ret
ssaCFG (CFG ext blocks init ret -> CFGPostdom blocks
forall ext (b :: Ctx (Ctx CrucibleType)) (i :: Ctx CrucibleType)
       (r :: CrucibleType).
CFG ext b i r -> CFGPostdom b
C.postdomInfo CFG ext blocks init ret
ssaCFG))
        FnHandleMap (FnState p sym ext)
hdlMap

data SomeFn f = forall args ret. SomeFn (f args ret)

lookupHandleMapByName ::
  W4.FunctionName ->
  C.FnHandleMap f ->
  Maybe (SomeFn f)
lookupHandleMapByName :: forall (f :: Ctx CrucibleType -> CrucibleType -> *).
FunctionName -> FnHandleMap f -> Maybe (SomeFn f)
lookupHandleMapByName FunctionName
fNm FnHandleMap f
hdls = do
  let sHdls :: [SomeHandle]
sHdls = FnHandleMap f -> [SomeHandle]
forall (f :: Ctx CrucibleType -> CrucibleType -> *).
FnHandleMap f -> [SomeHandle]
C.handleMapToHandles FnHandleMap f
hdls
  C.SomeHandle FnHandle args ret
h <- (SomeHandle -> Bool) -> [SomeHandle] -> Maybe SomeHandle
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find (\(C.SomeHandle FnHandle args ret
hdl) -> FnHandle args ret -> FunctionName
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
C.handleName FnHandle args ret
hdl FunctionName -> FunctionName -> Bool
forall a. Eq a => a -> a -> Bool
== FunctionName
fNm) [SomeHandle]
sHdls
  f args ret -> SomeFn f
forall {k} {k} (f :: k -> k -> *) (args :: k) (ret :: k).
f args ret -> SomeFn f
SomeFn (f args ret -> SomeFn f) -> Maybe (f args ret) -> Maybe (SomeFn f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> FnHandle args ret -> FnHandleMap f -> Maybe (f args ret)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (f :: Ctx CrucibleType -> CrucibleType -> *).
FnHandle args ret -> FnHandleMap f -> Maybe (f args ret)
C.lookupHandleMap FnHandle args ret
h FnHandleMap f
hdls

-- TODO: Upstream to Crucible as a Lens
modifySimContext ::
  (C.SimContext p sym ext -> C.SimContext p sym ext) ->
  C.ExecState p sym ext r ->
  C.ExecState p sym ext r
modifySimContext :: forall p sym ext r.
(SimContext p sym ext -> SimContext p sym ext)
-> ExecState p sym ext r -> ExecState p sym ext r
modifySimContext SimContext p sym ext -> SimContext p sym ext
f =
  \case
    C.ResultState ExecResult p sym ext r
r ->
      case ExecResult p sym ext r
r of
        C.FinishedResult SimContext p sym ext
ctx PartialResult sym ext r
x -> ExecResult p sym ext r -> ExecState p sym ext r
forall p sym ext rtp.
ExecResult p sym ext rtp -> ExecState p sym ext rtp
C.ResultState (SimContext p sym ext
-> PartialResult sym ext r -> ExecResult p sym ext r
forall p sym ext r.
SimContext p sym ext
-> PartialResult sym ext r -> ExecResult p sym ext r
C.FinishedResult (SimContext p sym ext -> SimContext p sym ext
f SimContext p sym ext
ctx) PartialResult sym ext r
x)
        C.AbortedResult SimContext p sym ext
ctx AbortedResult sym ext
x -> ExecResult p sym ext r -> ExecState p sym ext r
forall p sym ext rtp.
ExecResult p sym ext rtp -> ExecState p sym ext rtp
C.ResultState (SimContext p sym ext
-> AbortedResult sym ext -> ExecResult p sym ext r
forall p sym ext r.
SimContext p sym ext
-> AbortedResult sym ext -> ExecResult p sym ext r
C.AbortedResult (SimContext p sym ext -> SimContext p sym ext
f SimContext p sym ext
ctx) AbortedResult sym ext
x)
        C.TimeoutResult ExecState p sym ext r
es -> (SimContext p sym ext -> SimContext p sym ext)
-> ExecState p sym ext r -> ExecState p sym ext r
forall p sym ext r.
(SimContext p sym ext -> SimContext p sym ext)
-> ExecState p sym ext r -> ExecState p sym ext r
modifySimContext SimContext p sym ext -> SimContext p sym ext
f ExecState p sym ext r
es
    C.AbortState AbortExecReason
x SimState p sym ext r f a
s -> AbortExecReason
-> SimState p sym ext r f a -> ExecState p sym ext r
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType)).
AbortExecReason
-> SimState p sym ext rtp f a -> ExecState p sym ext rtp
C.AbortState AbortExecReason
x (SimState p sym ext r f a
s SimState p sym ext r f a
-> (SimState p sym ext r f a -> SimState p sym ext r f a)
-> SimState p sym ext r f a
forall a b. a -> (a -> b) -> b
Lens.& (SimContext p sym ext -> Identity (SimContext p sym ext))
-> SimState p sym ext r f a -> Identity (SimState p sym ext r f a)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: * -> *).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
C.stateContext ((SimContext p sym ext -> Identity (SimContext p sym ext))
 -> SimState p sym ext r f a -> Identity (SimState p sym ext r f a))
-> (SimContext p sym ext -> SimContext p sym ext)
-> SimState p sym ext r f a
-> SimState p sym ext r f a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
Lens.%~ SimContext p sym ext -> SimContext p sym ext
f)
    C.UnwindCallState ValueFromValue p sym ext r r
x AbortedResult sym ext
y SimState p sym ext r f a
s -> ValueFromValue p sym ext r r
-> AbortedResult sym ext
-> SimState p sym ext r f a
-> ExecState p sym ext r
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType))
       (r :: CrucibleType).
ValueFromValue p sym ext rtp r
-> AbortedResult sym ext
-> SimState p sym ext rtp f a
-> ExecState p sym ext rtp
C.UnwindCallState ValueFromValue p sym ext r r
x AbortedResult sym ext
y (SimState p sym ext r f a
s SimState p sym ext r f a
-> (SimState p sym ext r f a -> SimState p sym ext r f a)
-> SimState p sym ext r f a
forall a b. a -> (a -> b) -> b
Lens.& (SimContext p sym ext -> Identity (SimContext p sym ext))
-> SimState p sym ext r f a -> Identity (SimState p sym ext r f a)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: * -> *).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
C.stateContext ((SimContext p sym ext -> Identity (SimContext p sym ext))
 -> SimState p sym ext r f a -> Identity (SimState p sym ext r f a))
-> (SimContext p sym ext -> SimContext p sym ext)
-> SimState p sym ext r f a
-> SimState p sym ext r f a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
Lens.%~ SimContext p sym ext -> SimContext p sym ext
f)
    C.CallState ReturnHandler ret p sym ext r f a
x ResolvedCall p sym ext ret
y SimState p sym ext r f a
s -> ReturnHandler ret p sym ext r f a
-> ResolvedCall p sym ext ret
-> SimState p sym ext r f a
-> ExecState p sym ext r
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType))
       (ret :: CrucibleType).
ReturnHandler ret p sym ext rtp f a
-> ResolvedCall p sym ext ret
-> SimState p sym ext rtp f a
-> ExecState p sym ext rtp
C.CallState ReturnHandler ret p sym ext r f a
x ResolvedCall p sym ext ret
y (SimState p sym ext r f a
s SimState p sym ext r f a
-> (SimState p sym ext r f a -> SimState p sym ext r f a)
-> SimState p sym ext r f a
forall a b. a -> (a -> b) -> b
Lens.& (SimContext p sym ext -> Identity (SimContext p sym ext))
-> SimState p sym ext r f a -> Identity (SimState p sym ext r f a)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: * -> *).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
C.stateContext ((SimContext p sym ext -> Identity (SimContext p sym ext))
 -> SimState p sym ext r f a -> Identity (SimState p sym ext r f a))
-> (SimContext p sym ext -> SimContext p sym ext)
-> SimState p sym ext r f a
-> SimState p sym ext r f a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
Lens.%~ SimContext p sym ext -> SimContext p sym ext
f)
    C.TailCallState ValueFromValue p sym ext r ret
x ResolvedCall p sym ext ret
y SimState p sym ext r f a
s -> ValueFromValue p sym ext r ret
-> ResolvedCall p sym ext ret
-> SimState p sym ext r f a
-> ExecState p sym ext r
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType))
       (ret :: CrucibleType).
ValueFromValue p sym ext rtp ret
-> ResolvedCall p sym ext ret
-> SimState p sym ext rtp f a
-> ExecState p sym ext rtp
C.TailCallState ValueFromValue p sym ext r ret
x ResolvedCall p sym ext ret
y (SimState p sym ext r f a
s SimState p sym ext r f a
-> (SimState p sym ext r f a -> SimState p sym ext r f a)
-> SimState p sym ext r f a
forall a b. a -> (a -> b) -> b
Lens.& (SimContext p sym ext -> Identity (SimContext p sym ext))
-> SimState p sym ext r f a -> Identity (SimState p sym ext r f a)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: * -> *).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
C.stateContext ((SimContext p sym ext -> Identity (SimContext p sym ext))
 -> SimState p sym ext r f a -> Identity (SimState p sym ext r f a))
-> (SimContext p sym ext -> SimContext p sym ext)
-> SimState p sym ext r f a
-> SimState p sym ext r f a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
Lens.%~ SimContext p sym ext -> SimContext p sym ext
f)
    C.ReturnState FunctionName
x ValueFromValue p sym ext r ret
y RegEntry sym ret
z SimState p sym ext r f a
s -> FunctionName
-> ValueFromValue p sym ext r ret
-> RegEntry sym ret
-> SimState p sym ext r f a
-> ExecState p sym ext r
forall p sym ext rtp f (a :: Maybe (Ctx CrucibleType))
       (ret :: CrucibleType).
FunctionName
-> ValueFromValue p sym ext rtp ret
-> RegEntry sym ret
-> SimState p sym ext rtp f a
-> ExecState p sym ext rtp
C.ReturnState FunctionName
x ValueFromValue p sym ext r ret
y RegEntry sym ret
z (SimState p sym ext r f a
s SimState p sym ext r f a
-> (SimState p sym ext r f a -> SimState p sym ext r f a)
-> SimState p sym ext r f a
forall a b. a -> (a -> b) -> b
Lens.& (SimContext p sym ext -> Identity (SimContext p sym ext))
-> SimState p sym ext r f a -> Identity (SimState p sym ext r f a)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: * -> *).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
C.stateContext ((SimContext p sym ext -> Identity (SimContext p sym ext))
 -> SimState p sym ext r f a -> Identity (SimState p sym ext r f a))
-> (SimContext p sym ext -> SimContext p sym ext)
-> SimState p sym ext r f a
-> SimState p sym ext r f a
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
Lens.%~ SimContext p sym ext -> SimContext p sym ext
f)
    C.ControlTransferState ControlResumption p sym ext r f
x SimState p sym ext r f ('Just a)
s -> ControlResumption p sym ext r f
-> SimState p sym ext r f ('Just a) -> ExecState p sym ext r
forall p sym ext rtp f (a :: Ctx CrucibleType).
ControlResumption p sym ext rtp f
-> SimState p sym ext rtp f ('Just a) -> ExecState p sym ext rtp
C.ControlTransferState ControlResumption p sym ext r f
x (SimState p sym ext r f ('Just a)
s SimState p sym ext r f ('Just a)
-> (SimState p sym ext r f ('Just a)
    -> SimState p sym ext r f ('Just a))
-> SimState p sym ext r f ('Just a)
forall a b. a -> (a -> b) -> b
Lens.& (SimContext p sym ext -> Identity (SimContext p sym ext))
-> SimState p sym ext r f ('Just a)
-> Identity (SimState p sym ext r f ('Just a))
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: * -> *).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
C.stateContext ((SimContext p sym ext -> Identity (SimContext p sym ext))
 -> SimState p sym ext r f ('Just a)
 -> Identity (SimState p sym ext r f ('Just a)))
-> (SimContext p sym ext -> SimContext p sym ext)
-> SimState p sym ext r f ('Just a)
-> SimState p sym ext r f ('Just a)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
Lens.%~ SimContext p sym ext -> SimContext p sym ext
f)
    C.RunningState RunningStateInfo blocks args
x SimState p sym ext r (CrucibleLang blocks r) ('Just args)
s -> RunningStateInfo blocks args
-> SimState p sym ext r (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext r
forall p sym ext rtp (blocks :: Ctx (Ctx CrucibleType))
       (r :: CrucibleType) (args :: Ctx CrucibleType).
RunningStateInfo blocks args
-> SimState p sym ext rtp (CrucibleLang blocks r) ('Just args)
-> ExecState p sym ext rtp
C.RunningState RunningStateInfo blocks args
x (SimState p sym ext r (CrucibleLang blocks r) ('Just args)
s SimState p sym ext r (CrucibleLang blocks r) ('Just args)
-> (SimState p sym ext r (CrucibleLang blocks r) ('Just args)
    -> SimState p sym ext r (CrucibleLang blocks r) ('Just args))
-> SimState p sym ext r (CrucibleLang blocks r) ('Just args)
forall a b. a -> (a -> b) -> b
Lens.& (SimContext p sym ext -> Identity (SimContext p sym ext))
-> SimState p sym ext r (CrucibleLang blocks r) ('Just args)
-> Identity
     (SimState p sym ext r (CrucibleLang blocks r) ('Just args))
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: * -> *).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
C.stateContext ((SimContext p sym ext -> Identity (SimContext p sym ext))
 -> SimState p sym ext r (CrucibleLang blocks r) ('Just args)
 -> Identity
      (SimState p sym ext r (CrucibleLang blocks r) ('Just args)))
-> (SimContext p sym ext -> SimContext p sym ext)
-> SimState p sym ext r (CrucibleLang blocks r) ('Just args)
-> SimState p sym ext r (CrucibleLang blocks r) ('Just args)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
Lens.%~ SimContext p sym ext -> SimContext p sym ext
f)
    C.SymbolicBranchState Pred sym
x PausedFrame p sym ext r f
y PausedFrame p sym ext r f
z CrucibleBranchTarget f postdom_args
w SimState p sym ext r f ('Just args)
s -> Pred sym
-> PausedFrame p sym ext r f
-> PausedFrame p sym ext r f
-> CrucibleBranchTarget f postdom_args
-> SimState p sym ext r f ('Just args)
-> ExecState p sym ext r
forall p sym ext rtp f (args :: Ctx CrucibleType)
       (postdom_args :: Maybe (Ctx CrucibleType)).
Pred sym
-> PausedFrame p sym ext rtp f
-> PausedFrame p sym ext rtp f
-> CrucibleBranchTarget f postdom_args
-> SimState p sym ext rtp f ('Just args)
-> ExecState p sym ext rtp
C.SymbolicBranchState Pred sym
x PausedFrame p sym ext r f
y PausedFrame p sym ext r f
z CrucibleBranchTarget f postdom_args
w (SimState p sym ext r f ('Just args)
s SimState p sym ext r f ('Just args)
-> (SimState p sym ext r f ('Just args)
    -> SimState p sym ext r f ('Just args))
-> SimState p sym ext r f ('Just args)
forall a b. a -> (a -> b) -> b
Lens.& (SimContext p sym ext -> Identity (SimContext p sym ext))
-> SimState p sym ext r f ('Just args)
-> Identity (SimState p sym ext r f ('Just args))
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: * -> *).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
C.stateContext ((SimContext p sym ext -> Identity (SimContext p sym ext))
 -> SimState p sym ext r f ('Just args)
 -> Identity (SimState p sym ext r f ('Just args)))
-> (SimContext p sym ext -> SimContext p sym ext)
-> SimState p sym ext r f ('Just args)
-> SimState p sym ext r f ('Just args)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
Lens.%~ SimContext p sym ext -> SimContext p sym ext
f)
    C.OverrideState Override p sym ext args ret
x SimState p sym ext r (OverrideLang ret) ('Just args)
s -> Override p sym ext args ret
-> SimState p sym ext r (OverrideLang ret) ('Just args)
-> ExecState p sym ext r
forall p sym ext rtp (args :: Ctx CrucibleType)
       (ret :: CrucibleType).
Override p sym ext args ret
-> SimState p sym ext rtp (OverrideLang ret) ('Just args)
-> ExecState p sym ext rtp
C.OverrideState Override p sym ext args ret
x (SimState p sym ext r (OverrideLang ret) ('Just args)
s SimState p sym ext r (OverrideLang ret) ('Just args)
-> (SimState p sym ext r (OverrideLang ret) ('Just args)
    -> SimState p sym ext r (OverrideLang ret) ('Just args))
-> SimState p sym ext r (OverrideLang ret) ('Just args)
forall a b. a -> (a -> b) -> b
Lens.& (SimContext p sym ext -> Identity (SimContext p sym ext))
-> SimState p sym ext r (OverrideLang ret) ('Just args)
-> Identity (SimState p sym ext r (OverrideLang ret) ('Just args))
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: * -> *).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
C.stateContext ((SimContext p sym ext -> Identity (SimContext p sym ext))
 -> SimState p sym ext r (OverrideLang ret) ('Just args)
 -> Identity (SimState p sym ext r (OverrideLang ret) ('Just args)))
-> (SimContext p sym ext -> SimContext p sym ext)
-> SimState p sym ext r (OverrideLang ret) ('Just args)
-> SimState p sym ext r (OverrideLang ret) ('Just args)
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
Lens.%~ SimContext p sym ext -> SimContext p sym ext
f)
    C.BranchMergeState CrucibleBranchTarget f args
x SimState p sym ext r f args
s -> CrucibleBranchTarget f args
-> SimState p sym ext r f args -> ExecState p sym ext r
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
CrucibleBranchTarget f args
-> SimState p sym ext rtp f args -> ExecState p sym ext rtp
C.BranchMergeState CrucibleBranchTarget f args
x (SimState p sym ext r f args
s SimState p sym ext r f args
-> (SimState p sym ext r f args -> SimState p sym ext r f args)
-> SimState p sym ext r f args
forall a b. a -> (a -> b) -> b
Lens.& (SimContext p sym ext -> Identity (SimContext p sym ext))
-> SimState p sym ext r f args
-> Identity (SimState p sym ext r f args)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: * -> *).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
C.stateContext ((SimContext p sym ext -> Identity (SimContext p sym ext))
 -> SimState p sym ext r f args
 -> Identity (SimState p sym ext r f args))
-> (SimContext p sym ext -> SimContext p sym ext)
-> SimState p sym ext r f args
-> SimState p sym ext r f args
forall s t a b. ASetter s t a b -> (a -> b) -> s -> t
Lens.%~ SimContext p sym ext -> SimContext p sym ext
f)
    C.InitialState SimContext p sym ext
ctx SymGlobalState sym
x AbortHandler p sym ext (RegEntry sym ret)
y TypeRepr ret
z ExecCont
  p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
w -> 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 r
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 p sym ext -> SimContext p sym ext
f SimContext p sym ext
ctx) SymGlobalState sym
x AbortHandler p sym ext (RegEntry sym ret)
y TypeRepr ret
z ExecCont
  p sym ext (RegEntry sym ret) (OverrideLang ret) ('Just EmptyCtx)
w

---------------------------------------------------------------------
-- Commands, exported

backtrace ::
  C.ExecState p sym ext r ->
  IO (Response cExt)
backtrace :: forall p sym ext r cExt.
ExecState p sym ext r -> IO (Response cExt)
backtrace ExecState p sym ext r
execState =
  case ExecState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
forall p sym ext r.
ExecState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
execStateSimState ExecState p sym ext r
execState of
    Left NotApplicable
notApplicable -> Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (NotApplicable -> UserError cExt
forall cExt. NotApplicable -> UserError cExt
Resp.NotApplicable NotApplicable
notApplicable))
    Right (C.SomeSimState SimState p sym ext r f args
simState) -> do
      let frames :: [SomeFrame (SimFrame sym ext)]
frames = ActiveTree p sym ext r f args -> [SomeFrame (SimFrame sym ext)]
forall ctx sym ext root a (args :: Maybe (Ctx CrucibleType)).
ActiveTree ctx sym ext root a args
-> [SomeFrame (SimFrame sym ext)]
C.activeFrames (SimState p sym ext r f args -> ActiveTree p sym ext r f args
forall p sym ext rtp f (args :: Maybe (Ctx CrucibleType)).
SimState p sym ext rtp f args -> ActiveTree p sym ext rtp f args
C._stateTree SimState p sym ext r f args
simState)
      Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc Void -> Response cExt
forall cExt. Doc Void -> Response cExt
Resp.Backtrace ([SomeFrame (SimFrame sym ext)] -> Doc Void
forall sym ext ann. [SomeFrame (SimFrame sym ext)] -> Doc ann
C.ppExceptionContext [SomeFrame (SimFrame sym ext)]
frames))

block ::
  C.IsSyntaxExtension ext =>
  W4.IsExpr (W4.SymExpr sym) =>
  Context cExt p sym ext t ->
  C.ExecState p sym ext r ->
  IO (Response cExt)
block :: 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)
block Context cExt p sym ext t
_ctx ExecState p sym ext r
execState =
  case ExecState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
forall p sym ext r.
ExecState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
execStateSimState ExecState p sym ext r
execState of
    Left NotApplicable
notApplicable -> Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (NotApplicable -> UserError cExt
forall cExt. NotApplicable -> UserError cExt
Resp.NotApplicable NotApplicable
notApplicable))
    Right (C.SomeSimState SimState p sym ext r f args
simState) ->
      let fr :: SimFrame sym ext f args
fr = SimState p sym ext r f args
simState SimState p sym ext r f args
-> Getting
     (SimFrame sym ext f args)
     (SimState p sym ext r f args)
     (SimFrame sym ext f args)
-> SimFrame sym ext f args
forall s a. s -> Getting a s a -> a
Lens.^. (ActiveTree p sym ext r f args
 -> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args))
-> SimState p sym ext r f args
-> Const (SimFrame sym ext f args) (SimState p sym ext r f args)
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: * -> *).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
C.stateTree ((ActiveTree p sym ext r f args
  -> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args))
 -> SimState p sym ext r f args
 -> Const (SimFrame sym ext f args) (SimState p sym ext r f args))
-> ((SimFrame sym ext f args
     -> Const (SimFrame sym ext f args) (SimFrame sym ext f args))
    -> ActiveTree p sym ext r f args
    -> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args))
-> Getting
     (SimFrame sym ext f args)
     (SimState p sym ext r f args)
     (SimFrame sym ext f args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext f args
 -> Const (SimFrame sym ext f args) (TopFrame sym ext f args))
-> ActiveTree p sym ext r f args
-> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args)
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: * -> *).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
C.actFrame ((TopFrame sym ext f args
  -> Const (SimFrame sym ext f args) (TopFrame sym ext f args))
 -> ActiveTree p sym ext r f args
 -> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args))
-> ((SimFrame sym ext f args
     -> Const (SimFrame sym ext f args) (SimFrame sym ext f args))
    -> TopFrame sym ext f args
    -> Const (SimFrame sym ext f args) (TopFrame sym ext f args))
-> (SimFrame sym ext f args
    -> Const (SimFrame sym ext f args) (SimFrame sym ext f args))
-> ActiveTree p sym ext r f args
-> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimFrame sym ext f args
 -> Const (SimFrame sym ext f args) (SimFrame sym ext f args))
-> TopFrame sym ext f args
-> Const (SimFrame sym ext f args) (TopFrame sym ext f args)
forall sym u v (f :: * -> *).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
C.gpValue in
      case SimFrame sym ext f args
fr of
        C.MF CallFrame sym ext blocks ret args1
callFrame ->
          let regs :: Assignment (RegEntry sym) args1
regs = RegMap sym args1 -> Assignment (RegEntry sym) args1
forall sym (ctx :: Ctx CrucibleType).
RegMap sym ctx -> Assignment (RegEntry sym) ctx
C.regMap (CallFrame sym ext blocks ret args1
callFrame CallFrame sym ext blocks ret args1
-> Getting
     (RegMap sym args1)
     (CallFrame sym ext blocks ret args1)
     (RegMap sym args1)
-> RegMap sym args1
forall s a. s -> Getting a s a -> a
Lens.^. Getting
  (RegMap sym args1)
  (CallFrame sym ext blocks ret args1)
  (RegMap sym args1)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType) (f :: * -> *).
Functor f =>
(RegMap sym args -> f (RegMap sym args))
-> CallFrame sym ext blocks ret args
-> f (CallFrame sym ext blocks ret args)
C.frameRegs) in
          Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc Void -> Response cExt
forall cExt. Doc Void -> Response cExt
Resp.Block (Bool -> Size args1 -> StmtSeq ext blocks ret args1 -> Doc Void
forall ext (ctx :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) ann.
PrettyExt ext =>
Bool -> Size ctx -> StmtSeq ext blocks ret ctx -> Doc ann
ppStmtSeq Bool
False (Assignment (RegEntry sym) args1 -> Size args1
forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment (RegEntry sym) args1
regs) (CallFrame sym ext blocks ret args1 -> StmtSeq ext blocks ret args1
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args -> StmtSeq ext blocks ret args
C._frameStmts CallFrame sym ext blocks ret args1
callFrame)))
        C.OF {} -> Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (NotApplicable -> UserError cExt
forall cExt. NotApplicable -> UserError cExt
Resp.NotApplicable NotApplicable
Resp.NoCfg))
        C.RF {} -> Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (NotApplicable -> UserError cExt
forall cExt. NotApplicable -> UserError cExt
Resp.NotApplicable NotApplicable
Resp.NoCfg))
  where
    -- TODO: The below is taken from Crucible. Export?

    prefixLineNum :: Bool -> W4.ProgramLoc -> PP.Doc ann -> PP.Doc ann
    prefixLineNum :: forall ann. Bool -> ProgramLoc -> Doc ann -> Doc ann
prefixLineNum Bool
True ProgramLoc
pl Doc ann
d = [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat [Doc ann
"%" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> Position -> Doc ann
forall ann. Position -> Doc ann
W4.ppNoFileName (ProgramLoc -> Position
W4.plSourceLoc ProgramLoc
pl), Doc ann
d]
    prefixLineNum Bool
False ProgramLoc
_ Doc ann
d = Doc ann
d

    ppStmtSeq :: C.PrettyExt ext => Bool -> Ctx.Size ctx -> C.StmtSeq ext blocks ret ctx -> PP.Doc ann
    ppStmtSeq :: forall ext (ctx :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) ann.
PrettyExt ext =>
Bool -> Size ctx -> StmtSeq ext blocks ret ctx -> Doc ann
ppStmtSeq Bool
ppLineNum Size ctx
h (C.ConsStmt ProgramLoc
pl Stmt ext ctx ctx'
s StmtSeq ext blocks ret ctx'
r) =
      [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat
      [ Bool -> ProgramLoc -> Doc ann -> Doc ann
forall ann. Bool -> ProgramLoc -> Doc ann -> Doc ann
prefixLineNum Bool
ppLineNum ProgramLoc
pl (Size ctx -> Stmt ext ctx ctx' -> Doc ann
forall ext (ctx :: Ctx CrucibleType) (ctx' :: Ctx CrucibleType)
       ann.
PrettyExt ext =>
Size ctx -> Stmt ext ctx ctx' -> Doc ann
C.ppStmt Size ctx
h Stmt ext ctx ctx'
s)
      , Bool -> Size ctx' -> StmtSeq ext blocks ret ctx' -> Doc ann
forall ext (ctx :: Ctx CrucibleType)
       (blocks :: Ctx (Ctx CrucibleType)) (ret :: CrucibleType) ann.
PrettyExt ext =>
Bool -> Size ctx -> StmtSeq ext blocks ret ctx -> Doc ann
ppStmtSeq Bool
ppLineNum (Size ctx -> Stmt ext ctx ctx' -> Size ctx'
forall (ctx :: Ctx CrucibleType) ext (ctx' :: Ctx CrucibleType).
Size ctx -> Stmt ext ctx ctx' -> Size ctx'
C.nextStmtHeight Size ctx
h Stmt ext ctx ctx'
s) StmtSeq ext blocks ret ctx'
r
      ]
    ppStmtSeq Bool
ppLineNum Size ctx
_ (C.TermStmt ProgramLoc
pl TermStmt blocks ret ctx
s) =
      Bool -> ProgramLoc -> Doc ann -> Doc ann
forall ann. Bool -> ProgramLoc -> Doc ann -> Doc ann
prefixLineNum Bool
ppLineNum ProgramLoc
pl (TermStmt blocks ret ctx -> Doc ann
forall ann. TermStmt blocks ret ctx -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty TermStmt blocks ret ctx
s)

call ::
  C.IsSymInterface sym =>
  C.IsSyntaxExtension ext =>
  C.ExecState p sym ext (C.RegEntry sym t) ->
  C.TypeRepr t ->
  W4.FunctionName ->
  IO (C.ExecutionFeatureResult p sym ext (C.RegEntry sym t), Response cExt)
call :: 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)
call ExecState p sym ext (RegEntry sym t)
execState TypeRepr t
rTy FunctionName
fNm = do
  let fTy :: TypeRepr ('FunctionHandleType EmptyCtx 'UnitType)
fTy = CtxRepr EmptyCtx
-> TypeRepr 'UnitType
-> TypeRepr ('FunctionHandleType EmptyCtx 'UnitType)
forall (ctx :: Ctx CrucibleType) (ret :: CrucibleType).
CtxRepr ctx
-> TypeRepr ret -> TypeRepr ('FunctionHandleType ctx ret)
C.FunctionHandleRepr CtxRepr EmptyCtx
forall {k} (f :: k -> *). Assignment f EmptyCtx
Ctx.empty TypeRepr 'UnitType
C.UnitRepr
  let binds :: FunctionBindings p sym ext
binds = ExecState p sym ext (RegEntry sym t)
execState ExecState p sym ext (RegEntry sym t)
-> Getting
     (FunctionBindings p sym ext)
     (ExecState p sym ext (RegEntry sym t))
     (FunctionBindings p sym ext)
-> FunctionBindings p sym ext
forall s a. s -> Getting a s a -> a
Lens.^. (ExecState p sym ext (RegEntry sym t) -> SimContext p sym ext)
-> (SimContext p sym ext
    -> Const (FunctionBindings p sym ext) (SimContext p sym ext))
-> ExecState p sym ext (RegEntry sym t)
-> Const
     (FunctionBindings p sym ext) (ExecState p sym ext (RegEntry sym t))
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
Lens.to 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 ((SimContext p sym ext
  -> Const (FunctionBindings p sym ext) (SimContext p sym ext))
 -> ExecState p sym ext (RegEntry sym t)
 -> Const
      (FunctionBindings p sym ext)
      (ExecState p sym ext (RegEntry sym t)))
-> ((FunctionBindings p sym ext
     -> Const (FunctionBindings p sym ext) (FunctionBindings p sym ext))
    -> SimContext p sym ext
    -> Const (FunctionBindings p sym ext) (SimContext p sym ext))
-> Getting
     (FunctionBindings p sym ext)
     (ExecState p sym ext (RegEntry sym t))
     (FunctionBindings p sym ext)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FunctionBindings p sym ext
 -> Const (FunctionBindings p sym ext) (FunctionBindings p sym ext))
-> SimContext p sym ext
-> Const (FunctionBindings p sym ext) (SimContext p sym ext)
forall p sym ext (f :: * -> *).
Functor f =>
(FunctionBindings p sym ext -> f (FunctionBindings p sym ext))
-> SimContext p sym ext -> f (SimContext p sym ext)
C.functionBindings
  case FunctionName
-> TypeRepr ('FunctionHandleType EmptyCtx 'UnitType)
-> FnHandleMap (FnState p sym ext)
-> Maybe
     (FnHandle EmptyCtx 'UnitType, FnState p sym ext EmptyCtx 'UnitType)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType)
       (f :: Ctx CrucibleType -> CrucibleType -> *).
FunctionName
-> TypeRepr (FunctionHandleType args ret)
-> FnHandleMap f
-> Maybe (FnHandle args ret, f args ret)
C.searchHandleMap FunctionName
fNm TypeRepr ('FunctionHandleType EmptyCtx 'UnitType)
fTy (FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
forall p sym ext.
FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
C.fnBindings FunctionBindings p sym ext
binds) of
    Maybe
  (FnHandle EmptyCtx 'UnitType, FnState p sym ext EmptyCtx 'UnitType)
Nothing -> do
      let hdls :: [SomeHandle]
hdls = FnHandleMap (FnState p sym ext) -> [SomeHandle]
forall (f :: Ctx CrucibleType -> CrucibleType -> *).
FnHandleMap f -> [SomeHandle]
C.handleMapToHandles (FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
forall p sym ext.
FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
C.fnBindings FunctionBindings p sym ext
binds)
      let names :: [FunctionName]
names = (SomeHandle -> FunctionName) -> [SomeHandle] -> [FunctionName]
forall a b. (a -> b) -> [a] -> [b]
map (\(C.SomeHandle FnHandle args ret
hdl) -> FnHandle args ret -> FunctionName
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
C.handleName FnHandle args ret
hdl) [SomeHandle]
hdls
      (ExecutionFeatureResult p sym ext (RegEntry sym t), Response cExt)
-> IO
     (ExecutionFeatureResult p sym ext (RegEntry sym t), Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExecutionFeatureResult p sym ext (RegEntry sym t)
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNoChange, UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (FunctionName -> [FunctionName] -> UserError cExt
forall cExt. FunctionName -> [FunctionName] -> UserError cExt
Resp.FnNotFound FunctionName
fNm [FunctionName]
names))
    Just (FnHandle EmptyCtx 'UnitType
hdl, FnState p sym ext EmptyCtx 'UnitType
bind) -> do
      case ExecState p sym ext (RegEntry sym t)
-> Either NotApplicable (SomeSimState p sym ext (RegEntry sym t))
forall p sym ext r.
ExecState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
execStateSimState ExecState p sym ext (RegEntry sym t)
execState of
        Left NotApplicable
notApplicable -> (ExecutionFeatureResult p sym ext (RegEntry sym t), Response cExt)
-> IO
     (ExecutionFeatureResult p sym ext (RegEntry sym t), Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExecutionFeatureResult p sym ext (RegEntry sym t)
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNoChange, UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (NotApplicable -> UserError cExt
forall cExt. NotApplicable -> UserError cExt
Resp.NotApplicable NotApplicable
notApplicable))
        Right (C.SomeSimState SimState p sym ext (RegEntry sym t) f args
simState) -> do
          let initCtx :: SimContext p sym ext
initCtx = SimState p sym ext (RegEntry sym t) f args
simState SimState p sym ext (RegEntry sym t) f args
-> Getting
     (SimContext p sym ext)
     (SimState p sym ext (RegEntry sym t) f args)
     (SimContext p sym ext)
-> SimContext p sym ext
forall s a. s -> Getting a s a -> a
Lens.^. Getting
  (SimContext p sym ext)
  (SimState p sym ext (RegEntry sym t) f args)
  (SimContext p sym ext)
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: * -> *).
Functor f2 =>
(SimContext p sym ext -> f2 (SimContext p sym ext))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
C.stateContext
          let globs :: SymGlobalState sym
globs = SimState p sym ext (RegEntry sym t) f args
simState SimState p sym ext (RegEntry sym t) f args
-> Getting
     (SymGlobalState sym)
     (SimState p sym ext (RegEntry sym t) f args)
     (SymGlobalState sym)
-> SymGlobalState sym
forall s a. s -> Getting a s a -> a
Lens.^. Getting
  (SymGlobalState sym)
  (SimState p sym ext (RegEntry sym t) f args)
  (SymGlobalState sym)
forall p sym ext q f1 (args :: Maybe (Ctx CrucibleType))
       (f2 :: * -> *).
Functor f2 =>
(SymGlobalState sym -> f2 (SymGlobalState sym))
-> SimState p sym ext q f1 args
-> f2 (SimState p sym ext q f1 args)
C.stateGlobals
          let abortHdl :: AbortHandler p sym ext (RegEntry sym t)
abortHdl = SimState p sym ext (RegEntry sym t) f args
simState SimState p sym ext (RegEntry sym t) f args
-> Getting
     (AbortHandler p sym ext (RegEntry sym t))
     (SimState p sym ext (RegEntry sym t) f args)
     (AbortHandler p sym ext (RegEntry sym t))
-> AbortHandler p sym ext (RegEntry sym t)
forall s a. s -> Getting a s a -> a
Lens.^. Getting
  (AbortHandler p sym ext (RegEntry sym t))
  (SimState p sym ext (RegEntry sym t) f args)
  (AbortHandler p sym ext (RegEntry sym t))
forall p sym ext r f1 (a :: Maybe (Ctx CrucibleType))
       (f2 :: * -> *).
Functor f2 =>
(AbortHandler p sym ext r -> f2 (AbortHandler p sym ext r))
-> SimState p sym ext r f1 a -> f2 (SimState p sym ext r f1 a)
C.abortHandler
          let initState :: ExecState p sym ext (RegEntry sym t)
initState =
                SimContext p sym ext
-> SymGlobalState sym
-> AbortHandler p sym ext (RegEntry sym t)
-> TypeRepr t
-> ExecCont
     p sym ext (RegEntry sym t) (OverrideLang t) ('Just EmptyCtx)
-> ExecState p sym ext (RegEntry sym t)
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 p sym ext
initCtx SymGlobalState sym
globs AbortHandler p sym ext (RegEntry sym t)
abortHdl TypeRepr t
rTy (ExecCont
   p sym ext (RegEntry sym t) (OverrideLang t) ('Just EmptyCtx)
 -> ExecState p sym ext (RegEntry sym t))
-> ExecCont
     p sym ext (RegEntry sym t) (OverrideLang t) ('Just EmptyCtx)
-> ExecState p sym ext (RegEntry sym t)
forall a b. (a -> b) -> a -> b
$
                  TypeRepr t
-> OverrideSim
     p sym ext (RegEntry sym t) EmptyCtx t (RegValue sym t)
-> ExecCont
     p sym ext (RegEntry sym t) (OverrideLang t) ('Just EmptyCtx)
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 t
rTy (OverrideSim p sym ext (RegEntry sym t) EmptyCtx t (RegValue sym t)
 -> ExecCont
      p sym ext (RegEntry sym t) (OverrideLang t) ('Just EmptyCtx))
-> OverrideSim
     p sym ext (RegEntry sym t) EmptyCtx t (RegValue sym t)
-> ExecCont
     p sym ext (RegEntry sym t) (OverrideLang t) ('Just EmptyCtx)
forall a b. (a -> b) -> a -> b
$
                    let args :: RegMap sym EmptyCtx
args = Assignment (RegEntry sym) EmptyCtx -> RegMap sym EmptyCtx
forall sym (ctx :: Ctx CrucibleType).
Assignment (RegEntry sym) ctx -> RegMap sym ctx
C.RegMap Assignment (RegEntry sym) EmptyCtx
forall {k} (f :: k -> *). Assignment f EmptyCtx
Ctx.empty in
                    case FnState p sym ext EmptyCtx 'UnitType
bind of
                      C.UseOverride Override p sym ext EmptyCtx 'UnitType
o -> do
                        RegEntry sym 'UnitType
_ <- FnHandle EmptyCtx 'UnitType
-> Override p sym ext EmptyCtx 'UnitType
-> RegMap sym EmptyCtx
-> OverrideSim
     p sym ext (RegEntry sym t) EmptyCtx t (RegEntry sym 'UnitType)
forall (args :: Ctx CrucibleType) (ret :: CrucibleType) p sym ext
       rtp (a :: Ctx CrucibleType) (r :: CrucibleType).
FnHandle args ret
-> Override p sym ext args ret
-> RegMap sym args
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
C.callOverride FnHandle EmptyCtx 'UnitType
hdl Override p sym ext EmptyCtx 'UnitType
o RegMap sym EmptyCtx
forall {sym}. RegMap sym EmptyCtx
args
                        ExitCode
-> OverrideSim
     p sym ext (RegEntry sym t) EmptyCtx t (RegValue sym t)
forall sym p ext rtp (args :: Ctx CrucibleType) (r :: CrucibleType)
       a.
IsSymInterface sym =>
ExitCode -> OverrideSim p sym ext rtp args r a
C.exitExecution ExitCode
Exit.ExitSuccess
                      C.UseCFG CFG ext blocks EmptyCtx 'UnitType
c CFGPostdom blocks
_ -> do
                        RegEntry sym 'UnitType
_ <- CFG ext blocks EmptyCtx 'UnitType
-> RegMap sym EmptyCtx
-> OverrideSim
     p sym ext (RegEntry sym t) EmptyCtx t (RegEntry sym 'UnitType)
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType) sym p rtp
       (a :: Ctx CrucibleType) (r :: CrucibleType).
IsSyntaxExtension ext =>
CFG ext blocks init ret
-> RegMap sym init
-> OverrideSim p sym ext rtp a r (RegEntry sym ret)
C.callCFG CFG ext blocks EmptyCtx 'UnitType
c RegMap sym EmptyCtx
forall {sym}. RegMap sym EmptyCtx
args
                        ExitCode
-> OverrideSim
     p sym ext (RegEntry sym t) EmptyCtx t (RegValue sym t)
forall sym p ext rtp (args :: Ctx CrucibleType) (r :: CrucibleType)
       a.
IsSymInterface sym =>
ExitCode -> OverrideSim p sym ext rtp args r a
C.exitExecution ExitCode
Exit.ExitSuccess
          let featRes :: ExecutionFeatureResult p sym ext (RegEntry sym t)
featRes = ExecState p sym ext (RegEntry sym t)
-> ExecutionFeatureResult p sym ext (RegEntry sym t)
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNewState ExecState p sym ext (RegEntry sym t)
initState
          (ExecutionFeatureResult p sym ext (RegEntry sym t), Response cExt)
-> IO
     (ExecutionFeatureResult p sym ext (RegEntry sym t), Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExecutionFeatureResult p sym ext (RegEntry sym t)
featRes, Response cExt
forall cExt. Response cExt
Resp.Ok)

cfg ::
  C.IsSyntaxExtension ext =>
  C.ExecState p sym ext r ->
  Maybe W4.FunctionName ->
  IO (Response cExt)
cfg :: forall ext p sym r cExt.
IsSyntaxExtension ext =>
ExecState p sym ext r -> Maybe FunctionName -> IO (Response cExt)
cfg ExecState p sym ext r
execState =
  \case
    Just FunctionName
fNm -> do
      let binds :: FunctionBindings p sym ext
binds = ExecState p sym ext r
execState ExecState p sym ext r
-> Getting
     (FunctionBindings p sym ext)
     (ExecState p sym ext r)
     (FunctionBindings p sym ext)
-> FunctionBindings p sym ext
forall s a. s -> Getting a s a -> a
Lens.^. (ExecState p sym ext r -> SimContext p sym ext)
-> (SimContext p sym ext
    -> Const (FunctionBindings p sym ext) (SimContext p sym ext))
-> ExecState p sym ext r
-> Const (FunctionBindings p sym ext) (ExecState p sym ext r)
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
Lens.to ExecState p sym ext r -> SimContext p sym ext
forall p sym ext r. ExecState p sym ext r -> SimContext p sym ext
C.execStateContext ((SimContext p sym ext
  -> Const (FunctionBindings p sym ext) (SimContext p sym ext))
 -> ExecState p sym ext r
 -> Const (FunctionBindings p sym ext) (ExecState p sym ext r))
-> ((FunctionBindings p sym ext
     -> Const (FunctionBindings p sym ext) (FunctionBindings p sym ext))
    -> SimContext p sym ext
    -> Const (FunctionBindings p sym ext) (SimContext p sym ext))
-> Getting
     (FunctionBindings p sym ext)
     (ExecState p sym ext r)
     (FunctionBindings p sym ext)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FunctionBindings p sym ext
 -> Const (FunctionBindings p sym ext) (FunctionBindings p sym ext))
-> SimContext p sym ext
-> Const (FunctionBindings p sym ext) (SimContext p sym ext)
forall p sym ext (f :: * -> *).
Functor f =>
(FunctionBindings p sym ext -> f (FunctionBindings p sym ext))
-> SimContext p sym ext -> f (SimContext p sym ext)
C.functionBindings
      let hdls :: [SomeHandle]
hdls = FnHandleMap (FnState p sym ext) -> [SomeHandle]
forall (f :: Ctx CrucibleType -> CrucibleType -> *).
FnHandleMap f -> [SomeHandle]
C.handleMapToHandles (FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
forall p sym ext.
FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
C.fnBindings FunctionBindings p sym ext
binds)
      let names :: [FunctionName]
names = (SomeHandle -> FunctionName) -> [SomeHandle] -> [FunctionName]
forall a b. (a -> b) -> [a] -> [b]
map (\(C.SomeHandle FnHandle args ret
hdl) -> FnHandle args ret -> FunctionName
forall (args :: Ctx CrucibleType) (ret :: CrucibleType).
FnHandle args ret -> FunctionName
C.handleName FnHandle args ret
hdl) [SomeHandle]
hdls
      case FunctionName
-> FnHandleMap (FnState p sym ext)
-> Maybe (SomeFn (FnState p sym ext))
forall (f :: Ctx CrucibleType -> CrucibleType -> *).
FunctionName -> FnHandleMap f -> Maybe (SomeFn f)
lookupHandleMapByName FunctionName
fNm (FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
forall p sym ext.
FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
C.fnBindings FunctionBindings p sym ext
binds) of
        Maybe (SomeFn (FnState p sym ext))
Nothing -> Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (FunctionName -> [FunctionName] -> UserError cExt
forall cExt. FunctionName -> [FunctionName] -> UserError cExt
Resp.FnNotFound FunctionName
fNm [FunctionName]
names))
        Just (SomeFn (C.UseOverride {})) -> Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (FunctionName -> UserError cExt
forall cExt. FunctionName -> UserError cExt
Resp.NotACfg FunctionName
fNm))
        Just (SomeFn (C.UseCFG CFG ext blocks args ret
c CFGPostdom blocks
_)) -> Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc Void -> Response cExt
forall cExt. Doc Void -> Response cExt
Resp.Cfg (Bool -> CFG ext blocks args ret -> Doc Void
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType) ann.
PrettyExt ext =>
Bool -> CFG ext blocks init ret -> Doc ann
C.ppCFG Bool
True CFG ext blocks args ret
c))
    Maybe FunctionName
Nothing ->
      case ExecState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
forall p sym ext r.
ExecState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
execStateSimState ExecState p sym ext r
execState of
        Left NotApplicable
notApplicable -> Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (NotApplicable -> UserError cExt
forall cExt. NotApplicable -> UserError cExt
Resp.NotApplicable NotApplicable
notApplicable))
        Right (C.SomeSimState SimState p sym ext r f args
simState) -> do
          case SimState p sym ext r f args
simState SimState p sym ext r f args
-> Getting
     (SimFrame sym ext f args)
     (SimState p sym ext r f args)
     (SimFrame sym ext f args)
-> SimFrame sym ext f args
forall s a. s -> Getting a s a -> a
Lens.^. (ActiveTree p sym ext r f args
 -> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args))
-> SimState p sym ext r f args
-> Const (SimFrame sym ext f args) (SimState p sym ext r f args)
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: * -> *).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
C.stateTree ((ActiveTree p sym ext r f args
  -> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args))
 -> SimState p sym ext r f args
 -> Const (SimFrame sym ext f args) (SimState p sym ext r f args))
-> ((SimFrame sym ext f args
     -> Const (SimFrame sym ext f args) (SimFrame sym ext f args))
    -> ActiveTree p sym ext r f args
    -> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args))
-> Getting
     (SimFrame sym ext f args)
     (SimState p sym ext r f args)
     (SimFrame sym ext f args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext f args
 -> Const (SimFrame sym ext f args) (TopFrame sym ext f args))
-> ActiveTree p sym ext r f args
-> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args)
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: * -> *).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
C.actFrame ((TopFrame sym ext f args
  -> Const (SimFrame sym ext f args) (TopFrame sym ext f args))
 -> ActiveTree p sym ext r f args
 -> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args))
-> ((SimFrame sym ext f args
     -> Const (SimFrame sym ext f args) (SimFrame sym ext f args))
    -> TopFrame sym ext f args
    -> Const (SimFrame sym ext f args) (TopFrame sym ext f args))
-> (SimFrame sym ext f args
    -> Const (SimFrame sym ext f args) (SimFrame sym ext f args))
-> ActiveTree p sym ext r f args
-> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimFrame sym ext f args
 -> Const (SimFrame sym ext f args) (SimFrame sym ext f args))
-> TopFrame sym ext f args
-> Const (SimFrame sym ext f args) (TopFrame sym ext f args)
forall sym u v (f :: * -> *).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
C.gpValue of
            C.MF (C.CallFrame { _frameCFG :: ()
C._frameCFG = CFG ext blocks initialArgs ret
c }) ->
              Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc Void -> Response cExt
forall cExt. Doc Void -> Response cExt
Resp.Cfg (Bool -> CFG ext blocks initialArgs ret -> Doc Void
forall ext (blocks :: Ctx (Ctx CrucibleType))
       (init :: Ctx CrucibleType) (ret :: CrucibleType) ann.
PrettyExt ext =>
Bool -> CFG ext blocks init ret -> Doc ann
C.ppCFG Bool
True CFG ext blocks initialArgs ret
c))
            C.OF {} -> Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (NotApplicable -> UserError cExt
forall cExt. NotApplicable -> UserError cExt
Resp.NotApplicable NotApplicable
Resp.NoCfg))
            C.RF {} -> Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (NotApplicable -> UserError cExt
forall cExt. NotApplicable -> UserError cExt
Resp.NotApplicable NotApplicable
Resp.NoCfg))

frame ::
  C.IsSyntaxExtension ext =>
  W4.IsExpr (W4.SymExpr sym) =>
  Context cExt p sym ext t ->
  C.ExecState p sym ext r ->
  IO (Response cExt)
frame :: 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)
frame Context cExt p sym ext t
_ctx ExecState p sym ext r
execState =
  case ExecState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
forall p sym ext r.
ExecState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
execStateSimState ExecState p sym ext r
execState of
    Left NotApplicable
notApplicable -> Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (NotApplicable -> UserError cExt
forall cExt. NotApplicable -> UserError cExt
Resp.NotApplicable NotApplicable
notApplicable))
    Right (C.SomeSimState SimState p sym ext r f args
simState) ->
      Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Response cExt -> IO (Response cExt))
-> Response cExt -> IO (Response cExt)
forall a b. (a -> b) -> a -> b
$ Doc Void -> Response cExt
forall cExt. Doc Void -> Response cExt
Resp.Frame (Doc Void -> Response cExt) -> Doc Void -> Response cExt
forall a b. (a -> b) -> a -> b
$
        let fr :: SimFrame sym ext f args
fr = SimState p sym ext r f args
simState SimState p sym ext r f args
-> Getting
     (SimFrame sym ext f args)
     (SimState p sym ext r f args)
     (SimFrame sym ext f args)
-> SimFrame sym ext f args
forall s a. s -> Getting a s a -> a
Lens.^. (ActiveTree p sym ext r f args
 -> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args))
-> SimState p sym ext r f args
-> Const (SimFrame sym ext f args) (SimState p sym ext r f args)
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: * -> *).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
C.stateTree ((ActiveTree p sym ext r f args
  -> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args))
 -> SimState p sym ext r f args
 -> Const (SimFrame sym ext f args) (SimState p sym ext r f args))
-> ((SimFrame sym ext f args
     -> Const (SimFrame sym ext f args) (SimFrame sym ext f args))
    -> ActiveTree p sym ext r f args
    -> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args))
-> Getting
     (SimFrame sym ext f args)
     (SimState p sym ext r f args)
     (SimFrame sym ext f args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext f args
 -> Const (SimFrame sym ext f args) (TopFrame sym ext f args))
-> ActiveTree p sym ext r f args
-> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args)
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: * -> *).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
C.actFrame ((TopFrame sym ext f args
  -> Const (SimFrame sym ext f args) (TopFrame sym ext f args))
 -> ActiveTree p sym ext r f args
 -> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args))
-> ((SimFrame sym ext f args
     -> Const (SimFrame sym ext f args) (SimFrame sym ext f args))
    -> TopFrame sym ext f args
    -> Const (SimFrame sym ext f args) (TopFrame sym ext f args))
-> (SimFrame sym ext f args
    -> Const (SimFrame sym ext f args) (SimFrame sym ext f args))
-> ActiveTree p sym ext r f args
-> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimFrame sym ext f args
 -> Const (SimFrame sym ext f args) (SimFrame sym ext f args))
-> TopFrame sym ext f args
-> Const (SimFrame sym ext f args) (TopFrame sym ext f args)
forall sym u v (f :: * -> *).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
C.gpValue in
        let name :: FunctionName
name = SimFrame sym ext f args
fr SimFrame sym ext f args
-> Getting FunctionName (SimFrame sym ext f args) FunctionName
-> FunctionName
forall s a. s -> Getting a s a -> a
Lens.^. Getting FunctionName (SimFrame sym ext f args) FunctionName
forall sym ext f1 (a :: Maybe (Ctx CrucibleType)) (f2 :: * -> *).
(Contravariant f2, Functor f2) =>
(FunctionName -> f2 FunctionName)
-> SimFrame sym ext f1 a -> f2 (SimFrame sym ext f1 a)
C.frameFunctionName in
        case SimFrame sym ext f args
fr of
          C.OF OverrideFrame sym ret args1
ovFrame ->
            let regs :: Assignment (RegEntry sym) args1
regs = RegMap sym args1 -> Assignment (RegEntry sym) args1
forall sym (ctx :: Ctx CrucibleType).
RegMap sym ctx -> Assignment (RegEntry sym) ctx
C.regMap (OverrideFrame sym ret args1
ovFrame OverrideFrame sym ret args1
-> Getting
     (RegMap sym args1) (OverrideFrame sym ret args1) (RegMap sym args1)
-> RegMap sym args1
forall s a. s -> Getting a s a -> a
Lens.^. Getting
  (RegMap sym args1) (OverrideFrame sym ret args1) (RegMap sym args1)
forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType) (f :: * -> *).
Functor f =>
(RegMap sym args -> f (RegMap sym args'))
-> OverrideFrame sym ret args -> f (OverrideFrame sym ret args')
C.overrideRegMap) in
            [Doc Void] -> Doc Void
forall ann. [Doc ann] -> Doc ann
PP.vcat
            [ Doc Void
"Override:" Doc Void -> Doc Void -> Doc Void
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> FunctionName -> Doc Void
forall a ann. Pretty a => a -> Doc ann
forall ann. FunctionName -> Doc ann
PP.pretty FunctionName
name
            , Doc Void
""
            , Doc Void
"Argument types:"
            , [Doc Void] -> Doc Void
forall ann. [Doc ann] -> Doc ann
PP.vcat ([Doc Void] -> Doc Void) -> [Doc Void] -> Doc Void
forall a b. (a -> b) -> a -> b
$ (forall (x :: CrucibleType). RegEntry sym x -> Doc Void)
-> forall (x :: Ctx CrucibleType).
   Assignment (RegEntry sym) x -> [Doc Void]
forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: CrucibleType -> *) a.
(forall (x :: CrucibleType). f x -> a)
-> forall (x :: Ctx CrucibleType). Assignment f x -> [a]
toListFC (Doc Void -> Doc Void
forall {ann}. Doc ann -> Doc ann
bullet (Doc Void -> Doc Void)
-> (RegEntry sym x -> Doc Void) -> RegEntry sym x -> Doc Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeRepr x -> Doc Void
forall ann. TypeRepr x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (TypeRepr x -> Doc Void)
-> (RegEntry sym x -> TypeRepr x) -> RegEntry sym x -> Doc Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RegEntry sym x -> TypeRepr x
forall sym (tp :: CrucibleType). RegEntry sym tp -> TypeRepr tp
C.regType) Assignment (RegEntry sym) args1
regs
            ]
          C.MF CallFrame sym ext blocks ret args1
callFrame ->
            let regs :: Assignment (RegEntry sym) args1
regs = RegMap sym args1 -> Assignment (RegEntry sym) args1
forall sym (ctx :: Ctx CrucibleType).
RegMap sym ctx -> Assignment (RegEntry sym) ctx
C.regMap (CallFrame sym ext blocks ret args1
callFrame CallFrame sym ext blocks ret args1
-> Getting
     (RegMap sym args1)
     (CallFrame sym ext blocks ret args1)
     (RegMap sym args1)
-> RegMap sym args1
forall s a. s -> Getting a s a -> a
Lens.^. Getting
  (RegMap sym args1)
  (CallFrame sym ext blocks ret args1)
  (RegMap sym args1)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType) (f :: * -> *).
Functor f =>
(RegMap sym args -> f (RegMap sym args))
-> CallFrame sym ext blocks ret args
-> f (CallFrame sym ext blocks ret args)
C.frameRegs) in
            [Doc Void] -> Doc Void
forall ann. [Doc ann] -> Doc ann
PP.vcat
              [ Doc Void
"CFG:" Doc Void -> Doc Void -> Doc Void
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> FunctionName -> Doc Void
forall a ann. Pretty a => a -> Doc ann
forall ann. FunctionName -> Doc ann
PP.pretty FunctionName
name
              , Doc Void
"Block:" Doc Void -> Doc Void -> Doc Void
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> (forall (tp :: Ctx CrucibleType). BlockID blocks tp -> Doc Void)
-> Some (BlockID blocks) -> Doc Void
forall {k} (f :: k -> *) r.
(forall (tp :: k). f tp -> r) -> Some f -> r
viewSome BlockID blocks tp -> Doc Void
forall ann. BlockID blocks tp -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall (tp :: Ctx CrucibleType). BlockID blocks tp -> Doc Void
PP.pretty (CallFrame sym ext blocks ret args1 -> Some (BlockID blocks)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType).
CallFrame sym ext blocks ret args -> Some (BlockID blocks)
C._frameBlockID CallFrame sym ext blocks ret args1
callFrame)
              , Doc Void
""
              , Doc Void
"Argument types:"
              , [Doc Void] -> Doc Void
forall ann. [Doc ann] -> Doc ann
PP.vcat ([Doc Void] -> Doc Void) -> [Doc Void] -> Doc Void
forall a b. (a -> b) -> a -> b
$ (forall (x :: CrucibleType). RegEntry sym x -> Doc Void)
-> forall (x :: Ctx CrucibleType).
   Assignment (RegEntry sym) x -> [Doc Void]
forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: CrucibleType -> *) a.
(forall (x :: CrucibleType). f x -> a)
-> forall (x :: Ctx CrucibleType). Assignment f x -> [a]
toListFC (Doc Void -> Doc Void
forall {ann}. Doc ann -> Doc ann
bullet (Doc Void -> Doc Void)
-> (RegEntry sym x -> Doc Void) -> RegEntry sym x -> Doc Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeRepr x -> Doc Void
forall ann. TypeRepr x -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (TypeRepr x -> Doc Void)
-> (RegEntry sym x -> TypeRepr x) -> RegEntry sym x -> Doc Void
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RegEntry sym x -> TypeRepr x
forall sym (tp :: CrucibleType). RegEntry sym tp -> TypeRepr tp
C.regType) Assignment (RegEntry sym) args1
regs
              ]
          C.RF {} -> Doc Void
"Return:" Doc Void -> Doc Void -> Doc Void
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+> FunctionName -> Doc Void
forall a ann. Pretty a => a -> Doc ann
forall ann. FunctionName -> Doc ann
PP.pretty FunctionName
name
  where bullet :: Doc ann -> Doc ann
bullet = (Doc ann
"-" Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+>) (Doc ann -> Doc ann) -> (Doc ann -> Doc ann) -> Doc ann -> Doc ann
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc ann -> Doc ann
forall {ann}. Doc ann -> Doc ann
PP.align

help ::
  C.IsSyntaxExtension ext =>
  (?parserHooks :: C.ParserHooks ext) =>
  PP.Pretty cExt =>
  Cmd.CommandExt cExt ->
  Maybe (Cmd.Command cExt) ->
  Response cExt
help :: forall ext cExt.
(IsSyntaxExtension ext, ?parserHooks::ParserHooks ext,
 Pretty cExt) =>
CommandExt cExt -> Maybe (Command cExt) -> Response cExt
help CommandExt cExt
cExts =
  \case
    Maybe (Command cExt)
Nothing ->
      let mkHelp :: Command cExt -> Text
mkHelp Command cExt
c = CommandExt cExt -> Command cExt -> Text
forall cExt. CommandExt cExt -> Command cExt -> Text
Cmd.name CommandExt cExt
cExts Command cExt
c Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" (" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> CommandExt cExt -> Command cExt -> Text
forall cExt. CommandExt cExt -> Command cExt -> Text
Cmd.abbrev CommandExt cExt
cExts Command cExt
c Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
")" Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
": " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> CommandExt cExt -> Command cExt -> Text
forall cExt. CommandExt cExt -> Command cExt -> Text
Cmd.help CommandExt cExt
cExts Command cExt
c in
      Doc Void -> Response cExt
forall cExt. Doc Void -> Response cExt
Resp.Help (Text -> Doc Void
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty ([Text] -> Text
Text.unlines ([Text] -> [Text]
forall a. Ord a => [a] -> [a]
List.sort ((Command cExt -> Text) -> [Command cExt] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map Command cExt -> Text
mkHelp (CommandExt cExt -> [Command cExt]
forall cExt. CommandExt cExt -> [Command cExt]
Cmd.allCmds CommandExt cExt
cExts)))))
    Just Command cExt
cmd -> 
      Doc Void -> Response cExt
forall cExt. Doc Void -> Response cExt
Resp.Help (Doc Void -> Response cExt) -> Doc Void -> Response cExt
forall a b. (a -> b) -> a -> b
$
        -- See 'Lang.Crucible.Debug.Command.ext{Detail,Help}' for expectations
        -- on these strings, which are why it makes sense to format them this
        -- way (e.g., adding a period, printing "details" after "help"), etc.
        let basic :: [Doc Void]
basic = [CommandExt cExt -> Command cExt -> Doc Void
forall cExt ann.
Pretty cExt =>
CommandExt cExt -> Command cExt -> Doc ann
usage CommandExt cExt
cExts Command cExt
cmd, Doc Void
"", Text -> Doc Void
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty (CommandExt cExt -> Command cExt -> Text
forall cExt. CommandExt cExt -> Command cExt -> Text
Cmd.help CommandExt cExt
cExts Command cExt
cmd) Doc Void -> Doc Void -> Doc Void
forall a. Semigroup a => a -> a -> a
<> Doc Void
"."]
            detail :: [Doc Void]
detail =
              case CommandExt cExt -> Command cExt -> Maybe Text
forall cExt. CommandExt cExt -> Command cExt -> Maybe Text
Cmd.detail CommandExt cExt
cExts Command cExt
cmd of
                Just Text
more -> [Doc Void
"", Text -> Doc Void
forall ann. Text -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty Text
more]
                Maybe Text
Nothing -> []
        in [Doc Void] -> Doc Void
forall ann. [Doc ann] -> Doc ann
PP.vcat ([Doc Void]
basic [Doc Void] -> [Doc Void] -> [Doc Void]
forall a. [a] -> [a] -> [a]
++ [Doc Void]
detail)

load ::
  C.IsSyntaxExtension ext =>
  (?parserHooks :: C.ParserHooks ext) =>
  C.ExecState p sym ext r ->
  FilePath ->
  IO (C.ExecutionFeatureResult p sym ext r, Response cExt)
load :: 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)
load ExecState p sym ext r
execState0 FilePath
path = do
  Either IOException Text
eTxt <- IO Text -> IO (Either IOException Text)
forall e a. Exception e => IO a -> IO (Either e a)
X.try (FilePath -> IO Text
IO.readFile FilePath
path)
  case Either IOException Text
eTxt of
    Left IOException
ioErr -> (ExecutionFeatureResult p sym ext r, Response cExt)
-> IO (ExecutionFeatureResult p sym ext r, Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExecutionFeatureResult p sym ext r
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNoChange, IOException -> Response cExt
forall cExt. IOException -> Response cExt
Resp.IOError IOException
ioErr)
    Right Text
txt -> do
      case Parsec Void Text [Syntax Atomic]
-> FilePath
-> Text
-> Either (ParseErrorBundle Text Void) [Syntax Atomic]
forall e s a.
Parsec e s a -> FilePath -> s -> Either (ParseErrorBundle s e) a
MP.parse (Parser ()
C.skipWhitespace Parser ()
-> Parsec Void Text [Syntax Atomic]
-> Parsec Void Text [Syntax Atomic]
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity b
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f b
*> ParsecT Void Text Identity (Syntax Atomic)
-> Parsec Void Text [Syntax Atomic]
forall (m :: * -> *) a. MonadPlus m => m a -> m [a]
MP.many (Parser Atomic -> ParsecT Void Text Identity (Syntax Atomic)
forall a. Parser a -> Parser (Syntax a)
C.sexp Parser Atomic
C.atom) Parsec Void Text [Syntax Atomic]
-> Parser () -> Parsec Void Text [Syntax Atomic]
forall a b.
ParsecT Void Text Identity a
-> ParsecT Void Text Identity b -> ParsecT Void Text Identity a
forall (f :: * -> *) a b. Applicative f => f a -> f b -> f a
<* Parser ()
forall e s (m :: * -> *). MonadParsec e s m => m ()
MP.eof) FilePath
path Text
txt of
        Left ParseErrorBundle Text Void
err -> (ExecutionFeatureResult p sym ext r, Response cExt)
-> IO (ExecutionFeatureResult p sym ext r, Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExecutionFeatureResult p sym ext r
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNoChange, UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (ParseErrorBundle Text Void -> UserError cExt
forall cExt. ParseErrorBundle Text Void -> UserError cExt
Resp.LoadParseError ParseErrorBundle Text Void
err))
        Right [Syntax Atomic]
v ->
          (forall s.
 NonceGenerator IO s
 -> IO (ExecutionFeatureResult p sym ext r, Response cExt))
-> IO (ExecutionFeatureResult p sym ext r, Response cExt)
forall r. (forall s. NonceGenerator IO s -> IO r) -> IO r
Nonce.withIONonceGenerator ((forall s.
  NonceGenerator IO s
  -> IO (ExecutionFeatureResult p sym ext r, Response cExt))
 -> IO (ExecutionFeatureResult p sym ext r, Response cExt))
-> (forall s.
    NonceGenerator IO s
    -> IO (ExecutionFeatureResult p sym ext r, Response cExt))
-> IO (ExecutionFeatureResult p sym ext r, Response cExt)
forall a b. (a -> b) -> a -> b
$ \NonceGenerator IO s
ng -> do
            let execCtx :: SimContext p sym ext
execCtx = ExecState p sym ext r -> SimContext p sym ext
forall p sym ext r. ExecState p sym ext r -> SimContext p sym ext
C.execStateContext ExecState p sym ext r
execState0
            let ha :: HandleAllocator
ha = SimContext p sym ext -> HandleAllocator
forall personality sym ext.
SimContext personality sym ext -> HandleAllocator
C.simHandleAllocator SimContext p sym ext
execCtx
            Either (ExprErr s) (ParsedProgram ext)
parseResult <- NonceGenerator IO s
-> HandleAllocator
-> [(SomeHandle, Position)]
-> TopParser s (ParsedProgram ext)
-> IO (Either (ExprErr s) (ParsedProgram ext))
forall s a.
NonceGenerator IO s
-> HandleAllocator
-> [(SomeHandle, Position)]
-> TopParser s a
-> IO (Either (ExprErr s) a)
C.top NonceGenerator IO s
ng HandleAllocator
ha [] (TopParser s (ParsedProgram ext)
 -> IO (Either (ExprErr s) (ParsedProgram ext)))
-> TopParser s (ParsedProgram ext)
-> IO (Either (ExprErr s) (ParsedProgram ext))
forall a b. (a -> b) -> a -> b
$ [Syntax Atomic] -> TopParser s (ParsedProgram ext)
forall ext s.
(TraverseExt ext, IsSyntaxExtension ext,
 ?parserHooks::ParserHooks ext) =>
[Syntax Atomic] -> TopParser s (ParsedProgram ext)
C.prog [Syntax Atomic]
v
            case Either (ExprErr s) (ParsedProgram ext)
parseResult of
              Left ExprErr s
err ->
                (ExecutionFeatureResult p sym ext r, Response cExt)
-> IO (ExecutionFeatureResult p sym ext r, Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExecutionFeatureResult p sym ext r
forall p sym ext rtp. ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureNoChange, UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (Doc Void -> UserError cExt
forall cExt. Doc Void -> UserError cExt
Resp.LoadSyntaxError (ExprErr s -> Doc Void
forall ann. ExprErr s -> Doc ann
forall a ann. Pretty a => a -> Doc ann
PP.pretty ExprErr s
err)))
              Right (C.ParsedProgram{ parsedProgCFGs :: forall ext. ParsedProgram ext -> [AnyCFG ext]
C.parsedProgCFGs = [AnyCFG ext]
cfgs }) -> do
                let binds :: FnHandleMap (FnState p sym ext)
binds = ExecState p sym ext r
execState0 ExecState p sym ext r
-> Getting
     (FnHandleMap (FnState p sym ext))
     (ExecState p sym ext r)
     (FnHandleMap (FnState p sym ext))
-> FnHandleMap (FnState p sym ext)
forall s a. s -> Getting a s a -> a
Lens.^. (ExecState p sym ext r -> SimContext p sym ext)
-> (SimContext p sym ext
    -> Const (FnHandleMap (FnState p sym ext)) (SimContext p sym ext))
-> ExecState p sym ext r
-> Const (FnHandleMap (FnState p sym ext)) (ExecState p sym ext r)
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
Lens.to ExecState p sym ext r -> SimContext p sym ext
forall p sym ext r. ExecState p sym ext r -> SimContext p sym ext
C.execStateContext ((SimContext p sym ext
  -> Const (FnHandleMap (FnState p sym ext)) (SimContext p sym ext))
 -> ExecState p sym ext r
 -> Const (FnHandleMap (FnState p sym ext)) (ExecState p sym ext r))
-> ((FnHandleMap (FnState p sym ext)
     -> Const
          (FnHandleMap (FnState p sym ext))
          (FnHandleMap (FnState p sym ext)))
    -> SimContext p sym ext
    -> Const (FnHandleMap (FnState p sym ext)) (SimContext p sym ext))
-> Getting
     (FnHandleMap (FnState p sym ext))
     (ExecState p sym ext r)
     (FnHandleMap (FnState p sym ext))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FunctionBindings p sym ext
 -> Const
      (FnHandleMap (FnState p sym ext)) (FunctionBindings p sym ext))
-> SimContext p sym ext
-> Const (FnHandleMap (FnState p sym ext)) (SimContext p sym ext)
forall p sym ext (f :: * -> *).
Functor f =>
(FunctionBindings p sym ext -> f (FunctionBindings p sym ext))
-> SimContext p sym ext -> f (SimContext p sym ext)
C.functionBindings ((FunctionBindings p sym ext
  -> Const
       (FnHandleMap (FnState p sym ext)) (FunctionBindings p sym ext))
 -> SimContext p sym ext
 -> Const (FnHandleMap (FnState p sym ext)) (SimContext p sym ext))
-> ((FnHandleMap (FnState p sym ext)
     -> Const
          (FnHandleMap (FnState p sym ext))
          (FnHandleMap (FnState p sym ext)))
    -> FunctionBindings p sym ext
    -> Const
         (FnHandleMap (FnState p sym ext)) (FunctionBindings p sym ext))
-> (FnHandleMap (FnState p sym ext)
    -> Const
         (FnHandleMap (FnState p sym ext))
         (FnHandleMap (FnState p sym ext)))
-> SimContext p sym ext
-> Const (FnHandleMap (FnState p sym ext)) (SimContext p sym ext)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext))
-> (FnHandleMap (FnState p sym ext)
    -> Const
         (FnHandleMap (FnState p sym ext))
         (FnHandleMap (FnState p sym ext)))
-> FunctionBindings p sym ext
-> Const
     (FnHandleMap (FnState p sym ext)) (FunctionBindings p sym ext)
forall (p :: * -> * -> *) (f :: * -> *) s a.
(Profunctor p, Contravariant f) =>
(s -> a) -> Optic' p f s a
Lens.to FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
forall p sym ext.
FunctionBindings p sym ext -> FnHandleMap (FnState p sym ext)
C.fnBindings
                let binds' :: FnHandleMap (FnState p sym ext)
binds' = (FnHandleMap (FnState p sym ext)
 -> AnyCFG ext -> FnHandleMap (FnState p sym ext))
-> FnHandleMap (FnState p sym ext)
-> [AnyCFG ext]
-> FnHandleMap (FnState p sym ext)
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\FnHandleMap (FnState p sym ext)
bs (C.Reg.AnyCFG CFG ext blocks init ret
c) -> CFG ext blocks init ret
-> FnHandleMap (FnState p sym ext)
-> FnHandleMap (FnState p sym ext)
forall ext blocks (init :: Ctx CrucibleType) (ret :: CrucibleType)
       p sym.
IsSyntaxExtension ext =>
CFG ext blocks init ret
-> FnHandleMap (FnState p sym ext)
-> FnHandleMap (FnState p sym ext)
insertCfg CFG ext blocks init ret
c FnHandleMap (FnState p sym ext)
bs) FnHandleMap (FnState p sym ext)
binds [AnyCFG ext]
cfgs
                let execState :: ExecState p sym ext r
execState = (SimContext p sym ext -> SimContext p sym ext)
-> ExecState p sym ext r -> ExecState p sym ext r
forall p sym ext r.
(SimContext p sym ext -> SimContext p sym ext)
-> ExecState p sym ext r -> ExecState p sym ext r
modifySimContext (\SimContext p sym ext
c -> SimContext p sym ext
c SimContext p sym ext
-> (SimContext p sym ext -> SimContext p sym ext)
-> SimContext p sym ext
forall a b. a -> (a -> b) -> b
Lens.& (FunctionBindings p sym ext
 -> Identity (FunctionBindings p sym ext))
-> SimContext p sym ext -> Identity (SimContext p sym ext)
forall p sym ext (f :: * -> *).
Functor f =>
(FunctionBindings p sym ext -> f (FunctionBindings p sym ext))
-> SimContext p sym ext -> f (SimContext p sym ext)
C.functionBindings ((FunctionBindings p sym ext
  -> Identity (FunctionBindings p sym ext))
 -> SimContext p sym ext -> Identity (SimContext p sym ext))
-> FunctionBindings p sym ext
-> SimContext p sym ext
-> SimContext p sym ext
forall s t a b. ASetter s t a b -> b -> s -> t
Lens..~ 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)
binds') ExecState p sym ext r
execState0
                let featRes :: ExecutionFeatureResult p sym ext r
featRes = ExecState p sym ext r -> ExecutionFeatureResult p sym ext r
forall p sym ext rtp.
ExecState p sym ext rtp -> ExecutionFeatureResult p sym ext rtp
C.ExecutionFeatureModifiedState ExecState p sym ext r
execState
                (ExecutionFeatureResult p sym ext r, Response cExt)
-> IO (ExecutionFeatureResult p sym ext r, Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (ExecutionFeatureResult p sym ext r
featRes, FilePath -> Int -> Response cExt
forall cExt. FilePath -> Int -> Response cExt
Resp.Load FilePath
path ([AnyCFG ext] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [AnyCFG ext]
cfgs))

prove ::
  (sym ~ W4.ExprBuilder t st fs) =>
  C.IsSymBackend sym bak =>
  bak ->
  IO (Response cExt)
prove :: forall sym t (st :: * -> *) fs bak cExt.
(sym ~ ExprBuilder t st fs, IsSymBackend sym bak) =>
bak -> IO (Response cExt)
prove bak
bak = do
  let sym :: ExprBuilder t st fs
sym = bak -> ExprBuilder t st fs
forall sym bak. HasSymInterface sym bak => bak -> sym
C.backendGetSym bak
bak
  -- TODO(#270?): Configurable timeout
  let timeout :: Timeout
timeout = Seconds -> Timeout
CTO.Timeout (Int -> Seconds
Sec.secondsFromInt Int
5)
  -- TODO(#266): Configurable prover
  [ConfigDesc] -> Config -> IO ()
W4.extendConfig [ConfigDesc]
W4.z3Options (ExprBuilder t st fs -> Config
forall sym. IsExprBuilder sym => sym -> Config
W4.getConfiguration ExprBuilder t st fs
sym)
  let prover :: Prover
  (ExprBuilder t st fs)
  (ExceptT TimedOut IO)
  t
  (Seq (Doc Void, ProofResult))
prover = Timeout
-> IsSymExprBuilder (ExprBuilder t st fs) =>
   ExprBuilder t st fs
   -> LogData
   -> SolverAdapter st
   -> Prover
        (ExprBuilder t st fs)
        (ExceptT TimedOut IO)
        t
        (Seq (Doc Void, ProofResult))
forall (m :: * -> *) sym t (st :: * -> *) fs r.
(MonadError TimedOut m, MonadIO m, sym ~ ExprBuilder t st fs) =>
Timeout
-> IsSymExprBuilder sym =>
   sym -> LogData -> SolverAdapter st -> Prover sym m t r
Prove.offlineProver Timeout
timeout ExprBuilder t st fs
sym LogData
W4.defaultLogData SolverAdapter st
forall (st :: * -> *). SolverAdapter st
W4.z3Adapter
  let strat :: ProofStrategy
  (ExprBuilder t st fs)
  (ExceptT TimedOut IO)
  t
  (Seq (Doc Void, ProofResult))
strat = Prover
  (ExprBuilder t st fs)
  (ExceptT TimedOut IO)
  t
  (Seq (Doc Void, ProofResult))
-> Combiner (ExceptT TimedOut IO) (Seq (Doc Void, ProofResult))
-> ProofStrategy
     (ExprBuilder t st fs)
     (ExceptT TimedOut IO)
     t
     (Seq (Doc Void, ProofResult))
forall sym (m :: * -> *) t r.
Prover sym m t r -> Combiner m r -> ProofStrategy sym m t r
Prove.ProofStrategy Prover
  (ExprBuilder t st fs)
  (ExceptT TimedOut IO)
  t
  (Seq (Doc Void, ProofResult))
prover Combiner (ExceptT TimedOut IO) (Seq (Doc Void, ProofResult))
forall (m :: * -> *) r. (Monad m, Semigroup r) => Combiner m r
Prove.keepGoing
  let convertResult :: ProofResult sym t -> ProofResult
convertResult =
        \case
          Prove.Proved {} -> ProofResult
Resp.Proved
          Prove.Disproved {} -> ProofResult
Resp.Disproved
          Prove.Unknown {} -> ProofResult
Resp.Unknown
  let printer :: ProofConsumer (ExprBuilder t st fs) t (Seq (Doc Void, ProofResult))
printer = (ProofObligation (ExprBuilder t st fs)
 -> ProofResult (ExprBuilder t st fs) t
 -> IO (Seq (Doc Void, ProofResult)))
-> ProofConsumer
     (ExprBuilder t st fs) t (Seq (Doc Void, ProofResult))
forall sym t r.
(ProofObligation sym -> ProofResult sym t -> IO r)
-> ProofConsumer sym t r
Prove.ProofConsumer ((ProofObligation (ExprBuilder t st fs)
  -> ProofResult (ExprBuilder t st fs) t
  -> IO (Seq (Doc Void, ProofResult)))
 -> ProofConsumer
      (ExprBuilder t st fs) t (Seq (Doc Void, ProofResult)))
-> (ProofObligation (ExprBuilder t st fs)
    -> ProofResult (ExprBuilder t st fs) t
    -> IO (Seq (Doc Void, ProofResult)))
-> ProofConsumer
     (ExprBuilder t st fs) t (Seq (Doc Void, ProofResult))
forall a b. (a -> b) -> a -> b
$ \ProofObligation (ExprBuilder t st fs)
goal ProofResult (ExprBuilder t st fs) t
res -> do
        Doc Void
doc <- ExprBuilder t st fs
-> ProofObligation (ExprBuilder t st fs) -> IO (Doc Void)
forall sym ann.
IsExprBuilder sym =>
sym -> ProofObligation sym -> IO (Doc ann)
C.ppProofObligation ExprBuilder t st fs
sym ProofObligation (ExprBuilder t st fs)
goal
        Seq (Doc Void, ProofResult) -> IO (Seq (Doc Void, ProofResult))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([(Doc Void, ProofResult)] -> Seq (Doc Void, ProofResult)
forall a. [a] -> Seq a
Seq.fromList [(Doc Void
doc, ProofResult (ExprBuilder t st fs) t -> ProofResult
forall {sym} {t}. ProofResult sym t -> ProofResult
convertResult ProofResult (ExprBuilder t st fs) t
res)])
  ExceptT TimedOut IO (Seq (Doc Void, ProofResult))
-> IO (Either TimedOut (Seq (Doc Void, ProofResult)))
forall e (m :: * -> *) a. ExceptT e m a -> m (Either e a)
runExceptT (bak
-> ProofStrategy
     (ExprBuilder t st fs)
     (ExceptT TimedOut IO)
     t
     (Seq (Doc Void, ProofResult))
-> ProofConsumer
     (ExprBuilder t st fs) t (Seq (Doc Void, ProofResult))
-> ExceptT TimedOut IO (Seq (Doc Void, ProofResult))
forall (m :: * -> *) r sym t (st :: * -> *) fs bak.
(MonadIO m, Monoid r, sym ~ ExprBuilder t st fs,
 IsSymBackend sym bak) =>
bak -> ProofStrategy sym m t r -> ProofConsumer sym t r -> m r
Prove.proveCurrentObligations bak
bak ProofStrategy
  (ExprBuilder t st fs)
  (ExceptT TimedOut IO)
  t
  (Seq (Doc Void, ProofResult))
strat ProofConsumer (ExprBuilder t st fs) t (Seq (Doc Void, ProofResult))
printer) IO (Either TimedOut (Seq (Doc Void, ProofResult)))
-> (Either TimedOut (Seq (Doc Void, ProofResult))
    -> IO (Response cExt))
-> IO (Response cExt)
forall a b. IO a -> (a -> IO b) -> IO b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
    \case
      Left TimedOut
CTO.TimedOut -> Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Response cExt
forall cExt. Response cExt
Resp.ProveTimeout
      Right Seq (Doc Void, ProofResult)
results -> Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Seq (Doc Void, ProofResult) -> Response cExt
forall cExt. Seq (Doc Void, ProofResult) -> Response cExt
Resp.Prove Seq (Doc Void, ProofResult)
results)

-- TODO: Support taking a function or block name
reg ::
  forall p sym ext r t cExt.
  W4.IsExpr (W4.SymExpr sym) =>
  Context cExt p sym ext t ->
  C.ExecState p sym ext r ->
  [Int] ->
  IO (Response cExt)
reg :: 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)
reg Context cExt p sym ext t
ctx ExecState p sym ext r
execState [Int]
idxs =
  case ExecState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
forall p sym ext r.
ExecState p sym ext r
-> Either NotApplicable (SomeSimState p sym ext r)
execStateSimState ExecState p sym ext r
execState of
    Left NotApplicable
notApplicable -> Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (NotApplicable -> UserError cExt
forall cExt. NotApplicable -> UserError cExt
Resp.NotApplicable NotApplicable
notApplicable))
    Right (C.SomeSimState SimState p sym ext r f args
simState) -> do
      let fr :: SimFrame sym ext f args
fr = SimState p sym ext r f args
simState SimState p sym ext r f args
-> Getting
     (SimFrame sym ext f args)
     (SimState p sym ext r f args)
     (SimFrame sym ext f args)
-> SimFrame sym ext f args
forall s a. s -> Getting a s a -> a
Lens.^. (ActiveTree p sym ext r f args
 -> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args))
-> SimState p sym ext r f args
-> Const (SimFrame sym ext f args) (SimState p sym ext r f args)
forall p sym ext rtp f1 (a :: Maybe (Ctx CrucibleType)) g
       (b :: Maybe (Ctx CrucibleType)) (f2 :: * -> *).
Functor f2 =>
(ActiveTree p sym ext rtp f1 a
 -> f2 (ActiveTree p sym ext rtp g b))
-> SimState p sym ext rtp f1 a -> f2 (SimState p sym ext rtp g b)
C.stateTree ((ActiveTree p sym ext r f args
  -> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args))
 -> SimState p sym ext r f args
 -> Const (SimFrame sym ext f args) (SimState p sym ext r f args))
-> ((SimFrame sym ext f args
     -> Const (SimFrame sym ext f args) (SimFrame sym ext f args))
    -> ActiveTree p sym ext r f args
    -> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args))
-> Getting
     (SimFrame sym ext f args)
     (SimState p sym ext r f args)
     (SimFrame sym ext f args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (TopFrame sym ext f args
 -> Const (SimFrame sym ext f args) (TopFrame sym ext f args))
-> ActiveTree p sym ext r f args
-> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args)
forall p sym ext root f1 (args :: Maybe (Ctx CrucibleType))
       (args' :: Maybe (Ctx CrucibleType)) (f2 :: * -> *).
Functor f2 =>
(TopFrame sym ext f1 args -> f2 (TopFrame sym ext f1 args'))
-> ActiveTree p sym ext root f1 args
-> f2 (ActiveTree p sym ext root f1 args')
C.actFrame ((TopFrame sym ext f args
  -> Const (SimFrame sym ext f args) (TopFrame sym ext f args))
 -> ActiveTree p sym ext r f args
 -> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args))
-> ((SimFrame sym ext f args
     -> Const (SimFrame sym ext f args) (SimFrame sym ext f args))
    -> TopFrame sym ext f args
    -> Const (SimFrame sym ext f args) (TopFrame sym ext f args))
-> (SimFrame sym ext f args
    -> Const (SimFrame sym ext f args) (SimFrame sym ext f args))
-> ActiveTree p sym ext r f args
-> Const (SimFrame sym ext f args) (ActiveTree p sym ext r f args)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (SimFrame sym ext f args
 -> Const (SimFrame sym ext f args) (SimFrame sym ext f args))
-> TopFrame sym ext f args
-> Const (SimFrame sym ext f args) (TopFrame sym ext f args)
forall sym u v (f :: * -> *).
Functor f =>
(u -> f v) -> GlobalPair sym u -> f (GlobalPair sym v)
C.gpValue
      let regs :: Maybe (C.Some (C.RegMap sym))
          regs :: Maybe (Some (RegMap sym))
regs =
            case SimFrame sym ext f args
fr of
              C.OF OverrideFrame sym ret args1
ovFrame ->
                Some (RegMap sym) -> Maybe (Some (RegMap sym))
forall a. a -> Maybe a
Just (RegMap sym args1 -> Some (RegMap sym)
forall k (f :: k -> *) (x :: k). f x -> Some f
C.Some (OverrideFrame sym ret args1
ovFrame OverrideFrame sym ret args1
-> Getting
     (RegMap sym args1) (OverrideFrame sym ret args1) (RegMap sym args1)
-> RegMap sym args1
forall s a. s -> Getting a s a -> a
Lens.^. Getting
  (RegMap sym args1) (OverrideFrame sym ret args1) (RegMap sym args1)
forall sym (ret :: CrucibleType) (args :: Ctx CrucibleType)
       (args' :: Ctx CrucibleType) (f :: * -> *).
Functor f =>
(RegMap sym args -> f (RegMap sym args'))
-> OverrideFrame sym ret args -> f (OverrideFrame sym ret args')
C.overrideRegMap))
              C.MF CallFrame sym ext blocks ret args1
callFrame ->
                Some (RegMap sym) -> Maybe (Some (RegMap sym))
forall a. a -> Maybe a
Just (RegMap sym args1 -> Some (RegMap sym)
forall k (f :: k -> *) (x :: k). f x -> Some f
C.Some (CallFrame sym ext blocks ret args1
callFrame CallFrame sym ext blocks ret args1
-> Getting
     (RegMap sym args1)
     (CallFrame sym ext blocks ret args1)
     (RegMap sym args1)
-> RegMap sym args1
forall s a. s -> Getting a s a -> a
Lens.^. Getting
  (RegMap sym args1)
  (CallFrame sym ext blocks ret args1)
  (RegMap sym args1)
forall sym ext (blocks :: Ctx (Ctx CrucibleType))
       (ret :: CrucibleType) (args :: Ctx CrucibleType) (f :: * -> *).
Functor f =>
(RegMap sym args -> f (RegMap sym args))
-> CallFrame sym ext blocks ret args
-> f (CallFrame sym ext blocks ret args)
C.frameRegs))
              C.RF {} ->
                Maybe (Some (RegMap sym))
forall a. Maybe a
Nothing
      case Maybe (Some (RegMap sym))
regs of
        Maybe (Some (RegMap sym))
Nothing -> Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (NotApplicable -> UserError cExt
forall cExt. NotApplicable -> UserError cExt
Resp.NotApplicable NotApplicable
Resp.NoFrame))
        Just (C.Some (C.RegMap Assignment (RegEntry sym) x
rs)) -> do
          let sz :: Size x
sz = Assignment (RegEntry sym) x -> Size x
forall {k} (f :: k -> *) (ctx :: Ctx k).
Assignment f ctx -> Size ctx
Ctx.size Assignment (RegEntry sym) x
rs
          let mIdxs :: Either Int [Some (Index x)]
mIdxs =
                if [Int] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
List.null [Int]
idxs
                then [Some (Index x)] -> Either Int [Some (Index x)]
forall a b. b -> Either a b
Right ((forall (x :: CrucibleType). Index x x -> Some (Index x))
-> forall (x :: Ctx CrucibleType).
   Assignment (Index x) x -> [Some (Index x)]
forall k l (t :: (k -> *) -> l -> *) (f :: k -> *) a.
FoldableFC t =>
(forall (x :: k). f x -> a) -> forall (x :: l). t f x -> [a]
forall (f :: CrucibleType -> *) a.
(forall (x :: CrucibleType). f x -> a)
-> forall (x :: Ctx CrucibleType). Assignment f x -> [a]
toListFC Index x x -> Some (Index x)
forall k (f :: k -> *) (x :: k). f x -> Some f
forall (x :: CrucibleType). Index x x -> Some (Index x)
Some (Size x
-> (forall (tp :: CrucibleType). Index x tp -> Index x tp)
-> Assignment (Index x) x
forall {k} (ctx :: Ctx k) (f :: k -> *).
Size ctx
-> (forall (tp :: k). Index ctx tp -> f tp) -> Assignment f ctx
Ctx.generate Size x
sz Index x tp -> Index x tp
forall a. a -> a
forall (tp :: CrucibleType). Index x tp -> Index x tp
id))  -- all indices
                else (Int -> Either Int (Some (Index x)))
-> [Int] -> Either Int [Some (Index x)]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (\Int
i -> Int -> Maybe (Some (Index x)) -> Either Int (Some (Index x))
forall e a. e -> Maybe a -> Either e a
maybeToEither Int
i (Int -> Size x -> Maybe (Some (Index x))
forall {k} (ctx :: Ctx k).
Int -> Size ctx -> Maybe (Some (Index ctx))
Ctx.intIndex Int
i Size x
sz)) [Int]
idxs
          let ppArg :: Some (Index x) -> Doc Void
ppArg (C.Some Index x x
idx) =
                let C.RegEntry TypeRepr x
ty RegValue sym x
val = Assignment (RegEntry sym) x
rs Assignment (RegEntry sym) x
-> Getting
     (RegEntry sym x) (Assignment (RegEntry sym) x) (RegEntry sym x)
-> RegEntry sym x
forall s a. s -> Getting a s a -> a
Lens.^. IndexF (Assignment (RegEntry sym) x) x
-> Lens'
     (Assignment (RegEntry sym) x)
     (IxValueF (Assignment (RegEntry sym) x) x)
forall k m (x :: k).
IxedF' k m =>
IndexF m x -> Lens' m (IxValueF m x)
forall (x :: CrucibleType).
IndexF (Assignment (RegEntry sym) x) x
-> Lens'
     (Assignment (RegEntry sym) x)
     (IxValueF (Assignment (RegEntry sym) x) x)
ixF' IndexF (Assignment (RegEntry sym) x) x
Index x x
idx in
                IntrinsicPrinters sym -> TypeRepr x -> RegValue' sym x -> Doc Void
forall sym (tp :: CrucibleType) ann.
IsExpr (SymExpr sym) =>
IntrinsicPrinters sym -> TypeRepr tp -> RegValue' sym tp -> Doc ann
ppRegVal (Context cExt p sym ext t -> IntrinsicPrinters sym
forall cExt p sym ext (t :: CrucibleType).
Context cExt p sym ext t -> IntrinsicPrinters sym
Ctxt.dbgPpIntrinsic Context cExt p sym ext t
ctx) TypeRepr x
ty (RegValue sym x -> RegValue' sym x
forall sym (tp :: CrucibleType).
RegValue sym tp -> RegValue' sym tp
C.RV RegValue sym x
val)
          case Either Int [Some (Index x)]
mIdxs of
            Left Int
i -> Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (Int -> UserError cExt
forall cExt. Int -> UserError cExt
Resp.NoSuchArgument Int
i))
            Right [Some (Index x)]
idxs' -> Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Doc Void -> Response cExt
forall cExt. Doc Void -> Response cExt
Resp.Arg ([Doc Void] -> Doc Void
forall ann. [Doc ann] -> Doc ann
PP.vcat ((Some (Index x) -> Doc Void) -> [Some (Index x)] -> [Doc Void]
forall a b. (a -> b) -> [a] -> [b]
List.map Some (Index x) -> Doc Void
ppArg [Some (Index x)]
idxs')))
  where
    maybeToEither :: e -> Maybe a -> Either e a
    maybeToEither :: forall e a. e -> Maybe a -> Either e a
maybeToEither e
e =
      \case
        Maybe a
Nothing -> e -> Either e a
forall a b. a -> Either a b
Left e
e
        Just a
a -> a -> Either e a
forall a b. b -> Either a b
Right a
a

secret ::
  PP.Pretty cExt =>
  Context cExt p sym ext t ->
  C.ExecState p sym ext r ->
  Rgx.Match (Arg.Arg cExt) BCmd.SecretRegex ->
  IO (Resp.Response cExt)
secret :: 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)
secret Context cExt p sym ext t
ctx ExecState p sym ext r
execState Match (Arg cExt) SecretRegex
m =
  let cExt :: CommandExt cExt
cExt = 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 in
  case Match (Arg cExt) SecretRegex
m of
    -- Show what sort of tab-completion should be provided by the UI
    Rgx.MLeft (Rgx.MThen Match (Arg cExt) l
_complete (Rgx.MThen (Rgx.MLit (Arg.ACommand Command cExt
cmd)) (Rgx.MStar [Match (Arg cExt) r1]
args0))) -> do
      let args :: [FilePath]
args = (Match (Arg cExt) r1 -> FilePath)
-> [Match (Arg cExt) r1] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map (\(Rgx.MLit (Arg.AText Text
t)) -> Text -> FilePath
Text.unpack Text
t) [Match (Arg cExt) r1]
args0
      let cEnv :: CompletionEnv cExt
cEnv = Context cExt p sym ext t
-> ExecState p sym ext r -> 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 sym ext t
ctx ExecState p sym ext r
execState
      let line :: FilePath
line = [FilePath] -> FilePath
unwords (Doc Any -> FilePath
forall a. Show a => a -> FilePath
show (Command cExt -> Doc Any
forall a ann. Pretty a => a -> Doc ann
forall ann. Command cExt -> Doc ann
PP.pretty Command cExt
cmd) FilePath -> [FilePath] -> [FilePath]
forall a. a -> [a] -> [a]
: (FilePath -> FilePath) -> [FilePath] -> [FilePath]
forall a b. (a -> b) -> [a] -> [b]
map ((Char -> Bool) -> FilePath -> FilePath
forall a. (a -> Bool) -> [a] -> [a]
filter (Char -> Char -> Bool
forall a. Eq a => a -> a -> Bool
/= Char
'_')) [FilePath]
args)
      -- Act like we are completing as if the user pressed TAB at the "_"
      let cursor :: FilePath
cursor = FilePath -> Maybe FilePath -> FilePath
forall a. a -> Maybe a -> a
Maybe.fromMaybe FilePath
"_" ((FilePath -> Bool) -> [FilePath] -> Maybe FilePath
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
List.find (FilePath
"_" FilePath -> FilePath -> Bool
forall a. Eq a => [a] -> [a] -> Bool
`List.isSuffixOf`) [FilePath]
args)
      [Completions]
completions <- CompletionEnv cExt -> FilePath -> FilePath -> IO [Completions]
forall cExt.
CompletionEnv cExt -> FilePath -> FilePath -> IO [Completions]
Complete.complete CompletionEnv cExt
cEnv FilePath
line (FilePath -> FilePath
forall a. HasCallStack => [a] -> [a]
List.init FilePath
cursor)
      Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Response cExt -> IO (Response cExt))
-> Response cExt -> IO (Response cExt)
forall a b. (a -> b) -> a -> b
$
        Doc Void -> Response cExt
forall cExt. Doc Void -> Response cExt
Resp.Complete (Doc Void -> Response cExt) -> Doc Void -> Response cExt
forall a b. (a -> b) -> a -> b
$
          case [Completions]
completions of
            [] -> Doc Void
"No completions"
            [Completions]
_ -> [Doc Void] -> Doc Void
forall ann. [Doc ann] -> Doc ann
PP.vcat ((Completions -> Doc Void) -> [Completions] -> [Doc Void]
forall a b. (a -> b) -> [a] -> [b]
List.map Completions -> Doc Void
forall a ann. Pretty a => a -> Doc ann
forall ann. Completions -> Doc ann
PP.pretty [Completions]
completions)
    -- Show what sort of syntax-highlighting should be provided by the UI
    Rgx.MRight (Rgx.MThen Match (Arg cExt) l
_secret (Rgx.MThen (Rgx.MLit (Arg.ACommand Command cExt
cmd)) (Rgx.MStar [Match (Arg cExt) r1]
args0))) ->
      let args :: [Text]
args = (Match (Arg cExt) r1 -> Text) -> [Match (Arg cExt) r1] -> [Text]
forall a b. (a -> b) -> [a] -> [b]
map (\(Rgx.MLit (Arg.AText Text
t)) -> Text
t) [Match (Arg cExt) r1]
args0 in
      case CommandExt cExt -> Command cExt -> Some (RegexRepr ArgTypeRepr)
forall cExt.
CommandExt cExt -> Command cExt -> Some (RegexRepr ArgTypeRepr)
Cmd.regex CommandExt cExt
cExt Command cExt
cmd of
        Some RegexRepr ArgTypeRepr x
rx ->
          let sEnv :: StyleEnv cExt
sEnv = Context cExt p sym ext t -> ExecState p sym ext r -> 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 sym ext t
ctx ExecState p sym ext r
execState in
          Response cExt -> IO (Response cExt)
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Styled] -> Response cExt
forall cExt. [Styled] -> Response cExt
Resp.Style (StyleEnv cExt -> StyleT cExt Identity [Styled] -> [Styled]
forall cExt a. StyleEnv cExt -> StyleT cExt Identity a -> a
Style.runStyle StyleEnv cExt
sEnv (RegexRepr ArgTypeRepr x -> [Text] -> StyleT cExt Identity [Styled]
forall (m :: * -> *) (r :: Regex ArgType) cExt.
Monad m =>
RegexRepr ArgTypeRepr r -> [Text] -> StyleT cExt m [Styled]
Style.style RegexRepr ArgTypeRepr x
rx [Text]
args)))

source ::
  Context cExt p sym ext t ->
  FilePath ->
  IO (Either X.IOException (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)))
source :: 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)))
source Context cExt p sym ext t
ctx FilePath
path = do
  let cExt :: CommandExt cExt
cExt = 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
  Either IOException Text
eTxt <- IO (Either IOException Text) -> IO (Either IOException Text)
forall a. IO a -> IO a
forall (m :: * -> *) a. MonadIO m => IO a -> m a
liftIO (IO Text -> IO (Either IOException Text)
forall e a. Exception e => IO a -> IO (Either e a)
X.try (FilePath -> IO Text
IO.readFile FilePath
path))
  case Either IOException Text
eTxt of
    Left IOException
ioErr -> Either
  IOException
  (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt))
-> IO
     (Either
        IOException
        (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IOException
-> Either
     IOException
     (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt))
forall a b. a -> Either a b
Left IOException
ioErr)
    Right Text
txt -> do
      let lns :: [Text]
lns = Text -> [Text]
Text.lines Text
txt
      let cmds :: Either ParseError [Statement cExt]
cmds = (Text -> Either ParseError (Statement cExt))
-> [Text] -> Either ParseError [Statement cExt]
forall (t :: * -> *) (f :: * -> *) a b.
(Traversable t, Applicative f) =>
(a -> f b) -> t a -> f (t b)
forall (f :: * -> *) a b.
Applicative f =>
(a -> f b) -> [a] -> f [b]
traverse (CommandExt cExt -> Text -> Either ParseError (Statement cExt)
forall cExt.
CommandExt cExt -> Text -> Either ParseError (Statement cExt)
Stmt.parse CommandExt cExt
cExt) [Text]
lns
      case Either ParseError [Statement cExt]
cmds of
        Left ParseError
err -> do
          Outputs IO (Response cExt) -> Response cExt -> IO ()
forall (m :: * -> *) a. Outputs m a -> a -> m ()
Outps.send (Context cExt p sym 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 sym ext t
ctx) (UserError cExt -> Response cExt
forall cExt. UserError cExt -> Response cExt
Resp.UserError (ParseError -> UserError cExt
forall cExt. ParseError -> UserError cExt
Resp.SourceParseError ParseError
err))
          Either
  IOException
  (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt))
-> IO
     (Either
        IOException
        (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)))
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
-> Either
     IOException
     (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt))
forall a b. b -> Either a b
Right (Context cExt p sym 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 sym ext t
ctx))
        Right [Statement cExt]
stmts -> Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
-> Either
     IOException
     (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt))
forall a b. b -> Either a b
Right (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
 -> Either
      IOException
      (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)))
-> IO (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt))
-> IO
     (Either
        IOException
        (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Statement cExt]
-> Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
-> IO (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt))
forall (m :: * -> *) a.
MonadIO m =>
[a] -> Inputs m a -> IO (Inputs m a)
Inps.prepend [Statement cExt]
stmts (Context cExt p sym 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 sym ext t
ctx)

usage ::
  PP.Pretty cExt =>
  Cmd.CommandExt cExt ->
  Cmd.Command cExt ->
  PP.Doc ann
usage :: forall cExt ann.
Pretty cExt =>
CommandExt cExt -> Command cExt -> Doc ann
usage CommandExt cExt
cExt Command cExt
cmd =
  case CommandExt cExt -> Command cExt -> Some (RegexRepr ArgTypeRepr)
forall cExt.
CommandExt cExt -> Command cExt -> Some (RegexRepr ArgTypeRepr)
Cmd.regex CommandExt cExt
cExt Command cExt
cmd of
    Some RegexRepr ArgTypeRepr x
rx -> [Doc ann] -> Doc ann
forall ann. [Doc ann] -> Doc ann
PP.vcat ((Doc ann -> Doc ann) -> [Doc ann] -> [Doc ann]
forall a b. (a -> b) -> [a] -> [b]
map (Command cExt -> Doc ann
forall a ann. Pretty a => a -> Doc ann
forall ann. Command cExt -> Doc ann
PP.pretty Command cExt
cmd Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
PP.<+>) (RegexRepr ArgTypeRepr x -> [Doc ann]
forall (r :: Regex ArgType) ann.
RegexRepr ArgTypeRepr r -> [Doc ann]
Arg.usage RegexRepr ArgTypeRepr x
rx))