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                TypeDecl decl = currentSig.getTypeDecl();
226                TypeDeclElemVec elemvec = (TypeDeclElemVec)Utils.representsDecoration.get(decl);
227                // REVIEW: I added robustness in case elemvec is null, but is it allowed to be null
228                //   here in the first place?
229                if (elemvec == null)
230                {
231                  elemvec = TypeDeclElemVec.make();
232                  Utils.representsDecoration.set(decl, elemvec);
233                }
234                elemvec.addElement(e);
235            } else 
236                super.visitTypeDeclElem(e,currentSig,abstractMethodsOK, 
237                            inFinalClass, inInterface);
238        }
239    
240        public void visitMethodDecl(MethodDecl x, TypeSig currentSig,
241                            boolean abstractMethodsOK,
242                            boolean inFinalClass,
243                            boolean inInterface) {
244            if (Utils.findModifierPragma(x.pmodifiers,TagConstants.MODEL) == null) {
245                super.visitMethodDecl(x,currentSig,abstractMethodsOK,inFinalClass,inInterface);
246            } else {
247    
248            // Careful - the following is almost, but not quite, a duplicate of super.visitMethodDecl 
249    
250        if (Modifiers.isStatic(x.modifiers) && !inInterface
251            && !currentSig.isTopLevelType())
252            ErrorSet.error(x.locId,
253                           "Only methods of top-level classes may be static");
254    
255        // Modifiers can only be:
256        //   public protected private abstract static final synchronized native
257        //   strictfp
258        checkModifiers( x.modifiers,
259                       inInterface
260                       ? (Modifiers.ACC_PUBLIC | Modifiers.ACC_ABSTRACT | Modifiers.ACC_STATIC)
261                       : (Modifiers.ACCESS_MODIFIERS | Modifiers.ACC_ABSTRACT
262                       | Modifiers.ACC_FINAL | Modifiers.ACC_SYNCHRONIZED
263                       | Modifiers.ACC_STATIC | Modifiers.ACC_NATIVE
264                       | Modifiers.ACC_STRICT),
265                       x.loc, inInterface ? "interface method" : "method" );
266    
267        // If in interface, method is implicitly public
268        // But model methods are not implicitly abstract
269        if( inInterface )
270            x.modifiers |= Modifiers.ACC_PUBLIC;
271    
272        // private methods implicitly final
273        // members of final class are implicitly final
274        if( Modifiers.isPrivate(x.modifiers) || inFinalClass )
275          x.modifiers |= Modifiers.ACC_FINAL;
276    
277        // Error if an abstract method is also
278        // private, static, final, native, or synchronized.
279        if( Modifiers.isAbstract(x.modifiers) &&
280           (Modifiers.isPrivate(x.modifiers)
281            | Modifiers.isStatic(x.modifiers)
282            | Modifiers.isFinal(x.modifiers)
283            | Modifiers.isNative(x.modifiers)
284            | Modifiers.isSynchronized(x.modifiers)) )
285          ErrorSet.error( x.locId,
286            "Incompatible modifiers for abstract method");
287    
288        // resolve types
289         getEnvForCurrentSig(currentSig, true).resolveType( currentSig, x.returnType
290     );
291        for( int i=0; i<x.raises.size(); i++ )
292          getEnvForCurrentSig(currentSig, true).resolveType( currentSig, x.raises.elementAt(i) );
293        for( int i=0; i<x.args.size(); i++ )
294          getEnvForCurrentSig(currentSig, true).resolveType( currentSig, x.args.elementAt(i).type );
295    
296        // Error if two methods in type body with same signature
297        for( int i=0; i<methodSeq.size(); i++ )
298          {
299            if(Types.isSameMethodSig( x, (MethodDecl)methodSeq.elementAt(i) ) )
300              ErrorSet.error(x.loc,
301                             "Duplicate declaration of method "
302                             +"with same signature");
303          }
304    
305        methodSeq.addElement(x);
306    
307        }
308        }
309    
310        protected void addInheritedMembers(javafe.tc.TypeSig type,
311                                           javafe.tc.TypeSig superType) {
312    
313            super.addInheritedMembers(type,superType);
314            if (!(superType instanceof escjava.tc.TypeSig) ) return;
315    
316            escjava.tc.TypeSig st = (escjava.tc.TypeSig)superType;
317            for (int i=0; i<st.jmlFields.size(); ++i) {
318                FieldDecl fd = st.jmlFields.elementAt(i);
319                if (jmlFieldsSeq.contains(fd) ||
320                    jmlHiddenFieldsSeq.contains(fd)) {
321                    // skip
322                } else if (!superMemberAccessible(type,superType,fd.modifiers,
323                                                    fd.pmodifiers)) {
324                    jmlHiddenFieldsSeq.addElement(fd);
325                } else if (declaresField(type,fd.id,numJmlFields)) {
326                    // If the field is declared in this class (not inherited) as
327                    // either a java or jml field, then the super field is hidden
328                    jmlHiddenFieldsSeq.addElement(fd);
329                } else {
330                    // If the field is somehow inherited as a java field, but is
331                    // also inherited as a jml field, then for jml name lookup
332                    // it is considered an ambiguous reference.
333                    boolean found = false;
334                    for (int ii=0; ii<fieldSeq.size(); ++ii) {
335                        FieldDecl fdj = (FieldDecl)fieldSeq.elementAt(ii);
336                        if (fdj.id.equals(fd.id)) { found = true; break; }
337                    }
338                    if (!found) jmlFieldsSeq.addElement(fd);
339                    else        jmlDupFieldsSeq.addElement(fd);
340                    // FIXME - but this only checks the java fields that have
341                    // been added via addInheritedMembers so far - there might
342                    // be more interfaces to come. ???
343                }
344            }
345            for (int i=0; i<st.jmlHiddenFields.size(); ++i) {
346                jmlHiddenFieldsSeq.addElement(st.jmlHiddenFields.elementAt(i));
347            }
348            TypeDeclElemVec mpv = (TypeDeclElemVec)Utils.representsDecoration.get(type.getTypeDecl());
349            TypeDeclElemVec mpvsuper = (TypeDeclElemVec)Utils.representsDecoration.get(st.getTypeDecl());
350    
351            // REVIEW: I added robustness in case mpv is null, but is it allowed to be null
352            //   in the first place?
353            if (st.getTypeDecl() instanceof ClassDecl) {
354                if (mpv != null)
355                    mpv.append(mpvsuper);
356                else
357                    Utils.representsDecoration.set(type.getTypeDecl(), TypeDeclElemVec.make (mpvsuper.toArray()));
358            } else {
359                if (mpv != null)
360                    mpv.append(mpvsuper);
361                else
362                    Utils.representsDecoration.set(type.getTypeDecl(), TypeDeclElemVec.make (mpvsuper.toArray()));
363                    //interfaces get them from Object as well ?
364                    // FIXME - no dups
365                //for (int i=0; i<mpvsuper.size(); ++i) 
366            }
367        }
368    
369        protected boolean superMemberAccessible(javafe.tc.TypeSig type,
370                                            javafe.tc.TypeSig superType,
371                                            int modifiers,
372                                            ModifierPragmaVec pmodifiers) {
373            if (Utils.findModifierPragma(pmodifiers,TagConstants.SPEC_PUBLIC)
374                    != null) return true;
375            if (Utils.findModifierPragma(pmodifiers,TagConstants.SPEC_PROTECTED)
376                    != null) return true;
377            return super.superMemberAccessible(type,superType,modifiers,pmodifiers);
378        }
379    
380    /*
381        protected FieldDecl alreadyDeclared(Identifier id) {
382            for (int i=0; i<jmlFieldsSeq.size(); ++i) {
383                if (id.equals(((FieldDecl)jmlFieldsSeq.elementAt(i)).id)) 
384                    return (FieldDecl)jmlFieldsSeq.elementAt(i);
385            }
386            for (int i=0; i<fieldSeq.size(); ++i) {
387                if (id.equals(((FieldDecl)fieldSeq.elementAt(i)).id)) 
388                    return (FieldDecl)fieldSeq.elementAt(i);
389            }
390            return null;
391        }
392    */
393    
394        protected boolean declaresField(javafe.tc.TypeSig sig, Identifier id) {
395            return declaresField(sig,id,jmlFieldsSeq.size());
396        }
397    
398        private boolean declaresField(javafe.tc.TypeSig sig, Identifier id, int n) {
399                // The following returns true iff sig declares the field as a
400                // java field and does not inherit it from a parent 
401            boolean b = declaresFieldJava(sig,id);
402            if (b || !(sig instanceof escjava.tc.TypeSig)) return b;
403            for (int i=0; i<n; ++i) {
404                if (id.equals(((FieldDecl)jmlFieldsSeq.elementAt(i)).id)) return true;
405            }
406            for (int i=0; i<jmlHiddenFieldsSeq.size(); ++i) {
407                if (id.equals(((FieldDecl)jmlHiddenFieldsSeq.elementAt(i)).id)) return true;
408            }
409            for (int i=0; i<jmlDupFieldsSeq.size(); ++i) {
410                if (id.equals(((FieldDecl)jmlDupFieldsSeq.elementAt(i)).id)) return true;
411            }
412            return false;
413        }
414    
415        public javafe.tc.TypeSig getRootInterface() {
416            if (_rootCache != null) return _rootCache;
417            javafe.tc.TypeSig ts = super.getRootInterface();
418            InterfaceDecl td = (InterfaceDecl) ts.getTypeDecl();
419            // Add in any ghost or model fields
420    
421            TypeDecl object = Types.javaLangObject().getTypeDecl();
422            for (int i=0; i<object.elems.size(); ++i) {
423                TypeDeclElem e = object.elems.elementAt(i);
424    // FIXME - should really only do inherited elements
425    // FIXME - what about inherited model methods, types?
426                if ((e instanceof ModelDeclPragma)
427                    || (e instanceof GhostDeclPragma)
428                    || (e instanceof FieldDecl)) {
429                    if (!Modifiers.isStatic(e.getModifiers())) {
430                        e.getPModifiers().addElement(
431                            SimpleModifierPragma.make(TagConstants.INSTANCE,Location.NULL));
432                    }
433                    td.elems.addElement(e);
434                }
435            }
436    
437            _rootCache = ts;
438            return _rootCache;
439    
440    
441        }
442    
443    }