Skip to content

Commit 12b9dbc

Browse files
rossbergShinWonho
rossberg
and
ShinWonho
authored
[spectec] More functionality for the debugger (#2096)
Co-authored-by: ShinWonho <50018375+ShinWonho@users.noreply.github.com>
1 parent 44801dd commit 12b9dbc

4 files changed

Lines changed: 182 additions & 89 deletions

File tree

‎spectec/src/backend-interpreter/debugger.ml‎

Lines changed: 96 additions & 59 deletions
Original file line numberDiff line numberDiff line change
@@ -19,28 +19,56 @@ let state = ref (Step 1)
1919

2020
let help_msg =
2121
"
22-
h
23-
help: print help message
24-
b {algorithm name}*
25-
break {algorithm name}*: add break points
26-
rm {algorithm name}*
27-
remove {algorithm name}*: remove break points
28-
bp
29-
breakpoints: print all break points
30-
s {number}?
31-
step {number}?: take n steps
32-
si {number}?
33-
stepinstr {number}?: step n AL instructions
34-
c {number}?
35-
continue {number}?: continue steps until meet n break points
36-
al: print al context stack
37-
wasm: print wasm context stack
38-
store {field} {index}: print a value in store
39-
lookup {variable name}: lookup the variable
40-
q
41-
quit: quit
22+
s[tep] {number}?
23+
Take n steps
24+
si|stepinstr {number}?
25+
Step over n AL instructions
26+
c[ontinue] {number}?
27+
Continue until the n-th break point
28+
b[reak] {algorithm name}*
29+
Add break points
30+
rm|remove {algorithm name}*
31+
Remove break points
32+
bp|breakpoints
33+
Print all break points
34+
al
35+
Print AL context stack
36+
wasm
37+
Print Wasm context stack
38+
v[ar] {variable name} {field|index}*
39+
Print a value selected from an AL variable
40+
f[rame] {field|index}*
41+
Print a value selected from the current Wasm frame
42+
l[ocal] {index} {field|index}*
43+
Print a value selected from the current Wasm frame's locals
44+
(shorthand for `frame LOCALS`)
45+
m[odule] {field} {index}
46+
Print an index from the current Wasm frame's module
47+
(shorthand for `frame MODULE`)
48+
st[ore] {field|index}*
49+
Print a value from the Wasm store
50+
z|state {field|index}*
51+
Print a value indexed from the current Wasm frame's module
52+
(shorthand for the composition of module and store lookup)
53+
q[uit]
54+
Quit
55+
h[elp]
56+
Print help message
4257
"
4358

59+
let print_path path =
60+
if int_of_string_opt path <> None then
61+
"[" ^ path ^ "]"
62+
else
63+
"." ^ path
64+
65+
let print_value access root paths =
66+
print_endline (
67+
root ^ String.concat "" (List.map print_path paths) ^
68+
try " = " ^ string_of_value (access paths)
69+
with _ -> " does not exist"
70+
)
71+
4472
let allow_command ctx =
4573
let is_entry name il = name |> lookup_algo |> body_of_algo = il in
4674

@@ -71,77 +99,86 @@ let rec do_debug ctx =
7199
let _ = print_string "\ndebugger> " in
72100
read_line ()
73101
|> String.split_on_char ' '
74-
|> handle_command ctx;
102+
|> List.filter ((<>) "")
103+
|> handle_command ctx
104+
75105
and handle_command ctx = function
76106
| ("h" | "help") :: _ ->
77107
print_endline help_msg;
78108
do_debug ctx
79-
| ("b" | "break") :: t -> break_points := !break_points @ t; do_debug ctx
80-
| ("rm" | "remove") :: t ->
81-
break_points := List.filter (fun e -> not (List.mem e t)) !break_points;
109+
| ("b" | "break") :: t ->
110+
if t = [] then
111+
print_endline (String.concat " " !break_points)
112+
else
113+
break_points := !break_points @ t;
82114
do_debug ctx
83-
| ("bp" | "breakpoints") :: _ ->
115+
| ("bp" | "breakpoints") :: [] ->
84116
print_endline (String.concat " " !break_points);
85117
do_debug ctx
118+
| ("rm" | "remove") :: t ->
119+
break_points := List.filter (fun e -> not (List.mem e t)) !break_points;
120+
do_debug ctx
86121
| ("s" | "step") :: t ->
87122
(match t with
88-
| n :: _ when Option.is_some (int_of_string_opt n) ->
123+
| [] ->
124+
state := Step 1
125+
| [n] when int_of_string_opt n <> None ->
89126
state := Step (int_of_string n)
90127
| _ ->
91-
state := Step 1
128+
handle_command ctx ["help"]
92129
)
93130
| ("si" | "stepinstr") :: t ->
94131
(match ctx with
95132
| (AlContext.Al (name, _, il, _, _) | AlContext.Enter (name, il, _)) :: _
96-
when List.length il > 0 ->
133+
when List.length il > 0 ->
97134
(match t with
98-
| n :: _ when Option.is_some (int_of_string_opt n) ->
135+
| [] ->
136+
state := StepInstr (name, 1)
137+
| [n] when int_of_string_opt n <> None ->
99138
state := StepInstr (name, int_of_string n)
100139
| _ ->
101-
state := StepInstr (name, 1)
140+
handle_command ctx ["help"]
102141
)
103142
| _ ->
104143
handle_command ctx ("step" :: t)
105144
)
106145
| ("c" | "continue") :: t ->
107146
(match t with
108-
| n :: _ when Option.is_some (int_of_string_opt n) ->
147+
| [] ->
148+
state := Continue 1
149+
| [n] when int_of_string_opt n <> None ->
109150
state := Continue (int_of_string n)
110151
| _ ->
111-
state := Continue 1
152+
handle_command ctx ["help"]
112153
)
113-
| "al" :: _ ->
114-
ctx
115-
|> List.map AlContext.string_of_context
116-
|> List.iter print_endline;
154+
| "al" :: [] ->
155+
ctx |> List.map AlContext.string_of_context |> List.iter print_endline;
117156
do_debug ctx
118-
| "wasm" :: _ ->
157+
| "wasm" :: [] ->
119158
WasmContext.string_of_context_stack () |> print_endline;
120159
do_debug ctx
121-
| "store" :: field :: n :: _ ->
122-
(try
123-
let idx = int_of_string n in
124-
Store.access field
125-
|> unwrap_listv
126-
|> (!)
127-
|> (fun arr -> Array.get arr idx)
128-
|> string_of_value
129-
|> print_endline;
130-
with _ -> ()
131-
);
160+
| ("st" | "store") :: t ->
161+
print_value Access.access_store "store" t;
132162
do_debug ctx
133-
| "lookup" :: s :: _ ->
134-
(match ctx with
135-
| (Al (_, _, _, env, _) | Enter (_, _, env)) :: _ ->
136-
lookup_env_opt s env
137-
|> Option.map string_of_value
138-
|> Option.iter print_endline;
139-
| _ -> ()
140-
);
163+
| ("f" | "frame") :: t ->
164+
print_value Access.access_frame "frame" t;
141165
do_debug ctx
142-
| ("q" | "quit") :: _ -> debug := false
143-
| _ -> do_debug ctx
166+
| ("l" | "local") :: t ->
167+
print_value Access.access_frame "frame" ("LOCALS" :: t);
168+
do_debug ctx
169+
| ("m" | "module") :: t ->
170+
print_value Access.access_frame "frame" ("MODULE" :: t);
171+
do_debug ctx
172+
| ("z" | "state") :: t ->
173+
print_value Access.access_state "state" t;
174+
do_debug ctx
175+
| ("v" | "var") :: s :: t ->
176+
print_value (Access.access_env ctx s) s t;
177+
do_debug ctx
178+
| ("q" | "quit") :: [] ->
179+
debug := false
180+
| _ ->
181+
handle_command ctx ["help"]
144182

145183
let run ctx =
146-
147184
if !debug && allow_command ctx then do_debug ctx

‎spectec/src/backend-interpreter/ds.ml‎

Lines changed: 44 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -205,7 +205,7 @@ module AlContext = struct
205205

206206
let string_of_context = function
207207
| Al (s, args, il, _, _) ->
208-
Printf.sprintf "Al %s (%s):%s"
208+
Printf.sprintf "Al %s(%s):%s"
209209
s
210210
(args |> List.map string_of_arg |> String.concat ", ")
211211
(string_of_instrs il)
@@ -413,3 +413,46 @@ let init algos =
413413

414414
(* Initialize store *)
415415
Store.init ()
416+
417+
418+
(* Debugger aids *)
419+
420+
module Access = struct
421+
let rec access_paths paths v =
422+
match paths with
423+
| [] -> v
424+
| path :: t when int_of_string_opt path <> None ->
425+
v
426+
|> unwrap_listv
427+
|> (fun arr -> Array.get !arr (int_of_string path))
428+
|> access_paths t
429+
| path :: t ->
430+
v
431+
|> unwrap_strv
432+
|> List.assoc path
433+
|> (!)
434+
|> access_paths t
435+
436+
let access_store paths =
437+
Store.access (List.hd paths)
438+
|> access_paths (List.tl paths)
439+
440+
let access_frame paths =
441+
WasmContext.get_current_context "FRAME_"
442+
|> args_of_casev
443+
|> Fun.flip List.nth 1
444+
|> access_paths paths
445+
446+
let access_state paths =
447+
if List.length paths < 2 then access_frame ("MODULE" :: paths) else
448+
let field = List.hd paths in
449+
access_frame ["MODULE"; field; List.nth paths 1]
450+
|> unwrap_natv_to_int
451+
|> (fun i -> access_store (field :: string_of_int i :: Util.Lib.List.drop 2 paths))
452+
453+
let access_env (ctx : AlContext.t) s paths =
454+
match ctx with
455+
| (Al (_, _, _, env, _) | Enter (_, _, env)) :: _ ->
456+
lookup_env_opt s env |> Option.get |> access_paths paths
457+
| _ -> failwith "not in scope"
458+
end

‎spectec/src/backend-interpreter/ds.mli‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -91,4 +91,11 @@ module WasmContext : sig
9191
val pop_instr : unit -> value
9292
end
9393

94+
module Access : sig
95+
val access_store : string list -> value
96+
val access_frame : string list -> value
97+
val access_state : string list -> value
98+
val access_env : AlContext.t -> string -> string list -> value
99+
end
100+
94101
val init : algorithm list -> unit

‎spectec/src/backend-interpreter/interpreter.ml‎

Lines changed: 35 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -725,36 +725,42 @@ and step (ctx: AlContext.t) : AlContext.t =
725725

726726
Debugger.run ctx;
727727

728-
match ctx with
729-
| Al (name, args, il, env, n) :: ctx ->
730-
(match il with
731-
| [] -> ctx
732-
| [ instr ]
733-
when can_tail_call instr && n = 0 && not !Debugger.debug ->
734-
try_step_instr name ctx env instr
735-
| h :: t ->
736-
let new_ctx = Al (name, args, t, env, n) :: ctx in
737-
try_step_instr name new_ctx env h
738-
)
739-
| Wasm n :: ctx ->
740-
if n = 0 then
741-
ctx
742-
else
743-
try_step_wasm (Wasm n :: ctx) (WasmContext.pop_instr ())
744-
| Enter (name, il, env) :: ctx ->
745-
(match il with
746-
| [] ->
747-
(match ctx with
748-
| Wasm n :: t when not !Debugger.debug -> Wasm (n + 1) :: t
749-
| Enter (_, [], _) :: t -> Wasm 2 :: t
750-
| ctx -> Wasm 1 :: ctx
728+
try
729+
match ctx with
730+
| Al (name, args, il, env, n) :: ctx ->
731+
(match il with
732+
| [] -> ctx
733+
| [ instr ]
734+
when can_tail_call instr && n = 0 && not !Debugger.debug ->
735+
try_step_instr name ctx env instr
736+
| h :: t ->
737+
let new_ctx = Al (name, args, t, env, n) :: ctx in
738+
try_step_instr name new_ctx env h
751739
)
752-
| h :: t ->
753-
let new_ctx = Enter (name, t, env) :: ctx in
754-
try_step_instr name new_ctx env h
755-
)
756-
| Execute v :: ctx -> try_step_wasm ctx v
757-
| _ -> assert false
740+
| Wasm n :: ctx ->
741+
if n = 0 then
742+
ctx
743+
else
744+
try_step_wasm (Wasm n :: ctx) (WasmContext.pop_instr ())
745+
| Enter (name, il, env) :: ctx ->
746+
(match il with
747+
| [] ->
748+
(match ctx with
749+
| Wasm n :: t when not !Debugger.debug -> Wasm (n + 1) :: t
750+
| Enter (_, [], _) :: t -> Wasm 2 :: t
751+
| ctx -> Wasm 1 :: ctx
752+
)
753+
| h :: t ->
754+
let new_ctx = Enter (name, t, env) :: ctx in
755+
try_step_instr name new_ctx env h
756+
)
757+
| Execute v :: ctx -> try_step_wasm ctx v
758+
| _ -> assert false
759+
with exn when !Debugger.debug ->
760+
let bt = Printexc.get_raw_backtrace () in
761+
print_endline (Printexc.to_string exn);
762+
Debugger.do_debug ctx;
763+
Printexc.raise_with_backtrace exn bt
758764

759765

760766
(* AL interpreter Entry *)

0 commit comments

Comments
 (0)