ArrayBoundCheckerV2 false positive if indexer has size_t type

[Quuxplusone]

Bugzilla Link	PR45148
Status	CONFIRMED
Importance	P normal
Reported by	Balazs Benics (balazs.benics@sigmatechnology.se)
Reported on	2020-03-09 03:56:26 -0700
Last modified on	2020-08-31 05:31:23 -0700
Version	trunk
Hardware	PC Linux
CC	balazs.benics@sigmatechnology.se, dcoughlin@apple.com, llvm-bugs@lists.llvm.org, noqnoqneo@gmail.com
Fixed by commit(s)
Attachments	arrav2-exploded-graphs.zip (4053 bytes, application/zip) statemachine.svg (8797 bytes, image/svg+xml)
Blocks
Blocked by
See also

Created attachment 23216 Rewritten exploded graphs of all three functions of the example.

This bug was reported by Loïc Joly. You can read the original discussion at the cfe-dev archives: http://lists.llvm.org/pipermail/cfe-dev/2020-March/064783.html

The gist of this bug is demonstrated by this example:

// clang -cc1 -analyze -analyzer-checker=core,alpha.security.ArrayBoundV2 arrayv2.c
typedef unsigned long long size_t;
const char a[] = "aabbcc";

char f1(size_t len) {
  return a[len+1];
//       ^~~~~~~~
// arrayv2.c:7:10: warning: Out of bound memory access (access exceeds upper limit of memory block)
}
char f2(size_t len) {
  return a[len]; // no-warning
}
char f3(int len) {
  return a[len+1]; // no-warning
}

[Quuxplusone]

Attached arrav2-exploded-graphs.zip (4053 bytes, application/zip): Rewritten exploded graphs of all three functions of the example.

[Quuxplusone]

Attached statemachine.svg (8797 bytes, image/svg+xml): state machine representation of ArrayBoundCheckerV2::checkLocation

[Quuxplusone]

At a glance the state was computed incorrectly as well in case of overflow. Like, "x + 2 >= 0" is not the same as "x >= -2" in unsigned modular arithmetic (in fact the former is always true).

[Quuxplusone]

The fix is on review: https://reviews.llvm.org/D86874