(************************************************************************) (* * The Rocq Prover / The Rocq Development Team *) (* v * Copyright INRIA, CNRS and contributors *) (* <O___,, * (see version control and CREDITS file for authors & dates) *) (* \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) listref = 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)
type backtrace = Printexc.raw_backtrace let backtrace_to_string = Printexc.raw_backtrace_to_string
let backtrace_info : backtrace t = make "exninfo_backtrace"
let is_recording = reffalse
let record_backtrace b = let () = Printexc.record_backtrace b in
is_recording := b
let get_backtrace e = get e backtrace_info
let iraise (e,i) =
CThread.with_lock lock ~scope:(fun () -> let id = Thread.id (Thread.self ()) in
current := (id, (e,i)) :: remove_assoc id !current); match get i backtrace_info with
| None -> raise e
| Some bt ->
Printexc.raise_with_backtrace e bt
let find_and_remove () =
CThread.with_lock lock ~scope:(fun () -> let id = Thread.id (Thread.self ()) in let (v, l) = find_and_remove_assoc id !current in let () = current := l 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
let capture e = if !is_recording then (* This must be the first function call, otherwise the stack may be
destroyed *) let bt = Printexc.get_raw_backtrace () in let info = info e in
e, add info backtrace_info bt else
e, info e
let reify () = if !is_recording then let bt = Printexc.get_callstack 50 in
add null backtrace_info bt else
null
¤ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
