Adoption of JSpecify annotations in Guava

[cpovirk]

[note to self: See also Google-internal issue 192446998.]

(We'd spoken a while back about filing issues in the JSpecify tracker for some tasks that other projects would take but that have interdependencies worth tracking here. Here's one such issue.)

Currently, Guava is annotated with a combination of jsr305 annotations (both jsr305's built-in nullness annotations and Guava's custom "nicknames" built on jsr305) and Checker Framework annotations. For the most part, tools don't care too much which nullness annotations a project uses, but there's at least one big exception, which is Kotlin.

The annotations we've chosen have the advantage of mostly producing errors in Kotlin by default: Both the built-in jsr305 nullness annotations and the CF annotations do. The caveats are:

• Our CF annotations appear only in "type-use-only" locations and thus currently have no effect until users set -Xtype-enhancement-improvements-strict-mode.
• Our custom "nicknames" [edit: I think I might mean our custom @TypeQualifierDefault annotations, all of which are named "@ElementTypesAreNonnullByDefault"] currently produce only warnings until users set -Xjsr305=strict.

With JSpecify annotations currently producing only warnings for Kotlin users, the ideal first step (as soon as the JSpecify annotations are "stable enough" that we're comfortable) would be to add @NullMarked to our annotated classes while leaving the existing annotations in place. This would let users who opt in to -Xjspecify-annotations=strict (and additionally opt in to -Xtype-enhancement-improvements-strict-mode [edit: or maybe that's not necessary]) see Guava as almost completely annotated. [edit: Or would it be "overridden" by @ElementTypesAreNonnullByDefault or vice versa? But again, both flags are currently warning-only.] Aside from that, it may be a no-op for Kotlin users (I'd have to think more to confirm that), though it may help users of other tools by then.

Later, once JSpecify annotations produce errors by default in a Kotlin release (and that release is out for long enough that we're comfortable relying on it), we could remove the other annotations, replacing them with JSpecify annotations where necessary. In particular, we could remove one kind of jsr305 nickname that forces Kotlin users to still see platform types, even if they've set all the applicable flags.

[cpovirk]

(We think we can do this without needing a GWT module: We already strip @Nullable annotations from our GWT sources, and we should strip @NullMarked annotations (per this comment that refers to its predecessor @ElementTypesAreNonnullByDefault) for as long as we strip @Nullable (thereby sidestepping any problem that might exist for the @Target({MODULE, ...}) line in NullMarked).)

[cpovirk]

I should note that Guava's transitional @ParametricNullness annotations (which we'd hope to be able to avoid someday, since they'd be technically redundant after we're fully on JSpecify annotations) have been getting used by various tools, so we may want to keep them around longer. See this discussion with the NullAway folks and this comment in the annotation's source, for starters.

I know I've done at least one other experiment that relied on @ParametricNullness. That resulted in https://github.com/google/error-prone/commit/941974e5c658ef0164e90367cacee137112b787b. Now, Error Prone doesn't rely on the annotation on an ongoing basis. But it's worth noting that @ParametricNullness remains at least periodically handy, especially until we can deal with JDK-8225377.

[cpovirk]

A user inside Google just noticed that IntelliJ's support for JSpecify annotations turned on by default recently. The user reports some resulting false positives in some generics-heavy code. That's expected, and the question is just how widespread such false positives will be. We'll keep an eye out for more reports, and we can use those reports as input for the decision about which annotations to use in Guava when.

[cpovirk]

Hmm. To recap:

• We're using the JSpecify annotations for Guava internally.
• We're rewriting them to other annotations externally for now.

So: I wonder if some of the new IntelliJ Java checking for JSpecify annotations was already happening for other annotations for our external users. If so, then there would be no impact for IntelliJ Java users if we switched to JSpecify externally. It's probably not quite that simple, but it might be that the change would not be as significant as I'd initially thought.

[cpovirk]

In https://github.com/jspecify/jspecify/issues/24#issuecomment-1509090335, I mention another reason to stick with declaration annotations for now: Type-use annotations on arrays don't trigger kotlinc errors, only warnings. (That is the case even for people who set the flags to otherwise promote nullness warnings to errors.)

That bug may well be fixed [edit: happening in Kotlin 2.0.20] before we'd even be considering migrating fully from declaration to type-use annotations, anyway.

[cpovirk]

Hmm, I should probably also test what happens if users use a JSpecify-annotated Guava wihout enabling -Xtype-enhancement-improvements-strict-mode: Would Kotlin treat all our type arguments and array elements as non-nullable, since they appear in @NullMarked code but Kotlin might be ignoring any @Nullable arguments that appear on them? I would hope not, but I would want to check.

If there were a problem, it would at least not lead to outright errors (neither at runtime nor at compile time), since JSpecify annotations produce only warnings by default. (And if a user is willing to opt in to making JSpecify-related warnings into errors, then it could be inconvenient but ultimately reasonable to have to ask that user to also set -Xtype-enhancement-improvements-strict-mode.) The bigger concern (relevant to #24) is what would happen when JSpecify-related warnings become errors by default.

[cpovirk]

Good: The following works fine with -Xjspecify-annotations=strict, regardless of whether I also pass -Xtype-enhancement-improvements-strict-mode:

val f: Function<Any?, String> = constant("")

Interestingly, if I change Any? to Any (and continue to pass -Xjspecify-annotations=strict, I get a failure not only with -Xtype-enhancement-improvements-strict-mode (good) but also without (probably also good, just not sure if I would have expected it).

[cpovirk]

Note also that Guava recently started using @NonNull in a few places. We'd want to wait for Kotlin support for the JSpecify @NonNull before switching to JSpecify. [edit: That support landed in Kotlin 2.0.0.]

[cpovirk]

ascopes reports problems when building Javadoc against JSpecify, at least under certain settings: https://github.com/maxcellent/javadoc.io/issues/182

I'd need to read more to understand whether there is anything we can fix on the JSpecify side. At first glance, I get the impression that Guava (and other motivated consumers) could work around it with -linkoffline, which Guava already uses.

[cpovirk]

It's looking like IntelliJ always treats JSpecify annotations as producing warnings only, even if we add -Xjspecify-annotations=strict to the Kotlin compiler flags in its settings. We should see if that changes immediately when -Xjspecify-annotations=strict becomes the default (probably?) or if it requires a subsequent IntelliJ release.

[edit: Note also that we've seen a rare few cases in which kotlinc produces errors with -Xjspecify-annotations=warn but not with -Xjspecify-annotations=strict, IIRC. I'm not sure of the exact relevance of that here...]

[cpovirk]

https://stackoverflow.com/q/77915170/28465 suggests that Guava's current nullness annotations (perhaps specifically its usages of @CheckForNull) are not recognized by Eclipse, at least by default.

My suspicion, though, is that most nullness annotations are not recognized by Eclipse by default. The thing I'd have to look into is whether Eclipse nowadays lets you specify multiple annotations to treat like @Nullable. Apparently, many years ago, you could pick only one: 1, 2. I must have seen what the UI was when I experimented a few years back, but I don't remember offhand. It's possible that the answer exists somewhere in https://help.eclipse.org/latest/index.jsp?topic=%2Forg.eclipse.jdt.doc.user%2Ftasks%2Ftask-using_null_annotations.htm.

If Eclipse still supports only one annotation, then the main takeaway is that switching to JSpecify may improve things for Eclipse users: At least then, we'll consistently use the same annotation for the same thing (instead of mixing @Nullable and @CheckForNull). And of course the goal is that ultimately more tools recognize JSpecify annotations by default.

[cpovirk]

Oops, I should have waited until I clicked that final link on the Eclipse site... :)

The compiler supports exactly one primary set of annotation types for null specification. Additionally, an arbitrary number of secondary annotation types can be configured to carry the same semantics. Secondary annotation types are supported for the sole purpose of interfacing with 3rd party code that is already specified using other null annotations than the primary annotations types of the current project.

So multiple annotations are supported nowadays.

[cpovirk]

My impression from the recent activity on KT-59138 (and some quick testing) is that Kotlin 2.0 [edit: now deferred until at least 2.1.0] is going to start treating types like SettableFuture<String?> mostly the same as it currently treats SettableFuture<String>, at least until we're able to use the JSpecify annotations on them and rely on Kotlin to recognize those.

For example, today, code like this produces an error:

fun go(f: ListenableFuture<String?>): String = f.get()

Ditto for this slightly more complex code:

fun go(m: Multimap<String, String?>, s: String): String = m.get(s).iterator().next()

But with K2, neither of those will be an error anymore.

Granted, K2 still produces an error for this similar code, perhaps from magic in its handling of Collection?

fun go(m: Multiset<String?>): String = m.iterator().next()

So I don't know how widespread the impact of the change would be for Guava types.

I'm also not sure how much we can do about it until we're ready to use exclusively JSpecify annotations: Even though it's possible that we're at the point that we could use @NullMarked as a supplement to our existing nullness annotations, my fear is that its "warnings-mode" behavior would override (rather than supplement/enhance) the behavior of our JSR-305 defaulting annotations—which, admittedly, is also warnings-mode but which perhaps more users have upgraded to error-mode? Additionally, I think our @ParametricNullness annotations would undo much of the effect at the moment (though perhaps not all, like maybe helping in my Multimap example??). (In fact, I suspect that they're already preventing users from getting errors like the ones above in some cases.)

[cpovirk]

This is a minor thing (and not specific to Guava), but:

I get the impression that type-use annotations show up in the Summary section of rendered Javadoc but that declaration annotations do not. See, e.g., Equivalence, which shows onResultOf​(Function<? super F,​? extends @Nullable T> function) but doEquivalent​(T a, T b) (rather than doEquivalent​(@CheckForNull T a, @CheckForNull T b) or eventually doEquivalent​(@Nullable T a, @Nullable T b)).

The theory would be that seeing the nullness annotations in the summary is superior to having to look for them in the details, but in fairness, they can be noisy (worsened by https://github.com/google/guava/issues/6790). Admittedly the mix of sometimes showing them and sometimes not showing them may be the worst of both worlds.

[cpovirk]

A few things (about Kotlin unless otherwise noted) that I researched/tested today (most of which I was aware of but some of which might have been new):

• @CheckForNull and the Checker Framework @Nullable produce errors by default when used on return types; the JSpecify @Nullable, only warnings for now.
• There seems to be only one default "in effect" at a time: If we have @ParametersAreNonnullByDefault on the package and @NullMarked on the class, then Kotlin produces only warnings for null arguments passes for non-null parameters, even with -Xjsr305=strict, unless of course we set -Xjsr305=strict.
• @ParametersAreNonnullByDefault has an effect only with -Xjsr305=strict, as of course do our custom @ElementTypesAreNonnullByDefault annotations.
• J2ObjC still doesn't recognize @NullMarked by default, but that likely matters only internally and perhaps doesn't matter a ton to begin with. (I think that J2ObjC will still recognize a package-level @ParametersAreNonnullByDefault even if there's a class-level @NullMarked, at least if J2ObjC isn't configured to recognize @NullMarked, but I didn't confirm this.)
• The Checker Framework checker-qual release does include a module-info at this point.
• I released a version of Truth with JSpecify annotations last week. We've been using it internally for a while, but this is another chance to shake out any problems in the outside world.

I'll try to synthesize that into a proposed plan, maybe as soon as later today.

[cpovirk]

Here's my 4-phase proposal for comment by @netdpb and others. I've written it mostly from the perspective of users of Kotlin, since Kotlin has the most complete JSpecify/nullness support of tools in common use, but I'm taking into account what I know about other tools.

We could implement Phase 1 and Phase 2 today, or we could wait until JSpecify 1.0.0 or some other time of our choosing.

Phase 1: Replace @*AreNonnullByDefault with @NullMarked

This lets Kotlin produce warnings for code like ImmutableList<String?>. Those warnings may identify runtime problems, and they're a helpful transitional state on the way to when Kotlin upgrades the findings to errors. (Users can then upgrade to errors early with -Xjspecify-annotations=strict.)

Risks:

• Users see warnings (or even errors in rare cases) that they might not want to deal with right now. (To spread that change across time, we could in theory adopt @NullMarked package-by-package or even class-by-class. But my guess is that it's better to start slowing the bleeding for all of Guava now.)
• Users "need" a new dependency. (In practice, they can often get by without it—but not always. See also #294.)
• Users who already set -Xjsr305=strict no longer see errors in some of the cases they were used to, only warnings. (The solution to that is for anyone who already sets -Xjsr305=strict to also set -Xjspecify-annotations=strict, which is unlikely to affect many existing libraries other than Guava.)

Phase 2: Remove JSR-305 magic from @ParametricNullness

This lets Kotlin produce warnings for code like Futures.immediateFuture<String>(null). That's good and bad in the same ways as in Phase 1.

This can't happen before Phase 1 because @ParametricNullness undoes the unwanted part of the effects of @*NonnullByDefault. It could happen as part of the same release as Phase 1, but I'd probably instead publish 2 separate releases on the same day so that users can choose between picking up the changes incrementally and picking them both up at once.

Phase 3: Replace JSR-305 @CheckForNull with Checker Framework @Nullable

This is the final step to removing our JSR-305 dependency (which, among other things, is one of the blockers to making Guava a module).

This can't happen until after a bug fix in Kotlin 2.0.20 is adopted widely enough. (Realistically, we probably could do it sooner, since I don't think we have many APIs that return nullable arrays (example).)

Phase 4: Replace Checker Framework @Nullable with JSpecify @Nullable

This is the final step to using a single set of nullness annotations that provides all the information needed by Kotlin without need for compiler plugins.

This can't happen until enough Kotlin users adopt a future Kotlin release (2.1.0?) in which JSpecify annotations produce errors by default, as Checker Framework annotations do already.