New command-line option -AassumePureGetters

checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java

@@ -386,7 +386,8 @@ public TransferResult<NullnessValue, NullnessStore> visitMethodInvocation(
     MethodInvocationTree tree = n.getTree();
     ExecutableElement method = TreeUtils.elementFromUse(tree);
 
-    boolean isMethodSideEffectFree = PurityUtils.isSideEffectFree(atypeFactory, method);
+    boolean isMethodSideEffectFree =
+        atypeFactory.isSideEffectFree(method) || PurityUtils.isSideEffectFree(atypeFactory, method);
     Node receiver = n.getTarget().getReceiver();
     if (nonNullAssumptionAfterInvocation
         || isMethodSideEffectFree

checker/src/test/java/org/checkerframework/checker/test/junit/OptionalPureGettersTest.java

@@ -0,0 +1,28 @@
+package org.checkerframework.checker.test.junit;
+
+import java.io.File;
+import java.util.List;
+import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest;
+import org.junit.runners.Parameterized.Parameters;
+
+/** JUnit tests for the Optional Checker, which has the {@code @Present} annotation. */
+public class OptionalPureGettersTest extends CheckerFrameworkPerDirectoryTest {
+
+  /**
+   * Create an OptionalPureGettersTest.
+   *
+   * @param testFiles the files containing test code, which will be type-checked
+   */
+  public OptionalPureGettersTest(List<File> testFiles) {
+    super(
+        testFiles,
+        org.checkerframework.checker.optional.OptionalChecker.class,
+        "optional",
+        "-AassumePureGetters");
+  }
+
+  @Parameters
+  public static String[] getTestDirs() {
+    return new String[] {"optional-pure-getters"};
+  }
+}

checker/tests/optional-pure-getters/PureGetterTest.java

@@ -0,0 +1,76 @@
+import java.util.Optional;
+
+class PureGetterTest {
+
+  @SuppressWarnings("optional.field")
+  Optional<String> field;
+
+  // This method will be treated as @Pure because of -AassumePureGetters.
+  Optional<String> getOptional() {
+    return null;
+  }
+
+  Optional<String> otherOptional() {
+    return null;
+  }
+
+  void sideEffect() {}
+
+  void foo() {
+    if (field.isPresent()) {
+      field.get();
+    }
+    if (field.isPresent()) {
+      sideEffect();
+      // :: error: method.invocation
+      field.get();
+    }
+    if (field.isPresent()) {
+      getOptional();
+      field.get();
+    }
+    if (field.isPresent()) {
+      otherOptional();
+      // :: error: method.invocation
+      field.get();
+    }
+
+    if (getOptional().isPresent()) {
+      getOptional().get();
+    }
+    if (getOptional().isPresent()) {
+      sideEffect();
+      // :: error: method.invocation
+      getOptional().get();
+    }
+    if (getOptional().isPresent()) {
+      getOptional();
+      getOptional().get();
+    }
+    if (getOptional().isPresent()) {
+      otherOptional();
+      // :: error: method.invocation
+      getOptional().get();
+    }
+
+    if (otherOptional().isPresent()) {
+      // BUG: https://github.com/typetools/checker-framework/issues/6291 error: method.invocation
+      otherOptional().get();
+    }
+    if (otherOptional().isPresent()) {
+      sideEffect();
+      // :: error: method.invocation
+      otherOptional().get();
+    }
+    if (otherOptional().isPresent()) {
+      getOptional();
+      // BUG: https://github.com/typetools/checker-framework/issues/6291 error: method.invocation
+      otherOptional().get();
+    }
+    if (otherOptional().isPresent()) {
+      otherOptional();
+      // :: error: method.invocation
+      otherOptional().get();
+    }
+  }
+}

dataflow/src/main/java/org/checkerframework/dataflow/expression/MethodCall.java

@@ -88,7 +88,7 @@ public boolean containsOfClass(Class<? extends JavaExpression> clazz) {
 
   @Override
   public boolean isDeterministic(AnnotationProvider provider) {
-    return PurityUtils.isDeterministic(provider, method)
+    return (PurityUtils.isDeterministic(provider, method) || provider.isDeterministic(method))
         && listIsDeterministic(arguments, provider);
   }
 

dataflow/src/main/java/org/checkerframework/dataflow/util/PurityChecker.java

@@ -49,16 +49,19 @@ public class PurityChecker {
    * @param annoProvider the annotation provider
    * @param assumeSideEffectFree true if all methods should be assumed to be @SideEffectFree
    * @param assumeDeterministic true if all methods should be assumed to be @Deterministic
+   * @param assumePureGetters true if all getter methods should be assumed to be @Pure
    * @return information about whether the given statement is side-effect-free, deterministic, or
    *     both
    */
   public static PurityResult checkPurity(
       TreePath statement,
       AnnotationProvider annoProvider,
       boolean assumeSideEffectFree,
-      boolean assumeDeterministic) {
+      boolean assumeDeterministic,
+      boolean assumePureGetters) {
     PurityCheckerHelper helper =
-        new PurityCheckerHelper(annoProvider, assumeSideEffectFree, assumeDeterministic);
+        new PurityCheckerHelper(
+            annoProvider, assumeSideEffectFree, assumeDeterministic, assumePureGetters);
     helper.scan(statement, null);
     return helper.purityResult;
   }
@@ -204,20 +207,29 @@ protected static class PurityCheckerHelper extends TreePathScanner<Void, Void> {
      */
     private final boolean assumeDeterministic;
 
+    /**
+     * True if all getter methods should be assumed to be @SideEffectFree and @Deterministic, for
+     * the purposes of org.checkerframework.dataflow analysis.
+     */
+    private final boolean assumePureGetters;
+
     /**
      * Create a PurityCheckerHelper.
      *
      * @param annoProvider the annotation provider
      * @param assumeSideEffectFree true if all methods should be assumed to be @SideEffectFree
      * @param assumeDeterministic true if all methods should be assumed to be @Deterministic
+     * @param assumePureGetters true if getter methods should be assumed to be @Pure
      */
     public PurityCheckerHelper(
         AnnotationProvider annoProvider,
         boolean assumeSideEffectFree,
-        boolean assumeDeterministic) {
+        boolean assumeDeterministic,
+        boolean assumePureGetters) {
       this.annoProvider = annoProvider;
       this.assumeSideEffectFree = assumeSideEffectFree;
       this.assumeDeterministic = assumeDeterministic;
+      this.assumePureGetters = assumePureGetters;
     }
 
     @Override
@@ -237,7 +249,8 @@ public Void visitMethodInvocation(MethodInvocationTree tree, Void ignore) {
         purityResult.addNotBothReason(tree, "call");
       } else {
         EnumSet<Pure.Kind> purityKinds =
-            (assumeDeterministic && assumeSideEffectFree)
+            ((assumeDeterministic && assumeSideEffectFree)
+                    || (assumePureGetters && ElementUtils.isGetter(elt)))
                 // Avoid computation if not necessary
                 ? detAndSeFree
                 : PurityUtils.getPurityKinds(annoProvider, elt);
@@ -294,6 +307,7 @@ public Void visitNewClass(NewClassTree tree, Void ignore) {
       boolean deterministic =
           assumeDeterministic
               || okThrowDeterministic
+              // No need to check assumePureGetters because a constructor is never a getter.
               || PurityUtils.isDeterministic(annoProvider, ctorElement);
       boolean sideEffectFree =
           assumeSideEffectFree || PurityUtils.isSideEffectFree(annoProvider, ctorElement);

docs/CHANGELOG.md

@@ -3,6 +3,9 @@ Version 3.40.1 (December 1, 2023)
 
 **User-visible changes:**
 
+New command-line options:
+  -AassumePureGetters Unsoundly assume that every getter method is pure
+
 **Implementation details:**
 
 Added method `isDeterministic()` to the `AnnotationProvider` interface.

docs/manual/introduction.tex

@@ -578,9 +578,9 @@
   Suppress all errors and warnings within the definition of a given class
   --- or everywhere except within the definition of a given class.  See
   Section~\ref{askipdefs}.
-\item \<-AassumeSideEffectFree>, \<-AassumeDeterministic>, \<-AassumePure>
+\item \<-AassumeSideEffectFree>, \<-AassumeDeterministic>, \<-AassumePure>, \<-AassumePureGetters>
   Unsoundly assume that every method is side-effect-free, deterministic, or
-  both.
+  both; or that every getter method is pure.
   See Section~\ref{purity-suppress-warnings} and
   Section~\ref{type-refinement-purity}.
 \item \<-AassumeAssertionsAreEnabled>, \<-AassumeAssertionsAreDisabled>

docs/manual/purity-checker.tex

@@ -105,10 +105,16 @@
 \sectionAndLabel{Suppressing warnings}{purity-suppress-warnings}
 
 The command-line options \<-AassumeSideEffectFree>,
-\<-AassumeDeterministic>, and \<-AassumePure> make the Checker Framework unsoundly
-assume that \emph{every} called method is side-effect-free, is
+\<-AassumeDeterministic>, and \<-AassumePure> make the Checker Framework
+unsoundly assume that \emph{every} called method is side-effect-free, is
 deterministic, or is both, respectively.
 
+The command-line option \<-AassumePureGetters> makes the Checker Framework
+unsoundly assume that every getter method is side-effect-free and
+deterministic.  For the purposes of \<-AassumePureGetters>, a getter method
+is defined as an instance method with no formal parameters, whose name
+starts with ``get'' followed by an uppercase letter.
+
 This can make
 flow-sensitive type refinement much more effective, since method calls will
 not cause the analysis to discard information that it has learned.
@@ -120,6 +126,10 @@
 \item
   You are using the Checker Framework to find bugs but not to give a
   guarantee that no more errors exist of the given type.
+\item
+  You are working with an unannotated library that makes the given
+  assumptions, in which case (say) using \<-AassumePureGetters> is easier
+  than writing stub files for all the library's getter methods.
 \end{itemize}
 
 

framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java

@@ -261,6 +261,9 @@ public class BaseTypeVisitor<Factory extends GenericAnnotatedTypeFactory<?, ?, ?
   /** True if "-AassumeDeterministic" or "-aassumePure" was passed on the command line. */
   private final boolean assumeDeterministic;
 
+  /** True if "-AassumePureGetters" was passed on the command line. */
+  public final boolean assumePureGetters;
+
   /** True if "-AcheckCastElementType" was passed on the command line. */
   private final boolean checkCastElementType;
 
@@ -310,6 +313,7 @@ protected BaseTypeVisitor(BaseTypeChecker checker, @Nullable Factory typeFactory
         checker.hasOption("assumeSideEffectFree") || checker.hasOption("assumePure");
     assumeDeterministic =
         checker.hasOption("assumeDeterministic") || checker.hasOption("assumePure");
+    assumePureGetters = checker.hasOption("assumePureGetters");
     checkCastElementType = checker.hasOption("checkCastElementType");
     conservativeUninferredTypeArguments = checker.hasOption("conservativeUninferredTypeArguments");
     warnRedundantAnnotations = checker.hasOption("warnRedundantAnnotations");
@@ -1093,7 +1097,9 @@ protected void checkPurity(MethodTree tree) {
     if (body == null) {
       r = new PurityResult();
     } else {
-      r = PurityChecker.checkPurity(body, atypeFactory, assumeSideEffectFree, assumeDeterministic);
+      r =
+          PurityChecker.checkPurity(
+              body, atypeFactory, assumeSideEffectFree, assumeDeterministic, assumePureGetters);
     }
     if (!r.isPure(kinds)) {
       reportPurityErrors(r, tree, kinds);

framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java

@@ -41,6 +41,7 @@
 import org.checkerframework.javacutil.AnnotationBuilder;
 import org.checkerframework.javacutil.AnnotationUtils;
 import org.checkerframework.javacutil.BugInCF;
+import org.checkerframework.javacutil.ElementUtils;
 import org.plumelib.util.CollectionsPlume;
 import org.plumelib.util.IPair;
 import org.plumelib.util.ToStringComparator;
@@ -112,6 +113,9 @@ public Map<FieldAccess, V> getFieldValues() {
   /** True if -AassumeSideEffectFree or -AassumePure was passed on the command line. */
   private final boolean assumeSideEffectFree;
 
+  /** True if -AassumePureGetters was passed on the command line. */
+  private final boolean assumePureGetters;
+
   /** The unique ID for the next-created object. */
   private static final AtomicLong nextUid = new AtomicLong(0);
 
@@ -145,6 +149,7 @@ protected CFAbstractStore(CFAbstractAnalysis<V, S, ?> analysis, boolean sequenti
     assumeSideEffectFree =
         analysis.checker.hasOption("assumeSideEffectFree")
             || analysis.checker.hasOption("assumePure");
+    assumePureGetters = analysis.checker.hasOption("assumePureGetters");
   }
 
   /**
@@ -162,6 +167,7 @@ protected CFAbstractStore(CFAbstractStore<V, S> other) {
     classValues = new HashMap<>(other.classValues);
     sequentialSemantics = other.sequentialSemantics;
     assumeSideEffectFree = other.assumeSideEffectFree;
+    assumePureGetters = other.assumePureGetters;
   }
 
   /**
@@ -237,7 +243,11 @@ public void updateForMethodCall(
         (GenericAnnotatedTypeFactory<V, S, ?, ?>) atypeFactory;
 
     // Case 1: The method is side-effect-free.
-    if (!(assumeSideEffectFree || atypeFactory.isSideEffectFree(method))) {
+    boolean hasSideEffect =
+        !(assumeSideEffectFree
+            || (assumePureGetters && ElementUtils.isGetter(method))
+            || atypeFactory.isSideEffectFree(method));
+    if (hasSideEffect) {
 
       boolean sideEffectsUnrefineAliases = gatypeFactory.sideEffectsUnrefineAliases;
 

framework/src/main/java/org/checkerframework/framework/source/SourceChecker.java

@@ -125,6 +125,8 @@
   "assumeSideEffectFree",
   "assumeDeterministic",
   "assumePure",
+  // Unsoundly assume getter methods have no side effects and are deterministic.
+  "assumePureGetters",
 
   // Whether to assume that assertions are enabled or disabled
   // org.checkerframework.framework.flow.CFCFGBuilder.CFCFGBuilder
@@ -747,7 +749,7 @@ public Trees getTreeUtils() {
    */
   public AnnotationProvider getAnnotationProvider() {
     throw new UnsupportedOperationException(
-        "getAnnotationProvider is not implemented for this class.");
+        "getAnnotationProvider is not implemented for " + this.getClass().getSimpleName() + ".");
   }
 
   /**

framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java

@@ -379,6 +379,12 @@ public class AnnotatedTypeFactory implements AnnotationProvider {
    */
   private final boolean assumeDeterministic;
 
+  /**
+   * True if all getter methods should be assumed to be @Pure, for the purposes of
+   * org.checkerframework.dataflow analysis.
+   */
+  private final boolean assumePureGetters;
+
   /** True if -AmergeStubsWithSource was provided on the command line. */
   private final boolean mergeStubsWithSource;
 
@@ -571,6 +577,7 @@ public AnnotatedTypeFactory(BaseTypeChecker checker) {
         checker.hasOption("assumeSideEffectFree") || checker.hasOption("assumePure");
     this.assumeDeterministic =
         checker.hasOption("assumeDeterministic") || checker.hasOption("assumePure");
+    this.assumePureGetters = checker.hasOption("assumePureGetters");
 
     this.trees = Trees.instance(processingEnv);
     this.elements = processingEnv.getElementUtils();
@@ -5800,7 +5807,7 @@ public boolean isImmutable(TypeMirror type) {
 
   @Override
   public boolean isSideEffectFree(ExecutableElement methodElement) {
-    if (assumeSideEffectFree) {
+    if (assumeSideEffectFree || (assumePureGetters && ElementUtils.isGetter(methodElement))) {
       return true;
     }
     if (ElementUtils.isRecordAccessor(methodElement)
@@ -5819,7 +5826,7 @@ public boolean isSideEffectFree(ExecutableElement methodElement) {
 
   @Override
   public boolean isDeterministic(ExecutableElement methodElement) {
-    if (assumeDeterministic) {
+    if (assumeDeterministic || (assumePureGetters && ElementUtils.isGetter(methodElement))) {
       return true;
     }
     if (ElementUtils.isRecordAccessor(methodElement)