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