llvm dev - Feb 2020 - The semantics of nonnull attribute

On Wed, Feb 19, 2020 at 3:51 AM Juneyoung Lee via llvm-dev
<llvm-dev at lists.llvm.org> wrote:
> I think not_poison (Johannes's used keyword) makes sense. We can
simulate the original UB semantics by simply attaching it, as explained.
> For the attributes other than nonnull, we may need more discussion; align
attribute seems to be okay with defining it as poison, dereferenceable may need
UB even without nonnull (because it needs to be non-poison as shown Nuno's
hoisting example).
For reference, the hoisting example was:

f(dereferenceable(4) %p) {
  loop() {
    %v = load %p
    use(%v)
  }
}
=>
f(dereferenceable(4) %p) {
  %v = load %p
  loop() {
    use(%v)
  }
}

Would it be correct to resolve this by saying that dereferenceable(N)
*implies* not_poison? This would be helpful as a clarification of how
it all fits together.

Cheers,
Nicolai

Hello,
>  Would it be correct to resolve this by saying that dereferenceable(N)
> *implies* not_poison? This would be helpful as a clarification of how
> it all fits together.
Yes, I think it makes sense.

On Wed, Feb 19, 2020 at 12:14 PM Nicolai Hähnle <nhaehnle at gmail.com>
wrote:
> On Wed, Feb 19, 2020 at 3:51 AM Juneyoung Lee via llvm-dev
> <llvm-dev at lists.llvm.org> wrote:
> > I think not_poison (Johannes's used keyword) makes sense. We can
> simulate the original UB semantics by simply attaching it, as explained.
> > For the attributes other than nonnull, we may need more discussion;
> align attribute seems to be okay with defining it as poison,
> dereferenceable may need UB even without nonnull (because it needs to be
> non-poison as shown Nuno's hoisting example).
>
> For reference, the hoisting example was:
>
> f(dereferenceable(4) %p) {
>   loop() {
>     %v = load %p
>     use(%v)
>   }
> }
> =>
> f(dereferenceable(4) %p) {
>   %v = load %p
>   loop() {
>     use(%v)
>   }
> }
>
> Would it be correct to resolve this by saying that dereferenceable(N)
> *implies* not_poison? This would be helpful as a clarification of how
> it all fits together.
>
> Cheers,
> Nicolai
>

-- 

Juneyoung Lee
Software Foundation Lab, Seoul National University
-------------- next part --------------
An HTML attachment was scrubbed...
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20200219/238e5a98/attachment.html>

On 02/19, Juneyoung Lee via llvm-dev wrote:
> Hello,
> 
> >  Would it be correct to resolve this by saying that dereferenceable(N)
> > *implies* not_poison? This would be helpful as a clarification of how
> > it all fits together.
> 
> Yes, I think it makes sense.
I don't we should do that.

Take the `gep inbounds` example:

char* foo(char *arg) {
  return `gep inbounds %arg, -100`
}

Here it depends if we want to deduce the output is dereferenceable(100)
or not. If we do, we need dereferenceable to mean poison if violated, as
with nonnull, because it is derived from poison. Only if we don't derive
dereferenceable for the return value we can go for dereferenceable
violations are UB.

In the end, I think, it boils down to the question if there are
situations where violation of some attributes should be poison and
violation of others should be UB. If such situations exists it is
unclear to me what makes the UB/poison ones special.

> On Wed, Feb 19, 2020 at 12:14 PM Nicolai Hähnle <nhaehnle at
gmail.com> wrote:
> 
> > On Wed, Feb 19, 2020 at 3:51 AM Juneyoung Lee via llvm-dev
> > <llvm-dev at lists.llvm.org> wrote:
> > > I think not_poison (Johannes's used keyword) makes sense. We
can
> > simulate the original UB semantics by simply attaching it, as
explained.
> > > For the attributes other than nonnull, we may need more
discussion;
> > align attribute seems to be okay with defining it as poison,
> > dereferenceable may need UB even without nonnull (because it needs to
be
> > non-poison as shown Nuno's hoisting example).
> >
> > For reference, the hoisting example was:
> >
> > f(dereferenceable(4) %p) {
> >   loop() {
> >     %v = load %p
> >     use(%v)
> >   }
> > }
> > =>
> > f(dereferenceable(4) %p) {
> >   %v = load %p
> >   loop() {
> >     use(%v)
> >   }
> > }
> >
> > Would it be correct to resolve this by saying that dereferenceable(N)
> > *implies* not_poison? This would be helpful as a clarification of how
> > it all fits together.
> >
> > Cheers,
> > Nicolai
> >
> 
> 
> -- 
> 
> Juneyoung Lee
> Software Foundation Lab, Seoul National University
> _______________________________________________
> LLVM Developers mailing list
> llvm-dev at lists.llvm.org
> https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev

-- 

Johannes Doerfert
Researcher

Argonne National Laboratory
Lemont, IL 60439, USA

jdoerfert at anl.gov
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 228 bytes
Desc: not available
URL:
<http://lists.llvm.org/pipermail/llvm-dev/attachments/20200219/bed194ee/attachment.sig>