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

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

[dmalcolm at gcc dot 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.

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

[dmalcolm at gcc dot gnu.org]

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

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

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

--- Comment #1 from David Malcolm <dmalcolm at gcc dot gnu.org> ---
Tim: I'm CCing you in case you want to work on this; otherwise I might tackle
this in a few weeks.

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

[cvs-commit at gcc dot gnu.org]

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

--- Comment #2 from CVS Commits <cvs-commit at gcc dot gnu.org> ---
The master branch has been updated by Tim Lange <tlange@gcc.gnu.org>:

https://gcc.gnu.org/g:7a6564c9b277d9f93582605758d57457de696deb

commit r13-2546-g7a6564c9b277d9f93582605758d57457de696deb
Author: Tim Lange <mail@tim-lange.me>
Date:   Wed Sep 7 17:41:28 2022 +0200

    analyzer: support for symbolic values in the out-of-bounds checker
[PR106625]

    This patch adds support for reasoning about the inequality of two symbolic
    values in the special case specifically suited for reasoning about
    out-of-bounds past the end of the buffer. With this patch, the analyzer
    catches off-by-one errors and more even when the offset and capacity is
    symbolic.

    Regrtested on Linux x86_64 and tested on coreutils, curl, httpd and
    openssh as usual.

    2022-09-07  Tim Lange  <mail@tim-lange.me>

    gcc/analyzer/ChangeLog:

            PR analyzer/106625
            * analyzer.h (region_offset): Eliminate m_is_symbolic member.
            * region-model-impl-calls.cc (region_model::impl_call_realloc):
            Refine implementation to be more precise.
            * region-model.cc (class symbolic_past_the_end):
            Abstract diagnostic class to complain about accesses past the end
            with symbolic values.
            (class symbolic_buffer_overflow):
            Concrete diagnostic class to complain about buffer overflows with
            symbolic values.
            (class symbolic_buffer_overread):
            Concrete diagnostic class to complain about buffer overreads with
            symbolic values.
            (region_model::check_symbolic_bounds): New function.
            (maybe_get_integer_cst_tree): New helper function.
            (region_model::check_region_bounds):
            Add call to check_symbolic_bounds if offset is not concrete.
            (region_model::eval_condition_without_cm):
            Add support for EQ_EXPR and GT_EXPR with binaryop_svalues.
            (is_positive_svalue): New hleper function.
            (region_model::symbolic_greater_than):
            New function to handle GT_EXPR comparisons with symbolic values.
            (region_model::structural_equality): New function to compare
            whether two svalues are structured the same, i.e. evaluate to
            the same value.
            (test_struct): Reflect changes to region::calc_offset.
            (test_var): Likewise.
            (test_array_2): Likewise and add selftest with symbolic i.
            * region-model.h (class region_model): Add check_symbolic_bounds,
            symbolic_greater_than and structural_equality.
            * region.cc (region::get_offset):
            Reflect changes to region::calc_offset.
            (region::calc_offset):
            Compute the symbolic offset if the offset is not concrete.
            (region::get_relative_symbolic_offset): New function to return the
            symbolic offset in bytes relative to its parent.
            (field_region::get_relative_symbolic_offset): Likewise.
            (element_region::get_relative_symbolic_offset): Likewise.
            (offset_region::get_relative_symbolic_offset): Likewise.
            (bit_range_region::get_relative_symbolic_offset): Likewise.
            * region.h: Add get_relative_symbolic_offset.
            * store.cc (binding_key::make):
            Reflect changes to region::calc_offset.
            (binding_map::apply_ctor_val_to_range): Likewise.
            (binding_map::apply_ctor_pair_to_child_region): Likewise.
            (binding_cluster::bind_compound_sval): Likewise.
            (binding_cluster::get_any_binding): Likewise.
            (binding_cluster::maybe_get_compound_binding): Likewise.

    gcc/ChangeLog:

            PR analyzer/106625
            * doc/invoke.texi:
            State that the checker also reasons about symbolic values.

    gcc/testsuite/ChangeLog:

            PR analyzer/106625
            * gcc.dg/analyzer/data-model-1.c: Change expected result.
            * gcc.dg/analyzer/out-of-bounds-5.c: New test.
            * gcc.dg/analyzer/out-of-bounds-realloc-grow.c: New test.
            * gcc.dg/analyzer/symbolic-gt-1.c: New test.

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

[dmalcolm at gcc dot gnu.org]

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

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

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

--- Comment #3 from David Malcolm <dmalcolm at gcc dot gnu.org> ---
Tim implemented a version of this that supports the specific case above, in the
above patch; marking this as resolved.