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}