From d1fc5b2a7199ba1b4d62e65b75ba4aef44f17425 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 16 Dec 2021 01:45:53 +0100 Subject: [PATCH 1/3] add retries parameter to QCheck and QCheck2 --- src/core/QCheck.ml | 8 ++++---- src/core/QCheck.mli | 8 +++++--- src/core/QCheck2.ml | 25 ++++++++++++++++--------- src/core/QCheck2.mli | 11 ++++++----- 4 files changed, 31 insertions(+), 21 deletions(-) diff --git a/src/core/QCheck.ml b/src/core/QCheck.ml index 74c3e312..cce2e9df 100644 --- a/src/core/QCheck.ml +++ b/src/core/QCheck.ml @@ -1680,13 +1680,13 @@ module Test = struct let make_cell ?if_assumptions_fail ?count ?long_factor ?max_gen - ?max_fail ?small:_removed_in_qcheck_2 ?name arb law + ?max_fail ?small:_removed_in_qcheck_2 ?retries ?name arb law = let {gen; shrink; print; collect; stats; _} = arb in - QCheck2.Test.make_cell_from_QCheck1 ?if_assumptions_fail ?count ?long_factor ?max_gen ?max_fail ?name ~gen ?shrink ?print ?collect ~stats law + QCheck2.Test.make_cell_from_QCheck1 ?if_assumptions_fail ?count ?long_factor ?max_gen ?max_fail ?retries ?name ~gen ?shrink ?print ?collect ~stats law - let make ?if_assumptions_fail ?count ?long_factor ?max_gen ?max_fail ?small ?name arb law = - QCheck2.Test.Test (make_cell ?if_assumptions_fail ?count ?long_factor ?max_gen ?max_fail ?small ?name arb law) + let make ?if_assumptions_fail ?count ?long_factor ?max_gen ?max_fail ?small ?retries ?name arb law = + QCheck2.Test.Test (make_cell ?if_assumptions_fail ?count ?long_factor ?max_gen ?max_fail ?small ?retries ?name arb law) let fail_report = QCheck2.Test.fail_report diff --git a/src/core/QCheck.mli b/src/core/QCheck.mli index c511d7fc..b8bfaba4 100644 --- a/src/core/QCheck.mli +++ b/src/core/QCheck.mli @@ -988,13 +988,14 @@ module Test : sig val make_cell : ?if_assumptions_fail:([`Fatal | `Warning] * float) -> ?count:int -> ?long_factor:int -> ?max_gen:int -> ?max_fail:int -> - ?small:('a -> int) -> ?name:string -> 'a arbitrary -> ('a -> bool) -> - 'a cell + ?small:('a -> int) -> ?retries:int -> ?name:string -> + 'a arbitrary -> ('a -> bool) -> 'a cell (** [make_cell arb prop] builds a test that checks property [prop] on instances of the generator [arb]. @param name the name of the test. @param count number of test cases to run, counting only the test cases which satisfy preconditions. + @param retries number of times to retry the tested property while shrinking. @param long_factor the factor by which to multiply count, max_gen and max_fail when running a long test (default: 1). @param max_gen maximum number of times the generation function @@ -1035,7 +1036,8 @@ module Test : sig val make : ?if_assumptions_fail:([`Fatal | `Warning] * float) -> ?count:int -> ?long_factor:int -> ?max_gen:int -> ?max_fail:int -> - ?small:('a -> int) -> ?name:string -> 'a arbitrary -> ('a -> bool) -> t + ?small:('a -> int) -> ?retries:int -> ?name:string -> 'a arbitrary -> + ('a -> bool) -> t (** [make arb prop] builds a test that checks property [prop] on instances of the generator [arb]. See {!make_cell} for a description of the parameters. diff --git a/src/core/QCheck2.ml b/src/core/QCheck2.ml index b17c374d..32ade153 100644 --- a/src/core/QCheck2.ml +++ b/src/core/QCheck2.ml @@ -1361,6 +1361,7 @@ module Test = struct long_factor : int; (* multiplicative factor for long test count *) max_gen : int; (* max number of instances to generate (>= count) *) max_fail : int; (* max number of failures *) + retries : int; (* max number of retries during shrinking *) law : 'a -> bool; (* the law to check *) gen : 'a Gen.t; (* how to generate/shrink instances *) print : 'a Print.t option; (* how to print values *) @@ -1409,7 +1410,7 @@ module Test = struct let make_cell ?(if_assumptions_fail=default_if_assumptions_fail) ?(count) ?(long_factor=1) ?max_gen - ?(max_fail=1) ?(name=fresh_name()) ?print ?collect ?(stats=[]) gen law + ?(max_fail=1) ?(retries=1) ?(name=fresh_name()) ?print ?collect ?(stats=[]) gen law = let count = global_count count in let max_gen = match max_gen with None -> count + 200 | Some x->x in @@ -1421,6 +1422,7 @@ module Test = struct stats; max_gen; max_fail; + retries; name; count; long_factor; @@ -1430,7 +1432,7 @@ module Test = struct let make_cell_from_QCheck1 ?(if_assumptions_fail=default_if_assumptions_fail) ?(count) ?(long_factor=1) ?max_gen - ?(max_fail=1) ?(name=fresh_name()) ~gen ?shrink ?print ?collect ~stats law + ?(max_fail=1) ?(retries=1) ?(name=fresh_name()) ~gen ?shrink ?print ?collect ~stats law = let count = global_count count in (* Make a "fake" QCheck2 arbitrary with no shrinking *) @@ -1444,6 +1446,7 @@ module Test = struct stats; max_gen; max_fail; + retries; name; count; long_factor; @@ -1451,8 +1454,8 @@ module Test = struct qcheck1_shrink = shrink; } - let make ?if_assumptions_fail ?count ?long_factor ?max_gen ?max_fail ?name ?print ?collect ?stats gen law = - Test (make_cell ?if_assumptions_fail ?count ?long_factor ?max_gen ?max_fail ?name ?print ?collect ?stats gen law) + let make ?if_assumptions_fail ?count ?long_factor ?max_gen ?max_fail ?retries ?name ?print ?collect ?stats gen law = + Test (make_cell ?if_assumptions_fail ?count ?long_factor ?max_gen ?max_fail ?retries ?name ?print ?collect ?stats gen law) let test_get_count (Test cell) = get_count cell @@ -1543,9 +1546,13 @@ module Test = struct | Run_ok | Run_fail of string list - let run_law law x = + let run_law ~retries law x = + let rec loop i = match law x with + | false -> Run_fail [] + | true -> + if i<=1 then Run_ok else loop (i-1) in try - if law x then Run_ok else Run_fail [] + loop retries with User_fail msg -> Run_fail [msg] (* QCheck1-compatibility code *) @@ -1575,7 +1582,7 @@ module Test = struct try incr count; st.handler st.test.name st.test (Shrinking (steps, !count, x)); - begin match run_law st.test.law x with + begin match run_law ~retries:st.test.retries st.test.law x with | Run_fail m when not is_err -> Some (Tree.pure x, Shrink_fail, m) | _ -> None end @@ -1590,7 +1597,7 @@ module Test = struct try incr count; st.handler st.test.name st.test (Shrinking (steps, !count, x)); - begin match run_law st.test.law x with + begin match run_law ~retries:st.test.retries st.test.law x with | Run_fail m when not is_err -> Some (x_tree, Shrink_fail, m) | _ -> None end @@ -1668,7 +1675,7 @@ module Test = struct let res = try state.handler state.test.name state.test (Testing input); - begin match run_law state.test.law input with + begin match run_law ~retries:1 state.test.law input with | Run_ok -> (* one test ok *) decr_count state; diff --git a/src/core/QCheck2.mli b/src/core/QCheck2.mli index 0bf62ff5..1c6d818a 100644 --- a/src/core/QCheck2.mli +++ b/src/core/QCheck2.mli @@ -1585,8 +1585,8 @@ module Test : sig val make_cell : ?if_assumptions_fail:([`Fatal | `Warning] * float) -> - ?count:int -> ?long_factor:int -> ?max_gen:int -> ?max_fail:int -> ?name:string -> - ?print:'a Print.t -> ?collect:('a -> string) -> ?stats:('a stat list) -> + ?count:int -> ?long_factor:int -> ?max_gen:int -> ?max_fail:int -> ?retries:int -> + ?name:string -> ?print:'a Print.t -> ?collect:('a -> string) -> ?stats:('a stat list) -> 'a Gen.t -> ('a -> bool) -> 'a cell (** [make_cell gen prop] builds a test that checks property [prop] on instances @@ -1601,6 +1601,7 @@ module Test : sig preconditions (should be >= count). @param max_fail maximum number of failures before we stop generating inputs. This is useful if shrinking takes too much time. + @param retries number of times to retry the tested property while shrinking. @param if_assumptions_fail the minimum fraction of tests that must satisfy the precondition for a success to be considered valid. @@ -1616,7 +1617,7 @@ module Test : sig val make_cell_from_QCheck1 : ?if_assumptions_fail:([`Fatal | `Warning] * float) -> ?count:int -> ?long_factor:int -> ?max_gen:int -> ?max_fail:int -> - ?name:string -> gen:(Random.State.t -> 'a) -> ?shrink:('a -> ('a -> unit) -> unit) -> + ?retries:int -> ?name:string -> gen:(Random.State.t -> 'a) -> ?shrink:('a -> ('a -> unit) -> unit) -> ?print:('a -> string) -> ?collect:('a -> string) -> stats:'a stat list -> ('a -> bool) -> 'a cell (** ⚠️ Do not use, this is exposed for internal reasons only. ⚠️ @@ -1646,8 +1647,8 @@ module Test : sig val make : ?if_assumptions_fail:([`Fatal | `Warning] * float) -> - ?count:int -> ?long_factor:int -> ?max_gen:int -> ?max_fail:int -> ?name:string -> - ?print:('a Print.t) -> ?collect:('a -> string) -> ?stats:('a stat list) -> + ?count:int -> ?long_factor:int -> ?max_gen:int -> ?max_fail:int -> ?retries:int -> + ?name:string -> ?print:('a Print.t) -> ?collect:('a -> string) -> ?stats:('a stat list) -> 'a Gen.t -> ('a -> bool) -> t (** [make gen prop] builds a test that checks property [prop] on instances of the generator [gen]. From 8e764f9793809a9e44c79b3adfe0cdaf58d8efc7 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 16 Dec 2021 01:47:57 +0100 Subject: [PATCH 2/3] add retries expect tests --- test/core/QCheck2_expect_test.ml | 5 +++++ test/core/QCheck_expect_test.ml | 5 +++++ test/core/qcheck2_output.txt.expected | 10 ++++++++-- test/core/qcheck_output.txt.expected | 10 ++++++++-- 4 files changed, 26 insertions(+), 4 deletions(-) diff --git a/test/core/QCheck2_expect_test.ml b/test/core/QCheck2_expect_test.ml index fa710abf..91e82e3c 100644 --- a/test/core/QCheck2_expect_test.ml +++ b/test/core/QCheck2_expect_test.ml @@ -65,6 +65,10 @@ module Overall = struct ] (Gen.int_bound 120) (fun _ -> true) + let retries = + Test.make ~name:"with shrinking retries" ~retries:10 ~print:Print.int + Gen.small_nat (fun i -> Printf.printf "%i %!" i; i mod 3 <> 1) + let bad_assume_warn = Test.make ~name:"WARN_unlikely_precond" ~count:2_000 ~print:Print.int Gen.int @@ -86,6 +90,7 @@ module Overall = struct error; collect; stats; + retries; bad_assume_warn; bad_assume_fail; ] diff --git a/test/core/QCheck_expect_test.ml b/test/core/QCheck_expect_test.ml index 28fc0a25..b642e6fb 100644 --- a/test/core/QCheck_expect_test.ml +++ b/test/core/QCheck_expect_test.ml @@ -67,6 +67,10 @@ module Overall = struct ]) (fun _ -> true) + let retries = + Test.make ~name:"with shrinking retries" ~retries:10 + small_nat (fun i -> Printf.printf "%i %!" i; i mod 3 <> 1) + let bad_assume_warn = Test.make ~name:"WARN_unlikely_precond" ~count:2_000 int @@ -88,6 +92,7 @@ module Overall = struct error; collect; stats; + retries; bad_assume_warn; bad_assume_fail; ] diff --git a/test/core/qcheck2_output.txt.expected b/test/core/qcheck2_output.txt.expected index 208dfb3d..efe05edb 100644 --- a/test/core/qcheck2_output.txt.expected +++ b/test/core/qcheck2_output.txt.expected @@ -1,5 +1,5 @@ random seed: 1234 -2724675603984413065 +50 7 0 0 0 0 0 0 0 0 0 0 3 3 3 3 3 3 3 3 3 3 5 5 5 5 5 5 5 5 5 5 6 6 6 6 6 6 6 6 6 6 2724675603984413065 0 1362337801992206532 0 @@ -221,6 +221,12 @@ stats num: 110..115: ####################################################### 9 116..121: ################## 3 +--- Failure -------------------------------------------------------------------- + +Test with shrinking retries failed (0 shrink steps): + +7 + !!! Warning !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! Warning for test WARN_unlikely_precond: @@ -982,7 +988,7 @@ stats dist: 4150517416584649600.. 4611686018427387903: ################# 189 ================================================================================ 1 warning(s) -failure (35 tests failed, 1 tests errored, ran 83 tests) +failure (36 tests failed, 1 tests errored, ran 84 tests) random seed: 153870556 +++ Stats for int_dist_empty_bucket ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ diff --git a/test/core/qcheck_output.txt.expected b/test/core/qcheck_output.txt.expected index 6b455dda..880df258 100644 --- a/test/core/qcheck_output.txt.expected +++ b/test/core/qcheck_output.txt.expected @@ -1,5 +1,5 @@ random seed: 1234 -2724675603984413065 +50 7 4 2 2 2 2 2 2 2 2 2 2 3 3 3 3 3 3 3 3 3 3 2724675603984413065 1362337801992206533 681168900996103267 340584450498051634 @@ -156,6 +156,12 @@ stats num: 110..115: ####################################################### 9 116..121: ################## 3 +--- Failure -------------------------------------------------------------------- + +Test with shrinking retries failed (1 shrink steps): + +4 + !!! Warning !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!! Warning for test WARN_unlikely_precond: @@ -937,7 +943,7 @@ stats dist: 4150517416584649600.. 4611686018427387903: ################# 189 ================================================================================ 1 warning(s) -failure (34 tests failed, 1 tests errored, ran 89 tests) +failure (35 tests failed, 1 tests errored, ran 90 tests) random seed: 153870556 +++ Stats for int_dist_empty_bucket ++++++++++++++++++++++++++++++++++++++++++++++++++++++++ From 3af05923d07f9d3c28d1ba1dcb163a9ca5173228 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 16 Dec 2021 23:57:28 +0100 Subject: [PATCH 3/3] add desc. in comment --- src/core/QCheck2.ml | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/core/QCheck2.ml b/src/core/QCheck2.ml index 32ade153..d7c856b0 100644 --- a/src/core/QCheck2.ml +++ b/src/core/QCheck2.ml @@ -1546,6 +1546,26 @@ module Test = struct | Run_ok | Run_fail of string list + (* run_law is a helper function for testing a property [law] on a + generated input [x]. + + When passed a ~retries number n>1, the tested property is checked + n times for each shrunk input candidate. The default value is 1, + thus causing no change in behaviour. + + Retrying a property can be useful when testing non-deterministic + code with QCheck, e.g., for multicore execution. The idea is + described in + 'Testing a Database for Race Conditions with QuickCheck' + Hughes and Bolinder, Erlang 2011, Sec.6: + + "As we explained in section 4, we ensure that tests fail when + races are present simply by repeating each test a large number of + times, and by running on a dual core machine. We obtained the + minimal failing cases in the previous section by repeating each + test 100 times during shrinking: thus we stopped shrinking a test + case only when all of its candidate shrinkings passed 100 tests + in a row." *) let run_law ~retries law x = let rec loop i = match law x with | false -> Run_fail []