From e5e7fd14d8abaf978c9d7a927a266b53a49a90cc Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Tue, 7 Nov 2023 15:37:37 +0100 Subject: [PATCH 1/5] Add a `OutOfScope case for Impossible_term_substitution --- plugins/qcheck-stm/src/reserr.ml | 6 +++++- plugins/qcheck-stm/src/reserr.mli | 3 ++- plugins/qcheck-stm/src/stm_of_ir.ml | 2 +- 3 files changed, 8 insertions(+), 3 deletions(-) diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml index 25a2e935..b9e49a02 100644 --- a/plugins/qcheck-stm/src/reserr.ml +++ b/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 -> diff --git a/plugins/qcheck-stm/src/reserr.mli b/plugins/qcheck-stm/src/reserr.mli index 039da133..93bed454 100644 --- a/plugins/qcheck-stm/src/reserr.mli +++ b/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 diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml index b6da1c7f..1438b347 100644 --- a/plugins/qcheck-stm/src/stm_of_ir.ml +++ b/plugins/qcheck-stm/src/stm_of_ir.ml @@ -82,7 +82,7 @@ let subst_term state ~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 From 0c9fe93a44b41209ffa74a72a314fd56b2f49657 Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Tue, 7 Nov 2023 15:41:03 +0100 Subject: [PATCH 2/5] Check for out of scope variables when building `next_state` Returned values are out of scope in this function. The error message will not be printed to the user as we forget about why we counldn't use a term when looking for one suitable for `next_state`. (See the use of `to_option` in `next_state_case`) --- plugins/qcheck-stm/src/stm_of_ir.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml index 1438b347..b224f55f 100644 --- a/plugins/qcheck-stm/src/stm_of_ir.ml +++ b/plugins/qcheck-stm/src/stm_of_ir.ml @@ -78,8 +78,8 @@ 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 | `OutOfScope ]) @@ -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))) From a5113220494159ec37da1ee7e35c0f0cddf40b7d Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Tue, 7 Nov 2023 15:45:12 +0100 Subject: [PATCH 3/5] Add some tests. Fixes #171 Non compiling code is not generated anymore, but the user doesn't know why `next_state` was not generated. --- plugins/qcheck-stm/test/all_warnings.mli | 7 +++++++ plugins/qcheck-stm/test/all_warnings_errors.expected | 7 +++++++ 2 files changed, 14 insertions(+) diff --git a/plugins/qcheck-stm/test/all_warnings.mli b/plugins/qcheck-stm/test/all_warnings.mli index 1aa5e1e4..64b004cb 100644 --- a/plugins/qcheck-stm/test/all_warnings.mli +++ b/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 *) diff --git a/plugins/qcheck-stm/test/all_warnings_errors.expected b/plugins/qcheck-stm/test/all_warnings_errors.expected index e499965a..693022e9 100644 --- a/plugins/qcheck-stm/test/all_warnings_errors.expected +++ b/plugins/qcheck-stm/test/all_warnings_errors.expected @@ -59,6 +59,13 @@ 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. +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 = ..." where x is the SUT. File "all_warnings.mli", line 53, characters 16-54: 53 | ensures b = forall a. List.mem a t.contents -> p a *) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ From ceef18186ab65414d9a26179a1349606607b9051 Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Wed, 8 Nov 2023 10:30:05 +0100 Subject: [PATCH 4/5] Add information to Ensures_not_found_for_next_state error message --- plugins/qcheck-stm/doc/index.mld | 3 ++- plugins/qcheck-stm/src/reserr.ml | 3 ++- plugins/qcheck-stm/test/all_warnings_errors.expected | 6 ++++-- 3 files changed, 8 insertions(+), 4 deletions(-) diff --git a/plugins/qcheck-stm/doc/index.mld b/plugins/qcheck-stm/doc/index.mld index 1acba2d8..435f5df8 100644 --- a/plugins/qcheck-stm/doc/index.mld +++ b/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 diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml index b9e49a02..880f113e 100644 --- a/plugins/qcheck-stm/src/reserr.ml +++ b/plugins/qcheck-stm/src/reserr.ml @@ -143,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" diff --git a/plugins/qcheck-stm/test/all_warnings_errors.expected b/plugins/qcheck-stm/test/all_warnings_errors.expected index 693022e9..81df1242 100644 --- a/plugins/qcheck-stm/test/all_warnings_errors.expected +++ b/plugins/qcheck-stm/test/all_warnings_errors.expected @@ -58,14 +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 = ..." 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 53, characters 16-54: 53 | ensures b = forall a. List.mem a t.contents -> p a *) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ From cc86d616287cee57da696d1b22b232e8871cb0de Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Thu, 9 Nov 2023 10:40:28 +0100 Subject: [PATCH 5/5] Update CHANGES.md --- CHANGES.md | 2 ++ 1 file changed, 2 insertions(+) diff --git a/CHANGES.md b/CHANGES.md index f2f8b7ef..f7a660d9 100644 --- a/CHANGES.md +++ b/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)