diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,3 @@ +# 0.1 -- 2025-03-21 + +Initial release. diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -0,0 +1,30 @@ +Copyright (c) 2025 Galois Inc. +All rights reserved. + +Redistribution and use in source and binary forms, with or without +modification, are permitted provided that the following conditions +are met: + + * Redistributions of source code must retain the above copyright + notice, this list of conditions and the following disclaimer. + + * Redistributions in binary form must reproduce the above copyright + notice, this list of conditions and the following disclaimer in + the documentation and/or other materials provided with the + distribution. + + * Neither the name of Galois, Inc. nor the names of its contributors + may be used to endorse or promote products derived from this + software without specific prior written permission. + +THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS +IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED +TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A +PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT OWNER +OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, +EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, +PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR +PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF +LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING +NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS +SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,37 @@ +# crucible-debug + +`crucible-debug` is a library for interactive debugging of Crucible programs. +It is structured as an [`ExecutionFeature`][exec-feat], meaning that it can be used in situ inside of any program that uses Crucible. + +[exec-feat]: https://hackage.haskell.org/package/crucible-0.7.1/docs/Lang-Crucible-Simulator.html#t:ExecutionFeature + +Users interact with the debugger via a simple command language. +This language features a number of familiar commands such as setting and removing breakpoints (`break`/`delete`), printing stack traces (`backtrace`), stepping through symbolic execution (`step`), and loading debugger commands from files (`source`). +It additionally provides more Crucible-specific commands such as inspecting program CFGs (`cfg`) and printing the current path condition (`path-condition`). +All available commands can be listed using the interactive documentation system (`help`). + +In addition to the library, this package provides an executable. +The executable begins the debugger inside of a "minimal" Crucible program that immediately returns the unit value `()`. +This is not very interesting on its own, but the `load` command can load Crucible S-expression programs, and the `call` command can call functions from loaded programs. + +The command language can be extended by downstream packages. +Such extensions can be used to add commands that are specific to a particular Crucible syntax extension (i.e., source language). +For example, the `crucible-llvm-debug` package provides the `memory` command to print the current LLVM memory. + +This tool shares some functionality with the [surveyor] project. The principal architectural distinction is that `crucible-debug` is designed to be embedded into larger tools like Crux and SAW, while `surveyor` is a standalone application. + +[surveyor]: https://github.com/GaloisInc/surveyor + +The test suite is described in its Haddocks. + +## Acknowledgements + +This material is based upon work supported by the Defense Advanced Research Projects Agency under Contract No. W31P4Q-22-C-0017 and W31P4Q-23-C-0020 + +Any opinions, findings and conclusions or recommendations expressed in this material are those of the author(s) and do not necessarily reflect the views of the Defense Advanced Research Projects Agency or the U.S. Government. + +Distribution Statement A. Approved for public release: distribution is unlimited. + +## Copyright + +Copyright (c) Galois, Inc. 2025. diff --git a/app/Main.hs b/app/Main.hs new file mode 100644 --- /dev/null +++ b/app/Main.hs @@ -0,0 +1,14 @@ +{-# LANGUAGE ImportQualifiedPost #-} + +module Main (main) where + +import Data.Text.IO qualified as IO +import Lang.Crucible.Debug qualified as Debug + +main :: IO () +main = do + inputs <- Debug.defaultDebuggerInputs Debug.voidExts + Debug.bareDebugger + inputs + Debug.defaultDebuggerOutputs + IO.putStrLn diff --git a/crucible-debug.cabal b/crucible-debug.cabal new file mode 100644 --- /dev/null +++ b/crucible-debug.cabal @@ -0,0 +1,153 @@ +cabal-version: 2.4 +name: crucible-debug +version: 0.1.0 +author: Galois Inc. +maintainer: langston@galois.com +build-type: Simple +license: BSD-3-Clause +license-file: LICENSE +category: Language +synopsis: An interactive debugger for Crucible programs +description: + An interactive debugger for Crucible programs. + +extra-doc-files: README.md, CHANGELOG.md +extra-source-files: + LICENSE + test-data/**/*.txt + +common shared + -- Specifying -Wall and -Werror can cause the project to fail to build on + -- newer versions of GHC simply due to new warnings being added to -Wall. To + -- prevent this from happening we manually list which warnings should be + -- considered errors. We also list some warnings that are not in -Wall, though + -- try to avoid "opinionated" warnings (though this judgement is clearly + -- subjective). + -- + -- Warnings are grouped by the GHC version that introduced them, and then + -- alphabetically. + -- + -- A list of warnings and the GHC version in which they were introduced is + -- available here: + -- https://ghc.gitlab.haskell.org/ghc/doc/users_guide/using-warnings.html + + -- Since GHC 9.4 or earlier: + ghc-options: + -Wall + -Werror=ambiguous-fields + -Werror=compat-unqualified-imports + -Werror=deferred-type-errors + -Werror=deprecated-flags + -Werror=deprecations + -Werror=deriving-defaults + -Werror=dodgy-foreign-imports + -Werror=duplicate-exports + -Werror=empty-enumerations + -Werror=forall-identifier + -Werror=identities + -Werror=inaccessible-code + -Werror=incomplete-patterns + -Werror=incomplete-record-updates + -Werror=incomplete-uni-patterns + -Werror=inline-rule-shadowing + -Werror=misplaced-pragmas + -Werror=missed-extra-shared-lib + -Werror=missing-exported-signatures + -Werror=missing-fields + -Werror=missing-home-modules + -Werror=missing-methods + -Werror=operator-whitespace + -Werror=operator-whitespace-ext-conflict + -Werror=overflowed-literals + -Werror=overlapping-patterns + -Werror=partial-fields + -Werror=partial-type-signatures + -Werror=redundant-bang-patterns + -Werror=redundant-strictness-flags + -Werror=simplifiable-class-constraints + -Werror=star-binder + -Werror=star-is-type + -Werror=tabs + -Werror=typed-holes + -Werror=type-equality-out-of-scope + -Werror=type-equality-requires-operators + -Werror=unrecognised-pragmas + -Werror=unrecognised-warning-flags + -Werror=unsupported-calling-conventions + -Werror=unsupported-llvm-version + -Werror=unticked-promoted-constructors + -Werror=unused-imports + -Werror=warnings-deprecations + -Werror=wrong-do-bind + + ghc-prof-options: -O2 -fprof-auto-top + default-language: Haskell2010 + +library + import: shared + + build-depends: + base >= 4.13 && < 4.20, + containers, + crucible, + crucible-syntax, + directory, + filepath, + isocline, + lens, + megaparsec, + mtl, + parameterized-utils, + prettyprinter, + ring-buffer, + text, + vector, + what4, + + hs-source-dirs: src + + exposed-modules: + Lang.Crucible.Debug + Lang.Crucible.Debug.Inputs + Lang.Crucible.Debug.Outputs + Lang.Crucible.Pretty + + other-modules: + Lang.Crucible.Debug.Arg + Lang.Crucible.Debug.Arg.Type + Lang.Crucible.Debug.Breakpoint + Lang.Crucible.Debug.Command + Lang.Crucible.Debug.Command.Base + Lang.Crucible.Debug.Commands + Lang.Crucible.Debug.Complete + Lang.Crucible.Debug.Context + Lang.Crucible.Debug.Eval + Lang.Crucible.Debug.Regex + Lang.Crucible.Debug.Response + Lang.Crucible.Debug.Statement + Lang.Crucible.Debug.Style + Lang.Crucible.Debug.Trace + +test-suite crucible-debug-tests + import: shared + type: exitcode-stdio-1.0 + main-is: Test.hs + hs-source-dirs: test + build-depends: + base, + bytestring, + crucible-debug, + directory, + prettyprinter, + tasty, + tasty-golden, + text, + +executable crucible-debug + import: shared + hs-source-dirs: app + main-is: Main.hs + build-depends: + base >= 4.13, + crucible-debug, + text, diff --git a/src/Lang/Crucible/Debug.hs b/src/Lang/Crucible/Debug.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug.hs @@ -0,0 +1,327 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} + +module Lang.Crucible.Debug + ( debugger + , bareDebuggerExt + , bareDebugger + , Inps.defaultDebuggerInputs + , Outps.defaultDebuggerOutputs + , Arg.Arg(..) + , AType.ArgTypeRepr(..) + , type AType.Breakpoint + , type AType.Exactly + , type AType.Function + , type AType.Int + , type AType.Path + , type AType.Text + , Cmd.Command(Base, Ext) + , Cmd.CommandExt(..) + , Cmd.voidExts + , Cmds.execStateSimState + , Ctxt.EvalResult(..) + , Ctxt.Context(..) + , Ctxt.CommandImpl(..) + , Ctxt.ExtImpl(..) + , Ctxt.voidImpl + , Resp.Response(Ok, UserError, XResponse) + , Resp.UserError(NotApplicable) + , Resp.NotApplicable(DoneSimulating, NotYetSimulating) + , Resp.ResponseExt + , type Rgx.Regex + , type Rgx.Empty + , type Rgx.Lit + , type (Rgx.:|) + , type Rgx.Then + , type Rgx.Star + , Rgx.Match(..) + , Rgx.RegexRepr(..) + , Trace.Trace + , Trace.TraceEntry(..) + , Trace.latest + , IntrinsicPrinters(..) + ) 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.Maybe qualified as Maybe +import Data.Parameterized.Map qualified as MapF +import Data.Parameterized.Nonce qualified as Nonce +import Data.Parameterized.Some (Some(Some)) +import Data.Set qualified as Set +import Data.Text (Text) +import Data.Void (Void) +import Lang.Crucible.Backend qualified as C +import Lang.Crucible.Backend.Simple qualified as C +import Lang.Crucible.CFG.Extension qualified as C +import Lang.Crucible.Debug.Arg qualified as Arg +import Lang.Crucible.Debug.Arg.Type qualified as AType +import Lang.Crucible.Debug.Breakpoint qualified as Break +import Lang.Crucible.Debug.Command qualified as Cmd +import Lang.Crucible.Debug.Commands qualified as Cmds +import Lang.Crucible.Debug.Complete qualified as Complete +import Lang.Crucible.Debug.Complete (CompletionT) +import Lang.Crucible.Debug.Context (Context, DebuggerState) +import Lang.Crucible.Debug.Context qualified as Ctxt +import Lang.Crucible.Debug.Eval (EvalResult) +import Lang.Crucible.Debug.Eval qualified as Eval +import Lang.Crucible.Debug.Inputs (Inputs) +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.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.Style qualified as Style +import Lang.Crucible.Debug.Style (StyleT) +import Lang.Crucible.Debug.Trace qualified as Trace +import Lang.Crucible.FunctionHandle qualified as C +import Lang.Crucible.Pretty (IntrinsicPrinters(..)) +import Lang.Crucible.Simulator.CallFrame qualified as C +import Lang.Crucible.Simulator.EvalStmt qualified as C +import Lang.Crucible.Simulator.ExecutionTree qualified as C +import Lang.Crucible.Simulator qualified as C +import Lang.Crucible.Syntax.Concrete qualified as C +import Lang.Crucible.Types qualified as C +import Prettyprinter qualified as PP +import System.Exit qualified as Exit +import System.IO (stdout) +import What4.Expr qualified as W4 +import What4.Interface qualified as W4 + +-- Useful for debugging +_printState :: C.ExecState p sym ext rtp -> Text +_printState = + \case + C.AbortState {} -> "AbortState" + C.CallState {} -> "CallState" + C.TailCallState {} -> "TailCallState" + C.ReturnState {} -> "ReturnState" + C.ResultState {} -> "ResultState" + C.InitialState {} -> "InitialState" + C.OverrideState {} -> "OverrideState" + C.RunningState {} -> "RunningState" + C.SymbolicBranchState {} -> "SymbolicBranchState" + C.BranchMergeState {} -> "BranchMergeState" + C.ControlTransferState {} -> "ControlTransferState" + C.UnwindCallState {} -> "UnwindCallState" + +stepState :: + Context cExt p sym ext t -> + C.ExecState p sym ext rtp -> + IO DebuggerState +stepState ctx = + \case + C.AbortState {} -> + if Ctxt.dbgStopOnAbort ctx + then pure Ctxt.Stopped + else pure initState + C.CallState _retHandler frm _st -> do + C.SomeHandle hdl <- pure (C.resolvedCallHandle frm) + stepCall hdl + C.TailCallState _vfv frm _st -> do + C.SomeHandle hdl <- pure (C.resolvedCallHandle frm) + stepCall hdl + C.ReturnState _fnm _vfv _ret _st -> + case initState of + Ctxt.Running Ctxt.Finish -> pure Ctxt.Stopped + _ -> pure initState + C.RunningState (C.RunBlockEnd _) simState -> do + let fr = simState Lens.^. C.stateCrucibleFrame + C.CallFrame { C._frameCFG = cfg, C._frameBlockID = blkId } <- pure fr + let ent = Trace.TraceEntry cfg blkId + Trace.append (Ctxt.dbgTrace ctx) ent + pure initState + + -- Nothing to do for these... + C.InitialState {} -> pure initState + C.OverrideState {} -> pure initState + C.ResultState {} -> pure initState + C.RunningState {} -> pure initState + C.SymbolicBranchState {} -> pure initState + + -- These are mostly implementation details... + C.BranchMergeState {} -> pure initState + C.ControlTransferState {} -> pure initState + C.UnwindCallState {} -> pure initState + where + initState = Ctxt.dbgState ctx + + stepCall :: C.FnHandle args ret -> IO DebuggerState + stepCall hdl = do + let b = Break.BreakFunction (C.handleName hdl) + if Set.member b (Ctxt.dbgBreakpoints ctx) + then pure Ctxt.Stopped + else pure initState + +mergeResults :: + C.ExecutionFeatureResult p sym ext ret -> + C.ExecutionFeatureResult p sym ext ret -> + C.ExecutionFeatureResult p sym ext ret +mergeResults old new = + case old of + C.ExecutionFeatureNoChange -> new + _ -> + case new of + C.ExecutionFeatureNoChange -> old + _ -> new + +resultState :: + C.ExecutionFeatureResult p sym ext ret -> + Maybe (C.ExecState p sym ext ret) +resultState = + \case + C.ExecutionFeatureNoChange -> Nothing + C.ExecutionFeatureModifiedState s -> Just s + C.ExecutionFeatureNewState s -> Just s + +stopped :: + (sym ~ W4.ExprBuilder s st fs) => + C.IsSymInterface sym => + C.IsSyntaxExtension ext => + (?parserHooks :: C.ParserHooks ext) => + PP.Pretty cExt => + W4.IsExpr (W4.SymExpr sym) => + Context 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 + 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 + let featResult = mergeResults r (Eval.evalFeatureResult result0) + let result = result0 { Eval.evalFeatureResult = featResult } + let s = Maybe.fromMaybe s0 (resultState featResult) + let c = Eval.evalCtx result + Outps.send (Ctxt.dbgOutputs c) (Eval.evalResp result) + case Ctxt.dbgState c of + Ctxt.Quit -> pure result + Ctxt.Running {} -> pure result + Ctxt.Stopped -> go c s featResult + +dispatch :: + (sym ~ W4.ExprBuilder s st fs) => + C.IsSymInterface sym => + C.IsSyntaxExtension ext => + W4.IsExpr (W4.SymExpr sym) => + (?parserHooks :: C.ParserHooks ext) => + PP.Pretty cExt => + Context 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 = + 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 + Ctxt.Running (Ctxt.Step i) | i <= 1 -> do + let ctx = ctx0 { Ctxt.dbgState = Ctxt.Stopped } + dispatch ctx execState + Ctxt.Running (Ctxt.Step i) -> do + let ctx = ctx0 { Ctxt.dbgState = Ctxt.Running (Ctxt.Step (i - 1)) } + state <- stepState ctx execState + let ctx' = ctx0 { Ctxt.dbgState = state } + pure (ctx', C.ExecutionFeatureNoChange) + Ctxt.Running {} -> do + state <- stepState ctx0 execState + let ctx = ctx0 { Ctxt.dbgState = state } + pure (ctx, C.ExecutionFeatureNoChange) + Ctxt.Stopped -> do + result <- stopped ctx0 execState + pure (Eval.evalCtx result, Eval.evalFeatureResult result) + +debugger :: + (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 + +-- | Like 'bareDebugger', but with a syntax extension +bareDebuggerExt :: + C.IsSyntaxExtension ext => + (?parserHooks :: C.ParserHooks ext) => + PP.Pretty cExt => + Cmd.CommandExt cExt -> + (forall p sym t. C.IsSymInterface sym => Ctxt.ExtImpl cExt p sym ext t) -> + (forall p sym. C.IsSymInterface sym => C.ExtensionImpl p sym ext) -> + Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt) -> + Outputs IO (Response cExt) -> + (Text -> IO ()) -> + IO () +bareDebuggerExt cExts cEval extImpl inps outps logger = do + Some nonceGen <- Nonce.newIONonceGenerator + ha <- C.newHandleAllocator + sym <- W4.newExprBuilder W4.FloatIEEERepr W4.EmptyExprBuilderState nonceGen + 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 () + 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 + C.getProofObligations bak >>= \case + Nothing -> pure () + Just {} -> do + logger "There were unhandled proof obligations! Try `prove` and `clear`." + Exit.exitFailure + +-- | 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. +bareDebugger :: + Inputs (CompletionT Void (StyleT Void IO)) (Statement Void) -> + Outputs IO (Response Void) -> + (Text -> IO ()) -> + IO () +bareDebugger inps outps logger = + let ?parserHooks = C.ParserHooks Applicative.empty Applicative.empty in + bareDebuggerExt + Cmd.voidExts + Ctxt.voidImpl + C.emptyExtensionImpl + inps + outps + logger diff --git a/src/Lang/Crucible/Debug/Arg.hs b/src/Lang/Crucible/Debug/Arg.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug/Arg.hs @@ -0,0 +1,214 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett + +For the sake of correctness, consistency, and concision, it is desirable to +declaratively specify the types of arguments expected by 'Cmd.Command's. These +specifications are used to: + +* Parse said arguments (see 'match') +* Generate usage hints for @usage@ (see 'usage') +* Perform syntax highlighting (see "Lang.Crucible.Debug.Style") +* Provide tab-completions (see 'complete') + +Perhaps the simplest workable argument specification would be a list of basic +types (e.g., integer, string). However, the purpose of the command language +is to be convenient for interactive use. In particular, users should not have +to remember the names of several variants of a command that do fundamentally +similar tasks. To provide sufficient flexibilty to unite such variants under +a single command, the specification should allow (in increasing order of +sophistication): + +* sequencing (i.e., arity higher than 1), +* disjunction (at the very least, in a limited form), and +* quantification (optionality, repetition, and in particular, variable arity). + +To justify the necessity of such features, consider the following examples of +each, taken from the bread-and-butter commands of the @gdb@ command language: + +* sequencing: @break@ takes several (optional) arguments +* optionality: @step@ takes an optional integer argument +* quantification: @delete@ takes a variable number of breakpoint numbers + +The basic list-of-types specification clearly lacks such features. Luckily, +there is a well-understood specification language that allows all of the above, +namely, regular expressions. Thus, the debugger\'s commands are specified +using the facilities provided by "Lang.Crucible.Debug.Regex". The tokens of +the regular expression are basic types (see 'ArgTypeRepr'). Operations like +'derivative' are used internally to provide the high-level functionality +described at the beginning of this documentation. + +Commands that are not well-suited to this kind of argument validation can simply +accept @TEXT*@ and perform their own parsing (or not) at the cost of lacking +helpful documentation and completion. This is exactly the specification of the +comment (@#@) command, for example. +-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeOperators #-} + +module Lang.Crucible.Debug.Arg + ( Arg(..) + -- * Parsers + , ArgParseError(..) + , ArgParser(..) + , convert + -- * Operations + , match + , derivative + , types + , usage + ) where + +import Data.Coerce (coerce) +import Data.Foldable qualified as Foldable +import Data.Kind (Type) +import Data.Map.Strict (Map) +import Data.Map.Strict qualified as Map +import Data.Parameterized.Some (Some(Some)) +import Data.Parameterized.SymbolRepr (SymbolRepr, symbolRepr) +import Data.Parameterized.TraversableFC (fmapFC) +import Data.Sequence (Seq) +import Data.Text qualified as Text +import Lang.Crucible.Debug.Arg.Type (type ArgType(..), ArgTypeRepr(..)) +import Lang.Crucible.Debug.Breakpoint (Breakpoint(BreakFunction)) +import Lang.Crucible.Debug.Command qualified as Cmd +import Lang.Crucible.Debug.Regex qualified as Rgx +import Prelude hiding (Int) +import Prelude qualified as Prelude +import Prettyprinter qualified as PP +import Text.Read (readMaybe) +import What4.FunctionName qualified as W4 + +type Arg :: Type -> ArgType -> Type +data Arg cExt i where + ABreakpoint :: Breakpoint -> Arg cExt 'TBreakpoint + ACommand :: Cmd.Command cExt -> Arg cExt 'TCommand + AExactly :: SymbolRepr s -> Arg cExt ('TExactly s) + AFunction :: W4.FunctionName -> Arg cExt 'TFunction + AInt :: Prelude.Int -> Arg cExt 'TInt + APath :: Text.Text -> Arg cExt 'TPath + AText :: Text.Text -> Arg cExt 'TText + +data ArgParseError + = NotACommand Text.Text + | NotAnInt Text.Text + | NotExactly Text.Text Text.Text + deriving Show + +instance PP.Pretty ArgParseError where + pretty = + \case + NotACommand t -> PP.squotes (PP.pretty t) PP.<+> "is not a command" + NotAnInt t -> PP.squotes (PP.pretty t) PP.<+> "is not an integer" + NotExactly e t -> PP.squotes (PP.pretty t) PP.<+> "is not" PP.<+> PP.squotes (PP.pretty e) + +newtype ArgParser cExt t + = ArgParser { _runArgParser :: Rgx.TokenParser Text.Text ArgParseError (Arg cExt) t } + +argParser :: (Text.Text -> Either ArgParseError (Arg cExt t)) -> ArgParser cExt t +argParser = ArgParser . Rgx.TokenParser + +-- | Helper, not exported +maybeToEither :: e -> Maybe a -> Either e a +maybeToEither e = + \case + Nothing -> Left e + Just a -> Right a + +breakpoint :: ArgParser cExt 'TBreakpoint +breakpoint = + argParser (Right . ABreakpoint . BreakFunction . W4.functionNameFromText) + +function :: ArgParser cExt 'TFunction +function = + argParser (Right . AFunction . W4.functionNameFromText) + +command :: Cmd.CommandExt cExt -> ArgParser cExt 'TCommand +command cExt = argParser (\t -> ACommand <$> maybeToEither (NotACommand t) (Cmd.parse cExt t)) + +exactly :: SymbolRepr s -> ArgParser cExt ('TExactly s) +exactly s = + argParser $ \t -> + if t == symbolRepr s + then Right (AExactly s) + else Left (NotExactly (symbolRepr s) t) + +int :: ArgParser cExt 'TInt +int = argParser (\t -> AInt <$> maybeToEither (NotAnInt t) (readMaybe (Text.unpack t))) + +path :: ArgParser cExt 'TPath +path = argParser (Right . APath) + +text :: ArgParser cExt 'TText +text = argParser (Right . AText) + +parser :: Cmd.CommandExt cExt -> ArgTypeRepr t -> ArgParser cExt t +parser cExt = + \case + TBreakpointRepr -> breakpoint + TCommandRepr -> command cExt + TExactlyRepr s -> exactly s + TFunctionRepr -> function + TIntRepr -> int + TPathRepr -> path + TTextRepr -> text + +convert :: + Cmd.CommandExt cExt -> + Rgx.RegexRepr ArgTypeRepr r -> + Rgx.RegexRepr (ArgParser cExt) r +convert cExt = fmapFC (parser cExt) + +match :: + forall r cExt. + Rgx.RegexRepr (ArgParser cExt) r -> + [Text.Text] -> + Either (Rgx.MatchError Text.Text ArgParseError) (Rgx.Match (Arg cExt) r) +match r toks = + case Rgx.match @_ @_ @(Arg cExt) (coerce r) toks of + Left e -> Left e + Right (m, []) -> Right m + Right (_, as) -> Left (Rgx.NotEmpty as) + +derivative :: + forall cExt r. + Cmd.CommandExt cExt -> + Text.Text -> + Rgx.RegexRepr ArgTypeRepr r -> + Rgx.DerivativeResult ArgTypeRepr (Arg cExt) +derivative cExt = + Rgx.derivative + (coerce @_ @(Rgx.TokenParser _ ArgParseError (Arg cExt) _) . parser cExt) + +-- | Get the potential types that the regex assigns each argument, plus what it +-- would assign to the next one. +types :: + forall r cExt. + Cmd.CommandExt cExt -> + Rgx.RegexRepr ArgTypeRepr r -> + [Text.Text] -> + (Map Text.Text (Seq (Some ArgTypeRepr)), Seq (Some ArgTypeRepr)) +types cExt r = + \case + [] -> (Map.empty, Rgx.nextLits r) + (t : ts) -> + case derivative cExt t r of + Rgx.DerivativeResult (Some r') _ -> + let (m, final) = types cExt r' ts in + (Map.insertWith (<>) t (Rgx.nextLits r) m, final) + +usage :: Rgx.RegexRepr ArgTypeRepr r -> [PP.Doc ann] +usage r = + Foldable.toList $ + fmap (\(Some r') -> Rgx.prettySugar " " PP.pretty r') (Rgx.liftOrs (Rgx.sugar r)) diff --git a/src/Lang/Crucible/Debug/Arg/Type.hs b/src/Lang/Crucible/Debug/Arg/Type.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug/Arg/Type.hs @@ -0,0 +1,130 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE StandaloneKindSignatures #-} + +module Lang.Crucible.Debug.Arg.Type + ( type ArgType(..) + , type Breakpoint + , type Command + , type Exactly + , type Function + , type Int + , type Path + , type Text + , ArgTypeRepr(..) + ) where + +import Data.Kind (Type) +import Data.Parameterized.Classes (KnownRepr(knownRepr), ShowF (showF)) +import Data.Parameterized.SymbolRepr (SymbolRepr, knownSymbol, symbolRepr) +import Data.Type.Equality (TestEquality(testEquality), type (:~:)(Refl)) +import GHC.TypeLits (KnownSymbol, Symbol) +import Lang.Crucible.Debug.Regex qualified as Rgx +import Prelude hiding (Int) +import Prettyprinter qualified as PP + +-- | Type-level only +data ArgType + = TBreakpoint + | TCommand + | TExactly Symbol + | TFunction + | TInt + | TPath + | TText + +type Breakpoint = Rgx.Lit 'TBreakpoint +type Command = Rgx.Lit 'TCommand +type Exactly s = Rgx.Lit ('TExactly s) +type Function = Rgx.Lit 'TFunction +type Int = Rgx.Lit 'TInt +type Path = Rgx.Lit 'TPath +type Text = Rgx.Lit 'TText + +-- | Value-level representative of 'ArgType' +type ArgTypeRepr :: ArgType -> Type +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 + +instance Show (ArgTypeRepr t) where + show = + \case + TBreakpointRepr -> "TBreakpointRepr" + TCommandRepr -> "TCommandRepr" + TExactlyRepr s -> "TExactlyRepr(" ++ show s ++ ")" + TFunctionRepr -> "TFunctionRepr" + TIntRepr -> "TIntRepr" + TPathRepr -> "TPathRepr" + TTextRepr -> "TTextRepr" + +instance ShowF ArgTypeRepr where + showF = show + +instance TestEquality ArgTypeRepr where + testEquality r r' = + case (r, r') of + (TBreakpointRepr, TBreakpointRepr) -> Just Refl + (TBreakpointRepr, _) -> Nothing + (TCommandRepr, TCommandRepr) -> Just Refl + (TCommandRepr, _) -> Nothing + (TExactlyRepr s, TExactlyRepr s') -> + case testEquality s s' of + Just Refl -> Just Refl + Nothing -> Nothing + (TExactlyRepr {}, _) -> Nothing + (TFunctionRepr, TFunctionRepr) -> Just Refl + (TFunctionRepr {}, _) -> Nothing + (TIntRepr, TIntRepr) -> Just Refl + (TIntRepr, _) -> Nothing + (TPathRepr, TPathRepr) -> Just Refl + (TPathRepr, _) -> Nothing + (TTextRepr, TTextRepr) -> Just Refl + (TTextRepr, _) -> Nothing + +instance KnownRepr ArgTypeRepr 'TBreakpoint where + knownRepr = TBreakpointRepr + +instance KnownRepr ArgTypeRepr 'TCommand where + knownRepr = TCommandRepr + +instance KnownSymbol s => KnownRepr ArgTypeRepr ('TExactly s) where + knownRepr = TExactlyRepr knownSymbol + +instance KnownRepr ArgTypeRepr 'TFunction where + knownRepr = TFunctionRepr + +instance KnownRepr ArgTypeRepr 'TInt where + knownRepr = TIntRepr + +instance KnownRepr ArgTypeRepr 'TPath where + knownRepr = TPathRepr + +instance KnownRepr ArgTypeRepr 'TText where + knownRepr = TTextRepr + +instance PP.Pretty (ArgTypeRepr t) where + pretty = + \case + TBreakpointRepr -> "BREAKPOINT" + TCommandRepr -> "COMMAND" + TExactlyRepr s -> PP.pretty (symbolRepr s) + TFunctionRepr -> "FUNCTION" + TIntRepr -> "INT" + TPathRepr -> "PATH" + TTextRepr -> "TEXT" diff --git a/src/Lang/Crucible/Debug/Breakpoint.hs b/src/Lang/Crucible/Debug/Breakpoint.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug/Breakpoint.hs @@ -0,0 +1,28 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE ImportQualifiedPost #-} + +module Lang.Crucible.Debug.Breakpoint + ( Breakpoint(..) + , toString + , toText + ) where + +import Data.Text qualified as Text +import Data.Text (Text) +import What4.FunctionName qualified as W4 + +newtype Breakpoint + = BreakFunction W4.FunctionName + deriving (Eq, Ord) + +toString :: Breakpoint -> String +toString = Text.unpack . toText +{-# INLINE toString #-} + +toText :: Breakpoint -> Text +toText (BreakFunction fNm) = W4.functionName fNm +{-# INLINE toText #-} diff --git a/src/Lang/Crucible/Debug/Command.hs b/src/Lang/Crucible/Debug/Command.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug/Command.hs @@ -0,0 +1,114 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} + +module Lang.Crucible.Debug.Command + ( Command(..) + , CommandExt(..) + , voidExts + , allCmds + , name + , abbrev + , parse + , detail + , help + , regex + ) where + +import Data.List qualified as List +import Data.Parameterized.Some (Some) +import Data.Text (Text) +import Data.Void (Void, absurd) +import Lang.Crucible.Debug.Arg.Type (ArgTypeRepr) +import Lang.Crucible.Debug.Command.Base qualified as BCmd +import Lang.Crucible.Debug.Regex qualified as Rgx +import Prettyprinter qualified as PP + +data CommandExt cExt + = CommandExt + { -- | Used in 'abbrev', 'parse' + extAbbrev :: cExt -> Text + , extList :: [cExt] + -- | 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. + , extDetail :: cExt -> Maybe 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. + , extHelp :: cExt -> Text + -- | Used in 'help', 'parse' + , extName :: cExt -> Text + -- | Used in 'help' + , extRegex :: cExt -> Some (Rgx.RegexRepr ArgTypeRepr) + } + +voidExts :: CommandExt Void +voidExts = + CommandExt + { extAbbrev = absurd + , extDetail = absurd + , extHelp = absurd + , extList = [] + , extName = absurd + , extRegex = absurd + } + +data Command cExt + = Base BCmd.BaseCommand + | Ext cExt + deriving (Functor, Show) + +instance PP.Pretty cExt => PP.Pretty (Command cExt) where + pretty = + \case + Base bCmd -> PP.pretty bCmd + Ext xCmd -> PP.pretty xCmd + +name :: CommandExt cExt -> Command cExt -> Text +name cExts = + \case + Base bCmd -> BCmd.name bCmd + Ext xCmd -> extName cExts xCmd + +abbrev :: CommandExt cExt -> Command cExt -> Text +abbrev cExts = + \case + Base bCmd -> BCmd.abbrev bCmd + Ext xCmd -> extAbbrev cExts xCmd + +allCmds :: CommandExt cExt -> [Command cExt] +allCmds cExts = map Base [minBound..maxBound] ++ map Ext (extList cExts) + +parse :: CommandExt cExt -> Text -> Maybe (Command cExt) +parse cExts txt = + List.find (\c -> name cExts c == txt || abbrev cExts c == txt) (allCmds cExts) + +detail :: CommandExt cExt -> Command cExt -> Maybe Text +detail cExts = + \case + Base bCmd -> BCmd.detail bCmd + Ext xCmd -> extDetail cExts xCmd + +help :: CommandExt cExt -> Command cExt -> Text +help cExts = + \case + Base bCmd -> BCmd.help bCmd + Ext xCmd -> extHelp cExts xCmd + +regex :: CommandExt cExt -> Command cExt -> Some (Rgx.RegexRepr ArgTypeRepr) +regex cExts = + \case + Base bCmd -> BCmd.regex bCmd + Ext xCmd -> extRegex cExts xCmd diff --git a/src/Lang/Crucible/Debug/Command/Base.hs b/src/Lang/Crucible/Debug/Command/Base.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug/Command/Base.hs @@ -0,0 +1,335 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeOperators #-} + +module Lang.Crucible.Debug.Command.Base + ( BaseCommand(..) + , name + , abbrev + , detail + , help + , regex + -- * Regular expressions + , rBacktrace + , rBlock + , rBreak + , rCall + , rCfg + , rClear + , rComment + , rDelete + , rDone + , rFinish + , rFrame + , rHelp + , rLoad + , rLocation + , rObligation + , rPathCondition + , rProve + , rQuit + , rRegister + , rRun + , SecretRegex + , rSecret + , rSource + , rStep + , rTrace + , rUsage + ) where + +import Data.Parameterized.Classes (knownRepr) +import Data.Parameterized.Some (Some(Some)) +import Data.Text (Text) +import Lang.Crucible.Debug.Arg.Type (ArgTypeRepr) +import Lang.Crucible.Debug.Arg.Type qualified as AType +import Lang.Crucible.Debug.Regex qualified as Rgx +import Prettyprinter qualified as PP + +data BaseCommand + = Backtrace + | Block + | Break + | Call + | Cfg + | Clear + | Comment + | Delete + | Done + | Finish + | Frame + | Help + | Load + | Location + | Obligation + | PathCondition + | Prove + | Quit + | Register + | Run + | Secret + | Source + | Step + | Trace + | Usage + deriving (Bounded, Enum, Show) + +instance PP.Pretty BaseCommand where + pretty = PP.pretty . name + +name :: BaseCommand -> Text +name = + \case + Backtrace -> "backtrace" + Block -> "block" + Break -> "break" + Call -> "call" + Cfg -> "cfg" + Clear -> "clear" + Comment -> "#" + Delete -> "delete" + Done -> "done" + Finish -> "finish" + Frame -> "frame" + Help -> "help" + Load -> "load" + Location -> "location" + Obligation -> "obligation" + PathCondition -> "path-condition" + Prove -> "prove" + Quit -> "quit" + Register -> "register" + Run -> "run" + Secret -> "secret" + Step -> "step" + Source -> "source" + Trace -> "trace" + Usage -> "usage" + +abbrev :: BaseCommand -> Text +abbrev = + \case + Backtrace -> "bt" + Block -> "blk" + Break -> "b" + Call -> "cl" + Cfg -> "cg" + Clear -> "cr" + Comment -> "#" + Delete -> "d" + Done -> "done" + Finish -> "fh" + Frame -> "fr" + Help -> "h" + Load -> "l" + Location -> "loc" + Obligation -> "o" + PathCondition -> "pcond" + Prove -> "p" + Quit -> "q" + Register -> "reg" + Run -> "r" + Secret -> "." + Step -> "s" + Source -> "src" + Trace -> "trace" + Usage -> "u" + +-- | See 'Lang.Crucible.Debug.Command.extDetail' +detail :: BaseCommand -> Maybe Text +detail = + \case + Backtrace -> Nothing + Block -> Nothing + Break -> Nothing + Call -> Nothing + Cfg -> Nothing + Clear -> Nothing + Comment -> Nothing + Delete -> Nothing + Done -> Nothing + Finish -> Nothing + Frame -> Nothing + Help -> Nothing + Load -> Nothing + Location -> Nothing + Obligation -> Nothing + PathCondition -> Nothing + Prove -> Nothing + Quit -> Nothing + Register -> Just "\ + \When given no arguments, prints all values in scope. \ + \Otherwise, prints the values with the given numbers, one per line.\ + \\n\n\ + + \The value numbering scheme is based on the structure of Crucible CFGs. \ + \A Crucible CFG (function) is made up of *basic blocks*. \ + \Each basic block takes a list of arguments. \ + \The first block in the function is the *entry* block; \ + \the entry block takes the same arguments as the function. \ + \Each block contains a number of *statements*, which may define values. \ + \The value defined by a statement is in scope for the rest of the block.\ + \\n\n\ + + \Values are then numbered as follows: \ + \The first argument to the current block is numbered 0. \ + \Increasing numbers refer to later arguments. \ + \After arguments, higher numbers refer to values defined by statements.\ + \" + Run -> Nothing + Secret -> Nothing + Step -> Nothing + Source -> Nothing + Trace -> Nothing + Usage -> Nothing + +-- | See 'Lang.Crucible.Debug.Command.extHelp' +help :: BaseCommand -> Text +help = + \case + 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" + Call -> "Call a function (must take no arguments and return the unit type)" + Cfg -> "Print the CFG of a function (the current function if none is provided)" + Clear -> "Drop the current proof obligations" + Comment -> "Ignore all arguments and do nothing" + Delete -> "Remove a breakpoint" + Done -> "Like `quit`, but only applies when symbolic execution has finished" + Finish -> "Execute to the end of the current function" + Frame -> "Print information about the active stack frame" + Help -> "Display help text" + Load -> "Load a Crucible S-expression program from a file" + Location -> "Print the current program location" + Obligation -> "Print the current proof obligations" + PathCondition -> "Print the current path condition" + Prove -> "Prove the current goals" + Quit -> "Exit the debugger" + Register -> "Print registers (including block/function arguments)" + Run -> "Continue to the next breakpoint or the end of execution" + Secret -> "Maintenance commands, used for testing" + Step -> "Continue N steps of execution (default: 1)" + Source -> "Execute a file containing debugger commands" + Trace -> "Print the N most recently executed basic blocks (default: 2)" + Usage -> "Display command usage hint" + +regex :: BaseCommand -> Some (Rgx.RegexRepr ArgTypeRepr) +regex = + \case + Backtrace -> Some rBacktrace + Block -> Some rBlock + Break -> Some rBreak + Call -> Some rCall + Cfg -> Some rCfg + Clear -> Some rClear + Comment -> Some rComment + Delete -> Some rDelete + Done -> Some rDone + Finish -> Some rFinish + Frame -> Some rFrame + Help -> Some rHelp + Load -> Some rLoad + Location -> Some rLocation + Obligation -> Some rObligation + PathCondition -> Some rPathCondition + Prove -> Some rProve + Quit -> Some rQuit + Register -> Some rRegister + Run -> Some rRun + Secret -> Some rSecret + Step -> Some rStep + Source -> Some rSource + Trace -> Some rTrace + Usage -> Some rUsage + +rBacktrace :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty +rBacktrace = knownRepr + +rBlock :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty +rBlock = knownRepr + +rBreak :: Rgx.RegexRepr ArgTypeRepr AType.Function +rBreak = knownRepr + +rCall :: Rgx.RegexRepr ArgTypeRepr AType.Function +rCall = knownRepr + +rCfg :: Rgx.RegexRepr ArgTypeRepr (Rgx.Empty Rgx.:| AType.Function) +rCfg = knownRepr + +rClear :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty +rClear = knownRepr + +rComment :: Rgx.RegexRepr ArgTypeRepr (Rgx.Star AType.Text) +rComment = knownRepr + +rDelete :: Rgx.RegexRepr ArgTypeRepr AType.Breakpoint +rDelete = knownRepr + +rDone :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty +rDone = knownRepr + +rFinish :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty +rFinish = knownRepr + +rFrame :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty +rFrame = knownRepr + +rHelp :: Rgx.RegexRepr ArgTypeRepr (Rgx.Empty Rgx.:| AType.Command) +rHelp = knownRepr + +rLoad :: Rgx.RegexRepr ArgTypeRepr AType.Path +rLoad = knownRepr + +rLocation :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty +rLocation = knownRepr + +rObligation :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty +rObligation = knownRepr + +rPathCondition :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty +rPathCondition = knownRepr + +rProve :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty +rProve = knownRepr + +rQuit :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty +rQuit = knownRepr + +rRegister :: Rgx.RegexRepr ArgTypeRepr (Rgx.Star AType.Int) +rRegister = knownRepr + +rRun :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty +rRun = knownRepr + +type CompleteRegex + = Rgx.Then (AType.Exactly "complete") (Rgx.Then AType.Command (Rgx.Star AType.Text)) + +type StyleRegex + = Rgx.Then (AType.Exactly "style") (Rgx.Then AType.Command (Rgx.Star AType.Text)) + +type SecretRegex + = CompleteRegex Rgx.:| StyleRegex + +rSecret :: Rgx.RegexRepr ArgTypeRepr SecretRegex +rSecret = knownRepr + +rSource :: Rgx.RegexRepr ArgTypeRepr AType.Path +rSource = knownRepr + +rStep :: Rgx.RegexRepr ArgTypeRepr (Rgx.Empty Rgx.:| AType.Int) +rStep = knownRepr + +rTrace :: Rgx.RegexRepr ArgTypeRepr (Rgx.Empty Rgx.:| AType.Int) +rTrace = knownRepr + +rUsage :: Rgx.RegexRepr ArgTypeRepr AType.Command +rUsage = knownRepr diff --git a/src/Lang/Crucible/Debug/Commands.hs b/src/Lang/Crucible/Debug/Commands.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug/Commands.hs @@ -0,0 +1,481 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeOperators #-} + +module Lang.Crucible.Debug.Commands + ( execStateSimState + , backtrace + , block + , call + , cfg + , frame + , help + , load + , prove + , reg + , secret + , source + , usage + ) where + +import Control.Exception qualified as X +import Control.Lens qualified as Lens +import Control.Monad.Except (runExceptT) +import Control.Monad.IO.Class (liftIO) +import Data.List qualified as List +import Data.Maybe qualified as Maybe +import Data.Parameterized.Classes (ixF') +import Data.Parameterized.Context qualified as Ctx +import Data.Parameterized.Nonce qualified as Nonce +import Data.Parameterized.Some (Some(Some), viewSome) +import Data.Parameterized.TraversableFC (toListFC) +import Data.Sequence qualified as Seq +import Data.Text.IO qualified as IO +import Data.Text qualified as Text +import Lang.Crucible.Analysis.Postdom qualified as C +import Lang.Crucible.Backend.Prove qualified as Prove +import Lang.Crucible.Backend qualified as C +import Lang.Crucible.CFG.Core qualified as C +import Lang.Crucible.CFG.Extension qualified as C +import Lang.Crucible.CFG.Reg qualified as C.Reg +import Lang.Crucible.CFG.SSAConversion qualified as C +import Lang.Crucible.Debug.Arg qualified as Arg +import Lang.Crucible.Debug.Command.Base qualified as BCmd +import Lang.Crucible.Debug.Command qualified as Cmd +import Lang.Crucible.Debug.Complete (CompletionT) +import Lang.Crucible.Debug.Complete qualified as Complete +import Lang.Crucible.Debug.Context (Context) +import Lang.Crucible.Debug.Context qualified as Ctxt +import Lang.Crucible.Debug.Inputs (Inputs) +import Lang.Crucible.Debug.Inputs qualified as Inps +import Lang.Crucible.Debug.Outputs qualified as Outps +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 qualified as Stmt +import Lang.Crucible.Debug.Statement (Statement) +import Lang.Crucible.Debug.Style qualified as Style +import Lang.Crucible.Debug.Style (StyleT) +import Lang.Crucible.FunctionHandle qualified as C +import Lang.Crucible.Pretty (ppRegVal) +import Lang.Crucible.Simulator.CallFrame qualified as C +import Lang.Crucible.Simulator.EvalStmt qualified as C +import Lang.Crucible.Simulator.ExecutionTree qualified as C +import Lang.Crucible.Simulator qualified as C +import Lang.Crucible.Syntax.Atoms qualified as C +import Lang.Crucible.Syntax.Concrete qualified as C +import Lang.Crucible.Syntax.SExpr qualified as C +import Lang.Crucible.Utils.Seconds qualified as Sec +import Lang.Crucible.Utils.Timeout qualified as CTO +import Prettyprinter qualified as PP +import System.Exit qualified as Exit +import Text.Megaparsec qualified as MP +import What4.Config qualified as W4 +import What4.Expr.Builder qualified as W4 +import What4.FunctionName qualified as W4 +import What4.Interface qualified as W4 +import What4.ProgramLoc qualified as W4 +import What4.Solver qualified as W4 + +--------------------------------------------------------------------- +-- Helpers, exported + +execStateSimState :: + C.ExecState p sym ext r -> + Either Resp.NotApplicable (C.SomeSimState p sym ext r) +execStateSimState = + \case + C.ResultState _ -> Left Resp.DoneSimulating + C.AbortState _ st -> Right (C.SomeSimState st) + C.UnwindCallState _ _ st -> Right (C.SomeSimState st) + C.CallState _ _ st -> Right (C.SomeSimState st) + C.TailCallState _ _ st -> Right (C.SomeSimState st) + C.ReturnState _ _ _ st -> Right (C.SomeSimState st) + C.ControlTransferState _ st -> Right (C.SomeSimState st) + C.RunningState _ st -> Right (C.SomeSimState st) + C.SymbolicBranchState _ _ _ _ st -> Right (C.SomeSimState st) + C.OverrideState _ st -> Right (C.SomeSimState st) + C.BranchMergeState _ st -> Right (C.SomeSimState st) + C.InitialState _ _ _ _ _ -> Left Resp.NotYetSimulating + +--------------------------------------------------------------------- +-- Helpers, not exported + +insertCfg :: + C.IsSyntaxExtension ext => + C.Reg.CFG ext blocks init ret -> + C.FnHandleMap (C.FnState p sym ext) -> + C.FnHandleMap (C.FnState p sym ext) +insertCfg regCFG hdlMap = + case C.toSSA regCFG of + C.SomeCFG ssaCFG -> + C.insertHandleMap + (C.cfgHandle ssaCFG) + (C.UseCFG ssaCFG (C.postdomInfo ssaCFG)) + hdlMap + +data SomeFn f = forall args ret. SomeFn (f args ret) + +lookupHandleMapByName :: + W4.FunctionName -> + C.FnHandleMap f -> + Maybe (SomeFn f) +lookupHandleMapByName fNm hdls = do + let sHdls = C.handleMapToHandles hdls + C.SomeHandle h <- List.find (\(C.SomeHandle hdl) -> C.handleName hdl == fNm) sHdls + SomeFn <$> C.lookupHandleMap h hdls + +-- TODO: Upstream to Crucible as a Lens +modifySimContext :: + (C.SimContext p sym ext -> C.SimContext p sym ext) -> + C.ExecState p sym ext r -> + C.ExecState p sym ext r +modifySimContext f = + \case + C.ResultState r -> + case r of + C.FinishedResult ctx x -> C.ResultState (C.FinishedResult (f ctx) x) + C.AbortedResult ctx x -> C.ResultState (C.AbortedResult (f ctx) x) + C.TimeoutResult es -> modifySimContext f es + C.AbortState x s -> C.AbortState x (s Lens.& C.stateContext Lens.%~ f) + C.UnwindCallState x y s -> C.UnwindCallState x y (s Lens.& C.stateContext Lens.%~ f) + C.CallState x y s -> C.CallState x y (s Lens.& C.stateContext Lens.%~ f) + C.TailCallState x y s -> C.TailCallState x y (s Lens.& C.stateContext Lens.%~ f) + C.ReturnState x y z s -> C.ReturnState x y z (s Lens.& C.stateContext Lens.%~ f) + C.ControlTransferState x s -> C.ControlTransferState x (s Lens.& C.stateContext Lens.%~ f) + C.RunningState x s -> C.RunningState x (s Lens.& C.stateContext Lens.%~ f) + C.SymbolicBranchState x y z w s -> C.SymbolicBranchState x y z w (s Lens.& C.stateContext Lens.%~ f) + C.OverrideState x s -> C.OverrideState x (s Lens.& C.stateContext Lens.%~ f) + C.BranchMergeState x s -> C.BranchMergeState x (s Lens.& C.stateContext Lens.%~ f) + C.InitialState ctx x y z w -> C.InitialState (f ctx) x y z w + +--------------------------------------------------------------------- +-- Commands, exported + +backtrace :: + C.ExecState p sym ext r -> + IO (Response cExt) +backtrace execState = + case execStateSimState execState of + Left notApplicable -> pure (Resp.UserError (Resp.NotApplicable notApplicable)) + Right (C.SomeSimState simState) -> do + let frames = C.activeFrames (C._stateTree simState) + pure (Resp.Backtrace (C.ppExceptionContext frames)) + +block :: + C.IsSyntaxExtension ext => + W4.IsExpr (W4.SymExpr sym) => + Context cExt p sym ext t -> + C.ExecState p sym ext r -> + IO (Response cExt) +block _ctx execState = + case execStateSimState execState of + Left notApplicable -> pure (Resp.UserError (Resp.NotApplicable notApplicable)) + Right (C.SomeSimState simState) -> + let fr = simState Lens.^. C.stateTree . C.actFrame . C.gpValue in + case fr of + C.MF callFrame -> + let regs = C.regMap (callFrame Lens.^. C.frameRegs) in + pure (Resp.Block (ppStmtSeq False (Ctx.size regs) (C._frameStmts callFrame))) + C.OF {} -> pure (Resp.UserError (Resp.NotApplicable Resp.NoCfg)) + C.RF {} -> pure (Resp.UserError (Resp.NotApplicable Resp.NoCfg)) + where + -- TODO: The below is taken from Crucible. Export? + + prefixLineNum :: Bool -> W4.ProgramLoc -> PP.Doc ann -> PP.Doc ann + prefixLineNum True pl d = PP.vcat ["%" PP.<+> W4.ppNoFileName (W4.plSourceLoc pl), d] + prefixLineNum False _ d = d + + ppStmtSeq :: C.PrettyExt ext => Bool -> Ctx.Size ctx -> C.StmtSeq ext blocks ret ctx -> PP.Doc ann + ppStmtSeq ppLineNum h (C.ConsStmt pl s r) = + PP.vcat + [ prefixLineNum ppLineNum pl (C.ppStmt h s) + , ppStmtSeq ppLineNum (C.nextStmtHeight h s) r + ] + ppStmtSeq ppLineNum _ (C.TermStmt pl s) = + prefixLineNum ppLineNum pl (PP.pretty s) + +call :: + C.IsSymInterface sym => + C.IsSyntaxExtension ext => + C.ExecState p sym ext (C.RegEntry sym t) -> + C.TypeRepr t -> + W4.FunctionName -> + IO (C.ExecutionFeatureResult p sym ext (C.RegEntry sym t), Response cExt) +call execState rTy fNm = do + let fTy = C.FunctionHandleRepr Ctx.empty C.UnitRepr + let binds = execState Lens.^. Lens.to C.execStateContext . C.functionBindings + case C.searchHandleMap fNm fTy (C.fnBindings binds) of + Nothing -> do + let hdls = C.handleMapToHandles (C.fnBindings binds) + let names = map (\(C.SomeHandle hdl) -> C.handleName hdl) hdls + pure (C.ExecutionFeatureNoChange, Resp.UserError (Resp.FnNotFound fNm names)) + Just (hdl, bind) -> do + case execStateSimState execState of + Left notApplicable -> pure (C.ExecutionFeatureNoChange, Resp.UserError (Resp.NotApplicable notApplicable)) + Right (C.SomeSimState simState) -> do + let initCtx = simState Lens.^. C.stateContext + let globs = simState Lens.^. C.stateGlobals + let abortHdl = simState Lens.^. C.abortHandler + let initState = + C.InitialState initCtx globs abortHdl rTy $ + C.runOverrideSim rTy $ + let args = C.RegMap Ctx.empty in + case bind of + C.UseOverride o -> do + _ <- C.callOverride hdl o args + C.exitExecution Exit.ExitSuccess + C.UseCFG c _ -> do + _ <- C.callCFG c args + C.exitExecution Exit.ExitSuccess + let featRes = C.ExecutionFeatureNewState initState + pure (featRes, Resp.Ok) + +cfg :: + C.IsSyntaxExtension ext => + C.ExecState p sym ext r -> + Maybe W4.FunctionName -> + IO (Response cExt) +cfg execState = + \case + Just fNm -> do + let binds = execState Lens.^. Lens.to C.execStateContext . C.functionBindings + let hdls = C.handleMapToHandles (C.fnBindings binds) + let names = map (\(C.SomeHandle hdl) -> C.handleName hdl) hdls + case lookupHandleMapByName fNm (C.fnBindings binds) of + Nothing -> pure (Resp.UserError (Resp.FnNotFound fNm names)) + Just (SomeFn (C.UseOverride {})) -> pure (Resp.UserError (Resp.NotACfg fNm)) + Just (SomeFn (C.UseCFG c _)) -> pure (Resp.Cfg (C.ppCFG True c)) + Nothing -> + case execStateSimState execState of + Left notApplicable -> pure (Resp.UserError (Resp.NotApplicable notApplicable)) + Right (C.SomeSimState simState) -> do + case simState Lens.^. C.stateTree . C.actFrame . C.gpValue of + C.MF (C.CallFrame { C._frameCFG = c }) -> + pure (Resp.Cfg (C.ppCFG True c)) + C.OF {} -> pure (Resp.UserError (Resp.NotApplicable Resp.NoCfg)) + C.RF {} -> pure (Resp.UserError (Resp.NotApplicable Resp.NoCfg)) + +frame :: + C.IsSyntaxExtension ext => + W4.IsExpr (W4.SymExpr sym) => + Context cExt p sym ext t -> + C.ExecState p sym ext r -> + IO (Response cExt) +frame _ctx execState = + case execStateSimState execState of + Left notApplicable -> pure (Resp.UserError (Resp.NotApplicable notApplicable)) + Right (C.SomeSimState simState) -> + pure $ Resp.Frame $ + let fr = simState Lens.^. C.stateTree . C.actFrame . C.gpValue in + let name = fr Lens.^. C.frameFunctionName in + case fr of + C.OF ovFrame -> + let regs = C.regMap (ovFrame Lens.^. C.overrideRegMap) in + PP.vcat + [ "Override:" PP.<+> PP.pretty name + , "" + , "Argument types:" + , PP.vcat $ toListFC (bullet . PP.pretty . C.regType) regs + ] + C.MF callFrame -> + let regs = C.regMap (callFrame Lens.^. C.frameRegs) in + PP.vcat + [ "CFG:" PP.<+> PP.pretty name + , "Block:" PP.<+> viewSome PP.pretty (C._frameBlockID callFrame) + , "" + , "Argument types:" + , PP.vcat $ toListFC (bullet . PP.pretty . C.regType) regs + ] + C.RF {} -> "Return:" PP.<+> PP.pretty name + where bullet = ("-" PP.<+>) . PP.align + +help :: + C.IsSyntaxExtension ext => + (?parserHooks :: C.ParserHooks ext) => + PP.Pretty cExt => + Cmd.CommandExt cExt -> + Maybe (Cmd.Command cExt) -> + Response cExt +help cExts = + \case + Nothing -> + let mkHelp c = Cmd.name cExts c <> " (" <> Cmd.abbrev cExts c <> ")" <> ": " <> Cmd.help cExts c in + Resp.Help (PP.pretty (Text.unlines (List.sort (map mkHelp (Cmd.allCmds cExts))))) + Just cmd -> + Resp.Help $ + -- See 'Lang.Crucible.Debug.Command.ext{Detail,Help}' for expectations + -- on these strings, which are why it makes sense to format them this + -- way (e.g., adding a period, printing "details" after "help"), etc. + let basic = [usage cExts cmd, "", PP.pretty (Cmd.help cExts cmd) <> "."] + detail = + case Cmd.detail cExts cmd of + Just more -> ["", PP.pretty more] + Nothing -> [] + in PP.vcat (basic ++ detail) + +load :: + C.IsSyntaxExtension ext => + (?parserHooks :: C.ParserHooks ext) => + C.ExecState p sym ext r -> + FilePath -> + IO (C.ExecutionFeatureResult p sym ext r, Response cExt) +load execState0 path = do + eTxt <- X.try (IO.readFile path) + case eTxt of + Left ioErr -> pure (C.ExecutionFeatureNoChange, Resp.IOError ioErr) + Right txt -> do + case MP.parse (C.skipWhitespace *> MP.many (C.sexp C.atom) <* MP.eof) path txt of + Left err -> pure (C.ExecutionFeatureNoChange, Resp.UserError (Resp.LoadParseError err)) + Right v -> + Nonce.withIONonceGenerator $ \ng -> do + let execCtx = C.execStateContext execState0 + let ha = C.simHandleAllocator execCtx + parseResult <- C.top ng ha [] $ C.prog v + case parseResult of + Left err -> + pure (C.ExecutionFeatureNoChange, Resp.UserError (Resp.LoadSyntaxError (PP.pretty err))) + Right (C.ParsedProgram{ C.parsedProgCFGs = cfgs }) -> do + let binds = execState0 Lens.^. Lens.to C.execStateContext . C.functionBindings . Lens.to C.fnBindings + let binds' = foldl (\bs (C.Reg.AnyCFG c) -> insertCfg c bs) binds cfgs + let execState = modifySimContext (\c -> c Lens.& C.functionBindings Lens..~ C.FnBindings binds') execState0 + let featRes = C.ExecutionFeatureModifiedState execState + pure (featRes, Resp.Load path (length cfgs)) + +prove :: + (sym ~ W4.ExprBuilder t st fs) => + C.IsSymBackend sym bak => + bak -> + IO (Response cExt) +prove bak = do + let sym = C.backendGetSym bak + -- TODO(#270?): Configurable timeout + let timeout = CTO.Timeout (Sec.secondsFromInt 5) + -- TODO(#266): Configurable prover + W4.extendConfig W4.z3Options (W4.getConfiguration sym) + let prover = Prove.offlineProver timeout sym W4.defaultLogData W4.z3Adapter + let strat = Prove.ProofStrategy prover Prove.keepGoing + let convertResult = + \case + Prove.Proved {} -> Resp.Proved + Prove.Disproved {} -> Resp.Disproved + Prove.Unknown {} -> Resp.Unknown + let printer = Prove.ProofConsumer $ \goal res -> do + doc <- C.ppProofObligation sym goal + pure (Seq.fromList [(doc, convertResult res)]) + runExceptT (Prove.proveCurrentObligations bak strat printer) >>= + \case + Left CTO.TimedOut -> pure Resp.ProveTimeout + Right results -> pure (Resp.Prove results) + +-- TODO: Support taking a function or block name +reg :: + forall p sym ext r t cExt. + W4.IsExpr (W4.SymExpr sym) => + Context cExt p sym ext t -> + C.ExecState p sym ext r -> + [Int] -> + IO (Response cExt) +reg ctx execState idxs = + case execStateSimState execState of + Left notApplicable -> pure (Resp.UserError (Resp.NotApplicable notApplicable)) + Right (C.SomeSimState simState) -> do + let fr = simState Lens.^. C.stateTree . C.actFrame . C.gpValue + let regs :: Maybe (C.Some (C.RegMap sym)) + regs = + case fr of + C.OF ovFrame -> + Just (C.Some (ovFrame Lens.^. C.overrideRegMap)) + C.MF callFrame -> + Just (C.Some (callFrame Lens.^. C.frameRegs)) + C.RF {} -> + Nothing + case regs of + Nothing -> pure (Resp.UserError (Resp.NotApplicable Resp.NoFrame)) + Just (C.Some (C.RegMap rs)) -> do + let sz = Ctx.size rs + let mIdxs = + if List.null idxs + then Right (toListFC Some (Ctx.generate sz id)) -- all indices + else traverse (\i -> maybeToEither i (Ctx.intIndex i sz)) idxs + let ppArg (C.Some idx) = + let C.RegEntry ty val = rs Lens.^. ixF' idx in + ppRegVal (Ctxt.dbgPpIntrinsic ctx) ty (C.RV val) + case mIdxs of + Left i -> pure (Resp.UserError (Resp.NoSuchArgument i)) + Right idxs' -> pure (Resp.Arg (PP.vcat (List.map ppArg idxs'))) + where + maybeToEither :: e -> Maybe a -> Either e a + maybeToEither e = + \case + Nothing -> Left e + Just a -> Right a + +secret :: + PP.Pretty cExt => + Context cExt p sym ext t -> + C.ExecState p sym ext r -> + Rgx.Match (Arg.Arg cExt) BCmd.SecretRegex -> + IO (Resp.Response cExt) +secret ctx execState m = + let cExt = Ctxt.dbgCommandExt ctx in + case m of + -- Show what sort of tab-completion should be provided by the UI + Rgx.MLeft (Rgx.MThen _complete (Rgx.MThen (Rgx.MLit (Arg.ACommand cmd)) (Rgx.MStar args0))) -> do + let args = map (\(Rgx.MLit (Arg.AText t)) -> Text.unpack t) args0 + let cEnv = Ctxt.toCompletionEnv ctx execState + let line = unwords (show (PP.pretty cmd) : map (filter (/= '_')) args) + -- Act like we are completing as if the user pressed TAB at the "_" + let cursor = Maybe.fromMaybe "_" (List.find ("_" `List.isSuffixOf`) args) + completions <- Complete.complete cEnv line (List.init cursor) + pure $ + Resp.Complete $ + case completions of + [] -> "No completions" + _ -> PP.vcat (List.map PP.pretty completions) + -- Show what sort of syntax-highlighting should be provided by the UI + Rgx.MRight (Rgx.MThen _secret (Rgx.MThen (Rgx.MLit (Arg.ACommand cmd)) (Rgx.MStar args0))) -> + let args = map (\(Rgx.MLit (Arg.AText t)) -> t) args0 in + case Cmd.regex cExt cmd of + Some rx -> + let sEnv = Ctxt.toStyleEnv ctx execState in + pure (Resp.Style (Style.runStyle sEnv (Style.style rx args))) + +source :: + Context cExt p sym ext t -> + FilePath -> + IO (Either X.IOException (Inputs (CompletionT cExt (StyleT cExt IO)) (Statement cExt))) +source ctx path = do + let cExt = Ctxt.dbgCommandExt ctx + eTxt <- liftIO (X.try (IO.readFile path)) + case eTxt of + Left ioErr -> pure (Left ioErr) + Right txt -> do + let lns = Text.lines txt + let cmds = traverse (Stmt.parse cExt) lns + case cmds of + Left err -> do + Outps.send (Ctxt.dbgOutputs ctx) (Resp.UserError (Resp.SourceParseError err)) + pure (Right (Ctxt.dbgInputs ctx)) + Right stmts -> Right <$> Inps.prepend stmts (Ctxt.dbgInputs ctx) + +usage :: + PP.Pretty cExt => + Cmd.CommandExt cExt -> + Cmd.Command cExt -> + PP.Doc ann +usage cExt cmd = + case Cmd.regex cExt cmd of + Some rx -> PP.vcat (map (PP.pretty cmd PP.<+>) (Arg.usage rx)) diff --git a/src/Lang/Crucible/Debug/Complete.hs b/src/Lang/Crucible/Debug/Complete.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug/Complete.hs @@ -0,0 +1,219 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeApplications #-} + +module Lang.Crucible.Debug.Complete + ( CompletionEnv(..) + , CompletionT + , runCompletionT + , runCompletion + , runCompletionM + , CompletionType(..) + , Completions(..) + , complete + ) where + +import Control.Lens qualified as Lens +import Control.Monad qualified as Monad +import Control.Monad.IO.Class (MonadIO) +import Control.Monad.Reader (MonadReader, ReaderT) +import Control.Monad.Reader qualified as Reader +import Control.Monad.Trans (MonadTrans) +import Control.Exception qualified as X +import Data.Foldable (toList) +import Data.Function ((&)) +import Data.Functor ((<&>)) +import Data.Functor.Identity (Identity, runIdentity) +import Data.List qualified as List +import Data.Map.Strict qualified as Map +import Data.Maybe qualified as Maybe +import Data.Parameterized.Some (Some(Some), viewSome) +import Data.Parameterized.SymbolRepr (symbolRepr) +import Data.Set (Set) +import Data.Text qualified as Text +import Data.Text (Text) +import Lang.Crucible.Debug.Arg qualified as Arg +import Lang.Crucible.Debug.Arg.Type (ArgTypeRepr) +import Lang.Crucible.Debug.Arg.Type qualified as AType +import Lang.Crucible.Debug.Breakpoint qualified as Break +import Lang.Crucible.Debug.Breakpoint (Breakpoint) +import Lang.Crucible.Debug.Command (CommandExt) +import Lang.Crucible.Debug.Command qualified as Cmd +import Lang.Crucible.FunctionHandle qualified as C +import Lang.Crucible.Simulator.ExecutionTree qualified as C +import Prettyprinter qualified as PP +import System.Directory qualified as Dir +import System.FilePath qualified as FilePath +import What4.FunctionName qualified as W4 + +data CompletionEnv cExt + = forall p sym ext r. + CompletionEnv + { envBreakpoints :: Set Breakpoint + , envCommandExt :: CommandExt cExt + , envState :: C.ExecState p sym ext r + } + +newtype CompletionT cExt m a + = CompletionT { runCompletionT :: ReaderT (CompletionEnv cExt) m a } + deriving (Applicative, Functor, Monad, MonadFail, MonadIO, MonadReader (CompletionEnv cExt), MonadTrans) + +-- | Run 'CompletionT' over 'Identity' +runCompletion :: CompletionEnv cExt -> CompletionT cExt Identity a -> a +runCompletion env s = runIdentity (Reader.runReaderT (runCompletionT s) env) + +-- | Run 'CompletionT' over another monad +-- +-- This is kind of poorly named, but I can\'t think of a better name... +runCompletionM :: CompletionEnv cExt -> CompletionT cExt m a -> m a +runCompletionM env s = Reader.runReaderT (runCompletionT s) env + +data CompletionType + = CBreakpoint + | CCommand + | CExactly Text + | CFunction + | CPath + deriving (Eq, Show) + +instance PP.Pretty CompletionType where + pretty = + \case + CBreakpoint -> "breakpoint" + CCommand -> "command" + CExactly t -> PP.pretty t + CFunction -> "function" + CPath -> "path" + +completionType :: ArgTypeRepr t -> Maybe CompletionType +completionType = + \case + AType.TBreakpointRepr -> Just CBreakpoint + AType.TCommandRepr -> Just CCommand + AType.TExactlyRepr s -> Just (CExactly (symbolRepr s)) + AType.TFunctionRepr -> Just CFunction + AType.TIntRepr -> Nothing + AType.TPathRepr -> Just CPath + AType.TTextRepr -> Nothing + +commandsWithPrefix :: + CompletionEnv cExt -> + -- | Prefix + String -> + [String] +commandsWithPrefix cEnv pfx = filter (pfx `List.isPrefixOf`) allCmdNames + where + allCmdNames :: [String] + allCmdNames = + let cExts = envCommandExt cEnv in + map (Text.unpack . Cmd.name cExts) (Cmd.allCmds cExts) + +completePath :: FilePath -> IO [String] +completePath path = + if List.null path + then Dir.listDirectory =<< Dir.getCurrentDirectory + else do + isDir <- Dir.doesDirectoryExist path + if isDir && not (FilePath.hasTrailingPathSeparator path) + then pure [FilePath.addTrailingPathSeparator path] + else do + let dir = FilePath.addTrailingPathSeparator (FilePath.takeDirectory path) + contents <- Dir.listDirectory dir + let file = FilePath.takeFileName path + if List.null file + then pure (map (dir ++) contents) + else pure (map (dir ++) (filter (file `List.isPrefixOf`) contents)) + +completionsForType :: + CompletionEnv cExt -> + -- | Prefix + String -> + CompletionType -> + IO [String] +completionsForType cEnv pfx = + \case + CBreakpoint -> + pure $ + toList (envBreakpoints cEnv) & + map Break.toText & + filter (Text.pack pfx `Text.isPrefixOf`) & + map Text.unpack + CCommand -> pure (commandsWithPrefix cEnv pfx) + CExactly s -> + let s' = Text.unpack s in + pure (if pfx `List.isPrefixOf` s' then [s'] else []) + CFunction -> do + CompletionEnv { envState = execState } <- pure cEnv + let binds = execState Lens.^. Lens.to C.execStateContext . C.functionBindings + let hdls = C.handleMapToHandles (C.fnBindings binds) + pure (map (\(C.SomeHandle hdl) -> Text.unpack (W4.functionName (C.handleName hdl))) hdls) + CPath -> + X.try @X.IOException (completePath pfx) <&> + \case + Left _ -> [] + Right cs -> cs + +data Completions + = Completions + { completionsType :: CompletionType + , completions :: [String] + } + +-- | Used in the test suite with @. complete@ +instance PP.Pretty Completions where + pretty (Completions ty cs) = do + let def = + if null cs + then PP.pretty ty + else + PP.pretty ty PP.<> ":" PP.<+> PP.hsep (PP.punctuate "," (map PP.pretty cs)) + case ty of + CBreakpoint -> def + CCommand -> PP.pretty ty + CExactly {} -> + if null cs + then PP.pretty ty PP.<+> "(x)" + else PP.pretty ty + CFunction {} -> def + CPath -> def + +complete :: + CompletionEnv cExt -> + -- | Whole line + String -> + -- | Word being completed + String -> + IO [Completions] +complete cEnv input word = + case words input of + [] -> pure [Completions CCommand allCmdNames] + [_] | not (null word) -> + pure [Completions CCommand (commandsWithPrefix cEnv word)] + (c : args) -> do + case Cmd.parse cExts (Text.pack c) of + Just cmd -> + case Cmd.regex cExts cmd of + Some rx -> do + let (allTypes, next) = Arg.types cExts rx (map Text.pack args) + let types = + case Map.lookup (Text.pack word) allTypes of + Nothing -> next + Just ts -> ts + let cTypes = Maybe.mapMaybe (viewSome completionType) (toList types) + Monad.mapM (\t -> Completions t <$> completionsForType cEnv word t) cTypes + Nothing -> pure [] + where + cExts = envCommandExt cEnv + + allCmdNames :: [String] + allCmdNames = map (Text.unpack . Cmd.name cExts) (Cmd.allCmds cExts) diff --git a/src/Lang/Crucible/Debug/Context.hs b/src/Lang/Crucible/Debug/Context.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug/Context.hs @@ -0,0 +1,168 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE TypeApplications #-} + +module Lang.Crucible.Debug.Context + ( RunningState(..) + , DebuggerState(..) + , CommandImpl(..) + , ExtImpl(..) + , voidImpl + , EvalResult(..) + , Context(..) + , initCtx + , toCompletionEnv + , toStyleEnv + ) where + +import Data.Parameterized.NatRepr (knownNat) +import Data.Set qualified as Set +import Data.Set (Set) +import Data.Void (Void, absurd) +import Lang.Crucible.Debug.Arg qualified as Arg +import Lang.Crucible.Debug.Arg.Type qualified as AType +import Lang.Crucible.Debug.Breakpoint (Breakpoint) +import Lang.Crucible.Debug.Command (CommandExt) +import Lang.Crucible.Debug.Complete (CompletionT, CompletionEnv) +import Lang.Crucible.Debug.Complete qualified as Complete +import Lang.Crucible.Debug.Inputs (Inputs) +import Lang.Crucible.Debug.Outputs (Outputs) +import Lang.Crucible.Debug.Regex qualified as Rgx +import Lang.Crucible.Debug.Response (Response) +import Lang.Crucible.Debug.Statement (Statement) +import Lang.Crucible.Debug.Style qualified as Style +import Lang.Crucible.Debug.Style (StyleT, StyleEnv) +import Lang.Crucible.Debug.Trace (Trace) +import Lang.Crucible.Debug.Trace qualified as Trace +import Lang.Crucible.Pretty (IntrinsicPrinters) +import Lang.Crucible.Simulator.EvalStmt qualified as C +import Lang.Crucible.Simulator qualified as C +import Lang.Crucible.Types (TypeRepr) +import What4.Interface qualified as W4 + +data RunningState + = -- | User issued 'Cmd.Finish' + Finish + -- | User issued 'Cmd.Run' + | Run + -- | User issued 'Cmd.Step' + | Step {-# UNPACK #-} !Int + +data DebuggerState + = Running RunningState + -- | User issued 'Cmd.Quit' + | Quit + | Stopped + +data CommandImpl cExt p sym ext t + = forall r. + CommandImpl + { -- | A regular expression describing what kinds of arguments this command + -- takes. See "Lang.Crucible.Debug.Regex". + implRegex :: Rgx.RegexRepr AType.ArgTypeRepr r + -- | The implementation of the command, taking the arguments that result + -- from matching 'implRegex' against the command line provided by the + -- user. + , implBody :: + Context cExt p 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) + } + +newtype ExtImpl cExt p sym ext t + = ExtImpl { getExtImpl :: cExt -> CommandImpl cExt p sym ext t } + +voidImpl :: ExtImpl Void p sym ext t +voidImpl = ExtImpl absurd + +-- | The result of evaluating a 'Statement' +data EvalResult cExt p sym ext t + = EvalResult + { evalCtx :: Context cExt p sym ext t + , evalFeatureResult :: C.ExecutionFeatureResult p sym ext (C.RegEntry sym t) + , evalResp :: Response cExt + } + +-- | 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). +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 + } + +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 + t <- Trace.empty (knownNat @512) -- arbitrary max size + pure $ + Context + { dbgBreakpoints = Set.empty + , dbgCommandExt = cExts + , dbgExtImpl = impl + , dbgInputs = ins + , dbgOutputs = outs + , dbgPpIntrinsic = iFns + , dbgRetTy = rTy + , dbgState = Stopped + , dbgStopOnAbort = False + , dbgTrace = t + } + +toCompletionEnv :: + Context cExt p sym ext t -> + C.ExecState p sym ext r -> + CompletionEnv cExt +toCompletionEnv ctxt execState = + Complete.CompletionEnv + { Complete.envBreakpoints = dbgBreakpoints ctxt + , Complete.envCommandExt = dbgCommandExt ctxt + , Complete.envState = execState + } + +toStyleEnv :: + Context cExt p sym ext t -> + C.ExecState p sym ext r -> + StyleEnv cExt +toStyleEnv ctxt execState = + Style.StyleEnv + { Style.envBreakpoints = dbgBreakpoints ctxt + , Style.envCommandExt = dbgCommandExt ctxt + , Style.envState = execState + } diff --git a/src/Lang/Crucible/Debug/Eval.hs b/src/Lang/Crucible/Debug/Eval.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug/Eval.hs @@ -0,0 +1,335 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImplicitParams #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE TypeOperators #-} + +module Lang.Crucible.Debug.Eval + ( Ctxt.EvalResult(..) + , eval + ) where + +import Control.Lens qualified as Lens +import Data.Maybe qualified as Maybe +import Data.Set qualified as Set +import Data.Text qualified as Text +import Lang.Crucible.Backend qualified as C +import Lang.Crucible.CFG.Extension qualified as C +import Lang.Crucible.Debug.Arg qualified as Arg +import Lang.Crucible.Debug.Breakpoint (Breakpoint(BreakFunction)) +import Lang.Crucible.Debug.Command.Base qualified as BCmd +import Lang.Crucible.Debug.Command qualified as Cmd +import Lang.Crucible.Debug.Commands qualified as Cmds +import Lang.Crucible.Debug.Context (Context) +import Lang.Crucible.Debug.Context qualified as Ctxt +import Lang.Crucible.Debug.Regex qualified as Rgx +import Lang.Crucible.Debug.Response qualified as Resp +import Lang.Crucible.Debug.Statement qualified as Stmt +import Lang.Crucible.Debug.Statement (Statement) +import Lang.Crucible.Debug.Trace qualified as Trace +import Lang.Crucible.Simulator.EvalStmt qualified as C +import Lang.Crucible.Simulator.ExecutionTree qualified as C +import Lang.Crucible.Simulator qualified as C +import Lang.Crucible.Syntax.Concrete qualified as C +import Prettyprinter qualified as PP +import What4.Expr.Builder qualified as W4 +import What4.Interface qualified as W4 + +runCmd :: + Context cExt p sym ext t -> + C.ExecState p sym ext (C.RegEntry sym t) -> + Ctxt.RunningState -> + IO (Ctxt.EvalResult cExt p sym ext t) +runCmd ctx execState runState = + case execState of + C.ResultState {} -> + let resp = Resp.UserError (Resp.NotApplicable Resp.DoneSimulating) in + pure (def ctx) { Ctxt.evalResp = resp } + _ -> 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 ctx = Ctxt.EvalResult ctx C.ExecutionFeatureNoChange Resp.Ok + +baseImpl :: + (sym ~ W4.ExprBuilder s st fs) => + C.IsSymInterface sym => + C.IsSyntaxExtension ext => + (?parserHooks :: C.ParserHooks ext) => + PP.Pretty cExt => + W4.IsExpr (W4.SymExpr sym) => + BCmd.BaseCommand -> + Ctxt.CommandImpl cExt p sym ext t +baseImpl = + \case + BCmd.Backtrace -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rBacktrace + , Ctxt.implBody = \ctx execState Rgx.MEmpty -> do + resp <- Cmds.backtrace execState + pure (def ctx) { Ctxt.evalResp = resp } + } + + BCmd.Block -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rBlock + , Ctxt.implBody = \ctx execState Rgx.MEmpty -> do + resp <- Cmds.block ctx execState + pure (def ctx) { Ctxt.evalResp = resp } + } + + BCmd.Break -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rBreak + , Ctxt.implBody = \ctx _execState (Rgx.MLit (Arg.AFunction fNm)) -> do + let bs = Set.insert (BreakFunction fNm) (Ctxt.dbgBreakpoints ctx) + pure (def ctx) { Ctxt.evalCtx = ctx { Ctxt.dbgBreakpoints = bs } } + } + + BCmd.Call -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rCall + , Ctxt.implBody = \ctx execState (Rgx.MLit (Arg.AFunction fNm)) -> do + (featRes, resp) <- Cmds.call execState (Ctxt.dbgRetTy ctx) fNm + pure (def ctx) { Ctxt.evalFeatureResult = featRes, Ctxt.evalResp = resp } + } + + BCmd.Cfg -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rCfg + , Ctxt.implBody = \ctx execState m -> + case m of + Rgx.MLeft Rgx.MEmpty -> do + resp <- Cmds.cfg execState Nothing + pure (def ctx) { Ctxt.evalResp = resp } + Rgx.MRight (Rgx.MLit (Arg.AFunction fNm)) -> do + (featRes, resp) <- Cmds.call execState (Ctxt.dbgRetTy ctx) fNm + pure (def ctx) { Ctxt.evalFeatureResult = featRes, Ctxt.evalResp = resp } + } + + BCmd.Clear -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rClear + , Ctxt.implBody = \ctx execState Rgx.MEmpty -> + C.withBackend (C.execStateContext execState) $ \bak -> do + n <- length <$> C.getProofObligations bak + C.clearProofObligations bak + pure (def ctx) { Ctxt.evalResp = Resp.Clear n } + } + + BCmd.Comment -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rComment + , Ctxt.implBody = \ctx _execState (Rgx.MStar _) -> pure (def ctx) + } + + BCmd.Delete -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rDelete + , Ctxt.implBody = \ctx _execState (Rgx.MLit (Arg.ABreakpoint bp@(BreakFunction fNm))) -> do + let bs0 = Ctxt.dbgBreakpoints ctx + let wasElem = Set.member bp bs0 + let bs = Set.delete bp bs0 + pure (def ctx) + { Ctxt.evalCtx = ctx { Ctxt.dbgBreakpoints = bs } + , Ctxt.evalResp = Resp.Delete fNm wasElem + } + } + + BCmd.Done -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rDone + , Ctxt.implBody = \ctx execState Rgx.MEmpty -> do + case execState of + C.ResultState {} -> + pure (def ctx) { Ctxt.evalCtx = ctx { Ctxt.dbgState = Ctxt.Quit } } + _ -> + let resp = Resp.UserError (Resp.NotApplicable Resp.NotDone) in + pure (def ctx) { Ctxt.evalResp = resp } + } + + BCmd.Frame -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rFrame + , Ctxt.implBody = \ctx execState Rgx.MEmpty -> do + resp <- Cmds.frame ctx execState + pure (def ctx) { Ctxt.evalResp = resp } + } + + BCmd.Finish -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rFinish + , Ctxt.implBody = \ctx execState Rgx.MEmpty -> + runCmd ctx execState Ctxt.Finish + } + + BCmd.Help -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rHelp + , Ctxt.implBody = \ctx _execState m -> + case m of + Rgx.MLeft Rgx.MEmpty -> + pure (def ctx) { Ctxt.evalResp = Cmds.help (Ctxt.dbgCommandExt ctx) Nothing } + Rgx.MRight (Rgx.MLit (Arg.ACommand cmd)) -> + pure (def ctx) { Ctxt.evalResp = Cmds.help (Ctxt.dbgCommandExt ctx) (Just cmd) } + + } + + BCmd.Load -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rLoad + , Ctxt.implBody = \ctx execState (Rgx.MLit (Arg.APath path)) -> do + (featRes, resp) <- Cmds.load execState (Text.unpack path) + pure (def ctx) { Ctxt.evalFeatureResult = featRes, Ctxt.evalResp = resp } + } + + BCmd.Location -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rLocation + , Ctxt.implBody = \ctx execState Rgx.MEmpty -> do + let stateCtx = C.execStateContext execState + let sym = stateCtx Lens.^. C.ctxSymInterface + loc <- W4.getCurrentProgramLoc sym + pure (def ctx) { Ctxt.evalResp = Resp.Location loc } + } + + BCmd.Obligation -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rObligation + , Ctxt.implBody = \ctx execState Rgx.MEmpty -> + C.withBackend (C.execStateContext execState) $ \bak -> do + obls <- C.getProofObligations bak + let goals = Maybe.fromMaybe [] (C.goalsToList <$> obls) + let sym = C.backendGetSym bak + prettyGoals <- mapM (C.ppProofObligation sym) goals + pure (def ctx) { Ctxt.evalResp = Resp.Obligation prettyGoals } + } + + BCmd.PathCondition -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rPathCondition + , Ctxt.implBody = \ctx execState Rgx.MEmpty -> + C.withBackend (C.execStateContext execState) $ \bak -> do + pathCond <- W4.printSymExpr <$> C.getPathCondition bak + pure (def ctx) { Ctxt.evalResp = Resp.PathCondition pathCond } + } + + BCmd.Prove -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rProve + , Ctxt.implBody = \ctx execState Rgx.MEmpty -> do + resp <- C.withBackend (C.execStateContext execState) Cmds.prove + pure (def ctx) { Ctxt.evalResp = resp } + } + + BCmd.Quit -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rQuit + , Ctxt.implBody = \ctx _execState Rgx.MEmpty -> + pure (def ctx) { Ctxt.evalCtx = ctx { Ctxt.dbgState = Ctxt.Quit } } + } + + BCmd.Register -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rRegister + , Ctxt.implBody = \ctx execState (Rgx.MStar ints) -> do + let ints' = map (\(Rgx.MLit (Arg.AInt i)) -> i) ints + resp <- Cmds.reg ctx execState ints' + pure (def ctx) { Ctxt.evalResp = resp } + } + + BCmd.Run -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rRun + , Ctxt.implBody = \ctx execState Rgx.MEmpty -> + runCmd ctx execState Ctxt.Run + } + + BCmd.Secret -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rSecret + , Ctxt.implBody = \ctx execState m -> do + resp <- Cmds.secret ctx execState m + pure (def ctx) { Ctxt.evalResp = resp } + } + + BCmd.Step -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rStep + , Ctxt.implBody = \ctx execState m -> do + let n = + case m of + Rgx.MLeft Rgx.MEmpty -> 1 + Rgx.MRight (Rgx.MLit (Arg.AInt i)) -> i + runCmd ctx execState (Ctxt.Step n) + } + + BCmd.Source -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rSource + , Ctxt.implBody = \ctx _execState (Rgx.MLit (Arg.APath path)) -> do + r <- Cmds.source ctx (Text.unpack path) + case r of + Left ioErr -> pure (def ctx) { Ctxt.evalResp = Resp.IOError ioErr } + Right inputs -> pure (def ctx) { Ctxt.evalCtx = ctx { Ctxt.dbgInputs = inputs } } + } + + BCmd.Trace -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rTrace + , Ctxt.implBody = \ctx _execState m -> do + let n = + case m of + Rgx.MLeft Rgx.MEmpty -> 2 + Rgx.MRight (Rgx.MLit (Arg.AInt i)) -> i + ents <- reverse <$> Trace.latest (Ctxt.dbgTrace ctx) n + pure (def ctx) { Ctxt.evalResp = Resp.Trace (map PP.pretty ents) } + } + + BCmd.Usage -> + Ctxt.CommandImpl + { Ctxt.implRegex = BCmd.rUsage + , Ctxt.implBody = \ctx _execState (Rgx.MLit (Arg.ACommand cmd)) -> + pure (def ctx) { Ctxt.evalResp = Resp.Usage (Cmds.usage (Ctxt.dbgCommandExt ctx) cmd) } + } + +cmdImpl :: + (sym ~ W4.ExprBuilder s st fs) => + C.IsSymInterface sym => + C.IsSyntaxExtension ext => + (?parserHooks :: C.ParserHooks ext) => + PP.Pretty cExt => + W4.IsExpr (W4.SymExpr sym) => + Context cExt p sym ext t -> + Cmd.Command cExt -> + Ctxt.CommandImpl cExt p sym ext t +cmdImpl ctx cmd = + case cmd of + Cmd.Base bCmd -> baseImpl bCmd + Cmd.Ext xCmd -> Ctxt.getExtImpl (Ctxt.dbgExtImpl ctx) xCmd + +eval :: + (sym ~ W4.ExprBuilder s st fs) => + C.IsSymInterface sym => + C.IsSyntaxExtension ext => + (?parserHooks :: C.ParserHooks ext) => + PP.Pretty cExt => + W4.IsExpr (W4.SymExpr sym) => + Context 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 = + 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 + Ctxt.CommandImpl { Ctxt.implRegex = r, Ctxt.implBody = f } -> + case Arg.match (Arg.convert (Ctxt.dbgCommandExt ctx) r) args of + Left e -> pure (argError e) + Right m -> f ctx execState m diff --git a/src/Lang/Crucible/Debug/Inputs.hs b/src/Lang/Crucible/Debug/Inputs.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug/Inputs.hs @@ -0,0 +1,165 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TypeApplications #-} + +module Lang.Crucible.Debug.Inputs + ( Inputs + , recv + , fail + , parseInputs + , parseInputsWithRetry + , addPrompt + , prepend + , defaultDebuggerInputs + ) where + +import Control.Monad.IO.Class (MonadIO, liftIO) +import Control.Monad qualified as Monad +import Control.Monad.Reader qualified as Reader +import Control.Monad.Trans (MonadTrans(lift)) +import Data.Char qualified as Char +import Data.Functor.Contravariant (contramap) +import Data.IORef qualified as IORef +import Data.Text.IO qualified as IO +import Data.Text qualified as Text +import Data.Text (Text) +import Lang.Crucible.Debug.Command (CommandExt) +import Lang.Crucible.Debug.Complete (CompletionT) +import Lang.Crucible.Debug.Complete qualified as Complete +import Lang.Crucible.Debug.Outputs (Outputs) +import Lang.Crucible.Debug.Outputs qualified as Outs +import Lang.Crucible.Debug.Statement qualified as Stmt +import Lang.Crucible.Debug.Statement (Statement, ParseError, renderParseError) +import Lang.Crucible.Debug.Style qualified as Style +import Lang.Crucible.Debug.Style (StyleT) +import Prelude hiding (fail) +import System.Console.Isocline qualified as Isocline +import System.IO (Handle, hFlush, stdout) + +newtype Inputs m a = Inputs { recv :: m a } + deriving (Applicative, Functor, Monad) + +instance MonadFail m => MonadFail (Inputs m) where + fail = Inputs . Monad.fail + +instance MonadIO m => MonadIO (Inputs m) where + liftIO = Inputs . liftIO + +instance MonadTrans Inputs where + lift = Inputs + +fail :: MonadFail m => Inputs m a +fail = Monad.fail "No more inputs" + +addPrompt :: Handle -> Text -> Inputs IO a -> Inputs IO a +addPrompt hOut prompt (Inputs inps) = + Inputs $ do + IO.hPutStr hOut prompt + hFlush hOut + inps + +prepend :: MonadIO m => [a] -> Inputs m a -> IO (Inputs m a) +prepend inps (Inputs rest) = do + inpsRef <- IORef.newIORef inps + pure (Inputs (go inpsRef)) + where + go inpsRef = do + is <- liftIO (IORef.readIORef inpsRef) + case is of + [] -> rest + (i:is') -> do + liftIO (IORef.writeIORef inpsRef is') + pure i + +parseInputs :: + MonadFail m => + CommandExt cExt -> + Inputs m Text -> + Inputs m (Statement cExt) +parseInputs cExts (Inputs inps) = Inputs go + where + go = do + txt <- inps + case Stmt.parse cExts txt of + Left err -> Monad.fail (show err) + Right r -> pure r + +parseInputsWithRetry :: + Monad m => + CommandExt cExt -> + Inputs m Text -> + Outputs m ParseError -> + Inputs m (Statement cExt) +parseInputsWithRetry cExts (Inputs inps) errs = Inputs go + where + go = do + txt <- inps + case Stmt.parse cExts txt of + Left err -> do + Outs.send errs err + go + Right r -> pure r + +-- NOTE(lb): AFAIK, this only needs to be done once per process, not once per +-- debugger initialization. These settings probably persist no matter how many +-- times different debuggers (or defaultDebuggerInputs) are created. +initIsocline :: IO () +initIsocline = do + _ <- Isocline.enableAutoTab True + Isocline.setHistory ".crucible-debug" 512 + +-- | Like 'Isocline.completeWord', but allow IO. +-- +-- Implementation copied from 'Isocline.completeWord'. +completeWordIO :: + Isocline.CompletionEnv -> + String -> + Maybe (Char -> Bool) -> + (String -> IO [Isocline.Completion]) -> + IO () +completeWordIO cenv input isWordChar completer = + Isocline.completeWordPrim cenv input isWordChar cenvCompleter + where + cenvCompleter ce i = do + completes <- completer i + _ <- Isocline.addCompletions ce completes + return () + +readIsocline :: MonadIO m => CompletionT cExt (StyleT cExt m) String +readIsocline = do + let extraPrompt = "" -- prompt will be "> " + styleEnv <- lift Reader.ask + completionEnv <- Reader.ask + let completer :: Isocline.CompletionEnv -> String -> IO () + completer cEnv input = do + let isWordChar = Just (not . Char.isSpace) + let completeWord w = + mconcat . map Complete.completions <$> + Complete.complete completionEnv input w + let wordCompleter = fmap (map Isocline.completion) . completeWord + completeWordIO cEnv input isWordChar wordCompleter + liftIO $ + Isocline.readlineEx + extraPrompt + (Just completer) + (Just (Style.runStyle styleEnv . Style.highlighter)) + +defaultDebuggerInputs :: + MonadIO m => + CommandExt cExt -> + IO (Inputs (CompletionT cExt (StyleT cExt m)) (Statement cExt)) +defaultDebuggerInputs cExts = do + initIsocline + pure $ + parseInputsWithRetry + cExts + (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 new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug/Outputs.hs @@ -0,0 +1,56 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE OverloadedStrings #-} + +module Lang.Crucible.Debug.Outputs + ( Outputs + , send + , lift + , accumulate + , hPutStrLn + , pretty + , defaultDebuggerOutputs + ) where + +import Data.Functor.Contravariant (Contravariant(..)) +import Data.IORef (IORef) +import Data.IORef qualified as IORef +import Data.Text (Text) +import Data.Text.IO qualified as IO +import Lang.Crucible.Debug.Response (Response, ResponseExt) +import Prettyprinter qualified as PP +import Prettyprinter.Render.Text qualified as PP +import System.IO (Handle, stdout) + +newtype Outputs m a = Outputs { send :: a -> m () } + +instance Contravariant (Outputs m) where + contramap f (Outputs o) = Outputs (o . f) + +lift :: (n () -> m ()) -> Outputs n a -> Outputs m a +lift f (Outputs s) = Outputs (f . s) + +accumulate :: IORef [a] -> Outputs IO a +accumulate r = Outputs (IORef.modifyIORef r . (:)) + +hPutStrLn :: Handle -> Outputs IO Text +hPutStrLn hOut = Outputs (IO.hPutStrLn hOut) + +pretty :: + PP.Pretty a => + Handle -> + PP.LayoutOptions -> + Outputs IO a +pretty 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 diff --git a/src/Lang/Crucible/Debug/Regex.hs b/src/Lang/Crucible/Debug/Regex.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug/Regex.hs @@ -0,0 +1,412 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Lang.Crucible.Debug.Regex + ( type Regex + , type Empty + , type Lit + , type (:|) + , type Then + , type Star + , RegexRepr(..) + , AcceptsEmpty + , acceptsEmpty + , DerivativeResult(..) + , derivative + , Match(..) + , MatchError(..) + , TokenParser(..) + , match + , nextLits + , liftOrs + , Sugar(..) + , sugar + , prettySugar + ) where + +import Data.Bifunctor (first) +import Data.Foldable qualified as Foldable +import Data.Kind (Type) +import Data.Parameterized.BoolRepr (BoolRepr (..), (%||), (%&&)) +import Data.Parameterized.Classes (KnownRepr(knownRepr)) +import Data.Parameterized.Some (Some (Some)) +import Data.Parameterized.TraversableFC qualified as TFC +import Data.Sequence qualified as Seq +import Data.Sequence (Seq) +import Data.Type.Bool (type (||), type (&&)) +import Data.Type.Equality (TestEquality (testEquality), type (:~:)(Refl)) +import Prettyprinter qualified as PP + +-- | Type-level only +data Regex a + = TFail + | TEmpty + | TLit a + | TOr (Regex a) (Regex a) + | TThen (Regex a) (Regex a) + | TStar (Regex a) + +type Empty = 'TEmpty +type Lit = 'TLit +type a :| b = 'TOr a b +type Then = 'TThen +type Star = 'TStar + +-- | 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'. +type RegexRepr :: (k -> Type) -> Regex k -> Type +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) + +instance TestEquality f => TestEquality (RegexRepr f) where + testEquality rgx rgx' = + case (rgx, rgx') of + (Empty, Empty) -> Just Refl + (Empty, _) -> Nothing + (Fail, Fail) -> Just Refl + (Fail, _) -> Nothing + (Lit l, Lit l') -> + case testEquality l l' of + Just Refl -> Just Refl + Nothing -> Nothing + (Lit {}, _) -> Nothing + (Or l r, Or l' r') -> + case (testEquality l l', testEquality r r') of + (Just Refl, Just Refl) -> Just Refl + _ -> Nothing + (Or {}, _) -> Nothing + (Star r, Star r') -> + case testEquality r r' of + Just Refl -> Just Refl + Nothing -> Nothing + (Star {}, _) -> Nothing + (Then l r, Then l' r') -> + case (testEquality l l', testEquality r r') of + (Just Refl, Just Refl) -> Just Refl + _ -> Nothing + (Then {}, _) -> Nothing + +instance KnownRepr (RegexRepr f) 'TEmpty where + knownRepr = Empty + +instance KnownRepr (RegexRepr f) 'TFail where + knownRepr = Fail + +instance KnownRepr f t => KnownRepr (RegexRepr f) ('TLit t) where + knownRepr = Lit knownRepr + +instance + ( KnownRepr (RegexRepr f) l + , KnownRepr (RegexRepr f) r + ) => KnownRepr (RegexRepr f) ('TOr l r) where + knownRepr = Or knownRepr knownRepr + +instance + ( KnownRepr (RegexRepr f) l + , KnownRepr (RegexRepr f) r + ) => KnownRepr (RegexRepr f) ('TThen l r) where + knownRepr = Then knownRepr knownRepr + +instance KnownRepr (RegexRepr f) r => KnownRepr (RegexRepr f) ('TStar r) where + knownRepr = Star knownRepr + +instance TFC.FunctorFC RegexRepr where + fmapFC f = + \case + Empty -> Empty + Fail -> Fail + Lit l -> Lit (f l) + Or l r -> Or (TFC.fmapFC f l) (TFC.fmapFC f r) + Star r -> Star (TFC.fmapFC f r) + Then l r -> Then (TFC.fmapFC f l) (TFC.fmapFC f r) + +instance TFC.FoldableFC RegexRepr where + foldMapFC f = + \case + Empty -> mempty + Fail -> mempty + Lit l -> f l + Or l r -> TFC.foldMapFC f l <> TFC.foldMapFC f r + Star r -> TFC.foldMapFC f r + Then l r -> TFC.foldMapFC f l <> TFC.foldMapFC f r + +instance TFC.TraversableFC RegexRepr where + traverseFC f = + \case + Empty -> pure Empty + Fail -> pure Fail + Lit l -> Lit <$> f l + Or l r -> Or <$> TFC.traverseFC f l <*> TFC.traverseFC f r + Star r -> Star <$> TFC.traverseFC f r + Then l r -> Then <$> TFC.traverseFC f l <*> TFC.traverseFC f r + +type AcceptsEmpty :: Regex k -> Bool +type family AcceptsEmpty r where + AcceptsEmpty 'TFail = 'False + AcceptsEmpty 'TEmpty = 'True + AcceptsEmpty ('TLit _) = 'False + AcceptsEmpty ('TOr l r) = AcceptsEmpty l || AcceptsEmpty r + AcceptsEmpty ('TThen l r) = AcceptsEmpty l && AcceptsEmpty r + AcceptsEmpty ('TStar r) = 'True + +acceptsEmpty :: RegexRepr f r -> BoolRepr (AcceptsEmpty r) +acceptsEmpty = + \case + Empty -> TrueRepr + Fail -> FalseRepr + Lit {} -> FalseRepr + Or l r -> acceptsEmpty l %|| acceptsEmpty r + Star _ -> TrueRepr + Then l r -> acceptsEmpty l %&& acceptsEmpty r + +-- | Type-level version of 'nu'. +-- +-- See Wikipedia on "Brzozowski derivative" +type Nu :: Regex k -> Regex k +type family Nu r where + Nu 'TFail = 'TFail + Nu 'TEmpty = 'TEmpty + Nu ('TLit _) = 'TFail + Nu ('TOr l r) = 'TOr (Nu l) (Nu r) + Nu ('TThen l r) = 'TThen (Nu l) (Nu r) + Nu ('TStar r) = 'TEmpty + +-- | Auxiliary function for 'derivative'. +-- +-- Value-level version of 'Nu'. +-- +-- See Wikipedia on "Brzozowski derivative" +nu :: RegexRepr f r -> RegexRepr f (Nu r) +nu = + \case + Empty -> Empty + Fail -> Fail + Lit {} -> Fail + Or l r -> Or (nu l) (nu r) + Star _ -> Empty + Then l r -> Then (nu l) (nu r) + +-- | The result of 'derivative' +data DerivativeResult f g + = DerivativeResult + { -- | The remaining regex after matching that token + derivativeRegex :: Some (RegexRepr f) + -- | All the literals the token was matched at + , derivativeMatched :: Seq (Some g) + } + +-- | See Wikipedia on "Brzozowski derivative" +derivative :: + (forall t. f t -> TokenParser tok e g t) -> + tok -> + RegexRepr f r -> + DerivativeResult f g +derivative getParser tok = + let noMatch r = DerivativeResult r Seq.empty in + let doFail = noMatch (Some Fail) in + \case + Empty -> doFail + Fail -> doFail + Lit f -> + case runTokenParser (getParser f) tok of + Left _ -> doFail + Right m -> DerivativeResult (Some Empty) (Seq.singleton (Some m)) + Or l r -> + case (derivative getParser tok l, derivative getParser tok r) of + (DerivativeResult (Some Fail) _, r') -> r' + (l', DerivativeResult (Some Fail) _) -> l' + (DerivativeResult (Some l') ms, DerivativeResult (Some r') ms') -> + DerivativeResult (Some (Or l' r')) (ms <> ms') + Star f -> + case derivative getParser tok f of + DerivativeResult (Some f') ms -> + DerivativeResult (Some (Then f' (Star f))) ms + Then l r -> + case (derivative getParser tok l, derivative getParser tok r) of + (DerivativeResult (Some l') ms, DerivativeResult (Some r') ms') -> + DerivativeResult (Some (Or (Then l' r) (Then (nu l) r'))) (ms <> ms') + +-- | The result of 'match', in case of success +type Match :: (k -> Type) -> Regex k -> Type +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) + +-- | Failures that may arise during 'match' +data MatchError tok e + = EFail + | Eof + | EOr (MatchError tok e) (MatchError tok e) + | NotEmpty [tok] + | Token e + deriving Show + +instance (PP.Pretty e, PP.Pretty tok) => PP.Pretty (MatchError tok e) where + pretty = + \case + EFail -> "This regular expression never matches" + Eof -> "Unexpected end of input" + EOr l r -> + PP.vcat + [ "Both branches failed to match:" + , "-" PP.<+> PP.align (PP.pretty l) + , "-" PP.<+> PP.align (PP.pretty r) + ] + NotEmpty toks -> + "Expected end of input, but found:" PP.<+> PP.hsep (map PP.pretty toks) + Token e -> PP.pretty e + +type TokenParser :: Type -> Type -> (k -> Type) -> k -> Type +newtype TokenParser tok e f t + = TokenParser { runTokenParser :: tok -> Either e (f t) } + +-- | Match a regular expression against a token stream +match :: + -- | Regex + RegexRepr (TokenParser tok e g) r -> + -- | Token stream + [tok] -> + -- | Either a 'MatchError', or a 'Match' plus the unconsumed tokens + Either (MatchError tok e) (Match g r, [tok]) +match rgx toks = + case (rgx, toks) of + (Fail, _) -> Left EFail + (Empty, []) -> Right (MEmpty, toks) + (Empty, _) -> Left (NotEmpty toks) + (Lit _, []) -> Left Eof + (Lit ft, t : ts) -> do + m <- first Token (runTokenParser ft t) + pure (MLit m, ts) + (Then l r, ts) -> do + (ml, ts') <- match l ts + (mr, ts'') <- match r ts' + pure (MThen ml mr, ts'') + (Or l r, ts) -> + case match l ts of + Right (m, ts') -> Right (MLeft m, ts') + Left ef -> + case match r ts of + Right (m, ts') -> pure (MRight m, ts') + Left eg -> Left (EOr ef eg) + (Star f, ts) -> + case match f ts of + Left _ -> Right (MStar [], ts) + Right (m, ts') -> + first (\(MStar ms) -> MStar (m : ms)) <$> match (Star f) ts' + +-- | List the literals that could be matched next +nextLits :: RegexRepr f r -> Seq (Some f) +nextLits = + \case + Empty -> Seq.empty + Fail -> Seq.empty + Lit x -> Seq.singleton (Some x) + Or l r -> nextLits l <> nextLits r + Star r -> nextLits r + Then l r -> + case acceptsEmpty l of + TrueRepr -> nextLits l <> nextLits r + FalseRepr -> nextLits l + +-- | Syntactic sugar for displaying 'RegexRepr's, especially for quantification +type Sugar :: (k -> Type) -> Regex k -> Type +data Sugar f r where + SEmpty :: Sugar f 'TEmpty + SFail :: Sugar f 'TFail + SLit :: f t -> Sugar f ('TLit t) + SOptL :: Sugar f l -> Sugar f ('TOr l Empty) + SOptR :: Sugar f r -> Sugar f ('TOr Empty r) + SOr :: Sugar f l -> Sugar f r -> Sugar f ('TOr l r) + SSomeL :: Sugar f l -> Sugar f ('TOr ('TStar r) r) + SSomeR :: Sugar f r -> Sugar f ('TOr r ('TStar r)) + SStar :: Sugar f r -> Sugar f ('TStar r) + SThen :: Sugar f l -> Sugar f r -> Sugar f ('TThen l r) + +sugar :: TestEquality f => RegexRepr f r -> Sugar f r +sugar = + \case + Empty -> SEmpty + Fail -> SFail + Lit l -> SLit l + Or l Empty -> SOptL (sugar l) + Or Empty r -> SOptR (sugar r) + Or (Star l) r | Just Refl <- testEquality l r -> SSomeL (sugar l) + Or l (Star r) | Just Refl <- testEquality l r -> SSomeR (sugar l) + Or l r -> SOr (sugar l) (sugar r) + Star r -> SStar (sugar r) + Then l r -> SThen (sugar l) (sugar r) + +-- | Lift top-level 'Or's (i.e., those not under quantifiers) +liftOrs :: Sugar f r -> Seq (Some (Sugar f)) +liftOrs = + \case + SEmpty -> Seq.singleton (Some SEmpty) + SFail -> Seq.empty + SLit x -> Seq.singleton (Some (SLit x)) + r@(SOptL {}) -> Seq.singleton (Some r) + r@(SOptR {}) -> Seq.singleton (Some r) + SOr l r -> liftOrs l <> liftOrs r + r@(SSomeL {}) -> Seq.singleton (Some r) + r@(SSomeR {}) -> Seq.singleton (Some r) + SThen l r -> + Seq.fromList + [ Some (SThen x y) + | Some x <- Foldable.toList (liftOrs l) + , Some y <- Foldable.toList (liftOrs r) + ] + SStar r -> Seq.singleton (Some (SStar r)) + +prettySugar :: + -- | Separator for 'SThen' + PP.Doc ann -> + (forall t. f t -> PP.Doc ann) -> + Sugar f r -> + PP.Doc ann +prettySugar sep f = + \case + SEmpty -> "" + SFail -> "∅" + SLit l -> f l + SOptL (SLit l) -> f l PP.<> "?" + SOptL l -> PP.parens (prettySugar sep f l) PP.<> "?" + SOptR (SLit r) -> f r PP.<> "?" + SOptR r -> PP.parens (prettySugar sep f r) PP.<> "?" + SOr l r -> PP.parens (prettySugar sep f l PP.<> "|" PP.<> prettySugar sep f r) + SSomeL (SLit l) -> f l PP.<> "+" + SSomeL l -> PP.parens (prettySugar sep f l) PP.<> "+" + SSomeR (SLit r) -> f r PP.<> "+" + SSomeR r -> PP.parens (prettySugar sep f r) PP.<> "+" + SStar (SLit l) -> f l PP.<> "*" + SStar r -> PP.parens (prettySugar sep f r) PP.<> "*" + SThen l r -> prettySugar sep f l PP.<> sep PP.<> prettySugar sep f r diff --git a/src/Lang/Crucible/Debug/Response.hs b/src/Lang/Crucible/Debug/Response.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug/Response.hs @@ -0,0 +1,191 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeApplications #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE UndecidableInstances #-} + +module Lang.Crucible.Debug.Response + ( NotApplicable(..) + , UserError(..) + , ResponseExt + , ProofResult(..) + , Response(..) + ) where + +import Control.Exception (IOException) +import Data.Foldable qualified as Foldable +import Data.Kind (Type) +import Data.Sequence qualified as Seq +import Data.Text qualified as Text +import Data.Text (Text) +import Data.Void (Void, absurd) +import Lang.Crucible.Debug.Arg (ArgParseError) +import Lang.Crucible.Debug.Command.Base qualified as BCmd +import Lang.Crucible.Debug.Command (Command) +import Lang.Crucible.Debug.Command qualified as Cmd +import Lang.Crucible.Debug.Regex (MatchError) +import Lang.Crucible.Debug.Statement (ParseError) +import Lang.Crucible.Debug.Statement qualified as Stmt +import Lang.Crucible.Debug.Style (Styled) +import Prettyprinter qualified as PP +import Text.Megaparsec.Error qualified as MP +import What4.FunctionName (FunctionName) +import What4.FunctionName qualified as W4 +import What4.ProgramLoc qualified as W4 + +-- | The command was not applicable in this state +data NotApplicable + = DoneSimulating + | NoCfg + | NoFrame + | NotDone + | NotYetSimulating + deriving Show + +instance PP.Pretty NotApplicable where + pretty = + \case + DoneSimulating -> "The simulator is no longer running" + NoCfg -> "Not executing a CFG" + NoFrame -> "Not in a call frame" + NotDone -> "Execution is not finished" + NotYetSimulating -> "The simulator is not yet running" + +-- | The command could not be completed successfully for some reason the user +-- should have anticipated. +data UserError cExt + = ArgError (Command cExt) (MatchError Text ArgParseError) + | BadArgNumber Text + | FnNotFound FunctionName [FunctionName] + | LoadParseError (MP.ParseErrorBundle Text Void) + | LoadSyntaxError (PP.Doc Void) + | NoHelp [Text] + | NoSuchArgument Int + | NotACfg W4.FunctionName + | NotApplicable NotApplicable + | SourceParseError ParseError + deriving Show + +instance PP.Pretty cExt => PP.Pretty (UserError cExt) where + pretty = + \case + ArgError cmd e -> + PP.vsep + [ "Bad arguments for command" PP.<+> PP.pretty cmd PP.<> ":" + , PP.pretty e + ] + BadArgNumber txt -> + "Bad argument number:" PP.<+> PP.pretty txt + FnNotFound nm nms -> + PP.vcat + [ "No such function:" PP.<+> PP.pretty nm + , if null nms + then mempty + else + PP.vcat + [ "Known functions:" + , PP.vcat (map (PP.pretty . W4.functionName) nms) + ] + ] + LoadParseError err -> PP.pretty (MP.errorBundlePretty err) + LoadSyntaxError err -> fmap absurd err + NoHelp args -> "Can't help with" PP.<+> PP.pretty (Text.intercalate " " args) + NoSuchArgument i -> "No such argument:" PP.<+> PP.pretty i + NotACfg fNm -> "Not a CFG:" PP.<+> PP.pretty (W4.functionName fNm) + NotApplicable err -> PP.pretty err + SourceParseError err -> + "Parse error during" PP.<+> + PP.pretty (Cmd.Base @Void BCmd.Source) PP.<> + ":" PP.<+> + PP.pretty (Stmt.renderParseError err) + +type ResponseExt :: Type -> Type +type family ResponseExt cExt :: Type +type instance ResponseExt Void = Void + +data ProofResult + = Proved + | Disproved + | Unknown + deriving Show + +instance PP.Pretty ProofResult where + pretty = + \case + Proved -> "proved" + Disproved -> "disproved" + Unknown -> "unknown" + +data Response cExt + = Arg (PP.Doc Void) + | Backtrace (PP.Doc Void) + | Block (PP.Doc Void) + | Cfg (PP.Doc Void) + | Clear Int + | Complete (PP.Doc Void) + | Delete W4.FunctionName Bool + | Frame (PP.Doc Void) + | Help (PP.Doc Void) + | IOError IOException + | Load FilePath Int + | Location W4.ProgramLoc + | Obligation [PP.Doc Void] + | PathCondition (PP.Doc Void) + | Prove (Seq.Seq (PP.Doc Void, ProofResult)) + | ProveTimeout + | Ok + | Style [Styled] + | Trace [PP.Doc Void] + | Usage (PP.Doc Void) + | UserError (UserError cExt) + | XResponse (ResponseExt cExt) + +deriving instance (Show (ResponseExt cExt), Show cExt) => Show (Response cExt) + +instance (PP.Pretty (ResponseExt cExt), PP.Pretty cExt) => PP.Pretty (Response cExt) where + pretty = + \case + Arg a -> fmap absurd a + Backtrace bt -> fmap absurd bt + Block b -> fmap absurd b + Cfg c -> fmap absurd c + Complete c -> fmap absurd c + Clear 0 -> "No proof obligations to clear" + Clear 1 -> "Cleared 1 proof obligation" + Clear n -> "Cleared" PP.<+> PP.pretty n PP.<+> "proof obligations" + Delete nm True -> "Deleted breakpoint at" PP.<+> PP.pretty (W4.functionName nm) + Delete nm False -> "No breakpoint at" PP.<+> PP.pretty (W4.functionName nm) + Frame f -> fmap absurd f + Help h -> fmap absurd h + Style styles -> PP.hsep (map PP.pretty styles) + Load p i -> PP.hsep ["Loaded", PP.pretty i, "CFGs from", PP.pretty p] + IOError e -> PP.viaShow e + Location l -> PP.pretty (W4.plFunction l) PP.<> PP.viaShow (W4.plSourceLoc l) + Obligation obls -> + if null obls + then "No proof obligations" + else PP.vsep (map (fmap absurd) obls) + PathCondition p -> fmap absurd p + Prove results -> + if Seq.null results + then "No obligations to prove" + else + PP.vcat $ + map + (\(goal, result) -> PP.vcat [fmap absurd goal, PP.pretty result]) + (Foldable.toList results) + ProveTimeout -> "Proof timed out!" + Ok -> "Ok" + Trace t -> PP.vcat (PP.punctuate PP.line (map (fmap absurd) t)) + Usage u -> fmap absurd u + UserError e -> PP.pretty e + XResponse rExt -> PP.pretty rExt diff --git a/src/Lang/Crucible/Debug/Statement.hs b/src/Lang/Crucible/Debug/Statement.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug/Statement.hs @@ -0,0 +1,48 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} + +module Lang.Crucible.Debug.Statement + ( Statement(..) + , ParseError + , renderParseError + , parse + ) where + +import Data.Text (Text) +import Lang.Crucible.Debug.Command (Command) +import Lang.Crucible.Debug.Command qualified as Cmd +import Data.Text qualified as Text + +data Statement cExt + = Statement + { stmtCmd :: Command cExt + , stmtArgs :: [Text] + } + deriving Functor + +data ParseError + = InvalidCommand Text + | NoCommand + deriving Show + +renderParseError :: ParseError -> Text +renderParseError = + \case + InvalidCommand txt -> "Invalid command: " <> txt + NoCommand -> "No command given" + +parse :: Cmd.CommandExt cExt -> Text -> Either ParseError (Statement cExt) +parse cExts txt = + case Text.words txt of + [] -> Left NoCommand + (cmdText:args) -> + case Cmd.parse cExts cmdText of + Just cmd -> Right (Statement cmd args) + Nothing -> Left (InvalidCommand cmdText) diff --git a/src/Lang/Crucible/Debug/Style.hs b/src/Lang/Crucible/Debug/Style.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug/Style.hs @@ -0,0 +1,264 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE GADTs #-} +{-# LANGUAGE GeneralizedNewtypeDeriving #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE StandaloneDeriving #-} + +module Lang.Crucible.Debug.Style + ( StyleEnv(..) + , StyleT(..) + , runStyle + , runStyleM + , Style(..) + , Valid(..) + , Styled(..) + , style + , highlighter + ) where + +import Control.Lens qualified as Lens +import Control.Monad.IO.Class (MonadIO) +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.Functor.Identity (Identity, runIdentity) +import Data.List qualified as List +import Data.Parameterized.Some (Some(Some), viewSome) +import Data.Sequence qualified as Seq +import Data.Set qualified as Set +import Data.Set (Set) +import Data.Text qualified as Text +import Data.Text (Text) +import Lang.Crucible.Debug.Arg (Arg) +import Lang.Crucible.Debug.Arg qualified as Arg +import Lang.Crucible.Debug.Arg.Type (ArgTypeRepr) +import Lang.Crucible.Debug.Breakpoint (Breakpoint) +import Lang.Crucible.Debug.Command (CommandExt) +import Lang.Crucible.Debug.Command qualified as Cmd +import Lang.Crucible.Debug.Regex qualified as Rgx +import Lang.Crucible.FunctionHandle qualified as C +import Lang.Crucible.Simulator.ExecutionTree qualified as C +import Prettyprinter qualified as PP +import System.Console.Isocline qualified as Isocline + +data StyleEnv cExt + = forall p sym ext r. + StyleEnv + { envBreakpoints :: Set Breakpoint + , envCommandExt :: CommandExt cExt + , envState :: C.ExecState p sym ext r + } + +newtype StyleT cExt m a + = StyleT + { runStyleT :: ReaderT (StyleEnv cExt) m a } + deriving (Applicative, Functor, Monad, MonadFail, MonadIO, MonadReader (StyleEnv cExt), MonadTrans) + +-- | Run 'StyleT' over 'Identity' +runStyle :: StyleEnv cExt -> StyleT cExt Identity a -> a +runStyle env s = runIdentity (Reader.runReaderT (runStyleT s) env) + +-- | Run 'StyleT' over another monad +-- +-- This is kind of poorly named, but I can\'t think of a better name... +runStyleM :: StyleEnv cExt -> StyleT cExt m a -> m a +runStyleM env s = Reader.runReaderT (runStyleT s) env + +data Style + = SBreakpoint + | SCommand + | SExactly + | SFunction + | SNumber + | SPath + | SText + | SUnknown + deriving (Eq, Show) + +instance PP.Pretty Style where + pretty = + \case + SBreakpoint -> "breakpoint" + SCommand -> "command" + SExactly -> "exactly" + SFunction -> "function" + SNumber -> "number" + SPath -> "path" + SText -> "text" + SUnknown -> "unknown" + +styleFor :: Arg cExt t -> Style +styleFor = + \case + Arg.ABreakpoint {} -> SBreakpoint + Arg.ACommand {} -> SCommand + Arg.AExactly {} -> SExactly + Arg.AFunction {} -> SFunction + Arg.AInt {} -> SNumber + Arg.APath {} -> SPath + Arg.AText {} -> SText + +data Valid + = Invalid + | Valid + | Unknown + deriving (Eq, Show) + +instance PP.Pretty Valid where + pretty = + \case + Invalid -> "invalid" + Valid -> "valid" + Unknown -> "unknown" + +boolToValid :: Bool -> Valid +boolToValid False = Invalid +boolToValid True = Valid + +validate :: + Monad m => + Arg cExt t -> + StyleT cExt m Valid +validate = + \case + Arg.ACommand {} -> pure Valid + Arg.ABreakpoint b -> + boolToValid <$> Reader.asks (Set.member b . envBreakpoints) + Arg.AExactly {} -> pure Valid + Arg.AFunction fNm -> do + StyleEnv { envState = execState } <- Reader.ask + let binds = execState Lens.^. Lens.to C.execStateContext . C.functionBindings + let hdls = C.handleMapToHandles (C.fnBindings binds) + case List.find (\(C.SomeHandle hdl) -> C.handleName hdl == fNm) hdls of + Nothing -> + -- May just not yet be loaded/discovered + pure Unknown + Just {} -> pure Valid + Arg.AInt {} -> pure Valid + Arg.APath {} -> pure Valid + Arg.AText {} -> pure Valid + +data Styled + = Styled + { styledStyle :: Style + , styledValid :: Valid + } + deriving (Eq, Show) + +instance PP.Pretty Styled where + pretty s = + PP.pretty (styledStyle s) PP.<+> PP.parens (PP.pretty (styledValid s)) + +styled :: + Monad m => + Arg cExt t -> + StyleT cExt m Styled +styled a = Styled (styleFor a) <$> validate a + +style :: + Monad m => + Rgx.RegexRepr ArgTypeRepr r -> + [Text] -> + StyleT cExt m [Styled] +style r = + \case + [] -> pure [] + (word : ws) -> do + cExt <- Reader.asks envCommandExt + let bad = List.replicate (1 + length ws) (Styled SUnknown Invalid) + case Arg.derivative cExt word r of + Rgx.DerivativeResult (Some Rgx.Fail) _ -> pure bad + Rgx.DerivativeResult (Some _) Seq.Empty -> pure bad + Rgx.DerivativeResult (Some r') (Some m Seq.:<| Seq.Empty) -> do + s <- styled m + ss <- style r' ws + 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 + rest <- style r' ws + pure (combined : rest) + where + combineStyles :: Style -> Style -> Style + combineStyles s0 s = if s == s0 then s0 else SUnknown + + combineValid :: Valid -> Valid -> Valid + combineValid v0 v = if v == v0 then v0 else Unknown + + combineStyled :: Styled -> Styled -> Styled + combineStyled s0 s = + Styled + (combineStyles (styledStyle s0) (styledStyle s)) + (combineValid (styledValid s0) (styledValid s)) + +-- | Helper, not exported +badStyle :: String -> Isocline.Fmt +badStyle = Isocline.style "red" + +-- | Helper, not exported +cmdStyle :: String -> Isocline.Fmt +cmdStyle = Isocline.style "bold" + +highlightWithRegex :: + Monad m => + Rgx.RegexRepr ArgTypeRepr r -> + String -> + StyleT cExt m Isocline.Fmt +highlightWithRegex r line = do + let (initSpaces, rest) = splitOnSpaces line + let wds = List.map fst rest + styles <- style r (List.map Text.pack wds) + let styledWords = zipWith ($) (map doStyle styles) wds + let wordsWithSpaces = + foldMap (uncurry (++)) (zip styledWords (List.map snd rest)) + pure (initSpaces ++ wordsWithSpaces) + where + splitOnSpaces :: String -> (String, [(String, String)]) + splitOnSpaces s = + let (initSpaces, rest) = List.span (== ' ') s in + (initSpaces, go rest) + where + go "" = [] + go x = + let (word, rest) = List.span (/= ' ') x in + let (spaces, rest') = List.span (== ' ') rest in + (word, spaces) : go rest' + + -- Fairly arbitrary choices + doStyle :: Styled -> String -> Isocline.Fmt + doStyle s = + case styledValid s of + Invalid -> badStyle + _ -> + case styledStyle s of + SBreakpoint -> Isocline.style "green" + SCommand -> cmdStyle + SExactly -> Isocline.style "keyword" + SFunction -> Isocline.style "blue" + SNumber -> Isocline.style "number" + SPath -> Isocline.style "italic" + SText -> id + SUnknown -> id + +highlighter :: Monad m => String -> StyleT cExt m Isocline.Fmt +highlighter input = do + cExt <- Reader.asks envCommandExt + let (initSpaces, rest) = List.span (== ' ') input + let (cmdStr, rest') = List.span (/= ' ') rest + case Cmd.parse cExt (Text.pack cmdStr) of + Just cmd -> + case Cmd.regex cExt cmd of + Some rx -> do + styledRest <- highlightWithRegex rx rest' + pure $ List.concat [initSpaces , cmdStyle cmdStr, styledRest] + Nothing -> pure $ List.concat [initSpaces, badStyle cmdStr, rest'] + diff --git a/src/Lang/Crucible/Debug/Trace.hs b/src/Lang/Crucible/Debug/Trace.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Debug/Trace.hs @@ -0,0 +1,83 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE ExplicitNamespaces #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module Lang.Crucible.Debug.Trace + ( TraceEntry(..) + , Trace + , empty + , append + , latest + ) where + +import Control.Lens qualified as Lens +import Data.Parameterized.Classes (ixF') +import Data.Parameterized.Context qualified as Ctx +import Data.Parameterized.NatRepr qualified as NatRepr +import Data.Parameterized.NatRepr (type (<=), NatRepr) +import Data.Parameterized.Some (Some(Some)) +import Data.RingBuffer qualified as RB +import Data.Vector qualified as V +import Lang.Crucible.CFG.Core qualified as C +import Lang.Crucible.CFG.Extension qualified as C +import Prettyprinter qualified as PP +import What4.ProgramLoc qualified as W4 + +data TraceEntry ext + = forall blocks init ret. + TraceEntry + { traceCfg :: C.CFG ext blocks init ret + , traceBlock :: Some (C.BlockID blocks) + } + +instance C.PrettyExt ext => PP.Pretty (TraceEntry ext) where + pretty (TraceEntry cfg (Some blkId)) = + let blk = C.cfgBlockMap cfg Lens.^. ixF' (C.blockIDIndex blkId) in + ppStmtSeq True (Ctx.size (C.blockInputs blk)) (C._blockStmts blk) + -- TODO: Taken from Crucible. Export upstream? + where + prefixLineNum :: Bool -> W4.ProgramLoc -> PP.Doc ann -> PP.Doc ann + prefixLineNum True pl d = PP.vcat [PP.pretty "%" PP.<+> W4.ppNoFileName (W4.plSourceLoc pl), d] + prefixLineNum False _ d = d + + ppStmtSeq :: C.PrettyExt ext => Bool -> Ctx.Size ctx -> C.StmtSeq ext blocks ret ctx -> PP.Doc ann + ppStmtSeq ppLineNum h (C.ConsStmt pl s r) = + PP.vcat + [ prefixLineNum ppLineNum pl (C.ppStmt h s) + , ppStmtSeq ppLineNum (C.nextStmtHeight h s) r + ] + ppStmtSeq ppLineNum _ (C.TermStmt pl s) = + prefixLineNum ppLineNum pl (PP.pretty s) + + +newtype Trace ext = Trace (RB.RingBuffer V.Vector (TraceEntry ext)) + +-- 'RB.new' requires a nonzero input, which we enforce with types +empty :: (1 <= n) => NatRepr n -> IO (Trace ext) +empty n = Trace <$> RB.new (fromIntegral (NatRepr.natValue n)) + +-- | O(1). +append :: Trace ext -> TraceEntry ext -> IO () +append (Trace b) e = RB.append e b +{-# INLINEABLE append #-} + +-- | Get up to the @N@ latest entries +latest :: Trace ext -> Int -> IO [TraceEntry ext] +latest (Trace b) n = go n + where + go x | x <= 0 = pure [] + go x = do + mEnt <- RB.latest b (n - x) + case mEnt of + Nothing -> pure [] + Just ent -> (ent :) <$> go (x - 1) diff --git a/src/Lang/Crucible/Pretty.hs b/src/Lang/Crucible/Pretty.hs new file mode 100644 --- /dev/null +++ b/src/Lang/Crucible/Pretty.hs @@ -0,0 +1,122 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett +-} + +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneKindSignatures #-} +{-# LANGUAGE TypeApplications #-} + +module Lang.Crucible.Pretty + ( IntrinsicPrettyFn(..) + , IntrinsicPrinters(..) + , ppRegVal + ) where + +import qualified Data.List as List +import Data.Kind (Type) +import qualified Data.Text as Text + +import qualified Prettyprinter as PP + +import qualified Data.Parameterized.Context as Ctx +import Data.Parameterized.Map (MapF) +import qualified Data.Parameterized.Map as MapF +import Data.Parameterized.SymbolRepr (Symbol) +import Data.Parameterized.TraversableFC (toListFC) + +-- what4 +import qualified What4.Interface as W4 + +-- crucible +import qualified Lang.Crucible.FunctionHandle as C +import qualified Lang.Crucible.Simulator.Intrinsics as C +import qualified Lang.Crucible.Simulator.RegMap as C +import qualified Lang.Crucible.Simulator.SymSequence as C +import qualified Lang.Crucible.Types as C + +-- | Function for pretty-printing an intrinsic type +-- +-- TODO: Upstream to Crucible +type IntrinsicPrettyFn :: Type -> Symbol -> Type +newtype IntrinsicPrettyFn sym nm + = IntrinsicPrettyFn + (forall ctx ann. + Ctx.Assignment C.TypeRepr ctx -> + C.Intrinsic sym nm ctx -> + PP.Doc ann) + +newtype IntrinsicPrinters sym + = IntrinsicPrinters + { getIntrinsicPrinters :: MapF C.SymbolRepr (IntrinsicPrettyFn sym) } + +-- TODO: Complete all the cases, upstream to Crucible +-- | Pretty-print a 'C.RegValue'. +ppRegVal :: + forall sym tp ann. + W4.IsExpr (W4.SymExpr sym) => + IntrinsicPrinters sym -> + C.TypeRepr tp -> + C.RegValue' sym tp -> + PP.Doc ann +ppRegVal iFns tp (C.RV v) = + case tp of + -- Base types + C.BoolRepr -> W4.printSymExpr v + C.BVRepr _width -> W4.printSymExpr v + C.ComplexRealRepr -> W4.printSymExpr v + C.FloatRepr _fi -> W4.printSymExpr v + C.IEEEFloatRepr _fpp -> W4.printSymExpr v + C.IntegerRepr -> W4.printSymExpr v + C.NatRepr -> W4.printSymExpr (W4.natToIntegerPure v) + C.RealValRepr -> W4.printSymExpr v + C.StringRepr _si -> W4.printSymExpr v + C.SymbolicArrayRepr _idxs _tp' -> W4.printSymExpr v + C.SymbolicStructRepr _tys -> W4.printSymExpr v + + -- Trivial cases + C.UnitRepr -> "()" + C.CharRepr -> PP.pretty v + + -- Simple recursive cases + C.RecursiveRepr symb tyCtx -> + ppRegVal iFns (C.unrollType symb tyCtx) (C.RV @sym (C.unroll v)) + C.SequenceRepr tp' -> + C.prettySymSequence (ppRegVal iFns tp' . C.RV @sym) v + C.StructRepr fields -> + let struct = PP.encloseSep PP.lbrace PP.rbrace (PP.comma PP.<> PP.space) in + let entries = Ctx.zipWith (\t (C.RV fv) -> C.RegEntry @sym t fv) fields v in + struct (toListFC (\(C.RegEntry tp' val) -> ppRegVal iFns tp' (C.RV @sym val)) entries) + C.IntrinsicRepr nm tyCtx -> + case MapF.lookup nm (getIntrinsicPrinters iFns) of + Nothing -> + let strNm = Text.unpack (C.symbolRepr nm) in + -- TODO: Replace with `panic`, exception, or `Maybe` + error ("ppRegVal: Missing pretty-printing function for intrinsic: " List.++ strNm) + Just (IntrinsicPrettyFn f) -> f tyCtx v + + -- More complex cases + C.FunctionHandleRepr args ret -> ppFnVal args ret v + _ -> "" + +ppFnVal :: + C.CtxRepr ctx -> + C.TypeRepr ret -> + C.FnVal sym ctx ret -> + PP.Doc ann +ppFnVal args ret = + \case + C.HandleFnVal hdl -> + PP.hsep + [ PP.pretty (C.handleName hdl) + , ":" + , PP.hsep (PP.punctuate " ->" (toListFC PP.pretty args)) + , "->" + , PP.pretty ret + ] + _ -> "" diff --git a/test-data/backtrace.txt b/test-data/backtrace.txt new file mode 100644 --- /dev/null +++ b/test-data/backtrace.txt @@ -0,0 +1,59 @@ +> load test-data/three-calls.cbl + +Loaded 3 CFGs from test-data/three-calls.cbl + +> step + +Ok + +> break a + +Ok + +> break b + +Ok + +> break c + +Ok + +> call a + +Ok + +> run + +Ok + +> backtrace + +In a at test-data/three-calls.cbl:3:13 + +> run + +Ok + +> backtrace + +In b at test-data/three-calls.cbl:8:13 +In a at test-data/three-calls.cbl:3:13 + +> run + +Ok + +> backtrace + +In c at test-data/three-calls.cbl:13:13 +In b at test-data/three-calls.cbl:8:13 +In a at test-data/three-calls.cbl:3:13 + +> run + +Ok + +> done + +Ok + diff --git a/test-data/block.txt b/test-data/block.txt new file mode 100644 --- /dev/null +++ b/test-data/block.txt @@ -0,0 +1,33 @@ +> load test-data/add.cbl + +Loaded 2 CFGs from test-data/add.cbl + +> step + +Ok + +> break add + +Ok + +> call main + +Ok + +> run + +Ok + +> block + +$2 = intAdd($0, $1) +return $2 + +> run + +Ok + +> done + +Ok + diff --git a/test-data/break.txt b/test-data/break.txt new file mode 100644 --- /dev/null +++ b/test-data/break.txt @@ -0,0 +1,28 @@ +> load test-data/three-calls.cbl + +Loaded 3 CFGs from test-data/three-calls.cbl + +> step + +Ok + +> break b + +Ok + +> call a + +Ok + +> run + +Ok + +> run + +Ok + +> done + +Ok + diff --git a/test-data/call-basic.txt b/test-data/call-basic.txt new file mode 100644 --- /dev/null +++ b/test-data/call-basic.txt @@ -0,0 +1,20 @@ +> load test-data/basic.cbl + +Loaded 1 CFGs from test-data/basic.cbl + +> step + +Ok + +> call main + +Ok + +> run + +Ok + +> done + +Ok + diff --git a/test-data/clear.txt b/test-data/clear.txt new file mode 100644 --- /dev/null +++ b/test-data/clear.txt @@ -0,0 +1,28 @@ +> load test-data/assert-false.cbl + +Loaded 1 CFGs from test-data/assert-false.cbl + +> step + +Ok + +> call main + +Ok + +> run + +Ok + +> clear + +Cleared 1 proof obligation + +> prove + +No obligations to prove + +> done + +Ok + diff --git a/test-data/comment.txt b/test-data/comment.txt new file mode 100644 --- /dev/null +++ b/test-data/comment.txt @@ -0,0 +1,8 @@ +> # this is a comment + +Ok + +> quit + +Ok + diff --git a/test-data/complete/break.txt b/test-data/complete/break.txt new file mode 100644 --- /dev/null +++ b/test-data/complete/break.txt @@ -0,0 +1,28 @@ +> usage break + +break FUNCTION + +> . complete break + +function + +> . complete break fo_ + +function + +> load test-data/assert-false.cbl + +Loaded 1 CFGs from test-data/assert-false.cbl + +> . complete break + +function: main + +> . complete break ma_ + +function: main + +> quit + +Ok + diff --git a/test-data/complete/cfg.txt b/test-data/complete/cfg.txt new file mode 100644 --- /dev/null +++ b/test-data/complete/cfg.txt @@ -0,0 +1,16 @@ +> usage cfg + +cfg FUNCTION? + +> . complete cfg + +function + +> . complete cfg foo + +No completions + +> quit + +Ok + diff --git a/test-data/complete/comment.txt b/test-data/complete/comment.txt new file mode 100644 --- /dev/null +++ b/test-data/complete/comment.txt @@ -0,0 +1,20 @@ +> usage # + +# TEXT* + +> . complete # + +No completions + +> . complete # foo + +No completions + +> . complete # foo bar baz quux + +No completions + +> quit + +Ok + diff --git a/test-data/complete/delete.txt b/test-data/complete/delete.txt new file mode 100644 --- /dev/null +++ b/test-data/complete/delete.txt @@ -0,0 +1,40 @@ +> usage delete + +delete BREAKPOINT + +> . complete delete + +breakpoint + +> break foo + +Ok + +> break bar + +Ok + +> . complete delete + +breakpoint: bar, foo + +> . complete delete foo + +No completions + +> . complete delete fo_ + +breakpoint: foo + +> delete foo + +Deleted breakpoint at foo + +> . complete delete + +breakpoint: bar + +> quit + +Ok + diff --git a/test-data/complete/help.txt b/test-data/complete/help.txt new file mode 100644 --- /dev/null +++ b/test-data/complete/help.txt @@ -0,0 +1,16 @@ +> usage help + +help COMMAND? + +> . complete help + +command + +> . complete help secret + +No completions + +> quit + +Ok + diff --git a/test-data/complete/load.txt b/test-data/complete/load.txt new file mode 100644 --- /dev/null +++ b/test-data/complete/load.txt @@ -0,0 +1,28 @@ +> usage load + +load PATH + +> . complete load ap_ + +path: ./app + +> . complete load app_ + +path: app/ + +> . complete load app/_ + +path: app/Main.hs + +> . complete load app/M_ + +path: app/Main.hs + +> . complete load app/DoesNotExist._ + +path + +> quit + +Ok + diff --git a/test-data/complete/reg.txt b/test-data/complete/reg.txt new file mode 100644 --- /dev/null +++ b/test-data/complete/reg.txt @@ -0,0 +1,24 @@ +> usage reg + +register INT* + +> . complete reg + +No completions + +> . complete reg 1 + +No completions + +> . complete reg 1 0 + +No completions + +> . complete reg foo + +No completions + +> quit + +Ok + diff --git a/test-data/complete/secret.txt b/test-data/complete/secret.txt new file mode 100644 --- /dev/null +++ b/test-data/complete/secret.txt @@ -0,0 +1,27 @@ +> usage secret + +secret complete COMMAND TEXT* +secret style COMMAND TEXT* + +> . complete secret + +complete +style + +> . complete secret complete + +command + +> . complete secret complete secret complete secret + +No completions + +> . complete secret comp_ help + +complete +style (x) + +> quit + +Ok + diff --git a/test-data/delete.txt b/test-data/delete.txt new file mode 100644 --- /dev/null +++ b/test-data/delete.txt @@ -0,0 +1,16 @@ +> delete main + +No breakpoint at main + +> break main + +Ok + +> delete main + +Deleted breakpoint at main + +> quit + +Ok + diff --git a/test-data/error/cfg-fun-not-found.txt b/test-data/error/cfg-fun-not-found.txt new file mode 100644 --- /dev/null +++ b/test-data/error/cfg-fun-not-found.txt @@ -0,0 +1,9 @@ +> cfg no_such_function + +No such function: no_such_function + + +> quit + +Ok + diff --git a/test-data/error/cfg-no-cfg.txt b/test-data/error/cfg-no-cfg.txt new file mode 100644 --- /dev/null +++ b/test-data/error/cfg-no-cfg.txt @@ -0,0 +1,12 @@ +> step + +Ok + +> cfg + +Not executing a CFG + +> quit + +Ok + diff --git a/test-data/error/cfg-not-simulating.txt b/test-data/error/cfg-not-simulating.txt new file mode 100644 --- /dev/null +++ b/test-data/error/cfg-not-simulating.txt @@ -0,0 +1,8 @@ +> cfg + +The simulator is not yet running + +> quit + +Ok + diff --git a/test-data/error/frame-not-simulating.txt b/test-data/error/frame-not-simulating.txt new file mode 100644 --- /dev/null +++ b/test-data/error/frame-not-simulating.txt @@ -0,0 +1,8 @@ +> frame + +The simulator is not yet running + +> quit + +Ok + diff --git a/test-data/error/help-no-help.txt b/test-data/error/help-no-help.txt new file mode 100644 --- /dev/null +++ b/test-data/error/help-no-help.txt @@ -0,0 +1,11 @@ +> help asdf + +Bad arguments for command help: +Both branches failed to match: +- Expected end of input, but found: asdf +- 'asdf' is not a command + +> quit + +Ok + diff --git a/test-data/error/load-dir.txt b/test-data/error/load-dir.txt new file mode 100644 --- /dev/null +++ b/test-data/error/load-dir.txt @@ -0,0 +1,8 @@ +> load . + +.: openFile: inappropriate type (is a directory) + +> quit + +Ok + diff --git a/test-data/error/load-no-file.txt b/test-data/error/load-no-file.txt new file mode 100644 --- /dev/null +++ b/test-data/error/load-no-file.txt @@ -0,0 +1,8 @@ +> load does-not-exist.txt + +does-not-exist.txt: openFile: does not exist (No such file or directory) + +> quit + +Ok + diff --git a/test-data/error/load-parse-error.txt b/test-data/error/load-parse-error.txt new file mode 100644 --- /dev/null +++ b/test-data/error/load-parse-error.txt @@ -0,0 +1,14 @@ +> load LICENSE + +LICENSE:1:30: + | +1 | Copyright (c) 2025 Galois Inc. + | ^ +unexpected '.' +expecting '"', '#', '$', '(', '+', '-', '0', '@', decimal digit, or end of input + + +> quit + +Ok + diff --git a/test-data/error/run-bad-arity.txt b/test-data/error/run-bad-arity.txt new file mode 100644 --- /dev/null +++ b/test-data/error/run-bad-arity.txt @@ -0,0 +1,9 @@ +> run run_takes_no_args + +Bad arguments for command run: +Expected end of input, but found: run_takes_no_args + +> quit + +Ok + diff --git a/test-data/error/source-no-file.txt b/test-data/error/source-no-file.txt new file mode 100644 --- /dev/null +++ b/test-data/error/source-no-file.txt @@ -0,0 +1,8 @@ +> source does-not-exist.txt + +does-not-exist.txt: openFile: does not exist (No such file or directory) + +> quit + +Ok + diff --git a/test-data/error/source-parse-error.txt b/test-data/error/source-parse-error.txt new file mode 100644 --- /dev/null +++ b/test-data/error/source-parse-error.txt @@ -0,0 +1,16 @@ +> source LICENSE + +Parse error during source: Invalid command: Copyright + +> # TODO(lb): What's going on below here? + +Ok + +> quit + +Ok + +> done + +Ok + diff --git a/test-data/finish.txt b/test-data/finish.txt new file mode 100644 --- /dev/null +++ b/test-data/finish.txt @@ -0,0 +1,8 @@ +> finish + +Ok + +> done + +Ok + diff --git a/test-data/frame.txt b/test-data/frame.txt new file mode 100644 --- /dev/null +++ b/test-data/frame.txt @@ -0,0 +1,45 @@ +> load test-data/add.cbl + +Loaded 2 CFGs from test-data/add.cbl + +> frame + +The simulator is not yet running + +> step + +Ok + +> frame + +Return: _start + +> break add + +Ok + +> call main + +Ok + +> run + +Ok + +> frame + +CFG: add +Block: %0 + +Argument types: +- Integer +- Integer + +> run + +Ok + +> done + +Ok + diff --git a/test-data/help.txt b/test-data/help.txt new file mode 100644 --- /dev/null +++ b/test-data/help.txt @@ -0,0 +1,51 @@ +> help + +# (#): Ignore all arguments and do nothing +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 +call (cl): Call a function (must take no arguments and return the unit type) +cfg (cg): Print the CFG of a function (the current function if none is provided) +clear (cr): Drop the current proof obligations +delete (d): Remove a breakpoint +done (done): Like `quit`, but only applies when symbolic execution has finished +finish (fh): Execute to the end of the current function +frame (fr): Print information about the active stack frame +help (h): Display help text +load (l): Load a Crucible S-expression program from a file +location (loc): Print the current program location +obligation (o): Print the current proof obligations +path-condition (pcond): Print the current path condition +prove (p): Prove the current goals +quit (q): Exit the debugger +register (reg): Print registers (including block/function arguments) +run (r): Continue to the next breakpoint or the end of execution +secret (.): Maintenance commands, used for testing +source (src): Execute a file containing debugger commands +step (s): Continue N steps of execution (default: 1) +trace (trace): Print the N most recently executed basic blocks (default: 2) +usage (u): Display command usage hint + + +> help run + +run + +Continue to the next breakpoint or the end of execution. + +> help register + +register INT* + +Print registers (including block/function arguments). + +When given no arguments, prints all values in scope. Otherwise, prints the values with the given numbers, one per line. + +The value numbering scheme is based on the structure of Crucible CFGs. A Crucible CFG (function) is made up of *basic blocks*. Each basic block takes a list of arguments. The first block in the function is the *entry* block; the entry block takes the same arguments as the function. Each block contains a number of *statements*, which may define values. The value defined by a statement is in scope for the rest of the block. + +Values are then numbered as follows: The first argument to the current block is numbered 0. Increasing numbers refer to later arguments. After arguments, higher numbers refer to values defined by statements. + +> quit + +Ok + diff --git a/test-data/load-empty.txt b/test-data/load-empty.txt new file mode 100644 --- /dev/null +++ b/test-data/load-empty.txt @@ -0,0 +1,12 @@ +> load test-data/empty.cbl + +Loaded 0 CFGs from test-data/empty.cbl + +> run + +Ok + +> done + +Ok + diff --git a/test-data/location.txt b/test-data/location.txt new file mode 100644 --- /dev/null +++ b/test-data/location.txt @@ -0,0 +1,8 @@ +> location + +_start:1:0 + +> quit + +Ok + diff --git a/test-data/obligation-false.txt b/test-data/obligation-false.txt new file mode 100644 --- /dev/null +++ b/test-data/obligation-false.txt @@ -0,0 +1,32 @@ +> load test-data/assert-false.cbl + +Loaded 1 CFGs from test-data/assert-false.cbl + +> step + +Ok + +> call main + +Ok + +> run + +Ok + +> obligation + + +Prove: + test-data/assert-false.cbl:3:5: error: in main + false is true + false + +> clear + +Cleared 1 proof obligation + +> done + +Ok + diff --git a/test-data/obligation.txt b/test-data/obligation.txt new file mode 100644 --- /dev/null +++ b/test-data/obligation.txt @@ -0,0 +1,8 @@ +> obligation + +No proof obligations + +> quit + +Ok + diff --git a/test-data/path-condition.txt b/test-data/path-condition.txt new file mode 100644 --- /dev/null +++ b/test-data/path-condition.txt @@ -0,0 +1,12 @@ +> path-condition + +true + +> run + +Ok + +> done + +Ok + diff --git a/test-data/prove-false.txt b/test-data/prove-false.txt new file mode 100644 --- /dev/null +++ b/test-data/prove-false.txt @@ -0,0 +1,33 @@ +> load test-data/assert-false.cbl + +Loaded 1 CFGs from test-data/assert-false.cbl + +> step + +Ok + +> call main + +Ok + +> run + +Ok + +> prove + + +Prove: + test-data/assert-false.cbl:3:5: error: in main + false is true + false +disproved + +> clear + +Cleared 1 proof obligation + +> done + +Ok + diff --git a/test-data/prove-true.txt b/test-data/prove-true.txt new file mode 100644 --- /dev/null +++ b/test-data/prove-true.txt @@ -0,0 +1,24 @@ +> load test-data/assert-true.cbl + +Loaded 1 CFGs from test-data/assert-true.cbl + +> step + +Ok + +> call main + +Ok + +> run + +Ok + +> prove + +No obligations to prove + +> done + +Ok + diff --git a/test-data/prove.txt b/test-data/prove.txt new file mode 100644 --- /dev/null +++ b/test-data/prove.txt @@ -0,0 +1,8 @@ +> prove + +No obligations to prove + +> quit + +Ok + diff --git a/test-data/quit.txt b/test-data/quit.txt new file mode 100644 --- /dev/null +++ b/test-data/quit.txt @@ -0,0 +1,4 @@ +> quit + +Ok + diff --git a/test-data/r.txt b/test-data/r.txt new file mode 100644 --- /dev/null +++ b/test-data/r.txt @@ -0,0 +1,8 @@ +> r + +Ok + +> done + +Ok + diff --git a/test-data/reg.txt b/test-data/reg.txt new file mode 100644 --- /dev/null +++ b/test-data/reg.txt @@ -0,0 +1,78 @@ +> load test-data/args.cbl + +Loaded 2 CFGs from test-data/args.cbl + +> register + +The simulator is not yet running + +> step + +Ok + +> break add + +Ok + +> call main + +Ok + +> step 2 + +Ok + +> reg + + + +> step 2 + +Ok + +> reg + +cp@0:b +cx@1:i + +> reg 0 + +cp@0:b + +> reg 1 0 + +cx@1:i +cp@0:b + +> step 3 + +Ok + +> reg + +cx@1:i + +> run + +Ok + +> reg + +0 +ite cp@0:b cx@1:i 12 + +> finish + +Ok + +> reg + +ite cp@0:b cx@1:i 12 +add : Integer -> Integer -> Integer +0 +ite cp@0:b cx@1:i 12 + +> quit + +Ok + diff --git a/test-data/run.txt b/test-data/run.txt new file mode 100644 --- /dev/null +++ b/test-data/run.txt @@ -0,0 +1,8 @@ +> run + +Ok + +> done + +Ok + diff --git a/test-data/step.txt b/test-data/step.txt new file mode 100644 --- /dev/null +++ b/test-data/step.txt @@ -0,0 +1,16 @@ +> step + +Ok + +> step 2 + +Ok + +> step + +The simulator is no longer running + +> done + +Ok + diff --git a/test-data/style/break.txt b/test-data/style/break.txt new file mode 100644 --- /dev/null +++ b/test-data/style/break.txt @@ -0,0 +1,16 @@ +> usage break + +break FUNCTION + +> . style break + + + +> . style break foo + +function (unknown) + +> quit + +Ok + diff --git a/test-data/style/cfg.txt b/test-data/style/cfg.txt new file mode 100644 --- /dev/null +++ b/test-data/style/cfg.txt @@ -0,0 +1,16 @@ +> usage cfg + +cfg FUNCTION? + +> . style cfg + + + +> . style cfg foo + +function (unknown) + +> quit + +Ok + diff --git a/test-data/style/comment.txt b/test-data/style/comment.txt new file mode 100644 --- /dev/null +++ b/test-data/style/comment.txt @@ -0,0 +1,20 @@ +> usage # + +# TEXT* + +> . style # + + + +> . style # foo + +text (valid) + +> . style # foo bar baz quux + +text (valid) text (valid) text (valid) text (valid) + +> quit + +Ok + diff --git a/test-data/style/delete.txt b/test-data/style/delete.txt new file mode 100644 --- /dev/null +++ b/test-data/style/delete.txt @@ -0,0 +1,24 @@ +> usage delete + +delete BREAKPOINT + +> . style delete + + + +> . style delete foo + +breakpoint (invalid) + +> break foo + +Ok + +> . style delete foo + +breakpoint (valid) + +> quit + +Ok + diff --git a/test-data/style/help.txt b/test-data/style/help.txt new file mode 100644 --- /dev/null +++ b/test-data/style/help.txt @@ -0,0 +1,16 @@ +> usage help + +help COMMAND? + +> . style help + + + +> . style help secret + +command (valid) + +> quit + +Ok + diff --git a/test-data/style/reg.txt b/test-data/style/reg.txt new file mode 100644 --- /dev/null +++ b/test-data/style/reg.txt @@ -0,0 +1,24 @@ +> usage reg + +register INT* + +> . style reg + + + +> . style reg 1 + +number (valid) + +> . style reg 1 0 + +number (valid) number (valid) + +> . style reg foo + +unknown (invalid) + +> quit + +Ok + diff --git a/test-data/style/secret.txt b/test-data/style/secret.txt new file mode 100644 --- /dev/null +++ b/test-data/style/secret.txt @@ -0,0 +1,25 @@ +> usage secret + +secret complete COMMAND TEXT* +secret style COMMAND TEXT* + +> . style secret + + + +> # TODO(lb): Why do the following get "unknown"? + +Ok + +> . style secret complete + +unknown (valid) + +> . style secret complete secret complete secret + +unknown (valid) unknown (valid) text (valid) unknown (valid) + +> quit + +Ok + diff --git a/test-data/trace.txt b/test-data/trace.txt new file mode 100644 --- /dev/null +++ b/test-data/trace.txt @@ -0,0 +1,80 @@ +> load test-data/args.cbl + +Loaded 2 CFGs from test-data/args.cbl + +> register + +The simulator is not yet running + +> step + +Ok + +> break add + +Ok + +> call main + +Ok + +> run + +Ok + +> trace + +% 7:12 +$0 = fresh BaseBoolRepr p +% 8:12 +$1 = fresh BaseIntegerRepr x +% 9:5 +br $0 %1($1) %2() + +% 13:18 +$0 = intLit(12) +% 13:5 +jump %3($0) + +> finish + +Ok + +> finish + +Ok + +> trace 5 + +% 7:12 +$0 = fresh BaseBoolRepr p +% 8:12 +$1 = fresh BaseIntegerRepr x +% 9:5 +br $0 %1($1) %2() + +% 13:18 +$0 = intLit(12) +% 13:5 +jump %3($0) + +% 3:13 +$2 = intAdd($0, $1) +% 3:5 +return $2 + +% 15:5 +$1 = handleLit(add) +% 15:5 +$2 = intLit(0) +% 15:5 +$3 = call $1($2, $0); +% 16:13 +$4 = emptyApp() +% 16:5 +return $4 + +> quit + +Ok + diff --git a/test-data/usage.txt b/test-data/usage.txt new file mode 100644 --- /dev/null +++ b/test-data/usage.txt @@ -0,0 +1,25 @@ +> usage reg + +register INT* + +> usage help + +help COMMAND? + +> usage step + +step INT? + +> usage secret + +secret complete COMMAND TEXT* +secret style COMMAND TEXT* + +> usage usage + +usage COMMAND + +> quit + +Ok + diff --git a/test/Test.hs b/test/Test.hs new file mode 100644 --- /dev/null +++ b/test/Test.hs @@ -0,0 +1,101 @@ +{-| +Copyright : (c) Galois, Inc. 2025 +Maintainer : Langston Barrett + +This test suite is composed of golden test files. +Each file consists of inputs (@Statement@s) that begin with @> @, and outputs that follow them. +This comingling of inputs and outputs stands in contrast to a more customary golden test setup where the inputs are in one file and the outputs in another. +It makes the relationship between various inputs and outputs clear at a glance, which makes the tests easier to read and understand in a text editor or web interface. +This readability comes at the cost of a mildly gnarly test harness (see, e.g., 'parseTest' and 'runScript'). +To create a new test, simply create a new file with all of the input lines, and then run the test suite with the @--accept@ flag, i.e., @cabal test -- --accept@. +-} + +{-# LANGUAGE ImportQualifiedPost #-} +{-# LANGUAGE OverloadedStrings #-} +{-# LANGUAGE TupleSections #-} + +module Main (main) where + +import Data.ByteString (ByteString) +import Data.ByteString.Lazy qualified as BS +import Data.IORef qualified as IORef +import Data.List qualified as List +import Data.Text (Text) +import Data.Text qualified as Text +import Data.Text.Encoding as Text +import Data.Text.IO as IO +import Lang.Crucible.Debug qualified as Debug +import Lang.Crucible.Debug.Inputs qualified as Inps +import Lang.Crucible.Debug.Outputs qualified as Outps +import Prettyprinter qualified as PP +import Prettyprinter.Render.Text qualified as PP +import System.Directory qualified as Dir +import Test.Tasty qualified as Tasty +import Test.Tasty.Golden qualified as Golden + +testDir :: FilePath +testDir = "test-data/" + +-- | Parse a test file into a sequence of inputs and outputs +parseTest :: Text -> [(Text, Text)] +parseTest txt = List.reverse (go [] Nothing (Text.lines txt)) + where + go :: + -- | Accumulated result + [(Text, Text)] -> + -- | Perhaps (input, accumulated output) + Maybe (Text, [Text]) -> + -- | Remaining lines + [Text] -> + [(Text, Text)] + go accum Nothing [] = accum + go accum (Just (inp, out)) [] = (inp, Text.unlines (List.reverse out)) : accum + go accum soFar (l:ls) = + if l == "" + then go accum soFar ls + else + case (soFar, Text.stripPrefix "> " l) of + (Nothing, Nothing) -> error "Ill-formed test file" + (Nothing, Just l') -> go accum (Just (l', [])) ls + (Just (inp, out), Nothing) -> go accum (Just (inp, l:out)) ls + (Just (inp, out), Just l') -> + let accum' = (inp, Text.unlines (List.reverse out)) : accum in + go accum' (Just (l', [])) ls + +runScript :: FilePath -> IO ByteString +runScript path = do + testTxt <- IO.readFile path + let parsed = parseTest testTxt + let inputTxtLines = map fst parsed ++ ["done"] + inps <- Inps.parseInputs Debug.voidExts <$> Inps.prepend inputTxtLines Inps.fail + r <- IORef.newIORef [] + let logger = \_ -> pure () + Debug.bareDebugger inps (Outps.accumulate r) logger + outs <- List.reverse <$> IORef.readIORef r + let outsTxt = map (PP.renderStrict . PP.layoutPretty PP.defaultLayoutOptions . PP.pretty) outs + let inOuts = zipWith (\i o -> "> " <> i <> "\n\n" <> o <> "\n") inputTxtLines outsTxt + pure (Text.encodeUtf8 (Text.unlines inOuts)) + +mkTest :: FilePath -> FilePath -> Tasty.TestTree +mkTest dir path = + Golden.goldenVsStringDiff + path + (\x y -> ["diff", "-u", x, y]) + (dir ++ path) + (BS.fromStrict <$> runScript (dir ++ path)) + +loadTests :: FilePath -> IO Tasty.TestTree +loadTests dir = do + files <- Dir.listDirectory dir + let dbgScripts = List.filter (".txt" `List.isSuffixOf`) files + let tests = map (uncurry mkTest) (map (dir,) dbgScripts) + pure (Tasty.testGroup dir tests) + +main :: IO () +main = do + mainTests <- loadTests testDir + completeTests <- loadTests (testDir ++ "complete/") + errorTests <- loadTests (testDir ++ "error/") + styleTests <- loadTests (testDir ++ "style/") + let tests = [mainTests, completeTests, errorTests, styleTests] + Tasty.defaultMain (Tasty.testGroup "Tests" tests)