From c825bc9caf3abb9610310b79f9420688f06bdf54 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Wed, 8 Jan 2020 18:48:51 +0100 Subject: [ocaml] Remove Custom Backtrace module in favor of OCaml's As suggested by Pierre-Marie Pédrot, this is a more conservative version of #8771 . In this commit, we replace Coq's custom backtrace type with OCaml `Printexc.raw_backtrace`; this seems to already give some improvements in terms of backtraces [see below] and removes quite a bit of code. Main difference in terms of API is that backtraces become now first-class in `Exninfo`, and we seek to consolidate thus the exception-related APIs in that module. We also fix a bug in `vernac.ml` where the backtrace captured was the one of `edit_at`. Closes #6446 Example with backtrace from https://github.com/coq/coq/issues/11366 Old: ``` raise @ file "stdlib.ml", line 33, characters 17-33 frame @ file "pretyping/coercion.ml", line 406, characters 24-68 frame @ file "list.ml", line 117, characters 24-34 frame @ file "pretyping/coercion.ml", line 393, characters 4-1004 frame @ file "pretyping/coercion.ml", line 450, characters 12-40 raise @ unknown frame @ file "pretyping/coercion.ml", line 464, characters 6-46 raise @ unknown frame @ file "pretyping/pretyping.ml", line 839, characters 33-95 frame @ file "pretyping/pretyping.ml", line 875, characters 50-94 frame @ file "pretyping/pretyping.ml", line 1280, characters 2-81 frame @ file "pretyping/pretyping.ml", line 1342, characters 20-71 frame @ file "vernac/vernacentries.ml", line 1579, characters 17-48 frame @ file "vernac/vernacentries.ml", line 2215, characters 8-49 frame @ file "vernac/vernacinterp.ml", line 45, characters 4-13 ... ``` New: ``` Raised at file "stdlib.ml", line 33, characters 17-33 Called from file "pretyping/coercion.ml", line 406, characters 24-68 Called from file "list.ml", line 117, characters 24-34 Called from file "pretyping/coercion.ml", line 393, characters 4-1004 Called from file "pretyping/coercion.ml", line 450, characters 12-40 Called from file "pretyping/coercion.ml", line 464, characters 6-46 Called from file "pretyping/pretyping.ml", line 839, characters 33-95 Called from file "pretyping/pretyping.ml", line 875, characters 50-94 Called from file "pretyping/pretyping.ml" (inlined), line 1280, characters 2-81 Called from file "pretyping/pretyping.ml", line 1294, characters 21-94 Called from file "pretyping/pretyping.ml", line 1342, characters 20-71 Called from file "vernac/vernacentries.ml", line 1579, characters 17-48 Called from file "vernac/vernacentries.ml", line 2215, characters 8-49 Called from file "vernac/vernacinterp.ml", line 45, characters 4-13 ... ``` --- clib/backtrace.ml | 119 ----------------------------------------------------- clib/backtrace.mli | 98 ------------------------------------------- clib/exninfo.ml | 39 ++++++++++++++---- clib/exninfo.mli | 43 +++++++++++++++++++ 4 files changed, 74 insertions(+), 225 deletions(-) delete mode 100644 clib/backtrace.ml delete mode 100644 clib/backtrace.mli (limited to 'clib') diff --git a/clib/backtrace.ml b/clib/backtrace.ml deleted file mode 100644 index 81803a81a5..0000000000 --- a/clib/backtrace.ml +++ /dev/null @@ -1,119 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* 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 diff --git a/clib/backtrace.mli b/clib/backtrace.mli deleted file mode 100644 index 55c60e5483..0000000000 --- a/clib/backtrace.mli +++ /dev/null @@ -1,98 +0,0 @@ -(************************************************************************) -(* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) -(* t -(** Add the current backtrace information to a given backtrace. *) - -val repr : t -> frame list -(** Represent a backtrace as a list of frames. Leftmost element is the outermost - call. *) - -(** {5 Utilities} *) - -val print_frame : frame -> string -(** Represent a frame. *) - -(** {5 Exception handling} *) - -val record_backtrace : bool -> unit -(** Whether to activate the backtrace recording mechanism. Note that it will - only work whenever the program was compiled with the [debug] flag. *) - -val get_backtrace : Exninfo.info -> t option -(** Retrieve the optional backtrace coming with the exception. *) - -val add_backtrace : exn -> Exninfo.iexn -(** Add the current backtrace information to the given exception. - - The intended use case is of the form: {[ - - try foo - with - | Bar -> bar - | err -> let err = add_backtrace err in baz - - ]} - - WARNING: any intermediate code between the [with] and the handler may - modify the backtrace. Yes, that includes [when] clauses. Ideally, what you - should do is something like: {[ - - try foo - with err -> - let err = add_backtrace err in - match err with - | Bar -> bar - | err -> baz - - ]} - - I admit that's a bit heavy, but there is not much to do... - -*) - -val app_backtrace : src:Exninfo.info -> dst:Exninfo.info -> Exninfo.info -(** Append the backtrace from [src] to [dst]. The returned exception is [dst] - except for its backtrace information. This is targeted at container - exceptions, that is, exceptions that contain exceptions. This way, one can - transfer the backtrace from the container to the underlying exception, as if - the latter was the one originally raised. *) diff --git a/clib/exninfo.ml b/clib/exninfo.ml index 34f76a2edd..ee998c2f17 100644 --- a/clib/exninfo.ml +++ b/clib/exninfo.ml @@ -57,12 +57,29 @@ let rec find_and_remove_assoc (i : int) = function if rem == ans then (r, l) else (r, (j, v) :: ans) -let iraise e = +type backtrace = Printexc.raw_backtrace +let backtrace_to_string = Printexc.raw_backtrace_to_string + +let backtrace_info : backtrace t = make () + +let is_recording = ref false + +let record_backtrace b = + let () = Printexc.record_backtrace b in + is_recording := b + +let get_backtrace e = get e backtrace_info + +let iraise (e,i) = let () = Mutex.lock lock in let id = Thread.id (Thread.self ()) in - let () = current := (id, e) :: remove_assoc id !current in + let () = current := (id, (e,i)) :: remove_assoc id !current in let () = Mutex.unlock lock in - raise (fst e) + match get i backtrace_info with + | None -> + raise e + | Some bt -> + Printexc.raise_with_backtrace e bt let raise ?info e = match info with | None -> @@ -72,11 +89,7 @@ let raise ?info e = match info with let () = Mutex.unlock lock in raise e | Some i -> - let () = Mutex.lock lock in - let id = Thread.id (Thread.self ()) in - let () = current := (id, (e, i)) :: remove_assoc id !current in - let () = Mutex.unlock lock in - raise e + iraise (e,i) let find_and_remove () = let () = Mutex.lock lock in @@ -104,3 +117,13 @@ let info e = (* Mismatch: the raised exception is not the one stored, either because the previous raise was not instrumented, or because something went wrong. *) Store.empty + +let capture e = + if !is_recording then + (* This must be the first function call, otherwise the stack may be + destroyed *) + let bt = Printexc.get_raw_backtrace () in + let info = info e in + e, add info backtrace_info bt + else + e, info e diff --git a/clib/exninfo.mli b/clib/exninfo.mli index 30803e3e6a..36cc44cf82 100644 --- a/clib/exninfo.mli +++ b/clib/exninfo.mli @@ -34,6 +34,49 @@ val get : info -> 'a t -> 'a option val info : exn -> info (** Retrieve the information of the last exception raised. *) +type backtrace + +val get_backtrace : info -> backtrace option +(** [get_backtrace info] does get the backtrace associated to info *) + +val backtrace_to_string : backtrace -> string +(** [backtrace_to_string info] does get the backtrace associated to info *) + +val record_backtrace : bool -> unit + +val capture : exn -> iexn +(** Add the current backtrace information to the given exception. + + The intended use case is of the form: {[ + + try foo + with + | Bar -> bar + | exn -> + let exn = Exninfo.capture err in + baz + + ]} + + where [baz] should re-raise using [iraise] below. + + WARNING: any intermediate code between the [with] and the handler may + modify the backtrace. Yes, that includes [when] clauses. Ideally, what you + should do is something like: {[ + + try foo + with exn -> + let exn = Exninfo.capture exn in + match err with + | Bar -> bar + | err -> baz + + ]} + + I admit that's a bit heavy, but there is not much to do... + +*) + val iraise : iexn -> 'a (** Raise the given enriched exception. *) -- cgit v1.2.3