001package daikon; 002 003import java.io.IOException; 004import java.io.ObjectInputStream; 005import java.io.Serializable; 006import org.checkerframework.checker.interning.qual.Interned; 007import org.checkerframework.checker.lock.qual.GuardSatisfied; 008import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf; 009import org.checkerframework.checker.nullness.qual.Nullable; 010import org.checkerframework.dataflow.qual.Pure; 011import org.checkerframework.dataflow.qual.SideEffectFree; 012import org.plumelib.reflection.ReflectionPlume; 013 014/** 015 * PptName is an immutable ADT that represents naming data associated with a given program point, 016 * such as the class or method. 017 * 018 * <p>Examples below are as if the full value of this PptName were 019 * "DataStructures.StackAr.pop()Ljava/lang/Object;:::EXIT84" 020 * 021 * <p>PptName is deprecated, because declaration file format 2 should not need it. Uses of PptName 022 * should be eliminated. 023 */ 024// No "@Deprecated" annotation yet, but we should add it once support for 025// file format 1 is removed from Daikon. 026public class PptName implements Serializable { 027 static final long serialVersionUID = 20020122L; 028 029 // These are never changed but cannot be declared "final", because they 030 // must be re-interned upon deserialization. 031 /** Full program point name. */ 032 private @Interned String fullname; 033 034 // fn_name and point together comprise fullname 035 /** The part of fullname before ":::" */ 036 private @Interned String fn_name; 037 038 /** Post-separator (separator is ":::") */ 039 private @Interned String point; 040 041 // cls and method together comprise fn_name 042 /** Fully-qualified class name. */ 043 private @Nullable @Interned String cls; 044 045 /** Method signature, including types. */ 046 private final @Nullable @Interned String method; 047 048 // Representation invariant: 049 // 050 // fullname must contain ":::". 051 // fn_name is the part of fullname before ::: and point is the part after. 052 // If fn_name does contain a '(' and a '.' that comes before it, then 053 // cls is the portion before the dot and method is the portion after. 054 // If fn_name contains '(' but no dot, cls is null and method 055 // is the same as fn_name. 056 // If fn_name does not contain '(', then class is the same as fn_name and 057 // method is null. 058 059 // ==================== CONSTRUCTORS ==================== 060 061 /** 062 * @param name non-null ppt name as given in the decls file 063 */ 064 public PptName(String name) { 065 // If the name is well-formed, like "mvspc.setupGUI()V:::EXIT75", 066 // then this constructor will extract the class and method names. 067 // If not (eg for lisp code), it's okay because only the GUI uses 068 // this class/method information. 069 070 fullname = name.intern(); 071 int separatorPosition = name.indexOf(FileIO.ppt_tag_separator); 072 if (separatorPosition == -1) { 073 throw new Daikon.UserError("no ppt_tag_separator in '" + name + "'"); 074 // // probably a lisp program, which was instrumented differently 075 // cls = method = point = fn_name = null; 076 // return; 077 } 078 fn_name = name.substring(0, separatorPosition).intern(); 079 point = name.substring(separatorPosition + FileIO.ppt_tag_separator.length()).intern(); 080 081 int lparen = fn_name.indexOf('('); 082 if (lparen == -1) { 083 cls = fn_name; 084 method = null; 085 return; 086 } 087 int dot = fn_name.lastIndexOf('.', lparen); 088 if (dot == -1) { 089 method = fn_name; 090 cls = null; 091 return; 092 } 093 // now 0 <= dot < lparen 094 cls = fn_name.substring(0, dot).intern(); 095 method = fn_name.substring(dot + 1).intern(); 096 } 097 098 /** 099 * Creates a new PptName. {@code className} or {@code methodName} (or both) must be non-null. 100 * 101 * @param className fully-qualified class name 102 * @param methodName method signature, including types 103 * @param pointName post-separator (separator is ":::") 104 */ 105 public PptName(@Nullable String className, @Nullable String methodName, String pointName) { 106 if ((className == null) && (methodName == null)) { 107 throw new UnsupportedOperationException("One of class or method must be non-null"); 108 } 109 // First set class name 110 if (className != null) { 111 cls = className.intern(); 112 fn_name = cls; 113 } 114 // Then add method name 115 if (methodName == null) { 116 method = null; 117 if (fn_name == null) { 118 throw new RuntimeException("fn_name should not be null; probably bad arguments"); 119 } 120 } else { 121 method = methodName.intern(); 122 if (cls != null) { 123 fn_name = (cls + "." + method).intern(); 124 } else { 125 fn_name = method; 126 } 127 } 128 assert fn_name != null; 129 // Finally, add point 130 point = pointName.intern(); 131 fullname = (fn_name + FileIO.ppt_tag_separator + point).intern(); 132 } 133 134 // ==================== OBSERVERS ==================== 135 136 /** 137 * Returns getName() [convenience accessor]. 138 * 139 * @return getName() [convenience accessor] 140 * @see #getName() 141 */ 142 @Pure 143 public String name() { 144 return getName(); 145 } 146 147 /** 148 * Returns the complete program point name, e.g., 149 * "DataStructures.StackAr.pop()Ljava/lang/Object;:::EXIT84". 150 * 151 * @return the complete program point name 152 */ 153 @Pure 154 public String getName() { 155 return fullname; 156 } 157 158 /** 159 * Returns the fully-qualified class name, which uniquely identifies a given class. May be null. 160 * e.g. "DataStructures.StackAr". 161 * 162 * @return the fully-qualified class name 163 */ 164 public @Nullable String getFullClassName() { 165 return cls; 166 } 167 168 /** 169 * Returns the short name of the class, not including any additional context, such as the package 170 * it is in. May be null. e.g. "StackAr". 171 * 172 * @return the short name of the class, or null 173 */ 174 public @Nullable String getShortClassName() { 175 if (cls == null) { 176 return null; 177 } 178 int pt = cls.lastIndexOf('.'); 179 if (pt == -1) { 180 return cls; 181 } else { 182 return cls.substring(pt + 1); 183 } 184 } 185 186 /** 187 * Returns a guess at the package name. May be null. 188 * 189 * @return a guess at the package name. May be null 190 */ 191 public @Nullable String getPackageName() { 192 if (cls == null) { 193 return null; 194 } 195 int pt = cls.lastIndexOf('.'); 196 if (pt == -1) { 197 return null; 198 } else { 199 return cls.substring(0, pt); 200 } 201 } 202 203 /** 204 * Returns the full name which can uniquely identify a method within a class. The name includes 205 * symbols for the argument types and return type. May be null. e.g. "pop()Ljava/lang/Object;". 206 * 207 * @return the full name which can uniquely identify a method within a class 208 */ 209 public @Nullable String getSignature() { 210 return method; 211 } 212 213 /** 214 * Returns the name (identifier) of the method, not taking into account any arguments, return 215 * values, etc. May be null. e.g. "pop". 216 * 217 * @return the name (identifier) of the method, or null 218 */ 219 public @Nullable String getMethodName() { 220 if (method == null) { 221 return null; 222 } 223 int lparen = method.indexOf('('); 224 assert lparen >= 0; 225 return method.substring(0, lparen); 226 } 227 228 /** 229 * Returns the fully-qualified class and method name (and signature). Does not include any point 230 * information (such as ENTER or EXIT). May be null. e.g. 231 * "DataStructures.StackAr.pop()Ljava/lang/Object;" 232 * 233 * @return the fully-qualified class and method name (and signature) 234 */ 235 public @Nullable @Interned String getNameWithoutPoint() { 236 return fn_name; 237 // if (cls == null && method == null) { 238 // return null; 239 // } 240 // if (cls == null) { return method; } 241 // if (method == null) { return cls; } 242 // return (cls + "." + method).intern(); 243 } 244 245 /** 246 * Returns something interesting and descriptive about this point, along the lines of "ENTER" or 247 * "EXIT" or some such. The semantics of this method are not yet decided, so don't try to do 248 * anything useful with this result. May be null. e.g. "EXIT84". 249 * 250 * @return something interesting and descriptive about this 251 */ 252 public @Nullable String getPoint() { 253 return point; 254 } 255 256 /** 257 * Returns a numerical subscript of the given point, or Integer.MIN_VALUE if none exists. e.g. 258 * "84". 259 * 260 * @return a numerical subscript of the given point, or Integer.MIN_VALUE if none exists 261 * @see #exitLine() 262 */ 263 public int getPointSubscript() { 264 int result = Integer.MIN_VALUE; 265 if (point != null) { 266 // returns the largest substring [i..] which parses to an integer 267 for (int i = 0; i < point.length(); i++) { 268 char c = point.charAt(i); 269 if (('0' <= c) && (c <= '9')) { 270 try { 271 result = Integer.parseInt(point.substring(i)); 272 break; 273 } catch (NumberFormatException e) { 274 // continue; 275 } 276 } 277 } 278 } 279 return result; 280 } 281 282 /** 283 * Returns true iff this name refers to a synthetic object instance program point. 284 * 285 * @return true iff this name refers to a synthetic object instance program point 286 */ 287 @Pure 288 public boolean isObjectInstanceSynthetic() { 289 return FileIO.object_suffix.equals(point); 290 } 291 292 /** 293 * Returns true iff this name refers to a synthetic class instance program point. 294 * 295 * @return true iff this name refers to a synthetic class instance program point 296 */ 297 @Pure 298 public boolean isClassStaticSynthetic() { 299 return FileIO.class_static_suffix.equals(point); 300 } 301 302 /** 303 * Returns true iff this name refers to program globals. 304 * 305 * @return true iff this name refers to program globals 306 */ 307 @Pure 308 public boolean isGlobalPoint() { 309 return FileIO.global_suffix.equals(point); 310 } 311 312 /** 313 * Returns true iff this name refers to a procedure exit point. 314 * 315 * @return true iff this name refers to a procedure exit point 316 */ 317 @EnsuresNonNullIf(result = true, expression = "point") 318 @Pure 319 public boolean isExitPoint() { 320 return (point != null) && point.startsWith(FileIO.exit_suffix); 321 } 322 323 /** 324 * Returns true iff this name refers to an abrupt completion point. 325 * 326 * @return true iff this name refers to an abrupt completion point 327 */ 328 @EnsuresNonNullIf(result = true, expression = "point") 329 @Pure 330 public boolean isThrowsPoint() { 331 return (point != null) && point.startsWith(FileIO.throws_suffix); 332 } 333 334 /** 335 * Returns true iff this name refers to a combined (synthetic) procedure exit point. 336 * 337 * @return true iff this name refers to a combined (synthetic) procedure exit point 338 */ 339 @EnsuresNonNullIf(result = true, expression = "point") 340 @Pure 341 public boolean isCombinedExitPoint() { 342 return (point != null) && point.equals(FileIO.exit_suffix); 343 } 344 345 /** 346 * Returns true iff this name refers to an actual (not combined) procedure exit point (eg, 347 * EXIT22). 348 * 349 * @return true iff this name refers to an actual (not combined) procedure exit point 350 */ 351 @EnsuresNonNullIf(result = true, expression = "point") 352 @Pure 353 public boolean isNumberedExitPoint() { 354 return (point != null) && (isExitPoint() && !isCombinedExitPoint()); 355 } 356 357 /** 358 * Returns true iff this name refers to a procedure exit point. 359 * 360 * @return true iff this name refers to a procedure exit point 361 */ 362 @EnsuresNonNullIf(result = true, expression = "point") 363 @Pure 364 public boolean isEnterPoint() { 365 return (point != null) && point.startsWith(FileIO.enter_suffix); 366 } 367 368 /** 369 * Returns a string containing the line number, if this is an exit point; otherwise, returns an 370 * empty string. 371 * 372 * @return a string containing the line number, if this is an exit point; otherwise, return an 373 * empty string 374 * @see #getPointSubscript() 375 */ 376 public String exitLine() { 377 if (!isExitPoint()) { 378 return ""; 379 } 380 int non_digit; 381 for (non_digit = FileIO.exit_suffix.length(); non_digit < point.length(); non_digit++) { 382 if (!Character.isDigit(point.charAt(non_digit))) { 383 break; 384 } 385 } 386 return point.substring(FileIO.exit_suffix.length(), non_digit); 387 } 388 389 /** 390 * Returns true iff this program point is a constructor entry or exit. There are two ways in which 391 * this works. With the older declaration format, the method name starts with {@code <init>}. The 392 * newer declaration format does not have {@code <init>} but their method name includes the class 393 * name. For compatibility both mechanisms are checked. 394 * 395 * @return true iff this program point is a constructor entry or exit 396 */ 397 @Pure 398 public boolean isConstructor() { 399 400 if (method != null) { 401 402 if (method.startsWith("<init>")) { 403 return true; 404 } 405 406 if (cls == null) { 407 return false; 408 } 409 410 @SuppressWarnings("signature") // cls is allowed to be arbitrary, especially for non-Java code 411 String class_name = ReflectionPlume.fullyQualifiedNameToSimpleName(cls); 412 assert method != null; // for nullness checker 413 int arg_start = method.indexOf('('); 414 String method_name = method; 415 if (arg_start != -1) { 416 method_name = method.substring(0, arg_start); 417 } 418 419 // System.out.println ("fullname = " + fullname); 420 // System.out.println ("fn_name = " + fn_name); 421 // System.out.println ("method = " + method); 422 // System.out.println ("cls = " + cls); 423 // System.out.println ("class_name = " + class_name); 424 // System.out.println ("method_name = " + method_name); 425 426 if (class_name.equals(method_name)) { 427 return true; 428 } 429 } 430 431 return false; 432 } 433 434 /** 435 * Debugging output. 436 * 437 * @return a string representation of this 438 */ 439 public String repr() { 440 return "PptName: fullname=" 441 + fullname 442 + "; fn_name=" 443 + fn_name 444 + "; point=" 445 + point 446 + "; cls=" 447 + cls 448 + "; method=" 449 + method; 450 } 451 452 // ==================== PRODUCERS ==================== 453 454 /** 455 * Requires: this.isExitPoint() 456 * 457 * @return a name for the corresponding enter point 458 */ 459 public PptName makeEnter() { 460 // This associates throw points with the main entry point. 461 // We may wish to have a different exceptional than non-exceptional 462 // entry point; in particular, if there was an exception, then perhaps 463 // the precondition or object invariant was not met. 464 assert isExitPoint() : fullname; 465 466 assert isExitPoint() || isThrowsPoint(); 467 return new PptName(cls, method, FileIO.enter_suffix); 468 } 469 470 /** 471 * Requires: this.isExitPoint() || this.isEnterPoint() 472 * 473 * @return a name for the combined exit point 474 */ 475 public PptName makeExit() { 476 assert isExitPoint() || isEnterPoint() : fullname; 477 return new PptName(cls, method, FileIO.exit_suffix); 478 } 479 480 /** 481 * Requires: this.isExitPoint() || this.isEnterPoint() 482 * 483 * @return a name for the corresponding object invariant 484 */ 485 public PptName makeObject() { 486 assert isExitPoint() || isEnterPoint() : fullname; 487 return new PptName(cls, null, FileIO.object_suffix); 488 } 489 490 /** 491 * Requires: this.isExitPoint() || this.isEnterPoint() || this.isObjectInstanceSynthetic() 492 * 493 * @return a name for the corresponding class-static invariant 494 */ 495 public PptName makeClassStatic() { 496 assert isExitPoint() || isEnterPoint() || isObjectInstanceSynthetic() : fullname; 497 return new PptName(cls, null, FileIO.class_static_suffix); 498 } 499 500 // ==================== OBJECT METHODS ==================== 501 502 /* @return interned string such that this.equals(new PptName(this.toString())) */ 503 @SideEffectFree 504 @Override 505 public String toString(@GuardSatisfied PptName this) { 506 return fullname; 507 } 508 509 @EnsuresNonNullIf(result = true, expression = "#1") 510 @Pure 511 @Override 512 public boolean equals(@GuardSatisfied PptName this, @GuardSatisfied @Nullable Object o) { 513 return (o instanceof PptName) && equalsPptName((PptName) o); 514 } 515 516 @EnsuresNonNullIf(result = true, expression = "#1") 517 @Pure 518 public boolean equalsPptName(@GuardSatisfied PptName this, @GuardSatisfied PptName o) { 519 return (o != null) && (o.fullname == fullname); 520 } 521 522 @Pure 523 @Override 524 public int hashCode(@GuardSatisfied PptName this) { 525 return fullname.hashCode(); 526 } 527 528 // Interning is lost when an object is serialized and deserialized. 529 // Manually re-intern any interned fields upon deserialization. 530 private void readObject(ObjectInputStream in) throws IOException, ClassNotFoundException { 531 try { 532 in.defaultReadObject(); 533 if (fullname != null) { 534 fullname = fullname.intern(); 535 } 536 if (fn_name != null) { 537 fn_name = fn_name.intern(); 538 } 539 if (cls != null) { 540 cls = cls.intern(); 541 } 542 if (method != null) { 543 // method = method.intern(); 544 ReflectionPlume.setFinalField(this, "method", method.intern()); 545 } 546 if (point != null) { 547 point = point.intern(); 548 } 549 } catch (NoSuchFieldException e) { 550 throw new Error(e); 551 } 552 } 553}