    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    }