IgnatiusPang opened a new pull request, #25741:
URL: https://github.com/apache/datafusion/pull/25741

   ## Rationale for this change
   
   In `datafusion-functions::math::round` and 
`datafusion-functions::math::trunc`:
   
   1. **Floating-point overflow and underflow to `NaN`**:
      Rounding or truncating valid finite floats with large or negative 
`decimal_places` evaluates `10_f64.powi(dp)`.
      - For `f32` with `dp >= 39` (or `f64` with `dp >= 309`), the power factor 
evaluates to `+infinity`. The functions then compute `(value * inf).round() / 
inf = inf / inf = NaN`.
      - For `f32` with `dp <= -46` (or `f64` with `dp <= -325`), the power 
factor underflows to `0.0`, computing `0.0 / 0.0 = NaN`.
      - **User-visible symptom**: `SELECT round(1.5::float4, 40)` returns `NaN` 
instead of `1.5`, and `SELECT round(1.5::float4, -50)` returns `NaN` instead of 
`0.0`.
      - **Root cause in `round_factor`**: 
`T::from(10_f64.powi(decimal_places))` returns `Some(inf)` on `f32`/`f64`, so 
the error check never triggers and infinity/zero factors pass unchecked into 
the division arithmetic.
   
   2. **Silent 64-bit to 32-bit truncation in `trunc`**:
      `compute_truncate32`, `compute_truncate64`, and `truncate_float_array` 
cast `y: i64` to `i32` via `y as i32`, which silently wraps large precision 
inputs.
   
   ## What changes are included in this PR?
   
   1. **`round_with_factor` and `round_float` safety guards**:
      - Return `value` when `!value.is_finite()`.
      - When `factor.is_infinite()` (requested decimal places exceed float 
representable resolution), return `value` unchanged.
      - When `factor.is_zero()` (negative decimal places exceed float 
magnitude), return `0.0.copysign(value)`.
   2. **`truncate_with_factor` safety guards**:
      - Return `x` when `!x.is_finite()` or `factor.is_infinite()`.
      - Return `0.0.copysign(x)` when `factor.is_zero()`.
      - Clamp 64-bit precision to `[i32::MIN, i32::MAX]` before passing to 
`powi`.
   3. **Formal Verification (Lean 4)**:
      - Formally verified boundary contracts synthesized and applied via Lean 4 
Three-Way Semantic Merge:
        - `round_with_factor_no_nan`
        - `truncate_with_factor_no_nan`
   4. **Comprehensive Regression Tests**:
      - Unit tests in `round.rs` (`test_round_float_extreme_decimal_places`) 
and `trunc.rs` (`test_truncate_extreme_precision`).
      - Integration tests in `tests/math_extreme_precision.rs`.
   
   ## What is the testing strategy for this PR?
   
   - Full crate test suite pass (407 tests total):
     ```bash
     cargo test -p datafusion-functions
   


-- 
This is an automated message from the Apache Git Service.
To respond to the message, please log on to GitHub and use the
URL above to go to the specific comment.

To unsubscribe, e-mail: [email protected]

For queries about this service, please contact Infrastructure at:
[email protected]


---------------------------------------------------------------------
To unsubscribe, e-mail: [email protected]
For additional commands, e-mail: [email protected]

Reply via email to