Fix initialization annotation of outer receiver with explicit annotation by byd110 · Pull Request #1253 · eisop/checker-framework

byd110 · 2025-06-10T19:22:31Z

Problem description

fix #412. The explicit enclosing receiver annotation is captured by the receiver type of the constructor but not annotated in InitializationParentAnnotatedTypeFactory.CommitmentTreeAnnotator#visitMethod.

This yeild a false positive during the check if we specify the enclosing receiver to be @UnknownInitialized, but in the method body check the type is the default @Initialized.

Fix

If the method visiting has an annotated receiver type, then retrive the annotation and annotate the enclosing receiver with it.

Two test cases are added to check this edge case. checker/tests/initialization/Issue412a.java checks the fix is correct. framework/tests/h1h2checker/Issue412b.java make sure the general framework can also catch this problem.

…roblem.

…he outer receiver when possible during tree annotation.

…ssue412

…he previous run on my local system

….java Co-authored-by: Aosen Xiong <aosen.xiong@uwaterloo.ca>

# Conflicts: # checker/tests/nullness-enclosingexpr/NullnessEnclosingExprTest.java

wmdietl

Great, thanks for tracking this down and fixing this bug!
Please add an entry in the changelog, at least that the issue is fixed.

wmdietl · 2025-06-23T23:06:55Z

                exeType.getReturnType().replaceAnnotation(a);
+
+                // If the receiver type exists (meaning there is an enclosing type) and is
+                // annotated, then annotate the enclosing type with the same annotation.


The "enclosing type" reference is unclear. It looks like it is being added to the enclosing type of the return type of the method.

wmdietl · 2025-06-23T23:07:37Z

+
+                // If the receiver type exists (meaning there is an enclosing type) and is
+                // annotated, then annotate the enclosing type with the same annotation.
+                // TODO: look into why there is this inconsistency between receiver type and


Is this a separate issue? Is this PR not fixing all of #412?

I would classify this as a saparate issue. getEnclosingType returns the enclsoing type with the correct annotation, whereas the enclosing type in the receiver is not annotated.

This PR fully fixes the problem. The inconsistency only affacts the way to get the correct annotation.

I haven't looked into the root cause of this consistency. There is also no failing test cases to show this inconsistency would cause any problem.

wmdietl · 2025-06-23T23:10:13Z

+                                exeType.getReceiverType().getAnnotationInHierarchy(a);
+                        AnnotatedDeclaredType ret = (AnnotatedDeclaredType) exeType.getReturnType();
+                        if (ret.getEnclosingType() != null) {
+                            ret.getEnclosingType().addAnnotation(enclAnno);


The return type of a constructor can never be explicitly written in source code, right?
So there never can already be a manually written annotation on the enclosing type.
So using addAnnotation instead of the replaceAnnotation that is used above is always correct?
Can you write a short comment that hints at that?

wmdietl · 2025-06-23T23:10:42Z

+                if (exeType.getReceiverType() != null) {
+                    if (exeType.getReceiverType().hasAnnotationInHierarchy(a)) {


Suggested change

if (exeType.getReceiverType() != null) {

if (exeType.getReceiverType().hasAnnotationInHierarchy(a)) {

if (exeType.getReceiverType() != null && exeType.getReceiverType().hasAnnotationInHierarchy(a)) {

To reduce nesting levels.

wmdietl · 2025-06-23T23:14:09Z

        super(testFiles, NullnessChecker.class, "nullness", "-AcheckEnclosingExpr");
    }

+    /**


To write down what we discussed in person: This change wouldn't be strictly necessary.
However, our javadoc enforcement script sees that there is a change to a file NullnessEnclosingExprTest.java and doesn't take the full paths into account - there is another file with that base name in this PR.
This seems unlikely to occur frequently, so we're punting on the issue.

wmdietl · 2025-06-23T23:15:41Z

+    }
+
+    Issue412a() {
+        new InnerWithUnknownInitializationEnclosingExpression();


Can you add another class with a constructor that has no @UnknownInitialization Issue412a Issue412a.this receiver and call it here, to ensure we do get an error for that illegal invocation. (Or rename InnerWithUnknownInitializationEnclosingExpression and have two constructors in it.)

wmdietl · 2025-06-23T23:32:23Z

+    }
+
+    class Inner {
+        /* The framework can correctly identify the outer class reciever type to be @H1Top.


Suggested change

/* The framework can correctly identify the outer class reciever type to be @H1Top.

/* The framework can correctly identify the outer class receiver type to be @H1Top.

wmdietl · 2025-06-23T23:32:42Z

@@ -0,0 +1,21 @@
+import org.checkerframework.framework.testchecker.h1h2checker.quals.*;
+
+// @skip-test


Should this be unskipped? If it should be skipped, is there a new issue you can reference?

Yes, it should be unskipped. The error reported rules out the problem with general framework.

wmdietl · 2025-06-23T23:36:13Z

@byd110 Issue #412 mentions a possible relation to #226. Did you look into that?

byd110 · 2025-06-24T00:08:52Z

@byd110 Issue #412 mentions a possible relation to #226. Did you look into that?

I looked into it. It's another problem regarding method overide.

… CHANGELOG.md.

…ed with correct "-AcheckEnclosingExpr" flag

…eFactory.java`

…ssue412

# Conflicts: # docs/CHANGELOG.md

…ssue412

# Conflicts: # docs/CHANGELOG.md

…anation, refine the comment in Issue412a test case

byd110 and others added 12 commits June 8, 2025 20:29

Add a test case using h1h2 checker to exclude the general framework p…

fc4c246

…roblem.

Add comments.

990c16c

A naive fix to InitializationParentAnnotatedTypeFactory to update t…

d12cd6f

…he outer receiver when possible during tree annotation.

Add test case for initialization checker to check this issue.

7d19ed5

Finalize the test cases Issue412a and Issue412b.

ca16f80

fix typo in the test cases

87eca4e

fix typo in the test cases

cffd968

Merge branch 'master' into issue412

63af8f4

add the expected error to the previous test cases about the same issue.

d6f172c

Merge branch 'issue412' of github.com:byd110/checker-framework into i…

2799c93

…ssue412

Commit again to rerun the CI test, which does not have the error as t…

f9b3c09

…he previous run on my local system

Merge branch 'master' into issue412

597e9fe

aosen-xiong reviewed Jun 19, 2025

View reviewed changes

Comment thread checker/tests/nullness-enclosingexpr/NullnessEnclosingExprTest.java Outdated

byd110 and others added 4 commits June 19, 2025 14:47

Update checker/tests/nullness-enclosingexpr/NullnessEnclosingExprTest…

f41e4ab

….java Co-authored-by: Aosen Xiong <aosen.xiong@uwaterloo.ca>

add javadoc to the junit file to see if this fix the CI failure.

55fb61d

Merge remote-tracking branch 'origin/issue412' into issue412

883dad9

# Conflicts: # checker/tests/nullness-enclosingexpr/NullnessEnclosingExprTest.java

Merge branch 'master' into issue412

805b3cc

wmdietl requested changes Jun 23, 2025

View reviewed changes

wmdietl assigned byd110 Jun 23, 2025

byd110 and others added 9 commits June 23, 2025 20:54

Merge branch 'master' into issue412

38f8160

Accepts suggestions to change code, add comments, and add an entry in…

007e5f8

… CHANGELOG.md.

Move Issue412a.java to another test directory so that it can be check…

8624d0d

…ed with correct "-AcheckEnclosingExpr" flag

fix the wrong diagnostics location

0a26e7c

add more explanation to the TODO in `InitializationParentAnnotatedTyp…

061e5bd

…eFactory.java`

add more explanation to the TODO in `InitializationParentAnnotatedTyp…

7d9ad8e

…eFactory.java`

Merge branch 'issue412' of github.com:byd110/checker-framework into i…

ec99d3c

…ssue412

Merge branch 'issue412' of github.com:byd110/checker-framework into i…

39492b4

…ssue412

Merge remote-tracking branch 'origin/issue412' into issue412

d678e50

byd110 and others added 14 commits July 2, 2025 00:36

Undo the change to CHANGELOG.md

4aa105d

Undo the change to CHANGELOG.md

c131c0b

Merge remote-tracking branch 'origin/issue412' into issue412

2a25d47

# Conflicts: # docs/CHANGELOG.md

Merge remote-tracking branch 'origin/issue412' into issue412

628ca8d

# Conflicts: # docs/CHANGELOG.md

Merge remote-tracking branch 'origin/issue412' into issue412

7034451

# Conflicts: # docs/CHANGELOG.md

Undo the changes to CHANGELOG.md

25f0835

Merge branch 'issue412' of github.com:byd110/checker-framework into i…

5776c49

…ssue412

Merge branch 'master' into issue412

7bfdbec

Merge branch 'issue412' of github.com:byd110/checker-framework into i…

aa58f0f

…ssue412

redo the changes to CHANGELOG.md

8d50ef1

Merge branch 'master' into issue412

2fae5ca

Merge remote-tracking branch 'origin/master' into issue412

6487514

# Conflicts: # docs/CHANGELOG.md

Merge branch 'master' into issue412

bdb37a7

remove the TODO in InitializationParentAnnotatedTypeFactory with expl…

e582b38

…anation, refine the comment in Issue412a test case

byd110 requested a review from wmdietl September 26, 2025 05:46

byd110 added 2 commits October 3, 2025 13:39

Merge branch 'master' into issue412

5dcf68e

Merge branch 'master' into issue412

e6405d7

		if (exeType.getReceiverType() != null) {
		if (exeType.getReceiverType().hasAnnotationInHierarchy(a)) {

	if (exeType.getReceiverType() != null) {
	if (exeType.getReceiverType().hasAnnotationInHierarchy(a)) {
	if (exeType.getReceiverType() != null && exeType.getReceiverType().hasAnnotationInHierarchy(a)) {

	/* The framework can correctly identify the outer class reciever type to be @H1Top.
	/* The framework can correctly identify the outer class receiver type to be @H1Top.

		@@ -0,0 +1,21 @@
		import org.checkerframework.framework.testchecker.h1h2checker.quals.*;

		// @skip-test

Uh oh!

Conversation

byd110 commented Jun 10, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Problem description

Fix

Uh oh!

Uh oh!

wmdietl left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

wmdietl commented Jun 23, 2025

Uh oh!

byd110 commented Jun 24, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

byd110 commented Jun 10, 2025 •

edited

Loading