[Bug analyzer/95000] New: -fanalyzer confused by switch

[Bug analyzer/95000] New: -fanalyzer confused by switch

[felix-gcc at fefe dot de]

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

            Bug ID: 95000
           Summary: -fanalyzer confused by switch
           Product: gcc
           Version: 10.1.0
            Status: UNCONFIRMED
          Severity: normal
          Priority: P3
         Component: analyzer
          Assignee: dmalcolm at gcc dot gnu.org
          Reporter: felix-gcc at fefe dot de
  Target Milestone: ---

Consider this contrived test code:

void proof(char* x) {
  char* y=0;
  switch (*x) {
  case 'a':
    y="foo";
  case 'b':
    if (*x=='a') *y='b';
  }
}

-fanalyzer will warn about the *y='b' statement, that y might be NULL here.
However if *x=='a' then we got here via the case 'a' case which initialized it.

Other than this minor false positive issue thank you for -fanalyzer! It has
already found a few bugs for me!

[Bug analyzer/95000] -fanalyzer confused by switch

[jakub at gcc dot gnu.org]

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

Jakub Jelinek <jakub at gcc dot gnu.org> changed:

           What    |Removed                     |Added
----------------------------------------------------------------------------
                 CC|                            |jakub at gcc dot gnu.org

--- Comment #1 from Jakub Jelinek <jakub at gcc dot gnu.org> ---
That test is broken anyway, because you can't store into a string literal.

[Bug analyzer/95000] -fanalyzer confused by switch

[felix-gcc at fefe dot de]

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

--- Comment #2 from felix-gcc at fefe dot de ---
The false positive also happens if you fix that.
In fact, my original (much longer) code does not try to write to read-only
memory.

I put that in my test case in the hope that somebody would mention it, so I can
point out that gcc -fanalyzer could warn about it, but doesn't.

So thank you for falling for my trap. :-)

[Bug analyzer/95000] -fanalyzer confused by switch

[dmalcolm at gcc dot gnu.org]

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

--- Comment #3 from David Malcolm <dmalcolm at gcc dot gnu.org> ---
Thanks for filing this bug.

I've filed PR analyzer/95007 to track the RFE for a warning about writes to a
string literal.

Clearly there's a bug somewhere in the handling for the path condition for the
warning in comment #0; am investigating.

[Bug analyzer/95000] -fanalyzer confused by switch on non-int type

[dmalcolm at gcc dot gnu.org]

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

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

           What    |Removed                     |Added
----------------------------------------------------------------------------
     Ever confirmed|0                           |1
             Status|UNCONFIRMED                 |ASSIGNED
   Last reconfirmed|                            |2020-05-08
            Summary|-fanalyzer confused by      |-fanalyzer confused by
                   |switch                      |switch on non-int type

--- Comment #4 from David Malcolm <dmalcolm at gcc dot gnu.org> ---
This turns out to be a problem with tracking path-conditions with casts.

Switch statements on a non-int type (such as char) have an implicit cast to int
and trigger the issue.

Consider this test case, using the not-quite-a-builtin "__analyzer_eval" to
evaluate a condition.  In each case we expect  __analyzer_eval to emit "TRUE":

----------------------------------------------------------------------
extern void __analyzer_eval (int);

void test_switch_char(char x) {
  switch (x) {
  case 'b':
    __analyzer_eval (x == 'b');
  }
}

void test_switch_int(int x) {
  switch (x) {
  case 97:
    __analyzer_eval (x == 97);
  }
}

void test_if_char(char x) {
  if (x == 'b')
    __analyzer_eval (x == 'b');
}

void test_if_int(int x) {
  if (x == 97)
    __analyzer_eval (x == 97);
}
----------------------------------------------------------------------

I get this output (note that the output is in reverse order):

s.c: In function ‘test_if_int’:
s.c:24:5: warning: TRUE
   24 |     __analyzer_eval (x == 97);
      |     ^~~~~~~~~~~~~~~~~~~~~~~~~
s.c: In function ‘test_if_char’:
s.c:19:5: warning: TRUE
   19 |     __analyzer_eval (x == 'b');
      |     ^~~~~~~~~~~~~~~~~~~~~~~~~~
s.c: In function ‘test_switch_int’:
s.c:13:5: warning: TRUE
   13 |     __analyzer_eval (x == 97);
      |     ^~~~~~~~~~~~~~~~~~~~~~~~~
s.c: In function ‘test_switch_char’:
s.c:6:5: warning: UNKNOWN
    6 |     __analyzer_eval (x == 'b');
      |     ^~~~~~~~~~~~~~~~~~~~~~~~~~

where we get it wrong for test_switch_char.

At the gimple level, we have:

test_switch_char (char x)
{
  int _1;
  _Bool _2;
  int _3;

  <bb 2> :
  _1 = (int) x_5(D);
  if (_1 == 98)
    goto <bb 3>; [INV]
  else
    goto <bb 4>; [INV]

  <bb 3> :
<L0>:
  _2 = x_5(D) == 98;
  _3 = (int) _2;
  __analyzer_eval (_3);

  <bb 4> :
<L1>:
  return;

}

The cast here:
  _1 = (int) x_5(D);
  if (_1 == 98)
seems to thwart my constraint-tracking.

If I use -fno-analyzer-state-purge it at least "knows" that _1 == 98 within the
"case" BB.

I'm working on a rewrite of state-tracking for GCC 11 that ought to better
handle casts.

[Bug analyzer/95000] -fanalyzer confused by switch on non-int type

[dimhen at gmail dot com]

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

--- Comment #5 from Dmitry G. Dyachenko <dimhen at gmail dot com> ---
gcc version 11.0.0 20210210 (experimental) [master revision
bd0e37f68a3:deed5164277:72932511053596091ad291539022b51d9f2ba418]

PASS for me

[Bug analyzer/95000] -fanalyzer confused by switch on non-int type

[dmalcolm at gcc dot gnu.org]

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

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

           What    |Removed                     |Added
----------------------------------------------------------------------------
         Depends on|                            |104940

--- Comment #6 from David Malcolm <dmalcolm at gcc dot gnu.org> ---
Still happens on trunk; adding to SMT tracker.


Referenced Bugs:

https://gcc.gnu.org/bugzilla/show_bug.cgi?id=104940
[Bug 104940] RFE: integrate analyzer with an SMT solver

[Bug analyzer/95000] -fanalyzer confused by switch on non-int type

[cvs-commit at gcc dot gnu.org]

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

--- Comment #7 from CVS Commits <cvs-commit at gcc dot gnu.org> ---
The master branch has been updated by David Malcolm <dmalcolm@gcc.gnu.org>:

https://gcc.gnu.org/g:d1d95846e3c901faea6fe36a36e47b9169f5b133

commit r12-7659-gd1d95846e3c901faea6fe36a36e47b9169f5b133
Author: David Malcolm <dmalcolm@redhat.com>
Date:   Tue Mar 15 17:56:29 2022 -0400

    analyzer: add test coverage for PR 95000

    PR analyzer/95000 isn't fixed yet; add test coverage with XFAILs.

    gcc/testsuite/ChangeLog:
            PR analyzer/95000
            * gcc.dg/analyzer/pr95000-1.c: New test.

    Signed-off-by: David Malcolm <dmalcolm@redhat.com>