From ead989a05e2ae1fb99a855706141883ac05ed63b Mon Sep 17 00:00:00 2001 From: Nat Karmios Date: Sat, 2 Mar 2024 03:55:10 +0000 Subject: [PATCH] WIP --- Gillian-C/bin/gillian_c.ml | 4 +- Gillian-JS/lib/Debugging/JSLifter.ml | 4 +- GillianCore/debugging/adapter/time_travel.ml | 2 +- .../debugging/debugger/base_debugger.ml | 749 ++++++------------ .../debugging/debugger/debugger_intf.ml | 2 +- .../debugging/lifter/gil_fallback_lifter.ml | 149 ++-- GillianCore/debugging/lifter/gil_lifter.ml | 298 +++---- GillianCore/debugging/lifter/gil_lifter.mli | 18 +- .../debugging/lifter/gil_lifter_intf.ml | 45 ++ GillianCore/debugging/lifter/lifter.ml | 3 +- GillianCore/debugging/lifter/lifter_intf.ml | 77 +- GillianCore/debugging/log/debugger_log.ml | 6 + GillianCore/debugging/utils/exec_map.ml | 9 + .../general/g_interpreter.ml | 207 +++-- .../general/g_interpreter_intf.ml | 12 +- .../kani/c/wpst/llen.c.symtab.json | 40 +- .../kani/c/wpst/simple_branch.c.symtab.json | 108 +-- .../sampleWorkspace/list_length_rec.wisl | 2 +- kanillian/lib/lifter/kani_c_lifter.ml | 342 +++++--- wisl/lib/debugging/wislLifter.ml | 386 ++++++--- 20 files changed, 1318 insertions(+), 1145 deletions(-) create mode 100644 GillianCore/debugging/lifter/gil_lifter_intf.ml diff --git a/Gillian-C/bin/gillian_c.ml b/Gillian-C/bin/gillian_c.ml index 99192be51..307e53bbc 100644 --- a/Gillian-C/bin/gillian_c.ml +++ b/Gillian-C/bin/gillian_c.ml @@ -6,8 +6,8 @@ module Gil_to_c_lifter with type annot = CParserAndCompiler.Annot.t) = struct include - Gillian.Debugger.Lifter.Gil_lifter.Make (CParserAndCompiler) (Verification) - (SMemory) + Gillian.Debugger.Lifter.Gil_lifter.Make (SMemory) (CParserAndCompiler) + (Verification) let add_variables = MonadicSMemory.Lift.add_variables end diff --git a/Gillian-JS/lib/Debugging/JSLifter.ml b/Gillian-JS/lib/Debugging/JSLifter.ml index 39e1a4f6b..81d704ebd 100644 --- a/Gillian-JS/lib/Debugging/JSLifter.ml +++ b/Gillian-JS/lib/Debugging/JSLifter.ml @@ -7,8 +7,8 @@ module Make (Verification : Gillian.Abstraction.Verifier.S with type annot = PC.Annot.t) = struct module Gil_lifter = - Gillian.Debugger.Lifter.Gil_lifter.Make (PC) (Verification) - (Semantics.Symbolic) + Gillian.Debugger.Lifter.Gil_lifter.Make (Semantics.Symbolic) (PC) + (Verification) include Gil_lifter diff --git a/GillianCore/debugging/adapter/time_travel.ml b/GillianCore/debugging/adapter/time_travel.ml index 07254ffc3..4e7e8c516 100644 --- a/GillianCore/debugging/adapter/time_travel.ml +++ b/GillianCore/debugging/adapter/time_travel.ml @@ -25,7 +25,7 @@ module Make (Debugger : Debugger.S) = struct (fun _ -> let stop_reason = Debugger.step dbg in send_stopped_events stop_reason); - DL.set_rpc_command_handler rpc ~name:"Reverse" + DL.set_rpc_command_handler rpc ~name:"Reverse continue" (module Reverse_continue_command) (fun _ -> let stop_reason = Debugger.run ~reverse:true dbg in diff --git a/GillianCore/debugging/debugger/base_debugger.ml b/GillianCore/debugging/debugger/base_debugger.ml index a875c9a7f..81b60a288 100644 --- a/GillianCore/debugging/debugger/base_debugger.ml +++ b/GillianCore/debugging/debugger/base_debugger.ml @@ -33,7 +33,7 @@ struct type 'ext base_proc_state = { mutable cont_func : result_t cont_func_f option; mutable breakpoints : breakpoints; [@default Hashtbl.create 0] - mutable cur_report_id : L.Report_id.t; + mutable cur_report_id : L.Report_id.t option; (* TODO: The below fields only depend on the cur_report_id and could be refactored to use this *) mutable top_level_scopes : Variable.scope list; @@ -184,7 +184,7 @@ struct let procs = Hashtbl.fold (fun proc_name state acc -> - let current_cmd_id = state.cur_report_id in + let current_cmd_id = Option.get state.cur_report_id in let matches = state.lifter_state |> Lifter.get_matches_at_id current_cmd_id in @@ -414,7 +414,7 @@ struct let f report_id cfg state = let cmd = get_cmd report_id in - state.cur_report_id <- report_id; + state.cur_report_id <- Some report_id; state.frames <- call_stack_to_frames cmd.callstack cmd.proc_line cfg.prog; let lifted_scopes, variables = @@ -433,8 +433,6 @@ struct let jump_state_to_id id cfg state = try DL.log (fun m -> m "Jumping to id %a" L.Report_id.pp id); - (* state.exec_map |> snd |> Exec_map.path_of_id id |> ignore; *) - (* TODO *) state |> update_proc_state id cfg; Ok () with Failure msg -> Error msg @@ -473,28 +471,22 @@ struct in (exec_data, cmd) - module Execute_step = struct - open Verification.SAInterpreter.Logging - - type execute_step = - L.Report_id.t -> - ?branch_case:Branch_case.t -> - ?branch_path:Branch_case.path -> - debug_state -> - proc_state -> - stop_reason * L.Report_id.t option - - let get_branch_path prev_id case path state = - let branch_path = - match path with - | Some path -> path - | None -> state.lifter_state |> Lifter.select_next_path case prev_id + 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 - DL.log (fun m -> - m - ~json:[ ("path", Branch_case.path_to_yojson branch_path) ] - "Got path for ID %a" L.Report_id.pp prev_id); - branch_path + 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 let check_cur_report_id = function | None -> @@ -502,297 +494,251 @@ struct "Did not log report. Check the logging level is set correctly" | Some id -> id - let handle_lifter_result - (execute_step : execute_step) - ?default_next_id - dbg - state - on_stop - (result : Lift.handle_cmd_result) = - match result with - | ExecNext (id, branch_case) -> - DL.log (fun m -> - m "EXEC NEXT (%a, %a)" (pp_option L.Report_id.pp) id - (pp_option Branch_case.pp) branch_case); - let id = Option_utils.coalesce id default_next_id |> Option.get in - execute_step id ?branch_case dbg state - | Stop id -> on_stop id - - module Handle_continue = struct - (* A command step with no results *should* mean that we're returning. - If we're at the top of the callstack, this *should* mean that we're hitting the end of the program. *) - let is_eob ~content ~type_ ~id = - let is_root = - match - content |> Yojson.Safe.from_string |> ConfigReport.of_yojson - with - | Error _ -> - DL.log (fun m -> - m - "Handle_continue.is_eob: Not a ConfigReport (type %s); \ - I'm not sure what to do here." - type_); - true - | Ok report -> ( - match report.callstack with - | [] -> failwith "HORROR: Empty callstack!" - | [ _ ] -> true - | _ -> false) - in - if is_root then - L.Log_queryer.get_cmd_results id - |> List.for_all (fun (_, content) -> - let result = - content |> of_yojson_string CmdResult.of_yojson - in - result.errors <> []) - else false - - let get_report_and_check_type - ?(log_context = "execute_step") - ~on_proc_init - ~on_eob - ~continue - id = - let content, type_ = Option.get @@ L.Log_queryer.get_report id in + (* A command step with no results *should* mean that we're returning. + If we're at the top of the callstack, this *should* mean that we're hitting the end of the program. *) + let is_eob ~content ~type_ ~id = + let is_root = + match + content |> Yojson.Safe.from_string |> ConfigReport.of_yojson + with + | Error _ -> + DL.log (fun m -> + m + "Handle_continue.is_eob: Not a ConfigReport (type %s); I'm \ + not sure what to do here." + type_); + true + | Ok report -> ( + match report.callstack with + | [] -> failwith "HORROR: Empty callstack!" + | [ _ ] -> true + | _ -> false) + in + if is_root then + L.Log_queryer.get_cmd_results id + |> List.for_all (fun (_, content) -> + let result = content |> of_yojson_string CmdResult.of_yojson in + result.errors <> []) + else false + + type continue_kind = ProcInit | EoB | Continue + + let get_report_and_check_type ?(log_context = "execute_step") id = + let content, type_ = Option.get @@ L.Log_queryer.get_report id in + let kind = if type_ = Content_type.proc_init then ( DL.log (fun m -> m "Debugger.%s: Skipping proc_init..." log_context); - on_proc_init ()) + ProcInit) else if is_eob ~content ~type_ ~id then ( DL.log (fun m -> m "Debugger.%s: No non-error results for %a; stepping again \ for EoB" log_context L.Report_id.pp id); - on_eob ()) - else continue content - - let f - (execute_step : execute_step) - prev_id_in_frame - cur_report_id - branch_case - branch_path - new_branch_cases - cont_func - debug_state - proc_state = - let cur_report_id = check_cur_report_id cur_report_id in - proc_state.cont_func <- Some cont_func; - cur_report_id - |> get_report_and_check_type - ~on_proc_init:(fun () -> - execute_step prev_id_in_frame debug_state proc_state) - ~on_eob:(fun () -> - execute_step ~branch_path cur_report_id debug_state proc_state) - ~continue:(fun content -> - update_proc_state cur_report_id debug_state proc_state; - let cmd = content |> of_yojson_string ConfigReport.of_yojson in - let cmd_kind = Exec_map.kind_of_cases new_branch_cases in - let matches = - get_matches cur_report_id debug_state proc_state - in - let exec_data = - Lift.make_executed_cmd_data cmd_kind cur_report_id cmd - ~matches branch_path - in - proc_state.lifter_state - |> Lifter.handle_cmd prev_id_in_frame branch_case exec_data - |> handle_lifter_result ~default_next_id:cur_report_id - execute_step debug_state proc_state - (handle_stop debug_state proc_state cur_report_id)) - end - - let handle_continue = Handle_continue.f - - module Handle_end_of_branch = struct - let get_prev prev_id = - let prev = - let+ content, type_ = L.Log_queryer.get_report prev_id in - (prev_id, content, type_) - in - match prev with - | Some (prev_id, content, type_) when type_ = Content_type.cmd -> - (prev_id, content) - | Some (prev_id, _, type_) -> - Fmt.failwith "EndOfBranch: prev cmd (%a) is '%s', not '%s'!" - L.Report_id.pp prev_id type_ Content_type.cmd - | None -> - Fmt.failwith "EndOfBranch: prev id '%a' doesn't exist!" - L.Report_id.pp prev_id - - let f - (execute_step : execute_step) - prev_id_in_frame - result - cont_func - branch_path - debug_state - proc_state = - proc_state.cont_func <- Some cont_func; - let prev_id, content = get_prev prev_id_in_frame in - let prev_prev_id = - L.Log_queryer.get_previous_report_id prev_id |> Option.get - in - let exec_data, cmd = - build_final_cmd_data content result prev_id branch_path debug_state - in - update_proc_state prev_id debug_state proc_state; - proc_state.lifter_state - |> Lifter.handle_cmd prev_prev_id cmd.branch_case exec_data - |> handle_lifter_result execute_step debug_state proc_state - (handle_stop debug_state proc_state ~is_end:true prev_id) - end - - let handle_end_of_branch = Handle_end_of_branch.f - - let rec f - prev_id_in_frame - ?branch_case - ?branch_path - debug_state - proc_state = - let open Verification.SAInterpreter in - match proc_state.cont_func with - | None -> - DL.log (fun m -> m "No cont_func; reached end"); - (ReachedEnd, None) - | Some cont_func -> ( - let branch_path = - get_branch_path prev_id_in_frame branch_case branch_path - proc_state + EoB) + else Continue + in + (kind, content) + + (* + This is a bit weird; it hinges on the fact that the ReturnNormal GIL cmd gives no results + FIXME: I don't think g_interpreter actually logs the result? + this means we need to get results via cont_func and needs to be changed. + *) + let find_or_exec_eob + id + (cont_func : 'a Verification.SAInterpreter.cont_func_f) = + ignore id; + (* TODO try to find result in log *) + match cont_func ~selector:(IdCase (id, None)) () with + | Finished _ -> + failwith "HORROR: Shouldn't encounter Finished when debugging!" + | Continue _ -> failwith "Expected EoB, got Continue!" + | EndOfBranch (result, cont_func) -> (result, cont_func) + + let find_or_exec_next + id + case + path + (cont_func : 'a Verification.SAInterpreter.cont_func_f) = + let next = + let* id = id in + L.Log_queryer.get_next_reports id + |> List.find_map (fun (_, content, type_) -> + if type_ = Content_type.cmd then + let cmd = + content |> of_yojson_string Logging.ConfigReport.of_yojson + in + match (case, cmd.branch_case) with + | Some case, Some bc when bc = case -> Some id + | None, _ -> Some id + | _ -> None + else None) + in + match next with + | Some id -> + let new_branch_cases = + L.Log_queryer.get_cmd_results id + |> List.filter_map (fun (_, content) -> + let result = + of_yojson_string Logging.CmdResult.of_yojson content + in + result.branch_case) in - match cont_func ~path:branch_path () with + let branch_path = List_utils.cons_opt case path in + (id, branch_path, new_branch_cases, cont_func) + | None -> ( + let selector = + match id with + | Some id -> IdCase (id, case) + | None -> Path path + in + DL.log (fun m -> m "Calling cont func"); + match cont_func ~selector () with | Finished _ -> - proc_state.cont_func <- None; failwith "HORROR: Shouldn't encounter Finished when debugging!" - | EndOfBranch (result, cont_func) -> - handle_end_of_branch f prev_id_in_frame result cont_func - branch_path debug_state proc_state + | EndOfBranch _ -> failwith "Unexpected EndOfBranch!" | Continue { report_id; branch_path; new_branch_cases; cont_func } -> - handle_continue f prev_id_in_frame report_id branch_case - branch_path new_branch_cases cont_func debug_state proc_state) - end + let id = check_cur_report_id report_id in + (id, branch_path, new_branch_cases, cont_func)) + + let get_next_step id case path debug_state proc_state = + let cont_func = + Option_utils.or_else + (fun () -> failwith "HORROR: No cont func!") + proc_state.cont_func + in + let id, path, new_branch_cases, cont_func = + find_or_exec_next id case path cont_func + in + let continue_kind, content = get_report_and_check_type id in + let exec_data, cont_func = + match continue_kind with + | ProcInit -> failwith "Unexpected ProcInit!" + | Continue -> + let cmd_kind = Exec_map.kind_of_cases new_branch_cases in + let matches = get_matches id debug_state proc_state in + let report = + of_yojson_string Logging.ConfigReport.of_yojson content + in + let exec_data = + Lift.make_executed_cmd_data cmd_kind id report ~matches path + in + (exec_data, cont_func) + | EoB -> + let result, cont_func = find_or_exec_eob id cont_func in + let exec_data, _ = + build_final_cmd_data content result id path debug_state + in + (exec_data, cont_func) + in + let () = proc_state.cont_func <- Some cont_func in + exec_data + + let handle_step_effect id case path proc_state { debug_state; _ } = + let () = + let> id = id in + jump_state_to_id id debug_state proc_state |> Result.get_ok + in + let exec_data = get_next_step id case path debug_state proc_state in + let () = update_proc_state exec_data.id debug_state proc_state in + exec_data + + let with_lifter_effects f proc_state state = + let open Effect.Deep in + let open Lifter in + try_with f () + { + effc = + (fun (type a) (eff : a Effect.t) -> + match eff with + | Step (id, case, path) -> + Some + (fun (k : (a, _) continuation) -> + let step_result = + handle_step_effect id case path proc_state state + in + Effect.Deep.continue k step_result) + | _ -> + let s = Printexc.to_string (Effect.Unhandled eff) in + Fmt.failwith "HORROR: effect leak!\n%s" s); + } + + let lifter_call lifter_func proc_state state = + let stop_id, stop_reason = + with_lifter_effects lifter_func proc_state state + in + let++ () = jump_state_to_id stop_id state.debug_state proc_state in + stop_reason - let execute_step = Execute_step.f + let lifter_call_with_id state lifter_func = + let proc_state = get_proc_state_exn state in + let { cur_report_id; lifter_state; _ } = proc_state in + let id = Option.get cur_report_id in + let f () = lifter_func lifter_state id in + lifter_call f proc_state state |> Result.get_ok + + let over state = lifter_call_with_id state Lifter.step_over + let in_ state = lifter_call_with_id state Lifter.step_in + let out state = lifter_call_with_id state Lifter.step_out + + let branch case id state = + let proc_state = get_proc_state_exn ~cmd_id:id state in + let { lifter_state; _ } = proc_state in + let f () = Lifter.step_branch lifter_state id case in + lifter_call f proc_state state + + let back state = lifter_call_with_id state Lifter.step_back + let continue state = lifter_call_with_id state Lifter.continue + let continue_back state = lifter_call_with_id state Lifter.continue_back + end module Launch_proc = struct - open Verification.SAInterpreter.Logging + let check_init_report id = + let** id = + Option.to_result ~none:"HORROR: No report from initial cont!" id + in + match L.Log_queryer.get_report id with + | None -> Error "HORROR: No report on initial cont_func!" + | Some (_, type_) + when type_ = L.Logging_constants.Content_type.proc_init -> Ok () + | Some _ -> Error "HORROR: Initial report is not a proc_init!" + + (* For the initial step, we should always get a blank Continue *) + let get_cont_func proc_name debug_state = + match Debugger_impl.launch_proc ~proc_name debug_state with + | Continue + { report_id; branch_path = []; new_branch_cases = []; cont_func } -> + let++ () = check_init_report report_id in + cont_func + | _ -> Error "HORROR: Unexpected conf from initial cont!" - let handle_end_of_branch - proc_name - result - prev_id - report_state - cont_func - debug_state = - match prev_id with - | None -> Error "Nothing to run" - | Some prev_id -> - let lifter_state, _ = - let prev_content, _ = - L.Log_queryer.get_report prev_id |> Option.get - in - let exec_data, _ = - build_final_cmd_data prev_content result prev_id [] debug_state - in - Lifter.init_exn ~proc_name ~all_procs:debug_state.proc_names - debug_state.tl_ast debug_state.prog exec_data - in - let proc_state = - let make ext = - make_base_proc_state ~cont_func ~cur_report_id:prev_id - ~top_level_scopes ~lifter_state ~report_state ~ext () - in - let ext = Debugger_impl.init_proc debug_state (make ()) in - make ext - in - proc_state |> update_proc_state prev_id debug_state; - Ok (proc_state, ReachedEnd) - - let init_lifter - ~proc_name - ~report_id - ~cmd_report - ~branch_path - ~new_branch_cases - debug_state = + let init_lifter proc_name debug_state = let { proc_names; tl_ast; prog; _ } = debug_state in - let kind = Exec_map.kind_of_cases new_branch_cases in - let exec_data = - Lift.make_executed_cmd_data kind report_id cmd_report branch_path - in - Lifter.init_exn ~proc_name ~all_procs:proc_names tl_ast prog exec_data + Lifter.init_exn ~proc_name ~all_procs:proc_names tl_ast prog - let handle_continue - proc_name - new_branch_cases - branch_path - cur_report_id - build_proc_state - (cont_func : result_t cont_func_f) - report_state - debug_state = - let id = cur_report_id |> Execute_step.check_cur_report_id in - let aux () = build_proc_state (Some id) (cont_func ~path:[] ()) in - id - |> Execute_step.Handle_continue.get_report_and_check_type - ~log_context:"launch_proc" ~on_proc_init:aux ~on_eob:aux - ~continue:(fun content -> - let cmd_report = - content |> of_yojson_string ConfigReport.of_yojson - in - let lifter_state, handler_result = - init_lifter ~proc_name ~report_id:id ~cmd_report ~branch_path - ~new_branch_cases debug_state + let f proc_name state = + let { debug_state; _ } = state in + let report_state = L.Report_state.clone debug_state.report_state_base in + report_state + |> L.Report_state.with_state (fun () -> + let** cont_func = get_cont_func proc_name debug_state in + let lifter_state, init_lifter' = + init_lifter proc_name debug_state in let proc_state = let make ext = - make_base_proc_state ~cont_func ~cur_report_id:id - ~top_level_scopes ~lifter_state ~report_state ~ext () + make_base_proc_state ~cont_func ~top_level_scopes + ~lifter_state ~report_state ~ext () in let ext = Debugger_impl.init_proc debug_state (make ()) in make ext in - let stop_reason, id = - handler_result - |> Execute_step.handle_lifter_result execute_step - ~default_next_id:id debug_state proc_state - (handle_stop debug_state proc_state id) + let** stop_reason = + Step.lifter_call init_lifter' proc_state state in - let id = id |> Option.get in - update_proc_state id debug_state proc_state; Ok (proc_state, stop_reason)) - - let rec build_proc_state - proc_name - report_state - debug_state - prev_id - cont_func = - let build_proc_state = - build_proc_state proc_name report_state debug_state - in - match cont_func with - | Finished _ -> - Error "HORROR: Shouldn't encounter Finished when debugging!" - | EndOfBranch (result, cont_func) -> - handle_end_of_branch proc_name result prev_id report_state cont_func - debug_state - | Continue { report_id; branch_path; new_branch_cases; cont_func } -> - handle_continue proc_name new_branch_cases branch_path report_id - build_proc_state cont_func report_state debug_state - - let f proc_name debug_state = - let report_state = L.Report_state.clone debug_state.report_state_base in - report_state - |> L.Report_state.with_state (fun () -> - let cont_func = - Debugger_impl.launch_proc ~proc_name debug_state - in - build_proc_state proc_name report_state debug_state None - cont_func) end let launch_proc = Launch_proc.f @@ -837,231 +783,26 @@ struct let debug_state = build_debug_state file_name proc_name in let proc_name = debug_state.main_proc_name in let state = make_state debug_state in - let++ main_proc_state, _ = launch_proc proc_name debug_state in + let++ main_proc_state, _ = launch_proc proc_name state in main_proc_state.report_state |> L.Report_state.activate; Hashtbl.add state.procs proc_name main_proc_state; state end let launch = Launch.f + let step_in = Step.in_ + let step ?(reverse = false) = if reverse then Step.back else Step.over + let step_specific = Step.branch + let step_out = Step.out - 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_in_branch_case = struct - let step_backwards debug_state proc_state = - match - let { lifter_state; cur_report_id; _ } = proc_state in - lifter_state |> Lifter.previous_step cur_report_id - with - | None -> ReachedStart - | Some (prev_id, _) -> - update_proc_state prev_id debug_state proc_state; - Step - - let select_next branch_case nexts = - match branch_case with - | Some branch_case -> - List.find_opt (fun (_, bc) -> bc |> Option.get = branch_case) nexts - |> Option.map fst - | None -> Some (List.hd nexts |> fst) - - let step_forwards prev_id_in_frame branch_case debug_state proc_state = - let next_id = - match - proc_state.lifter_state - |> Lifter.existing_next_steps proc_state.cur_report_id - with - | [] -> None - | nexts -> select_next branch_case nexts - in - match next_id with - | None -> - DL.log (fun m -> m "No next report ID; executing next step"); - execute_step ?branch_case prev_id_in_frame debug_state proc_state - |> fst - | Some id -> - DL.show_report id "Next report ID found; not executing"; - update_proc_state id debug_state proc_state; - Step - - let f - prev_id_in_frame - ?branch_case - ?(reverse = false) - debug_state - proc_state = - let stop_reason = - if reverse then step_backwards debug_state proc_state - else step_forwards prev_id_in_frame branch_case debug_state proc_state - in - if has_hit_breakpoint proc_state then Breakpoint - else if List.length proc_state.errors > 0 then - let () = proc_state.cont_func <- None in - ExecutionError - else stop_reason - end - - let step_in_branch_case = Step_in_branch_case.f - - module Step_case = struct - let get_top_frame state = - match state.frames with - | [] -> failwith "Nothing in call stack, cannot step" - | cur_frame :: _ -> cur_frame - - (* TODO: re-evaluate - I think the lifter should handle this. *) - let step_until_cond - ?(reverse = false) - ?(branch_case : Branch_case.t option) - (cond : frame -> frame -> int -> int -> bool) - (debug_state : debug_state) - (proc_state : proc_state) : stop_reason = - let prev_frame = get_top_frame proc_state in - let prev_stack_depth = List.length proc_state.frames in - let rec aux () = - let prev_id_in_frame = proc_state.cur_report_id in - let stop_reason = - step_in_branch_case ~reverse ?branch_case prev_id_in_frame - debug_state proc_state - in - match stop_reason with - | Step -> - let cur_frame = get_top_frame proc_state in - let cur_stack_depth = List.length proc_state.frames in - if cond prev_frame cur_frame prev_stack_depth cur_stack_depth then - stop_reason - else aux () - | other_stop_reason -> other_stop_reason - in - aux () - - (* If GIL file, step until next cmd in the same frame (like in - regular debuggers) *) - let is_next_gil_step prev_frame cur_frame prev_stack_depth cur_stack_depth - = - cur_frame.source_path = prev_frame.source_path - && cur_frame.name = prev_frame.name - || cur_stack_depth < prev_stack_depth - - (* If target language file, step until the code origin location is - different, indicating an actual step in the target language*) - (* let is_next_tl_step prev_frame cur_frame _ _ = - cur_frame.source_path = prev_frame.source_path - && (cur_frame.start_line <> prev_frame.start_line - || cur_frame.start_column <> prev_frame.start_column - || cur_frame.end_line <> prev_frame.end_line - || cur_frame.end_column <> prev_frame.end_column) *) - let is_next_tl_step _ _ _ _ = true - - let get_cond { source_file; _ } = - if is_gil_file source_file then is_next_gil_step else is_next_tl_step - - let f ?(reverse = false) ?branch_case debug_state proc_state = - let cond = get_cond debug_state in - step_until_cond ~reverse ?branch_case cond debug_state proc_state - end - - let step_case = Step_case.f - - let step_in ?(reverse = false) state = - let proc_state = get_proc_state_exn state in - step_case ~reverse state.debug_state proc_state - - let step ?(reverse = false) state = - let proc_state = get_proc_state_exn state in - step_case ~reverse state.debug_state proc_state - - let step_specific branch_case prev_id state = - let { debug_state; _ } = state in - let** proc_state = state |> get_proc_state ~cmd_id:prev_id in - let id, branch_case = - proc_state.lifter_state |> Lifter.next_gil_step prev_id branch_case - in - let++ () = jump_state_to_id id debug_state proc_state in - proc_state |> step_case ?branch_case debug_state - - let step_out state = - let proc_state = get_proc_state_exn state in - step_case state.debug_state proc_state - - module Run = struct - let log_run current_id state = - DL.log (fun m -> - m - ~json: - [ - ("current_id", L.Report_id.to_yojson current_id); - ("lifter_state", state.lifter_state |> Lifter.dump); - ] - "Debugger.run") - - let run_backwards ~on_step dbg state = - let stop_reason = step_case ~reverse:true dbg state in - match stop_reason with - | Step -> on_step () - | Breakpoint -> Breakpoint - | other_stop_reason -> other_stop_reason - - let run_forwards - ~on_step - ~on_other_reason - current_id - debug_state - proc_state = - let unfinished = - proc_state.lifter_state - |> Lifter.find_unfinished_path ~at_id:current_id - in - match unfinished with - | None -> - DL.log (fun m -> m "Debugger.run: map has no unfinished branches"); - ReachedEnd - | Some (prev_id, branch_case) -> ( - jump_state_to_id prev_id debug_state proc_state |> Result.get_ok; - let stop_reason = step_case ?branch_case debug_state proc_state in - match stop_reason with - | Step -> on_step () - | Breakpoint -> Breakpoint - | _ -> on_other_reason ()) - - let f ?(reverse = false) ?(launch = false) state = - let { debug_state; _ } = state in - let proc_state = get_proc_state_exn state in - let current_id = proc_state.cur_report_id in - log_run current_id proc_state; - let rec aux ?(launch = false) count = - if count > 100 then failwith "Debugger.run: infinite loop?"; - let on_step () = aux count in - let on_other_reason () = aux (count + 1) in - (* We need to check if a breakpoint has been hit if run is called - immediately after launching to prevent missing a breakpoint on the first - line *) - if launch && has_hit_breakpoint proc_state then Breakpoint - else if reverse then run_backwards ~on_step debug_state proc_state - else - run_forwards ~on_step ~on_other_reason current_id debug_state - proc_state - in - aux ~launch 0 - end - - let run = Run.f + let run ?(reverse = false) ?(launch = false) = + ignore launch; + (* TODO *) + if reverse then Step.continue_back else Step.continue let start_proc proc_name state = let { debug_state; procs } = state in - let++ proc_state, stop_reason = launch_proc proc_name debug_state in + let++ proc_state, stop_reason = launch_proc proc_name state in Hashtbl.add procs proc_name proc_state; debug_state.cur_proc_name <- proc_name; stop_reason diff --git a/GillianCore/debugging/debugger/debugger_intf.ml b/GillianCore/debugging/debugger/debugger_intf.ml index c7d95a345..c5e445b8c 100644 --- a/GillianCore/debugging/debugger/debugger_intf.ml +++ b/GillianCore/debugging/debugger/debugger_intf.ml @@ -12,7 +12,7 @@ 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 : ?reverse:bool -> t -> stop_reason + val step_in : t -> stop_reason val step : ?reverse:bool -> t -> stop_reason val step_specific : diff --git a/GillianCore/debugging/lifter/gil_fallback_lifter.ml b/GillianCore/debugging/lifter/gil_fallback_lifter.ml index adf8f5b02..b16695b90 100644 --- a/GillianCore/debugging/lifter/gil_fallback_lifter.ml +++ b/GillianCore/debugging/lifter/gil_fallback_lifter.ml @@ -19,7 +19,7 @@ functor struct let gil_state = ref None - module Gil_lifter = Gil_lifter.Make (PC) (Verifier) (SMemory) + module Gil_lifter = Gil_lifter.Make (SMemory) (PC) (Verifier) module Gil_lifter_with_state = struct module Lifter = Gil_lifter @@ -29,46 +29,26 @@ functor module TLLifter = TLLifter (Gil_lifter_with_state) (Verifier) - type t = { - gil : Gil_lifter.t; [@to_yojson Gil_lifter.dump] - tl : TLLifter.t option; [@to_yojson opt_to_yojson TLLifter.dump] - } - [@@deriving to_yojson] - type memory = SMemory.t type tl_ast = PC.tl_ast type memory_error = SMemory.err_t type cmd_report = Verifier.SAInterpreter.Logging.ConfigReport.t type annot = PC.Annot.t - let init_exn ~proc_name ~all_procs tl_ast prog exec_data = - let gil, gil_result = - Gil_lifter.init_exn ~proc_name ~all_procs tl_ast prog exec_data - in - gil_state := Some gil; - let ret = - match TLLifter.init ~proc_name ~all_procs tl_ast prog exec_data with - | None -> ({ gil; tl = None }, gil_result) - | Some (tl, tl_result) -> ({ gil; tl = Some tl }, tl_result) - in - ret + type t = { + gil : Gil_lifter.t; [@to_yojson Gil_lifter.dump] + tl : TLLifter.t option; [@to_yojson opt_to_yojson TLLifter.dump] + mutable finish_gil_init : (cmd_report executed_cmd_data -> unit) option; + [@to_yojson fun _ -> `Null] + } + [@@deriving to_yojson] - let init ~proc_name ~all_procs tl_ast prog exec_data = - Some (init_exn ~proc_name ~all_procs tl_ast prog exec_data) + type _ Effect.t += + | Step : + (Logging.Report_id.t option * Branch_case.t option * Branch_case.path) + -> cmd_report executed_cmd_data Effect.t let dump = to_yojson - - let handle_cmd prev_id branch_case exec_data { gil; tl } = - let () = - match gil |> Gil_lifter.handle_cmd prev_id branch_case exec_data with - | Stop None -> () - | Stop _ -> failwith "HORROR - Gil_lifter tried to Stop with id!" - | _ -> failwith "HORROR - Gil_lifter didn't give Stop!" - in - match tl with - | None -> Stop None - | Some tl -> tl |> TLLifter.handle_cmd prev_id branch_case exec_data - let get_gil_map state = state.gil |> Gil_lifter.get_gil_map let get_lifted_map state = @@ -80,46 +60,91 @@ functor | None -> failwith "Can't get lifted map!" | Some map -> map - let get_matches_at_id id { gil; tl } = + let get_matches_at_id id { gil; tl; _ } = match tl with | Some tl -> tl |> TLLifter.get_matches_at_id id | None -> gil |> Gil_lifter.get_matches_at_id id - let get_root_id { gil; tl } = + let get_root_id { gil; tl; _ } = match tl with | Some tl -> tl |> TLLifter.get_root_id | None -> gil |> Gil_lifter.get_root_id - let path_of_id id { gil; tl } = - match tl with - | Some tl -> tl |> TLLifter.path_of_id id - | None -> gil |> Gil_lifter.path_of_id id - - let existing_next_steps id { gil; tl } = - match tl with - | Some tl -> tl |> TLLifter.existing_next_steps id - | None -> gil |> Gil_lifter.existing_next_steps id - - let next_gil_step id case { gil; tl } = - match tl with - | Some tl -> tl |> TLLifter.next_gil_step id case - | None -> gil |> Gil_lifter.next_gil_step id case + let memory_error_to_exception_info = TLLifter.memory_error_to_exception_info + let add_variables = TLLifter.add_variables - let previous_step id { gil; tl } = - match tl with - | Some tl -> tl |> TLLifter.previous_step id - | None -> gil |> Gil_lifter.previous_step id + let intercept_effect f state () = + let open Effect.Deep in + try_with f () + { + effc = + (fun (type a) (eff : a Effect.t) -> + match eff with + | TLLifter.Step (id, case, _ as s) -> + Some + (fun (k : (a, _) continuation) -> + let exec_data = Effect.perform (Step s) in + let () = + match state.finish_gil_init with + | Some finish_gil -> + let () = state.finish_gil_init <- None in + finish_gil exec_data + | None -> + Gil_lifter.handle_cmd (Option.get id) case exec_data + state.gil + in + Effect.Deep.continue k exec_data) + | Gil_lifter.Step s -> + Some + (fun (k : (a, _) continuation) -> + let exec_data = Effect.perform (Step s) in + Effect.Deep.continue k exec_data) + + | _ -> None); + } + + let defer_with_id tl_f gil_f state id = + let f = match state.tl with + | Some tl -> fun () -> tl_f tl id + | None -> fun () -> gil_f state.gil id + in + intercept_effect f state () - let select_next_path case id { gil; tl } = - match tl with - | Some tl -> tl |> TLLifter.select_next_path case id - | None -> gil |> Gil_lifter.select_next_path case id + let step_over = defer_with_id TLLifter.step_in Gil_lifter.step_in + let step_in = defer_with_id TLLifter.step_in Gil_lifter.step_in + let step_out = defer_with_id TLLifter.step_out Gil_lifter.step_out + let step_back state = defer_with_id TLLifter.step_back Gil_lifter.step_back state - let find_unfinished_path ?at_id { gil; tl } = - match tl with - | Some tl -> tl |> TLLifter.find_unfinished_path ?at_id - | None -> gil |> Gil_lifter.find_unfinished_path ?at_id + let step_branch state id case = + let f = match state.tl with + | Some tl -> fun () -> TLLifter.step_branch tl id case + | None -> fun () -> Gil_lifter.step_branch state.gil id case + in + intercept_effect f state () + + let continue = defer_with_id TLLifter.continue Gil_lifter.continue + + let continue_back = + defer_with_id TLLifter.continue_back Gil_lifter.continue_back + + let init_exn ~proc_name ~all_procs tl_ast prog = + let gil, finish_gil_init = Gil_lifter.init_manual proc_name all_procs in + let () = gil_state := Some gil in + let state, finish_init = + match TLLifter.init ~proc_name ~all_procs tl_ast prog with + | None -> + let finish_gil_init () = finish_gil_init None () in + ({ gil; tl = None; finish_gil_init = None }, finish_gil_init) + | Some (tl, finish_tl_init) -> + let finish_gil_init exec_data = + finish_gil_init (Some exec_data) () |> ignore + in + ( { gil; tl = Some tl; finish_gil_init = Some finish_gil_init }, + finish_tl_init ) + in + let finish_init = intercept_effect finish_init state in + (state, finish_init) - let memory_error_to_exception_info = TLLifter.memory_error_to_exception_info - let add_variables = TLLifter.add_variables + let init ~proc_name ~all_procs tl_ast prog = + Some (init_exn ~proc_name ~all_procs tl_ast prog) end diff --git a/GillianCore/debugging/lifter/gil_lifter.ml b/GillianCore/debugging/lifter/gil_lifter.ml index 5a762f736..4beb84b29 100644 --- a/GillianCore/debugging/lifter/gil_lifter.ml +++ b/GillianCore/debugging/lifter/gil_lifter.ml @@ -2,22 +2,12 @@ module L = Logging module DL = Debugger_log open Lifter -module type S = sig - include Lifter.S +include Gil_lifter_intf - val should_skip_cmd : cmd_report Lifter.executed_cmd_data -> t -> bool -end - -module Make +module Make : Make = functor + (SMemory : SMemory.S) (PC : ParserAndCompiler.S) - (Verifier : Verifier.S with type annot = PC.Annot.t) - (SMemory : SMemory.S) : - S - with type memory = SMemory.t - and type tl_ast = PC.tl_ast - and type memory_error = SMemory.err_t - and type cmd_report = Verifier.SAInterpreter.Logging.ConfigReport.t - and type annot = PC.Annot.t = struct + (Verifier : Verifier.S with type annot = PC.Annot.t) -> struct open Exec_map module Annot = PC.Annot @@ -40,11 +30,10 @@ module Make [@@deriving to_yojson] type t = { - map : map; + mutable map : map; root_proc : string; all_procs : string list; id_map : (L.Report_id.t, map) Hashtbl.t; [@to_yojson fun _ -> `Null] - mutable to_exec : (L.Report_id.t * Branch_case.t option) list; } [@@deriving to_yojson] @@ -57,6 +46,11 @@ module Make type exec_data = cmd_report executed_cmd_data [@@deriving yojson] + type _ Effect.t += + | Step : + (Logging.Report_id.t option * Branch_case.t option * Branch_case.path) + -> cmd_report executed_cmd_data Effect.t + let dump = to_yojson let get_proc_name ({ cmd_report; _ } : exec_data) = @@ -69,7 +63,7 @@ module Make ?(submap = NoSubmap) ~parent id_map - { kind; id; matches; errors; cmd_report : cmd_report; branch_path } + { 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 @@ -107,12 +101,7 @@ module Make ((Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data }) as map) -> Ok (map, data.branch_path) - let at_id_opt id state = - match at_id_result id state with - | Ok (map, branch_path) -> Some (map, branch_path) - | Error _ -> None - - let at_id id state = + let at_id_exn id state = match at_id_result id state with | Ok (map, branch_path) -> (map, branch_path) | Error s -> @@ -121,19 +110,11 @@ module Make [ ("id", L.Report_id.to_yojson id); ("state", dump state) ]) ("at_id: " ^ s) - let init_exn ~proc_name ~all_procs _ _ exec_data = - let id_map = Hashtbl.create 1 in - let map = new_cmd id_map exec_data ~parent:None () in - ({ map; root_proc = proc_name; all_procs; id_map; to_exec = [] }, Stop None) - - let init ~proc_name ~all_procs tl_ast prog exec_data = - Some (init_exn ~proc_name ~all_procs tl_ast prog exec_data) - let should_skip_cmd (exec_data : cmd_report executed_cmd_data) state : bool = let proc_name = get_proc_name exec_data in not (List.mem proc_name state.all_procs) - let handle_cmd prev_id branch_case exec_data state = + 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 branch_case = @@ -159,12 +140,13 @@ module Make | None -> failwith (Fmt.str "couldn't find prev_id %a!" L.Report_id.pp prev_id) in - let () = + let new_cmd = match map with | Cmd cmd when cmd.next = Nothing -> let parent = Some (map, None) in let new_cmd = new_cmd ~parent () in - cmd.next <- new_cmd + let () = cmd.next <- new_cmd in + new_cmd | Cmd _ -> failwith "cmd.next not Nothing!" | BranchCmd { nexts; _ } -> ( match branch_case with @@ -175,12 +157,17 @@ module Make | Some ((), Nothing) -> let parent = Some (map, Some case) in let new_cmd = new_cmd ~parent () in - Hashtbl.replace nexts case ((), new_cmd) + 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" in - Stop None + 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 @@ -201,7 +188,7 @@ module Make failwith "get_lifted_map not implemented for GIL lifter" let get_matches_at_id id state = - match state |> at_id id |> fst with + match state |> at_id_exn id |> fst with | Nothing -> DL.failwith (fun () -> @@ -216,103 +203,13 @@ module Make | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> Some data.id - let path_of_id id state = state |> at_id id |> snd - - let existing_next_steps id state = - match state |> at_id_opt id with - | None -> [] - | Some (map, _) -> ( - match map with - | Nothing -> failwith "existing_next_steps: map is Nothing!" - | Cmd { next = Nothing; _ } | FinalCmd _ -> [] - | Cmd { next; _ } -> - let id = get_id next in - [ (id, None) ] - | BranchCmd { nexts; _ } -> - let nexts = - Hashtbl.fold - (fun case (_, next) acc -> - match get_id_opt next with - | None -> acc - | Some id -> (id, Some case) :: acc) - nexts [] - in - List.rev nexts) + let path_of_id id state = state |> at_id_exn id |> snd - let next_gil_step id (case : Exec_map.Packaged.branch_case option) _ = - let case = - Option.map - (fun (_, json) -> json |> Branch_case.of_yojson |> Result.get_ok) - case - in - (id, case) - - let previous_step id state = - match state |> at_id id |> fst with - | Nothing -> failwith "HORROR - map is Nothing!" - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> ( - match data.parent with - | None -> None - | Some (Nothing, _) -> failwith "HORROR - parent is Nothing!" - | Some - ((Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data }), case) - -> - let case = case |> Option.map Exec_map.Packaged.package_gil_case in - Some (data.id, case)) - - let select_next_path case id state = - let map, path = state |> at_id id in - let failwith s = - DL.failwith - (fun () -> - [ - ("id", L.Report_id.to_yojson id); - ("state", dump state); - ("case", opt_to_yojson branch_case_to_yojson case); - ]) - ("select_next_path: " ^ s) - in - match (map, case) with - | Nothing, _ -> failwith "no next path (nothing)" - | FinalCmd _, _ -> failwith "no next path (final)" - | Cmd _, Some _ -> failwith "tried to select case for non-branch cmd" - | Cmd _, None -> path - | BranchCmd { nexts; _ }, None -> - Hashtbl.find_map (fun case _ -> Some (case :: path)) nexts |> Option.get - | BranchCmd { nexts; _ }, Some case -> ( - match Hashtbl.find_opt nexts case with - | None -> failwith "case not found" - | Some _ -> case :: path) - - let find_unfinished_path ?at_id state = - let rec aux = function - | Nothing -> - DL.failwith - (fun () -> - [ - ("state", dump state); - ("at_id", opt_to_yojson L.Report_id.to_yojson at_id); - ]) - "find_unfinished_path: started at Nothing" - | Cmd { data = { id; _ }; next = Nothing } -> Some (id, None) - | Cmd { next; _ } -> aux next - | BranchCmd { nexts; data = { id; _ } } -> ( - match - Hashtbl.find_map - (fun case (_, next) -> - if next = Nothing then Some (id, Some case) else None) - nexts - with - | None -> Hashtbl.find_map (fun _ (_, next) -> aux next) nexts - | result -> result) - | FinalCmd _ -> None - in - let map = - match at_id with - | None -> state.map - | Some id -> Hashtbl.find state.id_map id - in - aux map + 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 memory_error_to_exception_info { error; _ } : exception_info = { id = Fmt.to_to_string SMemory.pp_err error; description = None } @@ -342,4 +239,139 @@ module Make let () = Hashtbl.replace variables store_id store_vars in let () = Hashtbl.replace variables memory_id memory_vars in scopes + + let select_case nexts = + let case, _ = + Hashtbl.fold + (fun case (_, map) acc -> + match (map, acc) with + | _, (_, true) -> acc + | Nothing, (_, false) -> (Some case, true) + | _, (None, false) -> (Some case, false) + | _ -> acc) + nexts (None, false) + 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 _ -> 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 -> + let case = select_case nexts in + Either.Right (Some case) + | BranchCmd { nexts; _ }, Some case -> ( + match Hashtbl.find_opt nexts case with + | None -> failwith "case not found" + | Some (_, Nothing) -> Either.Right (Some case) + | Some (_, next) -> Either.Left next) + + let request_next state id case = + let path = path_of_id id state in + let exec_data = Effect.perform (Step (Some id, case, path)) in + consume_cmd id case exec_data state + + let step state id case = + let next = + 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 step_branch state id case = + let case = + Option.map + (fun (_, json) -> json |> Branch_case.of_yojson |> Result.get_ok) + case + in + let id = + match step state id case with + | Either.Left nexts -> nexts |> List.hd |> fst + | Either.Right end_id -> end_id + in + (id, Debugger_utils.Step) + + 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 continue state id = + let open Utils.Syntaxes.Option in + let rec aux stack ends = + match stack with + | [] -> List.rev ends + | (id, case) :: rest -> ( + match step state id case with + | Either.Left nexts -> aux (nexts @ rest) ends + | Either.Right end_id -> aux rest (end_id :: ends)) + 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; _ } -> + let stack = + nexts |> Hashtbl.to_seq + |> Seq.map (fun (case, _) -> (id, Some case)) + |> List.of_seq + in + (None, stack) + in + let- () = end_ in + let ends = aux stack [] in + List.hd ends + in + (end_, Debugger_utils.Step) + + 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) + + 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 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) + in + (state, finish_init) + + let init_exn ~proc_name ~all_procs _ _ = + let state, finish = init_manual proc_name all_procs in + (state, finish None) + + let init ~proc_name ~all_procs tl_ast prog = + Some (init_exn ~proc_name ~all_procs tl_ast prog) end diff --git a/GillianCore/debugging/lifter/gil_lifter.mli b/GillianCore/debugging/lifter/gil_lifter.mli index 3a3d614de..463050f0c 100644 --- a/GillianCore/debugging/lifter/gil_lifter.mli +++ b/GillianCore/debugging/lifter/gil_lifter.mli @@ -1,18 +1,4 @@ (** A basic "GIL-to-GIL" lifter implementation. *) -module type S = sig - include Lifter.S - - val should_skip_cmd : cmd_report Lifter.executed_cmd_data -> t -> bool -end - -module Make - (PC : ParserAndCompiler.S) - (V : Verifier.S with type annot = PC.Annot.t) - (SMemory : SMemory.S) : - S - with type memory = SMemory.t - and type tl_ast = PC.tl_ast - and type memory_error = SMemory.err_t - and type cmd_report = V.SAInterpreter.Logging.ConfigReport.t - and type annot = PC.Annot.t +(** @inline *) +include Gil_lifter_intf.Intf diff --git a/GillianCore/debugging/lifter/gil_lifter_intf.ml b/GillianCore/debugging/lifter/gil_lifter_intf.ml new file mode 100644 index 000000000..3998252e1 --- /dev/null +++ b/GillianCore/debugging/lifter/gil_lifter_intf.ml @@ -0,0 +1,45 @@ +module type S = sig + include Lifter.S + + (** A version of [init] that allows manually supplying exec_data instead of triggering + the Step effect - this is used when Gil is not the primary lifter. *) + val init_manual : + string -> + string list -> + t + * (cmd_report Lifter.executed_cmd_data option -> + unit -> + Logging.Report_id.t * stop_reason) + + val handle_cmd : + Logging.Report_id.t -> + Branch_case.t option -> + cmd_report Lifter.executed_cmd_data -> + t -> + unit + + val path_of_id : Logging.Report_id.t -> t -> Branch_case.path + + val should_skip_cmd : cmd_report Lifter.executed_cmd_data -> t -> bool + + val cases_at_id : Logging.Report_id.t -> t -> Branch_case.t list +end + +module type Make = functor + (SMemory : SMemory.S) + (PC : ParserAndCompiler.S) + (Verifier : Verifier.S with type annot = PC.Annot.t) -> + S + with type memory = SMemory.t + and type tl_ast = PC.tl_ast + and type memory_error = SMemory.err_t + and type cmd_report = Verifier.SAInterpreter.Logging.ConfigReport.t + and type annot = PC.Annot.t + +module type Intf = sig + module type S = S + + module type Make = Make + + module Make : Make +end \ No newline at end of file diff --git a/GillianCore/debugging/lifter/lifter.ml b/GillianCore/debugging/lifter/lifter.ml index 9d8d6a6ca..63eee4c39 100644 --- a/GillianCore/debugging/lifter/lifter.ml +++ b/GillianCore/debugging/lifter/lifter.ml @@ -2,10 +2,11 @@ module L = Logging include Lifter_intf let make_executed_cmd_data + ?(is_breakpoint = false) kind id cmd_report ?(matches = []) ?(errors = []) branch_path = - { kind; id; cmd_report; matches; errors; branch_path } + { is_breakpoint; 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 d97148d9a..982d3a0aa 100644 --- a/GillianCore/debugging/lifter/lifter_intf.ml +++ b/GillianCore/debugging/lifter/lifter_intf.ml @@ -10,6 +10,7 @@ module Types = struct } type 'cmd_report executed_cmd_data = { + is_breakpoint : bool; kind : (Branch_case.t, unit) Exec_map.cmd_kind; id : Logging.Report_id.t; cmd_report : 'cmd_report; @@ -37,6 +38,11 @@ module type S = sig type cmd_report type annot + type _ Effect.t += + | Step : + (Logging.Report_id.t option * Branch_case.t option * Branch_case.path) + -> cmd_report executed_cmd_data Effect.t + (** Given a proc name, a tl_ast, and the data from the first executed GIL command, initialise the lifter's state and handle the first command. @@ -46,8 +52,7 @@ module type S = sig all_procs:string list -> tl_ast option -> (annot, int) Prog.t -> - cmd_report executed_cmd_data -> - (t * handle_cmd_result) option + (t * (unit -> Logging.Report_id.t * stop_reason)) option (** Exception-raising version of {!init}. *) val init_exn : @@ -55,21 +60,28 @@ module type S = sig all_procs:string list -> tl_ast option -> (annot, int) Prog.t -> - cmd_report executed_cmd_data -> - t * handle_cmd_result + t * (unit -> Logging.Report_id.t * stop_reason) (** Gives a JSON representation of the lifter's state. Used for debugging problems with the lifter.*) val dump : t -> Yojson.Safe.t - (** Handles the execution result of a GIL command. *) - val handle_cmd : - Logging.Report_id.t -> - Branch_case.t option -> - cmd_report executed_cmd_data -> + val step_over : t -> Logging.Report_id.t -> Logging.Report_id.t * stop_reason + val step_in : t -> Logging.Report_id.t -> Logging.Report_id.t * stop_reason + val step_out : t -> Logging.Report_id.t -> Logging.Report_id.t * stop_reason + val step_back : t -> Logging.Report_id.t -> Logging.Report_id.t * stop_reason + + val step_branch : t -> - handle_cmd_result + Logging.Report_id.t -> + Exec_map.Packaged.branch_case option -> + Logging.Report_id.t * stop_reason + + val continue : t -> Logging.Report_id.t -> Logging.Report_id.t * stop_reason + + val continue_back : + t -> Logging.Report_id.t -> Logging.Report_id.t * stop_reason (** Gets the non-lifted execution map of GIL commands. @@ -91,50 +103,6 @@ module type S = sig (** Gives the id of the root (first) command in the execution map. *) val get_root_id : t -> Logging.Report_id.t option - (** Gives the path of (GIL) branch cases that lead to the specified command. *) - val path_of_id : Logging.Report_id.t -> t -> Branch_case.path - - (** Gets a list of ID/branch-case pairs that correspond to any commands that - directly succeed the specified command. *) - val existing_next_steps : - Logging.Report_id.t -> - t -> - (Logging.Report_id.t * Branch_case.t option) list - - (** Translates a command ID and (packaged) TL branch case to the command ID - and GIL branch case necessary to step forward. *) - val next_gil_step : - Logging.Report_id.t -> - Exec_map.Packaged.branch_case option -> - t -> - Logging.Report_id.t * Branch_case.t option - - (** If the given command has a previous command, gives its ID, and - the TL branch case that connects them (if applicable). *) - val previous_step : - Logging.Report_id.t -> - t -> - (Logging.Report_id.t * Exec_map.Packaged.branch_case option) option - - (** Gives a branch path that steps forward from the given command. - - If the given command branches, the desired branch case can be specified. *) - val select_next_path : - Branch_case.t option -> Logging.Report_id.t -> t -> Branch_case.path - - (** Gives a branch path under the specified command (or the root command, if - not specified) that hasn't yet been fully explored. - - The order in which unfinished branches are given in later calls is - unimportant. - - Returns [None] if all paths under the specified command have been fully - explored. *) - val find_unfinished_path : - ?at_id:Logging.Report_id.t -> - t -> - (Logging.Report_id.t * Branch_case.t option) option - val memory_error_to_exception_info : (memory_error, annot, tl_ast) memory_error_info -> exception_info @@ -157,6 +125,7 @@ module type Intf = sig module type S = S val make_executed_cmd_data : + ?is_breakpoint:bool -> (Branch_case.t, unit) Exec_map.cmd_kind -> Logging.Report_id.t -> 'cmd_report -> diff --git a/GillianCore/debugging/log/debugger_log.ml b/GillianCore/debugging/log/debugger_log.ml index 6952e591d..f526233c7 100644 --- a/GillianCore/debugging/log/debugger_log.ml +++ b/GillianCore/debugging/log/debugger_log.ml @@ -127,5 +127,11 @@ let set_rpc_command_handler rpc ?name module_ f = let err_json = err_json backtrace in log_async (fun m -> m ~json:err_json "[Error] Not found");%lwt raise Not_found + | (Effect.Unhandled _) as e -> + let backtrace = Printexc.get_backtrace () in + let err_json = err_json backtrace in + let s = Printexc.to_string e in + log_async (fun m -> m ~json:err_json "[Error] Unhandled exception\n%s" s);%lwt + raise e in Debug_rpc.set_command_handler rpc module_ f diff --git a/GillianCore/debugging/utils/exec_map.ml b/GillianCore/debugging/utils/exec_map.ml index 9878985f2..51db2d762 100644 --- a/GillianCore/debugging/utils/exec_map.ml +++ b/GillianCore/debugging/utils/exec_map.ml @@ -127,6 +127,15 @@ let at_path ?(stop_at = EndOfPath) path map = 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" + (** Exception-raising equivalent to [at_path] *) let at_path_exn ?(stop_at = EndOfPath) path map = match at_path ~stop_at path map with diff --git a/GillianCore/engine/general_semantics/general/g_interpreter.ml b/GillianCore/engine/general_semantics/general/g_interpreter.ml index 10046a946..384927858 100644 --- a/GillianCore/engine/general_semantics/general/g_interpreter.ml +++ b/GillianCore/engine/general_semantics/general/g_interpreter.ml @@ -1,5 +1,6 @@ open Literal open Branch_case +open Syntaxes.Result module L = Logging module DL = Debugger_log include G_interpreter_intf @@ -54,6 +55,7 @@ struct error_state : state_t; errors : err_t list; branch_path : branch_path; + prev_cmd_report_id : Logging.Report_id.t option; } [@@deriving yojson] @@ -77,6 +79,7 @@ struct ret_val : state_vt; final_state : state_t; branch_path : branch_path; + prev_cmd_report_id : Logging.Report_id.t option; } [@@deriving yojson] @@ -90,6 +93,7 @@ struct loop_ids : string list; branch_count : int; branch_path : branch_path; + prev_cmd_report_id : Logging.Report_id.t option; } [@@deriving yojson] @@ -130,6 +134,12 @@ struct branch_case; } + let get_prev_cmd_id = function + | ConfErr { prev_cmd_report_id; _ } -> prev_cmd_report_id + | ConfFinish { prev_cmd_report_id; _ } -> prev_cmd_report_id + | ConfSusp { prev_cmd_report_id; _ } -> prev_cmd_report_id + | ConfCont { prev_cmd_report_id; _ } -> prev_cmd_report_id + let get_branch_case = function | ConfCont { branch_case; _ } -> branch_case | _ -> None @@ -145,7 +155,13 @@ struct type conf_t = BConfErr of err_t list | BConfCont of State.t type result_t = (State.t, State.vt, err_t) Exec_res.t [@@deriving yojson] - type 'result cont_func_f = ?path:Branch_case.path -> unit -> 'result cont_func + type conf_selector = + | Path of Branch_case.path + | IdCase of L.Report_id.t * Branch_case.t option + [@@deriving to_yojson] + + type 'result cont_func_f = + ?selector:conf_selector -> unit -> 'result cont_func and 'result cont_func = | Finished of 'result list @@ -657,6 +673,7 @@ struct eval_expr : Expr.t -> Val.t; loop_action : loop_action; branch_path : branch_path; + prev_cmd_report_id : L.Report_id.t option; } module Do_eval = struct @@ -725,7 +742,7 @@ struct b_counter has_branched spec_name : CConf.t = - let { i; cs; branch_path; _ } = eval_state in + let { i; cs; branch_path; prev_cmd_report_id; _ } = eval_state in let process_ret_cont new_j = process_ret_cont new_j eval_state ix ret_state fl b_counter has_branched @@ -757,6 +774,7 @@ struct spec_name)); ]; branch_path; + prev_cmd_report_id; } let symb_exec_proc x pid v_args j params args eval_state () = @@ -777,7 +795,9 @@ struct ] let exec_with_spec spec x j args pid subst symb_exec_proc eval_state = - let { state; i; b_counter; cs; branch_path; _ } = eval_state in + let { state; i; b_counter; cs; branch_path; prev_cmd_report_id; _ } = + eval_state + in let process_ret = process_ret pid j eval_state in match !symb_exec_next with | true -> @@ -814,6 +834,7 @@ struct spec.data.spec_name)); ]; branch_path; + prev_cmd_report_id; }; ] else @@ -848,6 +869,7 @@ struct error_state = state; errors; branch_path; + prev_cmd_report_id; }; ] in @@ -864,6 +886,7 @@ struct prev; prev_loop_ids; branch_path; + prev_cmd_report_id; _; } = eval_state @@ -882,6 +905,7 @@ struct next_idx = i; branch_path; branch_count = b_counter; + prev_cmd_report_id; }; ]) else symb_exec_proc () @@ -961,6 +985,7 @@ struct prev_loop_ids; make_confcont; eval_expr; + prev_cmd_report_id; _; } = state @@ -1081,6 +1106,7 @@ struct error_state = state; errors = List.map (fun x -> Exec_err.EState x) errs; branch_path; + prev_cmd_report_id; }; ]) else @@ -1093,6 +1119,7 @@ struct error_state = state; errors = List.map (fun x -> Exec_err.EState x) errs; branch_path; + prev_cmd_report_id; }; ] in @@ -1113,6 +1140,7 @@ struct loop_action; branch_path; annot; + prev_cmd_report_id; _; } = state @@ -1157,6 +1185,7 @@ struct error_state = state; errors; branch_path; + prev_cmd_report_id; }) frames_and_states | _ -> @@ -1193,6 +1222,7 @@ struct error_state = state; errors; branch_path; + prev_cmd_report_id; }; ] in @@ -1375,6 +1405,7 @@ struct state; iframes; b_counter; + prev_cmd_report_id; _; } = eval_state @@ -1397,6 +1428,7 @@ struct ret_val = v_ret; final_state = state; branch_path; + prev_cmd_report_id; }; ] | ( Some v_ret, @@ -1442,6 +1474,7 @@ struct state; iframes; b_counter; + prev_cmd_report_id; _; } = eval_state @@ -1460,6 +1493,7 @@ struct ret_val = v_ret; final_state = state; branch_path : branch_path; + prev_cmd_report_id; }; ] | ( Some v_ret, @@ -1652,9 +1686,8 @@ struct L.Parent.set report_id); let branch_path = List_utils.cons_opt branch_case branch_path in - let make_confcont = - CConf.make_cont ?prev_cmd_report_id:!report_id_ref ~branch_path - in + let prev_cmd_report_id = !report_id_ref in + let make_confcont = CConf.make_cont ?prev_cmd_report_id ~branch_path in DL.log (fun m -> m ~json:[ ("path", branch_path_to_yojson branch_path) ] @@ -1677,6 +1710,7 @@ struct eval_expr; loop_action; branch_path; + prev_cmd_report_id; } in @@ -1705,6 +1739,7 @@ struct | _, (_, LAction _) -> simplify state | _ -> [ state ] in + let prev_cmd_report_id = !report_id_ref in List.concat_map (fun state -> try @@ -1720,6 +1755,7 @@ struct error_state; errors; branch_path = List_utils.cons_opt branch_case branch_path; + prev_cmd_report_id; }; ] | State.Internal_State_Error (errs, error_state) -> @@ -1732,6 +1768,7 @@ struct error_state; errors = List.map (fun x -> Exec_err.EState x) errs; branch_path = List_utils.cons_opt branch_case branch_path; + prev_cmd_report_id; }; ]) states @@ -1750,10 +1787,12 @@ struct module Evaluate_cmd_step = struct open CConf + type results = (L.Report_id.t option * branch_path * result_t) list + type 'a f = CConf.t list -> - branch_path option -> - (branch_path * result_t) list -> + conf_selector option -> + results -> 'a cont_func type 'a eval_step = @@ -1771,12 +1810,13 @@ struct hold_results : 'a list; on_hold : (CConf.t * string) list; branch_path : branch_path option; - results : (branch_path * result_t) list; + results : results; conf : CConf.t option; rest_confs : CConf.t list; parent_id_ref : L.Report_id.t option ref; f : 'a f; eval_step : 'a eval_step; + selector : conf_selector option; } let log_confcont parent_id_ref is_first = function @@ -1842,6 +1882,7 @@ struct error_state = state; errors; branch_path; + _; } :: _ -> CmdResult.log_result @@ -1872,16 +1913,24 @@ struct } else cont_func () - let select_conf branch_path confs = - match branch_path with + let select_conf selector confs = + match selector with | None -> DL.log (fun m -> - m "HORROR: branch_path shouldn't be None when debugging!"); + m "select_conf - HORROR: selector shouldn't be None when debugging!"); List_utils.hd_tl confs - | Some branch_path -> - confs - |> List_utils.pop_where (fun conf -> - CConf.get_branch_path conf = branch_path) + | Some selector -> + let f = + match selector with + | Path path -> fun conf -> CConf.get_branch_path conf = path + | IdCase (id, case) -> ( + fun conf -> + let case' = CConf.get_branch_case conf in + match CConf.get_prev_cmd_id conf with + | Some id' when id = id' && case = case' -> true + | _ -> false) + in + List_utils.pop_where f confs let debug_log conf rest_confs = DL.log (fun m -> @@ -1898,41 +1947,54 @@ struct ] "G_interpreter.evaluate_cmd_step: Evaluating conf") - let end_of_branch ?branch_case results eval_step_state = - let { conf; rest_confs; branch_path; ret_fun; f; _ } = eval_step_state in - match branch_path with - | None -> failwith "HORROR: branch_path shouldn't be None when debugging!" - | Some branch_path -> ( - match results |> List.assoc_opt branch_path with - | None -> - DL.failwith - (fun () -> - let result_jsons = - results - |> List.map (fun (path, result) -> - `Assoc - [ - ("path", branch_path_to_yojson path); - ("result", result_t_to_yojson result); - ]) - in - let conf_json = - match conf with - | None -> `Null - | Some conf -> CConf.to_yojson conf - in - [ - ("branch_path", branch_path_to_yojson branch_path); - ( "branch_case", - opt_to_yojson branch_case_to_yojson branch_case ); - ("results", `List result_jsons); - ("conf", conf_json); - ("rest_confs", `List (List.map CConf.to_yojson rest_confs)); - ]) - "No result for branch path!" - | Some result -> - EndOfBranch - (ret_fun result, fun ?path () -> f rest_confs path results)) + let find_result selector results = + let* pred = match selector with + | None -> Error "find_result - HORROR: selector shouldn't be None when debugging!" + | Some (IdCase (id, _)) -> + Ok (fun (id', _, result) -> + match id' with + | Some id' when id' = id -> Some result + | _ -> None) + | Some (Path path) -> + Ok (fun (_, path', result) -> if path = path' then Some result else None) + in + match List.find_map pred results with + | Some result -> Ok result + | None -> Error "No result for selector!" + + + let end_of_branch results eval_step_state = + let { conf; rest_confs; ret_fun; f; selector; _ } = eval_step_state in + match find_result selector results with + | Error msg -> + DL.failwith + (fun () -> + let result_jsons = + results + |> List.map (fun (id, path, result) -> + `Assoc + [ + ("id", opt_to_yojson L.Report_id.to_yojson id); + ("path", branch_path_to_yojson path); + ("result", result_t_to_yojson result); + ]) + in + let conf_json = + match conf with + | None -> `Null + | Some conf -> CConf.to_yojson conf + in + [ + ("selector", opt_to_yojson conf_selector_to_yojson selector); + ("results", `List result_jsons); + ("conf", conf_json); + ("rest_confs", `List (List.map CConf.to_yojson rest_confs)); + ]) + msg + | Ok result -> + EndOfBranch + ( ret_fun result, + fun ?selector () -> f rest_confs selector results ) module Handle_conf = struct let none eval_step_state = @@ -1954,7 +2016,7 @@ struct | [] when !Config.debug -> end_of_branch results eval_step_state | [] -> let results = - List.map (fun (_, result) -> ret_fun result) results + List.map (fun (_, _, result) -> ret_fun result) results in let results = hold_results @ results in if not retry then Finished results @@ -1966,8 +2028,9 @@ struct if Hashtbl.mem prog.specs pid then Some conf else None) on_hold in - continue_or_pause hold_confs (fun ?path () -> - eval_step ret_fun false prog results [] hold_confs path [])) + continue_or_pause hold_confs (fun ?selector () -> + eval_step ret_fun false prog results [] hold_confs selector + [])) eval_step_state let cont (cconf : CConf.cont) eval_step_state = @@ -1995,7 +2058,7 @@ struct b_counter parent_id_ref branch_path branch_case in continue_or_pause ~new_confs:true next_confs - (fun ?path () -> f (next_confs @ rest_confs) path results) + (fun ?selector () -> f (next_confs @ rest_confs) selector results) eval_step_state let max_branch (cconf : CConf.cont) eval_step_state = @@ -2026,33 +2089,35 @@ struct parent_id_ref := Some report_id; L.Parent.set report_id); continue_or_pause [] - (fun ?path () -> f rest_confs path results) + (fun ?selector () -> f rest_confs selector results) eval_step_state let err (cconf : CConf.err) eval_step_state = let { results; rest_confs; f; _ } = eval_step_state in - let { callstack; proc_idx; error_state; errors; branch_path } = cconf in + let { callstack; proc_idx; error_state; errors; branch_path; _ } = + cconf + in let proc = Call_stack.get_cur_proc_id callstack in let result = Exec_res.RFail { proc; proc_idx; error_state; errors } in - let results = (branch_path, result) :: results in + let results = (cconf.prev_cmd_report_id, branch_path, result) :: results in if !Config.debug then end_of_branch results eval_step_state else continue_or_pause rest_confs - (fun ?path () -> f rest_confs path results) + (fun ?selector () -> f rest_confs selector results) eval_step_state let finish (cconf : CConf.finish) eval_step_state = let { results; rest_confs; f; _ } = eval_step_state in - let { flag; ret_val; final_state; branch_path } = cconf in + let { flag; ret_val; final_state; branch_path; _ } = cconf in let result = Exec_res.RSucc { flag; ret_val; final_state; last_report = L.Parent.get () } in - let results = (branch_path, result) :: results in + let results = (cconf.prev_cmd_report_id, branch_path, result) :: results in if !Config.debug then end_of_branch results eval_step_state else continue_or_pause rest_confs - (fun ?path () -> f rest_confs path results) + (fun ?selector () -> f rest_confs selector results) eval_step_state let susp (cconf : CConf.susp) eval_step_state = @@ -2092,9 +2157,9 @@ struct verbose (fun m -> m "Suspending a computation that was trying to call %s" fid)); continue_or_pause [] - (fun ?path () -> + (fun ?selector () -> eval_step ret_fun retry prog hold_results ((conf, fid) :: on_hold) - rest_confs path results) + rest_confs selector results) eval_step_state end @@ -2105,15 +2170,16 @@ struct (hold_results : 'a list) (on_hold : (CConf.t * string) list) (confs : CConf.t list) - (branch_path : branch_path option) - (results : (branch_path * result_t) list) : 'a cont_func = + (selector : conf_selector option) + (results : results) : 'a cont_func = let f = eval_step ret_fun retry prog hold_results on_hold in let parent_id_ref = ref None in Fun.protect ~finally:(fun () -> L.Parent.release !parent_id_ref) (fun () -> - let conf, rest_confs = select_conf branch_path confs in + let conf, rest_confs = select_conf selector confs in + let branch_path = Option.map get_branch_path conf in let eval_step_state = { ret_fun; @@ -2128,6 +2194,7 @@ struct parent_id_ref; f; eval_step; + selector; } in debug_log conf rest_confs; @@ -2143,7 +2210,7 @@ struct | Some (ConfSusp c) when retry -> Handle_conf.susp c eval_step_state | Some _ -> continue_or_pause rest_confs - (fun ?path () -> f rest_confs path results) + (fun ?selector () -> f rest_confs selector results) eval_step_state) end @@ -2225,8 +2292,8 @@ struct branch_path = []; new_branch_cases = []; cont_func = - (fun ?path () -> - evaluate_cmd_step ret_fun true prog [] [] [ conf ] path []); + (fun ?selector () -> + evaluate_cmd_step ret_fun true prog [] [] [ conf ] selector []); } (** diff --git a/GillianCore/engine/general_semantics/general/g_interpreter_intf.ml b/GillianCore/engine/general_semantics/general/g_interpreter_intf.ml index 636df35c5..383b516db 100644 --- a/GillianCore/engine/general_semantics/general/g_interpreter_intf.ml +++ b/GillianCore/engine/general_semantics/general/g_interpreter_intf.ml @@ -34,6 +34,7 @@ module type S = sig error_state : state_t; errors : err_t list; branch_path : Branch_case.path; + prev_cmd_report_id : Logging.Report_id.t option; } type cont = { @@ -55,6 +56,7 @@ module type S = sig ret_val : state_vt; final_state : state_t; branch_path : Branch_case.path; + prev_cmd_report_id : Logging.Report_id.t option; } type susp = { @@ -67,6 +69,7 @@ module type S = sig loop_ids : string list; branch_count : int; branch_path : Branch_case.path; + prev_cmd_report_id : Logging.Report_id.t option; } type t = @@ -83,9 +86,14 @@ module type S = sig In the symbolic case, this is the result of {i one branch} of execution *) type result_t = (state_t, state_vt, err_t) Exec_res.t + type conf_selector = + | Path of Branch_case.path + | IdCase of Logging.Report_id.t * Branch_case.t option + (** To support the step-by-step behaviour of the debugger, execution is split into thunks; each invocation executes one GIL command. - By supplying a branch path, a particular branch of execution can be selected. *) - type 'result cont_func_f = ?path:Branch_case.path -> unit -> 'result cont_func + By supplying a branch path, or an ID and branch case, a particular branch of execution can be selected. *) + type 'result cont_func_f = + ?selector:conf_selector -> unit -> 'result cont_func and 'result cont_func = | Finished of 'result list diff --git a/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/llen.c.symtab.json b/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/llen.c.symtab.json index 5c4137cbc..8440f9a6e 100644 --- a/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/llen.c.symtab.json +++ b/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/llen.c.symtab.json @@ -138,7 +138,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" @@ -160,7 +160,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" @@ -2658,7 +2658,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" @@ -2680,7 +2680,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" @@ -2729,7 +2729,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" @@ -2755,7 +2755,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" @@ -2790,7 +2790,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" @@ -2812,7 +2812,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" @@ -7391,7 +7391,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "8" @@ -15358,7 +15358,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" @@ -15381,7 +15381,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" @@ -15407,7 +15407,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" @@ -15442,7 +15442,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" @@ -15464,7 +15464,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" @@ -15664,7 +15664,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" @@ -15686,7 +15686,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" @@ -15735,7 +15735,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" @@ -15761,7 +15761,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" @@ -15796,7 +15796,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" @@ -15818,7 +15818,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-787fab96/share/include/stdlib.h" + "id": "/home/nat/code/Gillian/_esy/default/store/i/gillian_platform-32fbba6f/share/include/stdlib.h" }, "line": { "id": "10" diff --git a/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c.symtab.json b/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c.symtab.json index 6d6318fe9..6812a9f58 100644 --- a/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c.symtab.json +++ b/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c.symtab.json @@ -7,7 +7,7 @@ "messageType": "STATUS-MESSAGE" }, { - "messageText": "Parsing /home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c", + "messageText": "Parsing debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c", "messageType": "STATUS-MESSAGE" }, { @@ -22,7 +22,7 @@ "messageText": "function '__nondet_int' is not declared", "messageType": "WARNING", "sourceLocation": { - "file": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c", + "file": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c", "function": "main", "line": "2", "workingDirectory": "/home/nat/code/Gillian" @@ -345,7 +345,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -412,7 +412,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -449,7 +449,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -485,7 +485,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -1923,7 +1923,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "line": { "id": "1" @@ -2005,7 +2005,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "line": { "id": "1" @@ -2049,7 +2049,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "line": { "id": "1" @@ -2069,7 +2069,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "line": { "id": "1" @@ -2114,7 +2114,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "line": { "id": "1" @@ -3114,7 +3114,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "line": { "id": "1" @@ -6275,7 +6275,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "line": { "id": "1" @@ -6298,7 +6298,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "line": { "id": "1" @@ -6336,7 +6336,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -6353,7 +6353,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "line": { "id": "1" @@ -6378,7 +6378,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -6406,7 +6406,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -6442,7 +6442,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -6478,7 +6478,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -6532,7 +6532,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -6560,7 +6560,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -6607,7 +6607,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -6706,7 +6706,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -6734,7 +6734,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -6770,7 +6770,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -6806,7 +6806,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -6852,7 +6852,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -6880,7 +6880,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -6927,7 +6927,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7026,7 +7026,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7054,7 +7054,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7093,7 +7093,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7137,7 +7137,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7165,7 +7165,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7193,7 +7193,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7232,7 +7232,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7270,7 +7270,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7287,7 +7287,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7315,7 +7315,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7343,7 +7343,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7382,7 +7382,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7418,7 +7418,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7454,7 +7454,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7493,7 +7493,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7542,7 +7542,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7570,7 +7570,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7617,7 +7617,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7779,7 +7779,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7807,7 +7807,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7846,7 +7846,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -7929,7 +7929,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -8020,7 +8020,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" @@ -8051,7 +8051,7 @@ "id": "", "namedSub": { "file": { - "id": "/home/nat/code/Gillian/debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" + "id": "debugger-vscode-extension/sampleWorkspace/kani/c/wpst/simple_branch.c" }, "function": { "id": "main" diff --git a/debugger-vscode-extension/sampleWorkspace/list_length_rec.wisl b/debugger-vscode-extension/sampleWorkspace/list_length_rec.wisl index deaef2953..6ff7fa574 100644 --- a/debugger-vscode-extension/sampleWorkspace/list_length_rec.wisl +++ b/debugger-vscode-extension/sampleWorkspace/list_length_rec.wisl @@ -6,7 +6,7 @@ predicate list(+x, alpha) { { (x == #x) * list(#x, #alpha) } function llen(x) { if (x = null) { - n := 0 + n := 1 } else { t := [x+1]; n := llen(t); diff --git a/kanillian/lib/lifter/kani_c_lifter.ml b/kanillian/lib/lifter/kani_c_lifter.ml index 0bc20450d..0a7be9e6f 100644 --- a/kanillian/lib/lifter/kani_c_lifter.ml +++ b/kanillian/lib/lifter/kani_c_lifter.ml @@ -47,6 +47,8 @@ struct type branch_data = rid * 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 _ Effect.t += Step : step_args -> exec_data Effect.t type map = (Branch_case.t, cmd_data, branch_data) Exec_map.t @@ -111,11 +113,9 @@ struct type partial_result = | Finished of finished - | StepAgain of (rid option * Gil_branch_case.t option) + | StepAgain of (rid * Gil_branch_case.t option) [@@deriving yojson] - let step_again ?id ?branch_case () = StepAgain (id, branch_case) - let ends_to_cases ~is_unevaluated_funcall ~nest_kind @@ -410,7 +410,7 @@ struct (* Finish or continue *) match Stack.pop_opt partial.unexplored_paths with | None -> finish partial - | Some (id, branch_case) -> step_again ~id ?branch_case () |> Result.ok + | Some (id, branch_case) -> StepAgain (id, branch_case) |> Result.ok end let update = Update.f @@ -629,7 +629,7 @@ struct in let** () = insert_cmd ~state ~prev ~stack_direction new_cmd in all_ids |> List.iter (fun id -> Hashtbl.replace id_map id new_cmd); - Ok ()) + Ok new_cmd) |> Result_utils.or_else (failwith ~state ~finished_partial) end @@ -677,7 +677,7 @@ struct ] in DL.failwith json "Kani_c_lifter: Encountered unknown cmd kind" - | Harness -> ExecNext (None, None) + | Harness -> Either.Left (exec_data.id, None) | Normal _ | Internal | Return | Hidden -> ( let get_prev = get_prev ~state ~gil_case ~prev_id in let partial_result = @@ -685,39 +685,13 @@ struct in match partial_result with | Finished finished -> - insert_new_cmd ~state finished; - Stop (Some finished.id) - | StepAgain (id, case) -> ExecNext (id, case)) + let cmd = insert_new_cmd ~state finished in + Either.Right cmd + | StepAgain (id, case) -> Either.Left (id, case)) end let init_or_handle = Init_or_handle.f - let init ~proc_name ~all_procs:_ tl_ast prog exec_data = - 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; - prog; - partial_cmds; - map = Nothing; - id_map; - func_return_map = Hashtbl.create 0; - func_return_count = 0; - } - in - let result = init_or_handle ~state exec_data in - (state, result) - - let init_exn ~proc_name ~all_procs tl_ast prog exec_data = - match init ~proc_name ~all_procs tl_ast prog exec_data with - | None -> failwith "init: kani_c_lifter needs a tl_ast!" - | Some x -> x - let handle_cmd prev_id gil_case exec_data state = init_or_handle ~state ~prev_id ?gil_case exec_data @@ -769,35 +743,6 @@ struct let path_of_id id { gil_state; _ } = Gil_lifter.path_of_id id gil_state - let existing_next_steps id { gil_state; id_map; _ } = - Gil_lifter.existing_next_steps id gil_state - |> List.filter (fun (id, _) -> Hashtbl.mem id_map id) - - let next_gil_step id case state = - let failwith s = - DL.failwith - (fun () -> - [ - ("state", dump state); - ("id", rid_to_yojson id); - ("case", opt_to_yojson Packaged.branch_case_to_yojson case); - ]) - ("next_gil_step: " ^ s) - in - match (Hashtbl.find state.id_map id, case) with - | Nothing, _ -> failwith "HORROR - cmd at id is Nothing!" - | FinalCmd _, _ -> failwith "can't get next at final cmd!" - | Cmd _, Some _ -> failwith "got branch case at non-branch cmd!" - | BranchCmd _, None -> failwith "expected branch case at branch cmd!" - | Cmd { data; _ }, None -> - let id = List.hd (List.rev data.all_ids) in - (id, None) - | BranchCmd { nexts; _ }, Some case -> ( - let case = case |> snd |> Branch_case.of_yojson |> Result.get_ok in - match Hashtbl.find_opt nexts case with - | None -> failwith "branch case not found!" - | Some ((id, case), _) -> (id, case)) - let previous_step id { id_map; _ } = let+ id, case = match Hashtbl.find id_map id with @@ -807,47 +752,246 @@ struct let case = case |> Option.map package_case in (id, case) - let select_next_path case id { gil_state; _ } = - Gil_lifter.select_next_path case id gil_state + let memory_error_to_exception_info + (_ : (memory_error, annot, tl_ast) memory_error_info) : exception_info = + { id = "unknown"; description = Some "Error lifting not supported yet!" } - let find_unfinished_path ?at_id state = - let { map; id_map; _ } = state in - let failwith m = - DL.failwith - (fun () -> - [ - ("state", dump state); ("at_id", opt_to_yojson rid_to_yojson at_id); - ]) - ("find_unfinished_path: " ^ m) + let add_variables = Memory_model.MonadicSMemory.Lift.add_variables + + let select_case nexts = + let case, _ = + Hashtbl.fold + (fun _ (id_case, map) acc -> + match (map, acc) with + | _, (_, true) -> acc + | Nothing, (_, false) -> (Some id_case, true) + | _, (None, false) -> (Some id_case, false) + | _ -> acc) + nexts (None, false) + in + Option.get case + + let 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 _, _ -> failwith "HORROR - tried to step from FinalCmd!" + | Cmd _, 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 + let case = match Gil_lifter.cases_at_id id state.gil_state with + | [] -> None + | [ case ] -> Some case + | _ -> Fmt.failwith "find_next: id %a has multiple cases - not sure where to step!" L.Report_id.pp id + in + Either.Right (id, case) + | Cmd { next; _ }, None -> Either.Left next + | BranchCmd { nexts; _ }, None -> + let id_case = select_case nexts in + Either.Right id_case + | BranchCmd { nexts; _ }, Some case -> ( + match Hashtbl.find_opt nexts case with + | None -> failwith "case not found" + | Some ((id, case), Nothing) -> Either.Right (id, case) + | Some (_, next) -> Either.Left next) + + let request_next state id case = + let rec aux id case = + let path = path_of_id id state in + 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 + in + aux id case + + let step state id case = + match find_next state id case with + | Either.Left next -> next + | Either.Right (id, case) -> request_next state id case + + (* If a FinalCmd is in a function call, get the caller ID + and the relevant branch case for stepping forward, + while checking that it actually exists. *) + let get_next_from_end state cmd = + let caller_id, (label, ix) = + match cmd with + | FinalCmd { data } -> + (List.hd data.callers, Option.get data.func_return_label) + | _ -> failwith "Expected non-final cmd!" in - let rec aux = function - | Nothing -> failwith "started at Nothing" - | Cmd { data = { all_ids; _ }; next = Nothing } -> - let id = List.hd (List.rev all_ids) in - Some (id, None) - | Cmd { next; _ } -> aux next + let case = Case (Func_exit label, ix) in + let () = + match Hashtbl.find state.id_map caller_id with | BranchCmd { nexts; _ } -> ( - let unfinished = - Hashtbl.find_map - (fun _ (gil_step, next) -> - if next = Nothing then Some gil_step else None) - nexts + match Hashtbl.find_opt nexts case with + | None -> failwith "Func return case not found!" + | Some _ -> ()) + | _ -> failwith "Expected a branch cmd!" + in + (caller_id, Some 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 rec aux ends = function + | [] -> List.rev ends + | (id, case) :: rest -> + let ends, nexts = + match step state id case with + | Nothing -> failwith "Stepped to Nothing!" + | Cmd { data; _ } -> (ends, (data.id, None) :: rest) + | BranchCmd { nexts; _ } -> + let new_nexts = + Hashtbl.to_seq_keys nexts + |> Seq.map (fun case -> (id, Some case)) + |> List.of_seq + in + (ends, new_nexts @ rest) + | FinalCmd { data } as end_ -> + let stack_depth' = List.length 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 end_ in + (ends, next :: rest) + else (end_ :: ends, rest) in - match unfinished with - | None -> Hashtbl.find_map (fun _ (_, next) -> aux next) nexts - | result -> result) - | FinalCmd _ -> None + aux ends nexts in - let map = - match at_id with - | None -> map - | Some id -> Hashtbl.find id_map id + match (case, cmd) with + | _, Nothing -> failwith "Stepping from Nothing!" + | _, FinalCmd _ -> [ cmd ] + | None, BranchCmd { nexts; _ } -> + let first_steps = + Hashtbl.to_seq_keys nexts + |> Seq.map (fun case -> (id, Some case)) + |> List.of_seq + 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 in - aux map + let next = step state id case in + let id = (get_cmd_data_exn next).id in + (id, Debugger_utils.Step) - let memory_error_to_exception_info - (_ : (memory_error, annot, tl_ast) memory_error_info) : exception_info = - { id = "unknown"; description = Some "Error lifting not supported yet!" } + let step_over state id = + let map = Hashtbl.find state.id_map id in + let () = + let () = + match map with + | BranchCmd { nexts; _ } -> + if Hashtbl.mem nexts Func_exit_placeholder 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 + | Submap m -> Some m + in + let _ = step_all state (get_cmd_data_exn submap).id None in + () + in + let data = get_cmd_data_exn (step state id None) in + (data.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!" + | FinalCmd _ -> (id, Debugger_utils.Step) + | Cmd { data; _ } | BranchCmd { 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 step_back state id = + let cmd = Hashtbl.find state.id_map id in + let data = get_cmd_data_exn cmd in + let id = + match data.prev with + | Some (id, _) -> id + | None -> id + in + (id, Debugger_utils.Step) + + let step_branch _ _ _ = failwith "TODO" + + let continue state id = + let ends = step_all state id None in + let id = (get_cmd_data_exn (List.hd ends)).id 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 + | [] -> continue state id + | caller_id :: _ -> step_over state caller_id + + let is_breakpoint _ = true (* TODO *) + + let continue_back state id = + let rec aux cmd = + let data = get_cmd_data_exn cmd in + if is_breakpoint cmd then (data.id, Debugger_utils.Breakpoint) + else + match previous_step data.id state with + | None -> failwith "No previous step!" + | Some (id, _) -> aux (Hashtbl.find state.id_map id) + in + aux (Hashtbl.find state.id_map id) - let add_variables = Memory_model.MonadicSMemory.Lift.add_variables + 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; + prog; + partial_cmds; + map = Nothing; + id_map; + func_return_map = Hashtbl.create 0; + func_return_count = 0; + } + in + let finish_init () = + let rec aux id_case = + let id, case, path = + match id_case with + | Some (id, case) -> + let path = path_of_id id state in + (Some id, case, path) + | None -> (None, None, []) + in + 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 + in + let map = aux None in + let id = (get_cmd_data_exn map).id in + (id, Debugger_utils.Step) + in + (state, finish_init) + + let init_exn ~proc_name ~all_procs tl_ast prog = + match init ~proc_name ~all_procs tl_ast prog with + | None -> failwith "init: wislLifter needs a tl_ast!" + | Some x -> x end diff --git a/wisl/lib/debugging/wislLifter.ml b/wisl/lib/debugging/wislLifter.ml index e0a49b85c..1e56d9383 100644 --- a/wisl/lib/debugging/wislLifter.ml +++ b/wisl/lib/debugging/wislLifter.ml @@ -91,6 +91,9 @@ struct } [@@deriving yojson] + type step_args = rid 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] @@ -140,9 +143,9 @@ struct type partial_result = | Finished of finished - | StepAgain of (rid option * Gil_branch_case.t option) + | StepAgain of (rid * Gil_branch_case.t option) - let step_again ?id ?branch_case () = Ok (StepAgain (id, branch_case)) + let step_again ~id ?branch_case () = Ok (StepAgain (id, branch_case)) let ends_to_cases ~nest_kind (ends : (Branch_case.case * branch_data) list) = @@ -628,7 +631,7 @@ struct insert_cmd ~state ~prev ~stack_direction ~func_return_label new_cmd in all_ids |> List.iter (fun id -> Hashtbl.replace id_map id new_cmd); - Ok () + Ok new_cmd in r |> Result_utils.or_else (fun e -> @@ -649,14 +652,14 @@ struct This would normally be [Hidden], but we want to only consider the true case of the function *) let handle_loop_prefix exec_data = - let annot = CmdReport.(exec_data.cmd_report.annot) in + let { cmd_report; id; _ } = exec_data in + let annot = CmdReport.(cmd_report.annot) in match annot.stmt_kind with | LoopPrefix -> - Some - (match exec_data.cmd_report.cmd with - | Cmd.GuardedGoto _ -> - ExecNext (None, Some (Gil_branch_case.GuardedGoto true)) - | _ -> ExecNext (None, None)) + (match exec_data.cmd_report.cmd with + | Cmd.GuardedGoto _ -> (id, Some (Gil_branch_case.GuardedGoto true)) + | _ -> (id, None)) + |> Option.some | _ -> None let get_prev ~state ~gil_case ~prev_id () = @@ -685,9 +688,12 @@ struct | Some case -> Ok (Some (data.id, Some case, data.callers)) | None -> Error "couldn't find prev in branches!") - let f ~state ?prev_id ?gil_case (exec_data : exec_data) : handle_cmd_result - = - let- () = handle_loop_prefix exec_data in + let f ~state ?prev_id ?gil_case (exec_data : exec_data) : + (rid * Gil_branch_case.t option, map) Either.t = + let- () = + let+ id, case = handle_loop_prefix exec_data in + Either.Left (id, case) + in let gil_case = Option_utils.coalesce gil_case exec_data.cmd_report.branch_case in @@ -709,45 +715,12 @@ struct ("finished", Partial_cmds.finished_to_yojson finished); ] "Finishing WISL command"); - insert_new_cmd ~state finished; - Stop (Some finished.id) - | StepAgain (id, case) -> ExecNext (id, case) + let cmd = insert_new_cmd ~state finished in + Either.Right cmd + | StepAgain (id, case) -> Either.Left (id, case) end let init_or_handle = Init_or_handle.f - - let init ~proc_name ~all_procs:_ tl_ast prog exec_data = - let gil_state = Gil.get_state () in - let+ tl_ast = tl_ast in - let partial_cmds = Hashtbl.create 0 in - let id_map = Hashtbl.create 0 in - let before_partial = None in - let state = - { - proc_name; - gil_state; - tl_ast; - partial_cmds; - map = Nothing; - id_map; - before_partial; - is_loop_func = false; - prog; - func_return_data = Hashtbl.create 0; - func_return_count = 0; - } - in - let result = init_or_handle ~state exec_data in - (state, result) - - let init_exn ~proc_name ~all_procs tl_ast prog exec_data = - match init ~proc_name ~all_procs tl_ast prog exec_data with - | None -> failwith "init: wislLifter needs a tl_ast!" - | Some x -> x - - let handle_cmd prev_id gil_case (exec_data : exec_data) state = - init_or_handle ~state ~prev_id ?gil_case exec_data - let get_gil_map _ = failwith "get_gil_map: not implemented!" let package_case case = @@ -795,35 +768,6 @@ struct let path_of_id id { gil_state; _ } = Gil_lifter.path_of_id id gil_state - let existing_next_steps id { gil_state; id_map; _ } = - Gil_lifter.existing_next_steps id gil_state - |> List.filter (fun (id, _) -> Hashtbl.mem id_map id) - - let next_gil_step id case state = - let failwith s = - DL.failwith - (fun () -> - [ - ("state", dump state); - ("id", rid_to_yojson id); - ("case", opt_to_yojson Packaged.branch_case_to_yojson case); - ]) - ("next_gil_step: " ^ s) - in - match (Hashtbl.find state.id_map id, case) with - | Nothing, _ -> failwith "HORROR - cmd at id is Nothing!" - | FinalCmd _, _ -> failwith "can't get next at final cmd!" - | Cmd _, Some _ -> failwith "got branch case at non-branch cmd!" - | BranchCmd _, None -> failwith "expected branch case at branch cmd!" - | Cmd { data; _ }, None -> - let id = List.hd (List.rev data.all_ids) in - (id, None) - | BranchCmd { nexts; _ }, Some case -> ( - let case = case |> snd |> Branch_case.of_yojson |> Result.get_ok in - match Hashtbl.find_opt nexts case with - | None -> failwith "branch case not found!" - | Some ((id, case), _) -> (id, case)) - let previous_step id { id_map; _ } = let+ id, case = match Hashtbl.find id_map id with @@ -833,52 +777,6 @@ struct let case = case |> Option.map package_case in (id, case) - let select_next_path case id { gil_state; _ } = - Gil_lifter.select_next_path case id gil_state - - let find_unfinished_path ?at_id state = - let { map; id_map; _ } = state in - let rec aux map = - match aux_submap map with - | None -> aux_map map - | result -> result - and aux_map = function - | Nothing -> - DL.failwith - (fun () -> - [ - ("state", dump state); - ("at_id", opt_to_yojson rid_to_yojson at_id); - ]) - "find_unfinished_path: started at Nothing" - | Cmd { data = { all_ids; _ }; next = Nothing } -> - let id = List.hd (List.rev all_ids) in - Some (id, None) - | Cmd { next; _ } -> aux next - | BranchCmd { nexts; _ } -> ( - match - Hashtbl.find_map - (fun _ ((id, gil_case), next) -> - if next = Nothing then Some (id, gil_case) else None) - nexts - with - | None -> Hashtbl.find_map (fun _ (_, next) -> aux next) nexts - | result -> result) - | FinalCmd _ -> None - and aux_submap = function - | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data; _ } -> ( - match data.submap with - | Submap map -> aux_map map - | _ -> None) - | Nothing -> None - in - let map = - match at_id with - | None -> map - | Some id -> Hashtbl.find id_map id - in - aux map - let get_wisl_stmt gil_cmd wisl_ast = let* annot = match gil_cmd with @@ -1005,4 +903,246 @@ struct { id; description } let add_variables = WislSMemory.add_debugger_variables + + let select_case nexts = + let case, _ = + Hashtbl.fold + (fun _ (id_case, map) acc -> + match (map, acc) with + | _, (_, true) -> acc + | Nothing, (_, false) -> (Some id_case, true) + | _, (None, false) -> (Some id_case, false) + | _ -> acc) + nexts (None, false) + in + Option.get case + + let 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 _, _ -> failwith "HORROR - tried to step from FinalCmd!" + | Cmd _, 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 + let case = match Gil_lifter.cases_at_id id state.gil_state with + | [] -> None + | [ case ] -> Some case + | _ -> Fmt.failwith "find_next: id %a has multiple cases - not sure where to step!" L.Report_id.pp id + in + Either.Right (id, case) + | Cmd { next; _ }, None -> Either.Left next + | BranchCmd { nexts; _ }, None -> + let id_case = select_case nexts in + Either.Right id_case + | BranchCmd { nexts; _ }, Some case -> ( + match Hashtbl.find_opt nexts case with + | None -> failwith "case not found" + | Some ((id, case), Nothing) -> Either.Right (id, case) + | Some (_, next) -> Either.Left next) + + let request_next state id case = + let rec aux id case = + let path = path_of_id id state in + 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 + in + aux id case + + let step state id case = + match find_next state id case with + | Either.Left next -> next + | Either.Right (id, case) -> request_next state id case + + (* If a FinalCmd is in a function call, get the caller ID + and the relevant branch case for stepping forward, + while checking that it actually exists. *) + let get_next_from_end state cmd = + let caller_id, (label, ix) = + match cmd with + | FinalCmd { data } -> + (List.hd data.callers, Option.get data.func_return_label) + | _ -> failwith "Expected non-final cmd!" + in + let case = Case (FuncExit label, ix) in + let () = + match Hashtbl.find state.id_map caller_id with + | BranchCmd { nexts; _ } -> ( + match Hashtbl.find_opt nexts case with + | None -> failwith "Func return case not found!" + | Some _ -> ()) + | _ -> failwith "Expected a branch cmd!" + in + (caller_id, Some 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 rec aux ends = function + | [] -> List.rev ends + | (id, case) :: rest -> + let ends, nexts = + match step state id case with + | Nothing -> failwith "Stepped to Nothing!" + | Cmd { data; _ } -> (ends, (data.id, None) :: rest) + | BranchCmd { nexts; _ } -> + let new_nexts = + Hashtbl.to_seq_keys nexts + |> Seq.map (fun case -> (id, Some case)) + |> List.of_seq + in + (ends, new_nexts @ rest) + | FinalCmd { data } as end_ -> + let stack_depth' = List.length 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 end_ in + (ends, next :: rest) + else (end_ :: ends, rest) + in + aux ends nexts + in + match (case, cmd) with + | _, Nothing -> failwith "Stepping from Nothing!" + | _, FinalCmd _ -> [ cmd ] + | None, BranchCmd { nexts; _ } -> + let first_steps = + Hashtbl.to_seq_keys nexts + |> Seq.map (fun case -> (id, Some case)) + |> List.of_seq + 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 + in + let next = step state id case in + let id = (get_cmd_data_exn next).id in + (id, Debugger_utils.Step) + + let step_over state id = + Debugger_log.to_file "Wisl stepping over..."; + let map = Hashtbl.find state.id_map id in + let () = + let () = + match map with + | BranchCmd { nexts; _ } -> + if Hashtbl.mem nexts FuncExitPlaceholder then + step state id (Some FuncExitPlaceholder) |> ignore + | _ -> () + in + let> submap = + match (get_cmd_data_exn map).submap with + | NoSubmap | Proc _ | Submap Nothing -> None + | Submap m -> Some m + in + let _ = step_all state (get_cmd_data_exn submap).id None in + () + in + let data = get_cmd_data_exn (step state id None) in + Debugger_log.to_file "Wisl stepped over!"; + (data.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!" + | FinalCmd _ -> (id, Debugger_utils.Step) + | Cmd { data; _ } | BranchCmd { 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 step_back state id = + let cmd = Hashtbl.find state.id_map id in + let data = get_cmd_data_exn cmd in + let id = + match data.prev with + | Some (id, _) -> id + | None -> id + in + (id, Debugger_utils.Step) + + let step_branch _ _ _ = failwith "TODO" + + let continue state id = + let ends = step_all state id None in + let id = (get_cmd_data_exn (List.hd ends)).id 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 + | [] -> continue state id + | caller_id :: _ -> step_over state caller_id + + let is_breakpoint _ = true (* TODO *) + + let continue_back state id = + let rec aux cmd = + let data = get_cmd_data_exn cmd in + if is_breakpoint cmd then (data.id, Debugger_utils.Breakpoint) + else + match previous_step data.id state with + | None -> failwith "No previous step!" + | Some (id, _) -> aux (Hashtbl.find state.id_map id) + in + aux (Hashtbl.find state.id_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 = Hashtbl.create 0 in + let id_map = Hashtbl.create 0 in + let before_partial = None in + let state = + { + proc_name; + gil_state; + tl_ast; + partial_cmds; + map = Nothing; + id_map; + before_partial; + is_loop_func = false; + prog; + func_return_data = Hashtbl.create 0; + func_return_count = 0; + } + in + let finish_init () = + let rec aux id_case = + let id, case, path = + match id_case with + | Some (id, case) -> + let path = path_of_id id state in + (Some id, case, path) + | None -> (None, None, []) + in + 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 + in + let map = aux None in + let id = (get_cmd_data_exn map).id in + (id, Debugger_utils.Step) + in + (state, finish_init) + + let init_exn ~proc_name ~all_procs tl_ast prog = + match init ~proc_name ~all_procs tl_ast prog with + | None -> failwith "init: wislLifter needs a tl_ast!" + | Some x -> x end