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    }