Protect exception by injecting them in result type

lib/STM.ml

@@ -1,4 +1,5 @@
 open QCheck
+include Util
 
 (** A revised state machine framework with parallel testing.
     This version does not come with built-in GC commands. *)
@@ -63,13 +64,6 @@ sig
       Note: [s] is in this case the model's state prior to command execution. *)
 end
 
-let rec repeat n prop = fun input ->
-  if n<0 then failwith "repeat: negative repetition count";
-  if n=0
-  then true
-  else prop input && repeat (n-1) prop input
-
-
 (** Derives a test framework from a state machine specification. *)
 module Make(Spec : StmSpec) (*: StmTest *)
   : sig
@@ -87,8 +81,6 @@ module Make(Spec : StmSpec) (*: StmTest *)
     val interp_sut_res : Spec.sut -> Spec.cmd list -> (Spec.cmd * Spec.res) list
     val check_obs : (Spec.cmd * Spec.res) list -> (Spec.cmd * Spec.res) list -> (Spec.cmd * Spec.res) list -> Spec.state -> bool
     val gen_cmds_size : Spec.state -> int Gen.t -> Spec.cmd list Gen.t
-  (*val print_triple : ...*)
-    val print_triple_vertical : ?fig_indent:int -> ?res_width:int -> ('a -> string) -> ('a list * 'a list * 'a list) -> string
   (*val shrink_triple : ...*)
     val arb_cmds_par : int -> int -> (Spec.cmd list * Spec.cmd list * Spec.cmd list) arbitrary
     val agree_prop_par         : (Spec.cmd list * Spec.cmd list * Spec.cmd list) -> bool
@@ -204,50 +196,6 @@ struct
            b2 && check_obs pref cs1 cs2' s')
 
   let gen_cmds_size s size_gen = Gen.sized_size size_gen (gen_cmds s)
-(*
-  let print_triple (seq,par1,par2) =
-    let header1, header2 = "Seq.prefix:", "Parallel procs.:" in
-    let pr_cmds = Print.list Spec.show_cmd in
-    let seq_str = pr_cmds seq in
-    let seq_len = max (String.length header1) (String.length seq_str) in
-    let buf = Buffer.create 64 in
-    begin
-      Printf.bprintf buf " %-*s  %s\n\n" seq_len header1 header2;
-      Printf.bprintf buf " %s  %s\n" (String.make seq_len ' ') (pr_cmds par1);
-      Printf.bprintf buf " %*s\n" seq_len seq_str;
-      Printf.bprintf buf " %s  %s\n" (String.make seq_len ' ') (pr_cmds par2);
-      Buffer.contents buf
-    end
- *)
-  let print_triple_vertical ?(fig_indent=10) ?(res_width=20) show (seq,cmds1,cmds2) =
-    let seq,cmds1,cmds2 = List.(map show seq, map show cmds1, map show cmds2) in
-    let max_width ss = List.fold_left max 0 (List.map String.length ss) in
-    let width = List.fold_left max 0 [max_width seq; max_width cmds1; max_width cmds2] in
-    let res_width = max width res_width in
-    let cmd_indent = String.make ((width-1)/2) ' ' in
-    let seq_indent = String.make ((res_width + 3)/2) ' ' in
-    let bar_cmd = Printf.sprintf "%-*s" res_width (cmd_indent ^ "|") in
-    let center c =
-      let clen = String.length c in
-      if clen > width (* it's a '|'-string *)
-      then c
-      else Printf.sprintf "%s%s" (String.make ((width - clen)/2) ' ') c in
-    let buf = Buffer.create 64 in
-    let indent () = Printf.bprintf buf "%s" (String.make fig_indent ' ') in
-    let print_seq_col c = Printf.bprintf buf "%s%-*s\n" seq_indent res_width c in
-    let print_par_col c1 c2 = Printf.bprintf buf "%-*s  %-*s\n" res_width c1 res_width c2 in
-    let print_hoz_line () =
-      Printf.bprintf buf "%-*s\n" res_width (cmd_indent ^ "." ^ (String.make (res_width + 1) '-') ^ ".") in
-    let rec print_par_cols cs cs' = match cs,cs' with
-      | [],   []    -> ()
-      | c::cs,[]    -> indent (); print_par_col (center c) ""; print_par_cols cs []
-      | [],   c::cs -> indent (); print_par_col "" (center c); print_par_cols [] cs
-      | l::ls,r::rs -> indent (); print_par_col (center l) (center r); print_par_cols ls rs in
-    (* actual printing *)
-    List.iter (fun c -> indent (); print_seq_col (center c)) ([bar_cmd] @ seq @ [bar_cmd]);
-    indent (); print_hoz_line ();
-    print_par_cols (bar_cmd::cmds1) (bar_cmd::cmds2);
-    Buffer.contents buf
 
   let shrink_triple =
     let open Iter in

lib/dune

@@ -2,13 +2,13 @@
  (name STM)
  (public_name multicorecheck.stm)
  (modules STM)
- (libraries qcheck domainslib))
+ (libraries qcheck domainslib util))
 
 (library
  (name lin)
  (public_name multicorecheck.lin)
  (modules lin)
- (libraries threads qcheck))
+ (libraries threads qcheck util))
 
 (library
  (name util)

lib/lin.ml

@@ -1,4 +1,5 @@
 open QCheck
+include Util
 
 module type CmdSpec = sig
   type t
@@ -30,49 +31,9 @@ module type CmdSpec = sig
   (** [run c t] should interpret the command [c] over the system under test [t] (typically side-effecting). *)
 end
 
-
-(* Horrible copy-paste for now, please FIXME *)
-let rec repeat n prop = fun input ->
-  if n<0 then failwith "repeat: negative repetition count";
-  if n=0
-  then true
-  else prop input && repeat (n-1) prop input
-
-
 module Make(Spec : CmdSpec) (*: StmTest *)
   = struct
 
-  (* Horrible copy-paste for now, please FIXME *)
-  let print_triple_vertical ?(fig_indent=10) ?(res_width=20) show (seq,cmds1,cmds2) =
-    let seq,cmds1,cmds2 = List.(map show seq, map show cmds1, map show cmds2) in
-    let max_width ss = List.fold_left max 0 (List.map String.length ss) in
-    let width = List.fold_left max 0 [max_width seq; max_width cmds1; max_width cmds2] in
-    let res_width = max width res_width in
-    let cmd_indent = String.make ((width-1)/2) ' ' in
-    let seq_indent = String.make ((res_width + 3)/2) ' ' in
-    let bar_cmd = Printf.sprintf "%-*s" res_width (cmd_indent ^ "|") in
-    let center c =
-      let clen = String.length c in
-      if clen > width (* it's a '|'-string *)
-      then c
-      else Printf.sprintf "%s%s" (String.make ((width - clen)/2) ' ') c in
-    let buf = Buffer.create 64 in
-    let indent () = Printf.bprintf buf "%s" (String.make fig_indent ' ') in
-    let print_seq_col c = Printf.bprintf buf "%s%-*s\n" seq_indent res_width c in
-    let print_par_col c1 c2 = Printf.bprintf buf "%-*s  %-*s\n" res_width c1 res_width c2 in
-    let print_hoz_line () =
-      Printf.bprintf buf "%-*s\n" res_width (cmd_indent ^ "." ^ (String.make (res_width + 1) '-') ^ ".") in
-    let rec print_par_cols cs cs' = match cs,cs' with
-      | [],   []    -> ()
-      | c::cs,[]    -> indent (); print_par_col (center c) ""; print_par_cols cs []
-      | [],   c::cs -> indent (); print_par_col "" (center c); print_par_cols [] cs
-      | l::ls,r::rs -> indent (); print_par_col (center l) (center r); print_par_cols ls rs in
-    (* actual printing *)
-    List.iter (fun c -> indent (); print_seq_col (center c)) ([bar_cmd] @ seq @ [bar_cmd]);
-    indent (); print_hoz_line ();
-    print_par_cols (bar_cmd::cmds1) (bar_cmd::cmds2);
-    Buffer.contents buf
-
   (* operate over arrays to avoid needless allocation underway *)
   let interp sut cs =
     let cs_arr = Array.of_list cs in

lib/util.ml

@@ -40,3 +40,40 @@ let fork_prop_with_timeout sec p x =
      | WEXITED code -> (0=code)
      | WSIGNALED _
      | WSTOPPED _  -> false)
+
+let print_triple_vertical ?(fig_indent=10) ?(res_width=20) show (seq,cmds1,cmds2) =
+  let seq,cmds1,cmds2 = List.(map show seq, map show cmds1, map show cmds2) in
+  let max_width ss = List.fold_left max 0 (List.map String.length ss) in
+  let width = List.fold_left max 0 [max_width seq; max_width cmds1; max_width cmds2] in
+  let res_width = max width res_width in
+  let cmd_indent = String.make ((width-1)/2) ' ' in
+  let seq_indent = String.make ((res_width + 3)/2) ' ' in
+  let bar_cmd = Printf.sprintf "%-*s" res_width (cmd_indent ^ "|") in
+  let center c =
+    let clen = String.length c in
+    if clen > width (* it's a '|'-string *)
+    then c
+    else Printf.sprintf "%s%s" (String.make ((width - clen)/2) ' ') c in
+  let buf = Buffer.create 64 in
+  let indent () = Printf.bprintf buf "%s" (String.make fig_indent ' ') in
+  let print_seq_col c = Printf.bprintf buf "%s%-*s\n" seq_indent res_width c in
+  let print_par_col c1 c2 = Printf.bprintf buf "%-*s  %-*s\n" res_width c1 res_width c2 in
+  let print_hoz_line () =
+    Printf.bprintf buf "%-*s\n" res_width (cmd_indent ^ "." ^ (String.make (res_width + 1) '-') ^ ".") in
+  let rec print_par_cols cs cs' = match cs,cs' with
+    | [],   []    -> ()
+    | c::cs,[]    -> indent (); print_par_col (center c) ""; print_par_cols cs []
+    | [],   c::cs -> indent (); print_par_col "" (center c); print_par_cols [] cs
+    | l::ls,r::rs -> indent (); print_par_col (center l) (center r); print_par_cols ls rs in
+  (* actual printing *)
+  List.iter (fun c -> indent (); print_seq_col (center c)) ([bar_cmd] @ seq @ [bar_cmd]);
+  indent (); print_hoz_line ();
+  print_par_cols (bar_cmd::cmds1) (bar_cmd::cmds2);
+  Buffer.contents buf
+
+let protect (f : 'a -> 'b) (a : 'a) : ('b, exn) result =
+  try Result.Ok (f a)
+  with e -> Result.Error e
+
+let pp_exn fmt e = Format.fprintf fmt "%s" (Printexc.to_string e)
+let show_exn e = Format.asprintf "%a" e pp_exn

src/domainslib/dune

@@ -9,7 +9,7 @@
 (executable
  (name ws_deque_test)
  (modules ws_deque_test)
- (libraries util qcheck STM domainslib)
+ (libraries qcheck STM domainslib)
  (preprocess (pps ppx_deriving.show)))
 
 (env

src/domainslib/ws_deque_test.ml

@@ -1,6 +1,7 @@
 (** Sequential tests of ws_deque *)
 
 open QCheck
+open STM
 
 module Ws_deque = Domainslib__Ws_deque
 
@@ -65,23 +66,23 @@ struct
     | RIs_empty of bool
     | RSize of int
     | RPush
-    | RPop of int option
-    | RSteal of int option [@@deriving show { with_path = false }]
+    | RPop of (int, exn) result
+    | RSteal of (int, exn) result [@@deriving show { with_path = false }]
 
   let run c d = match c with
     | Is_empty -> RIs_empty (Ws_deque.M.is_empty d)
     | Size     -> RSize (Ws_deque.M.size d)
     | Push i   -> (Ws_deque.M.push d i; RPush)
-    | Pop      -> RPop (try Some (Ws_deque.M.pop d) with Exit -> None)
-    | Steal    -> RSteal (try Some (Ws_deque.M.steal d) with Exit -> None)
+    | Pop      -> RPop (Util.protect Ws_deque.M.pop d)
+    | Steal    -> RSteal (Util.protect Ws_deque.M.steal d)
 
   let postcond c s res = match c,res with
     | Is_empty, RIs_empty b -> b = (s=[])
     | Size,     RSize size  -> (*Printf.printf "size:%i %!" size;*) size = (List.length s)
     | Push _,   RPush       -> true
-    | Pop,      RPop opt    -> (*Printf.printf "pop:%s %!" (match opt with None -> "None" | Some i -> string_of_int i);*)
-                               opt = (match s with | [] -> None | j::_ -> Some j)
-    | Steal,    RSteal opt  -> opt = (match List.rev s with | [] -> None | j::_ -> Some j)
+    | Pop,      RPop res    -> (*Printf.printf "pop:%s %!" (match opt with None -> "None" | Some i -> string_of_int i);*)
+                               (match s with | [] -> res = Error Exit | j::_ -> res = Ok j)
+    | Steal,    RSteal res  -> (match List.rev s with | [] -> Result.is_error res | j::_ -> res = Ok j)
     | _,_ -> false
 end
 

src/dune

@@ -24,7 +24,7 @@
 (executable
  (name atomic_test)
  (modules atomic_test)
- (libraries util qcheck STM)
+ (libraries qcheck STM)
  (preprocess (pps ppx_deriving.show)))
 
 (rule
@@ -71,13 +71,13 @@
 (executable
  (name lazy_stm_test)
  (modules lazy_stm_test)
- (libraries util qcheck STM)
+ (libraries qcheck STM)
  (preprocess (pps ppx_deriving.show)))
 
 (executable
  (name lazy_lin_test)
  (modules lazy_lin_test)
- (libraries util qcheck lin)
+ (libraries qcheck lin)
  (preprocess (pps ppx_deriving_qcheck ppx_deriving.show)))
 
 
@@ -87,7 +87,7 @@
  (name lin_tests)
  (modules lin_tests)
  (flags (:standard -w -27))
- (libraries util qcheck lin CList)
+ (libraries qcheck lin CList)
  (preprocess (pps ppx_deriving_qcheck ppx_deriving.show)))
 
 (rule

src/kcas/dune

@@ -16,7 +16,7 @@
  (name lin_tests)
  (modules lin_tests)
  (flags (:standard -w -27))
- (libraries util qcheck lin kcas)
+ (libraries qcheck lin kcas)
  (preprocess (pps ppx_deriving_qcheck ppx_deriving.show)))
 
 ; disable kcas test for now

src/lin_tests.ml

@@ -1,4 +1,5 @@
 open QCheck
+open Lin
 
 (** ********************************************************************** *)
 (**                   Tests of the Atomic module                           *)
@@ -108,7 +109,7 @@ struct
     | RClear
     | RAdd
     | RRemove
-    | RFind of int option
+    | RFind of (int, exn) result
     | RFind_opt of int option
     | RFind_all of int list
     | RReplace
@@ -121,9 +122,7 @@ struct
     | Clear         -> Hashtbl.clear h; RClear
     | Add (k,v)     -> Hashtbl.add h k v; RAdd
     | Remove k      -> Hashtbl.remove h k; RRemove
-    | Find k        -> RFind
-                         (try Some (Hashtbl.find h k)
-                          with Not_found -> None)
+    | Find k        -> RFind (Util.protect (Hashtbl.find h) k)
     | Find_opt k    -> RFind_opt (Hashtbl.find_opt h k)
     | Find_all k    -> RFind_all (Hashtbl.find_all h k)
     | Replace (k,v) -> Hashtbl.replace h k v; RReplace

src/lockfree/dune

@@ -9,7 +9,7 @@
 (executable
  (name lf_list_test)
  (modules lf_list_test)
- (libraries util qcheck STM lockfree)
+ (libraries qcheck STM lockfree)
  (preprocess (pps ppx_deriving.show)))
 
 (env
@@ -33,7 +33,7 @@
  (name lin_tests)
  (modules lin_tests)
  (flags (:standard -w -27))
- (libraries util qcheck lin lockfree)
+ (libraries qcheck lin lockfree)
  (preprocess (pps ppx_deriving_qcheck ppx_deriving.show)))
 
 (rule

src/neg_tests/dune

@@ -9,7 +9,7 @@
 (executable
  (name ref_test)
  (modules ref_test)
- (libraries util qcheck STM)
+ (libraries qcheck STM)
  (preprocess (pps ppx_deriving.show)))
 
 (env
@@ -34,7 +34,7 @@
 (executable
  (name conclist_test)
  (modules conclist_test)
- (libraries util CList qcheck STM)
+ (libraries CList qcheck STM)
  (preprocess (pps ppx_deriving.show)))
 
 (rule
@@ -54,7 +54,7 @@
  (name lin_tests)
  (modules lin_tests)
  (flags (:standard -w -27))
- (libraries util qcheck lin CList)
+ (libraries qcheck lin CList)
  (preprocess (pps ppx_deriving_qcheck ppx_deriving.show)))
 
 (rule

src/queue/dune

@@ -16,7 +16,7 @@
  (name lin_tests)
  (modules lin_tests)
  (flags (:standard -w -27))
- (libraries util qcheck lin)
+ (libraries qcheck lin)
  (preprocess (pps ppx_deriving_qcheck ppx_deriving.show)))
 
 (rule