Added backtrace information to anomalies

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

10 files changed, 73 insertions, 23 deletions

diff --git a/checker/checker.ml b/checker/checker.ml
index 1b7af5178..b3c8b0e8c 100644
--- a/checker/checker.ml
+++ b/checker/checker.ml
@@ -238,8 +238,6 @@ let rec explain_exn = function
       hov 0 (str "Out of memory")
   | Stack_overflow ->
       hov 0 (str "Stack overflow")
-  | Anomaly (s,pps) ->
-      hov 1 (anomaly_string () ++ where s ++ pps ++ report ())
   | Match_failure(filename,pos1,pos2) ->
       hov 1 (anomaly_string () ++ str "Match failure in file " ++
 	     str (guill filename) ++ str " at line " ++ int pos1 ++
@@ -283,6 +281,8 @@ let rec explain_exn = function
 		   str ", characters " ++ int e ++ str "-" ++
 		   int (e+6) ++ str ")")) ++
 	       report ())
+  | e when is_anomaly e ->
+      print_anomaly e
   | reraise ->
       hov 0 (anomaly_string () ++ str "Uncaught exception " ++
 	       str (Printexc.to_string reraise)++report())
diff --git a/lib/errors.ml b/lib/errors.ml
index 77f03f045..d4d285a05 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -10,9 +10,31 @@ open Pp
 
 (* Errors *)
 
-exception Anomaly of string * std_ppcmds  (* System errors *)
-let anomaly string = raise (Anomaly(string, str string))
-let anomalylabstrm string pps = raise (Anomaly(string,pps))
+type backtrace = string option
+
+exception Anomaly of string option * std_ppcmds * backtrace (* System errors *)
+
+let get_backtrace () =
+  if !Flags.debug then Some (Printexc.get_backtrace ())
+  else None
+
+let make_anomaly ?label pp =
+  let bt = get_backtrace () in
+  Anomaly (label, pp, bt)
+
+let anomaly_gen label pp =
+  let bt = get_backtrace () in
+  raise (Anomaly (label, pp, bt))
+
+let anomaly string =
+  anomaly_gen None (str string)
+
+let anomalylabstrm string pps =
+  anomaly_gen (Some string) pps
+
+let is_anomaly = function
+| Anomaly _ -> true
+| _ -> false
 
 exception UserError of string * std_ppcmds (* User errors *)
 let error string = raise (UserError("_", str string))
@@ -24,7 +46,10 @@ let alreadydeclared pps = raise (AlreadyDeclared(pps))
 let todo s = prerr_string ("TODO: "^s^"\n")
 
 (* raising located exceptions *)
-let anomaly_loc (loc,s,strm) = Loc.raise loc (Anomaly (s,strm))
+let anomaly_loc (loc,s,strm) =
+  let bt = get_backtrace () in
+  Loc.raise loc (Anomaly (Some s, strm, bt))
+
 let user_err_loc (loc,s,strm) = Loc.raise loc (UserError (s,strm))
 let invalid_arg_loc (loc,s) = Loc.raise loc (Invalid_argument s)
 
@@ -60,19 +85,28 @@ let rec print_gen bottom stk e =
     In usual situation, the [handle_stack] is treated as it if was always
     non-empty with [print_anomaly] as its bottom handler. *)
 
-let where s =
+let where = function
+| None -> mt ()
+| Some s ->
   if !Flags.debug then str ("in "^s^":") ++ spc () else mt ()
 
 let raw_anomaly e = match e with
-  | Anomaly (s,pps) -> where s ++ pps ++ str "."
+  | Anomaly (s, pps, bt) -> 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 =
-  if askreport then
-    hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ str "Please report.")
-  else
-    hov 0 (raw_anomaly e)
+  let bt_info = match e with
+  | Anomaly (_, _, Some bt) -> (fnl () ++ hov 0 (str bt))
+  | _ -> mt ()
+  in
+  let info =
+    if askreport then
+      hov 0 (str "Anomaly: " ++ raw_anomaly e ++ spc () ++ str "Please report.")
+    else
+      hov 0 (raw_anomaly e)
+  in
+  info ++ bt_info
 
 (** The standard exception printer *)
 let print e = print_gen (print_anomaly true) !handle_stack e
@@ -81,6 +115,8 @@ let print e = print_gen (print_anomaly true) !handle_stack e
     isn't printed (used in Ltac debugging). *)
 let print_no_report e = print_gen (print_anomaly false) !handle_stack e
 
+let print_anomaly e = print_anomaly true e
+
 (** Same as [print], except that anomalies are not printed but re-raised
     (used for the Fail command) *)
 let print_no_anomaly e = print_gen (fun e -> raise e) !handle_stack e
@@ -88,7 +124,7 @@ let print_no_anomaly e = print_gen (fun e -> raise e) !handle_stack e
 (** Predefined handlers **)
 
 let _ = register_handler begin function
-  | UserError(s,pps) -> hov 0 (str "Error: " ++ where s ++ pps)
+  | UserError(s,pps) -> hov 0 (str "Error: " ++ where (Some s) ++ pps)
   | _ -> raise Unhandled
 end
 
diff --git a/lib/errors.mli b/lib/errors.mli
index 3dd470a06..0b2defa1a 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -16,11 +16,16 @@ open Pp
  [Anomaly] is used for system errors and [UserError] for the
    user's ones. *)
 
-exception Anomaly of string * std_ppcmds
+val make_anomaly : ?label:string -> std_ppcmds -> exn
+(** Create an anomaly. *)
+
 val anomaly : string -> 'a
 val anomalylabstrm : string -> std_ppcmds -> 'a
 val anomaly_loc : Loc.t * string * std_ppcmds -> 'a
 
+val is_anomaly : exn -> bool
+(** Check whether a given exception is an anomaly. *)
+
 exception UserError of string * std_ppcmds
 val error : string -> 'a
 val errorlabstrm : string -> std_ppcmds -> 'a
@@ -70,6 +75,9 @@ val register_handler : (exn -> Pp.std_ppcmds) -> unit
 (** The standard exception printer *)
 val print : exn -> Pp.std_ppcmds
 
+(** Exception printer dedicated to anomalies. *)
+val print_anomaly : exn -> Pp.std_ppcmds
+
 (** Same as [print], except that the "Please report" part of an anomaly
     isn't printed (used in Ltac debugging). *)
 val print_no_report : exn -> Pp.std_ppcmds
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 15395ca7f..fe03cae8c 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -194,7 +194,7 @@ let invert_ltac_bound_name env id0 id =
 
 let protected_get_type_of env sigma c =
   try Retyping.get_type_of env sigma c
-  with Anomaly _ ->
+  with e when is_anomaly e ->
     errorlabstrm "" (str "Cannot reinterpret " ++ quote (print_constr c) ++ str " in the current environment.")
 
 let pretype_id loc env sigma (lvar,unbndltacvars) id =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 48b15b1dd..6ec5ab9b4 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -608,7 +608,7 @@ let clos_norm_flags flgs env sigma t =
     norm_val
       (create_clos_infos ~evars:(safe_evar_value sigma) flgs env)
       (inject t)
-  with Anomaly _ -> error "Tried to normalized ill-typed term"
+  with e when is_anomaly e -> error "Tried to normalized ill-typed term"
 
 let nf_beta = clos_norm_flags Closure.beta empty_env
 let nf_betaiota = clos_norm_flags Closure.betaiota empty_env
@@ -713,7 +713,7 @@ let test_conversion (f: ?l2r:bool-> ?evars:'a->'b) env sigma x y =
   try let _ =
     f ~evars:(safe_evar_value sigma) env x y in true
   with NotConvertible -> false
-    | Anomaly _ -> error "Conversion test raised an anomaly"
+    | e when is_anomaly e -> error "Conversion test raised an anomaly"
 
 let is_conv env sigma = test_conversion Reduction.conv env sigma
 let is_conv_leq env sigma = test_conversion Reduction.conv_leq env sigma
@@ -722,7 +722,7 @@ let is_fconv = function | CONV -> is_conv | CUMUL -> is_conv_leq
 let test_trans_conversion (f: ?l2r:bool-> ?evars:'a->'b) reds env sigma x y =
   try let _ = f ~evars:(safe_evar_value sigma) reds env x y in true
   with NotConvertible -> false
-    | Anomaly _ -> error "Conversion test raised an anomaly"
+    | e when is_anomaly e -> error "Conversion test raised an anomaly"
 
 let is_trans_conv reds env sigma = test_trans_conversion Reduction.trans_conv reds env sigma
 let is_trans_conv_leq reds env sigma = test_trans_conversion Reduction.trans_conv_leq reds env sigma
diff --git a/proofs/monads.ml b/proofs/monads.ml
index 1337931b1..78a79909e 100644
--- a/proofs/monads.ml
+++ b/proofs/monads.ml
@@ -166,7 +166,9 @@ end = struct
     (* spiwack: I cannot be sure right now, but [anomaly] shouldn't be
        reachable. If it is reachable there may be some redesign to be
        done around success continuations. *)
-    let anomaly = Errors.Anomaly ("Monads.Logic(T).split", Pp.str"[fk] should ignore this error") in
+    let anomaly = Errors.make_anomaly ~label:"Monads.Logic(T).split"
+      (Pp.str "[fk] should ignore this error")
+    in
     let fk e = T.return (Util.Inr e) in
     let sk a fk = T.return (Util.Inl (a,bind (lift (fk anomaly)) reflect)) in
     lift (x.go sk fk)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index ac349bd8d..7a041214d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1744,9 +1744,10 @@ and interp_atomic ist gl tac =
 	 is dropped as the evar_map taken as input (from
 	 extend_gl_hyps) is incorrect.  This means that evar
 	 instantiated by pf_interp_constr may be lost, there. *)
+      let to_catch = function Not_found -> true | e -> Errors.is_anomaly e in
       let (_,c_interp) =
 	try pf_interp_constr ist (extend_gl_hyps gl sign) c
-	with Not_found | Anomaly _ (* Hack *) ->
+	with e when to_catch e (* Hack *) ->
 	   errorlabstrm "" (strbrk "Failed to get enough information from the left-hand side to type the right-hand side.")
       in
       tclTHEN
diff --git a/toplevel/coqinit.ml b/toplevel/coqinit.ml
index 59d73e7bd..b4d0bc413 100644
--- a/toplevel/coqinit.ml
+++ b/toplevel/coqinit.ml
@@ -11,7 +11,9 @@ open Pp
 
 let (/) = Filename.concat
 
-let set_debug () = Flags.debug := true
+let set_debug () =
+  let () = Printexc.record_backtrace true in
+  Flags.debug := true
 
 (* Loading of the ressource file.
    rcfile is either $XDG_CONFIG_HOME/.coqrc.VERSION, or $XDG_CONFIG_HOME/.coqrc if the first one
diff --git a/toplevel/mltop.ml b/toplevel/mltop.ml
index cf5f64465..4ac6adc35 100644
--- a/toplevel/mltop.ml
+++ b/toplevel/mltop.ml
@@ -117,7 +117,8 @@ let dir_ml_load s =
     | WithTop t ->
       (try t.load_obj s
        with
-       | (UserError _ | Failure _ | Anomaly _ | Not_found as u) -> raise u
+       | (UserError _ | Failure _ | Not_found as u) -> raise u
+       | u when Errors.is_anomaly u -> raise u
        | exc ->
            let msg = report_on_load_obj_error exc in
            errorlabstrm "Mltop.load_object" (str"Cannot link ml-object " ++
diff --git a/toplevel/obligations.ml b/toplevel/obligations.ml
index fd5156453..03bad4c1c 100644
--- a/toplevel/obligations.ml
+++ b/toplevel/obligations.ml
@@ -823,7 +823,7 @@ and solve_obligation_by_tac prg obls i tac =
 	| Loc.Exc_located(_, Refiner.FailError (_, s))
 	| Refiner.FailError (_, s) ->
 	    user_err_loc (fst obl.obl_location, "solve_obligation", Lazy.force s)
-	| Errors.Anomaly _ as e -> raise e
+	| e when Errors.is_anomaly e -> raise e
 	| e -> false
 
 and solve_prg_obligations prg ?oblset tac =