001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package escjava.backpred;
004
005 import java.util.Enumeration;
006 import java.util.Hashtable;
007 import java.util.Vector;
008 import java.util.LinkedList;
009
010 import javafe.ast.*;
011 import escjava.ast.*;
012 import escjava.ast.TagConstants;
013 import escjava.ast.Modifiers;
014 import escjava.ast.ExprDeclPragmaVec; // compiler bug workaround
015
016 import javafe.tc.*;
017 import javafe.util.*;
018
019 import escjava.translate.GC;
020 import escjava.translate.GetSpec;
021 import escjava.translate.Inner;
022 import escjava.translate.Translate;
023 import escjava.translate.Helper;
024
025 /**
026 * This class is responsible for determining the contributors to a
027 * given TypeSig or RoutineDecl.
028 *
029 * <p> The contributors are divided into a set of TypeSigs, a set of
030 * Invariants, and a set of Fields.
031 */
032
033 public class FindContributors
034 {
035 // Public interface
036
037 /**
038 * Generate the contributors for a given TypeSig. This may result
039 * in errors being reported and TypeSigs being type checked. <p>
040 *
041 * The originType is taken to be that Typesig.<p>
042 *
043 * Precondition: T must have been typechecked.<p>
044 *
045 * Note: in the process of locating contributors,
046 * FindContributors may type check additional types leading
047 * possibly to type errors. If such error(s) occur, a fatal
048 * error is reproted.
049 */
050 public FindContributors(/*@ non_null @*/ TypeSig T) {
051 originType = T;
052 addType(T);
053
054 walk(T.getTypeDecl());
055 fieldToPossible = null; // conserve space
056
057 if (Info.on) {
058 Info.out("[[contributors: "
059 + contributorTypes.size() + " types "
060 + contributorInvariants.size() + " invariants "
061 + contributorFields.size() + " fields ]]");
062 }
063 }
064
065 /**
066 * Generate the contributors for a given RoutineDecl. This may
067 * result in errors being reported and TypeSigs being type checked.<p>
068 *
069 * The originType is taken to be the type declaring that RoutineDecl.<p>
070 *
071 * Precondition: the type declaring rd must have been typechecked.<p>
072 *
073 * Note: in the process of locating contributors,
074 * FindContributors may type check additional types leading
075 * possibly to type errors. If such error(s) occur, a fatal
076 * error is reproted.
077 */
078 public FindContributors(/*@ non_null @*/ RoutineDecl rd) {
079 originType = TypeSig.getSig(rd.parent);
080 addType(originType);
081
082 walk(rd);
083 fieldToPossible = null; // conserve space
084
085 if (Info.on) {
086 Info.out("[[local contributors: "
087 + contributorTypes.size() + " types "
088 + contributorInvariants.size() + " invariants "
089 + contributorFields.size() + " fields ]]");
090 }
091 }
092
093
094 /**
095 * Our origin type; used to determine visibility and accessibility
096 * when needed.
097 */
098 public TypeSig originType;
099
100
101 /**
102 * Enumerate the TypeSig contributors
103 */
104 public Enumeration typeSigs() {
105 return contributorTypes.elements();
106 }
107
108 /**
109 * Enumerate the invariant contributors
110 */
111 public Enumeration invariants() {
112 return contributorInvariants.elements();
113 }
114
115 /**
116 * Enumerate the field contributors
117 */
118 public Enumeration fields() {
119 return contributorFields.elements();
120 }
121
122
123 // Closure code
124
125 /** The set of routines visited so far.
126 */
127
128 private /*@ non_null @*/ Set visitedRoutines = new Set();
129
130 /**
131 * The set of TypeSigs we've determined to be contributors so far. <p>
132 *
133 * Invariant: This set is closed under taking supertypes
134 */
135 private /*@ non_null @*/ Set contributorTypes = new Set();
136
137 /**
138 * The set of invariants (elementType ExprDeclPragmas) we've
139 * determined to be contributors so far. <p>
140 *
141 * Closure Property: walk(-) has been called on each of
142 * these invariants.
143 */
144 private /*@ non_null @*/ Set contributorInvariants = new Set();
145
146 /**
147 * The set of fields (elementType FieldDecl) we've determined to be
148 * contributors so far. <p>
149 *
150 * Closure Property:
151 *
152 * all invariants J that are declared in types in
153 * contributorTypes and "mention the field" f for f a field in
154 * contributorFields are members of contributorInvariants
155 */
156 private /*@ non_null @*/ Set contributorFields = new Set();
157
158 public int preFieldMode = 0;
159 public /*@ non_null @*/ Set preFields = new Set();
160
161 /**
162 * A mapping from fields (FieldDecls) to possible invariant
163 * contributors (ExprDeclPragmaVec). <p>
164 *
165 * (An invariant is a possible contributor if it is declared in a
166 * type of contributorTypes.)
167 *
168 * Invariant:
169 *
170 * if (f,J) in fieldToPossible then the invariant J "mentions
171 * the field" f and J is a possible invariant contributor
172 *
173 * Closure property:
174 *
175 * if J is possible invariant contributor,
176 * J not in contributorInvariants, and J "mentions the field" f,
177 * then (f,J) is in fieldToPossible.
178 *
179 */
180 // can be null
181 Hashtable fieldToPossible = new Hashtable();
182
183
184
185 /**
186 * Add the TypeSigs mentioned explicitly in a given Type to
187 * contributorTypes, maintaining all the closure properties. <p>
188 *
189 * Precondition: T has been resolved.<p>
190 */
191 //@ requires T != null;
192 private void addType(Type T) {
193 // TypeName case:
194 if (T instanceof TypeName) {
195 T = TypeSig.getSig((TypeName)T);
196 Assert.precondition(T != null);
197 }
198
199 // ArrayType case:
200 if (T instanceof ArrayType) {
201 addType(((ArrayType)T).elemType);
202 return;
203 }
204
205 // PrimitiveType case:
206 if (T instanceof PrimitiveType)
207 return;
208
209 /*
210 * Remaining case is TypeSig:
211 */
212 TypeSig sig = (TypeSig)T;
213 if (contributorTypes.contains(sig))
214 return;
215
216 // make sure sig is typechecked:
217 typecheck(sig);
218
219 // Close over taking supertypes:
220 TypeDecl td = sig.getTypeDecl();
221 if (td instanceof ClassDecl) {
222 ClassDecl cd = (ClassDecl)td;
223 if (cd.superClass != null)
224 addType(cd.superClass);
225 }
226 for (int i=0; i<td.superInterfaces.size(); i++)
227 addType(td.superInterfaces.elementAt(i));
228
229 contributorTypes.add(sig);
230
231 // Add sig's invariants as possible contributor invariants:
232 for (int i = 0; i<td.elems.size(); i++) {
233 TypeDeclElem tde = td.elems.elementAt(i);
234
235 if (tde.getTag() == TagConstants.INVARIANT)
236 addPossibleInvariant((ExprDeclPragma)tde);
237 }
238
239
240 /*
241 * Hack: for 1.1, add an inner classes' this$0 pointer when
242 * that class is added as a type, rather than trying to keep
243 * track of everywhere it might be introduced.
244 */
245 if (!sig.isTopLevelType()) {
246 FieldDecl thisptr = Inner.getEnclosingInstanceField(sig);
247
248 backedgeToGenericVarDecl(thisptr, null, true, new LinkedList());
249 }
250 }
251
252
253 /**
254 * Add a given field to contributorFields, maintaining all the
255 * closure properties. <p>
256 */
257 //@ requires fd != null;
258 private void addField(FieldDecl fd) {
259 if (contributorFields.contains(fd))
260 return;
261
262 contributorFields.add(fd);
263
264 /*
265 * Turn possible invariant contributors that mention fd into
266 * real ones. We use fieldToPossible to do this quickly.
267 */
268 ExprDeclPragmaVec newInvariants =
269 (ExprDeclPragmaVec)fieldToPossible.get(fd);
270 if (newInvariants==null)
271 return;
272
273 // Note: newInvariants is not modified here because we added fd to
274 // contributorFields
275 for (int i=0; i<newInvariants.size(); i++)
276 addInvariant(newInvariants.elementAt(i));
277 }
278
279 /**
280 * Add the mapping (fd, J) to fieldToPossible.
281 *
282 * Precondition: J is a possible invariant contributor, J "mentions
283 * the field" fd.
284 */
285 private void addPossibleMentions(FieldDecl fd, /*@ non_null @*/ ExprDeclPragma J) {
286 ExprDeclPragmaVec range = (ExprDeclPragmaVec)fieldToPossible.get(fd);
287 if (range==null) {
288 range = ExprDeclPragmaVec.make();
289 fieldToPossible.put(fd, range);
290 }
291
292 range.addElement(J);
293 }
294
295
296 /**
297 * Add a possible invariant contributor to either fieldToPossible
298 * or contributorInvariants as approperiate, maintaining all
299 * closure properties. <p>
300 *
301 * Precondition: J has been type checked.
302 */
303 //@ requires J != null;
304 private void addPossibleInvariant(ExprDeclPragma J) {
305 FieldDeclVec fieldsMentioned = fieldsInvariantMentions(J);
306
307 for (int i=0; i<fieldsMentioned.size(); i++) {
308 FieldDecl fd = fieldsMentioned.elementAt(i);
309
310 if (contributorFields.contains(fd)) {
311 // Ah! J is actually a real invariant contributor:
312 addInvariant(J);
313 return;
314 }
315
316 // Add (f,J) to fieldToPossible:
317 addPossibleMentions(fd, J);
318 }
319 }
320
321 /**
322 * Add a given invariant to contributorInvarints, maintaining all
323 * closure properties. <p>
324 *
325 * Precondition: J has been type checked.
326 */
327 //@ requires J != null;
328 private void addInvariant(ExprDeclPragma J) {
329 if (contributorInvariants.contains(J))
330 return;
331
332 contributorInvariants.add(J);
333
334 walk(J);
335 }
336
337
338 // Walking ASTNodes
339
340 /**
341 * Walks a given ASTNode, adding all the types it "mentions" via
342 * addType and adding all the fields it "mentions" via
343 * addField. <p>
344 *
345 * Precondition: N has been typechecked.
346 *
347 * WARNING: N is assumed to have no free local or parameter
348 * varables.
349 */
350 private void walk(ASTNode N) {
351 walk(N, null, true, new LinkedList());
352 }
353
354
355 /**
356 * Returns the set of fields that a given invariant mentions. <p>
357 *
358 * Precondition: J must be an invariant, J must be typechecked.
359 */
360 private FieldDeclVec fieldsInvariantMentions(ExprDeclPragma J) {
361 // We may cache this function later...
362
363 FieldDeclVec result = FieldDeclVec.make();
364 walk(J, result, false, new LinkedList());
365 return result;
366 }
367
368
369 /**
370 * Walks a given ASTNode, finding all the types it "mentions" and
371 * all the fields it "mentions". <p>
372 *
373 * If fields is null, the fields mentioned are added via addField;
374 * otherwise, they are added to fields directly.<p>
375 *
376 * If addTypes is true, the types mentioned are added via addType.<p>
377 *
378 * Precondition: N has been typechecked.
379 */
380 private void walk(ASTNode N, FieldDeclVec fields, boolean addTypes,
381 LinkedList visited) {
382 /*
383 * Leaf nodes:
384 */
385 if (N==null)
386 return;
387 if (N instanceof Type) {
388 if (addTypes)
389 addType((Type)N);
390 return;
391 }
392
393 if (N instanceof LiteralExpr || N instanceof ClassLiteral) {
394 Expr lit = (Expr)N;
395 if (addTypes) {
396 addType(TypeCheck.inst.getType(lit));
397 }
398 }
399
400 /*
401 * Handle relevant backedges:
402 */
403 if (N instanceof VariableAccess) {
404 backedgeToGenericVarDecl(((VariableAccess)N).decl,
405 fields, addTypes, visited);
406 }
407 if (N instanceof FieldAccess) {
408 if (preFieldMode > 0) {
409 preFields.add(N);
410 }
411 backedgeToGenericVarDecl(((FieldAccess)N).decl,
412 fields, addTypes, visited);
413 }
414
415 if (N instanceof ConstructorInvocation) {
416 ConstructorInvocation ci = (ConstructorInvocation) N;
417 visited.addFirst(ci.decl);
418 int inline = Translate.inlineDecoration.get(ci) != null ? 2 :
419 isNonRecursiveHelperInvocation(ci.decl) ? 1 : 0;
420 backedgeToRoutineDecl(ci.decl, fields, addTypes, inline, visited);
421 }
422 if (N instanceof NewInstanceExpr) {
423 NewInstanceExpr ni = (NewInstanceExpr) N;
424 int inline = Translate.inlineDecoration.get(ni) != null ? 2 :
425 isNonRecursiveHelperInvocation(ni.decl) ? 1 : 0;
426 backedgeToRoutineDecl(ni.decl,fields, addTypes, inline, visited);
427 }
428 if (N instanceof MethodInvocation) {
429 MethodInvocation mi = (MethodInvocation) N;
430 int inline = Translate.inlineDecoration.get(mi) != null ? 2 :
431 isNonRecursiveHelperInvocation(mi.decl) ? 1 : 0;
432
433 backedgeToRoutineDecl(mi.decl, fields, addTypes, inline, visited);
434 }
435 // FIXME - add the type from quantified expression? set comprehension expr? new array expr?
436 /*
437 * Add references not explicitly in Java code or from backedges:
438 */
439 if (N instanceof RoutineDecl) {
440 // Get references in our derived spec:
441 backedgeToRoutineDecl((RoutineDecl)N, fields, addTypes, 0, visited);
442
443 // Add implicit references if N is a ConstructorDecl:
444 if (N instanceof ConstructorDecl)
445 addImplicitConstructorRefs((ConstructorDecl)N,
446 fields, addTypes, visited);
447 }
448
449 if (N.getTag() == TagConstants.PRE) {
450 ++preFieldMode;
451 }
452
453
454
455 /*
456 * Recurse to subnodes (this automatically ignores backedges):
457 *
458 * We intentionally skip TypeDecls so that we stay in the same type.
459 */
460 try {
461 int size = N.childCount();
462 for (int i=0; i<size; i++) {
463 Object child = N.childAt(i);
464 if (child instanceof ASTNode && !(child instanceof TypeDecl))
465 walk((ASTNode)child, fields, addTypes, visited);
466 }
467 } finally {
468 if (N.getTag() == TagConstants.PRE) {
469 --preFieldMode;
470 }
471 }
472 }
473
474 /** Returns <code>true</code> if and only if <code>r</code> is a helper
475 * routine that has not been visited by this <code>FindContributor</code>
476 * object.
477 */
478
479 private boolean isNonRecursiveHelperInvocation(/*@ non_null */ RoutineDecl r) {
480 return Helper.isHelper(r) && !visitedRoutines.contains(r);
481 }
482
483 /**
484 * Add implicit references from a ConstructorDecl that do not
485 * appear in Java code or via backedges as per walk(,,).
486 *
487 * Precondition: the type declaring cd has been typechecked.
488 */
489 private void addImplicitConstructorRefs(/*@ non_null @*/ ConstructorDecl cd,
490 FieldDeclVec fields,
491 boolean addTypes,
492 LinkedList visited) {
493 /*
494 * Walk the initialization code derived from the same class as
495 * the constructor:
496 */
497 TypeDecl td = cd.parent;
498 walkInstanceInitialier(td, fields, addTypes, visited);
499
500 /*
501 * For all superinterfaces that the constructor's type
502 * implements that are not already implemented by its
503 * superclass(es), walk the initialization code derived from
504 * them:
505 */
506 Enumeration FII = GetSpec.getFirstInheritedInterfaces((ClassDecl)td);
507 while (FII.hasMoreElements()) {
508 walkInstanceInitialier((TypeDecl)FII.nextElement(), fields,
509 addTypes, visited);
510 }
511 }
512
513
514 /**
515 * Walk the implicit instance initializer code for a given
516 * TypeDecl, excluding any field initializations of
517 * superinterface fields. <p>
518 *
519 * E.g., f_1 = 0; ...; f_3 = <initializer exp>; ... ; <instance
520 * initializer block>...
521 *
522 * This is the code that constructors of that type implicitly
523 * start with after their super/sibling call modulo the
524 * initialization of superinterface fields.
525 *
526 * See addImplicitConstructorRefs for the full version w/o the
527 * exclusion.
528 *
529 *
530 * Addition: This now also pulls in all invariants in the given
531 * TypeDecl, regardless of what they mention. This is
532 * to avoid user surprise; see also Vanilla.java in
533 * test58.
534 *
535 *
536 * Precondition: the TypeDecl has been typechecked.
537 */
538 private void walkInstanceInitialier(/*@ non_null @*/ TypeDecl td,
539 FieldDeclVec fields,
540 boolean addTypes,
541 LinkedList visited) {
542 for (int i = 0; i < td.elems.size(); i++) {
543 TypeDeclElem tde = td.elems.elementAt(i);
544
545 if (tde.getTag() == TagConstants.INVARIANT)
546 addInvariant((ExprDeclPragma)tde);
547
548 if (tde instanceof ModelDeclPragma)
549 tde = ((ModelDeclPragma)tde).decl;
550 if (tde instanceof GhostDeclPragma)
551 tde = ((GhostDeclPragma)tde).decl;
552 if (tde.getTag() == TagConstants.FIELDDECL
553 && !Modifiers.isStatic(((FieldDecl)tde).modifiers)) {
554 FieldDecl fd = (FieldDecl)tde;
555
556 // walk "fd := (fd.init==null ? <zero-equivalent> : fd.init)":
557 backedgeToGenericVarDecl(fd, fields, addTypes, visited);
558 walk(fd.init, fields, addTypes, visited);
559
560 } else if (tde.getTag() == TagConstants.INITBLOCK
561 && !Modifiers.isStatic(((InitBlock)tde).modifiers)) {
562 // walk any instance initializer blocks found:
563 walk((InitBlock)tde, fields, addTypes, visited);
564
565 }
566 }
567 }
568
569
570 /**
571 * Calculate the fields and types "mentioned" by a backedge to a
572 * GenericVarDecl and then add them as per walk(,,).
573 */
574 private void backedgeToGenericVarDecl(GenericVarDecl decl,
575 FieldDeclVec fields,
576 boolean addTypes,
577 LinkedList visited) {
578 // The length field of arraytypes is never considered "mentioned":
579 if (decl==javafe.tc.Types.lengthFieldDecl)
580 return;
581
582 if (decl instanceof FieldDecl) {
583 FieldDecl fd = (FieldDecl)decl;
584 typecheck(TypeSig.getSig(fd.parent));
585
586
587 // The range and domain types of fd are "mentioned":
588 addType(fd.type);
589 if (fd.parent != null) // "length" field has no parent...
590 addType(TypeSig.getSig(fd.parent));
591
592 /*
593 * Exit if have already processed this field; need to do
594 * this to avoid recursion in case the field's modifiers
595 * mention it.
596 */
597 if (fields==null) {
598 if (contributorFields.contains(fd))
599 return;
600 } else if (fields.contains(fd))
601 return;
602
603
604 // The field fd is "mentioned":
605 if (fields != null)
606 fields.addElement(fd);
607 else
608 addField(fd);
609
610 /*
611 * We need to walk the "spec" part of fd as well to handle
612 * readable_if and the like:
613 */
614 if (fd.pmodifiers != null) {
615 for (int i=0; i<fd.pmodifiers.size(); i++)
616 walk(fd.pmodifiers.elementAt(i), fields, addTypes, visited);
617 }
618 }
619
620 /*
621 * Ignore local & parameter variable Decls here, as they
622 * should already have been walked over.
623 */
624 }
625
626 /**
627 * Calculate the fields and types "mentioned" by a backedge to a
628 * RoutineDecl and then add them as per walk(,,). <p>
629 *
630 * <code>inlined</code> is one of: 0 (not an inlined routine),
631 * 1 (an inlined helper routine), or 2 (a routine inlined for
632 * a reason other than being a helper). (Why this complication,
633 * why not just use a boolean field "inlined"? By distinguishing
634 * cases 1 and 2, one can write a nice run-time assert inside the
635 * implementation of this method.)
636 */
637 //@ requires inlined == 0 || inlined == 1 || inlined == 2;
638 private void backedgeToRoutineDecl(RoutineDecl rd,
639 FieldDeclVec fields,
640 boolean addTypes,
641 int inlined, LinkedList visited) {
642 if (rd == null) return; // FIXME - this happens with some NewInstanceExpr
643 // FIXME - remove references to visited
644 //if (visited.contains(rd)) return;
645 //visited.addFirst(rd);
646 if (inlined==0 && visitedRoutines.contains(rd)) return;
647 //Assert.notFalse(inlined != 1 || !visitedRoutines.contains(rd));
648 visitedRoutines.add(rd);
649
650 TypeSig thisType = TypeSig.getSig(rd.parent);
651 typecheck(thisType);
652
653 /*
654 * Temporarily set GC.thisvar's type to thisType; we need to
655 * do this because GetSpec.getCombinedMethodDecl() returns
656 * GC.thisvar as the first argument of instance methods.
657 *
658 * If we don't do this, we may add the wrong type when we add
659 * the types of the routine's arguments below.
660 */
661 Type savedType = GC.thisvar.decl.type;
662 GC.thisvar.decl.type = thisType;
663
664 // Get the derived spec for rd:
665 DerivedMethodDecl dmd = GetSpec.getCombinedMethodDecl(rd);
666 dmd = GetSpec.filterMethodDecl(dmd, this);
667
668
669 /*
670 * The types in the called routine's Java signature are
671 * "mentioned" (including the type of Constructors): */
672 if (addTypes) {
673 // Add args here mostly for safely reasons
674 for (int i=0; i<dmd.args.size(); i++)
675 addType(dmd.args.elementAt(i).type);
676 for (int i=0; i<dmd.throwsSet.size(); i++)
677 addType(dmd.throwsSet.elementAt(i));
678 addType(dmd.returnType);
679 }
680
681 // We also need to walk the routine's spec:
682 for (int i=0; i<dmd.requires.size(); i++)
683 walk(dmd.requires.elementAt(i), fields, addTypes, visited);
684 if (inlined == 0) {
685 // Add modifies here mostly for safely reasons
686 for (int i=0; i<dmd.modifies.size(); i++)
687 walk(dmd.modifies.elementAt(i), fields, addTypes, visited);
688 }
689 for (int i=0; i<dmd.ensures.size(); i++)
690 walk(dmd.ensures.elementAt(i), fields, addTypes, visited);
691 for (int i=0; i<dmd.exsures.size(); i++)
692 walk(dmd.exsures.elementAt(i), fields, addTypes, visited);
693
694 if (inlined != 0) {
695 walk(rd.body, fields, addTypes, visited);
696 }
697
698 GC.thisvar.decl.type = savedType;
699 //visited.removeFirst();
700 }
701
702
703 // Utility routines
704
705 /**
706 * Make sure a given TypeSig has been type checked, type checking
707 * it if necessary. <p>
708 *
709 * Throws a fatal error if a type error occurs while checking sig.
710 */
711 void typecheck(/*@ non_null @*/ TypeSig sig) {
712 int errorCount = ErrorSet.errors;
713
714 sig.typecheck();
715 if (errorCount == ErrorSet.errors)
716 return;
717
718 ErrorSet.fatal("A type error has occurred at an unexpected point;"
719 + " unable to continue processing");
720 }
721 }