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
110
111
112
113
114
115
116
117
118
119
120
121
122
123
let interrupt = ref false
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
incr steps;
if !steps = 1000 then begin
Thread.delay 0.001;
steps := 0;
end
end
(** This function does not work on windows, sigh... *)
let unix_timeout n f x =
let open Unix in
let timeout_handler _ = raise Timeout in
let old_timer = getitimer ITIMER_REAL in
if old_timer.it_value > 0. && old_timer.it_value <= n then Ok (f x) else
let psh = Sys.signal Sys.sigalrm (Sys.Signal_handle timeout_handler) in
let restore_timeout () =
let timer_status = getitimer ITIMER_REAL in
let old_timer_value = old_timer.it_value -. n +. timer_status.it_value in
let old_timer_value = if old_timer.it_value <= 0. then 0. else
(if old_timer_value <= 0. then epsilon_float else old_timer_value) in
let _ = setitimer ITIMER_REAL { old_timer with it_value = old_timer_value } in
Sys.set_signal Sys.sigalrm psh
in
let open Memprof_coq.Resource_bind in
let& () = Memprof_coq.Masking.with_resource ~acquire:(fun () -> ()) () ~release:restore_timeout in
let _ = setitimer ITIMER_REAL {it_interval = 0.; it_value = n} in
try Ok (f x)
with Timeout as exn ->
let _, info = Exninfo.capture exn in
Error info
let windows_timeout n f x =
let killed = ref false in
let exited = ref false in
let thread init =
while not !killed do
let cur = Unix.gettimeofday () in
if n <= cur -. init then begin
interrupt := true;
exited := true;
Thread.exit () [@ocaml.warning "-3"]
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
let () = if n <= cur -. init then begin
exited := true;
raise Sys.Break
end in
Ok res
with
| Sys.Break ->
let _, info as e = Exninfo.capture Sys.Break in
if not !exited then begin killed := true; Exninfo.iraise e end
else Error info
| e ->
let e = Exninfo.capture e in
let () = killed := true in
Exninfo.iraise e
type timeout = { timeout : 'a 'b. float -> ('a -> 'b) -> 'a -> ('b, Exninfo.info) result }
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 = !timeout_fun_ref.timeout n f
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 = Exninfo.capture e in
Sys.set_signal Sys.sigalrm old_handler;
Exninfo.iraise e
with Invalid_argument _ ->
f x