From b9e9a1e76d006879033fe35144f734ff0b8e5a74 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Mon, 21 Sep 2026 09:07:56 -0700 Subject: [PATCH 1/7] The Purity Checker implies -AcheckPurityAnnotations Checking purity annotations is the entire purpose of the Purity Checker, so running it no longer requires also supplying -AcheckPurityAnnotations. --- docs/manual/purity-checker.tex | 2 ++ .../framework/util/PurityChecker.java | 18 +++++++++++++++++- 2 files changed, 19 insertions(+), 1 deletion(-) diff --git a/docs/manual/purity-checker.tex b/docs/manual/purity-checker.tex index 4b3d1b2f6528..a92652dd818b 100644 --- a/docs/manual/purity-checker.tex +++ b/docs/manual/purity-checker.tex @@ -11,6 +11,8 @@ However, you may run just the Purity Checker by supplying the following command-line option to javac: \code{-processor org.checkerframework.framework.util.PurityChecker}. +That implies \<-AcheckPurityAnnotations>, so you do not need to supply that +option as well. The Checker Framework can infer purity annotations. If you supply the command-line option \<-AsuggestPureMethods>, then the diff --git a/framework/src/main/java/org/checkerframework/framework/util/PurityChecker.java b/framework/src/main/java/org/checkerframework/framework/util/PurityChecker.java index 6d50face48b8..4d3a8f00b841 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/PurityChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/util/PurityChecker.java @@ -1,5 +1,6 @@ package org.checkerframework.framework.util; +import java.util.Map; import org.checkerframework.common.basetype.BaseTypeChecker; /** @@ -9,7 +10,22 @@ * flow-sensitive analysis */ public class PurityChecker extends BaseTypeChecker { - // There is no implementation here. + // Other than forcing -AcheckPurityAnnotations, there is no implementation here. // It uses functionality from BaseTypeChecker, which itself calls // dataflow's purity implementation. + + /** + * {@inheritDoc} + * + *

Checking purity annotations is the entire purpose of this checker, so this implementation + * behaves as if {@code -AcheckPurityAnnotations} was supplied on the command line. + */ + @Override + public Map getOptions() { + Map options = super.getOptions(); + if (!options.containsKey("checkPurityAnnotations")) { + options.put("checkPurityAnnotations", null); + } + return options; + } } From b9879e7326fe2c61b65735247909110f578f6253 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Tue, 22 Sep 2026 09:36:34 -0700 Subject: [PATCH 2/7] Add comment. --- build.gradle | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/build.gradle b/build.gradle index 4efdad8c0dab..7fd18299db50 100644 --- a/build.gradle +++ b/build.gradle @@ -1200,7 +1200,8 @@ subprojects { tasks.register("typecheck-part1") { description = "Run the Checker Framework on itself (part 1)" group = "Verification" - dependsOn("checkCompilerMessages", "checkFormatter", "checkInterning", "checkOptional", "checkPurity") + dependsOn("checkCompilerMessages", "checkFormatter", "checkInterning", "checkOptional") + // Can't run "checkPurity" because it issues too many warnings. } tasks.register("typecheck-part2") { description = "Run the Checker Framework on itself (part 2)" From 22f83cc37e1e974a903b2c3a30b36bc99a8d22ec Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Tue, 22 Sep 2026 10:10:22 -0700 Subject: [PATCH 3/7] Clarify that -AcheckPurityAnnotations is off by default only for checkers other than the Purity Checker --- docs/manual/purity-checker.tex | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/docs/manual/purity-checker.tex b/docs/manual/purity-checker.tex index a92652dd818b..c6c60b63c447 100644 --- a/docs/manual/purity-checker.tex +++ b/docs/manual/purity-checker.tex @@ -63,10 +63,11 @@ by writing \refqualclass{dataflow/qual}{Deterministic} on the declaration of a method that is not deterministic. -To enable -checking of the annotations, supply the command-line option -\<-AcheckPurityAnnotations>. It is not enabled by default because of a high false -positive rate. In the future, after a new purity-checking analysis is +When you run the Purity Checker directly, it checks the annotations. +To enable checking of the annotations when running any other checker, +supply the command-line option \<-AcheckPurityAnnotations>. +For checkers other than the Purity Checker, it is not enabled by default +because of a high false positive rate. In the future, after a new purity-checking analysis is implemented, the Checker Framework will default to checking purity annotations. From 5c705d3ee01c196c36dba90b240ac67d7a72f883 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Tue, 22 Sep 2026 10:11:24 -0700 Subject: [PATCH 4/7] Add a documented constructor to PurityChecker --- .../org/checkerframework/framework/util/PurityChecker.java | 3 +++ 1 file changed, 3 insertions(+) diff --git a/framework/src/main/java/org/checkerframework/framework/util/PurityChecker.java b/framework/src/main/java/org/checkerframework/framework/util/PurityChecker.java index 4d3a8f00b841..76e3c2b90686 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/PurityChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/util/PurityChecker.java @@ -14,6 +14,9 @@ public class PurityChecker extends BaseTypeChecker { // It uses functionality from BaseTypeChecker, which itself calls // dataflow's purity implementation. + /** Creates a PurityChecker. */ + public PurityChecker() {} + /** * {@inheritDoc} * From 5702c4d63b35e115d186805b36a979c831494934 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Tue, 22 Sep 2026 10:45:50 -0700 Subject: [PATCH 5/7] Use a non-null value for the checkPurityAnnotations option --- .../java/org/checkerframework/framework/util/PurityChecker.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/framework/src/main/java/org/checkerframework/framework/util/PurityChecker.java b/framework/src/main/java/org/checkerframework/framework/util/PurityChecker.java index 76e3c2b90686..078b05af6f68 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/PurityChecker.java +++ b/framework/src/main/java/org/checkerframework/framework/util/PurityChecker.java @@ -27,7 +27,7 @@ public PurityChecker() {} public Map getOptions() { Map options = super.getOptions(); if (!options.containsKey("checkPurityAnnotations")) { - options.put("checkPurityAnnotations", null); + options.put("checkPurityAnnotations", "true"); } return options; } From 090f2f0a3ec0bd041da4e9a66eb53c7abcb80873 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Tue, 22 Sep 2026 11:55:32 -0700 Subject: [PATCH 6/7] Test that the Purity Checker checks purity annotations without -AcheckPurityAnnotations --- .../test/junit/PurityCheckerTest.java | 25 ++++++++++ .../PurityCheckerChecksAnnotations.java | 48 +++++++++++++++++++ 2 files changed, 73 insertions(+) create mode 100644 framework/src/test/java/org/checkerframework/framework/test/junit/PurityCheckerTest.java create mode 100644 framework/tests/purity-checker/PurityCheckerChecksAnnotations.java diff --git a/framework/src/test/java/org/checkerframework/framework/test/junit/PurityCheckerTest.java b/framework/src/test/java/org/checkerframework/framework/test/junit/PurityCheckerTest.java new file mode 100644 index 000000000000..70ecf05be6ba --- /dev/null +++ b/framework/src/test/java/org/checkerframework/framework/test/junit/PurityCheckerTest.java @@ -0,0 +1,25 @@ +package org.checkerframework.framework.test.junit; + +import java.io.File; +import java.util.List; +import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; +import org.checkerframework.framework.util.PurityChecker; +import org.junit.runners.Parameterized.Parameters; + +/** + * Tests that the Purity Checker issues purity diagnostics without {@code -AcheckPurityAnnotations}. + */ +public class PurityCheckerTest extends CheckerFrameworkPerDirectoryTest { + + /** + * @param testFiles the files containing test code, which will be type-checked + */ + public PurityCheckerTest(List testFiles) { + super(testFiles, PurityChecker.class, "purity-checker"); + } + + @Parameters + public static String[] getTestDirs() { + return new String[] {"purity-checker"}; + } +} diff --git a/framework/tests/purity-checker/PurityCheckerChecksAnnotations.java b/framework/tests/purity-checker/PurityCheckerChecksAnnotations.java new file mode 100644 index 000000000000..c2cac2a2800f --- /dev/null +++ b/framework/tests/purity-checker/PurityCheckerChecksAnnotations.java @@ -0,0 +1,48 @@ +// The Purity Checker checks purity annotations even without -AcheckPurityAnnotations. This file +// holds the same violations as framework/tests/purity-not-checked/PurityMethodRefNotChecked.java, +// and expects a diagnostic for each of them. + +import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.dataflow.qual.SideEffectFree; + +public class PurityCheckerChecksAnnotations { + + int count = 0; + + @FunctionalInterface + interface PureFunc { + @Pure + String doNothing(); + } + + @FunctionalInterface + interface SefFunc { + @SideEffectFree + String doNothing(); + } + + static String myMethod() { + return ""; + } + + /** A method reference to a method that lacks the functional method's purity. */ + void methodReference() { + // :: error: [purity.methodref] + PureFunc f = PurityCheckerChecksAnnotations::myMethod; + // :: error: [purity.methodref] + SefFunc g = PurityCheckerChecksAnnotations::myMethod; + } + + /** A lambda whose body lacks the functional method's purity. */ + void lambda() { + // :: error: [purity.not.sideeffectfree.assign.field] + SefFunc f = () -> "" + count++; + } + + /** A method whose body lacks its own purity. */ + @SideEffectFree + int assignsField() { + // :: error: [purity.not.sideeffectfree.assign.field] + return count++; + } +} From 38a447d02a432e661090ba5303c640ecbe3ab018 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Wed, 23 Sep 2026 08:01:44 -0700 Subject: [PATCH 7/7] Doc tweaks --- docs/manual/purity-checker.tex | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/docs/manual/purity-checker.tex b/docs/manual/purity-checker.tex index c6c60b63c447..6261c4e3db10 100644 --- a/docs/manual/purity-checker.tex +++ b/docs/manual/purity-checker.tex @@ -11,8 +11,8 @@ However, you may run just the Purity Checker by supplying the following command-line option to javac: \code{-processor org.checkerframework.framework.util.PurityChecker}. -That implies \<-AcheckPurityAnnotations>, so you do not need to supply that -option as well. +That implies \<-AcheckPurityAnnotations>, so you do not need to supply +both options. The Checker Framework can infer purity annotations. If you supply the command-line option \<-AsuggestPureMethods>, then the @@ -67,7 +67,8 @@ To enable checking of the annotations when running any other checker, supply the command-line option \<-AcheckPurityAnnotations>. For checkers other than the Purity Checker, it is not enabled by default -because of a high false positive rate. In the future, after a new purity-checking analysis is +because of a high false +positive rate. In the future, after a new purity-checking analysis is implemented, the Checker Framework will default to checking purity annotations.