[Bug analyzer/109194] New: GCC Static Analyzer does not know "a+3 > b+1" in the true branch of "if (a > b) ", but it knows "a+2 > b+1"

[Bug analyzer/109194] New: GCC Static Analyzer does not know "a+3 > b+1" in the true branch of "if (a > b) ", but it knows "a+2 > b+1"

[geoffreydgr at icloud dot com]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=109194

            Bug ID: 109194
           Summary: GCC Static Analyzer does not know "a+3 > b+1"  in the
                    true branch of "if (a > b) ", but it knows "a+2 > b+1"
           Product: gcc
           Version: 13.0
            Status: UNCONFIRMED
          Severity: normal
          Priority: P3
         Component: analyzer
          Assignee: dmalcolm at gcc dot gnu.org
          Reporter: geoffreydgr at icloud dot com
  Target Milestone: ---

I found a problem that GCC Static Analyzer does not know "a+3 > b+1" (line 14)
in the true branch of "if (a > b) ", but it knows "a+2 > b+1"  (line 13) .

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

See it live: https://godbolt.org/z/61nMxo7Kv

Input:
```c
#include <stdint.h>
#include <stdbool.h>

int main(int a, int b, int c, int d) {
    if ((a>b)){
        __analyzer_eval(a>b);
        __analyzer_eval(!(a>b) == false);
        __analyzer_eval(-a < -b);
        __analyzer_eval(0-a < 0-b);
        __analyzer_eval( a+0 > b+0);
        __analyzer_eval( a+1 > b+1);
        __analyzer_eval( a+2 > b+2);
        __analyzer_eval( a+2 > b+1);
        __analyzer_eval( a+3 > b+1);
        __analyzer_eval( a*0 > b*0 == false);
        __analyzer_eval( a*1 > b*1);
        __analyzer_eval( a*2 > b*2);
        __analyzer_eval( a*3 > b*2);
    }
}
```
Output:
```bash
<source>: In function 'main':
<source>:6:9: warning: implicit declaration of function '__analyzer_eval'
[-Wimplicit-function-declaration]
    6 |         __analyzer_eval(a>b);
      |         ^~~~~~~~~~~~~~~
<source>:6:9: warning: TRUE
    6 |         __analyzer_eval(a>b);
      |         ^~~~~~~~~~~~~~~~~~~~
<source>:7:9: warning: TRUE
    7 |         __analyzer_eval(!(a>b) == false);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:8:9: warning: TRUE
    8 |         __analyzer_eval(-a < -b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~
<source>:9:9: warning: TRUE
    9 |         __analyzer_eval(0-a < 0-b);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:10:9: warning: TRUE
   10 |         __analyzer_eval( a+0 > b+0);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:11:9: warning: TRUE
   11 |         __analyzer_eval( a+1 > b+1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:12:9: warning: TRUE
   12 |         __analyzer_eval( a+2 > b+2);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:13:9: warning: TRUE
   13 |         __analyzer_eval( a+2 > b+1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:14:9: warning: UNKNOWN
   14 |         __analyzer_eval( a+3 > b+1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:15:9: warning: TRUE
   15 |         __analyzer_eval( a*0 > b*0 == false);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:16:9: warning: TRUE
   16 |         __analyzer_eval( a*1 > b*1);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:17:9: warning: TRUE
   17 |         __analyzer_eval( a*2 > b*2);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
<source>:18:9: warning: TRUE
   18 |         __analyzer_eval( a*3 > b*2);
      |         ^~~~~~~~~~~~~~~~~~~~~~~~~~~
Compiler returned: 0

```

[Bug analyzer/109194] GCC Static Analyzer does not know "a+3 > b+1" in the true branch of "if (a > b) ", but it knows "a+2 > b+1"

[dmalcolm at gcc dot gnu.org]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=109194

--- Comment #1 from David Malcolm <dmalcolm at gcc dot gnu.org> ---
Well, strictly speaking not all of these are true; consider

  a == INT_MAX
  b == INT_MAX - 1

Then a > b, but:

* a + 1 is, I believe, undefined, but we may want to treat it as INT_MIN

* b + 1 is INT_MAX

* with those semantics, a + 1 > b + 1 is INT_MIN > INT_MAX which is false

...and you can pick other values for b e.g. INT_MAX - 2 to get other results.

The constraint manager code is playing rather fast-and-loose in places.

I've been experimenting with adding an SMT solver (PR 104940) which would
support figuring out such cases precisely based on bit-vectors.

[Bug analyzer/109194] GCC Static Analyzer does not know "a+3 > b+1" in the true branch of "if (a > b) ", but it knows "a+2 > b+1"

[dmalcolm at gcc dot gnu.org]

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=109194

David Malcolm <dmalcolm at gcc dot gnu.org> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
             Status|UNCONFIRMED                 |RESOLVED
         Resolution|---                         |DUPLICATE

--- Comment #2 from David Malcolm <dmalcolm at gcc dot gnu.org> ---
As also noted in bug 109193, the constraint_manager has some heuristics to try
to handle common cases, but ultimately we're probably going to want to hand
this off to an SMT solver (PR 104940)

*** This bug has been marked as a duplicate of bug 104940 ***