From dbdcb1708ffe9bc0984c4a505a97c736ea69b9d3 Mon Sep 17 00:00:00 2001 From: Florian Lanzinger Date: Tue, 9 Jan 2024 21:08:35 +0100 Subject: [PATCH 1/4] Use adapted field types in initial store --- .../framework/flow/CFAbstractTransfer.java | 38 +++++++++++++----- .../ViewpointTestAnnotatedTypeFactory.java | 8 +--- .../ViewpointTestViewpointAdapter.java | 15 ++++++- .../test/java/viewpointtest/quals/Bottom.java | 2 +- .../src/test/java/viewpointtest/quals/C.java | 19 +++++++++ .../tests/viewpointtest/ReceiverAdaption.java | 40 +++++++++++++++++++ 6 files changed, 102 insertions(+), 20 deletions(-) create mode 100644 framework/src/test/java/viewpointtest/quals/C.java create mode 100644 framework/tests/viewpointtest/ReceiverAdaption.java diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index 8130f4aff65..00e175e3c34 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -53,6 +53,7 @@ import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeMirror; import org.checkerframework.framework.type.GenericAnnotatedTypeFactory; +import org.checkerframework.framework.util.AnnotatedTypes; import org.checkerframework.framework.util.Contract; import org.checkerframework.framework.util.Contract.ConditionalPostcondition; import org.checkerframework.framework.util.Contract.Postcondition; @@ -419,21 +420,36 @@ private void addInitialFieldValues(S store, ClassTree classTree, MethodTree meth continue; } - boolean isFieldOfCurrentClass = varEle.getEnclosingElement().equals(classEle); - // Maybe insert the declared type: - if (!isConstructor) { - // If it's not a constructor, use the declared type if the receiver of the method is - // fully initialized. - boolean isInitializedReceiver = !isNotFullyInitializedReceiver(methodTree); - if (isInitializedReceiver && isFieldOfCurrentClass) { - store.insertValue(fieldInitialValue.fieldDecl, fieldInitialValue.declared); - } - } else { + // If the field belongs to another class, don't add it to the store. + if (!varEle.getEnclosingElement().equals(classEle)) { + continue; + } + + // Maybe insert the adapted or declared field type: + if (isConstructor) { // If it is a constructor, then only use the declared type if the field has been // initialized. - if (fieldInitialValue.initializer != null && isFieldOfCurrentClass) { + if (fieldInitialValue.initializer != null) { store.insertValue(fieldInitialValue.fieldDecl, fieldInitialValue.declared); } + } else if (!isStaticMethod) { + // If it's a non-constructor object method, + // use the adapted type if the receiver of the method is + // fully initialized. + analysis.getTypeFactory().getAnnotatedType(fieldInitialValue.fieldDecl.getField()); + AnnotatedTypeMirror receiverType = + analysis.getTypeFactory().getSelfType(methodTree.getBody()); + AnnotatedTypeMirror adaptedType = + AnnotatedTypes.asMemberOf( + analysis.getTypes(), + analysis.getTypeFactory(), + receiverType, + fieldInitialValue.fieldDecl.getField()); + store.insertValue( + fieldInitialValue.fieldDecl, analysis.createAbstractValue(adaptedType)); + } else { + // If it's a static method, use the declared type. + store.insertValue(fieldInitialValue.fieldDecl, fieldInitialValue.declared); } } } diff --git a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java index f2027bae843..5a51de0c855 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java @@ -7,12 +7,7 @@ import java.lang.annotation.Annotation; import java.util.Set; -import viewpointtest.quals.A; -import viewpointtest.quals.B; -import viewpointtest.quals.Bottom; -import viewpointtest.quals.PolyVP; -import viewpointtest.quals.ReceiverDependentQual; -import viewpointtest.quals.Top; +import viewpointtest.quals.*; public class ViewpointTestAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { @@ -26,6 +21,7 @@ protected Set> createSupportedTypeQualifiers() { return getBundledTypeQualifiers( A.class, B.class, + C.class, Bottom.class, PolyVP.class, ReceiverDependentQual.class, diff --git a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java index 9da9504eead..ba715b46541 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestViewpointAdapter.java @@ -8,12 +8,14 @@ import javax.lang.model.element.AnnotationMirror; +import viewpointtest.quals.A; +import viewpointtest.quals.C; import viewpointtest.quals.ReceiverDependentQual; import viewpointtest.quals.Top; public class ViewpointTestViewpointAdapter extends AbstractViewpointAdapter { - private final AnnotationMirror TOP, RECEIVERDEPENDENTQUAL; + private final AnnotationMirror TOP, RECEIVERDEPENDENTQUAL, A, C; /** * The class constructor. @@ -26,6 +28,8 @@ public ViewpointTestViewpointAdapter(AnnotatedTypeFactory atypeFactory) { RECEIVERDEPENDENTQUAL = AnnotationBuilder.fromClass( atypeFactory.getElementUtils(), ReceiverDependentQual.class); + A = AnnotationBuilder.fromClass(atypeFactory.getElementUtils(), A.class); + C = AnnotationBuilder.fromClass(atypeFactory.getElementUtils(), C.class); } @Override @@ -39,7 +43,14 @@ protected AnnotationMirror combineAnnotationWithAnnotation( if (AnnotationUtils.areSame(declaredAnnotation, RECEIVERDEPENDENTQUAL)) { return receiverAnnotation; + } else if (AnnotationUtils.areSame(declaredAnnotation, C)) { + if (AnnotationUtils.areSame(receiverAnnotation, TOP)) { + return TOP; + } else { + return C; + } + } else { + return declaredAnnotation; } - return declaredAnnotation; } } diff --git a/framework/src/test/java/viewpointtest/quals/Bottom.java b/framework/src/test/java/viewpointtest/quals/Bottom.java index 484726ae7f4..f5066cfcf59 100644 --- a/framework/src/test/java/viewpointtest/quals/Bottom.java +++ b/framework/src/test/java/viewpointtest/quals/Bottom.java @@ -13,6 +13,6 @@ @Documented @Retention(RetentionPolicy.RUNTIME) @Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) -@SubtypeOf({A.class, B.class, ReceiverDependentQual.class}) +@SubtypeOf({A.class, B.class, C.class, ReceiverDependentQual.class}) @DefaultFor(TypeUseLocation.LOWER_BOUND) public @interface Bottom {} diff --git a/framework/src/test/java/viewpointtest/quals/C.java b/framework/src/test/java/viewpointtest/quals/C.java new file mode 100644 index 00000000000..0caeaef2a1e --- /dev/null +++ b/framework/src/test/java/viewpointtest/quals/C.java @@ -0,0 +1,19 @@ +package viewpointtest.quals; + +import org.checkerframework.framework.qual.SubtypeOf; + +import java.lang.annotation.Documented; +import java.lang.annotation.ElementType; +import java.lang.annotation.Retention; +import java.lang.annotation.RetentionPolicy; +import java.lang.annotation.Target; + +/** + * Unlike {@link A} and {@link B}, this qualifier is adapted to {@link Top} whenever it appears on a + * field of a {@link Top} receiver. In all other cases, it stays {@code C}. + */ +@Documented +@Retention(RetentionPolicy.RUNTIME) +@Target({ElementType.TYPE_USE, ElementType.TYPE_PARAMETER}) +@SubtypeOf({Top.class}) +public @interface C {} diff --git a/framework/tests/viewpointtest/ReceiverAdaption.java b/framework/tests/viewpointtest/ReceiverAdaption.java new file mode 100644 index 00000000000..c7e40978ed5 --- /dev/null +++ b/framework/tests/viewpointtest/ReceiverAdaption.java @@ -0,0 +1,40 @@ +import viewpointtest.quals.*; + +public class ReceiverAdaption { + + @ReceiverDependentQual Object dependent; + + @C Object c; + + void testA(@A ReceiverAdaption this) { + @A Object varA = dependent; + // :: error: (assignment.type.incompatible) + @B Object varB = dependent; + @C Object varC = c; + // :: error: (assignment.type.incompatible) + @A Object varAc = c; + // :: error: (assignment.type.incompatible) + @B Object varBc = c; + } + + void testB(@B ReceiverAdaption this) { + // :: error: (assignment.type.incompatible) + @A Object varA = dependent; + @B Object varB = dependent; + @C Object varC = c; + // :: error: (assignment.type.incompatible) + @A Object varAc = c; + // :: error: (assignment.type.incompatible) + @B Object varBc = c; + } + + void testTop(@Top ReceiverAdaption this) { + // :: error: (assignment.type.incompatible) + @A Object varA = dependent; + // :: error: (assignment.type.incompatible) + @B Object varB = dependent; + // :: error: (assignment.type.incompatible) + @C Object varC = c; + @Top Object varT = c; + } +} From bff38318b33e64f0dec56eb2709c628155aef820 Mon Sep 17 00:00:00 2001 From: Florian Lanzinger Date: Fri, 12 Jan 2024 19:04:55 +0100 Subject: [PATCH 2/4] Only use adapted field type for initialized receivers --- .../framework/flow/CFAbstractTransfer.java | 25 +++++++++++-------- 1 file changed, 14 insertions(+), 11 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index 00e175e3c34..82752f63057 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -436,17 +436,20 @@ private void addInitialFieldValues(S store, ClassTree classTree, MethodTree meth // If it's a non-constructor object method, // use the adapted type if the receiver of the method is // fully initialized. - analysis.getTypeFactory().getAnnotatedType(fieldInitialValue.fieldDecl.getField()); - AnnotatedTypeMirror receiverType = - analysis.getTypeFactory().getSelfType(methodTree.getBody()); - AnnotatedTypeMirror adaptedType = - AnnotatedTypes.asMemberOf( - analysis.getTypes(), - analysis.getTypeFactory(), - receiverType, - fieldInitialValue.fieldDecl.getField()); - store.insertValue( - fieldInitialValue.fieldDecl, analysis.createAbstractValue(adaptedType)); + if (!isNotFullyInitializedReceiver(methodTree)) { + analysis.getTypeFactory() + .getAnnotatedType(fieldInitialValue.fieldDecl.getField()); + AnnotatedTypeMirror receiverType = + analysis.getTypeFactory().getSelfType(methodTree.getBody()); + AnnotatedTypeMirror adaptedType = + AnnotatedTypes.asMemberOf( + analysis.getTypes(), + analysis.getTypeFactory(), + receiverType, + fieldInitialValue.fieldDecl.getField()); + store.insertValue( + fieldInitialValue.fieldDecl, analysis.createAbstractValue(adaptedType)); + } } else { // If it's a static method, use the declared type. store.insertValue(fieldInitialValue.fieldDecl, fieldInitialValue.declared); From f548d475139a43fefd1d481ef742468af5b9b38c Mon Sep 17 00:00:00 2001 From: Florian Lanzinger Date: Fri, 12 Jan 2024 21:15:33 +0100 Subject: [PATCH 3/4] Fix bug where dependent types were added to the store in non-normalized state --- .../framework/flow/CFAbstractAnalysis.java | 10 +++---- .../framework/flow/CFAbstractTransfer.java | 29 +++++++++---------- .../type/GenericAnnotatedTypeFactory.java | 6 ++-- 3 files changed, 20 insertions(+), 25 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java index f98260e8876..23b74ab65ec 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractAnalysis.java @@ -72,8 +72,8 @@ public static class FieldInitialValue> { /** A field access that corresponds to the declaration of a field. */ public final FieldAccess fieldDecl; - /** The value corresponding to the annotations on the declared type of the field. */ - public final V declared; + /** The declared type of the field. */ + public final AnnotatedTypeMirror declared; /** The value of the initializer of the field, or null if no initializer exists. */ public final @Nullable V initializer; @@ -82,12 +82,12 @@ public static class FieldInitialValue> { * Creates a new FieldInitialValue. * * @param fieldDecl a field access that corresponds to the declaration of a field - * @param declared value corresponding to the annotations on the declared type of {@code - * field} + * @param declared declared type of {@code field} * @param initializer value of the initializer of {@code field}, or null if no initializer * exists */ - public FieldInitialValue(FieldAccess fieldDecl, V declared, @Nullable V initializer) { + public FieldInitialValue( + FieldAccess fieldDecl, AnnotatedTypeMirror declared, @Nullable V initializer) { this.fieldDecl = fieldDecl; this.declared = declared; this.initializer = initializer; diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index 82752f63057..3f71fe1e298 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -426,19 +426,15 @@ private void addInitialFieldValues(S store, ClassTree classTree, MethodTree meth } // Maybe insert the adapted or declared field type: - if (isConstructor) { - // If it is a constructor, then only use the declared type if the field has been - // initialized. - if (fieldInitialValue.initializer != null) { - store.insertValue(fieldInitialValue.fieldDecl, fieldInitialValue.declared); - } + V value = null; + if ((isConstructor || isStaticMethod) && fieldInitialValue.initializer != null) { + // If it is a constructor or static method, then use the declared type + // if the field has been initialized. + value = analysis.createAbstractValue(fieldInitialValue.declared); } else if (!isStaticMethod) { // If it's a non-constructor object method, - // use the adapted type if the receiver of the method is - // fully initialized. + // use the adapted type if the receiver of the method is fully initialized. if (!isNotFullyInitializedReceiver(methodTree)) { - analysis.getTypeFactory() - .getAnnotatedType(fieldInitialValue.fieldDecl.getField()); AnnotatedTypeMirror receiverType = analysis.getTypeFactory().getSelfType(methodTree.getBody()); AnnotatedTypeMirror adaptedType = @@ -446,14 +442,15 @@ private void addInitialFieldValues(S store, ClassTree classTree, MethodTree meth analysis.getTypes(), analysis.getTypeFactory(), receiverType, - fieldInitialValue.fieldDecl.getField()); - store.insertValue( - fieldInitialValue.fieldDecl, analysis.createAbstractValue(adaptedType)); + fieldInitialValue.fieldDecl.getField(), + fieldInitialValue.declared); + value = analysis.createAbstractValue(adaptedType); + if (value == null) { + value = analysis.createAbstractValue(fieldInitialValue.declared); + } } - } else { - // If it's a static method, use the declared type. - store.insertValue(fieldInitialValue.fieldDecl, fieldInitialValue.declared); } + store.insertValue(fieldInitialValue.fieldDecl, value); } } 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 1ee058ca562..88b5fefbc92 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -1459,7 +1459,6 @@ protected void performFlowAnalysis(ClassTree classTree) { VariableTree vt = (VariableTree) m; ExpressionTree initializer = vt.getInitializer(); AnnotatedTypeMirror declaredType = getAnnotatedTypeLhs(vt); - Value declaredValue = analysis.createAbstractValue(declaredType); FieldAccess fieldExpr = (FieldAccess) JavaExpression.fromVariableTree(vt); // analyze initializer if present @@ -1480,12 +1479,11 @@ protected void performFlowAnalysis(ClassTree classTree) { if (initializerValue != null) { fieldValues.add( new FieldInitialValue<>( - fieldExpr, declaredValue, initializerValue)); + fieldExpr, declaredType, initializerValue)); break; } } - fieldValues.add( - new FieldInitialValue<>(fieldExpr, declaredValue, null)); + fieldValues.add(new FieldInitialValue<>(fieldExpr, declaredType, null)); break; case BLOCK: BlockTree b = (BlockTree) m; From cf7d72556fc739da9996e308919aed13fd5344e1 Mon Sep 17 00:00:00 2001 From: Florian Lanzinger Date: Mon, 15 Jan 2024 17:39:38 +0100 Subject: [PATCH 4/4] Don't use wildcard imports --- .../viewpointtest/ViewpointTestAnnotatedTypeFactory.java | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java index 5a51de0c855..548a7e3d19b 100644 --- a/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java +++ b/framework/src/test/java/viewpointtest/ViewpointTestAnnotatedTypeFactory.java @@ -7,7 +7,13 @@ import java.lang.annotation.Annotation; import java.util.Set; -import viewpointtest.quals.*; +import viewpointtest.quals.A; +import viewpointtest.quals.B; +import viewpointtest.quals.Bottom; +import viewpointtest.quals.C; +import viewpointtest.quals.PolyVP; +import viewpointtest.quals.ReceiverDependentQual; +import viewpointtest.quals.Top; public class ViewpointTestAnnotatedTypeFactory extends BaseAnnotatedTypeFactory {