    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     */