<html><head><meta http-equiv="Content-Type" content="text/html charset=utf-8"></head><body style="word-wrap: break-word; -webkit-nbsp-mode: space; -webkit-line-break: after-white-space;" class="">Sanjoy,<div class=""> My answer is that step 3, commuting the multiply with the sign-extends, is invalid,</div><div class="">As this is what causes the `udiv` to fault. I think it is invalid with or without the “freeze”,</div><div class="">why do you think step 3, the commute, without the “freeze" is valid ?</div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">Also, do you think you can come up with an example that does not depend on signed</div><div class="">overflow being “undefined” ?</div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">Peter Lawrence.</div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><br class=""></div><div class=""><div><blockquote type="cite" class=""><br class=""></blockquote><blockquote type="cite" class=""><div class=""> <br style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-stroke-width: 0px;" class=""><blockquote type="cite" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;" class=""><br class=""><br class=""><br class=""></blockquote></div></blockquote><pre style="white-space: pre-wrap; background-color: rgb(255, 255, 255);" class="">Hi John,
On 11/11/16, 1:58 PM, Sanjoy Das wrote:
>> I'm saying that you still get reasonable behavior from reasoning about
>> counterfactuals for these things, and I haven't been convinced that you
>> lose optimization power except in code that actually exhibits undefined
>> behavior.
>
> I'm not sure I understood your concern fully, but you could have cases like:
>
> for (...) {
> if (condition){
> i32 prod = x *nsw y
> i64 prod.sext = sext prod to i64
> i64 t = K `udiv` (-1 + (sum.prod >> 32))
> use(t)
> }
> }
I'm sure it is obvious to you, but there's a typo here -- it should
have been "i64 t = K `udiv` (-1 + (prod.sext >> 32))"
> The C program this came from is well defined in two cases (that are relevant here):
>
> 1. condition is false
> 2. condition is true and x * y does not sign overflow
>
> We'd like to LICM the entire expression tree out of control flow in a way that it helps the well defined case (2)
> without introducing a fault in the well defined case (1).
To be a 100% explicit, by (1) I mean a situation where:
a. condition is false
b. (say) x is 1 << 20, and y is 1 << 12 so "x *nsw y" does sign
overflow, and ((sext(x) * sext(y)) >> 32) is 1
I'll also spell out what I was trying to say more explicitly, since we
can easily sink too much time talking about subtly different things
otherwise (has happened in the past :) ):
Firstly consider this sequence of transforms:
for (...) {
if (condition){
i32 prod = x *nsw y
i64 prod.sext = sext prod to i64
i64 t = K `udiv` (-1 + (sum.prod >> 32))
use(t)
}
}
==> (step 1) multiplication and sext can be speculated
i32 prod = x *nsw y
i64 prod.sext = sext prod to i64
for (...) {
if (condition){
i64 t = K `udiv` (-1 + (prod.sext >> 32))
use(t)
}
}
==> (step 2) known bits analysis on sext to prove divisor is non-zero
i32 prod = x *nsw y
i64 prod.sext = sext prod to i64
i64 t = K `udiv` (-1 + (prod.sext >> 32))
for (...) {
if (condition){
use(t)
}
}
==> (step 3) commute sext through nsw multiplicationa
;; i32 prod = x *nsw y
i64 prod.sext = (sext x) *nsw (sext y)
i64 t = K `udiv` (-1 + (prod.sext >> 32))
for (...) {
if (condition){
use(t)
}
}
Now we've managed to introduce a fault if we were in case 1 -- the
source program was well defined but the target program divides by
zero.
This means whatever scheme / semantics / "rule book" LLVM implements
has to outlaw at least one of the steps above.
For the freeze/poison scheme that step is "step 2". Under the
freeze/poison scheme step 2 will be
i32 prod = x *nsw y
i64 prod.sext = sext prod to i64
for (...) {
if (condition){
i64 t = K `udiv` (-1 + (prod.sext >> 32))
use(t)
}
}
==> (step 2) known bits analysis on sext to prove divisor is non-zero
i32 prod = x *nsw y
i32 prod.frozen = freeze(prod)
i64 prod.sext = sext prod.frozen to i64
i64 t = K `udiv` (-1 + (prod.sext >> 32))
for (...) {
if (condition){
use(t)
}
}
Which would further outlaw step 3.
If we go with counterfactual reasoning, then what is that step above
that is illegal?
-- Sanjoy
</pre><div class=""><br class=""></div><blockquote type="cite" class=""><div class=""><blockquote type="cite" style="font-family: Helvetica; font-size: 12px; font-style: normal; font-variant-caps: normal; font-weight: normal; letter-spacing: normal; orphans: auto; text-align: start; text-indent: 0px; text-transform: none; white-space: normal; widows: auto; word-spacing: 0px; -webkit-text-size-adjust: auto; -webkit-text-stroke-width: 0px;" class=""><br class=""> <br class=""></blockquote><br class="Apple-interchange-newline"></div></blockquote></div><br class=""></div></body></html>