1(*  Title:      Pure/System/bash.ML
2    Author:     Makarius
3
4GNU bash processes, with propagation of interrupts -- POSIX version.
5*)
6
7signature BASH =
8sig
9  val string: string -> string
10  val strings: string list -> string
11  val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
12end;
13
14if ML_System.platform_is_windows then ML
15\<open>
16structure Bash: BASH =
17struct
18
19val string = Bash_Syntax.string;
20val strings = Bash_Syntax.strings;
21
22val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script =>
23  let
24    datatype result = Wait | Signal | Result of int;
25    val result = Synchronized.var "bash_result" Wait;
26
27    val id = serial_string ();
28    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
29    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
30    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
31    val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
32
33    fun cleanup_files () =
34     (try File.rm script_path;
35      try File.rm out_path;
36      try File.rm err_path;
37      try File.rm pid_path);
38    val _ = cleanup_files ();
39
40    val system_thread =
41      Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
42        Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ =>
43          let
44            val _ = File.write script_path script;
45            val bash_script =
46              "bash " ^ File.bash_path script_path ^
47                " > " ^ File.bash_path out_path ^
48                " 2> " ^ File.bash_path err_path;
49            val bash_process = getenv_strict "ISABELLE_BASH_PROCESS";
50            val rc =
51              Windows.simpleExecute ("",
52                quote (ML_System.platform_path bash_process) ^ " " ^
53                quote (File.platform_path pid_path) ^  " \"\" bash -c " ^ quote bash_script)
54              |> Windows.fromStatus |> SysWord.toInt;
55            val res = if rc = 130 orelse rc = 512 then Signal else Result rc;
56          in Synchronized.change result (K res) end
57          handle exn =>
58            (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
59
60    fun read_pid 0 = NONE
61      | read_pid count =
62          (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
63            NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
64          | some => some);
65
66    fun terminate NONE = ()
67      | terminate (SOME pid) =
68          let
69            fun kill s =
70              let
71                val cmd = getenv_strict "CYGWIN_ROOT" ^ "\\bin\\bash.exe";
72                val arg = "kill -" ^ s ^ " -" ^ string_of_int pid;
73              in
74                OS.Process.isSuccess (Windows.simpleExecute ("", quote cmd ^ " -c " ^ quote arg))
75                  handle OS.SysErr _ => false
76              end;
77
78            fun multi_kill count s =
79              count = 0 orelse
80                (kill s; kill "0") andalso
81                (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
82            val _ =
83              multi_kill 10 "INT" andalso
84              multi_kill 10 "TERM" andalso
85              multi_kill 10 "KILL";
86          in () end;
87
88    fun cleanup () =
89     (Standard_Thread.interrupt_unsynchronized system_thread;
90      cleanup_files ());
91  in
92    let
93      val _ =
94        restore_attributes (fn () =>
95          Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
96
97      val out = the_default "" (try File.read out_path);
98      val err = the_default "" (try File.read err_path);
99      val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
100      val pid = read_pid 1;
101      val _ = cleanup ();
102    in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
103    handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
104  end);
105
106end;
107\<close>
108else ML
109\<open>
110structure Bash: BASH =
111struct
112
113val string = Bash_Syntax.string;
114val strings = Bash_Syntax.strings;
115
116val process = Thread_Attributes.uninterruptible (fn restore_attributes => fn script =>
117  let
118    datatype result = Wait | Signal | Result of int;
119    val result = Synchronized.var "bash_result" Wait;
120
121    val id = serial_string ();
122    val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
123    val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
124    val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
125    val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
126
127    fun cleanup_files () =
128     (try File.rm script_path;
129      try File.rm out_path;
130      try File.rm err_path;
131      try File.rm pid_path);
132    val _ = cleanup_files ();
133
134    val system_thread =
135      Standard_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
136        Thread_Attributes.with_attributes Thread_Attributes.private_interrupts (fn _ =>
137          let
138            val _ = File.write script_path script;
139            val _ = getenv_strict "ISABELLE_BASH_PROCESS";
140            val status =
141              OS.Process.system
142                ("exec \"$ISABELLE_BASH_PROCESS\" " ^ File.bash_path pid_path ^ " \"\"" ^
143                  " bash " ^ File.bash_path script_path ^
144                  " > " ^ File.bash_path out_path ^
145                  " 2> " ^ File.bash_path err_path);
146            val res =
147              (case Posix.Process.fromStatus status of
148                Posix.Process.W_EXITED => Result 0
149              | Posix.Process.W_EXITSTATUS 0wx82 => Signal
150              | Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
151              | Posix.Process.W_SIGNALED s =>
152                  if s = Posix.Signal.int then Signal
153                  else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
154              | Posix.Process.W_STOPPED s =>
155                  Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
156          in Synchronized.change result (K res) end
157          handle exn =>
158            (Synchronized.change result (fn Wait => Signal | res => res); Exn.reraise exn)));
159
160    fun read_pid 0 = NONE
161      | read_pid count =
162          (case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
163            NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
164          | some => some);
165
166    fun terminate NONE = ()
167      | terminate (SOME pid) =
168          let
169            fun kill s =
170              (Posix.Process.kill
171                (Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true)
172              handle OS.SysErr _ => false;
173
174            fun multi_kill count s =
175              count = 0 orelse
176                (kill s; kill (Posix.Signal.fromWord 0w0)) andalso
177                (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
178            val _ =
179              multi_kill 10 Posix.Signal.int andalso
180              multi_kill 10 Posix.Signal.term andalso
181              multi_kill 10 Posix.Signal.kill;
182          in () end;
183
184    fun cleanup () =
185     (Standard_Thread.interrupt_unsynchronized system_thread;
186      cleanup_files ());
187  in
188    let
189      val _ =
190        restore_attributes (fn () =>
191          Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
192
193      val out = the_default "" (try File.read out_path);
194      val err = the_default "" (try File.read err_path);
195      val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
196      val pid = read_pid 1;
197      val _ = cleanup ();
198    in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
199    handle exn => (terminate (read_pid 10); cleanup (); Exn.reraise exn)
200  end);
201
202end;
203\<close>