From 866e1c2ddaff4a40187080093d27a6db892ecadd Mon Sep 17 00:00:00 2001 From: Yutong Zhu Date: Mon, 6 Oct 2025 17:33:57 -0400 Subject: [PATCH 1/6] Initial POC for JDK Annotation decoupling --- TestAnnotatedJdk.java | 10 +++++ framework/build.gradle | 9 ++++ .../stub/AnnotationFileElementTypes.java | 43 ++++++++++++++++++- 3 files changed, 61 insertions(+), 1 deletion(-) create mode 100644 TestAnnotatedJdk.java diff --git a/TestAnnotatedJdk.java b/TestAnnotatedJdk.java new file mode 100644 index 000000000000..f2a3949d5fc3 --- /dev/null +++ b/TestAnnotatedJdk.java @@ -0,0 +1,10 @@ +import java.util.List; +import java.util.ArrayList; + +public class TestAnnotatedJdk { + public static void main(String[] args) { + List list = new ArrayList<>(); + list.add("hello"); + list.add(null); // Should emit error with annotated JDK + } +} \ No newline at end of file diff --git a/framework/build.gradle b/framework/build.gradle index 9de168f9bb19..25ba7e05278a 100644 --- a/framework/build.gradle +++ b/framework/build.gradle @@ -148,6 +148,15 @@ task copyAndMinimizeAnnotatedJdkFiles(type: JavaExec, dependsOn: cloneAnnotatedJ sourcesJar.dependsOn(copyAndMinimizeAnnotatedJdkFiles) processResources.dependsOn(copyAndMinimizeAnnotatedJdkFiles) +task annotatedJdkJar(type: Jar, group: 'Build') { + description = 'Creates a separate JAR file containing only the annotated JDK stub files' + dependsOn(copyAndMinimizeAnnotatedJdkFiles) + destinationDirectory = file("/Users/yutongzhu/dev/URA/checker-framework/checker/dist") + archiveFileName = 'annotated-jdk.jar' + from "${buildDir}/generated/resources" + include 'annotated-jdk/**' +} + task allSourcesJar(type: Jar, group: 'Build') { description = 'Creates a sources jar that includes sources for all Checker Framework classes in framework.jar' destinationDirectory = file("${projectDir}/dist") diff --git a/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileElementTypes.java b/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileElementTypes.java index ebd0c8912375..34219d2b799f 100644 --- a/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileElementTypes.java +++ b/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileElementTypes.java @@ -863,7 +863,48 @@ private void parseJdkJarEntry(String jarEntryName) { * @return a JarURLConnection to "/jdk*" */ private JarURLConnection getJarURLConnectionToJdk() { - URL resourceURL = atypeFactory.getClass().getResource("/annotated-jdk"); + // System.out.println("getJarURLConnectionToJdk()"); + URL resourceURL = null; + + // First, try to use the external annotated-jdk.jar file if specified + String externalJdkPath = System.getProperty("checker.annotated.jdk.jar"); + if (externalJdkPath == null) { + // Default fallback path + externalJdkPath = + "/Users/yutongzhu/dev/URA/checker-framework/checker/dist/annotated-jdk.jar"; + } + + try { + File externalJdkFile = new File(externalJdkPath); + if (externalJdkFile.exists()) { + // Create a jar URL pointing to the annotated-jdk directory within the external JAR + resourceURL = + new URL( + "jar:file:" + + externalJdkFile.getAbsolutePath() + + "!/annotated-jdk"); + } + } catch (Exception e) { + // Fall back to classpath resource if external JAR fails + if (stubDebug) { + System.out.printf( + "Failed to load external annotated JDK from %s: %s%n", + externalJdkPath, e.getMessage()); + } + } + + // // Fallback to classpath resource if external JAR not found or failed + // if (resourceURL == null) { + // resourceURL = atypeFactory.getClass().getResource("/annotated-jdk"); + // } + + if (resourceURL == null) { + throw new BugInCF( + "Cannot find annotated JDK either at external path " + + externalJdkPath + + " or in classpath"); + } + JarURLConnection connection; try { connection = (JarURLConnection) resourceURL.openConnection(); From c424380afc6350eab24c7a8b706a9bd3d3240d73 Mon Sep 17 00:00:00 2001 From: Yutong Zhu Date: Thu, 16 Oct 2025 21:27:54 -0400 Subject: [PATCH 2/6] Clean up absolute paths and test files --- TestAnnotatedJdk.java | 10 ---------- framework/build.gradle | 9 --------- .../stub/AnnotationFileElementTypes.java | 15 +-------------- 3 files changed, 1 insertion(+), 33 deletions(-) delete mode 100644 TestAnnotatedJdk.java diff --git a/TestAnnotatedJdk.java b/TestAnnotatedJdk.java deleted file mode 100644 index f2a3949d5fc3..000000000000 --- a/TestAnnotatedJdk.java +++ /dev/null @@ -1,10 +0,0 @@ -import java.util.List; -import java.util.ArrayList; - -public class TestAnnotatedJdk { - public static void main(String[] args) { - List list = new ArrayList<>(); - list.add("hello"); - list.add(null); // Should emit error with annotated JDK - } -} \ No newline at end of file diff --git a/framework/build.gradle b/framework/build.gradle index 25ba7e05278a..9de168f9bb19 100644 --- a/framework/build.gradle +++ b/framework/build.gradle @@ -148,15 +148,6 @@ task copyAndMinimizeAnnotatedJdkFiles(type: JavaExec, dependsOn: cloneAnnotatedJ sourcesJar.dependsOn(copyAndMinimizeAnnotatedJdkFiles) processResources.dependsOn(copyAndMinimizeAnnotatedJdkFiles) -task annotatedJdkJar(type: Jar, group: 'Build') { - description = 'Creates a separate JAR file containing only the annotated JDK stub files' - dependsOn(copyAndMinimizeAnnotatedJdkFiles) - destinationDirectory = file("/Users/yutongzhu/dev/URA/checker-framework/checker/dist") - archiveFileName = 'annotated-jdk.jar' - from "${buildDir}/generated/resources" - include 'annotated-jdk/**' -} - task allSourcesJar(type: Jar, group: 'Build') { description = 'Creates a sources jar that includes sources for all Checker Framework classes in framework.jar' destinationDirectory = file("${projectDir}/dist") diff --git a/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileElementTypes.java b/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileElementTypes.java index 34219d2b799f..6b54684d1d4f 100644 --- a/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileElementTypes.java +++ b/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileElementTypes.java @@ -868,12 +868,6 @@ private JarURLConnection getJarURLConnectionToJdk() { // First, try to use the external annotated-jdk.jar file if specified String externalJdkPath = System.getProperty("checker.annotated.jdk.jar"); - if (externalJdkPath == null) { - // Default fallback path - externalJdkPath = - "/Users/yutongzhu/dev/URA/checker-framework/checker/dist/annotated-jdk.jar"; - } - try { File externalJdkFile = new File(externalJdkPath); if (externalJdkFile.exists()) { @@ -894,15 +888,8 @@ private JarURLConnection getJarURLConnectionToJdk() { } // // Fallback to classpath resource if external JAR not found or failed - // if (resourceURL == null) { - // resourceURL = atypeFactory.getClass().getResource("/annotated-jdk"); - // } - if (resourceURL == null) { - throw new BugInCF( - "Cannot find annotated JDK either at external path " - + externalJdkPath - + " or in classpath"); + resourceURL = atypeFactory.getClass().getResource("/annotated-jdk"); } JarURLConnection connection; From fd72edf082d2c11c4510e6f62c9f3c519d0439a6 Mon Sep 17 00:00:00 2001 From: Yutong Zhu Date: Thu, 16 Oct 2025 21:43:42 -0400 Subject: [PATCH 3/6] Remove comments --- .../framework/stub/AnnotationFileElementTypes.java | 4 ---- 1 file changed, 4 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileElementTypes.java b/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileElementTypes.java index 6b54684d1d4f..53f215f9efdb 100644 --- a/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileElementTypes.java +++ b/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileElementTypes.java @@ -863,7 +863,6 @@ private void parseJdkJarEntry(String jarEntryName) { * @return a JarURLConnection to "/jdk*" */ private JarURLConnection getJarURLConnectionToJdk() { - // System.out.println("getJarURLConnectionToJdk()"); URL resourceURL = null; // First, try to use the external annotated-jdk.jar file if specified @@ -871,7 +870,6 @@ private JarURLConnection getJarURLConnectionToJdk() { try { File externalJdkFile = new File(externalJdkPath); if (externalJdkFile.exists()) { - // Create a jar URL pointing to the annotated-jdk directory within the external JAR resourceURL = new URL( "jar:file:" @@ -879,7 +877,6 @@ private JarURLConnection getJarURLConnectionToJdk() { + "!/annotated-jdk"); } } catch (Exception e) { - // Fall back to classpath resource if external JAR fails if (stubDebug) { System.out.printf( "Failed to load external annotated JDK from %s: %s%n", @@ -887,7 +884,6 @@ private JarURLConnection getJarURLConnectionToJdk() { } } - // // Fallback to classpath resource if external JAR not found or failed if (resourceURL == null) { resourceURL = atypeFactory.getClass().getResource("/annotated-jdk"); } From 70f7e8e7a2f2e00ba2378d744c9b796e92506122 Mon Sep 17 00:00:00 2001 From: Yutong Zhu Date: Mon, 27 Oct 2025 01:09:52 -0400 Subject: [PATCH 4/6] Add a description to the manual tex file --- docs/manual/creating-a-checker.tex | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/docs/manual/creating-a-checker.tex b/docs/manual/creating-a-checker.tex index 166d77f01d5c..8767517618b8 100644 --- a/docs/manual/creating-a-checker.tex +++ b/docs/manual/creating-a-checker.tex @@ -1987,6 +1987,11 @@ While creating a stub file, you may find the debugging options described in Section~\ref{stub-troubleshooting} useful. +\item + If you want to use an external annotated JDK .jar file, you can specify it when you run the checker: + \begin{Verbatim} + javac -J-Dchecker.annotated.jdk.jar=/path/to/annotated-jdk.jar -processor ... + \end{Verbatim} \end{itemize} From 7f7764d9b56b1b490250bc2f991fb48e23ed5254 Mon Sep 17 00:00:00 2001 From: Yutong Zhu Date: Sun, 23 Nov 2025 15:45:13 -0500 Subject: [PATCH 5/6] Add a gradle task for generating JDK, change getJarURLConnectionToJdk to allow the checker to only look at the annotated-jdk.jar at the same directory of the checker.jar --- framework/build.gradle | 25 ++++++++++++ .../stub/AnnotationFileElementTypes.java | 39 ++++++++++++------- 2 files changed, 51 insertions(+), 13 deletions(-) diff --git a/framework/build.gradle b/framework/build.gradle index 9de168f9bb19..8f3e3b088ce0 100644 --- a/framework/build.gradle +++ b/framework/build.gradle @@ -119,6 +119,22 @@ task copyAndMinimizeAnnotatedJdkFiles(type: JavaExec, dependsOn: cloneAnnotatedJ args outputDir doFirst { + if (project.hasProperty('annotatedJdkBranch')) { + def repoDir = file(annotatedJdkHome) + exec { + workingDir repoDir + commandLine 'git', 'fetch', '--all', '--tags' + } + exec { + workingDir repoDir + commandLine 'git', 'checkout', project.property('annotatedJdkBranch') + } + exec { + workingDir repoDir + commandLine 'git', 'pull', '--ff-only' + } + } + FileTree tree = fileTree(dir: inputDir) NavigableSet annotatedForFiles = new TreeSet<>(); // Populate `annotatedForFiles`. @@ -148,6 +164,15 @@ task copyAndMinimizeAnnotatedJdkFiles(type: JavaExec, dependsOn: cloneAnnotatedJ sourcesJar.dependsOn(copyAndMinimizeAnnotatedJdkFiles) processResources.dependsOn(copyAndMinimizeAnnotatedJdkFiles) +task annotatedJdkJar(type: Jar, dependsOn: copyAndMinimizeAnnotatedJdkFiles, group: 'Build') { + description = 'Packages the generated annotated JDK stubs into annotated-jdk.jar at the repository root' + destinationDirectory = rootProject.layout.projectDirectory.dir("checker/dist"); + archiveFileName = 'annotated-jdk.jar' + from("${buildDir}/generated/resources/annotated-jdk") { + into 'annotated-jdk' + } +} + task allSourcesJar(type: Jar, group: 'Build') { description = 'Creates a sources jar that includes sources for all Checker Framework classes in framework.jar' destinationDirectory = file("${projectDir}/dist") diff --git a/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileElementTypes.java b/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileElementTypes.java index 53f215f9efdb..e190ebe44407 100644 --- a/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileElementTypes.java +++ b/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileElementTypes.java @@ -857,18 +857,10 @@ private void parseJdkJarEntry(String jarEntryName) { } } - /** - * Returns a JarURLConnection to "/jdk*". - * - * @return a JarURLConnection to "/jdk*" - */ - private JarURLConnection getJarURLConnectionToJdk() { - URL resourceURL = null; - - // First, try to use the external annotated-jdk.jar file if specified - String externalJdkPath = System.getProperty("checker.annotated.jdk.jar"); + private final URL getAnnotatedJDKResourceURL(String resourcePath) { try { - File externalJdkFile = new File(externalJdkPath); + URL resourceURL = null; + File externalJdkFile = new File(resourcePath); if (externalJdkFile.exists()) { resourceURL = new URL( @@ -876,16 +868,37 @@ private JarURLConnection getJarURLConnectionToJdk() { + externalJdkFile.getAbsolutePath() + "!/annotated-jdk"); } + return resourceURL; } catch (Exception e) { if (stubDebug) { System.out.printf( "Failed to load external annotated JDK from %s: %s%n", - externalJdkPath, e.getMessage()); + resourcePath, e.getMessage()); } + return null; } + } + /** + * Returns a JarURLConnection to "/jdk*". + * + * @return a JarURLConnection to "/jdk*" + */ + private JarURLConnection getJarURLConnectionToJdk() { + // First, try to use the external annotated-jdk.jar file if specified + String pathFromProperty = System.getProperty("checker.annotated.jdk.jar"); + URL resourceURL = getAnnotatedJDKResourceURL(pathFromProperty); if (resourceURL == null) { - resourceURL = atypeFactory.getClass().getResource("/annotated-jdk"); + // Get the location of checker.jar + URL location = + atypeFactory.getClass().getProtectionDomain().getCodeSource().getLocation(); + try { + Path checkerDir = Paths.get(location.toURI()).getParent(); + String annotatedJarPath = checkerDir.resolve("annotated-jdk.jar").toString(); + resourceURL = getAnnotatedJDKResourceURL(annotatedJarPath); + } catch (URISyntaxException e) { + throw new BugInCF("Cannot parse URL: " + location.toString(), e); + } } JarURLConnection connection; From 759137666aa5f131a80817f8dfdb88437d9b6705 Mon Sep 17 00:00:00 2001 From: Yutong Zhu Date: Wed, 26 Nov 2025 20:48:35 -0500 Subject: [PATCH 6/6] Modify build.gradle to remove copying annotated-jdk into checker.jar and run annotatedJdkJar task when compiling --- framework/build.gradle | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/framework/build.gradle b/framework/build.gradle index 8f3e3b088ce0..7b86495e30b0 100644 --- a/framework/build.gradle +++ b/framework/build.gradle @@ -104,7 +104,7 @@ task copyAndMinimizeAnnotatedJdkFiles(type: JavaExec, dependsOn: cloneAnnotatedJ dependsOn ':javacutil:jar' dependsOn ':dataflow:jar' def inputDir = "${annotatedJdkHome}/src" - def outputDir = "${buildDir}/generated/resources/annotated-jdk/" + def outputDir = "${buildDir}/generated/annotated-jdk/" description = "Copy annotated JDK files to ${outputDir}. Removes private and package-private methods, method bodies, comments, etc. from the annotated JDK" @@ -161,18 +161,18 @@ task copyAndMinimizeAnnotatedJdkFiles(type: JavaExec, dependsOn: cloneAnnotatedJ } } -sourcesJar.dependsOn(copyAndMinimizeAnnotatedJdkFiles) -processResources.dependsOn(copyAndMinimizeAnnotatedJdkFiles) task annotatedJdkJar(type: Jar, dependsOn: copyAndMinimizeAnnotatedJdkFiles, group: 'Build') { description = 'Packages the generated annotated JDK stubs into annotated-jdk.jar at the repository root' destinationDirectory = rootProject.layout.projectDirectory.dir("checker/dist"); archiveFileName = 'annotated-jdk.jar' - from("${buildDir}/generated/resources/annotated-jdk") { + from("${buildDir}/generated/annotated-jdk") { into 'annotated-jdk' } } +processResources.dependsOn(annotatedJdkJar) + task allSourcesJar(type: Jar, group: 'Build') { description = 'Creates a sources jar that includes sources for all Checker Framework classes in framework.jar' destinationDirectory = file("${projectDir}/dist")