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    }