60749
|
1 |
(* Title: Pure/Tools/debugger.ML
|
|
2 |
Author: Makarius
|
|
3 |
|
|
4 |
Interactive debugger for Isabelle/ML.
|
|
5 |
*)
|
|
6 |
|
60830
|
7 |
signature DEBUGGER =
|
|
8 |
sig
|
60834
|
9 |
val writeln_message: string -> unit
|
|
10 |
val warning_message: string -> unit
|
|
11 |
val error_message: string -> unit
|
60830
|
12 |
end;
|
|
13 |
|
|
14 |
structure Debugger: DEBUGGER =
|
60765
|
15 |
struct
|
|
16 |
|
60869
|
17 |
(** global state **)
|
|
18 |
|
|
19 |
(* output messages *)
|
60830
|
20 |
|
60856
|
21 |
val _ = Session.protocol_handler "isabelle.Debugger$Handler";
|
|
22 |
|
60834
|
23 |
fun output_message kind msg =
|
60864
|
24 |
if msg = "" then ()
|
|
25 |
else
|
|
26 |
Output.protocol_message
|
|
27 |
(Markup.debugger_output (Simple_Thread.the_name ()))
|
|
28 |
[Markup.markup (kind, Markup.serial_properties (serial ())) msg];
|
60834
|
29 |
|
|
30 |
val writeln_message = output_message Markup.writelnN;
|
|
31 |
val warning_message = output_message Markup.warningN;
|
|
32 |
val error_message = output_message Markup.errorN;
|
60830
|
33 |
|
60856
|
34 |
fun error_wrapper e = e ()
|
|
35 |
handle exn =>
|
|
36 |
if Exn.is_interrupt exn then reraise exn
|
|
37 |
else error_message (Runtime.exn_message exn);
|
|
38 |
|
60830
|
39 |
|
60869
|
40 |
(* thread names and input *)
|
60765
|
41 |
|
|
42 |
datatype state =
|
|
43 |
State of {
|
60829
|
44 |
threads: Thread.thread Symtab.table, (*thread name ~> thread*)
|
|
45 |
input: string list Queue.T Symtab.table (*thread name ~> input queue*)
|
60765
|
46 |
};
|
|
47 |
|
|
48 |
fun make_state (threads, input) = State {threads = threads, input = input};
|
|
49 |
val init_state = make_state (Symtab.empty, Symtab.empty);
|
|
50 |
fun map_state f (State {threads, input}) = make_state (f (threads, input));
|
|
51 |
|
|
52 |
val global_state = Synchronized.var "Debugger.state" init_state;
|
|
53 |
|
60842
|
54 |
fun cancel thread_name =
|
60765
|
55 |
Synchronized.change global_state (tap (fn State {threads, ...} =>
|
60842
|
56 |
(case Symtab.lookup threads thread_name of
|
60765
|
57 |
NONE => ()
|
|
58 |
| SOME thread => Simple_Thread.interrupt_unsynchronized thread)));
|
|
59 |
|
60842
|
60 |
fun input thread_name msg =
|
60765
|
61 |
Synchronized.change global_state (map_state (fn (threads, input) =>
|
60842
|
62 |
let val input' = Symtab.map_default (thread_name, Queue.empty) (Queue.enqueue msg) input;
|
60765
|
63 |
in (threads, input') end));
|
|
64 |
|
60842
|
65 |
fun get_input thread_name =
|
60765
|
66 |
Synchronized.guarded_access global_state (fn State {threads, input} =>
|
60842
|
67 |
(case Symtab.lookup input thread_name of
|
60765
|
68 |
NONE => NONE
|
|
69 |
| SOME queue =>
|
|
70 |
let
|
|
71 |
val (msg, queue') = Queue.dequeue queue;
|
|
72 |
val input' =
|
60842
|
73 |
if Queue.is_empty queue' then Symtab.delete_safe thread_name input
|
|
74 |
else Symtab.update (thread_name, queue') input;
|
60765
|
75 |
in SOME (msg, make_state (threads, input')) end));
|
|
76 |
|
|
77 |
|
60869
|
78 |
|
|
79 |
(** thread state **)
|
|
80 |
|
|
81 |
(* stack frame during debugging *)
|
60856
|
82 |
|
|
83 |
local
|
|
84 |
val tag = Universal.tag () : ML_Debugger.state list Universal.tag;
|
|
85 |
in
|
60765
|
86 |
|
60856
|
87 |
fun get_debugging () = the_default [] (Thread.getLocal tag);
|
|
88 |
val is_debugging = not o null o get_debugging;
|
60765
|
89 |
|
60856
|
90 |
fun with_debugging e =
|
|
91 |
setmp_thread_data tag (get_debugging ()) (ML_Debugger.state (Thread.self ())) e ();
|
60765
|
92 |
|
60749
|
93 |
end;
|
|
94 |
|
60858
|
95 |
fun the_debug_state thread_name index =
|
|
96 |
(case get_debugging () of
|
|
97 |
[] => error ("Missing debugger information for thread " ^ quote thread_name)
|
|
98 |
| states =>
|
|
99 |
if index < 0 orelse index >= length states then
|
|
100 |
error ("Bad debugger stack index " ^ signed_string_of_int index ^ " for thread " ^
|
|
101 |
quote thread_name)
|
|
102 |
else nth states index);
|
|
103 |
|
|
104 |
|
60869
|
105 |
(* flags for single-stepping *)
|
60765
|
106 |
|
60869
|
107 |
datatype stepping = Stepping of bool * int; (*stepping enabled, stack depth limit*)
|
|
108 |
|
|
109 |
local
|
|
110 |
val tag = Universal.tag () : stepping Universal.tag;
|
|
111 |
in
|
|
112 |
|
|
113 |
fun get_stepping () = the_default (Stepping (false, ~1)) (Thread.getLocal tag);
|
|
114 |
fun put_stepping stepping = Thread.setLocal (tag, Stepping stepping);
|
|
115 |
|
|
116 |
end;
|
|
117 |
|
|
118 |
fun is_stepping () =
|
|
119 |
let
|
|
120 |
val stack = ML_Debugger.state (Thread.self ());
|
|
121 |
val Stepping (stepping, depth) = get_stepping ();
|
|
122 |
in stepping andalso (depth < 0 orelse length stack <= depth) end;
|
|
123 |
|
|
124 |
fun step_stepping () = put_stepping (true, ~1);
|
|
125 |
fun step_over_stepping () = put_stepping (true, length (get_debugging ()));
|
|
126 |
fun step_out_stepping () = put_stepping (true, length (get_debugging ()) - 1);
|
|
127 |
fun continue_stepping () = put_stepping (false, ~1);
|
|
128 |
|
|
129 |
|
|
130 |
(** eval ML **)
|
60765
|
131 |
|
60862
|
132 |
local
|
|
133 |
|
|
134 |
val context_attempts =
|
|
135 |
map ML_Lex.read
|
|
136 |
["Context.set_thread_data (SOME (Context.Theory ML_context))",
|
|
137 |
"Context.set_thread_data (SOME (Context.Proof ML_context))",
|
|
138 |
"Context.set_thread_data (SOME ML_context)"];
|
|
139 |
|
|
140 |
fun evaluate {SML, verbose} =
|
|
141 |
ML_Context.eval
|
|
142 |
{SML = SML, exchange = false, redirect = false, verbose = verbose,
|
|
143 |
writeln = writeln_message, warning = warning_message}
|
|
144 |
Position.none;
|
|
145 |
|
|
146 |
in
|
|
147 |
|
60858
|
148 |
fun eval thread_name index SML txt1 txt2 =
|
|
149 |
let
|
60862
|
150 |
val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2);
|
60858
|
151 |
|
60862
|
152 |
val evaluate_verbose = evaluate {SML = SML, verbose = true};
|
60858
|
153 |
val context1 = ML_Context.the_generic_context ()
|
|
154 |
|> Context_Position.set_visible_generic false
|
60871
|
155 |
|> Config.put_generic ML_Options.debugger false
|
60862
|
156 |
|> ML_Env.add_name_space {SML = SML}
|
|
157 |
(ML_Debugger.debug_name_space (the_debug_state thread_name index));
|
|
158 |
val context2 =
|
|
159 |
if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks1
|
|
160 |
then context1
|
|
161 |
else
|
|
162 |
let
|
|
163 |
val context' = context1
|
|
164 |
|> ML_Context.exec (fn () => evaluate_verbose (ML_Lex.read "val ML_context = " @ toks1));
|
|
165 |
fun try_exec toks =
|
|
166 |
try (ML_Context.exec (fn () => evaluate {SML = false, verbose = false} toks)) context';
|
|
167 |
in
|
|
168 |
(case get_first try_exec context_attempts of
|
|
169 |
SOME context2 => context2
|
|
170 |
| NONE => error "Malformed context: expected type theory, Proof.context, Context.generic")
|
|
171 |
end;
|
|
172 |
in Context.setmp_thread_data (SOME context2) evaluate_verbose toks2 end;
|
|
173 |
|
|
174 |
end;
|
60749
|
175 |
|
60765
|
176 |
|
60869
|
177 |
|
|
178 |
(** debugger entry point **)
|
60857
|
179 |
|
|
180 |
local
|
60765
|
181 |
|
60842
|
182 |
fun debugger_state thread_name =
|
|
183 |
Output.protocol_message (Markup.debugger_state thread_name)
|
60856
|
184 |
[get_debugging ()
|
60842
|
185 |
|> map (fn st =>
|
|
186 |
(Position.properties_of (Exn_Properties.position_of (ML_Debugger.debug_location st)),
|
|
187 |
ML_Debugger.debug_function st))
|
|
188 |
|> let open XML.Encode in list (pair properties string) end
|
|
189 |
|> YXML.string_of_body];
|
|
190 |
|
60857
|
191 |
fun debugger_command thread_name =
|
|
192 |
(case get_input thread_name of
|
60869
|
193 |
["step"] => (step_stepping (); false)
|
|
194 |
| ["step_over"] => (step_over_stepping (); false)
|
|
195 |
| ["step_out"] => (step_out_stepping (); false)
|
|
196 |
| ["continue"] => (continue_stepping (); false)
|
60857
|
197 |
| ["eval", index, SML, txt1, txt2] =>
|
|
198 |
(error_wrapper (fn () =>
|
|
199 |
eval thread_name (Markup.parse_int index) (Markup.parse_bool SML) txt1 txt2); true)
|
|
200 |
| bad =>
|
|
201 |
(Output.system_message
|
|
202 |
("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true));
|
|
203 |
|
60842
|
204 |
fun debugger_loop thread_name =
|
60856
|
205 |
let
|
|
206 |
fun loop () =
|
60857
|
207 |
(debugger_state thread_name; if debugger_command thread_name then loop () else ());
|
60856
|
208 |
in with_debugging loop; debugger_state thread_name end;
|
60765
|
209 |
|
60857
|
210 |
in
|
|
211 |
|
60765
|
212 |
fun init () =
|
|
213 |
ML_Debugger.on_breakpoint
|
60869
|
214 |
(SOME (fn (_, break) =>
|
|
215 |
if not (is_debugging ()) andalso
|
|
216 |
(! break orelse Options.default_bool @{system_option ML_debugger_stepping} orelse
|
|
217 |
is_stepping ()) andalso
|
|
218 |
Options.default_bool @{system_option ML_debugger_active}
|
|
219 |
then
|
|
220 |
(case Simple_Thread.get_name () of
|
|
221 |
SOME thread_name => debugger_loop thread_name
|
|
222 |
| NONE => ())
|
|
223 |
else ()));
|
60765
|
224 |
|
60857
|
225 |
end;
|
|
226 |
|
60765
|
227 |
|
60869
|
228 |
|
|
229 |
(** protocol commands **)
|
60765
|
230 |
|
|
231 |
val _ =
|
|
232 |
Isabelle_Process.protocol_command "Debugger.init"
|
|
233 |
(fn [] => init ());
|
|
234 |
|
|
235 |
val _ =
|
|
236 |
Isabelle_Process.protocol_command "Debugger.cancel"
|
60842
|
237 |
(fn [thread_name] => cancel thread_name);
|
60765
|
238 |
|
|
239 |
val _ =
|
|
240 |
Isabelle_Process.protocol_command "Debugger.input"
|
60842
|
241 |
(fn thread_name :: msg => input thread_name msg);
|
60765
|
242 |
|
60749
|
243 |
end;
|