[llvm-bugs] [Bug 51940] New: [Analyzer] New false-positive finding by [core.DivideZero]

[via llvm-bugs]

https://bugs.llvm.org/show_bug.cgi?id=51940

            Bug ID: 51940
           Summary: [Analyzer] New false-positive finding by
                    [core.DivideZero]
           Product: clang
           Version: trunk
          Hardware: PC
                OS: Windows NT
            Status: NEW
          Severity: enhancement
          Priority: P
         Component: Static Analyzer
          Assignee: dcoughlin at apple.com
          Reporter: tauchris at utexas.edu
                CC: dcoughlin at apple.com, llvm-bugs at lists.llvm.org

Created attachment 25283
  --> https://bugs.llvm.org/attachment.cgi?id=25283&action=edit
Reproducer

The attached reproducer triggers a false positive from [core.DivideZero] at
line 28:

  CMD> cat -n reduced4.c 
     1  typedef int AT;
     2  typedef int BT;
     3  typedef struct {
     4    BT c;
     5  } DS;
     6  typedef struct {
     7    AT e;
     8    DS f;
     9  } GS;
    10  typedef struct {
    11    AT h;
    12  } KS;
    13  void j(KS *);
    14  struct QS *l(GS *m) {
    15    AT n = m->e / 40;
    16    if ( n % 40 == 0 ) { n = 1; }
    17    BT c = m->f.c;
    18    AT h = c * n;
    19    struct QS *o = 0;
    20    KS p;
    21    for (; h;)
    22      ;
    23    j(&p);
    24    for (AT q = 0; q < c; q++)
    25      ;
    26    AT ant;
    27    for (AT job = 0; p.h;)
    28      ant = job / n;
    29    (void)ant;
    30    return o;
    31  }

This is a false positive because of line 16, which guarantees n cannot be zero.
 I don't see any opportunities in this code for n to escape, but I may have
missed something.  This new warning appeared after commit
https://reviews.llvm.org/rG8ddbb442b6e87efc9c6599280740c6f4fc40963d. (Same
input file does not trigger a warning prior to this commit.)

Note that removing (commenting out) line 16 does not change behavior either
before or after commit 8ddbb442b6e -- with this commit, the warning is still
issued, and prior to this commit, there is still no warning.  So, I doubt that
the commit 8ddbb442b6e is actually to *blame* for this false positive --
perhaps it just increased the coverage of [core.DivideZero], and that
necessarily includes some new false positives in cases where the analyzer
cannot already recognize/reason about constraint changes as side effects of
code like line 16?  Not sure.

Running this with attached input file as:

  bash> clang -Xanalyzer -analyzer-werror -Xanalyzer -analyzer-output=text
--analyze reduced4.c 

Gives:

   reduced4.c:28:15: error: Division by zero [core.DivideZero]
      ant = job / n;
            ~~~~^~~
  reduced4.c:15:3: note: 'n' initialized here
    AT n = m->e / 40;
    ^~~~
  reduced4.c:16:8: note: Assuming the condition is false
    if ( n % 40 == 0 ) { n = 1; }
         ^~~~~~~~~~~
  reduced4.c:16:3: note: Taking false branch
    if ( n % 40 == 0 ) { n = 1; }
    ^
  reduced4.c:21:3: note: Loop condition is false. Execution continues on line
23
    for (; h;)
    ^
  reduced4.c:24:18: note: Assuming 'q' is < 'c'
    for (AT q = 0; q < c; q++)
                   ^~~~~
  reduced4.c:24:3: note: Loop condition is true.  Entering loop body
    for (AT q = 0; q < c; q++)
    ^
  reduced4.c:24:18: note: Assuming 'q' is >= 'c'
    for (AT q = 0; q < c; q++)
                   ^~~~~
  reduced4.c:24:3: note: Loop condition is false. Execution continues on line
26
    for (AT q = 0; q < c; q++)
    ^
  reduced4.c:27:3: note: Loop condition is true.  Entering loop body
    for (AT job = 0; p.h;)
    ^
  reduced4.c:28:15: note: Division by zero
      ant = job / n;
            ~~~~^~~
  1 error generated.

-- 
You are receiving this mail because:
You are on the CC list for the bug.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-bugs/attachments/20210922/d2ddba12/attachment.html>