From f97a80e0332c608d8b9b2703fd2246bda6efe63d Mon Sep 17 00:00:00 2001 From: "renovate[bot]" <29139614+renovate[bot]@users.noreply.github.com> Date: Mon, 6 Jan 2025 15:15:36 -0500 Subject: [PATCH 01/13] Update bazel-contrib/setup-bazel action to v0.12.0 (#1050) --- .github/workflows/ci.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 4c6b531c3e7..5e7b6254033 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -38,7 +38,7 @@ jobs: uses: gradle/actions/setup-gradle@v4.2.2 - name: Setup Bazel - uses: bazel-contrib/setup-bazel@0.10.0 + uses: bazel-contrib/setup-bazel@0.12.0 if: ${{ matrix.script == 'cftests-nonjunit' }} with: # Avoid downloading Bazel every time. @@ -212,7 +212,7 @@ jobs: texlive-font-utils texlive-fonts-recommended texlive-latex-recommended pip install black flake8 html5validator - name: Setup Bazel - uses: bazel-contrib/setup-bazel@0.10.0 + uses: bazel-contrib/setup-bazel@0.12.0 if: ${{ matrix.script == 'cftests-nonjunit' }} with: # Avoid downloading Bazel every time. From f70c3f9f9bed7640b2ca0a55365e0b4373d64e94 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 6 Jan 2025 13:08:45 -0800 Subject: [PATCH 02/13] Add CI test for the `templatefora-checker` (#1048) Co-authored-by: Werner Dietl --- checker/bin-devel/test-misc.sh | 4 ++++ checker/build.gradle | 37 ++++++++++++++++++++++++++++++++++ 2 files changed, 41 insertions(+) diff --git a/checker/bin-devel/test-misc.sh b/checker/bin-devel/test-misc.sh index 3e21746d48e..f2227a156e2 100755 --- a/checker/bin-devel/test-misc.sh +++ b/checker/bin-devel/test-misc.sh @@ -16,6 +16,10 @@ PLUME_SCRIPTS="$SCRIPTDIR/.plume-scripts" "$GIT_SCRIPTS/git-clone-related" eisop checker-framework.demos ./gradlew :checker:demosTests --console=plain --warning-mode=all +## Checker Framework templatefora-checker +"$GIT_SCRIPTS/git-clone-related" eisop templatefora-checker +./gradlew :checker:templateTests --console=plain --warning-mode=all + status=0 ## Code style and formatting diff --git a/checker/build.gradle b/checker/build.gradle index bbc55daf3cd..caedf1412ce 100644 --- a/checker/build.gradle +++ b/checker/build.gradle @@ -355,6 +355,43 @@ task demosTests(dependsOn: assembleForJavac, group: 'Verification') { } } +task templateTests(dependsOn: assembleForJavac, group: 'Verification') { + description = 'Test that the templatefora-checker is working as expected.' + + def injected = project.objects.newInstance(InjectedExecOps) + + doLast { + File templateforCheckerDir = new File(projectDir, '../../templatefora-checker'); + if (!templateforCheckerDir.exists()) { + injected.execOps.exec { + workingDir file(templateforCheckerDir.toString() + '/../') + executable 'git' + args = [ + 'clone', + '--depth', + '1', + 'https://github.com/eisop/templatefora-checker.git' + ] + } + } else { + injected.execOps.exec { + workingDir templateforCheckerDir + executable 'git' + args = [ + 'pull', + 'https://github.com/eisop/templatefora-checker.git' + ] + ignoreExitValue = true + } + } + println "Running Gradle build in $templateforCheckerDir" + injected.execOps.exec { + workingDir = templateforCheckerDir + commandLine "./gradlew", "build" + } + } +} + task allNullnessTests(type: Test, group: 'Verification') { description = 'Run all JUnit tests for the Nullness Checker.' include '**/Nullness*.class' From 3d9dcce0868c7666661899e7c08b0a2b1854be53 Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Tue, 7 Jan 2025 13:50:33 -0500 Subject: [PATCH 03/13] Add fixed issue to changelog --- docs/CHANGELOG.md | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 43c0d06238a..73848a6b390 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -31,8 +31,8 @@ Make `SourceChecker#suppressWarningsString` protected to allow adaptation in sub **Closed issues:** -eisop#413, eisop#782, eisop#815, eisop#860, eisop#873, eisop#875, eisop#927, eisop#982, -eisop#1012. +eisop#413, eisop#782, eisop#815, eisop#826, eisop#860, eisop#873, eisop#875, eisop#927, +eisop#982, eisop#1012. Version 3.42.0-eisop4 (July 12, 2024) From 141d6fde85f8dbe5cbbdc405693d874c08f762de Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Tue, 7 Jan 2025 20:52:20 -0500 Subject: [PATCH 04/13] Update to Spotless 7.0.1 and run `spotlessApply` (#1054) --- build.gradle | 6 ++-- .../checker/formatter/FormatterVisitor.java | 8 ++--- .../i18nformatter/I18nFormatterVisitor.java | 2 +- .../nullness/NullnessNoInitVisitor.java | 2 +- .../ResourceLeakAnnotatedTypeFactory.java | 4 ++- .../checker/signedness/SignednessVisitor.java | 8 ++--- ...ork.checker.nullness.NullnessChecker.ajava | 3 +- .../CheckerFrameworkBuilder.java | 3 +- checker/tests/fenum/TestSwitch.java | 4 +-- .../java17/SwitchExpressionInvariant.java | 4 +-- .../nullness/java17/SwitchTestIssue5412.java | 14 ++++---- .../tests/nullness/java21/NullRedundant.java | 12 +++---- .../java21/NullableSwitchSelector.java | 10 +++--- .../cfg/visualize/CFGVisualizeLauncher.java | 10 +++--- .../common/basetype/BaseTypeChecker.java | 4 ++- .../common/basetype/BaseTypeVisitor.java | 4 +-- .../AnnotationConverter.java | 2 +- .../WholeProgramInferenceImplementation.java | 36 +++++++++---------- ...holeProgramInferenceJavaParserStorage.java | 3 +- .../WholeProgramInferenceScenesStorage.java | 28 +++++++-------- .../framework/flow/CFTreeBuilder.java | 4 +-- .../framework/stub/AnnotationFileParser.java | 6 ++-- .../framework/type/AnnotatedTypeFactory.java | 34 +++++++++--------- .../type/GenericAnnotatedTypeFactory.java | 10 +++--- .../framework/util/JavaParserUtil.java | 12 +++---- .../util/defaults/QualifierDefaults.java | 6 ++-- .../tests/all-systems/java17/SwitchTests.java | 2 +- .../javacutil/CollectionUtils.java | 9 +++-- .../checkerframework/javacutil/TreeUtils.java | 6 ++-- 29 files changed, 134 insertions(+), 122 deletions(-) diff --git a/build.gradle b/build.gradle index 73a9d578bd3..c1a30166329 100644 --- a/build.gradle +++ b/build.gradle @@ -6,7 +6,7 @@ buildscript { // Code formatting; defines targets "spotlessApply" and "spotlessCheck". // https://github.com/diffplug/spotless/tags ; see tags starting "gradle/" // Only works on JDK 11+. - classpath 'com.diffplug.spotless:spotless-plugin-gradle:6.25.0' + classpath 'com.diffplug.spotless:spotless-plugin-gradle:7.0.1' } } } @@ -277,7 +277,7 @@ allprojects { target '*.md', '*.tex', '.gitignore', 'Makefile' targetExclude doNotFormat // define the steps to apply to those files - indentWithSpaces(2) + leadingTabsToSpaces(2) trimTrailingWhitespace() // endWithNewline() // Don't want to end empty files with a newline } @@ -314,7 +314,7 @@ allprojects { target '**/*.gradle' targetExclude doNotFormat greclipse() // which formatter Spotless should use to format .gradle files. - indentWithSpaces(4) + leadingTabsToSpaces(4) trimTrailingWhitespace() // endWithNewline() // Don't want to end empty files with a newline } diff --git a/checker/src/main/java/org/checkerframework/checker/formatter/FormatterVisitor.java b/checker/src/main/java/org/checkerframework/checker/formatter/FormatterVisitor.java index 65e3c092432..241954912e4 100644 --- a/checker/src/main/java/org/checkerframework/checker/formatter/FormatterVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/formatter/FormatterVisitor.java @@ -143,10 +143,10 @@ public Void visitMethodInvocation(MethodInvocationTree tree, Void p) { if (!isWrappedFormatCall(fc, enclosingMethod)) { ftu.warning(invc, "format.indirect.arguments"); } - // TODO: If it is explict array construction, such as "new Object[] { - // ... }", then we could treat it like the VARARGS case, analyzing each - // argument. "new array" is probably rare, in the varargs position. - // fall through + // TODO: If it is explict array construction, such as "new Object[] { + // ... }", then we could treat it like the VARARGS case, analyzing each + // argument. "new array" is probably rare, in the varargs position. + // fall through case NULLARRAY: for (ConversionCategory cat : formatCats) { if (cat == ConversionCategory.NULL) { diff --git a/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterVisitor.java b/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterVisitor.java index 8d3ffdc6471..3b1c3af7bd6 100644 --- a/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/i18nformatter/I18nFormatterVisitor.java @@ -105,7 +105,7 @@ private void checkInvocationFormatFor(I18nFormatCall fc) { } break; case NULLARRAY: - // fall-through + // fall-through case ARRAY: for (I18nConversionCategory cat : formatCats) { if (cat == I18nConversionCategory.UNUSED) { diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java index a11cc6173d6..b358a74ab5f 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java @@ -233,7 +233,7 @@ protected boolean commonAssignmentCheck( || !((IdentifierTree) receiver).getName().contentEquals("this")) { return null; } - // fallthrough + // fallthrough case IDENTIFIER: TreePath path = getCurrentPath(); if (TreePathUtil.inConstructor(path)) { diff --git a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java index 89d052cf7e2..be3c4da7403 100644 --- a/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/resourceleak/ResourceLeakAnnotatedTypeFactory.java @@ -378,7 +378,9 @@ public boolean canCreateObligations() { @Override @SuppressWarnings("TypeParameterUnusedInFormals") // Intentional abuse - public > @Nullable T getTypeFactoryOfSubcheckerOrNull(Class subCheckerClass) { + public > + @Nullable T getTypeFactoryOfSubcheckerOrNull( + Class subCheckerClass) { if (subCheckerClass == MustCallChecker.class) { if (!canCreateObligations()) { return super.getTypeFactoryOfSubcheckerOrNull( diff --git a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java index dc0f41b6624..38ce6a96736 100644 --- a/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/signedness/SignednessVisitor.java @@ -172,8 +172,8 @@ tree, getCurrentPath())) { } break; } - // Other plus binary trees should be handled in the default case. - // fall through + // Other plus binary trees should be handled in the default case. + // fall through default: if (leftOpType.hasEffectiveAnnotation(Unsigned.class) && rightOpType.hasEffectiveAnnotation(Signed.class)) { @@ -354,8 +354,8 @@ public Void visitCompoundAssignment(CompoundAssignmentTree tree, Void p) { } break; } - // Other plus binary trees should be handled in the default case. - // fall through + // Other plus binary trees should be handled in the default case. + // fall through default: if (varType.hasAnnotation(Unsigned.class) && exprType.hasAnnotation(Signed.class)) { checker.reportError( diff --git a/checker/tests/ainfer-nullness/input-annotation-files/TypeVarReturnAnnotated-org.checkerframework.checker.nullness.NullnessChecker.ajava b/checker/tests/ainfer-nullness/input-annotation-files/TypeVarReturnAnnotated-org.checkerframework.checker.nullness.NullnessChecker.ajava index 25145411d1f..11336ca0f7e 100644 --- a/checker/tests/ainfer-nullness/input-annotation-files/TypeVarReturnAnnotated-org.checkerframework.checker.nullness.NullnessChecker.ajava +++ b/checker/tests/ainfer-nullness/input-annotation-files/TypeVarReturnAnnotated-org.checkerframework.checker.nullness.NullnessChecker.ajava @@ -6,7 +6,8 @@ public class TypeVarReturnAnnotated { public static - @org.checkerframework.checker.initialization.qual.FBCBottom @org.checkerframework.checker.nullness.qual.Nullable T extract() { + @org.checkerframework.checker.initialization.qual.FBCBottom @org.checkerframework.checker.nullness.qual.Nullable T + extract() { return null; } } diff --git a/checker/tests/calledmethods-lombok/CheckerFrameworkBuilder.java b/checker/tests/calledmethods-lombok/CheckerFrameworkBuilder.java index f8fa4a1e023..5241db55261 100644 --- a/checker/tests/calledmethods-lombok/CheckerFrameworkBuilder.java +++ b/checker/tests/calledmethods-lombok/CheckerFrameworkBuilder.java @@ -197,7 +197,8 @@ public java.lang.String toString() { @org.checkerframework.dataflow.qual.SideEffectFree @java.lang.SuppressWarnings("all") - public static CheckerFrameworkBuilder.@org.checkerframework.common.aliasing.qual.Unique CheckerFrameworkBuilderBuilder builder() { + public static CheckerFrameworkBuilder.@org.checkerframework.common.aliasing.qual.Unique CheckerFrameworkBuilderBuilder + builder() { return new CheckerFrameworkBuilder.CheckerFrameworkBuilderBuilder(); } } diff --git a/checker/tests/fenum/TestSwitch.java b/checker/tests/fenum/TestSwitch.java index 22fdd4de495..8085c5a289b 100644 --- a/checker/tests/fenum/TestSwitch.java +++ b/checker/tests/fenum/TestSwitch.java @@ -11,7 +11,7 @@ void m() { int plain = 9; // FenumUnqualified switch (plain) { - // :: error: (switch.type.incompatible) + // :: error: (switch.type.incompatible) case annotated: default: } @@ -24,7 +24,7 @@ void m() { } switch (annotated) { - // :: error: (switch.type.incompatible) + // :: error: (switch.type.incompatible) case 45: default: } diff --git a/checker/tests/nullness/java17/SwitchExpressionInvariant.java b/checker/tests/nullness/java17/SwitchExpressionInvariant.java index 2e38564b5f2..c43ab5a23bf 100644 --- a/checker/tests/nullness/java17/SwitchExpressionInvariant.java +++ b/checker/tests/nullness/java17/SwitchExpressionInvariant.java @@ -15,14 +15,14 @@ void method( List<@NonNull String> list = // :: error: (assignment.type.incompatible) switch (fenum) { - // :: error: (switch.expression.type.incompatible) + // :: error: (switch.expression.type.incompatible) case 1 -> nonnullStrings; default -> nullableStrings; }; List<@Nullable String> list2 = switch (fenum) { - // :: error: (switch.expression.type.incompatible) + // :: error: (switch.expression.type.incompatible) case 1 -> nonnullStrings; default -> nullableStrings; }; diff --git a/checker/tests/nullness/java17/SwitchTestIssue5412.java b/checker/tests/nullness/java17/SwitchTestIssue5412.java index 75a52539eef..d7055c3190f 100644 --- a/checker/tests/nullness/java17/SwitchTestIssue5412.java +++ b/checker/tests/nullness/java17/SwitchTestIssue5412.java @@ -27,9 +27,9 @@ public String foo1a(MyEnum b) { case VAL1 -> "1"; case VAL2 -> "2"; case VAL3 -> "3"; - // The default case is dead code, so it would be possible for type-checking - // to skip it and not issue this warning. But giving the warning is also - // good. + // The default case is dead code, so it would be possible for type-checking + // to skip it and not issue this warning. But giving the warning is also + // good. default -> null; }; // :: error: (return.type.incompatible) @@ -82,8 +82,8 @@ public String foo4a(MyEnum b) { case VAL3: aString = "c"; break; - // The `default:` case is dead code, so it is acceptable for this method to compile - // without nullness errors. + // The `default:` case is dead code, so it is acceptable for this method to compile + // without nullness errors. default: break; } @@ -103,8 +103,8 @@ public String foo4b(MyEnum b) { case VAL3: aString = "c"; break; - // The `default:` case is dead code, so it is acceptable for this method to compile - // without nullness errors. + // The `default:` case is dead code, so it is acceptable for this method to compile + // without nullness errors. default: aString = null; break; diff --git a/checker/tests/nullness/java21/NullRedundant.java b/checker/tests/nullness/java21/NullRedundant.java index 10151a8714e..9a671569014 100644 --- a/checker/tests/nullness/java21/NullRedundant.java +++ b/checker/tests/nullness/java21/NullRedundant.java @@ -16,7 +16,7 @@ void test1(Object o) { case Number n: System.out.println("Number: " + n); break; - // :: warning: (nulltest.redundant) + // :: warning: (nulltest.redundant) case null: System.out.println("null"); break; @@ -25,7 +25,7 @@ void test1(Object o) { } switch (o) { - // :: warning: (nulltest.redundant) + // :: warning: (nulltest.redundant) case null, default: System.out.println("null"); break; @@ -35,27 +35,27 @@ void test1(Object o) { Object test2(Object o) { switch (o) { case Number n -> System.out.println("Number: " + n); - // :: warning: (nulltest.redundant) + // :: warning: (nulltest.redundant) case null -> System.out.println("null"); default -> System.out.println("anything else"); } ; switch (o) { - // :: warning: (nulltest.redundant) + // :: warning: (nulltest.redundant) case null, default -> System.out.println("null"); } var output = switch (o) { case Number n -> "Number: " + n; - // :: warning: (nulltest.redundant) + // :: warning: (nulltest.redundant) case null -> "null"; default -> "anything else"; }; return switch (o) { - // :: warning: (nulltest.redundant) + // :: warning: (nulltest.redundant) case null -> "null"; default -> "anything else"; }; diff --git a/checker/tests/nullness/java21/NullableSwitchSelector.java b/checker/tests/nullness/java21/NullableSwitchSelector.java index 49341e27958..9cb5a40ecf0 100644 --- a/checker/tests/nullness/java21/NullableSwitchSelector.java +++ b/checker/tests/nullness/java21/NullableSwitchSelector.java @@ -13,7 +13,7 @@ static String formatterPatternSwitch1(@Nullable Object obj) { return switch (obj) { case Integer i -> obj.toString(); case String s -> String.format("String %s", s); - // :: error: (dereference.of.nullable) + // :: error: (dereference.of.nullable) case null -> obj.toString(); default -> obj.toString(); }; @@ -24,9 +24,9 @@ static String formatterPatternSwitch2(@Nullable Object obj) { return switch (obj) { case Integer i -> obj.toString(); case String s -> String.format("String %s", s); - // TODO: If obj is null, this case isn't reachable, because a null pointer exception - // happens at the selector expression. - // :: error: (dereference.of.nullable) + // TODO: If obj is null, this case isn't reachable, because a null pointer exception + // happens at the selector expression. + // :: error: (dereference.of.nullable) default -> obj.toString(); }; } @@ -35,7 +35,7 @@ static String formatterPatternSwitch3(@Nullable Object obj) { return switch (obj) { case Integer i -> obj.toString(); case String s -> String.format("String %s", s); - // :: error: (dereference.of.nullable) + // :: error: (dereference.of.nullable) case null, default -> obj.toString(); }; } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/CFGVisualizeLauncher.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/CFGVisualizeLauncher.java index 8b2c6a28360..d0ff19faea2 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/CFGVisualizeLauncher.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/visualize/CFGVisualizeLauncher.java @@ -342,11 +342,11 @@ private static void producePDF(String file) { S extends Store, T extends TransferFunction> @Nullable Map generateStringOfCFG( - String inputFile, - String method, - String clas, - boolean verbose, - @Nullable Analysis analysis) { + String inputFile, + String method, + String clas, + boolean verbose, + @Nullable Analysis analysis) { ControlFlowGraph cfg = generateMethodCFG(inputFile, clas, method); if (analysis != null) { analysis.performAnalysis(cfg); diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java index 1f48581f81f..56353deb5e6 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeChecker.java @@ -436,7 +436,9 @@ public AnnotationProvider getAnnotationProvider() { * @return the type factory of the requested subchecker or null if not found */ @SuppressWarnings("TypeParameterUnusedInFormals") // Intentional abuse - public > @Nullable T getTypeFactoryOfSubcheckerOrNull(Class subCheckerClass) { + public > + @Nullable T getTypeFactoryOfSubcheckerOrNull( + Class subCheckerClass) { return getTypeFactory().getTypeFactoryOfSubcheckerOrNull(subCheckerClass); } diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index 6cb489b93f6..74bdcb4b22b 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -2948,7 +2948,7 @@ public void warnAboutIrrelevantJavaTypes( while (true) { switch (t.getKind()) { - // Recurse for compound types whose top level is not at the far left. + // Recurse for compound types whose top level is not at the far left. case ARRAY_TYPE: t = ((ArrayTypeTree) t).getType(); continue; @@ -2959,7 +2959,7 @@ public void warnAboutIrrelevantJavaTypes( t = ((ParameterizedTypeTree) t).getType(); continue; - // Base cases + // Base cases case PRIMITIVE_TYPE: case IDENTIFIER: maybeReportAnnoOnIrrelevant(t, TreeUtils.typeOf(t), annoTrees); diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/AnnotationConverter.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/AnnotationConverter.java index f77178d093b..b74e7799e3c 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/AnnotationConverter.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/AnnotationConverter.java @@ -128,7 +128,7 @@ protected static AnnotationFieldType typeMirrorToAnnotationFieldType(TypeMirror switch (tm.getKind()) { case BOOLEAN: return BasicAFT.forType(boolean.class); - // Primitives + // Primitives case BYTE: return BasicAFT.forType(byte.class); case CHAR: diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java index 9c5a0ae8722..cb27095f4d5 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java @@ -1114,19 +1114,19 @@ public void updateAtmWithLub(AnnotatedTypeMirror sourceCodeATM, AnnotatedTypeMir break; case WILDCARD: break; - // throw new BugInCF("This can't happen"); - // TODO: This comment is wrong: the wildcard case does get entered. - // Because inferring type arguments is not supported, wildcards won't be - // encountered. - // updateATMWithLUB( - // atf, - // ((AnnotatedWildcardType) sourceCodeATM).getExtendsBound(), - // ((AnnotatedWildcardType) ajavaATM).getExtendsBound()); - // updateATMWithLUB( - // atf, - // ((AnnotatedWildcardType) sourceCodeATM).getSuperBound(), - // ((AnnotatedWildcardType) ajavaATM).getSuperBound()); - // break; + // throw new BugInCF("This can't happen"); + // TODO: This comment is wrong: the wildcard case does get entered. + // Because inferring type arguments is not supported, wildcards won't be + // encountered. + // updateATMWithLUB( + // atf, + // ((AnnotatedWildcardType) sourceCodeATM).getExtendsBound(), + // ((AnnotatedWildcardType) ajavaATM).getExtendsBound()); + // updateATMWithLUB( + // atf, + // ((AnnotatedWildcardType) sourceCodeATM).getSuperBound(), + // ((AnnotatedWildcardType) ajavaATM).getSuperBound()); + // break; case ARRAY: AnnotatedTypeMirror sourceCodeComponent = ((AnnotatedArrayType) sourceCodeATM).getComponentType(); @@ -1147,11 +1147,11 @@ public void updateAtmWithLub(AnnotatedTypeMirror sourceCodeATM, AnnotatedTypeMir } } break; - // case DECLARED: - // Inferring annotations on type arguments is not supported, so no need to recur on - // generic types. If this was ever implemented, this method would need a - // VisitHistory object to prevent infinite recursion on types such as T extends - // List. + // case DECLARED: + // Inferring annotations on type arguments is not supported, so no need to recur on + // generic types. If this was ever implemented, this method would need a + // VisitHistory object to prevent infinite recursion on types such as T extends + // List. default: // ATM only has primary annotations break; diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java index 26fae9cbc72..77d3baa422d 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceJavaParserStorage.java @@ -1858,7 +1858,8 @@ public String toString() { * @param orig the map to copy * @return a deep copy of the map */ - private static @Nullable Map> deepCopyMapOfStringToPair( + private static @Nullable Map> + deepCopyMapOfStringToPair( @Nullable Map> orig) { if (orig == null) { return null; diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceScenesStorage.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceScenesStorage.java index d84d1b44b67..d41961853ea 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceScenesStorage.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceScenesStorage.java @@ -644,25 +644,25 @@ private void updateAtmWithLub(AnnotatedTypeMirror sourceCodeATM, AnnotatedTypeMi ((AnnotatedTypeVariable) sourceCodeATM).getUpperBound(), ((AnnotatedTypeVariable) jaifATM).getUpperBound()); break; - // case WILDCARD: - // Because inferring type arguments is not supported, wildcards won't be encoutered - // updateAtmWithLub(((AnnotatedWildcardType) - // sourceCodeATM).getExtendsBound(), - // ((AnnotatedWildcardType) - // jaifATM).getExtendsBound()); - // updateAtmWithLub(((AnnotatedWildcardType) - // sourceCodeATM).getSuperBound(), - // ((AnnotatedWildcardType) jaifATM).getSuperBound()); - // break; + // case WILDCARD: + // Because inferring type arguments is not supported, wildcards won't be encoutered + // updateAtmWithLub(((AnnotatedWildcardType) + // sourceCodeATM).getExtendsBound(), + // ((AnnotatedWildcardType) + // jaifATM).getExtendsBound()); + // updateAtmWithLub(((AnnotatedWildcardType) + // sourceCodeATM).getSuperBound(), + // ((AnnotatedWildcardType) jaifATM).getSuperBound()); + // break; case ARRAY: updateAtmWithLub( ((AnnotatedArrayType) sourceCodeATM).getComponentType(), ((AnnotatedArrayType) jaifATM).getComponentType()); break; - // case DECLARED: - // inferring annotations on type arguments is not supported, so no need to recur on - // generic types. If this was every implemented, this method would need VisitHistory - // object to prevent infinite recursion on types such as T extends List. + // case DECLARED: + // inferring annotations on type arguments is not supported, so no need to recur on + // generic types. If this was every implemented, this method would need VisitHistory + // object to prevent infinite recursion on types such as T extends List. default: // ATM only has primary annotations break; diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFTreeBuilder.java b/framework/src/main/java/org/checkerframework/framework/flow/CFTreeBuilder.java index 63b15c686b9..8a9ff638724 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFTreeBuilder.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFTreeBuilder.java @@ -169,8 +169,8 @@ private Tree createAnnotatedType(TypeMirror type) { } typeTree = maker.TypeIntersection(components); break; - // case UNION: - // TODO: case UNION similar to INTERSECTION, but write test first. + // case UNION: + // TODO: case UNION similar to INTERSECTION, but write test first. case DECLARED: typeTree = maker.Type((Type) type); diff --git a/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java b/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java index 955d4db1e30..866c00e3d1d 100644 --- a/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java +++ b/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java @@ -2745,9 +2745,9 @@ private Object getValueOfExpressionInAnnotation( return convert(((LongLiteralExpr) expr).asNumber(), valueKind); } else if (expr instanceof UnaryExpr) { switch (expr.toString()) { - // Special-case the minimum values. Separately parsing a "-" and a value - // doesn't correctly handle the minimum values, because the absolute value of - // the smallest member of an integral type is larger than the largest value. + // Special-case the minimum values. Separately parsing a "-" and a value + // doesn't correctly handle the minimum values, because the absolute value of + // the smallest member of an integral type is larger than the largest value. case "-9223372036854775808L": case "-9223372036854775808l": return convert(Long.MIN_VALUE, valueKind, false); diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java index 4bfa54ee549..8303920acd5 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -2833,23 +2833,23 @@ protected AnnotatedTypeMirror getIterableElementType( return dt.getTypeArguments().get(0); } - // TODO: Properly desugar Iterator.next(), which is needed if an annotated JDK has - // annotations on Iterator#next. - // The below doesn't work because methodFromUse() assumes that the expression tree - // matches the method element. - // TypeElement iteratorElement = - // ElementUtils.getTypeElement(processingEnv, Iterator.class); - // AnnotatedTypeMirror iteratorType = - // AnnotatedTypeMirror.createType(iteratorElement.asType(), this, false); - // Map mapping = new HashMap<>(); - // mapping.put( - // (TypeVariable) iteratorElement.getTypeParameters().get(0).asType(), - // typeArg); - // iteratorType = typeVarSubstitutor.substitute(mapping, iteratorType); - // ExecutableElement next = - // TreeUtils.getMethod("java.util.Iterator", "next", 0, processingEnv); - // ParameterizedExecutableType m = methodFromUse(expression, next, iteratorType); - // return m.executableType.getReturnType(); + // TODO: Properly desugar Iterator.next(), which is needed if an annotated JDK has + // annotations on Iterator#next. + // The below doesn't work because methodFromUse() assumes that the expression tree + // matches the method element. + // TypeElement iteratorElement = + // ElementUtils.getTypeElement(processingEnv, Iterator.class); + // AnnotatedTypeMirror iteratorType = + // AnnotatedTypeMirror.createType(iteratorElement.asType(), this, false); + // Map mapping = new HashMap<>(); + // mapping.put( + // (TypeVariable) iteratorElement.getTypeParameters().get(0).asType(), + // typeArg); + // iteratorType = typeVarSubstitutor.substitute(mapping, iteratorType); + // ExecutableElement next = + // TreeUtils.getMethod("java.util.Iterator", "next", 0, processingEnv); + // ParameterizedExecutableType m = methodFromUse(expression, next, iteratorType); + // return m.executableType.getReturnType(); default: throw new BugInCF( "AnnotatedTypeFactory.getIterableElementType: not iterable type: " diff --git a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java index 61dc17d5a01..aef2d003a88 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -2402,7 +2402,9 @@ public Store getEmptyStore() { * @see #getTypeFactoryOfSubchecker */ @SuppressWarnings("TypeParameterUnusedInFormals") // Intentional abuse - public > @Nullable T getTypeFactoryOfSubcheckerOrNull(Class subCheckerClass) { + public > + @Nullable T getTypeFactoryOfSubcheckerOrNull( + Class subCheckerClass) { BaseTypeChecker subchecker = checker.getSubchecker(subCheckerClass); if (subchecker == null) { return null; @@ -2664,8 +2666,8 @@ protected boolean isRelevantImpl(TypeMirror tm) { switch (tm.getKind()) { - // Primitives have no subtyping relationships, but the lookup might have failed - // because tm has metadata such as annotations. + // Primitives have no subtyping relationships, but the lookup might have failed + // because tm has metadata such as annotations. case BOOLEAN: case BYTE: case CHAR: @@ -2681,7 +2683,7 @@ protected boolean isRelevantImpl(TypeMirror tm) { } return false; - // Void is never relevant + // Void is never relevant case VOID: return false; diff --git a/framework/src/main/java/org/checkerframework/framework/util/JavaParserUtil.java b/framework/src/main/java/org/checkerframework/framework/util/JavaParserUtil.java index 97faa504467..870018a637e 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/JavaParserUtil.java +++ b/framework/src/main/java/org/checkerframework/framework/util/JavaParserUtil.java @@ -411,12 +411,12 @@ public static ParserConfiguration.LanguageLevel getCurrentSourceVersion( case "RELEASE_17": currentSourceVersion = ParserConfiguration.LanguageLevel.JAVA_17; break; - // JavaParser's ParserConfiguration.LanguageLevel has no constant for JDK 18, as - // of version 3.25.1 (2023-02-28). See - // https://www.javadoc.io/doc/com.github.javaparser/javaparser-core/latest/com/github/javaparser/ParserConfiguration.LanguageLevel.html . - // case "RELEASE_18": - // currentSourceVersion = ParserConfiguration.LanguageLevel.JAVA_18; - // break; + // JavaParser's ParserConfiguration.LanguageLevel has no constant for JDK 18, as + // of version 3.25.1 (2023-02-28). See + // https://www.javadoc.io/doc/com.github.javaparser/javaparser-core/latest/com/github/javaparser/ParserConfiguration.LanguageLevel.html . + // case "RELEASE_18": + // currentSourceVersion = ParserConfiguration.LanguageLevel.JAVA_18; + // break; default: currentSourceVersion = DEFAULT_LANGUAGE_LEVEL; } diff --git a/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java b/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java index a7b7c149fe8..4bab9d9688e 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java +++ b/framework/src/main/java/org/checkerframework/framework/util/defaults/QualifierDefaults.java @@ -582,9 +582,9 @@ private void applyDefaults(Tree tree, AnnotatedTypeMirror type) { elt = TreeUtils.elementFromUse((MethodInvocationTree) tree); break; - // TODO cases for array access, etc. -- every expression tree - // (The above probably means that we should use defaults in the - // scope of the declaration of the array. Is that right? -MDE) + // TODO cases for array access, etc. -- every expression tree + // (The above probably means that we should use defaults in the + // scope of the declaration of the array. Is that right? -MDE) default: // If no associated symbol was found, use the tree's (lexical) scope. diff --git a/framework/tests/all-systems/java17/SwitchTests.java b/framework/tests/all-systems/java17/SwitchTests.java index db96dff447d..faad3e33300 100644 --- a/framework/tests/all-systems/java17/SwitchTests.java +++ b/framework/tests/all-systems/java17/SwitchTests.java @@ -127,7 +127,7 @@ void fallthrough4(int myInt) { switch (myInt) { case 1: System.out.print("Hello "); - // Fall through to next case + // Fall through to next case case 2: System.out.println("World"); break; diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/CollectionUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/CollectionUtils.java index 0faf313b706..f1783877b1f 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/CollectionUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/CollectionUtils.java @@ -58,7 +58,8 @@ protected boolean removeEldestEntry(Map.Entry entry) { "nullness" // generics problem }) @Deprecated // 2023-06-02 - public static > @PolyNull C cloneElements(@PolyNull C orig) { + public static > + @PolyNull C cloneElements(@PolyNull C orig) { if (orig == null) { return null; } @@ -146,7 +147,8 @@ protected boolean removeEldestEntry(Map.Entry entry) { */ @Deprecated // 2023-06-02 @SuppressWarnings({"signedness", "nullness:argument"}) // problem with clone() - public static , C extends @Nullable Collection> @PolyNull C deepCopy(@PolyNull C orig) { + public static , C extends @Nullable Collection> + @PolyNull C deepCopy(@PolyNull C orig) { if (orig == null) { return null; } @@ -206,7 +208,8 @@ protected boolean removeEldestEntry(Map.Entry entry) { */ @Deprecated // 2023-06-02 @SuppressWarnings({"nullness", "signedness"}) // generics problem with clone - public static , M extends @Nullable Map> @PolyNull M deepCopyValues(@PolyNull M orig) { + public static , M extends @Nullable Map> + @PolyNull M deepCopyValues(@PolyNull M orig) { if (orig == null) { return null; } diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java index 6fbd74259f5..19a2985fc7f 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java @@ -692,8 +692,8 @@ public static VariableElement variableElementFromTree(Tree tree) { } switch (tree.getKind()) { - // symbol() only works on MethodSelects, so we need to get it manually - // for method invocations. + // symbol() only works on MethodSelects, so we need to get it manually + // for method invocations. case METHOD_INVOCATION: return TreeInfo.symbol(((JCMethodInvocation) tree).getMethodSelect()); @@ -2137,7 +2137,7 @@ public static boolean isWideningBinary(BinaryTree tree) { // These operators do binary promotion on the two arguments together. return true; - // TODO: CONDITIONAL_EXPRESSION (?:) sometimes does numeric promotion. + // TODO: CONDITIONAL_EXPRESSION (?:) sometimes does numeric promotion. default: return false; From 064d3279bfa8eeb3cf2c129152d5e75be2d840b1 Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Wed, 8 Jan 2025 19:41:57 -0500 Subject: [PATCH 05/13] Bump bazel-contrib/setup-bazel from 0.12.0 to 0.12.1 (#1056) --- .github/workflows/ci.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 5e7b6254033..b83b9af0da6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -38,7 +38,7 @@ jobs: uses: gradle/actions/setup-gradle@v4.2.2 - name: Setup Bazel - uses: bazel-contrib/setup-bazel@0.12.0 + uses: bazel-contrib/setup-bazel@0.12.1 if: ${{ matrix.script == 'cftests-nonjunit' }} with: # Avoid downloading Bazel every time. @@ -212,7 +212,7 @@ jobs: texlive-font-utils texlive-fonts-recommended texlive-latex-recommended pip install black flake8 html5validator - name: Setup Bazel - uses: bazel-contrib/setup-bazel@0.12.0 + uses: bazel-contrib/setup-bazel@0.12.1 if: ${{ matrix.script == 'cftests-nonjunit' }} with: # Avoid downloading Bazel every time. From 4935c5d74e2a26a2d52859075a10ac1f9fa42aad Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Sun, 12 Jan 2025 10:36:02 -0500 Subject: [PATCH 06/13] Remove unused static initializer block (#1057) --- .../framework/test/TestUtilities.java | 21 +++++++------------ 1 file changed, 8 insertions(+), 13 deletions(-) diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/TestUtilities.java b/framework-test/src/main/java/org/checkerframework/framework/test/TestUtilities.java index a7dda01afc2..ab4cf985122 100644 --- a/framework-test/src/main/java/org/checkerframework/framework/test/TestUtilities.java +++ b/framework-test/src/main/java/org/checkerframework/framework/test/TestUtilities.java @@ -11,13 +11,11 @@ import java.io.BufferedReader; import java.io.BufferedWriter; -import java.io.ByteArrayOutputStream; import java.io.File; import java.io.FileNotFoundException; import java.io.FileReader; import java.io.FileWriter; import java.io.IOException; -import java.io.OutputStream; import java.io.PrintWriter; import java.nio.file.FileAlreadyExistsException; import java.nio.file.Files; @@ -34,9 +32,7 @@ import java.util.StringJoiner; import javax.tools.Diagnostic; -import javax.tools.JavaCompiler; import javax.tools.JavaFileObject; -import javax.tools.ToolProvider; /** Utilities for testing. */ public class TestUtilities { @@ -80,12 +76,6 @@ public class TestUtilities { /** True if the JVM is version 21 or above. */ public static final boolean IS_AT_LEAST_21_JVM = SystemUtil.jreVersion >= 21; - static { - JavaCompiler compiler = ToolProvider.getSystemJavaCompiler(); - OutputStream err = new ByteArrayOutputStream(); - compiler.run(null, null, err, "-version"); - } - /** * Find test java sources within currentDir/tests. * @@ -120,7 +110,7 @@ public static List findRelativeNestedJavaFiles(File parent, String... dirN int i = 0; for (String dirName : dirNames) { dirs[i] = new File(parent, dirName); - i += 1; + ++i; } return getJavaFilesAsArgumentList(dirs); @@ -320,9 +310,15 @@ public static boolean isJavaTestFile(File file) { return true; } + /** + * Convert a compiler diagnostic to a string. + * + * @param diagnostic the compiler diagnostic + * @param usingAnomsgtxt whether message text should be excluded or not + * @return the compiler message string or null for certain lint warnings + */ public static @Nullable String diagnosticToString( Diagnostic diagnostic, boolean usingAnomsgtxt) { - String result = diagnostic.toString().trim(); // suppress Xlint warnings @@ -471,7 +467,6 @@ public static void writeDiagnostics( pw.println(); pw.println(); pw.flush(); - } catch (IOException e) { throw new RuntimeException(e); } From 730914af623fd1e7f5a71ddf8382db0633c7cc8f Mon Sep 17 00:00:00 2001 From: Alex Cook <43047600+thisisalexandercook@users.noreply.github.com> Date: Tue, 14 Jan 2025 20:24:11 -0500 Subject: [PATCH 07/13] Instanceof pattern variable nullness annotation checks (#1062) --- .../nullness/NullnessNoInitVisitor.java | 20 ++++++- .../nullness/java17/NullnessInstanceOf.java | 53 +++++++++++++++++++ docs/CHANGELOG.md | 5 +- 3 files changed, 75 insertions(+), 3 deletions(-) create mode 100644 checker/tests/nullness/java17/NullnessInstanceOf.java diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java index b358a74ab5f..2b85cf0efc9 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitVisitor.java @@ -55,6 +55,7 @@ import org.checkerframework.javacutil.TreePathUtil; import org.checkerframework.javacutil.TreeUtils; import org.checkerframework.javacutil.TreeUtilsAfterJava11; +import org.checkerframework.javacutil.TreeUtilsAfterJava11.BindingPatternUtils; import org.checkerframework.javacutil.TreeUtilsAfterJava11.SwitchExpressionUtils; import org.checkerframework.javacutil.TypesUtils; @@ -471,9 +472,23 @@ public Void visitInstanceOf(InstanceOfTree tree, Void p) { // Handle them properly. return null; } + + List annotations = null; if (refTypeTree.getKind() == Tree.Kind.ANNOTATED_TYPE) { - List annotations = - TreeUtils.annotationsFromTree((AnnotatedTypeTree) refTypeTree); + annotations = TreeUtils.annotationsFromTree((AnnotatedTypeTree) refTypeTree); + } else { + Tree patternTree = TreeUtilsAfterJava11.InstanceOfUtils.getPattern(tree); + if (patternTree != null && TreeUtils.isBindingPatternTree(patternTree)) { + VariableTree variableTree = BindingPatternUtils.getVariable(patternTree); + if (variableTree.getModifiers() != null) { + List annotationTree = + variableTree.getModifiers().getAnnotations(); + annotations = TreeUtils.annotationsFromTypeAnnotationTrees(annotationTree); + } + } + } + + if (annotations != null) { if (AnnotationUtils.containsSame(annotations, NULLABLE)) { checker.reportError(tree, "instanceof.nullable"); } @@ -481,6 +496,7 @@ public Void visitInstanceOf(InstanceOfTree tree, Void p) { checker.reportWarning(tree, "instanceof.nonnull.redundant"); } } + // Don't call super because it will issue an incorrect instanceof.unsafe warning. return null; } diff --git a/checker/tests/nullness/java17/NullnessInstanceOf.java b/checker/tests/nullness/java17/NullnessInstanceOf.java new file mode 100644 index 00000000000..f65b99629e6 --- /dev/null +++ b/checker/tests/nullness/java17/NullnessInstanceOf.java @@ -0,0 +1,53 @@ +// @below-java14-jdk-skip-test +import org.checkerframework.checker.nullness.qual.NonNull; +import org.checkerframework.checker.nullness.qual.Nullable; + +public class NullnessInstanceOf { + + public void testClassicInstanceOfNullable(Object x) { + // :: error: (instanceof.nullable) + if (x instanceof @Nullable String) { + System.out.println("Nullable String instanceof check."); + } + } + + public void testClassicInstanceOfNonNull(Object x) { + // :: warning: (instanceof.nonnull.redundant) + if (x instanceof @NonNull Number) { + System.out.println("NonNull Number instanceof check."); + } + } + + public void testPatternVariableNullable(Object x) { + // :: error: (instanceof.nullable) + if (x instanceof @Nullable String n) { + System.out.println("Length of String: " + n.length()); + } + } + + public void testPatternVariableNonNull(Object x) { + // :: warning: (instanceof.nonnull.redundant) + if (x instanceof @NonNull Number nn) { + System.out.println("Number's hashCode: " + nn.hashCode()); + } + } + + public void testUnannotatedClassic(Object x) { + if (x instanceof String) { + System.out.println("Unannotated String instanceof check."); + } + } + + public void testUnannotatedPatternVariable(Object x) { + if (x instanceof String unannotatedString) { + System.out.println("Unannotated String length: " + unannotatedString.length()); + } + } + + public void testUnusedPatternVariable(Object x) { + // :: error: (instanceof.nullable) + if (x instanceof @Nullable String unusedString) {} + // :: warning: (instanceof.nonnull.redundant) + if (x instanceof @NonNull Number unusedNumber) {} + } +} diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 73848a6b390..cf8806c2595 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -3,11 +3,14 @@ Version 3.42.0-eisop6 (January ??, 2025) **User-visible changes:** +The Nullness Checker now reports an error if any instanceof pattern variables are annotated with `@Nullable` +and a redundant warning if they are annotated with `@NonNull`. + **Implementation details:** **Closed issues:** -eisop#1003, eisop#1033. +eisop#1003, eisop#1033, eisop#1058. Version 3.42.0-eisop5 (December 20, 2024) From 17991582bc3a35509f15065b051d8e4c45c3e9ae Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Wed, 15 Jan 2025 18:43:56 -0500 Subject: [PATCH 08/13] Bump com.diffplug.spotless:spotless-plugin-gradle from 7.0.1 to 7.0.2 (#1063) --- build.gradle | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/build.gradle b/build.gradle index c1a30166329..a1e60e1efa6 100644 --- a/build.gradle +++ b/build.gradle @@ -6,7 +6,7 @@ buildscript { // Code formatting; defines targets "spotlessApply" and "spotlessCheck". // https://github.com/diffplug/spotless/tags ; see tags starting "gradle/" // Only works on JDK 11+. - classpath 'com.diffplug.spotless:spotless-plugin-gradle:7.0.1' + classpath 'com.diffplug.spotless:spotless-plugin-gradle:7.0.2' } } } From e126b05a4ab6910ae41b80ba2858561830e1e69c Mon Sep 17 00:00:00 2001 From: "dependabot[bot]" <49699333+dependabot[bot]@users.noreply.github.com> Date: Thu, 23 Jan 2025 09:47:26 -0500 Subject: [PATCH 09/13] Bump io.freefair.lombok from 8.11 to 8.12 in /docs/examples/lombok (#1070) --- docs/examples/lombok/build.gradle | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/examples/lombok/build.gradle b/docs/examples/lombok/build.gradle index d320fe13eaa..410b0c88be5 100644 --- a/docs/examples/lombok/build.gradle +++ b/docs/examples/lombok/build.gradle @@ -4,7 +4,7 @@ plugins { id 'java' - id 'io.freefair.lombok' version '8.11' + id 'io.freefair.lombok' version '8.12' // Checker Framework pluggable type-checking id 'org.checkerframework' version '0.6.48' } From 5499fb4570d4da994934f306508cf95ca967c13d Mon Sep 17 00:00:00 2001 From: "renovate[bot]" <29139614+renovate[bot]@users.noreply.github.com> Date: Sun, 26 Jan 2025 11:55:39 -0500 Subject: [PATCH 10/13] Update dependency gradle to v8.12.1 (#1072) --- gradle/wrapper/gradle-wrapper.properties | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/gradle/wrapper/gradle-wrapper.properties b/gradle/wrapper/gradle-wrapper.properties index cea7a793a84..e18bc253b85 100644 --- a/gradle/wrapper/gradle-wrapper.properties +++ b/gradle/wrapper/gradle-wrapper.properties @@ -1,6 +1,6 @@ distributionBase=GRADLE_USER_HOME distributionPath=wrapper/dists -distributionUrl=https\://services.gradle.org/distributions/gradle-8.12-bin.zip +distributionUrl=https\://services.gradle.org/distributions/gradle-8.12.1-bin.zip networkTimeout=10000 validateDistributionUrl=true zipStoreBase=GRADLE_USER_HOME From a014022eff779655fd2648001e2b81aa281655df Mon Sep 17 00:00:00 2001 From: "renovate[bot]" <29139614+renovate[bot]@users.noreply.github.com> Date: Sun, 26 Jan 2025 23:12:07 +0000 Subject: [PATCH 11/13] Update bazel-contrib/setup-bazel action to v0.13.0 (#1073) --- .github/workflows/ci.yml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b83b9af0da6..d6f6951c82c 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -38,7 +38,7 @@ jobs: uses: gradle/actions/setup-gradle@v4.2.2 - name: Setup Bazel - uses: bazel-contrib/setup-bazel@0.12.1 + uses: bazel-contrib/setup-bazel@0.13.0 if: ${{ matrix.script == 'cftests-nonjunit' }} with: # Avoid downloading Bazel every time. @@ -212,7 +212,7 @@ jobs: texlive-font-utils texlive-fonts-recommended texlive-latex-recommended pip install black flake8 html5validator - name: Setup Bazel - uses: bazel-contrib/setup-bazel@0.12.1 + uses: bazel-contrib/setup-bazel@0.13.0 if: ${{ matrix.script == 'cftests-nonjunit' }} with: # Avoid downloading Bazel every time. From ccfbe4b2269672ad0d29e48a4928e122514fe60b Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Tue, 28 Jan 2025 13:50:39 -0800 Subject: [PATCH 12/13] Fix a few Javadoc issues (#1075) --- .../substringindex/SubstringIndexAnnotatedTypeFactory.java | 4 ++-- .../framework/test/diagnostics/TestDiagnostic.java | 2 +- .../common/returnsreceiver/FluentAPIGenerator.java | 2 +- .../checkerframework/framework/stub/AnnotationFileParser.java | 2 +- .../framework/util/QualifierKindHierarchy.java | 2 +- 5 files changed, 6 insertions(+), 6 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/index/substringindex/SubstringIndexAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/index/substringindex/SubstringIndexAnnotatedTypeFactory.java index e5f5f2224a7..55f91d5e1c8 100644 --- a/checker/src/main/java/org/checkerframework/checker/index/substringindex/SubstringIndexAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/index/substringindex/SubstringIndexAnnotatedTypeFactory.java @@ -80,8 +80,8 @@ protected DependentTypesHelper createDependentTypesHelper() { /** * The Substring Index qualifier hierarchy. The hierarchy consists of a top element {@link - * UNKNOWN} of type {@link SubstringIndexUnknown}, bottom element {@link BOTTOM} of type {@link - * SubstringIndexBottom}, and elements of type {@link SubstringIndexFor} that follow the + * #UNKNOWN} of type {@link SubstringIndexUnknown}, bottom element {@link #BOTTOM} of type + * {@link SubstringIndexBottom}, and elements of type {@link SubstringIndexFor} that follow the * subtyping relation of {@link UBQualifier}. */ private final class SubstringIndexQualifierHierarchy extends ElementQualifierHierarchy { diff --git a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnostic.java b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnostic.java index 4c497203bbe..9e961dbe8ab 100644 --- a/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnostic.java +++ b/framework-test/src/main/java/org/checkerframework/framework/test/diagnostics/TestDiagnostic.java @@ -236,7 +236,7 @@ public int hashCode() { /** * Returns a representation of this diagnostic as if it appeared in a diagnostics file. This * uses only the base file name, not the full path, and only the message key, not the full - * message. Field {@link messageKeyParens} influences whether the message key is output in + * message. Field {@link #messageKeyParens} influences whether the message key is output in * parentheses. * * @return a representation of this diagnostic as if it appeared in a diagnostics file diff --git a/framework/src/main/java/org/checkerframework/common/returnsreceiver/FluentAPIGenerator.java b/framework/src/main/java/org/checkerframework/common/returnsreceiver/FluentAPIGenerator.java index 5a32a1a3130..16cd54eddea 100644 --- a/framework/src/main/java/org/checkerframework/common/returnsreceiver/FluentAPIGenerator.java +++ b/framework/src/main/java/org/checkerframework/common/returnsreceiver/FluentAPIGenerator.java @@ -51,7 +51,7 @@ private enum FluentAPIGenerators { /** * The qualified name of the AutoValue Builder annotation. This needs to be constructed * dynamically due to a side effect of the shadow plugin. See {@link - * getAutoValueBuilderCanonicalName()} for more information. + * #getAutoValueBuilderCanonicalName()} for more information. */ private final String AUTO_VALUE_BUILDER = getAutoValueBuilderCanonicalName(); diff --git a/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java b/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java index 866c00e3d1d..6b013084681 100644 --- a/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java +++ b/framework/src/main/java/org/checkerframework/framework/stub/AnnotationFileParser.java @@ -2070,7 +2070,7 @@ private void annotateTypeParameters( * zero or more mappings. Each mapping is from an element that {@code member} would override to * {@code member}. * - *

This method does not read or write field {@link annotationFileAnnos}. + *

This method does not read or write field {@link #annotationFileAnnos}. * * @param elementsToDecl the mapping that is side-effected by this method * @param fakeOverrideDecls fake overrides, also side-effected by this method diff --git a/framework/src/main/java/org/checkerframework/framework/util/QualifierKindHierarchy.java b/framework/src/main/java/org/checkerframework/framework/util/QualifierKindHierarchy.java index 3eddcfdee0c..fab9d20f63e 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/QualifierKindHierarchy.java +++ b/framework/src/main/java/org/checkerframework/framework/util/QualifierKindHierarchy.java @@ -30,7 +30,7 @@ * ElementQualifierHierarchy} (but not {@link MostlyNoElementQualifierHierarchy}) to * implement methods that compare {@link javax.lang.model.element.AnnotationMirror}s, such as {@link * org.checkerframework.framework.type.QualifierHierarchy#isSubtypeShallow(AnnotationMirror, - * TypeMirror, AnnotationMirror, TypeMirror)}. + * javax.lang.model.type.TypeMirror, AnnotationMirror, javax.lang.model.type.TypeMirror)}. * * @see DefaultQualifierKindHierarchy * @see org.checkerframework.framework.util.DefaultQualifierKindHierarchy.DefaultQualifierKind From e5589987c57f0d6a60f97bcfd520bdad182a8bb4 Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Wed, 29 Jan 2025 16:15:23 -0500 Subject: [PATCH 13/13] Fix intersection of wildcards with extends bounds (#1066) --- .../nullness/generics/WildcardBounds.java | 134 ++++++++++++++++++ .../generics/WildcardOverrideMore.java | 48 +++++++ docs/CHANGELOG.md | 2 + .../common/basetype/BaseTypeValidator.java | 7 + .../framework/type/DefaultTypeHierarchy.java | 49 +++++-- .../framework/util/AnnotatedTypes.java | 18 ++- .../tests/all-systems/WildcardInReturn.java | 25 ++++ .../tests/h1h2checker/WildcardBounds.java | 128 +++++++++++++++++ 8 files changed, 392 insertions(+), 19 deletions(-) create mode 100644 checker/tests/nullness/generics/WildcardBounds.java create mode 100644 checker/tests/nullness/generics/WildcardOverrideMore.java create mode 100644 framework/tests/all-systems/WildcardInReturn.java create mode 100644 framework/tests/h1h2checker/WildcardBounds.java diff --git a/checker/tests/nullness/generics/WildcardBounds.java b/checker/tests/nullness/generics/WildcardBounds.java new file mode 100644 index 00000000000..7faadc6add1 --- /dev/null +++ b/checker/tests/nullness/generics/WildcardBounds.java @@ -0,0 +1,134 @@ +import org.checkerframework.checker.nullness.qual.NonNull; +import org.checkerframework.checker.nullness.qual.Nullable; + +class WildcardBounds { + + abstract class OuterNbl { + abstract T get(); + + abstract class Inner { + abstract U get(); + + abstract class Chain { + abstract W get(); + } + + Object m0(Chain p) { + return p.get(); + } + + Object m1(Chain p) { + return p.get(); + } + + Object m2(Chain p) { + // :: error: (return.type.incompatible) + return p.get(); + } + + Object m3(Chain p) { + // :: error: (return.type.incompatible) + return p.get(); + } + + Object m4(Chain<@NonNull ?, @NonNull ?> p) { + return p.get(); + } + + void callsNonNull( + OuterNbl.Inner i, + OuterNbl.Inner.Chain n) { + i.m0(n); + i.m1(n); + i.m2(n); + i.m3(n); + i.m4(n); + } + + void callsNullable( + OuterNbl<@Nullable Object>.Inner<@Nullable Number> i, + OuterNbl<@Nullable Object>.Inner<@Nullable Number>.Chain< + @Nullable Integer, @Nullable Integer> + n) { + // :: error: (argument.type.incompatible) + i.m0(n); + // :: error: (argument.type.incompatible) + i.m1(n); + // OK + i.m2(n); + // OK + i.m3(n); + // :: error: (argument.type.incompatible) + i.m4(n); + } + } + + Object m0(Inner p) { + return p.get(); + } + + Object m1(Inner p) { + return p.get(); + } + + Object m2(Inner p) { + // :: error: (return.type.incompatible) + return p.get(); + } + + Object m3(Inner p) { + // :: error: (return.type.incompatible) + return p.get(); + } + + Object m4(Inner<@NonNull ?> p) { + return p.get(); + } + + // We could add calls for these methods. + } + + Object m0(OuterNbl p) { + return p.get(); + } + + Object m1(OuterNbl p) { + return p.get(); + } + + Object m2(OuterNbl p) { + // :: error: (return.type.incompatible) + return p.get(); + } + + Object m3(OuterNbl p) { + // :: error: (return.type.incompatible) + return p.get(); + } + + Object m4(OuterNbl<@NonNull ?> p) { + return p.get(); + } + + void callsOuter(OuterNbl s, OuterNbl<@Nullable String> ns) { + m0(s); + m1(s); + m2(s); + m3(s); + m4(s); + + // :: error: (argument.type.incompatible) + m0(ns); + // :: error: (argument.type.incompatible) + m1(ns); + // OK + m2(ns); + // OK + m3(ns); + // :: error: (argument.type.incompatible) + m4(ns); + } + + // We could add an OuterNonNull to also test with a non-null upper bound. + // But we probably already test that enough. +} diff --git a/checker/tests/nullness/generics/WildcardOverrideMore.java b/checker/tests/nullness/generics/WildcardOverrideMore.java new file mode 100644 index 00000000000..8e49434f8de --- /dev/null +++ b/checker/tests/nullness/generics/WildcardOverrideMore.java @@ -0,0 +1,48 @@ +import org.checkerframework.checker.nullness.qual.NonNull; +import org.checkerframework.checker.nullness.qual.Nullable; + +class WildcardOverrideMore { + interface Box {} + + interface Super { + void foo(Box lib); + + Box retfoo(); + + void bar(Box lib); + + Box retbar(); + } + + interface Sub extends Super { + @Override + void foo(Box lib); + + @Override + Box retfoo(); + + @Override + void bar(Box lib); + + @Override + Box retbar(); + } + + interface SubErrors extends Super { + @Override + // :: error: (override.param.invalid) + void foo(Box lib); + + @Override + // :: error: (override.return.invalid) + Box retfoo(); + + @Override + // :: error: (override.param.invalid) + void bar(Box<@NonNull ? super @NonNull W> lib); + + @Override + // :: error: (override.return.invalid) + Box<@Nullable ? super @NonNull W> retbar(); + } +} diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index cf8806c2595..5a852f11a74 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -8,6 +8,8 @@ and a redundant warning if they are annotated with `@NonNull`. **Implementation details:** +Fixed intersection of wildcards with extends bounds, to ensure the correct bounds are used. + **Closed issues:** eisop#1003, eisop#1033, eisop#1058. diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeValidator.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeValidator.java index 825bfb07400..5c609a25e4f 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeValidator.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeValidator.java @@ -628,6 +628,13 @@ protected Void visitParameterizedType(AnnotatedDeclaredType type, ParameterizedT if (!atypeFactory .getTypeHierarchy() .isSubtype(captureTypeVarUB, wildcard.getExtendsBound())) { + // For most captured type variables, this will trivially hold, as capturing + // incorporated the extends bound of the wildcard into the upper bound of the + // type variable. + // This will fail if the bound and the wildcard have generic types and there is + // no appropriate GLB. + // This issues an error for types that cannot be satisfied, because the two + // bounds have contradictory requirements. checker.reportError( tree.getTypeArguments().get(i), "type.argument.type.incompatible", diff --git a/framework/src/main/java/org/checkerframework/framework/type/DefaultTypeHierarchy.java b/framework/src/main/java/org/checkerframework/framework/type/DefaultTypeHierarchy.java index 0166487baa8..3a0ff8b650e 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/DefaultTypeHierarchy.java +++ b/framework/src/main/java/org/checkerframework/framework/type/DefaultTypeHierarchy.java @@ -82,7 +82,7 @@ public class DefaultTypeHierarchy extends AbstractAtmComboVisitor protected final StructuralEqualityVisitHistory areEqualVisitHistory; /** The Covariant.value field/element. */ - final ExecutableElement covariantValueElement; + protected final ExecutableElement covariantValueElement; /** * Creates a DefaultTypeHierarchy. @@ -392,8 +392,8 @@ protected boolean isContainedBy( areEqualVisitHistory.put(inside, outside, currentTop, result); return result; } - if ((TypesUtils.isCapturedTypeVariable(outside.getUnderlyingType()) - && !TypesUtils.isCapturedTypeVariable(inside.getUnderlyingType()))) { + if (TypesUtils.isCapturedTypeVariable(outside.getUnderlyingType()) + && !TypesUtils.isCapturedTypeVariable(inside.getUnderlyingType())) { // TODO: This branch should be removed after #979 is fixed. // This workaround is only needed when outside is a captured type variable, // but inside is not. @@ -977,33 +977,58 @@ public Boolean visitTypevar_Typevar( TypeMirror superTM = supertype.getUnderlyingType(); if (AnnotatedTypes.haveSameDeclaration(checker.getTypeUtils(), subtype, supertype)) { // The underlying types of subtype and supertype are uses of the same type parameter, - // but they - // may have different primary annotations. - boolean subtypeHasAnno = subtype.getAnnotationInHierarchy(currentTop) != null; - boolean supertypeHasAnno = supertype.getAnnotationInHierarchy(currentTop) != null; + // but they may have different primary annotations. + AnnotationMirror subtypeAnno = subtype.getAnnotationInHierarchy(currentTop); + boolean subtypeHasAnno = subtypeAnno != null; + AnnotationMirror supertypeAnno = supertype.getAnnotationInHierarchy(currentTop); + boolean supertypeHasAnno = supertypeAnno != null; if (subtypeHasAnno && supertypeHasAnno) { // If both have primary annotations then just check the primary annotations // as the bounds are the same. return isPrimarySubtype(subtype, supertype); } else if (!subtypeHasAnno && !supertypeHasAnno) { - // two unannotated uses of the same type parameter are of the same type - return areEqualInHierarchy(subtype, supertype); + // Two unannotated uses of the same type parameter need to compare + // both upper and lower bounds. + + // Upper bound of the subtype needs to be below the upper bound of the supertype. + if (!qualHierarchy.isSubtypeShallow( + subtype.getEffectiveAnnotationInHierarchy(currentTop), + subTM, + supertype.getEffectiveAnnotationInHierarchy(currentTop), + superTM)) { + return false; + } + + // Lower bound of the subtype needs to be below the lower bound of the supertype. + // TODO: Think through this and add better test coverage. + AnnotationMirrorSet subLBs = + AnnotatedTypes.findEffectiveLowerBoundAnnotations(qualHierarchy, subtype); + AnnotationMirror subLB = + qualHierarchy.findAnnotationInHierarchy(subLBs, currentTop); + AnnotationMirrorSet superLBs = + AnnotatedTypes.findEffectiveLowerBoundAnnotations(qualHierarchy, supertype); + AnnotationMirror superLB = + qualHierarchy.findAnnotationInHierarchy(superLBs, currentTop); + return qualHierarchy.isSubtypeShallow(subLB, subTM, superLB, superTM); } else if (subtypeHasAnno && !supertypeHasAnno) { // This is the case "@A T <: T" where T is a type variable. + // TODO: should this also test the upper bounds? AnnotationMirrorSet superLBs = AnnotatedTypes.findEffectiveLowerBoundAnnotations(qualHierarchy, supertype); AnnotationMirror superLB = qualHierarchy.findAnnotationInHierarchy(superLBs, currentTop); - return qualHierarchy.isSubtypeShallow( - subtype.getAnnotationInHierarchy(currentTop), subTM, superLB, superTM); + return qualHierarchy.isSubtypeShallow(subtypeAnno, subTM, superLB, superTM); } else if (!subtypeHasAnno && supertypeHasAnno) { // This is the case "T <: @A T" where T is a type variable. + // TODO: should this also test the lower bounds? return qualHierarchy.isSubtypeShallow( subtype.getEffectiveAnnotationInHierarchy(currentTop), subTM, - supertype.getAnnotationInHierarchy(currentTop), + supertypeAnno, superTM); + } else { + throw new BugInCF("Unreachable"); } } diff --git a/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java b/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java index 3d6429bb7ba..62c4c482ed6 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java +++ b/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java @@ -955,13 +955,17 @@ private static AnnotatedTypeMirror glbSubtype( if (subtype.getKind() != TypeKind.TYPEVAR) { throw new BugInCF("Missing primary annotations: subtype: %s", subtype); } - AnnotationMirrorSet lb = findEffectiveLowerBoundAnnotations(qualHierarchy, subtype); - AnnotationMirror lbAnno = qualHierarchy.findAnnotationInHierarchy(lb, top); - if (lbAnno != null - && !qualHierarchy.isSubtypeShallow(lbAnno, subTM, superAnno, superTM)) { - // The superAnno is lower than the lower bound annotation, so add it. - glb.addAnnotation(superAnno); - } // else don't add any annotation. + AnnotationMirror ubAnno = subtype.getEffectiveAnnotationInHierarchy(top); + if (!qualHierarchy.isSubtypeQualifiersOnly(ubAnno, superAnno)) { + // Instead of superAnno <: ubAnno check for ubAnno +// method return type: @UnknownVal TypeToken + +abstract class WildcardInReturn { + + abstract WildcardInReturn of(String key); + + abstract WildcardInReturn getSubtype(Class subclass); + + WildcardInReturn getSubtypeFromLowerBounds(Class subclass, String key) { + @SuppressWarnings("unchecked") // T's lower bound is + WildcardInReturn bound = (WildcardInReturn) of(key); + // Java supports only one lowerbound anyway. + return bound.getSubtype(subclass); + } +} diff --git a/framework/tests/h1h2checker/WildcardBounds.java b/framework/tests/h1h2checker/WildcardBounds.java new file mode 100644 index 00000000000..e2fa5f62bb4 --- /dev/null +++ b/framework/tests/h1h2checker/WildcardBounds.java @@ -0,0 +1,128 @@ +import org.checkerframework.framework.testchecker.h1h2checker.quals.H1S1; +import org.checkerframework.framework.testchecker.h1h2checker.quals.H1Top; + +class WildcardBounds { + + abstract class OuterTop { + abstract T get(); + + abstract class Inner { + abstract U get(); + + abstract class Chain { + abstract W get(); + } + + @H1S1 Object m0(Chain p) { + return p.get(); + } + + @H1S1 Object m1(Chain p) { + return p.get(); + } + + @H1S1 Object m2(Chain p) { + // :: error: (return.type.incompatible) + return p.get(); + } + + @H1S1 Object m3(Chain p) { + // :: error: (return.type.incompatible) + return p.get(); + } + + @H1S1 Object m4(Chain<@H1S1 ?, @H1S1 ?> p) { + return p.get(); + } + + void callsS1( + OuterTop<@H1S1 Object>.Inner<@H1S1 Number> i, + OuterTop<@H1S1 Object>.Inner<@H1S1 Number>.Chain<@H1S1 Integer, @H1S1 Integer> + n) { + i.m0(n); + i.m1(n); + i.m2(n); + i.m3(n); + i.m4(n); + } + + void callsTop( + OuterTop<@H1Top Object>.Inner<@H1Top Number> i, + OuterTop<@H1Top Object>.Inner<@H1Top Number>.Chain< + @H1Top Integer, @H1Top Integer> + n) { + // :: error: (argument.type.incompatible) + i.m0(n); + // :: error: (argument.type.incompatible) + i.m1(n); + // OK + i.m2(n); + // OK + i.m3(n); + // :: error: (argument.type.incompatible) + i.m4(n); + } + } + + @H1S1 Object m0(Inner p) { + return p.get(); + } + + @H1S1 Object m1(Inner p) { + return p.get(); + } + + @H1S1 Object m2(Inner p) { + // :: error: (return.type.incompatible) + return p.get(); + } + + @H1S1 Object m3(Inner p) { + // :: error: (return.type.incompatible) + return p.get(); + } + + @H1S1 Object m4(Inner<@H1S1 ?> p) { + return p.get(); + } + + // We could add calls for these methods. + } + + @H1S1 Object m0(OuterTop p) { + return p.get(); + } + + @H1S1 Object m1(OuterTop p) { + // :: error: (return.type.incompatible) + return p.get(); + } + + @H1S1 Object m2(OuterTop p) { + // :: error: (return.type.incompatible) + return p.get(); + } + + @H1S1 Object m3(OuterTop<@H1S1 ?> p) { + return p.get(); + } + + void callsOuter(OuterTop<@H1S1 String> s, OuterTop<@H1Top String> ns) { + m0(s); + m1(s); + m2(s); + m3(s); + + // :: error: (argument.type.incompatible) + m0(ns); + // OK + m1(ns); + // OK + m2(ns); + // :: error: (argument.type.incompatible) + m3(ns); + } + + // We could add an OuterS1 to also test with a non-top upper bound. + // But we probably already test that enough. +}