[all-commits] [llvm/llvm-project] de2547: [analyzer] Fix comparison logic in ArrayBoundCheck...

[DonatNagyE via All-commits]

  Branch: refs/heads/main
  Home:   https://github.com/llvm/llvm-project
  Commit: de2547329b41ad6ea4ea876d12731bde5a6b64c5
      https://github.com/llvm/llvm-project/commit/de2547329b41ad6ea4ea876d12731bde5a6b64c5
  Author: Donát Nagy <donat.nagy at ericsson.com>
  Date:   2023-04-26 (Wed, 26 Apr 2023)

  Changed paths:
    M clang/lib/StaticAnalyzer/Checkers/ArrayBoundCheckerV2.cpp
    A clang/test/Analysis/array-bound-v2-constraint-check.c
    R clang/test/Analysis/out-of-bounds-false-positive.c

  Log Message:
  -----------
  [analyzer] Fix comparison logic in ArrayBoundCheckerV2

The prototype checker alpha.security.ArrayBoundV2 performs two
comparisons to check that in an expression like Array[Index]
    0 <= Index < length(Array)
holds. These comparisons are handled by almost identical logic: the
inequality is first rearranged by getSimplifiedOffsets(), then evaluated
with evalBinOpNN().

However the simplification used "naive" elementary mathematical
schematics, but evalBinOpNN() performed the signed -> unsigned
conversions described in the C/C++ standards, and this confusion led to
wildly inaccurate results: false positives from the lower bound check
and false negatives from the upper bound check.

This commit eliminates the code duplication by moving the comparison
logic into a separate function, then adds an explicit check to this
unified code path, which handles the problematic case separately.

In addition to this, the commit also cleans up a testcase that was
demonstrating the presence of this problem. Note that while that
testcase was failing with an overflow error, its actual problem was in
the underflow handler logic:
(0) The testcase introduces a five-element array "char a[5]" and an
    unknown argument "size_t len"; then evaluates "a[len+1]".
(1) The underflow check tries to determine whether "len+1 < 0" holds.
(2) This inequality is rearranged to "len < -1".
(3) evalBinOpNN() evaluates this with the schematics of C/C++ and
    converts -1 to the size_t value SIZE_MAX.
(4) The engine concludes that len == SIZE_MAX, because otherwise we'd
    have an underflow here.
(5) The overflow check tries to determine whether "len+1 >= 5".
(6) This inequality is rearranged to "len >= 4".
(7) The engine substitutes len == SIZE_MAX and reports that we have
    an overflow.

Differential Revision: https://reviews.llvm.org/D135375