001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package escjava.translate; 004 005 import escjava.Main; 006 import escjava.ast.*; 007 import escjava.ast.Modifiers; 008 import escjava.ast.TagConstants; 009 import escjava.backpred.FindContributors; 010 import escjava.tc.TypeCheck; 011 import escjava.tc.Types; 012 import java.util.ArrayList; 013 import java.util.Enumeration; 014 import java.util.HashSet; 015 import java.util.Hashtable; 016 import java.util.Iterator; 017 import javafe.ast.*; 018 import javafe.tc.TypeSig; 019 020 import javafe.util.*; 021 022 /** 023 * Responsible for getting Spec for calls. Includes ... from ESCJ16c. 024 */ 025 026 public final class GetSpec { 027 028 public static Spec getSpecForCall(/*@ non_null */RoutineDecl rd, 029 /*@ non_null */FindContributors scope, Set predictedSynTargs) { 030 Spec spec = getCommonSpec(rd, scope, null); 031 return extendSpecForCall(spec, scope, predictedSynTargs); 032 } 033 034 /* used for calls that are inlined */ 035 public static Spec getSpecForInline(/*@ non_null */RoutineDecl rd, 036 /*@ non_null */FindContributors scope) { 037 return getCommonSpec(rd, scope, null); 038 // TBW: Should also add NonNullInit checks somewhere! 039 } 040 041 public static Spec getSpecForBody(/*@ non_null */RoutineDecl rd, 042 /*@ non_null */FindContributors scope, 043 /*@ non_null */Set synTargs, Hashtable premap) { 044 Spec spec = getCommonSpec(rd, scope, premap); 045 return extendSpecForBody(spec, scope, synTargs); 046 } 047 048 private static /*@ non_null @*/ Spec getCommonSpec( 049 /*@ non_null */RoutineDecl rd, 050 /*@ non_null */FindContributors scope, Hashtable premap) { 051 /* 052 * Need to typecheck TypeDecl containing callee so that 053 * requires/ensures/modifies clauses etc are resolved. 054 */ 055 056 TypeSig T = TypeSig.getSig(rd.parent); 057 T.typecheck(); 058 059 DerivedMethodDecl combined = getCombinedMethodDecl(rd); 060 DerivedMethodDecl filtered = filterMethodDecl(combined, scope); 061 062 /* 063 * If we are translating the spec for an inner-class constructor, then we 064 * need to substitute this$0arg for this.this$0 everywhere: 065 */ 066 Spec spec = null; 067 try { 068 if (filtered.isConstructor() && !T.isTopLevelType()) { 069 Inner.firstThis0 = Inner 070 .getEnclosingInstanceArg((ConstructorDecl)filtered.original); 071 } 072 073 spec = trMethodDecl(filtered, premap); 074 } finally { 075 Inner.firstThis0 = null; 076 } 077 078 return spec; 079 } 080 081 static private /*@ non_null @*/ ASTDecoration dmdDecoration = new ASTDecoration("dmd"); 082 083 /** 084 * * Implement GetCombinedMethodDecl from ESCJ 16c section 7: 085 * <p>* * Precondition: the type declaring rd has been typechecked. 086 * <p>* * Note: this routine may typecheck the supertypes of the type that * 087 * declares rd. 088 */ 089 //@ ensures \result != null; 090 public static DerivedMethodDecl getCombinedMethodDecl( 091 /*@ non_null */RoutineDecl rd) 092 { 093 DerivedMethodDecl dmd = (DerivedMethodDecl)dmdDecoration.get(rd); 094 if (dmd != null) return dmd; 095 096 dmd = new DerivedMethodDecl(rd); 097 dmdDecoration.set(rd, dmd); 098 099 dmd.throwsSet = rd.raises; 100 dmd.requires = ExprModifierPragmaVec.make(); 101 dmd.modifies = ModifiesGroupPragmaVec.make(); 102 dmd.ensures = ExprModifierPragmaVec.make(); 103 dmd.exsures = VarExprModifierPragmaVec.make(); 104 105 if (rd instanceof ConstructorDecl) { 106 // Handle constructor case: 107 dmd.args = rd.args; 108 TypeSig thisType = TypeSig.getSig(rd.parent); 109 if (!thisType.isTopLevelType()) { 110 // An Inner class; add this$0 argument: 111 dmd.args = rd.args.copy(); 112 FormalParaDecl this0arg = Inner 113 .getEnclosingInstanceArg((ConstructorDecl)rd); 114 dmd.args.insertElementAt(this0arg, 0); 115 } 116 117 dmd.returnType = thisType; 118 addModifiersToDMD(dmd, rd); 119 120 } else { 121 // Handle method case: 122 //@ assume rd instanceof MethodDecl; 123 124 MethodDecl md = (MethodDecl)rd; 125 dmd.returnType = md.returnType; 126 127 if (Modifiers.isStatic(rd.modifiers)) { 128 // static method 129 dmd.args = rd.args; 130 } else { 131 // instance method 132 dmd.args = md.args.copy(); 133 dmd.args.insertElementAt((FormalParaDecl)GC.thisvar.decl, 0); 134 } 135 136 /* 137 * Add modifiers from this method as well as all methods it overrides; 138 * also handle non_null: 139 */ 140 addModifiersToDMD(dmd, md); 141 Set overrides = escjava.tc.FlowInsensitiveChecks.getAllOverrides(md); 142 Enumeration overridden_methods = overrides.elements(); 143 while (overridden_methods.hasMoreElements()) { 144 MethodDecl smd = (MethodDecl)overridden_methods.nextElement(); 145 TypeSig.getSig(smd.parent).typecheck(); 146 147 addModifiersToDMD(dmd, smd); 148 } 149 } 150 151 dmd.computeFreshUsage(); 152 153 return dmd; 154 } 155 156 /** 157 * * Add the modifiers of rd to dmd, making any necessary substitions * of 158 * parameter names. Also propagates non_null's. 159 * <p>* * Precondition: rd has been typechecked. 160 * <p> 161 */ 162 private static void addModifiersToDMD(/*@ non_null */DerivedMethodDecl dmd, 163 /*@ non_null */RoutineDecl rd) { 164 /* 165 * Compute the substitution on parameter names to change a spec for an 166 * overridden method to refer to our method's parameter names instead of 167 * its; propagate non_nulls: 168 */ 169 Hashtable subst = new Hashtable(); 170 if (rd != dmd.original) { 171 for (int i = 0; i < rd.args.size(); i++) { 172 GenericVarDecl newDecl = dmd.original.args.elementAt(i); 173 GenericVarDecl oldDecl = rd.args.elementAt(i); 174 175 // This may no longer be necessary, but it doesn't hurt 176 SimpleModifierPragma nonnull = NonNullPragma(oldDecl); 177 if (nonnull != null) setNonNullPragma(newDecl, nonnull); 178 179 VariableAccess va = VariableAccess.make(newDecl.id, Location.NULL, 180 newDecl); 181 182 subst.put(oldDecl, va); 183 } 184 } 185 186 if (rd.pmodifiers == null) return; 187 188 for (int i = 0; i < rd.pmodifiers.size(); i++) { 189 // We omit pragmas that have something notimplemented, but carry on 190 // with the rest 191 try { 192 ModifierPragma mp = rd.pmodifiers.elementAt(i); 193 switch (mp.getTag()) { 194 case TagConstants.REQUIRES: 195 case TagConstants.ALSO_REQUIRES: 196 case TagConstants.PRECONDITION: { 197 ExprModifierPragma emp = (ExprModifierPragma)mp; 198 emp = doSubst(subst, emp); 199 dmd.requires.addElement(emp); 200 break; 201 } 202 case TagConstants.MODIFIESGROUPPRAGMA: { 203 ModifiesGroupPragma em = (ModifiesGroupPragma)mp; 204 for (int ii = 0; ii < em.items.size(); ++ii) { 205 CondExprModifierPragma emp = em.items.elementAt(ii); 206 if (emp.expr == null) { 207 em.items.removeElementAt(i); 208 --ii; 209 continue; 210 } 211 int t = emp.expr.getTag(); 212 // FIXME - no contribution to spec for these keywords 213 if (t == TagConstants.EVERYTHINGEXPR) { 214 dmd.modifiesEverything = true; 215 } else if (t == TagConstants.NOTSPECIFIEDEXPR) { 216 dmd.modifiesEverything = true; 217 emp.expr = EverythingExpr.make(emp.expr.getStartLoc()); 218 //} else if (t == TagConstants.NOTHINGEXPR ) { 219 // no action 220 } 221 emp = doSubst(subst, emp); 222 em.items.setElementAt(emp, ii); 223 } 224 dmd.modifies.addElement(em); 225 break; 226 } 227 /* 228 * case TagConstants.MODIFIES: case TagConstants.ALSO_MODIFIES: case 229 * TagConstants.MODIFIABLE: case TagConstants.ASSIGNABLE: { 230 * CondExprModifierPragma emp = (CondExprModifierPragma)mp; if 231 * (emp.expr == null) break; // ignore - informal int t = 232 * emp.expr.getTag(); // FIXME - no contribution to spec for these 233 * keywords if (t == TagConstants.EVERYTHINGEXPR) { 234 * dmd.modifiesEverything = true; } else if (t == 235 * TagConstants.NOTSPECIFIEDEXPR) { dmd.modifiesEverything = true; 236 * //emp = doSubst(subst, // EverythingExpr.make(emp.getStartLoc()) ); 237 * break; // FIXME } else if (t == TagConstants.NOTHINGEXPR ) { // no 238 * action } else { } emp = doSubst(subst, emp); 239 * dmd.modifies.addElement(emp); break; } 240 */ 241 case TagConstants.ENSURES: 242 case TagConstants.ALSO_ENSURES: 243 case TagConstants.POSTCONDITION: { 244 ExprModifierPragma emp = (ExprModifierPragma)mp; 245 int t = emp.errorTag; 246 emp = doSubst(subst, emp); 247 emp.errorTag = t; 248 dmd.ensures.addElement(emp); 249 break; 250 } 251 case TagConstants.NON_NULL: 252 /* 253 * if (dmd.nonnull == null) { dmd.nonnull = 254 * (SimpleModifierPragma)mp; } 255 */ 256 break; 257 case TagConstants.EXSURES: 258 case TagConstants.ALSO_EXSURES: 259 case TagConstants.SIGNALS: { 260 VarExprModifierPragma vemp = (VarExprModifierPragma)mp; 261 vemp = doSubst(subst, vemp); 262 dmd.exsures.addElement(vemp); 263 break; 264 } 265 default: 266 break; 267 } 268 } catch (NotImplementedException e) { 269 // Error message already printed 270 } 271 } 272 } 273 274 /** Perform a substitution on an ExprModifierPragma * */ 275 private static ExprModifierPragma doSubst(Hashtable subst, 276 /*@ non_null @*/ ExprModifierPragma emp) { 277 return ExprModifierPragma.make(emp.tag, 278 Substitute.doSubst(subst, emp.expr), emp.loc); 279 } 280 281 /** Perform a substitution on a CondExprModifierPragma * */ 282 private static CondExprModifierPragma doSubst(Hashtable subst, 283 /*@ non_null @*/ CondExprModifierPragma emp) 284 { 285 return CondExprModifierPragma.make(emp.tag, Substitute.doSubst(subst, 286 emp.expr), emp.loc, emp.cond == null ? null : Substitute.doSubst(subst, 287 emp.cond)); 288 } 289 290 /** Perform a substitution on a VarExprModifierPragma * */ 291 //@ ensures \result != null; 292 private static VarExprModifierPragma doSubst(Hashtable subst, 293 /*@ non_null @*/ VarExprModifierPragma vemp) 294 { 295 VarExprModifierPragma v = 296 VarExprModifierPragma.make(vemp.tag, vemp.arg, Substitute.doSubst( 297 subst, vemp.expr), vemp.loc); 298 v.setOriginalTag(vemp.originalTag()); 299 return v; 300 } 301 302 //@ ensures \result != null; 303 public static DerivedMethodDecl filterMethodDecl( 304 /*@ non_null */DerivedMethodDecl dmd, 305 /*@ non_null */FindContributors scope) { 306 if (!Main.options().filterMethodSpecs) { return dmd; } 307 308 DerivedMethodDecl dmdFiltered = new DerivedMethodDecl(dmd.original); 309 dmdFiltered.args = dmd.args; 310 dmdFiltered.returnType = dmd.returnType; 311 dmdFiltered.throwsSet = dmd.throwsSet; 312 313 dmdFiltered.requires = dmd.requires; 314 dmdFiltered.modifies = filterModifies(dmd.modifies, scope); 315 dmdFiltered.ensures = filterExprModPragmas(dmd.ensures, scope); 316 dmdFiltered.exsures = filterVarExprModPragmas(dmd.exsures, scope); 317 318 dmdFiltered.computeFreshUsage(); 319 320 return dmdFiltered; 321 } 322 323 //@ ensures \result != null; 324 private static ExprModifierPragmaVec filterExprModPragmas( 325 /*@ non_null */ExprModifierPragmaVec vec, 326 /*@ non_null */FindContributors scope) { 327 int n = vec.size(); 328 ExprModifierPragmaVec vecNew = null; // lazily allocated 329 for (int i = 0; i < n; i++) { 330 ExprModifierPragma emp = vec.elementAt(i); 331 if (exprIsVisible(scope.originType, emp.expr)) { 332 // keep this pragma 333 if (vecNew != null) { 334 vecNew.addElement(emp); 335 } 336 } else { 337 // filter out this pragma 338 if (vecNew == null) { 339 vecNew = ExprModifierPragmaVec.make(n - 1); 340 for (int j = 0; j < i; j++) { 341 vecNew.addElement(vec.elementAt(j)); 342 } 343 } 344 } 345 } 346 if (vecNew == null) { 347 return vec; 348 } else { 349 return vecNew; 350 } 351 } 352 353 //@ ensures \result != null; 354 private static ModifiesGroupPragmaVec filterModifies( 355 /*@ non_null */ModifiesGroupPragmaVec mvec, 356 /*@ non_null */FindContributors scope) { 357 ModifiesGroupPragmaVec result = ModifiesGroupPragmaVec.make(); 358 int mn = mvec.size(); 359 for (int j = 0; j < mn; ++j) { 360 ModifiesGroupPragma mv = mvec.elementAt(j); 361 CondExprModifierPragmaVec vec = mv.items; 362 CondExprModifierPragmaVec vecNew = null; // lazily allocated 363 int n = vec.size(); 364 for (int i = 0; i < n; i++) { 365 CondExprModifierPragma vemp = vec.elementAt(i); 366 if (exprIsVisible(scope.originType, vemp.expr) 367 && exprIsVisible(scope.originType, vemp.cond)) { 368 // keep this pragma 369 if (vecNew != null) { 370 vecNew.addElement(vemp); 371 } 372 } else { 373 // filter out this pragma 374 if (vecNew == null) { 375 vecNew = CondExprModifierPragmaVec.make(n - 1); 376 for (int k = 0; k < i; k++) { 377 vecNew.addElement(vec.elementAt(k)); 378 } 379 } 380 } 381 } 382 result.addElement(ModifiesGroupPragma.make(mv.tag, mv.clauseLoc).append( 383 vecNew == null ? vec : vecNew)); 384 } 385 return result; 386 } 387 388 //@ ensures \result != null; 389 private static VarExprModifierPragmaVec filterVarExprModPragmas( 390 /*@ non_null */VarExprModifierPragmaVec vec, 391 /*@ non_null */FindContributors scope) { 392 int n = vec.size(); 393 VarExprModifierPragmaVec vecNew = null; // lazily allocated 394 for (int i = 0; i < n; i++) { 395 VarExprModifierPragma vemp = vec.elementAt(i); 396 if (exprIsVisible(scope.originType, vemp.expr)) { 397 // keep this pragma 398 if (vecNew != null) { 399 vecNew.addElement(vemp); 400 } 401 } else { 402 // filter out this pragma 403 if (vecNew == null) { 404 vecNew = VarExprModifierPragmaVec.make(n - 1); 405 for (int j = 0; j < i; j++) { 406 vecNew.addElement(vec.elementAt(j)); 407 } 408 } 409 } 410 } 411 if (vecNew == null) { 412 return vec; 413 } else { 414 return vecNew; 415 } 416 } 417 418 //------------------------------------------------------------------------- 419 //------------------------------------------------------------------------- 420 //------------------------------------------------------------------------- 421 422 /** Translates a MethodDecl to a Spec. */ 423 424 //@ ensures \result != null; 425 private static Spec trMethodDecl(/*@ non_null */DerivedMethodDecl dmd, 426 Hashtable premap) { 427 Assert.notNull(dmd); 428 429 /* 430 * Unlike any body we may be translating, for these translations this's type 431 * is that of the type that contains the method or constructor dmd.original. 432 */ 433 TypeSig T = TypeSig.getSig(dmd.getContainingClass()); 434 Type savedType = GC.thisvar.decl.type; 435 GC.thisvar.decl.type = T; 436 437 // (we restore GC.thisvar.decl.type just before returning) 438 439 ExprVec preAssumptions = ExprVec.make(); 440 ConditionVec pre = trMethodDeclPreconditions(dmd, preAssumptions); 441 442 ExprVec targets = ExprVec.make(); 443 ExprVec specialTargets = ExprVec.make(); 444 445 if (!Utils.isPure(dmd.original)) { 446 targets.addElement(GC.statevar); 447 specialTargets.addElement(GC.statevar); 448 } 449 if (dmd.usesFresh) targets.addElement(GC.allocvar); 450 if (dmd.usesFresh) specialTargets.addElement(GC.allocvar); 451 452 // translates modifies list 453 454 for (int k = 0; k < dmd.modifies.size(); ++k) { 455 Frame.ModifiesIterator ii = new Frame.ModifiesIterator( 456 dmd.getContainingClass(),dmd.modifies.elementAt(k).items, true, true); 457 while (ii.hasNext()) { 458 Expr designator = (Expr)ii.next(); 459 //if (Utils.isModel(designator)) continue; 460 Expr gcDesignator = TrAnExpr.trSpecExpr(designator); 461 // Returns null for modifies \nothing, \everything FIXME? 462 // array-range, wild-ref expressions FIXME!! 463 if (gcDesignator != null) { 464 targets.addElement(gcDesignator); 465 } else if (designator instanceof ArrayRangeRefExpr) { 466 targets.addElement(GC.elemsvar); 467 } else if (designator instanceof EverythingExpr) { 468 targets.addElement(GC.elemsvar); 469 } 470 } 471 } 472 473 // handle targets stuff, and create preVarMap 474 475 Set roots = new Set(); // set of GenericVarDecls 476 477 for (int i = 0; i < targets.size(); i++) { 478 Expr gcDesignator = targets.elementAt(i); 479 VariableAccess shaved = shave(gcDesignator); 480 roots.add(shaved.decl); 481 } 482 483 Hashtable preVarMap = premap; 484 if (premap == null) preVarMap = makeSubst(roots.elements(), "pre"); 485 //else 486 // preVarMap = restrict( premap, roots.elements() ); 487 488 /* 489 * Re the change above: premap is a map from variables with a @pre suffix to 490 * their declarations; preVarMap is the relevant piece of this for the 491 * currnet method. However, that was determined by the set of locations 492 * specified in modifies clauses. That leads to erroneous behavior if the 493 * modifies clause is incorrect. 494 * 495 * The change is to use the premap without restriction. That allows the 496 * verification of a body of a method to proceed without dependence on the 497 * accuracy of the modifies clause. However it also adds a lot of conjuncts 498 * into the verification condition - and the premap is accumulated from the 499 * entire class declaration. An improvement would be to simply use the 500 * premap generated from the uses of \old in the body of the method + the 501 * spec of the method + the spec of the class. 502 */ 503 // Now create the postconditions 504 ExprVec postAssumptions = ExprVec.make(); 505 ConditionVec post = trMethodDeclPostcondition(dmd, preVarMap, 506 postAssumptions); 507 508 java.util.Set postlocs = new java.util.HashSet(); 509 int size = post.size(); 510 for (int ic = 0; ic < size; ++ic) { 511 collectFields(post.elementAt(ic).pred, postlocs); 512 } 513 514 Spec spec = Spec.make(dmd, targets, specialTargets, preVarMap, 515 preAssumptions, pre, postAssumptions, post, 516 false && dmd.modifiesEverything, postlocs); // FIXME - turning off 517 // modifies everything for 518 // now 519 520 GC.thisvar.decl.type = savedType; 521 522 return spec; 523 } 524 525 /** Computes the preconditions, according to section 7.2.0 of ESCJ 16. */ 526 527 //@ ensures \result != null; 528 private static ConditionVec trMethodDeclPreconditions( 529 /*@ non_null */DerivedMethodDecl dmd, ExprVec preAssumptions) { 530 ConditionVec pre = ConditionVec.make(); 531 532 // Account for properties about parameters 533 for (int i = 0; i < dmd.args.size(); i++) { 534 FormalParaDecl arg = dmd.args.elementAt(i); 535 536 if (i == 0 && arg == GC.thisvar.decl) { 537 // the special parameter "this" 538 addFreeTypeCorrectAs(arg, TypeSig.getSig(dmd.getContainingClass()), pre); 539 VariableAccess argAccess = TrAnExpr.makeVarAccess(arg, Location.NULL); 540 Expr nonnull = GC.nary(TagConstants.REFNE, argAccess, GC.nulllit); 541 Condition cond = GC.freeCondition(nonnull, Location.NULL); 542 pre.addElement(cond); 543 544 } else { 545 // regular parameters 546 addFreeTypeCorrectAs(arg, arg.type, pre); 547 /* 548 * non_null is handled in the desugaring SimpleModifierPragma 549 * nonNullPragma = NonNullPragma(arg); if (nonNullPragma != null) { 550 * VariableAccess argAccess = TrAnExpr.makeVarAccess(arg, 551 * Location.NULL); Expr nonnull = GC.nary(TagConstants.REFNE, argAccess, 552 * GC.nulllit); Condition cond = GC.freeCondition(nonnull, 553 * nonNullPragma.getStartLoc()); pre.addElement(cond); } 554 */ 555 } 556 } 557 558 if (dmd.isConstructor()) { 559 // Free: RES != null && !isAllocated(RES, wt[[alloc]]) 560 Expr nonnull = GC.nary(TagConstants.REFNE, GC.resultvar, GC.nulllit); 561 Expr allocated = GC.nary(TagConstants.ISALLOCATED, GC.resultvar, 562 GC.allocvar); 563 //(VariableAccess)wt.get(GC.allocvar.decl)); 564 Expr notAllocated = GC.not(allocated); 565 preAssumptions.addElement(nonnull); 566 preAssumptions.addElement(notAllocated); 567 } 568 // Add the declared preconditions 569 570 // Make the disjunction of all of the preconditions 571 572 java.util.Set axsToAdd = new java.util.HashSet(); 573 if (dmd.requires.size() != 0) { 574 Expr expr = dmd.requires.elementAt(0).expr; 575 int loc = dmd.requires.elementAt(0).getStartLoc(); 576 for (int i = 1; i < dmd.requires.size(); ++i) { 577 ExprModifierPragma e = dmd.requires.elementAt(i); 578 if (loc == Location.NULL) loc = e.getStartLoc(); 579 expr = BinaryExpr.make(TagConstants.OR, expr, e.expr, loc); 580 javafe.tc.FlowInsensitiveChecks.setType(expr, Types.booleanType); 581 } 582 TrAnExpr.initForClause(); 583 584 Hashtable map = null; 585 if (dmd.isConstructor()) { 586 map = new Hashtable(); 587 map.put(GC.thisvar.decl, GC.resultvar); 588 //map.put(GC.thisvar.decl, temporary(GC.resultvar.id.toString(), scall, 589 // scall) 590 } 591 Expr pred = TrAnExpr.trSpecExpr(expr, map, null); 592 593 //Expr pred = TrAnExpr.trSpecExpr(expr); 594 if (TrAnExpr.extraSpecs) { 595 preAssumptions.append(TrAnExpr.trSpecExprAuxAssumptions); 596 preAssumptions.append(TrAnExpr.trSpecExprAuxConditions); 597 axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded); 598 TrAnExpr.closeForClause(); 599 } 600 Condition cond = GC.condition(TagConstants.CHKPRECONDITION, pred, loc); 601 602 pre.addElement(cond); 603 } 604 605 addAxioms(axsToAdd, preAssumptions); 606 607 return pre; 608 } 609 610 /** Computes the postconditions, according to section 7.2.2 of ESCJ 16. */ 611 612 //@ ensures \result != null; 613 private static ConditionVec trMethodDeclPostcondition( 614 /*@ non_null */DerivedMethodDecl dmd, 615 /*@ non_null */Hashtable wt, 616 /*@ non_null */ExprVec postAssumptions) { 617 ConditionVec post = ConditionVec.make(); 618 619 // type correctness of targets (including "alloc", if "alloc" is a target) 620 Enumeration wtEnum = wt.keys(); 621 while (wtEnum.hasMoreElements()) { 622 GenericVarDecl vd = (GenericVarDecl)wtEnum.nextElement(); 623 Expr e = TrAnExpr.targetTypeCorrect(vd, wt); 624 Condition cond = GC.freeCondition(e, Location.NULL); 625 post.addElement(cond); 626 } 627 628 if (dmd.isConstructor()) { 629 // Free: RES != null && !isAllocated(RES, wt[[alloc]]) 630 Expr nonnull = GC.nary(TagConstants.REFNE, GC.resultvar, GC.nulllit); 631 Expr allocated = GC.nary(TagConstants.ISALLOCATED, GC.resultvar, 632 (VariableAccess)wt.get(GC.allocvar.decl)); 633 Expr notAllocated = GC.not(allocated); 634 Condition cond = GC.freeCondition(GC.and(nonnull, notAllocated), 635 Location.NULL); 636 post.addElement(cond); 637 } 638 639 if (!Types.isVoidType(dmd.returnType)) { 640 // Free: TypeCorrectAs[[ RES, T ]] 641 addFreeTypeCorrectAs(GC.resultvar.decl, dmd.returnType, post); 642 643 if (Utils.isPure(dmd.original) && ( 644 dmd.original instanceof ConstructorDecl || 645 !Utils.isAllocates(dmd.original))) { 646 Expr e = TrAnExpr.resultEqualsCall(GC.resultvar.decl, dmd.original, wt); 647 Condition cond = GC.freeCondition(e, Location.NULL); 648 post.addElement(cond); 649 } 650 } 651 652 TypeSig T = TypeSig.getSig(dmd.getContainingClass()); 653 if (dmd.isConstructor() && !T.isTopLevelType()) { 654 // Free: RES.this$0 == this$0arg 655 Expr this0 = TrAnExpr.makeVarAccess(Inner.getEnclosingInstanceField(T), 656 Location.NULL); 657 FormalParaDecl this0arg = Inner 658 .getEnclosingInstanceArg((ConstructorDecl)dmd.original); 659 Expr thisSet = GC.nary(TagConstants.REFEQ, 660 GC.select(this0, GC.resultvar), TrAnExpr.makeVarAccess(this0arg, 661 Location.NULL)); 662 Condition cond = GC.freeCondition(thisSet, Location.NULL); 663 post.addElement(cond); 664 } 665 666 if (dmd.throwsSet.size() == 0) { 667 // UnexpectedException: EC == ecReturn 668 Expr pred = GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_return); 669 Condition cond = GC.condition(TagConstants.CHKUNEXPECTEDEXCEPTION, pred, 670 Location.NULL); 671 if (NoWarn.getChkStatus(TagConstants.CHKUNEXPECTEDEXCEPTION) 672 == TagConstants.CHK_AS_ASSERT) post.addElement(cond); 673 cond = GC.condition(TagConstants.CHKUNEXPECTEDEXCEPTION2, pred, 674 Location.NULL); 675 if (NoWarn.getChkStatus(TagConstants.CHKUNEXPECTEDEXCEPTION2) 676 == TagConstants.CHK_AS_ASSERT) post.addElement(cond); 677 } else { 678 // Free: EC == ecThrow ==> 679 // XRES != null && typeof(XRES) <: Throwable && 680 // isAllocated(XRES, alloc) 681 Expr antecedent = GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_throw); 682 ExprVec ev = ExprVec.make(); 683 // XRES != null 684 Expr p = GC.nary(TagConstants.REFNE, GC.xresultvar, GC.nulllit); 685 ev.addElement(p); 686 // typeof(XRES) <: Throwable 687 p = GC.nary(TagConstants.TYPELE, GC.nary(TagConstants.TYPEOF, 688 GC.xresultvar), GC.typeExpr(Types.javaLangThrowable())); 689 ev.addElement(p); 690 // isAllocated(XRES, alloc) 691 p = GC.nary(TagConstants.ISALLOCATED, GC.xresultvar, GC.allocvar); 692 ev.addElement(p); 693 // conjoin and add free postcondition 694 Expr consequence = GC.and(ev); 695 Condition cond = GC.freeCondition(GC.implies(antecedent, consequence), 696 Location.NULL); 697 post.addElement(cond); 698 699 // UnexpectedException: 700 // EC == ecReturn || 701 // (EC == ecThrow && 702 // (typeof(XRES) <: X1 && ... &&& typeof(XRES) <: Xx)) 703 Expr normal = GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_return); 704 Expr except = GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_throw); 705 Expr typeofXRES = GC.nary(TagConstants.TYPEOF, GC.xresultvar); 706 ev.removeAllElements(); 707 int num = dmd.throwsSet.size(); 708 Object originalnum = Utils.exceptionDecoration.get(dmd.original); 709 if (originalnum != null) num = ((Integer)originalnum).intValue(); 710 for (int i = 0; i < num; i++) { 711 TypeName x = dmd.throwsSet.elementAt(i); 712 p = GC.nary(TagConstants.TYPELE, typeofXRES, GC.typeExpr(x)); 713 ev.addElement(p); 714 } 715 Expr pp = GC.or(normal, GC.and(except, GC.or(ev))); 716 717 if (!Main.options().strictExceptions) { 718 for (int i = num; i < dmd.throwsSet.size(); i++) { 719 TypeName x = dmd.throwsSet.elementAt(i); 720 p = GC.nary(TagConstants.TYPELE, typeofXRES, GC.typeExpr(x)); 721 ev.addElement(p); 722 } 723 } 724 725 Expr eOutcomes; 726 eOutcomes = GC.or(ev); 727 728 p = GC.or(normal, GC.and(except, eOutcomes)); 729 730 // Note: This is commented out because we sometimes fabricate a 731 // throws clause where there was none before. - DRCok 732 //Assert.notFalse(dmd.original.locThrowsKeyword != Location.NULL); 733 cond = GC 734 .condition(TagConstants.CHKUNEXPECTEDEXCEPTION, p, Location.NULL); 735 if (NoWarn.getChkStatus(TagConstants.CHKUNEXPECTEDEXCEPTION) 736 == TagConstants.CHK_AS_ASSERT) post.addElement(cond); 737 cond = GC 738 .condition(TagConstants.CHKUNEXPECTEDEXCEPTION2, pp, Location.NULL); 739 if (NoWarn.getChkStatus(TagConstants.CHKUNEXPECTEDEXCEPTION2) 740 == TagConstants.CHK_AS_ASSERT) post.addElement(cond); 741 } 742 743 // constructors ensure that the new object's owner field is null 744 if (dmd.isConstructor()) { 745 // get java.lang.Object 746 TypeSig obj = Types.javaLangObject(); 747 748 FieldDecl owner = null; // make the compiler happy 749 boolean found = true; 750 boolean save = escjava.tc.FlowInsensitiveChecks.inAnnotation; 751 try { 752 escjava.tc.FlowInsensitiveChecks.inAnnotation = true; 753 owner = Types.lookupField(obj, Identifier.intern("owner"), obj); 754 } catch (javafe.tc.LookupException e) { 755 found = false; 756 } finally { 757 escjava.tc.FlowInsensitiveChecks.inAnnotation = save; 758 } 759 // if we couldn't find the owner ghost field, there's nothing to do 760 if (found) { 761 VariableAccess ownerVA = TrAnExpr.makeVarAccess(owner, Location.NULL); 762 Expr everything; 763 Expr ownerNull = GC.nary(TagConstants.REFEQ, GC.select(ownerVA, 764 GC.resultvar), GC.nulllit); 765 // if there are no exceptions thrown, it is sufficient to do 766 // RES.owner == null 767 if (dmd.throwsSet.size() == 0) 768 everything = ownerNull; 769 // else we need to do (EC == ECReturn) ==> (RES.owner == null) 770 else { 771 Expr ret = GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_return); 772 everything = GC.implies(ret, ownerNull); 773 } 774 Condition cond = GC.condition(TagConstants.CHKOWNERNULL, everything, 775 Location.NULL); 776 post.addElement(cond); 777 } 778 } 779 780 // Finally, add declared postconditions 781 // First normal postconditions 782 try { 783 // EC == ecReturn 784 Expr ante = GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_return); 785 786 Hashtable map; 787 if (dmd.isConstructor()) { 788 map = new Hashtable(); 789 map.put(GC.thisvar.decl, GC.resultvar); 790 } else { 791 map = null; 792 } 793 java.util.Set axsToAdd = new java.util.HashSet(); 794 ArrayList conds = new ArrayList(); 795 for (int i = 0; i < dmd.ensures.size(); i++) { 796 try { 797 ExprModifierPragma prag = dmd.ensures.elementAt(i); 798 TrAnExpr.initForClause(); 799 Expr pred = TrAnExpr.trSpecExpr(prag.expr, map, wt); 800 if (TrAnExpr.extraSpecs) { 801 postAssumptions.append(TrAnExpr.trSpecExprAuxAssumptions); 802 postAssumptions.append(TrAnExpr.trSpecExprAuxConditions); 803 axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded); 804 TrAnExpr.closeForClause(); 805 } 806 pred = GC.implies(ante, pred); 807 int tag = prag.errorTag == 0 ? TagConstants.CHKPOSTCONDITION 808 : prag.errorTag; 809 Condition cond = GC.condition(tag, pred, prag.getStartLoc()); 810 conds.add(cond); 811 } catch (NotImplementedException e) { 812 TrAnExpr.closeForClause(); 813 // If something not implemented occurs, a message has already 814 // been issued (unless turned off by an option). We catch it 815 // at this point and go on to the next ensures clause, only 816 // skipping the clause containing the construct that is not 817 // implemented. 818 } 819 } 820 addAxioms(axsToAdd, postAssumptions); 821 Iterator jj = conds.iterator(); 822 while (jj.hasNext()) { 823 post.addElement((Condition)jj.next()); 824 } 825 } finally { 826 TrAnExpr.closeForClause(); 827 } 828 /* 829 * System.out.println("WT"); Enumeration ee = wt.keys(); while 830 * (ee.hasMoreElements()) { Object o = ee.nextElement(); 831 * System.out.println("MAP: " + o + " -->> " + wt.get(o)); } 832 */ 833 // Then exceptional postconditions 834 { 835 // EC == ecThrow 836 Expr ante0 = GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_throw); 837 // typeof(XRES) 838 Expr typeofXRES = GC.nary(TagConstants.TYPEOF, GC.xresultvar); 839 840 java.util.Set axsToAdd = new java.util.HashSet(); 841 ArrayList conds = new ArrayList(); 842 for (int i = 0; i < dmd.exsures.size(); i++) { 843 try { 844 // Pragma has the form: exsures (T v) E 845 VarExprModifierPragma prag = dmd.exsures.elementAt(i); 846 TrAnExpr.initForClause(); 847 // TrSpecExpr[[ E, {v-->XRES}, wt ]] 848 Hashtable map = new Hashtable(); 849 Expr pred; 850 if (prag.arg != null) { 851 map.put(prag.arg, GC.xresultvar); 852 pred = TrAnExpr.trSpecExpr(prag.expr, map, wt); 853 // typeof(XRES) <: T 854 Expr ante1 = GC.nary(TagConstants.TYPELE, typeofXRES, GC 855 .typeExpr(prag.arg.type)); 856 // EC == ecThrow && typeof(XRES) <: T 857 // ==> TrSpecExpr[[ E, {v-->XRES}, wt ]] 858 pred = GC.implies(GC.and(ante0, ante1), pred); 859 } else { 860 pred = TrAnExpr.trSpecExpr(prag.expr, map, wt); 861 pred = GC.implies(ante0, pred); 862 } 863 if (TrAnExpr.extraSpecs) { 864 postAssumptions.append(TrAnExpr.trSpecExprAuxAssumptions); 865 postAssumptions.append(TrAnExpr.trSpecExprAuxConditions); 866 axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded); 867 TrAnExpr.closeForClause(); 868 } 869 //int tag = prag.errorTag == 0 ? TagConstants.CHKPOSTCONDITION : 870 // prag.errorTag; 871 int tag = TagConstants.CHKPOSTCONDITION; 872 Condition cond = GC.condition(tag, pred, prag.getStartLoc()); 873 conds.add(cond); 874 } catch (NotImplementedException e) { 875 TrAnExpr.closeForClause(); 876 } 877 } 878 addAxioms(axsToAdd, postAssumptions); 879 Iterator jj = conds.iterator(); 880 while (jj.hasNext()) { 881 post.addElement((Condition)jj.next()); 882 } 883 } 884 885 // Then any initially clauses (for constructors, if not a helper) 886 887 boolean isHelper = Utils.findModifierPragma(dmd.original.pmodifiers, 888 TagConstants.HELPER) != null; 889 890 if (dmd.isConstructor() && !isHelper) { 891 Hashtable map = new Hashtable(); 892 map.put(GC.thisvar.decl, GC.resultvar); 893 TypeDeclElemVec pmods = dmd.getContainingClass().elems; 894 java.util.Set axsToAdd = new java.util.HashSet(); 895 for (int i = 0; i < pmods.size(); ++i) { 896 TypeDeclElem p = pmods.elementAt(i); 897 if (!(p instanceof TypeDeclElemPragma)) continue; 898 if (((TypeDeclElemPragma)p).getTag() != TagConstants.INITIALLY) 899 continue; 900 ExprDeclPragma prag = (ExprDeclPragma)p; 901 try { 902 TrAnExpr.initForClause(); 903 Expr pred = TrAnExpr.trSpecExpr(prag.expr, map, wt); 904 if (TrAnExpr.extraSpecs) { 905 postAssumptions.append(TrAnExpr.trSpecExprAuxAssumptions); 906 postAssumptions.append(TrAnExpr.trSpecExprAuxConditions); 907 axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded); 908 TrAnExpr.closeForClause(); 909 } 910 int tag = TagConstants.CHKINITIALLY; 911 Condition cond = GC.condition(tag, pred, prag.getStartLoc()); 912 post.addElement(cond); 913 } catch (NotImplementedException e) { 914 TrAnExpr.closeForClause(); 915 } 916 } 917 addAxioms(axsToAdd, postAssumptions); 918 } 919 920 if (dmd.isConstructor() || isHelper) return post; 921 // Then any constraint clauses (for methods) 922 923 TypeDecl tdecl = dmd.getContainingClass(); 924 Set s = new javafe.util.Set(); 925 if (tdecl instanceof InterfaceDecl) 926 s.add(tdecl); 927 else { 928 ClassDecl cdecl = (ClassDecl)tdecl; 929 while (true) { 930 post = addConstraintClauses(post, cdecl, wt, postAssumptions); 931 addSuperInterfaces(cdecl, s); 932 if (cdecl.superClass == null) break; 933 cdecl = (ClassDecl)TypeSig.getSig(cdecl.superClass).getTypeDecl(); 934 } 935 } 936 Enumeration en = s.elements(); 937 while (en.hasMoreElements()) { 938 InterfaceDecl ifd = (InterfaceDecl)en.nextElement(); 939 post = addConstraintClauses(post, ifd, wt, postAssumptions); 940 } 941 return post; 942 } 943 944 /** 945 * axsToAdd holds a Set of RepHelper - we need to add to the assumptions any 946 * axioms pertinent to the RepHelper. 947 */ 948 static public void addAxioms(/*@ non_null @*/ java.util.Set axsToAdd, ExprVec assumptions) { 949 java.util.Set axsDone = new java.util.HashSet(); 950 while (!axsToAdd.isEmpty()) { 951 RepHelper o = (RepHelper)axsToAdd.iterator().next(); 952 axsToAdd.remove(o); 953 if (!axsDone.add(o)) continue; 954 Expr e = TrAnExpr.getEquivalentAxioms(o, null); 955 assumptions.addElement(e); 956 axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded); 957 TrAnExpr.trSpecAuxAxiomsNeeded.clear(); 958 } 959 } 960 961 // FIXME - need to include inherited constraint clauses 962 static public ConditionVec addConstraintClauses(ConditionVec post, 963 /*@ non_null @*/ TypeDecl decl, 964 Hashtable wt, 965 ExprVec postAssumptions) { 966 TypeDeclElemVec pmods = decl.elems; 967 java.util.Set axsToAdd = new java.util.HashSet(); 968 for (int i = 0; i < pmods.size(); ++i) { 969 TypeDeclElem p = pmods.elementAt(i); 970 if (!(p instanceof TypeDeclElemPragma)) continue; 971 if (((TypeDeclElemPragma)p).getTag() != TagConstants.CONSTRAINT) 972 continue; 973 ExprDeclPragma prag = (ExprDeclPragma)p; 974 try { 975 TrAnExpr.initForClause(); 976 Expr pred = TrAnExpr.trSpecExpr(prag.expr, null, wt); 977 if (TrAnExpr.extraSpecs) { 978 postAssumptions.append(TrAnExpr.trSpecExprAuxAssumptions); 979 postAssumptions.append(TrAnExpr.trSpecExprAuxConditions); 980 axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded); 981 TrAnExpr.closeForClause(); 982 } 983 int tag = TagConstants.CHKCONSTRAINT; 984 Condition cond = GC.condition(tag, pred, prag.getStartLoc()); 985 post.addElement(cond); 986 } catch (NotImplementedException e) { 987 TrAnExpr.closeForClause(); 988 } 989 } 990 991 addAxioms(axsToAdd, postAssumptions); 992 return post; 993 } 994 995 //------------------------------------------------------------------------- 996 //------------------------------------------------------------------------- 997 //------------------------------------------------------------------------- 998 999 /** Implements ExtendSpecForCall, section 7.3 of ESCJ 16. */ 1000 1001 //@ ensures \result != null; 1002 private static Spec extendSpecForCall(/*@ non_null */Spec spec, 1003 /*@ non_null */FindContributors scope, 1004 Set predictedSynTargs) 1005 { 1006 // FIXME - I'm not sure that \old variables not in the modifies list get 1007 // translated here 1008 // I think those translations are in scope but not in spec. 1009 // spec.preVarMap contains the modified variables for the current routine 1010 // but it is the preVarMap in the initialState generated from scope that has 1011 // the 1012 // relevant mappings of variables mentioned in \old expressions 1013 1014 // The set of variables modified by *this* GC call: 1015 Set modifiedVars = new Set(spec.preVarMap.keys()); 1016 1017 ParamAndGlobalVarInfo vars = null; 1018 1019 boolean isConstructor = spec.dmd.isConstructor(); 1020 InvariantInfo ii = mergeInvariants(collectInvariants(scope, spec.preVarMap)); 1021 // FIXME - Possibly causes bloated VCs -- I haven't found an example 1022 // yet that needs this, but it seems it ought. 1023 //HashSet axs = collectInvariantsAxsToAdd; 1024 //ExprVec assumptions = addNewAxs(axs,null); 1025 //spec.preAssumptions.append(assumptions); 1026 //spec.postAssumptions.append(assumptions); 1027 1028 for (; ii != null; ii = ii.next) { 1029 1030 int tag = ii.prag.getTag(); 1031 boolean includeInPre = true; 1032 boolean includeInPost = tag != TagConstants.AXIOM; 1033 1034 /* 1035 * Does ii mention a variable that this GC call will modify? 1036 */ 1037 Set invFV = Substitute.freeVars(ii.J); 1038 boolean mentionsModifiedVars = Main.options().useAllInvPostCall 1039 || invFV.containsAny(modifiedVars) || spec.modifiesEverything; 1040 1041 /* 1042 * Does ii mention a variable that the body that is making the GC call 1043 * ever modifies? 1044 */ 1045 boolean falsifiable = true; 1046 if (predictedSynTargs != null || spec.modifiesEverything) { 1047 Assert.notFalse(!Main.options().useAllInvPreBody); 1048 falsifiable = invFV.containsAny(predictedSynTargs); 1049 } 1050 1051 if (ii.isStatic) { 1052 // static invariant 1053 1054 // PRECONDITION for static invariant 1055 Condition cond = GC.condition(TagConstants.CHKOBJECTINVARIANT, ii.J, 1056 ii.prag.getStartLoc()); 1057 if (falsifiable && includeInPre) spec.pre.addElement(cond); 1058 1059 // POSTCONDITION for static invariant 1060 1061 if (mentionsModifiedVars) { 1062 // The free variables of "J" overlap with "synTargs", so add "J" 1063 cond = GC.freeCondition(ii.J, ii.prag.getStartLoc()); 1064 if (includeInPost) spec.post.addElement(cond); 1065 } 1066 1067 } else { 1068 // instance invariant 1069 Assert.notNull(ii.sdecl); 1070 Assert.notNull(ii.s); 1071 1072 if (falsifiable) { 1073 // PRECONDITION for instance invariant 1074 1075 // Gather parameters and static fields, unless already cached 1076 if (vars == null) { 1077 vars = collectParamsAndGlobals(spec, scope); 1078 } 1079 1080 /* 1081 * Without any optimizations, we would generate one precondition here, 1082 * 1083 * p == null || !is(p, trType[[ U ]]) || TrSpecExpr[[ J, {this-->p}, {} ]] 1084 * 1085 * for each parameter or static field "p", where U is the type of this 1086 * in invariant J. 1087 * 1088 * 1089 * Optimizations: 1090 * - First, generate no preconditions for any p such that we can 1091 * prove statically that p cannot have type U at runtime. 1092 * - Second, combine all the remaining preconditions into 1 1093 * universally quantified precondition: 1094 * 1095 * (FORALL s :: (s == p0 || s == p1 || ...) ==> s == null || !is(s, 1096 * trType[[ U ]] || TrSpecExpr[[ J, {this-->p}, {} ]] ) 1097 * 1098 * where "p0", "p1", ... are the parameters and static fields. If the 1099 * list "p0", "p1", ... is empty, don't generate a precondition. 1100 * - Third, if all of the p_i's are "non_null", drop the disjunct "s == 1101 * null". 1102 * - Fourth, if all of the p_i's can be proved to be statically of 1103 * type U, drop the disjunct "!is(s, trType[[ U ]]". 1104 */ 1105 1106 // Build equalities & collect info on which disjuncts to include: 1107 boolean allAreNonnull = true; 1108 boolean allAreOfTypeU = true; 1109 ExprVec alternatives = ExprVec.make(); 1110 1111 for (ParamAndGlobalVarInfo info = vars; info != null; info = info.next) { 1112 if (!Types.isSubclassOf(info.U, ii.U)) { 1113 // p may not always/never hold an object of type U (ii.U) 1114 if (!Types.isSubclassOf(ii.U, info.U)) 1115 // p can never hold an object of type U (ii.U) 1116 continue; 1117 allAreOfTypeU = false; 1118 } 1119 1120 Expr eq = GC.nary(TagConstants.REFEQ, ii.s, TrAnExpr.makeVarAccess( 1121 info.vdecl, Location.NULL)); 1122 alternatives.addElement(eq); 1123 //if (! info.isNonnull) // FIXME 1124 allAreNonnull = false; 1125 } 1126 1127 /* 1128 * -noOutCalls changes this to check *in addition* all non-null 1129 * allocated objects of dynamic type U *except* objectToBeConstructed: 1130 */ 1131 if (Main.options().noOutCalls) { 1132 // isAllocated(ii.s, alloc [in pre-state]) 1133 Expr isAllocated = GC.nary(TagConstants.ISALLOCATED, ii.s, 1134 GC.allocvar); 1135 Expr notEq = GC.nary(TagConstants.REFNE, ii.s, GC.objectTBCvar); 1136 1137 alternatives.addElement(GC.and(isAllocated, notEq)); 1138 allAreNonnull = false; 1139 allAreOfTypeU = false; 1140 } 1141 1142 // build precondition if any alternatives: 1143 if (alternatives.size() != 0) { 1144 Expr ante = GC.or(alternatives); 1145 Expr cons = ii.J; 1146 1147 ExprVec disjuncts = ExprVec.make(); 1148 if (!allAreNonnull) 1149 disjuncts.addElement(GC.nary(TagConstants.REFEQ, ii.s, 1150 GC.nulllit)); 1151 if (!allAreOfTypeU) 1152 disjuncts.addElement(GC.not(GC.nary(TagConstants.IS, ii.s, 1153 TrAnExpr.trType(ii.U)))); 1154 if (disjuncts.size() != 0) { 1155 disjuncts.addElement(cons); 1156 cons = GC.or(disjuncts); 1157 } 1158 1159 Expr quant = GC.forall(ii.sdecl, GC.implies(ante, cons)); 1160 Condition cond = GC.condition(TagConstants.CHKOBJECTINVARIANT, 1161 quant, ii.prag.getStartLoc()); 1162 if (includeInPre) spec.pre.addElement(cond); 1163 } 1164 } 1165 1166 // POSTCONDITION for instance invariant 1167 1168 if (mentionsModifiedVars && includeInPost) { 1169 // TypeCorrectNoallocAs[[ s, U ]] && s != null 1170 ExprVec ev = TrAnExpr.typeAndNonNullAllocCorrectAs(ii.sdecl, ii.U, 1171 null, true, null, false); 1172 ExprVec nopats = ev.copy(); 1173 1174 Expr p = TrAnExpr.trSpecExpr(ii.prag.expr, TrAnExpr.union( 1175 spec.preVarMap, ii.map), null); 1176 if (spec.modifiesEverything) 1177 collectFields(p, spec.postconditionLocations); 1178 if (includeInPre) ev.addElement(p); 1179 1180 Expr ante = GC.and(ev); 1181 Expr impl = GC.implies(ante, ii.J); 1182 1183 spec.post.addElement(GC.freeCondition(GC.forall(ii.sdecl, impl, 1184 nopats), ii.prag.getStartLoc())); 1185 } 1186 } 1187 } 1188 1189 return spec; 1190 } 1191 1192 /** Implements ExtendSpecForBody, section 7.4 of ESCJ 16. */ 1193 1194 //@ ensures \result != null; 1195 private static Spec extendSpecForBody(/*@ non_null */Spec spec, 1196 /*@ non_null */FindContributors scope, 1197 /*@ non_null */Set synTargs) 1198 { 1199 1200 TypeDecl td = spec.dmd.getContainingClass(); 1201 boolean isConstructor = spec.dmd.isConstructor(); 1202 1203 // Add NonNullInit checks 1204 if (isConstructor && !spec.dmd.isConstructorThatCallsSibling()) { 1205 // first check fields in first-inherited interfaces 1206 ClassDecl cd = (ClassDecl)td; 1207 Enumeration inheritedInterfaces = getFirstInheritedInterfaces(cd); 1208 while (inheritedInterfaces.hasMoreElements()) { 1209 TypeDecl tdSuperInterface = (TypeDecl)inheritedInterfaces.nextElement(); 1210 nonNullInitChecks(tdSuperInterface, spec.post); 1211 } 1212 // then check fields in the current class 1213 nonNullInitChecks(td, spec.post); 1214 } 1215 1216 InvariantInfo ii = mergeInvariants(collectInvariants(scope, spec.preVarMap)); 1217 // FIXME - Possibly causing bloated VCs 1218 HashSet axsToAdd = collectInvariantsAxsToAdd; 1219 ExprVec assumptions = addNewAxs(axsToAdd, null); 1220 spec.preAssumptions.append(assumptions); 1221 spec.postAssumptions.append(assumptions); 1222 1223 for (; ii != null; ii = ii.next) { 1224 int tag = ii.prag.getTag(); 1225 addInvariantBody(ii, spec, synTargs); 1226 } 1227 1228 ExprVec axioms = collectAxioms(scope); 1229 1230 for (int i = 0; i < axioms.size(); i++) { 1231 spec.pre.addElement(GC.freeCondition(axioms.elementAt(i), Location.NULL)); 1232 } 1233 1234 // FIXME - possibly causing bloated VCs 1235 for (int i = 0; i < axioms.size(); i++) { 1236 spec.postAssumptions.addElement(axioms.elementAt(i)); 1237 } 1238 1239 return spec; 1240 } 1241 1242 /** 1243 * Add to <code>post</code> all NonNullInit checks for non_null instance 1244 * fields and instance ghost fields declared in <code>td</code>. 1245 */ 1246 private static void nonNullInitChecks(/*@ non_null */TypeDecl td, 1247 /*@ non_null */ConditionVec post) { 1248 TypeDeclElemVec tdes = td.elems; 1249 1250 // check that non_null instance fields have been initialized 1251 for (int i = 0; i < tdes.size(); i++) { 1252 TypeDeclElem tde = tdes.elementAt(i); 1253 FieldDecl fd; 1254 if (tde.getTag() == TagConstants.FIELDDECL) { 1255 fd = (FieldDecl)tde; 1256 } else if (tde.getTag() == TagConstants.GHOSTDECLPRAGMA) { 1257 fd = ((GhostDeclPragma)tde).decl; 1258 } else { 1259 continue; 1260 } 1261 1262 if (!Modifiers.isStatic(fd.modifiers)) { 1263 SimpleModifierPragma smp = NonNullPragma(fd); 1264 if (smp != null) { 1265 // NonNullInit: EC==ecReturn ==> f[RES] != null 1266 1267 Expr left = GC.nary(TagConstants.ANYEQ, GC.ecvar, GC.ec_return); 1268 1269 VariableAccess f = TrAnExpr.makeVarAccess(fd, Location.NULL); 1270 Expr right = GC.nary(TagConstants.REFNE, GC.select(f, GC.resultvar), 1271 GC.nulllit); 1272 Expr pred = GC.implies(left, right); 1273 Condition cond = GC.condition(TagConstants.CHKNONNULLINIT, pred, smp 1274 .getStartLoc()); 1275 post.addElement(cond); 1276 } 1277 } 1278 } 1279 } 1280 1281 //@ ensures \result != null && \result.elementType == \type(InterfaceDecl); 1282 static public Enumeration getFirstInheritedInterfaces( 1283 /*@non_null */ClassDecl cd) { 1284 Set interfaces = new Set(); 1285 addSuperInterfaces(cd, interfaces); 1286 if (interfaces.size() != 0 && cd.superClass != null) { 1287 TypeDecl tdSuper = TypeSig.getSig(cd.superClass).getTypeDecl(); 1288 Set superClassInterfaces = new Set(); 1289 addSuperInterfaces(tdSuper, superClassInterfaces); 1290 Enumeration superClassesInterfaces = superClassInterfaces.elements(); 1291 while (superClassesInterfaces.hasMoreElements()) { 1292 interfaces.remove(superClassesInterfaces.nextElement()); 1293 } 1294 } 1295 return interfaces.elements(); 1296 } 1297 1298 //@ requires set.elementType == \type(InterfaceDecl); 1299 private static void addSuperInterfaces(/*@ non_null */TypeDecl td, 1300 /*@ non_null */Set set) { 1301 if (td instanceof InterfaceDecl) { 1302 set.add(td); 1303 } 1304 // add superinterfaces of "td" 1305 TypeNameVec si = td.superInterfaces; 1306 for (int i = 0; i < si.size(); i++) { 1307 TypeName superName = si.elementAt(i); 1308 TypeDecl superDecl = TypeSig.getSig(superName).getTypeDecl(); 1309 addSuperInterfaces(superDecl, set); 1310 } 1311 } 1312 1313 /** 1314 * Extend <code>spec</code>, in a way appropriate for checking the body of 1315 * a method or constructor, to account for invariant <code>ii.J</code> 1316 * declared in class <code>ii.U</code>. The body to be checked has 1317 * syntactic targets <code>synTargs</code>. 1318 */ 1319 1320 private static void addInvariantBody(/*@ non_null */InvariantInfo ii, 1321 /*@ non_null */Spec spec, 1322 /*@ non_null */Set synTargs) { 1323 1324 Set invFV = Substitute.freeVars(ii.J); 1325 1326 /* 1327 * Include invariant in post only if intersection of vars of invariant and 1328 * vars modified in the method body is nonempty. 1329 */ 1330 // Also include it if we are dealing with a constructor, since then 1331 // the invariant might never have been established. 1332 boolean isConstructor = spec.dmd.isConstructor(); 1333 boolean includeInPre = true; 1334 boolean includeInPostOrig = true; 1335 boolean includeInPost = includeInPostOrig 1336 && (Main.options().useAllInvPostBody || invFV.containsAny(synTargs)); 1337 1338 if (ii.isStatic) { 1339 // static invariant 1340 1341 Condition cond = GC.freeCondition(ii.J, ii.prag.getStartLoc()); 1342 1343 if (includeInPre) spec.pre.addElement(cond); 1344 1345 if (includeInPost) { 1346 cond = GC.condition(TagConstants.CHKOBJECTINVARIANT, ii.J, ii.prag 1347 .getStartLoc()); 1348 spec.post.addElement(cond); 1349 } 1350 1351 } else { 1352 // instance invariant 1353 1354 // Do the precondition 1355 { 1356 // Method, or constructor not declared below: 1357 // (FORALL s :: TypeCorrectNoallocAs[[ s, U ]] && s != null ==> J) 1358 // 1359 // Constructor of a class T, where either 1360 // * U is a subtype of T, and 1361 // either U is not T or the constructor does not call a sibling 1362 // or 1363 // * U is an interface, and 1364 // + m calls sibling constructor and U is not a 1365 // superinterface of T 1366 // or 1367 // + m does not call sibling constructor and U is not a 1368 // superinterface of a proper superclass of T 1369 // (FORALL s :: TypeCorrectNoallocAs[[ s, U ]] && s != null && 1370 // s != objectToBeConstructed 1371 // ==> J) 1372 // 1373 // In either case, NOPATS is the same as the antecedent. 1374 ExprVec ante = TrAnExpr.typeAndNonNullAllocCorrectAs(ii.sdecl, ii.U, 1375 null, true, null, false); 1376 if (spec.dmd.isConstructor()) { 1377 TypeSig tU = ii.U; 1378 TypeSig tT = TypeSig.getSig(spec.dmd.getContainingClass()); 1379 boolean includeAntecedent = false; 1380 if (Types.isSubclassOf(tU, tT)) { 1381 if (!Types.isSameType(tU, tT) 1382 || !spec.dmd.isConstructorThatCallsSibling()) { 1383 includeAntecedent = true; 1384 } 1385 } else if (ii.prag.parent instanceof InterfaceDecl) { 1386 if (spec.dmd.isConstructorThatCallsSibling()) { 1387 if (!Types.isSubclassOf(tT, tU)) { 1388 includeAntecedent = true; 1389 } 1390 } else { 1391 ClassDecl cd = (ClassDecl)spec.dmd.getContainingClass(); 1392 if (!Types.isSubclassOf(TypeSig.getSig(cd.superClass), tU)) { 1393 includeAntecedent = true; 1394 } 1395 } 1396 } 1397 if (includeAntecedent) { 1398 Expr p = GC.nary(TagConstants.REFNE, ii.s, GC.objectTBCvar); 1399 ante.addElement(p); 1400 } 1401 } 1402 Expr body = GC.implies(GC.and(ante), ii.J); 1403 Expr quant = GC.forall(ii.sdecl, body, ante); 1404 Condition cond = GC.freeCondition(quant, ii.prag.getStartLoc()); 1405 if (includeInPre) spec.pre.addElement(cond); 1406 } 1407 1408 // Do the postcondition 1409 1410 // Include the invariant as a checked postcondition if its free variables 1411 // overlap with the syntactic targets of the body (as indicated by the 1412 // current value of "includeInPost"), or if the routine is a constructor 1413 // (that does not call a sibling) of some class "T" and the invariant is 1414 // declared in "T" or in one of "T"'s first-inherited interfaces. 1415 if (!includeInPost && spec.dmd.isConstructor() 1416 && !spec.dmd.isConstructorThatCallsSibling()) { 1417 TypeSig tU = ii.U; 1418 ClassDecl cd = (ClassDecl)spec.dmd.getContainingClass(); 1419 TypeSig tT = TypeSig.getSig(cd); 1420 if (Types.isSubclassOf(tT, tU) 1421 && (cd.superClass == null || !Types.isSubclassOf(TypeSig 1422 .getSig(cd.superClass), tU))) { 1423 // "U" is "T" or a first-inherited interface of "T" 1424 includeInPost = true; 1425 } 1426 } 1427 1428 if (includeInPost && includeInPostOrig) { 1429 // TypeCorrectAs[[ s, U ]] && s != null 1430 ExprVec ante = TrAnExpr.typeAndNonNullAllocCorrectAs(ii.sdecl, ii.U, 1431 null, true, null, true); 1432 1433 if (spec.dmd.isConstructor()) { 1434 TypeSig tU = ii.U; 1435 TypeSig tT = TypeSig.getSig(spec.dmd.getContainingClass()); 1436 if (!Types.isSubclassOf(tT, tU)) { 1437 // "m" is a constructor, and "U" is not a superclass or 1438 // superinterface of "T" 1439 // Add to antecedent the conjunct: s != this 1440 ante.addElement(GC.nary(TagConstants.REFNE, ii.s, GC.thisvar)); 1441 } else if (Types.isSameType(tU, tT) && spec.dmd.throwsSet.size() != 0) { 1442 // "m" is a constructor, and "U" is "T", and throws set is nonempty 1443 // Add to antecedent the conjunct: (EC == ecReturn || s != this) 1444 ante.addElement(GC.or(GC.nary(TagConstants.ANYEQ, GC.ecvar, 1445 GC.ec_return), GC.nary(TagConstants.REFNE, ii.s, GC.thisvar))); 1446 } 1447 } 1448 Expr body = GC.implies(GC.and(ante), ii.J); 1449 Expr quant = GC.forall(ii.sdecl, body); 1450 Condition cond = GC.condition(TagConstants.CHKOBJECTINVARIANT, quant, 1451 ii.prag.getStartLoc()); 1452 spec.post.addElement(cond); 1453 if (Info.on) { 1454 Info.out("[addInvariantBody: Including body-post-invariant at " 1455 + Location.toString(ii.prag.getStartLoc()) + "]"); 1456 } 1457 } else { 1458 if (Info.on) { 1459 Info.out("[addInvariantBody: Skipping body-post-invariant at " 1460 + Location.toString(ii.prag.getStartLoc()) + "]"); 1461 } 1462 } 1463 } 1464 } 1465 1466 /** Collects the axioms in <code>scope</code>. */ 1467 1468 //@ ensures \result != null; 1469 private static ExprVec collectAxioms(/*@ non_null */FindContributors scope) { 1470 1471 ExprVec r = ExprVec.make(); 1472 1473 TrAnExpr.initForClause(); 1474 for (Enumeration typeSigs = scope.typeSigs(); typeSigs.hasMoreElements();) { 1475 1476 TypeDecl td = ((javafe.tc.TypeSig)typeSigs.nextElement()).getTypeDecl(); 1477 1478 for (int i = 0; i < td.elems.size(); i++) { 1479 TypeDeclElem tde = td.elems.elementAt(i); 1480 if (tde.getTag() == TagConstants.AXIOM) { 1481 ExprDeclPragma axiom = (ExprDeclPragma)tde; 1482 if (!Main.options().filterInvariants 1483 || exprIsVisible(scope.originType, axiom.expr)) { 1484 r.addElement(TrAnExpr.trSpecExpr(axiom.expr, null, null)); 1485 } 1486 } 1487 } 1488 1489 TypeDeclElemVec tv = (TypeDeclElemVec)Utils.representsDecoration.get(td); 1490 for (int i = 0; i < tv.size(); ++i) { 1491 TypeDeclElem tde = tv.elementAt(i); 1492 NamedExprDeclPragma p = (NamedExprDeclPragma)tde; 1493 FieldDecl fd = ((FieldAccess)p.target).decl; 1494 Expr e = TrAnExpr.getRepresentsAxiom(p, null); 1495 r.addElement(e); 1496 } 1497 } 1498 1499 TrAnExpr.closeForClause(); 1500 return r; 1501 } 1502 1503 /** 1504 * Gets the represents clauses for a model field fd as seen from a type 1505 * declaration td; fd may be declared in td or in a supertype of td. 1506 * If td is null, then all represents clauses are returned, in any loaded class. 1507 */ 1508 static public TypeDeclElemVec getRepresentsClauses(TypeDecl td, FieldDecl fd) { 1509 if (td == null) return (TypeDeclElemVec)Utils.representsDecoration.get(fd); 1510 TypeDeclElemVec mpv = (TypeDeclElemVec)Utils.representsDecoration.get(td); 1511 TypeDeclElemVec n = TypeDeclElemVec.make(mpv.size()); 1512 for (int i = 0; i < mpv.size(); ++i) { 1513 TypeDeclElem m = mpv.elementAt(i); 1514 if (!(m instanceof NamedExprDeclPragma)) continue; 1515 NamedExprDeclPragma nem = (NamedExprDeclPragma)m; 1516 if (((FieldAccess)nem.target).decl == fd) n.addElement(m); 1517 } 1518 return n; 1519 } 1520 1521 /** Collects the invariants in <code>scope</code>. */ 1522 1523 private static HashSet collectInvariantsAxsToAdd; 1524 1525 private static InvariantInfo collectInvariants( 1526 /*@ non_null */FindContributors scope, Hashtable premap) { 1527 collectInvariantsAxsToAdd = null; 1528 InvariantInfo ii = null; 1529 InvariantInfo iiPrev = null; 1530 1531 Enumeration invariants = scope.invariants(); 1532 try { 1533 TrAnExpr.initForClause(); 1534 while (invariants.hasMoreElements()) { 1535 ExprDeclPragma ep = (ExprDeclPragma)invariants.nextElement(); 1536 Expr J = ep.expr; 1537 1538 boolean Jvisible = !Main.options().filterInvariants 1539 || exprIsVisible(scope.originType, J); 1540 1541 // System.out.print( (Jvisible?"Visible":"Invisible")+": "); 1542 // javafe.ast.PrettyPrint.inst.print(System.out, 0, J ); 1543 // System.out.println(); 1544 1545 if (Jvisible) { 1546 //System.out.println("COLLECTING INVARIANT " + 1547 // Location.toString(ep.getStartLoc())); 1548 1549 // Add a new node at the end of "ii" 1550 InvariantInfo invinfo = new InvariantInfo(); 1551 invinfo.prag = ep; 1552 invinfo.U = TypeSig.getSig(ep.parent); 1553 if (iiPrev == null) 1554 ii = invinfo; 1555 else 1556 iiPrev.next = invinfo; 1557 iiPrev = invinfo; 1558 1559 // The following determines whether or not an invariant is a 1560 // static invariant by, in essence, checking for occurrence 1561 // of "this" in the guarded-command translation of "J", not 1562 // in "J" itself. (These yield different results in the 1563 // unusual case that "J" mentioned "this" in a subexpression 1564 // "E.g", where "g" is a static field.) 1565 // First, build the map "{this-->s}" for a new "s". 1566 1567 LocalVarDecl sdecl = UniqName.newBoundThis(); 1568 VariableAccess s = TrAnExpr.makeVarAccess(sdecl, Location.NULL); 1569 Hashtable map = new Hashtable(); 1570 map.put(GC.thisvar.decl, s); 1571 1572 int cReplacementsBefore = TrAnExpr.getReplacementCount(); 1573 1574 /* 1575 * Unlike any body we may be translating, for these translations 1576 * this's type is that of the type that contains the invariant J. 1577 */ 1578 Type savedType = GC.thisvar.decl.type; 1579 GC.thisvar.decl.type = TypeSig.getSig(ep.getParent()); 1580 1581 invinfo.J = TrAnExpr.trSpecExpr(J, map, null); 1582 if (TrAnExpr.trSpecExprAuxConditions.size() != 0) { 1583 // Use andx here, because the op needs to be and in preconditions 1584 // and 1585 // implies in postconditions 1586 invinfo.J = GC.andx(GC.nary(TagConstants.BOOLAND, 1587 TrAnExpr.trSpecExprAuxConditions), invinfo.J); 1588 TrAnExpr.trSpecExprAuxConditions = ExprVec.make(); 1589 } 1590 GC.thisvar.decl.type = savedType; 1591 1592 if (cReplacementsBefore == TrAnExpr.getReplacementCount()) { 1593 // static invariant 1594 invinfo.isStatic = true; 1595 invinfo.sdecl = null; 1596 invinfo.s = null; 1597 invinfo.map = null; 1598 } else { 1599 invinfo.isStatic = false; 1600 invinfo.sdecl = sdecl; 1601 invinfo.s = s; 1602 invinfo.map = map; 1603 } 1604 //System.out.println("COLLECTING INVARIANT-END " + 1605 // Location.toString(ep.getStartLoc())); 1606 } 1607 } 1608 // FIXME - Possibly causing bloated VCs 1609 collectInvariantsAxsToAdd = new java.util.HashSet(); 1610 collectInvariantsAxsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded); 1611 java.util.Set axsToAdd = new java.util.HashSet(); 1612 //axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded); 1613 java.util.Set axsDone = new java.util.HashSet(); 1614 /* 1615 * while (false && ! axsToAdd.isEmpty()) { // FIXME - keep this off ??? 1616 * RepHelper o = (RepHelper)axsToAdd.iterator().next(); 1617 * axsToAdd.remove(o); if (!axsDone.add(o)) continue; Expr e = 1618 * TrAnExpr.getEquivalentAxioms(o,null); //axsToAdd.addAll( 1619 * TrAnExpr.trSpecAuxAxiomsNeeded); // Add a new node at the end of "ii" 1620 * InvariantInfo invinfo = new InvariantInfo(); invinfo.J = e; 1621 * invinfo.prag = ExprDeclPragma.make(TagConstants.AXIOM, e, 0, 1622 * Location.NULL); // FIXME invinfo.U = TypeSig.getSig(ep.parent); if 1623 * (iiPrev == null) ii = invinfo; else iiPrev.next = invinfo; iiPrev = 1624 * invinfo; if (true ) { //|| cReplacementsBefore == 1625 * TrAnExpr.getReplacementCount()) // FIXME // static invariant 1626 * invinfo.isStatic = true; invinfo.sdecl = null; invinfo.s = null; 1627 * invinfo.map = null; } else { invinfo.isStatic = false; // FIXME 1628 * invinfo.sdecl = sdecl; // FIXME invinfo.s = s; // FIXME invinfo.map = 1629 * map; } } 1630 */ 1631 } finally { 1632 TrAnExpr.closeForClause(); 1633 } 1634 1635 return ii; 1636 } 1637 1638 /** 1639 * Collects the parameters of <code>spec.args</code> and the static fields 1640 * in <code>scope</code>, whose types are class types. 1641 */ 1642 1643 private static ParamAndGlobalVarInfo collectParamsAndGlobals( 1644 /*@ non_null */Spec spec, 1645 /*@ non_null */FindContributors scope) { 1646 ParamAndGlobalVarInfo vars = null; 1647 ParamAndGlobalVarInfo varPrev = null; 1648 1649 // Add the parameters 1650 for (int i = 0; i < spec.dmd.args.size(); i++) { 1651 FormalParaDecl arg = spec.dmd.args.elementAt(i); 1652 TypeSig classSig; 1653 boolean isNonnull; 1654 if (i == 0 && arg == GC.thisvar.decl) { 1655 classSig = TypeSig.getSig(spec.dmd.getContainingClass()); 1656 isNonnull = true; 1657 } else { 1658 classSig = Types.toClassTypeSig(arg.type); 1659 isNonnull = NonNullPragma(arg) != null; 1660 isNonnull = false; // FIXME 1661 } 1662 1663 if (classSig != null) { 1664 // The parameter is of a class type 1665 ParamAndGlobalVarInfo info = new ParamAndGlobalVarInfo(); 1666 if (varPrev == null) 1667 vars = info; 1668 else 1669 varPrev.next = info; 1670 varPrev = info; 1671 1672 info.vdecl = arg; 1673 info.U = classSig; 1674 info.isNonnull = isNonnull; 1675 } 1676 } 1677 1678 // Add the static fields 1679 Enumeration fields = scope.fields(); 1680 while (fields.hasMoreElements()) { 1681 FieldDecl fd = (FieldDecl)fields.nextElement(); 1682 1683 TypeSig classSig = Types.toClassTypeSig(fd.type); 1684 1685 if (classSig != null && Modifiers.isStatic(fd.modifiers)) { 1686 // the field is a static field of a class type 1687 ParamAndGlobalVarInfo info = new ParamAndGlobalVarInfo(); 1688 if (varPrev == null) 1689 vars = info; 1690 else 1691 varPrev.next = info; 1692 varPrev = info; 1693 1694 info.vdecl = fd; 1695 info.U = classSig; 1696 info.isNonnull = NonNullPragma(fd) != null; 1697 } 1698 } 1699 1700 return vars; 1701 } 1702 1703 //@ ensures \result != null; 1704 private static ExprVec addNewAxs(/*@ non_null @*/ HashSet axsToAdd, ExprVec assumptions) { 1705 if (assumptions == null) assumptions = ExprVec.make(); 1706 java.util.Set axsDone = new java.util.HashSet(); 1707 while (!axsToAdd.isEmpty()) { 1708 RepHelper o = (RepHelper)axsToAdd.iterator().next(); 1709 axsToAdd.remove(o); 1710 if (!axsDone.add(o)) continue; 1711 Expr e = TrAnExpr.getEquivalentAxioms(o, null); 1712 assumptions.addElement(e); 1713 axsToAdd.addAll(TrAnExpr.trSpecAuxAxiomsNeeded); 1714 TrAnExpr.trSpecAuxAxiomsNeeded.clear(); 1715 } 1716 return assumptions; 1717 1718 } 1719 1720 /** Shaves a GC designator. */ 1721 1722 private static VariableAccess shave(/*@ non_null */Expr e) { 1723 switch (e.getTag()) { 1724 case TagConstants.VARIABLEACCESS: 1725 return (VariableAccess)e; 1726 1727 case TagConstants.SELECT: 1728 return shave(((NaryExpr)e).exprs.elementAt(0)); 1729 1730 default: 1731 Assert.fail("Unexpected case: " + " " 1732 + TagConstants.toString(e.getTag()) + " " + e + " " 1733 + Location.toString(e.getStartLoc())); 1734 return null; 1735 } 1736 } 1737 1738 /** 1739 * Creates and returns a new map that is <code>map</code> restricted to the 1740 * domain <code>e</code>. Assumes that every element in <code>e</code> is 1741 * in the domain of <code>map</code>. 1742 */ 1743 1744 //+@ requires map.keyType == \type(GenericVarDecl); 1745 //+@ requires map.elementType == \type(VariableAccess); 1746 //+@ requires e.elementType == \type(GenericVarDecl); 1747 //@ ensures \result != null; 1748 static Hashtable restrict(/*@ non_null @*/ Hashtable map, 1749 /*@ non_null @*/ Enumeration e) { 1750 Hashtable r = new Hashtable(); 1751 while (e.hasMoreElements()) { 1752 GenericVarDecl vd = (GenericVarDecl)e.nextElement(); 1753 VariableAccess variant = (VariableAccess)map.get(vd); 1754 Assert.notNull(variant); 1755 r.put(vd, variant); 1756 } 1757 return r; 1758 } 1759 1760 /** 1761 * Converts a GenericVarDecl enumeration to a mapping from those variables to 1762 * new Variableaccesses. 1763 */ 1764 1765 //@ requires e.elementType == \type(GenericVarDecl); 1766 //@ ensures \result != null; 1767 static Hashtable makeSubst(/*@ non_null */Enumeration e, 1768 /*@ non_null */String postfix) { 1769 Hashtable r = new Hashtable(); 1770 while (e.hasMoreElements()) { 1771 GenericVarDecl vd = (GenericVarDecl)e.nextElement(); 1772 VariableAccess variant = createVarVariant(vd, postfix); 1773 r.put(vd, variant); 1774 } 1775 return r; 1776 } 1777 1778 //@ ensures \result != null; 1779 static Hashtable makeSubst(/*@ non_null */FormalParaDeclVec args, 1780 /*@ non_null */String postfix) { 1781 Hashtable r = new Hashtable(); 1782 for (int i = 0; i < args.size(); i++) { 1783 GenericVarDecl vd = args.elementAt(i); 1784 VariableAccess variant = createVarVariant(vd, postfix); 1785 r.put(vd, variant); 1786 } 1787 return r; 1788 } 1789 1790 /** 1791 * * Given a GenericVarDecl named "x@old", returns a VariableAccess to a * 1792 * fresh LocalVarDecl named "x@ <postfix>". * * This handles ESCJ 23b case 13. 1793 */ 1794 //@ ensures \result != null; 1795 static VariableAccess createVarVariant(/*@ non_null */GenericVarDecl vd, 1796 /*@ non_null */String postfix) 1797 { 1798 String name = vd.id.toString(); 1799 if (name.indexOf('@') != -1) name = name.substring(0, name.indexOf('@')); 1800 1801 Identifier id = Identifier.intern(name + "@" + postfix); 1802 LocalVarDecl ld = LocalVarDecl.make(vd.modifiers, vd.pmodifiers, id, 1803 vd.type, vd.locId, null, Location.NULL); 1804 VariableAccess va = VariableAccess.make(id, vd.locId, ld); 1805 1806 return va; 1807 } 1808 1809 /** 1810 * Adds to <code>cv</code> a condition stating that <code>vd</code> has 1811 * type <code>type</code>. 1812 */ 1813 1814 private static void addFreeTypeCorrectAs(GenericVarDecl vd, Type type, 1815 /*@ non_null @*/ ConditionVec cv) { 1816 Expr e = TrAnExpr.typeCorrectAs(vd, type); 1817 Condition cond = GC.freeCondition(e, Location.NULL); 1818 cv.addElement(cond); 1819 } 1820 1821 /** 1822 * Returns a command that first does an <code>assume</code> for each 1823 * precondition in <code>spec</code>, then does <code>body</code>, then 1824 * checks the postconditions of <code>spec</code>, and finally checks the 1825 * modifies constraints implied by <code>spec</code>. 1826 */ 1827 1828 public static GuardedCmd surroundBodyBySpec(GuardedCmd body, 1829 /*@ non_null @*/ Spec spec, 1830 FindContributors scope, 1831 Set syntargets, 1832 Hashtable premap, 1833 int locEndCurlyBrace) 1834 { 1835 StackVector code = new StackVector(); 1836 code.push(); 1837 1838 addAssumptions(spec.preAssumptions, code); 1839 assumeConditions(spec.pre, code); 1840 code.addElement(body); 1841 addAssumptions(spec.postAssumptions, code); 1842 checkConditions(spec.post, locEndCurlyBrace, code); 1843 checkModifiesConstraints(spec, scope, syntargets, premap, locEndCurlyBrace, 1844 code); 1845 1846 return GC.seq(GuardedCmdVec.popFromStackVector(code)); 1847 } 1848 1849 /** 1850 * Appends <code>code</code> with an <code>assume C</code> command for 1851 * every condition <code>C</code> in <code>cv</code>. 1852 */ 1853 1854 private static void addAssumptions(/*@ non_null @*/ ExprVec ev, 1855 /*@ non_null @*/ StackVector code) 1856 { 1857 for (int i = 0; i < ev.size(); i++) { 1858 Expr e = ev.elementAt(i); 1859 code.addElement(GC.assume(e)); 1860 //code.addElement(GC.check(e.getStartLoc(),TagConstants.CHKCONSISTENT,e,e.getStartLoc(),null)); 1861 } 1862 } 1863 1864 private static void assumeConditions(/*@ non_null @*/ ConditionVec cv, 1865 /*@ non_null @*/ StackVector code) 1866 { 1867 for (int i = 0; i < cv.size(); i++) { 1868 Condition cond = cv.elementAt(i); 1869 code.addElement(GC.assumeAnnotation(cond.locPragmaDecl, cond.pred)); 1870 } 1871 } 1872 1873 /** 1874 * Appends <code>code</code> with an <code>check loc: C</code> command for 1875 * every condition <code>C</code> in <code>cv</code>. 1876 */ 1877 1878 private static void checkConditions(/*@ non_null @*/ ConditionVec cv, 1879 int loc, 1880 StackVector code) 1881 { 1882 for (int i = 0; i < cv.size(); i++) { 1883 Condition cond = cv.elementAt(i); 1884 if (cond.label == TagConstants.CHKUNEXPECTEDEXCEPTION2) continue; 1885 Translate.setop(cond.pred); 1886 // if the condition is an object invariant, send its guarded command 1887 // translation as auxiliary info to GC.check 1888 if (cond.label == TagConstants.CHKOBJECTINVARIANT) 1889 code.addElement(GC.check(loc, cond, cond.pred)); 1890 else 1891 code.addElement(GC.check(loc, cond)); 1892 } 1893 } 1894 1895 private static void checkModifiesConstraints(Spec spec, 1896 FindContributors scope, Set syntargets, Hashtable premap, int loc, 1897 StackVector code) { 1898 // TBW 1899 } 1900 1901 private static InvariantInfo mergeInvariants(InvariantInfo ii) { 1902 if (!Main.options().mergeInv) return ii; 1903 1904 // Combined static/dynamic invariants, indexed by TypeSIg 1905 Hashtable staticInvs = new Hashtable(); 1906 Hashtable dynInvs = new Hashtable(); 1907 1908 while (ii != null) { 1909 1910 Hashtable table = ii.isStatic ? staticInvs : dynInvs; 1911 1912 InvariantInfo old = (InvariantInfo)table.get(ii.U); 1913 1914 if (old == null) { 1915 1916 table.put(ii.U, ii); 1917 1918 } else { 1919 1920 // Add ii to old 1921 old.J = GC.and(old.J, ii.isStatic ? ii.J : GC.subst(ii.sdecl, old.s, 1922 ii.J)); 1923 } 1924 1925 ii = ii.next; 1926 } 1927 1928 // Now pull out merged invariants from tables 1929 Hashtable[] tables = {staticInvs, dynInvs}; 1930 ii = null; 1931 1932 for (int i = 0; i < 2; i++) { 1933 Hashtable table = tables[i]; 1934 1935 for (Enumeration e = table.elements(); e.hasMoreElements();) { 1936 InvariantInfo t = (InvariantInfo)e.nextElement(); 1937 t.next = ii; 1938 ii = t; 1939 } 1940 } 1941 1942 return ii; 1943 } 1944 1945 private static boolean exprIsVisible(TypeSig originType, 1946 /*@ non_null @*/ Expr e) { 1947 1948 switch (e.getTag()) { 1949 1950 case TagConstants.FIELDACCESS: { 1951 FieldAccess fa = (FieldAccess)e; 1952 FieldDecl decl = fa.decl; 1953 1954 if (fa.od instanceof ExprObjectDesignator 1955 && !exprIsVisible(originType, ((ExprObjectDesignator)fa.od).expr)) 1956 return false; 1957 1958 if (decl.parent == null) { 1959 // for array.length "field", there is no parent 1960 return true; 1961 } else if (Utils.findModifierPragma(decl, TagConstants.SPEC_PUBLIC) != null) { 1962 return true; 1963 } else { 1964 TypeSig sigDecl = TypeSig.getSig(decl.parent); 1965 return TypeCheck.inst.canAccess(originType, sigDecl, decl.modifiers, 1966 decl.pmodifiers); 1967 } 1968 } 1969 1970 default: { 1971 // Recurse over all children 1972 for (int i = 0; i < e.childCount(); i++) { 1973 Object o = e.childAt(i); 1974 if (o instanceof Expr) { 1975 if (!exprIsVisible(originType, (Expr)o)) return false; 1976 } 1977 } 1978 1979 return true; 1980 } 1981 } 1982 } 1983 1984 static public void collectFields(/*@ non_null @*/ Expr e, java.util.Set s) { 1985 // FIXME - have to avoid collecting bound variables of quantifiers 1986 switch (e.getTag()) { 1987 case TagConstants.PRE: 1988 return; 1989 case TagConstants.VARIABLEACCESS: 1990 VariableAccess va = (VariableAccess)e; 1991 if (va.decl instanceof FormalParaDecl) { 1992 //System.out.println("PARA " + ((VariableAccess)e).decl ); 1993 return; 1994 } 1995 if (va.id.toString().endsWith("@pre")) return; 1996 //System.out.println("COLLECTED-VA " + e); 1997 s.add(e); 1998 break; 1999 default: 2000 } 2001 2002 // Recurse over all children 2003 for (int i = 0; i < e.childCount(); i++) { 2004 Object o = e.childAt(i); 2005 if (o instanceof Expr) collectFields((Expr)o, s); 2006 } 2007 2008 } 2009 2010 /***************************************************************************** 2011 * * Handling NON_NULL: * * 2012 ****************************************************************************/ 2013 2014 /** 2015 * * Decorates <code>GenericVarDecl</code>'s to point to * NonNullPragmas 2016 * (SimpleModifierPragma's). 2017 */ 2018 //@ invariant nonnullDecoration != null; 2019 // FIXME @ invariant nonnullDecoration.decorationType == 2020 // FIXME @ \type(SimpleModifierPragma); 2021 /*@ spec_public */ 2022 private static ASTDecoration nonnullDecoration = new ASTDecoration( 2023 "nonnullDecoration"); 2024 2025 /** 2026 * * Mark v as non_null because of non_null pragma nonnull. * * Precondition: 2027 * nonnull is a NON_NULL pragma. * * (Used to implement inheritence of 2028 * non_null's.) 2029 */ 2030 private static void setNonNullPragma(GenericVarDecl v, 2031 SimpleModifierPragma nonnull) { 2032 nonnullDecoration.set(v, nonnull); 2033 } 2034 2035 /** 2036 * * Has a particular declaration been declared non_null? If so, * return the 2037 * non_null pragma responsible. Otherwise, return null. 2038 * <p>* * Precondition: if the declaration is a formal parameter, then the * 2039 * spec of it's routine has already been computed. 2040 * <p>* * * WARNING: this is the only authorized way to determine this * 2041 * information. Do *not* attempt to search for NON_NULL modifiers * directly. 2042 * (This is needed to handle inherited NON_NULL's * properly.) 2043 */ 2044 public static SimpleModifierPragma NonNullPragma(GenericVarDecl v) { 2045 // First check for a mark: 2046 /* 2047 * In JML, non_null pragmas do not inherit! SimpleModifierPragma mark = 2048 * (SimpleModifierPragma) nonnullDecoration.get(v); if (mark != null) return 2049 * mark; 2050 */ 2051 2052 // Else fall back on a direct search of local modifiers: 2053 return (SimpleModifierPragma)Utils.findModifierPragma(v, 2054 TagConstants.NON_NULL); 2055 } 2056 2057 /** 2058 * Returns non-null if the formal parameter is declared non-null in some 2059 * overridden declaration of the method. 2060 */ 2061 public static SimpleModifierPragma superNonNullPragma(GenericVarDecl v) { 2062 // First check for a mark: 2063 SimpleModifierPragma mark = (SimpleModifierPragma)nonnullDecoration.get(v); 2064 return mark; 2065 } 2066 2067 } 2068 2069 /** 2070 * * This class is used by <code>collectInvariants</code> and its callers, * 2071 * <code>extendSpecForCall</code> and <code>extendSpecForBody</code>. 2072 */ 2073 2074 class InvariantInfo { 2075 2076 ExprDeclPragma prag; 2077 2078 TypeSig U; // "TypeSig" of class or interface that contains "prag" 2079 2080 boolean isStatic; // "true" if pragma declares a static invariant 2081 2082 LocalVarDecl sdecl; // "null" if "isStatic"; otherwise, a dummy variable 2083 2084 VariableAccess s; // "null" if "isStatic"; otherwise, a variable access 2085 2086 // of "sdecl" 2087 Hashtable map; // "{this-->s}" 2088 2089 Expr J; // translated expression, with substitution 2090 2091 // "{this-->s}" if not "isStatic" 2092 InvariantInfo next; // for linking "InvariantInfo" nodes 2093 } 2094 2095 /** 2096 * This class is used by <code>collectParamsAndGlobalVars</code> and its * 2097 * caller, <code>extendSpecForCall</code>. 2098 */ 2099 2100 class ParamAndGlobalVarInfo { 2101 2102 GenericVarDecl vdecl; 2103 2104 TypeSig U; 2105 2106 boolean isNonnull; 2107 2108 ParamAndGlobalVarInfo next; 2109 } 2110