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 }