001 /* @(#)$Id: DefGCmd.java,v 1.13 2006/08/13 21:54:20 g_karab Exp $
002 *
003 * Copyright (C) 2006, Dependable Software Research Group, Concordia University
004 */
005
006 package escjava.translate;
007
008 import java.util.Hashtable;
009
010 import javafe.util.StackVector;
011 import javafe.util.Location;
012
013 import javafe.ast.*;
014 import javafe.util.Assert;
015 import javafe.util.ErrorSet;
016
017 import escjava.Main;
018 import escjava.ast.ExprCmd;
019 import escjava.ast.GCExpr;
020 import escjava.ast.GuardedCmd;
021 import escjava.ast.GuardedCmdVec;
022 import escjava.ast.LabelExpr;
023 import escjava.ast.NaryExpr;
024 import escjava.ast.TagConstants;
025
026 /**
027 * Class <code>DefGCmd</code> implements the definedness guarded commands
028 * for the requires clauses. The functionality is invoced by adding the -idc
029 * option to escj.
030 * Supported functionality:
031 * - <code>div</code> and <code>mod</code> operators generate CHKARITHMETIC checks
032 * - Conditional<code>&&</code> and <code>or</code> operators generate ifcmd
033 * guarded commands.
034 * - Dereferrencing is partially supported. Still working on this.
035 * Usage:
036 * - DefGCmd defGCmd=new DefGCmd();
037 * - defGCmd.trAndGen(expr); // expr is an untranslated expression.
038 * - GuardedCmd gc=defGCmd.popFromCode();
039 * NOTE: This is work inprogress and its fairly experimental,
040 * so bear with us for the time being :). Use at your own risk.
041 *
042 * @author <a href="mailto:g_karab@cs.concordia.ca">George Karabotsos</a>
043 * @version 1.0
044 */
045 public class DefGCmd
046 {
047 /**
048 * <code>code</code> is the StackVector instance and is used to hold the
049 * definednes guarded commands for each method.
050 *
051 */
052 private StackVector code;
053
054 /**
055 * <code>debug</code> is a central and convinient way of turning on/off
056 * debug messages.
057 *
058 */
059 public static boolean debug = Main.options().debug;
060
061 /**
062 * Creates a new <code>DefGCmd</code> instance.
063 *
064 */
065 public DefGCmd()
066 {
067 // debug = Main.options().debug;
068 if (debug) System.err.println(this.traceMethod());
069 this.code=new StackVector();
070 this.code.push();
071 }
072
073 /**
074 * Convenient shorthand for the command in the return statement.
075 *
076 * @return a <code>GuardedCmd</code> value
077 */
078 public GuardedCmd popFromCode()
079 {
080 return(GC.seq(GuardedCmdVec.popFromStackVector(code)));
081 }
082
083 /**
084 * This is the workhorse method. In this method we go through the
085 * <code>Expr</code> tree and generate the appropriate guarded commands.
086 * The guarded commands are generated and stored in the <code>code</code>
087 * field.
088 *
089 * @param x an <code>Expr</code> value
090 * @return an <code>Expr</code> value. This expression is always a GCExpr.
091 * its not set as GCExpr so that we do not get type mismatch between client
092 * methods.
093 */
094
095 /** (new trAndGent)
096 */
097
098 public Expr trAndGen(Expr e) {
099 int tag = e.getTag();
100 switch (tag) {
101 case TagConstants.THISEXPR: {
102 break;
103 }
104
105 // Literals (which are already GCExpr's)
106 case TagConstants.BOOLEANLIT:
107 case TagConstants.CHARLIT:
108 case TagConstants.DOUBLELIT:
109 case TagConstants.FLOATLIT:
110 case TagConstants.INTLIT:
111 case TagConstants.LONGLIT:
112 case TagConstants.NULLLIT: {
113 break;
114 }
115
116 case TagConstants.STRINGLIT: {
117 break;
118 }
119
120 case TagConstants.RESEXPR: {
121 break;
122 }
123
124 case TagConstants.LOCKSETEXPR: {
125 break;
126 }
127
128 case TagConstants.VARIABLEACCESS: {
129 break;
130 }
131
132 case TagConstants.FIELDACCESS: {
133 // <expr>.id
134 FieldAccess fa = (FieldAccess)e;
135 if (!Modifiers.isStatic(fa.decl.modifiers) &&
136 fa.od.getTag() == TagConstants.EXPROBJECTDESIGNATOR)
137 {
138 ExprObjectDesignator eod = (ExprObjectDesignator)fa.od;
139 Expr odExpr = trAndGen(eod.expr);
140 Expr refNEExpr=GC.nary(TagConstants.REFNE,odExpr,GC.nulllit);
141 GuardedCmd gc = GC.check(eod.locDot,
142 TagConstants.CHKNULLPOINTER,
143 refNEExpr,
144 Location.NULL);
145 this.code.addElement(gc);
146 }
147 break;
148 }
149
150 case TagConstants.ARRAYREFEXPR: {
151 ArrayRefExpr are=(ArrayRefExpr)e;
152 Expr array=this.trAndGen(are.array);
153 Expr index=this.trAndGen(are.index);
154 // Null check
155 Expr refNEExpr=GC.nary(TagConstants.REFNE,
156 array,GC.nulllit);
157 GuardedCmd gc = GC.check(are.locOpenBracket,
158 TagConstants.CHKNULLPOINTER,
159 refNEExpr,Location.NULL);
160 this.code.addElement(gc);
161 // Negative index check
162 Expr indexNeg=GC.nary(TagConstants.INTEGRALLE,
163 GC.zerolit, index);
164 GuardedCmd gc1=GC.check(are.locOpenBracket,
165 TagConstants.CHKINDEXNEGATIVE,
166 indexNeg,Location.NULL);
167 this.code.addElement(gc1);
168 // Index too big check
169 Expr length= GC.nary(TagConstants.ARRAYLENGTH, array);
170 Expr index2Big=GC.nary(TagConstants.INTEGRALLT,
171 index, length);
172 GuardedCmd gc2=GC.check(are.locOpenBracket,
173 TagConstants.CHKINDEXTOOBIG,
174 index2Big,Location.NULL);
175 this.code.addElement(gc2);
176 }
177
178 case TagConstants.ARRAYRANGEREFEXPR:
179 case TagConstants.WILDREFEXPR: {
180 break;
181 }
182
183 case TagConstants.PARENEXPR: {
184 ParenExpr pe = (ParenExpr)e;
185 // TrAnExpr.trSpecExpr drops the parenthesis, so do I :).
186 return trAndGen(pe.expr);
187 }
188
189 // Unary operator expressions
190
191 case TagConstants.UNARYSUB:
192 case TagConstants.NOT:
193 case TagConstants.BITNOT: {
194 UnaryExpr ue = (UnaryExpr)e;
195 int newtag = TrAnExpr.getGCTagForUnary(ue);
196 return GC.nary(ue.getStartLoc(), ue.getEndLoc(), newtag,
197 trAndGen(ue.expr));
198 }
199
200 case TagConstants.UNARYADD: {
201 UnaryExpr ue = (UnaryExpr)e;
202 return trAndGen(ue.expr);
203 }
204
205 case TagConstants.TYPEOF:
206 case TagConstants.ELEMTYPE:
207 case TagConstants.MAX: {
208 NaryExpr ne = (NaryExpr)e;
209 int n = ne.exprs.size();
210 ExprVec exprs = ExprVec.make(n);
211 for (int i = 0; i < n; i++) {
212 exprs.addElement(trAndGen(ne.exprs.elementAt(i)));
213 }
214 return GC.nary(ne.getStartLoc(), ne.getEndLoc(), ne.getTag(), exprs);
215 }
216
217 case TagConstants.DTTFSA: {
218 // take this expr as atomic -- could to more (see
219 // TrAnExpr.trSpecExpr), but probably isn't worth it
220 break;
221 }
222
223 case TagConstants.ELEMSNONNULL: {
224 NaryExpr ne = (NaryExpr)e;
225 VariableAccess elems = TrAnExpr.makeVarAccess(GC.elemsvar.decl,
226 e.getStartLoc());
227 return GC.nary(ne.getStartLoc(), ne.getEndLoc(), ne.getTag(),
228 trAndGen(ne.exprs.elementAt(0)), elems);
229 }
230
231 // Binary operator expressions
232
233 case TagConstants.OR: {
234 BinaryExpr be = (BinaryExpr)e;
235 Expr leftExpr = this.trAndGen(be.left);
236 this.code.push();
237 Expr rightExpr = this.trAndGen(be.right);
238 GuardedCmd rightGC=this.popFromCode();
239 GuardedCmd leftGC=GC.assume(GC.truelit);
240 GuardedCmd notleftGC=GC.assume(rightExpr);
241 this.code.
242 addElement(GC.ifcmd(leftExpr,
243 GC.assume(GC.truelit),
244 rightGC));
245 return GC.nary(e.getStartLoc(),e.getEndLoc(),
246 TagConstants.BOOLOR,
247 leftExpr,rightExpr);
248 }
249
250 case TagConstants.AND: {
251 BinaryExpr be = (BinaryExpr)e;
252 Expr leftExpr = this.trAndGen(be.left);
253 this.code.push();
254 Expr rightExpr = this.trAndGen(be.right);
255 GuardedCmd rightGC=this.popFromCode();
256 GuardedCmd leftGC=GC.assume(leftExpr);
257 GuardedCmd notLeftGC=GC.assume(GC.truelit);
258 this.code.
259 addElement(GC.ifcmd(leftExpr,rightGC,notLeftGC));
260 return GC.nary(e.getStartLoc(),e.getEndLoc(),
261 TagConstants.BOOLAND,
262 leftExpr,rightExpr);
263 }
264
265 case TagConstants.IMPLIES:
266 {
267 BinaryExpr be = (BinaryExpr)e;
268 Expr leftExpr = this.trAndGen(be.left);
269 Expr notLeftExpr=GC.nary(TagConstants.BOOLNOT,leftExpr);
270 this.code.push();
271 Expr rightExpr = this.trAndGen(be.right);
272 GuardedCmd rightGC=this.popFromCode();
273 GuardedCmd leftGC=GC.assume(GC.truelit);
274 GuardedCmd notleftGC=GC.assume(rightExpr);
275 this.code.
276 addElement(GC.ifcmd(notLeftExpr,
277 GC.assume(GC.truelit),
278 rightGC));
279 int newtag = TrAnExpr.getGCTagForBinary(be);
280 return GC.nary(e.getStartLoc(),e.getEndLoc(),
281 newtag,leftExpr,rightExpr);
282 }
283 case TagConstants.IFF:
284 case TagConstants.NIFF:
285 case TagConstants.BITOR:
286 case TagConstants.BITAND:
287 case TagConstants.BITXOR:
288 // fall through to the next group ...
289
290 case TagConstants.EQ:
291 case TagConstants.NE:
292 case TagConstants.LSHIFT:
293 case TagConstants.RSHIFT:
294 case TagConstants.URSHIFT:
295 // fall through to the next group ...
296
297 case TagConstants.GE:
298 case TagConstants.GT:
299 case TagConstants.LE:
300 case TagConstants.LT:
301 case TagConstants.ADD:
302 case TagConstants.SUB:
303 case TagConstants.STAR: {
304 BinaryExpr be = (BinaryExpr)e;
305 Expr leftExpr = this.trAndGen(be.left);
306 Expr rightExpr = this.trAndGen(be.right);
307 int newtag= TrAnExpr.getGCTagForBinary(be);
308 return GC.nary(e.getStartLoc(), e.getEndLoc(),
309 newtag, leftExpr, rightExpr);
310 }
311
312 case TagConstants.DIV:
313 case TagConstants.MOD: {
314 BinaryExpr be = (BinaryExpr)e;
315 Expr leftExpr = trAndGen(be.left);
316 Expr rightExpr = trAndGen(be.right);
317 Expr neZeroExpr=GC.nary(TagConstants.INTEGRALNE,
318 rightExpr,
319 GC.zerolit);
320 GuardedCmd gc=GC.check(be.locOp,
321 TagConstants.CHKARITHMETIC,
322 neZeroExpr,
323 Location.NULL);
324 this.code.addElement(gc);
325 int newtag= TrAnExpr.getGCTagForBinary(be);
326 return GC.nary(e.getStartLoc(), e.getEndLoc(),
327 newtag, leftExpr, rightExpr);
328 }
329
330 case TagConstants.NEWINSTANCEEXPR: {
331 NewInstanceExpr me = (NewInstanceExpr)e;
332 // ensure that definedness cond are generated
333 // for arguments to constructor ...
334 for (int i=0; i<me.args.size(); ++i) {
335 trAndGen(me.args.elementAt(i));
336 }
337 // but then let TrAnExpr actually do the translation ...
338 break;
339 }
340
341 case TagConstants.METHODINVOCATION: {
342 MethodInvocation me = (MethodInvocation)e;
343
344 // ensure that definedness cond are generated
345 // for arguments to method ...
346
347 // (eventually we will want to save the result so that we can use
348 // the translated actual param in a call to test the precondition of
349 // the method)
350
351 for (int i=0; i<me.args.size(); ++i) {
352 trAndGen(me.args.elementAt(i));
353 }
354
355 if (!Modifiers.isStatic(me.decl.modifiers) &&
356 me.od instanceof ExprObjectDesignator)
357 {
358 // Expr ex = ((ExprObjectDesignator)me.od).expr;
359 ExprObjectDesignator eod = (ExprObjectDesignator)me.od;
360 Expr odExpr = trAndGen(eod.expr);
361 Expr refNEExpr=GC.nary(TagConstants.REFNE,odExpr,GC.nulllit);
362 GuardedCmd gc = GC.check(eod.locDot,
363 TagConstants.CHKNULLPOINTER,
364 refNEExpr,
365 Location.NULL);
366 this.code.addElement(gc);
367 }
368 break;
369 }
370
371 case TagConstants.NEWARRAYEXPR: {
372 if(true) { break; } else { notImpl(e); }
373 return null;
374 }
375
376 case TagConstants.EXPLIES:
377 {
378 BinaryExpr be = (BinaryExpr)e;
379 Expr leftExpr = this.trAndGen(be.right);
380 Expr notLeftExpr=GC.nary(TagConstants.BOOLNOT,leftExpr);
381 this.code.push();
382 Expr rightExpr = this.trAndGen(be.left);
383 GuardedCmd rightGC=this.popFromCode();
384 GuardedCmd leftGC=GC.assume(GC.truelit);
385 GuardedCmd notleftGC=GC.assume(rightExpr);
386 this.code.
387 addElement(GC.ifcmd(notLeftExpr,
388 GC.assume(GC.truelit),
389 rightGC));
390 int newtag = TagConstants.BOOLIMPLIES;
391 return GC.nary(e.getStartLoc(),e.getEndLoc(),
392 newtag,leftExpr,rightExpr);
393 }
394
395 case TagConstants.SUBTYPE: {
396 if(true) { break; } else { notImpl(e); }
397 return null;
398 }
399
400 // Other expressions
401
402 case TagConstants.CONDEXPR: {
403 if(true) { break; } else { notImpl(e); }
404 return null;
405 }
406
407 case TagConstants.INSTANCEOFEXPR: {
408 break;
409 }
410
411 case TagConstants.CASTEXPR: {
412 if(true) { break; } else { notImpl(e); }
413 return null;
414 }
415
416 case TagConstants.CLASSLITERAL: {
417 if(true) { break; } else { notImpl(e); }
418 return null;
419 }
420
421 case TagConstants.TYPEEXPR: {
422 break;
423 }
424
425 case TagConstants.REACH: {
426 if(true) { break; } else { notImpl(e); }
427 return null;
428 }
429
430 case TagConstants.NUM_OF:
431 case TagConstants.SUM:
432 case TagConstants.PRODUCT: {
433 if(true) { break; } else { notImpl(e); }
434 return null;
435 }
436
437 case TagConstants.MIN:
438 case TagConstants.MAXQUANT: {
439 if(true) { break; } else { notImpl(e); }
440 return null;
441 }
442
443 case TagConstants.FORALL:
444 case TagConstants.EXISTS: {
445 if(true) { break; } else { notImpl(e); }
446 return null;
447 }
448
449 case TagConstants.SETCOMPEXPR: {
450 if(true) { break; } else { notImpl(e); }
451 return null;
452 }
453
454 case TagConstants.LABELEXPR: {
455 LabelExpr le = (LabelExpr)e;
456 return LabelExpr.make(le.getStartLoc(),
457 le.getEndLoc(),
458 le.positive,
459 le.label,
460 this.trAndGen(le.expr));
461 }
462
463 case TagConstants.PRE: {
464 if(true) { break; } else { notImpl(e); }
465 return null;
466 }
467
468 case TagConstants.FRESH: {
469 if(true) { break; } else { notImpl(e); }
470 return null;
471 }
472
473 case TagConstants.DOTDOT: {
474 if(true) { break; } else { notImpl(e); }
475 return null;
476 }
477
478 case TagConstants.NOWARN_OP:
479 case TagConstants.WACK_NOWARN:
480 case TagConstants.WARN_OP:
481 case TagConstants.WARN: {
482 if(true) { break; } else { notImpl(e); }
483 return null;
484 }
485
486 case TagConstants.IS_INITIALIZED:
487 case TagConstants.INVARIANT_FOR: {
488 if(true) { break; } else { notImpl(e); }
489 return null;
490 }
491
492 case TagConstants.SPACE:
493 case TagConstants.WACK_WORKING_SPACE:
494 case TagConstants.WACK_DURATION: {
495 if(true) { break; } else { notImpl(e); }
496 return null;
497 }
498
499 case TagConstants.NOTHINGEXPR:
500 case TagConstants.EVERYTHINGEXPR:
501 return null;
502
503 case TagConstants.NOTMODIFIEDEXPR: {
504 if(true) { break; } else { notImpl(e); }
505 return null;
506 }
507
508 default:
509 Assert.fail("UnknownTag<"+e.getTag()+","+
510 TagConstants.toString(e.getTag())+"> on "+e+ " " +
511 Location.toString(e.getStartLoc()));
512 return null; // dummy return
513 }
514
515 // In all cases that fall through, simply translate e into a GC expr.
516 return TrAnExpr.trSpecExpr(e, minHMap4Tr(), null);
517 }
518
519 private void notImpl(Expr e) {
520 ErrorSet.notImplemented(!Main.options().noNotCheckedWarnings,
521 e.getStartLoc(), e.toString());
522 }
523
524 private Hashtable minHMap4Tr() {
525 // The returned map is only needed for constructors, but since
526 // general type checking will have been done, we can simply
527 // use the same map in all cases (constructor or not).
528 Hashtable map = new Hashtable();
529 map.put(GC.thisvar.decl, GC.resultvar);
530 return(map);
531 }
532
533 private String traceMethod() {
534 Throwable t=new Throwable();
535 StackTraceElement [] stes=t.getStackTrace();
536 if (stes!=null || stes.length!=0)
537 {
538 return("GK-Trace : " + stes[1]);
539 }
540 return("GK-Trace : NA");
541 }
542 }