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 }