Improve QCheck2 string shrinking #157
Comments
|
Indeed in my opinion this is another example of why Hedgehog carries the I guess a way to go would be to add the This is also related to the current shrinking composition, so see #120 |
|
Here's an alternative version of let bytes_size ?(gen = char) (size : int t) : bytes t = fun st ->
let open Tree in
let size_tree = size st in
(* Adding char shrinks to a mutable list is expensive: ~20-30% cost increase *)
(* Adding char shrinks to a mutable lazy list is less expensive: ~15% cost increase *)
let char_trees_rev = ref [] in
let bytes = Bytes.init (root size_tree) (fun _ ->
let char_tree = gen st in
char_trees_rev := char_tree :: !char_trees_rev ;
(* Performance: return the root right now, the heavy processing of shrinks can wait until/if there is a need to shrink *)
root char_tree) in
let shrink = fun () ->
let char_trees = List.rev !char_trees_rev in
let char_list_tree = size_tree >>= fun new_size -> applicative_take new_size char_trees in
let bytes_tree = char_list_tree >|= fun char_list -> List.to_seq char_list |> Bytes.of_seq in
(* Technically [bytes_tree] is the whole tree, but for perf reasons we eagerly created the root above *)
children bytes_tree ()
in
Tree (bytes, shrink)Algorithmically it is almost identical to the previous version. Rather than try a shorter random string on a failure In the third attempt it finds a string containing a It is relatively efficient on my machine. I just cranked up a Algorithmically, it could be extended to try other sub-strings than prefixes (suffixes, middle-chunks?).
Since we are, in effect, just reducing |
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 -yofstring_never_has_000_charandstring_never_has_255_char:Since
Gen.stringends up callingGen.bytes_size- and since that generates a randomsizefirst and subsequently a string of that desiredsize, I believe the shrinker first investigates the shrink tree ofsizeto 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):The first line lists the first random string with a
\000found.The second line lists a second, smaller random string with a
\000(sizewas shrunk).At this point the generator cannot manage to find a smaller random string with a
\000so it starts reducing irrelevant characters to'a'.Interestingly, because the
chargenerator in line 2 is started in a different statestthe 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 usingRS.copy.Generally I think we should consider using a smarter default
stringshrinker, e.g., similar to those fromQCheck.listandQCheck2.Shrink.number_towards. After all, since we know thatGen.charcan produce any of these characters and sizes of 0-9999 withGen.nat, it can also produce"\000".In comparison, the QCheck shrink log reads:
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.stringshrinker doesn't reduce the contained characters:So that's another possible improvement we could consider.
Originally posted by @jmid in #153 (comment)
The text was updated successfully, but these errors were encountered: