Check type invariants in init_state

examples/lwt_dllist_tests.ml

@@ -544,7 +544,11 @@ module Spec =
       | Take_opt_r -> Res ((option int), (take_opt_r sut__016_))
   end
 module STMTests = (STM_sequential.Make)(Spec)
+let wrapped_init_state () = Spec.init_state
+let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs
 let _ =
-  QCheck_base_runner.run_tests_main
-    (let count = 1000 in
-     [STMTests.agree_test ~count ~name:"Lwt_dllist_spec STM tests"])
+  let open QCheck in
+    QCheck_base_runner.run_tests_main
+      (let count = 1000 in
+       [Test.make ~count ~name:"Lwt_dllist_spec STM tests"
+          (STMTests.arb_cmds Spec.init_state) agree_prop])

examples/varray_circular_tests.ml

@@ -1187,7 +1187,11 @@ module Spec =
               (protect (fun () -> fill sut__033_ pos len x_3) ()))
   end
 module STMTests = (STM_sequential.Make)(Spec)
+let wrapped_init_state () = Spec.init_state
+let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs
 let _ =
-  QCheck_base_runner.run_tests_main
-    (let count = 1000 in
-     [STMTests.agree_test ~count ~name:"Varray_circular_spec STM tests"])
+  let open QCheck in
+    QCheck_base_runner.run_tests_main
+      (let count = 1000 in
+       [Test.make ~count ~name:"Varray_circular_spec STM tests"
+          (STMTests.arb_cmds Spec.init_state) agree_prop])

examples/varray_tests.ml

@@ -1187,7 +1187,11 @@ module Spec =
               (protect (fun () -> fill sut__033_ pos len x_3) ()))
   end
 module STMTests = (STM_sequential.Make)(Spec)
+let wrapped_init_state () = Spec.init_state
+let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs
 let _ =
-  QCheck_base_runner.run_tests_main
-    (let count = 1000 in
-     [STMTests.agree_test ~count ~name:"Varray_spec STM tests"])
+  let open QCheck in
+    QCheck_base_runner.run_tests_main
+      (let count = 1000 in
+       [Test.make ~count ~name:"Varray_spec STM tests"
+          (STMTests.arb_cmds Spec.init_state) agree_prop])

plugins/qcheck-stm/src/stm_of_ir.ml

@@ -736,8 +736,42 @@ let init_state config ir =
                      Ppxlib.Location.none )))
       ir.state
   in
-  let expr = pexp_record fields None |> bindings in
-  let pat = pvar "init_state" in
+  let expr = pexp_record fields None |> bindings and pat = pvar "init_state" in
+  pstr_value Nonrecursive [ value_binding ~pat ~expr ] |> ok
+
+let wrapped_init_state config ir =
+  let init_state = [%expr Spec.init_state] in
+  let open Reserr in
+  (* Now we include a check that the new expression describing the inital state
+     respects the type invariants for sut *)
+  let* expr =
+    if Option.is_some ir.invariants then
+      let state_name = gen_symbol ~prefix:"__state" () in
+      let state_var = evar state_name
+      and state_pat = pvar state_name
+      and state_id = Ident.create ~loc:Location.none state_name in
+      let translate_invariants id t =
+        subst_term ir.state ~gos_t:id ~old_t:None ~new_t:(Some state_id) t
+        >>= ocaml_of_term config
+      in
+      let* invariants =
+        list_and
+        <$> Option.fold ~none:(ok [])
+              ~some:(fun (id, xs) -> map (translate_invariants id) xs)
+              ir.invariants
+      in
+      let msg =
+        [%expr
+          QCheck.Test.fail_report "INIT_SUT violates type invariants for SUT"]
+      in
+      pexp_let Nonrecursive
+        [ value_binding ~pat:state_pat ~expr:init_state ]
+        (pexp_ifthenelse invariants state_var (Some msg))
+      |> ok
+    else init_state |> ok
+  in
+  let expr = efun [ (Nolabel, punit) ] expr
+  and pat = pvar "wrapped_init_state" in
   pstr_value Nonrecursive [ value_binding ~pat ~expr ] |> ok
 
 let ghost_function config fct =
@@ -781,6 +815,12 @@ let ghost_functions config =
   in
   aux config []
 
+let agree_prop =
+  [%stri
+    let agree_prop cs =
+      let _ = wrapped_init_state () in
+      STMTests.agree_prop cs]
+
 let stm include_ config ir =
   let open Reserr in
   let* config, ghost_functions = ghost_functions config ir.ghost_functions in
@@ -807,6 +847,7 @@ let stm include_ config ir =
   let* run = run config ir in
   let* arb_cmd = arb_cmd ir in
   let* init_state = init_state config ir in
+  let* wrapped_init_state = wrapped_init_state config ir in
   let cleanup =
     let pat = pvar "cleanup" in
     let expr = efun [ (Nolabel, ppat_any) ] eunit in
@@ -854,11 +895,16 @@ let stm include_ config ir =
     let descr = estring (module_name ^ " STM tests") in
     [%stri
       let _ =
+        let open QCheck in
         QCheck_base_runner.run_tests_main
           (let count = 1000 in
-           [ STMTests.agree_test ~count ~name:[%e descr] ])]
+           [
+             Test.make ~count ~name:[%e descr]
+               (STMTests.arb_cmds Spec.init_state)
+               agree_prop;
+           ])]
   in
   ok
     ([ open_mod module_name ]
     @ ghost_functions
-    @ [ stm_spec; tests; call_tests ])
+    @ [ stm_spec; tests; wrapped_init_state; agree_prop; call_tests ])

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

@@ -590,6 +590,11 @@ module Spec =
       | Mem a_3 -> Res (bool, (mem a_3 sut__019_))
   end
 module STMTests = (STM_sequential.Make)(Spec)
+let wrapped_init_state () = Spec.init_state
+let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs
 let _ =
-  QCheck_base_runner.run_tests_main
-    (let count = 1000 in [STMTests.agree_test ~count ~name:"Array STM tests"])
+  let open QCheck in
+    QCheck_base_runner.run_tests_main
+      (let count = 1000 in
+       [Test.make ~count ~name:"Array STM tests"
+          (STMTests.arb_cmds Spec.init_state) agree_prop])

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

@@ -193,7 +193,11 @@ module Spec =
               (protect (fun () -> set sut__015_ i_1 a_2) ()))
   end
 module STMTests = (STM_sequential.Make)(Spec)
+let wrapped_init_state () = Spec.init_state
+let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs
 let _ =
-  QCheck_base_runner.run_tests_main
-    (let count = 1000 in
-     [STMTests.agree_test ~count ~name:"Conjunctive_clauses STM tests"])
+  let open QCheck in
+    QCheck_base_runner.run_tests_main
+      (let count = 1000 in
+       [Test.make ~count ~name:"Conjunctive_clauses STM tests"
+          (STMTests.arb_cmds Spec.init_state) agree_prop])

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

@@ -461,7 +461,11 @@ module Spec =
       | Length -> Res (int, (length sut__011_))
   end
 module STMTests = (STM_sequential.Make)(Spec)
+let wrapped_init_state () = Spec.init_state
+let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs
 let _ =
-  QCheck_base_runner.run_tests_main
-    (let count = 1000 in
-     [STMTests.agree_test ~count ~name:"Hashtbl STM tests"])
+  let open QCheck in
+    QCheck_base_runner.run_tests_main
+      (let count = 1000 in
+       [Test.make ~count ~name:"Hashtbl STM tests"
+          (STMTests.arb_cmds Spec.init_state) agree_prop])

plugins/qcheck-stm/test/invariants_errors.expected

@@ -0,0 +1,4 @@
+File "invariants.mli", line 4, characters 4-14:
+4 |     invariants List.length x.contents > 0 *)
+        ^^^^^^^^^^
+Error: Gospel error: Syntax error.

plugins/qcheck-stm/test/record_errors.expected

@@ -16,3 +16,8 @@ File "record.mli", line 3, characters 36-39:
                                         ^^^
 Warning: Skipping clause: occurrences of the SUT in clauses are only
          supported to access its model fields.
+File "record.mli", line 3, characters 36-39:
+3 |     with x invariant integer_of_int x.c = x.value *)
+                                        ^^^
+Warning: Skipping clause: occurrences of the SUT in clauses are only
+         supported to access its model fields.

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

@@ -157,7 +157,15 @@ module Spec =
       match cmd__010_ with | Get -> Res (int, (get sut__011_))
   end
 module STMTests = (STM_sequential.Make)(Spec)
+let wrapped_init_state () =
+  let __state__012_ = Spec.init_state in
+  if true
+  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 _ =
-  QCheck_base_runner.run_tests_main
-    (let count = 1000 in
-     [STMTests.agree_test ~count ~name:"Record STM tests"])
+  let open QCheck in
+    QCheck_base_runner.run_tests_main
+      (let count = 1000 in
+       [Test.make ~count ~name:"Record STM tests"
+          (STMTests.arb_cmds Spec.init_state) agree_prop])

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

@@ -78,6 +78,11 @@ module Spec =
       match cmd__010_ with | Get -> Res (int, (get sut__011_))
   end
 module STMTests = (STM_sequential.Make)(Spec)
+let wrapped_init_state () = Spec.init_state
+let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs
 let _ =
-  QCheck_base_runner.run_tests_main
-    (let count = 1000 in [STMTests.agree_test ~count ~name:"Ref STM tests"])
+  let open QCheck in
+    QCheck_base_runner.run_tests_main
+      (let count = 1000 in
+       [Test.make ~count ~name:"Ref STM tests"
+          (STMTests.arb_cmds Spec.init_state) agree_prop])

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

@@ -189,7 +189,11 @@ module Spec =
       | Remove_ -> Res ((option char), (remove_ sut__013_))
   end
 module STMTests = (STM_sequential.Make)(Spec)
+let wrapped_init_state () = Spec.init_state
+let agree_prop cs = let _ = wrapped_init_state () in STMTests.agree_prop cs
 let _ =
-  QCheck_base_runner.run_tests_main
-    (let count = 1000 in
-     [STMTests.agree_test ~count ~name:"Sequence_model STM tests"])
+  let open QCheck in
+    QCheck_base_runner.run_tests_main
+      (let count = 1000 in
+       [Test.make ~count ~name:"Sequence_model STM tests"
+          (STMTests.arb_cmds Spec.init_state) agree_prop])