From 6eb6f55499647b9b5a72626839683f6dff9c1549 Mon Sep 17 00:00:00 2001
From: Lasse Blaauwbroek
Date: Sat, 14 Nov 2020 12:35:21 +0100
Subject: 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.
---
 engine/logic_monad.ml  |  2 +-
 engine/logic_monad.mli |  2 +-
 engine/proofview.ml    | 22 ++++++----------------
 engine/proofview.mli   |  2 +-
 4 files changed, 9 insertions(+), 19 deletions(-)

(limited to 'engine')

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
-- 
cgit v1.2.3