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.

17 files changed, 116 insertions, 130 deletions

diff --git a/lib/backtrace.ml b/lib/backtrace.ml
index 19b07d876..b3b8bdea2 100644
--- a/lib/backtrace.ml
+++ b/lib/backtrace.ml
@@ -84,18 +84,23 @@ let get_backtrace e =
 
 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
+    | None -> (e, info)
     | Some fragment ->
-      let bt = match get_backtrace e with
+      let bt = match get_backtrace info with
       | None -> []
       | Some bt -> bt
       in
       let bt = fragment :: bt in
-      Exninfo.add e backtrace bt
+      (e, Exninfo.add info backtrace bt)
     end
-  else e
+  else
+    let info = Exninfo.info e in
+    (e, info)
 
 let app_backtrace ~src ~dst =
   if !is_recording then
diff --git a/lib/backtrace.mli b/lib/backtrace.mli
index ecd046b54..dd82165b6 100644
--- a/lib/backtrace.mli
+++ b/lib/backtrace.mli
@@ -56,10 +56,10 @@ 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 : exn -> t option
+val get_backtrace : Exninfo.info -> t option
 (** Retrieve the optional backtrace coming with the exception. *)
 
-val add_backtrace : exn -> exn
+val add_backtrace : exn -> Exninfo.iexn
 (** Add the current backtrace information to the given exception.
 
     The intended use case is of the form: {[
@@ -88,7 +88,7 @@ val add_backtrace : exn -> exn
 
 *)
 
-val app_backtrace : src:exn -> dst:exn -> exn
+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
diff --git a/lib/control.ml b/lib/control.ml
index cce9d3a9f..04d176092 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -41,7 +41,7 @@ let unix_timeout n f e =
   with e ->
     let e = Backtrace.add_backtrace e in
     restore_timeout ();
-    raise e
+    Exninfo.iraise e
 
 let windows_timeout n f e =
   let killed = ref false in
@@ -78,7 +78,7 @@ let windows_timeout n f e =
   | e ->
     let () = killed := true in
     let e = Backtrace.add_backtrace e in
-    raise e
+    Exninfo.iraise e
 
 type timeout = { timeout : 'a. int -> (unit -> 'a) -> exn -> 'a }
 
diff --git a/lib/errors.ml b/lib/errors.ml
index 45e0f9fdf..ab331d6a4 100644
--- a/lib/errors.ml
+++ b/lib/errors.ml
@@ -91,8 +91,10 @@ let print_anomaly askreport e =
     hov 0 (raw_anomaly e)
 
 (** The standard exception printer *)
-let print e =
-  print_gen (print_anomaly true) !handle_stack e ++ print_backtrace e
+let print ?(info = Exninfo.null) e =
+  print_gen (print_anomaly true) !handle_stack e ++ print_backtrace info
+
+let iprint (e, info) = print ~info e
 
 (** Same as [print], except that the "Please report" part of an anomaly
     isn't printed (used in Ltac debugging). *)
diff --git a/lib/errors.mli b/lib/errors.mli
index 7e296e45e..e4096a7ef 100644
--- a/lib/errors.mli
+++ b/lib/errors.mli
@@ -13,7 +13,7 @@ open Pp
 
 (** {6 Error handling} *)
 
-val push : exn -> exn
+val push : exn -> Exninfo.iexn
 (** Alias for [Backtrace.add_backtrace]. *)
 
 (** {6 Generic errors.}
@@ -74,7 +74,8 @@ exception Unhandled
 val register_handler : (exn -> Pp.std_ppcmds) -> unit
 
 (** The standard exception printer *)
-val print : exn -> Pp.std_ppcmds
+val print : ?info:Exninfo.info -> exn -> Pp.std_ppcmds
+val iprint : Exninfo.iexn -> Pp.std_ppcmds
 
 (** Same as [print], except that the "Please report" part of an anomaly
     isn't printed (used in Ltac debugging). *)
diff --git a/lib/exninfo.ml b/lib/exninfo.ml
index 845b8d190..2eca5f4a7 100644
--- a/lib/exninfo.ml
+++ b/lib/exninfo.ml
@@ -14,89 +14,44 @@ module Store = Store.Make(struct end)
 
 type 'a t = 'a Store.field
 
-let token = Obj.repr "HACK"
-(** Unique token used to recognize enriched exceptions. *)
+type info = Store.t
 
-let make = Store.field
-
-(** Discriminate normal data w.r.t enriched exceptions *)
-let is_data obj =
-  Obj.is_block obj && Obj.size obj = 2 && Obj.field obj 0 == token
-
-(** As [Array.blit] *)
-let blit obj1 off1 obj2 off2 len =
-  for i = 0 to len - 1 do
-    let data = Obj.field obj1 (off1 + i) in
-    Obj.set_field obj2 (off2 + i) data
-  done
-
-(** Retrieve the optional backtrace set in an exception. *)
-let get (e : exn) i =
-  let obj = Obj.repr e in
-  let len = Obj.size obj in
-  let lst = Obj.field obj (len - 1) in
-  if is_data lst then
-    let data = Obj.obj (Obj.field lst 1) in
-    Store.get data i
-  else None
+type iexn = exn * info
 
-(** Add data to any exception *)
-let add e i v : exn =
-  let obj = Obj.repr e in
-  let len = Obj.size obj in
-  let lst = Obj.field obj (len - 1) in
-  if is_data lst then
-    (** The exception was already enriched *)
-    let data = Obj.obj (Obj.field lst 1) in
-    (** We retrieve the old information and update it *)
-    let data = Store.set data i v in
-    let ans = Obj.dup obj in
-    let data = Obj.repr (token, data) in
-    let () = Obj.set_field ans (len - 1) data in
-    Obj.obj ans
+let make = Store.field
+let add = Store.set
+let get = Store.get
+let null = Store.empty
+
+exception Unique
+
+let dummy = (Unique, Store.empty)
+
+let current = ref dummy
+
+let iraise e =
+  let () = current := e in
+  raise (fst e)
+
+let raise ?info e = match info with
+| None -> raise e
+| Some i -> current := (e, i); raise e
+
+let info e =
+  let (src, data) = !current in
+  if src == e then
+    (** Slightly unsound, some exceptions may not be unique up to pointer
+        equality. Though, it should be quite exceptional to be in a situation
+        where the following holds:
+
+        1. An argument-free exception is raised through the enriched {!raise};
+        2. It is not captured by any enriched with-clause (which would reset
+            the current data);
+        3. The same exception is raised through the standard raise, accessing
+            the wrong data.
+    . *)
+    let () = current := dummy in
+    data
   else
-    (** This was a plain exception *)
-    let ans = Obj.new_block 0 (succ len) in
-    (** We build the new enriched exception from scratch *)
-    let () = blit obj 0 ans 0 len in
-    let data = Store.set Store.empty i v in
-    let data = Obj.repr (token, data) in
-    let () = Obj.set_field ans len data in
-    Obj.obj ans
-
-let clear e =
-  let obj = Obj.repr e in
-  let len = Obj.size obj in
-  let lst = Obj.field obj (len - 1) in
-  if is_data lst then
-    let ans = Obj.new_block 0 (pred len) in
-    let () = blit obj 0 ans 0 (pred len) in
-    Obj.obj ans
-  else e
-
-let copy (src : exn) (dst : exn) =
-  let obj = Obj.repr src in
-  let len = Obj.size obj in
-  let lst = Obj.field obj (len - 1) in
-  if is_data lst then
-    (** First object has data *)
-    let src_data = Obj.obj (Obj.field lst 1) in
-    let obj = Obj.repr dst in
-    let len = Obj.size obj in
-    let lst = Obj.field obj (len - 1) in
-    if is_data lst then
-      (** second object has data *)
-      let dst_data = Obj.obj (Obj.field lst 1) in
-      let ans = Obj.dup obj in
-      let data = Obj.repr (token, Store.merge src_data dst_data) in
-      let () = Obj.set_field ans len data in
-      Obj.obj ans
-    else
-      (** second object has no data *)
-      let ans = Obj.new_block 0 (succ len) in
-      (** We build the new enriched exception from scratch *)
-      let () = blit obj 0 ans 0 len in
-      let data = Obj.repr (token, src_data) in
-      let () = Obj.set_field ans len data in
-      Obj.obj ans
-  else dst
+    let () = current := dummy in
+    Store.empty
diff --git a/lib/exninfo.mli b/lib/exninfo.mli
index 844ff0f96..c960ac7c0 100644
--- a/lib/exninfo.mli
+++ b/lib/exninfo.mli
@@ -11,20 +11,29 @@
 type 'a t
 (** Information containing a given type. *)
 
+type info
+(** All information *)
+
+type iexn = exn * info
+(** Information-wearing exceptions *)
+
 val make : unit -> 'a t
 (** Create a new piece of information. *)
 
-val add : exn -> 'a t -> 'a -> exn
+val null : info
+(** No information *)
+
+val add : info -> 'a t -> 'a -> info
 (** Add information to an exception. *)
 
-val get : exn -> 'a t -> 'a option
+val get : info -> 'a t -> 'a option
 (** Get information worn by an exception. Returns [None] if undefined. *)
 
-(* val remove : exn -> 'a t -> exn *)
-(** TODO: Remove a given piece of information. *)
+val info : exn -> info
+(** Retrieve the information of the last exception raised. *)
 
-val clear : exn -> exn
-(** Remove any information. *)
+val iraise : iexn -> 'a
+(** Raise the given enriched exception. *)
 
-val copy : exn -> exn -> exn
-(** [copy src dst] adds the additional info from [src] to [dst]. *)
+val raise : ?info:info -> exn -> 'a
+(** Raise the given exception with additional information. *)
diff --git a/lib/flags.ml b/lib/flags.ml
index 31b40dc53..0c6fef8be 100644
--- a/lib/flags.ml
+++ b/lib/flags.ml
@@ -12,7 +12,7 @@ let with_option o f x =
    with reraise ->
      let reraise = Backtrace.add_backtrace reraise in
      let () = o := old in
-     raise reraise
+     Exninfo.iraise reraise
 
 let with_options ol f x =
   let vl = List.map (!) ol in
@@ -23,7 +23,7 @@ let with_options ol f x =
   with reraise ->
     let reraise = Backtrace.add_backtrace reraise in
     let () = List.iter2 (:=) ol vl in
-    raise reraise
+    Exninfo.iraise reraise
 
 let without_option o f x =
   let old = !o in o:=false;
@@ -31,7 +31,7 @@ let without_option o f x =
   with reraise ->
     let reraise = Backtrace.add_backtrace reraise in
     let () = o := old in
-    raise reraise
+    Exninfo.iraise reraise
 
 let with_extra_values o l f x =
   let old = !o in o:=old@l;
@@ -39,7 +39,7 @@ let with_extra_values o l f x =
   with reraise ->
     let reraise = Backtrace.add_backtrace reraise in
     let () = o := old in
-    raise reraise
+    Exninfo.iraise reraise
 
 let boot = ref false
 let load_init = ref true
diff --git a/lib/future.ml b/lib/future.ml
index b851f912c..52a060c93 100644
--- a/lib/future.ml
+++ b/lib/future.ml
@@ -26,7 +26,7 @@ let _ = Errors.register_handler (function
                 "asynchronous script processing.")
   | _ -> raise Errors.Unhandled)
 
-type fix_exn = exn -> exn
+type fix_exn = Exninfo.iexn -> Exninfo.iexn
 let id x = prerr_endline "Future: no fix_exn.\nYou have probably created a Future.computation from a value without passing the ~fix_exn argument.  You probably want to chain with an already existing future instead."; x
 
 module UUID = struct
@@ -43,7 +43,7 @@ end
 module UUIDMap = Map.Make(UUID)
 module UUIDSet = Set.Make(UUID)
 
-type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation]
+type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
 
 (* Val is not necessarily a final state, so the
    computation restarts from the state stocked into Val *)
@@ -51,7 +51,7 @@ and 'a comp =
   | Delegated of (unit -> unit)
   | Closure of (unit -> 'a)
   | Val of 'a * Dyn.t option
-  | Exn of exn (* Invariant: this exception is always "fixed" as in fix_exn *)
+  | Exn of Exninfo.iexn  (* Invariant: this exception is always "fixed" as in fix_exn *)
 
 and 'a comput =
   | Ongoing of (UUID.t * fix_exn * 'a comp ref) Ephemeron.key
@@ -66,9 +66,10 @@ let get x =
   | Finished v -> UUID.invalid, id, ref (Val (v,None))
   | Ongoing x ->
       try Ephemeron.get x
-      with Ephemeron.InvalidKey -> UUID.invalid, id, ref (Exn NotHere)
+      with Ephemeron.InvalidKey ->
+        UUID.invalid, id, ref (Exn (NotHere, Exninfo.null))
 
-type 'a value = [ `Val of 'a | `Exn of exn ]
+type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn  ]
 
 let is_over kx = let _, _, x = get kx in match !x with
   | Val _ | Exn _ -> true
@@ -116,7 +117,7 @@ let rec compute ~pure ck : 'a value =
   let _, fix_exn, c = get ck in
   match !c with
   | Val (x, _) -> `Val x
-  | Exn e -> `Exn e
+  | Exn (e, info) -> `Exn (e, info)
   | Delegated wait -> wait (); compute ~pure ck
   | Closure f ->
       try
@@ -127,12 +128,12 @@ let rec compute ~pure ck : 'a value =
         let e = Errors.push e in
         let e = fix_exn e in
         match e with
-        | NotReady -> `Exn e
+        | (NotReady, _) -> `Exn e
         | _ -> c := Exn e; `Exn e
 
 let force ~pure x = match compute ~pure x with
   | `Val v -> v
-  | `Exn e -> raise e
+  | `Exn e -> Exninfo.iraise e
 
 let chain ~pure ck f =
   let uuid, fix_exn, c = get ck in
@@ -167,12 +168,14 @@ let purify f x =
     let v = f x in
     !unfreeze state;
     v
-  with e -> let e = Errors.push e in !unfreeze state; raise e
+  with e ->
+    let e = Errors.push e in !unfreeze state; Exninfo.iraise e
 
 let transactify f x =
   let state = !freeze () in
   try f x
-  with e -> let e = Errors.push e in !unfreeze state; raise e
+  with e ->
+    let e = Errors.push e in !unfreeze state; Exninfo.iraise e
 
 let purify_future f x = if is_over x then f x else purify f x
 let compute x = purify_future (compute ~pure:false) x
@@ -214,4 +217,4 @@ let print f kx =
   | Closure _ -> str "Closure" ++ uid
   | Val (x, None) -> str "PureVal" ++ uid ++ spc () ++ hov 0 (f x)
   | Val (x, Some _) -> str "StateVal" ++ uid ++ spc () ++ hov 0 (f x)
-  | Exn e -> str "Exn"  ++ uid ++ spc () ++ hov 0 (str (Printexc.to_string e))
+  | Exn (e, _) -> str "Exn"  ++ uid ++ spc () ++ hov 0 (str (Printexc.to_string e))
diff --git a/lib/future.mli b/lib/future.mli
index bae4fa751..d97b46382 100644
--- a/lib/future.mli
+++ b/lib/future.mli
@@ -66,8 +66,8 @@ module UUIDSet : Set.S with type elt = UUID.t
 exception NotReady
 
 type 'a computation
-type 'a value = [ `Val of 'a | `Exn of exn ]
-type fix_exn = exn -> exn
+type 'a value = [ `Val of 'a | `Exn of Exninfo.iexn ]
+type fix_exn = Exninfo.iexn -> Exninfo.iexn
 
 (* Build a computation, no snapshot of the global state is taken.  If you need
    to grab a copy of the state start with from_here () and then chain.
@@ -98,7 +98,7 @@ val fix_exn_of : 'a computation -> fix_exn
 (* Run remotely, returns the function to assign.
    If not blocking (the default) it raises NotReady if forced before the
    delage assigns it. *)
-type 'a assignement = [ `Val of 'a | `Exn of exn | `Comp of 'a computation]
+type 'a assignement = [ `Val of 'a | `Exn of Exninfo.iexn | `Comp of 'a computation]
 val create_delegate :
   ?blocking:bool -> fix_exn -> 'a computation * ('a assignement -> unit)
 
diff --git a/lib/loc.ml b/lib/loc.ml
index 8f133ce0d..5ca345fd2 100644
--- a/lib/loc.ml
+++ b/lib/loc.ml
@@ -74,4 +74,6 @@ let add_loc e loc = Exninfo.add e location loc
 
 let get_loc e = Exninfo.get e location
 
-let raise loc e = raise (Exninfo.add e location loc)
+let raise loc e =
+  let info = Exninfo.add Exninfo.null location loc in
+  Exninfo.iraise (e, info)
diff --git a/lib/loc.mli b/lib/loc.mli
index a0b99c689..e9bf946a8 100644
--- a/lib/loc.mli
+++ b/lib/loc.mli
@@ -40,10 +40,10 @@ val represent : t -> (string * int * int * int * int)
 
 (** {5 Located exceptions} *)
 
-val add_loc : exn -> t -> exn
+val add_loc : Exninfo.info -> t -> Exninfo.info
 (** Adding location to an exception *)
 
-val get_loc : exn -> t option
+val get_loc : Exninfo.info -> t option
 (** Retrieving the optional location of an exception *)
 
 val raise : t -> exn -> 'a
diff --git a/lib/pp.ml b/lib/pp.ml
index 44036ca99..81a19d86d 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -360,7 +360,7 @@ let pp_dirs ?pp_tag ft =
     with reraise ->
       let reraise = Backtrace.add_backtrace reraise in
       let () = Format.pp_print_flush ft () in
-      raise reraise
+      Exninfo.iraise reraise
 
 
 
diff --git a/lib/stateid.mli b/lib/stateid.mli
index 341544a67..2c12c30c3 100644
--- a/lib/stateid.mli
+++ b/lib/stateid.mli
@@ -31,8 +31,8 @@ val of_xml : xml -> t
  * state id that is a valid state id before the error.
  * Backtracking to the valid id is safe.
  * The initial_state_id is assumed to be safe. *)
-val add : exn -> ?valid:t -> t -> exn
-val get : exn -> (t * t) option
+val add : Exninfo.info -> ?valid:t -> t -> Exninfo.info
+val get : Exninfo.info -> (t * t) option
 
 type ('a,'b) request = {
   exn_info : t * t;
diff --git a/lib/system.ml b/lib/system.ml
index 0c4e892b9..1d1968a7c 100644
--- a/lib/system.ml
+++ b/lib/system.ml
@@ -200,7 +200,7 @@ let extern_intern ?(warn=true) magic =
       with reraise ->
 	let reraise = Errors.push reraise in
         let () = try_remove filename in
-        raise reraise
+        iraise reraise
     with Sys_error s -> error ("System error: " ^ s)
   and intern_state paths name =
     try
diff --git a/lib/util.ml b/lib/util.ml
index 531e4fe7d..a8c25f745 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -128,3 +128,7 @@ type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
 let map_union f g = function
   | Inl a -> Inl (f a)
   | Inr b -> Inr (g b)
+
+type iexn = Exninfo.iexn
+
+let iraise = Exninfo.iraise
diff --git a/lib/util.mli b/lib/util.mli
index 86720fe47..66f4c9aff 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -95,6 +95,12 @@ type 'a delayed = unit -> 'a
 
 val delayed_force : 'a delayed -> 'a
 
+(** {6 Enriched exceptions} *)
+
+type iexn = Exninfo.iexn
+
+val iraise : iexn -> 'a
+
 (** {6 Misc. } *)
 
 type ('a, 'b) union = ('a, 'b) CSig.union = Inl of 'a | Inr of 'b
@@ -104,4 +110,3 @@ val map_union : ('a -> 'c) -> ('b -> 'd) -> ('a, 'b) union -> ('c, 'd) union
 
 type 'a until = 'a CSig.until = Stop of 'a | Cont of 'a
 (** Used for browsable-until structures. *)
-