From c3a799d78a7d549617cbbd5e5ba4b8a2ca74afe2 Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Mon, 20 Jan 2025 20:17:14 -0500 Subject: [PATCH 1/6] For GLBs of type variables, only change the upper bound --- .../framework/util/AnnotatedTypes.java | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) 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..b9440ef83af 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,15 @@ 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(superAnno, ubAnno)) { + // We know that `glb` is a type variable, because `subtype` is. + // Do not add the annotation to the type variable itself, because that would + // change the upper and the lower bound. + // Adding the more restrictive `superAnno` only to the upper bound ensures that + // the type variable is below `superAnno`. + ((AnnotatedTypeVariable) glb).getUpperBound().replaceAnnotation(superAnno); + } } else { throw new BugInCF("GLB: subtype: %s, supertype: %s", subtype, supertype); } From a8fa9a5f69592be4c57e92431f433a979da55a0d Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Mon, 20 Jan 2025 20:18:07 -0500 Subject: [PATCH 2/6] When comparing type variables, check upper and lower bounds separately --- .../framework/type/DefaultTypeHierarchy.java | 49 ++++++++++++++----- 1 file changed, 37 insertions(+), 12 deletions(-) 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"); } } From 07c24ce6406ac2c06f225f8d7f94873da98b997b Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Mon, 20 Jan 2025 20:18:43 -0500 Subject: [PATCH 3/6] Tests for wildcards with extends bounds --- .../nullness/generics/WildcardBounds.java | 134 ++++++++++++++++++ .../tests/h1h2checker/WildcardBounds.java | 128 +++++++++++++++++ 2 files changed, 262 insertions(+) create mode 100644 checker/tests/nullness/generics/WildcardBounds.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/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. +} From 645dddb24780a2cdaa161c78a71499ba1b1551a5 Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Tue, 21 Jan 2025 18:48:11 -0500 Subject: [PATCH 4/6] Tweak logic --- .../org/checkerframework/framework/util/AnnotatedTypes.java | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) 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 b9440ef83af..29f10f198ab 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java +++ b/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java @@ -956,7 +956,10 @@ private static AnnotatedTypeMirror glbSubtype( throw new BugInCF("Missing primary annotations: subtype: %s", subtype); } AnnotationMirror ubAnno = subtype.getEffectiveAnnotationInHierarchy(top); - if (qualHierarchy.isSubtypeQualifiersOnly(superAnno, ubAnno)) { + if (!qualHierarchy.isSubtypeQualifiersOnly(ubAnno, superAnno)) { + // if (qualHierarchy.isSubtypeQualifiersOnly(superAnno, ubAnno)) { + // Instead of superAnno <: ubAnno check for ubAnno Date: Tue, 21 Jan 2025 18:49:09 -0500 Subject: [PATCH 5/6] Add minimized tests of CI failures --- .../generics/WildcardOverrideMore.java | 48 +++++++++++++++++++ .../tests/all-systems/WildcardInReturn.java | 25 ++++++++++ 2 files changed, 73 insertions(+) create mode 100644 checker/tests/nullness/generics/WildcardOverrideMore.java create mode 100644 framework/tests/all-systems/WildcardInReturn.java 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/framework/tests/all-systems/WildcardInReturn.java b/framework/tests/all-systems/WildcardInReturn.java new file mode 100644 index 00000000000..7c9c785e820 --- /dev/null +++ b/framework/tests/all-systems/WildcardInReturn.java @@ -0,0 +1,25 @@ +// Minimized test case from +// +// https://github.com/eisop/guava/blob/290cfe5c926de28cfdda491535901b09bab90ef9/guava/src/com/google/common/reflect/TypeToken.java#L1228 +// which failed in https://github.com/eisop/checker-framework/pull/1066 with: +// +// guava/guava/src/com/google/common/reflect/TypeToken.java:[1228,29] error: [[value, +// allcheckers]:return.type.incompatible] incompatible types in return. +// type of expression: @UnknownVal TypeToken +// 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); + } +} From b403b49856e9fd630fd5edd29758c61a19e106e8 Mon Sep 17 00:00:00 2001 From: Werner Dietl Date: Tue, 21 Jan 2025 21:12:46 -0500 Subject: [PATCH 6/6] Remove old code comment --- .../java/org/checkerframework/framework/util/AnnotatedTypes.java | 1 - 1 file changed, 1 deletion(-) 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 29f10f198ab..62c4c482ed6 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java +++ b/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java @@ -957,7 +957,6 @@ private static AnnotatedTypeMirror glbSubtype( } AnnotationMirror ubAnno = subtype.getEffectiveAnnotationInHierarchy(top); if (!qualHierarchy.isSubtypeQualifiersOnly(ubAnno, superAnno)) { - // if (qualHierarchy.isSubtypeQualifiersOnly(superAnno, ubAnno)) { // Instead of superAnno <: ubAnno check for ubAnno