1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
|
(***********************************************************************)
(* v * The Coq Proof Assistant / The Coq Development Team *)
(* <O___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
(* \VV/ *************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(***********************************************************************)
(** Enriched exceptions have an additional field at the end of their usual data
containing a pair composed of the distinguishing [token] and the backtrace
information. We discriminate the token by pointer equality. *)
module Store = Store.Make(struct end)
type 'a t = 'a Store.field
type info = Store.t
type iexn = exn * info
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 : (int * iexn) list ref = ref []
(** List associating to each thread id the latest exception raised by an
instrumented raise (i.e. {!raise} from this module). It is shared between
threads, so we must take care of this when modifying it.
Invariants: all index keys are unique in the list.
*)
let lock = Mutex.create ()
let rec remove_assoc (i : int) = function
| [] -> []
| (j, v) :: rem as l ->
if i = j then rem
else
let ans = remove_assoc i rem in
if rem == ans then l
else (j, v) :: ans
let rec find_and_remove_assoc (i : int) = function
| [] -> dummy, []
| (j, v) :: rem as l ->
if i = j then (v, rem)
else
let (r, ans) = find_and_remove_assoc i rem in
if rem == ans then (r, l)
else (r, (j, v) :: ans)
let iraise e =
let () = Mutex.lock lock in
let id = Thread.id (Thread.self ()) in
let () = current := (id, e) :: remove_assoc id !current in
let () = Mutex.unlock lock in
raise (fst e)
let raise ?info e = match info with
| None ->
let () = Mutex.lock lock in
let id = Thread.id (Thread.self ()) in
let () = current := remove_assoc id !current in
let () = Mutex.unlock lock in
raise e
| Some i ->
let () = Mutex.lock lock in
let id = Thread.id (Thread.self ()) in
let () = current := (id, (e, i)) :: remove_assoc id !current in
let () = Mutex.unlock lock in
raise e
let find_and_remove () =
let () = Mutex.lock lock in
let id = Thread.id (Thread.self ()) in
let (v, l) = find_and_remove_assoc id !current in
let () = current := l in
let () = Mutex.unlock lock in
v
let info e =
let (src, data) = find_and_remove () 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.
. *)
data
else
(** Mismatch: the raised exception is not the one stored, either because the
previous raise was not instrumented, or because something went wrong. *)
Store.empty
|
