001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package escjava.sp; 004 005 import escjava.translate.GC; 006 import java.util.Hashtable; 007 import java.util.Enumeration; 008 009 import javafe.ast.*; 010 import escjava.ast.*; 011 import escjava.ast.TagConstants; 012 013 import javafe.util.Location; 014 import javafe.util.Assert; 015 import javafe.util.Set; 016 017 import escjava.Main; 018 019 class NXW 020 { 021 /* predicate for normal, exceptional, and wrong outcomes of a command */ 022 public Expr n,x,w; 023 } 024 025 public class SPVC 026 { 027 public static Expr compute(GuardedCmd g) { 028 SPVC spvc = new SPVC(); 029 return spvc.computeNotWrong(g); 030 } 031 032 private Hashtable cache = new Hashtable(); 033 private Set cacheHit = new Set(); 034 private DefPredVec preds = DefPredVec.make(); 035 private static int predNum = 0; 036 037 private Expr name(Expr e) { 038 if( Main.options().useDefpred && Util.size(e) >= Main.options().namePCsize) { 039 Identifier predId = Identifier.intern("PREDN"+predNum); 040 predNum++; 041 preds.addElement( DefPred.make( predId, GenericVarDeclVec.make(), e )); 042 return DefPredApplExpr.make( predId, ExprVec.make() ); 043 } else { 044 return e; 045 } 046 } 047 048 private Expr computeNotWrong(GuardedCmd root) { 049 Expr r = GC.nary(TagConstants.BOOLNOT, calcNxw(root).w); 050 if( Main.options().useDefpred ) { 051 return DefPredLetExpr.make( preds, r); 052 } else { 053 return r; 054 } 055 } 056 057 public static Expr computeN(GuardedCmd g) { 058 SPVC spvc = new SPVC(); 059 return spvc.calcNxw(g).n; 060 } 061 062 private NXW calcNxw(GuardedCmd g) { 063 064 NXW nxw = (NXW)cache.get(g); 065 if (nxw != null) { 066 cacheHit.add(g); 067 return nxw; 068 } 069 nxw = new NXW(); 070 071 switch (g.getTag()) { 072 case TagConstants.SKIPCMD: 073 /* norm(skip) == true 074 exc(skip) == false 075 wrong(skip) == false 076 */ 077 nxw.n = GC.truelit; 078 nxw.x = GC.falselit; 079 nxw.w = GC.falselit; 080 break; 081 082 case TagConstants.RAISECMD: 083 /* norm(raise) == false 084 exc(raise) == true 085 wrong(raise) == false 086 */ 087 nxw.n = GC.falselit; 088 nxw.x = GC.truelit; 089 nxw.w = GC.falselit; 090 break; 091 092 case TagConstants.ASSERTCMD: 093 /* norm(assert E) == E 094 exc(assert E) == false 095 wrong(assert E) == !E 096 */ 097 { 098 ExprCmd ec = (ExprCmd)g; 099 if (Main.options().strongAssertPost == 2 || 100 (Main.options().strongAssertPost == 1 && isSimpleConjunction(ec.pred))) { 101 nxw.n = ec.pred; 102 } else { 103 nxw.n = GC.truelit; 104 } 105 nxw.x = GC.falselit; 106 nxw.w = GC.nary(TagConstants.BOOLNOT, ec.pred); 107 break; 108 } 109 110 case TagConstants.ASSUMECMD: 111 /* norm(assume E) == E 112 exc(assume E) == false 113 wrong(assume E) == false 114 */ 115 { 116 ExprCmd ec = (ExprCmd)g; 117 nxw.n = ec.pred; 118 nxw.x = GC.falselit; 119 nxw.w = GC.falselit; 120 break; 121 } 122 123 case TagConstants.CHOOSECMD: 124 /* norm(A [] B) == norm(A) | norm(B) 125 exc(A [] B) == exc(A) | exc(B) 126 wrong(A [] B) == wrong(A) | wrong(B) 127 */ 128 { 129 CmdCmdCmd cc = (CmdCmdCmd)g; 130 NXW a = calcNxw(cc.g1); 131 NXW b = calcNxw(cc.g2); 132 nxw.n = GC.or(a.n, b.n); 133 nxw.x = GC.or(a.x, b.x); 134 nxw.w = GC.or(a.w, b.w); 135 break; 136 } 137 138 case TagConstants.TRYCMD: 139 /* norm(A ! B) == norm(A) | (exc(A) & norm(B ) 140 exc(A ! B) == exc(A) & exc(B) 141 wrong(A ! B) == wrong(A) | (exc(A) & wrong(B)) 142 */ 143 { 144 CmdCmdCmd cc = (CmdCmdCmd)g; 145 NXW a = calcNxw(cc.g1); 146 NXW b = calcNxw(cc.g2); 147 Expr ax = name(a.x); 148 nxw.n = GC.or(a.n, GC.and(ax, b.n)); 149 nxw.x = GC.and(ax, b.x); 150 nxw.w = GC.or(a.w, GC.and(ax, b.w)); 151 break; 152 } 153 154 case TagConstants.SEQCMD: 155 /* norm(A ; B) == norm(A) & norm(B) 156 exc(A ; B) == exc(A) | (norm(A) & exc(B)) 157 wrong(A ; B) == wrong(A) | (norm(A) & wrong(B)) 158 */ 159 { 160 SeqCmd sc = (SeqCmd)g; 161 162 nxw.n = GC.truelit; 163 nxw.x = GC.falselit; 164 nxw.w = GC.falselit; 165 166 167 for (int i = sc.cmds.size() -1; 0 <= i; i--) { 168 NXW temp = calcNxw(sc.cmds.elementAt(i)); 169 Expr tempn = name(temp.n); 170 Expr n = GC.and(tempn, nxw.n); 171 Expr x = GC.or(temp.x, GC.and(tempn, nxw.x)); 172 Expr w = GC.or(temp.w, GC.and(tempn, nxw.w)); 173 nxw.n = n; 174 nxw.x = x; 175 nxw.w = w; 176 } 177 break; 178 } 179 180 default: 181 //@ unreachable; 182 Assert.fail("Fall thru on "+g); 183 return null; 184 } 185 186 cache.put(g, nxw); 187 return nxw; 188 189 } 190 191 public static boolean isSimpleConjunction(Expr e) { 192 if (e instanceof NaryExpr) { 193 NaryExpr ne = (NaryExpr)e; 194 if (ne.op == TagConstants.BOOLAND || ne.op == TagConstants.BOOLANDX) { 195 for (int i = 0; i < ne.exprs.size(); i++) { 196 if (! isSimpleExpr(ne.exprs.elementAt(i))) { 197 return false; 198 } 199 } 200 return true; 201 } 202 } 203 return isSimpleExpr(e); 204 } 205 206 private static boolean isSimpleExpr(Expr e) { 207 switch (e.getTag()) { 208 case TagConstants.LABELEXPR: 209 { 210 LabelExpr le = (LabelExpr)e; 211 return isSimpleExpr(le.expr); 212 } 213 214 case TagConstants.GUARDEXPR: 215 { 216 GuardExpr ge = (GuardExpr)e; 217 return isSimpleExpr(ge.expr); 218 } 219 220 case TagConstants.FORALL: 221 case TagConstants.EXISTS: 222 return false; 223 224 case TagConstants.TYPEEXPR: 225 case TagConstants.LOCKSETEXPR: 226 case TagConstants.RESEXPR: 227 case TagConstants.WILDREFEXPR: 228 case TagConstants.ARRAYRANGEREFEXPR: 229 case TagConstants.THISEXPR: 230 case TagConstants.CLASSLITERAL: 231 232 case TagConstants.BOOLEANLIT: 233 case TagConstants.CHARLIT: 234 case TagConstants.DOUBLELIT: 235 case TagConstants.FLOATLIT: 236 case TagConstants.INTLIT: 237 case TagConstants.LONGLIT: 238 case TagConstants.NULLLIT: 239 case TagConstants.STRINGLIT: 240 case TagConstants.SYMBOLLIT: 241 242 case TagConstants.VARIABLEACCESS: 243 return true; 244 245 case TagConstants.BOOLAND: 246 case TagConstants.BOOLANDX: 247 case TagConstants.BOOLOR: 248 case TagConstants.DTTFSA: 249 return false; 250 251 case TagConstants.SUBSTEXPR: 252 { SubstExpr se = (SubstExpr)e ; 253 return isSimpleExpr(se.target) && isSimpleExpr(se.val) ; 254 } 255 256 default: 257 { 258 if (e instanceof NaryExpr) { 259 NaryExpr ne = (NaryExpr)e; 260 for (int i = 0; i < ne.exprs.size(); i++) { 261 if (! isSimpleExpr(ne.exprs.elementAt(i))) { 262 return false; 263 } 264 } 265 return true; 266 } else { 267 Assert.fail("Unexpected expr in SPVC.isSimpleExpr: "+e); 268 return false; // dummy return 269 } 270 } 271 } 272 } 273 }