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