cli: Add --debug-cmd flag to pass commands to the debugger

grease-cli/src/Grease/Cli.hs

@@ -12,6 +12,7 @@ module Grease.Cli (
   -- * Individual option parsers
   addrOverridesParser,
   boundsOptsParser,
+  debugOptsParser,
   fsOptsParser,
   fsRootParser,
   globalsParser,
@@ -223,6 +224,21 @@ addrOverridesParser =
           <> Opt.help "address overrides, in Crucible S-expression syntax"
       )
 
+debugOptsParser :: Opt.Parser GO.DebugOpts
+debugOptsParser = Opt.parserOptionGroup "Debugger options" $ do
+  debug <- Opt.switch (Opt.long "debug" <> Opt.help "run the debugger")
+  debugCmds <-
+    Opt.many
+      ( Opt.strOption
+          ( mconcat
+              [ Opt.long "debug-cmd"
+              , Opt.metavar "CMD"
+              , Opt.help "Command to pass to the debugger"
+              ]
+          )
+      )
+  pure GO.DebugOpts{..}
+
 fsOptsParser :: Opt.Parser GO.FsOpts
 fsOptsParser = Opt.parserOptionGroup "Symbolic I/O options" $ do
   fsRoot <- fsRootParser
@@ -332,7 +348,7 @@ symStdinParser =
 simOpts :: Opt.Parser GO.SimOpts
 simOpts = do
   simProgPath <- Opt.strArgument (Opt.help "filename of binary" <> Opt.metavar "FILENAME")
-  simDebug <- Opt.switch (Opt.long "debug" <> Opt.help "run the debugger")
+  simDebugOpts <- debugOptsParser
   simEntryPoints <- Opt.many entrypointParser
   simMutGlobs <- globalsParser
   simReqs <-
@@ -447,7 +463,7 @@ processSimOpts sOpts =
         (GO.simBoundsOpts sOpts)
           { GO.simTimeout =
               -- TODO(#37): Fully disable timeout if --debug is passed
-              if GO.simDebug sOpts
+              if GO.debug (GO.simDebugOpts sOpts)
                 then secondsFromInt maxBound
                 else GO.simTimeout (GO.simBoundsOpts sOpts)
           }

grease-exe/src/Grease/Main.hs

@@ -144,6 +144,7 @@ import Grease.Macaw.SimulatorState (GreaseSimulatorState, discoveredFnHandles, e
 import Grease.Main.Diagnostic qualified as Diag
 import Grease.MustFail qualified as MustFail
 import Grease.Options
+import Grease.Options qualified as GO
 import Grease.Output
 import Grease.Panic (Grease, panic)
 import Grease.Pretty (prettyPtrFnMap)
@@ -681,7 +682,7 @@ macawExecFeats ::
 macawExecFeats la bak archCtx macawCfgConfig simOpts = do
   profFeatLog <- traverse greaseProfilerFeature (simProfileTo simOpts)
   let dbgOpts =
-        if simDebug simOpts
+        if GO.debug (GO.simDebugOpts simOpts)
           then
             let mbElf = snd . Elf.getElf <$> mcElf macawCfgConfig
                 extImpl = MDebug.macawExtImpl prettyPtrFnMap (archCtx ^. archVals) mbElf
@@ -705,12 +706,33 @@ llvmExecFeats ::
 llvmExecFeats la bak simOpts memVar = do
   profFeatLog <- traverse greaseProfilerFeature (simProfileTo simOpts)
   let dbgOpts =
-        if simDebug simOpts
+        if GO.debug (GO.simDebugOpts simOpts)
           then Just (LDebug.llvmExtImpl memVar)
           else Nothing
   feats <- greaseExecFeats la bak dbgOpts
   pure (feats, snd <$> profFeatLog)
 
+initDebugger ::
+  WI.IsExpr (WI.SymExpr sym) =>
+  PP.Pretty cExt =>
+  PP.Pretty (Dbg.ResponseExt cExt) =>
+  GreaseLogAction ->
+  GO.DebugOpts ->
+  Dbg.CommandExt cExt ->
+  C.TypeRepr t ->
+  IO (Dbg.Context cExt sym ext t)
+initDebugger la dbgOpts cExt t = do
+  inps_ <- Dbg.defaultDebuggerInputs cExt
+  stmts <-
+    forM (GO.debugCmds dbgOpts) $ \cmdTxt ->
+      case Dbg.parse cExt cmdTxt of
+        Left err -> userError la (PP.pretty (Dbg.renderParseError err))
+        Right stmt -> pure stmt
+  inps <- Dbg.prepend stmts inps_
+  let pp = (PP.<> "\n") . PP.pretty
+  let outps = Dbg.Outputs (doLog la . Diag.DebuggerOutput . pp)
+  Dbg.initCtx cExt prettyPtrFnMap inps outps t
+
 macawMemConfig ::
   ( Symbolic.SymArchConstraints arch
   , C.IsSyntaxExtension (Symbolic.MacawExt arch)
@@ -853,15 +875,10 @@ macawInitState la archCtx halloc macawCfgConfig simOpts bak memVar memPtrTable s
   -- use an empty map instead. (See gitlab#118 for more discussion on this point.)
   let discoveredHdls = Maybe.maybe Map.empty (`Map.singleton` ssaCfgHdl) mbCfgAddr
 
+  let dbgOpts = GO.simDebugOpts simOpts
   let dbgCmdExt = MDebug.macawCommandExt (archCtx ^. archVals)
-  dbgInputs <- Dbg.defaultDebuggerInputs dbgCmdExt
-  dbgCtx <-
-    Dbg.initCtx
-      dbgCmdExt
-      prettyPtrFnMap
-      dbgInputs
-      Dbg.defaultDebuggerOutputs
-      (regStructRepr archCtx)
+  dbgCtx <- initDebugger la dbgOpts dbgCmdExt (regStructRepr archCtx)
+
   let personality =
         emptyGreaseSimulatorState toConcVar dbgCtx
           & discoveredFnHandles .~ discoveredHdls
@@ -1607,15 +1624,9 @@ simulateLlvmCfg la simOpts bak fm halloc llvmCtx llvmMod initMem setupHook mbSta
     let opts = simInitPrecondOpts simOpts
      in llvmInitArgShapes la opts llvmMod argNames cfg
 
+  let dbgOpts = GO.simDebugOpts simOpts
   let dbgCmdExt = LDebug.llvmCommandExt
-  dbgInputs <- Dbg.defaultDebuggerInputs dbgCmdExt
-  dbgCtx <-
-    Dbg.initCtx
-      dbgCmdExt
-      prettyPtrFnMap
-      dbgInputs
-      Dbg.defaultDebuggerOutputs
-      (C.cfgReturnType cfg)
+  dbgCtx <- initDebugger la dbgOpts dbgCmdExt (C.cfgReturnType cfg)
 
   let ?recordLLVMAnnotation = \_ _ _ -> pure ()
   let bounds = simBoundsOpts simOpts

grease-exe/tests/ux/debug-cmd.llvm.cbl

@@ -0,0 +1,16 @@
+; Copyright (c) Galois, Inc. 2025
+
+; Test `--debug-cmd`
+
+;; flags {"--symbol", "test"}
+;; flags {"--debug"}
+;; flags {"--debug-cmd", "help"}
+;; flags {"--debug-cmd", "quit"}
+;; go(prog)
+
+(defun @test () Unit
+  (start start:
+    (return ())))
+
+;; check "help (h): Display help text"
+;; ok()

grease/src/Grease/Main/Diagnostic.hs

@@ -43,6 +43,8 @@ data Diagnostic where
     Diagnostic
   BitcodeParseWarnings ::
     Seq ParseWarning -> Diagnostic
+  DebuggerOutput ::
+    PP.Doc Void -> Diagnostic
   Exception ::
     PP.Doc Void -> Diagnostic
   LoadedPrecondition ::
@@ -97,6 +99,7 @@ instance PP.Pretty Diagnostic where
           , PP.pretty entry
           ]
       BitcodeParseWarnings warns -> PP.viaShow (ppParseWarnings warns)
+      DebuggerOutput out -> fmap absurd out
       Exception err ->
         "Exception:" PP.<+> fmap absurd err
       FinishedAnalyzingEntrypoint entry duration ->
@@ -150,6 +153,7 @@ severity =
     AnalyzedEntrypoint{} -> Info
     AnalyzingEntrypoint{} -> Info
     BitcodeParseWarnings{} -> Warn
+    DebuggerOutput{} -> Info
     Exception{} -> Error
     FinishedAnalyzingEntrypoint{} -> Debug
     LoadedPrecondition{} -> Debug

grease/src/Grease/Options.hs

@@ -18,6 +18,7 @@ module Grease.Options (
   SkipInvalidCallAddrs (..),
   SkipUnsupportedRelocs (..),
   BoundsOpts (..),
+  DebugOpts (..),
   FsOpts (..),
   InitialPreconditionOpts (..),
   SimOpts (..),
@@ -131,6 +132,16 @@ data BoundsOpts
   }
   deriving Show
 
+-- | Options related to the debugger
+data DebugOpts
+  = DebugOpts
+  { debug :: Bool
+  -- ^ Start the debugger at the beginning of simulation
+  , debugCmds :: [Text]
+  -- ^ Commands to prepend to the debugger inputs (like GDB's @-iex@)
+  }
+  deriving Show
+
 data FsOpts
   = FsOpts
   { fsRoot :: Maybe FilePath
@@ -160,7 +171,7 @@ data InitialPreconditionOpts
 -- | Options that affect simulation
 data SimOpts
   = SimOpts
-  { simDebug :: Bool
+  { simDebugOpts :: DebugOpts
   -- ^ Run the debugger execution feature
   , simEntryPoints :: [Entrypoint]
   -- ^ Names or address of function to simulate