diff --git a/.vscode/launch.json b/.vscode/launch.json index 0370c2c51..79a152cb9 100644 --- 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 index e910b50ee..2854c55e6 100644 --- 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 index c92c800a6..3657026f2 100644 --- 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 index c5e445b8c..5aa5ea1cd 100644 --- 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 index e8e8016e3..0c422a6d0 100644 --- 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 diff --git a/GillianCore/debugging/lifter/gil_lifter.ml b/GillianCore/debugging/lifter/gil_lifter.ml index c9c7910f8..3e3bf8a8e 100644 --- a/GillianCore/debugging/lifter/gil_lifter.ml +++ b/GillianCore/debugging/lifter/gil_lifter.ml @@ -1,8 +1,10 @@ module L = Logging module DL = Debugger_log -open Lifter +open Lifter_intf include Gil_lifter_intf +type id = L.Report_id.t [@@deriving yojson] + module Make : Make = functor (SMemory : SMemory.S) @@ -17,26 +19,21 @@ functor type branch_case = Branch_case.t [@@deriving yojson] type branch_path = Branch_case.path [@@deriving yojson] - (* Some fields are Null'd in yojson to stop huge memory inefficiency *) - type map = (branch_case, cmd_data, unit) Exec_map.t - - and cmd_data = { - id : L.Report_id.t; + type cmd_data = { + id : id; display : string; matches : matching list; errors : string list; - submap : map submap; + submap : id submap; branch_path : branch_path; - parent : (map * branch_case option) option; [@to_yojson fun _ -> `Null] + parent : (id * branch_case option) option; } [@@deriving to_yojson] - type t = { - mutable map : map; - root_proc : string; - all_procs : string list; - id_map : (L.Report_id.t, map) Hashtbl.t; [@to_yojson fun _ -> `Null] - } + type map = (id, branch_case, cmd_data, unit) Exec_map.map + [@@deriving to_yojson] + + type t = { mutable map : map; root_proc : string; all_procs : string list } [@@deriving to_yojson] type memory = SMemory.t @@ -64,55 +61,32 @@ functor let new_cmd ?(submap = NoSubmap) ~parent - id_map - { kind; id; matches; errors; cmd_report : cmd_report; branch_path; _ } + map + { + next_kind; + id; + matches; + errors; + cmd_report : cmd_report; + branch_path; + _; + } () = let display = Fmt.to_to_string Cmd.pp_indexed cmd_report.cmd in let data = { id; display; matches; errors; submap; branch_path; parent } in - let cmd = - match kind with - | Normal -> Cmd { data; next = Nothing } - | Branch cases -> - let nexts = Hashtbl.create (List.length cases) in - let () = - List.iter - (fun (case, _) -> Hashtbl.add nexts case ((), Nothing)) - cases - in - BranchCmd { data; nexts } - | Final -> FinalCmd { data } + let next = + match next_kind with + | One () -> Some (Single (None, ())) + | Many cases -> + let nexts = List.map (fun (case, ()) -> (case, (None, ()))) cases in + Some (Branch nexts) + | Zero -> None in - Hashtbl.replace id_map id cmd; - cmd - - let get_id_opt = function - | Nothing -> None - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data; _ } -> - Some data.id - - let get_id map = - match get_id_opt map with - | None -> failwith "Tried to get id of Nothing!" - | Some id -> id - - let at_id_result id state = - match Hashtbl.find_opt state.id_map id with - | None -> Error "id not found" - | Some Nothing -> Error "HORROR - got Nothing at id!" - | Some - ((Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data }) as map) - -> Ok (map, data.branch_path) - - let at_id_exn id state = - match at_id_result id state with - | Ok (map, branch_path) -> (map, branch_path) - | Error s -> - DL.failwith - (fun () -> - [ ("id", L.Report_id.to_yojson id); ("state", dump state) ]) - ("at_id: " ^ s) + let node = { data; next } in + Hashtbl.replace map.entries id (Node node); + node let should_skip_cmd (exec_data : cmd_report executed_cmd_data) state : bool = @@ -120,8 +94,8 @@ functor not (List.mem proc_name state.all_procs) let consume_cmd prev_id branch_case exec_data state = - let { id_map; _ } = state in - let new_cmd = new_cmd id_map exec_data in + let { map; _ } = state in + let new_cmd = new_cmd map exec_data in let branch_case = Option_utils.coalesce branch_case exec_data.cmd_report.branch_case in @@ -131,92 +105,99 @@ functor [ ("state", dump state); ("exec_data", exec_data_to_yojson exec_data); - ("prev_id", L.Report_id.to_yojson prev_id); + ("prev_id", id_to_yojson prev_id); ("branch_case", opt_to_yojson branch_case_to_yojson branch_case); ]) ("Gil_lifter.handle_cmd: " ^ s) in - let branch_case = - Option_utils.coalesce branch_case exec_data.cmd_report.branch_case - in - let map = - match Hashtbl.find_opt id_map prev_id with - | Some map -> map + let prev = + match get map prev_id with + | Some prev -> prev | None -> failwith (Fmt.str "couldn't find prev_id %a!" L.Report_id.pp prev_id) in - let new_cmd = - match map with - | Cmd cmd when cmd.next = Nothing -> - let parent = Some (map, None) in + let new_cmd, new_next = + match prev.next with + | Some (Single (None, ())) -> + let parent = Some (prev_id, None) in let new_cmd = new_cmd ~parent () in - let () = cmd.next <- new_cmd in - new_cmd - | Cmd _ -> failwith "cmd.next not Nothing!" - | BranchCmd { nexts; _ } -> ( - match branch_case with - | None -> - failwith "HORROR - need branch case to insert to branch cmd!" - | Some case -> ( - match Hashtbl.find_opt nexts case with - | Some ((), Nothing) -> - let parent = Some (map, Some case) in - let new_cmd = new_cmd ~parent () in - let () = Hashtbl.replace nexts case ((), new_cmd) in - new_cmd - | Some ((), _) -> failwith "colliding cases in branch cmd" - | None -> failwith "inserted branch case not found on parent!")) - | _ -> failwith "can't insert to Nothing or FinalCmd" + (new_cmd, Single (Some new_cmd.data.id, ())) + | Some (Single _) -> failwith "cmd already has next!" + | Some (Branch nexts) -> ( + let case = + match branch_case with + | None -> + failwith "HORROR - need branch case to insert to branch cmd!" + | Some case -> case + in + match List.assoc_opt case nexts with + | Some (None, ()) -> + let parent = Some (prev_id, Some case) in + let new_cmd = new_cmd ~parent () in + let next = (Some new_cmd.data.id, ()) in + let nexts = List_utils.assoc_replace case next nexts in + (new_cmd, Branch nexts) + | Some _ -> failwith "colliding cases in branch cmd" + | None -> failwith "inserted branch case not found on parent!") + | None -> failwith "can't insert to final cmd" in + let prev' = { prev with next = Some new_next } in + let () = Hashtbl.replace map.entries prev.data.id (Node prev') in new_cmd let handle_cmd prev_id branch_case exec_data state = let _ = consume_cmd prev_id branch_case exec_data state in () - let package_case ~bd:_ ~all_cases:_ case = Packaged.package_gil_case case - - let package_data package { id; display; matches; errors; submap; _ } = - let submap = - match submap with - | NoSubmap -> NoSubmap - | Proc p -> Proc p - | Submap map -> Submap (package map) + let package_node { data : cmd_data; next } = + let data = + Packaged. + { + id = data.id; + all_ids = [ data.id ]; + display = data.display; + matches = data.matches; + errors = data.errors; + submap = data.submap; + } in - Packaged.{ id; all_ids = [ id ]; display; matches; errors; submap } + let next = + match next with + | Some (Single (next, ())) -> Some (Single (next, "")) + | Some (Branch nexts) -> + let nexts = + List.map + (fun (case, (next, ())) -> + let case, bdata = Packaged.package_gil_case case in + (case, (next, bdata))) + nexts + in + Some (Branch nexts) + | None -> None + in + { data; next } - let package = Packaged.package package_data package_case + let package = Packaged.package Fun.id package_node let get_gil_map state = package state.map let get_lifted_map _ = None let get_lifted_map_exn _ = failwith "get_lifted_map not implemented for GIL lifter" - let get_matches_at_id id state = - match state |> at_id_exn id |> fst with - | Nothing -> - DL.failwith - (fun () -> - [ ("id", L.Report_id.to_yojson id); ("state", dump state) ]) - "get_matches_at_id: HORROR - map is Nothing!" - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> - data.matches - - let get_root_id { map; _ } = - match map with - | Nothing -> None - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> - Some data.id - - let path_of_id id state = state |> at_id_exn id |> snd + let get_matches_at_id id state = (get_exn state.map id).data.matches + let path_of_id id state = (get_exn state.map id).data.branch_path let cases_at_id id state = - match state |> at_id_exn id |> fst with - | Nothing -> failwith "cases_at_id: map is Nothing!" - | FinalCmd _ -> failwith " cases_at_id: map is Final!" - | Cmd _ -> [] - | BranchCmd { nexts; _ } -> nexts |> Hashtbl.to_seq_keys |> List.of_seq + let next = + match get state.map id with + | None -> failwith "cases_at_id: couldn't find id!" + | Some node -> node.next + in + match next with + | None -> failwith " cases_at_id: map is Final!" + | Some (Single _) -> [] + | Some (Branch nexts) -> nexts |> List.map fst let memory_error_to_exception_info { error; _ } : exception_info = { id = Fmt.to_to_string SMemory.pp_err error; description = None } @@ -251,34 +232,36 @@ functor let select_case nexts = let case, _ = - Hashtbl.fold - (fun case (_, map) acc -> - match (map, acc) with + List.fold_left + (fun acc (case, (next, _)) -> + match (next, acc) with | _, (_, true) -> acc - | Nothing, (_, false) -> (Some case, true) + | None, (_, false) -> (Some case, true) | _, (None, false) -> (Some case, false) | _ -> acc) - nexts (None, false) + (None, false) nexts in Option.get case let find_next state id case = - let map, _ = state |> at_id_exn id in - match (map, case) with - | Nothing, _ -> failwith "HORROR - map is Nothing!" - | FinalCmd _, _ -> failwith "HORROR - tried to step from FinalCmd!" - | Cmd _, Some _ -> + let next = + match (get_exn state.map id).next with + | None -> failwith "HORROR - tried to step from FinalCmd!" + | Some next -> next + in + match (next, case) with + | Single _, Some _ -> failwith "HORROR - tried to step case for non-branch cmd" - | Cmd { next = Nothing; _ }, None -> Either.Right None - | Cmd { next; _ }, None -> Either.Left next - | BranchCmd { nexts; _ }, None -> + | Single (None, _), None -> Either.Right None + | Single (Some next, _), None -> Either.Left (get_exn state.map next) + | Branch nexts, None -> let case = select_case nexts in Either.Right (Some case) - | BranchCmd { nexts; _ }, Some case -> ( - match Hashtbl.find_opt nexts case with + | Branch nexts, Some case -> ( + match List.assoc_opt case nexts with | None -> failwith "case not found" - | Some (_, Nothing) -> Either.Right (Some case) - | Some (_, next) -> Either.Left next) + | Some (None, _) -> Either.Right (Some case) + | Some (Some next, _) -> Either.Left (get_exn state.map next)) let request_next state id case = let path = path_of_id id state in @@ -286,24 +269,22 @@ functor consume_cmd id case exec_data state let step state id case = - let next = + let next_node = match find_next state id case with | Either.Left next -> next | Either.Right case -> request_next state id case in - match next with - | Nothing -> failwith "HORROR - next is Nothing!" - | Cmd { data = { id; _ }; _ } -> Either.Left [ (id, None) ] - | BranchCmd { data = { id; _ }; nexts } -> - nexts |> Hashtbl.to_seq - |> Seq.map (fun (case, _) -> (id, Some case)) - |> List.of_seq |> Either.left - | FinalCmd { data = { id; _ } } -> Either.Right id + let id = next_node.data.id in + match next_node.next with + | Some (Single _) -> Either.Left [ (id, None) ] + | Some (Branch nexts) -> + nexts |> List.map (fun (case, _) -> (id, Some case)) |> Either.left + | None -> Either.Right id let step_branch state id case = let case = Option.map - (fun (_, json) -> json |> Branch_case.of_yojson |> Result.get_ok) + (fun json -> json |> Branch_case.of_yojson |> Result.get_ok) case in let id = @@ -316,15 +297,13 @@ functor let step_over state id = step_branch state id None let step_in = step_over - let step_back { id_map; _ } id = - match Hashtbl.find id_map id with - | Nothing -> failwith "HORROR - map is Nothing!" - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> ( - match data.parent with - | None -> failwith "HORROR - parent is None!" - | Some (parent, _) -> - let id = get_id parent in - (id, Debugger_utils.Step)) + let step_back { map; _ } id = + let stop_id = + match (get_exn map id).data.parent with + | None -> id + | Some (parent_id, _) -> parent_id + in + (stop_id, Debugger_utils.Step) let continue state id = let open Utils.Syntaxes.Option in @@ -338,15 +317,12 @@ functor in let end_ = let end_, stack = - match at_id_exn id state |> fst with - | Nothing -> failwith "HORROR - map is Nothing!" - | FinalCmd _ -> (Some id, []) - | Cmd _ -> (None, [ (id, None) ]) - | BranchCmd { nexts; _ } -> + match (get_exn state.map id).next with + | None -> (Some id, []) + | Some (Single _) -> (None, [ (id, None) ]) + | Some (Branch nexts) -> let stack = - nexts |> Hashtbl.to_seq - |> Seq.map (fun (case, _) -> (id, Some case)) - |> List.of_seq + nexts |> List.map (fun (case, _) -> (id, Some case)) in (None, stack) in @@ -358,23 +334,22 @@ functor let step_out = continue - let continue_back t _ = - match t.map with - | Nothing -> failwith "HORROR - map is Nothing!" - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> - (data.id, Debugger_utils.Step) + (* TODO: breakpoints *) + let continue_back t _ = (Option.get t.map.root, Debugger_utils.Step) let init_manual proc_name all_procs = - let id_map = Hashtbl.create 1 in - let state = { map = Nothing; root_proc = proc_name; all_procs; id_map } in + let map = Exec_map.make () in + let state = { map; root_proc = proc_name; all_procs } in let finish_init exec_data () = let exec_data = Option_utils.or_else (fun () -> Effect.perform (Step (None, None, []))) exec_data in - let () = state.map <- new_cmd id_map exec_data ~parent:None () in - (exec_data.id, Debugger_utils.Step) + let cmd = new_cmd map exec_data ~parent:None () in + let id = cmd.data.id in + let () = map.root <- Some id in + (id, Debugger_utils.Step) in (state, finish_init) diff --git a/GillianCore/debugging/lifter/lifter.ml b/GillianCore/debugging/lifter/lifter.ml index 63eee4c39..044dbc3c4 100644 --- a/GillianCore/debugging/lifter/lifter.ml +++ b/GillianCore/debugging/lifter/lifter.ml @@ -3,10 +3,10 @@ include Lifter_intf let make_executed_cmd_data ?(is_breakpoint = false) - kind + next_kind id cmd_report ?(matches = []) ?(errors = []) branch_path = - { is_breakpoint; kind; id; cmd_report; matches; errors; branch_path } + { is_breakpoint; next_kind; id; cmd_report; matches; errors; branch_path } diff --git a/GillianCore/debugging/lifter/lifter_intf.ml b/GillianCore/debugging/lifter/lifter_intf.ml index 982d3a0aa..b6a236436 100644 --- a/GillianCore/debugging/lifter/lifter_intf.ml +++ b/GillianCore/debugging/lifter/lifter_intf.ml @@ -11,7 +11,7 @@ module Types = struct type 'cmd_report executed_cmd_data = { is_breakpoint : bool; - kind : (Branch_case.t, unit) Exec_map.cmd_kind; + next_kind : (Branch_case.t, unit) Exec_map.next_kind; id : Logging.Report_id.t; cmd_report : 'cmd_report; matches : Exec_map.matching list; @@ -100,9 +100,6 @@ module type S = sig (** Gives a list of matches that occurred at the specified command. *) val get_matches_at_id : Logging.Report_id.t -> t -> Exec_map.matching list - (** Gives the id of the root (first) command in the execution map. *) - val get_root_id : t -> Logging.Report_id.t option - val memory_error_to_exception_info : (memory_error, annot, tl_ast) memory_error_info -> exception_info @@ -126,7 +123,7 @@ module type Intf = sig val make_executed_cmd_data : ?is_breakpoint:bool -> - (Branch_case.t, unit) Exec_map.cmd_kind -> + (Branch_case.t, unit) Exec_map.next_kind -> Logging.Report_id.t -> 'cmd_report -> ?matches:Exec_map.matching list -> diff --git a/GillianCore/debugging/utils/exec_map.ml b/GillianCore/debugging/utils/exec_map.ml index 282b43534..be63696f0 100644 --- a/GillianCore/debugging/utils/exec_map.ml +++ b/GillianCore/debugging/utils/exec_map.ml @@ -32,43 +32,73 @@ (**/**) module L = Logging +open Utils.Prelude +open Utils.Syntaxes.Option (**/**) (** The "kind" of a command in an exec map *) -type ('c, 'bd) cmd_kind = - | Normal (** A command that doesn't branch or terminate *) - | Branch of ('c * 'bd) list (** A branching command *) - | Final (** A terminating command *) +type ('c, 'bd) next_kind = + | One of 'bd (** A command that doesn't branch or terminate *) + | Many of ('c * 'bd) list (** A branching command *) + | Zero (** A terminating command *) [@@deriving yojson] (** Maps a list of branches to [Normal] if empty, or [Branch] *) let kind_of_cases = function - | [] -> Normal - | cases -> Branch (List.map (fun case -> (case, ())) cases) + | [] -> One () + | cases -> Many (List.map (fun case -> (case, ())) cases) (** An exec map / node in an exec map; takes the following type parameters: - ['branch_case]: the type that identifies a branch case - ['cmd_data]: the type of the data attached to each non-[Nothing] node - ['branch_data]: additional data attached to each branch case *) -type ('branch_case, 'cmd_data, 'branch_data) t = - | Nothing (** An empty space; represents a command yet to be executed*) - | Cmd of { - data : 'cmd_data; - mutable next : ('branch_case, 'cmd_data, 'branch_data) t; - } (** A non-branching command with one next command *) - | BranchCmd of { - data : 'cmd_data; - nexts : - ( 'branch_case, - 'branch_data * ('branch_case, 'cmd_data, 'branch_data) t ) - Hashtbl.t; - } (** A branching command, with one or more branch cases *) - | FinalCmd of { data : 'cmd_data } - (** A command with no subsequent ones, either due to normal termination or an error*) +(* type ('branch_case, 'cmd_data, 'branch_data) t = + | Nothing (** An empty space; represents a command yet to be executed*) + | Cmd of { + data : 'cmd_data; + mutable next : ('branch_case, 'cmd_data, 'branch_data) t; + } (** A non-branching command with one next command *) + | BranchCmd of { + data : 'cmd_data; + nexts : + ( 'branch_case, + 'branch_data * ('branch_case, 'cmd_data, 'branch_data) t ) + Hashtbl.t; + } (** A branching command, with one or more branch cases *) + | FinalCmd of { data : 'cmd_data } + (** A command with no subsequent ones, either due to normal termination or an error*) + [@@deriving yojson] *) + +type ('id, 'case, 'branch_data) next = + | Single of ('id option * 'branch_data) + | Branch of ('case * ('id option * 'branch_data)) list +[@@deriving yojson] + +type ('id, 'case, 'data, 'bdata) node = { + data : 'data; + next : ('id, 'case, 'bdata) next option; +} +[@@deriving yojson] + +type ('id, 'case, 'cmd_data, 'branch_data) entry = + | Node of ('id, 'case, 'cmd_data, 'branch_data) node + | Alias of 'id [@@deriving yojson] +type ('id, 'branch_case, 'cmd_data, 'branch_data) map = { + mutable root : 'id option; + entries : ('id, ('id, 'branch_case, 'cmd_data, 'branch_data) entry) Hashtbl.t; +} +[@@deriving yojson] + +(**/**) + +(**/**) + +(** A command in an exec map *) + (** Used for various map-traversal commands; signifies when to stop exploring paths *) type stop_at = | StartOfPath (** Stop at the start of the path, i.e. as soon as possible *) @@ -90,17 +120,73 @@ type 't submap = | Proc of string (** Embed the execution of another proc as a submap *) [@@deriving yojson] +let make () = { root = None; entries = Hashtbl.create 1 } + +(* Gets the node at an ID (while resolving aliases), along with its true ID *) +let rec get_with_id map id = + match Hashtbl.find_opt map.entries id with + | Some (Node node) -> Some (node, id) + | Some (Alias id) -> get_with_id map id + | None -> None + +(* Gets the node at an ID (while resolving aliases) *) +let get map id = get_with_id map id |> Option.map fst + +let map_node_extra map id f = + match get_with_id map id with + | Some (node, id) -> + let new_node, aux = f node in + let () = Hashtbl.replace map.entries id (Node new_node) in + Some aux + | None -> None + +let map_node_extra_exn map id f = + match map_node_extra map id f with + | Some aux -> aux + | None -> raise Not_found + +(* Maps a node at an ID, returning true if found, and false if not *) +let map_node map id f = + let f node = (f node, ()) in + match map_node_extra map id f with + | Some () -> true + | None -> false + +(* Maps a node at an ID. Raises [Not_found] if not found. *) +let map_node_exn map id f = if map_node map f id then () else raise Not_found + +let insert map ~id ~all_ids node = + let () = + List.iter (fun id' -> Hashtbl.replace map.entries id' (Alias id)) all_ids + in + let () = Hashtbl.replace map.entries id (Node node) in + () + +let get_exn map id = + match get map id with + | Some node -> node + | None -> failwith "Exec_map.get" + (** Traverse the map depth-first, giving the path to the first node that matches the given predicate (or [None] otherwise) *) let find_path pred map = - let rec aux acc = function - | (Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data }) - when pred data -> Some acc - | Cmd { next; _ } -> aux acc next - | BranchCmd { nexts; _ } -> - nexts |> Hashtbl.find_map (fun case (_, next) -> aux (case :: acc) next) - | _ -> None + let rec aux acc node = + let/ () = if pred node then Some acc else None in + let* next = node.next in + match next with + | Single (None, _) -> None + | Single (Some id, _) -> + let* next = get map id in + aux acc next + | Branch cases -> + cases + |> List.find_map (fun (case, (id, _)) -> + let* id = id in + let* next = get map id in + aux (case :: acc) next) in - aux [] map + let* root_id = map.root in + let* root = get map root_id in + aux [] root (** Exception-raising equivalent to [find_path] *) let find_path_exn pred map = @@ -110,31 +196,32 @@ let find_path_exn pred map = (** Gets the node at the given path *) let at_path ?(stop_at = EndOfPath) path map = - let rec aux path map = - match (map, path, stop_at) with - | map, [], StartOfPath -> Some map - | (Cmd { next = Nothing; _ } as map), [], BeforeNothing -> Some map - | (BranchCmd { nexts; _ } as map), [ case ], BeforeNothing - when Hashtbl.find_opt nexts case |> Option.map snd = Some Nothing -> - Some map - | Cmd { next; _ }, _, _ -> aux path next - | BranchCmd { nexts; _ }, case :: path, _ -> ( - match Hashtbl.find_opt nexts case with - | Some (_, next) -> aux path next - | None -> None) - | map, [], (EndOfPath | BeforeNothing) -> Some map + let is_branch_empty case nexts = + match List.assoc_opt case nexts with + | Some (None, _) -> true + | _ -> false + in + let rec aux path node = + match (node.next, path, stop_at) with + | _, [], StartOfPath -> Some node + | Some (Single (None, _)), [], BeforeNothing -> Some node + | Some (Branch nexts), [ case ], BeforeNothing + when is_branch_empty case nexts -> Some node + | Some (Single (Some id, _)), _, _ -> + let* next = get map id in + aux path next + | Some (Branch nexts), case :: path, _ -> ( + match List.assoc_opt case nexts with + | Some (Some id, _) -> + let* next = get map id in + aux path next + | _ -> None) + | _, [], (EndOfPath | BeforeNothing) -> Some node | _, _, _ -> None in - aux (List.rev path) map - -let get_cmd_data = function - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> Some data - | Nothing -> None - -let get_cmd_data_exn map = - match get_cmd_data map with - | Some map -> map - | None -> failwith "Tried to get data from Nothing map" + let* root_id = map.root in + let* root = get map root_id in + aux (List.rev path) root (** Exception-raising equivalent to [at_path] *) let at_path_exn ?(stop_at = EndOfPath) path map = @@ -142,67 +229,53 @@ let at_path_exn ?(stop_at = EndOfPath) path map = | Some map -> map | None -> failwith "Exec_map.at_path" -let map_data f = function - | Nothing -> Nothing - | Cmd { data; next } -> Cmd { data = f data; next } - | BranchCmd { data; nexts } -> BranchCmd { data = f data; nexts } - | FinalCmd { data } -> FinalCmd { data = f data } - (** An Exec_map to be passed to the debugger frontend and displayed *) module Packaged = struct - type branch_case = string * Yojson.Safe.t [@@deriving yojson] - - (* Need this to avoid name conflict *) - (**/**) + type id = L.Report_id.t [@@deriving yojson] + type branch_case = Yojson.Safe.t [@@deriving yojson] - type ('branch_case, 'cmd_data, 'branch_data) _map = - ('branch_case, 'cmd_data, 'branch_data) t - [@@deriving yojson] - - (**/**) - - type t = (branch_case, cmd_data, unit) _map - - and cmd_data = { + type cmd_data = { id : L.Report_id.t; all_ids : L.Report_id.t list; display : string; matches : matching list; errors : string list; - submap : t submap; + submap : id submap; } [@@deriving yojson] + type branch_data = string [@@deriving yojson] + + type t = (L.Report_id.t, branch_case, cmd_data, branch_data) map + [@@deriving yojson] + (** Converts a GIL branch case to a packaged branch case *) - let package_gil_case (case : Branch_case.t) : branch_case = + let package_gil_case (case : Branch_case.t) : branch_case * branch_data = let json = Branch_case.to_yojson case in let display = Fmt.str "%a" Branch_case.pp_short case in - (display, json) + (json, display) (** Converts an Exec_map to a packaged Exec_map *) - let package package_data package_case (map : ('c, 'd, 'bd) _map) : t = - let rec aux map = - match map with - | Nothing -> Nothing - | Cmd { data; next } -> - Cmd { data = package_data aux data; next = aux next } - | BranchCmd { data; nexts } -> - let data = package_data aux data in - let all_cases = - nexts |> Hashtbl.to_seq |> List.of_seq - |> List.map (fun (c, (bd, _)) -> (c, bd)) - in - let nexts = - nexts - |> Hashtbl.map (fun case (bdata, next) -> - let case = package_case ~bd:bdata ~all_cases case in - let next = aux next in - (case, ((), next))) + let package + package_id + package_node + ({ root; entries } : ('i, 'c, 'd, 'bd) map) : t = + let map' = + { + root = Option.map package_id root; + entries = Hashtbl.create (Hashtbl.length entries); + } + in + let () = + Hashtbl.iter + (fun id entry -> + let entry' = + match entry with + | Node node -> Node (package_node node) + | Alias id -> Alias (package_id id) in - BranchCmd { data; nexts } - | FinalCmd { data } -> - let data = package_data aux data in - FinalCmd { data } + Hashtbl.replace map'.entries (package_id id) entry') + entries in - aux map + map' end diff --git a/GillianCore/utils/list_utils.ml b/GillianCore/utils/list_utils.ml index 3624e8bb6..4c3a2b1b9 100644 --- a/GillianCore/utils/list_utils.ml +++ b/GillianCore/utils/list_utils.ml @@ -246,3 +246,8 @@ let[@tail_mod_cons] rec map_last f l = | [] -> [] | [ x ] -> [ f x ] | x :: l' -> x :: map_last f l' + +let[@tail_mod_cons] rec assoc_replace k v = function + | [] -> [ (k, v) ] + | (k', _) :: r when k = k' -> (k, v) :: r + | x :: r -> x :: assoc_replace k v r diff --git a/debugger-vscode-extension/.eslintrc.js b/debug-ui/.eslintrc.js similarity index 94% rename from debugger-vscode-extension/.eslintrc.js rename to debug-ui/.eslintrc.js index 2a52466b3..ec96732e9 100644 --- a/debugger-vscode-extension/.eslintrc.js +++ b/debug-ui/.eslintrc.js @@ -20,6 +20,6 @@ module.exports = { '@typescript-eslint/explicit-module-boundary-types': 0, '@typescript-eslint/no-non-null-assertion': 0, }, - ignorePatterns: ['sampleWorkspace'], + ignorePatterns: ['examples'], env: {'node': true} }; \ No newline at end of file diff --git a/debugger-vscode-extension/.gitignore b/debug-ui/.gitignore similarity index 75% rename from debugger-vscode-extension/.gitignore rename to debug-ui/.gitignore index f9acb94bf..bd4a6a6fe 100644 --- a/debugger-vscode-extension/.gitignore +++ b/debug-ui/.gitignore @@ -9,4 +9,4 @@ mock-debug.txt *.vsix .snowpack yarn-error.log -sampleWorkspace/.vscode/settings.json \ No newline at end of file +debug-ui/.vscode/settings.json \ No newline at end of file diff --git a/debugger-vscode-extension/.prettierrc b/debug-ui/.prettierrc similarity index 100% rename from debugger-vscode-extension/.prettierrc rename to debug-ui/.prettierrc diff --git a/debugger-vscode-extension/.vscodeignore b/debug-ui/.vscodeignore similarity index 95% rename from debugger-vscode-extension/.vscodeignore rename to debug-ui/.vscodeignore index 79e854561..8c8afb2f4 100644 --- a/debugger-vscode-extension/.vscodeignore +++ b/debug-ui/.vscodeignore @@ -15,6 +15,6 @@ node_modules tailwind.config.json webpack.config.js screenshots -sampleWorkspace +examples **/*.config.js tsconfig-webview.json diff --git a/debugger-vscode-extension/README.md b/debug-ui/README.md similarity index 100% rename from debugger-vscode-extension/README.md rename to debug-ui/README.md diff --git a/debugger-vscode-extension/build/extension.webpack.config.js b/debug-ui/build/extension.webpack.config.js similarity index 100% rename from debugger-vscode-extension/build/extension.webpack.config.js rename to debug-ui/build/extension.webpack.config.js diff --git a/debugger-vscode-extension/sampleWorkspace/.vscode/launch.json b/debug-ui/examples/.vscode/launch.json similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/.vscode/launch.json rename to debug-ui/examples/.vscode/launch.json diff --git a/debug-ui/examples/.vscode/settings.json b/debug-ui/examples/.vscode/settings.json new file mode 100644 index 000000000..cc754b97c --- /dev/null +++ b/debug-ui/examples/.vscode/settings.json @@ -0,0 +1,3 @@ +{ + "gillianDebugger.sourceDirectory": "${workspaceFolder}/../../" +} \ No newline at end of file diff --git a/debugger-vscode-extension/sampleWorkspace/compcert-c/amazon/bugs/mega.c b/debug-ui/examples/compcert-c/amazon/bugs/mega.c similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/compcert-c/amazon/bugs/mega.c rename to debug-ui/examples/compcert-c/amazon/bugs/mega.c diff --git a/debugger-vscode-extension/sampleWorkspace/compcert-c/amazon/logic/ByteLogic.gil b/debug-ui/examples/compcert-c/amazon/logic/ByteLogic.gil similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/compcert-c/amazon/logic/ByteLogic.gil rename to debug-ui/examples/compcert-c/amazon/logic/ByteLogic.gil diff --git a/debugger-vscode-extension/sampleWorkspace/compcert-c/amazon/logic/EncryptionHeaderLogic.gil b/debug-ui/examples/compcert-c/amazon/logic/EncryptionHeaderLogic.gil similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/compcert-c/amazon/logic/EncryptionHeaderLogic.gil rename to debug-ui/examples/compcert-c/amazon/logic/EncryptionHeaderLogic.gil diff --git a/debugger-vscode-extension/sampleWorkspace/compcert-c/amazon/logic/ListLogic.gil b/debug-ui/examples/compcert-c/amazon/logic/ListLogic.gil similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/compcert-c/amazon/logic/ListLogic.gil rename to debug-ui/examples/compcert-c/amazon/logic/ListLogic.gil diff --git a/debugger-vscode-extension/sampleWorkspace/compcert-c/amazon/logic/StringStruct.gil b/debug-ui/examples/compcert-c/amazon/logic/StringStruct.gil similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/compcert-c/amazon/logic/StringStruct.gil rename to debug-ui/examples/compcert-c/amazon/logic/StringStruct.gil diff --git a/debugger-vscode-extension/sampleWorkspace/compcert-c/amazon/logic/Utf8Logic.gil b/debug-ui/examples/compcert-c/amazon/logic/Utf8Logic.gil similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/compcert-c/amazon/logic/Utf8Logic.gil rename to debug-ui/examples/compcert-c/amazon/logic/Utf8Logic.gil diff --git a/debugger-vscode-extension/sampleWorkspace/compcert-c/amazon/logic/hash_table_ax.gil b/debug-ui/examples/compcert-c/amazon/logic/hash_table_ax.gil similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/compcert-c/amazon/logic/hash_table_ax.gil rename to debug-ui/examples/compcert-c/amazon/logic/hash_table_ax.gil diff --git a/debugger-vscode-extension/sampleWorkspace/kani-c/wpst/llen.c b/debug-ui/examples/kani-c/wpst/llen.c similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/kani-c/wpst/llen.c rename to debug-ui/examples/kani-c/wpst/llen.c diff --git a/debugger-vscode-extension/sampleWorkspace/kani-c/wpst/llen.c.symtab.json b/debug-ui/examples/kani-c/wpst/llen.c.symtab.json similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/kani-c/wpst/llen.c.symtab.json rename to debug-ui/examples/kani-c/wpst/llen.c.symtab.json diff --git a/debugger-vscode-extension/sampleWorkspace/kani-c/wpst/simple_branch.c b/debug-ui/examples/kani-c/wpst/simple_branch.c similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/kani-c/wpst/simple_branch.c rename to debug-ui/examples/kani-c/wpst/simple_branch.c diff --git a/debugger-vscode-extension/sampleWorkspace/kani-c/wpst/simple_branch.c.symtab.gil b/debug-ui/examples/kani-c/wpst/simple_branch.c.symtab.gil similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/kani-c/wpst/simple_branch.c.symtab.gil rename to debug-ui/examples/kani-c/wpst/simple_branch.c.symtab.gil diff --git a/debugger-vscode-extension/sampleWorkspace/kani-c/wpst/simple_branch.c.symtab.json b/debug-ui/examples/kani-c/wpst/simple_branch.c.symtab.json similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/kani-c/wpst/simple_branch.c.symtab.json rename to debug-ui/examples/kani-c/wpst/simple_branch.c.symtab.json diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/lab/dll/auto.wisl b/debug-ui/examples/wisl/lab/dll/auto.wisl similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/lab/dll/auto.wisl rename to debug-ui/examples/wisl/lab/dll/auto.wisl diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/lab/dll/manual.wisl b/debug-ui/examples/wisl/lab/dll/manual.wisl similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/lab/dll/manual.wisl rename to debug-ui/examples/wisl/lab/dll/manual.wisl diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/lab/dll/manual_solutions.wisl b/debug-ui/examples/wisl/lab/dll/manual_solutions.wisl similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/lab/dll/manual_solutions.wisl rename to debug-ui/examples/wisl/lab/dll/manual_solutions.wisl diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/lab/sll/auto.wisl b/debug-ui/examples/wisl/lab/sll/auto.wisl similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/lab/sll/auto.wisl rename to debug-ui/examples/wisl/lab/sll/auto.wisl diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/lab/sll/manual.wisl b/debug-ui/examples/wisl/lab/sll/manual.wisl similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/lab/sll/manual.wisl rename to debug-ui/examples/wisl/lab/sll/manual.wisl diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/lab/sll/manual_solutions.wisl b/debug-ui/examples/wisl/lab/sll/manual_solutions.wisl similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/lab/sll/manual_solutions.wisl rename to debug-ui/examples/wisl/lab/sll/manual_solutions.wisl diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/verify/SLL_ex_complete.wisl b/debug-ui/examples/wisl/verify/SLL_ex_complete.wisl similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/verify/SLL_ex_complete.wisl rename to debug-ui/examples/wisl/verify/SLL_ex_complete.wisl diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/verify/gil/SLL_ex_complete.gil b/debug-ui/examples/wisl/verify/gil/SLL_ex_complete.gil similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/verify/gil/SLL_ex_complete.gil rename to debug-ui/examples/wisl/verify/gil/SLL_ex_complete.gil diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/verify/gil/list_dispose.gil b/debug-ui/examples/wisl/verify/gil/list_dispose.gil similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/verify/gil/list_dispose.gil rename to debug-ui/examples/wisl/verify/gil/list_dispose.gil diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/verify/gil/list_dispose_bad.gil b/debug-ui/examples/wisl/verify/gil/list_dispose_bad.gil similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/verify/gil/list_dispose_bad.gil rename to debug-ui/examples/wisl/verify/gil/list_dispose_bad.gil diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/verify/gil/list_length_iter.gil b/debug-ui/examples/wisl/verify/gil/list_length_iter.gil similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/verify/gil/list_length_iter.gil rename to debug-ui/examples/wisl/verify/gil/list_length_iter.gil diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/verify/gil/list_length_rec.gil b/debug-ui/examples/wisl/verify/gil/list_length_rec.gil similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/verify/gil/list_length_rec.gil rename to debug-ui/examples/wisl/verify/gil/list_length_rec.gil diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/verify/gil/list_length_rec_bad_2.gil b/debug-ui/examples/wisl/verify/gil/list_length_rec_bad_2.gil similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/verify/gil/list_length_rec_bad_2.gil rename to debug-ui/examples/wisl/verify/gil/list_length_rec_bad_2.gil diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/verify/list_dispose.wisl b/debug-ui/examples/wisl/verify/list_dispose.wisl similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/verify/list_dispose.wisl rename to debug-ui/examples/wisl/verify/list_dispose.wisl diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/verify/list_dispose_bad.wisl b/debug-ui/examples/wisl/verify/list_dispose_bad.wisl similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/verify/list_dispose_bad.wisl rename to debug-ui/examples/wisl/verify/list_dispose_bad.wisl diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/verify/list_length_iter.wisl b/debug-ui/examples/wisl/verify/list_length_iter.wisl similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/verify/list_length_iter.wisl rename to debug-ui/examples/wisl/verify/list_length_iter.wisl diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/verify/list_length_rec.wisl b/debug-ui/examples/wisl/verify/list_length_rec.wisl similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/verify/list_length_rec.wisl rename to debug-ui/examples/wisl/verify/list_length_rec.wisl diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/verify/list_length_rec_bad_1.wisl b/debug-ui/examples/wisl/verify/list_length_rec_bad_1.wisl similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/verify/list_length_rec_bad_1.wisl rename to debug-ui/examples/wisl/verify/list_length_rec_bad_1.wisl diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/verify/list_length_rec_bad_2.wisl b/debug-ui/examples/wisl/verify/list_length_rec_bad_2.wisl similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/verify/list_length_rec_bad_2.wisl rename to debug-ui/examples/wisl/verify/list_length_rec_bad_2.wisl diff --git a/debugger-vscode-extension/sampleWorkspace/wisl/wpst/llen_wpst.wisl b/debug-ui/examples/wisl/wpst/llen_wpst.wisl similarity index 100% rename from debugger-vscode-extension/sampleWorkspace/wisl/wpst/llen_wpst.wisl rename to debug-ui/examples/wisl/wpst/llen_wpst.wisl diff --git a/debugger-vscode-extension/package.json b/debug-ui/package.json similarity index 100% rename from debugger-vscode-extension/package.json rename to debug-ui/package.json diff --git a/debugger-vscode-extension/postcss.config.js b/debug-ui/postcss.config.js similarity index 100% rename from debugger-vscode-extension/postcss.config.js rename to debug-ui/postcss.config.js diff --git a/debugger-vscode-extension/snowpack.config.js b/debug-ui/snowpack.config.js similarity index 100% rename from debugger-vscode-extension/snowpack.config.js rename to debug-ui/snowpack.config.js diff --git a/debugger-vscode-extension/src/WebviewPanel.ts b/debug-ui/src/WebviewPanel.ts similarity index 100% rename from debugger-vscode-extension/src/WebviewPanel.ts rename to debug-ui/src/WebviewPanel.ts diff --git a/debugger-vscode-extension/src/activateCodeLens.ts b/debug-ui/src/activateCodeLens.ts similarity index 96% rename from debugger-vscode-extension/src/activateCodeLens.ts rename to debug-ui/src/activateCodeLens.ts index 13207362a..d2e35ca44 100644 --- a/debugger-vscode-extension/src/activateCodeLens.ts +++ b/debug-ui/src/activateCodeLens.ts @@ -38,15 +38,17 @@ export function activateCodeLens(context: ExtensionContext) { function getLensKinds(): [ExecMode, string][] { const config = workspace.getConfiguration('gillianDebugger'); const lensKinds: [ExecMode, string][] = []; - if (config.showVerifyLens) - lensKinds.push(['debugverify', 'Verify ']); + if (config.showVerifyLens) lensKinds.push(['debugverify', 'Verify ']); if (config.showSymbolicDebugLens) lensKinds.push(['debugwpst', 'Symbolic-debug ']); return lensKinds; } class DebugCodeLensProvider implements CodeLensProvider { - private makeLensesFromPattern(pattern: RegExp, document: TextDocument): CodeLens[] { + private makeLensesFromPattern( + pattern: RegExp, + document: TextDocument + ): CodeLens[] { const text = document.getText(); const procNamePattern = /(.+?)\(/g; diff --git a/debugger-vscode-extension/src/commands.ts b/debug-ui/src/commands.ts similarity index 100% rename from debugger-vscode-extension/src/commands.ts rename to debug-ui/src/commands.ts diff --git a/debugger-vscode-extension/src/debug.ts b/debug-ui/src/debug.ts similarity index 100% rename from debugger-vscode-extension/src/debug.ts rename to debug-ui/src/debug.ts diff --git a/debugger-vscode-extension/src/extension.ts b/debug-ui/src/extension.ts similarity index 98% rename from debugger-vscode-extension/src/extension.ts rename to debug-ui/src/extension.ts index eefc4ae89..314d55d90 100644 --- a/debugger-vscode-extension/src/extension.ts +++ b/debug-ui/src/extension.ts @@ -28,7 +28,8 @@ function expandPath(s: string): string { } class DebugAdapterExecutableFactory - implements vscode.DebugAdapterDescriptorFactory { + implements vscode.DebugAdapterDescriptorFactory +{ // The following use of a DebugAdapter factory shows how to control what debug adapter executable is used. // Since the code implements the default behavior, it is absolutely not neccessary and we show it here only for educational purpose. diff --git a/debugger-vscode-extension/src/lib.ts b/debug-ui/src/lib.ts similarity index 100% rename from debugger-vscode-extension/src/lib.ts rename to debug-ui/src/lib.ts diff --git a/debugger-vscode-extension/src/types.d.ts b/debug-ui/src/types.d.ts similarity index 84% rename from debugger-vscode-extension/src/types.d.ts rename to debug-ui/src/types.d.ts index 814aa00ec..0caab9b97 100644 --- a/debugger-vscode-extension/src/types.d.ts +++ b/debug-ui/src/types.d.ts @@ -1,10 +1,10 @@ // #region ExecMap -export type BranchCase = [string, any]; +export type BranchCase = NonNullable; type Submap = | readonly ['NoSubmap'] - | readonly ['Submap', ExecMap] + | readonly ['Submap', number] | readonly ['Proc', string]; type Matching = { @@ -22,14 +22,28 @@ export type CmdData = { readonly submap: Submap; }; -export type ExecMap = - | readonly ['Nothing'] - | readonly ['Cmd', { data: CmdData; next: ExecMap }] - | readonly [ - 'BranchCmd', - { data: CmdData; nexts: [BranchCase, [null, ExecMap]][] } - ] - | readonly ['FinalCmd', { data: CmdData }]; +export type ExecMapNext = + | ['Single', [number | null, string]] + | ['Branch', readonly [BranchCase, [number | null, string]][]]; + +export type ExecMapNode = { + readonly data: CmdData; + readonly next: ExecMapNext | null; +}; + +export type ExecMapEntry = + | readonly ['Node', ExecMapNode] + | readonly ['Alias', number]; + +export type ExecMap = { + readonly root: number | null; + readonly entries: [number, ExecMapEntry][]; +}; + +export type SafeExecMap = { + readonly root: number | null; + readonly entries: Record; +}; // #endregion diff --git a/debugger-vscode-extension/src/vscode-variables.d.ts b/debug-ui/src/vscode-variables.d.ts similarity index 100% rename from debugger-vscode-extension/src/vscode-variables.d.ts rename to debug-ui/src/vscode-variables.d.ts diff --git a/debugger-vscode-extension/src/vscodeVariables.ts b/debug-ui/src/vscodeVariables.ts similarity index 100% rename from debugger-vscode-extension/src/vscodeVariables.ts rename to debug-ui/src/vscodeVariables.ts diff --git a/debugger-vscode-extension/src/webviews/src/App.tsx b/debug-ui/src/webviews/src/App.tsx similarity index 100% rename from debugger-vscode-extension/src/webviews/src/App.tsx rename to debug-ui/src/webviews/src/App.tsx diff --git a/debugger-vscode-extension/src/webviews/src/DebuggerPanel/DebuggerPanel.css b/debug-ui/src/webviews/src/DebuggerPanel/DebuggerPanel.css similarity index 100% rename from debugger-vscode-extension/src/webviews/src/DebuggerPanel/DebuggerPanel.css rename to debug-ui/src/webviews/src/DebuggerPanel/DebuggerPanel.css diff --git a/debugger-vscode-extension/src/webviews/src/DebuggerPanel/DebuggerPanel.tsx b/debug-ui/src/webviews/src/DebuggerPanel/DebuggerPanel.tsx similarity index 100% rename from debugger-vscode-extension/src/webviews/src/DebuggerPanel/DebuggerPanel.tsx rename to debug-ui/src/webviews/src/DebuggerPanel/DebuggerPanel.tsx diff --git a/debugger-vscode-extension/src/webviews/src/ExecMap/ExecMap.css b/debug-ui/src/webviews/src/ExecMap/ExecMap.css similarity index 100% rename from debugger-vscode-extension/src/webviews/src/ExecMap/ExecMap.css rename to debug-ui/src/webviews/src/ExecMap/ExecMap.css diff --git a/debugger-vscode-extension/src/webviews/src/ExecMap/ExecMapNode.tsx b/debug-ui/src/webviews/src/ExecMap/ExecMapNode.tsx similarity index 96% rename from debugger-vscode-extension/src/webviews/src/ExecMap/ExecMapNode.tsx rename to debug-ui/src/webviews/src/ExecMap/ExecMapNode.tsx index f4bca1296..78bb3f026 100644 --- a/debugger-vscode-extension/src/webviews/src/ExecMap/ExecMapNode.tsx +++ b/debug-ui/src/webviews/src/ExecMap/ExecMapNode.tsx @@ -5,7 +5,7 @@ import { VSCodeDivider, } from '@vscode/webview-ui-toolkit/react'; import { CmdData } from '../../../types'; -import type { Dims } from '../TreeMapView/TreeMapView'; +import type { NodeData } from '../TreeMapView/TreeMapView'; import NodeWrap from '../TreeMapView/NodeWrap'; import { NodeProps } from 'react-flow-renderer'; import { Code } from '../util'; @@ -34,7 +34,7 @@ export type ExecMapNodeData = { isActive: boolean } & ( } ); -const ExecMapNode = ({ data }: NodeProps) => { +const ExecMapNode = ({ data }: NodeProps) => { const { type, isActive, width, height } = data; if (type === 'Empty') { return ( diff --git a/debug-ui/src/webviews/src/ExecMap/ExecMapView.tsx b/debug-ui/src/webviews/src/ExecMap/ExecMapView.tsx new file mode 100644 index 000000000..8bf437c26 --- /dev/null +++ b/debug-ui/src/webviews/src/ExecMap/ExecMapView.tsx @@ -0,0 +1,239 @@ +import React from 'react'; +import { + BranchCase, + DebuggerState, + DebugProcState, + ExecMap, + SafeExecMap, +} from '../../../types'; +import TreeMapView, { PreNode as PreNode_ } from '../TreeMapView/TreeMapView'; +import { execSpecific, jumpToId, startProc } from '../VSCodeAPI'; +import ExecMapNode, { ExecMapNodeData } from './ExecMapNode'; +import { NODE_HEIGHT, DEFAULT_NODE_SIZE } from '../TreeMapView/TreeMapView'; + +export type Props = { + state: DebuggerState; + expandedNodes: Set; + toggleNodeExpanded: (id: string) => void; +}; + +type Id = + | ['Root'] + | ['Node', string, number] + | ['Empty'] + | ['ProcEmpty', string]; +type Aux = { + parentNode: string | undefined; + parentId: number | undefined; + branchCase: BranchCase | undefined; + edgeLabel: string; +}; +type D = ExecMapNodeData; +type PreNode = PreNode_; + +const emptyAux = { + parentNode: undefined, + parentId: undefined, + branchCase: undefined, + edgeLabel: '', +}; + +const ExecMapView = ({ state, expandedNodes, toggleNodeExpanded }: Props) => { + const { mainProc: mainProcName, currentProc: currentProcName, procs } = state; + + const procMapCache: Record = {}; + const getProcAndMap = ( + procName: string + ): [DebugProcState, SafeExecMap] | undefined => { + if (!(procName in procMapCache)) { + const proc = procs[procName]; + if (proc === undefined) return undefined; + const rawMap = proc.liftedExecMap ?? proc.execMap; + const map: SafeExecMap = { + root: rawMap.root, + entries: Object.fromEntries(rawMap.entries), + }; + procMapCache[procName] = [proc, map]; + } + return procMapCache[procName]; + }; + + const getRoot = (): PreNode => { + const procAndMap = getProcAndMap(mainProcName); + if (procAndMap === undefined) + throw `Couldn't find main proc ${mainProcName}`; + const rootId = procAndMap[1].root!; + const next: Id = ['Node', mainProcName, rootId]; + return { + id: 'root', + submap: undefined, + parent: undefined, + nexts: [[next, { ...emptyAux, parentNode: 'root' }]], + edgeLabel: undefined, + ...DEFAULT_NODE_SIZE, + data: { + type: 'Root', + procName: mainProcName, + isActive: currentProcName === mainProcName, + }, + }; + }; + + let emptyCount = 0; + const getEmpty = (aux: Aux): PreNode => { + const { parentNode, parentId, branchCase, edgeLabel } = aux; + if (parentId === undefined) throw 'Empty with no parent ID!'; + return { + id: `empty${emptyCount++}`, + submap: undefined, + parent: parentNode, + nexts: [], + edgeLabel, + width: NODE_HEIGHT, + height: NODE_HEIGHT, + data: { + type: 'Empty', + hasParent: true, + isActive: false, + exec: () => { + execSpecific(parentId, branchCase || null); + }, + }, + }; + }; + + const getProcEmpty = (procName: string): PreNode => { + return { + id: `empty-${procName}`, + submap: undefined, + parent: undefined, + nexts: [], + edgeLabel: undefined, + width: NODE_HEIGHT, + height: NODE_HEIGHT, + data: { + type: 'Empty', + hasParent: false, + isActive: false, + exec: () => { + startProc(procName); + }, + }, + }; + }; + + const getNode = (nodeId: Id, aux: Aux): PreNode => { + if (nodeId[0] === 'Root') return getRoot(); + if (nodeId[0] === 'Empty') return getEmpty(aux); + if (nodeId[0] === 'ProcEmpty') return getProcEmpty(nodeId[1]); + + const procName = nodeId[1]; + const procAndMap = getProcAndMap(procName); + if (procAndMap === undefined) throw `Couldn't find proc ${procName}`; + const [proc, map] = procAndMap; + const entry = map.entries[nodeId[2]]; + if (entry === undefined) { + console.error({ proc, nodeId, aux }); + throw `Couldn't find entry ${nodeId[2]} in ${procName}`; + } + if (entry[0] === 'Alias') return getNode(['Node', procName, entry[1]], aux); + const node = entry[1]; + const cmdData = node.data; + const id = cmdData.id; + const expanded = expandedNodes.has(`${id}`); + + const submap = ((): [Id, Aux] | undefined => { + if (!expanded) return undefined; + if (node.data.submap[0] === 'NoSubmap') return undefined; + if (node.data.submap[0] === 'Submap') { + return [['Node', procName, node.data.submap[1]], emptyAux]; + } + if (node.data.submap[0] === 'Proc') { + const procName = node.data.submap[1]; + const procAndMap = getProcAndMap(procName); + if (procAndMap === undefined) + return [['ProcEmpty', procName], emptyAux]; + const rootId = procAndMap[1].root!; + return [['Node', procName, rootId], emptyAux]; + } + })(); + + const nexts = ((): [Id, Aux][] => { + if (node.next === null) return []; + if (node.next[0] === 'Single') { + const [nextId, edgeLabel] = node.next[1]; + const aux = { + parentNode: `${id}`, + parentId: id, + branchCase: undefined, + edgeLabel, + }; + if (nextId === null) { + return [[['Empty'], aux]]; + } + return [[['Node', procName, nextId], aux]]; + } + // node.next[0] === 'Branch' + return node.next[1].map(([branchCase, [nextId, edgeLabel]]) => { + const aux = { + parentNode: `${id}`, + parentId: id, + branchCase, + edgeLabel, + }; + if (nextId === null) { + return [['Empty'], aux]; + } + return [['Node', procName, nextId], aux]; + }); + })(); + + const isCurrentCmd = + procName === currentProcName && + cmdData.all_ids.includes(proc.currentCmdId); + + const toggleExpanded = + node.data.submap[0] === 'NoSubmap' + ? undefined + : () => { + toggleNodeExpanded(`${id}`); + }; + + const data: ExecMapNodeData = { + type: 'Cmd', + cmdData, + isFinal: nexts.length === 0, + isCurrentCmd, + hasParent: aux.parentNode !== undefined, + jump: () => { + jumpToId(id); + }, + expanded, + toggleExpanded, + isActive: procName === currentProcName, + }; + + return { + id: `${id}`, + submap, + parent: aux.parentNode, + nexts, + edgeLabel: aux.edgeLabel, + ...DEFAULT_NODE_SIZE, + data, + }; + }; + + return ( + + ); +}; + +export default ExecMapView; diff --git a/debugger-vscode-extension/src/webviews/src/MatchView/MatchData.css b/debug-ui/src/webviews/src/MatchView/MatchData.css similarity index 100% rename from debugger-vscode-extension/src/webviews/src/MatchView/MatchData.css rename to debug-ui/src/webviews/src/MatchView/MatchData.css diff --git a/debugger-vscode-extension/src/webviews/src/MatchView/MatchData.tsx b/debug-ui/src/webviews/src/MatchView/MatchData.tsx similarity index 100% rename from debugger-vscode-extension/src/webviews/src/MatchView/MatchData.tsx rename to debug-ui/src/webviews/src/MatchView/MatchData.tsx diff --git a/debugger-vscode-extension/src/webviews/src/MatchView/MatchMapNode.css b/debug-ui/src/webviews/src/MatchView/MatchMapNode.css similarity index 100% rename from debugger-vscode-extension/src/webviews/src/MatchView/MatchMapNode.css rename to debug-ui/src/webviews/src/MatchView/MatchMapNode.css diff --git a/debugger-vscode-extension/src/webviews/src/MatchView/MatchMapNode.tsx b/debug-ui/src/webviews/src/MatchView/MatchMapNode.tsx similarity index 95% rename from debugger-vscode-extension/src/webviews/src/MatchView/MatchMapNode.tsx rename to debug-ui/src/webviews/src/MatchView/MatchMapNode.tsx index c1b768af5..b08815d72 100644 --- a/debugger-vscode-extension/src/webviews/src/MatchView/MatchMapNode.tsx +++ b/debug-ui/src/webviews/src/MatchView/MatchMapNode.tsx @@ -3,7 +3,7 @@ import { NodeProps } from 'react-flow-renderer'; import { VSCodeBadge, VSCodeButton } from '@vscode/webview-ui-toolkit/react'; import { AssertionData, MatchResult } from '../../../types'; import NodeWrap from '../TreeMapView/NodeWrap'; -import type { Dims } from '../TreeMapView/TreeMapView'; +import type { NodeData } from '../TreeMapView/TreeMapView'; import './MatchMapNode.css'; @@ -31,7 +31,7 @@ export type MatchMapNodeData = type: 'Missing'; }; -const MatchMapNode = ({ data }: NodeProps) => { +const MatchMapNode = ({ data }: NodeProps) => { const { type, width, height } = data; if (type === 'Root') { const { title, subtitle } = data; diff --git a/debug-ui/src/webviews/src/MatchView/MatchMapView.tsx b/debug-ui/src/webviews/src/MatchView/MatchMapView.tsx new file mode 100644 index 000000000..3f81d93ca --- /dev/null +++ b/debug-ui/src/webviews/src/MatchView/MatchMapView.tsx @@ -0,0 +1,198 @@ +import React from 'react'; +import { + AssertionData, + MatchingState, + MatchMap, + MatchMapInner, + MatchResult, + MatchSeg, + MatchStep, +} from '../../../types'; +import TreeMapView, { + PreNode as PreNode_, + DEFAULT_NODE_SIZE, +} from '../TreeMapView/TreeMapView'; +import MatchMapNode, { MatchMapNodeData } from './MatchMapNode'; + +import 'allotment/dist/style.css'; +import { getMatchName } from '../util'; +import useStore from '../store'; + +type Props = { + matchId: number; + selectStep: (step: MatchStep) => void; + matches: Record; + expandedNodes: Set; + requestMatching: (id: number) => void; + toggleNodeExpanded: (id: number) => void; +}; + +type Id = ['Assertion', number] | ['Result', number] | ['Root', number]; +type Aux = string | undefined; +type D = MatchMapNodeData; +type PreNode = PreNode_; + +const MatchMapView = ({ + matchId: baseMatchId, + selectStep, + expandedNodes, + matches, + requestMatching, + toggleNodeExpanded, +}: Props) => { + const rootTitles = useStore(state => getMatchName(state)); + + const assertions: Record = {}; + const results: Record = {}; + + const selectedId = (() => { + const match = matches[baseMatchId]!; + if (!match.selected) { + return -1; + } + + if (match.selected[0] === 'Assertion') { + return match.selected[1].id; + } else if (match.selected[0] === 'Result') { + return match.selected[1]; + } + })(); + + const prepNext = (seg: MatchSeg): Id => { + if (seg[0] === 'Assertion') { + const id = seg[1].id; + assertions[id] = [seg[1], seg[2]]; + return ['Assertion', id]; + } + // seg[0] === 'Result' + const id = seg[1]; + results[id] = seg[2]; + return ['Result', id]; + }; + + const getRoot = (matchId: number): PreNode => { + const match = matches[matchId]; + if (match === undefined) throw `Couldn't find match ${matchId}!`; + const id = `root-${matchId}`; + const map = match.map as MatchMap; + const [title, subtitle] = + // eslint-disable-next-line react/jsx-key + matchId === baseMatchId ? rootTitles : [Fold, undefined]; + const nexts = ((): [Id, Aux][] => { + if (map[1][0] === 'Direct') { + return [[prepNext(map[1][1]), id]]; + } + // map[1][0] === 'Fold' + return map[1][1].map(seg => [prepNext(seg), id]); + })(); + return { + id, + submap: undefined, + parent: undefined, + nexts, + edgeLabel: undefined, + ...DEFAULT_NODE_SIZE, + data: { + type: 'Root', + title, + subtitle, + }, + }; + }; + + const getResult = (id: number, parent: Aux): PreNode => { + const result = results[id]; + return { + id: `result-${id}`, + submap: undefined, + parent, + nexts: [], + edgeLabel: undefined, + ...DEFAULT_NODE_SIZE, + data: { + type: 'Result', + result, + setSelected: () => { + selectStep(['Result', id, result]); + }, + }, + }; + }; + + const getAssertion = (asrtId: number, parent: Aux): PreNode => { + const assertion = assertions[asrtId]; + if (assertion === undefined) throw `Couldn't find assertion ${asrtId}!`; + const [assertionData, seg] = assertion; + const id = `${asrtId}`; + const [nexts, result]: [[Id, Aux][], boolean | undefined] = (() => { + if (seg[0] !== 'MatchResult') return [[[prepNext(seg), id]], undefined]; + if (seg[2][0] === 'Success') return [[], true]; + return [[], false]; + })(); + + const expanded = expandedNodes.has(asrtId); + + const [submap, hasSubmap] = ((): [[Id, Aux] | undefined, boolean] => { + const fold = assertionData.fold; + // No fold + if (fold === null) return [undefined, false]; + + const foldId = fold[0]; + + // Fold matching hasn't been requested yet + if (!(foldId in matches)) { + requestMatching(foldId); + return [undefined, true]; + } + if (!expanded) return [undefined, true]; + + return [[['Root', foldId], undefined], true]; + })(); + + const toggleExpanded = hasSubmap + ? () => { + toggleNodeExpanded(asrtId); + } + : undefined; + + return { + id, + submap, + parent, + nexts, + edgeLabel: undefined, + ...DEFAULT_NODE_SIZE, + data: { + type: 'Assertion', + assertionData, + isSelected: asrtId === selectedId, + setSelected: () => { + selectStep(['Assertion', assertionData]); + }, + expanded, + toggleExpanded, + result, + }, + }; + }; + + const getNode = (nodeId: Id, aux: Aux): PreNode => { + if (nodeId[0] === 'Root') return getRoot(nodeId[1]); + if (nodeId[0] === 'Result') return getResult(nodeId[1], aux); + // nodeId[0] === 'Assertion') + return getAssertion(nodeId[1], aux); + }; + + return ( + + ); +}; + +export default MatchMapView; diff --git a/debugger-vscode-extension/src/webviews/src/MatchView/MatchView.tsx b/debug-ui/src/webviews/src/MatchView/MatchView.tsx similarity index 93% rename from debugger-vscode-extension/src/webviews/src/MatchView/MatchView.tsx rename to debug-ui/src/webviews/src/MatchView/MatchView.tsx index b24ce253d..86eb121be 100644 --- a/debugger-vscode-extension/src/webviews/src/MatchView/MatchView.tsx +++ b/debug-ui/src/webviews/src/MatchView/MatchView.tsx @@ -30,8 +30,7 @@ const MatchView = () => { const matchMapView = (() => { const matchId = path[0]; - const matching = matches[matchId]; - if (matching === undefined) { + if (!(matchId in matches)) { const load = () => { requestMatching(matchId); }; @@ -41,7 +40,7 @@ const MatchView = () => { return ( = { + id: string; + submap: [Id, Aux] | undefined; + parent: string | undefined; + nexts: [Id, Aux][]; + edgeLabel: string | undefined; + width: number; + height: number; + data: D; +}; + +type Props = { + getNode: (id: Id, aux: Aux) => PreNode; + rootId: Id; + rootAux: Aux; + nodeComponent: React.ComponentType>; +}; + +type StackElem = { + node: PreNode; + x: number; + y: number; +}; + +export type NodeData = { + width: number; + height: number; + maxX: number; + maxChildX: number; + maxChildY: number; + submap: string | undefined; + nexts: string[]; +}; + +export type FlowRef = React.MutableRefObject | undefined; +export const FlowRefContext = React.createContext(undefined as FlowRef); + +const TreeMapView = ({ + getNode: getNodeRaw, + rootId, + rootAux, + nodeComponent, +}: Props) => { + const reactFlowInstance = useReactFlow(); + const flowRef: FlowRef = useRef(undefined as unknown as HTMLDivElement); + + useEffect(() => { + events.subscribe('resetView', () => { + reactFlowInstance.setViewport({ x: 0, y: 0, zoom: 1 }); + }); + + return () => { + events.unsubscribe('resetView'); + }; + }, [reactFlowInstance]); + + const preNodeCache = new Map>(); + const getNode = (id: Id, aux: Aux) => { + if (preNodeCache.has(id)) return preNodeCache.get(id)!; + const node = getNodeRaw(id, aux); + preNodeCache.set(id, node); + return node; + }; + const root = getNode(rootId, rootAux); + + // First pass: initial elem placement, edges + const nodes: Record> = {}; + const edges: Edge[] = []; + const init = { node: root, x: 50, y: 50 }; + const preNodeStack: StackElem[] = [init]; + for (let i = init; i != undefined; i = preNodeStack[0]) { + // Function block here so we can 'continue' the outer loop by returning + (() => { + const { node, x, y } = i; + let width = node.width; + let height = node.height; + + // Handle submaps + let submapId: string | undefined = undefined; + if (node.submap !== undefined) { + const submap = getNode(...node.submap); + const submapNode = nodes[submap.id]; + if (submapNode) { + submapId = submapNode.id; + // Adjust size for submap + const subWidth = submapNode.data.maxX + NODE_PAD - x; + const subHeight = submapNode.data.maxChildY + NODE_PAD - y; + width = Math.max(width, subWidth); + height = Math.max(height, subHeight); + } else { + // Do submap first + preNodeStack.unshift({ + node: submap, + x: x + NODE_PAD, + y: y + NODE_HEIGHT + NODE_PAD, + }); + return; + } + } + + // Handle nexts + let maxChildX = x - NODE_GAP_X; + let maxChildY = y + height; + const nexts: string[] = []; + for (const [nextId, nextAux] of node.nexts) { + const next = getNode(nextId, nextAux); + const nextNode = nodes[next.id]; + if (nextNode) { + nexts.push(nextNode.id); + // Shift offset for next node + maxChildX = nextNode.data.maxX; + maxChildY = Math.max(maxChildY, nextNode.data.maxChildY); + } else { + // Do child first + preNodeStack.unshift({ + node: next, + x: maxChildX + NODE_GAP_X, + y: y + height + NODE_GAP_Y, + }); + return; + } + } + const maxX = Math.max(maxChildX, x + width); + + nodes[node.id] = { + id: `${node.id}`, + position: { x, y }, + type: 'customNode', + data: { + width, + height, + maxX, + maxChildX, + maxChildY, + nexts, + submap: submapId, + ...node.data, + }, + style: { + width: `${width}px`, + height: `${height}px`, + display: 'flex', + justifyContent: 'center', + }, + draggable: false, + connectable: false, + selectable: true, + }; + + // Add edge + if (node.parent !== undefined) { + edges.push({ + id: `${node.parent}-${node.id}`, + source: node.parent, + target: node.id, + ...(node.edgeLabel ? { label: node.edgeLabel } : {}), + }); + } + + preNodeStack.shift(); + })(); + } + + // Second pass: center nodes + const centerStack: [string, number][] = []; + for ( + let i: [string, number] | undefined = [root.id, 0]; + i !== undefined; + i = centerStack.shift() + ) { + const [id, parentOffset] = i; + const node = nodes[id]!; + const thisOffset = + parentOffset + (node.data.maxX - node.position.x - node.data.width) / 2; + const x = thisOffset + node.position.x; + node.position = { ...node.position, x }; + if (node.data.submap) { + const submapNode = nodes[node.data.submap]!; + const submapOffset = + thisOffset + + Math.max( + (node.position.x + + node.data.width - + NODE_PAD - + submapNode.data.maxX) / + 2, + 0 + ); + centerStack.unshift([node.data.submap, submapOffset]); + } + const nextOffset = + parentOffset + Math.max((node.data.maxX - node.data.maxChildX) / 2, 0); + for (const next of node.data.nexts) centerStack.unshift([next, nextOffset]); + } + + const nodeTypes = { customNode: nodeComponent }; + + return ( +
+ + + + + + +
+ ); +}; + +const TreeMapViewWrap = (props: Props) => ( + + + +); + +export default TreeMapViewWrap; diff --git a/debugger-vscode-extension/src/webviews/src/TreeMapView/TreeMapView.tsx b/debug-ui/src/webviews/src/TreeMapView/TreeMapViewOld.tsx similarity index 100% rename from debugger-vscode-extension/src/webviews/src/TreeMapView/TreeMapView.tsx rename to debug-ui/src/webviews/src/TreeMapView/TreeMapViewOld.tsx diff --git a/debugger-vscode-extension/src/webviews/src/VSCodeAPI.ts b/debug-ui/src/webviews/src/VSCodeAPI.ts similarity index 98% rename from debugger-vscode-extension/src/webviews/src/VSCodeAPI.ts rename to debug-ui/src/webviews/src/VSCodeAPI.ts index 7e24a21be..02d8fc3c9 100644 --- a/debugger-vscode-extension/src/webviews/src/VSCodeAPI.ts +++ b/debug-ui/src/webviews/src/VSCodeAPI.ts @@ -33,7 +33,7 @@ class VSCodeWrapper { } } -export const execSpecific = (prevId: number, branchCase: BranchCase) => { +export const execSpecific = (prevId: number, branchCase: BranchCase | null) => { VSCodeAPI.postMessage({ type: 'request_exec_specific', prevId, diff --git a/debugger-vscode-extension/src/webviews/src/events.ts b/debug-ui/src/webviews/src/events.ts similarity index 100% rename from debugger-vscode-extension/src/webviews/src/events.ts rename to debug-ui/src/webviews/src/events.ts diff --git a/debugger-vscode-extension/src/webviews/src/index.tsx b/debug-ui/src/webviews/src/index.tsx similarity index 100% rename from debugger-vscode-extension/src/webviews/src/index.tsx rename to debug-ui/src/webviews/src/index.tsx diff --git a/debugger-vscode-extension/src/webviews/src/store.tsx b/debug-ui/src/webviews/src/store.tsx similarity index 100% rename from debugger-vscode-extension/src/webviews/src/store.tsx rename to debug-ui/src/webviews/src/store.tsx diff --git a/debugger-vscode-extension/src/webviews/src/style.css b/debug-ui/src/webviews/src/style.css similarity index 100% rename from debugger-vscode-extension/src/webviews/src/style.css rename to debug-ui/src/webviews/src/style.css diff --git a/debugger-vscode-extension/src/webviews/src/util.tsx b/debug-ui/src/webviews/src/util.tsx similarity index 100% rename from debugger-vscode-extension/src/webviews/src/util.tsx rename to debug-ui/src/webviews/src/util.tsx diff --git a/debugger-vscode-extension/src/webviews/src/util/Hero.tsx b/debug-ui/src/webviews/src/util/Hero.tsx similarity index 100% rename from debugger-vscode-extension/src/webviews/src/util/Hero.tsx rename to debug-ui/src/webviews/src/util/Hero.tsx diff --git a/debugger-vscode-extension/src/webviews/src/util/Loading.tsx b/debug-ui/src/webviews/src/util/Loading.tsx similarity index 100% rename from debugger-vscode-extension/src/webviews/src/util/Loading.tsx rename to debug-ui/src/webviews/src/util/Loading.tsx diff --git a/debugger-vscode-extension/src/webviews/src/vscode.css b/debug-ui/src/webviews/src/vscode.css similarity index 100% rename from debugger-vscode-extension/src/webviews/src/vscode.css rename to debug-ui/src/webviews/src/vscode.css diff --git a/debugger-vscode-extension/src/webviews/types/static.d.ts b/debug-ui/src/webviews/types/static.d.ts similarity index 100% rename from debugger-vscode-extension/src/webviews/types/static.d.ts rename to debug-ui/src/webviews/types/static.d.ts diff --git a/debugger-vscode-extension/tailwind.config.js b/debug-ui/tailwind.config.js similarity index 100% rename from debugger-vscode-extension/tailwind.config.js rename to debug-ui/tailwind.config.js diff --git a/debugger-vscode-extension/tsconfig-webview.json b/debug-ui/tsconfig-webview.json similarity index 100% rename from debugger-vscode-extension/tsconfig-webview.json rename to debug-ui/tsconfig-webview.json diff --git a/debugger-vscode-extension/tsconfig.json b/debug-ui/tsconfig.json similarity index 100% rename from debugger-vscode-extension/tsconfig.json rename to debug-ui/tsconfig.json diff --git a/debugger-vscode-extension/webpack.config.js b/debug-ui/webpack.config.js similarity index 100% rename from debugger-vscode-extension/webpack.config.js rename to debug-ui/webpack.config.js diff --git a/debugger-vscode-extension/yarn.lock b/debug-ui/yarn.lock similarity index 100% rename from debugger-vscode-extension/yarn.lock rename to debug-ui/yarn.lock diff --git a/debugger-vscode-extension/src/webviews/src/ExecMap/ExecMapView.tsx b/debugger-vscode-extension/src/webviews/src/ExecMap/ExecMapView.tsx deleted file mode 100644 index 7c15cca53..000000000 --- a/debugger-vscode-extension/src/webviews/src/ExecMap/ExecMapView.tsx +++ /dev/null @@ -1,173 +0,0 @@ -import React from 'react'; -import { BranchCase, DebuggerState, ExecMap } from '../../../types'; -import TreeMapView, { - TransformResult, - TransformFunc, -} from '../TreeMapView/TreeMapView'; -import { execSpecific, jumpToId, startProc } from '../VSCodeAPI'; -import ExecMapNode, { ExecMapNodeData } from './ExecMapNode'; -import { NODE_HEIGHT, DEFAULT_NODE_SIZE } from '../TreeMapView/TreeMapView'; - -export type Props = { - state: DebuggerState; - expandedNodes: Set; - toggleNodeExpanded: (id: string) => void; -}; - -type M = ExecMap; -type D = ExecMapNodeData; -type A = { - procName: string; - branchCase?: BranchCase | null; - hasParent?: boolean; -}; - -const ExecMapView = ({ state, expandedNodes, toggleNodeExpanded }: Props) => { - const { mainProc: mainProcName, currentProc: currentProcName, procs } = state; - const mainProc = procs[mainProcName]; - const { execMap, liftedExecMap } = mainProc; - const usedExecMap = liftedExecMap ?? execMap; - - const initElem: TransformResult = { - id: 'root', - data: { - type: 'Root', - procName: mainProcName, - isActive: currentProcName === mainProcName, - }, - nexts: [[{ procName: mainProcName }, usedExecMap]], - ...DEFAULT_NODE_SIZE, - }; - - const cleanNexts = ( - nexts: [BranchCase | null, [null, M]][], - aux: A - ): [A, M][] => { - return nexts.map(next => { - return [{ ...aux, branchCase: next[0] }, next[1][1]]; - }); - }; - - let emptyCount = 0; - const transform: TransformFunc = (map, parent, aux) => { - const { procName, branchCase = null, hasParent = true } = aux; - const procState = procs[procName]; - const edgeLabel = - branchCase && branchCase[0] ? <>{branchCase[0]} : undefined; - const isActive = procName === currentProcName; - - if (map[0] == 'Nothing') { - if (parent === undefined) { - throw '`Nothing` node has no parent!'; - } - return { - id: `empty${emptyCount++}`, - data: { - type: 'Empty', - hasParent: true, - isActive, - exec: () => { - execSpecific(+parent, branchCase as BranchCase); - }, - }, - nexts: [], - edgeLabel, - width: NODE_HEIGHT, - height: NODE_HEIGHT, - }; - } - - const [, { data: cmdData }] = map; - const nexts = (() => { - if (map[0] === 'Cmd') { - return [[{ procName }, map[1].next] as [A, ExecMap]]; - } else if (map[0] === 'BranchCmd') { - return cleanNexts(map[1].nexts, { procName }); - } else { - return []; - } - })(); - - const id = `${cmdData.id}`; - const expanded = expandedNodes.has(id); - - let hasSubmap = false; - const submap = (() => { - if (cmdData.submap[0] === 'NoSubmap') return undefined; - - hasSubmap = true; - - if (!expanded) return undefined; - - if (cmdData.submap[0] === 'Submap') { - return transform(cmdData.submap[1], undefined, { - procName, - hasParent: false, - }); - } else if (cmdData.submap[0] === 'Proc') { - const submapProcName = cmdData.submap[1]; - const proc = procs[submapProcName]; - if (proc === undefined) { - const result: TransformResult = { - id: `empty-${submapProcName}`, - data: { - type: 'Empty', - hasParent: false, - isActive: false, - exec: () => { - startProc(submapProcName); - }, - }, - nexts: [], - edgeLabel: undefined, - width: NODE_HEIGHT, - height: NODE_HEIGHT, - }; - return result; - } else { - return transform(proc.liftedExecMap || proc.execMap, undefined, { - procName: submapProcName, - hasParent: false, - }); - } - } - })(); - - const toggleExpanded = hasSubmap - ? () => { - toggleNodeExpanded(id); - } - : undefined; - - const isCurrentCmd = - procName === currentProcName && - cmdData.all_ids.includes(procState.currentCmdId); - - return { - id, - data: { - type: 'Cmd', - cmdData, - isCurrentCmd, - isFinal: map[0] === 'FinalCmd', - hasParent, - isActive, - jump: () => { - jumpToId(cmdData.id); - }, - expanded, - toggleExpanded, - }, - nexts, - edgeLabel, - ...DEFAULT_NODE_SIZE, - submap, - }; - }; - - return ( - - ); -}; - -export default ExecMapView; diff --git a/debugger-vscode-extension/src/webviews/src/MatchView/MatchMapView.tsx b/debugger-vscode-extension/src/webviews/src/MatchView/MatchMapView.tsx deleted file mode 100644 index 0a9a3c7bf..000000000 --- a/debugger-vscode-extension/src/webviews/src/MatchView/MatchMapView.tsx +++ /dev/null @@ -1,161 +0,0 @@ -import React from 'react'; -import { - MatchingState, - MatchMap, - MatchMapInner, - MatchSeg, - MatchStep, -} from '../../../types'; -import TreeMapView, { - TransformFunc, - TransformResult, - DEFAULT_NODE_SIZE, -} from '../TreeMapView/TreeMapView'; -import MatchMapNode, { MatchMapNodeData } from './MatchMapNode'; - -import 'allotment/dist/style.css'; -import { getMatchName } from '../util'; -import useStore from '../store'; - -type Props = { - matching: MatchingState; - selectStep: (step: MatchStep) => void; - matches: Record; - expandedNodes: Set; - requestMatching: (id: number) => void; - toggleNodeExpanded: (id: number) => void; -}; - -type M = MatchSeg; -type D = MatchMapNodeData; -type A = null; - -const MatchMapView = ({ - matching, - selectStep, - expandedNodes, - matches, - requestMatching, - toggleNodeExpanded, -}: Props) => { - const matchMap = (matching.map as MatchMap)[1]; - const selectedId = (() => { - if (!matching.selected) { - return -1; - } - - if (matching.selected[0] === 'Assertion') { - return matching.selected[1].id; - } else if (matching.selected[0] === 'Result') { - return matching.selected[1]; - } - })(); - - const [title, subtitle] = useStore(state => getMatchName(state)); - const buildInitElem = ( - id: number, - title: React.ReactNode, - subtitle: React.ReactNode = <>, - map: MatchMapInner - ): TransformResult => ({ - id: `root-${id}`, - data: { - type: 'Root', - title, - subtitle, - }, - nexts: (() => { - if (map[0] === 'Direct') { - return [[null, map[1]]]; - } else { - return map[1].map(seg => [null, seg]); - } - })(), - ...DEFAULT_NODE_SIZE, - }); - - const initElem = buildInitElem(matching.id, title, subtitle, matchMap); - - const transform: TransformFunc = map => { - if (map[0] === 'MatchResult') { - const [, id, result] = map; - return { - id: `${id}`, - data: { - type: 'Result', - result, - setSelected: () => { - selectStep(['Result', id, result]); - }, - }, - nexts: [], - ...DEFAULT_NODE_SIZE, - }; - } - - const [, assertionData, next] = map; - const isSelected = assertionData.id === selectedId; - const { id, fold } = assertionData; - - const expanded = expandedNodes.has(id); - const [submap, hasSubmap] = (() => { - // No fold - if (fold === null) return [undefined, false]; - - const foldId = fold[0]; - - // Fold matching hasn't been requested yet - if (!(foldId in matches)) { - requestMatching(foldId); - return [undefined, true]; - } - - const matching = matches[foldId]; - - // Fold matching is loading or hidden - if (matching === undefined || !expanded) return [undefined, true]; - - const map = matching.map as MatchMap; - - const initElem = buildInitElem(foldId, Fold, undefined, map[1]); - return [initElem, true]; - })(); - - const toggleExpanded = hasSubmap - ? () => { - toggleNodeExpanded(id); - } - : undefined; - - const [nexts, result]: [[null, MatchSeg][], boolean | undefined] = (() => { - if (next[0] !== 'MatchResult') return [[[null, next]], undefined]; - if (next[2][0] === 'Success') return [[], true]; - return [[], false]; - })(); - return { - id: `${id}`, - data: { - type: 'Assertion', - assertionData, - isSelected, - setSelected: () => { - selectStep(['Assertion', assertionData]); - }, - expanded, - toggleExpanded, - result, - }, - nexts, - submap, - ...DEFAULT_NODE_SIZE, - }; - }; - - return ( - - ); -}; - -export default MatchMapView; diff --git a/debugger-vscode-extension/src/webviews/src/MatchView/UnifyData.tsx b/debugger-vscode-extension/src/webviews/src/MatchView/UnifyData.tsx deleted file mode 100644 index d479816d8..000000000 --- a/debugger-vscode-extension/src/webviews/src/MatchView/UnifyData.tsx +++ /dev/null @@ -1,211 +0,0 @@ -import { - VSCodeButton, - VSCodeDataGrid, - VSCodeDataGridCell, - VSCodeDataGridRow, - VSCodeDivider, - VSCodeLink, -} from '@vscode/webview-ui-toolkit/react'; -import React, { useEffect, useMemo } from 'react'; -import { MatchMap, MatchSeg, MatchStep } from '../../../types'; -import useStore, { mutateStore } from '../store'; -import { Code, getMatchName, showBaseMatchKind } from '../util'; -import { requestMatching } from '../VSCodeAPI'; - -import './MatchData.css'; - -type Props = { - selectStep: (step: MatchStep) => void; -}; - -const extractTargets = (seg: MatchSeg): { [key: number]: MatchStep } => { - if (seg[0] === 'MatchResult') { - const [, id, result] = seg; - return { [id]: ['Result', id, result] }; - } - - const [, asrt, next] = seg; - return { [asrt.id]: ['Assertion', asrt], ...extractTargets(next) }; -}; - -const MatchData = ({ selectStep }: Props) => { - const mainProcName = useStore(store => store.debuggerState?.mainProc || ''); - const [{ path, matches }, baseMatchKind] = useStore(store => [ - store.matchState, - showBaseMatchKind(store), - ]); - const { pushMatching, popMatchings } = mutateStore(); - const [title, subtitle] = useStore(state => getMatchName(state)); - - useEffect(() => { - console.log('Showing match data', path, matches); - }, [path, matches]); - const matching = matches[path[0]]; - const selectedStep = matching?.selected; - - const matchJumpTargets = useMemo(() => { - if (matching?.map === undefined) return {}; - const matchMap = matching?.map as MatchMap; - if (matchMap[1][0] === 'Direct') { - return extractTargets(matchMap[1][1]); - } else { - return matchMap[1][1].reduce( - (acc, seg) => ({ ...acc, ...extractTargets(seg) }), - {} - ); - } - }, [matching]); - - const matchNames = [ - <> - - {title} ({subtitle}) - - , - ]; - for (let i = path.length - 1; i > 0; i--) { - const matchId = path[i]; - const matching = matches[matchId]; - if ( - !matching || - !matching.selected || - matching.selected[0] !== 'Assertion' - ) { - console.error('MatchData: malformed state', { - path, - matchId, - matching, - }); - continue; - } - const { assertion } = matching.selected[1]; - - matchNames.push({assertion}); - } - const matchLinks = matchNames.map((name, i) => { - let link = - i > path.length - 2 ? ( - name - ) : ( - { - popMatchings(path.length - i - 1); - }} - > - {name} - - ); - if (i > 0) { - link = ( - <> -
- {link} - - ); - } - return ( -
- {link} -
- ); - }); - - let stepInFoldButton = <>; - let asrt = <>; - let subst = <>; - if (selectedStep !== undefined && selectedStep[0] === 'Assertion') { - const { assertion, fold, substitutions } = selectedStep[1]; - - asrt = ( -

- {assertion} -

- ); - - if (fold !== null) { - const foldId = fold[0]; - const stepInFold = () => { - const isInStore = pushMatching(foldId); - if (!isInStore) { - requestMatching(foldId); - } - }; - stepInFoldButton = ( - Step into fold - ); - } - - if (substitutions.length === 0) { - subst = No substitutions; - } else { - subst = ( - <> -

Substitutions

- - - - Expr - - - Value - - - - {substitutions.map(({ assertId, subst: [expr, val] }) => { - const target = matchJumpTargets[assertId]; - const jumpButtonIcon = - target === undefined ? 'question' : 'target'; - const jumpButton = ( - { - selectStep(target); - }} - > - - - ); - return ( - - - - {expr} - - - - {val} - - - {jumpButton} - - - ); - })} - - - ); - } - } - - return ( -
-
-

{matchLinks}

- {stepInFoldButton} - - - - {asrt} - {subst} -
-
- ); -}; - -export default MatchData; diff --git a/esy.odoc-test.json b/esy.odoc-test.json new file mode 100644 index 000000000..8842cdd58 --- /dev/null +++ b/esy.odoc-test.json @@ -0,0 +1,119 @@ +{ + "name": "gillian-platform", + "version": "0.0.0", + "private": true, + "description": "Gillian Core and maintained instantiations", + "author": { + "name": "Verified Trustworthy Software Specification Group at Imperial College", + "url": "https://vtss.doc.ic.ac.uk" + }, + "homepage": "GillianDev.github.io", + "license": "BSD-3-Clause", + "esy": { + "build": "dune build @install --promote-install-files", + "install": [ + "esy-installer gillian.install", + "esy-installer gillian-js.install", + "esy-installer gillian-c.install", + "esy-installer wisl.install", + "esy-installer kanillian.install" + ], + "release": { + "bin": [ + "kanillian", + "gillian-js", + "gillian-c", + "wisl" + ], + "includePackages": [ + "root", + "@opam/z3", + "compcert" + ] + }, + "buildsInSource": "_build", + "exportedEnv": { + "GILLIAN_JS_RUNTIME_PATH": { + "scope": "global", + "val": "#{self.share}/gillian-js" + }, + "WISL_RUNTIME_PATH": { + "val": "#{self.share}/wisl", + "scope": "global" + }, + "GILLIAN_C_RUNTIME_PATH": { + "scope": "global", + "val": "#{self.share}/gillian-c" + }, + "KANILLIAN_RUNTIME_PATH": { + "scope": "global", + "val": "#{self.share}/kanillian" + }, + "CPATH": { + "scope": "global", + "val": "#{self.share / 'include' : $CPATH}" + } + } + }, + "scripts": { + "format-check": "dune build @fmt", + "format": "dune build @fmt --auto-promote", + "js:init:env": "Gillian-JS/scripts/setup_environment.sh", + "c:init:env": "Gillian-C/scripts/setup_environment.sh", + "wisl:init:env": "wisl/scripts/setup_environment.sh", + "init:env": "sh -c \"esy js:init:env && esy c:init:env && esy wisl:init:env\"", + "test": "dune test", + "install-githooks": "./githooks/install.ml", + "clean-githooks": "./githooks/clean.ml", + "clean": "dune clean", + "watch": "dune build @install --promote-install-files --watch", + "odoc": "sh -c \"esy x dune build @doc && ./scripts/sync_odoc.sh > /dev/null\"", + "odoc:watch:build": "dune build @doc --watch", + "odoc:watch:sync": "sh -c \"./scripts/watch_odoc.sh > /dev/null\"", + "odoc:watch": "concurrently -n odoc,sync -c cyan,blue \"esy odoc:watch:build\" \"esy odoc:watch:sync\"", + "sphinx": "sphinx-build sphinx _docs/sphinx/", + "sphinx:watch": "sphinx-autobuild sphinx _docs/sphinx/", + "docs": "./scripts/build_docs.sh", + "docs:watch": "concurrently -n odoc,odoc-sync,sphinx -c cyan,blue,yellow \"esy odoc:watch:build\" \"esy odoc:watch:sync\" \"esy sphinx:watch\"" + }, + "dependencies": { + "@opam/fpath": "*", + "@opam/alcotest": "1.0.1", + "@opam/cmdliner": "^1.1.1", + "@opam/dap": "1.0.6", + "@opam/dune": "^3.0", + "@opam/fmt": "^0.8.8", + "@opam/flow_parser": "GillianPlatform/flow:flow_parser.opam#dfa43df0b8776f22e5fb2629a22d69a6d302e241", + "@opam/memtrace": "0.2.3", + "@opam/menhir": "20231231", + "@opam/ppx_deriving_yojson": "*", + "@opam/ppxlib": ">=0.18.0", + "@opam/printbox-text": "^0.6.1", + "@opam/sqlite3": "5.0.2", + "@opam/visitors": ">=2.3", + "@opam/yojson": "^1.7.0", + "@opam/zarith": ">=1.12", + "@opam/z3": "GillianPlatform/esy-z3#e8b2ce266d5d8bd67c54bd226c6301f7b180bb09", + "compcert": "GillianPlatform/CompCert#c20a63da768c2c59e114e074ae63cb60610d714b", + "ocaml": "5.1.x" + }, + "devDependencies": { + "ocaml": "5.1.x", + "@opam/cmitomli": "*", + "@opam/fileutils": "*", + "@opam/utop": "*", + "@opam/ocaml-lsp-server": "^1.17.0", + "@opam/odoc": "*", + "@opam/odoc-parser": "*", + "@opam/ocamlformat": "0.26.1", + "@opam/ocamlfind": "*", + "@opam/feather": "*", + "concurrently": "^7.6.0" + }, + "resolutions": { + "@opam/conf-sqlite3": "ManasJayanth/esy-sqlite:esy.json#28dfc73a8eda790213a8359ad708231069ed7079", + "@opam/odoc": "link:../odoc/odoc.opam", + "@opam/odoc-parser": "link:../odoc/odoc-parser.opam", + "esy-gmp": "GillianPlatform/esy-gmp:package.json#d68dce1a9aacc0534cca93d84d2b7f9c8105ee87" + } +} \ No newline at end of file diff --git a/kanillian/lib/lifter/kani_c_lifter.ml b/kanillian/lib/lifter/kani_c_lifter.ml index f80705fde..878a564e8 100644 --- a/kanillian/lib/lifter/kani_c_lifter.ml +++ b/kanillian/lib/lifter/kani_c_lifter.ml @@ -14,7 +14,7 @@ module Annot = Kanillian_compiler.K_annot open Annot open Branch_case -type rid = Gillian.Logging.Report_id.t [@@deriving yojson, show] +type id = Gillian.Logging.Report_id.t [@@deriving yojson, show] let rec int_to_letters = function | 0 -> "" @@ -44,50 +44,53 @@ struct module Gil_lifter = Gil.Lifter - type branch_data = rid * Gil_branch_case.t option [@@deriving yojson] + type branch_data = id * Gil_branch_case.t option [@@deriving yojson] type exec_data = cmd_report executed_cmd_data [@@deriving yojson] - type stack_direction = In | Out of rid [@@deriving yojson] - type step_args = rid option * Gil_branch_case.t option * Gil_branch_case.path + type stack_direction = In | Out of id [@@deriving yojson] + type step_args = id option * Gil_branch_case.t option * Gil_branch_case.path type _ Effect.t += Step : step_args -> exec_data Effect.t - type map = (Branch_case.t, cmd_data, branch_data) Exec_map.t - - and cmd_data = { - id : rid; - all_ids : rid list; + type cmd_data = { + id : id; + all_ids : id list; display : string; matches : matching list; errors : string list; - mutable submap : map submap; - prev : (rid * Branch_case.t option) option; - callers : rid list; + mutable submap : id submap; + prev : (id * Branch_case.t option) option; + callers : id list; func_return_label : (string * int) option; } [@@deriving yojson] + type map = (id, Branch_case.t, cmd_data, branch_data) Exec_map.map + [@@deriving yojson] + module Partial_cmds = struct let ( let++ ) f o = Result.map o f let ( let** ) o f = Result.bind o f type canonical_cmd_data = { - id : rid; + id : id; display : string; - callers : rid list; + callers : id list; stack_direction : stack_direction option; nest_kind : nest_kind option; } [@@deriving to_yojson] + type partial_end = Branch_case.case * (id * Gil_branch_case.t option) + [@@deriving to_yojson] + type partial_data = { - prev : (rid * Branch_case.t option * rid list) option; + prev : (id * Branch_case.t option * id list) option; (** Where to put the finished cmd in the map. *) - all_ids : (rid * (Branch_case.kind option * Branch_case.case)) Ext_list.t; + all_ids : (id * (Branch_case.kind option * Branch_case.case)) Ext_list.t; (** All the GIL cmd IDs that build into this one (and the relevant branch case info). *) - unexplored_paths : (rid * Gil_branch_case.t option) Stack.t; + unexplored_paths : (id * Gil_branch_case.t option) Stack.t; (** All the paths that haven't been explored yet; a stack means depth-first exploration. *) - ends : (Branch_case.case * (rid * Gil_branch_case.t option)) Ext_list.t; + ends : partial_end Ext_list.t; (** All the end points; there may be multiple if the cmd branches. *) - (* TODO: rename to matches *) matches : matching Ext_list.t; (** Unifications contained in this command *) errors : string Ext_list.t; (** Errors occurring during this command *) @@ -96,24 +99,24 @@ struct } [@@deriving to_yojson] - type t = (rid, partial_data) Hashtbl.t [@@deriving to_yojson] + type t = (id, partial_data) Hashtbl.t [@@deriving to_yojson] type finished = { - prev : (rid * Branch_case.t option) option; - id : rid; - all_ids : rid list; + prev : (id * Branch_case.t option) option; + id : id; + all_ids : id list; display : string; matches : Exec_map.matching list; errors : string list; - kind : (Branch_case.t, branch_data) cmd_kind; - callers : rid list; + next_kind : (Branch_case.t, branch_data) next_kind; + callers : id list; stack_direction : stack_direction option; } [@@deriving yojson] type partial_result = | Finished of finished - | StepAgain of (rid * Gil_branch_case.t option) + | StepAgain of (id * Gil_branch_case.t option) [@@deriving yojson] let ends_to_cases @@ -180,12 +183,13 @@ struct let matches = Ext_list.to_list matches in let errors = Ext_list.to_list errors in let ends = Ext_list.to_list ends in - let++ kind = + let++ next_kind = let++ cases = ends_to_cases ~is_unevaluated_funcall ~nest_kind ends in match cases with - | [] -> Final - | [ (Case (Unknown, _), _) ] -> Normal - | _ -> Branch cases + | [] -> Zero + | [ (Case (Unknown, _), _) ] -> + One (Option.get (List_utils.last all_ids), None) + | _ -> Many cases in Finished { @@ -195,7 +199,7 @@ struct display; matches; errors; - kind; + next_kind; callers; stack_direction; } @@ -247,22 +251,22 @@ struct ~annot ~branch_kind partial = - let ({ id; kind; _ } : exec_data) = exec_data in + let ({ id; next_kind; _ } : exec_data) = exec_data in let { ends; unexplored_paths; _ } = partial in - match (annot.cmd_kind, kind, is_end) with - | Return, _, _ | _, Final, _ -> Ok () - | _, Normal, false -> + match (annot.cmd_kind, next_kind, is_end) with + | Return, _, _ | _, Zero, _ -> Ok () + | _, One (), false -> Stack.push (id, None) unexplored_paths; Ok () - | _, Branch cases, false -> + | _, Many cases, false -> cases |> List.iter (fun (gil_case, ()) -> Stack.push (id, Some gil_case) unexplored_paths); Ok () - | _, Normal, true -> + | _, One (), true -> Ext_list.add (branch_case, (id, None)) ends; Ok () - | _, Branch cases, true -> + | _, Many cases, true -> cases |> List_utils.iter_results (fun (gil_case, ()) -> let++ case = @@ -468,9 +472,8 @@ struct tl_ast : tl_ast; [@to_yojson fun _ -> `Null] prog : (annot, int) Prog.t; [@to_yojson fun _ -> `Null] partial_cmds : Partial_cmds.t; - mutable map : map; - id_map : (rid, map) Hashtbl.t; - func_return_map : (rid, string * int ref) Hashtbl.t; + map : map; + func_return_map : (id, string * int ref) Hashtbl.t; mutable func_return_count : int; } [@@deriving to_yojson] @@ -494,24 +497,34 @@ struct (label, count) let update_caller_branches ~caller_id ~cont_id (label, ix) state = - match Hashtbl.find_opt state.id_map caller_id with + let result = + map_node_extra state.map caller_id (fun node -> + let new_next = + match node.next with + | Some (Branch nexts) -> + let nexts = List.remove_assoc Func_exit_placeholder nexts in + let case = Case (Func_exit label, ix) in + let bdata = (cont_id, None) in + let nexts = nexts @ [ (case, (None, bdata)) ] in + Ok (Some (Branch nexts)) + | None | Some (Single _) -> + Fmt.error "update_caller_branches - caller %a does not branch" + pp_id caller_id + in + match new_next with + | Ok next -> ({ node with next }, Ok ()) + | Error e -> (node, Error e)) + in + match result with + | Some r -> r | None -> - Fmt.error "update_caller_branches - caller %a not found" pp_rid - caller_id - | Some (BranchCmd { nexts; _ }) -> - Hashtbl.remove nexts Func_exit_placeholder; - let case = Case (Func_exit label, ix) in - let bdata = (cont_id, None) in - Hashtbl.add nexts case (bdata, Nothing); - Ok () - | Some _ -> - Fmt.error "update_caller_branches - caller %a does not branch" pp_rid + Fmt.error "update_caller_branches - caller %a not found" pp_id caller_id let resolve_func_branches ~state finished_partial = - let Partial_cmds.{ all_ids; kind; callers; _ } = finished_partial in - match (kind, callers) with - | Final, caller_id :: _ -> + let Partial_cmds.{ all_ids; next_kind; callers; _ } = finished_partial in + match (next_kind, callers) with + | Zero, caller_id :: _ -> let label, count = match Hashtbl.find_opt state.func_return_map caller_id with | Some (label, count) -> (label, count) @@ -526,7 +539,17 @@ struct let make_new_cmd ~func_return_label finished_partial = let Partial_cmds. - { all_ids; id; display; matches; errors; prev; kind; callers; _ } = + { + all_ids; + id; + display; + matches; + errors; + prev; + next_kind; + callers; + _; + } = finished_partial in let data = @@ -542,134 +565,149 @@ struct func_return_label; } in - match kind with - | Final -> FinalCmd { data } - | Normal -> Cmd { data; next = Nothing } - | Branch ends -> - let nexts = Hashtbl.create 0 in - List.iter - (fun (case, branch_data) -> - Hashtbl.add nexts case (branch_data, Nothing)) - ends; - BranchCmd { data; nexts } - - let insert_as_next ~state ~prev_id ?case new_cmd = - match (Hashtbl.find state.id_map prev_id, case) with - | Nothing, _ -> Error "trying to insert next of Nothing!" - | FinalCmd _, _ -> Error "trying to insert next of FinalCmd!" - | Cmd _, Some _ -> Error "tying to insert to non-branch cmd with branch!" - | BranchCmd _, None -> - Error "trying to insert to branch cmd with no branch!" - | Cmd c, None -> - c.next <- new_cmd; - Ok () - | BranchCmd { nexts; _ }, Some case -> ( - match Hashtbl.find nexts case with - | branch_data, Nothing -> - Hashtbl.replace nexts case (branch_data, new_cmd); - Ok () - | _ -> Error "duplicate insertion!") - - let insert_as_submap ~state ~parent_id new_cmd = - let** parent_data = - match Hashtbl.find state.id_map parent_id with - | Nothing -> Error "trying to insert submap of Nothing!" - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> Ok data + let next = + match next_kind with + | Zero -> None + | One bdata -> Some (Single (None, bdata)) + | Many ends -> + let nexts = + List.map (fun (case, bdata) -> (case, (None, bdata))) ends + in + Some (Branch nexts) + in + { data; next } + + let with_prev prev { data; next } = + let data = { data with prev } in + { data; next } + + let insert_as_next ~state ~prev_id ?case new_id = + map_node_extra_exn state.map prev_id (fun prev -> + let new_next = + let** next = + match prev.next with + | Some next -> Ok next + | None -> Error "trying to insert next of final cmd!" + in + match (next, case) with + | Single _, Some _ -> + Error "trying to insert to non-branch cmd with branch" + | Branch _, None -> + Error "trying to insert to branch cmd with no branch" + | Single (Some _, _), _ -> Error "duplicate insertion" + | Single (None, bdata), None -> + Ok (Some (Single (Some new_id, bdata))) + | Branch nexts, Some case -> ( + match List.assoc_opt case nexts with + | None -> Error "case not found" + | Some (Some _, _) -> Error "duplicate insertion" + | Some (None, bdata) -> + let nexts = + List_utils.assoc_replace case (Some new_id, bdata) nexts + in + Ok (Some (Branch nexts))) + in + match new_next with + | Ok next -> ({ prev with next }, Ok ()) + | Error e -> + (prev, Fmt.error "insert_as_next (%a) - %s" pp_id prev_id e)) + + let insert_as_submap ~state ~parent_id new_id = + map_node_extra_exn state.map parent_id (fun parent -> + match parent.data.submap with + | Proc _ | Submap _ -> (parent, Error "duplicate submaps!") + | NoSubmap -> + let data = { parent.data with submap = Submap new_id } in + ({ parent with data }, Ok ())) + + let insert_to_empty_map ~state ~prev ~stack_direction new_cmd = + let- () = + match state.map.root with + | Some _ -> Some None + | None -> None + in + let r = + match (stack_direction, prev) with + | Some _, _ -> Error "stepping in our out with empty map!" + | _, Some _ -> Error "inserting to empty map with prev!" + | None, None -> + let new_cmd = new_cmd |> with_prev None in + let () = state.map.root <- Some new_cmd.data.id in + Ok new_cmd in - match parent_data.submap with - | Proc _ | Submap _ -> Error "duplicate submaps!" - | NoSubmap -> - parent_data.submap <- Submap new_cmd; - Ok () + Some r let insert_cmd ~state ~prev ~stack_direction new_cmd = - match (stack_direction, state.map, prev) with - | Some _, Nothing, _ -> Error "stepping in our out with empty map!" - | _, Nothing, Some _ -> Error "inserting to empty map with prev!" - | None, Nothing, None -> - let () = state.map <- new_cmd in - Ok new_cmd - | _, _, None -> Error "inserting to non-empty map with no prev!" - | Some In, _, Some (parent_id, Some Func_exit_placeholder) - | Some In, _, Some (parent_id, None) -> - let new_cmd = new_cmd |> map_data (fun d -> { d with prev = None }) in - let++ () = insert_as_submap ~state ~parent_id new_cmd in + let- () = insert_to_empty_map ~state ~prev ~stack_direction new_cmd in + match (stack_direction, prev) with + | _, None -> Error "inserting to non-empty map with no prev!" + | Some In, Some (parent_id, Some Func_exit_placeholder) + | Some In, Some (parent_id, None) -> + let new_cmd = new_cmd |> with_prev None in + let++ () = insert_as_submap ~state ~parent_id new_cmd.data.id in new_cmd - | Some In, _, Some (_, Some _) -> Error "stepping in with branch case!" - | None, _, Some (prev_id, case) -> - let++ () = insert_as_next ~state ~prev_id ?case new_cmd in + | Some In, Some (_, Some _) -> Error "stepping in with branch case!" + | None, Some (prev_id, case) -> + let++ () = insert_as_next ~state ~prev_id ?case new_cmd.data.id in new_cmd - | Some (Out prev_id), _, Some (inner_prev_id, _) -> + | Some (Out prev_id), Some (inner_prev_id, _) -> let** case = let func_return_label = - match Hashtbl.find state.id_map inner_prev_id with - | Nothing -> None - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> - data.func_return_label + (get_exn state.map inner_prev_id).data.func_return_label in match func_return_label with | Some (label, ix) -> Ok (Case (Func_exit label, ix)) | None -> Error "stepping out without function return label!" in - let new_cmd = - new_cmd - |> map_data (fun d -> { d with prev = Some (prev_id, Some case) }) - in - let++ () = insert_as_next ~state ~prev_id ~case new_cmd in + let new_cmd = new_cmd |> with_prev (Some (prev_id, Some case)) in + let++ () = insert_as_next ~state ~prev_id ~case new_cmd.data.id in new_cmd - let get_return_label_from_prev ~state prev_id = - match Hashtbl.find state.id_map prev_id with - | Nothing -> None - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> - data.func_return_label - let f ~state finished_partial = - (let { id_map; _ } = state in - let Partial_cmds.{ all_ids; prev; stack_direction; _ } = - finished_partial - in - let** new_cmd = - let++ func_return_label = - resolve_func_branches ~state finished_partial - in - make_new_cmd ~func_return_label finished_partial - in - let** new_cmd = insert_cmd ~state ~prev ~stack_direction new_cmd in - all_ids |> List.iter (fun id -> Hashtbl.replace id_map id new_cmd); - Ok new_cmd) - |> Result_utils.or_else (failwith ~state ~finished_partial) + let r = + let Partial_cmds.{ id; all_ids; prev; stack_direction; _ } = + finished_partial + in + let** func_return_label = + resolve_func_branches ~state finished_partial + in + let new_cmd = make_new_cmd ~func_return_label finished_partial in + let** new_cmd = insert_cmd ~state ~prev ~stack_direction new_cmd in + let () = insert state.map ~id ~all_ids new_cmd in + Ok new_cmd + in + Result_utils.or_else (failwith ~state ~finished_partial) r end let insert_new_cmd = Insert_new_cmd.f module Init_or_handle = struct let get_prev ~state ~gil_case ~prev_id () = - let { map; id_map; _ } = state in + let { map; _ } = state in let=* prev_id = Ok prev_id in - let=* map = - match Hashtbl.find_opt id_map prev_id with + let=* prev = + match get map prev_id with | None -> ( - match map with - | Nothing -> - Ok None + match map.root with + | None -> (* It's okay to not have a prev if we're still in the harness *) + Ok None | _ -> Error "couldn't find map at prev_id!") | map -> Ok map in - match map with - | Nothing -> Error "got Nothing map!" - | FinalCmd { data; _ } | Cmd { data; _ } -> - Ok (Some (data.id, None, data.callers)) - | BranchCmd { data; nexts } -> ( + let { id; callers; _ } = prev.data in + match prev.next with + | None | Some (Single _) -> Ok (Some (id, None, callers)) + | Some (Branch nexts) -> ( let case = - Hashtbl.find_map - (fun case ((id, gil_case'), _) -> - if id = prev_id && gil_case' = gil_case then Some case else None) + List.find_map + (fun (case, (_, (prev_id', gil_case'))) -> + if prev_id' = prev_id && gil_case' = gil_case then Some case + else None) nexts in match case with - | Some case -> Ok (Some (data.id, Some case, data.callers)) + | Some case -> Ok (Some (id, Some case, callers)) | None -> Error "couldn't find prev in branches!") let f ~state ?prev_id ?gil_case (exec_data : exec_data) = @@ -709,54 +747,36 @@ struct let package_case case = let json = Branch_case.to_yojson case in let display = Branch_case.display case in - (display, json) - - let package_data package { id; all_ids; display; matches; errors; submap; _ } - = - let submap = - match submap with - | NoSubmap -> NoSubmap - | Proc p -> Proc p - | Submap m -> Submap (package m) - in + (json, display) + + let package_data { id; all_ids; display; matches; errors; submap; _ } = Packaged.{ id; all_ids; display; matches; errors; submap } - let package = - let package_case - ~(bd : branch_data) - ~(all_cases : (Branch_case.t * branch_data) list) - case = - ignore bd; - ignore all_cases; - package_case case + let package_node { data : cmd_data; next } = + let data = package_data data in + let next = + match next with + | None -> None + | Some (Single (next, _)) -> Some (Single (next, "")) + | Some (Branch nexts) -> + let nexts = + nexts + |> List.map (fun (case, (next, _)) -> + let case, bdata = package_case case in + (case, (next, bdata))) + in + Some (Branch nexts) in - Packaged.package package_data package_case + { data; next } + let package = Packaged.package Fun.id package_node let get_lifted_map_exn { map; _ } = package map let get_lifted_map state = Some (get_lifted_map_exn state) - - let get_matches_at_id id { id_map; _ } = - let map = Hashtbl.find id_map id in - match map with - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> - data.matches - | _ -> - failwith "get_matches_at_id: HORROR - tried to get matches at non-cmd!" - - let get_root_id { map; _ } = - match map with - | Nothing -> None - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> - Some data.id - + let get_matches_at_id id { map; _ } = (get_exn map id).data.matches let path_of_id id { gil_state; _ } = Gil_lifter.path_of_id id gil_state - let previous_step id { id_map; _ } = - let+ id, case = - match Hashtbl.find id_map id with - | Nothing -> None - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> data.prev - in + let previous_step id { map; _ } = + let+ id, case = (get_exn map id).data.prev in let case = case |> Option.map package_case in (id, case) @@ -768,14 +788,14 @@ struct let select_case nexts = let result = - Hashtbl.fold - (fun _ (id_case, map) acc -> - match (map, acc) with + List.fold_left + (fun acc (_, (next, id_case)) -> + match (next, acc) with | _, Some (Either.Right _) -> acc - | Nothing, _ -> Some (Either.Right id_case) - | map, None -> Some (Either.Left map) + | None, _ -> Some (Either.Right id_case) + | Some id, None -> Some (Either.Left id) | _ -> acc) - nexts None + None nexts in Option.get result @@ -787,20 +807,19 @@ struct let* label, ix = func_return_label in let case = Case (Func_exit label, ix) in let* _ = - match Hashtbl.find state.id_map caller_id with - | BranchCmd { nexts; _ } -> Hashtbl.find_opt nexts case + match (get_exn state.map caller_id).next with + | Some (Branch nexts) -> List.assoc_opt case nexts | _ -> None in Some (caller_id, Some case) let rec find_next state id case = - let map = Hashtbl.find state.id_map id in - match (map, case) with - | Nothing, _ -> failwith "HORROR - map is Nothing!" - | (FinalCmd _ | Cmd _), Some _ -> + let node = get_exn state.map id in + match (node.next, case) with + | (None | Some (Single _)), Some _ -> failwith "HORROR - tried to step case for non-branch cmd" - | Cmd { next = Nothing; data = { all_ids; _ } }, None -> - let id = List.hd (List.rev all_ids) in + | Some (Single (None, _)), None -> + let id = List.hd (List.rev node.data.all_ids) in let case = match Gil_lifter.cases_at_id id state.gil_state with | [] -> None @@ -811,17 +830,17 @@ struct L.Report_id.pp id in Either.Right (id, case) - | Cmd { next; _ }, None -> Either.Left next - | BranchCmd { nexts; _ }, None -> select_case nexts - | BranchCmd { nexts; _ }, Some case -> ( - match Hashtbl.find_opt nexts case with + | Some (Single (Some next, _)), None -> Either.Left next + | Some (Branch nexts), None -> select_case nexts + | Some (Branch nexts), Some case -> ( + match List.assoc_opt case nexts with | None -> failwith "case not found" - | Some ((id, case), Nothing) -> Either.Right (id, case) - | Some (_, next) -> Either.Left next) - | FinalCmd { data }, None -> ( - match get_next_from_end state data with + | Some (None, id_case) -> Either.Right id_case + | Some (Some next, _) -> Either.Left next) + | None, None -> ( + match get_next_from_end state node.data with | Some (id, case) -> find_next state id case - | None -> Either.left map) + | None -> Either.left id) let request_next state id case = let rec aux id case = @@ -829,108 +848,98 @@ struct let exec_data = Effect.perform (Step (Some id, case, path)) in match init_or_handle ~state ~prev_id:id ?gil_case:case exec_data with | Either.Left (id, case) -> aux id case - | Either.Right map -> map + | Either.Right map -> map.data.id in aux id case let step state id case = let () = DL.log (fun m -> - m "Stepping %a %a" pp_rid id (pp_option Branch_case.pp) case) + m "Stepping %a %a" pp_id id (pp_option Branch_case.pp) case) in match find_next state id case with | Either.Left next -> next | Either.Right (id, case) -> request_next state id case let step_all state id case = - let cmd = Hashtbl.find state.id_map id in - let stack_depth = List.length (get_cmd_data_exn cmd).callers in + let cmd = get_exn state.map id in + let stack_depth = List.length cmd.data.callers in let rec aux ends = function | [] -> List.rev ends | (id, case) :: rest -> + let next_id = step state id case in + let node = get_exn state.map next_id in let ends, nexts = - match step state id case with - | Nothing -> failwith "Stepped to Nothing!" - | Cmd { data; _ } -> (ends, (data.id, None) :: rest) - | BranchCmd { data; nexts } -> + match node.next with + | Some (Single _) -> (ends, (next_id, None) :: rest) + | Some (Branch nexts) -> let new_nexts = - Hashtbl.to_seq_keys nexts - |> Seq.map (fun case -> (data.id, Some case)) - |> List.of_seq + nexts |> List.map (fun (case, _) -> (next_id, Some case)) in (ends, new_nexts @ rest) - | FinalCmd { data } as end_ -> - let stack_depth' = List.length data.callers in + | None -> + let stack_depth' = List.length node.data.callers in if stack_depth' < stack_depth then failwith "Stack depth too small!" else if stack_depth' > stack_depth then - let next = get_next_from_end state data |> Option.get in + let next = get_next_from_end state node.data |> Option.get in (ends, next :: rest) - else (end_ :: ends, rest) + else (node :: ends, rest) in aux ends nexts in - match (case, cmd) with - | _, Nothing -> failwith "Stepping from Nothing!" - | _, FinalCmd _ -> [ cmd ] - | None, BranchCmd { nexts; _ } -> + match (case, cmd.next) with + | _, None -> [ cmd ] + | None, Some (Branch nexts) -> let first_steps = - Hashtbl.to_seq_keys nexts - |> Seq.map (fun case -> (id, Some case)) - |> List.of_seq + nexts |> List.map (fun (case, _) -> (id, Some case)) in aux [] first_steps | _, _ -> aux [] [ (id, case) ] let step_branch state id case = let case = - Option.map - (fun (_, json) -> json |> Branch_case.of_yojson |> Result.get_ok) - case + let+ json = case in + json |> Branch_case.of_yojson |> Result.get_ok in - let next = step state id case in - let id = (get_cmd_data_exn next).id in - (id, Debugger_utils.Step) + let next_id = step state id case in + (next_id, Debugger_utils.Step) let step_over state id = - let map = Hashtbl.find state.id_map id in + let node = get_exn state.map id in let () = let () = - match map with - | BranchCmd { nexts; _ } -> - if Hashtbl.mem nexts Func_exit_placeholder then + match node.next with + | Some (Branch nexts) -> + if List.mem_assoc Func_exit_placeholder nexts then step state id (Some Func_exit_placeholder) |> ignore | _ -> () in - let> submap = - match (get_cmd_data_exn map).submap with - | NoSubmap | Proc _ | Submap Nothing -> None + let> submap_id = + match node.data.submap with + | NoSubmap | Proc _ -> None | Submap m -> Some m in - let _ = step_all state (get_cmd_data_exn submap).id None in + let _ = step_all state submap_id None in () in - let data = get_cmd_data_exn (step state id None) in - (data.id, Debugger_utils.Step) + let stop_id = step state id None in + (stop_id, Debugger_utils.Step) let step_in state id = - let cmd = Hashtbl.find state.id_map id in - match cmd with - | Nothing -> failwith "Stepping in from Nothing!" - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> - (* Only BranchCmds should have submaps *) - let- () = - match data.submap with - | NoSubmap | Proc _ | Submap Nothing -> None - | Submap m -> Some ((get_cmd_data_exn m).id, Debugger_utils.Step) - in - step_branch state id None + let cmd = get_exn state.map id in + (* Only BranchCmds should have submaps *) + let- () = + match cmd.data.submap with + | NoSubmap | Proc _ -> None + | Submap submap_id -> Some (submap_id, Debugger_utils.Step) + in + step_branch state id None let step_back state id = - let cmd = Hashtbl.find state.id_map id in - let data = get_cmd_data_exn cmd in + let cmd = get_exn state.map id in let id = - match data.prev with + match cmd.data.prev with | Some (id, _) -> id | None -> id in @@ -943,45 +952,42 @@ struct let ends' = step_all state id case in let ends', nexts = ends' - |> List.partition_map (fun map -> - let data = get_cmd_data_exn map in + |> List.partition_map (fun { data; _ } -> match get_next_from_end state data with | Some (id, case) -> Either.Right (id, case) - | None -> Either.Left map) + | None -> Either.Left data.id) in aux (ends @ ends') (nexts @ rest) in let ends = aux [] [ (id, None) ] in - let id = (get_cmd_data_exn (List.hd ends)).id in + let id = List.hd ends in (id, Debugger_utils.Step) let step_out state id = - let cmd = Hashtbl.find state.id_map id in - match (get_cmd_data_exn cmd).callers with + match (get_exn state.map id).data.callers with | [] -> continue state id | caller_id :: _ -> step_over state caller_id - let is_breakpoint _ = true (* TODO *) + let is_breakpoint _ = false (* TODO *) let continue_back state id = - let rec aux cmd = - let { id; _ } = get_cmd_data_exn cmd in - if is_breakpoint cmd then (id, Debugger_utils.Breakpoint) + let rec aux node = + let { id; callers; _ } = node.data in + if is_breakpoint node then (id, Debugger_utils.Breakpoint) else match previous_step id state with | None -> ( - match (get_cmd_data_exn cmd).callers with + match callers with | [] -> (id, Debugger_utils.Step) - | caller_id :: _ -> aux (Hashtbl.find state.id_map caller_id)) - | Some (id, _) -> aux (Hashtbl.find state.id_map id) + | caller_id :: _ -> aux (get_exn state.map caller_id)) + | Some (id, _) -> aux (get_exn state.map id) in - aux (Hashtbl.find state.id_map id) + aux (get_exn state.map id) let init ~proc_name ~all_procs:_ tl_ast prog = let gil_state = Gil.get_state () in let+ tl_ast = tl_ast in let partial_cmds = Partial_cmds.init () in - let id_map = Hashtbl.create 0 in let state = { proc_name; @@ -989,8 +995,7 @@ struct tl_ast; prog; partial_cmds; - map = Nothing; - id_map; + map = Exec_map.make (); func_return_map = Hashtbl.create 0; func_return_count = 0; } @@ -1007,10 +1012,9 @@ struct let exec_data = Effect.perform (Step (id, case, path)) in match init_or_handle ~state ?prev_id:id ?gil_case:case exec_data with | Either.Left (id, case) -> aux (Some (id, case)) - | Either.Right map -> map + | Either.Right map -> map.data.id in - let map = aux None in - let id = (get_cmd_data_exn map).id in + let id = aux None in (id, Debugger_utils.Step) in (state, finish_init) diff --git a/sphinx/debugger.rst b/sphinx/debugger.rst index e8a1ca39a..e046ffc3f 100644 --- a/sphinx/debugger.rst +++ b/sphinx/debugger.rst @@ -12,13 +12,13 @@ The Gillian debugger provides a custom interface for visualising symbolic execut Setup ----- -The debugger is used via a custom VSCode extension, found under the ``debugger-vscode-extension/`` directory in the repo. +The debugger is used via a custom VSCode extension, found under the ``debug-ui/`` directory in the repo. To try out the debugger, follow these steps: * Install `the base Gillian extension `_ * Make sure Gillian is built (see :doc:`install`) -* cd into ``debugger-vscode-extension/`` +* cd into ``debug-ui/`` * Run ``yarn`` to set up dependencies * Run ``yarn build`` to build the extension (or ``yarn watch`` to rebuild automatically) * In the *Run and debug* tab of VSCode, make sure *Debugger Extension* is selected from the dropdown, and click the green play button to start the extension @@ -27,7 +27,7 @@ To try out the debugger, follow these steps: :width: 175px :align: center -* A new VSCode window should open in ``debugger-vscode-extension/sampleWorkspace/``, with the extension installed +* A new VSCode window should open in ``debug-ui/examples/``, with the extension installed * In this window, open the workspace settings, and under the *Extensions > Gillian Debugger* section: * Make sure *Run mode* is set to ``source`` diff --git a/wisl/lib/debugging/wislLifter.ml b/wisl/lib/debugging/wislLifter.ml index 8332f9c60..e234ba464 100644 --- a/wisl/lib/debugging/wislLifter.ml +++ b/wisl/lib/debugging/wislLifter.ml @@ -14,7 +14,7 @@ open Annot open Branch_case open Debugger.Lifter -type rid = L.Report_id.t [@@deriving yojson, show] +type id = L.Report_id.t [@@deriving yojson, show] let rec int_to_letters = function | 0 -> "" @@ -42,9 +42,9 @@ struct module Gil_lifter = Gil.Lifter type cmd_report = CmdReport.t [@@deriving yojson] - type branch_data = rid * Gil_branch_case.t option [@@deriving yojson] + type branch_data = id * Gil_branch_case.t option [@@deriving yojson] type exec_data = cmd_report executed_cmd_data [@@deriving yojson] - type stack_direction = In | Out of rid [@@deriving yojson] + type stack_direction = In | Out of id [@@deriving yojson] let annot_to_wisl_stmt annot wisl_ast = let origin_id = annot.origin_id in @@ -75,36 +75,37 @@ struct failwith "get_fun_call_name: function name wasn't a literal expr!") | _ -> None - type map = (Branch_case.t, cmd_data, branch_data) Exec_map.t - - and cmd_data = { - id : rid; - all_ids : rid list; + type cmd_data = { + id : id; + all_ids : id list; display : string; matches : matching list; errors : string list; - mutable submap : map submap; + mutable submap : id submap; (* branch_path : Branch_case.t list; *) - prev : (rid * Branch_case.t option) option; - callers : rid list; + prev : (id * Branch_case.t option) option; + callers : id list; func_return_label : (string * int) option; } [@@deriving yojson] - type step_args = rid option * Gil_branch_case.t option * Gil_branch_case.path + type map = (id, Branch_case.t, cmd_data, branch_data) Exec_map.map + [@@deriving yojson] + + type step_args = id option * Gil_branch_case.t option * Gil_branch_case.path type _ Effect.t += Step : step_args -> exec_data Effect.t module Partial_cmds = struct - type prev = rid * Branch_case.t option * rid list [@@deriving yojson] + type prev = id * Branch_case.t option * id list [@@deriving yojson] type partial_data = { prev : prev option; - all_ids : (rid * (Branch_case.kind option * Branch_case.case)) Ext_list.t; - unexplored_paths : (rid * Gil_branch_case.t option) Stack.t; + all_ids : (id * (Branch_case.kind option * Branch_case.case)) Ext_list.t; + unexplored_paths : (id * Gil_branch_case.t option) Stack.t; ends : (Branch_case.case * branch_data) Ext_list.t; - mutable id : rid option; + mutable id : id option; mutable display : string option; - mutable stack_info : (rid list * stack_direction option) option; + mutable stack_info : (id list * stack_direction option) option; mutable nest_kind : nest_kind option; mutable is_loop_end : bool; matches : matching Ext_list.t; @@ -129,25 +130,25 @@ struct errors = Ext_list.make (); } - type t = (rid, partial_data) Hashtbl.t [@@deriving to_yojson] + type t = (id, partial_data) Hashtbl.t [@@deriving to_yojson] type finished = { - prev : (rid * Branch_case.t option) option; - id : rid; - all_ids : rid list; + prev : (id * Branch_case.t option) option; + id : id; + all_ids : id list; display : string; matches : matching list; errors : string list; - kind : (Branch_case.t, branch_data) cmd_kind; - submap : map submap; - callers : rid list; + next_kind : (Branch_case.t, branch_data) next_kind; + submap : id submap; + callers : id list; stack_direction : stack_direction option; } [@@deriving yojson] type partial_result = | Finished of finished - | StepAgain of (rid * Gil_branch_case.t option) + | StepAgain of (id * Gil_branch_case.t option) let step_again ~id ?branch_case () = Ok (StepAgain (id, branch_case)) @@ -233,14 +234,15 @@ struct | Some (LoopBody p) -> Proc p | _ -> NoSubmap in - let++ kind = + let++ next_kind = let++ cases = ends_to_cases ~nest_kind ends in match cases with - | _ when is_return exec_data -> Final - | _ when is_loop_end -> Final - | [] -> Final - | [ (Case (Unknown, _), _) ] -> Normal - | _ -> Branch cases + | _ when is_return exec_data -> Zero + | _ when is_loop_end -> Zero + | [] -> Zero + | [ (Case (Unknown, _), _) ] -> + One (Option.get (List_utils.last all_ids), None) + | _ -> Many cases in Finished { @@ -253,7 +255,7 @@ struct matches; errors; submap; - kind; + next_kind; } module Update = struct @@ -280,24 +282,24 @@ struct Error "HORROR - branch kind is set with pre-existing case!" let update_paths ~exec_data ~branch_case ~branch_kind partial = - let ({ id; kind; cmd_report; _ } : exec_data) = exec_data in + let ({ id; next_kind; cmd_report; _ } : exec_data) = exec_data in let annot = CmdReport.(cmd_report.annot) in let { ends; unexplored_paths; _ } = partial in let** is_end = get_is_end annot in - match (is_end, kind) with - | _, Final -> Ok () - | false, Normal -> + match (is_end, next_kind) with + | _, Zero -> Ok () + | false, One () -> Stack.push (id, None) unexplored_paths; Ok () - | false, Branch cases -> + | false, Many cases -> cases |> List.iter (fun (gil_case, ()) -> Stack.push (id, Some gil_case) unexplored_paths); Ok () - | true, Normal -> + | true, One () -> Ext_list.add (branch_case, (id, None)) ends; Ok () - | true, Branch cases -> + | true, Many cases -> cases |> List_utils.iter_results (fun (gil_case, ()) -> let++ case = @@ -390,8 +392,11 @@ struct let update_submap ~prog ~(annot : Annot.t) partial = match (partial.nest_kind, annot.nest_kind) with - | None, Some (FunCall fn) when not (is_fcall_using_spec fn prog) -> - partial.nest_kind <- Some (FunCall fn); + | None, Some (FunCall fn) -> + let () = + if not (is_fcall_using_spec fn prog) then + partial.nest_kind <- Some (FunCall fn) + in Ok () | None, nest -> partial.nest_kind <- nest; @@ -477,11 +482,10 @@ struct gil_state : Gil_lifter.t; [@to_yojson Gil_lifter.dump] tl_ast : tl_ast; [@to_yojson fun _ -> `Null] partial_cmds : Partial_cmds.t; - mutable map : map; - id_map : (rid, map) Hashtbl.t; [@to_yojson fun _ -> `Null] + map : map; mutable is_loop_func : bool; prog : (annot, int) Prog.t; [@to_yojson fun _ -> `Null] - func_return_map : (rid, string * int ref) Hashtbl.t; + func_return_map : (id, string * int ref) Hashtbl.t; mutable func_return_count : int; } [@@deriving to_yojson] @@ -489,6 +493,16 @@ struct let dump = to_yojson module Insert_new_cmd = struct + let failwith ~state ~finished_partial msg = + DL.failwith + (fun () -> + [ + ("state", to_yojson state); + ( "finished_partial", + Partial_cmds.finished_to_yojson finished_partial ); + ]) + ("WislLifter.insert_new_cmd: " ^ msg) + let new_function_return_label caller_id state = state.func_return_count <- state.func_return_count + 1; let label = int_to_letters state.func_return_count in @@ -497,25 +511,34 @@ struct (label, count) let update_caller_branches ~caller_id ~cont_id (label, ix) state = - match Hashtbl.find_opt state.id_map caller_id with + let result = + map_node_extra state.map caller_id (fun node -> + let new_next = + match node.next with + | Some (Branch nexts) -> + let nexts = List.remove_assoc FuncExitPlaceholder nexts in + let case = Case (FuncExit label, ix) in + let bdata = (cont_id, None) in + let nexts = nexts @ [ (case, (None, bdata)) ] in + Ok (Some (Branch nexts)) + | None | Some (Single _) -> + Fmt.error "update_caller_branches - caller %a does not branch" + pp_id caller_id + in + match new_next with + | Ok next -> ({ node with next }, Ok ()) + | Error e -> (node, Error e)) + in + match result with + | Some r -> r | None -> - Fmt.error "update_caller_branches - caller %a not found" pp_rid - caller_id - | Some (BranchCmd { nexts; _ }) -> - Hashtbl.remove nexts FuncExitPlaceholder; - let case = Case (FuncExit label, ix) in - let bdata = (cont_id, None) in - Hashtbl.add nexts case (bdata, Nothing); - Ok () - | Some _ -> - Fmt.error "update_caller_branches - caller %a does not branch" pp_rid + Fmt.error "update_caller_branches - caller %a not found" pp_id caller_id let resolve_func_branches ~state finished_partial = - let Partial_cmds.{ all_ids; kind; callers; _ } = finished_partial in - match (kind, callers) with - | Final, caller_id :: _ -> - let () = DL.log (fun m -> m "A") in + let Partial_cmds.{ all_ids; next_kind; callers; _ } = finished_partial in + match (next_kind, callers) with + | Zero, caller_id :: _ -> let label, count = match Hashtbl.find_opt state.func_return_map caller_id with | Some (label, count) -> (label, count) @@ -526,11 +549,9 @@ struct let cont_id = all_ids |> List.rev |> List.hd in let** () = update_caller_branches ~caller_id ~cont_id label state in Ok (Some label) - | _ -> - let () = DL.log (fun m -> m "B") in - Ok None + | _ -> Ok None - let make_new_cmd ~func_return_label finished_partial : map = + let make_new_cmd ~func_return_label finished_partial = let Partial_cmds. { all_ids; @@ -541,7 +562,7 @@ struct submap; prev; callers; - kind; + next_kind; _; } = finished_partial @@ -559,87 +580,108 @@ struct func_return_label; } in - match kind with - | Final -> FinalCmd { data } - | Normal -> Cmd { data; next = Nothing } - | Branch ends -> - let nexts = Hashtbl.create 0 in - List.iter - (fun (case, branch_data) -> - Hashtbl.add nexts case (branch_data, Nothing)) - ends; - BranchCmd { data; nexts } - - let insert_as_next ~state ~prev_id ?case new_cmd = - match (Hashtbl.find state.id_map prev_id, case) with - | Nothing, _ -> Error "trying to insert next of Nothing!" - | FinalCmd _, _ -> Error "trying to insert next of FinalCmd!" - | Cmd _, Some _ -> Error "tying to insert to non-branch cmd with branch!" - | BranchCmd _, None -> - Error "trying to insert to branch cmd with no branch!" - | Cmd c, None -> - c.next <- new_cmd; - Ok () - | BranchCmd { nexts; _ }, Some case -> ( - match Hashtbl.find nexts case with - | branch_data, Nothing -> - Hashtbl.replace nexts case (branch_data, new_cmd); - Ok () - | _ -> Error "duplicate insertion!") - - let insert_as_submap ~state ~parent_id new_cmd = - let** parent_data = - match Hashtbl.find state.id_map parent_id with - | Nothing -> Error "trying to insert submap of Nothing!" - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> Ok data + let next = + match next_kind with + | Zero -> None + | One bdata -> Some (Single (None, bdata)) + | Many ends -> + let nexts = + List.map (fun (case, bdata) -> (case, (None, bdata))) ends + in + Some (Branch nexts) + in + { data; next } + + let with_prev prev { data; next } = + let data = { data with prev } in + { data; next } + + let insert_as_next ~state ~prev_id ?case new_id = + map_node_extra_exn state.map prev_id (fun prev -> + let new_next = + let** next = + match prev.next with + | Some next -> Ok next + | None -> Error "trying to insert next of final cmd!" + in + match (next, case) with + | Single _, Some _ -> + Error "trying to insert to non-branch cmd with branch" + | Branch _, None -> + Error "trying to insert to branch cmd with no branch" + | Single (Some _, _), _ -> Error "duplicate insertion" + | Single (None, bdata), None -> + Ok (Some (Single (Some new_id, bdata))) + | Branch nexts, Some case -> ( + match List.assoc_opt case nexts with + | None -> Error "case not found" + | Some (Some _, _) -> Error "duplicate insertion" + | Some (None, bdata) -> + let nexts = + List_utils.assoc_replace case (Some new_id, bdata) nexts + in + Ok (Some (Branch nexts))) + in + match new_next with + | Ok next -> ({ prev with next }, Ok ()) + | Error e -> + (prev, Fmt.error "insert_as_next (%a) - %s" pp_id prev_id e)) + + let insert_as_submap ~state ~parent_id new_id = + map_node_extra_exn state.map parent_id (fun parent -> + match parent.data.submap with + | Proc _ | Submap _ -> (parent, Error "duplicate submaps!") + | NoSubmap -> + let data = { parent.data with submap = Submap new_id } in + ({ parent with data }, Ok ())) + + let insert_to_empty_map ~state ~prev ~stack_direction new_cmd = + let- () = + match state.map.root with + | Some _ -> Some None + | None -> None + in + let r = + match (stack_direction, prev) with + | Some _, _ -> Error "stepping in our out with empty map!" + | _, Some _ -> Error "inserting to empty map with prev!" + | None, None -> + let new_cmd = new_cmd |> with_prev None in + let () = state.map.root <- Some new_cmd.data.id in + Ok new_cmd in - match parent_data.submap with - | Proc _ | Submap _ -> Error "duplicate submaps!" - | NoSubmap -> - parent_data.submap <- Submap new_cmd; - Ok () + Some r let insert_cmd ~state ~prev ~stack_direction new_cmd = - match (stack_direction, state.map, prev) with - | Some _, Nothing, _ -> Error "stepping in our out with empty map!" - | _, Nothing, Some _ -> Error "inserting to empty map with prev!" - | None, Nothing, None -> - state.map <- new_cmd; - Ok new_cmd - | _, _, None -> Error "inserting to non-empty map with no prev!" - | Some In, _, Some (parent_id, Some FuncExitPlaceholder) - | Some In, _, Some (parent_id, None) -> - let new_cmd = new_cmd |> map_data (fun d -> { d with prev = None }) in - let++ () = insert_as_submap ~state ~parent_id new_cmd in + let- () = insert_to_empty_map ~state ~prev ~stack_direction new_cmd in + match (stack_direction, prev) with + | _, None -> Error "inserting to non-empty map with no prev!" + | Some In, Some (parent_id, Some FuncExitPlaceholder) + | Some In, Some (parent_id, None) -> + let new_cmd = new_cmd |> with_prev None in + let++ () = insert_as_submap ~state ~parent_id new_cmd.data.id in new_cmd - | Some In, _, Some (_, Some case) -> + | Some In, Some (_, Some case) -> Fmt.error "stepping in with branch case (%a)!" Branch_case.pp case - | None, _, Some (prev_id, case) -> - let++ () = insert_as_next ~state ~prev_id ?case new_cmd in + | None, Some (prev_id, case) -> + let++ () = insert_as_next ~state ~prev_id ?case new_cmd.data.id in new_cmd - | Some (Out prev_id), _, Some (inner_prev_id, _) -> + | Some (Out prev_id), Some (inner_prev_id, _) -> let** case = let func_return_label = - match Hashtbl.find state.id_map inner_prev_id with - | Nothing -> None - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> - data.func_return_label + (get_exn state.map inner_prev_id).data.func_return_label in match func_return_label with | Some (label, ix) -> Ok (Case (FuncExit label, ix)) | None -> Error "stepping out without function return label!" in - let new_cmd = - new_cmd - |> map_data (fun d -> { d with prev = Some (prev_id, Some case) }) - in - let++ () = insert_as_next ~state ~prev_id ~case new_cmd in + let new_cmd = new_cmd |> with_prev (Some (prev_id, Some case)) in + let++ () = insert_as_next ~state ~prev_id ~case new_cmd.data.id in new_cmd let f ~state finished_partial = let r = - let { id_map; _ } = state in - let Partial_cmds.{ all_ids; prev; stack_direction; _ } = + let Partial_cmds.{ id; all_ids; prev; stack_direction; _ } = finished_partial in let** func_return_label = @@ -647,19 +689,10 @@ struct in let new_cmd = make_new_cmd ~func_return_label finished_partial in let** new_cmd = insert_cmd ~state ~prev ~stack_direction new_cmd in - all_ids |> List.iter (fun id -> Hashtbl.replace id_map id new_cmd); + let () = insert state.map ~id ~all_ids new_cmd in Ok new_cmd in - r - |> Result_utils.or_else (fun e -> - DL.failwith - (fun () -> - [ - ("state", dump state); - ( "finished_partial", - Partial_cmds.finished_to_yojson finished_partial ); - ]) - ("WislLifter.insert_new_cmd: " ^ e)) + Result_utils.or_else (failwith ~state ~finished_partial) r end let insert_new_cmd = Insert_new_cmd.f @@ -680,33 +713,32 @@ struct | _ -> None let get_prev ~state ~gil_case ~prev_id () = - let { map; id_map; _ } = state in + let { map; _ } = state in let=* prev_id = Ok prev_id in - let=* map = - match Hashtbl.find_opt id_map prev_id with + let=* prev = + match get map prev_id with | None -> ( - match map with - | Nothing -> Ok None + match map.root with + | None -> Ok None | _ -> Error "couldn't find map at prev_id!") | map -> Ok map in - match map with - | Nothing -> Error "got Nothing map!" - | FinalCmd { data } | Cmd { data; _ } -> - Ok (Some (data.id, None, data.callers)) - | BranchCmd { data; nexts } -> ( + let { id; callers; _ } = prev.data in + match prev.next with + | None | Some (Single _) -> Ok (Some (id, None, callers)) + | Some (Branch nexts) -> ( let case = - Hashtbl.find_map - (fun case ((id, gil_case'), _) -> - if id = prev_id && gil_case' = gil_case then Some case else None) + List.find_map + (fun (case, (_, (prev_id', gil_case'))) -> + if prev_id' = prev_id && gil_case' = gil_case then Some case + else None) nexts in match case with - | Some case -> Ok (Some (data.id, Some case, data.callers)) + | Some case -> Ok (Some (id, Some case, callers)) | None -> Error "couldn't find prev in branches!") - let f ~state ?prev_id ?gil_case (exec_data : exec_data) : - (rid * Gil_branch_case.t option, map) Either.t = + let f ~state ?prev_id ?gil_case (exec_data : exec_data) = let- () = let+ id, case = handle_loop_prefix exec_data in state.is_loop_func <- true; @@ -744,54 +776,36 @@ struct let package_case case = let json = Branch_case.to_yojson case in let display = Branch_case.display case in - (display, json) - - let package_data package { id; all_ids; display; matches; errors; submap; _ } - = - let submap = - match submap with - | NoSubmap -> NoSubmap - | Proc p -> Proc p - | Submap map -> Submap (package map) - in + (json, display) + + let package_data { id; all_ids; display; matches; errors; submap; _ } = Packaged.{ id; all_ids; display; matches; errors; submap } - let package = - let package_case - ~(bd : branch_data) - ~(all_cases : (Branch_case.t * branch_data) list) - case = - ignore bd; - ignore all_cases; - package_case case + let package_node { data : cmd_data; next } = + let data = package_data data in + let next = + match next with + | None -> None + | Some (Single (next, _)) -> Some (Single (next, "")) + | Some (Branch nexts) -> + let nexts = + nexts + |> List.map (fun (case, (next, _)) -> + let case, bdata = package_case case in + (case, (next, bdata))) + in + Some (Branch nexts) in - Packaged.package package_data package_case + { data; next } + let package = Packaged.package Fun.id package_node let get_lifted_map_exn { map; _ } = package map let get_lifted_map state = Some (get_lifted_map_exn state) - - let get_matches_at_id id { id_map; _ } = - let map = Hashtbl.find id_map id in - match map with - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> - data.matches - | _ -> - failwith "get_matches_at_id: HORROR - tried to get matches at non-cmd!" - - let get_root_id { map; _ } = - match map with - | Nothing -> None - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> - Some data.id - + let get_matches_at_id id { map; _ } = (get_exn map id).data.matches let path_of_id id { gil_state; _ } = Gil_lifter.path_of_id id gil_state - let previous_step id { id_map; _ } = - let+ id, case = - match Hashtbl.find id_map id with - | Nothing -> None - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> data.prev - in + let previous_step id { map; _ } = + let+ id, case = (get_exn map id).data.prev in let case = case |> Option.map package_case in (id, case) @@ -924,14 +938,14 @@ struct let select_case nexts = let result = - Hashtbl.fold - (fun _ (id_case, map) acc -> - match (map, acc) with + List.fold_left + (fun acc (_, (next, id_case)) -> + match (next, acc) with | _, Some (Either.Right _) -> acc - | Nothing, _ -> Some (Either.Right id_case) - | map, None -> Some (Either.Left map) + | None, _ -> Some (Either.Right id_case) + | Some id, None -> Some (Either.Left id) | _ -> acc) - nexts None + None nexts in Option.get result @@ -943,20 +957,19 @@ struct let* label, ix = func_return_label in let case = Case (FuncExit label, ix) in let* _ = - match Hashtbl.find state.id_map caller_id with - | BranchCmd { nexts; _ } -> Hashtbl.find_opt nexts case + match (get_exn state.map caller_id).next with + | Some (Branch nexts) -> List.assoc_opt case nexts | _ -> None in Some (caller_id, Some case) let rec find_next state id case = - let map = Hashtbl.find state.id_map id in - match (map, case) with - | Nothing, _ -> failwith "HORROR - map is Nothing!" - | (FinalCmd _ | Cmd _), Some _ -> + let node = get_exn state.map id in + match (node.next, case) with + | (None | Some (Single _)), Some _ -> failwith "HORROR - tried to step case for non-branch cmd" - | Cmd { next = Nothing; data = { all_ids; _ } }, None -> - let id = List.hd (List.rev all_ids) in + | Some (Single (None, _)), None -> + let id = List.hd (List.rev node.data.all_ids) in let case = match Gil_lifter.cases_at_id id state.gil_state with | [] -> None @@ -967,17 +980,17 @@ struct L.Report_id.pp id in Either.Right (id, case) - | Cmd { next; _ }, None -> Either.Left next - | BranchCmd { nexts; _ }, None -> select_case nexts - | BranchCmd { nexts; _ }, Some case -> ( - match Hashtbl.find_opt nexts case with + | Some (Single (Some next, _)), None -> Either.Left next + | Some (Branch nexts), None -> select_case nexts + | Some (Branch nexts), Some case -> ( + match List.assoc_opt case nexts with | None -> failwith "case not found" - | Some ((id, case), Nothing) -> Either.Right (id, case) - | Some (_, next) -> Either.Left next) - | FinalCmd { data }, None -> ( - match get_next_from_end state data with + | Some (None, id_case) -> Either.Right id_case + | Some (Some next, _) -> Either.Left next) + | None, None -> ( + match get_next_from_end state node.data with | Some (id, case) -> find_next state id case - | None -> Either.left map) + | None -> Either.left id) let request_next state id case = let rec aux id case = @@ -985,108 +998,98 @@ struct let exec_data = Effect.perform (Step (Some id, case, path)) in match init_or_handle ~state ~prev_id:id ?gil_case:case exec_data with | Either.Left (id, case) -> aux id case - | Either.Right map -> map + | Either.Right map -> map.data.id in aux id case let step state id case = let () = DL.log (fun m -> - m "Stepping %a %a" pp_rid id (pp_option Branch_case.pp) case) + m "Stepping %a %a" pp_id id (pp_option Branch_case.pp) case) in match find_next state id case with | Either.Left next -> next | Either.Right (id, case) -> request_next state id case let step_all state id case = - let cmd = Hashtbl.find state.id_map id in - let stack_depth = List.length (get_cmd_data_exn cmd).callers in + let cmd = get_exn state.map id in + let stack_depth = List.length cmd.data.callers in let rec aux ends = function | [] -> List.rev ends | (id, case) :: rest -> + let next_id = step state id case in + let node = get_exn state.map next_id in let ends, nexts = - match step state id case with - | Nothing -> failwith "Stepped to Nothing!" - | Cmd { data; _ } -> (ends, (data.id, None) :: rest) - | BranchCmd { data; nexts } -> + match node.next with + | Some (Single _) -> (ends, (next_id, None) :: rest) + | Some (Branch nexts) -> let new_nexts = - Hashtbl.to_seq_keys nexts - |> Seq.map (fun case -> (data.id, Some case)) - |> List.of_seq + nexts |> List.map (fun (case, _) -> (next_id, Some case)) in (ends, new_nexts @ rest) - | FinalCmd { data } as end_ -> - let stack_depth' = List.length data.callers in + | None -> + let stack_depth' = List.length node.data.callers in if stack_depth' < stack_depth then failwith "Stack depth too small!" else if stack_depth' > stack_depth then - let next = get_next_from_end state data |> Option.get in + let next = get_next_from_end state node.data |> Option.get in (ends, next :: rest) - else (end_ :: ends, rest) + else (node :: ends, rest) in aux ends nexts in - match (case, cmd) with - | _, Nothing -> failwith "Stepping from Nothing!" - | _, FinalCmd _ -> [ cmd ] - | None, BranchCmd { nexts; _ } -> + match (case, cmd.next) with + | _, None -> [ cmd ] + | None, Some (Branch nexts) -> let first_steps = - Hashtbl.to_seq_keys nexts - |> Seq.map (fun case -> (id, Some case)) - |> List.of_seq + nexts |> List.map (fun (case, _) -> (id, Some case)) in aux [] first_steps | _, _ -> aux [] [ (id, case) ] let step_branch state id case = let case = - Option.map - (fun (_, json) -> json |> Branch_case.of_yojson |> Result.get_ok) - case + let+ json = case in + json |> Branch_case.of_yojson |> Result.get_ok in - let next = step state id case in - let id = (get_cmd_data_exn next).id in - (id, Debugger_utils.Step) + let next_id = step state id case in + (next_id, Debugger_utils.Step) let step_over state id = - let map = Hashtbl.find state.id_map id in + let node = get_exn state.map id in let () = let () = - match map with - | BranchCmd { nexts; _ } -> - if Hashtbl.mem nexts FuncExitPlaceholder then + match node.next with + | Some (Branch nexts) -> + if List.mem_assoc FuncExitPlaceholder nexts then step state id (Some FuncExitPlaceholder) |> ignore | _ -> () in - let> submap = - match (get_cmd_data_exn map).submap with - | NoSubmap | Proc _ | Submap Nothing -> None + let> submap_id = + match node.data.submap with + | NoSubmap | Proc _ -> None | Submap m -> Some m in - let _ = step_all state (get_cmd_data_exn submap).id None in + let _ = step_all state submap_id None in () in - let data = get_cmd_data_exn (step state id None) in - (data.id, Debugger_utils.Step) + let stop_id = step state id None in + (stop_id, Debugger_utils.Step) let step_in state id = - let cmd = Hashtbl.find state.id_map id in - match cmd with - | Nothing -> failwith "Stepping in from Nothing!" - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> - (* Only BranchCmds should have submaps *) - let- () = - match data.submap with - | NoSubmap | Proc _ | Submap Nothing -> None - | Submap m -> Some ((get_cmd_data_exn m).id, Debugger_utils.Step) - in - step_branch state id None + let cmd = get_exn state.map id in + (* Only BranchCmds should have submaps *) + let- () = + match cmd.data.submap with + | NoSubmap | Proc _ -> None + | Submap submap_id -> Some (submap_id, Debugger_utils.Step) + in + step_branch state id None let step_back state id = - let cmd = Hashtbl.find state.id_map id in - let data = get_cmd_data_exn cmd in + let cmd = get_exn state.map id in let id = - match data.prev with + match cmd.data.prev with | Some (id, _) -> id | None -> id in @@ -1099,53 +1102,49 @@ struct let ends' = step_all state id case in let ends', nexts = ends' - |> List.partition_map (fun map -> - let data = get_cmd_data_exn map in + |> List.partition_map (fun { data; _ } -> match get_next_from_end state data with | Some (id, case) -> Either.Right (id, case) - | None -> Either.Left map) + | None -> Either.Left data.id) in aux (ends @ ends') (nexts @ rest) in let ends = aux [] [ (id, None) ] in - let id = (get_cmd_data_exn (List.hd ends)).id in + let id = List.hd ends in (id, Debugger_utils.Step) let step_out state id = - let cmd = Hashtbl.find state.id_map id in - match (get_cmd_data_exn cmd).callers with + match (get_exn state.map id).data.callers with | [] -> continue state id | caller_id :: _ -> step_over state caller_id - let is_breakpoint _ = true (* TODO *) + let is_breakpoint _ = false (* TODO *) let continue_back state id = - let rec aux cmd = - let { id; _ } = get_cmd_data_exn cmd in - if is_breakpoint cmd then (id, Debugger_utils.Breakpoint) + let rec aux node = + let { id; callers; _ } = node.data in + if is_breakpoint node then (id, Debugger_utils.Breakpoint) else match previous_step id state with | None -> ( - match (get_cmd_data_exn cmd).callers with + match callers with | [] -> (id, Debugger_utils.Step) - | caller_id :: _ -> aux (Hashtbl.find state.id_map caller_id)) - | Some (id, _) -> aux (Hashtbl.find state.id_map id) + | caller_id :: _ -> aux (get_exn state.map caller_id)) + | Some (id, _) -> aux (get_exn state.map id) in - aux (Hashtbl.find state.id_map id) + aux (get_exn state.map id) let init ~proc_name ~all_procs:_ tl_ast prog = let gil_state = Gil.get_state () in let+ tl_ast = tl_ast in let partial_cmds = Partial_cmds.init () in - let id_map = Hashtbl.create 0 in let state = { proc_name; gil_state; tl_ast; partial_cmds; - map = Nothing; - id_map; + map = Exec_map.make (); is_loop_func = false; prog; func_return_map = Hashtbl.create 0; @@ -1164,10 +1163,9 @@ struct let exec_data = Effect.perform (Step (id, case, path)) in match init_or_handle ~state ?prev_id:id ?gil_case:case exec_data with | Either.Left (id, case) -> aux (Some (id, case)) - | Either.Right map -> map + | Either.Right map -> map.data.id in - let map = aux None in - let id = (get_cmd_data_exn map).id in + let id = aux None in (id, Debugger_utils.Step) in (state, finish_init)