[Bug analyzer/110090] New: -fanalyze sometimes assumes contradictory conditions to be valid at the same time during path exploration

[Bug analyzer/110090] New: -fanalyze sometimes assumes contradictory conditions to be valid at the same time during path exploration

[girgias at php dot net]

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

            Bug ID: 110090
           Summary: -fanalyze sometimes assumes contradictory conditions
                    to be valid at the same time during path exploration
           Product: gcc
           Version: 13.1.1
            Status: UNCONFIRMED
          Severity: normal
          Priority: P3
         Component: analyzer
          Assignee: dmalcolm at gcc dot gnu.org
          Reporter: girgias at php dot net
  Target Milestone: ---

Hello,

I've run -fanalyze on the php-src code base and the analyzer will flag issues
which cannot happen as it will explore a branch where some variable/value is
assumed to be false, but then explore a branch where it assumes this same
variable/value to be true, resulting in a false positive warning.

The command used to build php-src was the following one:

./configure --disable-all CFLAGS="-fanalyzer
-Wno-analyzer-use-of-uninitialized-value -ggdb3" -C --enable-debug

And one relevant extract which shows this issue is:

/home/girgias/Dev/php-src/ext/date/php_date.c:3112:9: note: in expansion of
macro ‘RETURN_STR’
    | 3112 |         RETURN_STR(date_format(format, format_len, dateobj->time,
dateobj->time->is_localtime));
    |      |         ^~~~~~~~~~
    |
    +--> ‘date_format’: events 7-18
           |
           |  675 | static zend_string *date_format(const char *format, size_t
format_len, timelib_time *t, bool localtime)
           |      |                     ^~~~~~~~~~~
           |      |                     |
           |      |                     (7) entry to ‘date_format’
           |......
           |  681 |         timelib_time_offset *offset = NULL;
           |      |                              ~~~~~~
           |      |                              |
           |      |                              (8) ‘offset’ is NULL
           |......
           |  686 |         if (!format_len) {
           |      |            ~         
           |      |            |
           |      |            (9) following ‘false’ branch (when ‘format_len
!= 0’)...
           |......
           |  690 |         if (localtime) {
           |      |            ~         
           |      |            |
           |      |            (10) ...to here
           |      |            (11) following ‘false’ branch (when ‘localtime
== 0’)...
           |......
           |  712 |         for (i = 0; i < format_len; i++) {
           |      |              ~~~~~  ~~~~~~~~~~~~~~
           |      |                |      |
           |      |                |      (13) following ‘true’ branch (when ‘i
< format_len’)...
           |      |                (12) ...to here
           |  713 |                 rfc_colon = 0;
           |      |                 ~~~~~~~~~~~~~
           |      |                           |
           |      |                           (14) ...to here
           |  714 |                 switch (format[i]) {
           |      |                 ~~~~~~
           |      |                 |
           |      |                 (15) following ‘case 101:’ branch...
           |......
           |  786 |                         case 'e': if (!localtime) {
           |      |                         ~~~~         ~
           |      |                         |            |
           |      |                         |            (17) following ‘false’
branch...
           |      |                         (16) ...to here
           |......
           |  789 |                                                   switch
(t->zone_type) {
           |      |                                                          
~~~~~~~~~~~~
           |      |                                                           
|
           |      |                                                           
(18) ...to here
           |
         ‘date_format’: event 19



As you can see, on the bit where it analyzes line 690 it assumes localtime ==
0, thus following the false branch.
However, when analysing the if condition on line 786 it *also* follows the
false branch when this cannot happen as localtime == 0 and therefore *must* go
through the true branch.

A lot of the noise, and false positives within php-src seem to come from issues
similar to this.

[Bug analyzer/110090] -fanalyze sometimes assumes contradictory conditions to be valid at the same time during path exploration

[dmalcolm at gcc dot gnu.org]

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

--- Comment #1 from David Malcolm <dmalcolm at gcc dot gnu.org> ---
Thanks for filing this bug report, and sorry for not responding before.

Are you still able to reproduce this?

If so, please can you use -save-temps to generated a preprocessed file (.i)
that reproduces the issue, and attach it (and also post the precise
command-line flags you're seeing it with).  

See https://gcc.gnu.org/bugs/#need

Thanks!