GCC Static Analyzer does not know `1-a > 0-b` in the true branch of `if (a < b)`

[Geoffrey1014]

date: 2022-12-13 Commit: 8c8ca873216387bc26046615c806b96f0345ff9d args: -O0 -fanalyzer test:

#include <stdint.h>
#include <stdbool.h>

int main(int a, int b, int c, int d) {
    if ((a<b)){
        //Negation
        __analyzer_eval(!(a<b) == false); 
        __analyzer_eval(-a > -b);

        // Add a positive number after the negation
        __analyzer_eval(0-a > 0-b);
        __analyzer_eval(1-a > 0-b);
        __analyzer_eval(1-a > 1-b);
        __analyzer_eval(2-a > 0-b);
        __analyzer_eval(2-a > 1-b);
        __analyzer_eval(2-a > 2-b);

        // Add a negative number after the negation
        __analyzer_eval(-0-a > -0-b);
        __analyzer_eval(-1-a > -0-b);
        __analyzer_eval(-1-a > -1-b);
        __analyzer_eval(-2-a > -0-b);
        __analyzer_eval(-2-a > -1-b);
        __analyzer_eval(-2-a > -2-b);

        //Multiply the positive number after the negation
        __analyzer_eval( -a*0 == -b*0);
        __analyzer_eval( -a*1 > -b*1);
        __analyzer_eval( -a*2 > -b*2);
        __analyzer_eval( -a*3 > -b*3);

        //Multiply the negative number after the negation
        __analyzer_eval( -1*-a < -1*-b);
        __analyzer_eval( -2*-a < -2*-b);
        __analyzer_eval( -3*-a < -3*-b);
    }
}

report: https://gcc.gnu.org/bugzilla/show_bug.cgi?id=109193 fix: original:

[Geoffrey1014]

I found a problem that GCC Static Analyzer does not know 1-a > 0-b" (line 12) in the true branch of "if (a < b) ", but it knows “0-a > 0-b" (line 11) .

I run gcc (trunk) with options -fanalyzer -O0. https://godbolt.org/z/h4ddrKKrY

Input:

#include <stdint.h>
#include <stdbool.h>

int main(int a, int b, int c, int d) {
    if ((a<b)){
        //Negation
        __analyzer_eval(!(a<b) == false); 
        __analyzer_eval(-a > -b);

        // Add a positive number after the negation
        __analyzer_eval(0-a > 0-b);
        __analyzer_eval(1-a > 0-b);
        __analyzer_eval(1-a > 1-b);
        __analyzer_eval(2-a > 0-b);
        __analyzer_eval(2-a > 1-b);
        __analyzer_eval(2-a > 2-b);

        // Add a negative number after the negation
        __analyzer_eval(-0-a > -0-b);
        __analyzer_eval(-1-a > -0-b);
        __analyzer_eval(-1-a > -1-b);
        __analyzer_eval(-2-a > -0-b);
        __analyzer_eval(-2-a > -1-b);
        __analyzer_eval(-2-a > -2-b);

        //Multiply the positive number after the negation
        __analyzer_eval( -a*0 == -b*0);
        __analyzer_eval( -a*1 > -b*1);
        __analyzer_eval( -a*2 > -b*2);
        __analyzer_eval( -a*3 > -b*3);

        //Multiply the negative number after the negation
        __analyzer_eval( -1*-a < -1*-b);
        __analyzer_eval( -2*-a < -2*-b);
        __analyzer_eval( -3*-a < -3*-b);
    }
}

Output:

<source>: In function 'main':
<source>:7:9: warning: implicit declaration of function '__analyzer_eval' [-Wimplicit-function-declaration]
    7 |         __analyzer_eval(!(a<b) == false);
      |         ^~~~~~~~~~~~~~~
<source>:7:9: warning: TRUE
    7 |         __analyzer_eval(!(a<b) == false);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:8:9: warning: TRUE
    8 |         __analyzer_eval(-a > -b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~
<source>:11:9: warning: TRUE
   11 |         __analyzer_eval(0-a > 0-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:12:9: warning: UNKNOWN
   12 |         __analyzer_eval(1-a > 0-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:13:9: warning: TRUE
   13 |         __analyzer_eval(1-a > 1-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:14:9: warning: UNKNOWN
   14 |         __analyzer_eval(2-a > 0-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:15:9: warning: UNKNOWN
   15 |         __analyzer_eval(2-a > 1-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:16:9: warning: TRUE
   16 |         __analyzer_eval(2-a > 2-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:19:9: warning: TRUE
   19 |         __analyzer_eval(-0-a > -0-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:20:9: warning: UNKNOWN
   20 |         __analyzer_eval(-1-a > -0-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:21:9: warning: TRUE
   21 |         __analyzer_eval(-1-a > -1-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:22:9: warning: UNKNOWN
   22 |         __analyzer_eval(-2-a > -0-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:23:9: warning: UNKNOWN
   23 |         __analyzer_eval(-2-a > -1-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:24:9: warning: TRUE
   24 |         __analyzer_eval(-2-a > -2-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:27:9: warning: TRUE
   27 |         __analyzer_eval( -a*0 == -b*0);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:28:9: warning: TRUE
   28 |         __analyzer_eval( -a*1 > -b*1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:29:9: warning: TRUE
   29 |         __analyzer_eval( -a*2 > -b*2);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:30:9: warning: TRUE
   30 |         __analyzer_eval( -a*3 > -b*3);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:33:9: warning: TRUE
   33 |         __analyzer_eval( -1*-a < -1*-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:34:9: warning: TRUE
   34 |         __analyzer_eval( -2*-a < -2*-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:35:9: warning: TRUE
   35 |         __analyzer_eval( -3*-a < -3*-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Compiler returned: 0

[Geoffrey1014]

I found a problem that GCC Static Analyzer does not know "1-a > 0-b" (line 12) in the true branch of "if (a < b && 0 < a) ", but it knows “0-a > 0-b" (line 11) .

I run gcc (trunk) with options -fanalyzer -O0.

See it live: https://godbolt.org/z/6MjobMqnM

Input:

#include <stdint.h>
#include <stdbool.h>

int foo(int a, int b) {
    if ((a<b) && (0 < a)){
        //Negation
        __analyzer_eval(!(a<b) == false); 
        __analyzer_eval(-a > -b);

        // Add a positive number after the negation
        __analyzer_eval(0-a > 0-b);
        __analyzer_eval(1-a > 0-b);
        __analyzer_eval(1-a > 1-b);
        __analyzer_eval(2-a > 0-b);
        __analyzer_eval(2-a > 1-b);
        __analyzer_eval(2-a > 2-b);

    }
}

Output:

<source>: In function 'foo':
<source>:7:9: warning: implicit declaration of function '__analyzer_eval' [-Wimplicit-function-declaration]
    7 |         __analyzer_eval(!(a<b) == false);
      |         ^~~~~~~~~~~~~~~
<source>:7:9: warning: TRUE
    7 |         __analyzer_eval(!(a<b) == false);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:8:9: warning: TRUE
    8 |         __analyzer_eval(-a > -b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~
<source>:11:9: warning: TRUE
   11 |         __analyzer_eval(0-a > 0-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:12:9: warning: UNKNOWN
   12 |         __analyzer_eval(1-a > 0-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:13:9: warning: TRUE
   13 |         __analyzer_eval(1-a > 1-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:14:9: warning: UNKNOWN
   14 |         __analyzer_eval(2-a > 0-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:15:9: warning: UNKNOWN
   15 |         __analyzer_eval(2-a > 1-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:16:9: warning: TRUE
   16 |         __analyzer_eval(2-a > 2-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
Compiler returned: 0

[Geoffrey1014]

GSA does not know "b > 0" under the if condition that "a>0 && b > a" either.

See it live: https://godbolt.org/z/1aGds8aTq

CSA : https://godbolt.org/z/o5df457rz

CSA does not know "b > 0" under the if condition that "a>0 && b > a" https://github.com/llvm/llvm-project/issues/61511

[Geoffrey1014]

Bug 104940 - RFE: integrate analyzer with an SMT solver -fanalyzer currently has its own constraint_manager class for tracking the constraints that hold at a point on an execution path, but it only verifies some of the interactions between constraints and symbolic values, which can lead to false positives.

For example, consider:

#include "analyzer-decls.h"

void test (int x, int y)
{
  if (y == 3)
    if (2 * x == y)
      __analyzer_dump_path ();
}

[ghost]

Neither CSA nor GSA know "b > 0" under "a>0 && b > a": https://github.com/llvm/llvm-project/issues/61511