aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib
diff options
context:
space:
mode:
Diffstat (limited to 'lib')
-rw-r--r--lib/backtrace.ml13
-rw-r--r--lib/backtrace.mli6
-rw-r--r--lib/control.ml4
-rw-r--r--lib/errors.ml6
-rw-r--r--lib/errors.mli5
-rw-r--r--lib/exninfo.ml121
-rw-r--r--lib/exninfo.mli25
-rw-r--r--lib/flags.ml8
-rw-r--r--lib/future.ml25
-rw-r--r--lib/future.mli6
-rw-r--r--lib/loc.ml4
-rw-r--r--lib/loc.mli4
-rw-r--r--lib/pp.ml2
-rw-r--r--lib/stateid.mli4
-rw-r--r--lib/system.ml2
-rw-r--r--lib/util.ml4
-rw-r--r--lib/util.mli7
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. *)
-
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 21:20:35 +0000