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    }