diff options
| -rw-r--r-- | checker/check.mllib | 1 | ||||
| -rw-r--r-- | dev/printers.mllib | 1 | ||||
| -rw-r--r-- | grammar/grammar.mllib | 1 | ||||
| -rw-r--r-- | lib/backtrace.ml | 89 | ||||
| -rw-r--r-- | lib/backtrace.mli | 108 | ||||
| -rw-r--r-- | lib/clib.mllib | 1 |
6 files changed, 201 insertions, 0 deletions
diff --git a/checker/check.mllib b/checker/check.mllib index 1bc23734a..2d56e163b 100644 --- a/checker/check.mllib +++ b/checker/check.mllib @@ -1,4 +1,5 @@ Coq_config +Backtrace Int Pp_control Flags diff --git a/dev/printers.mllib b/dev/printers.mllib index 85e1d6fe6..7caf268b9 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -1,5 +1,6 @@ Coq_config +Backtrace Int Pp_control Loc diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib index 9a7bfed0f..4e1642a90 100644 --- a/grammar/grammar.mllib +++ b/grammar/grammar.mllib @@ -1,5 +1,6 @@ Coq_config +Backtrace Int Pp_control Flags diff --git a/lib/backtrace.ml b/lib/backtrace.ml new file mode 100644 index 000000000..84f208c9e --- /dev/null +++ b/lib/backtrace.ml @@ -0,0 +1,89 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +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 = frame list option + +let empty = Some [] + +let none = None + +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 push bt = match bt with +| None -> None +| Some stack -> + match get_exception_backtrace () with + | None -> bt + | Some frames -> + let len = Array.length frames in + let rec append accu i = + if i = len then accu + else append (of_raw frames.(i) :: accu) (succ i) + in + Some (append stack 0) + +(** 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 handlers = ref [] + +let register_backtrace_handler h = + handlers := h :: !handlers + +let rec push_exn_aux e = function +| [] -> e +| f :: l -> + match f e with + | None -> push_exn_aux e l + | Some e -> e + +let push_exn e = + push_exn_aux e !handlers + +let reraise e = + let e = push_exn e in + raise e diff --git a/lib/backtrace.mli b/lib/backtrace.mli new file mode 100644 index 000000000..d10753552 --- /dev/null +++ b/lib/backtrace.mli @@ -0,0 +1,108 @@ +(***********************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *) +(* \VV/ *************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(***********************************************************************) + +(** * 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 = frame list option +(** Type of backtraces. They're just stack of frames. [None] indicates that we + don't care about recording the backtraces. *) + +val empty : t +(** Empty frame stack. *) + +val none : t +(** Frame stack that will not register anything. *) + +val push : t -> t +(** Add the current backtrace information to a given backtrace. *) + +(** {5 Utilities} *) + +val print_frame : frame -> string +(** Represent a frame. *) + +(** {5 Exception handling} *) + +val register_backtrace_handler : (exn -> exn option) -> unit +(** Add a handler to enrich backtrace information that may be carried by + exceptions. If the handler returns [None], this means that it is not its + duty to handle this one. Otherwise, the new exception will be used by the + functions thereafter instead of the original one. + + Handlers are called in the reverse order of their registration. If no + handler match, the original exception is returned. +*) + +val push_exn : exn -> exn +(** Add the current backtrace information to the given exception, using the + registered handlers. + + The intended use case is of the form: {[ + + try foo + with + | Bar -> bar + | err -> let err = push_exn 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 = push_exn err in + match err with + | Bar -> bar + | err -> baz + + ]} + + I admit that's a bit heavy, but there is not much to do... + +*) + +val reraise : exn -> 'a +(** Convenience function which covers a generic pattern in Coq code. + [reraise e] is equivalent to [raise (push_exn e)]. + + The intended use case is of the form: {[ + + try foo + with + | Bar -> bar + | err -> reraise err + + ]} + +*) diff --git a/lib/clib.mllib b/lib/clib.mllib index d40df73a0..55bfdc835 100644 --- a/lib/clib.mllib +++ b/lib/clib.mllib @@ -1,3 +1,4 @@ +Backtrace Int Pp_control Pp |