forked from ocaml-multicore/multicoretests
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathstm_tests.ml
96 lines (84 loc) · 3.32 KB
/
stm_tests.ml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
open QCheck
open STM
(** parallel STM tests of Bytes *)
module ByConf =
struct
type cmd =
| Length
| Get of int
| Set of int * char
| Sub of int * int
| Copy
| Fill of int * int * char
| To_seq
[@@deriving show { with_path = false }]
type state = char list
type sut = Bytes.t
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*)
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;
map3 (fun i len c -> Fill (i,len,c)) int_gen int_gen char_gen; (* hack: reusing int_gen for length*)
return To_seq;
])
let byte_size = 16
let init_state = List.init byte_size (fun _ -> 'a')
let next_state c s = match c with
| Length -> s
| Get _ -> s
| Set (i,c) -> List.mapi (fun j c' -> if i = j then c else c') s
| Sub (_,_) -> s
| Copy -> 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
| To_seq -> s
let init_sut () = Bytes.make byte_size 'a'
let cleanup _ = ()
let precond c _s = match c with
| _ -> true
let run c b = match c with
| 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)
| Fill (i,l,c) -> Res (result unit exn, protect (Bytes.fill b i l) 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
| Length, Res ((Int,_),i) -> i = List.length s
| Get i, Res ((Result (Char,Exn),_), r) ->
if i < 0 || i >= List.length s
then r = Error (Invalid_argument "index out of bounds")
else r = Ok (List.nth s i)
| Set (i,_), Res ((Result (Unit,Exn),_), r) ->
if i < 0 || i >= List.length s
then r = Error (Invalid_argument "index out of bounds")
else r = Ok ()
| 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)
| 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" )
else r = Ok ()
| To_seq, Res ((Seq Char,_),r) -> Seq.equal (=) r (List.to_seq s)
| _, _ -> false
end
module BytesSTM_seq = STM_sequential.Make(ByConf)
module BytesSTM_dom = STM_domain.Make(ByConf)
;;
QCheck_base_runner.run_tests_main
(let count = 1000 in
[BytesSTM_seq.agree_test ~count ~name:"STM Bytes test sequential";
BytesSTM_dom.neg_agree_test_par ~count ~name:"STM Bytes test parallel"
])