    001    package escjava.tc;
    002
    003    import javafe.ast.TypeDeclElem;
    004    import javafe.tc.TypeSig;
    005    import javafe.ast.Expr;
    006    import javafe.ast.FieldAccess;
    007    import javafe.ast.FieldDecl;
    008    import javafe.ast.FieldDeclVec;
    009    import javafe.ast.MethodDecl;
    010    import javafe.ast.TypeDecl;
    011    import javafe.ast.ClassDecl;
    012    import javafe.ast.InterfaceDecl;
    013    import javafe.ast.Identifier;
    014    import javafe.ast.TypeNameVec;
    015    import javafe.ast.TypeDeclElemVec;
    016    import javafe.ast.ModifierPragmaVec;
    017    import javafe.util.ErrorSet;
    018    import javafe.util.StackVector;
    019    import javafe.util.Location;
    020    import escjava.ast.GhostDeclPragma;
    021    import escjava.ast.ModelDeclPragma;
    022    import escjava.ast.ModelMethodDeclPragma;
    023    import escjava.ast.ModelConstructorDeclPragma;
    024    import escjava.ast.ModelTypePragma;
    025    import escjava.ast.SimpleModifierPragma;
    026    import escjava.ast.Modifiers;
    027    import escjava.ast.TagConstants;
    028    import escjava.ast.Utils;
    029    import escjava.ast.NamedExprDeclPragma;
    030
    031    public class PrepTypeDeclaration extends javafe.tc.PrepTypeDeclaration {
    032
    033        public PrepTypeDeclaration() {
    034            inst = this;
    035        }
    036
    037        protected /*@ non_null */ StackVector jmlFieldsSeq = new StackVector();
    038        protected /*@ non_null */ StackVector jmlHiddenFieldsSeq= new StackVector();
    039        protected /*@ non_null */ StackVector jmlDupFieldsSeq = new StackVector();
    040
    041        private int numJmlFields = -1;
    042        private java.util.LinkedList numJmlList = new java.util.LinkedList();
    043
    044        public void prepStart(TypeSig sig, TypeDecl decl) {
    045            super.prepStart(sig,decl);
    046            if (sig instanceof escjava.tc.TypeSig) {
    047                jmlFieldsSeq.push();
    048                jmlHiddenFieldsSeq.push();
    049                jmlDupFieldsSeq.push();
    050                Utils.representsDecoration.set(decl, TypeDeclElemVec.make());
    051                numJmlList.addFirst(new Integer(numJmlFields));
    052                numJmlFields = -1;
    053            }
    054        }
    055
    056        public void prepEnd(TypeSig sig, TypeDecl decl) {
    057            super.prepEnd(sig,decl);
    058            if (! (sig instanceof escjava.tc.TypeSig)) return;
    059            escjava.tc.TypeSig s = (escjava.tc.TypeSig)sig;
    060            s.jmlFields = FieldDeclVec.popFromStackVector(jmlFieldsSeq);
    061            s.jmlHiddenFields = FieldDeclVec.popFromStackVector(jmlHiddenFieldsSeq);
    062            s.jmlDupFields = FieldDeclVec.popFromStackVector(jmlDupFieldsSeq);
    063            numJmlFields = ((Integer)numJmlList.removeFirst()).intValue();
    064
    065            if (!escjava.Main.options().showFields) return;
    066            System.out.println("DUMP " + sig );
    067            print("Java fields",sig.getFieldsRaw());
    068            print("Hidden Java fields",sig.getHiddenFields());
    069            print("Jml fields",s.jmlFields);
    070            print("Jml hidden fields",s.jmlHiddenFields);
    071            if (s.jmlDupFields.size() != 0) print("Jml dup fields",s.jmlDupFields);
    072            System.out.println(" DUMP-END");
    073        }
    074
    075        public void print(String s, FieldDeclVec fdv ) {
    076            System.out.println(" " + s);
    077            for (int i=0; i<fdv.size(); ++i) {
    078                    System.out.println("    "+ fdv.elementAt(i).id + " " + Location.toString(fdv.elementAt(i).getStartLoc()));
    079            }
    080        }
    081
    082        protected void startSupers() {
    083            numJmlFields = jmlFieldsSeq.size();
    084            super.startSupers();
    085        }
    086
    087        protected void checkSuperInterfaces(javafe.tc.TypeSig sig,
    088                                            TypeNameVec superInterfaces) {
    089            super.checkSuperInterfaces(sig,superInterfaces);
    090        }
    091
    092        protected void visitTypeDeclElem(/*@ non_null @*/ TypeDeclElem e,
    093                                     /*@ non_null @*/ TypeSig currentSig,
    094                                     boolean abstractMethodsOK,
    095                                     boolean inFinalClass,
    096                                     boolean inInterface ) {
    097            if (e instanceof GhostDeclPragma ||
    098                e instanceof ModelDeclPragma) {
    099                boolean isModel = e instanceof ModelDeclPragma;
    100                String jmltype;
    101                FieldDecl x;
    102                if (isModel) {
    103                    ModelDeclPragma g = (ModelDeclPragma)e;
    104                    x = g.decl;
    105                    jmltype = "model";
    106                } else {
    107                    GhostDeclPragma g = (GhostDeclPragma)e;
    108                    x = g.decl;
    109                    jmltype = "ghost";
    110                }
    111
    112    /* DOne in FLowInsensitiveChecks
    113                FieldDecl ad = alreadyDeclared(x.id);
    114                if (ad != null) {
    115                    ErrorSet.error(x.getStartLoc(),
    116                        "Identifier has already been declared",
    117                        ad.getStartLoc());
    118                }
    119    */
    120
    121                jmlFieldsSeq.addElement(x);
    122
    123                if (Modifiers.isStatic(x.modifiers) && !inInterface
    124                    && !currentSig.isTopLevelType() && !Modifiers.isFinal(x.modifiers))
    125                    ErrorSet.error(x.locId,
    126                      "Inner classes may not declare static members, unless they" +
    127                      " are compile-time constant fields");
    128
    129                // ghost fields differ from regular fields in that transient and
    130                // volatile do not apply to them
    131                // We have a special case of field decls in an interface that are
    132                // inherited from java.lang.Object - they might be protected
    133                boolean fromClass = x.parent instanceof ClassDecl;
    134                checkModifiers( x.modifiers,
    135                    (!inInterface ? Modifiers.ACCESS_MODIFIERS :
    136                     !fromClass ? Modifiers.ACC_PUBLIC :
    137                       Modifiers.ACC_PUBLIC|Modifiers.ACC_PROTECTED)
    138                                     | Modifiers.ACC_FINAL | Modifiers.ACC_STATIC ,
    139                    x.locId, jmltype + (inInterface ? " interface field" : " field"));
    140
    141                // ghost fields in an interface are implicitly public
    142                // they are not implicitly final as Java fields are
    143                // they are implicitly static only if they are not declared instance
    144                if (inInterface) {
    145                    x.modifiers |= Modifiers.ACC_PUBLIC;
    146                    if (Utils.findModifierPragma(
    147                            x.pmodifiers, TagConstants.INSTANCE) == null) {
    148                        x.modifiers |= Modifiers.ACC_STATIC;
    149                    }
    150                }
    151
    152                // FIXME - Java fields check for duplicate type names here
    153                // where is this done for ghost fields; also I don't think there
    154                // is a check anywhere that a ghost field is hiding a
    155                // super class Java field (or enclosing class Java field)
    156
    157                getEnvForCurrentSig(currentSig, true).resolveType( currentSig, x.type);
    158
    159            } else if (e instanceof MethodDecl) {
    160
    161                MethodDecl md = (MethodDecl)e;
    162                boolean isAbstract = Modifiers.isAbstract(md.modifiers);
    163
    164                visitMethodDecl(md,currentSig,abstractMethodsOK,
    165                            inFinalClass, inInterface);
    166
    167                if (!isAbstract && md.body != null
    168                    && Utils.findModifierPragma(md.pmodifiers,TagConstants.MODEL) != null)
    169                    md.modifiers = md.modifiers & ~ Modifiers.ACC_ABSTRACT;
    170
    171    /*
    172            These are not needed at present because routines and types are
    173            converted into regular Java routines and types prior to any
    174            type prepping or type checking.  However, this causes some scope
    175            problems.  When those are fixed, we may need to prep these types
    176            here in a manner similar to that done in javafe.tc.PrepTypeDeclaration
    177
    178            } else if (e instanceof ModelMethodDeclPragma) {
    179                ModelMethodDeclPragma g = (ModelMethodDeclPragma)e;
    180                MethodDecl x = g.decl;
    181
    182                if (Modifiers.isStatic(x.modifiers) && !inInterface
    183                    && !currentSig.isTopLevelType())
    184                    ErrorSet.error(x.locId,
    185                            "Only methods of top-level classes may be static");
    186
    187                if (inInterface)
    188                    checkModifiers( x.modifiers,
    189                            Modifiers.ACC_PUBLIC | Modifiers.ACC_ABSTRACT,
    190                            x.loc, "model interface method");
    191                else
    192                    checkModifiers( x.modifiers, Modifiers.ACCESS_MODIFIERS |
    193                            Modifiers.ACC_ABSTRACT | Modifiers.ACC_FINAL |
    194                            Modifiers.ACC_SYNCHRONIZED | Modifiers.ACC_STATIC |
    195                            Modifiers.ACC_STRICT,
    196                            x.loc, "model method");
    197                    // Model methods may not be native
    198
    199                if (inInterface)
    200                    x.modifiers |= Modifiers.ACC_ABSTRACT | Modifiers.ACC_PUBLIC;
    201
    202                if (Modifiers.isPrivate(x.modifiers) || inFinalClass)
    203                    x.modifiers |= Modifiers.ACC_FINAL;
    204
    205                if (Modifiers.isAbstract(x.modifiers) &&
    206                    (Modifiers.isPrivate(x.modifiers) |
    207                     Modifiers.isStatic(x.modifiers)  |
    208                     Modifiers.isFinal(x.modifiers)  |
    209                     Modifiers.isNative(x.modifiers)  |
    210                     Modifiers.isSynchronized(x.modifiers)) )
    211                    ErrorSet.error (x.locId,
    212                        "Incompatible modifiers for an abstract method");
    213
    214                    // FIXME - resolve types
    215                    // FIXME - check for duplicate method ids
    216                    System.out.println("MODEL METHOD PRAGMA");
    217
    218            } else if (e instanceof ModelConstructorDeclPragma) {
    219                    // FIXME - stuff from non-model constructor
    220                    System.out.println("MODEL CONSTRUCTOR PRAGMA");
    221            } else if (e instanceof ModelTypePragma) {
    222                    System.out.println("MODEL TYPE PRAGMA");
    223    */
    224            } else if (e instanceof NamedExprDeclPragma) {
    225                ((TypeDeclElemVec)Utils.representsDecoration.get(currentSig.getTypeDecl())).addElement(e);
    226            } else
    227                super.visitTypeDeclElem(e,currentSig,abstractMethodsOK,
    228                            inFinalClass, inInterface);
    229        }
    230
    231        public void visitMethodDecl(MethodDecl x, TypeSig currentSig,
    232                            boolean abstractMethodsOK,
    233                            boolean inFinalClass,
    234                            boolean inInterface) {
    235            if (Utils.findModifierPragma(x.pmodifiers,TagConstants.MODEL) == null) {
    236                super.visitMethodDecl(x,currentSig,abstractMethodsOK,inFinalClass,inInterface);
    237            } else {
    238
    239            // Careful - the following is almost, but not quite, a duplicate of super.visitMethodDecl
    240
    241        if (Modifiers.isStatic(x.modifiers) && !inInterface
    242            && !currentSig.isTopLevelType())
    243            ErrorSet.error(x.locId,
    244                           "Only methods of top-level classes may be static");
    245
    246        // Modifiers can only be:
    247        //   public protected private abstract static final synchronized native
    248        //   strictfp
    249        checkModifiers( x.modifiers,
    250                       inInterface
    251                       ? (Modifiers.ACC_PUBLIC | Modifiers.ACC_ABSTRACT | Modifiers.ACC_STATIC)
    252                       : (Modifiers.ACCESS_MODIFIERS | Modifiers.ACC_ABSTRACT
    253                       | Modifiers.ACC_FINAL | Modifiers.ACC_SYNCHRONIZED
    254                       | Modifiers.ACC_STATIC | Modifiers.ACC_NATIVE
    255                       | Modifiers.ACC_STRICT),
    256                       x.loc, inInterface ? "interface method" : "method" );
    257
    258        // If in interface, method is implicitly public
    259        // But model methods are not implicitly abstract
    260        if( inInterface )
    261            x.modifiers |= Modifiers.ACC_PUBLIC;
    262
    263        // private methods implicitly final
    264        // members of final class are implicitly final
    265        if( Modifiers.isPrivate(x.modifiers) || inFinalClass )
    266          x.modifiers |= Modifiers.ACC_FINAL;
    267
    268        // Error if an abstract method is also
    269        // private, static, final, native, or synchronized.
    270        if( Modifiers.isAbstract(x.modifiers) &&
    271           (Modifiers.isPrivate(x.modifiers)
    272            | Modifiers.isStatic(x.modifiers)
    273            | Modifiers.isFinal(x.modifiers)
    274            | Modifiers.isNative(x.modifiers)
    275            | Modifiers.isSynchronized(x.modifiers)) )
    276          ErrorSet.error( x.locId,
    277            "Incompatible modifiers for abstract method");
    278
    279        // resolve types
    280         getEnvForCurrentSig(currentSig, true).resolveType( currentSig, x.returnType
    281     );
    282        for( int i=0; i<x.raises.size(); i++ )
    283          getEnvForCurrentSig(currentSig, true).resolveType( currentSig, x.raises.elementAt(i) );
    284        for( int i=0; i<x.args.size(); i++ )
    285          getEnvForCurrentSig(currentSig, true).resolveType( currentSig, x.args.elementAt(i).type );
    286
    287        // Error if two methods in type body with same signature
    288        for( int i=0; i<methodSeq.size(); i++ )
    289          {
    290            if(Types.isSameMethodSig( x, (MethodDecl)methodSeq.elementAt(i) ) )
    291              ErrorSet.error(x.loc,
    292                             "Duplicate declaration of method "
    293                             +"with same signature");
    294          }
    295
    296        methodSeq.addElement(x);
    297
    298        }
    299        }
    300
    301        protected void addInheritedMembers(javafe.tc.TypeSig type,
    302                                           javafe.tc.TypeSig superType) {
    303
    304            super.addInheritedMembers(type,superType);
    305            if (!(superType instanceof escjava.tc.TypeSig) ) return;
    306
    307            escjava.tc.TypeSig st = (escjava.tc.TypeSig)superType;
    308            for (int i=0; i<st.jmlFields.size(); ++i) {
    309                FieldDecl fd = st.jmlFields.elementAt(i);
    310                if (jmlFieldsSeq.contains(fd) ||
    311                    jmlHiddenFieldsSeq.contains(fd)) {
    312                    // skip
    313                } else if (!superMemberAccessible(type,superType,fd.modifiers,
    314                                                    fd.pmodifiers)) {
    315                    jmlHiddenFieldsSeq.addElement(fd);
    316                } else if (declaresField(type,fd.id,numJmlFields)) {
    317                    // If the field is declared in this class (not inherited) as
    318                    // either a java or jml field, then the super field is hidden
    319                    jmlHiddenFieldsSeq.addElement(fd);
    320                } else {
    321                    // If the field is somehow inherited as a java field, but is
    322                    // also inherited as a jml field, then for jml name lookup
    323                    // it is considered an ambiguous reference.
    324                    boolean found = false;
    325                    for (int ii=0; ii<fieldSeq.size(); ++ii) {
    326                        FieldDecl fdj = (FieldDecl)fieldSeq.elementAt(ii);
    327                        if (fdj.id.equals(fd.id)) { found = true; break; }
    328                    }
    329                    if (!found) jmlFieldsSeq.addElement(fd);
    330                    else        jmlDupFieldsSeq.addElement(fd);
    331                    // FIXME - but this only checks the java fields that have
    332                    // been added via addInheritedMembers so far - there might
    333                    // be more interfaces to come. ???
    334                }
    335            }
    336            for (int i=0; i<st.jmlHiddenFields.size(); ++i) {
    337                jmlHiddenFieldsSeq.addElement(st.jmlHiddenFields.elementAt(i));
    338            }
    339            TypeDeclElemVec mpv = (TypeDeclElemVec)Utils.representsDecoration.get(type.getTypeDecl());
    340            TypeDeclElemVec mpvsuper = (TypeDeclElemVec)Utils.representsDecoration.get(st.getTypeDecl());
    341            if (st.getTypeDecl() instanceof ClassDecl) {
    342                mpv.append(mpvsuper);
    343            } else {
    344                mpv.append(mpvsuper);
    345                    //interfaces get them from Object as well ?
    346                    // FIXME - no dups
    347                //for (int i=0; i<mpvsuper.size(); ++i)
    348            }
    349        }
    350
    351        protected boolean superMemberAccessible(javafe.tc.TypeSig type,
    352                                            javafe.tc.TypeSig superType,
    353                                            int modifiers,
    354                                            ModifierPragmaVec pmodifiers) {
    355            if (Utils.findModifierPragma(pmodifiers,TagConstants.SPEC_PUBLIC)
    356                    != null) return true;
    357            if (Utils.findModifierPragma(pmodifiers,TagConstants.SPEC_PROTECTED)
    358                    != null) return true;
    359            return super.superMemberAccessible(type,superType,modifiers,pmodifiers);
    360        }
    361
    362    /*
    363        protected FieldDecl alreadyDeclared(Identifier id) {
    364            for (int i=0; i<jmlFieldsSeq.size(); ++i) {
    365                if (id.equals(((FieldDecl)jmlFieldsSeq.elementAt(i)).id))
    366                    return (FieldDecl)jmlFieldsSeq.elementAt(i);
    367            }
    368            for (int i=0; i<fieldSeq.size(); ++i) {
    369                if (id.equals(((FieldDecl)fieldSeq.elementAt(i)).id))
    370                    return (FieldDecl)fieldSeq.elementAt(i);
    371            }
    372            return null;
    373        }
    374    */
    375
    376        protected boolean declaresField(javafe.tc.TypeSig sig, Identifier id) {
    377            return declaresField(sig,id,jmlFieldsSeq.size());
    378        }
    379
    380        private boolean declaresField(javafe.tc.TypeSig sig, Identifier id, int n) {
    381                // The following returns true iff sig declares the field as a
    382                // java field and does not inherit it from a parent
    383            boolean b = declaresFieldJava(sig,id);
    384            if (b || !(sig instanceof escjava.tc.TypeSig)) return b;
    385            for (int i=0; i<n; ++i) {
    386                if (id.equals(((FieldDecl)jmlFieldsSeq.elementAt(i)).id)) return true;
    387            }
    388            for (int i=0; i<jmlHiddenFieldsSeq.size(); ++i) {
    389                if (id.equals(((FieldDecl)jmlHiddenFieldsSeq.elementAt(i)).id)) return true;
    390            }
    391            for (int i=0; i<jmlDupFieldsSeq.size(); ++i) {
    392                if (id.equals(((FieldDecl)jmlDupFieldsSeq.elementAt(i)).id)) return true;
    393            }
    394            return false;
    395        }
    396
    397        public javafe.tc.TypeSig getRootInterface() {
    398            if (_rootCache != null) return _rootCache;
    399            javafe.tc.TypeSig ts = super.getRootInterface();
    400            InterfaceDecl td = (InterfaceDecl) ts.getTypeDecl();
    401            // Add in any ghost or model fields
    402
    403            TypeDecl object = Types.javaLangObject().getTypeDecl();
    404            for (int i=0; i<object.elems.size(); ++i) {
    405                TypeDeclElem e = object.elems.elementAt(i);
    406    // FIXME - should really only do inherited elements
    407    // FIXME - what about inherited model methods, types?
    408                if ((e instanceof ModelDeclPragma)
    409                    || (e instanceof GhostDeclPragma)
    410                    || (e instanceof FieldDecl)) {
    411                    if (!Modifiers.isStatic(e.getModifiers())) {
    412                        e.getPModifiers().addElement(
    413                            SimpleModifierPragma.make(TagConstants.INSTANCE,Location.NULL));
    414                    }
    415                    td.elems.addElement(e);
    416                }
    417            }
    418
    419            _rootCache = ts;
    420            return _rootCache;
    421
    422
    423        }
    424
    425    }