Getting rid of Exninfo hacks.

Instead of modifying exceptions to wear additional information, we instead use
a dedicated type now. All exception-using functions were modified to support
this new type, in particular Future's fix_exn-s and the tactic monad.

To solve the problem of enriching exceptions at raise time and recover this
data in the try-with handler, we use a global datastructure recording the
given piece of data imperatively that we retrieve in the try-with handler.
We ensure that such instrumented try-with destroy the data so that there
may not be confusion with another exception. To further harden the correction
of this structure, we also check for pointer equality with the last raised
exception.

The global data structure is not thread-safe for now, which is incorrect as
the STM uses threads and enriched exceptions. Yet, we splitted the patch in
two parts, so that we do not introduce dependencies to the Thread library
immediatly. This will allow to revert only the second patch if ever we
switch to OCaml-coded lightweight threads.

1 files changed, 30 insertions, 25 deletions

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 01bb41ad35..f1d10bbe55 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -230,7 +230,7 @@ let apply env t sp =
   let ans = Proof.repr (Proof.run t false (sp,env)) in
   let ans = Logic_monad.NonLogical.run ans in
   match ans with
-  | Nil e -> raise (TacticFailure e)
+  | Nil (e, info) -> iraise (TacticFailure e, info)
   | Cons ((r, (state, _), status, info), _) ->
     r, state, status, Trace.to_tree info
 
@@ -260,7 +260,12 @@ module Monad = Proof
 
 
 (** [tclZERO e] fails with exception [e]. It has no success. *)
-let tclZERO = Proof.zero
+let tclZERO ?info e =
+  let info = match info with
+  | None -> Exninfo.null
+  | Some info -> info
+  in
+  Proof.zero (e, info)
 
 (** [tclOR t1 t2] behaves like [t1] as long as [t1] succeeds. Whenever
     the successes of [t1] have been depleted and it failed with [e],
@@ -312,17 +317,17 @@ let tclEXACTLY_ONCE e t =
   let open Logic_monad in
   let open Proof in
   split t >>= function
-    | Nil e -> tclZERO e
+    | Nil (e, info) -> tclZERO ~info e
     | Cons (x,k) ->
-        Proof.split (k e) >>= function
+        Proof.split (k (e, Exninfo.null)) >>= function
           | Nil _ -> tclUNIT x
           | _ -> tclZERO MoreThanOneSuccess
 
 
 (** [tclCASE t] wraps the {!Proofview_monad.Logical.split} primitive. *)
 type 'a case =
-| Fail of exn
-| Next of 'a * (exn -> 'a tactic)
+| Fail of iexn
+| Next of 'a * (iexn -> 'a tactic)
 let tclCASE t =
   let open Logic_monad in
   let map = function
@@ -745,12 +750,12 @@ let tclTIMEOUT n t =
         | Logic_monad.Nil e -> return (Util.Inr e)
         | Logic_monad.Cons (r, _) -> return (Util.Inl r)
       end
-      begin let open Logic_monad.NonLogical in function
-        | Logic_monad.Timeout -> return (Util.Inr Timeout)
-        | Logic_monad.TacticFailure e as src ->
-          let e = Backtrace.app_backtrace ~src ~dst:e in
-          return (Util.Inr e)
-        | e -> Logic_monad.NonLogical.raise e
+      begin let open Logic_monad.NonLogical in function (e, info) ->
+        match e with
+        | Logic_monad.Timeout -> return (Util.Inr (Timeout, info))
+        | Logic_monad.TacticFailure e ->
+          return (Util.Inr (e, info))
+        | e -> Logic_monad.NonLogical.raise ~info e
       end
   end >>= function
     | Util.Inl (res,s,m,i) ->
@@ -758,7 +763,7 @@ let tclTIMEOUT n t =
         Proof.put m >>
         Proof.update (fun _ -> i) >>
         return res
-    | Util.Inr e -> tclZERO e
+    | Util.Inr (e, info) -> tclZERO ~info e
 
 let tclTIME s t =
   let pr_time t1 t2 n msg =
@@ -775,11 +780,11 @@ let tclTIME s t =
     tclUNIT () >>= fun () ->
     let tstart = System.get_time() in
     Proof.split t >>= let open Logic_monad in function
-    | Nil e ->
+    | Nil (e, info) ->
       begin
         let tend = System.get_time() in
         pr_time tstart tend n "failure";
-        tclZERO e
+        tclZERO ~info e
       end
     | Cons (x,k) ->
         let tend = System.get_time() in
@@ -894,8 +899,8 @@ module Goal = struct
         let (gl, sigma) = nf_gmake env sigma goal in
         tclTHEN (Unsafe.tclEVARS sigma) (InfoL.tag (Info.DBranch) (f gl))
       with e when catchable_exception e ->
-        let e = Errors.push e in
-        tclZERO e
+        let (e, info) = Errors.push e in
+        tclZERO ~info e
     end
     end
 
@@ -917,8 +922,8 @@ module Goal = struct
       tclEVARMAP >>= fun sigma ->
       try f (gmake env sigma goal)
       with e when catchable_exception e ->
-        let e = Errors.push e in
-        tclZERO e
+        let (e, info) = Errors.push e in
+        tclZERO ~info e
     end
     end
 
@@ -1082,8 +1087,8 @@ module V82 = struct
       InfoL.leaf (Info.Tactic (fun () -> Pp.str"<unknown>")) >>
       Pv.set { solution = evd; comb = sgs; }
     with e when catchable_exception e ->
-      let e = Errors.push e in
-      tclZERO e
+      let (e, info) = Errors.push e in
+      tclZERO ~info e
 
 
   (* normalises the evars in the goals, and stores the result in
@@ -1141,9 +1146,8 @@ module V82 = struct
       let (_,final,_,_) = apply (GoalV82.env gls.Evd.sigma gls.Evd.it) t init in
       { Evd.sigma = final.solution ; it = final.comb }
     with Logic_monad.TacticFailure e as src ->
-      let src = Errors.push src in
-      let e = Backtrace.app_backtrace ~src ~dst:e in
-      raise e
+      let (_, info) = Errors.push src in
+      iraise (e, info)
 
   let put_status = Status.put
 
@@ -1151,6 +1155,7 @@ module V82 = struct
 
   let wrap_exceptions f =
     try f ()
-    with e when catchable_exception e -> let e = Errors.push e in tclZERO e
+    with e when catchable_exception e ->
+      let (e, info) = Errors.push e in tclZERO ~info e
 
 end