    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.prover;
    004
    005    import java.io.*;
    006    import java.util.Enumeration;
    007
    008    import javafe.util.*;
    009
    010    /**
    011     * <p> The interface to the Simplify theorem prover program using
    012     * Strings to send and S-expressions to receive. </p>
    013     *
    014     * <p> Note that a Java application will not exit normally (i.e., when
    015     * its <code>main()</code> method returns) until all subprocesses have
    016     * finished.  In particular, this implies that all
    017     * <code>Simplify</code> instances must be closed before this can
    018     * occur.  Alternatively, a Java application can just call
    019     * <code>java.lang.System.exit</code> to force an exit to occur
    020     * without waiting for subprocesses. </p>
    021     *
    022     *
    023     * <p> <strong>Warning:</strong> This class uses {@link
    024     * SubProcess#readSExp()}, which does not implement the full grammer
    025     * for SExps.  See that routine for the exact limitations. </p>
    026     *
    027     * @see SExp
    028     * @see SubProcess
    029     * @see escjava.prover.CECEnum
    030     */
    031
    032    public class Simplify
    033    {
    034        /**
    035         * Our Simplify subprocess; no actions should be taken on this
    036         * subprocess unless {@link #readySubProcess()} is called first.
    037         */
    038        //@ spec_public
    039        private final /*@ non_null @*/ SubProcess P;
    040
    041        //@ invariant P == null ==> closed;
    042
    043        /**
    044         * This variable holds the {@link CECEnum} that is currently using
    045         * Simplify (there can be at most 1 such CECEnum), or
    046         * <code>null</code> if there is no such CECEnum.
    047         *
    048         * <p> Simplify is available for use iff this is
    049         * <code>null</code>.  Use {@link #readySubProcess()} to make
    050         * Simplify available. </p>
    051         */
    052        //@ spec_public
    053        private CECEnum subProcessUser = null;
    054
    055        //@ public model boolean closed;
    056        //@ represents closed <- (P == null);
    057
    058        // Multiplexing Simplify
    059
    060        /**
    061         * Prepare Simplify for use.
    062         *
    063         * <p> Precondition: we are not closed. </p>
    064         *
    065         * <p> Ensures any {@link CECEnum} currently using Simplify
    066         * finishes. </p>
    067         */
    068        //@ requires !closed;
    069        //@ ensures subProcessUser != null ==> subProcessUser == null;
    070        private void readySubProcess() {
    071            if (subProcessUser != null) {
    072                subProcessUser.finishUsingSimplify();
    073                eatPrompt();
    074                subProcessUser = null;
    075            }
    076        }
    077
    078
    079        // Creation and destruction
    080
    081        /**
    082         * Create a new invocation of Simplify as a sub-process.
    083         *
    084         * <p> The resulting invocation is initially open, but may be
    085         * closed permanently with the {@link #close()} method. </p>
    086         *
    087         * <p> This constructor may result in a fatal error if any
    088         * problems occur. </p>
    089         */
    090        //@ ensures !closed;
    091        public Simplify() {
    092            P = new SubProcess("Simplify",
    093                               new String[] {
    094                                   java.lang.System.getProperty("simplify",
    095                                                                "/usr/local/escjava/bin/Simplify"),
    096                                   "-noprune",
    097                                   "-noplunge"}, // FIXME - make controllable
    098                               null);
    099            eatPrompt();
    100        }
    101
    102        /**
    103         * Close us.
    104         *
    105         * <p> This destroys the associated subprocess.  Afterwards, none
    106         * of our methods should ever be called again.  Likewise, no
    107         * methods of any {@link Enumeration} we've returned should ever
    108         * be called again. </p>
    109         *
    110         * <p> This method may result in a fatal error if any problems
    111         * occur.  Our subprocess is guaranteed to be destroyed afterwards,
    112         * regardless of which exit is taken. </p>
    113         */
    114        //@ ensures closed;
    115        public void close() {
    116            P.close();
    117        }
    118
    119
    120        // Client operations
    121
    122        /**
    123         * Send a single <code>String</code> command to Simplify.
    124         *
    125         * <p> A command is something that produces no output other than
    126         * whitespace and a prompt.  If any other output is produced, a
    127         * fatal error will result. </p>
    128         *
    129         * <p> Precondition: we are not closed. </p>
    130         *
    131         * @param s the string containing the command to be sent to
    132         * simplify.
    133         */
    134        //@ requires !closed;
    135        public void sendCommand(/*@ non_null @*/ String s) {
    136            readySubProcess();
    137            P.resetInfo();
    138
    139            if (Info.on) {
    140                Info.out("[calling Simplify with command '" + s + "']");
    141            }
    142
    143            P.send(s);
    144
    145            eatPrompt();
    146
    147            Info.out("[Simplify: command done]");
    148        }
    149
    150
    151        /**
    152         * Send a <code>String</code> containing zero-or-more commands to
    153         * our Simplify subprocess.
    154         *
    155         * <p> A command is something that produces no output other than
    156         * whitespace and a prompt.  If any other output is produced, a
    157         * fatal error will result. </p>
    158         *
    159         * <p> Precondition: we are not closed. </p>
    160         *
    161         * @param s the string containing the commands to be sent to
    162         * simplify.
    163         */
    164        //@ requires !closed;
    165        public void sendCommands(/*@ non_null @*/ String s) {
    166            readySubProcess();
    167            P.resetInfo();
    168
    169            if (Info.on) {
    170                Info.out("[calling Simplify with commands '" + s + "']");
    171            }
    172
    173            P.send(s);
    174
    175            // review kiniry 14 March 2004 - Why is this code block no
    176            // longer necessary?
    177
    178            /*
    179             // this is so we can be sure we have resynchronized the stream:
    180             P.send(" (LBL |<resync>| (EQ |<A>| |<B>|))");
    181
    182             // eat resulting prompts from s:
    183             while (P.peekChar() == '>')
    184             eatPrompt();
    185
    186             // Eat output from synchronization expression:
    187             Enumeration results = prove("");
    188             try {
    189             while (true) {
    190             if (!results.hasMoreElements()) {
    191             // get into exception handling code below
    192             throw new SExpTypeError();
    193             }
    194             SimplifyOutput so = (SimplifyOutput)results.nextElement();
    195             if (so.getKind() == SimplifyOutput.COUNTEREXAMPLE) {
    196             SimplifyResult sr = (SimplifyResult)so;
    197             if (sr.labels.at(0).getAtom().toString().equals("<resync>")) {
    198             // all is well (any remaining results will be eaten
    199             // with the next call to readySubProcess)
    200             break;
    201             }
    202             }
    203             }
    204             } catch (Exception e) {
    205             P.handleUnexpected("to have seen the label <resync>");
    206             }
    207             */
    208
    209            Info.out("[Simplify: commands done]");
    210        }
    211
    212        /**
    213         * Attempt to verify expression <code>exp</code>.
    214         *
    215         * <p> We always return an {@link Enumeration} of
    216         * non-<code>null</code> {@link SimplifyOutput}s.  If verifying
    217         * <code>exp</code> succeeds, the resulting {@link Enumeration}
    218         * will end with a {@link SimplifyOutput} of kind {@link
    219         * SimplifyOutput#VALID}. </p>
    220         *
    221         * <p> Precondition: we are not closed, and <code>exp</code> is
    222         * properly formed according to Simplify's rules. </p>
    223         */
    224        //@ requires !closed;
    225        //@ ensures \result.elementType == \type(SimplifyOutput);
    226        //@ ensures !\result.returnsNull;
    227        public /*@ non_null @*/ Enumeration prove(/*@ non_null @*/ String exp) {
    228            readySubProcess();
    229            subProcessUser = new CECEnum(P, exp);
    230            return subProcessUser;
    231        }
    232
    233        /**
    234         * Readies the simplify subprocess and sets its user to this, but
    235         * send no commands.
    236         */
    237        //@ normal_behavior
    238        //@   modifies subProcessUser;
    239        //@   ensures subProcessUser != null;
    240        public void startProve() {
    241            readySubProcess();
    242            subProcessUser = new CECEnum(P);
    243        }
    244
    245        //@ ensures \result.elementType == \type(SimplifyOutput);
    246        //@ ensures !\result.returnsNull;
    247        public /*@ non_null @*/ Enumeration streamProve() {
    248            P.ToStream().flush();
    249            while (P.peekChar() == '>') {
    250                eatPrompt();
    251            }
    252            return subProcessUser;
    253        }
    254
    255        //@ ensures \result == null <==> closed;
    256        public PrintStream subProcessToStream() {
    257            return P.ToStream();
    258        }
    259
    260
    261        // Utility routines
    262
    263        /**
    264         * Consume the prompt from our Simplify subprocess.  If the next
    265         * output characters are not exactly the prompt (possibly preceeded
    266         * by some whitespace), a fatal error is reported.
    267         *
    268         * <p> Precondition: we are not closed. </p>
    269         */
    270        //@ requires !closed;
    271        //@ requires P != null;
    272        private void eatPrompt() {
    273            P.eatWhitespace();
    274            P.checkChar('>');
    275            P.checkChar('\t');
    276        }
    277
    278
    279        // Test methods
    280
    281        /**
    282         * A simple test routine
    283         */
    284        public static void main(String[] args) throws IOException {
    285            Info.on = true;         // Turn on verbose mode
    286
    287            Simplify S = new Simplify();
    288
    289            exhaust(S.prove("(EQ A B)"));
    290
    291            exhaust(S.prove("(EQ A A)"));
    292
    293            S.sendCommand("(BG_PUSH (EQ B A))");
    294            exhaust(S.prove("(EQ A B)"));
    295            S.sendCommand("(BG_POP)");
    296
    297            exhaust(S.prove("(EQ A B)"));
    298
    299            S.sendCommands("(BG_PUSH (EQ B A)) (BG_POP)");
    300
    301            // The following is not a command and thus should produce
    302            // an error:
    303            try {
    304                S.sendCommand("(EQ A A)");
    305            } finally {
    306                S.close();
    307            }
    308        }
    309
    310        /**
    311         * Force an {@link Enumeration} to compute all of its elements
    312         */
    313        static void exhaust(/*@ non_null @*/ Enumeration n) {
    314            while (n.hasMoreElements())
    315                n.nextElement();
    316        }
    317    }