diff --git a/deps/crucible b/deps/crucible index 75a86581..04862768 160000 --- a/deps/crucible +++ b/deps/crucible @@ -1 +1 @@ -Subproject commit 75a86581549bf6fb2a75e239e1c9c94273205ad2 +Subproject commit 048627685fcff8e4e2ac96fdc6d3dbe998bfbbd1 diff --git a/grease-cli/src/Grease/Cli.hs b/grease-cli/src/Grease/Cli.hs index 04b55df6..d2b43d63 100644 --- a/grease-cli/src/Grease/Cli.hs +++ b/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) } diff --git a/grease-exe/src/Grease/Main.hs b/grease-exe/src/Grease/Main.hs index f576a4b2..1aae4353 100644 --- a/grease-exe/src/Grease/Main.hs +++ b/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 diff --git a/grease-exe/tests/ux/debug-cmd.llvm.cbl b/grease-exe/tests/ux/debug-cmd.llvm.cbl new file mode 100644 index 00000000..3da82138 --- /dev/null +++ b/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() diff --git a/grease/src/Grease/Main/Diagnostic.hs b/grease/src/Grease/Main/Diagnostic.hs index c46ebaeb..c03eb15a 100644 --- a/grease/src/Grease/Main/Diagnostic.hs +++ b/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 diff --git a/grease/src/Grease/Options.hs b/grease/src/Grease/Options.hs index e97b160b..ff92ae2f 100644 --- a/grease/src/Grease/Options.hs +++ b/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