facebook / infer

A static analyzer for Java, C, C++, and Objective-C
http://fbinfer.com/
MIT License
14.8k stars 2k forks source link

[java] DEADLOCK: False Negative in Infer analysis results after converting anonymous classes to lambda expressions #1775

Open mohui1999 opened 1 year ago

mohui1999 commented 1 year ago

Environment

Infer Version: v1.1.0-f93cb281ed
Operating System: Ubuntu 20.04.5 LTS

Description:

We converted anonymous classes to lambda expressions in the file infer/infer/tests/codetoanalyze/java/starvation-whole-program/MainMethod.java. After making this change, we ran the following command: sudo make direct_java_starvation-whole-program_test. However, we noticed inconsistencies between the results in issues.exp.test and the expected results in issues.exp. We expect Infer to detect certain converted codes to get results in issues.exp.test file similar to the ones mentioned in issues.exp. However, the result of MainMethod.java is different. The DEADLOCK issue does not appear in issues.exp.test. So we consider it as a false negative.

Steps to Reproduce:

  1. Convert anonymous classes to lambda expressions in MainMethod.java.
  2. Run the command: sudo make direct_java_starvation-whole-program_test.
  3. Compare the analysis results in issues.exp.test with the expected results in issues.exp.

Code Samples:

Original code in MainMethod.java:

class MainMethod {
    static Object monitorA, monitorB;

    public static void main(String args[]) {
        Thread t = new Thread(new Runnable() {
            @Override
            public void run() {
                synchronized (monitorA) {
                    synchronized (monitorB) {
                    }
                }
            }
        });
        t.start();

        synchronized (monitorB) {
            synchronized (monitorA) {
            }
        }
    }
}

Converted code in MainMethod.java:

class MainMethod {
    static Object monitorA, monitorB;

    public static void main(String[] args) {
        Thread t = new Thread(() -> {
            synchronized (monitorA) {
                synchronized (monitorB) {
                }
            }
        });
        t.start();

        synchronized (monitorB) {
            synchronized (monitorA) {
            }
        }
    }
}

Content in issue.exp:

codetoanalyze/java/starvation-whole-program/MainMethod.java, MainMethod.main(java.lang.String[]):void, 24, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void MainMethod.main(String[])`,Method call: `void MainMethod$1.run()`, locks `MainMethod.monitorA` in `class MainMethod`, locks `MainMethod.monitorB` in `class MainMethod`,[Trace 2] `void MainMethod.main(String[])`, locks `MainMethod.monitorB` in `class MainMethod`, locks `MainMethod.monitorA` in `class MainMethod`]
codetoanalyze/java/starvation-whole-program/MainMethod.java, MainMethod.main(java.lang.String[]):void, 26, DEADLOCK, no_bucket, ERROR, [[Trace 1] `void MainMethod.main(String[])`, locks `MainMethod.monitorB` in `class MainMethod`, locks `MainMethod.monitorA` in `class MainMethod`,[Trace 2] `void MainMethod.main(String[])`,Method call: `void MainMethod$1.run()`, locks `MainMethod.monitorA` in `class MainMethod`, locks `MainMethod.monitorB` in `class MainMethod`]
HKMANOJ commented 11 months ago

HI @mohui1999 I am interested to contribute for this can i take up this