001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package escjava.tc; 004 005 import java.util.Enumeration; 006 007 import javafe.ast.*; 008 009 import javafe.tc.Env; 010 import javafe.tc.EnvForLocals; 011 import javafe.tc.EnvForTypeSig; 012 import javafe.tc.LookupException; 013 import javafe.tc.TypeSig; 014 015 import javafe.util.*; 016 017 import escjava.ast.*; 018 import escjava.ast.Modifiers; 019 import escjava.ast.TagConstants; 020 import escjava.tc.Types; 021 import escjava.Main; 022 023 public class FlowInsensitiveChecks extends javafe.tc.FlowInsensitiveChecks 024 { 025 static { 026 inst = new FlowInsensitiveChecks(); 027 } 028 static public javafe.tc.FlowInsensitiveChecks inst() { return inst; } 029 030 // Setup for ghost variables 031 032 /** 033 * Are we in the middle of processing an annotation? (Used by {@link GhostEnv}.) 034 */ 035 public static boolean inAnnotation = false; 036 public static boolean inModelBody = false; 037 // FIXME - the above two variables are a hack! Note that below we have to save and 038 // restore their values so that the appropriate values are read out of these 039 // global-static variables by GhostEnv. It would be much better to create a sub 040 // Env that understands what to do and pass that along for the checks. -- DRCok 041 042 public escjava.AnnotationHandler annotationHandler = 043 new escjava.AnnotationHandler(); 044 /** 045 * Indicates whether <code>LS</code> is allowed in this context. The default is 046 * <code>true</code>. For contexts where <code>LS</code> is not allowed, 047 * <code>isLocksetContext</code> should be set <code>false</code> only temporarily. 048 */ 049 protected boolean isLocksetContext = true; 050 051 /** 052 * <code>\result</code> is allowed in this context when <code>isRESContext</code> 053 * is <code>true</code> and <code>returnType != null</code>. The default value 054 * of <code>isRESContext</code> is <code>false</code>. For contexts where 055 * <code>isRESContext</code> should be <code>true</code>, 056 * <code>isRESContext</code> should be set to <code>true</code> only temporarily. 057 */ 058 protected boolean isRESContext = false; 059 060 /** 061 * Indicates whether <code>\old</code> and <code>\fresh</code> are allowed in 062 * this context. The default is <code>false</code>. For contexts where these 063 * functions are allowed, <code>isTwoStateContext</code> should be set 064 * <code>true</code> only temporarily. 065 */ 066 protected boolean isTwoStateContext = false; 067 068 /** 069 * Indicates whether checking is currently being done inside a <code>PRE</code>. 070 * This is used by the code that disallows nested <code>PRE</code> expressions. 071 * Note: alternatively, one could use <code>isTwoStateContext</code> to implement 072 * this functionality, but by having a separate bit, a more precise error message 073 * can be produced. 074 */ 075 protected boolean isInsidePRE = false; 076 077 /** 078 * Indicates whether a quantification or labeled predicate is allowed in this 079 * context. This boolean is used only between one call of <code>checkExpr</code> 080 * to a following recursive call. 081 */ 082 protected boolean isPredicateContext = false; 083 084 /** 085 * Indicates whether private field accesses are allowed in the current context. 086 * Private field accesses are allowed everywhere, except in postconditions of 087 * overridable methods. 088 */ 089 protected boolean isPrivateFieldAccessAllowed = true; 090 091 protected int accessibilityLowerBound = ACC_LOW_BOUND_Private; 092 // Note, "ACC_LOW_BOUND_Private" would be the same as "no lower bound" 093 protected static final int ACC_LOW_BOUND_Private = 0; 094 protected static final int ACC_LOW_BOUND_Package = 1; 095 protected static final int ACC_LOW_BOUND_Protected = 2; 096 protected static final int ACC_LOW_BOUND_Public = 3; 097 098 /** 099 * If <code>accessibilityLowerBound != ACC_LOW_BOUND_Private</code>, then 100 * <code>accessibilityContext</code> is the field or routine whose modifier 101 * pragma is being type checked. 102 */ 103 /*@ invariant accessibilityContext == null || 104 @ accessibilityContext instanceof FieldDecl || 105 @ accessibilityContext instanceof RoutineDecl; 106 */ 107 //@ readable accessibilityContext if accessibilityLowerBound != ACC_LOW_BOUND_Private; 108 protected ASTNode accessibilityContext; 109 110 /** 111 * Acts as a parameter to <code>checkExpr</code>. Its value is meaningful only 112 * on entry to <code>checkExpr</code>. It indicates whether the expression to be 113 * checked is in a specification designator context. In particular, this 114 * parameter is used to disallow array index wild cards in non-spec designator 115 * contexts. 116 */ 117 protected boolean isSpecDesignatorContext = false; 118 119 /** 120 * Contains the loop invariant statement pragmas seen so far and not yet 121 * processed. 122 */ 123 protected ExprStmtPragmaVec loopInvariants = ExprStmtPragmaVec.make(); 124 125 /** 126 * Contains the loop decreases statement pragmas seen so far and not yet 127 * processed. 128 */ 129 protected ExprStmtPragmaVec loopDecreases = ExprStmtPragmaVec.make(); 130 131 protected ExprStmtPragmaVec loopPredicates = ExprStmtPragmaVec.make(); 132 133 protected LocalVarDeclVec skolemConstants = LocalVarDeclVec.make(); 134 135 /** 136 * Indicates whether we are are checking an invariant pragma. 137 */ 138 protected boolean invariantContext = false; 139 140 /** 141 * Counts the number of accesses of free variables and fields used for checking 142 * the appropriateness of invariants. 143 */ 144 //@ readable countFreeVarsAccesses if invariantContext; 145 protected int countFreeVarsAccesses = 0 ; 146 147 /** 148 * Override so that we use {@link GhostEnv} instead of {@link EnvForTypeSig}. 149 */ 150 protected EnvForTypeSig makeEnvForTypeSig(TypeSig s, 151 boolean staticContext) { 152 return new GhostEnv(s.getEnclosingEnv(), s, staticContext); 153 } 154 155 public static ASTDecoration envDecoration = 156 new ASTDecoration("env"); 157 public static ASTDecoration staticenvDecoration = 158 new ASTDecoration("staticenv"); 159 160 public void checkTypeDeclaration(/*@ non_null */ TypeSig s) { 161 super.checkTypeDeclaration(s); 162 TypeDecl td = s.getTypeDecl(); 163 envDecoration.set(td,rootIEnv); 164 staticenvDecoration.set(td,rootSEnv); 165 } 166 167 // Extensions to type declaration member checkers. 168 169 protected void checkTypeDeclElem(TypeDeclElem e) { 170 boolean savedInAnnotation = inAnnotation; 171 boolean savedInModelBody = inModelBody; 172 // FIXME - should this use Utils.isModel ??? 173 if (e instanceof ConstructorDecl && 174 null != Utils.findModifierPragma(((ConstructorDecl)e).pmodifiers,TagConstants.MODEL)) { 175 inAnnotation = true; 176 inModelBody = true; 177 } 178 if (e instanceof MethodDecl && 179 null != Utils.findModifierPragma(((MethodDecl)e).pmodifiers,TagConstants.MODEL)) { 180 inAnnotation = true; 181 inModelBody = true; 182 } 183 try { 184 super.checkTypeDeclElem(e); 185 if (e instanceof RoutineDecl) { 186 // Desugaring presumes that typechecking has already 187 // been performed 188 RoutineDecl m = (RoutineDecl)e; 189 /* 190 if ((m instanceof ConstructorDecl) && m.implicit) { 191 // The desugaring of m can require the desugared 192 // specs of a parent constructor, so we have to be 193 // sure that the parent constructor is typechecked. 194 TypeSig s = TypeSig.getSig(m.parent).superClass(); 195 if (s != null) checkTypeDeclElem(s.getTypeDecl()); 196 } 197 */ 198 /* 199 if (m.originalRaises != null && 200 m.originalRaises.size() != m.raises.size()) { 201 202 for (int i=m.originalRaises.size()+1; i < m.raises.size(); ++i) { 203 204 TypeSig t = TypeSig.getSig(m.raises.elementAt(i)); 205 System.out.println("FOUND " + t); 206 if (!t.isSubtypeOf(Types.javaLangRuntimeException())) { 207 ErrorSet.error(m.raises.elementAt(i).getStartLoc(), 208 "The type " + t + " is not a subtype of " + 209 "RuntimeException and is not declared by the API, and " + 210 "consequently may not be declared in a specification."); 211 System.out.println("BAD"); 212 } 213 } 214 } 215 */ 216 annotationHandler.desugar(m); 217 } 218 } finally { 219 inAnnotation = savedInAnnotation; 220 inModelBody = savedInModelBody; 221 } 222 223 // Do a separate set of checks - purity checking 224 // FIXME - perhaps these should be moved into this routine 225 annotationHandler.process(e); 226 227 if (e.getTag() == TagConstants.INITBLOCK) { 228 InitBlock ib = (InitBlock)e; 229 if (ib.pmodifiers != null) { 230 checkModifierPragmaVec(ib.pmodifiers,ib, 231 Modifiers.isStatic(ib.modifiers) ? rootSEnv : rootIEnv); 232 /* 233 for (int i = 0; i < ib.pmodifiers.size(); i++) { 234 ModifierPragma mp = (ModifierPragma)ib.pmodifiers.elementAt(i); 235 ErrorSet.error(mp.getStartLoc(), 236 TagConstants.toString(mp.getTag()) + 237 " pragma cannot be applied to initializer block"); 238 } 239 */ 240 } 241 } 242 243 } 244 245 // Extensions to Expr and Stmt checkers. 246 247 protected Env checkStmt(Env env, Stmt s) { 248 boolean savedTwoStateContext = isTwoStateContext; 249 isTwoStateContext = true; 250 try { 251 int tag = s.getTag(); 252 253 // Check for any loop invariants, loop bounds, loop predicates, or skolem 254 // constants in the wrong place 255 if (loopInvariants.size() != 0 || 256 loopDecreases.size() != 0 || 257 loopPredicates.size() != 0 || 258 skolemConstants.size() != 0) { 259 switch (tag) { 260 case TagConstants.DOSTMT: 261 case TagConstants.WHILESTMT: 262 case TagConstants.FORSTMT: 263 case TagConstants.LABELSTMT: 264 case TagConstants.LOOP_INVARIANT: 265 case TagConstants.MAINTAINING: 266 case TagConstants.DECREASES: 267 case TagConstants.DECREASING: 268 case TagConstants.LOOP_PREDICATE: 269 case TagConstants.SKOLEMCONSTANTPRAGMA: 270 break; 271 default: 272 checkLoopInvariants(env, false); 273 checkLoopDecreases(env, false); 274 checkLoopPredicates(env, false); 275 checkSkolemConstants(env, false); 276 break; 277 } 278 } 279 280 switch(tag) { 281 case TagConstants.DOSTMT: 282 case TagConstants.WHILESTMT: { 283 checkLoopInvariants(env, true); 284 checkLoopDecreases(env, true); 285 Env newEnv = checkSkolemConstants(env, true); 286 checkLoopPredicates(newEnv, true); 287 super.checkStmt(env, s); 288 break; 289 } 290 case TagConstants.FORSTMT: { 291 ForStmt f = (ForStmt)s; 292 293 ExprStmtPragmaVec invs = loopInvariants; 294 ExprStmtPragmaVec decrs = loopDecreases; 295 ExprStmtPragmaVec preds = loopPredicates; 296 LocalVarDeclVec skolemConsts = skolemConstants; 297 298 loopInvariants = ExprStmtPragmaVec.make(); 299 loopDecreases = ExprStmtPragmaVec.make(); 300 loopPredicates = ExprStmtPragmaVec.make(); 301 skolemConstants = LocalVarDeclVec.make(); 302 303 Env se = checkStmtVec(env, f.forInit); 304 305 Assert.notFalse(loopInvariants.size() == 0); 306 Assert.notFalse(loopDecreases.size() == 0); 307 Assert.notFalse(loopPredicates.size() == 0); 308 Assert.notFalse(skolemConstants.size() == 0); 309 310 loopInvariants = invs; 311 loopDecreases = decrs; 312 loopPredicates = preds; 313 skolemConstants = skolemConsts; 314 315 checkLoopInvariants(se, true); 316 checkLoopDecreases(se, true); 317 Env newEnv = checkSkolemConstants(se, true); 318 checkLoopPredicates(newEnv, true); 319 checkForLoopAfterInit(se, f); 320 break; 321 } 322 case TagConstants.BLOCKSTMT: { 323 env = super.checkStmt(env, s); 324 // Check for any loop_invariant statement pragmas at the end of the 325 // body. 326 checkLoopInvariants(env, false); 327 checkLoopDecreases(env, false); 328 checkLoopPredicates(env, false); 329 checkSkolemConstants(env, false); 330 break; 331 } 332 case TagConstants.VARDECLSTMT: { 333 VarDeclStmt vs = (VarDeclStmt)s; 334 LocalVarDecl x = vs.decl; 335 if (Utils.findModifierPragma(x.pmodifiers, 336 TagConstants.GHOST) != null) { 337 boolean savedInAnnotation = inAnnotation; 338 inAnnotation = true; 339 try { 340 env.resolveType(sig, x.type); 341 checkTypeModifiers(env, x.type); 342 javafe.tc.PrepTypeDeclaration.inst. 343 checkModifiers(x.modifiers, Modifiers.ACC_FINAL, 344 x.locId, "local ghost variable"); 345 checkModifierPragmaVec(x.pmodifiers, x, env); 346 347 Env newEnv = new EnvForGhostLocals(env,x); 348 if (x.init != null) 349 x.init = checkInit(newEnv, x.init, x.type); 350 env = newEnv; 351 } finally { 352 inAnnotation = savedInAnnotation; 353 } 354 break; 355 } 356 357 env = super.checkStmt(env, s); 358 break; 359 360 } 361 case TagConstants.CLASSDECLSTMT: { 362 ClassDeclStmt cds = (ClassDeclStmt)s; 363 ClassDecl cd = cds.decl; 364 (new escjava.AnnotationHandler.NestedPragmaParser()).parseAllRoutineSpecs(cd); 365 env = super.checkStmt(env, s); 366 annotationHandler.desugar(cd); 367 break; 368 } 369 default: 370 env = super.checkStmt(env, s); 371 break; 372 } 373 374 } finally { 375 isTwoStateContext = savedTwoStateContext; 376 } 377 return env; 378 } 379 380 protected void checkLoopInvariants(Env env, boolean allowed) { 381 for (int i = 0; i < loopInvariants.size(); i++) { 382 ExprStmtPragma s = loopInvariants.elementAt(i); 383 Assert.notFalse(s.getTag() == TagConstants.LOOP_INVARIANT 384 || s.getTag() == TagConstants.MAINTAINING); 385 if (allowed) { 386 //Assert.notFalse(!isTwoStateContext); 387 Assert.notFalse(!inAnnotation || inModelBody); 388 boolean savedInAnnotation = inAnnotation; 389 inAnnotation = true; 390 //isTwoStateContext = true; 391 try { 392 s.expr = checkPredicate(env, s.expr); 393 } finally { 394 inAnnotation = savedInAnnotation; 395 //isTwoStateContext = false; 396 } 397 } else { 398 errorExpectingLoop(s.getStartLoc(), TagConstants.LOOP_INVARIANT); 399 } 400 } 401 loopInvariants.removeAllElements(); 402 } 403 404 protected void checkLoopDecreases(Env env, boolean allowed) { 405 for (int i = 0; i < loopDecreases.size(); i++) { 406 ExprStmtPragma s = loopDecreases.elementAt(i); 407 Assert.notFalse(s.getTag() == TagConstants.DECREASES 408 || s.getTag() == TagConstants.DECREASING); 409 if (allowed) { 410 //Assert.notFalse(!isTwoStateContext); 411 Assert.notFalse(!inAnnotation || inModelBody); 412 boolean savedInAnnotation = inAnnotation; 413 inAnnotation = true; 414 try { 415 s.expr = checkExpr(env, s.expr, Types.bigintType); 416 } finally { 417 inAnnotation = savedInAnnotation; 418 } 419 } else { 420 errorExpectingLoop(s.getStartLoc(), TagConstants.DECREASES); 421 } 422 } 423 loopDecreases.removeAllElements(); 424 } 425 426 protected void checkLoopPredicates(Env env, boolean allowed) { 427 for (int i = 0; i < loopPredicates.size(); i++) { 428 ExprStmtPragma s = loopPredicates.elementAt(i); 429 Assert.notFalse(s.getTag() == TagConstants.LOOP_PREDICATE); 430 if (allowed) { 431 //Assert.notFalse(!isTwoStateContext); 432 Assert.notFalse(!inAnnotation || inModelBody); 433 boolean savedInAnnotation = inAnnotation; 434 inAnnotation = true; 435 //isTwoStateContext = true; 436 try { 437 s.expr = checkPredicate(env, s.expr); 438 } finally { 439 inAnnotation = savedInAnnotation; 440 //isTwoStateContext = false; 441 } 442 } else { 443 errorExpectingLoop(s.getStartLoc(), TagConstants.LOOP_PREDICATE); 444 } 445 } 446 loopPredicates.removeAllElements(); 447 } 448 449 protected Env checkSkolemConstants(Env env, boolean allowed) { 450 for (int i = 0; i < skolemConstants.size(); i++) { 451 LocalVarDecl s = skolemConstants.elementAt(i); 452 if (allowed) { 453 //Assert.notFalse(!isTwoStateContext); 454 Assert.notFalse(!inAnnotation || inModelBody); 455 boolean savedInAnnotation = inAnnotation; 456 inAnnotation = true; 457 //isTwoStateContext = true; 458 try { 459 env.resolveType(sig, s.type); 460 env = new EnvForLocals(env, s); 461 } finally { 462 inAnnotation = savedInAnnotation; 463 //isTwoStateContext = false; 464 } 465 } else { 466 errorExpectingLoop(s.getStartLoc(), TagConstants.SKOLEM_CONSTANT); 467 } 468 } 469 skolemConstants.removeAllElements(); 470 return env; 471 } 472 473 private void errorExpectingLoop(int loc, int tag) { 474 ErrorSet.error(loc, "'" + TagConstants.toString(tag) + 475 "' pragmas can occur " + 476 "only immediately prior to a loop statement. Loop " + 477 "statement expected (and not found) here."); 478 } 479 480 protected Expr checkPredicate(Env env, Expr e) { 481 boolean savedPredicateContext = isPredicateContext; 482 isPredicateContext = true; 483 Expr ee = checkExpr(env, e, Types.booleanType); 484 isPredicateContext = savedPredicateContext; 485 return ee; 486 } 487 488 //@ also requires e != null; 489 protected Expr checkExpr(Env env, Expr e) { 490 // Anticipate that the next context is probably not one suitable for 491 // quantifications and labels. "isPredicateContext" must revert to its old 492 // value before return. 493 boolean isCurrentlyPredicateContext = isPredicateContext; 494 isPredicateContext = false; 495 496 try { 497 498 if (getTypeOrNull(e) != null ) 499 // already done 500 return e; 501 502 // No recursive call to "checkExpr" is a specification designator context, so 503 // set "isSpecDesignatorContext" to "false", keeping the initial value in 504 // local variable "isCurrentlySpecDesignatorContext". 505 boolean isCurrentlySpecDesignatorContext = isSpecDesignatorContext; 506 isSpecDesignatorContext = false; 507 508 int tag = e.getTag(); 509 switch(tag) { 510 511 // Handle accesses to ghost fields as well... 512 case TagConstants.FIELDACCESS: 513 { 514 if (!inAnnotation) 515 return super.checkExpr(env, e); 516 517 // a field access is considerded a free variable access in an 518 // invariant. 519 if (invariantContext) countFreeVarsAccesses++; 520 521 // set default result type to errorType, in case there is an error. 522 setType( e, Types.errorType ); 523 FieldAccess fa = (FieldAccess)e; 524 Type t = checkObjectDesignator(env, fa.od); 525 if (t==null) 526 return fa; 527 if (t instanceof TypeName) 528 t = TypeSig.getSig( (TypeName) t ); 529 530 if (Types.isErrorType(t)) { 531 setType( fa, Types.errorType ); 532 return fa; 533 } 534 535 try { 536 fa.decl = escjava.tc.Types.lookupField( t, fa.id, sig ); 537 } catch( LookupException ex) { 538 if (!Types.isErrorType(t)) 539 reportLookupException(ex, "field", 540 Types.printName(t), fa.locId); 541 setType( fa, Types.errorType ); 542 return fa; 543 } 544 setType( fa, fa.decl.type ); 545 546 if (fa.od instanceof TypeObjectDesignator && 547 !GhostEnv.isStatic(fa.decl)) { 548 // Is fa.decl an instance field of the same class as fa is 549 // part of? 550 boolean thisField = false; 551 if (fa.decl.parent != null) 552 thisField = (env.getEnclosingClass() 553 .isSubtypeOf(TypeSig.getSig(fa.decl.parent))); 554 555 if (thisField || 556 ((TypeObjectDesignator)fa.od).type instanceof TypeName) { 557 558 ErrorSet.error(fa.locId, 559 "An instance field may be accessed only via " 560 + "an object and/or from a non-static" 561 + " context or an inner class enclosed" 562 + " by a type possessing that field."); 563 564 } else 565 ErrorSet.error(fa.locId, 566 "The instance fields of type " 567 + ((TypeObjectDesignator)fa.od).type 568 + " may not be accessed from type " 569 + sig ); 570 } 571 572 /* FIXME -- need to clean up testing of access modifiers and to make them 573 consistent with JML 574 if (!isPrivateFieldAccessAllowed && 575 Modifiers.isPrivate(fa.decl.modifiers) && 576 Utils.findModifierPragma(fa.decl, 577 TagConstants.SPEC_PUBLIC) == null && 578 Utils.findModifierPragma(fa.decl, 579 TagConstants.SPEC_PROTECTED) == null) { 580 ErrorSet.error(fa.locId, 581 "A private field can be used in "+ 582 "postconditions of overridable methods only if "+ 583 "it is declared spec_public or spec_protected"); 584 } 585 */ 586 587 // The following code checks that "fa" is at least as 588 // spec-accessible as "accessibilityContext" is Java-accessible. 589 // This is vacuously true if "accessibilityLowerBound" is 590 // private. 591 if (accessibilityLowerBound != ACC_LOW_BOUND_Private) { 592 boolean isAccessibleEnough; 593 if (Modifiers.isPublic(fa.decl.modifiers) || 594 Utils.findModifierPragma(fa.decl, 595 TagConstants.SPEC_PUBLIC) != null) { 596 // public and spec_public fields are always accessible 597 isAccessibleEnough = true; 598 } else if (Utils.findModifierPragma(fa.decl, 599 TagConstants.SPEC_PROTECTED) != null) { 600 601 // Copied from the protected case down below. 602 isAccessibleEnough = false; 603 if (accessibilityLowerBound == ACC_LOW_BOUND_Package) { 604 isAccessibleEnough = true; 605 } else if (accessibilityLowerBound == ACC_LOW_BOUND_Protected) { 606 TypeDecl tdContext; 607 if (accessibilityContext instanceof FieldDecl) { 608 tdContext = ((FieldDecl)accessibilityContext).parent; 609 } else { 610 tdContext = ((RoutineDecl)accessibilityContext).parent; 611 } 612 TypeSig tsContext = TypeSig.getSig(tdContext); 613 if (tsContext.isSubtypeOf(TypeSig.getSig(fa.decl.parent))) { 614 isAccessibleEnough = true; 615 } 616 } 617 618 } else if (Modifiers.isPrivate(fa.decl.modifiers)) { 619 // Note: if "fa" type-checked so far, then "fa.decl" and 620 // "accessibilityContext" are declared in the same class. 621 // It would be nice to assert this fact at run-time, but 622 // control may reach this point even if "fa" does not 623 // type-check above. 624 625 // "fa.decl" can be private only if 626 // "accessibilityContext" is private, which was checked 627 // above 628 isAccessibleEnough = false; 629 630 } else if (Modifiers.isPackage(fa.decl.modifiers)) { 631 // Note: if "fa" type-checked so far, then "fa.decl" and 632 // "accessibilityContext" are declared in the same 633 // package. It would be nice to assert this fact at 634 // run-time, but control may reach this point even if 635 // "fa" does not type-check above. 636 637 // "fa.decl" can be package (default) accessible only if 638 // "accessibilityContext" is private (which was checked 639 // above) or package 640 isAccessibleEnough = 641 (accessibilityLowerBound == ACC_LOW_BOUND_Package); 642 643 } else { 644 Assert.notFalse(Modifiers.isProtected(fa.decl.modifiers)); 645 // Note: if "fa" type-checked so far, then either 646 // "fa.decl" and "accessibilityContext" are declared in 647 // the same package or the class declaring 648 // "accessibilityContext" is a subtype of the class 649 // declaring "fa.decl". It would be nice to assert this 650 // fact at run-time, but control may reach this point 651 // even if "fa" does not type-check above. 652 653 // "fa.decl" can be protected only if 654 // "accessibilityContext" is private (which was checked 655 // above) or package, or if "accessibilityContext" is 656 // protected and "fa.decl" is declared in a superclass of 657 // the class that declares "accessibilityContext". 658 isAccessibleEnough = false; 659 if (accessibilityLowerBound == ACC_LOW_BOUND_Package) { 660 isAccessibleEnough = true; 661 } else if (accessibilityLowerBound == ACC_LOW_BOUND_Protected) { 662 TypeDecl tdContext; 663 if (accessibilityContext instanceof FieldDecl) { 664 tdContext = ((FieldDecl)accessibilityContext).parent; 665 } else { 666 tdContext = ((RoutineDecl)accessibilityContext).parent; 667 } 668 TypeSig tsContext = TypeSig.getSig(tdContext); 669 if (tsContext.isSubtypeOf(TypeSig.getSig(fa.decl.parent))) { 670 isAccessibleEnough = true; 671 } 672 } 673 } 674 /* Need to fix the accessibility checking to conform with JML - FIXME 675 if (!isAccessibleEnough) { 676 ErrorSet.error(fa.locId, "Fields mentioned in this modifier "+ 677 "pragma must be at least as accessible "+ 678 "as the field/method being modified (perhaps "+ 679 "try spec_public)"); 680 } 681 */ 682 } 683 684 return fa; 685 } 686 687 case TagConstants.METHODINVOCATION: 688 { 689 countFreeVarsAccesses++; 690 MethodInvocation mi = (MethodInvocation)e; 691 Type t = checkObjectDesignator(env, mi.od); 692 if (mi.od instanceof ExprObjectDesignator && Types.objectsetType == t) { 693 // FIXME - all reach expressions are true for now 694 Expr ee = LiteralExpr.make(TagConstants.BOOLEANLIT,Boolean.TRUE, 695 Location.NULL); 696 setType(ee, Types.booleanType); 697 return ee; 698 } else { 699 Expr ee = super.checkExpr(env,e); 700 return ee; 701 } 702 } 703 704 case TagConstants.IMPLIES: 705 case TagConstants.EXPLIES: 706 case TagConstants.IFF: 707 case TagConstants.NIFF: 708 { 709 BinaryExpr be = (BinaryExpr)e; 710 // each argument is allowed to contain quantifiers and labels if 711 // this expression is 712 isPredicateContext = isCurrentlyPredicateContext; 713 be.left = checkExpr(env, be.left, Types.booleanType); 714 isPredicateContext = isCurrentlyPredicateContext; 715 be.right = checkExpr(env, be.right, Types.booleanType); 716 717 // check illegal associativity of ==> and <== 718 if ((tag == TagConstants.IMPLIES && 719 (be.left.getTag() == TagConstants.EXPLIES || 720 be.right.getTag() == TagConstants.EXPLIES)) || 721 (tag == TagConstants.EXPLIES && 722 (be.left.getTag() == TagConstants.IMPLIES || 723 be.right.getTag() == TagConstants.IMPLIES))) { 724 // unfortunately, we don't have the location of either of the 725 // operators at fault 726 ErrorSet.error(be.getStartLoc(), 727 "Ambiguous association of ==> and <==. " + 728 "Use parentheses to disambiguate."); 729 } 730 731 setType(e, Types.booleanType); 732 return e; 733 } 734 735 case TagConstants.DOTDOT: 736 { 737 BinaryExpr be = (BinaryExpr)e; 738 // each argument is allowed to contain quantifiers and labels if 739 // this expression is 740 isPredicateContext = false; 741 be.left = checkExpr(env, be.left, Types.intType); 742 be.right = checkExpr(env, be.right, Types.intType); 743 744 // FIXME - this really needs to be a range type 745 setType(e, Types.intType); 746 return e; 747 } 748 749 case TagConstants.SUBTYPE: 750 { 751 BinaryExpr be = (BinaryExpr)e; 752 Type expected = Types.booleanType; 753 if (tag == TagConstants.SUBTYPE) 754 expected = Types.typecodeType; 755 be.left = checkExpr(env, be.left, expected); 756 be.right = checkExpr(env, be.right, expected); 757 setType(e, Types.booleanType); 758 return e; 759 } 760 761 case TagConstants.REACH: { 762 // FIXME - just enough to get by for now 763 NaryExpr ne = (NaryExpr)e; 764 Expr nu = 765 checkExpr(env, ne.exprs.elementAt(0)); 766 ne.exprs.setElementAt(nu, 0); 767 if (ne.exprs.size() != 1) { 768 ErrorSet.error(ne.sloc, 769 "A \\reach expression expects just one argument"); 770 setType(e, Types.errorType); 771 } else if (!Types.isReferenceOrNullType(getType(nu))) { 772 ErrorSet.error(nu.getStartLoc(), 773 "A \\reach expression expects an Object argument"); 774 } else { 775 setType(e, Types.objectsetType); 776 } 777 return e; 778 } 779 780 case TagConstants.FRESH: 781 { 782 NaryExpr ne = (NaryExpr)e; 783 if (ne.exprs.size() == 0) { 784 ErrorSet.error(ne.sloc, 785 "The function fresh must have at least one argument"); 786 } else if (!isTwoStateContext) { 787 ErrorSet.error(ne.sloc, 788 "The function \\fresh cannot be used in this context"); 789 } else if (isInsidePRE) { 790 ErrorSet.error(ne.sloc, "The function \\fresh cannot be used "+ 791 "inside a \\old expression"); 792 } else { 793 for (int i = 0; i<ne.exprs.size(); ++i) { 794 Expr nu = 795 checkExpr(env, ne.exprs.elementAt(i), Types.javaLangObject()); 796 ne.exprs.setElementAt(nu, i); 797 } 798 } 799 setType(e, Types.booleanType); 800 return e; 801 } 802 803 case TagConstants.ELEMSNONNULL: 804 { 805 NaryExpr ne = (NaryExpr)e; 806 if (ne.exprs.size() != 1) 807 ErrorSet.error(ne.sloc, 808 "The function \\nonnullelements takes only one argument"); 809 else { 810 Expr nu = checkExpr(env, ne.exprs.elementAt(0), 811 ArrayType.make(Types.javaLangObject(), 812 Location.NULL)); 813 ne.exprs.setElementAt(nu, 0); 814 } 815 setType(e, Types.booleanType); 816 return e; 817 } 818 819 case TagConstants.DTTFSA: 820 { 821 NaryExpr ne = (NaryExpr)e; 822 Type resultType = Types.voidType; 823 if (ne.exprs.size() < 2) { 824 Assert.notFalse(1 <= ne.exprs.size()); 825 ErrorSet.error(ne.sloc, 826 "The function \\dttfsa requires at least two arguments"); 827 } else { 828 // type check each of the arguments 829 for (int i = 0; i < ne.exprs.size(); i++) { 830 Expr nu = checkExpr(env, ne.exprs.elementAt(i)); 831 ne.exprs.setElementAt(nu, i); 832 } 833 // the first argument should be a TypeExpr; retrieve the type 834 // it denotes 835 resultType = ((TypeExpr)ne.exprs.elementAt(0)).type; 836 // the second argument should be a String literal 837 Expr arg1 = ne.exprs.elementAt(1); 838 if (arg1.getTag() != TagConstants.STRINGLIT) { 839 ErrorSet.error(arg1.getStartLoc(), 840 "The second argument to \\dttfsa must be a String literal"); 841 } else { 842 LiteralExpr lit = (LiteralExpr)arg1; 843 String op = (String)lit.value; 844 if (op.equals("identity") && ne.exprs.size() != 3) { 845 ErrorSet.error(ne.sloc, 846 "The function \\dttfsa requires exactly 3 arguments when the second argument is \"identity\""); 847 } 848 } 849 } 850 setType(e, resultType); 851 return e; 852 } 853 854 case TagConstants.WACK_NOWARN: 855 case TagConstants.NOWARN_OP: 856 case TagConstants.WARN: 857 case TagConstants.WARN_OP: 858 { 859 NaryExpr ne = (NaryExpr)e; 860 Expr nu; 861 if( ne.exprs.size() != 1 ) { 862 ErrorSet.error(ne.sloc, 863 "The function " + TagConstants.toString(tag) + 864 " takes only one argument"); 865 setType( e, Types.errorType ); 866 } else { 867 // Get rid of this - FIXME - these are an obsolete definition 868 e = checkExpr(env, ne.exprs.elementAt(0)); 869 //ne.exprs.setElementAt( nu, 0 ); 870 //setType( e, getType(nu) ); 871 } 872 return e; 873 } 874 875 case TagConstants.ELEMTYPE: 876 { 877 NaryExpr ne = (NaryExpr)e; 878 if( ne.exprs.size() != 1 ) 879 ErrorSet.error(ne.sloc, 880 "The function \\elemtype takes only one argument"); 881 else { 882 Expr nu = checkExpr(env, ne.exprs.elementAt(0)); 883 ne.exprs.setElementAt( nu, 0 ); 884 if (!Types.isTypeType(getType(nu))) 885 ErrorSet.error(nu.getStartLoc(), 886 "The argument must have TYPE type"); 887 } 888 setType( e, Types.typecodeType ); 889 return e; 890 } 891 892 case TagConstants.WACK_DURATION: 893 case TagConstants.WACK_WORKING_SPACE: 894 case TagConstants.SPACE: 895 { 896 NaryExpr ne = (NaryExpr)e; 897 if( ne.exprs.size() != 1 ) 898 ErrorSet.error(ne.sloc, 899 "The function " + TagConstants.toString(tag) + 900 " takes only one argument"); 901 else { 902 // Note: the arguments are not evaluated 903 Expr nu = checkExpr(env, ne.exprs.elementAt(0)); 904 ne.exprs.setElementAt( nu, 0 ); 905 } 906 setType( e, Types.longType ); 907 return e; 908 } 909 910 case TagConstants.INVARIANT_FOR: 911 case TagConstants.IS_INITIALIZED: 912 { 913 NaryExpr ne = (NaryExpr)e; 914 // FIXME - Is this a one argument function ? 915 if( ne.exprs.size() != 1 ) 916 ErrorSet.error( ne.sloc, 917 "The function takes only one argument"); 918 else { 919 Expr nu = checkExpr(env, ne.exprs.elementAt(0)); 920 ne.exprs.setElementAt( nu, 0 ); 921 } 922 setType( e, Types.booleanType ); 923 return e; 924 } 925 926 case TagConstants.NOTMODIFIEDEXPR: 927 { 928 NotModifiedExpr ne = (NotModifiedExpr)e; 929 ne.expr = checkExpr(env, ne.expr); 930 setType( e, Types.booleanType ); 931 return e; 932 } 933 934 case TagConstants.MAX: 935 { 936 NaryExpr ne = (NaryExpr)e; 937 if( ne.exprs.size() != 1 ) 938 ErrorSet.error( ne.sloc, 939 "The function \\max takes only one argument"); 940 else { 941 Expr nu = checkExpr(env, ne.exprs.elementAt(0), Types.locksetType); 942 ne.exprs.setElementAt( nu, 0 ); 943 } 944 setType( e, Types.javaLangObject() ); 945 return e; 946 } 947 948 case TagConstants.PRE: 949 { 950 NaryExpr ne = (NaryExpr)e; 951 if( ne.exprs.size() != 1 ) { 952 ErrorSet.error( ne.sloc, 953 "The function \\old takes only one argument"); 954 setType(e, Types.voidType); 955 } else if (!isTwoStateContext) { 956 ErrorSet.error(ne.sloc, 957 "The function \\old cannot be used in this context"); 958 setType(e, Types.voidType); 959 } else if (isInsidePRE) { 960 ErrorSet.error(ne.sloc, "Nested applications of \\old not allowed"); 961 setType(e, Types.voidType); 962 } else { 963 isInsidePRE = true; 964 Expr nu = checkExpr(env, ne.exprs.elementAt(0) ); 965 Assert.notFalse(isInsidePRE); 966 isInsidePRE = false; 967 ne.exprs.setElementAt( nu, 0 ); 968 setType( e, getType( nu ) ); 969 } 970 return e; 971 } 972 973 case TagConstants.TYPEOF: 974 { 975 NaryExpr ne = (NaryExpr)e; 976 if( ne.exprs.size() != 1 ) 977 ErrorSet.error( ne.sloc, 978 "The function \\typeof takes only one argument"); 979 else { 980 Expr ex = ne.exprs.elementAt(0); 981 Expr nu = checkExpr(env, ex ); 982 ne.exprs.setElementAt( nu, 0 ); 983 Type t = getType(nu); 984 if (t instanceof PrimitiveType) { 985 e = TypeExpr.make(ex.getStartLoc(),ex.getEndLoc(),t); 986 } 987 } 988 setType( e, Types.typecodeType ); 989 return e; 990 } 991 992 case TagConstants.TYPEEXPR: 993 { 994 TypeExpr te = (TypeExpr)e; 995 env.resolveType( sig, te.type ); 996 setType(e, Types.typecodeType ); 997 return e; 998 } 999 1000 case TagConstants.LABELEXPR: 1001 { 1002 LabelExpr le = (LabelExpr)e; 1003 if (!isCurrentlyPredicateContext) { 1004 ErrorSet.error(le.getStartLoc(), 1005 "Labeled predicates are not allowed in this context"); 1006 setType(e, Types.booleanType); 1007 } else { 1008 isPredicateContext = true; 1009 le.expr = checkExpr(env, le.expr); 1010 setType(e, getType( le.expr ) ); 1011 } 1012 return e; 1013 } 1014 1015 case TagConstants.NUM_OF: 1016 { 1017 NumericalQuantifiedExpr qe = (NumericalQuantifiedExpr)e; 1018 1019 // if (!isCurrentlyPredicateContext) { 1020 // ErrorSet.error(qe.getStartLoc(), 1021 // "Quantified expressions are not allowed in this context"); 1022 // } else 1023 { 1024 Env subenv = env; 1025 1026 for( int i=0; i<qe.vars.size(); i++) { 1027 GenericVarDecl decl = qe.vars.elementAt(i); 1028 env.resolveType( sig, decl.type ); 1029 1030 subenv = new EnvForLocals(subenv, decl); 1031 } 1032 isPredicateContext = true; 1033 qe.expr = checkExpr(subenv, qe.expr, Types.booleanType); 1034 } 1035 setType(e, Types.intType); 1036 return e; 1037 } 1038 1039 case TagConstants.SUM: 1040 case TagConstants.PRODUCT: 1041 case TagConstants.MIN: 1042 case TagConstants.MAXQUANT: 1043 { 1044 GeneralizedQuantifiedExpr qe = (GeneralizedQuantifiedExpr)e; 1045 1046 /* 1047 if (!isCurrentlyPredicateContext) { 1048 ErrorSet.error(qe.getStartLoc(), 1049 "Quantified expressions are not allowed in this context"); 1050 } else */ 1051 { 1052 Env subenv = env; 1053 1054 for( int i=0; i<qe.vars.size(); i++) { 1055 GenericVarDecl decl = qe.vars.elementAt(i); 1056 env.resolveType( sig, decl.type ); 1057 1058 subenv = new EnvForLocals(subenv, decl); 1059 } 1060 isPredicateContext = true; 1061 qe.rangeExpr = checkExpr(subenv, qe.rangeExpr, Types.booleanType); 1062 qe.expr = checkExpr(subenv, qe.expr, Types.intType); 1063 } 1064 setType(e, Types.intType); 1065 return e; 1066 } 1067 1068 case TagConstants.FORALL: 1069 case TagConstants.EXISTS: 1070 { 1071 QuantifiedExpr qe = (QuantifiedExpr)e; 1072 1073 if (!isCurrentlyPredicateContext) { 1074 ErrorSet.error(qe.getStartLoc(), 1075 "Quantified expressions are not allowed in this context"); 1076 } else { 1077 Env subenv = env; 1078 1079 for( int i = 0; i < qe.vars.size(); i++) { 1080 GenericVarDecl decl = qe.vars.elementAt(i); 1081 env.resolveType(sig, decl.type); 1082 1083 subenv = new EnvForLocals(subenv, decl, false); 1084 } 1085 isPredicateContext = true; 1086 if (qe.rangeExpr != null) { 1087 qe.rangeExpr = checkExpr(subenv, qe.rangeExpr, Types.booleanType); 1088 } 1089 qe.expr = checkExpr(subenv, qe.expr, Types.booleanType); 1090 } 1091 if (qe.rangeExpr == null) { // skip 1092 } else if (tag == TagConstants.FORALL) { 1093 qe.expr = BinaryExpr.make(TagConstants.IMPLIES, 1094 qe.rangeExpr,qe.expr,Location.NULL); 1095 setType(qe.expr,Types.booleanType); 1096 } else { 1097 qe.expr = BinaryExpr.make(TagConstants.AND, 1098 qe.rangeExpr,qe.expr,Location.NULL); 1099 setType(qe.expr,Types.booleanType); 1100 } 1101 setType(e, Types.booleanType); 1102 return e; 1103 } 1104 1105 case TagConstants.PARENEXPR: 1106 case TagConstants.NOT: 1107 { 1108 // the sub-expression is allowed to contain quantifiers and 1109 // labels if this expression is 1110 isPredicateContext = isCurrentlyPredicateContext; 1111 return super.checkExpr(env, e); 1112 } 1113 1114 case TagConstants.ADD: 1115 { 1116 Expr ee = super.checkExpr(env, e); 1117 if (!Main.options().useOldStringHandling && 1118 Types.isSameType(getType(ee),Types.javaLangString())) { 1119 boolean savedInAnnotation = inAnnotation; 1120 inAnnotation = true; 1121 BinaryExpr be = (BinaryExpr)ee; 1122 Expr left = be.left; 1123 Expr right = be.right; 1124 if (!Types.isSameType(getType(left),Types.javaLangString())) { 1125 Name nn = Name.make("java.lang.String.valueOf",left.getStartLoc()); 1126 ExprVec a = ExprVec.make(); 1127 a.addElement(left); 1128 AmbiguousMethodInvocation mi = AmbiguousMethodInvocation.make( 1129 nn,null,left.getStartLoc(),a); 1130 MethodInvocation mm = env.disambiguateMethodName(mi); 1131 left = checkExpr(env, mm); 1132 } 1133 if (!Types.isSameType(getType(right),Types.javaLangString())) { 1134 Name nn = Name.make("java.lang.String.valueOf",right.getStartLoc()); 1135 ExprVec a = ExprVec.make(); 1136 a.addElement(right); 1137 AmbiguousMethodInvocation mi = AmbiguousMethodInvocation.make( 1138 nn,null,right.getStartLoc(),a); 1139 MethodInvocation mm = env.disambiguateMethodName(mi); 1140 right = checkExpr(env, mm); 1141 } 1142 int loc = be.locOp; 1143 Name n = Name.make(TagConstants.STRINGCATINFIX,loc); 1144 ExprVec args = ExprVec.make(); 1145 args.addElement(left); 1146 args.addElement(right); 1147 AmbiguousMethodInvocation ami = AmbiguousMethodInvocation.make( 1148 n,null,loc,args); 1149 MethodInvocation m = env.disambiguateMethodName(ami); 1150 ee = checkExpr(env, m); 1151 inAnnotation = savedInAnnotation; 1152 } 1153 return ee; 1154 } 1155 1156 case TagConstants.OR: 1157 case TagConstants.AND: 1158 case TagConstants.EQ: 1159 case TagConstants.NE: 1160 { 1161 BinaryExpr be = (BinaryExpr)e; 1162 // each argument is allowed to contain quantifiers and labels if 1163 // this expression is 1164 isPredicateContext = isCurrentlyPredicateContext; 1165 be.left = checkExpr(env, be.left); 1166 isPredicateContext = isCurrentlyPredicateContext; 1167 be.right = checkExpr(env, be.right); 1168 if (false && Types.isTypeType(getType(be.left)) && 1169 // DO WE NEED TO check the composite expressions ??? FIXME TYPE-EQUIV 1170 Types.isTypeType(getType(be.right))) { 1171 setType( be, Types.booleanType); 1172 } else { 1173 Type t = checkBinaryExpr(be.op, be.left, be.right, be.locOp); 1174 setType( be, t ); 1175 } 1176 return be; 1177 } 1178 1179 case TagConstants.WILDREFEXPR: 1180 { 1181 // FIXME - WildRefExpr needs cleanup . In current usage r.od is always null 1182 // on input. 1183 WildRefExpr r = (WildRefExpr)e; 1184 if (!isCurrentlySpecDesignatorContext) { 1185 setType(r, Types.errorType); 1186 ErrorSet.error(r.getStartLoc(), 1187 "Reference wild cards allowed only as "+ 1188 "specification designators"); 1189 } else { 1190 // Can't set the type, but need to check the type of the od 1191 if (r.od == null) { 1192 if (r.var instanceof AmbiguousVariableAccess) { 1193 AmbiguousVariableAccess a = (AmbiguousVariableAccess)r.var; 1194 Object o = env.disambiguateTypeOrFieldName(a.name); 1195 if (o instanceof TypeSig) { 1196 r.od = TypeObjectDesignator.make(r.var.getStartLoc(), 1197 (TypeSig)o ); 1198 } else { 1199 r.var = checkExpr(env,r.var); 1200 // FIXME - really need locDot here 1201 r.od = ExprObjectDesignator.make( 1202 r.var.getEndLoc(), 1203 r.var); 1204 } 1205 r.var = null; 1206 } else { 1207 r.var = checkExpr(env,r.var); 1208 // FIXME - really need locDot here 1209 r.od = ExprObjectDesignator.make( 1210 r.var.getEndLoc(), 1211 r.var); 1212 } 1213 checkObjectDesignator(env,r.od); 1214 } else { 1215 Type t = checkObjectDesignator(env,r.od); 1216 // FIXME 1217 //System.out.println("TYPE " + t); 1218 } 1219 } 1220 return r; 1221 } 1222 1223 case TagConstants.ARRAYREFEXPR: 1224 { 1225 ArrayRefExpr r = (ArrayRefExpr)e; 1226 1227 r.array = checkExpr(env, r.array); 1228 Type arrType = getType( r.array ); 1229 r.index = checkExpr(env, r.index); 1230 Type t = getType( r.index ); 1231 1232 if( arrType instanceof ArrayType ) { 1233 setType( r, ((ArrayType)arrType).elemType ); 1234 Type ndxType = 1235 Types.isNumericType( t ) ? Types.unaryPromote( t ) : t; 1236 if( !Types.isSameType( ndxType, Types.intType ) && 1237 !Types.isErrorType(ndxType) ) 1238 ErrorSet.error(r.locOpenBracket, "Array index is not an integer"); 1239 1240 } else if( arrType.getTag() == TagConstants.LOCKSET ) { 1241 setType( r, Types.booleanType ); 1242 if( !Types.isReferenceOrNullType( t ) && 1243 !Types.isErrorType(t) ) 1244 ErrorSet.error(r.locOpenBracket, 1245 "Can only index \\lockset with a reference type"); 1246 } else { 1247 setType( r, Types.errorType ); 1248 if (!Types.isErrorType(arrType) ) 1249 ErrorSet.error( r.locOpenBracket, 1250 "Attempt to index a non-array value"); 1251 } 1252 1253 return r; 1254 } 1255 1256 case TagConstants.ARRAYRANGEREFEXPR: 1257 { 1258 ArrayRangeRefExpr r = (ArrayRangeRefExpr)e; 1259 if (!isCurrentlySpecDesignatorContext) { 1260 setType(r, Types.errorType); 1261 ErrorSet.error(r.getStartLoc(), 1262 "Array ranges are allowed only as "+ 1263 "specification designators"); 1264 } else { 1265 1266 r.array = checkExpr(env, r.array); 1267 Type arrType = getType( r.array ); 1268 if (r.lowIndex != null) r.lowIndex = checkExpr(env, r.lowIndex); 1269 if (r.highIndex != null) r.highIndex = checkExpr(env, r.highIndex); 1270 Type t = r.lowIndex == null ? null : getType( r.lowIndex ); 1271 Type tt = r.highIndex == null ? null : getType( r.highIndex ); 1272 1273 if( arrType instanceof ArrayType ) { 1274 setType( r, ((ArrayType)arrType).elemType ); 1275 if (t != null) { 1276 Type ndxType = 1277 Types.isNumericType( t ) ? Types.unaryPromote( t ) : t; 1278 if( !Types.isSameType( ndxType, Types.intType ) && 1279 !Types.isErrorType(ndxType) ) 1280 ErrorSet.error(r.locOpenBracket, "Array index is not an integer"); 1281 } 1282 if (tt != null) { 1283 Type ndxType = 1284 Types.isNumericType( tt ) ? Types.unaryPromote( tt ) : tt; 1285 if( !Types.isSameType( ndxType, Types.intType ) && 1286 !Types.isErrorType(ndxType) ) 1287 ErrorSet.error(r.locOpenBracket, "Array index is not an integer"); 1288 } 1289 1290 } else { 1291 setType( r, Types.errorType ); 1292 if (!Types.isErrorType(arrType) ) 1293 ErrorSet.error( r.locOpenBracket, 1294 "Attempt to index a non-array value"); 1295 } 1296 } 1297 1298 return r; 1299 } 1300 case TagConstants.RESEXPR: 1301 { 1302 if (!isRESContext || returnType == null) { 1303 if (!Types.isErrorType(returnType)) 1304 ErrorSet.error(e.getStartLoc(), 1305 "Keyword \\result is not allowed in this context"); 1306 setType( e, Types.errorType ); 1307 } 1308 else 1309 setType( e, returnType ); 1310 1311 return e; 1312 } 1313 1314 case TagConstants.SETCOMPEXPR: 1315 { 1316 SetCompExpr s = (SetCompExpr)e; 1317 1318 env.resolveType(sig, s.type); 1319 env.resolveType(sig, s.fp.type); 1320 Env subenv = new EnvForLocals(env,s.fp,false); 1321 boolean savedPredicateContext = isPredicateContext; 1322 isPredicateContext = true; 1323 s.expr = checkExpr(subenv, s.expr, Types.booleanType); 1324 isPredicateContext = savedPredicateContext; 1325 setType( e, s.type); 1326 // FIXME - CHeck that the type is only JMLObjectSet, JMLValueSet 1327 // Check that the predicate has the correct restricted form 1328 return e; 1329 } 1330 1331 case TagConstants.NOTSPECIFIEDEXPR: 1332 { 1333 setType( e, Types.voidType); 1334 return e; 1335 } 1336 case TagConstants.EVERYTHINGEXPR: 1337 { 1338 if (!isCurrentlySpecDesignatorContext) { 1339 ErrorSet.error(e.getStartLoc(), 1340 "Keyword \\everything is not allowed in this context"); 1341 setType( e, Types.errorType); 1342 } else { 1343 setType( e, Types.voidType); 1344 } 1345 return e; 1346 } 1347 case TagConstants.NOTHINGEXPR: 1348 { 1349 if (!isCurrentlySpecDesignatorContext) { 1350 ErrorSet.error(e.getStartLoc(), 1351 "Keyword \\nothing is not allowed in this context"); 1352 setType( e, Types.errorType); 1353 } else { 1354 setType( e, Types.voidType); 1355 } 1356 return e; 1357 } 1358 case TagConstants.LOCKSETEXPR: 1359 { 1360 if (! isLocksetContext) { 1361 ErrorSet.error(e.getStartLoc(), 1362 "Keyword \\lockset is not allowed in this context"); 1363 } 1364 setType( e, Types.locksetType ); 1365 return e; 1366 } 1367 1368 case TagConstants.LE: 1369 case TagConstants.LT: 1370 { 1371 BinaryExpr be = (BinaryExpr)e; 1372 be.left = checkExpr(env, be.left); 1373 be.right = checkExpr(env, be.right); 1374 1375 if( Types.isReferenceOrNullType( getType( be.left ) ) 1376 && Types.isReferenceOrNullType( getType( be.right ) ) ) { 1377 // is lock comparison, and is ok 1378 setType( be, Types.booleanType ); 1379 return be; 1380 } else { 1381 return super.checkExpr(env, e); 1382 } 1383 } 1384 1385 case TagConstants.NEWINSTANCEEXPR: 1386 case TagConstants.NEWARRAYEXPR: 1387 { 1388 countFreeVarsAccesses++; 1389 /* FIXME - Yes it can, but it must be pure! 1390 if (inAnnotation) { 1391 ErrorSet.error(e.getStartLoc(), 1392 "new cannot be used in specification expressions"); 1393 } 1394 */ 1395 return super.checkExpr(env, e); 1396 } 1397 1398 case TagConstants.ASSIGN: case TagConstants.ASGMUL: 1399 case TagConstants.ASGDIV: case TagConstants.ASGREM: 1400 case TagConstants.ASGADD: case TagConstants.ASGSUB: 1401 case TagConstants.ASGLSHIFT: case TagConstants.ASGRSHIFT: 1402 case TagConstants.ASGURSHIFT: case TagConstants.ASGBITAND: 1403 case TagConstants.ASGBITOR: case TagConstants.ASGBITXOR: 1404 { 1405 if (inAnnotation && !inModelBody) { 1406 BinaryExpr be = (BinaryExpr)e; 1407 ErrorSet.error(be.locOp, 1408 "assignments cannot be used in specification expressions"); 1409 } 1410 return super.checkExpr(env, e); 1411 } 1412 1413 case TagConstants.INC: case TagConstants.DEC: 1414 case TagConstants.POSTFIXINC: case TagConstants.POSTFIXDEC: 1415 { 1416 if (inAnnotation && !inModelBody) { 1417 UnaryExpr ue = (UnaryExpr)e; 1418 ErrorSet.error(ue.locOp, 1419 "assignments cannot be used in specification expressions"); 1420 } 1421 return super.checkExpr(env, e); 1422 } 1423 1424 default: 1425 return super.checkExpr(env, e); 1426 } 1427 1428 } finally { 1429 1430 isPredicateContext = isCurrentlyPredicateContext; 1431 } 1432 } 1433 1434 // Pragma checkers 1435 1436 protected void checkTypeDeclElemPragma(TypeDeclElemPragma e) { 1437 int tag = e.getTag(); 1438 boolean savedInAnnotation = inAnnotation; 1439 inAnnotation = true; // Must be reset before we exit! 1440 try { 1441 1442 switch(tag) { 1443 case TagConstants.AXIOM: 1444 case TagConstants.INITIALLY: 1445 case TagConstants.INVARIANT: 1446 case TagConstants.CONSTRAINT: // FIXME - do we need to change the logic below to handle constraints? 1447 { 1448 ExprDeclPragma ep = (ExprDeclPragma)e; 1449 Env rootEnv = (tag == TagConstants.AXIOM || 1450 Modifiers.isStatic(ep.modifiers)) ? rootSEnv : rootIEnv; 1451 1452 invariantContext = (tag == TagConstants.INVARIANT) || 1453 tag == TagConstants.INITIALLY; 1454 isTwoStateContext = (tag == TagConstants.CONSTRAINT); 1455 boolean oldIsLocksetContext = isLocksetContext; 1456 isLocksetContext = false; 1457 if (invariantContext){ 1458 // FIXME Assert.notFalse(countFreeVarsAccesses == 0); 1459 countFreeVarsAccesses = 0; 1460 } 1461 1462 ep.expr = checkPredicate(rootEnv, ep.expr); 1463 isLocksetContext = oldIsLocksetContext; 1464 1465 TypeSig sig = TypeSig.getSig(e.getParent()); 1466 if (sig==javafe.tc.Types.javaLangObject() || 1467 sig==javafe.tc.Types.javaLangCloneable()) { 1468 if (invariantContext) ErrorSet.fatal(e.getStartLoc(), 1469 "java.lang.Object and java.lang.Cloneable may not" 1470 + " contain invariants."); // FIXME - Why? 1471 } 1472 /* 1473 FIXME - see uses of countFreeVarsAccess 1474 if (invariantContext && countFreeVarsAccesses == 0 && 1475 // Don't print an error if the entire invariant 1476 // is an informal predicate 1477 escjava.parser.EscPragmaParser. 1478 informalPredicateDecoration.get(ep.expr)==null) { 1479 ErrorSet.error(e.getStartLoc(), 1480 "Class invariants must mention program variables" 1481 + " or fields."); 1482 } 1483 */ 1484 1485 if (invariantContext) {countFreeVarsAccesses = 0;} 1486 invariantContext = false; 1487 isTwoStateContext = false; 1488 break; 1489 } 1490 case TagConstants.REPRESENTS: 1491 { 1492 NamedExprDeclPragma ep = (NamedExprDeclPragma)e; 1493 boolean stat = Modifiers.isStatic(ep.modifiers); 1494 1495 // What about static model vars? 1496 // Can the represents clause be static ? FIXME 1497 Env rootEnv = stat? rootSEnv : rootIEnv; 1498 ep.target = checkExpr(rootEnv, ep.target); 1499 1500 if (ep.target instanceof FieldAccess) { 1501 invariantContext = false; 1502 isTwoStateContext = false; 1503 boolean oldIsLocksetContext = isLocksetContext; 1504 isLocksetContext = false; 1505 if (invariantContext){ 1506 // FIXME Assert.notFalse(countFreeVarsAccesses == 0); 1507 countFreeVarsAccesses = 0; 1508 } 1509 1510 ep.expr = checkPredicate(rootEnv, ep.expr); 1511 isLocksetContext = oldIsLocksetContext; 1512 1513 FieldAccess fa = (FieldAccess)ep.target; 1514 if (!Utils.isModel(fa.decl)) { 1515 ErrorSet.error(fa.getStartLoc(), 1516 "A represents clause must name a model field", 1517 fa.decl.locId); 1518 } 1519 if (stat && !Modifiers.isStatic(fa.decl.modifiers)) { 1520 ErrorSet.error(fa.getStartLoc(), 1521 "A static represents clause must name a static model field"); 1522 } 1523 if (!stat && Modifiers.isStatic(fa.decl.modifiers)) { 1524 ErrorSet.error(fa.getStartLoc(), 1525 "A non-static represents clause must name a non-static model field"); 1526 } 1527 1528 /* THis is done in type prepping 1529 TypeDecl td = ep.parent; 1530 TypeDeclElemVec tv = (TypeDeclElemVec)Utils.representsDecoration.get(td); 1531 if (tv == null) { 1532 tv = TypeDeclElemVec.make(10); 1533 Utils.representsDecoration.set(td,tv); 1534 } 1535 tv.addElement(ep); 1536 */ 1537 TypeDeclElemVec tv = (TypeDeclElemVec)Utils.representsDecoration.get(fa.decl); 1538 if (tv == null) { 1539 tv = TypeDeclElemVec.make(10); 1540 Utils.representsDecoration.set(fa.decl,tv); 1541 } 1542 tv.addElement(ep); 1543 } else if (!(ep.target instanceof AmbiguousVariableAccess)){ 1544 // If the type is Ambiguous, then an Undefined variable 1545 // error has already been issued. I'm not actually 1546 // sure that this point is reachable. 1547 ErrorSet.error(ep.target.getStartLoc(), 1548 "Expected a field identifier here"); 1549 } 1550 break; 1551 } 1552 case TagConstants.DEPENDS: 1553 { 1554 DependsPragma ep = (DependsPragma)e; 1555 // FIXME - perhaps use rootSEnv if the variable 1556 // being discussed is static ? 1557 Env rootEnv = rootIEnv; 1558 1559 ep.target = checkExpr(rootEnv, ep.target); 1560 1561 ExprVec ev = ep.exprs; 1562 for (int i=0; i<ev.size(); ++i) { 1563 ev.setElementAt( 1564 checkExpr(rootEnv, ev.elementAt(i)), i); 1565 } 1566 1567 // FIXME - Need to check that 1568 // LHS is a simple model variable, a field of 1569 // this or a super class or an interface 1570 // RHS consists of store-refs, no computed expressions 1571 // RHS may have other model variables 1572 // check access ? 1573 break; 1574 } 1575 1576 case TagConstants.MODELCONSTRUCTORDECLPRAGMA: { 1577 ModelConstructorDeclPragma me = (ModelConstructorDeclPragma)e; 1578 ConstructorDecl cd = me.decl; 1579 Env rootEnv = Modifiers.isStatic(cd.modifiers) 1580 ? rootSEnv 1581 : rootIEnv; 1582 1583 // All gets checked since the associated ConstructorDecl is 1584 // part of the type 1585 1586 // FIXME - the body needs to allow ghost/model vars 1587 break; 1588 } 1589 1590 1591 case TagConstants.MODELMETHODDECLPRAGMA: { 1592 MethodDecl decl = ((ModelMethodDeclPragma)e).decl; 1593 Env rootEnv = Modifiers.isStatic(decl.modifiers) 1594 ? rootSEnv 1595 : rootIEnv; 1596 1597 // All gets checked since the associated ConstructorDecl is 1598 // part of the type 1599 1600 // FIXME - the body needs to allow ghost/model vars 1601 break; 1602 } 1603 1604 case TagConstants.MONITORS_FOR: { 1605 IdExprDeclPragma emp = (IdExprDeclPragma)e; 1606 Identifier id = emp.id; 1607 TypeDeclElemVec elems = e.parent.elems; 1608 FieldDecl fd = null; 1609 for (int i=0; i<elems.size(); ++i) { 1610 TypeDeclElem td = elems.elementAt(i); 1611 if (td instanceof FieldDecl && 1612 ((FieldDecl)td).id == id) { 1613 fd = (FieldDecl)td; 1614 break; 1615 } 1616 } 1617 boolean isStatic = false; 1618 if (fd == null) { 1619 ErrorSet.error(emp.loc, 1620 "Could not find identifier " + id + " in this class"); 1621 } else { 1622 isStatic = Modifiers.isStatic(fd.modifiers); 1623 } 1624 if (Modifiers.isStatic(emp.modifiers)) isStatic = true; 1625 Env env = isStatic ? rootSEnv : rootIEnv; 1626 int oldAccessibilityLowerBound = accessibilityLowerBound; 1627 ASTNode oldAccessibilityContext = accessibilityContext; 1628 accessibilityLowerBound = getAccessibility(fd.modifiers); 1629 accessibilityContext = fd; 1630 emp.expr = checkExpr(env, emp.expr, Types.javaLangObject()); 1631 accessibilityLowerBound = oldAccessibilityLowerBound; 1632 accessibilityContext = oldAccessibilityContext; 1633 fd.pmodifiers.addElement( 1634 ExprModifierPragma.make( 1635 TagConstants.MONITORED_BY, 1636 emp.expr, 1637 emp.loc 1638 )); 1639 break; 1640 } 1641 1642 case TagConstants.WRITABLE: 1643 case TagConstants.READABLE: { 1644 NamedExprDeclPragma emp = (NamedExprDeclPragma)e; 1645 1646 isSpecDesignatorContext = true; 1647 Env newenv = rootIEnv; 1648 emp.target = checkDesignator(newenv, emp.target); 1649 isSpecDesignatorContext = false; 1650 emp.expr = checkPredicate(newenv, emp.expr); 1651 switch (emp.target.getTag()) { 1652 case TagConstants.FIELDACCESS: { 1653 FieldAccess fa = (FieldAccess)emp.target; 1654 if (fa.decl != null && 1655 // The array "length" field has already been checked 1656 // insuper.checkDesignator(). 1657 fa.decl != Types.lengthFieldDecl) { 1658 1659 if (tag == TagConstants.WRITABLE && 1660 Modifiers.isFinal(fa.decl.modifiers)) { 1661 // FIXME 1662 } 1663 fa.decl.pmodifiers.addElement( 1664 ExprModifierPragma.make( 1665 emp.tag == TagConstants.READABLE ? 1666 TagConstants.READABLE_IF: 1667 TagConstants.WRITABLE_IF, 1668 emp.expr, 1669 emp.loc 1670 ) 1671 ); 1672 } 1673 break; 1674 } 1675 1676 case TagConstants.ARRAYREFEXPR: 1677 case TagConstants.ARRAYRANGEREFEXPR: 1678 case TagConstants.WILDREFEXPR: 1679 case TagConstants.EVERYTHINGEXPR: 1680 case TagConstants.NOTHINGEXPR: 1681 case TagConstants.NOTSPECIFIEDEXPR: 1682 // FIXME - not implemented 1683 break; 1684 1685 default: 1686 if (escjava.parser.EscPragmaParser. 1687 informalPredicateDecoration.get(emp.target)==null) { 1688 // The expression is not a designator 1689 // but we allow an informal predicate 1690 if (!Types.isErrorType(getType(emp.target))) 1691 ErrorSet.error(emp.target.getStartLoc(), 1692 "Not a specification designator expression"); 1693 } else { 1694 emp.target = null; 1695 } 1696 } 1697 break; 1698 } 1699 1700 case TagConstants.MODELDECLPRAGMA: { 1701 FieldDecl decl = ((ModelDeclPragma)e).decl; 1702 Env rootEnv = Modifiers.isStatic(decl.modifiers) 1703 ? rootSEnv 1704 : rootIEnv; 1705 1706 rootEnv.resolveType( sig, decl.type ); 1707 checkModifierPragmaVec( decl.pmodifiers, decl, rootEnv ); 1708 checkTypeModifiers(rootEnv, decl.type); 1709 1710 // Check for both static and instance declarations 1711 1712 if (Modifiers.isStatic(decl.modifiers)) { 1713 ModifierPragma inst = Utils.findModifierPragma(decl, 1714 TagConstants.INSTANCE); 1715 if (inst != null) ErrorSet.error(inst.getStartLoc(), 1716 "May not specify both static and instance on a declaration"); 1717 } 1718 1719 /* 1720 * Check for other fields with the same name: 1721 */ 1722 { 1723 TypeDeclElemVec elems = decl.parent.elems; 1724 FieldDecl fd; 1725 for (int i = 0; i<elems.size(); ++i) { 1726 TypeDeclElem tde = elems.elementAt(i); 1727 if (tde instanceof FieldDecl) { 1728 fd = (FieldDecl)tde; 1729 } else if (tde instanceof GhostDeclPragma) { 1730 fd = ((GhostDeclPragma)tde).decl; 1731 } else if (tde instanceof ModelDeclPragma) { 1732 fd = ((ModelDeclPragma)tde).decl; 1733 } else 1734 continue; 1735 if (fd.id == decl.id && fd != decl) 1736 ErrorSet.error(decl.locId, 1737 "Another field named '"+decl.id.toString() 1738 +"' already exists in this type", fd.locId); 1739 } 1740 } 1741 1742 break; 1743 } 1744 1745 case TagConstants.GHOSTDECLPRAGMA: { 1746 FieldDecl decl = ((GhostDeclPragma)e).decl; 1747 ModifierPragma inst = Utils.findModifierPragma(decl, 1748 TagConstants.INSTANCE); 1749 // Check for both static and instance declarations 1750 1751 if (Modifiers.isStatic(decl.modifiers)) { 1752 if (inst != null) ErrorSet.error(inst.getStartLoc(), 1753 "May not specify both static and instance on a declaration"); 1754 } 1755 1756 Env rootEnv = Modifiers.isStatic(decl.modifiers) 1757 ? rootSEnv 1758 : rootIEnv; 1759 1760 rootEnv.resolveType( sig, decl.type ); 1761 checkModifierPragmaVec( decl.pmodifiers, decl, rootEnv ); 1762 checkTypeModifiers(rootEnv, decl.type); 1763 1764 1765 1766 /* 1767 * Handle initializer: 1768 */ 1769 1770 if (decl.init != null) { 1771 leftToRight = true; 1772 allowedExceptions.removeAllElements(); 1773 Assert.notFalse( allowedExceptions.size() == 0); 1774 decl.init = checkInit(rootEnv, decl.init, decl.type); 1775 } 1776 1777 /* 1778 * Check for other fields with the same name: 1779 */ 1780 { 1781 TypeDeclElemVec elems = decl.parent.elems; 1782 FieldDecl fd; 1783 for (int i = 0; i<elems.size(); ++i) { 1784 TypeDeclElem tde = elems.elementAt(i); 1785 if (tde instanceof FieldDecl) { 1786 fd = (FieldDecl)tde; 1787 } else if (tde instanceof GhostDeclPragma) { 1788 fd = ((GhostDeclPragma)tde).decl; 1789 } else if (tde instanceof ModelDeclPragma) { 1790 fd = ((ModelDeclPragma)tde).decl; 1791 } else 1792 continue; 1793 if (fd.id == decl.id && fd != decl) 1794 ErrorSet.error(decl.locId, 1795 "Another field named '"+decl.id.toString() 1796 +"' already exists in this type", fd.locId); 1797 } 1798 } 1799 1800 1801 break; 1802 } 1803 1804 case TagConstants.STILLDEFERREDDECLPRAGMA: { 1805 StillDeferredDeclPragma sddp = (StillDeferredDeclPragma)e; 1806 if (!sig.hasField(sddp.var)) { 1807 ErrorSet.error(sddp.locId, "No such field"); 1808 } 1809 1810 // TBW: To support still_deferred, one also needs to check that 1811 // "sddp.var" is declared as writable-deferred in the direct 1812 // superclass. 1813 break; 1814 } 1815 1816 default: 1817 Assert.fail("Unexpected tag " + tag + 1818 " " + TagConstants.toString(tag)); 1819 } 1820 } finally { 1821 inAnnotation = savedInAnnotation; 1822 } 1823 } 1824 1825 protected Env checkModifierPragma(ModifierPragma p, ASTNode ctxt, Env env) { 1826 1827 boolean savedInAnnotation = inAnnotation; 1828 inAnnotation = true; // Must be reset before we exit! 1829 try { 1830 int tag = p.getTag(); 1831 switch(tag) 1832 { 1833 case TagConstants.EVERYTHINGEXPR: 1834 case TagConstants.EVERYTHING: 1835 case TagConstants.NOTHING: 1836 case TagConstants.NOT_SPECIFIED: 1837 case TagConstants.NOTHINGEXPR: 1838 case TagConstants.NOTSPECIFIEDEXPR: 1839 // FIXME - check the context??? 1840 break; 1841 1842 case TagConstants.UNINITIALIZED: 1843 if( ctxt.getTag() != TagConstants.LOCALVARDECL ) { 1844 int loc; 1845 if (ctxt instanceof GenericVarDecl) 1846 loc = ((GenericVarDecl)ctxt).locId; 1847 else 1848 loc = p.getStartLoc(); 1849 ErrorSet.error(loc, 1850 "The uninitialized annotation can occur only on " 1851 +"local variable declarations"); 1852 } else if( ((LocalVarDecl)ctxt).init == null ) { 1853 ErrorSet.error(((GenericVarDecl)ctxt).locId, 1854 "The uninitialized annotation can occur only on " 1855 +"local variable declarations " 1856 +"that have an initializer"); 1857 } 1858 break; 1859 1860 case TagConstants.MONITORED: 1861 { 1862 if( ctxt.getTag() != TagConstants.FIELDDECL ) { 1863 int loc; 1864 if (ctxt instanceof GenericVarDecl) 1865 loc = ((GenericVarDecl)ctxt).locId; 1866 else 1867 loc = p.getStartLoc(); 1868 ErrorSet.error(loc, 1869 "The monitored annotation can occur only on " 1870 +"field declarations"); 1871 /* added functionality to have monitors on static fields 1872 } else if (env.isStaticContext()) { 1873 FieldDecl fd = (FieldDecl)ctxt; 1874 ErrorSet.error(fd.locId, 1875 "The monitored annotation can occur only on "+ 1876 "instance field declarations"); 1877 */ 1878 } 1879 break; 1880 } 1881 1882 case TagConstants.NON_NULL: 1883 // NOTE: Part of the NON_NULL check is found in checkTypeDeclElem() 1884 // above, since there's not enough context information here to 1885 // determine whether a formal parameter is declared for a method 1886 // override. 1887 switch (ctxt.getTag()) { 1888 case TagConstants.FORMALPARADECL: 1889 case TagConstants.LOCALVARDECL: 1890 case TagConstants.FIELDDECL: { 1891 GenericVarDecl vd = (GenericVarDecl)ctxt; 1892 if (! Types.isReferenceType(vd.type)) { 1893 ErrorSet.error(vd.locId, 1894 "The non_null pragma can be applied only to "+ 1895 "variables, fields, and parameters of "+ 1896 "reference types"); 1897 } 1898 break; 1899 } 1900 case TagConstants.METHODDECL: { 1901 MethodDecl md = (MethodDecl) ctxt; 1902 if (!Types.isReferenceType(md.returnType)) { 1903 ErrorSet.error(md.getStartLoc(), 1904 "'non_null' can only be used with methods whose "+ 1905 "result type is a reference type"); 1906 } 1907 break; 1908 } 1909 default: 1910 ErrorSet.error(p.getStartLoc(), 1911 "The non_null pragma can be applied only to "+ 1912 "variables, fields, parameters, and methods"); 1913 break; 1914 } 1915 break; 1916 1917 // FIXME - should have a spec_protected case as well ??? 1918 case TagConstants.SPEC_PUBLIC: 1919 case TagConstants.SPEC_PROTECTED: 1920 // JML now allows spec_public and spec_protected on declarations 1921 // of any java accessibiilty 1922 break; 1923 1924 case TagConstants.WRITABLE_DEFERRED: 1925 { 1926 if (ctxt.getTag() != TagConstants.FIELDDECL || 1927 Modifiers.isStatic(((FieldDecl)ctxt).modifiers)) { 1928 ErrorSet.error(p.getStartLoc(), 1929 "The writable_deferred annotation can occur only on " 1930 +"instance field declarations"); 1931 } 1932 break; 1933 } 1934 1935 case TagConstants.INSTANCE: 1936 { 1937 int ctag = ctxt.getTag(); 1938 1939 if (!(ctxt instanceof GhostDeclPragma) && 1940 !(ctxt instanceof ModelDeclPragma)) { 1941 1942 // FIXME - should this use Utils.isModel ??? 1943 if (ctxt instanceof FieldDecl && 1944 (Utils.findModifierPragma( ((FieldDecl)ctxt).pmodifiers, TagConstants.MODEL) != null || 1945 Utils.findModifierPragma( ((FieldDecl)ctxt).pmodifiers, TagConstants.GHOST) != null )) { 1946 // skip 1947 } else { 1948 ErrorSet.error(p.getStartLoc(), 1949 "An instance modifier may only be applied to ghost and model fields"); 1950 } 1951 } 1952 1953 break; 1954 } 1955 1956 case TagConstants.FUNCTION: 1957 // FIXME - do some checking 1958 // must be pure, static, immutable arguments, not void 1959 break; 1960 1961 case TagConstants.PURE: 1962 { 1963 if (ctxt instanceof RoutineDecl) { 1964 } else if (ctxt instanceof TypeDecl) { 1965 } else { 1966 ErrorSet.error(p.getStartLoc(), 1967 "Expected pure to modify a class, interface, constructor or method declaration"); 1968 } 1969 break; 1970 } 1971 1972 case TagConstants.HELPER: 1973 switch (ctxt.getTag()) { 1974 case TagConstants.CONSTRUCTORDECL: 1975 ((ConstructorDecl)ctxt).modifiers |= Modifiers.ACC_HELPER; 1976 break; 1977 case TagConstants.METHODDECL: 1978 { 1979 MethodDecl md = (MethodDecl) ctxt; 1980 md.modifiers |= Modifiers.ACC_HELPER; 1981 if (getOverrideStatus(md) != MSTATUS_NEW_ROUTINE) { 1982 ErrorSet.error(p.getStartLoc(), 1983 "The helper pragma cannot be " + 1984 "applied to a method override"); 1985 } else if (isOverridable(md)) { 1986 ErrorSet.error(p.getStartLoc(), 1987 "The helper pragma cannot be applied " + 1988 "to method that can be overridden"); 1989 } else if (md.body == null) { 1990 ErrorSet.error(p.getStartLoc(), 1991 "The helper pragma cannot be applied " + 1992 "to method without a body"); 1993 } 1994 break; 1995 } 1996 default: 1997 ErrorSet.error(p.getStartLoc(), 1998 "The helper pragma can only be applied to "+ 1999 "methods and constructors"); 2000 break; 2001 } 2002 break; 2003 2004 case TagConstants.IMMUTABLE: 2005 { 2006 if (!(ctxt instanceof TypeDecl)) { 2007 ErrorSet.error(p.getStartLoc(), 2008 "The immutable modifier may be applied only to type declarations"); 2009 } 2010 } 2011 break; 2012 2013 case TagConstants.WRITABLE_IF: 2014 case TagConstants.READABLE_IF: 2015 { 2016 ExprModifierPragma emp = (ExprModifierPragma)p; 2017 2018 if( ctxt.getTag() != TagConstants.FIELDDECL 2019 && ctxt.getTag() != TagConstants.LOCALVARDECL ) { 2020 ErrorSet.error(p.getStartLoc(), 2021 "The " + TagConstants.toString(tag) 2022 +" annotation can occur only on " 2023 +"field declarations and " 2024 +"local variable declarations"); 2025 } 2026 2027 int oldAccessibilityLowerBound = accessibilityLowerBound; 2028 ASTNode oldAccessibilityContext = accessibilityContext; 2029 if (ctxt.getTag() == TagConstants.FIELDDECL) { 2030 FieldDecl fd = (FieldDecl)ctxt; 2031 accessibilityLowerBound = getAccessibility(fd.modifiers); 2032 accessibilityContext = fd; 2033 } 2034 emp.expr = checkPredicate(env, emp.expr); 2035 accessibilityLowerBound = oldAccessibilityLowerBound; 2036 accessibilityContext = oldAccessibilityContext; 2037 break; 2038 } 2039 2040 case TagConstants.NO_WACK_FORALL: 2041 case TagConstants.OLD: 2042 { 2043 VarDeclModifierPragma vd = (VarDeclModifierPragma)p; 2044 LocalVarDecl x = vd.decl; 2045 env.resolveType( sig, vd.decl.type ); 2046 checkTypeModifiers(env, x.type); 2047 javafe.tc.PrepTypeDeclaration.inst. 2048 checkModifiers(x.modifiers, Modifiers.NONE, 2049 x.locId, "local specification variable"); 2050 2051 boolean savedContext = isTwoStateContext; 2052 isTwoStateContext = true; 2053 // The case of x.init==null is illegal and should have 2054 // been caught by the parser. 2055 if (x.init != null) { 2056 //if (x.init instanceof ArrayInit) { 2057 x.init = checkInit(env, x.init, x.type); 2058 //} else { 2059 //checkExpr(newEnv, (Expr)x.init, x.type); 2060 //} 2061 } 2062 isTwoStateContext = savedContext; 2063 // We create the new environment after checking the 2064 // initializer to be sure that the initializer does not 2065 // reference itself. 2066 env = new EnvForGhostLocals(env,x); 2067 break; 2068 } 2069 2070 case TagConstants.ALSO_REQUIRES: 2071 case TagConstants.REQUIRES: 2072 case TagConstants.PRECONDITION: 2073 { 2074 ExprModifierPragma emp = (ExprModifierPragma)p; 2075 2076 if( ctxt instanceof InitBlock ) { 2077 if (emp.expr.getTag() != TagConstants.NOTSPECIFIEDEXPR) 2078 emp.expr = checkPredicate(env, emp.expr); 2079 } else if( ctxt instanceof RoutineDecl ) { 2080 RoutineDecl rd = (RoutineDecl)ctxt; 2081 2082 int ms = getOverrideStatus(rd); 2083 2084 Env newenv = env; 2085 /* Interpret constructor as acting on an existing object, to initialize it, 2086 so this and fields are in scope. 2087 if (rd instanceof ConstructorDecl) { 2088 newenv = env.asStaticContext(); 2089 } 2090 */ 2091 int oldAccessibilityLowerBound = accessibilityLowerBound; 2092 ASTNode oldAccessibilityContext = accessibilityContext; 2093 accessibilityLowerBound = getAccessibility(rd.modifiers); 2094 accessibilityContext = rd; 2095 if (emp.expr.getTag() != TagConstants.NOTSPECIFIEDEXPR) 2096 emp.expr = checkPredicate(newenv, emp.expr); 2097 accessibilityLowerBound = oldAccessibilityLowerBound; 2098 accessibilityContext = oldAccessibilityContext; 2099 } else { 2100 ErrorSet.error(p.getStartLoc(), TagConstants.toString(tag) + 2101 " annotations can occur only on method" + 2102 ((tag == TagConstants.REQUIRES || 2103 tag == TagConstants.PRECONDITION) ? " and constructor" : "") + 2104 " declarations"); 2105 } 2106 break; 2107 } 2108 2109 case TagConstants.MEASURED_BY: 2110 case TagConstants.DURATION: 2111 case TagConstants.WORKING_SPACE: 2112 { 2113 CondExprModifierPragma emp = (CondExprModifierPragma)p; 2114 2115 if( !(ctxt instanceof RoutineDecl ) ) { 2116 ErrorSet.error(p.getStartLoc(), 2117 TagConstants.toString(tag) 2118 +" annotations can occur only on " 2119 +"method and constructor declarations"); 2120 } else { 2121 RoutineDecl rd = (RoutineDecl)ctxt; 2122 boolean oldIsRESContext = isRESContext; 2123 boolean oldIsTwoStateContext = isTwoStateContext; 2124 boolean oldIsPrivFieldAccessAllowed = isPrivateFieldAccessAllowed; 2125 isRESContext = true; 2126 isTwoStateContext = true; 2127 // If "rd" is an overridable method, then every private field 2128 // mentioned in "emp.expr" must be spec_public. 2129 if (rd instanceof MethodDecl && isOverridable((MethodDecl)rd)) { 2130 isPrivateFieldAccessAllowed = false; 2131 } 2132 try { 2133 if (tag == TagConstants.MEASURED_BY) { 2134 // FIXME - what type to use? 2135 emp.expr = checkExpr(env, emp.expr); 2136 } else if (emp.expr.getTag() != TagConstants.NOTSPECIFIEDEXPR) 2137 emp.expr = checkExpr(env, emp.expr, Types.longType); 2138 if (emp.cond != null) 2139 emp.cond = checkExpr(env, emp.cond, Types.booleanType); 2140 } finally { 2141 isRESContext = oldIsRESContext; 2142 isTwoStateContext = oldIsTwoStateContext; 2143 isPrivateFieldAccessAllowed = oldIsPrivFieldAccessAllowed; 2144 } 2145 } 2146 break; 2147 } 2148 2149 case TagConstants.DIVERGES: 2150 if (ctxt instanceof RoutineDecl) { 2151 RoutineDecl rd = (RoutineDecl)ctxt; 2152 if (Utils.isPure(rd)) { 2153 ExprModifierPragma emp = (ExprModifierPragma)p; 2154 if (emp.expr instanceof LiteralExpr && 2155 ((LiteralExpr)emp.expr).value == Boolean.FALSE) { 2156 // OK 2157 } else if (p.getStartLoc() == Location.NULL) { 2158 // Default clause - ignore it and deal with it during desugaring 2159 } else { 2160 int locp = Utils.findPurePragma(rd).getStartLoc(); 2161 int loc = p.getStartLoc(); 2162 if (loc == Location.NULL) { 2163 ErrorSet.error(locp, 2164 "A lightweight specification case for a pure method must have a 'diverges false' clause"); 2165 } else { 2166 ErrorSet.error(loc, 2167 "A pure method may not have a diverges clause", 2168 locp); 2169 } 2170 } 2171 } 2172 } 2173 // fall-through 2174 case TagConstants.ENSURES: 2175 case TagConstants.ALSO_ENSURES: 2176 case TagConstants.POSTCONDITION: 2177 case TagConstants.WHEN: 2178 { 2179 ExprModifierPragma emp = (ExprModifierPragma)p; 2180 2181 if( ctxt instanceof InitBlock ) { 2182 boolean oldIsRESContext = isRESContext; 2183 boolean oldIsTwoStateContext = isTwoStateContext; 2184 boolean oldIsPrivFieldAccessAllowed = isPrivateFieldAccessAllowed; 2185 try { 2186 isRESContext = true; 2187 isTwoStateContext = true; 2188 if (emp.expr.getTag() != TagConstants.NOTSPECIFIEDEXPR) 2189 emp.expr = checkPredicate(env, emp.expr); 2190 } finally { 2191 isRESContext = oldIsRESContext; 2192 isTwoStateContext = oldIsTwoStateContext; 2193 isPrivateFieldAccessAllowed = oldIsPrivFieldAccessAllowed; 2194 } 2195 } else if( ctxt instanceof RoutineDecl ) { 2196 RoutineDecl rd = (RoutineDecl)ctxt; 2197 escjava.ast.Utils.owningDecl.set(emp,rd); 2198 boolean oldIsRESContext = isRESContext; 2199 boolean oldIsTwoStateContext = isTwoStateContext; 2200 boolean oldIsPrivFieldAccessAllowed = isPrivateFieldAccessAllowed; 2201 isRESContext = true; 2202 isTwoStateContext = true; 2203 // If "rd" is an overridable method, then every private field 2204 // mentioned in "emp.expr" must be spec_public. 2205 if (rd instanceof MethodDecl && isOverridable((MethodDecl)rd)) { 2206 isPrivateFieldAccessAllowed = false; 2207 } 2208 try { 2209 if (emp.expr.getTag() != TagConstants.NOTSPECIFIEDEXPR) 2210 emp.expr = checkPredicate(env, emp.expr); 2211 } finally { 2212 isRESContext = oldIsRESContext; 2213 isTwoStateContext = oldIsTwoStateContext; 2214 isPrivateFieldAccessAllowed = oldIsPrivFieldAccessAllowed; 2215 } 2216 } else { 2217 ErrorSet.error(p.getStartLoc(), 2218 TagConstants.toString(tag) 2219 +" annotations can occur only on " 2220 +"initializer, method and constructor declarations"); 2221 } 2222 break; 2223 } 2224 2225 2226 case TagConstants.SIGNALS: 2227 { 2228 tag = p.originalTag(); 2229 VarExprModifierPragma vemp = (VarExprModifierPragma)p; 2230 2231 if( !(ctxt instanceof RoutineDecl ) ) { 2232 ErrorSet.error(p.getStartLoc(), 2233 TagConstants.toString(tag) 2234 +" annotations can occur only on " 2235 +"method and constructor declarations"); 2236 } else { 2237 RoutineDecl rd = (RoutineDecl)ctxt; 2238 2239 // Resolve type and check that it is a subtype of Throwable 2240 // and comparable to some type mentioned in the throws set. 2241 env.resolveType(sig,vemp.arg.type); 2242 //TypeSig top = Main.options().useThrowable ? 2243 // Types.javaLangThrowable() : Types.javaLangException(); 2244 TypeSig top = Types.javaLangThrowable(); 2245 // FIXME - JML actually requires that the var be a subtype of 2246 // Exception, but the original Esc/Java did not 2247 if (!Types.isSubclassOf(vemp.arg.type,top)) { 2248 ErrorSet.error(vemp.arg.type.getStartLoc(), 2249 "The type of the " + 2250 TagConstants.toString(tag) + 2251 " argument must be a subtype of " + 2252 Types.printName(top)); 2253 } else { 2254 // "vemp.arg.type" is a subclass of "Throwable", so it 2255 // must be a "TypeName" or a "TypeSig" 2256 TypeSig ssig; 2257 if (vemp.arg.type instanceof TypeSig) { 2258 ssig = (TypeSig)vemp.arg.type; 2259 } else { 2260 ssig = TypeSig.getSig((TypeName)vemp.arg.type); 2261 } 2262 boolean okay = false; 2263 for (int i = 0; i < rd.raises.size(); i++) { 2264 TypeName tn = rd.raises.elementAt(i); 2265 TypeSig tsig = TypeSig.getSig(tn); 2266 if (Types.isSubclassOf(ssig, tsig) || 2267 Types.isSubclassOf(tsig, ssig)) { 2268 okay = true; 2269 break; 2270 } 2271 } 2272 /* FIXME - what about Error exceptions, must they be mentioned? */ 2273 /* FIXME 2274 if (!okay) { 2275 if (!( (vemp.expr instanceof LiteralExpr) && 2276 ((LiteralExpr)vemp.expr).value.equals(Boolean.FALSE))) { 2277 ErrorSet.error(vemp.arg.type.getStartLoc(), 2278 "The type of the " + 2279 TagConstants.toString(tag) + 2280 " argument must be comparable to some type"+ 2281 " mentioned in the routine's throws set"); 2282 } 2283 } 2284 */ 2285 } 2286 2287 if (tag == TagConstants.SIGNALS_ONLY) { 2288 // Check that all Exceptions listed are either in the 2289 // throws list or are RuntimeExceptions 2290 2291 // FIXME 2292 2293 } 2294 2295 Env subenv = new EnvForLocals(env, vemp.arg); 2296 // FIXME - below we say that this is a twostate context, in which case we should not set this to static??? 2297 /* 2298 if (rd instanceof ConstructorDecl) { 2299 subenv = subenv.asStaticContext(); 2300 } 2301 */ 2302 2303 // Check the expression to be an appropriate predicate 2304 boolean oldIsTwoStateContext = isTwoStateContext; 2305 boolean oldIsPrivFieldAccessAllowed = isPrivateFieldAccessAllowed; 2306 isTwoStateContext = true; 2307 // If "rd" is an overridable method, then every private field 2308 // mentioned in "emp.expr" must be spec_public. 2309 if (rd instanceof MethodDecl && isOverridable((MethodDecl)rd)) { 2310 isPrivateFieldAccessAllowed = false; 2311 } 2312 try { 2313 if (vemp.expr.getTag() != TagConstants.NOTSPECIFIEDEXPR) 2314 vemp.expr = checkPredicate(subenv, vemp.expr); 2315 } finally { 2316 isTwoStateContext = oldIsTwoStateContext; 2317 isPrivateFieldAccessAllowed = oldIsPrivFieldAccessAllowed; 2318 } 2319 } 2320 break; 2321 } 2322 2323 2324 case TagConstants.MONITORED_BY: { 2325 ExprModifierPragma emp = (ExprModifierPragma)p; 2326 2327 if (ctxt.getTag() != TagConstants.FIELDDECL) { 2328 ErrorSet.error(emp.loc, 2329 "The monitored_by annotation can occur only on "+ 2330 "field declarations"); 2331 } else { 2332 FieldDecl fd = (FieldDecl)ctxt; 2333 2334 int oldAccessibilityLowerBound = accessibilityLowerBound; 2335 ASTNode oldAccessibilityContext = accessibilityContext; 2336 accessibilityLowerBound = getAccessibility(fd.modifiers); 2337 accessibilityContext = fd; 2338 emp.expr = checkExpr(env, emp.expr, Types.javaLangObject()); 2339 accessibilityLowerBound = oldAccessibilityLowerBound; 2340 accessibilityContext = oldAccessibilityContext; 2341 } 2342 break; 2343 } 2344 2345 case TagConstants.MODIFIESGROUPPRAGMA: { 2346 ModifiesGroupPragma mg = (ModifiesGroupPragma)p; 2347 if (ctxt instanceof InitBlock || ctxt instanceof RoutineDecl) { 2348 CondExprModifierPragmaVec v = mg.items; 2349 for (int i=0; i<v.size(); ++i) { 2350 checkModifierPragma(v.elementAt(i),ctxt,env); 2351 } 2352 if (mg.precondition != null) 2353 mg.precondition = checkPredicate(env,mg.precondition); // FIXME - pre environment ? 2354 } else { 2355 ErrorSet.error(mg.clauseLoc, 2356 "A modifies annotation " + 2357 "can occur only on " + 2358 "method and constructor declarations"); 2359 } 2360 break; 2361 } 2362 2363 case TagConstants.MODIFIES: 2364 case TagConstants.ASSIGNABLE: 2365 case TagConstants.MODIFIABLE: 2366 case TagConstants.STILL_DEFERRED: { 2367 CondExprModifierPragma emp = (CondExprModifierPragma)p; 2368 2369 if ((ctxt instanceof RoutineDecl ) ) { 2370 RoutineDecl rd = (RoutineDecl)ctxt; 2371 2372 Assert.notFalse(!isSpecDesignatorContext); 2373 isSpecDesignatorContext = true; 2374 Env newenv = env; 2375 /* 2376 // But we do need to allow the fields of this in the modifies clause, which 2377 // using the static context does not permit. 2378 if (rd instanceof ConstructorDecl) { 2379 // disallow "this" from constructor "modifies" clauses 2380 newenv = env.asStaticContext(); 2381 } 2382 */ 2383 emp.expr = checkDesignator(newenv, emp.expr); 2384 switch (emp.expr.getTag()) { 2385 case TagConstants.FIELDACCESS: { 2386 FieldAccess fa = (FieldAccess)emp.expr; 2387 if (fa.decl != null && 2388 (ctxt instanceof MethodDecl) && // FIXME - what about constructors 2389 Modifiers.isFinal(fa.decl.modifiers) && 2390 // The array "length" field has already been checked 2391 // insuper.checkDesignator(). 2392 fa.decl != Types.lengthFieldDecl) { 2393 2394 // java.lang.System has fields in, out, err that are special 2395 // cases. Somehow, Java allows them to be final and yet be 2396 // modified by public routines. Instead of a general 2397 // mechanism, we just do a special case here. 2398 if (fa.decl.parent != Types.javaLangSystem().getTypeDecl()) 2399 ErrorSet.caution(fa.locId, "a final field is not allowed as " + 2400 "the designator in a modifies clause"); 2401 } 2402 break; 2403 } 2404 2405 case TagConstants.ARRAYREFEXPR: 2406 case TagConstants.ARRAYRANGEREFEXPR: 2407 case TagConstants.WILDREFEXPR: 2408 case TagConstants.EVERYTHINGEXPR: 2409 case TagConstants.NOTHINGEXPR: 2410 case TagConstants.NOTSPECIFIEDEXPR: 2411 break; 2412 2413 default: 2414 if (escjava.parser.EscPragmaParser. 2415 informalPredicateDecoration.get(emp.expr)==null) { 2416 // The expression is not a designator 2417 // but we allow an informal predicate 2418 if (!Types.isErrorType(getType(emp.expr))) 2419 ErrorSet.error(emp.expr.getStartLoc(), 2420 "Not a specification designator expression"); 2421 } else { 2422 emp.expr = null; 2423 } 2424 } 2425 if (rd instanceof MethodDecl && Utils.isPure(rd) && 2426 emp.expr != null && emp.expr.getTag() != TagConstants.NOTHINGEXPR) { 2427 ErrorSet.error(p.getStartLoc(), 2428 "A pure method may not have a modifies clause", 2429 Utils.findPurePragma(rd).getStartLoc()); 2430 } 2431 if (rd instanceof ConstructorDecl && Utils.isPure(rd) && 2432 emp.expr != null && 2433 !(emp.expr.getTag() == TagConstants.NOTHINGEXPR || 2434 (emp.expr.getTag() == TagConstants.WILDREFEXPR && 2435 (((WildRefExpr)emp.expr).var instanceof ThisExpr) && 2436 ((ThisExpr)((WildRefExpr)emp.expr).var).classPrefix == null) 2437 || 2438 ((emp.expr instanceof FieldAccess) && 2439 Types.isSubclassOf( 2440 TypeSig.getSig(rd.parent), 2441 TypeSig.getSig(((FieldAccess)emp.expr).decl.parent) 2442 ) 2443 )) 2444 ) { 2445 ErrorSet.error(p.getStartLoc(), 2446 "A pure constructor may not have a modifies clause", 2447 Utils.findPurePragma(rd).getStartLoc()); 2448 } 2449 isSpecDesignatorContext = false; 2450 if (emp.cond != null) emp.cond = checkExpr(newenv, emp.cond); 2451 } 2452 break; 2453 } 2454 2455 case TagConstants.ALSO: 2456 case TagConstants.ALSO_REFINE: 2457 case TagConstants.MODEL_PROGRAM: 2458 case TagConstants.CODE_CONTRACT: 2459 case TagConstants.BEHAVIOR: 2460 case TagConstants.CLOSEPRAGMA: 2461 case TagConstants.EXAMPLE: 2462 case TagConstants.EXCEPTIONAL_BEHAVIOR: 2463 case TagConstants.EXCEPTIONAL_EXAMPLE: 2464 case TagConstants.FOR_EXAMPLE: 2465 case TagConstants.IMPLIES_THAT: 2466 case TagConstants.NORMAL_BEHAVIOR: 2467 case TagConstants.NORMAL_EXAMPLE: 2468 case TagConstants.OPENPRAGMA: 2469 // Desugaring happens before type-checking, 2470 // This shouldn't happen. 2471 break; 2472 2473 case TagConstants.GHOST: 2474 case TagConstants.MODEL: 2475 break; 2476 2477 case TagConstants.NESTEDMODIFIERPRAGMA: 2478 { 2479 java.util.ArrayList list = ((NestedModifierPragma)p).list; 2480 java.util.Iterator i = list.iterator(); 2481 while (i.hasNext()) { 2482 ModifierPragmaVec mpv = (ModifierPragmaVec)i.next(); 2483 checkModifierPragmaVec(mpv,ctxt,env); 2484 } 2485 break; 2486 } 2487 2488 case TagConstants.PARSEDSPECS: 2489 { 2490 escjava.ParsedRoutineSpecs pp = ((ParsedSpecs)p).specs; 2491 java.util.Iterator i = pp.specs.iterator(); 2492 while (i.hasNext()) { 2493 checkModifierPragmaVec((ModifierPragmaVec)i.next(),ctxt,env); 2494 } 2495 i = pp.impliesThat.iterator(); 2496 while (i.hasNext()) { 2497 checkModifierPragmaVec((ModifierPragmaVec)i.next(),ctxt,env); 2498 } 2499 i = pp.examples.iterator(); 2500 while (i.hasNext()) { 2501 checkModifierPragmaVec((ModifierPragmaVec)i.next(),ctxt,env); 2502 } 2503 /* This duplicates stuff 2504 // The last element is the ParsedSpecs containing all the 2505 // clauses etc. 2506 ModifierPragmaVec mpv = pp.modifiers; 2507 ModifierPragma last = mpv.elementAt(mpv.size()-1); 2508 mpv.removeElementAt(mpv.size()-1); 2509 checkModifierPragmaVec(mpv,ctxt,env); 2510 mpv.addElement(last); 2511 */ 2512 break; 2513 } 2514 2515 case TagConstants.MAPS: { 2516 Identifier fid = ((FieldDecl)ctxt).id; 2517 MapsExprModifierPragma ep = (MapsExprModifierPragma)p; 2518 //System.out.println("FOUND " + TagConstants.toString(tag) + " for " + fid + " " + ep.id); 2519 if (ep.expr != null) ep.expr = checkExpr(env,ep.expr); 2520 isSpecDesignatorContext = true; 2521 if (ep.mapsexpr != null) ep.mapsexpr = checkDesignator(env,ep.mapsexpr); 2522 isSpecDesignatorContext = false; 2523 Expr e = ep.expr; 2524 if (e == null || TypeCheck.inst.getType(e) == Types.errorType) { 2525 // skip 2526 } else if (e instanceof FieldAccess) { 2527 FieldAccess fe = (FieldAccess)e; // datagroup 2528 FieldDecl fd = (FieldDecl)ctxt; // field with which maps decl is associated 2529 if (Modifiers.isStatic( fe.decl.modifiers) 2530 && !Modifiers.isStatic( fd.modifiers) ){ 2531 ErrorSet.error(((FieldDecl)ctxt).getStartLoc(), 2532 "An instance field may not be added to a static datagroup", 2533 fe.decl.getStartLoc()); 2534 } else { 2535 Datagroups.add(fd.parent,fe.decl,ep.mapsexpr); 2536 } 2537 } else { 2538 ErrorSet.error(e.getStartLoc(), 2539 "Expected a field reference here, found " + 2540 e.getClass()); 2541 } 2542 break; 2543 } 2544 2545 case TagConstants.IN: { 2546 MapsExprModifierPragma ep = (MapsExprModifierPragma)p; 2547 if (ep.expr != null) ep.expr = checkExpr(env,ep.expr); 2548 Expr e = ep.expr; 2549 if (e == null || TypeCheck.inst.getType(e) == Types.errorType) { 2550 } else if (e instanceof FieldAccess) { 2551 FieldAccess fe = (FieldAccess)e; // datagroup 2552 FieldDecl fd = (FieldDecl)ctxt; // field being put in the datagroup 2553 Expr eva = AmbiguousVariableAccess.make( 2554 SimpleName.make(fd.id,fd.getStartLoc())); 2555 eva = checkExpr(env,eva); 2556 if (Modifiers.isStatic( fe.decl.modifiers ) && 2557 !Modifiers.isStatic(fd.modifiers)) { 2558 ErrorSet.error(fd.getStartLoc(), 2559 "An instance field may not be added to a static datagroup", 2560 fe.decl.getStartLoc()); 2561 } else { 2562 Datagroups.add(fd.parent,fe.decl,eva); 2563 } 2564 } else { 2565 ErrorSet.error(e.getStartLoc(), 2566 "Expected a field reference here, found " + 2567 e.getClass()); 2568 } 2569 break; 2570 } 2571 2572 case TagConstants.READONLY: 2573 case TagConstants.PEER: 2574 case TagConstants.REP: 2575 // FIXME - need to support these 2576 break; 2577 2578 default: 2579 ErrorSet.error(p.getStartLoc(), 2580 "Ignored unexpected " + 2581 TagConstants.toString(tag) + 2582 " tag"); 2583 break; 2584 } 2585 } finally { 2586 inAnnotation = savedInAnnotation; 2587 } 2588 return env; 2589 } 2590 2591 /** 2592 * @return whether or not <code>md</code> can be overridden in some possible 2593 * subclass. 2594 */ 2595 2596 public static boolean isOverridable(/*@ non_null */ MethodDecl md) { 2597 return !(Modifiers.isPrivate(md.modifiers) || 2598 Modifiers.isFinal(md.modifiers) || 2599 Modifiers.isFinal(md.parent.modifiers) || 2600 Modifiers.isStatic(md.modifiers)); 2601 } 2602 2603 /** 2604 * @return a value appropriate for assignment to 2605 * <code>accessibilityLowerBound</code>, given member modifiers. 2606 */ 2607 2608 protected int getAccessibility(int modifiers) { 2609 if (Modifiers.isPrivate(modifiers)) { 2610 return ACC_LOW_BOUND_Private; 2611 } else if (Modifiers.isPackage(modifiers)) { 2612 return ACC_LOW_BOUND_Package; 2613 } else if (Modifiers.isProtected(modifiers)) { 2614 return ACC_LOW_BOUND_Protected; 2615 } else { 2616 Assert.notFalse(Modifiers.isPublic(modifiers)); 2617 return ACC_LOW_BOUND_Public; 2618 } 2619 } 2620 2621 protected Env checkStmtPragma(Env e, StmtPragma s) { 2622 boolean savedInAnnotation = inAnnotation; 2623 inAnnotation = true; // Must be reset before we exit! 2624 boolean savedTwoStateContext = isTwoStateContext; 2625 isTwoStateContext = true; 2626 try { 2627 int tag = s.getTag(); 2628 switch(tag) { 2629 case TagConstants.UNREACHABLE: 2630 break; 2631 2632 case TagConstants.SETSTMTPRAGMA: { 2633 SetStmtPragma set = (SetStmtPragma)s; 2634 set.target = checkExpr(e, set.target); 2635 set.value = checkExpr(e, set.value); 2636 checkBinaryExpr(TagConstants.ASSIGN, set.target, 2637 set.value, set.locOp); 2638 Expr t = set.target; 2639 int nonGhostLoc = isGhost(t); 2640 if (nonGhostLoc != 0) { 2641 ErrorSet.error(s.getStartLoc(),"May use set only with assignment targets that are declared ghost",nonGhostLoc); 2642 } 2643 /* 2644 if (t instanceof FieldAccess && 2645 ((FieldAccess)t).decl == Types.lengthFieldDecl) { 2646 ErrorSet.error(s.getStartLoc(),"The length field of an array may not be set"); 2647 } 2648 */ 2649 break; 2650 } 2651 2652 case TagConstants.HENCE_BY: 2653 case TagConstants.ASSUME: 2654 case TagConstants.ASSERT: 2655 { 2656 ExprStmtPragma es = (ExprStmtPragma)s; 2657 es.expr = checkPredicate(e, es.expr); 2658 if (es.label != null) 2659 es.label = checkExpr(e, es.label); 2660 break; 2661 } 2662 2663 case TagConstants.LOOP_INVARIANT: 2664 case TagConstants.MAINTAINING: 2665 { 2666 ExprStmtPragma lis = (ExprStmtPragma)s; 2667 loopInvariants.addElement(lis); 2668 break; 2669 } 2670 2671 case TagConstants.DECREASES: 2672 case TagConstants.DECREASING: 2673 { 2674 ExprStmtPragma lis = (ExprStmtPragma)s; 2675 loopDecreases.addElement(lis); 2676 break; 2677 } 2678 2679 case TagConstants.LOOP_PREDICATE: 2680 { 2681 ExprStmtPragma lis = (ExprStmtPragma)s; 2682 loopPredicates.addElement(lis); 2683 break; 2684 } 2685 2686 case TagConstants.SKOLEMCONSTANTPRAGMA: 2687 { 2688 SkolemConstantPragma p = (SkolemConstantPragma)s; 2689 skolemConstants.append(p.decls); 2690 break; 2691 } 2692 2693 default: 2694 Assert.fail("Unexpected tag " + tag +" "+s + 2695 " " + Location.toString(s.getStartLoc())); 2696 } 2697 } finally { 2698 inAnnotation = savedInAnnotation; 2699 isTwoStateContext = savedTwoStateContext; 2700 } 2701 return e; 2702 } 2703 2704 2705 // Utility routines 2706 2707 /** 2708 * Copy the Type associated with an expression by the typechecking pass to 2709 * another Expr. This is used by Substitute to ensure it returns an Expr of the 2710 * same Type. 2711 */ 2712 public static void copyType(VarInit from, VarInit to) { 2713 Type t = getTypeOrNull(from); 2714 if (t != null) 2715 setType(to, t); 2716 } 2717 2718 /** 2719 * @return a set of *all* the methods a given method overrides. This includes 2720 * transitivity. 2721 */ 2722 //@ requires md != null; 2723 //@ ensures \result != null; 2724 //@ ensures \result.elementType == \type(MethodDecl); 2725 public static Set getAllOverrides(MethodDecl md) { 2726 Set direct = javafe.tc.PrepTypeDeclaration.inst.getOverrides(md.parent, md); 2727 Set result = new Set(); 2728 2729 Enumeration e = direct.elements(); 2730 while (e.hasMoreElements()) { 2731 MethodDecl directMD = (MethodDecl)(e.nextElement()); 2732 result.add(directMD); 2733 result.addEnumeration(getAllOverrides(directMD).elements()); 2734 } 2735 2736 return result; 2737 } 2738 2739 public static javafe.util.Set getDirectOverrides(MethodDecl md) { 2740 return javafe.tc.PrepTypeDeclaration.inst.getOverrides(md.parent, md); 2741 } 2742 2743 /** 2744 * @return If <code>md</code> is a method that overrides a method in a 2745 * superclass, the overridden method is returned. Otherwise, if <code>md</code> 2746 * overrides a method in an interface, such a method is returned. Otherwise, 2747 * <code>null</code> is returned. 2748 */ 2749 2750 public static MethodDecl getSuperClassOverride(MethodDecl md) { 2751 MethodDecl classOverride = null; 2752 MethodDecl interfaceOverride = null; 2753 Set direct = javafe.tc.PrepTypeDeclaration.inst.getOverrides(md.parent, md); 2754 Enumeration e = direct.elements(); 2755 while (e.hasMoreElements()) { 2756 MethodDecl directMD = (MethodDecl)(e.nextElement()); 2757 if (directMD.parent instanceof ClassDecl) { 2758 if (classOverride == null) { 2759 classOverride = directMD; 2760 } else { 2761 Assert.fail("we think this can no longer happen!"); 2762 // This suggests that the method is inherited from TWO classes! 2763 // This can actually happen, if the method is one that is 2764 // declared in Object, because every interface has the methods of 2765 // Object. In this case, pick the method override that does not 2766 // reside in Object. 2767 Type javaLangObject = Types.javaLangObject(); 2768 Type t0 = TypeSig.getSig(classOverride.parent); 2769 Type t1 = TypeSig.getSig(directMD.parent); 2770 Assert.notFalse(Types.isSameType(t0, javaLangObject) || 2771 Types.isSameType(t1, javaLangObject)); 2772 Assert.notFalse(!Types.isSameType(t0, javaLangObject) || 2773 !Types.isSameType(t1, javaLangObject)); 2774 if (!Types.isSameType(t1, javaLangObject)) { 2775 classOverride = directMD; 2776 } 2777 } 2778 } else { 2779 interfaceOverride = directMD; 2780 } 2781 } 2782 if (classOverride != null) { 2783 return classOverride; 2784 } else { 2785 return interfaceOverride; 2786 } 2787 } 2788 2789 /** 2790 * @return whether or not <code>rd</code> is a method override declaration, that 2791 * is, whether or not <code>rd</code> overrides a method declared in a superclass 2792 * or superinterface. 2793 */ 2794 2795 public static boolean isMethodOverride(RoutineDecl rd) { 2796 return getOverrideStatus(rd) != MSTATUS_NEW_ROUTINE; 2797 } 2798 2799 static public final int MSTATUS_NEW_ROUTINE = 0; 2800 static public final int MSTATUS_CLASS_NEW_METHOD = 1; 2801 static public final int MSTATUS_OVERRIDE = 2; 2802 2803 /** 2804 * @return <code>MSTATUS_NEW_ROUTINE</code> if <code>rd</code> is a routine that 2805 * doesn't override any other method. This includes the case where 2806 * <code>rd</code> is a constructor or a static method. 2807 * 2808 * <p> Returns <code>MSTATUS_CLASS_NEW_METHOD</code> if <code>rd</code> is a 2809 * method declared in a class, doesn't override any method in any superclass, but 2810 * overrides a method in an interface. 2811 * 2812 * <p> Otherwise, returns <code>MSTATUS_OVERRIDE</code>. 2813 */ 2814 2815 /*@ ensures \result == MSTATUS_NEW_ROUTINE || 2816 @ \result == MSTATUS_CLASS_NEW_METHOD || 2817 @ \result == MSTATUS_OVERRIDE; 2818 */ 2819 public static int getOverrideStatus(/*@ non_null */ RoutineDecl rd) { 2820 if (!(rd instanceof MethodDecl) || Modifiers.isStatic(rd.modifiers)) { 2821 return MSTATUS_NEW_ROUTINE; 2822 } 2823 MethodDecl md = (MethodDecl)rd; 2824 2825 Set direct = javafe.tc.PrepTypeDeclaration.inst.getOverrides(md.parent, md); 2826 if (direct.size() == 0) { 2827 return MSTATUS_NEW_ROUTINE; 2828 } 2829 if (!(md.parent instanceof ClassDecl)) { 2830 return MSTATUS_OVERRIDE; 2831 } 2832 2833 Enumeration e = direct.elements(); 2834 while (e.hasMoreElements()) { 2835 MethodDecl directMD = (MethodDecl)(e.nextElement()); 2836 if (directMD.parent instanceof ClassDecl) { 2837 return MSTATUS_OVERRIDE; 2838 } 2839 } 2840 return MSTATUS_CLASS_NEW_METHOD; 2841 } 2842 2843 /** 2844 * @return null if method md is allowed to declare its jth (counting from 0) 2845 * formal parameter as non_null. That is the case if the method does not 2846 * override anything, or if in everything that it does override that parameter is 2847 * declared non_null. Otherwise returns the MethodDecl corresponding to the 2848 * overridden method with which the argument rd is in conflict. 2849 */ 2850 static public MethodDecl getSuperNonNullStatus(RoutineDecl rd, int j) { 2851 if (!(rd instanceof MethodDecl) || Modifiers.isStatic(rd.modifiers)) { 2852 return null; 2853 } 2854 MethodDecl md = (MethodDecl)rd; 2855 2856 Set direct = javafe.tc.PrepTypeDeclaration.inst.getOverrides(md.parent, md); 2857 if (direct.size() == 0) { 2858 return null; 2859 } 2860 return getSuperNonNullStatus(rd,j,direct); 2861 } 2862 2863 static public MethodDecl getSuperNonNullStatus(RoutineDecl rd, int j, Set directOverrides) { 2864 Enumeration e = directOverrides.elements(); 2865 while (e.hasMoreElements()) { 2866 MethodDecl directMD = (MethodDecl)(e.nextElement()); 2867 FormalParaDecl f = directMD.args.elementAt(j); 2868 if (Utils.findModifierPragma(f,TagConstants.NON_NULL) == null) 2869 return directMD; 2870 } 2871 return null; 2872 } 2873 2874 /** Returns non-zero if the expression is a ghost expression - that is, it 2875 would not exist if all ghost declarations were removed. Otherwise 2876 returns a Location value of a relevant non-ghost declaration. 2877 */ 2878 public int isGhost(Expr t) { 2879 if (t instanceof ArrayRefExpr) { 2880 t = ((ArrayRefExpr)t).array; 2881 } 2882 if (t instanceof FieldAccess) { 2883 FieldAccess fa = (FieldAccess)t; 2884 if (fa.decl == null || GhostEnv.isGhostField(fa.decl)) 2885 return 0; 2886 int gl = isGhost(fa.od); 2887 if (gl == 0) return 0; 2888 if (gl == -1) return fa.decl.getStartLoc(); 2889 return gl; 2890 } else if (t instanceof VariableAccess) { 2891 VariableAccess va = (VariableAccess)t; 2892 GenericVarDecl gd = va.decl; 2893 if ( Utils.findModifierPragma( 2894 gd.pmodifiers,TagConstants.GHOST) == null) 2895 return gd.getStartLoc(); 2896 } else if (t instanceof ParenExpr) { 2897 return isGhost( ((ParenExpr)t).expr ); 2898 } else if (t instanceof CastExpr) { 2899 return isGhost( ((CastExpr)t).expr ); 2900 } 2901 return 0; 2902 // FIXME - need some test that the expression in advance of 2903 // a . in a field reference or the [] in an array reference 2904 // only designates ghost fields/variables 2905 // e.g. what about method calls, operator expressions? 2906 2907 } 2908 2909 public int isGhost(ObjectDesignator od) { 2910 if (od instanceof ExprObjectDesignator) { 2911 Expr e = ((ExprObjectDesignator)od).expr; 2912 if (e == null || e instanceof ThisExpr) return -1; 2913 return isGhost(e); 2914 } 2915 return -1; // OK for TypeObjectDesignator and SuperObjectDesignator 2916 } 2917 2918 protected boolean assignmentConvertable(Expr e, Type t) { 2919 if (super.assignmentConvertable(e,t)) return true; 2920 return Types.isTypeType(t) && Types.isTypeType(getType(e)); 2921 } 2922 2923 } // end of class FlowInsensitiveChecks 2924 2925 /* 2926 * Local Variables: 2927 * Mode: Java 2928 * fill-column: 85 2929 * End: 2930 */