[analyzer][RFC] Handle pointer difference of ElementRegion and SymbolicRegion

classic Classic list List threaded Threaded
3 messages Options
Reply | Threaded
Open this post in threaded view
|

[analyzer][RFC] Handle pointer difference of ElementRegion and SymbolicRegion

Keane, Erich via cfe-dev

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

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
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [analyzer][RFC] Handle pointer difference of ElementRegion and SymbolicRegion

Keane, Erich via cfe-dev
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). 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

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
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev


_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev
Reply | Threaded
Open this post in threaded view
|

Re: [analyzer][RFC] Handle pointer difference of ElementRegion and SymbolicRegion

Keane, Erich 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 <[hidden email]> 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). 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

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
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev

_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev


_______________________________________________
cfe-dev mailing list
[hidden email]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-dev