001 /* Copyright 2000, 2001, Compaq Computer Corporation */ 002 003 package escjava.backpred; 004 005 import java.util.Enumeration; 006 import java.util.Hashtable; 007 import java.util.Vector; 008 import java.util.LinkedList; 009 010 import javafe.ast.*; 011 import escjava.ast.*; 012 import escjava.ast.TagConstants; 013 import escjava.ast.Modifiers; 014 import escjava.ast.ExprDeclPragmaVec; // compiler bug workaround 015 016 import javafe.tc.*; 017 import javafe.util.*; 018 019 import escjava.translate.GC; 020 import escjava.translate.GetSpec; 021 import escjava.translate.Inner; 022 import escjava.translate.Translate; 023 import escjava.translate.Helper; 024 025 /** 026 * This class is responsible for determining the contributors to a 027 * given TypeSig or RoutineDecl. 028 * 029 * <p> The contributors are divided into a set of TypeSigs, a set of 030 * Invariants, and a set of Fields. 031 */ 032 033 public class FindContributors 034 { 035 // Public interface 036 037 /** 038 * Generate the contributors for a given TypeSig. This may result 039 * in errors being reported and TypeSigs being type checked. <p> 040 * 041 * The originType is taken to be that Typesig.<p> 042 * 043 * Precondition: T must have been typechecked.<p> 044 * 045 * Note: in the process of locating contributors, 046 * FindContributors may type check additional types leading 047 * possibly to type errors. If such error(s) occur, a fatal 048 * error is reproted. 049 */ 050 public FindContributors(/*@ non_null @*/ TypeSig T) { 051 originType = T; 052 addType(T); 053 054 walk(T.getTypeDecl()); 055 fieldToPossible = null; // conserve space 056 057 if (Info.on) { 058 Info.out("[[contributors: " 059 + contributorTypes.size() + " types " 060 + contributorInvariants.size() + " invariants " 061 + contributorFields.size() + " fields ]]"); 062 } 063 } 064 065 /** 066 * Generate the contributors for a given RoutineDecl. This may 067 * result in errors being reported and TypeSigs being type checked.<p> 068 * 069 * The originType is taken to be the type declaring that RoutineDecl.<p> 070 * 071 * Precondition: the type declaring rd must have been typechecked.<p> 072 * 073 * Note: in the process of locating contributors, 074 * FindContributors may type check additional types leading 075 * possibly to type errors. If such error(s) occur, a fatal 076 * error is reproted. 077 */ 078 public FindContributors(/*@ non_null @*/ RoutineDecl rd) { 079 originType = TypeSig.getSig(rd.parent); 080 addType(originType); 081 082 walk(rd); 083 fieldToPossible = null; // conserve space 084 085 if (Info.on) { 086 Info.out("[[local contributors: " 087 + contributorTypes.size() + " types " 088 + contributorInvariants.size() + " invariants " 089 + contributorFields.size() + " fields ]]"); 090 } 091 } 092 093 094 /** 095 * Our origin type; used to determine visibility and accessibility 096 * when needed. 097 */ 098 public TypeSig originType; 099 100 101 /** 102 * Enumerate the TypeSig contributors 103 */ 104 public Enumeration typeSigs() { 105 return contributorTypes.elements(); 106 } 107 108 /** 109 * Enumerate the invariant contributors 110 */ 111 public Enumeration invariants() { 112 return contributorInvariants.elements(); 113 } 114 115 /** 116 * Enumerate the field contributors 117 */ 118 public Enumeration fields() { 119 return contributorFields.elements(); 120 } 121 122 123 // Closure code 124 125 /** The set of routines visited so far. 126 */ 127 128 private /*@ non_null @*/ Set visitedRoutines = new Set(); 129 130 /** 131 * The set of TypeSigs we've determined to be contributors so far. <p> 132 * 133 * Invariant: This set is closed under taking supertypes 134 */ 135 private /*@ non_null @*/ Set contributorTypes = new Set(); 136 137 /** 138 * The set of invariants (elementType ExprDeclPragmas) we've 139 * determined to be contributors so far. <p> 140 * 141 * Closure Property: walk(-) has been called on each of 142 * these invariants. 143 */ 144 private /*@ non_null @*/ Set contributorInvariants = new Set(); 145 146 /** 147 * The set of fields (elementType FieldDecl) we've determined to be 148 * contributors so far. <p> 149 * 150 * Closure Property: 151 * 152 * all invariants J that are declared in types in 153 * contributorTypes and "mention the field" f for f a field in 154 * contributorFields are members of contributorInvariants 155 */ 156 private /*@ non_null @*/ Set contributorFields = new Set(); 157 158 public int preFieldMode = 0; 159 public /*@ non_null @*/ Set preFields = new Set(); 160 161 /** 162 * A mapping from fields (FieldDecls) to possible invariant 163 * contributors (ExprDeclPragmaVec). <p> 164 * 165 * (An invariant is a possible contributor if it is declared in a 166 * type of contributorTypes.) 167 * 168 * Invariant: 169 * 170 * if (f,J) in fieldToPossible then the invariant J "mentions 171 * the field" f and J is a possible invariant contributor 172 * 173 * Closure property: 174 * 175 * if J is possible invariant contributor, 176 * J not in contributorInvariants, and J "mentions the field" f, 177 * then (f,J) is in fieldToPossible. 178 * 179 */ 180 // can be null 181 Hashtable fieldToPossible = new Hashtable(); 182 183 184 185 /** 186 * Add the TypeSigs mentioned explicitly in a given Type to 187 * contributorTypes, maintaining all the closure properties. <p> 188 * 189 * Precondition: T has been resolved.<p> 190 */ 191 //@ requires T != null; 192 private void addType(Type T) { 193 // TypeName case: 194 if (T instanceof TypeName) { 195 T = TypeSig.getSig((TypeName)T); 196 Assert.precondition(T != null); 197 } 198 199 // ArrayType case: 200 if (T instanceof ArrayType) { 201 addType(((ArrayType)T).elemType); 202 return; 203 } 204 205 // PrimitiveType case: 206 if (T instanceof PrimitiveType) 207 return; 208 209 /* 210 * Remaining case is TypeSig: 211 */ 212 TypeSig sig = (TypeSig)T; 213 if (contributorTypes.contains(sig)) 214 return; 215 216 // make sure sig is typechecked: 217 typecheck(sig); 218 219 // Close over taking supertypes: 220 TypeDecl td = sig.getTypeDecl(); 221 if (td instanceof ClassDecl) { 222 ClassDecl cd = (ClassDecl)td; 223 if (cd.superClass != null) 224 addType(cd.superClass); 225 } 226 for (int i=0; i<td.superInterfaces.size(); i++) 227 addType(td.superInterfaces.elementAt(i)); 228 229 contributorTypes.add(sig); 230 231 // Add sig's invariants as possible contributor invariants: 232 for (int i = 0; i<td.elems.size(); i++) { 233 TypeDeclElem tde = td.elems.elementAt(i); 234 235 if (tde.getTag() == TagConstants.INVARIANT) 236 addPossibleInvariant((ExprDeclPragma)tde); 237 } 238 239 240 /* 241 * Hack: for 1.1, add an inner classes' this$0 pointer when 242 * that class is added as a type, rather than trying to keep 243 * track of everywhere it might be introduced. 244 */ 245 if (!sig.isTopLevelType()) { 246 FieldDecl thisptr = Inner.getEnclosingInstanceField(sig); 247 248 backedgeToGenericVarDecl(thisptr, null, true, new LinkedList()); 249 } 250 } 251 252 253 /** 254 * Add a given field to contributorFields, maintaining all the 255 * closure properties. <p> 256 */ 257 //@ requires fd != null; 258 private void addField(FieldDecl fd) { 259 if (contributorFields.contains(fd)) 260 return; 261 262 contributorFields.add(fd); 263 264 /* 265 * Turn possible invariant contributors that mention fd into 266 * real ones. We use fieldToPossible to do this quickly. 267 */ 268 ExprDeclPragmaVec newInvariants = 269 (ExprDeclPragmaVec)fieldToPossible.get(fd); 270 if (newInvariants==null) 271 return; 272 273 // Note: newInvariants is not modified here because we added fd to 274 // contributorFields 275 for (int i=0; i<newInvariants.size(); i++) 276 addInvariant(newInvariants.elementAt(i)); 277 } 278 279 /** 280 * Add the mapping (fd, J) to fieldToPossible. 281 * 282 * Precondition: J is a possible invariant contributor, J "mentions 283 * the field" fd. 284 */ 285 private void addPossibleMentions(FieldDecl fd, /*@ non_null @*/ ExprDeclPragma J) { 286 ExprDeclPragmaVec range = (ExprDeclPragmaVec)fieldToPossible.get(fd); 287 if (range==null) { 288 range = ExprDeclPragmaVec.make(); 289 fieldToPossible.put(fd, range); 290 } 291 292 range.addElement(J); 293 } 294 295 296 /** 297 * Add a possible invariant contributor to either fieldToPossible 298 * or contributorInvariants as approperiate, maintaining all 299 * closure properties. <p> 300 * 301 * Precondition: J has been type checked. 302 */ 303 //@ requires J != null; 304 private void addPossibleInvariant(ExprDeclPragma J) { 305 FieldDeclVec fieldsMentioned = fieldsInvariantMentions(J); 306 307 for (int i=0; i<fieldsMentioned.size(); i++) { 308 FieldDecl fd = fieldsMentioned.elementAt(i); 309 310 if (contributorFields.contains(fd)) { 311 // Ah! J is actually a real invariant contributor: 312 addInvariant(J); 313 return; 314 } 315 316 // Add (f,J) to fieldToPossible: 317 addPossibleMentions(fd, J); 318 } 319 } 320 321 /** 322 * Add a given invariant to contributorInvarints, maintaining all 323 * closure properties. <p> 324 * 325 * Precondition: J has been type checked. 326 */ 327 //@ requires J != null; 328 private void addInvariant(ExprDeclPragma J) { 329 if (contributorInvariants.contains(J)) 330 return; 331 332 contributorInvariants.add(J); 333 334 walk(J); 335 } 336 337 338 // Walking ASTNodes 339 340 /** 341 * Walks a given ASTNode, adding all the types it "mentions" via 342 * addType and adding all the fields it "mentions" via 343 * addField. <p> 344 * 345 * Precondition: N has been typechecked. 346 * 347 * WARNING: N is assumed to have no free local or parameter 348 * varables. 349 */ 350 private void walk(ASTNode N) { 351 walk(N, null, true, new LinkedList()); 352 } 353 354 355 /** 356 * Returns the set of fields that a given invariant mentions. <p> 357 * 358 * Precondition: J must be an invariant, J must be typechecked. 359 */ 360 private FieldDeclVec fieldsInvariantMentions(ExprDeclPragma J) { 361 // We may cache this function later... 362 363 FieldDeclVec result = FieldDeclVec.make(); 364 walk(J, result, false, new LinkedList()); 365 return result; 366 } 367 368 369 /** 370 * Walks a given ASTNode, finding all the types it "mentions" and 371 * all the fields it "mentions". <p> 372 * 373 * If fields is null, the fields mentioned are added via addField; 374 * otherwise, they are added to fields directly.<p> 375 * 376 * If addTypes is true, the types mentioned are added via addType.<p> 377 * 378 * Precondition: N has been typechecked. 379 */ 380 private void walk(ASTNode N, FieldDeclVec fields, boolean addTypes, 381 LinkedList visited) { 382 /* 383 * Leaf nodes: 384 */ 385 if (N==null) 386 return; 387 if (N instanceof Type) { 388 if (addTypes) 389 addType((Type)N); 390 return; 391 } 392 393 if (N instanceof LiteralExpr || N instanceof ClassLiteral) { 394 Expr lit = (Expr)N; 395 if (addTypes) { 396 addType(TypeCheck.inst.getType(lit)); 397 } 398 } 399 400 /* 401 * Handle relevant backedges: 402 */ 403 if (N instanceof VariableAccess) { 404 backedgeToGenericVarDecl(((VariableAccess)N).decl, 405 fields, addTypes, visited); 406 } 407 if (N instanceof FieldAccess) { 408 if (preFieldMode > 0) { 409 preFields.add(N); 410 } 411 backedgeToGenericVarDecl(((FieldAccess)N).decl, 412 fields, addTypes, visited); 413 } 414 415 if (N instanceof ConstructorInvocation) { 416 ConstructorInvocation ci = (ConstructorInvocation) N; 417 visited.addFirst(ci.decl); 418 int inline = Translate.inlineDecoration.get(ci) != null ? 2 : 419 isNonRecursiveHelperInvocation(ci.decl) ? 1 : 0; 420 backedgeToRoutineDecl(ci.decl, fields, addTypes, inline, visited); 421 } 422 if (N instanceof NewInstanceExpr) { 423 NewInstanceExpr ni = (NewInstanceExpr) N; 424 int inline = Translate.inlineDecoration.get(ni) != null ? 2 : 425 isNonRecursiveHelperInvocation(ni.decl) ? 1 : 0; 426 backedgeToRoutineDecl(ni.decl,fields, addTypes, inline, visited); 427 } 428 if (N instanceof MethodInvocation) { 429 MethodInvocation mi = (MethodInvocation) N; 430 int inline = Translate.inlineDecoration.get(mi) != null ? 2 : 431 isNonRecursiveHelperInvocation(mi.decl) ? 1 : 0; 432 433 backedgeToRoutineDecl(mi.decl, fields, addTypes, inline, visited); 434 } 435 // FIXME - add the type from quantified expression? set comprehension expr? new array expr? 436 /* 437 * Add references not explicitly in Java code or from backedges: 438 */ 439 if (N instanceof RoutineDecl) { 440 // Get references in our derived spec: 441 backedgeToRoutineDecl((RoutineDecl)N, fields, addTypes, 0, visited); 442 443 // Add implicit references if N is a ConstructorDecl: 444 if (N instanceof ConstructorDecl) 445 addImplicitConstructorRefs((ConstructorDecl)N, 446 fields, addTypes, visited); 447 } 448 449 if (N.getTag() == TagConstants.PRE) { 450 ++preFieldMode; 451 } 452 453 454 455 /* 456 * Recurse to subnodes (this automatically ignores backedges): 457 * 458 * We intentionally skip TypeDecls so that we stay in the same type. 459 */ 460 try { 461 int size = N.childCount(); 462 for (int i=0; i<size; i++) { 463 Object child = N.childAt(i); 464 if (child instanceof ASTNode && !(child instanceof TypeDecl)) 465 walk((ASTNode)child, fields, addTypes, visited); 466 } 467 } finally { 468 if (N.getTag() == TagConstants.PRE) { 469 --preFieldMode; 470 } 471 } 472 } 473 474 /** Returns <code>true</code> if and only if <code>r</code> is a helper 475 * routine that has not been visited by this <code>FindContributor</code> 476 * object. 477 */ 478 479 private boolean isNonRecursiveHelperInvocation(/*@ non_null */ RoutineDecl r) { 480 return Helper.isHelper(r) && !visitedRoutines.contains(r); 481 } 482 483 /** 484 * Add implicit references from a ConstructorDecl that do not 485 * appear in Java code or via backedges as per walk(,,). 486 * 487 * Precondition: the type declaring cd has been typechecked. 488 */ 489 private void addImplicitConstructorRefs(/*@ non_null @*/ ConstructorDecl cd, 490 FieldDeclVec fields, 491 boolean addTypes, 492 LinkedList visited) { 493 /* 494 * Walk the initialization code derived from the same class as 495 * the constructor: 496 */ 497 TypeDecl td = cd.parent; 498 walkInstanceInitialier(td, fields, addTypes, visited); 499 500 /* 501 * For all superinterfaces that the constructor's type 502 * implements that are not already implemented by its 503 * superclass(es), walk the initialization code derived from 504 * them: 505 */ 506 Enumeration FII = GetSpec.getFirstInheritedInterfaces((ClassDecl)td); 507 while (FII.hasMoreElements()) { 508 walkInstanceInitialier((TypeDecl)FII.nextElement(), fields, 509 addTypes, visited); 510 } 511 } 512 513 514 /** 515 * Walk the implicit instance initializer code for a given 516 * TypeDecl, excluding any field initializations of 517 * superinterface fields. <p> 518 * 519 * E.g., f_1 = 0; ...; f_3 = <initializer exp>; ... ; <instance 520 * initializer block>... 521 * 522 * This is the code that constructors of that type implicitly 523 * start with after their super/sibling call modulo the 524 * initialization of superinterface fields. 525 * 526 * See addImplicitConstructorRefs for the full version w/o the 527 * exclusion. 528 * 529 * 530 * Addition: This now also pulls in all invariants in the given 531 * TypeDecl, regardless of what they mention. This is 532 * to avoid user surprise; see also Vanilla.java in 533 * test58. 534 * 535 * 536 * Precondition: the TypeDecl has been typechecked. 537 */ 538 private void walkInstanceInitialier(/*@ non_null @*/ TypeDecl td, 539 FieldDeclVec fields, 540 boolean addTypes, 541 LinkedList visited) { 542 for (int i = 0; i < td.elems.size(); i++) { 543 TypeDeclElem tde = td.elems.elementAt(i); 544 545 if (tde.getTag() == TagConstants.INVARIANT) 546 addInvariant((ExprDeclPragma)tde); 547 548 if (tde instanceof ModelDeclPragma) 549 tde = ((ModelDeclPragma)tde).decl; 550 if (tde instanceof GhostDeclPragma) 551 tde = ((GhostDeclPragma)tde).decl; 552 if (tde.getTag() == TagConstants.FIELDDECL 553 && !Modifiers.isStatic(((FieldDecl)tde).modifiers)) { 554 FieldDecl fd = (FieldDecl)tde; 555 556 // walk "fd := (fd.init==null ? <zero-equivalent> : fd.init)": 557 backedgeToGenericVarDecl(fd, fields, addTypes, visited); 558 walk(fd.init, fields, addTypes, visited); 559 560 } else if (tde.getTag() == TagConstants.INITBLOCK 561 && !Modifiers.isStatic(((InitBlock)tde).modifiers)) { 562 // walk any instance initializer blocks found: 563 walk((InitBlock)tde, fields, addTypes, visited); 564 565 } 566 } 567 } 568 569 570 /** 571 * Calculate the fields and types "mentioned" by a backedge to a 572 * GenericVarDecl and then add them as per walk(,,). 573 */ 574 private void backedgeToGenericVarDecl(GenericVarDecl decl, 575 FieldDeclVec fields, 576 boolean addTypes, 577 LinkedList visited) { 578 // The length field of arraytypes is never considered "mentioned": 579 if (decl==javafe.tc.Types.lengthFieldDecl) 580 return; 581 582 if (decl instanceof FieldDecl) { 583 FieldDecl fd = (FieldDecl)decl; 584 typecheck(TypeSig.getSig(fd.parent)); 585 586 587 // The range and domain types of fd are "mentioned": 588 addType(fd.type); 589 if (fd.parent != null) // "length" field has no parent... 590 addType(TypeSig.getSig(fd.parent)); 591 592 /* 593 * Exit if have already processed this field; need to do 594 * this to avoid recursion in case the field's modifiers 595 * mention it. 596 */ 597 if (fields==null) { 598 if (contributorFields.contains(fd)) 599 return; 600 } else if (fields.contains(fd)) 601 return; 602 603 604 // The field fd is "mentioned": 605 if (fields != null) 606 fields.addElement(fd); 607 else 608 addField(fd); 609 610 /* 611 * We need to walk the "spec" part of fd as well to handle 612 * readable_if and the like: 613 */ 614 if (fd.pmodifiers != null) { 615 for (int i=0; i<fd.pmodifiers.size(); i++) 616 walk(fd.pmodifiers.elementAt(i), fields, addTypes, visited); 617 } 618 } 619 620 /* 621 * Ignore local & parameter variable Decls here, as they 622 * should already have been walked over. 623 */ 624 } 625 626 /** 627 * Calculate the fields and types "mentioned" by a backedge to a 628 * RoutineDecl and then add them as per walk(,,). <p> 629 * 630 * <code>inlined</code> is one of: 0 (not an inlined routine), 631 * 1 (an inlined helper routine), or 2 (a routine inlined for 632 * a reason other than being a helper). (Why this complication, 633 * why not just use a boolean field "inlined"? By distinguishing 634 * cases 1 and 2, one can write a nice run-time assert inside the 635 * implementation of this method.) 636 */ 637 //@ requires inlined == 0 || inlined == 1 || inlined == 2; 638 private void backedgeToRoutineDecl(RoutineDecl rd, 639 FieldDeclVec fields, 640 boolean addTypes, 641 int inlined, LinkedList visited) { 642 if (rd == null) return; // FIXME - this happens with some NewInstanceExpr 643 // FIXME - remove references to visited 644 //if (visited.contains(rd)) return; 645 //visited.addFirst(rd); 646 if (inlined==0 && visitedRoutines.contains(rd)) return; 647 //Assert.notFalse(inlined != 1 || !visitedRoutines.contains(rd)); 648 visitedRoutines.add(rd); 649 650 TypeSig thisType = TypeSig.getSig(rd.parent); 651 typecheck(thisType); 652 653 /* 654 * Temporarily set GC.thisvar's type to thisType; we need to 655 * do this because GetSpec.getCombinedMethodDecl() returns 656 * GC.thisvar as the first argument of instance methods. 657 * 658 * If we don't do this, we may add the wrong type when we add 659 * the types of the routine's arguments below. 660 */ 661 Type savedType = GC.thisvar.decl.type; 662 GC.thisvar.decl.type = thisType; 663 664 // Get the derived spec for rd: 665 DerivedMethodDecl dmd = GetSpec.getCombinedMethodDecl(rd); 666 dmd = GetSpec.filterMethodDecl(dmd, this); 667 668 669 /* 670 * The types in the called routine's Java signature are 671 * "mentioned" (including the type of Constructors): */ 672 if (addTypes) { 673 // Add args here mostly for safely reasons 674 for (int i=0; i<dmd.args.size(); i++) 675 addType(dmd.args.elementAt(i).type); 676 for (int i=0; i<dmd.throwsSet.size(); i++) 677 addType(dmd.throwsSet.elementAt(i)); 678 addType(dmd.returnType); 679 } 680 681 // We also need to walk the routine's spec: 682 for (int i=0; i<dmd.requires.size(); i++) 683 walk(dmd.requires.elementAt(i), fields, addTypes, visited); 684 if (inlined == 0) { 685 // Add modifies here mostly for safely reasons 686 for (int i=0; i<dmd.modifies.size(); i++) 687 walk(dmd.modifies.elementAt(i), fields, addTypes, visited); 688 } 689 for (int i=0; i<dmd.ensures.size(); i++) 690 walk(dmd.ensures.elementAt(i), fields, addTypes, visited); 691 for (int i=0; i<dmd.exsures.size(); i++) 692 walk(dmd.exsures.elementAt(i), fields, addTypes, visited); 693 694 if (inlined != 0) { 695 walk(rd.body, fields, addTypes, visited); 696 } 697 698 GC.thisvar.decl.type = savedType; 699 //visited.removeFirst(); 700 } 701 702 703 // Utility routines 704 705 /** 706 * Make sure a given TypeSig has been type checked, type checking 707 * it if necessary. <p> 708 * 709 * Throws a fatal error if a type error occurs while checking sig. 710 */ 711 void typecheck(/*@ non_null @*/ TypeSig sig) { 712 int errorCount = ErrorSet.errors; 713 714 sig.typecheck(); 715 if (errorCount == ErrorSet.errors) 716 return; 717 718 ErrorSet.fatal("A type error has occurred at an unexpected point;" 719 + " unable to continue processing"); 720 } 721 }