001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package escjava.prover;
004
005 import java.io.*;
006
007 import javafe.util.*;
008
009 /**
010 * Instances of this class represent subprocesses.
011 *
012 * <p> <code>SubProcess</code>es are created by invoking a named
013 * program with a given pathname. Input can be submitted to the
014 * resulting subprocess; routines are provided for use in parsing the
015 * subprocesses' resulting output. </p>
016 *
017 * <p> <code>SubProcess</code>es can be closed; afterwards none of
018 * their methods (except close) should ever be called again. </p>
019 *
020 * <p> If any errors occur (including parsing errors), a fatal error
021 * will be reported. </p>
022 *
023 * <p> As a debugging aid, if {@link Info#on} is true, we save all the
024 * characters read by clients from this subprocess since the last
025 * {@link #resetInfo()} call. In the event of a parsing error (see
026 * {@link #handleUnexpected(String)}), we use this information, if
027 * available, to produce a more useful error message. </p>
028 *
029 * <p> Note that a Java application will not exit normally (i.e., when
030 * its <code>main()</code> method returns) until all subprocesses have
031 * finished. In particular, this implies that all
032 * <code>SubProcess</code> instances must be closed before this can
033 * occur. Alternatively, a Java application can just call {@link
034 * java.lang.System#exit(int)} to force an exit to occur without
035 * waiting for subprocesses. </p>
036 *
037 * @todo Introduce a model variable notClosed that relates to P for
038 * clearer preconditions.
039 */
040
041 public class SubProcess {
042 static public class Died extends RuntimeException {
043 private static final long serialVersionUID = 2624260378471410994L;
044 }
045
046 final static public /*@ non_null @*/ Died DIED = new Died();
047
048 /**
049 * The name of the subprocess, suitable for use in error messages.
050 */
051 public final /*@ non_null @*/ String name;
052
053 /**
054 * The actual subprocess, or <code>null</code> if we are closed.
055 */
056 //@ spec_public
057 private Process P = null;
058
059 //@ public model boolean closed;
060 //@ private represents closed <- P == null;
061
062 /**
063 * The {@link PrintStream} to the actual subprocess, or
064 * <code>null</code> if we are closed.
065 */
066 //@ invariant (to == null) <==> (P == null);
067 //@ invariant (to == null) ==> closed;
068 //@ spec_public
069 private PrintStream to = null;
070
071 /**
072 * The {@link PushbackInputStream} from the actual subprocess, or
073 * <code>null</code> if we are closed.
074 */
075 //@ invariant (from == null) <==> (P == null);
076 //@ spec_public
077 private PushbackInputStream from = null;
078
079 /**
080 * If non-<code>null</code>, this buffer keeps a record of (some
081 * of) the characters read from this subprocess using {@link
082 * #getChar()}.
083 *
084 * <p> In the event of a parsing error (see {@link
085 * #handleUnexpected(String)}), we use this information, if
086 * available, to produce a more useful error message. </p>
087 */
088 //@ spec_public
089 private final StringBuffer readChars = (escjava.Main.options().trackReadChars ?
090 new StringBuffer() :
091 null);
092
093 /**
094 * Instantiate a subprocess.
095 *
096 * <p> The resulting invocation is initially open, but may be closed
097 * permanently with the {@link #close()} method. </p>
098 *
099 * <p> This constructor may result in a fatal error if any
100 * problems occur. </p>
101 *
102 * @param name should be a unique short name for use in error
103 * messages (E.g., "Simplify").
104 * @param pathAndArgs is an array containing the full pathname of the program to execute to
105 * obtain the subprocess (e.g., "/usr/bin/emacs") and any command-line arguments.
106 */
107 /*@ public normal_behavior
108 @ assignable this.name, to, from, P;
109 @ ensures this.name == name;
110 @ ensures to != null;
111 @ ensures from != null;
112 @ ensures !closed;
113 @*/
114 public SubProcess(/*@ non_null @*/ String name,
115 /*@ non_null @*/ String[] pathAndArgs,
116 String[] envp) {
117 this.name = name;
118 try {
119 P = Runtime.getRuntime().exec(pathAndArgs,envp);
120 if (P == null)
121 throw new IOException();
122 } catch (IOException e) {
123 javafe.util.ErrorSet.fatal("Unable to invoke " + name);
124 }
125
126 OutputStream out = P.getOutputStream();
127 Assert.notNull(out); //@ nowarn Pre; //Unsure if this is always true
128
129 if (escjava.Main.options().sxLog != null) {
130 try {
131 OutputStream fos = new FileOutputStream(escjava.Main.options().sxLog);
132 if (escjava.Main.options().prettyPrintVC)
133 fos = new PPOutputStream(fos);
134
135 out = new TeeOutputStream(fos, out);
136 } catch (FileNotFoundException fnfe) {
137 javafe.util.ErrorSet.fatal("error opening sxLog file " +
138 escjava.Main.options().sxLog);
139 }
140 }
141 to = new PrintStream(out);
142 from = new PushbackInputStream(P.getInputStream());
143 }
144
145
146 /**
147 * Close this subprocess.
148 *
149 * <p> This destroys the associated subprocess. Afterwards, none
150 * of the methods of this object should ever be called again. </p>
151 *
152 * <p> This method may result in a fatal error if any problems
153 * occur. This subprocess is guaranteed to be destroyed on
154 * completion, regardless of which exit is taken. </p>
155 */
156 /*@ public normal_behavior
157 @ modifies from, to, P;
158 @ ensures P == null;
159 @ ensures to == null;
160 @ ensures from == null;
161 @ ensures closed;
162 @*/
163 public void close() {
164 try {
165 if (to != null)
166 to.close();
167 if (from != null)
168 from.close(); // may throw IOException
169 } catch (IOException e) {
170 ErrorSet.fatal("The following I/O error occurred while "
171 + "trying to close the connection to " + name + ": "
172 + e.getMessage());
173 } finally {
174 if (P != null)
175 P.destroy();
176 P = null;
177 to = null;
178 from = null;
179 }
180 }
181
182 // Sending characters to a subprocess.
183
184 /**
185 * Send a string to this subprocess.
186 */
187 //@ public normal_behavior
188 //@ requires P != null;
189 //@ requires !closed;
190 //@ modifies to;
191 public void send(/*@ non_null @*/ String s) {
192 Assert.notNull(P); //@ nowarn Pre; // precondition
193 to.println(s);
194 to.flush();
195 }
196
197 //@ public normal_behavior
198 //@ requires !closed;
199 //@ ensures (\result == null) <==> (P == null);
200 public /*@ pure @*/ PrintStream ToStream() {
201 return to;
202 }
203
204 // Reading characters from a subprocess's output.
205
206 /**
207 * @return the next output character from this subprocess. If an
208 * I/O error occurs or there are no more characters available
209 * (i.e., EOF is reached), a fatal error is reported and a -1 is
210 * returned.
211 *
212 * <p> Saves the output character (if any) in {@link #readChars} if
213 * it is non-null. (This is a private debugging aid.) </p>
214 */
215 //@ public normal_behavior
216 //@ requires P != null;
217 //@ requires !closed;
218 //@ modifies readChars.*;
219 //@ ensures \result >= 0;
220 //@ also
221 //@ public exceptional_behavior
222 //@ requires P == null;
223 //@ modifies \everything;
224 //@ signals_only Died;
225 //@ signals (Died) true;
226 public int getChar() {
227 if (P == null) throw new Died();
228
229 try {
230 int next = from.read();
231 if (next < 0)
232 ErrorSet.fatal("Unexpected exit by " + name + " subprocess");
233 char c = (char)next;
234
235 if (readChars != null)
236 readChars.append(c);
237
238 return c;
239 } catch (IOException e) {
240 handleReadError(e);
241 return -0; // Make the compiler happy...
242 }
243 }
244
245 /**
246 * Like {@link #getChar()}, but leaves the character in the stream.
247 * If an I/O error occurs, a fatal error is reported.
248 *
249 * @return A -1 is returned on EOF, otherwise the next character
250 * read from the subprocess is returned as an integer.
251 */
252 //@ public normal_behavior
253 //@ requires P != null;
254 //@ requires !closed;
255 //@ modifies \everything;
256 //@ ensures \result >= -1;
257 //@ also
258 //@ public exceptional_behavior
259 //@ requires P == null;
260 //@ modifies \everything;
261 //@ signals_only Died;
262 //@ signals (Died) true;
263 public int peekChar() {
264 // P may have been closed on us
265 if (P == null) throw new Died();
266
267 try {
268 int next = from.read();
269 if (next != -1)
270 from.unread(next);
271 return next;
272 } catch (IOException e) {
273 handleReadError(e);
274 return -1; // dummy return
275 }
276 }
277
278 /**
279 * Reset the memory of the recent output from this subprocess.
280 *
281 * <p> In the event of a parsing error (see {@link
282 * #handleUnexpected(String)}), we use any remembered recent
283 * output to produce a more useful error message. </p>
284 */
285 //@ public normal_behavior
286 //@ requires !closed;
287 //@ modifies readChars.*;
288 //@ ensures (readChars != null) ==> readChars.length() == 0;
289 public void resetInfo() {
290 if (readChars != null)
291 readChars.setLength(0);
292 }
293
294 /**
295 * Turn an {@link IOException} resulting from a read on {@link
296 * #from} into a fatal error.
297 */
298 /*@ private behavior
299 @ requires true;
300 @ diverges true;
301 @ assignable \everything;
302 @ ensures false;
303 @ signals(Exception) false;
304 @*/
305 private void handleReadError(/*@ non_null @*/ IOException e) {
306 ErrorSet.fatal("I/O error encountered while reading "
307 + name + "'s output: " + e.getMessage());
308 }
309
310
311 // Verifying the subprocesses' output.
312
313 /**
314 * Report a fatal error due to unexpected output from the subprocess.
315 *
316 * <p> Use this routine if at all possible, because it provides
317 * additional useful information (when {@link javafe.util.Info#on}
318 * is true) about the output read recently, what was expected, and
319 * the remaining output. </p>
320 *
321 * @param wanted is the output we expected.
322 */
323 //@ behavior
324 //@ modifies \everything;
325 //@ ensures closed;
326 public void handleUnexpected(/*@ non_null @*/ String wanted) {
327 if (readChars != null && Info.on) {
328 Info.out("***** Unexpected output encountered while parsing "
329 + name + "'s output");
330 Info.out("Already read: [" + readChars.toString() + "]");
331 Info.out("Expected " + wanted);
332 }
333 if (readChars != null) {
334 if (P != null) {
335 to.close();
336 while (peekChar() != -1)
337 getChar();
338 }
339 }
340
341 StringBuffer errOut = new StringBuffer();
342 if (P != null) {
343 InputStream err = P.getErrorStream();
344 // FIXME - change this to read characters?
345 byte[] buf = new byte[1024];
346 try {
347 while (true) {
348 int r = err.read(buf);
349 if (r == -1) {
350 break;
351 }
352 errOut.append(new String(buf, 0, r));
353 }
354 } catch (IOException ioe) {
355 errOut.append("<IOException: ");
356 errOut.append(ioe.toString());
357 errOut.append(">");
358 }
359 }
360
361 close();
362
363 String suffix = null;
364 if (readChars != null) {
365 suffix = ":" +
366 "\n----- Begin unexpected output -----\n" +
367 trimNewlines(readChars.toString()) +
368 "\n----- End unexpected output -----";
369 }
370 if (errOut.length() != 0) {
371 if (suffix == null) {
372 suffix = ":";
373 }
374 suffix += "\n----- Begin stderr of unexpected output -----\n" +
375 errOut +
376 "\n----- End stderr or unexpected output -----";
377 }
378 ErrorSet.fatal("Unexpected output encountered while parsing " +
379 name + "'s output" +
380 (suffix == null ? "" : suffix));
381 }
382
383 /**
384 * @param s the string to trim.
385 * @return the parameter <code>s</code>, but with starting and
386 * ending newline characters removed
387 */
388 static private /*@ pure non_null @*/ String trimNewlines(/*@ non_null @*/ String s) {
389 int start = 0;
390 int end = s.length();
391 while (start < end && s.charAt(start) == '\n') {
392 start++;
393 }
394 while (start < end && s.charAt(end-1) == '\n') {
395 end--;
396 }
397 return s.substring(start, end);
398 }
399
400 /**
401 * Consume the next output character from this subprocess. If it
402 * is not exactly <code>c</code>, a fatal error is reported.
403 */
404 //@ public normal_behavior
405 //@ requires P != null;
406 //@ requires !closed;
407 //@ modifies \everything;
408 //@ also
409 //@ public behavior
410 //@ modifies \everything;
411 //@ ensures closed;
412 public void checkChar(char c) {
413 if (c == getChar())
414 return;
415
416 handleUnexpected("the character '" + c + "'");
417 }
418
419 /**
420 * Ensure that the next output characters from this subprocess
421 * (consumed in the process) matches the provided string. If this
422 * does not occur, a fatal error is reported.
423 *
424 * @param s the string to match.
425 */
426 //@ public normal_behavior
427 //@ requires P != null;
428 //@ requires !closed;
429 //@ modifies \everything;
430 //@ also
431 //@ public behavior
432 //@ modifies \everything;
433 //@ ensures closed;
434 public void checkString(/*@ non_null @*/ String s) {
435 for (int i = 0; i < s.length(); i++) {
436 checkChar(s.charAt(i));
437 }
438 }
439
440 // General purpose parsing routines.
441
442 /**
443 * Consume any whitespace (spaces, tabs, and newlines) present in
444 * the subprocesses' output.
445 */
446 //@ public normal_behavior
447 //@ requires P != null;
448 //@ requires !closed;
449 //@ modifies \everything;
450 public void eatWhitespace() {
451 for (int next = peekChar();
452 next == ' ' || next == '\t' || next == '\n';
453 next = peekChar())
454 getChar();
455 }
456
457 /**
458 * Read characters from this subprocess up to, but <em>not</em>
459 * including a character from the provided string
460 * <code>stops</code>, or an EOF.
461 *
462 * @param stops a string containing all characters on which to
463 * stop reading.
464 * @return the read characters, not including any character from
465 * <code>stops</code>.
466 */
467 /*@ public normal_behavior
468 @ requires P != null;
469 @ requires !closed;
470 @ modifies \everything;
471 @ ensures (\forall int i; 0 <= i && i <= \result.length();
472 @ stops.indexOf(\result.charAt(i)) == -1);
473 @ ensures \result != null;
474 @*/
475 public /*@ non_null @*/ String readWord(/*@ non_null @*/ String stops) {
476 StringBuffer soFar = new StringBuffer();
477
478 while (true) {
479 int next = peekChar();
480
481 if (next >= 0 && stops.indexOf((char)next) != -1)
482 break;
483
484 soFar.append((char)getChar());
485 }
486
487 return soFar.toString();
488 }
489
490 /**
491 * Reads a (possibly empty) sequence of digits from the subprocess
492 * and returns the digits as a number. Assumes no overflow will
493 * occur.
494 */
495 //@ public normal_behavior
496 //@ requires P != null;
497 //@ requires !closed;
498 //@ modifies \everything;
499 //@ ensures 0 <= \result;
500 public int readNumber() {
501 int n = 0;
502 while (Character.isDigit((char)peekChar())) {
503 n = 10*n + getChar() - '0';
504 }
505 return n;
506 }
507
508
509 // Reading SExps and SLists
510
511 /**
512 * @return a non-null {@link SList} from this subprocess. A fatal
513 * error is reported if any errors occur.
514 *
515 * @note See the warnings on {@link #readSExp()}!
516 */
517 //@ public normal_behavior
518 //@ requires P != null;
519 //@ requires !closed;
520 //@ modifies \everything;
521 public /*@ non_null @*/ SList readSList() {
522 eatWhitespace();
523 checkChar('(');
524
525 SList l = SList.make();
526 while (true) {
527 eatWhitespace();
528 if (peekChar()==')')
529 break;
530 l = new SPair(readSExp(), l);
531 }
532 l = SList.reverseD(l);
533 checkChar(')');
534 return l;
535 }
536
537 /**
538 * @return a non-null {@link SExp} read from this subprocess. A
539 * fatal error is reported if any errors occur.
540 *
541 * <p> We use the following grammar for {@link Atom}s and {@link
542 * SInt}s:
543 * <pre>
544 * SInt ::= ['+'|'-']<digit><not one of "() \n\t">*
545 *
546 * Atom ::= <not one of "() \n\t">+ modulo it's not a SInt as
547 * defined above.
548 * </pre>
549 *
550 * <p> We do further processing as follows:
551 * <ul>
552 * <li> integers are parsed to ints using the {@link
553 * java.lang.Integer} class. </li>
554 * <li> {@link Atom}s are parsed by removing the first and last
555 * characters iff the first character is a '|'. </li>
556 * </ul>
557 *
558 * @warning This means we do not handle correctly atoms containing
559 * the characters ' ', '\n', '\\', '(', ')', and '|' (the last
560 * inside the atom). Likewise, we do not handle {@link Atom}s
561 * that start with '|' but do not end with a different '|'. For
562 * speed reasons, this limitation may be left in the final
563 * version.
564 */
565 //@ public normal_behavior
566 //@ requires P != null;
567 //@ requires !closed;
568 //@ modifies \everything;
569 public /*@ non_null @*/ SExp readSExp() {
570 eatWhitespace();
571 if (peekChar() == '(')
572 return readSList();
573
574 // It's an Atom or integer, not a SList.
575 String token = readWord("() \n\t");
576 if (token.length() == 0)
577 handleUnexpected("SExp");
578
579 // Handle integers.
580 char first = token.charAt(0);
581 if (first == '+' || first == '-') {
582 if (token.length() > 1)
583 first = token.charAt(1);
584 }
585 if (Character.isDigit(first)) {
586 try {
587 return SExp.make(new Integer(token).intValue());
588 } catch (NumberFormatException e) {
589 handleUnexpected("valid integer");
590 }
591 }
592
593 // Handle atoms.
594 if (token.charAt(0) == '|')
595 token = token.substring(1, token.length() - 1);
596
597 return Atom.fromString(token);
598 }
599
600 /**
601 * Read a (possibly empty) series of {@link SList}s from this
602 * subprocess. A fatal error is reported if any errors occur.
603 *
604 * <p> I.e., "(a b) (c d (e) f)" returns the SExp ((a b) (c d (e)
605 * f)). This routine never returns <code>null</code>.
606 *
607 * @note See the warnings on {@link #readSExp()}!
608 */
609 //@ public normal_behavior
610 //@ requires P != null;
611 //@ requires !closed;
612 //@ modifies \everything;
613 public /*@ non_null @*/ SList readSLists() {
614 SList l = SList.make();
615
616 while (true) {
617 eatWhitespace();
618 if (peekChar() != '(')
619 break;
620 l = new SPair(readSList(), l);
621 }
622 l = SList.reverseD(l);
623 return l;
624 }
625
626 /**
627 * @param stop the character that causes reading to stop.
628 * @return the slist read from this subprocess.
629 *
630 * <p> Read a (possibly empty) series of {@link SExp}s from this
631 * subprocess, until the supplied stop character is seen (but not
632 * read). A fatal error is reported if any errors occur. </p>
633 *
634 * <p> I.e., "e (a b) (c d (e) f)$(1 3)" where $ is the stop
635 * character returns the {@link SExp} (e (a b) (c d (e) f)),
636 * leaving the remaining unprocessed output "$(1 3)". If the stop
637 * character occurs in the middle of atoms or {@link SList}s, it
638 * will not cause processing to stop. </p>
639 *
640 * @note See the warnings on {@link #readSExp()}!
641 */
642 //@ public normal_behavior
643 //@ requires P != null;
644 //@ requires !closed;
645 //@ requires stop != ' ' && stop != '\t' && stop != '\n';
646 //@ modifies \everything;
647 public /*@ non_null @*/ SList readSExps(char stop) {
648 SList l = SList.make();
649
650 while (true) {
651 eatWhitespace();
652 if (peekChar() == stop)
653 break;
654
655 l = new SPair(readSExp(), l);
656 }
657 l = SList.reverseD(l);
658 return l;
659 }
660 }