From 613f98cf41d70f19a333f2b0d7e5680fa7141b27 Mon Sep 17 00:00:00 2001 From: Manu Sridharan Date: Thu, 5 Oct 2023 08:55:17 -0700 Subject: [PATCH] Update to Checker Framework 3.39.0 (#839) Fixes #831 as Checker Framework dataflow now has support for JDK 21 constructs --- gradle/dependencies.gradle | 2 +- .../nullaway/jdk17/NullAwayRecordTests.java | 42 +++++++++++++++++++ .../nullaway/jdk17/NullAwaySwitchTests.java | 11 ++++- .../AccessPathNullnessPropagation.java | 8 ++++ 4 files changed, 60 insertions(+), 3 deletions(-) diff --git a/gradle/dependencies.gradle b/gradle/dependencies.gradle index c3499f78f7..e31eb389e8 100755 --- 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 index d60e264a77..69047bac82 100644 --- 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 index 6b7a1d28fe..ca349f5733 100644 --- 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 index 6681d69797..36f35e4513 100644 --- 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 visitExpressionStatement( return noStoreChanges(NULLABLE, input); } + @Override + public TransferResult visitDeconstructorPattern( + DeconstructorPatternNode deconstructorPatternNode, + TransferInput input) { + return noStoreChanges(NULLABLE, input); + } + @Override public TransferResult visitPackageName( PackageNameNode packageNameNode, TransferInput input) {