diff --git a/.github/workflows/common.yml b/.github/workflows/common.yml index c9919d48..db0e55fe 100644 --- a/.github/workflows/common.yml +++ b/.github/workflows/common.yml @@ -87,7 +87,7 @@ jobs: uses: actions/checkout@v4 with: repository: c-cube/qcheck - ref: v0.23 + ref: v0.25 path: multicoretests/qcheck - name: Pre-Setup diff --git a/CHANGES.md b/CHANGES.md index 8786f9b8..f2c90549 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -6,6 +6,7 @@ and `STM_thread` by utilizing `Gc.Memprof` callbacks. Avoid on 5.0-5.2 without `Gc.Memprof` support. - #546: Speed up `Lin`'s default `string` and `bytes` shrinkers. +- #547: Add `Util.Pp.{cst4,cst5}` ## 0.7 diff --git a/dune-project b/dune-project index f6d0941e..eb6ee6ae 100644 --- a/dune-project +++ b/dune-project @@ -17,7 +17,7 @@ the multicore run-time of OCaml 5.0.") (tags ("test" "test suite" "property" "qcheck" "quickcheck" "multicore" "non-determinism")) (depends base-domains - (qcheck-core (>= "0.23")) + (qcheck-core (>= "0.25")) (qcheck-lin (= :version)) (qcheck-stm (= :version)))) @@ -31,7 +31,7 @@ sequential and parallel tests against a declarative model.") (depopts base-domains) (depends (ocaml (>= 4.12)) - (qcheck-core (>= "0.23")) + (qcheck-core (>= "0.25")) (qcheck-multicoretests-util (= :version)))) (package @@ -46,7 +46,7 @@ and explained by some sequential interleaving.") (depopts base-domains) (depends (ocaml (>= 4.12)) - (qcheck-core (>= "0.23")) + (qcheck-core (>= "0.25")) (qcheck-multicoretests-util (= :version)))) (package @@ -57,4 +57,4 @@ multicore programs.") (tags ("test" "property" "qcheck" "quickcheck" "multicore" "non-determinism")) (depends (ocaml (>= 4.12)) - (qcheck-core (>= "0.23")))) + (qcheck-core (>= "0.25")))) diff --git a/lib/util.ml b/lib/util.ml index 33834963..a6c87ba9 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -146,6 +146,16 @@ module Pp = struct fprintf fmt "%s@[<2>%s (@,%a,@ %a,@ %a)@]%s" o name (pp1 false) x (pp2 false) y (pp3 false) z c + let cst4 (pp1 : 'a t) (pp2 : 'b t) (pp3 : 'c t) (pp4 : 'd t) name par fmt x y z w = + let o, c = if par then ("(", ")") else ("", "") in + fprintf fmt "%s@[<2>%s (@,%a,@ %a,@ %a,@ %a)@]%s" o name (pp1 false) x + (pp2 false) y (pp3 false) z (pp4 false) w c + + let cst5 (pp1 : 'a t) (pp2 : 'b t) (pp3 : 'c t) (pp4 : 'd t) (pp5 : 'e t) name par fmt x y z w v = + let o, c = if par then ("(", ")") else ("", "") in + fprintf fmt "%s@[<2>%s (@,%a,@ %a,@ %a,@ %a,@ %a)@]%s" o name (pp1 false) x + (pp2 false) y (pp3 false) z (pp4 false) w (pp5 false) v c + let pp_exn = of_show Printexc.to_string let pp_unit _ fmt () = pp_print_string fmt "()" let pp_bool _ fmt b = fprintf fmt "%B" b diff --git a/lib/util.mli b/lib/util.mli index 96902739..496e454a 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -79,6 +79,16 @@ module Pp : sig [name] with three parameters, using [pp]i to pretty-print its argument [v]i, wrapping itself into parentheses when [par]. *) + val cst4 : 'a t -> 'b t -> 'c t -> 'd t -> string -> bool -> Format.formatter -> 'a -> 'b -> 'c -> 'd -> unit + (** [cst4 pp1 pp2 pp3 pp4 name par v1 v2 v3 v4 fmt] pretty-prints a constructor + [name] with four parameters, using [pp]i to pretty-print its argument + [v]i, wrapping itself into parentheses when [par]. *) + + val cst5 : 'a t -> 'b t -> 'c t -> 'd t -> 'e t -> string -> bool -> Format.formatter -> 'a -> 'b -> 'c -> 'd -> 'e -> unit + (** [cst5 pp1 pp2 pp3 pp4 pp5 name par v1 v2 v3 v4 v5 fmt] pretty-prints a + constructor [name] with five parameters, using [pp]i to pretty-print its + argument [v]i, wrapping itself into parentheses when [par]. *) + val pp_exn : exn t (** Pretty-printer for exceptions reusing the standard {!Printexc.to_string}. The exception message will be wrapped conservatively (ie too often) in diff --git a/multicoretests.opam b/multicoretests.opam index 654f437f..67dc9aa2 100644 --- a/multicoretests.opam +++ b/multicoretests.opam @@ -22,7 +22,7 @@ bug-reports: "https://github.com/ocaml-multicore/multicoretests/issues" depends: [ "dune" {>= "3.0"} "base-domains" - "qcheck-core" {>= "0.23"} + "qcheck-core" {>= "0.25"} "qcheck-lin" {= version} "qcheck-stm" {= version} "odoc" {with-doc} diff --git a/qcheck-lin.opam b/qcheck-lin.opam index b9a75eb6..596a78b0 100644 --- a/qcheck-lin.opam +++ b/qcheck-lin.opam @@ -23,7 +23,7 @@ bug-reports: "https://github.com/ocaml-multicore/multicoretests/issues" depends: [ "dune" {>= "3.0"} "ocaml" {>= "4.12"} - "qcheck-core" {>= "0.23"} + "qcheck-core" {>= "0.25"} "qcheck-multicoretests-util" {= version} "odoc" {with-doc} ] diff --git a/qcheck-multicoretests-util.opam b/qcheck-multicoretests-util.opam index 4a0c9ed2..8a3e5385 100644 --- a/qcheck-multicoretests-util.opam +++ b/qcheck-multicoretests-util.opam @@ -15,7 +15,7 @@ bug-reports: "https://github.com/ocaml-multicore/multicoretests/issues" depends: [ "dune" {>= "3.0"} "ocaml" {>= "4.12"} - "qcheck-core" {>= "0.23"} + "qcheck-core" {>= "0.25"} "odoc" {with-doc} ] build: [ diff --git a/qcheck-stm.opam b/qcheck-stm.opam index 6c9070b2..167f5546 100644 --- a/qcheck-stm.opam +++ b/qcheck-stm.opam @@ -23,7 +23,7 @@ bug-reports: "https://github.com/ocaml-multicore/multicoretests/issues" depends: [ "dune" {>= "3.0"} "ocaml" {>= "4.12"} - "qcheck-core" {>= "0.23"} + "qcheck-core" {>= "0.25"} "qcheck-multicoretests-util" {= version} "odoc" {with-doc} ] diff --git a/src/bytes/stm_tests.ml b/src/bytes/stm_tests.ml index bdd47316..9f081b29 100644 --- a/src/bytes/stm_tests.ml +++ b/src/bytes/stm_tests.ml @@ -9,9 +9,14 @@ struct | Length | Get of int | Set of int * char - | Sub of int * int | Copy + | To_string + | Sub of int * int + | Sub_string of int * int | Fill of int * int * char + | Blit_string of string * int * int * int + | Index of char + | Index_opt of char | To_seq let pp_cmd par fmt x = @@ -20,9 +25,14 @@ struct | Length -> cst0 "Length" fmt | Get x -> cst1 pp_int "Get" par fmt x | Set (x, y) -> cst2 pp_int pp_char "Set" par fmt x y - | Sub (x, y) -> cst2 pp_int pp_int "Sub" par fmt x y | Copy -> cst0 "Copy" fmt + | To_string -> cst0 "To_string" fmt + | Sub (x, y) -> cst2 pp_int pp_int "Sub" par fmt x y + | Sub_string (x, y) -> cst2 pp_int pp_int "Sub_string" par fmt x y | Fill (x, y, z) -> cst3 pp_int pp_int pp_char "Fill" par fmt x y z + | Blit_string (x, y, z, w) -> cst4 pp_string pp_int pp_int pp_int "Blit_string" par fmt x y z w + | Index x -> cst1 pp_char "Index" par fmt x + | Index_opt x -> cst1 pp_char "Index_opt" par fmt x | To_seq -> cst0 "To_seq" fmt let show_cmd = Util.Pp.to_show pp_cmd @@ -30,17 +40,31 @@ struct type state = char list type sut = Bytes.t + let shrink_char c = if c = 'a' then Iter.empty else Iter.return 'a' (* much faster than the default *) + + let shrink_cmd c = match c with + | Blit_string (src,spos,dpos,l) -> + let open Iter in (* shrink spos int before src string *) + (Iter.map (fun spos -> Blit_string (src,spos,dpos,l)) (Shrink.int spos)) + <+> (Iter.map (fun src -> Blit_string (src,spos,dpos,l)) (Shrink.string ~shrink:shrink_char src)) + | _ -> Iter.empty + let arb_cmd s = let int_gen = Gen.(oneof [small_nat; int_bound (List.length s - 1)]) in let char_gen = Gen.printable in - QCheck.make ~print:show_cmd (*~shrink:shrink_cmd*) + QCheck.make ~print:show_cmd ~shrink:shrink_cmd Gen.(oneof [ return Length; map (fun i -> Get i) int_gen; map2 (fun i c -> Set (i,c)) int_gen char_gen; - map2 (fun i len -> Sub (i,len)) int_gen int_gen; (* hack: reusing int_gen for length *) return Copy; + return To_string; + map2 (fun i len -> Sub (i,len)) int_gen int_gen; (* hack: reusing int_gen for length *) + map2 (fun i len -> Sub_string (i,len)) int_gen int_gen; (* hack: reusing int_gen for length *) map3 (fun i len c -> Fill (i,len,c)) int_gen int_gen char_gen; (* hack: reusing int_gen for length*) + map4 (fun src spos dpos l -> Blit_string (src,spos,dpos,l)) string_small int_gen int_gen int_gen; (* hack: reusing int_gen for length*) + map (fun c -> Index c) char_gen; + map (fun c -> Index_opt c) char_gen; return To_seq; ]) @@ -52,12 +76,21 @@ struct | Length -> s | Get _ -> s | Set (i,c) -> List.mapi (fun j c' -> if i = j then c else c') s - | Sub (_,_) -> s | Copy -> s + | To_string -> s + | Sub (_,_) -> s + | Sub_string (_,_) -> s | Fill (i,l,c) -> if i >= 0 && l >= 0 && i+l-1 < (List.length s) then List.mapi (fun j c' -> if i <= j && j <= i+l-1 then c else c') s else s + | Blit_string (src,spos,dpos,l) -> + if spos >= 0 && l >= 0 && spos+l-1 < (String.length src) + && dpos >= 0 && dpos+l-1 < (List.length s) + then List.mapi (fun j c' -> if dpos <= j && j <= dpos+l-1 then src.[spos+j-dpos] else c') s + else s + | Index _ -> s + | Index_opt _ -> s | To_seq -> s let init_sut () = Bytes.make byte_size 'a' @@ -70,9 +103,14 @@ struct | Length -> Res (int, Bytes.length b) | Get i -> Res (result char exn, protect (Bytes.get b) i) | Set (i,c) -> Res (result unit exn, protect (Bytes.set b i) c) - | Sub (i,l) -> Res (result (bytes) exn, protect (Bytes.sub b i) l) | Copy -> Res (bytes, Bytes.copy b) + | To_string -> Res (string, Bytes.to_string b) + | Sub (i,l) -> Res (result bytes exn, protect (Bytes.sub b i) l) + | Sub_string (i,l) -> Res (result string exn, protect (Bytes.sub_string b i) l) | Fill (i,l,c) -> Res (result unit exn, protect (Bytes.fill b i l) c) + | Blit_string (src,spos,dpos,l) -> Res (result unit exn, protect (Bytes.blit_string src spos b dpos) l) + | Index c -> Res (result int exn, protect (Bytes.index b) c) + | Index_opt c -> Res (option int, Bytes.index_opt b c) | To_seq -> Res (seq char, List.to_seq (List.of_seq (Bytes.to_seq b))) let postcond c (s: char list) res = match c, res with @@ -85,15 +123,30 @@ struct if i < 0 || i >= List.length s then r = Error (Invalid_argument "index out of bounds") else r = Ok () + | Copy, Res ((Bytes,_),r) -> r = Bytes.of_seq (List.to_seq s) + | To_string, Res ((String,_),r) -> r = String.of_seq (List.to_seq s) | Sub (i,l), Res ((Result (Bytes,Exn),_), r) -> if i < 0 || l < 0 || i+l > List.length s then r = Error (Invalid_argument "String.sub / Bytes.sub") else r = Ok (Bytes.of_seq (List.to_seq (List.filteri (fun j _ -> i <= j && j <= i+l-1) s))) - | Copy, Res ((Bytes,_),r) -> r = Bytes.of_seq (List.to_seq s) + | Sub_string (i,l), Res ((Result (String,Exn),_), r) -> + if i < 0 || l < 0 || i+l > List.length s + then r = Error (Invalid_argument "String.sub / Bytes.sub") + else r = Ok (String.of_seq (List.to_seq (List.filteri (fun j _ -> i <= j && j <= i+l-1) s))) | Fill (i,l,_), Res ((Result (Unit,Exn),_), r) -> if i < 0 || l < 0 || i+l > List.length s - then r = Error (Invalid_argument "String.fill / Bytes.fill" ) + then r = Error (Invalid_argument "String.fill / Bytes.fill") + else r = Ok () + | Blit_string (src,spos,dpos,l), Res ((Result (Unit,Exn),_), r) -> + if spos < 0 || dpos < 0 || l < 0 || spos+l > String.length src || dpos+l > List.length s + then r = Error (Invalid_argument "String.blit / Bytes.blit_string") else r = Ok () + | Index c, Res ((Result (Int,Exn),_), r) -> + (match List.find_index (fun c' -> c' = c) s with + | Some i -> r = Ok i + | None -> r = Error Not_found) + | Index_opt c, Res ((Option Int,_), r) -> + r = List.find_index (fun c' -> c' = c) s | To_seq, Res ((Seq Char,_),r) -> Seq.equal (=) r (List.to_seq s) | _, _ -> false end