1 /* |
|
2 * $Id$ |
|
3 */ |
|
4 |
|
5 package isabelle; |
|
6 |
|
7 import java.io.*; |
|
8 import java.util.Locale; |
|
9 import java.util.ArrayList; |
|
10 import java.util.Properties; |
|
11 import java.util.Enumeration; |
|
12 import java.util.concurrent.LinkedBlockingQueue; |
|
13 |
|
14 /** |
|
15 * Posix process wrapper for Isabelle (see also <code>src/Pure/Tools/isabelle_process.ML</code>). |
|
16 * <p> |
|
17 * |
|
18 * The process model: |
|
19 * <p> |
|
20 * |
|
21 * <ol> |
|
22 * <li> input |
|
23 * <ul> |
|
24 * <li> stdin stream |
|
25 * <li> signals (interrupt, kill) |
|
26 * </ul> |
|
27 * |
|
28 * <li> output/results |
|
29 * <ul> |
|
30 * <li> stdout stream, interspersed with marked Isabelle messages |
|
31 * <li> stderr stream |
|
32 * <li> process init (pid and session property) |
|
33 * <li> process exit (return code) |
|
34 * </ul> |
|
35 * </ol> |
|
36 * |
|
37 * I/O is fully asynchronous, with unrestricted buffers. Text is encoded as UTF-8. |
|
38 * <p> |
|
39 * |
|
40 * System properties: |
|
41 * <p> |
|
42 * |
|
43 * <dl> |
|
44 * <dt> <code>isabelle.home</code> <di> <code>ISABELLE_HOME</code> of Isabelle installation |
|
45 * (default determined from isabelle-process via <code>PATH</code>) |
|
46 * <dt> <code>isabelle.shell</code> <di> optional shell command for <code>isabelle-process</code> (also requires isabelle.home) |
|
47 * <dt> <code>isabelle.kill</code> <di> optional kill command (default <code>kill</code>) |
|
48 */ |
|
49 |
|
50 public class IsabelleProcess { |
|
51 private volatile Process proc = null; |
|
52 private volatile String pid = null; |
|
53 private volatile boolean closing = false; |
|
54 private LinkedBlockingQueue<String> output = null; |
|
55 |
|
56 public volatile String session = null; |
|
57 |
|
58 |
|
59 /** |
|
60 * Models failures in process management. |
|
61 */ |
|
62 public static class IsabelleProcessException extends Exception { |
|
63 public IsabelleProcessException() { |
|
64 super(); |
|
65 } |
|
66 public IsabelleProcessException(String msg) { |
|
67 super(msg); |
|
68 } |
|
69 }; |
|
70 |
|
71 |
|
72 /** |
|
73 * Models cooked results from the process. |
|
74 */ |
|
75 public static class Result { |
|
76 public enum Kind { |
|
77 // Posix channels/events |
|
78 STDIN, STDOUT, STDERR, SIGNAL, EXIT, |
|
79 // Isabelle messages |
|
80 WRITELN, PRIORITY, TRACING, WARNING, ERROR, DEBUG, PROMPT, INIT, STATUS, |
|
81 // internal system notification |
|
82 SYSTEM |
|
83 }; |
|
84 public Kind kind; |
|
85 public Properties props; |
|
86 public String result; |
|
87 |
|
88 public Result(Kind kind, Properties props, String result) { |
|
89 this.kind = kind; |
|
90 this.props = props; |
|
91 this.result = result; |
|
92 } |
|
93 |
|
94 public boolean isRaw() { |
|
95 return |
|
96 this.kind == Kind.STDOUT || |
|
97 this.kind == Kind.STDERR; |
|
98 } |
|
99 |
|
100 public boolean isSystem() { |
|
101 return |
|
102 this.kind == Kind.STDIN || |
|
103 this.kind == Kind.SIGNAL || |
|
104 this.kind == Kind.EXIT || |
|
105 this.kind == Kind.PROMPT || |
|
106 this.kind == Kind.STATUS || |
|
107 this.kind == Kind.SYSTEM; |
|
108 } |
|
109 |
|
110 @Override |
|
111 public String toString() { |
|
112 if (this.props == null) { |
|
113 return this.kind.toString() + " [[" + this.result + "]]"; |
|
114 } else { |
|
115 return this.kind.toString() + " " + props.toString() + " [[" + this.result + "]]"; |
|
116 } |
|
117 } |
|
118 } |
|
119 |
|
120 |
|
121 /** |
|
122 * Main result queue -- accumulates cooked messages asynchronously. |
|
123 */ |
|
124 public LinkedBlockingQueue<Result> results; |
|
125 |
|
126 private synchronized void putResult(Result.Kind kind, Properties props, String result) { |
|
127 try { |
|
128 results.put(new Result(kind, props, result)); |
|
129 } catch (InterruptedException exn) { } |
|
130 } |
|
131 private synchronized void putResult(Result.Kind kind, String result) { |
|
132 putResult(kind, null, result); |
|
133 } |
|
134 |
|
135 |
|
136 /** |
|
137 * Interrupts Isabelle process via Posix signal. |
|
138 * @throws isabelle.IsabelleProcess.IsabelleProcessException |
|
139 */ |
|
140 public synchronized void interrupt() throws IsabelleProcessException |
|
141 { |
|
142 if (proc != null && pid != null) { |
|
143 String kill = System.getProperty("isabelle.kill", "kill"); |
|
144 String [] cmdline = {kill, "-INT", pid}; |
|
145 try { |
|
146 putResult(Result.Kind.SIGNAL, "INT"); |
|
147 int rc = Runtime.getRuntime().exec(cmdline).waitFor(); |
|
148 if (rc != 0) { |
|
149 throw new IsabelleProcessException("Cannot interrupt: kill command failed"); |
|
150 } |
|
151 } catch (IOException exn) { |
|
152 throw new IsabelleProcessException(exn.getMessage()); |
|
153 } catch (InterruptedException exn) { |
|
154 throw new IsabelleProcessException("Cannot interrupt: aborted"); |
|
155 } |
|
156 } else { |
|
157 throw new IsabelleProcessException("Cannot interrupt: no process"); |
|
158 } |
|
159 } |
|
160 |
|
161 |
|
162 /** |
|
163 * Kills Isabelle process: try close -- sleep -- destroy. |
|
164 */ |
|
165 public synchronized void kill() throws IsabelleProcessException |
|
166 { |
|
167 if (proc != null) { |
|
168 tryClose(); |
|
169 try { |
|
170 Thread.sleep(300); |
|
171 } catch (InterruptedException exn) { } |
|
172 putResult(Result.Kind.SIGNAL, "KILL"); |
|
173 proc.destroy(); |
|
174 proc = null; |
|
175 } else { |
|
176 throw new IsabelleProcessException("Cannot kill: no process"); |
|
177 } |
|
178 } |
|
179 |
|
180 |
|
181 /** |
|
182 * Models basic Isabelle properties |
|
183 */ |
|
184 public static class Property { |
|
185 public static String ID = "id"; |
|
186 public static String LINE = "line"; |
|
187 public static String FILE = "file"; |
|
188 } |
|
189 |
|
190 /** |
|
191 * Auxiliary operation to encode text as Isabelle string token. |
|
192 */ |
|
193 public static String encodeString(String str) { |
|
194 Locale locale = null; |
|
195 StringBuffer buf = new StringBuffer(100); |
|
196 int i; |
|
197 char c; |
|
198 |
|
199 buf.append("\""); |
|
200 for (i = 0; i < str.length(); i++) { |
|
201 c = str.charAt(i); |
|
202 if (c < 32 || c == '\\' || c == '\"') { |
|
203 buf.append(String.format(locale, "\\%03d", (int) c)); |
|
204 } else { |
|
205 buf.append(c); |
|
206 } |
|
207 } |
|
208 buf.append("\""); |
|
209 return buf.toString(); |
|
210 } |
|
211 |
|
212 /** |
|
213 * Auxiliary operation to encode properties as Isabelle outer syntax. |
|
214 */ |
|
215 public static String encodeProperties(Properties props) { |
|
216 StringBuffer buf = new StringBuffer(100); |
|
217 buf.append("("); |
|
218 for (Enumeration<String> e = (Enumeration<String>) props.propertyNames(); e.hasMoreElements(); ) { |
|
219 String x = e.nextElement(); |
|
220 buf.append(encodeString(x)); |
|
221 buf.append(" = "); |
|
222 buf.append(encodeString(props.getProperty(x))); |
|
223 if (e.hasMoreElements()) { |
|
224 buf.append(", "); |
|
225 } |
|
226 } |
|
227 buf.append(")"); |
|
228 return buf.toString(); |
|
229 } |
|
230 |
|
231 |
|
232 /* output being piped into the process (stdin) */ |
|
233 |
|
234 private volatile BufferedWriter outputWriter; |
|
235 private class OutputThread extends Thread |
|
236 { |
|
237 public void run() |
|
238 { |
|
239 while (outputWriter != null) { |
|
240 try { |
|
241 String s = output.take(); |
|
242 if (s.equals("\u0000")) { |
|
243 outputWriter.close(); |
|
244 outputWriter = null; |
|
245 } else { |
|
246 putResult(Result.Kind.STDIN, s); |
|
247 outputWriter.write(s); |
|
248 outputWriter.flush(); |
|
249 } |
|
250 } catch (InterruptedException exn) { |
|
251 putResult(Result.Kind.SYSTEM, "Output thread interrupted"); |
|
252 } catch (IOException exn) { |
|
253 putResult(Result.Kind.SYSTEM, exn.getMessage() + " (output thread)"); |
|
254 } |
|
255 } |
|
256 putResult(Result.Kind.SYSTEM, "Output thread terminated"); |
|
257 } |
|
258 } |
|
259 private OutputThread outputThread; |
|
260 |
|
261 |
|
262 // public operations |
|
263 |
|
264 /** |
|
265 * Feeds arbitrary text into the process. |
|
266 */ |
|
267 public synchronized void output(String text) throws IsabelleProcessException |
|
268 { |
|
269 if (proc != null && !closing) { |
|
270 try { |
|
271 output.put(text); |
|
272 } catch (InterruptedException ex) { |
|
273 throw new IsabelleProcessException("Cannot output: aborted"); |
|
274 } |
|
275 } else if (proc == null) { |
|
276 throw new IsabelleProcessException("Cannot output: no process"); |
|
277 } else { |
|
278 throw new IsabelleProcessException("Cannot output: already closing"); |
|
279 } |
|
280 } |
|
281 |
|
282 /** |
|
283 * Closes Isabelle process input, causing termination eventually. |
|
284 */ |
|
285 public synchronized void close() throws IsabelleProcessException |
|
286 { |
|
287 output("\u0000"); |
|
288 closing = true; |
|
289 // FIXME watchdog/timeout |
|
290 } |
|
291 |
|
292 /** |
|
293 * Closes Isabelle process input, causing termination eventually -- unless process already terminated. |
|
294 */ |
|
295 public synchronized void tryClose() |
|
296 { |
|
297 if (proc != null && !closing) { |
|
298 try { |
|
299 close(); |
|
300 } catch (IsabelleProcessException ex) { } |
|
301 } |
|
302 } |
|
303 |
|
304 private synchronized void outputSync(String text) throws IsabelleProcessException |
|
305 { |
|
306 output(" \\<^sync>\n; " + text + " \\<^sync>;\n"); |
|
307 } |
|
308 |
|
309 /** |
|
310 * Feeds exactly one Isabelle command into the process. |
|
311 */ |
|
312 public synchronized void command(String text) throws IsabelleProcessException |
|
313 { |
|
314 outputSync("Isabelle.command " + encodeString(text)); |
|
315 } |
|
316 |
|
317 /** |
|
318 * Isabelle command with properties. |
|
319 */ |
|
320 public synchronized void command(Properties props, String text) throws IsabelleProcessException |
|
321 { |
|
322 outputSync("Isabelle.command " + encodeProperties(props) + " " + encodeString(text)); |
|
323 } |
|
324 |
|
325 /** |
|
326 * Feeds ML toplevel declarations into the process. |
|
327 */ |
|
328 public synchronized void ML(String text) throws IsabelleProcessException |
|
329 { |
|
330 outputSync("ML_val " + encodeString(text)); |
|
331 } |
|
332 |
|
333 /** |
|
334 * ML command with properties. |
|
335 */ |
|
336 public synchronized void ML(Properties props, String text) throws IsabelleProcessException |
|
337 { |
|
338 command(props, "ML_val " + encodeString(text)); |
|
339 } |
|
340 |
|
341 |
|
342 /* input from the process (stdout/stderr) */ |
|
343 |
|
344 private volatile BufferedReader inputReader; |
|
345 private class InputThread extends Thread |
|
346 { |
|
347 public void run() |
|
348 { |
|
349 Result.Kind kind = Result.Kind.STDOUT; |
|
350 Properties props = null; |
|
351 StringBuffer buf = new StringBuffer(100); |
|
352 |
|
353 try { |
|
354 while (inputReader != null) { |
|
355 if (kind == Result.Kind.STDOUT) { |
|
356 // char mode |
|
357 int c = -1; |
|
358 while ((buf.length() == 0 || inputReader.ready()) && |
|
359 (c = inputReader.read()) > 0 && c != 2) { |
|
360 buf.append((char) c); |
|
361 } |
|
362 if (buf.length() > 0) { |
|
363 putResult(kind, buf.toString()); |
|
364 buf = new StringBuffer(100); |
|
365 } |
|
366 if (c == -1) { |
|
367 inputReader.close(); |
|
368 inputReader = null; |
|
369 tryClose(); |
|
370 } |
|
371 else if (c == 2) { |
|
372 c = inputReader.read(); |
|
373 switch (c) { |
|
374 case 'A': kind = Result.Kind.WRITELN; break; |
|
375 case 'B': kind = Result.Kind.PRIORITY; break; |
|
376 case 'C': kind = Result.Kind.TRACING; break; |
|
377 case 'D': kind = Result.Kind.WARNING; break; |
|
378 case 'E': kind = Result.Kind.ERROR; break; |
|
379 case 'F': kind = Result.Kind.DEBUG; break; |
|
380 case 'G': kind = Result.Kind.PROMPT; break; |
|
381 case 'H': kind = Result.Kind.INIT; break; |
|
382 case 'I': kind = Result.Kind.STATUS; break; |
|
383 default: kind = Result.Kind.STDOUT; break; |
|
384 } |
|
385 props = null; |
|
386 } |
|
387 } else { |
|
388 // line mode |
|
389 String line = null; |
|
390 if ((line = inputReader.readLine()) != null) { |
|
391 int len = line.length(); |
|
392 // property |
|
393 if (line.endsWith("\u0002,")) { |
|
394 int i = line.indexOf("="); |
|
395 if (i > 0) { |
|
396 String name = line.substring(0, i); |
|
397 String value = line.substring(i + 1, len - 2); |
|
398 if (props == null) |
|
399 props = new Properties(); |
|
400 if (!props.containsKey(name)) { |
|
401 props.setProperty(name, value); |
|
402 } |
|
403 } |
|
404 } |
|
405 // last text line |
|
406 else if (line.endsWith("\u0002.")) { |
|
407 if (kind == Result.Kind.INIT && props != null) { |
|
408 pid = props.getProperty("pid"); |
|
409 session = props.getProperty("session"); |
|
410 } |
|
411 buf.append(line.substring(0, len - 2)); |
|
412 putResult(kind, props, buf.toString()); |
|
413 buf = new StringBuffer(100); |
|
414 kind = Result.Kind.STDOUT; |
|
415 } |
|
416 // text line |
|
417 else { |
|
418 buf.append(line); |
|
419 buf.append("\n"); |
|
420 } |
|
421 } else { |
|
422 inputReader.close(); |
|
423 inputReader = null; |
|
424 tryClose(); |
|
425 } |
|
426 } |
|
427 } |
|
428 } catch (IOException exn) { |
|
429 putResult(Result.Kind.SYSTEM, exn.getMessage() + " (input thread)"); |
|
430 } |
|
431 putResult(Result.Kind.SYSTEM, "Input thread terminated"); |
|
432 } |
|
433 } |
|
434 private InputThread inputThread; |
|
435 |
|
436 private volatile BufferedReader errorReader; |
|
437 private class ErrorThread extends Thread |
|
438 { |
|
439 public void run() |
|
440 { |
|
441 try { |
|
442 while (errorReader != null) { |
|
443 StringBuffer buf = new StringBuffer(100); |
|
444 int c; |
|
445 while ((buf.length() == 0 || errorReader.ready()) && (c = errorReader.read()) > 0) { |
|
446 buf.append((char) c); |
|
447 } |
|
448 if (buf.length() > 0) { |
|
449 putResult(Result.Kind.STDERR, buf.toString()); |
|
450 } else { |
|
451 errorReader.close(); |
|
452 errorReader = null; |
|
453 tryClose(); |
|
454 } |
|
455 } |
|
456 } catch (IOException exn) { |
|
457 putResult(Result.Kind.SYSTEM, exn.getMessage() + " (error thread)"); |
|
458 } |
|
459 putResult(Result.Kind.SYSTEM, "Error thread terminated"); |
|
460 } |
|
461 } |
|
462 private ErrorThread errorThread; |
|
463 |
|
464 |
|
465 /* exit thread */ |
|
466 |
|
467 private class ExitThread extends Thread |
|
468 { |
|
469 public void run() |
|
470 { |
|
471 try { |
|
472 int rc = proc.waitFor(); |
|
473 Thread.sleep(300); |
|
474 putResult(Result.Kind.SYSTEM, "Exit thread terminated"); |
|
475 putResult(Result.Kind.EXIT, Integer.toString(rc)); |
|
476 proc = null; |
|
477 } catch (InterruptedException exn) { |
|
478 putResult(Result.Kind.SYSTEM, "Exit thread interrupted"); |
|
479 } |
|
480 } |
|
481 } |
|
482 private ExitThread exitThread; |
|
483 |
|
484 |
|
485 /** |
|
486 * Creates Isabelle process with specified logic image. |
|
487 */ |
|
488 public IsabelleProcess(String [] options, String logic) throws IsabelleProcessException |
|
489 { |
|
490 ArrayList<String> cmdline = new ArrayList<String> (); |
|
491 String shell = null; |
|
492 String home = null; |
|
493 String charset = "UTF-8"; |
|
494 |
|
495 shell = System.getProperty("isabelle.shell"); |
|
496 home = System.getProperty("isabelle.home"); |
|
497 if (shell != null && home != null) { |
|
498 cmdline.add(shell); |
|
499 cmdline.add(home + "/bin/isabelle-process"); |
|
500 } else if (home != null) { |
|
501 cmdline.add(home + "/bin/isabelle-process"); |
|
502 } else if (shell != null) { |
|
503 throw new IsabelleProcessException("Cannot start process: isabelle.shell property requires isabelle.home"); |
|
504 } else { |
|
505 cmdline.add("isabelle-process"); |
|
506 } |
|
507 cmdline.add("-W"); |
|
508 if (options != null) { |
|
509 for (String opt: options) cmdline.add(opt); |
|
510 } |
|
511 if (logic != null) cmdline.add(logic); |
|
512 |
|
513 try { |
|
514 String [] cmd = new String[cmdline.size()]; |
|
515 cmdline.toArray(cmd); |
|
516 proc = Runtime.getRuntime().exec(cmd); |
|
517 } catch (IOException exn) { |
|
518 throw new IsabelleProcessException(exn.getMessage()); |
|
519 } |
|
520 |
|
521 try { |
|
522 outputWriter = new BufferedWriter(new OutputStreamWriter(proc.getOutputStream(), charset)); |
|
523 inputReader = new BufferedReader(new InputStreamReader(proc.getInputStream(), charset)); |
|
524 errorReader = new BufferedReader(new InputStreamReader(proc.getErrorStream(), charset)); |
|
525 } catch (UnsupportedEncodingException exn) { |
|
526 proc.destroy(); |
|
527 throw new Error(exn.getMessage()); |
|
528 } |
|
529 |
|
530 output = new LinkedBlockingQueue<String>(); |
|
531 outputThread = new OutputThread(); |
|
532 |
|
533 results = new LinkedBlockingQueue<Result>(); |
|
534 inputThread = new InputThread(); |
|
535 errorThread = new ErrorThread(); |
|
536 exitThread = new ExitThread(); |
|
537 |
|
538 outputThread.start(); |
|
539 inputThread.start(); |
|
540 errorThread.start(); |
|
541 exitThread.start(); |
|
542 } |
|
543 |
|
544 /** |
|
545 * Creates Isabelle process without options. |
|
546 */ |
|
547 public IsabelleProcess(String logic) throws IsabelleProcessException { |
|
548 this(null, logic); |
|
549 } |
|
550 |
|
551 /** |
|
552 * Creates Isabelle process with default logic image. |
|
553 */ |
|
554 public IsabelleProcess() throws IsabelleProcessException { |
|
555 this(null); |
|
556 } |
|
557 } |
|