Filter out functions which return tuples

Replace an internal error by a proper warning.
Still does not generate test for functions returning tuples but prepare
the way by storing a list of returned values in the intermediary
representation

Co-authored-by: Samuel Hym <samuel.hym@rustyne.lautre.net>

plugins/qcheck-stm/src/ir.ml

@@ -32,7 +32,7 @@ type value = {
   sut_var : Ident.t;
   args : (Ppxlib.core_type * Ident.t option) list;
       (* arguments of unit types can be nameless *)
-  ret : Ident.t option;
+  ret : Ident.t list;
   next_state : next_state;
   precond : Tterm.term list;
   postcond : postcond;

plugins/qcheck-stm/src/ir_of_gospel.ml

@@ -10,7 +10,7 @@ let constant_test vd =
       (Constant_value (Fmt.str "%a" Ident.pp vd.vd_name), vd.vd_loc) |> error
   | _ -> ok ()
 
-let higher_order_test vd =
+let no_functional_arg_or_returned_tuple vd =
   let open Reserr in
   let open Ppxlib in
   let rec contains_arrow ty =
@@ -27,6 +27,7 @@ let higher_order_test vd =
     | Ptyp_arrow (_, l, r) ->
         let* _ = contains_arrow l in
         aux r
+    | Ptyp_tuple _ -> error (Returned_tuple vd.vd_name.id_str, ty.ptyp_loc)
     | _ -> ok ()
   in
   aux vd.vd_type
@@ -186,19 +187,22 @@ let postcond spec =
 
 let val_desc config state vd =
   let open Reserr in
-  let* () = constant_test vd and* () = higher_order_test vd in
+  let* () = constant_test vd and* () = no_functional_arg_or_returned_tuple vd in
   let* inst = ty_var_substitution config vd
   and* spec =
     of_option ~default:(No_spec vd.vd_name.id_str, vd.vd_loc) vd.vd_spec
   in
   let* sut, args = split_args config vd spec.sp_args
   and* ret =
-    match spec.sp_ret with
-    | [ Lnone vs ] -> ok (Some vs.vs_name)
-    | [] -> ok None
-    | Lghost vs :: _ | _ :: Lghost vs :: _ ->
-        error (Ghost_values (vd.vd_name.id_str, `Ret), vs.vs_name.id_loc)
-    | _ -> failwith "shouldn't happen (more than one return OCaml value)"
+    let p = function
+      | Lnone vs -> ok vs.vs_name
+      | Lghost vs ->
+          error (Ghost_values (vd.vd_name.id_str, `Ret), vs.vs_name.id_loc)
+      | _ ->
+          failwith
+            "shouldn't happen (only non labelled and ghost value are returned)"
+    in
+    List.map p spec.sp_ret |> sequence
   in
   let* next_state = next_state sut state spec in
   let postcond = postcond spec in

plugins/qcheck-stm/src/reserr.ml

@@ -31,6 +31,7 @@ type W.kind +=
   | Type_not_supported of string
   | Impossible_init_state_generation of init_state_error
   | Functional_argument of string
+  | Returned_tuple of string
   | Ghost_values of (string * [ `Arg | `Ret ])
   | Incompatible_sut of string
 
@@ -40,7 +41,7 @@ let level kind =
   | Multiple_sut_arguments _ | Incompatible_type _ | No_spec _
   | Impossible_term_substitution _ | Ignored_modifies
   | Ensures_not_found_for_next_state _ | Type_not_supported _
-  | Functional_argument _ | Ghost_values _ ->
+  | Functional_argument _ | Returned_tuple _ | Ghost_values _ ->
       W.Warning
   | No_sut_type _ | No_init_function _ | Syntax_error_in_type _
   | Sut_type_not_supported _ | Type_not_supported_for_sut_parameter _
@@ -136,6 +137,9 @@ let pp_kind ppf kind =
   | Functional_argument f ->
       pf ppf "Skipping %s:@ %a" f text
         "functions are not supported yet as arguments"
+  | Returned_tuple f ->
+      pf ppf "Skipping %s:@ %a" f text
+        "functions returning tuples are not supported yet"
   | Ghost_values (id, k) ->
       pf ppf "Skipping %s:@ %a%a%a" id text "functions with a ghost " text
         (match k with `Arg -> "argument" | `Ret -> "returned value")

plugins/qcheck-stm/src/reserr.mli

@@ -31,6 +31,7 @@ type W.kind +=
   | Type_not_supported of string
   | Impossible_init_state_generation of init_state_error
   | Functional_argument of string
+  | Returned_tuple of string
   | Ghost_values of (string * [ `Arg | `Ret ])
   | Incompatible_sut of string
 

plugins/qcheck-stm/src/stm_of_ir.ml

@@ -460,10 +460,14 @@ let postcond_case config state idx state_ident new_state_ident value =
     in
     let pat_ret =
       match value.ret with
-      | None ->
+      | [] ->
           if may_raise_exception value then pvar (str_of_ident res_default)
           else ppat_any
-      | Some id -> pvar (str_of_ident id)
+      | [ id ] -> pvar (str_of_ident id)
+      | _ ->
+          failwith
+            "shouldn't happen (functions returning tuples are filtered out \
+             before)"
     in
     ok
       (ppat_construct (lident "Res")
@@ -487,10 +491,14 @@ let postcond_case config state idx state_ident new_state_ident value =
   in
   let res, pat_ret =
     match value.ret with
-    | None -> (evar (str_of_ident res_default), ppat_any)
-    | Some id ->
+    | [] -> (evar (str_of_ident res_default), ppat_any)
+    | [ id ] ->
         let id = str_of_ident id in
         (evar id, pvar id)
+    | _ ->
+        failwith
+          "shouldn't happen (functions returning tuples are filtered out \
+           before)"
   in
   let* rhs =
     if may_raise_exception value then

plugins/qcheck-stm/test/all_warnings.mli

@@ -55,3 +55,6 @@ val unsupported_quantification : 'a t -> bool
 val record_not_model_field : 'a t -> bool
 (*@ b = record_not_model_field t
     requires Array.length t.v > 0 *)
+
+val return_tuple : 'a t -> 'a * bool
+(*@ (a, b) = return_tuple t *)

plugins/qcheck-stm/test/all_warnings_errors.expected

@@ -47,6 +47,11 @@ File "all_warnings.mli", line 49, characters 6-7:
            ^
 Warning: Skipping ghost_returned_value: functions with a ghost returned value
          are not supported.
+File "all_warnings.mli", line 59, characters 27-36:
+59 | val return_tuple : 'a t -> 'a * bool
+                                ^^^^^^^^^
+Warning: Skipping return_tuple: functions returning tuples are not supported
+         yet.
 File "all_warnings.mli", line 37, characters 13-23:
 37 |     modifies t.contents *)
                   ^^^^^^^^^^