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 }