diff --git a/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/EnsuresNonNullIf.java b/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/EnsuresNonNullIf.java index d74189c154ce..5d0fcf215b95 100644 --- a/checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/EnsuresNonNullIf.java +++ b/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(); diff --git a/checker-qual/src/main/java/org/checkerframework/dataflow/qual/DoesNotUnrefineReceiver.java b/checker-qual/src/main/java/org/checkerframework/dataflow/qual/DoesNotUnrefineReceiver.java new file mode 100644 index 000000000000..329ea505d64e --- /dev/null +++ b/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(); +} diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 02f88a04ae6d..7e7df90823b3 100644 --- a/docs/CHANGELOG.md +++ b/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) diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java index 98a85b056097..32ef97423bb8 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractStore.java +++ b/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,32 +238,64 @@ 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 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 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. @@ -270,11 +303,6 @@ public void updateForMethodCall( 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 atypeFactory) { + GenericAnnotatedTypeFactory atypeFactory, Predicate doNotUnrefine) { Map newFieldValues = new HashMap<>(MapsP.mapCapacity(fieldValues)); for (Map.Entry 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); diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java index e957d70d7e13..96df1705373d 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/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 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. * diff --git a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java index 16d1495dbbef..5c8ce7d64ad5 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/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); diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java b/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java index e71ba812dd0b..5e2b84a222d6 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/AnnotationProvider.java +++ b/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); } diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java b/javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java index a160fd8a800c..4fdb3b3fefe4 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/BasicAnnotationProvider.java @@ -83,4 +83,24 @@ public boolean isDeterministic(ExecutableElement methodElement) { return false; } + + /** + * {@inheritDoc} + * + *

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 typeSystems = + AnnotationUtils.getElementValueArray(am, "value", String.class, true); + return typeSystems.contains("allcheckers"); + } + } + return false; + } }