Make the Purity Checker always pass -AcheckPurityAnnotations

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

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
+both options.
 
 The Checker Framework can infer purity annotations.
 If you supply the command-line option \<-AsuggestPureMethods>, then the
@@ -61,9 +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
+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.

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,25 @@
  *     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.
+
+  /** Creates a PurityChecker. */
+  public PurityChecker() {}
+
+  /**
+   * {@inheritDoc}
+   *
+   * <p>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<String, String> getOptions() {
+    Map<String, String> options = super.getOptions();
+    if (!options.containsKey("checkPurityAnnotations")) {
+      options.put("checkPurityAnnotations", "true");
+    }
+    return options;
+  }
 }

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<File> testFiles) {
+    super(testFiles, PurityChecker.class, "purity-checker");
+  }
+
+  @Parameters
+  public static String[] getTestDirs() {
+    return new String[] {"purity-checker"};
+  }
+}

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