[spectec] More functionality for the debugger

spectec/src/backend-interpreter/debugger.ml

@@ -19,28 +19,56 @@ 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 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
 
@@ -71,77 +99,86 @@ 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.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.access_frame "frame" t;
     do_debug ctx
-  | ("q" | "quit") :: _ -> debug := false
-  | _ -> do_debug ctx
+  | ("l" | "local") :: t ->
+    print_value Access.access_frame "frame" ("LOCALS" :: t);
+    do_debug ctx
+  | ("m" | "module") :: t ->
+    print_value Access.access_frame "frame" ("MODULE" :: t);
+    do_debug ctx
+  | ("z" | "state") :: t ->
+    print_value Access.access_state "state" t;
+    do_debug ctx
+  | ("v" | "var") :: s :: t ->
+    print_value (Access.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

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

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

spectec/src/backend-interpreter/interpreter.ml

@@ -725,36 +725,42 @@ 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
       )
-    | 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
+    | 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
+      )
+    | Execute v :: ctx -> try_step_wasm ctx v
+    | _ -> assert false
+  with exn when !Debugger.debug ->
+    let bt = Printexc.get_raw_backtrace () in
+    print_endline (Printexc.to_string exn);
+    Debugger.do_debug ctx;
+    Printexc.raise_with_backtrace exn bt
 
 
 (* AL interpreter Entry *)