    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.backpred;
    004
    005    import java.util.Enumeration;
    006    import java.util.Hashtable;
    007    import java.util.Vector;
    008    import java.util.LinkedList;
    009
    010    import javafe.ast.*;
    011    import escjava.ast.*;
    012    import escjava.ast.TagConstants;
    013    import escjava.ast.Modifiers;
    014    import escjava.ast.ExprDeclPragmaVec;           // compiler bug workaround
    015
    016    import javafe.tc.*;
    017    import javafe.util.*;
    018
    019    import escjava.translate.GC;
    020    import escjava.translate.GetSpec;
    021    import escjava.translate.Inner;
    022    import escjava.translate.Translate;
    023    import escjava.translate.Helper;
    024
    025    /**
    026     * This class is responsible for determining the contributors to a
    027     * given TypeSig or RoutineDecl.
    028     *
    029     * <p> The contributors are divided into a set of TypeSigs, a set of
    030     * Invariants, and a set of Fields.
    031     */
    032
    033    public class FindContributors
    034    {
    035        // Public interface
    036
    037        /**
    038         * Generate the contributors for a given TypeSig.  This may result
    039         * in errors being reported and TypeSigs being type checked. <p>
    040         *
    041         * The originType is taken to be that Typesig.<p>
    042         *
    043         * Precondition: T must have been typechecked.<p>
    044         *
    045         * Note: in the process of locating contributors,
    046         * FindContributors may type check additional types leading
    047         * possibly to type errors.  If such error(s) occur, a fatal
    048         * error is reproted.
    049         */
    050        public FindContributors(/*@ non_null @*/ TypeSig T) {
    051            originType = T;
    052            addType(T);
    053
    054            walk(T.getTypeDecl());
    055            fieldToPossible = null;         // conserve space
    056
    057            if (Info.on) {
    058                Info.out("[[contributors: "
    059                    + contributorTypes.size() + " types "
    060                    + contributorInvariants.size() + " invariants "
    061                    + contributorFields.size() + " fields ]]");
    062            }
    063        }
    064
    065        /**
    066         * Generate the contributors for a given RoutineDecl.  This may
    067         * result in errors being reported and TypeSigs being type checked.<p>
    068         *
    069         * The originType is taken to be the type declaring that RoutineDecl.<p>
    070         *
    071         * Precondition: the type declaring rd must have been typechecked.<p>
    072         *
    073         * Note: in the process of locating contributors,
    074         * FindContributors may type check additional types leading
    075         * possibly to type errors.  If such error(s) occur, a fatal
    076         * error is reproted.
    077         */
    078        public FindContributors(/*@ non_null @*/ RoutineDecl rd) {
    079            originType = TypeSig.getSig(rd.parent);
    080            addType(originType);
    081
    082            walk(rd);
    083            fieldToPossible = null;         // conserve space
    084
    085            if (Info.on) {
    086                Info.out("[[local contributors: "
    087                    + contributorTypes.size() + " types "
    088                    + contributorInvariants.size() + " invariants "
    089                    + contributorFields.size() + " fields ]]");
    090            }
    091        }
    092
    093
    094        /**
    095         * Our origin type; used to determine visibility and accessibility
    096         * when needed.
    097         */
    098        public TypeSig originType;
    099
    100
    101        /**
    102         * Enumerate the TypeSig contributors
    103         */
    104        public Enumeration typeSigs() {
    105            return contributorTypes.elements();
    106        }
    107
    108        /**
    109         * Enumerate the invariant contributors
    110         */
    111        public Enumeration invariants() {
    112            return contributorInvariants.elements();
    113        }
    114
    115        /**
    116         * Enumerate the field contributors
    117         */
    118        public Enumeration fields() {
    119            return contributorFields.elements();
    120        }
    121
    122
    123        // Closure code
    124
    125        /** The set of routines visited so far.
    126         */
    127
    128        private /*@ non_null @*/ Set visitedRoutines = new Set();
    129
    130        /**
    131         * The set of TypeSigs we've determined to be contributors so far. <p>
    132         *
    133         * Invariant: This set is closed under taking supertypes
    134         */
    135        private /*@ non_null @*/ Set contributorTypes = new Set();
    136
    137        /**
    138         * The set of invariants (elementType ExprDeclPragmas) we've
    139         * determined to be contributors so far. <p>
    140         *
    141         * Closure Property: walk(-) has been called on each of
    142         * these invariants.
    143         */
    144        private /*@ non_null @*/ Set contributorInvariants = new Set();
    145
    146        /**
    147         * The set of fields (elementType FieldDecl) we've determined to be
    148         * contributors so far. <p>
    149         *
    150         * Closure Property:
    151         *
    152         *    all invariants J that are declared in types in
    153         *    contributorTypes and "mention the field" f for f a field in
    154         *    contributorFields are members of contributorInvariants
    155         */
    156        private /*@ non_null @*/ Set contributorFields = new Set();
    157
    158        public int preFieldMode = 0;
    159        public /*@ non_null @*/ Set preFields = new Set();
    160
    161        /**
    162         * A mapping from fields (FieldDecls) to possible invariant
    163         * contributors (ExprDeclPragmaVec). <p>
    164         *
    165         * (An invariant is a possible contributor if it is declared in a
    166         * type of contributorTypes.)
    167         *
    168         * Invariant:
    169         *
    170         *     if (f,J) in fieldToPossible then the invariant J "mentions
    171         *    the field" f and J is a possible invariant contributor
    172         *
    173         * Closure property:
    174         *
    175         *    if J is possible invariant contributor,
    176         *    J not in contributorInvariants, and J "mentions the field" f,
    177         *    then (f,J) is in fieldToPossible.
    178         *
    179         */
    180        // can be null
    181        Hashtable fieldToPossible = new Hashtable();
    182
    183
    184
    185        /**
    186         * Add the TypeSigs mentioned explicitly in a given Type to
    187         * contributorTypes, maintaining all the closure properties. <p>
    188         *
    189         * Precondition: T has been resolved.<p>
    190         */
    191        //@ requires T != null;
    192        private void addType(Type T) {
    193            // TypeName case:
    194            if (T instanceof TypeName) {
    195                T = TypeSig.getSig((TypeName)T);
    196                Assert.precondition(T != null);
    197            }
    198
    199            // ArrayType case:
    200            if (T instanceof ArrayType) {
    201                addType(((ArrayType)T).elemType);
    202                return;
    203            }
    204
    205            // PrimitiveType case:
    206            if (T instanceof PrimitiveType)
    207                return;
    208
    209            /*
    210             * Remaining case is TypeSig:
    211             */
    212            TypeSig sig = (TypeSig)T;
    213            if (contributorTypes.contains(sig))
    214                return;
    215
    216            // make sure sig is typechecked:
    217            typecheck(sig);
    218
    219            // Close over taking supertypes:
    220            TypeDecl td = sig.getTypeDecl();
    221            if (td instanceof ClassDecl) {
    222                ClassDecl cd = (ClassDecl)td;
    223                if (cd.superClass != null)
    224                    addType(cd.superClass);
    225            }
    226            for (int i=0; i<td.superInterfaces.size(); i++)
    227                addType(td.superInterfaces.elementAt(i));
    228
    229            contributorTypes.add(sig);
    230
    231            // Add sig's invariants as possible contributor invariants:
    232            for (int i = 0; i<td.elems.size(); i++) {
    233                TypeDeclElem tde = td.elems.elementAt(i);
    234
    235                if (tde.getTag() == TagConstants.INVARIANT)
    236                    addPossibleInvariant((ExprDeclPragma)tde);
    237            }
    238
    239
    240            /*
    241             * Hack: for 1.1, add an inner classes' this$0 pointer when
    242             * that class is added as a type, rather than trying to keep
    243             * track of everywhere it might be introduced.
    244             */
    245            if (!sig.isTopLevelType()) {
    246                FieldDecl thisptr = Inner.getEnclosingInstanceField(sig);
    247
    248                backedgeToGenericVarDecl(thisptr, null, true, new LinkedList());
    249            }
    250        }
    251
    252
    253        /**
    254         * Add a given field to contributorFields, maintaining all the
    255         * closure properties. <p>
    256         */
    257        //@ requires fd != null;
    258        private void addField(FieldDecl fd) {
    259            if (contributorFields.contains(fd))
    260                return;
    261
    262            contributorFields.add(fd);
    263
    264            /*
    265             * Turn possible invariant contributors that mention fd into
    266             * real ones.  We use fieldToPossible to do this quickly.
    267             */
    268            ExprDeclPragmaVec newInvariants =
    269                (ExprDeclPragmaVec)fieldToPossible.get(fd);
    270            if (newInvariants==null)
    271                return;
    272
    273            // Note: newInvariants is not modified here because we added fd to
    274            // contributorFields
    275            for (int i=0; i<newInvariants.size(); i++)
    276                addInvariant(newInvariants.elementAt(i));
    277        }
    278
    279        /**
    280         * Add the mapping (fd, J) to fieldToPossible.
    281         *
    282         * Precondition: J is a possible invariant contributor, J "mentions
    283         * the field" fd.
    284         */
    285        private void addPossibleMentions(FieldDecl fd, /*@ non_null @*/ ExprDeclPragma J) {
    286            ExprDeclPragmaVec range = (ExprDeclPragmaVec)fieldToPossible.get(fd);
    287            if (range==null) {
    288                range = ExprDeclPragmaVec.make();
    289                fieldToPossible.put(fd, range);
    290            }
    291
    292            range.addElement(J);
    293        }
    294
    295
    296        /**
    297         * Add a possible invariant contributor to either fieldToPossible
    298         * or contributorInvariants as approperiate, maintaining all
    299         * closure properties. <p>
    300         *
    301         * Precondition: J has been type checked.
    302         */
    303        //@ requires J != null;
    304        private void addPossibleInvariant(ExprDeclPragma J) {
    305            FieldDeclVec fieldsMentioned = fieldsInvariantMentions(J);
    306
    307            for (int i=0; i<fieldsMentioned.size(); i++) {
    308                FieldDecl fd = fieldsMentioned.elementAt(i);
    309
    310                if (contributorFields.contains(fd)) {
    311                    // Ah!  J is actually a real invariant contributor:
    312                    addInvariant(J);
    313                    return;
    314                }
    315
    316                // Add (f,J) to fieldToPossible:
    317                addPossibleMentions(fd, J);
    318            }
    319        }
    320
    321        /**
    322         * Add a given invariant to contributorInvarints, maintaining all
    323         * closure properties. <p>
    324         *
    325         * Precondition: J has been type checked.
    326         */
    327        //@ requires J != null;
    328        private void addInvariant(ExprDeclPragma J) {
    329            if (contributorInvariants.contains(J))
    330                return;
    331
    332            contributorInvariants.add(J);
    333
    334            walk(J);
    335        }
    336
    337
    338        // Walking ASTNodes
    339
    340        /**
    341         * Walks a given ASTNode, adding all the types it "mentions" via
    342         * addType and adding all the fields it "mentions" via
    343         * addField. <p>
    344         *
    345         * Precondition: N has been typechecked.
    346         *
    347         * WARNING: N is assumed to have no free local or parameter
    348         * varables.
    349         */
    350        private void walk(ASTNode N) {
    351            walk(N, null, true, new LinkedList());
    352        }
    353
    354
    355        /**
    356         * Returns the set of fields that a given invariant mentions. <p>
    357         *
    358         * Precondition: J must be an invariant, J must be typechecked.
    359         */
    360        private FieldDeclVec fieldsInvariantMentions(ExprDeclPragma J) {
    361            // We may cache this function later...
    362
    363            FieldDeclVec result = FieldDeclVec.make();
    364            walk(J, result, false, new LinkedList());
    365            return result;
    366        }
    367
    368
    369        /**
    370         * Walks a given ASTNode, finding all the types it "mentions" and
    371         * all the fields it "mentions". <p>
    372         *
    373         * If fields is null, the fields mentioned are added via addField;
    374         * otherwise, they are added to fields directly.<p>
    375         *
    376         * If addTypes is true, the types mentioned are added via addType.<p>
    377         *
    378         * Precondition: N has been typechecked.
    379         */
    380        private void walk(ASTNode N, FieldDeclVec fields, boolean addTypes,
    381                                    LinkedList visited) {
    382            /*
    383             * Leaf nodes:
    384             */
    385            if (N==null)
    386                return;
    387            if (N instanceof Type) {
    388                if (addTypes)
    389                    addType((Type)N);
    390                return;
    391            }
    392
    393            if (N instanceof LiteralExpr || N instanceof ClassLiteral) {
    394                Expr lit = (Expr)N;
    395                if (addTypes) {
    396                    addType(TypeCheck.inst.getType(lit));
    397                }
    398            }
    399
    400            /*
    401             * Handle relevant backedges:
    402             */
    403            if (N instanceof VariableAccess) {
    404                backedgeToGenericVarDecl(((VariableAccess)N).decl,
    405                                         fields, addTypes, visited);
    406            }
    407            if (N instanceof FieldAccess) {
    408                if (preFieldMode > 0) {
    409                    preFields.add(N);
    410                }
    411                backedgeToGenericVarDecl(((FieldAccess)N).decl,
    412                                         fields, addTypes, visited);
    413            }
    414
    415            if (N instanceof ConstructorInvocation) {
    416                ConstructorInvocation ci = (ConstructorInvocation) N;
    417                visited.addFirst(ci.decl);
    418                int inline = Translate.inlineDecoration.get(ci) != null ? 2 :
    419                             isNonRecursiveHelperInvocation(ci.decl) ? 1 : 0;
    420                backedgeToRoutineDecl(ci.decl, fields, addTypes, inline, visited);
    421            }
    422            if (N instanceof NewInstanceExpr) {
    423                NewInstanceExpr ni = (NewInstanceExpr) N;
    424                int inline = Translate.inlineDecoration.get(ni) != null ? 2 :
    425                             isNonRecursiveHelperInvocation(ni.decl) ? 1 : 0;
    426                backedgeToRoutineDecl(ni.decl,fields, addTypes, inline, visited);
    427            }
    428            if (N instanceof MethodInvocation) {
    429                MethodInvocation mi = (MethodInvocation) N;
    430                int inline = Translate.inlineDecoration.get(mi) != null ? 2 :
    431                             isNonRecursiveHelperInvocation(mi.decl) ? 1 : 0;
    432
    433                backedgeToRoutineDecl(mi.decl, fields, addTypes, inline, visited);
    434            }
    435    // FIXME - add the type from quantified expression? set comprehension expr? new array expr?
    436            /*
    437             * Add references not explicitly in Java code or from backedges:
    438             */
    439            if (N instanceof RoutineDecl) {
    440                // Get references in our derived spec:
    441                backedgeToRoutineDecl((RoutineDecl)N, fields, addTypes, 0, visited);
    442
    443                // Add implicit references if N is a ConstructorDecl:
    444                if (N instanceof ConstructorDecl)
    445                    addImplicitConstructorRefs((ConstructorDecl)N,
    446                                               fields, addTypes, visited);
    447            }
    448
    449            if (N.getTag() == TagConstants.PRE) {
    450                ++preFieldMode;
    451            }
    452
    453
    454
    455            /*
    456             * Recurse to subnodes (this automatically ignores backedges):
    457             *
    458             * We intentionally skip TypeDecls so that we stay in the same type.
    459             */
    460            try {
    461                int size = N.childCount();
    462                for (int i=0; i<size; i++) {
    463                    Object child = N.childAt(i);
    464                    if (child instanceof ASTNode && !(child instanceof TypeDecl))
    465                        walk((ASTNode)child, fields, addTypes, visited);
    466                }
    467            } finally {
    468                if (N.getTag() == TagConstants.PRE) {
    469                    --preFieldMode;
    470                }
    471            }
    472        }
    473
    474      /** Returns <code>true</code> if and only if <code>r</code> is a helper
    475        * routine that has not been visited by this <code>FindContributor</code>
    476        * object.
    477        */
    478
    479      private boolean isNonRecursiveHelperInvocation(/*@ non_null */ RoutineDecl r) {
    480        return Helper.isHelper(r) && !visitedRoutines.contains(r);
    481      }
    482
    483        /**
    484         * Add implicit references from a ConstructorDecl that do not
    485         * appear in Java code or via backedges as per walk(,,).
    486         *
    487         * Precondition: the type declaring cd has been typechecked.
    488         */
    489        private void addImplicitConstructorRefs(/*@ non_null @*/ ConstructorDecl cd,
    490                                                FieldDeclVec fields,
    491                                                boolean addTypes,
    492                                                LinkedList visited) {
    493            /*
    494             * Walk the initialization code derived from the same class as
    495             * the constructor:
    496             */
    497            TypeDecl td = cd.parent;
    498            walkInstanceInitialier(td, fields, addTypes, visited);
    499
    500            /*
    501             * For all superinterfaces that the constructor's type
    502             * implements that are not already implemented by its
    503             * superclass(es), walk the initialization code derived from
    504             * them:
    505             */
    506            Enumeration FII = GetSpec.getFirstInheritedInterfaces((ClassDecl)td);
    507            while (FII.hasMoreElements()) {
    508                walkInstanceInitialier((TypeDecl)FII.nextElement(), fields,
    509                                       addTypes, visited);
    510            }
    511        }
    512
    513
    514        /**
    515         * Walk the implicit instance initializer code for a given
    516         * TypeDecl, excluding any field initializations of
    517         * superinterface fields. <p>
    518         *
    519         * E.g., f_1 = 0; ...; f_3 = <initializer exp>; ... ; <instance
    520         * initializer block>...
    521         *
    522         * This is the code that constructors of that type implicitly
    523         * start with after their super/sibling call modulo the
    524         * initialization of superinterface fields.
    525         *
    526         * See addImplicitConstructorRefs for the full version w/o the
    527         * exclusion.
    528         *
    529         *
    530         * Addition: This now also pulls in all invariants in the given
    531         *           TypeDecl, regardless of what they mention.  This is
    532         *           to avoid user surprise; see also Vanilla.java in
    533         *           test58.
    534         *
    535         *
    536         * Precondition: the TypeDecl has been typechecked.
    537         */
    538        private void walkInstanceInitialier(/*@ non_null @*/ TypeDecl td,
    539                                            FieldDeclVec fields,
    540                                            boolean addTypes,
    541                                            LinkedList visited) {
    542            for (int i = 0; i < td.elems.size(); i++) {
    543                TypeDeclElem tde = td.elems.elementAt(i);
    544
    545                if (tde.getTag() == TagConstants.INVARIANT)
    546                    addInvariant((ExprDeclPragma)tde);
    547
    548                if (tde instanceof ModelDeclPragma)
    549                    tde = ((ModelDeclPragma)tde).decl;
    550                if (tde instanceof GhostDeclPragma)
    551                    tde = ((GhostDeclPragma)tde).decl;
    552                if (tde.getTag() == TagConstants.FIELDDECL
    553                      && !Modifiers.isStatic(((FieldDecl)tde).modifiers)) {
    554                    FieldDecl fd = (FieldDecl)tde;
    555
    556                    // walk "fd := (fd.init==null ? <zero-equivalent> : fd.init)":
    557                    backedgeToGenericVarDecl(fd, fields, addTypes, visited);
    558                    walk(fd.init, fields, addTypes, visited);
    559
    560                } else if (tde.getTag() == TagConstants.INITBLOCK
    561                      && !Modifiers.isStatic(((InitBlock)tde).modifiers)) {
    562                    // walk any instance initializer blocks found:
    563                    walk((InitBlock)tde, fields, addTypes, visited);
    564
    565                }
    566            }
    567        }
    568
    569
    570        /**
    571         * Calculate the fields and types "mentioned" by a backedge to a
    572         * GenericVarDecl and then add them as per walk(,,).
    573         */
    574        private void backedgeToGenericVarDecl(GenericVarDecl decl,
    575                                              FieldDeclVec fields,
    576                                              boolean addTypes,
    577                                              LinkedList visited) {
    578            // The length field of arraytypes is never considered "mentioned":
    579            if (decl==javafe.tc.Types.lengthFieldDecl)
    580                return;
    581
    582            if (decl instanceof FieldDecl) {
    583                FieldDecl fd = (FieldDecl)decl;
    584                typecheck(TypeSig.getSig(fd.parent));
    585
    586
    587                // The range and domain types of fd are "mentioned":
    588                addType(fd.type);
    589                if (fd.parent != null)      // "length" field has no parent...
    590                    addType(TypeSig.getSig(fd.parent));
    591
    592                /*
    593                 * Exit if have already processed this field; need to do
    594                 * this to avoid recursion in case the field's modifiers
    595                 * mention it.
    596                 */
    597                if (fields==null) {
    598                    if (contributorFields.contains(fd))
    599                        return;
    600                } else if (fields.contains(fd))
    601                    return;
    602
    603
    604                // The field fd is "mentioned":
    605                if (fields != null)
    606                    fields.addElement(fd);
    607                else
    608                    addField(fd);
    609
    610                /*
    611                 * We need to walk the "spec" part of fd as well to handle
    612                 * readable_if and the like:
    613                 */
    614                if (fd.pmodifiers != null) {
    615                    for (int i=0; i<fd.pmodifiers.size(); i++)
    616                        walk(fd.pmodifiers.elementAt(i), fields, addTypes, visited);
    617                }
    618            }
    619
    620            /*
    621             * Ignore local & parameter variable Decls here, as they
    622             * should already have been walked over.
    623             */
    624        }
    625
    626        /**
    627         * Calculate the fields and types "mentioned" by a backedge to a
    628         * RoutineDecl and then add them as per walk(,,). <p>
    629         *
    630         * <code>inlined</code> is one of: 0 (not an inlined routine),
    631         * 1 (an inlined helper routine), or 2 (a routine inlined for
    632         * a reason other than being a helper).  (Why this complication,
    633         * why not just use a boolean field "inlined"?  By distinguishing
    634         * cases 1 and 2, one can write a nice run-time assert inside the
    635         * implementation of this method.)
    636         */
    637        //@ requires inlined == 0 || inlined == 1 || inlined == 2;
    638        private void backedgeToRoutineDecl(RoutineDecl rd,
    639                                           FieldDeclVec fields,
    640                                           boolean addTypes,
    641                                           int inlined, LinkedList visited) {
    642            if (rd == null) return; // FIXME - this happens with some NewInstanceExpr
    643            // FIXME - remove references to visited
    644            //if (visited.contains(rd)) return;
    645            //visited.addFirst(rd);
    646            if (inlined==0 && visitedRoutines.contains(rd)) return;
    647            //Assert.notFalse(inlined != 1 || !visitedRoutines.contains(rd));
    648            visitedRoutines.add(rd);
    649
    650            TypeSig thisType = TypeSig.getSig(rd.parent);
    651            typecheck(thisType);
    652
    653            /*
    654             * Temporarily set GC.thisvar's type to thisType; we need to
    655             * do this because GetSpec.getCombinedMethodDecl() returns
    656             * GC.thisvar as the first argument of instance methods.
    657             *
    658             * If we don't do this, we may add the wrong type when we add
    659             * the types of the routine's arguments below.
    660             */
    661            Type savedType = GC.thisvar.decl.type;
    662            GC.thisvar.decl.type = thisType;
    663
    664            // Get the derived spec for rd:
    665            DerivedMethodDecl dmd = GetSpec.getCombinedMethodDecl(rd);
    666            dmd = GetSpec.filterMethodDecl(dmd, this);
    667
    668
    669            /*
    670             * The types in the called routine's Java signature are
    671             * "mentioned" (including the type of Constructors): */
    672            if (addTypes) {
    673                // Add args here mostly for safely reasons
    674                for (int i=0; i<dmd.args.size(); i++)
    675                    addType(dmd.args.elementAt(i).type);
    676                for (int i=0; i<dmd.throwsSet.size(); i++)
    677                    addType(dmd.throwsSet.elementAt(i));
    678                addType(dmd.returnType);
    679            }
    680
    681            // We also need to walk the routine's spec:
    682            for (int i=0; i<dmd.requires.size(); i++)
    683                walk(dmd.requires.elementAt(i), fields, addTypes, visited);
    684            if (inlined == 0) {
    685              // Add modifies here mostly for safely reasons
    686              for (int i=0; i<dmd.modifies.size(); i++)
    687                walk(dmd.modifies.elementAt(i), fields, addTypes, visited);
    688            }
    689            for (int i=0; i<dmd.ensures.size(); i++)
    690                walk(dmd.ensures.elementAt(i), fields, addTypes, visited);
    691            for (int i=0; i<dmd.exsures.size(); i++)
    692                walk(dmd.exsures.elementAt(i), fields, addTypes, visited);
    693
    694            if (inlined != 0) {
    695                walk(rd.body, fields, addTypes, visited);
    696            }
    697
    698            GC.thisvar.decl.type = savedType;
    699            //visited.removeFirst();
    700        }
    701
    702
    703        // Utility routines
    704
    705        /**
    706         * Make sure a given TypeSig has been type checked, type checking
    707         * it if necessary. <p>
    708         *
    709         * Throws a fatal error if a type error occurs while checking sig.
    710         */
    711        void typecheck(/*@ non_null @*/ TypeSig sig) {
    712            int errorCount = ErrorSet.errors;
    713
    714            sig.typecheck();
    715            if (errorCount == ErrorSet.errors)
    716                return;
    717
    718            ErrorSet.fatal("A type error has occurred at an unexpected point;"
    719                           + " unable to continue processing");
    720        }
    721    }