001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package javafe.tc;
004    
005    import javafe.ast.*;
006    import javafe.util.*;
007    import java.util.Hashtable;
008    import java.util.Enumeration;
009    
010    
011    /**
012     * Does type name resolution and type checking at signature level of
013     * a type declaration, and infers the members of the
014     * declaration. Also resolves type names at the signature
015     * level. Assumes the TypeSig was previously in the "supertype links
016     * resolved" state.
017     */
018    
019    public class PrepTypeDeclaration {
020    
021        /** A (possibly extended) instance of PrepTypeDeclaration. */
022        /*@spec_public*/ protected static PrepTypeDeclaration inst;
023        //@ public invariant inst!=null; //this is not meant to be a static invariant
024    
025        public static /*@non_null*/ PrepTypeDeclaration getInst() {
026           return inst;
027        }
028    
029      /** */
030    
031      public PrepTypeDeclaration() {
032        inst = this;
033        //@ set methodSeq.elementType      = \type(MethodDecl);
034        //@ set methodSeq.owner = this;
035    
036        //@ set fieldSeq.elementType       = \type(FieldDecl);
037        //@ set fieldSeq.owner = this;
038    
039        //@ set hiddenfieldSeq.elementType       = \type(FieldDecl);
040        //@ set hiddenfieldSeq.owner = this;
041    
042        //@ set constructorSeq.elementType = \type(ConstructorDecl);
043        //@ set constructorSeq.owner = this;
044    
045        //@ set overridesDecoration.decorationType = \type(Set);
046      }
047    
048      /** 
049        * Does type name resolution and type checking at signature level of
050        * a type declaration, and infers the members of the declaration. 
051        * Sets the "methods" and "fields" fields of the TypeSig appropriately.
052        */
053      
054      //@ ensures sig.fields != null;
055      //@ ensures sig.methods != null;
056      public void prepTypeSignature(/*@ non_null @*/ TypeSig sig) { 
057        
058        TypeDecl decl = sig.getTypeDecl();
059    
060        prepStart(sig,decl);
061        prepDo(sig,decl);
062        prepEnd(sig,decl);
063      }
064    
065      protected void prepStart(TypeSig sig, TypeDecl decl) {
066        /*
067         * Check for same simple name as an enclosing type:
068         */
069        for (TypeSig enclosing = sig.enclosingType;
070             enclosing != null;
071             enclosing = enclosing.enclosingType) {
072            if (decl.id.equals(enclosing.getTypeDecl().id))
073                ErrorSet.error(decl.locId,
074                               "A type may not have the same simple "
075                               + "name as any of its enclosing types.");
076        }
077    
078    
079        fieldSeq.push();
080        hiddenfieldSeq.push();
081        methodSeq.push();
082        constructorSeq.push();
083        numList.addFirst(new Integer(numFields));
084        numFields = -1;
085      }
086    
087      protected void prepDo(TypeSig sig, TypeDecl decl) {
088        //@ assert decl != null;
089        //@ assume (decl instanceof ClassDecl) || (decl instanceof InterfaceDecl);
090        if( decl instanceof ClassDecl ) 
091          visitClassDecl( (ClassDecl)decl, sig );
092        else
093          visitInterfaceDecl( (InterfaceDecl)decl, sig );
094      }
095    
096      protected void prepEnd(TypeSig sig, TypeDecl decl) {
097        sig.fields = FieldDeclVec.popFromStackVector( fieldSeq );
098        sig.hiddenfields = FieldDeclVec.popFromStackVector( hiddenfieldSeq );
099        sig.methods = MethodDeclVec.popFromStackVector( methodSeq );
100        constructorSeq.pop();
101        numFields = ((Integer)numList.removeFirst()).intValue();
102      }
103    
104      // ----------------------------------------------------------------------
105    
106      /** Decorates MethodDecl of prepped TypeDecls with a Set of
107       * methods that decl overrides or hides.  This is *NOT* transtitive! */
108    
109      //@ requires md != null && overrides != null;
110      private void addOverride(MethodDecl md, MethodDecl overrides) {
111        Set overridesSet = getOverrides( md );
112        overridesSet.add( overrides );
113      }
114    
115      /**
116       * Returns the set of all methods that <code>md</code> overrides,
117       * where <code>md</code> is considered to appear in those prepped
118       * subtypes of <code>md.parent</code> that inherit <code>md</code>.
119       *
120       * Warning: This set may expand as additional subtypes of
121       * <code>md.parent</code> are prepped.
122       *
123       * Warning: If you want the set of methods that <code>md</code>
124       * overrides, with <code>md</code> considered to appear in a
125       * particular type <code>td</code>, use getOverrides(TypeDecl,
126       * MethodDecl) instead!
127       */
128      //@ requires md != null;
129      //@ ensures \result != null;
130      //@ ensures \result.elementType == \type(MethodDecl);
131      public Set getOverrides(MethodDecl md) {
132        Set overrides = (Set)overridesDecoration.get( md );
133        //@ assume overrides.elementType == \type(MethodDecl);
134        if( overrides == null ) {
135          overrides = new Set();
136          //@ assume overrides.elementType == \type(MethodDecl);
137          overridesDecoration.set( md, overrides );
138        }
139        return overrides;
140      }
141    
142    
143      /**
144       * Returns the set of methods that <code>md</code> overrides, with
145       * <code>md</code> considered to appear in a particular type
146       * <code>td</code>. <p>
147       *
148       * This routine may result in <code>td</code> being prepped.
149       */
150      //@ requires td != null;
151      //@ requires md != null;
152      //@ ensures \result != null;
153      //@ ensures \result.elementType == \type(MethodDecl);
154      public Set getOverrides(TypeDecl td, MethodDecl md) {
155        TypeSig sig = TypeSig.getSig(td);
156        sig.prep();
157    
158        Set overrides = getOverrides(md);
159        Set actualOverrides = new Set();
160        //@ assume actualOverrides.elementType == \type(MethodDecl);
161    
162        Enumeration overridden_methods = overrides.elements();
163        while (overridden_methods.hasMoreElements()) {
164          MethodDecl smd = (MethodDecl)overridden_methods.nextElement();
165          //@ assume smd.hasParent;
166          if (sig.isSubtypeOf(TypeSig.getSig(smd.parent))) {
167            actualOverrides.add(smd);
168          }
169        }
170        
171        return actualOverrides;
172      }
173    
174      //@ invariant overridesDecoration.decorationType == \type(Set);
175      //@ spec_public
176      private static /*@ non_null @*/ ASTDecoration overridesDecoration 
177        = new ASTDecoration("overridesDecoration");
178      
179      // ----------------------------------------------------------------------
180      
181      // Stacks up the members of the type
182      //@ invariant fieldSeq.elementType == \type(FieldDecl);
183      //@ invariant fieldSeq.owner == this;
184      protected /*@ non_null @*/ StackVector fieldSeq = new StackVector();
185    
186      //@ invariant hiddenfieldSeq.elementType == \type(FieldDecl);
187      //@ invariant hiddenfieldSeq.owner == this;
188      protected /*@ non_null @*/ StackVector hiddenfieldSeq = new StackVector();
189    
190      // "invariant" <elements>.hasParent
191      //@ invariant methodSeq.elementType == \type(MethodDecl);
192      //@ invariant methodSeq.owner == this;
193      protected /*@ non_null @*/ StackVector methodSeq = new StackVector();
194    
195      //@ invariant constructorSeq.elementType == \type(ConstructorDecl);
196      //@ invariant constructorSeq.owner == this;
197      protected /*@ non_null @*/ StackVector constructorSeq = new StackVector();
198      
199      private int numFields = -1;
200      private java.util.LinkedList numList = new java.util.LinkedList();
201    
202      // ----------------------------------------------------------------------
203    
204      /** Does signature-level checking and adds type members to fieldSeq
205       *  and methodSeq.  */
206    
207      //@ requires decl != null && currentSig != null;
208      protected void visitClassDecl(ClassDecl decl, TypeSig currentSig ) {
209        
210        // Check that the modifiers are ok
211        checkTypeModifiers(decl, currentSig, true);
212    
213    
214        // Visit all enclosed member declarations
215        // They will add themselves to fieldSeq and methodSeq
216        
217        for(int i=0; i< decl.elems.size(); i++) {
218            TypeDeclElem elem = decl.elems.elementAt(i);
219            //@ assume elem.hasParent;   // "invariant"
220            visitTypeDeclElem(elem,
221                              currentSig,
222                              Modifiers.isAbstract(decl.modifiers),
223                              Modifiers.isFinal(decl.modifiers),
224                              false );
225        }
226    
227        startSupers();
228    
229        // Add members of direct super interfaces
230        
231        //checkSuperInterfaces( currentSig, decl.superInterfaces );
232        
233        // Add members of direct superclass, if any
234        // superclass may be null, or may name an interface
235    
236        TypeName superClassName = decl.superClass;
237        TypeSig superClassSig 
238          = superClassName == null ? null : TypeSig.getSig( superClassName );
239    
240        if( superClassSig != null ) {
241            if( superClassSig.getTypeDecl() instanceof ClassDecl ) 
242              {     
243                // check superclass is not final
244                if( Modifiers.isFinal(superClassSig.getTypeDecl().modifiers) )
245                  ErrorSet.error(superClassName.getStartLoc(),
246                                 "Can't subclass final classes: class "
247                                    + superClassSig.getExternalName());
248                else
249                  addInheritedMembers( currentSig, superClassSig );
250                checkSuperTypeAccessible(currentSig, superClassSig,
251                                         superClassName==null ?
252                                         decl.getStartLoc() :
253                                         superClassName.getStartLoc());
254              }
255            else
256              {
257                ErrorSet.error( superClassName.getStartLoc(),
258                               "Can't subclass interfaces: interface "
259                                    + superClassSig.getExternalName());
260              }
261          }
262        
263        // Add members of direct super interfaces
264        
265        checkSuperInterfaces( currentSig, decl.superInterfaces );
266    
267        // Check no two abstract methods with same method signature
268        // and different return types
269        
270        for( int i=0; i<methodSeq.size(); i++ ) 
271          {
272            MethodDecl mdi = (MethodDecl)methodSeq.elementAt(i);
273            for( int j=0; j<i; j++ ) 
274              {
275                MethodDecl mdj = (MethodDecl)methodSeq.elementAt(j);
276                
277                // Check if mdi and mdj are abstract methods
278                // with same signature and different return types
279                
280                if(   Modifiers.isAbstract(mdi.modifiers)
281                   && Modifiers.isAbstract(mdj.modifiers)
282                   && Types.isSameMethodSig( mdi, mdj )
283                   && !Types.isSameType( mdi.returnType, mdj.returnType ) )
284                  {
285                    ErrorSet.error( decl.loc,
286                                   "Class "+decl.id
287                                   +" contains two abstract methods"
288                                   +" with same signature"
289                                   +" but different return types");
290                  }
291              }
292          }
293        // All done
294      }
295      
296    
297        /**
298         * Check that the modifiers of a type are ok. <p>
299         *
300         * decl is the TypeDecl for the type, and currentSig its TypeSig. <p>
301         *
302         * isClass should be true iff the TypeDecl is a ClassDecl.<p>
303         */
304        public void checkTypeModifiers(/*@ non_null @*/ TypeDecl decl,
305                                       /*@ non_null @*/ TypeSig currentSig,
306                                       boolean isClass) {
307            /*
308             * Check abstract modifier:
309             *
310             *    allowed unless is a final class
311             */
312            if (isClass && Modifiers.isAbstract(decl.modifiers) 
313               && Modifiers.isFinal(decl.modifiers)) 
314                ErrorSet.error(decl.loc, 
315                       "A class cannot be declared both final and abstract");
316    
317            /*
318             * Check final modifier:
319             *
320             *    allowed on any non-interface
321             */
322            if (!isClass)
323                checkModifiers(decl.modifiers, ~(Modifiers.ACC_FINAL),
324                               decl.loc, "interface");
325    
326            /*
327             * Handle rest of non-member types: only abstract, final, and
328             * strictfp and allowed as their modifiers.
329             */
330            if (!currentSig.member) {
331                checkModifiers(decl.modifiers, 
332                               Modifiers.ACC_FINAL|Modifiers.ACC_ABSTRACT|
333                               Modifiers.ACC_STRICT,
334                               decl.loc,
335                               "non-member type");
336                return;
337            }
338    
339            // Only have to worry about member types from now on:
340    
341    
342            /*
343             * Check access modifiers (public,protected,private):
344             *
345             *   They are not allowed on non-member types;
346             *   only public is allowed for package-member types;
347             *   fields of interfaces may not be protected or private
348             */
349            boolean isInterfaceMember = false;
350            if (currentSig.enclosingType==null) {
351                checkModifiers(decl.modifiers, 
352                               ~(Modifiers.ACC_PROTECTED|Modifiers.ACC_PRIVATE),
353                               decl.loc, "package-member type");
354            } else {
355                isInterfaceMember = (currentSig.enclosingType.getTypeDecl())
356                    instanceof InterfaceDecl;
357                if (isInterfaceMember)
358                    checkModifiers(decl.modifiers, 
359                                   ~(Modifiers.ACC_PROTECTED|
360                                     Modifiers.ACC_PRIVATE),
361                                   decl.loc, "interface member");
362            }
363    
364    
365            /*
366             * Check static modifier:
367             *
368             *    Not allowed on package-member types.
369             *    Otherwise only allowed for members of top-level types and
370             *    interfaces.
371             */
372            if (currentSig.enclosingType==null) {
373                if ((decl.modifiers&Modifiers.ACC_STATIC) != 0)
374                    ErrorSet.error(decl.loc,
375                           "Package-member types cannot be declared static");
376            } else {
377                boolean staticAllowed = isInterfaceMember;
378                if (currentSig.enclosingType.isTopLevelType())
379                    staticAllowed = true;
380                if (Modifiers.isStatic(decl.modifiers) && !staticAllowed)
381                    ErrorSet.error(decl.loc,
382                                   "Nested type "+currentSig+" cannot be static;"
383                                   + " static types can be members of only"
384                                   + " interfaces and top-level classes.");
385    
386                // Interfaces are implicitly static:
387                if (!isClass) {
388                    if (!Modifiers.isStatic(decl.modifiers) && !staticAllowed)
389                        ErrorSet.error(decl.loc,
390                          "Static types can be members of only interfaces "
391                           + "and top-level classes.  (Interfaces are "
392                           + "implicitly static.)");
393    
394                    decl.modifiers |= Modifiers.ACC_STATIC;
395                }
396            }
397    
398    
399            /*
400             * The following modifiers are disallowed for all types:
401             */
402            checkModifiers(decl.modifiers, 
403                           ~(Modifiers.ACC_SYNCHRONIZED|Modifiers.ACC_VOLATILE|
404                             Modifiers.ACC_TRANSIENT|Modifiers.ACC_NATIVE),
405                           decl.loc, "type");
406        }
407    
408    
409      // ----------------------------------------------------------------------
410      
411      /** Does signature-level checking 
412        and adds type members to fieldSeq and methodSeq.
413          */
414      
415      //@ requires decl != null && currentSig != null;
416      protected void visitInterfaceDecl(InterfaceDecl decl,
417                                      TypeSig currentSig ) {
418        Info.out("[prepping enclosed interface " + decl.id + "]");
419        
420        // Check that the modifiers are ok
421        checkTypeModifiers(decl, currentSig, false);
422    
423    
424        // Visit all enclosed member declarations
425        // They will add themselves to fieldSeq and methodSeq
426        
427        for(int i=0; i<decl.elems.size(); i++) {
428            TypeDeclElem elem = decl.elems.elementAt(i);
429            //@ assume elem.hasParent;   // "invariant"
430            visitTypeDeclElem(elem, currentSig, true, false, true );
431        }
432    
433        checkSuperInterfaces( currentSig, decl.superInterfaces);
434        
435    
436        /*
437         * Interfaces with no superinterface fields inherit from the root
438         * interface unless they are the root interface itself...
439         */
440        if (decl.superInterfaces.size()==0) {
441            TypeSig root = getRootInterface();
442            if (root != currentSig)
443                addInheritedMembers(currentSig, root);
444        }
445    
446    
447        // ### STILL NEED TO CHECK NO DUPLICATE METHOD SIGNATURES ???
448        
449        // All done
450      }
451      
452      // ----------------------------------------------------------------------
453      
454      protected void startSupers() {
455        numFields = fieldSeq.size();
456      }
457    
458      /** Check superinterfaces 
459        and add their members to fieldSeq and methodSeq. 
460          */
461      
462      // Precondition: all the types in superinterfaces have been resolved
463      //@ requires sig != null && superInterfaces != null;
464      protected void checkSuperInterfaces(TypeSig sig, 
465                                        TypeNameVec superInterfaces ) {
466        
467        // Check no duplicates in superinterfaces
468        // Check all TypeNames are interfaces
469        // Add inherited methods to fieldSeq and methodSeq
470        
471        Hashtable t = new Hashtable(10);
472        for( int i=0; i<superInterfaces.size(); i++ ) 
473          {
474            TypeName superInterfaceName = superInterfaces.elementAt(i);
475            TypeSig superInterface = TypeSig.getSig( superInterfaceName );
476            int loc = superInterfaceName.name.getStartLoc();
477    
478            checkSuperTypeAccessible(sig, superInterface, loc);
479    
480            if( t.containsKey(superInterface) )
481              ErrorSet.error(loc,
482                             "Duplicate interface "
483                             +superInterfaceName.name.printName() );
484            else if( !( superInterface.getTypeDecl() instanceof InterfaceDecl ) ) 
485              ErrorSet.error(loc,
486                            "Interfaces may not extend classes: class "
487                            + superInterface.getExternalName());
488            else 
489              {
490                t.put( superInterface, superInterface );
491                addInheritedMembers( sig, superInterface );
492              }
493          }
494      }
495      
496      // ----------------------------------------------------------------------
497      
498      /** Visit a TypeDeclElem, check it 
499        and add it to fieldSeq or methodSeq, if appropriate
500          */
501    
502      //@ requires e.hasParent;
503      protected void visitTypeDeclElem(/*@ non_null @*/ TypeDeclElem e,
504                                     /*@ non_null @*/ TypeSig currentSig,
505                                     boolean abstractMethodsOK,
506                                     boolean inFinalClass,
507                                     boolean inInterface ) {
508        
509        if( e instanceof FieldDecl )
510          visitFieldDecl( (FieldDecl) e, currentSig,
511                         abstractMethodsOK, inFinalClass, inInterface );
512        
513        else if( e instanceof MethodDecl )
514          visitMethodDecl( (MethodDecl) e, currentSig,
515                          abstractMethodsOK, inFinalClass, inInterface );
516        
517        else if( e instanceof ConstructorDecl )
518          visitConstructorDecl( (ConstructorDecl) e, currentSig,
519                               abstractMethodsOK, inFinalClass, inInterface );
520        else if (e instanceof TypeDecl) {
521            /*
522             * Check for duplicates; only complain about 2nd and later ones
523             */
524            TypeDecl decl = (TypeDecl)e;
525            TypeDecl parent = e.getParent();
526    
527            // Find first declaration with same id:
528            TypeDecl first = decl;
529            for (int i=0; i<parent.elems.size(); i++) {
530                TypeDeclElem tde = parent.elems.elementAt(i);
531                if (tde instanceof TypeDecl && ((TypeDecl)tde).id==first.id) {
532                    first = (TypeDecl)tde;
533                    break;
534                }
535            }
536    
537            if (first != decl)
538                ErrorSet.error(decl.locId,
539                               "Duplicate nested-type declaration: the type "
540                               + TypeSig.getSig(decl)
541                               + " is already declared",
542                               first.locId);
543        } else if (e instanceof InitBlock) {
544            InitBlock x = (InitBlock)e;
545            
546            if (Modifiers.isStatic(x.modifiers) && !inInterface
547                && !currentSig.isTopLevelType())
548                ErrorSet.error(x.getStartLoc(), 
549                               "Only top-level classes may"
550                               + " contain static initializer blocks");
551        } else if (!(e instanceof TypeDeclElemPragma))
552          Assert.fail("Unexpected TypeDeclElem");
553        
554      }
555      
556      // ----------------------------------------------------------------------
557      
558      /** Visit a FieldDecl, check it and add it to fieldSeq. */
559      
560      //@ requires x != null && currentSig != null;
561      protected void visitFieldDecl(FieldDecl x,
562                                  TypeSig currentSig,
563                                  boolean abstractMethodsOK,
564                                  boolean inFinalClass,
565                                  boolean inInterface ) {
566    
567        if (Modifiers.isStatic(x.modifiers) && !inInterface
568            && !currentSig.isTopLevelType() && !Modifiers.isFinal(x.modifiers))
569            ErrorSet.error(x.locId, 
570              "Inner classes may not declare static members, unless they are"
571              + " compile-time constant fields");
572        
573        checkModifiers( x.modifiers, 
574                       inInterface
575                       ? Modifiers.ACC_PUBLIC | Modifiers.ACC_FINAL 
576                       | Modifiers.ACC_STATIC
577                       : Modifiers.ACCESS_MODIFIERS | Modifiers.ACC_FINAL 
578                       | Modifiers.ACC_STATIC
579                       | Modifiers.ACC_TRANSIENT | Modifiers.ACC_VOLATILE,
580                       x.locId, inInterface ? "interface field" : "field" );
581        
582        // If in an interface, field declaration is implicitly
583        // public static final
584        
585        if( inInterface )
586          x.modifiers |= 
587            Modifiers.ACC_PUBLIC | Modifiers.ACC_FINAL | Modifiers.ACC_STATIC;
588        
589        if( Modifiers.isFinal(x.modifiers) 
590            && Modifiers.isVolatile(x.modifiers) )
591          ErrorSet.error( x.locId, "final fields cannot be volatile");
592        
593        // Error if two fields in type body with same name
594        for( int i=0; i<fieldSeq.size(); i++ ) 
595          {
596            FieldDecl e = (FieldDecl)fieldSeq.elementAt(i);
597            if( e.id == x.id )
598              ErrorSet.error(x.locId, 
599                             "Duplicate field with same identifier",e.locId);
600          }
601    
602        getEnvForCurrentSig(currentSig, true).resolveType(currentSig, x.type );
603        
604        fieldSeq.addElement( x );
605      }
606      
607      // ----------------------------------------------------------------------
608      
609      /** Visit a MethodDecl, check it and add it to methodSeq. */
610      
611      //@ requires x != null && currentSig != null;
612      protected void visitMethodDecl(MethodDecl x,
613                                   TypeSig currentSig,
614                                   boolean abstractMethodsOK,
615                                   boolean inFinalClass,
616                                   boolean inInterface ) {
617    
618        if (Modifiers.isStatic(x.modifiers) && !inInterface
619            && !currentSig.isTopLevelType())
620            ErrorSet.error(x.locId, 
621                           "Only methods of top-level classes may be static");
622        
623        // Modifiers can only be:  
624        //   public protected private abstract static final synchronized native
625        //   strictfp
626        checkModifiers( x.modifiers, 
627                       inInterface
628                       ? (Modifiers.ACC_PUBLIC | Modifiers.ACC_ABSTRACT)
629                       : (Modifiers.ACCESS_MODIFIERS | Modifiers.ACC_ABSTRACT 
630                       | Modifiers.ACC_FINAL | Modifiers.ACC_SYNCHRONIZED 
631                       | Modifiers.ACC_STATIC | Modifiers.ACC_NATIVE
632                       | Modifiers.ACC_STRICT),
633                       x.loc, inInterface ? "interface method" : "method" );
634    
635        // If in interface, method is implicitly abstract and public
636        if( inInterface ) 
637            x.modifiers |= Modifiers.ACC_ABSTRACT | Modifiers.ACC_PUBLIC;
638        
639        // private methods implicitly final
640        // members of final class are implicitly final
641        if( Modifiers.isPrivate(x.modifiers) || inFinalClass ) 
642          x.modifiers |= Modifiers.ACC_FINAL;
643        
644        // Error if an abstract method is also
645        // private, static, final, native, or synchronized. 
646        if( Modifiers.isAbstract(x.modifiers) &&
647           (Modifiers.isPrivate(x.modifiers)
648            | Modifiers.isStatic(x.modifiers)
649            | Modifiers.isFinal(x.modifiers)
650            | Modifiers.isNative(x.modifiers)
651            | Modifiers.isSynchronized(x.modifiers)) )
652          ErrorSet.error( x.locId, 
653            "Incompatible modifiers for abstract method");
654    
655        // resolve types
656         getEnvForCurrentSig(currentSig, true).resolveType( currentSig, x.returnType );
657        for( int i=0; i<x.raises.size(); i++ )
658          getEnvForCurrentSig(currentSig, true).resolveType( currentSig, x.raises.elementAt(i) );
659        for( int i=0; i<x.args.size(); i++ )
660          getEnvForCurrentSig(currentSig, true).resolveType( currentSig, x.args.elementAt(i).type );
661        
662        // Error if two methods in type body with same signature
663        for( int i=0; i<methodSeq.size(); i++ ) 
664          {
665            if(Types.isSameMethodSig( x, (MethodDecl)methodSeq.elementAt(i) ) )
666              ErrorSet.error(x.loc, 
667                             "Duplicate declaration of method "
668                             +"with same signature");
669          }
670        
671        methodSeq.addElement(x);
672      }
673      
674      // ----------------------------------------------------------------------
675      
676      /** Visit ConstructorDecl, check it, and add it to constructorSeq. */
677      
678      //@ requires x != null && currentSig != null;
679      protected void visitConstructorDecl(ConstructorDecl x,
680                                        TypeSig currentSig,
681                                        boolean abstractMethodsOK,
682                                        boolean inFinalClass,
683                                        boolean inInterface ) {
684    
685        if( inInterface ) 
686          ErrorSet.error("Interfaces cannot include a constructor");
687        
688        // Modifiers can only be: public protected private strictfp
689        checkModifiers(x.modifiers,
690                       Modifiers.ACCESS_MODIFIERS | Modifiers.ACC_STRICT,
691                       x.loc, "constructor" );
692        
693        // resolve types
694        for( int i=0; i<x.raises.size(); i++ )
695          getEnvForCurrentSig(currentSig, true).resolveType( currentSig, x.raises.elementAt(i) );
696        for( int i=0; i<x.args.size(); i++ ) {
697          getEnvForCurrentSig(currentSig, true).resolveType( currentSig, x.args.elementAt(i).type );
698        }
699    
700        // Error if two constructors in type body with same signature
701        for( int i=0; i<constructorSeq.size(); i++ ) 
702          {
703            ConstructorDecl cd = (ConstructorDecl)constructorSeq.elementAt(i);
704            if( Types.isSameFormalParaDeclVec(x.args, cd.args ))
705              ErrorSet.error( x.loc, 
706                             "Duplicate declaration of constructor "
707                             +"with same signature",
708                            cd.loc);
709          }
710        
711        constructorSeq.addElement(x);
712      }
713      
714      // *********************************************************************
715    
716      /**
717       * Find all members of a supertype inherited by a type.
718       * Adds these members to fieldSeq and methodSeq.
719       *
720       * The order in which superTypes are added is crucial.  See the
721       * comment below marked by a <<>>
722       */
723      
724      //@ requires type != null && superType != null;
725      protected void addInheritedMembers(TypeSig type, TypeSig superType ) {
726    
727        TypeDecl jLOTypeDecl = Types.javaLangObject().getTypeDecl();
728        
729        FieldDeclVec superFields = superType.getFields(false);
730        for( int i=0; i<superFields.size(); i++ ) {
731            FieldDecl superField = superFields.elementAt(i);
732            //@ assume superField.hasParent;  // "ensures"
733            
734            // A type inherits from its direct supertypes all fields
735            // that are accessible and not hidden ( JLS 8.3 and 9.2)
736            // If multiple paths by which same field declaration 
737            // could be inherited, then it is inherited only once.
738            
739            if (fieldSeq.contains( superField )  ||
740                hiddenfieldSeq.contains(superField) )  {
741                    // field already included by inheritance through another
742                    // interface
743            } else if( superMemberAccessible( type, superType, superField.modifiers,
744                                                            superField.pmodifiers ) 
745               && !declaresFieldJava( type, superField.id ) ) {
746                fieldSeq.addElement( superField );
747            } else {
748                hiddenfieldSeq.addElement( superField );
749            }
750        }
751        superFields = superType.getHiddenFields();
752        for( int i=0; i<superFields.size(); i++ ) {
753            hiddenfieldSeq.addElement(superFields.elementAt(i));
754        }
755    
756        MethodDeclVec superMethods = superType.getMethods();
757        for( int i=0; i<superMethods.size(); i++ ) {
758            MethodDecl superMethod = superMethods.elementAt(i);
759            //@ assume superMethod.hasParent;  // "ensures"
760            
761            /* <<>>
762             *
763             * If superType is an interface, ignore any method's it may
764             * have inherited from java.lang.Object; The methods of
765             * java.lang.Object will either already been added via a
766             * superclass (if type is a class) or will be added separately
767             * at the end (if type is an interface).
768             *
769             * This ensures that the methods of java.lang.Object inherited
770             * from an interface never override anything.
771             */
772            if (superMethod.parent == jLOTypeDecl &&
773                (superType.getTypeDecl() instanceof InterfaceDecl))
774                continue;
775    
776    
777            // a class inherits from its direct supertypes all methods
778            // that are accessible and not overridden nor hidden 
779            
780            // Override (8.4.6.1) if declare instance method with same signature
781            // Hide (8.4.6.2) if declare static method with same signature
782            
783            // If inheriting an abstract method, 
784            // and class already has inherited non-abstract method
785            // with same sig, then the abstract method is overridden
786            // by the non-abstract method
787            
788            if( superMemberAccessible( type, superType, superMethod.modifiers,
789                                                    superMethod.pmodifiers ) ) 
790              {
791                
792                // Extract signature to check if overridden or hidden
793                Type[] argTypes = Types.getFormalParaTypes( superMethod.args );
794                
795                MethodDecl overridingMethod = 
796                  declaresMethod( type, superMethod.id, argTypes );
797                
798                if( overridingMethod == null ) {
799                  // The decl does not declare such a method
800                  
801                  if( Modifiers.isAbstract(superMethod.modifiers) ) 
802                    {
803                      
804                      // Check if overridden by concrete method in Vec
805                      for( int k=0; k<methodSeq.size(); k++ ) 
806                        {
807                          MethodDecl md = (MethodDecl) methodSeq.elementAt(k);
808                          //@ assume md.hasParent;  // "invariant"
809                          
810                          if( ! Modifiers.isAbstract(md.modifiers)
811                             && Types.isSameMethodSig( md, superMethod ) ) 
812                            {
813                              // This abstract method is overridden
814                              overridingMethod = md;
815                            }
816                        }
817                    }
818                }
819                
820                if( overridingMethod == null ) 
821                  {
822                    // Not overridden
823                    methodSeq.addElement( superMethod );
824                  } 
825                else 
826                  {
827                    // Variety of checks between overridden and overriding methods
828                    if( Modifiers.isFinal(superMethod.modifiers) )
829                      ErrorSet.error(overridingMethod.loc,
830                                     "Attempt to override or hide a final method");
831                    
832                    if (Modifiers.isStatic(overridingMethod.modifiers) 
833                        && !Modifiers.isStatic(superMethod.modifiers) ) 
834                      ErrorSet.error(overridingMethod.loc,
835                                     "Static method hides an instance method");
836                    
837                    if(!Modifiers.isStatic(overridingMethod.modifiers)
838                       && Modifiers.isStatic(superMethod.modifiers) ) 
839                      ErrorSet.error(overridingMethod.loc,
840                                     "Instance method overrides a static method");
841                    
842                    if( !Types.isSameType(overridingMethod.returnType, 
843                                          superMethod.returnType ) ) 
844                      ErrorSet.error(overridingMethod.loc,
845                             "Different return types on overridden(hidden) and "+
846                                     "overriding(hiding) methods");
847                    
848                    if( !Types.isCompatibleRaises(overridingMethod.raises,
849                                                  superMethod.raises)
850                        && !(superMethod.parent.isBinary() ||
851                             overridingMethod.parent.isBinary()) )
852                      ErrorSet.error(overridingMethod.loc,
853                             "Incompatible throws clauses between "+
854                             "overridden(hidden) and overriding(hiding) methods");
855                    
856                    if( !Types.isCompatibleAccess(overridingMethod.modifiers 
857                                                  & Modifiers.ACCESS_MODIFIERS,
858                                                  superMethod.modifiers
859                                                  & Modifiers.ACCESS_MODIFIERS) ) {
860                      ErrorSet.error(overridingMethod.loc,
861                             "Incompatible access modifiers between "+
862                             "overridden(hidden) ["
863                              + Modifiers.toString(superMethod.modifiers & 
864                                    Modifiers.ACCESS_MODIFIERS)
865                              + ", " + Location.toString(superMethod.loc)
866                              + "] and overriding(hiding) methods ["
867                              + Modifiers.toString(overridingMethod.modifiers & 
868                                    Modifiers.ACCESS_MODIFIERS) + "]");
869                    }
870                    
871                    // Record that the method is overridden if it is not hidden:
872                    if (!Modifiers.isStatic(overridingMethod.modifiers)) {
873                      addOverride( overridingMethod, superMethod );
874                    }
875                    
876                  }
877              }
878        }
879      }                             // end addInheritedMembers
880      
881      
882      /** Check if a member is accessible from a direct subclass. */
883      
884      //@ requires type != null && superType != null;
885      protected boolean superMemberAccessible(TypeSig type, 
886                                            TypeSig superType, 
887                                            int modifiers,
888                                            ModifierPragmaVec pmodifiers ) {
889          
890          // if private then not inherited by subclass
891          // Only protected and public members are inherited by subclasses
892          // in a different package
893          
894          return (!Modifiers.isPrivate(modifiers)
895                  && (type.inSamePackageAs( superType )
896                      || Modifiers.isProtected(modifiers)
897                      || Modifiers.isPublic(modifiers) ));
898        }
899      
900      /** Check if a type declares a field. */
901      
902      //@ requires sig != null;
903      protected boolean declaresFieldJava(TypeSig sig, Identifier id ) {
904    
905        TypeDeclElemVec elems = sig.getTypeDecl().elems;    
906        for( int i=0; i<elems.size(); i++ ) {
907          TypeDeclElem elem = elems.elementAt(i);
908          if( elem.getTag() == TagConstants.FIELDDECL
909             && ((FieldDecl)elem).id.equals( id ) )
910            return true;
911        }
912        // Not found
913        return false;
914      }
915      
916      /** Check if a type declares a method. */
917      
918      //@ requires sig != null && \nonnullelements(argTypes);
919      //@ ensures \result != null ==> \result.hasParent;
920      private MethodDecl 
921        declaresMethod( TypeSig sig, Identifier id, Type[] argTypes ) 
922      {
923        TypeDeclElemVec elems = sig.getTypeDecl().elems;
924      search:
925        for( int i=0; i<elems.size(); i++ ) {
926          TypeDeclElem elem = elems.elementAt(i);
927          //@ assume elem.hasParent;  // "invariant"
928          if( elem.getTag() == TagConstants.METHODDECL ) {
929            MethodDecl md = (MethodDecl)elem;
930            if( md.id == id && md.args.size() == argTypes.length ) {
931              for( int j=0; j<argTypes.length; j++ ) {
932                if( !Types.isSameType(md.args.elementAt(j).type, 
933                                      argTypes[j] ) )
934                  // Not same sig
935                  continue search;
936              }
937              // Same sig
938              return md;
939            }
940          }
941        }
942        
943        // Not found
944        return null;
945      }
946      
947      // *********************************************************************
948      
949      //@ requires loc != Location.NULL;
950      public void checkModifiers(int modifiers, int allowed, int loc, String decl) {
951        for (int i = 0; i < Modifiers.SIZE_MODIFIER_BITSET; i++) {
952          int bit = 1<<i;
953          if ((modifiers & bit) != 0 && (allowed & bit) == 0)
954            ErrorSet.error(loc, "Modifier '" + Modifiers.name(i) +
955                           "' not allowed on " + decl + " declarations");
956        }
957      }
958      
959    
960        /**
961         * Check to make sure a supertype is accessible; reports an error
962         * to ErrorSet if not.<p>
963         *
964         * Here, supertype is a supertype of currentSig; this fact is
965         * declared at loc.  E.g., loc is the location of the supertype
966         * name in the extends or implements clause of currentSig.<p>
967         */
968        //@ requires loc != Location.NULL;
969        public void checkSuperTypeAccessible(/*@ non_null @*/ TypeSig currentSig,
970                                             /*@ non_null @*/ TypeSig supertype,
971                                             int loc) {
972    /* FIXME - this error is commented out because it incorrectly disallows
973     using a protected nested class of a public supertype that is not in 
974    the same package.
975     There are presumably situations this should check, but that will take
976     some research, and in any case, we could just leave them to java.
977    
978            // fix for 1.1: !!!!
979            if (! Modifiers.isPublic(supertype.getTypeDecl().modifiers)
980                && ! currentSig.inSamePackageAs(supertype))
981                ErrorSet.error(loc, "Supertype is not accessible.");
982    */
983        }
984    
985    
986        /**
987         * This routine constructs and returns the interface that all
988         * interfaces are de-facto subinterfaces of.<p>
989         *
990         * This interface is not an actual Java interface, but rather a
991         * made up one.  Its locations will be valid, but misleading.<p>
992         *
993         *
994         * The root interface is composed of all the public methods of
995         * java.lang.Object turned into abstract methods.<p>
996         */
997        //@ ensures \result != null;
998        public TypeSig getRootInterface() {
999            if (_rootCache != null)
1000                return _rootCache;
1001    
1002            TypeSig objSig = Types.javaLangObject();
1003            TypeDecl object = objSig.getTypeDecl();
1004            objSig.prep();
1005    
1006            TypeDeclElemVec newElems = TypeDeclElemVec.make();
1007            for(int i=0; i< object.elems.size(); i++) {
1008                TypeDeclElem e = object.elems.elementAt(i);
1009                if (!(e instanceof MethodDecl))
1010                    continue;
1011                MethodDecl m = (MethodDecl)e;
1012                if (!Modifiers.isPublic(m.modifiers)
1013                    || Modifiers.isStatic(m.modifiers))
1014                    continue;
1015    
1016                MethodDecl newM = MethodDecl.make(
1017                                    Modifiers.ACC_PUBLIC|Modifiers.ACC_ABSTRACT,
1018                                    m.pmodifiers,
1019                                    m.tmodifiers,
1020                                    m.args,
1021                                    m.raises,
1022                                    null /* body */,
1023                                    Location.NULL,
1024                                    m.loc,
1025                                    m.locId,
1026                                    m.locThrowsKeyword,
1027                                    m.id,
1028                                    m.returnType,
1029                                    m.locType);
1030                newElems.addElement(newM);
1031            }
1032    
1033            TypeDecl i = InterfaceDecl.make(Modifiers.ACC_PUBLIC,
1034                                            null /*pmodifiers*/,
1035                                            object.id,
1036                                            TypeNameVec.make(),
1037                                            null,
1038                                            newElems,
1039                                            object.loc,
1040                                            object.locId,
1041                                            object.locOpenBrace,
1042                                            object.locCloseBrace);
1043            _rootCache = Types.makeTypeSig(objSig.packageName,
1044                                     "<the root interface>",
1045                                     null, i, objSig.getCompilationUnit());
1046    
1047            // PrettyPrint.inst.print(System.out, 0, i);
1048    
1049            return _rootCache;
1050        }
1051    
1052    
1053        protected TypeSig _rootCache = null;
1054    
1055    
1056    
1057        //@ ensures \result != null;
1058        public javafe.tc.TypeSig processTypeNameAnnotations(/*@ non_null @*/ TypeName tn,
1059                                                            /*@ non_null @*/javafe.tc.TypeSig sig,
1060                                                            Env env) {
1061            return sig;
1062        }
1063    
1064        //@ ensures \result != null;
1065        protected EnvForTypeSig getEnvForCurrentSig(/*@ non_null @*/ TypeSig sig,
1066                                                    boolean isStatic) {
1067          return sig.getEnv(isStatic);
1068        }
1069        
1070      }