Unexpected SideEffectFree annotation in compiled classes

[andreas...@coremedia.com]

Hi,

the Checker Framework seems to add the annotation @SideEffectFree to certain class files when checking the code. We're using version 2.4.0 to execute a custom checker.

This annotation causes problems in our Maven build where we use the Maven Dependency Analyzer (analyze-only goal of the maven-dependency-plugin) to check module dependencies. The Maven Dependency Analyzer scans the class files and now issues warnings that classes use checker-qual.jar. Because of that, the maven-dependency-plugin asks me to add a compile dependency to checker-qual. But the source code of that module does not use checker-qual anywhere.

Is there a reason why the Checker Framework needs to add this annotation? Or is there an option to disable this behaviour? I was a bit surprised that the Checker Framework changes the compile result in such a way. Are there other differences in the compiled classes? Sorry, if this is explained in the documentation - I may have missed that part.

Thank you,
Andreas

[Michael Ernst]

Andreas-

I'm sorry you are having trouble. Thanks for the bug report.

Can you provide a minimal example of the bug? That will help us to test
that our changes really fix it.
Thanks!

-Mike

> Subject: Unexpected SideEffectFree annotation in compiled classes
> From: andreas...@coremedia.com
> To: Checker Framework discussion
> <checker-fram...@googlegroups.com>
> Date: Mon, 5 Mar 2018 05:44:28 -0800 (PST)

> --
>
> ---
> You received this message because you are subscribed to the Google
> Groups "Checker Framework discussion" group.
> To unsubscribe from this group and stop receiving emails from it, send
> an email to checker-framework-...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[Werner Dietl]

Andreas,

the Checker Framework automatically propagates certain declaration
annotations from a superclass to a subclass:
https://github.com/typetools/checker-framework/commit/51db893303c404badd234bc703b691a7a40eb20b

@SideEffectFree and @Pure being two of those annotations.

It looks like we didn't update the manual in enough places to explain
this fully.

Many methods in java.lang.Object are marked as @Pure or @SEF:
https://github.com/typetools/checker-framework/blob/master/checker/jdk/nullness/src/java/lang/Object.java
Therefore, any class that overrides these methods will implicitly also
mark these methods as @Pure and @SEF, explaining why these annotations
would appear in the bytecode.

Without inheriting these annotations, one would get invalid-override
warnings for all such methods, because it is not allowed to e.g.
override the @Pure java.lang.Object#equals method with a non-@Pure
version (which is the default for method declarations).
As the side-effect annotations are currently trusted and not checked,
adding these annotations doesn't cause additional warnings.

Also note that type qualifiers that have been defaulted will appear in
bytecode, even though the source code doesn't mention them explicitly.
For example with the Nullness Checker, by default types are @NonNull;
source code without any explicit annotations will result in bytecode
with @NonNull dependencies.
Is the Maven Dependency Analyzer not complaining about type annotations?

So in effect, bytecode that is generated by the Checker Framework can
automatically depend on checker-qual, even though the source code
didn't explicitly depend on any qualifiers.

Would it be easy to add checker-qual as a compile dependency for all
classes that get compiled by the Checker Framework?

Best,
cu, WMD.

P.S.: At the moment this annotation inheritance only happens for
declaration annotations. @InheritedAnnotation can be used to mark
additional declaration annotations to be inherited.
Type qualifiers are currently not inherited, but that might change:
https://github.com/typetools/checker-framework/issues/286
Also relevant: https://github.com/typetools/checker-framework/issues/342

> --
>
> ---
> You received this message because you are subscribed to the Google Groups
> "Checker Framework discussion" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to checker-framework-...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

--
http://www.google.com/profiles/wdietl

[andreas...@coremedia.com]

Werner,

thanks for the explanation. This really makes sense.

> Is the Maven Dependency Analyzer not complaining about type annotations?

It should complain but there was a bug in the Maven Dependency Analyzer that it ignored type annotations. I've fixed that recently: https://issues.apache.org/jira/browse/MSHARED-674
The Maven Dependency Plugin uses the Maven Dependency Analyzer under the hood. There's no release of the Maven Dependency Plugin with the fix yet (https://issues.apache.org/jira/browse/MDEP-594).
But it will complain about type annotations in the future with one of the next releases.

> Would it be easy to add checker-qual as a compile dependency for all  classes that get compiled by the Checker Framework?

This could lead to warnings about an "unused declared dependency" for checked modules where no annotation from checker-qual is written to the class files.

I think I 'd rather configure the Maven Dependency Plugin to ignore checker-qual.jar for dependency analysis: https://maven.apache.org/plugins/maven-dependency-plugin/examples/exclude-dependencies-from-dependency-analysis.html
That's okay as a workaround for me.

Best,
Andreas

> email to checker-framework-discuss+unsub...@googlegroups.com.