Clean up debug logging signature

GillianPlatform · Mar 13, 2024 · 14ed2ba · 14ed2ba
1 parent aaa58c2
commit 14ed2ba
Show file tree

Hide file tree

Showing 7 changed files with 35 additions and 33 deletions.
diff --git a/GillianCore/debugging/adapter/breakpoints.ml b/GillianCore/debugging/adapter/breakpoints.ml
@@ -7,9 +7,9 @@ module DL = Debugger_log
 (**/**)
 
 module Make (Debugger : Debugger.S) = struct
-  let run ~dump_dbg dbg rpc =
+  let run dbg rpc =
     Lwt.pause ();%lwt
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Set breakpoints"
+    DL.set_rpc_command_handler rpc ~name:"Set breakpoints"
       (module Set_breakpoints_command)
       (fun args ->
         let source =

diff --git a/GillianCore/debugging/adapter/inspect.ml b/GillianCore/debugging/adapter/inspect.ml
@@ -9,13 +9,13 @@ module DL = Debugger_log
 module Make (Debugger : Debugger.S) = struct
   open Custom_commands (Debugger)
 
-  let run ~dump_dbg dbg rpc =
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Threads"
+  let run dbg rpc =
+    DL.set_rpc_command_handler rpc ~name:"Threads"
       (module Threads_command)
       (fun () ->
         let main_thread = Thread.make ~id:0 ~name:"main" in
         Lwt.return (Threads_command.Result.make ~threads:[ main_thread ] ()));
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Stack trace"
+    DL.set_rpc_command_handler rpc ~name:"Stack trace"
       (module Stack_trace_command)
       (fun _ ->
         let (frames : frame list) = Debugger.get_frames dbg in
@@ -31,7 +31,7 @@ module Make (Debugger : Debugger.S) = struct
                    ~end_column:(Some frame.end_column) ())
         in
         Lwt.return Stack_trace_command.Result.(make ~stack_frames ()));
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Scopes"
+    DL.set_rpc_command_handler rpc ~name:"Scopes"
       (module Scopes_command)
       (fun _ ->
         let scopes = Debugger.get_scopes dbg in
@@ -43,7 +43,7 @@ module Make (Debugger : Debugger.S) = struct
                  Scope.make ~name ~variables_reference ~expensive:false ())
         in
         Lwt.return (Scopes_command.Result.make ~scopes ()));
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Variables"
+    DL.set_rpc_command_handler rpc ~name:"Variables"
       (module Variables_command)
       (fun args ->
         let variables = Debugger.get_variables args.variables_reference dbg in
@@ -57,7 +57,7 @@ module Make (Debugger : Debugger.S) = struct
                  Variable.make ~name ~value ~type_ ~variables_reference ())
         in
         Lwt.return (Variables_command.Result.make ~variables ()));
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Exception info"
+    DL.set_rpc_command_handler rpc ~name:"Exception info"
       (module Exception_info_command)
       (fun _ ->
         let exception_info = Debugger.get_exception_info dbg in
@@ -67,10 +67,10 @@ module Make (Debugger : Debugger.S) = struct
         Lwt.return
           (Exception_info_command.Result.make ~exception_id ~description
              ~break_mode ()));
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Debugger state"
+    DL.set_rpc_command_handler rpc ~name:"Debugger state"
       (module Debugger_state_command)
       (fun _ -> Lwt.return (Debugger.Inspect.get_debug_state dbg));
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Matching"
+    DL.set_rpc_command_handler rpc ~name:"Matching"
       (module Matching_command)
       (fun { id } ->
         let match_map = dbg |> Debugger.Inspect.get_match_map id in

diff --git a/GillianCore/debugging/adapter/lifecycle.ml b/GillianCore/debugging/adapter/lifecycle.ml
@@ -9,13 +9,13 @@ module DL = Debugger_log
 module Make (Debugger : Debugger.S) = struct
   open Custom_events (Debugger)
 
-  let run ~dump_dbg launch_args dbg rpc =
+  let run launch_args dbg rpc =
     let promise, resolver = Lwt.task () in
     Lwt.pause ();%lwt
     let send_initialize_event () =
       Debug_rpc.send_event rpc (module Initialized_event) ()
     in
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Configuration-done"
+    DL.set_rpc_command_handler rpc ~name:"Configuration-done"
       (module Configuration_done_command)
       (fun _ ->
         let open Launch_command.Arguments in
@@ -43,7 +43,7 @@ module Make (Debugger : Debugger.S) = struct
             Stopped_event.Payload.(
               make ~reason:Stopped_event.Payload.Reason.Entry
                 ~thread_id:(Some 0) ()));
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Disconnect"
+    DL.set_rpc_command_handler rpc ~name:"Disconnect"
       (module Disconnect_command)
       (fun _ ->
         DL.log (fun m -> m "Interrupting the debugger is not supported");

diff --git a/GillianCore/debugging/adapter/state_debug.ml b/GillianCore/debugging/adapter/state_debug.ml
@@ -5,14 +5,13 @@ module Make (Debugger : Debugger.S) = struct
   module Breakpoints = Breakpoints.Make (Debugger)
 
   let run launch_args dbg rpc =
-    let dump_dbg () =
-      Debugger.Inspect.(get_debug_state dbg |> debug_state_view_to_yojson)
-    in
+    Debugger_log.set_debug_state_dumper (fun () ->
+        Debugger.Inspect.(get_debug_state dbg |> debug_state_view_to_yojson));
     Lwt.join
       [
-        Lifecycle.run ~dump_dbg launch_args dbg rpc;
-        Inspect.run ~dump_dbg dbg rpc;
-        TimeTravel.run ~dump_dbg dbg rpc;
-        Breakpoints.run ~dump_dbg dbg rpc;
+        Lifecycle.run launch_args dbg rpc;
+        Inspect.run dbg rpc;
+        TimeTravel.run dbg rpc;
+        Breakpoints.run dbg rpc;
       ]
 end
diff --git a/GillianCore/debugging/adapter/time_travel.ml b/GillianCore/debugging/adapter/time_travel.ml
@@ -10,42 +10,42 @@ module Make (Debugger : Debugger.S) = struct
   open Custom_events (Debugger)
   open Custom_commands (Debugger)
 
-  let run ~dump_dbg dbg rpc =
+  let run dbg rpc =
     let send_stopped_events = send_stopped_events dbg rpc in
     let promise, _ = Lwt.task () in
     Lwt.pause ();%lwt
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Continue"
+    DL.set_rpc_command_handler rpc ~name:"Continue"
       (module Continue_command)
       (fun _ ->
         let stop_reason = Debugger.run dbg in
         send_stopped_events stop_reason;%lwt
         Lwt.return (Continue_command.Result.make ()));
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Next"
+    DL.set_rpc_command_handler rpc ~name:"Next"
       (module Next_command)
       (fun _ ->
         let stop_reason = Debugger.step dbg in
         send_stopped_events stop_reason);
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Reverse continue"
+    DL.set_rpc_command_handler rpc ~name:"Reverse continue"
       (module Reverse_continue_command)
       (fun _ ->
         let stop_reason = Debugger.run ~reverse:true dbg in
         send_stopped_events stop_reason);
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Step back"
+    DL.set_rpc_command_handler rpc ~name:"Step back"
       (module Step_back_command)
       (fun _ ->
         let stop_reason = Debugger.step ~reverse:true dbg in
         send_stopped_events stop_reason);
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Step in"
+    DL.set_rpc_command_handler rpc ~name:"Step in"
       (module Step_in_command)
       (fun _ ->
         let stop_reason = Debugger.step_in dbg in
         send_stopped_events stop_reason);
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Step out"
+    DL.set_rpc_command_handler rpc ~name:"Step out"
       (module Step_out_command)
       (fun _ ->
         let stop_reason = Debugger.step_out dbg in
         send_stopped_events stop_reason);
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Jump"
+    DL.set_rpc_command_handler rpc ~name:"Jump"
       (module Jump_command)
       (fun { id } ->
         match dbg |> Debugger.jump_to_id id with
@@ -55,7 +55,7 @@ module Make (Debugger : Debugger.S) = struct
         | Ok () ->
             send_stopped_events Step;%lwt
             Lwt.return (Jump_command.Result.make ~success:true ()));
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Step specific"
+    DL.set_rpc_command_handler rpc ~name:"Step specific"
       (module Step_specific_command)
       (fun { prev_id; branch_case } ->
         match dbg |> Debugger.step_specific branch_case prev_id with
@@ -65,7 +65,7 @@ module Make (Debugger : Debugger.S) = struct
         | Ok stop_reason ->
             send_stopped_events stop_reason;%lwt
             Lwt.return (Step_specific_command.Result.make ~success:true ()));
-    DL.set_rpc_command_handler rpc ~dump_dbg ~name:"Start proc"
+    DL.set_rpc_command_handler rpc ~name:"Start proc"
       (module Start_proc_command)
       (fun { proc_name } ->
         match dbg |> Debugger.start_proc proc_name with

diff --git a/GillianCore/debugging/log/debugger_log.ml b/GillianCore/debugging/log/debugger_log.ml
@@ -96,15 +96,18 @@ let setup rpc =
   reset ();
   rpc_ref := Some rpc
 
-let set_rpc_command_handler rpc ?name ?dump_dbg module_ f =
+let dump_dbg : (unit -> Yojson.Safe.t) option ref = ref None
+let set_debug_state_dumper f = dump_dbg := Some f
+
+let set_rpc_command_handler rpc ?name module_ f =
   let f x =
     let name_json =
       match name with
       | Some name -> [ ("dap_cmd", `String name) ]
       | None -> []
     in
     let dbg_json =
-      match dump_dbg with
+      match !dump_dbg with
       | Some dump_dbg -> [ ("debug_state", dump_dbg ()) ]
       | None -> []
     in

diff --git a/GillianCore/debugging/log/debugger_log.mli b/GillianCore/debugging/log/debugger_log.mli
@@ -36,11 +36,11 @@ end
 include module type of Public
 
 val setup : Debug_rpc.t -> unit
+val set_debug_state_dumper : (unit -> Yojson.Safe.t) -> unit
 
 val set_rpc_command_handler :
   Debug_rpc.t ->
   ?name:string ->
-  ?dump_dbg:(unit -> Yojson.Safe.t) ->
   (module Debug_protocol.COMMAND
      with type Arguments.t = 'a
       and type Result.t = 'b) ->