[cfe-dev] [analyzer][RFC] Handle pointer difference of ElementRegion and SymbolicRegion

[Valeriy Savchenko via cfe-dev]

> ...only base regions and raw offsets are truly material.

I strongly agree with this statement and believe that the analysis should operate only in these terms.  However, for a better experience of us (the analyzer developers), I would still leave ElementRegion or FieldRegion as a very thin layer over base + offset for debugging purposes.

> On 28 Jul 2020, at 22:38, Artem Dergachev via cfe-dev <cfe-dev at lists.llvm.org> wrote:
> 
> Yes, we should totally handle this case. I'll take a look at the patch.
> 
> The bigger picture here is that ElementRegion is on its own a fairly annoying fundamental bug in our region hierarchy (https://bugs.llvm.org/show_bug.cgi?id=43364 <https://bugs.llvm.org/show_bug.cgi?id=43364>). I ultimately prefer to solve this by eliminating ElementRegion, FieldRegion, etc., entirely; only base regions and raw offsets are truly material.
> 
> On 7/28/20 3:47 AM, Balázs Benics via cfe-dev wrote:
>> Currently, if the analyzer evaluates an expression like to - from, it only computes reasonable answer if both are representing ElementRegions.
>> 
>> Formally, for all memory region X and for all SVal offset Y:
>> &Element{SymRegion{X},Y,char} - &SymRegion{X} => Y
>> The same for the symmetric version, but returning -Y instead.
>> 
>> I'm curious why don't we handle the case, when only one of the operands is an ElementRegion and the other is a plain SymbolicRegion.
>> IMO if the super memory region of the ElementRegion is the same as the SymbolicRegion then we can still return a reasonable answer.
>> 
>> In this patch, I suppose an extension to resolve this in https://reviews.llvm.org/D84736 <https://reviews.llvm.org/D84736>
>> Unfortunately, Phabricator patches require passing the tests to start a discussion recently.
>> 
>> Analyzer devs, could you share your opinion on this?
>> 
>> Balazs.
>> 
>> 
>> 
>> 
>> 
>> 
>> _______________________________________________
>> cfe-dev mailing list
>> cfe-dev at lists.llvm.org <mailto:cfe-dev at lists.llvm.org>
>> https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev <https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev>
> 
> _______________________________________________
> 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/20200729/4e7b9c8c/attachment.html>