From 866be4a8429fd88bd837abf08264a07fde408e70 Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Tue, 16 Apr 2024 17:35:30 +0200 Subject: [PATCH 1/3] Collect `cleanup` function in configuration module The `cleanup` function is optional. --- plugins/qcheck-stm/src/config.ml | 23 +++++++++++++++++++++-- plugins/qcheck-stm/src/stm_of_ir.ml | 9 ++++++--- 2 files changed, 27 insertions(+), 5 deletions(-) diff --git a/plugins/qcheck-stm/src/config.ml b/plugins/qcheck-stm/src/config.ml index a1216a98..46c001d9 100644 --- a/plugins/qcheck-stm/src/config.ml +++ b/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 diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml index b6b3edae..90528776 100644 --- a/plugins/qcheck-stm/src/stm_of_ir.ml +++ b/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 From 75b85e1b449f11320161f155e63bd630062a62ec Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Thu, 16 May 2024 10:37:44 +0200 Subject: [PATCH 2/3] Add test for cleanup function generation --- plugins/qcheck-stm/test/dune.inc | 53 ++++++++++ plugins/qcheck-stm/test/dune_gen.args | 2 + plugins/qcheck-stm/test/test_cleanup.ml | 4 + plugins/qcheck-stm/test/test_cleanup.mli | 11 ++ .../qcheck-stm/test/test_cleanup_config.ml | 7 ++ .../test/test_cleanup_stm_tests.expected.ml | 100 ++++++++++++++++++ 6 files changed, 177 insertions(+) create mode 100644 plugins/qcheck-stm/test/test_cleanup.ml create mode 100644 plugins/qcheck-stm/test/test_cleanup.mli create mode 100644 plugins/qcheck-stm/test/test_cleanup_config.ml create mode 100644 plugins/qcheck-stm/test/test_cleanup_stm_tests.expected.ml diff --git a/plugins/qcheck-stm/test/dune.inc b/plugins/qcheck-stm/test/dune.inc index a9132b53..e654496b 100644 --- a/plugins/qcheck-stm/test/dune.inc +++ b/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))) + diff --git a/plugins/qcheck-stm/test/dune_gen.args b/plugins/qcheck-stm/test/dune_gen.args index 65c8bfa7..1234a6a0 100644 --- a/plugins/qcheck-stm/test/dune_gen.args +++ b/plugins/qcheck-stm/test/dune_gen.args @@ -24,3 +24,5 @@ tuples tuples_config functional_model functional_model_config +test_cleanup +test_cleanup_config diff --git a/plugins/qcheck-stm/test/test_cleanup.ml b/plugins/qcheck-stm/test/test_cleanup.ml new file mode 100644 index 00000000..dd1106ba --- /dev/null +++ b/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 diff --git a/plugins/qcheck-stm/test/test_cleanup.mli b/plugins/qcheck-stm/test/test_cleanup.mli new file mode 100644 index 00000000..edafc559 --- /dev/null +++ b/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 *) diff --git a/plugins/qcheck-stm/test/test_cleanup_config.ml b/plugins/qcheck-stm/test/test_cleanup_config.ml new file mode 100644 index 00000000..324681df --- /dev/null +++ b/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 diff --git a/plugins/qcheck-stm/test/test_cleanup_stm_tests.expected.ml b/plugins/qcheck-stm/test/test_cleanup_stm_tests.expected.ml new file mode 100644 index 00000000..2f7dd31d --- /dev/null +++ b/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]) From 22beab971961677c142798afbe5a3bfe37244e25 Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Thu, 16 May 2024 10:46:03 +0200 Subject: [PATCH 3/3] Update Changelog --- CHANGES.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index ac35d929..947ac9e4 100644 --- a/CHANGES.md +++ b/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