|
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 |
java.lang.Objectescjava.prover.SubProcess
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.
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 |
public static final SubProcess.Died DIED
public final java.lang.String name
private java.lang.Process P
null
if we are closed.
private java.io.PrintStream to
PrintStream
to the actual subprocess, or
null
if we are closed.
private java.io.PushbackInputStream from
PushbackInputStream
from the actual subprocess, or
null
if we are closed.
private final java.lang.StringBuffer readChars
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 |
public SubProcess(java.lang.String name, java.lang.String[] pathAndArgs, java.lang.String[] envp)
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.
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 |
public void close()
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.
public void send(java.lang.String s)
public java.io.PrintStream ToStream()
public int getChar()
Saves the output character (if any) in readChars
if
it is non-null. (This is a private debugging aid.)
public int peekChar()
getChar()
, but leaves the character in the stream.
If an I/O error occurs, a fatal error is reported.
public void resetInfo()
In the event of a parsing error (see handleUnexpected(String)
), we use any remembered recent
output to produce a more useful error message.
private void handleReadError(java.io.IOException e)
IOException
resulting from a read on from
into a fatal error.
public void handleUnexpected(java.lang.String wanted)
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.
wanted
- is the output we expected.private static java.lang.String trimNewlines(java.lang.String s)
s
- the string to trim.
s
, but with starting and
ending newline characters removedpublic void checkChar(char c)
c
, a fatal error is reported.
public void checkString(java.lang.String s)
s
- the string to match.public void eatWhitespace()
public java.lang.String readWord(java.lang.String stops)
stops
, or an EOF.
stops
- a string containing all characters on which to
stop reading.
stops
.public int readNumber()
public SList readSList()
SList
from this subprocess. A fatal
error is reported if any errors occur.readSExp()
!public SExp readSExp()
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:
Integer
class. Atom
s are parsed by removing the first and last
characters iff the first character is a '|'. Atom
s
that start with '|' but do not end with a different '|'. For
speed reasons, this limitation may be left in the final
version.public SList readSLists()
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
.
readSExp()
!public SList readSExps(char stop)
stop
- the character that causes reading to stop.
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.
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 |
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | ||||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |