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 }