Add @DoesNotUnrefineReceiver annotation

checker-qual/src/main/java/org/checkerframework/checker/index/qual/IndexOrHigh.java

@@ -33,6 +33,11 @@
 @Retention(RetentionPolicy.RUNTIME)
 @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER})
 public @interface IndexOrHigh {
-  /** Sequences that the annotated expression is a valid index for or is equal to the length of. */
+  /**
+   * The annotated expression is a valid index for, or is equal to the length of, each sequence.
+   *
+   * @return sequences that the annotated expression is a valid index for or is equal to the length
+   *     of
+   */
   String[] value();
 }

checker-qual/src/main/java/org/checkerframework/checker/lock/qual/LockPossiblyHeld.java

@@ -16,7 +16,7 @@
 /**
  * Indicates that an expression is not known to be {@link LockHeld}.
  *
- * <p>This annotation may not be written in source code; it is an implementation detail of the
+ * <p>This annotation should not be written in source code; it is an implementation detail of the
  * checker.
  *
  * @see LockHeld

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/common/aliasing/qual/LeakedToResult.java

@@ -27,6 +27,6 @@
 
 @Documented
 @Retention(RetentionPolicy.RUNTIME)
-@Target({ElementType.TYPE_USE})
+@Target({ElementType.TYPE_USE}) // no TYPE_PARAMETER
 @SubtypeOf({NonLeaked.class})
 public @interface LeakedToResult {}

checker-qual/src/main/java/org/checkerframework/common/subtyping/qual/Unqualified.java

@@ -12,7 +12,7 @@
  * A special annotation intended solely for representing an unqualified type in the qualifier
  * hierarchy, as an argument to {@link SubtypeOf#value()}, in a type qualifier declaration.
  *
- * <p>This annotation may not be written in source code; it is an implementation detail of the
+ * <p>This annotation should not be written in source code; it is an implementation detail of the
  * checker.
  *
  * <p>Use this qualifier only when experimenting with very simple type systems. For any more

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

@@ -0,0 +1,30 @@
+package org.checkerframework.framework.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
+ */
+@Documented
+@InheritedAnnotation
+@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();
+}

checker-qual/src/main/java/org/checkerframework/framework/qual/PreconditionAnnotation.java

@@ -43,7 +43,7 @@
  * {@code @MinLen(2)} upon entry.
  *
  * <pre><code>
- *  {@literal @}RequiresMinLen(value = "field", targetValue = 2")
+ *  {@literal @}RequiresMinLen(value = "field", targetValue = 2)
  *  public char getThirdCharacter() {
  *    return field.charAt(2);
  *  }

checker/tests/resourceleak/TwoResourcesECM.java

@@ -18,6 +18,9 @@ class TwoResourcesECM {
   @EnsuresCalledMethods(
       value = {"this.s1", "this.s2"},
       methods = {"close"})
+  // "contracts.postcondition" is a false positive warning, because no side effect should
+  // unrefine the "@Closed" type of `s1`.
+  // :: error: [contracts.postcondition]
   // :: error: [contracts.exceptional.postcondition]
   public void dispose() throws IOException {
     s1.close();

checker/tests/resourceleak/sideeffect-free-stubs-tests/AutoCloseableClose.java

@@ -14,6 +14,9 @@ class AutoCloseableClose implements AutoCloseable {
   @EnsuresCalledMethods(
       value = {"this.first", "this.second"},
       methods = "close")
+  // This is a false positive warning, because no side effect should unrefine the
+  // "@Closed" type of `first`.
+  // :: error: [contracts.postcondition]
   public void close() {
     try {
       first.close();

checker/tests/resourceleak/sideeffect-free-stubs-tests/CloseableClose.java

@@ -15,6 +15,9 @@ class CloseableClose implements Closeable {
   @EnsuresCalledMethods(
       value = {"this.first", "this.second"},
       methods = "close")
+  // This is a false positive warning, because no side effect should unrefine the
+  // "@Closed" type of `first`.
+  // :: error: [contracts.postcondition]
   public void close() {
     try {
       try {

checker/tests/tainting/TestDoesNotUnrefine.java

@@ -0,0 +1,28 @@
+import org.checkerframework.checker.tainting.qual.Untainted;
+import org.checkerframework.framework.qual.DoesNotUnrefineReceiver;
+
+public class TestDoesNotUnrefine {
+  static class MyClass {
+
+    @DoesNotUnrefineReceiver("tainting")
+    String doesNotUnrefine() {
+      return "";
+    }
+
+    String doesUnrefine() {
+      return "";
+    }
+  }
+
+  MyClass field;
+
+  void test(@Untainted MyClass untainted) {
+    field = untainted;
+    field.doesNotUnrefine();
+    @Untainted MyClass anotherLocal = field;
+
+    field.doesUnrefine();
+    // :: error: [assignment]
+    @Untainted MyClass anotherLocal2 = field;
+  }
+}

docs/CHANGELOG.md

@@ -15,6 +15,9 @@ Removed deprecated names "builder", "object.construction", and
 
 ### Implementation details
 
+New method annotation `@DoesNotUnrefineReceiver`.
+`AnnotatedTypeFactory` 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

@@ -98,6 +98,7 @@
 import org.checkerframework.common.wholeprograminference.WholeProgramInferenceScenesStorage;
 import org.checkerframework.dataflow.qual.SideEffectFree;
 import org.checkerframework.framework.qual.AnnotatedFor;
+import org.checkerframework.framework.qual.DoesNotUnrefineReceiver;
 import org.checkerframework.framework.qual.EnsuresQualifier;
 import org.checkerframework.framework.qual.EnsuresQualifierIf;
 import org.checkerframework.framework.qual.FieldInvariant;
@@ -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,29 @@ public boolean isDeterministic(ExecutableElement methodElement) {
     return false;
   }
 
+  /**
+   * 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
+   */
+  public boolean hasDoesNotUnrefineReceiver(ExecutableElement methodElement) {
+    for (AnnotationMirror am : getDeclAnnotations(methodElement)) {
+      if (areSameByClass(am, org.checkerframework.framework.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);