001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package escjava.translate; 004 005 import java.io.ByteArrayOutputStream; 006 import java.util.ArrayList; 007 import java.util.Enumeration; 008 import java.util.HashMap; 009 import java.util.Hashtable; 010 import java.util.Iterator; 011 import java.util.LinkedList; 012 import java.util.Map; 013 import java.util.Vector; 014 015 import javafe.Tool; 016 import javafe.ast.ASTDecoration; 017 import javafe.ast.ASTNode; 018 import javafe.ast.ArrayInit; 019 import javafe.ast.ArrayRefExpr; 020 import javafe.ast.ArrayType; 021 import javafe.ast.AssertStmt; 022 import javafe.ast.BinaryExpr; 023 import javafe.ast.BreakStmt; 024 import javafe.ast.CastExpr; 025 import javafe.ast.CatchClause; 026 import javafe.ast.ClassDecl; 027 import javafe.ast.ClassLiteral; 028 import javafe.ast.CondExpr; 029 import javafe.ast.ConstructorDecl; 030 import javafe.ast.ConstructorInvocation; 031 import javafe.ast.ContinueStmt; 032 import javafe.ast.DoStmt; 033 import javafe.ast.EvalStmt; 034 import javafe.ast.Expr; 035 import javafe.ast.ExprObjectDesignator; 036 import javafe.ast.ExprVec; 037 import javafe.ast.FieldAccess; 038 import javafe.ast.FieldDecl; 039 import javafe.ast.ForStmt; 040 import javafe.ast.FormalParaDecl; 041 import javafe.ast.GenericBlockStmt; 042 import javafe.ast.GenericVarDecl; 043 import javafe.ast.Identifier; 044 import javafe.ast.IfStmt; 045 import javafe.ast.InitBlock; 046 import javafe.ast.InstanceOfExpr; 047 import javafe.ast.LabelStmt; 048 import javafe.ast.LiteralExpr; 049 import javafe.ast.LocalVarDecl; 050 import javafe.ast.MethodDecl; 051 import javafe.ast.MethodInvocation; 052 import javafe.ast.ModifierPragma; 053 import javafe.ast.NewArrayExpr; 054 import javafe.ast.NewInstanceExpr; 055 import javafe.ast.ParenExpr; 056 import javafe.ast.PrettyPrint; 057 import javafe.ast.PrimitiveType; 058 import javafe.ast.ReturnStmt; 059 import javafe.ast.RoutineDecl; 060 import javafe.ast.Stmt; 061 import javafe.ast.SwitchLabel; 062 import javafe.ast.SwitchStmt; 063 import javafe.ast.SynchronizeStmt; 064 import javafe.ast.ThisExpr; 065 import javafe.ast.ThrowStmt; 066 import javafe.ast.TryCatchStmt; 067 import javafe.ast.TryFinallyStmt; 068 import javafe.ast.Type; 069 import javafe.ast.TypeDecl; 070 import javafe.ast.TypeDeclElem; 071 import javafe.ast.TypeName; 072 import javafe.ast.UnaryExpr; 073 import javafe.ast.VarDeclStmt; 074 import javafe.ast.VarInit; 075 import javafe.ast.VariableAccess; 076 import javafe.ast.WhileStmt; 077 import javafe.tc.TypeSig; 078 import javafe.util.Assert; 079 import javafe.util.ErrorSet; 080 import javafe.util.Info; 081 import javafe.util.Location; 082 import javafe.util.Set; 083 import javafe.util.StackVector; 084 import escjava.Main; 085 import escjava.Options; 086 import escjava.ast.ArrayRangeRefExpr; 087 import escjava.ast.Call; 088 import escjava.ast.CmdCmdCmd; 089 import escjava.ast.Condition; 090 import escjava.ast.ConditionVec; 091 import escjava.ast.DecreasesInfo; 092 import escjava.ast.DecreasesInfoVec; 093 import escjava.ast.DerivedMethodDecl; 094 import escjava.ast.DynInstCmd; 095 import escjava.ast.EscPrettyPrint; 096 import escjava.ast.EverythingExpr; 097 import escjava.ast.ExprCmd; 098 import escjava.ast.ExprModifierPragma; 099 import escjava.ast.ExprStmtPragma; 100 import escjava.ast.ExprStmtPragmaVec; 101 import escjava.ast.GenericVarDeclVec; 102 import escjava.ast.GetsCmd; 103 import escjava.ast.GhostDeclPragma; 104 import escjava.ast.GuardedCmd; 105 import escjava.ast.GuardedCmdVec; 106 import escjava.ast.LabelExpr; 107 import escjava.ast.LocalVarDeclVec; 108 import escjava.ast.LoopCmd; 109 import escjava.ast.ModelDeclPragma; 110 import escjava.ast.Modifiers; 111 import escjava.ast.ModifiesGroupPragma; 112 import escjava.ast.ModifiesGroupPragmaVec; 113 import escjava.ast.NaryExpr; 114 import escjava.ast.NothingExpr; 115 import escjava.ast.RestoreFromCmd; 116 import escjava.ast.SeqCmd; 117 import escjava.ast.SetStmtPragma; 118 import escjava.ast.SimpleModifierPragma; 119 import escjava.ast.SkolemConstantPragma; 120 import escjava.ast.Spec; 121 import escjava.ast.SubGetsCmd; 122 import escjava.ast.SubSubGetsCmd; 123 import escjava.ast.TagConstants; 124 import escjava.ast.TypeExpr; 125 import escjava.ast.Utils; 126 import escjava.ast.VarInCmd; 127 import escjava.ast.WildRefExpr; 128 import escjava.backpred.FindContributors; 129 import escjava.tc.FlowInsensitiveChecks; 130 import escjava.tc.TypeCheck; 131 import escjava.tc.Types; 132 133 public final class Translate 134 { 135 Frame frameHandler = null; 136 137 // This Set contains method declarations for which axioms derived from 138 // postconditions need to be added to the assumptions for verifying the body. 139 public static java.util.Set axsToAdd = new java.util.HashSet(); 140 141 private Hashtable premap; 142 private Hashtable premapWithArgs; 143 144 /** The type containing the routine whose body is being translated. */ 145 private TypeDecl typeDecl; 146 147 /** 148 * Translates the body of a method or constructor, as described in ESCJ 16, section 149 * 8. 150 * 151 * @param predictedSynTargs for correct translation, this must contain an upper 152 * bound for the syntactic targets of the result of this call. A value of null is 153 * taken to represent the set of all variables & is hence always a safe value. 154 * 155 * @note passing a value of <the empty set> for predictedSynTargs will give a 156 * translation missing assert statements for checking call preconditions, but 157 * otherwise correct. The resulting computation runs faster than passing null, 158 * while still having the same set of targets. escjava.Main is currently using 159 * this trick as a kludge to compute the syntactic targets upper bound. 160 */ 161 //@ requires rd.body != null; 162 public GuardedCmd trBody(/*@ non_null */ RoutineDecl rd, 163 /*@ non_null */ FindContributors scope, 164 Hashtable premap, 165 Set predictedSynTargs, 166 Translate inlineParent, 167 boolean issueCautions) { 168 169 Hashtable paramMap = GetSpec.makeSubst(rd.args, "pre"); 170 premapWithArgs = new Hashtable(); 171 premapWithArgs.putAll(paramMap); 172 if (premap != null) premapWithArgs.putAll(premap); 173 174 frameHandler = new Frame(this, issueCautions, rd, premapWithArgs); 175 TrAnExpr.translate = this; 176 this.typeDecl = rd.parent; 177 this.premap = premap; 178 axsToAdd = new java.util.HashSet(); 179 180 // Reset the state of the AuxInfo module if this is top-level call to trBody 181 if (inlineParent == null) { 182 AuxInfo.reset(); 183 } 184 185 // Reset the internal state of <code>this</code> 186 this.rdCurrent = rd; 187 this.scope = scope; 188 this.predictedSynTargs = predictedSynTargs; 189 this.inlineParent = inlineParent; 190 if (inlineParent == null) { 191 this.inConstructorContext = isStandaloneConstructor(rd); 192 } else { 193 this.inConstructorContext = inlineParent.inConstructorContext && 194 rdCurrent.parent == inlineParent.rdCurrent.parent; 195 } 196 this.issueCautions = issueCautions; 197 this.modifyEverythingLocations = new ArrayList(); 198 199 if (Info.on) { 200 System.out.print("trBody: "); 201 for (Translate ttIR = inlineParent; 202 ttIR != null; 203 ttIR = ttIR.inlineParent) { 204 System.out.print(" "); 205 } 206 System.out.println(TypeCheck.inst.getSig(rd.parent).toString() + "." + 207 TypeCheck.inst.getRoutineName(rd) + 208 TypeCheck.getSignature(rd)); 209 System.out.flush(); 210 } 211 212 code.clear(); code.push(); // this mark popped by "spill" 213 declaredLocals.clear(); 214 temporaries.clear(); temporaries.push(); // this mark popped by "spill" 215 tmpcount = 0; 216 217 GC.thisvar.decl.type = scope.originType; 218 219 code.push(); // this mark popped below 220 221 /* 222 * Translate body: 223 */ 224 if (rd.getTag() == TagConstants.METHODDECL) { 225 if (! Modifiers.isSynchronized(rd.modifiers)) { 226 // non-synchronized method 227 trStmt(rd.body,rd.parent); 228 } else if (! Modifiers.isStatic(rd.modifiers)) { 229 // synchronized instance method 230 trSynchronizedBody(GC.thisvar, rd.body, rd.locOpenBrace, typeDecl); 231 } else { 232 // synchronized static method 233 trSynchronizedBody(GC.nary(TagConstants.CLASSLITERALFUNC, 234 getClassObject(rd.parent)), 235 rd.body, rd.locOpenBrace, typeDecl); 236 } 237 } else { 238 Assert.notFalse(rd.getTag() == TagConstants.CONSTRUCTORDECL); 239 trConstructorBody((ConstructorDecl)rd, premap); 240 } 241 242 243 // "code" now contains two marks followed by what ESCJ 16 calls "CS" 244 // (except for the "assume !isAllocated(objectToBeConstructed, alloc)", 245 // which has already been prepended to "code" here) 246 if (Main.options().traceInfo > 0 && 247 (inlineParent != null || Main.options().traceInfo > 1)) { 248 // add a label to track the implicit return ("falling off the end 249 // of the routine") 250 int loc = rd.getEndLoc(); 251 Assert.notFalse(loc != Location.NULL); 252 GuardedCmd g = traceInfoLabelCmd(loc, loc, "ImplicitReturn", loc); 253 code.addElement(g); 254 } 255 code.addElement(GC.gets(GC.ecvar, GC.ec_return)); 256 code.addElement(GC.trycmd(GC.seq(GuardedCmdVec.popFromStackVector(code)), 257 GC.skip())); 258 if (rd.getTag() == TagConstants.CONSTRUCTORDECL) { 259 code.addElement(GC.gets(GC.resultvar, GC.thisvar)); 260 } 261 GuardedCmd body = spill(); 262 // "code" is now empty: 263 Assert.notFalse(code.vectors()==1 && code.size()==0); 264 265 // Finally, if there are any formal parameters, wrap "body" in a 266 // statement that saves and restores the values of the formal parameters 267 GuardedCmd res; 268 if (rd.args.size() == 0) { 269 res = body; 270 } 271 else { 272 273 declaredLocals.push(); // this mark popped by "popDeclBlock" 274 code.push(); // this mark popped by "popDeclBlock" 275 276 VariableAccess[] ppp = new VariableAccess[rd.args.size() * 2]; 277 for (int i = 0; i < rd.args.size(); i++) { 278 FormalParaDecl arg = rd.args.elementAt(i); 279 VariableAccess va = (VariableAccess)paramMap.get(arg); 280 declaredLocals.addElement(va.decl); 281 ppp[2*i] = TrAnExpr.makeVarAccess(arg, Location.NULL); 282 ppp[2*i+1] = va; 283 } 284 for (int i = 0; i < ppp.length; i += 2) { 285 code.addElement(GC.gets(ppp[i+1], ppp[i])); 286 } 287 code.addElement(body); 288 for (int i = 0; i < ppp.length; i += 2) { 289 code.addElement(GC.restoreFrom(ppp[i], ppp[i+1])); 290 } 291 res = popDeclBlock(); 292 } 293 //TrAnExpr.translate = null; 294 // Don't turn the above off because at present helper methods 295 // are inlined in which case this method is called recursively. 296 return res; 297 } 298 299 /** 300 * @return <code>true</code> when <code>rd</code> is a constructor that does not 301 * call a sibling constructor. 302 */ 303 private boolean isStandaloneConstructor(/*@ non_null */ RoutineDecl rd) { 304 if (!(rd instanceof ConstructorDecl)) { 305 return false; 306 } 307 ConstructorDecl cd = (ConstructorDecl)rd; 308 // From here on, return "true" unless there is a call to a sibling 309 // constructor. 310 311 if (cd.body == null || cd.body.getTag() != TagConstants.BLOCKSTMT) { 312 return true; 313 } 314 GenericBlockStmt body = (GenericBlockStmt)cd.body; 315 316 if (body.stmts.size() == 0) { 317 return true; 318 } 319 Stmt s0 = body.stmts.elementAt(0); 320 321 if (s0.getTag() != TagConstants.CONSTRUCTORINVOCATION) { 322 return true; 323 } 324 ConstructorInvocation ccall = (ConstructorInvocation)s0; 325 326 return ccall.decl.parent != cd.parent; 327 } 328 329 /** 330 * Auxiliary routine used by trBody to translate the body of a constructor, as 331 * described in ESCJ 16, section 8. 332 */ 333 //@ requires cd.body != null; 334 private void trConstructorBody(/*@ non_null */ ConstructorDecl cd, 335 Hashtable premap) { 336 // assume !isAllocated(objectToBeConstructed, alloc); 337 { 338 Expr isAllocated = GC.nary(TagConstants.ISALLOCATED, 339 GC.objectTBCvar, GC.allocvar); 340 code.addElement(GC.assume(GC.not(isAllocated))); 341 } 342 343 344 if (cd.body == null) return; 345 // FIXME - not entirely sure we should omit everything 346 // from here on if there is no body. 347 /* 348 * Find the call to the superclass or sibling constructor, if 349 * any. In particular, set both "body" and "ccall" to 350 * non-"null" values if "cd.body" starts with a constructor 351 * call. ("ccall" is non-"null" only if "body" is, too.) 352 */ 353 GenericBlockStmt body = null; 354 ConstructorInvocation ccall = null; 355 if (cd.body.getTag() == TagConstants.BLOCKSTMT) { 356 body = (GenericBlockStmt)cd.body; 357 if (1 <= body.stmts.size()) { 358 Stmt s0 = body.stmts.elementAt(0); 359 if (s0.getTag() == TagConstants.CONSTRUCTORINVOCATION) { 360 ccall = (ConstructorInvocation)s0; 361 } 362 } 363 } 364 365 366 if (ccall==null) { 367 /* 368 * Here "cd" refers to a constructor of class "Object" 369 * that does not call any sibling constructor. 370 * 371 * The code that used to be here can be found in revision 372 * 1.87 of this file (Translate.java); it is probably 373 * somewhat "rotted", though. 374 */ 375 Assert.notFalse(Types.isSameType(TypeSig.getSig(cd.parent), 376 Types.javaLangObject())); 377 Assert.notImplemented("Checking of Object constructor body"); 378 } 379 380 381 TypeDecl tdecl = cd.parent; 382 TypeSig type = TypeSig.getSig(tdecl); 383 try { 384 if (!type.isTopLevelType()) 385 Inner.firstThis0 = Inner.getEnclosingInstanceArg(cd); 386 387 trConstructorCallStmt(ccall); 388 } finally { 389 Inner.firstThis0 = null; 390 } 391 392 393 // assume typeof(this) <: T 394 TypeExpr texpr = TypeExpr.make(tdecl.getStartLoc(), 395 tdecl.getEndLoc(), 396 type); 397 Expr goodType = GC.nary(TagConstants.TYPELE, 398 GC.nary(TagConstants.TYPEOF, GC.thisvar), 399 texpr); 400 code.addElement(GC.assume(goodType)); 401 402 // assume objectToBeConstructed == this; 403 code.addElement(GC.assume(GC.nary(TagConstants.REFEQ, 404 GC.objectTBCvar, 405 GC.thisvar))); 406 407 /* 408 * Insert this.this$0 = this$0arg if we are an inner-class constructor: 409 */ 410 { 411 TypeSig T = TypeSig.getSig(cd.parent); 412 if (!T.isTopLevelType()) { 413 FieldDecl this0 = Inner.getEnclosingInstanceField(T); 414 FormalParaDecl this0arg = Inner.getEnclosingInstanceArg(cd); 415 416 code.addElement(GC.subgets( 417 TrAnExpr.makeVarAccess(this0, Location.NULL), 418 GC.thisvar, 419 TrAnExpr.makeVarAccess(this0arg, Location.NULL))); 420 } 421 } 422 423 424 if (ccall.decl.parent != cd.parent) { 425 // superclass (not sibling) constructor call: 426 instanceInitializers(cd.parent); 427 } 428 429 // call "trStmt" on the rest of the body: 430 declaredLocals.push(); // this mark popped by "wrapUpDeclBlock" 431 code.push(); // this mark popped by "wrapUpDeclBlock" 432 for (int i = 1; i < body.stmts.size(); i++) { 433 trStmt(body.stmts.elementAt(i),cd.parent); 434 } 435 wrapUpDeclBlock(); 436 } 437 438 private TypeExpr getClassObject(/*@ non_null */ TypeDecl tdClass) { 439 Type type = TypeSig.getSig(tdClass); 440 TypeExpr texpr = TypeExpr.make(tdClass.getStartLoc(), tdClass.getEndLoc(), 441 type); 442 return texpr; 443 } 444 445 446 /** 447 * This method implements "InstanceInitializers", as described in section 8.1 of 448 * ESCJ 16. 449 */ 450 private void instanceInitializers(/*@ non_null */ TypeDecl tdecl) { 451 // First, provide zero-equivalent values for fields in first-inherited 452 // interfaces 453 if (tdecl instanceof ClassDecl) { 454 Enumeration interfaces = GetSpec.getFirstInheritedInterfaces((ClassDecl)tdecl); 455 while (interfaces.hasMoreElements()) { 456 TypeDecl tdSuperInterface = (TypeDecl)interfaces.nextElement(); 457 instanceInitializeZero(tdSuperInterface); 458 } 459 } 460 // Then, provide zero-equivalent values for fields in "tdecl" 461 instanceInitializeZero(tdecl); 462 463 // Finally, compute the programmer-supplied initial values and assign 464 // the fields appropriately. (Note, first-inherited interfaces don't 465 // have programmer-supplied initial values for instance fields, since 466 // the only instance fields in interfaces are ghost fields and they 467 // don't have initial values.) 468 for (int i = 0; i < tdecl.elems.size(); i++) { 469 TypeDeclElem tde = tdecl.elems.elementAt(i); 470 if (tde instanceof ModelDeclPragma) continue; 471 if (tde instanceof GhostDeclPragma) 472 tde = ((GhostDeclPragma)tde).decl; 473 474 if (tde.getTag() == TagConstants.INITBLOCK) { 475 InitBlock ib = (InitBlock)tde; 476 if (!Modifiers.isStatic(ib.modifiers)) { 477 trStmt(ib.block,tdecl); 478 } 479 } else if (tde.getTag() == TagConstants.FIELDDECL) { 480 FieldDecl fd = (FieldDecl)tde; 481 if (!Modifiers.isStatic(fd.modifiers) && fd.init != null) { 482 Assert.notFalse(fd.locAssignOp != Location.NULL); 483 // e= Expr[[ fd.init ]] 484 Expr e = ptrExpr(fd.init); 485 // WriteCheck[[ f[this], e ]] 486 VariableAccess f = TrAnExpr.makeVarAccess(fd, Location.NULL); 487 Expr lhs = GC.select(f, GC.thisvar); 488 writeCheck(lhs, fd.init, e, fd.locAssignOp, true); 489 // f[this] = e 490 code.addElement(GC.subgets(f, GC.thisvar, e)); 491 } 492 } 493 } 494 } 495 496 /** 497 * Called by <code>instanceInitializers</code>. 498 */ 499 private void instanceInitializeZero(/*@ non_null */ TypeDecl tdecl) { 500 for (int i = 0; i < tdecl.elems.size(); i++) { 501 TypeDeclElem tde = tdecl.elems.elementAt(i); 502 if (tde instanceof ModelDeclPragma) continue; 503 if (tde instanceof GhostDeclPragma) 504 tde = ((GhostDeclPragma)tde).decl; 505 506 if (tde.getTag() == TagConstants.FIELDDECL) { 507 FieldDecl fd = (FieldDecl)tde; 508 if (!Modifiers.isStatic(fd.modifiers)) { 509 // f[this] = <default value> 510 VariableAccess fdref = TrAnExpr.makeVarAccess(fd, Location.NULL); 511 Expr defaultValue = null; 512 switch (fd.type.getTag()) { 513 case TagConstants.BOOLEANTYPE: 514 defaultValue = GC.falselit; 515 break; 516 517 case TagConstants.BIGINTTYPE: 518 case TagConstants.INTTYPE: 519 case TagConstants.LONGTYPE: 520 case TagConstants.CHARTYPE: 521 case TagConstants.BYTETYPE: 522 case TagConstants.SHORTTYPE: 523 defaultValue = GC.zerolit; 524 break; 525 526 case TagConstants.ARRAYTYPE: 527 case TagConstants.TYPENAME: 528 case TagConstants.TYPESIG: 529 if (GetSpec.NonNullPragma(fd) != null) { 530 defaultValue = temporary(fd.id.toString() + "@zero", 531 fd.getStartLoc()); 532 } else { 533 defaultValue = GC.nulllit; 534 } 535 break; 536 537 case TagConstants.DOUBLETYPE: 538 case TagConstants.FLOATTYPE: 539 defaultValue = GC.nary(TagConstants.CAST, GC.zerolit, 540 GC.typeExpr(fd.type)); 541 break; 542 543 case TagConstants.TYPECODE: 544 // TYPE fields have no default value: 545 defaultValue = temporary(fd.id.toString() + "@zero", 546 fd.getStartLoc()); 547 break; 548 549 case TagConstants.NULLTYPE: 550 default: 551 /*@ unreachable ;*/ 552 Assert.fail("Unexpected type tag " + TagConstants.toString(fd.type.getTag())); 553 break; 554 } 555 if (defaultValue != null) 556 code.addElement(GC.subgets(fdref, GC.thisvar, defaultValue)); 557 } 558 } 559 } 560 } 561 562 //// Instance variables 563 564 /** References the routine currently being checked by trBody. */ 565 566 private RoutineDecl rdCurrent; 567 568 /** 569 * Singly-linked list of the inline parents. Is <code>null</code> if this 570 * translation is not being inlined. 571 */ 572 private Translate inlineParent; 573 574 /** 575 * Indicates whether to issue cautions. Value is set from outer call to trBody 576 * and also used by nested/recursive calls. 577 */ 578 private boolean issueCautions; 579 580 /** 581 * Indicates whether or not the current routine is in a "constructor context", 582 * meaning that it is a constructor being checked or a method in the same class 583 * that's being inlined into the constructor. 584 */ 585 private boolean inConstructorContext; 586 587 /** 588 * Contains the guarded commands generated so far for the current method. As the 589 * translation enters into Java blocks, <code>code</code> gets pushed. As blocks 590 * are left, <code>code</code> is poped into a <code>GuardedCmdVec</code> which 591 * is wrapped inside a BLOCK guarded command that gets appended onto 592 * <code>code</code>. 593 */ 594 /*@ spec_public */ private final StackVector code = new StackVector(); 595 596 /** 597 * List of loop invariant pragmas seen so far (and not yet used) within the 598 * current method. 599 */ 600 private ExprStmtPragmaVec loopinvariants = ExprStmtPragmaVec.make(); 601 602 /** 603 * List of loop decreases pragmas seen so far (and not yet used) within the 604 * current method. 605 */ 606 607 private /*@ non_null */ ExprStmtPragmaVec loopDecreases = ExprStmtPragmaVec.make(); 608 609 private /*@ non_null */ ExprStmtPragmaVec loopPredicates = ExprStmtPragmaVec.make(); 610 611 protected /*@ non_null */ LocalVarDeclVec skolemConstants = LocalVarDeclVec.make(); 612 613 /** 614 * Contains the local Java variables declared in the current <em>block</em> so 615 * far for the current block and enclosing blocks of the current method. This 616 * variable is maintained parallel to <code>code</code>: Each time a Java block 617 * is entered, <code>declaredLocals</code> gets pushed; when a block is left, 618 * <code>declaredLocals</code> is popped into a <code>GenericVarDeclVec</code> 619 * that gets wrapped inside a BLOCK guarded command. 620 */ 621 private final /*@ non_null */ StackVector declaredLocals = new StackVector(); 622 623 /** 624 * Contains the temporaries that generated for the current method that haven't 625 * yet been declared in a VARINCMD. 626 */ 627 private final /*@ non_null */ StackVector temporaries = new StackVector(); 628 629 630 /** Describes the current scope. */ 631 632 private FindContributors scope; 633 634 /** 635 * Describes the current predicted set of synTargs. 636 * 637 * <p> If non-null, then represents an <em>*upper*</em> bound on 638 * freeVars of the result of the current trBody(...) call. 639 */ 640 private Set predictedSynTargs; 641 642 /** 643 * Describes what aspects of an inlined call to check and what 644 * aspects to either assert or simply ignore. A call 645 * (MethodInvocation, ConstructorInvocation, NewInstanceExpr) may 646 * map to an <code>InlineSettings</code> object in which the 647 * <code>nextInlineCheckDepth</code> and 648 * <code>nextInlineDepthPastCheck</code> fields are unused. 649 * 650 * <p> This variable is used only for some call-site specific 651 * inlining, in particular, currently only to handle the 652 * -inlineConstructors flag. Other reasons for inlining are taken 653 * care of in method <code>computeInlineSettings</code>. </p> 654 */ 655 public static final /*@ non_null */ ASTDecoration inlineDecoration = 656 new ASTDecoration("inlineDecoration"); 657 658 659 //// Generation of variables to put into guarded commands 660 661 /** 662 * Pops temporaries and code, and makes these into a VARINCMD command that is 663 * returned. If there are no temporaries, only the code is returned. 664 */ 665 private GuardedCmd spill() { 666 GuardedCmd body = GC.seq(GuardedCmdVec.popFromStackVector(code)); 667 GenericVarDeclVec temps = GenericVarDeclVec.popFromStackVector(temporaries); 668 return GC.block(temps, body); 669 } 670 671 672 /** 673 * Make a fresh version of a special variable to save it in. 674 * 675 * (This partially handles ESCJ 23b, case 4.) 676 */ 677 //@ requires (* v accesses a special variable. *); 678 private VariableAccess adorn(VariableAccess v) { 679 Assert.precondition(v.decl.locId == UniqName.specialVariable); 680 681 VariableAccess result= GC.makeVar(v.decl.id, v.decl.locId); 682 result.loc= v.getStartLoc(); 683 684 temporaries.addElement(result.decl); 685 return result; 686 } 687 688 689 /** 690 * Make a fresh "boolean" variable to hold the initialized status 691 * of a Java variable that is marked as "uninitialized". 692 * 693 * (This partially handles ESCJ 23b, case 13.) 694 */ 695 //@ requires (* v accesses a normal Java variable. *); 696 private VariableAccess initadorn(/*@ non_null */ LocalVarDecl d) { 697 Identifier idn = Identifier.intern(d.id + "@init"); 698 699 VariableAccess result = GC.makeVar(idn, d.locId); 700 result.loc = Location.NULL; 701 702 return result; 703 } 704 705 706 //// Statement translation 707 708 // Utility routines 709 710 private boolean isRecursiveInvocation(/*@ non_null */ RoutineDecl r) { 711 Translate t = this; 712 while (t != null) { 713 if (t.rdCurrent == r) { 714 return true; // the routine has been visited before 715 } 716 t = t.inlineParent; 717 } 718 return false; 719 } 720 721 /** Reduces number of stack marks by 1. */ 722 723 private GuardedCmd opBlockCmd(Expr label) { 724 GuardedCmd g= GC.seq(GuardedCmdVec.popFromStackVector(code)); 725 GuardedCmd ifc= GC.ifcmd(GC.nary(TagConstants.ANYEQ, GC.ecvar, label), 726 GC.skip(), GC.raise()); 727 return GC.trycmd(g, ifc); 728 } 729 730 private Expr breakLabel(Stmt s) {return GC.symlit(s, "L_");} 731 private Expr continueLabel(Stmt s) {return GC.symlit(s, "C_");} 732 733 /** 734 * Emits the commands <code>EC= label; raise</code> to <code>code</code>. 735 */ 736 private void raise(Expr label) { 737 code.addElement(GC.gets(GC.ecvar, label)); 738 code.addElement(GC.raise()); 739 } 740 741 /** 742 * Computes purity information for Java expression <code>e</code>, translates 743 * <code>e</code> (emitting any code needed to account for impurities or side 744 * effects in the expression), and emits code that performs a <code>RAISE 745 * label</code> command if the expression evaluates to <code>false</code>. As 746 * usual, emitted code is appended to <code>code</code> and temporaries are 747 * appended to <code>temporaries</code>. 748 */ 749 private void guard(Expr e, Expr label) { 750 Expr grd = ptrExpr(e); 751 code.push(); // popped off by boxPopFromStackVector 752 code.addElement(GC.assume(grd)); 753 code.addElement(GC.skip()); 754 code.push(); // popped off by boxPopFromStackVector 755 code.addElement(GC.assumeNegation(grd)); 756 raise(label); 757 GuardedCmd ifc= GC.boxPopFromStackVector(code); 758 code.addElement(ifc); 759 } 760 761 /** 762 * Appends to <code>code</code> commands that make up a loop with nominal body 763 * <code>guard;body</code>, where <code>label</code> is raised within 764 * <code>body</code> to terminate the loop. The vector <code>J</code> contains 765 * the user-declared loop invariant pragmas. The vector <code>decreases</code> 766 * contains the user-declared bound function pragmas. The scope of the variables 767 * in <code>tempVars</code> is the nominal body; this method will wrap an 768 * appropriate <code>var .. in .. end</code> command around these. 769 */ 770 private void makeLoop(int sLoop, int eLoop, int locHotspot, 771 GenericVarDeclVec tempVars, 772 GuardedCmd guard, 773 GuardedCmd body, 774 /*@ non_null */ ExprStmtPragmaVec J, 775 ExprStmtPragmaVec decreases, 776 LocalVarDeclVec skolemConsts, 777 /*@ non_null */ ExprStmtPragmaVec P, 778 Expr label) { 779 780 code.push(); // this mark popped by "opBlockCmd" 781 782 // construct old variants of the variables that are targets of the loop. 783 code.push(); 784 temporaries.push(); 785 GuardedCmd S = GC.seq(guard, body); 786 Set normalTargets = Targets.normal(GC.block(tempVars, S)); 787 Hashtable h = GetSpec.makeSubst(normalTargets.elements(), "loopold"); 788 789 for (Enumeration keys = h.keys(); keys.hasMoreElements(); ) { 790 GenericVarDecl vd = (GenericVarDecl) keys.nextElement(); 791 VariableAccess va = (VariableAccess) h.get(vd); 792 temporaries.addElement(va.decl); 793 code.addElement(GC.assume(GC.nary(TagConstants.ANYEQ, 794 VariableAccess.make(vd.id, sLoop, vd), va))); 795 } 796 797 798 ExprVec ev = ExprVec.make(10); 799 800 ConditionVec invs = ConditionVec.make(); 801 for (int i = 0; i < J.size(); i++) { 802 TrAnExpr.initForClause(); 803 ExprStmtPragma loopinv = J.elementAt(i); 804 Expr pred = TrAnExpr.trSpecExpr(loopinv.expr, null, h); // FIXME - what about formal params in old? 805 Condition cond = GC.condition(TagConstants.CHKLOOPINVARIANT, 806 pred, 807 loopinv.getStartLoc()); 808 if (TrAnExpr.extraSpecs) ev.append(addNewAssumptionsNow()); 809 invs.addElement(cond); 810 } 811 812 DecreasesInfoVec decs = DecreasesInfoVec.make(); 813 for (int i = 0; i < decreases.size(); i++) { 814 ExprStmtPragma d = decreases.elementAt(i); 815 TrAnExpr.initForClause(); 816 Expr de = TrAnExpr.trSpecExpr(d.expr); // FIXME - what about old? 817 int loc = d.getStartLoc(); 818 VariableAccess fOld = temporary("decreases", loc, loc); 819 DecreasesInfo di = new DecreasesInfo(loc, de, fOld); 820 if (TrAnExpr.extraSpecs) ev.append(addNewAssumptionsNow()); 821 decs.addElement(di); 822 } 823 824 ExprVec preds = ExprVec.make(); 825 for (int i = 0; i < P.size(); i++) { 826 ExprStmtPragma looppred = P.elementAt(i); 827 Expr e = TrAnExpr.trSpecExpr(looppred.expr, null, h); // FIXME - what about params? 828 if (TrAnExpr.extraSpecs) ev.append(addNewAssumptionsNow()); 829 preds.addElement(e); 830 } 831 832 // If we ever implement the "safe" (as opposed to "fast") version of 833 // loops, then "invs" should be extended with loop object invariant 834 // conditions, and "guard" should be prefixed by a sequence of 835 // TargetTypeCorrect assume commands, per ESCJ 16. 836 837 LoopCmd loop = GC.loop(sLoop, eLoop, locHotspot, h, 838 invs, decs, skolemConsts, preds, 839 tempVars, guard, body); 840 switch (Main.options().loopTranslation) { 841 case Options.LOOP_FAST: 842 case Options.LOOP_FALL_THRU: 843 desugarLoopFast(loop,ev); 844 break; 845 846 case Options.LOOP_SAFE: 847 desugarLoopSafe(loop,ev); 848 break; 849 850 default: 851 Assert.fail("unexpected loop translation scheme: " + 852 Main.options().loopTranslation); 853 } 854 855 code.addElement(loop); 856 857 code.addElement(spill()); 858 859 code.addElement(opBlockCmd(label)); 860 } 861 862 /** 863 * Desugars <code>loop</code> according to the fast option. In particular, sets 864 * <code>loop.desugared</code> to the desugaring. 865 */ 866 private void desugarLoopFast(LoopCmd loop, ExprVec axs) { 867 // A fast-desugared loop has the shape: 868 // var V in J;B;S;J;B;S;J;..;fail end 869 // where "V" is the list of temporary variables used within the 870 // loop, "J" is the command that checks loop invariants, "B" is 871 // the guard command, and "S" is the rest of the body of the 872 // loop. 873 // 874 // The number of repetitions of "J;B;S" is determined by 875 // "Main.loopUnrollCount". After these repetitions is another 876 // "J", and if "Main.loopUnrollHalf" is "true", then there is 877 // then one more "B". As shown above, the sequence ends with 878 // a "fail" command. 879 // 880 // If "Main.traceInfo" is positive, then each "J" is immediately 881 // preceded by a command of the form: 882 // assume (lblpos trace.LoopIter^L#i true) 883 // where "L" is the source location of the loop and "i" is the 884 // iteration count. 885 886 // Build a command that checks loop invariants 887 code.push(); // this mark popped below 888 checkLoopInvariants(loop,axs); 889 GuardedCmd J = GC.seq(GuardedCmdVec.popFromStackVector(code)); 890 891 code.push(); // this mark popped below after for loop 892 893 String locString = UniqName.locToSuffix(loop.getStartLoc()) + "#"; 894 895 int numOfComponents = 3 * Main.options().loopUnrollCount + 896 (Main.options().loopUnrollHalf ? 2 : 1); 897 int iComp = 0; 898 int i = 0; 899 for ( ; true; i++) { 900 code.push(); // this mark popped below 901 902 // -- J -- 903 Assert.notFalse(iComp != numOfComponents); 904 if (Main.options().traceInfo > 0) { 905 String label = locString + i; 906 code.addElement(traceInfoLabelCmd(loop.getStartLoc(), 907 loop.getEndLoc(), 908 "LoopIter", label)); 909 } 910 code.addElement(J); 911 iComp++; 912 if (iComp == numOfComponents) { 913 break; 914 } 915 // -- B -- 916 addLoopDecreases(loop, 0); // fOld = F; 917 GuardedCmd B = loop.guard; 918 if (Main.options().traceInfo > 0 && 0 < i) { 919 B = cloneGuardedCommand(B); 920 } 921 code.addElement(B); 922 iComp++; 923 if (iComp == numOfComponents) { 924 break; 925 } 926 // -- S -- 927 GuardedCmd S = loop.body; 928 if (Main.options().traceInfo > 0 && 0 < i) { 929 S = cloneGuardedCommand(S); 930 } 931 code.addElement(S); 932 addNewAssumptionsNow(axs); 933 addLoopDecreases(loop, 1); // check 0 <= fOld; 934 addLoopDecreases(loop, 2); // check F < fOld; 935 iComp++; 936 937 GuardedCmd iter = wrapUpUnrolledIteration(locString, i, loop.tempVars); 938 code.addElement(iter); 939 940 Assert.notFalse(iComp != numOfComponents); 941 } 942 943 // pop once more to get J or J;B as the case might be 944 GuardedCmd iter = wrapUpUnrolledIteration(locString, i, loop.tempVars); 945 code.addElement(iter); 946 947 // Stop unrolling here 948 if (Main.options().loopTranslation != Options.LOOP_FALL_THRU) { 949 code.addElement(GC.fail()); 950 } 951 952 loop.desugared = GC.seq(GuardedCmdVec.popFromStackVector(code)); 953 } 954 955 //@ requires 0 <= iteration; 956 private GuardedCmd wrapUpUnrolledIteration(/*@ non_null */ String locString, 957 int iteration, 958 /*@ non_null */ GenericVarDeclVec tempVars) { 959 GuardedCmd body = GC.seq(GuardedCmdVec.popFromStackVector(code)); 960 body = GC.block(tempVars, body); 961 GuardedCmd iter = DynInstCmd.make(locString + iteration, body); 962 return iter; 963 } 964 965 /** 966 * Adds to <code>code</code> the various pieces of the translation of the 967 * decreases pragma. The pieces are: 968 * <ul> 969 * <li> 0. fOld = F; 970 * <li> 1. check 0 <= fOld; 971 * <li> 2. check F < fOld; 972 * </ul> 973 */ 974 //@ requires 0 <= piece && piece < 3; 975 //@ modifies code.elementCount; 976 private void addLoopDecreases(/*@ non_null */ LoopCmd loop, 977 int piece) { 978 for (int i = 0; i < loop.decreases.size(); i++) { 979 DecreasesInfo di = loop.decreases.elementAt(i); 980 switch (piece) { 981 case 0: // fOld = F; 982 code.addElement(GC.gets(di.fOld, di.f)); 983 break; 984 case 1: // check 0 <= fOld; 985 addCheck(loop.locHotspot, TagConstants.CHKDECREASES_BOUND, 986 GC.nary(TagConstants.INTEGRALLE, GC.zerolit, di.fOld), 987 di.loc); 988 break; 989 case 2: // check F < fOld; 990 addCheck(loop.locHotspot, TagConstants.CHKDECREASES_DECR, 991 GC.nary(TagConstants.INTEGRALLT, di.f, di.fOld), 992 di.loc); 993 break; 994 default: 995 //@ unreachable; 996 Assert.fail("addLoopDecreases: unexpected piece number"); 997 break; 998 } 999 } 1000 } 1001 1002 1003 /** 1004 * targets is set of GenericVarDecls. aTargets is set of ATargets. 1005 */ 1006 public GuardedCmd modifyATargets(/*@ non_null */ Set aTargets, int loc) { 1007 code.push(); 1008 for (Enumeration e = aTargets.elements(); e.hasMoreElements();) { 1009 ATarget at = (ATarget)e.nextElement(); 1010 VariableAccess va = VariableAccess.make(at.x.id, loc, at.x); 1011 1012 if (at.indices.length == 0 || 1013 (at.indices[0] == null && 1014 (at.indices.length == 1 || at.indices[1] == null))) { 1015 // x, x[*], x[*][*] 1016 // System.out.println("x = " + at.x.id.toString() + 1017 // ", at.indices.length = " + at.indices.length); 1018 code.addElement(modify(va, loc)); 1019 } else if (at.indices.length == 1) { 1020 // x[e] 1021 VariableAccess newVal = temporary(va.id.toString(), loc, loc); 1022 code.addElement(GC.subgets(va, at.indices[0], newVal)); 1023 } else if (at.indices[0] == null) { 1024 // x[*][e] 1025 VariableAccess newVal = temporary(va.id.toString(), loc, loc); 1026 VariableAccess var1 = GC.makeVar("i", loc); 1027 VariableAccess var2 = GC.makeVar("j", loc); 1028 1029 Expr a = GC.implies(GC.nary(TagConstants.ANYNE, var2, at.indices[1]), 1030 GC.nary(TagConstants.ANYEQ, 1031 GC.select(GC.select(va, var1), var2), 1032 GC.select(GC.select(newVal, var1), var2))); 1033 code.addElement(GC.assume(GC.forall(var1.decl,GC.forall(var2.decl, a )))); 1034 code.addElement(GC.gets(va, newVal)); 1035 } else if (at.indices[1] == null) { 1036 // x[e][*] 1037 VariableAccess newVal = temporary(va.id.toString(), loc, loc); 1038 VariableAccess var1 = GC.makeVar("i", loc); 1039 VariableAccess var2 = GC.makeVar("j", loc); 1040 1041 Expr a = GC.implies(GC.and( GC.nary(TagConstants.ANYNE, var1, at.indices[0]), 1042 GC.nary(TagConstants.IS, var2, TrAnExpr.trType(Types.intType))), 1043 GC.nary(TagConstants.ANYEQ, 1044 GC.select(GC.select(va, var1), var2), 1045 GC.select(GC.select(newVal, var1), var2))); 1046 code.addElement(GC.assume(GC.forall(var1.decl, GC.forall(var2.decl, a)))); 1047 code.addElement(GC.gets(va, newVal)); 1048 } else { 1049 // x[e][e] 1050 VariableAccess newVal = temporary(va.id.toString(), loc, loc); 1051 code.addElement(GC.subsubgets(va, at.indices[0], at.indices[1], newVal)); 1052 } 1053 } 1054 1055 return GC.seq(GuardedCmdVec.popFromStackVector(code)); 1056 } 1057 1058 public GuardedCmd modify(/*@ non_null */ Set simpleTargets, int loc) { 1059 code.push(); 1060 for (Enumeration e = simpleTargets.elements(); e.hasMoreElements();) { 1061 GenericVarDecl at = (GenericVarDecl)e.nextElement(); 1062 VariableAccess va = VariableAccess.make(at.id, loc, at); 1063 code.addElement(modify(va, loc)); 1064 } 1065 1066 return GC.seq(GuardedCmdVec.popFromStackVector(code)); 1067 } 1068 1069 /** 1070 * Desugars <code>loop</code> according to the safe option. In particular, sets 1071 * <code>loop.desugared</code> to the desugaring. 1072 */ 1073 public void desugarLoopSafe(LoopCmd loop, ExprVec axs) { 1074 // Build a command that checks loop invariants safely 1075 1076 code.push(); // this mark popped below 1077 checkLoopInvariants(loop,axs); 1078 code.addElement(GC.fail()); 1079 GuardedCmd checkInvariantsInitially = 1080 GC.seq(GuardedCmdVec.popFromStackVector(code)); 1081 1082 code.push(); // this mark popped shortly 1083 addLoopDecreases(loop, 0); // fOld = F; 1084 code.addElement(loop.guard); 1085 code.addElement(loop.body); 1086 addNewAssumptionsNow(axs); 1087 addLoopDecreases(loop, 1); // check 0 <= fOld; 1088 addLoopDecreases(loop, 2); // check F < fOld; 1089 GuardedCmd S = GC.seq(GuardedCmdVec.popFromStackVector(code)); 1090 1091 Set vds = Targets.normal(GC.block(loop.tempVars, S)); 1092 GuardedCmd modifyGc = modify(vds, loop.locStart); 1093 1094 if( Main.options().preciseTargets ) { 1095 Set aTargets = ATarget.compute( GC.block(loop.tempVars, loop )); 1096 modifyGc = modifyATargets( aTargets, S.getStartLoc()); 1097 } 1098 1099 code.push(); // this mark popped below 1100 code.addElement(modifyGc); 1101 1102 for (Enumeration e = vds.elements(); e.hasMoreElements();) { 1103 GenericVarDecl vd = (GenericVarDecl)e.nextElement(); 1104 1105 if (!vd.id.toString().endsWith("@init")) { 1106 code.addElement(GC.assume(TrAnExpr.targetTypeCorrect(vd, loop.oldmap))); 1107 } 1108 } 1109 addNewAssumptionsNow(axs); 1110 for (int i = 0; i < loop.invariants.size(); i++) { 1111 Condition cond = loop.invariants.elementAt(i); 1112 code.addElement(GC.assume(cond.pred)); 1113 } 1114 1115 if (Main.options().traceInfo > 0) { 1116 String label = UniqName.locToSuffix(loop.getStartLoc()); 1117 code.addElement(traceInfoLabelCmd(loop, "LoopIter")); 1118 } 1119 1120 code.addElement(DynInstCmd.make(UniqName.locToSuffix(loop.getStartLoc()), S)); 1121 1122 checkLoopInvariants(loop,axs); 1123 code.addElement(GC.fail()); 1124 GuardedCmd checkInvariantsAfterIteration = 1125 GC.seq(GuardedCmdVec.popFromStackVector(code)); 1126 1127 loop.desugared = GC.choosecmd(checkInvariantsInitially, 1128 checkInvariantsAfterIteration); 1129 } 1130 1131 /** 1132 * Add to "code" checks for all loop invariants of "loop". 1133 */ 1134 private void checkLoopInvariants(/*@ non_null */ LoopCmd loop, ExprVec axs) { 1135 addNewAssumptionsNow(axs); 1136 for (int i = 0; i < loop.invariants.size(); i++) { 1137 Condition cond = loop.invariants.elementAt(i); 1138 addCheck(loop.locHotspot, cond); 1139 } 1140 } 1141 1142 //@ requires Main.options().traceInfo > 0; 1143 private GuardedCmd traceInfoLabelCmd(/*@ non_null */ ASTNode ast, 1144 /*@ non_null */ String traceInfoTag) { 1145 int sloc = ast.getStartLoc(); 1146 int eloc = ast.getEndLoc(); 1147 return traceInfoLabelCmd(sloc, eloc, traceInfoTag, sloc); 1148 } 1149 1150 //@ requires Main.options().traceInfo > 0; 1151 //@ requires loc != Location.NULL; 1152 private GuardedCmd traceInfoLabelCmd(/*@ non_null */ ASTNode ast, 1153 /*@ non_null */ String traceInfoTag, 1154 int loc) { 1155 return traceInfoLabelCmd(ast.getStartLoc(), ast.getEndLoc(), 1156 traceInfoTag, loc); 1157 } 1158 1159 //@ requires Main.options().traceInfo > 0; 1160 //@ requires loc != Location.NULL; 1161 private GuardedCmd traceInfoLabelCmd(int sloc, int eloc, 1162 /*@ non_null */ String traceInfoTag, 1163 int loc) { 1164 return traceInfoLabelCmd(sloc, eloc, traceInfoTag, 1165 UniqName.locToSuffix(loc)); 1166 } 1167 1168 1169 private GuardedCmd traceInfoLabelCmd(int sloc, int eloc, 1170 /*@ non_null */ String traceInfoTag, 1171 String sortSeq) { 1172 Assert.notFalse(Main.options().traceInfo > 0); 1173 1174 String str = "trace." + traceInfoTag + "^" + sortSeq; 1175 Identifier id = Identifier.intern(str); 1176 Expr l = LabelExpr.make(sloc, eloc, true, id, GC.truelit); 1177 return GC.assume(l); 1178 } 1179 1180 /** 1181 * This method returns a guarded command <code>G</code> that is like 1182 * <code>gc</code> except that where <code>gc</code> contains a mutable command, 1183 * <code>G</code> contains a fresh copy of that command. Thus, the resulting 1184 * command is as good as a fresh copy of <code>gc</code>, since all other guarded 1185 * commands are to be read-only after construction.<p> 1186 * 1187 * There is only one mutable command, namely an "assume" command 1188 * of the form: 1189 * <pre> 1190 * assume (lblpos id true) 1191 * </pre> 1192 * where "id" is a trace label. A fresh copy of this command consists of a fresh 1193 * assume command with a fresh labeled expression. However, the "id" reference 1194 * may be shared in the fresh command. 1195 */ 1196 private GuardedCmd cloneGuardedCommand(/*@ non_null */ GuardedCmd gc) { 1197 switch (gc.getTag()) { 1198 case TagConstants.SKIPCMD: 1199 case TagConstants.RAISECMD: 1200 case TagConstants.ASSERTCMD: 1201 case TagConstants.GETSCMD: 1202 case TagConstants.SUBGETSCMD: 1203 case TagConstants.SUBSUBGETSCMD: 1204 case TagConstants.RESTOREFROMCMD: 1205 return gc; 1206 1207 case TagConstants.ASSUMECMD: { 1208 ExprCmd ec = (ExprCmd)gc; 1209 if (ec.pred.getTag() == TagConstants.LABELEXPR) { 1210 LabelExpr le = (LabelExpr)ec.pred; 1211 if (le.positive && le.expr == GC.truelit) { 1212 String str = le.label.toString(); 1213 if (ErrorMsg.isTraceLabel(str)) { 1214 return GC.assume(LabelExpr.make(le.sloc, le.eloc, true, 1215 le.label, GC.truelit)); 1216 } 1217 } 1218 } 1219 return gc; 1220 } 1221 1222 case TagConstants.VARINCMD: { 1223 VarInCmd vc = (VarInCmd)gc; 1224 GuardedCmd body = cloneGuardedCommand(vc.g); 1225 if (body != vc.g) { 1226 return GC.block(vc.v, body); 1227 } 1228 return gc; 1229 } 1230 1231 case TagConstants.DYNINSTCMD: { 1232 DynInstCmd dc = (DynInstCmd)gc; 1233 GuardedCmd body = cloneGuardedCommand(dc.g); 1234 if (body != dc.g) { 1235 return DynInstCmd.make(dc.s, body); 1236 } 1237 return gc; 1238 } 1239 1240 case TagConstants.SEQCMD: { 1241 SeqCmd sc = (SeqCmd)gc; 1242 int len = sc.cmds.size(); 1243 GuardedCmd[] cmds = null; // allocate this array lazily 1244 for (int i = 0; i < len; i++) { 1245 GuardedCmd c = sc.cmds.elementAt(i); 1246 GuardedCmd g = cloneGuardedCommand(c); 1247 if (g != c) { 1248 if (cmds == null) { 1249 cmds = new GuardedCmd[len]; 1250 // all elements up until now have been the same 1251 for (int j = 0; j < i; j++) { 1252 cmds[j] = sc.cmds.elementAt(j); 1253 } 1254 } 1255 cmds[i] = g; 1256 } else if (cmds != null) { 1257 cmds[i] = g; 1258 } 1259 } 1260 if (cmds != null) { 1261 return GC.seq(GuardedCmdVec.make(cmds)); 1262 } 1263 return gc; 1264 } 1265 1266 case TagConstants.CALL: { 1267 Call call = (Call)gc; 1268 GuardedCmd desugared = cloneGuardedCommand(call.desugared); 1269 if (desugared != call.desugared) { 1270 Call newCall = Call.make(call.args, call.scall, call.ecall, 1271 call.inlined); 1272 newCall.rd = call.rd; 1273 newCall.spec = call.spec; 1274 newCall.desugared = desugared; 1275 return newCall; 1276 } 1277 return gc; 1278 } 1279 1280 case TagConstants.TRYCMD: { 1281 CmdCmdCmd tc = (CmdCmdCmd)gc; 1282 GuardedCmd g1 = cloneGuardedCommand(tc.g1); 1283 GuardedCmd g2 = cloneGuardedCommand(tc.g2); 1284 if (g1 != tc.g1 || g2 != tc.g2) { 1285 return GC.trycmd(g1, g2); 1286 } 1287 return gc; 1288 } 1289 1290 case TagConstants.LOOPCMD: { 1291 LoopCmd lp = (LoopCmd)gc; 1292 GuardedCmd guard = cloneGuardedCommand(lp.guard); 1293 GuardedCmd body = cloneGuardedCommand(lp.body); 1294 LoopCmd newLoop = GC.loop(lp.locStart, lp.locEnd, lp.locHotspot, lp.oldmap, 1295 lp.invariants, lp.decreases, 1296 lp.skolemConstants, lp.predicates, lp.tempVars, 1297 guard, body); 1298 newLoop.desugared = cloneGuardedCommand(lp.desugared); 1299 // A desugared loop contains trace info labels, and thus: 1300 Assert.notFalse(newLoop.desugared != lp.desugared); 1301 return newLoop; 1302 } 1303 1304 case TagConstants.CHOOSECMD: { 1305 CmdCmdCmd cc = (CmdCmdCmd)gc; 1306 GuardedCmd g1 = cloneGuardedCommand(cc.g1); 1307 GuardedCmd g2 = cloneGuardedCommand(cc.g2); 1308 if (g1 != cc.g1 || g2 != cc.g2) { 1309 return GC.choosecmd(g1, g2); 1310 } 1311 return gc; 1312 } 1313 1314 default: 1315 //@ unreachable; 1316 Assert.notFalse(false); 1317 return null; 1318 } 1319 } 1320 1321 /** 1322 * Pops <code>declaredLocals</code> and <code>code</code> and then appends 1323 * <code>code</code> with a VARINCMD (if there were any new declared locals) or a 1324 * sequence of commands (otherwise). The new code becomes the body of the 1325 * VARINCMD or the sequence of commands. 1326 */ 1327 private void wrapUpDeclBlock() { 1328 if (code.size() == 0) { 1329 declaredLocals.pop(); 1330 code.pop(); 1331 } else { 1332 if (declaredLocals.size() == 0) { 1333 declaredLocals.pop(); 1334 code.merge(); 1335 } else { 1336 code.addElement(popDeclBlock()); 1337 } 1338 } 1339 } 1340 1341 /** 1342 * Pops the code and declared local variables, makes these into a command 1343 * (usually a VAR .. IN .. END command, but possibly a sequence command if there 1344 * are no declared local variables). The command is then returned. 1345 */ 1346 private GuardedCmd popDeclBlock() { 1347 GuardedCmd body= GC.seq(GuardedCmdVec.popFromStackVector(code)); 1348 // The following "if" statement seems to be a bug, because it 1349 // fails to pop "declaredLocals". Better would be not to even 1350 // check the "if", but to always pop from the stack vector, and 1351 // then let "GC.block" do the optimization. --KRML, 29 Sep 1999 1352 // Actually, popDeclBlock is not called with declaredLocals.size()==0 1353 if (declaredLocals.size() == 0) 1354 return body; 1355 GenericVarDeclVec locals 1356 = GenericVarDeclVec.popFromStackVector(declaredLocals); 1357 return GC.block(locals, body); 1358 } 1359 1360 /** 1361 * Translate <code>stmt</code> into a sequence of guarded commands 1362 * that are appended to <code>code</code>. 1363 * 1364 * <p> Temporaries generated for expressions in <code>stmt</code> 1365 * are added to <code>temporaries</code>, loop invariant pragmas are 1366 * added to <code>loopinvariants</code>, decreases pragmas are added 1367 * to <code>loopDecreases</code>, loop predicates are added to 1368 * <code>looppredicates<code>, and local skolemized variables are 1369 * added to <code>skolemConstants</code>. </p> 1370 * 1371 * @param stmt the statement that is to be translated. 1372 */ 1373 //@ assignable loopinvariants, loopDecreases, skolemConstants, loopPredicates; 1374 private void trStmt(/*@ non_null */ Stmt stmt, TypeDecl decl) { 1375 int tag = stmt.getTag(); 1376 switch (tag) { 1377 1378 case TagConstants.RETURNSTMT: 1379 { 1380 ReturnStmt r = (ReturnStmt)stmt; 1381 if (r.expr != null) 1382 code.addElement(GC.gets(GC.resultvar, ptrExpr(r.expr))); 1383 if (Main.options().traceInfo > 0) { 1384 // add a label to track the return 1385 GuardedCmd g = traceInfoLabelCmd(r, "Return", r.loc); 1386 code.addElement(g); 1387 } 1388 raise(GC.ec_return); 1389 return; 1390 } 1391 1392 case TagConstants.THROWSTMT: 1393 { 1394 ThrowStmt t = (ThrowStmt)stmt; 1395 code.addElement(GC.gets(GC.xresultvar, ptrExpr(t.expr))); 1396 nullCheck(t.expr, GC.xresultvar, t.getStartLoc()); 1397 if (Main.options().traceInfo > 0) { 1398 // add a label to track the throw 1399 GuardedCmd g = traceInfoLabelCmd(t, "Throw", t.loc); 1400 code.addElement(g); 1401 } 1402 raise(GC.ec_throw); 1403 return; 1404 } 1405 1406 case TagConstants.SWITCHSTMT: 1407 { 1408 SwitchStmt c = (SwitchStmt)stmt; 1409 VariableAccess e = fresh(c.expr, c.expr.getStartLoc(), "switch"); 1410 code.addElement( GC.gets( e, ptrExpr( c.expr ))); 1411 1412 // we walk thru the switch body, building up the GC 1413 // at each case label, we wrap up the GC generated so far 1414 // on the lhs of a box, and put the new assume on the rhs. 1415 1416 code.push(); 1417 code.addElement(GC.assume(GC.falselit)); 1418 1419 for(int i=0; i<c.stmts.size(); i++) { 1420 Stmt s = c.stmts.elementAt(i); 1421 1422 if( s.getTag() != TagConstants.SWITCHLABEL ) { 1423 // just a regular statement 1424 trStmt( s , decl); 1425 } else { 1426 1427 SwitchLabel sl = (SwitchLabel)s; 1428 1429 GuardedCmdVec vec = GuardedCmdVec.popFromStackVector(code); 1430 GuardedCmd boxLhs = GC.block(GenericVarDeclVec.make(), 1431 GC.seq(vec)); 1432 1433 Expr C; 1434 if( sl.expr != null ) { 1435 1436 C = GC.nary(s.getStartLoc(),s.getEndLoc(), 1437 TagConstants.INTEGRALEQ, 1438 e, TrAnExpr.trSpecExpr(sl.expr)); // FIXME -why a trSpecExpr? 1439 } else { 1440 1441 C = GC.truelit; 1442 for(int j=0; j<c.stmts.size(); j++) { 1443 1444 Stmt s2 = c.stmts.elementAt(j); 1445 if( s2.getTag() == TagConstants.SWITCHLABEL ) { 1446 1447 SwitchLabel sl2 = (SwitchLabel)s2; 1448 1449 if( sl2.expr != null ) 1450 C = GC.and(s.getStartLoc(),s.getEndLoc(), 1451 C, 1452 GC.nary(s.getStartLoc(),s.getEndLoc(), 1453 TagConstants.INTEGRALNE, 1454 e, TrAnExpr.trSpecExpr(sl2.expr))); // FIXME - why a specExpr 1455 } 1456 } 1457 } 1458 1459 GuardedCmd boxRhs = GC.assume(C); 1460 if (Main.options().traceInfo > 0) { 1461 // add a label to track the switch branch taken 1462 GuardedCmd g = traceInfoLabelCmd(s, "Switch"); 1463 boxRhs = GC.seq(g, boxRhs); 1464 } 1465 GuardedCmd box = GC.choosecmd(boxLhs, boxRhs); 1466 1467 code.push(); 1468 code.addElement(box); 1469 1470 } 1471 } 1472 1473 GuardedCmd body = GC.seq(GuardedCmdVec.popFromStackVector(code)); 1474 GuardedCmd block = GC.blockL(c, body); 1475 code.addElement(block); 1476 1477 return; 1478 } 1479 1480 case TagConstants.BLOCKSTMT: 1481 { 1482 GenericBlockStmt b = (GenericBlockStmt)stmt; 1483 declaredLocals.push(); // this mark popped by "wrapUpDeclBlock" 1484 code.push(); // this mark popped by "wrapUpDeclBlock" 1485 1486 for (int i= 0; i < b.stmts.size(); i++) 1487 trStmt(b.stmts.elementAt(i),decl); 1488 1489 wrapUpDeclBlock(); 1490 return; 1491 } 1492 1493 case TagConstants.WHILESTMT: 1494 { 1495 WhileStmt w = (WhileStmt)stmt; 1496 Expr bLabel = breakLabel(w); 1497 1498 temporaries.push(); // this mark popped below 1499 1500 code.push(); // this mark popped below 1501 guard(w.expr, bLabel); 1502 GuardedCmd guardCmd = 1503 GC.seq(GuardedCmdVec.popFromStackVector(code)); 1504 1505 ExprStmtPragmaVec invariants = loopinvariants; 1506 loopinvariants = ExprStmtPragmaVec.make(); 1507 ExprStmtPragmaVec decreases = loopDecreases; 1508 loopDecreases = ExprStmtPragmaVec.make(); 1509 ExprStmtPragmaVec predicates = loopPredicates; 1510 loopPredicates = ExprStmtPragmaVec.make(); 1511 LocalVarDeclVec skolemConsts = skolemConstants; 1512 skolemConstants = LocalVarDeclVec.make(); 1513 1514 code.push(); // this mark popped by "opBlockCmd" 1515 trStmt(w.stmt,decl); 1516 GuardedCmd bodyCmd = opBlockCmd(continueLabel(w)); 1517 1518 makeLoop(w.getStartLoc(), w.getEndLoc(), w.locGuardOpenParen, 1519 GenericVarDeclVec.popFromStackVector(temporaries), 1520 guardCmd, bodyCmd, invariants, decreases, 1521 skolemConsts, predicates, bLabel); 1522 1523 return; 1524 } 1525 1526 case TagConstants.DOSTMT: 1527 { 1528 DoStmt d = (DoStmt)stmt; 1529 Expr bLabel = breakLabel(d); 1530 1531 // the following 3 marks are popped below 1532 temporaries.push(); 1533 code.push(); 1534 1535 ExprStmtPragmaVec invariants = loopinvariants; 1536 loopinvariants = ExprStmtPragmaVec.make(); 1537 ExprStmtPragmaVec decreases = loopDecreases; 1538 loopDecreases = ExprStmtPragmaVec.make(); 1539 ExprStmtPragmaVec predicates = loopPredicates; 1540 loopPredicates = ExprStmtPragmaVec.make(); 1541 LocalVarDeclVec skolemConsts = skolemConstants; 1542 skolemConstants = LocalVarDeclVec.make(); 1543 1544 code.push(); // this mark popped by "opBlockCmd" 1545 trStmt(d.stmt,decl); 1546 code.addElement(opBlockCmd(continueLabel(d))); 1547 1548 guard(d.expr, bLabel); 1549 1550 GuardedCmd body = GC.seq(GuardedCmdVec.popFromStackVector(code)); 1551 1552 makeLoop(d.getStartLoc(), d.getEndLoc(), d.loc, 1553 GenericVarDeclVec.popFromStackVector(temporaries), 1554 GC.skip(), body, invariants, decreases, 1555 skolemConsts, predicates, bLabel); 1556 return; 1557 } 1558 1559 case TagConstants.FORSTMT: 1560 { 1561 ForStmt x = (ForStmt)stmt; 1562 1563 declaredLocals.push(); // this mark popped by "wrapUpDeclBlock" 1564 code.push(); // this mark popped by "wrapUpDeclBlock" 1565 1566 // initializers 1567 for (int i= 0; i < x.forInit.size(); i++) 1568 trStmt(x.forInit.elementAt(i),decl); 1569 1570 Expr bLabel = breakLabel(x); 1571 1572 temporaries.push(); // this mark popped below 1573 1574 ExprStmtPragmaVec invariants = loopinvariants; 1575 loopinvariants = ExprStmtPragmaVec.make(); 1576 ExprStmtPragmaVec decreases = loopDecreases; 1577 loopDecreases = ExprStmtPragmaVec.make(); 1578 ExprStmtPragmaVec predicates = loopPredicates; 1579 loopPredicates = ExprStmtPragmaVec.make(); 1580 LocalVarDeclVec skolemConsts = skolemConstants; 1581 skolemConstants = LocalVarDeclVec.make(); 1582 1583 code.push(); // this mark popped below 1584 guard(x.test, bLabel); 1585 GuardedCmd guardCmd = 1586 GC.seq(GuardedCmdVec.popFromStackVector(code)); 1587 1588 code.push(); // this mark popped below 1589 1590 code.push(); // this mark popped by "opBlockCmd" 1591 trStmt(x.body,decl); 1592 code.addElement(opBlockCmd(continueLabel(x))); 1593 1594 for(int i=0; i < x.forUpdate.size(); i++) 1595 ptrExpr(x.forUpdate.elementAt(i)); 1596 1597 GuardedCmd bodyCmd = GC.seq(GuardedCmdVec.popFromStackVector(code)); 1598 1599 makeLoop(x.getStartLoc(), x.getEndLoc(), x.locFirstSemi, 1600 GenericVarDeclVec.popFromStackVector(temporaries), 1601 guardCmd, bodyCmd, invariants, decreases, 1602 skolemConsts, predicates, bLabel); 1603 1604 wrapUpDeclBlock(); 1605 return; 1606 } 1607 1608 case TagConstants.IFSTMT: 1609 { 1610 IfStmt i = (IfStmt)stmt; 1611 trIfStmt(i.expr, i.thn, i.els, decl); 1612 return; 1613 } 1614 1615 case TagConstants.BREAKSTMT: 1616 { 1617 BreakStmt b = (BreakStmt)stmt; 1618 Stmt label = TypeCheck.inst.getBranchLabel(b); 1619 if (Main.options().traceInfo > 0) { 1620 // add a label to track the break 1621 GuardedCmd g = traceInfoLabelCmd(b, "Break", b.loc); 1622 code.addElement(g); 1623 } 1624 raise(breakLabel(label)); 1625 return; 1626 } 1627 1628 case TagConstants.CONTINUESTMT: 1629 { 1630 ContinueStmt c = (ContinueStmt)stmt; 1631 Stmt label = TypeCheck.inst.getBranchLabel(c); 1632 if (Main.options().traceInfo > 0) { 1633 // add a label to track the continue 1634 GuardedCmd g = traceInfoLabelCmd(c, "Continue", c.loc); 1635 code.addElement(g); 1636 } 1637 raise(continueLabel(label)); 1638 return; 1639 } 1640 1641 case TagConstants.SYNCHRONIZESTMT: 1642 { 1643 SynchronizeStmt x = (SynchronizeStmt)stmt; 1644 int xStart = x.getStartLoc(); 1645 int xEnd = x.getEndLoc(); 1646 VariableAccess mu = fresh(x.expr, x.expr.getStartLoc(), 1647 "synchronized"); 1648 Expr e = ptrExpr(x.expr); 1649 code.addElement(GC.gets(mu,e)); 1650 1651 nullCheck(x.expr, mu, x.locOpenParen); 1652 1653 trSynchronizedBody(mu, x.stmt, x.locOpenParen, decl); 1654 return; 1655 } 1656 1657 1658 case TagConstants.EVALSTMT: 1659 { 1660 EvalStmt x = (EvalStmt)stmt; 1661 ptrExpr(x.expr); 1662 return; 1663 } 1664 1665 case TagConstants.LABELSTMT: 1666 { 1667 LabelStmt x = (LabelStmt)stmt; 1668 code.push(); // this mark popped by "opBlockCmd" 1669 trStmt(x.stmt,decl); 1670 code.addElement(opBlockCmd(breakLabel(x.stmt))); 1671 return; 1672 } 1673 1674 case TagConstants.SKIPSTMT: 1675 return; 1676 1677 case TagConstants.TRYFINALLYSTMT: 1678 { 1679 TryFinallyStmt x = (TryFinallyStmt)stmt; 1680 int xStart = x.getStartLoc(); 1681 int xEnd = x.getEndLoc(); 1682 GuardedCmd temp; 1683 1684 code.push(); 1685 trStmt(x.tryClause,decl); 1686 GuardedCmd c0 = GC.seq(GuardedCmdVec.popFromStackVector(code)); 1687 1688 code.push(); 1689 VariableAccess ecSave = adorn(GC.ecvar); 1690 VariableAccess resultSave = adorn(GC.resultvar); 1691 VariableAccess xresultSave = adorn(GC.xresultvar); 1692 1693 if (Main.options().traceInfo > 0) { 1694 // add a label to track that the finally clause is entered because 1695 // an exception was raised 1696 GuardedCmd g = traceInfoLabelCmd(x, "FinallyBegin", x.locFinally); 1697 code.addElement(g); 1698 } 1699 code.addElement(GC.assume(GC.nary(xStart,xEnd, 1700 TagConstants.ANYEQ, 1701 GC.ecvar, ecSave))); 1702 code.addElement(GC.assume(GC.nary(xStart,xEnd, 1703 TagConstants.REFEQ, 1704 GC.resultvar, resultSave))); 1705 code.addElement(GC.assume(GC.nary(xStart,xEnd, 1706 TagConstants.REFEQ, 1707 GC.xresultvar, xresultSave))); 1708 1709 code.push(); 1710 trStmt(x.finallyClause,decl); 1711 temp = DynInstCmd.make(UniqName.locToSuffix(x.getStartLoc()) + "#n", 1712 GC.seq(GuardedCmdVec.popFromStackVector(code))); 1713 code.addElement(temp); 1714 1715 code.addElement(GC.gets(GC.ecvar, ecSave)); 1716 code.addElement(GC.gets(GC.resultvar, resultSave)); 1717 code.addElement(GC.gets(GC.xresultvar, xresultSave)); 1718 if (Main.options().traceInfo > 0) { 1719 // add a label to track that the finally clause is exited when it 1720 // was entered due to that an exception was raised 1721 GuardedCmd g = traceInfoLabelCmd(x, "FinallyEnd", x.getEndLoc()); 1722 code.addElement(g); 1723 } 1724 code.addElement(GC.raise()); 1725 1726 GuardedCmd c1 = GC.seq(GuardedCmdVec.popFromStackVector(code)); 1727 1728 code.addElement(GC.trycmd(c0,c1)); 1729 1730 code.push(); 1731 trStmt(x.finallyClause,decl); 1732 temp = DynInstCmd.make(UniqName.locToSuffix(x.getStartLoc()) + "#x", 1733 GC.seq(GuardedCmdVec.popFromStackVector(code))); 1734 code.addElement(temp); 1735 1736 return; 1737 } 1738 1739 case TagConstants.TRYCATCHSTMT: 1740 { 1741 TryCatchStmt x = (TryCatchStmt)stmt; 1742 int xStart = x.getStartLoc(); 1743 int xEnd = x.getEndLoc(); 1744 1745 code.push(); 1746 trStmt(x.tryClause,decl); 1747 GuardedCmd tryGC = GC.seq(GuardedCmdVec.popFromStackVector(code)); 1748 1749 GuardedCmd els = GC.raise(); 1750 1751 for(int i=x.catchClauses.size()-1; i>=0; i--) { 1752 CatchClause cc = (CatchClause)x.catchClauses.elementAt(i); 1753 int ccStart=cc.getStartLoc(); 1754 int ccEnd=cc.getEndLoc(); 1755 1756 // tst is typeof(XRES) <: Ti 1757 Expr tst = GC.nary(ccStart,ccEnd, 1758 TagConstants.TYPELE, 1759 GC.nary(ccStart,ccEnd, 1760 TagConstants.TYPEOF, 1761 GC.xresultvar), 1762 TypeExpr.make(ccStart,ccEnd, 1763 cc.arg.type)); 1764 1765 if( i==0 ) { 1766 // extend tst with a disjunct XRES==null 1767 tst = GC.or(ccStart,ccEnd, 1768 tst, 1769 GC.nary(ccStart,ccEnd, 1770 TagConstants.REFEQ, 1771 GC.xresultvar, 1772 GC.nulllit)); 1773 } 1774 1775 1776 code.push(); 1777 declaredLocals.addElement(cc.arg); 1778 VariableAccess arg = VariableAccess.make( cc.arg.id, ccStart, 1779 cc.arg ); 1780 1781 code.addElement(GC.assume(GC.nary(ccStart,ccEnd, 1782 TagConstants.ANYEQ, 1783 arg, 1784 GC.xresultvar))); 1785 trStmt(cc.body,decl); 1786 GuardedCmd thn = GC.seq(GuardedCmdVec.popFromStackVector(code)); 1787 1788 els = GC.ifcmd(tst, thn, els); 1789 } 1790 1791 1792 GuardedCmd handler = 1793 GC.ifcmd( GC.nary(xStart,xEnd, 1794 TagConstants.ANYNE, 1795 GC.ecvar, 1796 GC.ec_throw), 1797 GC.raise(), 1798 els ); 1799 1800 code.addElement(GC.trycmd(tryGC,handler)); 1801 1802 return; 1803 } 1804 1805 case TagConstants.VARDECLSTMT: 1806 { 1807 LocalVarDecl vd = ((VarDeclStmt)stmt).decl; 1808 declaredLocals.addElement(vd); 1809 boolean isUninitialized = false; 1810 boolean isGhost = false; 1811 if (vd.pmodifiers != null) { 1812 isGhost = Utils.findModifierPragma(vd.pmodifiers,TagConstants.GHOST) != null; 1813 for (int i= 0; i < vd.pmodifiers.size(); i++) { 1814 ModifierPragma prag= vd.pmodifiers.elementAt(i); 1815 if (prag.getTag() == TagConstants.UNINITIALIZED) { 1816 VariableAccess init = initadorn(vd); 1817 declaredLocals.addElement(init.decl); 1818 setInitVar(vd, init); 1819 isUninitialized = true; 1820 break; // don't look for any further UNINITIALIZED modifiers 1821 } 1822 } 1823 } 1824 1825 if (null != vd.init) { 1826 Assert.notFalse(vd.locAssignOp != Location.NULL); 1827 VariableAccess lhs = TrAnExpr.makeVarAccess(vd, vd.getStartLoc()); 1828 TrAnExpr.initForClause(); 1829 Expr rval = isGhost ? 1830 TrAnExpr.trSpecExpr((Expr)vd.init,null,premapWithArgs) : 1831 ptrExpr(vd.init); 1832 if (TrAnExpr.extraSpecs) addNewAssumptions(); 1833 if (! isUninitialized) { 1834 writeCheck(lhs, vd.init, rval, vd.locAssignOp, false); 1835 } 1836 code.addElement(GC.gets(lhs, rval)); 1837 } 1838 return; 1839 } 1840 1841 case TagConstants.CONSTRUCTORINVOCATION: 1842 //@ unreachable; 1843 // If the following assert breaks, there's something wrong in 1844 // "trBody" where the constructor call is split up from the rest of 1845 // the constructor body. 1846 Assert.fail("constructor invocation handled in TrConstructorCallStmt"); 1847 return; 1848 1849 case TagConstants.UNREACHABLE: 1850 addCheck(stmt, TagConstants.CHKCODEREACHABILITY, GC.falselit); 1851 return; 1852 1853 case TagConstants.SETSTMTPRAGMA: { 1854 SetStmtPragma s = (SetStmtPragma)stmt; 1855 1856 if (s.target instanceof FieldAccess) { 1857 FieldAccess fa = (FieldAccess)s.target; 1858 TrAnExpr.initForClause(); 1859 Expr lhs= trFieldAccess(true, fa); // FIXME - premap? 1860 Expr rval = TrAnExpr.trSpecExpr(s.value,null,premapWithArgs); 1861 if (TrAnExpr.extraSpecs) addNewAssumptions(); 1862 // Add check that the lhs is allowed to be written (writable pragma) 1863 writeCheck(lhs, s.value, rval, s.locOp, false); 1864 // Add checks that the lhs is allowed to be assigned (assignable pragma) 1865 frameHandler.modifiesCheckField(lhs,fa.getStartLoc(),fa.decl); 1866 String name; 1867 if (lhs.getTag() == TagConstants.VARIABLEACCESS) { 1868 VariableAccess valhs = (VariableAccess)lhs; 1869 name = valhs.decl.id.toString(); 1870 code.addElement(GC.gets(valhs, rval)); 1871 if (Modifiers.isStatic(valhs.decl.modifiers)) { 1872 code.addElement(modify(GC.statevar,s.getStartLoc())); 1873 } 1874 } else { 1875 // Instance field 1876 NaryExpr target = (NaryExpr)lhs; 1877 VariableAccess field = (VariableAccess)target.exprs.elementAt(0); 1878 name = field.decl.id.toString(); 1879 Expr obj = target.exprs.elementAt(1); 1880 code.addElement(GC.subgets(field, obj,rval)); 1881 code.addElement(modify(GC.statevar,s.getStartLoc())); 1882 } 1883 return; 1884 /* 1885 This was originally here. The if block just above was inserted to 1886 make the correspondence with assignment complete. 1887 Not sure if the protect expressions belong ??? FIXME 1888 1889 VariableAccess field = VariableAccess.make(fa.id, fa.locId, fa.decl); 1890 if (Modifiers.isStatic(fa.decl.modifiers)) { 1891 code.addElement(GC.gets( field, 1892 TrAnExpr.trSpecExpr(s.value))); 1893 } else { 1894 Expr obj = ((ExprObjectDesignator)fa.od).expr; 1895 code.addElement(GC.subgets( field, 1896 TrAnExpr.trSpecExpr(obj), 1897 TrAnExpr.trSpecExpr(s.value) )); 1898 } 1899 */ 1900 1901 } else if (s.target instanceof VariableAccess) { 1902 // Assignments to local ghost variables end here 1903 VariableAccess lhs = (VariableAccess)s.target; 1904 TrAnExpr.initForClause(); 1905 Expr rval = TrAnExpr.trSpecExpr(s.value,null,premapWithArgs); 1906 if (TrAnExpr.extraSpecs) addNewAssumptions(); 1907 writeCheck(lhs, s.value, rval, s.locOp, false); 1908 code.addElement(GC.gets(lhs,rval)); 1909 // A local variable is not part of an assignable frame so there is no 1910 // assignable clause to check 1911 VariableAccess init = getInitVar(lhs.decl); 1912 if (init != null) 1913 code.addElement(GC.gets(init, GC.truelit)); 1914 return; 1915 } else if (s.target instanceof ArrayRefExpr) { 1916 ArrayRefExpr lhs= (ArrayRefExpr)s.target; 1917 1918 TrAnExpr.initForClause(); 1919 Expr array= TrAnExpr.trSpecExpr(lhs.array,null,premapWithArgs); 1920 Expr index= TrAnExpr.trSpecExpr(lhs.index,null,premapWithArgs); 1921 Expr rval= TrAnExpr.trSpecExpr(s.value,null,premapWithArgs); 1922 if (TrAnExpr.extraSpecs) addNewAssumptions(); 1923 // Add a check that the value of the array index is in bounds 1924 arrayAccessCheck(lhs.array, array, lhs.index, index, lhs.locOpenBracket); 1925 // Add a check that the assignment to an array element is allowed 1926 // by the assignable clauses 1927 frameHandler.modifiesCheckArray(array,index,lhs.getStartLoc()); 1928 if (! isFinal(TypeCheck.inst.getType(lhs.array))) { 1929 addCheck(s.loc, 1930 TagConstants.CHKARRAYSTORE, 1931 GC.nary(TagConstants.IS, rval, 1932 GC.nary(TagConstants.ELEMTYPE, 1933 GC.nary(TagConstants.TYPEOF, array))), 1934 Location.NULL, lhs.array); 1935 } 1936 1937 code.addElement(GC.subsubgets(GC.elemsvar, array, index, rval)); 1938 code.addElement(modify(GC.statevar,lhs.getStartLoc())); 1939 Expr a= GC.select(GC.elemsvar, array); 1940 return; 1941 1942 } else { 1943 1944 ErrorSet.fatal(s.getStartLoc(), 1945 "Unknown construct to translate"); 1946 } 1947 break; 1948 } 1949 1950 case TagConstants.HENCE_BY: 1951 // FIXME - ignored - unclear semantics 1952 return; 1953 1954 case TagConstants.ASSUME: 1955 { 1956 ExprStmtPragma x = (ExprStmtPragma)stmt; 1957 TrAnExpr.initForClause(); 1958 Expr p = TrAnExpr.trSpecExpr(x.expr,null,premapWithArgs); 1959 if (TrAnExpr.extraSpecs) addNewAssumptionsNow(); 1960 code.addElement(GC.assume(p)); 1961 return; 1962 } 1963 1964 case TagConstants.ASSERT: { 1965 ExprStmtPragma x = (ExprStmtPragma)stmt; 1966 TrAnExpr.initForClause(); 1967 Expr p = TrAnExpr.trSpecExpr(x.expr,null,premapWithArgs); 1968 if (TrAnExpr.extraSpecs) addNewAssumptionsNow(); 1969 code.addElement(GC.check(x.getStartLoc(), TagConstants.CHKASSERT, 1970 p, Location.NULL)); 1971 return; 1972 } 1973 1974 case TagConstants.LOOP_INVARIANT: 1975 case TagConstants.MAINTAINING: 1976 { 1977 ExprStmtPragma x = (ExprStmtPragma)stmt; 1978 loopinvariants.addElement(x); 1979 return; 1980 } 1981 1982 case TagConstants.DECREASES: 1983 case TagConstants.DECREASING: 1984 { 1985 ExprStmtPragma x = (ExprStmtPragma)stmt; 1986 loopDecreases.addElement(x); 1987 return; 1988 } 1989 1990 case TagConstants.LOOP_PREDICATE: 1991 { 1992 ExprStmtPragma x = (ExprStmtPragma)stmt; 1993 loopPredicates.addElement(x); 1994 return; 1995 } 1996 1997 case TagConstants.SKOLEMCONSTANTPRAGMA: 1998 { 1999 SkolemConstantPragma p = (SkolemConstantPragma)stmt; 2000 skolemConstants.append(p.decls); 2001 break; 2002 } 2003 2004 case TagConstants.CLASSDECLSTMT: 2005 if (this.issueCautions && !escjava.Main.options().noNotCheckedWarnings) { 2006 ErrorSet.caution(stmt.getStartLoc(), 2007 "Not checking block-level types"); 2008 } 2009 return; 2010 2011 case TagConstants.ASSERTSTMT: { 2012 // Only process if we are supposed to be parsing Java 2013 // 1.4 or later and assertions are enabled. 2014 AssertStmt assertStmt = (AssertStmt)stmt; 2015 if (!Tool.options.assertIsKeyword || !Tool.options.assertionsEnabled) { 2016 // continue - simply skip the assertions 2017 } else if (Main.options().assertionMode == 2018 Options.JML_ASSERTIONS) { 2019 // Treat a Java assert as a JML assert 2020 // Since it is a Java statement, it can't contain JML constructs 2021 // FIXME - so should it be translated this way? 2022 Expr predicate = TrAnExpr.trSpecExpr(assertStmt.pred); 2023 code.addElement(GC.check(assertStmt.getStartLoc(), TagConstants.CHKASSERT, 2024 predicate, Location.NULL)); 2025 } else if (Main.options().assertionMode == 2026 Options.JAVA_ASSERTIONS) { 2027 // Treat a Java assert as a (conditional) throw 2028 trIfStmt(assertStmt.ifStmt.expr, assertStmt.ifStmt.thn, assertStmt.ifStmt.els,decl); 2029 } 2030 return; 2031 } 2032 default: 2033 //@ unreachable; 2034 Assert.notFalse(false,"Unexpected tag " + TagConstants.toString(tag) 2035 + " " + stmt + " " + 2036 Location.toString(stmt.getStartLoc())); 2037 return; 2038 } 2039 } 2040 2041 /** 2042 * Translate an "if" statement. 2043 * 2044 * @design This method was refactored out to handle Java's "assert" keyword as 2045 * well as normal "if" statements. 2046 */ 2047 private void trIfStmt(Expr guard, Stmt thenStmt, Stmt elseStmt, TypeDecl decl) { 2048 Expr guardExpr = ptrExpr(guard); 2049 2050 code.push(); 2051 if (Main.options().traceInfo > 0) { 2052 // add a label to track the if branch taken 2053 GuardedCmd g = traceInfoLabelCmd(thenStmt, "Then"); 2054 code.addElement(g); 2055 } 2056 trStmt(thenStmt,decl); 2057 GuardedCmd thenGuardedCmd = GC.seq(GuardedCmdVec.popFromStackVector(code)); 2058 2059 code.push(); 2060 if (Main.options().traceInfo > 0) { 2061 // add a label to track the if branch taken 2062 GuardedCmd g = traceInfoLabelCmd(elseStmt, "Else"); 2063 code.addElement(g); 2064 } 2065 trStmt(elseStmt,decl); 2066 GuardedCmd elseGuardedCmd = GC.seq(GuardedCmdVec.popFromStackVector(code)); 2067 2068 code.addElement(GC.ifcmd(guardExpr, thenGuardedCmd, elseGuardedCmd)); 2069 return; 2070 } 2071 2072 //@ requires loc != Location.NULL; 2073 private void trSynchronizedBody(/*@ non_null */ Expr mu, 2074 /*@ non_null */ Stmt stmt, int loc, TypeDecl decl) { 2075 // check LockingOrderViolation: mutexLE(max(LS),mu) || LS[mu] 2076 addCheck(loc, 2077 TagConstants.CHKLOCKINGORDER, 2078 GC.or(GC.nary(TagConstants.LOCKLE, 2079 GC.nary(TagConstants.MAX, GC.LSvar), 2080 mu), 2081 GC.nary(TagConstants.SELECT, GC.LSvar, mu))); 2082 2083 VariableAccess newLS = adorn(GC.LSvar); 2084 2085 // e1 is ( lockLE(max(LS),mu) && mu == max(newLS) ) 2086 Expr e1 = GC.and( 2087 // lockLE(max(LS),mu) 2088 GC.nary(TagConstants.LOCKLE, 2089 GC.nary(TagConstants.MAX, GC.LSvar), 2090 mu), 2091 // mu == max(newLS) 2092 GC.nary(TagConstants.REFEQ, 2093 mu, 2094 GC.nary(TagConstants.MAX, newLS))); 2095 2096 // e2 is ( LS[mu] && newLS == LS ) 2097 Expr e2 = GC.and( 2098 // LS[mu] 2099 GC.select(GC.LSvar, mu ), 2100 // newLS == LS 2101 GC.nary(TagConstants.REFEQ, newLS, GC.LSvar)); 2102 2103 // assume (e1 || e2) 2104 code.addElement(GC.assume(GC.or(e1, e2))); 2105 2106 // assume newLS == store(LS,mu,boolTrue) 2107 code.addElement(GC.assume(GC.nary(TagConstants.REFEQ, // or LOCKSETEQ? 2108 newLS, 2109 GC.nary(TagConstants.STORE, 2110 GC.LSvar, mu, GC.truelit)))); 2111 2112 // assume newLS == asLockSet(newLS) 2113 code.addElement(GC.assume(GC.nary(TagConstants.REFEQ, // or LOCKSETEQ? 2114 newLS, 2115 GC.nary(TagConstants.ASLOCKSET, 2116 newLS)))); 2117 2118 // Translate the body, using the new LS 2119 VariableAccess oldLS = GC.LSvar; 2120 GC.LSvar = newLS; 2121 trStmt(stmt,decl); 2122 GC.LSvar = oldLS; 2123 } 2124 2125 /** 2126 * This method implements "TrConstructorCallStmt" as described in section 6 of 2127 * ESCJ 16. 2128 */ 2129 private void trConstructorCallStmt(/*@ non_null */ ConstructorInvocation ci) { 2130 // Check if this is a constructor for an inner class; if so, we need to pass 2131 // an enclosing instance as the first argument. 2132 TypeSig resultType = TypeSig.getSig(ci.decl.parent); 2133 boolean inner = !resultType.isTopLevelType(); 2134 2135 // translate arguments 2136 int argsSize = ci.args.size() + (inner ? 1 : 0); 2137 ExprVec rawArgs = ci.args.copy(); 2138 ExprVec args = ExprVec.make(argsSize); 2139 2140 if (inner) { 2141 Expr rawExpr = ci.enclosingInstance; 2142 Assert.notNull(rawExpr); 2143 rawArgs.insertElementAt(rawExpr, 0); 2144 2145 Purity.decorate(rawExpr); 2146 Expr arg = trExpr(true, rawExpr); 2147 args.addElement(arg); 2148 2149 // do nullCheck here rather than non-null check in call(...): 2150 nullCheck(rawExpr, arg, ci.locDot); 2151 } 2152 for (int i = 0; i < ci.args.size(); i++) { 2153 Expr rawExpr = ci.args.elementAt(i); 2154 Purity.decorate(rawExpr); 2155 // protect all but the last argument 2156 Expr arg = trExpr(i != ci.args.size()-1, rawExpr); 2157 args.addElement(arg); 2158 } 2159 2160 InlineSettings is = (InlineSettings)inlineDecoration.get(ci); 2161 code.addElement(call(ci.decl, rawArgs, args, scope, 2162 ci.getStartLoc(), ci.getEndLoc(), 2163 ci.locOpenParen, true, is, null, false)); // FIXME - set the eod=null to the right value 2164 // this = RES 2165 code.addElement(GC.gets(GC.thisvar, GC.resultvar)); 2166 2167 // FIXME - this is for a 'this' or 'super' call within a constructor - need to put in modifies checks 2168 } 2169 2170 //// Expression translation 2171 2172 /** 2173 * Extends the code array with a command that evaluates e and returns an 2174 * expession which denotes this value in the poststate of that command. If 2175 * <code>protect</code> is true, then the expression returned will depend only on 2176 * values of temporary variables (that is, the expression returned will not be 2177 * affected by changes to program variables).<p> If <code>protect</code> is 2178 * <code>true</code>, then the value returned is certain to be of type 2179 * <code>VariableAccess</code>. 2180 */ 2181 //@ ensures protect ==> \result instanceof VariableAccess; 2182 private Expr protect(boolean protect, Expr e, int loc) { 2183 if (protect) { 2184 VariableAccess result = fresh(e, loc); 2185 code.addElement(GC.gets(result, e)); 2186 return result; 2187 } else return e; 2188 } 2189 2190 //@ ensures protect ==> \result instanceof VariableAccess; 2191 private Expr protect(boolean protect, Expr e, int loc, String suffix) { 2192 if (protect) { 2193 VariableAccess result = fresh(e, loc, suffix); 2194 code.addElement(GC.gets(result, e)); 2195 return result; 2196 } else return e; 2197 } 2198 2199 /** Purify and translate expr without protection */ 2200 private Expr ptrExpr(VarInit expr) { 2201 Purity.decorate(expr); 2202 return trExpr(false, expr); 2203 } 2204 2205 /** 2206 * Translate <code>expr</code> into a sequence of guarded commands that are 2207 * appended to <code>code</code> and return an expression denoting the value of 2208 * the expression. New temporaries may be generated; these are added to 2209 * <code>temporaries</code>. 2210 * 2211 * @param protect if true, then the expression return will depend only on values 2212 * of temporary variables (that is, the expression returned will not be affected 2213 * by changes in program variables). 2214 */ 2215 private Expr trExpr(boolean protect, /*@ non_null */ VarInit expr) { 2216 int tag = expr.getTag(); 2217 2218 switch (tag) { 2219 case TagConstants.ARRAYINIT: 2220 { 2221 ArrayInit x = (ArrayInit)expr; 2222 int xStart = x.getStartLoc(); 2223 int xEnd = x.getEndLoc(); 2224 2225 int len = x.elems.size(); 2226 boolean isPure[] = new boolean[len]; 2227 Expr[] elems = new Expr[len]; 2228 2229 // set isPure[i] to true if {E_{i+1},...,E_n} are all pure 2230 if( len != 0 ) isPure[len-1] = true; 2231 for(int i=len-2; i>=0; i-- ) { 2232 isPure[i] = isPure[i+1] && !Purity.impure(x.elems.elementAt(i+1)); 2233 } 2234 2235 for(int i=0; i<len; i++ ) 2236 elems[i] = trExpr(isPure[i], x.elems.elementAt(i)); 2237 2238 // Construct variables 2239 VariableAccess a = fresh(x, xStart, "arrayinit"); 2240 VariableAccess newallocvar = adorn(GC.allocvar); 2241 2242 // assume !isAllocated(a, alloc); 2243 code.addElement(GC.assume(GC.not(xStart, xEnd, 2244 GC.nary(xStart, xEnd, 2245 TagConstants.ISALLOCATED, 2246 a, GC.allocvar)))); 2247 // assume isAllocated(a, alloc'); 2248 code.addElement(GC.assume(GC.nary(xStart, xEnd, 2249 TagConstants.ISALLOCATED, 2250 a, 2251 newallocvar ))); 2252 // assume a != null; 2253 code.addElement(GC.assume(GC.nary(xStart, xEnd, 2254 TagConstants.REFNE, 2255 a, 2256 GC.nulllit ))); 2257 // assume typeof(a) == array(T); 2258 Expr typeofa = GC.nary(xStart, xEnd, 2259 TagConstants.TYPEOF, a); 2260 Expr arrayT = TypeExpr.make(xStart, xEnd, 2261 TypeCheck.inst.getType(x)); 2262 2263 code.addElement(GC.assume(GC.nary(xStart, xEnd, 2264 TagConstants.TYPEEQ, 2265 typeofa, arrayT ))); 2266 2267 // assume arrayLength(a) == n 2268 code.addElement(GC.assume(GC.nary(xStart, xEnd, 2269 TagConstants.INTEGRALEQ, 2270 GC.nary(xStart, xEnd, 2271 TagConstants.ARRAYLENGTH, 2272 a), 2273 LiteralExpr.make(TagConstants.INTLIT, 2274 new Integer(len), 2275 xStart)))); 2276 2277 // elems[a][i] = ei 2278 Expr elemsAta = GC.nary(xStart, xEnd, 2279 TagConstants.SELECT, 2280 GC.elemsvar, a); 2281 for(int i=0; i<len; i++ ) { 2282 Expr iLit = 2283 LiteralExpr.make(TagConstants.INTLIT, new Integer(i), xStart); 2284 Expr elemsAtaAti = GC.nary(xStart, xEnd, 2285 TagConstants.SELECT, 2286 elemsAta, iLit); 2287 code.addElement(GC.assume(GC.nary(xStart, xEnd, 2288 TagConstants.REFEQ, 2289 elemsAtaAti, elems[i] ))); 2290 } 2291 2292 // assume that everything allocated is an array 2293 code.addElement(GC.assume(predEvathangsAnArray(GC.allocvar, 2294 newallocvar))); 2295 // alloc = alloc' 2296 code.addElement(GC.gets(GC.allocvar, newallocvar)); 2297 2298 return a; 2299 } 2300 2301 case TagConstants.THISEXPR: { 2302 ThisExpr t = (ThisExpr)expr; 2303 if (t.classPrefix != null) 2304 return trExpr(protect, Inner.unfoldThis(t)); 2305 2306 // We ignore "protect" here, since "this" is (almost) never 2307 // assigned to. (In the one case where "this" is assigned-- 2308 // after the super-or-sibling constructor call in a 2309 // constructor--"protect" is not needed. 2310 return GC.thisvar; 2311 } 2312 2313 case TagConstants.SETCOMPEXPR: 2314 ErrorSet.fatal(expr.getStartLoc(), "Set comprehension is not supported"); 2315 2316 // Literals 2317 case TagConstants.BOOLEANLIT: 2318 case TagConstants.CHARLIT: 2319 case TagConstants.DOUBLELIT: 2320 case TagConstants.FLOATLIT: 2321 case TagConstants.INTLIT: 2322 case TagConstants.LONGLIT: 2323 case TagConstants.NULLLIT: 2324 return (Expr)expr; 2325 2326 case TagConstants.STRINGLIT: 2327 { 2328 String s = ((LiteralExpr)expr).value.toString(); 2329 Expr result = GC.nary( 2330 TagConstants.INTERN, 2331 GC.symlit(Strings.intern(s).toString()), 2332 GC.symlit(Integer.toString(s.length())) ); 2333 2334 return result; 2335 } 2336 2337 case TagConstants.ARRAYREFEXPR: 2338 { 2339 ArrayRefExpr x= (ArrayRefExpr)expr; 2340 Expr array= trExpr(Purity.impure(x.index), x.array); 2341 Expr index= trExpr(false, x.index); 2342 2343 arrayAccessCheck(x.array, array, x.index, index, x.locOpenBracket); 2344 2345 Expr a= GC.select(GC.elemsvar, array); 2346 return protect(protect, GC.select(a, index), x.locOpenBracket); 2347 } 2348 2349 case TagConstants.NEWINSTANCEEXPR: 2350 { 2351 NewInstanceExpr ni= (NewInstanceExpr)expr; 2352 2353 ExprVec rawArgs = ni.args.copy(); 2354 ExprVec args = ExprVec.make(ni.args.size()); 2355 2356 if (ni.anonDecl != null) { 2357 if (this.issueCautions && ! Main.options().noNotCheckedWarnings) { 2358 ErrorSet.caution(ni.anonDecl.loc, 2359 "Not checking body of anonymous class" + 2360 " (subclass of " + 2361 ni.type.name.printName() + ")"); 2362 } 2363 } 2364 2365 // translate enclosing instance argument if present: 2366 if (ni.enclosingInstance != null) { 2367 rawArgs.insertElementAt(ni.enclosingInstance, 0); 2368 Expr arg = trExpr(true, ni.enclosingInstance); 2369 args.addElement(arg); 2370 2371 // do nullCheck here rather than non-null check in call(...): 2372 nullCheck(ni.enclosingInstance, arg, ni.locDot); 2373 } 2374 2375 // translate normal arguments 2376 for (int i = 0; i < ni.args.size(); i++) { 2377 // protect all but the last argument 2378 Expr arg = trExpr(i != ni.args.size()-1, ni.args.elementAt(i)); 2379 args.addElement(arg); 2380 } 2381 2382 InlineSettings is = (InlineSettings)inlineDecoration.get(ni); 2383 code.addElement(call(ni.decl, rawArgs, args, scope, 2384 ni.loc, ni.getEndLoc(), ni.locOpenParen, 2385 false, is, temporary("RES", ni.loc, ni.loc), 2386 true)); 2387 2388 { Expr tType = TypeExpr.make(ni.loc, ni.getEndLoc(), ni.type); 2389 Expr resType = GC.nary(TagConstants.TYPEOF, GC.resultvar); 2390 if (ni.anonDecl != null) { 2391 // assume typeof(RES) != T (for anonymous new) 2392 code.addElement(GC.assume(GC.nary(TagConstants.TYPENE, 2393 resType, 2394 tType))); 2395 } else { 2396 // assume typeof(RES) == T (for ordinary new) 2397 code.addElement(GC.assume(GC.nary(TagConstants.TYPEEQ, 2398 resType, 2399 tType))); 2400 } 2401 } 2402 2403 ByteArrayOutputStream baos = new ByteArrayOutputStream(); 2404 PrettyPrint.write(baos, "new!"); 2405 PrettyPrint.inst.print(baos, ni.type); 2406 return protect(protect, GC.resultvar, ni.locOpenParen, baos.toString()); 2407 } 2408 2409 case TagConstants.NEWARRAYEXPR: 2410 { 2411 NewArrayExpr x= (NewArrayExpr)expr; 2412 int nd= x.dims.size(); 2413 2414 if (x.init != null) { 2415 return trExpr(true, x.init); 2416 } 2417 2418 // Construct variables 2419 ByteArrayOutputStream baos = new ByteArrayOutputStream(); 2420 PrettyPrint.write(baos, "new!"); 2421 PrettyPrint.inst.print(baos, x.type); 2422 for (int i = 0; i < nd; i++) { 2423 PrettyPrint.write(baos, "[]"); 2424 } 2425 VariableAccess result= fresh(x, x.loc, baos.toString()); 2426 VariableAccess newallocvar= adorn(GC.allocvar); 2427 2428 // Evaluate length in each dimension 2429 Expr[] dims= new Expr[nd]; 2430 for (int i= 0; i < nd; i++) { 2431 boolean protectDim= false; 2432 for (int j= i+1; j < nd && ! protectDim; j++) 2433 protectDim= Purity.impure(x.dims.elementAt(j)); 2434 dims[i]= trExpr(protectDim, x.dims.elementAt(i)); 2435 // "nd" squared iterations, but nd should be small 2436 } 2437 2438 // Check for negative array sizes 2439 for (int i= 0; i < nd; i++) { 2440 Expr nonneg= GC.nary(TagConstants.INTEGRALLE, GC.zerolit, dims[i]); 2441 Condition cond= GC.condition(TagConstants.CHKNEGATIVEARRAYSIZE, 2442 nonneg, Location.NULL); 2443 Expr je= x.dims.elementAt(i); 2444 code.addElement(GC.check(x.locOpenBrackets[i], cond, 2445 trim(x.dims.elementAt(i)))); 2446 } 2447 2448 // Construct call to arrayFresh 2449 Expr shape= GC.nary(TagConstants.ARRAYSHAPEONE, dims[nd-1]); 2450 Type type= ArrayType.make(x.type, Location.NULL); 2451 for (int i= nd-2; 0 <= i; i--) { 2452 shape= GC.nary(TagConstants.ARRAYSHAPEMORE, dims[i], shape); 2453 type= ArrayType.make(type, Location.NULL); 2454 } 2455 Expr[] arrayFreshArgs= { 2456 result, GC.allocvar, newallocvar, GC.elemsvar, shape, 2457 GC.typeExpr(type), GC.zeroequiv(x.type) 2458 }; 2459 Expr arrayFresh= GC.nary(x.getStartLoc(), x.getEndLoc(), 2460 TagConstants.ARRAYFRESH, 2461 ExprVec.make(arrayFreshArgs)); 2462 2463 // Emit the Assume and a Gets commands 2464 code.addElement(GC.assume(arrayFresh)); 2465 code.addElement(GC.assume(predEvathangsAnArray(GC.allocvar, 2466 newallocvar))); 2467 Expr ownerNull = predArrayOwnerNull(GC.allocvar, newallocvar, 2468 result); 2469 if (ownerNull != null) 2470 code.addElement(GC.assume(ownerNull)); 2471 code.addElement(GC.gets(GC.allocvar, newallocvar)); 2472 2473 // Return the variable containing the newly-allocated array 2474 return result; 2475 } 2476 2477 case TagConstants.CONDEXPR: 2478 { 2479 CondExpr x= (CondExpr)expr; 2480 // ifCmd((tr(x.test), tr(x.thn), tr(x.els)) 2481 Expr test= trExpr(false, x.test); 2482 VariableAccess result= fresh(x, x.locQuestion, "cond"); 2483 2484 code.push(); 2485 if (Main.options().traceInfo > 0) { 2486 // add a label to track the if branch taken 2487 GuardedCmd g = traceInfoLabelCmd(x.thn, "Then"); 2488 code.addElement(g); 2489 } 2490 Expr thnP= trExpr(false, x.thn); 2491 code.addElement(GC.gets(result, thnP)); 2492 GuardedCmd thenbody= GC.seq(GuardedCmdVec.popFromStackVector(code)); 2493 2494 code.push(); 2495 if (Main.options().traceInfo > 0) { 2496 // add a label to track the if branch taken 2497 GuardedCmd g = traceInfoLabelCmd(x.els, "Else"); 2498 code.addElement(g); 2499 } 2500 Expr elsP= trExpr(false, x.els); 2501 code.addElement(GC.gets(result, elsP)); 2502 GuardedCmd elsebody= GC.seq(GuardedCmdVec.popFromStackVector(code)); 2503 2504 code.addElement(GC.ifcmd(test, thenbody, elsebody)); 2505 return result; 2506 } 2507 2508 case TagConstants.INSTANCEOFEXPR: 2509 { 2510 InstanceOfExpr x= (InstanceOfExpr)expr; 2511 Expr obj = trExpr(protect, x.expr); 2512 2513 Expr isOfType = GC.nary(x.getStartLoc(), x.getEndLoc(), 2514 TagConstants.IS, obj, 2515 TypeExpr.make(x.type.getStartLoc(), 2516 x.type.getEndLoc(), 2517 x.type)); 2518 Expr notNull = GC.nary(x.getStartLoc(), x.getEndLoc(), 2519 TagConstants.REFNE, obj, GC.nulllit); 2520 2521 return GC.and(x.getStartLoc(), x.getEndLoc(), 2522 isOfType, 2523 notNull); 2524 } 2525 2526 case TagConstants.CASTEXPR: 2527 { 2528 CastExpr x= (CastExpr)expr; 2529 Expr result= trExpr(protect, x.expr); 2530 Expr te = GC.typeExpr(x.type); 2531 if (Types.isReferenceType(x.type)) { 2532 addCheck(expr, 2533 TagConstants.CHKCLASSCAST, 2534 GC.nary(TagConstants.IS, result, te)); 2535 } 2536 result = GC.nary(TagConstants.CAST, result, te); 2537 return result; 2538 } 2539 2540 case TagConstants.CLASSLITERAL: 2541 { 2542 ClassLiteral x= (ClassLiteral)expr; 2543 return GC.nary(x.getStartLoc(), x.getEndLoc(), 2544 TagConstants.CLASSLITERALFUNC, 2545 TypeExpr.make(x.type.getStartLoc(), 2546 x.type.getEndLoc(), 2547 x.type)); 2548 } 2549 2550 // Binary expressions 2551 case TagConstants.OR: case TagConstants.AND: 2552 { 2553 BinaryExpr x= (BinaryExpr)expr; 2554 VariableAccess result= fresh(x, x.locOp, 2555 (tag == TagConstants.OR ? 2556 "cor" : "cand")); 2557 Expr left= trExpr(false, x.left); 2558 2559 // Create a chunk of code that evaluates the right expr and 2560 // saves its value in "result" 2561 code.push(); 2562 Expr right= trExpr(false, x.right); 2563 code.addElement(GC.gets(result, right)); 2564 GuardedCmd rightbody= GC.seq(GuardedCmdVec.popFromStackVector(code)); 2565 2566 GuardedCmd thn, els; 2567 if (tag == TagConstants.OR) { 2568 thn= GC.gets(result, GC.truelit); 2569 els= rightbody; 2570 } else { 2571 thn= rightbody; 2572 els= GC.gets(result, GC.falselit); 2573 } 2574 if (Main.options().traceInfo > 0) { 2575 // add labels to track which operands are evaluated 2576 GuardedCmd g = traceInfoLabelCmd(x, "FirstOpOnly", x.locOp); 2577 if (tag == TagConstants.OR) { 2578 thn = GC.seq(g, thn); 2579 } 2580 else { 2581 els = GC.seq(g, els); 2582 } 2583 } 2584 code.addElement(GC.ifcmd(left, thn, els)); 2585 return result; 2586 } 2587 2588 case TagConstants.BITOR: case TagConstants.BITXOR: 2589 case TagConstants.BITAND: case TagConstants.NE: 2590 case TagConstants.EQ: case TagConstants.GE: 2591 case TagConstants.GT: case TagConstants.LE: 2592 case TagConstants.LT: case TagConstants.LSHIFT: 2593 case TagConstants.RSHIFT: case TagConstants.URSHIFT: 2594 case TagConstants.ADD: case TagConstants.SUB: 2595 case TagConstants.STAR: 2596 case TagConstants.DIV: case TagConstants.MOD: 2597 { 2598 BinaryExpr x= (BinaryExpr)expr; 2599 Expr left= trExpr(Purity.impure(x.right), x.left); 2600 Expr right= trExpr(false, x.right); 2601 if (tag == TagConstants.DIV || tag == TagConstants.MOD) { 2602 if (Types.isIntegralType(TypeCheck.inst.getType(x.right))) { 2603 addCheck(x.locOp, TagConstants.CHKARITHMETIC, 2604 GC.nary(TagConstants.INTEGRALNE, right, GC.zerolit)); 2605 } 2606 } 2607 int newtag= TrAnExpr.getGCTagForBinary(x); 2608 if (tag == TagConstants.GT || tag == TagConstants.GE || 2609 tag == TagConstants.LT || tag == TagConstants.LE) { 2610 // Must be primitive types 2611 int leftTag = ((PrimitiveType)TypeCheck.inst.getType(x.left)).getTag(); 2612 int rightTag = ((PrimitiveType)TypeCheck.inst.getType(x.right)).getTag(); 2613 if (leftTag == rightTag) 2614 ; // do nothing 2615 else if (leftTag == TagConstants.REALTYPE && rightTag != TagConstants.REALTYPE) 2616 right = GC.cast(right,Types.realType); 2617 else if (leftTag != TagConstants.REALTYPE && rightTag == TagConstants.REALTYPE) 2618 left = GC.cast(left,Types.realType); 2619 else if (leftTag == TagConstants.DOUBLETYPE && rightTag != TagConstants.DOUBLETYPE) 2620 right = GC.cast(right,Types.doubleType); 2621 else if (leftTag != TagConstants.DOUBLETYPE && rightTag == TagConstants.DOUBLETYPE) 2622 left = GC.cast(left,Types.doubleType); 2623 else if (leftTag == TagConstants.FLOATTYPE && rightTag != TagConstants.FLOATTYPE) 2624 right = GC.cast(right,Types.floatType); 2625 else if (leftTag != TagConstants.FLOATTYPE && rightTag == TagConstants.FLOATTYPE) 2626 left = GC.cast(left,Types.floatType); 2627 2628 // FIXME - other promotions ? Also in TrAnExpr.java 2629 2630 } 2631 if (newtag == TagConstants.STRINGCAT) { 2632 return addNewString(x,left,right); 2633 2634 } else { 2635 return protect(protect, GC.nary(x.getStartLoc(), x.getEndLoc(), 2636 newtag, left, right), 2637 x.locOp); 2638 } 2639 } 2640 2641 case TagConstants.ASSIGN: 2642 { 2643 BinaryExpr x= (BinaryExpr)expr; 2644 Expr right= x.right; 2645 Expr left= x.left; 2646 2647 int ltag = left.getTag(); 2648 if (ltag == TagConstants.VARIABLEACCESS) { 2649 VariableAccess lhs= (VariableAccess)left; 2650 Expr rval= trExpr(false, right); 2651 writeCheck(lhs, right, rval, x.locOp, false); 2652 code.addElement(GC.gets(lhs, rval)); 2653 VariableAccess init= getInitVar(lhs.decl); 2654 if (init != null) 2655 code.addElement(GC.gets(init, GC.truelit)); 2656 if (Modifiers.isStatic(lhs.decl.modifiers)) { 2657 code.addElement(modify(GC.statevar,x.getStartLoc())); 2658 } 2659 return protect(protect, left, x.locOp, lhs.decl.id.toString() + "="); 2660 2661 } else if (ltag == TagConstants.FIELDACCESS) { 2662 Expr lhs= trFieldAccess(true, (FieldAccess)left); 2663 Expr rval= trExpr(false, right); 2664 String name; 2665 writeCheck(lhs, right, rval, x.locOp, false); 2666 // Add a check that the lhs field may be assigned (assignable clause) 2667 frameHandler.modifiesCheckField(lhs,lhs.getStartLoc(), 2668 ((FieldAccess)left).decl); 2669 if (lhs.getTag() == TagConstants.VARIABLEACCESS) { 2670 VariableAccess vaLhs = (VariableAccess)lhs; 2671 name = vaLhs.decl.id.toString(); 2672 code.addElement(GC.gets(vaLhs, rval)); 2673 } else { 2674 NaryExpr target= (NaryExpr)lhs; 2675 VariableAccess field= (VariableAccess)target.exprs.elementAt(0); 2676 name = field.decl.id.toString(); 2677 Expr obj= target.exprs.elementAt(1); 2678 code.addElement(GC.subgets(field, obj, rval)); 2679 } 2680 code.addElement(modify(GC.statevar,x.locOp)); 2681 return protect(protect, lhs, x.locOp, name + "="); 2682 2683 } else if (ltag == TagConstants.ARRAYREFEXPR) { 2684 ArrayRefExpr lhs= (ArrayRefExpr)left; 2685 2686 Expr array= trExpr(true, lhs.array); 2687 Expr index= trExpr(true, lhs.index); 2688 Expr rval= trExpr(false, right); 2689 2690 arrayAccessCheck(lhs.array, array, lhs.index, index, lhs.locOpenBracket); 2691 // Add a check that the array[index] on the lhs is assignable 2692 frameHandler.modifiesCheckArray(array,index,lhs.getStartLoc()); 2693 if (! isFinal(TypeCheck.inst.getType(lhs.array))) { 2694 addCheck(x.locOp, 2695 TagConstants.CHKARRAYSTORE, 2696 GC.nary(TagConstants.IS, rval, 2697 GC.nary(TagConstants.ELEMTYPE, 2698 GC.nary(TagConstants.TYPEOF, array))), 2699 Location.NULL, lhs.array); 2700 } 2701 2702 code.addElement(GC.subsubgets(GC.elemsvar, array, index, rval)); 2703 code.addElement(modify(GC.statevar,x.locOp)); 2704 Expr a= GC.select(GC.elemsvar, array); 2705 return protect(protect, GC.select(a, index), x.locOp); 2706 2707 } else { 2708 Assert.fail("Unexpected tag " + TagConstants.toString(ltag) 2709 + " (" + ltag + ")"); 2710 } 2711 } 2712 2713 case TagConstants.INC: case TagConstants.DEC: 2714 case TagConstants.POSTFIXINC: case TagConstants.POSTFIXDEC: 2715 case TagConstants.ASGMUL: 2716 case TagConstants.ASGADD: case TagConstants.ASGSUB: 2717 case TagConstants.ASGLSHIFT: case TagConstants.ASGRSHIFT: 2718 case TagConstants.ASGURSHIFT: case TagConstants.ASGBITAND: 2719 case TagConstants.ASGBITOR: case TagConstants.ASGBITXOR: 2720 case TagConstants.ASGDIV: case TagConstants.ASGREM: 2721 { 2722 Expr right, left; 2723 int op; 2724 int locOp; 2725 Type rType; 2726 if (expr instanceof UnaryExpr) { 2727 UnaryExpr u= (UnaryExpr) expr; 2728 right= GC.onelit; 2729 rType = Types.intType; 2730 left= u.expr; 2731 op= TrAnExpr.getGCTagForUnary(u); 2732 locOp = u.locOp; 2733 } else { 2734 BinaryExpr x= (BinaryExpr)expr; 2735 right= x.right; 2736 rType = TypeCheck.inst.getType(right); 2737 left= x.left; 2738 op= TrAnExpr.getGCTagForBinary(x); 2739 locOp = x.locOp; 2740 } 2741 Type lType = TypeCheck.inst.getType(left); 2742 boolean returnold= (tag == TagConstants.POSTFIXINC 2743 || tag == TagConstants.POSTFIXDEC); 2744 2745 int ltag = left.getTag(); 2746 if (ltag == TagConstants.VARIABLEACCESS) { 2747 VariableAccess lhs= (VariableAccess)left; 2748 readCheck(lhs, lhs.getStartLoc()); 2749 2750 Expr oldLval= protect(Purity.impure(right) || returnold, lhs, 2751 locOp, "old!" + lhs.decl.id.toString()); 2752 Expr rval= trExpr(false, right); 2753 2754 if (tag == TagConstants.ASGDIV || tag == TagConstants.ASGREM) { 2755 Assert.notFalse(expr instanceof BinaryExpr); 2756 if (Types.isIntegralType(TypeCheck.inst.getType(right))) { 2757 addCheck(locOp, TagConstants.CHKARITHMETIC, 2758 GC.nary(TagConstants.INTEGRALNE, rval, GC.zerolit)); 2759 } 2760 } 2761 2762 if (op == TagConstants.STRINGCAT) { 2763 rval = addNewString(expr,left,rval); 2764 2765 } else { 2766 rval= GC.nary(expr.getStartLoc(), expr.getEndLoc(), op, oldLval, rval); 2767 rval= addRelAsgCast(rval, lType, rType); 2768 } 2769 2770 writeCheck(lhs, null, rval, locOp, false); 2771 code.addElement(GC.gets(lhs, rval)); 2772 if (returnold) { 2773 return oldLval; 2774 } else { 2775 return protect(protect, lhs, locOp, lhs.decl.id.toString() + "="); 2776 } 2777 2778 } else if (ltag == TagConstants.FIELDACCESS) { 2779 FieldAccess lhs = (FieldAccess)left; 2780 Expr lval= trFieldAccess(true, lhs); 2781 readCheck(lval, lhs.locId); 2782 // Add a check that the lhs is assignable 2783 frameHandler.modifiesCheckField(lval,lhs.getStartLoc(), 2784 ((FieldAccess)left).decl); 2785 2786 String name = lhs.decl.id.toString(); 2787 Expr oldLval = protect(Purity.impure(right) || returnold, lval, 2788 locOp, "old!" + name); 2789 Expr rval= trExpr(false, right); 2790 if (tag == TagConstants.ASGDIV || tag == TagConstants.ASGREM) { 2791 Assert.notFalse(expr instanceof BinaryExpr); 2792 if (Types.isIntegralType(TypeCheck.inst.getType(right))) { 2793 addCheck(locOp, TagConstants.CHKARITHMETIC, 2794 GC.nary(TagConstants.INTEGRALNE, rval, GC.zerolit)); 2795 } 2796 } 2797 2798 if (op == TagConstants.STRINGCAT) { 2799 rval = addNewString(expr,lval,rval); 2800 2801 } else { 2802 rval= GC.nary(expr.getStartLoc(), expr.getEndLoc(), 2803 op, oldLval, rval); 2804 rval= addRelAsgCast(rval, lType, rType); 2805 } 2806 2807 writeCheck(lval, null, rval, locOp, false); 2808 if (lval.getTag() == TagConstants.VARIABLEACCESS) { 2809 code.addElement(GC.gets((VariableAccess)lval, rval)); 2810 } else { 2811 NaryExpr target= (NaryExpr)lval; 2812 VariableAccess field= (VariableAccess)target.exprs.elementAt(0); 2813 Expr obj= target.exprs.elementAt(1); 2814 code.addElement(GC.subgets(field, obj, rval)); 2815 } 2816 code.addElement(modify(GC.statevar,locOp)); 2817 if (returnold) { 2818 return oldLval; 2819 } else { 2820 return protect(protect, lval, locOp, name + "="); 2821 } 2822 2823 } else if (ltag == TagConstants.ARRAYREFEXPR) { 2824 ArrayRefExpr lhs= (ArrayRefExpr)left; 2825 2826 Expr array= trExpr(true, lhs.array); 2827 Expr index= trExpr(true, lhs.index); 2828 arrayAccessCheck(lhs.array, array, lhs.index, index, lhs.locOpenBracket); 2829 // Add a check that the lhs is assignable 2830 frameHandler.modifiesCheckArray(array,index,lhs.getStartLoc()); 2831 Expr oldLval = protect(Purity.impure(right) || returnold, 2832 GC.select(GC.select(GC.elemsvar, array), 2833 index), 2834 locOp, "old"); 2835 2836 Expr rval= trExpr(false, right); 2837 if (tag == TagConstants.ASGDIV || tag == TagConstants.ASGREM) { 2838 Assert.notFalse(expr instanceof BinaryExpr); 2839 if (Types.isIntegralType(TypeCheck.inst.getType(right))) { 2840 addCheck(locOp, TagConstants.CHKARITHMETIC, 2841 GC.nary(TagConstants.INTEGRALNE, rval, GC.zerolit)); 2842 } 2843 } 2844 2845 rval= GC.nary(expr.getStartLoc(), expr.getEndLoc(), 2846 op, oldLval, rval); 2847 rval= addRelAsgCast(rval, lType, rType); 2848 2849 code.addElement(GC.subsubgets(GC.elemsvar, array, index, rval)); 2850 code.addElement(modify(GC.statevar,locOp)); 2851 if (returnold) { 2852 return oldLval; 2853 } else { 2854 Expr a= GC.select(GC.elemsvar, array); 2855 return protect(protect, GC.select(a, index), locOp); 2856 } 2857 2858 } else { 2859 Assert.fail("Unexpected tag " + TagConstants.toString(ltag) 2860 + " (" + ltag + ")"); 2861 } 2862 } 2863 2864 // Unary expressions 2865 case TagConstants.UNARYADD: 2866 { 2867 // drop UnaryADD 2868 UnaryExpr x= (UnaryExpr)expr; 2869 return trExpr(protect, x.expr); 2870 } 2871 2872 case TagConstants.UNARYSUB: 2873 case TagConstants.NOT: case TagConstants.BITNOT: 2874 { 2875 UnaryExpr x= (UnaryExpr)expr; 2876 Expr x2= trExpr(false, x.expr); 2877 int newtag= TrAnExpr.getGCTagForUnary(x); 2878 return protect(protect, GC.nary(x.getStartLoc(), x.getEndLoc(), 2879 newtag, x2), 2880 x.locOp); 2881 } 2882 2883 case TagConstants.PARENEXPR: 2884 { 2885 ParenExpr x= (ParenExpr)expr; 2886 return trExpr(protect, x.expr); 2887 } 2888 2889 case TagConstants.VARIABLEACCESS: 2890 { 2891 VariableAccess x= (VariableAccess)expr; 2892 readCheck(x, x.getStartLoc()); 2893 return protect(protect, x, x.getStartLoc(), x.decl.id.toString()); 2894 } 2895 2896 case TagConstants.FIELDACCESS: 2897 { 2898 FieldAccess fa = (FieldAccess)expr; 2899 Expr result = trFieldAccess(false, fa); 2900 if (fa.decl != Types.lengthFieldDecl) 2901 readCheck(result, fa.locId); 2902 return protect(protect, result, fa.locId, fa.decl.id.toString()); 2903 } 2904 2905 case TagConstants.METHODINVOCATION: 2906 { 2907 return trMethodInvocation(protect, (MethodInvocation)expr); 2908 } 2909 2910 default: 2911 //@ unreachable; 2912 Assert.fail("UnknownTag<" + TagConstants.toString(tag) + ">"); 2913 return null; 2914 } 2915 } 2916 2917 private static Expr addRelAsgCast(Expr rval, Type lType, Type rType) { 2918 if (!(lType instanceof PrimitiveType)) 2919 return rval; 2920 2921 switch (lType.getTag()) { 2922 case TagConstants.BYTETYPE: 2923 case TagConstants.SHORTTYPE: 2924 case TagConstants.CHARTYPE: 2925 break; // cast needed 2926 case TagConstants.INTTYPE: 2927 if (Types.isLongType(rType) || Types.isFloatingPointType(rType)) { 2928 break; // cast needed 2929 } else { 2930 return rval; 2931 } 2932 case TagConstants.LONGTYPE: 2933 if (Types.isFloatingPointType(rType)) { 2934 break; // cast needed 2935 } else { 2936 return rval; 2937 } 2938 case TagConstants.FLOATTYPE: 2939 case TagConstants.DOUBLETYPE: 2940 return rval; 2941 default: 2942 return rval; 2943 } 2944 return GC.nary(TagConstants.CAST, rval, GC.typeExpr(lType)); 2945 } 2946 2947 /** 2948 * Returns the guarded-command expression: 2949 * <pre> 2950 * (FORALL o :: !isAllocated(o, allocOld) && isAllocated(o, allocNew) 2951 * ==> isNewArray(o)) 2952 * </pre> 2953 */ 2954 private static Expr predEvathangsAnArray(VariableAccess allocOld, 2955 VariableAccess allocNew) { 2956 LocalVarDecl odecl = UniqName.newBoundVariable('o'); 2957 VariableAccess o = TrAnExpr.makeVarAccess(odecl, Location.NULL); 2958 2959 Expr e0 = GC.not(GC.nary(TagConstants.ISALLOCATED, o, allocOld)); 2960 Expr e1 = GC.nary(TagConstants.ISALLOCATED, o, allocNew); 2961 Expr e2 = GC.nary(TagConstants.ISNEWARRAY, o); 2962 2963 Expr body = GC.implies(GC.and(e0, e1), e2); 2964 2965 // TBW: "e2" should be the trigger of the following quantification 2966 return GC.forall(odecl, body); 2967 } 2968 2969 2970 /** 2971 * Returns the guarded-command expression: 2972 * <pre> 2973 * (FORALL o :: !isAllocated(o, allocOld) && isAllocated(o, allocNew) 2974 * ==> o.owner == null) 2975 * </pre> 2976 */ 2977 private static Expr predArrayOwnerNull(VariableAccess allocOld, 2978 VariableAccess allocNew, 2979 VariableAccess arr) { 2980 // get java.lang.Object 2981 TypeSig obj = Types.javaLangObject(); 2982 2983 FieldDecl owner = null; // make the compiler happy 2984 boolean notFound = false; 2985 try { 2986 owner = Types.lookupField(obj, Identifier.intern("owner"), 2987 obj); 2988 } 2989 catch (javafe.tc.LookupException e) { 2990 notFound = true; 2991 } 2992 // if we couldn't find the owner ghost field, there's nothing to do 2993 if (notFound) 2994 return null; 2995 2996 VariableAccess ownerVA = TrAnExpr.makeVarAccess(owner, Location.NULL); 2997 2998 LocalVarDecl odecl = UniqName.newBoundVariable('o'); 2999 VariableAccess o = TrAnExpr.makeVarAccess(odecl, Location.NULL); 3000 3001 Expr e0 = GC.not(GC.nary(TagConstants.ISALLOCATED, o, allocOld)); 3002 Expr e1 = GC.nary(TagConstants.ISALLOCATED, o, allocNew); 3003 Expr e2 = GC.nary(TagConstants.REFEQ, GC.select(ownerVA, arr), 3004 GC.nulllit); 3005 3006 3007 Expr body = GC.implies(GC.and(e0, e1), e2); 3008 3009 return GC.forall(odecl, body); 3010 } 3011 3012 // @todo Should be moved type javafe.tc.Types 3013 3014 /** 3015 * @return true if there can be no subtypes of <code>t</code>. 3016 * @design The definition of final used by this method is as follows. Reference 3017 * types are "final" if they have the <code>final</code> modifier. Array types 3018 * are "final" if their element types satisfy <code>isFinal</code>. Primitive 3019 * types are "final". 3020 */ 3021 public static boolean isFinal(/*@ non_null */ Type t) { 3022 int tag= t.getTag(); 3023 switch (tag) { 3024 case TagConstants.BOOLEANTYPE: 3025 case TagConstants.INTTYPE: 3026 case TagConstants.LONGTYPE: 3027 case TagConstants.CHARTYPE: 3028 case TagConstants.FLOATTYPE: 3029 case TagConstants.DOUBLETYPE: 3030 case TagConstants.BYTETYPE: 3031 case TagConstants.SHORTTYPE: 3032 return true; 3033 3034 case TagConstants.ARRAYTYPE: 3035 return isFinal(((ArrayType)t).elemType); 3036 3037 case TagConstants.TYPENAME: 3038 t= TypeCheck.inst.getSig((TypeName)t); 3039 case TagConstants.TYPESIG: 3040 TypeSig ts= (TypeSig)t; 3041 return Modifiers.isFinal(ts.getTypeDecl().modifiers); 3042 3043 default: 3044 //@ unreachable; 3045 Assert.fail("Unexpected tag " + TagConstants.toString(tag) + " (" 3046 + tag + ")"); 3047 return false; 3048 } 3049 } 3050 3051 //// Factor processing of FieldAccess nodes 3052 3053 /** 3054 * Returns either a <code>VariableAccess</code> if <code>fa</code> is a class 3055 * variable or a <code>SELECT</code> application if <code>fa</code> is an 3056 * instance variable access, or an <code>ARRAYLENGTH</code> application if 3057 * <code>fa</code> is the final array field <code>length</code>. In the second 3058 * case, will emit code for computing the object designator and also a check to 3059 * ensure that object is not null. 3060 */ 3061 private Expr trFieldAccess(boolean protectObject, 3062 /*@ non_null */ FieldAccess fa) { 3063 VariableAccess va; 3064 Iterator iter = modifyEverythingLocations.iterator(); 3065 if (iter.hasNext()) { 3066 va = TrAnExpr.makeVarAccess(fa.decl, fa.locId); 3067 EverythingLoc s = (EverythingLoc)iter.next(); 3068 s.add(va); 3069 3070 } else { 3071 va = TrAnExpr.makeVarAccess(fa.decl, fa.locId); 3072 } 3073 3074 int tag= fa.od.getTag(); 3075 if (Modifiers.isStatic(fa.decl.modifiers)) { 3076 // static field 3077 switch (tag) { 3078 case TagConstants.TYPEOBJECTDESIGNATOR: 3079 case TagConstants.SUPEROBJECTDESIGNATOR: 3080 break; 3081 case TagConstants.EXPROBJECTDESIGNATOR: { 3082 ExprObjectDesignator od= (ExprObjectDesignator)fa.od; 3083 Expr discardResult = trExpr(false, od.expr); 3084 break; 3085 } 3086 default: 3087 //@ unreachable; 3088 Assert.fail("Unexpected tag " + TagConstants.toString(tag) 3089 + " (" + tag + ")"); 3090 break; 3091 } 3092 return va; 3093 3094 } else { 3095 // instance variable 3096 Expr obj; 3097 switch (tag) { 3098 case TagConstants.EXPROBJECTDESIGNATOR: { 3099 ExprObjectDesignator od= (ExprObjectDesignator)fa.od; 3100 obj= trExpr(protectObject, od.expr); 3101 nullCheck(od.expr, obj, fa.od.locDot); 3102 break; 3103 } 3104 case TagConstants.SUPEROBJECTDESIGNATOR: 3105 obj= GC.thisvar; 3106 break; 3107 case TagConstants.TYPEOBJECTDESIGNATOR: 3108 // This case is not legal Java and should already have been 3109 // checked by the type checker 3110 //@ unreachable; 3111 Assert.fail("Unexpected tag"); 3112 obj= null; // dummy assignment 3113 break; 3114 default: 3115 //@ unreachable; 3116 Assert.fail("Unexpected tag " + TagConstants.toString(tag) 3117 + " (" + tag + ")"); 3118 obj= null; // dummy assignment 3119 break; 3120 } 3121 3122 Expr res; 3123 if (fa.decl == Types.lengthFieldDecl) { 3124 return GC.nary(fa.getStartLoc(), fa.getEndLoc(), 3125 TagConstants.ARRAYLENGTH, obj); 3126 } else { 3127 return GC.nary(fa.getStartLoc(), fa.getEndLoc(), 3128 TagConstants.SELECT, va, obj); 3129 } 3130 } 3131 } 3132 3133 /** 3134 * This translation of method invocation follows section 4.1 of ESCJ 16. 3135 */ 3136 private Expr trMethodInvocation(boolean protect, 3137 /*@ non_null */ MethodInvocation mi) { 3138 boolean isStatic = Modifiers.isStatic(mi.decl.modifiers); 3139 3140 // for holding the translated arguments 3141 ExprVec args = ExprVec.make(mi.args.size() + 1); 3142 ExprVec argsRaw = ExprVec.make(mi.args.size() + 1); 3143 Expr nullcheckArg = null; // Java expression 3144 /*-@ uninitialized */ int nullcheckLoc = Location.NULL; 3145 // FIXME /*@ readable nullcheckLoc if nullcheckArg != null; */ 3146 3147 Expr eod = null; 3148 int tag= mi.od.getTag(); 3149 switch (tag) { 3150 case TagConstants.TYPEOBJECTDESIGNATOR: { 3151 Assert.notFalse(isStatic); // non-static is not legal Java 3152 // the arguments are translated below 3153 break; 3154 } 3155 case TagConstants.EXPROBJECTDESIGNATOR: { 3156 ExprObjectDesignator od = (ExprObjectDesignator)mi.od; 3157 if (isStatic) { 3158 Expr discardResult = trExpr(false, od.expr); 3159 } else { 3160 // protect "self" if there are more arguments 3161 Expr self = trExpr(mi.args.size() != 0, od.expr); 3162 args.addElement(self); 3163 argsRaw.addElement(od.expr); 3164 nullcheckArg = od.expr; 3165 nullcheckLoc = od.locDot; 3166 eod = self; 3167 } 3168 // the (rest of) the arguments are translated below 3169 break; 3170 } 3171 case TagConstants.SUPEROBJECTDESIGNATOR: { 3172 if (! isStatic) { 3173 args.addElement(GC.thisvar); 3174 argsRaw.addElement(ThisExpr.make(null, mi.od.getStartLoc())); 3175 eod = GC.thisvar; 3176 } 3177 // the (rest of) the arguments are translated below 3178 break; 3179 } 3180 default: 3181 //@ unreachable; 3182 Assert.fail("Unexpected tag " + TagConstants.toString(tag) 3183 + " (" + tag + ")"); 3184 break; 3185 } 3186 3187 // translate remaining arguments 3188 for (int i = 0; i < mi.args.size(); i++) { 3189 // protect all but the last argument 3190 Expr argRaw = mi.args.elementAt(i); 3191 Expr arg = trExpr(i != mi.args.size()-1, argRaw); 3192 args.addElement(arg); 3193 argsRaw.addElement(argRaw); 3194 } 3195 3196 if (nullcheckArg != null) { 3197 nullCheck(nullcheckArg, args.elementAt(0), nullcheckLoc); 3198 } 3199 3200 InlineSettings is = (InlineSettings)inlineDecoration.get(mi); 3201 code.addElement( call( mi.decl, argsRaw, args, scope, mi.locId, 3202 mi.getEndLoc(), mi.locOpenParen, false, is, eod, false)); 3203 return protect(protect, GC.resultvar, mi.locOpenParen, 3204 mi.decl.id.toString()); 3205 } 3206 3207 3208 //// Helper methods for generating check assertions/assumptions 3209 3210 /** 3211 * Emit a check at location <code>loc</code> that guarded command expression 3212 * <code>e</code>, which was translated from the Java expression <code>E</code>, 3213 * is not <code>null</code>. If <code>E</code> denotes an expression that is 3214 * guaranteed not to be <code>null</code>, no check is emitted. 3215 */ 3216 private void nullCheck(/*@ non_null */ VarInit E, Expr e, int loc) { 3217 nullCheck(E, e, loc, TagConstants.CHKNULLPOINTER, Location.NULL); 3218 } 3219 3220 private void nullCheck(/*@ non_null */ VarInit E, Expr e, int loc, 3221 int errorName, int locPragma) { 3222 // start by peeling off parentheses and casts 3223 E = trim(E); 3224 3225 switch (E.getTag()) { 3226 case TagConstants.THISEXPR: 3227 return; 3228 3229 case TagConstants.VARIABLEACCESS: { 3230 GenericVarDecl d = ((VariableAccess)E).decl; 3231 SimpleModifierPragma nonNullPragma = GetSpec.NonNullPragma(d); 3232 if (nonNullPragma != null && !Main.options().guardedVC) { 3233 LabelInfoToString.recordAnnotationAssumption(nonNullPragma.getStartLoc()); 3234 return; 3235 } 3236 break; // perform check 3237 } 3238 3239 case TagConstants.FIELDACCESS: { 3240 FieldDecl fd = ((FieldAccess)E).decl; 3241 SimpleModifierPragma nonNullPragma = GetSpec.NonNullPragma(fd); 3242 if (nonNullPragma != null && !Main.options().guardedVC) { 3243 if (Modifiers.isStatic(fd.modifiers) || 3244 rdCurrent.getTag() != TagConstants.CONSTRUCTORDECL || 3245 rdCurrent.parent != fd.parent) { 3246 LabelInfoToString.recordAnnotationAssumption(nonNullPragma.getStartLoc()); 3247 return; 3248 } 3249 } 3250 break; // perform check 3251 } 3252 3253 default: 3254 break; // perform check 3255 } 3256 3257 Expr nullcheck = GC.nary(TagConstants.REFNE, e, GC.nulllit); 3258 addCheck(loc, errorName, nullcheck, locPragma, E); 3259 } 3260 3261 /** 3262 * Peels off parentheses and casts from <code>E</code> and returns the result 3263 */ 3264 private VarInit trim(/*@ non_null */ VarInit E) { 3265 while (true) { 3266 if (E.getTag() == TagConstants.PARENEXPR) { 3267 E = ((ParenExpr)E).expr; 3268 } else if (E.getTag() == TagConstants.CASTEXPR) { 3269 E = ((CastExpr)E).expr; 3270 } else { 3271 return E; 3272 } 3273 } 3274 } 3275 3276 /** 3277 * Emit the checks that <code>array</code> is non-null and that 3278 * <code>index</code> is inbounds for <code>array</code>. Implements the 3279 * ArrayAccessCheck function of ESCJ16. 3280 */ 3281 private void arrayAccessCheck(/*@ non_null */ Expr Array, /*@ non_null */ Expr array, 3282 /*@ non_null */ Expr Index, /*@ non_null */ Expr index, 3283 int locOpenBracket) { 3284 nullCheck(Array, array, locOpenBracket); 3285 3286 Expr length= GC.nary(TagConstants.ARRAYLENGTH, array); 3287 Expr indexNeg = GC.nary(TagConstants.INTEGRALLE, GC.zerolit, index); 3288 addCheck(locOpenBracket, TagConstants.CHKINDEXNEGATIVE, indexNeg, 3289 Location.NULL, trim(Index)); 3290 Expr indexTooBig = GC.nary(TagConstants.INTEGRALLT, index, length); 3291 addCheck(locOpenBracket, TagConstants.CHKINDEXTOOBIG, indexTooBig); 3292 } 3293 3294 /** 3295 * Used by <code>readCheck</code> and <code>writeCheck</code> to accumulate the 3296 * list of mutexes protecting a shared variable. Thus, these methods are not 3297 * thread re-entrant. 3298 */ 3299 private /*@ non_null */ ExprVec mutexList = ExprVec.make(5); 3300 private /*@ non_null */ ArrayList locList = new ArrayList(5); 3301 3302 /** 3303 * Insert checks done before reading variables. 3304 * 3305 * <p> This method implements ReadCheck as defined in ESCJ16. Handles reads of 3306 * local, class, and instance variables (ESCJ16 splits these into two ReadCheck 3307 * functions). </p> 3308 * 3309 * @param va is the variable being read; it must be either a 3310 * <code>VariableAccess</code> (in the case of local variables and class fields) 3311 * or a <code>SELECT</code> <code>NaryExpr</code> (in the case of instance 3312 * fields). 3313 * @param locId is the location of the variable or field being read. It is used 3314 * to determine the location of the "wrong" part of the check's label. 3315 */ 3316 private void readCheck(/*@ non_null */ Expr va, int locId) { 3317 Assert.notFalse(locId != Location.NULL); 3318 // "d" is the declaration of the variable being read 3319 GenericVarDecl d; 3320 Expr actualSelf = null; 3321 if (va.getTag() == TagConstants.SELECT) { 3322 NaryExpr sel= (NaryExpr)va; 3323 d= ((VariableAccess)sel.exprs.elementAt(0)).decl; 3324 actualSelf = sel.exprs.elementAt(1); 3325 } else { 3326 d= ((VariableAccess)va).decl; 3327 } 3328 3329 if (d.pmodifiers == null) return; 3330 3331 Hashtable map = null; 3332 3333 mutexList.removeAllElements(); 3334 locList.clear(); 3335 ModifierPragma firstMonitoredPragma = null; 3336 for (int i= 0; i < d.pmodifiers.size(); i++) { 3337 ModifierPragma prag= d.pmodifiers.elementAt(i); 3338 int tag= prag.getTag(); 3339 switch (tag) { 3340 case TagConstants.NON_NULL: 3341 case TagConstants.SPEC_PUBLIC: 3342 case TagConstants.SPEC_PROTECTED: 3343 case TagConstants.WRITABLE_IF: 3344 break; 3345 3346 case TagConstants.UNINITIALIZED: 3347 // "uninitialized" can be used only with local variables 3348 Assert.notFalse(va.getTag() != TagConstants.SELECT); 3349 VariableAccess init= getInitVar((LocalVarDecl) d); 3350 addCheck(locId, TagConstants.CHKINITIALIZATION, init, prag); 3351 break; 3352 3353 case TagConstants.READABLE_IF: 3354 map = initializeRWCheckSubstMap(map, actualSelf, locId); 3355 Expr dc = TrAnExpr.trSpecExpr(((ExprModifierPragma)prag).expr, map, null); 3356 addCheck(locId, TagConstants.CHKDEFINEDNESS, dc, prag); 3357 break; 3358 3359 case TagConstants.MONITORED_BY: { 3360 ExprModifierPragma emp = (ExprModifierPragma)prag; 3361 map = initializeRWCheckSubstMap(map, actualSelf, locId); 3362 mutexList.addElement(TrAnExpr.trSpecExpr(emp.expr, map, null)); 3363 locList.add(new Integer(emp.expr.getStartLoc())); 3364 if (firstMonitoredPragma == null) 3365 firstMonitoredPragma = prag; 3366 break; 3367 } 3368 3369 case TagConstants.MONITORED: 3370 Assert.notFalse(d instanceof FieldDecl); 3371 if (Modifiers.isStatic(d.modifiers)) { 3372 mutexList.addElement( 3373 GC.nary(TagConstants.CLASSLITERALFUNC, 3374 getClassObject(((FieldDecl)d).parent))); 3375 } else { 3376 mutexList.addElement(actualSelf); 3377 } 3378 locList.add(new Integer(prag.getStartLoc())); 3379 if (firstMonitoredPragma == null) 3380 firstMonitoredPragma = prag; 3381 break; 3382 3383 case TagConstants.INSTANCE: 3384 case TagConstants.IN: 3385 case TagConstants.MAPS: 3386 case TagConstants.GHOST: 3387 case TagConstants.MODEL: 3388 // ignore 3389 break; 3390 3391 default: 3392 Assert.fail("Unexpected tag \"" + TagConstants.toString(tag) 3393 + "\" (" + tag + ")"); 3394 } 3395 } 3396 3397 if (mutexList.size() != 0) { 3398 Expr onelocked= GC.falselit; 3399 for (int i= mutexList.size()-1; 0 <= i; i--) { 3400 Expr mu= mutexList.elementAt(i); 3401 onelocked= GC.or(GC.and(GC.nary(TagConstants.REFNE, mu, GC.nulllit), 3402 GC.nary(TagConstants.SELECT, GC.LSvar, mu)), 3403 onelocked); 3404 } 3405 if (rdCurrent instanceof ConstructorDecl && actualSelf != null) { 3406 // In constructors, always allow access to the fields of the object 3407 // being constructed. 3408 // Note: The following could be optimized so that if "actualSelf" 3409 // is ``obviously'' "this", then the check could be omitted altogether. 3410 onelocked = GC.or(GC.nary(TagConstants.REFEQ, actualSelf, GC.thisvar), 3411 onelocked); 3412 } 3413 // For a read race, we have a race condition if none of the 3414 // monitors are locked. Since we can't point to all of them 3415 // we point to the beginning of the first monitored declaration, 3416 // rather than to a specific expresssion - will likely be 3417 // confusing to the user anyway. 3418 addCheck(locId, TagConstants.CHKSHARING, onelocked, 3419 firstMonitoredPragma); 3420 } 3421 mutexList.removeAllElements(); // Help the garbage collector... 3422 locList.clear(); // Help the garbage collector... 3423 } 3424 3425 /** 3426 * Insert checks done before writing variables, as prescribed by WriteCheck in 3427 * ESCJ 16. Handles writes of local, class, and instance variables (ESCJ 16 3428 * splits these into two WriteCheck functions). 3429 * 3430 * @param va is the variable being written; it must be either a 3431 * <code>VariableAccess</code> (in the case of local variables and class fields) 3432 * or a <code>SELECT</code> <code>NaryExpr</code> (in the case of instance 3433 * fields). 3434 * @param rval is the guarded command expression being written into 3435 * <code>va</code>. The argument <code>Rval</code> is either the Java expression 3436 * from which <code>rval</code> was translated, or <code>null</code> if 3437 * <code>rval</code> was somehow synthesized. 3438 * @param locAssignOp is the location of the assignment operator that prescribes 3439 * the write. It is used to determine the location of the "wrong" part of the 3440 * check's label. 3441 * @param inInitializerContext indicates whether or not the expression whose 3442 * write check is to be performed is the initializing expression of a field. 3443 */ 3444 private void writeCheck(/*@ non_null */ Expr va, 3445 VarInit Rval, Expr rval, int locAssignOp, 3446 boolean inInitializerContext) { 3447 Assert.notFalse(locAssignOp != Location.NULL); 3448 // "d" is the declaration of the variable being written 3449 GenericVarDecl d; 3450 Expr actualSelf = null; 3451 if (va.getTag() == TagConstants.SELECT) { 3452 NaryExpr sel= (NaryExpr)va; 3453 d= ((VariableAccess)sel.exprs.elementAt(0)).decl; 3454 actualSelf = sel.exprs.elementAt(1); 3455 } else { 3456 d= ((VariableAccess)va).decl; 3457 } 3458 3459 // Handle non_null variables 3460 SimpleModifierPragma nonNullPragma = GetSpec.NonNullPragma(d); 3461 if (nonNullPragma != null) { 3462 if (Rval == null) { 3463 Expr nullcheck = GC.nary(TagConstants.REFNE, rval, GC.nulllit); 3464 addCheck(locAssignOp, TagConstants.CHKNONNULL, nullcheck, 3465 nonNullPragma.getStartLoc()); 3466 } else if (!Main.options().excuseNullInitializers || !inInitializerContext || 3467 trim(Rval).getTag() != TagConstants.NULLLIT) { 3468 nullCheck(Rval, rval, locAssignOp, TagConstants.CHKNONNULL, 3469 nonNullPragma.getStartLoc()); 3470 } 3471 } 3472 3473 if (d.pmodifiers == null) return; 3474 3475 Hashtable map = null; 3476 3477 mutexList.removeAllElements(); 3478 locList.clear(); 3479 Expr onenotnull= GC.falselit; 3480 ModifierPragma firstMonitoredPragma = null; 3481 for (int i= 0; i < d.pmodifiers.size(); i++) { 3482 ModifierPragma prag= d.pmodifiers.elementAt(i); 3483 int tag= prag.getTag(); 3484 switch (tag) { 3485 case TagConstants.IN: 3486 case TagConstants.MAPS: 3487 case TagConstants.INSTANCE: 3488 case TagConstants.UNINITIALIZED: 3489 case TagConstants.READABLE_IF: 3490 case TagConstants.SPEC_PUBLIC: 3491 case TagConstants.SPEC_PROTECTED: 3492 case TagConstants.GHOST: 3493 case TagConstants.NON_NULL: // handled above 3494 break; 3495 3496 case TagConstants.MODEL: 3497 ErrorSet.error(locAssignOp,"May not assign to a model variable"); 3498 break; 3499 3500 case TagConstants.WRITABLE_IF: 3501 map = initializeRWCheckSubstMap(map, actualSelf, locAssignOp); 3502 Expr dc = TrAnExpr.trSpecExpr(((ExprModifierPragma)prag).expr, map, null); 3503 addCheck(locAssignOp, TagConstants.CHKWRITABLE, dc, prag); 3504 break; 3505 3506 case TagConstants.MONITORED_BY: { 3507 ExprModifierPragma emp = (ExprModifierPragma)prag; 3508 map = initializeRWCheckSubstMap(map, actualSelf, locAssignOp); 3509 // We keep a list of locations in locList because the 3510 // translated expr (if it refers to this) may have a 3511 // dummy location and we want to be sure to have any 3512 // Race warning point to the actual object whose monitor 3513 // has not been acquired. 3514 mutexList.addElement(TrAnExpr.trSpecExpr(emp.expr, map, null)); 3515 locList.add(new Integer(emp.expr.getStartLoc())); 3516 if (firstMonitoredPragma == null) 3517 firstMonitoredPragma = prag; 3518 break; 3519 } 3520 3521 case TagConstants.MONITORED: 3522 Assert.notFalse(d instanceof FieldDecl); 3523 if (Modifiers.isStatic(d.modifiers)) { 3524 mutexList.addElement(GC.nary( 3525 TagConstants.CLASSLITERALFUNC, 3526 getClassObject(((FieldDecl)d).parent))); 3527 } else { 3528 mutexList.addElement(actualSelf); 3529 } 3530 locList.add(new Integer(prag.getStartLoc())); 3531 onenotnull= GC.truelit; 3532 if (firstMonitoredPragma == null) 3533 firstMonitoredPragma = prag; 3534 break; 3535 3536 default: 3537 Assert.fail("Unexpected tag \"" + TagConstants.toString(tag) 3538 + "\" (" + tag + ")"); 3539 } 3540 } 3541 3542 if (mutexList.size() != 0) { 3543 Expr allnullorlocked= GC.truelit; 3544 boolean doConst = rdCurrent instanceof ConstructorDecl && 3545 actualSelf != null; 3546 for (int i= mutexList.size()-1; 0 <= i; i--) { 3547 Expr mu= mutexList.elementAt(i); 3548 onenotnull= GC.or(GC.nary(TagConstants.REFNE, mu, GC.nulllit), 3549 onenotnull); 3550 Expr nullOrLocked = 3551 GC.or(GC.nary(TagConstants.REFEQ, mu, GC.nulllit), 3552 GC.select(GC.LSvar, mu)); 3553 if (!doConst) { 3554 int loc = mu.getStartLoc(); 3555 if (loc == Location.NULL) loc = ((Integer)locList.get(i)).intValue(); 3556 addCheck(locAssignOp, TagConstants.CHKSHARING, 3557 nullOrLocked,loc); 3558 } 3559 allnullorlocked= 3560 GC.and(nullOrLocked, allnullorlocked); 3561 } 3562 Expr p = GC.and(onenotnull, allnullorlocked); 3563 if (doConst) { 3564 // In constructors, always allow access to the fields of the object 3565 // being constructed. 3566 // Note: The following could be optimized so that if "actualSelf" 3567 // is ``obviously'' "this", then the check could be omitted altogether. 3568 p = GC.or(GC.nary(TagConstants.REFEQ, actualSelf, GC.thisvar), p); 3569 addCheck(locAssignOp, TagConstants.CHKSHARING, p, firstMonitoredPragma); 3570 } else { 3571 addCheck(locAssignOp, TagConstants.CHKSHARINGALLNULL, onenotnull, firstMonitoredPragma); 3572 } 3573 } 3574 mutexList.removeAllElements(); // Help the garbage collector... 3575 locList.clear(); // Help the garbage collector... 3576 } 3577 3578 /** 3579 * The following method is used in readCheck and writeCheck to lazily construct a 3580 * substitution map (which may also create another temporary variable). 3581 */ 3582 private Hashtable initializeRWCheckSubstMap(Hashtable prevMap, 3583 Expr actualSelf, 3584 int loc) { 3585 if (actualSelf == null) { 3586 // no map needed 3587 Assert.notFalse(prevMap == null); 3588 return null; 3589 } else if (prevMap != null) { 3590 return prevMap; 3591 } else { 3592 Hashtable map = new Hashtable(); 3593 VariableAccess vaSelf; 3594 if (actualSelf instanceof VariableAccess) { 3595 vaSelf = (VariableAccess)actualSelf; 3596 } else { 3597 vaSelf = (VariableAccess)protect(true, actualSelf, loc, "od"); 3598 } 3599 map.put(GC.thisvar.decl, vaSelf); 3600 return map; 3601 } 3602 } 3603 3604 /** 3605 * Calls <code>GC.check</code> to create a check and appends the result to 3606 * <code>code</code>. 3607 */ 3608 //@ modifies code.elementCount; 3609 private void addCheck(int locUse, Condition cond) { 3610 code.addElement(GC.check(locUse, cond)); 3611 } 3612 3613 /** 3614 * Calls <code>GC.check</code> to create a check and appends the result to 3615 * <code>code</code>. 3616 */ 3617 //@ modifies code.elementCount; 3618 void addCheck(int locUse, int errorName, Expr pred) { 3619 addCheck(locUse, errorName, pred, Location.NULL); 3620 } 3621 3622 /** 3623 * Calls <code>GC.check</code> to create a check and appends the result to 3624 * <code>code</code>. 3625 */ 3626 //@ modifies code.elementCount; 3627 private void addCheck(/*@ non_null */ ASTNode use, int errorName, Expr pred) { 3628 code.addElement(GC.check(use.getStartLoc(), 3629 errorName, pred, 3630 Location.NULL)); 3631 } 3632 3633 /** 3634 * Calls <code>GC.check</code> to create a check and appends the result to 3635 * <code>code</code>. 3636 */ 3637 //@ modifies code.elementCount; 3638 private void addCheck(int locUse, int errorName, Expr pred, int locPragmaDecl) { 3639 code.addElement(GC.check(locUse, errorName, pred, locPragmaDecl)); 3640 } 3641 3642 void addCheck(int locUse, int errorName, Expr pred, int locPragmaDecl, int auxLoc) { 3643 code.addElement(GC.check(locUse, errorName, pred, locPragmaDecl, auxLoc, null)); 3644 } 3645 3646 /** 3647 * Calls <code>GC.check</code> to create a check and appends the result to 3648 * <code>code</code>. 3649 */ 3650 //@ modifies code.elementCount; 3651 private void addCheck(int locUse, int errorName, Expr pred, int locPragmaDecl, 3652 Object aux) { 3653 code.addElement(GC.check(locUse, errorName, pred, locPragmaDecl, aux)); 3654 } 3655 3656 /** Calls <code>GC.check</code> to create a check and appends the 3657 result to <code>code</code>. */ 3658 3659 //@ modifies code.elementCount; 3660 private void addCheck(int locUse, int errorName, Expr pred, 3661 /*@ non_null */ ASTNode prag) { 3662 code.addElement(GC.check(locUse, errorName, pred, prag.getStartLoc())); 3663 } 3664 3665 private void addAssumption(Expr pred) { 3666 code.addElement(GC.assume(pred)); 3667 //code.addElement(GC.check(pred.getStartLoc(),TagConstants.CHKCONSISTENT, pred, 3668 // Location.NULL, null)); 3669 } 3670 3671 private void addAssumptions(ExprVec ev) { 3672 if (ev == null) return; 3673 for (int i=0; i<ev.size(); ++i) { 3674 addAssumption(ev.elementAt(i)); 3675 } 3676 } 3677 3678 private void addNewAssumptions() { 3679 addNewAssumptionsHelper(); 3680 axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded); 3681 TrAnExpr.closeForClause(); 3682 } 3683 ExprVec addNewAssumptionsNow() { 3684 addNewAssumptionsHelper(); 3685 if (TrAnExpr.trSpecAuxAxiomsNeeded != null) 3686 axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded); 3687 ExprVec ev = ExprVec.make(10); 3688 GetSpec.addAxioms(axsToAdd,ev); 3689 addNewAssumptionsNow(ev); 3690 TrAnExpr.closeForClause(); 3691 return ev; 3692 } 3693 private void addNewAssumptionsNow(ExprVec ev) { 3694 //addNewAssumptionsHelper(); 3695 for (int i=0; i<ev.size(); ++i) { 3696 addAssumption(ev.elementAt(i)); 3697 } 3698 } 3699 private void addNewAssumptionsHelper() { 3700 if (TrAnExpr.trSpecModelVarsUsed != null) { 3701 // These assignments with a null rhs are used to indicate 3702 // that the target has some unknown new value. 3703 Iterator ii = TrAnExpr.trSpecModelVarsUsed.values().iterator(); 3704 while (ii.hasNext()) { 3705 VariableAccess d = (VariableAccess)ii.next(); 3706 code.addElement(GC.gets(d,null)); // FIXME - what about array model vars, static model vars 3707 } 3708 } 3709 addAssumptions(TrAnExpr.trSpecExprAuxConditions); 3710 addAssumptions(TrAnExpr.trSpecExprAuxAssumptions); 3711 } 3712 /** 3713 * Return the <code>VariableAccesss</code> associated with <code>d</code> by a 3714 * call to <code>setInitVar</code>. If none has been associated with 3715 * <code>d</code>, returns <code>null</code>. 3716 */ 3717 private static VariableAccess getInitVar(GenericVarDecl d) { 3718 return (VariableAccess)Purity.translateDecoration.get(d); 3719 } 3720 3721 /** 3722 * Associates <code>init</code> with <code>d</code>; will be returned by a call 3723 * to <code>getInitVar</code>. 3724 */ 3725 private static void setInitVar(GenericVarDecl d, VariableAccess init) { 3726 Purity.translateDecoration.set(d, init); 3727 } 3728 3729 /** Modifies a GC designator. GC designator can include SubstExpr. */ 3730 3731 private GuardedCmd modify(/*@ non_null */ VariableAccess va, int loc) { 3732 VariableAccess newVal = temporary(va.id.toString(), loc, loc); 3733 return GC.gets(va, newVal); 3734 } 3735 3736 private GuardedCmd modify(/*@ non_null */ Expr e, Hashtable pt, int loc) { 3737 VariableAccess newVal = temporary("after@" + UniqName.locToSuffix(loc), 3738 e.getStartLoc(), e.getStartLoc()); 3739 3740 int etag = e.getTag(); 3741 if (etag == TagConstants.VARIABLEACCESS) { 3742 // "e" is a single variable 3743 return GC.gets( (VariableAccess)e, newVal ); 3744 } 3745 3746 Assert.notFalse(etag == TagConstants.SELECT); 3747 NaryExpr nary = (NaryExpr)e; 3748 e = nary.exprs.elementAt(0); 3749 Expr index = nary.exprs.elementAt(1); 3750 if (pt != null) { 3751 index = GC.subst(Location.NULL, Location.NULL, pt, index); 3752 } 3753 etag = e.getTag(); 3754 if (etag == TagConstants.VARIABLEACCESS) { 3755 // The given "e" had the form "f[index]" 3756 return GC.subgets((VariableAccess)e, index, newVal); 3757 } 3758 3759 // The given "e" had the form "elems[array][index]" 3760 //Assert.notFalse(etag == TagConstants.SELECT); 3761 //nary = (NaryExpr)e; 3762 //VariableAccess elems = (VariableAccess)nary.exprs.elementAt(0); 3763 //Expr array = nary.exprs.elementAt(1); 3764 //if (pt != null) { 3765 // array = GC.subst(Location.NULL, Location.NULL, pt, array); 3766 //} 3767 //return GC.subsubgets(elems, array, index, newVal); 3768 return null; 3769 } 3770 3771 3772 // the inlining depth at which to perform checking. 3773 public int inlineCheckDepth = 0; 3774 // the number of levels of inlining after the level that is checked. 3775 public int inlineDepthPastCheck = 0; 3776 3777 /** 3778 * Creates and desugars a call node, extended to allow the possibility of 3779 * inlining a call. 3780 */ 3781 private Call call(RoutineDecl rd, ExprVec argsRaw, ExprVec args, 3782 FindContributors scope, 3783 int scall, int ecall, int locOpenParen, 3784 boolean superOrSiblingConstructorCall, 3785 InlineSettings inline, Expr eod, boolean freshResult) { 3786 // save the current status of checking assertions 3787 boolean useGlobalStatus = NoWarn.useGlobalStatus; 3788 3789 // obtain the appropriate inlining flags 3790 inline = computeInlineSettings(rd, argsRaw, inline, scall); 3791 3792 // create call 3793 Call call = Call.make( args, scall, ecall, inline != null); 3794 call.rd = rd; 3795 3796 // now figure out desugared part 3797 3798 String description; 3799 Spec spec; 3800 if (inline != null) { 3801 if (inline.getSpecForInline) { 3802 //System.out.println("GETTING SPEC FOR INLINE"); 3803 spec = GetSpec.getSpecForInline(call.rd, scope); 3804 } else { 3805 Set synTargs = predictedSynTargs; 3806 if (synTargs == null) 3807 synTargs = new Set(); 3808 //System.out.println("GETTING SPEC FOR BODY"); 3809 spec = GetSpec.getSpecForBody(call.rd, scope, synTargs, null); 3810 } 3811 description = "inlined call"; 3812 } 3813 else { 3814 //System.out.println("GETTING SPEC FOR CALL " + Location.toString(call.rd.loc) ); 3815 spec = GetSpec.getSpecForCall( call.rd, scope, predictedSynTargs ); 3816 if (spec.modifiesEverything) { 3817 ErrorSet.caution(scall, 3818 "A method that 'modifies everything' has been called; the verification of a body with such a call is not correct."); 3819 } 3820 description = "call"; 3821 } 3822 call.spec = spec; 3823 3824 Assert.notFalse( spec.dmd.args.size() == call.args.size(), 3825 "formal args: " + spec.dmd.args.size() 3826 + " actualargs: " + call.args.size() ); 3827 3828 3829 // now start creating code and temporaries 3830 code.push(); // this mark popped by "spill" 3831 temporaries.push(); // this mark popped by "spill" 3832 3833 // create pt = { p* -> p*@L, wt*@pre -> wt*@L } 3834 3835 Vector ptDomain = new Vector(); 3836 for(int i=0; i<spec.dmd.args.size(); i++) 3837 ptDomain.addElement( spec.dmd.args.elementAt(i) ); 3838 3839 // spec.preVarMap gives the set of locations that are in modifies clauses for the 3840 // called routine 3841 for(Enumeration e = spec.preVarMap.elements(); e.hasMoreElements(); ) 3842 ptDomain.addElement( ((VariableAccess)e.nextElement()).decl ); 3843 Hashtable pt = GetSpec.makeSubst( ptDomain.elements(), 3844 UniqName.locToSuffix(call.scall) ); 3845 3846 /* if the dontCheckPreconditions flag is set, turn off the following 3847 checks for non_null parameters and preconditions */ 3848 if (inline != null) { 3849 globallyTurnOffChecks(inline.dontCheckPreconditions); 3850 } 3851 3852 // var p*@L = e* in 3853 Hashtable argsMap = new Hashtable(); 3854 VariableAccess[] piLs = new VariableAccess[ call.args.size() ]; 3855 for(int i=0; i<spec.dmd.args.size(); i++) { 3856 GenericVarDecl pi = spec.dmd.args.elementAt(i); 3857 piLs[i] = (VariableAccess)pt.get( pi ); 3858 temporaries.addElement( piLs[i].decl ); 3859 /* non_null pragmas are handled by desugaring now 3860 SimpleModifierPragma nonnull = null; // GetSpec.NonNullPragma(pi); 3861 if (nonnull != null && !pi.id.toString().equals("this$0arg")) { 3862 Expr argRaw = argsRaw.elementAt(i); 3863 nullCheck(argRaw, call.args.elementAt(i), 3864 argRaw.getStartLoc(), 3865 TagConstants.CHKNONNULL, nonnull.getStartLoc()); 3866 } 3867 */ 3868 argsMap.put(pi,piLs[i]); 3869 code.addElement(GC.gets(piLs[i], call.args.elementAt(i))); 3870 } 3871 3872 if (spec.dmd.isConstructor()) { 3873 code.addElement(GC.gets(GC.resultvar, eod)); 3874 } 3875 3876 for (int i=0; i<spec.preAssumptions.size(); ++i) { 3877 addAssumption(spec.preAssumptions.elementAt(i)); 3878 } 3879 3880 // check all preconditions 3881 for(int i=0; i<spec.pre.size(); i++) { 3882 Condition cond = spec.pre.elementAt(i); 3883 int label = cond.label; 3884 Expr p = cond.pred; 3885 if (cond.label == TagConstants.CHKPRECONDITION) { 3886 p = mapLocation(p,locOpenParen); 3887 label = TagConstants.CHKQUIET; 3888 } 3889 addCheck(locOpenParen, 3890 label, 3891 GC.subst( call.scall, call.ecall, pt, p ), 3892 cond.locPragmaDecl); 3893 } 3894 3895 // Add a check that all the locations that might be assigned by the callee 3896 // are allowed to be assigned by the caller 3897 DerivedMethodDecl calledSpecs = GetSpec.getCombinedMethodDecl(rd); 3898 frameHandler.modifiesCheckMethodI(calledSpecs.modifies, 3899 eod, locOpenParen, pt,freshResult, rd.parent); 3900 3901 if (inline != null && Main.options().traceInfo > 0) { 3902 // add a label to say that a routine is being called 3903 GuardedCmd g = traceInfoLabelCmd(call.scall, call.ecall, 3904 "Call", call.scall); 3905 code.addElement(g); 3906 } 3907 3908 3909 // var w*@L = w in 3910 for(Enumeration e = spec.preVarMap.keys(); e.hasMoreElements(); ) 3911 { 3912 GenericVarDecl w = (GenericVarDecl)e.nextElement(); 3913 VariableAccess wPre = (VariableAccess)spec.preVarMap.get(w); 3914 VariableAccess wL = (VariableAccess)pt.get( wPre.decl ); 3915 Assert.notNull( wL ); 3916 VariableAccess wAccess = VariableAccess.make( w.id, call.scall, w ); 3917 3918 temporaries.addElement( wL.decl ); 3919 code.addElement( GC.gets( wL, wAccess ) ); 3920 } 3921 3922 // restore original checking of warnings 3923 NoWarn.useGlobalStatus = useGlobalStatus; 3924 3925 3926 if (inline != null) { 3927 3928 // insert the translated body, with appropriate substitutions of 3929 // formals for the new names provided above 3930 Translate trInline = new Translate(); 3931 trInline.inlineCheckDepth = inline.nextInlineCheckDepth; 3932 trInline.inlineDepthPastCheck = inline.nextInlineDepthPastCheck; 3933 3934 // turn off body checks if the appropriate flag is set 3935 globallyTurnOffChecks(inline.dontCheckInlinedBody); 3936 3937 GuardedCmd body = trInline.trBody(rd, scope, null, predictedSynTargs, 3938 this, this.issueCautions); 3939 body = substituteGC(pt, body); 3940 code.addElement(body); 3941 3942 for (int i=0; i<spec.postAssumptions.size(); ++i) { 3943 addAssumption(spec.postAssumptions.elementAt(i)); 3944 } 3945 3946 // check all postconditions 3947 for(int i=0; i<spec.post.size(); i++) { 3948 Condition cond = spec.post.elementAt(i); 3949 if (cond.label == TagConstants.CHKUNEXPECTEDEXCEPTION2) continue; 3950 addCheck(rd.getEndLoc(), 3951 cond.label, 3952 GC.subst( call.scall, call.ecall, pt, cond.pred), 3953 cond.locPragmaDecl); 3954 } 3955 if (Main.options().traceInfo > 1) { 3956 // add a label to say that the inlined call has returned 3957 GuardedCmd g = traceInfoLabelCmd(call.scall, call.ecall, 3958 "CallReturn", call.scall); 3959 code.addElement(g); 3960 } 3961 // restore original checking of warnings 3962 NoWarn.useGlobalStatus = useGlobalStatus; 3963 } 3964 3965 else { 3966 Type savedType = GC.thisvar.decl.type; 3967 3968 // We need to evaluate all of the expressions in the 3969 // modifies clauses before we set the locations that are 3970 // in the modifies clauses to arbitrary values, since 3971 // some of the expressions might also be modified. 3972 // For example, a clause might be modifies i,a[i]; 3973 // We don't try to see what expressions are modified; 3974 // we simply translate all of them, assigning the results 3975 // to some temporary variables. Those temporary variables 3976 // are then used later. 3977 3978 // For each item in the modifies clauses we add 0 or more 3979 // items to the translations and locations lists. Later 3980 // we iterate over the modifies clauses again, in precisely 3981 // the same order - being sure to take off EXACTLY the same 3982 // items as we put on, for each kind of entry in the modifies 3983 // clause. 3984 /* System.out.println("ARGS " ); 3985 { java.util.Iterator im = argsMap.keySet().iterator(); 3986 while (im.hasNext()) { 3987 Object o = im.next(); 3988 System.out.println("ITEM " + o + " ::: " + argsMap.get(o)); 3989 } 3990 }*/ 3991 Expr thisTrans = eod; 3992 /* System.out.println("THISTRSANS"); 3993 if (thisTrans != null) EscPrettyPrint.inst.print(System.out,0,thisTrans); 3994 System.out.println("");*/ 3995 LinkedList translations = new LinkedList(); 3996 LinkedList locations = new LinkedList(); 3997 ModifiesGroupPragmaVec mgpv = calledSpecs.modifies; 3998 for (int i=0; i<mgpv.size(); ++i) { 3999 GC.thisvar.decl.type = TypeSig.getSig(calledSpecs.getContainingClass()); 4000 ModifiesGroupPragma mgp = mgpv.elementAt(i); 4001 Expr precondition = mgp.precondition; 4002 precondition = TrAnExpr.trSpecExpr(precondition,argsMap,argsMap,eod); 4003 codevec = GuardedCmdVec.make(); 4004 Frame.ModifiesIterator iter = new Frame.ModifiesIterator( 4005 rd.parent,mgp.items,true,true); 4006 while (iter.hasNext()) { 4007 Object o = iter.next(); 4008 if (o instanceof FieldAccess) { 4009 FieldAccess fa = (FieldAccess)o; 4010 //System.out.println("FIELD ACCESS " + fa + " " + Location.toString(fa.getStartLoc()) + " " + Location.toString(fa.decl.getStartLoc())); 4011 Expr b = TrAnExpr.trSpecExpr(fa,argsMap,argsMap,eod); 4012 if (b instanceof NaryExpr && ((NaryExpr)b).op == TagConstants.SELECT) { 4013 // instance fields 4014 NaryExpr n = (NaryExpr)b; 4015 translations.add(n.exprs.elementAt(0)); 4016 translations.add(cacheValue(n.exprs.elementAt(1))); 4017 locations.add(new Integer(fa.getStartLoc())); 4018 } else if (b instanceof VariableAccess) { 4019 // static fields 4020 translations.add(b); 4021 translations.add(null); 4022 locations.add(new Integer(fa.getStartLoc())); 4023 } else if (b instanceof NaryExpr && ((NaryExpr)b).op == TagConstants.METHODCALL) { 4024 // model variable - skip 4025 translations.add(null); 4026 } else { 4027 translations.add(null); 4028 // FIXME - turn into an internal error 4029 System.out.println("UNSPPORTRED-EB " + b.getClass() + " " + TagConstants.toString(((NaryExpr)b).op)); 4030 escjava.ast.EscPrettyPrint.inst.print(System.out,0,b); 4031 System.out.println(""); 4032 } 4033 } else if (o instanceof ArrayRefExpr) { 4034 // array elements like a[i] 4035 ArrayRefExpr arr = (ArrayRefExpr)o; 4036 Expr a = TrAnExpr.trSpecExpr(arr.array,argsMap,argsMap,thisTrans); 4037 Expr index = arr.index == null ? GC.zerolit : 4038 TrAnExpr.trSpecExpr(arr.index,argsMap,argsMap,thisTrans); 4039 translations.add(cacheValue(a)); 4040 locations.add(new Integer(arr.getStartLoc())); 4041 translations.add(cacheValue(index)); 4042 } else if (o instanceof ArrayRangeRefExpr){ 4043 // array ranges like a[i..j] or a[*] 4044 ArrayRangeRefExpr arr = (ArrayRangeRefExpr)o; 4045 Expr a = TrAnExpr.trSpecExpr(arr.array,argsMap,argsMap,thisTrans); 4046 Expr low = arr.lowIndex == null ? GC.zerolit : 4047 TrAnExpr.trSpecExpr(arr.lowIndex,argsMap,argsMap,thisTrans); 4048 Expr hi = arr.highIndex == null ? 4049 GC.nary(TagConstants.INTEGRALSUB,GC.nary(TagConstants.ARRAYLENGTH,a),GC.onelit) : 4050 TrAnExpr.trSpecExpr(arr.highIndex,argsMap,argsMap,thisTrans); 4051 translations.add(cacheValue(a)); 4052 translations.add(cacheValue(low)); 4053 translations.add(cacheValue(hi)); 4054 } else if (o instanceof NothingExpr) { 4055 // skip 4056 } else if (o instanceof EverythingExpr) { 4057 // skip 4058 } else if (o instanceof WildRefExpr) { 4059 // store refs like a.* or this.* or Type.* or super.* 4060 // skip - the wildref expression is expanded into 4061 // all of the fields by the iterator 4062 } else { 4063 // FIXME - turn into internal error 4064 System.out.println("UNSUPPORTED " + o.getClass()); 4065 } 4066 } 4067 4068 GC.thisvar.decl.type = savedType; // FIXME - put in finally clause? 4069 4070 // An assignment generated for each modified target 4071 // of the form i:7.19 = after@16.2:20.19 4072 4073 // Here we handle special variables like alloc and state 4074 for (int ii=0; ii<spec.specialTargets.size(); ii++) { 4075 Expr target = spec.specialTargets.elementAt(ii); 4076 GuardedCmd gc = modify(target, pt, scall); 4077 4078 if (gc != null) codevec.addElement(gc); 4079 } 4080 4081 // Here we set everything in the modifies clauses to 4082 // unspecified values. For instance, for simple variables 4083 // we add the command: i:7.19 = after@16.2:20.19 4084 // There is nothing specified about the after variables. 4085 iter = new Frame.ModifiesIterator(rd.parent,mgp.items,true,true); 4086 while (iter.hasNext()) { 4087 Object o = iter.next(); 4088 if (o instanceof FieldAccess) { 4089 VariableAccess a = (VariableAccess)translations.removeFirst(); 4090 if (a != null) { 4091 Expr obj = (Expr)translations.removeFirst(); 4092 // if obj == null, the variable is static 4093 int loc = ((Integer)(locations.removeFirst())).intValue(); 4094 VariableAccess newVal = 4095 temporary("after@" + UniqName.locToSuffix(scall), 4096 loc, loc); 4097 GuardedCmd g = obj != null ? 4098 GC.subgets(a, obj, newVal ) : 4099 GC.gets(a, newVal); 4100 codevec.addElement(g); 4101 } 4102 } else if (o instanceof ArrayRefExpr) { 4103 Expr a = (Expr)translations.removeFirst(); 4104 Expr index = (Expr)translations.removeFirst(); 4105 int loc = ((Integer)(locations.removeFirst())).intValue(); 4106 VariableAccess newVal = temporary("after@" + UniqName.locToSuffix(scall), 4107 loc, loc); 4108 GuardedCmd g = GC.subsubgets(GC.elemsvar, a, index, newVal); 4109 codevec.addElement(g); 4110 } else if (o instanceof ArrayRangeRefExpr){ 4111 // This one is slightly different. The array a is 4112 // replaced by a new array unset(a,low,hi). 4113 // In the background predicate, unset(a,i,j) has the 4114 // same array elements as a, except for values between 4115 // i and j, inclusive. 4116 Expr a = (Expr)translations.removeFirst(); 4117 Expr low = (Expr)translations.removeFirst(); 4118 Expr hi = (Expr)translations.removeFirst(); 4119 GuardedCmd g = GC.subgets(GC.elemsvar, a, GC.nary(TagConstants.UNSET, GC.select(GC.elemsvar,a), low, hi)); 4120 codevec.addElement(g); 4121 } else if (o instanceof NothingExpr) { 4122 // skip 4123 } else if (o instanceof EverythingExpr) { 4124 // FIXME !!! 4125 } else if (o instanceof WildRefExpr) { 4126 // skip - the wildref expression is expanded into 4127 // all of the fields by the iterator 4128 } else { 4129 // FIXME - turn into an internal error 4130 System.out.println("UNSUPPORTED " + o.getClass()); 4131 } 4132 } 4133 GuardedCmd seq = GC.seq(codevec); 4134 GuardedCmd ifcmd = GC.ifcmd(precondition,seq,GC.skip()); 4135 code.addElement(ifcmd); 4136 } 4137 4138 if (spec.modifiesEverything) { 4139 EverythingLoc el = new EverythingLoc(scall,pt); 4140 modifyEverythingLocations.add(el); 4141 el.completed.add(GC.ecvar); 4142 el.completed.add(GC.resultvar); 4143 el.completed.add(GC.xresultvar); 4144 code.addElement(el.gcseq); 4145 Iterator iter = spec.postconditionLocations.iterator(); 4146 while (iter.hasNext()) { 4147 Object o = iter.next(); 4148 if (o instanceof Expr) el.add((Expr)o); 4149 else System.out.println("WHAT? " + o.getClass() + " " + o); 4150 // FIXME 4151 } 4152 4153 } 4154 4155 // modify EC, RES, XRES 4156 code.addElement(modify(GC.ecvar, scall)); 4157 if (!spec.dmd.isConstructor()) { 4158 if (freshResult) code.addElement(GC.gets(GC.resultvar, eod)); 4159 else { 4160 code.addElement(modify(GC.resultvar, scall)); 4161 } 4162 } 4163 code.addElement(modify(GC.xresultvar, scall)); 4164 4165 // FIXME - we might be doing statevar twice - once 4166 // up above before the assignments of after values to 4167 // all the items in the modifies clause 4168 if (!Utils.isPure(rd)) 4169 code.addElement(modify(GC.statevar, scall)); 4170 4171 for (int i=0; i<spec.postAssumptions.size(); ++i) { 4172 addAssumption(spec.postAssumptions.elementAt(i)); 4173 } 4174 4175 // FIXME - do we need this - I think we already do it 4176 // FIXME - figure out why this needs Exception instead of Throwable 4177 4178 addAssumption( 4179 GC.or( 4180 GC.nary(TagConstants.ANYEQ,GC.ecvar,GC.ec_return), 4181 GC.and( 4182 GC.nary(TagConstants.ANYEQ,GC.ecvar,GC.ec_throw), 4183 GC.nary(TagConstants.TYPELE, 4184 GC.nary(TagConstants.TYPEOF,GC.xresultvar), 4185 GC.typeExpr( 4186 Main.options().useThrowable ? 4187 Types.javaLangThrowable() : Types.javaLangException() ) 4188 ) 4189 ) 4190 ) 4191 ); 4192 4193 // assume postconditions 4194 Condition exceptionCondition = null; 4195 for(int i=0; i<spec.post.size(); i++) { 4196 Condition cond = spec.post.elementAt(i); 4197 if (cond.label == TagConstants.CHKUNEXPECTEDEXCEPTION) { 4198 continue; 4199 } 4200 if (cond.label == TagConstants.CHKUNEXPECTEDEXCEPTION2) { 4201 exceptionCondition = cond; 4202 continue; 4203 } 4204 code.addElement(GC.assumeAnnotation(cond.locPragmaDecl, 4205 GC.subst(call.scall, call.ecall, 4206 pt, cond.pred))); 4207 } 4208 if (exceptionCondition != null && 4209 NoWarn.getChkStatus(TagConstants.CHKUNEXPECTEDEXCEPTION2) == 4210 TagConstants.CHK_AS_ASSERT) { 4211 Condition cond = exceptionCondition; 4212 int loc = rd.locThrowsKeyword; 4213 if (loc == Location.NULL) loc = rd.getStartLoc(); 4214 addCheck(call.scall, 4215 TagConstants.CHKUNEXPECTEDEXCEPTION2, 4216 GC.subst( call.scall, call.ecall, pt, cond.pred), 4217 loc); 4218 } 4219 } 4220 4221 if( spec.dmd.throwsSet != null && spec.dmd.throwsSet.size() != 0 ) { 4222 // #if (! superOrSiblingConstructorCall) 4223 // assume EC == ec$return [] assume EC == ec$throw; raise 4224 // #else 4225 // assume EC == ec$return [] 4226 // assume EC == ec$throw; assume !isAllocated(objectToBeConstructed, alloc); raise 4227 // #end 4228 4229 code.push(); 4230 code.addElement( GC.assume( GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_return ))); 4231 4232 code.push(); 4233 if (Main.options().traceInfo > 0) { 4234 // add a label to track whether the method invocation throws an 4235 // exception 4236 GuardedCmd g = traceInfoLabelCmd(scall, ecall, 4237 "RoutineException", scall); 4238 code.addElement(g); 4239 } 4240 GuardedCmd cmd = GC.assume( GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_throw )); 4241 code.addElement( cmd ); 4242 4243 if (superOrSiblingConstructorCall) { 4244 Expr isAllocated = GC.nary(TagConstants.ISALLOCATED, 4245 GC.objectTBCvar, GC.allocvar); 4246 code.addElement(GC.assume(GC.not(isAllocated))); 4247 } 4248 code.addElement( GC.raise() ); 4249 4250 code.addElement( GC.boxPopFromStackVector(code) ); 4251 } 4252 4253 // extract code and temporaries created, and put into call.desugared 4254 4255 call.desugared = DynInstCmd.make(UniqName.locToSuffix(call.scall), spill()); 4256 4257 // all done 4258 return call; 4259 } 4260 4261 /** 4262 * Computes the inlining settings for a given call. A return value of 4263 * <code>null</code> means "don't inline". 4264 */ 4265 private InlineSettings computeInlineSettings(/*@ non_null */ RoutineDecl rd, 4266 /*@ non_null */ ExprVec argsRaw, 4267 InlineSettings inline, 4268 int scall) { 4269 // Try to use the given inline settings, but bag out if the routine 4270 // doesn't have a body 4271 if (inline != null) { 4272 if (rd.body == null) { 4273 // if we don't have the routine's body, we can't inline it 4274 // (does this ever happen? --jbs) 4275 if (this.issueCautions) { 4276 ErrorSet.caution(scall, "Couldn't inline call because the routine's body was not found"); 4277 } 4278 return null; 4279 } 4280 // TBW: should there be a check for isRecursiveInvocation here? 4281 return new InlineSettings(inline, 4282 inlineCheckDepth, inlineDepthPastCheck); 4283 } 4284 4285 if (rd.body == null) { 4286 return null; 4287 } 4288 4289 // Set the inlining bits appropriately, according to any given "helper" 4290 // pragma, but only if this is a non-recursive call. 4291 if (Helper.isHelper(rd) && !isRecursiveInvocation(rd)) { 4292 return new InlineSettings(false, false, true, 4293 inlineCheckDepth, inlineDepthPastCheck); 4294 } 4295 4296 // Set the inlining bits appropriately, according to the 4297 // flag -inlineFromConstructors. 4298 if (Main.options().inlineFromConstructors && inConstructorContext && 4299 !isRecursiveInvocation(rd)) { 4300 // inline if "rd" is an instance method in the same class as rdCurrent 4301 if (rd instanceof MethodDecl && !Modifiers.isStatic(rd.modifiers) && 4302 rd.parent == rdCurrent.parent) { 4303 // ...and the method is not overridable 4304 if (!FlowInsensitiveChecks.isOverridable((MethodDecl)rd)) { 4305 // ...and the method is clearly being invoked on the "this" object 4306 Assert.notFalse(1 <= argsRaw.size()); // it's an instance method! 4307 VarInit e0 = argsRaw.elementAt(0); 4308 e0 = trim(e0); 4309 if (e0.getTag() == TagConstants.THISEXPR && 4310 ((ThisExpr)e0).classPrefix == null) { 4311 // inline it! 4312 return new InlineSettings(false, false, true, 4313 inlineCheckDepth, inlineDepthPastCheck); 4314 } 4315 } 4316 } 4317 } 4318 4319 // Set the inlining bits appropriately, according to the two 4320 // inlining depth flags. 4321 // Also set the inlining depth flags for the next level appropriately. 4322 // We don't inline constructors because of problems with checking 4323 // the constructor for Object. 4324 if ((inlineCheckDepth > 0 || inlineDepthPastCheck > 0) && 4325 rd instanceof MethodDecl && rd.body != null) { 4326 4327 InlineSettings is = new InlineSettings(true, true, true, 4328 inlineCheckDepth, 4329 inlineDepthPastCheck); 4330 if (inlineCheckDepth > 1) { 4331 // don't check anything until we've reached the check depth 4332 is.nextInlineCheckDepth--; 4333 } else if (inlineCheckDepth == 1) { 4334 // check the body at the check depth 4335 is.dontCheckInlinedBody = false; 4336 is.getSpecForInline = false; 4337 is.nextInlineCheckDepth--; 4338 } else if (inlineCheckDepth == 0) { 4339 // check the preconditions of calls from the check depth 4340 is.dontCheckPreconditions = false; 4341 is.nextInlineCheckDepth--; 4342 is.nextInlineDepthPastCheck--; 4343 } else { 4344 // don't check anything lower than the check depth 4345 is.nextInlineDepthPastCheck--; 4346 } 4347 4348 return is; 4349 } 4350 4351 // don't inline 4352 return null; 4353 } 4354 4355 /** 4356 * If the flag is true, set all assertion checks to assumes. Otherwise, make 4357 * sure that regular checking of assertions is performed. 4358 */ 4359 public static void globallyTurnOffChecks(boolean flag) { 4360 if (flag) { 4361 // turn precondition checks into assumes 4362 NoWarn.useGlobalStatus = true; 4363 NoWarn.globalStatus = TagConstants.CHK_AS_ASSUME; 4364 } 4365 else 4366 NoWarn.useGlobalStatus = false; 4367 } 4368 4369 /** 4370 * When a call is inlined, we need to substitute the new names given to its 4371 * formal parameters for its original names in the inlined body. 4372 */ 4373 private static GuardedCmd substituteGC(/*@ non_null */ Hashtable pt, 4374 /*@ non_null */ GuardedCmd gc) { 4375 int tag = gc.getTag(); 4376 switch (tag) { 4377 case TagConstants.SKIPCMD: 4378 case TagConstants.RAISECMD: 4379 return gc; 4380 case TagConstants.ASSERTCMD: 4381 case TagConstants.ASSUMECMD: 4382 { 4383 ExprCmd exprcmd = (ExprCmd) gc; 4384 return ExprCmd.make(exprcmd.cmd, 4385 Substitute.doSubst(pt, exprcmd.pred), 4386 exprcmd.loc); 4387 } 4388 case TagConstants.GETSCMD: 4389 { 4390 GetsCmd getscmd = (GetsCmd) gc; 4391 return GetsCmd.make((VariableAccess) 4392 Substitute.doSubst(pt, getscmd.v), 4393 Substitute.doSubst(pt, getscmd.rhs)); 4394 } 4395 case TagConstants.SUBGETSCMD: 4396 { 4397 SubGetsCmd sgetscmd = (SubGetsCmd) gc; 4398 return SubGetsCmd.make((VariableAccess) 4399 Substitute.doSubst(pt, sgetscmd.v), 4400 Substitute.doSubst(pt, sgetscmd.rhs), 4401 Substitute.doSubst(pt, sgetscmd.index)); 4402 } 4403 case TagConstants.SUBSUBGETSCMD: 4404 { 4405 SubSubGetsCmd ssgetscmd = (SubSubGetsCmd) gc; 4406 return SubSubGetsCmd.make((VariableAccess) 4407 Substitute.doSubst(pt, ssgetscmd.v), 4408 Substitute.doSubst(pt, ssgetscmd.rhs), 4409 Substitute.doSubst(pt, ssgetscmd.index1), 4410 Substitute.doSubst(pt, ssgetscmd.index2)); 4411 } 4412 case TagConstants.RESTOREFROMCMD: 4413 { 4414 RestoreFromCmd rfcmd = (RestoreFromCmd) gc; 4415 return RestoreFromCmd.make((VariableAccess) 4416 Substitute.doSubst(pt, rfcmd.v), 4417 Substitute.doSubst(pt, rfcmd.rhs)); 4418 } 4419 case TagConstants.SEQCMD: 4420 { 4421 SeqCmd scmd = (SeqCmd) gc; 4422 int size = scmd.cmds.size(); 4423 GuardedCmdVec vec = GuardedCmdVec.make(size); 4424 for (int i = 0; i < size; i++) 4425 vec.addElement(substituteGC(pt, scmd.cmds.elementAt(i))); 4426 return SeqCmd.make(vec); 4427 } 4428 case TagConstants.VARINCMD: 4429 { 4430 VarInCmd vicmd = (VarInCmd) gc; 4431 return GC.block(vicmd.v, substituteGC(pt, vicmd.g)); 4432 } 4433 case TagConstants.DYNINSTCMD: 4434 { 4435 DynInstCmd dc = (DynInstCmd) gc; 4436 return DynInstCmd.make(dc.s, substituteGC(pt, dc.g)); 4437 } 4438 case TagConstants.TRYCMD: 4439 case TagConstants.CHOOSECMD: 4440 { 4441 CmdCmdCmd cccmd = (CmdCmdCmd) gc; 4442 return CmdCmdCmd.make(cccmd.cmd, 4443 substituteGC(pt, cccmd.g1), 4444 substituteGC(pt, cccmd.g2)); 4445 } 4446 case TagConstants.CALL: 4447 { 4448 Call call = (Call) gc; 4449 int size = call.args.size(); 4450 ExprVec vec = ExprVec.make(size); 4451 for (int i = 0; i < size; i++) 4452 vec.addElement(Substitute.doSubst(pt, 4453 call.args.elementAt(i))); 4454 Call res = Call.make(vec, call.scall, call.ecall, 4455 call.inlined); 4456 res.desugared = substituteGC(pt, call.desugared); 4457 res.rd = call.rd; 4458 res.spec = call.spec; 4459 return res; 4460 } 4461 case TagConstants.LOOPCMD: 4462 { 4463 LoopCmd lcmd = (LoopCmd) gc; 4464 LoopCmd res = GC.loop(lcmd.locStart, lcmd.locEnd, lcmd.locHotspot, 4465 lcmd.oldmap, 4466 lcmd.invariants, lcmd.decreases, 4467 lcmd.skolemConstants, lcmd.predicates, 4468 lcmd.tempVars, lcmd.guard, 4469 lcmd.body); 4470 res.desugared = substituteGC(pt, lcmd.desugared); 4471 return res; 4472 } 4473 default: 4474 //@ unreachable; 4475 Assert.fail("Unknown kind of guarded command encountered"); 4476 return null; 4477 } 4478 } 4479 4480 /** 4481 * Destructively change the trace labels in <code>gc</code> to insert sequence 4482 * numbers that are used by the ErrorMsg class in printing trace labels in the 4483 * correct execution order. This method requires that trace labels do not yet 4484 * contain sequence numbers. 4485 */ 4486 public static void addTraceLabelSequenceNumbers(/*@ non_null */ GuardedCmd gc) { 4487 // order the body's trace labels by execution order 4488 if (Main.options().traceInfo > 0) { 4489 orderTraceLabels(gc, 0); 4490 } 4491 } 4492 4493 /** 4494 * Walk through the guarded command translation of a method, adding unique number 4495 * to its location sequence, in order to sort trace labels in order of execution. 4496 * This is a destructive operation. 4497 */ 4498 private static int orderTraceLabels(/*@ non_null */ GuardedCmd gc, int count) { 4499 int tag = gc.getTag(); 4500 switch (tag) { 4501 case TagConstants.SKIPCMD: 4502 case TagConstants.RAISECMD: 4503 case TagConstants.ASSERTCMD: 4504 case TagConstants.GETSCMD: 4505 case TagConstants.SUBGETSCMD: 4506 case TagConstants.SUBSUBGETSCMD: 4507 case TagConstants.RESTOREFROMCMD: 4508 return count; 4509 case TagConstants.ASSUMECMD: 4510 { 4511 Expr pred = ((ExprCmd) gc).pred; 4512 if (pred.getTag() == TagConstants.LABELEXPR) { 4513 LabelExpr le = (LabelExpr) pred; 4514 count = orderTraceLabel(le, count); 4515 } 4516 return count; 4517 } 4518 case TagConstants.SEQCMD: 4519 { 4520 SeqCmd scmd = (SeqCmd) gc; 4521 int size = scmd.cmds.size(); 4522 for (int i = 0; i < size; i++) 4523 count = orderTraceLabels(scmd.cmds.elementAt(i), count); 4524 return count; 4525 } 4526 case TagConstants.VARINCMD: 4527 { 4528 VarInCmd vicmd = (VarInCmd) gc; 4529 return orderTraceLabels(vicmd.g, count); 4530 } 4531 case TagConstants.DYNINSTCMD: 4532 { 4533 DynInstCmd dc = (DynInstCmd) gc; 4534 return orderTraceLabels(dc.g, count); 4535 } 4536 case TagConstants.TRYCMD: 4537 case TagConstants.CHOOSECMD: 4538 { 4539 CmdCmdCmd cccmd = (CmdCmdCmd) gc; 4540 count = orderTraceLabels(cccmd.g1, count); 4541 return orderTraceLabels(cccmd.g2, count); 4542 } 4543 case TagConstants.CALL: 4544 { 4545 Call call = (Call) gc; 4546 return orderTraceLabels(call.desugared, count); 4547 } 4548 case TagConstants.LOOPCMD: 4549 { 4550 LoopCmd lcmd = (LoopCmd) gc; 4551 return orderTraceLabels(lcmd.desugared, count); 4552 } 4553 default: 4554 //@ unreachable; 4555 Assert.fail("Unknown kind of guarded command encountered"); 4556 return -1; 4557 } 4558 } 4559 4560 /** 4561 * If the given label is a trace label, add the <code>count</code> number to the 4562 * given label expression's label name, so that trace labels will sort correctly. 4563 */ 4564 private static int orderTraceLabel(/*@ non_null */ LabelExpr le, int count) { 4565 String name = le.label.toString(); 4566 if (ErrorMsg.isTraceLabel(name)) { 4567 // check that we aren't touching a label that has already had a 4568 // number prefixed to it 4569 Assert.notFalse(name.indexOf(",") == -1); 4570 int k = name.indexOf("^"); 4571 Assert.notFalse(k != -1); 4572 name = name.substring(0, k+1) + String.valueOf(count) + "," + 4573 name.substring(k+1); 4574 le.label = Identifier.intern(name); 4575 count++; 4576 } 4577 4578 return count; 4579 } 4580 4581 4582 /*************************************************** 4583 * * 4584 * Generating temporary variables: * 4585 * * 4586 ***************************************************/ 4587 4588 /** 4589 * Countains the number of temporaries generated for the method currently being 4590 * translated. 4591 * 4592 * <p> Reset to 0 on entry to {@link #trExpr(boolean, VarInit)}. 4593 */ 4594 private int tmpcount; 4595 4596 /** 4597 * Generate a temporary for the result of a given expression. 4598 * 4599 * <p> This partially implements ESCJ 23b, case 6. 4600 */ 4601 private VariableAccess fresh(/*@ non_null */ VarInit e, int loc) { 4602 return fresh(e, loc, null); 4603 } 4604 4605 private VariableAccess fresh(/*@ non_null */ VarInit e, int loc, String suffix) { 4606 String name = "tmp" + tmpcount++; 4607 if (suffix != null) { 4608 name += "!" + suffix; 4609 } 4610 return temporary(name, e.getStartLoc(), loc); 4611 } 4612 4613 /** 4614 * Generate a temporary variable with prefix <code>s</code> and associated 4615 * expression location information <code>locAccess</code>. 4616 */ 4617 private VariableAccess temporary(String s, int locAccess) { 4618 return temporary(s, locAccess, Location.NULL); 4619 } 4620 4621 private VariableAccess temporary(String s, int locAccess, int locIdDecl) { 4622 // As per ESCJ 23b, case 6, we do not use locId: 4623 if (locIdDecl == Location.NULL) { 4624 locIdDecl = UniqName.temporaryVariable; 4625 } 4626 4627 Identifier idn = Identifier.intern(s); 4628 VariableAccess result = GC.makeVar(idn, locIdDecl); 4629 temporaries.addElement(result.decl); 4630 result.loc = locAccess; 4631 4632 return result; 4633 } 4634 4635 public static Expr mapLocation(Expr e, int loc) { 4636 int tag = e.getTag(); 4637 switch (tag) { 4638 case TagConstants.LABELEXPR: 4639 LabelExpr le = (LabelExpr)e; 4640 String s = le.label.toString(); 4641 if (s.indexOf('@') != -1) return e; 4642 return LabelExpr.make(le.sloc,le.eloc,le.positive, 4643 Identifier.intern( 4644 s+"@"+UniqName.locToSuffix(loc)), 4645 le.expr); 4646 case TagConstants.BOOLOR: 4647 case TagConstants.BOOLAND: 4648 case TagConstants.BOOLANDX: 4649 ExprVec ev = ExprVec.make(); 4650 NaryExpr ne = (NaryExpr)e; 4651 ExprVec evo = ne.exprs; 4652 for (int k=0; k<evo.size(); ++k) { 4653 Expr ex = evo.elementAt(k); 4654 ex = mapLocation(ex,loc); 4655 ev.addElement(ex); 4656 } 4657 return NaryExpr.make(ne.sloc, ne.eloc, ne.op, 4658 ne.methodName, ev); 4659 default: 4660 return e; 4661 } 4662 } 4663 4664 public ArrayList modifyEverythingLocations = new ArrayList(); 4665 4666 public class EverythingLoc { 4667 public int loc; 4668 public Hashtable pt; 4669 public SeqCmd gcseq = SeqCmd.make(GuardedCmdVec.make()); 4670 public Set completed = new Set(); 4671 public EverythingLoc(int loc, Hashtable pt) { 4672 this.loc = loc; 4673 this.pt = pt; 4674 } 4675 public void add(Expr e) { 4676 if (e instanceof VariableAccess) { 4677 if (completed.contains( ((VariableAccess)e).decl )) return; 4678 completed.add( ((VariableAccess)e).decl ); 4679 } 4680 GuardedCmd gc = modify(e, pt, loc); 4681 if (gc != null) gcseq.cmds.addElement(gc); 4682 } 4683 } 4684 4685 public void addMoreLocations(java.util.Set s) { 4686 Iterator ii = modifyEverythingLocations.iterator(); 4687 while (ii.hasNext()) { 4688 EverythingLoc ev = (EverythingLoc)ii.next(); 4689 Iterator i = s.iterator(); 4690 while (i.hasNext()) { 4691 Object o = i.next(); 4692 ev.add((Expr)o); 4693 } 4694 } 4695 } 4696 4697 // Changes all BOOLANDX operations to BOOLIMPLIES, in place 4698 static void setop(ASTNode e) { 4699 if (e instanceof NaryExpr) { 4700 NaryExpr ne = (NaryExpr)e; 4701 if (ne.getTag() == TagConstants.BOOLANDX) { 4702 ne.op = TagConstants.BOOLIMPLIES; 4703 } 4704 } 4705 int n = e.childCount(); 4706 for (int i = 0; i<n; ++i) { 4707 Object o = e.childAt(i); 4708 if (o != null && o instanceof ASTNode) setop((ASTNode)o); 4709 } 4710 } 4711 4712 public Expr addNewString(VarInit x, Expr left, Expr right) { 4713 // Construct variables 4714 VariableAccess result= fresh(x, x.getStartLoc(), "newString!"); 4715 VariableAccess newallocvar= adorn(GC.allocvar); 4716 4717 ExprVec ev = ExprVec.make(5); 4718 ev.addElement(result); 4719 ev.addElement(left); 4720 ev.addElement(right); 4721 ev.addElement(GC.allocvar); 4722 ev.addElement(newallocvar); 4723 4724 Expr newstring = GC.nary(x.getStartLoc(), x.getEndLoc(), 4725 TagConstants.STRINGCATP, ev); 4726 4727 // Emit the Assume and a Gets commands 4728 code.addElement(GC.assume(newstring)); 4729 code.addElement(GC.gets(GC.allocvar, newallocvar)); 4730 4731 return result; // FIXME - we are omitting the protect, which I don't understand 4732 } 4733 4734 public static class Strings { 4735 static Map map = new HashMap(); 4736 static private int count = 0; 4737 static Integer intern(String s) { 4738 Object o = map.get(s); 4739 if (o != null) return ((Integer)o); 4740 Integer i = new Integer(++count); 4741 map.put(s,i); 4742 return i; 4743 } 4744 } 4745 4746 private GuardedCmdVec codevec; 4747 private Identifier cacheVar = Identifier.intern("modCache"); 4748 4749 public VariableAccess cacheValue(Expr e) { 4750 VariableAccess va = GC.makeVar(cacheVar, e.getStartLoc()); 4751 codevec.addElement(GC.gets(va, e)); 4752 return va; 4753 } 4754 } // end of class Translate 4755 4756 // FIXME - translation of model vars is handled for set, assume, assert, ghost decls 4757 // But still need to do so for other types of statement pragmas 4758 // Also need to do so for quantified expresssions. 4759 // What about for old expressions? 4760 4761 /* 4762 * Local Variables: 4763 * Mode: Java 4764 * fill-column: 85 4765 * End: 4766 */