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

[Sanjoy Das via llvm-dev]

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