[Bug analyzer/106625] New: RFE: support some symbolic values in -Wanalyzer-out-of-bounds

["dmalcolm at gcc dot gnu.org" <gcc-bugzilla@gcc.gnu.org>]

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

            Bug ID: 106625
           Summary: RFE: support some symbolic values in
                    -Wanalyzer-out-of-bounds
           Product: gcc
           Version: 13.0
            Status: UNCONFIRMED
          Severity: normal
          Priority: P3
         Component: analyzer
          Assignee: dmalcolm at gcc dot gnu.org
          Reporter: dmalcolm at gcc dot gnu.org
  Target Milestone: ---

Currently -Wanalyzer-out-of-bounds only warns when:
* the size of the memory access is constant, rather than symbolic, and 
* the capacity of the underlying memory region being accessed is constant,
rather than symbolic, and
* the offset of the memory access is constant, rather than symbolic

I'd like to eventually generalize the warning so that it can "do something
sensible" when at least some of the above are symbolic - for some meaning of
"something sensible".  I'm not quite sure what subset we can support, but
-Wanalyzer-out-of-bounds should probably continue to restrict itself to
"definitely out-of-bounds" cases.

For example, consider the classic mistake in C of confusing the size vs length
of a 0-terminated string:

char *
test_concat (const char *x, const char *y)
{
  size_t len_x = __builtin_strlen (x);
  size_t len_y = __builtin_strlen (y);
  size_t sz = len_x + len_y; // BUG (root cause): forgot to add 1 for
terminator;
  char *result = __builtin_malloc (sz);
  if (!result)
    return NULL;
  __builtin_memcpy (result, x, len_x);
  __builtin_memcpy (result + len_x, y, len_y);
  result[len_x + len_y] = '\0'; // BUG (symptom): off-by-one out-of-bounds
write to heap
  return result;
}

Currently -Wanalyzer-out-of-bounds doesn't warn for this; it would be great if
void region_model::check_region_bounds could handle this.  Specifically, in
this case, although the size of the access:
   result[len_x + len_y] = '\0';
is constant (1 byte), the offset of the access is symbolic (len_x + len_y), and
the capacity of "result" is symbolic.  That said the symbolic offset of the
access and symbolic capacity of the base region are directly related, and the
former is definitely wrong with respect to the latter.