sideEffectsUnrefineAliases feature

checker/src/main/java/org/checkerframework/checker/lock/LockStore.java

@@ -185,6 +185,9 @@ public void updateForMethodCall(
             MethodInvocationNode n, AnnotatedTypeFactory atypeFactory, CFValue val) {
         super.updateForMethodCall(n, atypeFactory, val);
         ExecutableElement method = n.getTarget().getMethod();
+        // The following behavior is similar to setting the sideEffectsUnrefineAliases field of
+        // Lockannotatedtypefactory, but it affects only one of the two type hierarchies, so it
+        // cannot use that logic.
         if (!isSideEffectFree(atypeFactory, method)) {
             // After the call to super.updateForMethodCall, only final fields are left in
             // fieldValues (if the method called is side-effecting). For the LockPossiblyHeld

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

@@ -77,6 +77,11 @@ public KeyForAnnotatedTypeFactory(BaseTypeChecker checker) {
         addAliasedAnnotation(
                 "org.checkerframework.checker.nullness.compatqual.KeyForType", KeyFor.class, true);
 
+        // While strictly required for soundness, this leads to too many false positives.  Printing
+        // a key or putting it in a map erases all knowledge of what maps it was a key for.
+        // TODO: Revisit when side effect annotations are more precise.
+        // sideEffectsUnrefineAliases = true;
+
         this.postInit();
     }
 

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

@@ -256,6 +256,7 @@ private boolean polyNullIsNonNull(ExecutableElement method, NullnessStore s) {
      * A scanner that returns true if there is an occurrence of @PolyNull that is not at the top
      * level.
      */
+    // Not static so it can access field POLYNULL.
     private class ContainsPolyNullNotAtTopLevelScanner
             extends SimpleAnnotatedTypeScanner<Boolean, Void> {
         /**

checker/tests/nullness/KeyForLocalSideEffect.java

@@ -0,0 +1,23 @@
+import java.util.HashMap;
+import org.checkerframework.checker.nullness.qual.*;
+
+public class KeyForLocalSideEffect {
+
+    String k = "key";
+    HashMap<String, Integer> m = new HashMap<>();
+
+    void testContainsKeyForFieldKeyAndLocalMap() {
+        HashMap<String, Integer> m_local = m;
+
+        if (m_local.containsKey(k)) {
+            @KeyFor("m_local") String s = k;
+            havoc();
+            // TODO: This should be an error, because s is no longer a key for m_local.
+            @NonNull Integer val = m_local.get(s);
+        }
+    }
+
+    void havoc() {
+        m = new HashMap<>();
+    }
+}

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

@@ -199,55 +199,78 @@ public void updateForMethodCall(
         if (!(analysis.checker.hasOption("assumeSideEffectFree")
                 || analysis.checker.hasOption("assumePure")
                 || isSideEffectFree(atypeFactory, method))) {
-            // update field values
-            Map<FieldAccess, V> newFieldValues = new HashMap<>();
-            for (Map.Entry<FieldAccess, V> e : fieldValues.entrySet()) {
-                FieldAccess fieldAccess = e.getKey();
-                V otherVal = e.getValue();
 
-                // case 3: the field has a monotonic annotation
-                if (!((GenericAnnotatedTypeFactory<?, ?, ?, ?>) atypeFactory)
-                        .getSupportedMonotonicTypeQualifiers()
-                        .isEmpty()) {
-                    List<Pair<AnnotationMirror, AnnotationMirror>> fieldAnnotations =
-                            atypeFactory.getAnnotationWithMetaAnnotation(
-                                    fieldAccess.getField(), MonotonicQualifier.class);
-                    V newOtherVal = null;
-                    for (Pair<AnnotationMirror, AnnotationMirror> fieldAnnotation :
-                            fieldAnnotations) {
-                        AnnotationMirror monotonicAnnotation = fieldAnnotation.second;
-                        Name annotation =
-                                AnnotationUtils.getElementValueClassName(
-                                        monotonicAnnotation, "value", false);
-                        AnnotationMirror target =
-                                AnnotationBuilder.fromName(
-                                        atypeFactory.getElementUtils(), annotation);
-                        // Make sure the 'target' annotation is present.
-                        if (AnnotationUtils.containsSame(otherVal.getAnnotations(), target)) {
-                            newOtherVal =
-                                    analysis.createSingleAnnotationValue(
-                                                    target, otherVal.getUnderlyingType())
-                                            .mostSpecific(newOtherVal, null);
+            boolean sideEffectsUnrefineAliases =
+                    ((GenericAnnotatedTypeFactory) atypeFactory).sideEffectsUnrefineAliases;
+
+            // update local variables
+            // TODO: Also remove if any element/argument to the annotation is not
+            // isUnmodifiableByOtherCode.  Example: @KeyFor("valueThatCanBeMutated").
+            if (sideEffectsUnrefineAliases) {
+                localVariableValues
+                        .entrySet()
+                        .removeIf(e -> !e.getKey().isUnmodifiableByOtherCode());
+            }
+
+            // update this value
+            if (sideEffectsUnrefineAliases) {
+                thisValue = null;
+            }
+
+            // update field values
+            if (sideEffectsUnrefineAliases) {
+                fieldValues.entrySet().removeIf(e -> !e.getKey().isUnmodifiableByOtherCode());
+            } else {
+                Map<FieldAccess, V> newFieldValues = new HashMap<>();
+                for (Map.Entry<FieldAccess, V> e : fieldValues.entrySet()) {
+                    FieldAccess fieldAccess = e.getKey();
+                    V otherVal = e.getValue();
+
+                    // case 3: the field has a monotonic annotation
+                    if (!((GenericAnnotatedTypeFactory<?, ?, ?, ?>) atypeFactory)
+                            .getSupportedMonotonicTypeQualifiers()
+                            .isEmpty()) {
+                        List<Pair<AnnotationMirror, AnnotationMirror>> fieldAnnotations =
+                                atypeFactory.getAnnotationWithMetaAnnotation(
+                                        fieldAccess.getField(), MonotonicQualifier.class);
+                        V newOtherVal = null;
+                        for (Pair<AnnotationMirror, AnnotationMirror> fieldAnnotation :
+                                fieldAnnotations) {
+                            AnnotationMirror monotonicAnnotation = fieldAnnotation.second;
+                            Name annotation =
+                                    AnnotationUtils.getElementValueClassName(
+                                            monotonicAnnotation, "value", false);
+                            AnnotationMirror target =
+                                    AnnotationBuilder.fromName(
+                                            atypeFactory.getElementUtils(), annotation);
+                            // Make sure the 'target' annotation is present.
+                            if (AnnotationUtils.containsSame(otherVal.getAnnotations(), target)) {
+                                newOtherVal =
+                                        analysis.createSingleAnnotationValue(
+                                                        target, otherVal.getUnderlyingType())
+                                                .mostSpecific(newOtherVal, null);
+                            }
+                        }
+                        if (newOtherVal != null) {
+                            // keep information for all hierarchies where we had a
+                            // monotone annotation.
+                            newFieldValues.put(fieldAccess, newOtherVal);
+                            continue;
                         }
                     }
-                    if (newOtherVal != null) {
-                        // keep information for all hierarchies where we had a
-                        // monotone annotation.
-                        newFieldValues.put(fieldAccess, newOtherVal);
-                        continue;
+
+                    // case 2:
+                    if (!fieldAccess.isUnassignableByOtherCode()) {
+                        continue; // remove information completely
                     }
-                }
 
-                // case 2:
-                if (!fieldAccess.isUnassignableByOtherCode()) {
-                    continue; // remove information completely
+                    // keep information
+                    newFieldValues.put(fieldAccess, otherVal);
                 }
-
-                // keep information
-                newFieldValues.put(fieldAccess, otherVal);
+                fieldValues = newFieldValues;
             }
-            fieldValues = newFieldValues;
 
+            // update array values
             arrayValues.clear();
 
             // update method values

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

@@ -209,6 +209,17 @@ public abstract class GenericAnnotatedTypeFactory<
      */
     private Map<Tree, AnnotatedTypeMirror> initializerCache;
 
+    /**
+     * Should the analysis assume that side effects to a value can change the type of aliased
+     * references?
+     *
+     * <p>For many type systems, once a local variable's type is refined, side effects to the
+     * variable's value do not change the variable's type annotations. For some type systems, a side
+     * effect to the value could change them; set this field to true.
+     */
+    // Not final so that subclasses can set it.
+    public boolean sideEffectsUnrefineAliases = false;
+
     /** An empty store. */
     // Set in postInit only
     protected Store emptyStore;