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    }