Re: C provenance semantics proposal

[Peter Sewell <Peter dot Sewell at cl dot cam dot ac dot uk>]

On 25/04/2019, Richard Biener <richard.guenther@gmail.com> wrote:
> On Wed, Apr 24, 2019 at 11:18 PM Peter Sewell <Peter.Sewell@cl.cam.ac.uk>
> wrote:
>>
>> On 24/04/2019, Jeff Law <law@redhat.com> wrote:
>> > On 4/24/19 4:19 AM, Richard Biener wrote:
>> >> On Thu, Apr 18, 2019 at 3:42 PM Jeff Law <law@redhat.com> wrote:
>> >>>
>> >>> On 4/18/19 6:20 AM, Uecker, Martin wrote:
>> >>>> Am Donnerstag, den 18.04.2019, 11:45 +0100 schrieb Peter Sewell:
>> >>>>> On Thu, 18 Apr 2019 at 10:32, Richard Biener
>> >>>>> <richard.guenther@gmail.com> wrote:
>> >>>>
>> >>>>
>> >>>>> An equality test of two pointers, on the other hand, doesn't
>> >>>>> necessarily
>> >>>>> mean that they are interchangeable.  I don't see any good way to
>> >>>>> avoid that in a provenance semantics, where a one-past
>> >>>>> pointer might sometimes compare equal to a pointer to an
>> >>>>> adjacent object but be illegal for accessing it.
>> >>>>
>> >>>> As I see it, there are essentially four options:
>> >>>>
>> >>>> 1.) Compilers do not use conditional equivalences for
>> >>>> optimizations of pointers (or only when additional
>> >>>> conditions apply which make it safe)
>> >>> I know this will hit DOM and CSE.  I wouldn't be surprised if it
>> >>> touches
>> >>> VRP as well, maybe PTA.  It seems simple enough though :-)
>> >>
>> >> Also touches fundamental PHI-OPT transforms like
>> >>
>> >>  if (a == b)
>> >> ...
>> >>
>> >>  # c = PHI <a, b>
>> >>
>> >> where we'd lose eliding such a conditional.  IMHO that's bad
>> >> and very undesirable.
>> > But if we only suppress this optimization for pointers is it that
>> > terrible?
>>
>> As far as I can see right now, there isn't a serious alternative.
>> Suppose x and y are adjacent, p=&x+1, and q=&y, so p==q might
>> be true (either in a semantics for the source-language == that just
>> compares the concrete representations or in one that's allowed
>> but not required to be provenance-sensitive).   It's not possible
>> to simultaneously have *p UB (which AIUI the compiler has to
>> have in the intermediate language, to make alias analysis sound),
>> *q not UB, and p interchangeable with q.    Am I missing something?
>
> No, you are not missing anything.  We do have this issue right now,
> independent of standard wordings.  But the standard has that, too,
> not allowing *(&x + 1), allowing the compare and allowing *&y.
> Isn't that a defect as well?

In the source-language semantics, it's ok for p==q to not imply
that p and q are interchangeable, and if compilers are doing
provenance-based alias analysis (so address equality doesn't
imply equally-readable/writable), it's pretty much inescapable.

Hence why (without knowing much about the optimisations that
actually go on) it's tempting to suggest that for pointer equality
comparison one could just not infer that interchangeability. I'd be
very interested to know the actual cost of that.

(The standard does also have a defect in its definition of equality - on
the one hand, it says that &x+1==&y comparison must be true
if they are adjacent, but on the other (in DR260) that everything
might be provenance-aware.   My preference would be to resolve
that by requiring source-language == to not be provenance aware,
but I think this is a more-or-less independent thing.)

Peter