001 // This class is generated as part of the 2003 Revision of the ESC Tools 002 // Author: David Cok 003 004 package escjava; 005 006 import java.util.ArrayList; 007 import java.util.Iterator; 008 009 import javafe.ast.ASTNode; 010 import javafe.ast.BinaryExpr; 011 import javafe.ast.CompilationUnit; 012 import javafe.ast.ConstructorDecl; 013 import javafe.ast.Expr; 014 import javafe.ast.ExprObjectDesignator; 015 import javafe.ast.ExprVec; 016 import javafe.ast.FormalParaDecl; 017 import javafe.ast.FormalParaDeclVec; 018 import javafe.ast.Identifier; 019 import javafe.ast.InstanceOfExpr; 020 import javafe.ast.InterfaceDecl; 021 import javafe.ast.LexicalPragma; 022 import javafe.ast.LiteralExpr; 023 import javafe.ast.MethodDecl; 024 import javafe.ast.MethodInvocation; 025 import javafe.ast.ModifierPragma; 026 import javafe.ast.ModifierPragmaVec; 027 import javafe.ast.NewInstanceExpr; 028 import javafe.ast.PrettyPrint; 029 import javafe.ast.RoutineDecl; 030 import javafe.ast.ThisExpr; 031 import javafe.ast.Type; 032 import javafe.ast.TypeName; 033 import javafe.ast.TypeNameVec; 034 import javafe.ast.TypeDecl; 035 import javafe.ast.TypeDeclElem; 036 import javafe.ast.TypeDeclElemVec; 037 import javafe.ast.TypeDeclVec; 038 import javafe.ast.VariableAccess; 039 import javafe.tc.TypeSig; 040 import javafe.tc.Types; 041 import javafe.util.ErrorSet; 042 import javafe.util.Location; 043 import escjava.ast.CondExprModifierPragma; 044 import escjava.ast.EscPrettyPrint; 045 import escjava.ast.EverythingExpr; 046 import escjava.ast.ExprModifierPragma; 047 import escjava.ast.GenericVarDeclVec; 048 import escjava.ast.ImportPragma; 049 import escjava.ast.LabelExpr; 050 import escjava.ast.ModelConstructorDeclPragma; 051 import escjava.ast.ModelMethodDeclPragma; 052 import escjava.ast.ModelTypePragma; 053 import escjava.ast.Modifiers; 054 import escjava.ast.ModifiesGroupPragma; 055 import escjava.ast.NaryExpr; 056 import escjava.ast.NestedModifierPragma; 057 import escjava.ast.NothingExpr; 058 import escjava.ast.ParsedSpecs; 059 import escjava.ast.QuantifiedExpr; 060 import escjava.ast.ResExpr; 061 import escjava.ast.SimpleModifierPragma; 062 import escjava.ast.TagConstants; 063 import escjava.ast.Utils; 064 import escjava.ast.VarDeclModifierPragma; 065 import escjava.ast.VarExprModifierPragma; 066 import escjava.ast.WildRefExpr; 067 import escjava.tc.FlowInsensitiveChecks; 068 069 /** 070 * This class handles the desugaring of annotations. 071 * 072 */ 073 public class AnnotationHandler { 074 075 public AnnotationHandler() {} 076 077 protected TypeDecl td = null; 078 079 /** 080 * This must be called on a compilation unit to get the model imports listed, 081 * so that type names used in annotations can be found, and to get model 082 * methods put into the class's signature. It is called as part of 083 * EscSrcReader, a subclass of SrcReader, defined in EscTypeReader. 084 */ 085 public void handlePragmas(CompilationUnit cu) { 086 if (cu == null) return; 087 // move any model imports into the list of imports 088 for (int i = 0; i < cu.lexicalPragmas.size(); ++i) { 089 LexicalPragma p = cu.lexicalPragmas.elementAt(i); 090 if (p instanceof ImportPragma) 091 cu.imports.addElement(((ImportPragma)p).decl); 092 } 093 094 TypeDeclVec elems = cu.elems; 095 for (int i = 0; i < elems.size(); ++i) { 096 TypeDecl td = elems.elementAt(i); 097 handleTypeDecl(td); 098 } 099 } 100 101 /** 102 * After parsing, but before type checking, we need to convert model methods 103 * to regular methods, so that names are resolved correctly; also need to set 104 * ACC_PURE bits correctly in all classes so that later checks get done 105 * correctly. 106 */ 107 // FIXME - possibly should put these in GhostEnv?? 108 public void handleTypeDecl(TypeDecl td) { 109 handlePragmas(td); 110 for (int j = 0; j < td.elems.size(); ++j) { 111 TypeDeclElem tde = td.elems.elementAt(j); 112 // Handle nested types 113 if (tde instanceof TypeDecl) { 114 handleTypeDecl((TypeDecl)tde); 115 } 116 // move any model methods into the list of methods 117 if (tde instanceof ModelMethodDeclPragma) { 118 handlePragmas(tde); 119 ModelMethodDeclPragma mmp = (ModelMethodDeclPragma)tde; 120 td.elems.setElementAt(((ModelMethodDeclPragma)tde).decl, j); 121 } else if (tde instanceof ModelConstructorDeclPragma) { 122 handlePragmas(tde); 123 ModelConstructorDeclPragma mmp = (ModelConstructorDeclPragma)tde; 124 if (mmp.id == null) { 125 // An error reported already - improper name cf. EscPragmaParser 126 } else if (mmp.id.id != td.id) { 127 ErrorSet 128 .error( 129 mmp.id.getStartLoc(), 130 "A constructor-like declaration has an id which is not the same as the id of the enclosing type: " 131 + mmp.id.id + " vs. " + td.id, td.locId); 132 } else { 133 td.elems.setElementAt(((ModelConstructorDeclPragma)tde).decl, j); 134 } 135 } else if (tde instanceof ModelTypePragma) { 136 handlePragmas(tde); 137 ModelTypePragma tdp = (ModelTypePragma)tde; 138 td.elems.setElementAt(tdp.decl, j); 139 } 140 // handle PURE pragmas 141 if (tde instanceof MethodDecl || tde instanceof ConstructorDecl) { 142 handlePragmas(tde); 143 } 144 } 145 } 146 147 public void handlePragmas(TypeDeclElem tde) {} 148 149 //----------------------------------------------------------------------- 150 /* 151 * public void process(TypeDecl td) { this.td = td; 152 * 153 * for (int i=0; i <td.elems.size(); ++i) { TypeDeclElem tde = 154 * td.elems.elementAt(i); process(tde); } } 155 */ 156 157 public void process(TypeDeclElem tde) { 158 int tag = tde.getTag(); 159 switch (tag) { 160 // What about initially, monitored_by, readable_if clauses ??? FIXME 161 // What about nested classes ??? FIXME 162 // What about redundant clauses ??? FIXME 163 164 case TagConstants.CONSTRUCTORDECL: 165 case TagConstants.METHODDECL: 166 process((RoutineDecl)tde); 167 break; 168 169 case TagConstants.FIELDDECL: 170 break; 171 172 case TagConstants.GHOSTDECLPRAGMA: 173 case TagConstants.MODELDECLPRAGMA: 174 case TagConstants.INVARIANT: 175 case TagConstants.INVARIANT_REDUNDANTLY: 176 case TagConstants.CONSTRAINT: 177 Context c = new Context(); 178 c.expr = null; // ((TypeDeclElemPragma)tde).expr; 179 (new CheckPurity()).visitNode((ASTNode)tde, c); 180 break; 181 182 case TagConstants.REPRESENTS: 183 case TagConstants.AXIOM: 184 (new CheckPurity()).visitNode((ASTNode)tde, null); 185 break; 186 187 case TagConstants.DEPENDS: 188 default: 189 //System.out.println("TAG " + tag + " " + TagConstants.toString(tag) + " " 190 // + tde.getClass() ); 191 } 192 193 } 194 195 protected void process(RoutineDecl tde) { 196 ModifierPragmaVec pmodifiers = tde.pmodifiers; 197 //System.out.println(" Mods " + Modifiers.toString(tde.modifiers)); 198 if (pmodifiers != null) { 199 for (int i = 0; i < pmodifiers.size(); ++i) { 200 ModifierPragma mp = pmodifiers.elementAt(i); 201 (new CheckPurity()).visitNode((ASTNode)mp, null); 202 } 203 } 204 } 205 206 //----------------------------------------------------------------------- 207 // Desugaring is done as a last stage of type-checking. The desugar 208 // methods below may presume that all expressions are type-checked. 209 // As a result, any constructed expressions must have type information 210 // inserted. 211 212 public void desugar(TypeDecl td) { 213 int n = td.elems.size(); 214 for (int i = 0; i < n; ++i) { 215 TypeDeclElem tde = td.elems.elementAt(i); 216 if (tde instanceof RoutineDecl) desugar((RoutineDecl)tde); 217 if (tde instanceof TypeDecl) desugar((TypeDecl)tde); 218 // FIXME - what about model routines and types 219 } 220 } 221 222 public void desugar(RoutineDecl tde) { 223 if ((tde.modifiers & Modifiers.ACC_DESUGARED) != 0) return; 224 225 // Now desugar this routine itself 226 227 ModifierPragmaVec pmodifiers = tde.pmodifiers; 228 Identifier id = tde instanceof MethodDecl ? ((MethodDecl)tde).id : tde 229 .getParent().id; 230 // javafe.util.Info.out("Desugaring specifications for " + tde.parent.id + 231 // "." + id); 232 233 if (Main.options().desugaredSpecs) { 234 System.out.println("Desugaring specifications for " + tde.parent.id + "." 235 + id); 236 printSpecs(tde); 237 System.out.println("\n"); 238 } 239 240 try { // Just for safety's sake 241 tde.pmodifiers = desugarAnnotations(pmodifiers, tde); 242 } catch (Exception e) { 243 tde.pmodifiers = ModifierPragmaVec.make(); 244 ErrorSet.error(tde.getStartLoc(), 245 "Internal error while desugaring annotations: " + e); 246 e.printStackTrace(); 247 } 248 tde.modifiers |= Modifiers.ACC_DESUGARED; 249 250 if (Main.options().desugaredSpecs) { 251 System.out.println("Desugared specifications for " + tde.parent.id + "." 252 + id); 253 printSpecs(tde); 254 } 255 } 256 257 static public void printSpecs(RoutineDecl tde) { 258 if (tde.pmodifiers != null) 259 for (int i = 0; i < tde.pmodifiers.size(); ++i) { 260 ModifierPragma mp = tde.pmodifiers.elementAt(i); 261 printSpec(mp); 262 } 263 } 264 265 static public void printSpec(ModifierPragma mp) { 266 if (mp instanceof ModifiesGroupPragma) { 267 EscPrettyPrint.inst.print(System.out, 0, (ModifiesGroupPragma)mp); 268 System.out.println(""); 269 return; 270 } 271 System.out.print(" " + escjava.ast.TagConstants.toString(mp.getTag()) 272 + " "); 273 if (mp instanceof ExprModifierPragma) { 274 ExprModifierPragma mpe = (ExprModifierPragma)mp; 275 print(mpe.expr); 276 } else if (mp instanceof CondExprModifierPragma) { 277 CondExprModifierPragma mpe = (CondExprModifierPragma)mp; 278 print(mpe.expr); 279 if (mpe.cond != null) { 280 System.out.print(" if "); 281 print(mpe.cond); 282 } 283 } else if (mp instanceof VarExprModifierPragma) { 284 VarExprModifierPragma mpe = (VarExprModifierPragma)mp; 285 System.out.print("(" 286 + Types.toClassTypeSig(mpe.arg.type).getExternalName() 287 + (mpe.arg.id == TagConstants.ExsuresIdnName ? "" : " " 288 + mpe.arg.id.toString()) + ")"); 289 print(mpe.expr); 290 } else { 291 EscPrettyPrint.inst.print(System.out, 0, mp); 292 } 293 System.out.println(""); 294 } 295 296 protected ModifierPragmaVec desugarAnnotations(ModifierPragmaVec pm, 297 RoutineDecl tde) { 298 if (pm == null) { 299 pm = ModifierPragmaVec.make(); 300 } 301 302 ModifierPragmaVec newpm = ModifierPragmaVec.make(); 303 304 boolean isConstructor = tde instanceof ConstructorDecl; 305 306 // Get non_null specs 307 ModifierPragmaVec nonnullBehavior = getNonNull(tde); 308 309 javafe.util.Set overrideSet = null; 310 if (!isConstructor) 311 overrideSet = FlowInsensitiveChecks.getDirectOverrides((MethodDecl)tde); 312 313 boolean overrides = !isConstructor && !overrideSet.isEmpty(); 314 315 boolean defaultSpecs = false; 316 if (!overrides && nonnullBehavior.size() == 0) { 317 // Add a default 'requires true' clause if there are no 318 // specs at all and the routine is not overriding anything 319 boolean doit = pm.size() == 0; 320 if (!doit) { 321 // Need to determine if there are any clause specs 322 doit = true; 323 int k = pm.size(); 324 while ((--k) >= 0) { 325 ModifierPragma mpp = pm.elementAt(k); 326 if (!(mpp instanceof ParsedSpecs)) { 327 break; 328 } 329 if (((ParsedSpecs)mpp).specs.specs.size() != 0) { 330 doit = false; 331 break; 332 } 333 } 334 // FIXME - why do we get ExprModifierPragmas here (e.g. test8) 335 //System.out.println("QT " + mpp.getClass()); 336 } 337 if (doit) { 338 defaultSpecs = true; 339 ExprModifierPragma e = ExprModifierPragma.make(TagConstants.REQUIRES, 340 T, tde.getStartLoc()); 341 newpm.addElement(e); 342 newpm.addElement(defaultModifies(tde.getStartLoc(), T, tde)); 343 newpm.addElement(defaultSignalsOnly(tde, T)); 344 } 345 } 346 347 RoutineDecl previousDecl = null; 348 int pos = 0; 349 while (pos < pm.size()) { 350 ModifierPragma p = pm.elementAt(pos++); 351 if (p.getTag() == TagConstants.PARSEDSPECS) { 352 ParsedSpecs ps = (ParsedSpecs)p; 353 previousDecl = ps.decl; 354 if (overrides && ps.specs.initialAlso == null 355 && ps.specs.specs.size() != 0) { 356 ErrorSet 357 .caution( 358 ps.getStartLoc(), 359 "JML requires a specification to begin with 'also' when the method overrides other methods", 360 ((MethodDecl)overrideSet.elements().nextElement()).locType); 361 } 362 if (!overrides && ps.specs.initialAlso != null) { 363 if (!(tde.parent instanceof InterfaceDecl)) { 364 ErrorSet 365 .caution(ps.specs.initialAlso.getStartLoc(), 366 "No initial also expected since there are no overridden or refined methods"); 367 } else { 368 MethodDecl omd = Types.javaLangObject().hasMethod( 369 ((MethodDecl)tde).id, tde.argTypes()); 370 if (omd == null || Modifiers.isPrivate(omd.modifiers)) 371 ErrorSet 372 .caution(ps.specs.initialAlso.getStartLoc(), 373 "No initial also expected since there are no overridden or refined methods"); 374 } 375 } 376 break; 377 } 378 } 379 while (pos < pm.size()) { 380 ModifierPragma p = pm.elementAt(pos++); 381 if (p.getTag() == TagConstants.PARSEDSPECS) { 382 ParsedSpecs ps = (ParsedSpecs)p; 383 if (ps.specs.initialAlso == null && ps.specs.specs.size() != 0) { 384 ErrorSet 385 .caution( 386 ps.getStartLoc(), 387 "JML requires a specification to begin with 'also' when the declaration refines a previous declaration", 388 previousDecl.locId); 389 } 390 previousDecl = ps.decl; 391 } 392 } 393 394 ParsedRoutineSpecs accumulatedSpecs = new ParsedRoutineSpecs(); 395 396 pos = 0; 397 while (pos < pm.size()) { 398 ModifierPragma p = pm.elementAt(pos++); 399 if (p.getTag() == TagConstants.PARSEDSPECS) { 400 ParsedRoutineSpecs ps = ((ParsedSpecs)p).specs; 401 ParsedRoutineSpecs newps = new ParsedRoutineSpecs(); 402 deNest(ps.specs, nonnullBehavior, newps.specs); 403 deNest(ps.impliesThat, nonnullBehavior, newps.impliesThat); 404 deNest(ps.examples, nonnullBehavior, newps.examples); 405 accumulatedSpecs.specs.addAll(newps.specs); 406 accumulatedSpecs.impliesThat.addAll(newps.impliesThat); 407 accumulatedSpecs.examples.addAll(newps.examples); 408 } else { 409 newpm.addElement(p); 410 } 411 } 412 413 414 ModifierPragmaVec r = desugar(accumulatedSpecs.specs, tde); 415 // accumulatedSpecs.impliesThat = desugar(accumulatedSpecs.impliesThat); 416 // accumulatedSpecs.examples = desugar(accumulatedSpecs.examples); // FIXME 417 // - not doing this because we are not doing anything with the result. 418 newpm.append(r); 419 if (defaultSpecs && (tde instanceof ConstructorDecl) && tde.implicit) { 420 TypeSig td = TypeSig.getSig(tde.parent); 421 TypeSig tds = td.superClass(); 422 if (tds != null && tde.pmodifiers != null && tde.pmodifiers.size() > 0) 423 try { 424 ConstructorDecl cd = tds.lookupConstructor(new Type[0], td); 425 desugar(cd); 426 // Only remove previous elements after successfully finding 427 // a parent constructor 428 newpm.removeAllElements(); 429 ModifierPragmaVec mp = cd.pmodifiers; 430 for (int i = 0; i < mp.size(); ++i) { 431 ModifierPragma m = mp.elementAt(i); 432 int t = m.getTag(); 433 if (t == TagConstants.REQUIRES || t == TagConstants.PRECONDITION 434 || t == TagConstants.MODIFIESGROUPPRAGMA 435 || t == TagConstants.MODIFIES || t == TagConstants.ASSIGNABLE) { 436 newpm.addElement(m); 437 } 438 } 439 } catch (Exception e) { 440 // Purposely ignore this 441 } 442 } 443 checkSignalsOnly(newpm,tde); 444 return newpm; 445 } 446 447 public void checkSignalsOnly(ModifierPragmaVec mpv, RoutineDecl tde) { 448 Utils.exceptionDecoration.set(tde,new Integer(tde.raises.size())); 449 int throwsLoc = tde.locThrowsKeyword; 450 if (throwsLoc == Location.NULL) throwsLoc = tde.getStartLoc(); 451 for (int i=0; i<mpv.size(); i++) { 452 ModifierPragma m = mpv.elementAt(i); 453 int tag = m.originalTag(); 454 if (tag == TagConstants.SIGNALS_ONLY) { 455 TypeNameVec tv = tde.raises; 456 if (tv.size() == 0) tde.raises = tv = TypeNameVec.make(); 457 Expr e = ((VarExprModifierPragma)m).expr; 458 checkMaybeAdd(e,tv,throwsLoc); 459 } 460 } 461 } 462 463 private void checkMaybeAdd(Expr e, TypeNameVec tv, int locThrows) { 464 int tag = e.getTag(); 465 if (tag == TagConstants.OR) { 466 checkMaybeAdd( ((BinaryExpr)e).left, tv, locThrows); 467 checkMaybeAdd( ((BinaryExpr)e).right, tv, locThrows); 468 } else if (tag == TagConstants.INSTANCEOFEXPR) { 469 Type t = ((InstanceOfExpr)e).type; 470 TypeSig ts = Types.toClassTypeSig(t); 471 boolean found = false; 472 for (int i=0; i<tv.size(); ++i) { 473 TypeSig tts = TypeSig.getSig(tv.elementAt(i)); 474 if (!ts.isSubtypeOf(tts)) continue; 475 found = true; 476 break; 477 } 478 if (!found) { 479 // NOTE: The original Esc/java may have prefered that we warn about 480 // every exception in a signals_only clause that was not listed 481 // in the throws clause. Instead, we silently add types that are 482 // subtypes of RuntimeException or Error. 483 boolean b = Main.options().useThrowable; 484 if (b && !ts.isSubtypeOf(Types.javaLangRuntimeException()) && 485 !ts.isSubtypeOf(Types.javaLangError()) && 486 !Types.isSameType(ts,Types.javaLangThrowable())) { 487 ErrorSet.error(t.getStartLoc(), 488 "The signals_only clause may not contain an exception type " + 489 Types.printName(t) + 490 " that is not a subtype of either RuntimeException, Error or " + 491 "a type in the routine's throws clause", 492 locThrows); 493 } else if (!b && 494 !ts.isSubtypeOf(Types.javaLangRuntimeException()) ) { 495 ErrorSet.error(t.getStartLoc(), 496 "The signals_only clause may not contain an exception type " + 497 Types.printName(t) + 498 " that is not a subtype of either RuntimeException or " + 499 "a type in the routine's throws clause", 500 locThrows); 501 } else { 502 tv.addElement((TypeName)t); 503 } 504 } 505 } else if (tag == TagConstants.BOOLEANLIT) { 506 // skip 507 } else if (tag == TagConstants.IMPLIES) { 508 // left side is the precondition 509 checkMaybeAdd( ((BinaryExpr)e).right, tv, locThrows); 510 } else { 511 System.out.println("INTERNAL ERROR " + TagConstants.toString(tag)); 512 } 513 } 514 515 // NOTE: We are doing desugaring after typechecking, so we need to 516 // be sure to annotate any created expressions with types. 517 // (If expressions are created before typechecking they must not be 518 // annotated with types, so that typechecking happens properly). 519 520 public ModifierPragmaVec getNonNull(RoutineDecl rd) { 521 ModifierPragmaVec result = ModifierPragmaVec.make(2); 522 FormalParaDeclVec args = rd.args; 523 524 // Check that non_null on parameters is allowed 525 if (rd instanceof MethodDecl) { 526 MethodDecl md = (MethodDecl)rd; 527 // Need to check all overrides, because we may not have processed a 528 // given direct override yet, removing its spurious non_null 529 javafe.util.Set overrides = FlowInsensitiveChecks.getAllOverrides(md); 530 if (overrides != null && !overrides.isEmpty()) { 531 for (int i = 0; i < args.size(); ++i) { 532 FormalParaDecl arg = args.elementAt(i); 533 ModifierPragma m = Utils.findModifierPragma(arg, 534 TagConstants.NON_NULL); 535 if (m != null) { // overriding method has non_null for parameter i 536 MethodDecl smd = FlowInsensitiveChecks.getSuperNonNullStatus(md, i, 537 overrides); 538 if (smd != null) { // overridden method does not have non_null for i 539 FormalParaDecl sf = smd.args.elementAt(i); 540 ErrorSet 541 .caution( 542 m.getStartLoc(), 543 "The non_null annotation is ignored because this method overrides a method declaration in which this parameter is not declared non_null: ", 544 sf.getStartLoc()); 545 Utils.removeModifierPragma(arg, TagConstants.NON_NULL); 546 } 547 } 548 } 549 } 550 } 551 552 // Handle non_null on any parameter 553 for (int i = 0; i < args.size(); ++i) { 554 FormalParaDecl arg = args.elementAt(i); 555 ModifierPragma m = Utils.findModifierPragma(arg.pmodifiers, 556 TagConstants.NON_NULL); 557 if (m == null) continue; 558 int locNN = m.getStartLoc(); 559 result.addElement(ExprModifierPragma.make(TagConstants.REQUIRES, 560 NonNullExpr.make(arg, locNN), locNN)); 561 } 562 563 // Handle non_null on the result 564 // non_null is not allowed on constructors - an error should have 565 // been previously given 566 if (rd instanceof MethodDecl) { 567 ModifierPragma m = Utils.findModifierPragma(rd.pmodifiers, 568 TagConstants.NON_NULL); 569 if (m != null) { 570 int locNN = m.getStartLoc(); 571 Expr r = ResExpr.make(locNN); 572 javafe.tc.FlowInsensitiveChecks.setType(r, ((MethodDecl)rd).returnType); 573 Expr n = LiteralExpr.make(TagConstants.NULLLIT, null, locNN); 574 javafe.tc.FlowInsensitiveChecks.setType(n, Types.nullType); 575 Expr e = BinaryExpr.make(TagConstants.NE, r, n, locNN); 576 javafe.tc.FlowInsensitiveChecks.setType(e, Types.booleanType); 577 ExprModifierPragma emp = ExprModifierPragma.make(TagConstants.ENSURES, 578 e, locNN); 579 Utils.owningDecl.set(emp,rd); 580 emp.errorTag = TagConstants.CHKNONNULLRESULT; 581 result.addElement(emp); 582 } 583 } 584 return result; 585 } 586 587 // Argument is an ArrayList of ModifierPragmaVec corresponding to 588 // also-connected de-nested specification cases 589 // result is a single ModifierPragmaVec with all the requires 590 // clauses combined and all the other clauses guarded by the 591 // relevant precondition 592 public ModifierPragmaVec desugar(ArrayList ps, RoutineDecl tde) { 593 ArrayList requiresList = new ArrayList(); 594 ModifierPragmaVec resultList = ModifierPragmaVec.make(); 595 resultList.addElement(null); // replaced below 596 Iterator i = ps.iterator(); 597 while (i.hasNext()) { 598 ModifierPragmaVec m = (ModifierPragmaVec)i.next(); 599 desugar(m, requiresList, resultList, tde); 600 } 601 // combine all of the requires 602 ExprModifierPragma requires = or(requiresList); 603 resultList.setElementAt(requires, 0); 604 if (requires == null) resultList.removeElementAt(0); 605 return resultList; 606 } 607 608 // requiresList is an ArrayList of ModifierPragma 609 public void desugar(ModifierPragmaVec m, ArrayList requiresList, 610 ModifierPragmaVec resultList, RoutineDecl tde) { 611 GenericVarDeclVec foralls = GenericVarDeclVec.make(); 612 // First collect all the requires clauses together 613 int pos = 0; 614 ArrayList list = new ArrayList(); 615 boolean addTypeCheck = (!Modifiers.isStatic(tde.getModifiers()) && tde instanceof MethodDecl); 616 TypeSig ts = TypeSig.getSig(tde.parent); 617 int loc = Location.NULL; 618 619 while (pos < m.size()) { 620 ModifierPragma mp = m.elementAt(pos++); 621 // FIXME - what if some foralls happen after requires - not in scope? 622 int tag = mp.getTag(); 623 if (tag == TagConstants.NO_WACK_FORALL) 624 foralls.addElement(((VarDeclModifierPragma)mp).decl); 625 if (tag != TagConstants.REQUIRES && tag != TagConstants.PRECONDITION) 626 continue; 627 if (((ExprModifierPragma)mp).expr.getTag() == TagConstants.NOTSPECIFIEDEXPR) 628 continue; 629 loc = mp.getStartLoc(); 630 list.add(forallWrap(foralls, mp)); 631 } 632 if (addTypeCheck) { 633 Expr e = ThisExpr.make(null, Location.NULL); 634 javafe.tc.FlowInsensitiveChecks.setType(e, ts); 635 e = InstanceOfExpr.make(e, ts, Location.NULL); 636 javafe.tc.FlowInsensitiveChecks.setType(e, Types.booleanType); 637 list.add(0,(ExprModifierPragma.make(TagConstants.REQUIRES,e,loc))); 638 } 639 ExprModifierPragma conjunction = and(list); 640 boolean reqIsTrue = conjunction == null || isTrue(conjunction.expr); 641 Expr reqexpr = conjunction == null ? null : conjunction.expr; 642 Expr req = T; 643 if (reqexpr != null) { 644 ExprVec arg = ExprVec.make(new Expr[] { reqexpr }); 645 req = NaryExpr.make(Location.NULL, reqexpr.getStartLoc(), 646 TagConstants.PRE, Identifier.intern("\\old"), arg); 647 javafe.tc.FlowInsensitiveChecks.setType(req, Types.booleanType); 648 } 649 650 if (reqIsTrue && m.size() == 0) return; 651 652 requiresList.add(reqIsTrue ? ExprModifierPragma.make(TagConstants.REQUIRES, 653 T, Location.NULL) : andLabeled(list)); 654 655 // Now transform each non-requires pragma 656 boolean foundDiverges = false; 657 VarExprModifierPragma foundSignalsOnly = null; 658 ExprModifierPragma defaultDiverges = null; 659 boolean foundModifies = false; 660 boolean isLightweight = true; 661 pos = 0; 662 while (pos < m.size()) { 663 ModifierPragma mp = m.elementAt(pos++); 664 int tag = mp.getTag(); 665 if (tag == TagConstants.REQUIRES || tag == TagConstants.PRECONDITION) 666 continue; 667 switch (tag) { 668 case TagConstants.DIVERGES: 669 foundDiverges = true; 670 // fall-through 671 case TagConstants.ENSURES: 672 case TagConstants.POSTCONDITION: 673 case TagConstants.WHEN: { 674 ExprModifierPragma mm = (ExprModifierPragma)mp; 675 if (mm.expr.getTag() == TagConstants.NOTSPECIFIEDEXPR) break; 676 if (mm.expr.getTag() == TagConstants.INFORMALPRED_TOKEN) break; 677 if (isTrue(mm.expr)) break; 678 if (!reqIsTrue) mm.expr = implies(req, mm.expr); 679 resultList.addElement(mm); 680 break; 681 } 682 683 case TagConstants.SIGNALS: { 684 if (mp.originalTag() == TagConstants.SIGNALS_ONLY) { 685 if (foundSignalsOnly != null) { 686 ErrorSet.error(mp.getStartLoc(), 687 "Only one signals_only clause is allowed per specification case", 688 foundSignalsOnly.getStartLoc()); 689 } else { 690 foundSignalsOnly = (VarExprModifierPragma)mp; 691 } 692 } 693 VarExprModifierPragma mm = (VarExprModifierPragma)mp; 694 if (mm.expr.getTag() == TagConstants.NOTSPECIFIEDEXPR) break; 695 if (mm.expr.getTag() == TagConstants.INFORMALPRED_TOKEN) break; 696 if (isTrue(mm.expr)) break; 697 if (!reqIsTrue) mm.expr = implies(req, mm.expr); 698 resultList.addElement(mm); 699 break; 700 } 701 case TagConstants.MODIFIESGROUPPRAGMA: { 702 foundModifies = true; 703 ModifiesGroupPragma mm = (ModifiesGroupPragma)mp; 704 mm.precondition = req; 705 resultList.addElement(mm); 706 break; 707 } 708 /* 709 * case TagConstants.MODIFIES: case TagConstants.MODIFIABLE: case 710 * TagConstants.ASSIGNABLE: { CondExprModifierPragma mm = 711 * (CondExprModifierPragma)mp; if (mm.expr != null && mm.expr.getTag() == 712 * TagConstants.NOTSPECIFIEDEXPR) break; foundModifies = true; mm.cond = 713 * and(mm.cond,req); resultList.addElement(mm); break; } 714 */ 715 716 case TagConstants.WORKING_SPACE: 717 case TagConstants.DURATION: { 718 CondExprModifierPragma mm = (CondExprModifierPragma)mp; 719 if (mm.expr != null 720 && mm.expr.getTag() == TagConstants.NOTSPECIFIEDEXPR) break; 721 mm.cond = and(mm.cond, req); 722 resultList.addElement(mm); 723 break; 724 } 725 726 case TagConstants.ACCESSIBLE: 727 case TagConstants.CALLABLE: 728 case TagConstants.MEASURED_BY: 729 case TagConstants.MODEL_PROGRAM: 730 case TagConstants.CODE_CONTRACT: 731 // Remember to skip if not specified 732 // FIXME - not yet handled 733 foundModifies = true; // Don't add a default modifies 734 foundDiverges = true; 735 break; 736 737 case TagConstants.NO_WACK_FORALL: 738 case TagConstants.OLD: 739 // These are handled elsewhere and don't get put into 740 // the pragma list. 741 break; 742 743 case TagConstants.MONITORED_BY: 744 ErrorSet.error(mp.getStartLoc(), 745 "monitored_by is obsolete and only applies to fields"); 746 break; 747 748 case TagConstants.MONITORED: 749 ErrorSet.error(mp.getStartLoc(), "monitored only applies to fields"); 750 break; 751 752 case TagConstants.BEHAVIOR: 753 // Used to distinguish lightweight and heavyweight sequences 754 isLightweight = false; 755 break; 756 757 default: 758 ErrorSet.error(mp.getStartLoc(), 759 "Unknown kind of pragma for a routine declaration: " 760 + TagConstants.toString(tag)); 761 break; 762 } 763 } 764 if (foundSignalsOnly == null) { 765 Expr defaultExpr = AnnotationHandler.F; 766 // Create a default signals_only clause using the list of exceptions 767 // prior to any adjustment 768 foundSignalsOnly = defaultSignalsOnly(tde,req); 769 resultList.addElement(foundSignalsOnly); 770 m.insertElementAt(foundSignalsOnly,0); 771 } 772 if (!foundDiverges) { 773 // The default diverges clause is 'false' 774 resultList.addElement(ExprModifierPragma.make(TagConstants.DIVERGES, 775 implies(req, AnnotationHandler.F), Location.NULL)); 776 } 777 778 if (!foundModifies) { 779 resultList.addElement(defaultModifies(tde.getStartLoc(), req, tde)); 780 } 781 Expr sexpr = foundSignalsOnly.expr; 782 pos = 0; 783 while (pos < m.size()) { 784 ModifierPragma mp = m.elementAt(pos++); 785 int tag = mp.getTag(); 786 if (tag != TagConstants.SIGNALS) continue; 787 if (mp.originalTag() == TagConstants.SIGNALS_ONLY) continue; 788 VarExprModifierPragma vmp = (VarExprModifierPragma)mp; 789 if (isFalse(vmp.expr)) continue; 790 if ((vmp.expr instanceof BinaryExpr) && ((BinaryExpr)vmp.expr).op == TagConstants.IMPLIES && isFalse(((BinaryExpr)vmp.expr).right)) continue; 791 Type t = vmp.arg.type; 792 if (!isInSignalsOnlyExpr(t,sexpr,true)) { 793 if (Types.isCastable(t,Types.javaLangThrowable()) && 794 !Types.isCastable(t,Types.javaLangException())) {} 795 else 796 ErrorSet.error(t.getStartLoc(), 797 "Exception type in signals clause must be listed in either a " + 798 "corresponding signals_only clause or the method's throws list", 799 foundSignalsOnly.getStartLoc()); 800 } 801 } 802 } 803 804 private boolean isInSignalsOnlyExpr(Type t, Expr e, boolean allowSuperTypes) { 805 if (e == null) return false; 806 if (e instanceof BinaryExpr) { 807 BinaryExpr be = (BinaryExpr)e; 808 if (be.op == TagConstants.IMPLIES) return isInSignalsOnlyExpr(t,be.right,allowSuperTypes); 809 return isInSignalsOnlyExpr(t,be.left,allowSuperTypes) || 810 isInSignalsOnlyExpr(t,be.right,allowSuperTypes); 811 } else if (e instanceof NaryExpr) { 812 NaryExpr ne = (NaryExpr)e; 813 for (int i=0; i<ne.exprs.size(); ++i) { 814 Expr ee = ne.exprs.elementAt(i); 815 if (isInSignalsOnlyExpr(t,ee,allowSuperTypes)) return true; 816 } 817 return false; 818 } else if (e instanceof LiteralExpr) { 819 return false; 820 } else if (e instanceof InstanceOfExpr) { 821 InstanceOfExpr ie = (InstanceOfExpr)e; 822 if (allowSuperTypes) { 823 if (Types.isCastable(ie.type,t)) return true; 824 } 825 if ( Types.isCastable(t,ie.type) ) return true; 826 return false; 827 } else { 828 System.out.println("UNHANDLED TYPE-A " + e.getClass()); 829 return false; 830 } 831 } 832 833 public final static VarExprModifierPragma defaultSignalsOnly( 834 RoutineDecl tde, Expr req) { 835 int throwsLoc = tde.locThrowsKeyword; 836 if (throwsLoc == Location.NULL) throwsLoc = tde.getStartLoc(); 837 Expr defaultExpr = AnnotationHandler.F; 838 TypeNameVec tv = tde.raises; 839 Identifier id = TagConstants.ExsuresIdnName; 840 FormalParaDecl arg = FormalParaDecl.make(0, null, id, 841 Main.options().useThrowable ? 842 Types.javaLangThrowable() : Types.javaLangException(), 843 throwsLoc); 844 for (int i=0; i<tv.size(); ++i) { 845 TypeName tn =tv.elementAt(i); 846 int loc = tn.getStartLoc(); 847 Expr e = InstanceOfExpr.make( 848 VariableAccess.make(id, loc, arg), tn, loc); 849 FlowInsensitiveChecks.setType(e, Types.booleanType); 850 defaultExpr = BinaryExpr.make(TagConstants.OR, 851 defaultExpr, e, loc); 852 FlowInsensitiveChecks.setType(defaultExpr, Types.booleanType); 853 } 854 VarExprModifierPragma newmp = VarExprModifierPragma.make( 855 TagConstants.SIGNALS, arg, defaultExpr, throwsLoc); 856 newmp.setOriginalTag(TagConstants.SIGNALS_ONLY); 857 newmp.expr = implies(req, newmp.expr); 858 return newmp; 859 } 860 861 public final static ModifiesGroupPragma defaultModifies(int loc, Expr req, 862 RoutineDecl rd) { 863 boolean everythingIsDefault = true; 864 boolean nothing = !everythingIsDefault; 865 boolean isPure = Utils.isPure(rd); 866 867 if (isPure) nothing = true; 868 Expr e; 869 if (isPure && rd instanceof ConstructorDecl) { 870 ExprObjectDesignator eod = ExprObjectDesignator.make(loc, ThisExpr.make( 871 null, loc)); 872 FlowInsensitiveChecks.setType(eod.expr, TypeSig.getSig(rd.parent)); 873 e = WildRefExpr.make(null, eod); 874 } else if (nothing) { 875 e = NothingExpr.make(loc); 876 } else { 877 e = EverythingExpr.make(loc); 878 } 879 880 // FIXME - need default for COnstructor, ModelConstructor 881 ModifiesGroupPragma r = ModifiesGroupPragma 882 .make(TagConstants.MODIFIES, loc); 883 r.addElement(CondExprModifierPragma.make(TagConstants.MODIFIES, e, loc, 884 null)); 885 r.precondition = req; 886 return r; 887 } 888 889 public ModifierPragma forallWrap(GenericVarDeclVec foralls, ModifierPragma mp) { 890 if (mp instanceof ExprModifierPragma) { 891 ExprModifierPragma emp = (ExprModifierPragma)mp; 892 emp.expr = forallWrap(foralls, emp.expr); 893 FlowInsensitiveChecks.setType(emp.expr, Types.booleanType); 894 } 895 return mp; 896 } 897 898 public Expr forallWrap(GenericVarDeclVec foralls, Expr e) { 899 if (foralls.size() == 0) return e; 900 int loc = foralls.elementAt(0).getStartLoc(); 901 int endLoc = foralls.elementAt(foralls.size() - 1).getStartLoc(); 902 return QuantifiedExpr.make(loc, endLoc, TagConstants.FORALL, foralls, null, 903 e, null, null); 904 } 905 906 public void deNest(ArrayList ps, ModifierPragmaVec prefix, 907 ArrayList deNestedSpecs) { 908 if (ps.size() == 0 && prefix.size() != 0) { 909 combineModifies(prefix); 910 fixDefaultSpecs(prefix); 911 deNestedSpecs.add(prefix); 912 } else { 913 Iterator i = ps.iterator(); 914 while (i.hasNext()) { 915 ModifierPragmaVec m = (ModifierPragmaVec)i.next(); 916 deNest(m, prefix, deNestedSpecs); 917 } 918 } 919 } 920 921 public void combineModifies(ModifierPragmaVec list) { 922 ModifiesGroupPragma m = null; 923 for (int i = 0; i < list.size(); ++i) { 924 ModifierPragma mp = list.elementAt(i); 925 if (mp.getTag() == TagConstants.MODIFIESGROUPPRAGMA) { 926 ModifiesGroupPragma mm = (ModifiesGroupPragma)mp; 927 if (m == null) 928 m = mm; 929 else { 930 m.append(mm); 931 list.removeElementAt(i); 932 --i; 933 } 934 } 935 } 936 } 937 938 //@ requires (* m.size() > 0 *); 939 // Uses the fact that if there is a nesting it is the last element of 940 // the ModifierPragmaVec 941 public void deNest(ModifierPragmaVec m, ModifierPragmaVec prefix, 942 ArrayList deNestedSpecs) { 943 ModifierPragma last = m.elementAt(m.size() - 1); 944 if (last instanceof NestedModifierPragma) { 945 m.removeElementAt(m.size() - 1); 946 ModifierPragmaVec newprefix = prefix.copy(); 947 newprefix.append(m); 948 m.addElement(last); 949 ArrayList list = ((NestedModifierPragma)last).list; 950 deNest(list, newprefix, deNestedSpecs); 951 } else { 952 ModifierPragmaVec mm = prefix.copy(); 953 mm.append(m); 954 combineModifies(mm); 955 fixDefaultSpecs(mm); 956 deNestedSpecs.add(mm); 957 } 958 } 959 960 public void fixDefaultSpecs(ModifierPragmaVec prefix) { 961 // This step is necessary because a singleton instance of a default 962 // Pragma can be used. Since we are going to change the expression. 963 for (int i = 0; i < prefix.size(); ++i) { 964 ModifierPragma mp = prefix.elementAt(i); 965 if (mp.getTag() == TagConstants.SIGNALS) { 966 VarExprModifierPragma vmp = (VarExprModifierPragma)mp; 967 if (isFalse(vmp.expr)) { 968 VarExprModifierPragma newvmp = VarExprModifierPragma.make(vmp.tag, 969 vmp.arg, vmp.expr, vmp.loc); 970 newvmp.setOriginalTag(vmp.originalTag()); 971 prefix.setElementAt(newvmp, i); 972 } 973 } 974 if (mp.getTag() == TagConstants.ENSURES) { 975 ExprModifierPragma vmp = (ExprModifierPragma)mp; 976 if (isFalse(vmp.expr)) { 977 ExprModifierPragma newvmp = ExprModifierPragma.make(vmp.tag, 978 vmp.expr, vmp.loc); 979 newvmp.setOriginalTag(vmp.originalTag()); 980 if (Utils.ensuresDecoration.isTrue(vmp)) 981 Utils.ensuresDecoration.set(newvmp,true); 982 prefix.setElementAt(newvmp, i); 983 } 984 } 985 // FIXME - perhaps diverges, modifies 986 } 987 } 988 989 /** 990 * Produces an expression which is the conjunction of the two expressions. If 991 * either input is null, the other is returned. If either input is literally 992 * true or false, the appropriate constant folding is performed. 993 */ 994 static public Expr and(Expr e1, Expr e2) { 995 if (e1 == null || isTrue(e1)) return e2; 996 if (e2 == null || isTrue(e2)) return e1; 997 if (isFalse(e1)) return e1; 998 if (isFalse(e2)) return e2; 999 Expr e = BinaryExpr.make(TagConstants.AND, e1, e2, e1.getStartLoc()); 1000 javafe.tc.FlowInsensitiveChecks.setType(e, Types.booleanType); 1001 return e; 1002 } 1003 1004 /** 1005 * Produces an ExprModifierPragma whose expression is the conjunction of the 1006 * expressions in the input pragmas. If either input is null, the other is 1007 * returned. If either input is literally true or false, the appropriate 1008 * constant folding is performed. 1009 */ 1010 static public ExprModifierPragma and(ExprModifierPragma e1, 1011 ExprModifierPragma e2) { 1012 if (e1 == null || isTrue(e1.expr)) return e2; 1013 if (e2 == null || isTrue(e2.expr)) return e1; 1014 if (isFalse(e1.expr)) return e1; 1015 if (isFalse(e2.expr)) return e2; 1016 Expr e = BinaryExpr.make(TagConstants.AND, e1.expr, e2.expr, e1 1017 .getStartLoc()); 1018 javafe.tc.FlowInsensitiveChecks.setType(e, Types.booleanType); 1019 return ExprModifierPragma.make(e1.getTag(), e, e1.getStartLoc()); 1020 } 1021 1022 /** 1023 * Produces an ExprModifierPragma whose expression is the conjunction of all 1024 * of the expressions in the ExprModifierPragmas in the argument. If the 1025 * argument is empty, null is returned. Otherwise, some object is returned, 1026 * though its expression might be a literal. 1027 */ 1028 static public ExprModifierPragma and(/* @ non_null */ArrayList a) { 1029 if (a.size() == 0) { 1030 return null; 1031 } else if (a.size() == 1) { 1032 return (ExprModifierPragma)a.get(0); 1033 } else { 1034 ExprModifierPragma e = null; 1035 Iterator i = a.iterator(); 1036 while (i.hasNext()) { 1037 e = and(e, (ExprModifierPragma)i.next()); 1038 } 1039 return e; 1040 } 1041 } 1042 1043 /** 1044 * The same as and(ArrayList), but produces labelled expressions within the 1045 * conjunction so that error messages come out with useful locations. 1046 */ 1047 static public ExprModifierPragma andLabeled(/* @ non_null */ArrayList a) { 1048 if (a.size() == 0) { 1049 return null; 1050 } else { 1051 Expr e = null; 1052 int floc = Location.NULL; 1053 Iterator i = a.iterator(); 1054 while (i.hasNext()) { 1055 ExprModifierPragma emp = (ExprModifierPragma)i.next(); 1056 int loc = emp.getStartLoc(); 1057 if (floc == Location.NULL) floc = loc; 1058 boolean nn = emp.expr instanceof NonNullExpr; 1059 Expr le = LabelExpr.make(emp.getStartLoc(), emp.getEndLoc(), false, 1060 escjava.translate.GC.makeFullLabel(nn ? "NonNull" : "Pre", loc, 1061 Location.NULL), // FIXME - does this get translated to include 1062 // an @ location ? 1063 emp.expr); 1064 javafe.tc.FlowInsensitiveChecks.setType(le, Types.booleanType); 1065 if (!isTrue(emp.expr)) 1066 e = and(e, le); 1067 else if (e == null) e = le; 1068 javafe.tc.FlowInsensitiveChecks.setType(e, Types.booleanType); 1069 } 1070 return ExprModifierPragma.make(TagConstants.REQUIRES, e, floc); 1071 } 1072 } 1073 1074 /* 1075 * static public Expr or(Expr e1, Expr e2) { if (e1 == null || isFalse(e1)) 1076 * return e2; if (e2 == null || isFalse(e2)) return e1; if (isTrue(e1)) return 1077 * e1; if (isTrue(e2)) return e2; Expr e = 1078 * BinaryExpr.make(TagConstants.OR,e1,e2,e1.getStartLoc()); 1079 * javafe.tc.FlowInsensitiveChecks.setType(e,Types.booleanType); return e; } 1080 */ 1081 /** 1082 * Produces an ExprModifierPragma whose expression is the disjunction of the 1083 * expressions in the input pragmas. If either input is null, the other is 1084 * returned. If either input is literally true or false, the appropriate 1085 * constant folding is performed. 1086 */ 1087 static public ExprModifierPragma or(ExprModifierPragma e1, 1088 ExprModifierPragma e2) { 1089 if (e1 == null || isFalse(e1.expr)) return e2; 1090 if (e2 == null || isFalse(e2.expr)) return e1; 1091 if (isTrue(e1.expr)) return e1; 1092 if (isTrue(e2.expr)) return e2; 1093 Expr e = BinaryExpr.make(TagConstants.OR, e1.expr, e2.expr, e1 1094 .getStartLoc()); 1095 javafe.tc.FlowInsensitiveChecks.setType(e, Types.booleanType); 1096 return ExprModifierPragma.make(e1.getTag(), e, e1.getStartLoc()); 1097 } 1098 1099 /** 1100 * Produces an ExprModifierPragma whose expression is the disjunction of all 1101 * of the expressions in the ExprModifierPragmas in the argument. If the 1102 * argument is empty, null is returned. Otherwise, some object is returned, 1103 * though its expression might be a literal. 1104 */ 1105 static public ExprModifierPragma or(/* @ non_null */ArrayList a) { 1106 if (a.size() == 0) { 1107 return null; 1108 } else if (a.size() == 1) { 1109 return (ExprModifierPragma)a.get(0); 1110 } else { 1111 ExprModifierPragma e = null; 1112 Iterator i = a.iterator(); 1113 while (i.hasNext()) { 1114 e = or(e, (ExprModifierPragma)i.next()); 1115 } 1116 return e; 1117 } 1118 } 1119 1120 /** 1121 * Produces an expression which is the implication of the two expressions. 1122 * Neither input may be null. If either input is literally true or false, the 1123 * appropriate constant folding is performed. 1124 */ 1125 static public Expr implies(/* @ non_null */Expr e1, /* @ non_null */Expr e2) { 1126 if (isTrue(e1)) return e2; 1127 if (isTrue(e2)) return e2; // Use e2 instead of T to keep location info 1128 if (isFalse(e1)) return T; 1129 Expr e = BinaryExpr.make(TagConstants.IMPLIES, e1, e2, e2.getStartLoc()); 1130 javafe.tc.FlowInsensitiveChecks.setType(e, Types.booleanType); 1131 return e; 1132 } 1133 1134 /** 1135 * Returns true if the argument is literally true, and returns false if it is 1136 * not a literal or is literally false. 1137 */ 1138 static boolean isTrue(/* @ non_null */Expr e) { 1139 return e == T 1140 || (e instanceof LiteralExpr && ((LiteralExpr)e).value.equals(T.value)); 1141 } 1142 1143 /** 1144 * Returns true if the argument is literally false, and returns false if it is 1145 * not a literal or is literally true. 1146 */ 1147 static boolean isFalse(/* @ non_null */Expr e) { 1148 return e == F 1149 || (e instanceof LiteralExpr && ((LiteralExpr)e).value.equals(F.value)); 1150 } 1151 1152 public final static LiteralExpr T = (LiteralExpr)FlowInsensitiveChecks 1153 .setType(LiteralExpr.make(TagConstants.BOOLEANLIT, Boolean.TRUE, 1154 Location.NULL), Types.booleanType); 1155 1156 public final static LiteralExpr F = (LiteralExpr)FlowInsensitiveChecks 1157 .setType(LiteralExpr.make(TagConstants.BOOLEANLIT, Boolean.FALSE, 1158 Location.NULL), Types.booleanType); 1159 1160 static public class Context { 1161 public Expr expr; 1162 1163 } 1164 1165 static public class CheckPurity { 1166 1167 public void visitNode(ASTNode x, Context cc) { 1168 if (x == null) return; 1169 //System.out.println("CP TAG " + TagConstants.toString(x.getTag())); 1170 switch (x.getTag()) { 1171 case TagConstants.METHODINVOCATION: 1172 MethodInvocation m = (MethodInvocation)x; 1173 if (Main.options().checkPurity && !Utils.isPure(m.decl)) { 1174 ErrorSet.error(m.locId, "Method " + m.id 1175 + " may not be used in an annotation since it is not pure", 1176 m.decl.loc); 1177 if (Main.options().checkPurity && Utils.isAllocates(m.decl)) { 1178 ErrorSet.error(m.locId, "Method " + m.id 1179 + " may not be used in an annotation since it allocates" 1180 + " fresh storage"); 1181 } 1182 } 1183 break; 1184 case TagConstants.NEWINSTANCEEXPR: 1185 NewInstanceExpr c = (NewInstanceExpr)x; 1186 // @review kiniry, chalin 21 Aug 2005 - If/when we revise assertion semantics, 1187 // this will need to be updated appropriately. 1188 if (Main.options().checkPurity && !Utils.isPure(c.decl)) { 1189 ErrorSet.error(c.loc, "Constructor is used in an annotation" 1190 + " but is not pure (" + Location.toFileLineString(c.decl.loc) 1191 + ")"); 1192 } 1193 break; 1194 case TagConstants.WACK_DURATION: 1195 case TagConstants.WACK_WORKING_SPACE: 1196 case TagConstants.SPACE: 1197 // The argument of these built-in functions is not 1198 // evaluated, so it need not be pure. 1199 return; 1200 1201 case TagConstants.ENSURES: 1202 case TagConstants.POSTCONDITION: 1203 case TagConstants.REQUIRES: 1204 case TagConstants.PRECONDITION: { 1205 // @bug kiniry 21 Aug 2005 - Won't this crash with a SOO if any of these spec 1206 // expressions are recursive? 1207 Context cn = new Context(); 1208 cn.expr = ((ExprModifierPragma)x).expr; 1209 visitNode(cn.expr, cn); 1210 ((ExprModifierPragma)x).expr = cn.expr; 1211 return; 1212 } 1213 1214 case TagConstants.SIGNALS: 1215 case TagConstants.EXSURES: 1216 // @review kiniry 21 Aug 2005 - Why are we not checking subexpressions of these 1217 // spec expressions? 1218 break; 1219 } 1220 { 1221 int n = x.childCount(); 1222 for (int i = 0; i < n; ++i) { 1223 if (x.childAt(i) instanceof ASTNode) 1224 visitNode((ASTNode)x.childAt(i), cc); 1225 } 1226 } 1227 } 1228 1229 } 1230 1231 static private void print(Expr e) { 1232 if (e != null) PrettyPrint.inst.print(System.out, 0, e); 1233 } 1234 1235 static public class NonNullExpr extends BinaryExpr { 1236 1237 static NonNullExpr make(FormalParaDecl arg, int locNN) { 1238 NonNullExpr e = new NonNullExpr(); 1239 int loc = arg.getStartLoc(); 1240 Expr v = VariableAccess.make(arg.id, loc, arg); 1241 javafe.tc.FlowInsensitiveChecks.setType(v, arg.type); 1242 Expr n = LiteralExpr.make(TagConstants.NULLLIT, null, locNN); 1243 javafe.tc.FlowInsensitiveChecks.setType(n, Types.nullType); 1244 e.op = TagConstants.NE; 1245 e.left = v; 1246 e.right = n; 1247 e.locOp = locNN; 1248 javafe.tc.FlowInsensitiveChecks.setType(e, Types.booleanType); 1249 return e; 1250 } 1251 } 1252 1253 //---------------------------------------------------------------------- 1254 // Parsing the sequence of ModifierPragmas for each method of a 1255 // compilation unit happens as a part of the original parsing and 1256 // refinement processing. 1257 1258 static NestedPragmaParser specparser = new NestedPragmaParser(); 1259 1260 public void parseAllRoutineSpecs(CompilationUnit ccu) { 1261 specparser.parseAllRoutineSpecs(ccu); 1262 } 1263 1264 /** 1265 * The routines in this class parse a sequence of ModifierPragma that occur 1266 * prior to a method or constructor declaration. These consist of lightweight 1267 * or heavyweight specifications, possibly nested or with consecutive 1268 * spec-cases separated by 'also'. The parsing of the compilation unit simply 1269 * produces a flat sequence of such ModifierPragmas, since they may occur in 1270 * separate annotation comments and the Javafe parser does not provide 1271 * mechanisms to associate them together. However, we do need to determine the 1272 * nesting structure of the sequence of pragmas because the forall and old 1273 * pragmas introduce new variable declarations that may be used in subsequent 1274 * pragmas. This parsing into the nested structure (and checking of it) needs 1275 * to be completed prior to type checking so that the variable references are 1276 * properly determined. The ultimate desugaring then happens after 1277 * typechecking. 1278 * 1279 * The resulting pmodifiers vector for each routine consists of a 1280 * possibly-empty sequence of simple routine modifiers (e.g. pure, non_null) 1281 * terminated with a single ParsedSpecs element. 1282 */ 1283 1284 static public class NestedPragmaParser { 1285 1286 /** 1287 * Parses the sequence of pragma modifiers for each routine in the 1288 * CompilationUnit, replacing the existing sequence with the parsed one in 1289 * each case. 1290 */ 1291 public void parseAllRoutineSpecs(CompilationUnit ccu) { 1292 TypeDeclVec v = ccu.elems; 1293 for (int i = 0; i < v.size(); ++i) { 1294 parseAllRoutineSpecs(v.elementAt(i)); 1295 } 1296 } 1297 1298 public void parseAllRoutineSpecs(TypeDecl td) { 1299 TypeDeclElemVec v = td.elems; 1300 for (int i = 0; i < v.size(); ++i) { 1301 TypeDeclElem tde = v.elementAt(i); 1302 if (tde instanceof RoutineDecl) { 1303 parseRoutineSpecs((RoutineDecl)tde); 1304 } else if (tde instanceof ModelMethodDeclPragma) { 1305 parseRoutineSpecs(((ModelMethodDeclPragma)tde).decl); 1306 } else if (tde instanceof ModelConstructorDeclPragma) { 1307 parseRoutineSpecs(((ModelConstructorDeclPragma)tde).decl); 1308 } else if (tde instanceof TypeDecl) { 1309 parseAllRoutineSpecs((TypeDecl)tde); 1310 } 1311 } 1312 } 1313 1314 public void parseRoutineSpecs(RoutineDecl rd) { 1315 ModifierPragmaVec pm = rd.pmodifiers; 1316 if (pm == null || pm.size() == 0) { 1317 ParsedRoutineSpecs pms = new ParsedRoutineSpecs(); 1318 pms.modifiers.addElement(ParsedSpecs.make(rd, pms)); 1319 rd.pmodifiers = pms.modifiers; 1320 return; 1321 } 1322 if (pm.elementAt(pm.size() - 1) instanceof ParsedSpecs) { 1323 // It is a bit of a design problem that the parsing of the 1324 // sequence of pragmas produces a new ModifierPragmaVec that 1325 // overwrites the old one. That means that if we call 1326 // parseRoutineSpecs twice on a routine we get problems. 1327 // This test is here to avoid problems if a bug elsewhere 1328 // causes this to happen. 1329 System.out.println("OUCH - attempt to reparse " 1330 + Location.toString(rd.getStartLoc())); 1331 javafe.util.ErrorSet.dump("OUCH"); 1332 return; 1333 } 1334 1335 // We add this (internal use only) END pragma so that we don't have 1336 // to continually check the value of pos vs. the size of the array 1337 pm.addElement(SimpleModifierPragma.make(TagConstants.END, 1338 pm.size() == 0 ? Location.NULL : pm.elementAt(pm.size() - 1) 1339 .getStartLoc())); 1340 1341 ParsedRoutineSpecs pms = new ParsedRoutineSpecs(); 1342 int pos = 0; 1343 if (pm.elementAt(0).getTag() == TagConstants.ALSO) { 1344 pms.initialAlso = pm.elementAt(0); 1345 ++pos; 1346 } 1347 pos = parseAlsoSeq(pos, pm, 1, null, pms.specs); 1348 if (pm.elementAt(pos).getTag() == TagConstants.IMPLIES_THAT) { 1349 ++pos; 1350 pos = parseAlsoSeq(pos, pm, 1, null, pms.impliesThat); 1351 } 1352 if (pm.elementAt(pos).getTag() == TagConstants.FOR_EXAMPLE) { 1353 ++pos; 1354 pos = parseAlsoSeq(pos, pm, 2, null, pms.examples); 1355 } 1356 if (pm.elementAt(pos).getTag() == TagConstants.IMPLIES_THAT) { 1357 ErrorSet 1358 .caution(pm.elementAt(pos).getStartLoc(), 1359 "implies_that sections are expected to precede for_example sections"); 1360 ++pos; 1361 pos = parseAlsoSeq(pos, pm, 1, null, pms.impliesThat); 1362 } 1363 while (true) { 1364 ModifierPragma mp = pm.elementAt(pos); 1365 int tag = mp.getTag(); 1366 if (tag == TagConstants.END) break; 1367 // Turned off because of problems with annotations after the declaration 1368 // - FIXME 1369 if (false && !isRoutineModifier(tag)) { 1370 int loc = Location.NULL; 1371 if (pms.modifiers.size() > 0) 1372 loc = pms.modifiers.elementAt(0).getStartLoc(); 1373 ErrorSet 1374 .error( 1375 mp.getStartLoc(), 1376 "Unexpected or out of order pragma (expected a simple routine modifier)", 1377 loc); 1378 } else { 1379 pms.modifiers.addElement(mp); 1380 } 1381 ++pos; 1382 } 1383 pms.modifiers.addElement(ParsedSpecs.make(rd, pms)); 1384 rd.pmodifiers = pms.modifiers; 1385 } 1386 1387 static public boolean isRoutineModifier(int tag) { 1388 return tag == TagConstants.PURE || tag == TagConstants.SPEC_PUBLIC 1389 || tag == TagConstants.SPEC_PROTECTED || tag == TagConstants.HELPER 1390 || tag == TagConstants.GHOST || // Actually should not occur 1391 tag == TagConstants.MODEL || tag == TagConstants.MONITORED 1392 || tag == TagConstants.FUNCTION || tag == TagConstants.NON_NULL; 1393 } 1394 1395 static public boolean isEndingModifier(int tag) { 1396 return tag == TagConstants.END || tag == TagConstants.ALSO 1397 || tag == TagConstants.IMPLIES_THAT 1398 || tag == TagConstants.FOR_EXAMPLE; 1399 } 1400 1401 // behaviorMode == 0 : nested call 1402 // behaviorMode == 1 : outer call - non-example mode, model programs allowed 1403 // behaviorMode == 2 : outer call - example mode 1404 // The behaviorMode is used to determine which behavior/example keywords 1405 // are valid - but this is only needed on the outermost nesting level. 1406 // The behaviorTag is used to determine whether signals or ensures clauses 1407 // are permitted; 0 means either are ok; not valid on outermost call 1408 public int parseAlsoSeq(int pos, ModifierPragmaVec pm, int behaviorMode, 1409 ModifierPragma behavior, ArrayList result) { 1410 while (true) { 1411 ModifierPragmaVec mpv = ModifierPragmaVec.make(); 1412 if (behaviorMode != 0) { 1413 ModifierPragma mp = pm.elementAt(pos); 1414 behavior = mp; 1415 int behaviorTag = mp.getTag(); 1416 ++pos; 1417 encounteredError = false; 1418 switch (behaviorTag) { 1419 case TagConstants.MODEL_PROGRAM: 1420 if (behaviorMode == 2) { 1421 ErrorSet.error(mp.getStartLoc(), 1422 "Model programs may not be in the examples section"); 1423 encounteredError = true; 1424 } else if (!isEndingModifier(pm.elementAt(pos).getTag()) 1425 && !isRoutineModifier(pm.elementAt(pos).getTag())) { 1426 ErrorSet.error(mp.getStartLoc(), 1427 "A model_program may not be combined with other clauses"); 1428 } else { 1429 mpv.addElement(mp); 1430 result.add(mpv); 1431 break; 1432 } 1433 continue; 1434 case TagConstants.CODE_CONTRACT: 1435 if (behaviorMode == 2) { 1436 ErrorSet.error(mp.getStartLoc(), 1437 "code_contract sections may not be in an examples section"); 1438 encounteredError = true; 1439 } else { 1440 // FIXME - code_contract sections are ignored for now 1441 ModifierPragmaVec r = ModifierPragmaVec.make(); 1442 pos = parseCCSeq(pos, pm, r); 1443 mpv.addElement(mp); 1444 result.add(mpv); 1445 break; 1446 } 1447 continue; 1448 1449 case TagConstants.BEHAVIOR: 1450 if (behaviorMode == 2) 1451 ErrorSet 1452 .error(mp.getStartLoc(), 1453 "Behavior keywords may not be in the for_example section"); 1454 break; 1455 case TagConstants.NORMAL_BEHAVIOR: 1456 if (behaviorMode == 2) 1457 ErrorSet 1458 .error(mp.getStartLoc(), 1459 "Behavior keywords may not be in the for_example section"); 1460 mpv.addElement(VarExprModifierPragma.make(TagConstants.SIGNALS, 1461 FormalParaDecl.make(0, null, TagConstants.ExsuresIdnName, 1462 Types.javaLangException(), mp.getStartLoc()), 1463 AnnotationHandler.F, mp.getStartLoc()). 1464 setOriginalTag(TagConstants.SIGNALS_ONLY)); 1465 break; 1466 case TagConstants.EXCEPTIONAL_BEHAVIOR: 1467 if (behaviorMode == 2) 1468 ErrorSet 1469 .error(mp.getStartLoc(), 1470 "Behavior keywords may not be in the for_example section"); 1471 ExprModifierPragma emp = ExprModifierPragma.make( 1472 TagConstants.ENSURES, AnnotationHandler.F, mp.getStartLoc()); 1473 Utils.ensuresDecoration.set(emp, true); 1474 mpv.addElement(emp); 1475 break; 1476 case TagConstants.EXAMPLE: 1477 if (behaviorMode == 1) 1478 ErrorSet 1479 .error(mp.getStartLoc(), 1480 "Example keywords may be used only in the for_example section"); 1481 break; 1482 case TagConstants.NORMAL_EXAMPLE: 1483 if (behaviorMode == 1) 1484 ErrorSet 1485 .error(mp.getStartLoc(), 1486 "Example keywords may be used only in the for_example section"); 1487 mpv.addElement(VarExprModifierPragma.make(TagConstants.SIGNALS, 1488 FormalParaDecl.make(0, null, TagConstants.ExsuresIdnName, 1489 Types.javaLangException(), mp.getStartLoc()), 1490 AnnotationHandler.F, mp.getStartLoc()). 1491 setOriginalTag(TagConstants.SIGNALS_ONLY)); 1492 break; 1493 case TagConstants.EXCEPTIONAL_EXAMPLE: 1494 if (behaviorMode == 1) 1495 ErrorSet 1496 .error(mp.getStartLoc(), 1497 "Example keywords may be used only in the for_example section"); 1498 ExprModifierPragma empp = ExprModifierPragma.make( 1499 TagConstants.ENSURES, AnnotationHandler.F, mp.getStartLoc()); 1500 Utils.ensuresDecoration.set(empp, true); 1501 mpv.addElement(empp); 1502 break; 1503 default: 1504 // lightweight 1505 --pos; 1506 behavior = null; 1507 } 1508 } 1509 pos = parseSeq(pos, pm, 0, behavior, mpv); 1510 if (behaviorMode != 0 && behavior != null) { 1511 // Tag each heavyweight spec case 1512 //if (mpv.size() > 0) mpv.addElement(heavyweightFlag); 1513 } 1514 if (mpv.size() != 0) 1515 result.add(mpv); 1516 else if (behaviorMode == 0 || result.size() != 0) { 1517 if (!encounteredError) 1518 ErrorSet.error(pm.elementAt(pos).getStartLoc(), 1519 "JML does not allow empty clause sequences"); 1520 encounteredError = false; 1521 } 1522 if (pm.elementAt(pos).getTag() != TagConstants.ALSO) break; 1523 ++pos; 1524 } 1525 if (behaviorMode != 0) { 1526 while (pm.elementAt(pos).getTag() == TagConstants.CLOSEPRAGMA) { 1527 ErrorSet.error(pm.elementAt(pos).getStartLoc(), 1528 "There is no opening {| to match this closing |}"); 1529 ++pos; 1530 } 1531 } 1532 return pos; 1533 } 1534 1535 private boolean encounteredError; 1536 1537 /** Parse the clauses in a code_contract section */ 1538 public int parseCCSeq(int pos, ModifierPragmaVec pm, 1539 ModifierPragmaVec result) { 1540 boolean badCCSection = false; 1541 while (true) { 1542 ModifierPragma mp = pm.elementAt(pos); 1543 int loc = mp.getStartLoc(); 1544 int tag = mp.getTag(); 1545 // System.out.println("TAG " + TagConstants.toString(tag)); 1546 if (isRoutineModifier(tag)) return pos; 1547 switch (tag) { 1548 case TagConstants.END: 1549 case TagConstants.IMPLIES_THAT: 1550 case TagConstants.FOR_EXAMPLE: 1551 case TagConstants.ALSO: 1552 return pos; 1553 1554 case TagConstants.ACCESSIBLE: 1555 case TagConstants.CALLABLE: 1556 case TagConstants.MEASURED_BY: 1557 result.addElement(mp); 1558 ++pos; 1559 break; 1560 1561 default: 1562 if (!badCCSection) 1563 // Just one error message 1564 ErrorSet.error(loc, 1565 "Unexpected pragma in a code_contract section"); 1566 badCCSection = true; 1567 ++pos; 1568 break; 1569 } 1570 } 1571 } 1572 1573 //@ requires (* pm.elementAt(pm.size()-1).getTag() == TagConstants.END *); 1574 public int parseSeq(int pos, ModifierPragmaVec pm, int behaviorMode, 1575 ModifierPragma behavior, ModifierPragmaVec result) { 1576 int behaviorTag = behavior == null ? 0 : behavior.getTag(); 1577 //System.out.println("STARTING " + behaviorMode + " " + behaviorTag); 1578 if (pm.elementAt(pos).getTag() == TagConstants.MODEL_PROGRAM) { 1579 if (behaviorMode == 0) { 1580 ErrorSet.error(pm.elementAt(pos).getStartLoc(), 1581 "Model programs may not be nested"); 1582 encounteredError = true; 1583 } 1584 ++pos; 1585 } 1586 if (pm.elementAt(pos).getTag() == TagConstants.CODE_CONTRACT) { 1587 if (behaviorMode == 0) { 1588 ErrorSet.error(pm.elementAt(pos).getStartLoc(), 1589 "code_contract sections may not be nested"); 1590 encounteredError = true; 1591 } 1592 ++pos; 1593 } 1594 while (true) { 1595 ModifierPragma mp = pm.elementAt(pos); 1596 int loc = mp.getStartLoc(); 1597 int tag = mp.getTag(); 1598 if (isRoutineModifier(tag)) return pos; 1599 //System.out.println("TAG " + TagConstants.toString(tag)); 1600 switch (tag) { 1601 case TagConstants.END: 1602 case TagConstants.IMPLIES_THAT: 1603 case TagConstants.FOR_EXAMPLE: 1604 case TagConstants.ALSO: 1605 case TagConstants.CLOSEPRAGMA: 1606 return pos; 1607 1608 case TagConstants.MODEL_PROGRAM: 1609 ErrorSet.error(mp.getStartLoc(), 1610 "Model programs may not be combined with other clauses"); 1611 ++pos; 1612 break; 1613 1614 case TagConstants.CODE_CONTRACT: 1615 ErrorSet 1616 .error(mp.getStartLoc(), 1617 "code_contract sections may not be combined with other clauses"); 1618 ++pos; 1619 break; 1620 1621 case TagConstants.ACCESSIBLE: 1622 case TagConstants.CALLABLE: 1623 case TagConstants.MEASURED_BY: 1624 ErrorSet.error(mp.getStartLoc(), 1625 "This clause may only be in a code_contract section"); 1626 ++pos; 1627 break; 1628 1629 case TagConstants.BEHAVIOR: 1630 case TagConstants.NORMAL_BEHAVIOR: 1631 case TagConstants.EXCEPTIONAL_BEHAVIOR: 1632 case TagConstants.EXAMPLE: 1633 case TagConstants.NORMAL_EXAMPLE: 1634 case TagConstants.EXCEPTIONAL_EXAMPLE: 1635 if (behaviorMode == 0) 1636 ErrorSet.error(mp.getStartLoc(), "Misplaced " 1637 + TagConstants.toString(tag) + " keyword"); 1638 ++pos; 1639 break; 1640 1641 case TagConstants.OPENPRAGMA: { 1642 int openLoc = loc; 1643 ++pos; 1644 ArrayList s = new ArrayList(); 1645 pos = parseAlsoSeq(pos, pm, 0, behavior, s); 1646 if (pm.elementAt(pos).getTag() != TagConstants.CLOSEPRAGMA) { 1647 ErrorSet.error(pm.elementAt(pos).getStartLoc(), 1648 "Expected a closing |}", openLoc); 1649 } else { 1650 ++pos; 1651 } 1652 // Empty sequences are noted in parseAlsoSeq 1653 if (s.size() != 0) { 1654 result.addElement(NestedModifierPragma.make(s)); 1655 } 1656 } 1657 break; 1658 1659 // Any clause keyword ends up in the default (as well as 1660 // anything unrecognized). We do that because there are 1661 // so many clause keywords. However, that means that we 1662 // have to be sure to have the list of keywords in 1663 // isRoutineModifier correct. 1664 default: 1665 if ((((behaviorTag == TagConstants.NORMAL_BEHAVIOR || behaviorTag == TagConstants.NORMAL_EXAMPLE) && (tag == TagConstants.SIGNALS || tag == TagConstants.EXSURES))) 1666 || (((behaviorTag == TagConstants.EXCEPTIONAL_BEHAVIOR || behaviorTag == TagConstants.EXCEPTIONAL_EXAMPLE) && (tag == TagConstants.ENSURES || tag == TagConstants.POSTCONDITION)))) { 1667 ErrorSet.error(loc, "A " + TagConstants.toString(tag) 1668 + " clause is not allowed in a " 1669 + TagConstants.toString(behaviorTag) + " section", behavior 1670 .getStartLoc()); 1671 } else { 1672 result.addElement(mp); 1673 } 1674 ++pos; 1675 } 1676 } 1677 } 1678 } 1679 1680 /* 1681 * public static List findRepresents(FieldDecl fd) { TypeDecl td = fd.parent; 1682 * TypeDeclElemVec tdepv = td.elems; for (int i=0; i <tdepv.size(); ++i) { 1683 * TypeDeclElem tde = tdepv.elementAt(i); if (!(tde instanceof 1684 * TypeDeclElemPragma)) continue; if (tde.getTag() != TagConstants.REPRESENTS) 1685 * continue; Expr target = ((NamedExprDeclPragma)tde).target; if (!(target 1686 * instanceof FieldAccess)) { ErrorSet.error(tde.getStartLoc(), "INTERNAL 1687 * ERROR: Expected FieldAccess here"); continue; } FieldDecl fdd = 1688 * ((FieldAccess)target).decl; if (fd != fdd) continue; results.add( 1689 * ((NamedExprDeclPragma)tde).expr ); } return results; } 1690 */ 1691 static private ModifierPragma heavyweightFlag = SimpleModifierPragma.make( 1692 TagConstants.BEHAVIOR, Location.NULL); 1693 } 1694 // FIXME - things not checked 1695 // There should be no clauses after a |} (only |} only also or END or simple 1696 // mods) 1697 // The order of clauses is not checked 1698 // JML only allows forall, old, requires prior to a nesting.