Read optional cleanup function from configuration module

CHANGES.md

@@ -1,5 +1,7 @@
 # 0.3.0
 
+- Read an optional `cleanup` function from configuration module
+  [\#226](https://github.com/ocaml-gospel/ortac/pull/226)
 - Fix field access translation
   [\#229](https://github.com/ocaml-gospel/ortac/pull/229)
 - Add support for functional type in model

plugins/qcheck-stm/src/config.ml

@@ -8,6 +8,7 @@ type config_under_construction = {
   gen_mod' : Ppxlib.structure option;
   pp_mod' : Ppxlib.structure option;
   ty_mod' : Ppxlib.structure option;
+  cleanup' : Ppxlib.structure_item option;
 }
 
 let config_under_construction =
@@ -17,6 +18,7 @@ let config_under_construction =
     gen_mod' = None;
     pp_mod' = None;
     ty_mod' = None;
+    cleanup' = None;
   }
 
 type t = {
@@ -27,6 +29,7 @@ type t = {
   gen_mod : Ppxlib.structure option; (* Containing custom QCheck generators *)
   pp_mod : Ppxlib.structure option; (* Containing custom pretty printers *)
   ty_mod : Ppxlib.structure option; (* Containing custom STM.ty extensions *)
+  cleanup : Ppxlib.structure_item option;
 }
 
 let mk_config context cfg_uc =
@@ -43,8 +46,19 @@ let mk_config context cfg_uc =
   let init_sut_txt = Fmt.str "%a" Pprintast.expression init_sut
   and gen_mod = cfg_uc.gen_mod'
   and pp_mod = cfg_uc.pp_mod'
-  and ty_mod = cfg_uc.ty_mod' in
-  ok { context; sut_core_type; init_sut; init_sut_txt; gen_mod; pp_mod; ty_mod }
+  and ty_mod = cfg_uc.ty_mod'
+  and cleanup = cfg_uc.cleanup' in
+  ok
+    {
+      context;
+      sut_core_type;
+      init_sut;
+      init_sut_txt;
+      gen_mod;
+      pp_mod;
+      ty_mod;
+      cleanup;
+    }
 
 let get_sut_type_name config =
   let open Ppxlib in
@@ -104,6 +118,11 @@ let value_bindings cfg_uc =
     | Ppat_var s when String.equal "init_sut" s.txt ->
         let init_sut' = Some vb.pvb_expr in
         ok { cfg_uc with init_sut' }
+    | Ppat_var s when String.equal "cleanup" s.txt ->
+        let cleanup' =
+          Option.some @@ Ortac_core.Builder.pstr_value Nonrecursive [ vb ]
+        in
+        ok { cfg_uc with cleanup' }
     | _ -> ok cfg_uc
   in
   fold_left aux cfg_uc

plugins/qcheck-stm/src/stm_of_ir.ml

@@ -1114,9 +1114,12 @@ let stm config ir =
   let* init_state = init_state config ir in
   let* check_init_state = check_init_state config ir in
   let cleanup =
-    let pat = pvar "cleanup" in
-    let expr = efun [ (Nolabel, ppat_any) ] eunit in
-    pstr_value Nonrecursive [ value_binding ~pat ~expr ]
+    let default =
+      let pat = pvar "cleanup" in
+      let expr = efun [ (Nolabel, ppat_any) ] eunit in
+      pstr_value Nonrecursive [ value_binding ~pat ~expr ]
+    in
+    Option.value config.cleanup ~default
   in
   let init_sut =
     let pat = pvar "init_sut" in

plugins/qcheck-stm/test/dune.inc

@@ -687,3 +687,56 @@
  (action
   (run %{dep:functional_model_stm_tests.exe} -v)))
 
+(library
+ (name test_cleanup)
+ (modules test_cleanup))
+
+(rule
+ (target test_cleanup_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
+    test_cleanup_errors
+    (run
+     ortac
+     qcheck-stm
+     %{dep:test_cleanup.mli}
+     %{dep:test_cleanup_config.ml}
+     -o
+     %{target})))))
+
+(test
+ (name test_cleanup_stm_tests)
+ (package ortac-qcheck-stm)
+ (modules test_cleanup_stm_tests)
+ (libraries
+  qcheck-core
+  qcheck-core.runner
+  qcheck-stm.stm
+  qcheck-stm.sequential
+  qcheck-multicoretests-util
+  ortac-runtime-qcheck-stm
+  test_cleanup)
+ (action
+  (echo
+   "\n%{dep:test_cleanup_stm_tests.exe} has been generated with the ortac-qcheck-stm plugin.\n")))
+
+(rule
+ (alias runtest)
+ (package ortac-qcheck-stm)
+ (action
+  (progn
+   (diff test_cleanup_errors.expected test_cleanup_errors)
+   (diff test_cleanup_stm_tests.expected.ml test_cleanup_stm_tests.ml))))
+
+(rule
+ (alias launchtests)
+ (action
+  (run %{dep:test_cleanup_stm_tests.exe} -v)))
+

plugins/qcheck-stm/test/dune_gen.args

@@ -24,3 +24,5 @@ tuples
 tuples_config
 functional_model
 functional_model_config
+test_cleanup
+test_cleanup_config

plugins/qcheck-stm/test/test_cleanup.ml

@@ -0,0 +1,4 @@
+type t = A of int ref
+
+let create () = A (ref 0)
+let use (A x) = incr x

plugins/qcheck-stm/test/test_cleanup.mli

@@ -0,0 +1,11 @@
+type t
+(*@ mutable model m : integer *)
+
+val create : unit -> t
+(*@ t = create ()
+    ensures t.m = 0 *)
+
+val use : t -> unit
+(*@ use t
+    modifies t.m
+    ensures t.m = 1 + old t.m *)

plugins/qcheck-stm/test/test_cleanup_config.ml

@@ -0,0 +1,7 @@
+open Test_cleanup
+
+let init_sut = create ()
+
+type sut = t
+
+let cleanup t = ignore t

plugins/qcheck-stm/test/test_cleanup_stm_tests.expected.ml

@@ -0,0 +1,100 @@
+(* This file is generated by ortac qcheck-stm,
+   edit how you run the tool instead *)
+[@@@ocaml.warning "-26-27-69-32"]
+open Test_cleanup
+module Ortac_runtime = Ortac_runtime_qcheck_stm
+module Spec =
+  struct
+    open STM
+    type _ ty +=  
+      | Integer: Ortac_runtime.integer ty 
+    let integer = (Integer, Ortac_runtime.string_of_integer)
+    type sut = t
+    type cmd =
+      | Use 
+    let show_cmd cmd__001_ =
+      match cmd__001_ with | Use -> Format.asprintf "%s sut" "use"
+    type nonrec state = {
+      m: Ortac_runtime.integer }
+    let init_state =
+      let () = () in
+      {
+        m =
+          (try Ortac_runtime.Gospelstdlib.integer_of_int 0
+           with
+           | e ->
+               raise
+                 (Ortac_runtime.Partial_function
+                    (e,
+                      {
+                        Ortac_runtime.start =
+                          {
+                            pos_fname = "test_cleanup.mli";
+                            pos_lnum = 6;
+                            pos_bol = 227;
+                            pos_cnum = 245
+                          };
+                        Ortac_runtime.stop =
+                          {
+                            pos_fname = "test_cleanup.mli";
+                            pos_lnum = 6;
+                            pos_bol = 227;
+                            pos_cnum = 246
+                          }
+                      })))
+      }
+    let init_sut () = create ()
+    let cleanup t = ignore t
+    let arb_cmd _ =
+      let open QCheck in
+        make ~print:show_cmd (let open Gen in oneof [pure Use])
+    let next_state cmd__002_ state__003_ =
+      match cmd__002_ with
+      | Use ->
+          {
+            m =
+              ((try
+                  Ortac_runtime.Gospelstdlib.(+)
+                    (Ortac_runtime.Gospelstdlib.integer_of_int 1)
+                    state__003_.m
+                with
+                | e ->
+                    raise
+                      (Ortac_runtime.Partial_function
+                         (e,
+                           {
+                             Ortac_runtime.start =
+                               {
+                                 pos_fname = "test_cleanup.mli";
+                                 pos_lnum = 11;
+                                 pos_bol = 377;
+                                 pos_cnum = 397
+                               };
+                             Ortac_runtime.stop =
+                               {
+                                 pos_fname = "test_cleanup.mli";
+                                 pos_lnum = 11;
+                                 pos_bol = 377;
+                                 pos_cnum = 398
+                               }
+                           }))))
+          }
+    let precond cmd__008_ state__009_ = match cmd__008_ with | Use -> true
+    let postcond _ _ _ = true
+    let run cmd__010_ sut__011_ =
+      match cmd__010_ with | Use -> Res (unit, (use sut__011_))
+  end
+module STMTests = (Ortac_runtime.Make)(Spec)
+let check_init_state () = ()
+let ortac_postcond cmd__004_ state__005_ res__006_ =
+  let open Spec in
+    let open STM in
+      let new_state__007_ = lazy (next_state cmd__004_ state__005_) in
+      match (cmd__004_, res__006_) with
+      | (Use, Res ((Unit, _), _)) -> None
+      | _ -> None
+let _ =
+  QCheck_base_runner.run_tests_main
+    (let count = 1000 in
+     [STMTests.agree_test ~count ~name:"Test_cleanup STM tests"
+        check_init_state ortac_postcond])