001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package escjava.sp; 004 005 006 import javafe.ast.*; 007 import escjava.ast.*; 008 import escjava.ast.TagConstants; 009 010 import escjava.translate.GC; 011 import escjava.translate.UniqName; 012 import escjava.translate.Substitute; 013 014 import escjava.Main; 015 016 import javafe.util.Location; 017 import javafe.util.Assert; 018 import javafe.util.Set; 019 020 import java.util.Hashtable; 021 import java.util.Enumeration; 022 023 024 public class DSA { 025 026 public static GuardedCmd dsa(/*@ non_null */ GuardedCmd g) { 027 VarMapPair out = new VarMapPair(); 028 return dsa( g, out ); 029 } 030 031 public static GuardedCmd dsa(/*@ non_null */ GuardedCmd g, VarMapPair out) { 032 RefInt preOrderCount; 033 Hashtable lastVarUse; 034 if (Main.options().lastVarUseOpt) { 035 preOrderCount = new RefInt(0); 036 lastVarUse = new Hashtable(); // mapping GenericVarDecl to RefInt 037 //+@ set lastVarUse.keyType = \type(GenericVarDecl); 038 //+@ set lastVarUse.elementType = \type(RefInt); 039 computeLastVarUses(g, preOrderCount, lastVarUse); 040 // reset the pre-order count 041 preOrderCount.value = 0; 042 } else { 043 preOrderCount = null; 044 lastVarUse = null; 045 } 046 return dsa(g, VarMap.identity(), out, "", preOrderCount, lastVarUse); 047 } 048 049 /** Parameters <code>preOrderCount</code> and <code>lastVarUse</code> 050 * are used to perform a dead-variable analysis on variables, so that 051 * merges of variables can be smaller. These parameters should either 052 * both be non-<code>null</code> or both be <code>null</code>. If 053 * they are <code>null</code>, the dead-variable analysis and optimization 054 * will not be performed. 055 **/ 056 057 //@ requires (preOrderCount == null) == (lastVarUse == null); 058 /*+@ requires lastVarUse != null ==> 059 lastVarUse.keyType == \type(GenericVarDecl) && 060 lastVarUse.elementType == \type(RefInt); */ 061 //@ modifies out.n, out.x; 062 //@ ensures out.n != null && out.x != null; 063 private static GuardedCmd dsa(/*@ non_null */ GuardedCmd g, 064 /*@ non_null */ VarMap map, 065 /*@ non_null */ VarMapPair out, 066 String dynInstPrefix, 067 RefInt preOrderCount, 068 Hashtable lastVarUse) { 069 if (map.isBottom()) { 070 if (preOrderCount != null) { 071 // Note that we must still update "preOrderCount" appropriately. 072 doPreOrderCount(g, preOrderCount); 073 } 074 out.n = map; 075 out.x = map; 076 return GC.skip(); 077 } 078 079 if (preOrderCount != null) { 080 preOrderCount.value++; 081 } 082 083 switch (g.getTag()) { 084 case TagConstants.SKIPCMD: 085 /* dsa[[ Skip, M ]] == 086 Skip, M, bottom 087 */ 088 out.n = map; 089 out.x = VarMap.bottom(); 090 return g; 091 092 case TagConstants.RAISECMD: 093 /* dsa[[ Raise, M ]] == 094 Raise, bottom, M 095 */ 096 out.n = VarMap.bottom(); 097 out.x = map; 098 return g; 099 100 case TagConstants.LOOPCMD: 101 // "dsa" only cares about the desugared form a loop. 102 { 103 LoopCmd lp= (LoopCmd)g; 104 return dsa(lp.desugared, map, out, dynInstPrefix, preOrderCount, lastVarUse); 105 } 106 107 case TagConstants.CALL: 108 // "dsa" only cares about the desugared form a call. 109 { 110 Call call= (Call)g; 111 return dsa(call.desugared, map, out, dynInstPrefix, preOrderCount, lastVarUse ); 112 } 113 114 case TagConstants.ASSERTCMD: 115 /* dsa[[ Assert x, M ]] == 116 Assert M[[e]], M, bottom 117 */ 118 { 119 ExprCmd ec = (ExprCmd)g; 120 out.n = map; 121 out.x = VarMap.bottom(); 122 return ExprCmd.make(TagConstants.ASSERTCMD, 123 map.apply(ec.pred), ec.loc); 124 } 125 126 case TagConstants.ASSUMECMD: 127 /* dsa[[ Assume x, M ]] == 128 Assume M[[e]], M, bottom 129 */ 130 { 131 ExprCmd ec = (ExprCmd)g; 132 out.n = map; 133 out.x = VarMap.bottom(); 134 return GC.assume(map.apply(ec.pred)); 135 } 136 137 case TagConstants.GETSCMD: 138 case TagConstants.SUBGETSCMD: 139 case TagConstants.SUBSUBGETSCMD: 140 case TagConstants.RESTOREFROMCMD: 141 { 142 /* dsa[[ x = e, M ]] == 143 assume x' = M[[e]], M[x->x'], bottom 144 dsa[[ x[e0] = e, M ]] == 145 assume x' = M[[ store(x, e0, e) ]], M[x->x'], bottom 146 dsa[[ x[e0][e1] = e, M ]] == 147 assume x' = M[[ store(x, e0, store(select(x, e0), e1, e)) ]], 148 M[x->x'], bottom 149 150 (where "x'" is a fresh inflected form of "x"). 151 */ 152 153 AssignCmd gc = (AssignCmd)g; 154 155 // Create the declaration for "x'". 156 LocalVarDecl xpDecl = UniqName.newIntermediateStateVar(gc.v, dynInstPrefix); 157 VariableAccess xpRef = VariableAccess.make( gc.v.id, gc.v.loc, 158 xpDecl ); 159 160 // Calculate the new value of "x'". 161 Expr nuv = null; 162 switch( g.getTag() ) { 163 case TagConstants.GETSCMD: 164 case TagConstants.RESTOREFROMCMD: 165 { 166 nuv = gc.rhs; 167 break; 168 } 169 170 case TagConstants.SUBGETSCMD: 171 { 172 SubGetsCmd sgc = (SubGetsCmd)g; 173 if (sgc.rhs == null) break; 174 nuv = GC.nary(Location.NULL, Location.NULL, 175 TagConstants.STORE, sgc.v, sgc.index, sgc.rhs); 176 break; 177 } 178 179 case TagConstants.SUBSUBGETSCMD: 180 { 181 SubSubGetsCmd ssgc = (SubSubGetsCmd)g; 182 if (ssgc.rhs == null) break; 183 184 Expr innermap = GC.nary(Location.NULL, 185 Location.NULL, 186 TagConstants.SELECT, ssgc.v, ssgc.index1); 187 Expr newinnermap = GC.nary(Location.NULL, 188 Location.NULL, 189 TagConstants.STORE, innermap, ssgc.index2, 190 ssgc.rhs); 191 nuv = GC.nary(Location.NULL,Location.NULL, 192 TagConstants.STORE, ssgc.v, ssgc.index1, 193 newinnermap); 194 break; 195 } 196 197 default: 198 Assert.fail("Unreachable"); 199 nuv = null; // dummy assignment 200 } 201 202 out.x = VarMap.bottom(); 203 if (nuv == null) { 204 out.n = map.extend( gc.v.decl, xpRef); 205 return GC.skip(); 206 } else if( GC.isSimple( nuv ) ) { 207 nuv = map.apply( nuv ); 208 out.n = map.extend( gc.v.decl, nuv ); 209 return GC.skip(); 210 } else { 211 nuv = map.apply( nuv ); 212 out.n = map.extend(gc.v.decl, xpRef); 213 return GC.assume(GC.nary( gc.v.loc, gc.v.loc, 214 TagConstants.ANYEQ, xpRef, nuv )); 215 } 216 } 217 218 case TagConstants.VARINCMD: 219 /* dsa[[ var v in S, M ]] == 220 S', N[v->v], X[v->v] 221 where dsa[[ S, M ]] == S', N, X . 222 */ 223 224 { 225 VarInCmd vc = (VarInCmd)g; 226 VarMapPair nx = new VarMapPair(); 227 228 Hashtable h1 = new Hashtable(); 229 Hashtable h2 = new Hashtable(); 230 for (int i = 0; i < vc.v.size(); i++) { 231 GenericVarDecl v = vc.v.elementAt(i); 232 LocalVarDecl decl = UniqName.newIntermediateStateVar(v, dynInstPrefix); 233 VariableAccess xpRef = VariableAccess.make( decl.id, decl.locId, decl ); 234 h1.put(v, xpRef); 235 Expr oldExpr = (Expr) map.get(v); 236 if (oldExpr != null) { 237 h2.put(v, oldExpr); 238 } 239 } 240 241 GuardedCmd sp = dsa(vc.g, map.extend(h1), nx, dynInstPrefix, preOrderCount, lastVarUse); 242 243 out.n = nx.n.unmap(vc.v).extend(h2); 244 out.x = nx.x.unmap(vc.v).extend(h2); 245 246 return sp; 247 } 248 249 case TagConstants.DYNINSTCMD: 250 { 251 DynInstCmd dc = (DynInstCmd)g; 252 253 return dsa(dc.g, map, out, dynInstPrefix + "-" + dc.s, preOrderCount, lastVarUse); 254 } 255 256 case TagConstants.SEQCMD: 257 /* dsa[[ A ; B , M ]] == 258 let A', AN, AX == dsa[[ A , M ]] 259 B', BN, BX == dsa[[ B , AN ]] 260 AXR, BXR, X == merge(AX, BX) 261 in 262 ((A' ! (AXR ; raise)) ; (B' ! (BXR ; raise))), BN, X 263 */ 264 { 265 SeqCmd sc = (SeqCmd)g; 266 GuardedCmd[] ap = new GuardedCmd[sc.cmds.size()]; 267 VarMap[] xmap = new VarMap[sc.cmds.size()]; 268 VarMapPair temp = new VarMapPair(); 269 270 for (int i = 0; i < sc.cmds.size(); i++) { 271 ap[i] = dsa(sc.cmds.elementAt(i), map, temp, dynInstPrefix, preOrderCount, lastVarUse); 272 map = temp.n; 273 xmap[i] = temp.x; 274 } 275 276 out.n = map; 277 GuardedCmdVec[] rename = new GuardedCmdVec[sc.cmds.size()]; 278 int p = (preOrderCount == null ? 0 : preOrderCount.value); 279 out.x = VarMap.merge(xmap, rename, sc.getStartLoc(), p, lastVarUse); 280 281 GuardedCmdVec res = GuardedCmdVec.make(sc.cmds.size()); 282 for (int i = 0; i < sc.cmds.size(); i++) { 283 if (rename[i].size() > 0) { 284 ap[i] = GC.trycmd(ap[i], GC.seq(GC.seq(rename[i]),GC.raise())); 285 } 286 } 287 return GC.seq(GuardedCmdVec.make(ap)); 288 } 289 290 case TagConstants.TRYCMD: 291 /* dsa[[ A ! B , M ]] == 292 let A', AN, AX == dsa[[ A , M ]] 293 B', BN, BX == dsa[[ B , AX ]] 294 ANR, BNR, N == merge(AN, BN) 295 in 296 ((A' ; AN) ! (B' ; BN)), N, BX 297 */ 298 { 299 CmdCmdCmd tc = (CmdCmdCmd)g; 300 VarMapPair amaps = new VarMapPair(); 301 VarMapPair bmaps = new VarMapPair(); 302 GuardedCmd ap = dsa(tc.g1, map, amaps, dynInstPrefix, preOrderCount, lastVarUse); 303 GuardedCmd bp = dsa(tc.g2, amaps.x, bmaps, dynInstPrefix, preOrderCount, lastVarUse); 304 out.x = bmaps.x; 305 GuardedCmdVec[] rename = new GuardedCmdVec[2]; 306 int p = (preOrderCount == null ? 0 : preOrderCount.value); 307 out.n = VarMap.merge(amaps.n, bmaps.n, rename, tc.getStartLoc(), 308 p, lastVarUse); 309 return GC.trycmd( GC.seq(ap, GC.seq(rename[0])), 310 GC.seq(bp, GC.seq(rename[1]))); 311 } 312 313 case TagConstants.CHOOSECMD: 314 /* dsa[[ A [] B , M ]] == 315 let A', AN, AX == dsa[[ A , M ]] 316 B', BN, BX == dsa[[ B , M ]] 317 ANR, BNR, N == merge(AN, BN) 318 AXR, BXR, X == merge(AX, BX) 319 in 320 (((A' ; AN) ! (AX ; raise)) [] ((B' ; BN) ! (BX ; raise))), 321 N, X 322 */ 323 { 324 CmdCmdCmd cc = (CmdCmdCmd)g; 325 VarMapPair amaps = new VarMapPair(); 326 VarMapPair bmaps = new VarMapPair(); 327 GuardedCmd ap = dsa(cc.g1, map, amaps, dynInstPrefix, preOrderCount, lastVarUse); 328 GuardedCmd bp = dsa(cc.g2, map, bmaps, dynInstPrefix, preOrderCount, lastVarUse); 329 330 GuardedCmdVec[] nrename = new GuardedCmdVec[2]; 331 GuardedCmdVec[] xrename = new GuardedCmdVec[2]; 332 int p = (preOrderCount == null ? 0 : preOrderCount.value); 333 out.n = VarMap.merge(amaps.n, bmaps.n, nrename, cc.getStartLoc(), 334 p, lastVarUse); 335 out.x = VarMap.merge(amaps.x, bmaps.x, xrename, cc.getStartLoc(), 336 p, lastVarUse); 337 return GC.choosecmd(GC.trycmd(GC.seq(ap, GC.seq(nrename[0])), 338 GC.seq(GC.seq(xrename[0]), GC.raise())), 339 GC.trycmd(GC.seq(bp, GC.seq(nrename[1])), 340 GC.seq(GC.seq(xrename[1]), GC.raise()))); 341 } 342 343 default: 344 //@ unreachable; 345 Assert.fail("Fall thru on "+g); 346 return null; 347 } 348 } 349 350 //+@ requires lastVarUse.keyType == \type(GenericVarDecl); 351 //+@ requires lastVarUse.elementType == \type(RefInt); 352 private static void computeLastVarUses(/*@ non_null */ GuardedCmd g, 353 /*@ non_null */ RefInt preOrderCount, 354 /*@ non_null */ Hashtable lastVarUse) { 355 int id = preOrderCount.value; 356 preOrderCount.value++; 357 358 switch (g.getTag()) { 359 case TagConstants.SKIPCMD: 360 case TagConstants.RAISECMD: 361 break; 362 363 case TagConstants.LOOPCMD: 364 { 365 LoopCmd lp= (LoopCmd)g; 366 computeLastVarUses(lp.desugared, preOrderCount, lastVarUse); 367 break; 368 } 369 370 case TagConstants.CALL: 371 { 372 Call call= (Call)g; 373 computeLastVarUses(call.desugared, preOrderCount, lastVarUse); 374 break; 375 } 376 377 case TagConstants.ASSERTCMD: 378 case TagConstants.ASSUMECMD: 379 { 380 ExprCmd ec = (ExprCmd)g; 381 RefInt pi = new RefInt(id); 382 for (Enumeration e = Substitute.freeVars(ec.pred).elements(); 383 e.hasMoreElements(); ) { 384 GenericVarDecl v = (GenericVarDecl)e.nextElement(); 385 lastVarUse.put(v, pi); 386 } 387 break; 388 } 389 390 case TagConstants.GETSCMD: 391 case TagConstants.SUBGETSCMD: 392 case TagConstants.SUBSUBGETSCMD: 393 case TagConstants.RESTOREFROMCMD: 394 { 395 AssignCmd gc = (AssignCmd)g; 396 397 // Calculate the rhs of the assignment 398 Expr nuv = null; 399 switch( g.getTag() ) { 400 case TagConstants.GETSCMD: 401 case TagConstants.RESTOREFROMCMD: 402 { 403 nuv = gc.rhs; 404 break; 405 } 406 407 case TagConstants.SUBGETSCMD: 408 { 409 SubGetsCmd sgc = (SubGetsCmd)g; 410 if (sgc.rhs == null) break; 411 nuv = GC.nary(Location.NULL, Location.NULL, 412 TagConstants.STORE, sgc.v, sgc.index, sgc.rhs); 413 break; 414 } 415 416 case TagConstants.SUBSUBGETSCMD: 417 { 418 SubSubGetsCmd ssgc = (SubSubGetsCmd)g; 419 if (ssgc.rhs == null) break; 420 421 Expr innermap = GC.nary(Location.NULL, 422 Location.NULL, 423 TagConstants.SELECT, ssgc.v, ssgc.index1); 424 Expr newinnermap = GC.nary(Location.NULL, 425 Location.NULL, 426 TagConstants.STORE, innermap, ssgc.index2, 427 ssgc.rhs); 428 nuv = GC.nary(Location.NULL,Location.NULL, 429 TagConstants.STORE, ssgc.v, ssgc.index1, 430 newinnermap); 431 break; 432 } 433 434 default: 435 Assert.fail("Unreachable"); 436 nuv = null; // dummy assignment 437 } 438 439 if (nuv != null) { 440 RefInt pi = new RefInt(id); 441 for (Enumeration e = Substitute.freeVars(nuv).elements(); 442 e.hasMoreElements(); ) { 443 GenericVarDecl v = (GenericVarDecl)e.nextElement(); 444 lastVarUse.put(v, pi); 445 } 446 } 447 break; 448 } 449 450 case TagConstants.VARINCMD: 451 { 452 VarInCmd vc = (VarInCmd)g; 453 computeLastVarUses(vc.g, preOrderCount, lastVarUse); 454 break; 455 } 456 457 case TagConstants.DYNINSTCMD: 458 { 459 DynInstCmd dc = (DynInstCmd)g; 460 computeLastVarUses(dc.g, preOrderCount, lastVarUse); 461 break; 462 } 463 464 case TagConstants.SEQCMD: 465 { 466 SeqCmd sc = (SeqCmd)g; 467 for (int i = 0; i < sc.cmds.size(); i++) { 468 computeLastVarUses(sc.cmds.elementAt(i), preOrderCount, lastVarUse); 469 } 470 break; 471 } 472 473 case TagConstants.TRYCMD: 474 case TagConstants.CHOOSECMD: 475 { 476 CmdCmdCmd tc = (CmdCmdCmd)g; 477 computeLastVarUses(tc.g1, preOrderCount, lastVarUse); 478 computeLastVarUses(tc.g2, preOrderCount, lastVarUse); 479 break; 480 } 481 482 default: 483 //@ unreachable; 484 Assert.fail("Fall thru on "+g); 485 break; 486 } 487 } 488 489 private static void doPreOrderCount(/*@ non_null */ GuardedCmd g, 490 /*@ non_null */ RefInt preOrderCount) { 491 preOrderCount.value++; 492 493 switch (g.getTag()) { 494 case TagConstants.SKIPCMD: 495 case TagConstants.RAISECMD: 496 break; 497 498 case TagConstants.LOOPCMD: 499 { 500 LoopCmd lp= (LoopCmd)g; 501 doPreOrderCount(lp.desugared, preOrderCount); 502 break; 503 } 504 505 case TagConstants.CALL: 506 { 507 Call call= (Call)g; 508 doPreOrderCount(call.desugared, preOrderCount); 509 break; 510 } 511 512 case TagConstants.ASSERTCMD: 513 case TagConstants.ASSUMECMD: 514 break; 515 516 case TagConstants.GETSCMD: 517 case TagConstants.SUBGETSCMD: 518 case TagConstants.SUBSUBGETSCMD: 519 case TagConstants.RESTOREFROMCMD: 520 break; 521 522 case TagConstants.VARINCMD: 523 { 524 VarInCmd vc = (VarInCmd)g; 525 doPreOrderCount(vc.g, preOrderCount); 526 break; 527 } 528 529 case TagConstants.DYNINSTCMD: 530 { 531 DynInstCmd dc = (DynInstCmd)g; 532 doPreOrderCount(dc.g, preOrderCount); 533 break; 534 } 535 536 case TagConstants.SEQCMD: 537 { 538 SeqCmd sc = (SeqCmd)g; 539 for (int i = 0; i < sc.cmds.size(); i++) { 540 doPreOrderCount(sc.cmds.elementAt(i), preOrderCount); 541 } 542 break; 543 } 544 545 case TagConstants.TRYCMD: 546 case TagConstants.CHOOSECMD: 547 { 548 CmdCmdCmd tc = (CmdCmdCmd)g; 549 doPreOrderCount(tc.g1, preOrderCount); 550 doPreOrderCount(tc.g2, preOrderCount); 551 break; 552 } 553 554 default: 555 //@ unreachable; 556 Assert.fail("Fall thru on "+g); 557 break; 558 } 559 } 560 }