Copyright	(c) Galois Inc. 2025
Maintainer	Langston Barrett <langston@galois.com>
Safe Haskell	Safe-Inferred
Language	Haskell2010

Lang.Crucible.Debug

Description

Synopsis

debugger :: sym ~ ExprBuilder s st fs => IsSymInterface sym => IsSyntaxExtension ext => IsExpr (SymExpr sym) => (?parserHooks :: ParserHooks ext) => Pretty cExt => CommandExt cExt -> ExtImpl cExt p sym ext t -> IntrinsicPrinters sym -> Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt) -> Outputs IO (Response cExt) -> TypeRepr t -> IO (ExecutionFeature p sym ext (RegEntry sym t))
bareDebuggerExt :: IsSyntaxExtension ext => (?parserHooks :: ParserHooks ext) => Pretty cExt => CommandExt cExt -> (forall p sym t. IsSymInterface sym => ExtImpl cExt p sym ext t) -> (forall p sym. IsSymInterface sym => ExtensionImpl p sym ext) -> Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt) -> Outputs IO (Response cExt) -> (Text -> IO ()) -> IO ()
bareDebugger :: Inputs (CompletionT Void (StyleT Void IO)) (Statement Void) -> Outputs IO (Response Void) -> (Text -> IO ()) -> IO ()
defaultDebuggerInputs :: MonadIO m => CommandExt cExt -> IO (Inputs (CompletionT cExt (StyleT cExt m)) (Statement cExt))
defaultDebuggerOutputs :: Pretty cExt => Pretty (ResponseExt cExt) => Outputs IO (Response cExt)
data Arg cExt i where
- ABreakpoint :: Breakpoint -> Arg cExt 'TBreakpoint
- ACommand :: Command cExt -> Arg cExt 'TCommand
- AExactly :: SymbolRepr s -> Arg cExt ('TExactly s)
- AFunction :: FunctionName -> Arg cExt 'TFunction
- AInt :: Int -> Arg cExt 'TInt
- APath :: Text -> Arg cExt 'TPath
- AText :: Text -> Arg cExt 'TText
data ArgTypeRepr i where
- TBreakpointRepr :: ArgTypeRepr 'TBreakpoint
- TCommandRepr :: ArgTypeRepr 'TCommand
- TExactlyRepr :: SymbolRepr s -> ArgTypeRepr ('TExactly s)
- TFunctionRepr :: ArgTypeRepr 'TFunction
- TIntRepr :: ArgTypeRepr 'TInt
- TPathRepr :: ArgTypeRepr 'TPath
- TTextRepr :: ArgTypeRepr 'TText
type Breakpoint = Lit 'TBreakpoint
type Exactly s = Lit ('TExactly s)
type Function = Lit 'TFunction
type Int = Lit 'TInt
type Path = Lit 'TPath
type Text = Lit 'TText
data Command cExt
- = Base BaseCommand
- | Ext cExt
data CommandExt cExt = CommandExt {
- extAbbrev :: cExt -> Text
- extList :: [cExt]
- extDetail :: cExt -> Maybe Text
- extHelp :: cExt -> Text
- extName :: cExt -> Text
- extRegex :: cExt -> Some (RegexRepr ArgTypeRepr)
}
voidExts :: CommandExt Void
execStateSimState :: ExecState p sym ext r -> Either NotApplicable (SomeSimState p sym ext r)
data EvalResult cExt p sym ext t = EvalResult {
- evalCtx :: Context cExt p sym ext t
- evalFeatureResult :: ExecutionFeatureResult p sym ext (RegEntry sym t)
- evalResp :: Response cExt
}
data Context cExt p sym ext t = Context {
- dbgBreakpoints :: Set Breakpoint
- dbgCommandExt :: CommandExt cExt
- dbgExtImpl :: ExtImpl cExt p sym ext t
- dbgInputs :: Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt)
- dbgOutputs :: Outputs IO (Response cExt)
- dbgPpIntrinsic :: IntrinsicPrinters sym
- dbgRetTy :: TypeRepr t
- dbgState :: DebuggerState
- dbgStopOnAbort :: Bool
- dbgTrace :: Trace ext
}
data CommandImpl cExt p sym ext t = forall r.CommandImpl {
- implRegex :: RegexRepr ArgTypeRepr r
- implBody :: Context cExt p sym ext t -> ExecState p sym ext (RegEntry sym t) -> Match (Arg cExt) r -> IO (EvalResult cExt p sym ext t)
}
newtype ExtImpl cExt p sym ext t = ExtImpl {
- getExtImpl :: cExt -> CommandImpl cExt p sym ext t
}
voidImpl :: ExtImpl Void p sym ext t
data Response cExt
- = Ok
- | UserError (UserError cExt)
- | XResponse (ResponseExt cExt)
data UserError cExt = NotApplicable NotApplicable
data NotApplicable
- = DoneSimulating
- | NotYetSimulating
type family ResponseExt cExt :: Type
data Regex a
type Empty = 'TEmpty
type Lit = 'TLit
type (:|) a b = 'TOr a b
type Then = 'TThen
type Star = 'TStar
data Match k r where
- MEmpty :: Match f 'TEmpty
- MLit :: f t -> Match f ('TLit t)
- MLeft :: Match f l -> Match f ('TOr l r)
- MRight :: Match f r -> Match f ('TOr l r)
- MThen :: Match f l -> Match f r -> Match f ('TThen l r)
- MStar :: [Match f r] -> Match f ('TStar r)
data RegexRepr f r where
- Empty :: RegexRepr f 'TEmpty
- Fail :: RegexRepr f 'TFail
- Lit :: f t -> RegexRepr f ('TLit t)
- Or :: RegexRepr f l -> RegexRepr f r -> RegexRepr f ('TOr l r)
- Star :: RegexRepr f r -> RegexRepr f ('TStar r)
- Then :: RegexRepr f l -> RegexRepr f r -> RegexRepr f ('TThen l r)
data Trace ext
data TraceEntry ext = forall blocks init ret.TraceEntry {
- traceCfg :: CFG ext blocks init ret
- traceBlock :: Some (BlockID blocks)
}
latest :: Trace ext -> Int -> IO [TraceEntry ext]
newtype IntrinsicPrinters sym = IntrinsicPrinters {
- getIntrinsicPrinters :: MapF SymbolRepr (IntrinsicPrettyFn sym)
}

Documentation

debugger :: sym ~ ExprBuilder s st fs => IsSymInterface sym => IsSyntaxExtension ext => IsExpr (SymExpr sym) => (?parserHooks :: ParserHooks ext) => Pretty cExt => CommandExt cExt -> ExtImpl cExt p sym ext t -> IntrinsicPrinters sym -> Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt) -> Outputs IO (Response cExt) -> TypeRepr t -> IO (ExecutionFeature p sym ext (RegEntry sym t)) Source #

bareDebuggerExt :: IsSyntaxExtension ext => (?parserHooks :: ParserHooks ext) => Pretty cExt => CommandExt cExt -> (forall p sym t. IsSymInterface sym => ExtImpl cExt p sym ext t) -> (forall p sym. IsSymInterface sym => ExtensionImpl p sym ext) -> Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt) -> Outputs IO (Response cExt) -> (Text -> IO ()) -> IO () Source #

Like bareDebugger, but with a syntax extension

bareDebugger :: Inputs (CompletionT Void (StyleT Void IO)) (Statement Void) -> Outputs IO (Response Void) -> (Text -> IO ()) -> IO () Source #

Start a debugger instance in an empty Crucible program.

The Crucible program simply returns the unit value. The idea is to use the Load and Call commands to actually run some Crucible CFG(s).

Proves obligations using Z3.

defaultDebuggerInputs :: MonadIO m => CommandExt cExt -> IO (Inputs (CompletionT cExt (StyleT cExt m)) (Statement cExt)) Source #

defaultDebuggerOutputs :: Pretty cExt => Pretty (ResponseExt cExt) => Outputs IO (Response cExt) Source #

data Arg cExt i where Source #

Constructors

ABreakpoint :: Breakpoint -> Arg cExt 'TBreakpoint
ACommand :: Command cExt -> Arg cExt 'TCommand
AExactly :: SymbolRepr s -> Arg cExt ('TExactly s)
AFunction :: FunctionName -> Arg cExt 'TFunction
AInt :: Int -> Arg cExt 'TInt
APath :: Text -> Arg cExt 'TPath
AText :: Text -> Arg cExt 'TText

data ArgTypeRepr i where Source #

Value-level representative of ArgType

Constructors

TBreakpointRepr :: ArgTypeRepr 'TBreakpoint
TCommandRepr :: ArgTypeRepr 'TCommand
TExactlyRepr :: SymbolRepr s -> ArgTypeRepr ('TExactly s)
TFunctionRepr :: ArgTypeRepr 'TFunction
TIntRepr :: ArgTypeRepr 'TInt
TPathRepr :: ArgTypeRepr 'TPath
TTextRepr :: ArgTypeRepr 'TText

Instances

Instances details

Show (ArgTypeRepr t) Source #
Instance details Defined in Lang.Crucible.Debug.Arg.Type Methods showsPrec :: Int -> ArgTypeRepr t -> ShowS # show :: ArgTypeRepr t -> String # showList :: [ArgTypeRepr t] -> ShowS #
Pretty (ArgTypeRepr t) Source #
Instance details Defined in Lang.Crucible.Debug.Arg.Type Methods pretty :: ArgTypeRepr t -> Doc ann # prettyList :: [ArgTypeRepr t] -> Doc ann #

type Breakpoint = Lit 'TBreakpoint Source #

type Exactly s = Lit ('TExactly s) Source #

type Function = Lit 'TFunction Source #

type Int = Lit 'TInt Source #

type Path = Lit 'TPath Source #

type Text = Lit 'TText Source #

data Command cExt Source #

Constructors

Base BaseCommand
Ext cExt

Instances

Instances details

Functor Command Source #
Instance details Defined in Lang.Crucible.Debug.Command Methods fmap :: (a -> b) -> Command a -> Command b # (<$) :: a -> Command b -> Command a #
Show cExt => Show (Command cExt) Source #
Instance details Defined in Lang.Crucible.Debug.Command Methods showsPrec :: Int -> Command cExt -> ShowS # show :: Command cExt -> String # showList :: [Command cExt] -> ShowS #
Pretty cExt => Pretty (Command cExt) Source #
Instance details Defined in Lang.Crucible.Debug.Command Methods pretty :: Command cExt -> Doc ann # prettyList :: [Command cExt] -> Doc ann #

data CommandExt cExt Source #

Constructors

CommandExt

Fields

extAbbrev :: cExt -> Text
Used in abbrev, parse
extList :: [cExt]
extDetail :: cExt -> Maybe Text
Multi-line help string. Used in detail.
This is always displayed as a new paragraph following extHelp, so it should not repeat the information there.
Should be long-form prose, with proper capitalization and punctuation. Should not rely on being shown in monospaced font.
extHelp :: cExt -> Text
Single-line help string. Used in help.
The first letter should be capitalized, it should not end in a period. It should probably be less than about 70 characters long.
extName :: cExt -> Text
Used in help, parse
extRegex :: cExt -> Some (RegexRepr ArgTypeRepr)
Used in help

voidExts :: CommandExt Void Source #

execStateSimState :: ExecState p sym ext r -> Either NotApplicable (SomeSimState p sym ext r) Source #

data EvalResult cExt p sym ext t Source #

The result of evaluating a Statement

Constructors

EvalResult
Fields evalCtx :: Context cExt p sym ext t evalFeatureResult :: ExecutionFeatureResult p sym ext (RegEntry sym t) evalResp :: Response cExt

data Context cExt p sym ext t Source #

Debugger state.

Type parameters:

cExt is the command extension type, see CommandExt
p, sym, ext are as in OverrideSim
t is the Crucible type of the RegValue returned by the program

cExt is different from ext because it's not necessarily true that you would want the debugger command extensions to be tied in a 1:1 fashion with the syntax extension (source language).

Constructors

Context
Fields dbgBreakpoints :: Set Breakpoint dbgCommandExt :: CommandExt cExt dbgExtImpl :: ExtImpl cExt p sym ext t dbgInputs :: Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt) dbgOutputs :: Outputs IO (Response cExt) dbgPpIntrinsic :: IntrinsicPrinters sym dbgRetTy :: TypeRepr t dbgState :: DebuggerState dbgStopOnAbort :: Bool dbgTrace :: Trace ext

data CommandImpl cExt p sym ext t Source #

Constructors

forall r. CommandImpl

Fields

implRegex :: RegexRepr ArgTypeRepr r
A regular expression describing what kinds of arguments this command takes. See Lang.Crucible.Debug.Regex.
implBody :: Context cExt p sym ext t -> ExecState p sym ext (RegEntry sym t) -> Match (Arg cExt) r -> IO (EvalResult cExt p sym ext t)
The implementation of the command, taking the arguments that result from matching implRegex against the command line provided by the user.

newtype ExtImpl cExt p sym ext t Source #

Constructors

ExtImpl
Fields getExtImpl :: cExt -> CommandImpl cExt p sym ext t

voidImpl :: ExtImpl Void p sym ext t Source #

data Response cExt Source #

Constructors

Ok
UserError (UserError cExt)
XResponse (ResponseExt cExt)

Instances

Instances details

(Show (ResponseExt cExt), Show cExt) => Show (Response cExt) Source #
Instance details Defined in Lang.Crucible.Debug.Response Methods showsPrec :: Int -> Response cExt -> ShowS # show :: Response cExt -> String # showList :: [Response cExt] -> ShowS #
(Pretty (ResponseExt cExt), Pretty cExt) => Pretty (Response cExt) Source #
Instance details Defined in Lang.Crucible.Debug.Response Methods pretty :: Response cExt -> Doc ann # prettyList :: [Response cExt] -> Doc ann #

data UserError cExt Source #

The command could not be completed successfully for some reason the user should have anticipated.

Constructors

NotApplicable NotApplicable

Instances

Instances details

Show cExt => Show (UserError cExt) Source #
Instance details Defined in Lang.Crucible.Debug.Response Methods showsPrec :: Int -> UserError cExt -> ShowS # show :: UserError cExt -> String # showList :: [UserError cExt] -> ShowS #
Pretty cExt => Pretty (UserError cExt) Source #
Instance details Defined in Lang.Crucible.Debug.Response Methods pretty :: UserError cExt -> Doc ann # prettyList :: [UserError cExt] -> Doc ann #

data NotApplicable Source #

The command was not applicable in this state

Constructors

DoneSimulating
NotYetSimulating

Instances

Instances details

Show NotApplicable Source #
Instance details Defined in Lang.Crucible.Debug.Response Methods showsPrec :: Int -> NotApplicable -> ShowS # show :: NotApplicable -> String # showList :: [NotApplicable] -> ShowS #
Pretty NotApplicable Source #
Instance details Defined in Lang.Crucible.Debug.Response Methods pretty :: NotApplicable -> Doc ann # prettyList :: [NotApplicable] -> Doc ann #

type family ResponseExt cExt :: Type Source #

Instances

Instances details

type ResponseExt Void Source #
Instance details Defined in Lang.Crucible.Debug.Response type ResponseExt Void = Void

data Regex a Source #

Type-level only

Instances

Instances details

FoldableFC (RegexRepr :: (k -> Type) -> Regex k -> Type) Source #
Instance details Defined in Lang.Crucible.Debug.Regex Methods foldMapFC :: forall f m. Monoid m => (forall (x :: k0). f x -> m) -> forall (x :: l). RegexRepr f x -> m # foldrFC :: (forall (x :: k0). f x -> b -> b) -> forall (x :: l). b -> RegexRepr f x -> b # foldlFC :: forall f b. (forall (x :: k0). b -> f x -> b) -> forall (x :: l). b -> RegexRepr f x -> b # foldrFC' :: (forall (x :: k0). f x -> b -> b) -> forall (x :: l). b -> RegexRepr f x -> b # foldlFC' :: forall f b. (forall (x :: k0). b -> f x -> b) -> forall (x :: l). b -> RegexRepr f x -> b # toListFC :: (forall (x :: k0). f x -> a) -> forall (x :: l). RegexRepr f x -> [a] #
FunctorFC (RegexRepr :: (k -> Type) -> Regex k -> Type) Source #
Instance details Defined in Lang.Crucible.Debug.Regex Methods fmapFC :: (forall (x :: k0). f x -> g x) -> forall (x :: l). RegexRepr f x -> RegexRepr g x #
TraversableFC (RegexRepr :: (k -> Type) -> Regex k -> Type) Source #
Instance details Defined in Lang.Crucible.Debug.Regex Methods traverseFC :: forall f g m. Applicative m => (forall (x :: k0). f x -> m (g x)) -> forall (x :: l). RegexRepr f x -> m (RegexRepr g x) #
TestEquality f => TestEquality (RegexRepr f :: Regex k -> Type) Source #
Instance details Defined in Lang.Crucible.Debug.Regex Methods testEquality :: forall (a :: k0) (b :: k0). RegexRepr f a -> RegexRepr f b -> Maybe (a :~: b) #

type Empty = 'TEmpty Source #

type Lit = 'TLit Source #

type (:|) a b = 'TOr a b Source #

type Then = 'TThen Source #

type Star = 'TStar Source #

data Match k r where Source #

The result of match, in case of success

Constructors

MEmpty :: Match f 'TEmpty
MLit :: f t -> Match f ('TLit t)
MLeft :: Match f l -> Match f ('TOr l r)
MRight :: Match f r -> Match f ('TOr l r)
MThen :: Match f l -> Match f r -> Match f ('TThen l r)
MStar :: [Match f r] -> Match f ('TStar r)

data RegexRepr f r where Source #

Value-level representative of Regex

The order of the type parameters is a bit arbitrary... This order gives KnownRepr and TestEquality instances but requires flipping the type parameters to get TraversableF.

Constructors

Empty :: RegexRepr f 'TEmpty
Fail :: RegexRepr f 'TFail
Lit :: f t -> RegexRepr f ('TLit t)
Or :: RegexRepr f l -> RegexRepr f r -> RegexRepr f ('TOr l r)
Star :: RegexRepr f r -> RegexRepr f ('TStar r)
Then :: RegexRepr f l -> RegexRepr f r -> RegexRepr f ('TThen l r)

Instances

Instances details

FoldableFC (RegexRepr :: (k -> Type) -> Regex k -> Type) Source #
Instance details Defined in Lang.Crucible.Debug.Regex Methods foldMapFC :: forall f m. Monoid m => (forall (x :: k0). f x -> m) -> forall (x :: l). RegexRepr f x -> m # foldrFC :: (forall (x :: k0). f x -> b -> b) -> forall (x :: l). b -> RegexRepr f x -> b # foldlFC :: forall f b. (forall (x :: k0). b -> f x -> b) -> forall (x :: l). b -> RegexRepr f x -> b # foldrFC' :: (forall (x :: k0). f x -> b -> b) -> forall (x :: l). b -> RegexRepr f x -> b # foldlFC' :: forall f b. (forall (x :: k0). b -> f x -> b) -> forall (x :: l). b -> RegexRepr f x -> b # toListFC :: (forall (x :: k0). f x -> a) -> forall (x :: l). RegexRepr f x -> [a] #
FunctorFC (RegexRepr :: (k -> Type) -> Regex k -> Type) Source #
Instance details Defined in Lang.Crucible.Debug.Regex Methods fmapFC :: (forall (x :: k0). f x -> g x) -> forall (x :: l). RegexRepr f x -> RegexRepr g x #
TraversableFC (RegexRepr :: (k -> Type) -> Regex k -> Type) Source #
Instance details Defined in Lang.Crucible.Debug.Regex Methods traverseFC :: forall f g m. Applicative m => (forall (x :: k0). f x -> m (g x)) -> forall (x :: l). RegexRepr f x -> m (RegexRepr g x) #
TestEquality f => TestEquality (RegexRepr f :: Regex k -> Type) Source #
Instance details Defined in Lang.Crucible.Debug.Regex Methods testEquality :: forall (a :: k0) (b :: k0). RegexRepr f a -> RegexRepr f b -> Maybe (a :~: b) #

data Trace ext Source #

data TraceEntry ext Source #

Constructors

forall blocks init ret. TraceEntry
Fields traceCfg :: CFG ext blocks init ret traceBlock :: Some (BlockID blocks)

Instances

Instances details

PrettyExt ext => Pretty (TraceEntry ext) Source #
Instance details Defined in Lang.Crucible.Debug.Trace Methods pretty :: TraceEntry ext -> Doc ann # prettyList :: [TraceEntry ext] -> Doc ann #

latest :: Trace ext -> Int -> IO [TraceEntry ext] Source #

Get up to the N latest entries

newtype IntrinsicPrinters sym Source #

Constructors

IntrinsicPrinters
Fields getIntrinsicPrinters :: MapF SymbolRepr (IntrinsicPrettyFn sym)