Fix QCheck{,2}.Gen.float distribution

[jmid]

I accidentally discovered that the following test ("all floats are smaller or equal than 1e10") passed:

  let float_leq_1e10 =
    Test.make ~name:"float <= 1e10" ~count:1000
      float (fun f -> f <= 1e10)

Upon further inspection, it turns out QCheck{,2}.Gen.float uses exp to generate floating point numbers and has an output with an exponent between $2^{-21}$ and $2^{22}$ (see stats output in 0f48fc2) which is far from the $2^{-1022}$ and $2^{1023}$ bounds described in https://en.wikipedia.org/wiki/Double-precision_floating-point_format. This is unfortunate, as a limited distribution means that bugs outside the above range may have flown under the rader.

This PR thus replaces the existing generator with one based on Int64.float_of_bits which is fed 64 random bits.
The latter is achieved by stitching together enough 30-bit Random.State.bits chunks together.
OCaml 4.14+ does offer Random.State.bits64 but we are already maintaining 4 expect test outputs ({ocaml4,ocaml5} x {32-bit,64-bit}) and I don't feel like extending the first set of that matrix with an OCaml 4.8.-4.13. entry. I instead suggest replacing the stitching once we push the lower bound to OCaml 4.14.

The resulting generator should have an equal chance of all 64-bit patterns - not to be confused with an equal chance of all 64-bit floating point numbers, as, e.g., multiple bit-patterns may represent nan.

I've added a collect statistic illustrating that the replacement generator may output both nan and subnormal floating point numbers for now:

Collect results for test float classify:

FP_normal: 4994 cases
FP_nan: 2 cases
FP_subnormal: 4 cases

If the interpretation differs across architectures (AMD64,ARM64,s390x,RISC-V,PPC64) we may have to remove this expect test again. I found it nice to confirm a difference with the previous distribution with all FP_normal classification.

Finally, the expect tests illustrate the need for a QCheck float shrinker. I was working on such a thing when I discovered the above limitation.

The PR is structured as follows:

• 76ade80 and 0f48fc2 add float expect tests and distribution tests illustrating the problem
• 0d7eac8 contains the fix
• 4ced52b updates the expect test outputs (illustrating how the above example test now fails as expected)
• dcf5794 and eb4af5a adds the classify_float stat

Polite ping to @c-cube and to @rmonat who has been using the QCheck2.Gen.float generator recently 🙂

[c-cube]

I think it's great. It seems like QCheck.ml has the same issue, too(!).

I wonder if the shrinker can also operate on nans by going back to the bitwise representation?

[rmonat]

Looks great, nothing to add on the generation side, thank you @jmid!

[jmid]

Thanks both! 🙏

I think it's great. It seems like QCheck.ml has the same issue, too(!).

Yep, the PR fixes both. QCheck{,2} is my (not particularly clear 😅 ) way of writing QCheck and QCheck2.

I wonder if the shrinker can also operate on nans by going back to the bitwise representation?

I hadn't considered that! 🤔
My WIP shrinker makes no attempt to shrink nans and infinities, from the rationale that these were already special enough to report as is. Like @rmonat I've also needed to print counterexamples in hex (rather than in approximate decimal) to understand and reproduce failing runs... I was therefore thinking of adding a friendly heads-up to the documentation about it.

Finally, the CI was failing on Windows, which has an annoying habit of printing a leading exponent zero in floating point numbers (such as -1.00001604579e-010) which causes the expect tests to fail...
https://github.com/c-cube/qcheck/actions/runs/16118634163/job/45478438841?pr=350

--- a/_build/default/test/core/QCheck2_expect_test.expected
+++ b/_build/default/test/core/QCheck2_expect_test.exe.output
@@ -376,13 +376,13 @@ Test float < 1.0 failed (450 shrink steps):
 
 Test float <= 1e-10 failed (482 shrink steps):
 
-1.00003747936e-10
+1.00003747936e-010
 
 --- Failure --------------------------------------------------------------------
 
 Test float >= -1e-10 failed (661 shrink steps):
 
--1.00001604579e-10
+-1.00001604579e-010
 
 --- Failure --------------------------------------------------------------------

5e65bfe lifts the workaround from #326 to apply to both Print.float functions.
I earlier opened an issue for this "papercut" here ocaml-windows/papercuts#13 but perhaps it should just be opened on/transferred to ocaml/ocaml for visibility 🤷

[rmonat]

I wonder if the shrinker can also operate on nans by going back to the bitwise representation?

I hadn't considered that! 🤔
My WIP shrinker makes no attempt to shrink nans and infinities, from the rationale that these were already special enough to report as is.

This may be equivalent, but I would rather consider shrinking on the exponent and mantissa?

[jmid]

This may be equivalent, but I would rather consider shrinking on the exponent and mantissa?

Yep, that's also my approach 👍 The WIP however gives up on nan and infinities before proceeding to do so:

  let float x yield =
    if Float.is_infinite x || Float.is_nan x then () else
   ...

[rmonat]

This may be equivalent, but I would rather consider shrinking on the exponent and mantissa?

Yep, that's also my approach 👍 The WIP however gives up on nan and infinities before proceeding to do so:

  let float x yield =
    if Float.is_infinite x || Float.is_nan x then () else
   ...

Nice! I guess it might be interesting to have a shrinker for NaNs in some specialized cases, but this is a highly advanced feature IMO.

[c-cube]

I didn't mean to derail with the NaN comment. Tbh a very simple shrinker could be that we pick a canonical NaN value and just shrink any other NaN to it (which is useful info when a bug is triggered by any NaN)