Issue understanding static analyzer output

Hello, I have the following code (you can see it live here: https://godbolt.org/z/iiki_w)

typedefunsignedlonglong size_t;

char f1(size_t len) {
char a[] = "Hello world!";
auto p = a+len+1;
return *p;
}

char f2(size_t len) {
char a[] = "Hello world!";
auto p = a+len;
return *p;
}

char f3(int len) {
char a[] = "Hello world!";
auto p = a+len+1;
return *p;
}

For f1, the static analyzer reports an of bounds memory access, not for the other 2 cases, that look quite similar (one is removing adding 1 to an unknown SVal, the other one is working with int instead of size_t).

I tried to look into the exploded graph, and I got the following constraint appearing right on the last node of the graph:
"constraints": ["symbol": "reg_$0<size_t len>", "range": "{ [18446744073709551615, 18446744073709551615] }

I fail to see where this constraint on "len" come from. I know I4m using an alpha checker, but I'm not sure this is meaningful in this case?

Do you have any idea?

Thank you!

Hi,
I’m pretty confident that this is a bug.

Btw we can minimize the example even more:

typedef unsigned long long size_t;
const char a[] = “aabbcc”;

char f1(size_t len) {
return a[len+1];
}
char f2(size_t len) {
return a[len];
}
char f3(int len) {
return a[len+1];
}

After some investigation, I narrowed down to the ArrayBoundCheckerV2::checkLocation function, so your guess was right.

I will dig deeper and create a patch if I’m done.

Regards Balazs.

Loïc Joly via cfe-dev <cfe-dev@lists.llvm.org> ezt írta (időpont: 2020. márc. 3., K, 15:58):

Hi,

I filed the bug, made some investigations about the issue.

The description there will help the Checker developers in the future to refactor the ArrayBoundCheckerV2 checker.
IMO this issue is the reason why this checker is an alpha checker.

Anybody can follow the discussion at Bugzilla, https://bugs.llvm.org/show_bug.cgi?id=45148.
Unfortunately, I don’t have time to continue with this, but I’m sure some Checker dev will pick my observations up.

Any opinion on this? Any volunteer - shouldn’t be too hard to fix.

Regards, Balazs.

Balázs Benics <benicsbalazs@gmail.com> ezt írta (időpont: 2020. márc. 5., Cs, 13:56):