WPI: inconsistency between warning and inferred annotations

[skehrli]

Weird behavior of the WPI script: Running WPI with the ResourceLeakChecker on a directory gives a warning. When the ResourceLeakChecker is run on the annotated file provided by WPI, there is no warning.

Reproduce:
wpiTest.zip
Unzip the provided zip file and run WPI with the resourceLeakChecker. Observe the warning about a not-called method.
unzip wpiTest.zip && cd RLCtest
/path/to/wpi.sh -- --checker org.checkerframework.checker.resourceleak.ResourceLeakChecker
The output of WPI will contain information about the annotated file, which was in /temp/wpi-ajava-/iteration1/RLCcheckerTest-org.checkerframework.checker.resourceleak.ResourceLeakChecker.ajava for me.
Change the file type from ajava to java. Now, run the ResourceLeakChecker on the file.
javacheck -processor resourceleak /path/to/annotated/file.java
Assuming javacheck is correctly set as an alias to the javac version of the checker framework, this runs the resourceleak checker on the file. There is no warning now, since all inferred annotations in the file are correct. It seems somehow WPI misses some annotation information.

[kelloggm]

@skehrli I attempted to reproduce the problem you're describing here and could not. It's possible, however, that it arises from a misreading of the output of the wpi.sh script.

When I execute /path/to/wpi.sh -- --checker org.checkerframework.checker.resourceleak.ResourceLeakChecker on your example, I get a wpi.log file with the following contents:

➜  dljc-out cat wpi.log

Running 'echo' '"-----------------------------------------------------------"'

"-----------------------------------------------------------"

Running '/Users/mjk76/jsr308/checker-framework/checker/bin/javac' '-Xmaxerrs' '10000' '-Xmaxwarns' '10000' '-J--add-opens=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.parser=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED' '-classpath' '/Users/mjk76/Downloads/wpi-6417/RLCtest/build' '-processor' 'org.checkerframework.checker.resourceleak.ResourceLeakChecker' '-d' '/Users/mjk76/Downloads/wpi-6417/RLCtest/build' '-sourcepath' '/Users/mjk76/Downloads/wpi-6417/RLCtest/src' '-g:none' '/Users/mjk76/Downloads/wpi-6417/RLCtest/src/RLCcheckerTest.java' '-Ainfer=ajava' '-Awarns'

/Users/mjk76/Downloads/wpi-6417/RLCtest/src/RLCcheckerTest.java:27: warning: [required.method.not.called] @MustCall method close may not have been invoked on new ZipFile(archivename) or any of its aliases.
    zf = new ZipFile(archivename);
         ^
  The type of object is: java.util.zip.ZipFile.
  Reason for going out of scope: regular method exit
1 warning

Running '/Users/mjk76/jsr308/checker-framework/checker/bin/javac' '-Xmaxerrs' '10000' '-Xmaxwarns' '10000' '-J--add-opens=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.parser=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED' '-Aajava=/var/folders/03/b2tvjr914yb7msv0crx4893w0000gn/T/wpi-ajava-20240124-102652-gub_jg4d/iteration0' '-classpath' '/Users/mjk76/Downloads/wpi-6417/RLCtest/build' '-processor' 'org.checkerframework.checker.resourceleak.ResourceLeakChecker' '-d' '/Users/mjk76/Downloads/wpi-6417/RLCtest/build' '-sourcepath' '/Users/mjk76/Downloads/wpi-6417/RLCtest/src' '-g:none' '/Users/mjk76/Downloads/wpi-6417/RLCtest/src/RLCcheckerTest.java' '-Ainfer=ajava' '-Awarns'


Running '/Users/mjk76/jsr308/checker-framework/checker/bin/javac' '-Xmaxerrs' '10000' '-Xmaxwarns' '10000' '-J--add-opens=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.parser=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED' '-J--add-opens=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED' '-Aajava=/var/folders/03/b2tvjr914yb7msv0crx4893w0000gn/T/wpi-ajava-20240124-102652-gub_jg4d/iteration0' '-classpath' '/Users/mjk76/Downloads/wpi-6417/RLCtest/build' '-processor' 'org.checkerframework.checker.resourceleak.ResourceLeakChecker' '-d' '/Users/mjk76/Downloads/wpi-6417/RLCtest/build' '-sourcepath' '/Users/mjk76/Downloads/wpi-6417/RLCtest/src' '-g:none' '/Users/mjk76/Downloads/wpi-6417/RLCtest/src/RLCcheckerTest.java'

This is the full log of the WPI run: that is, it is a log of all iterations of WPI on this target program. Each line that starts with "Running" and then a path to a Checker Framework javac is an iteration of WPI's outer loop; any warnings that appear in between them are the warnings that the checker produced during inference on that iteration. So, what we can deduce from this log is that on this program:

• WPI ran for three iterations
• in the first iteration, there was one warning; in iterations 2 and 3, there are no warnings
• there are no warnings after fixpoint is reached

This behavior is consistent with what you've observed, except I'm not seeing a warning on the final iteration (only one during an earlier iteration). If this explains what you're seeing, great (we can close this issue). If you're seeing something different, please add more details here.

[jyoo980]

One thing you could do is run the RLC on the final program with type annotations inferred via WPI; it should be the one with the highest numbered iteration folder.

I think that could help debug the issue and answer Martin's question of whether the errors are only being issued on intermediate iterations.

[skehrli]

Thank you for your responses. The warning is only issued in the first iteration and no longer in later iterations, I misread the output, I'm sorry about that.

I'll close the issue.

[mernst]

Is there something we can improve in the output? Other people have made exactly this error before.
For example, could we put a big, conspicuous break in the log between iterations?