Re: C provenance semantics proposal

[Jens Gustedt <jens.gustedt@inria.fr>]

[-- Attachment #1: Type: text/plain, Size: 1660 bytes --]

Hello Peter,

On Fri, 19 Apr 2019 10:11:43 +0100 Peter Sewell
<Peter.Sewell@cl.cam.ac.uk> wrote:

> On 19/04/2019, Jakub Jelinek <jakub@redhat.com> wrote:
> > On Fri, Apr 19, 2019 at 10:19:28AM +0200, Jens Gustedt wrote:  
>  [...]  

> > That penalizes quite a few optimizations though.
> > If you have
> > ptr != ptr2
> > and points-to analysis finds a set of variables ptr as well as ptr2
> > points to and the sets would be disjoint, it would be nice to be
> > able to optimize that comparison away (gcc does); similarly, if one
> > of the pointers is &object or &object + sizeof (object).
> > By requiring what you request above, it can be pretty much never
> > optimized, unless the points-to analysis is able to also record if
> > the pointer points to the start, middle or end of object and only
> > if it is known to be in the middle it can safely optimize, for
> > start or end it would need to prove the other pointer is to end or
> > start and only non-zero sized objects are involved.  
> 
> A possible compromise position might be to make it
> implementation-defined whether round-trip casts of a one-past pointer
> into integer and back preserve provenance.   I don't know whether
> that corner case crops up in real code...

Wouldn't that impose to keep track of some provenance information in
integers?

Jens

-- 
:: INRIA Nancy Grand Est ::: Camus ::::::: ICube/ICPS :::
:: ::::::::::::::: office Strasbourg : +33 368854536   ::
:: :::::::::::::::::::::: gsm France : +33 651400183   ::
:: ::::::::::::::: gsm international : +49 15737185122 ::
:: http://icube-icps.unistra.fr/index.php/Jens_Gustedt ::

[-- Attachment #2: Digitale Signatur von OpenPGP --]
[-- Type: application/pgp-signature, Size: 195 bytes --]