[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
Loading
Please sign in to comment