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

Clang Frontend Static Analyzer
1

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.

2

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 (). I ultimately prefer to solve this by eliminating ElementRegion, FieldRegion, etc., entirely; only base regions and raw offsets are truly material.

3

…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.