Fix timeout by ensuring signal exceptions are not erroneously caught

Fixes #7430 and fixes #10968

This commit makes the following changes:
- Add an exception `Signal` used to convert OCaml signals to exceptions.
`Signal` is registered as critical in `CErrors` to avoid being caught in the
wrong `with` clauses.
- Make `Control.timeout` into a safer interface based on `option` instead of
exceptions.
- Modify `tclTIMEOUT` to fail with `CErrors.Timeout` instead of
`Logic_monad.Tac_timeout`, as was already advertised in the ocamldoc documentation.
- Removes `Logic_monad.Tac_timeout` altogether because it no longer has a use.

1 files changed, 13 insertions, 11 deletions

diff --git a/lib/control.ml b/lib/control.ml
index 95ea3935a7..7da95ff3dd 100644
--- a/lib/control.ml
+++ b/lib/control.ml
@@ -16,6 +16,8 @@ let steps = ref 0
 
 let enable_thread_delay = ref false
 
+exception Timeout
+
 let check_for_interrupt () =
   if !interrupt then begin interrupt := false; raise Sys.Break end;
   if !enable_thread_delay then begin
@@ -27,8 +29,8 @@ let check_for_interrupt () =
   end
 
 (** This function does not work on windows, sigh... *)
-let unix_timeout n f x e =
-  let timeout_handler _ = raise e in
+let unix_timeout n f x =
+  let timeout_handler _ = raise Timeout in
   let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
   let _ = Unix.alarm n in
   let restore_timeout () =
@@ -38,13 +40,13 @@ let unix_timeout n f x e =
   try
     let res = f x in
     restore_timeout ();
-    res
-  with e ->
-    let e = Exninfo.capture e in
+    Some res
+  with Timeout ->
     restore_timeout ();
-    Exninfo.iraise e
+    None
+
 
-let windows_timeout n f x e =
+let windows_timeout n f x =
   let killed = ref false in
   let exited = ref false in
   let thread init =
@@ -70,18 +72,18 @@ let windows_timeout n f x e =
       exited := true;
       raise Sys.Break
     end in
-    res
+    Some res
   with
   | Sys.Break ->
     (* Just in case, it could be a regular Ctrl+C *)
     if not !exited then begin killed := true; raise Sys.Break end
-    else raise e
+    else None
   | e ->
     let e = Exninfo.capture e in
     let () = killed := true in
     Exninfo.iraise e
 
-type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b }
+type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> 'b option }
 
 let timeout_fun = match Sys.os_type with
 | "Unix" | "Cygwin" -> { timeout = unix_timeout }
@@ -90,7 +92,7 @@ let timeout_fun = match Sys.os_type with
 let timeout_fun_ref = ref timeout_fun
 let set_timeout f = timeout_fun_ref := f
 
-let timeout n f e = !timeout_fun_ref.timeout n f e
+let timeout n f = !timeout_fun_ref.timeout n f
 
 let protect_sigalrm f x =
   let timed_out = ref false in