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

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 https://github.com/jspecify/jspecify/issues/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.

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.

(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.

https://github.com/jspecify/jspecify/issues/309#issuecomment-1301198808 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 https://github.com/jspecify/jspecify/issues/309#issuecomment-1307390787, in which maybe I can see something that the exception type could give some tools, arguably, someday, maybe?]

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.

I agree that most of the value is tied up in recognizing very common methods like Objects.requireNonNull so that examples like https://github.com/jspecify/jspecify/issues/226#issuecomment-1674839970 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 https://github.com/jspecify/jspecify/issues/226#issuecomment-1650287729 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.

@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 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.

1. 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.

1. 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.)

(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.)

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.

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).