    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003    package escjava.sp;
    004
    005    import javafe.ast.*;
    006    import escjava.ast.*;
    007    import escjava.ast.Modifiers;
    008    import escjava.ast.TagConstants;
    009    import escjava.translate.GC;
    010    import escjava.translate.Substitute;
    011
    012    import javafe.util.Location;
    013    import javafe.util.Assert;
    014
    015    import java.util.Hashtable;
    016    import java.util.Enumeration;
    017
    018    public class VarMap
    019    {
    020        /**
    021         * Clients should construct new "base" VarMap's only by calling
    022         * identity() or bottom().
    023         */
    024
    025        private VarMap() {
    026        }
    027
    028        /*@ spec_public */ private Hashtable table;
    029        /*+@ invariant table != null ==>
    030         table.keyType == \type(GenericVarDecl) &&
    031         table.elementType == \type(Expr); */
    032
    033        //@ spec_public
    034        final private static VarMap botMap = new VarMap();
    035        //@ invariant botMap.table == null;
    036        //@ invariant this == botMap || this.table != null;
    037
    038        //@ spec_public
    039        final private static VarMap idMap = new VarMap();
    040        //@ invariant botMap != idMap;
    041
    042        static {
    043            idMap.table = new Hashtable();
    044        }
    045
    046        /** Returns the special "bottom" VarMap. */
    047
    048        //@ ensures \result != null;
    049        //@ ensures \result.table == null;
    050        public static VarMap bottom() {
    051            return botMap;
    052        }
    053
    054        //@ ensures \result == (table == null);
    055        public boolean isBottom() {
    056            return table == null;
    057        }
    058
    059        /** Returns the identity VarMap. */
    060
    061        //@ ensures \result != null;
    062        //@ ensures \result.table != null;
    063        public static VarMap identity() {
    064            return idMap;
    065        }
    066
    067        /** Returns a VarMap identical to "this", except mapping "v" to "e". */
    068
    069        //@ ensures \result != null;
    070        //@ ensures table != null ==> \result.table != null;
    071        public VarMap extend(/*@ non_null */ GenericVarDecl v,
    072                             /*@ non_null */ Expr e) {
    073            if (this == botMap) return botMap;
    074            VarMap r = new VarMap();
    075            r.table = (Hashtable)table.clone();
    076            //+@ assume r.table.keyType == table.keyType;
    077            //+@ assume r.table.elementType == table.elementType;
    078            r.table.put(v,e);
    079            return r;
    080        }
    081
    082        /**
    083         * Returns a VarMap identical to "this", except mapping "v" to "e"
    084         * for every pair <v,e> in the hashtable h.
    085         */
    086
    087        //+@ requires table != null ==> table.keyType <: h.keyType;
    088        //+@ requires table != null ==> h.elementType <: table.elementType;
    089        //@ ensures \result != null;
    090        //@ ensures table != null ==> \result.table != null;
    091        public VarMap extend(/*@ non_null */ Hashtable h) {
    092            if (this == botMap) return botMap;
    093            VarMap r = new VarMap();
    094            r.table = (Hashtable)table.clone();
    095            //+@ assume r.table.keyType == table.keyType;
    096            //+@ assume r.table.elementType == table.elementType;
    097            for( Enumeration e = h.keys(); e.hasMoreElements(); ) {
    098                GenericVarDecl v = (GenericVarDecl)e.nextElement();
    099                r.table.put(v, h.get(v));
    100            }
    101            return r;
    102        }
    103
    104        /**
    105         * Returns a VarMap identical to "this", except mapping each
    106         * element of "vec" to itself.
    107         */
    108
    109        //@ ensures \result != null;
    110        //@ ensures table != null ==> \result.table != null;
    111        public VarMap unmap (/*@ non_null */ GenericVarDeclVec vec) {
    112            if (this == botMap) return botMap;
    113            VarMap r = new VarMap();
    114            r.table = (Hashtable)table.clone();
    115            //+@ assume r.table.keyType == table.keyType;
    116            //+@ assume r.table.elementType == table.elementType;
    117            for (int i = 0; i < vec.size(); i++)
    118                r.table.remove(vec.elementAt(i));
    119            return r;
    120        }
    121
    122        public Expr get(/*@ non_null */ GenericVarDecl v) {
    123            return (Expr) table.get(v);
    124        }
    125
    126        /**
    127         * This is the two-input-map version of the more general
    128         * <code>merge</code> method below.<p>
    129         */
    130
    131        //@ requires rename.length == 2;
    132        //@ requires \typeof(rename) == \type(GuardedCmdVec[]);
    133        /*+@ requires lastVarUse != null ==>
    134         lastVarUse.keyType == \type(GenericVarDecl) &&
    135         lastVarUse.elementType == \type(RefInt); */
    136        //@ ensures \result != null;
    137        //@ ensures m.table != null || n.table != null ==> \result.table != null;
    138        static VarMap merge(/*@ non_null */ VarMap m, /*@ non_null */ VarMap n,
    139                            /*@ non_null */ GuardedCmdVec[] rename, int loc,
    140                            int p, Hashtable lastVarUse){
    141            VarMap[] mm = {m, n};
    142            return merge(mm, rename, loc, p, lastVarUse);
    143        }
    144
    145        /**
    146         * If all elements of "mm" are "bottom" then the result is
    147         * "bottom".  Otherwise, the result is a map whose domain is the
    148         * union of the domains of the elements of "mm", restricted to
    149         * those variables whose "lastVarUse" value is at least "p" (if a
    150         * variable is not in the domain of "lastVarUse", its "lastVarUse"
    151         * value is considered to be negative infinity).  For each
    152         * variable "v" in the domain of the output map: <ul> <li> if all
    153         * non-"bottom" elements of "mm" map "v" to the same expression,
    154         * then the output map also maps "v" to that expression; <li>
    155         * otherwise, the output map maps "v" to a fresh variable "v'"
    156         * (where the print name of "v'" is appropriately chosen given "v"
    157         * and "loc"), and for each non-"bottom" "mm[i]", "rename[i]"
    158         * includes "assume v' == mm[i][[v]]".  </ul>
    159         *
    160         * Parameter <code>lastVarUse</code> may be passed in as
    161         * <code>null</code>, in which case the method acts as if
    162         * <code>lastVarUse</code> had been a hashtable that maps every
    163         * variable to max infinity.
    164         */
    165
    166        //@ requires \nonnullelements(mm);
    167        //@ requires mm.length == rename.length;
    168        //@ requires \typeof(mm) == \type(VarMap[]);
    169        //@ requires \typeof(rename) == \type(GuardedCmdVec[]);
    170        /*+@ requires lastVarUse != null ==>
    171         lastVarUse.keyType == \type(GenericVarDecl) &&
    172         lastVarUse.elementType == \type(RefInt); */
    173        //@ ensures \result != null;
    174        /*@ ensures (\exists int i; 0 <= i && i < mm.length && mm[i].table != null)
    175         ==> \result.table != null; */
    176        //@ modifies rename[*];
    177        //@ ensures \nonnullelements(rename);
    178        static VarMap merge(VarMap[] mm, /*@ non_null */ GuardedCmdVec[] rename, int loc,
    179                            int p, Hashtable lastVarUse){
    180            //
    181            // The following should be ok, but code currently crashes because this
    182            // precondition is not respected:
    183            //
    184            //  Assert.notFalse(loc != Location.NULL);      !!!!
    185
    186            Hashtable vars = new Hashtable();
    187            boolean nonBottom = false;
    188            for( int i=0; i<mm.length; i++) {
    189                rename[i] = GuardedCmdVec.make();
    190                if( mm[i].table != null ) {
    191                    nonBottom = true;
    192                    for( Enumeration e = mm[i].table.keys(); e.hasMoreElements(); ) {
    193                        GenericVarDecl var = (GenericVarDecl)e.nextElement();
    194                        boolean putIt;
    195                        if (lastVarUse != null) {
    196                            RefInt lastUse = (RefInt)lastVarUse.get(var);
    197                            putIt = lastUse != null && p <= lastUse.value;
    198                        } else {
    199                            putIt = true;
    200                        }
    201                        if (putIt) {
    202                            vars.put(var, mm[i].table.get(var));
    203                        }
    204                    }
    205                }
    206            }
    207
    208            if (!nonBottom) return botMap;
    209
    210            VarMap r = new VarMap();
    211            r.table = new Hashtable();
    212
    213            for( Enumeration e = vars.keys(); e.hasMoreElements(); ) {
    214                GenericVarDecl var = (GenericVarDecl)e.nextElement();
    215                Expr expr = (Expr)vars.get(var);
    216                boolean conflict = false;
    217                for( int i=0; i<mm.length; i++) {
    218                    if( mm[i].table != null ) {
    219                        Expr mapto = (Expr)mm[i].table.get(var);
    220                        if (expr != mapto) {
    221                            conflict = true;
    222                            break;
    223                        }
    224                    }
    225                }
    226
    227                if (conflict) {
    228                    int uloc = loc;
    229                    if (uloc==Location.NULL)
    230                        uloc = var.locId;
    231
    232                    LocalVarDecl varPrime
    233                        = LocalVarDecl.make( Modifiers.NONE,
    234                                             null,
    235                                             var.id,
    236                                             var.type,
    237                                             uloc,
    238                                             null, Location.NULL );
    239                    VariableAccess varPrimeRef = VariableAccess.make( var.id, loc,
    240                                                                      varPrime );
    241                    VariableAccess varRef = VariableAccess.make( var.id, loc, var );
    242
    243                    for( int i=0; i<mm.length; i++) {
    244                        if( mm[i].table != null ) {
    245                            Expr mapto = (Expr)mm[i].table.get(var);
    246                            if (mapto == null)
    247                                mapto = varRef;
    248                            rename[i].addElement(GC.assume(GC.nary(TagConstants.ANYEQ,
    249                                                                   varPrimeRef, mapto)));
    250                        }
    251                    }
    252                    r.table.put(var,varPrimeRef);
    253                } else {
    254                    r.table.put(var, expr);
    255                }
    256            }
    257
    258            return r;
    259
    260        }
    261
    262        /**
    263         * Returns the result of applying "this", viewed as a
    264         * substituiton, to "e".
    265         */
    266
    267        //@ requires table != null;
    268        //@ ensures \result != null;
    269        public Expr apply(/*@ non_null */ Expr e){
    270            return GC.subst(Location.NULL, Location.NULL, table, e) ;
    271        }
    272    }