Skip to content

Commit e1923a9

Browse files
HenryXi1HenryXi1
committed
Add support for NonNullIfReturnsTrue and NonNullIfReturnsFalse
1 parent 2588840 commit e1923a9

8 files changed

Lines changed: 264 additions & 105 deletions

File tree

checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NotNullIfReturns.java renamed to checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturns.java

Lines changed: 11 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@
1212
* A <b>parameter</b> contract: expresses that the parameter is non-null when the method returns the
1313
* given value.
1414
*
15-
* <p><b>Semantic meaning:</b> {@code @NotNullIfReturns(v)} means: <i>this parameter is non-null
15+
* <p><b>Semantic meaning:</b> {@code @NonNullIfReturns(v)} means: <i>this parameter is non-null
1616
* when the method returns v</i>. That is: {@code method returns value() ⇒ parameter != null}.
1717
*
1818
* <p>This annotation only makes sense on parameters whose root type is {@code @Nullable} or
@@ -23,7 +23,7 @@
2323
* <p><b>Example 1: hasLength</b> — param is non-null when method returns true.
2424
*
2525
* <pre>{@code
26-
* public static boolean hasLength(@NotNullIfReturns(true) @Nullable String str) {
26+
* public static boolean hasLength(@NonNullIfReturns(true) @Nullable String str) {
2727
* return (str != null && !str.isEmpty());
2828
* }
2929
* }</pre>
@@ -34,15 +34,15 @@
3434
*
3535
* <pre>{@code
3636
* @Override
37-
* public boolean equals(@NotNullIfReturns(true) @Nullable Object other) {
37+
* public boolean equals(@NonNullIfReturns(true) @Nullable Object other) {
3838
* return this == other;
3939
* }
4040
* }</pre>
4141
*
4242
* <p><b>Example 3: isNull</b> — param is non-null when method returns false.
4343
*
4444
* <pre>{@code
45-
* public static boolean isNull(@NotNullIfReturns(false) @Nullable Object obj) {
45+
* public static boolean isNull(@NonNullIfReturns(false) @Nullable Object obj) {
4646
* return obj == null;
4747
* }
4848
* }</pre>
@@ -51,11 +51,16 @@
5151
*
5252
* <ul>
5353
* <li><b>Scope:</b> The annotation applies only to the parameter on which it is written.
54-
* <li><b>Meaning:</b> {@code @NotNullIfReturns(v)} means: param is non-null when method returns
54+
* <li><b>Meaning:</b> {@code @NonNullIfReturns(v)} means: param is non-null when method returns
5555
* v.
5656
* <li><b>Target:</b> Only formal parameters.
5757
* </ul>
5858
*
59+
* <p>For a fixed return value, use {@link NonNullIfReturnsTrue} or {@link NonNullIfReturnsFalse}
60+
* instead.
61+
*
62+
* @see NonNullIfReturnsTrue
63+
* @see NonNullIfReturnsFalse
5964
* @see EnsuresNonNullIf
6065
* @see NonNull
6166
* @see Nullable
@@ -66,7 +71,7 @@
6671
@Retention(RetentionPolicy.RUNTIME)
6772
@Target({ElementType.PARAMETER})
6873
@ParameterConditionalPostconditionAnnotation(qualifier = NonNull.class)
69-
public @interface NotNullIfReturns {
74+
public @interface NonNullIfReturns {
7075
/**
7176
* The return value under which the parameter is non-null.
7277
*

‎checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturnsFalse.java‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
package org.checkerframework.checker.nullness.qual;
2+
3+
import org.checkerframework.framework.qual.ParameterConditionalPostconditionAnnotation;
4+
5+
import java.lang.annotation.Documented;
6+
import java.lang.annotation.ElementType;
7+
import java.lang.annotation.Retention;
8+
import java.lang.annotation.RetentionPolicy;
9+
import java.lang.annotation.Target;
10+
11+
/**
12+
* A <b>parameter</b> contract: the parameter is non-null when the method returns {@code false}.
13+
*
14+
* <p>Equivalent to {@code @NonNullIfReturns(false)} but with a fixed value for use when the return
15+
* condition is always false (e.g. {@code isNull}).
16+
*
17+
* @see NonNullIfReturns
18+
* @see NonNullIfReturnsTrue
19+
*/
20+
@Documented
21+
@Retention(RetentionPolicy.RUNTIME)
22+
@Target({ElementType.PARAMETER})
23+
@ParameterConditionalPostconditionAnnotation(qualifier = NonNull.class, result = false)
24+
public @interface NonNullIfReturnsFalse {}

‎checker-qual/src/main/java/org/checkerframework/checker/nullness/qual/NonNullIfReturnsTrue.java‎

Lines changed: 24 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,24 @@
1+
package org.checkerframework.checker.nullness.qual;
2+
3+
import org.checkerframework.framework.qual.ParameterConditionalPostconditionAnnotation;
4+
5+
import java.lang.annotation.Documented;
6+
import java.lang.annotation.ElementType;
7+
import java.lang.annotation.Retention;
8+
import java.lang.annotation.RetentionPolicy;
9+
import java.lang.annotation.Target;
10+
11+
/**
12+
* A <b>parameter</b> contract: the parameter is non-null when the method returns {@code true}.
13+
*
14+
* <p>Equivalent to {@code @NonNullIfReturns(true)} but with a fixed value for use when the return
15+
* condition is always true (e.g. {@code hasLength}, {@code equals}).
16+
*
17+
* @see NonNullIfReturns
18+
* @see NonNullIfReturnsFalse
19+
*/
20+
@Documented
21+
@Retention(RetentionPolicy.RUNTIME)
22+
@Target({ElementType.PARAMETER})
23+
@ParameterConditionalPostconditionAnnotation(qualifier = NonNull.class, result = true)
24+
public @interface NonNullIfReturnsTrue {}

‎checker-qual/src/main/java/org/checkerframework/framework/qual/ParameterConditionalPostconditionAnnotation.java‎

Lines changed: 21 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -12,23 +12,26 @@
1212
* postcondition annotation: E is written on a formal parameter and expresses that the annotated
1313
* parameter has a given qualifier when the method returns a given boolean value.
1414
*
15-
* <p>E must have a single element {@code value()} of type {@code boolean} with the same meaning as
16-
* {@link EnsuresQualifierIf#result()}. The expression to which the qualifier applies is implicit:
17-
* it is the annotated parameter (e.g. {@code "#1"} for the first parameter).
15+
* <p>E either has a single element {@code value()} of type {@code boolean} with the same meaning as
16+
* {@link EnsuresQualifierIf#result()}, or E has no such element and the result is fixed by this
17+
* meta-annotation's {@link #result()} (for concrete annotations like
18+
* {@code @NonNullIfReturnsTrue}). The expression to which the qualifier applies is implicit: it is
19+
* the annotated parameter (e.g. {@code "#1"} for the first parameter).
1820
*
1921
* <p>For example, the nullness checker defines {@link
20-
* org.checkerframework.checker.nullness.qual.NotNullIfReturns}:
22+
* org.checkerframework.checker.nullness.qual.NonNullIfReturns}:
2123
*
2224
* <pre><code>
2325
* {@literal @}ParameterConditionalPostconditionAnnotation(qualifier = NonNull.class)
2426
* {@literal @}Target(ElementType.PARAMETER)
25-
* public {@literal @}interface NotNullIfReturns {
27+
* public {@literal @}interface NonNullIfReturns {
2628
* boolean value();
2729
* }
2830
* </code></pre>
2931
*
30-
* <p>Usage: {@code @NotNullIfReturns(true)} means the parameter is non-null when the method returns
31-
* true.
32+
* <p>Usage: {@code @NonNullIfReturns(true)} or {@code @NonNullIfReturnsTrue} means the parameter is
33+
* non-null when the method returns true; {@code @NonNullIfReturns(false)} or
34+
* {@code @NonNullIfReturnsFalse} when it returns false.
3235
*
3336
* @see ConditionalPostconditionAnnotation
3437
* @see EnsuresQualifierIf
@@ -39,9 +42,19 @@
3942
public @interface ParameterConditionalPostconditionAnnotation {
4043
/**
4144
* The qualifier that is established on the annotated parameter when the method returns the
42-
* value specified by the parameter annotation's {@code value()} element.
45+
* value specified by the parameter annotation's {@code value()} element, or by this {@link
46+
* #result()} when the annotation has no {@code value()} (e.g. {@code @NonNullIfReturnsTrue}).
4347
*
4448
* @return the qualifier
4549
*/
4650
Class<? extends Annotation> qualifier();
51+
52+
/**
53+
* The return value under which the qualifier holds. Used when the concrete annotation has no
54+
* {@code value()} element (e.g. {@code @NonNullIfReturnsTrue} /
55+
* {@code @NonNullIfReturnsFalse}). Ignored when the concrete annotation has {@code value()}.
56+
*
57+
* @return true if the qualifier holds when the method returns true, false when it returns false
58+
*/
59+
boolean result() default true;
4760
}

‎checker/tests/nullness/NonNullIfReturnsTest.java‎

Lines changed: 162 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,162 @@
1+
// Tests @NonNullIfReturns, @NonNullIfReturnsTrue, and @NonNullIfReturnsFalse (parameter-level
2+
// conditional postconditions) for both correct refinement and expected errors.
3+
4+
import org.checkerframework.checker.nullness.qual.NonNull;
5+
import org.checkerframework.checker.nullness.qual.NonNullIfReturns;
6+
import org.checkerframework.checker.nullness.qual.NonNullIfReturnsFalse;
7+
import org.checkerframework.checker.nullness.qual.NonNullIfReturnsTrue;
8+
import org.checkerframework.checker.nullness.qual.Nullable;
9+
10+
public class NonNullIfReturnsTest {
11+
12+
// -----------------------------------------------------------------------
13+
// @NonNullIfReturns(true) / (false)
14+
// -----------------------------------------------------------------------
15+
16+
public static boolean hasLength(@NonNullIfReturns(true) @Nullable String str) {
17+
return (str != null && !str.isEmpty());
18+
}
19+
20+
void useHasLength(@Nullable String s) {
21+
if (hasLength(s)) {
22+
@NonNull String n = s;
23+
n.hashCode();
24+
} else {
25+
// :: error: (assignment.type.incompatible)
26+
@NonNull String n = s;
27+
}
28+
}
29+
30+
@Override
31+
public boolean equals(@NonNullIfReturns(true) @Nullable Object other) {
32+
return this == other;
33+
}
34+
35+
void useEquals(NonNullIfReturnsTest a, @Nullable Object b) {
36+
if (a.equals(b)) {
37+
@NonNull Object n = b;
38+
n.hashCode();
39+
}
40+
}
41+
42+
public static boolean isNull(@NonNullIfReturns(false) @Nullable Object obj) {
43+
return obj == null;
44+
}
45+
46+
void useIsNull(@Nullable Object p) {
47+
if (!isNull(p)) {
48+
@NonNull Object n = p;
49+
n.hashCode();
50+
} else {
51+
// :: error: (assignment.type.incompatible)
52+
@NonNull Object n = p;
53+
}
54+
}
55+
56+
public static boolean bothNonNull(
57+
@NonNullIfReturns(true) @Nullable Object a,
58+
@NonNullIfReturns(true) @Nullable Object b) {
59+
return a != null && b != null;
60+
}
61+
62+
void useBothNonNull(@Nullable Object x, @Nullable Object y) {
63+
if (bothNonNull(x, y)) {
64+
@NonNull Object nx = x;
65+
@NonNull Object ny = y;
66+
nx.hashCode();
67+
ny.hashCode();
68+
} else {
69+
// :: error: (assignment.type.incompatible)
70+
@NonNull Object nx = x;
71+
// :: error: (assignment.type.incompatible)
72+
@NonNull Object ny = y;
73+
}
74+
}
75+
76+
// Checker trusts the annotation; does not verify method body.
77+
public boolean alwaysTrue(@NonNullIfReturns(true) @Nullable Object obj) {
78+
return true;
79+
}
80+
81+
void useAlwaysTrue(@Nullable Object p) {
82+
if (alwaysTrue(p)) {
83+
@NonNull Object n = p;
84+
n.hashCode();
85+
} else {
86+
// :: error: (assignment.type.incompatible)
87+
@NonNull Object n = p;
88+
}
89+
}
90+
91+
// -----------------------------------------------------------------------
92+
// @NonNullIfReturnsTrue
93+
// -----------------------------------------------------------------------
94+
95+
public static boolean hasLengthTrue(@NonNullIfReturnsTrue @Nullable String str) {
96+
return (str != null && !str.isEmpty());
97+
}
98+
99+
void useHasLengthTrue(@Nullable String s) {
100+
if (hasLengthTrue(s)) {
101+
@NonNull String n = s;
102+
n.hashCode();
103+
} else {
104+
// :: error: (assignment.type.incompatible)
105+
@NonNull String n = s;
106+
}
107+
}
108+
109+
public static boolean bothNonNullTrue(
110+
@NonNullIfReturnsTrue @Nullable Object a, @NonNullIfReturnsTrue @Nullable Object b) {
111+
return a != null && b != null;
112+
}
113+
114+
void useBothNonNullTrue(@Nullable Object x, @Nullable Object y) {
115+
if (bothNonNullTrue(x, y)) {
116+
@NonNull Object nx = x;
117+
@NonNull Object ny = y;
118+
nx.hashCode();
119+
} else {
120+
// :: error: (assignment.type.incompatible)
121+
@NonNull Object nx = x;
122+
// :: error: (assignment.type.incompatible)
123+
@NonNull Object ny = y;
124+
}
125+
}
126+
127+
// -----------------------------------------------------------------------
128+
// @NonNullIfReturnsFalse
129+
// -----------------------------------------------------------------------
130+
131+
public static boolean isNullFalse(@NonNullIfReturnsFalse @Nullable Object obj) {
132+
return obj == null;
133+
}
134+
135+
void useIsNullFalse(@Nullable Object p) {
136+
if (!isNullFalse(p)) {
137+
@NonNull Object n = p;
138+
n.hashCode();
139+
} else {
140+
// :: error: (assignment.type.incompatible)
141+
@NonNull Object n = p;
142+
}
143+
}
144+
145+
public static boolean neitherNull(
146+
@NonNullIfReturnsFalse @Nullable Object a, @NonNullIfReturnsFalse @Nullable Object b) {
147+
return a == null || b == null;
148+
}
149+
150+
void useNeitherNull(@Nullable Object x, @Nullable Object y) {
151+
if (!neitherNull(x, y)) {
152+
@NonNull Object nx = x;
153+
@NonNull Object ny = y;
154+
nx.hashCode();
155+
} else {
156+
// :: error: (assignment.type.incompatible)
157+
@NonNull Object nx = x;
158+
// :: error: (assignment.type.incompatible)
159+
@NonNull Object ny = y;
160+
}
161+
}
162+
}

0 commit comments

Comments
 (0)