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, 38 insertions, 83 deletions

diff --git a/lib/exninfo.ml b/lib/exninfo.ml
index 845b8d1909..2eca5f4a71 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