Merge pull request #175 from n-osborne/fix-out-of-scope

Check for out of scope variables.

CHANGES.md

@@ -1,5 +1,7 @@
 # Unreleased
 
+- Check for out of scope variables
+  [\#175](https://github.com/ocaml-gospel/ortac/pull/175)
 - Translate constant integer patterns with a guard testing for equality
   [\#174](https://github.com/ocaml-gospel/ortac/pull/174)
 

plugins/qcheck-stm/doc/index.mld

@@ -228,7 +228,8 @@ File "example_next_state.mli", line 15, characters 13-23:
 Warning: Skipping ensures_not_found_for_next_state: model contents is
          declared as modified by the function but no suitable ensures clause
          was found. Specifications should contain at least one "ensures
-         x.contents = ..." where x is the SUT.
+         x.contents = expr" where x is the SUT and expr can refer to the SUT
+         only under an old operator and can't refer to the returned value.
 ]}
 
 Note that you don't have to rewrite the clause. Maybe it contains information

plugins/qcheck-stm/src/reserr.ml

@@ -25,7 +25,8 @@ type W.kind +=
   | Sut_type_not_specified of string
   | No_models of string
   | No_spec of string
-  | Impossible_term_substitution of [ `Never | `New | `Old | `NotModel ]
+  | Impossible_term_substitution of
+      [ `Never | `New | `Old | `NotModel | `OutOfScope ]
   | Ignored_modifies
   | Ensures_not_found_for_next_state of (string * string)
   | Type_not_supported of string
@@ -129,6 +130,9 @@ let pp_kind ppf kind =
         | `New ->
             "occurrences of the SUT in clauses are not supported above old \
              operator"
+        | `OutOfScope ->
+            "occurrences of returned values that are out of scope in the \
+             next_state function"
       in
       pf ppf "Skipping clause:@ %a" text msg
   | Ignored_modifies ->
@@ -139,7 +143,8 @@ let pp_kind ppf kind =
         "is declared as modified by the function but no suitable ensures \
          clause was found."
         text "Specifications should contain at least one \"ensures x." m text
-        " = ...\" where x is the SUT"
+        " = expr\" where x is the SUT and expr can refer to the SUT only under \
+         an old operator and can't refer to the returned value"
   | Functional_argument f ->
       pf ppf "Skipping %s:@ %a" f text
         "functions are not supported yet as arguments"

plugins/qcheck-stm/src/reserr.mli

@@ -25,7 +25,8 @@ type W.kind +=
   | Sut_type_not_specified of string
   | No_models of string
   | No_spec of string
-  | Impossible_term_substitution of [ `Never | `New | `Old | `NotModel ]
+  | Impossible_term_substitution of
+      [ `Never | `New | `Old | `NotModel | `OutOfScope ]
   | Ignored_modifies
   | Ensures_not_found_for_next_state of (string * string)
   | Type_not_supported of string

plugins/qcheck-stm/src/stm_of_ir.ml

@@ -78,11 +78,11 @@ let ocaml_of_term cfg t =
     always be in a position in which it is applied to one of its model fields.
     Calling [subst_term] with [new_t] and [old_t] as None will check that the
     term does not contain [gos_t] *)
-let subst_term state ~gos_t ?(old_lz = false) ~old_t ?(new_lz = false) ~new_t
-    term =
+let subst_term state ?(out_of_scope = []) ~gos_t ?(old_lz = false) ~old_t
+    ?(new_lz = false) ~new_t term =
   let exception
     ImpossibleSubst of
-      (Gospel.Tterm.term * [ `Never | `New | `Old | `NotModel ])
+      (Gospel.Tterm.term * [ `Never | `New | `Old | `NotModel | `OutOfScope ])
   in
   let rec aux cur_lz cur_t term =
     let open Gospel.Tterm in
@@ -112,6 +112,9 @@ let subst_term state ~gos_t ?(old_lz = false) ~old_t ?(new_lz = false) ~new_t
        access one of its model fields, so we error out *)
     | Tvar { vs_name; _ } when Ident.equal vs_name gos_t ->
         raise (ImpossibleSubst (term, `NotModel))
+    (* Then, we check if the variable is not out_of_scope in the function we are building *)
+    | Tvar { vs_name; _ } when List.exists (Ident.equal vs_name) out_of_scope ->
+        raise (ImpossibleSubst (term, `OutOfScope))
     | Tconst _ -> term
     | Tvar _ -> term
     | Tapp (ls, terms) -> { term with t_node = Tapp (ls, List.map next terms) }
@@ -331,8 +334,8 @@ let next_state_case state config state_ident nb_models value =
     let descriptions =
       List.filter_map
         (fun (i, { model; description }) ->
-          subst_term state ~gos_t:value.sut_var ~old_t:(Some state_ident)
-            ~new_t:None description
+          subst_term ~out_of_scope:value.ret state ~gos_t:value.sut_var
+            ~old_t:(Some state_ident) ~new_t:None description
           >>= ocaml_of_term config
           |> to_option
           |> Option.map (fun description -> (i, model, description)))

plugins/qcheck-stm/test/all_warnings.mli

@@ -58,3 +58,10 @@ val record_not_model_field : 'a t -> bool
 
 val return_tuple : 'a t -> 'a * bool
 (*@ (a, b) = return_tuple t *)
+
+val term_refer_to_returned_value_next_state : 'a t -> 'a option
+(*@ o = term_refer_to_returned_value_next_state t
+    modifies t.contents
+    ensures t.contents = match o with
+                        | None -> old t.contents
+                        | Some _ -> old t.contents *)

plugins/qcheck-stm/test/all_warnings_errors.expected

@@ -58,7 +58,16 @@ File "all_warnings.mli", line 37, characters 13-23:
 Warning: Skipping ensures_not_found_for_next_state: model contents is
          declared as modified by the function but no suitable ensures clause
          was found. Specifications should contain at least one "ensures
-         x.contents = ..." where x is the SUT.
+         x.contents = expr" where x is the SUT and expr can refer to the SUT
+         only under an old operator and can't refer to the returned value.
+File "all_warnings.mli", line 64, characters 13-23:
+64 |     modifies t.contents
+                  ^^^^^^^^^^
+Warning: Skipping term_refer_to_returned_value_next_state: model contents is
+         declared as modified by the function but no suitable ensures clause
+         was found. Specifications should contain at least one "ensures
+         x.contents = expr" where x is the SUT and expr can refer to the SUT
+         only under an old operator and can't refer to the returned value.
 File "all_warnings.mli", line 53, characters 16-54:
 53 |     ensures b = forall a. List.mem a t.contents -> p a *)
                      ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^