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

[Peter Lawrence via llvm-dev]

> On Jun 7, 2017, at 2:23 PM, Nuno Lopes <nunoplopes at sapo.pt> wrote:
> 
> Since most add/sub operations compiled from C have the nsw attribute, we cannot simply restrict movement of these instructions.

Nuno,
          I’m not saying the operations can’t be moved,
I’m saying that once you move one the ‘nsw’ attribute no longer applies,
unless you can mathematically prove that it still does,
otherwise an “add nsw” has to be converted to plain “add”.

It is only by illegally retaining the ‘nsw’ after hoisting the multiply out of the ‘if’ statement
that subsequent transformations yield end-to-end-miscompilation in Sanjoy’s example.

Don’t you agree ?

-Peter.







> 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