[Mesa-dev] [PATCH 08/10] nir: Simplify 0 < fabs(a)

[Matt Turner]

On Fri, Mar 11, 2016 at 11:21 AM, Ian Romanick <idr at freedesktop.org> wrote:
> On 03/11/2016 08:51 AM, Patrick Baggett wrote:
>> On Fri, Mar 11, 2016 at 10:21 AM, Ian Romanick <idr at freedesktop.org> wrote:
>>> On 03/10/2016 01:24 PM, Patrick Baggett wrote:
>>>> On Thu, Mar 10, 2016 at 3:08 PM, Patrick Baggett
>>>> <baggett.patrick at gmail.com> wrote:
>>>>> On Thu, Mar 10, 2016 at 12:25 PM, Ian Romanick <idr at freedesktop.org> wrote:
>>>>>> From: Ian Romanick <ian.d.romanick at intel.com>
>>>>>>
>>>>>> Sandy Bridge / Ivy Bridge / Haswell
>>>>>> total instructions in shared programs: 8462180 -> 8462174 (-0.00%)
>>>>>> instructions in affected programs: 564 -> 558 (-1.06%)
>>>>>> helped: 6
>>>>>> HURT: 0
>>>>>>
>>>>>> total cycles in shared programs: 117542462 -> 117542276 (-0.00%)
>>>>>> cycles in affected programs: 9768 -> 9582 (-1.90%)
>>>>>> helped: 12
>>>>>> HURT: 0
>>>>>>
>>>>>> Broadwell / Skylake
>>>>>> total instructions in shared programs: 8980833 -> 8980826 (-0.00%)
>>>>>> instructions in affected programs: 626 -> 619 (-1.12%)
>>>>>> helped: 7
>>>>>> HURT: 0
>>>>>>
>>>>>> total cycles in shared programs: 70077900 -> 70077714 (-0.00%)
>>>>>> cycles in affected programs: 9378 -> 9192 (-1.98%)
>>>>>> helped: 12
>>>>>> HURT: 0
>>>>>>
>>>>>> G45 and Ironlake showed no change.
>>>>>>
>>>>>> Signed-off-by: Ian Romanick <ian.d.romanick at intel.com>
>>>>>> ---
>>>>>>  src/compiler/nir/nir_opt_algebraic.py | 5 +++++
>>>>>>  1 file changed, 5 insertions(+)
>>>>>>
>>>>>> diff --git a/src/compiler/nir/nir_opt_algebraic.py b/src/compiler/nir/nir_opt_algebraic.py
>>>>>> index 4db8f84..1442ce8 100644
>>>>>> --- a/src/compiler/nir/nir_opt_algebraic.py
>>>>>> +++ b/src/compiler/nir/nir_opt_algebraic.py
>>>>>> @@ -108,6 +108,11 @@ optimizations = [
>>>>>>     # inot(a)
>>>>>>     (('fge', 0.0, ('b2f', a)), ('inot', a)),
>>>>>>
>>>>>> +   # 0.0 < fabs(a)
>>>>>> +   # 0.0 != fabs(a)  because fabs(a) must be >= 0
>>>>> I think this is wrong. Because >= 0.0 can mean that fabs(a) == 0.0 for
>>>>> some a, you can't say then fabs(a) != 0.0.
>>>>>
>>>>> Then, the counter-example is when a = 0.0
>>>>>
>>>>> 1) 0.0 != fabs(0.0)
>>>>> 2) 0.0 != 0.0
>>>>>
>>>> Rather, I mean the comment is wrong, but the conclusion that:
>>>> 0 < fabs(a) <-> a != 0.0
>>>> is correct. You can just build a truth table or just observe that when
>>>> a == 0, 0 < 0 is false, and
>>>> when a != 0.0, fabs(a) will be > 0, so 0 < fabs(a) will be always true.
>>>
>>> How about if I change it to
>>>
>>>    # 0.0 != fabs(a)  Since fabs(a) >= 0, 0 <= fabs(a) must be true
>>>
>>> I think it's trivial to see how to get from "0 < fabs(a)" to "0 !=
>>> fabs(a)" based on that.
>> Yeah, I think what gave me a pause when I read was "0.0 != fabs(a)",
>
> Right... I was forming this like a proof.  At each line I was just
> trying to provide justification for the change from the previous line.
> "0.0 != fabs(a)" is equivalent to "0.0 < fabs(a)" for the reason
> provided.  I did the same thing in the previous patch.
>
> I want to get consensus on the right way to do this because I have a
> bunch more patches to nir_opt_algebraic.py that use the same technique
> to show that a simplification is correct.

I think the step-by-step proof is fine. The only suggestion I have is
to change '0 < fabs(a)' to 'fabs(a) > 0'. The latter is a lot easier
for me to think about for some reason, and the proof becomes more
obviously a proof.