CSA does not know `!(a>b) && !(c>d) == false` is true in the true branch of `if (a>b || c>d )`

[Geoffrey1014]

date: 2022-12-13 Commit: args: --analyze -Xclang -analyzer-stats -Xclang -analyzer-constraints=range -Xclang -setup-static-analyzer -Xclang -analyzer-config -Xclang eagerly-assume=false -Xclang -analyzer-checker=core,debug.ExprInspection test:

#include <stdint.h>
#include <stdbool.h>
void clang_analyzer_eval(int);

int foo(int a, int b, int c, int d) {
    if (a>b || c>d ){
        // clang_analyzer_eval(a);
        // clang_analyzer_eval(b);
        clang_analyzer_eval((a>b || c>d));
        // clang_analyzer_eval((a>b || c>d) == true);
        clang_analyzer_eval(!(a>b || c>d) == false);
        clang_analyzer_eval(!(a>b) && !(c>d) == false);
    }
}

report: https://github.com/llvm/llvm-project/issues/59491 fix: original:

[Geoffrey1014]

I found a problem that CSA evaluates '!(a>b) && !(c>d) == false' (line 12) to be TRUE and FLASE in the true branch of ' if (a>b || c>d )'. I think CSA should evaluate '!(a>b) && !(c>d) == false' only for one time and the result should be TRUE.

I run clang (trunk) with options --analyze -Xclang -analyzer-stats -Xclang -analyzer-constraints=range -Xclang -setup-static-analyzer -Xclang -analyzer-config -Xclang eagerly-assume=false -Xclang -analyzer-checker=core,debug.ExprInspection.

https://godbolt.org/z/9G8c3cnrc

Input:

#include <stdint.h>
#include <stdbool.h>
void clang_analyzer_eval(int);

int foo(int a, int b, int c, int d) {
    if (a>b || c>d ){
        // clang_analyzer_eval(a);
        // clang_analyzer_eval(b);
        clang_analyzer_eval((a>b || c>d));
        // clang_analyzer_eval((a>b || c>d) == true);
        clang_analyzer_eval(!(a>b || c>d) == false);
        clang_analyzer_eval(!(a>b) && !(c>d) == false);
    }
}

Output:

<source>:9:9: warning: TRUE [debug.ExprInspection]
        clang_analyzer_eval((a>b || c>d));
        ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:11:9: warning: TRUE [debug.ExprInspection]
        clang_analyzer_eval(!(a>b || c>d) == false);
        ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:12:9: warning: FALSE [debug.ExprInspection]
        clang_analyzer_eval(!(a>b) && !(c>d) == false);
        ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:12:9: warning: TRUE [debug.ExprInspection]
        clang_analyzer_eval(!(a>b) && !(c>d) == false);

[Geoffrey1014]

CSA is right. I realized that “==” has higher priority than "&&". So, CSA evaluated "!(a>b)" instead of "!(a>b) && !(c>d) " at line 12. And "a>b" could be true or false. Hence, CSA's evaluation is right. https://godbolt.org/z/bK67TazPd