Protect exception throwing calls in scenario

n-osborne · Mar 14, 2024 · 828e11f · 828e11f
1 parent b59417f
commit 828e11f
Show file tree

Hide file tree

Showing 5 changed files with 44 additions and 27 deletions.
diff --git a/examples/lwt_dllist_tests.ml b/examples/lwt_dllist_tests.ml
@@ -25,8 +25,8 @@ module Spec =
           Format.asprintf "%s %a %s" "add_l" (Util.Pp.pp_int true) a_1 "sut"
       | Add_r a_2 ->
           Format.asprintf "%s %a %s" "add_r" (Util.Pp.pp_int true) a_2 "sut"
-      | Take_l -> Format.asprintf "%s %s" "take_l" "sut"
-      | Take_r -> Format.asprintf "%s %s" "take_r" "sut"
+      | Take_l -> Format.asprintf "protect (fun () -> %s %s)" "take_l" "sut"
+      | Take_r -> Format.asprintf "protect (fun () -> %s %s)" "take_r" "sut"
       | Take_opt_l -> Format.asprintf "%s %s" "take_opt_l" "sut"
       | Take_opt_r -> Format.asprintf "%s %s" "take_opt_r" "sut"
     type nonrec state = {

diff --git a/examples/varray_circular_tests.ml b/examples/varray_circular_tests.ml
@@ -82,30 +82,34 @@ module Spec =
       | Push_back x ->
           Format.asprintf "%s %s %a" "push_back" "sut"
             (Util.Pp.pp_elt Util.Pp.pp_char true) x
-      | Pop_back -> Format.asprintf "%s %s" "pop_back" "sut"
+      | Pop_back ->
+          Format.asprintf "protect (fun () -> %s %s)" "pop_back" "sut"
       | Push_front x_1 ->
           Format.asprintf "%s %s %a" "push_front" "sut"
             (Util.Pp.pp_elt Util.Pp.pp_char true) x_1
-      | Pop_front -> Format.asprintf "%s %s" "pop_front" "sut"
+      | Pop_front ->
+          Format.asprintf "protect (fun () -> %s %s)" "pop_front" "sut"
       | Insert_at (i_1, x_2) ->
-          Format.asprintf "%s %s %a %a" "insert_at" "sut"
+          Format.asprintf "protect (fun () -> %s %s %a %a)" "insert_at" "sut"
             (Util.Pp.pp_int true) i_1 (Util.Pp.pp_elt Util.Pp.pp_char true)
             x_2
       | Pop_at i_2 ->
-          Format.asprintf "%s %s %a" "pop_at" "sut" (Util.Pp.pp_int true) i_2
+          Format.asprintf "protect (fun () -> %s %s %a)" "pop_at" "sut"
+            (Util.Pp.pp_int true) i_2
       | Delete_at i_3 ->
-          Format.asprintf "%s %s %a" "delete_at" "sut" (Util.Pp.pp_int true)
-            i_3
+          Format.asprintf "protect (fun () -> %s %s %a)" "delete_at" "sut"
+            (Util.Pp.pp_int true) i_3
       | Get i_4 ->
-          Format.asprintf "%s %s %a" "get" "sut" (Util.Pp.pp_int true) i_4
+          Format.asprintf "protect (fun () -> %s %s %a)" "get" "sut"
+            (Util.Pp.pp_int true) i_4
       | Set (i_5, v) ->
-          Format.asprintf "%s %s %a %a" "set" "sut" (Util.Pp.pp_int true) i_5
-            (Util.Pp.pp_elt Util.Pp.pp_char true) v
+          Format.asprintf "protect (fun () -> %s %s %a %a)" "set" "sut"
+            (Util.Pp.pp_int true) i_5 (Util.Pp.pp_elt Util.Pp.pp_char true) v
       | Length -> Format.asprintf "%s %s" "length" "sut"
       | Is_empty -> Format.asprintf "%s %s" "is_empty" "sut"
       | Fill (pos, len, x_3) ->
-          Format.asprintf "%s %s %a %a %a" "fill" "sut" (Util.Pp.pp_int true)
-            pos (Util.Pp.pp_int true) len
+          Format.asprintf "protect (fun () -> %s %s %a %a %a)" "fill" "sut"
+            (Util.Pp.pp_int true) pos (Util.Pp.pp_int true) len
             (Util.Pp.pp_elt Util.Pp.pp_char true) x_3
     type nonrec state = {
       contents: char Ortac_runtime.Gospelstdlib.sequence }

diff --git a/examples/varray_tests.ml b/examples/varray_tests.ml
@@ -82,30 +82,34 @@ module Spec =
       | Push_back x ->
           Format.asprintf "%s %s %a" "push_back" "sut"
             (Util.Pp.pp_elt Util.Pp.pp_char true) x
-      | Pop_back -> Format.asprintf "%s %s" "pop_back" "sut"
+      | Pop_back ->
+          Format.asprintf "protect (fun () -> %s %s)" "pop_back" "sut"
       | Push_front x_1 ->
           Format.asprintf "%s %s %a" "push_front" "sut"
             (Util.Pp.pp_elt Util.Pp.pp_char true) x_1
-      | Pop_front -> Format.asprintf "%s %s" "pop_front" "sut"
+      | Pop_front ->
+          Format.asprintf "protect (fun () -> %s %s)" "pop_front" "sut"
       | Insert_at (i_1, x_2) ->
-          Format.asprintf "%s %s %a %a" "insert_at" "sut"
+          Format.asprintf "protect (fun () -> %s %s %a %a)" "insert_at" "sut"
             (Util.Pp.pp_int true) i_1 (Util.Pp.pp_elt Util.Pp.pp_char true)
             x_2
       | Pop_at i_2 ->
-          Format.asprintf "%s %s %a" "pop_at" "sut" (Util.Pp.pp_int true) i_2
+          Format.asprintf "protect (fun () -> %s %s %a)" "pop_at" "sut"
+            (Util.Pp.pp_int true) i_2
       | Delete_at i_3 ->
-          Format.asprintf "%s %s %a" "delete_at" "sut" (Util.Pp.pp_int true)
-            i_3
+          Format.asprintf "protect (fun () -> %s %s %a)" "delete_at" "sut"
+            (Util.Pp.pp_int true) i_3
       | Get i_4 ->
-          Format.asprintf "%s %s %a" "get" "sut" (Util.Pp.pp_int true) i_4
+          Format.asprintf "protect (fun () -> %s %s %a)" "get" "sut"
+            (Util.Pp.pp_int true) i_4
       | Set (i_5, v) ->
-          Format.asprintf "%s %s %a %a" "set" "sut" (Util.Pp.pp_int true) i_5
-            (Util.Pp.pp_elt Util.Pp.pp_char true) v
+          Format.asprintf "protect (fun () -> %s %s %a %a)" "set" "sut"
+            (Util.Pp.pp_int true) i_5 (Util.Pp.pp_elt Util.Pp.pp_char true) v
       | Length -> Format.asprintf "%s %s" "length" "sut"
       | Is_empty -> Format.asprintf "%s %s" "is_empty" "sut"
       | Fill (pos, len, x_3) ->
-          Format.asprintf "%s %s %a %a %a" "fill" "sut" (Util.Pp.pp_int true)
-            pos (Util.Pp.pp_int true) len
+          Format.asprintf "protect (fun () -> %s %s %a %a %a)" "fill" "sut"
+            (Util.Pp.pp_int true) pos (Util.Pp.pp_int true) len
             (Util.Pp.pp_elt Util.Pp.pp_char true) x_3
     type nonrec state = {
       contents: char Ortac_runtime.Gospelstdlib.sequence }

diff --git a/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml b/plugins/qcheck-stm/src/runtime/ortac_runtime_qcheck_stm.ml
@@ -47,7 +47,12 @@ module Make (Spec : Spec) = struct
           aux ppf xs
       | _ -> assert false
     in
-    pf ppf "@[open %s@\nlet sut = %s@\n%a@]" mod_name init_sut aux trace
+    pf ppf
+      "@[open %s@\n\
+       let protect f = try Ok (f ()) with e -> Error e@\n\
+       let sut = %s@\n\
+       %a@]"
+      mod_name init_sut aux trace
 
   let pp_terms ppf err =
     let open Fmt in

diff --git a/plugins/qcheck-stm/src/stm_of_ir.ml b/plugins/qcheck-stm/src/stm_of_ir.ml
@@ -746,9 +746,13 @@ let pp_cmd_case config value =
              type)"
     in
     let* fmt, pp_args = aux value.ty value.args in
-    let fmt = String.concat " " ("%s" :: fmt) |> estring in
+    let fmt =
+      let call = String.concat " " ("%s" :: fmt) in
+      if may_raise_exception value then "protect (fun () -> " ^ call ^ ")"
+      else call
+    in
     let args =
-      List.map (fun x -> (Nolabel, x)) (fmt :: estring name :: pp_args)
+      List.map (fun x -> (Nolabel, x)) (estring fmt :: estring name :: pp_args)
     in
     pexp_apply (qualify [ "Format" ] "asprintf") args |> ok
   in