`Test.make_cell` `~count` overflow bug

[alpaylan]

I think I hit an overflow bug when the count is too high, likely culpript (

qcheck/src/core/QCheck2.ml

Line 1621 in 7a70422

let max_gen = match max_gen with None -> count + 200 | Some x->x in

or

qcheck/src/core/QCheck2.ml

Line 1648 in 7a70422

let max_gen = match max_gen with None -> count + 200 | Some x->x in

).

Context: I maintain ETNA which also has qcheck workloads, I hit the error when I was working on a migration for one of them.

(* QCheck2.Test.check_cell silently runs zero iterations when
   `count` exceeds (max_int - 199).

   On a 64-bit system, max_int = 2^62-1 = 4611686018427387903.
   The threshold is empirically max_int - 199 = 4611686018427387704
   — at that count and above, `get_count_gen result` returns 0 even
   though the property is `fun _ -> false` and would fail at the first
   iteration if the loop ran.

   Bisect with this binary:
     dune exec ./repro.exe -- <count>

   Observed (qcheck-core 0.26 on ocaml 5.3.0 / 4.14.0):
     count=1                     -> tested=1
     count=10000000              -> tested=1
     count=4611686018427387703   -> tested=1     (max_int - 200)
     count=4611686018427387704   -> tested=0     (max_int - 199, BUG)
     count=4611686018427387903   -> tested=0     (max_int)

   This strongly suggests a `count + K` arithmetic step inside
   check_cell (or its setup) overflows to a negative int for
   `count > max_int - K`, after which the iteration loop exits
   immediately. K appears to be 200 -- likely a corner-cases buffer
   added to the user-supplied count.
*)
open QCheck2

let () =
  let count =
    if Array.length Sys.argv < 2 then max_int
    else int_of_string Sys.argv.(1)
  in
  let cell =
    Test.make_cell ~name:"never_true" ~count Gen.nat (fun _ -> false)
  in
  let result = Test.check_cell cell ~rand:(Random.State.make [| 0 |]) in
  Printf.printf
    "count=%d tested=%d\n"
    count (TestResult.get_count_gen result)

[jmid]

Thanks for the report! 🙏

Indeed for properties with preconditions that aren't always satisfied, we may need to generate some more inputs (by default count + 200), and that's not going to work well when count = max_int as you've discovered.

I guess max count (count + 200) could work instead - and the documentation will also need updating.
Do you want to submit a PR for it?

[alpaylan]

Thanks for the triage! I'll submit the PR tomorrow at latest.

[alpaylan]

Done! #410