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

iamsanjaymalakar commented 2 weeks ago

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 commented 1 week ago

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:

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!)
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 commented 1 week ago

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 commented 1 day ago

@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

typetools / checker-framework