crucible-debug 0.1.0 → 0.1.2.0

raw patch · 18 files changed

+456/−79 lines, 18 filesdep +extradep ~basedep ~cruciblenew-uploaderPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: extra

Dependency ranges changed: base, crucible

API changes (from Hackage documentation)

Files

• CHANGELOG.md +4/−0
• crucible-debug.cabal +36/−6
• src/Lang/Crucible/Debug.hs +68/−31
• src/Lang/Crucible/Debug/Command/Base.hs +11/−1
• src/Lang/Crucible/Debug/Commands.hs +5/−5
• src/Lang/Crucible/Debug/Context.hs +9/−10
• src/Lang/Crucible/Debug/Eval.hs +21/−8
• src/Lang/Crucible/Debug/Inputs.hs +10/−4
• src/Lang/Crucible/Debug/Outputs.hs +5/−6
• src/Lang/Crucible/Debug/Override.hs +90/−0
• src/Lang/Crucible/Debug/Personality.hs +73/−0
• src/Lang/Crucible/Debug/Response.hs +2/−0
• src/Lang/Crucible/Debug/Style.hs +3/−3
• src/Lang/Crucible/Pretty.hs +9/−0
• test-data/backend.txt +101/−0
• test-data/error/load-parse-error.txt +4/−4
• test-data/help.txt +1/−0
• test/Test.hs +4/−1

@@ -1,3 +1,7 @@+# 0.1.2 - 2025-11-09++- Store debugger state in the Crucible personality.+ # 0.1 -- 2025-03-21  Initial release.

@@ -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

@@ -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.

@@ -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

@@ -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

@@ -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   }+

@@ -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)

@@ -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)))

@@ -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

@@ -0,0 +1,90 @@+{-|+Copyright        : (c) Galois, Inc. 2025+Maintainer       : Langston Barrett <langston@galois.com>+-}++{-# 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]+  }

@@ -0,0 +1,73 @@+{-|+Copyright        : (c) Galois, Inc. 2025+Maintainer       : Langston Barrett <langston@galois.com>+-}++{-# 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 }

@@ -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

@@ -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

@@ -3,6 +3,7 @@ Maintainer       : Langston Barrett <langston@galois.com> -} +{-# 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     _ -> "<unsupported>"  ppFnVal ::

@@ -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+

@@ -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  

@@ -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

@@ -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)