Skip to content

QCheck 1/2 expect tests - #153

Merged
c-cube merged 53 commits into
c-cube:masterfrom
jmid:qcheck1-2-expect-tests
Aug 17, 2021
Merged

QCheck 1/2 expect tests#153
c-cube merged 53 commits into
c-cube:masterfrom
jmid:qcheck1-2-expect-tests

Conversation

@jmid

@jmidjmid commented Aug 13, 2021

Copy link
Copy Markdown
Collaborator

This PR contains the beginnings of an expect test suite for both QCheck and QCheck2.
It consists of a bunch of positive and negative tests formulated with both.
With the expected output this makes a regression comparison possible, using:

 diff -y test/core/qcheck_output.txt.expected test/core/qcheck2_output.txt.expected

For this reason it focuses on tests which can be phrased with both implementations.

The test suite started with the original tests from example/QCheck_runner_test.ml

  • they have been grouped thematically and renamed
  • more tests have been written
  • I've added tests from some of the issues and PRs

Overall, the idea was to supplement the unit tests from @sir4ur0n in test/core/test.ml
with a PBT test suite - and leave the example-directory for ... examples ;-)
There is still plenty more to do.
There's also results we should discuss - I'll try to mention them one-by-one below.

@jmid

jmid commented Aug 13, 2021

Copy link
Copy Markdown
CollaboratorAuthor

Here comes a number of observations. We can create issues for them if need be.
Some things concern QCheck2 (ping to @sir4ur0n@vch9) and others to the "original" QCheck prior to integrated shrinking.

QCheck2.Gen.list_size crashes with Stack_overflow

I added a few tests with a sized list generator from issue #64 which crashes the QCheck2.Gen.list_size generator with Stack_overflow. I believe that this is because it isn't tail recursive like foldn underlying QCheck.Gen.list_size:
https://github.com/c-cube/qcheck/pull/153/files#diff-44df483bf5666cb8dd729f02820e34cec6c7b7199bedcb551d82fcfccdff8c05R160-R176
Can it be formulated with an accumulator instead?

On the other hand, the test list_shorter_4332 triggers (too) aggressive QCheck.list shrinking behaviour which causes it to take a long time shrinking. Even using only QCheck.Shrink.list_spine (like #64) it still takes a bit (too) long. If the plan is to switch to QCheck2 long term I don't know whether it should be fixed.

@jmid

jmid commented Aug 13, 2021

Copy link
Copy Markdown
CollaboratorAuthor

QCheck.char doesn't shrink, but QCheck2.Gen.char does

I was surprised to discover this - illustrated by test char_is_never_abcdef.
QCheck reports a 'd' counterexample, while QCheck2 shrinks it to a:

Test char is never produces 'abcdef' failed (0 shrink steps): |	Test char is never produces 'abcdef' failed (1 shrink steps):
'd' |	'a'

This is a defect in QCheck.char IMO - users would expect it to shrink.

@jmid

jmid commented Aug 13, 2021

Copy link
Copy Markdown
CollaboratorAuthor

QCheck shrinks but QCheck2 doesn't

The reverse is also the case, however this is generally expected as integrated shrinking promises to only shrink to counterexamples that the generator can produce.

When the first counterexample found is max_int, e.g., from small_int_corners in this test:

(* test from issue #59 *)let ints_smaller_209609 =Test.make ~name:"ints < 209609"~print:Print.int
(Gen.small_int_corners()) (funi -> i <209609)

this results in different counterexamples reported by the two approaches:

Test ints < 209609 failed (52 shrink steps): |	Test ints < 209609 failed (0 shrink steps):
209609 |	4611686018427387903

This behaviour is debatable. On the one hand as a user, I would like the smallest counterexample reported.
On the other hand I don't think the generator can produce 209609 in the first place, so it can also confuse users needlessly by reporting it.
Another variant of this issue is big bound issue59 (manually choosing between a number or corner cases).

Comparing the output of the test long_shrink

let long_shrink =let listgen =Gen.(list_size (int_range 100010000) int) inTest.make ~name:"long_shrink"~print:Print.(pair (listint) (listint))
(Gen.pair listgen listgen)
(fun (xs,ys) -> List.rev (xs@ys) = (List.rev xs)@(List.rev ys))

the difference in counterexamples is much less debatable:

Test long_shrink failed (149 shrink steps): |	Test long_shrink failed (3040 shrink steps):
([0], [-1]) |	([0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; ...(two lists of length 1000 cut off by my terminal)

Since the user explicitly asks for lists of length 1000-10000 list this QCheck2 behaviour seems quite reasonable.

@jmid

jmid commented Aug 16, 2021

Copy link
Copy Markdown
CollaboratorAuthor

Sub-optimal string shrinkers

By design, with integrated shrinking a shrinker inherits the generator's structure. As a consequence, the reduced counterexamples are not as small as previously. Here's diff -y of string_never_has_000_char and string_never_has_255_char:

--- Failure -------------------------------------------------	--- Failure -------------------------------------------------
Test string never has a \000 char failed (25 shrink steps): |	Test string never has a \000 char failed (22 shrink steps):
"\000" |	"aaaaaa\000aaaaaaaaaaaaaaaa"
--- Failure -------------------------------------------------	--- Failure -------------------------------------------------
Test string never has a \255 char failed (249 shrink steps): |	Test string never has a \255 char failed (59 shrink steps):
"\255" |	"aaaaaaaaaaaaaaaaaaaaaaaaaa\255aaaaaaaaaaaaaaaaaaaaaaaa"

Since Gen.string ends up calling Gen.bytes_size - and since that generates a random size first and subsequently a string of that desired size, I believe the shrinker first investigates the shrink tree of size to find the smallest one to fail the property, and then fixes that while reducing the individual characters. This can be confirmed with a shrink log (here I just list successful string shrinks):

"\011\241\027<r\r\130\187\151\200'\000\181,\019qi7\193\029\195\218L\210\186_"
"V\020\214t\235a\000hl\014z\200\243,\227\171Sg\172\211\244\183F"
"a\020\214t\235a\000hl\014z\200\243,\227\171Sg\172\211\244\183F"
"aa\214t\235a\000hl\014z\200\243,\227\171Sg\172\211\244\183F"
"aaat\235a\000hl\014z\200\243,\227\171Sg\172\211\244\183F"
"aaaa\235a\000hl\014z\200\243,\227\171Sg\172\211\244\183F"
"aaaaaa\000hl\014z\200\243,\227\171Sg\172\211\244\183F"
"aaaaaa\000al\014z\200\243,\227\171Sg\172\211\244\183F"
"aaaaaa\000aa\014z\200\243,\227\171Sg\172\211\244\183F"
... [some line omitted]
"aaaaaa\000aaaaaaaaaaaaa\244\183F"
"aaaaaa\000aaaaaaaaaaaaaa\183F"
"aaaaaa\000aaaaaaaaaaaaaaaF"
"aaaaaa\000aaaaaaaaaaaaaaaa"

The first line lists the first random string with a \000 found.
The second line lists a second, smaller random string with a \000 (size was shrunk).
At this point the generator cannot manage to find a smaller random string with a \000 so it starts reducing irrelevant characters to 'a'.
Interestingly, because the char generator in line 2 is started in a different state st the second counterexample bears no resemblance to the first! I think this is a good reason to reconsider using a splittable random number generator (issue #86) - or at least an approximation thereof using RS.copy.

Generally I think we should consider using a smarter default string shrinker, e.g., similar to those from QCheck.list and QCheck2.Shrink.number_towards. After all, since we know that Gen.char can produce any of these characters and sizes of 0-9999 with Gen.nat, it can also produce "\000".
In comparison, the QCheck shrink log reads:

"\011\241\027<r\r\130\187\151\200'\000\181,\019qi7\193\029\195\218L\210\186_"
"\241\027<r\r\130\187\151\200'\000\181,\019qi7\193\029\195\218L\210\186_"
"\027<r\r\130\187\151\200'\000\181,\019qi7\193\029\195\218L\210\186_"
"<r\r\130\187\151\200'\000\181,\019qi7\193\029\195\218L\210\186_"
"r\r\130\187\151\200'\000\181,\019qi7\193\029\195\218L\210\186_"
"\r\130\187\151\200'\000\181,\019qi7\193\029\195\218L\210\186_"
"\130\187\151\200'\000\181,\019qi7\193\029\195\218L\210\186_"
"\187\151\200'\000\181,\019qi7\193\029\195\218L\210\186_"
"\151\200'\000\181,\019qi7\193\029\195\218L\210\186_"
"\200'\000\181,\019qi7\193\029\195\218L\210\186_"
"'\000\181,\019qi7\193\029\195\218L\210\186_"
"\000\181,\019qi7\193\029\195\218L\210\186_"
"\000,\019qi7\193\029\195\218L\210\186_"
"\000\019qi7\193\029\195\218L\210\186_"
"\000qi7\193\029\195\218L\210\186_"
"\000i7\193\029\195\218L\210\186_"
"\0007\193\029\195\218L\210\186_"
"\000\193\029\195\218L\210\186_"
"\000\029\195\218L\210\186_"
"\000\195\218L\210\186_"
"\000\218L\210\186_"
"\000L\210\186_"
"\000\210\186_"
"\000\186_"
"\000_"
"\000"

Notice the different strategy of repeated modifications of the original counter example. As a side note we could improve QCheck.string's shrinker to use bisection instead, since this will take needlessly long for long strings).
Secondly, I noticed that the QCheck.string shrinker doesn't reduce the contained characters:

Test strings are empty failed (249 shrink steps): |	Test strings are empty failed (8 shrink steps):
"\177" |	"a"

So that's another possible improvement we could consider.

@c-cube

Copy link
Copy Markdown
Owner

just a remark:

Secondly, I noticed that the QCheck.string shrinker doesn't reduce the contained characters:

I think that jives with your remark earlier that we don't shrink char at all in QCheck 🙂

@jmid

jmid commented Aug 16, 2021

Copy link
Copy Markdown
CollaboratorAuthor

Unclear QCheck2.Gen.small_string signature

The interface says:

valsmall_string : ?gen:chart -> stringt(** Builds a string generator, length is {!small_nat}. Accepts an optional character generator (the default is {!char}). Shrinks on the number of characters first, then on the characters.*)

However I had problems using it without the optional argument. Then I noticed the implementation:

letsmall_string?genst= string_size ?gen small_nat st

This implementation uses a labelled but required argument (notice there is no default value provided).
If we want to continue with optional generator parameters following the discussion in #75 and #155 this definition should probably read:

letsmall_string?(gen = char)st= string_size ?gen small_nat st

@jmid

jmid commented Aug 16, 2021

Copy link
Copy Markdown
CollaboratorAuthor

I think that jives with your remark earlier that we don't shrink char at all in QCheck slightly_smiling_face

I'm not sure I follow you. The QCheck.Shrink.string algorithm doesn't use any char shrinker:

letstringsyield=for i =0toString.length s-1dolet s' =Bytes.init (String.length s-1)
(funj -> if j<i then s.[j] else s.[j+1])
in
yield (Bytes.unsafe_to_string s')
done

We nevertheless have a QCheck.Shrink.char shrinker:

letcharcyield=ifChar.code c >0then yield (Char.chr (Char.code c-1))

It just isn't used by QCheck.char (I just noticed 🤔). So even if we define the latter as

letchar= make_scalar ~print:(sprintf "%C") ~shrink:Shrink.charGen.char

char tests could reduce chars, while string tests wouldn't.

@c-cube

Copy link
Copy Markdown
Owner

my bad, I also thought we didn't have a Shrink.char. there's a lot to be unearthed here it seems.

@sir4ur0n

Copy link
Copy Markdown
Contributor

About #153 (comment) in my opinion QCheck2 behaves correctly - and no, I'm not saying that because I rewrote/changed a big part of it 😄

small_int_corners

In my opinion this is a weird, maybe even bad function to begin with 😅 (I understand the reason why it exists, but IMHO it's more a use case for frequency).

Anyway, there's no way to know how to shrink once graft_corners is used. Maybe the corners even violate the invariants of the generator to begin with!

Note that the documentation of small_int_corners does not mention shrinking.

Shrinking of big list

Since the user explicitly asks for lists of length 1000-10000 list this QCheck2 behaviour seems quite reasonable.

I 💯 agree with you

@sir4ur0n

Copy link
Copy Markdown
Contributor

Thank you @jmid for the PR and the analysis, it's really neat 👍 Well done!

I have opened issues for what I believe are QCheck2 problems (the stackoverflow may or may not be an important issue; the string shrinking is not in my opinion)

@jmid

jmid commented Aug 17, 2021

Copy link
Copy Markdown
CollaboratorAuthor

I just have a few more ones that I would like to add (they take a bit of time to analyze and write up though...):

Sub-optimal list shrinkers

Similar to strings, lists in QCheck2.Gen are generated and thus shrunk by size first and afterwards proceeding to the element reduction (with a fixed size). Again this leads to small but not minimal counterexamples, e.g., for this test:

let list_unique_elems =Test.make ~name:"lists have unique elems"~print:Print.(listint)
Gen.(list small_int)
(funxs -> let ys =List.sort_uniq Int.compare xs in
print_list xs; List.length xs =List.length ys)

The reported counterexamples differ:

Test lists have unique elems failed (7 shrink steps): |	Test lists have unique elems failed (11 shrink steps):
[7; 7] |	[0; 0; 0; 0; 0]

Above I've added a side-effect to the property that prints the tested input every time the property is tested. This gives a log of all shrink attempts - both successful and unsuccessful ones (the shrink log of #88 only logs successful ones).

Here's the QCheck shrink log:

[7; 1; 42; 1; 8; 5; 3; 9; 5; 38; 3; 3; 0; 1; 98; 1; 4; 13; 9; 2; 6; 9; 47; 6; 5; 8; 8; 6; 0; 9; 7; 2; 8; 6; 62; 6; 4; 31; 19; 1; 41; 60; 6; 5; 8; 1; 1; 4; 7; 7; 0; 5; 5; 71; 14; 26; 47; 5; 1; 6; 34; 9; 4; 2; 37; 3; 8; 4; 31; 6; 2; 1; 0; 7; 5; 1; 0; 15; 6; 1; 8; 13; 0; 6; 2; 4; 2; 6; 6; 1; 4; 1; 9; 79; 0; 87; 6; 8; 8; 62; 1; 4; 62; 6; 31; 1; 5; 6; 5; 9; 3; 3; 1; 79; 4; 3; 2; 67; 5; 7; 12; 70; 8; 8; 6; 1; 3; 14; 15; 1; 61; 4; 1; 4; 1; 7; 4; 4; 4; 2; 8; 8; 7; 5; 4; 27; 0; 9; 80; 25; 1; 8; 1; 3; 7; 4; 3; 5; 5; 6; 5; 5; 31; 7; 0; 3; 3; 6; 71; 76; 28; 60; 6; 2; 6; 3; 0; 4; 1; 0; 5; 7; 0; 28; 86; 4; 7; 51; 36; 0; 5; 0; 1; 4; 3; 6; 0; 1; 1; 8; 18; 4; 2; 8; 8; 1; 4; 7; 1; 0; 93; 5; 3; 0; 80; 1; 7; 7; 8; 8; 5; 7; 8; 9; 24; 4; 25; 8; 8; 5; 4; 90; 4; 6; 8; 4; 4; 0; 60; 8; 9; 7; 44; 5; 1; 2; 9; 74; 7; 7]
[1; 3; 14; 15; 1; 61; 4; 1; 4; 1; 7; 4; 4; 4; 2; 8; 8; 7; 5; 4; 27; 0; 9; 80; 25; 1; 8; 1; 3; 7; 4; 3; 5; 5; 6; 5; 5; 31; 7; 0; 3; 3; 6; 71; 76; 28; 60; 6; 2; 6; 3; 0; 4; 1; 0; 5; 7; 0; 28; 86; 4; 7; 51; 36; 0; 5; 0; 1; 4; 3; 6; 0; 1; 1; 8; 18; 4; 2; 8; 8; 1; 4; 7; 1; 0; 93; 5; 3; 0; 80; 1; 7; 7; 8; 8; 5; 7; 8; 9; 24; 4; 25; 8; 8; 5; 4; 90; 4; 6; 8; 4; 4; 0; 60; 8; 9; 7; 44; 5; 1; 2; 9; 74; 7; 7]
[36; 0; 5; 0; 1; 4; 3; 6; 0; 1; 1; 8; 18; 4; 2; 8; 8; 1; 4; 7; 1; 0; 93; 5; 3; 0; 80; 1; 7; 7; 8; 8; 5; 7; 8; 9; 24; 4; 25; 8; 8; 5; 4; 90; 4; 6; 8; 4; 4; 0; 60; 8; 9; 7; 44; 5; 1; 2; 9; 74; 7; 7]
[8; 5; 7; 8; 9; 24; 4; 25; 8; 8; 5; 4; 90; 4; 6; 8; 4; 4; 0; 60; 8; 9; 7; 44; 5; 1; 2; 9; 74; 7; 7]
[4; 4; 0; 60; 8; 9; 7; 44; 5; 1; 2; 9; 74; 7; 7]
[5; 1; 2; 9; 74; 7; 7]
[74; 7; 7]
[7]
[74]
[7; 7]
[7]
[7]
[4; 7]
[6; 7]
[6; 7]
[7; 4]
[7; 6]
[7; 6]

Using bisection the algorithm uses the first 7 steps to find [74;7;7]. After two failures it finds [7;7] which it fails 8 times to reduce further and thus reports [7;7].

The shrink log of QCheck2 reads:

[7; 1; 42; 1; 8; 5; 3; 9; 5; 38; 3; 3; 0; 1; 98; 1; 4; 13; 9; 2; 6; 9; 47; 6; 5; 8; 8; 6; 0; 9; 7; 2; 8; 6; 62; 6; 4; 31; 19; 1; 41; 60; 6; 5; 8; 1; 1; 4; 7; 7; 0; 5; 5; 71; 14; 26; 47; 5; 1; 6; 34; 9; 4; 2; 37; 3; 8; 4; 31; 6; 2; 1; 0; 7; 5; 1; 0; 15; 6; 1; 8; 13; 0; 6; 2; 4; 2; 6; 6; 1; 4; 1; 9; 79; 0; 87; 6; 8; 8; 62; 1; 4; 62; 6; 31; 1; 5; 6; 5; 9; 3; 3; 1; 79; 4; 3; 2; 67; 5; 7; 12; 70; 8; 8; 6; 1; 3; 14; 15; 1; 61; 4; 1; 4; 1; 7; 4; 4; 4; 2; 8; 8; 7; 5; 4; 27; 0; 9; 80; 25; 1; 8; 1; 3; 7; 4; 3; 5; 5; 6; 5; 5; 31; 7; 0; 3; 3; 6; 71; 76; 28; 60; 6; 2; 6; 3; 0; 4; 1; 0; 5; 7; 0; 28; 86; 4; 7; 51; 36; 0; 5; 0; 1; 4; 3; 6; 0; 1; 1; 8; 18; 4; 2; 8; 8; 1; 4; 7; 1; 0; 93; 5; 3; 0; 80; 1; 7; 7; 8; 8; 5; 7; 8; 9; 24; 4; 25; 8; 8; 5; 4; 90; 4; 6; 8; 4; 4; 0; 60; 8; 9; 7; 44; 5; 1; 2; 9; 74; 7; 7]
[]
[9; 61; 8; 4; 69; 2; 0; 72; 4; 41; 3; 8; 75; 83; 7; 7; 3; 9; 5; 8; 4; 1; 0; 2; 1; 4; 7; 6; 2; 1; 4; 86; 3; 79; 7; 86; 52; 39; 19; 0; 4; 7; 7; 7; 0; 4; 8; 8; 0; 5; 13; 1; 5; 0; 7; 12; 64; 34; 1; 1; 85; 8; 2; 9; 76; 0; 2; 5; 76; 69; 8; 8; 0; 1; 2; 2; 4; 60; 29; 5; 9; 4; 0; 8; 3; 3; 5; 1; 35; 8; 2; 7; 23; 61; 56; 8; 1; 1; 78; 7; 5; 0; 30; 9; 3; 7; 28; 57; 98; 3; 52; 3; 82; 7; 5; 5; 6; 8; 1; 6; 8; 9; 8; 16; 0]
[]
[1; 9; 8; 28; 47; 8; 5; 6; 8; 9; 2; 5; 8; 30; 6; 8; 84; 0; 6; 7; 76; 7; 9; 1; 0; 5; 76; 95; 2; 2; 1; 45; 7; 8; 8; 1; 6; 37; 5; 6; 73; 8; 0; 85; 8; 0; 4; 5; 2; 0; 26; 59; 0; 5; 13; 4; 7; 3; 6; 8; 1; 3]
[]
[5; 0; 0; 4; 10; 2; 4; 9; 5; 73; 6; 1; 5; 5; 3; 10; 5; 31; 1; 4; 3; 8; 9; 13; 41; 20; 96; 5; 1; 2; 8]
[]
[9; 8; 73; 5; 8; 2; 1; 8; 2; 6; 4; 18; 5; 76; 3]
[]
[0; 6; 2; 8; 8; 1; 4]
[]
[5; 2; 3]
[3; 2; 7; 3; 3]
[]
[5; 3]
[5; 3; 2]
[9; 87; 7; 0]
[0; 2; 7; 3; 3]
[0; 0; 7; 3; 3]
[0; 0; 0; 3; 3]
[0; 0; 0; 0; 3]
[0; 0; 0; 0; 0]

There is a couple of things to observe here:

  1. Again, like for strings, the state of the random number generator has evolved after the first generated counterexample, so the generated elements up to [3;2;7;3;3] has no resemblance to each other. At this point it tries to generate a list of size 0-4 with duplicates and fails (randomly). It thus settles on size 5 and reduces the elements to 0s. When it gets to the two 3s there are already duplicate 0s in the list, so it can proceed to reduce 🙃
  2. While reducing size, every second attempt tried is [] (size 0). This is a consequence of using Tree.make_primitive in Gen.nat - which calls itself recursively with the same shrinker argument (Shrink.int_towards with a shrink destination of 0) as far as I can tell.

For 1, I really think we should consider

  • using some kind of splittable RNG.
    (I have a "poor mans" implementation based on Random.State here: https://github.com/jmid/sm2-tes21/blob/main/lec10/intqc.ml#L66-L75)
  • improve the built-in list shrinker to approach the algorithmic behaviour of QCheck a bit more.
    Continuing from the found counterexample is a good start I think. Then one could extract a sub-list of shrunk_size elements (they could be consecutive) where shrunk_size comes from the shrink tree of size.
    For other client, e.g., of list_size with custom sizes and custom generators (silly example: "prime length lists of Fibonacci numbers") this of course shouldn't apply, but for simple Gen.(list int) usage it would be nice if the shrinker's effectiveness was roughly the same.

For 2, I tried to optimize the original list shrinker in #64 by removing such repeated empty tests for it. Back then this came at the price of trying [] last - by bisection we will eventually hit the empty list.
In QCheck2 it is an artifact of the natsize shrinker, which emits a (redundant) 0 first in the suggestion Seq at each recursion layer of Tree.make_primitive call. This is confirmed by ints_are_0 (it uses Gen.int but the behaviour is the same for Gen.nat):

let ints_are_0 =Test.make ~name:"ints are 0"~count:1000~print:Print.intGen.int (funi -> Printf.printf "%i\n" i; i =0)

and its shrink log:

1571754099758104554
0
785877049879052277
0
392938524939526138
0
196469262469763069
0
98234631234881534
0
49117315617440767
0
24558657808720383
0
12279328904360191
0
6139664452180095
0
3069832226090047
0
1534916113045023
0
767458056522511
0
383729028261255
0
191864514130627
0
95932257065313
0
47966128532656
0
23983064266328
0
11991532133164
0
5995766066582
0
2997883033291
0
1498941516645
0
749470758322
0
374735379161
0
187367689580
0
93683844790
0
46841922395
0
23420961197
0
11710480598
0
5855240299
0
2927620149
0
1463810074
0
731905037
0
365952518
0
182976259
0
91488129
0
45744064
0
22872032
0
11436016
0
5718008
0
2859004
0
1429502
0
714751
0
357375
0
178687
0
89343
0
44671
0
22335
0
11167
0
5583
0
2791
0
1395
0
697
0
348
0
174
0
87
0
43
0
21
0
10
0
5
0
2
0
1
0

So this aspect of the list shrinker issue turns out to be about the int shrinker (and friends)... 😀
What to do? Potentially we could adjust Number.int_towards to similarly be less aggressive and try 0 later. However after comparing my share of shrink logs for QCheck and QCheck2 I have grown (only slightly) wiser 😉 and see value in how QCheck2 tries a 0 first:

  • it quickly helps reduce irrelevant entries, e.g., in an int list, rather than say, repeatedly halve every entry to get there (in comparison, for list_shorter_10 QCheck uses 50 shrink steps whereas QCheck2 uses only 16 steps. For longer lists it hurts more, e.g., list_shorter_432 QCheck uses 1696 shrink steps, so it could definitely be improved by using such a strategy)
  • as ints drive size-generators of other generators (list, string, ...) these should benefit as well in terms of smaller shrink trees (less memory) and speed (less redundant inputs tested).

As such, ideally I would prefer to keep 0 in line 2 above and remove all subsequent ones. I think this is possible. We could adjust Shrink.number_towards to not include destination in the returned sequence and instead return it as the first component of a pair: 'a * ('a -> 'a Seq).
Carrying a root/destination 'a option down through the recursion of make_primitive would then be one way to signal insertion only at the desired top/root position. Alternatively (isomorphically?) one could have two functions Tree.(make_primitive_zero, make_primitive) and have the first glue a destination at the top/root of Tree.make_primitive's output (it can probably be done more elegantly).

@jmid

jmid commented Aug 17, 2021

Copy link
Copy Markdown
CollaboratorAuthor

Sub-optimal function shrinkers

A number of the function tests illustrate a difference in the function shrinker's output (terminal cuts off at width 160):

--- Failure -----------------------------------------------------------------	--- Failure -----------------------------------------------------------------
Test fail_pred_map_commute failed (127 shrink steps): |	Test fail_pred_map_commute failed (16 shrink steps):
([3], {_ -> 0}, {3 -> false; _ -> true}) |	([2], {_ -> 0}, {1 -> false; 2 -> true; _ -> false})
...
--- Failure -----------------------------------------------------------------	--- Failure -----------------------------------------------------------------
Test fold_left fold_right failed (25 shrink steps): |	Test fold_left fold_right failed (22 shrink steps):
(0, [1], {(1, 0) -> 1; _ -> 0}) |	(0, [1], {(1, 0) -> 1; (8, 0) -> 0; (8, 8) -> 0; (8, 93) -> 0; (7, 7) -> 0; (
...
--- Failure -----------------------------------------------------------------	--- Failure -----------------------------------------------------------------
Test fold_left fold_right uncurried failed (111 shrink steps): |	Test fold_left fold_right uncurried failed (325 shrink steps):
({(5, 7) -> 0; _ -> 7}, 0, [5; 0]) |	({(23, 62) -> 0; (9, 42) -> 0; (8, 61) -> 0; (8, 5) -> 0; (30, 5) -> 0; (9, 6
--- Failure -----------------------------------------------------------------	--- Failure -----------------------------------------------------------------
Test fold_left fold_right uncurried fun last failed (26 shrink steps): |	Test fold_left fold_right uncurried fun last failed (25 shrink steps):
(0, [1], {(0, 1) -> 1; _ -> 0}) |	(0, [1], {(0, 2) -> 0; (8, 80) -> 0; (93, 9) -> 0; (7, 24) -> 0; (8, 0) -> 0;

The steps spent vary between the two approaches. The last two are perhaps most saying.
First off, here's the counterexamples reported by QCheck2:

--- Failure --------------------------------------------------------------------
Test fold_left fold_right uncurried failed (325 shrink steps):
({(23, 62) -> 0; (9, 42) -> 0; (8, 61) -> 0; (8, 5) -> 0; (30, 5) -> 0; (9, 6) -> 0; (76, 6) -> 0; (19, 31) -> 0; (7, 62) -> 0; (0, 7) -> 1; (7, 1) -> 0; (78, 4) -> 0; (8, 2) -> 0; (78, 0) -> 0; (3, 47) -> 0; (4, 8) -> 0; (98, 9) -> 0; (1, 38) -> 0; (0, 26) -> 0; (1, 7) -> 0; (86, 3) -> 0; (9, 37) -> 0; (8, 1) -> 0; (79, 9) -> 0; (3, 5) -> 0; (56, 8) -> 0; (2, 5) -> 0; (8, 8) -> 0; (56, 67) -> 0; (5, 60) -> 0; (2, 31) -> 0; (61, 6) -> 0; (12, 5) -> 0; (76, 2) -> 0; (78, 8) -> 0; (1, 1) -> 0; (8, 9) -> 0; (7, 8) -> 0; (2, 9) -> 0; (29, 7) -> 0; (5, 8) -> 0; (28, 6) -> 0; (1, 4) -> 0; (9, 79) -> 0; (0, 1) -> 0; (1, 41) -> 0; (82, 98) -> 0; (6, 79) -> 0; (7, 6) -> 0; (4, 3) -> 0; (8, 12) -> 0; (5, 1) -> 0; (39, 1) -> 0; (3, 6) -> 0; (1, 2) -> 0; (76, 31) -> 0; (4, 1) -> 0; (6, 5) -> 0; (0, 8) -> 0; (8, 7) -> 0; (2, 6) -> 0; (52, 5) -> 0; (8, 47) -> 0; (5, 3) -> 0; (7, 9) -> 0; (13, 13) -> 0; (0, 87) -> 0; (82, 0) -> 0; (34, 8) -> 0; (1, 14) -> 0; (2, 71) -> 0; (52, 4) -> 0; (1, 3) -> 0; (85, 6) -> 0; (8, 19) -> 0; (3, 13) -> 0; (69, 1) -> 0; (5, 62) -> 0; (0, 15) -> 0; (34, 0) -> 0; (9, 4) -> 0; (0, 6) -> 0; (1, 8) -> 0; (86, 6) -> 0; (4, 5) -> 0; (3, 1) -> 0; (57, 2) -> 0; (3, 3) -> 0; (4, 0) -> 0; (30, 6) -> 0; (5, 34) -> 0; (0, 4) -> 0; (2, 3) -> 0; (5, 6) -> 0; (5, 7) -> 0; (5, 0) -> 0; (4, 4) -> 0; (7, 5) -> 0; (78, 2) -> 0; (9, 8) -> 0; (7, 70) -> 0; (35, 1) -> 0; (64, 7) -> 0; (60, 0) -> 0; (1, 9) -> 0; _ -> 0}, 0, [0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 0; 7])
--- Failure --------------------------------------------------------------------
Test fold_left fold_right uncurried fun last failed (25 shrink steps):
(0, [1], {(0, 2) -> 0; (8, 80) -> 0; (93, 9) -> 0; (7, 24) -> 0; (8, 0) -> 0; (9, 7) -> 0; (0, 24) -> 0; (0, 7) -> 0; (7, 1) -> 0; (8, 9) -> 0; (24, 0) -> 0; (5, 8) -> 0; (1, 0) -> 1; (4, 8) -> 0; (7, 0) -> 0; (5, 7) -> 0; (8, 4) -> 0; (24, 5) -> 0; (0, 1) -> 0; (2, 8) -> 0; (9, 1) -> 0; (8, 8) -> 0; _ -> 0})

It is clear that generating functions last in a tuple rather than first (a hard-learned lesson from issue #8) is still a clear win for integrated shrinking. Still, there is quite a few more bindings reported in the above counterexample compared to QCheck.
Looking at the function generator and shrinker I can see a list of bindings is reduced using Tree.applicative_take which takes at 0-len bindings:

letshrinks : (k, v) t Tree.t Seq.t =fun() ->
(* This only gets evaluated *after* the test was run for [tbl], meaning it is correctly populated with bindings recorded during the test already *)letcurrent_bindings : (k * v Tree.t) list =List.rev !(root.p_tree_bindings_rev) inlettake_at_most_tree : int Tree.t =Tree.make_primitive (Shrink.int_towards 0) (List.length current_bindings) inletcurrent_tree_bindings : (k * v) Tree.t list =List.map (fun (k, tree) -> Tree.map (funv -> (k, v)) tree) current_bindings inletshrunk_bindings_tree : (k * v) list Tree.t =Tree.bind take_at_most_tree (funtake_at_most -> Tree.applicative_take take_at_most current_tree_bindings) in(* During shrinking, we don't want to record/add bindings, so [~extend:false]. *)letshrunk_poly_tbl_tree : (k, v) t Tree.t =Tree.map (funbindings -> List.to_seq bindings |>T.of_seq |> make ~extend:false) shrunk_bindings_tree in(* [shrunk_poly_tbl_tree] is a bit misleading: its root *should* be the same as [root] but because of the required laziness induced by the mutation of bindings, we don't use it, only graft its children to the original [root]. *)Tree.children shrunk_poly_tbl_tree ()inTree.Tree (root, shrinks)

This looks like a quick algorithmic list shrinker to me - also with opportunities for improvements.

It puzzled me that the take_at_most wasn't reducing the above list of bindings further. After all, the outlier binding (1, 0) -> 1 is in the middle!

I therefore added a shrink log of successful shrink attempts by replacing l.355 of QCheck2_expect_test.ml with:

QCheck_base_runner.run_tests ~colors:false~debug_shrink:(Some (open_out "funshrinklog.txt")) ~debug_shrink_list:["fold_left fold_right uncurried fun last"] ([

After rerunning the tests, this revealed the following in _build/default/test/core/funshrinklog.txt:


~~~ Shrink ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Test fold_left fold_right uncurried fun last sucessfully shrunk counter example (step 0) to:
(5, [7; 8; 9; 24], {(8, 80) -> 0; (7, 24) -> 7; (8, 9) -> 7; (7, 0) -> 3; (5, 7) -> 8; (24, 5) -> 1; (9, 1) -> 80; (8, 8) -> 8; _ -> 25})
~~~ Shrink ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Test fold_left fold_right uncurried fun last sucessfully shrunk counter example (step 1) to:
(0, [7; 8; 9; 24], {(8, 80) -> 0; (93, 9) -> 0; (7, 24) -> 7; (9, 7) -> 4; (0, 24) -> 1; (0, 7) -> 5; (7, 1) -> 8; (8, 9) -> 7; (24, 0) -> 7; (5, 8) -> 93; (7, 0) -> 3; (5, 7) -> 8; (8, 4) -> 1; (24, 5) -> 1; (9, 1) -> 80; (8, 8) -> 8; _ -> 25})
~~~ Shrink ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Test fold_left fold_right uncurried fun last sucessfully shrunk counter example (step 2) to:
(0, [2; 8], {(0, 2) -> 4; (8, 80) -> 0; (93, 9) -> 0; (7, 24) -> 7; (8, 0) -> 8; (9, 7) -> 4; (0, 24) -> 1; (0, 7) -> 5; (7, 1) -> 8; (8, 9) -> 7; (24, 0) -> 7; (5, 8) -> 93; (4, 8) -> 18; (7, 0) -> 3; (5, 7) -> 8; (8, 4) -> 1; (24, 5) -> 1; (2, 8) -> 1; (9, 1) -> 80; (8, 8) -> 8; _ -> 25})
~~~ Shrink ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Test fold_left fold_right uncurried fun last sucessfully shrunk counter example (step 3) to:
(0, [1], {(0, 2) -> 4; (8, 80) -> 0; (93, 9) -> 0; (7, 24) -> 7; (8, 0) -> 8; (9, 7) -> 4; (0, 24) -> 1; (0, 7) -> 5; (7, 1) -> 8; (8, 9) -> 7; (24, 0) -> 7; (5, 8) -> 93; (1, 0) -> 6; (4, 8) -> 18; (7, 0) -> 3; (5, 7) -> 8; (8, 4) -> 1; (24, 5) -> 1; (0, 1) -> 0; (2, 8) -> 1; (9, 1) -> 80; (8, 8) -> 8; _ -> 25})
~~~ Shrink ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Test fold_left fold_right uncurried fun last sucessfully shrunk counter example (step 4) to:
(0, [1], {(0, 2) -> 4; (8, 80) -> 0; (93, 9) -> 0; (7, 24) -> 7; (8, 0) -> 8; (9, 7) -> 4; (0, 24) -> 1; (0, 7) -> 5; (7, 1) -> 8; (8, 9) -> 7; (24, 0) -> 7; (5, 8) -> 93; (1, 0) -> 6; (4, 8) -> 18; (7, 0) -> 3; (5, 7) -> 8; (0, 0) -> 3; (8, 4) -> 1; (24, 5) -> 1; (0, 1) -> 0; (2, 8) -> 1; (9, 1) -> 80; (8, 8) -> 8; _ -> 0})
[...]

This looks fishy to me: while the first elements of the tuple are reduced, the last one (the function table) actually gets longer in each attempt!
I think this is actually due to how Gen.triple is currently defined (and thus shrinks). I'll therefore add some tests for it and report separately.

@jmid

jmid commented Aug 17, 2021

Copy link
Copy Markdown
CollaboratorAuthor

The last two things I had noted were:

Different Gen.int distribution

The regression diff -y finds a difference in average, standard deviation, etc. of Gen.int whereas the remaining generators reveal the exact same distribution:

+++ Stats for int dist ++++++++++++++++++++++++++++++++++++++++++++++++++++++	+++ Stats for int dist ++++++++++++++++++++++++++++++++++++++++++++++++++++++
stats dist: stats dist:
num: 100000, avg: 2541076923587387.50, stddev: 2660730801206827008.00, medi | num: 100000, avg: 6126662802445055.00, stddev: 2661484817981980672.00, medi
-4611522359435274428..-4150369195341695293: ############################### | -4611578348806740501..-4150415539984062486: ###############################
-4150369195341695292..-3689216031248116157: ############################### | -4150415539984062485..-3689252731161384470: ###############################
-3689216031248116156..-3228062867154537021: ############################### | -3689252731161384469..-3228089922338706454: ###############################
-3228062867154537020..-2766909703060957885: ############################### | -3228089922338706453..-2766927113516028438: ###############################
-2766909703060957884..-2305756538967378749: ############################### | -2766927113516028437..-2305764304693350422: ###############################
-2305756538967378748..-1844603374873799613: ############################### | -2305764304693350421..-1844601495870672406: ###############################
-1844603374873799612..-1383450210780220477: ############################### | -1844601495870672405..-1383438687047994390: ###############################
-1383450210780220476.. -922297046686641341: ############################### | -1383438687047994389.. -922275878225316374: ###############################
-922297046686641340.. -461143882593062205: ############################### | -922275878225316373.. -461113069402638358: ###############################
-461143882593062204.. 9281500516931: ############################### | -461113069402638357.. 49739420039658: ###############################
9281500516932.. 461162445594096067: ############################### | 49739420039659.. 461212548242717674: ###############################
461162445594096068.. 922315609687675203: ############################### | 461212548242717675.. 922375357065395690: ###############################
922315609687675204.. 1383468773781254339: ############################### | 922375357065395691.. 1383538165888073706: ###############################
1383468773781254340.. 1844621937874833475: ############################### | 1383538165888073707.. 1844700974710751722: ###############################
1844621937874833476.. 2305775101968412611: ############################### | 1844700974710751723.. 2305863783533429738: ###############################
2305775101968412612.. 2766928266061991747: ############################### | 2305863783533429739.. 2767026592356107754: ###############################
2766928266061991748.. 3228081430155570883: ############################### | 2767026592356107755.. 3228189401178785770: ###############################
3228081430155570884.. 3689234594249150019: ############################### | 3228189401178785771.. 3689352210001463786: ###############################
3689234594249150020.. 4150387758342729155: ############################### | 3689352210001463787.. 4150515018824141802: ###############################
4150387758342729156.. 4611540922436308291: ############################### | 4150515018824141803.. 4611677827646819818: ###############################

I believe this is expected, since QCheck2.Gen.int relies on a reworked pint generator from
bdfc905. The two underlying implementations look very much the same if one compares QCheck:

(* Uniform random int generator *)let pint =ifSys.word_size =32thenfunst -> RS.bits st
else(* word size = 64 *)funst ->
RS.bits st (* Bottom 30 bits *)lor (RS.bits st lsl30) (* Middle 30 bits *)lor ((RS.bits st land3) lsl60) (* Top 2 bits *)(* top bit = 0 *)

to QCheck2:

letpint_raw (st: RS.t) : int =ifSys.word_size =32thenRS.bits st
else(* word size = 64 *)(* Bottom 30 bits *)let right =RS.bits st in(* Middle 30 bits *)let middle = (RS.bits st lsl30) in(* Technically we could write [3] but this is clearer *)let two_bits_mask =0b11in(* Top 2 bits *)let left = ((RS.bits st land two_bits_mask) lsl60) in
left lor middle lor right

As far as I can tell, it is better documented (yay!) and the call order to RS.bits is fixed with let-bindings (also yay!). As such, I suspect the difference is actually caused by our good old friend - unspecified evaluation order of function calls 😬
With right-to-left evaluation I thus suspect the QCheck version generates the top, middle, bottom parts in that order, whereas QCheck2 enforces a bottom, middle, top order. Here I think QCheck should follow suit:

  • relying on the evaluation order is bad for reproducability
  • there would be no diff -y for the Gen.int distribution (like all other stat tests so far)

Counterexamples from mod3_should_fail differ

Finally I noted that the reported counterexample of mod3_should_fail differs between the two:

--- Failure -----------------------------------------------------------------	--- Failure -----------------------------------------------------------------
Test ints arent 0 mod 3 failed (84 shrink steps): |	Test ints arent 0 mod 3 failed (1 shrink steps):
-21 |	0

for the test:

let ints_arent_0_mod_3 =Test.make ~name:"ints arent 0 mod 3"~count:1000int (funi -> i mod3<>0)

I'll just remark here that this is another benefit of QCheck2's aggressive "try 0 / destination first" approach that I highlight and argue for above. As a consequence QCheck2 reduces in only 1 shrink step, whereas QCheck spends several steps to cut a big (negative) number down to -21, after which it fails to add 3.6,9,... to cut it further down.

end of comments

If you are happy with the PR, I'd like to merge it (rather than continue to rebase and resolve merge conflicts 😬).
Of course, you are welcome to make/suggest stylistic changes.
I just pushed tests of Gen.nat - but merging sooner rather than later would enable others to chip in (and adjust the expected output as issues are potentially fixed).

Going forward, I was imagining

  • adding tests for (some of) the remaining generators in QCheck2.Gen - ideally both a successful test in Generator, a negative test in Shrink, and a distribution test in Stats for each.
  • adding tests of custom generators (trees etc)
  • perhaps refactor the tests into two common files and keep the QCheck_base_runner drivers in the current ones. This would allow us to reuse the common files for testing the expected output of both the ounit and alcotest drivers with both QCheck and QCheck2.
  • ...

@c-cube

Copy link
Copy Markdown
Owner

My goodness, that's amazing work @jmid . I'm a bit scared of the size of it, but we're suddenly getting to best-in-class levels of testing 😁 . I think it'd be good to open separate issues for the actionable remarks (e.g. the pint order of evaluation from the last comment) to keep each discussion reasonably focused.

Sign up for freeto join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants

@jmid@c-cube@sir4ur0n@kit-ty-kate