diff options
| -rw-r--r-- | clib/backtrace.ml | 119 | ||||
| -rw-r--r-- | clib/backtrace.mli | 98 | ||||
| -rw-r--r-- | clib/exninfo.ml | 39 | ||||
| -rw-r--r-- | clib/exninfo.mli | 43 | ||||
| -rw-r--r-- | dev/doc/changes.md | 7 | ||||
| -rw-r--r-- | ide/coqide.ml | 2 | ||||
| -rw-r--r-- | lib/cErrors.ml | 8 | ||||
| -rw-r--r-- | lib/control.ml | 6 | ||||
| -rw-r--r-- | lib/flags.ml | 4 | ||||
| -rw-r--r-- | lib/pp.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqargs.ml | 2 | ||||
| -rw-r--r-- | toplevel/coqinit.ml | 2 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 2 | ||||
| -rw-r--r-- | vernac/topfmt.ml | 4 |
14 files changed, 96 insertions, 242 deletions
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 *) -(* <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 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 *) -(* <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) *) -(************************************************************************) - -(** * Low-level management of OCaml backtraces. - - Currently, OCaml manages its backtraces in a very imperative way. That is to - say, it only keeps track of the stack destroyed by the last raised exception. - So we have to be very careful when using this module not to do silly things. - - Basically, you need to manually handle the reraising of exceptions. In order - to do so, each time the backtrace is lost, you must [push] the stack fragment. - This essentially occurs whenever a [with] handler is crossed. - -*) - -(** {5 Backtrace information} *) - -type location = { - loc_filename : string; - loc_line : int; - loc_start : int; - loc_end : int; -} -(** OCaml debugging information for function calls. *) - -type frame = { frame_location : location option; frame_raised : bool; } -(** A frame contains two informations: its optional physical location, and - whether it raised the exception or let it pass through. *) - -type t -(** Type of backtraces. They're essentially stack of frames. *) - -val empty : t -(** Empty frame stack. *) - -val push : t -> 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. *) diff --git a/dev/doc/changes.md b/dev/doc/changes.md index 04b20c6889..3bc92e6aee 100644 --- a/dev/doc/changes.md +++ b/dev/doc/changes.md @@ -2,6 +2,13 @@ ### ML API +Exception handling: + +- Coq's custom `Backtrace` module has been removed in favor of OCaml's + native backtrace implementation. Please use the functions in + `Exninfo.capture` and `iraise` when re-raising inside an exception + handler. + Printers: - Functions such as Printer.pr_lconstr_goal_style_env have been diff --git a/ide/coqide.ml b/ide/coqide.ml index d7e155f6bb..e0347d3c5f 100644 --- a/ide/coqide.ml +++ b/ide/coqide.ml @@ -1366,7 +1366,7 @@ let read_coqide_args argv = |"-debug"::args -> Minilib.debug := true; Flags.debug := true; - Backtrace.record_backtrace true; + Exninfo.record_backtrace true; filter_coqtop coqtop project_files bindings_files ("-debug"::out) args |"-coqtop-flags" :: flags :: args-> Coq.ideslave_coqtop_flags := Some flags; diff --git a/lib/cErrors.ml b/lib/cErrors.ml index b9735d0579..9f496f5845 100644 --- a/lib/cErrors.ml +++ b/lib/cErrors.ml @@ -12,7 +12,7 @@ open Pp (** Aliases *) -let push = Backtrace.add_backtrace +let push = Exninfo.capture (* Errors *) @@ -51,12 +51,10 @@ let raw_anomaly e = match e with | _ -> str "Uncaught exception " ++ str (Printexc.to_string e) ++ str "." -let print_backtrace e = match Backtrace.get_backtrace e with +let print_backtrace e = match Exninfo.get_backtrace e with | None -> mt () | Some bt -> - let bt = Backtrace.repr bt in - let pr_frame f = str (Backtrace.print_frame f) in - let bt = prlist_with_sep fnl pr_frame bt in + let bt = str (Exninfo.backtrace_to_string bt) in fnl () ++ hov 0 bt let print_anomaly askreport e = diff --git a/lib/control.ml b/lib/control.ml index 7d54838df8..e67e88ee95 100644 --- a/lib/control.ml +++ b/lib/control.ml @@ -38,7 +38,7 @@ let unix_timeout n f x e = restore_timeout (); res with e -> - let e = Backtrace.add_backtrace e in + let e = Exninfo.capture e in restore_timeout (); Exninfo.iraise e @@ -76,7 +76,7 @@ let windows_timeout n f x e = else raise e | e -> let () = killed := true in - let e = Backtrace.add_backtrace e in + let e = Exninfo.capture e in Exninfo.iraise e type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b } @@ -102,7 +102,7 @@ let protect_sigalrm f x = | true, Sys.Signal_handle f -> f Sys.sigalrm; res | _, _ -> res with e -> - let e = Backtrace.add_backtrace e in + let e = Exninfo.capture e in Sys.set_signal Sys.sigalrm old_handler; Exninfo.iraise e with Invalid_argument _ -> (* This happens on Windows, as handling SIGALRM does not seem supported *) diff --git a/lib/flags.ml b/lib/flags.ml index b87ba46634..ad48024761 100644 --- a/lib/flags.ml +++ b/lib/flags.ml @@ -19,7 +19,7 @@ let with_modified_ref ?(restore=true) r nf f x = if restore || pre == !r then r := old_ref; res with reraise -> - let reraise = Backtrace.add_backtrace reraise in + let reraise = Exninfo.capture reraise in r := old_ref; Exninfo.iraise reraise @@ -37,7 +37,7 @@ let with_options ol f x = let r = f x in let () = List.iter2 (:=) ol vl in r with reraise -> - let reraise = Backtrace.add_backtrace reraise in + let reraise = Exninfo.capture reraise in let () = List.iter2 (:=) ol vl in Exninfo.iraise reraise @@ -203,7 +203,7 @@ let pp_with ft pp = in try pp_cmd pp with reraise -> - let reraise = Backtrace.add_backtrace reraise in + let reraise = Exninfo.capture reraise in let () = Format.pp_print_flush ft () in Exninfo.iraise reraise diff --git a/toplevel/coqargs.ml b/toplevel/coqargs.ml index 56a6312b61..52e2562ae8 100644 --- a/toplevel/coqargs.ml +++ b/toplevel/coqargs.ml @@ -513,7 +513,7 @@ let parse_args ~help ~init arglist : t * string list = }}} |"-test-mode" -> Vernacinterp.test_mode := true; oval |"-beautify" -> Flags.beautify := true; oval - |"-bt" -> Backtrace.record_backtrace true; oval + |"-bt" -> Exninfo.record_backtrace true; oval |"-color" -> set_color oval (next ()) |"-config"|"--config" -> set_query oval PrintConfig |"-debug" -> Coqinit.set_debug (); oval diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml index ae37e40101..ac348b9646 100644 --- a/toplevel/coqinit.ml +++ b/toplevel/coqinit.ml @@ -14,7 +14,7 @@ open Pp let ( / ) s1 s2 = Filename.concat s1 s2 let set_debug () = - let () = Backtrace.record_backtrace true in + let () = Exninfo.record_backtrace true in Flags.debug := true (* Loading of the resource file. diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index bca6b48499..adcce67b0d 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -69,10 +69,10 @@ let interp_vernac ~check ~interactive ~state ({CAst.loc;_} as com) = let new_proof = Vernacstate.Proof_global.give_me_the_proof_opt () [@ocaml.warning "-3"] in { state with doc = ndoc; sid = nsid; proof = new_proof; } with reraise -> + let (reraise, info) = CErrors.push reraise in (* XXX: In non-interactive mode edit_at seems to do very weird things, so we better avoid it while we investigate *) if interactive then ignore(Stm.edit_at ~doc:state.doc state.sid); - let (reraise, info) = CErrors.push reraise in let info = begin match Loc.get_loc info with | None -> Option.cata (Loc.add_loc info) info loc diff --git a/vernac/topfmt.ml b/vernac/topfmt.ml index 45f40b1258..de02f7ecfb 100644 --- a/vernac/topfmt.ml +++ b/vernac/topfmt.ml @@ -359,7 +359,7 @@ let in_phase ~phase f x = default_phase := op; res with exn -> - let iexn = Backtrace.add_backtrace exn in + let iexn = Exninfo.capture exn in default_phase := op; Util.iraise iexn @@ -415,7 +415,7 @@ let with_output_to_file fname func input = close_out channel; output with reraise -> - let reraise = Backtrace.add_backtrace reraise in + let reraise = Exninfo.capture reraise in std_ft := Util.pi1 old_fmt; err_ft := Util.pi2 old_fmt; deep_ft := Util.pi3 old_fmt; |