Peter Lawrence via llvm-dev
2017-Jun-02 01:18 UTC
[llvm-dev] RFC: Killing undef and spreading poison
Sanjoy, My answer is that step 3, commuting the multiply with the sign-extends, is invalid, As this is what causes the `udiv` to fault. I think it is invalid with or without the “freeze”, why do you think step 3, the commute, without the “freeze" is valid ? Also, do you think you can come up with an example that does not depend on signed overflow being “undefined” ? Peter Lawrence.> > >> >> >>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>> >> >-------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20170601/64cea6e2/attachment.html>
Sanjoy Das via llvm-dev
2017-Jun-05 04:13 UTC
[llvm-dev] RFC: Killing undef and spreading poison
Hi Peter, On Thu, Jun 1, 2017 at 6:18 PM, Peter Lawrence via llvm-dev <llvm-dev at lists.llvm.org> wrote:> My answer is that step 3, commuting the multiply with the > sign-extends, is invalid, > As this is what causes the `udiv` to fault. I think it is invalid with or > without the “freeze”, > why do you think step 3, the commute, without the “freeze" is valid ?I think it is valid by definition -- since "A *nsw B" does not sign wrap, "sext(A *nsw B)" == (sext A) * (sext B). In other words, these two expressions are inequal only if "A *nsw B" sign wraps.> Also, do you think you can come up with an example that does not depend on > signed > overflow being “undefined” ?Can you be more specific? Example that does what? -- Sanjoy
Peter Lawrence via llvm-dev
2017-Jun-05 22:56 UTC
[llvm-dev] RFC: Killing undef and spreading poison
Sanjay, Your original example showed end-to-end-miscompilation, After a sequence of transformations, Where “undefined behavior” is a part of the problem. My question is can you show some additional examples that do not rely on “nsw” or “nuw” ? Thanks, Peter Lawrence.> On Jun 4, 2017, at 9:13 PM, Sanjoy Das <sanjoy at playingwithpointers.com> wrote: > > Hi Peter, > > On Thu, Jun 1, 2017 at 6:18 PM, Peter Lawrence via llvm-dev > <llvm-dev at lists.llvm.org <mailto:llvm-dev at lists.llvm.org>> wrote: > >> Also, do you think you can come up with an example that does not depend on >> signed >> overflow being “undefined” ? > > Can you be more specific? Example that does what? > > -- Sanjoy-------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20170605/ba18aeaa/attachment.html>
Peter Lawrence via llvm-dev
2017-Jun-07 19:48 UTC
[llvm-dev] RFC: Killing undef and spreading poison
Sanjoy, In that case I change my answer and say that the illegal optimization was (step 1) hoisting the “nsw” out of the if-statement, When inside the protection of the if-clause the “nsw” was conditional on the if-clause, but when you hoisted it out of the if-statement there is no reason to continue assuming “nsw” is true. (This is true regardless of how the original “nsw” got there, either by language definition or by analysis). “Nsw” isn’t an opcode, it is analysis information, and as we all know Analysis information can and does get invalidated by transformations. This is a case in point. I think the “nsw” got hoisted out of the if-statement by accident, assuming it was part of the opcode, but we have just seen that this is incorrect. - - - - - - - - - - - - - - - - - - - - If the above analysis is correct (I am pretty sure it is, but have been known to make mistakes!), then my concern is that since this example was incorrectly root-caused I am not sure we are ready to commit to “poison” and “freeze” changes, and need to see more original source causes of end-to-end-miscompilation to be sure we haven’t also mis-diagnosed those as well. Peter Lawrence.> On Jun 5, 2017, at 12:02 PM, Sanjoy Das <sanjoy at playingwithpointers.com> wrote: > > Hi Peter, > > On Mon, Jun 5, 2017 at 9:43 AM, Peter Lawrence > <peterl95124 at sbcglobal.net> wrote: >>> I think it is valid by definition -- since "A *nsw B" does not sign >>> wrap, "sext(A *nsw B)" == (sext A) * (sext B). In other words, these >>> two expressions are inequal only if "A *nsw B" sign wraps. >> >> The way you use “nsw” it seems like an assertion or an assumption. > > Yes, that is correct. > >> Where did the “nsw” come from, is it from the source language definition, >> Or compiler derived analysis information ? > > Both are possible. In C/C++, as you know, most (all?) signed > arithmetic can be marked nsw. In many cases the optimizer will also > infer nsw if it can prove the arithmetic does not overflow (e.g. if (a > != INT_SMAX) b = a + 1; ==> if (a != INT_SMAX) b = a+nsw 1;). > > -- SanjoyHere’s the original source example for context ——————————————————————————————— [llvm-dev] RFC: Killing undef and spreading poison Sanjoy Das via llvm-dev llvm-dev at lists.llvm.org <mailto:llvm-dev%40lists.llvm.org?Subject=Re%3A%20%5Bllvm-dev%5D%20RFC%3A%20Killing%20undef%20and%20spreading%20poison&In-Reply-To=%3C5826CAF4.9000409%40playingwithpointers.com%3E>Fri Nov 11 23:55:32 PST 2016 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. -------------- next part -------------- An HTML attachment was scrubbed... URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20170607/ce78a4ca/attachment.html>
Nuno Lopes via llvm-dev
2017-Jun-07 21:23 UTC
[llvm-dev] RFC: Killing undef and spreading poison
Since most add/sub operations compiled from C have the nsw attribute, we cannot simply restrict movement of these instructions. Sure, we could drop nsw when moving these instructions, but there are still many other problems left. Please read more about the topic here: https://blog.regehr.org/archives/1496 For example, doing loop unswitching, followed by inline (just to illustrate that the reasoning cannot be local), plus GVN gives you end-to-end miscompilations easily. Nuno -----Original Message----- From: Peter Lawrence via llvm-dev Sent: Wednesday, June 7, 2017 8:48 PM Subject: Re: [llvm-dev] RFC: Killing undef and spreading poison Sanjoy, In that case I change my answer and say that the illegal optimization was (step 1) hoisting the “nsw” out of the if-statement, When inside the protection of the if-clause the “nsw” was conditional on the if-clause, but when you hoisted it out of the if-statement there is no reason to continue assuming “nsw” is true. (This is true regardless of how the original “nsw” got there, either by language definition or by analysis). “Nsw” isn’t an opcode, it is analysis information, and as we all know Analysis information can and does get invalidated by transformations. This is a case in point. I think the “nsw” got hoisted out of the if-statement by accident, assuming it was part of the opcode, but we have just seen that this is incorrect. - - - - - - - - - - - - - - - - - - - - If the above analysis is correct (I am pretty sure it is, but have been known to make mistakes!), then my concern is that since this example was incorrectly root-caused I am not sure we are ready to commit to “poison” and “freeze” changes, and need to see more original source causes of end-to-end-miscompilation to be sure we haven’t also mis-diagnosed those as well. Peter Lawrence. On Jun 5, 2017, at 12:02 PM, Sanjoy Das <sanjoy at playingwithpointers.com> wrote: Hi Peter, On Mon, Jun 5, 2017 at 9:43 AM, Peter Lawrence <peterl95124 at sbcglobal.net> wrote: I think it is valid by definition -- since "A *nsw B" does not sign wrap, "sext(A *nsw B)" == (sext A) * (sext B). In other words, these two expressions are inequal only if "A *nsw B" sign wraps. The way you use “nsw” it seems like an assertion or an assumption. Yes, that is correct. Where did the “nsw” come from, is it from the source language definition, Or compiler derived analysis information ? Both are possible. In C/C++, as you know, most (all?) signed arithmetic can be marked nsw. In many cases the optimizer will also infer nsw if it can prove the arithmetic does not overflow (e.g. if (a != INT_SMAX) b = a + 1; ==> if (a != INT_SMAX) b = a+nsw 1;). -- Sanjoy Here’s the original source example for context ——————————————————————————————— [llvm-dev] RFC: Killing undef and spreading poison Sanjoy Das via llvm-dev llvm-dev at lists.llvm.org Fri Nov 11 23:55:32 PST 2016 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. _______________________________________________ LLVM Developers mailing list llvm-dev at lists.llvm.org http://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-dev
John Regehr via llvm-dev
2017-Jun-07 21:27 UTC
[llvm-dev] RFC: Killing undef and spreading poison
Peter, it looks to me like you've misunderstood how nsw works. You are saying that the transformation below is incorrect. If it is incorrect, there needs to be a valuation of x and y (and also a choice of "..." and "condition") that causes the transformed code to call use(t) with a different t than the original code would have. Please tell us those values. John> 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) > } > }