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 /* EscPrettyPrint.inst.toString(e) */);
269 return false; // dummy return
270 }
271 }
272 }
273 }
274 }