JSpecify and annotated packages option

[msridhar]

Once we land support for @NullMarked, it seems the AnnotatedPackages option would no longer be absolutely necessary. If we end up adding a flag for "JSpecify mode", we could say that at least one of the JSpecify or AnnotatedPackages options should be given (and giving both would of course be supported). We could instead just make AnnotatedPackages optional, but I'm concerned that could lead to confusion for users who are also not using @NullMarked.

[bannmann]

I started adopting JSpecify annotations in a 20K LOC code base. In line with the recommendations in the JSpecify user guide, I planned to annotate one package after another, adding @NullMarked to each package once I finished it.

Having learned that NullAway does not yet support @NullMarked, once I finish annotating a package, I will now add it to the AnnotatedPackages option in addition to flagging the package itself as @NullMarked. The eventual goal would of course be to put @NullMarked on the module level.

Regarding configuration, I share @msridhar's concerns about just making AnnotatedPackages optional.

I suggest adding a second option to control this behavior. It could be called e.g. NullMarkedMode and its values would look something like this:

• UsePackageAllowList makes NullAway require the AnnotatedPackages option, just like today (the default value)
• OnlyAnnotatedCode limits NullAway to those packages / modules that have JSpecify @NullMarked annotations. The AnnotatedPackages option would not be required.
  • Whether that mode can be further restricted by AnnotatedPackages is up for debate. Personally, I don't see a point in that and would want to avoid the confusion by having AnnotatedPackages throw an error if it's used together with this mode.

[msridhar]

@bannmann NullAway should support @NullMarked and @NullUmarked now! Can you open a separate bug if you're seeing that it's not supported? The only place where support likely won't work yet is on modules, but I would expect packages to work.

[msridhar]

Regarding your suggested configurations options @bannmann I like them! We are going to have a messy and probably somewhat lengthy transition over to JSpecify checking, with an unfortunate amount of configuration, in order to not break existing users. I think your options fit well with such a transition plan. If, in your experimentation, it would be beneficial to have a flag that forbids AnnotatedPackages so NullAway relies entirely on @NullMarked, let us know and we can try to add it.