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 }