[cfe-dev] Issue understanding static analyzer output

[Balázs Benics via cfe-dev]

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 at gmail.com> ezt írta (időpont: 2020. márc. 5.,
Cs, 13:56):

> 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 at lists.llvm.org> ezt írta (időpont: 2020.
> márc. 3., K, 15:58):
>
>> 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!
>>
>>
>> ---
>>
>> Loïc Joly
>>
>>
>>
>> _______________________________________________
>> cfe-dev mailing list
>> cfe-dev at lists.llvm.org
>> https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/cfe-dev/attachments/20200311/77a33224/attachment-0001.html>