Merge pull request #146 from shym/pure

Add pure OCaml and ghost functions to the context

plugins/qcheck-stm/src/config.ml

@@ -83,6 +83,18 @@ let init path init_sut sut_str =
     assert (List.length env = 1);
     let namespace = List.hd env in
     let context = Context.init module_name namespace in
+    let add ctx s =
+      (* we add to the context the pure OCaml values and the functions and
+         predicates with a body *)
+      match s.Tast.sig_desc with
+      | Sig_val ({ vd_name; vd_spec = Some { sp_pure = true; _ }; _ }, _) ->
+          let ls = Context.get_ls ctx [ vd_name.id_str ] in
+          Context.add_function ls vd_name.id_str ctx
+      | Sig_function { fun_ls; fun_def = Some _; _ } ->
+          Context.add_function fun_ls fun_ls.ls_name.id_str ctx
+      | _ -> ctx
+    in
+    let context = List.fold_left add context sigs in
     let* sut_core_type = sut_core_type sut_str
     and* init_sut = init_sut_from_string init_sut in
     ok (sigs, { context; sut_core_type; init_sut })

plugins/qcheck-stm/test/record.ml

@@ -1,4 +1,6 @@
 type t = { c : int }
 
 let make i = { c = i }
+let plus1 i = i + 1
+let plus2 i = i + 2
 let get { c } = c

plugins/qcheck-stm/test/record.mli

@@ -6,8 +6,21 @@ val make : int -> t
 (*@ r = make i
     ensures r.value = i *)
 
+val plus1 : int -> int
+(*@ i1 = plus1 i
+    ensures i1 = i + 1 *)
+
+(*@ function plus1 (i: integer) : integer = i + 1 *)
+
+val plus2 : int -> int
+(*@ i2 = plus2 i
+    pure
+    ensures i2 = i + 2 *)
+
 val get : t -> int
 (*@ i = get r
     pure
     ensures i = r.value
-    ensures i = r.c *)
+    ensures i = r.c
+    ensures plus1 i = i + 1
+    ensures plus2 i = i + 2 *)

plugins/qcheck-stm/test/record_errors.expected

@@ -1,5 +1,13 @@
-File "record.mli", line 13, characters 16-19:
-13 |     ensures i = r.c *)
+File "record.mli", line 9, characters 12-22:
+9 | val plus1 : int -> int
+                ^^^^^^^^^^
+Warning: Skipping plus1: functions with no SUT argument cannot be tested.
+File "record.mli", line 15, characters 12-22:
+15 | val plus2 : int -> int
+                 ^^^^^^^^^^
+Warning: Skipping plus2: functions with no SUT argument cannot be tested.
+File "record.mli", line 24, characters 16-19:
+24 |     ensures i = r.c
                      ^^^
 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

@@ -1,4 +1,7 @@
 open Record
+let plus1_1 i =
+  Ortac_runtime.Gospelstdlib.(+) i
+    (Ortac_runtime.Gospelstdlib.integer_of_int 1)
 module Spec =
   struct
     open STM
@@ -11,8 +14,8 @@ module Spec =
     type nonrec state = {
       value: Ortac_runtime.integer }
     let init_state =
-      let i_1 = 42 in
-      { value = (Ortac_runtime.Gospelstdlib.integer_of_int i_1) }
+      let i_2 = 42 in
+      { value = (Ortac_runtime.Gospelstdlib.integer_of_int i_2) }
     let init_sut () = make 42
     let cleanup _ = ()
     let arb_cmd _ =
@@ -24,9 +27,19 @@ module Spec =
     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
-      | (Get, Res ((Int, _), i)) ->
-          (Ortac_runtime.Gospelstdlib.integer_of_int i) =
-            (Lazy.force new_state__007_).value
+      | (Get, Res ((Int, _), i_1)) ->
+          ((Ortac_runtime.Gospelstdlib.integer_of_int i_1) =
+             (Lazy.force new_state__007_).value)
+            &&
+            (((plus1_1 (Ortac_runtime.Gospelstdlib.integer_of_int i_1)) =
+                (Ortac_runtime.Gospelstdlib.(+)
+                   (Ortac_runtime.Gospelstdlib.integer_of_int i_1)
+                   (Ortac_runtime.Gospelstdlib.integer_of_int 1)))
+               &&
+               ((Ortac_runtime.Gospelstdlib.integer_of_int (plus2 i_1)) =
+                  (Ortac_runtime.Gospelstdlib.(+)
+                     (Ortac_runtime.Gospelstdlib.integer_of_int i_1)
+                     (Ortac_runtime.Gospelstdlib.integer_of_int 2))))
       | _ -> true
     let run cmd__010_ sut__011_ =
       match cmd__010_ with | Get -> Res (int, (get sut__011_))