[llvm-dev] RFC: Killing undef and spreading poison
John McCall via llvm-dev
llvm-dev at lists.llvm.org
Sat Nov 12 13:38:14 PST 2016
> 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.
More information about the llvm-dev
mailing list