Support IntelliJ IDEA external annotations (annotations.xml); fixes #6258

docs/CHANGELOG.md

@@ -7,12 +7,17 @@
 
 ### User-visible changes
 
+Added support for IntelliJ IDEA annotation files (`annotations.xml`) via the
+`-AintellijAnnotations` command-line option.
+
 ### Changes for type system implementers
 
 Renamed `AnnotatedTypes.innerMostType()` to `innermostComponentType()`.
 
 ### Closed issues
 
+(Filled in at release time.)
+
 ## Version 4.2.3 (2026-09-01)
 
 ### User-visible changes

docs/manual/annotating-libraries.tex

@@ -897,7 +897,11 @@
   By default, the Checker Framework warns about such problems in a stub
   file provided on the command line, but does not warn about built-in stub files.
   These command-line options turn the warnings on or off (respectively) for
-  all stub files. \\
+  all stub files.
+  An IntelliJ IDEA annotation file (Section~\ref{intellij-annotations}) is always
+  provided on the command line, so the Checker Framework warns about it by default;
+  \<-AstubNoWarnIfNotFound> turns those warnings off.
+  \\
   The \<@NoAnnotationFileParserWarning> annotation on a package or type in a stub file
   causes no warning to be issued for that package or type, regardless of
   the command-line options.
@@ -913,6 +917,8 @@
   to report only missing methods/fields, but ignore missing classes, even if
   other classes from the same package are present.
   Useful if a package spans more than one jar.
+  This also applies to IntelliJ IDEA annotation files
+  (Section~\ref{intellij-annotations}).
 
 \item[\<-AstubWarnIfRedundantWithBytecode>]
   Warn if a stub file entry is redundant with bytecode information.  The
@@ -1081,6 +1087,29 @@
 \end{Verbatim}
 
 
+\sectionAndLabel{External annotations in IntelliJ IDEA format}{intellij-annotations}
+
+The Checker Framework can read external annotations stored in IntelliJ
+IDEA's \code{annotations.xml} format.  This allows users to create
+\href{https://www.jetbrains.com/help/rider/Code_Analysis__External_Annotations.html}{external
+annotations}
+using
+\href{https://www.jetbrains.com/help/idea/annotating-source-code.html#external-annotations}{IntelliJ
+IDEA's user interface}.
+
+The \code{-AintellijAnnotations} command-line argument takes a
+path-separated list of \code{annotations.xml} files, directories, jar files, or zip files
+containing \code{annotations.xml} files arranged in directory structures matching their package names.
+The path separator is colon on Unix and semicolon on Windows.
+
+For example:
+\begin{Verbatim}
+  javac -processor org.checkerframework.checker.nullness.NullnessChecker \
+    -AintellijAnnotations=path/to/annotations-dir:path/to/annotations.jar \
+    MyFile.java
+\end{Verbatim}
+
+
 \sectionAndLabel{Troubleshooting/debugging annotated libraries}{libraries-troubleshooting}
 
 Sometimes, it may seem that a checker is treating a library as unannotated

docs/manual/contributors.tex

@@ -25,6 +25,7 @@
 Calvin Loncaric,
 Charles Chen,
 Charlie Garrett,
+Chimaobi Emeka-Iheonu,
 Chris Povirk,
 Chris Toxiadis,
 Christopher Mackie,

docs/manual/introduction.tex

@@ -748,6 +748,10 @@
 \item \<-Astubs>
   List of stub files or directories; see Section~\ref{stub-using}.
 
+\item \<-AintellijAnnotations>
+  List of IntelliJ IDEA annotation files, directories, jar files, or zip files;
+  see Section~\ref{intellij-annotations}.
+
 \item
   \<-AstubWarnIfNotFound>,
   \<-AstubNoWarnIfNotFound>,

framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java

@@ -271,8 +271,11 @@
   // Additional ajava files to use
   // org.checkerframework.framework.type.AnnotatedTypeFactory.parserAjavaFiles()
   "ajava",
-  // Whether to print warnings about types/members in a stub file
-  // that were not found on the class path
+  // Annotations in IntelliJ annotations.xml format
+  // org.checkerframework.framework.stub.AnnotationFileElementTypes.parseIntellijAnnotations()
+  "intellijAnnotations",
+  // Whether to print warnings about types/members in a stub file (or IntelliJ
+  // IDEA annotation file) that were not found on the classpath.
   // org.checkerframework.framework.stub.AnnotationFileParser.warnIfNotFound
   "stubWarnIfNotFound",
   "stubNoWarnIfNotFound",

framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileElementTypes.java

@@ -144,6 +144,8 @@ public boolean isParsing() {
    *   <li>Stub files returned by {@link BaseTypeChecker#getExtraStubFiles} (treated like those
    *       listed in @StubFiles annotation)
    *   <li>Stub files provided via {@code -Astubs} compiler option
+   *   <li>IntelliJ IDEA external annotations provided via {@code -AintellijAnnotations} compiler
+   *       option
    * </ol>
    *
    * <p>If a type is annotated with a qualifier from the same hierarchy in more than one stub file,
@@ -202,6 +204,13 @@ public void parseStubFiles() {
           AnnotationFileType.COMMAND_LINE_STUB);
     }
 
+    // 6. Annotations provided via -AintellijAnnotations command-line option
+    String intellijAnnotationsOption = checker.getOption("intellijAnnotations");
+    if (intellijAnnotationsOption != null) {
+      parseIntellijAnnotations(
+          SystemUtil.pathSeparatorSplitter.splitToList(intellijAnnotationsOption));
+    }
+
     parsing = false;
 
     if (stubDebug) {
@@ -288,6 +297,80 @@ public void parseAjavaFileWithTree(String ajavaPath, CompilationUnitTree root) {
     }
   }
 
+  /**
+   * Parses IntelliJ annotation files.
+   *
+   * @param intellijAnnotationPaths list of files, directories, or jars/zips to parse
+   */
+  public void parseIntellijAnnotations(List<String> intellijAnnotationPaths) {
+    if (intellijAnnotationPaths.isEmpty()) {
+      return;
+    }
+    boolean wasParsing = parsing;
+    parsing = true;
+    try {
+      ProcessingEnvironment processingEnv = factory.getProcessingEnv();
+      if (stubDebug) {
+        AnnotationFileParser.stubDebugStatic(
+            processingEnv, "AFET.parseIntellijAnnotations(%s)", intellijAnnotationPaths);
+      }
+      SourceChecker checker = factory.getChecker();
+      for (String path : intellijAnnotationPaths) {
+        String fullPath = resolveAgainstTestSrc(path);
+
+        List<AnnotationFileResource> allFiles =
+            AnnotationFileUtil.allAnnotationFiles(
+                fullPath, AnnotationFileType.INTELLIJ_ANNOTATIONS);
+        if (allFiles == null) {
+          checker.message(
+              Diagnostic.Kind.ERROR, "IntelliJ IDEA annotations file not found: " + path);
+        } else if (allFiles.isEmpty()) {
+          // The path exists but contains no annotations.xml file, so the user gets no
+          // annotations from it.  That is most likely a mistake, so warn rather than issuing a
+          // note, which javac does not display by default.
+          checker.message(Diagnostic.Kind.WARNING, "No annotations.xml file found within " + path);
+        } else {
+          for (AnnotationFileResource resource : allFiles) {
+            // Closing the stream is safe even for a jar file entry:  it does not close the
+            // JarFile that other entries in `allFiles` share.
+            try (BufferedInputStream annotationFileStream =
+                new BufferedInputStream(resource.getInputStream())) {
+              IntelliJAnnotationParser.parseAnnotationsXml(
+                  resource.getDescription(),
+                  annotationFileStream,
+                  factory,
+                  processingEnv,
+                  annotationFileAnnos);
+            } catch (IOException e) {
+              checker.message(
+                  Diagnostic.Kind.ERROR,
+                  "Could not read IntelliJ IDEA annotations: " + resource.getDescription());
+            }
+          }
+        }
+      }
+    } finally {
+      parsing = wasParsing;
+    }
+  }
+
+  /**
+   * Returns the path to use for an annotation file that was named on the command line. This is a
+   * special case when running in jtreg, which runs the compiler in a different directory than the
+   * one that contains the test's annotation files.
+   *
+   * @param path a relative or absolute path, from a command-line argument
+   * @return {@code path}, resolved against the {@code test.src} system property if that property is
+   *     set and {@code path} is relative
+   */
+  private static String resolveAgainstTestSrc(String path) {
+    String base = System.getProperty("test.src");
+    if (base == null || Paths.get(path).isAbsolute()) {
+      return path;
+    }
+    return base + "/" + path;
+  }
+
   /**
    * Parses the files in {@code annotationFiles} of the given file type. This includes files listed
    * directly in {@code annotationFiles} and for each listed directory, also includes all files
@@ -315,9 +398,7 @@ private void parseAnnotationFiles(List<String> annotationFiles, AnnotationFileTy
           processingEnv, "AFET.parseAnnotationFiles(%s, %s)", annotationFiles, fileType);
     }
     for (String path : annotationFiles) {
-      // Special case when running in jtreg.
-      String base = System.getProperty("test.src");
-      String fullPath = (base == null) ? path : base + "/" + path;
+      String fullPath = resolveAgainstTestSrc(path);
 
       List<AnnotationFileResource> allFiles =
           AnnotationFileUtil.allAnnotationFiles(fullPath, fileType);

framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileUtil.java

@@ -60,7 +60,9 @@ public enum AnnotationFileType {
     /** Ajava file being parsed as if it is a stub file. */
     AJAVA_AS_STUB,
     /** Ajava file provided on command line. */
-    AJAVA;
+    AJAVA,
+    /** IntelliJ annotations. */
+    INTELLIJ_ANNOTATIONS;
 
     /**
      * Returns true if this represents a stub file.
@@ -70,7 +72,7 @@ public enum AnnotationFileType {
     public boolean isStub() {
       return switch (this) {
         case JDK_STUB, BUILTIN_STUB, COMMAND_LINE_STUB, AJAVA_AS_STUB -> true;
-        case AJAVA -> false;
+        case AJAVA, INTELLIJ_ANNOTATIONS -> false;
         default -> throw new BugInCF("unhandled case " + this);
       };
     }
@@ -83,7 +85,7 @@ public boolean isStub() {
     public boolean isBuiltIn() {
       return switch (this) {
         case JDK_STUB, BUILTIN_STUB -> true;
-        case COMMAND_LINE_STUB, AJAVA_AS_STUB, AJAVA -> false;
+        case COMMAND_LINE_STUB, AJAVA_AS_STUB, AJAVA, INTELLIJ_ANNOTATIONS -> false;
         default -> throw new BugInCF("unhandled case " + this);
       };
     }
@@ -96,7 +98,7 @@ public boolean isBuiltIn() {
     public boolean isCommandLine() {
       return switch (this) {
         case JDK_STUB, BUILTIN_STUB -> false;
-        case COMMAND_LINE_STUB, AJAVA_AS_STUB, AJAVA -> true;
+        case COMMAND_LINE_STUB, AJAVA_AS_STUB, AJAVA, INTELLIJ_ANNOTATIONS -> true;
         default -> throw new BugInCF("unhandled case " + this);
       };
     }
@@ -352,8 +354,11 @@ public void visit(WildcardType n, Void arg) {
   /**
    * Returns annotation files found at a given file system location (does not look on classpath).
    *
-   * @param location an annotation file (stub file or ajava file), a jarfile, or a directory. Look
-   *     for it as an absolute file and relative to the current directory.
+   * @param location an annotation file (a stub file, ajava file, or IntelliJ IDEA annotation file),
+   *     a jarfile, or a directory. Look for it as an absolute file and relative to the current
+   *     directory. Because it is named explicitly, a file is used no matter what its name is;
+   *     within a jarfile or directory, only files whose name indicates that they are of type {@code
+   *     fileType} are used.
    * @param fileType file type of files to collect
    * @return annotation files with the given file type found in the file system (does not look on
    *     classpath). Returns null if the file system location does not exist; the caller may wish to
@@ -364,7 +369,7 @@ public void visit(WildcardType n, Void arg) {
     File file = new File(location);
     if (file.exists()) {
       List<AnnotationFileResource> resources = new ArrayList<>();
-      addAnnotationFilesToList(file, resources, fileType);
+      addAnnotationFilesToList(file, resources, fileType, true);
       return resources;
     }
 
@@ -373,7 +378,7 @@ public void visit(WildcardType n, Void arg) {
     file = new File(System.getProperty("user.dir"), location);
     if (file.exists()) {
       List<AnnotationFileResource> resources = new ArrayList<>();
-      addAnnotationFilesToList(file, resources, fileType);
+      addAnnotationFilesToList(file, resources, fileType, true);
       return resources;
     }
 
@@ -400,39 +405,55 @@ private static boolean isAnnotationFile(File f, AnnotationFileType fileType) {
    *     otherwise
    */
   private static boolean isAnnotationFile(String path, AnnotationFileType fileType) {
+    if (fileType == AnnotationFileType.INTELLIJ_ANNOTATIONS) {
+      // Within a directory or an archive, an IntelliJ IDEA annotation file is always named
+      // "annotations.xml".  (A file named on the command line may have any name; see
+      // addAnnotationFilesToList.)
+      return "annotations.xml".equals(new File(path).getName());
+    }
     return path.endsWith(fileType.isStub() ? ".astub" : ".ajava");
   }
 
-  private static boolean isJar(File f) {
-    return f.isFile() && f.getName().endsWith(".jar");
+  /**
+   * Returns true if {@code f} is a JAR or ZIP archive file.
+   *
+   * @param f the file to check
+   * @return true if {@code f} is a JAR or ZIP file
+   */
+  private static boolean isJarOrZip(File f) {
+    return f.isFile() && (f.getName().endsWith(".jar") || f.getName().endsWith(".zip"));
   }
 
   /**
    * Side-effects {@code resources} by adding annotation files of the given file type to it.
    *
-   * @param location an annotation file (a stub file or ajava file), a jarfile, or a directory. If a
-   *     stub file or ajava file, add it to the {@code resources} list. If a jarfile, use all
-   *     annotation files (of type {@code fileType}) contained in it. If a directory, recurse on all
-   *     files contained in it.
+   * @param location an annotation file (a stub file, ajava file, or IntelliJ IDEA annotation file),
+   *     a jarfile, or a directory. If an annotation file, add it to the {@code resources} list. If
+   *     a jarfile, use all annotation files (of type {@code fileType}) contained in it. If a
+   *     directory, recurse on all files contained in it.
    * @param resources the list to add the found files to
    * @param fileType type of annotation files to add
+   * @param isUserSupplied true if {@code location} was named by the user (say, on the command line)
+   *     rather than being found by searching a directory or an archive. A file named by the user is
+   *     used no matter what its name is; a file found by searching is used only if its name
+   *     indicates that it is an annotation file of type {@code fileType}.
    */
   @SuppressWarnings({
     "JdkObsolete", // JarFile.entries()
-    "nullness:argument", // inference failed in Arrays.sort
     "builder:required.method.not.called" // ownership passed to list of
     // JarEntryAnnotationFileResource, where `file` appears in every element of the list
   })
   private static void addAnnotationFilesToList(
-      File location, List<AnnotationFileResource> resources, AnnotationFileType fileType) {
-    if (isAnnotationFile(location, fileType)) {
-      resources.add(new FileAnnotationFileResource(location));
-    } else if (isJar(location)) {
+      File location,
+      List<AnnotationFileResource> resources,
+      AnnotationFileType fileType,
+      boolean isUserSupplied) {
+    if (isJarOrZip(location)) {
       JarFile file;
       try {
         file = new JarFile(location);
       } catch (IOException e) {
-        System.err.println("AnnotationFileUtil: could not process JAR file: " + location);
+        System.err.println("AnnotationFileUtil: could not process archive: " + location);
         return;
       }
       Enumeration<JarEntry> entries = file.entries();
@@ -445,10 +466,16 @@ private static void addAnnotationFilesToList(
 
     } else if (location.isDirectory()) {
       File[] directoryContents = location.listFiles();
+      if (directoryContents == null) {
+        System.err.println("AnnotationFileUtil: could not list directory: " + location);
+        return;
+      }
       Arrays.sort(directoryContents, Comparator.comparing(File::getName));
       for (File enclosed : directoryContents) {
-        addAnnotationFilesToList(enclosed, resources, fileType);
+        addAnnotationFilesToList(enclosed, resources, fileType, false);
       }
+    } else if ((isUserSupplied && location.isFile()) || isAnnotationFile(location, fileType)) {
+      resources.add(new FileAnnotationFileResource(location));
     }
   }