Add a runtime for qcheck-stm

The runtime reimplement the QCheckSTM.Sequential.Make functor to use new postcond function. It also implement how the failure message is printed and the append function for postcond.
ocaml-gospel · Feb 15, 2024 · c5d2a8b · c5d2a8b
1 parent c684ec1
commit c5d2a8b
Show file tree

Hide file tree

Showing 23 changed files with 225 additions and 92 deletions.
diff --git a/dune-project b/dune-project
@@ -179,6 +179,24 @@
   ortac-core
   (ortac-qcheck-stm :with-test)))
 
+(package
+ (name ortac-runtime-qcheck-stm)
+ (synopsis "Runtime support library for Ortac/QCheck-STM-generated code")
+ (description
+  "\> The ortac-runtime-qcheck-stm library provides support for the code
+  "\> generated by the Ortac/QCheck-STM plugin (provided by the
+  "\> ortac-qcheck-stm package).
+  "\>
+  "\> Ortac (OCaml Runtime Assertion Checking) is a tool to turn
+  "\> executable Gospel specifications into code to test they hold.
+  )
+ (authors "Nicolas Osborne <[email protected]>")
+ (maintainers "Nicolas Osborne <[email protected]>")
+ (depends
+  (ocaml (>= 4.11.0))
+  qcheck-stm
+  ortac-runtime))
+
 (package
  (name ortac-examples)
  (synopsis

diff --git a/examples/dune.lwt_dllist.inc b/examples/dune.lwt_dllist.inc
@@ -56,7 +56,7 @@
   qcheck-stm.stm
   qcheck-stm.sequential
   qcheck-multicoretests-util
-  ortac-runtime)
+  ortac-runtime-qcheck-stm)
  (package ortac-examples)
  (action
   (run

diff --git a/examples/dune.varray.inc b/examples/dune.varray.inc
@@ -56,7 +56,7 @@
   qcheck-stm.stm
   qcheck-stm.sequential
   qcheck-multicoretests-util
-  ortac-runtime)
+  ortac-runtime-qcheck-stm)
  (package ortac-examples)
  (action
   (run

diff --git a/examples/dune.varray_circular.inc b/examples/dune.varray_circular.inc
@@ -56,7 +56,7 @@
   qcheck-stm.stm
   qcheck-stm.sequential
   qcheck-multicoretests-util
-  ortac-runtime)
+  ortac-runtime-qcheck-stm)
  (package ortac-examples)
  (action
   (run

diff --git a/examples/lwt_dllist_tests.ml b/examples/lwt_dllist_tests.ml
@@ -1,5 +1,6 @@
 [@@@ocaml.warning "-26-27"]
 open Lwt_dllist_spec
+module Ortac_runtime = Ortac_runtime_qcheck_stm
 module Spec =
   struct
     open STM
@@ -296,7 +297,7 @@ module Spec =
       | Take_opt_l -> Res ((option int), (take_opt_l sut__016_))
       | Take_opt_r -> Res ((option int), (take_opt_r sut__016_))
   end
-module STMTests = (STM_sequential.Make)(Spec)
+module STMTests = (Ortac_runtime.Make)(Spec)
 let wrapped_init_state () = Spec.init_state
 let ortac_postcond cmd__005_ state__006_ res__007_ =
   let (++) = Ortac_runtime.(++) in
@@ -725,10 +726,8 @@ let ortac_postcond cmd__005_ state__006_ res__007_ =
                        }
                    })])
       | _ -> None
-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:"Lwt_dllist_spec STM tests"
-          (STMTests.arb_cmds Spec.init_state) agree_prop])
+  QCheck_base_runner.run_tests_main
+    (let count = 1000 in
+     [STMTests.agree_test ~count ~name:"Lwt_dllist_spec STM tests"
+        wrapped_init_state ortac_postcond])
diff --git a/examples/varray_circular_tests.ml b/examples/varray_circular_tests.ml
@@ -1,5 +1,6 @@
 [@@@ocaml.warning "-26-27"]
 open Varray_circular_spec
+module Ortac_runtime = Ortac_runtime_qcheck_stm
 let inside i s =
   try
     if
@@ -705,7 +706,7 @@ module Spec =
             ((result unit exn),
               (protect (fun () -> fill sut__033_ pos len x_3) ()))
   end
-module STMTests = (STM_sequential.Make)(Spec)
+module STMTests = (Ortac_runtime.Make)(Spec)
 let wrapped_init_state () = Spec.init_state
 let ortac_postcond cmd__016_ state__017_ res__018_ =
   let (++) = Ortac_runtime.(++) in
@@ -1862,10 +1863,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                                  }
                              })])))
       | _ -> None
-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:"Varray_circular_spec STM tests"
-          (STMTests.arb_cmds Spec.init_state) agree_prop])
+  QCheck_base_runner.run_tests_main
+    (let count = 1000 in
+     [STMTests.agree_test ~count ~name:"Varray_circular_spec STM tests"
+        wrapped_init_state ortac_postcond])
diff --git a/examples/varray_tests.ml b/examples/varray_tests.ml
@@ -1,5 +1,6 @@
 [@@@ocaml.warning "-26-27"]
 open Varray_spec
+module Ortac_runtime = Ortac_runtime_qcheck_stm
 let inside i s =
   try
     if
@@ -705,7 +706,7 @@ module Spec =
             ((result unit exn),
               (protect (fun () -> fill sut__033_ pos len x_3) ()))
   end
-module STMTests = (STM_sequential.Make)(Spec)
+module STMTests = (Ortac_runtime.Make)(Spec)
 let wrapped_init_state () = Spec.init_state
 let ortac_postcond cmd__016_ state__017_ res__018_ =
   let (++) = Ortac_runtime.(++) in
@@ -1844,10 +1845,8 @@ let ortac_postcond cmd__016_ state__017_ res__018_ =
                                  }
                              })])))
       | _ -> None
-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:"Varray_spec STM tests"
-          (STMTests.arb_cmds Spec.init_state) agree_prop])
+  QCheck_base_runner.run_tests_main
+    (let count = 1000 in
+     [STMTests.agree_test ~count ~name:"Varray_spec STM tests"
+        wrapped_init_state ortac_postcond])
diff --git a/ortac-runtime-qcheck-stm.opam b/ortac-runtime-qcheck-stm.opam
@@ -0,0 +1,40 @@
+# This file is generated by dune, edit dune-project instead
+opam-version: "2.0"
+synopsis: "Runtime support library for Ortac/QCheck-STM-generated code"
+description: """
+The ortac-runtime-qcheck-stm library provides support for the code
+generated by the Ortac/QCheck-STM plugin (provided by the
+ortac-qcheck-stm package).
+
+Ortac (OCaml Runtime Assertion Checking) is a tool to turn
+executable Gospel specifications into code to test they hold.
+"""
+maintainer: ["Nicolas Osborne <[email protected]>"]
+authors: ["Nicolas Osborne <[email protected]>"]
+license: "MIT"
+homepage: "https://github.com/ocaml-gospel/ortac"
+bug-reports: "https://github.com/ocaml-gospel/ortac/issues"
+depends: [
+  "dune" {>= "3.8"}
+  "ocaml" {>= "4.11.0"}
+  "qcheck-stm"
+  "ortac-runtime"
+  "odoc" {with-doc}
+]
+build: [
+  ["dune" "subst"] {dev}
+  [
+    "dune"
+    "build"
+    "-p"
+    name
+    "-j"
+    jobs
+    "--promote-install-files=false"
+    "@install"
+    "@runtest" {with-test}
+    "@doc" {with-doc}
+  ]
+  ["dune" "install" "-p" name "--create-install-files" name]
+]
+dev-repo: "git+https://github.com/ocaml-gospel/ortac.git"
diff --git a/plugins/dune-rules/src/qcheck_stm.ml b/plugins/dune-rules/src/qcheck_stm.ml
@@ -61,7 +61,7 @@ let libraries =
   let k ppf config =
     pf ppf
       "libraries@ %s@ qcheck-stm.stm@ qcheck-stm.sequential@ \
-       qcheck-multicoretests-util@ ortac-runtime"
+       qcheck-multicoretests-util@ ortac-runtime-qcheck-stm"
       config.interface_file
   in
   stanza k

diff --git a/plugins/dune-rules/test/test.t b/plugins/dune-rules/test/test.t
@@ -57,7 +57,7 @@ generated.
     qcheck-stm.stm
     qcheck-stm.sequential
     qcheck-multicoretests-util
-    ortac-runtime)
+    ortac-runtime-qcheck-stm)
    (package my_package)
    (action
     (run
@@ -127,7 +127,7 @@ this fact.
     qcheck-stm.stm
     qcheck-stm.sequential
     qcheck-multicoretests-util
-    ortac-runtime)
+    ortac-runtime-qcheck-stm)
    (package my_package)
    (action
     (run

diff --git a/plugins/qcheck-stm/src/runtime/dune b/plugins/qcheck-stm/src/runtime/dune
@@ -0,0 +1,10 @@
+(library
+ (name ortac_runtime_qcheck_stm)
+ (public_name ortac-runtime-qcheck-stm)
+ (libraries
+  qcheck-core
+  qcheck-core.runner
+  qcheck-stm.stm
+  qcheck-stm.sequential
+  qcheck-multicoretests-util
+  ortac-runtime))
diff --git a/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml b/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml
@@ -0,0 +1,74 @@
+open STM
+include Ortac_runtime
+
+let ( ++ ) a b =
+  match (a, b) with
+  | None, None -> None
+  | Some (_, _), None -> a
+  | None, Some (_, _) -> b
+  | Some (cmd0, terms0), Some (cmd1, terms1) ->
+      assert (cmd0 = cmd1);
+      Some (cmd0, terms0 @ terms1)
+
+module Make (Spec : Spec) = struct
+  open QCheck
+  module Internal = Internal.Make (Spec) [@alert "-internal"]
+
+  let pp_trace ppf trace =
+    let open Fmt in
+    let pp_aux ppf (c, r) = pf ppf "%s : %s" (Spec.show_cmd c) (show_res r) in
+    pf ppf "@[%a@]" (list ~sep:(any "@\n") pp_aux) trace
+
+  let pp_terms ppf err =
+    let open Fmt in
+    let pp_aux ppf (term, l) = pf ppf "@[%a@\n  @[%s@]@]@\n" pp_loc l term in
+    pf ppf "%a" (list ~sep:(any "@\n") pp_aux) err
+
+  let message trace cmd terms =
+    Test.fail_reportf
+      "Gospel specification violation in function %s\n\
+       @;\
+      \  @[%a@]@\n\
+       when executing the following sequence of operations:@\n\
+       @;\
+      \  @[%a@]@." cmd pp_terms terms pp_trace trace
+
+  let rec check_disagree postcond s sut cs =
+    match cs with
+    | [] -> None
+    | c :: cs -> (
+        let res = Spec.run c sut in
+        (* This functor will be called after a modified postcond has been
+           defined, returning a list of 3-plets containing the command, the
+           term and the location *)
+        match postcond c s res with
+        | None -> (
+            let s' = Spec.next_state c s in
+            match check_disagree postcond s' sut cs with
+            | None -> None
+            | Some (rest, cmd, terms) -> Some ((c, res) :: rest, cmd, terms))
+        | Some (cmd, terms) -> Some ([ (c, res) ], cmd, terms))
+
+  let agree_prop wrapped_init_state postcond cs =
+    let _ = wrapped_init_state () in
+    assume (Internal.cmds_ok Spec.init_state cs);
+    let sut = Spec.init_sut () in
+    (* reset system's state *)
+    let res =
+      try Ok (check_disagree postcond Spec.init_state sut cs)
+      with exn -> Error exn
+    in
+    let () = Spec.cleanup sut in
+    let res = match res with Ok res -> res | Error exn -> raise exn in
+    match res with
+    | None -> true
+    | Some (trace, cmd, terms) -> message trace cmd terms
+  (* Test.fail_reportf *)
+  (*   "%a@\n@[@,  when executing this sequence of operations:@]@\n@\n%a@." *)
+  (*   pp_err err pp_trace trace *)
+
+  let agree_test ~count ~name wrapped_init_state postcond =
+    Test.make ~name ~count
+      (Internal.arb_cmds Spec.init_state)
+      (agree_prop wrapped_init_state postcond)
+end
diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml
@@ -922,7 +922,7 @@ let stm include_ config ir =
       (module_binding ~name:(noloc (Some "STMTests"))
          ~expr:
            (pmod_apply
-              (pmod_ident (Ldot (Lident "STM_sequential", "Make") |> noloc))
+              (pmod_ident (Ldot (Lident "Ortac_runtime", "Make") |> noloc))
               (pmod_ident (lident "Spec"))))
   in
   let module_name = Ortac_core.Context.module_name config.context in
@@ -931,16 +931,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
            [
-             Test.make ~count ~name:[%e descr]
-               (STMTests.arb_cmds Spec.init_state)
-               agree_prop;
+             STMTests.agree_test ~count ~name:[%e descr] wrapped_init_state
+               ortac_postcond;
            ])]
   in
   ok
-    ((warn :: open_mod module_name :: ghost_functions)
-    @ [ stm_spec; tests; wrapped_init_state; postcond; agree_prop; call_tests ]
-    )
+    (warn
+     :: open_mod module_name
+     :: [%stri module Ortac_runtime = Ortac_runtime_qcheck_stm]
+     :: ghost_functions
+    @ [ stm_spec; tests; wrapped_init_state; postcond; call_tests ])
diff --git a/plugins/qcheck-stm/test/array_stm_tests.expected.ml b/plugins/qcheck-stm/test/array_stm_tests.expected.ml
@@ -1,5 +1,6 @@
 [@@@ocaml.warning "-26-27"]
 open Array
+module Ortac_runtime = Ortac_runtime_qcheck_stm
 module Spec =
   struct
     open STM
@@ -326,7 +327,7 @@ module Spec =
       | To_list -> Res ((list char), (to_list sut__019_))
       | Mem a_3 -> Res (bool, (mem a_3 sut__019_))
   end
-module STMTests = (STM_sequential.Make)(Spec)
+module STMTests = (Ortac_runtime.Make)(Spec)
 let wrapped_init_state () = Spec.init_state
 let ortac_postcond cmd__008_ state__009_ res__010_ =
   let (++) = Ortac_runtime.(++) in
@@ -1056,10 +1057,8 @@ let ortac_postcond cmd__008_ state__009_ res__010_ =
                        }
                    })])
       | _ -> None
-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:"Array STM tests"
-          (STMTests.arb_cmds Spec.init_state) agree_prop])
+  QCheck_base_runner.run_tests_main
+    (let count = 1000 in
+     [STMTests.agree_test ~count ~name:"Array STM tests" wrapped_init_state
+        ortac_postcond])
diff --git a/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml b/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml
@@ -1,5 +1,6 @@
 [@@@ocaml.warning "-26-27"]
 open Conjunctive_clauses
+module Ortac_runtime = Ortac_runtime_qcheck_stm
 let set_contents c i a_1 =
   try
     Ortac_runtime.Gospelstdlib.List.mapi
@@ -152,7 +153,7 @@ module Spec =
             ((result unit exn),
               (protect (fun () -> set sut__015_ i_1 a_2) ()))
   end
-module STMTests = (STM_sequential.Make)(Spec)
+module STMTests = (Ortac_runtime.Make)(Spec)
 let wrapped_init_state () = Spec.init_state
 let ortac_postcond cmd__006_ state__007_ res__008_ =
   let (++) = Ortac_runtime.(++) in
@@ -276,10 +277,8 @@ let ortac_postcond cmd__006_ state__007_ res__008_ =
                                  }
                              })])))
       | _ -> None
-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:"Conjunctive_clauses STM tests"
-          (STMTests.arb_cmds Spec.init_state) agree_prop])
+  QCheck_base_runner.run_tests_main
+    (let count = 1000 in
+     [STMTests.agree_test ~count ~name:"Conjunctive_clauses STM tests"
+        wrapped_init_state ortac_postcond])