Don't write irrelevant annotations in .ajava files

checker/tests/ainfer-index/non-annotated/DependentTypesViewpointAdaptationTest.java

@@ -59,13 +59,11 @@ public static void testThisInference(
 
   public void compute5(
       DependentTypesViewpointAdaptationTest this, DependentTypesViewpointAdaptationTest other) {
-    // :: warning: (assignment)
-    @SameLen("this") DependentTypesViewpointAdaptationTest myOther = other;
+    DependentTypesViewpointAdaptationTest myOther = other;
   }
 
   // Same as compute5, but without an explicit this parameter.
   public void compute6(DependentTypesViewpointAdaptationTest other) {
-    // :: warning: (assignment)
-    @SameLen("this") DependentTypesViewpointAdaptationTest myOther = other;
+    DependentTypesViewpointAdaptationTest myOther = other;
   }
 }

docs/manual/inference.tex

@@ -135,7 +135,7 @@
 A typical invocation of \<wpi.sh> is
 
 \begin{Verbatim}
-  wpi.sh -- --checker nullness
+  $CHECKERFRAMEWORK/bin/wpi.sh -- --checker nullness
 \end{Verbatim}
 
 The result is a set of log files placed in the \<dljc-out/> folder of the

framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java

@@ -23,9 +23,15 @@
 import com.github.javaparser.ast.expr.NormalAnnotationExpr;
 import com.github.javaparser.ast.expr.ObjectCreationExpr;
 import com.github.javaparser.ast.expr.SingleMemberAnnotationExpr;
+import com.github.javaparser.ast.type.ArrayType;
 import com.github.javaparser.ast.type.ClassOrInterfaceType;
+import com.github.javaparser.ast.type.IntersectionType;
+import com.github.javaparser.ast.type.PrimitiveType;
 import com.github.javaparser.ast.type.Type;
 import com.github.javaparser.ast.type.TypeParameter;
+import com.github.javaparser.ast.type.UnionType;
+import com.github.javaparser.ast.type.VarType;
+import com.github.javaparser.ast.type.WildcardType;
 import com.github.javaparser.ast.visitor.CloneVisitor;
 import com.github.javaparser.ast.visitor.VoidVisitor;
 import com.github.javaparser.printer.DefaultPrettyPrinter;
@@ -1062,6 +1068,65 @@ public void writeResultsToFile(OutputFormat outputFormat, BaseTypeChecker checke
     modifiedFiles.clear();
   }
 
+  /**
+   * Returns true if the annotation is relevant (where it appears in the program). This
+   * implementation is conservative and only returns false if the qualifier is definitely not
+   * relevant.
+   *
+   * @param anno an annotation
+   * @return true if the annotation might be relevant
+   */
+  boolean annotationIsRelevant(AnnotationExpr anno) {
+    GenericAnnotatedTypeFactory<?, ?, ?, ?> gatf = (GenericAnnotatedTypeFactory) atypeFactory;
+    if (gatf.relevantJavaTypes == null) {
+      return true;
+    }
+
+    // `aname` is a fully-qualified name.
+    String aName = anno.getNameAsString();
+    if (!atypeFactory.isSupportedQualifier(aName)) {
+      // The annotation might be a declaration qualifier, such as a side effect specification.
+      return true;
+    }
+    Node parentNode = anno.getParentNode().get();
+
+    if (parentNode instanceof ArrayType) {
+      return gatf.arraysAreRelevant();
+    }
+    if (parentNode instanceof ClassOrInterfaceType) {
+      ClassOrInterfaceType classType = (ClassOrInterfaceType) parentNode;
+      String simpleName = classType.getName().toString();
+      String scopedName = classType.getNameWithScope();
+      // TODO: Do I need to remove type parameters?
+      return gatf.isRelevant(simpleName) || gatf.isRelevant(scopedName);
+    }
+    if (parentNode instanceof IntersectionType) {
+      return true; // TODO
+    }
+    if (parentNode instanceof Parameter) {
+      Parameter param = (Parameter) parentNode;
+      if (param.isVarArgs()) {
+        return gatf.arraysAreRelevant();
+      } else {
+        throw new Error("Unexpected type annotation on non-varargs Parameter: " + param);
+      }
+    }
+    if (parentNode instanceof PrimitiveType) {
+      return gatf.isRelevant(parentNode.toString());
+    }
+    if (parentNode instanceof UnionType) {
+      return true; // TODO
+    }
+    if (parentNode instanceof VarType) {
+      return gatf.nonprimitivesAreRelevant();
+    }
+    if (parentNode instanceof WildcardType) {
+      return true; // TODO
+    }
+
+    throw new Error("What parent? " + parentNode.getClass().getSimpleName() + " " + parentNode);
+  }
+
   /**
    * Write an ajava file to disk.
    *
@@ -1071,14 +1136,15 @@ public void writeResultsToFile(OutputFormat outputFormat, BaseTypeChecker checke
   private void writeAjavaFile(File outputPath, CompilationUnitAnnos root) {
     try (Writer writer = new BufferedWriter(new FileWriter(outputPath))) {
 
-      // JavaParser can output using lexical preserving printing, which writes the file such
-      // that its formatting is close to the original source file it was parsed from as
-      // possible. Currently, this feature is very buggy and crashes when adding annotations
-      // in certain locations. This implementation could be used instead if it's fixed in
-      // JavaParser.
+      // This implementation uses JavaParser's lexical preserving printing, which writes the file
+      // such that its formatting is close to the original source file it was parsed from as
+      // possible. It is commented out because, this feature is very buggy and crashes when adding
+      // annotations in certain locations.
       // LexicalPreservingPrinter.print(root.declaration, writer);
 
-      // Do not print invisible qualifiers, to avoid cluttering the output.
+      // To avoid cluttering the output, do not print:
+      //  * invisible qualifiers
+      //  * irrelevant qualifiers.
       Set<String> invisibleQualifierNames = getInvisibleQualifierNames(this.atypeFactory);
       DefaultPrettyPrinter prettyPrinter =
           new DefaultPrettyPrinter() {
@@ -1091,6 +1157,9 @@ public void visit(MarkerAnnotationExpr n, Void arg) {
                       if (invisibleQualifierNames.contains(n.getName().toString())) {
                         return;
                       }
+                      if (!annotationIsRelevant(n)) {
+                        return;
+                      }
                       super.visit(n, arg);
                     }
 
@@ -1099,6 +1168,9 @@ public void visit(SingleMemberAnnotationExpr n, Void arg) {
                       if (invisibleQualifierNames.contains(n.getName().toString())) {
                         return;
                       }
+                      if (!annotationIsRelevant(n)) {
+                        return;
+                      }
                       super.visit(n, arg);
                     }
 
@@ -1107,6 +1179,9 @@ public void visit(NormalAnnotationExpr n, Void arg) {
                       if (invisibleQualifierNames.contains(n.getName().toString())) {
                         return;
                       }
+                      if (!annotationIsRelevant(n)) {
+                        return;
+                      }
                       super.visit(n, arg);
                     }
                   };

framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java

@@ -187,15 +187,25 @@ public abstract class GenericAnnotatedTypeFactory<
    * <p>Although a {@code Class<?>} object exists for every element, this does not contain those
    * {@code Class<?>} objects because the elements will be compared to TypeMirrors for which Class
    * objects may not exist (they might not be on the classpath).
+   *
+   * <p>For their names, see {@link #relevantJavaTypeNames}.
    */
   public final @Nullable Set<TypeMirror> relevantJavaTypes;
 
   /**
-   * Whether users may write type annotations on arrays. Ignored unless {@link #relevantJavaTypes}
-   * is non-null.
+   * The fully-qualified names <b>and</b> simple names of the types in {@link #relevantJavaTypes}.
    */
+  public final @Nullable Set<String> relevantJavaTypeNames;
+
+  /** Whether users may write type annotations on arrays. */
   protected final boolean arraysAreRelevant;
 
+  /**
+   * Whether users may write type annotations on non-primitives (classes, arrays, etc.). This is
+   * redundant with the value of {@link #relevantJavaTypes} but is included for efficiency.
+   */
+  protected final boolean nonprimitivesAreRelevant;
+
   // Flow related fields
 
   /** Should flow be used by default? */
@@ -358,26 +368,49 @@ protected GenericAnnotatedTypeFactory(BaseTypeChecker checker, boolean useFlow)
         checker.getClass().getAnnotation(RelevantJavaTypes.class);
     if (relevantJavaTypesAnno == null) {
       this.relevantJavaTypes = null;
+      this.relevantJavaTypeNames = null;
       this.arraysAreRelevant = true;
+      this.nonprimitivesAreRelevant = true;
     } else {
       Types types = getChecker().getTypeUtils();
       Elements elements = getElementUtils();
       Class<?>[] classes = relevantJavaTypesAnno.value();
-      this.relevantJavaTypes = new HashSet<>(CollectionsPlume.mapCapacity(classes.length));
+      Set<TypeMirror> relevantJavaTypesTemp =
+          new HashSet<>(CollectionsPlume.mapCapacity(classes.length));
+      Set<String> relevantJavaTypeNamesTemp =
+          new HashSet<>(CollectionsPlume.mapCapacity(classes.length));
       boolean arraysAreRelevantTemp = false;
+      boolean nonprimitivesAreRelevantTemp = false;
       for (Class<?> clazz : classes) {
         if (clazz == Object[].class) {
           arraysAreRelevantTemp = true;
+          nonprimitivesAreRelevantTemp = true;
         } else if (clazz.isArray()) {
           throw new TypeSystemError(
               "Don't use arrays other than Object[] in @RelevantJavaTypes on "
                   + this.getClass().getSimpleName());
         } else {
           TypeMirror relevantType = TypesUtils.typeFromClass(clazz, types, elements);
-          relevantJavaTypes.add(types.erasure(relevantType));
+          TypeMirror erased = types.erasure(relevantType);
+          relevantJavaTypesTemp.add(erased);
+          String typeString = erased.toString();
+          relevantJavaTypeNamesTemp.add(typeString);
+          if (clazz.isPrimitive()) {
+            nonprimitivesAreRelevantTemp = true;
+          } else {
+            int dotIndex = typeString.lastIndexOf('.');
+            if (dotIndex != -1) {
+              // It's a fully-qualified name.  Add the simple name as well.
+              // TODO: This might not handle a user writing a nested class like "Map.Entry".
+              relevantJavaTypeNamesTemp.add(typeString.substring(dotIndex + 1));
+            }
+          }
         }
       }
+      this.relevantJavaTypes = Collections.unmodifiableSet(relevantJavaTypesTemp);
+      this.relevantJavaTypeNames = Collections.unmodifiableSet(relevantJavaTypeNamesTemp);
       this.arraysAreRelevant = arraysAreRelevantTemp;
+      this.nonprimitivesAreRelevant = nonprimitivesAreRelevantTemp;
     }
 
     contractsUtils = createContractsFromMethod();
@@ -2393,8 +2426,9 @@ private static void log(String format, Object... args) {
    * Returns true if users can write type annotations from this type system directly on the given
    * Java type.
    *
-   * <p>May return false for a compound type (for which it is possible to write type qualifiers on
-   * elements of the type).
+   * <p>For a compound type, returns true only if a programmer may write a type qualifier on the top
+   * level of the compound type. That is, this method may return false, when it is possible to write
+   * type qualifiers on elements of the type.
    *
    * <p>Subclasses should override {@code #isRelevantImpl} instead of this method.
    *
@@ -2403,12 +2437,15 @@ private static void log(String format, Object... args) {
    *     Java type
    */
   public final boolean isRelevant(TypeMirror tm) {
+    if (relevantJavaTypes == null) {
+      return true;
+    }
     if (tm.getKind() != TypeKind.PACKAGE && tm.getKind() != TypeKind.MODULE) {
       tm = types.erasure(tm);
     }
-    Boolean cachedResult = isRelevantCache.get(tm);
-    if (cachedResult != null) {
-      return cachedResult;
+    Boolean resultBoxed = isRelevantCache.get(tm);
+    if (resultBoxed != null) {
+      return resultBoxed;
     }
     boolean result = isRelevantImpl(tm);
     isRelevantCache.put(tm, result);
@@ -2419,8 +2456,9 @@ public final boolean isRelevant(TypeMirror tm) {
    * Returns true if users can write type annotations from this type system directly on the given
    * Java type.
    *
-   * <p>May return false for a compound type (for which it is possible to write type qualifiers on
-   * elements of the type).
+   * <p>For a compound type, returns true only if it a programmer may write a type qualifier on the
+   * top level of the compound type. That is, this method may return false, when it is possible to
+   * write type qualifiers on elements of the type.
    *
    * <p>Subclasses should override {@code #isRelevantImpl} instead of this method.
    *
@@ -2439,12 +2477,19 @@ public final boolean isRelevant(AnnotatedTypeMirror tm) {
    * <p>Clients should never call this. Call {@link #isRelevant} instead. This is a helper method
    * for {@link #isRelevant}.
    *
+   * <p>This should <b>not</b> be called if {@code relevantJavaTypes == null ||
+   * relevantJavaTypes.contains(tm))}.
+   *
    * @param tm a type
    * @return true if users can write type annotations from this type system on the given Java type
    */
   protected boolean isRelevantImpl(TypeMirror tm) {
 
-    if (relevantJavaTypes == null || relevantJavaTypes.contains(tm)) {
+    if (relevantJavaTypes == null) {
+      return true;
+    }
+
+    if (relevantJavaTypes.contains(tm)) {
       return true;
     }
 
@@ -2524,6 +2569,43 @@ protected boolean isRelevantImpl(TypeMirror tm) {
     }
   }
 
+  /**
+   * Returns true if users can write type annotations from this type system directly on the given
+   * Java type.
+   *
+   * <p>For a compound type, returns true only if it is permitted to write a type qualifier on the
+   * top level of the compound type. That is, this method may return false, when it is possible to
+   * write type qualifiers on elements of the type.
+   *
+   * <p>Subclasses should override {@code #isRelevantImpl} instead of this method.
+   *
+   * @param type a fully-qualified or simple type; should not be an array (use {@link
+   *     #arraysAreRelevant} instead)
+   * @return true if users can write type annotations from this type system directly on the given
+   *     Java type
+   */
+  public final boolean isRelevant(String type) {
+    return relevantJavaTypeNames == null || relevantJavaTypeNames.contains(type);
+  }
+
+  /**
+   * Returns true if users can write type annotations from this type system on array types.
+   *
+   * @return true if users can write type annotations from this type system on array types
+   */
+  public final boolean arraysAreRelevant() {
+    return arraysAreRelevant;
+  }
+
+  /**
+   * Returns true if users can write type annotations from this type system on non-primitive types.
+   *
+   * @return true if users can write type annotations from this type system on non-primitive types
+   */
+  public final boolean nonprimitivesAreRelevant() {
+    return nonprimitivesAreRelevant;
+  }
+
   /** The cached message about relevant types. */
   private @MonotonicNonNull String irrelevantExtraMessage = null;
 

framework/src/main/java/org/checkerframework/framework/type/QualifierHierarchy.java

@@ -43,9 +43,9 @@ public QualifierHierarchy(GenericAnnotatedTypeFactory<?, ?, ?, ?> atypeFactory)
   }
 
   /**
-   * Determine whether this is valid.
+   * Determine whether this QualifierHierarchy is valid.
    *
-   * @return true if this is valid
+   * @return true if this QualifierHierarchy is valid
    */
   public boolean isValid() {
     return true;

javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java

@@ -171,10 +171,10 @@ public static Class<?> getClassFromType(TypeMirror typeMirror) {
   }
 
   /**
-   * Returns the simple type name, without annotations.
+   * Returns the simple type name, without annotations but including array brackets.
    *
    * @param type a type
-   * @return the simple type name, without annotations
+   * @return the simple type name
    */
   public static String simpleTypeName(TypeMirror type) {
     switch (type.getKind()) {
@@ -218,10 +218,10 @@ public static String simpleTypeName(TypeMirror type) {
   }
 
   /**
-   * Returns the binary name.
+   * Returns the binary name of a type.
    *
    * @param type a type
-   * @return the binary name
+   * @return its binary name
    */
   public static @BinaryName String binaryName(TypeMirror type) {
     if (type.getKind() != TypeKind.DECLARED) {