[Bug analyzer/108598] New: GCC analyzer reports false positive for buffer overflow/over-read in C code with a write in middle of an array.

[Bug analyzer/108598] New: GCC analyzer reports false positive for buffer overflow/over-read in C code with a write in middle of an array.

[psimovec at redhat dot com]

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

            Bug ID: 108598
           Summary: GCC analyzer reports false positive for buffer
                    overflow/over-read in C code with a write in middle of
                    an array.
           Product: gcc
           Version: 13.0
            Status: UNCONFIRMED
          Severity: normal
          Priority: P3
         Component: analyzer
          Assignee: dmalcolm at gcc dot gnu.org
          Reporter: psimovec at redhat dot com
  Target Milestone: ---

In this test case, gcc analyzer found 3 new true positives, but one False
positive. (Compared to analyzer in gcc 12)

It reports an error "write of 4 bytes to beyond the end of the region" with
write in middle of array.

Test case:
#include <stdlib.h>
extern int __VERIFIER_nondet_int(void);
extern char __VERIFIER_nondet_char(void);

int main(void)
{
    int length = 99;

    int *arr = alloca(length);

    for (int i = 0; i < length; i++) {
        arr[i] = __VERIFIER_nondet_int();
    }

    for (int i = 0; i < length; i++) {
        if (arr[i] == '\0')
            arr[i]++;
    }

    arr[length / 2 + 1] = '\0'; // <- false positive here
    int *a = arr;
    int *b = arr + length - 1;
    int tmp;
    while (*a != 0 && *b != 0) {
        tmp = *a;
        *a = *b;
        *b = tmp;
        a++;
        b--;
    }
    return 0;
}

GCC analyzer reported errors:
Error: GCC_ANALYZER_WARNING (CWE-121): <--- False positive
./test-0006.c: scope_hint: In function 'main'
./test-0006.c:20:25: warning[-Wanalyzer-out-of-bounds]: stack-based buffer
overflow
/usr/include/stdlib.h:587: included_from: Included from here.
./test-0006.c:1: included_from: Included from here.
./test-0006.c:20:25: note: write of 4 bytes to beyond the end of the region

Error: GCC_ANALYZER_WARNING (CWE-126): 
./test-0006.c:24:23: warning[-Wanalyzer-out-of-bounds]: stack-based buffer
over-read
./test-0006.c:24:23: note: read of 4 bytes from after the end of the region

Error: GCC_ANALYZER_WARNING (CWE-126):
./test-0006.c:26:14: warning[-Wanalyzer-out-of-bounds]: stack-based buffer
over-read
./test-0006.c:26:14: note: read of 4 bytes from after the end of the region

Error: GCC_ANALYZER_WARNING (CWE-121):
./test-0006.c:27:12: warning[-Wanalyzer-out-of-bounds]: stack-based buffer
overflow
./test-0006.c:27:12: note: write of 4 bytes to beyond the end of the region

---------------------------------------------
gcc (GCC) 13.0.1 20230127 (Red Hat 13.0.1-0)
Fedora release 38 (Rawhide)

[Bug analyzer/108598] GCC analyzer reports false positive for buffer overflow/over-read in C code with a write in middle of an array.

[dmalcolm at gcc dot gnu.org]

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

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

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

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

It looks like the tool you're using to collate diagnostics is omitting
important information from the report.

Specifically, if I try the example with Compiler Explorer here:
  https://godbolt.org/z/sWon4rqG9
...I see useful information within the execution paths that isn't in the text
you pasted into this BZ report.

In particular, the full report from -fanalyzer shows that:

    |    9 |     int *arr = alloca(length);
    |      |                ^~~~~~
    |      |                |
    |      |                (1) capacity: 99 bytes
    |
[...snip...]

    |   20 |     arr[length / 2 + 1] = '\0'; // <- false positive here
    |      |     ~~~~~~~~~~~~~~~~~~~~~~~~~~
    |      |                         |
    |      |                         (6) out-of-bounds write from byte 200 till
byte 203 but region ends at byte 99
    |

The issue is that "arr" is an int *, not a char *, and hence, given a target
where sizeof(int) == 4, each access of arr[x] is a 4-byte access starting at
byte (x * 4).  Hence arr[length / 2 + 1] == arr[50], and accessing arr[50] is
accessing bytes 200-203, but the buffer is only 99 bytes in size.

So if I'm reading this right, this is a true positive, so I'm going to mark it
as "RESOLVED INVALID".

PVS Studio also complains about it:
  https://godbolt.org/z/hqbKKs6hd

That said, valgrind doesn't seem to complain about this write for some reason:

#include <stdlib.h>

int main(void)
{
    int length = 99;

    int *arr = alloca(length);

    arr[length / 2 + 1] = '\0';

    return 0;
}

There's also a missing warning from -Wanalyzer-allocation-size when the alloca
result is assigned to "int *", which I've filed as PR analyzer/108616.

[Bug analyzer/108598] GCC analyzer reports false positive for buffer overflow/over-read in C code with a write in middle of an array.

[psimovec at redhat dot com]

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

--- Comment #2 from Pavel Šimovec <psimovec at redhat dot com> ---
Thanks for the insightful response.

We agree with the resolution, and I have missed that one of the tools actually
verifies the error:
https://github.com/aufover/aufover-benchmark/blob/77f9432747988bfbfb3a943b246c00904086b234/tests/single-c/arrays-and-loops/reverse-array-bad-0006/output-exp%40symbiotic#L2

It just found the error sooner - already inside the first loop:
for (int i = 0; i < length; i++) {
    arr[i] = __VERIFIER_nondet_int();
}

[Bug analyzer/108598] GCC analyzer reports false positive for buffer overflow/over-read in C code with a write in middle of an array.

[dmalcolm at gcc dot gnu.org]

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

--- Comment #3 from David Malcolm <dmalcolm at gcc dot gnu.org> ---
Yeah, it would be good if -fanalyzer detected such issues within loops, and
identified the iteration at which the access goes out-of-bounds.  Handling that
is bug 108432 (which I'm treating as an RFE).

Thanks for the link to aufover-benchmark; taking a look now.