Skip to content

Commit b9e806b

Browse files
jmidjmid
authored
Merge pull request #210 from jmid/inline-stm-modules
Inline STM modules
2 parents b9866dd + f1a3858 commit b9e806b

File tree

12 files changed

+377
-370
lines changed

12 files changed

+377
-370
lines changed

‎lib/STM_base.ml‎

Lines changed: 299 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,302 @@
11
(** Base module for specifying STM tests *)
22

3-
module STM_internal = STM_internal
4-
module STM_spec = STM_spec
5-
include STM_spec
3+
open QCheck
4+
5+
type 'a ty = ..
6+
7+
type _ ty +=
8+
| Unit : unit ty
9+
| Bool : bool ty
10+
| Char : char ty
11+
| Int : int ty
12+
| Int32 : int32 ty
13+
| Int64 : int64 ty
14+
| Float : float ty
15+
| String : string ty
16+
| Bytes : bytes ty
17+
| Exn : exn ty
18+
| Option : 'a ty -> 'a option ty
19+
| Result : 'a ty * 'b ty -> ('a, 'b) result ty
20+
| List : 'a ty -> 'a list ty
21+
| Array : 'a ty -> 'a array ty
22+
| Seq : 'a ty -> 'a Seq.t ty
23+
24+
type 'a ty_show = 'a ty * ('a -> string)
25+
26+
let unit = (Unit, fun () -> "()")
27+
let bool = (Bool, string_of_bool)
28+
let char = (Char, fun c -> Printf.sprintf "%C" c)
29+
let int = (Int, string_of_int)
30+
let int32 = (Int32, Int32.to_string)
31+
let int64 = (Int64, Int64.to_string)
32+
let float = (Float, Float.to_string)
33+
let string = (String, QCheck.Print.string)
34+
let bytes = (Bytes, fun b -> QCheck.Print.string (Bytes.to_string b))
35+
let option spec =
36+
let (ty,show) = spec in
37+
(Option ty, QCheck.Print.option show)
38+
let exn = (Exn, Printexc.to_string)
39+
40+
let show_result show_ok show_err = function
41+
| Ok x -> Printf.sprintf "Ok (%s)" (show_ok x)
42+
| Error y -> Printf.sprintf "Error (%s)" (show_err y)
43+
44+
let result spec_ok spec_err =
45+
let (ty_ok, show_ok) = spec_ok in
46+
let (ty_err, show_err) = spec_err in
47+
(Result (ty_ok, ty_err), show_result show_ok show_err)
48+
let list spec =
49+
let (ty,show) = spec in
50+
(List ty, QCheck.Print.list show)
51+
let array spec =
52+
let (ty,show) = spec in
53+
(Array ty, QCheck.Print.array show)
54+
let seq spec =
55+
let (ty,show) = spec in
56+
(Seq ty, fun s -> QCheck.Print.list show (List.of_seq s))
57+
58+
59+
60+
type res =
61+
Res : 'a ty_show * 'a -> res
62+
63+
let show_res (Res ((_,show), v)) = show v
64+
65+
(** The specification of a state machine. *)
66+
module type STM_spec =
67+
sig
68+
type cmd
69+
(** The type of commands *)
70+
71+
type state
72+
(** The type of the model's state *)
73+
74+
type sut
75+
(** The type of the system under test *)
76+
77+
val arb_cmd : state -> cmd arbitrary
78+
(** A command generator. Accepts a state parameter to enable state-dependent [cmd] generation. *)
79+
80+
val init_state : state
81+
(** The model's initial state. *)
82+
83+
val show_cmd : cmd -> string
84+
(** [show_cmd c] returns a string representing the command [c]. *)
85+
86+
val next_state : cmd -> state -> state
87+
(** Move the internal state machine to the next state. *)
88+
89+
val init_sut : unit -> sut
90+
(** Initialize the system under test. *)
91+
92+
val cleanup : sut -> unit
93+
(** Utility function to clean up the [sut] after each test instance,
94+
e.g., for closing sockets, files, or resetting global parameters*)
95+
96+
val precond : cmd -> state -> bool
97+
(** [precond c s] expresses preconditions for command [c].
98+
This is useful, e.g., to prevent the shrinker from breaking invariants when minimizing
99+
counterexamples. *)
100+
101+
val run : cmd -> sut -> res
102+
(** [run c i] should interpret the command [c] over the system under test (typically side-effecting). *)
103+
104+
val postcond : cmd -> state -> res -> bool
105+
(** [postcond c s res] checks whether [res] arising from interpreting the
106+
command [c] over the system under test with [run] agrees with the
107+
model's result.
108+
Note: [s] is in this case the model's state prior to command execution. *)
109+
end
110+
111+
112+
module STM_internal =
113+
struct
114+
module Make(Spec : STM_spec) = struct
115+
116+
let rec gen_cmds arb s fuel =
117+
Gen.(if fuel = 0
118+
then return []
119+
else
120+
(arb s).gen >>= fun c ->
121+
(gen_cmds arb (Spec.next_state c s) (fuel-1)) >>= fun cs ->
122+
return (c::cs))
123+
(** A fueled command list generator.
124+
Accepts a state parameter to enable state-dependent [cmd] generation. *)
125+
126+
let rec cmds_ok s cs = match cs with
127+
| [] -> true
128+
| c::cs ->
129+
Spec.precond c s &&
130+
let s' = Spec.next_state c s in
131+
cmds_ok s' cs
132+
133+
let arb_cmds s =
134+
let cmds_gen = Gen.sized (gen_cmds Spec.arb_cmd s) in
135+
let shrinker = match (Spec.arb_cmd s).shrink with
136+
| None -> Shrink.list ~shrink:Shrink.nil (* no elem. shrinker provided *)
137+
| Some s -> Shrink.list ~shrink:s in
138+
let ac = QCheck.make ~shrink:(Shrink.filter (cmds_ok Spec.init_state) shrinker) cmds_gen in
139+
(match (Spec.arb_cmd s).print with
140+
| None -> ac
141+
| Some p -> set_print (Print.list p) ac)
142+
143+
let consistency_test ~count ~name =
144+
Test.make ~name ~count (arb_cmds Spec.init_state) (cmds_ok Spec.init_state)
145+
146+
let rec interp_agree s sut cs = match cs with
147+
| [] -> true
148+
| c::cs ->
149+
let res = Spec.run c sut in
150+
let b = Spec.postcond c s res in
151+
let s' = Spec.next_state c s in
152+
b && interp_agree s' sut cs
153+
154+
let rec check_disagree s sut cs = match cs with
155+
| [] -> None
156+
| c::cs ->
157+
let res = Spec.run c sut in
158+
let b = Spec.postcond c s res in
159+
let s' = Spec.next_state c s in
160+
if b
161+
then
162+
match check_disagree s' sut cs with
163+
| None -> None
164+
| Some rest -> Some ((c,res)::rest)
165+
else Some [c,res]
166+
167+
let check_and_next (c,res) s =
168+
let b = Spec.postcond c s res in
169+
let s' = Spec.next_state c s in
170+
b,s'
171+
172+
(* checks that all interleavings of a cmd triple satisfies all preconditions *)
173+
let rec all_interleavings_ok pref cs1 cs2 s =
174+
match pref with
175+
| c::pref' ->
176+
Spec.precond c s &&
177+
let s' = Spec.next_state c s in
178+
all_interleavings_ok pref' cs1 cs2 s'
179+
| [] ->
180+
match cs1,cs2 with
181+
| [],[] -> true
182+
| [],c2::cs2' ->
183+
Spec.precond c2 s &&
184+
let s' = Spec.next_state c2 s in
185+
all_interleavings_ok pref cs1 cs2' s'
186+
| c1::cs1',[] ->
187+
Spec.precond c1 s &&
188+
let s' = Spec.next_state c1 s in
189+
all_interleavings_ok pref cs1' cs2 s'
190+
| c1::cs1',c2::cs2' ->
191+
(Spec.precond c1 s &&
192+
let s' = Spec.next_state c1 s in
193+
all_interleavings_ok pref cs1' cs2 s')
194+
&&
195+
(Spec.precond c2 s &&
196+
let s' = Spec.next_state c2 s in
197+
all_interleavings_ok pref cs1 cs2' s')
198+
199+
let rec check_obs pref cs1 cs2 s =
200+
match pref with
201+
| p::pref' ->
202+
let b,s' = check_and_next p s in
203+
b && check_obs pref' cs1 cs2 s'
204+
| [] ->
205+
match cs1,cs2 with
206+
| [],[] -> true
207+
| [],p2::cs2' ->
208+
let b,s' = check_and_next p2 s in
209+
b && check_obs pref cs1 cs2' s'
210+
| p1::cs1',[] ->
211+
let b,s' = check_and_next p1 s in
212+
b && check_obs pref cs1' cs2 s'
213+
| p1::cs1',p2::cs2' ->
214+
(let b1,s' = check_and_next p1 s in
215+
b1 && check_obs pref cs1' cs2 s')
216+
||
217+
(let b2,s' = check_and_next p2 s in
218+
b2 && check_obs pref cs1 cs2' s')
219+
220+
let gen_cmds_size gen s size_gen = Gen.sized_size size_gen (gen_cmds gen s)
221+
222+
(* Shrinks a single cmd, starting in the given state *)
223+
let shrink_cmd arb cmd state =
224+
Option.value (arb state).shrink ~default:Shrink.nil @@ cmd
225+
226+
(* Shrinks cmd lists, starting in the given state *)
227+
let rec shrink_cmd_list arb cs state = match cs with
228+
| [] -> Iter.empty
229+
| c::cs ->
230+
if Spec.precond c state
231+
then
232+
Iter.(
233+
map (fun c -> c::cs) (shrink_cmd arb c state)
234+
<+>
235+
map (fun cs -> c::cs) (shrink_cmd_list arb cs Spec.(next_state c state))
236+
)
237+
else Iter.empty
238+
239+
(* Shrinks cmd elements in triples *)
240+
let shrink_triple_elems arb0 arb1 arb2 (seq,p1,p2) =
241+
let shrink_prefix cs state =
242+
Iter.map (fun cs -> (cs,p1,p2)) (shrink_cmd_list arb0 cs state)
243+
in
244+
let rec shrink_par_suffix cs state = match cs with
245+
| [] ->
246+
(* try only one option: p1s or p2s first - both valid interleavings *)
247+
Iter.(map (fun p1 -> (seq,p1,p2)) (shrink_cmd_list arb1 p1 state)
248+
<+>
249+
map (fun p2 -> (seq,p1,p2)) (shrink_cmd_list arb2 p2 state))
250+
| c::cs ->
251+
(* walk seq prefix (again) to advance state *)
252+
if Spec.precond c state
253+
then shrink_par_suffix cs Spec.(next_state c state)
254+
else Iter.empty
255+
in
256+
match Spec.(arb_cmd init_state).shrink with
257+
| None -> Iter.empty (* stop early if no cmd shrinker is available *)
258+
| Some _ ->
259+
Iter.(shrink_prefix seq Spec.init_state
260+
<+>
261+
shrink_par_suffix seq Spec.init_state)
262+
263+
(* General shrinker of cmd triples *)
264+
let shrink_triple arb0 arb1 arb2 =
265+
let open Iter in
266+
Shrink.filter
267+
(fun (seq,p1,p2) -> all_interleavings_ok seq p1 p2 Spec.init_state)
268+
(fun ((seq,p1,p2) as triple) ->
269+
(* Shrinking heuristic:
270+
First reduce the cmd list sizes as much as possible, since the interleaving
271+
is most costly over long cmd lists. *)
272+
(map (fun seq' -> (seq',p1,p2)) (Shrink.list_spine seq))
273+
<+>
274+
(match p1 with [] -> Iter.empty | c1::c1s -> Iter.return (seq@[c1],c1s,p2))
275+
<+>
276+
(match p2 with [] -> Iter.empty | c2::c2s -> Iter.return (seq@[c2],p1,c2s))
277+
<+>
278+
(map (fun p1' -> (seq,p1',p2)) (Shrink.list_spine p1))
279+
<+>
280+
(map (fun p2' -> (seq,p1,p2')) (Shrink.list_spine p2))
281+
<+>
282+
(* Secondly reduce the cmd data of individual list elements *)
283+
(shrink_triple_elems arb0 arb1 arb2 triple))
284+
285+
let arb_triple seq_len par_len arb0 arb1 arb2 =
286+
let seq_pref_gen = gen_cmds_size arb0 Spec.init_state (Gen.int_bound seq_len) in
287+
let shrink_triple = shrink_triple arb0 arb1 arb2 in
288+
let gen_triple =
289+
Gen.(seq_pref_gen >>= fun seq_pref ->
290+
int_range 2 (2*par_len) >>= fun dbl_plen ->
291+
let spawn_state = List.fold_left (fun st c -> Spec.next_state c st) Spec.init_state seq_pref in
292+
let par_len1 = dbl_plen/2 in
293+
let par_gen1 = gen_cmds_size arb1 spawn_state (return par_len1) in
294+
let par_gen2 = gen_cmds_size arb2 spawn_state (return (dbl_plen - par_len1)) in
295+
triple (return seq_pref) par_gen1 par_gen2) in
296+
make ~print:(Util.print_triple_vertical Spec.show_cmd) ~shrink:shrink_triple gen_triple
297+
298+
let arb_cmds_par seq_len par_len = arb_triple seq_len par_len Spec.arb_cmd Spec.arb_cmd Spec.arb_cmd
299+
end
300+
end
301+
6302
include Util

‎lib/STM_spec.mli‎ renamed to ‎lib/STM_base.mli‎

Lines changed: 69 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -74,8 +74,9 @@ type res =
7474

7575
val show_res : res -> string
7676

77+
7778
(** The specification of a state machine. *)
78-
module type Spec =
79+
module type STM_spec =
7980
sig
8081
type cmd
8182
(** The type of commands *)
@@ -124,3 +125,70 @@ sig
124125
{b Note:} the state parameter [s] is the model's {!state} before executing the command [c] (the "old/pre" state).
125126
This is helpful to model, e.g., a [remove] [cmd] that returns the removed element. *)
126127
end
128+
129+
130+
module STM_internal : sig
131+
open QCheck
132+
(** Internal helper module to build STM tests. *)
133+
134+
135+
(** Derives a test framework from a state machine specification. *)
136+
module Make (Spec : STM_spec) :
137+
sig
138+
(** {3 The resulting test framework derived from a state machine specification} *)
139+
140+
val cmds_ok : Spec.state -> Spec.cmd list -> bool
141+
(** A precondition checker (stops early, thanks to short-circuit Boolean evaluation).
142+
Accepts the initial state and the command sequence as parameters. *)
143+
144+
val arb_cmds : Spec.state -> Spec.cmd list arbitrary
145+
(** A generator of command sequences. Accepts the initial state as parameter. *)
146+
147+
val consistency_test : count:int -> name:string -> QCheck.Test.t
148+
(** A consistency test that generates a number of [cmd] sequences and
149+
checks that all contained [cmd]s satisfy the precondition [precond].
150+
Accepts two labeled parameters:
151+
[count] is the test count and [name] is the printed test name. *)
152+
153+
val interp_agree : Spec.state -> Spec.sut -> Spec.cmd list -> bool
154+
(** Checks agreement between the model and the system under test
155+
(stops early, thanks to short-circuit Boolean evaluation). *)
156+
157+
val check_disagree : Spec.state -> Spec.sut -> Spec.cmd list -> (Spec.cmd * res) list option
158+
(** [check_disagree state sut pg] checks that none of the commands present
159+
in [pg] violated the declared postconditions when [pg] is run in [state].
160+
Return [None] if none of the commands violate its postcondition, and
161+
[Some] list corresponding to the prefix of [pg] ending with the [cmd]
162+
violating its postcondition. *)
163+
164+
val check_obs : (Spec.cmd * res) list -> (Spec.cmd * res) list -> (Spec.cmd * res) list -> Spec.state -> bool
165+
(** [check_obs pref cs1 cs2 s] tests whether the observations from the sequential prefix [pref]
166+
and the parallel traces [cs1] [cs2] agree with the model started in state [s]. *)
167+
168+
val gen_cmds_size : (Spec.state -> Spec.cmd arbitrary) -> Spec.state -> int Gen.t -> Spec.cmd list Gen.t
169+
(** [gen_cmds_size arb state gen_int] generates a program of size generated
170+
by [gen_int] using [arb] to generate [cmd]s according to the current
171+
state. [state] is the starting state. *)
172+
173+
val arb_cmds_par : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) arbitrary
174+
(** [arb_cmds_par seq_len par_len] generates a [cmd] triple with at most [seq_len]
175+
sequential commands and at most [par_len] parallel commands each. *)
176+
177+
val all_interleavings_ok : Spec.cmd list -> Spec.cmd list -> Spec.cmd list -> Spec.state -> bool
178+
(** [all_interleavings_ok seq spawn0 spawn1 state] checks that
179+
preconditions of all the [cmd]s of [seq], [spawn0], and [spawn1] are satisfied in all the
180+
possible interleavings and starting with [state] *)
181+
182+
val shrink_triple : (Spec.state -> Spec.cmd arbitrary) -> (Spec.state -> Spec.cmd arbitrary) -> (Spec.state -> Spec.cmd arbitrary) -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) Shrink.t
183+
(** [shrink_triple arb0 arb1 arb2] is a [Shrinker.t] for programs (triple of list of [cmd]s) that is specialized for each part of the program. *)
184+
185+
val arb_triple : int -> int -> (Spec.state -> Spec.cmd arbitrary) -> (Spec.state -> Spec.cmd arbitrary) -> (Spec.state -> Spec.cmd arbitrary) -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) arbitrary
186+
(** [arb_triple seq_len par_len arb0 arb1 arb2] generates a [cmd] triple with at most [seq_len]
187+
sequential commands and at most [par_len] parallel commands each.
188+
The three [cmd] components are generated with [arb0], [arb1], and [arb2], respectively.
189+
Each of these take the model state as a parameter. *)
190+
end
191+
end
192+
193+
val protect : ('a -> 'b) -> 'a -> ('b, exn) result
194+
(** [protect f] turns an [exception] throwing function into a [result] returning function. *)

0 commit comments

Comments
 (0)