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 }