From b5a5f260d7120d69bc54418e0d0fb4b29c17637c Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Fri, 27 Oct 2023 12:53:21 -0400 Subject: [PATCH 1/5] 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 95960617f61..3d2aad07349 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java @@ -1912,6 +1912,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 58bc84f520655e87b97b680b5beffb30cfb659d9 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Mon, 13 Nov 2023 10:25:55 -0500 Subject: [PATCH 2/5] 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 3d2aad07349..1b92f9ceb49 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java @@ -1912,7 +1912,7 @@ private void fixupBoundAnnotations() { if (lowerBound != null) { lowerBound.replaceAnnotations(newAnnos); } - this.getAnnotationsField().clear(); + this.getAnnotationsField().clear(); // clear annotations } } From dbd67acc91557a14e49583b09769a088b327c1b3 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Mon, 13 Nov 2023 11:34:23 -0500 Subject: [PATCH 3/5] 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 1b92f9ceb49..95960617f61 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeMirror.java @@ -1912,7 +1912,6 @@ private void fixupBoundAnnotations() { if (lowerBound != null) { lowerBound.replaceAnnotations(newAnnos); } - this.getAnnotationsField().clear(); // clear annotations } } From 554dee97a4945e4bea4cf38a64fb5453fe3ce1c8 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Mon, 13 Nov 2023 15:44:54 -0500 Subject: [PATCH 4/5] 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 f4e5394adefc4ef61b8ec88d2d2c25f6685e1f0c Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Sat, 18 Nov 2023 11:36:54 -0500 Subject: [PATCH 5/5] 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())) {