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 }