    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.prover;
    004
    005
    006    import java.util.*;
    007
    008    import javafe.util.*;
    009
    010
    011    /**
    012     ** This class is used privately by Simplify to enumerate the list of
    013     ** counter-example contexts found by Simplify to a given verification
    014     ** condition. <p>
    015     **
    016     ** If the enumeration ends with a SimplifyOutput of kind VALID, then
    017     ** Simplify verified the theorem. <p>
    018     **
    019     **
    020     ** This class will eventually be fairly lazy to allow error reporting
    021     ** as each error is found.<p>
    022     **
    023     **
    024     ** Warning: This class uses SubProcess.readSExp(), which does not
    025     ** implement the full grammer for SExps.  See that routine for the
    026     ** exact limitations.<p>
    027     **/
    028
    029    class CECEnum implements Enumeration {
    030
    031        /***************************************************
    032         *                                                 *
    033         * Instance variables:                             *
    034         *                                                 *
    035         ***************************************************/
    036
    037        /**
    038         ** The Simplify subprocess. <p>
    039         **/
    040        private /*@ non_null @*/ final SubProcess P;
    041
    042
    043        /**
    044         ** Is Simplify done processing our verification request? <p>
    045         **
    046         ** If so, all remaining results must be in <code>pending</code>.
    047         ** Otherwise, the remaining results are those in <code>pending</code>
    048         ** followed by the results we have yet to read from Simplify.<p>
    049         **/
    050        //@ spec_public
    051        private boolean simplifyDone = false;
    052
    053        /**
    054         ** The next results we are to return.
    055         **/
    056        //@ invariant pending.elementType == \type(SimplifyOutput);
    057        //@ invariant !pending.containsNull;
    058        //@ spec_public
    059        private final Vector pending = new Vector();
    060
    061
    062        /***************************************************
    063         *                                                 *
    064         * Creation:                                       *
    065         *                                                 *
    066         ***************************************************/
    067
    068        /**
    069         ** Create an Enumeration of the counter-example contexts for
    070         ** expression <code>exp</code> using Simplify process
    071         ** <code>simplify</code>. <p>
    072         **
    073         ** We always return an Enumeration of non-null SimplifyOutput's.
    074         ** If verifying <code>exp</code> succeeds, the resulting Enumeration
    075         ** will end with a SimplifyOutput of kind VALID. <p>
    076         **
    077         ** Precondition: <code>simplify</code> is not closed, and
    078         **               <code>exp</code> is properly formed according to
    079         **               Simplify's rules.<p>
    080         **
    081         ** Note: This routine should be called *only* from class Simplify.<p>
    082         **/
    083        /*package*/ CECEnum(/*@ non_null @*/ SubProcess simplify,
    084                            /*@ non_null @*/ String exp) {
    085            //@ set pending.elementType = \type(SimplifyOutput);
    086            //@ set pending.containsNull = false;
    087
    088            P = simplify;
    089            P.resetInfo();
    090
    091            if (Info.on) {
    092              Info.out("[calling Simplify on '" + exp + "']");
    093            }
    094            P.send(exp);
    095
    096        }
    097
    098        /*package*/ CECEnum(/*@ non_null @*/ SubProcess simplify) {
    099            //@ set pending.elementType = \type(SimplifyOutput);
    100            //@ set pending.containsNull = false;
    101
    102            P = simplify;
    103            P.resetInfo();
    104
    105            if (Info.on) {
    106                Info.out("[calling Simplify on VC stream]");
    107            }
    108        }
    109
    110        /***************************************************
    111         *                                                 *
    112         * Implementing the Enumeration interface:         *
    113         *                                                 *
    114         ***************************************************/
    115
    116        //@ represents moreElements <- !(simplifyDone && pending.elementCount == 0);
    117
    118        //@ invariant_redundantly pending.elementCount > 0 ==> moreElements;
    119        //@ invariant_redundantly moreElements ==> !simplifyDone || pending.elementCount > 0;
    120
    121
    122        /**
    123         ** The type of the elements we return.
    124         **/
    125        //@ invariant elementType==\type(SimplifyOutput);
    126
    127        /**
    128         ** Do we ever return null as an element?
    129         **/
    130        //@ invariant !returnsNull;
    131
    132
    133        /**
    134         ** Returns true iff any more elements exist in this enumeration.
    135         **/
    136        //@ also modifies simplifyDone, pending.elementCount;
    137        //@      ensures \result ==> pending.elementCount>0;
    138        final public boolean hasMoreElements() {
    139            if (pending.size()==0 && !simplifyDone)
    140                readFromSimplify();
    141
    142            return pending.size()!=0;
    143        }
    144
    145        /**
    146         ** Returns the next element of the enumeration. Calls to this
    147         ** method will enumerate successive elements.  Throws
    148         ** NoSuchElementException if no more elements are left.
    149         **/
    150        //@ also modifies simplifyDone;
    151        public Object nextElement() /*throws NoSuchElementException*/ {
    152            if (!hasMoreElements())
    153                throw new NoSuchElementException();
    154
    155            Object result = pending.firstElement();
    156            pending.removeElementAt(0);
    157
    158            if (Info.on) {
    159              Info.out("  [Simplify returned: " + result.toString() + "]");
    160            }
    161
    162            return result;
    163        }
    164
    165
    166        /***************************************************
    167         *                                                 *
    168         * Reading results from Simplify:                  *
    169         *                                                 *
    170         ***************************************************/
    171
    172        /**
    173         ** Ensure that we are done using Simplify.  We promise not to
    174         ** ever use Simplify again after this routine returns.
    175         **/
    176        /*package*/ void finishUsingSimplify() {
    177            while (!simplifyDone)
    178                readFromSimplify();
    179        }
    180
    181
    182        /**
    183         ** Attempt to read another output (for example, a counter-example)
    184         ** from Simplify, then append it to <code>pending</code>.
    185         **/
    186        //@ requires !simplifyDone;
    187        //@ modifies simplifyDone, pending.elementCount;
    188        //@ ensures simplifyDone || pending.elementCount > 0;
    189        private void readFromSimplify() {
    190            P.eatWhitespace();
    191
    192            SimplifyOutput so;
    193            if (Character.isDigit((char)P.peekChar())) {
    194              so = readSentinel();
    195              simplifyDone = true;
    196            } else {
    197              so = readResultMessage();
    198            }
    199            pending.addElement(so);
    200        }
    201
    202        private /*@ non_null @*/ SimplifyOutputSentinel readSentinel() {
    203          int n = P.readNumber();
    204          P.checkString(": ");
    205
    206          int kind;
    207          switch (P.peekChar()) {
    208            case 'V':
    209              P.checkString("Valid.");
    210              kind = SimplifyOutput.VALID;
    211              P.eatWhitespace();
    212              if (P.peekChar() == '(')
    213                    P.checkString("(Added to background predicate).");
    214              break;
    215            case 'I':
    216              P.checkString("Invalid.");
    217              kind = SimplifyOutput.INVALID;
    218              break;
    219            case 'U':
    220              P.checkString("Unknown.");
    221              kind = SimplifyOutput.UNKNOWN;
    222              break;
    223            default:
    224              P.handleUnexpected("'Valid', 'Invalid', or 'Unknown'");
    225              return null;  // dummy return
    226          }
    227          P.eatWhitespace();
    228
    229          return new SimplifyOutputSentinel(kind, n);
    230        }
    231
    232        //@ ensures \result != null;
    233        private SimplifyResult readResultMessage() {
    234          String msg = P.readWord("\n");
    235          P.checkChar('\n');
    236          SimplifyResult result = null;
    237          int kind;
    238          if (msg.startsWith("Counterexample:")) {
    239            kind = SimplifyOutput.COUNTEREXAMPLE;
    240          } else if (msg.startsWith("Exceeded PROVER_KILL_TIME")) {
    241            kind = SimplifyOutput.EXCEEDED_PROVER_KILL_TIME;
    242          } else if (msg.startsWith("Exceeded PROVER_KILL_ITER")) {
    243            kind = SimplifyOutput.EXCEEDED_PROVER_KILL_ITER;
    244          } else if (msg.startsWith("Reached PROVER_CC_LIMIT")) {
    245            kind = SimplifyOutput.REACHED_CC_LIMIT;
    246          } else if (msg.startsWith("Exceeded PROVER_SUBGOAL_KILL_TIME")) {
    247            kind = SimplifyOutput.EXCEEDED_PROVER_SUBGOAL_KILL_TIME;
    248          } else if (msg.startsWith("Exceeded PROVER_SUBGOAL_KILL_ITER")) {
    249            kind = SimplifyOutput.EXCEEDED_PROVER_SUBGOAL_KILL_ITER;
    250          } else if (msg.startsWith("Warning: triggerless quantifier body")) {
    251            SExp e0 = P.readSExp();
    252            P.eatWhitespace();
    253            P.checkString("with ");
    254            int n = P.readNumber();
    255            String restOfLine = P.readWord("\n");
    256            SExp e1 = P.readSExp();
    257            result = new TriggerlessQuantWarning(null, null, e0, n, e1);
    258            kind = result.getKind();
    259          } else {
    260            P.handleUnexpected("result message");
    261            return null;  // dummy return
    262          }
    263
    264          if (result == null) {
    265            result = new SimplifyResult(kind, null, null);
    266          }
    267
    268          P.eatWhitespace();
    269
    270          // Read in the labels, if any
    271          if (P.peekChar() == 'l') {
    272            P.checkString("labels:");
    273            result.labels = P.readSList();
    274            P.eatWhitespace();
    275          }
    276
    277          // Read in the set of counterexample contexts, if present
    278          if (P.peekChar() == 'c') {
    279            P.checkString("context:\n");
    280            result.context = P.readSList();
    281            P.eatWhitespace();
    282          }
    283
    284          return result;
    285        }
    286    }