001    /* Copyright 2000, 2001, Compaq Computer Corporation */
002    
003    package javafe.tc;
004    
005    import java.io.ByteArrayOutputStream;
006    import javafe.ast.*;
007    import javafe.tc.TagConstants;
008    import javafe.util.Assert;
009    import javafe.util.Location;
010    
011    public class Types
012    {
013        /**
014         * Types uses the inst pattern to allow subclasses to provide alternative
015         * implementations of some of the static methods here.
016         */
017        static public /*@ non_null */ Types inst;
018    
019        static {
020            inst = new Types();
021        }
022      
023        /**
024         * Factory method for TypeSig structures
025         */
026        //@ requires !(enclosingEnv instanceof EnvForCU);
027        //@ ensures \result != null;
028        public static TypeSig makeTypeSig(String simpleName,
029                                          /*@ non_null */ Env enclosingEnv,
030                                          /*@ non_null */ TypeDecl decl) {
031            return inst.makeTypeSigInstance(simpleName,
032                                            enclosingEnv,
033                                            decl);
034        }
035      
036        //@ requires !(enclosingEnv instanceof EnvForCU);
037        //@ ensures \result != null;
038        protected TypeSig makeTypeSigInstance(String simpleName,
039                                              /*@ non_null */ Env enclosingEnv,
040                                              /*@ non_null */ TypeDecl decl) {
041            return new javafe.tc.TypeSig(simpleName,
042                                         enclosingEnv,
043                                         decl);
044        }
045    
046        /**
047         * Factory method for TypeSig structures
048         */
049        //@ requires \nonnullelements(packageName);
050        //@ requires (enclosingType != null) ==> (decl != null);
051        //@ requires (decl==null) == (CU==null);
052        //@ ensures \result != null;
053        protected static TypeSig makeTypeSig(String[] packageName,
054                                             /*@ non_null */ String simpleName,
055                                             TypeSig enclosingType,
056                                             TypeDecl decl, 
057                                             CompilationUnit CU) {
058            return inst.makeTypeSigInstance(packageName,
059                                            simpleName,
060                                            enclosingType,
061                                            decl, 
062                                            CU);
063        }
064        
065        //@ requires \nonnullelements(packageName);
066        //@ requires (enclosingType != null) ==> (decl != null);
067        //@ requires (decl==null) == (CU==null);
068        //@ ensures \result != null;
069        protected TypeSig makeTypeSigInstance(String[] packageName,
070                                              /*@ non_null */ String simpleName,
071                                              TypeSig enclosingType,
072                                              TypeDecl decl, 
073                                              CompilationUnit CU) {
074            return new javafe.tc.TypeSig(packageName,
075                                         simpleName,
076                                         enclosingType,
077                                         decl, 
078                                         CU);
079        }
080      
081        // ----------------------------------------------------------------------
082        // Hidden constructor
083    
084        public Types() {}
085    
086        /** Used to indicate the type of an illegal operation, so that error messages do
087         * not unnecessarily propagate; should only be used if the error has already been
088         * reported.
089         */
090        //@ invariant errorType != null;
091        public static Type errorType = ErrorType.make();
092    
093        // ----------------------------------------------------------------------
094        // Fields for primitive types
095    
096        /*@ requires (tag == TagConstants.BOOLEANTYPE || tag == TagConstants.INTTYPE
097         || tag == TagConstants.LONGTYPE || tag == TagConstants.CHARTYPE
098         || tag == TagConstants.FLOATTYPE || tag == TagConstants.DOUBLETYPE
099         || tag == TagConstants.VOIDTYPE || tag == TagConstants.NULLTYPE
100         || tag == TagConstants.BYTETYPE || tag == TagConstants.SHORTTYPE); */
101        //@ ensures \result != null;
102        private static final PrimitiveType makePrimitiveType(int tag) {
103            return PrimitiveType.makeNonSyntax(tag);
104        }
105    
106        //@ invariant voidType != null;
107        public static PrimitiveType 
108                voidType = makePrimitiveType( TagConstants.VOIDTYPE );
109    
110        //@ invariant booleanType != null;
111        public static PrimitiveType
112                booleanType = makePrimitiveType( TagConstants.BOOLEANTYPE );
113    
114        //@ invariant intType != null;
115        public static PrimitiveType
116                intType = makePrimitiveType( TagConstants.INTTYPE );
117    
118        //@ invariant doubleType != null;
119        public static PrimitiveType
120                doubleType = makePrimitiveType( TagConstants.DOUBLETYPE );
121    
122        //@ invariant floatType != null;
123        public static PrimitiveType
124                floatType = makePrimitiveType( TagConstants.FLOATTYPE );
125    
126        //@ invariant longType != null;
127        public static PrimitiveType
128                longType = makePrimitiveType( TagConstants.LONGTYPE );
129    
130        //@ invariant charType != null;
131        public static PrimitiveType
132                charType = makePrimitiveType( TagConstants.CHARTYPE );
133    
134        //@ invariant nullType != null;
135        public static PrimitiveType
136                nullType = makePrimitiveType( TagConstants.NULLTYPE );
137    
138        //@ invariant byteType != null;
139        public static PrimitiveType
140                byteType = makePrimitiveType( TagConstants.BYTETYPE );
141    
142        //@ invariant shortType != null;
143        public static PrimitiveType
144                shortType = makePrimitiveType( TagConstants.SHORTTYPE );
145    
146        public static void remakeTypes() {
147                errorType = ErrorType.make();
148                voidType = makePrimitiveType( TagConstants.VOIDTYPE );
149                booleanType = makePrimitiveType( TagConstants.BOOLEANTYPE );
150                intType = makePrimitiveType( TagConstants.INTTYPE );
151                doubleType = makePrimitiveType( TagConstants.DOUBLETYPE );
152                floatType = makePrimitiveType( TagConstants.FLOATTYPE );
153                longType = makePrimitiveType( TagConstants.LONGTYPE );
154                charType = makePrimitiveType( TagConstants.CHARTYPE );
155                nullType = makePrimitiveType( TagConstants.NULLTYPE );
156                byteType = makePrimitiveType( TagConstants.BYTETYPE );
157                shortType = makePrimitiveType( TagConstants.SHORTTYPE );
158    
159            s_javaLangPackage = null;
160            s_javaLangObject = null;
161            s_javaLangError = null;
162            s_javaLangException = null;
163            s_javaLangThrowable = null;
164            s_javaLangString = null;
165            s_javaLangCloneable = null;
166            s_javaLangRuntimeException = null;
167            s_javaLangClass = null;
168            s_javaLangSystem = null;
169        }
170    
171        /***************************************************
172         *                                                 *
173         * Fields for java.lang types:                     *
174         *                                                 *
175         **************************************************/
176    
177        /**
178         * Return the package java.lang as a String[] for use in calling
179         * OutsideEnv.lookup[deferred].
180         */
181        //@ ensures \nonnullelements(\result);
182        public static String[] javaLangPackage() {
183            if (s_javaLangPackage==null) {
184                s_javaLangPackage = new String[2];
185                s_javaLangPackage[0] = "java";
186                s_javaLangPackage[1] = "lang";
187            }
188    
189            return s_javaLangPackage;
190        }
191        //@ invariant s_javaLangPackage==null || \nonnullelements(s_javaLangPackage);
192    
193        //@ spec_public
194        private static String[] s_javaLangPackage = null;
195    
196    
197        /**
198         * Find the TypeSig for the required package-member type
199         * java.lang.T.<p>
200         *
201         * If the type is not found in the classpath, an error message is
202         * reported via ErrorSet and an unloaded TypeSig is returned.<p>
203         *
204         * Precondition: the TypeSig has been initialized.<p>
205         */
206        //@ requires T != null;
207        //@ ensures \result != null;
208        public static TypeSig getJavaLang(String T) {
209            return OutsideEnv.lookupDeferred(javaLangPackage(), T);
210        }
211      
212    
213        /*
214         * NOTE: All of the following javaLangXXX routines require that
215         * TypeSig be properly initialized as a precondition.
216         */
217    
218        //* Returns the TypeSig for java.lang.Object.
219        //@ ensures \result != null;
220        public static TypeSig javaLangObject() {
221            if (s_javaLangObject == null)
222                s_javaLangObject = getJavaLang("Object");
223            return s_javaLangObject;
224        }
225        private static TypeSig s_javaLangObject;
226    
227        //* Returns the TypeSig for java.lang.System.
228        //@ ensures \result != null;
229        public static TypeSig javaLangSystem() {
230            if (s_javaLangSystem == null)
231                s_javaLangSystem = getJavaLang("System");
232            return s_javaLangSystem;
233        }
234        private static TypeSig s_javaLangSystem;
235    
236        //* Returns the TypeSig for java.lang.Error.
237        //@ ensures \result != null;
238        public static TypeSig javaLangError() {
239            if (s_javaLangError == null)
240                s_javaLangError = getJavaLang("Error");
241            return s_javaLangError;
242        }
243        private static TypeSig s_javaLangError;
244    
245        //* Returns the TypeSig for java.lang.Exception.
246        //@ ensures \result != null;
247        public static TypeSig javaLangException() {
248            if (s_javaLangException == null)
249                s_javaLangException = getJavaLang("Exception");
250            return s_javaLangException;
251        }
252        private static TypeSig s_javaLangException;
253    
254        //* Returns the TypeSig for java.lang.Throwable.
255        //@ ensures \result != null;
256        public static TypeSig javaLangThrowable() {
257            if (s_javaLangThrowable == null)
258                s_javaLangThrowable = getJavaLang("Throwable");
259            return s_javaLangThrowable;
260        }
261        private static TypeSig s_javaLangThrowable;
262    
263        //* Returns the TypeSig for java.lang.String.
264        //@ ensures \result != null;
265        public static TypeSig javaLangString() {
266            if (s_javaLangString == null)
267                s_javaLangString = getJavaLang("String");
268            return s_javaLangString;
269        }
270        private static TypeSig s_javaLangString;
271    
272        //* Returns the TypeSig for java.lang.RuntimeException.
273        //@ ensures \result != null;
274        public static TypeSig javaLangRuntimeException() {
275            if (s_javaLangRuntimeException == null)
276                s_javaLangRuntimeException =
277                    getJavaLang("RuntimeException");
278            return s_javaLangRuntimeException;
279        }
280        private static TypeSig s_javaLangRuntimeException;
281    
282        //* Returns the TypeSig for java.lang.Cloneable.
283        //@ ensures \result != null;
284        public static TypeSig javaLangCloneable() {
285            if (s_javaLangCloneable == null)
286                s_javaLangCloneable = getJavaLang("Cloneable");
287            return s_javaLangCloneable;
288        }
289        private static TypeSig s_javaLangCloneable;
290    
291        //* Returns the TypeSig for java.lang.Class
292        //@ ensures \result != null;
293        public static TypeSig javaLangClass() {
294            if (s_javaLangClass == null)
295                s_javaLangClass = getJavaLang("Class");
296            return s_javaLangClass;
297        }
298        private static TypeSig s_javaLangClass;
299    
300    
301        /***************************************************
302         *                                                 *
303         * Predicates on types:                            *
304         *                                                 *
305         **************************************************/
306    
307        public static boolean isErrorType(Type t) {
308            return t instanceof ErrorType;
309        }
310    
311        public static boolean isReferenceType(Type t) {
312            return !(t instanceof PrimitiveType)
313                && !isErrorType(t);
314        }
315    
316        public static boolean isReferenceOrNullType(Type t) {
317            return isReferenceType(t)
318                || t.getTag() == TagConstants.NULLTYPE;
319        }
320    
321        private static boolean isPrimitiveType(Type t, int tag) {
322            return (t instanceof PrimitiveType) && ( ((PrimitiveType)t).tag == tag);
323        }
324    
325        public static boolean isByteType(Type t) {
326            return isPrimitiveType( t, TagConstants.BYTETYPE );
327        }
328    
329        public static boolean isBooleanType(Type t) {
330            return isPrimitiveType( t, TagConstants.BOOLEANTYPE );
331        }
332    
333        public static boolean isShortType(Type t){
334            return isPrimitiveType( t, TagConstants.SHORTTYPE );
335        }
336        public static boolean isCharType(Type t){
337            return isPrimitiveType( t, TagConstants.CHARTYPE );
338        }
339        public static boolean isDoubleType(Type t){
340            return isPrimitiveType( t, TagConstants.DOUBLETYPE );
341        }
342        public static boolean isFloatType(Type t){
343            return isPrimitiveType( t, TagConstants.FLOATTYPE );
344        }
345        public static boolean isIntType(Type t){
346            return isPrimitiveType( t, TagConstants.INTTYPE );
347        }
348        public static boolean isLongType(Type t){
349            return isPrimitiveType( t, TagConstants.LONGTYPE );
350        }
351        public static boolean isVoidType(Type t){
352            return isPrimitiveType( t, TagConstants.VOIDTYPE );
353        }
354      
355        public static boolean isNumericType(Type t){
356            return inst.isNumericTypeInstance(t);
357        }
358        public boolean isNumericTypeInstance(Type t){
359            if( t instanceof PrimitiveType ) {
360                switch( ((PrimitiveType)t).tag ) {
361                    case TagConstants.BYTETYPE: 
362                    case TagConstants.SHORTTYPE: 
363                    case TagConstants.INTTYPE: 
364                    case TagConstants.LONGTYPE: 
365                    case TagConstants.CHARTYPE: 
366                    case TagConstants.FLOATTYPE: 
367                    case TagConstants.DOUBLETYPE: 
368                        return true;
369                    default:
370                        return false;
371                }
372            } else
373                return false;
374        }
375    
376        public static boolean isIntegralType(Type t){
377            return inst.isIntegralTypeInstance(t);
378        }
379        
380        //@ ensures \result ==> t instanceof PrimitiveType;
381        public boolean isIntegralTypeInstance(Type t){
382            if( t instanceof PrimitiveType ) {
383                switch( ((PrimitiveType)t).tag ) {
384                    case TagConstants.BYTETYPE: 
385                    case TagConstants.SHORTTYPE: 
386                    case TagConstants.INTTYPE: 
387                    case TagConstants.LONGTYPE: 
388                    case TagConstants.CHARTYPE: 
389                        return true;
390                    default:
391                        return false;
392                }
393            } else
394                return false;
395        }
396    
397        public static boolean isFloatingPointType(Type t){
398            return inst.isFloatingPointTypeInstance(t);
399        }
400        
401        public boolean isFloatingPointTypeInstance(Type t){
402            if( t instanceof PrimitiveType ) {
403                switch( ((PrimitiveType)t).tag ) {
404    
405                    case TagConstants.FLOATTYPE: 
406                    case TagConstants.DOUBLETYPE: 
407                        return true;
408                    default:
409                        return false;
410                }
411            } else
412                return false;
413        }
414    
415        // ======================================================================
416        // Conversions on Types
417    
418        //@ requires x != null && y != null;
419        /*@ ensures \result ==>
420         (x instanceof PrimitiveType) == (y instanceof PrimitiveType); */
421        public static boolean isSameType( Type x, Type y ) {
422            return inst.isSameTypeInstance(x, y);
423        }
424    
425        //@ requires x != null && y != null;
426        /*@ ensures \result ==>
427         (x instanceof PrimitiveType) == (y instanceof PrimitiveType); */
428        protected boolean isSameTypeInstance( Type x, Type y ) {
429            if( x instanceof TypeName ) x = TypeSig.getSig( (TypeName)x);
430            if( y instanceof TypeName ) y = TypeSig.getSig( (TypeName)y);
431    
432            int xTag = x.getTag();
433            if( xTag != y.getTag() ) return false;
434    
435            switch( xTag ) {
436                case TagConstants.ARRAYTYPE:
437                    return isSameType( ((ArrayType)x).elemType, ((ArrayType)y).elemType );
438                case TagConstants.TYPESIG:
439                    return x==y;
440                default:
441                    // x and y are the same primitive type
442                    return true;
443            }
444        }
445    
446        /** Returns true if and only if <code>x</code> is a subclass or
447         * superinterface of <code>y</code>.  (The occurrence of "class"
448         * in the name of the method is rather unfortunate.)
449         */
450        //@ requires x != null && y != null;
451        //@ ensures \result ==> (x instanceof TypeSig) || (x instanceof TypeName);
452        public static boolean isSubclassOf( Type x, TypeSig y ) {
453        
454            if (x instanceof TypeName)
455                x = TypeSig.getSig( (TypeName)x);
456    
457            Assert.notNull(y);
458    
459            if( x instanceof TypeSig ) {
460                return ((TypeSig)x).isSubtypeOf(y);
461            } else
462                return false;
463        }
464    
465        /** 
466         * Returns true iff <code>x</code> is a superclass or
467         * superinterface of <code>y</code>, or if <code>x</code> is the
468         * same type as <code>y</code>.
469         *
470         * <b>Warning</b>: This is *not* the same as is <code>x</code> a
471         * subtype of <code>y</code>!  It does not consider short below
472         * int.
473         */
474        //@ requires x != null && y != null;
475        public static boolean isSubClassOrEq(/*non_null*/ Type x,
476                                             /*non_null*/ Type y) {
477            if (x instanceof ArrayType && y instanceof ArrayType) {
478                return isSubClassOrEq(((ArrayType)x).elemType, ((ArrayType)y).elemType);
479            }
480    
481            if (x instanceof TypeName)
482                x = TypeSig.getSig((TypeName)x);
483    
484            if (y instanceof TypeName)
485                y = TypeSig.getSig((TypeName)y);
486    
487            if (x instanceof TypeSig && y instanceof TypeSig)
488                return ((TypeSig)x).isSubtypeOf((TypeSig)y);
489            else
490                return isSameType(x, y);
491        }
492    
493    
494        /** Checks if one Type is castable to another.
495         See JLS, P.67.
496         */
497      
498        //@ requires s != null && t != null;
499        public static boolean isCastable( Type s, Type t ) {
500            // Replace TypeNames by corresponding TypeSigs
501            if( s instanceof TypeName ) s = TypeSig.getSig( (TypeName)s);
502            if( t instanceof TypeName ) t = TypeSig.getSig( (TypeName)t);
503            return inst.isCastableInstance(s, t);
504        }
505      
506        //@ requires s != null && t != null;
507        protected boolean isCastableInstance( Type s, Type t ) {
508            Assert.notNull( s );
509            Assert.notNull( t );
510    
511        
512            if( s instanceof PrimitiveType ) 
513            {
514                if( t instanceof PrimitiveType ) {
515                    return isAnyPrimitiveConvertable( (PrimitiveType)s, (PrimitiveType)t );
516                }
517                else if( s.getTag() == TagConstants.NULLTYPE ) {
518                    // a cast from null to a reference type
519                    return true;
520                }
521            }
522            else if( s instanceof TypeSig ) 
523            {
524                TypeSig sSig = (TypeSig)s;
525                TypeDecl sDecl = sSig.getTypeDecl();
526                if( sDecl instanceof ClassDecl ) 
527                {
528                    // s is a class
529                
530                    if( t instanceof TypeSig ) 
531                    {
532                        TypeSig tSig = (TypeSig)t;
533                        TypeDecl tDecl = tSig.getTypeDecl();
534                        if( tDecl instanceof ClassDecl ) 
535                        {
536                            // t is a class
537                            // must be related classes
538                            return tSig.isSubtypeOf( sSig ) 
539                                || sSig.isSubtypeOf( tSig );
540                        } 
541                        else 
542                        {
543                            // t is an interface
544                            // Require s is not final, or s implements t
545                            return !Modifiers.isFinal( sDecl.modifiers )
546                                || sSig.isSubtypeOf( tSig );
547                        }
548                    } 
549                    else if( t instanceof ArrayType ) 
550                    {
551                        // t is an array type, s must be Object
552                        return isSameType( sSig, javaLangObject() );
553                    } 
554                    else
555                    {
556                        // t is a primitive type, s is a class, so not castable
557                        Assert.notFalse( t instanceof PrimitiveType ); //@nowarn Pre;
558                        return false;
559                    }
560                }
561                else 
562                {
563                    // s is an interface
564                    if( t instanceof TypeSig ) 
565                    {
566                        TypeSig tSig = (TypeSig)t;
567                        TypeDecl tDecl = tSig.getTypeDecl();
568                        if( tDecl instanceof ClassDecl ) 
569                        {
570                            // t is a class
571                            // require t is not final, or t implements s
572                            return !Modifiers.isFinal( tDecl.modifiers ) 
573                                || tSig.isSubtypeOf( sSig );
574                        } 
575                        else
576                        {
577                            // t is an interface
578                            // is s and t contain methods with the same signature but
579                            // different return types, then an error occurs
580                            // TO BE DONE
581                            return true;
582                        }
583                    } 
584                    else 
585                    {
586                        // t is a primitive or array type
587                        // MAYBE SHOULD ALLOW CASTING OF CLONEABLE TO ARRAY
588                        Assert.notFalse( t instanceof PrimitiveType  //@ nowarn Pre;
589                                         || t instanceof ArrayType );
590                        return false;
591                    }
592                }
593            } 
594            else if( s instanceof ArrayType ) 
595            {
596                // s is an array
597            
598                Type sElem = ((ArrayType)s).elemType;
599            
600                if( t instanceof TypeSig ) 
601                {
602                    // Must be Object or Cloneable
603                    Type tSig = (TypeSig)t;
604                    return isSameType( tSig, javaLangObject() )
605                        || isSameType( tSig, javaLangCloneable() );
606                }
607                else if( t instanceof ArrayType )
608                {
609                    Type tElem = ((ArrayType)t).elemType;
610                
611                    if( sElem instanceof PrimitiveType 
612                        && tElem instanceof PrimitiveType )
613                    {
614                        // require same element type
615                        return sElem.getTag() == tElem.getTag();
616                    }
617                    else if( !(sElem instanceof PrimitiveType)
618                             && !(tElem instanceof PrimitiveType) )
619                    {
620                        // require elements to be castable
621                        return isCastable( sElem, tElem );
622                    }
623                    else
624                        return false;
625                }
626                else 
627                {
628                    Assert.notFalse( t instanceof PrimitiveType ); //@ nowarn Pre;
629                    return false;
630                }
631            }
632            // Assert.fail("Fall thru2, s="+printName(s)+" t="+t+printName(t));
633            return false;
634        }
635    
636        //@ requires x != null && y != null;
637        public static boolean isInvocationConvertable( Type x, Type y ) {
638            if( x instanceof TypeName ) x = TypeSig.getSig( (TypeName)x);
639            if( y instanceof TypeName ) y = TypeSig.getSig( (TypeName)y);
640            return inst.isInvocationConvertableInstance(x, y);
641        }
642      
643        //@ requires x != null && y != null;
644        protected boolean isInvocationConvertableInstance( Type x, Type y ) {
645            if( isSameType(x,y) ) return true;
646            if( isWideningPrimitiveConvertable(x,y) ) return true;
647            if( isWideningReferenceConvertable(x,y) ) return true;
648            return false;
649        }
650    
651        //@ requires x != null && y != null;
652        protected static boolean isWideningPrimitiveConvertable( Type x, Type y ) {
653            return inst.isWideningPrimitiveConvertableInstance(x,y);
654        }
655            
656        //@ requires x != null && y != null;
657        protected boolean isWideningPrimitiveConvertableInstance( Type x, Type y ) {
658    
659            switch( x.getTag() ) {
660                case TagConstants.BYTETYPE:
661                    switch( y.getTag() ) {
662                        case TagConstants.SHORTTYPE: 
663                        case TagConstants.INTTYPE: case TagConstants.LONGTYPE: 
664                        case TagConstants.FLOATTYPE: case TagConstants.DOUBLETYPE:
665                            return true;
666                        default:
667                            return false;
668                    }
669                case TagConstants.SHORTTYPE: case TagConstants.CHARTYPE:
670                    switch( y.getTag() ) {
671                        case TagConstants.INTTYPE: case TagConstants.LONGTYPE: 
672                        case TagConstants.FLOATTYPE: case TagConstants.DOUBLETYPE:
673                            return true;
674                        default:
675                            return false;
676                    }
677                case TagConstants.INTTYPE:
678                    switch( y.getTag() ) {
679                        case TagConstants.LONGTYPE: 
680                        case TagConstants.FLOATTYPE: case TagConstants.DOUBLETYPE:
681                            return true;
682                        default:
683                            return false;
684                    }
685                case TagConstants.LONGTYPE:
686                    switch( y.getTag() ) {
687                        case TagConstants.FLOATTYPE: case TagConstants.DOUBLETYPE:
688                            return true;
689                        default:
690                            return false;
691                    }
692                case TagConstants.FLOATTYPE:
693                    switch( y.getTag() ) {
694                        case TagConstants.DOUBLETYPE:
695                            return true;
696                        default:
697                            return false;
698                    }
699                default:
700                    return false;
701            }
702        }
703    
704        /** Returns true iff the first argument is convertable to the second
705         *  argument, either through a widening primitive conversion,
706         *  a narrowing primitive conversion, or the identity conversion.
707         */
708    
709        protected static boolean isAnyPrimitiveConvertable( Type x, Type y ) {
710            return true;
711        }
712    
713        //@ requires s != null && t != null;
714        protected static boolean isWideningReferenceConvertable( Type s, Type t ) {
715            return inst.isWideningReferenceConvertableInstance(s, t);
716        }
717    
718        //@ requires s != null && t != null;
719        protected boolean isWideningReferenceConvertableInstance( Type s, Type t ) {
720    
721            if( s instanceof TypeName ) s = TypeSig.getSig( (TypeName)s);
722            if( t instanceof TypeName ) t = TypeSig.getSig( (TypeName)t);
723       
724            if(s instanceof TypeSig 
725               && t instanceof TypeSig 
726               && ((TypeSig)s).isSubtypeOf( (TypeSig)t )) 
727                return true;
728         
729            if( s.getTag() == TagConstants.NULLTYPE &&
730                ( t instanceof TypeSig || t.getTag() == TagConstants.ARRAYTYPE ) )
731                return true;
732         
733            if( s.getTag() == TagConstants.ARRAYTYPE ) {
734                if( t.getTag() == TagConstants.ARRAYTYPE ) {
735                    Type sElem = ((ArrayType)s).elemType;
736                    Type tElem = ((ArrayType)t).elemType;
737            
738                    return isSameType( sElem, tElem )
739                        || isWideningReferenceConvertable(sElem,tElem);
740                } 
741                else if( Types.isSameType( t, javaLangObject() ) ) {
742                    return true;
743                } 
744                else 
745                    return false;
746            }
747        
748            return false;
749        }
750    
751        /** Returns the TypeSig for a Type x, if x denotes a class type,
752         otherwise returns null. */
753    
754        //@ requires x != null;
755        public static TypeSig toClassTypeSig( Type x ) {
756    
757            switch( x.getTag() ) {
758    
759                case TagConstants.TYPENAME:
760                    {
761                        x = TypeSig.getSig( (TypeName)x);
762                        // fall thru
763                    }
764            
765                case TagConstants.TYPESIG:
766                    {
767                        TypeSig tsig = (TypeSig)x;
768                        if( tsig.getTypeDecl() instanceof ClassDecl ) {
769                            return tsig;
770                        } else {
771                            // must be an interface type
772                            return null;
773                        }
774                    }
775            
776                default:
777                    // x is a primitive type or an array type
778                    return null;
779            }
780        }
781      
782        // ----------------------------------------------------------------------
783        // Numeric promotions
784      
785        //@ requires t != null;
786        //@ ensures \result != null;
787        public static Type unaryPromote(Type t) {
788            if( isByteType(t) || isShortType(t) || isCharType(t) )
789                return intType; 
790            else if( isNumericType(t) )
791                return t;
792            else {
793                Assert.fail("Not a numeric type");
794                return null;                // dummy return
795            }
796        }
797    
798        //@ ensures \result != null;
799        public static Type binaryNumericPromotion(Type x, Type y) {
800            Assert.notFalse( isNumericType(x) && isNumericType(y) );        //@ nowarn Pre;
801        
802            if( isDoubleType(x) || isDoubleType(y) )
803                return doubleType;
804            else if( isFloatType(x) || isFloatType(y) )
805                return floatType;
806            else if( isLongType(x) || isLongType(y) )
807                return longType;
808            else
809                return intType;
810        }
811    
812        public static Type baseType(Type t) {
813            if (!(t instanceof ArrayType)) return t;
814            return baseType( ((ArrayType)t).elemType );
815        }
816    
817        public static LiteralExpr zeroEquivalent(Type t) {
818            if (isReferenceType(t)) {
819                return LiteralExpr.make(TagConstants.NULLLIT,null,Location.NULL);
820            } else if (isIntType(t)) {
821                return LiteralExpr.make(TagConstants.INTLIT, new Integer(0), Location.NULL);
822            } else if (isLongType(t)) {
823                return LiteralExpr.make(TagConstants.LONGLIT, new Long(0), Location.NULL);
824            } else if (isBooleanType(t)) {
825                return LiteralExpr.make(TagConstants.BOOLEANLIT, Boolean.FALSE, Location.NULL);
826            } else if (isDoubleType(t)) {
827                return LiteralExpr.make(TagConstants.DOUBLELIT, new Double(0), Location.NULL);
828            } else if (isFloatType(t)) {
829                return LiteralExpr.make(TagConstants.FLOATLIT, new Float(0), Location.NULL);
830            } else if (isShortType(t)) {
831                return LiteralExpr.make(TagConstants.SHORTLIT, new Short((short)0), Location.NULL);
832            } else if (isByteType(t)) {
833                return LiteralExpr.make(TagConstants.BYTELIT, new Byte((byte)0), Location.NULL);
834            } else if (isCharType(t)) {
835                return LiteralExpr.make(TagConstants.CHARLIT, new Character((char)0), Location.NULL);
836            }
837            System.out.println("UNSUPPORTED TYPE - zeroEquivalent " + printName(t));
838            return null;
839        }
840    
841        // ----------------------------------------------------------------------
842        // Miscilaneous operations
843      
844        //@ requires x != null && y != null;
845        public static boolean isSameMethodSig(MethodDecl x, MethodDecl y) {
846            if( x.id != y.id ) return false;
847            return isSameFormalParaDeclVec( x.args, y.args );
848        }
849    
850        //@ requires x != null && y != null;
851        public static boolean 
852                isSameFormalParaDeclVec(FormalParaDeclVec x, FormalParaDeclVec y) {
853          
854            if(x.size() != y.size() ) return false;
855            for( int i=0; i<x.size(); i++ ) 
856                if( !isSameType( x.elementAt(i).type, y.elementAt(i).type ) )
857                    return false;
858            return true;
859        }
860    
861        //@ requires x != null && y != null;
862        //@ requires x.args.count == y.args.count;
863        public static boolean routineMoreSpecific( RoutineDecl x, RoutineDecl y ) {
864    
865            // should check that type containing x is invocation convertable
866            // to type containing y
867        
868            Assert.notFalse( x.args.size() == y.args.size() );
869        
870            for( int i=0; i<x.args.size(); i++ )
871            {
872                if( !isInvocationConvertable(x.args.elementAt(i).type,
873                                             y.args.elementAt(i).type ))
874                    return false;
875            }
876            return true;
877        }
878    
879        // *********************************************************************
880    
881    
882        /**
883         * Is an exception a checked one?
884         */
885        static boolean isCheckedException(/*@ non_null */ Type E) {
886            return !Types.isSubclassOf(E, Types.javaLangRuntimeException())
887                && !Types.isSubclassOf(E, Types.javaLangError());
888        }
889    
890    
891        /**
892         * Is "throws <x>" a valid overriding of "throws <y>"? <p>
893         *
894         * Answer: Each exception E in the list <x> must be either:
895         *    (a) an unchecked exception
896         *    (b) a subtype of some exception in the list <y>
897         */
898        //@ requires x != null && y != null;
899        static boolean isCompatibleRaises( TypeNameVec x, TypeNameVec y) {
900            nextx:
901            for (int i=0; i<x.size(); i++) {
902                TypeSig xsig = TypeSig.getSig(x.elementAt(i));
903    
904                // Check (a):
905                if (!isCheckedException(xsig))
906                    continue;
907    
908                // Check (b):
909                for (int j=0; j<y.size(); j++) {
910                    if (xsig.isSubtypeOf(TypeSig.getSig(y.elementAt(j))))
911                        continue nextx;
912                }
913                //CF: For Houdini uses, disable this check for now
914                return false;
915            }
916    
917            return true;
918        }
919    
920    
921        static boolean isCompatibleAccess( int x, int y ) {
922            if( Modifiers.isPublic(y) && !Modifiers.isPublic(x) ) 
923                return false;
924            if(Modifiers.isProtected(y) && !Modifiers.isPublic(x)
925               && !Modifiers.isProtected(x) ) 
926                return false;
927            if( Modifiers.isPackage(y) && Modifiers.isPrivate(x) ) 
928                return false;
929            return true;
930        }
931    
932        //@ requires args != null;
933        //@ ensures \nonnullelements(\result);
934        public static Type[] getFormalParaTypes( FormalParaDeclVec args ) {
935            Type[] r = new Type[ args.size() ];
936            for( int i=0; i<args.size(); i++ ) 
937                r[i] = args.elementAt(i).type;
938            return r;
939        }
940    
941    
942        /***************************************************
943         *                                                 *
944         * Generating print names for Type(s):             *
945         *                                                 *
946         **************************************************/
947    
948        /**
949         * Returns the name of a <code>Type</code> as a
950         * <code>String</code>.  The resulting name will be fully qualified
951         * if the <code>Type</code> has been name resolved. <p>
952         *
953         * Note: <code>t</code> may safely be null.<p>
954         *
955         * Precondition: <code>PrettyPrint.inst</code> != null <p>
956         */
957        //@ ensures \result != null;
958        public static String printName(Type t) {
959            return inst.printNameInstance(t);
960        }
961    
962        //@ ensures \result != null;
963        protected String printNameInstance(Type t) {
964            if (t instanceof TypeName) {
965                TypeSig sig = TypeSig.getRawSig((TypeName)t);
966                if (sig != null)
967                    return sig.toString();
968            } else if (t instanceof ArrayType)
969                return printName(((ArrayType)t).elemType) + "[]";
970    
971            ByteArrayOutputStream result = new ByteArrayOutputStream(20);
972            javafe.ast.PrettyPrint.inst.print(result, t);
973            return result.toString();
974        }
975    
976        /**
977         * Formats an array of <code>Type</code>s as a <code>String</code>
978         * containing a parenthesized list of user-readable names.  The
979         * resulting names  will be fully qualified if the
980         * <code>Type</code>s have been name resolved.  <p>
981         *
982         * Sample output: "(int, javafe.tc.TypeSig, char[])" <p>
983         *
984         * Precondition: <code>PrettyPrint.inst</code> != null,
985         *                <code>ts</code> != null <p>
986         */
987        //@ requires ts != null;
988        public static String printName(Type[] ts) {
989            StringBuffer s = new StringBuffer("(");
990    
991            for (int i=0; i<ts.length; i++ ) {
992                if (i != 0)
993                    s.append(", ");
994                s.append(printName(ts[i]));
995            }
996    
997            s.append(")");
998            return s.toString();
999        }
1000      
1001      
1002        // ======================================================================
1003      
1004        protected static Identifier lenId = Identifier.intern("length");
1005      
1006        //@ invariant lengthFieldDecl.id == lenId;
1007        public static /*@ non_null */ FieldDecl lengthFieldDecl
1008                = FieldDecl.make(Modifiers.ACC_PUBLIC|Modifiers.ACC_FINAL,
1009                                 null,
1010                                 lenId,
1011                                 Types.intType,
1012                                 Location.NULL,  // ERROR!!
1013                                 null,
1014                                 Location.NULL);
1015      
1016    
1017    
1018        //@ requires t != null && caller != null;
1019        //@ ensures \result != null;
1020        //@ ensures \result.id == id;
1021        public static FieldDecl lookupField(Type t, Identifier id, TypeSig caller) 
1022                throws LookupException
1023        {
1024            return inst.lookupFieldInstance(t, id, caller);
1025        }
1026    
1027        //@ requires t != null && caller != null;
1028        //@ ensures \result != null;
1029        //@ ensures \result.id == id;
1030        protected FieldDecl lookupFieldInstance(Type t, Identifier id, TypeSig caller) 
1031                throws LookupException
1032        {
1033            Assert.notNull(t);
1034            
1035            if( t instanceof TypeName)
1036                t = TypeSig.getSig( (TypeName) t );
1037            
1038            if( t instanceof TypeSig) {
1039                return ((TypeSig)t).lookupField(id, caller );
1040            } else  if( t instanceof ArrayType ) {
1041                if( id == lenId ) 
1042                    return lengthFieldDecl;
1043                else
1044                    // Arrays inherit all fields from java.lang.Object:
1045                    return javaLangObject().lookupField(id, caller);
1046            } else if( t instanceof PrimitiveType || isErrorType(t) ) {
1047                throw new LookupException( LookupException.NOTFOUND );
1048            } else {
1049                Assert.fail("Unexpected type "+ t + "(" + t.getTag() + "), " + TagConstants.toString(t.getTag()));
1050                return null;
1051            }
1052        }
1053      
1054        //@ requires \nonnullelements(args) && caller != null;
1055        //@ ensures \result != null;
1056        //@ ensures \result.id == id;
1057        public static MethodDecl lookupMethod(Type t, Identifier id, 
1058                                              Type[] args, TypeSig caller ) 
1059                throws LookupException
1060        {
1061            return inst.lookupMethodInstance(t, id, args, caller);
1062        }
1063    
1064        //@ requires \nonnullelements(args) && caller != null;
1065        //@ ensures \result != null;
1066        //@ ensures \result.id == id;
1067        protected MethodDecl lookupMethodInstance(Type t, Identifier id, 
1068                                                  Type[] args, TypeSig caller ) 
1069                throws LookupException
1070        {
1071            // Convert TypeName's to their corresponding TypeSig:
1072            if (t instanceof TypeName)
1073                t = TypeSig.getSig( (TypeName) t );
1074    
1075            // All array methods are methods of java.lang.Object:
1076            if (t instanceof ArrayType)
1077                t = javaLangObject();
1078    
1079    
1080            // Remaining cases: TypeSig, PrimitiveType, <unknown>
1081            if (t instanceof TypeSig)
1082                return ((TypeSig)t).lookupMethod(id, args, caller );
1083    
1084            if (!(t instanceof PrimitiveType) && !isErrorType(t))
1085                Assert.fail("Unexpected type: "+t);
1086    
1087            throw new LookupException( LookupException.NOTFOUND );
1088        }
1089    } // end of class Types
1090    
1091    /*
1092     * Local Variables:
1093     * Mode: Java
1094     * fill-column: 85
1095     * End:
1096     */