crux: Add a --debug flag to drop into the Crucible debugger (#1297)

* crux: Add a `--debug` flag to drop into the Crucible debugger

* crux{,-llvm}: Update READMEs and CHANGELOGs to mention `--debug`

* crux*: More documentation re: `--debug`

crucible-debug/src/Lang/Crucible/Debug.hs

@@ -51,6 +51,7 @@ module Lang.Crucible.Debug
   , Trace.Trace
   , Trace.TraceEntry(..)
   , Trace.latest
+  , IntrinsicPrinters(..)
   ) where
 
 import Control.Applicative qualified as Applicative
@@ -90,7 +91,7 @@ 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.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

crux-llvm/CHANGELOG.md

@@ -1,6 +1,7 @@
 # next -- TBA
 
 * Add support for the Bitwuzla SMT solver in the test suite.
+* Add `--debug` option for starting the Crucible debugger.
 
 # 0.9 -- 2024-08-30
 

crux-llvm/README.md

@@ -406,6 +406,8 @@ In addition, the following flags can optionally be provided:
   a symbolic filesystem to use during symbolic execution.  See the Symbolic I/O
   documentation for the format of this directory. [Experimental]
 
+* `--debug`: Start the Crucible debugger.
+
 # Environment Variables
 
 The following environment variables are supported:

crux-mir/CHANGELOG.md

@@ -1,3 +1,7 @@
+# next -- TBA
+
+* Add `--debug` option for starting the Crucible debugger.
+
 # 0.9 -- 2024-08-30
 
 * Add support for GHC 9.8

crux/CHANGELOG.md

@@ -1,6 +1,9 @@
 # next -- TBA
 
 * Add support for the Bitwuzla SMT solver.
+* Add `--debug` option for starting the Crucible debugger.
+* For the sake of the `--debug` flag, Crux now depends on the
+  `crucible-{debug,syntax}` packages.
 
 # 0.7.1 -- 2024-08-30
 

crux/crux.cabal

@@ -34,6 +34,8 @@ library
     containers,
     contravariant >= 1.5 && < 1.6,
     crucible,
+    crucible-debug,
+    crucible-syntax,
     directory,
     filepath,
     generic-lens,

crux/src/Crux.hs

@@ -28,6 +28,7 @@ module Crux
   , module Crux.Log
   ) where
 
+import qualified Control.Applicative as Applicative
 import qualified Control.Exception as Ex
 import           Control.Lens
 import           Control.Monad ( unless, void, when )
@@ -53,20 +54,23 @@ import           System.FilePath ((</>))
 import           System.IO ( Handle, hPutStr, stdout, stderr )
 
 import           Data.Parameterized.Classes
+import qualified Data.Parameterized.Map as MapF
 import           Data.Parameterized.Nonce (newIONonceGenerator, NonceGenerator)
 import           Data.Parameterized.Some ( Some(..) )
 
 import           Lang.Crucible.Backend
 import           Lang.Crucible.Backend.Online
 import qualified Lang.Crucible.Backend.Simple as CBS
 import           Lang.Crucible.CFG.Extension
+import qualified Lang.Crucible.Debug as Debug
 import           Lang.Crucible.Simulator
 import           Lang.Crucible.Simulator.BoundedExec
 import           Lang.Crucible.Simulator.BoundedRecursion
 import           Lang.Crucible.Simulator.PathSatisfiability
 import           Lang.Crucible.Simulator.PathSplitting
 import           Lang.Crucible.Simulator.PositionTracking
 import           Lang.Crucible.Simulator.Profiling
+import qualified Lang.Crucible.Syntax.Concrete as Syn
 import           Lang.Crucible.Types
 
 
@@ -675,14 +679,38 @@ doSimWithResults cruxOpts simCallback bak execFeatures profInfo monline goalProv
     RunnableStateWithExtensions initSt exts <- setup bak monline
     explainFailure <- onError bak
 
+    -- This can't be initialized with the rest of the execution features,
+    -- because it is not a 'GenericExecutionFeature'.
+    --
+    -- Ideally, we would use language-extension-specific command extensions
+    -- (e.g., LLVM commands for Crux-LLVM) and parser hooks, but that would
+    -- require some refactoring to pass those in...
+    let debugging = debug cruxOpts
+    debugger <-
+      if debugging
+      then do
+        let ?parserHooks = Syn.ParserHooks Applicative.empty Applicative.empty
+        let cExts = Debug.voidExts
+        inps <- Debug.defaultDebuggerInputs cExts
+        dbg <-
+          Debug.debugger
+            cExts
+            Debug.voidImpl
+            (Debug.IntrinsicPrinters MapF.empty)
+            inps
+            Debug.defaultDebuggerOutputs
+            UnitRepr
+        pure [dbg]
+      else pure []
+
     -- execute the simulator
     case pathStrategy cruxOpts of
       AlwaysMergePaths ->
-        do res <- executeCrucible (map genericToExecutionFeature execFeatures ++ exts) initSt
+        do res <- executeCrucible (map genericToExecutionFeature execFeatures ++ exts ++ debugger) initSt
            void $ resultCont compRef glsRef frm explainFailure (Result res)
       SplitAndExploreDepthFirst ->
         do (i,ws) <- executeCrucibleDFSPaths
-                         (map genericToExecutionFeature execFeatures ++ exts)
+                         (map genericToExecutionFeature execFeatures ++ exts ++ debugger)
                          initSt
                          (resultCont compRef glsRef frm explainFailure . Result)
            sayCrux (Log.TotalPathsExplored i)

crux/src/Crux/Config/Common.hs

@@ -205,6 +205,9 @@ data CruxOptions = CruxOptions
   , outputOptions            :: OutputOptions
     -- ^ Output options grouped together for easy transfer to the logger
 
+  , debug                    :: Bool
+    -- ^ Drop into the Crucible debugger before simulation begins
+
   }
   deriving (Generic)
 
@@ -364,6 +367,10 @@ cruxOptions = Config
 
           onlineProblemFeatures <- pure noFeatures
 
+          debug <-
+            section "debug" yesOrNoSpec False
+            "Drop into the Crucible debugger before simulation begins"
+
           pure CruxOptions
             { outputOptions = OutputOptions
               { colorOptions = ColorOptions
@@ -525,6 +532,10 @@ cruxOptions = Config
          ++ " i.e. one of [real|ieee|uninterpreted|default]. "
          ++ "Default representation is solver specific: [cvc4|yices]=>real, z3=>ieee.")
         $ ReqArg "FPREP" $ \v opts -> Right opts { floatMode = map toLower v }
+
+      , Option [] ["debug"]
+        "Drop into the Crucible debugger before simulation begins"
+        $ NoArg $ \opts -> Right opts { debug = True }
       ]
   }