False-positive with Checker Framework 3 and Buck on JDK11

[swarren12]

Recently, I helped in an attmept to update a large monorepo built using Buck from JDK1.8 to JDK11; as part of that migration Checker Framework was updated from 2.10 to 3.17. However, the project no longer builds as Checker Framework throws errors that were not present previously. From what I can tell, it appears that the upgrade has introduced some false positives.

I have recreated one particular problem with a cutdown project.

At a guess I would point a finger here at some incompatibility between Checker 3 and Buck; however, the manual does not seem to suggest that there are any known issues.

Commands

export JAVA_HOME=/path/to/your/jdk11
git clone https://github.com/swarren12/checker-weirdness.git
cd checker-weirdness
./build-buck
./buck fetch //... && ./buck build //app:main

Inputs

n/a

Outputs

Command failed with exit code 1.

stderr: app/src/main/java/com/example/Main.java:11: error: [conflicting.annos] invalid type: conflicting annotations [@s(Prefix.milli), @s(Prefix.milli)] in type "@s(Prefix.milli) @s(Prefix.milli) long"
        final @Milliseconds long time = clock.currentTimeMillis();
                                                               ^
Errors: 1. Warnings: 0.

    When running <javac>.
    When building rule //app:main.

Expectation

The project should build without an error.

Justification:

• the line that is failing is final @Milliseconds long time = clock.currentTimeMillis();.
• the Clock interface is annotated as @Milliseconds long currentTimeMillis();;
• therefore the signatures should match.

Additionally, if I'm reading the error correctly, Checker Framework does think the signatures match and so I'm unclear as to exactly why it is failing.

[mernst]

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

I appreciate the simple reproduction instructions. I am able to reproduce your problem within Buck.

However, I have not been able to reproduce the problem outside Buck.
The two attached variants of your project show three different attempts. (If you are interested, see the two README files for details.)

How can I get Buck to output the exact javac command line that it runs, so that I can reproduce the problem outside Buck?
I don't see documentation of this at, for example, https://buck.build/command/build.html (except for C++, and those instructions don't work in your build).

checker-weirdness-2.tar.gz
checker-weirdness-3.tar.gz

[swarren12]

I believe running the build with --verbose 8 should give you the output you want, i.e. ./buck build --verbose 8 //app:main. You may need to do a ./buck clean first to get some meaningful output (and then make sure to ./buck fetch //...!).

[swarren12]

I ran this myself earlier and I've attached the output. Specifically, the command that appears to be failing is:

javac -source 11 -target 11 -sourcepath  -g -processor org.checkerframework.checker.units.UnitsChecker -processorpath buck-out/gen/__checker-framework__/checker-framework.jar:buck-out/gen/__checker-qual__/checker-qual.jar:buck-out/gen/__checker-util__/checker-util.jar -verbose -d buck-out/bin/app/lib__main__scratch/classes -s buck-out/annotation/app/__main_gen__ -classpath buck-out/gen/__checker-framework__/checker-framework.jar:buck-out/gen/__checker-qual__/checker-qual.jar:buck-out/gen/__checker-util__/checker-util.jar:buck-out/gen/annotations/time/lib__annotations-time__output/annotations-time.jar:buck-out/gen/utils/clock/lib__clock__output/clock.jar @buck-out/gen/app/__main__srcs

Some other observations:

• Running this command from the terminal doesn't reproduce the error; so either Buck isn't being entirely honest about what it's running or there's some difference in the javac being used by Buck and being used outside?
• I added a new branch to the project showing that Bazel doesn't suffer the same problem, further pointing to Buck doing something weird!

(Edit) A further observation: running the build multiple times seems to sometimes work:

user@host $ ./buck clean && ./buck fetch //... && ./buck build //app:main
Not using buckd because watchman isn't installed.
Not using buckd because watchman isn't installed.
Parsing buck files: finished in 1.3 sec
Building: finished in 3.0 sec (100%) 3/3 jobs, 3 updated
  Total time: 4.4 sec
Not using buckd because watchman isn't installed.
Parsing buck files: finished in 1.2 sec
Building: finished in 5.9 sec (100%) 14/14 jobs, 11 updated
  Total time: 7.3 sec
Command failed with exit code 1.

stderr: app/src/main/java/com/example/Main.java:11: error: [conflicting.annos] invalid type: conflicting annotations [@s(Prefix.milli), @s(Prefix.milli)] in type "@s(Prefix.milli) @s(Prefix.milli) long"
        final @Milliseconds long time = clock.currentTimeMillis();
                                                               ^
Errors: 1. Warnings: 0.

    When running <javac>.
    When building rule //app:main.

user@host $ ./buck build //app:main 
Not using buckd because watchman isn't installed.
Parsing buck files: finished in 1.2 sec
Building: finished in 3.5 sec (100%) 11/11 jobs, 1 updated
  Total time: 4.9 sec

[msridhar]

This is weird. My wild guess would be some classloader issue, where the @Milliseconds annotation is somehow getting loaded by two unrelated classloaders and hence they look incompatible to the Checker Framework. But if the build succeeds after multiple runs then it might be something different.

@artempyanykh any idea what is going on here (if you have time)?

[artempyanykh]

Assuming, there's not a lot of differences between our internal setup and OSS version of buck (I think there shouldn't, at least conceptually):

1. The command lines that buck prints with -v 8 is not what's actually getting executed.
2. Buck doesn't invoke external javac, but uses in process compilation [link], potentially multi-threaded. This is configurable to an extent [docs].
3. It also may use multiple classloaders that are cached [link].

When I need to debug such issues in our code, I usually run buck in debug mode (it's java process anyway), put breakpoints in the analyser's code and see what's going on exactly that makes the check fail.

[mernst]

@artempyanykh Is there a way to configure Buck to use an external javac? In general I realize that starting a new process is inefficient.

[artempyanykh]

@mernst the easiest one is probably via a config flag -c tools.javac=[path-to-javac].

I've made several iterations of the following, and there were no errors.

./buck-exe clean && ./buck-exe fetch //... && ./buck-exe build //app:main -c tools.javac=(which javac)

Without an external javac the error can be reproed easily.

Note: @swarren12 huge thanks for providing the repo with a repro! One small suggestion is to rename buck to something like buck-exe because on MacOS the filesystem is not case sensitive so having both buck and BUCK files makes things weird.

[mernst]

I have made a pull request that summarizes this discussion in the Checker Framework manual.

Could one of you please review it to ensure that it is accurate?
Please see #5072 .

Thanks!