Merge pull request #144 from n-osborne/fix_init_state

Reject clauses that involves returned `sut` for `init_state`

plugins/qcheck-stm/src/ir.ml

@@ -40,6 +40,7 @@ type value = {
 
 type init_state = {
   arguments : (Tast.lb_arg * Ppxlib.expression) list;
+  returned_sut : Ident.t;
   descriptions : new_state_formulae list;
 }
 

plugins/qcheck-stm/src/ir_of_gospel.ml

@@ -331,7 +331,7 @@ let init_state config state sigs =
     match ty.ptyp_desc with Ptyp_arrow (_, _, r) -> return_type r | _ -> ty
   in
   let ret_sut = Cfg.is_sut config (return_type value.vd_type) in
-  let* sut =
+  let* returned_sut =
     List.find_map
       (function Lnone vs when ret_sut -> Some vs.vs_name | _ -> None)
       spec.sp_ret
@@ -342,7 +342,7 @@ let init_state config state sigs =
                   (Fmt.str "%a" Gospel.Identifier.Ident.pp value.Tast.vd_name)),
              value.vd_loc )
   in
-  let is_t vs = Ident.equal sut vs.vs_name in
+  let is_t vs = Ident.equal returned_sut vs.vs_name in
   let descriptions =
     get_state_description_with_index is_t state spec |> List.map snd
   in
@@ -367,7 +367,7 @@ let init_state config state sigs =
               (No_appropriate_specifications (fct_str, missing_models)),
             spec.sp_loc )
   in
-  ok (fct_str, Ir.{ arguments; descriptions })
+  ok (fct_str, Ir.{ arguments; returned_sut; descriptions })
 
 let signature config init_fct state sigs =
   List.filter_map (sig_item config init_fct state) sigs |> Reserr.promote

plugins/qcheck-stm/src/reserr.ml

@@ -25,7 +25,7 @@ type W.kind +=
   | Sut_type_not_specified of string
   | No_models of string
   | No_spec of string
-  | Impossible_term_substitution of [ `New | `Old | `NotModel ]
+  | Impossible_term_substitution of [ `Never | `New | `Old | `NotModel ]
   | Ignored_modifies
   | Ensures_not_found_for_next_state of (string * string)
   | Type_not_supported of string
@@ -117,6 +117,10 @@ let pp_kind ppf kind =
         | `NotModel ->
             "occurrences of the SUT in clauses are only supported to access \
              its model fields"
+        (* The  [`Never] case is used when generating [init_state] *)
+        | `Never ->
+            "impossible to define the initial value of the model with a \
+             recursive expression"
         (* The following cases should not be reported to the user at the moment
            (because they should be caught at some other points) *)
         | `Old ->

plugins/qcheck-stm/src/reserr.mli

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

plugins/qcheck-stm/src/stm_of_ir.ml

@@ -88,11 +88,14 @@ let ocaml_of_term cfg t =
     occurrences of [gos_t] with [new_t] or [old_t] depending on whether the
     occurrence appears above or under the [old] operator, adding a [Lazy.force]
     if the corresponding [xxx_lz] is [true] (defaults to [false]). [gos_t] must
-    always be in a position in which it is applied to one of its model fields *)
+    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 exception
-    ImpossibleSubst of (Gospel.Tterm.term * [ `New | `Old | `NotModel ])
+    ImpossibleSubst of
+      (Gospel.Tterm.term * [ `Never | `New | `Old | `NotModel ])
   in
   let rec aux cur_lz cur_t term =
     let open Gospel.Tterm in
@@ -109,7 +112,12 @@ let subst_term state ~gos_t ?(old_lz = false) ~old_t ?(new_lz = false) ~new_t
               { term with t_node = Tfield (t, ls) }
           | None ->
               raise
-                (ImpossibleSubst (subt, if cur_t = new_t then `New else `Old))
+                (ImpossibleSubst
+                   ( subt,
+                     match (new_t, old_t) with
+                     | None, None -> `Never
+                     | None, _ -> `New
+                     | _, _ -> `Old ))
         else
           (* case x.f where f is _not_ a model field *)
           raise (ImpossibleSubst (term, `NotModel))
@@ -707,7 +715,11 @@ let init_state config ir =
   in
   let open Reserr in
   let translate_field_desc Ir.{ model; description } =
-    let* desc = ocaml_of_term config description in
+    let* desc =
+      subst_term ir.state ~gos_t:ir.init_state.returned_sut ~old_t:None
+        ~new_t:None description
+      >>= ocaml_of_term config
+    in
     ok (model, desc)
   in
   let* fields = map translate_field_desc ir.Ir.init_state.descriptions in

plugins/qcheck-stm/test/test_errors.t

@@ -189,3 +189,21 @@ It checks the number of arguments in the function call:
   $ ortac qcheck-stm foo.mli "make 42 73" "int t"
   Error: Error in INIT expression make 42 73: mismatch in the number of
          arguments between the INIT expression and the function specification.
+We shouldn't be able to define a model by itsef in the `make` function:
+  $ cat > foo.mli << EOF
+  > type 'a t
+  > (*@ mutable model value : 'a list *)
+  > val make : 'a -> 'a t
+  > (*@ t = make a
+  >     requires true
+  >     ensures t.value = t.value *)
+  > EOF
+  $ ortac qcheck-stm foo.mli "make 42" "int t"
+  Error: Unsupported INIT function: the specification of the function called in
+         the INIT expression does not provide a translatable specification for
+         the following field of the model: value.
+  File "foo.mli", line 6, characters 22-23:
+  6 |     ensures t.value = t.value *)
+                            ^
+  Warning: Skipping clause: impossible to define the initial value of the model
+           with a recursive expression.