From c31ab6a60f5e784e737299f9568d6e0c619953e4 Mon Sep 17 00:00:00 2001 From: Aosen Xiong <82676488+Ao-senXiong@users.noreply.github.com> Date: Sun, 8 Dec 2024 17:13:43 -0800 Subject: [PATCH] Handle the `InitializationChecker` as upstream checker (#991) Co-authored-by: Werner Dietl --- .../initialization/InitializationChecker.java | 15 ++++++++++ .../InitializationFieldAccessSubchecker.java | 6 +++- .../AnnotatedForNullness.java | 29 ++++++++++++++++--- 3 files changed, 45 insertions(+), 5 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationChecker.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationChecker.java index a1b145647fc..8aa8cdd3db3 100644 --- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationChecker.java +++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationChecker.java @@ -12,6 +12,7 @@ import org.checkerframework.checker.nullness.qual.EnsuresNonNull; import org.checkerframework.checker.nullness.qual.NonNull; import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.checker.signature.qual.FullyQualifiedName; import org.checkerframework.common.basetype.BaseTypeChecker; import java.util.ArrayList; @@ -87,6 +88,20 @@ public InitializationChecker() {} */ public abstract Class getTargetCheckerClass(); + /** + * Also handle {@code AnnotatedFor} annotations for this checker. See {@link + * InitializationFieldAccessSubchecker#getUpstreamCheckerNames()} and the two implementations + * should be kept in sync. + */ + @Override + public List<@FullyQualifiedName String> getUpstreamCheckerNames() { + if (upstreamCheckerNames == null) { + super.getUpstreamCheckerNames(); + upstreamCheckerNames.add(InitializationChecker.class.getName()); + } + return upstreamCheckerNames; + } + @Override public NavigableSet getSuppressWarningsPrefixes() { NavigableSet result = super.getSuppressWarningsPrefixes(); diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationFieldAccessSubchecker.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationFieldAccessSubchecker.java index b4bae1887ba..0d3f5799020 100644 --- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationFieldAccessSubchecker.java +++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationFieldAccessSubchecker.java @@ -25,7 +25,11 @@ public class InitializationFieldAccessSubchecker extends BaseTypeChecker { /** Default constructor for InitializationFieldAccessSubchecker. */ public InitializationFieldAccessSubchecker() {} - /** Also handle {@code AnnotatedFor} annotations for the {@link InitializationChecker}. */ + /** + * Also handle {@code AnnotatedFor} annotations for the {@link InitializationChecker}. See + * {@link InitializationChecker#getUpstreamCheckerNames()} and the two implementations should be + * kept in sync. + */ @Override public List<@FullyQualifiedName String> getUpstreamCheckerNames() { if (upstreamCheckerNames == null) { diff --git a/checker/tests/nulless-conservative-defaults/annotatedfornullness/AnnotatedForNullness.java b/checker/tests/nulless-conservative-defaults/annotatedfornullness/AnnotatedForNullness.java index 70795715acc..b0c4472ec50 100644 --- a/checker/tests/nulless-conservative-defaults/annotatedfornullness/AnnotatedForNullness.java +++ b/checker/tests/nulless-conservative-defaults/annotatedfornullness/AnnotatedForNullness.java @@ -34,12 +34,13 @@ Object unannotatedFor(Object test) { @AnnotatedFor("nullness") void foo(@Initialized AnnotatedForNullness this) { - // Expect an error because conservative defaults are applied to `unannotatedFor` and it - // expects a @FBCBottom @KeyForBottom @Nonull Object. + // Expect two [argument.type.incompatible] errors in KeyForChecker and InitilizationChecker + // because conservative defaults are applied to `unannotatedFor` and it expects a @FBCBottom + // @KeyForBottom @Nonull Object. // ::error: (argument.type.incompatible) unannotatedFor(initializedField); - // Expect an error because conservative defaults are applied to `annotatedForInitialization` - // for hierarchies other than the Initialization Checker and + // Expect an error in KeyForChecker because conservative defaults are applied to + // `annotatedForInitialization` for hierarchies other than the Initialization Checker and // it expects an @Initialized @KeyForBottom @Nonull Object. // ::error: (argument.type.incompatible) annotatedForInitialization(initializedField); @@ -52,4 +53,24 @@ void foo(@Initialized AnnotatedForNullness this) { annotatedForNullness(initializedField); annotatedForNullnessAndInitialization(initializedField); } + + @AnnotatedFor("initialization") + void bar() { + // Expect an error in InitilizationChecker because conservative defaults are applied to + // `unannotatedFor` and it expects a @FBCBottom @UnknownKeyFor @Nonull Object. + // ::error: (argument.type.incompatible) + unannotatedFor(initializedField); + // Do not expect an error because the warning is suppressed other than initialzation + // hierarchy when conservative defaults are applied to source code and it expects an + // @Initialized @KeyForBottom @Nonull Object. + annotatedForInitialization(initializedField); + // Do not expect an error when conservative defaults are applied to + // `annotatedForInitialization` for hierarchies other than the Initialization Checker and + // it expects an @Initialized @KeyForBottom @Nonull Object. + annotatedForInitialization(initializedKeyForBottomField); + // Do not expect an error because these are AnnotatedFor("nullness") and these expect + // @Initialized @UnknownKeyFor @Nonnull Object. + annotatedForNullness(initializedField); + annotatedForNullnessAndInitialization(initializedField); + } }