    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    }