jspecify: The signatures of `{require,check,verify}NonNull` [working decision: nullable, but see #226]

It will be helpful to users for JSpecify to state, as an example, correct types for methods like requireNonNull and verifyNotNull.

I propose that these methods take a @NonNull formal parameter and return a @NonNull result. The reason for this is that in a correct execution of the program, null never flows to these methods.

(This is a discussion about the specification, not about the behavior of any tool. Specific tools may choose to treat these methods specially, such as not issuing warnings for uses of them that may lead to a NullPointerException.)

About this issue

Original URL
State: closed
Created 3 years ago
Comments: 15 (2 by maintainers)

Most upvoted comments

A lot of the discussion that had been insisting they be non-nullable turned out to be thinking of a different method, castNonNull, which is not in the set we’re talking about here

Not sure about this characterization unless I missed something, since I believe castNonNull/castToNonNull is the one case that was always generally agreed to be taking a @Nullable argument (because it acts as a type cast, which is already an escape hatch from sound static typing).

That said, this doesn’t change the resolution. The agreement is that for {require,check,verify}NonNull the annotation of the parameter is @Nullable with an extra specification that they are supposed to fail at runtime on any null value (#226).

lazaroclapp on Feb 2, 2022

Thanks @Mooninaut and sorry we didn’t respond yet. Your 3 categories correspond to these types (using String as example):

String - definitely non-null
NullType - definitely null, continues to be non-denotable
@Nullable String - String U NullType

I think checkers will be able to track “definitely null” for purposes of issuing “redundant null check” warnings, but I do want to classify that as a lesser type of warning/error than actual type errors, for what that’s worth. Overall I don’t think we worry much about it.

I also came to the conclusion that we’re going to need a special annotation to use with methods like requireNonNull.

Specifically, this would be a parameter annotation that declares, “this method promises not to complete normally if this parameter is null”. This is what would allow checkers to “learn” about the non-nullness of a ref-transparent expression below the point where that expression is passed to requireNonNull etc. And that’s useful/important.

Fortunately, if these methods require a specialized marking, that takes the pressure off this particular issue/question. I will maintain that the parameters are still very much nullable in this scenario. (A lot of the discussion that had been insisting they be non-nullable turned out to be thinking of a different method, castNonNull, which is not in the set we’re talking about here.)

But, the new issue I’m gonna file for the annotation can encompass this nullable question, so I think we’ll be closing this one soon.

kevinb9n on Jan 19, 2022