Add @DoesNotUnrefineReceiver annotation

checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/EnsuresNonNullIf.java

@@ -84,7 +84,7 @@
   /**
    * Returns Java expression(s) that are non-null after the method returns the given result.
    *
-   * @return Java expression(s) that are non-null after the method returns the given result
+   * @return the Java expression(s) that are non-null after the method returns the given result
    * @checker_framework.manual #java-expressions-as-arguments Syntax of Java expressions
    */
   String[] expression();

checker-qual/src/main/java/org/checkerframework/dataflow/qual/DoesNotUnrefineReceiver.java

@@ -0,0 +1,31 @@
+package org.checkerframework.dataflow.qual;
+
+import java.lang.annotation.Documented;
+import java.lang.annotation.ElementType;
+import java.lang.annotation.Retention;
+import java.lang.annotation.RetentionPolicy;
+import java.lang.annotation.Target;
+
+/**
+ * At a call to a side-effecting method, the framework ordinarily discards all refined type
+ * information, since the side-effecting method might invalidate that information. This annotation
+ * indicates that, at a call to the annotated method, the receiver's type should not be unrefined.
+ * That is, a call to the method does not affect the type qualifier (in the given hierarchy).
+ *
+ * @checker_framework.manual #type-refinement-purity Side effects, determinism, purity, and
+ *     flow-sensitive analysis
+ */
+// @InheritedAnnotation cannot be written here, because "dataflow" project cannot depend on
+// "framework" project.
+@Documented
+@Retention(RetentionPolicy.RUNTIME)
+@Target({ElementType.METHOD, ElementType.CONSTRUCTOR})
+public @interface DoesNotUnrefineReceiver {
+  /**
+   * The name of the checker(s) that this annotation affects. For example, "modifiability" or
+   * "nullness". Use "allcheckers" to affect all checkers.
+   *
+   * @return the name of the checker that this annotation affects
+   */
+  String[] value();
+}

docs/CHANGELOG.md

@@ -9,6 +9,9 @@
 
 ### Implementation details
 
+New method annotation `DoesNotUnrefineReceiver`.
+Interface `AnnotationProvider` has a new method `hasDoesNotUnrefineReceiver()`.
+
 ### Closed issues
 
 ## Version 4.0.0 (2026-04-07)

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

@@ -10,6 +10,7 @@
 import java.util.StringJoiner;
 import java.util.concurrent.atomic.AtomicLong;
 import java.util.function.BinaryOperator;
+import java.util.function.Predicate;
 import javax.lang.model.element.AnnotationMirror;
 import javax.lang.model.element.ExecutableElement;
 import javax.lang.model.element.Name;
@@ -237,44 +238,71 @@ public void updateForMethodCall(
     if (hasSideEffect) {
 
       boolean sideEffectsUnrefineAliases = gatypeFactory.sideEffectsUnrefineAliases;
+      Node receiver = methodInvocationNode.getTarget().getReceiver();
+      boolean hasDoesNotUnrefineReceiver = atypeFactory.hasDoesNotUnrefineReceiver(method);
 
-      // update local variables
       // TODO: Also remove if any element/argument to the annotation is not
       // isUnmodifiableByOtherCode.  Example: @KeyFor("valueThatCanBeMutated").
+
+      // If @DoesNotUnrefineReceiver is present, compute the receiver as a JavaExpression so
+      // that it can be exempted from unrefinement in all expression categories below.
+      @Nullable JavaExpression receiverJe =
+          hasDoesNotUnrefineReceiver ? JavaExpression.fromNode(receiver) : null;
+      // Returns true if the expression should NOT be unrefined (because the method is
+      // annotated @DoesNotUnrefineReceiver and the expression is the receiver).
+      Predicate<JavaExpression> doNotUnrefine =
+          receiverJe != null ? je -> je.equals(receiverJe) : je -> false;
+
+      // Update local variables.
       if (sideEffectsUnrefineAliases) {
-        localVariableValues.entrySet().removeIf(e -> e.getKey().isModifiableByOtherCode());
+        localVariableValues
+            .entrySet()
+            .removeIf(
+                e -> {
+                  LocalVariable lv = e.getKey();
+                  return lv.isModifiableByOtherCode() && !doNotUnrefine.test(lv);
+                });
       }
 
-      // update this value
-      if (sideEffectsUnrefineAliases) {
+      // Update this value.
+      if (sideEffectsUnrefineAliases
+          && !(receiverJe instanceof ThisReference)
+          && !(receiverJe instanceof SuperReference)) {
         thisValue = null;
       }
 
-      // update field values
+      // Update field values.
       if (sideEffectsUnrefineAliases) {
-        fieldValues.entrySet().removeIf(e -> e.getKey().isModifiableByOtherCode());
+        fieldValues
+            .entrySet()
+            .removeIf(
+                (Map.Entry<FieldAccess, V> e) -> {
+                  FieldAccess fa = e.getKey();
+                  return fa.isModifiableByOtherCode() && !doNotUnrefine.test(fa);
+                });
       } else {
-        // Case 2 (unassignable fields) and case 3 (monotonic fields)
-        updateFieldValuesForMethodCall(gatypeFactory);
+        // Case 2 (unassignable fields) and case 3 (monotonic fields).
+        updateFieldValuesForMethodCall(gatypeFactory, doNotUnrefine::test);
       }
 
       // Update array values.
-      arrayValues.clear();
+      arrayValues.entrySet().removeIf(e -> !doNotUnrefine.test(e.getKey()));
 
       // Update information about method calls.
-      updateMethodCallValues();
+      methodCallExpressions
+          .entrySet()
+          .removeIf(
+              e -> {
+                MethodCall mc = e.getKey();
+                return mc.isModifiableByOtherCode() && !doNotUnrefine.test(mc);
+              });
     }
 
     // Store information about method calls if possible.
     JavaExpression methodCall = JavaExpression.fromNode(methodInvocationNode);
     replaceValue(methodCall, val);
   }
 
-  /** Update information about method calls. */
-  private void updateMethodCallValues() {
-    methodCallExpressions.keySet().removeIf(MethodCall::isModifiableByOtherCode);
-  }
-
   /**
    * Returns the new value of a field after a method call, or {@code null} if the field should be
    * removed from the store.
@@ -358,15 +386,23 @@ protected V newMonotonicFieldValueAfterMethodCall(
    * fields that have a monotonic annotation.
    *
    * @param atypeFactory AnnotatedTypeFactory of the associated checker
+   * @param doNotUnrefine if true of a field access, don't unrefine it. This predicate indicates
+   *     exceptions: fields that are not updated by this method.
    */
   private void updateFieldValuesForMethodCall(
-      GenericAnnotatedTypeFactory<V, S, ?, ?> atypeFactory) {
+      GenericAnnotatedTypeFactory<V, S, ?, ?> atypeFactory, Predicate<FieldAccess> doNotUnrefine) {
     Map<FieldAccess, V> newFieldValues = new HashMap<>(MapsP.mapCapacity(fieldValues));
     for (Map.Entry<FieldAccess, V> e : fieldValues.entrySet()) {
       FieldAccess fieldAccess = e.getKey();
       V previousValue = e.getValue();
 
-      V newValue = newFieldValueAfterMethodCall(fieldAccess, atypeFactory, previousValue);
+      V newValue;
+      boolean doNotUnrefineResult = doNotUnrefine.test(fieldAccess);
+      if (doNotUnrefineResult) {
+        newValue = previousValue;
+      } else {
+        newValue = newFieldValueAfterMethodCall(fieldAccess, atypeFactory, previousValue);
+      }
       if (newValue != null) {
         // Keep information for all hierarchies where we had a monotonic annotation.
         newFieldValues.put(fieldAccess, newValue);

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

@@ -96,6 +96,7 @@
 import org.checkerframework.common.wholeprograminference.WholeProgramInferenceJavaParserStorage;
 import org.checkerframework.common.wholeprograminference.WholeProgramInferenceJavaParserStorage.InferredDeclared;
 import org.checkerframework.common.wholeprograminference.WholeProgramInferenceScenesStorage;
+import org.checkerframework.dataflow.qual.DoesNotUnrefineReceiver;
 import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.checkerframework.framework.qual.AnnotatedFor;
 import org.checkerframework.framework.qual.EnsuresQualifier;
@@ -218,6 +219,9 @@ public class AnnotatedTypeFactory implements AnnotationProvider {
   /** The AnnotatedFor.value argument/element. */
   protected final ExecutableElement annotatedForValueElement;
 
+  /** The DoesNotUnrefineReceiver.value argument/element. */
+  protected final ExecutableElement doesNotUnrefineReceiverValueElement;
+
   /** The EnsuresQualifier.expression field/element. */
   protected final ExecutableElement ensuresQualifierExpressionElement;
 
@@ -674,6 +678,8 @@ public AnnotatedTypeFactory(BaseTypeChecker checker) {
     this.debugStubParser = checker.hasOption("stubDebug");
 
     annotatedForValueElement = TreeUtils.getMethod(AnnotatedFor.class, "value", 0, processingEnv);
+    doesNotUnrefineReceiverValueElement =
+        TreeUtils.getMethod(DoesNotUnrefineReceiver.class, "value", 0, processingEnv);
     ensuresQualifierExpressionElement =
         TreeUtils.getMethod(EnsuresQualifier.class, "expression", 0, processingEnv);
     ensuresQualifierListValueElement =
@@ -5856,6 +5862,24 @@ public boolean isDeterministic(ExecutableElement methodElement) {
     return false;
   }
 
+  @Override
+  public boolean hasDoesNotUnrefineReceiver(ExecutableElement methodElement) {
+    for (AnnotationMirror am : getDeclAnnotations(methodElement)) {
+      if (areSameByClass(am, org.checkerframework.dataflow.qual.DoesNotUnrefineReceiver.class)) {
+        List<String> typeSystems =
+            AnnotationUtils.getElementValueArray(
+                am, doesNotUnrefineReceiverValueElement, String.class);
+        for (String prefix : checker.getSuppressWarningsPrefixes()) {
+          if (typeSystems.contains(prefix)) {
+            return true;
+          }
+        }
+        return false;
+      }
+    }
+    return false;
+  }
+
   /**
    * Output a message about {@link #getAnnotatedType}, if logging is on.
    *

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

@@ -1367,6 +1367,7 @@ protected void performFlowAnalysisForClass(ClassTree classTree) {
               methods.add(method);
             }
             case VARIABLE -> {
+              // A top-level variable is a field.
               VariableTree vt = (VariableTree) m;
               ExpressionTree initializer = vt.getInitializer();
               AnnotatedTypeMirror declaredType = getAnnotatedTypeLhs(vt);
@@ -1383,8 +1384,8 @@ protected void performFlowAnalysisForClass(ClassTree classTree) {
                         new CFGStatement(vt, ct),
                         fieldValues,
                         null,
-                        true,
-                        true,
+                        /* isInitializationCode= */ true,
+                        /* updateInitializationStore= */ true,
                         isStatic,
                         capturedStore);
                 postAnalyze(cfg);

javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java

@@ -56,4 +56,12 @@ public interface AnnotationProvider {
    * @return true if multiple calls to the method (with the same arguments) return the same value
    */
   boolean isDeterministic(ExecutableElement methodElement);
+
+  /**
+   * Returns true if the given method may have side effects but does not unrefine its receiver.
+   *
+   * @param methodElement a method
+   * @return true if the method does not unrefine its receiver
+   */
+  boolean hasDoesNotUnrefineReceiver(ExecutableElement methodElement);
 }

javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java

@@ -83,4 +83,24 @@ public boolean isDeterministic(ExecutableElement methodElement) {
 
     return false;
   }
+
+  /**
+   * {@inheritDoc}
+   *
+   * <p>This implementation returns true if the {@code @DoesNotUnrefineReceiver} annotation is
+   * present on the given method, with "allcheckers" in the {@code value} element.
+   */
+  @Override
+  public boolean hasDoesNotUnrefineReceiver(ExecutableElement methodElement) {
+    for (AnnotationMirror am : methodElement.getAnnotationMirrors()) {
+      if (AnnotationUtils.areSameByName(
+          am, "org.checkerframework.dataflow.qual.DoesNotUnrefineReceiver")) {
+        @SuppressWarnings("deprecation") // calls from the framework are permitted
+        List<String> typeSystems =
+            AnnotationUtils.getElementValueArray(am, "value", String.class, true);
+        return typeSystems.contains("allcheckers");
+      }
+    }
+    return false;
+  }
 }