GCC Static Analyzer doesn't realize `0-width < 0` when `width > 0` and width is int type

[Geoffrey1014]

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

#include <assert.h>
#include <stdbool.h>
extern void __analyzer_eval (int);

void decode(int width) {
//   assert(width > 0);
if (width > 0){
  int base;
  bool inited = false;

  int i = 0;
  if (i - width < 0) {
    base = 512;
    inited = true;
  }
//   assert(inited); // <- if i uncomment this, the warning is gone.
  base+=1;

  if (base >> 10)
    assert(false);
}
}

report: https://gcc.gnu.org/bugzilla/show_bug.cgi?id=107948 fix: https://gcc.gnu.org/git/gitweb.cgi?p=gcc.git;h=0b737090a69624dea5318c380620283f0321a92e original:

[Geoffrey1014]

I got a false negative error when compiling the following program with gcc(trunk) -fanalyzer -O0. https://godbolt.org/z/jvcbr3xfc

extern void __analyzer_eval (int);

void foo(int width) {
    int i = 0;
    int base;
    if (width > 0){
        __analyzer_eval(i == 0);
        __analyzer_eval(width > 0);
        __analyzer_eval(width - i > 0);
        __analyzer_eval(i - width < 0);
        if (i - width < 0) {
        base = 512;
        }
    }
    base+=1;
}

Output:

<source>: In function 'foo':
<source>:7:9: warning: TRUE
    7 |         __analyzer_eval(i == 0);
      |         ^~~~~~~~~~~~~~~~~~~~~~~
<source>:8:9: warning: TRUE
    8 |         __analyzer_eval(width > 0);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:9:9: warning: TRUE
    9 |         __analyzer_eval(width - i > 0);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:10:9: warning: UNKNOWN
   10 |         __analyzer_eval(i - width < 0);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:15:9: warning: use of uninitialized value 'base' [CWE-457] [-Wanalyzer-use-of-uninitialized-value]
   15 |     base+=1;
      |     ~~~~^~~
  'foo': events 1-3
    |
    |    5 |     int base;
    |      |         ^~~~
    |      |         |
    |      |         (1) region created on stack here
    |      |         (2) capacity: 4 bytes
    |......
    |   15 |     base+=1;
    |      |     ~~~~~~~
    |      |         |
    |      |         (3) use of uninitialized value 'base' here
    |

GCC Static Analyzer doesn't realize 0 - width < 0 is always true when width > 0 and width is int type，hence it reports a wrong use-of-uninitialized-value warning.

The analysis result shows that analyzer knows "width - i > 0" is true but does not know the equivalence formula " i - width < 0" is also true.

[Geoffrey1014]

The original case：GCC Analyzer doesn't realize '0 % x' is 0. https://godbolt.org/z/619bh6onn

#include <assert.h>
#include <stdbool.h>
extern void __analyzer_eval (int);

void decode(unsigned width) {
  assert(width > 0);

  int base;
  bool inited = false;

  int i = 0;
    __analyzer_eval(i % width == 0);
  if (i % width == 0) {
      __analyzer_eval(i % width == 0);
    base = 512;
    inited = true;
  }
 __analyzer_eval(i % width == 0);
//   assert(inited); // <- if i uncomment this, the warning is gone.
  base+=1;

  if (base >> 10)
    assert(false);
}

<source>: In function 'decode':
<source>:12:5: warning: UNKNOWN
   12 |     __analyzer_eval(i % width == 0);
      |     ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:14:7: warning: TRUE
   14 |       __analyzer_eval(i % width == 0);
      |       ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:18:2: warning: FALSE
   18 |  __analyzer_eval(i % width == 0);
      |  ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:18:2: warning: TRUE
<source>:20:7: warning: use of uninitialized value 'base' [CWE-457] [-Wanalyzer-use-of-uninitialized-value]
   20 |   base+=1;
      |   ~~~~^~~
  'decode': events 1-2
    |
    |    8 |   int base;
    |      |       ^~~~
    |      |       |
    |      |       (1) region created on stack here
    |      |       (2) capacity: 4 bytes
    |
  'decode': event 3
    |
    |    6 |   assert(width > 0);
    |      |   ^~~~~~
    |      |   |
    |      |   (3) following 'true' branch (when 'width != 0')...
    |
  'decode': events 4-7
    |
    |    9 |   bool inited = false;
    |      |        ^~~~~~
    |      |        |
    |      |        (4) ...to here
    |......
    |   13 |   if (i % width == 0) {
    |      |      ~  
    |      |      |
    |      |      (5) following 'false' branch...
    |......
    |   18 |  __analyzer_eval(i % width == 0);
    |      |                  ~~~~~~~~~
    |      |                    |
    |      |                    (6) ...to here
    |   19 | //   assert(inited); // <- if i uncomment this, the warning is gone.
    |   20 |   base+=1;
    |      |   ~~~~~~~
    |      |       |
    |      |       (7) use of uninitialized value 'base' here
    |

[Geoffrey1014]

But if i use the option -fanalyzer -O1, the bug goes away. So the optimization can realisze '0 % x' is 0

https://godbolt.org/z/5o9ezx3eK

[ghost]

CSA can handle it with Z3: https://github.com/llvm/llvm-project/issues/62463