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    }