1 (* Title: Pure/Concurrent/bash.ML |
|
2 Author: Makarius |
|
3 |
|
4 GNU bash processes, with propagation of interrupts -- POSIX version. |
|
5 *) |
|
6 |
|
7 signature BASH = |
|
8 sig |
|
9 val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit} |
|
10 end; |
|
11 |
|
12 structure Bash: BASH = |
|
13 struct |
|
14 |
|
15 val process = uninterruptible (fn restore_attributes => fn script => |
|
16 let |
|
17 datatype result = Wait | Signal | Result of int; |
|
18 val result = Synchronized.var "bash_result" Wait; |
|
19 |
|
20 val id = serial_string (); |
|
21 val script_path = File.tmp_path (Path.basic ("bash_script" ^ id)); |
|
22 val out_path = File.tmp_path (Path.basic ("bash_out" ^ id)); |
|
23 val err_path = File.tmp_path (Path.basic ("bash_err" ^ id)); |
|
24 val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id)); |
|
25 |
|
26 fun cleanup_files () = |
|
27 (try File.rm script_path; |
|
28 try File.rm out_path; |
|
29 try File.rm err_path; |
|
30 try File.rm pid_path); |
|
31 val _ = cleanup_files (); |
|
32 |
|
33 val system_thread = |
|
34 Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () => |
|
35 Multithreading.with_attributes Multithreading.private_interrupts (fn _ => |
|
36 let |
|
37 val _ = File.write script_path script; |
|
38 val _ = getenv_strict "ISABELLE_BASH_PROCESS"; |
|
39 val status = |
|
40 OS.Process.system |
|
41 ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ " \"\"" ^ |
|
42 " bash " ^ File.bash_path script_path ^ |
|
43 " > " ^ File.bash_path out_path ^ |
|
44 " 2> " ^ File.bash_path err_path); |
|
45 val res = |
|
46 (case Posix.Process.fromStatus status of |
|
47 Posix.Process.W_EXITED => Result 0 |
|
48 | Posix.Process.W_EXITSTATUS 0wx82 => Signal |
|
49 | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w) |
|
50 | Posix.Process.W_SIGNALED s => |
|
51 if s = Posix.Signal.int then Signal |
|
52 else Result (256 + LargeWord.toInt (Posix.Signal.toWord s)) |
|
53 | Posix.Process.W_STOPPED s => |
|
54 Result (512 + LargeWord.toInt (Posix.Signal.toWord s))); |
|
55 in Synchronized.change result (K res) end |
|
56 handle exn => |
|
57 (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn))); |
|
58 |
|
59 fun read_pid 0 = NONE |
|
60 | read_pid count = |
|
61 (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of |
|
62 NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1)) |
|
63 | some => some); |
|
64 |
|
65 fun terminate NONE = () |
|
66 | terminate (SOME pid) = |
|
67 let |
|
68 fun kill s = |
|
69 (Posix.Process.kill |
|
70 (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true) |
|
71 handle OS.SysErr _ => false; |
|
72 |
|
73 fun multi_kill count s = |
|
74 count = 0 orelse |
|
75 (kill s; kill (Posix.Signal.fromWord 0w0)) andalso |
|
76 (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s); |
|
77 val _ = |
|
78 multi_kill 10 Posix.Signal.int andalso |
|
79 multi_kill 10 Posix.Signal.term andalso |
|
80 multi_kill 10 Posix.Signal.kill; |
|
81 in () end; |
|
82 |
|
83 fun cleanup () = |
|
84 (Standard_Thread.interrupt_unsynchronized system_thread; |
|
85 cleanup_files ()); |
|
86 in |
|
87 let |
|
88 val _ = |
|
89 restore_attributes (fn () => |
|
90 Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) (); |
|
91 |
|
92 val out = the_default "" (try File.read out_path); |
|
93 val err = the_default "" (try File.read err_path); |
|
94 val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc); |
|
95 val pid = read_pid 1; |
|
96 val _ = cleanup (); |
|
97 in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end |
|
98 handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn) |
|
99 end); |
|
100 |
|
101 end; |
|
102 |
|