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 }