From d9d63fd13fe3e8a7178104acc2213f2e928f4014 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Fri, 7 Feb 2025 14:58:11 -0500
Subject: [PATCH] debug: Take a number of steps as an argument to `step`
 (#1298)

Fixes #1287
---
 crucible-debug/src/Lang/Crucible/Debug.hs     |  7 +++++-
 .../src/Lang/Crucible/Debug/Command/Base.hs   |  4 ++--
 .../src/Lang/Crucible/Debug/Context.hs        |  2 +-
 .../src/Lang/Crucible/Debug/Eval.hs           |  8 +++++--
 crucible-debug/test-data/help.txt             |  2 +-
 crucible-debug/test-data/reg.txt              | 22 +++----------------
 crucible-debug/test-data/step.txt             |  6 +----
 crucible-debug/test-data/usage.txt            |  2 +-
 8 files changed, 21 insertions(+), 32 deletions(-)

diff --git a/crucible-debug/src/Lang/Crucible/Debug.hs b/crucible-debug/src/Lang/Crucible/Debug.hs
index 39ef11a12..0890404a2 100644
--- a/crucible-debug/src/Lang/Crucible/Debug.hs
+++ b/crucible-debug/src/Lang/Crucible/Debug.hs
@@ -233,9 +233,14 @@ dispatch ctx0 execState =
     Ctxt.Running {} | C.ResultState {} <- execState -> do
       let ctx = ctx0 { Ctxt.dbgState = Ctxt.Stopped }
       dispatch ctx execState
-    Ctxt.Running Ctxt.Step -> do
+    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 }
diff --git a/crucible-debug/src/Lang/Crucible/Debug/Command/Base.hs b/crucible-debug/src/Lang/Crucible/Debug/Command/Base.hs
index c475dad06..4f5d7263d 100644
--- a/crucible-debug/src/Lang/Crucible/Debug/Command/Base.hs
+++ b/crucible-debug/src/Lang/Crucible/Debug/Command/Base.hs
@@ -216,7 +216,7 @@ help =
     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 one step of execution"
+    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"
@@ -325,7 +325,7 @@ rSecret = knownRepr
 rSource :: Rgx.RegexRepr ArgTypeRepr AType.Path
 rSource = knownRepr
 
-rStep :: Rgx.RegexRepr ArgTypeRepr Rgx.Empty
+rStep :: Rgx.RegexRepr ArgTypeRepr (Rgx.Empty Rgx.:| AType.Int)
 rStep = knownRepr
 
 rTrace :: Rgx.RegexRepr ArgTypeRepr (Rgx.Empty Rgx.:| AType.Int)
diff --git a/crucible-debug/src/Lang/Crucible/Debug/Context.hs b/crucible-debug/src/Lang/Crucible/Debug/Context.hs
index d96a7dce1..a7a3a4fad 100644
--- a/crucible-debug/src/Lang/Crucible/Debug/Context.hs
+++ b/crucible-debug/src/Lang/Crucible/Debug/Context.hs
@@ -57,7 +57,7 @@ data RunningState
     -- | User issued 'Cmd.Run'
   | Run
     -- | User issued 'Cmd.Step'
-  | Step
+  | Step {-# UNPACK #-} !Int
 
 data DebuggerState
   = Running RunningState
diff --git a/crucible-debug/src/Lang/Crucible/Debug/Eval.hs b/crucible-debug/src/Lang/Crucible/Debug/Eval.hs
index d4f190c5d..0889bf58c 100644
--- a/crucible-debug/src/Lang/Crucible/Debug/Eval.hs
+++ b/crucible-debug/src/Lang/Crucible/Debug/Eval.hs
@@ -262,8 +262,12 @@ baseImpl =
     BCmd.Step ->
       Ctxt.CommandImpl
       { Ctxt.implRegex = BCmd.rStep
-      , Ctxt.implBody = \ctx execState Rgx.MEmpty ->
-          runCmd ctx execState Ctxt.Step
+      , 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 ->
diff --git a/crucible-debug/test-data/help.txt b/crucible-debug/test-data/help.txt
index 7bd1df361..8d2dbcc67 100644
--- a/crucible-debug/test-data/help.txt
+++ b/crucible-debug/test-data/help.txt
@@ -22,7 +22,7 @@ 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 one step of execution
+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
 
diff --git a/crucible-debug/test-data/reg.txt b/crucible-debug/test-data/reg.txt
index 108da4b61..1f4fb21fa 100644
--- a/crucible-debug/test-data/reg.txt
+++ b/crucible-debug/test-data/reg.txt
@@ -18,11 +18,7 @@ Ok
 
 Ok
 
-> step
-
-Ok
-
-> step
+> step 2
 
 Ok
 
@@ -30,11 +26,7 @@ Ok
 
 
 
-> step
-
-Ok
-
-> step
+> step 2
 
 Ok
 
@@ -52,15 +44,7 @@ cp@0:b
 cx@1:i
 cp@0:b
 
-> step
-
-Ok
-
-> step
-
-Ok
-
-> step
+> step 3
 
 Ok
 
diff --git a/crucible-debug/test-data/step.txt b/crucible-debug/test-data/step.txt
index 6f202daac..e12745a05 100644
--- a/crucible-debug/test-data/step.txt
+++ b/crucible-debug/test-data/step.txt
@@ -2,11 +2,7 @@
 
 Ok
 
-> step
-
-Ok
-
-> step
+> step 2
 
 Ok
 
diff --git a/crucible-debug/test-data/usage.txt b/crucible-debug/test-data/usage.txt
index 47a36cf5b..a4020a54f 100644
--- a/crucible-debug/test-data/usage.txt
+++ b/crucible-debug/test-data/usage.txt
@@ -8,7 +8,7 @@ help COMMAND?
 
 > usage step
 
-step 
+step INT?
 
 > usage secret