From 089e1bc874bb1ce341cbcceb1615d3c36566bf38 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Mon, 21 Sep 2026 09:07:56 -0700 Subject: [PATCH 01/10] 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. Co-Authored-By: Claude Opus 5 --- docs/CHANGELOG.md | 4 ++++ docs/manual/purity-checker.tex | 2 ++ .../framework/util/PurityChecker.java | 18 +++++++++++++++++- 3 files changed, 23 insertions(+), 1 deletion(-) diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 04ceacd097aa..501f368d02a1 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -14,6 +14,10 @@ New `wpi2.sh` script does whole-program inference, but requires buildfile edits. The Purity Checker has been improved, so `-AcheckPurityAnnotations` may issue warnings that it did not previously. +Running the Purity Checker on its own (`-processor +org.checkerframework.framework.util.PurityChecker`) implies +`-AcheckPurityAnnotations`, which no longer needs to be supplied explicitly. + ### Changes for type system implementers `JavaParserUtil`: moved `DEFAULT_LANGUAGE_LEVEL`, `parseCompilationUnit()`, diff --git a/docs/manual/purity-checker.tex b/docs/manual/purity-checker.tex index a334e5f8c365..20386550d3b9 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 260c556b4ff3b79a766141f883751bbdceec023a Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Mon, 21 Sep 2026 09:26:23 -0700 Subject: [PATCH 02/10] Add some purity annos. --- .../org/checkerframework/javacutil/AnnotationUtils.java | 6 ++++-- .../checkerframework/javacutil/TreeUtilsAfterJava11.java | 2 +- 2 files changed, 5 insertions(+), 3 deletions(-) diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java index 8dba22ce3539..331669629835 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java @@ -71,7 +71,8 @@ private AnnotationUtils() { * @param annotation the annotation whose name to return * @return the fully-qualified name of an annotation as a String */ - public static final @CanonicalName String annotationName(AnnotationMirror annotation) { + @Pure + public static @CanonicalName String annotationName(AnnotationMirror annotation) { if (annotation instanceof AnnotationBuilder.CheckerFrameworkAnnotationMirror cfam) { return cfam.annotationName; } @@ -150,6 +151,7 @@ public static boolean areSame(AnnotationMirror a1, AnnotationMirror a2) { * @see #areSame(AnnotationMirror, AnnotationMirror) */ @EqualsMethod + @Pure public static int compareByName(AnnotationMirror a1, AnnotationMirror a2) { if (a1 == a2) { return 0; @@ -705,7 +707,7 @@ private static class NoSuchElementException extends BugInCF { * * @param message the detail message */ - @Pure + @SideEffectFree public NoSuchElementException(String message) { super(message); } diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtilsAfterJava11.java b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtilsAfterJava11.java index ddf855c42600..df4dd0db1ba4 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtilsAfterJava11.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtilsAfterJava11.java @@ -18,7 +18,7 @@ * This class contains utility methods for reflectively accessing Tree classes and methods that were * added after Java 11. */ -@SuppressWarnings("PMD.MissingStaticMethodInNonInstantiatableClass") +@SuppressWarnings({"PMD.MissingStaticMethodInNonInstantiatableClass", "purity"}) @Deprecated(forRemoval = true, since = "4.0.0") public final class TreeUtilsAfterJava11 { From e222c8997359f23abe66ff796205fe6e59a87c9e Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Mon, 21 Sep 2026 11:19:16 -0700 Subject: [PATCH 03/10] Make javacutil pass the Purity Checker Now that the Purity Checker implies -AcheckPurityAnnotations, `checkPurity` verifies purity annotations rather than trusting them, and javacutil reported about 100 errors. It now reports none. Most are fixed by writing the annotation that was missing: * @SideEffectFree on BugInCF's constructors and @Pure on getLocation(). This alone fixed 14 errors, because `throw new BugInCF(...)` appears in many methods that are declared pure. * @Pure on ten TreeUtils methods, each of which reads a tree or symbol field. * @Pure on CheckerFrameworkAnnotationValue.getValue(), and @SideEffectFree on DefaultAnnotationFormatter's constructor. The rest are suppressed, and the suppressions are concentrated in one structural limitation: the Purity Checker has no escape analysis. It therefore cannot verify: * a @Deterministic method that iterates a collection, because Collection.iterator() and Map.keySet()/entrySet() allocate a fresh iterator or view -- so they are @SideEffectFree but not @Deterministic -- and Iterator.next() mutates the iterator; * a @SideEffectFree method that mutates a locally allocated StringBuilder, StringJoiner, or TreeSet, or that memoizes its result in a field; * a @Deterministic method containing a catch block. Because java.util.Map and java.util.Set declare containsKey, get, contains, equals, and hashCode as @Pure, and purity annotations are inherited, every collection implementation inherits an obligation that it cannot discharge. AnnotationMirrorMap takes a class-level suppression for that reason, since all of its inherited pure methods are affected; elsewhere the suppressions are per-method. This is concretely the "high false positive rate" that the manual cites for not enabling -AcheckPurityAnnotations by default, and it is what the new purity analysis promised there would need to address. Two annotations are retained with a suppression rather than removed, because each is load-bearing for type refinement in callers: AnnotationUtils.annotationName (Name.toString() returns a fresh but always-equal String) and AbstractTypeProcessor.getCompilerLog (Log.instance() registers the Log in the compiler Context on its first call). Dropping @SideEffectFree from the latter costs three nullness errors in CFGProcessor, whose fields lose their refinement across the call. `typecheck-part1` runs `checkPurity` only on javacutil; the other subprojects do not pass it yet. Each still has its own `checkPurity` task to run directly. Co-Authored-By: Claude Opus 5 --- build.gradle | 7 ++++++- .../javacutil/AbstractTypeProcessor.java | 5 +++++ .../checkerframework/javacutil/AnnotationBuilder.java | 5 +++++ .../javacutil/AnnotationMirrorMap.java | 6 ++++++ .../javacutil/AnnotationMirrorSet.java | 2 ++ .../checkerframework/javacutil/AnnotationUtils.java | 11 ++++++++++- .../java/org/checkerframework/javacutil/BugInCF.java | 10 ++++++++++ .../javacutil/DefaultAnnotationFormatter.java | 3 +++ .../org/checkerframework/javacutil/TreeUtils.java | 10 ++++++++++ 9 files changed, 57 insertions(+), 2 deletions(-) diff --git a/build.gradle b/build.gradle index 7de6e0f76c9c..cc4486c906f9 100644 --- a/build.gradle +++ b/build.gradle @@ -1191,7 +1191,12 @@ 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") + // The Purity Checker passes only on javacutil so far. To work on another subproject, run + // its `checkPurity` task directly, such as `./gradlew :dataflow:checkPurity`. + if (project.name.equals("javacutil")) { + dependsOn("checkPurity") + } } tasks.register("typecheck-part2") { description = "Run the Checker Framework on itself (part 2)" diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AbstractTypeProcessor.java b/javacutil/src/main/java/org/checkerframework/javacutil/AbstractTypeProcessor.java index 36f33920dceb..83777f656d10 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AbstractTypeProcessor.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/AbstractTypeProcessor.java @@ -153,7 +153,12 @@ public void typeProcessingOver() { * * @return the compiler log, which contains errors and warnings */ + // Log.instance() constructs the Log and registers it in the compiler Context on its first + // call, so it is not strictly side-effect-free. @SideEffectFree is retained because javac + // creates the Log before any annotation processor runs, and because callers rely on it to + // preserve field refinements across the call. @SideEffectFree + @SuppressWarnings("purity") // Log.instance() registers the Log in the Context on the first call public Log getCompilerLog() { return Log.instance(((JavacProcessingEnvironment) processingEnv).getContext()); } diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationBuilder.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationBuilder.java index 1e6115e528d7..75c840d0bccc 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationBuilder.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationBuilder.java @@ -32,6 +32,7 @@ import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.checker.signature.qual.CanonicalName; import org.checkerframework.checker.signature.qual.FullyQualifiedName; +import org.checkerframework.dataflow.qual.Pure; import org.checkerframework.dataflow.qual.SideEffectFree; import org.plumelib.reflection.ReflectionP; import org.plumelib.util.ArrayMap; @@ -832,6 +833,7 @@ public DeclaredType getAnnotationType() { } @SideEffectFree + @SuppressWarnings("purity") // mutates only local builders and memoizes toString @Override public String toString() { if (toStringVal != null) { @@ -875,12 +877,14 @@ private static class CheckerFrameworkAnnotationValue implements AnnotationValue this.value = obj; } + @Pure @Override public Object getValue() { return value; } @SideEffectFree + @SuppressWarnings("purity") // mutates only a local String and memoizes toString @Override public String toString() { if (this.toStringVal != null) { @@ -944,6 +948,7 @@ public R accept(AnnotationValueVisitor v, P p) { } } + @SuppressWarnings("purity") // getValue() may allocate; comparison is by content @Override public boolean equals(@Nullable Object obj) { // System.out.printf("Calling CFAV.equals()%n"); diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorMap.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorMap.java index b88da0781242..bea1905f0aeb 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorMap.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorMap.java @@ -27,6 +27,12 @@ *

AnnotationMirror is an interface and not all implementing classes provide a correct equals * method; therefore, existing implementations of Map cannot be used. */ +// Every @Pure method inherited from Map (containsKey, get, equals, hashCode) iterates a +// collection, which the Purity Checker cannot verify: Collection.iterator() and +// Map.keySet()/entrySet() are @SideEffectFree but not @Deterministic, because each call +// allocates a fresh iterator or view, and Iterator.next() mutates it. The catch block in +// equals() is likewise forbidden in a @Deterministic method. +@SuppressWarnings("purity") public class AnnotationMirrorMap implements Map<@KeyFor("this") AnnotationMirror, V> { /** The actual map to which all work is delegated. */ diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorSet.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorSet.java index 51719fb685ac..ecb0fcca6b83 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorSet.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorSet.java @@ -135,6 +135,7 @@ public boolean isEmpty() { return shadowSet.isEmpty(); } + @SuppressWarnings("purity") // containsSame iterates the set @Override public boolean contains( @UnknownInitialization(AnnotationMirrorSet.class) AnnotationMirrorSet this, @@ -261,6 +262,7 @@ public boolean equals(@Nullable Object o) { return containsAll(s); } + @SuppressWarnings("purity") // iterates the set @Override public int hashCode() { int result = 0; diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java index 331669629835..388ec356b280 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java @@ -78,7 +78,14 @@ private AnnotationUtils() { } DeclaredType annoType = annotation.getAnnotationType(); TypeElement elm = (TypeElement) annoType.asElement(); - @SuppressWarnings("signature:assignment") // JDK needs annotations + // Name.toString() returns a String that is `equals` to, but not `==` to, the result of any + // previous call, so this method is not deterministic in the strict sense that @Deterministic + // requires. Every client compares annotation names by content, so @Pure is the useful + // specification. + @SuppressWarnings({ + "signature:assignment", // JDK needs annotations + "purity" // Name.toString() returns a fresh but always-equal String + }) @CanonicalName String name = elm.getQualifiedName().toString(); return name; } @@ -399,6 +406,7 @@ public static boolean containsSameByName( * @return an ordering over AnnotationMirrors based on their name and values */ @Pure + @SuppressWarnings("purity") // mutates only a newly allocated set public static int compareAnnotationMirrors(AnnotationMirror a1, AnnotationMirror a2) { int nameComparison = compareByName(a1, a2); if (nameComparison != 0) { @@ -1473,6 +1481,7 @@ public static boolean hasTypeQualifierElementTypes(ElementType[] elements, Class * @return the string representation, using simple (not fully-qualified) names */ @SideEffectFree + @SuppressWarnings("purity") // mutates only a newly allocated StringJoiner public static String toStringSimple(AnnotationMirrorSet annos) { DefaultAnnotationFormatter defaultAnnotationFormatter = new DefaultAnnotationFormatter(); StringJoiner result = new StringJoiner(" "); diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/BugInCF.java b/javacutil/src/main/java/org/checkerframework/javacutil/BugInCF.java index a7fd353e2ec4..75591ca644c8 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/BugInCF.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/BugInCF.java @@ -3,6 +3,8 @@ import com.sun.source.tree.Tree; import org.checkerframework.checker.formatter.qual.FormatMethod; import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.dataflow.qual.SideEffectFree; /** * Exception type indicating a bug in the framework. @@ -22,6 +24,7 @@ public class BugInCF extends RuntimeException { * * @param message the detail message */ + @SideEffectFree public BugInCF(String message) { this(message, new Throwable()); } @@ -34,6 +37,7 @@ public BugInCF(String message) { * @param args the arguments for the format string */ @FormatMethod + @SideEffectFree public BugInCF(String fmt, @Nullable Object... args) { this(String.format(fmt, args), new Throwable()); } @@ -43,6 +47,7 @@ public BugInCF(String fmt, @Nullable Object... args) { * * @param cause the cause; its detail message will be used and must be non-null */ + @SideEffectFree public BugInCF(Throwable cause) { this((Tree) null, cause); } @@ -53,6 +58,7 @@ public BugInCF(Throwable cause) { * @param location where to report the bug * @param cause the cause; its detail message will be used and must be non-null */ + @SideEffectFree public BugInCF(@Nullable Tree location, Throwable cause) { this( location, @@ -69,6 +75,7 @@ public BugInCF(@Nullable Tree location, Throwable cause) { * @param args the arguments for the format string */ @FormatMethod + @SideEffectFree public BugInCF(Throwable cause, String fmt, @Nullable Object... args) { this(String.format(fmt, args), cause); } @@ -79,6 +86,7 @@ public BugInCF(Throwable cause, String fmt, @Nullable Object... args) { * @param message the detail message * @param cause the cause */ + @SideEffectFree public BugInCF(String message, Throwable cause) { this(null, message, cause); } @@ -90,6 +98,7 @@ public BugInCF(String message, Throwable cause) { * @param message the detail message * @param cause the cause */ + @SideEffectFree public BugInCF(@Nullable Tree location, String message, Throwable cause) { super(message, cause); if (cause instanceof BugInCF bugInCf && bugInCf.getLocation() != null) { @@ -110,6 +119,7 @@ public BugInCF(@Nullable Tree location, String message, Throwable cause) { * * @return the tree at which to report the exception */ + @Pure public @Nullable Tree getLocation() { return location; } diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/DefaultAnnotationFormatter.java b/javacutil/src/main/java/org/checkerframework/javacutil/DefaultAnnotationFormatter.java index 3c479ed5b62b..c163802a5f76 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/DefaultAnnotationFormatter.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/DefaultAnnotationFormatter.java @@ -16,6 +16,7 @@ /** A utility for converting AnnotationMirrors to Strings. It omits full package names. */ public class DefaultAnnotationFormatter implements AnnotationFormatter { /** Creates a DefaultAnnotationFormatter. */ + @SideEffectFree public DefaultAnnotationFormatter() {} /** @@ -46,6 +47,7 @@ public static boolean isInvisibleQualified(AnnotationMirror anno) { */ @Override @SideEffectFree + @SuppressWarnings("purity") // appends only to a local StringBuilder public String formatAnnotationString( Collection annos, boolean printInvisible) { StringBuilder sb = new StringBuilder(); @@ -73,6 +75,7 @@ public String formatAnnotationString( */ @Override @SideEffectFree + @SuppressWarnings("purity") // appends only to a local StringBuilder public String formatAnnotationMirror(AnnotationMirror anno) { StringBuilder sb = new StringBuilder(); formatAnnotationMirror(anno, sb); diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java index b4222cecf197..f91d885f9185 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java @@ -276,6 +276,7 @@ public static boolean isSelfAccess(ExpressionTree tree) { * @param tree an expression tree * @return the outermost non-parenthesized tree enclosed by the given tree */ + @Pure @SuppressWarnings("interning:return") // polymorphism implementation public static @PolyInterned ExpressionTree withoutParens(@PolyInterned ExpressionTree tree) { ExpressionTree t = tree; @@ -292,6 +293,7 @@ public static boolean isSelfAccess(ExpressionTree tree) { * @param tree an expression tree * @return the outermost non-parenthesized non-cast tree enclosed by the given tree */ + @Pure @SuppressWarnings("interning:return") // polymorphism implementation public static @PolyInterned ExpressionTree withoutParensOrCasts( @PolyInterned ExpressionTree tree) { @@ -322,6 +324,7 @@ public static boolean isSelfAccess(ExpressionTree tree) { * @param tree class declaration * @return the element for the given class */ + @Pure public static @Nullable TypeElement elementFromDeclaration(ClassTree tree) { TypeElement result = (TypeElement) TreeInfo.symbolFor((JCTree) tree); return result; @@ -541,6 +544,7 @@ public static ExecutableElement elementFromUse(MemberReferenceTree tree) { * @param tree a method declaration * @return the element for the given method */ + @Pure public static @Nullable ExecutableElement elementFromDeclaration(MethodTree tree) { ExecutableElement result = (ExecutableElement) TreeInfo.symbolFor((JCTree) tree); return result; @@ -629,6 +633,7 @@ public static ExecutableElement elementFromUse(NewClassTree tree) { * @param tree the variable * @return the element for the given variable */ + @Pure public static @Nullable VariableElement elementFromDeclaration(VariableTree tree) { VariableElement result = (VariableElement) TreeInfo.symbolFor((JCTree) tree); // `result` can be null, for example for this variable declaration: @@ -1114,6 +1119,7 @@ public static Set classAndMethodTreeKinds() { * * @return the set of kinds that represent classes */ + @Pure public static Set classTreeKinds() { return classTreeKinds; } @@ -1124,6 +1130,7 @@ public static Set classTreeKinds() { * @param tree the tree to test * @return true, iff the given kind is a class kind */ + @Pure public static boolean isClassTree(Tree tree) { return classTreeKinds().contains(tree.getKind()); } @@ -1653,6 +1660,7 @@ public static VariableElement getField( * @param tree the Tree to test * @return true if the tree is an ExpressionTree */ + @Pure public static boolean isExpressionTree(Tree tree) { return tree instanceof ExpressionTree; } @@ -1679,6 +1687,7 @@ public static boolean isEnumSuperCall(MethodInvocationTree tree) { * @param tree the Tree to test * @return true if the tree is a type declaration */ + @Pure public static boolean isTypeDeclaration(Tree tree) { return isClassTree(tree) || tree instanceof TypeParameterTree; } @@ -1858,6 +1867,7 @@ public static boolean isLocalVariable(Tree tree) { * * @return the type as a TypeMirror of {@code tree} */ + @Pure public static TypeMirror typeOf(Tree tree) { return ((JCTree) tree).type; } From 4fa2b3010b1c282038d21211a9aff6eb22787ab4 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Mon, 21 Sep 2026 11:40:25 -0700 Subject: [PATCH 04/10] Make checker-qual, checker-util, and framework-test pass the Purity Checker This clears 21 errors across 6 files, and brings the number of subprojects that pass `checkPurity` from one to five: checker-qual-android needed no edit, because its 14 errors were in generated copies of the two checker-qual files fixed here. ConversionCategory.toString() was declared @Pure, which contradicts the rule that the annotated JDK records in a @CFComment on Object.toString(): a toString() that builds its result returns a string that differs according to ==, and @Deterministic requires that two calls return == results. It is now @SideEffectFree. That was a wrong annotation rather than a false positive. The other errors are the structural limitation described in the previous commit: the Purity Checker has no escape analysis, so it cannot verify a method that mutates a locally allocated StringBuilder, StringJoiner, or list, that calls String.format or Character.toString (each of which returns a fresh string), or that contains a catch block. Three of RegexUtil's suppressions already explained this reasoning -- one comment reads "temp value used in pure method is equal up to equals but not up to ==" -- so "purity" joins the existing @SuppressWarnings lists rather than arriving as a separate annotation, and each key now carries its own justification. In framework-test, both errors reached the same helper, so annotating the chain (TestUtilities.optionMapToList, SimpleOptionMap.getOptionsAsList, and ImmutableTestConfiguration.getFlatOptions as @SideEffectFree) needs one suppression instead of two and gives those methods a correct specification. `typecheck-part1` now excludes `checkPurity` by naming the four subprojects that still fail -- annotation-file-utilities, checker, dataflow, and framework -- so that a subproject is covered as soon as it passes. Co-Authored-By: Claude Opus 5 --- build.gradle | 10 +++++++--- .../formatter/qual/ConversionCategory.java | 7 +++++-- .../qual/I18nConversionCategory.java | 1 + .../checker/formatter/util/FormatUtil.java | 2 ++ .../checker/regex/util/RegexUtil.java | 16 ++++++++++++---- .../test/ImmutableTestConfiguration.java | 2 ++ .../framework/test/SimpleOptionMap.java | 2 ++ .../framework/test/TestUtilities.java | 3 +++ 8 files changed, 34 insertions(+), 9 deletions(-) diff --git a/build.gradle b/build.gradle index cc4486c906f9..2d21d2bdf8fc 100644 --- a/build.gradle +++ b/build.gradle @@ -1192,9 +1192,13 @@ subprojects { description = "Run the Checker Framework on itself (part 1)" group = "Verification" dependsOn("checkCompilerMessages", "checkFormatter", "checkInterning", "checkOptional") - // The Purity Checker passes only on javacutil so far. To work on another subproject, run - // its `checkPurity` task directly, such as `./gradlew :dataflow:checkPurity`. - if (project.name.equals("javacutil")) { + // The Purity Checker does not yet pass on annotation-file-utilities, checker, dataflow, + // or framework. To work on one of those, run its `checkPurity` task directly, such as + // `./gradlew :dataflow:checkPurity`. + if (!(project.name.equals("annotation-file-utilities") + || project.name.equals("checker") + || project.name.equals("dataflow") + || project.name.equals("framework"))) { dependsOn("checkPurity") } } diff --git a/checker-qual/src/main/java/org/checkerframework/checker/formatter/qual/ConversionCategory.java b/checker-qual/src/main/java/org/checkerframework/checker/formatter/qual/ConversionCategory.java index d6fb615cac07..d4e122b4a47f 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/formatter/qual/ConversionCategory.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/formatter/qual/ConversionCategory.java @@ -11,7 +11,7 @@ import java.util.Set; import java.util.StringJoiner; import org.checkerframework.checker.nullness.qual.Nullable; -import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.dataflow.qual.SideEffectFree; import org.checkerframework.framework.qual.AnnotatedFor; /** @@ -353,7 +353,10 @@ public boolean isAssignableFrom(Class argType) { } /** Returns a pretty-printed {@link ConversionCategory}. */ - @Pure + // This is @SideEffectFree rather than @Pure because it returns a string that differs + // according to ==, and @Deterministic requires that two calls return == results. + @SideEffectFree + @SuppressWarnings("purity") // appends only to a local StringBuilder @Override public String toString() { StringBuilder sb = new StringBuilder(32); diff --git a/checker-qual/src/main/java/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java b/checker-qual/src/main/java/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java index dc21f1a33b60..b0d2a5b315a1 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java +++ b/checker-qual/src/main/java/org/checkerframework/checker/i18nformatter/qual/I18nConversionCategory.java @@ -197,6 +197,7 @@ public boolean isAssignableFrom(Class argType) { } /** Returns a pretty-printed {@link I18nConversionCategory}. */ + @SuppressWarnings("purity") // appends only to a local StringBuilder @Override public String toString() { StringBuilder sb = new StringBuilder(this.name()); diff --git a/checker-util/src/main/java/org/checkerframework/checker/formatter/util/FormatUtil.java b/checker-util/src/main/java/org/checkerframework/checker/formatter/util/FormatUtil.java index 05f17e02b2b5..d2f8560f6714 100644 --- a/checker-util/src/main/java/org/checkerframework/checker/formatter/util/FormatUtil.java +++ b/checker-util/src/main/java/org/checkerframework/checker/formatter/util/FormatUtil.java @@ -294,6 +294,7 @@ public int getFound() { return found; } + @SuppressWarnings("purity") // String.format() returns a fresh but always-equal String @Override public String getMessage() { return String.format("Expected %d arguments but found %d.", expected, found); @@ -325,6 +326,7 @@ public ConversionCategory getFound() { return found; } + @SuppressWarnings("purity") // String.format() returns a fresh but always-equal String @Override public String getMessage() { return String.format("Expected category %s but found %s.", expected, found); diff --git a/checker-util/src/main/java/org/checkerframework/checker/regex/util/RegexUtil.java b/checker-util/src/main/java/org/checkerframework/checker/regex/util/RegexUtil.java index e697598fcc41..06c3c013775f 100644 --- a/checker-util/src/main/java/org/checkerframework/checker/regex/util/RegexUtil.java +++ b/checker-util/src/main/java/org/checkerframework/checker/regex/util/RegexUtil.java @@ -163,7 +163,10 @@ public static boolean isRegex(String s) { * @param groups number of groups expected * @return true iff s is a regular expression with {@code groups} groups */ - @SuppressWarnings("regex") // RegexUtil + @SuppressWarnings({ + "regex", // RegexUtil + "purity" // catch block is a guard; the result depends only on the arguments + }) @Pure // @EnsuresQualifierIf annotation is extraneous because this method is special-cased // in RegexTransfer. @@ -185,8 +188,10 @@ public static boolean isRegex(String s, int groups) { * @return true iff c is a regular expression */ @SuppressWarnings({ - "regex", "lock" - }) // RegexUtil; temp value used in pure method is equal up to equals but not up to == + "regex", // RegexUtil + "lock", // temp value used in pure method is equal up to equals but not up to == + "purity" // Character.toString() returns a fresh but always-equal String + }) @Pure @EnsuresQualifierIf(result = true, expression = "#1", qualifier = Regex.class) public static boolean isRegex(char c) { @@ -333,7 +338,10 @@ private static String regexErrorMessage(String s, int expectedGroups, int actual * @param p pattern whose groups to count * @return the count of groups in the argument */ - @SuppressWarnings("lock") // does not depend on object identity + @SuppressWarnings({ + "lock", // does not depend on object identity + "purity" // Pattern.matcher() allocates; the count depends only on the argument + }) @Pure private static int getGroupCount(Pattern p) { return p.matcher("").groupCount(); diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/ImmutableTestConfiguration.java b/framework-test/src/main/java/org/checkerframework/framework/test/ImmutableTestConfiguration.java index e765cb0626d7..d15d213aa5b7 100644 --- a/framework-test/src/main/java/org/checkerframework/framework/test/ImmutableTestConfiguration.java +++ b/framework-test/src/main/java/org/checkerframework/framework/test/ImmutableTestConfiguration.java @@ -8,6 +8,7 @@ import java.util.Map; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.checker.signature.qual.BinaryName; +import org.checkerframework.dataflow.qual.SideEffectFree; import org.plumelib.util.StringsP; /** @@ -90,6 +91,7 @@ public List getDiagnosticFiles() { return options; } + @SideEffectFree @Override public List getFlatOptions() { return TestUtilities.optionMapToList(options); diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/SimpleOptionMap.java b/framework-test/src/main/java/org/checkerframework/framework/test/SimpleOptionMap.java index 49263af5aae1..227afc03f6db 100644 --- a/framework-test/src/main/java/org/checkerframework/framework/test/SimpleOptionMap.java +++ b/framework-test/src/main/java/org/checkerframework/framework/test/SimpleOptionMap.java @@ -6,6 +6,7 @@ import java.util.List; import java.util.Map; import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.dataflow.qual.SideEffectFree; /** * SimpleOptionMap is a very basic command-line option container. The keys of the option container @@ -147,6 +148,7 @@ public void addOptions(Iterable newOptions) { * * @return a list of the string representations of the options in this object */ + @SideEffectFree public List getOptionsAsList() { return TestUtilities.optionMapToList(options); } diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/TestUtilities.java b/framework-test/src/main/java/org/checkerframework/framework/test/TestUtilities.java index 6f32b83b046f..60072dc711b3 100644 --- a/framework-test/src/main/java/org/checkerframework/framework/test/TestUtilities.java +++ b/framework-test/src/main/java/org/checkerframework/framework/test/TestUtilities.java @@ -27,6 +27,7 @@ import javax.tools.ToolProvider; import org.checkerframework.checker.nullness.qual.NonNull; import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.dataflow.qual.SideEffectFree; import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.SystemUtil; import org.junit.Assert; @@ -371,6 +372,8 @@ public static File findComparisonFile(File testFile) { * @param options an option map * @return return a list of option names */ + @SideEffectFree + @SuppressWarnings("purity") // adds only to a newly allocated list public static List optionMapToList(Map options) { List optionList = new ArrayList<>(options.size() * 2); From 3410fa552d151c90f4bb545e76fe3e7d4bc8eab4 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Mon, 21 Sep 2026 12:18:00 -0700 Subject: [PATCH 05/10] Make annotationName and compareByName @SideEffectFree rather than @Pure annotationName returns `elm.getQualifiedName().toString()`, a freshly built string, so it is not deterministic in the sense @Deterministic requires. The annotated JDK records that rule in a @CFComment on Object.toString(): such a method "returns a string that differs according to ==, and @Deterministic requires that the results of two calls of the method are ==." compareByName is weakened for the same reason, because it compares the results of two annotationName calls. Weakening it cascades no further: areSameByName(AnnotationMirror, AnnotationMirror) has no purity annotation, and compareAnnotationMirrors already needs its own suppression for the local TreeSet that it builds. This removes a suppression rather than adding one. The @Pure annotation on annotationName required suppressing the determinism warning on its own body, which amounted to documenting that the annotation was not true; the accurate annotation needs no suppression at all. Verified that nothing regresses: `typecheck-part1` and `typecheck-part2` (all nine checkers) pass with no errors for every subproject that runs checkPurity, and `checkNullness` still passes for framework and checker, which is where the weaker specification could have cost type refinement. Co-Authored-By: Claude Opus 5 --- .../checkerframework/javacutil/AnnotationUtils.java | 13 +++---------- 1 file changed, 3 insertions(+), 10 deletions(-) diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java index 388ec356b280..118cadd0e653 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java @@ -71,21 +71,14 @@ private AnnotationUtils() { * @param annotation the annotation whose name to return * @return the fully-qualified name of an annotation as a String */ - @Pure + @SideEffectFree public static @CanonicalName String annotationName(AnnotationMirror annotation) { if (annotation instanceof AnnotationBuilder.CheckerFrameworkAnnotationMirror cfam) { return cfam.annotationName; } DeclaredType annoType = annotation.getAnnotationType(); TypeElement elm = (TypeElement) annoType.asElement(); - // Name.toString() returns a String that is `equals` to, but not `==` to, the result of any - // previous call, so this method is not deterministic in the strict sense that @Deterministic - // requires. Every client compares annotation names by content, so @Pure is the useful - // specification. - @SuppressWarnings({ - "signature:assignment", // JDK needs annotations - "purity" // Name.toString() returns a fresh but always-equal String - }) + @SuppressWarnings("signature:assignment") // JDK needs annotations @CanonicalName String name = elm.getQualifiedName().toString(); return name; } @@ -158,7 +151,7 @@ public static boolean areSame(AnnotationMirror a1, AnnotationMirror a2) { * @see #areSame(AnnotationMirror, AnnotationMirror) */ @EqualsMethod - @Pure + @SideEffectFree public static int compareByName(AnnotationMirror a1, AnnotationMirror a2) { if (a1 == a2) { return 0; From f8af5206836550b028b0b04d07f3e3a41c58c7b3 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Tue, 22 Sep 2026 08:27:11 -0700 Subject: [PATCH 06/10] Remove changelog. --- docs/CHANGELOG.md | 4 ---- 1 file changed, 4 deletions(-) diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 501f368d02a1..04ceacd097aa 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -14,10 +14,6 @@ New `wpi2.sh` script does whole-program inference, but requires buildfile edits. The Purity Checker has been improved, so `-AcheckPurityAnnotations` may issue warnings that it did not previously. -Running the Purity Checker on its own (`-processor -org.checkerframework.framework.util.PurityChecker`) implies -`-AcheckPurityAnnotations`, which no longer needs to be supplied explicitly. - ### Changes for type system implementers `JavaParserUtil`: moved `DEFAULT_LANGUAGE_LEVEL`, `parseCompilationUnit()`, From 7b8e182f9004c55e4ebf244a34a92b21c3b12eb8 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Wed, 23 Sep 2026 09:11:12 -0700 Subject: [PATCH 07/10] Annotate Issue579 constructor as @SideEffectFree Comparator.thenComparing is @SideEffectFree in the annotated JDK, so the overriding method in Issue579 inherits that annotation and may only call side-effect-free constructors. --- checker/tests/nullness/java8/Issue579.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/checker/tests/nullness/java8/Issue579.java b/checker/tests/nullness/java8/Issue579.java index a01ac4940300..70510d6bae56 100644 --- a/checker/tests/nullness/java8/Issue579.java +++ b/checker/tests/nullness/java8/Issue579.java @@ -2,11 +2,13 @@ // https://github.com/typetools/checker-framework/issues/579 import java.util.Comparator; +import org.checkerframework.dataflow.qual.SideEffectFree; public class Issue579 implements Comparator { private final Comparator real; @SuppressWarnings("unchecked") + @SideEffectFree Issue579(Comparator real) { this.real = (Comparator) real; } From 74595feb52a1ca7ec0472701ae62ad05a7655dc9 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Wed, 23 Sep 2026 09:35:54 -0700 Subject: [PATCH 08/10] Add purity annotations so javacutil and framework-test pass the Purity Checker Methods annotated @SideEffectsOnly are now checked, so their callees need purity annotations. --- .../test/diagnostics/DiagnosticKind.java | 2 ++ .../diagnostics/JavaDiagnosticReader.java | 3 +++ .../test/diagnostics/TestDiagnostic.java | 4 ++++ .../test/diagnostics/TestDiagnosticLine.java | 2 ++ .../test/diagnostics/TestDiagnosticUtils.java | 19 ++++++++++++++++++- .../javacutil/AnnotationMirrorSet.java | 2 ++ .../javacutil/AnnotationUtils.java | 7 +++++++ .../javacutil/TypesUtils.java | 2 ++ 8 files changed, 40 insertions(+), 1 deletion(-) diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/DiagnosticKind.java b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/DiagnosticKind.java index 422e7e8794f1..566c9dec8ffa 100644 --- a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/DiagnosticKind.java +++ b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/DiagnosticKind.java @@ -3,6 +3,7 @@ import java.util.LinkedHashMap; import java.util.Map; import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.dataflow.qual.Pure; /** The kinds of errors that can be encountered during typechecking. */ public enum DiagnosticKind { @@ -31,6 +32,7 @@ public enum DiagnosticKind { } /** Convert a string as it would appear in error messages or source code into a DiagnosticKind. */ + @Pure public static @Nullable DiagnosticKind fromParseString(String parseStr) { return stringToCategory.get(parseStr); } diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/JavaDiagnosticReader.java b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/JavaDiagnosticReader.java index a2203acd4f97..a3b867c244a6 100644 --- a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/JavaDiagnosticReader.java +++ b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/JavaDiagnosticReader.java @@ -18,6 +18,7 @@ import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.checker.nullness.qual.RequiresNonNull; import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.dataflow.qual.SideEffectFree; import org.checkerframework.dataflow.qual.SideEffectsOnly; /** @@ -145,6 +146,7 @@ private interface StringToTestDiagnosticLine { * @param lineNumber the line number of the line * @return TestDiagnosticLine corresponding to {@code line} */ + @SideEffectFree TestDiagnosticLine createTestDiagnosticLine(String filename, String line, long lineNumber); } @@ -268,6 +270,7 @@ public TestDiagnosticLine next() { * @throws IOException if there is trouble while reading */ @RequiresNonNull("reader") + @SideEffectsOnly("this") /*package-private*/ void advance(@UnknownInitialization JavaDiagnosticReader this) throws IOException { nextLine = reader.readLine(); diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnostic.java b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnostic.java index 7d186475eae9..5bff9aa409e7 100644 --- a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnostic.java +++ b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnostic.java @@ -2,6 +2,8 @@ import java.util.Objects; import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.dataflow.qual.SideEffectFree; /** * Represents an expected error/warning message in a Java test file or an error/warning reported by @@ -44,6 +46,7 @@ public class TestDiagnostic { * @param isFixable true if this diagnostic should no longer be reported after whole-program * inference */ + @SideEffectFree public TestDiagnostic( String filename, long lineNumber, @@ -63,6 +66,7 @@ public String getFilename() { return filename; } + @Pure public long getLineNumber() { return lineNumber; } diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnosticLine.java b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnosticLine.java index 7c12461db61d..37a5a63ace31 100644 --- a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnosticLine.java +++ b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnosticLine.java @@ -1,6 +1,7 @@ package org.checkerframework.framework.test.diagnostics; import java.util.List; +import org.checkerframework.dataflow.qual.SideEffectFree; /** Represents a list of TestDiagnostics, which was read from a one line of a file. */ public class TestDiagnosticLine { @@ -9,6 +10,7 @@ public class TestDiagnosticLine { private final String originalLine; private final List diagnostics; + @SideEffectFree public TestDiagnosticLine( String filename, long lineNumber, String originalLine, List diagnostics) { this.filename = filename; diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnosticUtils.java b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnosticUtils.java index 011fecb84c5f..ef4012663905 100644 --- a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnosticUtils.java +++ b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnosticUtils.java @@ -12,6 +12,7 @@ import javax.tools.JavaFileObject; import org.checkerframework.checker.nullness.qual.EnsuresNonNullIf; import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.dataflow.qual.SideEffectFree; import org.checkerframework.javacutil.BugInCF; import org.plumelib.util.CollectionsP; @@ -97,6 +98,7 @@ private TestDiagnosticUtils() { * @param stringFromDiagnosticFile a single diagnostic string to parse * @return a new TestDiagnostic */ + @SideEffectFree public static TestDiagnostic fromDiagnosticFileString(String stringFromDiagnosticFile) { return fromPatternMatching( DIAGNOSTIC_FILE_PATTERN, @@ -116,6 +118,7 @@ public static TestDiagnostic fromDiagnosticFileString(String stringFromDiagnosti * @param stringFromJavaFile the string containing the diagnostic * @return a new TestDiagnostic */ + @SideEffectFree public static TestDiagnostic fromJavaFileComment( String filename, long lineNumber, String stringFromJavaFile) { return fromPatternMatching( @@ -155,6 +158,7 @@ public static TestDiagnostic fromJavaxToolsDiagnostic(String diagnosticString) { * @param stringFromJavaFile the string containing the diagnostic * @return a new TestDiagnostic */ + @SideEffectFree public static TestDiagnostic fromJSpecifyFileComment( String filename, long lineNumber, String stringFromJavaFile) { return new TestDiagnostic( @@ -177,6 +181,7 @@ public static TestDiagnostic fromJSpecifyFileComment( * @param diagnosticString the string to parse * @return a diagnostic parsed from the given string */ + @SideEffectFree @SuppressWarnings({ "nullness", // TODO: regular expression group access "regex:group.count" // group count varies by pattern; callers ensure correct group counts @@ -350,6 +355,7 @@ private static boolean retainAllLines(String message) { * @param category a category string that may be prepended with "fixable-" * @return the category and whether it was prepended with "fixable-" */ + @SideEffectFree private static CategoryAndFixable categoryAndFixable(String category) { String fixable = "fixable-"; boolean isFixable = category.startsWith(fixable); @@ -370,12 +376,17 @@ private static CategoryAndFixable categoryAndFixable(String category) { * @param kind the diagnostic category * @param isFixable true if the category string was prepended with "fixable-" */ - private record CategoryAndFixable(DiagnosticKind kind, boolean isFixable) {} + private record CategoryAndFixable(DiagnosticKind kind, boolean isFixable) { + /** Creates a CategoryAndFixable. */ + @SideEffectFree + CategoryAndFixable {} + } /** * Returns true if this line in a Java file indicates an expected diagnostic that might be * continued on the next line. */ + @SideEffectFree public static boolean isJavaDiagnosticLineStart(String originalLine) { String trimmedLine = originalLine.trim(); return trimmedLine.startsWith("// ::") || trimmedLine.startsWith("// warning:"); @@ -395,6 +406,7 @@ public static boolean isJavaDiagnosticLineStart(String originalLine) { * (to avoid false positive matches, such as when "// ::" is commented out in source code). It * could be extended in the future if such an extension is necessary. */ + @SideEffectFree public static String handleEndOfLineJavaDiagnostic(String originalLine) { int curlyIndex = originalLine.indexOf("{ // ::"); if (curlyIndex == -1) { @@ -406,6 +418,7 @@ public static String handleEndOfLineJavaDiagnostic(String originalLine) { /** Return true if this line in a Java file continues an expected diagnostic. */ @EnsuresNonNullIf(result = true, expression = "#1") + @SideEffectFree public static boolean isJavaDiagnosticLineContinuation(@Nullable String originalLine) { if (originalLine == null) { return false; @@ -421,6 +434,7 @@ public static boolean isJavaDiagnosticLineContinuation(@Nullable String original * Returns the continuation part. The argument is such that {@link * #isJavaDiagnosticLineContinuation} returns true. */ + @SideEffectFree public static String continuationPart(String originalLine) { return originalLine.trim().substring(2).trim(); } @@ -431,6 +445,8 @@ public static String continuationPart(String originalLine) { *

The input {@code line} is possibly the concatenation of multiple source lines, if the * diagnostic was split across lines in the source code. */ + @SideEffectFree + @SuppressWarnings("purity") // CollectionsP.mapList is side-effect-free but unannotated public static TestDiagnosticLine fromJavaSourceLine( String filename, String line, long lineNumber) { String trimmedLine = line.trim(); @@ -475,6 +491,7 @@ public static TestDiagnosticLine fromJavaSourceLine( } /** Convert a line in a DiagnosticFile to a TestDiagnosticLine. */ + @SideEffectFree public static TestDiagnosticLine fromDiagnosticFileLine(String diagnosticLine) { String trimmedLine = diagnosticLine.trim(); if (trimmedLine.startsWith("#") || trimmedLine.isEmpty()) { diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorSet.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorSet.java index ecb0fcca6b83..f22d1fe49df5 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorSet.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationMirrorSet.java @@ -14,6 +14,7 @@ import org.checkerframework.checker.nullness.qual.PolyNull; import org.checkerframework.common.returnsreceiver.qual.This; import org.checkerframework.dataflow.qual.Pure; +import org.checkerframework.dataflow.qual.SideEffectFree; import org.checkerframework.dataflow.qual.SideEffectsOnly; import org.plumelib.util.DeepCopyable; @@ -46,6 +47,7 @@ public class AnnotationMirrorSet // Constructors and factory methods /** Default constructor. */ + @SideEffectFree public AnnotationMirrorSet() {} // TODO: Should this be an unmodifiable set? diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java index 90f690bb32e3..53ff684d091b 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationUtils.java @@ -128,6 +128,7 @@ private AnnotationUtils() { * @return true iff a1 and a2 are the same annotation */ @EqualsMethod + @SideEffectFree public static boolean areSame(AnnotationMirror a1, AnnotationMirror a2) { if (a1 == a2) { return true; @@ -188,6 +189,7 @@ public static int compareByName(AnnotationMirror a1, AnnotationMirror a2) { * @see #areSame(AnnotationMirror, AnnotationMirror) */ @EqualsMethod + @SideEffectFree public static boolean areSameByName(AnnotationMirror a1, AnnotationMirror a2) { if (a1 == a2) { return true; @@ -287,6 +289,7 @@ public static boolean containsSame( * @return AnnotationMirror with the same class as {@code anno} iff c contains anno, according to * areSame; otherwise, {@code null} */ + @SideEffectFree public static @Nullable AnnotationMirror getSame( Collection c, AnnotationMirror anno) { for (AnnotationMirror an : c) { @@ -446,6 +449,7 @@ public static int compareAnnotationMirrors(AnnotationMirror a1, AnnotationMirror * @return -1 if the first is lesser, 0 if they are the same, or 1 if the first is greater */ @CompareToMethod + @SideEffectFree private static int compareAnnotationValue(AnnotationValue av1, AnnotationValue av2) { if (av1 == av2) { return 0; @@ -466,6 +470,7 @@ private static int compareAnnotationValue(AnnotationValue av1, AnnotationValue a * than, equal to, or greater than the second annotation value */ @CompareToMethod + @SideEffectFree private static int compareAnnotationValueValue(@Nullable Object val1, @Nullable Object val2) { if (val1 == val2) { return 0; @@ -1191,6 +1196,7 @@ public static > T[] annotationValueListToEnumArray( * @return true if the two annotations have the same elements (fields) */ @EqualsMethod + @SideEffectFree private static boolean sameElementValues(AnnotationMirror am1, AnnotationMirror am2) { // This method might return true even if these maps differ, because of default values. @@ -1261,6 +1267,7 @@ private static boolean sameElementValues(AnnotationMirror am1, AnnotationMirror * @param av2 the second AnnotationValue to compare * @return true if the two annotation values are the same */ + @SideEffectFree public static boolean sameAnnotationValue(AnnotationValue av1, AnnotationValue av2) { return compareAnnotationValue(av1, av2) == 0; } diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java index 0ad276bb14a1..71b38b3a3db2 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TypesUtils.java @@ -48,6 +48,7 @@ import org.checkerframework.checker.signature.qual.CanonicalNameOrEmpty; import org.checkerframework.checker.signature.qual.DotSeparatedIdentifiers; import org.checkerframework.checker.signature.qual.FullyQualifiedName; +import org.checkerframework.dataflow.qual.SideEffectFree; import org.plumelib.util.CollectionsP; import org.plumelib.util.ImmutableTypes; import org.plumelib.util.StringsP; @@ -296,6 +297,7 @@ public static TypeMirror getInnermostComponentType(ArrayType arrayType) { * @param t2 the second type to test * @return true if the arguments are the same declared types */ + @SideEffectFree public static boolean areSameDeclaredTypes(Type.ClassType t1, Type.ClassType t2) { // Do a cheaper test first if (t1.tsym.name != t2.tsym.name) { From c80e9e71f43b2f565d6770922bca19288a8df385 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Wed, 23 Sep 2026 09:38:36 -0700 Subject: [PATCH 09/10] Skip javadoc. --- SKIP-REQUIRE-JAVADOC | 0 1 file changed, 0 insertions(+), 0 deletions(-) create mode 100644 SKIP-REQUIRE-JAVADOC diff --git a/SKIP-REQUIRE-JAVADOC b/SKIP-REQUIRE-JAVADOC new file mode 100644 index 000000000000..e69de29bb2d1 From e94e6055169c6ac2cfdb307b4c47ee80aeaf3cff Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Wed, 23 Sep 2026 12:28:30 -0700 Subject: [PATCH 10/10] Remove expected error now that Record() is @SideEffectFree --- checker/tests/lock-records/LockRecord.java | 1 - 1 file changed, 1 deletion(-) diff --git a/checker/tests/lock-records/LockRecord.java b/checker/tests/lock-records/LockRecord.java index d2bbfcfec397..4102038c2c5d 100644 --- a/checker/tests/lock-records/LockRecord.java +++ b/checker/tests/lock-records/LockRecord.java @@ -3,7 +3,6 @@ public record LockRecord(String s, ReentrantLock lock) { @LockingFree - // :: error: [method.guarantee.violated] public LockRecord { // :: error: [method.guarantee.violated] lock.lock();