From 82cea6651af1a7cfd70033c8ec33151bed7238d0 Mon Sep 17 00:00:00 2001 From: Nat Karmios Date: Wed, 27 Sep 2023 15:26:22 +0100 Subject: [PATCH] Introduce abstract debugger --- GillianCore/command_line/command_line.ml | 15 +- .../debug_verification_console.ml | 1 + .../command_line/debug_wpst_console.ml | 28 + GillianCore/debugging/adapter/inspect.ml | 4 +- .../debugging/debugger/base_debugger.ml | 1078 ++++++++++++++++ GillianCore/debugging/debugger/debugger.ml | 1106 +---------------- .../debugging/debugger/debugger_intf.ml | 47 +- .../debugging/debugger/symbolic_debugger.ml | 47 + .../debugger/verification_debugger.ml | 139 +++ .../debugging/lifter/gil_fallback_lifter.ml | 13 +- .../lifter/gil_fallback_lifter_intf.ml | 2 +- GillianCore/debugging/lifter/gil_lifter.ml | 111 +- GillianCore/debugging/lifter/gil_lifter.mli | 8 +- GillianCore/debugging/lifter/lifter_intf.ml | 8 +- GillianCore/debugging/utils/exec_map.ml | 6 +- GillianCore/utils/list_utils.ml | 5 + wisl/lib/ParserAndCompiler/WAnnot.ml | 6 +- wisl/lib/ParserAndCompiler/wisl2Gil.ml | 7 +- wisl/lib/debugging/wislLifter.ml | 742 +++++++---- wisl/lib/utils/wBranchCase.ml | 12 +- 20 files changed, 1946 insertions(+), 1439 deletions(-) create mode 100644 GillianCore/command_line/debug_wpst_console.ml create mode 100644 GillianCore/debugging/debugger/base_debugger.ml create mode 100644 GillianCore/debugging/debugger/symbolic_debugger.ml create mode 100644 GillianCore/debugging/debugger/verification_debugger.ml diff --git a/GillianCore/command_line/command_line.ml b/GillianCore/command_line/command_line.ml index e6f7d59fa..91432c501 100644 --- a/GillianCore/command_line/command_line.ml +++ b/GillianCore/command_line/command_line.ml @@ -35,8 +35,12 @@ struct module Verification = Verifier.Make (SState) (SPState) (PC) (External) module Lifter = Lifter (Verification) module Abductor = Abductor.Make (SPState) (PC) (External) - module Debugger = Debugger.Make (ID) (PC) (Verification) (Lifter) - module Debug_adapter = Debug_adapter.Make (Debugger) + + module Symb_debugger = + Debugger.Symbolic_debugger.Make (ID) (PC) (Verification) (Lifter) + + module Verif_debugger = + Debugger.Verification_debugger.Make (ID) (PC) (Verification) (Lifter) let main () = Memtrace.trace_if_requested (); @@ -60,7 +64,12 @@ struct (Gil_parsing)); (module Verification_console.Make (ID) (PC) (Verification) (Gil_parsing)); (module Act_console.Make (ID) (PC) (Abductor) (Gil_parsing)); - (module Debug_verification_console.Make (PC) (Debug_adapter)); + (module Debug_verification_console.Make + (PC) + (Debug_adapter.Make (Verif_debugger))); + (module Debug_wpst_console.Make + (PC) + (Debug_adapter.Make (Symb_debugger))); (module Bulk_console.Make (PC) (Runners)); ] in diff --git a/GillianCore/command_line/debug_verification_console.ml b/GillianCore/command_line/debug_verification_console.ml index b0eb862f8..ad89ba3e8 100644 --- a/GillianCore/command_line/debug_verification_console.ml +++ b/GillianCore/command_line/debug_verification_console.ml @@ -21,6 +21,7 @@ module Make (PC : ParserAndCompiler.S) (Debug_adapter : Debug_adapter.S) : Cmd.info "debugverify" ~doc ~man let start_debug_adapter manual () = + Config.current_exec_mode := Utils.Exec_mode.Verification; Config.manual_proof := manual; Lwt_main.run (Debug_adapter.start Lwt_io.stdin Lwt_io.stdout) diff --git a/GillianCore/command_line/debug_wpst_console.ml b/GillianCore/command_line/debug_wpst_console.ml new file mode 100644 index 000000000..1c2f50dcb --- /dev/null +++ b/GillianCore/command_line/debug_wpst_console.ml @@ -0,0 +1,28 @@ +open Cmdliner + +module Make (PC : ParserAndCompiler.S) (Debug_adapter : Debug_adapter.S) : + Console.S = struct + module Common_args = Common_args.Make (PC) + + let debug_wpst_info = + let doc = + "Starts Gillian in debugging mode for whole-program symbolic testing" + in + let man = + [ + `S Manpage.s_description; + `P + "Starts Gillian in debugging mode for whole-program symbolic \ + testing, which communicates via the Debug Adapter Protocol"; + ] + in + Cmd.info "debugwpst" ~doc ~man + + let start_debug_adapter () = + Config.current_exec_mode := Utils.Exec_mode.Symbolic; + Lwt_main.run (Debug_adapter.start Lwt_io.stdin Lwt_io.stdout) + + let debug_wpst_t = Common_args.use Term.(const start_debug_adapter) + let debug_wpst_cmd = Cmd.v debug_wpst_info debug_wpst_t + let cmds = [ debug_wpst_cmd ] +end diff --git a/GillianCore/debugging/adapter/inspect.ml b/GillianCore/debugging/adapter/inspect.ml index 65aad7fa8..2b36e76f0 100644 --- a/GillianCore/debugging/adapter/inspect.ml +++ b/GillianCore/debugging/adapter/inspect.ml @@ -73,8 +73,8 @@ module Make (Debugger : Debugger.S) = struct DL.set_rpc_command_handler rpc ~name:"Unification" (module Unification_command) (fun { id } -> - let unify_id, unify_map = dbg |> Debugger.Inspect.get_unification id in - let result = Unification_command.Result.make ~unify_id ~unify_map in + let unify_map = dbg |> Debugger.Inspect.get_unify_map id in + let result = Unification_command.Result.make ~unify_id:id ~unify_map in Lwt.return result); Lwt.return () end diff --git a/GillianCore/debugging/debugger/base_debugger.ml b/GillianCore/debugging/debugger/base_debugger.ml new file mode 100644 index 000000000..6edea9884 --- /dev/null +++ b/GillianCore/debugging/debugger/base_debugger.ml @@ -0,0 +1,1078 @@ +open Syntaxes.Option +module L = Logging +module DL = Debugger_log +module Lift = Debugger_lifter +module Exec_map = Exec_map + +let ( let** ) = Result.bind +let ( let++ ) f o = Result.map o f + +module Premake + (ID : Init_data.S) + (PC : ParserAndCompiler.S with type init_data = ID.t) + (Verification : Verifier.S + with type SPState.init_data = ID.t + and type annot = PC.Annot.t) + (Lifter : Lift.S + with type memory = Verification.SAInterpreter.heap_t + and type memory_error = Verification.SPState.m_err_t + and type tl_ast = PC.tl_ast + and type cmd_report = + Verification.SAInterpreter.Logging.ConfigReport.t + and type annot = PC.Annot.t) = +struct + open Verification.SAInterpreter + module Gil_parsing = Gil_parsing.Make (PC.Annot) + module Breakpoints = Set.Make (Int) + module Annot = PC.Annot + module Content_type = L.Logging_constants.Content_type + module State = Verification.SPState + + type breakpoints = (string, Breakpoints.t) Hashtbl.t + type tl_ast = PC.tl_ast + + 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; + (* 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; + mutable frames : frame list; + mutable variables : Variable.ts; [@default Hashtbl.create 0] + mutable errors : err_t list; + mutable cur_cmd : (int Cmd.t * Annot.t) option; + mutable proc_name : string option; + lifter_state : Lifter.t; + report_state : L.Report_state.t; + ext : 'ext; + } + [@@deriving make] + + type 'ext base_debug_state = { + source_file : string; + source_files : SourceFiles.t option; + prog : Verification.prog_t; + tl_ast : tl_ast option; + main_proc_name : string; + report_state_base : L.Report_state.t; + init_data : ID.t; + proc_names : string list; + mutable cur_proc_name : string; + ext : 'ext; + } + [@@deriving make] + + type ('proc_state, 'debug_state) state = { + procs : (string, 'proc_state) Hashtbl.t; + debug_state : 'debug_state; + } + + module type Debugger_impl = sig + type proc_state_ext + type debug_state_ext + + val preprocess_prog : + no_unfold:bool -> (annot, int) Prog.t -> (annot, int) Prog.t + + val init : unit base_debug_state -> debug_state_ext + + val init_proc : + debug_state_ext base_debug_state -> unit base_proc_state -> proc_state_ext + + val launch_proc : + proc_name:string -> debug_state_ext base_debug_state -> result_t cont_func + + module Unify : sig + val unify_final_cmd : + L.Report_id.t -> + proc_name:string -> + (state_t, state_vt, err_t) Exec_res.t -> + debug_state_ext base_debug_state -> + Exec_map.unification list + + val get_unifys : + L.Report_id.t -> + debug_state_ext base_debug_state -> + proc_state_ext base_proc_state -> + Exec_map.unification list + + val get_unify_map : + L.Report_id.t -> debug_state_ext base_debug_state -> Unify_map.t + end + end + + module Make (Debugger_impl : Debugger_impl) = struct + open Debugger_impl + open Debugger_impl.Unify + + type nonrec breakpoints = breakpoints + type nonrec tl_ast = tl_ast + type proc_state = proc_state_ext base_proc_state + type debug_state = debug_state_ext base_debug_state + type t = (proc_state, debug_state) state + + let get_root_proc_name_of_id id = + let content, type_ = + L.Log_queryer.get_report id + |> Option_utils.or_else (fun () -> + Fmt.failwith "Couldn't get report for %a" L.Report_id.pp id) + in + if type_ <> L.Logging_constants.Content_type.cmd then + Fmt.failwith "Report %a is not type '%s'" L.Report_id.pp id + L.Logging_constants.Content_type.cmd; + let cmd = content |> of_yojson_string Logging.ConfigReport.of_yojson in + (List_utils.last cmd.callstack |> Option.get).pid + + let get_proc_state ?cmd_id ?(activate_report_state = true) state = + let { debug_state; procs } = state in + let proc_name = + match cmd_id with + | Some cmd_id -> + let proc_name = get_root_proc_name_of_id cmd_id in + debug_state.cur_proc_name <- proc_name; + proc_name + | None -> debug_state.cur_proc_name + in + match Hashtbl.find_opt procs proc_name with + | None -> Error ("get_proc_state: couldn't find proc " ^ proc_name) + | Some proc_state -> + if activate_report_state then + L.Report_state.activate proc_state.report_state; + Ok proc_state + + let get_proc_state_exn ?cmd_id ?(activate_report_state = true) dbg = + match get_proc_state ?cmd_id ~activate_report_state dbg with + | Ok proc_state -> proc_state + | Error msg -> failwith msg + + module Inspect = struct + type debug_proc_state_view = { + exec_map : Exec_map.Packaged.t; [@key "execMap"] + lifted_exec_map : Exec_map.Packaged.t option; [@key "liftedExecMap"] + current_cmd_id : L.Report_id.t; [@key "currentCmdId"] + unifys : Exec_map.unification list; + proc_name : string; [@key "procName"] + } + [@@deriving yojson] + + let procs_to_yosjon procs : Yojson.Safe.t = + let procs = + procs + |> List.map (fun (k, v) -> (k, debug_proc_state_view_to_yojson v)) + in + `Assoc procs + + let procs_of_yojson json = + let procs = + json |> Yojson.Safe.Util.to_assoc + |> List_utils.map_results (fun (k, v) -> + let++ v' = debug_proc_state_view_of_yojson v in + (k, v')) + in + procs + + type debug_state_view = { + main_proc_name : string; [@key "mainProc"] + current_proc_name : string; [@key "currentProc"] + procs : (string * debug_proc_state_view) list; + [@to_yojson procs_to_yosjon] [@of_yojson procs_of_yojson] + } + [@@deriving yojson] + + let get_debug_state ({ debug_state; procs } : t) : debug_state_view = + DL.log (fun m -> m "Getting debug state"); + let procs = + Hashtbl.fold + (fun proc_name state acc -> + let current_cmd_id = state.cur_report_id in + let unifys = + state.lifter_state |> Lifter.get_unifys_at_id current_cmd_id + in + let exec_map = state.lifter_state |> Lifter.get_gil_map in + let lifted_exec_map = + state.lifter_state |> Lifter.get_lifted_map + in + let proc = + { exec_map; lifted_exec_map; current_cmd_id; unifys; proc_name } + in + (proc_name, proc) :: acc) + procs [] + in + DL.log (fun m -> m "Got debug state"); + { + main_proc_name = debug_state.main_proc_name; + current_proc_name = debug_state.cur_proc_name; + procs; + } + + let get_unify_map id { debug_state; _ } = get_unify_map id debug_state + end + + let top_level_scopes : Variable.scope list = + let top_level_scope_names = + (* [ "Store"; "Heap"; "Pure Formulae"; "Typing Environment"; "Predicates" ] *) + [ "Pure Formulae"; "Typing Environment"; "Predicates" ] + in + List.mapi + (fun i name -> Variable.{ name; id = i + 1 }) + top_level_scope_names + + let is_gil_file file_name = Filename.check_suffix file_name "gil" + + let get_pure_formulae_vars (state : state_t) : Variable.t list = + let open Variable in + State.get_pfs state |> PFS.to_list + |> List.map (fun formula -> + let value = Fmt.to_to_string (Fmt.hbox Formula.pp) formula in + { name = ""; value; type_ = None; var_ref = 0 }) + |> List.sort (fun v w -> Stdlib.compare v.value w.value) + + let get_type_env_vars (state : state_t) : Variable.t list = + let open Variable in + let typ_env = State.get_typ_env state in + Type_env.to_list typ_env + |> List.sort (fun (v, _) (w, _) -> Stdlib.compare v w) + |> List.map (fun (name, value) -> + let value = Type.str value in + { name; value; type_ = None; var_ref = 0 }) + |> List.sort (fun v w -> Stdlib.compare v.name w.name) + + let get_pred_vars (state : state_t) : Variable.t list = + let open Variable in + State.get_preds state |> Preds.SPreds.to_list + |> List.map (fun pred -> + let value = + Fmt.to_to_string (Fmt.hbox Preds.SPreds.pp_pabs) pred + in + { name = ""; value; type_ = None; var_ref = 0 }) + |> List.sort (fun v w -> Stdlib.compare v.value w.value) + + module Process_files = struct + let get_progs_or_fail = function + | Ok progs -> ( + match progs.ParserAndCompiler.gil_progs with + | [] -> + Fmt.pr "Error: expected at least one GIL program\n"; + exit 1 + | _ -> progs) + | Error err -> + Fmt.pr "Error during compilation to GIL:\n%a" PC.pp_err err; + exit 1 + + let compile_tl_files files = + let progs = get_progs_or_fail (PC.parse_and_compile_files files) in + let e_progs = progs.gil_progs in + let () = Gil_parsing.cache_labelled_progs (List.tl e_progs) in + let e_prog = snd (List.hd e_progs) in + let source_files = progs.source_files in + (e_prog, progs.init_data, Some source_files, Some progs.tl_ast) + + let parse_gil_file file = + let Gil_parsing.{ labeled_prog; init_data } = + Gil_parsing.parse_eprog_from_file file + in + let init_data = + match ID.of_yojson init_data with + | Ok d -> d + | Error e -> failwith e + in + (labeled_prog, init_data, None, None) + + let log_procs procs = + DL.log (fun m -> + let proc_to_yojson = + Proc.to_yojson Annot.to_yojson (fun x -> `Int x) + in + let procs_json = + Hashtbl.fold + (fun name proc acc -> (name, proc_to_yojson proc) :: acc) + procs [] + in + m ~json:procs_json "Got %d procs" (Hashtbl.length procs)) + + let f ~outfile ~no_unfold ~already_compiled files = + let e_prog, init_data, source_files_opt, tl_ast = + if already_compiled then parse_gil_file (List.hd files) + else compile_tl_files files + in + Command_line_utils.burn_gil ~init_data:(ID.to_yojson init_data) + ~pp_prog:Prog.pp_labeled e_prog outfile; + (* Prog.perform_syntax_checks e_prog; *) + let other_imports = + Command_line_utils.convert_other_imports PC.other_imports + in + let prog = Gil_parsing.eprog_to_prog ~other_imports e_prog in + L.verbose (fun m -> + m "@\nProgram as parsed:@\n%a@\n" Prog.pp_indexed prog); + let prog = Debugger_impl.preprocess_prog ~no_unfold prog in + (prog, init_data, source_files_opt, tl_ast) + end + + let process_files = Process_files.f + + let has_hit_breakpoint dbg = + match dbg.frames with + | [] -> false + | frame :: _ -> + if Hashtbl.mem dbg.breakpoints frame.source_path then + let breakpoints = Hashtbl.find dbg.breakpoints frame.source_path in + (* Currently only one breakpoint per line is supported *) + Breakpoints.mem frame.start_line breakpoints + else false + + let rec call_stack_to_frames call_stack next_proc_body_idx prog = + match call_stack with + | [] -> [] + | (se : Call_stack.stack_element) :: rest -> + let start_line, start_column, end_line, end_column, source_path = + (let* proc = Prog.get_proc prog se.pid in + let annot, _, _ = proc.proc_body.(next_proc_body_idx) in + let+ loc = Annot.get_origin_loc annot in + let Location.{ loc_start; loc_end; loc_source } = + location_to_display_location loc + in + ( loc_start.pos_line, + loc_start.pos_column, + loc_end.pos_line, + loc_end.pos_column, + loc_source )) + |> Option.value ~default:(0, 0, 0, 0, "") + in + (* TODO: make index guaranteed to be unique *) + let frame = + make_frame ~index:se.call_index ~name:se.pid ~source_path + ~start_line ~start_column ~end_line ~end_column + in + frame :: call_stack_to_frames rest se.call_index prog + + module Update_proc_state = struct + let get_cmd id = + match L.Log_queryer.get_report id with + | None -> + Fmt.failwith + "Unable to find report id '%a'. Check the logging level is set \ + correctly" + L.Report_id.pp id + | Some (content, type_) -> + if type_ <> Content_type.cmd then + Fmt.failwith + "Debugger: don't know how to handle report of type '%s'!" type_ + else + DL.show_report id ("Debugger.update...: Got report type " ^ type_); + content |> of_yojson_string Logging.ConfigReport.of_yojson + + let get_cur_cmd (cmd : Lifter.cmd_report) cfg = + match cmd.callstack with + | [] -> None + | (se : Call_stack.stack_element) :: _ -> ( + let proc = Prog.get_proc cfg.prog se.pid in + match proc with + | None -> None + | Some proc -> + let annot, _, cmd = proc.proc_body.(cmd.proc_line) in + Some (cmd, annot)) + + let create_variables (state : state_t option) (is_gil_file : bool) : + Variable.scope list * Variable.ts = + let variables = Hashtbl.create 0 in + (* New scope ids must be higher than last top level scope id to prevent + duplicate scope ids *) + let scope_id = ref (List.length top_level_scopes) in + let get_new_scope_id () = + let () = scope_id := !scope_id + 1 in + !scope_id + in + let lifted_scopes = + match state with + | None -> [] + | Some state -> + let store = State.get_store state |> Store.bindings in + let memory = State.get_heap state in + let lifted_scopes = + Lifter.add_variables ~store ~memory ~is_gil_file + ~get_new_scope_id variables + in + let pure_formulae_vars = get_pure_formulae_vars state in + let type_env_vars = get_type_env_vars state in + let pred_vars = get_pred_vars state in + let vars_list = + [ pure_formulae_vars; type_env_vars; pred_vars ] + in + let () = + List.iter2 + (fun (scope : Variable.scope) vars -> + Hashtbl.replace variables scope.id vars) + top_level_scopes vars_list + in + lifted_scopes + in + (lifted_scopes, variables) + + let f report_id cfg state = + let cmd = get_cmd report_id in + state.cur_report_id <- report_id; + state.frames <- + call_stack_to_frames cmd.callstack cmd.proc_line cfg.prog; + let lifted_scopes, variables = + create_variables (Some cmd.state) (is_gil_file cfg.source_file) + in + state.variables <- variables; + state.top_level_scopes <- + List.concat [ lifted_scopes; top_level_scopes ]; + (* TODO: fix *) + (* let () = dbg.errors <- cmd_result.errors in *) + state.cur_cmd <- get_cur_cmd cmd cfg + end + + let update_proc_state = Update_proc_state.f + + let show_result_errors = function + | Exec_res.RSucc _ -> [] + | Exec_res.RFail { errors; _ } -> errors |> List.map show_err_t + + let build_final_cmd_data content result prev_id branch_path debug_state = + let cmd = content |> of_yojson_string Logging.ConfigReport.of_yojson in + let proc_name = (List.hd cmd.callstack).pid in + let errors = show_result_errors result in + let unifys = unify_final_cmd prev_id ~proc_name result debug_state in + let exec_data = + Lift.make_executed_cmd_data Exec_map.Final prev_id cmd ~unifys ~errors + branch_path + in + (exec_data, cmd) + + module Execute_step = struct + open Verification.SAInterpreter.Logging + + type execute_step = + L.Report_id.t -> + ?branch_case:BranchCase.t -> + ?branch_path:BranchCase.path -> + debug_state -> + proc_state -> + stop_reason * L.Report_id.t option + + let get_branch_path prev_id case path state = + DL.log (fun m -> + m + ~json: + [ + ("id", L.Report_id.to_yojson prev_id); + ("lifter_state", state.lifter_state |> Lifter.dump); + ] + "Grabbing path for step..."); + let branch_path = + match path with + | Some path -> path + | None -> state.lifter_state |> Lifter.select_next_path case prev_id + in + DL.log (fun m -> + m + ~json:[ ("path", BranchCase.path_to_yojson branch_path) ] + "Got path"); + branch_path + + let check_cur_report_id = function + | None -> + failwith + "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 BranchCase.pp) branch_case); + let id = Option_utils.coalesce id default_next_id |> Option.get in + execute_step id ?branch_case dbg state + | Stop -> on_stop () + + module Handle_continue = struct + 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 + if type_ = Content_type.proc_init then ( + DL.log (fun m -> m "Debugger.%s: Skipping proc_init..." log_context); + on_proc_init ()) + else if + L.Log_queryer.get_cmd_results id + |> List.for_all (fun (_, content) -> + let result = + content |> of_yojson_string CmdResult.of_yojson + in + result.errors <> []) + then ( + DL.log (fun m -> + m "Debugger.%s: No non-error results; stepping again for EoB" + log_context); + 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 open Exec_map in + let cmd = content |> of_yojson_string ConfigReport.of_yojson in + let cmd_kind = + new_branch_cases + |> Option.fold ~none:Normal ~some:Exec_map.kind_of_cases + in + let unifys = get_unifys cur_report_id debug_state proc_state in + let exec_data = + Lift.make_executed_cmd_data cmd_kind cur_report_id cmd + ~unifys 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 (fun () -> + DL.log (fun m -> + m "STOP (%a)" L.Report_id.pp cur_report_id); + (Step, Some 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 (fun () -> + DL.log (fun m -> m "STOP (end)"); + (ReachedEnd, None)) + 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 + in + match cont_func ~path:branch_path () 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 + | Continue (cur_report_id, branch_path, new_branch_cases, cont_func) + -> + handle_continue f prev_id_in_frame cur_report_id branch_case + branch_path new_branch_cases cont_func debug_state proc_state) + end + + let execute_step = Execute_step.f + + module Launch_proc = struct + open Verification.SAInterpreter.Logging + + 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 id cmd branch_path new_branch_cases debug_state + = + let { proc_names; tl_ast; prog; _ } = debug_state in + let kind = + let cases = Option.value ~default:[] new_branch_cases in + Exec_map.kind_of_cases cases + in + let exec_data = Lift.make_executed_cmd_data kind id cmd branch_path in + Lifter.init_exn ~proc_name ~all_procs:proc_names tl_ast prog exec_data + + 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 = content |> of_yojson_string ConfigReport.of_yojson in + let lifter_state, handler_result = + init_lifter proc_name id cmd branch_path new_branch_cases + 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 () + 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 (fun () -> + DL.log (fun m -> m "STOP (%a)" L.Report_id.pp id); + (Step, Some id)) + 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 (cur_report_id, branch_path, new_branch_cases, cont_func) -> + handle_continue proc_name new_branch_cases branch_path cur_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 + + module Launch = struct + let build_debug_state file_name proc_name = + (* If the file is a GIL file, assume it is already compiled *) + let already_compiled = is_gil_file file_name in + let outfile, no_unfold = (None, false) in + (* TODO: Support debugging incremental mode *) + (* let incremental = false in *) + let prog, init_data, source_files, tl_ast = + process_files ~outfile ~no_unfold ~already_compiled [ file_name ] + in + let proc_name = + proc_name |> Option_utils.or_else (fun () -> failwith "No proc name!") + in + let proc_names = + prog.procs |> Hashtbl.to_seq + |> Seq.filter_map (fun (name, proc) -> + if Proc.(proc.proc_internal) then None else Some name) + |> List.of_seq + in + let report_state_base = L.Report_state.(clone global_state) in + let cfg = + let make ext = + make_base_debug_state ~source_file:file_name ?source_files ~prog + ?tl_ast ~main_proc_name:proc_name ~report_state_base ~init_data + ~proc_names ~cur_proc_name:proc_name ~ext () + in + let ext = Debugger_impl.init (make ()) in + make ext + in + cfg + + let make_state debug_state = { debug_state; procs = Hashtbl.create 0 } + + let f file_name proc_name : (t, string) result = + Fmt_tty.setup_std_outputs (); + PC.initialize !Config.current_exec_mode; + Config.stats := false; + 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 + 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 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 + + let jump_to_id id (state : t) = + let** proc_state = get_proc_state ~cmd_id:id state in + jump_state_to_id id state.debug_state proc_state + + 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 + + let step_until_cond + ?(reverse = false) + ?(branch_case : BranchCase.t option) + (cond : frame -> frame -> int -> int -> bool) + (debug_state : debug_state) + (proc_state : proc_state) : stop_reason = + let prev_id_in_frame = proc_state.cur_report_id in + let prev_frame = get_top_frame proc_state in + let prev_stack_depth = List.length proc_state.frames in + let rec aux () = + 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 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 start_proc proc_name state = + let { debug_state; procs } = state in + let++ proc_state, stop_reason = launch_proc proc_name debug_state in + Hashtbl.add procs proc_name proc_state; + debug_state.cur_proc_name <- proc_name; + stop_reason + + let terminate state = + L.Report_state.(activate global_state); + Verification.postprocess_files state.debug_state.source_files; + if !Config.stats then Statistics.print_statistics (); + L.wrap_up () + + let get_frames state = + let { frames; _ } = get_proc_state_exn state in + frames + + let get_scopes state = + let { top_level_scopes; _ } = get_proc_state_exn state in + top_level_scopes + + let get_variables (var_ref : int) (state : t) : Variable.t list = + let { variables; _ } = get_proc_state_exn state in + match Hashtbl.find_opt variables var_ref with + | None -> [] + | Some vars -> vars + + let get_exception_info state = + let proc_state = get_proc_state_exn state in + let error = List.hd proc_state.errors in + let non_mem_exception_info = + { id = Fmt.to_to_string Logging.pp_err error; description = None } + in + match error with + | Exec_err.ESt state_error -> ( + match state_error with + | StateErr.EMem merr -> + let tl_ast = state.debug_state.tl_ast in + Lifter.memory_error_to_exception_info + { error = merr; command = proc_state.cur_cmd; tl_ast } + | _ -> non_mem_exception_info) + | _ -> non_mem_exception_info + + let set_breakpoints source bp_list dbg = + let state = dbg |> get_proc_state_exn in + match source with + (* We can't set the breakpoints if we do not know the source file *) + | None -> () + | Some source -> + let bp_set = Breakpoints.of_list bp_list in + Hashtbl.replace state.breakpoints source bp_set + end +end diff --git a/GillianCore/debugging/debugger/debugger.ml b/GillianCore/debugging/debugger/debugger.ml index e1aff392d..e9b6356cc 100644 --- a/GillianCore/debugging/debugger/debugger.ml +++ b/GillianCore/debugging/debugger/debugger.ml @@ -1,1105 +1,3 @@ include Debugger_intf -open Syntaxes.Option -module L = Logging -module DL = Debugger_log -module Lift = Debugger_lifter -module Exec_map = Exec_map - -let ( let** ) = Result.bind -let ( let++ ) f o = Result.map o f - -module Make : Make = -functor - (ID : Init_data.S) - (PC : ParserAndCompiler.S with type init_data = ID.t) - (Verification : Verifier.S - with type SPState.init_data = ID.t - and type annot = PC.Annot.t) - (Lifter : Lift.S - with type memory = Verification.SAInterpreter.heap_t - and type memory_error = Verification.SPState.m_err_t - and type tl_ast = PC.tl_ast - and type cmd_report = - Verification.SAInterpreter.Logging.ConfigReport.t - and type annot = PC.Annot.t) - -> - struct - open Verification.SAInterpreter - module Gil_parsing = Gil_parsing.Make (PC.Annot) - module Breakpoints = Set.Make (Int) - module Annot = PC.Annot - module Content_type = L.Logging_constants.Content_type - - type breakpoints = (string, Breakpoints.t) Hashtbl.t - type tl_ast = PC.tl_ast - type unify_result = Unify_map.unify_result = Success | Failure - - let build_unify_map = - let module Build = Unify_map.Make_builder (Verification) in - Build.f - - type debug_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; - (* 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; - mutable frames : frame list; - mutable variables : Variable.ts; [@default Hashtbl.create 0] - mutable errors : err_t list; - mutable cur_cmd : (int Cmd.t * Annot.t) option; - mutable proc_name : string option; - mutable unify_maps : (L.Report_id.t * Unify_map.t) list; - lifter_state : Lifter.t; - report_state : L.Report_state.t; - } - [@@deriving make] - - type debug_cfg = { - source_file : string; - source_files : SourceFiles.t option; - prog : Verification.prog_t; - tl_ast : tl_ast option; - tests : (string * Verification.t) list; - main_proc_name : string; - report_state_base : L.Report_state.t; - init_data : ID.t; - } - [@@deriving make] - - type debug_state = { - cfg : debug_cfg; - procs : (string, debug_proc_state) Hashtbl.t; - mutable cur_proc_name : string; - } - - let get_proc_name_of_id id = - let content, type_ = - L.Log_queryer.get_report id - |> Option_utils.or_else (fun () -> - Fmt.failwith "Couldn't get report for %a" L.Report_id.pp id) - in - DL.log (fun m -> m "=== TYPE %s ===" type_); - if type_ <> L.Logging_constants.Content_type.cmd then - Fmt.failwith "Report %a is not type '%s'" L.Report_id.pp id - L.Logging_constants.Content_type.cmd; - let cmd = content |> of_yojson_string Logging.ConfigReport.of_yojson in - cmd.proc_name - - let get_proc_state ?cmd_id ?(activate_report_state = true) dbg = - let proc_name = - match cmd_id with - | Some cmd_id -> - let proc_name = get_proc_name_of_id cmd_id in - dbg.cur_proc_name <- proc_name; - proc_name - | None -> dbg.cur_proc_name - in - match Hashtbl.find_opt dbg.procs proc_name with - | None -> Error ("get_proc_state: couldn't find proc " ^ proc_name) - | Some proc_state -> - if activate_report_state then - L.Report_state.activate proc_state.report_state; - Ok proc_state - - let get_proc_state_exn ?cmd_id ?(activate_report_state = true) dbg = - match get_proc_state ?cmd_id ~activate_report_state dbg with - | Ok proc_state -> proc_state - | Error msg -> failwith msg - - module Inspect = struct - type debug_proc_state_view = { - exec_map : Exec_map.Packaged.t; [@key "execMap"] - lifted_exec_map : Exec_map.Packaged.t option; [@key "liftedExecMap"] - current_cmd_id : L.Report_id.t; [@key "currentCmdId"] - unifys : Exec_map.unification list; - proc_name : string; [@key "procName"] - } - [@@deriving yojson] - - let procs_to_yosjon procs : Yojson.Safe.t = - let procs = - procs - |> List.map (fun (k, v) -> (k, debug_proc_state_view_to_yojson v)) - in - `Assoc procs - - let procs_of_yojson json = - let procs = - json |> Yojson.Safe.Util.to_assoc - |> List_utils.map_results (fun (k, v) -> - let++ v' = debug_proc_state_view_of_yojson v in - (k, v')) - in - procs - - type debug_state_view = { - main_proc_name : string; [@key "mainProc"] - current_proc_name : string; [@key "currentProc"] - procs : (string * debug_proc_state_view) list; - [@to_yojson procs_to_yosjon] [@of_yojson procs_of_yojson] - } - [@@deriving yojson] - - let get_debug_state (dbg : debug_state) : debug_state_view = - DL.log (fun m -> m "Getting debug state"); - let procs = - Hashtbl.fold - (fun proc_name state acc -> - let current_cmd_id = state.cur_report_id in - let unifys = - state.lifter_state |> Lifter.get_unifys_at_id current_cmd_id - in - let exec_map = state.lifter_state |> Lifter.get_gil_map in - let lifted_exec_map = - state.lifter_state |> Lifter.get_lifted_map - in - let proc = - { exec_map; lifted_exec_map; current_cmd_id; unifys; proc_name } - in - (proc_name, proc) :: acc) - dbg.procs [] - in - DL.log (fun m -> m "Got debug state"); - { - main_proc_name = dbg.cfg.main_proc_name; - current_proc_name = dbg.cur_proc_name; - procs; - } - - let get_unification unify_id dbg = - let state = dbg |> get_proc_state_exn in - match state.unify_maps |> List.assoc_opt unify_id with - | Some map -> (unify_id, map) - | None -> - let map = build_unify_map unify_id in - state.unify_maps <- (unify_id, map) :: state.unify_maps; - (unify_id, map) - end - - let top_level_scopes : Variable.scope list = - let top_level_scope_names = - (* [ "Store"; "Heap"; "Pure Formulae"; "Typing Environment"; "Predicates" ] *) - [ "Pure Formulae"; "Typing Environment"; "Predicates" ] - in - List.mapi - (fun i name -> Variable.{ name; id = i + 1 }) - top_level_scope_names - - let is_gil_file file_name = Filename.check_suffix file_name "gil" - - let get_pure_formulae_vars (state : state_t) : Variable.t list = - let open Variable in - Verification.SPState.get_pfs state - |> PFS.to_list - |> List.map (fun formula -> - let value = Fmt.to_to_string (Fmt.hbox Formula.pp) formula in - { name = ""; value; type_ = None; var_ref = 0 }) - |> List.sort (fun v w -> Stdlib.compare v.value w.value) - - let get_type_env_vars (state : state_t) : Variable.t list = - let open Variable in - let typ_env = Verification.SPState.get_typ_env state in - Type_env.to_list typ_env - |> List.sort (fun (v, _) (w, _) -> Stdlib.compare v w) - |> List.map (fun (name, value) -> - let value = Type.str value in - { name; value; type_ = None; var_ref = 0 }) - |> List.sort (fun v w -> Stdlib.compare v.name w.name) - - let get_pred_vars (state : state_t) : Variable.t list = - let open Variable in - Verification.SPState.get_preds state - |> Preds.SPreds.to_list - |> List.map (fun pred -> - let value = - Fmt.to_to_string (Fmt.hbox Preds.SPreds.pp_pabs) pred - in - { name = ""; value; type_ = None; var_ref = 0 }) - |> List.sort (fun v w -> Stdlib.compare v.value w.value) - - module Preprocess_files = struct - let get_progs_or_fail = function - | Ok progs -> ( - match progs.ParserAndCompiler.gil_progs with - | [] -> - Fmt.pr "Error: expected at least one GIL program\n"; - exit 1 - | _ -> progs) - | Error err -> - Fmt.pr "Error during compilation to GIL:\n%a" PC.pp_err err; - exit 1 - - let compile_tl_files files = - let progs = get_progs_or_fail (PC.parse_and_compile_files files) in - let e_progs = progs.gil_progs in - let () = Gil_parsing.cache_labelled_progs (List.tl e_progs) in - let e_prog = snd (List.hd e_progs) in - let source_files = progs.source_files in - (e_prog, progs.init_data, Some source_files, Some progs.tl_ast) - - let parse_gil_file file = - let Gil_parsing.{ labeled_prog; init_data } = - Gil_parsing.parse_eprog_from_file file - in - let init_data = - match ID.of_yojson init_data with - | Ok d -> d - | Error e -> failwith e - in - (labeled_prog, init_data, None, None) - - let log_procs procs = - DL.log (fun m -> - let proc_to_yojson = - Proc.to_yojson Annot.to_yojson (fun x -> `Int x) - in - let procs_json = - Hashtbl.fold - (fun name proc acc -> (name, proc_to_yojson proc) :: acc) - procs [] - in - m ~json:procs_json "Got %d procs" (Hashtbl.length procs)) - - let f files already_compiled outfile_opt no_unfold = - let e_prog, init_data, source_files_opt, tl_ast = - if already_compiled then parse_gil_file (List.hd files) - else compile_tl_files files - in - Command_line_utils.burn_gil ~init_data:(ID.to_yojson init_data) - ~pp_prog:Prog.pp_labeled e_prog outfile_opt; - (* Prog.perform_syntax_checks e_prog; *) - let other_imports = - Command_line_utils.convert_other_imports PC.other_imports - in - let prog = Gil_parsing.eprog_to_prog ~other_imports e_prog in - L.verbose (fun m -> - m "@\nProgram as parsed:@\n%a@\n" Prog.pp_indexed prog); - let prog = LogicPreprocessing.preprocess prog (not no_unfold) in - L.verbose (fun m -> - m "@\nProgram after logic preprocessing:@\n%a@\n" Prog.pp_indexed - prog); - log_procs prog.procs; - (prog, init_data, source_files_opt, tl_ast) - end - - let preprocess_files = Preprocess_files.f - - let has_hit_breakpoint dbg = - match dbg.frames with - | [] -> false - | frame :: _ -> - if Hashtbl.mem dbg.breakpoints frame.source_path then - let breakpoints = Hashtbl.find dbg.breakpoints frame.source_path in - (* Currently only one breakpoint per line is supported *) - Breakpoints.mem frame.start_line breakpoints - else false - - let rec call_stack_to_frames call_stack next_proc_body_idx prog = - match call_stack with - | [] -> [] - | (se : Call_stack.stack_element) :: rest -> - let start_line, start_column, end_line, end_column, source_path = - (let* proc = Prog.get_proc prog se.pid in - let annot, _, _ = proc.proc_body.(next_proc_body_idx) in - let+ loc = Annot.get_origin_loc annot in - let Location.{ loc_start; loc_end; loc_source } = - location_to_display_location loc - in - ( loc_start.pos_line, - loc_start.pos_column, - loc_end.pos_line, - loc_end.pos_column, - loc_source )) - |> Option.value ~default:(0, 0, 0, 0, "") - in - (* TODO: make index guaranteed to be unique *) - let frame = - make_frame ~index:se.call_index ~name:se.pid ~source_path - ~start_line ~start_column ~end_line ~end_column - in - frame :: call_stack_to_frames rest se.call_index prog - - module Update_proc_state = struct - let get_cmd id = - match L.Log_queryer.get_report id with - | None -> - Fmt.failwith - "Unable to find report id '%a'. Check the logging level is set \ - correctly" - L.Report_id.pp id - | Some (content, type_) -> - if type_ <> Content_type.cmd then - Fmt.failwith - "Debugger: don't know how to handle report of type '%s'!" type_ - else - DL.show_report id ("Debugger.update...: Got report type " ^ type_); - content |> of_yojson_string Logging.ConfigReport.of_yojson - - let get_cur_cmd (cmd : Lifter.cmd_report) cfg = - match cmd.callstack with - | [] -> None - | (se : Call_stack.stack_element) :: _ -> ( - let proc = Prog.get_proc cfg.prog se.pid in - match proc with - | None -> None - | Some proc -> - let annot, _, cmd = proc.proc_body.(cmd.proc_line) in - Some (cmd, annot)) - - let create_variables (state : state_t option) (is_gil_file : bool) : - Variable.scope list * Variable.ts = - let variables = Hashtbl.create 0 in - (* New scope ids must be higher than last top level scope id to prevent - duplicate scope ids *) - let scope_id = ref (List.length top_level_scopes) in - let get_new_scope_id () = - let () = scope_id := !scope_id + 1 in - !scope_id - in - let lifted_scopes = - match state with - | None -> [] - | Some state -> - let store = - Verification.SPState.get_store state |> Store.bindings - in - let memory = Verification.SPState.get_heap state in - let lifted_scopes = - Lifter.add_variables ~store ~memory ~is_gil_file - ~get_new_scope_id variables - in - let pure_formulae_vars = get_pure_formulae_vars state in - let type_env_vars = get_type_env_vars state in - let pred_vars = get_pred_vars state in - let vars_list = - [ pure_formulae_vars; type_env_vars; pred_vars ] - in - let () = - List.iter2 - (fun (scope : Variable.scope) vars -> - Hashtbl.replace variables scope.id vars) - top_level_scopes vars_list - in - lifted_scopes - in - (lifted_scopes, variables) - - let f report_id cfg state = - let cmd = get_cmd report_id in - state.cur_report_id <- report_id; - state.frames <- - call_stack_to_frames cmd.callstack cmd.proc_line cfg.prog; - let lifted_scopes, variables = - create_variables (Some cmd.state) (is_gil_file cfg.source_file) - in - state.variables <- variables; - state.top_level_scopes <- - List.concat [ lifted_scopes; top_level_scopes ]; - (* TODO: fix *) - (* let () = dbg.errors <- cmd_result.errors in *) - state.cur_cmd <- get_cur_cmd cmd cfg - end - - let update_proc_state = Update_proc_state.f - - module Unify = struct - open Verification.SUnifier.Logging - - let get_test dbg proc_name = - match dbg.tests |> List.assoc_opt proc_name with - | None -> - DL.failwith - (fun () -> - let tests_json = Verification.proc_tests_to_yojson dbg.tests in - [ ("tests", tests_json) ]) - (Fmt.str "No test found for proc `%s`!" proc_name) - | Some test -> test - - let is_unify_successful id = - L.Log_queryer.get_unify_results id - |> List.exists (fun (_, content) -> - let result = - content |> Yojson.Safe.from_string - |> UnifyResultReport.of_yojson |> Result.get_ok - in - match result with - | Success _ -> true - | Failure _ -> false) - - let do_unify prev_id test result = - DL.log (fun m -> m "Unifying result for %a" L.Report_id.pp prev_id); - let success = Verification.Debug.analyse_result test prev_id result in - let+ id, content = L.Log_queryer.get_unify_for prev_id in - (id, content, success) - - let f result proc_name prev_id dbg = - let test = get_test dbg proc_name in - let+ id, content, success = - match L.Log_queryer.get_unify_for prev_id with - | Some (id, content) -> Some (id, content, is_unify_successful id) - | None -> do_unify prev_id test result - in - let unify_report = content |> of_yojson_string UnifyReport.of_yojson in - let kind = unify_report.unify_kind in - let result = if success then Success else Failure in - (id, kind, result) - end - - let unify = Unify.f - - let show_result_errors = function - | Exec_res.RSucc _ -> [] - | Exec_res.RFail { errors; _ } -> errors |> List.map show_err_t - - let build_final_cmd_data content result prev_id branch_path dbg = - let { cfg; _ } = dbg in - let cmd = content |> of_yojson_string Logging.ConfigReport.of_yojson in - let proc_name = (List.hd cmd.callstack).pid in - let errors = show_result_errors result in - let unifys = - match unify result proc_name prev_id cfg with - | None -> [] - | Some (id, kind, result) -> [ Exec_map.{ id; kind; result } ] - in - let exec_data = - Lift.make_executed_cmd_data Exec_map.Final prev_id cmd ~unifys ~errors - branch_path - in - (exec_data, cmd) - - module Execute_step = struct - open Verification.SAInterpreter.Logging - - type execute_step = - L.Report_id.t -> - ?branch_case:BranchCase.t -> - ?branch_path:BranchCase.path -> - debug_state -> - debug_proc_state -> - stop_reason * L.Report_id.t option - - let get_branch_path prev_id case path state = - DL.log (fun m -> - m - ~json: - [ - ("id", L.Report_id.to_yojson prev_id); - ("lifter_state", state.lifter_state |> Lifter.dump); - ] - "Grabbing path for step..."); - let branch_path = - match path with - | Some path -> path - | None -> state.lifter_state |> Lifter.select_next_path case prev_id - in - DL.log (fun m -> - m - ~json:[ ("path", BranchCase.path_to_yojson branch_path) ] - "Got path"); - branch_path - - let check_cur_report_id = function - | None -> - failwith - "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 BranchCase.pp) branch_case); - let id = Option_utils.coalesce id default_next_id |> Option.get in - execute_step id ?branch_case dbg state - | Stop -> on_stop () - - module Handle_continue = struct - let get_unifys cur_report_id state = - let unify = - DL.log (fun m -> - m "getting unify_result for %a" L.Report_id.pp cur_report_id); - let+ unify_id, _ = L.Log_queryer.get_unify_for cur_report_id in - let unify_map = - match state.unify_maps |> List.assoc_opt unify_id with - | Some map -> map - | None -> - let map = build_unify_map unify_id in - state.unify_maps <- (unify_id, map) :: state.unify_maps; - map - in - let result = unify_map |> Unify_map.result in - (unify_id, fst unify_map, result) - in - match unify with - | None -> [] - | Some (id, kind, result) -> [ Exec_map.{ id; kind; result } ] - - 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 - if type_ = Content_type.proc_init then ( - DL.log (fun m -> m "Debugger.%s: Skipping proc_init..." log_context); - on_proc_init ()) - else if - L.Log_queryer.get_cmd_results id - |> List.for_all (fun (_, content) -> - let result = - content |> of_yojson_string CmdResult.of_yojson - in - result.errors <> []) - then ( - DL.log (fun m -> - m "Debugger.%s: No non-error results; stepping again for EoB" - log_context); - 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 - dbg - state = - let { cfg; _ } = dbg in - let cur_report_id = check_cur_report_id cur_report_id in - state.cont_func <- Some cont_func; - cur_report_id - |> get_report_and_check_type - ~on_proc_init:(fun () -> - state |> execute_step prev_id_in_frame dbg) - ~on_eob:(fun () -> - state |> execute_step ~branch_path cur_report_id dbg) - ~continue:(fun content -> - state |> update_proc_state cur_report_id cfg; - let open Exec_map in - let cmd = content |> of_yojson_string ConfigReport.of_yojson in - let cmd_kind = - new_branch_cases - |> Option.fold ~none:Normal ~some:Exec_map.kind_of_cases - in - let unifys = get_unifys cur_report_id state in - let exec_data = - Lift.make_executed_cmd_data cmd_kind cur_report_id cmd - ~unifys branch_path - in - 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 dbg state (fun () -> - DL.log (fun m -> - m "STOP (%a)" L.Report_id.pp cur_report_id); - (Step, Some 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 - state - dbg = - let { cfg; _ } = dbg in - 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 dbg - in - state |> update_proc_state prev_id cfg; - state.lifter_state - |> Lifter.handle_cmd prev_prev_id cmd.branch_case exec_data - |> handle_lifter_result execute_step dbg state (fun () -> - DL.log (fun m -> m "STOP (end)"); - (ReachedEnd, None)) - end - - let handle_end_of_branch = Handle_end_of_branch.f - - let rec f prev_id_in_frame ?branch_case ?branch_path dbg state = - let open Verification.SAInterpreter in - match 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 state - in - match cont_func ~path:branch_path () with - | Finished _ -> - 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 state dbg - | Continue (cur_report_id, branch_path, new_branch_cases, cont_func) - -> - handle_continue f prev_id_in_frame cur_report_id branch_case - branch_path new_branch_cases cont_func dbg state) - end - - let execute_step = Execute_step.f - - module Launch_proc = struct - open Verification.SAInterpreter.Logging - - let handle_end_of_branch - proc_name - result - prev_id - report_state - cont_func - dbg = - let { cfg; _ } = dbg in - 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 [] dbg - in - Lifter.init_exn proc_name cfg.tl_ast exec_data - in - let state = - make_debug_proc_state ~cont_func ~cur_report_id:prev_id - ~top_level_scopes ~lifter_state ~report_state () - in - state |> update_proc_state prev_id cfg; - Ok (state, ReachedEnd) - - let init_lifter proc_name id cmd branch_path new_branch_cases dbg = - let { cfg; _ } = dbg in - let kind = - let cases = Option.value ~default:[] new_branch_cases in - Exec_map.kind_of_cases cases - in - let exec_data = Lift.make_executed_cmd_data kind id cmd branch_path in - Lifter.init_exn proc_name cfg.tl_ast exec_data - - 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 - dbg = - let { cfg; _ } = dbg in - 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 = content |> of_yojson_string ConfigReport.of_yojson in - let lifter_state, handler_result = - init_lifter proc_name id cmd branch_path new_branch_cases dbg - in - let proc_state = - make_debug_proc_state ~cont_func ~cur_report_id:id - ~top_level_scopes ~lifter_state ~report_state () - in - let stop_reason, id = - handler_result - |> Execute_step.handle_lifter_result execute_step - ~default_next_id:id dbg proc_state (fun () -> - DL.log (fun m -> m "STOP (%a)" L.Report_id.pp id); - (Step, Some id)) - in - let id = id |> Option.get in - proc_state |> update_proc_state id cfg; - Ok (proc_state, stop_reason)) - - let rec build_proc_state proc_name report_state dbg prev_id cont_func = - let build_proc_state = build_proc_state proc_name report_state dbg 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 - dbg - | Continue (cur_report_id, branch_path, new_branch_cases, cont_func) -> - handle_continue proc_name new_branch_cases branch_path cur_report_id - build_proc_state cont_func report_state dbg - - let do_launch proc_name report_state dbg () = - let { cfg; _ } = dbg in - let cont_func = - Verification.verify_up_to_procs ~init_data:cfg.init_data ~proc_name - cfg.prog - in - build_proc_state proc_name report_state dbg None cont_func - - let f proc_name dbg = - let { cfg; _ } = dbg in - let report_state = L.Report_state.clone cfg.report_state_base in - Config.Verification.( - let procs_to_verify = !procs_to_verify in - if not (procs_to_verify |> List.mem proc_name) then - set_procs_to_verify (procs_to_verify @ [ proc_name ])); - report_state - |> L.Report_state.with_state (do_launch proc_name report_state dbg) - end - - let launch_proc = Launch_proc.f - - module Launch = struct - let build_debug_cfg file_name proc_name = - (* If the file is a GIL file, assume it is already compiled *) - let already_compiled = is_gil_file file_name in - let outfile_opt, no_unfold = (None, false) in - (* TODO: Support debugging incremental mode *) - (* let incremental = false in *) - let prog, init_data, source_files, tl_ast = - preprocess_files [ file_name ] already_compiled outfile_opt no_unfold - in - let tests = Verification.Debug.get_tests_for_prog ~init_data prog in - let proc_name = - proc_name |> Option_utils.or_else (fun () -> tests |> List.hd |> fst) - in - let report_state_base = L.Report_state.(clone global_state) in - let cfg = - make_debug_cfg ~source_file:file_name ?source_files ~prog ?tl_ast - ~tests ~main_proc_name:proc_name ~report_state_base ~init_data () - in - (cfg, proc_name) - - let f file_name proc_name = - Fmt_tty.setup_std_outputs (); - Config.current_exec_mode := Verification; - PC.initialize Verification; - Config.stats := false; - Config.lemma_proof := true; - proc_name - |> Option.iter (fun proc_name -> - Config.Verification.set_procs_to_verify [ proc_name ]); - let cfg, proc_name = build_debug_cfg file_name proc_name in - let dbg = - { cfg; procs = Hashtbl.create 0; cur_proc_name = proc_name } - in - let++ main_proc_state, _ = dbg |> launch_proc proc_name in - main_proc_state.report_state |> L.Report_state.activate; - Hashtbl.add dbg.procs proc_name main_proc_state; - dbg - end - - let launch = Launch.f - - 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 - - let jump_to_id id dbg = - let { cfg; _ } = dbg in - let** state = dbg |> get_proc_state ~cmd_id:id in - state |> jump_state_to_id id cfg - - let jump_to_start dbg = - let { cfg; _ } = dbg in - let state = dbg |> get_proc_state_exn in - let result = - let** root_id = - state.lifter_state |> Lifter.get_root_id - |> Option.to_result ~none:"Debugger.jump_to_start: No root id found!" - in - state |> jump_state_to_id root_id cfg - in - match result with - | Error msg -> failwith msg - | Ok () -> () - - module Step_in_branch_case = struct - let step_backwards state dbg = - let { cfg; _ } = dbg in - match - state.lifter_state |> Lifter.previous_step state.cur_report_id - with - | None -> ReachedStart - | Some (prev_id, _) -> - state |> update_proc_state prev_id cfg; - 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 state dbg = - let { cfg; _ } = dbg in - let next_id = - match - state.lifter_state |> Lifter.existing_next_steps 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"); - state |> execute_step ?branch_case prev_id_in_frame dbg |> fst - | Some id -> - DL.show_report id "Next report ID found; not executing"; - state |> update_proc_state id cfg; - Step - - let f prev_id_in_frame ?branch_case ?(reverse = false) dbg state = - let stop_reason = - if reverse then step_backwards state dbg - else step_forwards prev_id_in_frame branch_case state dbg - in - if has_hit_breakpoint state then Breakpoint - else if List.length state.errors > 0 then - let () = state.cont_func <- None in - ExecutionError - else stop_reason - end - - let step_in_branch_case = Step_in_branch_case.f - - let step_in_state ?(reverse = false) cfg state = - step_in_branch_case state.cur_report_id ?branch_case:None ~reverse cfg - state - - let step_in ?(reverse = false) dbg = - let state = dbg |> get_proc_state_exn in - step_in_state ~reverse dbg state - - module Step_case = struct - let get_top_frame state = - match state.frames with - | [] -> failwith "Nothing in call stack, cannot step" - | cur_frame :: _ -> cur_frame - - let step_until_cond - ?(reverse = false) - ?(branch_case : BranchCase.t option) - (cond : frame -> frame -> int -> int -> bool) - (dbg : debug_state) - (state : debug_proc_state) : stop_reason = - let prev_id_in_frame = state.cur_report_id in - let prev_frame = get_top_frame state in - let prev_stack_depth = List.length state.frames in - let rec aux () = - let stop_reason = - step_in_branch_case ~reverse ?branch_case prev_id_in_frame dbg state - in - match stop_reason with - | Step -> - let cur_frame = get_top_frame state in - let cur_stack_depth = List.length 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 get_cond dbg = - let { cfg; _ } = dbg in - if is_gil_file cfg.source_file then is_next_gil_step - else is_next_tl_step - - let f ?(reverse = false) ?branch_case dbg state = - let cond = get_cond dbg in - state |> step_until_cond ~reverse ?branch_case cond dbg - end - - let step_case = Step_case.f - - let step ?(reverse = false) dbg = - let state = dbg |> get_proc_state_exn in - step_case ~reverse dbg state - - let step_specific branch_case prev_id dbg = - let { cfg; _ } = dbg in - let** state = dbg |> get_proc_state ~cmd_id:prev_id in - let id, branch_case = - state.lifter_state |> Lifter.next_gil_step prev_id branch_case - in - let++ () = state |> jump_state_to_id id cfg in - state |> step_case ?branch_case dbg - - let step_out dbg = - let state = dbg |> get_proc_state_exn in - let rec aux stack_depth = - let stop_reason = state |> step_in_state dbg in - match stop_reason with - | Step -> - if List.length state.frames < stack_depth then stop_reason - else aux stack_depth - | other_stop_reason -> other_stop_reason - in - aux (List.length state.frames) - - 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 dbg state = - let { cfg; _ } = dbg in - let unfinished = - 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) -> ( - state |> jump_state_to_id prev_id cfg |> Result.get_ok; - let stop_reason = step_case ?branch_case dbg state in - match stop_reason with - | Step -> on_step () - | Breakpoint -> Breakpoint - | _ -> on_other_reason ()) - - let f ?(reverse = false) ?(launch = false) dbg = - let state = dbg |> get_proc_state_exn in - let current_id = state.cur_report_id in - log_run current_id 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 state then Breakpoint - else if reverse then run_backwards ~on_step dbg state - else run_forwards ~on_step ~on_other_reason current_id dbg state - in - aux ~launch 0 - end - - let run = Run.f - - let start_proc proc_name dbg = - let++ proc_state, stop_reason = dbg |> launch_proc proc_name in - Hashtbl.add dbg.procs proc_name proc_state; - dbg.cur_proc_name <- proc_name; - stop_reason - - let terminate dbg = - L.Report_state.(activate global_state); - Verification.postprocess_files dbg.cfg.source_files; - if !Config.stats then Statistics.print_statistics (); - L.wrap_up () - - let get_frames dbg = - let state = dbg |> get_proc_state_exn in - state.frames - - let get_scopes dbg = - let state = dbg |> get_proc_state_exn in - state.top_level_scopes - - let get_variables (var_ref : int) (dbg : debug_state) : Variable.t list = - let state = dbg |> get_proc_state_exn in - match Hashtbl.find_opt state.variables var_ref with - | None -> [] - | Some vars -> vars - - let get_exception_info (dbg : debug_state) = - let { cfg; _ } = dbg in - let state = dbg |> get_proc_state_exn in - let error = List.hd state.errors in - let non_mem_exception_info = - { id = Fmt.to_to_string Logging.pp_err error; description = None } - in - match error with - | Exec_err.ESt state_error -> ( - match state_error with - | StateErr.EMem merr -> - Lifter.memory_error_to_exception_info - { error = merr; command = state.cur_cmd; tl_ast = cfg.tl_ast } - | _ -> non_mem_exception_info) - | _ -> non_mem_exception_info - - let set_breakpoints source bp_list dbg = - let state = dbg |> get_proc_state_exn in - match source with - (* We can't set the breakpoints if we do not know the source file *) - | None -> () - | Some source -> - let bp_set = Breakpoints.of_list bp_list in - Hashtbl.replace state.breakpoints source bp_set - end +module Symbolic_debugger = Symbolic_debugger +module Verification_debugger = Verification_debugger diff --git a/GillianCore/debugging/debugger/debugger_intf.ml b/GillianCore/debugging/debugger/debugger_intf.ml index 1806221be..973063c08 100644 --- a/GillianCore/debugging/debugger/debugger_intf.ml +++ b/GillianCore/debugging/debugger/debugger_intf.ml @@ -1,37 +1,35 @@ module type S = sig type tl_ast - type debug_state + type t module Inspect : sig type debug_state_view [@@deriving yojson] - val get_debug_state : debug_state -> debug_state_view - - val get_unification : - Logging.Report_id.t -> debug_state -> Logging.Report_id.t * Unify_map.t + val get_debug_state : t -> debug_state_view + val get_unify_map : Logging.Report_id.t -> t -> Unify_map.t end - val launch : string -> string option -> (debug_state, string) result - val jump_to_id : Logging.Report_id.t -> debug_state -> (unit, string) result - val jump_to_start : debug_state -> unit - val step_in : ?reverse:bool -> debug_state -> stop_reason - val step : ?reverse:bool -> debug_state -> stop_reason + 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 : ?reverse:bool -> t -> stop_reason val step_specific : Exec_map.Packaged.branch_case option -> Logging.Report_id.t -> - debug_state -> + t -> (stop_reason, string) result - val step_out : debug_state -> stop_reason - val run : ?reverse:bool -> ?launch:bool -> debug_state -> stop_reason - val start_proc : string -> debug_state -> (stop_reason, string) result - val terminate : debug_state -> unit - val get_frames : debug_state -> frame list - val get_scopes : debug_state -> Variable.scope list - val get_variables : int -> debug_state -> Variable.t list - val get_exception_info : debug_state -> exception_info - val set_breakpoints : string option -> int list -> debug_state -> unit + val step_out : t -> stop_reason + val run : ?reverse:bool -> ?launch:bool -> t -> stop_reason + val start_proc : string -> t -> (stop_reason, string) result + val terminate : t -> unit + val get_frames : t -> frame list + val get_scopes : t -> Variable.scope list + val get_variables : int -> t -> Variable.t list + val get_exception_info : t -> exception_info + val set_breakpoints : string option -> int list -> t -> unit end module type Make = functor @@ -56,6 +54,11 @@ module type Intf = sig (**/**) - (** @canonical Gillian.Debugger.Make *) - module Make : Make + module Verification_debugger : sig + module Make : Make + end + + module Symbolic_debugger : sig + module Make : Make + end end diff --git a/GillianCore/debugging/debugger/symbolic_debugger.ml b/GillianCore/debugging/debugger/symbolic_debugger.ml new file mode 100644 index 000000000..3dc9a0a43 --- /dev/null +++ b/GillianCore/debugging/debugger/symbolic_debugger.ml @@ -0,0 +1,47 @@ +module Make + (ID : Init_data.S) + (PC : ParserAndCompiler.S with type init_data = ID.t) + (Verification : Verifier.S + with type SPState.init_data = ID.t + and type annot = PC.Annot.t) + (Lifter : Debugger_lifter.S + with type memory = Verification.SAInterpreter.heap_t + and type memory_error = Verification.SPState.m_err_t + and type tl_ast = PC.tl_ast + and type cmd_report = + Verification.SAInterpreter.Logging.ConfigReport.t + and type annot = PC.Annot.t) = +struct + open Base_debugger.Premake (ID) (PC) (Verification) (Lifter) + + module Impl : Debugger_impl = struct + type proc_state_ext = unit + type debug_state_ext = unit + + let preprocess_prog ~no_unfold:_ prog = prog + let init _ = () + let init_proc _ _ = () + + let launch_proc ~proc_name (debug_state : debug_state_ext base_debug_state) + = + let prog = + match UP.init_prog debug_state.prog with + | Error _ -> failwith "Creation of unification plans failed" + | Ok prog -> prog + in + Verification.SAInterpreter.init_evaluate_proc + (fun x -> x) + prog proc_name [] + (State.init debug_state.init_data) + + module Unify = struct + let unify_final_cmd _ ~proc_name:_ _ _ = [] + let get_unifys _ _ _ = [] + + let get_unify_map _ _ = + failwith "Can't get unification in symbolic debugging!" + end + end + + include Make (Impl) +end diff --git a/GillianCore/debugging/debugger/verification_debugger.ml b/GillianCore/debugging/debugger/verification_debugger.ml new file mode 100644 index 000000000..b84373188 --- /dev/null +++ b/GillianCore/debugging/debugger/verification_debugger.ml @@ -0,0 +1,139 @@ +open Syntaxes.Option +module L = Logging +module DL = Debugger_log + +module Make + (ID : Init_data.S) + (PC : ParserAndCompiler.S with type init_data = ID.t) + (Verification : Verifier.S + with type SPState.init_data = ID.t + and type annot = PC.Annot.t) + (Lifter : Debugger_lifter.S + with type memory = Verification.SAInterpreter.heap_t + and type memory_error = Verification.SPState.m_err_t + and type tl_ast = PC.tl_ast + and type cmd_report = + Verification.SAInterpreter.Logging.ConfigReport.t + and type annot = PC.Annot.t) = +struct + open Base_debugger.Premake (ID) (PC) (Verification) (Lifter) + + module Impl : Debugger_impl = struct + type proc_state_ext = unit + + type debug_state_ext = { + mutable unify_maps : (L.Report_id.t * Unify_map.t) list; + tests : (string * Verification.t) list; + } + + let preprocess_prog ~no_unfold prog = + LogicPreprocessing.preprocess prog (not no_unfold) + + let init (debug_state : unit base_debug_state) = + let { init_data; prog; main_proc_name; _ } = debug_state in + Config.Verification.set_procs_to_verify [ main_proc_name ]; + let tests = Verification.Debug.get_tests_for_prog ~init_data prog in + { tests; unify_maps = [] } + + let init_proc _ _ = () + + let launch_proc ~proc_name (debug_state : debug_state_ext base_debug_state) + = + Config.Verification.( + let procs_to_verify = !procs_to_verify in + if not (procs_to_verify |> List.mem proc_name) then + set_procs_to_verify (procs_to_verify @ [ proc_name ])); + Verification.verify_up_to_procs ~init_data:debug_state.init_data + ~proc_name debug_state.prog + + module Unify = struct + open Verification.SUnifier.Logging + + type unify_result = Unify_map.unify_result = Success | Failure + + module Build_map = Unify_map.Make_builder (Verification) + + let build_unify_map = Build_map.f + + let get_test debug_state proc_name = + let tests = debug_state.ext.tests in + match tests |> List.assoc_opt proc_name with + | None -> + DL.failwith + (fun () -> + let tests_json = Verification.proc_tests_to_yojson tests in + [ ("tests", tests_json) ]) + (Fmt.str "No test found for proc `%s`!" proc_name) + | Some test -> test + + let is_unify_successful id = + L.Log_queryer.get_unify_results id + |> List.exists (fun (_, content) -> + let result = + content |> Yojson.Safe.from_string + |> UnifyResultReport.of_yojson |> Result.get_ok + in + match result with + | Success _ -> true + | Failure _ -> false) + + let do_unify prev_id test result = + DL.log (fun m -> m "Unifying result for %a" L.Report_id.pp prev_id); + let success = Verification.Debug.analyse_result test prev_id result in + let+ id, content = L.Log_queryer.get_unify_for prev_id in + (id, content, success) + + let f result proc_name prev_id debug_state = + let test = get_test debug_state proc_name in + let+ id, content, success = + match L.Log_queryer.get_unify_for prev_id with + | Some (id, content) -> Some (id, content, is_unify_successful id) + | None -> do_unify prev_id test result + in + let unify_report = content |> of_yojson_string UnifyReport.of_yojson in + let kind = unify_report.unify_kind in + let result = if success then Success else Failure in + (id, kind, result) + + let get_unifys + cur_report_id + (debug_state : debug_state_ext base_debug_state) + _ = + let { ext; _ } = debug_state in + let unify = + DL.log (fun m -> + m "getting unify_result for %a" L.Report_id.pp cur_report_id); + let+ unify_id, _ = L.Log_queryer.get_unify_for cur_report_id in + let unify_map = + match ext.unify_maps |> List.assoc_opt unify_id with + | Some map -> map + | None -> + let map = build_unify_map unify_id in + ext.unify_maps <- (unify_id, map) :: ext.unify_maps; + map + in + let result = unify_map |> Unify_map.result in + (unify_id, fst unify_map, result) + in + match unify with + | None -> [] + | Some (id, kind, result) -> [ Exec_map.{ id; kind; result } ] + + let unify_final_cmd prev_id ~proc_name result debug_state = + match f result proc_name prev_id debug_state with + | None -> [] + | Some (id, kind, result) -> [ Exec_map.{ id; kind; result } ] + + let get_unify_map unify_id debug_state = + let ext = debug_state.ext in + match ext.unify_maps |> List.assoc_opt unify_id with + | Some map -> map + | None -> + let map = build_unify_map unify_id in + ext.unify_maps <- (unify_id, map) :: ext.unify_maps; + map + end + end + + include Make (Impl) +end diff --git a/GillianCore/debugging/lifter/gil_fallback_lifter.ml b/GillianCore/debugging/lifter/gil_fallback_lifter.ml index a6278fc58..f3be8a477 100644 --- a/GillianCore/debugging/lifter/gil_fallback_lifter.ml +++ b/GillianCore/debugging/lifter/gil_fallback_lifter.ml @@ -41,22 +41,25 @@ functor type cmd_report = Verifier.SAInterpreter.Logging.ConfigReport.t type annot = PC.Annot.t - let init_exn proc_name tl_ast exec_data = - let gil, gil_result = Gil_lifter.init_exn proc_name tl_ast exec_data in + 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 tl_ast exec_data with + 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 - let init proc_name tl_ast exec_data = - Some (init_exn proc_name tl_ast exec_data) + let init ~proc_name ~all_procs tl_ast prog exec_data = + Some (init_exn ~proc_name ~all_procs tl_ast prog exec_data) let dump = to_yojson let handle_cmd prev_id branch_case exec_data { gil; tl } = + (* TODO: defer skipping to TL lifter *) match gil |> Gil_lifter.handle_cmd prev_id branch_case exec_data with | Stop -> ( match tl with diff --git a/GillianCore/debugging/lifter/gil_fallback_lifter_intf.ml b/GillianCore/debugging/lifter/gil_fallback_lifter_intf.ml index ebd425944..c31e48754 100644 --- a/GillianCore/debugging/lifter/gil_fallback_lifter_intf.ml +++ b/GillianCore/debugging/lifter/gil_fallback_lifter_intf.ml @@ -1,5 +1,5 @@ module type Gil_lifter_with_state = sig - module Lifter : Lifter.S + module Lifter : Gil_lifter.S val get_state : unit -> Lifter.t end diff --git a/GillianCore/debugging/lifter/gil_lifter.ml b/GillianCore/debugging/lifter/gil_lifter.ml index 9cb3a375f..4f145d5b2 100644 --- a/GillianCore/debugging/lifter/gil_lifter.ml +++ b/GillianCore/debugging/lifter/gil_lifter.ml @@ -2,6 +2,12 @@ module L = Logging module DL = Debugger_log open Lifter +module type S = sig + include Lifter.S + + val pop_to_exec : t -> (Logging.Report_id.t * BranchCase.t option) option +end + module Make (PC : ParserAndCompiler.S) (Verifier : Verifier.S with type annot = PC.Annot.t) @@ -36,7 +42,9 @@ module Make type t = { 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 * BranchCase.t option) list; } [@@deriving to_yojson] @@ -65,18 +73,22 @@ module Make () = let display = Fmt.to_to_string Cmd.pp_indexed cmd_report.cmd in let data = { id; display; unifys; errors; submap; branch_path; parent } in - let cmd = + let cmd, to_exec = match kind with - | Normal -> Cmd { data; next = Nothing } + | Normal -> (Cmd { data; next = Nothing }, [ (id, None) ]) | Branch cases -> let nexts = Hashtbl.create (List.length cases) in - cases - |> List.iter (fun (case, _) -> Hashtbl.add nexts case ((), Nothing)); - BranchCmd { data; nexts } - | Final -> FinalCmd { data } + let to_exec = + cases + |> List.map (fun (case, _) -> + Hashtbl.add nexts case ((), Nothing); + (id, Some case)) + in + (BranchCmd { data; nexts }, to_exec) + | Final -> (FinalCmd { data }, []) in Hashtbl.replace id_map id cmd; - cmd + (cmd, to_exec) let get_id_opt = function | Nothing -> None @@ -110,16 +122,28 @@ module Make [ ("id", L.Report_id.to_yojson id); ("state", dump state) ]) ("at_id: " ^ s) - let init_exn _ _ exec_data = + 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 - let root_proc = get_proc_name exec_data in - ({ map; root_proc; id_map }, Stop) - - let init _ _ exec_data = Some (init_exn "" None exec_data) + let map, _ = new_cmd id_map exec_data ~parent:None () in + ({ map; root_proc = proc_name; all_procs; id_map; to_exec = [] }, Stop) + + 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 annot = exec_data.cmd_report.annot in + if Annot.is_hidden annot then ( + DL.log (fun m -> m "Gil_lifter: skipping hidden cmd"); + true) + else + let proc_name = get_proc_name exec_data in + if not (List.mem proc_name state.all_procs) then ( + DL.log (fun m -> m "Gil_lifter: skipping cmd from internal proc"); + true) + else false let handle_cmd prev_id branch_case exec_data state = - let { root_proc; id_map; _ } = state in + let { id_map; _ } = state in let new_cmd = new_cmd id_map exec_data in let failwith s = DL.failwith @@ -138,28 +162,36 @@ module Make | None -> failwith (Fmt.str "couldn't find prev_id %a!" L.Report_id.pp prev_id) in - (match map with - | Cmd cmd when cmd.next = Nothing -> - let parent = Some (map, None) in - cmd.next <- new_cmd ~parent () - | Cmd _ -> failwith "cmd.next not Nothing!" - | BranchCmd { nexts; _ } -> ( - match branch_case with - | None -> failwith "HORROR - need branch case to insert to branch cmd!" - | Some case -> ( - match Hashtbl.find_opt nexts case with - | Some ((), Nothing) -> - let parent = Some (map, Some case) in - Hashtbl.replace nexts case ((), new_cmd ~parent ()) - | _ -> failwith "colliding cases in branch cmd")) - | _ -> failwith "can't insert to Nothing or FinalCmd"); - let { id; cmd_report; _ } = exec_data in - let current_proc = get_proc_name exec_data in - if root_proc <> current_proc || Annot.is_hidden cmd_report.annot then - ExecNext (Some id, None) - else Stop - - let package_case _ = Packaged.package_gil_case + let to_exec = + match map with + | Cmd cmd when cmd.next = Nothing -> + let parent = Some (map, None) in + let new_cmd, to_exec = new_cmd ~parent () in + cmd.next <- new_cmd; + to_exec + | Cmd _ -> failwith "cmd.next not Nothing!" + | BranchCmd { nexts; _ } -> ( + match branch_case with + | None -> + failwith "HORROR - need branch case to insert to branch cmd!" + | Some case -> ( + match Hashtbl.find_opt nexts case with + | Some ((), Nothing) -> + let parent = Some (map, Some case) in + let new_cmd, to_exec = new_cmd ~parent () in + Hashtbl.replace nexts case ((), new_cmd); + to_exec + | 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 + match (should_skip_cmd exec_data state, to_exec @ state.to_exec) with + | true, (id, case) :: to_exec -> + state.to_exec <- to_exec; + ExecNext (Some id, case) + | _ -> Stop + + let package_case _ case _ = Packaged.package_gil_case case let package_data package { id; display; unifys; errors; submap; _ } = let submap = @@ -317,4 +349,11 @@ module Make let () = Hashtbl.replace variables store_id store_vars in let () = Hashtbl.replace variables memory_id memory_vars in scopes + + let pop_to_exec state = + match state.to_exec with + | [] -> None + | (id, case) :: to_exec -> + state.to_exec <- to_exec; + Some (id, case) end diff --git a/GillianCore/debugging/lifter/gil_lifter.mli b/GillianCore/debugging/lifter/gil_lifter.mli index 9cde55f74..816117b04 100644 --- a/GillianCore/debugging/lifter/gil_lifter.mli +++ b/GillianCore/debugging/lifter/gil_lifter.mli @@ -1,10 +1,16 @@ (** A basic "GIL-to-GIL" lifter implementation. *) +module type S = sig + include Lifter.S + + val pop_to_exec : t -> (Logging.Report_id.t * BranchCase.t option) option +end + module Make (PC : ParserAndCompiler.S) (V : Verifier.S with type annot = PC.Annot.t) (SMemory : SMemory.S) : - Lifter.S + S with type memory = SMemory.t and type tl_ast = PC.tl_ast and type memory_error = SMemory.err_t diff --git a/GillianCore/debugging/lifter/lifter_intf.ml b/GillianCore/debugging/lifter/lifter_intf.ml index 3b9fb135d..7d3e4879c 100644 --- a/GillianCore/debugging/lifter/lifter_intf.ml +++ b/GillianCore/debugging/lifter/lifter_intf.ml @@ -42,15 +42,19 @@ module type S = sig Returns [None] if lifting is unsupported (i.e. if [tl_ast] is [None]). *) val init : - string -> + proc_name:string -> + all_procs:string list -> tl_ast option -> + (annot, int) Prog.t -> cmd_report executed_cmd_data -> (t * handle_cmd_result) option (** Exception-raising version of {!init}. *) val init_exn : - string -> + proc_name:string -> + all_procs:string list -> tl_ast option -> + (annot, int) Prog.t -> cmd_report executed_cmd_data -> t * handle_cmd_result diff --git a/GillianCore/debugging/utils/exec_map.ml b/GillianCore/debugging/utils/exec_map.ml index 4f5146ce4..09948528e 100644 --- a/GillianCore/debugging/utils/exec_map.ml +++ b/GillianCore/debugging/utils/exec_map.ml @@ -190,10 +190,14 @@ module Packaged = struct Cmd { data = package_data aux data; next = aux next } | BranchCmd { data; nexts } -> let data = package_data aux data in + let all_cases = + nexts |> Hashtbl.to_seq |> List.of_seq + |> List.map (fun (c, (bd, _)) -> (c, bd)) + in let nexts = nexts |> Hashtbl.map (fun case (bdata, next) -> - let case = package_case bdata case in + let case = package_case bdata case all_cases in let next = aux next in (case, ((), next))) in diff --git a/GillianCore/utils/list_utils.ml b/GillianCore/utils/list_utils.ml index 5b02f5915..f2f129002 100644 --- a/GillianCore/utils/list_utils.ml +++ b/GillianCore/utils/list_utils.ml @@ -190,3 +190,8 @@ let at_least_two f l = else aux ~found_one r in aux ~found_one:false l + +let rec last = function + | [] -> None + | [ x ] -> Some x + | _ :: xs -> last xs diff --git a/wisl/lib/ParserAndCompiler/WAnnot.ml b/wisl/lib/ParserAndCompiler/WAnnot.ml index c2933c24d..ad8f80358 100644 --- a/wisl/lib/ParserAndCompiler/WAnnot.ml +++ b/wisl/lib/ParserAndCompiler/WAnnot.ml @@ -1,7 +1,8 @@ type nest_kind = | NoNest (** This command doesn't contain a nest *) - | Proc of string - (** This command "nests" the execution of another (named) procedure *) + | LoopBody of string + (** This command nests its loop body an (abstracted) function call *) + | FunCall of string (** This command nests the body of a function call *) [@@deriving yojson] type stmt_end_kind = NotEnd | EndNormal | EndWithBranch of WBranchCase.t @@ -24,6 +25,7 @@ type t = { nest_kind : nest_kind; [@default NoNest] is_hidden : bool; [@default false] (** Should this command be hidden when debugging? *) + is_return : bool; [@default false] } [@@deriving yojson, make] diff --git a/wisl/lib/ParserAndCompiler/wisl2Gil.ml b/wisl/lib/ParserAndCompiler/wisl2Gil.ml index e3ed22b78..2002550a1 100644 --- a/wisl/lib/ParserAndCompiler/wisl2Gil.ml +++ b/wisl/lib/ParserAndCompiler/wisl2Gil.ml @@ -602,7 +602,7 @@ let compile_inv_and_while ~fname ~while_stmt ~invariant = map_reassign_vars ((annot_while, None, cmd) :: acc) rest | [] -> List.rev acc in - let annot_call_while = { annot_while with nest_kind = Proc loop_fname } in + let annot_call_while = { annot_while with nest_kind = LoopBody loop_fname } in let lab_cmds = (annot_call_while, None, call_cmd) :: map_reassign_vars [] reassign_vars in @@ -824,7 +824,8 @@ let rec compile_stmt_list ?(fname = "main") ?(is_loop_prefix = false) stmtl = in let cmd = Cmd.Call (x, expr_fn, params, None, bindings) in let annot = - WAnnot.make ~origin_id:sid ~origin_loc:(CodeLoc.to_location sloc) () + WAnnot.make ~origin_id:sid ~origin_loc:(CodeLoc.to_location sloc) + ~nest_kind:(FunCall fn) () in let comp_rest, new_functions = compile_list rest in (List.concat cmdles @ [ (annot, None, cmd) ] @ comp_rest, new_functions) @@ -969,7 +970,7 @@ let rec compile_function let mk = WAnnot.make ~origin_loc:(CodeLoc.to_location (WExpr.get_loc return_expr)) - ~origin_id:(WExpr.get_id return_expr) + ~origin_id:(WExpr.get_id return_expr) ~is_return:true in (mk ~stmt_kind:(Multi NotEnd) (), mk ~stmt_kind:(Multi EndNormal) ()) in diff --git a/wisl/lib/debugging/wislLifter.ml b/wisl/lib/debugging/wislLifter.ml index bbbac23b1..15199e659 100644 --- a/wisl/lib/debugging/wislLifter.ml +++ b/wisl/lib/debugging/wislLifter.ml @@ -14,6 +14,14 @@ open Debugger.Lifter type rid = L.Report_id.t [@@deriving yojson, show] +let rec int_to_letters = function + | 0 -> "" + | i -> + let i = i - 1 in + let remainder = i mod 26 in + let char = Char.chr (65 + remainder) |> Char.escaped in + char ^ int_to_letters (i / 26) + module Make (Gil : Gillian.Debugger.Lifter.Gil_fallback_lifter.Gil_lifter_with_state) (Verification : Engine.Verifier.S with type annot = Annot.t) = @@ -32,6 +40,7 @@ struct type branch_case = WBranchCase.t [@@deriving yojson] type branch_data = rid * BranchCase.t option [@@deriving yojson] type exec_data = cmd_report executed_cmd_data [@@deriving yojson] + type stack_direction = In | Out of rid let annot_to_wisl_stmt annot wisl_ast = let origin_id = annot.origin_id in @@ -71,10 +80,12 @@ struct display : string; unifys : unification list; errors : string list; - submap : map submap; + mutable submap : map submap; gil_branch_path : BranchCase.path; branch_path : branch_case list; parent : parent; [@to_yojson fun _ -> `Null] + callers : rid list; + func_return_label : (string * int) option; } and parent = (map * (branch_data * branch_case) option) option @@ -142,7 +153,7 @@ struct | Final -> ()); match (d.submap, annot.nest_kind) with | _, NoNest -> () - | NoSubmap, Proc p -> d.submap <- Proc p + | NoSubmap, LoopBody p -> d.submap <- Proc p | _, _ -> DL.failwith (fun () -> @@ -154,15 +165,17 @@ struct "WislLifter.update_partial_data: multiple submaps in WISL \ statement!" + type finished_partial_data = { + ids : rid list; + display : string; + unifys : unification list; + errors : string list; + cmd_kind : (branch_case, branch_data) cmd_kind; + submap : map submap; + } + type partial_cmd_result = - | Finished of { - ids : rid list; - display : string; - unifys : unification list; - errors : string list; - cmd_kind : (branch_case, branch_data) cmd_kind; - submap : map submap; - } + | Finished of finished_partial_data | StepAgain of (rid option * BranchCase.t option) let make_finished_partial @@ -206,6 +219,7 @@ struct let is_final, result = match (exec_data.kind, end_kind) with | Final, _ -> (true, None) + | _, EndNormal when annot.is_return -> (true, None) | _, (EndNormal | EndWithBranch _) | Branch _, _ -> (false, None) | Normal, _ -> (false, Some (StepAgain (None, None))) in @@ -257,6 +271,9 @@ struct id_map : (rid, map) Hashtbl.t; [@to_yojson fun _ -> `Null] mutable before_partial : (rid * BranchCase.t option) option; mutable is_loop_func : bool; + prog : (annot, int) Prog.t; [@to_yojson fun _ -> `Null] + func_return_data : (rid, string * int ref) Hashtbl.t; + mutable func_return_count : int; } [@@deriving to_yojson] @@ -270,261 +287,451 @@ struct | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> data.gil_branch_path - let id_of_map_opt ?(last = false) = function + let id_of_map ?(last = false) = function | Nothing -> None | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> if last then Some (List.hd (List.rev data.ids)) else Some (List.hd data.ids) - let id_of_map ?(last = false) map = - match id_of_map_opt ~last map with + let id_of_map_exn ?(last = false) map = + match id_of_map ~last map with | None -> failwith "id_of_map: Nothing" | Some id -> id - let new_cmd - id_map - kind - ids - display - unifys - errors - gil_branch_path - ?(submap = NoSubmap) - ~(parent : parent) - () : map = - let branch_path = - match parent with - | None -> [] - | Some (parent_map, case) -> ( - let parent_path = path_of_map parent_map in - match case with - | None -> parent_path - | Some (_, case) -> case :: parent_path) - in - let data = - { - ids; - display; - unifys; - errors; - submap; - gil_branch_path; - branch_path; - parent; - } - in - let cmd = + let cmd_data_of_map = function + | Nothing -> None + | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> Some data + + let cmd_data_of_map_exn map = + match cmd_data_of_map map with + | None -> failwith "cmd_data_of_map: Nothing" + | Some callers -> callers + + let dump = to_yojson + + module Init_or_handle = struct + let new_function_return_label caller_id state = + state.func_return_count <- state.func_return_count + 1; + let label = int_to_letters state.func_return_count in + let count = ref 0 in + Hashtbl.add state.func_return_data caller_id (label, count); + (label, count) + + let update_caller_branches ~caller_id ~cont_id func_return_label state = + match Hashtbl.find_opt state.id_map caller_id with + | None -> + Fmt.failwith "update_caller_branches: caller %a not found" pp_rid + caller_id + | Some (BranchCmd { nexts; _ }) -> + Hashtbl.remove nexts FuncExitPlaceholder; + let case = FuncExit func_return_label in + let bdata = (cont_id, None) in + Hashtbl.add nexts case (bdata, Nothing) + | Some _ -> + Fmt.failwith "update_caller_branches: caller %a does not branch" + pp_rid caller_id + + let new_cmd + state + kind + ids + display + unifys + errors + gil_branch_path + ?(submap = NoSubmap) + ~parent + ~callers + () : map = + let branch_path = + match parent with + | None -> [] + | Some (parent_map, case) -> ( + let parent_path = path_of_map parent_map in + match case with + | None -> parent_path + | Some (_, case) -> case :: parent_path) + in + let func_return_label = + match (kind, callers) with + | Final, caller_id :: _ -> + let label, count = + match Hashtbl.find_opt state.func_return_data caller_id with + | Some (label, count) -> (label, count) + | None -> new_function_return_label caller_id state + in + incr count; + let label = (label, !count) in + let cont_id = ids |> List.rev |> List.hd in + update_caller_branches ~caller_id ~cont_id label state; + Some label + | _ -> None + in + let data = + { + ids; + display; + unifys; + errors; + submap; + gil_branch_path; + branch_path; + parent; + callers; + func_return_label; + } + in + let cmd = + match kind with + | Normal -> Cmd { data; next = Nothing } + | Branch cases -> ( + match cases with + | [ (Gil _, (_, None)) ] -> Cmd { data; next = Nothing } + | _ -> + let nexts = Hashtbl.create (List.length cases) in + cases + |> List.iter (fun (case, bdata) -> + Hashtbl.add nexts case (bdata, Nothing)); + BranchCmd { data; nexts }) + | Final -> FinalCmd { data } + in + ids |> List.iter (fun id -> Hashtbl.replace state.id_map id cmd); + cmd + + let convert_kind id kind = + let json cases = + let cmd_kind_to_yojson = + cmd_kind_to_yojson BranchCase.to_yojson (fun () -> `Null) + in + let cases_to_yojson cases = + cases |> List.map fst |> list_to_yojson BranchCase.to_yojson + in + [ + ("id", L.Report_id.to_yojson id); + ("kind", cmd_kind_to_yojson kind); + ("cases", cases_to_yojson cases); + ] + in + let failwith cases msg = DL.failwith (fun () -> json cases) msg in match kind with - | Normal -> Cmd { data; next = Nothing } + | Normal -> Normal + | Final -> Final | Branch cases -> ( match cases with - | [ (Gil _, (_, None)) ] -> Cmd { data; next = Nothing } + | (BranchCase.GuardedGoto _, ()) :: _ -> + let cases = + cases + |> List.map (fun (case, _) -> + match case with + | BranchCase.GuardedGoto b -> (IfElse b, (id, Some case)) + | _ -> + failwith cases + "convert_kind: inconsistent branch cases!") + in + Branch cases + | (BranchCase.LCmd _, ()) :: _ -> + let cases = + cases + |> List.map (fun (case, _) -> + match case with + | BranchCase.LCmd lcmd -> (LCmd lcmd, (id, Some case)) + | _ -> + failwith cases + "convert_kind: inconsistent branch cases!") + in + Branch cases | _ -> - let nexts = Hashtbl.create (List.length cases) in - cases - |> List.iter (fun (case, bdata) -> - Hashtbl.add nexts case (bdata, Nothing)); - BranchCmd { data; nexts }) - | Final -> FinalCmd { data } - in - ids |> List.iter (fun id -> Hashtbl.replace id_map id cmd); - cmd + DL.log (fun m -> + m ~json:(json cases) + "convert_kind: WARNING - unknown branch case!"); + let cases = + cases |> List.mapi (fun i (case, _) -> (Gil i, (id, Some case))) + in + Branch cases) - let dump = to_yojson + (** If the given ID isn't in the map, attempt to step backwards through the + GIL map until an ID (and map node) that *is* in the lifted map is found. *) + let rec get_prev_in_map id state = + match Hashtbl.find_opt state.id_map id with + | None -> ( + DL.log (fun m -> + m "couldn't find id %a; attempting with previous step from GIL." + pp_rid id); + match state.gil_state |> Gil_lifter.previous_step id with + | None -> None + | Some (prev_id, _) -> get_prev_in_map prev_id state) + | Some map -> Some (id, map) - let convert_kind id = function - | Normal -> Normal - | Final -> Final - | Branch cases -> ( - match cases with - | (BranchCase.GuardedGoto _, ()) :: _ -> - let cases = - cases - |> List.map (fun (case, _) -> - match case with - | BranchCase.GuardedGoto b -> (IfElse b, (id, Some case)) - | _ -> failwith "convert_kind: inconsistent branch cases!") - in - Branch cases - | (BranchCase.LCmd _, ()) :: _ -> - let cases = - cases - |> List.map (fun (case, _) -> - match case with - | BranchCase.LCmd lcmd -> (LCmd lcmd, (id, Some case)) - | _ -> failwith "convert_kind: inconsistent branch cases!") - in - Branch cases - | _ -> failwith "convert_kind: unsupported branch case!") - - let rec insert_new_cmd - (new_cmd : parent:parent -> unit -> map) - (new_id : rid) - (id : rid) - (gil_case : BranchCase.t option) - state = - let failwith s = failwith ("WislLifter.insert_new_cmd: " ^ s) in - let { id_map; gil_state; _ } = state in - match Hashtbl.find_opt id_map id with - | None -> ( - DL.log (fun m -> - m "couldn't find id %a; attempting with previous step from GIL." - pp_rid id); - match gil_state |> Gil_lifter.previous_step id with - | None -> failwith "couldn't step back any farther!" - | Some (prev_id, _) -> - insert_new_cmd new_cmd new_id prev_id gil_case state) - | Some map -> ( - match map with - | Cmd c -> - let parent = Some (map, None) in - c.next <- new_cmd ~parent () - | BranchCmd { nexts; _ } -> - let case, next, bdata = - match gil_case with - | None -> - let rec aux new_id = - let result = - nexts - |> Hashtbl.find_map (fun case (bdata, next) -> - match bdata with - | case_id, None when case_id = new_id -> - Some (case, next, bdata) - | _ -> None) - in - match result with - | Some r -> r - | None -> ( - let prev = - gil_state |> Gil_lifter.previous_step new_id - in - match prev with - | Some (new_id, _) -> - DL.log (fun m -> - m - "Inserting without gil case; attempting to \ - look back for link"); - aux new_id - | _ -> - failwith - "HORROR - tried to insert without branch case!") - in - aux new_id - | Some gil_case -> - Hashtbl.find_map - (fun case (bdata, next) -> - let gil_case' = bdata |> snd |> Option.get in - if gil_case <> gil_case' then None - else Some (case, next, bdata)) + let insert_new_cmd + (new_cmd : parent:parent -> unit -> map) + (new_id : rid) + (id : rid) + (gil_case : BranchCase.t option) + (stack_direction : stack_direction option) + state = + let failwith s = failwith ("WislLifter.insert_new_cmd: " ^ s) in + let map = + match stack_direction with + | Some (Out id) -> Hashtbl.find state.id_map id + | _ -> ( + match get_prev_in_map id state with + | None -> + failwith + (Fmt.str "Couldn't get prev command of '%a'!" pp_rid id) + | Some (_, map) -> map) + in + match (stack_direction, map) with + (* First command in a (nested) function call *) + | Some In, (Cmd { data; _ } | BranchCmd { data; _ }) -> + assert (data.submap = NoSubmap); + data.submap <- Submap (new_cmd ~parent:None ()) + | _, Cmd c -> + let parent = Some (map, None) in + c.next <- new_cmd ~parent () + | _, BranchCmd { nexts; _ } -> + (* If applicable, find the (empty) branch that will be replaced*) + let case, next, bdata = + match gil_case with + | None -> + let rec aux new_id = + let result = nexts - |> Option.get - in - if next <> Nothing then - failwith "HORROR - tried to insert to non-Nothing!"; - let parent = Some (map, Some (bdata, case)) in - Hashtbl.replace nexts case (bdata, new_cmd ~parent ()) - | _ -> failwith "HORROR - tried to insert to FinalCmd or Nothing!") - - let prepare_basic_cmd ?display ?(final = false) tl_ast id_map exec_data = - let { cmd_report; _ } = exec_data in - let annot = CmdReport.(cmd_report.annot) in - let { origin_id; nest_kind; _ } = annot in - let display = - match display with - | Some d -> d - | None -> - get_origin_node_str tl_ast origin_id - |> Option.value ~default:"Unknown command!" - in - let { id; unifys; errors; branch_path = gil_branch_path; kind; _ } = - exec_data - in - let submap = - match nest_kind with - | NoNest -> NoSubmap - | Proc p -> Proc p - in - let kind = if final then Final else convert_kind id kind in - new_cmd id_map kind [ id ] display unifys errors gil_branch_path ~submap - - let handle_loop_prefix exec_data = - let annot = CmdReport.(exec_data.cmd_report.annot) in - match annot.stmt_kind with - | LoopPrefix -> - Some - (match exec_data.cmd_report.cmd with - | Cmd.GuardedGoto _ -> - ExecNext (None, Some (BranchCase.GuardedGoto true)) - | _ -> ExecNext (None, None)) - | _ -> None + |> Hashtbl.find_map (fun case (bdata, next) -> + match bdata with + | case_id, _ when case_id = new_id -> + Some (case, next, bdata) + | _ -> None) + in + match result with + | Some r -> r + | None -> ( + let prev = + state.gil_state |> Gil_lifter.previous_step new_id + in + match prev with + | Some (new_id, _) -> + DL.log (fun m -> + m + "Inserting without gil case; attempting to \ + look back for link (prev: %a)" + L.Report_id.pp new_id); + aux new_id + | _ -> + failwith + "HORROR - tried to insert without branch case!") + in + aux new_id + | Some gil_case -> + Hashtbl.find_map + (fun case (bdata, next) -> + let gil_case' = bdata |> snd |> Option.get in + if gil_case <> gil_case' then None + else Some (case, next, bdata)) + nexts + |> Option.get + in + if next <> Nothing then + failwith "HORROR - tried to insert to non-Nothing!"; + let parent = Some (map, Some (bdata, case)) in + Hashtbl.replace nexts case (bdata, new_cmd ~parent ()) + | _ -> failwith "HORROR - tried to insert to FinalCmd or Nothing!" - let init_or_handle prev_id branch_case exec_data state = - let Debugger.Lifter.{ id; _ } = exec_data in - DL.log (fun m -> - m - ~json: - [ - ("state", dump state); ("exec_data", exec_data_to_yojson exec_data); - ] - "HANDLING %a (prev %a)" L.Report_id.pp id (pp_option L.Report_id.pp) - prev_id); - let { tl_ast; partial_cmds; id_map; proc_name; is_loop_func; _ } = state in - match handle_loop_prefix exec_data with - | Some result -> - state.is_loop_func <- true; - result - | None -> ( - match PartialCmds.handle exec_data tl_ast partial_cmds with - | Some (StepAgain result) -> - if Option.is_none state.before_partial then - prev_id - |> Option.iter (fun prev_id -> - state.before_partial <- Some (prev_id, branch_case)); - ExecNext result + let is_fcall_using_spec fn (prog : (annot, int) Prog.t) = + let open Gillian.Utils in + (match !Config.current_exec_mode with + | Exec_mode.Verification | Exec_mode.BiAbduction -> true + | Exec_mode.Concrete | Exec_mode.Symbolic -> false) + && + match Hashtbl.find_opt prog.procs fn with + | Some proc -> Option.is_some proc.proc_spec + | None -> false + + let prepare_basic_cmd ?display ?(final = false) tl_ast id_map prog exec_data + = + let { cmd_report; _ } = exec_data in + let annot = CmdReport.(cmd_report.annot) in + let { origin_id; nest_kind; _ } = annot in + let display = + match display with + | Some d -> d | None -> - let display, final = - if is_loop_func && get_fun_call_name exec_data = Some proc_name - then (Some "", true) - else (None, false) - in - let new_cmd = - prepare_basic_cmd ?display ~final tl_ast id_map exec_data - in - (match (state.map, prev_id) with - | Nothing, _ -> state.map <- new_cmd ~parent:None () - | _, Some prev_id -> - insert_new_cmd new_cmd id prev_id branch_case state - | _, _ -> - failwith - "HORROR - tried to insert to non-Nothing map without \ - previous id!"); - Stop - | Some (Finished { ids; display; unifys; errors; cmd_kind; submap }) -> - let gil_branch_path = - Gil_lifter.path_of_id (List.hd ids) state.gil_state - in - let new_cmd = - new_cmd id_map cmd_kind ids display unifys errors gil_branch_path - ~submap - in - let prev_id, branch_case = - match state.before_partial with - | Some (prev_id, branch_case) -> - state.before_partial <- None; - (Some prev_id, branch_case) - | None -> (prev_id, branch_case) - in - (match (state.map, prev_id) with - | Nothing, _ -> state.map <- new_cmd ~parent:None () - | _, Some prev_id -> - insert_new_cmd new_cmd id prev_id branch_case state - | _, _ -> - failwith - "HORROR - tried to insert to non-Nothing map without \ - previous id!"); - Stop) + get_origin_node_str tl_ast origin_id + |> Option.value ~default:"Unknown command!" + in + let { id; unifys; errors; branch_path = gil_branch_path; kind; _ } = + exec_data + in + let submap = + match nest_kind with + | LoopBody p -> Proc p + | _ -> NoSubmap + in + let kind = + if final then Final + else + match nest_kind with + | FunCall fn when not (is_fcall_using_spec fn prog) -> + Branch [ (FuncExitPlaceholder, (id, None)) ] + | _ -> convert_kind id kind + in + new_cmd id_map kind [ id ] display unifys errors gil_branch_path ~submap - let init proc_name tl_ast exec_data = + let handle_loop_prefix exec_data = + let annot = CmdReport.(exec_data.cmd_report.annot) in + match annot.stmt_kind with + | LoopPrefix -> + Some + (match exec_data.cmd_report.cmd with + | Cmd.GuardedGoto _ -> + ExecNext (None, Some (BranchCase.GuardedGoto true)) + | _ -> ExecNext (None, None)) + | _ -> None + + let compute_callers prev_id (exec_data : exec_data) state : + rid list * stack_direction option = + let prev = + let* prev_id = prev_id in + get_prev_in_map prev_id state + in + match prev with + | None -> ([], None) + | Some (prev_id, prev_node) -> ( + let prev = cmd_data_of_map_exn prev_node in + let depth_change = + let cs = exec_data.cmd_report.callstack in + assert ((List.hd cs).pid = exec_data.cmd_report.proc_name); + let prev_depth = List.length prev.callers in + List.length cs - prev_depth - 1 + in + match depth_change with + | 0 -> (prev.callers, None) + | 1 -> (prev_id :: prev.callers, Some In) + | -1 -> ( + match prev.callers with + | [] -> failwith "HORROR - prev.callers is empty!" + | hd :: tl -> (tl, Some (Out hd))) + | _ -> + Fmt.failwith + "WislLifter.compute_callers: HORROR - cmd %a has too great a \ + depth change!" + pp_rid prev_id) + + let handle_no_partial + callers + stack_direction + prev_id + branch_case + exec_data + state = + let Debugger.Lifter.{ id; _ } = exec_data in + let { tl_ast; proc_name; is_loop_func; _ } = state in + let display, final = + if is_loop_func && get_fun_call_name exec_data = Some proc_name then + (Some "", true) + else (None, false) + in + let new_cmd = + prepare_basic_cmd ?display ~final ~callers tl_ast state state.prog + exec_data + in + (match (state.map, prev_id) with + | Nothing, _ -> state.map <- new_cmd ~parent:None () + | _, Some prev_id -> + insert_new_cmd new_cmd id prev_id branch_case stack_direction state + | _, _ -> + failwith + "HORROR - tried to insert to non-Nothing map without previous id!"); + Stop + + let handle_finished_partial + finished_data + callers + stack_direction + prev_id + branch_case + exec_data + state = + let Debugger.Lifter.{ id; _ } = exec_data in + let PartialCmds.{ ids; display; unifys; errors; cmd_kind; submap } = + finished_data + in + let gil_branch_path = + Gil_lifter.path_of_id (List.hd ids) state.gil_state + in + let new_cmd = + new_cmd state cmd_kind ids display unifys errors gil_branch_path ~submap + in + let prev_id, branch_case = + match state.before_partial with + | Some (prev_id, branch_case) -> + state.before_partial <- None; + (Some prev_id, branch_case) + | None -> (prev_id, branch_case) + in + (match (state.map, prev_id) with + (* First insertion to empty map *) + | Nothing, _ -> state.map <- new_cmd ~callers:[] ~parent:None () + (* Normal insertion *) + | _, Some prev_id -> + insert_new_cmd (new_cmd ~callers) id prev_id branch_case + stack_direction state + | _, _ -> + failwith + "HORROR - tried to insert to non-Nothing map without previous id!"); + Stop + + let do_handle prev_id branch_case exec_data state = + let { tl_ast; partial_cmds; _ } = state in + match handle_loop_prefix exec_data with + | Some result -> + state.is_loop_func <- true; + result + | None -> ( + let callers, stack_direction = + compute_callers prev_id exec_data state + in + match PartialCmds.handle exec_data tl_ast partial_cmds with + | Some (StepAgain result) -> + if Option.is_none state.before_partial then + prev_id + |> Option.iter (fun prev_id -> + state.before_partial <- Some (prev_id, branch_case)); + ExecNext result + | None -> + handle_no_partial callers stack_direction prev_id branch_case + exec_data state + | Some (Finished finished_data) -> + handle_finished_partial finished_data callers stack_direction + prev_id branch_case exec_data state) + + let check_gil_to_exec result state = + match result with + | Stop -> ( + match Gil_lifter.pop_to_exec state.gil_state with + | Some (id, case) -> ExecNext (Some id, case) + | None -> Stop) + | _ -> result + + let f prev_id branch_case exec_data state = + let Debugger.Lifter.{ id; _ } = exec_data in + DL.log (fun m -> + m + ~json: + [ + ("state", dump state); + ("exec_data", exec_data_to_yojson exec_data); + ("prev_id", (opt_to_yojson L.Report_id.to_yojson) prev_id); + ("branch_case", (opt_to_yojson BranchCase.to_yojson) branch_case); + ] + "HANDLING %a (prev %a)" L.Report_id.pp id (pp_option L.Report_id.pp) + prev_id); + let result = do_handle prev_id branch_case exec_data state in + check_gil_to_exec result state + 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 @@ -540,13 +747,16 @@ struct 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 None None exec_data state in (state, result) - let init_exn proc_name tl_ast exec_data = - match init proc_name tl_ast exec_data with + 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 @@ -555,26 +765,36 @@ struct let get_gil_map _ = failwith "get_gil_map: not implemented!" - let package_case (bd : branch_data) (case : branch_case) : + let package_case (bd : branch_data) (case : branch_case) all_cases : Packaged.branch_case = let json = branch_case_to_yojson case in let kind, display = match case with | IfElse b -> ("IfElse", ("If/Else", Fmt.str "%B" b)) | LCmd x -> ("LCmd", ("Logical command", Fmt.str "%d" x)) - | Gil _ -> ( + | Gil x -> ( let id, gil_case = bd in match gil_case with | Some gil_case -> - let kind_display, display = + let kind_display, _ = Packaged.(package_gil_case gil_case).display in let kind = "GIL" in let kind_display = Fmt.str "(GIL) %s" kind_display in - let display = Fmt.str "(%a) %s" pp_rid id display in + (* let display = Fmt.str "(%a) %s" pp_rid id display in *) + let display = Int.to_string x in (kind, (kind_display, display)) | None -> ("GIL", ("(GIL) Unknown", Fmt.str "(%a) Unknown" pp_rid id)) ) + | FuncExit (label, i) -> + ("FuncExit", ("Return case", Fmt.str "%s-%d" label i)) + | FuncExitPlaceholder -> + ("FuncExitPlaceholder", ("Return case", "")) + in + let display = + match (WBranchCase.is_hidden_when_single case, all_cases) with + | true, [ _ ] -> ("", "") + | _ -> display in { kind; display; json } @@ -643,9 +863,9 @@ struct | Nothing -> None | Cmd { data; _ } | BranchCmd { data; _ } | FinalCmd { data } -> let+ parent, case = data.parent in - let id = id_of_map parent in + let id = id_of_map_exn parent in let case = - case |> Option.map (fun (bdata, case) -> package_case bdata case) + case |> Option.map (fun (bdata, case) -> package_case bdata case []) in (id, case) @@ -654,7 +874,11 @@ struct let find_unfinished_path ?at_id state = let { map; id_map; _ } = state in - let rec aux = function + let rec aux map = + match aux_submap map with + | None -> aux_map map + | result -> result + and aux_map = function | Nothing -> DL.failwith (fun () -> @@ -677,6 +901,12 @@ struct | 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 diff --git a/wisl/lib/utils/wBranchCase.ml b/wisl/lib/utils/wBranchCase.ml index 8ee335a18..fe9224096 100644 --- a/wisl/lib/utils/wBranchCase.ml +++ b/wisl/lib/utils/wBranchCase.ml @@ -1 +1,11 @@ -type t = IfElse of bool | LCmd of int | Gil of int [@@deriving yojson] +type t = + | IfElse of bool + | LCmd of int + | Gil of int + | FuncExitPlaceholder + | FuncExit of (string * int) +[@@deriving yojson] + +let is_hidden_when_single = function + | Gil _ | FuncExit _ -> true + | _ -> false