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