    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    }