Rethink Exec Map (#306)

* Rethink Exec_map * Update debug ui for exec map change
GillianPlatform · Aug 3, 2024 · c6cc0e4 · c6cc0e4
1 parent 364bfdf
commit c6cc0e4
Show file tree

Hide file tree

Showing 101 changed files with 1,765 additions and 1,456 deletions.
diff --git a/.vscode/launch.json b/.vscode/launch.json
@@ -7,7 +7,7 @@
 			"request": "launch",
 			"args": [
 				"--extensionDevelopmentPath=${workspaceFolder}/debugger-vscode-extension",
-				"${workspaceFolder}/debugger-vscode-extension/sampleWorkspace"
+				"${workspaceFolder}/debug-ui/examples"
 			],
 			"outFiles": [
 				"${workspaceFolder}/debugger-vscode-extension/out/**/*.js"

diff --git a/GillianCore/debugging/adapter/lifecycle.ml b/GillianCore/debugging/adapter/lifecycle.ml
@@ -19,7 +19,7 @@ module Make (Debugger : Debugger.S) = struct
       (module Configuration_done_command)
       (fun _ ->
         let open Launch_command.Arguments in
-        if not launch_args.stop_on_entry then (
+        if not launch_args.stop_on_entry then
           let stop_reason = Debugger.run ~launch:true dbg in
           match stop_reason with
           | Step ->
@@ -34,9 +34,7 @@ module Make (Debugger : Debugger.S) = struct
                 Stopped_event.Payload.(
                   make ~reason:Stopped_event.Payload.Reason.Exception
                     ~thread_id:(Some 0) ())
-          | reason ->
-              dbg |> Debugger.jump_to_start;
-              send_stopped_events dbg rpc reason)
+          | reason -> send_stopped_events dbg rpc reason
         else
           Debug_rpc.send_event rpc
             (module Stopped_event)

diff --git a/GillianCore/debugging/debugger/base_debugger.ml b/GillianCore/debugging/debugger/base_debugger.ml
@@ -462,29 +462,16 @@ struct
 
     let build_final_cmd_data content result prev_id branch_path debug_state =
       let cmd = content |> of_yojson_string Logging.ConfigReport.of_yojson in
-      let proc_name = (List.hd cmd.callstack).pid in
-      let errors = show_result_errors result in
-      let matches = match_final_cmd prev_id ~proc_name result debug_state in
       let exec_data =
-        Lift.make_executed_cmd_data Exec_map.Final prev_id cmd ~matches ~errors
+        let proc_name = (List.hd cmd.callstack).pid in
+        let errors = show_result_errors result in
+        let matches = match_final_cmd prev_id ~proc_name result debug_state in
+        let next_kind = Exec_map.Zero in
+        Lift.make_executed_cmd_data next_kind prev_id cmd ~matches ~errors
           branch_path
       in
       (exec_data, cmd)
 
-    let jump_to_start (state : t) =
-      let { debug_state; _ } = state in
-      let proc_state = get_proc_state_exn state in
-      let result =
-        let** root_id =
-          proc_state.lifter_state |> Lifter.get_root_id
-          |> Option.to_result ~none:"Debugger.jump_to_start: No root id found!"
-        in
-        jump_state_to_id root_id debug_state proc_state
-      in
-      match result with
-      | Error msg -> failwith msg
-      | Ok () -> ()
-
     module Step = struct
       open Verification.SAInterpreter.Logging
 

diff --git a/GillianCore/debugging/debugger/debugger_intf.ml b/GillianCore/debugging/debugger/debugger_intf.ml
@@ -11,7 +11,6 @@ module type S = sig
 
   val launch : string -> string option -> (t, string) result
   val jump_to_id : Logging.Report_id.t -> t -> (unit, string) result
-  val jump_to_start : t -> unit
   val step_in : t -> stop_reason
   val step : ?reverse:bool -> t -> stop_reason
 

diff --git a/GillianCore/debugging/lifter/gil_fallback_lifter.ml b/GillianCore/debugging/lifter/gil_fallback_lifter.ml
@@ -65,11 +65,6 @@ functor
       | Some tl -> tl |> TLLifter.get_matches_at_id id
       | None -> gil |> Gil_lifter.get_matches_at_id id
 
-    let get_root_id { gil; tl; _ } =
-      match tl with
-      | Some tl -> tl |> TLLifter.get_root_id
-      | None -> gil |> Gil_lifter.get_root_id
-
     let memory_error_to_exception_info = TLLifter.memory_error_to_exception_info
     let add_variables = TLLifter.add_variables