[LLVMdev] RFC: Proposal for Poison Semantics

[David Majnemer]

On Tue, Jan 27, 2015 at 7:59 PM, Sanjoy Das <sanjoy at playingwithpointers.com>
wrote:

> On Tue, Jan 27, 2015 at 7:44 PM, David Majnemer
> <david.majnemer at gmail.com> wrote:
> > On Tue, Jan 27, 2015 at 7:23 PM, Sanjoy Das <
> sanjoy at playingwithpointers.com>
> > wrote:
> >>
> >> Hi David,
> >>
> >> I spent some time thinking about poison semantics this way, but here
> >> is where I always get stuck:
> >>
> >> Consider the IR fragment
> >>
> >>   %x = zext i32 %maybe_poison to i64
> >>   %y = lshr i64 %x 32
> >>   %ptr = gep %global, %y
> >>   store 42 to %ptr
> >>
> >> If %maybe_poison is poison, then is %y poison?  For all i32 values of
> >> %maybe_poison, %y is i64 0, so in some sense you can determine the
> >> value %y without looking at %x.
> >
> >
> > I agree, this makes sense.
> >
> >>
> >> Given that, the store in the above
> >> fragment is not undefined behavior even if %maybe_poison is poison.
> >> However, this means if "%maybe_poison" is "add nuw %m, %n" it cannot
> >> be optimized to "add nuw (zext %m) (zext %n)" since that will change
> >> program behavior in an otherwise well-defined program.
> >
> >
> > Hmm, I'm not so sure this is right.
> >
> > Are we talking about transforming:
> > %add = add nuw i32 %x, %y
> > %res = zext i32 %add to i64
> >
> > to:
> > %z1 = zext i32 %x to i64
> > %z2 = zext i32 %y to i64
> > %res = add nuw i64 %z1, %z2
> >
> > ?
> >
> > This is OK because performing a zext by that many bits cannot result in a
> > NUW violation.
>
> No, I'm talking about "zext(add nuw X Y)" ==> "add nuw (zext X) (zext
> Y)".  In the example, replacing %x, a zext of an nuw add with an nuw
> add of zexts changes the behavior of a well-defined program.
>

Correct me if I am wrong but we are talking about transforming:
   %maybe_poison = add nuw i32 %a, %b
   %x = zext i32 %maybe_poison to i64
   %y = lshr i64 %x 32

To:
   %za = zext i32 %a to i64
   %zb = zext i32 %b to i64
   %x = add nuw i64 %za, %zb
   %y = lshr i64 %x 32

?

If so, this seems fine in the model given by the RFC.

In the before case:
%maybe_poison doesn't infect the upper bits of %x with its poison which
allows %y to have the well defined result 0.

In the after case:
%za and %zb will have their top 32-bits filled with zeros making it
impossible for nuw to be violated for %x, %y would have the well defined
result 0.


> > sext must be dependent on the underlying value because it splats the sign
> > bit.
>
> Right, which is why I initially chose zext. :)
>
> But with sexts with you a similar problem:
>
>
>   %t = add nsw <known positive>, <known positive>
>   %t1 = and %t, 0x7fff...
>   %t2 = sext %t1
>   %t3 = lshr %t2, <width of typeof %t>
>   store_to (gep %global, %t2)
>
> Now %t3 is always zero and this program is well-defined if even if %t
> is poison.  However, I cannot reason "%t never overflows, so it is
> always >0 and hence %t1 == %t" since substituting %t1 with %t will
> change the meaning of a well-defined program.
>
> -- Sanjoy
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20150127/e8ea72b3/attachment.html>