Skip to content

Expand on STM Bytes test #547

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 10 commits into from
Apr 8, 2025
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension


Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion .github/workflows/common.yml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
1 change: 1 addition & 0 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down
8 changes: 4 additions & 4 deletions dune-project
Original file line number Diff line number Diff line change
Expand Up @@ -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))))

Expand All @@ -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
Expand All @@ -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
Expand All @@ -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"))))
10 changes: 10 additions & 0 deletions lib/util.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
10 changes: 10 additions & 0 deletions lib/util.mli
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion multicoretests.opam
Original file line number Diff line number Diff line change
Expand Up @@ -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}
Expand Down
2 changes: 1 addition & 1 deletion qcheck-lin.opam
Original file line number Diff line number Diff line change
Expand Up @@ -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}
]
Expand Down
2 changes: 1 addition & 1 deletion qcheck-multicoretests-util.opam
Original file line number Diff line number Diff line change
Expand Up @@ -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: [
Expand Down
2 changes: 1 addition & 1 deletion qcheck-stm.opam
Original file line number Diff line number Diff line change
Expand Up @@ -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}
]
Expand Down
69 changes: 61 additions & 8 deletions src/bytes/stm_tests.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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 =
Expand All @@ -20,27 +25,46 @@ 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

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;
])

Expand All @@ -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'
Expand All @@ -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
Expand All @@ -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
Expand Down