Ways to mark a method which promises to throw on a null argument

[kevinb9n]

Our overarching design direction is to capture nullness data through types alone, and have those types work as analogously to base types as possible.

This gives us most of what we need, but a few things are missing.

One is: if a method actually promises it will not complete normally upon null input (or maybe more specifically promises to throw NPE?), that is valuable knowledge to capture somehow, and our current annotations don't provide for it.

Oddly, all four combinations are valid between this and @Nullable itself. Some methods like Double.valueOf could make this promise for a non-nullable parameter. But our friends checkNotNull and the like want to make this promise for a nullable parameter!

A checker can use this information. Particularly, for the checkNotNull case, it would then be able to "learn" that the type of a variable becomes non-nullable below the place where it was passed to that method. This is the main motivating case I think.

I believe that the various worries some of us had about checkNotNull being nullable can be addressed this way instead (and it will be nullable).

[lazaroclapp]

As a note, the way NullAway handles this is to support a subset of JetBrains's @Contract annotations. In particular:

@Contract("null -> fail")
public Object checkNotNull(@Nullable Object o) {...}

I imagine there will be some hesitancy to make JSpecify dependent on something like JetBrains's @Contract, particularly since even in NullAway we handle only a subset of its contract specifications. But, at the same time, I want to note that contracts over nullness are generally useful, beyond "if the Nth argument is null, method fails".

For example, we regularly see usage of the following specs:

@Contract("!null -> !null") // Usually for methods that return their argument after operating on it.
@Contract("null -> true") // This can be understood as implying arg != null when `false`... e.g. Strings.isEmpty(...)
@Contract("null -> false") // Converse of the above (implies arg != null when `true`).

Wonder if we want something like @ThrowsOnNull(arg#N) here (for minimality), or something more general along the lines of these @Contract annotations (to cover more common use cases).

[cpovirk]

Good point about @Contract vs. individual annotations.

I'm going to predict that @kevinb9n will propose keeping this thread focused on the question of whether "promise to throw NPE" is a requirement, with the discussion of the "API" in a separate issue. Maybe we should start that thread now, along with other threads for the other possible requirements. Kevin?

(For searchability: In CF terminology, we're talking about (part of) @EnsuresNonNull. A possible future thread could cover @EnsuresNonNullIf. Yet another possible future thread could cover the fact that CF lets those annotations tell you about other methods, as in "if hasFoo() returns true, then getFoo() returns non-null." And there's already a thread about @PolyNull, including some thoughts that I should flesh out someday about why I lean toward a separate annotation over a @Contract annotation for that.)

[lazaroclapp]

If this is two separate questions:

a) Should there be a JSpecify mechanism to mark a method as throwing an exception when passed null, even though @Nullable is the accepted argument type at compile time?

and

b) What should that mechanism look like?

Then my take on (a) is unambiguously that there should be. Tools already have different ways to handle this case, showing that it matters in practice, and it does happen at the interface between clients and libraries, which suggests that we might want a uniform way to handle it across tools. Certainly not a 1.0/MVP requirement, but seems well within scope of JSpecify.

My take on (b) is less clear. NullAway uses @Contract primarily for this purpose. I like @Contract("null -> fail") over @EnsuresNonNull("#1") mostly on account of it being more readable as documentation (the second option requires you to reason "the method must guarantee the argument is non-null on successful termination, Java passes arguments by reference, ergo the only option left to the method to implement the semantics is to terminate with an exception if the argument is null on method entry"; the first can be read "if passed null, this method fails"). Also, as mentioned above, the pre/post syntax of @Contract can cover a few other cases with static checking (thought I think all those listed could also be covered by a version of @EnsuresNonNullIf that allows for result to be an enum of FALSE, TRUE, NULL, NONNULL instead of just a boolean).

On the other hand, NullAway does implement a version of @EnsuresNonNull and @RequiresNonNull for fields, since the JetBrains @Contract strings make it harder to implement per/post conditions on fields. We have given some thought to having a generalized version of @Contract that covers both arguments and fields, and we lean towards it being contract-like because of the readability argument above, but we could switch over to ensures/requires style if it can cover the @Contract("!null -> !null") case too, which we have found extremely common.

[kevinb9n]

I think it's probably fair to treat the @Contract mini-language as a "bridge too far" for this project for the foreseeable future. That could change, say, if two different tool owners start pushing that plan forward of their own motivations.

Of course every checker should be absolutely free to respect any other @Contract annotation it wants to, putting that information together with what it learns from JSpecify annotations. I think that is what winning looks like. (There are limits; analysis should only refine types, not go the other direction, so once any source determines something to be non-null there probably shouldn't be a way to say no cancel that.)

[kevinb9n]

• Could it possibly be worth even adding to non-nullable arguments (Double.valueOf(s))? Knowing the method can be trusted to do a runtime check could be theoretically worth something, but it changes the situation drastically if this is going to start popping up everywhere. And it would be dodgy to put this on a non-final or @Override method.

• It seems like this might be too special-case to worry about, but I do think a lot of teams have cloned versions of something like Guava Preconditions (hey, even I know it would be silly to depend on Guava for only that), so a checker could never hard code them all, and those methods end up having a lot of usages so the benefits would multiply.

[kevinb9n]

(I believe this annotation does not want to dictate what exception type has to be thrown. All that matters is that the method will not complete normally in that case.)

[artempyanykh]

My 2¢:

1. It's valuable for a tool to support some form of contracts as it improves the fidelity of the analysis and its UX. Our internal tool supports JetBrains' @Contract annotation. We actually went as far as adding a small specialized SMT solver which handles @Contract and other kinds of inference problems.
2. Would it be great to have a unified contract definition language that would work both for Java and Kotlin (unfortunately, @Contract doesn't work in Kotlin)? Yes!
3. Should we make some contracts relating nullness and runtime behaviour a part of JSpecify spec? Hm... not that obvious.
   1. Types cover some aspects of run-time behaviour but not all. Exceptions in Java are the norm so potentially all methods can throw and the question of the return type of the method is orthogonal to the question of whether the method will actually return the value at all.
   2. The information that "the method throws on null" is probably of the main interest in the implementation code and probably with regards to flow sensitive type refinements. As far as I remember the original focus of JSpecify was on the API surface.
   3. Where do we draw the line between what types of "contract" we want to make first-class citizen and what won't make the cut? Is it only checkNotNull types of contract? How about checkState? How about Objects.null/nonNull - when combined with conditionals they also provide important information?

I guess, for me the main question is: do we feel that the presence of this marker annotation is essential for completeness of JSpecify's basic nullness semantics?

I can say that in out internal code the number of methods that actually require a contract like checkNotNull is a rounding error, so I'm not really sure whether it should be a part of JSpecify's core package.

[kevinb9n]

2. The information that "the method throws on null" is probably of the main interest in the implementation code and probably with regards to flow sensitive type refinements. As far as I remember the original focus of JSpecify was on the API surface.

Well, yes and no. Annotations you put in your file only to benefit that file itself have less need to be standardized. It is annoying when you and your teammate prefer different tools, but you could at least just agree on one. Annotations you put in your file for the benefit of dependent files (which basically is why we're talking about the APIs) are different and you do need a standardized answer.

If checkNotNull-type methods in released libraries were a really common thing then this would justify why we need a resolution to this issue. But, they probably shouldn't be, so maybe we can just pass around a hardcoded config file to each other.

3. Where do we draw the line between what types of "contract" we want to make first-class citizen and what won't make the cut? Is it only checkNotNull types of contract? How about checkState? How about Objects.null/nonNull - when combined with conditionals they also provide important information?

Indeed. And with a whole contract language we'd have a pile of those decisions to make all up front just to get it off the ground. Annotations seem to make it easier to just go one by one.

Maybe "drawing the line" is like this?: if at least two different tool owners feel motivated enough to add/support the annotation themselves, then better standardize it?

I guess, for me the main question is: do we feel that the presence of this marker annotation is essential for completeness of JSpecify's basic nullness semantics?

Yeah I do think this question is why it's been labeled post-1.0.

I can say that in out internal code the number of methods that actually require a contract like checkNotNull is a rounding error, so I'm not really sure whether it should be a part of JSpecify's core package.

(As noted above, maybe the value scales with the # of calls to those methods though. Except that the most popular such methods would be the ones checkers are hardcoding anyway.)

[artempyanykh]

Except that the most popular such methods would be the ones checkers are hardcoding anyway

Yes. I guess the TL;DR: of my comment is that: since people usually don't roll out their own checkNotNull (IOW there's a small number of existing methods), checkers hard-code support for these, and the semantics is really straightforward here (= no divergence between checkers), I struggle to see the added value of standardising this one annotation.

On the other hand, if we do end up standardising whatever @FailOnNull annotation we come up with (an imaginary example below):

public <T extends Object> T checkNotNull(@FailOnNull @Nullable T)

Supporting it will take us a couple LOCs, so no big deal. But also I don't think it'll allow us to remove any of the hard-coded configs we already have; at least in the foreseeable future.

[kevinb9n]

Makes sense and imho this is the right way to think.

I think leaving this open but tagged Post-1.0 seems appropriate. We could further have distinct labels for "core nullness" vs "non-core nullness" or something, but for now, seems good.

(I sometimes comment on non-1.0 issues but I do spend most of my "what to do next" time looking at a 1.0 view.)

When it comes to eliminating hard coding, just for the remaining hardcoded lists to "feel like they have an expiration date" would be a good state to reach, even if a very distant one.

[cpovirk]

(nothing exciting here; just cross-referencing discussions and recording a false start in my thinking)

I believe this annotation does not want to dictate what exception type has to be thrown.

#309 (comment) is a reminder that there's at least one family of common methods that throw something other than NullPointerException in this case. (I'm pretty sure that something Charset-related does, too.)

I want to say that the Checker Framework does dataflow based on specific exception types. But after all of 30 seconds of thought, I'm not sure that it could actually benefit from knowing the specific type of exception that is thrown in case of a null argument:

Suppose that an argument foo has a @Nullable type and that a method call bar(foo) is known to throw SomeException when its parameter is null. That still doesn't prove anything about foo inside a catch (SomeException e) block or inside any other catch block. (And inside the try, we already know it's non-null after the call, regardless of what type would have been thrown.) If we knew that a method could throw SomeException if and only if a parameter were null, then we might be able to get somewhere. But I would expect the value of that additional information to be minimal, and it might well be more than offset by people who use that annotation when "if and only if" does not hold.

[edit: But see also #309 (comment), in which maybe I can see something that the exception type could give some tools, arguably, someday, maybe?]

[Mooninaut]

I think an annotation that says that a method throws 100% of the time if a given parameter is null does have value as a form of documentation, so I support it.

I'm much more ambivalent on the exception type parameter than I previously was.

In theory, a tool could suppress a "nullable value passed as non-nullable method parameter" warning if the method call is inside a try block with a catch (SomeException e) block, and the parameter is annotated @ThrowsOnNull(SomeException.class).

The benefit of specifying the exception type is theoretical and if implemented would be marginal at best. I think it probably doesn't matter.

I'm leaning in the direction that a standardized way for tools to share detailed semantic information about library methods (like "Throws SomeException when parameter X is null") completely independent of annotations would be more valuable for these edge cases than creating a new annotation for every edge case. That is also outside the scope of JSpecify. JSpecify annotations should be broadly applicable and have simple, easy to understand semantics.

[cpovirk]

Given the amount of time it takes to annotate a library for nullness, and given that we'd ideally want the annotation discussed here to be enforced by tools, and given the amount of noise it would introduce to put @MethodThrowsIfNull on a ton of parameters (or the inconsistency if we don't use it everywhere it makes sense)[*], I explicitly do not want to advocate for designing this anytime soon. But I do want to make a note while it's on my mind:

One of the challenges we're facing now is how to update Kotlin code that would fail to compile after we add nullness information. For example, once Kotlin knows that a method parameter has a non-nullable type, it won't let us pass nullable values anymore. The obvious solution is to add !! to each such argument. But that preserves behavior only if the method was going to throw NPE (or if the argument is never null in practice). And while that's very often the case, it's not the case if someone declares a SettableFuture<Foo> and then tries to call set(null) on it: The right solution there isn't to write set(null!!) but rather to change to SettableFuture<Foo?>.

Anyway, my point here is that it would be convenient if our tooling knew that set(null) would not trigger an immediate NPE but that (say) ImmutableList.of(null) would.

[*] We could make the annotation burden less bad by having a @NullMarked-style "defaulting" annotation. But that leads to get more design questions: Presumably the annotation applies all non-nullable parameters... and presumably there's a way to override it for individual parameters that don't follow the class's usual behavior.... Do we end up with a system of 4 annotations just for this purpose? But I'm really not trying to design this now, just trying to note that the design would be non-trivial.

[Mooninaut]

@cpovirk I can't speak to Kotlin, but don't think the majority of Java projects would need to write this annotation at all; they could rely on standard nullability annotations. I don't see a need for a @NullMarked-style default. But I agree with kevinb9n that:

A checker can use this information. Particularly, for the checkNotNull case, it would then be able to "learn" that the type of a variable becomes non-nullable below the place where it was passed to that method. This is the main motivating case I think."

I think annotating the Java standard library and the most-used utility libraries like Apache Commons, Guava, etc. would provide 99% of the potential value of this annotation. I imagine static analysis tools already hard-code this information for the most common APIs, so that would reduce their workload.

Applications and non-utility libraries wouldn't have to annotate their APIs with it, except possibly their own utility methods, but would still benefit from consuming libraries that do.

[agentgt]

@Mooninaut is right that a good portion of the checkNotNull in the world are hard coded in some systems and for good reason.

For example in Eclipse:

@Nullable Object o = ...;
Objects.requireNonNull(o); // no assignment back to o
out.println(o.toString()); // Eclipse and most know that o is now nonnull.

Ditto for assert.

But if you write your own requireNonNull it does not work (well unless you do assignment back).

For other use cases I'm not sure I understand other than general bug prevention which seems out of scope for JSpecify.

[cpovirk]

I agree that most of the value is tied up in recognizing very common methods like Objects.requireNonNull so that examples like #226 (comment) work.

After that, the next most important thing is likely the ability to specify that com.mycompany.Checks.throwIfNull should be treated similarly. (As discussed above, this ability already exists in NullAway and in the Checker Framework. We might not have yet mentioned the similar Kotlin feature, contracts, which I believe is still experimental.) I don't personally have a feel for exactly how important that is: Even if you need 3 different tools to recognize your com.mycompany.Checks.throwIfNull method, it's still not necessarily intolerable to have to write 3 different annotations on it, given how rarely this comes up in comparison to annotations like @Nullable. Plus, it's worth remembering that mere annotations are unlikely to handle cases like assertThat(foo).isNotNull() or checkState(foo != null) (1, 2), and so there may always be a place for hard-coding of particular APIs and call patterns.

The alternative use case that I was discussing in #226 (comment) would have some value to the migration we're currently doing. But it's likely that we can get a lot of the value there by hard-coding specific APIs, too. Now, if we envision a future world in which lots of people need to automatically update lots of Kotlin code to "suppress" its nullness errors, then there might be more cause for an annotation for that use case. But it's possible that we can still get most of the value from hard-coding, and we may be able to get some of the remaining value from analyzing the source code or bytecode of the methods to identify those that obviously throw NPE for a null input.

[agentgt]

I can't decide if this is tangental or relevant as I'm less familiar with this area but many of the checkNotNull / requireNonNull vary on annotations so I guess I see value here on that regard.

See checker unlike most others has Objects.requireNonNull as a @NonNull parameter. The idea being that it is just an extra check like an assert. This is partly because checker wants to avoid NPE a little too aggressive in my opinion as you might just be replacing NPE with some other exception.

I and I think many others use requireNonNull as a casting mechanism as it is more or less the only builtin JDK option for doing something like that. I think Checkers argument is very valid though. (btw IIRC the jspecify jdk is annotated @Nullable for this).

I guess what I'm getting at or realizing is that there or more use cases and interpretations of these kinds of methods:

1. casting - edge or boundaries... it could be null and we want to fail with the most obvious exception (we also want the checker to move on and be happy... sort of like removing the parameters from a generic). One argument against these guys is they should not be throwing NPE.
2. asserting - It should be nonnull and you are just doing defensive programming. The argument against these guys is unlike range checks in arrays nullity can be proven at compile time.
3. contractual - you might even be expected to catch the NPE or some other exception

The last one I consider pretty fringe. I guess my question is what group is under discussion here for say google's (insert other ... I don't know kotlin that well)?

My repeating concern of JSpecify and in general is consensus on annotating libraries because arguably even JSpecify could make requireNonNull @NonNull.

[cpovirk]

I don't know if this will serve as much of an answer, but maybe it gives you an idea of where at least one person's head is.

I've found it clarifying to have multiple nullness analyzers in mind. (I think I've heard it said that you don't have a standard unless you have multiple implementations :)) Google uses a few in different places, but the ones I'm most familiar with are the Checker Framework and Kotlin.

One thing that's stuck out to me about Kotlin is the idea that nullness-augmented types can be made to be "real runtime types": If you have a Kotlin function that declares a non-null parameter, then the Kotlin compiler will automatically insert a runtime check at the beginning of that method's implementation, throwing NullPointerException if it sees null. (Compare to how the JVM will give you a ClassCastException if you manage to sneak the wrong kind of object into a method parameter.) As a result, if you want Java's requireNonNull to be able to throw a NullPointerException with the message you provided (instead of the automatic NPE with a generic message), or if you want JUnit's assertNotNull to be able to actually throw an AssertionError (instead of the automatic NPE), then you'd need to declare the parameter as having a nullable type—if it were written in Kotlin, or if you applied bytecode rewriting to add automatic null checks to Java (as at least one plugin does), or if a future version of Java were to insert such checks for any built-in nullness support it might have. (And even today, Kotlin makes it very difficult to pass null even to a Java method that is annotated as not allowing it.)

(Given that, and given a few historical discussions (which include discussion of your "casting" use case), I'm comfortable stating that requireNonNull will keep the @Nullable annotation that we currently have on it.)

Compare also similar cases in which null is not always safe, like Collection.contains(null). The Checker Framework philosophy is to make the parameters as non-nullable to avoid NPE; the Kotlin philosophy is to make them as nullable so that you can pass null in the cases in which you need to. (This would probably fit into your group 1, including the part about how they arguably shouldn't throw NPE at all.)

And yes, group 3 is pretty weird—things like "This Comparator should throw NPE so that code like AbstractSet.equals can catch it."

One way to support both tools better is to support #113 in the future. Then we could say that a method like Collection.contains has a @Nullable type but might still throw if you pass null, and tools can respond accordingly.

[cpovirk]

(more on some of those topics in https://github.com/jspecify/jspecify/wiki/nullness-borderline-cases and in the nullness design FAQ under "How are we supposed to eradicate NullPointerExceptions if even a method with all nullable parameters is still allowed to throw it?.")

[cpovirk]

Dumping one other note for the future:

Caveats:

• This is a different use case.
• We hope that we can continue to address that use case in a different way for a long time.
• We still don't know whether we'll ever add the annotation under discussion here.

One unfortunate fact about the Java Collections API is that sometimes we have methods like Collection.contains(@Nullable Object e), for which many implementations tolerate null inputs (including by returning false if the implementation doesn't support nulls) but some throw NullPointerException. Our approach to that so far has been to annotate Collection.contains as above but to annotate overrides of that method as @Nullable or not to express whether they throw an exception or not. [edit: But even that's not enough for full understanding of classes like TreeSet, whose support for null depends on the specific Comparator, whose type argument we sometimes can see in the type argument for the TreeSet and which we couldn't make use of without not just receiver-parameter type arguments but probably also @PolyNull, as in "boolean contains(TreeSet<@PolyNull E> this, @PolyNull Object obj)?"]

(IIRC, there is another complication here, which is that some implementations don't override all the relevant methods themselves, so there is sometimes no method for us to annotate. Oh, and plus, users often declare a field or local variable to hold a general type, like Collection or List, rather than the specific one with the more precise annotations (though there are exceptions, like ConcurrentMap). But setting that aside....)

This works because, even though checkers are likely to produce errors for an override contains([@NonNull] Object e), users can suppress those. (Or they can just not use a nullness checker on that code.)

(Hmm, I'm suddenly remembering that there was also a philosophical discussion about all this :))

But we can imagine cases in which a language might be stricter about such things. If so, we'd really like for the superclass and subclass to agree. And "clearly" they need to agree on @Nullable.

But then users of the null-rejecting subclasses get no protection against NPEs.

So what if we were to annotate them as contains(@ThrowsOnNull @Nullable Object e)?

But would that even help most users? If we expect users to want to pass nullable values to other methods that are annotated in the same way (like checkNotNull), then it's unlikely that users will want to see errors for such calls. And thus they still won't get errors for dangerous calls to contains. [edit: And this still doesn't help with TreeSet, discussed above.]

So I think this goes nowhere. But I wanted to write it down while it was fresh in my mind.

[cpovirk]

(Also, note that this annotation would be insufficient to accomplish another goal that tools might have: Tools like the Checker Framework like to annotate methods like Method.invoke to require a non-nullable "receiver," since that parameter is sometimes required to be non-nullable. We've discussed (somewhere?) that it might be nice to have an annotation @PassingNullForANullableParameterNeverLeadsToANullPointerException (and/or perhaps finer-grained annotations along those same lines). Then the Checker Framework could still produce an error for passing null to a @Nullable unless it found that annotation. Anyway, the point here is that @ThrowsOnNull would not accomplish that goal because Method.invoke does not make that promise.)

[Mooninaut]

@cpovirk I wonder when we hit diminishing returns on finer and finer-grained single-purpose annotations and increasing returns on @Contract (or something like it).

Regarding the difference between contains and null-check methods, I think there's a difference in intent and usage which justifies different tool behavior.

Annotating an API method that it throws if parameter X is null allows static tools to warn against passing nullable values. The information flows from the tool to the programmer.

Annotating a null-checking method that it throws if its parameter is null effectively casts the parameter value from nullable to non-null, suppressing further nullness warnings on that value. The information flows from the programmer to the tool.

While the runtime effect of calling either method with null is the same (NPE), the use cases are different. I don't want a nullness warning/error on a null checking method (unless the value is statically always null), but I do want one for the API method.

To give absurdly verbose names, we want @WarnUserThatCallingWithNullWillThrowNPE and @KnowThatParameterValueIsNotNullAfterThisMethodReturns. Whether that should end up looking like @ThrowsIfNull and @CheckNotNull, or @ThrowsIfNull(warn=true) and @ThrowsIfNull(warn=false), I couldn't say.

[kevinb9n]

@cpovirk I wonder when we hit diminishing returns on finer and finer-grained single-purpose annotations and increasing returns on @Contract (or something like it).

#454
There may be stuff about this I couldn't find to link in. Didn't find an existing issue dedicated to it.

[netdpb]

Current decision: This feature is not required for JSpecify 1.0.

Proposal for 1.0: Finalize the current decision. If you agree, please add a thumbs-up emoji (👍) to this comment. If you disagree, please add a thumbs-down emoji (👎) to this comment and briefly explain your disagreement. Please only add a thumbs-down if you feel you can make a strong case why this decision will be materially worse for users or tool providers than an alternative.