Re: [EXTERNAL] Re: [PATCH] tree-optimization: Optimize division followed by multiply [PR95176]

[Richard Biener <richard.guenther@gmail.com>]

On Sat, Jun 19, 2021 at 7:05 PM Marc Glisse <marc.glisse@inria.fr> wrote:
>
> On Fri, 18 Jun 2021, Richard Biener wrote:
>
> >> Option 2: Add a new pattern to support scenarios that the existing nop_convert pattern bails out on.
> >>
> >> Existing pattern:
> >>
> >> (simplify
> >>    (minus (nop_convert1? @0) (nop_convert2? (minus (nop_convert3? @@0) @1)))
> >>    (view_convert @1))
>
> I tried to check with a program when
>
> T3 x;
> T1 y;
> (T2)x-(T2)((T1)x-y)
>
> can be safely replaced with
>
> (T2)y
>
> From the output, it looks like this is safe when T1 is at least as large
> as T2. It is wrong when T1 is unsigned and smaller than T2. And when T1 is
> signed and smaller than T2, it is ok if T3 is the same type as T1 (signed
> then) or has strictly less precision (any sign), and not in other cases.
>
> Note that this is when signed implies undefined overflow and unsigned
> implies wrapping, and I wouldn't put too much faith in this recently
> dusted program. And it doesn't say how to write the match.pd pattern with
> '?', "@@", disabling it if TYPE_OVERFLOW_SANITIZED, etc.
>
> Mostly, I wanted to say that if we are going to go handle more than
> nop_convert for more than just 1 or 2 easy transformations, I think some
> kind of computer verification would be useful, it would save a lot of time
> and headaches.

True.  I wonder if auto-generating such tests from match.pd rules would
be a good project to work on (GSoC?).  When there's define_match
involved things get a little tricky, but then one item on the TODO list
is "inlining" those at the use site (exploding the decision tree even more).

Richard.

> (I just check by brute force all possible precisions (from 1 to 6) and
> signedness for T1, T2 and T3, all possible values for x and y, compute
> the before and after formulas, accepting if there is UB before, rejecting
> if there is UB after (and not before), and manually try to see a pattern
> in the list of types that work)
>
> --
> Marc Glisse