From 7b8e85a26ae02f3233daf62ce87e50dbb36a9fb2 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 10 Nov 2023 17:34:22 +0100 Subject: [PATCH 1/4] Add for_all and exists to Array STM tests --- src/array/stm_tests.ml | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/array/stm_tests.ml b/src/array/stm_tests.ml index 0a6ce52b..d5ae8c25 100644 --- a/src/array/stm_tests.ml +++ b/src/array/stm_tests.ml @@ -5,6 +5,11 @@ open STM module AConf = struct + type char_bool_fun = (char -> bool) fun_ + + let pp_char_bool_fun par fmt f = + Format.fprintf fmt (if par then "(%s)" else "%s") (Fn.print f) + type cmd = | Length | Get of int @@ -13,6 +18,8 @@ struct | Copy | Fill of int * int * char | To_list + | For_all of char_bool_fun + | Exists of char_bool_fun | Mem of char | Sort | To_seq @@ -27,6 +34,8 @@ struct | Copy -> cst0 "Copy" fmt | Fill (x, y, z) -> cst3 pp_int pp_int pp_char "Fill" par fmt x y z | To_list -> cst0 "To_list" fmt + | For_all f -> cst1 pp_char_bool_fun "For_all" par fmt f + | Exists f -> cst1 pp_char_bool_fun "Exists" par fmt f | Mem x -> cst1 pp_char "Mem" par fmt x | Sort -> cst0 "Sort" fmt | To_seq -> cst0 "To_seq" fmt @@ -48,6 +57,8 @@ struct return Copy; map3 (fun i len c -> Fill (i,len,c)) int_gen int_gen char_gen; (* hack: reusing int_gen for length *) return To_list; + map (fun f -> For_all f) (fun1 Observable.char QCheck.bool).gen; + map (fun f -> Exists f) (fun1 Observable.char QCheck.bool).gen; map (fun c -> Mem c) char_gen; return Sort; return To_seq; @@ -70,6 +81,8 @@ struct List.mapi (fun j c' -> if i <= j && j <= i+l-1 then c else c') s else s | To_list -> s + | For_all _ -> s + | Exists _ -> s | Mem _ -> s | Sort -> List.sort Char.compare s | To_seq -> s @@ -88,6 +101,8 @@ struct | Copy -> Res (array char, Array.copy a) | Fill (i,l,c) -> Res (result unit exn, protect (Array.fill a i l) c) | To_list -> Res (list char, Array.to_list a) + | For_all (Fun (_,f)) -> Res (bool, Array.for_all f a) + | Exists (Fun (_,f)) -> Res (bool, Array.exists f a) | Mem c -> Res (bool, Array.mem c a) | Sort -> Res (unit, Array.sort Char.compare a) | To_seq -> Res (seq char, List.to_seq (List.of_seq (Array.to_seq a))) (* workaround: Array.to_seq is lazy and will otherwise see and report later Array.set state changes... *) @@ -112,6 +127,8 @@ struct then r = Error (Invalid_argument "Array.fill") else r = Ok () | To_list, Res ((List Char,_),cs) -> cs = s + | For_all (Fun (_,f)), Res ((Bool,_),r) -> r = List.for_all f s + | Exists (Fun (_,f)), Res ((Bool,_),r) -> r = List.exists f s | Mem c, Res ((Bool,_),r) -> r = List.mem c s | Sort, Res ((Unit,_),r) -> r = () | To_seq, Res ((Seq Char,_),r) -> Seq.equal (=) r (List.to_seq s) From 059a3dd0887fc855f261693da99503f97a20a113 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 10 Nov 2023 17:41:43 +0100 Subject: [PATCH 2/4] Add find_opt and find_index to Array STM tests --- src/array/stm_tests.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/array/stm_tests.ml b/src/array/stm_tests.ml index d5ae8c25..5080c637 100644 --- a/src/array/stm_tests.ml +++ b/src/array/stm_tests.ml @@ -21,6 +21,8 @@ struct | For_all of char_bool_fun | Exists of char_bool_fun | Mem of char + | Find_opt of char_bool_fun + | Find_index of char_bool_fun | Sort | To_seq @@ -37,6 +39,8 @@ struct | For_all f -> cst1 pp_char_bool_fun "For_all" par fmt f | Exists f -> cst1 pp_char_bool_fun "Exists" par fmt f | Mem x -> cst1 pp_char "Mem" par fmt x + | Find_opt f -> cst1 pp_char_bool_fun "Find_opt" par fmt f + | Find_index f -> cst1 pp_char_bool_fun "Find_index" par fmt f | Sort -> cst0 "Sort" fmt | To_seq -> cst0 "To_seq" fmt @@ -60,6 +64,8 @@ struct map (fun f -> For_all f) (fun1 Observable.char QCheck.bool).gen; map (fun f -> Exists f) (fun1 Observable.char QCheck.bool).gen; map (fun c -> Mem c) char_gen; + map (fun f -> Find_opt f) (fun1 Observable.char QCheck.bool).gen; + map (fun f -> Find_index f) (fun1 Observable.char QCheck.bool).gen; return Sort; return To_seq; ]) @@ -84,6 +90,8 @@ struct | For_all _ -> s | Exists _ -> s | Mem _ -> s + | Find_opt _ -> s + | Find_index _ -> s | Sort -> List.sort Char.compare s | To_seq -> s @@ -104,6 +112,8 @@ struct | For_all (Fun (_,f)) -> Res (bool, Array.for_all f a) | Exists (Fun (_,f)) -> Res (bool, Array.exists f a) | Mem c -> Res (bool, Array.mem c a) + | Find_opt (Fun (_,f)) -> Res (option char, Array.find_opt f a) + | Find_index (Fun (_,f)) -> Res (option int, Array.find_index f a) | Sort -> Res (unit, Array.sort Char.compare a) | To_seq -> Res (seq char, List.to_seq (List.of_seq (Array.to_seq a))) (* workaround: Array.to_seq is lazy and will otherwise see and report later Array.set state changes... *) @@ -130,6 +140,8 @@ struct | For_all (Fun (_,f)), Res ((Bool,_),r) -> r = List.for_all f s | Exists (Fun (_,f)), Res ((Bool,_),r) -> r = List.exists f s | Mem c, Res ((Bool,_),r) -> r = List.mem c s + | Find_opt (Fun (_,f)), Res ((Option Char,_),r) -> r = List.find_opt f s + | Find_index (Fun (_,f)), Res ((Option Int,_),r) -> r = List.find_index f s | Sort, Res ((Unit,_),r) -> r = () | To_seq, Res ((Seq Char,_),r) -> Seq.equal (=) r (List.to_seq s) | _, _ -> false From 09ccb5b0ea541547a4b51b6e10280f0efe790059 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 10 Nov 2023 17:47:25 +0100 Subject: [PATCH 3/4] Add stable_sort and fast_sort to Array STM tests --- src/array/stm_tests.ml | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/src/array/stm_tests.ml b/src/array/stm_tests.ml index 5080c637..3af9492b 100644 --- a/src/array/stm_tests.ml +++ b/src/array/stm_tests.ml @@ -24,6 +24,8 @@ struct | Find_opt of char_bool_fun | Find_index of char_bool_fun | Sort + | Stable_sort + | Fast_sort | To_seq let pp_cmd par fmt x = @@ -42,6 +44,8 @@ struct | Find_opt f -> cst1 pp_char_bool_fun "Find_opt" par fmt f | Find_index f -> cst1 pp_char_bool_fun "Find_index" par fmt f | Sort -> cst0 "Sort" fmt + | Stable_sort -> cst0 "Stable_sort" fmt + | Fast_sort -> cst0 "Fast_sort" fmt | To_seq -> cst0 "To_seq" fmt let show_cmd = Util.Pp.to_show pp_cmd @@ -67,6 +71,8 @@ struct map (fun f -> Find_opt f) (fun1 Observable.char QCheck.bool).gen; map (fun f -> Find_index f) (fun1 Observable.char QCheck.bool).gen; return Sort; + return Stable_sort; + return Fast_sort; return To_seq; ]) @@ -93,6 +99,8 @@ struct | Find_opt _ -> s | Find_index _ -> s | Sort -> List.sort Char.compare s + | Stable_sort -> List.stable_sort Char.compare s + | Fast_sort -> List.fast_sort Char.compare s | To_seq -> s let init_sut () = Array.make array_size 'a' @@ -115,6 +123,8 @@ struct | Find_opt (Fun (_,f)) -> Res (option char, Array.find_opt f a) | Find_index (Fun (_,f)) -> Res (option int, Array.find_index f a) | Sort -> Res (unit, Array.sort Char.compare a) + | Stable_sort -> Res (unit, Array.stable_sort Char.compare a) + | Fast_sort -> Res (unit, Array.fast_sort Char.compare a) | To_seq -> Res (seq char, List.to_seq (List.of_seq (Array.to_seq a))) (* workaround: Array.to_seq is lazy and will otherwise see and report later Array.set state changes... *) let postcond c (s:char list) res = match c, res with @@ -143,6 +153,8 @@ struct | Find_opt (Fun (_,f)), Res ((Option Char,_),r) -> r = List.find_opt f s | Find_index (Fun (_,f)), Res ((Option Int,_),r) -> r = List.find_index f s | Sort, Res ((Unit,_),r) -> r = () + | Stable_sort, Res ((Unit,_),r) -> r = () + | Fast_sort, Res ((Unit,_),r) -> r = () | To_seq, Res ((Seq Char,_),r) -> Seq.equal (=) r (List.to_seq s) | _, _ -> false end From affbb377be08d971e40f47722fa4fe2cc0b1051f Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Mon, 13 Nov 2023 10:15:38 +0100 Subject: [PATCH 4/4] Disable Array.find_index which is not available in 5.0 --- src/array/stm_tests.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/array/stm_tests.ml b/src/array/stm_tests.ml index 3af9492b..2e012438 100644 --- a/src/array/stm_tests.ml +++ b/src/array/stm_tests.ml @@ -22,7 +22,7 @@ struct | Exists of char_bool_fun | Mem of char | Find_opt of char_bool_fun - | Find_index of char_bool_fun + (*| Find_index of char_bool_fun since 5.1*) | Sort | Stable_sort | Fast_sort @@ -42,7 +42,7 @@ struct | Exists f -> cst1 pp_char_bool_fun "Exists" par fmt f | Mem x -> cst1 pp_char "Mem" par fmt x | Find_opt f -> cst1 pp_char_bool_fun "Find_opt" par fmt f - | Find_index f -> cst1 pp_char_bool_fun "Find_index" par fmt f + (*| Find_index f -> cst1 pp_char_bool_fun "Find_index" par fmt f*) | Sort -> cst0 "Sort" fmt | Stable_sort -> cst0 "Stable_sort" fmt | Fast_sort -> cst0 "Fast_sort" fmt @@ -69,7 +69,7 @@ struct map (fun f -> Exists f) (fun1 Observable.char QCheck.bool).gen; map (fun c -> Mem c) char_gen; map (fun f -> Find_opt f) (fun1 Observable.char QCheck.bool).gen; - map (fun f -> Find_index f) (fun1 Observable.char QCheck.bool).gen; + (*map (fun f -> Find_index f) (fun1 Observable.char QCheck.bool).gen;*) return Sort; return Stable_sort; return Fast_sort; @@ -97,7 +97,7 @@ struct | Exists _ -> s | Mem _ -> s | Find_opt _ -> s - | Find_index _ -> s + (*| Find_index _ -> s*) | Sort -> List.sort Char.compare s | Stable_sort -> List.stable_sort Char.compare s | Fast_sort -> List.fast_sort Char.compare s @@ -121,7 +121,7 @@ struct | Exists (Fun (_,f)) -> Res (bool, Array.exists f a) | Mem c -> Res (bool, Array.mem c a) | Find_opt (Fun (_,f)) -> Res (option char, Array.find_opt f a) - | Find_index (Fun (_,f)) -> Res (option int, Array.find_index f a) + (*| Find_index (Fun (_,f)) -> Res (option int, Array.find_index f a)*) | Sort -> Res (unit, Array.sort Char.compare a) | Stable_sort -> Res (unit, Array.stable_sort Char.compare a) | Fast_sort -> Res (unit, Array.fast_sort Char.compare a) @@ -151,7 +151,7 @@ struct | Exists (Fun (_,f)), Res ((Bool,_),r) -> r = List.exists f s | Mem c, Res ((Bool,_),r) -> r = List.mem c s | Find_opt (Fun (_,f)), Res ((Option Char,_),r) -> r = List.find_opt f s - | Find_index (Fun (_,f)), Res ((Option Int,_),r) -> r = List.find_index f s + (*| Find_index (Fun (_,f)), Res ((Option Int,_),r) -> r = List.find_index f s*) | Sort, Res ((Unit,_),r) -> r = () | Stable_sort, Res ((Unit,_),r) -> r = () | Fast_sort, Res ((Unit,_),r) -> r = ()