[llvm-dev] RFC: Killing undef and spreading poison

[John McCall via llvm-dev]

> On Nov 11, 2016, at 11:55 PM, Sanjoy Das <sanjoy at playingwithpointers.com> wrote:
> 
> 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?

I see your point.  I think this is going to be a very limited tool, suitable for things
like nsw that have obvious "right answers" that you can freeze the poison out of,
but I concede that it's nice for optimizing the overflow cases.

John.