001    // $Id: FlowInsensitiveChecks.java,v 1.42 2006/09/25 15:13:29 chalin Exp $
002    /* Copyright 2000, 2001, Compaq Computer Corporation */
003    
004    package javafe.tc;
005    
006    import java.util.HashSet;
007    import java.util.Set;
008    
009    import javafe.ast.ASTDecoration;
010    import javafe.ast.ASTNode;
011    import javafe.ast.AmbiguousMethodInvocation;
012    import javafe.ast.AmbiguousVariableAccess;
013    import javafe.ast.ArrayInit;
014    import javafe.ast.ArrayRefExpr;
015    import javafe.ast.ArrayType;
016    import javafe.ast.AssertStmt;
017    import javafe.ast.BinaryExpr;
018    import javafe.ast.BranchStmt;
019    import javafe.ast.CastExpr;
020    import javafe.ast.CatchClause;
021    import javafe.ast.ClassDecl;
022    import javafe.ast.ClassDeclStmt;
023    import javafe.ast.ClassLiteral;
024    import javafe.ast.CondExpr;
025    import javafe.ast.ConstructorDecl;
026    import javafe.ast.ConstructorInvocation;
027    import javafe.ast.DoStmt;
028    import javafe.ast.EvalStmt;
029    import javafe.ast.Expr;
030    import javafe.ast.ExprObjectDesignator;
031    import javafe.ast.ExprVec;
032    import javafe.ast.FieldAccess;
033    import javafe.ast.FieldDecl;
034    import javafe.ast.ForStmt;
035    import javafe.ast.FormalParaDecl;
036    import javafe.ast.GenericBlockStmt;
037    import javafe.ast.GenericVarDecl;
038    import javafe.ast.Identifier;
039    import javafe.ast.IfStmt;
040    import javafe.ast.InitBlock;
041    import javafe.ast.InstanceOfExpr;
042    import javafe.ast.InterfaceDecl;
043    import javafe.ast.LabelStmt;
044    import javafe.ast.LocalVarDecl;
045    import javafe.ast.MethodDecl;
046    import javafe.ast.MethodInvocation;
047    import javafe.ast.ModifierPragma;
048    import javafe.ast.ModifierPragmaVec;
049    import javafe.ast.Modifiers;
050    import javafe.ast.Name;
051    import javafe.ast.NewArrayExpr;
052    import javafe.ast.NewInstanceExpr;
053    import javafe.ast.ObjectDesignator;
054    import javafe.ast.ParenExpr;
055    import javafe.ast.PrettyPrint;
056    import javafe.ast.PrimitiveType;
057    import javafe.ast.ReturnStmt;
058    import javafe.ast.RoutineDecl;
059    import javafe.ast.SkipStmt;
060    import javafe.ast.Stmt;
061    import javafe.ast.StmtPragma;
062    import javafe.ast.StmtVec;
063    import javafe.ast.SuperObjectDesignator;
064    import javafe.ast.SwitchLabel;
065    import javafe.ast.SwitchStmt;
066    import javafe.ast.SynchronizeStmt;
067    import javafe.ast.ThisExpr;
068    import javafe.ast.ThrowStmt;
069    import javafe.ast.TryCatchStmt;
070    import javafe.ast.TryFinallyStmt;
071    import javafe.ast.Type;
072    import javafe.ast.TypeDecl;
073    import javafe.ast.TypeDeclElem;
074    import javafe.ast.TypeDeclElemPragma;
075    import javafe.ast.TypeModifierPragma;
076    import javafe.ast.TypeModifierPragmaVec;
077    import javafe.ast.TypeName;
078    import javafe.ast.TypeObjectDesignator;
079    import javafe.ast.UnaryExpr;
080    import javafe.ast.VarDeclStmt;
081    import javafe.ast.VarInit;
082    import javafe.ast.VariableAccess;
083    import javafe.ast.WhileStmt;
084    import javafe.parser.ParseUtil;
085    import javafe.util.Assert;
086    import javafe.util.ErrorSet;
087    import javafe.util.Location;
088    
089    /**
090     * Does disambiguation and flow insensitive checks on a type
091     * declaration.
092     */
093    // TODO: Universes should be implemented by subclassing (rgrig).
094    public class FlowInsensitiveChecks
095    {
096        static public FlowInsensitiveChecks inst = new FlowInsensitiveChecks();
097        static public FlowInsensitiveChecks inst() { return inst; }
098    
099        /**
100         * Controls whether or not implicit super-calls in constructors
101         * are made explicit.  By default they are.
102         */
103        public static boolean dontAddImplicitConstructorInvocations = false;
104    
105        //alx: fields introduced by dw
106        protected boolean useUniverses=false;
107        boolean readonlyStdForPureCtor=false;
108        boolean inPure=false;
109        boolean inCtor=false;
110        boolean inStatic=false;
111        int universeReturnType = 0;
112        int universeElementReturnType = 0;
113        //alx-end
114    
115        // Use this to get an instance in order to get proper derived behavior.
116        protected FlowInsensitiveChecks() { 
117            //alx: dw init useUniverses
118            useUniverses=javafe.Tool.options!=null && 
119                         javafe.Tool.options.useUniverseTypeSystem && 
120                         javafe.Tool.options.universeLevel%5!=0;
121            readonlyStdForPureCtor=javafe.Tool.options!=null && 
122                         javafe.Tool.options.useUniverseTypeSystem && 
123                         javafe.Tool.options.universeLevel%7==0;
124        }
125    
126        /**
127         * Factory method so subclasses can override.
128         */
129        //@ requires s != null;
130        //@ ensures \result != null;
131        protected EnvForTypeSig makeEnvForTypeSig(TypeSig s,
132                                                  boolean staticContext) {
133            return s.getEnv(staticContext);
134        }
135    
136    
137        ///////////////////////////////////////////////////////////////////////
138        //                                                                   //
139        // Information that remains the same during processing of entire     //
140        // type decl.                                                        //
141        //                                                                   //
142        ///////////////////////////////////////////////////////////////////////
143    
144        //@ invariant sig != null ==> rootIEnv != null && rootSEnv != null;
145        /*@ spec_public */ protected TypeSig sig;
146    
147        // Inv: rootIEnv.peer == sig; !rootIEnv.staticContext
148        /*@ spec_public */ protected EnvForTypeSig rootIEnv;
149    
150        // Inv: rootIEnv.peer == sig; !rootIEnv.staticContext
151        /*@ spec_public */ protected EnvForTypeSig rootSEnv;
152      
153    
154        ///////////////////////////////////////////////////////////////////////
155        //                                                                   //
156        // Information that changes for the processing of each member of     //
157        // the decl.                                                         //
158        //                                                                   //
159        ///////////////////////////////////////////////////////////////////////
160      
161        //* Cannot access fields defined later? 
162        protected boolean leftToRight;
163    
164        //* Type for return statements. 
165        protected Type returnType;
166      
167    
168        ///////////////////////////////////////////////////////////////////////
169        // Information that changes within a member in a stack-like          //
170        // manner.                                                           //
171        ///////////////////////////////////////////////////////////////////////
172      
173        //@ invariant allowedExceptions != null;
174        protected TypeSigVec allowedExceptions = TypeSigVec.make();
175    
176        //@ invariant enclosingLabels != null;
177        protected StmtVec enclosingLabels = StmtVec.make();
178    
179        // -------------------------------------------------------------
180        /**
181         * Moves <code>s</code> into implementation checked state.
182         *
183         */
184        //@ requires (* <code>s</code> is in prepped state.*);
185        //@ requires s.state >= TypeSig.PREPPED;
186        public void checkTypeDeclaration(/*@ non_null @*/ TypeSig s) {
187            Assert.precondition(s.state >= TypeSig.PREPPED);
188    
189            // Set up variables for entire traversal:
190            rootSEnv = makeEnvForTypeSig(s, true);
191            rootIEnv = makeEnvForTypeSig(s, false);
192            sig = s;
193    
194            TypeDecl d = s.getTypeDecl();
195    
196            // Process each member declaration
197            for(int i = 0, sz = d.elems.size(); i < sz; i++) {
198                TypeDeclElem e = d.elems.elementAt(i);
199                checkTypeDeclElem(e);
200            }
201    
202            // Process ModifierPragmas
203            checkModifierPragmaVec(d.pmodifiers, d, rootSEnv);
204    
205            sig = null;
206        }
207    
208        // -------------------------------------------------------------
209    
210        /**
211         * Moves <code>fd</code> into implementation checked state.
212         *
213         */
214        //@ requires (* <code>fd</code> is in prepped state. *);
215        //@ modifies sig, rootSEnv, rootIEnv;
216        public void checkFieldDecl(/*@ non_null @*/ FieldDecl fd) {
217            /*
218             * Special case for free-floating fields like length.
219             *
220             * Such fields must not have any modifier pragmas or an initializer.
221             */
222            if (fd.parent==null) {
223                Assert.notFalse(fd.pmodifiers == null,   //@ nowarn Pre;
224                                "Free-floating FieldDecls may not have any ModifierPragmas");
225                Assert.notFalse(fd.init == null,         //@ nowarn Pre;
226                                "Free-floating FieldDecls may not have initializers");
227    
228                return;         // No other works needs to be done
229            }
230    
231    
232            TypeSig sig = TypeSig.getSig(fd.parent);
233            if (sig.state < TypeSig.CHECKED) {
234                // Type check this decl
235            
236                // Info.out("[Pre-checking "+Types.printName(sig)+"."+fd.id+"]");
237                sig.prep();
238    
239                // Set up variables for entire traversal
240                rootSEnv = makeEnvForTypeSig(sig, true);
241                rootIEnv = makeEnvForTypeSig(sig, false);
242                this.sig = sig;
243    
244                checkTypeDeclElem(fd);
245            }
246            this.sig = null;
247        }
248    
249        /**
250         * Tests if universe modifiers of <code>r</code> can be 
251         * assigned to <code>l</code>.
252         *
253         */
254        //alx: dw test if universe modifiers of r can be assigned to l
255        //TODO: check if the specs are enough
256        public static void checkUniverseAssignability(/*@ non_null @*/ ASTNode l, 
257                                                      /*@ non_null @*/ ASTNode r) {
258            if (!universeIsSubtypeOf(ParseUtil.getUniverse(r),
259                                     ParseUtil.getUniverse(l)))
260                ErrorSet.error(r.getStartLoc(),
261                    "cannot assign "+
262                    TagConstants.toString(ParseUtil.getUniverse(r))+
263                    " to "+
264                    TagConstants.toString(ParseUtil.getUniverse(l)));
265            else if (!universeIsSubtypeOf(ParseUtil.getElementUniverse(r),
266                                          ParseUtil.getElementUniverse(l)))
267                ErrorSet.error(r.getStartLoc(),
268                    "cannot assign "+
269                    TagConstants.toString(ParseUtil.getUniverse(r))+
270                    " "+
271                    TagConstants.toString(ParseUtil.getElementUniverse(r))+
272                    " to "+
273                    TagConstants.toString(ParseUtil.getUniverse(l))+
274                    " "+
275                    TagConstants.toString(ParseUtil.getElementUniverse(l)));
276        }
277        //alx-end
278    
279        /**
280         * Tests if the cast of the universe modifiers <code>l</code>  
281         * <code>r</code> is ever possible.
282         *
283         */
284        //alx: dw test if cast of universe modifier of l and r is ever possible
285        //TODO: check if the specs are enough
286        public static void checkUniverseCastability(/*@ non_null @*/ ASTNode l, 
287                                                    /*@ non_null @*/ ASTNode r) {
288            if (!universeIsSubtypeOf(ParseUtil.getUniverse(r),
289                                     ParseUtil.getUniverse(l)) && 
290                !universeIsSubtypeOf(ParseUtil.getUniverse(l),
291                                     ParseUtil.getUniverse(r)))
292                ErrorSet.error(r.getStartLoc(),
293                               "A "+
294                               TagConstants.toString(ParseUtil.getUniverse(r))+
295                               " instance can never be of universe type "+
296                               TagConstants.toString(ParseUtil.getUniverse(l)));
297            else if (!universeIsSubtypeOf(ParseUtil.getElementUniverse(r),
298                                          ParseUtil.getElementUniverse(l)) && 
299                     !universeIsSubtypeOf(ParseUtil.getElementUniverse(l),
300                                          ParseUtil.getElementUniverse(r)))
301                ErrorSet.error(r.getStartLoc(),
302                               "A "+
303                               TagConstants.toString(ParseUtil.getUniverse(r))+
304                               " "+
305                               TagConstants.toString(ParseUtil.getElementUniverse(r))+
306                               " instance can never be of universe type "+
307                               TagConstants.toString(ParseUtil.getUniverse(l))+
308                               " "+
309                               TagConstants.toString(ParseUtil.getElementUniverse(l)));
310        }
311        //alx-end
312    
313    
314        //alx: dw test if universe modifiers of sub is subtype of them of sup
315        //TODO: chceck how this method is used, add specs
316        /**
317         * Tests if the universe modifier <code>sub</code> is a subtype of 
318         * the universe modifier <code>sup</code>.
319         *
320         */
321        public static boolean universeIsSubtypeOf(int sub, int sup){
322            if (sub==TagConstants.NULLLIT || sub==0 || sup==0)
323                return true;
324            if (sub==TagConstants.THISEXPR || sub==TagConstants.IMPL_PEER)
325                sub=TagConstants.PEER;
326            if (sup==TagConstants.THISEXPR || sup==TagConstants.IMPL_PEER)
327                sup=TagConstants.PEER;
328            return (sup==sub || sup==TagConstants.READONLY); 
329        }
330        //alx-end    
331    
332        //------------------------------------------------------------
333    
334        // @note e must already have been prepped!
335        //@ requires e != null && sig != null;
336        //@ requires sig.state >= TypeSig.PREPPED;
337        protected void checkTypeDeclElem(TypeDeclElem e) {
338    
339            Assert.notNull(sig);
340            Assert.notFalse(sig.state >= TypeSig.PREPPED);
341            TypeDecl d = sig.getTypeDecl();
342            boolean specOnly = d.specOnly;
343    
344            switch (e.getTag()) {
345            
346                case TagConstants.FIELDDECL: {              
347                    FieldDecl fd = (FieldDecl)e;
348    
349                    // Process ModifierPragmas
350                    Env rootEnv = Modifiers.isStatic(fd.modifiers) ? rootSEnv : rootIEnv;
351                    checkModifierPragmaVec(fd.pmodifiers, fd, rootEnv);
352                    checkTypeModifiers(rootEnv, fd.type);
353    
354                    //alx: dw check the universe annotations
355                    if (useUniverses) 
356                        checkUniverseForField(fd);
357    
358                    // Resolve the initializer of a field decl
359                    if (fd.init != null) {
360                        leftToRight = true;
361                        allowedExceptions.removeAllElements();
362                        Assert.notFalse(allowedExceptions.size() == 0);
363                        fd.init = checkInit(rootEnv, fd.init, fd.type);
364                        //alx: dw check the universe annotations
365                        if (useUniverses) {
366                            //Array-initializers don't know their universe type, 
367                            //we have to take it form the field declaration
368                            if (ParseUtil.getUniverse(fd.init)==0 && 
369                                ParseUtil.getElementUniverse(fd.init)!=0)
370                                ParseUtil.setUniverse(fd.init, 
371                                                      ParseUtil.getUniverse(fd));
372                            checkUniverseAssignability(fd, fd.init);
373                        }
374                        //alx-end
375                    }
376                    else if (Modifiers.isFinal(fd.modifiers) && 
377                             Modifiers.isStatic(fd.modifiers) && 
378                             Modifiers.isPublic(fd.modifiers) && !specOnly) {
379                        
380                        String msg = ("Variable " + fd.id
381                                      + " might not have been initialized");
382                        ErrorSet.caution(fd.locId, msg); 
383                    }
384                    break;
385                }
386            
387                case TagConstants.METHODDECL:
388                case TagConstants.CONSTRUCTORDECL: {
389                    RoutineDecl rd = (RoutineDecl) e;
390                    Env rootEnv = Modifiers.isStatic(rd.modifiers)
391                        ? rootSEnv : rootIEnv;
392              
393                    //alx: dw remember if we are in a static or pure context
394                    inStatic=Modifiers.isStatic(rd.modifiers);
395                    inPure=isPure(rd);
396                    //alx-end
397    
398                    // First do method/constructor specific stuff
399                    if(rd instanceof MethodDecl) {
400                
401                        MethodDecl md = (MethodDecl) e;
402    
403                        checkTypeModifiers(rootEnv, md.returnType);
404                  
405                        returnType = md.returnType;
406    
407                        //alx:dw check that return type is not rep in a 
408                        //    static context and remember universe type of 
409                        //    the return value
410                        if (useUniverses) {
411                                checkNoRepInStaticContext(md);
412                                if (ParseUtil.getUniverse(md)!=0) {
413                                universeReturnType = ParseUtil.getUniverse(md);
414                                if (ParseUtil.getElementUniverse(md)!=0)
415                                    universeElementReturnType = 
416                                        ParseUtil.getElementUniverse(md);
417                                }
418                        }
419                        //alx-end
420    
421                        if (md.body != null && !specOnly) {
422                  
423                            if(Modifiers.isAbstract(md.modifiers))
424                                ErrorSet.error(md.loc, 
425                                               "An abstract method cannot include a body");
426                            if(Modifiers.isNative(md.modifiers))
427                                ErrorSet.error(md.loc, 
428                                               "A native method cannot include a body");
429                        } else {
430    /* We allow any method to have no body -- DRCok
431                            if(!Modifiers.isAbstract(md.modifiers)
432                               && !Modifiers.isNative(md.modifiers) && !specOnly)
433                                ErrorSet.error(md.loc, 
434                                               "Method must include a body unless "
435                                               +"it is declared abstract or native");
436    */
437                        }
438                    } else {
439                        // Constructor
440                        ConstructorDecl cd = (ConstructorDecl)rd;
441    
442                        //alx:dw remember if in constructor
443                        inCtor=true;
444                        //alx-end
445    
446                        // Was checked in parser
447                        Assert.notFalse(!(d instanceof InterfaceDecl)); //@ nowarn Pre;
448    
449                        // Modifiers were checked when we prep'ed the constructed
450                        returnType = Types.voidType;
451    
452                        // Check if we need to add an implicit constructor invocation
453                        //@ assume !specOnly ==> cd.body != null;
454                        if(!dontAddImplicitConstructorInvocations && !specOnly &&
455                            cd.body != null && // FIXME - we've broken the assumption above by allowing spec files - need to fix that uniformly
456                            !(cd.body.stmts.size() > 0
457                              && cd.body.stmts.elementAt(0) instanceof 
458                              ConstructorInvocation)) {
459                            // no explicit constructor invocation
460                            if(sig != Types.javaLangObject()) {
461                                // add implicit constructor invocation
462    
463                                ExprVec args = ExprVec.make();
464                                ConstructorInvocation ci 
465                                    = ConstructorInvocation.make(true, null, Location.NULL,
466                                                                 cd.body.locOpenBrace,
467                                                                 cd.body.locOpenBrace, args);
468                                cd.body.stmts.insertElementAt(ci, 0);
469                            }
470                        }
471                    }
472    
473                    // Now do stuff common to methods and constructors.
474    
475                    leftToRight = false;
476                    enclosingLabels.removeAllElements();
477              
478                    allowedExceptions.removeAllElements();
479                    for(int j=0; j<rd.raises.size(); j++) {
480                        TypeName n = rd.raises.elementAt(j);
481                        rootEnv.resolveType(sig,n);
482                        checkTypeModifiers(rootEnv, n);
483                        allowedExceptions.addElement(TypeSig.getSig(n));
484                    }
485    
486                    Env env = new EnvForEnclosedScope(rootEnv);
487                    for(int j = 0; j < rd.args.size(); j++) {
488                        FormalParaDecl formal = rd.args.elementAt(j);
489                        PrepTypeDeclaration.inst.
490                            checkModifiers(formal.modifiers, Modifiers.ACC_FINAL, 
491                                           formal.getStartLoc(), "formal parameter");
492                        checkModifierPragmaVec(formal.pmodifiers, formal, rootEnv);
493    
494                        env = new EnvForLocals(env, formal);
495                        checkTypeModifiers(env, formal.type);
496                        //alx: dw test universe types of arguments
497                        if (useUniverses) {
498                                int tag=ParseUtil.getUniverse(formal);
499                                if (tag!=0) { //is not a primitive type
500                                if (inCtor && tag==TagConstants.REP)
501                                    ErrorSet.error(formal.getStartLoc(),
502                                       "rep not allowed in constructor signature");
503                                else if (!inCtor && inPure) {
504                                    if (tag!=TagConstants.IMPL_PEER && 
505                                        tag!=TagConstants.READONLY)
506                                        ErrorSet.error(formal.getStartLoc(),
507                                                   "arguments of pure methods"+
508                                                   " must have readonly "+
509                                                   "universe type");
510                                    ParseUtil.setUniverse(formal,
511                                                      TagConstants.READONLY);
512                                } else if (inCtor && 
513                                           inPure && 
514                                           readonlyStdForPureCtor && 
515                                           tag==TagConstants.IMPL_PEER) {
516                                    ParseUtil.setUniverse(formal,
517                                                          TagConstants.READONLY);
518                                } else {
519                                    checkNoRepInStaticContext(formal);
520                                }
521                                }
522                        }
523                        //alx-end
524                    }
525    
526                    // Process ModifierPragmas
527                    checkModifierPragmaVec(rd.pmodifiers, rd, env);
528              
529                    if (rd.body != null) {
530                        checkStmt(env, rd.body);
531                    }
532    
533                    break;
534                }
535            
536                case TagConstants.INITBLOCK: {
537                    InitBlock si = (InitBlock) e;
538                    PrepTypeDeclaration.inst.
539                        checkModifiers(si.modifiers, Modifiers.ACC_STATIC, 
540                                       si.getStartLoc(), "initializer body");
541                    Env rootEnv = Modifiers.isStatic(si.modifiers) ? rootSEnv : rootIEnv;
542                    returnType = null;
543                    checkStmt(new EnvForEnclosedScope(rootEnv), si.block);
544                    //alx:dw remember if in static context
545                    if (useUniverses)
546                        inStatic = Modifiers.isStatic(si.modifiers);
547                    //alx-end
548                    break;
549                }
550            
551                case TagConstants.CLASSDECL:
552                case TagConstants.INTERFACEDECL: {
553                    TypeSig.getSig((TypeDecl)e).typecheck();
554                    break;
555                }
556    
557                default:
558                    if(e instanceof TypeDeclElemPragma)
559                        checkTypeDeclElemPragma((TypeDeclElemPragma)e);
560                    else
561                        Assert.fail("Switch fall-through (" + e.getTag() + ")");
562            }
563            //alx:dw reset for the next TypeDeclElem
564            inPure=false;
565            inCtor=false;
566            inStatic=false;
567            universeReturnType = 0;
568            universeElementReturnType = 0;
569            //alx-end
570        }
571        
572        // === Typecheck statements : begin ===
573    
574        protected Env checkVarDeclStmt(Env e, LocalVarDecl s) {
575            e.resolveType(sig, s.type);
576            checkTypeModifiers(e, s.type);
577            PrepTypeDeclaration.inst.checkModifiers(
578                s.modifiers, 
579                Modifiers.ACC_FINAL,
580                s.locId, 
581                "local variable");
582            checkModifierPragmaVec(s.pmodifiers, s, e);
583    
584            Env newEnv = new EnvForLocals(e, s);
585            if (s.init != null) {
586                s.init = checkInit(newEnv, s.init, s.type);
587                //alx: dw set the universe type for array inits and test it
588                if (useUniverses) {
589                        if (ParseUtil.getUniverse(s.init) == 0 
590                            &&  ParseUtil.getElementUniverse(s.init)!=0) {
591                            ParseUtil.setUniverse(s.init, 
592                                ParseUtil.getUniverse(s));
593                        }
594                        checkUniverseAssignability(s, s.init);
595                }
596                //alx-end
597            }
598            //alx: dw test if the given universe modifier is allowed 
599            //   for this context
600            if (useUniverses) {
601                checkNoRepInStaticContext(s);
602            }
603            //alx-end
604            return newEnv;
605        }
606        
607        protected Env checkClassDeclStmt(Env e, ClassDeclStmt s) {
608            // TODO: Check this!
609            Env newEnv = new EnvForLocalType(e, s.decl);
610            TypeSig T = Types.makeTypeSig(s.decl.id.toString(), newEnv, s.decl);
611            T.typecheck();
612            return newEnv;
613        }
614        
615        protected Env checkSwitchStmt(Env e, SwitchStmt s) {
616            s.expr = checkExpr(e, s.expr);
617            Env env = e;
618    
619            // Now do special handling of the following block with case stmts
620            Type switchType = getType(s.expr);
621            if (!Types.isIntegralType(switchType) || Types.isLongType(switchType)) {
622                ErrorSet.error(
623                    s.expr.getStartLoc(),
624                    "The type of a switch expression must be char,"
625                        + " byte, short, or int.");
626                switchType = Types.intType;
627            }
628    
629            // What case values encountered so far.
630            java.util.Set switchValues = new HashSet();
631    
632            boolean defaultEncountered = false;
633            enclosingLabels.addElement(s);
634    
635            for (int i = 0, sz = s.stmts.size(); i < sz; i++) {
636                Stmt stmt = s.stmts.elementAt(i);
637    
638                if (stmt.getTag() == TagConstants.SWITCHLABEL) {
639                    SwitchLabel x = (SwitchLabel)stmt;
640                    if (x.expr != null) {
641                        x.expr = checkExpr(env, x.expr);
642                        Object val = ConstantExpr.eval(x.expr);
643                        // System.out.println("At
644                        // "+Location.toString(x.expr.getStartLoc()));
645    
646                        if (val == null)
647                            ErrorSet.error(
648                                x.loc,
649                                "Non-constant value in switch label");
650                        else if (!ConstantExpr.constantValueFitsIn(
651                            val,
652                            (PrimitiveType)switchType))
653                            ErrorSet.error(x.loc, "Case label value (" + val
654                                + ") not assignable to "
655                                + "the switch expression type "
656                                + Types.printName(switchType));
657                        else {
658                            // Check if it is a duplicate
659                            // val may be Integer or Long, convert to Long for
660                            // duplicate checking
661                            Assert.notFalse(val instanceof Long // @ nowarn Pre;
662                                || val instanceof Integer);
663                            Long valLong = new Long(
664                                ConstantExpr.getLongConstant(val));
665                            if (switchValues.contains(valLong)) {
666                                // Point to dup label - FIXME
667                                ErrorSet.error(x.loc, "Duplicate case label " + val
668                                    + " in switch statement");
669                            } else {
670                                switchValues.add(valLong);
671                            }
672                        }
673                    } else {
674                        // this is default
675                        if (defaultEncountered)
676                            // Point to dup label - FIXME
677                            ErrorSet.error(
678                                x.loc,
679                                "Duplicate default label in switch statement");
680                        else
681                            defaultEncountered = true;
682                    }
683    
684                } else
685                    env = checkStmt(env, stmt);
686            }
687    
688            enclosingLabels.pop();
689            return e;
690        }
691    
692        /**
693         * Typecheck a statement in a given environment then return the environment
694         * in effect for statements that follow the given statement.
695         * <p>
696         * (The returned environment will be the same as the one passed in unless
697         * the statement is a declaration.)
698         * </p>
699         */
700        // @ requires e != null && s != null;
701        // @ requires !(e instanceof EnvForCU);
702        // @ requires sig != null;
703        // @ ensures \result != null;
704        // @ ensures !(\result instanceof EnvForCU);
705        protected Env checkStmt(Env e, Stmt s) {
706    
707            switch (s.getTag()) {
708            // === Handle declarations ===
709            case TagConstants.VARDECLSTMT:
710                return checkVarDeclStmt(e, ((VarDeclStmt)s).decl);
711            case TagConstants.CLASSDECLSTMT:
712                return checkClassDeclStmt(e, (ClassDeclStmt)s);
713    
714            // === Handle `switch' and related statements ===
715            // NOTE: The block following `switch' is also handled.
716            case TagConstants.SWITCHLABEL:
717                Assert.precondition("Switch label passed to checkStmt!");
718            case TagConstants.SWITCHSTMT:
719                return checkSwitchStmt(e, (SwitchStmt)s);
720    
721            // === Handle the rest of the statements ===
722            case TagConstants.BREAKSTMT:
723            case TagConstants.CONTINUESTMT: {
724                BranchStmt bs = (BranchStmt)s;
725                Stmt dest = null;
726                int size = enclosingLabels.size();
727    
728                String expectedStmtKind = s.getTag() == TagConstants.BREAKSTMT ? "switch, while, do, or for"
729                    : "while, do or for";
730    
731                for (int i = size - 1; i >= 0 && dest == null; i--) {
732                    Stmt ati = enclosingLabels.elementAt(i);
733                    Stmt target = ati instanceof LabelStmt ? ((LabelStmt)ati).stmt
734                        : ati;
735    
736                    // continue target must be a loop statement
737                    // unlabelled break target must be a loop or switch
738                    // labelled break can be any statement
739    
740                    boolean loopTarget = (target instanceof ForStmt)
741                        || (target instanceof WhileStmt)
742                        || (target instanceof DoStmt);
743    
744                    boolean validTarget = loopTarget
745                        || (s.getTag() == TagConstants.BREAKSTMT && (target instanceof SwitchStmt || bs.label != null));
746    
747                    if (bs.label == null) {
748                        if (validTarget)
749                            dest = target;
750                        else
751                            continue;
752                    } else if (ati instanceof LabelStmt
753                        && ((LabelStmt)ati).label == bs.label) {
754                        if (!validTarget)
755                            ErrorSet.caution(
756                                bs.loc,
757                                "Enclosing statement labelled '" + bs.label
758                                    + "' is not a " + expectedStmtKind
759                                    + " statement");
760                        // just give a warning and continue, since javac accepts
761                        // this
762                        dest = target;
763                    }
764                    // else continue
765                }
766    
767                if (dest == null) {
768                    ErrorSet.error(
769                        bs.loc,
770                        bs.label == null ? "No enclosing unlabelled "
771                            + expectedStmtKind + " statement" : "No enclosing "
772                            + expectedStmtKind + " statement labelled '" + bs.label
773                            + "'");
774                } else
775                    setBranchLabel(bs, dest);
776    
777                return e;
778            }
779    
780            case TagConstants.SKIPSTMT:
781                return e;
782    
783            case TagConstants.RETURNSTMT: {
784                ReturnStmt rs = (ReturnStmt)s;
785    
786                if (rs.expr != null) rs.expr = checkExpr(e, rs.expr);
787    
788                if (returnType == null)
789                    ErrorSet.error(
790                        rs.loc,
791                        "Returns are not allowed in a static initializer");
792                else {
793                    if (rs.expr != null) {
794                        Type res = getType(rs.expr);
795    
796                        // alx: dw test universe of return stmt
797                        if (useUniverses
798                            && !universeIsSubtypeOf(
799                                universeReturnType,
800                                ParseUtil.getUniverse(rs.expr)))
801                            ErrorSet.error(
802                                rs.getStartLoc(),
803                                "This routine must return "
804                                    + TagConstants.toString(universeReturnType)
805                                    + ", not "
806                                    + TagConstants.toString(ParseUtil.getUniverse(rs.expr)));
807                        else if (useUniverses
808                            && !universeIsSubtypeOf(
809                                universeElementReturnType,
810                                ParseUtil.getElementUniverse(rs.expr)))
811                            ErrorSet.error(
812                                rs.getStartLoc(),
813                                "This routine must return "
814                                    + TagConstants.toString(universeReturnType)
815                                    + " "
816                                    + TagConstants.toString(universeElementReturnType)
817                                    + ", not "
818                                    + TagConstants.toString(ParseUtil.getUniverse(rs.expr))
819                                    + " "
820                                    + TagConstants.toString(ParseUtil.getElementUniverse(rs.expr)));
821                        // alx-end
822    
823                        if (Types.isSameType(returnType, Types.voidType))
824                            ErrorSet.error(
825                                rs.loc,
826                                "This routine is not expected to return a value");
827                        else if (!assignmentConvertable(rs.expr, returnType)) {
828                            if (!Types.isErrorType(res))
829                                ErrorSet.error(rs.loc, "Cannot convert "
830                                    + Types.printName(res) + " to return type "
831                                    + Types.printName(returnType));
832                        }
833                    } else {
834                        if (!Types.isSameType(returnType, Types.voidType))
835                            ErrorSet.error(
836                                rs.loc,
837                                "This routine must return a value");
838                    }
839                }
840                return e;
841            }
842    
843            case TagConstants.THROWSTMT: {
844                ThrowStmt t = (ThrowStmt)s;
845                t.expr = checkExpr(e, t.expr);
846                Type res = getType(t.expr);
847    
848                if (!Types.isSubclassOf(res, Types.javaLangThrowable())) {
849                    ErrorSet.error(t.loc, "Cannot throw values of type "
850                        + Types.printName(res));
851                } else {
852    
853                    if (Types.isCheckedException(res)) {
854    
855                        // Must be caught by try or throws clause
856                        for (int i = 0; i < allowedExceptions.size(); i++) {
857                            if (Types.isSubclassOf(
858                                res,
859                                allowedExceptions.elementAt(i)))
860                            // is ok
861                                return e;
862                        }
863                        // Not caught
864                        ErrorSet.error(
865                            t.loc,
866                            "Exception must be caught by an enclosing try "
867                                + "or throws clause");
868                    }
869                }
870                return e;
871            }
872    
873            case TagConstants.BLOCKSTMT:
874                checkStmtVec(e, ((GenericBlockStmt)s).stmts);
875                return e;
876    
877            case TagConstants.WHILESTMT: {
878                WhileStmt w = (WhileStmt)s;
879                w.expr = checkExpr(e, w.expr, Types.booleanType);
880                enclosingLabels.addElement(w);
881                checkStmt(e, w.stmt);
882                enclosingLabels.pop();
883                return e;
884            }
885    
886            case TagConstants.DOSTMT: {
887                DoStmt d = (DoStmt)s;
888                d.expr = checkExpr(e, d.expr, Types.booleanType);
889                enclosingLabels.addElement(d);
890                checkStmt(e, d.stmt);
891                enclosingLabels.pop();
892                return e;
893            }
894    
895            case TagConstants.IFSTMT: {
896                IfStmt i = (IfStmt)s;
897                i.expr = checkExpr(e, i.expr, Types.booleanType);
898                checkStmt(e, i.thn);
899                checkStmt(e, i.els);
900                return e;
901            }
902    
903            case TagConstants.SYNCHRONIZESTMT: {
904                SynchronizeStmt ss = (SynchronizeStmt)s;
905                ss.expr = checkExpr(e, ss.expr, Types.javaLangObject());
906                checkStmt(e, ss.stmt);
907                return e;
908            }
909    
910            case TagConstants.EVALSTMT: {
911                EvalStmt v = (EvalStmt)s;
912                v.expr = checkExpr(e, v.expr);
913                return e;
914            }
915    
916            case TagConstants.LABELSTMT: {
917                LabelStmt ls = (LabelStmt)s;
918                for (int i = 0; i < enclosingLabels.size(); i++) {
919                    Stmt enclosing = enclosingLabels.elementAt(i);
920                    if (enclosing instanceof LabelStmt
921                        && ((LabelStmt)enclosing).label == ls.label)
922                        ErrorSet.error(ls.locId, "Label '" + ls.label
923                            + "' already used in this scope");
924                    // FIXME - point to dup
925                }
926    
927                enclosingLabels.addElement(ls);
928                checkStmt(e, ls.stmt);
929                enclosingLabels.pop();
930    
931                return e;
932            }
933    
934            case TagConstants.TRYFINALLYSTMT: {
935                TryFinallyStmt tf = (TryFinallyStmt)s;
936                checkStmt(e, tf.tryClause);
937                checkStmt(e, tf.finallyClause);
938                return e;
939            }
940    
941            case TagConstants.TRYCATCHSTMT: {
942                TryCatchStmt tc = (TryCatchStmt)s;
943                TypeSigVec newExceptions = allowedExceptions.copy();
944    
945                // add all catch clause exceptions to allowedExceptions
946                for (int i = 0; i < tc.catchClauses.size(); i++) {
947                    CatchClause c = tc.catchClauses.elementAt(i);
948                    Type t = c.arg.type;
949                    e.resolveType(sig, t);
950                    checkTypeModifiers(e, t);
951                    if (!Types.isSubclassOf(t, Types.javaLangThrowable()))
952                        ErrorSet.error(
953                            c.loc,
954                            "Declared type of a catch formal parameter "
955                                + "must be a subclass of java.lang.Throwable");
956                    else {
957                        if (t instanceof TypeName) {
958                            t = TypeSig.getSig((TypeName)t);
959                        }
960                        newExceptions.addElement((TypeSig)t);
961                    }
962                    PrepTypeDeclaration.inst.checkModifiers(
963                        c.arg.modifiers,
964                        Modifiers.ACC_FINAL,
965                        c.arg.getStartLoc(),
966                        "formal parameter");
967    
968                    EnvForLocals subenv = new EnvForLocals(e, c.arg, false);
969                    checkStmt(subenv, c.body);
970                }
971    
972                TypeSigVec oldExceptions = allowedExceptions;
973                allowedExceptions = newExceptions;
974                checkStmt(e, tc.tryClause);
975                allowedExceptions = oldExceptions;
976    
977                return e;
978            }
979    
980            case TagConstants.FORSTMT: {
981                ForStmt f = (ForStmt)s;
982                Env se = checkStmtVec(e, f.forInit);
983                checkForLoopAfterInit(se, f);
984                return e;
985            }
986    
987            case TagConstants.CONSTRUCTORINVOCATION: {
988                ConstructorInvocation ci = (ConstructorInvocation)s;
989    
990                TypeSig calleeSig = ci.superCall ? TypeSig.getSig(((ClassDecl)sig.getTypeDecl()) // @nowarn
991                                                                                                    // Cast,NonNull;
992                    .superClass)
993                    : sig;
994    
995                /*
996                 * Everything before the constructor invocation call occurs is
997                 * considered to be in a static context:
998                 */
999                Env sEnv = e.asStaticContext();
1000    
1001                Type[] argTypes = checkExprVec(sEnv, ci.args);
1002    
1003                /*
1004                 * Handle type checking/inference for enclosing instance ptr:
1005                 */
1006    
1007                // Get the type of calleeSig's enclosing instance or null if none
1008                // exists:
1009                TypeSig enclosingInstanceType = calleeSig.getEnv(false).getEnclosingInstance();
1010    
1011                // If calleeSig has an enclosing instance and the user didn't supply
1012                // a value for it, try to infer one:
1013                if (ci.enclosingInstance == null && enclosingInstanceType != null) {
1014                    ci.locDot = ci.getStartLoc();
1015                    ci.enclosingInstance = sEnv.lookupEnclosingInstance(
1016                        enclosingInstanceType,
1017                        ci.getStartLoc());
1018                }
1019    
1020                if (ci.enclosingInstance != null) {
1021                    if (enclosingInstanceType != null)
1022                        ci.enclosingInstance = checkExpr(
1023                            sEnv,
1024                            ci.enclosingInstance,
1025                            enclosingInstanceType);
1026                    else
1027                        ErrorSet.error(
1028                            ci.enclosingInstance.getStartLoc(),
1029                            "An enclosing instance may be provided only "
1030                                + "when the superclass has an enclosing instance");
1031                } else if (enclosingInstanceType != null) {
1032                    /*
1033                     * Compute appropriate error message details:
1034                     */
1035                    String details;
1036                    if (ci.locKeyword == sig.getTypeDecl().locOpenBrace) {
1037                        // inferred constructor with an inferred super inside it:
1038                        details = "cannot create a default constructor for class "
1039                            + sig + ".";
1040                    } else if (ci.locKeyword == ci.locOpenParen) {
1041                        // inferred super(...) in an explicit constructor:
1042                        details = "cannot create a default superclass constructor."
1043                            + "  (superclass is " + calleeSig + ")";
1044                    } else {
1045                        // explicit super(...) case...
1046                        details = "an explicit one must be"
1047                            + " provided when creating inner class " + calleeSig
1048                            + ".";
1049                    }
1050    
1051                    ErrorSet.error(
1052                        ci.getStartLoc(),
1053                        "No enclosing instance of class " + enclosingInstanceType
1054                            + " is in scope; " + details);
1055                }
1056    
1057                try {
1058                    ConstructorDecl cd = calleeSig.lookupConstructor(argTypes, sig);
1059                    Assert.notNull(cd);
1060                    ci.decl = cd;
1061                } catch (LookupException ex) {
1062                    // Don't print an error if superclass is an interface (an
1063                    // error has already been reported in this case)
1064                    if (!ci.superCall
1065                        || calleeSig.getTypeDecl().getTag() == TagConstants.CLASSDECL)
1066                        reportLookupException(
1067                            ex,
1068                            "constructor " + calleeSig.getTypeDecl().id
1069                                + Types.printName(argTypes),
1070                            Types.printName(calleeSig),
1071                            ci.locKeyword);
1072                }
1073    
1074                // Rest of constructor body is in the normal non-static context:
1075                return e;
1076            }
1077    
1078            case TagConstants.ASSERTSTMT: {
1079                AssertStmt assertStmt = (AssertStmt)s;
1080                if (assertStmt.label != null)
1081                    assertStmt.label = checkExpr(e, assertStmt.label);
1082                assertStmt.pred = checkExpr(e, assertStmt.pred, Types.booleanType);
1083    
1084                // Turn a Java assert into a conditional throw and attach it to the
1085                // AssertStmt.
1086    
1087                // assert Predicate ;
1088                // ==>
1089                // if (! Predicate)
1090                // throw new java.lang.AssertionError();
1091                // or
1092                // assert Predicate : LabelExpr ;
1093                // ==>
1094                // if (! Predicate)
1095                // throw new java.lang.AssertionError(LabelExpr);
1096                int startLoc = assertStmt.getStartLoc();
1097                int endLoc = assertStmt.getEndLoc();
1098                Assert.notFalse(startLoc != Location.NULL);
1099                UnaryExpr negatedPredicate = UnaryExpr.make(
1100                    TagConstants.NOT,
1101                    assertStmt.pred,
1102                    startLoc);
1103                ParenExpr parenthesizedNegatedPredicate = ParenExpr.make(
1104                    negatedPredicate,
1105                    startLoc,
1106                    endLoc);
1107                Name javaLangAssertionErrorName = Name.make(
1108                    "java.lang.AssertionError",
1109                    startLoc);
1110                TypeName javaLangAssertionTypeName = TypeName.make(javaLangAssertionErrorName);
1111                ExprVec constructorArgs = null;
1112                if (assertStmt.label != null) {
1113                    Expr[] constructorArgsAsArray = { assertStmt.label };
1114                    constructorArgs = ExprVec.make(constructorArgsAsArray);
1115                } else {
1116                    constructorArgs = ExprVec.make();
1117                }
1118                NewInstanceExpr newAssertionError = NewInstanceExpr.make(
1119                    null,
1120                    Location.NULL,
1121                    javaLangAssertionTypeName,
1122                    constructorArgs,
1123                    null,
1124                    startLoc,
1125                    endLoc);
1126                ThrowStmt throwAssertionError = ThrowStmt.make(
1127                    newAssertionError,
1128                    startLoc);
1129                Stmt elseSkip = SkipStmt.make(startLoc);
1130                IfStmt ifStmt = IfStmt.make(
1131                    parenthesizedNegatedPredicate,
1132                    throwAssertionError,
1133                    elseSkip,
1134                    startLoc);
1135                // Now typecheck the generated IfStmt so that it is fully resolved.
1136                ifStmt.expr = checkExpr(e, ifStmt.expr, Types.booleanType);
1137                checkStmt(e, ifStmt.thn);
1138                checkStmt(e, ifStmt.els);
1139                // Reattach this translated form to the AST node.
1140                assertStmt.ifStmt = ifStmt;
1141    
1142                return e;
1143            }
1144    
1145            default:
1146                if (s instanceof StmtPragma)
1147                    checkStmtPragma(e, (StmtPragma)s);
1148                else {
1149                    Assert.fail("Switch fall-through (" + s.getTag() + " "
1150                        + TagConstants.toString(s.getTag()) + " "
1151                        + Location.toString(s.getStartLoc()) + ")");
1152                }
1153            }
1154            return e; // dummy
1155        }
1156        // === Typecheck statements : end ===
1157        
1158    
1159        // @ requires !(se instanceof EnvForCU);
1160        // @ requires sig != null;
1161        protected void checkForLoopAfterInit(/* @ non_null */ Env se,
1162                                             /* @ non_null */ ForStmt f) {
1163            f.test = checkExpr(se, f.test);
1164            for (int i = 0; i < f.forUpdate.size(); i++) {
1165                Expr ex = checkExpr(se, f.forUpdate.elementAt(i));
1166                f.forUpdate.setElementAt(ex, i);
1167            }
1168            enclosingLabels.addElement(f);
1169            checkStmt(se, f.body);
1170            enclosingLabels.pop();
1171        }
1172    
1173        // @ requires env != null && v != null;
1174        // @ requires !(env instanceof EnvForCU);
1175        // @ requires sig != null;
1176        // @ ensures \result != null;
1177        // @ ensures !(\result instanceof EnvForCU);
1178        protected Env checkStmtVec(Env env, StmtVec v) {
1179            for(int i = 0, sz = v.size(); i < sz; i++) {
1180                Stmt stmt = v.elementAt(i);
1181                
1182                env = checkStmt(env, stmt);
1183            }
1184    
1185            return env;
1186        }
1187    
1188      
1189        // @ requires env != null && ev != null ;
1190        // @ requires !(env instanceof EnvForCU);
1191        // @ requires sig != null;
1192        // @ ensures \nonnullelements(\result);
1193        protected Type[] checkExprVec(Env env, ExprVec ev) {
1194    
1195            Type[] r = new Type[ ev.size() ];
1196    
1197            for(int i = 0; i < ev.size(); i++) {
1198                Expr expr = ev.elementAt(i);
1199                Expr newExpr = checkExpr(env, expr);
1200                ev.setElementAt(newExpr, i);
1201                r[i] = getType(newExpr);
1202            }
1203    
1204            return r;
1205        }
1206    
1207    
1208        // @ requires sig != null;
1209        // @ requires !(env instanceof EnvForCU);
1210        // @ requires env != null && x != null && expectedResult != null;
1211        // @ ensures \result != null;
1212        // @ ensures (x instanceof ArrayInit) ==> \result instanceof ArrayInit;
1213        protected VarInit checkInit(Env env, VarInit x, Type expectedResult) {
1214            if (x instanceof ArrayInit) {
1215                ArrayInit ai = (ArrayInit)x;
1216    
1217                if(expectedResult instanceof ArrayType) {
1218                    //alx: dw remember least upper bound for universes
1219                        int bound=TagConstants.NULLLIT;
1220                    //alx-end
1221    
1222                    Type elemType = ((ArrayType)expectedResult).elemType;
1223                    for(int i=0; i< ai.elems.size(); i++) {
1224                        VarInit disamb = checkInit(env, ai.elems.elementAt(i), elemType);
1225                        ai.elems.setElementAt(disamb, i);
1226                        //alx: dw TODO: explain that addition
1227                        bound=leastUpperUniverseBound(bound,
1228                                               ParseUtil.getUniverse(disamb));
1229                        //alx-end
1230                    }
1231                    //alx: dw save bound as universe for the elements
1232                    ParseUtil.setElementUniverse(ai,bound);
1233                    //alx-end
1234    
1235                    setType(ai, expectedResult);
1236                } else {
1237                    ErrorSet.error(ai.locOpenBrace, 
1238                                   "Unexpected array value in initializer");
1239                }
1240                return x;
1241    
1242            } else {
1243                //@ assume \typeof(x) <: \type(Expr);
1244                return checkExpr(env, (Expr) x, expectedResult);
1245            }
1246        }
1247    
1248        //@ requires env != null && e != null;
1249        //@ requires !(env instanceof EnvForCU);
1250        //@ requires sig != null;
1251        //@ ensures \result != null;
1252        protected Expr checkDesignator(Env env, Expr e) {
1253            Expr result = checkExpr(env, e);
1254            if (result.getTag() == TagConstants.FIELDACCESS) {
1255                FieldAccess fa = (FieldAccess)result;
1256                if (fa.decl == Types.lengthFieldDecl) {
1257                    ErrorSet.error(fa.locId, "Invalid designator");
1258                }
1259                // Note, if it weren't for some Java 1.1 features, one could also
1260                // rule out the case:
1261                //   fa.decl != null && Modifiers.isFinal(fa.decl.modifiers)
1262                // here with a message "Final fields cannot be used as designators",
1263                // but Java 1.1 allows assignments to final fields in some contexts.
1264                // A more elaborate test could perhaps be used, though.
1265            }
1266            return result;
1267        }
1268    
1269        /**
1270         * Typechecks expressions.
1271         * @param env  The current environment.
1272         * @param expr The expression to be checked.
1273         * @param t    The expected type.
1274         * @return     The checked expression.
1275         */
1276        //@ requires !(env instanceof EnvForCU);
1277        //@ requires sig != null;
1278        //@ ensures \result == expr;
1279        protected Expr checkExpr(
1280            /*@ non_null */ Env env, 
1281            /*@ non_null */ Expr expr, 
1282            /*@ non_null */ Type t
1283        ) {
1284            Expr ne = checkExpr(env,expr);
1285            checkType(ne, t);
1286            return ne;
1287        }
1288        
1289        /**
1290         * Typechecks expressions. Work is delegated to specialized methods.
1291         * This way the clients that inherit from this class have a finer
1292         * grained control by overriding methods.
1293         * 
1294         * @param env The current environment.
1295         * @param x   The expression to typecheck.
1296         * @return    The checked expression. It has the type set.
1297         */
1298        //@ requires !(env instanceof EnvForCU);
1299        //@ requires sig != null;
1300        //@ ensures \result == x;
1301        //@ ensures getTypeOrNull(\result) != null;
1302        protected Expr checkExpr(/*@ non_null */ Env env, /*@ non_null */ Expr x) {
1303            // System.out.println("Checking: "+Location.toString(x.getStartLoc()));
1304    
1305            if (getTypeOrNull(x) != null) {
1306                // already checked
1307                return x;
1308            }
1309    
1310            // Set default result type to error.
1311            setType(x, Types.errorType);
1312    
1313            switch (x.getTag()) {
1314            case TagConstants.THISEXPR:
1315                return checkThisExpr(env, (ThisExpr)x);
1316    
1317            // The environment is not needed to check literals.
1318            case TagConstants.STRINGLIT:
1319                return checkStringLitExpr(x);
1320            case TagConstants.CHARLIT:
1321                return checkCharLitExpr(x);
1322            case TagConstants.BOOLEANLIT:
1323                return checkBooleanLitExpr(x);
1324            case TagConstants.FLOATLIT:
1325                return checkFloatLitExpr(x);
1326            case TagConstants.DOUBLELIT:
1327                return checkDoubleLitExpr(x);
1328            case TagConstants.INTLIT: 
1329                return checkIntLitExpr(x);
1330            case TagConstants.LONGLIT:
1331                return checkLongLitExpr(x);
1332            case TagConstants.NULLLIT: 
1333                return checkNullLitExpr(x);
1334    
1335            case TagConstants.ARRAYREFEXPR:
1336                return checkArrayRefExpr(env, (ArrayRefExpr)x);
1337            case TagConstants.NEWINSTANCEEXPR:
1338                return checkNewInstanceExpr(env, (NewInstanceExpr)x);
1339            case TagConstants.NEWARRAYEXPR:
1340                return checkNewArrayExpr(env, (NewArrayExpr)x);
1341            case TagConstants.CONDEXPR:
1342                return checkCondExpr(env, (CondExpr)x);
1343            case TagConstants.INSTANCEOFEXPR:
1344                return checkInstanceOfExpr(env, (InstanceOfExpr)x);
1345            case TagConstants.CASTEXPR:
1346                return checkCastExpr(env, (CastExpr)x);
1347    
1348            case TagConstants.CLASSLITERAL:
1349                return checkClassLiteralExpr(env, (ClassLiteral)x);
1350    
1351            case TagConstants.OR: case TagConstants.AND:
1352            case TagConstants.BITOR: case TagConstants.BITXOR:
1353            case TagConstants.BITAND: case TagConstants.NE:
1354            case TagConstants.EQ: case TagConstants.GE:
1355            case TagConstants.GT: case TagConstants.LE:
1356            case TagConstants.LT: case TagConstants.LSHIFT:
1357            case TagConstants.RSHIFT: case TagConstants.URSHIFT:
1358            case TagConstants.ADD: case TagConstants.SUB:
1359            case TagConstants.DIV: case TagConstants.MOD:
1360            case TagConstants.STAR:
1361                return checkBinaryExpr(env, (BinaryExpr)x);
1362      
1363            case TagConstants.ASSIGN: case TagConstants.ASGMUL:
1364            case TagConstants.ASGDIV: case TagConstants.ASGREM:
1365            case TagConstants.ASGADD: case TagConstants.ASGSUB:
1366            case TagConstants.ASGLSHIFT: case TagConstants.ASGRSHIFT:
1367            case TagConstants.ASGURSHIFT: case TagConstants.ASGBITAND:
1368            case TagConstants.ASGBITOR: case TagConstants.ASGBITXOR: 
1369                return checkAssignmentExpr(env, (BinaryExpr)x);
1370    
1371            case TagConstants.UNARYADD: 
1372            case TagConstants.UNARYSUB:
1373                return checkSignExpr(env, (UnaryExpr)x);
1374    
1375            case TagConstants.BITNOT:
1376                return checkBitnotExpr(env, (UnaryExpr)x);
1377    
1378            case TagConstants.INC: case TagConstants.DEC: 
1379            case TagConstants.POSTFIXINC: case TagConstants.POSTFIXDEC:
1380                return checkIncDecExpr(env, (UnaryExpr)x);
1381      
1382            case TagConstants.NOT:
1383                return checkNotExpr(env, (UnaryExpr)x);
1384      
1385            case TagConstants.PARENEXPR:
1386                return checkParenExpr(env, (ParenExpr)x);
1387    
1388            case TagConstants.AMBIGUOUSVARIABLEACCESS:
1389                return checkAmbiguousVariableAccessExpr(env, (AmbiguousVariableAccess)x);
1390            case TagConstants.FIELDACCESS:
1391                return checkFieldAccessExpr(env, (FieldAccess)x);
1392            case TagConstants.AMBIGUOUSMETHODINVOCATION:
1393                return checkAmbiguousMethodInvocationExpr(env, (AmbiguousMethodInvocation)x);
1394            case TagConstants.METHODINVOCATION:
1395                return checkMethodInvocationExpr(env, (MethodInvocation)x);
1396    
1397            case TagConstants.VARIABLEACCESS:
1398                // TODO: No environment needed? (rgrig)
1399                return checkVariableAccessExpr((VariableAccess)x); 
1400    
1401            default:
1402                System.out.println("FAIL " + x);
1403                System.out.println(" AT " + Location.toString(x.getStartLoc())); 
1404                Assert.fail(
1405                    "Switch fall-through (" + TagConstants.toString(x.getTag()) + ")"
1406                );
1407                //@ assert false;
1408                return null; // dummy
1409            }
1410        }
1411    
1412        /**
1413         * Typecheck variable access. 
1414         * @param lva The variable access.
1415         * @return    The variable access.
1416         */
1417        //@ ensures getTypeOrNull(\result) != null;
1418        protected Expr checkVariableAccessExpr(/*@ non_null */ VariableAccess lva) {
1419            setType(lva, lva.decl.type);
1420            Assert.notNull(getType(lva));
1421    
1422            //alx: dw take the universes of the declaration
1423            if (useUniverses) {
1424                copyUniverses(lva, lva.decl);
1425            }
1426            //alx-end
1427    
1428            // Front-end VariableAccess's never point to fields.
1429            Assert.notFalse(!(lva.decl instanceof FieldDecl)); //@ nowarn Pre;
1430    
1431            // Make sure only access final variables from enclosing instances.
1432            if (Env.whereDeclared(lva.decl) != sig && 
1433                !Modifiers.isFinal(lva.decl.modifiers)) {
1434                ErrorSet.error(
1435                    lva.loc,
1436                    "Attempt to use a non-final variable from a different " +
1437                    "method. From enclosing blocks, only final local variables " +
1438                    "are available."
1439                );
1440            }
1441    
1442            return lva;
1443        }
1444    
1445        /**
1446         * Typecheck method invocation.
1447         * @param env The current environment.
1448         * @param mi  The method invocation.
1449         * @return    The checked method invocation.
1450         */
1451        //@ ensures getTypeOrNull(\result) != null;
1452        protected MethodInvocation checkMethodInvocationExpr(
1453            /*@ non_null */ Env env, 
1454            /*@ non_null */ MethodInvocation mi
1455        ) {
1456            Type t = checkObjectDesignator(env, mi.od);
1457            Type[] argTypes = checkExprVec(env, mi.args);
1458    
1459            // TODO: Shouldn't an error be reported for [t == null]? (rgrig)
1460            if (t != null) {
1461                try {
1462                    mi.decl = Types.lookupMethod(t, mi.id, argTypes, sig);
1463                    setType(mi, mi.decl.returnType);
1464    
1465                    //alx: dw determine or set default universe modifier
1466                    if (useUniverses) {
1467                        determineUniverseForMethodInvocation(mi);
1468                    }
1469                    // alx-end
1470    
1471                    // When [x.y] is correctly used, x being a class (type) implies
1472                    // that y is a static method; otherwise something is wrong. 
1473                    if (mi.od instanceof TypeObjectDesignator &&
1474                        !Modifiers.isStatic(mi.decl.modifiers)) {
1475                        // Figure out what exactly is wrong.
1476    
1477                        // Is mi.decl an instance method of the same class as
1478                        // mi is part of?
1479                        boolean thisMethod = false;
1480                        if (mi.decl.parent != null) {
1481                            thisMethod = 
1482                                env.getEnclosingClass().isSubtypeOf(TypeSig.getSig(mi.decl.parent));
1483                        }
1484    
1485                        if (thisMethod ||
1486                            ((TypeObjectDesignator)mi.od).type instanceof TypeName) {
1487                            ErrorSet.error(
1488                                mi.locId, 
1489                                "An instance method may be invoked" +
1490                                    " only via an object and/or from a non-static" +
1491                                    " context or an inner class enclosed by a type" +
1492                                    " possessing that method."
1493                            );
1494                        } else {
1495                            ErrorSet.error(
1496                                mi.locId,
1497                                "The instance methods of type " +
1498                                    ((TypeObjectDesignator)mi.od).type +
1499                                    " may not be invoked from type " + sig
1500                            );
1501                        }
1502                    }
1503                } catch(LookupException ex) {
1504                    if (!Types.isErrorType(t)) {
1505                        reportLookupException(
1506                            ex, 
1507                            "method " + mi.id + Types.printName(argTypes), 
1508                            Types.printName(t), 
1509                            mi.locId
1510                        );
1511                    }
1512                    setType(mi, Types.errorType);
1513                }
1514            }
1515            return mi;
1516        }
1517    
1518        /**
1519         * Disambiguates an ambiguous method invocation and then typechecks it.
1520         * @param env The current environment.
1521         * @param ami The ambiguous method invocation.
1522         * @return    The checked ambiguous invocation.
1523         */
1524        //@ ensures getTypeOrNull(\result) != null;
1525        protected Expr checkAmbiguousMethodInvocationExpr(
1526            /*@ non_null */ Env env, 
1527            /*@ non_null */ AmbiguousMethodInvocation ami
1528        ) {
1529            MethodInvocation resolved = env.disambiguateMethodName(ami);
1530            Assert.notFalse(
1531                resolved != null, 
1532                "Disambiguation failure should result in a fatal error."
1533            );
1534            return checkExpr(env, resolved);
1535        }
1536    
1537        /**
1538         * Typechecks a field access (e.g., <tt>this.x</tt>).
1539         * @param env The current environment.
1540         * @param fa  The field access.
1541         * @return    The checked field access.
1542         */
1543        //@ ensures getTypeOrNull(\result) != null;
1544        protected FieldAccess checkFieldAccessExpr(
1545            /*@ non_null */ Env env, 
1546            /*@ non_null */ FieldAccess fa
1547        ) {
1548            Type t = checkObjectDesignator(env, fa.od);
1549            if (t != null) {
1550                try {
1551                    fa.decl = Types.lookupField(t, fa.id, sig);
1552                    setType(fa, fa.decl.type);
1553    
1554                    // TODO: The following code duplicates a lot of the code in checkMethodInvocation.
1555                    // Given [x.y]. It should hold that if x is a class then y is static.
1556                    if (fa.od instanceof TypeObjectDesignator &&
1557                        !Modifiers.isStatic(fa.decl.modifiers)) {
1558                        // Determine what error should be produced.
1559                        
1560                        // Is fa.decl an instance field of the same class as
1561                        // fa is part of?
1562                        boolean thisField = false;
1563                        if (fa.decl.parent != null) {
1564                            thisField = 
1565                                env.getEnclosingClass().isSubtypeOf(TypeSig.getSig(fa.decl.parent));
1566                        }
1567                        if (thisField ||
1568                            ((TypeObjectDesignator)fa.od).type instanceof TypeName) {
1569                            ErrorSet.error(
1570                                fa.locId,
1571                                "An instance field may be accessed only via " +
1572                                    "an object and/or from a non-static" +
1573                                    " context or an inner class enclosed" +
1574                                    " by a type possessing that field."
1575                            );
1576                        } else {
1577                            // FIXME - point to declaration
1578                            // _Also_ point to [fa.decl.locId]? (rgrig)
1579                            ErrorSet.error(
1580                                fa.locId,
1581                                "The instance fields of type " +
1582                                    ((TypeObjectDesignator)fa.od).type +
1583                                    " may not be accessed from type " + sig
1584                            );
1585                            // FIXME = point to declaration
1586                        }
1587                    }
1588                    //alx: dw determine or set universe type
1589                    if (useUniverses) {
1590                        determineUniverseForFieldAccess(fa);
1591                    }
1592                    //alx-end
1593                } catch(LookupException ex) {
1594                    if (!Types.isErrorType(t)) {
1595                        reportLookupException(ex, "field", Types.printName(t), fa.locId);
1596                    }
1597                    setType(fa, Types.errorType);
1598                }
1599            } 
1600            // alx: dw if no target, just copy universe modifier of declaration. 
1601            // does this ever happen???
1602            else if (useUniverses) {
1603                copyUniverses(fa, fa.decl);
1604            }
1605            //alx-end
1606            return fa;
1607        }
1608    
1609        
1610        /**
1611         * Disambiguates an ambiguous variable access and then typechecks
1612         * (e.g., <tt>x</tt>).
1613         * @param env The current environment.
1614         * @param av  The variable access.
1615         * @return    The disambiguated and checked variable access.
1616         */
1617        //@ ensures getTypeOrNull(\result) != null;
1618        protected Expr checkAmbiguousVariableAccessExpr(
1619            /*@ non_null */ Env env, 
1620            /*@ non_null */ AmbiguousVariableAccess av
1621        ) {
1622            Assert.notNull(av.name);
1623            Expr resolved = env.disambiguateExprName(av.name);
1624            if(resolved == null) {
1625                if (av.name.size() == 1) {
1626                    ErrorSet.error(
1627                        av.getStartLoc(),
1628                        "Undefined variable '" + av.name.printName() + "'"
1629                    );
1630                } else {
1631                    ErrorSet.error(
1632                        av.getStartLoc(),
1633                        "Cannot resolve variable access '" +
1634                        av.name.printName() + "'"
1635                    );
1636                }
1637                setType(av, Types.errorType);
1638                return av;
1639            }
1640            Assert.notFalse(resolved.getTag() != TagConstants.AMBIGUOUSVARIABLEACCESS); 
1641            return checkExpr(env, resolved);
1642        }
1643    
1644        
1645        /**
1646         * Typechecks paranthesis.
1647         * @param env The current environment.
1648         * @param pe  The paranthesis expression.
1649         * @return    The checked paranthesis expression.
1650         */
1651        //@ ensures getTypeOrNull(\result) != null;
1652        protected Expr checkParenExpr(
1653            /*@ non_null */ Env env, 
1654            /*@ non_null */ ParenExpr pe
1655        ) {
1656            pe.expr = checkExpr(env, pe.expr);
1657            setType(pe, getType(pe.expr));
1658            //alx: dw copy the universes to the paren-expr
1659            if (useUniverses) {
1660                copyUniverses(pe,pe.expr);
1661            }
1662            //alx-end
1663            return pe;
1664        }
1665    
1666        
1667        /**
1668         * Typecheck boolean not (e.g., <tt>!x</tt>). 
1669         * The argument must be boolean and the result is a boolean.
1670         * @param env The current environment.
1671         * @param ue  The unary expression containing the boolean not operation.
1672         * @return The typechecked not expression.
1673         */
1674        //@ requires ue.getTag() == TagConstants.NOT;
1675        //@ ensures getTypeOrNull(\result) != null;
1676        protected Expr checkNotExpr(
1677            /*@ non_null */ Env env, 
1678            /*@ non_null */ UnaryExpr ue
1679        ) {
1680            // Argument must be boolean, result is boolean
1681            ue.expr = checkExpr(env, ue.expr, Types.booleanType);
1682            setType(ue, Types.booleanType);
1683            return ue;
1684        }
1685    
1686        
1687        /**
1688         * Typecheck unary increment and decrement operators (e.g., <tt>++x</tt>). 
1689         * @param env The current environment.
1690         * @param ue  The unary expression representing the inc(dec)rement.
1691         * @return The checked expression.
1692         */
1693        /*@ requires ue.getTag() == TagConstants.INC || 
1694                     ue.getTag() == TagConstants.DEC ||
1695                     ue.getTag() == TagConstants.POSTFIXINC ||
1696                     ue.getTag() == TagConstants.POSTFIXDEC;
1697            ensures getTypeOrNull(\result) != null; */
1698        protected Expr checkIncDecExpr(
1699            /*@ non_null */ Env env, 
1700            /*@ non_null */ UnaryExpr ue
1701        ) {
1702            ue.expr = checkDesignator(env, ue.expr);
1703            if (ue.expr instanceof VariableAccess) {
1704                GenericVarDecl v = ((VariableAccess)ue.expr).decl;
1705                if (Modifiers.isFinal(v.modifiers)) {
1706                    ErrorSet.caution(
1707                        ue.expr.getStartLoc(),
1708                        "May not assign to a final variable",
1709                        v.getStartLoc()
1710                    );
1711                }
1712            } else if (ue.expr instanceof FieldAccess) {
1713                GenericVarDecl v = ((FieldAccess)ue.expr).decl;
1714                // v is null if there was an error such as a field
1715                // name that does not exist
1716                if (v == Types.lengthFieldDecl) { 
1717                    ErrorSet.error(
1718                        ue.expr.getStartLoc(),
1719                        "May not assign to array's length field"
1720                    );
1721                }
1722                else if (v != null && Modifiers.isFinal(v.modifiers)) {
1723                    ErrorSet.caution(
1724                        ue.expr.getStartLoc(),
1725                        "May not assign to a final field",
1726                        v.getStartLoc()
1727                    );
1728                }
1729            }
1730    
1731            // FIXME - need checks of more complicated expressions
1732    
1733            // Argument must be primitive numeric variable type
1734            if (checkNumericType(ue.expr)) {
1735                if(!isVariable(ue.expr))
1736                    ErrorSet.error(ue.locOp,
1737                            "Argument of increment/decrement operation "
1738                            +"is not a location");
1739                // Result is of same type
1740                setType(ue, getType(ue.expr));
1741            }
1742            return ue;
1743        }
1744    
1745        
1746        /**
1747         * Typecheck bitwise negation (e.g., <tt>~x</tt>).
1748         * The argument must be a primitive numeric type; the result
1749         * has the same type as the argument. 
1750         * @param env The current environment.
1751         * @param ue  The unary expression representing bitwise negation.
1752         * @return The checked expression.
1753         */
1754        //@ requires ue.getTag() == TagConstants.BITNOT;
1755        //@ ensures getTypeOrNull(\result) != null;
1756        protected Expr checkBitnotExpr(
1757            /*@ non_null */ Env env, 
1758            /*@ non_null */ UnaryExpr ue
1759        ) {
1760            ue.expr = checkExpr(env, ue.expr);
1761            if(checkIntegralType(ue.expr)) {
1762                setType(ue, Types.unaryPromote(getType(ue.expr)));
1763            } 
1764            return ue;
1765        }
1766    
1767        /**
1768         * Typecheck sign (e.g. <tt>+x</tt> or <tt>-x</tt>).
1769         * The argument must be a primitive numeric type; the result
1770         * has the same type as the argument.
1771         * @param env The current environment;
1772         * @param ue  The unary expression representing the sign.
1773         * @return The checked expression.
1774         */
1775        /*@ requires ue.getTag() == TagConstants.UNARYADD ||
1776                     ue.getTag() == TagConstants.UNARYSUB;
1777            ensures getTypeOrNull(\result) != null; */
1778        protected Expr checkSignExpr(
1779            /*@ non_null */ Env env, 
1780            /*@ non_null */ UnaryExpr ue
1781        ) {
1782            ue.expr = checkExpr(env, ue.expr);
1783            Type t = getType(ue.expr);
1784            if(checkNumericType(ue.expr)) {
1785                setType(ue, Types.unaryPromote(getType(ue.expr)));
1786            }
1787            return ue;
1788        }
1789    
1790        /**
1791         * Typecheck assignment-like expressions (e.g., <tt>a += 2</tt>).
1792         * @param env The current environment.
1793         * @param be  The binary expression representing the assignment.
1794         * @return The checked expression.
1795         */
1796        /*@ requires be.getTag() == TagConstants.ASSIGN ||
1797                     be.getTag() == TagConstants.ASGMUL ||
1798                     be.getTag() == TagConstants.ASGDIV ||
1799                     be.getTag() == TagConstants.ASGREM ||
1800                     be.getTag() == TagConstants.ASGADD ||
1801                     be.getTag() == TagConstants.ASGSUB ||
1802                     be.getTag() == TagConstants.ASGLSHIFT ||
1803                     be.getTag() == TagConstants.ASGRSHIFT ||
1804                     be.getTag() == TagConstants.ASGURSHIFT ||
1805                     be.getTag() == TagConstants.ASGBITAND ||
1806                     be.getTag() == TagConstants.ASGBITOR ||
1807                     be.getTag() == TagConstants.ASGBITXOR;
1808            ensures getTypeOrNull(\result) != null; */
1809        protected Expr checkAssignmentExpr(
1810            /*@ non_null */ Env env, 
1811            /*@ non_null */ BinaryExpr be
1812        ) {
1813            be.left = checkDesignator(env, be.left);
1814            be.right = checkExpr(env, be.right);
1815            Type t = checkBinaryExpr(be.op, be.left, be.right, be.locOp);
1816            setType(be, t);
1817            return be;
1818        }
1819    
1820        /**
1821         * Typecheck simple binary expressions (e.g., <tt>x + y</tt>).
1822         * @param env The current environment.
1823         * @param be  The simple binary expression.
1824         * @return    The checked expression.
1825         */
1826        // TODO: It's ugly to have two methods with the same name. (rgrig)
1827        /*@ requires be.getTag() == TagConstants.OR ||
1828                     be.getTag() == TagConstants.AND ||
1829                     be.getTag() == TagConstants.BITOR ||
1830                     be.getTag() == TagConstants.BITXOR ||
1831                     be.getTag() == TagConstants.BITAND ||
1832                     be.getTag() == TagConstants.NE ||
1833                     be.getTag() == TagConstants.EQ ||
1834                     be.getTag() == TagConstants.GE ||
1835                     be.getTag() == TagConstants.GT ||
1836                     be.getTag() == TagConstants.LE ||
1837                     be.getTag() == TagConstants.LT ||
1838                     be.getTag() == TagConstants.LSHIFT ||
1839                     be.getTag() == TagConstants.RSHIFT ||
1840                     be.getTag() == TagConstants.URSHIFT ||
1841                     be.getTag() == TagConstants.ADD ||
1842                     be.getTag() == TagConstants.SUB ||
1843                     be.getTag() == TagConstants.DIV ||
1844                     be.getTag() == TagConstants.MOD ||
1845                     be.getTag() == TagConstants.STAR;
1846            ensures getTypeOrNull(\result) != null; */
1847        protected Expr checkBinaryExpr(
1848            /*@ non_null */ Env env, 
1849            /*@ non_null */ BinaryExpr be
1850        ) {
1851            be.left = checkExpr(env, be.left);
1852            be.right = checkExpr(env, be.right);
1853            Type t = checkBinaryExpr(be.op, be.left, be.right, be.locOp);
1854            //alx: dw set universe for the binary expression, if any
1855            if (useUniverses) {
1856                copyUniverses(be,be.left);
1857            }
1858            // alx-end
1859            setType(be, t);
1860            return be;
1861        }
1862    
1863        /**
1864         * Typechecks a class literal (e.g., <tt>X</tt> which might appear
1865         * as the rhs of <tt>instanceof</tt>).
1866         * @param env The current environment.
1867         * @param cl  The class literal to check.
1868         * @return    The checked expression.
1869         */
1870        //@ ensures getTypeOrNull(\result) != null;
1871        protected Expr checkClassLiteralExpr(
1872            /*@ non_null */ Env env, 
1873            /*@ non_null */ ClassLiteral cl
1874        ) {
1875            env.resolveType(sig,cl.type);
1876            checkTypeModifiers(env, cl.type); 
1877            setType(cl, Types.javaLangClass());
1878            //alx: dw is a field => set to IMPL_PEER
1879            ParseUtil.setUniverse(cl,TagConstants.IMPL_PEER);
1880            //alx-end
1881            return cl;
1882        }
1883    
1884        /**
1885         * Typecheck a (dynamic) cast.
1886         * @param env The current environment.
1887         * @param ce  The cast to be checked.
1888         * @return    The checked expression.
1889         */
1890        //@ ensures getTypeOrNull(\result) != null;
1891        protected CastExpr checkCastExpr(
1892            /*@ non_null */ Env env, 
1893            /*@ non_null */ CastExpr ce
1894        ) {
1895            ce.expr = checkExpr(env, ce.expr);
1896            Type exprType = getType(ce.expr);
1897            env.resolveType(sig, ce.type);
1898            checkTypeModifiers(env, ce.type); 
1899     
1900            if(!Types.isCastable(exprType, ce.type)) {
1901                ErrorSet.error(
1902                    ce.locOpenParen, 
1903                    "Bad cast from "+Types.printName(exprType) + " to " +
1904                        Types.printName(ce.type)
1905                );
1906            }
1907            //alx: dw check castability and 'no rep in static context'
1908            if (useUniverses) {
1909                checkUniverseCastability(ce, ce.expr);
1910                checkNoRepInStaticContext(ce);
1911            }
1912            //alx-end
1913            setType(ce, ce.type);
1914            return ce;
1915        }
1916    
1917        /**
1918         * Typechecks a dynamic type probe (e.g., <tt>x instanceof X</tt>).
1919         * @param env The current environment.
1920         * @param ie  The <tt>instance of</tt> expression.
1921         * @return    The checked expression.
1922         */
1923        //@ ensures getTypeOrNull(\result) != null;
1924        protected Expr checkInstanceOfExpr(
1925            /*@ non_null */ Env env, 
1926            /*@ non_null */ InstanceOfExpr ie
1927        ) {
1928            ie.expr = checkExpr(env, ie.expr);
1929            Type exprType = getType(ie.expr);
1930            env.resolveType(sig, ie.type);
1931            checkTypeModifiers(env, ie.type);
1932            if(!Types.isReferenceType(ie.type)) {
1933                ErrorSet.error(ie.loc, "Non-reference type in instanceof operation");
1934            }
1935            else if(!Types.isCastable(exprType, ie.type)) {
1936                ErrorSet.error(
1937                    ie.loc, 
1938                    "Invalid instanceof operation: " +
1939                        "A value of type " + Types.printName(exprType) +
1940                        " can never be an instance of " +
1941                        Types.printName(ie.type)
1942                );
1943            }
1944            //alx: dw check castability for instanceof-expr
1945            if (useUniverses) {
1946                checkUniverseCastability(ie,ie.expr);
1947                checkNoRepInStaticContext(ie);
1948            }
1949            //alx-end
1950    
1951            setType(ie, Types.booleanType);
1952            return ie;
1953        }
1954    
1955        /**
1956         * Typechecks a conditional expression (e..g, <tt>a == 0 ? x : 0</tt>).
1957         * @param env The current environment.
1958         * @param ce  The expression to check.
1959         * @return    The checked expression.
1960         */
1961        //@ ensures getTypeOrNull(\result) != null;
1962        protected Expr checkCondExpr(
1963            /*@ non_null */ Env env, 
1964            /*@ non_null */ CondExpr ce
1965        ) {
1966            ce.test = checkExpr(env, ce.test, Types.booleanType);
1967            ce.thn = checkExpr(env, ce.thn);
1968            ce.els = checkExpr(env, ce.els);
1969    
1970            // The two branches should have compatible types (i.e., at least one
1971            // should be castable to the other).
1972            Type res = tryCondExprMatch(ce.thn, ce.els);
1973            if (res != null) {
1974                setType(ce, res);
1975            } else {
1976                ErrorSet.error(
1977                    ce.locQuestion,
1978                    "Incompatible arguments to the ?: operator"
1979                );
1980            }
1981            
1982            //alx: dw determine universe for 'b? (peer T) x: (rep T) x;'
1983            if (useUniverses) {
1984                int l = ParseUtil.getUniverse(ce.thn);
1985                int r = ParseUtil.getUniverse(ce.els);
1986                if (l != 0) { //isn't a primitiv type
1987                    int n = leastUpperUniverseBound(l, r);
1988                    ParseUtil.setUniverse(ce, n);
1989                    l = ParseUtil.getElementUniverse(ce.thn);
1990                    r = ParseUtil.getElementUniverse(ce.els);
1991                    n = leastUpperUniverseBound(l, r);
1992                    ParseUtil.setElementUniverse(ce,n);
1993                }
1994            }
1995            //alx-end
1996    
1997            return ce;
1998        }
1999    
2000        /**
2001         * Typecheck a new array construction (e.g., <tt>new int[100]</tt>).
2002         * @param env The current environment.
2003         * @param na  The expression to check.
2004         * @return    The checked expression.
2005         */
2006        //@ ensures getTypeOrNull(\result) != null;
2007        protected Expr checkNewArrayExpr(
2008            /*@ non_null */ Env env, 
2009            /*@ non_null */ NewArrayExpr na
2010        ) {
2011            env.resolveType(sig, na.type);
2012            Type r = na.type;
2013            checkTypeModifiers(env, r); 
2014            for (int i = 0; i < na.dims.size(); i++) {
2015                // (Type)Check the dimension is an integer.
2016                Expr e = na.dims.elementAt(i);
2017                Expr newExpr = checkExpr(env, e, Types.intType);
2018                na.dims.setElementAt(newExpr, i);
2019                
2020                // Add a dimension to the array type.
2021                r = ArrayType.make(r, na.locOpenBrackets[i]);
2022                checkTypeModifiers(env, r); 
2023            }
2024            setType(na, r);
2025    
2026            if (na.init != null) {
2027                // Check the case where we have something like
2028                //   new int[] {1, 2, 3}
2029                na.init = (ArrayInit)checkInit(env, na.init, r);
2030                //alx: dw set the universe type for array inits and test it
2031                if (useUniverses) {
2032                    if (ParseUtil.getUniverse(na.init) == 0 && 
2033                        ParseUtil.getElementUniverse(na.init) != 0) {
2034                        ParseUtil.setUniverse(na.init, ParseUtil.getUniverse(na));
2035                    }
2036                    checkUniverseAssignability(na,na.init);
2037                }
2038                //alx-end
2039            }
2040            
2041            //alx: dw check if universes are used in the static context
2042            if (useUniverses) {
2043                checkNoRepInStaticContext(na);
2044            }
2045            //alx-end
2046    
2047            return na;
2048        }
2049    
2050        /**
2051         * Typecheck a class instantiation (e.g., <tt>new C()</tt>).
2052         * @param env The current environment.
2053         * @param ne  The instantiotion to check.
2054         * @return    The checked instantiation.
2055         */
2056        //@ ensures getTypeOrNull(\result) != null;
2057        protected NewInstanceExpr checkNewInstanceExpr(
2058            /*@ non_null */ Env env,
2059            /*@ non_null */ NewInstanceExpr ne
2060        ) {
2061            /*
2062             * We handle the "scoping" of ne.type differently depending on
2063             * whether or not an explicit enclosing instance ptr is
2064             * provided:
2065             */
2066            TypeSig calleeSig;
2067            if (ne.enclosingInstance==null) {
2068                // 1.0 case:  new N(...) ...
2069                env.resolveType(sig,ne.type);
2070                checkTypeModifiers(env, ne.type);
2071                calleeSig = TypeSig.getSig(ne.type);
2072            } else {
2073                // 1.1 case: E.new I(...) ...
2074    
2075                // Type check E to get class type enclosingType:
2076                ne.enclosingInstance = checkExpr(env, ne.enclosingInstance);
2077                TypeSig enclosingInstanceType;
2078                try {
2079                    enclosingInstanceType =
2080                        (TypeSig)getType(ne.enclosingInstance);  //@ nowarn Cast;//caught
2081                } catch (ClassCastException E) {
2082                    ErrorSet.error(ne.enclosingInstance.getStartLoc(),
2083                                   "The enclosing instance supplied in a new"
2084                                   + " expression must be of a class type.");
2085                    enclosingInstanceType = Types.javaLangObject();
2086                }
2087    
2088                // Check and "resolve" I:
2089                if (ne.type.name.size() != 1)
2090                    ErrorSet.error(ne.type.getStartLoc(),
2091                                   "Only a simple name can be used after new"
2092                                   + " when an enclosing instance is supplied.");
2093                Identifier id = ne.type.name.identifierAt(0);
2094                int idLoc = ne.type.name.locIdAt(0);
2095                calleeSig = enclosingInstanceType.lookupType(enclosingInstanceType, id, idLoc);
2096                if (calleeSig==null)
2097                    ErrorSet.fatal(ne.type.getStartLoc(),
2098                                   "No such type: "
2099                                   + enclosingInstanceType.toString()+"$"+id);
2100                checkTypeModifiers(env, ne.type);
2101                TypeSig.setSig(ne.type, calleeSig);
2102            }
2103    
2104    
2105            /*
2106             * Handle remaining type checking/inference for enclosing instance ptr:
2107             */
2108    
2109            // Get the type of calleeSig's enclosing instance or null if none
2110            // exists:
2111            TypeSig enclosingInstanceType = calleeSig.getEnv(false)
2112                .getEnclosingInstance();
2113    
2114            // If calleeSig has an enclosing instance and the user didn't supply
2115            // a value for it, try to infer one:
2116            if (ne.enclosingInstance==null && enclosingInstanceType != null) {
2117                Expr enclosingInstance =
2118                    env.lookupEnclosingInstance(enclosingInstanceType,
2119                                                ne.getStartLoc());
2120                if (enclosingInstance != null) {
2121                    ne.locDot = ne.getStartLoc();
2122                    ne.enclosingInstance = enclosingInstance;
2123                    checkExpr(env, ne.enclosingInstance, enclosingInstanceType);
2124                }
2125            }
2126    
2127            if (ne.enclosingInstance != null) {
2128                if (enclosingInstanceType==null)
2129                    ErrorSet.error(ne.enclosingInstance.getStartLoc(),
2130                                   "An enclosing instance may be provided only "
2131                                   + "when the named instance type is an inner class");
2132            } else if (enclosingInstanceType != null) {
2133                ErrorSet.error(ne.getStartLoc(),
2134                               "No enclosing instance of class "
2135                               + enclosingInstanceType
2136                               + " is in scope; an explicit one must be provided"
2137                               + " when creating instances of inner class "
2138                               + calleeSig + ".");
2139            }
2140    
2141            /*
2142             * The type that will *actually* call the constructor
2143             * 
2144             * (matters if the constructor is "protected"!)
2145             */
2146            TypeSig caller = sig;
2147    
2148            /*
2149             * Handle anonymous class case:
2150             */
2151            if (ne.anonDecl != null) {
2152                // Update anonDecl to have proper supertype:
2153                if (calleeSig.getTypeDecl() instanceof ClassDecl) {
2154                    Assert.notFalse(ne.anonDecl.superClass==null);  //@ nowarn Pre;
2155                    ne.anonDecl.superClass = ne.type;
2156                } else {
2157                    ne.anonDecl.superInterfaces.addElement(ne.type);
2158                    calleeSig = Types.javaLangObject();
2159                }
2160    
2161                // Create and check TypeSig for declared type:
2162                TypeSig T = Types.makeTypeSig(null, env, ne.anonDecl);
2163                T.typecheck();
2164                caller = T;
2165                setType(ne, T);
2166            } else
2167                setType(ne, ne.type);
2168    
2169    
2170            Type[] argTypes = checkExprVec(env, ne.args);
2171    
2172            if (!(calleeSig.getTypeDecl() instanceof ClassDecl))
2173                ErrorSet.error(ne.loc, 
2174                               "Cannot create an instance of an interface");
2175            else if (Modifiers.isAbstract(calleeSig.getTypeDecl().modifiers)
2176                     && ne.anonDecl==null)
2177                ErrorSet.error(ne.loc,
2178                               "Cannot create an instance of an abstract class");
2179            else { 
2180                try {
2181                    ConstructorDecl cd = calleeSig.lookupConstructor(argTypes, caller);
2182                    ne.decl = cd;
2183                } catch(LookupException e) {
2184                    reportLookupException(e, "constructor", 
2185                                          Types.printName(calleeSig), ne.loc);
2186                }
2187            }
2188            
2189            //alx: dw test args uf .ctor
2190            if (useUniverses) {
2191                checkNoRepInStaticContext(ne);
2192                for (int i = 0; i<ne.args.size(); i++) {
2193                    FormalParaDecl decl_arg = ne.decl.args.elementAt(i);
2194                    if (
2195                        readonlyStdForPureCtor && 
2196                        ParseUtil.getUniverse(decl_arg)==TagConstants.IMPL_PEER
2197                    ) {
2198                        ParseUtil.setUniverse(decl_arg, TagConstants.READONLY);
2199                        checkUniverseAssignability(
2200                            ne.decl.args.elementAt(i),
2201                            ne.args.elementAt(i)
2202                        );
2203                    }
2204                }
2205            }
2206            //alx-end
2207    
2208            return ne;
2209        }
2210    
2211        /**
2212         * Typechecks an array reference expression (e.g., <tt>a[3]</tt>). 
2213         * @param env The current environment.
2214         * @param r   The expression to check.
2215         * @return    The checked expression.
2216         */
2217        //@ ensures getTypeOrNull(\result) != null;
2218        protected ArrayRefExpr checkArrayRefExpr(
2219            /*@ non_null */ Env env, 
2220            /*@ non_null */ ArrayRefExpr r
2221        ) {
2222            r.array = checkExpr(env, r.array);
2223            Type arrType = getType(r.array);
2224    
2225            if(arrType instanceof ArrayType) {
2226                setType(r, ((ArrayType)arrType).elemType);
2227            } else {
2228                setType(r, Types.errorType);
2229                if (!Types.isErrorType(arrType)) {
2230                    ErrorSet.error(r.locOpenBracket, "Attempt to index a non-array value");
2231                }
2232            }
2233      
2234            r.index = checkExpr(env, r.index);
2235            Type t = getType(r.index);
2236            Type ndxType = Types.isNumericType(t) ? Types.unaryPromote(t) : t;
2237            if (
2238                !Types.isSameType(ndxType, Types.intType) &&
2239                !Types.isErrorType(ndxType)
2240            ) { 
2241                ErrorSet.error(r.locOpenBracket, "Array index is not an integer");
2242            }
2243    
2244            //alx: dw set universe modifier for ArrayRefExpr, but this is 
2245            //   never used because for this switch-case the overriding 
2246            //   method in escjava doesn't call the super implementation
2247            if (useUniverses) {
2248                determineUniverseForArrayRefExpr(r);
2249            }
2250            //alx-end
2251            
2252            return r;
2253        }
2254    
2255        /**
2256         * Typechecks <tt>null</tt>.
2257         * @param x The null expression.
2258         * @return  The null expression.
2259         */
2260        //@ requires x.getTag() == TagConstants.NULLLIT;
2261        //@ ensures getTypeOrNull(\result) != null;
2262        protected Expr checkNullLitExpr(/*@ non_null */ Expr x) {
2263            //alx: dw use NULLLIT as a universe modifier
2264            setType(x, Types.nullType);
2265            if (useUniverses) {
2266                ParseUtil.setUniverse(x,TagConstants.NULLLIT);
2267            }
2268            //alx-end
2269            return x;
2270        }
2271    
2272        /**
2273         * Typechecks long literal expressions (e.g., <tt>29L</tt>).
2274         * @param x The literal.
2275         * @return  The literal.
2276         */
2277        //@ requires x.getTag() == TagConstants.LONGLIT;
2278        //@ ensures getTypeOrNull(\result) != null;
2279        protected Expr checkLongLitExpr(/*@ non_null */ Expr x) {
2280            setType(x, Types.longType);
2281            return x;
2282        }
2283    
2284        /**
2285         * Typechecks integers (e.g., <tt>29</tt>).
2286         * @param x The literal.
2287         * @return  The literal.
2288         */
2289        //@ requires x.getTag() == TagConstants.INTLIT;
2290        //@ ensures getTypeOrNull(\result) != null;
2291        protected Expr checkIntLitExpr(/*@ non_null */ Expr x) {
2292            setType(x, Types.intType);
2293            return x;
2294        }
2295    
2296        /**
2297         * Typechecks doubles (e.g., <tt>2.9</tt>).
2298         * @param x The literal.
2299         * @return  The literal.
2300         */
2301        //@ requires x.getTag() == TagConstants.DOUBLELIT;
2302        //@ ensures getTypeOrNull(\result) != null;
2303        protected Expr checkDoubleLitExpr(/*@ non_null */ Expr x) {
2304            setType(x, Types.doubleType);
2305            return x;
2306        }
2307    
2308        /**
2309         * Typechecks floats (e.g., <tt>2.9F</tt>). 
2310         * @param x The literal.
2311         * @return  The literal.
2312         */
2313        //@ requires x.getTag() == TagConstants.FLOATLIT;
2314        //@ ensures getTypeOrNull(\result) != null;
2315        protected Expr checkFloatLitExpr(/*@ non_null */ Expr x) {
2316            setType(x, Types.floatType);
2317            return x;
2318        }
2319    
2320        /**
2321         * Typechecks booleans.
2322         * @param x The literal.
2323         * @return  The literal.
2324         */
2325        //@ requires x.getTag() == TagConstants.BOOLEANLIT;
2326        //@ ensures getTypeOrNull(\result) != null;
2327        protected Expr checkBooleanLitExpr(Expr x) {
2328            setType(x, Types.booleanType);
2329            return x;
2330        }
2331    
2332        /**
2333         * Typechecks characters.
2334         * @param x The literal.
2335         * @return  The literal.
2336         */
2337        //@ requires x.getTag() == TagConstants.CHARLIT;
2338        //@ ensures getTypeOrNull(\result) != null;
2339        protected Expr checkCharLitExpr(/*@ non_null */ Expr x) {
2340            setType(x, Types.charType);
2341            return x;
2342        }
2343    
2344        /**
2345         * Typechecks strings.
2346         * @param x The expression to be checked.
2347         * @return  The checked expression.
2348         */
2349        //@ requires x.getTag() == TagConstants.STRINGLIT;
2350        //@ ensures getTypeOrNull(\result) != null;
2351        protected Expr checkStringLitExpr(/*@ non_null */ Expr x) {
2352            setType(x, Types.javaLangString());
2353            //alx: dw set to implicit peer
2354            ParseUtil.setUniverse(x, TagConstants.IMPL_PEER);
2355            //alx-end
2356            return x;
2357        }
2358    
2359        /**
2360         * Typechecks <tt>this</tt> expression.
2361         * @param env The current environment.
2362         * @param e   The expression to check.
2363         * @return    The checked expression (which was mutated).
2364         */
2365        //@ ensures getTypeOrNull(\result) != null;
2366        protected Expr checkThisExpr(/*@ non_null */ Env env, /*@ non_null */ ThisExpr e) {
2367                 //alx: dw use this like a universe modifier to simplify universeTypeCombiner
2368                 if (useUniverses) {
2369                     ParseUtil.setUniverse(e, TagConstants.THISEXPR);
2370            }
2371                 // alx-end
2372    
2373            // It is illegal to use [this] in static methods.
2374            if (env.isStaticContext() && e.classPrefix == null) {
2375                ErrorSet.error(
2376                    e.getStartLoc(),
2377                    "Unqualified this cannot be used in static contexts"
2378                );
2379            }
2380    
2381            Type referredType = sig;
2382            if (e.classPrefix != null) {
2383                env.resolveType(sig, e.classPrefix);
2384                referredType = e.classPrefix;
2385                checkTypeModifiers(env, referredType);
2386    
2387                // It is illegal to use [X.this] if we are not within X.
2388                TypeSig classPrefix = Types.toClassTypeSig(referredType);
2389                if (classPrefix == null || !env.canAccessInstance(classPrefix)) {
2390                    ErrorSet.error(
2391                        e.getStartLoc(),
2392                        "Undefined variable: "
2393                            + PrettyPrint.inst.toString(referredType) + ".this"
2394                    );
2395                    setType(e, Types.errorType);
2396                    return e;
2397                }
2398                
2399                // alx: dw this of enclosing instances is peer in pure .ctors
2400                if (useUniverses) {
2401                    if (inCtor && inPure) {
2402                        ParseUtil.setUniverse(e, TagConstants.READONLY);
2403                    } else {
2404                        ParseUtil.setUniverse(e, TagConstants.PEER);
2405                    }
2406                }
2407                // alx-end
2408            }
2409    
2410            setType(e, referredType);
2411            return e;
2412        }
2413    
2414        // ======================================================================
2415    
2416        //@ requires env != null && od != null;
2417        //@ requires !(env instanceof EnvForCU);
2418        //@ requires sig != null;
2419        protected Type checkObjectDesignator(Env env, ObjectDesignator od) {
2420    
2421            switch(od.getTag()) {
2422          
2423                case TagConstants.EXPROBJECTDESIGNATOR: {
2424                    ExprObjectDesignator eod = (ExprObjectDesignator)od;
2425                    eod.expr = checkExpr(env, eod.expr);
2426                    eod.type = getType(eod.expr);
2427                    //alx: dw copy universes of the inner expression
2428                    if (useUniverses && ParseUtil.getUniverse(eod.expr)!=0)
2429                            ParseUtil.setUniverse(eod,
2430                                                  ParseUtil.getUniverse(eod.expr));
2431                    //alx-end
2432                    return eod.type;
2433                }
2434    
2435                case TagConstants.TYPEOBJECTDESIGNATOR: {
2436                    TypeObjectDesignator tod = (TypeObjectDesignator)od;
2437                    // Type has been created by disambiguation code, so it is ok.
2438    
2439                    Type t = tod.type;
2440                    if(t instanceof TypeName) {
2441                        t = TypeSig.getSig((TypeName)t);
2442                        tod.type = t;
2443                    }
2444                    Assert.notFalse(t instanceof TypeSig);
2445                    checkTypeModifiers(env, t);  
2446                    return (TypeSig)t;
2447                }
2448    
2449                case TagConstants.SUPEROBJECTDESIGNATOR: {
2450                    SuperObjectDesignator sod = (SuperObjectDesignator)od;
2451                    //alx: dw super is peer
2452                    if (useUniverses)
2453                        ParseUtil.setUniverse(sod,TagConstants.PEER);
2454                    //alx-end
2455    
2456                    if(env.isStaticContext()) {
2457                        ErrorSet.error(sod.locSuper,
2458                                       "Keyword super cannot be used in a static context");
2459                        return null;
2460                    }
2461                    else {
2462                        TypeDecl d = sig.getTypeDecl();
2463                        if (d instanceof ClassDecl) {
2464                            TypeName superClass = ((ClassDecl)d).superClass;
2465                            if (superClass==null) {
2466                                Assert.notFalse(sig==Types.javaLangObject()); //@ nowarn Pre;
2467                                ErrorSet.error(sod.locDot, 
2468                                                "Can't use keyword super in java.lang.Object");
2469                                return null;
2470                            }
2471    
2472                            TypeSig ts = TypeSig.getSig(superClass);
2473                            sod.type = ts;
2474                            return ts;
2475                        } else {
2476                            ErrorSet.error(sod.locDot, 
2477                                            "Can't use keyword super in an interface");
2478                            return null;
2479                        }
2480                    }
2481                }
2482    
2483                default:
2484                    Assert.fail("Fall thru");
2485                    return null; // dummy return
2486            }
2487        }
2488    
2489        // ======================================================================
2490    
2491        /**
2492         * Return the type of a E1 : L ? R expression given the typechecked Expr's for L
2493         * and R, as per JLS 15.24.
2494         *
2495         * @return null if the given combination is illegal.
2496         */
2497        //@ requires leftExpr != null && rightExpr != null;
2498        private Type tryCondExprMatch(Expr leftExpr, Expr rightExpr) {
2499            Type leftType = getType(leftExpr);
2500            Type rightType = getType(rightExpr);
2501                                              
2502            /*
2503             * If the second and third operands have the same type,
2504             * then than is the type of the conditional expression:
2505             */
2506            if (Types.isSameType(leftType, rightType))
2507                return leftType;
2508    
2509    
2510            /*
2511             * Rules for case where both L and R have numeric types:
2512             */
2513            if (Types.isNumericType(leftType)
2514                && Types.isNumericType(rightType)) {
2515                /*
2516                 * If one of the operands is of type byte 
2517                 * and the other is of type short, 
2518                 * then the type of the conditional expression is short:
2519                 */
2520                if (Types.isSameType(leftType, Types.byteType) &&
2521                    Types.isSameType(rightType, Types.shortType))
2522                    return Types.shortType;
2523                if (Types.isSameType(rightType, Types.byteType) &&
2524                    Types.isSameType(leftType, Types.shortType))
2525                    return Types.shortType;
2526    
2527                /*
2528                 * If one of the operands is of type T where T is byte/short/char, 
2529                 * and the other operand is a constant expression of type int
2530                 * whose value is representable in type T,
2531                 * then the type of the conditional expression is T.
2532                 */
2533                if ((Types.isSameType(leftType, Types.byteType) ||
2534                     Types.isSameType(leftType, Types.shortType) ||
2535                     Types.isSameType(leftType, Types.charType))
2536                    && ConstantExpr.
2537                    constantValueFitsIn(ConstantExpr.eval(rightExpr),
2538                                        (PrimitiveType)leftType))
2539                    return leftType;
2540                if ((Types.isSameType(rightType, Types.byteType) ||
2541                     Types.isSameType(rightType, Types.shortType) ||
2542                     Types.isSameType(rightType, Types.charType))
2543                    && ConstantExpr.
2544                    constantValueFitsIn(ConstantExpr.eval(leftExpr),
2545                                        (PrimitiveType)rightType))
2546                    return rightType;
2547    
2548    
2549                /*
2550                 * Otherwise, binary numeric promotion (5.6.2) is applied
2551                 * to the operand types, and the type of the conditional
2552                 * expression is the promoted type:
2553                 */
2554                return Types.binaryNumericPromotion(leftType, rightType);
2555            }
2556    
2557    
2558            /*
2559             * If one operands is of the null type and the other is 
2560             * a reference type, then the result type is that reference type
2561             */
2562            if (Types.isSameType(leftType, Types.nullType) &&
2563                Types.isReferenceType(rightType)) 
2564                return rightType;
2565            if (Types.isSameType(rightType, Types.nullType) &&
2566                Types.isReferenceType(leftType)) 
2567                return leftType;
2568    
2569    
2570            /*
2571             * If the second and third operands are of different reference
2572             * types, then it must be possible to convert one of the types
2573             * to the other type (call this latter type T) by assignment
2574             * conversion (5.2); the type of the conditional expression
2575             * is T. It is a compile-time error if neither type is
2576             * assignment compatible with the other type.
2577             */
2578            if (Types.isReferenceType(leftType) 
2579                && Types.isReferenceType(rightType)) {
2580                if (assignmentConvertable(leftExpr, rightType))
2581                    return rightType;
2582                if (assignmentConvertable(rightExpr, leftType))
2583                    return leftType;
2584            }
2585    
2586            // Invalid combination
2587            return null;
2588    
2589        }
2590    
2591        // ======================================================================
2592    
2593        //@ requires left != null && right != null;
2594        //@ requires loc != Location.NULL;
2595        //@ ensures \result != null  ;
2596        protected Type checkBinaryExpr(int op, Expr left, Expr right, int loc) {
2597      
2598            Type leftType = getType(left);
2599            Type rightType = getType(right);
2600    
2601            switch(op) {
2602        
2603                case TagConstants.ADD:
2604        
2605                    if(Types.isSameType(leftType, Types.javaLangString()) 
2606                        || Types.isSameType(rightType, Types.javaLangString())) {
2607          
2608                        // Operation is string concatenation
2609                        return Types.javaLangString();
2610                    }
2611                    // else fall thru
2612          
2613                case TagConstants.STAR: 
2614                case TagConstants.DIV: 
2615                case TagConstants.MOD: 
2616                case TagConstants.SUB: {
2617                    if(checkNumericType(left)
2618                        && checkNumericType(right))
2619                        return Types.binaryNumericPromotion(leftType, rightType);
2620                    else
2621                        // error recovery
2622                        return Types.intType;
2623                } 
2624    
2625                case TagConstants.LSHIFT: 
2626                case TagConstants.RSHIFT: 
2627                case TagConstants.URSHIFT:
2628          
2629                    // Arguments must be primitive integral types
2630                    // result is unary promoted type of left operand
2631          
2632                    if(checkIntegralType(left) 
2633                        && checkIntegralType(right))
2634                        return Types.unaryPromote(leftType);
2635                    else
2636                        // error recovery
2637                        return Types.intType;
2638          
2639                case TagConstants.LT: 
2640                case TagConstants.LE: 
2641                case TagConstants.GT: 
2642                case TagConstants.GE:
2643          
2644                    // Arguments must be primitive numeric types
2645                    // result is boolean
2646          
2647                    checkNumericType(left);
2648                    checkNumericType(right);
2649                    return Types.booleanType;
2650          
2651                case TagConstants.BITAND: 
2652                case TagConstants.BITOR: 
2653                case TagConstants.BITXOR: {
2654                    if(!Types.isBooleanType(leftType)) {
2655              
2656                        // Arguments are primitive integral
2657                        // binary numeric promotion is performed
2658                        // type of result is promoted type of operands
2659              
2660                        if(checkIntegralType(left)
2661                            && checkIntegralType(right))
2662                            return Types.binaryNumericPromotion(leftType, rightType);
2663                        else
2664                            // error recovery
2665                            return Types.intType;
2666                    } 
2667            
2668                    // else fall thru. Arguments must be boolean, result is boolean
2669                }
2670          
2671                case TagConstants.AND: 
2672                case TagConstants.OR: {
2673                    // Arguments must be boolean, result is also boolean
2674                    checkType(left, Types.booleanType);
2675                    checkType(right, Types.booleanType);
2676                    return Types.booleanType;
2677                }
2678          
2679                case TagConstants.EQ: 
2680                case TagConstants.NE:
2681                    if( (Types.isNumericType(leftType) 
2682                           && Types.isNumericType(rightType))
2683                          || (!Types.isVoidType(leftType)
2684                              && Types.isSameType(leftType, rightType))
2685                          || (Types.isReferenceOrNullType(leftType) 
2686                              && Types.isReferenceOrNullType(rightType))) {
2687            
2688                        if(  Types.isCastable(leftType, rightType) 
2689                              || Types.isCastable(rightType, leftType)) {
2690                            // is ok, result boolean
2691                            return Types.booleanType;
2692                        } 
2693                    }
2694          
2695                    // Fall thru to here on error
2696    
2697                    if (!Types.isErrorType(leftType) && !Types.isErrorType(rightType)) {
2698                        ErrorSet.error(loc, 
2699                                   "Invalid types ("+Types.printName(leftType)
2700                                   +" and "+Types.printName(rightType)
2701                                   +") in equality comparison");
2702                    }
2703                    return Types.booleanType;
2704          
2705                case TagConstants.ASSIGN:
2706                case TagConstants.ASGMUL: 
2707                case TagConstants.ASGDIV: 
2708                case TagConstants.ASGREM: 
2709                case TagConstants.ASGADD: 
2710                case TagConstants.ASGSUB:
2711                case TagConstants.ASGLSHIFT: 
2712                case TagConstants.ASGRSHIFT: 
2713                case TagConstants.ASGURSHIFT:
2714                case TagConstants.ASGBITAND:
2715                case TagConstants.ASGBITOR: 
2716                case TagConstants.ASGBITXOR: {
2717                    if (left instanceof VariableAccess) {
2718                        //alx: dw check that target is not readonly & 
2719                        //        field is not rep (if target!=this)
2720                        if (useUniverses) {
2721                            FieldAccess fa = (FieldAccess) left;
2722                            if (ParseUtil.getUniverse(fa.od)==TagConstants.READONLY)
2723                                ErrorSet.error(fa.getStartLoc(),
2724                                      "cannot assign to field of readonly target");
2725                            else if (ParseUtil.getUniverse(fa.decl)==TagConstants.REP && 
2726                                     ParseUtil.getUniverse(fa.od)!=TagConstants.THISEXPR)
2727                                ErrorSet.error(fa.getStartLoc(),
2728                                      "cannot assign to rep field of target "+
2729                                      "different from this");
2730                        }
2731                        GenericVarDecl v = ((VariableAccess)left).decl;
2732                        if (Modifiers.isFinal(v.modifiers) && 
2733                            (v instanceof FormalParaDecl ||
2734                            (v instanceof LocalVarDecl &&
2735                                ((LocalVarDecl)v).init != null)
2736                            ))
2737                            ErrorSet.caution(left.getStartLoc(),
2738                                "May not assign to a final variable",
2739                                v.getStartLoc());
2740                    } else if (left instanceof FieldAccess) {
2741                        GenericVarDecl v = ((FieldAccess)left).decl;
2742                        // v is null if there was an error such as a field
2743                        // name that does not exist
2744                        if (v == Types.lengthFieldDecl) 
2745                            ErrorSet.error(left.getStartLoc(),
2746                                "May not assign to array's length field");
2747                        else if (v != null && Modifiers.isFinal(v.modifiers) &&
2748                            v instanceof FieldDecl &&
2749                            ((FieldDecl)v).init != null)
2750                            ErrorSet.caution(left.getStartLoc(),
2751                                "May not assign to a final field",
2752                                v.getStartLoc());
2753    
2754                    }
2755                        // FIXME - need checks of more complicated expressions
2756    
2757                    if(!isVariable(left)) {
2758                        if (!Types.isErrorType(leftType)) ErrorSet.error(loc,
2759                                       "Left hand side of assignment operator "+
2760                                       "is not a location");
2761                    } else if(op == TagConstants.ASSIGN) {
2762                        if(!assignmentConvertable(right, leftType) &&
2763                            !Types.isErrorType(getType(right)) && !Types.isErrorType(leftType))
2764                            ErrorSet.error(loc,
2765                                           "Value of type "+Types.printName(getType(right))
2766                                           +" cannot be assigned to location of type "
2767                                           + Types.printName(leftType));
2768                        //alx: dw check that target is not readonly for 
2769                        //        array element assignments and test universe
2770                        //        type assignment
2771                        if (useUniverses) {
2772                                if (left instanceof ArrayRefExpr) {
2773                                ArrayRefExpr ar = (ArrayRefExpr) left;
2774                                if (ParseUtil.getUniverse(ar.array)==TagConstants.READONLY)
2775                                    ErrorSet.error(ar.getStartLoc(),
2776                                           "cannot assign to elements of "+
2777                                           "a readonly array reference");
2778                                }
2779                                // test universe types of assignment
2780                                checkUniverseAssignability(left,right);
2781                        }
2782                        //alx-end
2783                    } else {
2784                        // E1 op= E2 is equivalent to
2785                        // E1 = (T)(E1 op E2), where T is type of E1
2786                        int simpleop;
2787                        switch(op) {
2788                            case TagConstants.ASGMUL:    simpleop=TagConstants.STAR;    break;
2789                            case TagConstants.ASGDIV:    simpleop=TagConstants.DIV;     break;
2790                            case TagConstants.ASGREM:    simpleop=TagConstants.MOD;     break;
2791                            case TagConstants.ASGADD:    simpleop=TagConstants.ADD;     break;
2792                            case TagConstants.ASGSUB:    simpleop=TagConstants.SUB;     break;
2793                            case TagConstants.ASGLSHIFT: simpleop=TagConstants.LSHIFT;  break;
2794                            case TagConstants.ASGRSHIFT: simpleop=TagConstants.RSHIFT;  break;
2795                            case TagConstants.ASGURSHIFT:simpleop=TagConstants.URSHIFT; break;
2796                            case TagConstants.ASGBITAND: simpleop=TagConstants.BITAND;  break;
2797                            case TagConstants.ASGBITOR:  simpleop=TagConstants.BITOR;   break;
2798                            case TagConstants.ASGBITXOR: simpleop=TagConstants.BITXOR;  break;
2799                            default: Assert.fail("Incomplete case"); simpleop=0; // dummy init
2800                        }
2801                        Type result = checkBinaryExpr(simpleop, left, right, loc);
2802                        // Check if result is convertable to leftType
2803                        if(!Types.isCastable(result, leftType))
2804                            ErrorSet.error(loc, 
2805                                           "Result type "+Types.printName(result)
2806                                           +" of assignment operation cannot be cast to type "
2807                                           +Types.printName(leftType));
2808                    }  
2809                    // done
2810                    return leftType;
2811                }
2812    
2813                default:
2814                    Assert.fail("Fall thru, op = "+op); 
2815                    return null;
2816            }
2817        }
2818    
2819        // *********************************************************************
2820    
2821        //@ requires e != null;
2822        static boolean checkIntegralType(Expr e) {
2823            Type t = getType(e);
2824            if(Types.isIntegralType(t)) {
2825                return true;
2826            } else {
2827                if (!Types.isErrorType(t))
2828                    ErrorSet.error(e.getStartLoc(), 
2829                                "Cannot convert "+Types.printName(t)
2830                                +" to an integral type");
2831                return false;
2832            }
2833        }
2834    
2835        //@ requires e != null;
2836        static boolean checkNumericType(Expr e) {
2837            Type t = getType(e);
2838            if(!Types.isNumericType(t)) {
2839                if (!Types.isErrorType(t))
2840                    ErrorSet.error(e.getStartLoc(), 
2841                                "Cannot convert "+Types.printName(t)
2842                                +" to a numeric type ");
2843                return false;
2844            } else {
2845                return true;
2846            }    
2847        }
2848    
2849        //@ requires e != null;
2850        static boolean isVariable(Expr e) {
2851            switch(e.getTag()) {
2852                case TagConstants.ARRAYREFEXPR:
2853                case TagConstants.VARIABLEACCESS:
2854                case TagConstants.FIELDACCESS: 
2855                    return true;
2856    
2857                default:
2858                    return false;
2859            }
2860        }
2861    
2862        // ======================================================================
2863    
2864        /**
2865         * Decorates <code>VarInit</code> nodes to point to <code>Type</code> objects.
2866         */
2867        //@ private static invariant typeDecoration.decorationType == \type(Type);
2868        private static /*@non_null*/ ASTDecoration typeDecoration
2869            = new ASTDecoration("typeDecoration");
2870        static { 
2871          initTypeDecoration();
2872        }
2873        private /*@helper*/ static void initTypeDecoration()
2874        {
2875          //@ set typeDecoration.decorationType = \type(Type);
2876        }
2877    
2878        //@ requires i != null && t != null;
2879        public static VarInit setType(VarInit i, Type t) {
2880            if (t instanceof TypeName)
2881                t = TypeSig.getSig((TypeName)t);
2882            typeDecoration.set(i, t);
2883            return i;
2884        }
2885    
2886        /**
2887         * Retrieves the <code>Type</code> of a <code>VarInit</code>.  This type is
2888         * associated with an expression by the typechecking pass. If the expression does
2889         * not have an associated type, then null is returned.
2890         */
2891        //@ requires i != null;
2892        protected static Type getTypeOrNull(VarInit i) {
2893            return (Type)typeDecoration.get(i);
2894        }
2895    
2896        /**
2897         * Retrieves the <code>Type</code> of a <code>VarInit</code>.  This type is
2898         * associated with an expression by the typechecking pass. If the expression does
2899         * not have an associated type, then <code>Assert.fail</code> is called.
2900         */
2901        //@ requires i != null;
2902        //@ ensures \result != null;
2903        public static Type getType(VarInit i) {
2904            Type t = getTypeOrNull(i);
2905            if (t == null) {
2906                Assert.fail(
2907                    "getType at " + i.getTag() + " " + PrettyPrint.inst.toString(i) +
2908                        Location.toString(i.getStartLoc())
2909                );
2910            }
2911            return t;
2912        }
2913    
2914    
2915        // ======================================================================
2916    
2917        /**
2918         * Decorates <code>BranchStmt</code> nodes to point to labelled <code>Stmt</code>
2919         * objects.
2920         */
2921        //@ private invariant branchDecoration != null;
2922        //@ private invariant branchDecoration.decorationType == \type(Stmt);
2923        private static ASTDecoration branchDecoration
2924            = new ASTDecoration("branchDecoration");
2925    
2926        //@ requires s != null && l != null;
2927        private static void setBranchLabel(BranchStmt s, Stmt l) {
2928            Assert.notFalse(branchDecoration.get(s) == null);        //@ nowarn Pre;
2929            branchDecoration.set(s,l);
2930        }
2931    
2932        /**
2933         * Retrieves the <code>Stmt</code> target of a <code>BranchStmt</code>.  This
2934         * <code>Stmt</code> may be mentioned either explicitly (as in <code>break
2935         * label;</code>), or implicitly (as in <code>break;</code>) by the
2936         * <code>BranchStmt</code>.  The correct <code>Stmt</code> target is associated
2937         * with the <code>BranchStmt</code> by the typechecking pass. This type is
2938         * associated with an expression by the typechecking pass. If the
2939         * <code>BranchStmt</code> does not have an associated <code>Stmt</code> target,
2940         * then <code>Assert.fail</code> is called.
2941         */
2942        //@ requires s != null;
2943        static Stmt getBranchLabel(BranchStmt s) {
2944            Stmt l = (Stmt)branchDecoration.get(s);
2945            if(l==null)
2946                Assert.fail("getBranchLabel failed at "+s.getTag());
2947            return l;
2948        }
2949    
2950        // ======================================================================
2951    
2952        //@ requires expr != null && t != null;
2953        static void checkType(Expr expr, Type t) {
2954            if(!inst.assignmentConvertable(expr, t)) {
2955                if (!Types.isErrorType(getType(expr)))
2956                    ErrorSet.error(expr.getStartLoc(), 
2957                                "Cannot convert "+Types.printName(getType(expr))
2958                                +" to "+Types.printName(t));
2959            }
2960        
2961        }
2962    
2963        //@ requires e != null && s != null && t != null;
2964        //@ requires loc != Location.NULL;
2965        protected static void reportLookupException(LookupException e, 
2966                                                    String s, 
2967                                                    String t, 
2968                                                    int loc) {
2969            switch(e.reason) {
2970                case LookupException.NOTFOUND:
2971                    ErrorSet.error(loc, "No such "+s+" in type "+t);
2972                    break;
2973                case LookupException.AMBIGUOUS:
2974                    ErrorSet.error(loc, "Ambiguous "+s+" for type "+t);
2975                    break;
2976                case LookupException.BADTYPECOMBO:
2977                    ErrorSet.error(loc, "No "+s+" matching given argument types");
2978                    break;
2979                case LookupException.NOTACCESSIBLE:
2980                    ErrorSet.error(loc, "Cannot access this "+s);
2981                    break;
2982                default:
2983                    Assert.fail("Bad lookup exception: "+e.reason);
2984            }
2985        }
2986    
2987        /**
2988         * Checks if Exp e can be assigned to Type t.  This method is here instead of in
2989         * {@link javafe.tc.Types}, because it needs to mess with constants.
2990         */ 
2991        //@ requires e != null && t != null;
2992        protected boolean assignmentConvertable(Expr e, Type t) {
2993    
2994            Type te = getType(e);
2995    
2996            if(Types.isInvocationConvertable(te, t))
2997                return true;
2998    
2999            // Check if t is byte/short/char, 
3000            // and e a constant expression whose value fits in t.
3001    
3002            switch(t.getTag()) {
3003                case TagConstants.BYTETYPE:
3004                case TagConstants.SHORTTYPE:
3005                case TagConstants.CHARTYPE:
3006                    Object val = ConstantExpr.eval(e);
3007                    if(val != null &&
3008                       ConstantExpr.constantValueFitsIn(val, (PrimitiveType)t))
3009                        return true;
3010                    else return false;
3011                default:
3012                    return false;
3013            }
3014        }
3015    
3016        // ======================================================================
3017    
3018        //@ requires e != null;
3019        protected void checkTypeDeclElemPragma(TypeDeclElemPragma e) {
3020            Assert.fail("Unexpected TypeDeclElemPragma");
3021        }
3022    
3023        /**
3024         * Hook to do additional processing on <code>ModifierVec</code>s.  The
3025         * <code>ASTNode</code> is the parent of the <code>ModifierPragma</code>, and
3026         * <code>env</code> is the current environment.
3027         */
3028        //@ requires env != null;
3029        protected Env checkModifierPragmaVec(ModifierPragmaVec v, 
3030                                             ASTNode ctxt, 
3031                                             Env env) {
3032            if (v != null)
3033              for(int i = 0; i < v.size(); i++) {
3034                env = checkModifierPragma(v.elementAt(i), ctxt, env);
3035                  }
3036              return env;
3037        }
3038    
3039        /**
3040         * Hook to do additional processing on <code>Modifier</code>s.  The
3041         * <code>ASTNode</code> is the parent of the <code>ModifierPragma</code>, and
3042         * <code>env</code> is the current environment.
3043         * @return true if pragma should be deleted
3044         */
3045        //@ requires p != null && env != null;
3046        protected Env checkModifierPragma(ModifierPragma p, ASTNode ctxt, Env env) {
3047            // Assert.fail("Unexpected ModifierPragma");
3048            return env;
3049        }
3050    
3051        //@ requires e != null && s != null;
3052        protected Env checkStmtPragma(Env e, StmtPragma s) {
3053            Assert.fail("Unexpected StmtPragma");
3054            return e;
3055        }
3056    
3057        //@ requires env != null;
3058        protected Env checkTypeModifierPragmaVec(TypeModifierPragmaVec v, 
3059                                                  ASTNode ctxt, 
3060                                                  Env env) {
3061            if(v != null)
3062                for(int i=0; i<v.size(); i++)
3063                    env = checkTypeModifierPragma(v.elementAt(i), ctxt, env);
3064            return env;
3065        }
3066        
3067        //@ requires p != null && env != null;
3068        protected Env checkTypeModifierPragma(TypeModifierPragma p,
3069                                               ASTNode ctxt,
3070                                               Env env) {
3071            Assert.fail("Unexpected TypeModifierPragma");
3072            return env;
3073        }
3074    
3075        /**
3076         * This may be called more than once on a Type t.
3077         */
3078        //@ requires t != null;
3079        protected Env checkTypeModifiers(Env env, Type t) {
3080            // don't know context for type, so pull it out of the type's decorations.
3081            if (env == null) {
3082                env = (Env)Env.typeEnv.get(t);
3083            }        
3084            Assert.notFalse(env != null);  //@ nowarn Pre;
3085            checkTypeModifierPragmaVec(t.tmodifiers, t, env);
3086            if (t instanceof ArrayType) {
3087                env = checkTypeModifiers(env, ((ArrayType)t).elemType);
3088            }
3089            return env;
3090        }
3091    
3092        //alx: dw needs overriding method
3093        //no assumptions on the parameter, TODO: what does that method
3094        protected boolean isPure(RoutineDecl rd) {
3095                return false;
3096        }
3097        //alx-end
3098        
3099        //alx: dw TODO what does that method
3100        protected static int universeTypeCombiner(int l, int r) {
3101                switch (l) {
3102                case TagConstants.THISEXPR:        //dw: special case for l=peer=this
3103                {
3104                        return r;
3105                }
3106                case TagConstants.PEER:
3107                case TagConstants.IMPL_PEER:
3108                {
3109                        if (r==TagConstants.PEER || r==TagConstants.IMPL_PEER)
3110                        return TagConstants.PEER;
3111                        return TagConstants.READONLY;
3112                }
3113                case TagConstants.REP:
3114                {
3115                        if (r==TagConstants.PEER || r==TagConstants.IMPL_PEER)
3116                        return TagConstants.REP;
3117                        return TagConstants.READONLY;
3118                }
3119                case TagConstants.READONLY:
3120                {
3121                        return TagConstants.READONLY;
3122                }
3123                }
3124                
3125                return 0;
3126        }
3127        //alx-end
3128        
3129        //alx: dw TODO: what does the method
3130        protected static int universeTypeCombiner(/*@ non_null @*/ ASTNode left, 
3131                                                  /*@ non_null @*/ ASTNode right) {
3132                return universeTypeCombiner(ParseUtil.getUniverse(left),
3133                                        ParseUtil.getUniverse(right)); 
3134        }
3135        //alx-end
3136        
3137        //alx: dw TODO: what does the method
3138        protected void checkNoRepInStaticContext(/*@ non_null @*/ ASTNode n) {
3139                if (inStatic && ParseUtil.getUniverse(n)==TagConstants.REP)
3140                ErrorSet.error(n.getStartLoc(),
3141                               "usage of rep not allowed in static contexts");
3142        }
3143        //alx-end
3144        
3145        
3146        //alx: dw TODO: what does the method
3147        protected void checkUniverseForField(/*@ non_null @*/ GenericVarDecl gvd) {
3148                int mod=ParseUtil.getUniverse(gvd);
3149                if (mod!=0 && Modifiers.isStatic(gvd.modifiers) && 
3150                mod!=TagConstants.READONLY) {
3151                if (mod==TagConstants.REP)
3152                    ErrorSet.error(gvd.getStartLoc(),
3153                                   "static fields cannot be of universe type rep");
3154                if (!impl_peerInStaticCautionThrown && 
3155                    mod==TagConstants.IMPL_PEER) {
3156                    ErrorSet.caution(gvd.getStartLoc(),
3157                                     "using 'implicit peer' as default for "+
3158                                     "static fields, but should be readonly");
3159                    impl_peerInStaticCautionThrown=true;
3160                }
3161                }
3162        }
3163        //alx-end
3164        
3165        //alx: dw TODO: where is it used?
3166        boolean impl_peerInStaticCautionThrown = false;
3167        //alx-end
3168        
3169        //alx: dw TODO whad does the method?
3170        public static void copyUniverses(/*@ non_null @*/ ASTNode dest,
3171                                         /*@ non_null @*/ ASTNode source) {
3172                int r = ParseUtil.getUniverse(source);
3173                if (r!=0) {
3174                ParseUtil.setUniverse(dest,r);
3175                int e = ParseUtil.getElementUniverse(source);
3176                if (e!=0)
3177                    ParseUtil.setElementUniverse(dest,e);
3178                }
3179        }
3180        //alx-end
3181        
3182        
3183        //alx: dw the first common supertype (used for array inits and ?: )
3184        //TODO: what are the specs here?
3185        public static int leastUpperUniverseBound(int l, int r) {
3186                if (l==TagConstants.THISEXPR || l==TagConstants.IMPL_PEER)
3187                l=TagConstants.PEER;
3188                if (r==TagConstants.THISEXPR || r==TagConstants.IMPL_PEER)
3189                r=TagConstants.PEER;
3190                
3191                if (l==r)
3192                return r;
3193                else if (l==TagConstants.NULLLIT)
3194                return r;
3195                else if (r==TagConstants.NULLLIT)
3196                return l;
3197                else
3198                return TagConstants.READONLY;
3199        }
3200        //alx-end
3201        
3202        
3203        //alx: dw determine & set universe type of field access by applying 
3204        //        universeTypeCombiner. fa.od must not be null!!!
3205        //TODO: is the spec OK?
3206        public static void determineUniverseForFieldAccess(
3207                                        /*@ non_null @*/ FieldAccess fa) {
3208                //if target has no universe modifier, set it to impl_peer
3209                if (fa.od!=null && ParseUtil.getUniverse(fa.od)==0)
3210                ParseUtil.setUniverse(fa.od,TagConstants.IMPL_PEER);
3211                //if decl has no universe modifier, set to default
3212                if (!(fa.decl.type instanceof PrimitiveType) && 
3213                ParseUtil.getUniverse(fa.decl)==0)
3214                ParseUtil.setUniverse(fa.decl,
3215                                      new int[] {0,0},
3216                                      fa.decl.type,
3217                                      Location.NULL);
3218                //use universeTypeCombiner
3219                if (ParseUtil.getUniverse(fa.decl)!=0) {
3220                ParseUtil.setUniverse(fa,universeTypeCombiner(fa.od,fa.decl));
3221                if (ParseUtil.getElementUniverse(fa.decl)!=0)
3222                    ParseUtil.setElementUniverse(fa, 
3223                                        ParseUtil.getElementUniverse(fa.decl));
3224                }
3225        }
3226        //alx-end
3227        
3228        //alx: dw TODO what does the method?
3229        public void determineUniverseForMethodInvocation(
3230                                        /*@ non_null @*/ MethodInvocation mi) {
3231                //if target has no universe modifier, set it to impl_peer
3232                if (mi.od!=null && ParseUtil.getUniverse(mi.od)==0)
3233                ParseUtil.setUniverse(mi.od,TagConstants.IMPL_PEER);
3234                int od = ParseUtil.getUniverse(mi.od);
3235                //if decl has no universe modifier, set to default
3236                if (!(mi.decl.returnType instanceof PrimitiveType) && 
3237                ParseUtil.getUniverse(mi.decl)==0)
3238                  ParseUtil.setUniverse(mi.decl,
3239                                        new int[] {0,0},
3240                                        mi.decl.returnType,
3241                                        Location.NULL);
3242                //use universeTypeCombiner
3243                if (ParseUtil.getUniverse(mi.decl)!=0) { 
3244                ParseUtil.setUniverse(mi,universeTypeCombiner(mi.od,mi.decl));
3245                if (ParseUtil.getElementUniverse(mi.decl)!=0)
3246                    ParseUtil.setElementUniverse(mi,
3247                                        ParseUtil.getElementUniverse(mi.decl));
3248                       
3249                }
3250                boolean isPureMeth=isPure(mi.decl);
3251                if (od==TagConstants.READONLY && !isPureMeth)
3252                ErrorSet.error(mi.getStartLoc(),
3253                       "only pure methods can be called on readonly targets");
3254                boolean repIsError = od!=TagConstants.THISEXPR;
3255                for (int i = 0; i<mi.args.size(); i++) {
3256                int decl_universe_arg;
3257                FormalParaDecl decl_arg=mi.decl.args.elementAt(i);
3258                if (decl_arg.type instanceof PrimitiveType)
3259                    continue;
3260                Expr actual_arg=mi.args.elementAt(i);
3261                if (ParseUtil.getUniverse(decl_arg)==0 && !isPureMeth)
3262                    ParseUtil.setUniverse(decl_arg,
3263                                          new int[] {0,0},
3264                                          decl_arg.type,
3265                                          Location.NULL);
3266                else if (isPureMeth) {
3267                    decl_universe_arg = ParseUtil.getUniverse(decl_arg);
3268                    if (decl_universe_arg!=TagConstants.READONLY) {
3269                        if (decl_universe_arg!=TagConstants.IMPL_PEER && 
3270                            decl_universe_arg!=0)
3271                            ErrorSet.error(decl_arg.getStartLoc(),
3272                                 "parameters of pure methods have to be readonly");
3273                        ParseUtil.setUniverse(decl_arg,TagConstants.READONLY);
3274                    }
3275                }
3276                decl_universe_arg = ParseUtil.getUniverse(decl_arg);
3277                //if the target is rep and a method is defined as foo(peer T x), 
3278                //then the actual argument has to be 
3279                // rep T. (universeTypeCombiner: rep*peer=rep)
3280                if (od==TagConstants.REP && 
3281                    (decl_universe_arg==TagConstants.PEER || 
3282                     decl_universe_arg==TagConstants.IMPL_PEER)) {
3283                    if (ParseUtil.getUniverse(actual_arg)!=TagConstants.REP)
3284                        ErrorSet.error(actual_arg.getStartLoc(),
3285                                       "the argument has to be rep: rep*peer=rep");
3286                }
3287                else {
3288                    checkUniverseAssignability(decl_arg,actual_arg);
3289                    if (repIsError && decl_universe_arg==TagConstants.REP) {
3290                        ErrorSet.error(mi.getStartLoc(),
3291                                       "methods with rep arguments can only be "+
3292                                       "called on target this");
3293                        repIsError=false;
3294                    }
3295                }
3296                }
3297        }
3298        //alx-end
3299        
3300        //alx: dw TODO what does the method
3301        public static void determineUniverseForArrayRefExpr(
3302                                  /*@ non_null @*/ ArrayRefExpr r) {
3303                ParseUtil.setUniverse(r,universeTypeCombiner(
3304                           ParseUtil.getUniverse(r.array),
3305                           ParseUtil.getElementUniverse(r.array)));
3306        }
3307        //alx-end
3308    }
3309    
3310    /*
3311     * Local Variables:
3312     * Mode: Java
3313     * fill-column: 85
3314     * End:
3315     */