Add support for type invariants

CHANGES.md

@@ -2,6 +2,8 @@
 
 - Add a comment warning that the file is generated
   [\#198](https://github.com/ocaml-gospel/ortac/pull/198)
+- Add support for type invariants
+  [\#197](https://github.com/ocaml-gospel/ortac/pull/197)
 - Add an include option to qcheck-stm cli
   [\#181](https://github.com/ocaml-gospel/ortac/pull/181)
 - Add a quiet flag

examples/lwt_dllist_tests.ml

@@ -546,7 +546,10 @@ module Spec =
       | Take_opt_r -> Res ((option int), (take_opt_r sut__016_))
   end
 module STMTests = (STM_sequential.Make)(Spec)
+let check_init_state () = ()
+let agree_prop cs = check_init_state (); 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"])
+     [QCheck.Test.make ~count ~name:"Lwt_dllist_spec STM tests"
+        (STMTests.arb_cmds Spec.init_state) agree_prop])

examples/varray_circular_tests.ml

@@ -1189,7 +1189,10 @@ module Spec =
               (protect (fun () -> fill sut__033_ pos len x_3) ()))
   end
 module STMTests = (STM_sequential.Make)(Spec)
+let check_init_state () = ()
+let agree_prop cs = check_init_state (); 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"])
+     [QCheck.Test.make ~count ~name:"Varray_circular_spec STM tests"
+        (STMTests.arb_cmds Spec.init_state) agree_prop])

examples/varray_tests.ml

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

plugins/qcheck-stm/src/ir.ml

@@ -56,6 +56,7 @@ let value id ty inst sut_var args ret next_state precond postcond =
 
 type t = {
   state : (Ident.t * Ppxlib.core_type) list;
+  invariants : (Ident.t * Tterm.term list) option;
   init_state : init_state;
   ghost_functions : Tast.function_ list;
   values : value list;

plugins/qcheck-stm/src/ir_of_gospel.ml

@@ -219,39 +219,27 @@ let sig_item config init_fct state s =
       else Some (val_desc config state vd)
   | _ -> None
 
-let state config sigs =
+let state_and_invariants config sigs =
   let sut_name = Cfg.get_sut_type_name_str config in
   let is_sut_decl s =
     let p t = t.td_ts.ts_ident.id_str = sut_name in
     match s.sig_desc with
-    | Sig_type (_, ts, _) -> (
-        List.filter p ts |> function
-        | [] -> None
-        | [ t ] -> Some t
-        (* As multiple type declarations with the same name is illegal, last
-           case can't happen *)
-        | _ -> assert false)
+    | Sig_type (_, ts, _) -> List.find_opt p ts
     | _ -> None
   in
   let open Reserr in
   let* ty =
-    match List.filter_map is_sut_decl sigs with
-    | [] -> error (No_sut_type sut_name, Ppxlib.Location.none)
-    | [ ty ] -> ok ty
-    (* As multiple type declarations with the same name is illegal, last
-       case can't happen *)
-    | _ -> assert false
+    List.filter_map is_sut_decl sigs
+    |> Fun.flip List.nth_opt 0
+    |> of_option ~default:(No_sut_type sut_name, Ppxlib.Location.none)
   in
   let open Ortac_core in
   let* subst =
     Fun.flip List.assoc_opt
     <$> (Ocaml_of_gospel.core_type_of_tysymbol ~context:config.context ty.td_ts
         |> unify (`Type ty) config.sut_core_type)
-  in
-  let* spec =
-    match ty.td_spec with
-    | None -> error (Sut_type_not_specified sut_name, ty.td_loc)
-    | Some spec -> ok spec
+  and* spec =
+    of_option ~default:(Sut_type_not_specified sut_name, ty.td_loc) ty.td_spec
   in
   let process_model (ls, _) =
     let open Symbols in
@@ -260,9 +248,15 @@ let state config sigs =
       |> Ocaml_of_gospel.core_type_of_ty_with_subst ~context:config.context
            subst )
   in
-  match spec.ty_fields with
-  | [] -> error (No_models sut_name, spec.ty_loc)
-  | xs -> List.map process_model xs |> ok
+  let* state =
+    match spec.ty_fields with
+    | [] -> error (No_models sut_name, spec.ty_loc)
+    | xs -> List.map process_model xs |> ok
+  in
+  let invariants =
+    Option.map (fun (vs, xs) -> (vs.Symbols.vs_name, xs)) spec.ty_invariants
+  in
+  ok (state, invariants)
 
 let init_state config state sigs =
   let open Cfg in
@@ -383,8 +377,8 @@ let ghost_functions =
 let run sigs config =
   let open Reserr in
   let open Ir in
-  let* state = state config sigs in
+  let* state, invariants = state_and_invariants config sigs in
   let* init_fct, init_state = init_state config state sigs in
   let ghost_functions = ghost_functions sigs in
   let* values = signature config init_fct state sigs in
-  ok { state; init_state; ghost_functions; values }
+  ok { state; invariants; init_state; ghost_functions; values }

plugins/qcheck-stm/src/stm_of_ir.ml

@@ -14,16 +14,6 @@ let may_raise_exception v =
   | [], [] -> false
   | _, _ -> true
 
-let qualify ms v =
-  let lid =
-    match ms with
-    | [] -> Lident v
-    | m :: ms ->
-        let pref = List.fold_left (fun acc x -> Ldot (acc, x)) (Lident m) ms in
-        Ldot (pref, v)
-  in
-  Ast_helper.Exp.ident (noloc lid)
-
 let subst_core_type inst ty =
   let rec aux ty =
     {
@@ -429,12 +419,17 @@ let precond config ir =
   in
   pstr_value Nonrecursive [ value_binding ~pat ~expr ] |> ok
 
-let postcond_case config state idx state_ident new_state_ident value =
+let postcond_case config state invariants idx state_ident new_state_ident value
+    =
   let open Reserr in
   let translate_postcond t =
     subst_term state ~gos_t:value.sut_var ~old_t:(Some state_ident) ~new_lz:true
       ~new_t:(Some new_state_ident) t
     >>= ocaml_of_term config
+  and translate_invariants id t =
+    subst_term state ~gos_t:id ~old_t:None ~new_t:(Some new_state_ident)
+      ~new_lz:true t
+    >>= ocaml_of_term config
   in
   let idx = List.sort Int.compare idx in
   let lhs0 = mk_cmd_pattern value in
@@ -485,7 +480,13 @@ let postcond_case config state idx state_ident new_state_ident value =
       in
       aux idx value.postcond.normal
     in
-    list_and <$> map translate_postcond normal
+    let* postcond = map translate_postcond normal
+    and* invariants =
+      Option.fold ~none:(ok [])
+        ~some:(fun (id, xs) -> map (translate_invariants id) xs)
+        invariants
+    in
+    list_and (postcond @ invariants) |> ok
   in
   let res, pat_ret =
     match value.ret with
@@ -568,8 +569,8 @@ let postcond config idx ir =
     (Fun.flip ( @ )) [ case ~lhs:ppat_any ~guard:None ~rhs:(ebool true) ]
     <$> map
           (fun v ->
-            postcond_case config ir.state (List.assoc v.id idx) state_ident
-              new_state_ident v)
+            postcond_case config ir.state ir.invariants (List.assoc v.id idx)
+              state_ident new_state_ident v)
           ir.values
   in
   let body =
@@ -725,8 +726,36 @@ 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 check_init_state config ir =
+  let init_state = qualify [ "Spec" ] "init_state" in
+  let open Reserr in
+  let state_name = gen_symbol ~prefix:"__state" () in
+  let state_pat = pvar state_name
+  and state_id = Ident.create ~loc:Location.none state_name in
+  let translate_invariants id t =
+    enot
+    <$> (subst_term ir.state ~gos_t:id ~old_t:None ~new_t:(Some state_id) t
+        >>= ocaml_of_term config)
+  and msg =
+    let f = qualify [ "QCheck"; "Test" ] "fail_report"
+    and s = estring "INIT_SUT violates type invariants for SUT" in
+    eapply f [ s ]
+  in
+  let* expr =
+    (function
+      | [] -> eunit
+      | xs ->
+          pexp_let Nonrecursive
+            [ value_binding ~pat:state_pat ~expr:init_state ]
+            (pexp_ifthenelse (list_or xs) msg None))
+    <$> Option.fold ~none:(ok [])
+          ~some:(fun (id, xs) -> map (translate_invariants id) xs)
+          ir.invariants
+  in
+  let pat = pvar "check_init_state" and expr = efun [ (Nolabel, punit) ] expr in
   pstr_value Nonrecursive [ value_binding ~pat ~expr ] |> ok
 
 let ghost_function config fct =
@@ -770,6 +799,12 @@ let ghost_functions config =
   in
   aux config []
 
+let agree_prop =
+  [%stri
+    let agree_prop cs =
+      check_init_state ();
+      STMTests.agree_prop cs]
+
 let stm include_ config ir =
   let open Reserr in
   let* config, ghost_functions = ghost_functions config ir.ghost_functions in
@@ -796,6 +831,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* check_init_state = check_init_state config ir in
   let cleanup =
     let pat = pvar "cleanup" in
     let expr = efun [ (Nolabel, ppat_any) ] eunit in
@@ -845,9 +881,13 @@ let stm include_ config ir =
       let _ =
         QCheck_base_runner.run_tests_main
           (let count = 1000 in
-           [ STMTests.agree_test ~count ~name:[%e descr] ])]
+           [
+             QCheck.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; check_init_state; agree_prop; call_tests ])

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

@@ -592,6 +592,10 @@ module Spec =
       | Mem a_3 -> Res (bool, (mem a_3 sut__019_))
   end
 module STMTests = (STM_sequential.Make)(Spec)
+let check_init_state () = ()
+let agree_prop cs = check_init_state (); STMTests.agree_prop cs
 let _ =
   QCheck_base_runner.run_tests_main
-    (let count = 1000 in [STMTests.agree_test ~count ~name:"Array STM tests"])
+    (let count = 1000 in
+     [QCheck.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

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

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)))
+

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"

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

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

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

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) *)