lib/control.ml

  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109

(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2019       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)

(*s interruption *)

let interrupt = ref false

let steps = ref 0

let enable_thread_delay = ref false

let check_for_interrupt () =
  if !interrupt then begin interrupt := false; raise Sys.Break end;
  incr steps;
  if !enable_thread_delay && !steps = 1000 then begin
    Thread.delay 0.001;
    steps := 0;
  end

(** This function does not work on windows, sigh... *)
let unix_timeout n f x e =
  let timeout_handler _ = raise e in
  let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
  let _ = Unix.alarm n in
  let restore_timeout () =
    let _ = Unix.alarm 0 in
    Sys.set_signal Sys.sigalrm psh
  in
  try
    let res = f x in
    restore_timeout ();
    res
  with e ->
    let e = Backtrace.add_backtrace e in
    restore_timeout ();
    Exninfo.iraise e

let windows_timeout n f x e =
  let killed = ref false in
  let exited = ref false in
  let thread init =
    while not !killed do
      let cur = Unix.gettimeofday () in
      if float_of_int n <= cur -. init then begin
        interrupt := true;
        exited := true;
        Thread.exit ()
      end;
      Thread.delay 0.5
    done
  in
  let init = Unix.gettimeofday () in
  let _id = CThread.create thread init in
  try
    let res = f x in
    let () = killed := true in
    let cur = Unix.gettimeofday () in
    (* The thread did not interrupt, but the computation took longer than
       expected. *)
    let () = if float_of_int n <= cur -. init then begin
      exited := true;
      raise Sys.Break
    end in
    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
  | e ->
    let () = killed := true in
    let e = Backtrace.add_backtrace e in
    Exninfo.iraise e

type timeout = { timeout : 'a 'b. int -> ('a -> 'b) -> 'a -> exn -> 'b }

let timeout_fun = match Sys.os_type with
| "Unix" | "Cygwin" -> { timeout = unix_timeout }
| _ -> { timeout = windows_timeout }

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 protect_sigalrm f x =
  let timed_out = ref false in
  let timeout_handler _ = timed_out := true in
  try
    let old_handler = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
    try
      let res = f x in
      Sys.set_signal Sys.sigalrm old_handler;
      match !timed_out, old_handler with
      | true, Sys.Signal_handle f -> f Sys.sigalrm; res
      | _, _ -> res
    with e ->
      let e = Backtrace.add_backtrace e in
      Sys.set_signal Sys.sigalrm old_handler;
      Exninfo.iraise e
  with Invalid_argument _ -> (* This happens on Windows, as handling SIGALRM does not seem supported *)
    f x