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 }