|
1 /* |
|
2 * $Id$ |
|
3 * |
|
4 * Posix process wrapper for Isabelle (see also src/Pure/Tools/isabelle_process.ML). |
|
5 * |
|
6 * The process model: |
|
7 * |
|
8 * (1) input |
|
9 * - stdin stream |
|
10 * - signals (interrupt, kill) |
|
11 * |
|
12 * (2) output/results |
|
13 * - stdout stream, interspersed with marked Isabelle messages |
|
14 * - stderr stream |
|
15 * - process exit (return code) |
|
16 * |
|
17 * I/O is fully asynchronous, with unrestricted buffers. Text is encoded as UTF-8. |
|
18 */ |
|
19 |
|
20 package isabelle; |
|
21 |
|
22 import java.io.*; |
|
23 import java.util.Locale; |
|
24 import java.util.concurrent.LinkedBlockingQueue; |
|
25 |
|
26 public class IsabelleProcess { |
|
27 private volatile Process proc = null; |
|
28 private volatile String pid = null; |
|
29 private volatile boolean closing = false; |
|
30 private LinkedBlockingQueue<String> output = null; |
|
31 |
|
32 |
|
33 /* exceptions */ |
|
34 |
|
35 public static class IsabelleProcessException extends Exception { |
|
36 public IsabelleProcessException() { |
|
37 super(); |
|
38 } |
|
39 public IsabelleProcessException(String msg) { |
|
40 super(msg); |
|
41 } |
|
42 }; |
|
43 |
|
44 |
|
45 /* results from the process */ |
|
46 |
|
47 public static class Result { |
|
48 public enum Kind { |
|
49 STDIN, STDOUT, STDERR, SIGNAL, EXIT, // Posix channels/events |
|
50 WRITELN, PRIORITY, TRACING, WARNING, ERROR, DEBUG, // Isabelle messages |
|
51 SYSTEM // internal system notification |
|
52 }; |
|
53 public Kind kind; |
|
54 public String result; |
|
55 |
|
56 public Result(Kind kind, String result) { |
|
57 this.kind = kind; |
|
58 this.result = result; |
|
59 } |
|
60 |
|
61 public String toString() { |
|
62 return this.kind.toString() + " [[" + this.result + "]]"; |
|
63 } |
|
64 } |
|
65 |
|
66 public LinkedBlockingQueue<Result> results; |
|
67 |
|
68 private synchronized void putResult(Result.Kind kind, String result) { |
|
69 try { |
|
70 results.put(new Result(kind, result)); |
|
71 } catch (InterruptedException exn) { } |
|
72 } |
|
73 |
|
74 |
|
75 /* interrupt process */ |
|
76 |
|
77 public synchronized void interrupt() throws IsabelleProcessException |
|
78 { |
|
79 if (proc != null && pid != null) { |
|
80 try { |
|
81 putResult(Result.Kind.SIGNAL, "INT"); |
|
82 int rc = Runtime.getRuntime().exec("kill -INT " + pid).waitFor(); |
|
83 if (rc != 0) { |
|
84 throw new IsabelleProcessException("Cannot interrupt: kill command failed"); |
|
85 } |
|
86 } catch (IOException exn) { |
|
87 throw new IsabelleProcessException(exn.getMessage()); |
|
88 } catch (InterruptedException exn) { |
|
89 throw new IsabelleProcessException("Cannot interrupt: aborted"); |
|
90 } |
|
91 } else { |
|
92 throw new IsabelleProcessException("Cannot interrupt: no process"); |
|
93 } |
|
94 } |
|
95 |
|
96 |
|
97 /* kill process */ |
|
98 |
|
99 public synchronized void kill() throws IsabelleProcessException |
|
100 { |
|
101 if (proc != null) { |
|
102 tryClose(); |
|
103 try { |
|
104 Thread.sleep(300); |
|
105 } catch (InterruptedException exn) { } |
|
106 putResult(Result.Kind.SIGNAL, "KILL"); |
|
107 proc.destroy(); |
|
108 proc = null; |
|
109 } else { |
|
110 throw new IsabelleProcessException("Cannot kill: no process"); |
|
111 } |
|
112 } |
|
113 |
|
114 |
|
115 /* encode text as string token */ |
|
116 |
|
117 public static String encodeString(String str) { |
|
118 Locale locale = null; |
|
119 StringBuffer buf = new StringBuffer(100); |
|
120 int i; |
|
121 char c; |
|
122 |
|
123 buf.append("\""); |
|
124 for (i = 0; i < str.length(); i++) { |
|
125 c = str.charAt(i); |
|
126 if (c < 32 || c == '\\' || c == '\"') { |
|
127 buf.append(String.format(locale, "\\%03d", (int) c)); |
|
128 } else { |
|
129 buf.append(c); |
|
130 } |
|
131 } |
|
132 buf.append("\""); |
|
133 return buf.toString(); |
|
134 } |
|
135 |
|
136 |
|
137 /* output being piped into the process (stdin) */ |
|
138 |
|
139 private volatile BufferedWriter outputWriter; |
|
140 private class OutputThread extends Thread |
|
141 { |
|
142 public void run() |
|
143 { |
|
144 while (outputWriter != null) { |
|
145 try { |
|
146 String s = output.take(); |
|
147 if (s.equals("\u0000")) { |
|
148 outputWriter.close(); |
|
149 outputWriter = null; |
|
150 } else { |
|
151 putResult(Result.Kind.STDIN, s); |
|
152 outputWriter.write(s); |
|
153 outputWriter.flush(); |
|
154 } |
|
155 } catch (InterruptedException exn) { |
|
156 putResult(Result.Kind.SYSTEM, "Output thread interrupted"); |
|
157 } catch (IOException exn) { |
|
158 putResult(Result.Kind.SYSTEM, exn.getMessage()); |
|
159 } |
|
160 } |
|
161 putResult(Result.Kind.SYSTEM, "Output thread terminated"); |
|
162 } |
|
163 } |
|
164 private OutputThread outputThread; |
|
165 |
|
166 |
|
167 // public operations |
|
168 |
|
169 public synchronized void output(String text) throws IsabelleProcessException |
|
170 { |
|
171 if (proc != null && !closing) { |
|
172 try { |
|
173 output.put(text); |
|
174 } catch (InterruptedException ex) { |
|
175 throw new IsabelleProcessException("Cannot output: aborted"); |
|
176 } |
|
177 } else if (proc == null) { |
|
178 throw new IsabelleProcessException("Cannot output: no process"); |
|
179 } else { |
|
180 throw new IsabelleProcessException("Cannot output: already closing"); |
|
181 } |
|
182 } |
|
183 |
|
184 public synchronized void close() throws IsabelleProcessException |
|
185 { |
|
186 output("\u0000"); |
|
187 closing = true; |
|
188 // FIXME watchdog/timeout |
|
189 } |
|
190 |
|
191 public synchronized void tryClose() |
|
192 { |
|
193 if (proc != null && !closing) { |
|
194 try { |
|
195 close(); |
|
196 } catch (IsabelleProcessException ex) { } |
|
197 } |
|
198 } |
|
199 |
|
200 private synchronized void outputSync(String text) throws IsabelleProcessException |
|
201 { |
|
202 output(" \\<^sync>\n; " + text + " \\<^sync>;\n"); |
|
203 } |
|
204 |
|
205 public synchronized void command(String text) throws IsabelleProcessException |
|
206 { |
|
207 outputSync("Isabelle.command " + encodeString(text)); |
|
208 } |
|
209 |
|
210 public synchronized void ML(String text) throws IsabelleProcessException |
|
211 { |
|
212 outputSync("ML " + encodeString(text)); |
|
213 } |
|
214 |
|
215 |
|
216 /* input from the process (stdout/stderr) */ |
|
217 |
|
218 private volatile BufferedReader inputReader; |
|
219 private class InputThread extends Thread |
|
220 { |
|
221 public void run() |
|
222 { |
|
223 Result.Kind kind = Result.Kind.STDOUT; |
|
224 StringBuffer buf = new StringBuffer(100); |
|
225 |
|
226 try { |
|
227 while (inputReader != null) { |
|
228 if (kind == Result.Kind.STDOUT && pid != null) { |
|
229 // char mode |
|
230 int c = -1; |
|
231 while ((buf.length() == 0 || inputReader.ready()) && |
|
232 (c = inputReader.read()) > 0 && c != 2) { |
|
233 buf.append((char) c); |
|
234 } |
|
235 if (buf.length() > 0) { |
|
236 putResult(kind, buf.toString()); |
|
237 buf = new StringBuffer(100); |
|
238 } |
|
239 if (c == 2) { |
|
240 c = inputReader.read(); |
|
241 switch (c) { |
|
242 case 'A': kind = Result.Kind.WRITELN; break; |
|
243 case 'B': kind = Result.Kind.PRIORITY; break; |
|
244 case 'C': kind = Result.Kind.TRACING; break; |
|
245 case 'D': kind = Result.Kind.WARNING; break; |
|
246 case 'E': kind = Result.Kind.ERROR; break; |
|
247 case 'F': kind = Result.Kind.DEBUG; break; |
|
248 default: kind = Result.Kind.STDOUT; break; |
|
249 } |
|
250 } |
|
251 if (c == -1) { |
|
252 inputReader.close(); |
|
253 inputReader = null; |
|
254 tryClose(); |
|
255 } |
|
256 } else { |
|
257 // line mode |
|
258 String line = null; |
|
259 if ((line = inputReader.readLine()) != null) { |
|
260 if (pid == null && kind == Result.Kind.STDOUT && line.startsWith("PID=")) { |
|
261 pid = line.substring("PID=".length()); |
|
262 } else if (kind == Result.Kind.STDOUT) { |
|
263 buf.append(line); |
|
264 buf.append("\n"); |
|
265 putResult(kind, buf.toString()); |
|
266 buf = new StringBuffer(100); |
|
267 } else { |
|
268 int len = line.length(); |
|
269 if (len >= 2 && line.charAt(len - 2) == 2 && line.charAt(len - 1) == '.') { |
|
270 buf.append(line.substring(0, len - 2)); |
|
271 putResult(kind, buf.toString()); |
|
272 buf = new StringBuffer(100); |
|
273 kind = Result.Kind.STDOUT; |
|
274 } else { |
|
275 buf.append(line); |
|
276 buf.append("\n"); |
|
277 } |
|
278 } |
|
279 } else { |
|
280 inputReader.close(); |
|
281 inputReader = null; |
|
282 tryClose(); |
|
283 } |
|
284 } |
|
285 } |
|
286 } catch (IOException exn) { |
|
287 putResult(Result.Kind.SYSTEM, exn.getMessage()); |
|
288 } |
|
289 putResult(Result.Kind.SYSTEM, "Input thread terminated"); |
|
290 } |
|
291 } |
|
292 private InputThread inputThread; |
|
293 |
|
294 private volatile BufferedReader errorReader; |
|
295 private class ErrorThread extends Thread |
|
296 { |
|
297 public void run() |
|
298 { |
|
299 try { |
|
300 while (errorReader != null) { |
|
301 StringBuffer buf = new StringBuffer(100); |
|
302 int c; |
|
303 while ((buf.length() == 0 || errorReader.ready()) && (c = errorReader.read()) > 0) { |
|
304 buf.append((char) c); |
|
305 } |
|
306 if (buf.length() > 0) { |
|
307 putResult(Result.Kind.STDERR, buf.toString()); |
|
308 } else { |
|
309 errorReader.close(); |
|
310 errorReader = null; |
|
311 tryClose(); |
|
312 } |
|
313 } |
|
314 } catch (IOException exn) { |
|
315 putResult(Result.Kind.SYSTEM, exn.getMessage()); |
|
316 } |
|
317 putResult(Result.Kind.SYSTEM, "Error thread terminated"); |
|
318 } |
|
319 } |
|
320 private ErrorThread errorThread; |
|
321 |
|
322 |
|
323 /* exit thread */ |
|
324 |
|
325 private class ExitThread extends Thread |
|
326 { |
|
327 public void run() |
|
328 { |
|
329 try { |
|
330 int rc = proc.waitFor(); |
|
331 putResult(Result.Kind.EXIT, Integer.toString(rc)); |
|
332 proc = null; |
|
333 } catch (InterruptedException exn) { |
|
334 putResult(Result.Kind.SYSTEM, "Exit thread interrupted"); |
|
335 } |
|
336 putResult(Result.Kind.SYSTEM, "Exit thread terminated"); |
|
337 } |
|
338 } |
|
339 private ExitThread exitThread; |
|
340 |
|
341 |
|
342 /* create process */ |
|
343 |
|
344 public IsabelleProcess(String logic) throws IsabelleProcessException |
|
345 { |
|
346 String [] cmdline = {"bash", "isabelle-process", "-W", logic}; |
|
347 String charset = "UTF-8"; |
|
348 try { |
|
349 proc = Runtime.getRuntime().exec(cmdline); |
|
350 } catch (IOException exn) { |
|
351 throw new IsabelleProcessException(exn.getMessage()); |
|
352 } |
|
353 |
|
354 try { |
|
355 outputWriter = new BufferedWriter(new OutputStreamWriter(proc.getOutputStream(), charset)); |
|
356 inputReader = new BufferedReader(new InputStreamReader(proc.getInputStream(), charset)); |
|
357 errorReader = new BufferedReader(new InputStreamReader(proc.getErrorStream(), charset)); |
|
358 } catch (UnsupportedEncodingException exn) { |
|
359 proc.destroy(); |
|
360 throw new Error(exn.getMessage()); |
|
361 } |
|
362 |
|
363 output = new LinkedBlockingQueue<String>(); |
|
364 outputThread = new OutputThread(); |
|
365 |
|
366 results = new LinkedBlockingQueue<Result>(); |
|
367 inputThread = new InputThread(); |
|
368 errorThread = new ErrorThread(); |
|
369 exitThread = new ExitThread(); |
|
370 |
|
371 outputThread.start(); |
|
372 inputThread.start(); |
|
373 errorThread.start(); |
|
374 exitThread.start(); |
|
375 } |
|
376 } |