From c479361859a80ee53d2a808234bc2dc5f05a1f60 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Fri, 27 Oct 2023 12:53:21 -0400 Subject: [PATCH 01/11] fix viewpoint adaptation --- .../type/AbstractViewpointAdapter.java | 6 ++++++ .../framework/type/AnnotatedTypeMirror.java | 1 + .../viewpointtest/AnnoOnTypeVariableUse.java | 20 +++++++++++++++++++ 3 files changed, 27 insertions(+) create mode 100644 framework/tests/viewpointtest/AnnoOnTypeVariableUse.java diff --git a/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java b/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java index d85f0814579..fc4a96dbebf 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java @@ -8,6 +8,7 @@ import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedPrimitiveType; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedTypeVariable; import org.checkerframework.framework.type.AnnotatedTypeMirror.AnnotatedWildcardType; +import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.ElementUtils; import org.plumelib.util.IPair; @@ -408,6 +409,11 @@ private AnnotatedTypeMirror substituteTVars(AnnotatedTypeMirror lhs, AnnotatedTy // Base case where actual type argument is extracted if (lhs.getKind() == TypeKind.DECLARED) { rhs = getTypeVariableSubstitution((AnnotatedDeclaredType) lhs, atv); + if (AnnotationUtils.areSame( + atv.getLowerBound().getAnnotations(), + atv.getUpperBound().getAnnotations())) { + rhs.replaceAnnotations(atv.getLowerBound().getAnnotations()); + } } } else if (rhs.getKind() == TypeKind.DECLARED) { AnnotatedDeclaredType adt = (AnnotatedDeclaredType) rhs.shallowCopy(); diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java index afef59f6f87..58083cc25e6 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java @@ -1934,6 +1934,7 @@ private void fixupBoundAnnotations() { if (lowerBound != null) { lowerBound.replaceAnnotations(newAnnos); } + this.getAnnotationsField().clear(); } } diff --git a/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java b/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java new file mode 100644 index 00000000000..ed507fb97e5 --- /dev/null +++ b/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java @@ -0,0 +1,20 @@ +import viewpointtest.quals.*; + +@SuppressWarnings("cast.unsafe.constructor.invocation") +class AnnoOnTypeVariableUse { + @ReceiverDependentQual E element; + + // E element2; + + static void test() { + AnnoOnTypeVariableUse<@B Element> d = new @A AnnoOnTypeVariableUse<@B Element>(); + // d.element = @A |> @RDQ = @A + // thus expects no error here + d.element = new @A Element(); + // d.element2 = new @B Element(); + } +} + +class Element { + int f = 1; +} From 0b71144dc8a18059b726183e6b84b5c1962b1664 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Mon, 13 Nov 2023 10:25:55 -0500 Subject: [PATCH 02/11] add comments --- .../checkerframework/framework/type/AnnotatedTypeMirror.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java index 58083cc25e6..2d08d5efa59 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java @@ -1934,7 +1934,7 @@ private void fixupBoundAnnotations() { if (lowerBound != null) { lowerBound.replaceAnnotations(newAnnos); } - this.getAnnotationsField().clear(); + this.getAnnotationsField().clear(); // clear annotations } } From 3f4b065f5b545a221bfde01a33339a337f7029ea Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Mon, 13 Nov 2023 11:34:23 -0500 Subject: [PATCH 03/11] remove getannotationsfield().clear() --- .../org/checkerframework/framework/type/AnnotatedTypeMirror.java | 1 - 1 file changed, 1 deletion(-) diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java index 2d08d5efa59..afef59f6f87 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java @@ -1934,7 +1934,6 @@ private void fixupBoundAnnotations() { if (lowerBound != null) { lowerBound.replaceAnnotations(newAnnos); } - this.getAnnotationsField().clear(); // clear annotations } } From 7d78a7d2fbc1effa52abca9740cfe2f5071104f1 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Mon, 13 Nov 2023 15:44:54 -0500 Subject: [PATCH 04/11] reset annotated type variables in viewpoint adaptation --- .../framework/type/AbstractViewpointAdapter.java | 1 + framework/tests/viewpointtest/AnnoOnTypeVariableUse.java | 3 --- 2 files changed, 1 insertion(+), 3 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java b/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java index fc4a96dbebf..6467383b269 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java @@ -287,6 +287,7 @@ protected AnnotatedTypeMirror combineAnnotationWithType( combineAnnotationWithType(receiverAnnotation, atv.getLowerBound()); mappings.put(atv.getLowerBound(), resLower); + atv.clearAnnotations(); AnnotatedTypeMirror result = AnnotatedTypeCopierWithReplacement.replace(atv, mappings); diff --git a/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java b/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java index ed507fb97e5..c71c97abf3b 100644 --- a/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java +++ b/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java @@ -4,14 +4,11 @@ class AnnoOnTypeVariableUse { @ReceiverDependentQual E element; - // E element2; - static void test() { AnnoOnTypeVariableUse<@B Element> d = new @A AnnoOnTypeVariableUse<@B Element>(); // d.element = @A |> @RDQ = @A // thus expects no error here d.element = new @A Element(); - // d.element2 = new @B Element(); } } From 06c15e5b7de7093e13f76fec590db7eb8584afbe Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Sat, 18 Nov 2023 11:36:54 -0500 Subject: [PATCH 05/11] add comments --- .../type/AbstractViewpointAdapter.java | 20 ++++++++++++++++++- 1 file changed, 19 insertions(+), 1 deletion(-) diff --git a/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java b/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java index 6467383b269..e62afd33dce 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java @@ -286,7 +286,11 @@ protected AnnotatedTypeMirror combineAnnotationWithType( AnnotatedTypeMirror resLower = combineAnnotationWithType(receiverAnnotation, atv.getLowerBound()); mappings.put(atv.getLowerBound(), resLower); - + // The values of the mappings are the viewpoint adapted lower and upper bounds, + // and we wish to replace the old bounds of atv with the new mappings. + // However, we need to first remove the primary annotations of atv, otherwise + // in later replacement, the primary annotations would override our computed + // new mappings (see method fixupBoundAnnotations). atv.clearAnnotations(); AnnotatedTypeMirror result = AnnotatedTypeCopierWithReplacement.replace(atv, mappings); @@ -410,6 +414,20 @@ private AnnotatedTypeMirror substituteTVars(AnnotatedTypeMirror lhs, AnnotatedTy // Base case where actual type argument is extracted if (lhs.getKind() == TypeKind.DECLARED) { rhs = getTypeVariableSubstitution((AnnotatedDeclaredType) lhs, atv); + // When substituting an annotated type variable use (e.g., fields, return type), we + // don't want to replace the type qualifier of it with the qualifier on the + // type argument, as specified in + // https://checkerframework.org/manual/#type-variable-use. However, method + // getTypeVariableSubstitution will replace the annotated type qualifier as well. + // We fix up the substitution by checking if the types of the lower and upper bound + // are the same. If they are the same: (1) either the type variable use is + // annotated, and we need to fix up the + // primary annotation of the substituted result (rhs) by replacing it with the + // previous annotated type qualifier (from atv); (2) or the use is not annotated, + // but + // the type parameter is declared with the same upper and lower bounds, and it's no + // harm doing the same replacement as (1) because the qualifiers of the substituted + // result (rhs) and the old type variable use (atv) must be the same. if (AnnotationUtils.areSame( atv.getLowerBound().getAnnotations(), atv.getUpperBound().getAnnotations())) { From 584d98ff8e4a2f7679fed6cebc8f8d81e6ecbb85 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 3 Jul 2024 12:05:12 -0400 Subject: [PATCH 06/11] Refine the comment --- .../type/AbstractViewpointAdapter.java | 26 +++++++++---------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java b/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java index e62afd33dce..50adca6232f 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java @@ -414,20 +414,18 @@ private AnnotatedTypeMirror substituteTVars(AnnotatedTypeMirror lhs, AnnotatedTy // Base case where actual type argument is extracted if (lhs.getKind() == TypeKind.DECLARED) { rhs = getTypeVariableSubstitution((AnnotatedDeclaredType) lhs, atv); - // When substituting an annotated type variable use (e.g., fields, return type), we - // don't want to replace the type qualifier of it with the qualifier on the - // type argument, as specified in - // https://checkerframework.org/manual/#type-variable-use. However, method - // getTypeVariableSubstitution will replace the annotated type qualifier as well. - // We fix up the substitution by checking if the types of the lower and upper bound - // are the same. If they are the same: (1) either the type variable use is - // annotated, and we need to fix up the - // primary annotation of the substituted result (rhs) by replacing it with the - // previous annotated type qualifier (from atv); (2) or the use is not annotated, - // but - // the type parameter is declared with the same upper and lower bounds, and it's no - // harm doing the same replacement as (1) because the qualifiers of the substituted - // result (rhs) and the old type variable use (atv) must be the same. + // A type annotation on a use of a generic type variable overrides/ignores any type + // qualifier (in the same type hierarchy) on the corresponding actual type argument. + // See https://eisop.github.io/cf/manual/manual.html#type-variable-use + // However, #getTypeVariableSubstitution will replace the type qualifier with the + // qualifier on type variable declaration. + // Here check if the types of the lower and upper bound are the same. If they are: + // (1) If the type variable use is annotated, replacing the primary annotation of + // the substituted result (rhs) with the previous annotated type qualifier. + // (2) If the type variable use is not annotated and the type parameter is declared + // with the same upper and lower bounds, and doing the same replace as (1) is safe + // because the qualifiers of the substituted result (rhs) and the old type variable + // use (atv) are the same. if (AnnotationUtils.areSame( atv.getLowerBound().getAnnotations(), atv.getUpperBound().getAnnotations())) { From 371a623dbada5b25d8f4982a98f89c9ad598756c Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 3 Jul 2024 12:05:45 -0400 Subject: [PATCH 07/11] Test case with expected failure --- .../viewpointtest/AnnoOnTypeVariableUse.java | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) diff --git a/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java b/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java index c71c97abf3b..a5e7e987d81 100644 --- a/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java +++ b/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java @@ -3,12 +3,21 @@ @SuppressWarnings("cast.unsafe.constructor.invocation") class AnnoOnTypeVariableUse { @ReceiverDependentQual E element; + @A E a; + @B E b; - static void test() { - AnnoOnTypeVariableUse<@B Element> d = new @A AnnoOnTypeVariableUse<@B Element>(); + void test() { + AnnoOnTypeVariableUse<@B Element> d = new @A AnnoOnTypeVariableUse<>(); // d.element = @A |> @RDQ = @A - // thus expects no error here d.element = new @A Element(); + // d.a = @A |> @A = @A + d.a = new @A Element(); + // :: error: (assignment.type.incompatible) + d.a = new @B Element(); + // d.b = @B |> @B = @B + d.b = new @B Element(); + // :: error: (assignment.type.incompatible) + d.b = new @A Element(); } } From eb4a8bd29419f6495eba0623b92387fd92722e01 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 3 Jul 2024 17:40:53 -0400 Subject: [PATCH 08/11] Empty commit for CI From 48ef74505ca49d6b063befe48a040e7bf50d1b10 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Thu, 4 Jul 2024 17:12:49 -0400 Subject: [PATCH 09/11] Assign @B to effectively @A should fail --- framework/tests/viewpointtest/AnnoOnTypeVariableUse.java | 2 ++ 1 file changed, 2 insertions(+) diff --git a/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java b/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java index a5e7e987d81..6d368fd1ded 100644 --- a/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java +++ b/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java @@ -10,6 +10,8 @@ void test() { AnnoOnTypeVariableUse<@B Element> d = new @A AnnoOnTypeVariableUse<>(); // d.element = @A |> @RDQ = @A d.element = new @A Element(); + // :: error: (assignment.type.incompatible) + d.element = new @B Element(); // d.a = @A |> @A = @A d.a = new @A Element(); // :: error: (assignment.type.incompatible) From 46f8fba68fc8444a02fd8193910423c8a4de8b09 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Fri, 6 Sep 2024 14:39:18 -0400 Subject: [PATCH 10/11] Clear comment how the code change fix the problem --- .../framework/type/AbstractViewpointAdapter.java | 16 ++++------------ .../viewpointtest/AnnoOnTypeVariableUse.java | 12 +++++------- 2 files changed, 9 insertions(+), 19 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java b/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java index 50adca6232f..8e915942ff8 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AbstractViewpointAdapter.java @@ -413,19 +413,11 @@ private AnnotatedTypeMirror substituteTVars(AnnotatedTypeMirror lhs, AnnotatedTy // Base case where actual type argument is extracted if (lhs.getKind() == TypeKind.DECLARED) { + // Replace type variable with its actual type argument rhs = getTypeVariableSubstitution((AnnotatedDeclaredType) lhs, atv); - // A type annotation on a use of a generic type variable overrides/ignores any type - // qualifier (in the same type hierarchy) on the corresponding actual type argument. - // See https://eisop.github.io/cf/manual/manual.html#type-variable-use - // However, #getTypeVariableSubstitution will replace the type qualifier with the - // qualifier on type variable declaration. - // Here check if the types of the lower and upper bound are the same. If they are: - // (1) If the type variable use is annotated, replacing the primary annotation of - // the substituted result (rhs) with the previous annotated type qualifier. - // (2) If the type variable use is not annotated and the type parameter is declared - // with the same upper and lower bounds, and doing the same replace as (1) is safe - // because the qualifiers of the substituted result (rhs) and the old type variable - // use (atv) are the same. + // If the type variable use is annotated, the upperbound and lowerbound annotation + // on the type variable are the same. Replace the primary annotation of the + // substituted result (rhs) with annotation on type variable use. if (AnnotationUtils.areSame( atv.getLowerBound().getAnnotations(), atv.getUpperBound().getAnnotations())) { diff --git a/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java b/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java index 6d368fd1ded..784c6a07700 100644 --- a/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java +++ b/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java @@ -2,27 +2,25 @@ @SuppressWarnings("cast.unsafe.constructor.invocation") class AnnoOnTypeVariableUse { - @ReceiverDependentQual E element; + @ReceiverDependentQual E rdq; @A E a; @B E b; void test() { AnnoOnTypeVariableUse<@B Element> d = new @A AnnoOnTypeVariableUse<>(); // d.element = @A |> @RDQ = @A - d.element = new @A Element(); + d.rdq = new @A Element(); // :: error: (assignment.type.incompatible) - d.element = new @B Element(); + d.rdq = new @B Element(); // d.a = @A |> @A = @A d.a = new @A Element(); // :: error: (assignment.type.incompatible) d.a = new @B Element(); - // d.b = @B |> @B = @B + // d.b = @A |> @B = @B d.b = new @B Element(); // :: error: (assignment.type.incompatible) d.b = new @A Element(); } -} -class Element { - int f = 1; + class Element {} } From ed7cfbd9009194d77615b2ca4f0190df7a3ed3c9 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 18 Dec 2024 15:35:04 -0800 Subject: [PATCH 11/11] Also add unannotated type variable use in test --- framework/tests/viewpointtest/AnnoOnTypeVariableUse.java | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java b/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java index 784c6a07700..ca530274e20 100644 --- a/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java +++ b/framework/tests/viewpointtest/AnnoOnTypeVariableUse.java @@ -5,6 +5,7 @@ class AnnoOnTypeVariableUse { @ReceiverDependentQual E rdq; @A E a; @B E b; + E c; void test() { AnnoOnTypeVariableUse<@B Element> d = new @A AnnoOnTypeVariableUse<>(); @@ -20,6 +21,10 @@ void test() { d.b = new @B Element(); // :: error: (assignment.type.incompatible) d.b = new @A Element(); + // :: error: (assignment.type.incompatible) + d.c = new @A Element(); + // d.c = @B type argument subsitution with unannotated field + d.c = new @B Element(); } class Element {}