From 64e14b923b6612192075dd21f464e03ae08b2ea6 Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Wed, 7 Feb 2024 10:53:28 +0100 Subject: [PATCH] Add some tests --- plugins/qcheck-stm/test/dune.inc | 53 +++++++ plugins/qcheck-stm/test/dune_gen.args | 2 + plugins/qcheck-stm/test/invariants.ml | 4 + plugins/qcheck-stm/test/invariants.mli | 13 ++ .../test/invariants_errors.expected | 4 - .../test/invariants_stm_tests.expected.ml | 148 ++++++++++++++++++ 6 files changed, 220 insertions(+), 4 deletions(-) create mode 100644 plugins/qcheck-stm/test/invariants.ml create mode 100644 plugins/qcheck-stm/test/invariants.mli create mode 100644 plugins/qcheck-stm/test/invariants_stm_tests.expected.ml diff --git a/plugins/qcheck-stm/test/dune.inc b/plugins/qcheck-stm/test/dune.inc index 1d7a8ccd..b90555f8 100644 --- a/plugins/qcheck-stm/test/dune.inc +++ b/plugins/qcheck-stm/test/dune.inc @@ -316,3 +316,56 @@ (action (run %{dep:sequence_model_stm_tests.exe} -v))) +(library + (name invariants) + (modules invariants)) + +(rule + (target invariants_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 + invariants_errors + (run + ortac + qcheck-stm + %{dep:invariants.mli} + "create 42" "int t" + -o + %{target}))))) + +(test + (name invariants_stm_tests) + (package ortac-qcheck-stm) + (modules invariants_stm_tests) + (libraries + qcheck-core + qcheck-core.runner + qcheck-stm.stm + qcheck-stm.sequential + qcheck-multicoretests-util + ortac-runtime + invariants) + (action + (echo + "\n%{dep:invariants_stm_tests.exe} has been generated with the ortac-qcheck-stm plugin.\n"))) + +(rule + (alias runtest) + (package ortac-qcheck-stm) + (action + (progn + (diff invariants_errors.expected invariants_errors) + (diff invariants_stm_tests.expected.ml invariants_stm_tests.ml)))) + +(rule + (alias launchtests) + (action + (run %{dep:invariants_stm_tests.exe} -v))) + diff --git a/plugins/qcheck-stm/test/dune_gen.args b/plugins/qcheck-stm/test/dune_gen.args index 9fbea307..0fd84b7c 100644 --- a/plugins/qcheck-stm/test/dune_gen.args +++ b/plugins/qcheck-stm/test/dune_gen.args @@ -10,3 +10,5 @@ conjunctive_clauses "make 42 'a'" "char t" sequence_model "create ()" "char t" +invariants +"create 42" "int t" diff --git a/plugins/qcheck-stm/test/invariants.ml b/plugins/qcheck-stm/test/invariants.ml new file mode 100644 index 00000000..d2de1303 --- /dev/null +++ b/plugins/qcheck-stm/test/invariants.ml @@ -0,0 +1,4 @@ +type 'a t = 'a list ref + +let create a = ref [ a ] +let push a t = t := a :: !t diff --git a/plugins/qcheck-stm/test/invariants.mli b/plugins/qcheck-stm/test/invariants.mli new file mode 100644 index 00000000..b826d036 --- /dev/null +++ b/plugins/qcheck-stm/test/invariants.mli @@ -0,0 +1,13 @@ +type 'a t +(*@ mutable model contents : 'a list + with x + invariant List.length x.contents > 0 *) + +val create : 'a -> 'a t +(*@ t = create a + ensures t.contents = a :: [] *) + +val push : 'a -> 'a t -> unit +(*@ push a t + modifies t + ensures t.contents = a :: (old t.contents) *) diff --git a/plugins/qcheck-stm/test/invariants_errors.expected b/plugins/qcheck-stm/test/invariants_errors.expected index 5225c8b4..e69de29b 100644 --- a/plugins/qcheck-stm/test/invariants_errors.expected +++ b/plugins/qcheck-stm/test/invariants_errors.expected @@ -1,4 +0,0 @@ -File "invariants.mli", line 4, characters 4-14: -4 | invariants List.length x.contents > 0 *) - ^^^^^^^^^^ -Error: Gospel error: Syntax error. diff --git a/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml b/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml new file mode 100644 index 00000000..cf3b1987 --- /dev/null +++ b/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml @@ -0,0 +1,148 @@ +open Invariants +module Spec = + struct + open STM + [@@@ocaml.warning "-26-27"] + type sut = int t + type cmd = + | Push of int + let show_cmd cmd__001_ = + match cmd__001_ with + | Push a_1 -> Format.asprintf "%s %a" "push" (Util.Pp.pp_int true) a_1 + type nonrec state = { + contents: int list } + let init_state = + let a_2 = 42 in + { + contents = + (try a_2 :: [] + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "invariants.mli"; + pos_lnum = 8; + pos_bol = 292; + pos_cnum = 317 + }; + Ortac_runtime.stop = + { + pos_fname = "invariants.mli"; + pos_lnum = 8; + pos_bol = 292; + pos_cnum = 324 + } + }))) + } + let init_sut () = create 42 + let cleanup _ = () + let arb_cmd _ = + let open QCheck in + make ~print:show_cmd + (let open Gen in oneof [(pure (fun a_1 -> Push a_1)) <*> int]) + let next_state cmd__002_ state__003_ = + match cmd__002_ with + | Push a_1 -> + { + contents = + ((try a_1 :: state__003_.contents + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "invariants.mli"; + pos_lnum = 13; + pos_bol = 476; + pos_cnum = 501 + }; + Ortac_runtime.stop = + { + pos_fname = "invariants.mli"; + pos_lnum = 13; + pos_bol = 476; + pos_cnum = 522 + } + })))) + } + let precond cmd__008_ state__009_ = + match cmd__008_ with | Push a_1 -> true + let postcond cmd__004_ state__005_ res__006_ = + let new_state__007_ = lazy (next_state cmd__004_ state__005_) in + match (cmd__004_, res__006_) with + | (Push a_1, Res ((Unit, _), _)) -> + (try + Ortac_runtime.Gospelstdlib.(>) + (Ortac_runtime.Gospelstdlib.List.length + (Lazy.force new_state__007_).contents) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "invariants.mli"; + pos_lnum = 4; + pos_bol = 110; + pos_cnum = 124 + }; + Ortac_runtime.stop = + { + pos_fname = "invariants.mli"; + pos_lnum = 4; + pos_bol = 110; + pos_cnum = 150 + } + }))) + | _ -> true + let run cmd__010_ sut__011_ = + match cmd__010_ with | Push a_1 -> Res (unit, (push a_1 sut__011_)) + end +module STMTests = (STM_sequential.Make)(Spec) +let wrapped_init_state () = + let __state__012_ = Spec.init_state in + if + try + Ortac_runtime.Gospelstdlib.(>) + (Ortac_runtime.Gospelstdlib.List.length __state__012_.contents) + (Ortac_runtime.Gospelstdlib.integer_of_int 0) + with + | e -> + raise + (Ortac_runtime.Partial_function + (e, + { + Ortac_runtime.start = + { + pos_fname = "invariants.mli"; + pos_lnum = 4; + pos_bol = 110; + pos_cnum = 124 + }; + Ortac_runtime.stop = + { + pos_fname = "invariants.mli"; + pos_lnum = 4; + pos_bol = 110; + pos_cnum = 150 + } + })) + then __state__012_ + else QCheck.Test.fail_report "INIT_SUT violates type invariants for SUT" +let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs +let _ = + let open QCheck in + QCheck_base_runner.run_tests_main + (let count = 1000 in + [Test.make ~count ~name:"Invariants STM tests" + (STMTests.arb_cmds Spec.init_state) agree_prop])