Merge PR #13377: Fix timeout by ensuring signal exceptions are not erroneously caught

Reviewed-by: ppedrot

3 files changed, 23 insertions, 18 deletions

diff --git a/lib/cErrors.ml b/lib/cErrors.ml
index cb64e36755..760c07783b 100644
--- a/lib/cErrors.ml
+++ b/lib/cErrors.ml
@@ -37,7 +37,7 @@ let user_err ?loc ?info ?hdr strm =
   let info = Option.cata (Loc.add_loc info) info loc in
   Exninfo.iraise (UserError (hdr, strm), info)
 
-exception Timeout
+exception Timeout = Control.Timeout
 
 (** Only anomalies should reach the bottom of the handler stack.
     In usual situation, the [handle_stack] is treated as it if was always
@@ -135,7 +135,7 @@ let _ = register_handler begin function
   | UserError(s, pps) ->
     Some (where s ++ pps)
   | _ -> None
-end
+  end
 
 (** Critical exceptions should not be caught and ignored by mistake
     by inner functions during a [vernacinterp]. They should be handled
@@ -145,7 +145,7 @@ end
 let noncritical = function
   | Sys.Break | Out_of_memory | Stack_overflow
   | Assert_failure _ | Match_failure _ | Anomaly _
-  | Timeout -> false
+  | Control.Timeout -> false
   | Invalid_argument "equal: functional value" -> false
   | _ -> true
 [@@@ocaml.warning "+52"]
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
diff --git a/lib/control.mli b/lib/control.mli
index 25135934bc..9465d8f0d5 100644
--- a/lib/control.mli
+++ b/lib/control.mli
@@ -10,6 +10,9 @@
 
 (** Global control of Coq. *)
 
+(** Used to convert signals to exceptions *)
+exception Timeout
+
 (** Will periodically call [Thread.delay] if set to true *)
 val enable_thread_delay : bool ref
 
@@ -21,13 +24,13 @@ val check_for_interrupt : unit -> unit
 (** Use this function as a potential yield function. If {!interrupt} has been
     set, il will raise [Sys.Break]. *)
 
-val timeout : int -> ('a -> 'b) -> 'a -> exn -> 'b
-(** [timeout n f x e] tries to compute [f x], and if it fails to do so
-    before [n] seconds, it raises [e] instead. *)
+val timeout : int -> ('a -> 'b) -> 'a -> 'b option
+(** [timeout n f x] tries to compute [Some (f x)], and if it fails to do so
+    before [n] seconds, returns [None] instead. *)
 
 (** Set a particular timeout function; warning, this is an internal
    API and it is scheduled to go away. *)
-type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b }
+type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> 'b option }
 val set_timeout : timeout -> unit
 
 (** [protect_sigalrm f x] computes [f x], but if SIGALRM is received during that