Filter dependent type annotations referencing out-of-scope local vari…

checker/tests/index/ScopeCleanup.java

@@ -0,0 +1,60 @@
+import org.checkerframework.checker.index.qual.LessThan;
+import org.checkerframework.checker.index.qual.NonNegative;
+
+/**
+ * Test case for scope cleanup of dependent type annotations.
+ *
+ * <p>When a local variable goes out of scope, any dependent type annotation that references that
+ * variable should be invalidated. This test verifies that annotations like @LessThan("b") on
+ * variable 'a' are properly dropped when 'b' goes out of scope.
+ */
+public class ScopeCleanup {
+
+  /**
+   * Test that @LessThan annotation is properly cleaned up when the referenced variable goes out of
+   * scope.
+   */
+  void testScopeCleanup() {
+    int a = 5;
+
+    {
+      int b = 10;
+      a = b - 1;
+      // At this point, 'a' should have type @LessThan("b") and that's correct.
+
+      // This should be fine: a < b is true
+      @LessThan("b") int shouldWork = a;
+    }
+
+    // After exiting scope, 'b' is no longer in scope.
+    // The @LessThan("b") annotation on 'a' should be dropped.
+    // However, non-dependent annotations should survive.
+    @NonNegative int ok = a; // This should still work - a is still non-negative (a=9)
+
+    {
+      int b = 3; // Different variable 'b' with a smaller value!
+      // Without the fix, the old @LessThan("b") annotation would incorrectly refer to THIS 'b'.
+      // But a = 9 and this b = 3, so a > b, not a < b.
+
+      // This should be an error - we can no longer prove a < b
+      // The assignment below should fail type-checking because we can't prove a < b
+      // :: error: (assignment)
+      @LessThan("b") int shouldFail = a;
+    }
+  }
+
+  /**
+   * Test that method parameters are not affected by scope cleanup (they should always be considered
+   * in scope).
+   */
+  void testParametersRemainInScope(@NonNegative int param) {
+    int x;
+    {
+      int localVar = param + 1;
+      x = param - 1; // x < param should be valid
+    }
+    // Even after the block ends, 'param' is still in scope, so @LessThan("param") should be valid
+    // This test ensures method parameters are handled correctly
+    @LessThan("param") int shouldWork = x;
+  }
+}

docs/manual/contributors.tex

@@ -131,6 +131,7 @@
 Sean McLaughlin,
 Sebastian Schuberth,
 Shinya Yoshida,
+Shubham Kapoor,
 Shubham Raj,
 Sidney Monteiro,
 Simon Gerst,

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

@@ -2,11 +2,13 @@
 
 import java.util.ArrayList;
 import java.util.Collection;
+import java.util.Collections;
 import java.util.HashMap;
 import java.util.Iterator;
 import java.util.List;
 import java.util.Map;
 import java.util.Objects;
+import java.util.Set;
 import java.util.StringJoiner;
 import java.util.concurrent.atomic.AtomicLong;
 import java.util.function.BinaryOperator;
@@ -1141,6 +1143,17 @@ public boolean canAlias(JavaExpression a, JavaExpression b) {
     return localVariableValues.get(new LocalVariable(el));
   }
 
+  /**
+   * Returns the set of local variables currently tracked in this store.
+   *
+   * <p>Clients should not side-effect the returned value, which is aliased to internal state.
+   *
+   * @return the set of local variables currently in scope
+   */
+  public Set<LocalVariable> getLocalVariables() {
+    return Collections.unmodifiableSet(localVariableValues.keySet());
+  }
+
   /* --------------------------------------------------------- */
   /* Handling of the current object */
   /* --------------------------------------------------------- */

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

@@ -1989,6 +1989,16 @@ protected void addComputedTypeAnnotations(Tree tree, AnnotatedTypeMirror type, b
         log(
             "%s GATF.addComputedTypeAnnotations#8(%s, %s), inferred=%s%n",
             thisClass, treeString, type, inferred);
+
+        // Filter out dependent type annotations that reference out-of-scope local variables
+        if (dependentTypesHelper.hasDependentAnnotations()) {
+          Store store = getStoreBefore(tree);
+          if (store != null) {
+            Set<LocalVariable> inScopeVars = store.getLocalVariables();
+            dependentTypesHelper.filterAnnotationsForOutOfScopeVars(
+                type, inScopeVars, getPath(tree));
+          }
+        }
       }
     }
     log(

framework/src/main/java/org/checkerframework/framework/util/dependenttypes/DependentTypesHelper.java

@@ -755,6 +755,74 @@ public JavaExpression visitSuperReference(SuperReference superRef, Void unused)
     convertAnnotatedTypeMirror(stringToJavaExpr, atm);
   }
 
+  /**
+   * Filters dependent type annotations in {@code type}, removing those that reference local
+   * variables not currently in scope.
+   *
+   * <p>When a local variable goes out of scope, any dependent type annotation that references that
+   * variable becomes invalid and should be dropped. This method checks each expression in dependent
+   * type annotations and drops expressions that reference local variables not in {@code
+   * inScopeLocalVars}.
+   *
+   * @param type the type whose annotations may be filtered; is side-effected by this method
+   * @param inScopeLocalVars the set of local variables currently in scope
+   * @param path the tree path for expression parsing context; may be null
+   */
+  public void filterAnnotationsForOutOfScopeVars(
+      AnnotatedTypeMirror type, Set<LocalVariable> inScopeLocalVars, TreePath path) {
+    if (!hasDependentType(type)) {
+      return;
+    }
+
+    if (path == null) {
+      return;
+    }
+
+    StringToJavaExpression stringToJavaExpr =
+        expression -> {
+          // Check if this should be passed through unchanged
+          if (shouldPassThroughExpression(expression)) {
+            return new PassThroughExpression(objectTM, expression);
+          }
+
+          JavaExpression javaExpr;
+          try {
+            javaExpr = StringToJavaExpression.atPath(expression, path, factory.getChecker());
+          } catch (JavaExpressionParseException ex) {
+            // If the expression can't be parsed, keep it unchanged. The expression might reference
+            // a variable being declared (e.g., @KeyFor("a") where a is the variable itself),
+            // or might use syntax we don't need to filter. Only drop expressions when we confirm
+            // they reference out-of-scope local variables via FoundLocalVarException below.
+            return new PassThroughExpression(objectTM, expression);
+          }
+
+          // Check if the expression references any local variable not in scope
+          JavaExpressionConverter jec =
+              new JavaExpressionConverter() {
+                @Override
+                protected JavaExpression visitLocalVariable(LocalVariable localVarExpr, Void p) {
+                  // Check if this local variable is a method parameter
+                  if (localVarExpr.getElement().getKind() == ElementKind.PARAMETER) {
+                    return localVarExpr; // Parameters are always in scope
+                  }
+                  // Check if the local variable is in scope
+                  if (!inScopeLocalVars.contains(localVarExpr)) {
+                    throw new FoundLocalVarException();
+                  }
+                  return localVarExpr;
+                }
+              };
+
+          try {
+            return jec.convert(javaExpr);
+          } catch (FoundLocalVarException ex) {
+            return null; // Drop this expression - variable is out of scope
+          }
+        };
+
+    convertAnnotatedTypeMirror(stringToJavaExpr, type);
+  }
+
   /**
    * Calls {@link #convertAnnotationMirror(StringToJavaExpression, AnnotationMirror)} on each
    * annotation mirror on type with {@code stringToJavaExpr}. And replaces the annotation with the