Long integer shrinking from within toplevel/utop

[jmid]

Consider the following code:

open QCheck

let rec fac n = match n with
  | 0 -> 1
  | n -> n * fac (n - 1)

let test_fac =
  Test.make ~name:"fac mod'"
    (small_int_corners ())
    (fun n -> try (fac n) mod n = 0
              with Division_by_zero -> (n=0))
;;
QCheck_runner.run_tests ~verbose:true [test_fac]

Assume you save the above to a file bug.ml.

If I compile the example test with the bytecode backend I quickly (0.5s) find the bound (262049) for blowing the bytecode stack:

$ ocamlbuild -use-ocamlfind -package qcheck bug.byte
Finished, 3 targets (0 cached) in 00:00:00.
$ ./bug.byte 
random seed: 317373207
generated error fail pass / total     time test name
[✗]    4    1    0    3 /  100     0.5s fac mod'

=== Error ======================================================================

Test fac mod' errored on (138 shrink steps):

262049

exception Stack overflow

================================================================================
failure (0 tests failed, 1 tests errored, ran 1 tests)

Similarly I can quickly (0.4s) find the bound (524115) for blowing the native-code stack:

$ ocamlbuild -use-ocamlfind -package qcheck bug.native
Finished, 4 targets (2 cached) in 00:00:00.
$ ./bug.native 
random seed: 448617552
generated error fail pass / total     time test name
[✗]    4    1    0    3 /  100     0.4s fac mod'

=== Error ======================================================================

Test fac mod' errored on (215 shrink steps):

524115

exception Stack overflow

================================================================================
failure (0 tests failed, 1 tests errored, ran 1 tests)

However, if I try the same thing within the OCaml toplevel or utop -- I consistently get very long shrinking times (237.9s) with many (52578!) shrinking steps - to the point that I thought I had hit an infinite loop:

utop # #require "qcheck";;
─( 17:51:25 )─< command 1 >────────────────────────────────────────────{ counter: 0 }─
utop # #use "bug.ml";;
val fac : int -> int = <fun>
val test_fac : Test.t = QCheck.Test.Test <abstr>
random seed: 175072808
generated error fail pass / total     time test name
[✗]    4    1    0    3 /  100   237.9s fac mod'

=== Error ======================================================================

Test fac mod' errored on (52578 shrink steps):

209609

exception Stack overflow

================================================================================
failure (0 tests failed, 1 tests errored, ran 1 tests)
- : int = 1

Is this example triggering a sore point in the built-in integer shrinker, or is something else going on?
This is on Mac OS X with OCaml 4.07.1 and QCheck 0.9.

[c-cube]

I can reproduce, indeed (although on my linux computer the native version takes a few seconds, the stack might be bigger). In the normal toplevel it takes 387s to shrink.

This is very puzzling and I doubt it's a qcheck bug in itself (the code is the same! I set a fixed random state just to be sure). Maybe it's a difference in stack size?

[williamhammond]

I compiled with
ocamlbuild -cflag -g -use-ocamlfind -package qcheck bug.native
and then ran with
OCAMLRUNPARAM=b ./bug.native
and got

exception Stack overflow
Raised by primitive operation at file "src/QCheck_runner.ml", line 407, characters 10-29
Called from file "src/QCheck.ml", line 1227, characters 9-14
Called from file "src/QCheck.ml", line 1310, characters 22-50

I just pulled the package from opam. Is there a way to get a version of the source that was used for opam? I tried to follow the trace and the latest code on github and ended up on a comment found it looking now, I'm on version 0.8

[jmid]

Here's another experiment that may (or may not) cast light on the matter:

utop # #require "qcheck";;
─( 07:50:05 )─< command 1 >────────────────────────────────────────────{ counter: 0 }─
utop # open QCheck;;
─( 07:50:09 )─< command 2 >────────────────────────────────────────────{ counter: 0 }─
utop # let t = Test.make (small_int_corners()) (fun i -> i < 209609);;
val t : Test.t = QCheck.Test.Test <abstr>
─( 07:50:15 )─< command 3 >────────────────────────────────────────────{ counter: 0 }─
utop # QCheck_runner.run_tests ~verbose:true [t];;
random seed: 14708131
generated error fail pass / total     time test name
[✗]    4    0    1    3 /  100     0.2s anon_test_1

--- Failure --------------------------------------------------------------------

Test anon_test_1 failed (52578 shrink steps):

209609
================================================================================
failure (1 tests failed, 0 tests errored, ran 1 tests)
- : int = 1
─( 07:50:19 )─< command 4 >────────────────────────────────────────────{ counter: 0 }─
utop # 

So searching (shrinking) for the minimal constant (209609) that disproves the property just takes an awful lot of shrinking steps (52578!) compared to the bytecode run (138) and native-code run (215). Doing x200 more shrinking steps is almost instant here (0.2s) but with a computationally more expensive property it will clearly be more costly.

Finally, small_int_corners() deterministically tries a number of known corner cases, before proceeding to randomized input. As far as I can see, the fourth deterministic constant tried is always max_int (the first counterexample found in both the above):

utop # Gen.generate ~n:6 (small_int_corners()).gen;;
- : int list = [9; 8; 4611686018427387903; 2; 1; 0]
─( 07:56:11 )─< command 7 >────────────────────────────────────────────{ counter: 0 }─
utop # Gen.generate ~n:6 (small_int_corners()).gen;;
- : int list = [80; 4; 4611686018427387903; 2; 1; 0]
─( 08:03:14 )─< command 8 >────────────────────────────────────────────{ counter: 0 }─
utop # Gen.generate ~n:6 (small_int_corners()).gen;;
- : int list = [776; 5; 4611686018427387903; 2; 1; 0]

which means we could investigate whether the built-in integer shrinker strategy can be revisited to better handle the present case. Orthogonally, it would also be nice to establish why the initial property is so expensive (stack overflow causing many expensive context switches?).

[c-cube]

I just merged #60, thanks to @Gbury. It does fix this issue, so maybe it was a problem of utop/toplevel having a slightly different stack size available, which lead to a bad path in integer shrinking.

Integer shrinking tried {n, n/2, n/4, n/8, …, 1, 0}, and if this failed, n-1 (and recursively). Now it tries {0, n/2, 3n/4, 7n/8, …} and falls back to n-1, but this actually works much better as a shortcut (whereas previously if n/2 failed, trying n/4 didn't make much sense).

[jmid]

This is very nice, although my brain hurts when trying to grasp the combination of recursive shrinker invocations and internal imperative state... :-D

The patch indeed solves the above by bringing the property (fun i -> i < 209609) down from 52578 (successful) shrink steps to 52 - and additionally lowering the shrink steps for
(fun i -> i < 262049) from 138 down to 46 and (fun i -> i < 524115) from 215 down to 47 when using small_int_corners().

I also tried comparing the two shrinkers on the above three properties with the int generator to see how well the new one would fare when shrinking from something different than max_int. With seed 12345 for example it reduced 494262 shrink steps to 47 on property (fun i -> i < 524115) on my machine. Thank you @Gbury ! :-)