Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

## escjava.prover
Class SubProcess

    java.lang.Object
      escjava.prover.SubProcess

public class SubProcess
extends java.lang.Object

Instances of this class represent subprocesses.

`SubProcess`es are created by invoking a named program with a given pathname. Input can be submitted to the resulting subprocess; routines are provided for use in parsing the subprocesses' resulting output.

`SubProcess`es can be closed; afterwards none of their methods (except close) should ever be called again.

If any errors occur (including parsing errors), a fatal error will be reported.

As a debugging aid, if `Info.on` is true, we save all the characters read by clients from this subprocess since the last `resetInfo()` call. In the event of a parsing error (see `handleUnexpected(String)`), we use this information, if available, to produce a more useful error message.

Note that a Java application will not exit normally (i.e., when its `main()` method returns) until all subprocesses have finished. In particular, this implies that all `SubProcess` instances must be closed before this can occur. Alternatively, a Java application can just call `System.exit(int)` to force an exit to occur without waiting for subprocesses.

Todo:
  Introduce a model variable notClosed that relates to P for clearer preconditions.

Nested Class Summary
`static class` | `SubProcess.Died`

Field Summary
`static SubProcess.Died` | `DIED`
`private java.io.PushbackInputStream` | `from` The `PushbackInputStream` from the actual subprocess, or `null` if we are closed.
`java.lang.String` | `name` The name of the subprocess, suitable for use in error messages.
`private java.lang.Process` | `P` The actual subprocess, or `null` if we are closed.
`private java.lang.StringBuffer` | `readChars` If non-`null`, this buffer keeps a record of (some of) the characters read from this subprocess using `getChar()`.
`private java.io.PrintStream` | `to` The `PrintStream` to the actual subprocess, or `null` if we are closed.

Constructor Summary
`SubProcess(java.lang.String name, java.lang.String[] pathAndArgs, java.lang.String[] envp)` Instantiate a subprocess.

Method Summary
`void` | `checkChar(char c)` Consume the next output character from this subprocess.
`void` | `checkString(java.lang.String s)` Ensure that the next output characters from this subprocess (consumed in the process) matches the provided string.
`void` | `close()` Close this subprocess.
`void` | `eatWhitespace()` Consume any whitespace (spaces, tabs, and newlines) present in the subprocesses' output.
`int` | `getChar()`
`private void` | `handleReadError(java.io.IOException e)` Turn an `IOException` resulting from a read on `from` into a fatal error.
`void` | `handleUnexpected(java.lang.String wanted)` Report a fatal error due to unexpected output from the subprocess.
`int` | `peekChar()` Like `getChar()`, but leaves the character in the stream.
`int` | `readNumber()` Reads a (possibly empty) sequence of digits from the subprocess and returns the digits as a number.
`SExp` | `readSExp()`
`SList` | `readSExps(char stop)`
`SList` | `readSList()`
`SList` | `readSLists()` Read a (possibly empty) series of `SList`s from this subprocess.
`java.lang.String` | `readWord(java.lang.String stops)` Read characters from this subprocess up to, but not including a character from the provided string `stops`, or an EOF.
`void` | `resetInfo()` Reset the memory of the recent output from this subprocess.
`void` | `send(java.lang.String s)` Send a string to this subprocess.
`java.io.PrintStream` | `ToStream()`
`private static java.lang.String` | `trimNewlines(java.lang.String s)`

Methods inherited from class java.lang.Object
`clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait`

Field Detail

### DIED

    public static final SubProcess.Died DIED

### name

    public final java.lang.String name

  The name of the subprocess, suitable for use in error messages.

### P

    private java.lang.Process P

  The actual subprocess, or `null` if we are closed.

### to

    private java.io.PrintStream to

  The `PrintStream` to the actual subprocess, or `null` if we are closed.

### from

    private java.io.PushbackInputStream from

  The `PushbackInputStream` from the actual subprocess, or `null` if we are closed.

### readChars

    private final java.lang.StringBuffer readChars

  If non-`null`, this buffer keeps a record of (some of) the characters read from this subprocess using `getChar()`.

  In the event of a parsing error (see `handleUnexpected(String)`), we use this information, if available, to produce a more useful error message.

Constructor Detail

### SubProcess

    public SubProcess(java.lang.String name,
                      java.lang.String[] pathAndArgs,
                      java.lang.String[] envp)

  Instantiate a subprocess.

  The resulting invocation is initially open, but may be closed permanently with the `close()` method.

  This constructor may result in a fatal error if any problems occur.

Parameters:
  `name` - should be a unique short name for use in error messages (E.g., "Simplify").
  `pathAndArgs` - is an array containing the full pathname of the program to execute to obtain the subprocess (e.g., "/usr/bin/emacs") and any command-line arguments.

Method Detail

### close

    public void close()

  Close this subprocess.

  This destroys the associated subprocess. Afterwards, none of the methods of this object should ever be called again.

  This method may result in a fatal error if any problems occur. This subprocess is guaranteed to be destroyed on completion, regardless of which exit is taken.

### send

    public void send(java.lang.String s)

  Send a string to this subprocess.

### ToStream

    public java.io.PrintStream ToStream()

### getChar

    public int getChar()

  Returns:
    the next output character from this subprocess. If an I/O error occurs or there are no more characters available (i.e., EOF is reached), a fatal error is reported and a -1 is returned.

    Saves the output character (if any) in `readChars` if it is non-null. (This is a private debugging aid.)

### peekChar

    public int peekChar()

  Like `getChar()`, but leaves the character in the stream. If an I/O error occurs, a fatal error is reported.

  Returns:
    A -1 is returned on EOF, otherwise the next character read from the subprocess is returned as an integer.

### resetInfo

    public void resetInfo()

  Reset the memory of the recent output from this subprocess.

  In the event of a parsing error (see `handleUnexpected(String)`), we use any remembered recent output to produce a more useful error message.

### handleReadError

    private void handleReadError(java.io.IOException e)

  Turn an `IOException` resulting from a read on `from` into a fatal error.

### handleUnexpected

    public void handleUnexpected(java.lang.String wanted)

  Report a fatal error due to unexpected output from the subprocess.

  Use this routine if at all possible, because it provides additional useful information (when `Info.on` is true) about the output read recently, what was expected, and the remaining output.

  Parameters:
    `wanted` - is the output we expected.

### trimNewlines

    private static java.lang.String trimNewlines(java.lang.String s)

  Parameters:
    `s` - the string to trim.
  Returns:
    the parameter `s`, but with starting and ending newline characters removed

### checkChar

    public void checkChar(char c)

  Consume the next output character from this subprocess. If it is not exactly `c`, a fatal error is reported.

### checkString

    public void checkString(java.lang.String s)

  Ensure that the next output characters from this subprocess (consumed in the process) matches the provided string. If this does not occur, a fatal error is reported.

  Parameters:
    `s` - the string to match.

### eatWhitespace

    public void eatWhitespace()

  Consume any whitespace (spaces, tabs, and newlines) present in the subprocesses' output.

### readWord

    public java.lang.String readWord(java.lang.String stops)

  Read characters from this subprocess up to, but not including a character from the provided string `stops`, or an EOF.

  Parameters:
    `stops` - a string containing all characters on which to stop reading.
  Returns:
    the read characters, not including any character from `stops`.

### readNumber

    public int readNumber()

  Reads a (possibly empty) sequence of digits from the subprocess and returns the digits as a number. Assumes no overflow will occur.

### readSList

    public SList readSList()

  Returns:
    a non-null `SList` from this subprocess. A fatal error is reported if any errors occur.
  Note:
    See the warnings on `readSExp()`!

### readSExp

    public SExp readSExp()

  Returns:
    a non-null `SExp` read from this subprocess. A fatal error is reported if any errors occur.

    We use the following grammar for `Atom`s and `SInt`s:

             SInt  ::= ['+'|'-']*

             Atom ::= + modulo it's not a SInt as
                      defined above.

    We do further processing as follows:

    - integers are parsed to ints using the `Integer` class.
    - `Atom`s are parsed by removing the first and last characters iff the first character is a '|'.
  Warning:
    This means we do not handle correctly atoms containing the characters ' ', '\n', '\\', '(', ')', and '|' (the last inside the atom). Likewise, we do not handle `Atom`s that start with '|' but do not end with a different '|'. For speed reasons, this limitation may be left in the final version.

### readSLists

    public SList readSLists()

  Read a (possibly empty) series of `SList`s from this subprocess. A fatal error is reported if any errors occur.

  I.e., "(a b) (c d (e) f)" returns the SExp ((a b) (c d (e) f)). This routine never returns `null`.

  Note:
    See the warnings on `readSExp()`!

### readSExps

    public SList readSExps(char stop)

  Parameters:
    `stop` - the character that causes reading to stop.
  Returns:
    the slist read from this subprocess.

    Read a (possibly empty) series of `SExp`s from this subprocess, until the supplied stop character is seen (but not read). A fatal error is reported if any errors occur.

    I.e., "e (a b) (c d (e) f)$(1 3)" where $ is the stop character returns the `SExp` (e (a b) (c d (e) f)), leaving the remaining unprocessed output "$(1 3)". If the stop character occurs in the middle of atoms or `SList`s, it will not cause processing to stop.

  Note:
    See the warnings on `readSExp()`!

Overview | Package | Class | Use | Tree | Deprecated | Index | Help
| ESC/Java2 © 2003,2004,2005 David Cok and Joseph Kiniry © 2005 UCD Dublin © 2003,2004 Radboud University Nijmegen © 1999,2000 Compaq Computer Corporation © 1997,1998,1999 Digital Equipment Corporation All Rights Reserved
PREV CLASS NEXT CLASS | FRAMES NO FRAMES
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD

The ESC/Java2 Project Homepage