Updating the backtrace handling mechanism to accomodate the new

exception information addition facility.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16213 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 71 insertions, 119 deletions

diff --git a/lib/backtrace.ml b/lib/backtrace.ml
index 84f208c9ef..4955437b37 100644
--- a/lib/backtrace.ml
+++ b/lib/backtrace.ml
@@ -26,11 +26,9 @@ 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
+type t = frame list
 
-let empty = Some []
-
-let none = None
+let empty = []
 
 let of_raw = function
 | Unknown_location r ->
@@ -44,18 +42,15 @@ let of_raw = function
   } 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)
+let push stack = match get_exception_backtrace () with
+| None -> []
+| 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
+  append stack 0
 
 (** Utilities *)
 
@@ -69,21 +64,33 @@ let print_frame frame =
 
 (** 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
+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
+    let current = get_exception_backtrace () in
+    begin match current with
+    | None -> e
+    | 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
+      let old = match get_backtrace e with
+      | None -> []
+      | Some bt -> bt
+      in
+      let bt = append old 0 in
+      Exninfo.add e backtrace bt
+    end
+  else e
diff --git a/lib/backtrace.mli b/lib/backtrace.mli
index d107535523..d5a96e6f75 100644
--- a/lib/backtrace.mli
+++ b/lib/backtrace.mli
@@ -32,16 +32,13 @@ 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 t = frame list
 (** 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. *)
 
@@ -52,26 +49,22 @@ val print_frame : frame -> string
 
 (** {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.
+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. *)
 
-    Handlers are called in the reverse order of their registration. If no
-    handler match, the original exception is returned.
-*)
+val get_backtrace : exn -> t option
+(** Retrieve the optional backtrace coming with the exception. *)
 
-val push_exn : exn -> exn
-(** Add the current backtrace information to the given exception, using the
-    registered handlers.
+val add_backtrace : exn -> exn
+(** 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 = push_exn err in baz
+      | err -> let err = add_backtrace err in baz
 
     ]}
 
@@ -81,7 +74,7 @@ val push_exn : exn -> exn
 
     try foo
       with err ->
-        let err = push_exn err in
+        let err = add_backtrace err in
         match err with
         | Bar -> bar
         | err -> baz
@@ -91,18 +84,3 @@ val push_exn : exn -> exn
     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/errors.ml b/lib/errors.ml
index e1a8d46b76..92e5ac6423 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -10,37 +10,23 @@ open Pp
 
 (** Aliases *)
 
-let push = Backtrace.push_exn
-
-let reraise = Backtrace.reraise
+let push = Backtrace.add_backtrace
 
 (* Errors *)
 
-exception Anomaly of string option * std_ppcmds * Backtrace.t (* System errors *)
+exception Anomaly of string option * std_ppcmds (* System errors *)
 
 let make_anomaly ?label pp =
-  let bt =
-    if !Flags.debug then Backtrace.empty
-    else Backtrace.none
-  in
-  Anomaly (label, pp, bt)
+  Anomaly (label, pp)
 
 let anomaly_gen label pp =
-  let bt =
-    if !Flags.debug then Backtrace.empty
-    else Backtrace.none
-  in
-  raise (Anomaly (label, pp, bt))
+  raise (Anomaly (label, pp))
 
 let anomaly ?loc ?label pp =
-  let bt =
-    if !Flags.debug then Backtrace.empty
-    else Backtrace.none
-  in
   match loc with
-  | None -> raise (Anomaly (label, pp, bt))
+  | None -> raise (Anomaly (label, pp))
   | Some loc ->
-    Loc.raise loc (Anomaly (label, pp, bt))
+    Loc.raise loc (Anomaly (label, pp))
 
 let anomalylabstrm string pps =
   anomaly_gen (Some string) pps
@@ -99,17 +85,17 @@ let where = function
   if !Flags.debug then str ("in "^s^":") ++ spc () else mt ()
 
 let raw_anomaly e = match e with
-  | Anomaly (s, pps, bt) -> where s ++ pps ++ str "."
+  | Anomaly (s, pps) -> where s ++ pps ++ str "."
   | Assert_failure _ | Match_failure _ -> str (Printexc.to_string e ^ ".")
   | _ -> str ("Uncaught exception " ^ Printexc.to_string e ^ ".")
 
 let print_anomaly askreport e =
-  let bt_info = match e with
-  | Anomaly (_, _, Some bt) ->
+  let bt_info = match Backtrace.get_backtrace e with
+  | None -> mt ()
+  | Some bt ->
     let pr_frame f = str (Backtrace.print_frame f) in
     let bt = prlist_with_sep fnl pr_frame bt in
     fnl () ++ hov 0 bt
-  | _ -> mt ()
   in
   let info =
     if askreport then
@@ -138,22 +124,3 @@ let _ = register_handler begin function
   | UserError(s,pps) -> hov 0 (str "Error: " ++ where (Some s) ++ pps)
   | _ -> raise Unhandled
 end
-
-let rec anomaly_handler = function
-| Anomaly (lbl, pp, bt) ->
-  let bt = Backtrace.push bt in
-  Some (Anomaly (lbl, pp, bt))
-| Loc.Exc_located (loc, e) ->
-  begin match anomaly_handler e with
-  | None -> None
-  | Some e -> Some (Loc.Exc_located (loc, e))
-  end
-| Error_in_file (s, data, e) ->
-  begin match anomaly_handler e with
-  | None -> None
-  | Some e -> Some (Error_in_file (s, data, e))
-  end
-| e -> None
-
-let record_backtrace () =
-  Backtrace.register_backtrace_handler anomaly_handler
diff --git a/lib/errors.mli b/lib/errors.mli
index d596abb55a..3e551e394c 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -14,10 +14,7 @@ open Pp
 (** {6 Error handling} *)
 
 val push : exn -> exn
-(** Alias for [Backtrace.push_exn]. *)
-
-val reraise : exn -> 'a
-(** Alias for [Backtrace.reraise]. *)
+(** Alias for [Backtrace.add_backtrace]. *)
 
 (** {6 Generic errors.}
 
@@ -93,6 +90,3 @@ val print_no_report : exn -> Pp.std_ppcmds
 (** Same as [print], except that anomalies are not printed but re-raised
     (used for the Fail command) *)
 val print_no_anomaly : exn -> Pp.std_ppcmds
-
-(** Enable registering of backtrace information. *)
-val record_backtrace : unit -> unit
diff --git a/lib/flags.ml b/lib/flags.ml
index b4c72b38a1..727e2184b7 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -9,12 +9,18 @@
 let with_option o f x =
   let old = !o in o:=true;
   try let r = f x in o := old; r
-  with e -> o := old; Backtrace.reraise e
+  with e ->
+    let e = Backtrace.add_backtrace e in
+    let () = o := old in
+    raise e
 
 let without_option o f x =
   let old = !o in o:=false;
   try let r = f x in o := old; r
-  with e -> o := old; Backtrace.reraise e
+  with e ->
+    let e = Backtrace.add_backtrace e in
+    let () = o := old in
+    raise e
 
 let boot = ref false
 
diff --git a/lib/pp.ml b/lib/pp.ml
index b9dc05edff..99bd93411b 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -263,7 +263,7 @@ let pp_dirs ft =
     try
       Stream.iter pp_dir dirstream; com_brk ft
     with e ->
-      let e = Backtrace.push_exn e in
+      let e = Backtrace.add_backtrace e in
       let () = Format.pp_print_flush ft () in
       raise e