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    }