(* Title: Pure/Concurrent/bash.ML
Author: Makarius
GNU bash processes, with propagation of interrupts.
*)
signature BASH =
sig
val process: string -> {out: string, err: string, rc: int, terminate: unit -> unit}
end;
structure Bash: BASH =
struct
val process = uninterruptible (fn restore_attributes => fn script =>
let
datatype result = Wait | Signal | Result of int;
val result = Synchronized.var "bash_result" Wait;
val id = serial_string ();
val script_path = File.tmp_path (Path.basic ("bash_script" ^ id));
val out_path = File.tmp_path (Path.basic ("bash_out" ^ id));
val err_path = File.tmp_path (Path.basic ("bash_err" ^ id));
val pid_path = File.tmp_path (Path.basic ("bash_pid" ^ id));
fun cleanup_files () =
(try File.rm script_path;
try File.rm out_path;
try File.rm err_path;
try File.rm pid_path);
val _ = cleanup_files ();
val system_thread =
Simple_Thread.fork false (fn () =>
Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
let
val _ = File.write script_path script;
val bash_script =
"exec bash " ^
File.shell_path script_path ^
" > " ^ File.shell_path out_path ^
" 2> " ^ File.shell_path err_path;
val _ = getenv_strict "EXEC_PROCESS";
val status =
OS.Process.system
("exec \"$EXEC_PROCESS\" " ^ File.shell_path pid_path ^ " " ^ quote bash_script);
val res =
(case Posix.Process.fromStatus status of
Posix.Process.W_EXITED => Result 0
| Posix.Process.W_EXITSTATUS 0wx82 => Signal
| Posix.Process.W_EXITSTATUS w => Result (Word8.toInt w)
| Posix.Process.W_SIGNALED s =>
if s = Posix.Signal.int then Signal
else Result (256 + LargeWord.toInt (Posix.Signal.toWord s))
| Posix.Process.W_STOPPED s =>
Result (512 + LargeWord.toInt (Posix.Signal.toWord s)));
in Synchronized.change result (K res) end
handle exn =>
(Synchronized.change result (fn Wait => Signal | res => res); reraise exn)));
fun read_pid 0 = NONE
| read_pid count =
(case (Int.fromString (File.read pid_path) handle IO.Io _ => NONE) of
NONE => (OS.Process.sleep (seconds 0.1); read_pid (count - 1))
| some => some);
fun terminate NONE = ()
| terminate (SOME pid) =
let
val sig_test = Posix.Signal.fromWord 0w0;
fun kill_group pid s =
(Posix.Process.kill
(Posix.Process.K_GROUP (Posix.Process.wordToPid (LargeWord.fromInt pid)), s); true)
handle OS.SysErr _ => false;
fun kill s = (kill_group pid s; kill_group pid sig_test);
fun multi_kill count s =
count = 0 orelse
kill s andalso (OS.Process.sleep (seconds 0.1); multi_kill (count - 1) s);
val _ =
multi_kill 10 Posix.Signal.int andalso
multi_kill 10 Posix.Signal.term andalso
multi_kill 10 Posix.Signal.kill;
in () end;
fun cleanup () =
(Simple_Thread.interrupt_unsynchronized system_thread;
cleanup_files ());
in
let
val _ =
restore_attributes (fn () =>
Synchronized.guarded_access result (fn Wait => NONE | x => SOME ((), x))) ();
val out = the_default "" (try File.read out_path);
val err = the_default "" (try File.read err_path);
val rc = (case Synchronized.value result of Signal => Exn.interrupt () | Result rc => rc);
val pid = read_pid 1;
val _ = cleanup ();
in {out = out, err = err, rc = rc, terminate = fn () => terminate pid} end
handle exn => (terminate (read_pid 10); cleanup (); reraise exn)
end);
end;