Feedback with Spring Framework codebase

[Sebastien Deleuze]

Hi,

As discussed recently, I would like to create an up-to-date experimental branch of Spring Framework using JSpecify annotations instead of JSR 305 in order to provide hopefully meaningful feedback before a potential future new release of JSpecify. I think we did that with a very early version of JSpecify, but that makes probably sense to perform this exercice again with the latest progresses.

I am wondering:

 - If I should use 0.3.0 artifacts available on Maven Central or a custom build of JSpecify main branch

 - What is or are the recommended Gradle plugins to check null-safety consistency accros Spring Framework code base (currently we don't have such build time check)

Best regards,

Sébastien

[Chris Povirk]

Hi, Sébastien,

That sounds great!

You should be able to use the 0.3.0 artifacts. They contain the same annotations as we currently have at head on the main branch.

For a nullness checker, I wouldn't say there's a single obvious choice at this point. In your position, I would probably try NullAway for your experiment and then reevaluate once you have some experience. My thinking:

• Our reference checker is currently inconvenient to run. Even after it becomes convenient to run, it will remain experimental (which might be OK for your case). We're working on it, but I wouldn't recommend the checker for now unless you try others first and find that they don't fit your needs.
• The Checker Framework performs thorough checking even for code that uses generics and JDK APIs. (And if you configure its Gradle plugin to use the eisop version, you'll get support for the slight differences in the meaning of generics in the scope of @NullMarked.) However, it's also very strict, even in ways that don't often catch bugs. You can undo some of that by passing -AassumeInitialized and -AassumePure and by passing some common error kinds to -AsuppressWarnings=.... But it remains more strict than most alternatives.
• NullAway doesn't understand generics much yet, but it's a lot faster and less strict, while still catching many problems. It might make a good tool to try first, especially for an experimental project. It provides Gradle integration through an Error Prone plugin. (Error Prone is itself great, but you may end up wanting to configure it to disable its main checks so that you can work straight on nullness :))

We of course have some Checker Framework and NullAway developers in the group who may want to chime in :)

With any of the checkers, you may want to enable them even before you switch to JSpecify annotations to see what you're in for. (I think they'll all recognize your existing @Nullable and @NonNull annotations, and they can be made to assume behavior similar to @NonNullApi by default.)

[Manu Sridharan]

Hi Sébastien,

Just wanted to chime in and say that if you give NullAway a shot, we would be very happy to get your feedback and to try to improve the tool for your use case!  As Chris notes below, our support for generics is not really “there” yet, which may cause some pain.  My hope is that the situation will be at least somewhat improved in the next few months and we’ll have some kind of limited but usable support.

Best,

Manu

--
You received this message because you are subscribed to the Google Groups "jspecify-discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to jspecify-discu...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/jspecify-discuss/CAEvq2nr83y9h_imCAPr-_1_n9%3DYv16neWcmPBHUHc0qw12oLZA%40mail.gmail.com.

[Werner Dietl]

Hi Sébastien,

Chris provided a great summary.

I'm happy to help if you want to try EISOP. Besides the better `@NullMarked` support, EISOP provides `-AassumeInitialized` to turn off initialization checking.

It is strict, but there are many options to focus your attention only on certain files/packages.

There is still some work to do for full JSpecify compliance, but the current implementation should already work for a strict interpretation of JSpecify.

Best,

cu, WMD.

To view this discussion on the web visit https://groups.google.com/d/msgid/jspecify-discuss/CAFXXopMqrM5FoO%2B%2Bj49tVLC0U5OnBmD8j3VYJxON62EazVFKTA%40mail.gmail.com.

--

https://ece.uwaterloo.ca/~wdietl/

[Sebastien Deleuze]

Thanks for the useful feedback. It looks like NullAway is pretty close to what we need (Spring does not support null-safety on generics) so we would like, as a first step, to enable NullAway in the upcoming Spring Framework 6.2 (still with JSR 305), see spring-framework#32475 related issue. That should give us more confidence to switch to JSpecify later if we decide it.

That said, we currently seems to have a very common pattern currently not supported by NullAway. We have various places in our code that is using Assert#notNull. IntelliJ seems able to understand the related code flow after such invocation, the value asserted can't be null. NullAway seems not able to take that in account. We would really need that. Is there a workaround or should we create a related issue in https://github.com/uber/NullAway/issues?

[Manu Sridharan]

(jspecify-discuss to bcc)

Hi Sebastian, yes, please file an issue on the NullAway repo and we’d be glad to take a look.  At first glance, I think if you write @Contract(“null, _ -> fail”) on that method, NullAway should be able to pick up what is going on.  See here:

https://github.com/uber/NullAway/wiki/Supported-Annotations#contracts

If you don’t want a dependence on JetBrains @Contract we can probably support something else as an alias (or possibly we already do).  Anyway, happy to follow up via email or the NullAway issue tracker.

Best,

Manu

This electronic communication and the information and any files transmitted with it, or attached to it, are confidential and are intended solely for the use of the individual or entity to whom it is addressed and may contain information that is confidential, legally privileged, protected by privacy laws, or otherwise restricted from disclosure to anyone else. If you are not the intended recipient or the person responsible for delivering the e-mail to the intended recipient, you are hereby notified that any use, copying, distributing, dissemination, forwarding, printing, or copying of this e-mail is strictly prohibited. If you received this e-mail in error, please return the e-mail to the sender, delete it from your computer, and destroy any printed copy of it.

--
You received this message because you are subscribed to the Google Groups "jspecify-discuss" group.
To unsubscribe from this group and stop receiving emails from it, send an email to jspecify-discu...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/jspecify-discuss/9880098b-6070-4989-a4c4-fa8843dbc3edn%40googlegroups.com.

[Sebastien Deleuze]

Custom contracts work perfectly, we are going to leverage that, thanks!

[Sebastien Deleuze]

FYI, we have merged NullAway build-time checks in Spring Framework build (just for spring-core scope for now, will add other modules in the upcoming days) via this commit.

When finished, I will make a test with JSpecify annotations instead of JSR 305 to provide a feedback to this group (but Spring plans to stay on JSR 305 for Spring Framework 6.2).

[Sebastien Deleuze]

Spring Framework main branch has now 100% of its code checked with NullAway at build time.
I have created a branch which uses JSpecify instead of JSR 305 to see how that goes, see https://github.com/sdeleuze/spring-framework/tree/jspecify.
Good news:  meta annotating Spring annotation with JSpecify seems to work as expected with NullAway checks, 0 errors and the checks seems to be effective.
The main point to discuss is that unless I missed something, @NullMarked does not allow to differentiate @NonNullApi from @NonNullFields use cases, which make the migration path from JSR 305 to JSpecify challenging for us, so let's maybe discuss that in the next meeting.