    001    /* Copyright 2000, 2001, Compaq Computer Corporation */
    002
    003
    004    package escjava.translate;
    005
    006    import javafe.ast.*;
    007    import escjava.ast.*;
    008    import escjava.ast.TagConstants;
    009    import escjava.sp.VarMap;
    010
    011    import javafe.util.Location;
    012    import javafe.util.Assert;
    013
    014    public abstract class Ejp {
    015
    016      public static Expr compute(/*@ non_null */ GuardedCmd g,
    017                                 /*@ non_null */ Expr normal,
    018                                 /*@ non_null */ Expr exceptional) {
    019        VarMap dynInstMap = VarMap.identity();
    020        return compute(g, normal, exceptional, "", dynInstMap);
    021      }
    022
    023      /* @ requires (* "normal" and "exceptional" have been as inflected by
    024                       "dynInstMap" as they need to be, that is, this method
    025                       is not to apply "dynInstMap" to "normal" and
    026                       "exceptional" *);
    027           ensures (* \result has been as inflected by "dynInstMap" as it needs
    028                      to be *);
    029       */
    030      private static Expr compute(/*@ non_null */ GuardedCmd g,
    031                                  /*@ non_null */ Expr normal,
    032                                  /*@ non_null */ Expr exceptional,
    033                                  /*@ non_null */ String dynInstPrefix,
    034                                  /*@ non_null */ VarMap dynInstMap) {
    035        switch (g.getTag()) {
    036        case TagConstants.SKIPCMD:
    037          // ejp[[ Skip ]](N,X) = N
    038          return normal;
    039
    040        case TagConstants.LOOPCMD:
    041        {
    042          LoopCmd lp= (LoopCmd)g;
    043          return compute(lp.desugared, normal, exceptional,
    044                         dynInstPrefix, dynInstMap);
    045        }
    046
    047        case TagConstants.RAISECMD:
    048          // ejp[[ Raise ]](N,X) = X
    049          return exceptional;
    050
    051        case TagConstants.ASSERTCMD: {
    052          // ejp[[ Assert x ]](N,X) = x /\ P
    053          ExprCmd ec = (ExprCmd)g;
    054          return GC.and(dynInstMap.apply(ec.pred), normal);
    055        }
    056
    057        case TagConstants.ASSUMECMD: {
    058          // ejp[[ Assume x ]](N,X) = x ==> N
    059          ExprCmd ec = (ExprCmd)g;
    060          return GC.implies(dynInstMap.apply(ec.pred), normal);
    061        }
    062
    063        case TagConstants.CALL:
    064          {
    065            Call call = (Call)g;
    066            return compute(call.desugared, normal, exceptional,
    067                           dynInstPrefix, dynInstMap);
    068          }
    069
    070        case TagConstants.GETSCMD:
    071        case TagConstants.SUBGETSCMD:
    072        case TagConstants.SUBSUBGETSCMD:
    073        case TagConstants.RESTOREFROMCMD:
    074            {
    075              // ejp[[ v = x ]](N,X) =
    076              //   (forall t :: t==x ==> N[dynInstMap(v):=t])
    077              // and variants for the other kinds of assignment
    078
    079              AssignCmd gc = (AssignCmd)g;
    080
    081              // Create t
    082              LocalVarDecl tDecl = UniqName.newIntermediateStateVar(gc.v,
    083                                                                    dynInstPrefix);
    084              VariableAccess tRef = VariableAccess.make(tDecl.id, gc.v.loc, tDecl);
    085
    086              // Calculate the new value of v
    087              Expr nuv;
    088              switch( g.getTag() ) {
    089                case TagConstants.GETSCMD:
    090                case TagConstants.RESTOREFROMCMD:
    091                  {
    092                    // ejp[[ v = x ]](N,X) =
    093                    //   (forall t :: t==x ==> N[dynInstMap(v):=t])
    094                    // ejp[[ RESTORE v FROM x ]] == ejp[[ v = x ]]
    095
    096                    nuv = gc.rhs;
    097                    break;
    098                  }
    099
    100                case TagConstants.SUBGETSCMD:
    101                  {
    102                    // ejp[[ v[i] = x ]](N,X) =
    103                    //   (forall t :: t==store(v,i,x) ==> N[dynInstMap(v):=t])
    104
    105                    SubGetsCmd sgc = (SubGetsCmd)g;
    106                    nuv = GC.nary(Location.NULL, Location.NULL,
    107                                  TagConstants.STORE, sgc.v, sgc.index, sgc.rhs);
    108                    break;
    109                  }
    110
    111                case TagConstants.SUBSUBGETSCMD:
    112                  {
    113                    // ejp[[ v[i1][i2] = x]](N,X) =
    114                    //    (forall t :: t==store(v, i1, store(select(v,i1), i2, x))
    115                    //                 ==>
    116                    //                 N[dynInstMap(v):=t])
    117
    118                    SubSubGetsCmd ssgc = (SubSubGetsCmd)g;
    119
    120                    Expr innermap = GC.nary(Location.NULL, Location.NULL,
    121                                            TagConstants.SELECT,
    122                                            ssgc.v, ssgc.index1);
    123                    Expr newinnermap = GC.nary(Location.NULL, Location.NULL,
    124                                               TagConstants.STORE,
    125                                               innermap, ssgc.index2, ssgc.rhs);
    126                    nuv = GC.nary(Location.NULL, Location.NULL,
    127                                  TagConstants.STORE,
    128                                  ssgc.v, ssgc.index1, newinnermap);
    129                    break;
    130                  }
    131
    132                default:
    133                  Assert.fail("Unreachable");
    134                  nuv = null; // dummy assignment
    135              }
    136
    137              // vv = dynInstMap(v)
    138              VariableAccess vva = (VariableAccess)dynInstMap.get(gc.v.decl);
    139              GenericVarDecl vv;
    140              if (vva == null) {
    141                vv = gc.v.decl;
    142              } else {
    143                vv = vva.decl;
    144              }
    145
    146              Expr normal2 = GC.subst(vv, tRef, normal);
    147              int locStart = g.getStartLoc();
    148              int locEnd = g.getEndLoc();
    149              Expr equals = GC.nary(locStart, locEnd,
    150                                    TagConstants.ANYEQ,
    151                                    tRef, dynInstMap.apply(nuv));
    152              Expr implies = GC.implies(locStart, locEnd, equals, normal2);
    153              return GC.forall(locStart, locEnd, tDecl, null, implies);
    154            }
    155
    156        case TagConstants.VARINCMD: {
    157          // ejp[[ var v in S ]](N,X) = (forall v . ejp[[S]](N,X))
    158          VarInCmd vc = (VarInCmd)g;
    159
    160          LocalVarDecl[] newNames = new LocalVarDecl[vc.v.size()];
    161          for (int i = 0; i < vc.v.size(); i++) {
    162            GenericVarDecl v = vc.v.elementAt(i);
    163
    164            // create a new variable with a unique name...
    165            LocalVarDecl decl = UniqName.newIntermediateStateVar(v, dynInstPrefix);
    166            newNames[i] = decl;
    167            VariableAccess xpRef = VariableAccess.make(decl.id, decl.locId, decl);
    168            // ...and map "v" to it
    169            dynInstMap = dynInstMap.extend(v, xpRef);
    170          }
    171
    172          Expr result = Ejp.compute(vc.g, normal, exceptional, dynInstPrefix,
    173                                    dynInstMap);
    174          for (int i = newNames.length-1; 0 <= i; i--) {
    175            result = GC.forall(newNames[i], result);
    176          }
    177
    178          return result;
    179        }
    180
    181        case TagConstants.DYNINSTCMD: {
    182          // ejp[[ DynamicInstanceCommand s in S end]](N,X) = ejp[[S]](N,X))
    183          DynInstCmd dc = (DynInstCmd)g;
    184          return Ejp.compute(dc.g, normal, exceptional,
    185                             dynInstPrefix + "-" + dc.s, dynInstMap);
    186        }
    187
    188        case TagConstants.SEQCMD: {
    189          // ejp[[ S1 ; S2 ]](N,X) = ejp[[S1]](ejp[[S2]](N,X), X)
    190          SeqCmd sc = (SeqCmd)g;
    191          for (int i = sc.cmds.size()-1; 0 <= i; i--)
    192            normal = Ejp.compute(sc.cmds.elementAt(i), normal, exceptional,
    193                                 dynInstPrefix, dynInstMap);
    194          return normal;
    195        }
    196
    197        case TagConstants.TRYCMD: {
    198          // ejp[[ S1 ! S2 ]](N,X) = ejp[[S1]](N, ejp[[S2]](N,X))
    199          CmdCmdCmd tc = (CmdCmdCmd)g;
    200          return Ejp.compute(tc.g1,
    201                             normal, Ejp.compute(tc.g2, normal, exceptional,
    202                                                 dynInstPrefix, dynInstMap),
    203                             dynInstPrefix, dynInstMap);
    204        }
    205
    206        case TagConstants.CHOOSECMD: {
    207          // ejp[[ S1 [] S2 ]](N,X) = ejp[[S1]](N,X) /\ ejp[[S2]](N,X)
    208          CmdCmdCmd cc = (CmdCmdCmd)g;
    209          return GC.and(Ejp.compute(cc.g1, normal, exceptional,
    210                                    dynInstPrefix, dynInstMap),
    211                        Ejp.compute(cc.g2, normal, exceptional,
    212                                    dynInstPrefix, dynInstMap));
    213        }
    214
    215        default:
    216          //@ unreachable;
    217          Assert.fail("Fall thru on "+g);
    218          return null;
    219        }
    220      }
    221    }