Skip to content

Commit f49c336

Browse files
jmidjmid
authored
Merge pull request #149 from shym/multiple-ts-fix
Multiple ts fix
2 parents fffc73e + bb5be6d commit f49c336

File tree

12 files changed

+202
-25
lines changed

12 files changed

+202
-25
lines changed

‎lib/lin.ml‎

Lines changed: 48 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -24,10 +24,15 @@ end
2424
module Env : sig
2525
type t = Var.t list
2626
val gen_t_var : t -> Var.t Gen.t
27+
val valid_t_vars : t -> Var.t -> Var.t Iter.t
2728
end =
2829
struct
2930
type t = Var.t list
3031
let gen_t_var env = Gen.oneofl env
32+
let valid_t_vars env v =
33+
match List.filter (fun v' -> v' <= v) env with
34+
| v' :: _ when v' = v -> Iter.return v
35+
| env' -> Iter.of_list env'
3136
end
3237

3338
module type CmdSpec = sig
@@ -49,6 +54,15 @@ module type CmdSpec = sig
4954
(** A command shrinker.
5055
To a first approximation you can use [Shrink.nil]. *)
5156

57+
val fix_cmd : Env.t -> cmd -> cmd Iter.t
58+
(** A command fixer.
59+
Fixes the given [cmd] so that it uses only states in the given
60+
[Env.t]. If the initial [cmd] used a state that is no longer
61+
available, it should iterate over all the lesser states
62+
available in [Env.t]. If all the necessary states are still
63+
available, it should generate a one-element iterator.
64+
Can assume that [Env.t] is sorted in decreasing order. *)
65+
5266
type res
5367
(** The command result type *)
5468

@@ -110,20 +124,47 @@ module MakeDomThr(Spec : CmdSpec)
110124

111125
let shrink_cmd (opt,c) = Iter.map (fun c -> opt,c) (Spec.shrink_cmd c)
112126

127+
(* Note: the [env] fed to [Spec.fix_cmd] are in reverse (ie should
128+
be _decreasing_) order *)
129+
let fix_cmds env cmds =
130+
let rec aux env cmds =
131+
match cmds with
132+
| [] -> Iter.return []
133+
| (opt,cmd) :: cmds ->
134+
let env' = Option.fold ~none:env ~some:(fun i -> i::env) opt in
135+
Iter.map2 (fun cmd cmds -> (opt,cmd)::cmds) (Spec.fix_cmd env cmd) (aux env' cmds)
136+
in aux env cmds
137+
138+
(* Note that the result is built in reverse (ie should be
139+
_decreasing_) order *)
140+
let rec extract_env env cmds =
141+
match cmds with
142+
| [] -> env
143+
| (Some i, _) :: cmds -> extract_env (i::env) cmds
144+
| (None, _) :: cmds -> extract_env env cmds
145+
113146
let shrink_triple' (seq,p1,p2) =
114147
let open Iter in
115148
(* Shrinking heuristic:
116149
First reduce the cmd list sizes as much as possible, since the interleaving
117150
is most costly over long cmd lists. *)
118-
(map (fun seq' -> (seq',p1,p2)) (Shrink.list_spine seq))
151+
let concat_map f it = flatten (map f it) in
152+
let fix_seq seq =
153+
let seq_env = extract_env [0] seq in
154+
let triple seq p1 p2 = (seq,p1,p2) in
155+
map triple (fix_cmds [0] seq) <*> fix_cmds seq_env p1 <*> fix_cmds seq_env p2
156+
in
157+
let seq_env = extract_env [0] seq in
158+
159+
concat_map fix_seq (Shrink.list_spine seq)
119160
<+>
120161
(match p1 with [] -> Iter.empty | c1::c1s -> Iter.return (seq@[c1],c1s,p2))
121162
<+>
122163
(match p2 with [] -> Iter.empty | c2::c2s -> Iter.return (seq@[c2],p1,c2s))
123164
<+>
124-
(map (fun p1' -> (seq,p1',p2)) (Shrink.list_spine p1))
165+
concat_map (fun p1 -> Iter.map (fun p1 -> (seq,p1,p2)) (fix_cmds seq_env p1)) (Shrink.list_spine p1)
125166
<+>
126-
(map (fun p2' -> (seq,p1,p2')) (Shrink.list_spine p2))
167+
concat_map (fun p2 -> Iter.map (fun p2 -> (seq,p1,p2)) (fix_cmds seq_env p2)) (Shrink.list_spine p2)
127168
<+>
128169
(* Secondly reduce the cmd data of individual list elements *)
129170
(map (fun seq' -> (seq',p1,p2)) (Shrink.list_elems shrink_cmd seq))
@@ -296,6 +337,10 @@ module Make(Spec : CmdSpec)
296337
[(3,Gen.return (None,SchedYield));
297338
(5,Gen.map (fun (opt,c) -> (opt,UserCmd c)) (Spec.gen_cmd env))])
298339

340+
let fix_cmd env = function
341+
| SchedYield -> Iter.return SchedYield
342+
| UserCmd cmd -> Iter.map (fun c -> UserCmd c) (Spec.fix_cmd env cmd)
343+
299344
let shrink_cmd c = match c with
300345
| SchedYield -> Iter.empty
301346
| UserCmd c -> Iter.map (fun c' -> UserCmd c') (Spec.shrink_cmd c)

‎lib/lin_api.ml‎

Lines changed: 26 additions & 18 deletions
Original file line numberDiff line numberDiff line change
@@ -60,6 +60,14 @@ let array : type a c s. (a, c, s, combinable) ty -> (a array, c, s, combinable)
6060
| GenDeconstr (arb, print, eq) -> GenDeconstr (QCheck.array arb, QCheck.Print.array print, Array.for_all2 eq)
6161
| Deconstr (print, eq) -> Deconstr (QCheck.Print.array print, Array.for_all2 eq)
6262

63+
let bounded_array : type a c s. int -> (a, c, s, combinable) ty -> (a array, c, s, combinable) ty =
64+
fun maxsize ty ->
65+
let array = QCheck.array_of_size (QCheck.Gen.int_bound maxsize) in
66+
match ty with
67+
| Gen (arb, print) -> Gen (array arb, QCheck.Print.array print)
68+
| GenDeconstr (arb, print, eq) -> GenDeconstr (array arb, QCheck.Print.array print, Array.for_all2 eq)
69+
| Deconstr (print, eq) -> Deconstr (QCheck.Print.array print, Array.for_all2 eq)
70+
6371
let print_seq pp s =
6472
let b = Buffer.create 25 in
6573
Buffer.add_char b '<';
@@ -269,6 +277,19 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
269277

270278
let show_cmd (Cmd (_,args,_,print,_,_)) = print args
271279

280+
let rec fix_args
281+
: type a r. Lin.Env.t -> (a, r) Args.args -> (a, r) Args.args QCheck.Iter.t =
282+
fun env args ->
283+
let open QCheck in
284+
let fn_state i args = Args.FnState (i,args) in
285+
match args with
286+
| FnState (i, args) -> Iter.(map fn_state (Lin.Env.valid_t_vars env i) <*> fix_args env args)
287+
| Fn (x, args) -> Iter.map (fun args -> Args.Fn (x, args)) (fix_args env args)
288+
| _ -> Iter.return args
289+
290+
let fix_cmd env (Cmd (name,args,rty,print,shrink,f)) =
291+
QCheck.Iter.map (fun args -> Cmd (name,args,rty,print,shrink,f)) (fix_args env args)
292+
272293
let shrink_cmd (Cmd (name,args,rty,print,shrink,f)) =
273294
QCheck.Iter.map (fun args -> Cmd (name,args,rty,print,shrink,f)) (shrink args)
274295

@@ -287,18 +308,9 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
287308
let rec apply_f
288309
: type a r. a -> (a, r) Args.args -> t array -> Lin.Var.t option -> r = fun f args state opt_target ->
289310
match args with
290-
| Ret _ ->
291-
(* This happens only if there was a non-function value in the API,
292-
which I'm not sure makes sense *)
293-
raise (Invalid_argument "apply_f")
294-
| Ret_or_exc _ ->
295-
(* This happens only if there was a non-function value in the API,
296-
which I'm not sure makes sense *)
297-
raise (Invalid_argument "apply_f")
298-
| Ret_ignore _ ->
299-
(* This happens only if there was a non-function value in the API,
300-
which I'm not sure makes sense *)
301-
raise (Invalid_argument "apply_f")
311+
| Ret _
312+
| Ret_or_exc _
313+
| Ret_ignore _
302314
| Ret_ignore_or_exc _ ->
303315
(* This happens only if there was a non-function value in the API,
304316
which I'm not sure makes sense *)
@@ -326,9 +338,7 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
326338
try Ok (ignore @@ f state.(index))
327339
with e -> Error e
328340
end)
329-
| FnState (index, (Fn _ as rem)) ->
330-
apply_f (f state.(index)) rem state opt_target
331-
| FnState (index, (FnState _ as rem)) ->
341+
| FnState (index, rem) ->
332342
apply_f (f state.(index)) rem state opt_target
333343
| Fn (arg, Ret _) ->
334344
f arg
@@ -344,9 +354,7 @@ module MakeCmd (ApiSpec : ApiSpec) : Lin.CmdSpec = struct
344354
try Ok (ignore @@ f arg)
345355
with e -> Error e
346356
end
347-
| Fn (arg, (Fn _ as rem)) ->
348-
apply_f (f arg) rem state opt_target
349-
| Fn (arg, (FnState _ as rem)) ->
357+
| Fn (arg, rem) ->
350358
apply_f (f arg) rem state opt_target
351359

352360
let run (opt_target,cmd) state =

‎lib/lin_api.mli‎

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -45,6 +45,7 @@ val opt :
4545
('a, 'b, 'c, combinable) ty -> ('a option, 'b, 'c, combinable) ty
4646
val list : ('a, 'c, 's, combinable) ty -> ('a list, 'c, 's, combinable) ty
4747
val array : ('a, 'c, 's, combinable) ty -> ('a array, 'c, 's, combinable) ty (* FIXME: shouldn't be deconstructible? *)
48+
val bounded_array : int -> ('a, 'c, 's, combinable) ty -> ('a array, 'c, 's, combinable) ty
4849
val seq : ('a, 'c, 's, combinable) ty -> ('a Seq.t, 'c, 's, combinable) ty
4950

5051
val state : ('a, constructible, 'a, noncombinable) ty

‎src/array/lin_tests.ml‎

Lines changed: 13 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -58,6 +58,19 @@ struct
5858
| Sort v -> Iter.map (fun v -> Sort v) (Var.shrink v)
5959
| To_seq v -> Iter.map (fun v -> To_seq v) (Var.shrink v)
6060

61+
let fix_cmd env = function
62+
| Length i -> Iter.map (fun i -> Length i ) (Env.valid_t_vars env i)
63+
| Get (i,x) -> Iter.map (fun i -> Get (i,x) ) (Env.valid_t_vars env i)
64+
| Set (i,x,z) -> Iter.map (fun i -> Set (i,x,z) ) (Env.valid_t_vars env i)
65+
| Sub (i,x,y) -> Iter.map (fun i -> Sub (i,x,y) ) (Env.valid_t_vars env i)
66+
| Copy i -> Iter.map (fun i -> Copy i ) (Env.valid_t_vars env i)
67+
| Fill (i,x,y,z) -> Iter.map (fun i -> Fill (i,x,y,z)) (Env.valid_t_vars env i)
68+
| To_list i -> Iter.map (fun i -> To_list i ) (Env.valid_t_vars env i)
69+
| Mem (i,z) -> Iter.map (fun i -> Mem (i,z) ) (Env.valid_t_vars env i)
70+
| Sort i -> Iter.map (fun i -> Sort i ) (Env.valid_t_vars env i)
71+
| To_seq i -> Iter.map (fun i -> To_seq i ) (Env.valid_t_vars env i)
72+
| Append (i,j) -> Iter.(map (fun i j -> Append (i,j)) (Env.valid_t_vars env i) <*> (Env.valid_t_vars env j))
73+
6174
open Util
6275
(*let pp_exn = Util.pp_exn*)
6376
let pp fmt t = Format.fprintf fmt "%s" (QCheck.Print.(array char) t)

‎src/atomic/lin_tests.ml‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -32,6 +32,16 @@ struct
3232

3333
let shrink_cmd = Shrink.nil
3434

35+
let fix_cmd env = function
36+
| Make x as cmd -> Iter.return cmd
37+
| Get i -> Iter.map (fun i -> Get i ) (Env.valid_t_vars env i)
38+
| Set (i,x) -> Iter.map (fun i -> Set (i,x) ) (Env.valid_t_vars env i)
39+
| Exchange (i,x) -> Iter.map (fun i -> Exchange (i,x) ) (Env.valid_t_vars env i)
40+
| Compare_and_set (i,x,y) -> Iter.map (fun i -> Compare_and_set (i,x,y)) (Env.valid_t_vars env i)
41+
| Fetch_and_add (i,x) -> Iter.map (fun i -> Fetch_and_add (i,x) ) (Env.valid_t_vars env i)
42+
| Incr i -> Iter.map (fun i -> Incr i ) (Env.valid_t_vars env i)
43+
| Decr i -> Iter.map (fun i -> Decr i ) (Env.valid_t_vars env i)
44+
3545
type res =
3646
| RMake of unit
3747
| RGet of int

‎src/bigarray/lin_tests_dsl.ml‎

Lines changed: 40 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -2,26 +2,62 @@
22
(* Tests of thread-unsafe [Bigarray.Array1] of ints *)
33
(* ********************************************************************** *)
44

5+
(* Bigarray.Array1 API:
6+
7+
val create : ('a, 'b) Bigarray.kind -> 'c Bigarray.layout -> int -> ('a, 'b, 'c) t
8+
val init : ('a, 'b) Bigarray.kind -> 'c Bigarray.layout -> int -> (int -> 'a) -> ('a, 'b, 'c) t
9+
external dim : ('a, 'b, 'c) t -> int
10+
external kind : ('a, 'b, 'c) t -> ('a, 'b) Bigarray.kind
11+
external layout : ('a, 'b, 'c) t -> 'c Bigarray.layout
12+
val change_layout : ('a, 'b, 'c) t -> 'd Bigarray.layout -> ('a, 'b, 'd) t
13+
val size_in_bytes : ('a, 'b, 'c) t -> int
14+
external get : ('a, 'b, 'c) t -> int -> 'a
15+
external set : ('a, 'b, 'c) t -> int -> 'a -> unit
16+
external sub : ('a, 'b, 'c) t -> int -> int -> ('a, 'b, 'c) t
17+
val slice : ('a, 'b, 'c) t -> int -> ('a, 'b, 'c) Bigarray.Array0.t
18+
external blit : ('a, 'b, 'c) t -> ('a, 'b, 'c) t -> unit
19+
external fill : ('a, 'b, 'c) t -> 'a -> unit
20+
val of_array : ('a, 'b) Bigarray.kind -> 'c Bigarray.layout -> 'a array -> ('a, 'b, 'c) t
21+
external unsafe_get : ('a, 'b, 'c) t -> int -> 'a
22+
external unsafe_set : ('a, 'b, 'c) t -> int -> 'a -> unit
23+
*)
24+
525
module BA1Conf =
626
struct
727
open Bigarray
828
type t = (int, int_elt, c_layout) Array1.t
929

10-
let array_size = 16
11-
let init () =
12-
let arr = Array1.create int C_layout array_size in
30+
let array_create sz =
31+
let arr = Array1.create int C_layout sz in
1332
Array1.fill arr 0 ;
1433
arr
34+
let of_array = Array1.of_array int C_layout
35+
let dummy_change_layout arr = Array1.change_layout arr C_layout
36+
37+
let array_size = 16
38+
let init () = array_create array_size
1539
let cleanup _ = ()
1640

1741
open Lin_api
1842
let int = int_small
1943

2044
let api =
21-
[ val_ "Bigarray.Array1.size_in_bytes" Array1.size_in_bytes (t @-> returning int);
45+
[ val_ "Bigarray.Array1.create" array_create (int @-> returning_ t);
46+
(* [Array1.init] requires a function *)
47+
val_ "Bigarray.Array1.dim" Array1.dim (t @-> returning int);
48+
(* [Array1.kind] returns an untestable value *)
49+
(* [change_layout]: the layout is fixed in our sut, so we test a dummy version *)
50+
val_ "Bigarray.Array1.change_layout" dummy_change_layout (t @-> returning_ t);
51+
val_ "Bigarray.Array1.size_in_bytes" Array1.size_in_bytes (t @-> returning int);
2252
val_ "Bigarray.Array1.get" Array1.get (t @-> int @-> returning_or_exc int);
2353
val_ "Bigarray.Array1.set" Array1.set (t @-> int @-> int @-> returning_or_exc unit);
54+
val_ "Bigarray.Array1.sub" Array1.sub (t @-> int @-> int @-> returning_or_exc_ t);
55+
(* [Array1.slice]: cannot be tested since it produces a Bigarray.Array0.t *)
56+
val_ "Bigarray.Array1.blit" Array1.blit (t @-> t @-> returning unit);
2457
val_ "Bigarray.Array1.fill" Array1.fill (t @-> int @-> returning unit);
58+
val_ "Bigarray.Array1.of_array" of_array (bounded_array 100 int @-> returning_ t);
59+
(* [Array1.unsafe_get] and [Array1.unsafe_set] cannot be tested:
60+
they can segfault or produce any useless result *)
2561
]
2662
end
2763

‎src/hashtbl/lin_tests.ml‎

Lines changed: 12 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -53,6 +53,18 @@ struct
5353
| Mem (v,c) -> Iter.map (fun c -> Mem (v,c)) (Shrink.char c)
5454
| Length _ -> Iter.empty
5555

56+
let fix_cmd env = function
57+
| Clear i -> Iter.map (fun i -> Clear i ) (Env.valid_t_vars env i)
58+
| Copy i -> Iter.map (fun i -> Copy i ) (Env.valid_t_vars env i)
59+
| Add (i,x,y) -> Iter.map (fun i -> Add (i,x,y) ) (Env.valid_t_vars env i)
60+
| Remove (i,x) -> Iter.map (fun i -> Remove (i,x) ) (Env.valid_t_vars env i)
61+
| Find (i,x) -> Iter.map (fun i -> Find (i,x) ) (Env.valid_t_vars env i)
62+
| Find_opt (i,x) -> Iter.map (fun i -> Find_opt (i,x) ) (Env.valid_t_vars env i)
63+
| Find_all (i,x) -> Iter.map (fun i -> Find_all (i,x) ) (Env.valid_t_vars env i)
64+
| Replace (i,x,y) -> Iter.map (fun i -> Replace (i,x,y)) (Env.valid_t_vars env i)
65+
| Mem (i,x) -> Iter.map (fun i -> Mem (i,x) ) (Env.valid_t_vars env i)
66+
| Length i -> Iter.map (fun i -> Length i ) (Env.valid_t_vars env i)
67+
5668
type res =
5769
| RClear
5870
| RCopy

‎src/internal/cleanup.ml‎

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,11 @@ struct
2424

2525
let shrink_cmd = Shrink.nil
2626

27+
let fix_cmd env = function
28+
| Get i -> Iter.map (fun i -> Get i ) (Lin.Env.valid_states env i)
29+
| Set (i,x) -> Iter.map (fun i -> Set (i,x)) (Lin.Env.valid_states env i)
30+
| Add (i,x) -> Iter.map (fun i -> Add (i,x)) (Lin.Env.valid_states env i)
31+
2732
let init () = (ref Inited, ref 0)
2833

2934
let cleanup (status,_) =

‎src/lazy/lin_tests.ml‎

Lines changed: 7 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -62,6 +62,13 @@ struct
6262
(* the Lazy tests already take a while to run - so better avoid spending extra time shrinking *)
6363
let shrink_cmd = Shrink.nil
6464

65+
let fix_cmd env = function
66+
| Force i -> Iter.map (fun i -> Force i ) (Env.valid_t_vars env i)
67+
| Force_val i -> Iter.map (fun i -> Force_val i ) (Env.valid_t_vars env i)
68+
| Is_val i -> Iter.map (fun i -> Is_val i ) (Env.valid_t_vars env i)
69+
| Map (i,f) -> Iter.map (fun i -> Map (i,f) ) (Env.valid_t_vars env i)
70+
| Map_val (i,f) -> Iter.map (fun i -> Map_val (i,f)) (Env.valid_t_vars env i)
71+
6572
type t = int Lazy.t
6673

6774
let cleanup _ = ()

‎src/neg_tests/lin_tests_common.ml‎

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -52,6 +52,13 @@ module RConf_int = struct
5252
| Set (t,i) -> Iter.map (fun i -> Set (t,i)) (Shrink.int i)
5353
| Add (t,i) -> Iter.map (fun i -> Add (t,i)) (Shrink.int i)
5454

55+
let fix_cmd env = function
56+
| Get i -> Iter.map (fun i -> Get i ) (Env.valid_t_vars env i)
57+
| Set (i,x) -> Iter.map (fun i -> Set (i,x)) (Env.valid_t_vars env i)
58+
| Add (i,x) -> Iter.map (fun i -> Add (i,x)) (Env.valid_t_vars env i)
59+
| Incr i -> Iter.map (fun i -> Incr i ) (Env.valid_t_vars env i)
60+
| Decr i -> Iter.map (fun i -> Decr i ) (Env.valid_t_vars env i)
61+
5562
type res = RGet of int | RSet | RAdd | RIncr | RDecr [@@deriving show { with_path = false }, eq]
5663

5764
let init () = Sut_int.init ()
@@ -97,6 +104,13 @@ module RConf_int64 = struct
97104
| Set (t,i) -> Iter.map (fun i -> Set (t,i)) (Shrink.int64 i)
98105
| Add (t,i) -> Iter.map (fun i -> Add (t,i)) (Shrink.int64 i)
99106

107+
let fix_cmd env = function
108+
| Get i -> Iter.map (fun i -> Get i ) (Env.valid_t_vars env i)
109+
| Set (i,x) -> Iter.map (fun i -> Set (i,x)) (Env.valid_t_vars env i)
110+
| Add (i,x) -> Iter.map (fun i -> Add (i,x)) (Env.valid_t_vars env i)
111+
| Incr i -> Iter.map (fun i -> Incr i ) (Env.valid_t_vars env i)
112+
| Decr i -> Iter.map (fun i -> Decr i ) (Env.valid_t_vars env i)
113+
100114
type res = RGet of int64 | RSet | RAdd | RIncr | RDecr [@@deriving show { with_path = false }, eq]
101115

102116
let init () = Sut_int64.init ()
@@ -146,6 +160,10 @@ struct
146160
| Add_node (t,i) -> Iter.map (fun i -> Add_node (t,i)) (T.shrink i)
147161
| Member (t,i) -> Iter.map (fun i -> Member (t,i)) (T.shrink i)
148162

163+
let fix_cmd env = function
164+
| Add_node (i,x) -> Iter.map (fun i -> Add_node (i,x)) (Lin.Env.valid_t_vars env i)
165+
| Member (i,x) -> Iter.map (fun i -> Member (i,x) ) (Lin.Env.valid_t_vars env i)
166+
149167
type res = RAdd_node of bool | RMember of bool [@@deriving show { with_path = false }, eq]
150168

151169
let init () = CList.list_init T.zero

0 commit comments

Comments
 (0)