|
1 (* Title: Pure/Concurrent/bash.ML |
|
2 Author: Makarius |
|
3 |
|
4 GNU bash processes, with propagation of interrupts. |
|
5 *) |
|
6 |
|
7 local |
|
8 |
|
9 fun read_file name = |
|
10 let val is = TextIO.openIn name |
|
11 in Exn.release (Exn.capture TextIO.inputAll is before TextIO.closeIn is) end; |
|
12 |
|
13 fun write_file name txt = |
|
14 let val os = TextIO.openOut name |
|
15 in Exn.release (Exn.capture TextIO.output (os, txt) before TextIO.closeOut os) end; |
|
16 |
|
17 in |
|
18 |
|
19 fun bash_output script = |
|
20 Multithreading.with_attributes Multithreading.no_interrupts (fn orig_atts => |
|
21 let |
|
22 val script_name = OS.FileSys.tmpName (); |
|
23 val _ = write_file script_name script; |
|
24 |
|
25 val pid_name = OS.FileSys.tmpName (); |
|
26 val output_name = OS.FileSys.tmpName (); |
|
27 |
|
28 (*result state*) |
|
29 datatype result = Wait | Signal | Result of int; |
|
30 val result = Unsynchronized.ref Wait; |
|
31 val lock = Mutex.mutex (); |
|
32 val cond = ConditionVar.conditionVar (); |
|
33 fun set_result res = |
|
34 (Mutex.lock lock; result := res; ConditionVar.signal cond; Mutex.unlock lock); |
|
35 |
|
36 val _ = Mutex.lock lock; |
|
37 |
|
38 (*system thread*) |
|
39 val system_thread = Thread.fork (fn () => |
|
40 let |
|
41 val status = |
|
42 OS.Process.system ("exec \"$ISABELLE_HOME/lib/scripts/process\" group " ^ pid_name ^ |
|
43 " script \"exec bash " ^ script_name ^ " > " ^ output_name ^ "\""); |
|
44 val res = |
|
45 (case Posix.Process.fromStatus status of |
|
46 Posix.Process.W_EXITED => Result 0 |
|
47 | Posix.Process.W_EXITSTATUS 0wx82 => Signal |
|
48 | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w) |
|
49 | Posix.Process.W_SIGNALED s => |
|
50 if s = Posix.Signal.int then Signal |
|
51 else Result (256 + LargeWord.toInt (Posix.Signal.toWord s)) |
|
52 | Posix.Process.W_STOPPED s => Result (512 + LargeWord.toInt (Posix.Signal.toWord s))); |
|
53 in set_result res end handle _ (*sic*) => set_result (Result 2), []); |
|
54 |
|
55 (*main thread -- proxy for interrupts*) |
|
56 fun kill n = |
|
57 (case Int.fromString (read_file pid_name) of |
|
58 SOME pid => |
|
59 Posix.Process.kill |
|
60 (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), |
|
61 Posix.Signal.int) |
|
62 | NONE => ()) |
|
63 handle OS.SysErr _ => () | IO.Io _ => |
|
64 (OS.Process.sleep (seconds 0.1); if n > 0 then kill (n - 1) else ()); |
|
65 |
|
66 val _ = |
|
67 while ! result = Wait do |
|
68 let val res = |
|
69 Multithreading.sync_wait (SOME orig_atts) |
|
70 (SOME (Time.+ (Time.now (), seconds 0.1))) cond lock |
|
71 in if Exn.is_interrupt_exn res then kill 10 else () end; |
|
72 |
|
73 (*cleanup*) |
|
74 val output = read_file output_name handle IO.Io _ => ""; |
|
75 val _ = OS.FileSys.remove script_name handle OS.SysErr _ => (); |
|
76 val _ = OS.FileSys.remove pid_name handle OS.SysErr _ => (); |
|
77 val _ = OS.FileSys.remove output_name handle OS.SysErr _ => (); |
|
78 val _ = Thread.interrupt system_thread handle Thread _ => (); |
|
79 val rc = (case ! result of Signal => Exn.interrupt () | Result rc => rc); |
|
80 in (output, rc) end); |
|
81 |
|
82 end; |
|
83 |