From 8164e85e5e8f444bd4fb843a388099f6e9c04cd7 Mon Sep 17 00:00:00 2001 From: Nicolas Osborne Date: Wed, 21 Feb 2024 12:10:05 +0100 Subject: [PATCH] wip --- examples/lwt_dllist_tests.ml | 16 +++---- examples/varray_circular_tests.ml | 42 +++++++++--------- examples/varray_tests.ml | 42 +++++++++--------- plugins/qcheck-stm/src/ir.ml | 16 ++++++- plugins/qcheck-stm/src/ir_of_gospel.ml | 21 ++++++++- plugins/qcheck-stm/src/reserr.ml | 10 ++++- plugins/qcheck-stm/src/reserr.mli | 1 + .../src/runtime/ortac_runtime_qcheck_stm.ml | 38 ++++++++++------ plugins/qcheck-stm/src/stm_of_ir.ml | 43 ++++++++++++++++++- .../test/array_stm_tests.expected.ml | 28 ++++++------ .../conjunctive_clauses_stm_tests.expected.ml | 4 +- .../test/hashtbl_stm_tests.expected.ml | 12 +++--- .../test/invariants_stm_tests.expected.ml | 2 +- .../test/record_stm_tests.expected.ml | 6 +-- .../qcheck-stm/test/ref_stm_tests.expected.ml | 2 +- 15 files changed, 186 insertions(+), 97 deletions(-) diff --git a/examples/lwt_dllist_tests.ml b/examples/lwt_dllist_tests.ml index 867109ab..8ea259e2 100644 --- a/examples/lwt_dllist_tests.ml +++ b/examples/lwt_dllist_tests.ml @@ -335,7 +335,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ = then None else Some - ("is_empty", + (None, "is_empty", [("b <-> s.contents = Sequence.empty", { Ortac_runtime.start = @@ -383,7 +383,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ = then None else Some - ("length", + (None, "length", [("l = Sequence.length s.contents", { Ortac_runtime.start = @@ -440,7 +440,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ = then None else Some - ("take_l", + (None, "take_l", [("if old s.contents = Sequence.empty\n then false\n else a = Sequence.hd (old s.contents)", { Ortac_runtime.start = @@ -492,7 +492,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ = then None else Some - ("take_l", + (None, "take_l", [("old s.contents = Sequence.empty = s.contents", { Ortac_runtime.start = @@ -552,7 +552,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ = then None else Some - ("take_r", + (None, "take_r", [("if old s.contents = Sequence.empty\n then false\n else a = (old s.contents)[Sequence.length (old s.contents) - 1]", { Ortac_runtime.start = @@ -604,7 +604,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ = then None else Some - ("take_r", + (None, "take_r", [("old s.contents = Sequence.empty = s.contents", { Ortac_runtime.start = @@ -656,7 +656,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ = then None else Some - ("take_opt_l", + (None, "take_opt_l", [("old s.contents = match o with\n | None -> Sequence.empty\n | Some a -> Sequence.cons a s.contents", { Ortac_runtime.start = @@ -707,7 +707,7 @@ let ortac_postcond cmd__005_ state__006_ res__007_ = then None else Some - ("take_opt_r", + (None, "take_opt_r", [("old s.contents = match o with\n | None -> Sequence.empty\n | Some a -> Sequence.snoc s.contents a", { Ortac_runtime.start = diff --git a/examples/varray_circular_tests.ml b/examples/varray_circular_tests.ml index 50ebc7a0..524a6026 100644 --- a/examples/varray_circular_tests.ml +++ b/examples/varray_circular_tests.ml @@ -759,7 +759,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_back", + (None, "pop_back", [("if old t.contents = Sequence.empty\n then false\n else proj x = (old t.contents)[Sequence.length (old t.contents) - 1]", { Ortac_runtime.start = @@ -811,7 +811,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_back", + (None, "pop_back", [("t.contents = old t.contents = Sequence.empty", { Ortac_runtime.start = @@ -868,7 +868,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_front", + (None, "pop_front", [("if old t.contents = Sequence.empty\n then false\n else proj x = Sequence.hd (old t.contents)", { Ortac_runtime.start = @@ -920,7 +920,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_front", + (None, "pop_front", [("t.contents = old t.contents = Sequence.empty", { Ortac_runtime.start = @@ -976,7 +976,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("insert_at", + ((Some (Res (unit, ()))), "insert_at", [("0 <= i <= Sequence.length t.contents", { Ortac_runtime.start = @@ -1038,7 +1038,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("insert_at", + ((Some (Res (unit, ()))), "insert_at", [("0 <= i <= Sequence.length t.contents", { Ortac_runtime.start = @@ -1086,7 +1086,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_at", + (None, "pop_at", [("inside i t.contents", { Ortac_runtime.start = @@ -1140,7 +1140,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_at", + (None, "pop_at", [("(proj x) = old t.contents[i]", { Ortac_runtime.start = @@ -1195,7 +1195,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_at", + (None, "pop_at", [("inside i t.contents", { Ortac_runtime.start = @@ -1243,7 +1243,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("delete_at", + ((Some (Res (unit, ()))), "delete_at", [("inside i t.contents", { Ortac_runtime.start = @@ -1300,7 +1300,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("delete_at", + ((Some (Res (unit, ()))), "delete_at", [("Sequence.length t.contents = Sequence.length (old t.contents) - 1", { Ortac_runtime.start = @@ -1355,7 +1355,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("delete_at", + ((Some (Res (unit, ()))), "delete_at", [("inside i t.contents", { Ortac_runtime.start = @@ -1403,7 +1403,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("get", + (None, "get", [("inside i t.contents", { Ortac_runtime.start = @@ -1457,7 +1457,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("get", + (None, "get", [("(proj x) = t.contents[i]", { Ortac_runtime.start = @@ -1512,7 +1512,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("get", + (None, "get", [("inside i t.contents", { Ortac_runtime.start = @@ -1560,7 +1560,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("set", + ((Some (Res (unit, ()))), "set", [("inside i t.contents", { Ortac_runtime.start = @@ -1616,7 +1616,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("set", + ((Some (Res (unit, ()))), "set", [("inside i t.contents", { Ortac_runtime.start = @@ -1664,7 +1664,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("length", + (None, "length", [("l = Sequence.length t.contents", { Ortac_runtime.start = @@ -1712,7 +1712,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("is_empty", + (None, "is_empty", [("b <-> t.contents = Sequence.empty", { Ortac_runtime.start = @@ -1775,7 +1775,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("fill", + ((Some (Res (unit, ()))), "fill", [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents", { Ortac_runtime.start = @@ -1847,7 +1847,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("fill", + ((Some (Res (unit, ()))), "fill", [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents", { Ortac_runtime.start = diff --git a/examples/varray_tests.ml b/examples/varray_tests.ml index 9f3a22e4..f34c257f 100644 --- a/examples/varray_tests.ml +++ b/examples/varray_tests.ml @@ -759,7 +759,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_back", + (None, "pop_back", [("if old t.contents = Sequence.empty\n then false\n else proj x = (old t.contents)[Sequence.length (old t.contents) - 1]", { Ortac_runtime.start = @@ -811,7 +811,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_back", + (None, "pop_back", [("t.contents = old t.contents = Sequence.empty", { Ortac_runtime.start = @@ -868,7 +868,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_front", + (None, "pop_front", [("if old t.contents = Sequence.empty\n then false\n else proj x = Sequence.hd (old t.contents)", { Ortac_runtime.start = @@ -920,7 +920,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_front", + (None, "pop_front", [("t.contents = old t.contents = Sequence.empty", { Ortac_runtime.start = @@ -976,7 +976,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("insert_at", + ((Some (Res (unit, ()))), "insert_at", [("0 <= i <= Sequence.length t.contents", { Ortac_runtime.start = @@ -1036,7 +1036,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("insert_at", + ((Some (Res (unit, ()))), "insert_at", [("0 <= i <= Sequence.length t.contents", { Ortac_runtime.start = @@ -1084,7 +1084,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_at", + (None, "pop_at", [("inside i t.contents", { Ortac_runtime.start = @@ -1136,7 +1136,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_at", + (None, "pop_at", [("(proj x) = old t.contents[i]", { Ortac_runtime.start = @@ -1189,7 +1189,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("pop_at", + (None, "pop_at", [("inside i t.contents", { Ortac_runtime.start = @@ -1237,7 +1237,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("delete_at", + ((Some (Res (unit, ()))), "delete_at", [("inside i t.contents", { Ortac_runtime.start = @@ -1292,7 +1292,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("delete_at", + ((Some (Res (unit, ()))), "delete_at", [("Sequence.length t.contents = Sequence.length (old t.contents) - 1", { Ortac_runtime.start = @@ -1345,7 +1345,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("delete_at", + ((Some (Res (unit, ()))), "delete_at", [("inside i t.contents", { Ortac_runtime.start = @@ -1393,7 +1393,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("get", + (None, "get", [("inside i t.contents", { Ortac_runtime.start = @@ -1445,7 +1445,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("get", + (None, "get", [("(proj x) = t.contents[i]", { Ortac_runtime.start = @@ -1498,7 +1498,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("get", + (None, "get", [("inside i t.contents", { Ortac_runtime.start = @@ -1546,7 +1546,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("set", + ((Some (Res (unit, ()))), "set", [("inside i t.contents", { Ortac_runtime.start = @@ -1600,7 +1600,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("set", + ((Some (Res (unit, ()))), "set", [("inside i t.contents", { Ortac_runtime.start = @@ -1648,7 +1648,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("length", + (None, "length", [("l = Sequence.length t.contents", { Ortac_runtime.start = @@ -1696,7 +1696,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("is_empty", + (None, "is_empty", [("b <-> t.contents = Sequence.empty", { Ortac_runtime.start = @@ -1759,7 +1759,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("fill", + ((Some (Res (unit, ()))), "fill", [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents", { Ortac_runtime.start = @@ -1829,7 +1829,7 @@ let ortac_postcond cmd__016_ state__017_ res__018_ = then None else Some - ("fill", + ((Some (Res (unit, ()))), "fill", [("0 <= pos /\\ 0 <= len /\\ pos + len < Sequence.length t.contents", { Ortac_runtime.start = diff --git a/plugins/qcheck-stm/src/ir.ml b/plugins/qcheck-stm/src/ir.ml index 92a956bf..0e54918f 100644 --- a/plugins/qcheck-stm/src/ir.ml +++ b/plugins/qcheck-stm/src/ir.ml @@ -45,6 +45,7 @@ type value = { args : (Ppxlib.core_type * Ident.t option) list; (* arguments of unit types can be nameless *) ret : Ident.t list; + ret_values : term list list; next_state : next_state; precond : Tterm.term list; postcond : postcond; @@ -63,8 +64,19 @@ let get_return_type value = in aux value.ty -let value id ty inst sut_var args ret next_state precond postcond = - { id; ty; inst; sut_var; args; ret; next_state; precond; postcond } +let value id ty inst sut_var args ret ret_values next_state precond postcond = + { + id; + ty; + inst; + sut_var; + args; + ret; + ret_values; + next_state; + precond; + postcond; + } type t = { state : (Ident.t * Ppxlib.core_type) list; diff --git a/plugins/qcheck-stm/src/ir_of_gospel.ml b/plugins/qcheck-stm/src/ir_of_gospel.ml index 9627a04f..a2a99fec 100644 --- a/plugins/qcheck-stm/src/ir_of_gospel.ml +++ b/plugins/qcheck-stm/src/ir_of_gospel.ml @@ -167,6 +167,22 @@ let next_state sut state spec = in ok Ir.{ formulae; modifies } +let returned_value spec ret = + let open Tterm in + let is_ret vs = + let open Symbols in + Ident.equal ret vs.vs_name + in + let rec pred t = + match t.t_node with + | Tapp (ls, [ { t_node = Tvar vs; _ }; right ]) + when Symbols.(ls_equal ps_equ ls) && is_ret vs -> + [ Ir.term_val spec right ] + | Tbinop ((Tand | Tand_asym), l, r) -> pred l @ pred r + | _ -> [] + in + List.concat_map pred spec.sp_post + let postcond spec = let normal = List.mapi (fun i x -> (i, Ir.term_val spec x)) spec.sp_post and exceptional = @@ -216,10 +232,11 @@ let val_desc config state vd = in List.map p spec.sp_ret |> sequence in + let ret_values = List.map (returned_value spec) ret in let* next_state = next_state sut state spec in let postcond = postcond spec in - Ir.value vd.vd_name vd.vd_type inst sut args ret next_state spec.sp_pre - postcond + Ir.value vd.vd_name vd.vd_type inst sut args ret ret_values next_state + spec.sp_pre postcond |> ok let sig_item config init_fct state s = diff --git a/plugins/qcheck-stm/src/reserr.ml b/plugins/qcheck-stm/src/reserr.ml index 50c004c6..7885521f 100644 --- a/plugins/qcheck-stm/src/reserr.ml +++ b/plugins/qcheck-stm/src/reserr.ml @@ -35,6 +35,7 @@ type W.kind += | Returned_tuple of string | Ghost_values of (string * [ `Arg | `Ret ]) | Incompatible_sut of string + | Incomplete_ret_val_computation of string let level kind = match kind with @@ -42,7 +43,8 @@ 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 _ | Returned_tuple _ | Ghost_values _ -> + | Functional_argument _ | Returned_tuple _ | Ghost_values _ + | Incomplete_ret_val_computation _ -> W.Warning | No_sut_type _ | No_init_function _ | Syntax_error_in_type _ | Sut_type_not_supported _ | Type_not_supported_for_sut_parameter _ @@ -216,6 +218,12 @@ let pp_kind ppf kind = "the declaration of the SUT type is incompatible with the configured \ one: " t + | Incomplete_ret_val_computation fct -> + pf ppf + "Incomplete computation of the returned value in the specification in \ + %s. Failure message won't be able to display the expected returned \ + value." + fct | _ -> W.pp_kind ppf kind let pp_errors = W.pp_param pp_kind level |> Fmt.list diff --git a/plugins/qcheck-stm/src/reserr.mli b/plugins/qcheck-stm/src/reserr.mli index a716a6dd..02756ce4 100644 --- a/plugins/qcheck-stm/src/reserr.mli +++ b/plugins/qcheck-stm/src/reserr.mli @@ -35,6 +35,7 @@ type W.kind += | Returned_tuple of string | Ghost_values of (string * [ `Arg | `Ret ]) | Incompatible_sut of string + | Incomplete_ret_val_computation of string type 'a reserr diff --git a/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml b/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml index d0030338..50e89784 100644 --- a/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml +++ b/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml @@ -4,36 +4,47 @@ include Ortac_runtime let ( ++ ) a b = match (a, b) with | None, None -> None - | Some (_, _), None -> a - | None, Some (_, _) -> b - | Some (cmd0, terms0), Some (cmd1, terms1) -> + | Some (_, _, _), None -> a + | None, Some (_, _, _) -> b + | Some (ret, cmd0, terms0), Some (_, cmd1, terms1) -> assert (cmd0 = cmd1); - Some (cmd0, terms0 @ terms1) + Some (ret, cmd0, terms0 @ terms1) module Make (Spec : Spec) = struct open QCheck module Internal = Internal.Make (Spec) [@alert "-internal"] - let pp_trace ppf trace = + let pp_trace ppf (trace, ret) = let open Fmt in - let pp_aux ppf (c, r) = - pf ppf "ignore (%s); (* returned %s *)" (Spec.show_cmd c) (show_res r) + let rec aux ppf = function + | [ (c, r) ] -> ( + match ret with + | Some ret -> + pf ppf "ignore (%s); (* returned %s, expected %s *)" + (Spec.show_cmd c) (show_res r) (show_res ret) + | None -> + pf ppf "ignore (%s); (* returned %s *)" (Spec.show_cmd c) + (show_res r)) + | (c, r) :: xs -> + pf ppf "ignore (%s); (* returned %s *)" (Spec.show_cmd c) (show_res r); + aux ppf xs + | _ -> assert false in - pf ppf "@[let sut = init_sut in@\n%a@]" (list ~sep:(any "@\n") pp_aux) trace + pf ppf "@[let sut = init_sut in@\n%a@]" aux trace let pp_terms ppf err = let open Fmt in let pp_aux ppf (term, l) = pf ppf "@[%a@\n @[%s@]@]@\n" pp_loc l term in pf ppf "%a" (list ~sep:(any "@\n") pp_aux) err - let message trace cmd terms = + let message trace ret cmd terms = Test.fail_reportf "Gospel specification violation in function %s\n\ @;\ \ @[%a@]@\n\ when executing the following sequence of operations:@\n\ @;\ - \ @[%a@]@." cmd pp_terms terms pp_trace trace + \ @[%a@]@." cmd pp_terms terms pp_trace (trace, ret) let rec check_disagree postcond s sut cs = match cs with @@ -48,8 +59,9 @@ module Make (Spec : Spec) = struct let s' = Spec.next_state c s in match check_disagree postcond s' sut cs with | None -> None - | Some (rest, cmd, terms) -> Some ((c, res) :: rest, cmd, terms)) - | Some (cmd, terms) -> Some ([ (c, res) ], cmd, terms)) + | Some (rest, ret, cmd, terms) -> + Some ((c, res) :: rest, ret, cmd, terms)) + | Some (ret, cmd, terms) -> Some ([ (c, res) ], ret, cmd, terms)) let agree_prop wrapped_init_state postcond cs = let _ = wrapped_init_state () in @@ -64,7 +76,7 @@ module Make (Spec : Spec) = struct let res = match res with Ok res -> res | Error exn -> raise exn in match res with | None -> true - | Some (trace, cmd, terms) -> message trace cmd terms + | Some (trace, ret, cmd, terms) -> message trace ret cmd terms let agree_test ~count ~name wrapped_init_state postcond = Test.make ~name ~count diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml index 2b7766b2..8bc97bac 100644 --- a/plugins/qcheck-stm/src/stm_of_ir.ml +++ b/plugins/qcheck-stm/src/stm_of_ir.ml @@ -432,6 +432,38 @@ let precond config ir = in pstr_value Nonrecursive [ value_binding ~pat ~expr ] |> ok +let returned_value translate_postcond value = + let open Reserr in + let res = lident "Res" and ty_ret = Ir.get_return_type value in + let* ty_show = exp_of_core_type value.inst ty_ret in + let aux ty comp = + match (ty.ptyp_desc, comp) with + | Ptyp_constr ({ txt = Lident "unit"; _ }, _), _ -> ok eunit + | _, xs -> ( + let* xs = map translate_postcond xs in + match xs with + | [] -> + error + ( Incomplete_ret_val_computation (Fmt.str "%a" Ident.pp value.id), + Location.none ) + | x :: _ -> ok x) + in + let* ret_values = + match ty_ret.ptyp_desc with + | Ptyp_tuple tys -> + pexp_tuple <$> sequence (List.map2 aux tys value.ret_values) + | Ptyp_constr ({ txt = Lident "unit"; _ }, _) -> ok eunit + | _ -> ( + match value.ret_values with + | [] -> + error + ( Incomplete_ret_val_computation (Fmt.str "%a" Ident.pp value.id), + Location.none ) + | (xs::_) -> aux ty_ret xs) + in + let args = pexp_tuple_opt [ ty_show; ret_values ] in + pexp_construct res args |> ok + let postcond_case config state invariants idx state_ident new_state_ident value = let open Reserr in @@ -443,12 +475,19 @@ let postcond_case config state invariants idx state_ident new_state_ident value subst_term state ~gos_t:id ~old_t:None ~new_t:(Some new_state_ident) ~new_lz:true t >>= ocaml_of_term config - and wrap_check t e = + in + let ret_val = + match to_option @@ returned_value translate_postcond value with + | None -> enone + | Some e -> esome e + in + let wrap_check t e = let term = estring t.text and cmd = Fmt.str "%a" Ident.pp value.id |> estring and l = t.Ir.term.Gospel.Tterm.t_loc |> elocation in pexp_ifthenelse e enone - (Some (esome @@ pexp_tuple [ cmd; elist [ pexp_tuple [ term; l ] ] ])) + (Some + (esome @@ pexp_tuple [ ret_val; cmd; elist [ pexp_tuple [ term; l ] ] ])) in let idx = List.sort Int.compare idx in let lhs0 = mk_cmd_pattern value in diff --git a/plugins/qcheck-stm/test/array_stm_tests.expected.ml b/plugins/qcheck-stm/test/array_stm_tests.expected.ml index 7d900008..d4d27324 100644 --- a/plugins/qcheck-stm/test/array_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/array_stm_tests.expected.ml @@ -364,7 +364,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("length", + (None, "length", [("i = t.size", { Ortac_runtime.start = @@ -419,7 +419,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("get", + (None, "get", [("0 <= i < t.size", { Ortac_runtime.start = @@ -471,7 +471,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("get", + (None, "get", [("a = List.nth t.contents i", { Ortac_runtime.start = @@ -530,7 +530,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("get", + (None, "get", [("0 <= i < t.size", { Ortac_runtime.start = @@ -585,7 +585,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("set", + ((Some (Res (unit, ()))), "set", [("0 <= i < t.size", { Ortac_runtime.start = @@ -645,7 +645,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("set", + ((Some (Res (unit, ()))), "set", [("0 <= i < t.size", { Ortac_runtime.start = @@ -693,7 +693,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("fill", + ((Some (Res (unit, ()))), "fill", [("0 <= i", { Ortac_runtime.start = @@ -741,7 +741,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("fill", + ((Some (Res (unit, ()))), "fill", [("0 <= j", { Ortac_runtime.start = @@ -793,7 +793,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("fill", + ((Some (Res (unit, ()))), "fill", [("i + j <= t.size", { Ortac_runtime.start = @@ -846,7 +846,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("fill", + ((Some (Res (unit, ()))), "fill", [("0 <= i", { Ortac_runtime.start = @@ -894,7 +894,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("fill", + ((Some (Res (unit, ()))), "fill", [("0 <= j", { Ortac_runtime.start = @@ -947,7 +947,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("fill", + ((Some (Res (unit, ()))), "fill", [("i + j <= t.size", { Ortac_runtime.start = @@ -992,7 +992,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("to_list", + (None, "to_list", [("l = t.contents", { Ortac_runtime.start = @@ -1040,7 +1040,7 @@ let ortac_postcond cmd__008_ state__009_ res__010_ = then None else Some - ("mem", + (None, "mem", [("b = List.mem a t.contents", { Ortac_runtime.start = diff --git a/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml b/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml index 3e78a989..041c55d6 100644 --- a/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/conjunctive_clauses_stm_tests.expected.ml @@ -198,7 +198,7 @@ let ortac_postcond cmd__006_ state__007_ res__008_ = then None else Some - ("set", + ((Some (Res (unit, ()))), "set", [("0 <= i < List.length t.contents", { Ortac_runtime.start = @@ -258,7 +258,7 @@ let ortac_postcond cmd__006_ state__007_ res__008_ = then None else Some - ("set", + ((Some (Res (unit, ()))), "set", [("0 <= i < List.length t.contents", { Ortac_runtime.start = diff --git a/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml b/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml index 31b3a6d8..924629b6 100644 --- a/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/hashtbl_stm_tests.expected.ml @@ -322,7 +322,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("find", + (None, "find", [("List.mem (a, b) h.contents", { Ortac_runtime.start = @@ -372,7 +372,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("find", + (None, "find", [("not (List.mem a (List.map fst h.contents))", { Ortac_runtime.start = @@ -435,7 +435,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("find_opt", + (None, "find_opt", [("match o with\n | None -> not (List.mem a (List.map fst h.contents))\n | Some b -> List.mem (a, b) h.contents", { Ortac_runtime.start = @@ -485,7 +485,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("find_all", + (None, "find_all", [("bs = Sequence.filter_map (fun (x, y) -> if x = a then Some y else None) h.contents", { Ortac_runtime.start = @@ -535,7 +535,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("mem", + (None, "mem", [("b = List.mem a (List.map fst h.contents)", { Ortac_runtime.start = @@ -585,7 +585,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("length", + (None, "length", [("i = List.length h.contents", { Ortac_runtime.start = diff --git a/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml b/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml index d55ab075..cdd134c1 100644 --- a/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/invariants_stm_tests.expected.ml @@ -148,7 +148,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("push", + ((Some (Res (unit, ()))), "push", [("List.length x.contents > 0", { Ortac_runtime.start = diff --git a/plugins/qcheck-stm/test/record_stm_tests.expected.ml b/plugins/qcheck-stm/test/record_stm_tests.expected.ml index 836e4388..d2dc7e04 100644 --- a/plugins/qcheck-stm/test/record_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/record_stm_tests.expected.ml @@ -116,7 +116,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("get", + (None, "get", [("i = r.value", { Ortac_runtime.start = @@ -165,7 +165,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("get", + (None, "get", [("plus1 i = i + 1", { Ortac_runtime.start = @@ -215,7 +215,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("get", + (None, "get", [("plus2 i = i + 2", { Ortac_runtime.start = diff --git a/plugins/qcheck-stm/test/ref_stm_tests.expected.ml b/plugins/qcheck-stm/test/ref_stm_tests.expected.ml index 0b65aa4f..b5656f52 100644 --- a/plugins/qcheck-stm/test/ref_stm_tests.expected.ml +++ b/plugins/qcheck-stm/test/ref_stm_tests.expected.ml @@ -87,7 +87,7 @@ let ortac_postcond cmd__004_ state__005_ res__006_ = then None else Some - ("get", + (None, "get", [("i = r.value", { Ortac_runtime.start =