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>