Add an optional argument for protecting the run of the tests

CHANGES.md

@@ -1,5 +1,7 @@
 # Unreleased
 
+- Add the protect-call optional argument
+  [\#205](https://github.com/ocaml-gospel/ortac/pull/205)
 - Add a comment warning that the file is generated
   [\#198](https://github.com/ocaml-gospel/ortac/pull/198)
 - Add an include option to qcheck-stm cli

plugins/qcheck-stm/doc/index.mld

@@ -141,6 +141,8 @@ In order to generate postcondition-checking, Ortac/QCheck-STM uses the
 [ensures] clauses that were not used for the [next_state] function but it also
 uses the [checks] clauses and the [raises] ones.
 
+{1 How to generate the test file }
+
 Now you can generate the QCheck-STM file by running the following command where
 you indicate the file you want to test, the function call to build a value of
 the type indicated in the third argument. You can write the generated code into
@@ -177,6 +179,20 @@ like the following:
   (run %{test} --verbose)))
 ]}
 
+There are other optional argument that are worth detailing here.
+
+The first one is the [-i] optional argument, taking the name of the module to
+include in the generated code. This is a flexible way to provide pretty
+pinters, QCheck generators and extenstions to the [STM.ty] type.
+
+The second one is the [-p] optional argument, taking a string. The string
+should be the name of a function, and the function will be protecting the call
+to the generated tests. The function should be implemented in the included
+module (the one passed to the [-i] optional argument). The funciton is of type
+[(unit -> unit) -> unit]. That means that it takes the suspended call the the
+generated tests as argument, so don't forget to launch them when implementing
+the function. One use case of this optional argument is to set up a [Lwt]
+scheduler berfore running the tests.
 {1 Warning system}
 
 Now that you know what Gospel specifications for the [qcheck-stm] plugin should

plugins/qcheck-stm/src/config.ml

@@ -6,6 +6,8 @@ type t = {
   context : Context.t;
   sut_core_type : Ppxlib.core_type;
   init_sut : Ppxlib.expression;
+  include_ : string option;
+  protect_call : string option;
 }
 
 let get_sut_type_name config =
@@ -97,6 +99,14 @@ let init path init_sut sut_str =
     let context = List.fold_left add context sigs in
     let* sut_core_type = sut_core_type sut_str
     and* init_sut = init_sut_from_string init_sut in
-    ok (sigs, { context; sut_core_type; init_sut })
+    ok
+      ( sigs,
+        {
+          context;
+          sut_core_type;
+          init_sut;
+          include_ = None;
+          protect_call = None;
+        } )
   with Gospel.Warnings.Error (l, k) ->
     error (Ortac_core.Warnings.GospelError k, l)

plugins/qcheck-stm/src/ortac_qcheck_stm.ml

@@ -4,14 +4,15 @@ module Ir_of_gospel = Ir_of_gospel
 module Reserr = Reserr
 module Stm_of_ir = Stm_of_ir
 
-let main path init sut include_ output quiet () =
+let main path init sut include_ protect_call output quiet () =
   let open Reserr in
   let fmt = Registration.get_out_formatter output in
   let pp = pp quiet Ppxlib_ast.Pprintast.structure fmt in
   pp
     (let* sigs, config = Config.init path init sut in
      let* ir = Ir_of_gospel.run sigs config in
-     Stm_of_ir.stm include_ config ir)
+     let config = { config with include_; protect_call } in
+     Stm_of_ir.stm config ir)
 
 open Cmdliner
 
@@ -38,6 +39,15 @@ end = struct
              system under test."
           ~docv:"INIT")
 
+  let protect_call =
+    Arg.(
+      value
+      & opt (some string) None
+      & info [ "p"; "protect-call" ] ~docv:"PROTECT_CALL"
+          ~doc:
+            "Protect the call of the QCheck tests with PROTECT_CALL. \
+             PROTECT_CALL should be the name of a function.")
+
   let term =
     let open Registration in
     Term.(
@@ -46,6 +56,7 @@ end = struct
       $ init
       $ sut
       $ include_
+      $ protect_call
       $ output_file
       $ quiet
       $ setup_log)

plugins/qcheck-stm/src/stm_of_ir.ml

@@ -770,7 +770,7 @@ let ghost_functions config =
   in
   aux config []
 
-let stm include_ config ir =
+let stm config ir =
   let open Reserr in
   let* config, ghost_functions = ghost_functions config ir.ghost_functions in
   let warn = [%stri [@@@ocaml.warning "-26-27"]] in
@@ -783,7 +783,7 @@ let stm include_ config ir =
         |> Mod.ident
         |> Incl.mk
         |> pstr_include)
-      include_
+      config.include_
     |> Option.to_list
   in
   let sut = sut_type config in
@@ -841,11 +841,20 @@ let stm include_ config ir =
   let call_tests =
     let loc = Location.none in
     let descr = estring (module_name ^ " STM tests") in
-    [%stri
-      let _ =
+    let expr =
+      [%expr
         QCheck_base_runner.run_tests_main
           (let count = 1000 in
            [ STMTests.agree_test ~count ~name:[%e descr] ])]
+    in
+    let expr =
+      match config.protect_call with
+      | None -> expr
+      | Some f ->
+          pexp_apply (qualify [ "Spec" ] f)
+            [ (Nolabel, efun [ (Nolabel, punit) ] expr) ]
+    in
+    pstr_value Nonrecursive [ value_binding ~pat:ppat_any ~expr ]
   in
   ok
     ([ open_mod module_name ]

plugins/qcheck-stm/test/dune

@@ -42,3 +42,61 @@
  (alias runtest)
  (action
   (diff dune.inc dune.inc.gen)))
+
+; include dependency is not handle by dune_gen
+
+(library
+ (name protect_with)
+ (modules protect_with))
+
+(rule
+ (target protect_with_stm_tests.ml)
+ (package ortac-qcheck-stm)
+ (deps
+  (package ortac-core)
+  (package ortac-qcheck-stm))
+ (action
+  (setenv
+   ORTAC_ONLY_PLUGIN
+   qcheck-stm
+   (with-stderr-to
+    protect_with_errors
+    (run
+     ortac
+     qcheck-stm
+     %{dep:protect_with.mli}
+     "make ()"
+     "int t"
+     --include=protect_with_include
+     --protect-call=run_tests
+     -o
+     %{target})))))
+
+(test
+ (name protect_with_stm_tests)
+ (package ortac-qcheck-stm)
+ (modules protect_with_stm_tests protect_with_include)
+ (libraries
+  qcheck-core
+  qcheck-core.runner
+  qcheck-stm.stm
+  qcheck-stm.sequential
+  qcheck-multicoretests-util
+  ortac-runtime
+  protect_with)
+ (action
+  (echo
+   "\n%{dep:protect_with_stm_tests.exe} has been generated with the ortac-qcheck-stm plugin.\n")))
+
+(rule
+ (alias runtest)
+ (package ortac-qcheck-stm)
+ (action
+  (progn
+   (diff protect_with_errors.expected protect_with_errors)
+   (diff protect_with_stm_tests.expected.ml protect_with_stm_tests.ml))))
+
+(rule
+ (alias launchtests)
+ (action
+  (run %{dep:protect_with_stm_tests.exe} -v)))

plugins/qcheck-stm/test/protect_with.ml

@@ -0,0 +1,13 @@
+type 'a t = 'a list ref
+
+exception Empty
+
+let make () = ref []
+let push a t = t := a :: !t
+
+let pop t =
+  match !t with
+  | [] -> raise Empty
+  | x :: xs ->
+      t := xs;
+      x

plugins/qcheck-stm/test/protect_with.mli

@@ -0,0 +1,22 @@
+type 'a t
+(*@ mutable model contents : 'a sequence *)
+
+exception Empty
+
+val make : unit -> 'a t
+(*@ t = make ()
+    ensures t.contents = Sequence.empty *)
+
+val push : 'a -> 'a t -> unit
+(*@ push a t
+    modifies t.contents
+    ensures t.contents = Sequence.cons a (old t.contents) *)
+
+val pop : 'a t -> 'a
+(*@ a = pop t
+    modifies t.contents
+    ensures t.contents = if old t.contents = Sequence.empty
+                         then Sequence.empty
+                         else Sequence.tl (old t.contents)
+    ensures (old t.contents) = Sequence.cons a t.contents
+    raises Empty -> old t.contents = Sequence.empty = t.contents *)

plugins/qcheck-stm/test/protect_with_include.ml

@@ -0,0 +1 @@
+let run_tests tests = tests ()