What if a tool provided an option to check only @NullMarked code?

[cpovirk]

(prompted in part by #127 (comment), but I'm not claiming that Lázaro was proposing this)

One important feature of JSpecify is that it is designed to be possible to run a nullness checker on unannotated code and get useful results -- some errors from the nullness information that is available (from annotated dependencies or usages of null literals) but not errors for every method that, e.g., should someday have a @Nullable annotation on its return type.

Another important feature is that it's possible to sprinkle annotations across a codebase without first making the entire thing pass nullness checking.

Nevertheless... code that is run through a nullness checker is much more likely to be correctly annotated.

Plus, configuring a build to apply nullness checking to exactly the right set of files can be annoying.

It's easy to imagine, for example, that someone might enable nullness checking for a codebase, start to put @NullMarked on packages, and then respond to nullness errors in those packages by adding @SuppressWarnings("nullness") to some classes. This leaves behind classes that are in the scope of @NullMarked but probably don't have correct nullness information.

So: Would it be reasonable for a tool to offer, hopefully in addition to its normal behavior (of checking all given code, all code that matches a given pattern, etc.), a mode in which it checks only code that is in the scope of a @NullMarked annotation (and, presumably, not negated by a @NullUnmarked annotation)? This would nudge users toward running the checker on any code that they make a serious attempt to annotate, and it would encourage them to put @NullUnmarked (rather than just a suppression) on sections that they choose not to seriously annotate.

Is this even "a JSpecify question?" I'm not sure:

• One argument says that it's not our business to say what code a nullness checker would run on: That's configured separately. Our job is just to specify types.
• The other argument says that... our job is just to specify types. If tools interpret @NullMarked as an instruction to check code (if they're running in that mode), then they're assigning meaning to our annotations that they aren't meant to have.

Opinions?

[edit: much later, a proposal of such an option]

[msridhar]

This is an interesting point. NullAway has concepts of "excluded" and "unannotated" source classes (admittedly not carefully-chosen terms). If a class is "excluded," then we do not check it for nullability errors, but we treat its API as @NullMarked. If a class is "unannotated," then we do not treat its API as @NullMarked, and we also do not check it for nullability errors. NullAway currently does not have a mode where we check a class for nullability errors but do not treat its API as @NullMarked. We've never seen a need for that, but I guess other tools might.

I personally prefer the tool behavior of not doing nullability checking inside @NullUnmarked code, and I expect that NullAway will always behave in this manner. For a class that a user does not want to worry about yet in terms of nullness checking, it seems annoying / confusing to have to both write @NullUnmarked and also @SuppressWarnings("nullness"). I don't know if JSpecify needs to prescribe this behavior. Is the current internal JSpecify checker behaving otherwise?

It might be interesting to consider the variant that NullAway already supports, skipping checking for certain @NullMarked classes. NullAway sometimes uses this for generated code, where the generated APIs are fine but the generated implementation has issues. I would not say this is a high-priority issue for JSpecify though.

[cpovirk]

Thanks!

To answer your question about the checker we're using inside Google: Checking and annotating code are currently completely independent. So it's possible to check code without annotating it and vice versa. In practice, we have code in the "annotated and checked" bucket and code in the "annotated but not checked" bucket (and probably almost all of that second bucket is only partially annotated, aside from the generated-code case you mentioned) -- and of course lots of code in the "neither annotated nor checked" bucket -- but a very small amount in the "checked but not annotated" bucket.

I have wondering if "checked but not annotated" will be more useful in the future, but I haven't been placing a lot of hope in that. Theoretically, it could make it easier for us to flip checking on by default for our depot. And even before turning on full checking, I could imagine some kind of more conservative checking that we'd try to enable for the whole depot, even if only one-off checks more like EqualsBrokenForNull.

[msridhar]

Running one-off checks like EqualsBrokenForNull on code that isn't annotated seems reasonable to me. From a JSpecify standpoint, IMO we can see how these things play out a bit with real-world tools before recommending an option to check only @NullMarked code.

[cpovirk]

I've belatedly thought of more precedent for coupling checking and annotating: the Checker Framework.

The Checker Framework does something similar but in the opposite direction: If you enable checking, then the Checker Framework's modified javac writes inferred annotations to the generated bytecode.

We don't plan to go that direction with JSpecify because we don't want for the same code to be treated differently depending on which compiler it was built with. Nevertheless, this is another case that demonstrates how users may be used to coupling checking and annotating.

[kevinb9n]

• The other argument says that... our job is just to specify types. If tools interpret @NullMarked as an instruction to check code (if they're running in that mode), then they're assigning meaning to our annotations that they aren't meant to have.

I think this is the right general point; we "don't want" tools to treat our annotations as meaning anything other than what we say they mean, and will try to discourage them from doing that somehow.

In this case maybe it's reasonable though. "I see there {will/won't} be a critical mass of usable information in this code, so I {will/won't} analyze it....."

[cpovirk]

(Thanks, the "critical mass" phrasing expresses that point of view well.)

I remembered another benign(?) possible case case for "assigning meaning to our annotations that they aren't meant to have": Past discussions have touched on the idea that some users may want tools to enforce the rule like "All classes in this directory must be @NullMarked." The question then is what should be done with classes that aren't @NullMarked yet. One possibility is simply to add @SuppressWarnings("ShouldBeNullMarked") or whatever. Another possibility is to say that @NullUnmarked is another way to suppress the warning. After all, it calls attention to the problem, too. And it fits well with the act of using @NullUnmarked on smaller scopes (if we support that).

This would mean that tools act differently when they see @NullUnmarked than when they see code that is implicitly not null-marked. I think that's probably OK -- though maybe I should be worried that users would want for tools to report the annotation as redundant! But if we talk ourselves into thinking that that would be OK, then we would arguably be taking the tiniest of steps toward saying that it would be OK for a tool to check only @NullMarked code.

[cpovirk]

One other thing that I'd forgotten was to connect this proposal to the problem of package-level @NullMarked and split packages. That problem, again, is: If you put @NullMarked in your production code's package-info, that already applies to tests -- in the limited sense that a nullness checker run over your tests would see most parameters as non-null by default, etc. But if a tool were to implement this proposal we're contemplating, then the nullness checker would actually run over those tests, and you'd likely see errors because you probably haven't annotated all your test code yet.

Now, different projects will have different opinions on whether they're ready to start annotating and checking their tests. But setting that aside, the main point is that we'd be making package-level @NullMarked, which is already surprising, become even more so. (And of course some users will find the idea that @NullMarked enables nullness checking to be surprising on its own!) Of course, part of my takeaway from that is that we have yet another reason to consider avoiding package-level annotations :)

[cpovirk]

Another thing to consider for further down the road, when users can realistically expect their build tools and the IDEs to come with extensive support for JSpecify's feature set:

Someone who is adopting nullness checking incrementally would be happy to be able to share configuration for that checking across tools. After all, no one is going to be excited to update both a build configuration and an IDE configuration whenever it's time to enable checking for a new class. If tools were to recognize @NullMarked as a way to enable checking, we'd go from a 3-part update (annotate, configure build, configure IDE) to a 1-part update (just annotate).

I worry that that's actually too convenient and that it will lead users to not run nullness checking on unannotated code at all. That wouldn't be the end of the world, but it could be sad for a lone @NullUnmarked method in a @NullMarked class to lose out on some easy checking. One way around that is to provide a second @RunNullnessChecking annotation. But that loses some of the convenience that comes with using @NullMarked, and it takes us clearly away from the principle that "We're just specifying types." So I kind of still like having the option to use @NullMarked for this. But I could imagine that some tools may provide only that behavior or at least strongly push users in that direction. So this may end up being a consequential decision, and I don't mean to sound too confident about it.

[cpovirk]

It sounds like @Nullsafe may contain configuration for both annotated-ness and checked-ness, if I'm skimming its Javadoc and #35 (comment) correctly.

[kevinb9n]

I have no issue with a tool deciding to check only null-marked code, or have an option for checking only null-marked code.

And I definitely don't think we should need to worry about a possible @YoCheckThis annotation. Some tool might introduce one. If multiple start wanting it we should talk then.

Closeable?