Publishing artifacts without generated CF annotations

[Meijuh]

When publishing library artifacts (that have been built with CF support ) they include generated CF annotations, sometimes a lot. For example I have a library with a public API method, that has the following generated annotations:

@Pure
public @UnknownKeyFor @NonNull @Initialized @SubstringIndexUnknown @UnknownVal @SearchIndexUnknown @SameLenUnknown @LessThanUnknown @LowerBoundUnknown @UpperBoundUnknown @UnknownThis @CalledMethods({})
Integer getPeriodicity() {
    return 1;
}

Even when developing apps that require this library that have CF enabled, this clutters code hinting a lot in IDEs. So my questions:

1. Why does this Gradle plugin export code with generated annotations? Is it necessary for proving correctness in applications that depend on such libraries, or is it only to speed up the verification?
2. Is it possible to publish artifacts without CF generated annotations? Also, if we do, what are the consequences?

[kelloggm]

When publishing library artifacts (that have been built with CF support ) they include generated CF annotations, sometimes a lot

As you've surmised, this is intentional. Our reasoning is that library users shouldn't be looking at the generated .class files directly, but you're right that this perspective doesn't take into account that IDEs usually decompile the .class files for libraries when a user wants to read library code (which leads to the situation you've observed, with generated annotations that are meant for machine consumption becoming visible to users).

Why does this Gradle plugin export code with generated annotations? Is it necessary for proving correctness in applications that depend on such libraries, or is it only to speed up the verification?

It's often necessary for proving correctness in applications that depend on libraries. The Checker Framework cannot examine the source code of the library to determine the intended specification for an un-annotated library, so if we don't retain annotations in the bytecode then there is no way to communicate that the code has been typechecked. In that case, the Checker Framework falls back on worst-case assumptions about libraries, which often leads to false positive warnings in client code (and the need to write stub files or otherwise provide annotations for the libraries). It's definitely a better experience for Checker Framework users if libraries that have been typechecked can automatically use any facts that were proved when they were compiled.

Is it possible to publish artifacts without CF generated annotations? Also, if we do, what are the consequences?

I don't know of a way to do this easily (@mernst might?). You could remove them from the .class files in a post-processing step using a library like ASM or a tool like ProGuard, but I've never tried to do that with any of those tools so I'm not sure how well-supported this use case would be.

As a bit of background for why this is tricky, whether or not annotations are put into the bytecode is determined by the @RetentionPolicy of the annotation when the annotation itself is compiled. That means you can't easily change it without recompiling the annotations. Another option here that might work is that you could:

• download a copy of the Checker Framework's source code
• change the @RetentionPolicy of any annotations you don't want to appear (or all annotations...) to @RetentionPolicy(SOURCE), which would prevent them from appearing in class files
• rebuild checker-qual.jar
• change you checkerFramework dependency to use your newly-rebuilt checker-qual.jar

It might also be possible to work around the problem in the IDE itself - either by pointing it at the source code instead of letting it use the decompiler or by changing some setting in the decompiler itself (e.g., to not show or not decompile type annotations). I don't know if IDEs support those things (and I definitely don't know whether your IDE supports them), but either could plausibly work to avoid this problem.

[Meijuh]

Thanks so much for the clarification. Instead of modifying the produced bytecode afterwards, we could also produce an additional JAR, without CF annotations, and, e.g., with Maven archive classifier no-cf? We would probably need an extra task that compiles the source code again, but with CF disabled?

[kelloggm]

Instead of modifying the produced bytecode afterwards, we could also produce an additional JAR, without CF annotations, and, e.g., with Maven archive classifier no-cf? We would probably need an extra task that compiles the source code again, but with CF disabled?

Definitely! (and this is so much simpler than what I suggested, nice!)

[Meijuh]

Would you like a PR for this?

Op wo 14 feb 2024 18:04 schreef Martin Kellogg @.***>:

Instead of modifying the produced bytecode afterwards, we could also produce an additional JAR, without CF annotations, and, e.g., with Maven archive classifier https://www.baeldung.com/maven-artifact-classifiers no-cf? We would probably need an extra task that compiles the source code again, but with CF disabled?

Definitely! (and this is so much simpler than what I suggested, nice!)

— Reply to this email directly, view it on GitHub https://github.com/kelloggm/checkerframework-gradle-plugin/issues/268#issuecomment-1944245272, or unsubscribe https://github.com/notifications/unsubscribe-auth/AAL6XQERLQ7HF2LEYYWA5JLYTTVAZAVCNFSM6AAAAABC7VORPGVHI2DSMVQWIX3LMV43OSLTON2WKQ3PNVWWK3TUHMYTSNBUGI2DKMRXGI . You are receiving this because you authored the thread.Message ID: @.***>

[kelloggm]

Would you like a PR for this?

Definitely, if you're willing to write one! I'd accept either:

• documentation on how to do it in the the user's build.gradle file (in the README), or
• an option in the plugin that turns it on for users, controlled by a property in CheckerFrameworkExtension

Thanks in advance!

[Meijuh]

It looks more complicated than I initially thought as Gradle does not seem to have a straightforward way to copy task configurations. E.g., there seems no easy way for me to duplicate the configuration of the JavaCompile task, and modify it with checkerFramework.skipCheckerFramework = true. However, what could be a way to go is to use nested builds for this. This means in a first step we do something like:

tasks.register('noCfCompileJava', GradleBuild) {
    tasks = ['compileJava']
    startParameter.projectProperties['skipCheckerFramework'] = 'true'
    startParameter.projectProperties['buildDir'] = file(buildDir.toString() + "/no-cf").toString()
    buildName = "ncf${project.path}"
}

but above will not use start parameters like the log level from the root build.

The next step would be to create an archive like:

tasks.register('noCfJar', Jar) {
    from(buildDir.toString() + "/no-cf/classes/java/main")
    archiveClassifier.set('no-cf')
}

But I'm not too convinced of this approach. Any idea if task configurations can be duplicated? Or something else?