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

escjava.prover
Class SubProcess

java.lang.Object
  extended byescjava.prover.SubProcess

public class SubProcess
extends java.lang.Object

Instances of this class represent subprocesses.

SubProcesses 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.

SubProcesses 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 SLists 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 Atoms and SInts:

     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.
  • Atoms 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 Atoms 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 SLists 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 SExps 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 SLists, it will not cause processing to stop.

Note:
See the warnings on readSExp()!

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

The ESC/Java2 Project Homepage