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

Author: Chimaobi Emeka-Iheonu

docs/CHANGELOG.md

@@ -7,6 +7,9 @@
 
 ### User-visible changes
 
+Added support for IntelliJ IDEA external annotations (`annotations.xml`) via the
+`-AexternalAnnotations` command-line option.
+
 The `-AsuggestPureMethods` command-line option and the `purity.effectively.pure`
 warning no longer require `-AcheckPurityAnnotations` to also be supplied.
 

docs/manual/annotating-libraries.tex

@@ -1081,6 +1081,28 @@
 \end{Verbatim}
 
 
+\sectionAndLabel{External annotations (IntelliJ format)}{intellij-external-annotations}
+
+The Checker Framework can read external annotations stored in IntelliJ IDEA's \code{annotations.xml} format.
+This allows users to create external annotations using IntelliJ IDEA's user interface and supply them directly
+to the Checker Framework.
+
+\subsectionAndLabel{Using external annotations}{external-annotations-using}
+
+To supply external annotations to a checker, pass the \code{-AexternalAnnotations} command-line argument.
+It takes a colon-separated (on Unix) or semicolon-separated (on Windows) list of directories, JAR files, or ZIP files
+containing \code{annotations.xml} files arranged in directory structures matching their package names.
+
+For example:
+\begin{myxsmall}
+\begin{Verbatim}
+  javac -processor org.checkerframework.checker.nullness.NullnessChecker \
+    -AexternalAnnotations=path/to/annotations-dir:path/to/annotations.jar \
+    MyFile.java
+\end{Verbatim}
+\end{myxsmall}
+
+
 \sectionAndLabel{Troubleshooting/debugging annotated libraries}{libraries-troubleshooting}
 
 Sometimes, it may seem that a checker is treating a library as unannotated

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

@@ -271,6 +271,9 @@
   // Additional ajava files to use
   // org.checkerframework.framework.type.AnnotatedTypeFactory.parserAjavaFiles()
   "ajava",
+  // Additional external annotations (IntelliJ annotations.xml format)
+  // org.checkerframework.framework.stub.AnnotationFileElementTypes.parseExternalAnnotations()
+  "externalAnnotations",
   // Whether to print warnings about types/members in a stub file
   // that were not found on the class path
   // org.checkerframework.framework.stub.AnnotationFileParser.warnIfNotFound

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

@@ -202,6 +202,13 @@ public void parseStubFiles() {
           AnnotationFileType.COMMAND_LINE_STUB);
     }
 
+    // 6. External annotations provided via -AexternalAnnotations command-line option
+    String externalAnnotationsOption = checker.getOption("externalAnnotations");
+    if (externalAnnotationsOption != null) {
+      parseExternalAnnotations(
+          SystemUtil.pathSeparatorSplitter.splitToList(externalAnnotationsOption));
+    }
+
     parsing = false;
 
     if (stubDebug) {
@@ -288,6 +295,50 @@ public void parseAjavaFileWithTree(String ajavaPath, CompilationUnitTree root) {
     }
   }
 
+  /**
+   * Parses the external annotations files (IntelliJ annotations.xml format) at the given paths.
+   *
+   * @param externalAnnotationPaths list of files, directories, or jars/zips to parse
+   */
+  public void parseExternalAnnotations(List<String> externalAnnotationPaths) {
+    if (externalAnnotationPaths.isEmpty()) {
+      return;
+    }
+    SourceChecker checker = factory.getChecker();
+    ProcessingEnvironment processingEnv = factory.getProcessingEnv();
+    if (stubDebug) {
+      AnnotationFileParser.stubDebugStatic(
+          processingEnv, "AFET.parseExternalAnnotations(%s)", externalAnnotationPaths);
+    }
+    for (String path : externalAnnotationPaths) {
+      String base = System.getProperty("test.src");
+      String fullPath = (base == null) ? path : base + "/" + path;
+
+      List<AnnotationFileResource> allFiles =
+          AnnotationFileUtil.allAnnotationFiles(fullPath, AnnotationFileType.EXTERNAL_ANNOTATIONS);
+      if (allFiles != null) {
+        for (AnnotationFileResource resource : allFiles) {
+          try (InputStream annotationFileStream =
+              new BufferedInputStream(resource.getInputStream())) {
+            IntelliJAnnotationParser.parseAnnotationsXml(
+                resource.getDescription(),
+                annotationFileStream,
+                factory,
+                processingEnv,
+                annotationFileAnnos);
+          } catch (IOException e) {
+            checker.message(
+                Diagnostic.Kind.NOTE,
+                "Could not read external annotations resource: " + resource.getDescription());
+          }
+        }
+      } else {
+        checker.message(
+            Diagnostic.Kind.WARNING, "External annotations location not found: " + 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

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,
+    /** External annotations (IntelliJ annotations.xml format). */
+    EXTERNAL_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, EXTERNAL_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, EXTERNAL_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, EXTERNAL_ANNOTATIONS -> true;
         default -> throw new BugInCF("unhandled case " + this);
       };
     }
@@ -400,11 +402,14 @@ private static boolean isAnnotationFile(File f, AnnotationFileType fileType) {
    *     otherwise
    */
   private static boolean isAnnotationFile(String path, AnnotationFileType fileType) {
+    if (fileType == AnnotationFileType.EXTERNAL_ANNOTATIONS) {
+      return path.endsWith("annotations.xml") || path.endsWith(".xml");
+    }
     return path.endsWith(fileType.isStub() ? ".astub" : ".ajava");
   }
 
   private static boolean isJar(File f) {
-    return f.isFile() && f.getName().endsWith(".jar");
+    return f.isFile() && (f.getName().endsWith(".jar") || f.getName().endsWith(".zip"));
   }
 
   /**