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    }