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    }