001 /* 002 * Created on Jan 8, 2005 003 * 004 */ 005 package escjava.translate; 006 007 import java.util.Hashtable; 008 import java.util.Iterator; 009 import java.util.LinkedList; 010 import java.util.List; 011 import java.util.NoSuchElementException; 012 013 import javafe.ast.ASTNode; 014 import javafe.ast.ArrayRefExpr; 015 import javafe.ast.Expr; 016 import javafe.ast.ExprObjectDesignator; 017 import javafe.ast.ExprVec; 018 import javafe.ast.FieldAccess; 019 import javafe.ast.FieldDecl; 020 import javafe.ast.Identifier; 021 import javafe.ast.LiteralExpr; 022 import javafe.ast.ObjectDesignator; 023 import javafe.ast.RoutineDecl; 024 import javafe.ast.SuperObjectDesignator; 025 import javafe.ast.ThisExpr; 026 import javafe.ast.Type; 027 import javafe.ast.TypeDecl; 028 import javafe.ast.TypeObjectDesignator; 029 import javafe.ast.VariableAccess; 030 import javafe.tc.EnvForTypeSig; 031 import javafe.tc.TypeSig; 032 import javafe.util.ErrorSet; 033 import javafe.util.Location; 034 import escjava.Main; 035 import escjava.ast.ArrayRangeRefExpr; 036 import escjava.ast.CondExprModifierPragmaVec; 037 import escjava.ast.EverythingExpr; 038 import escjava.ast.Modifiers; 039 import escjava.ast.ModifiesGroupPragma; 040 import escjava.ast.ModifiesGroupPragmaVec; 041 import escjava.ast.NaryExpr; 042 import escjava.ast.NothingExpr; 043 import escjava.ast.TagConstants; 044 import escjava.ast.WildRefExpr; 045 import escjava.tc.Datagroups; 046 import escjava.tc.FlowInsensitiveChecks; 047 import escjava.tc.TypeCheck; 048 import escjava.tc.Types; 049 050 051 /** 052 * @author David Cok 053 * 054 * This class contains methods for handling frame conditions. 055 * <p> 056 * Note the following about the implementation of Modifies Pragmas. 057 * The desugared frame specifications of a method are contained in a 058 * ModifiesGroupPragmaVec, which is a vector of ModifiesGroupPragma elements. 059 * Each ModifiesGroupPragma instance corresponds to the frame conditions for 060 * a single specification case. Since each specification case of a method 061 * must be independently satisfied, each ModifiesGroupPragma must be 062 * satisfied. 063 * <p> 064 * A ModifiesGroupPragma contains a precondition (the Expr <obj>.precondition) 065 * and a set of CondExprModifierPragma elements in a CondExprModifierPragmaVec. 066 * Each CondExprModifierPragma corresponds to one store-ref location as might 067 * be listed in an assignable clause (e.g. a field, an array reference, 068 * wild-card items such as obj.* or array[*], array ranges such as array[i..j]). 069 * The Expr that is in a CondExprModifierPragma is obsolete. [It used to be 070 * that an assignable clause had an optional conditional expression, but that 071 * has been deprecated.] The list of store-refs in a ModifierGroupPragma is 072 * essentially a union - within a specification case a specifier can list 073 * multiple store-ref locations that may be assigned. A particular assignment 074 * statement will have a lhs which must match one of the store-ref locations 075 * in the ModifiesGroup Pragma, and must do so for each ModifiesGroupPragma 076 * in the ModifiesGroupPragmaVec. 077 * <p> 078 * 079 */ 080 public class Frame { 081 082 /** The Translate instance that owns this instance of Frame */ 083 final private Translate translator; 084 085 /** The value of issueCautions obtained from the Translate owner */ 086 final private boolean issueCautions; 087 088 /** The RoutineDecl whose body is in the process of being translated */ 089 final private RoutineDecl rdCurrent; 090 091 /** The mapping to be used for \old variables to get pre-state values */ 092 final private Hashtable premap; 093 094 /** This holds a value across recursive invocations of methods 095 * within this class; it designates that the object whose field 096 * is being assigned is known to be fresh. 097 */ 098 private boolean pFreshResult = false; 099 100 /** A precomputed Identifier for 'this', to be used in constructing 101 * Expressions. 102 */ 103 static private final Identifier thisId = Identifier.intern("this"); 104 105 /** The constructor of a Frame instance; should be called only from 106 * Translate 107 * @param t The instance of Translate to which this Frame belongs 108 * @param issueCautions Whether to issue Caution messages to the user 109 * @param rdCurrent The RoutineDecl whose body is being translated 110 * @param premap The mapping to pre-state values to be used in translation 111 */ 112 public Frame(Translate t, boolean issueCautions, RoutineDecl rdCurrent, 113 Hashtable premap) { 114 translator = t; 115 this.issueCautions = issueCautions; 116 this.rdCurrent = rdCurrent; 117 this.premap = premap; 118 } 119 120 // These fields are used in the course of generating checks 121 122 /** The kind of expression being checked, e.g. assignment or method call. 123 * Used in the message displayed to the user when the check fails. 124 */ 125 private String kindOfModCheck = "assignment"; 126 127 /** This method returns whether the given field (fd) of the given object 128 * (eod) (which is null if the field is static) is definitely not allowed 129 * to be assigned according to the specs of the current RoutineDecl. By 130 * definitely not allowed, we mean that it can be determined without needing 131 * to prove the truth or falsity of a given expression. For example, if 132 * the FieldDecl is nowhere mentioned in the ModifiesGroupPragma, then it 133 * definitely may not be assigned. In a situation where the assignable 134 * clause contained something like <expr>.field where field matches fd, 135 * then the assignment is allowed if <expr> == eod. But that would have 136 * to be proved: it might be that the assignment is not allowed, if 137 * <expr> != eod, but we don't definitely know for sure. 138 * @param eod The object whose field is being assigned, or null if the field 139 * is static 140 * @param fd The declaration corresponding to the field being assigned. 141 * @return true if it is known without a prover that the field may not be 142 * assigned; false if it may or possibly may be assigned 143 */ 144 public boolean isDefinitelyNotAssignable(Expr eod, FieldDecl fd) { 145 definitelyNotAssignable = true; 146 modifiesCheckFieldHelper(eod, Location.NULL, fd, 147 Location.NULL, null, false, null, null, null); 148 boolean r = definitelyNotAssignable; 149 definitelyNotAssignable = false; 150 return r; 151 } 152 153 /** A private variable used to get information without using the 154 * return value, in support of method isDefinitelylNotAssignable. 155 */ 156 private boolean definitelyNotAssignable = false; 157 158 /** This method generates checks that the field in lhs is allowed to be 159 * assigned according to the specification of the current RoutineDecl 160 * (rdCurrent). This may depend on the object whose field is being 161 * assigned. This is called for both static and instance fields. 162 * @param lhs The expression being assigned to (which will be a field 163 * dereference). 164 * @param callLoc The location of the field access expression (the lhs). 165 * @param fd The location of the declaration of the field being assigned 166 */ 167 void modifiesCheckField(Expr lhs, int callLoc, FieldDecl fd) { 168 kindOfModCheck = "assignment"; 169 // FIXME - I don't think this handles this and super that are not the 170 // prefix. 171 if (!issueCautions) return; 172 // eod is the object part of the FieldAccess, as in an assigment of the 173 // form <eod>.<field> = expr; 174 Expr eod = null; 175 if (lhs instanceof NaryExpr) { 176 eod = (Expr)((NaryExpr)lhs).childAt(2); 177 } else if (lhs instanceof VariableAccess) { 178 // static field 179 // eod stays null 180 } else { 181 ErrorSet.caution(callLoc,"INTERNAL ERROR: Unhandled type of lhs in Frame.modifiesCheckField " 182 + lhs.getClass()); 183 escjava.ast.EscPrettyPrint.inst.println(System.out,lhs); 184 return; 185 } 186 modifiesCheckFieldHelper(eod,callLoc,fd,Location.NULL, 187 null,false,null,null,null); 188 } 189 190 /** This is a helper method to generate checks that a particular 191 * field assignment is allowed by the frame conditions. 192 * @param eod The object owning the field being assigned; null if the field 193 * is static 194 * @param callLoc The location of the field access being assigned to 195 * @param fd The declaration of the field being assigned to 196 * @param calleeLoc The location of the assignment or method call 197 * @param callee_tprecondition The precondition under which the callee might 198 * assign this field; null is equivalent to true 199 * @param genExpr true if an Expr containing the formjula to be checked is 200 * to be returned, false if checks are to be inserted in the code 201 * @param mg the set of specifications against which the assignment of the 202 * field is to be tested 203 * @param thisexpr the expression to be used for 'this' in translating 204 * input expressions, or null if no translation is to be done 205 * @param args the set of variable mappings to be used in translation 206 * @return the expression that must be true to allow the assignment, if 207 * genExpr is true; if genExpr is false, null is returned 208 */ 209 private Expr modifiesCheckFieldHelper(Expr eod, int callLoc, 210 FieldDecl fd, int calleeLoc, 211 Expr callee_tprecondition, boolean genExpr, 212 ModifiesGroupPragmaVec mg, 213 Expr thisexpr, Hashtable args) { 214 215 // We need to create a translated predicate expression that is true 216 // if the lhs is allowed to be modified and false if it is not 217 // allowed to be modified. This will be an OR across each of the 218 // modify pragmas. Each pragma will contribute 219 // - obviously false if it is not the same declaration or same type 220 // - obviously true if is is the same declaration and both have 'this' 221 // as the od and the condition is true 222 // - obviously true (and then no check) if it is modifies everything 223 // with a true condition 224 // - some expression which is the AND of the condition and that 225 // the lhs matches the modifies expression: 226 // fields must have the same object designator 227 // arrays must have the same array expression and same index 228 229 // Loop over each specification case in turn 230 if (mg == null) mg = GetSpec.getCombinedMethodDecl(rdCurrent).modifies; 231 ExprVec eev = ExprVec.make(mg.size()); 232 for (int kk=0; kk<mg.size(); ++kk) { 233 ModifiesGroupPragma mge = mg.elementAt(kk); // The ModifiesGroupPragma 234 // for the current specification case 235 int callerLoc = mge.clauseLoc; // Location of one of the modifies 236 // clauses for this specification case 237 // ev collects assertions - if any one of them is true then the 238 // assignment is allowed; if nothing is in it then it is equivalent 239 // to 'false'; if ev is later set to null it means that a literal 240 // 'true' would have been added, so the composite meaning is true 241 ExprVec ev = ExprVec.make(10); 242 243 // If the field is not a static field, then the assignment is 244 // ok if the owning object is fresh since the pre-state. 245 if (!definitelyNotAssignable && !genExpr && !Modifiers.isStatic(fd.modifiers)) addAllocExpression(ev,eod); 246 // FIXME - why this check on definitelyNotAssignable???? 247 248 // Now iterate over all the store-refs in this specification case, 249 // including store-refs that are in datagroups - we use this 250 // iterator to hide the expansion of the datagroups 251 ModifiesIterator caller_iterator = new ModifiesIterator( 252 rdCurrent.parent,mge.items,true); 253 while (ev != null && caller_iterator.hasNext()) { 254 Object ex = caller_iterator.next(); 255 if (ex instanceof FieldAccess || ex instanceof FieldDecl) { 256 FieldDecl fdd; 257 ObjectDesignator odd; 258 if (ex instanceof FieldAccess) { 259 fdd = ((FieldAccess)ex).decl; 260 odd = ((FieldAccess)ex).od; 261 } else { 262 fdd = (FieldDecl)ex; 263 odd = null; 264 } 265 if (fd == fdd) { 266 // The declaration for the assigned field is the same as the 267 // declaration in the assignable clause 268 if (Modifiers.isStatic(fd.modifiers)) { 269 // The matching declarations are static - so they match. 270 ev = null; 271 } else { 272 // Instance references, so the objects need to be equal in order 273 // for the store-refs to match 274 Expr e1 = eod; 275 Expr e2 = odd instanceof ExprObjectDesignator ? 276 ((ExprObjectDesignator)odd).expr: 277 ThisExpr.make(null,Location.NULL); 278 if ( ((e1 instanceof ThisExpr) || 279 ((e1 instanceof VariableAccess) && 280 ((VariableAccess)e1).id == thisId)) && 281 e2 instanceof ThisExpr) { 282 // The objects references are both 'this' 283 ev = null; 284 } else { 285 // Create a check that the two object references are equal 286 ExprVec evv = ExprVec.make(1); 287 evv.addElement(e2); 288 e1 = eod; 289 e2 = modTranslate(e2,!genExpr,thisexpr,args); 290 Expr e = GC.nary(TagConstants.REFEQ,e1,e2); 291 ev.addElement(e); 292 } 293 } 294 } 295 } else if (ex instanceof ArrayRefExpr) { 296 // skip - not a match 297 } else if (ex instanceof NothingExpr) { 298 // skip - not a match 299 } else if (ex instanceof EverythingExpr) { 300 // anything matches \everything 301 ev = null; 302 } else if (ex instanceof ArrayRangeRefExpr) { 303 // skip - not a match 304 } else if (ex instanceof WildRefExpr) { 305 ObjectDesignator odd = ((WildRefExpr)ex).od; 306 if (odd instanceof TypeObjectDesignator) { 307 if (Modifiers.isStatic(fd.modifiers)) { 308 // A static field reference matches <Type>.* if 309 // the static field is a field of the Type or its subtypes 310 TypeSig t = TypeCheck.inst.getSig(fd.parent); // type in which the field is declared 311 Type tt = ((TypeObjectDesignator)odd).type; 312 if (t == tt || Types.isSubclassOf(tt,t)) { 313 ev = null; 314 } 315 } // If not static then is not a match 316 } else if (odd instanceof ExprObjectDesignator) { 317 if (!Modifiers.isStatic(fd.modifiers)) { 318 // An instance field matches <obj>.* if the 319 // object references are equal 320 Expr e1 = eod; 321 Expr e2 = modTranslate(((ExprObjectDesignator)odd).expr, 322 !genExpr,thisexpr,args); 323 e1 = GC.nary(TagConstants.REFEQ,e1,e2); 324 ev.addElement(e1); 325 } // If not an instance reference then not a match 326 } else { 327 ErrorSet.caution("INTERNAL ERROR: Unhandled ObjectDesignator case in modifiesCheckFieldHelper " + odd.getClass()); 328 escjava.ast.EscPrettyPrint.inst.println(System.out,odd); 329 } 330 } else { 331 ErrorSet.caution("INTERNAL ERROR: Unhandled case in modifiesCheckFieldHelper " + ex.getClass()); 332 escjava.ast.EscPrettyPrint.inst.println(System.out,ex); 333 } 334 } 335 // We have looped over all of the assignable store-refs in the 336 // specification case. If ev is null, there has been a definite 337 // match and the assignment is ok for this case; if ev is empty 338 // then there is no store-ref that is even a possible match; 339 // otherwise the assignment is ok if the disjunction of the contents of ev 340 // is true - and that needs to be proven by the checker. 341 342 // Two conditions 343 // if this method has been called on an assignment, we just have 344 // a callerLoc 345 // if the method has been called on a method call, we have a 346 // calleeLoc and a callerLoc and we want the calleeLoc to be 347 // the first associated location 348 349 // definitelyNotAssignable must be true on return if there is any 350 // specification case that does not allow the assignment 351 352 if (definitelyNotAssignable) { 353 //TrAnExpr.closeForClause(); 354 // FIXME - why don't we check the preconditions here 355 if (ev != null && ev.size() == 0) return null; 356 357 } else { 358 359 Expr e = modChecksComplete(mge.precondition, 360 callee_tprecondition,ev,callLoc, 361 calleeLoc==Location.NULL ? callerLoc : calleeLoc, 362 calleeLoc==Location.NULL ? Location.NULL: callerLoc, genExpr); 363 if (genExpr && ev != null) eev.addElement(e); 364 } 365 } 366 definitelyNotAssignable = false; 367 return !genExpr ? null : eev.size() == 0 ? null : GC.and(eev); 368 } 369 370 /* Implementation note on frame conditions when methods are called. 371 * 372 * We have frame conditions for the callee. Any store-ref that 373 * might be assigned by the callee at this point in the program 374 * must be allowed to be assigned by the caller. So we iterate 375 * over each store-ref in each ModifiesGroupPragma in each 376 * specification case of the callee, testing to see whether that 377 * store-ref is allowed to be assigned by the caller. 378 * <p> 379 * There are a couple wrinkles. First, there is a callee_precondition 380 * that states under what circumstances the callee's store-ref might 381 * possibly be assigned. Only if that is true does the store-ref need 382 * to be assignable by the caller. 383 * <p> 384 * Second, just because a store-ref is listed as assignable in a spec case 385 * of the callee does not mean that the callee is actually allowed to assign 386 * to it. Such assignment may be precluded by another spec case of the callee. 387 * For example, given 388 * <pre> 389 requires P; 390 modifies i,j; 391 also 392 requires Q; 393 modifies i,k; 394 </pre> 395 * j may be assigned only if P && !Q, since if Q is true only 396 * i and k, but not j may be assigned. Thus we have to test each store-ref 397 * of the callee against all of the spec cases of its own specification. 398 */ 399 400 /** This method generates checks that the locations possibly assigned by 401 * a called method are allowed to be assigned by the caller. 402 * @param calleeFrameConditions the frame conditions of the callee 403 * @param eod the receiver object of the call 404 * @param loccall the location of the call 405 * @param args the mapping of the arguments of the call 406 * @param freshResult - true if eod is known to be fresh since the prestate 407 * @param td_callee The TypeDecl in which the called method is declared 408 */ 409 void modifiesCheckMethodI(ModifiesGroupPragmaVec calleeFrameConditions, 410 Expr eod, int loccall, Hashtable args, boolean freshResult, 411 TypeDecl td_callee) { 412 if (!issueCautions) return; 413 kindOfModCheck = "method call"; 414 for (int i=0; i<calleeFrameConditions.size(); ++i) { 415 ModifiesGroupPragma mg = calleeFrameConditions.elementAt(i); 416 // FIXME - the precondition should not be null - guarding against bugs 417 // upstream - e.g. current ArcType, but that may be because of model type problems 418 if (mg.precondition == null) { 419 //System.out.println("ADDING LIT " + Location.toString(mg.clauseLoc)); 420 mg.precondition = LiteralExpr.make(TagConstants.BOOLEANLIT, 421 Boolean.TRUE, Location.NULL); 422 javafe.tc.FlowInsensitiveChecks.setType(mg.precondition,Types.booleanType); 423 } 424 Expr tp = modTranslate(mg.precondition,false,eod,args); 425 ModifiesIterator callee_iterator = new ModifiesIterator(td_callee,mg.items,false); 426 while (callee_iterator.hasNext()) { 427 Object ex = callee_iterator.next(); 428 Expr e = modifiesCheckMethod(eod, Location.NULL, 429 args, false, 430 ex, 431 tp,true,calleeFrameConditions); 432 if (e == GC.falselit) { 433 continue; 434 } 435 436 ModifiesGroupPragmaVec mge = GetSpec.getCombinedMethodDecl(rdCurrent).modifies; 437 modifiesCheckMethod(eod, loccall, 438 args, freshResult, 439 ex, 440 e == null ? tp : GC.and(tp,e),false,mge); 441 } 442 } 443 } 444 445 /** 446 * Helper method that checks that a particular store-ref in 447 * the frame conditions of a 448 * called method against the frame conditions of the caller. 449 * 450 * @param eod The receiver object of the called method 451 * @param loccall The location of the call 452 * @param args The mapping to be used for callee variables 453 * @param freshResult true if the receiver is known to be fresh (allocated 454 * since the pre-state of the caller) 455 * @param calleeStoreRef the store-ref of the callee to check 456 * @param callee_tprecondition The precondition of the store-ref under investigation 457 * @param genExpr if true, an expression is returned that must be true to allow 458 * the store-ref; if false, a check is created and null is returned 459 * @param mg the caller frame conditions against which to check 460 * @return if genExpr is true, the expression that constitutes the condition 461 * that must be true if the frame condition is to be allowed is returned; 462 * if genExpr is false, null is returned (a assertion check is inserted into 463 * the generated guarded commands) 464 */ 465 private Expr modifiesCheckMethod(Expr eod, int loccall, 466 Hashtable args, 467 boolean freshResult, 468 Object calleeStoreRef, 469 Expr callee_tprecondition, boolean genExpr, 470 ModifiesGroupPragmaVec mg) { 471 472 int calleeLoc = ((ASTNode)calleeStoreRef).getStartLoc(); 473 pFreshResult = freshResult; 474 ExprVec eev = ExprVec.make(mg.size()); 475 try { 476 // Iterating over specification cases 477 for (int kk=0; kk<mg.size(); ++kk) { 478 // Check that ex is assignable for each specification case 479 // in the caller. Need to issue an error if ex is not assignable; 480 // need to issue a check to be proven if it might or might not be 481 // assignable; can skip the iteration if ex is definitely assignable 482 ModifiesGroupPragma mge = mg.elementAt(kk); 483 int callerLoc = mge.getStartLoc(); 484 ExprVec ev = ExprVec.make(10); 485 486 if (calleeStoreRef instanceof EverythingExpr) { 487 ModifiesIterator caller_iterator = new ModifiesIterator( 488 rdCurrent.parent,mge.items,true); 489 while (caller_iterator.hasNext()) { 490 Object callerStoreRef = caller_iterator.next(); 491 if (callerStoreRef instanceof EverythingExpr) { 492 // calleeStoreRef is \everything but there is also an \everything in 493 // the caller, so there is a match 494 ev = null; 495 break; 496 } 497 } 498 } else if (calleeStoreRef instanceof NothingExpr) { 499 ev = null; // Anything in the caller will match 500 } else if (calleeStoreRef instanceof FieldAccess) { 501 FieldAccess fa = (FieldAccess)calleeStoreRef; 502 Expr eeod = (fa.od instanceof ExprObjectDesignator) ? 503 ((ExprObjectDesignator)fa.od).expr : null; 504 Expr lval = eeod == null ? null 505 : modTranslate(eeod, false, eod, args); 506 507 Expr e = modifiesCheckFieldHelper(lval,loccall, fa.decl, calleeLoc, 508 callee_tprecondition,genExpr,mg,eod,args); 509 if (genExpr && e != null) eev.addElement(e); 510 // A bit of a hack - the FieldHelper routine iterates over 511 // all of the caller frame conditions, so we short-circuit 512 // that here. Skip the modChecksComplete at the end as well. 513 break; 514 } else if (calleeStoreRef instanceof ArrayRefExpr) { 515 Expr array= modTranslate(((ArrayRefExpr)calleeStoreRef).array, false, eod, args ); 516 Expr index= modTranslate(((ArrayRefExpr)calleeStoreRef).index, false, eod, args ); 517 modifiesCheckArray(array,index,loccall,calleeLoc, callee_tprecondition, 518 genExpr,mg,eod,args); 519 // A bit of a hack - the helper routine iterates over 520 // all of the caller frame conditions, so we short-circuit 521 // that here. Skip the modChecksComplete at the end as well. 522 break; 523 } else if (calleeStoreRef instanceof WildRefExpr) { 524 ObjectDesignator odd = ((WildRefExpr)calleeStoreRef).od; 525 Expr e1 = null; 526 if (odd instanceof ExprObjectDesignator) { 527 e1 = modTranslate(((ExprObjectDesignator)odd).expr, 528 false,eod,args); 529 if (!genExpr) addAllocExpression(ev,e1); 530 } 531 ModifiesIterator caller_iterator = new ModifiesIterator( 532 rdCurrent.parent,mge.items,true); 533 while (caller_iterator.hasNext()) { 534 Object callerStoreRef = caller_iterator.next(); 535 //System.out.println("CALLER " + callerStoreRef); 536 if (callerStoreRef instanceof EverythingExpr) { 537 ev = null; 538 break; 539 } else if (callerStoreRef instanceof WildRefExpr) { 540 ObjectDesignator oddd = ((WildRefExpr)callerStoreRef).od; 541 if ((odd instanceof TypeObjectDesignator) && (oddd instanceof TypeObjectDesignator)) { 542 Type t = ((TypeObjectDesignator)odd).type; 543 Type tt = ((TypeObjectDesignator)oddd).type; 544 if (t == tt || ((t instanceof TypeSig) && Types.isSubclassOf(tt,(TypeSig)t)) ) { 545 ev = null; 546 break; 547 } 548 } else if (odd instanceof ExprObjectDesignator && oddd instanceof ExprObjectDesignator) { 549 Expr e2 = modTranslate(((ExprObjectDesignator)oddd).expr, 550 !genExpr, eod, args); 551 e1 = GC.nary(TagConstants.REFEQ,e1,e2); 552 ev.addElement(e1); 553 } else if (odd instanceof SuperObjectDesignator || oddd instanceof SuperObjectDesignator) { 554 ErrorSet.caution("INTERNAL ERROR: Unhandled ObjectDesignator in Frame.modifiesCheckMethod: " + odd.getClass()); 555 } 556 } 557 } 558 } else if (calleeStoreRef instanceof ArrayRangeRefExpr) { 559 ArrayRangeRefExpr aexpr = (ArrayRangeRefExpr)calleeStoreRef; 560 Expr array = aexpr.array; 561 Expr lowIndex = aexpr.lowIndex; 562 Expr highIndex = aexpr.highIndex; 563 Expr ao = modTranslate(array,false,eod,args); 564 Expr al = lowIndex == null ? null : 565 modTranslate(lowIndex,false,eod,args); 566 Expr ah = highIndex == null ? null : 567 modTranslate(highIndex,false,eod,args); 568 if (!genExpr) addAllocExpression(ev,ao); 569 ModifiesIterator caller_iterator = new ModifiesIterator( 570 rdCurrent.parent,mge.items,true); 571 while (caller_iterator.hasNext()) { 572 Object callerStoreRef = caller_iterator.next(); 573 if (callerStoreRef instanceof EverythingExpr) { 574 ev = null; 575 } else if (callerStoreRef instanceof ArrayRangeRefExpr) { 576 ArrayRangeRefExpr aaexpr = (ArrayRangeRefExpr)callerStoreRef; 577 Expr aarray = aaexpr.array; 578 Expr alowIndex = aaexpr.lowIndex; 579 Expr ahighIndex = aaexpr.highIndex; 580 Expr aao = modTranslate(aarray,!genExpr,eod,args); 581 Expr aal = alowIndex == null ? null : 582 modTranslate(alowIndex,!genExpr,eod,args); 583 Expr aah = ahighIndex == null ? null : 584 modTranslate(ahighIndex,!genExpr,eod,args); 585 // ao, aao are the callee/caller array expressions 586 // al, aal are the callee/caller low index expressions, or 587 // null if the low index is not specified 588 // ah, aah are the callee/caller high index expressions, or 589 // null if the high index is not specified 590 // All expressions are already translated 591 // We need to have the array expressions be equal 592 // AND aal <= al AND ah <= aah 593 // A null low index is equivalent to 0 594 // A null high index is equivalent to the length-1 595 // (since the arrays have to be the same, the lengths can be 596 // presumed to be the same) 597 if (ah == null && aah != null) continue; // FIXME - could compare against the length of ao 598 aao = GC.nary(TagConstants.REFEQ,ao,aao); 599 aal = aal == null ? null : 600 GC.nary(TagConstants.INTEGRALLE,aal, 601 al != null ? al: GC.zerolit); 602 aah = aah == null ? null : 603 GC.nary(TagConstants.INTEGRALLE,ah,aah); 604 aal = aal == null ? aah : aah == null ? aal : GC.and(aal,aah); 605 aao = aal == null ? aao : GC.and(aao,aal); 606 ev.addElement(aao); 607 } else if (callerStoreRef instanceof ArrayRefExpr) { 608 // Here the callee is an array range; 609 // the caller is an array element; they match if 610 // the range is just the single element. 611 // FIXME: Note that we don't find matches of a 612 // callee array range against the corresponding list 613 // of individual array elements in the caller (or against 614 // a list of caller array range store refs that when 615 // combined match the callee) 616 if (ah == null) continue; // FIXME - could compare against the length of ao 617 ArrayRefExpr aaexpr = (ArrayRefExpr)callerStoreRef; 618 Expr aarray = aaexpr.array; 619 Expr aindex = aaexpr.index; 620 Expr aao = modTranslate(aarray,!genExpr,eod,args); 621 aindex = modTranslate(aindex,!genExpr,eod,args); 622 aao = GC.nary(TagConstants.REFEQ,ao,aao); 623 Expr aal = GC.nary(TagConstants.INTEGRALLE,aindex, 624 al != null ? al: GC.zerolit); 625 Expr aah = GC.nary(TagConstants.INTEGRALLE,ah,aindex); 626 aal = GC.and(aal,aah); 627 aao = GC.and(aao,aal); 628 ev.addElement(aao); 629 } 630 } 631 } else { 632 // Leaving ev empty is equivalent to false 633 ErrorSet.caution("INTERNAL ERROR: Modifies Check not implemented for " + calleeStoreRef.getClass()); 634 } 635 Expr e = modChecksComplete(mge.precondition,callee_tprecondition,ev, 636 loccall,calleeLoc,callerLoc,genExpr); 637 if (genExpr && e != null) eev.addElement(e); 638 } // end of iterating over spec cases 639 } finally { 640 pFreshResult = false; 641 } 642 return !genExpr ? null : eev.size() == 0 ? null : GC.and(eev); 643 } 644 645 646 /** This adds checks for whether the given array with the given 647 * index may be assigned to. 648 * 649 * @param array the array object whose element is being assigned 650 * @param arrayIndex the index of the elemtn being assigned 651 * @param callLoc the location of the assignment 652 */ 653 void modifiesCheckArray(Expr array, Expr arrayIndex, int callLoc) { 654 if (!issueCautions) return; 655 kindOfModCheck = "assignment"; 656 modifiesCheckArray(array,arrayIndex,callLoc,Location.NULL,null,false,null,null,null); 657 } 658 659 /** This adds checks for whether the given array with the given 660 * index may be assigned to. 661 * 662 * @param array the array object whose element is being assigned 663 * @param arrayIndex the index of the elemtn being assigned 664 * @param callLoc the location of the assignment 665 * @param calleeLoc 666 * @param callee_tprecondition The precondition under which the callee might 667 * assign this array element; null is equivalent to true 668 * @param genExpr true if an Expr containing the formula to be checked is 669 * to be returned, false if checks are to be inserted in the code 670 * @param mg the set of specifications against which the assignment of the 671 * field is to be tested 672 * @param thisexpr the expression to be used for 'this' in translating 673 * input expressions, or null if no translation is to be done 674 * @param args the set of variable mappings to be used in translation 675 * @return the expression that must be true to allow the assignment, if 676 * genExpr is true; if genExpr is false, null is returned 677 */ 678 private Expr modifiesCheckArray(Expr array, Expr arrayIndex, 679 int callLoc, int calleeLoc, 680 Expr callee_tprecondition, 681 boolean genExpr, ModifiesGroupPragmaVec mg, 682 Expr thisexpr, Hashtable args) { 683 684 if (mg == null) mg = GetSpec.getCombinedMethodDecl(rdCurrent).modifies; 685 ExprVec eev = ExprVec.make(mg.size()); 686 687 // FIXME - I don't think this handles this and super that are not the 688 // prefix. 689 690 // We need to create a translated predicate expression that is true 691 // if the lhs is allowed to be modified and false if it is not 692 // allowed to be modified. Each specification case must be 693 // satisfied. Within a specification case there will be an OR across 694 // each of the store-ref expressions within the ModifiesGroupPragma 695 // Each store-ref expression will contribute 696 // - obviously false if it is not the same declaration or same type 697 // - obviously true in some cases, such as if the store-ref location 698 // is \everything 699 // - some expression which is the AND of the condition and that 700 // the lhs matches the modifies expression: 701 // fields must have the same object designator 702 // arrays must have the same array expression and same index 703 704 for (int kk=0; kk<mg.size(); ++kk) { 705 ModifiesGroupPragma mge = mg.elementAt(kk); 706 int callerLoc = mge.clauseLoc; 707 // The composite condition is the OR of everything in ev. 708 // This is false if there is nothing in ev. 709 // ev is set to null if a literal TRUE would be added 710 ExprVec ev = ExprVec.make(10); 711 // The assignment is ok if the array whose element is assigned 712 // is fresh since the prestate 713 if (!genExpr) addAllocExpression(ev,array); 714 ModifiesIterator caller_iterator = new ModifiesIterator( 715 rdCurrent.parent,mge.items,true); 716 while (ev != null && caller_iterator.hasNext()) { 717 Object ex = caller_iterator.next(); 718 if (ex instanceof FieldAccess) { 719 // skip - no match 720 } else if (ex instanceof FieldDecl) { 721 // skip - no match 722 } else if (ex instanceof ArrayRefExpr) { 723 if (array != null) { // FIXME - why would array be null? 724 Expr ao = ((ArrayRefExpr)ex).array; 725 Expr ai = ((ArrayRefExpr)ex).index; 726 ao = modTranslate(ao,!genExpr,thisexpr,args); 727 ai = modTranslate(ai,!genExpr,thisexpr,args); 728 ao = GC.nary(TagConstants.REFEQ,array,ao); 729 ai = GC.nary(TagConstants.INTEGRALEQ,arrayIndex,ai); 730 ao = GC.and(ao,ai); 731 ev.addElement(ao); 732 } 733 } else if (ex instanceof NothingExpr) { 734 // skip - no match 735 } else if (ex instanceof EverythingExpr) { 736 ev = null; 737 } else if (ex instanceof ArrayRangeRefExpr) { 738 if (array != null) { // FIXME - why would array be null? 739 ArrayRangeRefExpr a = (ArrayRangeRefExpr)ex; 740 Expr ao = modTranslate(a.array,!genExpr,thisexpr,args); 741 Expr al = a.lowIndex == null ? null : 742 modTranslate(a.lowIndex,!genExpr,thisexpr,args); 743 Expr ah = a.highIndex == null ? null : 744 modTranslate(a.highIndex,!genExpr,thisexpr,args); 745 ao = GC.nary(TagConstants.REFEQ,array,ao); 746 al = al == null ? null : 747 GC.nary(TagConstants.INTEGRALLE,al,arrayIndex); 748 ah = ah == null ? null : 749 GC.nary(TagConstants.INTEGRALLE,arrayIndex,ah); 750 al = al == null ? ah : ah == null ? al : 751 GC.and(al,ah); 752 ao = al == null ? ao : GC.and(ao,al); 753 ev.addElement(ao); 754 } 755 } else if (ex instanceof WildRefExpr) { 756 // skip - an array reference does not match against a <obj>.* 757 } else { 758 ErrorSet.caution("INTERNAL ERROR: Unhandled store-ref type in Frame.modifiesCheckArray: " + ex.getClass()); 759 } 760 } 761 if (ev != null) { 762 Expr e = modChecksComplete(mge.precondition, 763 callee_tprecondition,ev,callLoc, 764 calleeLoc==Location.NULL ? callerLoc : calleeLoc, 765 calleeLoc==Location.NULL ? Location.NULL: callerLoc,genExpr); 766 if (genExpr && ev != null) eev.addElement(e); 767 } 768 } 769 return !genExpr ? null : eev.size() == 0 ? null : GC.and(eev); 770 } 771 772 773 /** Adds an expression into ev stating that e is allocated now but was 774 * not allocated in the pre-state. No expression is added to ev if it 775 * is definitely false that e is fresh - such as if e is this or is null 776 * (meaning the field is static). Otherwise if pFreshResult is true, 777 * a literal True expression is added. Otherwise some non-trivial 778 * expression is added. 779 * <p> 780 * Also uses pFreshResult, which must be true iff e is known to be fresh 781 * since the prestate. 782 * @param ev A vector to accumulate assertions 783 * @param e An expression to be tested for freshness 784 */ 785 private void addAllocExpression(ExprVec ev, Expr e) { 786 if (e == null) return; 787 if (e instanceof ThisExpr) return; 788 if ((e instanceof VariableAccess) && 789 (((VariableAccess)e).id == thisId)) return; 790 if (pFreshResult) { 791 ev.addElement(GC.truelit); 792 return; 793 } 794 ev.addElement ( 795 GC.and( 796 GC.nary(TagConstants.ISALLOCATED,e, 797 TrAnExpr.trSpecExpr(GC.allocvar)), 798 GC.not(GC.nary(TagConstants.ISALLOCATED,e, 799 TrAnExpr.trSpecExpr(GC.allocvar,premap,premap))) 800 ) 801 ); 802 } 803 804 /** 805 * Generates the actual check with the condition 806 * 'if (precondition && tprecond2) then (disjunction of ev)' 807 * 808 * @param precondition A precondition, not yet translated 809 * @param tprecond2 A second, already translated, precondition 810 * (possibly null, meaning true) 811 * @param ev Disjunction of conditions to be proven; an empty list means false 812 * @param callLoc Location of the assignment statement or method call 813 * @param aloc First associated location, possibly null 814 * @param aloc2 Second associated location, possibly null 815 * @param genExpr if true, returns an Expr that must be true; 816 * if false, creates a check for that expression and 817 * returns null 818 * @return The expr to be proved true, if genExpr is true; if 819 * genExpr is false, returns null 820 */ 821 private Expr modChecksComplete( 822 /*@ non_null */ Expr precondition, 823 Expr tprecond2, 824 ExprVec ev, 825 int callLoc, int aloc, int aloc2, boolean genExpr) { 826 if (ev == null) { 827 // always true, so we don't need to prove anything 828 return genExpr ? GC.truelit : null; 829 } 830 831 boolean genCheck = true; 832 833 // Check to see if the modifies check is disabled in general or 834 // for the callLoc or aloc lines - if so just exit 835 if (!genExpr && NoWarn.getChkStatus(TagConstants.CHKMODIFIES,callLoc,aloc==Location.NULL?callLoc:aloc) 836 != TagConstants.CHK_AS_ASSERT) { 837 TrAnExpr.closeForClause(); 838 genCheck = false; 839 } 840 // If aloc2 is not null, check to see if the warning is disabled for that 841 // line - if so just exit 842 if (aloc2 != Location.NULL && !genExpr) { 843 if (NoWarn.getChkStatus(TagConstants.CHKMODIFIES,callLoc,aloc2) 844 != TagConstants.CHK_AS_ASSERT) { 845 TrAnExpr.closeForClause(); 846 genCheck = false; 847 } 848 } 849 if (!genExpr && !genCheck) return null; 850 851 Expr tprecondition = modTranslate(precondition,true,null,null); // FIXME!!! 852 if (tprecond2 != null && !isTrueLiteral(tprecond2)) { 853 tprecondition = GC.and(tprecondition, tprecond2); 854 } 855 856 Expr expr = 857 ev.size() != 0 ? GC.implies(tprecondition,GC.or(ev)) : 858 !isTrueLiteral(tprecondition) ? GC.not(tprecondition) : 859 GC.falselit; 860 if (genExpr) { 861 // skip generating checks 862 } else if (expr == GC.falselit) { 863 // We need to prove (false), which we know without 864 // benefit of the prover is false - so we immediately issue 865 // an error 866 if (aloc == TagConstants.NULL) { 867 ErrorSet.error(callLoc, 868 "There is no assignable clause allowing this " + 869 kindOfModCheck); 870 } else { 871 ErrorSet.error(callLoc, 872 "There is no assignable clause allowing this " 873 + kindOfModCheck,aloc); 874 } 875 if (aloc2 != Location.NULL) ErrorSet.assocLoc(aloc2); 876 } else if (aloc == Location.NULL) { 877 //System.out.println("Generating a modifies check " + ev.size()); 878 translator.addNewAssumptionsNow(); 879 translator.addCheck(callLoc,TagConstants.CHKMODIFIES, 880 expr); 881 } else { 882 //System.out.println("Generating a modifies check " + ev.size()); 883 translator.addNewAssumptionsNow(); 884 translator.addCheck(callLoc,TagConstants.CHKMODIFIES, 885 expr, 886 aloc,aloc2); 887 // FIXME - could also include a list of locations from the caller modifies group 888 } 889 TrAnExpr.closeForClause(); 890 return genExpr ? expr : null; 891 } 892 893 /** Translates the Expr e into guarded commands:<BR> 894 * if old is true, uses the premap to map variables 895 * if old is false, uses args as the variable mapping 896 * 897 * @param e the Expr to translate 898 * @param old if true, translates in the context of the pre-state (using the 899 * mapping in the class field 'premap' 900 * @param thisexpr the Expr to use for 'this' 901 * @param args the mapping to use if old is false (if args is not null) 902 * @return the translated expression 903 */ 904 private Expr modTranslate( 905 /*@ non_null */Expr e, 906 boolean old, 907 Expr thisexpr, 908 Hashtable args) { 909 TrAnExpr.initForClause(true); 910 if (old) return TrAnExpr.trSpecExpr(e,premap,premap,null); 911 else if (args == null) return TrAnExpr.trSpecExpr(e,thisexpr); 912 else return TrAnExpr.trSpecExpr(e,args,args,thisexpr); 913 } 914 915 /** A utility function that returns true if the argument 916 * expression is null or strictly equal to a boolean TRUE. 917 * 918 * @param p The expression to be tested 919 * @return true if the argument is null or a Boolean LiteralExpr 920 * with value true 921 */ 922 private boolean isTrueLiteral(Expr p) { 923 if (p == null) return true; 924 if (!(p instanceof LiteralExpr)) return false; 925 LiteralExpr lit = (LiteralExpr)p; 926 if (lit.getTag() != TagConstants.BOOLEANLIT) return false; 927 Object value = lit.value; 928 return ((Boolean)value).booleanValue() ; 929 } 930 931 /** This class enables iterating over the set of store-ref 932 * locations in a ModifiesGroupPragma. It also has the ability 933 * to include in the iteration the contents of datagroups that 934 * are part of the set of store-ref locations. 935 * 936 * @author David Cok 937 * 938 */ 939 static class ModifiesIterator { 940 941 /** The TypeDecl whose view of any datagroups is to be used.*/ 942 final private TypeDecl td; 943 944 /** The set of store-ref locations over which to iterate. */ 945 final private CondExprModifierPragmaVec mp; 946 947 /** Fields that have yet to be iterated over. This 948 * is a list of FieldAccess objects. */ 949 final private List others = new LinkedList(); 950 951 /** The datagroups that have already been expanded */ 952 final private List done = new LinkedList(); 953 954 /** If true, then datagroups are expanded and their contents 955 * made part of the iteration. 956 */ 957 final private boolean expandDatagroups; 958 959 /** If true, then field wild card store refs (obj.* and 960 * Type.*) are expanded and their contents made part of the 961 * iteration. 962 */ 963 final private boolean expandWild; 964 965 /** An array index into mp */ 966 private int i = 0; 967 968 /** Creates an iterator over the store-ref locations in 969 * the CondExprModifierPragmaVec. The expandWild parameter 970 * is set false. 971 * @param mp The set of store-ref locations over which to 972 * iterate 973 * @param expandDatagroups if true, then datagroups are 974 * expanded and their contents (recursively) become 975 * steps in the iteration 976 */ 977 public ModifiesIterator(TypeDecl td, 978 CondExprModifierPragmaVec mp, boolean expandDatagroups) { 979 this(td,mp,expandDatagroups,false); 980 } 981 982 983 /** Creates an iterator over the store-ref locations in 984 * the CondExprModifierPragmaVec. 985 * @param mp The set of store-ref locations over which to 986 * iterate 987 * @param expandDatagroups if true, then datagroups are 988 * expanded and their contents (recursively) become 989 * steps in the iteration 990 * @param expandWild if true, then store-ref expressions 991 * of the form obj.* are expanded into their 992 * individual fields 993 */ 994 public ModifiesIterator(TypeDecl td, CondExprModifierPragmaVec mp, 995 boolean expandDatagroups, boolean expandWild) { 996 this.td = td; 997 this.mp = mp; 998 this.expandDatagroups = expandDatagroups; 999 this.expandWild = expandWild; 1000 i = 0; 1001 } 1002 1003 /** Resets the iteration back to the beginning */ 1004 public void reset() { 1005 i = 0; 1006 others.clear(); 1007 done.clear(); 1008 } 1009 1010 /** Returns true if there is more to the iteration 1011 * @return true if there is more to the iteration 1012 */ 1013 public boolean hasNext() { 1014 return i < mp.size() || !others.isEmpty(); 1015 } 1016 1017 /** Returns the next element of the iteration; only valid 1018 * if hasNext returns true, otherwise throws an exception 1019 * @return the next element of the iteration 1020 * @throws NoSuchElementException if there are no more elements 1021 * in the iteration 1022 */ 1023 public Object next() throws NoSuchElementException { 1024 Object ex; 1025 if (!others.isEmpty()) { 1026 ex = others.remove(0); 1027 } else if (i >= mp.size()) { 1028 throw new NoSuchElementException(); 1029 } else { 1030 ex = mp.elementAt(i).expr; 1031 ++i; 1032 done.clear(); 1033 } 1034 if (ex instanceof FieldAccess) { 1035 if (expandDatagroups) add(((FieldAccess)ex).od,((FieldAccess)ex).decl); 1036 } else if (expandWild && (ex instanceof WildRefExpr)) { 1037 //System.out.println("EXPANDING " + Location.toString(((WildRefExpr)ex).getStartLoc())); 1038 ObjectDesignator od = ((WildRefExpr)ex).od; 1039 addFields(od); 1040 } 1041 1042 return ex; 1043 } 1044 1045 /** The maximum number of times to unroll a maps reference. */ 1046 private int limit = Main.options().mapsUnrollCount; 1047 // FIXME - should find a better way of testing than using a limited unrolling 1048 1049 /** Adds all the fields of the od (whether it is a type 1050 * or an object) into the 'others' list as FieldAccess 1051 * items. 1052 * @param od 1053 */ 1054 private void addFields(ObjectDesignator od) { 1055 Type type; 1056 boolean stat; 1057 if (od instanceof TypeObjectDesignator) { 1058 type = ((TypeObjectDesignator)od).type; 1059 stat = true; 1060 } else if (od instanceof ExprObjectDesignator) { 1061 type = TypeCheck.inst.getType(((ExprObjectDesignator)od).expr); 1062 stat = false; 1063 } else { 1064 ErrorSet.caution("INTERNAL ERROR: Unhandled ObjectDesignator (od) in ModifiesIterator.addFields: " + od.getClass()); 1065 return; 1066 } 1067 if (type instanceof javafe.tc.TypeSig) { 1068 TypeSig ts = (TypeSig)type; 1069 EnvForTypeSig env; 1070 if (stat) 1071 env = (EnvForTypeSig)FlowInsensitiveChecks.staticenvDecoration.get(ts.getTypeDecl()); 1072 else 1073 env = (EnvForTypeSig)FlowInsensitiveChecks.envDecoration.get(ts.getTypeDecl()); 1074 if (env == null) env = ((TypeSig)type).getEnv(stat); 1075 // The true in the following means all fields are gotten, 1076 // whether or not they are visible or inherited. 1077 // It does also return ghost and model fields. 1078 javafe.ast.FieldDeclVec fds = env.getFields(true); 1079 for (int i=0; i<fds.size(); ++i) { 1080 FieldDecl fd = fds.elementAt(i); 1081 if (stat != Modifiers.isStatic(fd.modifiers)) continue; 1082 FieldAccess fa = FieldAccess.make(od,fd.id,Location.NULL); 1083 fa.decl = fd; 1084 fa = (FieldAccess)javafe.tc.FlowInsensitiveChecks.setType(fa,fd.type); 1085 others.add(fa); 1086 //System.out.println("ADDING " + fd.id + " " + fd.type); 1087 } 1088 } else { 1089 ErrorSet.caution("INTERNAL ERROR: Unhandled Type in ModifiesIterator.addFields: " + type.getClass()); 1090 } 1091 } 1092 1093 /** Adds the contents of the datagroup d (of object od, which 1094 * may not be null) to the 'others' list. 1095 * @param od Object reference 1096 * @param d Declaration of the datagroup 1097 */ 1098 //@ requires od != null && d != null; 1099 private void add(ObjectDesignator od, FieldDecl d) { 1100 if (count(d) >= limit) return; 1101 done.add(d); 1102 if (od == null) { 1103 System.out.println("UNSUPPORTED OPTION IN FRAME.ModifiesIterator"); 1104 others.addAll(Datagroups.get(td,d)); 1105 } else if (od instanceof TypeObjectDesignator) { 1106 TypeSig ts = (TypeSig)((TypeObjectDesignator)od).type; 1107 TypeDecl tdd = ts.getTypeDecl(); 1108 if (TypeSig.getSig(td).isSubtypeOf(ts)) tdd = td; 1109 others.addAll(Datagroups.get(tdd,d)); 1110 } else if (od instanceof ExprObjectDesignator) { 1111 Expr e = ((ExprObjectDesignator)od).expr; 1112 Type t = javafe.tc.FlowInsensitiveChecks.getType(e); 1113 TypeDecl tdd = ((TypeSig)t).getTypeDecl(); 1114 if (TypeSig.getSig(td).isSubtypeOf((TypeSig)t)) tdd = td; 1115 Iterator i = Datagroups.get(tdd,d).iterator(); 1116 // FIXME - need to determine what the permissible content 1117 // of Datagroups.get() is 1118 Hashtable h = new Hashtable(); 1119 h.put(Substitute.thisexpr,e); 1120 while (i.hasNext()) { 1121 Object o = i.next(); 1122 if (o instanceof FieldDecl) { 1123 ErrorSet.caution("INTERNAL ERROR: Unhandled FieldDecl in ModifiesIterator.add: " + o); 1124 } else if (o instanceof Expr) { 1125 Expr ee = (Expr)o; 1126 ee = Substitute.doSubst(h,ee); 1127 others.add(ee); 1128 } else { 1129 ErrorSet.caution("INTERNAL ERROR: Unhandled case in ModifiesIterator.add: " + o.getClass()); 1130 } 1131 } 1132 } else if (od instanceof SuperObjectDesignator) { 1133 TypeSig ts = (TypeSig)((SuperObjectDesignator)od).type; 1134 TypeDecl tdd = ts.getTypeDecl(); 1135 if (TypeSig.getSig(td).isSubtypeOf(ts)) tdd = td; 1136 others.addAll(Datagroups.get(tdd,d)); 1137 } 1138 } 1139 1140 /** Returns the number of times the argument is in the 'done' 1141 * list 1142 * @param d Object to be checked 1143 * @return The number of times the argument is in the 'done' list 1144 */ 1145 private int count(FieldDecl d) { 1146 int k = 0; 1147 Iterator i = done.iterator(); 1148 while (i.hasNext()) { 1149 if (i.next() == d) ++k; 1150 } 1151 return k; 1152 } 1153 1154 } 1155 1156 1157 }