From dc8ee8eb42ca9b9b2e41bc183bd0a036030c439f Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 2 Aug 2023 01:40:47 -0400 Subject: [PATCH 1/9] fix typo --- .../checker/initialization/InitializationTransfer.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationTransfer.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationTransfer.java index f3fd93b79b3..f46ef5eba09 100644 --- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationTransfer.java @@ -168,7 +168,7 @@ public TransferResult visitAssignment(AssignmentNode n, TransferInput Date: Wed, 2 Aug 2023 03:02:28 -0400 Subject: [PATCH 2/9] fix typo --- .../org/checkerframework/framework/flow/CFAbstractTransfer.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java index 99ccb3645f7..13833b8ab0e 100644 --- a/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java +++ b/framework/src/main/java/org/checkerframework/framework/flow/CFAbstractTransfer.java @@ -589,7 +589,7 @@ protected TransferResult createTransferResult(@Nullable V value, TransferI * * @param value the value; possibly null * @param in the TransferResult to copy - * @return the input informatio + * @return the input information */ @SideEffectFree protected TransferResult recreateTransferResult( From c5f519aecda52b1c2371fc34b0a7610ed835e717 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 2 Aug 2023 14:49:53 -0400 Subject: [PATCH 3/9] fix typo --- .../org/checkerframework/dataflow/cfg/node/FieldAccessNode.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 3051ed91755..a56d986e586 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 @@ -36,7 +36,7 @@ public class FieldAccessNode extends Node { * Creates a new FieldAccessNode. * * @param tree the tree from which to create a FieldAccessNode - * @param receiver the receiver for the resuling FieldAccessNode + * @param receiver the receiver for the resulting FieldAccessNode */ public FieldAccessNode(Tree tree, Node receiver) { super(TreeUtils.typeOf(tree)); From a6980cac800cfa4f00b0772a9bceba569b96d68c Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Wed, 2 Aug 2023 18:19:13 -0400 Subject: [PATCH 4/9] fix typo --- .../org/checkerframework/checker/optional/OptionalChecker.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/checker/src/main/java/org/checkerframework/checker/optional/OptionalChecker.java b/checker/src/main/java/org/checkerframework/checker/optional/OptionalChecker.java index f804f943d73..fca4c4b4273 100644 --- a/checker/src/main/java/org/checkerframework/checker/optional/OptionalChecker.java +++ b/checker/src/main/java/org/checkerframework/checker/optional/OptionalChecker.java @@ -10,7 +10,7 @@ * * @checker_framework.manual #optional-checker Optional Checker */ -// TODO: For a call to ofNullable, if the argument has type @NonNull, make the return type have type +// TODO: For a call to of Nullable, if the argument has type @NonNull, make the return type have type // @Present. Make Optional Checker a subchecker of the Nullness Checker. @RelevantJavaTypes(Optional.class) public class OptionalChecker extends BaseTypeChecker {} From b9d3d643538ceb4ce2089eec4fde48b9ca8f8926 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Thu, 3 Aug 2023 21:07:51 -0400 Subject: [PATCH 5/9] test changes --- .../EISOPissue548/ConservativeClassLiteral.java | 15 +++++++++++++++ checker/jtreg/nullness/EISOPissue548/MyEnum.java | 3 +++ .../checker/nullness/NullnessTransfer.java | 9 +++++++++ .../common/basetype/BaseTypeVisitor.java | 14 ++++++++------ 4 files changed, 35 insertions(+), 6 deletions(-) create mode 100644 checker/jtreg/nullness/EISOPissue548/ConservativeClassLiteral.java create mode 100644 checker/jtreg/nullness/EISOPissue548/MyEnum.java diff --git a/checker/jtreg/nullness/EISOPissue548/ConservativeClassLiteral.java b/checker/jtreg/nullness/EISOPissue548/ConservativeClassLiteral.java new file mode 100644 index 00000000000..246648a4e53 --- /dev/null +++ b/checker/jtreg/nullness/EISOPissue548/ConservativeClassLiteral.java @@ -0,0 +1,15 @@ +/* + * @test + * @summary Test class literals in CFGs and their type with conservative nullness. + * + * @compile MyEnum.java + * @compile -processor org.checkerframework.checker.nullness.NullnessChecker -AuseConservativeDefaultsForUncheckedCode=bytecode,-source ConservativeClassLiteral.java + */ + +import java.util.EnumSet; + +class ConservativeClassLiteral { + EnumSet none() { + return EnumSet.noneOf(MyEnum.class); + } +} diff --git a/checker/jtreg/nullness/EISOPissue548/MyEnum.java b/checker/jtreg/nullness/EISOPissue548/MyEnum.java new file mode 100644 index 00000000000..c4b60a93a39 --- /dev/null +++ b/checker/jtreg/nullness/EISOPissue548/MyEnum.java @@ -0,0 +1,3 @@ +enum MyEnum { + VALUE; +} diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java index 5e594dc0cc9..cf292d85a71 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessTransfer.java @@ -10,6 +10,7 @@ import org.checkerframework.checker.nullness.qual.PolyNull; import org.checkerframework.common.basetype.BaseTypeChecker; import org.checkerframework.dataflow.analysis.ConditionalTransferResult; +import org.checkerframework.dataflow.analysis.RegularTransferResult; import org.checkerframework.dataflow.analysis.TransferInput; import org.checkerframework.dataflow.analysis.TransferResult; import org.checkerframework.dataflow.cfg.node.ArrayAccessNode; @@ -351,6 +352,14 @@ public TransferResult visitMethodAccess( @Override public TransferResult visitFieldAccess( FieldAccessNode n, TransferInput p) { + if (n.getFieldName().equals("class")) { + NullnessStore store = p.getRegularStore(); + NullnessValue storeValue = store.getValue(n); + TransferResult result = + new RegularTransferResult(storeValue, store); + makeNonNull(result, n.getReceiver()); + return result; + } TransferResult result = super.visitFieldAccess(n, p); makeNonNull(result, n.getReceiver()); return result; 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 0b1be9798d2..8e8f546776c 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -3103,12 +3103,14 @@ protected void commonAssignmentCheck( Tree valueExpTree, @CompilerMessageKey String errorKey, Object... extraArgs) { - - commonAssignmentCheckStartDiagnostic(varType, valueType, valueExpTree); - - AnnotatedTypeMirror widenedValueType = atypeFactory.getWidenedType(valueType, varType); - boolean success = atypeFactory.getTypeHierarchy().isSubtype(widenedValueType, varType); - + boolean success; + if (valueExpTree.toString().endsWith(".class")) { + success = true; + } else { + commonAssignmentCheckStartDiagnostic(varType, valueType, valueExpTree); + AnnotatedTypeMirror widenedValueType = atypeFactory.getWidenedType(valueType, varType); + success = atypeFactory.getTypeHierarchy().isSubtype(widenedValueType, varType); + } // TODO: integrate with subtype test. if (success) { for (Class mono : From 4b73445c6d0ea38dda4b09c16d4d56af5982da5e Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Fri, 4 Aug 2023 03:02:37 -0400 Subject: [PATCH 6/9] apply spotless --- .../org/checkerframework/common/basetype/BaseTypeVisitor.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 8e8f546776c..b0d72136aae 100644 --- a/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java +++ b/framework/src/main/java/org/checkerframework/common/basetype/BaseTypeVisitor.java @@ -3109,7 +3109,7 @@ protected void commonAssignmentCheck( } else { commonAssignmentCheckStartDiagnostic(varType, valueType, valueExpTree); AnnotatedTypeMirror widenedValueType = atypeFactory.getWidenedType(valueType, varType); - success = atypeFactory.getTypeHierarchy().isSubtype(widenedValueType, varType); + success = atypeFactory.getTypeHierarchy().isSubtype(widenedValueType, varType); } // TODO: integrate with subtype test. if (success) { From 92248dc6bbf986ddd9351aaee157cd7e22cc1834 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Fri, 4 Aug 2023 19:13:29 -0400 Subject: [PATCH 7/9] apply spotless --- .../checkerframework/checker/optional/OptionalChecker.java | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/optional/OptionalChecker.java b/checker/src/main/java/org/checkerframework/checker/optional/OptionalChecker.java index fca4c4b4273..aa78b92148f 100644 --- a/checker/src/main/java/org/checkerframework/checker/optional/OptionalChecker.java +++ b/checker/src/main/java/org/checkerframework/checker/optional/OptionalChecker.java @@ -10,7 +10,7 @@ * * @checker_framework.manual #optional-checker Optional Checker */ -// TODO: For a call to of Nullable, if the argument has type @NonNull, make the return type have type -// @Present. Make Optional Checker a subchecker of the Nullness Checker. +// TODO: For a call to of Nullable, if the argument has type @NonNull, make the return type have +// type @Present. Make Optional Checker a subchecker of the Nullness Checker. @RelevantJavaTypes(Optional.class) public class OptionalChecker extends BaseTypeChecker {} From 00a3855e84a03483fcad4f856a6977a51beda0dc Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 7 Aug 2023 23:02:26 -0400 Subject: [PATCH 8/9] test pipelines --- checker/tests/nullness/Issue3020.java | 1 + 1 file changed, 1 insertion(+) diff --git a/checker/tests/nullness/Issue3020.java b/checker/tests/nullness/Issue3020.java index b8d735d9eba..e98d5a723fc 100644 --- a/checker/tests/nullness/Issue3020.java +++ b/checker/tests/nullness/Issue3020.java @@ -4,6 +4,7 @@ enum Issue3020 { void retrieveConstant() { Class theClass = Issue3020.class; // :: error: (accessing.nullable) + // :: error: (dereference.of.nullable) Object unused = passThrough(theClass.getEnumConstants())[0]; } From 17e79e3234df196cd30187ad4fc92b12d80d7a58 Mon Sep 17 00:00:00 2001 From: Aosen Xiong Date: Mon, 16 Oct 2023 01:18:26 -0400 Subject: [PATCH 9/9] initial commit --- .../InitializationParentAnnotatedTypeFactory.java | 4 ++++ .../checker/nullness/NullnessNoInitAnnotatedTypeFactory.java | 3 +++ checker/tests/nullness/Issue3020.java | 1 - .../dataflow/cfg/builder/CFGTranslationPhaseOne.java | 2 +- .../org/checkerframework/dataflow/cfg/node/ClassNameNode.java | 4 +++- .../main/java/org/checkerframework/javacutil/TreeUtils.java | 2 +- 6 files changed, 12 insertions(+), 4 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationParentAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationParentAnnotatedTypeFactory.java index 39b13e367bd..775ec0f9bdb 100644 --- a/checker/src/main/java/org/checkerframework/checker/initialization/InitializationParentAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/initialization/InitializationParentAnnotatedTypeFactory.java @@ -779,6 +779,10 @@ public Void visitNewArray(NewArrayTree tree, AnnotatedTypeMirror type) { @Override public Void visitMemberSelect( MemberSelectTree tree, AnnotatedTypeMirror annotatedTypeMirror) { + Element elt = TreeUtils.elementFromUse(tree); + if (elt.toString().equals("class")) { + annotatedTypeMirror.replaceAnnotation(INITIALIZED); + } if (TreeUtils.isArrayLengthAccess(tree)) { annotatedTypeMirror.replaceAnnotation(INITIALIZED); } diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java index 9d55f343a6a..5ef1f66e8aa 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessNoInitAnnotatedTypeFactory.java @@ -670,6 +670,9 @@ public Void visitMemberSelect(MemberSelectTree tree, AnnotatedTypeMirror type) { type.replaceAnnotation(NONNULL); } + if (elt.toString().equals("class")) { + type.replaceAnnotation(NONNULL); + } return null; } diff --git a/checker/tests/nullness/Issue3020.java b/checker/tests/nullness/Issue3020.java index e98d5a723fc..b8d735d9eba 100644 --- a/checker/tests/nullness/Issue3020.java +++ b/checker/tests/nullness/Issue3020.java @@ -4,7 +4,6 @@ enum Issue3020 { void retrieveConstant() { Class theClass = Issue3020.class; // :: error: (accessing.nullable) - // :: error: (dereference.of.nullable) Object unused = passThrough(theClass.getEnumConstants())[0]; } diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java index 9dc97a5cbfe..a1aa7b5b1da 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/builder/CFGTranslationPhaseOne.java @@ -3585,7 +3585,7 @@ public Node visitMemberSelect(MemberSelectTree tree, Void p) { if (!TreeUtils.isFieldAccess(tree)) { // Could be a selector of a class or package Element element = TreeUtils.elementFromUse(tree); - if (ElementUtils.isTypeElement(element)) { + if (ElementUtils.isTypeElement(element) || element.toString().equals("class")) { ClassNameNode result = new ClassNameNode(tree, expr); extendWithClassNameNode(result); return result; diff --git a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ClassNameNode.java b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ClassNameNode.java index b34299862fc..7f5f0db1c23 100644 --- a/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ClassNameNode.java +++ b/dataflow/src/main/java/org/checkerframework/dataflow/cfg/node/ClassNameNode.java @@ -63,7 +63,9 @@ public ClassNameNode(MemberSelectTree tree, Node parent) { this.tree = tree; assert TreeUtils.isUseOfElement(tree) : "@AssumeAssertion(nullness): tree kind"; Element element = TreeUtils.elementFromUse(tree); - assert element instanceof TypeElement || element instanceof TypeParameterElement + assert element instanceof TypeElement + || element instanceof TypeParameterElement + || element.toString().equals("class") : "@AssumeAssertion(nullness)"; this.element = element; this.parent = parent; diff --git a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java index 850770dc6ba..c455a0216aa 100644 --- a/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java +++ b/javacutil/src/main/java/org/checkerframework/javacutil/TreeUtils.java @@ -1570,7 +1570,7 @@ public static boolean isFieldAccess(Tree tree) { MemberSelectTree memberSelect = (MemberSelectTree) tree; assert isUseOfElement(memberSelect) : "@AssumeAssertion(nullness): tree kind"; Element el = TreeUtils.elementFromUse(memberSelect); - if (el.getKind().isField()) { + if (el.getKind().isField() && !el.toString().equals("class")) { return (VariableElement) el; } } else if (tree.getKind() == Tree.Kind.IDENTIFIER) {