From 2c0b7d1fcfa18973f9f61316d800513590a780bf Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Fri, 27 Feb 2026 12:19:21 +0100
Subject: [PATCH 1/4] [spectec] More functionality for the debugger

---
 spectec/src/backend-interpreter/debugger.ml | 193 ++++++++++++++------
 spectec/src/backend-interpreter/ds.ml       |   2 +-
 2 files changed, 135 insertions(+), 60 deletions(-)

diff --git a/spectec/src/backend-interpreter/debugger.ml b/spectec/src/backend-interpreter/debugger.ml
index 71dcdf1457..5137cf4d0f 100644
--- a/spectec/src/backend-interpreter/debugger.ml
+++ b/spectec/src/backend-interpreter/debugger.ml
@@ -19,26 +19,41 @@ let state = ref (Step 1)
 
 let help_msg =
   "
-  h
-  help: print help message
-  b {algorithm name}*
-  break {algorithm name}*: add break points
-  rm {algorithm name}*
-  remove {algorithm name}*: remove break points
-  bp
-  breakpoints: print all break points
-  s {number}?
-  step {number}?: take n steps
-  si {number}?
-  stepinstr {number}?: step n AL instructions
-  c {number}?
-  continue {number}?: continue steps until meet n break points
-  al: print al context stack
-  wasm: print wasm context stack
-  store {field} {index}: print a value in store
-  lookup {variable name}: lookup the variable
-  q
-  quit: quit
+  s[tep] {number}?
+    Take n steps
+  si|stepinstr {number}?
+    Step over n AL instructions
+  c[ontinue] {number}?
+    Continue until the n-th break point
+  b[reak] {algorithm name}*
+    Add break points
+  rm|remove {algorithm name}*
+    Remove break points
+  bp|breakpoints
+    Print all break points
+  al
+    Print AL context stack
+  wasm
+    Print Wasm context stack
+  v[ar] {variable name} {field|index}*
+    Print a value selected from an AL variable
+  f[rame] {field|index}*
+    Print a value selected from the current Wasm frame
+  l[ocal] {index} {field|index}*
+    Print a value selected from the current Wasm frame's locals
+    (shorthand for `frame LOCALS`)
+  m[odule] {field} {index}
+    Print an index from the current Wasm frame's module
+    (shorthand for `frame MODULE`)
+  st[ore] {field|index}*
+    Print a value from the Wasm store
+  z|state {field|index}*
+    Print a value indexed from the current Wasm frame's module
+    (shorthand for the composition of module and store lookup)
+  q[uit]
+    Quit
+  h[elp]
+    Print help message
   "
 
 let allow_command ctx =
@@ -67,81 +82,141 @@ let allow_command ctx =
     )
   | _ -> false
 
+let rec access_paths paths v =
+  match paths with
+  | [] -> v
+  | path :: t when int_of_string_opt path <> None ->
+    v
+    |> unwrap_listv
+    |> (fun arr -> Array.get !arr (int_of_string path))
+    |> access_paths t
+  | path :: t ->
+    v
+    |> unwrap_strv
+    |> List.assoc path
+    |> (!)
+    |> access_paths t
+
+let access_store paths =
+  Store.access (List.hd paths)
+  |> access_paths (List.tl paths)
+
+let access_frame paths =
+  WasmContext.get_current_context "FRAME_"
+  |> args_of_casev
+  |> Fun.flip List.nth 1
+  |> access_paths paths
+
+let access_state paths =
+  if List.length paths < 2 then access_frame ("MODULE" :: paths) else
+  let field = List.hd paths in
+  access_frame ["MODULE"; field; List.nth paths 1]
+  |> unwrap_natv_to_int
+  |> (fun i -> access_store (field :: string_of_int i :: Util.Lib.List.drop 2 paths))
+
+let access_env (ctx : AlContext.t) s paths =
+  match ctx with
+  | (Al (_, _, _, env, _) | Enter (_, _, env)) :: _ ->
+    lookup_env_opt s env |> Option.get |> access_paths paths
+  | _ -> failwith "not in scope"
+
+let print_path path =
+  if int_of_string_opt path <> None then
+    "[" ^ path ^ "]"
+  else
+    "." ^ path
+
+let print_value access root paths =
+  print_endline (
+    root ^ String.concat "" (List.map print_path paths) ^
+    try " = " ^ string_of_value (access paths)
+    with _ -> " does not exist"
+  )
+
 let rec do_debug ctx =
   let _ = print_string "\ndebugger> " in
   read_line ()
   |> String.split_on_char ' '
-  |> handle_command ctx;
+  |> List.filter ((<>) "")
+  |> handle_command ctx
+
 and handle_command ctx = function
   | ("h" | "help") :: _ ->
     print_endline help_msg;
     do_debug ctx
-  | ("b" | "break") :: t -> break_points := !break_points @ t; do_debug ctx
-  | ("rm" | "remove") :: t ->
-    break_points := List.filter (fun e -> not (List.mem e t)) !break_points;
+  | ("b" | "break") :: t ->
+    if t = [] then
+      print_endline (String.concat " " !break_points)
+    else
+      break_points := !break_points @ t;
     do_debug ctx
-  | ("bp" | "breakpoints") :: _ ->
+  | ("bp" | "breakpoints") :: [] ->
     print_endline (String.concat " " !break_points);
     do_debug ctx
+  | ("rm" | "remove") :: t ->
+    break_points := List.filter (fun e -> not (List.mem e t)) !break_points;
+    do_debug ctx
   | ("s" | "step") :: t ->
     (match t with
-    | n :: _ when Option.is_some (int_of_string_opt n) ->
+    | [] ->
+      state := Step 1
+    | [n] when int_of_string_opt n <> None ->
       state := Step (int_of_string n)
     | _ ->
-      state := Step 1
+      handle_command ctx ["help"]
     )
   | ("si" | "stepinstr") :: t ->
     (match ctx with
     | (AlContext.Al (name, _, il, _, _) | AlContext.Enter (name, il, _)) :: _
-    when List.length il > 0 ->
+      when List.length il > 0 ->
       (match t with
-      | n :: _ when Option.is_some (int_of_string_opt n) ->
+      | [] ->
+        state := StepInstr (name, 1)
+      | [n] when int_of_string_opt n <> None ->
         state := StepInstr (name, int_of_string n)
       | _ ->
-        state := StepInstr (name, 1)
+        handle_command ctx ["help"]
       )
     | _ ->
       handle_command ctx ("step" :: t)
     )
   | ("c" | "continue") :: t ->
     (match t with
-    | n :: _ when Option.is_some (int_of_string_opt n) ->
+    | [] ->
+      state := Continue 1
+    | [n] when int_of_string_opt n <> None ->
       state := Continue (int_of_string n)
     | _ ->
-      state := Continue 1
+      handle_command ctx ["help"]
     )
-  | "al" :: _ ->
-    ctx
-    |> List.map AlContext.string_of_context
-    |> List.iter print_endline;
+  | "al" :: [] ->
+    ctx |> List.map AlContext.string_of_context |> List.iter print_endline;
     do_debug ctx
-  | "wasm" :: _ ->
+  | "wasm" :: [] ->
     WasmContext.string_of_context_stack () |> print_endline;
     do_debug ctx
-  | "store" :: field :: n :: _ ->
-    (try
-      let idx = int_of_string n in
-      Store.access field
-      |> unwrap_listv
-      |> (!)
-      |> (fun arr -> Array.get arr idx)
-      |> string_of_value
-      |> print_endline;
-    with _ -> ()
-    );
+  | ("st" | "store") :: t ->
+    print_value access_store "store" t;
     do_debug ctx
-  | "lookup" :: s :: _ ->
-    (match ctx with
-    | (Al (_, _, _, env, _) | Enter (_, _, env)) :: _ ->
-      lookup_env_opt s env
-      |> Option.map string_of_value
-      |> Option.iter print_endline;
-    | _ -> ()
-    );
+  | ("f" | "frame") :: t ->
+    print_value access_frame "frame" t;
+    do_debug ctx
+  | ("l" | "local") :: t ->
+    print_value access_frame "frame" ("LOCALS" :: t);
+    do_debug ctx
+  | ("m" | "module") :: t ->
+    print_value access_frame "frame" ("MODULE" :: t);
     do_debug ctx
-  | ("q" | "quit") :: _ -> debug := false
-  | _ -> do_debug ctx
+  | ("z" | "state") :: t ->
+    print_value access_state "state" t;
+    do_debug ctx
+  | ("v" | "var") :: s :: t ->
+    print_value (access_env ctx s) s t;
+    do_debug ctx
+  | ("q" | "quit") :: [] ->
+    debug := false
+  | _ ->
+    handle_command ctx ["help"]
 
 let run ctx =
-
   if !debug && allow_command ctx then do_debug ctx
diff --git a/spectec/src/backend-interpreter/ds.ml b/spectec/src/backend-interpreter/ds.ml
index ef138a84e4..59fef32eb5 100644
--- a/spectec/src/backend-interpreter/ds.ml
+++ b/spectec/src/backend-interpreter/ds.ml
@@ -205,7 +205,7 @@ module AlContext = struct
 
   let string_of_context = function
     | Al (s, args, il, _, _) ->
-      Printf.sprintf "Al %s (%s):%s"
+      Printf.sprintf "Al %s(%s):%s"
         s
         (args |> List.map string_of_arg |> String.concat ", ")
         (string_of_instrs il)

From a38d35c4acca47ed5c07de0012ea2b608d5cf639 Mon Sep 17 00:00:00 2001
From: ShinWonho <50018375+ShinWonho@users.noreply.github.com>
Date: Thu, 12 Mar 2026 20:54:23 +0900
Subject: [PATCH 2/4] [spectec] Catch error in debugger (#2110)

---
 .../src/backend-interpreter/interpreter.ml    | 63 ++++++++++---------
 1 file changed, 35 insertions(+), 28 deletions(-)

diff --git a/spectec/src/backend-interpreter/interpreter.ml b/spectec/src/backend-interpreter/interpreter.ml
index 16878b2572..e22e8e3a0f 100644
--- a/spectec/src/backend-interpreter/interpreter.ml
+++ b/spectec/src/backend-interpreter/interpreter.ml
@@ -725,36 +725,43 @@ and step (ctx: AlContext.t) : AlContext.t =
 
   Debugger.run ctx;
 
-  match ctx with
-  | Al (name, args, il, env, n) :: ctx ->
-    (match il with
-    | [] -> ctx
-    | [ instr ]
-    when can_tail_call instr && n = 0 && not !Debugger.debug ->
-      try_step_instr name ctx env instr
-    | h :: t ->
-      let new_ctx = Al (name, args, t, env, n) :: ctx in
-      try_step_instr name new_ctx env h
-    )
-  | Wasm n :: ctx ->
-    if n = 0 then
-      ctx
-    else
-      try_step_wasm (Wasm n :: ctx) (WasmContext.pop_instr ())
-  | Enter (name, il, env) :: ctx ->
-    (match il with
-    | [] ->
-      (match ctx with
-      | Wasm n :: t when not !Debugger.debug -> Wasm (n + 1) :: t
-      | Enter (_, [], _) :: t -> Wasm 2 :: t
-      | ctx -> Wasm 1 :: ctx
+  try
+    (match ctx with
+    | Al (name, args, il, env, n) :: ctx ->
+      (match il with
+      | [] -> ctx
+      | [ instr ]
+      when can_tail_call instr && n = 0 && not !Debugger.debug ->
+        try_step_instr name ctx env instr
+      | h :: t ->
+        let new_ctx = Al (name, args, t, env, n) :: ctx in
+        try_step_instr name new_ctx env h
+      )
+    | Wasm n :: ctx ->
+      if n = 0 then
+        ctx
+      else
+        try_step_wasm (Wasm n :: ctx) (WasmContext.pop_instr ())
+    | Enter (name, il, env) :: ctx ->
+      (match il with
+      | [] ->
+        (match ctx with
+        | Wasm n :: t when not !Debugger.debug -> Wasm (n + 1) :: t
+        | Enter (_, [], _) :: t -> Wasm 2 :: t
+        | ctx -> Wasm 1 :: ctx
+        )
+      | h :: t ->
+        let new_ctx = Enter (name, t, env) :: ctx in
+        try_step_instr name new_ctx env h
       )
-    | h :: t ->
-      let new_ctx = Enter (name, t, env) :: ctx in
-      try_step_instr name new_ctx env h
+    | Execute v :: ctx -> try_step_wasm ctx v
+    | _ -> assert false
     )
-  | Execute v :: ctx -> try_step_wasm ctx v
-  | _ -> assert false
+  with exn ->
+    let bt = Printexc.get_raw_backtrace () in
+    print_endline (Printexc.to_string exn);
+    if !Debugger.debug then Debugger.do_debug ctx;
+    Printexc.raise_with_backtrace exn bt
 
 
 (* AL interpreter Entry *)

From 63fbb2b78fd4f70adbd8a7e112d4b2b134d42ba7 Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Thu, 12 Mar 2026 13:04:06 +0100
Subject: [PATCH 3/4] Move access functions to Ds

---
 spectec/src/backend-interpreter/debugger.ml | 76 ++++++---------------
 spectec/src/backend-interpreter/ds.ml       | 43 ++++++++++++
 spectec/src/backend-interpreter/ds.mli      |  7 ++
 3 files changed, 69 insertions(+), 57 deletions(-)

diff --git a/spectec/src/backend-interpreter/debugger.ml b/spectec/src/backend-interpreter/debugger.ml
index 5137cf4d0f..afe3380a1c 100644
--- a/spectec/src/backend-interpreter/debugger.ml
+++ b/spectec/src/backend-interpreter/debugger.ml
@@ -56,6 +56,19 @@ let help_msg =
     Print help message
   "
 
+let print_path path =
+  if int_of_string_opt path <> None then
+    "[" ^ path ^ "]"
+  else
+    "." ^ path
+
+let print_value access root paths =
+  print_endline (
+    root ^ String.concat "" (List.map print_path paths) ^
+    try " = " ^ string_of_value (access paths)
+    with _ -> " does not exist"
+  )
+
 let allow_command ctx =
   let is_entry name il = name |> lookup_algo |> body_of_algo = il in
 
@@ -82,57 +95,6 @@ let allow_command ctx =
     )
   | _ -> false
 
-let rec access_paths paths v =
-  match paths with
-  | [] -> v
-  | path :: t when int_of_string_opt path <> None ->
-    v
-    |> unwrap_listv
-    |> (fun arr -> Array.get !arr (int_of_string path))
-    |> access_paths t
-  | path :: t ->
-    v
-    |> unwrap_strv
-    |> List.assoc path
-    |> (!)
-    |> access_paths t
-
-let access_store paths =
-  Store.access (List.hd paths)
-  |> access_paths (List.tl paths)
-
-let access_frame paths =
-  WasmContext.get_current_context "FRAME_"
-  |> args_of_casev
-  |> Fun.flip List.nth 1
-  |> access_paths paths
-
-let access_state paths =
-  if List.length paths < 2 then access_frame ("MODULE" :: paths) else
-  let field = List.hd paths in
-  access_frame ["MODULE"; field; List.nth paths 1]
-  |> unwrap_natv_to_int
-  |> (fun i -> access_store (field :: string_of_int i :: Util.Lib.List.drop 2 paths))
-
-let access_env (ctx : AlContext.t) s paths =
-  match ctx with
-  | (Al (_, _, _, env, _) | Enter (_, _, env)) :: _ ->
-    lookup_env_opt s env |> Option.get |> access_paths paths
-  | _ -> failwith "not in scope"
-
-let print_path path =
-  if int_of_string_opt path <> None then
-    "[" ^ path ^ "]"
-  else
-    "." ^ path
-
-let print_value access root paths =
-  print_endline (
-    root ^ String.concat "" (List.map print_path paths) ^
-    try " = " ^ string_of_value (access paths)
-    with _ -> " does not exist"
-  )
-
 let rec do_debug ctx =
   let _ = print_string "\ndebugger> " in
   read_line ()
@@ -196,22 +158,22 @@ and handle_command ctx = function
     WasmContext.string_of_context_stack () |> print_endline;
     do_debug ctx
   | ("st" | "store") :: t ->
-    print_value access_store "store" t;
+    print_value Access.access_store "store" t;
     do_debug ctx
   | ("f" | "frame") :: t ->
-    print_value access_frame "frame" t;
+    print_value Access.access_frame "frame" t;
     do_debug ctx
   | ("l" | "local") :: t ->
-    print_value access_frame "frame" ("LOCALS" :: t);
+    print_value Access.access_frame "frame" ("LOCALS" :: t);
     do_debug ctx
   | ("m" | "module") :: t ->
-    print_value access_frame "frame" ("MODULE" :: t);
+    print_value Access.access_frame "frame" ("MODULE" :: t);
     do_debug ctx
   | ("z" | "state") :: t ->
-    print_value access_state "state" t;
+    print_value Access.access_state "state" t;
     do_debug ctx
   | ("v" | "var") :: s :: t ->
-    print_value (access_env ctx s) s t;
+    print_value (Access.access_env ctx s) s t;
     do_debug ctx
   | ("q" | "quit") :: [] ->
     debug := false
diff --git a/spectec/src/backend-interpreter/ds.ml b/spectec/src/backend-interpreter/ds.ml
index 59fef32eb5..bbfd7e7bdd 100644
--- a/spectec/src/backend-interpreter/ds.ml
+++ b/spectec/src/backend-interpreter/ds.ml
@@ -413,3 +413,46 @@ let init algos =
 
   (* Initialize store *)
   Store.init ()
+
+
+(* Debugger aids *)
+
+module Access = struct
+  let rec access_paths paths v =
+    match paths with
+    | [] -> v
+    | path :: t when int_of_string_opt path <> None ->
+      v
+      |> unwrap_listv
+      |> (fun arr -> Array.get !arr (int_of_string path))
+      |> access_paths t
+    | path :: t ->
+      v
+      |> unwrap_strv
+      |> List.assoc path
+      |> (!)
+      |> access_paths t
+
+  let access_store paths =
+    Store.access (List.hd paths)
+    |> access_paths (List.tl paths)
+
+  let access_frame paths =
+    WasmContext.get_current_context "FRAME_"
+    |> args_of_casev
+    |> Fun.flip List.nth 1
+    |> access_paths paths
+
+  let access_state paths =
+    if List.length paths < 2 then access_frame ("MODULE" :: paths) else
+    let field = List.hd paths in
+    access_frame ["MODULE"; field; List.nth paths 1]
+    |> unwrap_natv_to_int
+    |> (fun i -> access_store (field :: string_of_int i :: Util.Lib.List.drop 2 paths))
+
+  let access_env (ctx : AlContext.t) s paths =
+    match ctx with
+    | (Al (_, _, _, env, _) | Enter (_, _, env)) :: _ ->
+      lookup_env_opt s env |> Option.get |> access_paths paths
+    | _ -> failwith "not in scope"
+end
diff --git a/spectec/src/backend-interpreter/ds.mli b/spectec/src/backend-interpreter/ds.mli
index a4e5d11824..fae46fc49f 100644
--- a/spectec/src/backend-interpreter/ds.mli
+++ b/spectec/src/backend-interpreter/ds.mli
@@ -91,4 +91,11 @@ module WasmContext : sig
   val pop_instr : unit -> value
 end
 
+module Access : sig
+  val access_store : string list -> value
+  val access_frame : string list -> value
+  val access_state : string list -> value
+  val access_env : AlContext.t -> string -> string list -> value
+end
+
 val init : algorithm list -> unit

From def7d0aec2d8f368f045669af1537d872b41874d Mon Sep 17 00:00:00 2001
From: Andreas Rossberg <rossberg@mpi-sws.org>
Date: Thu, 12 Mar 2026 13:09:57 +0100
Subject: [PATCH 4/4] Avoid extra output when debugger isn't active

---
 spectec/src/backend-interpreter/interpreter.ml | 7 +++----
 1 file changed, 3 insertions(+), 4 deletions(-)

diff --git a/spectec/src/backend-interpreter/interpreter.ml b/spectec/src/backend-interpreter/interpreter.ml
index e22e8e3a0f..4cedf25b7e 100644
--- a/spectec/src/backend-interpreter/interpreter.ml
+++ b/spectec/src/backend-interpreter/interpreter.ml
@@ -726,7 +726,7 @@ and step (ctx: AlContext.t) : AlContext.t =
   Debugger.run ctx;
 
   try
-    (match ctx with
+    match ctx with
     | Al (name, args, il, env, n) :: ctx ->
       (match il with
       | [] -> ctx
@@ -756,11 +756,10 @@ and step (ctx: AlContext.t) : AlContext.t =
       )
     | Execute v :: ctx -> try_step_wasm ctx v
     | _ -> assert false
-    )
-  with exn ->
+  with exn when !Debugger.debug ->
     let bt = Printexc.get_raw_backtrace () in
     print_endline (Printexc.to_string exn);
-    if !Debugger.debug then Debugger.do_debug ctx;
+    Debugger.do_debug ctx;
     Printexc.raise_with_backtrace exn bt