Don't output top annotations to .ajava files

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

@@ -943,6 +943,12 @@ public void wpiPrepareClassForWriting(
       return;
     }
 
+    // fields
+    for (Map.Entry<String, FieldAnnos> fieldEntry : classAnnos.fields.entrySet()) {
+      fieldEntry.getValue().removePrimaryTopAnnotations();
+    }
+
+    // methods
     for (Map.Entry<String, CallableDeclarationAnnos> methodEntry :
         classAnnos.callableDeclarations.entrySet()) {
       String jvmSignature = methodEntry.getKey();
@@ -1069,9 +1075,9 @@ public void writeResultsToFile(OutputFormat outputFormat, BaseTypeChecker checke
   private void writeAjavaFile(File outputPath, CompilationUnitAnnos root) {
     try (Writer writer = new BufferedWriter(new FileWriter(outputPath))) {
 
-      // 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
+      // This one-line 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);
 
@@ -1784,6 +1790,21 @@ public void transferAnnotations() {
       }
     }
 
+    /** Removes the primary annotations in the signature that are the top in their hierarchy. */
+    public void removePrimaryTopAnnotations() {
+      if (returnType != null) {
+        returnType.removePrimaryTopAnnotations();
+      }
+      if (receiverType != null) {
+        receiverType.removePrimaryTopAnnotations();
+      }
+      if (parameterTypes != null) {
+        for (AnnotatedTypeMirror atm : parameterTypes) {
+          atm.removePrimaryTopAnnotations();
+        }
+      }
+    }
+
     @Override
     public String toString() {
       return "CallableDeclarationAnnos [declaration="
@@ -1944,6 +1965,13 @@ public void transferAnnotations() {
       declaration.setType(newType);
     }
 
+    /** Removes the top annotations from this. */
+    public void removePrimaryTopAnnotations() {
+      if (type != null) {
+        type.removePrimaryTopAnnotations();
+      }
+    }
+
     @Override
     public String toString() {
       return "FieldAnnos [declaration=" + declaration + ", type=" + type + "]";

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

@@ -1058,6 +1058,16 @@ public final QualifierHierarchy getQualifierHierarchy() {
     return qualHierarchy;
   }
 
+  /**
+   * Returns true if the given qualifer is one of the top annotations for the qualifer hierarchy.
+   *
+   * @param qualifier a type qualifier
+   * @return true if the given qualifer is one of the top annotations for the qualifer hierarchy
+   */
+  public final boolean isTop(AnnotationMirror qualifier) {
+    return qualHierarchy.isTop(qualifier);
+  }
+
   /**
    * Creates the type hierarchy to be used by this factory.
    *
@@ -5527,6 +5537,10 @@ public boolean wpiShouldInferTypesForReceivers() {
    * to an annotation file.
    *
    * @param methodAnnos the method or constructor annotations to modify
+   * @see #wpiPrepareMethodForWriting(
+   *     WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos,
+   *     Collection<WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos>,
+   *     Collection<WholeProgramInferenceJavaParserStorage.CallableDeclarationAnnos>)
    */
   public void wpiPrepareMethodForWriting(AMethod methodAnnos) {
     // This implementation does nothing.
@@ -5561,6 +5575,11 @@ public void wpiPrepareMethodForWriting(
       makeConditionConsistentWithOtherMethod(precondMap, inSubtype, true, false);
       makeConditionConsistentWithOtherMethod(postcondMap, inSubtype, false, false);
     }
+
+    // Remove top annotations on the method signature after the above runs.
+    // This side effect won't affect any future call to wpiPrepareMethodForWriting, because
+    // methodAnnos is a deep copy of the real inference storage data structure.
+    methodAnnos.removePrimaryTopAnnotations();
   }
 
   /**

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

@@ -769,7 +769,7 @@ public boolean removePrimaryAnnotationByClass(Class<? extends Annotation> a) {
    * Remove any primary annotation that is in the same qualifier hierarchy as the parameter.
    *
    * @param a an annotation from the same qualifier hierarchy
-   * @return if an annotation was removed
+   * @return true if an annotation was removed
    */
   public boolean removePrimaryAnnotationInHierarchy(AnnotationMirror a) {
     AnnotationMirror prev = this.getPrimaryAnnotationInHierarchy(a);
@@ -779,6 +779,17 @@ public boolean removePrimaryAnnotationInHierarchy(AnnotationMirror a) {
     return false;
   }
 
+  /**
+   * Remove any annotation that is the top annotation in its qualifier hierarchy.
+   *
+   * @return true if an annotation was removed
+   */
+  public boolean removePrimaryTopAnnotations() {
+    int oldSize = primaryAnnotations.size();
+    primaryAnnotations.removeIf(am -> atypeFactory.isTop(am));
+    return oldSize != primaryAnnotations.size();
+  }
+
   /**
    * Remove an annotation that is in the same qualifier hierarchy as the parameter, unless it's the
    * top annotation.

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

@@ -11,6 +11,7 @@
 import org.checkerframework.checker.nullness.qual.Nullable;
 import org.checkerframework.framework.qual.AnnotatedFor;
 import org.checkerframework.javacutil.AnnotationMirrorSet;
+import org.checkerframework.javacutil.AnnotationUtils;
 import org.checkerframework.javacutil.BugInCF;
 import org.plumelib.util.StringsPlume;
 
@@ -72,6 +73,16 @@ public int getWidth() {
    */
   public abstract AnnotationMirrorSet getTopAnnotations();
 
+  /**
+   * Returns true if the given qualifer is one of the top annotations for this qualifer hierarchy.
+   *
+   * @param qualifier any qualifier from one of the qualifier hierarchies represented by this
+   * @return true if the given qualifer is one of the top annotations for this qualifer hierarchy
+   */
+  public boolean isTop(AnnotationMirror qualifier) {
+    return AnnotationUtils.containsSame(getTopAnnotations(), qualifier);
+  }
+
   /**
    * Return the top qualifier for the given qualifier, that is, the qualifier that is a supertype of
    * {@code qualifier} but no further supertypes exist.