<div class="gmail_quote">On 10 August 2011 13:07, Eli Friedman <span dir="ltr"><<a href="mailto:eli.friedman@gmail.com" target="_blank">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>On Wed, Aug 10, 2011 at 12:57 PM, Nick Lewycky <<a href="mailto:nlewycky@google.com" target="_blank">nlewycky@google.com</a>> wrote:<br>
> On 10 August 2011 12:37, Pranav Bhandarkar <<a href="mailto:pranavb@codeaurora.org" target="_blank">pranavb@codeaurora.org</a>> wrote:<br>
>><br>
>> Hi Nick,<br>
>><br>
>> >>Thanks for working on this! Firstly, I have a high-level question: why<br>
>> can't (X +nsw (C1 +nsw C2) always become (X +nsw C3)? Your patch spends a<br>
>> lot of time verifying that >>overflow couldn't occur, but you're given 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. 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 where<br>
> C3 = C1+C2 (no nsw requirement)? 127 and 2 don't work as counter-examples<br>
> because that triggers undefined behaviour (it violates the 'nsw' bit present<br>
> on the add).<br>
<br>
</div>X = -128, C1 = 127, C1 = 2?<br></blockquote><div><br></div><div>I assume C2 = 2 and all i8 values. That doesn't work because the expression was "(X +nsw (C1 +nsw C2)" and 127 +nsw 2 invokes undefined behaviour, crossing from 127 to -128/128 to reach -127/129. In fact nsw-adding anything positive to 127 is invalid, so you'd have to be sure to pick a negative C2 given a C1 of 127.</div>


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