Inconsistent inferred annotated file generation during WPI iterations causing non-termination

[iamsanjaymalakar]

Description

We are experiencing a non-termination issue where the Checker Framework inconsistently generates output files during Whole Program Inference (WPI). Specifically, the framework alternates between generating annotated files in one iteration and generating no files in the subsequent iteration. This pattern affects the 'build/whole-program-inference' directory, where output files are expected in each iteration but are absent in even-numbered iterations.

This is causing non-termination in the WPI script.

Diff between two iterations:

Only in ../dataset/june2020_dataset_copy/url7a69e77641_benmouh_MySgbd_tgz-pJ8-Demo_CheckRowNumJ8/wpi-iterations/temp1: Demo
Only in ../dataset/june2020_dataset_copy/url7a69e77641_benmouh_MySgbd_tgz-pJ8-Demo_CheckRowNumJ8/wpi-iterations/temp1: org

Test Project

benmouh_repro.zip

Steps to Reproduce

• Run the Whole Program Inference (WPI) using the provided script and project.
• In the zip folder, there is one shell script named wpi.sh and one folder containing the project's source code.
• Run the script with the project path as an argument:

  ./wpi.sh url7a69e77641_benmouh_MySgbd_tgz-pJ8-Demo_CheckRowNumJ8

• Check the build/whole-program-inference directory after each iteration.
• After each iteration, the inference outputs are stored in the project's root folder, in the wpi-iterations directory. You can also check the inference results for each iteration there.

[kelloggm]

Here is a minimized test case:

// test case for https://github.com/typetools/checker-framework/issues/6570

// A class is technically permitted to end with a semicolon (though it doesn't do
// anything).
public class EndsWithSemicolon {

};

Running ./gradlew ainferTestCheckerAjavaTest after adding this test to either checker/tests/all-systems or checker/tests/ainfer-testchecker/non-annotated demonstrates the crash that's causing the periodic behavior that @iamsanjaymalakar is observing. What's happening is that in the first round, the Checker Framework creates a .ajava file for the class Demo/MDemo.java in the target project (which you'll note ends in a semicolon for some reason, just like the minimized test case above). In the next round, the Checker Framework crashes while attempting to jointly parse the original source file and the created .ajava file. Because the framework crashes, annotation files for some classes don't get written, causing the "only in ..." behavior that @iamsanjaymalakar observed.

Here's the important part of the stack trace (note that I've removed the bodies of the MDemo class that get printed, because they're not important):

Caused by: org.checkerframework.javacutil.BugInCF: org.checkerframework.framework.stub.AnnotationFileParser.AjavaAnnotationCollectorVisitor.visitLists(
public class MDemo {
...
},; [size 2], [@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.mustcall.MustCallChecker")
public class MDemo {
...
}] [size 1])
	at org.checkerframework.framework.ajava.JointJavacJavaParserVisitor.visitLists(JointJavacJavaParserVisitor.java:2279)
	at org.checkerframework.framework.ajava.JointJavacJavaParserVisitor.visitCompilationUnit(JointJavacJavaParserVisitor.java:651)
	at org.checkerframework.framework.ajava.JointJavacJavaParserVisitor.visitCompilationUnit(JointJavacJavaParserVisitor.java:188)
	at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCCompilationUnit.accept(JCTree.java:623)
	at org.checkerframework.framework.stub.AnnotationFileParser.processCompilationUnit(AnnotationFileParser.java:825)
	at org.checkerframework.framework.stub.AnnotationFileParser.processStubUnit(AnnotationFileParser.java:790)
	at org.checkerframework.framework.stub.AnnotationFileParser.process(AnnotationFileParser.java:779)
	at org.checkerframework.framework.stub.AnnotationFileParser.parseAjavaFile(AnnotationFileParser.java:696)
	at org.checkerframework.framework.stub.AnnotationFileElementTypes.parseAjavaFileWithTree(AnnotationFileElementTypes.java:286)
	at org.checkerframework.framework.type.AnnotatedTypeFactory.setRoot(AnnotatedTypeFactory.java:1013)

The issue is that javac tree for the original source file has two "compilation units": the class itself and then a single semicolon. The JavaParser tree for the .ajava file only has one "compilation unit": the class itself. In particular, there is not a semicolon at the end of the generated .ajava file: the CF doesn't include it when building the .ajava file.

There are two possible fixes, and I'm not sure which is better. @smillst and @mernst I'd appreciate your input on which of these you think we should pursue:

1. change JointJavacJavaParserVisitor so that it tolerates extraneous semicolons in the list of compilation units (in theory, someone could put arbitrary numbers of semicolons between their classes, if they'd like - not just at the end!)
2. change ajava file generation so that it preserves extraneous semicolons in the input

The trade-offs between the two approaches that I see are:

• approach 1 will be simpler to implement: just write a filter for the list of compilation units and remove any that contain only a single semicolon before passing the list to visitLists. However, it feels a bit like a band-aid over the bigger problem, which is that the .ajava file doesn't match the input source file.
• approach 2 is more in the spirit of what a .ajava file is supposed to be, but I'm not sure how difficult it will be to implement. We'll first need to figure out why the generated .ajava file doesn't contain these extraneous semicolons, which could well be a JavaParser issue.

[mernst]

If this is a JavaParser issue, then I don't want to go anywhere near it.

I think that approach 1 is acceptable. This will probably be a relatively rare occurrence.

[iamsanjaymalakar]

@kelloggm I ran on the original project url7a69e77641_benmouh_MySgbd_tgz-pJ8-Demo_CheckRowNumJ8 with the fix from #6588, but still getting the non-termination. Seems like the compier erorr still exists:

An exception has occurred in the compiler (11.0.22). Please file a bug against the Java compiler via the Java bug reporting page (https://bugreport.java.com) after checking the Bug Database (https://bugs.java.com) for duplicates. Include your program and the following diagnostic in your report. Thank you.
com.sun.tools.javac.util.ClientCodeException: java.lang.Error: Problem while parsing ../dataset/june2020_dataset_copy/url7a69e77641_benmouh_MySgbd_tgz-pJ8-Demo_CheckRowNumJ8/wpi-out/Demo/Mtest-org.checkerframework.checker.mustcall.MustCallChecker.ajava that corresponds to ../dataset/june2020_dataset_copy/url7a69e77641_benmouh_MySgbd_tgz-pJ8-Demo_CheckRowNumJ8/src/Demo/Mtest.java
	at jdk.compiler/com.sun.tools.javac.api.ClientCodeWrapper$WrappedTaskListener.finished(ClientCodeWrapper.java:832)
	at jdk.compiler/com.sun.tools.javac.api.MultiTaskListener.finished(MultiTaskListener.java:132)
	at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1414)
	at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.flow(JavaCompiler.java:1371)
	at jdk.compiler/com.sun.tools.javac.main.JavaCompiler.compile(JavaCompiler.java:973)
	at jdk.compiler/com.sun.tools.javac.main.Main.compile(Main.java:311)
	at jdk.compiler/com.sun.tools.javac.main.Main.compile(Main.java:170)
	at jdk.compiler/com.sun.tools.javac.Main.compile(Main.java:57)
	at jdk.compiler/com.sun.tools.javac.Main.main(Main.java:43)
Caused by: java.lang.Error: Problem while parsing ../dataset/june2020_dataset_copy/url7a69e77641_benmouh_MySgbd_tgz-pJ8-Demo_CheckRowNumJ8/wpi-out/Demo/Mtest-org.checkerframework.checker.mustcall.MustCallChecker.ajava that corresponds to ../dataset/june2020_dataset_copy/url7a69e77641_benmouh_MySgbd_tgz-pJ8-Demo_CheckRowNumJ8/src/Demo/Mtest.java
	at org.checkerframework.framework.type.AnnotatedTypeFactory.setRoot(AnnotatedTypeFactory.java:1013)
	at org.checkerframework.framework.type.GenericAnnotatedTypeFactory.setRoot(GenericAnnotatedTypeFactory.java:443)
	at org.checkerframework.checker.mustcall.MustCallAnnotatedTypeFactory.setRoot(MustCallAnnotatedTypeFactory.java:153)
	at org.checkerframework.common.basetype.BaseTypeVisitor.setRoot(BaseTypeVisitor.java:387)
	at org.checkerframework.framework.source.SourceChecker.setRoot(SourceChecker.java:682)
	at org.checkerframework.common.basetype.BaseTypeChecker.setRoot(BaseTypeChecker.java:167)
	at org.checkerframework.framework.source.SourceChecker.typeProcess(SourceChecker.java:1071)
	at org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:559)
	at org.checkerframework.common.basetype.BaseTypeChecker.typeProcess(BaseTypeChecker.java:552)
	at org.checkerframework.javacutil.AbstractTypeProcessor$AttributionTaskListener.finished(AbstractTypeProcessor.java:188)
	at jdk.compiler/com.sun.tools.javac.api.ClientCodeWrapper$WrappedTaskListener.finished(ClientCodeWrapper.java:828)
	... 8 more
Caused by: org.checkerframework.javacutil.BugInCF: org.checkerframework.framework.stub.AnnotationFileParser.AjavaAnnotationCollectorVisitor.visitLists(
public class Mtest {
    
    public Mtest() {
        super();
    }
    
    public static void main(String[] args) {
        try {
            MqlParser p = new MqlParser();
            p.initParser(new ByteArrayInputStream(args[0].getBytes()));
            MStatement st = p.readStatement();
            System.out.println(st.toString());
            MQuery q = (MQuery)st;
            Vector v = q.getSelect();
            for (int i = 0; i < v.size(); i++) {
                MSelectItem it = (MSelectItem)v.elementAt(i);
                System.out.print("col=" + it.getColumn() + ",agg=" + it.getAggregate());
                String s = it.getSchema();
                if (s != null) System.out.print(",schema=" + s);
                s = it.getTable();
                if (s != null) System.out.print(",table=" + s);
                System.out.println();
            }
        } catch (Exception e) {
            e.printStackTrace();
        }
    }
},; [size 2], [@org.checkerframework.framework.qual.AnnotatedFor("org.checkerframework.checker.mustcall.MustCallChecker")
public class Mtest {

    @org.checkerframework.dataflow.qual.Impure
    public static void main(String[] args) {
        try {
            MqlParser p = new MqlParser();
            p.initParser(new ByteArrayInputStream(args[0].getBytes()));
            MStatement st = p.readStatement();
            System.out.println(st.toString());
            MQuery q = (MQuery) st;
            Vector v = q.getSelect();
            for (int i = 0; i < v.size(); i++) {
                MSelectItem it = (MSelectItem) v.elementAt(i);
                System.out.print("col=" + it.getColumn() + ",agg=" + it.getAggregate());
                String s = it.getSchema();
                if (s != null)
                    System.out.print(",schema=" + s);
                s = it.getTable();
                if (s != null)
                    System.out.print(",table=" + s);
                System.out.println();
            }
        } catch (Exception e) {
            e.printStackTrace();
        }
    }
}] [size 1])
	at org.checkerframework.framework.ajava.JointJavacJavaParserVisitor.visitLists(JointJavacJavaParserVisitor.java:2279)
	at org.checkerframework.framework.ajava.JointJavacJavaParserVisitor.visitCompilationUnit(JointJavacJavaParserVisitor.java:651)
	at org.checkerframework.framework.ajava.JointJavacJavaParserVisitor.visitCompilationUnit(JointJavacJavaParserVisitor.java:188)
	at jdk.compiler/com.sun.tools.javac.tree.JCTree$JCCompilationUnit.accept(JCTree.java:591)
	at org.checkerframework.framework.stub.AnnotationFileParser.processCompilationUnit(AnnotationFileParser.java:821)
	at org.checkerframework.framework.stub.AnnotationFileParser.processStubUnit(AnnotationFileParser.java:786)
	at org.checkerframework.framework.stub.AnnotationFileParser.process(AnnotationFileParser.java:775)
	at org.checkerframework.framework.stub.AnnotationFileParser.parseAjavaFile(AnnotationFileParser.java:692)
	at org.checkerframework.framework.stub.AnnotationFileElementTypes.parseAjavaFileWithTree(AnnotationFileElementTypes.java:286)
	at org.checkerframework.framework.type.AnnotatedTypeFactory.setRoot(AnnotatedTypeFactory.java:1011)
	... 18 more
Caused by: java.lang.Throwable
	at org.checkerframework.javacutil.BugInCF.<init>(BugInCF.java:34)
	... 28 more

[kelloggm]

@kelloggm I ran on the original project url7a69e77641_benmouh_MySgbd_tgz-pJ8-Demo_CheckRowNumJ8 with the fix from #6588, but still getting the non-termination. Seems like the compier erorr still exists:

@iamsanjaymalakar I can't reproduce the problem that you're reporting on master. In particular, I just ran your wpi.sh script using a Checker Framework built from commit ac49fb80320f706419ef63f31bd73071451c9676 in the reproduction package that you provided, and observed that WPI terminates in nine iterations. Can you double-check that you're using a CF version that contains the fix, and if so can you provide another reproduction package that exactly matches the environment you're using? If you're still observing the issue, there must be some difference between your setup and mine.

[iamsanjaymalakar]

@kelloggm I just rechecked the commit of my checker.jar. It turns out the checker version has been incremented to 3.43.1 from 3.43.0. I was still using the JARs from the 3.43.0 snapshot version, which is the issue.

I'll run on the 3.43.1 snapshot version and close the issue if the project terminates. Sorry for the confusion.