[LLVMdev] RFC: Proposal for Poison Semantics

[Sanjoy Das]

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.

> 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