From 0994c6aca41c9f64b63b6f4064d4f0f050b02e19 Mon Sep 17 00:00:00 2001 From: Suvrat1629 Date: Sun, 4 Jan 2026 01:05:59 +0530 Subject: [PATCH 1/4] ternary false negative fix --- .../checker/nullness/NullnessVisitor.java | 90 ++++++++++++++----- checker/tests/nullness/Issue6849.java | 16 ++++ 2 files changed, 84 insertions(+), 22 deletions(-) create mode 100644 checker/tests/nullness/Issue6849.java diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java index 324c1fbb74c0..c7ea94207fbf 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java @@ -68,7 +68,8 @@ public class NullnessVisitor extends InitializationVisitor { // Error message keys - // private static final @CompilerMessageKey String ASSIGNMENT_TYPE_INCOMPATIBLE = "assignment"; + // private static final @CompilerMessageKey String ASSIGNMENT_TYPE_INCOMPATIBLE + // = "assignment"; private static final @CompilerMessageKey String UNBOXING_OF_NULLABLE = "unboxing.of.nullable"; private static final @CompilerMessageKey String LOCKING_NULLABLE = "locking.nullable"; private static final @CompilerMessageKey String THROWING_NULLABLE = "throwing.nullable"; @@ -140,7 +141,8 @@ public NullnessAnnotatedTypeFactory createTypeFactory() { @Override public boolean isValidUse(AnnotatedPrimitiveType type, Tree tree) { - // The Nullness Checker issues a more comprehensible "nullness.on.primitive" error rather + // The Nullness Checker issues a more comprehensible "nullness.on.primitive" + // error rather // than the "annotations.on.use" error this method would issue. return true; } @@ -152,10 +154,13 @@ protected boolean commonAssignmentCheck( @CompilerMessageKey String errorKey, Object... extraArgs) { - // Allow a MonotonicNonNull field to be initialized to null at its declaration, in a - // constructor, or in an initializer block. (The latter two are, strictly speaking, unsound - // because the constructor or initializer block might have previously set the field to a - // non-null value. Maybe add an option to disable that behavior.) + // Allow a MonotonicNonNull field to be initialized to null at its declaration, + // in a + // constructor, or in an initializer block. (The latter two are, strictly + // speaking, unsound + // because the constructor or initializer block might have previously set the + // field to a + // non-null value. Maybe add an option to disable that behavior.) Element elem = initializedElement(varTree); if (elem != null && atypeFactory.fromElement(elem).hasEffectiveAnnotation(MONOTONIC_NONNULL) @@ -184,9 +189,10 @@ protected boolean commonAssignmentCheck( MemberSelectTree mst = (MemberSelectTree) varTree; ExpressionTree receiver = mst.getExpression(); // This recognizes "this.fieldname = ..." but not "MyClass.fieldname = ..." or - // "MyClass.this.fieldname = ...". The latter forms are probably rare in a + // "MyClass.this.fieldname = ...". The latter forms are probably rare in a // constructor. - // Note that this method should return non-null only for fields of this class, not + // Note that this method should return non-null only for fields of this class, + // not // fields of any other class, including outer classes. if (!(receiver instanceof IdentifierTree) || !((IdentifierTree) receiver).getName().contentEquals("this")) { @@ -212,9 +218,12 @@ protected boolean commonAssignmentCheck( ExpressionTree valueExp, @CompilerMessageKey String errorKey, Object... extraArgs) { - // Use the valueExp as the context because data flow will have a value for that tree. It - // might not have a value for the var tree. This is sound because if data flow has - // determined @PolyNull is @Nullable at the RHS, then it is also @Nullable for the LHS. + // Use the valueExp as the context because data flow will have a value for that + // tree. It + // might not have a value for the var tree. This is sound because if data flow + // has + // determined @PolyNull is @Nullable at the RHS, then it is also @Nullable for + // the LHS. atypeFactory.replacePolyQualifier(varType, valueExp); return super.commonAssignmentCheck(varType, valueExp, errorKey, extraArgs); } @@ -382,9 +391,12 @@ public Void visitAssert(AssertTree tree, Void p) { // See also // org.checkerframework.dataflow.cfg.builder.CFGBuilder.CFGTranslationPhaseOne.visitAssert - // In cases where neither assumeAssertionsAreEnabled nor assumeAssertionsAreDisabled are - // turned on and @AssumeAssertions is not used, checkForNullability is still called since - // the CFGBuilder will have generated one branch for which asserts are assumed to be + // In cases where neither assumeAssertionsAreEnabled nor + // assumeAssertionsAreDisabled are + // turned on and @AssumeAssertions is not used, checkForNullability is still + // called since + // the CFGBuilder will have generated one branch for which asserts are assumed + // to be // enabled. boolean doVisitAssert; @@ -427,7 +439,8 @@ public Void visitInstanceOf(InstanceOfTree tree, Void p) { } } } - // Don't call super because it will issue an incorrect instanceof.unsafe warning. + // Don't call super because it will issue an incorrect instanceof.unsafe + // warning. // Instead, just scan the part before "instanceof". super.scan(tree.getExpression(), p); return null; @@ -555,7 +568,7 @@ public Void visitMethodInvocation(MethodInvocationTree tree, Void p) { * @param tree a method invocation whose first formal parameter is of String type * @return the first argument if it is a literal, otherwise null */ - /*package-private*/ static @Nullable String literalFirstArgument(MethodInvocationTree tree) { + /* package-private */ static @Nullable String literalFirstArgument(MethodInvocationTree tree) { List args = tree.getArguments(); assert !args.isEmpty(); ExpressionTree arg = args.get(0); @@ -683,7 +696,8 @@ private boolean isUnboxingOperation(BinaryTree tree) { return isPrimitive(tree.getLeftOperand()) != isPrimitive(tree.getRightOperand()); } else { // All BinaryTree's are of type String, a primitive type or the reference type - // equivalent of a primitive type. Furthermore, Strings don't have a primitive type, and + // equivalent of a primitive type. Furthermore, Strings don't have a primitive + // type, and // therefore only BinaryTrees that aren't String can cause unboxing. return !isString(tree); } @@ -772,6 +786,33 @@ public Void visitDoWhileLoop(DoWhileLoopTree tree, Void p) { @Override public Void visitConditionalExpression(ConditionalExpressionTree tree, Void p) { checkForNullability(tree.getCondition(), CONDITION_NULLABLE); + // If the overall conditional expression has a primitive Java type but one or both + // operand expressions are reference types, then unboxing will occur as part of + // evaluating the conditional. In that case, check the operand(s) for possible + // nullness (unboxing.of.nullable). + AnnotatedTypeMirror type = atypeFactory.getAnnotatedType(tree); + // Only check for unboxing when javac has chosen a primitive underlying type + // for the conditional expression, but one or both operands are non-primitive. + if (type.getKind().isPrimitive()) { + ExpressionTree trueExpr = tree.getTrueExpression(); + ExpressionTree falseExpr = tree.getFalseExpression(); + boolean trueNeedsUnboxing = !TypesUtils.isPrimitive(TreeUtils.typeOf(trueExpr)); + boolean falseNeedsUnboxing = !TypesUtils.isPrimitive(TreeUtils.typeOf(falseExpr)); + + if (trueNeedsUnboxing) { + if (!checkForNullability(trueExpr, UNBOXING_OF_NULLABLE)) { + // If we reported an unboxing.of.nullable error for the true arm, stop + // further checking to avoid cascading errors. + return null; + } + } + if (falseNeedsUnboxing) { + if (!checkForNullability(falseExpr, UNBOXING_OF_NULLABLE)) { + return null; + } + } + } + return super.visitConditionalExpression(tree, p); } @@ -781,19 +822,24 @@ protected void checkExceptionParameter(CatchTree tree) { List annoTrees = param.getModifiers().getAnnotations(); Tree paramType = param.getType(); if (atypeFactory.containsNullnessAnnotation(annoTrees, paramType)) { - // This is a warning rather than an error because writing `@Nullable` could make sense - // if the catch block re-assigns the variable to null. (That would be bad style.) + // This is a warning rather than an error because writing `@Nullable` could make + // sense + // if the catch block re-assigns the variable to null. (That would be bad + // style.) checker.reportWarning(param, "nullness.on.exception.parameter"); } // Don't call super. - // BasetypeVisitor forces annotations on exception parameters to be top, but because - // exceptions can never be null, the Nullness Checker does not require this check. + // BasetypeVisitor forces annotations on exception parameters to be top, but + // because + // exceptions can never be null, the Nullness Checker does not require this + // check. } @Override public Void visitAnnotation(AnnotationTree tree, Void p) { - // All annotation arguments are non-null and initialized, so no need to check them. + // All annotation arguments are non-null and initialized, so no need to check + // them. return null; } diff --git a/checker/tests/nullness/Issue6849.java b/checker/tests/nullness/Issue6849.java new file mode 100644 index 000000000000..9f29f262f8f4 --- /dev/null +++ b/checker/tests/nullness/Issue6849.java @@ -0,0 +1,16 @@ +import java.util.*; +import org.checkerframework.checker.nullness.qual.*; + +public class Issue6849 { + + public static T m(List lst) { + return lst.get(0); + } + + public static void main(String[] args) { + List<@Nullable Integer> lst = new LinkedList<>(); + lst.add(null); + int y = ((true) ? Issue6849.<@Nullable Integer>m(lst) : 10); + // :: error: (unboxing.of.nullable) + } +} From f60011f31405225afd1b31beaa85efd1f8933365 Mon Sep 17 00:00:00 2001 From: Suvrat1629 Date: Sun, 4 Jan 2026 12:16:00 +0530 Subject: [PATCH 2/4] change --- .../checker/nullness/NullnessVisitor.java | 63 +++++++------------ checker/tests/nullness/Issue6849.java | 2 +- 2 files changed, 23 insertions(+), 42 deletions(-) diff --git a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java index c7ea94207fbf..d1188f7eccd3 100644 --- a/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java +++ b/checker/src/main/java/org/checkerframework/checker/nullness/NullnessVisitor.java @@ -68,8 +68,7 @@ public class NullnessVisitor extends InitializationVisitor { // Error message keys - // private static final @CompilerMessageKey String ASSIGNMENT_TYPE_INCOMPATIBLE - // = "assignment"; + // private static final @CompilerMessageKey String ASSIGNMENT_TYPE_INCOMPATIBLE = "assignment"; private static final @CompilerMessageKey String UNBOXING_OF_NULLABLE = "unboxing.of.nullable"; private static final @CompilerMessageKey String LOCKING_NULLABLE = "locking.nullable"; private static final @CompilerMessageKey String THROWING_NULLABLE = "throwing.nullable"; @@ -141,8 +140,7 @@ public NullnessAnnotatedTypeFactory createTypeFactory() { @Override public boolean isValidUse(AnnotatedPrimitiveType type, Tree tree) { - // The Nullness Checker issues a more comprehensible "nullness.on.primitive" - // error rather + // The Nullness Checker issues a more comprehensible "nullness.on.primitive" error rather // than the "annotations.on.use" error this method would issue. return true; } @@ -154,13 +152,10 @@ protected boolean commonAssignmentCheck( @CompilerMessageKey String errorKey, Object... extraArgs) { - // Allow a MonotonicNonNull field to be initialized to null at its declaration, - // in a - // constructor, or in an initializer block. (The latter two are, strictly - // speaking, unsound - // because the constructor or initializer block might have previously set the - // field to a - // non-null value. Maybe add an option to disable that behavior.) + // Allow a MonotonicNonNull field to be initialized to null at its declaration, in a + // constructor, or in an initializer block. (The latter two are, strictly speaking, unsound + // because the constructor or initializer block might have previously set the field to a + // non-null value. Maybe add an option to disable that behavior.) Element elem = initializedElement(varTree); if (elem != null && atypeFactory.fromElement(elem).hasEffectiveAnnotation(MONOTONIC_NONNULL) @@ -189,10 +184,9 @@ protected boolean commonAssignmentCheck( MemberSelectTree mst = (MemberSelectTree) varTree; ExpressionTree receiver = mst.getExpression(); // This recognizes "this.fieldname = ..." but not "MyClass.fieldname = ..." or - // "MyClass.this.fieldname = ...". The latter forms are probably rare in a + // "MyClass.this.fieldname = ...". The latter forms are probably rare in a // constructor. - // Note that this method should return non-null only for fields of this class, - // not + // Note that this method should return non-null only for fields of this class, not // fields of any other class, including outer classes. if (!(receiver instanceof IdentifierTree) || !((IdentifierTree) receiver).getName().contentEquals("this")) { @@ -218,12 +212,9 @@ protected boolean commonAssignmentCheck( ExpressionTree valueExp, @CompilerMessageKey String errorKey, Object... extraArgs) { - // Use the valueExp as the context because data flow will have a value for that - // tree. It - // might not have a value for the var tree. This is sound because if data flow - // has - // determined @PolyNull is @Nullable at the RHS, then it is also @Nullable for - // the LHS. + // Use the valueExp as the context because data flow will have a value for that tree. It + // might not have a value for the var tree. This is sound because if data flow has + // determined @PolyNull is @Nullable at the RHS, then it is also @Nullable for the LHS. atypeFactory.replacePolyQualifier(varType, valueExp); return super.commonAssignmentCheck(varType, valueExp, errorKey, extraArgs); } @@ -391,12 +382,9 @@ public Void visitAssert(AssertTree tree, Void p) { // See also // org.checkerframework.dataflow.cfg.builder.CFGBuilder.CFGTranslationPhaseOne.visitAssert - // In cases where neither assumeAssertionsAreEnabled nor - // assumeAssertionsAreDisabled are - // turned on and @AssumeAssertions is not used, checkForNullability is still - // called since - // the CFGBuilder will have generated one branch for which asserts are assumed - // to be + // In cases where neither assumeAssertionsAreEnabled nor assumeAssertionsAreDisabled are + // turned on and @AssumeAssertions is not used, checkForNullability is still called since + // the CFGBuilder will have generated one branch for which asserts are assumed to be // enabled. boolean doVisitAssert; @@ -439,8 +427,7 @@ public Void visitInstanceOf(InstanceOfTree tree, Void p) { } } } - // Don't call super because it will issue an incorrect instanceof.unsafe - // warning. + // Don't call super because it will issue an incorrect instanceof.unsafe warning. // Instead, just scan the part before "instanceof". super.scan(tree.getExpression(), p); return null; @@ -568,7 +555,7 @@ public Void visitMethodInvocation(MethodInvocationTree tree, Void p) { * @param tree a method invocation whose first formal parameter is of String type * @return the first argument if it is a literal, otherwise null */ - /* package-private */ static @Nullable String literalFirstArgument(MethodInvocationTree tree) { + /*package-private*/ static @Nullable String literalFirstArgument(MethodInvocationTree tree) { List args = tree.getArguments(); assert !args.isEmpty(); ExpressionTree arg = args.get(0); @@ -696,8 +683,7 @@ private boolean isUnboxingOperation(BinaryTree tree) { return isPrimitive(tree.getLeftOperand()) != isPrimitive(tree.getRightOperand()); } else { // All BinaryTree's are of type String, a primitive type or the reference type - // equivalent of a primitive type. Furthermore, Strings don't have a primitive - // type, and + // equivalent of a primitive type. Furthermore, Strings don't have a primitive type, and // therefore only BinaryTrees that aren't String can cause unboxing. return !isString(tree); } @@ -822,24 +808,19 @@ protected void checkExceptionParameter(CatchTree tree) { List annoTrees = param.getModifiers().getAnnotations(); Tree paramType = param.getType(); if (atypeFactory.containsNullnessAnnotation(annoTrees, paramType)) { - // This is a warning rather than an error because writing `@Nullable` could make - // sense - // if the catch block re-assigns the variable to null. (That would be bad - // style.) + // This is a warning rather than an error because writing `@Nullable` could make sense + // if the catch block re-assigns the variable to null. (That would be bad style.) checker.reportWarning(param, "nullness.on.exception.parameter"); } // Don't call super. - // BasetypeVisitor forces annotations on exception parameters to be top, but - // because - // exceptions can never be null, the Nullness Checker does not require this - // check. + // BasetypeVisitor forces annotations on exception parameters to be top, but because + // exceptions can never be null, the Nullness Checker does not require this check. } @Override public Void visitAnnotation(AnnotationTree tree, Void p) { - // All annotation arguments are non-null and initialized, so no need to check - // them. + // All annotation arguments are non-null and initialized, so no need to check them. return null; } diff --git a/checker/tests/nullness/Issue6849.java b/checker/tests/nullness/Issue6849.java index 9f29f262f8f4..2b11474f0b12 100644 --- a/checker/tests/nullness/Issue6849.java +++ b/checker/tests/nullness/Issue6849.java @@ -10,7 +10,7 @@ public static T m(List lst) { public static void main(String[] args) { List<@Nullable Integer> lst = new LinkedList<>(); lst.add(null); - int y = ((true) ? Issue6849.<@Nullable Integer>m(lst) : 10); // :: error: (unboxing.of.nullable) + int y = ((true) ? Issue6849.<@Nullable Integer>m(lst) : 10); } } From 8ba70182bcf2fad92a68246a173313cc35091a22 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Wed, 4 Mar 2026 07:55:59 -0800 Subject: [PATCH 3/4] Put error message key in brackets --- checker/tests/nullness/Issue6849.java | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/checker/tests/nullness/Issue6849.java b/checker/tests/nullness/Issue6849.java index 2b11474f0b12..553b9a7d6620 100644 --- a/checker/tests/nullness/Issue6849.java +++ b/checker/tests/nullness/Issue6849.java @@ -10,7 +10,7 @@ public static T m(List lst) { public static void main(String[] args) { List<@Nullable Integer> lst = new LinkedList<>(); lst.add(null); - // :: error: (unboxing.of.nullable) + // :: error: [unboxing.of.nullable] int y = ((true) ? Issue6849.<@Nullable Integer>m(lst) : 10); } } From c885fc1a3490b007e66315d697a95ba7cc521c93 Mon Sep 17 00:00:00 2001 From: Michael Ernst Date: Thu, 23 Apr 2026 08:22:12 -0700 Subject: [PATCH 4/4] Add contributor --- docs/manual/contributors.tex | 1 + 1 file changed, 1 insertion(+) diff --git a/docs/manual/contributors.tex b/docs/manual/contributors.tex index fc5a6d8872f5..2eb88be2fa3b 100644 --- a/docs/manual/contributors.tex +++ b/docs/manual/contributors.tex @@ -141,6 +141,7 @@ Steph Dietzel, Stephan Schroevers, Stuart Pernsteiner, +Suvrat Acharya, Suzanne Millstein, Thomas Schweizer, Thomas Wei\ss schuh,