Update to Checker Framework 3.39.0 (#839)

Fixes #831 as Checker Framework dataflow now has support for JDK 21 constructs
uber · Oct 5, 2023 · 613f98c · 613f98c
1 parent 91374c3
commit 613f98c
Show file tree

Hide file tree

Showing 4 changed files with 60 additions and 3 deletions.
diff --git a/gradle/dependencies.gradle b/gradle/dependencies.gradle
@@ -40,7 +40,7 @@ if (project.hasProperty("epApiVersion")) {
 
 def versions = [
     asm                    : "9.3",
-    checkerFramework       : "3.38.0",
+    checkerFramework       : "3.39.0",
     // for comparisons in other parts of the build
     errorProneLatest       : latestErrorProneVersion,
     // The version of Error Prone used to check NullAway's code.

diff --git a/jdk-recent-unit-tests/src/test/java/com/uber/nullaway/jdk17/NullAwayRecordTests.java b/jdk-recent-unit-tests/src/test/java/com/uber/nullaway/jdk17/NullAwayRecordTests.java
@@ -210,4 +210,46 @@ public void recordEqualsNull() {
             "}")
         .doTest();
   }
+
+  @Test
+  public void recordDeconstructionPatternInstanceOf() {
+    defaultCompilationHelper
+        .addSourceLines(
+            "Records.java",
+            "package com.uber;",
+            "import javax.annotation.Nullable;",
+            "class Records {",
+            "  record Rec(Object first, @Nullable Object second) { }",
+            "  void recordDeconstructionInstanceOf(Object obj) {",
+            "    if (obj instanceof Rec(Object f, @Nullable Object s)) {",
+            "      f.toString();",
+            "      // TODO: NullAway should report a warning here!",
+            "      // See https://github.com/uber/NullAway/issues/840",
+            "      s.toString();",
+            "    }",
+            "  }",
+            "}")
+        .doTest();
+  }
+
+  @Test
+  public void recordDeconstructionPatternSwitchCase() {
+    defaultCompilationHelper
+        .addSourceLines(
+            "Records.java",
+            "package com.uber;",
+            "import javax.annotation.Nullable;",
+            "class Records {",
+            "  record Rec(Object first, @Nullable Object second) { }",
+            "  int recordDeconstructionSwitchCase(Object obj) {",
+            "    return switch (obj) {",
+            "      // TODO: NullAway should report a warning here!",
+            "      // See https://github.com/uber/NullAway/issues/840",
+            "      case Rec(Object f, @Nullable Object s) -> s.toString().length();",
+            "      default -> 0;",
+            "    };",
+            "  }",
+            "}")
+        .doTest();
+  }
 }
diff --git a/jdk-recent-unit-tests/src/test/java/com/uber/nullaway/jdk17/NullAwaySwitchTests.java b/jdk-recent-unit-tests/src/test/java/com/uber/nullaway/jdk17/NullAwaySwitchTests.java
@@ -25,7 +25,6 @@
 import com.uber.nullaway.NullAway;
 import java.util.Arrays;
 import org.junit.Before;
-import org.junit.Ignore;
 import org.junit.Rule;
 import org.junit.Test;
 import org.junit.rules.TemporaryFolder;
@@ -176,7 +175,6 @@ public void testSwitchExprLambda() {
         .doTest();
   }
 
-  @Ignore("requires fix for crash in Checker dataflow library")
   @Test
   public void testSwitchExprNullCase() {
     defaultCompilationHelper
@@ -196,6 +194,15 @@ public void testSwitchExprNullCase() {
             "      case null -> throw new IllegalArgumentException(\"NullableEnum parameter is required\");",
             "    };",
             "  }",
+            "  static Object handleNullableEnumNoCaseNull(@Nullable NullableEnum nullableEnum) {",
+            "    // NOTE: in this case NullAway should report a bug, as there will be an NPE if nullableEnum",
+            "    // is null (since there is no `case null` in the switch).  This requires Error Prone support",
+            "    // for matching on switch expressions (https://github.com/google/error-prone/issues/4119)",
+            "    return switch (nullableEnum) {",
+            "      case A -> new Object();",
+            "      case B -> new Object();",
+            "    };",
+            "  }",
             "}")
         .doTest();
   }

diff --git a/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java b/nullaway/src/main/java/com/uber/nullaway/dataflow/AccessPathNullnessPropagation.java
@@ -72,6 +72,7 @@
 import org.checkerframework.nullaway.dataflow.cfg.node.ConditionalAndNode;
 import org.checkerframework.nullaway.dataflow.cfg.node.ConditionalNotNode;
 import org.checkerframework.nullaway.dataflow.cfg.node.ConditionalOrNode;
+import org.checkerframework.nullaway.dataflow.cfg.node.DeconstructorPatternNode;
 import org.checkerframework.nullaway.dataflow.cfg.node.DoubleLiteralNode;
 import org.checkerframework.nullaway.dataflow.cfg.node.EqualToNode;
 import org.checkerframework.nullaway.dataflow.cfg.node.ExplicitThisNode;
@@ -1085,6 +1086,13 @@ public TransferResult<Nullness, NullnessStore> visitExpressionStatement(
     return noStoreChanges(NULLABLE, input);
   }
 
+  @Override
+  public TransferResult<Nullness, NullnessStore> visitDeconstructorPattern(
+      DeconstructorPatternNode deconstructorPatternNode,
+      TransferInput<Nullness, NullnessStore> input) {
+    return noStoreChanges(NULLABLE, input);
+  }
+
   @Override
   public TransferResult<Nullness, NullnessStore> visitPackageName(
       PackageNameNode packageNameNode, TransferInput<Nullness, NullnessStore> input) {