1/*  Title:      Pure/System/bash.scala
2    Author:     Makarius
3
4GNU bash processes, with propagation of interrupts.
5*/
6
7package isabelle
8
9
10import java.io.{File => JFile, BufferedReader, InputStreamReader,
11  BufferedWriter, OutputStreamWriter}
12
13
14object Bash
15{
16  /* concrete syntax */
17
18  private def bash_chr(c: Byte): String =
19  {
20    val ch = c.toChar
21    ch match {
22      case '\t' => "$'\\t'"
23      case '\n' => "$'\\n'"
24      case '\f' => "$'\\f'"
25      case '\r' => "$'\\r'"
26      case _ =>
27        if (Symbol.is_ascii_letter(ch) || Symbol.is_ascii_digit(ch) || "+,-./:_".contains(ch))
28          Symbol.ascii(ch)
29        else if (c < 0) "$'\\x" + Integer.toHexString(256 + c) + "'"
30        else if (c < 16) "$'\\x0" + Integer.toHexString(c) + "'"
31        else if (c < 32 || c >= 127) "$'\\x" + Integer.toHexString(c) + "'"
32        else  "\\" + ch
33    }
34  }
35
36  def string(s: String): String =
37    if (s == "") "\"\""
38    else UTF8.bytes(s).iterator.map(bash_chr(_)).mkString
39
40  def strings(ss: List[String]): String =
41    ss.iterator.map(Bash.string(_)).mkString(" ")
42
43
44  /* process and result */
45
46  private class Limited_Progress(proc: Process, progress_limit: Option[Long])
47  {
48    private var count = 0L
49    def apply(progress: String => Unit)(line: String): Unit = synchronized {
50      progress(line)
51      count = count + line.length + 1
52      progress_limit match {
53        case Some(limit) if count > limit => proc.terminate
54        case _ =>
55      }
56    }
57  }
58
59  def process(script: String,
60      cwd: JFile = null,
61      env: Map[String, String] = Isabelle_System.settings(),
62      redirect: Boolean = false,
63      cleanup: () => Unit = () => ()): Process =
64    new Process(script, cwd, env, redirect, cleanup)
65
66  class Process private[Bash](
67      script: String,
68      cwd: JFile,
69      env: Map[String, String],
70      redirect: Boolean,
71      cleanup: () => Unit)
72  {
73    private val timing_file = Isabelle_System.tmp_file("bash_timing")
74    private val timing = Synchronized[Option[Timing]](None)
75    def get_timing: Timing = timing.value getOrElse Timing.zero
76
77    private val script_file = Isabelle_System.tmp_file("bash_script")
78    File.write(script_file, script)
79
80    private val proc =
81      Isabelle_System.process(
82        List(File.platform_path(Path.variable("ISABELLE_BASH_PROCESS")), "-",
83          File.standard_path(timing_file), "bash", File.standard_path(script_file)),
84        cwd = cwd, env = env, redirect = redirect)
85
86
87    // channels
88
89    val stdin: BufferedWriter =
90      new BufferedWriter(new OutputStreamWriter(proc.getOutputStream, UTF8.charset))
91
92    val stdout: BufferedReader =
93      new BufferedReader(new InputStreamReader(proc.getInputStream, UTF8.charset))
94
95    val stderr: BufferedReader =
96      new BufferedReader(new InputStreamReader(proc.getErrorStream, UTF8.charset))
97
98
99    // signals
100
101    private val pid = stdout.readLine
102
103    def interrupt()
104    { Exn.Interrupt.postpone { Isabelle_System.kill("INT", pid) } }
105
106    private def kill(signal: String): Boolean =
107      Exn.Interrupt.postpone {
108        Isabelle_System.kill(signal, pid)
109        Isabelle_System.kill("0", pid)._2 == 0 } getOrElse true
110
111    private def multi_kill(signal: String): Boolean =
112    {
113      var running = true
114      var count = 10
115      while (running && count > 0) {
116        if (kill(signal)) {
117          Exn.Interrupt.postpone {
118            Thread.sleep(100)
119            count -= 1
120          }
121        }
122        else running = false
123      }
124      running
125    }
126
127    def terminate()
128    {
129      multi_kill("INT") && multi_kill("TERM") && kill("KILL")
130      proc.destroy
131      do_cleanup()
132    }
133
134
135    // JVM shutdown hook
136
137    private val shutdown_hook = new Thread { override def run = terminate() }
138
139    try { Runtime.getRuntime.addShutdownHook(shutdown_hook) }
140    catch { case _: IllegalStateException => }
141
142
143    // cleanup
144
145    private def do_cleanup()
146    {
147      try { Runtime.getRuntime.removeShutdownHook(shutdown_hook) }
148      catch { case _: IllegalStateException => }
149
150      script_file.delete
151
152      timing.change {
153        case None =>
154          if (timing_file.isFile) {
155            val t =
156              Word.explode(File.read(timing_file)) match {
157                case List(Value.Long(elapsed), Value.Long(cpu)) =>
158                  Timing(Time.ms(elapsed), Time.ms(cpu), Time.zero)
159                case _ => Timing.zero
160              }
161            timing_file.delete
162            Some(t)
163          }
164          else Some(Timing.zero)
165        case some => some
166      }
167
168      cleanup()
169    }
170
171
172    // join
173
174    def join: Int =
175    {
176      val rc = proc.waitFor
177      do_cleanup()
178      rc
179    }
180
181
182    // result
183
184    def result(
185      progress_stdout: String => Unit = (_: String) => (),
186      progress_stderr: String => Unit = (_: String) => (),
187      progress_limit: Option[Long] = None,
188      strict: Boolean = true): Process_Result =
189    {
190      stdin.close
191
192      val limited = new Limited_Progress(this, progress_limit)
193      val out_lines =
194        Future.thread("bash_stdout") { File.read_lines(stdout, limited(progress_stdout)) }
195      val err_lines =
196        Future.thread("bash_stderr") { File.read_lines(stderr, limited(progress_stderr)) }
197
198      val rc =
199        try { join }
200        catch { case Exn.Interrupt() => terminate(); Exn.Interrupt.return_code }
201      if (strict && rc == Exn.Interrupt.return_code) throw Exn.Interrupt()
202
203      Process_Result(rc, out_lines.join, err_lines.join, false, get_timing)
204    }
205  }
206}
207