Make checkPurity pass for javacutils.

build.gradle

@@ -1201,7 +1201,15 @@ subprojects {
       description = "Run the Checker Framework on itself (part 1)"
       group = "Verification"
       dependsOn("checkCompilerMessages", "checkFormatter", "checkInterning", "checkOptional")
-      // Can't run "checkPurity" because it issues too many warnings.
+      // 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")
+      }
     }
     tasks.register("typecheck-part2") {
       description = "Run the Checker Framework on itself (part 2)"

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);

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());

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);

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();

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();

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<T> implements Comparator<T> {
   private final Comparator<T> real;
 
   @SuppressWarnings("unchecked")
+  @SideEffectFree
   Issue579(Comparator<? super T> real) {
     this.real = (Comparator<T>) real;
   }

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<File> getDiagnosticFiles() {
     return options;
   }
 
+  @SideEffectFree
   @Override
   public List<String> getFlatOptions() {
     return TestUtilities.optionMapToList(options);

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<String> newOptions) {
    *
    * @return a list of the string representations of the options in this object
    */
+  @SideEffectFree
   public List<String> getOptionsAsList() {
     return TestUtilities.optionMapToList(options);
   }

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<String> optionMapToList(Map<String, @Nullable String> options) {
     List<String> optionList = new ArrayList<>(options.size() * 2);
 

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);
   }

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();

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;
   }

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<TestDiagnostic> diagnostics;
 
+  @SideEffectFree
   public TestDiagnosticLine(
       String filename, long lineNumber, String originalLine, List<TestDiagnostic> diagnostics) {
     this.filename = filename;

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) {
    * <p>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()) {

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());
   }