001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package javafe.tc;
004    
005    import java.util.Hashtable;
006    
007    import javafe.ast.*;
008    import javafe.util.*;
009    
010    /**
011     * Does disambiguation and flow insensitive checks on a type
012     * declaration.
013     */
014    
015    public class FlowInsensitiveChecks
016    {
017        static public FlowInsensitiveChecks inst = new FlowInsensitiveChecks();
018        static public FlowInsensitiveChecks inst() { return inst; }
019    
020        /**
021         * Controls whether or not implicit super-calls in constructors
022         * are made explicit.  By default they are.
023         */
024        public static boolean dontAddImplicitConstructorInvocations = false;
025    
026        // Use this to get an instance in order to get proper derived behavior.
027        protected FlowInsensitiveChecks() { }
028    
029        /**
030         * Factory method so subclasses can override.
031         */
032        //@ requires s != null;
033        //@ ensures \result != null;
034        protected EnvForTypeSig makeEnvForTypeSig(TypeSig s,
035                                                  boolean staticContext) {
036            return s.getEnv(staticContext);
037        }
038    
039    
040        ///////////////////////////////////////////////////////////////////////
041        //                                                                   //
042        // Information that remains the same during processing of entire     //
043        // type decl.                                                        //
044        //                                                                   //
045        ///////////////////////////////////////////////////////////////////////
046    
047        //@ invariant sig != null ==> rootIEnv != null && rootSEnv != null;
048        /*@ spec_public */ protected TypeSig sig;
049    
050        // Inv: rootIEnv.peer == sig; !rootIEnv.staticContext
051        /*@ spec_public */ protected EnvForTypeSig rootIEnv;
052    
053        // Inv: rootIEnv.peer == sig; !rootIEnv.staticContext
054        /*@ spec_public */ protected EnvForTypeSig rootSEnv;
055      
056    
057        ///////////////////////////////////////////////////////////////////////
058        //                                                                   //
059        // Information that changes for the processing of each member of     //
060        // the decl.                                                         //
061        //                                                                   //
062        ///////////////////////////////////////////////////////////////////////
063      
064        //* Cannot access fields defined later? 
065        protected boolean leftToRight;
066    
067        //* Type for return statements. 
068        protected Type returnType;
069      
070    
071        ///////////////////////////////////////////////////////////////////////
072        // Information that changes within a member in a stack-like          //
073        // manner.                                                           //
074        ///////////////////////////////////////////////////////////////////////
075      
076        //@ invariant allowedExceptions != null;
077        protected TypeSigVec allowedExceptions = TypeSigVec.make();
078    
079        //@ invariant enclosingLabels != null;
080        protected StmtVec enclosingLabels = StmtVec.make();
081    
082        // -------------------------------------------------------------
083        /**
084         * Moves <code>s</code> into implementation checked state.
085         *
086         */
087        //@ requires (* <code>s</code> is in prepped state.*);
088        //@ requires s.state >= TypeSig.PREPPED;
089        public void checkTypeDeclaration(/*@ non_null @*/ TypeSig s) {
090            Assert.precondition(s.state >= TypeSig.PREPPED);
091    
092            // Set up variables for entire traversal:
093            rootSEnv = makeEnvForTypeSig(s, true);
094            rootIEnv = makeEnvForTypeSig(s, false);
095            sig = s;
096    
097            TypeDecl d = s.getTypeDecl();
098    
099            // Process each member declaration
100            for(int i = 0, sz = d.elems.size(); i < sz; i++) {
101                TypeDeclElem e = d.elems.elementAt(i);
102                checkTypeDeclElem(e);
103            }
104    
105            // Process ModifierPragmas
106            checkModifierPragmaVec(d.pmodifiers, d, rootSEnv);
107    
108            sig = null;
109        }
110    
111        // -------------------------------------------------------------
112    
113        /**
114         * Moves <code>fd</code> into implementation checked state.
115         *
116         */
117        //@ requires (* <code>fd</code> is in prepped state. *);
118        //@ modifies sig, rootSEnv, rootIEnv;
119        public void checkFieldDecl(/*@ non_null @*/ FieldDecl fd) {
120            /*
121             * Special case for free-floating fields like length.
122             *
123             * Such fields must not have any modifier pragmas or an initializer.
124             */
125            if (fd.parent==null) {
126                Assert.notFalse(fd.pmodifiers == null,   //@ nowarn Pre;
127                                "Free-floating FieldDecls may not have any ModifierPragmas");
128                Assert.notFalse(fd.init == null,         //@ nowarn Pre;
129                                "Free-floating FieldDecls may not have initializers");
130    
131                return;         // No other works needs to be done
132            }
133    
134    
135            TypeSig sig = TypeSig.getSig(fd.parent);
136            if (sig.state < TypeSig.CHECKED) {
137                // Type check this decl
138            
139                // Info.out("[Pre-checking "+Types.printName(sig)+"."+fd.id+"]");
140                sig.prep();
141    
142                // Set up variables for entire traversal
143                rootSEnv = makeEnvForTypeSig(sig, true);
144                rootIEnv = makeEnvForTypeSig(sig, false);
145                this.sig = sig;
146    
147                checkTypeDeclElem(fd);
148            }
149            this.sig = null;
150        }
151    
152        //------------------------------------------------------------
153    
154        // @note e must already have been prepped!
155        //@ requires e != null && sig != null;
156        //@ requires sig.state >= TypeSig.PREPPED;
157        protected void checkTypeDeclElem(TypeDeclElem e) {
158    
159            Assert.notNull(sig);
160            Assert.notFalse(sig.state>= TypeSig.PREPPED);
161            TypeDecl d = sig.getTypeDecl();
162            boolean specOnly = d.specOnly;
163    
164            switch (e.getTag()) {
165            
166                case TagConstants.FIELDDECL: {              
167                    FieldDecl fd = (FieldDecl)e;
168    
169                    // Process ModifierPragmas
170                    Env rootEnv = Modifiers.isStatic(fd.modifiers) ? rootSEnv : rootIEnv;
171                    checkModifierPragmaVec(fd.pmodifiers, fd, rootEnv);
172                    checkTypeModifiers(rootEnv, fd.type);
173    
174                    // Resolve the initializer of a field decl
175                    if (fd.init != null) {
176                        leftToRight = true;
177                        allowedExceptions.removeAllElements();
178                        Assert.notFalse(allowedExceptions.size() == 0);
179                        fd.init = checkInit(rootEnv, fd.init, fd.type);
180                    }
181                    else if (Modifiers.isFinal(fd.modifiers) && !specOnly) {
182                        // Removed for 1.1:
183                        //  ErrorSet.caution(fd.locId, 
184                        //    "Final variables must be initialized");
185                    }
186                    break;
187                }
188            
189                case TagConstants.METHODDECL:
190                case TagConstants.CONSTRUCTORDECL: {
191                    RoutineDecl rd = (RoutineDecl) e;
192                    Env rootEnv = Modifiers.isStatic(rd.modifiers)
193                        ? rootSEnv : rootIEnv;
194              
195                    // First do method/constructor specific stuff
196                    if(rd instanceof MethodDecl) {
197                
198                        MethodDecl md = (MethodDecl) e;
199    
200                        checkTypeModifiers(rootEnv, md.returnType);
201                  
202                        returnType = md.returnType;
203    
204                        if (md.body != null && !specOnly) {
205                  
206                            if(Modifiers.isAbstract(md.modifiers))
207                                ErrorSet.error(md.loc, 
208                                               "An abstract method cannot include a body");
209                            if(Modifiers.isNative(md.modifiers))
210                                ErrorSet.error(md.loc, 
211                                               "A native method cannot include a body");
212                        } else {
213    /* We allow any method to have no body -- DRCok
214                            if(!Modifiers.isAbstract(md.modifiers)
215                               && !Modifiers.isNative(md.modifiers) && !specOnly)
216                                ErrorSet.error(md.loc, 
217                                               "Method must include a body unless "
218                                               +"it is declared abstract or native");
219    */
220                        }
221                    } else {
222                        // Constructor
223                        ConstructorDecl cd = (ConstructorDecl)rd;
224    
225                        // Was checked in parser
226                        Assert.notFalse(!(d instanceof InterfaceDecl)); //@ nowarn Pre;
227    
228                        // Modifiers were checked when we prep'ed the constructed
229                        returnType = Types.voidType;
230    
231                        // Check if we need to add an implicit constructor invocation
232                        //@ assume !specOnly ==> cd.body != null;
233                        if(!dontAddImplicitConstructorInvocations && !specOnly &&
234                            cd.body != null && // FIXME - we've broken the assumption above by allowing spec files - need to fix that uniformly
235                            !(cd.body.stmts.size() > 0
236                              && cd.body.stmts.elementAt(0) instanceof 
237                              ConstructorInvocation)) {
238                            // no explicit constructor invocation
239                            if(sig != Types.javaLangObject()) {
240                                // add implicit constructor invocation
241    
242                                ExprVec args = ExprVec.make();
243                                ConstructorInvocation ci 
244                                    = ConstructorInvocation.make(true, null, Location.NULL,
245                                                                 cd.body.locOpenBrace,
246                                                                 cd.body.locOpenBrace, args);
247                                cd.body.stmts.insertElementAt(ci, 0);
248                            }
249                        }
250                    }
251    
252                    // Now do stuff common to methods and constructors.
253    
254                    leftToRight = false;
255                    enclosingLabels.removeAllElements();
256              
257                    allowedExceptions.removeAllElements();
258                    for(int j=0; j<rd.raises.size(); j++) {
259                        TypeName n = rd.raises.elementAt(j);
260                        rootEnv.resolveType(sig,n);
261                        checkTypeModifiers(rootEnv, n);
262                        allowedExceptions.addElement(TypeSig.getSig(n));
263                    }
264    
265                    Env env = new EnvForEnclosedScope(rootEnv);
266                    for(int j = 0; j < rd.args.size(); j++) {
267                        FormalParaDecl formal = rd.args.elementAt(j);
268                        PrepTypeDeclaration.inst.
269                            checkModifiers(formal.modifiers, Modifiers.ACC_FINAL, 
270                                           formal.getStartLoc(), "formal parameter");
271                        checkModifierPragmaVec(formal.pmodifiers, formal, rootEnv);
272    
273                        env = new EnvForLocals(env, formal);
274                        checkTypeModifiers(env, formal.type);
275                    }
276    
277                    // Process ModifierPragmas
278                    checkModifierPragmaVec(rd.pmodifiers, rd, env);
279              
280                    if (rd.body != null) {
281                        checkStmt(env, rd.body);
282                    }
283    
284                    break;
285                }
286            
287                case TagConstants.INITBLOCK: {
288                    InitBlock si = (InitBlock) e;
289                    PrepTypeDeclaration.inst.
290                        checkModifiers(si.modifiers, Modifiers.ACC_STATIC, 
291                                       si.getStartLoc(), "initializer body");
292                    Env rootEnv = Modifiers.isStatic(si.modifiers) ? rootSEnv : rootIEnv;
293                    returnType = null;
294                    checkStmt(new EnvForEnclosedScope(rootEnv), si.block);
295                    break;
296                }
297            
298                case TagConstants.CLASSDECL:
299                case TagConstants.INTERFACEDECL: {
300                    TypeSig.getSig((TypeDecl)e).typecheck();
301                    break;
302                }
303    
304                default:
305                    if(e instanceof TypeDeclElemPragma)
306                        checkTypeDeclElemPragma((TypeDeclElemPragma)e);
307                    else
308                        Assert.fail("Switch fall-through (" + e.getTag() + ")");
309            }
310        }
311    
312    
313        /**
314         * Typecheck a statement in a given environment then return the environment in
315         * effect for statements that follow the given statement.
316         *
317         * <p> (The returned environment will be the same as the one passed in unless the
318         * statement is a declaration.)
319         *
320         * </p>
321         */
322        //@ requires e != null && s != null;
323        //@ requires !(e instanceof EnvForCU);
324        //@ requires sig != null;
325        //@ ensures \result != null;
326        //@ ensures !(\result instanceof EnvForCU);
327        protected Env checkStmt(Env e, Stmt s) {
328    
329    
330            switch (s.getTag()) {
331      
332                /*
333                 * Handle declarations first:
334                 */
335    
336                case TagConstants.VARDECLSTMT: {
337                    LocalVarDecl x = ((VarDeclStmt)s).decl;
338                    e.resolveType(sig,x.type);
339                    checkTypeModifiers(e, x.type);
340                    PrepTypeDeclaration.inst.
341                        checkModifiers(x.modifiers, Modifiers.ACC_FINAL,
342                                       x.locId, "local variable");
343                    checkModifierPragmaVec(x.pmodifiers, x, e);
344    
345                    Env newEnv = new EnvForLocals(e,x);
346                    if (x.init != null)
347                        x.init = checkInit(newEnv, x.init, x.type);
348                    return newEnv;
349                }
350    
351                case TagConstants.CLASSDECLSTMT: {
352                    ClassDeclStmt cds = (ClassDeclStmt)s;
353    
354                    // Create and check TypeSig for declared type:
355                    // Note: this code was altered to pass the new environment including the
356                    // new class into the TypeSig for the class.  Without that change, uses of
357                    // the class name inside the class were not resolved.  I'm not sure that
358                    // this is correct for all matters of scope and name visibility, but it
359                    // solves this problem.  -- DRCok 10/2/2003
360                    Env newenv = new EnvForLocalType(e, cds.decl);
361                    TypeSig T = Types.makeTypeSig(cds.decl.id.toString(), newenv, cds.decl);
362                    T.typecheck();
363    
364                    return newenv;
365                }
366    
367    
368                    /*
369                     * Next handle switch statement & associated statements; it needs
370                     * special treatment to deal with labels properly.
371                     */
372    
373                case TagConstants.SWITCHLABEL:
374                    Assert.precondition("Switch label passed to checkStmt!");
375    
376    
377                case TagConstants.SWITCHSTMT: {
378                    SwitchStmt c = (SwitchStmt)s;
379                    c.expr = checkExpr(e, c.expr);
380                    Env env = e;
381    
382                    // Now do special handling of the following block with case stmts
383    
384                    Type switchType = getType(c.expr);
385                    if (!Types.isIntegralType(switchType)||Types.isLongType(switchType)) {
386                        ErrorSet.error(c.expr.getStartLoc(),
387                                       "The type of a switch expression must be char,"
388                                       + " byte, short, or int.");
389                        switchType = Types.intType;
390                    }
391    
392    
393                    // What case values encountered so far. 
394                    Hashtable switchValues = new Hashtable();
395    
396                    boolean defaultEncountered = false;
397                    enclosingLabels.addElement(c);
398    
399                    for(int i = 0, sz = c.stmts.size(); i < sz; i++) {
400                        Stmt stmt = c.stmts.elementAt(i);
401        
402                        if (stmt.getTag() == TagConstants.SWITCHLABEL) {
403                            SwitchLabel x = (SwitchLabel)stmt;
404                            if (x.expr != null) {
405                                x.expr = checkExpr(env, x.expr);
406                                Object val = ConstantExpr.eval(x.expr);
407                                // System.out.println("At "+Location.toString(x.expr.getStartLoc()));
408                  
409                                if(val == null)             
410                                    ErrorSet.error(x.loc, "Non-constant value in switch label");
411                                else if(!ConstantExpr.
412                                         constantValueFitsIn(val, (PrimitiveType)switchType)) 
413                                    ErrorSet.error(x.loc, 
414                                                   "Case label value (" + val
415                                                   +") not assignable to "
416                                                   +"the switch expression type "
417                                                   +Types.printName(switchType));
418                                else {
419                                    // Check if it is a duplicate
420                                    // val may be Integer or Long, convert to Long for
421                                    // duplicate checking
422                                    Assert.notFalse(val instanceof Long    //@ nowarn Pre;
423                                                    || val instanceof Integer);
424                                    Long valLong = new Long(ConstantExpr.getLongConstant(val));
425                                    if(switchValues.containsKey(valLong)) {
426                                            // Point to dup label - FIXME
427                                        ErrorSet.error(x.loc, 
428                                                       "Duplicate case label "+val
429                                                       +" in switch statement");
430                                    } else {
431                                        switchValues.put(valLong,valLong);
432                                    }
433                                }
434                            } else {
435                                // this is default
436                                if(defaultEncountered)
437                                            // Point to dup label - FIXME
438                                    ErrorSet.error(x.loc, 
439                                                   "Duplicate default label in switch statement");
440                                else
441                                    defaultEncountered = true;
442                            }
443                
444                        } else
445                            env = checkStmt(env, stmt);
446                    }
447    
448                    enclosingLabels.pop();
449                    return e;
450                }
451    
452    
453                    /*
454                     * Finally handle remaining statements.
455                     */
456    
457                case TagConstants.BREAKSTMT:
458                case TagConstants.CONTINUESTMT: {
459                    BranchStmt bs = (BranchStmt)s;
460                    Stmt dest = null;
461                    int size = enclosingLabels.size();
462    
463                    String expectedStmtKind =
464                        s.getTag() == TagConstants.BREAKSTMT ? "switch, while, do, or for" 
465                        : "while, do or for" ;
466                
467                    for(int i=size-1; i>=0 && dest==null; i--) {
468                        Stmt ati = enclosingLabels.elementAt(i);
469                        Stmt target 
470                            = ati instanceof LabelStmt ? ((LabelStmt)ati).stmt : ati;
471              
472                        // continue target must be a loop statement
473                        // unlabelled break target must be a loop or switch
474                        // labelled break can be any statement
475              
476                        boolean loopTarget = 
477                            (target instanceof ForStmt)
478                            || (target instanceof WhileStmt)
479                            || (target instanceof DoStmt);
480    
481                        boolean validTarget = 
482                            loopTarget
483                            || (s.getTag() == TagConstants.BREAKSTMT 
484                                && (target instanceof SwitchStmt
485                                    || bs.label != null));
486    
487                        if(bs.label == null) {
488                            if(validTarget)
489                                dest = target;
490                            else 
491                                continue;
492                        } else if(ati instanceof LabelStmt
493                                   && ((LabelStmt)ati).label == bs.label) {
494                            if(!validTarget)
495                                ErrorSet.caution(bs.loc, 
496                                                 "Enclosing statement labelled '"
497                                                 +bs.label+"' is not a "
498                                                 +expectedStmtKind+" statement");
499                            // just give a warning and continue, since javac accepts this
500                            dest = target;
501                        }
502                        // else continue
503                    }
504    
505                    if(dest == null) {
506                        ErrorSet.error(bs.loc, 
507                                       bs.label == null 
508                                       ? "No enclosing unlabelled "+expectedStmtKind+" statement"
509                                       : "No enclosing "+expectedStmtKind+" statement labelled '"+bs.label+"'");
510                    } else
511                        setBranchLabel(bs, dest);
512    
513                    return e;
514                }
515    
516                case TagConstants.SKIPSTMT:
517                    return e;
518      
519                case TagConstants.RETURNSTMT: {
520                    ReturnStmt rs = (ReturnStmt)s;
521    
522                    if(rs.expr != null) 
523                        rs.expr = checkExpr(e, rs.expr);
524    
525                    if(returnType == null) 
526                        ErrorSet.error(rs.loc, 
527                                       "Returns are not allowed in a static initializer");
528                    else {
529                        if(rs.expr != null) {
530                            Type res = getType(rs.expr);
531    
532                            if(Types.isSameType(returnType, Types.voidType))
533                                ErrorSet.error(rs.loc, 
534                                               "This routine is not expected to return a value");
535                            else if(!assignmentConvertable(rs.expr, returnType)) {
536                                if (!Types.isErrorType(res))
537                                    ErrorSet.error(rs.loc, 
538                                                "Cannot convert "+Types.printName(res)
539                                                +" to return type "+Types.printName(returnType));
540                            }
541                        } else {
542                            if(!Types.isSameType(returnType, Types.voidType))
543                                ErrorSet.error(rs.loc, "This routine must return a value");
544                        }
545                    }
546                    return e;
547                }
548    
549                case TagConstants.THROWSTMT: {
550                    ThrowStmt t = (ThrowStmt)s;
551                    t.expr = checkExpr(e, t.expr);
552                    Type res = getType(t.expr);
553    
554                    if(!Types.isSubclassOf(res, Types.javaLangThrowable())) {
555                        ErrorSet.error(t.loc, 
556                                        "Cannot throw values of type "+Types.printName(res));
557                    } else {
558    
559                        if (Types.isCheckedException(res)) {
560              
561                            // Must be caught by try or throws clause
562                            for(int i=0; i<allowedExceptions.size(); i++) {
563                                if(Types.isSubclassOf(res, allowedExceptions.elementAt(i)))
564                                    // is ok
565                                    return e;
566                            }
567                            // Not caught
568                            ErrorSet.error(t.loc, 
569                                            "Exception must be caught by an enclosing try "
570                                            +"or throws clause");
571                        }
572                    }
573                    return e;
574                }
575    
576                case TagConstants.BLOCKSTMT:
577                    checkStmtVec(e, ((GenericBlockStmt)s).stmts);
578                    return e;
579          
580                case TagConstants.WHILESTMT: {
581                    WhileStmt w = (WhileStmt)s;
582                    w.expr = checkExpr(e, w.expr, Types.booleanType);
583                    enclosingLabels.addElement(w);
584                    checkStmt(e, w.stmt);
585                    enclosingLabels.pop();
586                    return e;
587                }
588          
589                case TagConstants.DOSTMT: {
590                    DoStmt d = (DoStmt)s;
591                    d.expr = checkExpr(e, d.expr, Types.booleanType);
592                    enclosingLabels.addElement(d);
593                    checkStmt(e, d.stmt);
594                    enclosingLabels.pop();
595                    return e;
596                }
597          
598                case TagConstants.IFSTMT: {
599                    IfStmt i = (IfStmt)s;
600                    i.expr = checkExpr(e, i.expr, Types.booleanType);
601                    checkStmt(e, i.thn);
602                    checkStmt(e, i.els);
603                    return e;
604                }
605          
606                case TagConstants.SYNCHRONIZESTMT: {
607                    SynchronizeStmt ss = (SynchronizeStmt)s;
608                    ss.expr = checkExpr(e, ss.expr, Types.javaLangObject());
609                    checkStmt(e, ss.stmt);
610                    return e;
611                }
612          
613                case TagConstants.EVALSTMT: {
614                    EvalStmt v = (EvalStmt) s;
615                    v.expr = checkExpr(e, v.expr);
616                    return e;
617                }
618          
619                case TagConstants.LABELSTMT: {
620                    LabelStmt ls = (LabelStmt)s;
621                    for(int i=0; i<enclosingLabels.size(); i++) {
622                        Stmt enclosing = enclosingLabels.elementAt(i);
623                        if(enclosing instanceof LabelStmt 
624                            && ((LabelStmt)enclosing).label == ls.label)
625                            ErrorSet.error(ls.locId, 
626                                           "Label '"+ls.label+"' already used in this scope");
627                                    // FIXME - point to dup
628                    }
629        
630                    enclosingLabels.addElement(ls);
631                    checkStmt(e, ls.stmt);
632                    enclosingLabels.pop();
633    
634                    return e;
635                }
636          
637                case TagConstants.TRYFINALLYSTMT: {
638                    TryFinallyStmt tf = (TryFinallyStmt)s;
639                    checkStmt(e, tf.tryClause);
640                    checkStmt(e, tf.finallyClause);
641                    return e;
642                }
643          
644                case TagConstants.TRYCATCHSTMT: {
645                    TryCatchStmt tc = (TryCatchStmt)s;
646                    TypeSigVec newExceptions = allowedExceptions.copy();
647    
648                    // add all catch clause exceptions to allowedExceptions
649                    for(int i=0; i<tc.catchClauses.size(); i++) {
650                        CatchClause c = tc.catchClauses.elementAt(i);
651                        Type t = c.arg.type;
652                        e.resolveType(sig,t);
653                        checkTypeModifiers(e, t);
654                        if(!Types.isSubclassOf(t, Types.javaLangThrowable()))
655                            ErrorSet.error(c.loc, 
656                                            "Declared type of a catch formal parameter "
657                                            +"must be a subclass of java.lang.Throwable");
658                        else {
659                            if (t instanceof TypeName) {
660                                t = TypeSig.getSig((TypeName)t);
661                            }
662                            newExceptions.addElement((TypeSig)t);
663                        }
664                        PrepTypeDeclaration.inst.checkModifiers(c.arg.modifiers,
665                                                                Modifiers.ACC_FINAL,
666                                                                c.arg.getStartLoc(),
667                                                                "formal parameter");
668    
669                        EnvForLocals subenv = new EnvForLocals(e, c.arg, false);
670                        checkStmt(subenv, c.body);
671                    }
672    
673                    TypeSigVec oldExceptions = allowedExceptions;
674                    allowedExceptions = newExceptions;
675                    checkStmt(e, tc.tryClause);
676                    allowedExceptions = oldExceptions;
677    
678                    return e;
679                }
680    
681                case TagConstants.FORSTMT: {
682                    ForStmt f = (ForStmt) s;
683                    Env se = checkStmtVec(e, f.forInit);
684                    checkForLoopAfterInit(se, f);
685                    return e;
686                }
687          
688                case TagConstants.CONSTRUCTORINVOCATION: {
689                    ConstructorInvocation ci = (ConstructorInvocation)s;
690    
691                    TypeSig calleeSig =
692                        ci.superCall 
693                        ? TypeSig.getSig(((ClassDecl)sig.getTypeDecl()) //@nowarn Cast,NonNull;
694                                         .superClass)
695                        : sig;
696    
697                    /*
698                     * Everything before the constructor invocation call occurs is
699                     * considered to be in a static context:
700                     */
701                    Env sEnv = e.asStaticContext();
702    
703                    Type[] argTypes = checkExprVec(sEnv, ci.args);
704    
705    
706                    /*
707                     * Handle type checking/inference for enclosing instance ptr:
708                     */
709    
710                    // Get the type of calleeSig's enclosing instance or null if none
711                    // exists:
712                    TypeSig enclosingInstanceType = calleeSig.getEnv(false)
713                        .getEnclosingInstance();
714    
715                    // If calleeSig has an enclosing instance and the user didn't supply
716                    // a value for it, try to infer one:
717                    if (ci.enclosingInstance==null && enclosingInstanceType != null) {
718                        ci.locDot = ci.getStartLoc();
719                        ci.enclosingInstance =
720                            sEnv.lookupEnclosingInstance(enclosingInstanceType,
721                                                         ci.getStartLoc());
722                    }
723    
724                    if (ci.enclosingInstance != null) {
725                        if (enclosingInstanceType != null)
726                            ci.enclosingInstance = checkExpr(sEnv,
727                                                             ci.enclosingInstance,
728                                                             enclosingInstanceType);
729                        else
730                            ErrorSet.error(ci.enclosingInstance.getStartLoc(),
731                                           "An enclosing instance may be provided only "
732                                           + "when the superclass has an enclosing instance");
733                    } else if (enclosingInstanceType != null) {
734                        /*
735                         * Compute appropriate error message details:
736                         */
737                        String details;
738                        if (ci.locKeyword == sig.getTypeDecl().locOpenBrace) {
739                            // inferred constructor with an inferred super inside it:
740                            details = "cannot create a default constructor for class "
741                                + sig + ".";
742                        } else if (ci.locKeyword == ci.locOpenParen) {
743                            // inferred super(...) in an explicit constructor:
744                            details = "cannot create a default superclass constructor."
745                                + "  (superclass is " + calleeSig + ")";
746                        } else {
747                            // explicit super(...) case...
748                            details = "an explicit one must be"
749                                + " provided when creating inner class "
750                                + calleeSig + ".";
751                        }
752    
753                        ErrorSet.error(ci.getStartLoc(),
754                                       "No enclosing instance of class "
755                                       + enclosingInstanceType
756                                       + " is in scope; " + details);
757                    }
758    
759    
760                    try {
761                        ConstructorDecl cd 
762                            = calleeSig.lookupConstructor(argTypes, sig);
763                        Assert.notNull(cd);
764                        ci.decl = cd;
765                    } catch(LookupException ex) {
766                        // Don't print an error if superclass is an interface (an
767                        // error has already been reported in this case)
768                        if (! ci.superCall
769                            || calleeSig.getTypeDecl().getTag() == TagConstants.CLASSDECL)
770                            reportLookupException(ex, 
771                                                  "constructor " + calleeSig.getTypeDecl().id
772                                                  + Types.printName(argTypes), 
773                                                  Types.printName(calleeSig), 
774                                                  ci.locKeyword);
775                    }
776    
777                    // Rest of constructor body is in the normal non-static context:
778                    return e;
779                }
780    
781                case TagConstants.ASSERTSTMT: {
782                    AssertStmt assertStmt = (AssertStmt)s;
783                    if (assertStmt.label != null)
784                        assertStmt.label = checkExpr(e, assertStmt.label);
785                    assertStmt.pred = checkExpr(e, assertStmt.pred, Types.booleanType);
786    
787                    // Turn a Java assert into a conditional throw and attach it to the
788                    // AssertStmt.
789    
790                    // assert Predicate ;
791                    // ==>
792                    // if (! Predicate)
793                    //   throw new java.lang.AssertionError();
794                    // or
795                    // assert Predicate : LabelExpr ;
796                    // ==>
797                    // if (! Predicate)
798                    //   throw new java.lang.AssertionError(LabelExpr);
799                    int startLoc = assertStmt.getStartLoc();
800                    int endLoc = assertStmt.getEndLoc();
801                    Assert.notFalse(startLoc != Location.NULL);
802                    UnaryExpr negatedPredicate = 
803                        UnaryExpr.make(TagConstants.NOT, assertStmt.pred, startLoc);
804                    ParenExpr parenthesizedNegatedPredicate =
805                        ParenExpr.make(negatedPredicate, startLoc, endLoc);
806                    Name javaLangAssertionErrorName = 
807                        Name.make("java.lang.AssertionError", startLoc);
808                    TypeName javaLangAssertionTypeName = TypeName.make(javaLangAssertionErrorName);
809                    ExprVec constructorArgs = null;
810                    if (assertStmt.label != null) {
811                        Expr [] constructorArgsAsArray = { assertStmt.label };
812                        constructorArgs = ExprVec.make(constructorArgsAsArray);
813                    } else {
814                        constructorArgs = ExprVec.make();
815                    }
816                    NewInstanceExpr newAssertionError = 
817                        NewInstanceExpr.make(null, Location.NULL, javaLangAssertionTypeName,
818                                             constructorArgs, null, startLoc, endLoc);
819                    ThrowStmt throwAssertionError = ThrowStmt.make(newAssertionError, 
820                                                                   startLoc);
821                    Stmt elseSkip = SkipStmt.make(startLoc);
822                    IfStmt ifStmt = IfStmt.make(parenthesizedNegatedPredicate, throwAssertionError, 
823                                                elseSkip, startLoc);
824                    // Now typecheck the generated IfStmt so that it is fully resolved.
825                    ifStmt.expr = checkExpr(e, ifStmt.expr, Types.booleanType);
826                    checkStmt(e, ifStmt.thn);
827                    checkStmt(e, ifStmt.els);
828                    // Reattach this translated form to the AST node.
829                    assertStmt.ifStmt = ifStmt;
830    
831                    return e;
832                }
833    
834                default:
835                    if(s instanceof StmtPragma)
836                        checkStmtPragma(e, (StmtPragma)s);
837                    else {
838                        Assert.fail("Switch fall-through (" + s.getTag() + " " +
839                            TagConstants.toString(s.getTag()) + " " +
840                            Location.toString(s.getStartLoc()) + ")");
841                    }
842            }
843            return e;                       // dummy
844        }
845    
846        //@ requires !(se instanceof EnvForCU);
847        //@ requires sig != null;
848        protected void checkForLoopAfterInit(/*@ non_null */ Env se,
849                                             /*@ non_null */ ForStmt f) {
850            f.test = checkExpr(se, f.test);
851            for (int i = 0; i < f.forUpdate.size(); i++) {
852                Expr ex = checkExpr(se, f.forUpdate.elementAt(i));
853                f.forUpdate.setElementAt(ex, i);
854            }
855            enclosingLabels.addElement(f);
856            checkStmt(se, f.body);
857            enclosingLabels.pop();
858        }
859    
860        //@ requires env != null && v != null;
861        //@ requires !(env instanceof EnvForCU);
862        //@ requires sig != null;
863        //@ ensures \result != null;
864        //@ ensures !(\result instanceof EnvForCU);
865        protected Env checkStmtVec(Env env, StmtVec v) {
866            for(int i = 0, sz = v.size(); i < sz; i++) {
867                Stmt stmt = v.elementAt(i);
868                
869                env = checkStmt(env, stmt);
870            }
871    
872            return env;
873        }
874    
875      
876        //@ requires env != null && ev != null  ;
877        //@ requires !(env instanceof EnvForCU);
878        //@ requires sig != null;
879        //@ ensures \nonnullelements(\result);
880        protected Type[] checkExprVec(Env env, ExprVec ev) {
881    
882            Type[] r = new Type[ ev.size() ];
883    
884            for(int i = 0; i < ev.size(); i++) {
885                Expr expr = ev.elementAt(i);
886                Expr newExpr = checkExpr(env, expr);
887                ev.setElementAt(newExpr, i);
888                r[i] = getType(newExpr);
889            }
890    
891            return r;
892        }
893    
894    
895        //@ requires sig != null;
896        //@ requires !(env instanceof EnvForCU);
897        //@ requires env != null && x != null && expectedResult != null;
898        //@ ensures \result != null;
899        //@ ensures (x instanceof ArrayInit) ==> \result instanceof ArrayInit;
900        protected VarInit checkInit(Env env, VarInit x, Type expectedResult) {
901            if (x instanceof ArrayInit) {
902                ArrayInit ai = (ArrayInit)x;
903    
904                if(expectedResult instanceof ArrayType) {
905                    Type elemType = ((ArrayType)expectedResult).elemType;
906                    for(int i=0; i< ai.elems.size(); i++) {
907                        VarInit disamb = checkInit(env, ai.elems.elementAt(i), elemType);
908                        ai.elems.setElementAt(disamb, i);
909                    }
910                    setType(ai, expectedResult);
911                } else {
912                    ErrorSet.error(ai.locOpenBrace, 
913                                   "Unexpected array value in initializer");
914                }
915                return x;
916    
917            } else {
918                //@ assume \typeof(x) <: \type(Expr);
919                return checkExpr(env, (Expr) x, expectedResult);
920            }
921        }
922    
923        //@ requires env != null && e != null;
924        //@ requires !(env instanceof EnvForCU);
925        //@ requires sig != null;
926        //@ ensures \result != null;
927        protected Expr checkDesignator(Env env, Expr e) {
928            Expr result = checkExpr(env, e);
929            if (result.getTag() == TagConstants.FIELDACCESS) {
930                FieldAccess fa = (FieldAccess)result;
931                if (fa.decl == Types.lengthFieldDecl) {
932                    ErrorSet.error(fa.locId, "Invalid designator");
933                }
934                // Note, if it weren't for some Java 1.1 features, one could also
935                // rule out the case:
936                //   fa.decl != null && Modifiers.isFinal(fa.decl.modifiers)
937                // here with a message "Final fields cannot be used as designators",
938                // but Java 1.1 allows assignments to final fields in some contexts.
939                // A more elaborate test could perhaps be used, though.
940            }
941            return result;
942        }
943    
944        //@ requires env != null && expr != null && t != null;
945        //@ requires !(env instanceof EnvForCU);
946        //@ requires sig != null;
947        //@ ensures \result != null;
948        protected Expr checkExpr(Env env, Expr expr, Type t) {
949            Expr ne = checkExpr(env,expr);
950            checkType(ne, t);
951            return ne;
952        }
953    
954        /**
955         * This method should call <code>setType</code> on <code>x</code> before its
956         * done.
957         */
958        //@ requires env != null && x != null;
959        //@ requires !(env instanceof EnvForCU);
960        //@ requires sig != null;
961        //@ ensures \result != null;
962        protected Expr checkExpr(Env env, Expr x) {
963    
964            // System.out.println("Checking: "+Location.toString(x.getStartLoc()));
965    
966            if (getTypeOrNull(x) != null)
967                // already done
968                return x;
969    
970            // set default result type to integer, in case there is an error
971            setType(x, Types.intType);
972    
973            switch (x.getTag()) {
974        
975                case TagConstants.THISEXPR: {
976                    ThisExpr t = (ThisExpr)x;
977    
978                    if (env.isStaticContext() && t.classPrefix==null) {
979                        ErrorSet.error(x.getStartLoc(),
980                           "Unqualified this cannot be used in static contexts");
981                    }
982    
983                    Type referredType = sig;
984                    if (t.classPrefix != null) {
985                        env.resolveType(sig,t.classPrefix);
986                        referredType = t.classPrefix;
987                        checkTypeModifiers(env, referredType);
988    
989                        /*
990                         * Check that t.classPrefix is the class of one of our
991                         * current/enclosing instances:
992                         */
993                        TypeSig classPrefix = Types.toClassTypeSig(referredType);
994                        if (classPrefix==null || !env.canAccessInstance(classPrefix)) {
995                            ErrorSet.error(t.getStartLoc(),
996                                           "Undefined variable: "
997                                           + PrettyPrint.inst.toString(referredType)
998                                           + ".this");
999                            setType(x, Types.errorType);
1000                            return x;
1001                        }
1002                    }
1003    
1004                    setType(x, referredType);
1005                    return x;
1006                }
1007        
1008                case TagConstants.STRINGLIT:
1009                    setType(x, Types.javaLangString());
1010                    return x;
1011    
1012                case TagConstants.CHARLIT:
1013                    setType(x, Types.charType);
1014                    return x;
1015    
1016                case TagConstants.BOOLEANLIT:
1017                    setType(x, Types.booleanType);
1018                    return x;
1019    
1020                case TagConstants.FLOATLIT:
1021                    setType(x, Types.floatType);
1022                    return x;
1023    
1024                case TagConstants.DOUBLELIT:
1025                    setType(x, Types.doubleType);
1026                    return x;
1027    
1028                case TagConstants.INTLIT: 
1029                    setType(x, Types.intType);
1030                    return x;
1031    
1032                case TagConstants.LONGLIT:
1033                    setType(x, Types.longType);
1034                    return x;
1035    
1036                case TagConstants.NULLLIT:
1037                    setType(x, Types.nullType);
1038                    return x;
1039        
1040                case TagConstants.ARRAYREFEXPR: {
1041                    ArrayRefExpr r = (ArrayRefExpr)x;
1042            
1043                    r.array = checkExpr(env, r.array);
1044                    Type arrType = getType(r.array);
1045            
1046                    if(arrType instanceof ArrayType) {
1047                        setType(r, ((ArrayType)arrType).elemType);
1048                    } else {
1049                        setType(r, Types.errorType);
1050                        if (!Types.isErrorType(arrType))
1051                            ErrorSet.error(r.locOpenBracket, 
1052                                        "Attempt to index a non-array value");
1053                    }
1054              
1055                    r.index = checkExpr(env, r.index);
1056                    Type t = getType(r.index);
1057                    Type ndxType = Types.isNumericType(t) ? Types.unaryPromote(t) : t;
1058                    if(!Types.isSameType(ndxType, Types.intType) &&
1059                       !Types.isErrorType(ndxType)) 
1060                        ErrorSet.error(r.locOpenBracket, "Array index is not an integer");
1061    
1062                    return r;
1063                }
1064    
1065                case TagConstants.NEWINSTANCEEXPR: {
1066                    NewInstanceExpr ne = (NewInstanceExpr)x;
1067    
1068                    /*
1069                     * We handle the "scoping" of ne.type differently depending on
1070                     * whether or not an explicit enclosing instance ptr is
1071                     * provided:
1072                     */
1073                    TypeSig calleeSig;
1074                    if (ne.enclosingInstance==null) {
1075                        // 1.0 case:  new N(...) ...
1076                        env.resolveType(sig,ne.type);
1077                        checkTypeModifiers(env, ne.type);
1078                        calleeSig = TypeSig.getSig(ne.type);
1079                    } else {
1080                        // 1.1 case: E.new I(...) ...
1081    
1082                        // Type check E to get class type enclosingType:
1083                        ne.enclosingInstance = checkExpr(env, ne.enclosingInstance);
1084                        TypeSig enclosingInstanceType;
1085                        try {
1086                            enclosingInstanceType =
1087                                (TypeSig)getType(ne.enclosingInstance);  //@ nowarn Cast;//caught
1088                        } catch (ClassCastException E) {
1089                            ErrorSet.error(ne.enclosingInstance.getStartLoc(),
1090                                           "The enclosing instance supplied in a new"
1091                                           + " expression must be of a class type.");
1092                            enclosingInstanceType = Types.javaLangObject();
1093                        }
1094    
1095                        // Check and "resolve" I:
1096                        if (ne.type.name.size() != 1)
1097                            ErrorSet.error(ne.type.getStartLoc(),
1098                                           "Only a simple name can be used after new"
1099                                           + " when an enclosing instance is supplied.");
1100                        Identifier id = ne.type.name.identifierAt(0);
1101                        int idLoc = ne.type.name.locIdAt(0);
1102                        calleeSig = enclosingInstanceType.lookupType(enclosingInstanceType, id, idLoc);
1103                        if (calleeSig==null)
1104                            ErrorSet.fatal(ne.type.getStartLoc(),
1105                                           "No such type: "
1106                                           + enclosingInstanceType.toString()+"$"+id);
1107                        checkTypeModifiers(env, ne.type);
1108                        TypeSig.setSig(ne.type, calleeSig);
1109                    }
1110    
1111    
1112                    /*
1113                     * Handle remaining type checking/inference for enclosing instance ptr:
1114                     */
1115    
1116                    // Get the type of calleeSig's enclosing instance or null if none
1117                    // exists:
1118                    TypeSig enclosingInstanceType = calleeSig.getEnv(false)
1119                        .getEnclosingInstance();
1120    
1121                    // If calleeSig has an enclosing instance and the user didn't supply
1122                    // a value for it, try to infer one:
1123                    if (ne.enclosingInstance==null && enclosingInstanceType != null) {
1124                        Expr enclosingInstance =
1125                            env.lookupEnclosingInstance(enclosingInstanceType,
1126                                                        ne.getStartLoc());
1127                        if (enclosingInstance != null) {
1128                            ne.locDot = ne.getStartLoc();
1129                            ne.enclosingInstance = enclosingInstance;
1130                            checkExpr(env, ne.enclosingInstance, enclosingInstanceType);
1131                        }
1132                    }
1133    
1134                    if (ne.enclosingInstance != null) {
1135                        if (enclosingInstanceType==null)
1136                            ErrorSet.error(ne.enclosingInstance.getStartLoc(),
1137                                           "An enclosing instance may be provided only "
1138                                           + "when the named instance type is an inner class");
1139                    } else if (enclosingInstanceType != null) {
1140                        ErrorSet.error(ne.getStartLoc(),
1141                                       "No enclosing instance of class "
1142                                       + enclosingInstanceType
1143                                       + " is in scope; an explicit one must be provided"
1144                                       + " when creating instances of inner class "
1145                                       + calleeSig + ".");
1146                    }
1147    
1148                    /*
1149                     * The type that will *actually* call the constructor
1150                     * 
1151                     * (matters if the constructor is "protected"!)
1152                     */
1153                    TypeSig caller = sig;
1154    
1155                    /*
1156                     * Handle anonymous class case:
1157                     */
1158                    if (ne.anonDecl != null) {
1159                        // Update anonDecl to have proper supertype:
1160                        if (calleeSig.getTypeDecl() instanceof ClassDecl) {
1161                            Assert.notFalse(ne.anonDecl.superClass==null);  //@ nowarn Pre;
1162                            ne.anonDecl.superClass = ne.type;
1163                        } else {
1164                            ne.anonDecl.superInterfaces.addElement(ne.type);
1165                            calleeSig = Types.javaLangObject();
1166                        }
1167    
1168                        // Create and check TypeSig for declared type:
1169                        TypeSig T = Types.makeTypeSig(null, env, ne.anonDecl);
1170                        T.typecheck();
1171                        caller = T;
1172                        setType(ne, T);
1173                    } else
1174                        setType(ne, ne.type);
1175    
1176    
1177                    Type[] argTypes = checkExprVec(env, ne.args);
1178    
1179                    if (!(calleeSig.getTypeDecl() instanceof ClassDecl))
1180                        ErrorSet.error(ne.loc, 
1181                                       "Cannot create an instance of an interface");
1182                    else if (Modifiers.isAbstract(calleeSig.getTypeDecl().modifiers)
1183                             && ne.anonDecl==null)
1184                        ErrorSet.error(ne.loc,
1185                                       "Cannot create an instance of an abstract class");
1186                    else { 
1187                        try {
1188                            ConstructorDecl cd = calleeSig.lookupConstructor(argTypes, caller);
1189                            ne.decl = cd;
1190                        } catch(LookupException e) {
1191                            reportLookupException(e, "constructor", 
1192                                                  Types.printName(calleeSig), ne.loc);
1193                        }
1194                    }
1195            
1196                    return ne;
1197                }
1198    
1199                case TagConstants.NEWARRAYEXPR: {
1200                    NewArrayExpr na = (NewArrayExpr)x;
1201                    env.resolveType(sig,na.type);
1202                    Type r = na.type;
1203                    checkTypeModifiers(env, r); 
1204                    for(int i = 0; i < na.dims.size(); i++) {
1205                        Expr e = na.dims.elementAt(i);
1206                        Expr newExpr = checkExpr(env, e, Types.intType);
1207                        na.dims.setElementAt(newExpr, i);
1208                        r = ArrayType.make(r, na.locOpenBrackets[i]);
1209                        checkTypeModifiers(env, r); 
1210                    }
1211                    setType(na, r);
1212    
1213                    if (na.init != null)
1214                        na.init = (ArrayInit)checkInit(env, na.init, r);
1215    
1216                    return na;
1217                }
1218    
1219                case TagConstants.CONDEXPR: {
1220                    CondExpr ce = (CondExpr)x;
1221                    ce.test = checkExpr(env, ce.test, Types.booleanType);
1222                    ce.thn = checkExpr(env, ce.thn);
1223                    ce.els = checkExpr(env, ce.els);
1224    
1225                    Type res = tryCondExprMatch(ce.thn, ce.els);
1226                    if (res != null)
1227                        setType(ce, res);
1228                    else
1229                        ErrorSet.error(ce.locQuestion,
1230                                        "Incompatible arguments to the ?: operator");
1231    
1232                    return ce;
1233                }
1234    
1235                case TagConstants.INSTANCEOFEXPR: {
1236                    InstanceOfExpr ie = (InstanceOfExpr)x;
1237                    ie.expr = checkExpr(env, ie.expr);
1238                    Type exprType = getType(ie.expr);
1239                    env.resolveType(sig,ie.type);
1240                    checkTypeModifiers(env, ie.type);
1241                    if(!Types.isReferenceType(ie.type)) {
1242                        ErrorSet.error(ie.loc, "Non-reference type in instanceof operation");
1243                    }
1244                    else if(!Types.isCastable(exprType, ie.type)) {
1245                        ErrorSet.error(ie.loc, 
1246                                       "Invalid instanceof operation: "+
1247                                       "A value of type "+Types.printName(exprType)
1248                                       +" can never be an instance of "
1249                                       +Types.printName(ie.type));
1250                    }
1251                    setType(ie, Types.booleanType);
1252                    return ie;
1253                }
1254    
1255                case TagConstants.CASTEXPR: {
1256                    CastExpr ce = (CastExpr)x;
1257                    ce.expr = checkExpr(env, ce.expr);
1258                    Type exprType = getType(ce.expr);
1259                    env.resolveType(sig,ce.type);
1260                    checkTypeModifiers(env, ce.type); 
1261     
1262                    if(!Types.isCastable(exprType, ce.type)) {
1263                        ErrorSet.error(ce.locOpenParen, 
1264                                       "Bad cast from "+Types.printName(exprType)
1265                                       +" to "+Types.printName(ce.type));
1266                    }
1267                    setType(ce, ce.type);
1268                    return ce;
1269                }
1270    
1271                case TagConstants.CLASSLITERAL: {
1272                    ClassLiteral cl = (ClassLiteral)x;
1273                    env.resolveType(sig,cl.type);
1274                    checkTypeModifiers(env, cl.type); 
1275                    setType(cl, Types.javaLangClass());
1276                    return cl;
1277                }
1278    
1279                case TagConstants.OR: case TagConstants.AND:
1280                case TagConstants.BITOR: case TagConstants.BITXOR:
1281                case TagConstants.BITAND: case TagConstants.NE:
1282                case TagConstants.EQ: case TagConstants.GE:
1283                case TagConstants.GT: case TagConstants.LE:
1284                case TagConstants.LT: case TagConstants.LSHIFT:
1285                case TagConstants.RSHIFT: case TagConstants.URSHIFT:
1286                case TagConstants.ADD: case TagConstants.SUB:
1287                case TagConstants.DIV: case TagConstants.MOD:
1288                case TagConstants.STAR: {
1289                    BinaryExpr be = (BinaryExpr)x;
1290                    be.left = checkExpr(env, be.left);
1291                    be.right = checkExpr(env, be.right);
1292                    Type t = checkBinaryExpr(be.op, be.left, be.right, be.locOp);
1293                    setType(be, t);
1294                    return be;
1295                }
1296          
1297                case TagConstants.ASSIGN: case TagConstants.ASGMUL:
1298                case TagConstants.ASGDIV: case TagConstants.ASGREM:
1299                case TagConstants.ASGADD: case TagConstants.ASGSUB:
1300                case TagConstants.ASGLSHIFT: case TagConstants.ASGRSHIFT:
1301                case TagConstants.ASGURSHIFT: case TagConstants.ASGBITAND:
1302                case TagConstants.ASGBITOR: case TagConstants.ASGBITXOR: {
1303                    BinaryExpr be = (BinaryExpr)x;
1304                    be.left = checkDesignator(env, be.left);
1305                    be.right = checkExpr(env, be.right);
1306                    Type t = checkBinaryExpr(be.op, be.left, be.right, be.locOp);
1307                    setType(be, t);
1308                    return be;
1309                }
1310    
1311                    // Unary operations
1312    
1313                case TagConstants.UNARYADD: 
1314                case TagConstants.UNARYSUB: {
1315                    UnaryExpr ue = (UnaryExpr)x;
1316                    ue.expr = checkExpr(env, ue.expr);
1317                    // Argument must be primitive numeric type
1318                    Type t = getType(ue.expr);
1319                    if(checkNumericType(ue.expr)) {
1320                        // Result is value of unary promoted type of arg
1321                        setType(ue, Types.unaryPromote(getType(ue.expr)));
1322                    }
1323                    return ue;
1324                }
1325    
1326                case TagConstants.BITNOT: {
1327                    UnaryExpr ue = (UnaryExpr)x;
1328                    ue.expr = checkExpr(env, ue.expr);
1329                    // Argument must be primitive numeric type
1330                    if(checkIntegralType(ue.expr)) {
1331                        // Result is value of unary promoted type of arg
1332                        setType(ue, Types.unaryPromote(getType(ue.expr)));
1333                    } 
1334                    return ue;
1335                }
1336    
1337                case TagConstants.INC: case TagConstants.DEC: 
1338                case TagConstants.POSTFIXINC: case TagConstants.POSTFIXDEC: {
1339                    UnaryExpr ue = (UnaryExpr)x;
1340                    ue.expr = checkDesignator(env, ue.expr);
1341    
1342                    if (ue.expr instanceof VariableAccess) {
1343                        GenericVarDecl v = ((VariableAccess)ue.expr).decl;
1344                        if (Modifiers.isFinal(v.modifiers))
1345                            ErrorSet.caution(ue.expr.getStartLoc(),
1346                                "May not assign to a final variable",
1347                                v.getStartLoc());
1348                    } else if (ue.expr instanceof FieldAccess) {
1349                        GenericVarDecl v = ((FieldAccess)ue.expr).decl;
1350                        // v is null if there was an error such as a field
1351                        // name that does not exist
1352                        if (v == Types.lengthFieldDecl) 
1353                            ErrorSet.error(ue.expr.getStartLoc(),
1354                                "May not assign to array's length field");
1355                        else if (v != null && Modifiers.isFinal(v.modifiers))
1356                            ErrorSet.caution(ue.expr.getStartLoc(),
1357                                "May not assign to a final field",
1358                                v.getStartLoc());
1359    
1360                    }
1361                        // FIXME - need checks of more complicated expressions
1362    
1363                    // Argument must be primitive numeric variable type
1364                    if (checkNumericType(ue.expr)) {
1365                        if(!isVariable(ue.expr))
1366                            ErrorSet.error(ue.locOp,
1367                                            "Argument of increment/decrement operation "
1368                                            +"is not a location");
1369                        // Result is of same type
1370                        setType(ue, getType(ue.expr));
1371                    }
1372                    return ue;
1373                }
1374          
1375                case TagConstants.NOT: {
1376                    // Argument must be boolean, result is boolean
1377                    UnaryExpr ue = (UnaryExpr)x;
1378                    ue.expr = checkExpr(env, ue.expr, Types.booleanType);
1379                    setType(ue, Types.booleanType);
1380                    return ue;
1381                }
1382          
1383                case TagConstants.PARENEXPR: {
1384                    ParenExpr pe = (ParenExpr)x;
1385                    pe.expr = checkExpr(env, pe.expr);
1386                    setType(pe, getType(pe.expr));
1387                    return pe;
1388                }
1389    
1390                case TagConstants.AMBIGUOUSVARIABLEACCESS: {
1391                    AmbiguousVariableAccess av = (AmbiguousVariableAccess)x;
1392                    Assert.notNull(av.name);
1393                    Expr resolved = env.disambiguateExprName(av.name);
1394                    if(resolved == null) {
1395                        if (av.name.size() == 1) {
1396                            ErrorSet.error(av.getStartLoc(),
1397                                           "Undefined variable '" + av.name.printName() + "'");
1398                        } else ErrorSet.error(av.getStartLoc(),
1399                                            "Cannot resolve variable access '"
1400                                            +av.name.printName()+"'");
1401                        setType(x, Types.errorType);
1402                        return av;
1403                    }
1404                    Assert.notFalse(resolved.getTag() !=
1405                                    TagConstants.AMBIGUOUSVARIABLEACCESS); 
1406                    return checkExpr(env, resolved);
1407                }
1408    
1409                case TagConstants.FIELDACCESS: {
1410                    FieldAccess fa = (FieldAccess)x;
1411                    Type t = checkObjectDesignator(env, fa.od);
1412                    if(t != null) {
1413                        try {
1414                            fa.decl = Types.lookupField(t, fa.id, sig);
1415                            setType(fa, fa.decl.type);
1416    
1417                            if (fa.od instanceof TypeObjectDesignator &&
1418                                !Modifiers.isStatic(fa.decl.modifiers)) {
1419                                // Is fa.decl an instance field of the same class as
1420                                // fa is part of?
1421                                boolean thisField = false;
1422                                if (fa.decl.parent != null)
1423                                    thisField = (env.getEnclosingClass()
1424                                                 .isSubtypeOf(TypeSig.getSig(fa.decl.parent)));
1425                                if (thisField ||
1426                                    ((TypeObjectDesignator)fa.od).type instanceof TypeName)
1427                                    ErrorSet.error(fa.locId,
1428                                                   "An instance field may be accessed only via "
1429                                                   + "an object and/or from a non-static"
1430                                                   + " context or an inner class enclosed"
1431                                                   + " by a type possessing that field.");
1432                                            // FIXME - point to declaration
1433                                else
1434                                    ErrorSet.error(fa.locId,
1435                                                   "The instance fields of type "
1436                                                   + ((TypeObjectDesignator)fa.od).type
1437                                                   + " may not be accessed from type "
1438                                                   + sig);
1439                                            // FIXME = point to declaration
1440                            }
1441                        } catch(LookupException ex) {
1442                            if (!Types.isErrorType(t))
1443                                reportLookupException(ex, "field", 
1444                                    Types.printName(t), fa.locId);
1445                            setType(fa, Types.errorType);
1446                        }
1447                    }
1448                    return fa;
1449                }
1450    
1451                case TagConstants.AMBIGUOUSMETHODINVOCATION: {
1452                    AmbiguousMethodInvocation ami = (AmbiguousMethodInvocation)x;
1453                    MethodInvocation resolved = env.disambiguateMethodName(ami);
1454                    if (resolved == null) {
1455                        // This currently never happens because non-resolvable
1456                        // ambiguous methods result in a fatal error.  (See EnvForTypeSig)
1457                        ErrorSet.error(ami.getStartLoc(),
1458                                        "Ambiguous method invocation");
1459                        return ami;
1460                    }
1461                    return checkExpr(env, resolved);
1462                }
1463    
1464                case TagConstants.METHODINVOCATION: {
1465                    MethodInvocation mi = (MethodInvocation)x;
1466                    Type t = checkObjectDesignator(env, mi.od);
1467                    Type[] argTypes = checkExprVec(env, mi.args);
1468                    if(t != null) {
1469                        try {
1470                            mi.decl = Types.lookupMethod(t, mi.id, argTypes, sig);
1471                            setType(mi, mi.decl.returnType);
1472    
1473                            if (mi.od instanceof TypeObjectDesignator &&
1474                                !Modifiers.isStatic(mi.decl.modifiers)) {
1475                                // Is mi.decl an instance method of the same class as
1476                                // mi is part of?
1477                                boolean thisMethod = false;
1478                                if (mi.decl.parent != null)
1479                                    thisMethod = 
1480                                        env.getEnclosingClass().isSubtypeOf(TypeSig.getSig(mi.decl.parent));
1481    
1482                                if (thisMethod ||
1483                                    ((TypeObjectDesignator)mi.od).type instanceof TypeName)
1484                                    ErrorSet.error(mi.locId, "An instance method may be invoked" +
1485                                                   " only via an object and/or from a non-static" +
1486                                                   " context or an inner class enclosed by a type" +
1487                                                   " possessing that method.");
1488                                else
1489                                    ErrorSet.error(mi.locId,
1490                                                   "The instance methods of type "
1491                                                   + ((TypeObjectDesignator)mi.od).type
1492                                                   + " may not be invoked from type "
1493                                                   + sig);
1494                            }
1495                        } catch(LookupException ex) {
1496                            if (!Types.isErrorType(t))
1497                                reportLookupException(ex, 
1498                                                  "method "+mi.id
1499                                                  +Types.printName(argTypes), 
1500                                                  Types.printName(t), mi.locId);
1501                            setType(mi, Types.errorType);
1502                        }
1503                    }
1504                    return mi;
1505                }
1506    
1507                case TagConstants.VARIABLEACCESS: {
1508                    VariableAccess lva = (VariableAccess)x;
1509                    setType(lva, lva.decl.type);
1510                    Assert.notNull(getType(lva));
1511    
1512                    // Front-end VariableAccess's never point to fields:
1513                    Assert.notFalse(!(lva.decl instanceof FieldDecl)); //@ nowarn Pre;
1514    
1515                    // Make sure only access final variables from enclosing instances:
1516                    if (Env.whereDeclared(lva.decl) != sig &&
1517                        !Modifiers.isFinal(lva.decl.modifiers))
1518                        ErrorSet.error(lva.loc,
1519                                       "Attempt to use a non-final variable"
1520                                       + " from a different method.  From enclosing"
1521                                       + " blocks, only final local variables are"
1522                                       + " available.");
1523    
1524                    return lva;
1525                }
1526    
1527                default:
1528                    System.out.println("FAIL " + x);
1529                    System.out.println(" AT " + Location.toString(x.getStartLoc())); 
1530                    Assert.fail("Switch fall-through (" + 
1531                                TagConstants.toString(x.getTag()) + ")");
1532                    return null;            // Dummy
1533            }
1534        }
1535    
1536        // ======================================================================
1537    
1538        //@ requires env != null && od != null;
1539        //@ requires !(env instanceof EnvForCU);
1540        //@ requires sig != null;
1541        protected Type checkObjectDesignator(Env env, ObjectDesignator od) {
1542    
1543            switch(od.getTag()) {
1544          
1545                case TagConstants.EXPROBJECTDESIGNATOR: {
1546                    ExprObjectDesignator eod = (ExprObjectDesignator)od;
1547                    eod.expr = checkExpr(env, eod.expr);
1548                    eod.type = getType(eod.expr);
1549                    return eod.type;
1550                }
1551    
1552                case TagConstants.TYPEOBJECTDESIGNATOR: {
1553                    TypeObjectDesignator tod = (TypeObjectDesignator)od;
1554                    // Type has been created by disambiguation code, so it is ok.
1555    
1556                    Type t = tod.type;
1557                    if(t instanceof TypeName) {
1558                        t = TypeSig.getSig((TypeName)t);
1559                        tod.type = t;
1560                    }
1561                    Assert.notFalse(t instanceof TypeSig);
1562                    checkTypeModifiers(env, t);  
1563                    return (TypeSig)t;
1564                }
1565    
1566                case TagConstants.SUPEROBJECTDESIGNATOR: {
1567                    SuperObjectDesignator sod = (SuperObjectDesignator)od;
1568                    if(env.isStaticContext()) {
1569                        ErrorSet.error(sod.locSuper,
1570                                       "Keyword super cannot be used in a static context");
1571                        return null;
1572                    }
1573                    else {
1574                        TypeDecl d = sig.getTypeDecl();
1575                        if (d instanceof ClassDecl) {
1576                            TypeName superClass = ((ClassDecl)d).superClass;
1577                            if (superClass==null) {
1578                                Assert.notFalse(sig==Types.javaLangObject()); //@ nowarn Pre;
1579                                ErrorSet.error(sod.locDot, 
1580                                                "Can't use keyword super in java.lang.Object");
1581                                return null;
1582                            }
1583    
1584                            TypeSig ts = TypeSig.getSig(superClass);
1585                            sod.type = ts;
1586                            return ts;
1587                        } else {
1588                            ErrorSet.error(sod.locDot, 
1589                                            "Can't use keyword super in an interface");
1590                            return null;
1591                        }
1592                    }
1593                }
1594    
1595                default:
1596                    Assert.fail("Fall thru");
1597                    return null; // dummy return
1598            }
1599        }
1600    
1601        // ======================================================================
1602    
1603        /**
1604         * Return the type of a E1 : L ? R expression given the typechecked Expr's for L
1605         * and R, as per JLS 15.24.
1606         *
1607         * @return null if the given combination is illegal.
1608         */
1609        //@ requires leftExpr != null && rightExpr != null;
1610        private Type tryCondExprMatch(Expr leftExpr, Expr rightExpr) {
1611            Type leftType = getType(leftExpr);
1612            Type rightType = getType(rightExpr);
1613                                              
1614            /*
1615             * If the second and third operands have the same type,
1616             * then than is the type of the conditional expression:
1617             */
1618            if (Types.isSameType(leftType, rightType))
1619                return leftType;
1620    
1621    
1622            /*
1623             * Rules for case where both L and R have numeric types:
1624             */
1625            if (Types.isNumericType(leftType)
1626                && Types.isNumericType(rightType)) {
1627                /*
1628                 * If one of the operands is of type byte 
1629                 * and the other is of type short, 
1630                 * then the type of the conditional expression is short:
1631                 */
1632                if (Types.isSameType(leftType, Types.byteType) &&
1633                    Types.isSameType(rightType, Types.shortType))
1634                    return Types.shortType;
1635                if (Types.isSameType(rightType, Types.byteType) &&
1636                    Types.isSameType(leftType, Types.shortType))
1637                    return Types.shortType;
1638    
1639                /*
1640                 * If one of the operands is of type T where T is byte/short/char, 
1641                 * and the other operand is a constant expression of type int
1642                 * whose value is representable in type T,
1643                 * then the type of the conditional expression is T.
1644                 */
1645                if ((Types.isSameType(leftType, Types.byteType) ||
1646                     Types.isSameType(leftType, Types.shortType) ||
1647                     Types.isSameType(leftType, Types.charType))
1648                    && ConstantExpr.
1649                    constantValueFitsIn(ConstantExpr.eval(rightExpr),
1650                                        (PrimitiveType)leftType))
1651                    return leftType;
1652                if ((Types.isSameType(rightType, Types.byteType) ||
1653                     Types.isSameType(rightType, Types.shortType) ||
1654                     Types.isSameType(rightType, Types.charType))
1655                    && ConstantExpr.
1656                    constantValueFitsIn(ConstantExpr.eval(leftExpr),
1657                                        (PrimitiveType)rightType))
1658                    return rightType;
1659    
1660    
1661                /*
1662                 * Otherwise, binary numeric promotion (5.6.2) is applied
1663                 * to the operand types, and the type of the conditional
1664                 * expression is the promoted type:
1665                 */
1666                return Types.binaryNumericPromotion(leftType, rightType);
1667            }
1668    
1669    
1670            /*
1671             * If one operands is of the null type and the other is 
1672             * a reference type, then the result type is that reference type
1673             */
1674            if (Types.isSameType(leftType, Types.nullType) &&
1675                Types.isReferenceType(rightType)) 
1676                return rightType;
1677            if (Types.isSameType(rightType, Types.nullType) &&
1678                Types.isReferenceType(leftType)) 
1679                return leftType;
1680    
1681    
1682            /*
1683             * If the second and third operands are of different reference
1684             * types, then it must be possible to convert one of the types
1685             * to the other type (call this latter type T) by assignment
1686             * conversion (5.2); the type of the conditional expression
1687             * is T. It is a compile-time error if neither type is
1688             * assignment compatible with the other type.
1689             */
1690            if (Types.isReferenceType(leftType) 
1691                && Types.isReferenceType(rightType)) {
1692                if (assignmentConvertable(leftExpr, rightType))
1693                    return rightType;
1694                if (assignmentConvertable(rightExpr, leftType))
1695                    return leftType;
1696            }
1697    
1698            // Invalid combination
1699            return null;
1700    
1701        }
1702    
1703        // ======================================================================
1704    
1705        //@ requires left != null && right != null;
1706        //@ requires loc != Location.NULL;
1707        //@ ensures \result != null  ;
1708        protected Type checkBinaryExpr(int op, Expr left, Expr right, int loc) {
1709      
1710            Type leftType = getType(left);
1711            Type rightType = getType(right);
1712    
1713            switch(op) {
1714        
1715                case TagConstants.ADD:
1716        
1717                    if(Types.isSameType(leftType, Types.javaLangString()) 
1718                        || Types.isSameType(rightType, Types.javaLangString())) {
1719          
1720                        // Operation is string concatenation
1721                        return Types.javaLangString();
1722                    }
1723                    // else fall thru
1724          
1725                case TagConstants.STAR: 
1726                case TagConstants.DIV: 
1727                case TagConstants.MOD: 
1728                case TagConstants.SUB: {
1729                    if(checkNumericType(left)
1730                        && checkNumericType(right))
1731                        return Types.binaryNumericPromotion(leftType, rightType);
1732                    else
1733                        // error recovery
1734                        return Types.intType;
1735                } 
1736    
1737                case TagConstants.LSHIFT: 
1738                case TagConstants.RSHIFT: 
1739                case TagConstants.URSHIFT:
1740          
1741                    // Arguments must be primitive integral types
1742                    // result is unary promoted type of left operand
1743          
1744                    if(checkIntegralType(left) 
1745                        && checkIntegralType(right))
1746                        return Types.unaryPromote(leftType);
1747                    else
1748                        // error recovery
1749                        return Types.intType;
1750          
1751                case TagConstants.LT: 
1752                case TagConstants.LE: 
1753                case TagConstants.GT: 
1754                case TagConstants.GE:
1755          
1756                    // Arguments must be primitive numeric types
1757                    // result is boolean
1758          
1759                    checkNumericType(left);
1760                    checkNumericType(right);
1761                    return Types.booleanType;
1762          
1763                case TagConstants.BITAND: 
1764                case TagConstants.BITOR: 
1765                case TagConstants.BITXOR: {
1766                    if(!Types.isBooleanType(leftType)) {
1767              
1768                        // Arguments are primitive integral
1769                        // binary numeric promotion is performed
1770                        // type of result is promoted type of operands
1771              
1772                        if(checkIntegralType(left)
1773                            && checkIntegralType(right))
1774                            return Types.binaryNumericPromotion(leftType, rightType);
1775                        else
1776                            // error recovery
1777                            return Types.intType;
1778                    } 
1779            
1780                    // else fall thru. Arguments must be boolean, result is boolean
1781                }
1782          
1783                case TagConstants.AND: 
1784                case TagConstants.OR: {
1785                    // Arguments must be boolean, result is also boolean
1786                    checkType(left, Types.booleanType);
1787                    checkType(right, Types.booleanType);
1788                    return Types.booleanType;
1789                }
1790          
1791                case TagConstants.EQ: 
1792                case TagConstants.NE:
1793                    if( (Types.isNumericType(leftType) 
1794                           && Types.isNumericType(rightType))
1795                          || (!Types.isVoidType(leftType)
1796                              && Types.isSameType(leftType, rightType))
1797                          || (Types.isReferenceOrNullType(leftType) 
1798                              && Types.isReferenceOrNullType(rightType))) {
1799            
1800                        if(  Types.isCastable(leftType, rightType) 
1801                              || Types.isCastable(rightType, leftType)) {
1802                            // is ok, result boolean
1803                            return Types.booleanType;
1804                        } 
1805                    }
1806          
1807                    // Fall thru to here on error
1808    
1809                    if (!Types.isErrorType(leftType) && !Types.isErrorType(rightType)) {
1810                        ErrorSet.error(loc, 
1811                                   "Invalid types ("+Types.printName(leftType)
1812                                   +" and "+Types.printName(rightType)
1813                                   +") in equality comparison");
1814                    }
1815                    return Types.booleanType;
1816          
1817                case TagConstants.ASSIGN:
1818                case TagConstants.ASGMUL: 
1819                case TagConstants.ASGDIV: 
1820                case TagConstants.ASGREM: 
1821                case TagConstants.ASGADD: 
1822                case TagConstants.ASGSUB:
1823                case TagConstants.ASGLSHIFT: 
1824                case TagConstants.ASGRSHIFT: 
1825                case TagConstants.ASGURSHIFT:
1826                case TagConstants.ASGBITAND:
1827                case TagConstants.ASGBITOR: 
1828                case TagConstants.ASGBITXOR: {
1829                    if (left instanceof VariableAccess) {
1830                        GenericVarDecl v = ((VariableAccess)left).decl;
1831                        if (Modifiers.isFinal(v.modifiers) && 
1832                            (v instanceof FormalParaDecl ||
1833                            (v instanceof LocalVarDecl &&
1834                                ((LocalVarDecl)v).init != null)
1835                            ))
1836                            ErrorSet.caution(left.getStartLoc(),
1837                                "May not assign to a final variable",
1838                                v.getStartLoc());
1839                    } else if (left instanceof FieldAccess) {
1840                        GenericVarDecl v = ((FieldAccess)left).decl;
1841                        // v is null if there was an error such as a field
1842                        // name that does not exist
1843                        if (v == Types.lengthFieldDecl) 
1844                            ErrorSet.error(left.getStartLoc(),
1845                                "May not assign to array's length field");
1846                        else if (v != null && Modifiers.isFinal(v.modifiers) &&
1847                            v instanceof FieldDecl &&
1848                            ((FieldDecl)v).init != null)
1849                            ErrorSet.caution(left.getStartLoc(),
1850                                "May not assign to a final field",
1851                                v.getStartLoc());
1852    
1853                    }
1854                        // FIXME - need checks of more complicated expressions
1855    
1856                    if(!isVariable(left)) {
1857                        if (!Types.isErrorType(leftType)) ErrorSet.error(loc,
1858                                       "Left hand side of assignment operator "+
1859                                       "is not a location");
1860                    } else if(op == TagConstants.ASSIGN) {
1861                        if(!assignmentConvertable(right, leftType) &&
1862                            !Types.isErrorType(getType(right)) && !Types.isErrorType(leftType))
1863                            ErrorSet.error(loc,
1864                                           "Value of type "+Types.printName(getType(right))
1865                                           +" cannot be assigned to location of type "
1866                                           + Types.printName(leftType));
1867                    } else {
1868                        // E1 op= E2 is equivalent to
1869                        // E1 = (T)(E1 op E2), where T is type of E1
1870                        int simpleop;
1871                        switch(op) {
1872                            case TagConstants.ASGMUL:    simpleop=TagConstants.STAR;    break;
1873                            case TagConstants.ASGDIV:    simpleop=TagConstants.DIV;     break;
1874                            case TagConstants.ASGREM:    simpleop=TagConstants.MOD;     break;
1875                            case TagConstants.ASGADD:    simpleop=TagConstants.ADD;     break;
1876                            case TagConstants.ASGSUB:    simpleop=TagConstants.SUB;     break;
1877                            case TagConstants.ASGLSHIFT: simpleop=TagConstants.LSHIFT;  break;
1878                            case TagConstants.ASGRSHIFT: simpleop=TagConstants.RSHIFT;  break;
1879                            case TagConstants.ASGURSHIFT:simpleop=TagConstants.URSHIFT; break;
1880                            case TagConstants.ASGBITAND: simpleop=TagConstants.BITAND;  break;
1881                            case TagConstants.ASGBITOR:  simpleop=TagConstants.BITOR;   break;
1882                            case TagConstants.ASGBITXOR: simpleop=TagConstants.BITXOR;  break;
1883                            default: Assert.fail("Incomplete case"); simpleop=0; // dummy init
1884                        }
1885                        Type result = checkBinaryExpr(simpleop, left, right, loc);
1886                        // Check if result is convertable to leftType
1887                        if(!Types.isCastable(result, leftType))
1888                            ErrorSet.error(loc, 
1889                                           "Result type "+Types.printName(result)
1890                                           +" of assignment operation cannot be cast to type "
1891                                           +Types.printName(leftType));
1892                    }  
1893                    // done
1894                    return leftType;
1895                }
1896    
1897                default:
1898                    Assert.fail("Fall thru, op = "+op); 
1899                    return null;
1900            }
1901        }
1902    
1903        // *********************************************************************
1904    
1905        //@ requires e != null;
1906        static boolean checkIntegralType(Expr e) {
1907            Type t = getType(e);
1908            if(Types.isIntegralType(t)) {
1909                return true;
1910            } else {
1911                if (!Types.isErrorType(t))
1912                    ErrorSet.error(e.getStartLoc(), 
1913                                "Cannot convert "+Types.printName(t)
1914                                +" to an integral type");
1915                return false;
1916            }
1917        }
1918    
1919        //@ requires e != null;
1920        static boolean checkNumericType(Expr e) {
1921            Type t = getType(e);
1922            if(!Types.isNumericType(t)) {
1923                if (!Types.isErrorType(t))
1924                    ErrorSet.error(e.getStartLoc(), 
1925                                "Cannot convert "+Types.printName(t)
1926                                +" to a numeric type ");
1927                return false;
1928            } else {
1929                return true;
1930            }    
1931        }
1932    
1933        //@ requires e != null;
1934        static boolean isVariable(Expr e) {
1935            switch(e.getTag()) {
1936                case TagConstants.ARRAYREFEXPR:
1937                case TagConstants.VARIABLEACCESS:
1938                case TagConstants.FIELDACCESS: 
1939                    return true;
1940    
1941                default:
1942                    return false;
1943            }
1944        }
1945    
1946        // ======================================================================
1947    
1948        /**
1949         * Decorates <code>VarInit</code> nodes to point to <code>Type</code> objects.
1950         */
1951        //@ private invariant typeDecoration != null;
1952        //@ private invariant typeDecoration.decorationType == \type(Type);
1953        private static ASTDecoration typeDecoration
1954            = new ASTDecoration("typeDecoration");
1955    
1956        //@ requires i != null && t != null;
1957        public static VarInit setType(VarInit i, Type t) {
1958            if (t instanceof TypeName)
1959                t = TypeSig.getSig((TypeName)t);
1960            typeDecoration.set(i, t);
1961            return i;
1962        }
1963    
1964        /**
1965         * Retrieves the <code>Type</code> of a <code>VarInit</code>.  This type is
1966         * associated with an expression by the typechecking pass. If the expression does
1967         * not have an associated type, then null is returned.
1968         */
1969        //@ requires i != null;
1970        protected static Type getTypeOrNull(VarInit i) {
1971            return (Type)typeDecoration.get(i);
1972        }
1973    
1974        /**
1975         * Retrieves the <code>Type</code> of a <code>VarInit</code>.  This type is
1976         * associated with an expression by the typechecking pass. If the expression does
1977         * not have an associated type, then <code>Assert.fail</code> is called.
1978         */
1979        //@ requires i != null;
1980        //@ ensures \result != null;
1981        public static Type getType(VarInit i) {
1982            Type t = getTypeOrNull(i);
1983            if(t==null) 
1984                Assert.fail("getType at "+i.getTag()+" "+
1985                            PrettyPrint.inst.toString(i) +
1986                            Location.toString(i.getStartLoc()));
1987            return t;
1988        }
1989    
1990    
1991        // ======================================================================
1992    
1993        /**
1994         * Decorates <code>BranchStmt</code> nodes to point to labelled <code>Stmt</code>
1995         * objects.
1996         */
1997        //@ private invariant branchDecoration != null;
1998        //@ private invariant branchDecoration.decorationType == \type(Stmt);
1999        private static ASTDecoration branchDecoration
2000            = new ASTDecoration("branchDecoration");
2001    
2002        //@ requires s != null && l != null;
2003        private static void setBranchLabel(BranchStmt s, Stmt l) {
2004            Assert.notFalse(branchDecoration.get(s) == null);       //@ nowarn Pre;
2005            branchDecoration.set(s,l);
2006        }
2007    
2008        /**
2009         * Retrieves the <code>Stmt</code> target of a <code>BranchStmt</code>.  This
2010         * <code>Stmt</code> may be mentioned either explicitly (as in <code>break
2011         * label;</code>), or implicitly (as in <code>break;</code>) by the
2012         * <code>BranchStmt</code>.  The correct <code>Stmt</code> target is associated
2013         * with the <code>BranchStmt</code> by the typechecking pass. This type is
2014         * associated with an expression by the typechecking pass. If the
2015         * <code>BranchStmt</code> does not have an associated <code>Stmt</code> target,
2016         * then <code>Assert.fail</code> is called.
2017         */
2018        //@ requires s != null;
2019        static Stmt getBranchLabel(BranchStmt s) {
2020            Stmt l = (Stmt)branchDecoration.get(s);
2021            if(l==null)
2022                Assert.fail("getBranchLabel failed at "+s.getTag());
2023            return l;
2024        }
2025    
2026        // ======================================================================
2027    
2028        //@ requires expr != null && t != null;
2029        static void checkType(Expr expr, Type t) {
2030            if(!inst.assignmentConvertable(expr, t)) {
2031                if (!Types.isErrorType(getType(expr)))
2032                    ErrorSet.error(expr.getStartLoc(), 
2033                                "Cannot convert "+Types.printName(getType(expr))
2034                                +" to "+Types.printName(t));
2035            }
2036        
2037        }
2038    
2039        //@ requires e != null && s != null && t != null;
2040        //@ requires loc != Location.NULL;
2041        protected static void reportLookupException(LookupException e, 
2042                                                    String s, 
2043                                                    String t, 
2044                                                    int loc) {
2045            switch(e.reason) {
2046                case LookupException.NOTFOUND:
2047                    ErrorSet.error(loc, "No such "+s+" in type "+t);
2048                    break;
2049                case LookupException.AMBIGUOUS:
2050                    ErrorSet.error(loc, "Ambiguous "+s+" for type "+t);
2051                    break;
2052                case LookupException.BADTYPECOMBO:
2053                    ErrorSet.error(loc, "No "+s+" matching given argument types");
2054                    break;
2055                case LookupException.NOTACCESSIBLE:
2056                    ErrorSet.error(loc, "Cannot access this "+s);
2057                    break;
2058                default:
2059                    Assert.fail("Bad lookup exception: "+e.reason);
2060            }
2061        }
2062    
2063        /**
2064         * Checks if Exp e can be assigned to Type t.  This method is here instead of in
2065         * {@link javafe.tc.Types}, because it needs to mess with constants.
2066         */ 
2067        //@ requires e != null && t != null;
2068        protected boolean assignmentConvertable(Expr e, Type t) {
2069    
2070            Type te = getType(e);
2071    
2072            if(Types.isInvocationConvertable(te, t))
2073                return true;
2074    
2075            // Check if t is byte/short/char, 
2076            // and e a constant expression whose value fits in t.
2077    
2078            switch(t.getTag()) {
2079                case TagConstants.BYTETYPE:
2080                case TagConstants.SHORTTYPE:
2081                case TagConstants.CHARTYPE:
2082                    Object val = ConstantExpr.eval(e);
2083                    if(val != null &&
2084                       ConstantExpr.constantValueFitsIn(val, (PrimitiveType)t))
2085                        return true;
2086                    else return false;
2087                default:
2088                    return false;
2089            }
2090        }
2091    
2092        // ======================================================================
2093    
2094        //@ requires e != null;
2095        protected void checkTypeDeclElemPragma(TypeDeclElemPragma e) {
2096            Assert.fail("Unexpected TypeDeclElemPragma");
2097        }
2098    
2099        /**
2100         * Hook to do additional processing on <code>ModifierVec</code>s.  The
2101         * <code>ASTNode</code> is the parent of the <code>ModifierPragma</code>, and
2102         * <code>env</code> is the current environment.
2103         */
2104        //@ requires env != null;
2105        protected Env checkModifierPragmaVec(ModifierPragmaVec v, 
2106                                             ASTNode ctxt, 
2107                                             Env env) {
2108            if (v != null)
2109              for(int i = 0; i < v.size(); i++) {
2110                env = checkModifierPragma(v.elementAt(i), ctxt, env);
2111                  }
2112              return env;
2113        }
2114    
2115        /**
2116         * Hook to do additional processing on <code>Modifier</code>s.  The
2117         * <code>ASTNode</code> is the parent of the <code>ModifierPragma</code>, and
2118         * <code>env</code> is the current environment.
2119         * @return true if pragma should be deleted
2120         */
2121        //@ requires p != null && env != null;
2122        protected Env checkModifierPragma(ModifierPragma p, ASTNode ctxt, Env env) {
2123            // Assert.fail("Unexpected ModifierPragma");
2124            return env;
2125        }
2126    
2127        //@ requires e != null && s != null;
2128        protected Env checkStmtPragma(Env e, StmtPragma s) {
2129            Assert.fail("Unexpected StmtPragma");
2130            return e;
2131        }
2132    
2133        //@ requires env != null;
2134        protected Env checkTypeModifierPragmaVec(TypeModifierPragmaVec v, 
2135                                                  ASTNode ctxt, 
2136                                                  Env env) {
2137            if(v != null)
2138                for(int i=0; i<v.size(); i++)
2139                    env = checkTypeModifierPragma(v.elementAt(i), ctxt, env);
2140            return env;
2141        }
2142        
2143        //@ requires p != null && env != null;
2144        protected Env checkTypeModifierPragma(TypeModifierPragma p,
2145                                               ASTNode ctxt,
2146                                               Env env) {
2147            Assert.fail("Unexpected TypeModifierPragma");
2148            return env;
2149        }
2150    
2151        /**
2152         * This may be called more than once on a Type t.
2153         */
2154        //@ requires t != null;
2155        protected Env checkTypeModifiers(Env env, Type t) {
2156            // don't know context for type, so pull it out of the type's decorations.
2157            if (env == null) {
2158                env = (Env)Env.typeEnv.get(t);
2159            }       
2160            Assert.notFalse(env != null);  //@ nowarn Pre;
2161            checkTypeModifierPragmaVec(t.tmodifiers, t, env);
2162            if (t instanceof ArrayType) {
2163                env = checkTypeModifiers(env, ((ArrayType)t).elemType);
2164            }
2165            return env;
2166        }
2167    
2168    }
2169    
2170    /*
2171     * Local Variables:
2172     * Mode: Java
2173     * fill-column: 85
2174     * End:
2175     */