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.

9 files changed, 36 insertions, 39 deletions

diff --git a/engine/logic_monad.ml b/engine/logic_monad.ml
index 4c7ed9047d..38ec668884 100644
--- a/engine/logic_monad.ml
+++ b/engine/logic_monad.ml
@@ -99,7 +99,7 @@ struct
   let print_char = fun c -> (); fun () -> print_char c
 
   let timeout = fun n t -> (); fun () ->
-    Control.timeout n t () (Exception Tac_Timeout)
+    Control.timeout n t ()
 
   let make f = (); fun () ->
     try f ()
diff --git a/engine/logic_monad.mli b/engine/logic_monad.mli
index 7df29c6653..7784b38c80 100644
--- a/engine/logic_monad.mli
+++ b/engine/logic_monad.mli
@@ -74,7 +74,7 @@ module NonLogical : sig
 
   (** [try ... with ...] but restricted to {!Exception}. *)
   val catch : 'a t -> (Exninfo.iexn -> 'a t) -> 'a t
-  val timeout : int -> 'a t -> 'a t
+  val timeout : int -> 'a t -> 'a option t
 
   (** Construct a monadified side-effect. Exceptions raised by the argument are
       wrapped with {!Exception}. *)
diff --git a/engine/proofview.ml b/engine/proofview.ml
index 978088872c..22863f451d 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -937,22 +937,12 @@ let tclTIMEOUT n t =
   Proof.get >>= fun initial ->
   Proof.current >>= fun envvar ->
   Proof.lift begin
-    Logic_monad.NonLogical.catch
-      begin
-        let open Logic_monad.NonLogical in
-        timeout n (Proof.repr (Proof.run t envvar initial)) >>= fun r ->
-        match r with
-        | Logic_monad.Nil e -> return (Util.Inr e)
-        | Logic_monad.Cons (r, _) -> return (Util.Inl r)
-      end
-      begin let open Logic_monad.NonLogical in function (e, info) ->
-        match e with
-        | Logic_monad.Tac_Timeout ->
-          return (Util.Inr (Logic_monad.Tac_Timeout, info))
-        | Logic_monad.TacticFailure e ->
-          return (Util.Inr (e, info))
-        | e -> Logic_monad.NonLogical.raise (e, info)
-      end
+    let open Logic_monad.NonLogical in
+    timeout n (Proof.repr (Proof.run t envvar initial)) >>= fun r ->
+    match r with
+    | None -> return (Util.Inr (Logic_monad.Tac_Timeout, Exninfo.null))
+    | Some (Logic_monad.Nil e) -> return (Util.Inr e)
+    | Some (Logic_monad.Cons (r, _)) -> return (Util.Inl r)
   end >>= function
     | Util.Inl (res,s,m,i) ->
         Proof.set s >>
diff --git a/engine/proofview.mli b/engine/proofview.mli
index 816b45984b..fe0d7ae51e 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -417,7 +417,7 @@ end
 val tclCHECKINTERRUPT : unit tactic
 
 (** [tclTIMEOUT n t] can have only one success.
-    In case of timeout if fails with [tclZERO Timeout]. *)
+    In case of timeout it fails with [tclZERO Tac_Timeout]. *)
 val tclTIMEOUT : int -> 'a tactic -> 'a tactic
 
 (** [tclTIME s t] displays time for each atomic call to t, using s as an
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
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 982814fdfc..095ee61835 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1943,7 +1943,7 @@ let w_unify_to_subterm_list env evd flags hdmeta oplist t =
               try (* First try finding a subterm w/o conversion on open terms *)
                 let flags = set_no_delta_open_flags flags in
                 w_unify_to_subterm env evd ~flags t'
-              with e ->
+              with e when CErrors.noncritical e ->
                 (* If this fails, try with full conversion *)
                 w_unify_to_subterm env evd ~flags t'
             else w_unify_to_subterm env evd ~flags t'
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index edf48fef1a..0e77fdd339 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -82,7 +82,9 @@ let vernac_timeout ?timeout (f : 'a -> 'b) (x : 'a) : 'b =
   match !default_timeout, timeout with
   | _, Some n
   | Some n, None ->
-    Control.timeout n f x CErrors.Timeout
+    (match Control.timeout n f x with
+    | None -> Exninfo.iraise (Exninfo.capture CErrors.Timeout)
+    | Some x -> x)
   | None, None ->
     f x