Derive each program point's type from its name

java/daikon/FileIO.java

@@ -376,7 +376,8 @@ public static void read_declaration_file(File filename, PptMap all_ppts) throws
     VarDefinition vardef = null;
     List<ParentRelation> ppt_parents = new ArrayList<>();
     EnumSet<PptFlags> ppt_flags = EnumSet.noneOf(PptFlags.class);
-    PptType ppt_type = PptType.POINT;
+    // Null if the declaration has no ppt-type record.
+    PptType ppt_type = null;
 
     try {
       // Read the records that define this program point
@@ -504,9 +505,12 @@ public static void read_declaration_file(File filename, PptMap all_ppts) throws
     }
 
     // Build the program point
-    PptTopLevel newppt = new PptTopLevel(ppt_name, ppt_type, ppt_parents, ppt_flags, vi_array);
-
-    return newppt;
+    try {
+      return new PptTopLevel(ppt_name, ppt_type, ppt_parents, ppt_flags, vi_array);
+    } catch (IllegalArgumentException e) {
+      decl_error(state, e);
+      throw new Error(); // this can't happen
+    }
   }
 
   /** Parses a ppt parent hierarchy record and returns it. */

java/daikon/PptConditional.java

@@ -29,6 +29,7 @@ public PptConditional(PptTopLevel parent, Splitter splitter, boolean splitter_in
     super(ctor_name_helper(parent, splitter, splitter_inverse), ctor_vis_helper(parent));
     // assert splitter.instantiated() == false;
     this.parent = parent;
+    this.type = parent.type;
     @SuppressWarnings({"nullness"}) // won't be used until it's fully initialized
     @Initialized PptConditional thisNonRaw = this;
     this.splitter = splitter.instantiateSplitter(thisNonRaw);

java/daikon/PptTopLevel.java

@@ -89,6 +89,7 @@
 import java.util.LinkedHashMap;
 import java.util.LinkedHashSet;
 import java.util.List;
+import java.util.Locale;
 import java.util.Map;
 import java.util.NoSuchElementException;
 import java.util.Set;
@@ -411,19 +412,19 @@ public boolean has_splitters() {
   @SuppressWarnings("fields.uninitialized") // todo: initialization and helper methods
   public PptTopLevel(
       String name,
-      PptType type,
+      @Nullable PptType type,
       List<ParentRelation> parents,
       EnumSet<PptFlags> flags,
       VarInfo[] var_infos) {
     super(var_infos);
 
     this.name = name;
     if (!name.contains(":::")) {
-      name += ":::" + type;
+      name += ":::" + (type == null ? PptType.POINT : type);
     }
     this.ppt_name = new PptName(name);
     this.flags = flags;
-    this.type = type;
+    this.type = normalize_type(ppt_name, type);
     this.parent_relations = parents;
     init_vars();
   }
@@ -433,13 +434,95 @@ private void readObject(ObjectInputStream in) throws IOException, ClassNotFoundE
     in.defaultReadObject();
   }
 
+  /**
+   * Returns the type that a program point with the given name and declared type should have.
+   *
+   * <p>A program point that has no declared type (as in a version 1 decls file, or a version 2
+   * decls file that omits the ppt-type record) gets its type from its name:
+   *
+   * <ul>
+   *   <li>foo:::ENTER is an {@link PptType#ENTER},
+   *   <li>a combined exit point, foo:::EXIT, is an {@link PptType#EXIT},
+   *   <li>a numbered exit point such as foo:::EXIT22 is a {@link PptType#SUBEXIT},
+   *   <li>Foo:::OBJECT is an {@link PptType#OBJECT},
+   *   <li>Foo:::CLASS is a {@link PptType#CLASS}, and
+   *   <li>any other program point is a generic {@link PptType#POINT}.
+   * </ul>
+   *
+   * <p>A program point that is declared with type {@link PptType#EXIT} or {@link PptType#SUBEXIT}
+   * is a combined exit or a numbered exit, according to its name. (Some front ends declare a
+   * numbered exit with type {@link PptType#EXIT}.)
+   *
+   * <p>A program point that is declared with any other type keeps that type. Its name must conform
+   * to the type, except for {@link PptType#POINT}, which permits any name.
+   *
+   * <p>As a result, the predicates is_enter, is_subexit, is_combined_exit, etc. agree with one
+   * another and with the program point's name.
+   *
+   * @param ppt_name the name of the program point
+   * @param type the declared type of the program point, or null if none was declared
+   * @return the type that the program point should have
+   * @throws IllegalArgumentException if the declared type does not conform to the name
+   */
+  private static PptType normalize_type(PptName ppt_name, @Nullable PptType type) {
+    if (type == null) {
+      if (ppt_name.isEnterPoint()) {
+        return PptType.ENTER;
+      } else if (ppt_name.isCombinedExitPoint()) {
+        return PptType.EXIT;
+      } else if (ppt_name.isNumberedExitPoint()) {
+        return PptType.SUBEXIT;
+      } else if (ppt_name.isObjectInstanceSynthetic()) {
+        return PptType.OBJECT;
+      } else if (ppt_name.isClassStaticSynthetic()) {
+        return PptType.CLASS;
+      } else {
+        return PptType.POINT;
+      }
+    }
+
+    boolean conforms;
+    switch (type) {
+      case POINT:
+        return type;
+      case ENTER:
+        conforms = ppt_name.isEnterPoint();
+        break;
+      case EXIT:
+      case SUBEXIT:
+        if (ppt_name.isCombinedExitPoint()) {
+          return PptType.EXIT;
+        } else if (ppt_name.isNumberedExitPoint()) {
+          return PptType.SUBEXIT;
+        }
+        conforms = false;
+        break;
+      case OBJECT:
+        conforms = ppt_name.isObjectInstanceSynthetic();
+        break;
+      case CLASS:
+        conforms = ppt_name.isClassStaticSynthetic();
+        break;
+      default:
+        throw new Error("Unexpected program point type " + type);
+    }
+    if (!conforms) {
+      throw new IllegalArgumentException(
+          String.format(
+              "Program point %s has type %s, but its name does not conform to that type",
+              ppt_name.getName(), type.toString().toLowerCase(Locale.ROOT)));
+    }
+    return type;
+  }
+
   // Used by DaikonSimple, InvMap, and tests.  Violates invariants.
   @SuppressWarnings(
       "nullness:fields.uninitialized") // violates invariants; also uses helper function
   public PptTopLevel(String name, VarInfo[] var_infos) {
     super(var_infos);
     this.name = name;
     ppt_name = new PptName(name);
+    type = normalize_type(ppt_name, null);
     init_vars();
   }
 
@@ -4646,11 +4729,7 @@ public void incSampleNumber() {
   /** Is this is an exit ppt (combined or specific)? */
   @Pure
   public boolean is_exit() {
-    if (type != null) {
-      return (type == PptType.EXIT) || (type == PptType.SUBEXIT);
-    } else {
-      return ppt_name.isExitPoint();
-    }
+    return (type == PptType.EXIT) || (type == PptType.SUBEXIT);
   }
 
   /**
@@ -4660,48 +4739,31 @@ public boolean is_exit() {
    */
   @Pure
   public boolean is_enter() {
-    if (type != null) {
-      return (type == PptType.ENTER);
-    } else {
-      return ppt_name.isEnterPoint();
-    }
+    return type == PptType.ENTER;
   }
 
   /** Is this a combined exit point? */
   @Pure
   public boolean is_combined_exit() {
-    if (type != null) {
-      return (type == PptType.EXIT);
-    } else {
-      return ppt_name.isCombinedExitPoint();
-    }
+    return type == PptType.EXIT;
   }
 
   /** Is this a numbered (specific) exit point? */
   @Pure
   public boolean is_subexit() {
-    if (type != null) {
-      return (type == PptType.SUBEXIT);
-    } else {
-      return ppt_name.isExitPoint() && !ppt_name.isCombinedExitPoint();
-    }
+    return type == PptType.SUBEXIT;
   }
 
   /** Is this a ppt that represents an object? */
   @Pure
   public boolean is_object() {
-    if (type != null) {
-      return (type == PptType.OBJECT);
-    } else {
-      return ppt_name.isObjectInstanceSynthetic();
-    }
+    return type == PptType.OBJECT;
   }
 
   /** Is this a ppt that represents a class? */
-  @EnsuresNonNullIf(result = true, expression = "type")
   @Pure
   public boolean is_class() {
-    return (type != null && type == PptType.CLASS);
+    return type == PptType.CLASS;
   }
 
   public String var_names() {

tests/daikon-tests/KnownValues/KnownValues.txt-daikon.goal

@@ -1,59 +1,59 @@
 ===========================================================================
-constantMinMaxDifferent:::EXIT1
+constantMinMaxDifferent:::EXIT
 return == 1
 ===========================================================================
-constantMinMaxMatch:::EXIT1
+constantMinMaxMatch:::EXIT
 ===========================================================================
-constantPairMinMaxMatch:::EXIT1
+constantPairMinMaxMatch:::EXIT
 ===========================================================================
-intOneOfNotSuppressed:::EXIT1
+intOneOfNotSuppressed:::EXIT
 a one of { 0, 1, 2 }
 ===========================================================================
-intOneOfSuppressed:::EXIT1
+intOneOfSuppressed:::EXIT
 ===========================================================================
-lowerBoundNotSuppressedStronger:::EXIT1
+lowerBoundNotSuppressedStronger:::EXIT
 a >= 1
 ===========================================================================
-lowerBoundNotSuppressedWeaker:::EXIT1
+lowerBoundNotSuppressedWeaker:::EXIT
 a >= 1
 ===========================================================================
-lowerBoundSuppressed:::EXIT1
+lowerBoundSuppressed:::EXIT
 ===========================================================================
-sequenceElementOneOfSuppressed:::EXIT1
+sequenceElementOneOfSuppressed:::EXIT
 size(a[]) == 7
 ===========================================================================
-sequenceIntOneOfNotSuppressed:::EXIT1
+sequenceIntOneOfNotSuppressed:::EXIT
 a[] == [0, 1, 0, 2]
 a[] elements one of { 0, 1, 2 }
 size(a[]) == 4
 ===========================================================================
-sequenceIntOneOfSuppressed:::EXIT1
+sequenceIntOneOfSuppressed:::EXIT
 a[] == [0, 1, 0]
 size(a[]) == 3
 ===========================================================================
-sequenceOneOfSuppressed:::EXIT1
+sequenceOneOfSuppressed:::EXIT
 ===========================================================================
-sequenceStringValidValuesNotSuppressed:::EXIT1
+sequenceStringValidValuesNotSuppressed:::EXIT
 a[] == [true, false, potato]
 a[] elements one of { "false", "potato", "true" }
 size(a[]) == 3
 ===========================================================================
-sequenceStringValidValuesSuppressed:::EXIT1
+sequenceStringValidValuesSuppressed:::EXIT
 a[] == [true, false]
 size(a[]) == 2
 ===========================================================================
-singletonSequenceOneOfSuppressed:::EXIT1
+singletonSequenceOneOfSuppressed:::EXIT
 a has only one value
 ===========================================================================
-stringValidValuesNotSuppressed:::EXIT1
+stringValidValuesNotSuppressed:::EXIT
 a one of { "false", "potato", "true" }
 a is printable
 ===========================================================================
-stringValidValuesSuppressed:::EXIT1
+stringValidValuesSuppressed:::EXIT
 a is printable
 ===========================================================================
-upperBoundSuppressed:::EXIT1
+upperBoundSuppressed:::EXIT
 ===========================================================================
-variableGreaterEqualSuppressed:::EXIT1
+variableGreaterEqualSuppressed:::EXIT
 ===========================================================================
-variableGreaterSuppressed:::EXIT1
+variableGreaterSuppressed:::EXIT

tests/daikon-tests/KnownValuesNewDecls/KnownValuesNewDecls.txt-daikon.goal

@@ -1,5 +1,5 @@
 ===========================================================================
-constantMinMaxMatch:::EXIT1
+constantMinMaxMatch:::EXIT
 ===========================================================================
-singletonSequenceOneOfSuppressed:::EXIT1
+singletonSequenceOneOfSuppressed:::EXIT
 a has only one value

tests/daikon-tests/NonZeroLargeRange/NonZeroLargeRange.txt-daikon.goal

@@ -3,7 +3,7 @@ NonZeroLargeRange.m(long):::ENTER
 x != 0
 x is a pointer
 ===========================================================================
-NonZeroLargeRange.m(long):::EXIT1
+NonZeroLargeRange.m(long):::EXIT
 x == orig(x)
 x != 0
 x is a pointer