diff options
| -rw-r--r-- | Makefile.build | 28 | ||||
| -rw-r--r-- | lib/exninfo.ml | 61 |
2 files changed, 69 insertions, 20 deletions
diff --git a/Makefile.build b/Makefile.build index 52f67dc8e..3aa681bfd 100644 --- a/Makefile.build +++ b/Makefile.build @@ -92,7 +92,7 @@ SHOW := $(if $(VERBOSE),@true "",@echo "") HIDE := $(if $(VERBOSE),,@) LOCALINCLUDES=$(addprefix -I , $(SRCDIRS) ) -MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) +MLINCLUDES=$(LOCALINCLUDES) -I $(MYCAMLP4LIB) -thread OCAMLC := $(OCAMLC) $(CAMLFLAGS) OCAMLOPT := $(OCAMLOPT) $(CAMLFLAGS) @@ -124,11 +124,13 @@ else CAMLP4USE=-D$(CAMLVERSION) endif +CAMLP4FLAGS=-I $(CAMLLIB) -I $(CAMLLIB)/threads -I $(MYCAMLP4LIB) unix.cma threads.cma + PR_O := $(if $(READABLE_ML4),pr_o.cmo,pr_dump.cmo) # works also with new camlp4 -SYSMOD:=str unix dynlink -SYSCMA:=$(addsuffix .cma,$(SYSMOD) threads) -SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD) threads) +SYSMOD:=str unix dynlink threads +SYSCMA:=$(addsuffix .cma,$(SYSMOD)) +SYSCMXA:=$(addsuffix .cmxa,$(SYSMOD)) ifeq ($(CAMLP4),camlp5) P4CMA:=gramlib.cma @@ -320,7 +322,7 @@ coqide-files: $(IDEFILES) ifeq ($(HASCOQIDE),opt) $(COQIDE): $(LINKIDEOPT) $(SHOW)'OCAMLOPT -o $@' - $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa lablgtk.cmxa \ + $(HIDE)$(OCAMLOPT) $(COQIDEFLAGS) $(OPTFLAGS) -o $@ unix.cmxa threads.cmxa lablgtk.cmxa \ lablgtksourceview2.cmxa str.cmxa $(IDEFLAGS:.cma=.cmxa) $^ $(STRIP) $@ else @@ -330,7 +332,7 @@ endif $(COQIDEBYTE): $(LINKIDE) $(SHOW)'OCAMLC -o $@' - $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma lablgtk.cma \ + $(HIDE)$(OCAMLC) $(COQIDEFLAGS) $(BYTEFLAGS) -o $@ unix.cma threads.cma lablgtk.cma \ lablgtksourceview2.cma str.cma $(IDEFLAGS) $(IDECDEPSFLAGS) $^ # install targets @@ -619,7 +621,7 @@ $(GALLINA): $(addsuffix $(BESTOBJ), tools/gallina_lexer tools/gallina) $(COQMAKEFILE): $(patsubst %.cma,%$(BESTLIB),$(COQMAKEFILECMO:.cmo=$(BESTOBJ))) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,,str unix) + $(HIDE)$(call bestocaml,,str unix threads) $(COQTEX): tools/coq_tex$(BESTOBJ) $(SHOW)'OCAMLBEST -o $@' @@ -643,7 +645,7 @@ $(COQWORKMGR): $(addsuffix $(BESTOBJ), stm/coqworkmgrApi tools/coqworkmgr) \ $(FAKEIDE): lib/clib$(BESTLIB) lib/xml_lexer$(BESTOBJ) lib/xml_parser$(BESTOBJ) lib/xml_printer$(BESTOBJ) lib/errors$(BESTOBJ) lib/spawn$(BESTOBJ) ide/document$(BESTOBJ) ide/xmlprotocol$(BESTOBJ) tools/fake_ide$(BESTOBJ) | $(IDETOPLOOPCMA:.cma=$(BESTDYN)) $(SHOW)'OCAMLBEST -o $@' - $(HIDE)$(call bestocaml,-I ide,str unix) + $(HIDE)$(call bestocaml,-I ide,str unix threads) # votour: a small vo explorer (based on the checker) @@ -655,9 +657,9 @@ bin/votour: lib/cObj$(BESTOBJ) checker/values$(BESTOBJ) checker/votour.ml ifeq ($(CAMLP4),camlp4) tools/compat5.cmo: tools/compat5.mlp - $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -I $(MYCAMLP4LIB) -impl' -impl $< + $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $< tools/compat5b.cmo: tools/compat5b.mlp - $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) -I $(MYCAMLP4LIB) -impl' -impl $< + $(OCAMLC) -c -I $(MYCAMLP4LIB) -pp '$(CAMLP4O) $(CAMLP4FLAGS) -impl' -impl $< else tools/compat5.cmo: tools/compat5.ml $(OCAMLC) -c $< @@ -876,7 +878,7 @@ dev/printers.cma: | dev/printers.mllib.d grammar/grammar.cma: | grammar/grammar.mllib.d $(SHOW)'Testing $@' @touch test.ml4 - $(HIDE)$(CAMLP4O) -I $(CAMLLIB) -I $(MYCAMLP4LIB) $^ -impl test.ml4 -o test.ml + $(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $^ -impl test.ml4 -o test.ml $(HIDE)$(OCAMLC) $(MLINCLUDES) $(BYTEFLAGS) test.ml -o test-grammar @rm -f test-grammar test.* $(SHOW)'OCAMLC -a $@' @@ -884,7 +886,7 @@ grammar/grammar.cma: | grammar/grammar.mllib.d ide/coqide_main.ml: ide/coqide_main.ml4 config/Makefile # no camlp4deps here $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@ + $(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) $(CAMLP4USE) -D$(IDEINT) -impl $< -o $@ # pretty printing of the revision number when compiling a checked out # source tree @@ -1022,7 +1024,7 @@ plugins/%_mod.ml: plugins/%.mllib %.ml: %.ml4 | %.ml4.d tools/compat5.cmo tools/compat5b.cmo $(SHOW)'CAMLP4O $<' - $(HIDE)$(CAMLP4O) -I $(MYCAMLP4LIB) $(PR_O) -I $(CAMLLIB) tools/compat5.cmo \ + $(HIDE)$(CAMLP4O) $(CAMLP4FLAGS) $(PR_O) tools/compat5.cmo \ $(call CAMLP4DEPS,$<) $(CAMLP4USE) $(CAMLP4COMPAT) -impl $< -o $@ %.vo %.glob: %.v theories/Init/Prelude.vo $(VO_TOOLS_DEP) | %.v.d diff --git a/lib/exninfo.ml b/lib/exninfo.ml index 2eca5f4a7..d049dc6cf 100644 --- a/lib/exninfo.ml +++ b/lib/exninfo.ml @@ -27,18 +27,65 @@ exception Unique let dummy = (Unique, Store.empty) -let current = ref dummy +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 () = current := e in + 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 -> raise e -| Some i -> current := (e, i); raise e +| 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) = !current in + 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 @@ -50,8 +97,8 @@ let info e = 3. The same exception is raised through the standard raise, accessing the wrong data. . *) - let () = current := dummy in data else - let () = current := dummy in + (** Mismatch: the raised exception is not the one stored, either because the + previous raise was not instrumented, or because something went wrong. *) Store.empty |