001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003
004 package escjava.translate;
005
006 import java.util.Hashtable;
007 import java.util.Enumeration;
008 import javafe.ast.*;
009 import javafe.tc.*;
010 import javafe.util.Location;
011 import javafe.util.Assert;
012 import javafe.util.Info;
013 import javafe.util.StackVector;
014 import escjava.ast.*;
015 import escjava.ast.TagConstants;
016 import escjava.tc.Types;
017 import escjava.Main;
018
019 public final class GC {
020
021 //// Makers for guarded commands
022
023 //@ ensures \result != null;
024 public static GuardedCmd block(/*@ non_null @*/ GenericVarDeclVec v,
025 /*@ non_null @*/ GuardedCmd g)
026 {
027 if (v.size() == 0)
028 return g;
029 else
030 return VarInCmd.make(v, g);
031 }
032
033 //@ ensures \result != null;
034 public static GuardedCmd blockL(Stmt label, GuardedCmd g) {
035 return trycmd(g, ifcmd( nary(TagConstants.ANYEQ,
036 ecvar,
037 symlit(label, "L_")),
038 skip(),
039 raise()));
040 }
041
042 /** Requires <code>0 < cmds.size()</code>. */
043 public static GuardedCmd seq(/*@ non_null @*/ GuardedCmd g1,
044 /*@ non_null @*/ GuardedCmd g2)
045 { GuardedCmd[] cvec= {g1,g2};
046 return seq(GuardedCmdVec.make(cvec)); }
047
048 public static GuardedCmd seq(/*@ non_null @*/ GuardedCmd g1,
049 /*@ non_null @*/ GuardedCmd g2,
050 /*@ non_null @*/ GuardedCmd g3 )
051 { GuardedCmd[] cvec= {g1,g2,g3};
052 return seq(GuardedCmdVec.make(cvec)); }
053
054 public static GuardedCmd seq(/*@ non_null @*/ GuardedCmd g1,
055 /*@ non_null @*/ GuardedCmd g2,
056 /*@ non_null @*/ GuardedCmd g3,
057 /*@ non_null @*/ GuardedCmd g4 )
058 { GuardedCmd[] cvec= {g1,g2,g3,g4};
059 return seq(GuardedCmdVec.make(cvec)); }
060
061 /** May mutilate contents of <code>cmds</code>. The caller is expected
062 * not to use <code>cmds</code> after this call.
063 **/
064
065 //@ ensures \result != null;
066 public static GuardedCmd seq(/*@ non_null */ GuardedCmdVec cmds) {
067 int n;
068 if (!Main.options().peepOptGC) {
069 n = cmds.size();
070 } else {
071 n = 0;
072 LOOP: for (int i = 0; i < cmds.size(); i++) {
073 GuardedCmd g = cmds.elementAt(i);
074 int tag = g.getTag();
075 switch (tag) {
076 case TagConstants.SKIPCMD:
077 // don't keep (that is, don't copy and don't increment "n"
078 break;
079
080 case TagConstants.RAISECMD:
081 cmds.setElementAt(g, n);
082 n++;
083 // don't keep any further commands, since they won't
084 // be reached anyway
085 break LOOP;
086
087 case TagConstants.ASSERTCMD:
088 case TagConstants.ASSUMECMD:
089 {
090 cmds.setElementAt(g, n);
091 n++;
092 if ((tag != TagConstants.ASSERTCMD ||
093 !Main.options().noPeepOptGCAssertFalse) &&
094 isFalse(((ExprCmd)g).pred)) {
095 // don't keep any further commands, since they won't
096 // be reached anyway
097 break LOOP;
098 }
099 break;
100 }
101
102 default:
103 cmds.setElementAt(g, n);
104 n++;
105 break;
106 }
107 }
108 }
109 if (n == 0)
110 return SimpleCmd.make(TagConstants.SKIPCMD, Location.NULL);
111 if (n == 1)
112 return cmds.elementAt(0);
113 for (int elementsToBeRemoved = cmds.size() - n;
114 elementsToBeRemoved != 0; elementsToBeRemoved--) {
115 cmds.pop();
116 }
117 return SeqCmd.make(cmds);
118 }
119
120 //@ ensures \result != null;
121 public static GuardedCmd gets(/*@ non_null @*/ VariableAccess lhs,
122 /*@ non_null @*/ Expr rhs) {
123 return GetsCmd.make(lhs, rhs);
124 }
125
126 //@ ensures \result != null;
127 public static GuardedCmd subgets(/*@ non_null @*/ VariableAccess lhs,
128 /*@ non_null @*/ Expr index,
129 /*@ non_null @*/ Expr rhs) {
130 return SubGetsCmd.make(lhs, rhs, index);
131 }
132
133 //@ ensures \result != null;
134 public static GuardedCmd subsubgets(/*@ non_null @*/ VariableAccess lhs,
135 /*@ non_null @*/ Expr array,
136 /*@ non_null @*/ Expr index,
137 /*@ non_null @*/ Expr rhs) {
138 return SubSubGetsCmd.make(lhs, rhs, array, index);
139 }
140
141 //@ ensures \result != null;
142 public static GuardedCmd restoreFrom(/*@ non_null @*/ VariableAccess lhs,
143 /*@ non_null @*/ Expr rhs) {
144 return RestoreFromCmd.make(lhs, rhs);
145 }
146
147 //@ ensures \result != null;
148 public static GuardedCmd raise() {
149 return SimpleCmd.make(TagConstants.RAISECMD, Location.NULL);
150 }
151
152 //@ ensures \result != null;
153 public static GuardedCmd skip() {
154 return SimpleCmd.make(TagConstants.SKIPCMD, Location.NULL);
155 }
156
157 public static LoopCmd loop(int sLoop, int eLoop, int locHotspot,
158 /*@ non_null @*/ Hashtable oldmap,
159 /*@ non_null @*/ ConditionVec J,
160 /*@ non_null @*/ DecreasesInfoVec decs,
161 /*@ non_null @*/ LocalVarDeclVec skolemConsts,
162 /*@ non_null @*/ ExprVec P,
163 /*@ non_null @*/ GenericVarDeclVec tempVars,
164 /*@ non_null @*/ GuardedCmd B,
165 /*@ non_null @*/ GuardedCmd S) {
166 return LoopCmd.make(sLoop, eLoop, locHotspot, oldmap, J, decs,
167 skolemConsts, P, tempVars, B, S);
168 }
169
170 //@ ensures \result != null;
171 public static GuardedCmd ifcmd(/*@ non_null @*/ Expr t,
172 /*@ non_null @*/ GuardedCmd c,
173 /*@ non_null @*/ GuardedCmd a)
174 {
175 GuardedCmd thn = GC.seq(GC.assume(t), c);
176 GuardedCmd els = GC.seq(GC.assumeNegation(t), a);
177 return choosecmd(thn, els);
178 }
179
180 /** Pops two command sequences off <code>s</code>, call them <code>a</code>
181 and <code>b</code>. Then returns the box composition of these
182 commands, that is, <code>a [] b</code>. */
183
184 //@ ensures \result != null;
185 public static GuardedCmd boxPopFromStackVector(/*@ non_null @*/ StackVector s) {
186 GuardedCmdVec b = GuardedCmdVec.popFromStackVector(s);
187 GuardedCmdVec a = GuardedCmdVec.popFromStackVector(s);
188 return choosecmd(GC.seq(a), GC.seq(b));
189 }
190
191 //@ ensures \result != null;
192 public static GuardedCmd choosecmd(/*@ non_null @*/ GuardedCmd a,
193 /*@ non_null @*/ GuardedCmd b)
194 {
195 if (Main.options().peepOptGC) {
196 if (a.getTag() == TagConstants.ASSUMECMD && isFalse(((ExprCmd)a).pred)) {
197 return b;
198 }
199 if (b.getTag() == TagConstants.ASSUMECMD && isFalse(((ExprCmd)b).pred)) {
200 return a;
201 }
202 if (a.getTag() == TagConstants.ASSERTCMD && isFalse(((ExprCmd)a).pred)) {
203 return a;
204 }
205 if (b.getTag() == TagConstants.ASSERTCMD && isFalse(((ExprCmd)b).pred)) {
206 return b;
207 }
208 }
209 return CmdCmdCmd.make(TagConstants.CHOOSECMD, a, b);
210 }
211
212 //@ ensures \result != null;
213 public static GuardedCmd trycmd(/*@ non_null @*/ GuardedCmd c,
214 /*@ non_null @*/ GuardedCmd a) {
215 if (Main.options().peepOptGC) {
216 if (a.getTag() == TagConstants.RAISECMD) {
217 return c;
218 }
219 // It would be nice to do the following:
220 // if (!canRaise(c)) {
221 // return c;
222 // }
223 // but we don't keep track of the possible outcomes of expressions,
224 // and thus we'd end up spending quadratic time. Instead, we do:
225 switch (c.getTag()) {
226 case TagConstants.SKIPCMD:
227 return c;
228
229 case TagConstants.RAISECMD:
230 return a;
231
232 case TagConstants.GETSCMD:
233 case TagConstants.SUBGETSCMD:
234 case TagConstants.SUBSUBGETSCMD:
235 case TagConstants.RESTOREFROMCMD:
236 case TagConstants.ASSERTCMD:
237 case TagConstants.ASSUMECMD:
238 return c;
239
240 default:
241 break;
242 }
243 }
244 return CmdCmdCmd.make(TagConstants.TRYCMD, c, a);
245 }
246
247 /** Returns <code>true</code> when <code>e</code> is a boolean
248 * literal expression whose value is <code>b</code>.
249 **/
250 public static boolean isBooleanLiteral(/*@ non_null */ Expr e, boolean b) {
251 if (e.getTag() == TagConstants.BOOLEANLIT) {
252 LiteralExpr le = (LiteralExpr)e;
253 if (le.value != null) {
254 Boolean bb = (Boolean)le.value;
255 return bb.booleanValue() == b;
256 }
257 } else if( e.getTag() == TagConstants.BOOLNOT) {
258 return isBooleanLiteral( ((NaryExpr)e).exprs.elementAt(0), !b );
259 }
260 return false;
261 }
262
263 /** Returns <code>true</code> only if <code>e</code> represents an
264 * expression equivalent to <code>false</code>. This method may
265 * return <code>false</code> under any circumstance, but tries to
266 * use cheap methods to figure out whether <code>e</code> is equivalent
267 * to <code>false</code>, in which case <code>true</code> is returned.
268 **/
269
270 public static boolean isFalse(/*@ non_null @*/ Expr e) {
271 // first strip off any Simplify label
272 while (e.getTag() == TagConstants.LABELEXPR) {
273 LabelExpr le = (LabelExpr)e;
274 e = le.expr;
275 }
276
277 return isBooleanLiteral(e, false);
278 }
279
280 /** Creates an assert, assume, or skip command, depending on
281 the kind of given error name and locations, and depending on what
282 checks are enabled where. There are two versions of the
283 <code>check</code> method.
284
285 In the first version, <code>errorName</code> is the error name
286 (that is, the tag constant of the type of check), <code>pred</code>
287 evaluates to <code>false</code> if the check goes wrong,
288 <code>locUse</code> is the source location of the command or
289 expression that can go wrong, and <code>locPragmaDecl</code> is
290 the location of the associated pragma, if any (or <code>Location.NULL</code>
291 if not applicable).
292
293 In the second version, <code>errorName</code>, <code>pred</code>,
294 and <code>locPragmaDecl</code> are taken from the components of the
295 given condition <code>cond</code>. */
296
297 //@ ensures \result != null;
298 public static GuardedCmd check(int locUse,
299 int errorName,
300 /*@ non_null @*/ Expr pred,
301 int locPragmaDecl) {
302 return check(locUse, errorName, pred, locPragmaDecl, null);
303 }
304
305 //@ ensures \result != null;
306 public static GuardedCmd check(int locUse,
307 int errorName,
308 /*@ non_null @*/ Expr pred,
309 int locPragmaDecl,
310 /*@ non_null @*/ Object aux) {
311 return check(locUse,errorName, pred, locPragmaDecl, Location.NULL,aux);
312 }
313
314 //@ ensures \result != null;
315 public static GuardedCmd check(int locUse,
316 int errorName,
317 /*@ non_null @*/ Expr pred,
318 int locPragmaDecl,
319 int auxLoc,
320 /*@ non_null @*/ Object aux) {
321 //Assert.notFalse(locUse != Location.NULL);
322 if (Main.options().guardedVC && locPragmaDecl != Location.NULL) {
323 pred = GuardExpr.make(pred, locPragmaDecl);
324 }
325 switch( NoWarn.getChkStatus( errorName, locUse, locPragmaDecl) ) {
326 case TagConstants.CHK_AS_ASSUME:
327 LabelInfoToString.recordAnnotationAssumption(locPragmaDecl);
328 return assume(pred);
329 case TagConstants.CHK_AS_ASSERT:
330 LabelInfoToString.recordAnnotationAssumption(locPragmaDecl);
331 return assertPredicate(locUse, errorName, pred, locPragmaDecl, auxLoc, aux);
332 case TagConstants.CHK_AS_SKIP:
333 return skip();
334 default:
335 Assert.fail("unreachable");
336 return null; // dummy return
337 }
338
339 }
340
341
342 /** See description of <code>check</code> above. */
343
344 //@ ensures \result != null;
345 public static GuardedCmd check(int locUse, /*@ non_null @*/ Condition cond) {
346 Assert.notFalse(locUse != Location.NULL);
347 return check(locUse, cond.label, cond.pred, cond.locPragmaDecl, null);
348 }
349
350 /** See description of <code>check</code> above. */
351
352 //@ ensures \result != null;
353 public static GuardedCmd check(int locUse,
354 /*@ non_null @*/ Condition cond,
355 /*@ non_null @*/ Object aux)
356 {
357 Assert.notFalse(locUse != Location.NULL);
358 return check(locUse, cond.label, cond.pred, cond.locPragmaDecl, aux);
359 }
360
361 //@ requires label != TagConstants.CHKFREE;
362 //@ ensures \result != null;
363 public static Condition condition(int label,
364 /*@ non_null @*/ Expr pred,
365 int locPragmaDecl) {
366 Assert.notFalse(label != TagConstants.CHKFREE);
367 return Condition.make(label, pred, locPragmaDecl);
368 }
369
370 //@ ensures \result != null;
371 public static Condition freeCondition(/*@ non_null @*/ Expr pred, int locPragmaDecl) {
372 return Condition.make(TagConstants.CHKFREE, pred, locPragmaDecl);
373 }
374
375 //@ ensures \result != null;
376 public static Condition assumeCondition(/*@ non_null @*/ Expr pred, int locPragmaDecl) {
377 return Condition.make(TagConstants.CHKASSUME, pred, locPragmaDecl);
378 }
379
380 //@ requires locPragmaDecl != Location.NULL;
381 //@ ensures \result != null;
382 public static GuardedCmd assumeAnnotation(int locPragmaDecl,
383 /*@ non_null */ Expr p) {
384 if (Main.options().guardedVC && locPragmaDecl != Location.NULL) {
385 p = GuardExpr.make(p, locPragmaDecl);
386 }
387 LabelInfoToString.recordAnnotationAssumption(locPragmaDecl);
388 return assume(p);
389 }
390
391 //@ ensures \result != null;
392 public static GuardedCmd assume(/*@ non_null @*/ Expr p)
393 {
394 if (Main.options().peepOptGC && isBooleanLiteral(p, true)) {
395 return skip();
396 }
397 if (p.getTag() == TagConstants.BOOLAND && (p instanceof NaryExpr)
398 && ((NaryExpr)p).exprs.size() > 1) {
399 // An optimization that makes ASSUME commands simpler - unpacks an AND
400 // into multiple ASSUMEs to make reading easier.
401 NaryExpr ne = (NaryExpr)p;
402 GuardedCmdVec gcv = GuardedCmdVec.make(ne.exprs.size());
403 for (int i=0; i<ne.exprs.size(); ++i) {
404 Expr e = ne.exprs.elementAt(i);
405 ExprCmd a = ExprCmd.make(TagConstants.ASSUMECMD, e, Location.NULL);
406 gcv.addElement(a);
407 }
408 return GC.seq(gcv);
409 }
410 if (p.getTag() == TagConstants.FORALL && (p instanceof QuantifiedExpr)) {
411 // This is an optimization that changes a Forall of a boolean and into
412 // a sequence of foralls of the conjuncts.
413 QuantifiedExpr qe = (QuantifiedExpr)p;
414 if (qe.expr.getTag() == TagConstants.BOOLAND) {
415 ExprVec ev = ((NaryExpr)qe.expr).exprs;
416 if (ev.size() > 1) {
417 GuardedCmdVec gcv = GuardedCmdVec.make(ev.size());
418 for (int i=0; i<ev.size(); ++i) {
419 Expr e = QuantifiedExpr.make(qe.sloc,qe.eloc,qe.quantifier,
420 qe.vars,qe.rangeExpr,ev.elementAt(i),qe.nopats,qe.pats);
421 ExprCmd a = ExprCmd.make(TagConstants.ASSUMECMD, e, Location.NULL);
422 gcv.addElement(a);
423 }
424 return GC.seq(gcv);
425 }
426 }
427 }
428 return ExprCmd.make(TagConstants.ASSUMECMD, p, Location.NULL);
429 }
430
431 //@ ensures \result != null;
432 public static GuardedCmd assumeNegation(/*@ non_null @*/ Expr p) {
433 Expr non_p = not(p.getStartLoc(), p.getEndLoc(), p);
434 return assume(non_p);
435 }
436
437 //@ ensures \result != null;
438 public static GuardedCmd fail() {
439 return assume(falselit);
440 }
441
442 private static int assertContinueCounter = 0;
443
444 // //@ requires locUse != Location.NULL;
445 // private static GuardedCmd assertPredicate(int locUse,
446 // int errorName, Expr pred,
447 // int locPragmaDecl,
448 // Object aux) {
449 // return assertPredicate(locUse, errorName, pred, locPragmaDecl,
450 // Location.NULL, aux);
451 // }
452
453 //@ ensures \result != null;
454 private static GuardedCmd assertPredicate(int locUse,
455 int errorName,
456 /*@ non_null @*/ Expr pred,
457 int locPragmaDecl,
458 int auxLoc,
459 /*@ non_null @*/ Object aux) {
460 if (Main.options().assertContinue) {
461 Identifier idn = Identifier.intern("assertContinue" +
462 assertContinueCounter);
463 assertContinueCounter++;
464 VariableAccess acVar = makeVar(idn, locUse);
465 acVar.loc = Location.NULL;
466 pred = or(pred, acVar);
467 }
468 if (errorName != TagConstants.CHKQUIET) {
469 String name = TagConstants.toString(errorName);
470 if (aux != null && Main.options().suggest) {
471 int n = AuxInfo.put(aux);
472 name += "/" + n;
473 }
474 Identifier en = makeLabel(name,locPragmaDecl,auxLoc,locUse);
475 pred = LabelExpr.make(locUse, locUse, false, en, pred);
476 }
477 return ExprCmd.make(TagConstants.ASSERTCMD, pred, locUse);
478 }
479
480 //@ ensures \result != null;
481 public static Identifier makeLabel(/*@ non_null @*/ String name,
482 int locPragmaDecl, int auxLoc, int locUse) {
483 String lab = name;
484 if (locPragmaDecl != Location.NULL) {
485 lab = lab + ":" + UniqName.locToSuffix(locPragmaDecl);
486 }
487 if (auxLoc != Location.NULL) {
488 lab = lab + ":" + UniqName.locToSuffix(auxLoc);
489 }
490 if (locUse != Location.NULL)
491 lab += "@" + UniqName.locToSuffix(locUse);
492 return Identifier.intern(lab);
493 }
494
495 //@ ensures \result != null;
496 public static Identifier makeLabel(/*@ non_null @*/ String name,
497 int locPragmaDecl, int locUse) {
498 String lab = name;
499 if (locPragmaDecl != Location.NULL) {
500 lab = lab + ":" + UniqName.locToSuffix(locPragmaDecl);
501 }
502 if (locUse != Location.NULL)
503 lab += "@" + UniqName.locToSuffix(locUse);
504 return Identifier.intern(lab);
505 }
506
507 //@ ensures \result != null;
508 public static Identifier makeFullLabel(/*@ non_null @*/ String name,
509 int locPragmaDecl, int locUse)
510 {
511 String lab = name;
512 if (locPragmaDecl != Location.NULL) {
513 lab = lab + ":" + UniqName.locToSuffix(locPragmaDecl,false);
514 }
515 if (locUse != Location.NULL)
516 lab += "@" + UniqName.locToSuffix(locUse,false);
517 return Identifier.intern(lab);
518 }
519
520 //@ requires subst != null && target != null ;
521 //+@ requires subst.keyType == \type(GenericVarDecl) ;
522 //+@ requires subst.elementType <: \type(Expr) ;
523 public static Expr subst(int sloc, int eloc, Hashtable subst, Expr target)
524 {
525 if ( !Main.options().lazySubst ) {
526 // perform substitution eagerly
527
528 return Substitute.doSubst( subst, target );
529
530 } else {
531 // create lazy substitutions
532
533 for(Enumeration e = subst.keys(); e.hasMoreElements(); )
534 {
535 GenericVarDecl vd = (GenericVarDecl)e.nextElement();
536 Expr to = (Expr)subst.get( vd );
537 target = subst(sloc, eloc, vd, to, target);
538 }
539 return target;
540 }
541 }
542
543 //@ requires target != null ;
544 //@ requires var!=null && val!=null;
545 public static Expr subst(int sloc, int eloc,
546 GenericVarDecl var, Expr val, Expr target) {
547 if ( !Main.options().lazySubst ) {
548 // perform substitution eagerly
549 Hashtable t = new Hashtable();
550 t.put( var, val );
551 return subst( sloc, eloc, t, target );
552 } else {
553 return SubstExpr.make( sloc, eloc, var, val, target );
554 }
555 }
556
557 //@ requires target != null ;
558 //@ requires var != null && val!=null;
559 public static Expr subst(GenericVarDecl var, Expr val, Expr target) {
560 return subst( Location.NULL, Location.NULL, var, val, target );
561 }
562
563
564 //// Makers for literals
565
566 public static final /*@ non_null @*/ Expr nulllit =
567 LiteralExpr.make(TagConstants.NULLLIT, null, Location.NULL);
568
569 public static final /*@ non_null @*/ Expr zerolit =
570 LiteralExpr.make(TagConstants.INTLIT, new Integer(0), Location.NULL);
571
572 public static final /*@ non_null @*/ Expr onelit =
573 LiteralExpr.make(TagConstants.INTLIT, new Integer(1), Location.NULL);
574
575 public static final /*@ non_null @*/ Expr truelit =
576 LiteralExpr.make(TagConstants.BOOLEANLIT,Boolean.TRUE,Location.NULL);
577
578 public static final /*@ non_null @*/ Expr falselit =
579 LiteralExpr.make(TagConstants.BOOLEANLIT,Boolean.FALSE,Location.NULL);
580
581 public static final /*@ non_null @*/ Expr dzerolit =
582 LiteralExpr.make(TagConstants.DOUBLELIT, new Double(0.0), Location.NULL);
583
584 //@ ensures \result != null;
585 public static Expr symlit(/*null*/ String s) {
586 return LiteralExpr.make(TagConstants.SYMBOLLIT, s, Location.NULL);
587 }
588
589 //@ ensures \result != null;
590 public static Expr symlit(/*@ non_null @*/ Stmt s, /*@ non_null @*/ String prefix) {
591 return symlit(prefix + UniqName.locToSuffix(s.getStartLoc()));
592 }
593
594 //@ ensures \result != null;
595 public static Expr zeroequiv(/*@ non_null @*/ Type t) {
596 switch (t.getTag()) {
597 case TagConstants.ARRAYTYPE:
598 case TagConstants.NULLTYPE:
599 case TagConstants.TYPENAME:
600 case TagConstants.TYPESIG:
601 return nulllit;
602
603 case TagConstants.BOOLEANTYPE:
604 return falselit;
605
606 case TagConstants.INTTYPE:
607 case TagConstants.LONGTYPE:
608 case TagConstants.CHARTYPE:
609 case TagConstants.BYTETYPE:
610 case TagConstants.SHORTTYPE:
611 return zerolit;
612
613 case TagConstants.DOUBLETYPE:
614 case TagConstants.FLOATTYPE:
615 return dzerolit;
616 }
617 /*@ unreachable; */
618 Assert.fail("Bad tag");
619 return null;
620 }
621
622
623 //// Makers for variables
624
625 //@ ensures \result != null;
626 public static VariableAccess makeVar(/*@ non_null @*/ Identifier name, int locId) {
627 LocalVarDecl v
628 = LocalVarDecl.make(0, null, name, Types.anyType, locId,
629 null, Location.NULL);
630 return VariableAccess.make(name, Location.NULL, v);
631 }
632
633 //@ ensures \result != null;
634 public static VariableAccess makeVar(/*@ non_null @*/ String name, int locId) {
635 return makeVar(Identifier.intern(name), locId);
636 }
637
638 //@ ensures \result != null;
639 public static VariableAccess makeFormalPara(/*@ non_null @*/ String name,
640 /*@ non_null @*/ Type type,
641 int locId) {
642 Identifier nameId = Identifier.intern(name);
643 FormalParaDecl v
644 = FormalParaDecl.make(0, null, nameId, type, locId);
645 return VariableAccess.make( Identifier.intern(name), Location.NULL, v);
646 }
647
648
649 //@ ensures \result != null;
650 public static VariableAccess makeVar(/*@ non_null @*/ String name) {
651 return makeVar(name, Location.NULL);
652 }
653
654 //@ ensures \result != null;
655 public static VariableAccess makeVar(/*@ non_null @*/ Identifier name) {
656 return makeVar(name, Location.NULL);
657 }
658
659 //@ ensures \result != null;
660 public static VariableAccess makeFormalPara(/*@ non_null @*/ String name,
661 /*@ non_null @*/ Type type) {
662 return makeFormalPara(name, type, Location.NULL);
663 }
664
665 //@ ensures \result != null;
666 public static VariableAccess makeFormalPara(/*@ non_null @*/ String name) {
667 return makeFormalPara(name, Types.anyType);
668 }
669
670
671 public static final /*@ non_null @*/ VariableAccess allocvar = makeVar("alloc",
672 UniqName.specialVariable);
673 public static final /*@ non_null @*/ VariableAccess ecvar = makeVar("EC",
674 UniqName.specialVariable);
675 public static final /*@ non_null @*/ VariableAccess elemsvar = makeVar("elems",
676 UniqName.specialVariable);
677 public static final /*@ non_null @*/ VariableAccess resultvar = makeVar("RES",
678 UniqName.specialVariable);
679 public static final /*@ non_null @*/ VariableAccess xresultvar = makeVar("XRES",
680 UniqName.specialVariable);
681 public static final /*@ non_null @*/ VariableAccess objectTBCvar = makeVar("objectToBeConstructed",
682 UniqName.specialVariable);
683 public static final /*@ non_null @*/ VariableAccess statevar = makeVar("state",
684 UniqName.specialVariable);
685
686 // LSvar is not final because it is temporarily updated at
687 // synchronized expressions. See trExpr
688 public static VariableAccess LSvar = makeVar("LS",
689 UniqName.specialVariable);
690
691
692 /*
693 * The type of thisvar (thisvar.decl.type) is set by
694 * Translate.trBody. It is also temporarily changed by
695 * GetSpec.trMethodDecl.
696 */
697 //@ invariant thisvar.decl.type instanceof TypeSig;
698 public static final /*@ non_null @*/ VariableAccess thisvar =
699 makeFormalPara("this", javafe.tc.Types.javaLangObject(),
700 UniqName.specialVariable);
701
702
703 /*
704 * These handle case 5 of ESCJ 23b:
705 */
706 public static final /*@ non_null @*/ Expr ec_throw = symlit("ecThrow");
707 public static final /*@ non_null @*/ Expr ec_return = symlit("ecReturn");
708
709 //// Makers for expressions
710
711 //@ ensures \result != null;
712 public static Expr typeExpr(/*@ non_null @*/ Type t)
713 { return TypeExpr.make(Location.NULL, Location.NULL, t); }
714
715 public static Expr cast(/*@ non_null @*/ Expr e,
716 /*@ non_null @*/ Type t)
717 {
718 if (e instanceof LiteralExpr)
719 return LiteralExpr.cast((LiteralExpr)e,
720 t == Types.doubleType ? TagConstants.DOUBLELIT :
721 t == Types.floatType ? TagConstants.FLOATLIT :
722 t == Types.longType ? TagConstants.LONGLIT :
723 TagConstants.INTLIT);
724 return nary(TagConstants.CAST, e, typeExpr(t));
725 }
726
727 // Various forms of nary()
728
729 //@ ensures \result != null;
730 public static Expr nary(int tag, /*@ non_null */ Expr e) {
731 return nary(Location.NULL, Location.NULL, tag, e);
732 }
733
734 //@ ensures \result != null;
735 public static Expr nary(int sloc, int eloc, int tag,
736 /*@ non_null */ Expr e) {
737 Expr[] args = { e };
738 return nary( sloc, eloc, tag, ExprVec.make(args));
739 }
740
741 //@ ensures \result != null;
742 public static Expr nary(int tag,
743 /*@ non_null */ Expr e1, /*@ non_null */ Expr e2) {
744 return nary(Location.NULL, Location.NULL, tag, e1, e2);
745 }
746
747 //@ ensures \result != null;
748 public static Expr nary(int sloc, int eloc, int tag,
749 /*@ non_null */ Expr e1, /*@ non_null */ Expr e2) {
750 Expr[] args = { e1, e2 };
751 return nary(sloc,eloc,tag, ExprVec.make(args));
752 }
753
754 //@ ensures \result != null;
755 public static Expr nary(int tag, /*@ non_null */ Expr e1,
756 /*@ non_null */ Expr e2, /*@ non_null */ Expr e3) {
757 return nary(Location.NULL, Location.NULL, tag, e1, e2, e3);
758 }
759
760 //@ ensures \result != null;
761 public static Expr nary(int sloc, int eloc, int tag,
762 /*@ non_null */ Expr e1, /*@ non_null */ Expr e2,
763 /*@ non_null */ Expr e3) {
764 Expr[] args = { e1, e2, e3 };
765 return nary(sloc,eloc,tag, ExprVec.make(args));
766 }
767
768 //@ ensures \result != null;
769 public static Expr nary(int tag, /*@ non_null @*/ ExprVec ev) {
770 return nary(Location.NULL, Location.NULL, tag, ev);
771 }
772
773 //@ ensures \result != null;
774 public static Expr nary(/*@ non_null @*/ Identifier id, /*@ non_null @*/ ExprVec ev) {
775 Expr e = nary(Location.NULL, Location.NULL, TagConstants.METHODCALL, ev);
776 ((NaryExpr)e).methodName = id;
777 return e;
778 }
779
780 //@ ensures \result != null;
781 public static Expr nary(/*@ non_null @*/ Identifier id, /*@ non_null @*/ Expr e) {
782 ExprVec ev = ExprVec.make(1);
783 ev.addElement(e);
784 return nary(id,ev);
785 }
786
787 //@ ensures \result != null;
788 public static Expr nary(/*@ non_null @*/ Identifier id,
789 /*@ non_null @*/ Expr e1,
790 /*@ non_null @*/ Expr e2)
791 {
792 ExprVec ev = ExprVec.make(2);
793 ev.addElement(e1);
794 ev.addElement(e2);
795 return nary(id,ev);
796 }
797
798 //@ ensures \result != null;
799 public static Expr nary(int sloc, int eloc,
800 /*@ non_null @*/ Identifier id,
801 /*@ non_null @*/ ExprVec ev)
802 {
803 Expr e = nary(sloc, eloc, TagConstants.METHODCALL, ev);
804 ((NaryExpr)e).methodName = id;
805 return e;
806 }
807
808 //@ ensures \result != null;
809 public static Expr nary(int sloc, int eloc, int tag,
810 /*@ non_null @*/ ExprVec ev)
811 {
812 if( Main.options().peepOptE ) {
813 // Do some optimizations ...
814
815 switch( tag ) {
816 case TagConstants.BOOLAND:
817 case TagConstants.BOOLANDX:
818 {
819 ExprVec w = ExprVec.make( ev.size() );
820 if( selectiveAdd( w, ev, truelit, falselit,
821 tag ) )
822 {
823 return falselit;
824 }
825
826 if( w.size() == 0 )
827 return truelit;
828 else if( w.size() == 1 )
829 return w.elementAt(0);
830 else
831 return NaryExpr.make( sloc, eloc, tag, null, w);
832 }
833
834 case TagConstants.BOOLOR:
835 {
836 ExprVec w = ExprVec.make( ev.size() );
837 if( selectiveAdd( w, ev, falselit, truelit,
838 TagConstants.BOOLOR ) )
839 {
840 return truelit;
841 }
842
843 if( w.size() == 0 )
844 return falselit;
845 else if( w.size() == 1 )
846 return w.elementAt(0);
847 else
848 return NaryExpr.make( sloc, eloc, TagConstants.BOOLOR, null, w);
849 }
850
851 case TagConstants.BOOLIMPLIES:
852 {
853 Expr c0 = ev.elementAt(0);
854 Expr c1 = ev.elementAt(1);
855
856 if( Main.options().bubbleNotDown ) {
857 return or( sloc, eloc,
858 not( sloc, eloc, c0 ),
859 c1 );
860 } else {
861 // Change a ==> (b ==> c) to (a ^ b) ==> c
862 if(c1.getTag() == TagConstants.BOOLIMPLIES ) {
863 NaryExpr ne = (NaryExpr)c1;
864 return implies( sloc, eloc,
865 and( sloc, eloc, c0, ne.exprs.elementAt(0) ),
866 ne.exprs.elementAt(1) );
867 } else if (isBooleanLiteral(c0, false)) {
868 // false ==> X --> true
869 return GC.truelit;
870 } else if (isBooleanLiteral(c1, true)) {
871 // X ==> true --> true
872 return GC.truelit;
873 } else if (isBooleanLiteral(c0, true)) {
874 // true ==> X --> X
875 return c1;
876 } else if (isBooleanLiteral(c1, false)) {
877 // X ==> false --> !X
878 return nary(sloc, eloc, TagConstants.BOOLNOT, c0);
879 } else {
880 break; // go to default case
881 }
882 }
883 }
884
885 case TagConstants.BOOLNOT:
886 // Change (not (and a b)) -> (or (not a) (not b)), etc
887 // Also (not (not a)) -> a
888 {
889 Expr c0 = ev.elementAt(0);
890 if (isBooleanLiteral(c0, false)) {
891 return truelit;
892 } else if (isBooleanLiteral(c0, true)) {
893 return falselit;
894 } else if ( c0.getTag() == TagConstants.BOOLNOT ) {
895 return ((NaryExpr)c0).exprs.elementAt(0);
896 } else if( Main.options().bubbleNotDown ) {
897 switch( c0.getTag() ) {
898 case TagConstants.BOOLOR:
899 case TagConstants.BOOLAND:
900 case TagConstants.BOOLANDX:
901 {
902 ExprVec w = ((NaryExpr)c0).exprs;
903 ExprVec r = ExprVec.make();
904 for(int i=0; i<w.size(); i++) {
905 r.addElement( not( sloc, eloc, w.elementAt(i)));
906 }
907 return nary( sloc, eloc,
908 c0.getTag() == TagConstants.BOOLOR ?
909 TagConstants.BOOLAND : TagConstants.BOOLOR,
910 r );
911 }
912 }
913 }
914
915 break; // go to default case
916 }
917
918 case TagConstants.ANYEQ:
919 // Change (ANYEQ a a) -> true
920 {
921 if( ev.size() == 2 &&
922 ev.elementAt(0) instanceof VariableAccess &&
923 ev.elementAt(1) instanceof VariableAccess &&
924 ((VariableAccess)ev.elementAt(0)).decl ==
925 ((VariableAccess)ev.elementAt(1)).decl ) {
926 return GC.truelit;
927 }
928
929 if( ev.size() == 2 &&
930 ev.elementAt(0) instanceof LiteralExpr &&
931 ev.elementAt(1) instanceof LiteralExpr &&
932 ((LiteralExpr)ev.elementAt(0)).value.equals(
933 ((LiteralExpr)ev.elementAt(1)).value )) {
934 return GC.truelit;
935 }
936
937 break; // go to default case
938 }
939
940 }
941 }
942
943 // No special case, so do default
944 return NaryExpr.make(sloc,eloc,tag, null, ev);
945 }
946
947
948 //// Makers for other GCExpr nodes
949
950 //@ ensures \result != null;
951 public static Expr select(/*@ non_null @*/ Expr c0, /*@ non_null @*/ Expr c1) {
952 return nary(TagConstants.SELECT, c0, c1);
953 }
954
955 //@ ensures \result != null;
956 public static Expr not(/*@ non_null @*/ Expr c) {
957 return not(Location.NULL, Location.NULL, c);
958 }
959
960 //@ ensures \result != null;
961 public static Expr not(int sloc, int eloc, /*@ non_null @*/ Expr c) {
962 return nary(sloc, eloc, TagConstants.BOOLNOT, c);
963 }
964
965 //@ ensures \result != null;
966 public static Expr and(/*@ non_null @*/ Expr c1, /*@ non_null @*/ Expr c2) {
967 return and(Location.NULL, Location.NULL, c1, c2);
968 }
969
970 //@ ensures \result != null;
971 public static Expr andx(/*@ non_null @*/ Expr c1, /*@ non_null @*/ Expr c2) {
972 ExprVec es = ExprVec.make(2);
973 es.addElement(c1);
974 es.addElement(c2);
975 return nary(Location.NULL, Location.NULL, TagConstants.BOOLANDX, es);
976 }
977
978 //@ ensures \result != null;
979 public static Expr and(int sloc, int eloc, /*@ non_null @*/ Expr c1, /*@ non_null @*/ Expr c2) {
980 Expr[] es = {c1, c2};
981 return and( sloc, eloc, ExprVec.make(es) );
982 }
983
984 //@ ensures \result != null;
985 public static Expr and(/*@ non_null @*/ ExprVec v) {
986 return and(Location.NULL, Location.NULL, v);
987 }
988
989 //@ ensures \result != null;
990 public static Expr and(int sloc, int eloc, /*@ non_null @*/ ExprVec v) {
991 return nary( sloc, eloc, TagConstants.BOOLAND, v );
992 }
993
994 //@ ensures \result != null;
995 public static Expr or(/*@ non_null @*/ Expr c1, /*@ non_null @*/ Expr c2) {
996 return or(Location.NULL, Location.NULL, c1, c2);
997 }
998
999 //@ ensures \result != null;
1000 public static Expr or(int sloc, int eloc,
1001 /*@ non_null @*/ Expr c1, /*@ non_null @*/ Expr c2) {
1002 Expr[] es = {c1, c2};
1003 return or( sloc, eloc, ExprVec.make(es) );
1004 }
1005
1006 //@ ensures \result != null;
1007 public static Expr or(/*@ non_null @*/ ExprVec v) {
1008 return or(Location.NULL, Location.NULL, v);
1009 }
1010
1011 //@ ensures \result != null;
1012 public static Expr or(int sloc, int eloc, /*@ non_null @*/ ExprVec v) {
1013 return nary( sloc, eloc, TagConstants.BOOLOR, v );
1014 }
1015
1016 //@ ensures \result != null;
1017 public static Expr implies(/*@ non_null @*/ Expr c0, /*@ non_null @*/ Expr c1) {
1018 return implies( Location.NULL, Location.NULL, c0, c1 );
1019 }
1020
1021 //@ ensures \result != null;
1022 public static Expr implies(int sloc, int eloc, /*@ non_null @*/ Expr c0, /*@ non_null @*/ Expr c1) {
1023 return nary( sloc, eloc, TagConstants.BOOLIMPLIES, c0, c1);
1024 }
1025
1026 //@ ensures \result != null;
1027 public static Expr forall(/*@ non_null @*/ GenericVarDecl v, /*@ non_null @*/ Expr e) {
1028 return forall( Location.NULL, Location.NULL, v, GC.truelit, e, null );
1029 }
1030
1031 //@ ensures \result != null;
1032 public static Expr forall(/*@ non_null @*/ GenericVarDecl v, Expr range, /*@ non_null @*/ Expr e) {
1033 return forall( Location.NULL, Location.NULL, v, range, e, null );
1034 }
1035
1036 //@ ensures \result != null;
1037 public static Expr forall(/*@ non_null @*/ GenericVarDeclVec v,
1038 /*null?*/ Expr range,
1039 /*@ non_null @*/ Expr e)
1040 {
1041 return quantifiedExpr( Location.NULL, Location.NULL,
1042 TagConstants.FORALL, v, range, e, null, null );
1043 }
1044
1045 //@ ensures \result != null;
1046 public static Expr forall(/*@ non_null @*/ GenericVarDecl v,
1047 /*@ non_null @*/ Expr e,
1048 ExprVec nopats)
1049 {
1050 return forall( Location.NULL, Location.NULL, v, GC.truelit, e, nopats );
1051 }
1052
1053 //@ ensures \result != null;
1054 public static Expr forallwithpats(/*@ non_null @*/ GenericVarDecl v,
1055 /*@ non_null @*/ Expr e,
1056 /*@ non_null @*/ ExprVec pats) {
1057 return quantifiedExpr( Location.NULL, Location.NULL,
1058 TagConstants.FORALL, v, GC.truelit, e, null, pats );
1059 }
1060
1061 //@ ensures \result != null;
1062 public static Expr forall(int sloc, int eloc, /*@ non_null @*/ GenericVarDecl v,
1063 Expr range, /*@ non_null @*/ Expr e) {
1064 return forall(sloc, eloc, v, range, e, null);
1065 }
1066
1067 //@ ensures \result != null;
1068 public static Expr forall(int sloc, int eloc,
1069 /*@ non_null @*/ GenericVarDecl v,
1070 Expr range,
1071 /*@ non_null @*/ Expr e,
1072 ExprVec nopats) {
1073 Assert.notNull(v);
1074 Assert.notNull(e);
1075
1076 if( Main.options().peepOptE ) {
1077
1078 // Change forall (a) ((a==b) ==> e) -> e[b/a] if b a variable
1079
1080 if( e.getTag() == TagConstants.BOOLIMPLIES ) {
1081
1082 NaryExpr nary = (NaryExpr)e;
1083 Expr impliesLhs = nary.exprs.elementAt(0);
1084 Expr impliesRhs = nary.exprs.elementAt(1);
1085 switch( impliesLhs.getTag() ) {
1086 case TagConstants.ANYEQ:
1087 case TagConstants.BOOLEQ:
1088 case TagConstants.INTEGRALEQ:
1089 case TagConstants.REFEQ:
1090 case TagConstants.TYPEEQ:
1091
1092 NaryExpr lhsNary = (NaryExpr)impliesLhs;
1093 Expr eqLhs = lhsNary.exprs.elementAt(0);
1094 Expr eqRhs = lhsNary.exprs.elementAt(1);
1095 if( eqLhs.getTag() == TagConstants.VARIABLEACCESS
1096 && ((VariableAccess)eqLhs).decl == v
1097 && isSimple( eqRhs ))
1098 {
1099 // Can replace the forall with a substitution
1100 return subst( v, eqRhs, impliesRhs );
1101 }
1102 }
1103 }
1104 }
1105
1106 // could not do the substitution
1107 return quantifiedExpr(sloc, eloc, TagConstants.FORALL, v, range, e, nopats, null);
1108 }
1109
1110 //@ ensures \result != null;
1111 public static Expr quantifiedExpr(int sloc, int eloc, int tag,
1112 /*@ non_null @*/ GenericVarDecl v,
1113 Expr range,
1114 /*@ non_null @*/ Expr e,
1115 ExprVec nopats,
1116 ExprVec pats)
1117 {
1118 GenericVarDeclVec vs = GenericVarDeclVec.make();
1119 vs.addElement(v);
1120 return quantifiedExpr(sloc, eloc, tag, vs, range, e, nopats, pats );
1121 }
1122
1123 //@ ensures \result != null;
1124 public static Expr quantifiedExpr(int sloc, int eloc, int tag,
1125 /*@ non_null @*/ GenericVarDeclVec vs,
1126 /*null?*/ Expr range,
1127 /*@ non_null @*/ Expr e,
1128 /*null?*/ ExprVec nopats,
1129 /*null?*/ ExprVec pats)
1130 {
1131 Assert.notFalse( tag == TagConstants.FORALL
1132 || tag == TagConstants.EXISTS );
1133
1134 if( tag == TagConstants.FORALL && vs.size() == 0 ) {
1135 // empty forall
1136 return e;
1137 }
1138
1139 if( Main.options().peepOptE ) {
1140
1141 // change Q(a)Q(b)e -> Q(a b) e, where Q is a quantifier
1142
1143 if( e.getTag() == tag ) {
1144 QuantifiedExpr qe = (QuantifiedExpr)e;
1145 GenericVarDeclVec copy = vs.copy();
1146 copy.append( qe.vars );
1147 if (qe.nopats != null) {
1148 if (nopats == null) {
1149 nopats = qe.nopats;
1150 } else {
1151 nopats = nopats.copy();
1152 nopats.append(qe.nopats);
1153 }
1154 }
1155 if (range == null) range = qe.rangeExpr;
1156 else if (qe.rangeExpr != null) range = GC.and(range,qe.rangeExpr);
1157 return QuantifiedExpr.make( sloc, eloc, tag, copy,
1158 range, qe.expr,
1159 nopats, qe.pats );
1160 }
1161 }
1162
1163 // No optimization done
1164 return QuantifiedExpr.make( sloc, eloc, tag, vs, range, e, nopats, pats );
1165 }
1166
1167 public static boolean isSimple(/*@ non_null @*/ Expr e) {
1168 switch( e.getTag() ) {
1169 case TagConstants.VARIABLEACCESS:
1170 case TagConstants.TYPEEXPR:
1171 case TagConstants.BOOLEANLIT:
1172 case TagConstants.CHARLIT:
1173 case TagConstants.DOUBLELIT:
1174 case TagConstants.FLOATLIT:
1175 case TagConstants.INTLIT:
1176 case TagConstants.LONGLIT:
1177 case TagConstants.NULLLIT:
1178 case TagConstants.STRINGLIT:
1179 case TagConstants.SYMBOLLIT:
1180 return true;
1181
1182 default:
1183 return false;
1184 }
1185 }
1186
1187 /**
1188 * Adds elements to <code>to</code> from <code>from</code>.
1189 * Elements equal to bot are dropped. If an element equal to top is
1190 * encountered, true is returned and to is undefined. If top is
1191 * never encountered, false is returned. If from contains an
1192 * NaryExpr with tag naryTagMerge, the components of that NaryExpr
1193 * are treated in a similar manner.
1194 */
1195 private static boolean selectiveAdd(/*@ non_null @*/ ExprVec to,
1196 /*@ non_null @*/ ExprVec from,
1197 Expr bot, Expr top, int naryTagMerge)
1198 {
1199 for(int i=0; i<from.size(); i++) {
1200 Expr e = from.elementAt(i);
1201 if( e == bot ) {
1202 // drop e
1203 } else if( e == top ) {
1204 return true;
1205 } else if( e.getTag() == naryTagMerge ) {
1206 ExprVec exprs = ((NaryExpr)e).exprs;
1207 if( selectiveAdd( to, exprs, bot, top, naryTagMerge ) )
1208 return true;
1209 } else {
1210 // nothing special
1211 to.addElement(e);
1212 }
1213 }
1214 return false;
1215 }
1216
1217 }