diff options
author | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
---|---|---|
committer | Benjamin Barenblat <bbaren@debian.org> | 2018-12-29 14:31:27 -0500 |
commit | 9043add656177eeac1491a73d2f3ab92bec0013c (patch) | |
tree | 2b0092c84bfbf718eca10c81f60b2640dc8cab05 /clib/exninfo.ml | |
parent | a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 (diff) |
Imported Upstream version 8.8.2upstream/8.8.2
Diffstat (limited to 'clib/exninfo.ml')
-rw-r--r-- | clib/exninfo.ml | 106 |
1 files changed, 106 insertions, 0 deletions
diff --git a/clib/exninfo.ml b/clib/exninfo.ml new file mode 100644 index 00000000..2d130498 --- /dev/null +++ b/clib/exninfo.ml @@ -0,0 +1,106 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(** 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 () + +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 |