<div class="gmail_quote">On 10 August 2011 13:19, Eli Friedman <span dir="ltr"><<a href="mailto:eli.friedman@gmail.com">eli.friedman@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">

<div><div></div><div class="h5">On Wed, Aug 10, 2011 at 1:11 PM, Nick Lewycky <<a href="mailto:nlewycky@google.com">nlewycky@google.com</a>> wrote:<br>
> On 10 August 2011 13:07, Eli Friedman <<a href="mailto:eli.friedman@gmail.com">eli.friedman@gmail.com</a>> wrote:<br>
>><br>
>> On Wed, Aug 10, 2011 at 12:57 PM, Nick Lewycky <<a href="mailto:nlewycky@google.com">nlewycky@google.com</a>><br>
>> wrote:<br>
>> > On 10 August 2011 12:37, Pranav Bhandarkar <<a href="mailto:pranavb@codeaurora.org">pranavb@codeaurora.org</a>><br>
>> > wrote:<br>
>> >><br>
>> >> Hi Nick,<br>
>> >><br>
>> >> >>Thanks for working on this! Firstly, I have a high-level question:<br>
>> >> >> why<br>
>> >> can't (X +nsw (C1 +nsw C2) always become (X +nsw C3)? Your patch spends<br>
>> >> a<br>
>> >> lot of time verifying that >>overflow couldn't occur, but you're given<br>
>> >> an<br>
>> >> assumption a priori that it can't because the nsw flag is present.<br>
>> >><br>
>> >> The reason is that 127 (C1) + 2 (C2) = 129 (C3) is not strictly true<br>
>> >> always.<br>
>> >> For instance, when the type is i8, then C3 is -127.<br>
>> ><br>
>> > 127 + 2 = 129 remains true with i8 values, because i8 -127 = i8 129.<br>
>> > They<br>
>> > have the same bit pattern.<br>
>> > Can you pick values for X, C1 and C2 which still satisfy the +nsw<br>
>> > relationship between each other that can't be converted into X +nsw C3<br>
>> > where<br>
>> > C3 = C1+C2 (no nsw requirement)? 127 and 2 don't work as<br>
>> > counter-examples<br>
>> > because that triggers undefined behaviour (it violates the 'nsw' bit<br>
>> > present<br>
>> > on the add).<br>
>><br>
>> X = -128, C1 = 127, C1 = 2?<br>
><br>
> I assume C2 = 2 and all i8 values. That doesn't work because the expression<br>
> was "(X +nsw (C1 +nsw C2)" and 127 +nsw 2 invokes undefined behaviour,<br>
> crossing from 127 to -128/128 to reach -127/129. In fact nsw-adding anything<br>
> positive to 127 is invalid, so you'd have to be sure to pick a negative C2<br>
> given a C1 of 127.<br>
<br>
</div></div>The original expression is ((X +nsw C1) +nsw C2).<br></blockquote><div><br></div><div>Doh! Thanks.</div><div><br></div><div>So the original code with your values does:</div><div>((X +nsw C1) +nsw C2) --> ((-128 +nsw 127) +nsw 2) = 1, and none of the nsw's are violated. Good.</div>

<div><br></div><div>After my proposed transform, we get:</div><div>C3 = C1 + C2 --> C3 = 127 + 2 = -127.</div><div>(X +nsw C3) --> (-128 +nsw -127) = 1, and the nsw wasn't violated (we moved towards zero 129 times, starting from -128 up past -1 and crossed the unsigned boundary to 0 finally landing at 1, never crossing the signed boundary).</div>

<div><br></div><div>I may still be wrong, but I don't think so. :-) More generally I think we can always take the intersection of the nuw/nsw/exact flags available on any string of the same instruction. Start mixing instructions and things get messy though.</div>

<div><br></div><div>Nick</div><div><br></div></div>