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 }