Re: [PATCH] range-op-float: Fix up multiplication and division reverse operation [PR107879]

[Jakub Jelinek <jakub@redhat.com>]

On Mon, Dec 05, 2022 at 10:20:53AM +0100, Aldy Hernandez wrote:
> > For the division, [-0., 0.] / VARYING is computed (IMHO correctly)
> > as [-0., 0.] +-NAN, because 0 / anything but 0 or NAN is still
> > 0 and 0 / 0 is NAN and ditto 0 / NAN.  And then we just
> > float_binary_op_range_finish, which figures out that because lhs
> > can't be NAN, neither operand can be NAN.  So, the end range is
> > [-0., 0.].  But that is not correct for the reverse multiplication.
> > When the result is 0, if op2 can be zero, then x can be anything
> > (VARYING), to be precise anything but INF (unless result can be NAN),
> 
> Not an objection, just an observation... If we know it can't be INF, could
> we drop INF from the range?  We have frange_drop_{inf,ninf} for this.

Do you mind if I try that incrementally and only if it doesn't make the
code too large/too unreadable?

> > +	// If both lhs and op2 could be zeros or both could be infinities,
> > +	// we don't know anything about op1 except maybe for the sign
> > +	// and perhaps if it can be NAN or not.
> > +	REAL_VALUE_TYPE lb, ub;
> > +	int signbit_known = signbit_known_p (lhs_lb, lhs_ub, op2_lb, op2_ub);
> > +	zero_to_inf_range (lb, ub, signbit_known);
> > +	r.set (type, lb, ub);
> 
> I assume we don't know anything about the sign of the NAN because of all the
> weird IEEE rules?

Yes, sign bit of NAN is unknown after binary operation or even in the
reverse case of binary operations.
The sign rule is for non-NAN.

"When neither the inputs nor result are NaN, the sign of a product or quotient is the exclusive OR of the
operands' signs; the sign of a sum, or of a difference x–y regarded as a sum x+(–y), differs from at most one of
the addends' signs; and the sign of the result of the roundToIntegral operations and roundToIntegralExact (see
7.3.1) is the sign of the operand. These rules shall apply even when operands or results are zero or
infinite."

	Jakub