diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /clib/backtrace.ml | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'clib/backtrace.ml')
-rw-r--r-- | clib/backtrace.ml | 119 |
1 files changed, 119 insertions, 0 deletions
diff --git a/clib/backtrace.ml b/clib/backtrace.ml new file mode 100644 index 00000000..27ed6fbf --- /dev/null +++ b/clib/backtrace.ml @@ -0,0 +1,119 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) +[@@@ocaml.warning "-37"] + +type raw_frame = +| Known_location of bool (* is_raise *) + * string (* filename *) + * int (* line number *) + * int (* start char *) + * int (* end char *) +| Unknown_location of bool (*is_raise*) + +type location = { + loc_filename : string; + loc_line : int; + loc_start : int; + loc_end : int; +} + +type frame = { frame_location : location option; frame_raised : bool; } + +external get_exception_backtrace: unit -> raw_frame array option + = "caml_get_exception_backtrace" + +type t = raw_frame array list +(** List of partial raw stack frames, in reverse order *) + +let empty = [] + +let of_raw = function +| Unknown_location r -> + { frame_location = None; frame_raised = r; } +| Known_location (r, file, line, st, en) -> + let loc = { + loc_filename = file; + loc_line = line; + loc_start = st; + loc_end = en; + } in + { frame_location = Some loc; frame_raised = r; } + +let rec repr_aux accu = function +| [] -> accu +| fragment :: stack -> + let len = Array.length fragment in + let rec append accu i = + if i = len then accu + else append (of_raw fragment.(i) :: accu) (succ i) + in + repr_aux (append accu 0) stack + +let repr bt = repr_aux [] (List.rev bt) + +let push stack = match get_exception_backtrace () with +| None -> [] +| Some frames -> frames :: stack + +(** Utilities *) + +let print_frame frame = + let raise = if frame.frame_raised then "raise" else "frame" in + match frame.frame_location with + | None -> Printf.sprintf "%s @ unknown" raise + | Some loc -> + Printf.sprintf "%s @ file \"%s\", line %d, characters %d-%d" + raise loc.loc_filename loc.loc_line loc.loc_start loc.loc_end + +(** Exception manipulation *) + +let backtrace : t Exninfo.t = Exninfo.make () + +let is_recording = ref false + +let record_backtrace b = + let () = Printexc.record_backtrace b in + is_recording := b + +let get_backtrace e = + Exninfo.get e backtrace + +let add_backtrace e = + if !is_recording then + (** This must be the first function call, otherwise the stack may be + destroyed *) + let current = get_exception_backtrace () in + let info = Exninfo.info e in + begin match current with + | None -> (e, info) + | Some fragment -> + let bt = match get_backtrace info with + | None -> [] + | Some bt -> bt + in + let bt = fragment :: bt in + (e, Exninfo.add info backtrace bt) + end + else + let info = Exninfo.info e in + (e, info) + +let app_backtrace ~src ~dst = + if !is_recording then + match get_backtrace src with + | None -> dst + | Some bt -> + match get_backtrace dst with + | None -> + Exninfo.add dst backtrace bt + | Some nbt -> + let bt = bt @ nbt in + Exninfo.add dst backtrace bt + else dst |