[llvm-dev] The semantics of nonnull attribute

[Nicolai Hähnle via llvm-dev]

Hi Johannes,

On Wed, Feb 19, 2020 at 8:17 AM Doerfert, Johannes
<johannesdoerfert at gmail.com> wrote:
> 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.

That's a fair point. The same kind of argument actually applies to an
analog of the example 4 that started this thread. If the argument is
dead, then:

f(dereferenceable(N) %ptr)
==>
f(dereferenceable(N) undef)

... would introduce UB and therefore be forbidden. So if that example
serves as motivation for making nonnull weaker and introducing
not_poison, then it should really serve as motivation for making _all_
function argument attributes weaker.

Besides, there's a certain elegance in treating _all_ attributes on
function arguments the same:

* passing function arguments that do not satisfy the attribute
constraints turn the corresponding value into poison
* passing poison for a not_poison argument causes immediate UB (and
this rule applies _after_ the first rule had a chance to poison
things)

That seems like it would be far less error prone than having to
remember on a case-by-case basis whether certain attributes cause
poison or immediate UB.

Cheers,
Nicolai


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



-- 
Lerne, wie die Welt wirklich ist,
aber vergiss niemals, wie sie sein sollte.