src/Pure/Tools/debugger.ML
author wenzelm
Mon Oct 09 21:12:22 2017 +0200 (21 months ago)
changeset 66822 4642cf4a7ebb
parent 65222 fb8253564483
child 67381 146757999c8d
permissions -rw-r--r--
tuned signature;
     1 (*  Title:      Pure/Tools/debugger.ML
     2     Author:     Makarius
     3 
     4 Interactive debugger for Isabelle/ML.
     5 *)
     6 
     7 signature DEBUGGER =
     8 sig
     9   val writeln_message: string -> unit
    10   val warning_message: string -> unit
    11   val error_message: string -> unit
    12 end;
    13 
    14 structure Debugger: DEBUGGER =
    15 struct
    16 
    17 (** global state **)
    18 
    19 (* output messages *)
    20 
    21 fun output_message kind msg =
    22   if msg = "" then ()
    23   else
    24     Output.protocol_message
    25       (Markup.debugger_output (Standard_Thread.the_name ()))
    26       [Markup.markup (kind, Markup.serial_properties (serial ())) msg];
    27 
    28 val writeln_message = output_message Markup.writelnN;
    29 val warning_message = output_message Markup.warningN;
    30 val error_message = output_message Markup.errorN;
    31 
    32 fun error_wrapper e = e ()
    33   handle exn =>
    34     if Exn.is_interrupt exn then Exn.reraise exn
    35     else error_message (Runtime.exn_message exn);
    36 
    37 
    38 (* thread input *)
    39 
    40 val thread_input =
    41   Synchronized.var "Debugger.state" (NONE: string list Queue.T Symtab.table option);
    42 
    43 fun init_input () = Synchronized.change thread_input (K (SOME Symtab.empty));
    44 fun exit_input () = Synchronized.change thread_input (K NONE);
    45 
    46 fun input thread_name msg =
    47   if null msg then error "Empty input"
    48   else
    49     Synchronized.change thread_input
    50       (Option.map (Symtab.map_default (thread_name, Queue.empty) (Queue.enqueue msg)));
    51 
    52 fun get_input thread_name =
    53   Synchronized.guarded_access thread_input
    54     (fn NONE => SOME ([], NONE)
    55       | SOME input =>
    56           (case Symtab.lookup input thread_name of
    57             NONE => NONE
    58           | SOME queue =>
    59               let
    60                 val (msg, queue') = Queue.dequeue queue;
    61                 val input' =
    62                   if Queue.is_empty queue' then Symtab.delete_safe thread_name input
    63                   else Symtab.update (thread_name, queue') input;
    64               in SOME (msg, SOME input') end));
    65 
    66 
    67 (* global break *)
    68 
    69 local
    70   val break = Synchronized.var "Debugger.break" false;
    71 in
    72 
    73 fun is_break () = Synchronized.value break;
    74 fun set_break b = Synchronized.change break (K b);
    75 
    76 end;
    77 
    78 
    79 
    80 (** thread state **)
    81 
    82 (* stack frame during debugging *)
    83 
    84 val debugging_var = Thread_Data.var () : PolyML.DebuggerInterface.debugState list Thread_Data.var;
    85 
    86 fun get_debugging () = the_default [] (Thread_Data.get debugging_var);
    87 val is_debugging = not o null o get_debugging;
    88 
    89 fun with_debugging e =
    90   Thread_Data.setmp debugging_var (SOME (PolyML.DebuggerInterface.debugState (Thread.self ()))) e ();
    91 
    92 fun the_debug_state thread_name index =
    93   (case get_debugging () of
    94     [] => error ("Missing debugger information for thread " ^ quote thread_name)
    95   | states =>
    96       if index < 0 orelse index >= length states then
    97         error ("Bad debugger stack index " ^ signed_string_of_int index ^ " for thread " ^
    98           quote thread_name)
    99       else nth states index);
   100 
   101 
   102 (* flags for single-stepping *)
   103 
   104 datatype stepping = Stepping of bool * int;  (*stepping enabled, stack depth limit*)
   105 
   106 val stepping_var = Thread_Data.var () : stepping Thread_Data.var;
   107 
   108 fun get_stepping () = the_default (Stepping (false, ~1)) (Thread_Data.get stepping_var);
   109 fun put_stepping stepping = Thread_Data.put stepping_var (SOME (Stepping stepping));
   110 
   111 fun is_stepping () =
   112   let
   113     val stack = PolyML.DebuggerInterface.debugState (Thread.self ());
   114     val Stepping (stepping, depth) = get_stepping ();
   115   in stepping andalso (depth < 0 orelse length stack <= depth) end;
   116 
   117 fun continue () = put_stepping (false, ~1);
   118 fun step () = put_stepping (true, ~1);
   119 fun step_over () = put_stepping (true, length (get_debugging ()));
   120 fun step_out () = put_stepping (true, length (get_debugging ()) - 1);
   121 
   122 
   123 
   124 (** eval ML **)
   125 
   126 local
   127 
   128 val context_attempts =
   129   map ML_Lex.read
   130    ["Context.put_generic_context (SOME (Context.Theory ML_context))",
   131     "Context.put_generic_context (SOME (Context.Proof ML_context))",
   132     "Context.put_generic_context (SOME ML_context)"];
   133 
   134 fun evaluate {SML, verbose} =
   135   ML_Context.eval
   136     {SML = SML, exchange = false, redirect = false, verbose = verbose,
   137       debug = SOME false, writeln = writeln_message, warning = warning_message}
   138     Position.none;
   139 
   140 fun eval_setup thread_name index SML context =
   141   context
   142   |> Context_Position.set_visible_generic false
   143   |> ML_Env.add_name_space {SML = SML}
   144       (PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index));
   145 
   146 fun eval_context thread_name index SML toks =
   147   let
   148     val context = Context.the_generic_context ();
   149     val context1 =
   150       if SML orelse forall (fn Antiquote.Text tok => ML_Lex.is_improper tok | _ => false) toks
   151       then context
   152       else
   153         let
   154           val context' = context
   155             |> eval_setup thread_name index SML
   156             |> ML_Context.exec (fn () =>
   157                 evaluate {SML = SML, verbose = true} (ML_Lex.read "val ML_context = " @ toks));
   158           fun try_exec toks =
   159             try (ML_Context.exec (fn () => evaluate {SML = false, verbose = false} toks)) context';
   160         in
   161           (case get_first try_exec context_attempts of
   162             SOME context2 => context2
   163           | NONE => error "Malformed context: expected type theory, Proof.context, Context.generic")
   164         end;
   165   in context1 |> eval_setup thread_name index SML end;
   166 
   167 in
   168 
   169 fun eval thread_name index SML txt1 txt2 =
   170   let
   171     val (toks1, toks2) = apply2 (ML_Lex.read_source SML o Input.string) (txt1, txt2);
   172     val context = eval_context thread_name index SML toks1;
   173   in Context.setmp_generic_context (SOME context) (evaluate {SML = SML, verbose = true}) toks2 end;
   174 
   175 fun print_vals thread_name index SML txt =
   176   let
   177     val toks = ML_Lex.read_source SML (Input.string txt)
   178     val context = eval_context thread_name index SML toks;
   179     val space = PolyML.DebuggerInterface.debugNameSpace (the_debug_state thread_name index);
   180 
   181     fun print x =
   182       Pretty.from_polyml
   183         (PolyML.NameSpace.Values.printWithType
   184           (x, FixedInt.fromInt (ML_Print_Depth.get_print_depth ()), SOME space));
   185     fun print_all () =
   186       #allVal (PolyML.DebuggerInterface.debugLocalNameSpace (the_debug_state thread_name index)) ()
   187       |> sort_by #1 |> map (Pretty.item o single o print o #2)
   188       |> Pretty.chunks |> Pretty.string_of |> writeln_message;
   189   in Context.setmp_generic_context (SOME context) print_all () end;
   190 
   191 end;
   192 
   193 
   194 
   195 (** debugger loop **)
   196 
   197 local
   198 
   199 fun debugger_state thread_name =
   200   Output.protocol_message (Markup.debugger_state thread_name)
   201    [get_debugging ()
   202     |> map (fn st =>
   203       (Position.properties_of
   204         (Exn_Properties.position_of_polyml_location (PolyML.DebuggerInterface.debugLocation st)),
   205        PolyML.DebuggerInterface.debugFunction st))
   206     |> let open XML.Encode in list (pair properties string) end
   207     |> YXML.string_of_body];
   208 
   209 fun debugger_command thread_name =
   210   (case get_input thread_name of
   211     [] => (continue (); false)
   212   | ["continue"] => (continue (); false)
   213   | ["step"] => (step (); false)
   214   | ["step_over"] => (step_over (); false)
   215   | ["step_out"] => (step_out (); false)
   216   | ["eval", index, SML, txt1, txt2] =>
   217      (error_wrapper (fn () =>
   218         eval thread_name (Value.parse_int index) (Value.parse_bool SML) txt1 txt2); true)
   219   | ["print_vals", index, SML, txt] =>
   220      (error_wrapper (fn () =>
   221         print_vals thread_name (Value.parse_int index) (Value.parse_bool SML) txt); true)
   222   | bad =>
   223      (Output.system_message
   224         ("Debugger: bad input " ^ ML_Syntax.print_list ML_Syntax.print_string bad); true));
   225 
   226 in
   227 
   228 fun debugger_loop thread_name =
   229   Thread_Attributes.uninterruptible (fn restore_attributes => fn () =>
   230     let
   231       fun loop () =
   232         (debugger_state thread_name; if debugger_command thread_name then loop () else ());
   233       val result = Exn.capture (restore_attributes with_debugging) loop;
   234       val _ = debugger_state thread_name;
   235     in Exn.release result end) ();
   236 
   237 end;
   238 
   239 
   240 
   241 (** protocol commands **)
   242 
   243 val _ =
   244   Isabelle_Process.protocol_command "Debugger.init"
   245     (fn [] =>
   246      (init_input ();
   247       PolyML.DebuggerInterface.setOnBreakPoint
   248         (SOME (fn (_, break) =>
   249           if not (is_debugging ()) andalso (! break orelse is_break () orelse is_stepping ())
   250           then
   251             (case Standard_Thread.get_name () of
   252               SOME thread_name => debugger_loop thread_name
   253             | NONE => ())
   254           else ()))));
   255 
   256 val _ =
   257   Isabelle_Process.protocol_command "Debugger.exit"
   258     (fn [] => (PolyML.DebuggerInterface.setOnBreakPoint NONE; exit_input ()));
   259 
   260 val _ =
   261   Isabelle_Process.protocol_command "Debugger.break"
   262     (fn [b] => set_break (Value.parse_bool b));
   263 
   264 val _ =
   265   Isabelle_Process.protocol_command "Debugger.breakpoint"
   266     (fn [node_name, id0, breakpoint0, breakpoint_state0] =>
   267       let
   268         val id = Value.parse_int id0;
   269         val breakpoint = Value.parse_int breakpoint0;
   270         val breakpoint_state = Value.parse_bool breakpoint_state0;
   271 
   272         fun err () = error ("Bad exec for command " ^ Value.print_int id);
   273       in
   274         (case Document.command_exec (Document.state ()) node_name id of
   275           SOME (eval, _) =>
   276             if Command.eval_finished eval then
   277               let
   278                 val st = Command.eval_result_state eval;
   279                 val ctxt = Toplevel.presentation_context_of st
   280                   handle Toplevel.UNDEF => err ();
   281               in
   282                 (case ML_Env.get_breakpoint (Context.Proof ctxt) breakpoint of
   283                   SOME (b, _) => b := breakpoint_state
   284                 | NONE => err ())
   285               end
   286             else err ()
   287         | NONE => err ())
   288       end);
   289 
   290 val _ =
   291   Isabelle_Process.protocol_command "Debugger.input"
   292     (fn thread_name :: msg => input thread_name msg);
   293 
   294 end;