<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Tue, Jan 27, 2015 at 7:59 PM, Sanjoy Das <span dir="ltr"><<a href="mailto:sanjoy@playingwithpointers.com" target="_blank">sanjoy@playingwithpointers.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex"><div class=""><div class="h5">On Tue, Jan 27, 2015 at 7:44 PM, David Majnemer<br>
<<a href="mailto:david.majnemer@gmail.com">david.majnemer@gmail.com</a>> wrote:<br>
> On Tue, Jan 27, 2015 at 7:23 PM, Sanjoy Das <<a href="mailto:sanjoy@playingwithpointers.com">sanjoy@playingwithpointers.com</a>><br>
> wrote:<br>
>><br>
>> Hi David,<br>
>><br>
>> I spent some time thinking about poison semantics this way, but here<br>
>> is where I always get stuck:<br>
>><br>
>> Consider the IR fragment<br>
>><br>
>> %x = zext i32 %maybe_poison to i64<br>
>> %y = lshr i64 %x 32<br>
>> %ptr = gep %global, %y<br>
>> store 42 to %ptr<br>
>><br>
>> If %maybe_poison is poison, then is %y poison? For all i32 values of<br>
>> %maybe_poison, %y is i64 0, so in some sense you can determine the<br>
>> value %y without looking at %x.<br>
><br>
><br>
> I agree, this makes sense.<br>
><br>
>><br>
>> Given that, the store in the above<br>
>> fragment is not undefined behavior even if %maybe_poison is poison.<br>
>> However, this means if "%maybe_poison" is "add nuw %m, %n" it cannot<br>
>> be optimized to "add nuw (zext %m) (zext %n)" since that will change<br>
>> program behavior in an otherwise well-defined program.<br>
><br>
><br>
> Hmm, I'm not so sure this is right.<br>
><br>
> Are we talking about transforming:<br>
> %add = add nuw i32 %x, %y<br>
> %res = zext i32 %add to i64<br>
><br>
> to:<br>
> %z1 = zext i32 %x to i64<br>
> %z2 = zext i32 %y to i64<br>
> %res = add nuw i64 %z1, %z2<br>
><br>
> ?<br>
><br>
> This is OK because performing a zext by that many bits cannot result in a<br>
> NUW violation.<br>
<br>
</div></div>No, I'm talking about "zext(add nuw X Y)" ==> "add nuw (zext X) (zext<br>
Y)". In the example, replacing %x, a zext of an nuw add with an nuw<br>
add of zexts changes the behavior of a well-defined program.<br></blockquote><div><br></div><div>Correct me if I am wrong but we are talking about transforming:</div><div><div> %maybe_poison = add nuw i32 %a, %b</div><div> %x = zext i32 %maybe_poison to i64</div><div> %y = lshr i64 %x 32</div></div><div> </div><div>To:</div><div> %za = zext i32 %a to i64</div><div></div><div> %zb = zext i32 %b to i64</div><div></div><div> %x = add nuw i64 %za, %zb<br></div><div><div> %y = lshr i64 %x 32<br></div></div><div><br></div><div>?</div><div><br></div><div>If so, this seems fine in the model given by the RFC.</div><div><br></div><div>In the before case:</div><div>%maybe_poison doesn't infect the upper bits of %x with its poison which allows %y to have the well defined result 0.</div><div><br></div><div>In the after case:</div><div>%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.</div><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-color:rgb(204,204,204);border-left-style:solid;padding-left:1ex">
<span class=""><br>
> sext must be dependent on the underlying value because it splats the sign<br>
> bit.<br>
<br>
</span>Right, which is why I initially chose zext. :)<br>
<br>
But with sexts with you a similar problem:<br>
<br>
<br>
%t = add nsw <known positive>, <known positive><br>
%t1 = and %t, 0x7fff...<br>
%t2 = sext %t1<br>
%t3 = lshr %t2, <width of typeof %t><br>
store_to (gep %global, %t2)<br>
<br>
Now %t3 is always zero and this program is well-defined if even if %t<br>
is poison. However, I cannot reason "%t never overflows, so it is<br>
always >0 and hence %t1 == %t" since substituting %t1 with %t will<br>
change the meaning of a well-defined program.<br>
<span class=""><font color="#888888"><br>
-- Sanjoy<br>
</font></span></blockquote></div><br></div></div>