001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package escjava; 004 005 import javafe.ast.CompilationUnit; 006 import javafe.ast.LexicalPragmaVec; 007 import javafe.ast.Modifiers; 008 import javafe.ast.Identifier; 009 import javafe.ast.Name; 010 import javafe.ast.*; 011 import javafe.ast.TypeDecl; 012 import javafe.ast.TypeDeclVec; 013 import javafe.tc.TypeSig; 014 import javafe.ast.PrettyPrint; // Debugging methods only 015 import javafe.ast.StandardPrettyPrint; // Debugging methods only 016 import javafe.ast.DelegatingPrettyPrint; // Debugging methods only 017 import escjava.ast.EscPrettyPrint; // Debugging methods only 018 import javafe.util.Location; 019 import escjava.ast.RefinePragma; 020 import escjava.ast.*; 021 import escjava.ast.TagConstants; // Resolves ambiguity 022 //import escjava.reader.EscTypeReader; 023 024 import escjava.AnnotationHandler; 025 import javafe.genericfile.*; 026 import javafe.parser.PragmaParser; 027 import javafe.filespace.Tree; 028 import javafe.filespace.Query; 029 030 import javafe.util.Assert; 031 import javafe.util.ErrorSet; 032 import javafe.util.Info; 033 034 import javafe.reader.*; 035 import javafe.tc.OutsideEnv; 036 037 import java.util.ArrayList; 038 import java.util.Enumeration; 039 import java.util.HashMap; 040 import java.util.Map; 041 042 public class RefinementSequence extends CompilationUnit { 043 044 protected CompilationUnit javacu; 045 protected ArrayList refinements; // list of CompilationUnits 046 protected boolean hasJavaDef; 047 protected boolean javaIsBinary = false; 048 049 public ArrayList refinements() { return refinements; } 050 051 //@ requires refinements != null; 052 //@ requires refinements.size() > 0; 053 public RefinementSequence( 054 ArrayList refinements, // list of CompilationUnit 055 CompilationUnit javacu, 056 AnnotationHandler ah) { 057 this.refinements = refinements; 058 this.javacu = javacu; 059 hasJavaDef = javacu != null; 060 if (hasJavaDef) javaIsBinary = javacu.isBinary(); 061 062 // Put everything together 063 CompilationUnit newcu = consolidateRefinements(refinements,javacu); 064 065 // Copy results into self 066 pkgName = newcu.pkgName; 067 lexicalPragmas = newcu.lexicalPragmas; 068 imports = newcu.imports; 069 elems = newcu.elems; 070 loc = newcu.loc; 071 } 072 073 //@ requires refinements != null; 074 //-@ requires refinements.size() > 0; 075 CompilationUnit consolidateRefinements(ArrayList refinements, 076 CompilationUnit javacu) { 077 078 // There are two tasks. First we have to create a consolidated 079 // signature, consisting of both java and jml information. For 080 // the java information, we use the java or class file, if they 081 // are available, and do not allow anything to be added to that. 082 // If they are not available, we create the java signature by 083 // combining all disjoint type elements from the various 084 // refinement files. The jml signature is created by combining 085 // the various refinements. We have to do this now, prior to any 086 // type checking, so that the type signature registered for this 087 // type is accurate for other types to check against. [It would 088 // be better to establish and register all signatures, and then 089 // do any checking, but escjava is not organized that way.] 090 091 // Secondly, we have to combine all specifications. We are doing 092 // that here, before the typechecking. It is convenient to 093 // syntactically combine the specs, but the type names in the text 094 // are not resolved, causing difficulties in matching elements of 095 // type declarations. 096 // However, if we delay merging material until after all 097 // typechecking is performed, then it is complicated to register 098 // a type signature. Perhaps this can be worked around and is 099 // probably the better way in the long run, but for the moment 100 // the work is done here and the type comparisons are not real 101 // robust. FIXME -- DRCok 102 103 Info.out("Consolidating " + refinements.size() + " refinement; java file " + (hasJavaDef? "exists" : "does not exist")); 104 105 CompilationUnit lastcu = (CompilationUnit)refinements.get(refinements.size()-1); 106 107 // There are two cases in which we can avoid this work and just return 108 // the CU that we are given: 109 // - no Java CU and a single element of the refinement sequence 110 // - a Java CU that is the same as the single element of the RS 111 /* 112 if (refinements.size() == 1) { 113 CompilationUnit cu = (CompilationUnit)refinements.get(0); 114 if (javacu == null || javacu == cu) return cu; 115 } 116 */ 117 118 // Otherwise we set up a clean version of the types into which we 119 // put everything as we accumulate declarations from the RS. 120 121 // Variables into which to accumulate all the refinements 122 Name pkgName = (javacu==null?lastcu:javacu).pkgName; 123 LexicalPragmaVec lexicalPragmaVec = LexicalPragmaVec.make(); 124 ImportDeclVec imports = ImportDeclVec.make(); 125 TypeDeclVec types = TypeDeclVec.make(); 126 initblockmap = new HashMap(); 127 if (javacu != null) { 128 imports = javacu.imports.copy(); 129 types = cleancopy(javacu.elems); 130 } 131 IdentifierVec ids = IdentifierVec.make(3); 132 ids.addElement(Identifier.intern("org")); 133 ids.addElement(Identifier.intern("jmlspecs")); 134 ids.addElement(Identifier.intern("lang")); 135 int[] nulls = new int[] {Location.NULL,Location.NULL,Location.NULL}; 136 //@ assert nulls.length == ids.size(); 137 lexicalPragmaVec.addElement( ImportPragma.make( 138 OnDemandImportDecl.make(Location.NULL,CompoundName.make(ids, 139 nulls,nulls) ),Location.NULL) ); 140 141 int loc = ((CompilationUnit)refinements.get(0)).loc; 142 143 for (int k=refinements.size()-1; k>=0; --k) { 144 CompilationUnit cu = (CompilationUnit)refinements.get(k); 145 Info.out("Combining " + cu.sourceFile().getHumanName()); 146 147 //escjava.ast.EscPrettyPrint.inst.print(System.out,cu); 148 149 // Check that the package name is always consistent 150 String p = pkgName==null ? "" : pkgName.printName(); 151 String cp = cu.pkgName==null ? "" : cu.pkgName.printName(); 152 if (!cp.equals(p)) { 153 ErrorSet.error(cu.loc,"Package name does not match the package name in " + Location.toFile(loc).getHumanName() + ": " + 154 cp + " vs. " + p); 155 // FIXME - try this with the Name (does it have a location?) 156 // to improve the error message 157 } 158 159 // Combine all the NoWarn and Import pragmas 160 // (leave out RefinePragmas) 161 LexicalPragmaVec lexvec = cu.lexicalPragmas; 162 for (int i=0; i<lexvec.size(); ++i) { 163 LexicalPragma lexp = lexvec.elementAt(i); 164 if (!(lexp instanceof RefinePragma)) { 165 lexicalPragmaVec.addElement(lexp); 166 } 167 } 168 169 // Combine imports 170 // FIXME - this may duplicate a lot of them 171 // FIXME - might adding imports change the interpretation of any types? 172 imports.append(cu.imports); 173 174 // Stick in any top-level model type declarations 175 /* 176 TypeDeclElemVec tdev = cu.otherPragmas; 177 for (int kk=0; kk<tdev.size(); ++kk) { 178 TypeDeclElem tde = tdev.elementAt(kk); 179 if (tde instanceof ModelTypePragma) { 180 types.addElement( ((ModelTypePragma)tde).decl ); 181 } else { 182 System.out.println("NOT A MODEL TYPE " + tde.getClass() + " " + tde); 183 } 184 } 185 */ 186 187 TypeDeclElemVec tdev = cu.otherPragmas; 188 for (int kk=0; kk<tdev.size(); ++kk) { 189 TypeDeclElem tde = tdev.elementAt(kk); 190 if (!(tde instanceof ModelTypePragma)) { 191 System.out.println("NOT A MODEL TYPE " + tde.getClass() + " " + tde); 192 continue; 193 } 194 TypeDecl td = ((ModelTypePragma)tde).decl; 195 boolean foundMatch = false; 196 for (int j=0; j<types.size(); ++j) { 197 if (types.elementAt(j).id.equals(td.id)) { 198 foundMatch = true; 199 combineType(td,types.elementAt(j),true); 200 break; 201 } 202 } 203 if (!foundMatch) { 204 // model types need not have a Java declaration 205 types.addElement(td); 206 } 207 } 208 // Combine all of the top-level type declarations 209 TypeDeclVec typevec = cu.elems; 210 for (int i=0; i<typevec.size(); ++i) { 211 TypeDecl td = typevec.elementAt(i); 212 boolean foundMatch = false; 213 for (int j=0; j<types.size(); ++j) { 214 if (types.elementAt(j).id.equals(td.id)) { 215 foundMatch = true; 216 combineType(td,types.elementAt(j),!hasJavaDef); 217 break; 218 } 219 } 220 if (!foundMatch) { 221 if (!hasJavaDef) { 222 types.addElement(td); 223 } else { 224 ErrorSet.error(td.getStartLoc(), 225 "Type declaration is not in the java file"); 226 } 227 } 228 } 229 } 230 return CompilationUnit.make(pkgName,lexicalPragmaVec,imports,types,loc,null); 231 } 232 233 void combineFields(FieldDecl newfd, FieldDecl fd) { 234 if (newfd.modifiers != fd.modifiers) { 235 ErrorSet.error(newfd.getStartLoc(), 236 "Field has been redeclared with different Java modifiers", 237 fd.getStartLoc()); 238 } 239 // DOes it matter if we duplicate pragmas ? -- FIXME 240 if (newfd.pmodifiers != null) { 241 if (fd.pmodifiers == null) 242 fd.pmodifiers = newfd.pmodifiers.copy(); 243 else fd.pmodifiers.append(newfd.pmodifiers); 244 } 245 if (newfd.init != null && fd.init != newfd.init && 246 Utils.findModifierPragma(newfd.pmodifiers,TagConstants.GHOST) 247 == null) { 248 ErrorSet.error(newfd.init.getStartLoc(), 249 "A java field declaration may not be initialized in a specification file"); 250 } else if (fd.init == null) { 251 fd.init = newfd.init; 252 } else if (newfd.init != null && fd.init != newfd.init) { 253 // Note - fd is initialized by a cleancopy() of the java file, if 254 // it exists; then the files of the RS are added in. One of those 255 // might be the java file, back to put in its annotations. So 256 // we can't complain if the java file has it's initializer. 257 ErrorSet.error(newfd.locAssignOp, 258 "A field may be initialized only once in a refinement sequence", 259 fd.locAssignOp); 260 } 261 if (!equalTypes(fd.type,newfd.type)) { 262 ErrorSet.error(newfd.type.getStartLoc(), 263 "The field has been redeclared with a new type (see " + 264 Location.toString(fd.type.getStartLoc()) + ")"); 265 } 266 } 267 268 boolean match(RoutineDecl newrd, RoutineDecl rd) { 269 if ((newrd instanceof MethodDecl) != 270 (rd instanceof MethodDecl)) return false; 271 if ((newrd instanceof ConstructorDecl) != 272 (rd instanceof ConstructorDecl)) return false; 273 if (newrd instanceof MethodDecl) { 274 MethodDecl newmd = (MethodDecl)newrd; 275 MethodDecl md = (MethodDecl)rd; 276 if ( !newmd.id.equals( md.id ) ) return false; 277 // FIXME - check reutrn type 278 } 279 if (newrd.args.size() != rd.args.size()) return false; 280 for (int i=0; i<newrd.args.size(); ++i) { 281 FormalParaDecl newarg = newrd.args.elementAt(i); 282 FormalParaDecl arg = rd.args.elementAt(i); 283 // Mismatched id - an error or a non-match??? 284 //System.out.println("IDS " + newarg.id + " " + arg.id); 285 // This comparison does not work for binary specs 286 //if (!(newarg.id.equals(arg.id))) return false; 287 // FIXME - check id 288 // FIXME - chech type 289 Type newtype = newarg.type; 290 Type type = arg.type; 291 if (!equalTypes(type,newtype)) return false; 292 293 } 294 return true; 295 } 296 297 public boolean equalTypes(Type t, Type tt) { 298 if (t instanceof PrimitiveType) { 299 if (!(tt instanceof PrimitiveType)) return false; 300 return ((PrimitiveType)t).tag == ((PrimitiveType)tt).tag; 301 } else if (t instanceof ArrayType) { 302 if (!(tt instanceof ArrayType)) return false; 303 return equalTypes( ((ArrayType)t).elemType, ((ArrayType)tt).elemType ); 304 } else if (t instanceof TypeName) { 305 if (!(tt instanceof TypeName)) return false; 306 // This is not a robust way to check for equality of types 307 // An unqualified name may be resolved differently depending 308 // on the imports present; also thsi may not work for 309 // nested types. But this is the best we can do if we are 310 // testing equality before type resolution. 311 String s = ((TypeName)t).name.printName(); 312 String ss = ((TypeName)tt).name.printName(); 313 boolean b = s.equals(ss) || s.endsWith("." + ss) || ss.endsWith("." + s); 314 //System.out.println("COMP NAMES " + s + " " + ss + " " + b); 315 return b; 316 } else { 317 ErrorSet.error("Implementation error: Unknown type in RefinementSequence.equalType " + t.getClass()); 318 return t.getClass() == tt.getClass(); 319 } 320 } 321 322 /* This presumes that newrd.pmodifiers has already been parsed, 323 and hence consists of just a sequence of simple routine modifiers 324 and a single ParsedSpecs containing all the clauses. 325 The output rd.pmodifiers will consist of a sequence of ParsedSpecs, 326 one (or zero) for each of the CUs in the Refinement Sequence, along 327 with any simple routine modifiers. 328 This difference is why all routines need to go through this method, 329 even if there is only one item in the refinement sequence. 330 */ 331 void combineRoutine(RoutineDecl newrd, RoutineDecl rd) { 332 //System.out.println("Combining routine "+Location.toString(newrd.getStartLoc()) + " " +Location.toString(rd.getStartLoc()) + " " + rd.binaryArgNames + " " + Modifiers.toString(rd.modifiers) ); 333 //System.out.println(newrd.id() + " " + (newrd.body!= null) + (rd.body != null)); 334 rd.loc = newrd.loc; 335 { 336 int nn = newrd.raises.size(); 337 for (int i=0; i<nn; ++i) { 338 TypeName t = newrd.raises.elementAt(i); 339 boolean found = false; 340 for (int j=0; j<rd.raises.size(); ++j) { 341 TypeName tt = rd.raises.elementAt(j); 342 if (equalTypes(t,tt)) { found = true; break; } 343 } 344 if (found) continue; 345 // The following line is necessary because the parser (at least the 346 // class file parser) uses a dedicated singleton object for all 347 // empty lists 348 if (rd.raises.size() == 0) { 349 rd.raises = TypeNameVec.make(); 350 rd.locThrowsKeyword = newrd.locThrowsKeyword; 351 } 352 rd.raises.addElement(t); 353 //System.out.println("ADDING EXCEPTION " + t + " TO SIGNATURE FOR " 354 // + rd.parent.id + "#" + rd.id()); 355 } 356 } 357 // FIXME - check exceptions 358 for (int i=0; i<newrd.args.size(); ++i) { 359 FormalParaDecl newarg = newrd.args.elementAt(i); 360 FormalParaDecl arg = rd.args.elementAt(i); 361 // FIXME - check modifiers 362 // FIXME - check pragmas; does it matter if we duplicate pragmas? 363 arg.modifiers |= newarg.modifiers; 364 if (newarg.pmodifiers != null) { 365 if (arg.pmodifiers == null) 366 arg.pmodifiers = ModifierPragmaVec.make(); 367 arg.pmodifiers.append(newarg.pmodifiers); 368 } 369 // If rd is from a binary file, the argument names will 370 // be non-existent, so we need to fix them. 371 if (rd.binaryArgNames) { 372 arg.id = newarg.id; 373 arg.locId = newarg.locId; 374 } else if (!arg.id.toString().equals(newarg.id.toString())) { 375 ErrorSet.error(newarg.locId, 376 "Refinements may not change the names of formal parameters (" + 377 newarg.id + " vs. " + arg.id + ")", arg.locId); 378 } 379 } 380 rd.binaryArgNames = false; 381 if (false && rd.modifiers != newrd.modifiers) { 382 // FIXME - careful - some default modifiers get added in to a binary file 383 // that may not yet be present in source files. 384 ErrorSet.caution(newrd.getStartLoc(), 385 "The routine must have the same set of Java modifiers in each specification file: " + 386 Modifiers.toString(newrd.modifiers) + " vs. " + Modifiers.toString(rd.modifiers), 387 rd.getStartLoc()); 388 } 389 390 // Body: 391 // Java routines: 392 // if we have a java/class file, the body will already 393 // be present. The specs should not have a body, and we 394 // don't add it if they do, even if it is not present in 395 // the Java file. 396 // JML routines: Add the body if we do not have one already. 397 // (We don't check the case of no Java body but a spec body 398 // for a Java routine.) 399 if (newrd.body != null) { 400 boolean isModel = 401 Utils.findModifierPragma(newrd.parent.pmodifiers, 402 TagConstants.MODEL) != null || 403 Utils.findModifierPragma(newrd.pmodifiers, 404 TagConstants.MODEL) != null; 405 // If the bodies are the same object then we are just adding 406 // back the java method that was part of the starting CU. 407 // If 'implicit' is true, then the method is added by the 408 // compiler, and is the same method (e.g. default constructor). 409 if (!isModel && newrd.body != rd.body && !newrd.implicit && !rd.implicit) { 410 ErrorSet.error(newrd.body.locOpenBrace, 411 "Routine body may not be specified in a specification file"); 412 } 413 if (isModel && newrd.body != rd.body && rd.body != null && 414 !newrd.implicit && !rd.implicit) 415 ErrorSet.error(newrd.body.locOpenBrace, 416 "Model routine body is specified more than once", rd.body.locOpenBrace); 417 } 418 419 // combine pragmas 420 if (newrd.pmodifiers != null) { 421 if (rd.pmodifiers == null) { 422 rd.pmodifiers = ModifierPragmaVec.make(); 423 } 424 // FIXME - check the pmodifiers - don't drop any 425 // FIXME - should not need this check anymore 426 if (rd.pmodifiers != newrd.pmodifiers) 427 rd.pmodifiers.append(newrd.pmodifiers); 428 } 429 if (newrd.tmodifiers != null) { 430 if (rd.tmodifiers == null) { 431 rd.tmodifiers = TypeModifierPragmaVec.make(); 432 } 433 // FIXME - should not need this check anymore 434 if (rd.tmodifiers != newrd.tmodifiers) 435 rd.tmodifiers.append(newrd.tmodifiers); 436 } 437 438 } 439 440 void combineType(TypeDecl newtd, TypeDecl td, boolean addNewItems) { 441 // Compare modifiers -- FIXME 442 td.modifiers |= newtd.modifiers; 443 td.specOnly = td.specOnly && newtd.specOnly; 444 td.loc = newtd.loc; // Just to avoid having loc in a class file 445 // Need to understand and make more robust - FIXME 446 447 // Add to the type's annotations 448 if (newtd.pmodifiers != null) { 449 if (td.pmodifiers == null) { 450 td.pmodifiers = ModifierPragmaVec.make(); 451 } 452 td.pmodifiers.append(newtd.pmodifiers); 453 } 454 if (newtd.tmodifiers != null) { 455 if (td.tmodifiers == null) { 456 td.tmodifiers = TypeModifierPragmaVec.make(); 457 } 458 td.tmodifiers.append(newtd.tmodifiers); 459 } 460 461 // Verify that both are classes or both are interfaces --- FIXME 462 // Verify that superInterfaces are identical -- FIXME 463 // Verify that superclass is identical -- FIXME 464 465 // Check and combine the fields etc. of the type declarations 466 for (int i=0; i<newtd.elems.size(); ++i) { 467 TypeDeclElem tde = newtd.elems.elementAt(i); 468 boolean found = false; 469 if (tde instanceof FieldDecl) { 470 for (int k=0; !found && k<td.elems.size(); ++k) { 471 TypeDeclElem tdee = td.elems.elementAt(k); 472 if (!(tdee instanceof FieldDecl)) continue; 473 if (!( ((FieldDecl)tde).id.equals( ((FieldDecl)tdee).id ))) continue; 474 combineFields( (FieldDecl)tde, (FieldDecl)tdee ); 475 found = true; 476 } 477 if (!found) { 478 if (addNewItems) { 479 td.elems.addElement(tde); 480 tde.setParent(td); 481 } else { 482 ErrorSet.error(tde.getStartLoc(), 483 "Field is not declared in the java/class file"); 484 } 485 } 486 } else if (tde instanceof RoutineDecl) { 487 for (int k=0; !found && k<td.elems.size(); ++k) { 488 TypeDeclElem tdee = td.elems.elementAt(k); 489 if (!(tdee instanceof RoutineDecl)) continue; 490 if (!match( (RoutineDecl)tde, (RoutineDecl)tdee )) continue; 491 combineRoutine( (RoutineDecl)tde, (RoutineDecl)tdee ); 492 found = true; 493 } 494 if (!found) { 495 if (tde instanceof ConstructorDecl && ((ConstructorDecl)tde).implicit){ 496 // skip - don't add in implicit constructors 497 } else if (true || addNewItems) { 498 td.elems.addElement(tde); 499 tde.setParent(td); 500 } else { 501 // This is obsolete - FIXME - once addNewItems is always true 502 if (((RoutineDecl)tde).parent instanceof InterfaceDecl && 503 (tde instanceof MethodDecl) ) { 504 // An interface may specify some methods that 505 // it does not declare, but 'knows' that its 506 // classes implement. For example CharSequence 507 // specifies some methods that are in Object 508 // even though Object is not a superinterface 509 // of CharSequence. Perhaps this is only 510 // relevant to methods of Object, but for the 511 // moment we will make this a caution, though 512 // eventually we should detect that the method 513 // is a method of Object and either say nothing 514 // or give an error. FIXME 515 TypeDecl otd = getObjectDecl(); 516 MethodDecl md = (MethodDecl)tde; 517 md = findMatchingMethod(md,otd); 518 if (md == null) { 519 ErrorSet.caution(((RoutineDecl)tde).locId, 520 "Method is not declared in the java/class file"); 521 } 522 523 } else if (!((RoutineDecl)tde).implicit) { 524 // FIXME - the use of implicit prevents some spurious 525 // error messages, but should the default constructor 526 // be created at all ? 527 ErrorSet.error(((RoutineDecl)tde).locId, 528 "Method is not declared in the java/class file"); 529 } 530 } 531 } 532 } else if (tde instanceof TypeDecl) { 533 for (int k=0; k<td.elems.size(); ++k) { 534 TypeDeclElem tdee = td.elems.elementAt(k); 535 if (!(tdee instanceof TypeDecl)) continue; 536 if ( ((TypeDecl)tde).id.equals( ((TypeDecl)tdee).id)) { 537 combineType( (TypeDecl)tde, (TypeDecl)tdee, addNewItems ); 538 found = true; 539 } 540 } 541 if (!found) { 542 if (addNewItems) { 543 td.elems.addElement(tde); 544 tde.setParent(td); 545 } else if (!javaIsBinary) { 546 // Can't do this error for binary files - additional types in a file are put in their own class file, including nested classes 547 // Do need to check these against the real class file. FIXME 548 ErrorSet.error(tde.getStartLoc(), 549 "Type is not declared in the java file"); 550 } 551 } 552 } else if (tde instanceof InitBlock) { 553 // FIXME - combine modifiers ??? 554 // FIXME - combine pmodifiers ??? 555 InitBlock newtde = (InitBlock)initblockmap.get(tde); 556 if (newtde != null) { 557 newtde.pmodifiers = ((InitBlock)tde).pmodifiers; // combine ???? FIXME 558 } else if (addNewItems) { 559 td.elems.addElement(tde); 560 tde.setParent(td); 561 } else { 562 ErrorSet.error(tde.getStartLoc(), 563 "InitBlock should not be present in a spec file"); 564 } 565 } else if (tde instanceof GhostDeclPragma) { 566 GhostDeclPragma g = (GhostDeclPragma)tde; 567 for (int k=0; !found && k<td.elems.size(); ++k) { 568 TypeDeclElem tdee = td.elems.elementAt(k); 569 if (!(tdee instanceof GhostDeclPragma)) continue; 570 GhostDeclPragma gg = (GhostDeclPragma)tdee; 571 if ( g.decl.id.equals(gg.decl.id) 572 && g.decl.modifiers == gg.decl.modifiers) { 573 combineFields( ((GhostDeclPragma)tde).decl, 574 ((GhostDeclPragma)tdee).decl); 575 found = true; 576 } 577 } 578 if (!found) { 579 // Can always add specification stuff 580 // Could really just at it at the end, but then a bunch 581 // of tests fail because things get out of order. 582 int line = Location.toLineNumber(tde.getStartLoc()); 583 int z; 584 for (z=0; z<td.elems.size(); ++z) { 585 int ln = Location.toLineNumber( td.elems.elementAt(z).getStartLoc() ); 586 if (line < ln) break; 587 } 588 td.elems.insertElementAt(tde,z); 589 tde.setParent(td); 590 } 591 } else if (tde instanceof ModelDeclPragma) { 592 ModelDeclPragma g = (ModelDeclPragma)tde; 593 for (int k=0; !found && k<td.elems.size(); ++k) { 594 TypeDeclElem tdee = td.elems.elementAt(k); 595 if (!(tdee instanceof ModelDeclPragma)) continue; 596 if ( ((ModelDeclPragma)tde).decl.id.equals( ((ModelDeclPragma)tdee).decl.id)) { 597 combineFields( ((ModelDeclPragma)tde).decl, 598 ((ModelDeclPragma)tdee).decl); 599 found = true; 600 } 601 } 602 if (!found) { 603 // Can always add specification stuff 604 // Could really just at it at the end, but then a bunch 605 // of tests fail because things get out of order. 606 int line = Location.toLineNumber(tde.getStartLoc()); 607 int z; 608 for (z=0; z<td.elems.size(); ++z) { 609 int ln = Location.toLineNumber( td.elems.elementAt(z).getStartLoc() ); 610 if (line < ln) break; 611 } 612 td.elems.insertElementAt(tde,z); 613 tde.setParent(td); 614 } 615 } else if (tde instanceof ModelMethodDeclPragma) { 616 for (int k=0; !found && k<td.elems.size(); ++k) { 617 TypeDeclElem tdee = td.elems.elementAt(k); 618 if (!(tdee instanceof ModelMethodDeclPragma)) continue; 619 if (match( ((ModelMethodDeclPragma)tde).decl, 620 ((ModelMethodDeclPragma)tdee).decl)) { 621 tdee.setModifiers(tdee.getModifiers() | tde.getModifiers()); // trim & check 622 // FIXME - check types and modifiers 623 // FIXME - what combining to do??? 624 RoutineDecl rd = ((ModelMethodDeclPragma)tde).decl; 625 RoutineDecl rde = ((ModelMethodDeclPragma)tdee).decl; 626 if (rd.body != null && rde.body != null && rd.body != rde.body) { 627 ErrorSet.error(rd.body.getStartLoc(), 628 "Model method has more than one implementation", 629 rde.body.getStartLoc()); 630 } 631 found = true; 632 } 633 } 634 if (!found) { 635 // Can always add specification stuff 636 // Could really just at it at the end, but then a bunch 637 // of tests fail because things get out of order. 638 int line = Location.toLineNumber(tde.getStartLoc()); 639 int z; 640 for (z=0; z<td.elems.size(); ++z) { 641 int ln = Location.toLineNumber( td.elems.elementAt(z).getStartLoc() ); 642 if (line < ln) break; 643 } 644 td.elems.insertElementAt(tde,z); 645 tde.setParent(td); 646 } 647 648 } else if (tde instanceof ModelConstructorDeclPragma) { 649 ModelConstructorDeclPragma g = (ModelConstructorDeclPragma)tde; 650 for (int k=0; !found && k<td.elems.size(); ++k) { 651 TypeDeclElem tdee = td.elems.elementAt(k); 652 if (!(tdee instanceof ModelConstructorDeclPragma)) continue; 653 if (match( ((ModelConstructorDeclPragma)tde).decl, 654 ((ModelConstructorDeclPragma)tdee).decl)) { 655 tdee.setModifiers(tdee.getModifiers() | tde.getModifiers()); // trim & check 656 // FIXME - check types and modifiers 657 // FIXME - what combining to do??? 658 RoutineDecl rd = ((ModelConstructorDeclPragma)tde).decl; 659 RoutineDecl rde = ((ModelConstructorDeclPragma)tdee).decl; 660 if (rd.body != null && rde.body != null && rd.body != rde.body) { 661 ErrorSet.error(rd.body.getStartLoc(), 662 "Model constructor has more than one implementation", 663 rde.body.getStartLoc()); 664 } 665 found = true; 666 } 667 } 668 if (!found) { 669 // Can always add specification stuff 670 // Could really just at it at the end, but then a bunch 671 // of tests fail because things get out of order. 672 int line = Location.toLineNumber(tde.getStartLoc()); 673 int z; 674 for (z=0; z<td.elems.size(); ++z) { 675 int ln = Location.toLineNumber( td.elems.elementAt(z).getStartLoc() ); 676 if (line < ln) break; 677 } 678 td.elems.insertElementAt(tde,z); 679 tde.setParent(td); 680 } 681 682 } else if (tde instanceof TypeDeclElemPragma) { 683 // This include model types 684 // FIXME - should we allow merging ??? 685 // Can always add specification stuff 686 // Could really just at it at the end, but then a bunch 687 // of tests fail because things get out of order. 688 // FIXME - on a debug run it appeared that ln was always 1 689 int line = Location.toLineNumber(tde.getStartLoc()); 690 int z; 691 for (z=0; z<td.elems.size(); ++z) { 692 int ln = Location.toLineNumber( td.elems.elementAt(z).getStartLoc() ); 693 if (line < ln) break; 694 } 695 /* 696 if (tde instanceof ModelTypePragma) { 697 System.out.println("MODEL TYPE " + ((ModelTypePragma)tde).decl.id); 698 TypeDecl tdd = ((ModelTypePragma)tde).decl; 699 for (int ik=0; ik<tdd.elems.size(); ++ik) { 700 TypeDeclElem tdee = tdd.elems.elementAt(ik); 701 System.out.println(" " + tdee); 702 } 703 } 704 */ 705 706 707 td.elems.insertElementAt(tde,z); 708 tde.setParent(td); 709 } else { 710 ErrorSet.error(tde.getStartLoc(),"This type of type declaration element is not implemented - please report the problem: " + tde.getClass()); 711 } 712 } 713 } 714 715 MethodDecl findMatchingMethod(MethodDecl md, TypeDecl td) { 716 for (int k=0; k<td.elems.size(); ++k) { 717 TypeDeclElem tdee = td.elems.elementAt(k); 718 if (!(tdee instanceof MethodDecl)) continue; 719 if (match( md, (RoutineDecl)tdee )) return (MethodDecl)tdee; 720 } 721 return null; 722 } 723 724 private TypeDecl objectDecl = null; 725 TypeDecl getObjectDecl() { 726 if (objectDecl != null) return objectDecl; 727 String[] pack = { "java", "lang"}; 728 CompilationUnit ocu = javafe.tc.OutsideEnv.lookup(pack,"Object").getCompilationUnit(); 729 objectDecl = ocu.elems.elementAt(0); 730 return objectDecl; 731 } 732 733 /* These cleancopy routines produce a fresh, somewhat deep copy of a set 734 of TypeDecl objects. The purpose is to provide a copy that can be 735 modified by adding in the refinements, without modifying the original 736 compilation unit obtained from java or class files. Any part that 737 needs to be changed via refinement is cloned. In addition all 738 pragma stuff is removed (to be added in via the refinement sequence). 739 Even pragma stuff in the java file is removed, so that it is added in 740 in the correct sequence and is not added in twice. In the case of 741 binary files, we record in the binaryArgNames the fact that the binary 742 file has arbitrary formal argument names, so that we don't complain 743 about mismatches on formal names. 744 */ 745 TypeDeclVec cleancopy(TypeDeclVec types) { 746 TypeDeclVec v = TypeDeclVec.make(); 747 for (int i = 0; i<types.size(); ++i) { 748 v.addElement(cleancopy(types.elementAt(i))); 749 } 750 return v; 751 } 752 753 TypeDecl cleancopy(TypeDecl td) { 754 TypeDeclElemVec newelems = TypeDeclElemVec.make(td.elems.size()); 755 for (int i=0; i<td.elems.size(); ++i) { 756 TypeDeclElem tde = cleancopy(td.elems.elementAt(i)); 757 if (tde != null) newelems.addElement(tde); 758 } 759 TypeDecl newtd = null; 760 if (td instanceof ClassDecl) { 761 ClassDecl cd = (ClassDecl)td; 762 newtd = ClassDecl.make( 763 cd.modifiers, // shrink to Java only 764 null, 765 cd.id, 766 cd.superInterfaces, 767 null, 768 newelems, 769 cd.loc, 770 cd.locId, 771 cd.locOpenBrace, 772 cd.locCloseBrace, 773 cd.superClass); 774 } else if (td instanceof InterfaceDecl) { 775 InterfaceDecl cd = (InterfaceDecl)td; 776 newtd = InterfaceDecl.make( 777 cd.modifiers, 778 null, 779 cd.id, 780 cd.superInterfaces, 781 null, 782 newelems, 783 cd.loc, 784 cd.locId, 785 cd.locOpenBrace, 786 cd.locCloseBrace); 787 } else { 788 ErrorSet.fatal(td.getStartLoc(), 789 "Not implemented: Unable to process this type in Refinement.cleancopy: " + td.getClass()); 790 return null; 791 } 792 newtd.specOnly = td.specOnly; 793 return newtd; 794 } 795 796 TypeDeclElem cleancopy(TypeDeclElem tde) { 797 TypeDeclElem newtde = null; 798 if (tde instanceof FieldDecl) { 799 FieldDecl d = (FieldDecl)tde; 800 newtde = FieldDecl.make( 801 d.modifiers, // FIXME trim 802 null, 803 d.id, 804 d.type, 805 d.locId, 806 d.init, 807 d.locAssignOp); 808 } else if (tde instanceof MethodDecl) { 809 MethodDecl d = (MethodDecl)tde; 810 newtde = MethodDecl.make( 811 d.modifiers, 812 null, 813 null, 814 cleancopy(d.args,false), 815 d.raises, 816 javaIsBinary? null: d.body, 817 d.locOpenBrace, 818 d.loc, 819 d.locId, 820 d.locThrowsKeyword, 821 d.id, 822 d.returnType, 823 d.locType); 824 ((RoutineDecl)newtde).implicit = d.implicit; 825 } else if (tde instanceof ConstructorDecl) { 826 ConstructorDecl d = (ConstructorDecl)tde; 827 boolean enclosed = d.parent.parent != null && !Modifiers.isStatic(d.parent.modifiers) && javaIsBinary; 828 newtde = ConstructorDecl.make( 829 d.modifiers, 830 null, 831 null, 832 cleancopy(d.args,false && enclosed), // FIXME - fixed in the binary reader 833 d.raises, 834 javaIsBinary? null: d.body, 835 d.locOpenBrace, 836 d.loc, 837 d.locId, 838 d.locThrowsKeyword); 839 ((RoutineDecl)newtde).implicit = d.implicit; 840 } else if (tde instanceof TypeDecl) { 841 newtde = cleancopy((TypeDecl)tde); 842 } else if (tde instanceof InitBlock) { 843 InitBlock d = (InitBlock)tde; 844 newtde = InitBlock.make( 845 d.modifiers, // FIXME trim 846 null, 847 javaIsBinary? null: d.block); 848 initblockmap.put(d,newtde); 849 } else if (tde instanceof TypeDeclElemPragma) { 850 newtde = null; 851 } else { 852 ErrorSet.fatal(tde.getStartLoc(), 853 "Not implemented: Unable to process this type in Refinement.cleancopy: " + tde.getClass()); 854 } 855 if (javaIsBinary && newtde instanceof RoutineDecl) { 856 ((RoutineDecl)newtde).binaryArgNames = true; 857 } 858 return newtde; 859 } 860 861 private Map initblockmap = new HashMap(); 862 public FormalParaDeclVec cleancopy(FormalParaDeclVec args,boolean omitFirst) { 863 int offset = omitFirst ? 1 : 0; 864 FormalParaDeclVec result = FormalParaDeclVec.make(args.size() - offset ); 865 for (int i=offset; i<args.size(); ++i) { 866 FormalParaDecl a = args.elementAt(i); 867 a = FormalParaDecl.make(a.modifiers, 868 null, // clean out the pragmas 869 a.id, 870 a.type, 871 a.locId); 872 result.addElement(a); 873 } 874 return result; 875 } 876 }