From ebb561b532ccc06f12d6c2b81644d70d15c2a38f Mon Sep 17 00:00:00 2001 From: Erfan Arvan Date: Wed, 5 Jun 2024 11:37:25 -0400 Subject: [PATCH 01/33] Handle WPI loop on Unknowninitialization annotations --- .../WholeProgramInferenceImplementation.java | 22 +++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java index e19422d3bfff..44c088a96884 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java @@ -18,6 +18,8 @@ import javax.lang.model.util.ElementFilter; import org.checkerframework.afu.scenelib.util.JVMNames; import org.checkerframework.checker.index.qual.Positive; +import org.checkerframework.checker.initialization.qual.UnknownInitialization; +import org.checkerframework.checker.nullness.qual.MonotonicNonNull; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.dataflow.analysis.Analysis; @@ -1001,6 +1003,26 @@ protected void updateAnnotationSet( return; } + // For parameters, If rhsmATM is Nullable or MonotonicNonNull and has the + // UnknownInitialization annotation, and if the annotation is not + // UnknownInitialization(java.lang.Object.class), replace it with + // UnknownInitialization(java.lang.Object.class). This is because there is + // likely a constructor where it hasn't been initialized, and we haven't + // considered its effect. Otherwise, WPI might get stuck in a loop. + if(defLoc == TypeUseLocation.PARAMETER && (rhsATM.hasPrimaryAnnotation(Nullable.class) || rhsATM + .hasPrimaryAnnotation(MonotonicNonNull.class))){ + for (AnnotationMirror anno : rhsATM.getPrimaryAnnotations()) { + if (anno.getAnnotationType().asElement().getSimpleName().contentEquals( + "UnknownInitialization") && !anno.getAnnotationType().toString().equals("@org" + + ".checkerframework.checker.initialization.qual.UnknownInitialization(java.lang.Object.class)")) { + AnnotationMirror unanno = + AnnotationBuilder.fromClass(atypeFactory.getElementUtils(), + UnknownInitialization.class); + rhsATM.replaceAnnotation(unanno); + } + } + } + AnnotatedTypeMirror atmFromStorage = storage.atmFromStorageLocation(rhsATM.getUnderlyingType(), annotationsToUpdate); updateAtmWithLub(rhsATM, atmFromStorage); From 30d842f471ad1189c4308cc6ff986ffcd211e5c1 Mon Sep 17 00:00:00 2001 From: Erfan Arvan Date: Tue, 18 Jun 2024 22:55:18 -0400 Subject: [PATCH 02/33] Resolved merge conflicts --- .../WholeProgramInferenceImplementation.java | 21 ++++++++++++------- 1 file changed, 14 insertions(+), 7 deletions(-) diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java index 44c088a96884..733861694310 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java @@ -1009,15 +1009,22 @@ protected void updateAnnotationSet( // UnknownInitialization(java.lang.Object.class). This is because there is // likely a constructor where it hasn't been initialized, and we haven't // considered its effect. Otherwise, WPI might get stuck in a loop. - if(defLoc == TypeUseLocation.PARAMETER && (rhsATM.hasPrimaryAnnotation(Nullable.class) || rhsATM - .hasPrimaryAnnotation(MonotonicNonNull.class))){ + if (defLoc == TypeUseLocation.PARAMETER + && (rhsATM.hasPrimaryAnnotation(Nullable.class) + || rhsATM.hasPrimaryAnnotation(MonotonicNonNull.class))) { for (AnnotationMirror anno : rhsATM.getPrimaryAnnotations()) { - if (anno.getAnnotationType().asElement().getSimpleName().contentEquals( - "UnknownInitialization") && !anno.getAnnotationType().toString().equals("@org" + - ".checkerframework.checker.initialization.qual.UnknownInitialization(java.lang.Object.class)")) { + if (anno.getAnnotationType() + .asElement() + .getSimpleName() + .contentEquals("UnknownInitialization") + && !anno.getAnnotationType() + .toString() + .equals( + "@org" + + ".checkerframework.checker.initialization.qual.UnknownInitialization(java.lang.Object.class)")) { AnnotationMirror unanno = - AnnotationBuilder.fromClass(atypeFactory.getElementUtils(), - UnknownInitialization.class); + AnnotationBuilder.fromClass( + atypeFactory.getElementUtils(), UnknownInitialization.class); rhsATM.replaceAnnotation(unanno); } } From 05ef6fbb183c984c1a2394adead9c5fa74a5b59d Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Tue, 4 Jun 2024 20:53:17 -0700 Subject: [PATCH 03/33] Rename FlowExpression to JavaExpression in tests --- ...ionsTest.java => JavaExpressionsTest.java} | 4 +-- ...Bug.java => JavaExpressionParsingBug.java} | 10 +++---- ...st.java => JavaExpressionCheckerTest.java} | 10 +++---- .../flowexpression/FlowExpressionChecker.java | 5 ---- .../JavaExpressionAnnotatedTypeFactory.java} | 26 +++++++++---------- .../javaexpression/JavaExpressionChecker.java | 5 ++++ .../qual/FEBottom.java | 2 +- .../qual/FETop.java | 2 +- .../qual/FlowExp.java | 2 +- .../Class1.java | 0 .../Class2.java | 0 .../Issue862.java | 0 .../ArrayCreationParsing.java | 4 +-- .../BinaryOperations.java | 4 +-- .../Canonicalization.java | 2 +- .../CharAndDoubleParsing.java | 4 +-- .../ClassLiterals.java | 4 +-- .../Complex.java | 4 +-- .../Constructor.java | 2 +- .../Fields.java | 6 ++--- .../InnerClasses.java | 4 +-- .../Issue1609.java | 2 +- .../LambdaParameter.java | 2 +- .../Private.java | 4 +-- .../SimpleVPA.java | 4 +-- .../Standardize.java | 4 +-- .../TestParsing.java | 2 +- .../ThisStaticContext.java | 2 +- .../ThisSuper.java | 2 +- .../UnaryOperations.java | 4 +-- .../Unparsable.java | 4 +-- .../UnsupportJavaCode.java | 4 +-- .../UsePrivate.java | 4 +-- .../ValueLiterals.java | 2 +- .../ViewPointAdaptMethods.java | 4 +-- .../ViewpointAdaptation.java | 2 +- .../ViewpointAdaptation2.java | 2 +- 37 files changed, 74 insertions(+), 74 deletions(-) rename checker/tests/lock/{FlowExpressionsTest.java => JavaExpressionsTest.java} (93%) rename checker/tests/nullness/{FlowExpressionParsingBug.java => JavaExpressionParsingBug.java} (87%) rename framework/src/test/java/org/checkerframework/framework/test/junit/{FlowExpressionCheckerTest.java => JavaExpressionCheckerTest.java} (54%) delete mode 100644 framework/src/test/java/org/checkerframework/framework/testchecker/flowexpression/FlowExpressionChecker.java rename framework/src/test/java/org/checkerframework/framework/testchecker/{flowexpression/FlowExpressionAnnotatedTypeFactory.java => javaexpression/JavaExpressionAnnotatedTypeFactory.java} (83%) create mode 100644 framework/src/test/java/org/checkerframework/framework/testchecker/javaexpression/JavaExpressionChecker.java rename framework/src/test/java/org/checkerframework/framework/testchecker/{flowexpression => javaexpression}/qual/FEBottom.java (80%) rename framework/src/test/java/org/checkerframework/framework/testchecker/{flowexpression => javaexpression}/qual/FETop.java (84%) rename framework/src/test/java/org/checkerframework/framework/testchecker/{flowexpression => javaexpression}/qual/FlowExp.java (85%) rename framework/tests/flow/{flowexpression-scope => javaexpression-scope}/Class1.java (100%) rename framework/tests/flow/{flowexpression-scope => javaexpression-scope}/Class2.java (100%) rename framework/tests/flow/{flowexpression-scope => javaexpression-scope}/Issue862.java (100%) rename framework/tests/{flowexpression => javaexpression}/ArrayCreationParsing.java (87%) rename framework/tests/{flowexpression => javaexpression}/BinaryOperations.java (62%) rename framework/tests/{flowexpression => javaexpression}/Canonicalization.java (94%) rename framework/tests/{flowexpression => javaexpression}/CharAndDoubleParsing.java (75%) rename framework/tests/{flowexpression => javaexpression}/ClassLiterals.java (90%) rename framework/tests/{flowexpression => javaexpression}/Complex.java (91%) rename framework/tests/{flowexpression => javaexpression}/Constructor.java (91%) rename framework/tests/{flowexpression => javaexpression}/Fields.java (72%) rename framework/tests/{flowexpression => javaexpression}/InnerClasses.java (91%) rename framework/tests/{flowexpression => javaexpression}/Issue1609.java (99%) rename framework/tests/{flowexpression => javaexpression}/LambdaParameter.java (96%) rename framework/tests/{flowexpression => javaexpression}/Private.java (77%) rename framework/tests/{flowexpression => javaexpression}/SimpleVPA.java (78%) rename framework/tests/{flowexpression => javaexpression}/Standardize.java (97%) rename framework/tests/{flowexpression => javaexpression}/TestParsing.java (83%) rename framework/tests/{flowexpression => javaexpression}/ThisStaticContext.java (94%) rename framework/tests/{flowexpression => javaexpression}/ThisSuper.java (94%) rename framework/tests/{flowexpression => javaexpression}/UnaryOperations.java (67%) rename framework/tests/{flowexpression => javaexpression}/Unparsable.java (78%) rename framework/tests/{flowexpression => javaexpression}/UnsupportJavaCode.java (73%) rename framework/tests/{flowexpression => javaexpression}/UsePrivate.java (78%) rename framework/tests/{flowexpression => javaexpression}/ValueLiterals.java (83%) rename framework/tests/{flowexpression => javaexpression}/ViewPointAdaptMethods.java (91%) rename framework/tests/{flowexpression => javaexpression}/ViewpointAdaptation.java (93%) rename framework/tests/{flowexpression => javaexpression}/ViewpointAdaptation2.java (94%) diff --git a/checker/tests/lock/FlowExpressionsTest.java b/checker/tests/lock/JavaExpressionsTest.java similarity index 93% rename from checker/tests/lock/FlowExpressionsTest.java rename to checker/tests/lock/JavaExpressionsTest.java index 6c1c164f00ee..b0720d331e59 100644 --- a/checker/tests/lock/FlowExpressionsTest.java +++ b/checker/tests/lock/JavaExpressionsTest.java @@ -1,14 +1,14 @@ import org.checkerframework.checker.lock.qual.*; import org.checkerframework.dataflow.qual.Pure; -public class FlowExpressionsTest { +public class JavaExpressionsTest { class MyClass { public Object field; } private final @GuardedBy({""}) MyClass m; - FlowExpressionsTest() { + JavaExpressionsTest() { m = new MyClass(); } diff --git a/checker/tests/nullness/FlowExpressionParsingBug.java b/checker/tests/nullness/JavaExpressionParsingBug.java similarity index 87% rename from checker/tests/nullness/FlowExpressionParsingBug.java rename to checker/tests/nullness/JavaExpressionParsingBug.java index a4a42a970698..cd94b1e04a1a 100644 --- a/checker/tests/nullness/FlowExpressionParsingBug.java +++ b/checker/tests/nullness/JavaExpressionParsingBug.java @@ -2,7 +2,7 @@ import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.checker.nullness.qual.RequiresNonNull; -public abstract class FlowExpressionParsingBug { +public abstract class JavaExpressionParsingBug { //// Check that JavaExpressions with explicit and implicit 'this' work @@ -18,7 +18,7 @@ public void addFavorite1() {} static @Nullable String i = null; - @RequiresNonNull("FlowExpressionParsingBug.i") + @RequiresNonNull("JavaExpressionParsingBug.i") public void a() {} @RequiresNonNull("i") @@ -30,7 +30,7 @@ public void c() {} void test1() { // :: error: (contracts.precondition) a(); - FlowExpressionParsingBug.i = ""; + JavaExpressionParsingBug.i = ""; a(); } @@ -51,7 +51,7 @@ void test1c() { void test2() { // :: error: (contracts.precondition) b(); - FlowExpressionParsingBug.i = ""; + JavaExpressionParsingBug.i = ""; b(); } @@ -72,7 +72,7 @@ void test2c() { void test3() { // :: error: (contracts.precondition) c(); - FlowExpressionParsingBug.i = ""; + JavaExpressionParsingBug.i = ""; c(); } diff --git a/framework/src/test/java/org/checkerframework/framework/test/junit/FlowExpressionCheckerTest.java b/framework/src/test/java/org/checkerframework/framework/test/junit/JavaExpressionCheckerTest.java similarity index 54% rename from framework/src/test/java/org/checkerframework/framework/test/junit/FlowExpressionCheckerTest.java rename to framework/src/test/java/org/checkerframework/framework/test/junit/JavaExpressionCheckerTest.java index df6cf4e04086..4cc1338ad57f 100644 --- a/framework/src/test/java/org/checkerframework/framework/test/junit/FlowExpressionCheckerTest.java +++ b/framework/src/test/java/org/checkerframework/framework/test/junit/JavaExpressionCheckerTest.java @@ -3,20 +3,20 @@ import java.io.File; import java.util.List; import org.checkerframework.framework.test.CheckerFrameworkPerDirectoryTest; -import org.checkerframework.framework.testchecker.flowexpression.FlowExpressionChecker; +import org.checkerframework.framework.testchecker.javaexpression.JavaExpressionChecker; import org.junit.runners.Parameterized.Parameters; -public class FlowExpressionCheckerTest extends CheckerFrameworkPerDirectoryTest { +public class JavaExpressionCheckerTest extends CheckerFrameworkPerDirectoryTest { /** * @param testFiles the files containing test code, which will be type-checked */ - public FlowExpressionCheckerTest(List testFiles) { - super(testFiles, FlowExpressionChecker.class, "flowexpression"); + public JavaExpressionCheckerTest(List testFiles) { + super(testFiles, JavaExpressionChecker.class, "javaexpression"); } @Parameters public static String[] getTestDirs() { - return new String[] {"flowexpression", "all-systems"}; + return new String[] {"javaexpression", "all-systems"}; } } diff --git a/framework/src/test/java/org/checkerframework/framework/testchecker/flowexpression/FlowExpressionChecker.java b/framework/src/test/java/org/checkerframework/framework/testchecker/flowexpression/FlowExpressionChecker.java deleted file mode 100644 index a6e0fe6facbd..000000000000 --- a/framework/src/test/java/org/checkerframework/framework/testchecker/flowexpression/FlowExpressionChecker.java +++ /dev/null @@ -1,5 +0,0 @@ -package org.checkerframework.framework.testchecker.flowexpression; - -import org.checkerframework.common.basetype.BaseTypeChecker; - -public class FlowExpressionChecker extends BaseTypeChecker {} diff --git a/framework/src/test/java/org/checkerframework/framework/testchecker/flowexpression/FlowExpressionAnnotatedTypeFactory.java b/framework/src/test/java/org/checkerframework/framework/testchecker/javaexpression/JavaExpressionAnnotatedTypeFactory.java similarity index 83% rename from framework/src/test/java/org/checkerframework/framework/testchecker/flowexpression/FlowExpressionAnnotatedTypeFactory.java rename to framework/src/test/java/org/checkerframework/framework/testchecker/javaexpression/JavaExpressionAnnotatedTypeFactory.java index b653b269e305..f8d934918ee2 100644 --- a/framework/src/test/java/org/checkerframework/framework/testchecker/flowexpression/FlowExpressionAnnotatedTypeFactory.java +++ b/framework/src/test/java/org/checkerframework/framework/testchecker/javaexpression/JavaExpressionAnnotatedTypeFactory.java @@ -1,4 +1,4 @@ -package org.checkerframework.framework.testchecker.flowexpression; +package org.checkerframework.framework.testchecker.javaexpression; import java.lang.annotation.Annotation; import java.util.List; @@ -8,9 +8,9 @@ import javax.lang.model.util.Elements; import org.checkerframework.common.basetype.BaseAnnotatedTypeFactory; import org.checkerframework.common.basetype.BaseTypeChecker; -import org.checkerframework.framework.testchecker.flowexpression.qual.FEBottom; -import org.checkerframework.framework.testchecker.flowexpression.qual.FETop; -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FEBottom; +import org.checkerframework.framework.testchecker.javaexpression.qual.FETop; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; import org.checkerframework.framework.type.MostlyNoElementQualifierHierarchy; import org.checkerframework.framework.util.QualifierKind; import org.checkerframework.framework.util.dependenttypes.DependentTypesHelper; @@ -18,7 +18,7 @@ import org.checkerframework.javacutil.AnnotationUtils; import org.checkerframework.javacutil.TreeUtils; -public class FlowExpressionAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { +public class JavaExpressionAnnotatedTypeFactory extends BaseAnnotatedTypeFactory { private AnnotationMirror TOP, BOTTOM; /** The FlowExp.value field/element. */ @@ -26,11 +26,11 @@ public class FlowExpressionAnnotatedTypeFactory extends BaseAnnotatedTypeFactory TreeUtils.getMethod(FlowExp.class, "value", 0, processingEnv); /** - * Creates a new FlowExpressionAnnotatedTypeFactory. + * Creates a new JavaExpressionAnnotatedTypeFactory. * * @param checker the checker */ - public FlowExpressionAnnotatedTypeFactory(BaseTypeChecker checker) { + public JavaExpressionAnnotatedTypeFactory(BaseTypeChecker checker) { super(checker); TOP = AnnotationBuilder.fromClass(elements, FETop.class); BOTTOM = AnnotationBuilder.fromClass(elements, FEBottom.class); @@ -43,21 +43,21 @@ protected DependentTypesHelper createDependentTypesHelper() { } @Override - protected FlowExpressionQualifierHierarchy createQualifierHierarchy() { - return new FlowExpressionQualifierHierarchy(this.getSupportedTypeQualifiers(), elements); + protected JavaExpressionQualifierHierarchy createQualifierHierarchy() { + return new JavaExpressionQualifierHierarchy(this.getSupportedTypeQualifiers(), elements); } - private class FlowExpressionQualifierHierarchy extends MostlyNoElementQualifierHierarchy { + private class JavaExpressionQualifierHierarchy extends MostlyNoElementQualifierHierarchy { /** - * Create a {@code FlowExpressionQualifierHierarchy}. + * Create a {@code JavaExpressionQualifierHierarchy}. * * @param qualifierClasses classes of annotations that are the qualifiers * @param elements element utils */ - public FlowExpressionQualifierHierarchy( + public JavaExpressionQualifierHierarchy( Set> qualifierClasses, Elements elements) { - super(qualifierClasses, elements, FlowExpressionAnnotatedTypeFactory.this); + super(qualifierClasses, elements, JavaExpressionAnnotatedTypeFactory.this); } @Override diff --git a/framework/src/test/java/org/checkerframework/framework/testchecker/javaexpression/JavaExpressionChecker.java b/framework/src/test/java/org/checkerframework/framework/testchecker/javaexpression/JavaExpressionChecker.java new file mode 100644 index 000000000000..59b51457f357 --- /dev/null +++ b/framework/src/test/java/org/checkerframework/framework/testchecker/javaexpression/JavaExpressionChecker.java @@ -0,0 +1,5 @@ +package org.checkerframework.framework.testchecker.javaexpression; + +import org.checkerframework.common.basetype.BaseTypeChecker; + +public class JavaExpressionChecker extends BaseTypeChecker {} diff --git a/framework/src/test/java/org/checkerframework/framework/testchecker/flowexpression/qual/FEBottom.java b/framework/src/test/java/org/checkerframework/framework/testchecker/javaexpression/qual/FEBottom.java similarity index 80% rename from framework/src/test/java/org/checkerframework/framework/testchecker/flowexpression/qual/FEBottom.java rename to framework/src/test/java/org/checkerframework/framework/testchecker/javaexpression/qual/FEBottom.java index ddad660ef933..81677188a2be 100644 --- a/framework/src/test/java/org/checkerframework/framework/testchecker/flowexpression/qual/FEBottom.java +++ b/framework/src/test/java/org/checkerframework/framework/testchecker/javaexpression/qual/FEBottom.java @@ -1,4 +1,4 @@ -package org.checkerframework.framework.testchecker.flowexpression.qual; +package org.checkerframework.framework.testchecker.javaexpression.qual; import java.lang.annotation.ElementType; import java.lang.annotation.Target; diff --git a/framework/src/test/java/org/checkerframework/framework/testchecker/flowexpression/qual/FETop.java b/framework/src/test/java/org/checkerframework/framework/testchecker/javaexpression/qual/FETop.java similarity index 84% rename from framework/src/test/java/org/checkerframework/framework/testchecker/flowexpression/qual/FETop.java rename to framework/src/test/java/org/checkerframework/framework/testchecker/javaexpression/qual/FETop.java index f272e014b5a4..e056fe519974 100644 --- a/framework/src/test/java/org/checkerframework/framework/testchecker/flowexpression/qual/FETop.java +++ b/framework/src/test/java/org/checkerframework/framework/testchecker/javaexpression/qual/FETop.java @@ -1,4 +1,4 @@ -package org.checkerframework.framework.testchecker.flowexpression.qual; +package org.checkerframework.framework.testchecker.javaexpression.qual; import java.lang.annotation.ElementType; import java.lang.annotation.Target; diff --git a/framework/src/test/java/org/checkerframework/framework/testchecker/flowexpression/qual/FlowExp.java b/framework/src/test/java/org/checkerframework/framework/testchecker/javaexpression/qual/FlowExp.java similarity index 85% rename from framework/src/test/java/org/checkerframework/framework/testchecker/flowexpression/qual/FlowExp.java rename to framework/src/test/java/org/checkerframework/framework/testchecker/javaexpression/qual/FlowExp.java index cd2a452dc89a..ddf7a6f2820f 100644 --- a/framework/src/test/java/org/checkerframework/framework/testchecker/flowexpression/qual/FlowExp.java +++ b/framework/src/test/java/org/checkerframework/framework/testchecker/javaexpression/qual/FlowExp.java @@ -1,4 +1,4 @@ -package org.checkerframework.framework.testchecker.flowexpression.qual; +package org.checkerframework.framework.testchecker.javaexpression.qual; import java.lang.annotation.ElementType; import java.lang.annotation.Target; diff --git a/framework/tests/flow/flowexpression-scope/Class1.java b/framework/tests/flow/javaexpression-scope/Class1.java similarity index 100% rename from framework/tests/flow/flowexpression-scope/Class1.java rename to framework/tests/flow/javaexpression-scope/Class1.java diff --git a/framework/tests/flow/flowexpression-scope/Class2.java b/framework/tests/flow/javaexpression-scope/Class2.java similarity index 100% rename from framework/tests/flow/flowexpression-scope/Class2.java rename to framework/tests/flow/javaexpression-scope/Class2.java diff --git a/framework/tests/flow/flowexpression-scope/Issue862.java b/framework/tests/flow/javaexpression-scope/Issue862.java similarity index 100% rename from framework/tests/flow/flowexpression-scope/Issue862.java rename to framework/tests/flow/javaexpression-scope/Issue862.java diff --git a/framework/tests/flowexpression/ArrayCreationParsing.java b/framework/tests/javaexpression/ArrayCreationParsing.java similarity index 87% rename from framework/tests/flowexpression/ArrayCreationParsing.java rename to framework/tests/javaexpression/ArrayCreationParsing.java index 771051eedf34..c4bed6c4da25 100644 --- a/framework/tests/flowexpression/ArrayCreationParsing.java +++ b/framework/tests/javaexpression/ArrayCreationParsing.java @@ -1,6 +1,6 @@ -package flowexpression; +package javaexpression; -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class ArrayCreationParsing { @FlowExp("new int[2]") Object value1; diff --git a/framework/tests/flowexpression/BinaryOperations.java b/framework/tests/javaexpression/BinaryOperations.java similarity index 62% rename from framework/tests/flowexpression/BinaryOperations.java rename to framework/tests/javaexpression/BinaryOperations.java index 8b36de6977a7..4627141f893a 100644 --- a/framework/tests/flowexpression/BinaryOperations.java +++ b/framework/tests/javaexpression/BinaryOperations.java @@ -1,6 +1,6 @@ -package flowexpression; +package javaexpression; -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class BinaryOperations { diff --git a/framework/tests/flowexpression/Canonicalization.java b/framework/tests/javaexpression/Canonicalization.java similarity index 94% rename from framework/tests/flowexpression/Canonicalization.java rename to framework/tests/javaexpression/Canonicalization.java index 5bf7c8c28e6d..6fc58ddae3c1 100644 --- a/framework/tests/flowexpression/Canonicalization.java +++ b/framework/tests/javaexpression/Canonicalization.java @@ -1,4 +1,4 @@ -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class Canonicalization { diff --git a/framework/tests/flowexpression/CharAndDoubleParsing.java b/framework/tests/javaexpression/CharAndDoubleParsing.java similarity index 75% rename from framework/tests/flowexpression/CharAndDoubleParsing.java rename to framework/tests/javaexpression/CharAndDoubleParsing.java index 01341ba1fafd..7402463711d0 100644 --- a/framework/tests/flowexpression/CharAndDoubleParsing.java +++ b/framework/tests/javaexpression/CharAndDoubleParsing.java @@ -1,6 +1,6 @@ -package flowexpression; +package javaexpression; -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class CharAndDoubleParsing { void doubleParsing(@FlowExp("1.0") Object doubleValue) { diff --git a/framework/tests/flowexpression/ClassLiterals.java b/framework/tests/javaexpression/ClassLiterals.java similarity index 90% rename from framework/tests/flowexpression/ClassLiterals.java rename to framework/tests/javaexpression/ClassLiterals.java index 4b62eea36daa..77eda48b4329 100644 --- a/framework/tests/flowexpression/ClassLiterals.java +++ b/framework/tests/javaexpression/ClassLiterals.java @@ -1,6 +1,6 @@ -package flowexpression; +package javaexpression; -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class ClassLiterals { static class String {} diff --git a/framework/tests/flowexpression/Complex.java b/framework/tests/javaexpression/Complex.java similarity index 91% rename from framework/tests/flowexpression/Complex.java rename to framework/tests/javaexpression/Complex.java index 576bd0d617eb..772cc64755f0 100644 --- a/framework/tests/flowexpression/Complex.java +++ b/framework/tests/javaexpression/Complex.java @@ -1,10 +1,10 @@ -package flowexpression; +package javaexpression; import java.util.Collection; import java.util.HashMap; import java.util.List; import java.util.Map; -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class Complex { class DocCategory { diff --git a/framework/tests/flowexpression/Constructor.java b/framework/tests/javaexpression/Constructor.java similarity index 91% rename from framework/tests/flowexpression/Constructor.java rename to framework/tests/javaexpression/Constructor.java index 02d62294333c..7072781e80a2 100644 --- a/framework/tests/flowexpression/Constructor.java +++ b/framework/tests/javaexpression/Constructor.java @@ -1,4 +1,4 @@ -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class Constructor { diff --git a/framework/tests/flowexpression/Fields.java b/framework/tests/javaexpression/Fields.java similarity index 72% rename from framework/tests/flowexpression/Fields.java rename to framework/tests/javaexpression/Fields.java index 5bd68888d335..6ac621ca8473 100644 --- a/framework/tests/flowexpression/Fields.java +++ b/framework/tests/javaexpression/Fields.java @@ -1,6 +1,6 @@ -package flowexpression; +package javaexpression; -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class Fields { static class String { @@ -13,6 +13,6 @@ void method( // :: error: (assignment) @FlowExp("String.HELLO") Object l1 = p1; @FlowExp("String.HELLO") Object l2 = p2; - @FlowExp("flowexpression.Fields.String.HELLO") Object l3 = p2; + @FlowExp("javaexpression.Fields.String.HELLO") Object l3 = p2; } } diff --git a/framework/tests/flowexpression/InnerClasses.java b/framework/tests/javaexpression/InnerClasses.java similarity index 91% rename from framework/tests/flowexpression/InnerClasses.java rename to framework/tests/javaexpression/InnerClasses.java index 99a3ca913c50..40b08a596e57 100644 --- a/framework/tests/flowexpression/InnerClasses.java +++ b/framework/tests/javaexpression/InnerClasses.java @@ -1,6 +1,6 @@ -package flowexpression; +package javaexpression; -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class InnerClasses { public String outerInstanceField = ""; diff --git a/framework/tests/flowexpression/Issue1609.java b/framework/tests/javaexpression/Issue1609.java similarity index 99% rename from framework/tests/flowexpression/Issue1609.java rename to framework/tests/javaexpression/Issue1609.java index be71f4647b5c..f3979c2c7773 100644 --- a/framework/tests/flowexpression/Issue1609.java +++ b/framework/tests/javaexpression/Issue1609.java @@ -1,7 +1,7 @@ // Test case for Issue 1609 // https://github.com/typetools/checker-framework/issues/1609 -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class Issue1609 { void method(@FlowExp("\"" + s + "\"") String x) {} diff --git a/framework/tests/flowexpression/LambdaParameter.java b/framework/tests/javaexpression/LambdaParameter.java similarity index 96% rename from framework/tests/flowexpression/LambdaParameter.java rename to framework/tests/javaexpression/LambdaParameter.java index f26fc90ff79b..375bcaaef414 100644 --- a/framework/tests/flowexpression/LambdaParameter.java +++ b/framework/tests/javaexpression/LambdaParameter.java @@ -1,5 +1,5 @@ import java.util.function.Function; -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class LambdaParameter { diff --git a/framework/tests/flowexpression/Private.java b/framework/tests/javaexpression/Private.java similarity index 77% rename from framework/tests/flowexpression/Private.java rename to framework/tests/javaexpression/Private.java index 95c714b62a77..76030264dccc 100644 --- a/framework/tests/flowexpression/Private.java +++ b/framework/tests/javaexpression/Private.java @@ -1,9 +1,9 @@ -package flowexpression; +package javaexpression; import java.util.Collection; import java.util.LinkedHashMap; import java.util.Map; -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class Private { private final Map nameToPpt = new LinkedHashMap<>(); diff --git a/framework/tests/flowexpression/SimpleVPA.java b/framework/tests/javaexpression/SimpleVPA.java similarity index 78% rename from framework/tests/flowexpression/SimpleVPA.java rename to framework/tests/javaexpression/SimpleVPA.java index 97d3cf3ac2f5..d76ca491ead4 100644 --- a/framework/tests/flowexpression/SimpleVPA.java +++ b/framework/tests/javaexpression/SimpleVPA.java @@ -1,6 +1,6 @@ -package flowexpression; +package javaexpression; -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class SimpleVPA { diff --git a/framework/tests/flowexpression/Standardize.java b/framework/tests/javaexpression/Standardize.java similarity index 97% rename from framework/tests/flowexpression/Standardize.java rename to framework/tests/javaexpression/Standardize.java index 93ad51c50304..bd5fcb0facaf 100644 --- a/framework/tests/flowexpression/Standardize.java +++ b/framework/tests/javaexpression/Standardize.java @@ -1,10 +1,10 @@ -package flowexpression; +package javaexpression; import java.io.FileInputStream; import java.util.HashMap; import java.util.List; import java.util.Map; -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class Standardize { Object field; diff --git a/framework/tests/flowexpression/TestParsing.java b/framework/tests/javaexpression/TestParsing.java similarity index 83% rename from framework/tests/flowexpression/TestParsing.java rename to framework/tests/javaexpression/TestParsing.java index f2d84e77755b..7989f0fee0d7 100644 --- a/framework/tests/flowexpression/TestParsing.java +++ b/framework/tests/javaexpression/TestParsing.java @@ -1,4 +1,4 @@ -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class TestParsing { int[] a = {1, 2}; diff --git a/framework/tests/flowexpression/ThisStaticContext.java b/framework/tests/javaexpression/ThisStaticContext.java similarity index 94% rename from framework/tests/flowexpression/ThisStaticContext.java rename to framework/tests/javaexpression/ThisStaticContext.java index c4201d986521..1e8323b13c02 100644 --- a/framework/tests/flowexpression/ThisStaticContext.java +++ b/framework/tests/javaexpression/ThisStaticContext.java @@ -1,5 +1,5 @@ import java.util.Map; -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class ThisStaticContext { public static Map staticField; diff --git a/framework/tests/flowexpression/ThisSuper.java b/framework/tests/javaexpression/ThisSuper.java similarity index 94% rename from framework/tests/flowexpression/ThisSuper.java rename to framework/tests/javaexpression/ThisSuper.java index 667e2613d471..83ca94940edf 100644 --- a/framework/tests/flowexpression/ThisSuper.java +++ b/framework/tests/javaexpression/ThisSuper.java @@ -1,6 +1,6 @@ // Test case for // https://github.com/typetools/checker-framework/issues/152 -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; // @skip-test public class ThisSuper { diff --git a/framework/tests/flowexpression/UnaryOperations.java b/framework/tests/javaexpression/UnaryOperations.java similarity index 67% rename from framework/tests/flowexpression/UnaryOperations.java rename to framework/tests/javaexpression/UnaryOperations.java index 9c36ecd52d42..97e4537b8468 100644 --- a/framework/tests/flowexpression/UnaryOperations.java +++ b/framework/tests/javaexpression/UnaryOperations.java @@ -1,6 +1,6 @@ -package flowexpression; +package javaexpression; -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class UnaryOperations { diff --git a/framework/tests/flowexpression/Unparsable.java b/framework/tests/javaexpression/Unparsable.java similarity index 78% rename from framework/tests/flowexpression/Unparsable.java rename to framework/tests/javaexpression/Unparsable.java index cad8849572c3..12d7af5b6500 100644 --- a/framework/tests/flowexpression/Unparsable.java +++ b/framework/tests/javaexpression/Unparsable.java @@ -1,6 +1,6 @@ -package flowexpression; +package javaexpression; -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class Unparsable { // :: error: (expression.unparsable) diff --git a/framework/tests/flowexpression/UnsupportJavaCode.java b/framework/tests/javaexpression/UnsupportJavaCode.java similarity index 73% rename from framework/tests/flowexpression/UnsupportJavaCode.java rename to framework/tests/javaexpression/UnsupportJavaCode.java index 0bb1712a29ad..1fd5d7f54a34 100644 --- a/framework/tests/flowexpression/UnsupportJavaCode.java +++ b/framework/tests/javaexpression/UnsupportJavaCode.java @@ -1,6 +1,6 @@ -package flowexpression; +package javaexpression; -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class UnsupportJavaCode { diff --git a/framework/tests/flowexpression/UsePrivate.java b/framework/tests/javaexpression/UsePrivate.java similarity index 78% rename from framework/tests/flowexpression/UsePrivate.java rename to framework/tests/javaexpression/UsePrivate.java index aef6f624be12..acc233a27abf 100644 --- a/framework/tests/flowexpression/UsePrivate.java +++ b/framework/tests/javaexpression/UsePrivate.java @@ -1,7 +1,7 @@ -package flowexpression; +package javaexpression; import java.util.Collection; -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class UsePrivate { void test(Private app_ppts, Private test_ppts) { diff --git a/framework/tests/flowexpression/ValueLiterals.java b/framework/tests/javaexpression/ValueLiterals.java similarity index 83% rename from framework/tests/flowexpression/ValueLiterals.java rename to framework/tests/javaexpression/ValueLiterals.java index 5acc3b0d17f6..198e10273364 100644 --- a/framework/tests/flowexpression/ValueLiterals.java +++ b/framework/tests/javaexpression/ValueLiterals.java @@ -1,4 +1,4 @@ -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class ValueLiterals { void test(@FlowExp("0") Object a, @FlowExp("0L") Object b) {} diff --git a/framework/tests/flowexpression/ViewPointAdaptMethods.java b/framework/tests/javaexpression/ViewPointAdaptMethods.java similarity index 91% rename from framework/tests/flowexpression/ViewPointAdaptMethods.java rename to framework/tests/javaexpression/ViewPointAdaptMethods.java index d9b9c18e2b1e..a6775c081d17 100644 --- a/framework/tests/flowexpression/ViewPointAdaptMethods.java +++ b/framework/tests/javaexpression/ViewPointAdaptMethods.java @@ -1,6 +1,6 @@ -package flowexpression; +package javaexpression; -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class ViewPointAdaptMethods { Object param1; diff --git a/framework/tests/flowexpression/ViewpointAdaptation.java b/framework/tests/javaexpression/ViewpointAdaptation.java similarity index 93% rename from framework/tests/flowexpression/ViewpointAdaptation.java rename to framework/tests/javaexpression/ViewpointAdaptation.java index a047a97c7e56..6a7457573adb 100644 --- a/framework/tests/flowexpression/ViewpointAdaptation.java +++ b/framework/tests/javaexpression/ViewpointAdaptation.java @@ -1,4 +1,4 @@ -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class ViewpointAdaptation { diff --git a/framework/tests/flowexpression/ViewpointAdaptation2.java b/framework/tests/javaexpression/ViewpointAdaptation2.java similarity index 94% rename from framework/tests/flowexpression/ViewpointAdaptation2.java rename to framework/tests/javaexpression/ViewpointAdaptation2.java index 4e56d54a8dfc..744d7e4e7a63 100644 --- a/framework/tests/flowexpression/ViewpointAdaptation2.java +++ b/framework/tests/javaexpression/ViewpointAdaptation2.java @@ -1,4 +1,4 @@ -import org.checkerframework.framework.testchecker.flowexpression.qual.FlowExp; +import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; public class ViewpointAdaptation2 { class LockExample { From ebf782c77141451934070c10d8bc79a921ac0422 Mon Sep 17 00:00:00 2001 From: "renovate[bot]" <29139614+renovate[bot]@users.noreply.github.com> Date: Wed, 5 Jun 2024 06:31:28 -0700 Subject: [PATCH 04/33] Update dependency io.github.classgraph:classgraph to v4.8.173 (#6653) Co-authored-by: renovate[bot] <29139614+renovate[bot]@users.noreply.github.com> --- framework/build.gradle | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/framework/build.gradle b/framework/build.gradle index 25bf2cf251a6..a81592a5003d 100644 --- a/framework/build.gradle +++ b/framework/build.gradle @@ -45,7 +45,7 @@ dependencies { implementation "org.plumelib:hashmap-util:${versions.hashmapUtil}" implementation "org.plumelib:plume-util:${versions.plumeUtil}" implementation "org.plumelib:reflection-util:${versions.reflectionUtil}" - implementation 'io.github.classgraph:classgraph:4.8.172' + implementation 'io.github.classgraph:classgraph:4.8.173' testImplementation group: 'junit', name: 'junit', version: '4.13.2' testImplementation project(':framework-test') From 5167ed1489b69c8f6bb7937083f241d87356af1a Mon Sep 17 00:00:00 2001 From: James Yoo <24359440+jyoo980@users.noreply.github.com> Date: Wed, 5 Jun 2024 09:39:58 -0700 Subject: [PATCH 05/33] Implement `JavaExpression.SuperReference` Co-authored-by: Suzanne Millstein Co-authored-by: Michael Ernst --- checker/tests/optional/Shadowing.java | 34 +++++++++ .../tests/optional/ShadowingMethodCalls.java | 72 ++++++++++++++++++ .../dataflow/expression/FieldAccess.java | 12 ++- .../dataflow/expression/JavaExpression.java | 7 +- .../expression/JavaExpressionConverter.java | 5 ++ .../expression/JavaExpressionScanner.java | 5 ++ .../expression/JavaExpressionVisitor.java | 9 +++ .../dataflow/expression/MethodCall.java | 5 +- .../dataflow/expression/SuperReference.java | 76 +++++++++++++++++++ .../util/JavaExpressionParseUtil.java | 15 +++- .../dependenttypes/DependentTypesHelper.java | 6 ++ framework/tests/flow/FieldShadowing.java | 1 - framework/tests/javaexpression/ThisSuper.java | 14 ---- 13 files changed, 241 insertions(+), 20 deletions(-) create mode 100644 checker/tests/optional/Shadowing.java create mode 100644 checker/tests/optional/ShadowingMethodCalls.java create mode 100644 dataflow/src/main/java/org/checkerframework/dataflow/expression/SuperReference.java diff --git a/checker/tests/optional/Shadowing.java b/checker/tests/optional/Shadowing.java new file mode 100644 index 000000000000..9d40c86b6d63 --- /dev/null +++ b/checker/tests/optional/Shadowing.java @@ -0,0 +1,34 @@ +import java.util.Optional; +import org.checkerframework.checker.optional.qual.*; +import org.checkerframework.dataflow.qual.*; + +@SuppressWarnings({"optional:field", "optional:parameter"}) +public class Shadowing { + + public Optional f; + + public Optional g; + + class Sub extends Shadowing { + Optional f; + + void foo(@Present Optional present) { + super.f = present; + @Present Optional ok = super.f; + } + + void bar(@Present Optional present) { + this.f = present; + @Present Optional ok = this.f; + } + + void baz(@Present Optional present) { + super.g = present; + @Present Optional ok1 = this.g; + @Present Optional ok2 = super.g; + } + + // @RequiresPresent("super.f") + // void bar() {} + } +} diff --git a/checker/tests/optional/ShadowingMethodCalls.java b/checker/tests/optional/ShadowingMethodCalls.java new file mode 100644 index 000000000000..7bd2c58ef45e --- /dev/null +++ b/checker/tests/optional/ShadowingMethodCalls.java @@ -0,0 +1,72 @@ +import java.util.Optional; +import org.checkerframework.checker.optional.qual.EnsuresPresent; +import org.checkerframework.dataflow.qual.Pure; + +@SuppressWarnings({"optional:field", "optional:parameter"}) +public class ShadowingMethodCalls { + + Optional f; + + @EnsuresPresent("this.f") + void setF() { + this.f = Optional.of("Hello from Parent"); + } + + class Child extends ShadowingMethodCalls { + + Optional f; + + @EnsuresPresent("super.f") + void setF() { + super.f = Optional.of("Hello from Child"); + } + + void callThisAndCheckSuper() { + this.setF(); + super.f.get(); + } + + void callSuperAndCheckSuper() { + super.setF(); + super.f.get(); + } + + void callSuperAndCheckThis() { + super.setF(); + // :: error: (method.invocation) + this.f.get(); + } + + void callThisAndCheckThis() { + this.setF(); + // :: error: (method.invocation) + this.f.get(); + super.f.get(); + } + } + + static class ClassA { + + @Pure + Optional getOpt() { + throw new RuntimeException(); + } + } + + static class ClassB extends ClassA { + void use() { + if (super.getOpt().isPresent()) { + String s = super.getOpt().get(); + } + if (super.getOpt().isPresent()) { + String s = this.getOpt().get(); + } + if (this.getOpt().isPresent()) { + String s = super.getOpt().get(); + } + if (this.getOpt().isPresent()) { + String s = this.getOpt().get(); + } + } + } +} diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/expression/FieldAccess.java b/dataflow/src/main/java/org/checkerframework/dataflow/expression/FieldAccess.java index 3e7deff0dddf..92908cfe1515 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/expression/FieldAccess.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/expression/FieldAccess.java @@ -99,7 +99,17 @@ public boolean equals(@Nullable Object obj) { return false; } FieldAccess fa = (FieldAccess) obj; - return fa.getField().equals(getField()) && fa.getReceiver().equals(getReceiver()); + if (!fa.getField().equals(getField())) { + return false; + } + + if (fa.getReceiver().equals(getReceiver())) { + return true; + } + + return (fa.getReceiver() instanceof SuperReference || fa.getReceiver() instanceof ThisReference) + && (this.getReceiver() instanceof SuperReference + || this.getReceiver() instanceof ThisReference); } @Override diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpression.java b/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpression.java index 73f351f52ca0..0924dfbf0d50 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpression.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpression.java @@ -385,7 +385,7 @@ public static JavaExpression fromNode(Node receiverNode) { } else if (receiverNode instanceof ThisNode) { result = new ThisReference(receiverNode.getType()); } else if (receiverNode instanceof SuperNode) { - result = new ThisReference(receiverNode.getType()); + result = new SuperReference(receiverNode.getType()); } else if (receiverNode instanceof LocalVariableNode) { LocalVariableNode lv = (LocalVariableNode) receiverNode; result = new LocalVariable(lv); @@ -533,9 +533,12 @@ public static JavaExpression fromTree(ExpressionTree tree) { IdentifierTree identifierTree = (IdentifierTree) tree; TypeMirror typeOfId = TreeUtils.typeOf(identifierTree); Name identifierName = identifierTree.getName(); - if (identifierName.contentEquals("this") || identifierName.contentEquals("super")) { + if (identifierName.contentEquals("this")) { result = new ThisReference(typeOfId); break; + } else if (identifierName.contentEquals("super")) { + result = new SuperReference(typeOfId); + break; } assert TreeUtils.isUseOfElement(identifierTree) : "@AssumeAssertion(nullness): tree kind"; Element ele = TreeUtils.elementFromUse(identifierTree); diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionConverter.java b/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionConverter.java index 1b811ec44431..78066c112251 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionConverter.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionConverter.java @@ -101,6 +101,11 @@ protected JavaExpression visitThisReference(ThisReference thisExpr, Void unused) return thisExpr; } + @Override + protected JavaExpression visitSuperReference(SuperReference superExpr, Void unused) { + return superExpr; + } + @Override protected JavaExpression visitUnaryOperation(UnaryOperation unaryOpExpr, Void unused) { JavaExpression operand = convert(unaryOpExpr.getOperand()); diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionScanner.java b/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionScanner.java index e282ce5a11dd..79c9eb0f158f 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionScanner.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionScanner.java @@ -88,6 +88,11 @@ protected Void visitThisReference(ThisReference thisExpr, P p) { return null; } + @Override + protected Void visitSuperReference(SuperReference superExpr, P p) { + return null; + } + @Override protected Void visitUnaryOperation(UnaryOperation unaryOpExpr, P p) { visit(unaryOpExpr.getOperand(), p); diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionVisitor.java b/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionVisitor.java index 1511dea1277a..2fa169f8bc87 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionVisitor.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/expression/JavaExpressionVisitor.java @@ -100,6 +100,15 @@ public R visit(JavaExpression javaExpr, P p) { */ protected abstract R visitThisReference(ThisReference thisExpr, P p); + /** + * Visit a {@link SuperReference}. + * + * @param superExpr the JavaExpression to visit + * @param p the parameter to pass to the visit method + * @return the result of visiting the {@code superExpr} + */ + protected abstract R visitSuperReference(SuperReference superExpr, P p); + /** * Visit an {@link UnaryOperation}. * diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/expression/MethodCall.java b/dataflow/src/main/java/org/checkerframework/dataflow/expression/MethodCall.java index 28c92fd91e11..bfdde9cafb7c 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/expression/MethodCall.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/expression/MethodCall.java @@ -155,8 +155,11 @@ public boolean equals(@Nullable Object obj) { return false; } MethodCall other = (MethodCall) obj; + boolean isComparingSuperWithThis = + (receiver instanceof SuperReference && other.receiver instanceof ThisReference) + || (receiver instanceof ThisReference && other.receiver instanceof SuperReference); return method.equals(other.method) - && receiver.equals(other.receiver) + && (receiver.equals(other.receiver) || isComparingSuperWithThis) && arguments.equals(other.arguments); } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/expression/SuperReference.java b/dataflow/src/main/java/org/checkerframework/dataflow/expression/SuperReference.java new file mode 100644 index 000000000000..c71e9afa1981 --- /dev/null +++ b/dataflow/src/main/java/org/checkerframework/dataflow/expression/SuperReference.java @@ -0,0 +1,76 @@ +package org.checkerframework.dataflow.expression; + +import javax.lang.model.type.TypeMirror; +import org.checkerframework.checker.nullness.qual.Nullable; +import org.checkerframework.dataflow.analysis.Store; +import org.checkerframework.javacutil.AnnotationProvider; +import org.checkerframework.javacutil.TypesUtils; + +/** A use of {@code super}. */ +public class SuperReference extends JavaExpression { + + /** + * Creates a new {@link SuperReference}. + * + * @param type the type of the {@code super} reference + */ + public SuperReference(TypeMirror type) { + super(type); + } + + @SuppressWarnings("unchecked") // generic cast + @Override + public @Nullable T containedOfClass(Class clazz) { + return getClass() == clazz ? (T) this : null; + } + + @Override + public boolean isDeterministic(AnnotationProvider provider) { + return true; + } + + @Override + public boolean isAssignableByOtherCode() { + return false; + } + + @Override + public boolean isModifiableByOtherCode() { + return !TypesUtils.isImmutableTypeInJdk(type); + } + + @Override + public boolean containsModifiableAliasOf(Store store, JavaExpression other) { + return false; + } + + @Override + public boolean syntacticEquals(JavaExpression je) { + return je instanceof SuperReference; + } + + @Override + public boolean containsSyntacticEqualJavaExpression(JavaExpression other) { + return this.syntacticEquals(other); + } + + @Override + public boolean equals(@Nullable Object obj) { + return obj instanceof SuperReference; + } + + @Override + public int hashCode() { + return 0; + } + + @Override + public R accept(JavaExpressionVisitor visitor, P p) { + return visitor.visitSuperReference(this, p); + } + + @Override + public String toString() { + return "super"; + } +} diff --git a/framework/src/main/java/org/checkerframework/framework/util/JavaExpressionParseUtil.java b/framework/src/main/java/org/checkerframework/framework/util/JavaExpressionParseUtil.java index a4c367904d4e..2097abd37925 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/JavaExpressionParseUtil.java +++ b/framework/src/main/java/org/checkerframework/framework/util/JavaExpressionParseUtil.java @@ -63,6 +63,7 @@ import org.checkerframework.dataflow.expression.JavaExpression; import org.checkerframework.dataflow.expression.LocalVariable; import org.checkerframework.dataflow.expression.MethodCall; +import org.checkerframework.dataflow.expression.SuperReference; import org.checkerframework.dataflow.expression.ThisReference; import org.checkerframework.dataflow.expression.UnaryOperation; import org.checkerframework.dataflow.expression.ValueLiteral; @@ -366,13 +367,17 @@ public JavaExpression visit(ThisExpr n, Void aVoid) { @Override public JavaExpression visit(SuperExpr n, Void aVoid) { + if (thisReference == null) { + throw new ParseRuntimeException( + constructJavaExpressionParseError("super", "\"super\" isn't allowed here")); + } // super literal TypeMirror superclass = TypesUtils.getSuperclass(enclosingType, types); if (superclass == null) { throw new ParseRuntimeException( constructJavaExpressionParseError("super", enclosingType + " has no superclass")); } - return new ThisReference(superclass); + return new SuperReference(superclass); } // expr is an expression in parentheses. @@ -630,6 +635,14 @@ public JavaExpression visit(NameExpr expr, Void aVoid) { // field not found. return null; } + if (receiverExpr instanceof SuperReference + && thisReference.getType().getKind() == TypeKind.DECLARED) { + Element thisFieldElem = + resolver.findField(identifier, thisReference.getType(), pathToCompilationUnit); + if (thisFieldElem == null) { + receiverExpr = thisReference; + } + } } // `fieldElem` is now set. Construct a FieldAccess expression. diff --git a/framework/src/main/java/org/checkerframework/framework/util/dependenttypes/DependentTypesHelper.java b/framework/src/main/java/org/checkerframework/framework/util/dependenttypes/DependentTypesHelper.java index 1fff50b2a85b..9f20744f19d9 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/dependenttypes/DependentTypesHelper.java +++ b/framework/src/main/java/org/checkerframework/framework/util/dependenttypes/DependentTypesHelper.java @@ -38,6 +38,7 @@ import org.checkerframework.dataflow.expression.JavaExpression; import org.checkerframework.dataflow.expression.JavaExpressionConverter; import org.checkerframework.dataflow.expression.LocalVariable; +import org.checkerframework.dataflow.expression.SuperReference; import org.checkerframework.dataflow.expression.ThisReference; import org.checkerframework.dataflow.expression.Unknown; import org.checkerframework.framework.source.SourceChecker; @@ -730,6 +731,11 @@ public JavaExpression visitLocalVariable(LocalVariable local, Void unused) { public JavaExpression visitThisReference(ThisReference thisRef, Void unused) { throw new FoundLocalVarException(); } + + @Override + public JavaExpression visitSuperReference(SuperReference superRef, Void unused) { + throw new FoundLocalVarException(); + } }; try { diff --git a/framework/tests/flow/FieldShadowing.java b/framework/tests/flow/FieldShadowing.java index cfef3d69afaa..bd3962ad4c52 100644 --- a/framework/tests/flow/FieldShadowing.java +++ b/framework/tests/flow/FieldShadowing.java @@ -1,6 +1,5 @@ import org.checkerframework.dataflow.qual.Pure; import org.checkerframework.framework.qual.RequiresQualifier; -import org.checkerframework.framework.test.*; import org.checkerframework.framework.testchecker.util.*; // various tests for the precondition mechanism diff --git a/framework/tests/javaexpression/ThisSuper.java b/framework/tests/javaexpression/ThisSuper.java index 83ca94940edf..0bc50a42101c 100644 --- a/framework/tests/javaexpression/ThisSuper.java +++ b/framework/tests/javaexpression/ThisSuper.java @@ -2,7 +2,6 @@ // https://github.com/typetools/checker-framework/issues/152 import org.checkerframework.framework.testchecker.javaexpression.qual.FlowExp; -// @skip-test public class ThisSuper { static class SuperClass { protected final Object field = new Object(); @@ -28,17 +27,4 @@ void method() { @FlowExp("this.field") Object o2 = this.subField; } } - - class OuterClass { - private final Object lock = new Object(); - - @FlowExp("this.lock") Object field; - - class InnerClass { - private final Object lock = new Object(); - - // :: error: (assignment) - @FlowExp("this.lock") Object field2 = field; - } - } } From ee517ea86b4a8a8eafc31a6318764bef952151d8 Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Wed, 5 Jun 2024 20:52:01 -0700 Subject: [PATCH 06/33] Added a Tree argument to AnnotatedTypes.adaptParameters() Co-authored-by: Michael Ernst --- .../checker/guieffect/GuiEffectVisitor.java | 2 +- .../lock/LockAnnotatedTypeFactory.java | 2 +- .../checker/lock/LockVisitor.java | 10 +++++- docs/CHANGELOG.md | 2 ++ .../common/basetype/BaseTypeVisitor.java | 4 +-- .../poly/AbstractQualifierPolymorphism.java | 9 +++-- .../framework/util/AnnotatedTypes.java | 36 +++++++++++-------- framework/tests/all-systems/Issue6078.java | 9 ++++- .../checkerframework/javacutil/TreeUtils.java | 22 +++++++++++- 9 files changed, 72 insertions(+), 24 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/guieffect/GuiEffectVisitor.java b/checker/src/main/java/org/checkerframework/checker/guieffect/GuiEffectVisitor.java index abd40c033599..cd962d62f7e2 100644 --- a/checker/src/main/java/org/checkerframework/checker/guieffect/GuiEffectVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/guieffect/GuiEffectVisitor.java @@ -509,7 +509,7 @@ private void scanUp(TreePath path) { List methodParams = method.getParameters(); List paramTypes = AnnotatedTypes.adaptParameters( - atypeFactory, invokedMethod, invocationTree.getArguments()); + atypeFactory, invokedMethod, invocationTree.getArguments(), invocationTree); for (int i = 0; i < args.size(); ++i) { if (args.get(i).getKind() == Tree.Kind.NEW_CLASS || args.get(i).getKind() == Tree.Kind.LAMBDA_EXPRESSION) { diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java index afc29c79c109..06bda188edc9 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockAnnotatedTypeFactory.java @@ -630,7 +630,7 @@ && replaceAnnotationInGuardedByHierarchyIfGuardSatisfiedIndexMatches( List methodInvocationTreeArguments = ((MethodInvocationTree) tree).getArguments(); List paramTypes = - AnnotatedTypes.adaptParameters(this, invokedMethod, methodInvocationTreeArguments); + AnnotatedTypes.adaptParameters(this, invokedMethod, methodInvocationTreeArguments, tree); for (int i = 0; i < paramTypes.size(); i++) { if (replaceAnnotationInGuardedByHierarchyIfGuardSatisfiedIndexMatches( diff --git a/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java b/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java index 24f6832e938c..e8925e96f772 100644 --- a/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/lock/LockVisitor.java @@ -528,6 +528,14 @@ public boolean isValidUse( */ @Override public Void visitMethodInvocation(MethodInvocationTree methodInvocationTree, Void p) { + // Skip calls to the Enum constructor (they're generated by javac and + // hard to check), also see CFGBuilder.visitMethodInvocation. + // (This code is copied from super.) + if (TreeUtils.elementFromUse(methodInvocationTree) == null + || TreeUtils.isEnumSuperCall(methodInvocationTree)) { + return super.visitMethodInvocation(methodInvocationTree, p); + } + ExecutableElement methodElement = TreeUtils.elementFromUse(methodInvocationTree); SideEffectAnnotation seaOfInvokedMethod = @@ -617,7 +625,7 @@ public Void visitMethodInvocation(MethodInvocationTree methodInvocationTree, Voi List paramTypes = AnnotatedTypes.adaptParameters( - atypeFactory, invokedMethod, methodInvocationTree.getArguments()); + atypeFactory, invokedMethod, methodInvocationTree.getArguments(), methodInvocationTree); // Index on @GuardSatisfied at each location. -1 when no @GuardSatisfied annotation was // present. diff --git a/docs/CHANGELOG.md b/docs/CHANGELOG.md index 24077ea29449..1e399cd1a676 100644 --- a/docs/CHANGELOG.md +++ b/docs/CHANGELOG.md @@ -5,6 +5,8 @@ Version 3.45.0 (July 2, 2024) **Implementation details:** +Added a `Tree` argument to `AnnotatedTypes.adaptParameters()` + Deprecated methods: * `TreeUtils.isVarArgs()` => `isVarargsCall()` * `TreeUtils.isVarArgMethodCall()` => `isVarargsCall()` diff --git a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java index b8bf7d257ee9..92aec12fcd35 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -1848,7 +1848,7 @@ public Void visitMethodInvocation(MethodInvocationTree tree, Void p) { methodName, invokedMethod.getTypeVariables()); List params = - AnnotatedTypes.adaptParameters(atypeFactory, invokedMethod, tree.getArguments()); + AnnotatedTypes.adaptParameters(atypeFactory, invokedMethod, tree.getArguments(), tree); checkArguments(params, tree.getArguments(), methodName, method.getParameters()); checkVarargs(invokedMethod, tree); @@ -2171,7 +2171,7 @@ public Void visitNewClass(NewClassTree tree, Void p) { List passedArguments = tree.getArguments(); List params = - AnnotatedTypes.adaptParameters(atypeFactory, constructorType, passedArguments); + AnnotatedTypes.adaptParameters(atypeFactory, constructorType, passedArguments, tree); ExecutableElement constructor = constructorType.getElement(); CharSequence constructorName = ElementUtils.getSimpleDescription(constructor); diff --git a/framework/src/main/java/org/checkerframework/framework/type/poly/AbstractQualifierPolymorphism.java b/framework/src/main/java/org/checkerframework/framework/type/poly/AbstractQualifierPolymorphism.java index 2bda809ef9e7..4bdeabf6db0d 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/poly/AbstractQualifierPolymorphism.java +++ b/framework/src/main/java/org/checkerframework/framework/type/poly/AbstractQualifierPolymorphism.java @@ -50,7 +50,7 @@ *
  • the PolyCollector creates an instantiation *
  • if the instantiation is non-empty: the Replacer does resolution -- that is, it replaces * each occurrence of {@code @Poly*} by the concrete qualifier it maps to in the instantiation - *
  • if the instantiation is empty, the Completer replaces each {@code @Poly*} by the top + *
  • if the instantiation is empty, the Completer replaces each {@code @Poly*} by the bottom * qualifier * */ @@ -82,6 +82,9 @@ public abstract class AbstractQualifierPolymorphism implements QualifierPolymorp /** * Completes a type by removing any unresolved polymorphic qualifiers, replacing them with the * bottom qualifiers. + * + *

    This is only called when {@code instantiationMapping} is empty. (And that implies that there + * are no polymorphic qualifiers on formal parameters??) */ private final SimpleAnnotatedTypeScanner completer; @@ -181,7 +184,7 @@ public void resolve(MethodInvocationTree tree, AnnotatedExecutableType type) { return; } List parameters = - AnnotatedTypes.adaptParameters(atypeFactory, type, tree.getArguments()); + AnnotatedTypes.adaptParameters(atypeFactory, type, tree.getArguments(), tree); List arguments = CollectionsPlume.mapList(atypeFactory::getAnnotatedType, tree.getArguments()); @@ -216,7 +219,7 @@ public void resolve(NewClassTree tree, AnnotatedExecutableType type) { } List parameters = - AnnotatedTypes.adaptParameters(atypeFactory, type, tree.getArguments()); + AnnotatedTypes.adaptParameters(atypeFactory, type, tree.getArguments(), tree); List arguments = CollectionsPlume.mapList(atypeFactory::getAnnotatedType, tree.getArguments()); diff --git a/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java b/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java index 6a97cd42405f..4b20005dbb83 100644 --- a/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java +++ b/framework/src/main/java/org/checkerframework/framework/util/AnnotatedTypes.java @@ -986,15 +986,15 @@ private static AnnotatedTypeMirror glbSubtype( * @param method the method's type * @param args the arguments to the method invocation * @return the types that the method invocation arguments need to be subtype of - * @deprecated Use {@link #adaptParameters(AnnotatedTypeFactory, - * AnnotatedTypeMirror.AnnotatedExecutableType, List)} instead + * @deprecated Use {@link #adaptParameters(AnnotatedTypeFactory, AnnotatedExecutableType, List, + * Tree)} instead */ @Deprecated // 2022-04-21 public static List expandVarArgsParameters( AnnotatedTypeFactory atypeFactory, AnnotatedExecutableType method, List args) { - return adaptParameters(atypeFactory, method, args); + return adaptParameters(atypeFactory, method, args, null); } /** @@ -1008,29 +1008,31 @@ public static List expandVarArgsParameters( * @param atypeFactory the type factory to use for fetching annotated types * @param method the method or constructor's type * @param args the arguments to the method or constructor invocation + * @param invok the method or constructor invocation * @return a list of the types that the invocation arguments need to be subtype of; has the same * length as {@code args} */ public static List adaptParameters( AnnotatedTypeFactory atypeFactory, AnnotatedExecutableType method, - List args) { + List args, + Tree invok) { List parameters = method.getParameterTypes(); - // Handle anonymous constructors that extend a class with an enclosing type. + // Handle anonymous constructors that extend a class with an enclosing type, + // as in `new MyClass(){ ... }`. if (method.getElement().getKind() == ElementKind.CONSTRUCTOR && method.getElement().getEnclosingElement().getSimpleName().contentEquals("")) { DeclaredType t = TypesUtils.getSuperClassOrInterface( method.getElement().getEnclosingElement().asType(), atypeFactory.types); if (t.getEnclosingType() != null) { - if (args.isEmpty() && !parameters.isEmpty()) { - parameters = parameters.subList(1, parameters.size()); - } else if (!parameters.isEmpty()) { + if (!parameters.isEmpty()) { if (atypeFactory.types.isSameType( t.getEnclosingType(), parameters.get(0).getUnderlyingType())) { - if (!atypeFactory.types.isSameType( - TreeUtils.typeOf(args.get(0)), parameters.get(0).getUnderlyingType())) { + if (args.isEmpty() + || !atypeFactory.types.isSameType( + TreeUtils.typeOf(args.get(0)), parameters.get(0).getUnderlyingType())) { parameters = parameters.subList(1, parameters.size()); } } @@ -1039,14 +1041,20 @@ public static List adaptParameters( } // Handle vararg methods. - if (!method.getElement().isVarArgs()) { + if (!TreeUtils.isVarargsCall(invok)) { return parameters; } - if (parameters.size() == 0) { - return parameters; + if (parameters.isEmpty()) { + throw new BugInCF("isVarargsCall but parameters is empty: %s", invok); } - AnnotatedArrayType varargs = (AnnotatedArrayType) parameters.get(parameters.size() - 1); + AnnotatedTypeMirror lastParam = parameters.get(parameters.size() - 1); + if (!(lastParam instanceof AnnotatedArrayType)) { + throw new BugInCF( + String.format( + "for varargs call %s, last parameter %s is not an array", invok, lastParam)); + } + AnnotatedArrayType varargs = (AnnotatedArrayType) lastParam; if (parameters.size() == args.size()) { // Check if one sent an element or an array diff --git a/framework/tests/all-systems/Issue6078.java b/framework/tests/all-systems/Issue6078.java index 6e0d2c27b664..7d6a9d9cd6b7 100644 --- a/framework/tests/all-systems/Issue6078.java +++ b/framework/tests/all-systems/Issue6078.java @@ -1,8 +1,15 @@ import java.lang.invoke.MethodHandle; public class Issue6078 { - static void call(MethodHandle methodHandle) throws Throwable { + @SuppressWarnings("nullness:argument") // true positive. + static void call(MethodHandle methodHandle, Object[] array) throws Throwable { + // The vararg parameter disappears for the below method. It's some sort of bug in javac. + // It is worked around in TreeUtils.isVarargsCall(). methodHandle.invoke(); + // The vararg parameter does not disappaer for these method calls. + methodHandle.invoke(""); + methodHandle.invoke(array); + methodHandle.invoke(null); } void use() { diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java index 9acafe19b69b..2e225bfc43eb 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java @@ -85,6 +85,7 @@ import javax.lang.model.element.NestingKind; import javax.lang.model.element.TypeElement; import javax.lang.model.element.VariableElement; +import javax.lang.model.type.ArrayType; import javax.lang.model.type.DeclaredType; import javax.lang.model.type.ExecutableType; import javax.lang.model.type.TypeKind; @@ -2591,7 +2592,26 @@ public static boolean isVarArgs(MethodInvocationTree invok) { * @return true if the given method invocation is a varargs invocation */ public static boolean isVarargsCall(MethodInvocationTree invok) { - return ((JCMethodInvocation) invok).varargsElement != null; + if (((JCMethodInvocation) invok).varargsElement != null) { + return true; + } + + // For some calls the varargsElement element disappears when it should not. This seems to only + // be a problem with MethodHandle#invoke and only with no arguments. See + // framework/tests/all-systems/Issue6078.java. + // So also check for a mismatch between parameter and argument size. + // Such a mismatch occurs for every enum constructor: no args, two params (String name, int + // ordinal). + + List parameters = elementFromUse(invok).getParameters(); + int numParameters = parameters.size(); + if (numParameters != invok.getArguments().size()) { + if (numParameters > 0 && parameters.get(numParameters - 1).asType() instanceof ArrayType) { + return true; + } + } + + return false; } /** From f3a08a7bcdf18a3886c00fd3338d18aa6678b432 Mon Sep 17 00:00:00 2001 From: Erfan Arvan Date: Thu, 6 Jun 2024 09:42:57 -0400 Subject: [PATCH 07/33] Update contributors.tex --- docs/manual/contributors.tex | 145 ----------------------------------- 1 file changed, 145 deletions(-) diff --git a/docs/manual/contributors.tex b/docs/manual/contributors.tex index 48feb7546767..e69de29bb2d1 100644 --- a/docs/manual/contributors.tex +++ b/docs/manual/contributors.tex @@ -1,145 +0,0 @@ -Abraham Lin, -Adian Qian, -Aditya Singh, -Akash Srivastava, -Alex Liu, -Alvin Abdagic, -Anant Jain, -Anatoly Kupriyanov, -Andy Turner, -Aosen Xiong, -Arie van Deursen, -Artem Pyanykh, -Arthur Baars, -Ashish Rana, -Asumu Takikawa, -Atul Dada, -Ayush Agarwal, -Baorui Zhou, -Basil Peace, -Benno Stein, -Bohdan Sharipov, -Brian Corcoran, -Calvin Loncaric, -Charles Chen, -Charlie Garrett, -Chris Povirk, -Chris Toxiadis, -Christopher Mackie, -Colin S. Gordon, -Craig Day, -Dan Brotherston, -Dan Brown, -Daniel Zhu, -David Lazar, -David McArthur, -Di Wang, -Dilraj Singh, -Dmitriy Shepelev, -Eric Spishak, -Ethan Koenig, -Farzan Mirshekari, -Felipe R. Monteiro, -Florian Lanzinger, -Gautam Korlam, -Google Inc.\ (via @wmdietlGC), -Haaris Ahmed, -Haifeng Shi, -Hamed Taghani, -Heath Borders, -Jakub Vr\'ana, -James Yoo, -Jason Waataja, -Javier Thaine, -Jeff Luo, -Jenny Xiang, -Jeroen Meijer, -Jianchu Li, -Jiangqi Zhang, -Jiasen (Jason) Xu, -Joe Schafer, -John Vandenberg, -Jonathan Burke, -Jonathan Nieder, -Joshua Peterson, -Jugal Mistry, -Junhao Hu, -Kanak Das, -Kartikeya Goswami, -Kenneth Knowles, -Kivanc Muslu, -Konstantin Weitz, -Lazaro Clapp, -Leo Liu, -Liam Miller-Cushon, -Lian Sun, -Luqman Aden, -Mahmood Ali, -Manu Sridharan, -Mark Roberts, -Markus Frohme, -Martin Kellogg, -Matt Mullen, -Maximilian Gama, -Michael Bayne, -Michael Coblenz, -Michael Ernst, -Michael Hixson, -Michael Sloan, -Michal Stehlik, -Mier Ta, -Mrigank Arora, -Muyeed Ahmed, -Narges Shadab, -Neil Brown, -Nhat Dinh, -Nhat Nguyen, -Nicholas Breen, -Nikhil Shinde, -Nima Karimipour, -Nitin Kumar Das, -Oleg Shchelykalnov, -Olek Wojnar, -Pascal Wittmann, -Patrick Meiring, -Paul Vines, -Paulo Barros, -Philip Lai, -Pratik Bhusal, -Prionti Nasir, -Priti Chattopadhyay, -Rashmi Mudduluru, -Ravi Roshan, -Renato Athaydes, -Ren\'e Just, -Ren\'e Kraneis, -Rob Bygrave, -Ruturaj Mohanty, -Ryan Oblak, -Sadaf Tajik, -Sagar Tewari, -Sanjay Malakar, -Sean C. Sullivan, -Sean McLaughlin, -Sebastian Schuberth, -Shinya Yoshida, -Shubham Raj, -Sidney Monteiro, -Simon Gerst, -Stefan Heule, -Steph Dietzel, -Stephan Schroevers, -Stuart Pernsteiner, -Suzanne Millstein, -Thomas Schweizer, -Thomas Wei\ss schuh, -Tony Wang, -Trask Stalnaker, -Travis Haagen, -Utsav Oza, -Vatsal Sura, -Vladimir Sitnikov, -Vlastimil Dort, -Weitian Xing, -Werner Dietl, -Zhiping Cai. From 5df02b702be60c46fbb22b60abd327f2874c55c0 Mon Sep 17 00:00:00 2001 From: Erfan Arvan Date: Thu, 6 Jun 2024 10:09:20 -0400 Subject: [PATCH 08/33] Update contributors.tex to include the latest contributors --- docs/manual/contributors.tex | 145 +++++++++++++++++++++++++++++++++++ 1 file changed, 145 insertions(+) diff --git a/docs/manual/contributors.tex b/docs/manual/contributors.tex index e69de29bb2d1..48feb7546767 100644 --- a/docs/manual/contributors.tex +++ b/docs/manual/contributors.tex @@ -0,0 +1,145 @@ +Abraham Lin, +Adian Qian, +Aditya Singh, +Akash Srivastava, +Alex Liu, +Alvin Abdagic, +Anant Jain, +Anatoly Kupriyanov, +Andy Turner, +Aosen Xiong, +Arie van Deursen, +Artem Pyanykh, +Arthur Baars, +Ashish Rana, +Asumu Takikawa, +Atul Dada, +Ayush Agarwal, +Baorui Zhou, +Basil Peace, +Benno Stein, +Bohdan Sharipov, +Brian Corcoran, +Calvin Loncaric, +Charles Chen, +Charlie Garrett, +Chris Povirk, +Chris Toxiadis, +Christopher Mackie, +Colin S. Gordon, +Craig Day, +Dan Brotherston, +Dan Brown, +Daniel Zhu, +David Lazar, +David McArthur, +Di Wang, +Dilraj Singh, +Dmitriy Shepelev, +Eric Spishak, +Ethan Koenig, +Farzan Mirshekari, +Felipe R. Monteiro, +Florian Lanzinger, +Gautam Korlam, +Google Inc.\ (via @wmdietlGC), +Haaris Ahmed, +Haifeng Shi, +Hamed Taghani, +Heath Borders, +Jakub Vr\'ana, +James Yoo, +Jason Waataja, +Javier Thaine, +Jeff Luo, +Jenny Xiang, +Jeroen Meijer, +Jianchu Li, +Jiangqi Zhang, +Jiasen (Jason) Xu, +Joe Schafer, +John Vandenberg, +Jonathan Burke, +Jonathan Nieder, +Joshua Peterson, +Jugal Mistry, +Junhao Hu, +Kanak Das, +Kartikeya Goswami, +Kenneth Knowles, +Kivanc Muslu, +Konstantin Weitz, +Lazaro Clapp, +Leo Liu, +Liam Miller-Cushon, +Lian Sun, +Luqman Aden, +Mahmood Ali, +Manu Sridharan, +Mark Roberts, +Markus Frohme, +Martin Kellogg, +Matt Mullen, +Maximilian Gama, +Michael Bayne, +Michael Coblenz, +Michael Ernst, +Michael Hixson, +Michael Sloan, +Michal Stehlik, +Mier Ta, +Mrigank Arora, +Muyeed Ahmed, +Narges Shadab, +Neil Brown, +Nhat Dinh, +Nhat Nguyen, +Nicholas Breen, +Nikhil Shinde, +Nima Karimipour, +Nitin Kumar Das, +Oleg Shchelykalnov, +Olek Wojnar, +Pascal Wittmann, +Patrick Meiring, +Paul Vines, +Paulo Barros, +Philip Lai, +Pratik Bhusal, +Prionti Nasir, +Priti Chattopadhyay, +Rashmi Mudduluru, +Ravi Roshan, +Renato Athaydes, +Ren\'e Just, +Ren\'e Kraneis, +Rob Bygrave, +Ruturaj Mohanty, +Ryan Oblak, +Sadaf Tajik, +Sagar Tewari, +Sanjay Malakar, +Sean C. Sullivan, +Sean McLaughlin, +Sebastian Schuberth, +Shinya Yoshida, +Shubham Raj, +Sidney Monteiro, +Simon Gerst, +Stefan Heule, +Steph Dietzel, +Stephan Schroevers, +Stuart Pernsteiner, +Suzanne Millstein, +Thomas Schweizer, +Thomas Wei\ss schuh, +Tony Wang, +Trask Stalnaker, +Travis Haagen, +Utsav Oza, +Vatsal Sura, +Vladimir Sitnikov, +Vlastimil Dort, +Weitian Xing, +Werner Dietl, +Zhiping Cai. From 42d7812da7f48f971f97ddec79fdb5e3f3ae237a Mon Sep 17 00:00:00 2001 From: Erfan Arvan Date: Thu, 6 Jun 2024 15:10:29 -0400 Subject: [PATCH 09/33] Update contributors.tex to include my name --- docs/manual/contributors.tex | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/manual/contributors.tex b/docs/manual/contributors.tex index 48feb7546767..73fc71477c09 100644 --- a/docs/manual/contributors.tex +++ b/docs/manual/contributors.tex @@ -142,4 +142,5 @@ Vlastimil Dort, Weitian Xing, Werner Dietl, -Zhiping Cai. +Zhiping Cai, +Erfan Arvan. From 711ae4dd12fb2778d0aaf15c69ee48727e0d6cd4 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Thu, 6 Jun 2024 08:20:58 -0700 Subject: [PATCH 10/33] How to indicate that side effects can change a value's type qualifiers (#6660) --- docs/manual/creating-a-checker.tex | 21 +++++++++++++++++---- 1 file changed, 17 insertions(+), 4 deletions(-) diff --git a/docs/manual/creating-a-checker.tex b/docs/manual/creating-a-checker.tex index 14b376d2d46c..0ccef018c1f0 100644 --- a/docs/manual/creating-a-checker.tex +++ b/docs/manual/creating-a-checker.tex @@ -1872,10 +1872,23 @@ \end{enumerate} -\subsectionAndLabel{Disabling flow-sensitive inference}{creating-dataflow-disable} - -In the uncommon case that you wish to disable the Checker Framework's -built-in flow inference in your checker (this is different than choosing +\label{creating-dataflow-disable} % temporary label; remove in January 2025 +\subsectionAndLabel{Further customizing flow-sensitive inference}{creating-dataflow-customization} + +By default, the Checker Framework assumes that modifications to an object's +fields do not change its type qualifiers. This is true for all +provenance-based type systems (see +Section~\ref{type-refinement-runtime-tests}), for all value-based type +systems over immutable values, and for some other type systems. To +indicate that \textbf{side effects can change a value's type qualifiers}, +write \ in the type factory +constructor, before the call to \. Note that this +setting may lead to large numbers of false positive warnings. You can +reduce the number of false positive warnings by writing more precise side +effect annotations. + +In the uncommon case that you wish to \textbf{disable the Checker Framework's +built-in flow inference} in your checker (this is different than choosing not to extend it as described in Section~\ref{creating-dataflow}), put the following two lines at the beginning of the constructor for your subtype of \refclass{common/basetype}{BaseAnnotatedTypeFactory}: From d9a6504e834606f38f1b3d494f16522b3e542287 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Thu, 6 Jun 2024 09:02:38 -0700 Subject: [PATCH 11/33] Define `TreeUtils.fieldsFromClassTree()` (#6659) --- .../InitializationAnnotatedTypeFactory.java | 4 ++-- .../org/checkerframework/javacutil/TreeUtils.java | 14 ++++++++++++++ 2 files changed, 16 insertions(+), 2 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationAnnotatedTypeFactory.java index db848a02e13b..35da707a4d63 100644 --- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationAnnotatedTypeFactory.java @@ -582,7 +582,7 @@ public IPair, List> getUninitializedFields( boolean isStatic, Collection receiverAnnotations) { ClassTree currentClass = TreePathUtil.enclosingClass(path); - List fields = InitializationChecker.getAllFields(currentClass); + List fields = TreeUtils.fieldsFromClassTree(currentClass); List uninitWithInvariantAnno = new ArrayList<>(); List uninitWithoutInvariantAnno = new ArrayList<>(); for (VariableTree field : fields) { @@ -635,7 +635,7 @@ public List getInitializedInvariantFields(Store store, TreePath pa // TODO: Instead of passing the TreePath around, can we use // getCurrentClassTree? ClassTree currentClass = TreePathUtil.enclosingClass(path); - List fields = InitializationChecker.getAllFields(currentClass); + List fields = TreeUtils.fieldsFromClassTree(currentClass); List initializedFields = new ArrayList<>(); for (VariableTree field : fields) { VariableElement fieldElem = TreeUtils.elementFromDeclaration(field); diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java index 2e225bfc43eb..d72bbfe65cb7 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java @@ -75,6 +75,7 @@ import java.util.List; import java.util.Set; import java.util.StringJoiner; +import java.util.stream.Collectors; import javax.annotation.processing.ProcessingEnvironment; import javax.lang.model.SourceVersion; import javax.lang.model.element.AnnotationMirror; @@ -334,6 +335,19 @@ public static boolean isSelfAccess(ExpressionTree tree) { return elementFromDeclaration(tree); } + /** + * Returns the fields that are declared within the given class declaration. + * + * @param tree the {@link ClassTree} node to get the fields for + * @return the list of fields that are declared within the given class declaration + */ + public static List fieldsFromClassTree(ClassTree tree) { + return tree.getMembers().stream() + .filter(t -> t.getKind() == Kind.VARIABLE) + .map(t -> (VariableTree) t) + .collect(Collectors.toList()); + } + /** * Returns the element corresponding to the given tree. * From 342bc94955b5b5ab413f4437781e028a5ba4be26 Mon Sep 17 00:00:00 2001 From: Erfan Arvan Date: Fri, 7 Jun 2024 01:50:30 -0400 Subject: [PATCH 12/33] Update contributors.tex after make it again --- docs/manual/contributors.tex | 146 ----------------------------------- 1 file changed, 146 deletions(-) diff --git a/docs/manual/contributors.tex b/docs/manual/contributors.tex index 73fc71477c09..e69de29bb2d1 100644 --- a/docs/manual/contributors.tex +++ b/docs/manual/contributors.tex @@ -1,146 +0,0 @@ -Abraham Lin, -Adian Qian, -Aditya Singh, -Akash Srivastava, -Alex Liu, -Alvin Abdagic, -Anant Jain, -Anatoly Kupriyanov, -Andy Turner, -Aosen Xiong, -Arie van Deursen, -Artem Pyanykh, -Arthur Baars, -Ashish Rana, -Asumu Takikawa, -Atul Dada, -Ayush Agarwal, -Baorui Zhou, -Basil Peace, -Benno Stein, -Bohdan Sharipov, -Brian Corcoran, -Calvin Loncaric, -Charles Chen, -Charlie Garrett, -Chris Povirk, -Chris Toxiadis, -Christopher Mackie, -Colin S. Gordon, -Craig Day, -Dan Brotherston, -Dan Brown, -Daniel Zhu, -David Lazar, -David McArthur, -Di Wang, -Dilraj Singh, -Dmitriy Shepelev, -Eric Spishak, -Ethan Koenig, -Farzan Mirshekari, -Felipe R. Monteiro, -Florian Lanzinger, -Gautam Korlam, -Google Inc.\ (via @wmdietlGC), -Haaris Ahmed, -Haifeng Shi, -Hamed Taghani, -Heath Borders, -Jakub Vr\'ana, -James Yoo, -Jason Waataja, -Javier Thaine, -Jeff Luo, -Jenny Xiang, -Jeroen Meijer, -Jianchu Li, -Jiangqi Zhang, -Jiasen (Jason) Xu, -Joe Schafer, -John Vandenberg, -Jonathan Burke, -Jonathan Nieder, -Joshua Peterson, -Jugal Mistry, -Junhao Hu, -Kanak Das, -Kartikeya Goswami, -Kenneth Knowles, -Kivanc Muslu, -Konstantin Weitz, -Lazaro Clapp, -Leo Liu, -Liam Miller-Cushon, -Lian Sun, -Luqman Aden, -Mahmood Ali, -Manu Sridharan, -Mark Roberts, -Markus Frohme, -Martin Kellogg, -Matt Mullen, -Maximilian Gama, -Michael Bayne, -Michael Coblenz, -Michael Ernst, -Michael Hixson, -Michael Sloan, -Michal Stehlik, -Mier Ta, -Mrigank Arora, -Muyeed Ahmed, -Narges Shadab, -Neil Brown, -Nhat Dinh, -Nhat Nguyen, -Nicholas Breen, -Nikhil Shinde, -Nima Karimipour, -Nitin Kumar Das, -Oleg Shchelykalnov, -Olek Wojnar, -Pascal Wittmann, -Patrick Meiring, -Paul Vines, -Paulo Barros, -Philip Lai, -Pratik Bhusal, -Prionti Nasir, -Priti Chattopadhyay, -Rashmi Mudduluru, -Ravi Roshan, -Renato Athaydes, -Ren\'e Just, -Ren\'e Kraneis, -Rob Bygrave, -Ruturaj Mohanty, -Ryan Oblak, -Sadaf Tajik, -Sagar Tewari, -Sanjay Malakar, -Sean C. Sullivan, -Sean McLaughlin, -Sebastian Schuberth, -Shinya Yoshida, -Shubham Raj, -Sidney Monteiro, -Simon Gerst, -Stefan Heule, -Steph Dietzel, -Stephan Schroevers, -Stuart Pernsteiner, -Suzanne Millstein, -Thomas Schweizer, -Thomas Wei\ss schuh, -Tony Wang, -Trask Stalnaker, -Travis Haagen, -Utsav Oza, -Vatsal Sura, -Vladimir Sitnikov, -Vlastimil Dort, -Weitian Xing, -Werner Dietl, -Zhiping Cai, -Erfan Arvan. From b5a62d8cb530dcffb393003f3e0b35b6c62c22b5 Mon Sep 17 00:00:00 2001 From: Erfan Arvan Date: Fri, 7 Jun 2024 02:05:10 -0400 Subject: [PATCH 13/33] Try to pass CI test -> Contrubutors names --- docs/manual/contributors.tex | 146 +++++++++++++++++++++++++++++++++++ 1 file changed, 146 insertions(+) diff --git a/docs/manual/contributors.tex b/docs/manual/contributors.tex index e69de29bb2d1..711b5d8ee944 100644 --- a/docs/manual/contributors.tex +++ b/docs/manual/contributors.tex @@ -0,0 +1,146 @@ +Abraham Lin, +Adian Qian, +Aditya Singh, +Akash Srivastava, +Alex Liu, +Alvin Abdagic, +Anant Jain, +Anatoly Kupriyanov, +Andy Turner, +Aosen Xiong, +Arie van Deursen, +Artem Pyanykh, +Arthur Baars, +Ashish Rana, +Asumu Takikawa, +Atul Dada, +Ayush Agarwal, +Baorui Zhou, +Basil Peace, +Benno Stein, +Bohdan Sharipov, +Brian Corcoran, +Calvin Loncaric, +Charles Chen, +Charlie Garrett, +Chris Povirk, +Chris Toxiadis, +Christopher Mackie, +Colin S. Gordon, +Craig Day, +Dan Brotherston, +Dan Brown, +Daniel Zhu, +David Lazar, +David McArthur, +Di Wang, +Dilraj Singh, +Dmitriy Shepelev, +Erfan Arvan, +Eric Spishak, +Ethan Koenig, +Farzan Mirshekari, +Felipe R. Monteiro, +Florian Lanzinger, +Gautam Korlam, +Google Inc.\ (via @wmdietlGC), +Haaris Ahmed, +Haifeng Shi, +Hamed Taghani, +Heath Borders, +Jakub Vr\'ana, +James Yoo, +Jason Waataja, +Javier Thaine, +Jeff Luo, +Jenny Xiang, +Jeroen Meijer, +Jianchu Li, +Jiangqi Zhang, +Jiasen (Jason) Xu, +Joe Schafer, +John Vandenberg, +Jonathan Burke, +Jonathan Nieder, +Joshua Peterson, +Jugal Mistry, +Junhao Hu, +Kanak Das, +Kartikeya Goswami, +Kenneth Knowles, +Kivanc Muslu, +Konstantin Weitz, +Lazaro Clapp, +Leo Liu, +Liam Miller-Cushon, +Lian Sun, +Luqman Aden, +Mahmood Ali, +Manu Sridharan, +Mark Roberts, +Markus Frohme, +Martin Kellogg, +Matt Mullen, +Maximilian Gama, +Michael Bayne, +Michael Coblenz, +Michael Ernst, +Michael Hixson, +Michael Sloan, +Michal Stehlik, +Mier Ta, +Mrigank Arora, +Muyeed Ahmed, +Narges Shadab, +Neil Brown, +Nhat Dinh, +Nhat Nguyen, +Nicholas Breen, +Nikhil Shinde, +Nima Karimipour, +Nitin Kumar Das, +Oleg Shchelykalnov, +Olek Wojnar, +Pascal Wittmann, +Patrick Meiring, +Paul Vines, +Paulo Barros, +Philip Lai, +Pratik Bhusal, +Prionti Nasir, +Priti Chattopadhyay, +Rashmi Mudduluru, +Ravi Roshan, +Renato Athaydes, +Ren\'e Just, +Ren\'e Kraneis, +Rob Bygrave, +Ruturaj Mohanty, +Ryan Oblak, +Sadaf Tajik, +Sagar Tewari, +Sanjay Malakar, +Sean C. Sullivan, +Sean McLaughlin, +Sebastian Schuberth, +Shinya Yoshida, +Shubham Raj, +Sidney Monteiro, +Simon Gerst, +Stefan Heule, +Steph Dietzel, +Stephan Schroevers, +Stuart Pernsteiner, +Suzanne Millstein, +Thomas Schweizer, +Thomas Wei\ss schuh, +Tony Wang, +Trask Stalnaker, +Travis Haagen, +Utsav Oza, +Vatsal Sura, +Vladimir Sitnikov, +Vlastimil Dort, +Weitian Xing, +Werner Dietl, +Zhiping Cai. From 5f3f89dbdf8db20c3d20fc0a94d6cbfea7a460da Mon Sep 17 00:00:00 2001 From: Erfan Arvan Date: Fri, 7 Jun 2024 03:25:38 -0400 Subject: [PATCH 14/33] Update contributors.tex to reflect latest changes --- docs/manual/contributors.tex | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/docs/manual/contributors.tex b/docs/manual/contributors.tex index 711b5d8ee944..490300844ea1 100644 --- a/docs/manual/contributors.tex +++ b/docs/manual/contributors.tex @@ -143,4 +143,5 @@ Vlastimil Dort, Weitian Xing, Werner Dietl, -Zhiping Cai. +Zhiping Cai, +erfanarvan. From 81f1f2be4cb3fc92085b59343d80d4bd94eaa02b Mon Sep 17 00:00:00 2001 From: Suzanne Millstein Date: Sat, 8 Jun 2024 15:34:47 -0700 Subject: [PATCH 15/33] Improve Javadoc for `getAnnotationFromJavaExpression` --- .../type/GenericAnnotatedTypeFactory.java | 43 +++++++++++++------ 1 file changed, 30 insertions(+), 13 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 6cd18de42243..d9cb6cf1827f 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -907,13 +907,20 @@ protected void postDirectSuperTypes( } /** - * Returns the primary annotation on expression if it were evaluated at path. + * Returns the primary annotation with {@code clazz} on {@code expression}'s type, at a particular + * location. The returned annotation may be null even if the expression should have a primary + * annotation of {@code clazz}. This is because {@link JavaExpression}s do not always have enough + * information to get an annotated type. * - * @param expression a Java expression + *

    This method should only be used if a tree, element, or node is not available for {@code + * expression}. Use {@link #getAnnotatedType(Tree)} or {@link #getAnnotatedType(Element)} instead. + * + * @param expression the expression for which the annotation is returned * @param tree current tree * @param path location at which expression is evaluated - * @param clazz class of the annotation - * @return the annotation on expression or null if one does not exist + * @param clazz the annotation class for which to look + * @return the annotation of {@code clazz} on {@code expression}'s type, or null if one does not + * exist or if {@code expression} does not have enough information to get the annotated type * @throws JavaExpressionParseException thrown if the expression cannot be parsed */ public @Nullable AnnotationMirror getAnnotationFromJavaExpressionString( @@ -924,12 +931,19 @@ protected void postDirectSuperTypes( } /** - * Returns the primary annotation on an expression, at a particular location. + * Returns the primary annotation with {@code clazz} on {@code expr}'s type, at a particular + * location. The returned annotation may be null even if the expression should have a primary + * annotation of {@code clazz}. This is because {@link JavaExpression}s do not always have enough + * information to get an annotated type. + * + *

    This method should only be used if a tree, element, or node is not available for {@code + * expr}. Use {@link #getAnnotatedType(Tree)} or {@link #getAnnotatedType(Element)} instead. * * @param expr the expression for which the annotation is returned * @param tree current tree - * @param clazz the Class of the annotation - * @return the annotation on expression or null if one does not exist + * @param clazz the annotation class for which to look + * @return the annotation of {@code clazz} on {@code expr}'s type, or null if one does not exist + * or if {@code expr} does not have enough information to get the annotated type */ public @Nullable AnnotationMirror getAnnotationFromJavaExpression( JavaExpression expr, Tree tree, Class clazz) { @@ -937,14 +951,19 @@ protected void postDirectSuperTypes( } /** - * Returns the primary annotations on an expression, at a particular location. + * Returns the primary annotations on an expression, at a particular location. The returned set of + * annotations may be empty even if the expression should have primary annotations. This is + * because {@link JavaExpression} do not always have enough information to get an annotated type. + * + *

    This method should only be used if a tree, element, or node is not available for {@code + * expr}. Use {@link #getAnnotatedType(Tree)} or {@link #getAnnotatedType(Element)} instead. * * @param expr the expression for which the annotation is returned * @param tree current tree - * @return the annotation on expression or null if one does not exist + * @return the annotations on the expression. May be empty if {@code expr} does not have enough + * information to get the annotated type. */ - public @Nullable AnnotationMirrorSet getAnnotationsFromJavaExpression( - JavaExpression expr, Tree tree) { + public AnnotationMirrorSet getAnnotationsFromJavaExpression(JavaExpression expr, Tree tree) { // Look in the store if (CFAbstractStore.canInsertJavaExpression(expr)) { @@ -953,8 +972,6 @@ protected void postDirectSuperTypes( if (store != null) { Value value = store.getValue(expr); if (value != null) { - // Is it possible that this lacks some annotations that appear in the type - // factory? return value.getAnnotations(); } } From 8c345fde372a414a5036cc6321100e81b54b94b1 Mon Sep 17 00:00:00 2001 From: James Yoo <24359440+jyoo980@users.noreply.github.com> Date: Tue, 11 Jun 2024 15:21:57 -0400 Subject: [PATCH 16/33] Add `graphviz` to list of dev dependencies for macOS --- docs/manual/troubleshooting.tex | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/docs/manual/troubleshooting.tex b/docs/manual/troubleshooting.tex index 9e0b72f568d0..530ec346feb6 100644 --- a/docs/manual/troubleshooting.tex +++ b/docs/manual/troubleshooting.tex @@ -767,7 +767,7 @@ \begin{Verbatim} brew update -brew install git ant hevea maven librsvg unzip make +brew install git graphviz ant hevea maven librsvg unzip make brew tap homebrew/cask-versions brew install --cask temurin17 brew install --cask mactex From 118b7716511fcaad592fa6ceb39aa0a5b2bf4655 Mon Sep 17 00:00:00 2001 From: Erfan Arvan Date: Tue, 18 Jun 2024 19:55:54 -0400 Subject: [PATCH 17/33] Exclude my username from contributors.tex --- docs/manual/contributors.tex | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/docs/manual/contributors.tex b/docs/manual/contributors.tex index 490300844ea1..711b5d8ee944 100644 --- a/docs/manual/contributors.tex +++ b/docs/manual/contributors.tex @@ -143,5 +143,4 @@ Vlastimil Dort, Weitian Xing, Werner Dietl, -Zhiping Cai, -erfanarvan. +Zhiping Cai. From 4818ac2602fb1c8717848cd8373c92d4e39e2888 Mon Sep 17 00:00:00 2001 From: Erfan Arvan Date: Tue, 18 Jun 2024 19:48:37 -0400 Subject: [PATCH 18/33] Transferred the proposed change for handling WPI loop for unknowninitialization annotations to NullnessAnnotatedTypeFactory --- .../NullnessAnnotatedTypeFactory.java | 24 ++++++++++++++ .../WholeProgramInferenceImplementation.java | 31 ++----------------- .../framework/type/AnnotatedTypeFactory.java | 9 ++++++ 3 files changed, 36 insertions(+), 28 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java index e7d0044377ca..793ee10ead7e 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java @@ -961,6 +961,30 @@ public void wpiAdjustForUpdateNonField(AnnotatedTypeMirror rhsATM) { } } + // For all assignments, If rhsmATM is Nullable or MonotonicNonNull and has + // the UnknownInitialization annotation, and if the annotation is not + // UnknownInitialization(java.lang.Object.class), replace it with + // UnknownInitialization(java.lang.Object.class). This is because there is + // likely a constructor where it hasn't been initialized, and we haven't + // considered its effect. Otherwise, WPI might get stuck in a loop. + @Override + public void wpiAdjustForInitializationAnnotations(AnnotatedTypeMirror rhsATM) { + if ((rhsATM.hasPrimaryAnnotation(Nullable.class) + || rhsATM.hasPrimaryAnnotation(MonotonicNonNull.class))) { + for (AnnotationMirror anno : rhsATM.getPrimaryAnnotations()) { + if (AnnotationUtils.areSameByName( + anno, "org.checkerframework.checker.initialization.qual.UnknownInitialization") + && !anno.getAnnotationType() + .toString() + .equals( + "@org" + + ".checkerframework.checker.initialization.qual.UnknownInitialization(java.lang.Object.class)")) { + rhsATM.replaceAnnotation(UNDER_INITALIZATION); + } + } + } + } + @Override public boolean wpiShouldInferTypesForReceivers() { // All receivers must be non-null, or the dereference involved in diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java index 733861694310..262258fb105c 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java @@ -18,8 +18,6 @@ import javax.lang.model.util.ElementFilter; import org.checkerframework.afu.scenelib.util.JVMNames; import org.checkerframework.checker.index.qual.Positive; -import org.checkerframework.checker.initialization.qual.UnknownInitialization; -import org.checkerframework.checker.nullness.qual.MonotonicNonNull; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.dataflow.analysis.Analysis; @@ -1003,32 +1001,9 @@ protected void updateAnnotationSet( return; } - // For parameters, If rhsmATM is Nullable or MonotonicNonNull and has the - // UnknownInitialization annotation, and if the annotation is not - // UnknownInitialization(java.lang.Object.class), replace it with - // UnknownInitialization(java.lang.Object.class). This is because there is - // likely a constructor where it hasn't been initialized, and we haven't - // considered its effect. Otherwise, WPI might get stuck in a loop. - if (defLoc == TypeUseLocation.PARAMETER - && (rhsATM.hasPrimaryAnnotation(Nullable.class) - || rhsATM.hasPrimaryAnnotation(MonotonicNonNull.class))) { - for (AnnotationMirror anno : rhsATM.getPrimaryAnnotations()) { - if (anno.getAnnotationType() - .asElement() - .getSimpleName() - .contentEquals("UnknownInitialization") - && !anno.getAnnotationType() - .toString() - .equals( - "@org" - + ".checkerframework.checker.initialization.qual.UnknownInitialization(java.lang.Object.class)")) { - AnnotationMirror unanno = - AnnotationBuilder.fromClass( - atypeFactory.getElementUtils(), UnknownInitialization.class); - rhsATM.replaceAnnotation(unanno); - } - } - } + // Update Initialization Annotations in WPI. It is only applied to + // Nullness-related qualifiers' inference to prevent possible loops. + atypeFactory.wpiAdjustForInitializationAnnotations(rhsATM); AnnotatedTypeMirror atmFromStorage = storage.atmFromStorageLocation(rhsATM.getUnderlyingType(), annotationsToUpdate); diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java index 84c918264499..d14ae32e2eda 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -5523,6 +5523,15 @@ public boolean wpiShouldInferTypesForReceivers() { return true; } + /** + * Changes the type of {@code rhsATM} when being assigned to anything, for use by whole-program + * inference. The default implementation does nothing. + * + * @param rhsATM the type of the rhs of the pseudo-assignment, which is side-effected by this + * method + */ + public void wpiAdjustForInitializationAnnotations(AnnotatedTypeMirror rhsATM) {} + /** * Side-effects the method or constructor annotations to make any desired changes before writing * to an annotation file. From 1c31423488d11db50af9de66a1580e955d45e175 Mon Sep 17 00:00:00 2001 From: Erfan Arvan Date: Tue, 18 Jun 2024 19:55:54 -0400 Subject: [PATCH 19/33] Rename method to adjust annotations before updating annotation set, update method usage, and revise comments --- .../checker/nullness/NullnessAnnotatedTypeFactory.java | 10 ++++------ docs/manual/contributors.tex | 3 +-- .../WholeProgramInferenceImplementation.java | 5 ++--- .../framework/type/AnnotatedTypeFactory.java | 2 +- 4 files changed, 8 insertions(+), 12 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java index 793ee10ead7e..67b707a80ee9 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java @@ -968,17 +968,15 @@ public void wpiAdjustForUpdateNonField(AnnotatedTypeMirror rhsATM) { // likely a constructor where it hasn't been initialized, and we haven't // considered its effect. Otherwise, WPI might get stuck in a loop. @Override - public void wpiAdjustForInitializationAnnotations(AnnotatedTypeMirror rhsATM) { + public void wpiAdjustAnnotationsBeforeUpdate(AnnotatedTypeMirror rhsATM) { if ((rhsATM.hasPrimaryAnnotation(Nullable.class) || rhsATM.hasPrimaryAnnotation(MonotonicNonNull.class))) { for (AnnotationMirror anno : rhsATM.getPrimaryAnnotations()) { if (AnnotationUtils.areSameByName( anno, "org.checkerframework.checker.initialization.qual.UnknownInitialization") - && !anno.getAnnotationType() - .toString() - .equals( - "@org" - + ".checkerframework.checker.initialization.qual.UnknownInitialization(java.lang.Object.class)")) { + && !AnnotationUtils.areSameByName( + anno, + "org.checkerframework.checker.initialization.qual.UnderInitialization(java.lang.Object.class")) { rhsATM.replaceAnnotation(UNDER_INITALIZATION); } } diff --git a/docs/manual/contributors.tex b/docs/manual/contributors.tex index 490300844ea1..711b5d8ee944 100644 --- a/docs/manual/contributors.tex +++ b/docs/manual/contributors.tex @@ -143,5 +143,4 @@ Vlastimil Dort, Weitian Xing, Werner Dietl, -Zhiping Cai, -erfanarvan. +Zhiping Cai. diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java index 262258fb105c..1d65dc9d1c81 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java @@ -1001,9 +1001,8 @@ protected void updateAnnotationSet( return; } - // Update Initialization Annotations in WPI. It is only applied to - // Nullness-related qualifiers' inference to prevent possible loops. - atypeFactory.wpiAdjustForInitializationAnnotations(rhsATM); + // Update the right-hand side (rhs) annotations if necessary before updating the annotation set + atypeFactory.wpiAdjustAnnotationsBeforeUpdate(rhsATM); AnnotatedTypeMirror atmFromStorage = storage.atmFromStorageLocation(rhsATM.getUnderlyingType(), annotationsToUpdate); diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java index d14ae32e2eda..8b1f86fc3159 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -5530,7 +5530,7 @@ public boolean wpiShouldInferTypesForReceivers() { * @param rhsATM the type of the rhs of the pseudo-assignment, which is side-effected by this * method */ - public void wpiAdjustForInitializationAnnotations(AnnotatedTypeMirror rhsATM) {} + public void wpiAdjustAnnotationsBeforeUpdate(AnnotatedTypeMirror rhsATM) {} /** * Side-effects the method or constructor annotations to make any desired changes before writing From d7acb57182b2ea56d5e6426a80c838e566a2ff5d Mon Sep 17 00:00:00 2001 From: Erfan Arvan Date: Sat, 6 Jul 2024 01:43:03 -0400 Subject: [PATCH 20/33] Changed the name of the method, enhanced the body, and transferred the method to NullnessAnnotatedTypeFactory.java to make it local for Nullness-related inference rather than for all checkers. Also added a test case for the corresponding issue in the ainfer-nullness tests. --- .../NullnessAnnotatedTypeFactory.java | 38 ++++--- ...rk.checker.nullness.KeyForSubchecker.ajava | 94 ++++++++++++++++ ...ork.checker.nullness.NullnessChecker.ajava | 101 ++++++++++++++++++ .../ainfer-nullness/non-annotated/Game.java | 73 +++++++++++++ .../WholeProgramInferenceImplementation.java | 3 - .../framework/type/AnnotatedTypeFactory.java | 9 -- 6 files changed, 293 insertions(+), 25 deletions(-) create mode 100644 checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.KeyForSubchecker.ajava create mode 100644 checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.NullnessChecker.ajava create mode 100644 checker/tests/ainfer-nullness/non-annotated/Game.java diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java index 67b707a80ee9..b09b7c91a977 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessAnnotatedTypeFactory.java @@ -50,6 +50,7 @@ import org.checkerframework.dataflow.cfg.node.Node; import org.checkerframework.dataflow.util.NodeUtils; import org.checkerframework.framework.flow.CFAbstractAnalysis; +import org.checkerframework.framework.qual.TypeUseLocation; import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.framework.type.AnnotatedTypeFormatter; import org.checkerframework.framework.type.AnnotatedTypeMirror; @@ -938,6 +939,8 @@ public boolean isImmutable(TypeMirror type) { @Override public void wpiAdjustForUpdateField( Tree lhsTree, Element element, String fieldName, AnnotatedTypeMirror rhsATM) { + // Adjust initialization annotations first + wpiAdjustInitializationAnnotations(rhsATM, TypeUseLocation.FIELD); // Synthetic variable names contain "#". Ignore them. if (!rhsATM.hasPrimaryAnnotation(Nullable.class) || fieldName.contains("#")) { return; @@ -956,28 +959,37 @@ public void wpiAdjustForUpdateField( // then change rhs to @Nullable @Override public void wpiAdjustForUpdateNonField(AnnotatedTypeMirror rhsATM) { + // Adjust initialization annotations first + wpiAdjustInitializationAnnotations(rhsATM, TypeUseLocation.OTHERWISE); if (rhsATM.hasPrimaryAnnotation(MonotonicNonNull.class)) { rhsATM.replaceAnnotation(NULLABLE); } } - // For all assignments, If rhsmATM is Nullable or MonotonicNonNull and has - // the UnknownInitialization annotation, and if the annotation is not - // UnknownInitialization(java.lang.Object.class), replace it with - // UnknownInitialization(java.lang.Object.class). This is because there is - // likely a constructor where it hasn't been initialized, and we haven't - // considered its effect. Otherwise, WPI might get stuck in a loop. - @Override - public void wpiAdjustAnnotationsBeforeUpdate(AnnotatedTypeMirror rhsATM) { + /** + * Changes the type of {@code rhsATM} when assigned to any pseudo-assignment, for use by + * whole-program inference. + * + *

    If {@code rhsATM} is Nullable or MonotonicNonNull and has the UnknownInitialization + * annotation, replace it with {@code UnknownInitialization(java.lang.Object.class)}. This ensures + * that if there is a constructor where the type hasn't been initialized, its effect is + * considered. Otherwise, whole-program inference might get stuck in a loop. + * + * @param rhsATM the type of the right-hand side of the pseudo-assignment, which is side-effected + * by this method + * @param defLoc the location where the annotation will be added. It is either a FIELD or a + * non-field (OTHERWISE). + */ + public void wpiAdjustInitializationAnnotations( + AnnotatedTypeMirror rhsATM, TypeUseLocation defLoc) { + // defLoc is defined to be used in the future if needed to differentiate between field and + // non-field locations if ((rhsATM.hasPrimaryAnnotation(Nullable.class) || rhsATM.hasPrimaryAnnotation(MonotonicNonNull.class))) { for (AnnotationMirror anno : rhsATM.getPrimaryAnnotations()) { if (AnnotationUtils.areSameByName( - anno, "org.checkerframework.checker.initialization.qual.UnknownInitialization") - && !AnnotationUtils.areSameByName( - anno, - "org.checkerframework.checker.initialization.qual.UnderInitialization(java.lang.Object.class")) { - rhsATM.replaceAnnotation(UNDER_INITALIZATION); + anno, "org.checkerframework.checker.initialization.qual" + ".UnknownInitialization")) { + rhsATM.replaceAnnotation(UNKNOWN_INITIALIZATION); } } } diff --git a/checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.KeyForSubchecker.ajava b/checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.KeyForSubchecker.ajava new file mode 100644 index 000000000000..789d78763eeb --- /dev/null +++ b/checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.KeyForSubchecker.ajava @@ -0,0 +1,94 @@ +import org.checkerframework.checker.initialization.qual.*; +import org.checkerframework.checker.nullness.qual.*; + +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker") +interface Game { + + @org.checkerframework.dataflow.qual.SideEffectFree + void newGame(); +} + +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker") +class // package-private +GameImpl implements // package-private +Game { + + private MoveValidator moveValidator; + + @org.checkerframework.dataflow.qual.Impure + public GameImpl(MoveValidator mValidator) { + mValidator.setGame(this); + moveValidator = mValidator; + } + + @org.checkerframework.dataflow.qual.SideEffectFree + public GameImpl() { + } + + @org.checkerframework.dataflow.qual.SideEffectFree + public void newGame( // package-private + GameImpl this) { + // Implementation of starting a new game + } +} + +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker") +interface MoveValidator { + + @org.checkerframework.dataflow.qual.Impure + void setGame( MoveValidator this, Game game); +} + +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker") +class // package-private +PlayerDependentMoveValidator implements // package-private +MoveValidator { + + private Game game; + + private MoveValidator blackMoveValidator = new SimpleMoveValidator(); + + @org.checkerframework.dataflow.qual.Impure + public void setGame( // package-private + PlayerDependentMoveValidator this, Game game) { + this.game = game; + } + + @org.checkerframework.dataflow.qual.SideEffectFree + public PlayerDependentMoveValidator() { + } + + @org.checkerframework.dataflow.qual.Impure + public PlayerDependentMoveValidator( Game game) { + this.setGame(game); + blackMoveValidator.setGame(game); + } +} + +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker") +class // package-private +SimpleMoveValidator implements // package-private +MoveValidator { + + private Game game; + + @org.checkerframework.dataflow.qual.Impure + public void setGame( // package-private + SimpleMoveValidator this, Game game) { + this.game = game; + } + + @org.checkerframework.dataflow.qual.SideEffectFree + public SimpleMoveValidator() { + } + + @org.checkerframework.dataflow.qual.Pure + public MoveValidator createMoveValidator() { + return new PlayerDependentMoveValidator(game); + } + public void test(){ + PlayerDependentMoveValidator g1 = + new PlayerDependentMoveValidator(game); + this.game = g1.game; + } +} diff --git a/checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.NullnessChecker.ajava b/checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.NullnessChecker.ajava new file mode 100644 index 000000000000..e5ea01792230 --- /dev/null +++ b/checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.NullnessChecker.ajava @@ -0,0 +1,101 @@ +import org.checkerframework.checker.initialization.qual.*; +import org.checkerframework.checker.nullness.qual.*; + +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker") +interface Game { + + @org.checkerframework.dataflow.qual.SideEffectFree + void newGame(); +} + +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker") +class // package-private +GameImpl implements // package-private +Game { + + private @org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.MonotonicNonNull MoveValidator moveValidator; + + @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.moveValidator" }) + @org.checkerframework.dataflow.qual.Impure + public GameImpl(MoveValidator mValidator) { + mValidator.setGame(this); + moveValidator = mValidator; + } + + @org.checkerframework.dataflow.qual.SideEffectFree + public GameImpl() { + } + + @org.checkerframework.framework.qual.EnsuresQualifier(expression = { "this.moveValidator" }, qualifier = org.checkerframework.checker.nullness.qual.Nullable.class) + @org.checkerframework.dataflow.qual.SideEffectFree + public void newGame(@org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull // package-private + GameImpl this) { + // Implementation of starting a new game + } +} + +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker") +interface MoveValidator { + + @org.checkerframework.dataflow.qual.Impure + void setGame(@org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.Nullable Game game); +} + +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker") +class // package-private +PlayerDependentMoveValidator implements // package-private +MoveValidator { + + private @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.Nullable Game game; + + private @org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull MoveValidator blackMoveValidator = new SimpleMoveValidator(); + + @org.checkerframework.framework.qual.EnsuresQualifier(expression = { "this.game" }, qualifier = org.checkerframework.checker.nullness.qual.Nullable.class) + @org.checkerframework.dataflow.qual.Impure + public void setGame(@org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull // package-private + PlayerDependentMoveValidator this, @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.Nullable Game game) { + this.game = game; + } + + @org.checkerframework.dataflow.qual.SideEffectFree + public PlayerDependentMoveValidator() { + } + + @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "#1" }) + @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.game" }) + @org.checkerframework.dataflow.qual.Impure + public PlayerDependentMoveValidator(@org.checkerframework.checker.initialization.qual.UnknownInitialization(java.lang.Object.class) @org.checkerframework.checker.nullness.qual.Nullable Game game) { + this.setGame(game); + blackMoveValidator.setGame(game); + } +} + +@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker") +class // package-private +SimpleMoveValidator implements // package-private +MoveValidator { + + private @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.MonotonicNonNull Game game; + + @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.game" }) + @org.checkerframework.dataflow.qual.Impure + public void setGame(@org.checkerframework.checker.initialization.qual.Initialized @org.checkerframework.checker.nullness.qual.NonNull // package-private + SimpleMoveValidator this, @org.checkerframework.checker.initialization.qual.UnknownInitialization(GameImpl.class) @org.checkerframework.checker.nullness.qual.NonNull Game game) { + this.game = game; + } + + @org.checkerframework.dataflow.qual.SideEffectFree + public SimpleMoveValidator() { + } + + @org.checkerframework.checker.nullness.qual.EnsuresNonNull({ "this.game" }) + @org.checkerframework.dataflow.qual.Pure + public @org.checkerframework.checker.initialization.qual.UnderInitialization(PlayerDependentMoveValidator.class) @org.checkerframework.checker.nullness.qual.NonNull MoveValidator createMoveValidator() { + return new PlayerDependentMoveValidator(game); + } + public void test(){ + PlayerDependentMoveValidator g1 = + new PlayerDependentMoveValidator(game); + this.game = g1.game; + } +} diff --git a/checker/tests/ainfer-nullness/non-annotated/Game.java b/checker/tests/ainfer-nullness/non-annotated/Game.java new file mode 100644 index 000000000000..99272777446b --- /dev/null +++ b/checker/tests/ainfer-nullness/non-annotated/Game.java @@ -0,0 +1,73 @@ +import org.checkerframework.checker.initialization.qual.*; +import org.checkerframework.checker.nullness.qual.*; + +interface Game { + void newGame(); +} + +class GameImpl implements Game { // package-private + private MoveValidator moveValidator; + + public GameImpl(MoveValidator mValidator) { + mValidator.setGame(this); + moveValidator = mValidator; + } + + public GameImpl() {} + + @Override + public void newGame() { + // Implementation of starting a new game + } +} + +interface MoveValidator { + void setGame(Game game); +} + +class PlayerDependentMoveValidator implements MoveValidator { // package-private + public Game game; + private MoveValidator blackMoveValidator = new SimpleMoveValidator(); + + @SuppressWarnings({"override.param", "contracts.postcondition"}) + @Override + public void setGame(Game game) { + this.game = game; + } + + public PlayerDependentMoveValidator() {} + + @SuppressWarnings({"contracts.postcondition", "argument", "method.invocation"}) + public PlayerDependentMoveValidator(Game game) { + this.setGame(game); + blackMoveValidator.setGame(game); + } +} + +class SimpleMoveValidator implements MoveValidator { // package-private + private Game game; + + @SuppressWarnings({"override.param", "contracts.postcondition"}) + @Override + public void setGame(Game game) { + this.game = game; + } + + public SimpleMoveValidator() {} + + @SuppressWarnings({ + "purity.not.deterministic.object.creation", + "purity" + ".not.sideeffectfree.call", + "contracts.postcondition", + "return" + }) + public MoveValidator createMoveValidator() { + return new PlayerDependentMoveValidator(game); + } + + public void test() { + PlayerDependentMoveValidator g1 = new PlayerDependentMoveValidator(game); + // :: warning: (assignment) + this.game = g1.game; + } +} diff --git a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java index 1d65dc9d1c81..e19422d3bfff 100644 --- a/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java +++ b/framework/src/main/java/org/checkerframework/common/wholeprograminference/WholeProgramInferenceImplementation.java @@ -1001,9 +1001,6 @@ protected void updateAnnotationSet( return; } - // Update the right-hand side (rhs) annotations if necessary before updating the annotation set - atypeFactory.wpiAdjustAnnotationsBeforeUpdate(rhsATM); - AnnotatedTypeMirror atmFromStorage = storage.atmFromStorageLocation(rhsATM.getUnderlyingType(), annotationsToUpdate); updateAtmWithLub(rhsATM, atmFromStorage); diff --git a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java index 8b1f86fc3159..84c918264499 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/AnnotatedTypeFactory.java @@ -5523,15 +5523,6 @@ public boolean wpiShouldInferTypesForReceivers() { return true; } - /** - * Changes the type of {@code rhsATM} when being assigned to anything, for use by whole-program - * inference. The default implementation does nothing. - * - * @param rhsATM the type of the rhs of the pseudo-assignment, which is side-effected by this - * method - */ - public void wpiAdjustAnnotationsBeforeUpdate(AnnotatedTypeMirror rhsATM) {} - /** * Side-effects the method or constructor annotations to make any desired changes before writing * to an annotation file. From 882627552db074a69a3a514679a318ce85786ae5 Mon Sep 17 00:00:00 2001 From: Erfan Arvan Date: Sun, 7 Jul 2024 00:20:36 -0400 Subject: [PATCH 21/33] Removed unnecessary comments --- checker/tests/ainfer-nullness/non-annotated/Game.java | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/checker/tests/ainfer-nullness/non-annotated/Game.java b/checker/tests/ainfer-nullness/non-annotated/Game.java index 99272777446b..3587412d8dce 100644 --- a/checker/tests/ainfer-nullness/non-annotated/Game.java +++ b/checker/tests/ainfer-nullness/non-annotated/Game.java @@ -5,7 +5,7 @@ interface Game { void newGame(); } -class GameImpl implements Game { // package-private +class GameImpl implements Game { private MoveValidator moveValidator; public GameImpl(MoveValidator mValidator) { @@ -17,7 +17,6 @@ public GameImpl() {} @Override public void newGame() { - // Implementation of starting a new game } } @@ -25,7 +24,7 @@ interface MoveValidator { void setGame(Game game); } -class PlayerDependentMoveValidator implements MoveValidator { // package-private +class PlayerDependentMoveValidator implements MoveValidator { public Game game; private MoveValidator blackMoveValidator = new SimpleMoveValidator(); @@ -44,7 +43,7 @@ public PlayerDependentMoveValidator(Game game) { } } -class SimpleMoveValidator implements MoveValidator { // package-private +class SimpleMoveValidator implements MoveValidator { private Game game; @SuppressWarnings({"override.param", "contracts.postcondition"}) From eb798556222cc2b218c301e7fafc81a26d406646 Mon Sep 17 00:00:00 2001 From: Erfan Arvan Date: Sun, 7 Jul 2024 01:05:48 -0400 Subject: [PATCH 22/33] Removed the imports from the test case --- ...checkerframework.checker.nullness.KeyForSubchecker.ajava | 3 --- ....checkerframework.checker.nullness.NullnessChecker.ajava | 3 --- checker/tests/ainfer-nullness/non-annotated/Game.java | 6 +----- 3 files changed, 1 insertion(+), 11 deletions(-) diff --git a/checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.KeyForSubchecker.ajava b/checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.KeyForSubchecker.ajava index 789d78763eeb..1641b30ad5a6 100644 --- a/checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.KeyForSubchecker.ajava +++ b/checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.KeyForSubchecker.ajava @@ -1,6 +1,3 @@ -import org.checkerframework.checker.initialization.qual.*; -import org.checkerframework.checker.nullness.qual.*; - @org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.KeyForSubchecker") interface Game { diff --git a/checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.NullnessChecker.ajava b/checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.NullnessChecker.ajava index e5ea01792230..82c1429be032 100644 --- a/checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.NullnessChecker.ajava +++ b/checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.NullnessChecker.ajava @@ -1,6 +1,3 @@ -import org.checkerframework.checker.initialization.qual.*; -import org.checkerframework.checker.nullness.qual.*; - @org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.nullness.NullnessChecker") interface Game { diff --git a/checker/tests/ainfer-nullness/non-annotated/Game.java b/checker/tests/ainfer-nullness/non-annotated/Game.java index 3587412d8dce..dba5956754b5 100644 --- a/checker/tests/ainfer-nullness/non-annotated/Game.java +++ b/checker/tests/ainfer-nullness/non-annotated/Game.java @@ -1,6 +1,3 @@ -import org.checkerframework.checker.initialization.qual.*; -import org.checkerframework.checker.nullness.qual.*; - interface Game { void newGame(); } @@ -16,8 +13,7 @@ public GameImpl(MoveValidator mValidator) { public GameImpl() {} @Override - public void newGame() { - } + public void newGame() {} } interface MoveValidator { From 6ae7fbad6689a43a218af7f1b66e30d9920554b4 Mon Sep 17 00:00:00 2001 From: Erfan Arvan Date: Sun, 7 Jul 2024 01:09:17 -0400 Subject: [PATCH 23/33] Changed the name of the test case --- ...-org.checkerframework.checker.nullness.KeyForSubchecker.ajava} | 0 ...t-org.checkerframework.checker.nullness.NullnessChecker.ajava} | 0 .../{Game.java => WPIUnknownInitializationLoopTest.java} | 0 3 files changed, 0 insertions(+), 0 deletions(-) rename checker/tests/ainfer-nullness/input-annotation-files/{Game-org.checkerframework.checker.nullness.KeyForSubchecker.ajava => WPIUnknownInitializationLoopTest-org.checkerframework.checker.nullness.KeyForSubchecker.ajava} (100%) rename checker/tests/ainfer-nullness/input-annotation-files/{Game-org.checkerframework.checker.nullness.NullnessChecker.ajava => WPIUnknownInitializationLoopTest-org.checkerframework.checker.nullness.NullnessChecker.ajava} (100%) rename checker/tests/ainfer-nullness/non-annotated/{Game.java => WPIUnknownInitializationLoopTest.java} (100%) diff --git a/checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.KeyForSubchecker.ajava b/checker/tests/ainfer-nullness/input-annotation-files/WPIUnknownInitializationLoopTest-org.checkerframework.checker.nullness.KeyForSubchecker.ajava similarity index 100% rename from checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.KeyForSubchecker.ajava rename to checker/tests/ainfer-nullness/input-annotation-files/WPIUnknownInitializationLoopTest-org.checkerframework.checker.nullness.KeyForSubchecker.ajava diff --git a/checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.NullnessChecker.ajava b/checker/tests/ainfer-nullness/input-annotation-files/WPIUnknownInitializationLoopTest-org.checkerframework.checker.nullness.NullnessChecker.ajava similarity index 100% rename from checker/tests/ainfer-nullness/input-annotation-files/Game-org.checkerframework.checker.nullness.NullnessChecker.ajava rename to checker/tests/ainfer-nullness/input-annotation-files/WPIUnknownInitializationLoopTest-org.checkerframework.checker.nullness.NullnessChecker.ajava diff --git a/checker/tests/ainfer-nullness/non-annotated/Game.java b/checker/tests/ainfer-nullness/non-annotated/WPIUnknownInitializationLoopTest.java similarity index 100% rename from checker/tests/ainfer-nullness/non-annotated/Game.java rename to checker/tests/ainfer-nullness/non-annotated/WPIUnknownInitializationLoopTest.java From f0578946abbecbe8667fb6947af633ed66a6bd0f Mon Sep 17 00:00:00 2001 From: Erfan Arvan Date: Tue, 9 Jul 2024 22:52:54 -0400 Subject: [PATCH 24/33] Update checker build.gradle to fix ainferNullnessGenerateJaifs task issue and add comments to the test file --- checker/build.gradle | 4 +++- .../non-annotated/WPIUnknownInitializationLoopTest.java | 7 +++++++ 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/checker/build.gradle b/checker/build.gradle index 1448fde7ffb9..85c79671364f 100644 --- a/checker/build.gradle +++ b/checker/build.gradle @@ -813,6 +813,9 @@ task ainferNullnessGenerateJaifs(type: Test) { delete('tests/ainfer-nullness/annotated/TwoCtorGenericAbstract.java') delete('tests/ainfer-nullness/annotated/TypeVarReturnAnnotated.java') + //This test shouldn't be expected to work without the input .ajava file. + delete('tests/ainfer-nullness/annotated/WPIUnknownInitializationLoopTest.java') + // Inserting annotations from .jaif files in-place. String jaifsDir = 'tests/ainfer-nullness/inference-output'; List jaifs = fileTree(jaifsDir).matching { @@ -1079,4 +1082,3 @@ publishing { signing { sign publishing.publications.checker } - diff --git a/checker/tests/ainfer-nullness/non-annotated/WPIUnknownInitializationLoopTest.java b/checker/tests/ainfer-nullness/non-annotated/WPIUnknownInitializationLoopTest.java index dba5956754b5..81ae9b927098 100644 --- a/checker/tests/ainfer-nullness/non-annotated/WPIUnknownInitializationLoopTest.java +++ b/checker/tests/ainfer-nullness/non-annotated/WPIUnknownInitializationLoopTest.java @@ -1,3 +1,10 @@ +// WPI gets stuck in a loop for codes like this because it +// does not currently consider the facts related to the absence of some initializations +// when there are multiple constructors for a class. A solution for this problem makes the +// ainfernullness test on this code pass. The current solution changes the UnknownInitialization +// annotations with all arguments for a Nullable or MonotonicNonNull object to +// UnknownInitialization(java.lang.Object.class). + interface Game { void newGame(); } From 1a32487636081c34a1cb1493f41ff9a024b3e99d Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sun, 7 Jul 2024 10:21:56 -0700 Subject: [PATCH 25/33] Rename an instance of `VarArgsTest` --- .../tests/all-systems/java8/memberref/VarArgs.java | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/framework/tests/all-systems/java8/memberref/VarArgs.java b/framework/tests/all-systems/java8/memberref/VarArgs.java index 9ecc432b38fe..a8d88392a86e 100644 --- a/framework/tests/all-systems/java8/memberref/VarArgs.java +++ b/framework/tests/all-systems/java8/memberref/VarArgs.java @@ -6,17 +6,17 @@ interface ArrayFunc { void take(String[] in); } -class VarArgsTest { +class MemberRefVarArgsTest { static void myMethod(String... in) {} static void myMethodArray(String[] in) {} - VarArgsFunc v1 = VarArgsTest::myMethod; - VarArgsFunc v2 = VarArgsTest::myMethodArray; + VarArgsFunc v1 = MemberRefVarArgsTest::myMethod; + VarArgsFunc v2 = MemberRefVarArgsTest::myMethodArray; - ArrayFunc v3 = VarArgsTest::myMethod; - ArrayFunc v4 = VarArgsTest::myMethodArray; + ArrayFunc v3 = MemberRefVarArgsTest::myMethod; + ArrayFunc v4 = MemberRefVarArgsTest::myMethodArray; } interface RegularFunc { From 90129a30df1768c1e398ecab3f7d9e9dca91bfa5 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sun, 7 Jul 2024 15:23:21 -0700 Subject: [PATCH 26/33] Give `DefaultQualifier` runtime retention --- .../org/checkerframework/framework/qual/DefaultQualifier.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/checker-qual/src/main/java/org/checkerframework/framework/qual/DefaultQualifier.java b/checker-qual/src/main/java/org/checkerframework/framework/qual/DefaultQualifier.java index 7409d9141440..ef783ca9a850 100644 --- a/checker-qual/src/main/java/org/checkerframework/framework/qual/DefaultQualifier.java +++ b/checker-qual/src/main/java/org/checkerframework/framework/qual/DefaultQualifier.java @@ -34,7 +34,7 @@ * @checker_framework.manual #defaults Default qualifier for unannotated types */ @Documented -@Retention(RetentionPolicy.SOURCE) +@Retention(RetentionPolicy.RUNTIME) @Target({ ElementType.PACKAGE, ElementType.TYPE, From cf451ba3bfa04b2fc43f36b64d86c5d0e3b09266 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Sun, 7 Jul 2024 18:53:53 -0700 Subject: [PATCH 27/33] Minor changes related to Non-Empty Checker --- .../checker/optional/OptionalTransfer.java | 15 +++++++-------- docs/manual/non-empty-checker.tex | 6 +++--- 2 files changed, 10 insertions(+), 11 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java b/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java index de521118adc2..a3d266c7f927 100644 --- a/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java @@ -22,13 +22,15 @@ import org.checkerframework.framework.flow.CFStore; import org.checkerframework.framework.flow.CFTransfer; import org.checkerframework.framework.flow.CFValue; -import org.checkerframework.framework.type.AnnotatedTypeFactory; import org.checkerframework.javacutil.AnnotationBuilder; import org.checkerframework.javacutil.TreeUtils; /** The transfer function for the Optional Checker. */ public class OptionalTransfer extends CFTransfer { + /** The {@link OptionalAnnotatedTypeFactory} instance for this transfer class. */ + private final OptionalAnnotatedTypeFactory optionalTypeFactory; + /** The @{@link Present} annotation. */ private final AnnotationMirror PRESENT; @@ -38,9 +40,6 @@ public class OptionalTransfer extends CFTransfer { /** The element for java.util.Optional.ifPresentOrElse(), or null. */ private final @Nullable ExecutableElement optionalIfPresentOrElse; - /** The type factory associated with this transfer function. */ - private final AnnotatedTypeFactory atypeFactory; - /** * Create an OptionalTransfer. * @@ -48,10 +47,10 @@ public class OptionalTransfer extends CFTransfer { */ public OptionalTransfer(CFAbstractAnalysis analysis) { super(analysis); - atypeFactory = analysis.getTypeFactory(); - Elements elements = atypeFactory.getElementUtils(); + optionalTypeFactory = (OptionalAnnotatedTypeFactory) analysis.getTypeFactory(); + Elements elements = optionalTypeFactory.getElementUtils(); PRESENT = AnnotationBuilder.fromClass(elements, Present.class); - ProcessingEnvironment env = atypeFactory.getProcessingEnv(); + ProcessingEnvironment env = optionalTypeFactory.getProcessingEnv(); optionalIfPresent = TreeUtils.getMethod("java.util.Optional", "ifPresent", 1, env); optionalIfPresentOrElse = TreeUtils.getMethodOrNull("java.util.Optional", "ifPresentOrElse", 2, env); @@ -70,7 +69,7 @@ public CFStore initialStore(UnderlyingAST underlyingAST, List LambdaExpressionTree lambdaTree = cfgLambda.getLambdaTree(); List lambdaParams = lambdaTree.getParameters(); if (lambdaParams.size() == 1) { - TreePath lambdaPath = atypeFactory.getPath(lambdaTree); + TreePath lambdaPath = optionalTypeFactory.getPath(lambdaTree); Tree lambdaParent = lambdaPath.getParentPath().getLeaf(); if (lambdaParent.getKind() == Tree.Kind.METHOD_INVOCATION) { MethodInvocationTree invok = (MethodInvocationTree) lambdaParent; diff --git a/docs/manual/non-empty-checker.tex b/docs/manual/non-empty-checker.tex index f7ff42bb4e26..72aa041a35fd 100644 --- a/docs/manual/non-empty-checker.tex +++ b/docs/manual/non-empty-checker.tex @@ -1,8 +1,8 @@ \htmlhr \chapterAndLabel{Non-Empty Checker for container classes}{non-empty-checker} -The Non-Empty Checker tracks whether a container may be empty. -It works on containers such as +The Non-Empty Checker tracks whether a container is possibly-empty or is +definitely non-empty. It works on containers such as \s, \s, \s, and \s, but not \s. If the Non-Empty Checker issues no warnings, then your program does not @@ -145,7 +145,7 @@ by the Non-Empty Checker: \begin{Verbatim} -// This method might return an empty list, depending on the argument +// This method might return an empty list, depending on the argument. List getRegionIds(String region) { ... } void parseRegions() { From 8eafe7d7470d03f32027ba60532fe5219b34074f Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Mon, 8 Jul 2024 08:21:20 -0700 Subject: [PATCH 28/33] Use `filePermissions` instead of deprecated `fileMode` (#6693) --- checker-qual-android/build.gradle | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/checker-qual-android/build.gradle b/checker-qual-android/build.gradle index 816f06e18b1e..ed9b8671ed29 100644 --- a/checker-qual-android/build.gradle +++ b/checker-qual-android/build.gradle @@ -19,7 +19,19 @@ task copySources(type: Copy) { into file(layout.buildDirectory.dir("generated/sources/main/java")) - fileMode(0555) + filePermissions { + user { + read = true + write = true + execute = true + } + group { + read = true + write = true + execute = true + } + other.read = true + } } sourceSets { From 1d5fb60cc7ff885ff1eb63473a1c8c6f7b899bac Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Mon, 8 Jul 2024 08:32:45 -0700 Subject: [PATCH 29/33] Disambiguate owners of fields in output (#6699) --- .../dataflow/cfg/node/ExplicitThisNode.java | 6 +++++- .../dataflow/cfg/node/FieldAccessNode.java | 7 ++++++- .../dataflow/cfg/node/ImplicitThisNode.java | 6 +++++- .../org/checkerframework/dataflow/cfg/node/Node.java | 6 ++++++ .../checkerframework/dataflow/cfg/node/SuperNode.java | 9 ++++++++- .../dataflow/expression/FieldAccess.java | 7 +++++-- .../dataflow/expression/ThisReference.java | 7 ++++++- .../expression/ViewpointAdaptJavaExpression.java | 2 +- .../java/org/checkerframework/javacutil/TreeUtils.java | 3 +++ 9 files changed, 45 insertions(+), 8 deletions(-) diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ExplicitThisNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ExplicitThisNode.java index dba86498d56d..4d3636a3db90 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ExplicitThisNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ExplicitThisNode.java @@ -32,6 +32,10 @@ public R accept(NodeVisitor visitor, P p) { @Override public String toString() { - return "this"; + if (Node.disambiguateOwner) { + return "this{owner=" + type + "}"; + } else { + return "this"; + } } } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java index 7ad59de9eefa..a2e112cf07a6 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/FieldAccessNode.java @@ -3,6 +3,7 @@ import com.sun.source.tree.IdentifierTree; import com.sun.source.tree.MemberSelectTree; import com.sun.source.tree.Tree; +import com.sun.tools.javac.code.Symbol; import java.util.Collection; import java.util.Collections; import java.util.Objects; @@ -91,7 +92,11 @@ public R accept(NodeVisitor visitor, P p) { @Override public String toString() { - return getReceiver() + "." + field; + if (Node.disambiguateOwner) { + return getReceiver() + "." + field + "{owner=" + ((Symbol) element).owner + "}"; + } else { + return getReceiver() + "." + field; + } } /** diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ImplicitThisNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ImplicitThisNode.java index 751b50a8126c..dafb4b1b85c0 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ImplicitThisNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ImplicitThisNode.java @@ -26,6 +26,10 @@ public R accept(NodeVisitor visitor, P p) { // used in an inner class context. @Override public String toString() { - return "(this)"; + if (Node.disambiguateOwner) { + return "(this{owner=" + type + "})"; + } else { + return "(this)"; + } } } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/Node.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/Node.java index d249fa593442..dfd2a92d58d6 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/Node.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/Node.java @@ -35,6 +35,12 @@ */ public abstract class Node implements UniqueId { + /** + * If true, print the owner of each field and {@code this}, to disambiguate shadowing. This field + * is intended for debugging. + */ + public static final boolean disambiguateOwner = false; + /** * The basic block this node belongs to. If null, this object represents a method formal * parameter. diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/SuperNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/SuperNode.java index c1fbf5722867..8dcf7ec87c30 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/SuperNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/SuperNode.java @@ -13,6 +13,9 @@ * 

      *   super
  *
    + * + * Its {@link #type} field is the type of the class in which "super" appears, not the type + * to which the "super" identifier resolves. */ public class SuperNode extends Node { @@ -36,7 +39,11 @@ public R accept(NodeVisitor visitor, P p) { @Override public String toString() { - return "super"; + if (Node.disambiguateOwner) { + return "super{owner=" + type + "}"; + } else { + return "super"; + } } @Override diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/expression/FieldAccess.java b/dataflow/src/main/java/org/checkerframework/dataflow/expression/FieldAccess.java index 92908cfe1515..b0289d761c25 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/expression/FieldAccess.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/expression/FieldAccess.java @@ -7,6 +7,7 @@ import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.dataflow.analysis.Store; import org.checkerframework.dataflow.cfg.node.FieldAccessNode; +import org.checkerframework.dataflow.cfg.node.Node; import org.checkerframework.javacutil.AnnotationProvider; import org.checkerframework.javacutil.BugInCF; import org.checkerframework.javacutil.ElementUtils; @@ -139,8 +140,10 @@ public boolean containsModifiableAliasOf(Store store, JavaExpression other) { @Override public String toString() { - if (receiver instanceof ClassName) { - return receiver.getType() + "." + field; + String receiverString = + (receiver instanceof ClassName) ? receiver.getType().toString() : receiver.toString(); + if (Node.disambiguateOwner) { + return receiverString + "." + field + "{owner=" + ((Symbol) field).owner + "}"; } else { return receiver + "." + field; } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/expression/ThisReference.java b/dataflow/src/main/java/org/checkerframework/dataflow/expression/ThisReference.java index 6339e5b817eb..ef7ff28b3ab8 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/expression/ThisReference.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/expression/ThisReference.java @@ -3,6 +3,7 @@ import javax.lang.model.type.TypeMirror; import org.checkerframework.checker.nullness.qual.Nullable; import org.checkerframework.dataflow.analysis.Store; +import org.checkerframework.dataflow.cfg.node.Node; import org.checkerframework.javacutil.AnnotationProvider; import org.checkerframework.javacutil.TypesUtils; @@ -29,7 +30,11 @@ public int hashCode() { @Override public String toString() { - return "this"; + if (Node.disambiguateOwner) { + return "this{" + type + "}"; + } else { + return "this"; + } } @SuppressWarnings("unchecked") // generic cast diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/expression/ViewpointAdaptJavaExpression.java b/dataflow/src/main/java/org/checkerframework/dataflow/expression/ViewpointAdaptJavaExpression.java index 422a70ea8470..4ef93e6fbd41 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/expression/ViewpointAdaptJavaExpression.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/expression/ViewpointAdaptJavaExpression.java @@ -62,7 +62,7 @@ public static JavaExpression viewpointAdapt( /** List of arguments used to replace occurrences {@link FormalParameter}s. */ private final @Nullable List args; - /** The expression to replace occurrences of {@link ThisReference}s. */ + /** The expression to replace occurrences of {@link ThisReference}. */ private final @Nullable JavaExpression thisReference; // Instance methods diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java index bf246a66b649..4cebc77f38b1 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java @@ -1844,6 +1844,9 @@ public static boolean isLocalVariable(Tree tree) { * Returns the type as a TypeMirror of {@code tree}. To obtain {@code tree}'s AnnotatedTypeMirror, * call {@code AnnotatedTypeFactory.getAnnotatedType()}. * + *

    Note that for the expression "super", this method returns the type of "this", not "this"'s + * superclass. + * * @return the type as a TypeMirror of {@code tree} */ public static TypeMirror typeOf(Tree tree) { From 217ba505fc5a85afdc914a01f96e640c3ef886c8 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Mon, 8 Jul 2024 08:33:40 -0700 Subject: [PATCH 30/33] Comment changes (#6700) --- .../dataflow/analysis/AbstractAnalysis.java | 5 ++++- .../dataflow/analysis/TransferInput.java | 14 +++++++------- .../type/GenericAnnotatedTypeFactory.java | 1 + 3 files changed, 12 insertions(+), 8 deletions(-) diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java index 80e3372143be..2711c3b6e6ab 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/AbstractAnalysis.java @@ -468,7 +468,10 @@ protected boolean updateNodeValues(Node node, TransferResult transferResul * @param b the block to add to {@link #worklist} */ protected void addToWorklist(Block b) { - // TODO: use a more efficient way to check if b is already present + // TODO: This costs linear (!) time. Use a more efficient way to check if b is already present. + // Two possibilities: + // * add unconditionally, and detect duplicates when removing from the queue. + // * maintain a HashSet of the elements that are already in the queue. if (!worklist.contains(b)) { worklist.add(b); } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/TransferInput.java b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/TransferInput.java index ced4f8be5704..b84bfc27da84 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/analysis/TransferInput.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/analysis/TransferInput.java @@ -11,10 +11,10 @@ /** * {@code TransferInput} is used as the input type of the individual transfer functions of a {@link * ForwardTransferFunction} or a {@link BackwardTransferFunction}. It also contains a reference to - * the node for which the transfer function will be applied. + * the node to which the transfer function will be applied. * *

    A {@code TransferInput} contains one or two stores. If two stores are present, one belongs to - * 'then', and the other to 'else'. + * "then", and the other to "else". * * @param type of the abstract value that is tracked * @param the store type used in the analysis @@ -36,12 +36,12 @@ public class TransferInput, S extends Store> imple protected final @Nullable S store; /** - * The 'then' result store (or {@code null} if none is present). See invariant at {@link #store}. + * The "then" result store (or {@code null} if none is present). See invariant at {@link #store}. */ protected final @Nullable S thenStore; /** - * The 'else' result store (or {@code null} if none is present). See invariant at {@link #store}. + * The "else" result store (or {@code null} if none is present). See invariant at {@link #store}. */ protected final @Nullable S elseStore; @@ -64,8 +64,8 @@ public long getUid(@UnknownInitialization TransferInput this) { * * @param node the corresponding node * @param store the regular result store, or {@code null} if none is present - * @param thenStore the 'then' result store, or {@code null} if none is present - * @param elseStore the 'else' result store, or {@code null} if none is present + * @param thenStore the "then" result store, or {@code null} if none is present + * @param elseStore the "else" result store, or {@code null} if none is present * @param analysis analysis the corresponding analysis class to get intermediate flow results */ private TransferInput( @@ -166,7 +166,7 @@ protected TransferInput(TransferInput from) { } /** - * Returns the abstract value of node {@code n}, which is required to be a 'sub-node' (that is, a + * Returns the abstract value of node {@code n}, which is required to be a "sub-node" (that is, a * direct or indirect child) of the node this transfer input is associated with. Furthermore, * {@code n} cannot be a l-value node. Returns {@code null} if no value is available. * 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 d9cb6cf1827f..7e95cd9efa2f 100644 --- a/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java +++ b/framework/src/main/java/org/checkerframework/framework/type/GenericAnnotatedTypeFactory.java @@ -2439,6 +2439,7 @@ protected void addAnnotationsFromDefaultForType( @FormatMethod private static void log(String format, Object... args) { if (debug) { + System.out.flush(); SystemPlume.sleep(1); // logging can interleave with typechecker output System.out.printf(format, args); } From 8aafb3b092ab92fae807b1ab7d58cbe819ac32d2 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 3 Mar 2026 09:44:40 -0800 Subject: [PATCH 31/33] OptionalAnnotatedTypeFactory => OptionalImplAnnotatedTypeFactory --- .../checker/optional/OptionalImplVisitor.java | 2 +- .../checkerframework/checker/optional/OptionalTransfer.java | 6 +++--- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/optional/OptionalImplVisitor.java b/checker/src/main/java/org/checkerframework/checker/optional/OptionalImplVisitor.java index 3862a33b9342..47caf36ee578 100644 --- a/checker/src/main/java/org/checkerframework/checker/optional/OptionalImplVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/optional/OptionalImplVisitor.java @@ -65,7 +65,7 @@ * @checker_framework.manual #optional-checker Optional Checker */ public class OptionalImplVisitor - extends BaseTypeVisitor { + extends BaseTypeVisitor { /** The Collection type. */ private final TypeMirror collectionType; diff --git a/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java b/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java index a3d266c7f927..cf93f36e4470 100644 --- a/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java @@ -28,8 +28,8 @@ /** The transfer function for the Optional Checker. */ public class OptionalTransfer extends CFTransfer { - /** The {@link OptionalAnnotatedTypeFactory} instance for this transfer class. */ - private final OptionalAnnotatedTypeFactory optionalTypeFactory; + /** The {@link OptionalImplAnnotatedTypeFactory} instance for this transfer class. */ + private final OptionalImplAnnotatedTypeFactory optionalTypeFactory; /** The @{@link Present} annotation. */ private final AnnotationMirror PRESENT; @@ -47,7 +47,7 @@ public class OptionalTransfer extends CFTransfer { */ public OptionalTransfer(CFAbstractAnalysis analysis) { super(analysis); - optionalTypeFactory = (OptionalAnnotatedTypeFactory) analysis.getTypeFactory(); + optionalTypeFactory = (OptionalImplAnnotatedTypeFactory) analysis.getTypeFactory(); Elements elements = optionalTypeFactory.getElementUtils(); PRESENT = AnnotationBuilder.fromClass(elements, Present.class); ProcessingEnvironment env = optionalTypeFactory.getProcessingEnv(); From 7b2c05f0a436e4a01f51bd334ea418d8c064c8e7 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Tue, 3 Mar 2026 09:49:09 -0800 Subject: [PATCH 32/33] Use --- .../org/checkerframework/checker/optional/OptionalTransfer.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java b/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java index cf93f36e4470..adaaacfde10f 100644 --- a/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java @@ -71,7 +71,7 @@ public CFStore initialStore(UnderlyingAST underlyingAST, List if (lambdaParams.size() == 1) { TreePath lambdaPath = optionalTypeFactory.getPath(lambdaTree); Tree lambdaParent = lambdaPath.getParentPath().getLeaf(); - if (lambdaParent.getKind() == Tree.Kind.METHOD_INVOCATION) { + if (lambdaParent.getKind() instanceof MethodInvocationTree) { MethodInvocationTree invok = (MethodInvocationTree) lambdaParent; ExecutableElement methodElt = TreeUtils.elementFromUse(invok); if (methodElt.equals(optionalIfPresent) || methodElt.equals(optionalIfPresentOrElse)) { From a5eb537857b88ddd6f79d54ad9df14e6f8f24778 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Wed, 4 Mar 2026 07:15:21 -0800 Subject: [PATCH 33/33] Put error message key in brackets --- .../org/checkerframework/checker/optional/OptionalTransfer.java | 2 +- .../non-annotated/WPIUnknownInitializationLoopTest.java | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java b/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java index adaaacfde10f..60ef360cea82 100644 --- a/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/optional/OptionalTransfer.java @@ -71,7 +71,7 @@ public CFStore initialStore(UnderlyingAST underlyingAST, List if (lambdaParams.size() == 1) { TreePath lambdaPath = optionalTypeFactory.getPath(lambdaTree); Tree lambdaParent = lambdaPath.getParentPath().getLeaf(); - if (lambdaParent.getKind() instanceof MethodInvocationTree) { + if (lambdaParent instanceof MethodInvocationTree) { MethodInvocationTree invok = (MethodInvocationTree) lambdaParent; ExecutableElement methodElt = TreeUtils.elementFromUse(invok); if (methodElt.equals(optionalIfPresent) || methodElt.equals(optionalIfPresentOrElse)) { diff --git a/checker/tests/ainfer-nullness/non-annotated/WPIUnknownInitializationLoopTest.java b/checker/tests/ainfer-nullness/non-annotated/WPIUnknownInitializationLoopTest.java index 81ae9b927098..52ee5d1a6bbf 100644 --- a/checker/tests/ainfer-nullness/non-annotated/WPIUnknownInitializationLoopTest.java +++ b/checker/tests/ainfer-nullness/non-annotated/WPIUnknownInitializationLoopTest.java @@ -69,7 +69,7 @@ public MoveValidator createMoveValidator() { public void test() { PlayerDependentMoveValidator g1 = new PlayerDependentMoveValidator(game); - // :: warning: (assignment) + // :: warning: [assignment] this.game = g1.game; } }