From 2135b46edc6a2d10d65dbc1d9dc3ee3b2dd6f450 Mon Sep 17 00:00:00 2001
From: Michael Ernst <mernst@cs.washington.edu>
Date: Fri, 5 Aug 2022 14:55:33 -0700
Subject: [PATCH] Expand definition of local variable

---
 .../java17/InstanceOfPatternVariable.java     | 16 ++++++++++++
 .../javacutil/ElementUtils.java               |  6 ++---
 .../checkerframework/javacutil/Resolver.java  | 25 +++++++++++++++----
 3 files changed, 39 insertions(+), 8 deletions(-)
 create mode 100644 checker/tests/nullness/java17/InstanceOfPatternVariable.java

diff --git a/checker/tests/nullness/java17/InstanceOfPatternVariable.java b/checker/tests/nullness/java17/InstanceOfPatternVariable.java
new file mode 100644
index 00000000000..0c9e300c473
--- /dev/null
+++ b/checker/tests/nullness/java17/InstanceOfPatternVariable.java
@@ -0,0 +1,16 @@
+// @below-java17-jdk-skip-test
+// Test case for https://github.com/typetools/checker-framework/issues/5240
+
+import java.util.Map;
+import org.checkerframework.checker.nullness.qual.KeyFor;
+
+public class InstanceOfPatternVariable {
+
+  public void doSomething(final Object x) {
+    if (x instanceof Map<?, ?> m) {
+      // final var ct = (ClassOrInterfaceType) type;
+
+      @KeyFor("m") Object y = m.keySet().iterator().next();
+    }
+  }
+}
diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java
index 8d508883c52..0c8f24c07d6 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/ElementUtils.java
@@ -787,14 +787,14 @@ public static boolean isTypeDeclaration(Element elt) {
   /**
    * Return true if the element is a binding variable.
    *
-   * <p>Note: This is to conditionally support Java 15 instanceof pattern matching. When available,
-   * this should use {@code ElementKind.BINDING_VARIABLE} directly.
+   * <p>This implementation compiles under JDK 8 and 11 as well as versions that contain {@code
+   * ElementKind.BINDING_VARIABLE}.
    *
    * @param element the element to test
    * @return true if the element is a binding variable
    */
   public static boolean isBindingVariable(Element element) {
-    return "BINDING_VARIABLE".equals(element.getKind().name());
+    return SystemUtil.jreVersion >= 16 && "BINDING_VARIABLE".equals(element.getKind().name());
   }
 
   /**
diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/Resolver.java b/javacutil/src/main/java/org/checkerframework/javacutil/Resolver.java
index 9a0dc5e5af5..8663d77df07 100644
--- a/javacutil/src/main/java/org/checkerframework/javacutil/Resolver.java
+++ b/javacutil/src/main/java/org/checkerframework/javacutil/Resolver.java
@@ -245,11 +245,26 @@ public Env<AttrContext> getEnvForPath(TreePath path) {
     try {
       Env<AttrContext> env = getEnvForPath(path);
       Element res = wrapInvocationOnResolveInstance(FIND_VAR, env, names.fromString(name));
-      if (res.getKind() == ElementKind.LOCAL_VARIABLE || res.getKind() == ElementKind.PARAMETER) {
-        return (VariableElement) res;
-      } else {
-        // The Element might be FIELD or a SymbolNotFoundError.
-        return null;
+      // Every kind in the documentation of Element.getKind() is explicitly tested, possibly in the
+      // "default:" case.
+      switch (res.getKind()) {
+        case EXCEPTION_PARAMETER:
+        case LOCAL_VARIABLE:
+        case PARAMETER:
+        case RESOURCE_VARIABLE:
+          return (VariableElement) res;
+        case ENUM_CONSTANT:
+        case FIELD:
+          return null;
+        default:
+          if (ElementUtils.isBindingVariable(res)) {
+            return (VariableElement) res;
+          }
+          if (res instanceof VariableElement) {
+            throw new BugInCF("unhandled variable ElementKind " + res.getKind());
+          }
+          // The Element might be a SymbolNotFoundError.
+          return null;
       }
     } finally {
       log.popDiagnosticHandler(discardDiagnosticHandler);