diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,7 @@ +# 0.1.2 - 2025-11-09 + +- Store debugger state in the Crucible personality. + # 0.1 -- 2025-03-21 Initial release. diff --git a/crucible-debug.cabal b/crucible-debug.cabal --- a/crucible-debug.cabal +++ b/crucible-debug.cabal @@ -1,6 +1,6 @@ cabal-version: 2.4 name: crucible-debug -version: 0.1.0 +version: 0.1.2.0 author: Galois Inc. maintainer: langston@galois.com build-type: Simple @@ -31,7 +31,7 @@ -- available here: -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html - -- Since GHC 9.4 or earlier: + -- Since GHC 9.6 or earlier: ghc-options: -Wall -Werror=ambiguous-fields @@ -40,10 +40,11 @@ -Werror=deprecated-flags -Werror=deprecations -Werror=deriving-defaults + -Werror=deriving-typeable -Werror=dodgy-foreign-imports -Werror=duplicate-exports -Werror=empty-enumerations - -Werror=forall-identifier + -Werror=gadt-mono-local-binds -Werror=identities -Werror=inaccessible-code -Werror=incomplete-patterns @@ -56,30 +57,56 @@ -Werror=missing-fields -Werror=missing-home-modules -Werror=missing-methods + -Werror=missing-pattern-synonym-signatures + -Werror=missing-signatures + -Werror=name-shadowing + -Werror=noncanonical-monad-instances + -Werror=noncanonical-monoid-instances -Werror=operator-whitespace -Werror=operator-whitespace-ext-conflict + -Werror=orphans -Werror=overflowed-literals -Werror=overlapping-patterns -Werror=partial-fields -Werror=partial-type-signatures -Werror=redundant-bang-patterns + -Werror=redundant-record-wildcards -Werror=redundant-strictness-flags -Werror=simplifiable-class-constraints -Werror=star-binder -Werror=star-is-type -Werror=tabs + -Werror=type-defaults -Werror=typed-holes -Werror=type-equality-out-of-scope -Werror=type-equality-requires-operators + -Werror=unicode-bidirectional-format-characters -Werror=unrecognised-pragmas -Werror=unrecognised-warning-flags -Werror=unsupported-calling-conventions -Werror=unsupported-llvm-version - -Werror=unticked-promoted-constructors + -Werror=unused-do-bind -Werror=unused-imports + -Werror=unused-record-wildcards -Werror=warnings-deprecations -Werror=wrong-do-bind + if impl(ghc < 9.8) + ghc-options: + -Werror=forall-identifier + + if impl(ghc >= 9.8) + ghc-options: + -Werror=incomplete-export-warnings + -Werror=inconsistent-flags + + if impl(ghc >= 9.10) + ghc-options: + -Werror=badly-staged-types + -Werror=data-kinds-tc + -Werror=deprecated-type-abstractions + -Werror=incomplete-record-selectors + ghc-prof-options: -O2 -fprof-auto-top default-language: Haskell2010 @@ -87,11 +114,12 @@ import: shared build-depends: - base >= 4.13 && < 4.20, + base >= 4.13 && < 4.21, containers, crucible, crucible-syntax, directory, + extra, filepath, isocline, lens, @@ -122,6 +150,8 @@ Lang.Crucible.Debug.Complete Lang.Crucible.Debug.Context Lang.Crucible.Debug.Eval + Lang.Crucible.Debug.Override + Lang.Crucible.Debug.Personality Lang.Crucible.Debug.Regex Lang.Crucible.Debug.Response Lang.Crucible.Debug.Statement @@ -142,7 +172,7 @@ tasty, tasty-golden, text, - + executable crucible-debug import: shared hs-source-dirs: app diff --git a/src/Lang/Crucible/Debug.hs b/src/Lang/Crucible/Debug.hs --- a/src/Lang/Crucible/Debug.hs +++ b/src/Lang/Crucible/Debug.hs @@ -17,7 +17,11 @@ ( debugger , bareDebuggerExt , bareDebugger + , Inps.Inputs(..) , Inps.defaultDebuggerInputs + , Inps.prepend + , Outps.prettyOut + , Outps.Outputs(..) , Outps.defaultDebuggerOutputs , Arg.Arg(..) , AType.ArgTypeRepr(..) @@ -36,6 +40,7 @@ , Ctxt.CommandImpl(..) , Ctxt.ExtImpl(..) , Ctxt.voidImpl + , Ctxt.DebuggerState(..) , Resp.Response(Ok, UserError, XResponse) , Resp.UserError(NotApplicable) , Resp.NotApplicable(DoneSimulating, NotYetSimulating) @@ -48,16 +53,26 @@ , type Rgx.Star , Rgx.Match(..) , Rgx.RegexRepr(..) + , Stmt.ParseError + , Stmt.parse + , Stmt.renderParseError , Trace.Trace , Trace.TraceEntry(..) , Trace.latest , IntrinsicPrinters(..) + , Ctxt.initCtx + , Pers.HasContext(..) + , Ov.debuggerPrepend + , Ov.debuggerQuit + , Ov.debuggerStop + , Ov.debugOverride + , Ov.debugRunOverride ) where import Control.Applicative qualified as Applicative import Control.Lens qualified as Lens import Control.Monad qualified as Monad -import Data.IORef qualified as IORef +import Data.Function ((&)) import Data.Maybe qualified as Maybe import Data.Parameterized.Map qualified as MapF import Data.Parameterized.Nonce qualified as Nonce @@ -83,10 +98,13 @@ import Lang.Crucible.Debug.Inputs qualified as Inps import Lang.Crucible.Debug.Outputs (Outputs) import Lang.Crucible.Debug.Outputs qualified as Outps +import Lang.Crucible.Debug.Override qualified as Ov +import Lang.Crucible.Debug.Personality qualified as Pers 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 (Statement) +import Lang.Crucible.Debug.Statement qualified as Stmt import Lang.Crucible.Debug.Style qualified as Style import Lang.Crucible.Debug.Style (StyleT) import Lang.Crucible.Debug.Trace qualified as Trace @@ -99,6 +117,7 @@ import Lang.Crucible.Syntax.Concrete qualified as C import Lang.Crucible.Types qualified as C import Prettyprinter qualified as PP +import Prettyprinter.Render.Text qualified as PP import System.Exit qualified as Exit import System.IO (stdout) import What4.Expr qualified as W4 @@ -122,7 +141,7 @@ C.UnwindCallState {} -> "UnwindCallState" stepState :: - Context cExt p sym ext t -> + Context cExt sym ext t -> C.ExecState p sym ext rtp -> IO DebuggerState stepState ctx = @@ -197,16 +216,17 @@ (?parserHooks :: C.ParserHooks ext) => PP.Pretty cExt => W4.IsExpr (W4.SymExpr sym) => - Context cExt p sym ext t -> + Context cExt sym ext t -> + Ctxt.ExtImpl cExt p sym ext t -> C.ExecState p sym ext (C.RegEntry sym t) -> IO (EvalResult cExt p sym ext t) -stopped ctx0 execState0 = go ctx0 execState0 C.ExecutionFeatureNoChange +stopped ctx0 ext execState0 = go ctx0 execState0 C.ExecutionFeatureNoChange where go c0 s0 r = do let cEnv = Ctxt.toCompletionEnv c0 s0 let sEnv = Ctxt.toStyleEnv c0 s0 stmt <- Style.runStyleM sEnv (Complete.runCompletionM cEnv (Inps.recv (Ctxt.dbgInputs c0))) - result0 <- Eval.eval c0 s0 stmt + result0 <- Eval.eval c0 ext s0 stmt let featResult = mergeResults r (Eval.evalFeatureResult result0) let result = result0 { Eval.evalFeatureResult = featResult } let s = Maybe.fromMaybe s0 (resultState featResult) @@ -224,19 +244,20 @@ W4.IsExpr (W4.SymExpr sym) => (?parserHooks :: C.ParserHooks ext) => PP.Pretty cExt => - Context cExt p sym ext t -> + Context cExt sym ext t -> + Ctxt.ExtImpl cExt p sym ext t -> C.ExecState p sym ext (C.RegEntry sym t) -> - IO (Context cExt p sym ext t, C.ExecutionFeatureResult p sym ext (C.RegEntry sym t)) -dispatch ctx0 execState = + IO (Context cExt sym ext t, C.ExecutionFeatureResult p sym ext (C.RegEntry sym t)) +dispatch ctx0 ext execState = case Ctxt.dbgState ctx0 of Ctxt.Quit -> pure (ctx0, C.ExecutionFeatureNoChange) Ctxt.Running {} | C.ResultState {} <- execState -> do let ctx = ctx0 { Ctxt.dbgState = Ctxt.Stopped } - dispatch ctx execState + dispatch ctx ext execState Ctxt.Running (Ctxt.Step i) | i <= 1 -> do let ctx = ctx0 { Ctxt.dbgState = Ctxt.Stopped } - dispatch ctx execState + dispatch ctx ext execState Ctxt.Running (Ctxt.Step i) -> do let ctx = ctx0 { Ctxt.dbgState = Ctxt.Running (Ctxt.Step (i - 1)) } state <- stepState ctx execState @@ -247,31 +268,43 @@ let ctx = ctx0 { Ctxt.dbgState = state } pure (ctx, C.ExecutionFeatureNoChange) Ctxt.Stopped -> do - result <- stopped ctx0 execState + result <- stopped ctx0 ext execState pure (Eval.evalCtx result, Eval.evalFeatureResult result) debugger :: + Pers.HasContext p cExt sym ext t => (sym ~ W4.ExprBuilder s st fs) => C.IsSymInterface sym => C.IsSyntaxExtension ext => W4.IsExpr (W4.SymExpr sym) => (?parserHooks :: C.ParserHooks ext) => PP.Pretty cExt => - Cmd.CommandExt cExt -> Ctxt.ExtImpl cExt p sym ext t -> - IntrinsicPrinters sym -> - Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt) -> - Outputs IO (Response cExt) -> - C.TypeRepr t -> - IO (C.ExecutionFeature p sym ext (C.RegEntry sym t)) -debugger cExt impl iFns ins outs rTy = do - ctxRef <- IORef.newIORef =<< Ctxt.initCtx cExt impl iFns ins outs rTy - pure $ - C.ExecutionFeature $ \execState -> do - ctx0 <- IORef.readIORef ctxRef - (ctx, featResult) <- dispatch ctx0 execState - IORef.writeIORef ctxRef ctx - pure featResult + C.ExecutionFeature p sym ext (C.RegEntry sym t) +debugger ext = + C.ExecutionFeature $ \execState -> do + let simCtx = execState Lens.^. Lens.to C.execStateContext + let ctx0 = simCtx Lens.^. C.cruciblePersonality . Pers.context + (ctx, featResult) <- dispatch ctx0 ext execState + let simCtx' = + case featResult of + C.ExecutionFeatureNoChange -> simCtx + C.ExecutionFeatureModifiedState execState' -> + C.execStateContext execState' + C.ExecutionFeatureNewState execState' -> + C.execStateContext execState' + let simCtx'' = simCtx' & C.cruciblePersonality . Pers.context Lens..~ ctx + pure $ + case featResult of + C.ExecutionFeatureNoChange -> + C.ExecutionFeatureModifiedState + (C.setExecStateContext simCtx'' execState) + C.ExecutionFeatureModifiedState execState' -> + C.ExecutionFeatureModifiedState + (C.setExecStateContext simCtx'' execState') + C.ExecutionFeatureNewState execState' -> + C.ExecutionFeatureNewState + (C.setExecStateContext simCtx'' execState') -- | Like 'bareDebugger', but with a syntax extension bareDebuggerExt :: @@ -292,17 +325,21 @@ bak <- C.newSimpleBackend sym let retType = C.UnitRepr let fns = C.FnBindings C.emptyHandleMap - let simCtx = C.initSimContext bak C.emptyIntrinsicTypes ha stdout fns extImpl () + initCtx <- do + let iFns = IntrinsicPrinters MapF.empty + Ctxt.initCtx cExts iFns inps outps retType + let simCtx = C.initSimContext bak C.emptyIntrinsicTypes ha stdout fns extImpl initCtx let ov = C.runOverrideSim retType $ return () let simSt = C.InitialState simCtx C.emptyGlobals C.defaultAbortHandler retType ov - dbgr <- do - let iFns = IntrinsicPrinters MapF.empty - debugger cExts cEval iFns inps outps retType - Monad.void $ C.executeCrucible [dbgr] simSt + Monad.void $ C.executeCrucible [debugger cEval] simSt C.getProofObligations bak >>= \case Nothing -> pure () - Just {} -> do + Just obls -> do logger "There were unhandled proof obligations! Try `prove` and `clear`." + let goals = C.goalsToList obls + prettyGoals <- mapM (C.ppProofObligation sym) goals + let render = PP.renderStrict . PP.layoutSmart PP.defaultLayoutOptions + logger (render (PP.vcat prettyGoals)) Exit.exitFailure -- | Start a debugger instance in an empty Crucible program. diff --git a/src/Lang/Crucible/Debug/Command/Base.hs b/src/Lang/Crucible/Debug/Command/Base.hs --- a/src/Lang/Crucible/Debug/Command/Base.hs +++ b/src/Lang/Crucible/Debug/Command/Base.hs @@ -18,6 +18,7 @@ , help , regex -- * Regular expressions + , rBackend , rBacktrace , rBlock , rBreak @@ -55,7 +56,8 @@ import Prettyprinter qualified as PP data BaseCommand - = Backtrace + = Backend + | Backtrace | Block | Break | Call @@ -88,6 +90,7 @@ name :: BaseCommand -> Text name = \case + Backend -> "backend" Backtrace -> "backtrace" Block -> "block" Break -> "break" @@ -117,6 +120,7 @@ abbrev :: BaseCommand -> Text abbrev = \case + Backend -> "bak" Backtrace -> "bt" Block -> "blk" Break -> "b" @@ -147,6 +151,7 @@ detail :: BaseCommand -> Maybe Text detail = \case + Backend -> Nothing Backtrace -> Nothing Block -> Nothing Break -> Nothing @@ -195,6 +200,7 @@ help :: BaseCommand -> Text help = \case + Backend -> "Print the state of the symbolic backend" Backtrace -> "Print the backtrace (AKA stack trace)" Block -> "Print the statements in the current block" Break -> "Set a breakpoint at the entry to a function" @@ -224,6 +230,7 @@ regex :: BaseCommand -> Some (Rgx.RegexRepr ArgTypeRepr) regex = \case + Backend -> Some rBackend Backtrace -> Some rBacktrace Block -> Some rBlock Break -> Some rBreak @@ -249,6 +256,9 @@ Source -> Some rSource Trace -> Some rTrace Usage -> Some rUsage + +rBackend :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty +rBackend = knownRepr rBacktrace :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty rBacktrace = knownRepr diff --git a/src/Lang/Crucible/Debug/Commands.hs b/src/Lang/Crucible/Debug/Commands.hs --- a/src/Lang/Crucible/Debug/Commands.hs +++ b/src/Lang/Crucible/Debug/Commands.hs @@ -177,7 +177,7 @@ block :: C.IsSyntaxExtension ext => W4.IsExpr (W4.SymExpr sym) => - Context cExt p sym ext t -> + Context cExt sym ext t -> C.ExecState p sym ext r -> IO (Response cExt) block _ctx execState = @@ -271,7 +271,7 @@ frame :: C.IsSyntaxExtension ext => W4.IsExpr (W4.SymExpr sym) => - Context cExt p sym ext t -> + Context cExt sym ext t -> C.ExecState p sym ext r -> IO (Response cExt) frame _ctx execState = @@ -384,7 +384,7 @@ reg :: forall p sym ext r t cExt. W4.IsExpr (W4.SymExpr sym) => - Context cExt p sym ext t -> + Context cExt sym ext t -> C.ExecState p sym ext r -> [Int] -> IO (Response cExt) @@ -425,7 +425,7 @@ secret :: PP.Pretty cExt => - Context cExt p sym ext t -> + Context cExt sym ext t -> C.ExecState p sym ext r -> Rgx.Match (Arg.Arg cExt) BCmd.SecretRegex -> IO (Resp.Response cExt) @@ -454,7 +454,7 @@ pure (Resp.Style (Style.runStyle sEnv (Style.style rx args))) source :: - Context cExt p sym ext t -> + Context cExt sym ext t -> FilePath -> IO (Either X.IOException (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt))) source ctx path = do diff --git a/src/Lang/Crucible/Debug/Context.hs b/src/Lang/Crucible/Debug/Context.hs --- a/src/Lang/Crucible/Debug/Context.hs +++ b/src/Lang/Crucible/Debug/Context.hs @@ -75,7 +75,7 @@ -- from matching 'implRegex' against the command line provided by the -- user. , implBody :: - Context cExt p sym ext t -> + Context cExt sym ext t -> C.ExecState p sym ext (C.RegEntry sym t) -> Rgx.Match (Arg.Arg cExt) r -> IO (EvalResult cExt p sym ext t) @@ -90,7 +90,7 @@ -- | The result of evaluating a 'Statement' data EvalResult cExt p sym ext t = EvalResult - { evalCtx :: Context cExt p sym ext t + { evalCtx :: Context cExt sym ext t , evalFeatureResult :: C.ExecutionFeatureResult p sym ext (C.RegEntry sym t) , evalResp :: Response cExt } @@ -106,11 +106,10 @@ -- '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). -data Context cExt p sym ext t +data Context cExt 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 @@ -123,19 +122,17 @@ initCtx :: W4.IsExpr (W4.SymExpr sym) => 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 (Context cExt p sym ext t) -initCtx cExts impl iFns ins outs rTy = do + IO (Context cExt sym ext t) +initCtx cExts iFns ins outs rTy = do t <- Trace.empty (knownNat @512) -- arbitrary max size pure $ Context { dbgBreakpoints = Set.empty , dbgCommandExt = cExts - , dbgExtImpl = impl , dbgInputs = ins , dbgOutputs = outs , dbgPpIntrinsic = iFns @@ -145,8 +142,9 @@ , dbgTrace = t } + toCompletionEnv :: - Context cExt p sym ext t -> + Context cExt sym ext t -> C.ExecState p sym ext r -> CompletionEnv cExt toCompletionEnv ctxt execState = @@ -157,7 +155,7 @@ } toStyleEnv :: - Context cExt p sym ext t -> + Context cExt sym ext t -> C.ExecState p sym ext r -> StyleEnv cExt toStyleEnv ctxt execState = @@ -166,3 +164,4 @@ , Style.envCommandExt = dbgCommandExt ctxt , Style.envState = execState } + diff --git a/src/Lang/Crucible/Debug/Eval.hs b/src/Lang/Crucible/Debug/Eval.hs --- a/src/Lang/Crucible/Debug/Eval.hs +++ b/src/Lang/Crucible/Debug/Eval.hs @@ -42,7 +42,7 @@ import What4.Interface qualified as W4 runCmd :: - Context cExt p sym ext t -> + Context cExt sym ext t -> C.ExecState p sym ext (C.RegEntry sym t) -> Ctxt.RunningState -> IO (Ctxt.EvalResult cExt p sym ext t) @@ -54,7 +54,7 @@ _ -> pure (def ctx) { Ctxt.evalCtx = ctx { Ctxt.dbgState = Ctxt.Running runState } } -- | Helper, not exported -def :: Context cExt p sym ext t -> Ctxt.EvalResult cExt p sym ext t +def :: Context cExt sym ext t -> Ctxt.EvalResult cExt p sym ext t def ctx = Ctxt.EvalResult ctx C.ExecutionFeatureNoChange Resp.Ok baseImpl :: @@ -68,6 +68,18 @@ Ctxt.CommandImpl cExt p sym ext t baseImpl = \case + BCmd.Backend -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rBackend + , Ctxt.implBody = \ctx execState Rgx.MEmpty -> do + let stateCtx = C.execStateContext execState + C.withBackend stateCtx $ \bak -> do + let sym = C.backendGetSym bak + state <- C.getBackendState bak + let resp = C.ppAssumptionState (Just sym) state + pure (def ctx) { Ctxt.evalResp = Resp.Backend resp } + } + BCmd.Backtrace -> Ctxt.CommandImpl { Ctxt.implRegex = BCmd.rBacktrace @@ -306,13 +318,13 @@ (?parserHooks :: C.ParserHooks ext) => PP.Pretty cExt => W4.IsExpr (W4.SymExpr sym) => - Context cExt p sym ext t -> + Ctxt.ExtImpl cExt p sym ext t -> Cmd.Command cExt -> Ctxt.CommandImpl cExt p sym ext t -cmdImpl ctx cmd = +cmdImpl ext cmd = case cmd of Cmd.Base bCmd -> baseImpl bCmd - Cmd.Ext xCmd -> Ctxt.getExtImpl (Ctxt.dbgExtImpl ctx) xCmd + Cmd.Ext xCmd -> Ctxt.getExtImpl ext xCmd eval :: (sym ~ W4.ExprBuilder s st fs) => @@ -321,14 +333,15 @@ (?parserHooks :: C.ParserHooks ext) => PP.Pretty cExt => W4.IsExpr (W4.SymExpr sym) => - Context cExt p sym ext t -> + Context cExt sym ext t -> + Ctxt.ExtImpl cExt p sym ext t -> C.ExecState p sym ext (C.RegEntry sym t) -> Statement cExt -> IO (Ctxt.EvalResult cExt p sym ext t) -eval ctx execState stmt = +eval ctx ext execState stmt = let args = Stmt.stmtArgs stmt in let argError err = (def ctx) { Ctxt.evalResp = Resp.UserError (Resp.ArgError (Stmt.stmtCmd stmt) err) } in - case cmdImpl ctx (Stmt.stmtCmd stmt) of + case cmdImpl ext (Stmt.stmtCmd stmt) of Ctxt.CommandImpl { Ctxt.implRegex = r, Ctxt.implBody = f } -> case Arg.match (Arg.convert (Ctxt.dbgCommandExt ctx) r) args of Left e -> pure (argError e) diff --git a/src/Lang/Crucible/Debug/Inputs.hs b/src/Lang/Crucible/Debug/Inputs.hs --- a/src/Lang/Crucible/Debug/Inputs.hs +++ b/src/Lang/Crucible/Debug/Inputs.hs @@ -11,8 +11,7 @@ {-# LANGUAGE TypeApplications #-} module Lang.Crucible.Debug.Inputs - ( Inputs - , recv + ( Inputs(..) , fail , parseInputs , parseInputsWithRetry @@ -21,6 +20,7 @@ , defaultDebuggerInputs ) where +import Control.Concurrent.Extra (once) import Control.Monad.IO.Class (MonadIO, liftIO) import Control.Monad qualified as Monad import Control.Monad.Reader qualified as Reader @@ -157,9 +157,15 @@ CommandExt cExt -> IO (Inputs (CompletionT cExt (StyleT cExt m)) (Statement cExt)) defaultDebuggerInputs cExts = do - initIsocline + -- NB: We delay initializing Isocline until the first input is requested, and + -- then use 'once' to ensure that initialization occurs at most once. The + -- benefit of doing it like this is that we ensure that a .crucible-debug + -- file won't be created unless a Crux user specifically requests the + -- debugger. + initialize <- once initIsocline pure $ parseInputsWithRetry cExts - (Text.pack <$> lift readIsocline) + (do liftIO initialize + Text.pack <$> lift readIsocline) (contramap renderParseError (Outs.lift (lift . liftIO) (Outs.hPutStrLn stdout))) diff --git a/src/Lang/Crucible/Debug/Outputs.hs b/src/Lang/Crucible/Debug/Outputs.hs --- a/src/Lang/Crucible/Debug/Outputs.hs +++ b/src/Lang/Crucible/Debug/Outputs.hs @@ -8,12 +8,11 @@ {-# LANGUAGE OverloadedStrings #-} module Lang.Crucible.Debug.Outputs - ( Outputs - , send + ( Outputs(..) , lift , accumulate , hPutStrLn - , pretty + , prettyOut , defaultDebuggerOutputs ) where @@ -41,16 +40,16 @@ hPutStrLn :: Handle -> Outputs IO Text hPutStrLn hOut = Outputs (IO.hPutStrLn hOut) -pretty :: +prettyOut :: PP.Pretty a => Handle -> PP.LayoutOptions -> Outputs IO a -pretty hOut opts = +prettyOut hOut opts = Outputs (PP.renderIO hOut . PP.layoutPretty opts . (PP.<> "\n") . PP.pretty) defaultDebuggerOutputs :: PP.Pretty cExt => PP.Pretty (ResponseExt cExt) => Outputs IO (Response cExt) -defaultDebuggerOutputs = pretty stdout PP.defaultLayoutOptions +defaultDebuggerOutputs = prettyOut stdout PP.defaultLayoutOptions diff --git a/src/Lang/Crucible/Debug/Override.hs b/src/Lang/Crucible/Debug/Override.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug/Override.hs @@ -0,0 +1,90 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} + +module Lang.Crucible.Debug.Override + ( debuggerPrepend + , debuggerQuit + , debuggerStop + , debugOverride + , debugRunOverride + ) where + +import Control.Lens qualified as Lens +import Control.Monad.IO.Class (liftIO) +import Data.Text qualified as Text +import Data.Parameterized.Context qualified as Ctx +import Lang.Crucible.Debug.Command qualified as Cmd +import Lang.Crucible.Debug.Personality qualified as Pers +import Lang.Crucible.Debug.Personality (HasContext) +import Lang.Crucible.Debug.Statement (Statement) +import Lang.Crucible.Debug.Statement qualified as Stmt +import Lang.Crucible.Backend qualified as CB +import Lang.Crucible.Simulator.ExecutionTree qualified as C +import Lang.Crucible.Simulator.OverrideSim qualified as C +import Lang.Crucible.Simulator.RegValue qualified as C +import Lang.Crucible.Types qualified as CT +import What4.Interface qualified as WI + +debuggerPrepend :: + HasContext p cExt sym ext t => + [Statement cExt] -> + C.OverrideSim p sym ext rtp args ret () +debuggerPrepend stmts = do + simCtx <- Lens.use C.stateContext + simCtx' <- liftIO (Pers.prepend stmts simCtx) + C.stateContext Lens..= simCtx' + +debuggerQuit :: + HasContext p cExt sym ext t => + C.OverrideSim p sym ext rtp args ret () +debuggerQuit = C.stateContext Lens.%= Pers.quit +{-# INLINEABLE debuggerQuit #-} + +debuggerStop :: + HasContext p cExt sym ext t => + C.OverrideSim p sym ext rtp args ret () +debuggerStop = C.stateContext Lens.%= Pers.stop +{-# INLINEABLE debuggerStop #-} + +-- | An override that stops the debugger at this location +debugOverride :: + HasContext p cExt sym ext t => + C.TypedOverride p sym ext Ctx.EmptyCtx CT.UnitType +debugOverride = + C.TypedOverride + { C.typedOverrideArgs = CT.knownRepr + , C.typedOverrideRet = CT.knownRepr + , C.typedOverrideHandler = \_args -> debuggerStop + } + +-- | An override that adds a command to the debugger +debugRunOverride :: + WI.IsExpr (WI.SymExpr sym) => + WI.IsExprBuilder sym => + HasContext p cExt sym ext t => + Cmd.CommandExt cExt -> + C.TypedOverride p sym ext (Ctx.EmptyCtx Ctx.::> CT.StringType CT.Unicode) CT.UnitType +debugRunOverride extImpl = + C.TypedOverride + { C.typedOverrideArgs = CT.knownRepr + , C.typedOverrideRet = CT.knownRepr + , C.typedOverrideHandler = + \(Ctx.viewAssign -> Ctx.AssignExtend _ (C.RV s)) -> do + sym <- C.getSymInterface + case WI.asString s of + Nothing -> + CB.throwUnsupported sym "Must pass concrete string to @debug-run" + Just (WI.UnicodeLiteral txt) -> do + case Stmt.parse extImpl txt of + Left err -> + CB.throwUnsupported sym (Text.unpack (Stmt.renderParseError err)) + Right stmt -> debuggerPrepend [stmt] + } diff --git a/src/Lang/Crucible/Debug/Personality.hs b/src/Lang/Crucible/Debug/Personality.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug/Personality.hs @@ -0,0 +1,73 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE FunctionalDependencies #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE MultiParamTypeClasses #-} + +module Lang.Crucible.Debug.Personality + ( HasContext(..) + , prepend + , quit + , stop + ) where + +import Control.Lens qualified as Lens +import Data.Function ((&)) +import Lang.Crucible.Debug.Context (Context) +import Lang.Crucible.Debug.Context qualified as Ctxt +import Lang.Crucible.Debug.Inputs qualified as Inps +import Lang.Crucible.Debug.Statement (Statement) +import Lang.Crucible.Simulator.ExecutionTree qualified as C + +-- | A class for Crucible personality types @p@ (see +-- 'Lang.Crucible.Simulator.ExecutionTree.cruciblePersonality') which contain a +-- 'Context'. This execution feature is polymorphic over the personality so that +-- downstream users can supply their own personality types that extend 'Context' +-- further. +class HasContext p cExt sym ext t | p -> cExt sym ext t where + context :: Lens.Lens' p (Context cExt sym ext t) + +instance HasContext (Context cExt sym ext t) cExt sym ext t where + context = id + {-# INLINE context #-} + +-- | 'Inps.prepend' some 'Statements' to the debugger inputs +prepend :: + HasContext p cExt sym ext t => + [Statement cExt] -> + C.SimContext p sym ext -> + IO (C.SimContext p sym ext) +prepend stmts simCtx = do + let inps = + simCtx Lens.^. C.cruciblePersonality . context . Lens.to Ctxt.dbgInputs + inps' <- Inps.prepend stmts inps + pure $ + simCtx & + C.cruciblePersonality . context Lens.%~ + \c -> c { Ctxt.dbgInputs = inps' } + +-- | Cause the debugger to transition to the 'Ctxt.Quit' state. +quit :: + HasContext p cExt sym ext t => + C.SimContext p sym ext -> + C.SimContext p sym ext +quit simCtx = + simCtx & + C.cruciblePersonality . context Lens.%~ + \c -> c { Ctxt.dbgState = Ctxt.Quit } + +-- | Cause the debugger to transition to the 'Ctxt.Stopped' state. +-- +-- This can be used to reactive the debugger after it has been quit. +stop :: + HasContext p cExt sym ext t => + C.SimContext p sym ext -> + C.SimContext p sym ext +stop simCtx = + simCtx & + C.cruciblePersonality . context Lens.%~ + \c -> c { Ctxt.dbgState = Ctxt.Stopped } diff --git a/src/Lang/Crucible/Debug/Response.hs b/src/Lang/Crucible/Debug/Response.hs --- a/src/Lang/Crucible/Debug/Response.hs +++ b/src/Lang/Crucible/Debug/Response.hs @@ -127,6 +127,7 @@ data Response cExt = Arg (PP.Doc Void) + | Backend (PP.Doc Void) | Backtrace (PP.Doc Void) | Block (PP.Doc Void) | Cfg (PP.Doc Void) @@ -155,6 +156,7 @@ pretty = \case Arg a -> fmap absurd a + Backend b -> fmap absurd b Backtrace bt -> fmap absurd bt Block b -> fmap absurd b Cfg c -> fmap absurd c diff --git a/src/Lang/Crucible/Debug/Style.hs b/src/Lang/Crucible/Debug/Style.hs --- a/src/Lang/Crucible/Debug/Style.hs +++ b/src/Lang/Crucible/Debug/Style.hs @@ -28,7 +28,7 @@ import Control.Monad.Reader (MonadReader, ReaderT) import Control.Monad.Reader qualified as Reader import Control.Monad.Trans (MonadTrans) -import Data.Foldable (foldl', toList) +import Data.Foldable qualified as Foldable import Data.Functor.Identity (Identity, runIdentity) import Data.List qualified as List import Data.Parameterized.Some (Some(Some), viewSome) @@ -183,8 +183,8 @@ pure (s : ss) Rgx.DerivativeResult (Some r') (Some m Seq.:<| ms) -> do s <- styled m - ss <- mapM (viewSome styled) (toList ms) - let combined = foldl' combineStyled s ss + ss <- mapM (viewSome styled) (Foldable.toList ms) + let combined = Foldable.foldl' combineStyled s ss rest <- style r' ws pure (combined : rest) where diff --git a/src/Lang/Crucible/Pretty.hs b/src/Lang/Crucible/Pretty.hs --- a/src/Lang/Crucible/Pretty.hs +++ b/src/Lang/Crucible/Pretty.hs @@ -3,6 +3,7 @@ Maintainer : Langston Barrett -} +{-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-} @@ -32,6 +33,7 @@ -- what4 import qualified What4.Interface as W4 +import qualified What4.Partial as W4 -- crucible import qualified Lang.Crucible.FunctionHandle as C @@ -102,6 +104,13 @@ -- More complex cases C.FunctionHandleRepr args ret -> ppFnVal args ret v + C.MaybeRepr tpr -> case v of + W4.Unassigned -> "Nothing" + W4.PE cond v' -> + let base = "Just" PP.<+> ppRegVal iFns tpr (C.RV v') in + case W4.asConstantPred cond of + Just True -> base + _ -> base PP.<+> "if" PP.<+> W4.printSymExpr cond _ -> "" ppFnVal :: diff --git a/test-data/backend.txt b/test-data/backend.txt new file mode 100644 --- /dev/null +++ b/test-data/backend.txt @@ -0,0 +1,101 @@ +> backend + +Top-level goals: +[] + + +> load test-data/backend.cbl + +Loaded 1 CFGs from test-data/backend.cbl + +> step + +Ok + +> b main + +Ok + +> call main + +Ok + +> step 2 + +Ok + +> finish + +Ok + +> backend + +Top-level goals: +[ Labeled predicate: + cgoal0@0:b + test-data/backend.cbl:4:5: error: in main + assertion #0 ] +Assumptions: + in main test-data/backend.cbl:6:5: assumption #0 + casmp0@1:b + Prove all: + [ Labeled predicate: + cgoal1@2:b + test-data/backend.cbl:8:5: error: in main + assertion #1 + , Assuming: + [ The branch in main from test-data/backend.cbl:10:5 to test-data/backend.cbl:12:16 + cb0@3:b + , in main test-data/backend.cbl:13:5: assumption #1: if branch + casmp1@5:b ] + Prove: + Labeled predicate: + cgoal2@6:b + test-data/backend.cbl:15:5: error: in main + assertion #2: if branch + , Assuming: + [ The branch in main from test-data/backend.cbl:10:5 to test-data/backend.cbl:18:16 + not cb0@3:b + , in main test-data/backend.cbl:19:5: assumption #2: else branch + casmp2@9:b + , in main test-data/backend.cbl:21:5: assumption #3: else branch + casmp3@10:b ] + Prove: + Prove both: + Labeled predicate: + cgoal3@11:b + test-data/backend.cbl:23:5: error: in main + assertion #3: else branch + Labeled predicate: + cgoal4@12:b + test-data/backend.cbl:25:5: error: in main + assertion #4: else branch ] + Assumptions: + [ if not cb0@3:b + then [ The branch in main from test-data/backend.cbl:10:5 to test-data/backend.cbl:18:16 + not cb0@3:b + , in main test-data/backend.cbl:19:5: assumption #2: else branch + casmp2@9:b + , in main test-data/backend.cbl:21:5: assumption #3: else branch + casmp3@10:b ] + else [ The branch in main from test-data/backend.cbl:10:5 to test-data/backend.cbl:12:16 + cb0@3:b + , in main test-data/backend.cbl:13:5: assumption #1: if branch + casmp1@5:b ] + , in main test-data/backend.cbl:29:5: assumption #4: end + casmp4@13:b ] + Prove all: + [ Labeled predicate: + cgoal5@14:b + test-data/backend.cbl:31:5: error: in main + assertion #5: end ] + + +> clear + +Cleared 1 proof obligation + +> done + +Ok + diff --git a/test-data/error/load-parse-error.txt b/test-data/error/load-parse-error.txt --- a/test-data/error/load-parse-error.txt +++ b/test-data/error/load-parse-error.txt @@ -1,10 +1,10 @@ > load LICENSE -LICENSE:1:30: +LICENSE:4:50: | -1 | Copyright (c) 2025 Galois Inc. - | ^ -unexpected '.' +4 | Redistribution and use in source and binary forms, with or without + | ^ +unexpected ',' expecting '"', '#', '$', '(', '+', '-', '0', '@', decimal digit, or end of input diff --git a/test-data/help.txt b/test-data/help.txt --- a/test-data/help.txt +++ b/test-data/help.txt @@ -1,6 +1,7 @@ > help # (#): Ignore all arguments and do nothing +backend (bak): Print the state of the symbolic backend backtrace (bt): Print the backtrace (AKA stack trace) block (blk): Print the statements in the current block break (b): Set a breakpoint at the entry to a function diff --git a/test/Test.hs b/test/Test.hs --- a/test/Test.hs +++ b/test/Test.hs @@ -86,7 +86,10 @@ loadTests :: FilePath -> IO Tasty.TestTree loadTests dir = do - files <- Dir.listDirectory dir + -- This `List.sort` is not technically necessary, it just ensures that test + -- cases will be performed in a stable ordering, since `Dir.listDirectory` + -- doesn't guarantee such an ordering. + files <- List.sort <$> Dir.listDirectory dir let dbgScripts = List.filter (".txt" `List.isSuffixOf`) files let tests = map (uncurry mkTest) (map (dir,) dbgScripts) pure (Tasty.testGroup dir tests)