Merge pull request #558 from ocaml-multicore/weak-re-revision

STM Weak test re-revision

Author: jmid

src/weak/stm_tests_hashset_spec.ml

@@ -16,11 +16,11 @@ type cmd =
   | Find_all of data
   | Count
   | Stats
-and data = int64
+and data = string
 
 let pp_cmd par fmt x =
   let open Util.Pp in
-  let pp_data = pp_int64 in
+  let pp_data = pp_string in
   match x with
   | Clear -> cst0 "Clear" fmt
   | Merge x -> cst1 pp_data "Merge" par fmt x
@@ -37,19 +37,10 @@ let show_cmd = Util.Pp.to_show pp_cmd
 
 type state = data list
 
-module Int64 =
-struct
-  [@@@warning "-unused-value-declaration"]
-  (* support Int64.hash added in 5.1, without triggering an 'unused hash' error *)
-  external seeded_hash_param :
-    int -> int -> int -> 'a -> int = "caml_hash" [@@noalloc]
-  let hash x = seeded_hash_param 10 100 0 x
-  include Stdlib.Int64
-end
-module WHS = Weak.Make(Int64)
+module WHS = Weak.Make(String)
 type sut = WHS.t
 
-let shrink_data d = Shrink.int64 d
+let shrink_data d = Shrink.string ~shrink:Shrink.nil d
 
 let _shrink_cmd c = match c with
   | Clear -> Iter.empty
@@ -64,14 +55,15 @@ let _shrink_cmd c = match c with
   | Stats -> Iter.empty
 
 let arb_cmd s =
+  let string_gen = Gen.(string_small_of printable) in
   let data_gen = match s with
-    | [] -> Gen.(map Int64.of_int small_int)
-    | _::_ -> Gen.(oneof [oneofl s; map Int64.of_int small_int]) in
+    | [] -> string_gen
+    | _::_ -> Gen.(oneof [oneofl s; string_gen]) in
   QCheck.make ~print:show_cmd (*~shrink:shrink_cmd*)
     Gen.(frequency
            [ 1,return Clear;
-             1,map (fun d -> Merge d) data_gen;
-             1,map (fun d -> Add d) data_gen;
+             2,map (fun d -> Merge d) data_gen;
+             2,map (fun d -> Add d) data_gen;
              1,map (fun d -> Remove d) data_gen;
              1,map (fun d -> Find d) data_gen;
              1,map (fun d -> Find_opt d) data_gen;
@@ -104,8 +96,7 @@ let weak_size = 16
 let init_sut () = Gc.minor (); WHS.create weak_size
 let cleanup _   = ()
 
-let precond c _s = match c with
-  | _ -> true
+let precond _c _s = true
 
 type _ ty += Tup6 : 'a ty * 'b ty * 'c ty * 'd ty * 'e ty * 'f ty -> ('a * 'b * 'c * 'd * 'e * 'f) ty
 
@@ -121,39 +112,35 @@ let tup6 spec_a spec_b spec_c spec_d spec_e spec_f =
 
 let run c hs = match c with
   | Clear      -> Res (unit, WHS.clear hs)
-  | Merge d    -> Res (result int64 exn, protect (WHS.merge hs) d)
-  | Add d      -> Res (result unit exn, protect (WHS.add hs) d)
-  | Remove d   -> Res (result unit exn, protect (WHS.remove hs) d)
-  | Find d     -> Res (result int64 exn, protect (WHS.find hs) d)
-  | Find_opt d -> Res (result (option int64) exn, protect (WHS.find_opt hs) d)
-  | Find_all d -> Res (result (list int64) exn, protect (WHS.find_all hs) d)
-  | Mem d      -> Res (result bool exn, protect (WHS.mem hs) d)
+  | Merge d    -> Res (result string exn, protect (fun () -> WHS.merge hs d) ())
+  | Add d      -> Res (result unit exn, protect (fun () -> WHS.add hs d) ())
+  | Remove d   -> Res (result unit exn, protect (fun () -> WHS.remove hs d) ())
+  | Find d     -> Res (result string exn, protect (fun () -> WHS.find hs d) ())
+  | Find_opt d -> Res (result (option string) exn, protect (fun () -> WHS.find_opt hs d) ())
+  | Find_all d -> Res (result (list string) exn, protect (fun () -> WHS.find_all hs d) ())
+  | Mem d      -> Res (result bool exn, protect (fun () -> WHS.mem hs d) ())
   | Count      -> Res (int, WHS.count hs)
   | Stats      -> Res (tup6 int int int int int int, WHS.stats hs)
 
 let postcond c (s:data list) res = match c, res with
   | Clear, Res ((Unit,_),())  -> true
-  | Merge d, Res ((Result (Int64,Exn),_),r) ->
+  | Merge d, Res ((Result (String,Exn),_),r) ->
     (match r with
-     | Error e -> e = Invalid_argument "index out of bounds"
+     | Error _ -> false
      | Ok r -> if List.mem d s then r = d else r == d)
   | Add _, Res ((Result (Unit,Exn),_),r) ->
-    r = Error (Invalid_argument "index out of bounds") || r = Ok ()
+    r = Ok ()
   | Remove _, Res ((Result (Unit,Exn),_),r) ->
-    r = Error (Invalid_argument "index out of bounds") || r = Ok ()
-  | Find d, Res ((Result (Int64,Exn),_),r) ->
-    r = Error (Invalid_argument "index out of bounds") ||
-    r = Error Not_found ||
-    (List.mem d s && r = Ok d)
-  | Find_opt d, Res ((Result (Option Int64,Exn),_),r) ->
-    r = Error (Invalid_argument "index out of bounds") ||
-    r = Ok None || r = Ok (Some d)
-  | Find_all d, Res ((Result (List Int64,Exn),_),r) ->
+    r = Ok ()
+  | Find d, Res ((Result (String,Exn),_),r) ->
+    r = Error Not_found || (List.mem d s && r = Ok d)
+  | Find_opt d, Res ((Result (Option String,Exn),_),r) ->
+    r = Ok None || (List.mem d s && r = Ok (Some d))
+  | Find_all d, Res ((Result (List String,Exn),_),r) ->
     (match r with
-     | Error e -> e = Invalid_argument "index out of bounds"
+     | Error _ -> false
      | Ok r -> List.for_all (fun d' -> d' = d) r)
   | Mem d, Res ((Result (Bool,Exn),_),r) ->
-    r = Error (Invalid_argument "index out of bounds") ||
     r = Ok (List.mem d s) || r = Ok false
   | Count, Res ((Int,_),r) ->
     r <= List.length s

src/weak/stm_tests_weak_spec.ml

@@ -10,18 +10,18 @@ type cmd =
   | Get_copy of int
   | Check of int
   | Fill of int * int * data option
-and data = int64
+and data = string
 
 let pp_cmd par fmt x =
   let open Util.Pp in
   match x with
   | Length -> cst0 "Length" fmt
-  | Set (x, y) -> cst2 pp_int (pp_option pp_int64) "Set" par fmt x y
+  | Set (x, y) -> cst2 pp_int (pp_option pp_string) "Set" par fmt x y
   | Get x -> cst1 pp_int "Get" par fmt x
   | Get_copy x -> cst1 pp_int "Get_copy" par fmt x
   | Check x -> cst1 pp_int "Check" par fmt x
   | Fill (x, y, z) ->
-    cst3 pp_int pp_int (pp_option pp_int64) "Fill" par fmt x y z
+    cst3 pp_int pp_int (pp_option pp_string) "Fill" par fmt x y z
 
 let show_cmd = Util.Pp.to_show pp_cmd
 
@@ -41,66 +41,65 @@ let _shrink_cmd c = match c with
 
 let arb_cmd s =
   let int_gen = Gen.(oneof [small_nat; int_bound (List.length s - 1)]) in
-  let int64_gen = Gen.(map Int64.of_int small_int) in
+  let data_gen = Gen.(string_small_of printable) in
   QCheck.make ~print:show_cmd (*~shrink:shrink_cmd*)
     Gen.(frequency
            [ 1,return Length;
-             1,map2 (fun i c -> Set (i,c)) int_gen (option int64_gen);
+             1,map2 (fun i d_opt -> Set (i,d_opt)) int_gen (option data_gen);
              2,map (fun i -> Get i) int_gen;
              2,map (fun i -> Get_copy i) int_gen;
              2,map (fun i -> Check i) int_gen;
-             1,map3 (fun i len c -> Fill (i,len,c)) int_gen int_gen (option int64_gen); (* hack: reusing int_gen for length *)
+             2,map3 (fun i len d_opt -> Fill (i,len,d_opt)) int_gen int_gen (option data_gen); (* hack: reusing int_gen for length *)
            ])
 
-let weak_size = 16
+let weak_size = 10
 
 let init_state  = List.init weak_size (fun _ -> None)
 
 let next_state c s = match c with
   | Length -> s
-  | Set (i,c) ->
-    List.mapi (fun j c' -> if i=j then c else c') s
-  | Get _  -> s
-  | Get_copy _  -> s
+  | Set (i,d_opt) ->
+    List.mapi (fun j d_opt' -> if i=j then d_opt else d_opt') s
+  | Get _ -> s
+  | Get_copy _ -> s
   | Check _  -> s
-  | Fill (i,l,c) ->
+  | Fill (i,l,d_opt) ->
     if i >= 0 && l >= 0 && i+l-1 < List.length s
     then
-      List.mapi (fun j c' -> if i <= j && j <= i+l-1 then c else c') s
+      List.mapi (fun j d_opt' -> if i <= j && j <= i+l-1 then d_opt else d_opt') s
     else s
 
 let init_sut () = Gc.minor (); Weak.create weak_size
 let cleanup _   = ()
 
-let precond c _s = match c with
-  | _ -> true
+let precond _c _s = true
 
 let run c a = match c with
   | Length       -> Res (int, Weak.length a)
-  | Set (i,c)    -> Res (result unit exn, protect (Weak.set a i) c)
-  | Get i        -> Res (result (option int64) exn, protect (Weak.get a) i)
-  | Get_copy i   -> Res (result (option int64) exn, protect (Weak.get_copy a) i)
-  | Check i      -> Res (result bool exn, protect (Weak.check a) i)
-  | Fill (i,l,c) -> Res (result unit exn, protect (Weak.fill a i l) c)
+  | Set (i,d_opt)    -> Res (result unit exn, protect (fun () -> Weak.set a i d_opt) ())
+  | Get i        -> Res (result (option string) exn, protect (fun () -> Weak.get a i) ())
+  | Get_copy i   -> Res (result (option string) exn, protect (fun () -> Weak.get_copy a i) ())
+  | Check i      -> Res (result bool exn, protect (fun () -> Weak.check a i) ())
+  | Fill (i,l,d_opt) -> Res (result unit exn, protect (fun () -> Weak.fill a i l d_opt) ())
 
-let postcond c (s:int64 option list) res = match c, res with
+let postcond c (s:state) res = match c, res with
   | Length, Res ((Int,_),i) -> i = List.length s
   | Set (i,_), Res ((Result (Unit,Exn),_), r) ->
     if i < 0 || i >= List.length s
     then r = Error (Invalid_argument "Weak.set")
     else r = Ok ()
-  | Get i, Res ((Result (Option Int64,Exn),_), r) ->
+  | Get i, Res ((Result (Option String,Exn),_), r) ->
     if i < 0 || i >= List.length s
     then r = Error (Invalid_argument "Weak.get")
-    else r = Ok (List.nth s i)
-  | Get_copy i, Res ((Result (Option Int64,Exn),_), r) ->
+    else r = Ok None || r = Ok (List.nth s i)
+  | Get_copy i, Res ((Result (Option String,Exn),_), r) ->
     if i < 0 || i >= List.length s
     then r = Error (Invalid_argument "Weak.get_copy")
-    else r = Ok (List.nth s i)
+    else r = Ok None || r = Ok (List.nth s i)
   | Check i, Res ((Result (Bool,Exn),_),r) ->
     if i < 0 || i >= List.length s
     then r = Error (Invalid_argument "Weak.check")
-    else r = Ok (None <> List.nth s i)
+    else r = Ok false || r = Ok (None <> List.nth s i)
   | Fill (i,l,_), Res ((Result (Unit,Exn),_), r) ->
     if i < 0 || l < 0 || i+l > List.length s
     then r = Error (Invalid_argument "Weak.fill")