    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      }