From 620fab90adb06ad82f3b1dcf8c91cd66f0bb6fea Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Mon, 11 Apr 2022 10:18:16 -0400 Subject: [PATCH 1/9] add receiver refinement in getAnnotatedTypeLhs --- .../framework/type/GenericAnnotatedTypeFactory.java | 13 +++++++++++-- 1 file changed, 11 insertions(+), 2 deletions(-) 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 9b022eff62a0..a25643811e7b 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -1626,6 +1626,15 @@ public AnnotatedTypeMirror getAnnotatedTypeLhsNoTypeVarDefault(Tree lhsTree) { return type; } + @Override + public AnnotatedTypeMirror getAnnotatedType(Tree tree) { + boolean oldUseFlow = useFlow; + useFlow = true; // what if the useFlow passes in is false? + AnnotatedTypeMirror res = super.getAnnotatedType(tree); + useFlow = oldUseFlow; + return res; + } + /** * Returns the type of a left-hand side of an assignment. * @@ -1648,7 +1657,7 @@ public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree) { case IDENTIFIER: case MEMBER_SELECT: case ARRAY_ACCESS: - res = getAnnotatedType(lhsTree); + res = super.getAnnotatedType(lhsTree); break; case PARENTHESIZED: res = getAnnotatedTypeLhs(TreeUtils.withoutParens((ExpressionTree) lhsTree)); @@ -1657,7 +1666,7 @@ public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree) { if (TreeUtils.isTypeTree(lhsTree)) { // lhsTree is a type tree at the pseudo assignment of a returned expression to // declared return type. - res = getAnnotatedType(lhsTree); + res = super.getAnnotatedType(lhsTree); } else { throw new BugInCF( "GenericAnnotatedTypeFactory: Unexpected tree passed to" From 3e0b59dfa4bf35e83d470626a07644fa71e82a63 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Wed, 13 Apr 2022 09:45:38 -0400 Subject: [PATCH 2/9] introduce initialUseFlow --- .../framework/type/GenericAnnotatedTypeFactory.java | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) 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 a25643811e7b..61169951c829 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -207,6 +207,9 @@ public abstract class GenericAnnotatedTypeFactory< */ private boolean useFlow; + /* Record the initial value of useFlow passed in */ + private boolean initialUseFlow; + /** Is this type factory configured to use flow-sensitive type refinement? */ private final boolean everUseFlow; @@ -331,6 +334,7 @@ protected GenericAnnotatedTypeFactory(BaseTypeChecker checker, boolean useFlow) this.everUseFlow = useFlow; this.shouldDefaultTypeVarLocals = useFlow; this.useFlow = useFlow; + this.initialUseFlow = useFlow; this.variablesUnderInitialization = new HashSet<>(); this.scannedClasses = new HashMap<>(); @@ -1629,7 +1633,7 @@ public AnnotatedTypeMirror getAnnotatedTypeLhsNoTypeVarDefault(Tree lhsTree) { @Override public AnnotatedTypeMirror getAnnotatedType(Tree tree) { boolean oldUseFlow = useFlow; - useFlow = true; // what if the useFlow passes in is false? + useFlow = initialUseFlow; AnnotatedTypeMirror res = super.getAnnotatedType(tree); useFlow = oldUseFlow; return res; From 7bb1651788f1e2aa42eb51006928055db76044f3 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Wed, 13 Apr 2022 10:05:58 -0400 Subject: [PATCH 3/9] reformat --- .../framework/type/GenericAnnotatedTypeFactory.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 61169951c829..84258c9c90f8 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -207,7 +207,7 @@ public abstract class GenericAnnotatedTypeFactory< */ private boolean useFlow; - /* Record the initial value of useFlow passed in */ + /** Record the initial value of useFlow passed in. */ private boolean initialUseFlow; /** Is this type factory configured to use flow-sensitive type refinement? */ From ca206c5930bf4e411001ebd7f248949a90b23f6d Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Sun, 17 Apr 2022 17:36:59 -0400 Subject: [PATCH 4/9] delete duplicate variable, add test case --- .../type/GenericAnnotatedTypeFactory.java | 7 ++--- .../test/junit/ViewpointTestCheckerTest.java | 2 +- .../viewpointtest/TestGetAnnotatedLhs.java | 28 +++++++++++++++++++ 3 files changed, 31 insertions(+), 6 deletions(-) create mode 100644 framework/tests/viewpointtest/TestGetAnnotatedLhs.java 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 84258c9c90f8..32e63e749df2 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -207,9 +207,6 @@ public abstract class GenericAnnotatedTypeFactory< */ private boolean useFlow; - /** Record the initial value of useFlow passed in. */ - private boolean initialUseFlow; - /** Is this type factory configured to use flow-sensitive type refinement? */ private final boolean everUseFlow; @@ -334,7 +331,6 @@ protected GenericAnnotatedTypeFactory(BaseTypeChecker checker, boolean useFlow) this.everUseFlow = useFlow; this.shouldDefaultTypeVarLocals = useFlow; this.useFlow = useFlow; - this.initialUseFlow = useFlow; this.variablesUnderInitialization = new HashSet<>(); this.scannedClasses = new HashMap<>(); @@ -1633,7 +1629,7 @@ public AnnotatedTypeMirror getAnnotatedTypeLhsNoTypeVarDefault(Tree lhsTree) { @Override public AnnotatedTypeMirror getAnnotatedType(Tree tree) { boolean oldUseFlow = useFlow; - useFlow = initialUseFlow; + useFlow = everUseFlow; AnnotatedTypeMirror res = super.getAnnotatedType(tree); useFlow = oldUseFlow; return res; @@ -1661,6 +1657,7 @@ public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree) { case IDENTIFIER: case MEMBER_SELECT: case ARRAY_ACCESS: + // For member-select tree, we want the receiver to have the refinement res = super.getAnnotatedType(lhsTree); break; case PARENTHESIZED: diff --git a/framework/src/test/java/org/checkerframework/framework/test/junit/ViewpointTestCheckerTest.java b/framework/src/test/java/org/checkerframework/framework/test/junit/ViewpointTestCheckerTest.java index 2f5fb6662405..0e1678577287 100644 --- a/framework/src/test/java/org/checkerframework/framework/test/junit/ViewpointTestCheckerTest.java +++ b/framework/src/test/java/org/checkerframework/framework/test/junit/ViewpointTestCheckerTest.java @@ -1,4 +1,4 @@ -package tests; +package org.checkerframework.framework.test.junit; import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; import org.junit.runners.Parameterized; diff --git a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java b/framework/tests/viewpointtest/TestGetAnnotatedLhs.java new file mode 100644 index 000000000000..fbad4d25c235 --- /dev/null +++ b/framework/tests/viewpointtest/TestGetAnnotatedLhs.java @@ -0,0 +1,28 @@ +import viewpointtest.quals.A; +import viewpointtest.quals.B; +import viewpointtest.quals.ReceiverDependentQual; +import viewpointtest.quals.Top; + +@ReceiverDependentQual +class TestGetAnnotatedLhs { + @ReceiverDependentQual Object f; + + @SuppressWarnings({ + "inconsistent.constructor.type", + "super.invocation.invalid", + "cast.unsafe.constructor.invocation" + }) + @ReceiverDependentQual + Test() { + this.f = new @ReceiverDependentQual Object(); + } + + @SuppressWarnings({"cast.unsafe.constructor.invocation"}) + void test1() { + Test a = new @A Test(); + Test top = new @Top Test(); + top = a; + // :: error: (assignment.type.incompatible) + top.f = new @B Object(); + } +} From 10a22a4662263bca8ddda3e89b20e9c43de87028 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Sun, 17 Apr 2022 18:17:17 -0400 Subject: [PATCH 5/9] fix TestGetAnnotatedLhs.java test case --- framework/tests/viewpointtest/TestGetAnnotatedLhs.java | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java b/framework/tests/viewpointtest/TestGetAnnotatedLhs.java index fbad4d25c235..bd853a4cf5fe 100644 --- a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java +++ b/framework/tests/viewpointtest/TestGetAnnotatedLhs.java @@ -13,14 +13,14 @@ class TestGetAnnotatedLhs { "cast.unsafe.constructor.invocation" }) @ReceiverDependentQual - Test() { + TestGetAnnotatedLhs() { this.f = new @ReceiverDependentQual Object(); } @SuppressWarnings({"cast.unsafe.constructor.invocation"}) void test1() { - Test a = new @A Test(); - Test top = new @Top Test(); + TestGetAnnotatedLhs a = new @A TestGetAnnotatedLhs(); + TestGetAnnotatedLhs top = new @Top TestGetAnnotatedLhs(); top = a; // :: error: (assignment.type.incompatible) top.f = new @B Object(); From 0d555508a93b81aa7ef4f4b23ea495d4a505e03b Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Mon, 2 May 2022 17:47:50 -0400 Subject: [PATCH 6/9] add tests to viewpointtest checker --- .../framework/type/GenericAnnotatedTypeFactory.java | 9 +++++++++ framework/tests/viewpointtest/TestGetAnnotatedLhs.java | 9 ++++++++- 2 files changed, 17 insertions(+), 1 deletion(-) 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 32e63e749df2..4f07f83ab3d9 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -1626,6 +1626,15 @@ public AnnotatedTypeMirror getAnnotatedTypeLhsNoTypeVarDefault(Tree lhsTree) { return type; } + /** + * The method is overridden for having receiver refinement. Previously, {@code + * getAnnotatedTypeLhs} sets {@code useFlow} to false and calls {@code getAnnotatedType}, + * resulting in no refinement for receiver type. This workaround overrides {@code + * getAnnotatedType} to re-set {@code useFlow} as the initial value passes in. Note that if any + * other checker overrides {@code getAnnotatedType} and calls {@code getAnnotatedTypeLhs}, the + * super version of {@code getAnnotatedType} will be called rather than the one customized by + * the sub checker. + */ @Override public AnnotatedTypeMirror getAnnotatedType(Tree tree) { boolean oldUseFlow = useFlow; diff --git a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java b/framework/tests/viewpointtest/TestGetAnnotatedLhs.java index bd853a4cf5fe..4e9da8cc411f 100644 --- a/framework/tests/viewpointtest/TestGetAnnotatedLhs.java +++ b/framework/tests/viewpointtest/TestGetAnnotatedLhs.java @@ -18,11 +18,18 @@ class TestGetAnnotatedLhs { } @SuppressWarnings({"cast.unsafe.constructor.invocation"}) - void test1() { + void topWithRefinement() { TestGetAnnotatedLhs a = new @A TestGetAnnotatedLhs(); TestGetAnnotatedLhs top = new @Top TestGetAnnotatedLhs(); top = a; // :: error: (assignment.type.incompatible) top.f = new @B Object(); + top.f = new @A Object(); // no error here + } + + @SuppressWarnings({"cast.unsafe.constructor.invocation"}) + void topWithoutRefinement() { + TestGetAnnotatedLhs top = new @Top TestGetAnnotatedLhs(); + top.f = new @A Object(); } } From f1e3f0ee3a901f91052682450562bb54cd152ac9 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Mon, 2 May 2022 17:51:12 -0400 Subject: [PATCH 7/9] add comment in getAnnotatedType --- .../framework/type/GenericAnnotatedTypeFactory.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) 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 4f07f83ab3d9..3e0d49cb4d5e 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -1632,8 +1632,8 @@ public AnnotatedTypeMirror getAnnotatedTypeLhsNoTypeVarDefault(Tree lhsTree) { * resulting in no refinement for receiver type. This workaround overrides {@code * getAnnotatedType} to re-set {@code useFlow} as the initial value passes in. Note that if any * other checker overrides {@code getAnnotatedType} and calls {@code getAnnotatedTypeLhs}, the - * super version of {@code getAnnotatedType} will be called rather than the one customized by - * the sub checker. + * {@code AnnotatedTypeFactory} version of {@code getAnnotatedType} will be called rather than + * the one customized by the sub checker. */ @Override public AnnotatedTypeMirror getAnnotatedType(Tree tree) { From 940bdad67c1881a449671f3f9532d3e461cab296 Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Mon, 2 May 2022 17:54:35 -0400 Subject: [PATCH 8/9] add comment in getAnnotatedType --- .../framework/type/GenericAnnotatedTypeFactory.java | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) 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 3e0d49cb4d5e..7bb583a0b818 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -1630,10 +1630,10 @@ public AnnotatedTypeMirror getAnnotatedTypeLhsNoTypeVarDefault(Tree lhsTree) { * The method is overridden for having receiver refinement. Previously, {@code * getAnnotatedTypeLhs} sets {@code useFlow} to false and calls {@code getAnnotatedType}, * resulting in no refinement for receiver type. This workaround overrides {@code - * getAnnotatedType} to re-set {@code useFlow} as the initial value passes in. Note that if any - * other checker overrides {@code getAnnotatedType} and calls {@code getAnnotatedTypeLhs}, the - * {@code AnnotatedTypeFactory} version of {@code getAnnotatedType} will be called rather than - * the one customized by the sub checker. + * getAnnotatedType} to re-set {@code useFlow} as the initial value passes in. Now if any other + * checker overrides {@code getAnnotatedType} and calls {@code getAnnotatedTypeLhs}, the {@code + * AnnotatedTypeFactory} version of {@code getAnnotatedType} will be called rather than the one + * customized by the sub checker. */ @Override public AnnotatedTypeMirror getAnnotatedType(Tree tree) { From 8070c87c40e8241d2c8514849212bf6d4d1a9c2e Mon Sep 17 00:00:00 2001 From: Haifeng Shi Date: Thu, 7 Jul 2022 19:51:00 -0400 Subject: [PATCH 9/9] remove getAnnotatedType in GenericAnnotatedTypeFactory.java --- .../type/GenericAnnotatedTypeFactory.java | 25 ++----------------- 1 file changed, 2 insertions(+), 23 deletions(-) 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 7bb583a0b818..b1204bdf7be4 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -1626,24 +1626,6 @@ public AnnotatedTypeMirror getAnnotatedTypeLhsNoTypeVarDefault(Tree lhsTree) { return type; } - /** - * The method is overridden for having receiver refinement. Previously, {@code - * getAnnotatedTypeLhs} sets {@code useFlow} to false and calls {@code getAnnotatedType}, - * resulting in no refinement for receiver type. This workaround overrides {@code - * getAnnotatedType} to re-set {@code useFlow} as the initial value passes in. Now if any other - * checker overrides {@code getAnnotatedType} and calls {@code getAnnotatedTypeLhs}, the {@code - * AnnotatedTypeFactory} version of {@code getAnnotatedType} will be called rather than the one - * customized by the sub checker. - */ - @Override - public AnnotatedTypeMirror getAnnotatedType(Tree tree) { - boolean oldUseFlow = useFlow; - useFlow = everUseFlow; - AnnotatedTypeMirror res = super.getAnnotatedType(tree); - useFlow = oldUseFlow; - return res; - } - /** * Returns the type of a left-hand side of an assignment. * @@ -1655,9 +1637,7 @@ public AnnotatedTypeMirror getAnnotatedType(Tree tree) { */ public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree) { AnnotatedTypeMirror res; - boolean oldUseFlow = useFlow; boolean oldShouldCache = shouldCache; - useFlow = false; // Don't cache the result because getAnnotatedType(lhsTree) could // be called from elsewhere and would expect flow-sensitive type refinements. shouldCache = false; @@ -1667,7 +1647,7 @@ public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree) { case MEMBER_SELECT: case ARRAY_ACCESS: // For member-select tree, we want the receiver to have the refinement - res = super.getAnnotatedType(lhsTree); + res = getAnnotatedType(lhsTree); break; case PARENTHESIZED: res = getAnnotatedTypeLhs(TreeUtils.withoutParens((ExpressionTree) lhsTree)); @@ -1676,7 +1656,7 @@ public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree) { if (TreeUtils.isTypeTree(lhsTree)) { // lhsTree is a type tree at the pseudo assignment of a returned expression to // declared return type. - res = super.getAnnotatedType(lhsTree); + res = getAnnotatedType(lhsTree); } else { throw new BugInCF( "GenericAnnotatedTypeFactory: Unexpected tree passed to" @@ -1686,7 +1666,6 @@ public AnnotatedTypeMirror getAnnotatedTypeLhs(Tree lhsTree) { + lhsTree.getKind()); } } - useFlow = oldUseFlow; shouldCache = oldShouldCache; return res; }