Introduce SpecExt to allow wrapping tests with handlers

Author: polytypic

lib/STM.ml

@@ -108,6 +108,19 @@ sig
       Note: [s] is in this case the model's state prior to command execution. *)
 end
 
+module type SpecExt =
+sig
+  include Spec
+
+  val wrap : (unit -> 'a) -> 'a
+end
+
+module SpecDefaults =
+struct
+  let cleanup = ignore
+  let precond _ _ = true
+  let wrap th = th ()
+end
 
 module Internal =
 struct

lib/STM.mli

@@ -126,6 +126,18 @@ sig
       This is helpful to model, e.g., a [remove] [cmd] that returns the removed element. *)
 end
 
+module type SpecExt =
+sig
+  include Spec
+
+  val wrap : (unit -> 'a) -> 'a
+end
+
+module SpecDefaults : sig
+  val cleanup : 'sut -> unit
+  val precond : 'cmd -> 'state -> bool
+  val wrap : (unit -> 'a) -> 'a
+end
 
 module Internal : sig
 open QCheck

lib/STM_domain.ml

@@ -1,6 +1,6 @@
 open STM
 
-module Make (Spec: Spec) = struct
+module MakeExt (Spec: SpecExt) = struct
 
   open Util
   open QCheck
@@ -24,9 +24,9 @@ module Make (Spec: Spec) = struct
 
   let run_par seq_pref cmds1 cmds2 =
     let sut = Spec.init_sut () in
-    let pref_obs = interp_sut_res sut seq_pref in
+    let pref_obs = Spec.wrap @@ fun () -> interp_sut_res sut seq_pref in
     let barrier = Atomic.make 2 in
-    let main cmds () =
+    let main cmds () = Spec.wrap @@ fun () ->
       Atomic.decr barrier;
       while Atomic.get barrier <> 0 do Domain.cpu_relax() done;
       try Ok (interp_sut_res sut cmds) with exn -> Error exn
@@ -125,3 +125,9 @@ module Make (Spec: Spec) = struct
          assume (all_interleavings_ok triple);
          repeat rep_count agree_prop_par_asym triple) (* 25 times each, then 25 * 10 times when shrinking *)
 end
+
+module Make (Spec: Spec) =
+  MakeExt (struct
+    include SpecDefaults
+    include Spec
+  end)

lib/STM_domain.mli

@@ -96,3 +96,6 @@ module Make : functor (Spec : STM.Spec) ->
         interleaving search like {!agree_test_par} and {!neg_agree_test_par}. *)
 
  end
+
+module MakeExt : functor (Spec : STM.SpecExt) ->
+  module type of Make (Spec)

lib/STM_sequential.ml

@@ -1,6 +1,6 @@
 open STM
 
-module Make (Spec: Spec) = struct
+module MakeExt (Spec: SpecExt) = struct
 
   open QCheck
   open Internal.Make(Spec)
@@ -18,7 +18,7 @@ module Make (Spec: Spec) = struct
   let agree_prop cs =
     assume (cmds_ok Spec.init_state cs);
     let sut = Spec.init_sut () in (* reset system's state *)
-    let res = try Ok (check_disagree Spec.init_state sut cs) with exn -> Error exn in
+    let res = try Ok (Spec.wrap @@ fun () -> check_disagree Spec.init_state sut cs) with exn -> Error exn in
     let ()  = Spec.cleanup sut in
     let res = match res with Ok res -> res | Error exn -> raise exn in
     match res with
@@ -34,3 +34,9 @@ module Make (Spec: Spec) = struct
     Test.make_neg ~name ~count (arb_cmds Spec.init_state) agree_prop
 
   end
+
+module Make (Spec : Spec) =
+  MakeExt (struct
+    include SpecDefaults
+    include Spec
+  end)

lib/STM_sequential.mli

@@ -25,3 +25,6 @@ module Make : functor (Spec : STM.Spec) ->
     (** A negative agreement test (for convenience). Accepts two labeled parameters:
         [count] is the test count and [name] is the printed test name. *)
   end
+
+module MakeExt : functor (Spec : STM.SpecExt) ->
+  module type of Make (Spec)