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 }