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 Thu, Apr 25, 2019 at 3:03 PM Peter Sewell <Peter.Sewell@cl.cam.ac.uk>
> wrote:
>>
>> 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.
>
> Since we at the moment track provenance through non-pointers
> it means we cannot do this for non-pointer equivalences either.
> So doing this means no longer tracking provenance through
> non-pointers.

Yes, it would mean that.

(As you may recall, we did earlier propose a source-language
semantics that did track provenance through integers, so that's
not inconceivable - but it does get complicated, and the
current consensus seems to be towards the not-via-integer
options.)

>> (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.)
>
> I think it's related at least to us using provenance to optimize
> pointer comparisons.

Yes.  If that's a significant win, one would want to keep allowing
(but not requiring) == to be provenance-aware.  The argument
in the other direction is that it would simplify the source semantics.

Peter

> Richard.
>
>> Peter
>