From 71083dd3b92438419263d5f0c22c1f478c925b80 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 15 Jun 2023 10:23:15 +0200 Subject: [PATCH 01/53] Initial STM tests of Out_channel --- src/io/dune | 8 ++++ src/io/stm_tests.ml | 102 ++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 110 insertions(+) create mode 100644 src/io/stm_tests.ml diff --git a/src/io/dune b/src/io/dune index 76cf14c4..d296546e 100644 --- a/src/io/dune +++ b/src/io/dune @@ -37,3 +37,11 @@ ; (action (run %{test} --verbose)) (action (echo "Skipping src/io/%{test} from the test suite\n\n")) ) + +(test + (name stm_tests) + (modules stm_tests) + (package multicoretests) + (libraries qcheck-stm.sequential qcheck-stm.domain) + (action (run %{test} --verbose)) +) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml new file mode 100644 index 00000000..56c7e27b --- /dev/null +++ b/src/io/stm_tests.ml @@ -0,0 +1,102 @@ +open QCheck +open STM + +(** parallel STM tests of Weak arrays *) + +module OCConf = +struct + type cmd = + (*| Seek of int64*) + | Pos + (*| Length*) + | Close + | Output_char of char + | Output_string of string + + let pp_cmd par fmt x = + let open Util.Pp in + match x with + (* | Seek i -> cst1 pp_int64 "Seek" par fmt i*) + | Pos -> cst0 "Pos" fmt + (* | Length -> cst0 "Length" fmt *) + | Close -> cst0 "Close" fmt + | Output_char c -> cst1 pp_char "Output_char" par fmt c + | Output_string s -> cst1 pp_string "Output_string" par fmt s + + let show_cmd = Util.Pp.to_show pp_cmd + + (* a path and an open channel to that file; we need to keep the path + to cleanup after the test run *) + type sut = string * Out_channel.t + + (*type status = Open | Closed*) + type state = Closed + | Open of { position : int64 } + + let arb_cmd _s = + (*let int64_gen = Gen.(map Int64.of_int small_int) in*) + let char_gen = Gen.printable in + let string_gen = Gen.small_string in + QCheck.make ~print:show_cmd (*~shrink:shrink_cmd*) + Gen.(frequency + [ (*1,map (fun i -> Seek i) int64_gen;*) + 5,return Pos; + (*1,return Length;*) + 1,return Close; + 5,map (fun c -> Output_char c) char_gen; + 5,map (fun c -> Output_string c) string_gen; + ]) + + let init_state = Open { position = 0L } + + let next_state c s = match c,s with + | Pos,_ -> s + (* | Length,_ -> s *) + | Close, _ -> Closed + | Output_char _c, Closed -> s + | Output_char _c, Open {position} -> Open {position = Int64.succ position } + | Output_string _str, Closed -> s + | Output_string str, Open {position} -> Open {position = Int64.(add position (of_int (String.length str))) } + + let init_sut () = Filename.open_temp_file "lin-dsl-" "" + let cleanup (path, chan) = + Out_channel.close chan ; + Sys.remove path + + let precond c _s = match c with + | _ -> true + + let run c (_path,oc) = match c with + | Pos -> Res (result int64 exn, protect Out_channel.pos oc) + (* | Length -> Res (result int64 exn, protect Out_channel.length oc) *) + | Close -> Res (result unit exn, protect Out_channel.close oc) + | Output_char c -> Res (result unit exn, protect (Out_channel.output_char oc) c) + | Output_string s -> Res (result unit exn, protect (Out_channel.output_string oc) s) + + let postcond c (s:state) res = match c, res with + | Pos, Res ((Result (Int64,Exn),_), r) -> + (match s with + | Closed -> true (*r = Error (Invalid_argument "Pos exception") - unspecified *) + | Open {position} -> r = Ok position) + (* | Length, Res ((Int,_),i) -> i = List.length s *) + | Close, Res ((Result (Unit,Exn),_), r) -> + ((*match s with + | Closed -> r = Error (Invalid_argument "Close exception") + | Open {position = _} ->*) r = Ok ()) + | Output_char _c, Res ((Result (Unit,Exn),_), r) -> + s = Closed || r = Ok () (* print on closed unspecified *) + (* if s = Closed + then r = Error (Sys_error "Bad file descriptor") + else r = Ok () *) + | Output_string _c, Res ((Result (Unit,Exn),_), r) -> + s = Closed || r = Ok () (* print on closed unspecified *) + | _, _ -> false +end + +module OCSTM_seq = STM_sequential.Make(OCConf) +module OCSTM_dom = STM_domain.Make(OCConf) +;; +QCheck_base_runner.run_tests_main [ + OCSTM_seq.agree_test ~count:1000 ~name:"STM Out_channel test sequential"; + OCSTM_dom.agree_test_par ~count:1000 ~name:"STM Out_channel test parallel"; + ] From 5e3f2e8392cb46e087e551117fc971992634c6d8 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 16 Jun 2023 23:41:32 +0200 Subject: [PATCH 02/53] More Out_channel STM hacking --- src/io/stm_tests.ml | 149 +++++++++++++++++++++++++++++++++----------- 1 file changed, 112 insertions(+), 37 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 56c7e27b..3c17e04e 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -6,20 +6,24 @@ open STM module OCConf = struct type cmd = + | Open_text (*| Seek of int64*) | Pos - (*| Length*) + | Length | Close + | Flush | Output_char of char | Output_string of string let pp_cmd par fmt x = let open Util.Pp in match x with - (* | Seek i -> cst1 pp_int64 "Seek" par fmt i*) + | Open_text -> cst0 "Open_text" fmt + (*| Seek i -> cst1 pp_int64 "Seek" par fmt i*) | Pos -> cst0 "Pos" fmt - (* | Length -> cst0 "Length" fmt *) + | Length -> cst0 "Length" fmt | Close -> cst0 "Close" fmt + | Flush -> cst0 "Flush" fmt | Output_char c -> cst1 pp_char "Output_char" par fmt c | Output_string s -> cst1 pp_string "Output_string" par fmt s @@ -27,76 +31,147 @@ struct (* a path and an open channel to that file; we need to keep the path to cleanup after the test run *) - type sut = string * Out_channel.t + type sut = { path : string; + mutable channel : Out_channel.t } - (*type status = Open | Closed*) - type state = Closed - | Open of { position : int64 } + (*type status = Opened | Closed*) + type state = Closed of int64 + | Open of { position : int64; + length : int64; } - let arb_cmd _s = - (*let int64_gen = Gen.(map Int64.of_int small_int) in*) + let arb_cmd s = + let _int64_gen = Gen.(map Int64.of_int small_int) in let char_gen = Gen.printable in let string_gen = Gen.small_string in QCheck.make ~print:show_cmd (*~shrink:shrink_cmd*) - Gen.(frequency - [ (*1,map (fun i -> Seek i) int64_gen;*) - 5,return Pos; - (*1,return Length;*) - 1,return Close; - 5,map (fun c -> Output_char c) char_gen; - 5,map (fun c -> Output_string c) string_gen; - ]) + (match s with + | Closed _ -> Gen.return Open_text + | Open _ -> + Gen.(frequency + [ + (*1,return Open_text;*) + (*3,map (fun i -> Seek i) int64_gen;*) + 3,return Pos; + 3,return Length; + 1,return Close; + 3,return Flush; + 3,map (fun c -> Output_char c) char_gen; + 3,map (fun c -> Output_string c) string_gen; + ])) - let init_state = Open { position = 0L } + let init_state = Closed 0L (*Open { position = 0L; length = 0L }*) let next_state c s = match c,s with + | Open_text, Closed _l -> Open { position = 0L; length = (*l*) 0L } + | Open_text, Open _ -> s +(* | Seek _, Closed _ -> s + | Seek p, Open _ -> Open { position = p; length = (*l*) 0L }*) | Pos,_ -> s - (* | Length,_ -> s *) - | Close, _ -> Closed - | Output_char _c, Closed -> s - | Output_char _c, Open {position} -> Open {position = Int64.succ position } - | Output_string _str, Closed -> s - | Output_string str, Open {position} -> Open {position = Int64.(add position (of_int (String.length str))) } - - let init_sut () = Filename.open_temp_file "lin-dsl-" "" - let cleanup (path, chan) = - Out_channel.close chan ; + | Length,_ -> s + | Close, Open { position = _; length = _ } -> Closed 0L(*length*) + | Close, Closed _ -> s + | Flush, Open _ -> s(*length*) + | Flush, Closed _ -> s + | Output_char _c, Closed _ -> s + | Output_char _c, Open {position; length = _} -> + Open {position = Int64.succ position; + length = (*Int64.succ length*)0L; } + | Output_string _str, Closed _ -> s + | Output_string str, Open {position; length = _} -> + let str_len = Int64.of_int (String.length str) in + Open {position = Int64.add position str_len; + length = (*Int64.add length str_len*) 0L; } + + let init_sut () = + let path = Filename.temp_file "lin-dsl-" "" in + (*Printf.printf "init_sut %s\n%!" path;*) + let channel = Stdlib.stdout in + (*let path, channel = Filename.open_temp_file "lin-dsl-" "" in*) + { path; channel } + let cleanup { path; channel } = + if channel <> Stdlib.stdout + then Out_channel.close channel; + (*Printf.printf "Removing %s\n%!" path;*) Sys.remove path - let precond c _s = match c with - | _ -> true + let precond c s = match c,s with + | Open_text, Closed _ -> true + | Open_text, Open _ -> false + | _, Open _ -> true + | _, _ -> false - let run c (_path,oc) = match c with + let run c ({path;channel = oc} as r) = match c with + | Open_text -> Res (result unit exn, protect (fun path -> (r.channel <- Out_channel.open_text path;())) path) + (*| Seek p -> Res (unit, Out_channel.seek oc p)*) | Pos -> Res (result int64 exn, protect Out_channel.pos oc) - (* | Length -> Res (result int64 exn, protect Out_channel.length oc) *) + | Length -> Res (int64, Out_channel.length oc) | Close -> Res (result unit exn, protect Out_channel.close oc) + | Flush -> Res (unit, Out_channel.flush oc) | Output_char c -> Res (result unit exn, protect (Out_channel.output_char oc) c) | Output_string s -> Res (result unit exn, protect (Out_channel.output_string oc) s) let postcond c (s:state) res = match c, res with + | Open_text, Res ((Result (Unit,Exn),_), r) -> + (match s,r with + | Closed _, Ok () + | Closed _, Error (Sys_error _) (*"/tmp/lin-dsl-03ba23: Too many open files"*) + | Open _, Ok () + | Open _, Error (Sys_error _) -> true + | _ -> false) + (*| Seek _, Res ((Unit,_), ()) -> true*) | Pos, Res ((Result (Int64,Exn),_), r) -> (match s with - | Closed -> true (*r = Error (Invalid_argument "Pos exception") - unspecified *) - | Open {position} -> r = Ok position) - (* | Length, Res ((Int,_),i) -> i = List.length s *) + | Closed _ -> true (*r = Error (Invalid_argument "Pos exception") - unspecified *) + | Open {position;length = _} -> r = Ok position) + | Length, Res ((Int64,_),i) -> + (*Printf.printf "Length returned %Li\n%!" i;*) + (match s with + | Closed _ -> true + | Open { position = _; length = _ } -> i = 0L) | Close, Res ((Result (Unit,Exn),_), r) -> ((*match s with | Closed -> r = Error (Invalid_argument "Close exception") | Open {position = _} ->*) r = Ok ()) + | Flush, Res ((Unit,_), r) -> r = () | Output_char _c, Res ((Result (Unit,Exn),_), r) -> - s = Closed || r = Ok () (* print on closed unspecified *) + (match s with + | Closed _ -> true + | Open _ -> r = Ok ()) (* print on closed unspecified *) (* if s = Closed then r = Error (Sys_error "Bad file descriptor") else r = Ok () *) | Output_string _c, Res ((Result (Unit,Exn),_), r) -> - s = Closed || r = Ok () (* print on closed unspecified *) + (match s with + | Closed _ -> true + | Open _ -> r = Ok ()) (* print on closed unspecified *) | _, _ -> false end module OCSTM_seq = STM_sequential.Make(OCConf) module OCSTM_dom = STM_domain.Make(OCConf) + +let print_seq_trace trace = + List.fold_left + (fun acc c -> Printf.sprintf "%s\n %s" acc (OCConf.show_cmd c)) + "" trace + +let _seq_agree_test = + Test.make ~count:1000 ~name:"STM Out_channel test sequential" + (OCSTM_seq.arb_cmds OCConf.init_state) + (fun seq -> + try + Printf.printf "%s\n%!" (print_seq_trace seq); + let r = OCSTM_seq.agree_prop seq in + Printf.printf "Prop: %s\n%!" (if r then "true" else "false"); + r + with e -> + Printf.printf "Prop: false\n%!"; + raise e + ) + ;; QCheck_base_runner.run_tests_main [ + (*seq_agree_test;*) OCSTM_seq.agree_test ~count:1000 ~name:"STM Out_channel test sequential"; OCSTM_dom.agree_test_par ~count:1000 ~name:"STM Out_channel test parallel"; ] From 72a5458eddf6cbff98fb01c280c2f1d7a3869a55 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 13:51:59 +0100 Subject: [PATCH 03/53] Update positions accordingly --- src/io/stm_tests.ml | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 3c17e04e..f02684f0 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -73,14 +73,14 @@ struct | Flush, Open _ -> s(*length*) | Flush, Closed _ -> s | Output_char _c, Closed _ -> s - | Output_char _c, Open {position; length = _} -> + | Output_char _c, Open { position; length } -> Open {position = Int64.succ position; - length = (*Int64.succ length*)0L; } + length = Int64.succ length; } | Output_string _str, Closed _ -> s - | Output_string str, Open {position; length = _} -> + | Output_string str, Open { position; length } -> let str_len = Int64.of_int (String.length str) in Open {position = Int64.add position str_len; - length = (*Int64.add length str_len*) 0L; } + length = Int64.add length str_len; } let init_sut () = let path = Filename.temp_file "lin-dsl-" "" in @@ -127,7 +127,7 @@ struct (*Printf.printf "Length returned %Li\n%!" i;*) (match s with | Closed _ -> true - | Open { position = _; length = _ } -> i = 0L) + | Open { position = _; length } -> i = length) | Close, Res ((Result (Unit,Exn),_), r) -> ((*match s with | Closed -> r = Error (Invalid_argument "Close exception") From fc97895fea10727c5c90d60cb87642669c393c90 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 13:54:28 +0100 Subject: [PATCH 04/53] Length before flushing may not be up-to-date --- src/io/stm_tests.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index f02684f0..7458e34d 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -127,7 +127,7 @@ struct (*Printf.printf "Length returned %Li\n%!" i;*) (match s with | Closed _ -> true - | Open { position = _; length } -> i = length) + | Open { position = _; length } -> i <= length) | Close, Res ((Result (Unit,Exn),_), r) -> ((*match s with | Closed -> r = Error (Invalid_argument "Close exception") From 46774d6af247a50703603b6698ba45eec5c513a9 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 13:58:31 +0100 Subject: [PATCH 05/53] Whitespace/comment polish --- src/io/stm_tests.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 7458e34d..7463b54e 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -1,7 +1,7 @@ open QCheck open STM -(** parallel STM tests of Weak arrays *) +(** parallel STM tests of Out_channels *) module OCConf = struct @@ -172,6 +172,6 @@ let _seq_agree_test = ;; QCheck_base_runner.run_tests_main [ (*seq_agree_test;*) - OCSTM_seq.agree_test ~count:1000 ~name:"STM Out_channel test sequential"; - OCSTM_dom.agree_test_par ~count:1000 ~name:"STM Out_channel test parallel"; + OCSTM_seq.agree_test ~count:1000 ~name:"STM Out_channel test sequential"; + OCSTM_dom.agree_test_par ~count:1000 ~name:"STM Out_channel test parallel"; ] From 894c6435751b5bcb02c0e4316dffd72b154dcc03 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 14:17:24 +0100 Subject: [PATCH 06/53] Add Seek cmd --- src/io/stm_tests.ml | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 7463b54e..e33e0b5f 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -7,7 +7,7 @@ module OCConf = struct type cmd = | Open_text - (*| Seek of int64*) + | Seek of int64 | Pos | Length | Close @@ -19,7 +19,7 @@ struct let open Util.Pp in match x with | Open_text -> cst0 "Open_text" fmt - (*| Seek i -> cst1 pp_int64 "Seek" par fmt i*) + | Seek i -> cst1 pp_int64 "Seek" par fmt i | Pos -> cst0 "Pos" fmt | Length -> cst0 "Length" fmt | Close -> cst0 "Close" fmt @@ -40,7 +40,7 @@ struct length : int64; } let arb_cmd s = - let _int64_gen = Gen.(map Int64.of_int small_int) in + let int64_gen = Gen.(map Int64.of_int small_int) in let char_gen = Gen.printable in let string_gen = Gen.small_string in QCheck.make ~print:show_cmd (*~shrink:shrink_cmd*) @@ -50,7 +50,7 @@ struct Gen.(frequency [ (*1,return Open_text;*) - (*3,map (fun i -> Seek i) int64_gen;*) + 3,map (fun i -> Seek i) int64_gen; 3,return Pos; 3,return Length; 1,return Close; @@ -64,13 +64,13 @@ struct let next_state c s = match c,s with | Open_text, Closed _l -> Open { position = 0L; length = (*l*) 0L } | Open_text, Open _ -> s -(* | Seek _, Closed _ -> s - | Seek p, Open _ -> Open { position = p; length = (*l*) 0L }*) + | Seek _, Closed _ -> s + | Seek p, Open { position = _; length } -> Open { position = p; length = Int64.max length p } | Pos,_ -> s | Length,_ -> s | Close, Open { position = _; length = _ } -> Closed 0L(*length*) | Close, Closed _ -> s - | Flush, Open _ -> s(*length*) + | Flush, Open _ -> s | Flush, Closed _ -> s | Output_char _c, Closed _ -> s | Output_char _c, Open { position; length } -> @@ -102,7 +102,7 @@ struct let run c ({path;channel = oc} as r) = match c with | Open_text -> Res (result unit exn, protect (fun path -> (r.channel <- Out_channel.open_text path;())) path) - (*| Seek p -> Res (unit, Out_channel.seek oc p)*) + | Seek p -> Res (unit, Out_channel.seek oc p) | Pos -> Res (result int64 exn, protect Out_channel.pos oc) | Length -> Res (int64, Out_channel.length oc) | Close -> Res (result unit exn, protect Out_channel.close oc) @@ -118,7 +118,7 @@ struct | Open _, Ok () | Open _, Error (Sys_error _) -> true | _ -> false) - (*| Seek _, Res ((Unit,_), ()) -> true*) + | Seek _, Res ((Unit,_), ()) -> true | Pos, Res ((Result (Int64,Exn),_), r) -> (match s with | Closed _ -> true (*r = Error (Invalid_argument "Pos exception") - unspecified *) From c3677add7e1acbcea415313f298b631395aca643 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 14:48:48 +0100 Subject: [PATCH 07/53] Add close_noerr cmd --- src/io/stm_tests.ml | 43 +++++++++++++++++++++++++++---------------- 1 file changed, 27 insertions(+), 16 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index e33e0b5f..18cb1e21 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -11,6 +11,7 @@ struct | Pos | Length | Close + | Close_noerr | Flush | Output_char of char | Output_string of string @@ -23,6 +24,7 @@ struct | Pos -> cst0 "Pos" fmt | Length -> cst0 "Length" fmt | Close -> cst0 "Close" fmt + | Close_noerr -> cst0 "Close_noerr" fmt | Flush -> cst0 "Flush" fmt | Output_char c -> cst1 pp_char "Output_char" par fmt c | Output_string s -> cst1 pp_string "Output_string" par fmt s @@ -45,19 +47,19 @@ struct let string_gen = Gen.small_string in QCheck.make ~print:show_cmd (*~shrink:shrink_cmd*) (match s with - | Closed _ -> Gen.return Open_text + | Closed _ -> Gen.return Open_text (* close can trigger a fatal error *) | Open _ -> - Gen.(frequency - [ - (*1,return Open_text;*) - 3,map (fun i -> Seek i) int64_gen; - 3,return Pos; - 3,return Length; - 1,return Close; - 3,return Flush; - 3,map (fun c -> Output_char c) char_gen; - 3,map (fun c -> Output_string c) string_gen; - ])) + Gen.(frequency [ + (*1,return Open_text;*) + 5,map (fun i -> Seek i) int64_gen; + 5,return Pos; + 5,return Length; + 1,return Close; + 1,return Close_noerr; + 5,return Flush; + 5,map (fun c -> Output_char c) char_gen; + 5,map (fun c -> Output_string c) string_gen; + ])) let init_state = Closed 0L (*Open { position = 0L; length = 0L }*) @@ -68,8 +70,10 @@ struct | Seek p, Open { position = _; length } -> Open { position = p; length = Int64.max length p } | Pos,_ -> s | Length,_ -> s - | Close, Open { position = _; length = _ } -> Closed 0L(*length*) + | Close, Open { position = _; length = _ } -> Closed 0L | Close, Closed _ -> s + | Close_noerr, Open { position = _; length = _ } -> Closed 0L + | Close_noerr, Closed _ -> s | Flush, Open _ -> s | Flush, Closed _ -> s | Output_char _c, Closed _ -> s @@ -88,6 +92,7 @@ struct let channel = Stdlib.stdout in (*let path, channel = Filename.open_temp_file "lin-dsl-" "" in*) { path; channel } + let cleanup { path; channel } = if channel <> Stdlib.stdout then Out_channel.close channel; @@ -106,6 +111,7 @@ struct | Pos -> Res (result int64 exn, protect Out_channel.pos oc) | Length -> Res (int64, Out_channel.length oc) | Close -> Res (result unit exn, protect Out_channel.close oc) + | Close_noerr -> Res (unit, Out_channel.close_noerr oc) | Flush -> Res (unit, Out_channel.flush oc) | Output_char c -> Res (result unit exn, protect (Out_channel.output_char oc) c) | Output_string s -> Res (result unit exn, protect (Out_channel.output_string oc) s) @@ -129,9 +135,14 @@ struct | Closed _ -> true | Open { position = _; length } -> i <= length) | Close, Res ((Result (Unit,Exn),_), r) -> - ((*match s with - | Closed -> r = Error (Invalid_argument "Close exception") - | Open {position = _} ->*) r = Ok ()) + (match s,r with + | Closed _, Error (Sys_error _) (*"Close exception" - unspecified *) + | Open {position = _; length = _}, Ok () -> true + | _ -> false) + | Close_noerr, Res ((Unit,_), r) -> + (match s,r with + | Closed _, () + | Open {position = _; length = _}, () -> true) | Flush, Res ((Unit,_), r) -> r = () | Output_char _c, Res ((Result (Unit,Exn),_), r) -> (match s with From 04a0f95c62cceece21f43cb071dbdd49e1cd5765 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 14:53:16 +0100 Subject: [PATCH 08/53] Add output_byte cmd --- src/io/stm_tests.ml | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 18cb1e21..0d7a734c 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -14,6 +14,7 @@ struct | Close_noerr | Flush | Output_char of char + | Output_byte of int | Output_string of string let pp_cmd par fmt x = @@ -27,6 +28,7 @@ struct | Close_noerr -> cst0 "Close_noerr" fmt | Flush -> cst0 "Flush" fmt | Output_char c -> cst1 pp_char "Output_char" par fmt c + | Output_byte i -> cst1 pp_int "Output_byte" par fmt i | Output_string s -> cst1 pp_string "Output_string" par fmt s let show_cmd = Util.Pp.to_show pp_cmd @@ -44,6 +46,7 @@ struct let arb_cmd s = let int64_gen = Gen.(map Int64.of_int small_int) in let char_gen = Gen.printable in + let byte_gen = Gen.small_int in let string_gen = Gen.small_string in QCheck.make ~print:show_cmd (*~shrink:shrink_cmd*) (match s with @@ -58,6 +61,7 @@ struct 1,return Close_noerr; 5,return Flush; 5,map (fun c -> Output_char c) char_gen; + 5,map (fun i -> Output_byte i) byte_gen; 5,map (fun c -> Output_string c) string_gen; ])) @@ -80,6 +84,10 @@ struct | Output_char _c, Open { position; length } -> Open {position = Int64.succ position; length = Int64.succ length; } + | Output_byte _i, Closed _ -> s + | Output_byte _i, Open { position; length } -> + Open {position = Int64.succ position; + length = Int64.succ length; } | Output_string _str, Closed _ -> s | Output_string str, Open { position; length } -> let str_len = Int64.of_int (String.length str) in @@ -114,6 +122,7 @@ struct | Close_noerr -> Res (unit, Out_channel.close_noerr oc) | Flush -> Res (unit, Out_channel.flush oc) | Output_char c -> Res (result unit exn, protect (Out_channel.output_char oc) c) + | Output_byte i -> Res (result unit exn, protect (Out_channel.output_byte oc) i) | Output_string s -> Res (result unit exn, protect (Out_channel.output_string oc) s) let postcond c (s:state) res = match c, res with @@ -148,9 +157,10 @@ struct (match s with | Closed _ -> true | Open _ -> r = Ok ()) (* print on closed unspecified *) - (* if s = Closed - then r = Error (Sys_error "Bad file descriptor") - else r = Ok () *) + | Output_byte _i, Res ((Result (Unit,Exn),_), r) -> + (match s with + | Closed _ -> true + | Open _ -> r = Ok ()) (* print on closed unspecified *) | Output_string _c, Res ((Result (Unit,Exn),_), r) -> (match s with | Closed _ -> true From c69ec6d35087f75822b938b09b57ea0fb90eb547 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 15:10:21 +0100 Subject: [PATCH 09/53] Add output_bytes cmd --- src/io/stm_tests.ml | 22 ++++++++++++++++++---- 1 file changed, 18 insertions(+), 4 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 0d7a734c..bb3e83d4 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -16,6 +16,7 @@ struct | Output_char of char | Output_byte of int | Output_string of string + | Output_bytes of bytes let pp_cmd par fmt x = let open Util.Pp in @@ -30,6 +31,7 @@ struct | Output_char c -> cst1 pp_char "Output_char" par fmt c | Output_byte i -> cst1 pp_int "Output_byte" par fmt i | Output_string s -> cst1 pp_string "Output_string" par fmt s + | Output_bytes b -> cst1 pp_bytes "Output_bytes" par fmt b let show_cmd = Util.Pp.to_show pp_cmd @@ -48,6 +50,7 @@ struct let char_gen = Gen.printable in let byte_gen = Gen.small_int in let string_gen = Gen.small_string in + let bytes_gen = Gen.bytes_small in QCheck.make ~print:show_cmd (*~shrink:shrink_cmd*) (match s with | Closed _ -> Gen.return Open_text (* close can trigger a fatal error *) @@ -63,6 +66,7 @@ struct 5,map (fun c -> Output_char c) char_gen; 5,map (fun i -> Output_byte i) byte_gen; 5,map (fun c -> Output_string c) string_gen; + 5,map (fun b -> Output_bytes b) bytes_gen; ])) let init_state = Closed 0L (*Open { position = 0L; length = 0L }*) @@ -90,9 +94,14 @@ struct length = Int64.succ length; } | Output_string _str, Closed _ -> s | Output_string str, Open { position; length } -> - let str_len = Int64.of_int (String.length str) in - Open {position = Int64.add position str_len; - length = Int64.add length str_len; } + let len = Int64.of_int (String.length str) in + Open {position = Int64.add position len; + length = Int64.add length len; } + | Output_bytes _str, Closed _ -> s + | Output_bytes b, Open { position; length } -> + let len = Int64.of_int (Bytes.length b) in + Open {position = Int64.add position len; + length = Int64.add length len; } let init_sut () = let path = Filename.temp_file "lin-dsl-" "" in @@ -124,6 +133,7 @@ struct | Output_char c -> Res (result unit exn, protect (Out_channel.output_char oc) c) | Output_byte i -> Res (result unit exn, protect (Out_channel.output_byte oc) i) | Output_string s -> Res (result unit exn, protect (Out_channel.output_string oc) s) + | Output_bytes b -> Res (result unit exn, protect (Out_channel.output_bytes oc) b) let postcond c (s:state) res = match c, res with | Open_text, Res ((Result (Unit,Exn),_), r) -> @@ -161,7 +171,11 @@ struct (match s with | Closed _ -> true | Open _ -> r = Ok ()) (* print on closed unspecified *) - | Output_string _c, Res ((Result (Unit,Exn),_), r) -> + | Output_string _s, Res ((Result (Unit,Exn),_), r) -> + (match s with + | Closed _ -> true + | Open _ -> r = Ok ()) (* print on closed unspecified *) + | Output_bytes _b, Res ((Result (Unit,Exn),_), r) -> (match s with | Closed _ -> true | Open _ -> r = Ok ()) (* print on closed unspecified *) From f4aede152548966bf07cb6c4f0f6a082a47dcde3 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 15:33:02 +0100 Subject: [PATCH 10/53] Add output cmd --- src/io/stm_tests.ml | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index bb3e83d4..f01c47cc 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -17,6 +17,7 @@ struct | Output_byte of int | Output_string of string | Output_bytes of bytes + | Output of bytes * int * int let pp_cmd par fmt x = let open Util.Pp in @@ -32,6 +33,7 @@ struct | Output_byte i -> cst1 pp_int "Output_byte" par fmt i | Output_string s -> cst1 pp_string "Output_string" par fmt s | Output_bytes b -> cst1 pp_bytes "Output_bytes" par fmt b + | Output (b,p,l) -> cst3 pp_bytes pp_int pp_int "Output" par fmt b p l let show_cmd = Util.Pp.to_show pp_cmd @@ -67,6 +69,7 @@ struct 5,map (fun i -> Output_byte i) byte_gen; 5,map (fun c -> Output_string c) string_gen; 5,map (fun b -> Output_bytes b) bytes_gen; + 5,map3 (fun b p l -> Output (b,p,l)) bytes_gen byte_gen byte_gen; ])) let init_state = Closed 0L (*Open { position = 0L; length = 0L }*) @@ -102,6 +105,16 @@ struct let len = Int64.of_int (Bytes.length b) in Open {position = Int64.add position len; length = Int64.add length len; } + | Output (_,_,_), Closed _ -> s + | Output (b,p,l), Open { position; length } -> + let bytes_len = Bytes.length b in + if 0 <= p && p < bytes_len && + 0 <= l && p+l <= bytes_len + then + let len = Int64.of_int l in + Open {position = Int64.add position len; + length = Int64.add length len; } + else s let init_sut () = let path = Filename.temp_file "lin-dsl-" "" in @@ -134,6 +147,7 @@ struct | Output_byte i -> Res (result unit exn, protect (Out_channel.output_byte oc) i) | Output_string s -> Res (result unit exn, protect (Out_channel.output_string oc) s) | Output_bytes b -> Res (result unit exn, protect (Out_channel.output_bytes oc) b) + | Output (b,p,l) -> Res (result unit exn, protect (Out_channel.output oc b p) l) let postcond c (s:state) res = match c, res with | Open_text, Res ((Result (Unit,Exn),_), r) -> @@ -179,6 +193,14 @@ struct (match s with | Closed _ -> true | Open _ -> r = Ok ()) (* print on closed unspecified *) + | Output (b,p,l), Res ((Result (Unit,Exn),_), r) -> + (match s,r with + | Closed _,_ + | Open _, Ok () -> true + | Open _, Error (Invalid_argument _) -> (*"output"*) + let bytes_len = Bytes.length b in + p < 0 || p >= bytes_len || l < 0 || p+l > bytes_len + | Open _, _ -> false) | _, _ -> false end From f89ee562ac294b1b4c9a87480ab566174f5bf9a2 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 15:40:13 +0100 Subject: [PATCH 11/53] Add output_substring cmd --- src/io/stm_tests.ml | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index f01c47cc..fbea7e28 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -18,6 +18,7 @@ struct | Output_string of string | Output_bytes of bytes | Output of bytes * int * int + | Output_substring of string * int * int let pp_cmd par fmt x = let open Util.Pp in @@ -34,6 +35,7 @@ struct | Output_string s -> cst1 pp_string "Output_string" par fmt s | Output_bytes b -> cst1 pp_bytes "Output_bytes" par fmt b | Output (b,p,l) -> cst3 pp_bytes pp_int pp_int "Output" par fmt b p l + | Output_substring (s,p,l) -> cst3 pp_string pp_int pp_int "Output_substring" par fmt s p l let show_cmd = Util.Pp.to_show pp_cmd @@ -70,6 +72,7 @@ struct 5,map (fun c -> Output_string c) string_gen; 5,map (fun b -> Output_bytes b) bytes_gen; 5,map3 (fun b p l -> Output (b,p,l)) bytes_gen byte_gen byte_gen; + 5,map3 (fun s p l -> Output_substring (s,p,l)) string_gen byte_gen byte_gen; ])) let init_state = Closed 0L (*Open { position = 0L; length = 0L }*) @@ -115,6 +118,16 @@ struct Open {position = Int64.add position len; length = Int64.add length len; } else s + | Output_substring (_,_,_), Closed _ -> s + | Output_substring (str,p,l), Open { position; length } -> + let str_len = String.length str in + if 0 <= p && p < str_len && + 0 <= l && p+l <= str_len + then + let len = Int64.of_int l in + Open {position = Int64.add position len; + length = Int64.add length len; } + else s let init_sut () = let path = Filename.temp_file "lin-dsl-" "" in @@ -148,6 +161,7 @@ struct | Output_string s -> Res (result unit exn, protect (Out_channel.output_string oc) s) | Output_bytes b -> Res (result unit exn, protect (Out_channel.output_bytes oc) b) | Output (b,p,l) -> Res (result unit exn, protect (Out_channel.output oc b p) l) + | Output_substring (s,p,l) -> Res (result unit exn, protect (Out_channel.output_substring oc s p) l) let postcond c (s:state) res = match c, res with | Open_text, Res ((Result (Unit,Exn),_), r) -> @@ -201,6 +215,14 @@ struct let bytes_len = Bytes.length b in p < 0 || p >= bytes_len || l < 0 || p+l > bytes_len | Open _, _ -> false) + | Output_substring (str,p,l), Res ((Result (Unit,Exn),_), r) -> + (match s,r with + | Closed _,_ + | Open _, Ok () -> true + | Open _, Error (Invalid_argument _) -> (*"output_substring"*) + let str_len = String.length str in + p < 0 || p >= str_len || l < 0 || p+l > str_len + | Open _, _ -> false) | _, _ -> false end From a90cd1895a801ff6f09eec1c509ed41c5a743694 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 15:45:10 +0100 Subject: [PATCH 12/53] Adjust weights --- src/io/stm_tests.ml | 20 ++++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index fbea7e28..51f1cad2 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -61,18 +61,18 @@ struct | Open _ -> Gen.(frequency [ (*1,return Open_text;*) - 5,map (fun i -> Seek i) int64_gen; - 5,return Pos; - 5,return Length; + 3,map (fun i -> Seek i) int64_gen; + 3,return Pos; + 3,return Length; 1,return Close; 1,return Close_noerr; - 5,return Flush; - 5,map (fun c -> Output_char c) char_gen; - 5,map (fun i -> Output_byte i) byte_gen; - 5,map (fun c -> Output_string c) string_gen; - 5,map (fun b -> Output_bytes b) bytes_gen; - 5,map3 (fun b p l -> Output (b,p,l)) bytes_gen byte_gen byte_gen; - 5,map3 (fun s p l -> Output_substring (s,p,l)) string_gen byte_gen byte_gen; + 3,return Flush; + 3,map (fun c -> Output_char c) char_gen; + 3,map (fun i -> Output_byte i) byte_gen; + 3,map (fun c -> Output_string c) string_gen; + 3,map (fun b -> Output_bytes b) bytes_gen; + 3,map3 (fun b p l -> Output (b,p,l)) bytes_gen byte_gen byte_gen; + 3,map3 (fun s p l -> Output_substring (s,p,l)) string_gen byte_gen byte_gen; ])) let init_state = Closed 0L (*Open { position = 0L; length = 0L }*) From bfa89dfb8afade457b844c69d799a6852c9a1b68 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 15:56:00 +0100 Subject: [PATCH 13/53] Clean up next_state --- src/io/stm_tests.ml | 51 ++++++++++++++++++++++----------------------- 1 file changed, 25 insertions(+), 26 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 51f1cad2..a68168d6 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -75,59 +75,58 @@ struct 3,map3 (fun s p l -> Output_substring (s,p,l)) string_gen byte_gen byte_gen; ])) - let init_state = Closed 0L (*Open { position = 0L; length = 0L }*) + let init_state = Closed 0L let next_state c s = match c,s with - | Open_text, Closed _l -> Open { position = 0L; length = (*l*) 0L } + | Open_text, Closed _l -> Open { position = 0L; length = 0L } | Open_text, Open _ -> s - | Seek _, Closed _ -> s + (* non-open cmd on closed Out_channel *) + | Output_char _, Closed _ + | Output_byte _, Closed _ + | Output_string _, Closed _ + | Output_bytes _, Closed _ + | Output (_,_,_), Closed _ + | Output_substring (_,_,_), Closed _ + | Seek _, Closed _ + | Close, Closed _ + | Close_noerr, Closed _ + | Flush, Closed _ -> s + (* non-open cmd on open Out_channel *) | Seek p, Open { position = _; length } -> Open { position = p; length = Int64.max length p } | Pos,_ -> s | Length,_ -> s - | Close, Open { position = _; length = _ } -> Closed 0L - | Close, Closed _ -> s - | Close_noerr, Open { position = _; length = _ } -> Closed 0L - | Close_noerr, Closed _ -> s + | Close, Open _ -> Closed 0L + | Close_noerr, Open _ -> Closed 0L | Flush, Open _ -> s - | Flush, Closed _ -> s - | Output_char _c, Closed _ -> s - | Output_char _c, Open { position; length } -> - Open {position = Int64.succ position; - length = Int64.succ length; } - | Output_byte _i, Closed _ -> s - | Output_byte _i, Open { position; length } -> + (* output on open Out_channel *) + | Output_char _, Open { position; length } + | Output_byte _, Open { position; length } -> Open {position = Int64.succ position; length = Int64.succ length; } - | Output_string _str, Closed _ -> s | Output_string str, Open { position; length } -> let len = Int64.of_int (String.length str) in Open {position = Int64.add position len; length = Int64.add length len; } - | Output_bytes _str, Closed _ -> s | Output_bytes b, Open { position; length } -> let len = Int64.of_int (Bytes.length b) in Open {position = Int64.add position len; length = Int64.add length len; } - | Output (_,_,_), Closed _ -> s | Output (b,p,l), Open { position; length } -> let bytes_len = Bytes.length b in - if 0 <= p && p < bytes_len && - 0 <= l && p+l <= bytes_len - then + if p < 0 || p >= bytes_len || l < 0 || p+l > bytes_len + then s + else let len = Int64.of_int l in Open {position = Int64.add position len; length = Int64.add length len; } - else s - | Output_substring (_,_,_), Closed _ -> s | Output_substring (str,p,l), Open { position; length } -> let str_len = String.length str in - if 0 <= p && p < str_len && - 0 <= l && p+l <= str_len - then + if p < 0 || p >= str_len || l < 0 || p+l > str_len + then s + else let len = Int64.of_int l in Open {position = Int64.add position len; length = Int64.add length len; } - else s let init_sut () = let path = Filename.temp_file "lin-dsl-" "" in From 1bbef8860e0813631044044de01f779e0f52a238 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 15:57:54 +0100 Subject: [PATCH 14/53] Remove dead code --- src/io/stm_tests.ml | 21 --------------------- 1 file changed, 21 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index a68168d6..0f3c635e 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -227,29 +227,8 @@ end module OCSTM_seq = STM_sequential.Make(OCConf) module OCSTM_dom = STM_domain.Make(OCConf) - -let print_seq_trace trace = - List.fold_left - (fun acc c -> Printf.sprintf "%s\n %s" acc (OCConf.show_cmd c)) - "" trace - -let _seq_agree_test = - Test.make ~count:1000 ~name:"STM Out_channel test sequential" - (OCSTM_seq.arb_cmds OCConf.init_state) - (fun seq -> - try - Printf.printf "%s\n%!" (print_seq_trace seq); - let r = OCSTM_seq.agree_prop seq in - Printf.printf "Prop: %s\n%!" (if r then "true" else "false"); - r - with e -> - Printf.printf "Prop: false\n%!"; - raise e - ) - ;; QCheck_base_runner.run_tests_main [ - (*seq_agree_test;*) OCSTM_seq.agree_test ~count:1000 ~name:"STM Out_channel test sequential"; OCSTM_dom.agree_test_par ~count:1000 ~name:"STM Out_channel test parallel"; ] From 76ca5f7775e8a24c33d09463da28aa06856f317b Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 16:00:29 +0100 Subject: [PATCH 15/53] More code clean-ups --- src/io/stm_tests.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 0f3c635e..5e4b8d8f 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -44,7 +44,6 @@ struct type sut = { path : string; mutable channel : Out_channel.t } - (*type status = Opened | Closed*) type state = Closed of int64 | Open of { position : int64; length : int64; } @@ -176,19 +175,18 @@ struct | Closed _ -> true (*r = Error (Invalid_argument "Pos exception") - unspecified *) | Open {position;length = _} -> r = Ok position) | Length, Res ((Int64,_),i) -> - (*Printf.printf "Length returned %Li\n%!" i;*) (match s with | Closed _ -> true | Open { position = _; length } -> i <= length) | Close, Res ((Result (Unit,Exn),_), r) -> (match s,r with | Closed _, Error (Sys_error _) (*"Close exception" - unspecified *) - | Open {position = _; length = _}, Ok () -> true + | Open _, Ok () -> true | _ -> false) | Close_noerr, Res ((Unit,_), r) -> (match s,r with | Closed _, () - | Open {position = _; length = _}, () -> true) + | Open _, () -> true) | Flush, Res ((Unit,_), r) -> r = () | Output_char _c, Res ((Result (Unit,Exn),_), r) -> (match s with From b67b5608f9b1aa6af4a2746ec3eb6f614df20297 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 16:08:06 +0100 Subject: [PATCH 16/53] Add initial is_buffered cmd --- src/io/stm_tests.ml | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 5e4b8d8f..25e3052b 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -19,6 +19,7 @@ struct | Output_bytes of bytes | Output of bytes * int * int | Output_substring of string * int * int + | Is_buffered let pp_cmd par fmt x = let open Util.Pp in @@ -36,6 +37,7 @@ struct | Output_bytes b -> cst1 pp_bytes "Output_bytes" par fmt b | Output (b,p,l) -> cst3 pp_bytes pp_int pp_int "Output" par fmt b p l | Output_substring (s,p,l) -> cst3 pp_string pp_int pp_int "Output_substring" par fmt s p l + | Is_buffered -> cst0 "Is_buffered" fmt let show_cmd = Util.Pp.to_show pp_cmd @@ -72,6 +74,7 @@ struct 3,map (fun b -> Output_bytes b) bytes_gen; 3,map3 (fun b p l -> Output (b,p,l)) bytes_gen byte_gen byte_gen; 3,map3 (fun s p l -> Output_substring (s,p,l)) string_gen byte_gen byte_gen; + 3,return Is_buffered; ])) let init_state = Closed 0L @@ -88,15 +91,15 @@ struct | Output_substring (_,_,_), Closed _ | Seek _, Closed _ | Close, Closed _ - | Close_noerr, Closed _ - | Flush, Closed _ -> s + | Close_noerr, Closed _ -> s (* non-open cmd on open Out_channel *) | Seek p, Open { position = _; length } -> Open { position = p; length = Int64.max length p } | Pos,_ -> s | Length,_ -> s | Close, Open _ -> Closed 0L | Close_noerr, Open _ -> Closed 0L - | Flush, Open _ -> s + | Flush, _ -> s + | Is_buffered, _ -> s (* output on open Out_channel *) | Output_char _, Open { position; length } | Output_byte _, Open { position; length } -> @@ -160,6 +163,7 @@ struct | Output_bytes b -> Res (result unit exn, protect (Out_channel.output_bytes oc) b) | Output (b,p,l) -> Res (result unit exn, protect (Out_channel.output oc b p) l) | Output_substring (s,p,l) -> Res (result unit exn, protect (Out_channel.output_substring oc s p) l) + | Is_buffered -> Res (bool, Out_channel.is_buffered oc) let postcond c (s:state) res = match c, res with | Open_text, Res ((Result (Unit,Exn),_), r) -> @@ -220,6 +224,10 @@ struct let str_len = String.length str in p < 0 || p >= str_len || l < 0 || p+l > str_len | Open _, _ -> false) + | Is_buffered, Res ((Bool,_),r) -> + (match s with + | Closed _ -> true + | Open _ -> r = true) | _, _ -> false end From 172130a7c3fa79ac4f3e3b2850513898d167d1eb Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 16:30:27 +0100 Subject: [PATCH 17/53] Add set_buffered cmd --- src/io/stm_tests.ml | 63 ++++++++++++++++++++++++++++----------------- 1 file changed, 40 insertions(+), 23 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 25e3052b..8d9a9c28 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -19,6 +19,7 @@ struct | Output_bytes of bytes | Output of bytes * int * int | Output_substring of string * int * int + | Set_buffered of bool | Is_buffered let pp_cmd par fmt x = @@ -37,6 +38,7 @@ struct | Output_bytes b -> cst1 pp_bytes "Output_bytes" par fmt b | Output (b,p,l) -> cst3 pp_bytes pp_int pp_int "Output" par fmt b p l | Output_substring (s,p,l) -> cst3 pp_string pp_int pp_int "Output_substring" par fmt s p l + | Set_buffered b -> cst1 pp_bool "Set_buffered" par fmt b | Is_buffered -> cst0 "Is_buffered" fmt let show_cmd = Util.Pp.to_show pp_cmd @@ -48,7 +50,8 @@ struct type state = Closed of int64 | Open of { position : int64; - length : int64; } + length : int64; + buffered : bool; } let arb_cmd s = let int64_gen = Gen.(map Int64.of_int small_int) in @@ -74,13 +77,14 @@ struct 3,map (fun b -> Output_bytes b) bytes_gen; 3,map3 (fun b p l -> Output (b,p,l)) bytes_gen byte_gen byte_gen; 3,map3 (fun s p l -> Output_substring (s,p,l)) string_gen byte_gen byte_gen; + 3,map (fun b -> Set_buffered b) Gen.bool; 3,return Is_buffered; ])) let init_state = Closed 0L let next_state c s = match c,s with - | Open_text, Closed _l -> Open { position = 0L; length = 0L } + | Open_text, Closed _l -> Open { position = 0L; length = 0L; buffered = true; } | Open_text, Open _ -> s (* non-open cmd on closed Out_channel *) | Output_char _, Closed _ @@ -91,44 +95,55 @@ struct | Output_substring (_,_,_), Closed _ | Seek _, Closed _ | Close, Closed _ - | Close_noerr, Closed _ -> s + | Close_noerr, Closed _ + | Set_buffered _, Closed _ -> s (* non-open cmd on open Out_channel *) - | Seek p, Open { position = _; length } -> Open { position = p; length = Int64.max length p } + | Seek p, Open { position = _; length; buffered } -> + Open { position = p; + length = Int64.max length p; + buffered; } | Pos,_ -> s | Length,_ -> s | Close, Open _ -> Closed 0L | Close_noerr, Open _ -> Closed 0L | Flush, _ -> s | Is_buffered, _ -> s + | Set_buffered b, Open { position; length; buffered = _ } -> + Open { position; length; buffered = b; } (* output on open Out_channel *) - | Output_char _, Open { position; length } - | Output_byte _, Open { position; length } -> - Open {position = Int64.succ position; - length = Int64.succ length; } - | Output_string str, Open { position; length } -> + | Output_char _, Open { position; length; buffered } + | Output_byte _, Open { position; length; buffered } -> + Open { position = Int64.succ position; + length = Int64.succ length; + buffered; } + | Output_string str, Open { position; length; buffered } -> let len = Int64.of_int (String.length str) in - Open {position = Int64.add position len; - length = Int64.add length len; } - | Output_bytes b, Open { position; length } -> + Open { position = Int64.add position len; + length = Int64.add length len; + buffered; } + | Output_bytes b, Open { position; length; buffered } -> let len = Int64.of_int (Bytes.length b) in - Open {position = Int64.add position len; - length = Int64.add length len; } - | Output (b,p,l), Open { position; length } -> + Open { position = Int64.add position len; + length = Int64.add length len; + buffered; } + | Output (b,p,l), Open { position; length; buffered } -> let bytes_len = Bytes.length b in if p < 0 || p >= bytes_len || l < 0 || p+l > bytes_len then s else let len = Int64.of_int l in - Open {position = Int64.add position len; - length = Int64.add length len; } - | Output_substring (str,p,l), Open { position; length } -> + Open { position = Int64.add position len; + length = Int64.add length len; + buffered; } + | Output_substring (str,p,l), Open { position; length; buffered } -> let str_len = String.length str in if p < 0 || p >= str_len || l < 0 || p+l > str_len then s else let len = Int64.of_int l in - Open {position = Int64.add position len; - length = Int64.add length len; } + Open { position = Int64.add position len; + length = Int64.add length len; + buffered; } let init_sut () = let path = Filename.temp_file "lin-dsl-" "" in @@ -163,6 +178,7 @@ struct | Output_bytes b -> Res (result unit exn, protect (Out_channel.output_bytes oc) b) | Output (b,p,l) -> Res (result unit exn, protect (Out_channel.output oc b p) l) | Output_substring (s,p,l) -> Res (result unit exn, protect (Out_channel.output_substring oc s p) l) + | Set_buffered b -> Res (unit, Out_channel.set_buffered oc b) | Is_buffered -> Res (bool, Out_channel.is_buffered oc) let postcond c (s:state) res = match c, res with @@ -177,11 +193,11 @@ struct | Pos, Res ((Result (Int64,Exn),_), r) -> (match s with | Closed _ -> true (*r = Error (Invalid_argument "Pos exception") - unspecified *) - | Open {position;length = _} -> r = Ok position) + | Open { position; length = _; buffered = _ } -> r = Ok position) | Length, Res ((Int64,_),i) -> (match s with | Closed _ -> true - | Open { position = _; length } -> i <= length) + | Open { position = _; length; buffered = _ } -> i <= length) | Close, Res ((Result (Unit,Exn),_), r) -> (match s,r with | Closed _, Error (Sys_error _) (*"Close exception" - unspecified *) @@ -224,10 +240,11 @@ struct let str_len = String.length str in p < 0 || p >= str_len || l < 0 || p+l > str_len | Open _, _ -> false) + | Set_buffered _, Res ((Unit,_), ()) -> true | Is_buffered, Res ((Bool,_),r) -> (match s with | Closed _ -> true - | Open _ -> r = true) + | Open { position = _; length = _; buffered } -> r = buffered) | _, _ -> false end From 5deb8b154e8f56bd2ae2ee036c0359ad70a98051 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 16:43:41 +0100 Subject: [PATCH 18/53] Add set_binary_mode cmd --- src/io/stm_tests.ml | 63 +++++++++++++++++++++++++++++---------------- 1 file changed, 41 insertions(+), 22 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 8d9a9c28..2def6b7a 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -19,6 +19,7 @@ struct | Output_bytes of bytes | Output of bytes * int * int | Output_substring of string * int * int + | Set_binary_mode of bool | Set_buffered of bool | Is_buffered @@ -38,6 +39,7 @@ struct | Output_bytes b -> cst1 pp_bytes "Output_bytes" par fmt b | Output (b,p,l) -> cst3 pp_bytes pp_int pp_int "Output" par fmt b p l | Output_substring (s,p,l) -> cst3 pp_string pp_int pp_int "Output_substring" par fmt s p l + | Set_binary_mode b -> cst1 pp_bool "Set_binary_mode" par fmt b | Set_buffered b -> cst1 pp_bool "Set_buffered" par fmt b | Is_buffered -> cst0 "Is_buffered" fmt @@ -49,9 +51,10 @@ struct mutable channel : Out_channel.t } type state = Closed of int64 - | Open of { position : int64; - length : int64; - buffered : bool; } + | Open of { position : int64; + length : int64; + buffered : bool; + binary_mode : bool; } let arb_cmd s = let int64_gen = Gen.(map Int64.of_int small_int) in @@ -77,6 +80,7 @@ struct 3,map (fun b -> Output_bytes b) bytes_gen; 3,map3 (fun b p l -> Output (b,p,l)) bytes_gen byte_gen byte_gen; 3,map3 (fun s p l -> Output_substring (s,p,l)) string_gen byte_gen byte_gen; + 3,map (fun b -> Set_binary_mode b) Gen.bool; 3,map (fun b -> Set_buffered b) Gen.bool; 3,return Is_buffered; ])) @@ -84,7 +88,11 @@ struct let init_state = Closed 0L let next_state c s = match c,s with - | Open_text, Closed _l -> Open { position = 0L; length = 0L; buffered = true; } + | Open_text, Closed _l -> + Open { position = 0L; + length = 0L; + buffered = true; + binary_mode = false; } | Open_text, Open _ -> s (* non-open cmd on closed Out_channel *) | Output_char _, Closed _ @@ -96,37 +104,44 @@ struct | Seek _, Closed _ | Close, Closed _ | Close_noerr, Closed _ + | Set_binary_mode _, Closed _ | Set_buffered _, Closed _ -> s (* non-open cmd on open Out_channel *) - | Seek p, Open { position = _; length; buffered } -> + | Seek p, Open { position = _; length; buffered; binary_mode } -> Open { position = p; length = Int64.max length p; - buffered; } + buffered; + binary_mode; } | Pos,_ -> s | Length,_ -> s | Close, Open _ -> Closed 0L | Close_noerr, Open _ -> Closed 0L | Flush, _ -> s + | Set_binary_mode b, Open { position; length; buffered; binary_mode = _ } -> + Open { position; length; buffered; binary_mode = b } | Is_buffered, _ -> s - | Set_buffered b, Open { position; length; buffered = _ } -> - Open { position; length; buffered = b; } + | Set_buffered b, Open { position; length; buffered = _; binary_mode } -> + Open { position; length; buffered = b; binary_mode } (* output on open Out_channel *) - | Output_char _, Open { position; length; buffered } - | Output_byte _, Open { position; length; buffered } -> + | Output_char _, Open { position; length; buffered; binary_mode } + | Output_byte _, Open { position; length; buffered; binary_mode } -> Open { position = Int64.succ position; length = Int64.succ length; - buffered; } - | Output_string str, Open { position; length; buffered } -> + buffered; + binary_mode; } + | Output_string str, Open { position; length; buffered; binary_mode } -> let len = Int64.of_int (String.length str) in Open { position = Int64.add position len; length = Int64.add length len; - buffered; } - | Output_bytes b, Open { position; length; buffered } -> + buffered; + binary_mode; } + | Output_bytes b, Open { position; length; buffered; binary_mode } -> let len = Int64.of_int (Bytes.length b) in Open { position = Int64.add position len; length = Int64.add length len; - buffered; } - | Output (b,p,l), Open { position; length; buffered } -> + buffered; + binary_mode; } + | Output (b,p,l), Open { position; length; buffered; binary_mode } -> let bytes_len = Bytes.length b in if p < 0 || p >= bytes_len || l < 0 || p+l > bytes_len then s @@ -134,8 +149,9 @@ struct let len = Int64.of_int l in Open { position = Int64.add position len; length = Int64.add length len; - buffered; } - | Output_substring (str,p,l), Open { position; length; buffered } -> + buffered; + binary_mode; } + | Output_substring (str,p,l), Open { position; length; buffered; binary_mode } -> let str_len = String.length str in if p < 0 || p >= str_len || l < 0 || p+l > str_len then s @@ -143,7 +159,8 @@ struct let len = Int64.of_int l in Open { position = Int64.add position len; length = Int64.add length len; - buffered; } + buffered; + binary_mode; } let init_sut () = let path = Filename.temp_file "lin-dsl-" "" in @@ -178,6 +195,7 @@ struct | Output_bytes b -> Res (result unit exn, protect (Out_channel.output_bytes oc) b) | Output (b,p,l) -> Res (result unit exn, protect (Out_channel.output oc b p) l) | Output_substring (s,p,l) -> Res (result unit exn, protect (Out_channel.output_substring oc s p) l) + | Set_binary_mode b -> Res (unit, Out_channel.set_binary_mode oc b) | Set_buffered b -> Res (unit, Out_channel.set_buffered oc b) | Is_buffered -> Res (bool, Out_channel.is_buffered oc) @@ -193,11 +211,11 @@ struct | Pos, Res ((Result (Int64,Exn),_), r) -> (match s with | Closed _ -> true (*r = Error (Invalid_argument "Pos exception") - unspecified *) - | Open { position; length = _; buffered = _ } -> r = Ok position) + | Open { position; length = _; buffered = _; binary_mode = _ } -> r = Ok position) | Length, Res ((Int64,_),i) -> (match s with | Closed _ -> true - | Open { position = _; length; buffered = _ } -> i <= length) + | Open { position = _; length; buffered = _; binary_mode = _ } -> i <= length) | Close, Res ((Result (Unit,Exn),_), r) -> (match s,r with | Closed _, Error (Sys_error _) (*"Close exception" - unspecified *) @@ -240,11 +258,12 @@ struct let str_len = String.length str in p < 0 || p >= str_len || l < 0 || p+l > str_len | Open _, _ -> false) + | Set_binary_mode _, Res ((Unit,_), ()) -> true | Set_buffered _, Res ((Unit,_), ()) -> true | Is_buffered, Res ((Bool,_),r) -> (match s with | Closed _ -> true - | Open { position = _; length = _; buffered } -> r = buffered) + | Open { position = _; length = _; buffered; binary_mode = _ } -> r = buffered) | _, _ -> false end From 8799ba6a66f866a80a21621cc5132b77a55c2cac Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 17:59:09 +0100 Subject: [PATCH 19/53] Adjust output{_char,_string,_bytes,,_substring} to reflect nl translation on MinGW+Cygwin --- src/io/stm_tests.ml | 47 ++++++++++++++++++++++++++++++++------------- 1 file changed, 34 insertions(+), 13 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 2def6b7a..cfbe6b00 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -87,6 +87,9 @@ struct let init_state = Closed 0L + let count_nls s = + String.fold_right (fun c count -> if c = '\n' then 1+count else count) s 0 + let next_state c s = match c,s with | Open_text, Closed _l -> Open { position = 0L; @@ -123,30 +126,45 @@ struct | Set_buffered b, Open { position; length; buffered = _; binary_mode } -> Open { position; length; buffered = b; binary_mode } (* output on open Out_channel *) - | Output_char _, Open { position; length; buffered; binary_mode } + | Output_char c, Open { position; length; buffered; binary_mode } -> + let len = (* Windows text mode maps '\n' to "\r\n" *) + if (Sys.win32 || Sys.cygwin) && not binary_mode && c = '\n' then 2L else 1L in + Open { position = Int64.add position len; + length = Int64.add length len; + buffered; + binary_mode; } | Output_byte _, Open { position; length; buffered; binary_mode } -> Open { position = Int64.succ position; length = Int64.succ length; buffered; binary_mode; } | Output_string str, Open { position; length; buffered; binary_mode } -> - let len = Int64.of_int (String.length str) in - Open { position = Int64.add position len; - length = Int64.add length len; - buffered; - binary_mode; } + let len = (* Windows text mode maps '\n' to "\r\n" *) + if (Sys.win32 || Sys.cygwin) && not binary_mode + then Int64.of_int (String.length str + count_nls str) + else Int64.of_int (String.length str) in + Open { position = Int64.add position len; + length = Int64.add length len; + buffered; + binary_mode; } | Output_bytes b, Open { position; length; buffered; binary_mode } -> - let len = Int64.of_int (Bytes.length b) in - Open { position = Int64.add position len; - length = Int64.add length len; - buffered; - binary_mode; } + let len = (* Windows text mode maps '\n' to "\r\n" *) + if (Sys.win32 || Sys.cygwin) && not binary_mode + then Int64.of_int (Bytes.length b + count_nls (String.of_bytes b)) + else Int64.of_int (Bytes.length b) in + Open { position = Int64.add position len; + length = Int64.add length len; + buffered; + binary_mode; } | Output (b,p,l), Open { position; length; buffered; binary_mode } -> let bytes_len = Bytes.length b in if p < 0 || p >= bytes_len || l < 0 || p+l > bytes_len then s else - let len = Int64.of_int l in + let len = (* Windows text mode maps '\n' to "\r\n" *) + if (Sys.win32 || Sys.cygwin) && not binary_mode + then Int64.of_int (l + count_nls String.(sub (of_bytes b) p l)) + else Int64.of_int l in Open { position = Int64.add position len; length = Int64.add length len; buffered; @@ -156,7 +174,10 @@ struct if p < 0 || p >= str_len || l < 0 || p+l > str_len then s else - let len = Int64.of_int l in + let len = (* Windows text mode maps '\n' to "\r\n" *) + if (Sys.win32 || Sys.cygwin) && not binary_mode + then Int64.of_int (l + count_nls (String.sub str p l)) + else Int64.of_int l in Open { position = Int64.add position len; length = Int64.add length len; buffered; From 44c16dee71c1c5d429de74b08886da127924916d Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 18:44:20 +0100 Subject: [PATCH 20/53] Adjust translation on MinGW+Cygwin to change length, not position - also add output_byte --- src/io/stm_tests.ml | 88 ++++++++++++++++++++++----------------------- 1 file changed, 43 insertions(+), 45 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index cfbe6b00..bbc81030 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -127,61 +127,59 @@ struct Open { position; length; buffered = b; binary_mode } (* output on open Out_channel *) | Output_char c, Open { position; length; buffered; binary_mode } -> - let len = (* Windows text mode maps '\n' to "\r\n" *) - if (Sys.win32 || Sys.cygwin) && not binary_mode && c = '\n' then 2L else 1L in - Open { position = Int64.add position len; - length = Int64.add length len; - buffered; - binary_mode; } - | Output_byte _, Open { position; length; buffered; binary_mode } -> - Open { position = Int64.succ position; - length = Int64.succ length; - buffered; - binary_mode; } - | Output_string str, Open { position; length; buffered; binary_mode } -> - let len = (* Windows text mode maps '\n' to "\r\n" *) - if (Sys.win32 || Sys.cygwin) && not binary_mode - then Int64.of_int (String.length str + count_nls str) - else Int64.of_int (String.length str) in - Open { position = Int64.add position len; - length = Int64.add length len; - buffered; - binary_mode; } - | Output_bytes b, Open { position; length; buffered; binary_mode } -> - let len = (* Windows text mode maps '\n' to "\r\n" *) - if (Sys.win32 || Sys.cygwin) && not binary_mode - then Int64.of_int (Bytes.length b + count_nls (String.of_bytes b)) - else Int64.of_int (Bytes.length b) in - Open { position = Int64.add position len; - length = Int64.add length len; - buffered; - binary_mode; } + let position = Int64.succ position in + let length = (* Windows text mode maps '\n' to "\r\n" *) + Int64.add length + (if (Sys.win32 || Sys.cygwin) && not binary_mode && c = '\n' then 2L else 1L) in + Open { position; length; buffered; binary_mode; } + | Output_byte i, Open { position; length; buffered; binary_mode } -> + let position = Int64.succ position in + let length = (* Windows text mode maps '\n' to "\r\n" *) + Int64.add length + (if (Sys.win32 || Sys.cygwin) && not binary_mode && (i mod 256 = 10) then 2L else 1L) in + Open { position; length; buffered; binary_mode; } + | Output_string arg, Open { position; length; buffered; binary_mode } -> + let arg_len = String.length arg in + let position = Int64.add position (Int64.of_int arg_len) in + let length = (* Windows text mode maps '\n' to "\r\n" *) + Int64.add length + (if (Sys.win32 || Sys.cygwin) && not binary_mode + then Int64.of_int (arg_len + count_nls arg) + else Int64.of_int arg_len) in + Open { position; length; buffered; binary_mode; } + | Output_bytes arg, Open { position; length; buffered; binary_mode } -> + let arg_len = Bytes.length arg in + let position = Int64.add position (Int64.of_int arg_len) in + let length = (* Windows text mode maps '\n' to "\r\n" *) + Int64.add length + (if (Sys.win32 || Sys.cygwin) && not binary_mode + then Int64.of_int (arg_len + count_nls (String.of_bytes arg)) + else Int64.of_int arg_len) in + Open { position; length; buffered; binary_mode; } | Output (b,p,l), Open { position; length; buffered; binary_mode } -> let bytes_len = Bytes.length b in if p < 0 || p >= bytes_len || l < 0 || p+l > bytes_len then s else - let len = (* Windows text mode maps '\n' to "\r\n" *) - if (Sys.win32 || Sys.cygwin) && not binary_mode - then Int64.of_int (l + count_nls String.(sub (of_bytes b) p l)) - else Int64.of_int l in - Open { position = Int64.add position len; - length = Int64.add length len; - buffered; - binary_mode; } + let position = Int64.add position (Int64.of_int l) in + let length = (* Windows text mode maps '\n' to "\r\n" *) + Int64.add length + (if (Sys.win32 || Sys.cygwin) && not binary_mode + then Int64.of_int (l + count_nls String.(sub (of_bytes b) p l)) + else Int64.of_int l) in + Open { position; length; buffered; binary_mode; } | Output_substring (str,p,l), Open { position; length; buffered; binary_mode } -> let str_len = String.length str in if p < 0 || p >= str_len || l < 0 || p+l > str_len then s else - let len = (* Windows text mode maps '\n' to "\r\n" *) - if (Sys.win32 || Sys.cygwin) && not binary_mode - then Int64.of_int (l + count_nls (String.sub str p l)) - else Int64.of_int l in - Open { position = Int64.add position len; - length = Int64.add length len; - buffered; - binary_mode; } + let position = Int64.add position (Int64.of_int l) in + let length = (* Windows text mode maps '\n' to "\r\n" *) + Int64.add length + (if (Sys.win32 || Sys.cygwin) && not binary_mode + then Int64.of_int (l + count_nls String.(sub str p l)) + else Int64.of_int l) in + Open { position; length; buffered; binary_mode; } let init_sut () = let path = Filename.temp_file "lin-dsl-" "" in From 32fd287c9164119b054eb93b30d13450577e455f Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 19:07:28 +0100 Subject: [PATCH 21/53] Flush before changing binary mode on Windows, for output to reflect prev mode --- src/io/stm_tests.ml | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index bbc81030..d6eff120 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -214,7 +214,10 @@ struct | Output_bytes b -> Res (result unit exn, protect (Out_channel.output_bytes oc) b) | Output (b,p,l) -> Res (result unit exn, protect (Out_channel.output oc b p) l) | Output_substring (s,p,l) -> Res (result unit exn, protect (Out_channel.output_substring oc s p) l) - | Set_binary_mode b -> Res (unit, Out_channel.set_binary_mode oc b) + | Set_binary_mode b -> + if Sys.win32 || Sys.cygwin + then Res (unit, (Out_channel.flush oc; Out_channel.set_binary_mode oc b)) (* flush before changing mode *) + else Res (unit, Out_channel.set_binary_mode oc b) | Set_buffered b -> Res (unit, Out_channel.set_buffered oc b) | Is_buffered -> Res (bool, Out_channel.is_buffered oc) From bc1bee404e42c8b77d307b9d1239ccbcd0bc5eed Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 5 Jan 2024 19:08:22 +0100 Subject: [PATCH 22/53] Remove Lin Out_channel tests --- src/io/dune | 4 +-- src/io/lin_tests_domain.ml | 16 +++------- src/io/lin_tests_spec_io.ml | 58 ------------------------------------- src/io/lin_tests_thread.ml | 4 +-- 4 files changed, 6 insertions(+), 76 deletions(-) diff --git a/src/io/dune b/src/io/dune index d296546e..942c96d2 100644 --- a/src/io/dune +++ b/src/io/dune @@ -23,9 +23,7 @@ (package multicoretests) ;(flags (:standard -w -27)) (libraries qcheck-lin.domain lin_tests_spec_io) - (action - (setenv OCAML_SYSTEM %{system} - (run %{test} --verbose))) + (action (run %{test} --verbose)) ) (test diff --git a/src/io/lin_tests_domain.ml b/src/io/lin_tests_domain.ml index d4c372b4..b10c5775 100644 --- a/src/io/lin_tests_domain.ml +++ b/src/io/lin_tests_domain.ml @@ -1,18 +1,10 @@ (* ********************************************************************** *) -(* Tests of in and out channels *) +(* Tests of In_channels *) (* ********************************************************************** *) module IC_domain = Lin_domain.Make(Lin_tests_spec_io.ICConf) -module OC_domain = Lin_domain.Make(Lin_tests_spec_io.OCConf) -let tests = - IC_domain.neg_lin_test ~count:1000 ~name:"Lin In_channel test with Domain" :: - if Sys.getenv_opt "OCAML_SYSTEM" = Some "macosx" - then ( - Printf.printf "Lin Out_channel test with Domain disabled under macOS\n\n%!"; - [] - ) else [ - OC_domain.neg_lin_test ~count:5000 ~name:"Lin Out_channel test with Domain"; +let _ = + QCheck_base_runner.run_tests_main [ + IC_domain.neg_lin_test ~count:1000 ~name:"Lin In_channel test with Domain" ] - -let _ = QCheck_base_runner.run_tests_main tests diff --git a/src/io/lin_tests_spec_io.ml b/src/io/lin_tests_spec_io.ml index c611aad3..6e023be3 100644 --- a/src/io/lin_tests_spec_io.ml +++ b/src/io/lin_tests_spec_io.ml @@ -61,61 +61,3 @@ module ICConf : Lin.Spec = struct val_ "In_channel.set_binary_mode" In_channel.set_binary_mode (t @-> bool @-> returning_or_exc unit) ; ] end - -module OCConf : Lin.Spec = struct - (* a path and an open channel to that file; we need to keep the path - to cleanup after the test run *) - type t = Out_channel.t - let path = ref "" - - let init () = - let p,ch = Filename.open_temp_file "lin-" "" in - path := p; - ch - - let cleanup chan = - Out_channel.close chan; - Sys.remove !path - - open Lin - let int,int64 = nat_small,nat64_small - - (* disable string and bytes char shrinking as too many shrinking candidates - triggers long Out_channel shrink runs on Mingw + Cygwin *) - let string = - let string = QCheck.(set_shrink Shrink.(string ~shrink:nil) string_small) in - gen_deconstructible string (print Lin.string) String.equal - let bytes = - let bytes = QCheck.(set_shrink Shrink.(bytes ~shrink:nil) bytes_small) in - gen_deconstructible bytes (print Lin.bytes) Bytes.equal - - let api = [ - (* Only one t is tested, so skip stdout, stderr and opening functions *) - - (* val_ "Out_channel.stdout" Out_channel.stdout (t) ; *) - (* val_ "Out_channel.stderr" Out_channel.stderr (t) ; *) - (* val_ "Out_channel.open_bin" Out_channel.open_bin (string @-> returning t) ; *) - (* val_ "Out_channel.open_text" Out_channel.open_text (string @-> returning t) ; *) - (* val_ "Out_channel.open_gen" Out_channel.open_gen (open_flag list @-> int @-> string @-> returning t) ; *) - (* val_ "Out_channel.with_open_bin" Out_channel.with_open_bin (string @-> (t @-> 'a) @-> returning 'a) ; *) - (* val_ "Out_channel.with_open_text" Out_channel.with_open_text (string @-> (t @-> 'a) @-> returning 'a) ; *) - (* val_ "Out_channel.with_open_gen" Out_channel.with_open_gen (open_flag list @-> int @-> string @-> (t @-> 'a) @-> returning 'a) ; *) - - val_freq 10 "Out_channel.seek" Out_channel.seek (t @-> int64 @-> returning_or_exc unit) ; - val_freq 20 "Out_channel.pos" Out_channel.pos (t @-> returning_or_exc int64) ; - val_freq 20 "Out_channel.length" Out_channel.length (t @-> returning_or_exc int64) ; - val_freq 10 "Out_channel.close" Out_channel.close (t @-> returning_or_exc unit) ; - val_freq 10 "Out_channel.close_noerr" Out_channel.close_noerr (t @-> returning unit) ; - val_freq 10 "Out_channel.flush" Out_channel.flush (t @-> returning_or_exc unit) ; - (*val_freq 1 "Out_channel.flush_all" Out_channel.flush_all (unit @-> returning_or_exc unit) ;*) - val_freq 10 "Out_channel.output_char" Out_channel.output_char (t @-> char @-> returning_or_exc unit) ; - val_freq 10 "Out_channel.output_byte" Out_channel.output_byte (t @-> int @-> returning_or_exc unit) ; - val_freq 10 "Out_channel.output_string" Out_channel.output_string (t @-> string @-> returning_or_exc unit) ; - val_freq 10 "Out_channel.output_bytes" Out_channel.output_bytes (t @-> bytes @-> returning_or_exc unit) ; - val_freq 10 "Out_channel.output" Out_channel.output (t @-> bytes @-> int @-> int @-> returning_or_exc unit) ; - val_freq 10 "Out_channel.output_substring" Out_channel.output_substring (t @-> string @-> int @-> int @-> returning_or_exc unit) ; - val_freq 10 "Out_channel.set_binary_mode" Out_channel.set_binary_mode (t @-> bool @-> returning_or_exc unit) ; - val_freq 10 "Out_channel.set_buffered" Out_channel.set_buffered (t @-> bool @-> returning_or_exc unit) ; - val_freq 10 "Out_channel.is_buffered" Out_channel.is_buffered (t @-> returning_or_exc bool) ; - ] -end diff --git a/src/io/lin_tests_thread.ml b/src/io/lin_tests_thread.ml index 729b9851..4a2a1bf0 100644 --- a/src/io/lin_tests_thread.ml +++ b/src/io/lin_tests_thread.ml @@ -1,12 +1,10 @@ (* ********************************************************************** *) -(* Tests of in and out channels *) +(* Tests of In_channels *) (* ********************************************************************** *) module IC_thread = Lin_thread.Make(Lin_tests_spec_io.ICConf) [@@alert "-experimental"] -module OC_thread = Lin_thread.Make(Lin_tests_spec_io.OCConf) [@@alert "-experimental"] let _ = QCheck_base_runner.run_tests_main [ IC_thread.neg_lin_test ~count:1000 ~name:"Lin In_channel test with Thread"; - OC_thread.neg_lin_test ~count:1000 ~name:"Lin Out_channel test with Thread"; ] From 75447d6861f252df678bd45d0cb060409484762a Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 11 Jan 2024 15:52:31 +0100 Subject: [PATCH 23/53] Remove unused argument to Closed --- src/io/stm_tests.ml | 62 ++++++++++++++++++++++----------------------- 1 file changed, 31 insertions(+), 31 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index d6eff120..4deae906 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -50,7 +50,7 @@ struct type sut = { path : string; mutable channel : Out_channel.t } - type state = Closed of int64 + type state = Closed | Open of { position : int64; length : int64; buffered : bool; @@ -64,7 +64,7 @@ struct let bytes_gen = Gen.bytes_small in QCheck.make ~print:show_cmd (*~shrink:shrink_cmd*) (match s with - | Closed _ -> Gen.return Open_text (* close can trigger a fatal error *) + | Closed -> Gen.return Open_text (* close can trigger a fatal error *) | Open _ -> Gen.(frequency [ (*1,return Open_text;*) @@ -85,30 +85,30 @@ struct 3,return Is_buffered; ])) - let init_state = Closed 0L + let init_state = Closed let count_nls s = String.fold_right (fun c count -> if c = '\n' then 1+count else count) s 0 let next_state c s = match c,s with - | Open_text, Closed _l -> + | Open_text, Closed -> Open { position = 0L; length = 0L; buffered = true; binary_mode = false; } | Open_text, Open _ -> s (* non-open cmd on closed Out_channel *) - | Output_char _, Closed _ - | Output_byte _, Closed _ - | Output_string _, Closed _ - | Output_bytes _, Closed _ - | Output (_,_,_), Closed _ - | Output_substring (_,_,_), Closed _ - | Seek _, Closed _ - | Close, Closed _ - | Close_noerr, Closed _ - | Set_binary_mode _, Closed _ - | Set_buffered _, Closed _ -> s + | Output_char _, Closed + | Output_byte _, Closed + | Output_string _, Closed + | Output_bytes _, Closed + | Output (_,_,_), Closed + | Output_substring (_,_,_), Closed + | Seek _, Closed + | Close, Closed + | Close_noerr, Closed + | Set_binary_mode _, Closed + | Set_buffered _, Closed -> s (* non-open cmd on open Out_channel *) | Seek p, Open { position = _; length; buffered; binary_mode } -> Open { position = p; @@ -117,8 +117,8 @@ struct binary_mode; } | Pos,_ -> s | Length,_ -> s - | Close, Open _ -> Closed 0L - | Close_noerr, Open _ -> Closed 0L + | Close, Open _ -> Closed + | Close_noerr, Open _ -> Closed | Flush, _ -> s | Set_binary_mode b, Open { position; length; buffered; binary_mode = _ } -> Open { position; length; buffered; binary_mode = b } @@ -195,7 +195,7 @@ struct Sys.remove path let precond c s = match c,s with - | Open_text, Closed _ -> true + | Open_text, Closed -> true | Open_text, Open _ -> false | _, Open _ -> true | _, _ -> false @@ -224,49 +224,49 @@ struct let postcond c (s:state) res = match c, res with | Open_text, Res ((Result (Unit,Exn),_), r) -> (match s,r with - | Closed _, Ok () - | Closed _, Error (Sys_error _) (*"/tmp/lin-dsl-03ba23: Too many open files"*) + | Closed, Ok () + | Closed, Error (Sys_error _) (*"/tmp/lin-dsl-03ba23: Too many open files"*) | Open _, Ok () | Open _, Error (Sys_error _) -> true | _ -> false) | Seek _, Res ((Unit,_), ()) -> true | Pos, Res ((Result (Int64,Exn),_), r) -> (match s with - | Closed _ -> true (*r = Error (Invalid_argument "Pos exception") - unspecified *) + | Closed -> true (*r = Error (Invalid_argument "Pos exception") - unspecified *) | Open { position; length = _; buffered = _; binary_mode = _ } -> r = Ok position) | Length, Res ((Int64,_),i) -> (match s with - | Closed _ -> true + | Closed -> true | Open { position = _; length; buffered = _; binary_mode = _ } -> i <= length) | Close, Res ((Result (Unit,Exn),_), r) -> (match s,r with - | Closed _, Error (Sys_error _) (*"Close exception" - unspecified *) + | Closed, Error (Sys_error _) (*"Close exception" - unspecified *) | Open _, Ok () -> true | _ -> false) | Close_noerr, Res ((Unit,_), r) -> (match s,r with - | Closed _, () + | Closed, () | Open _, () -> true) | Flush, Res ((Unit,_), r) -> r = () | Output_char _c, Res ((Result (Unit,Exn),_), r) -> (match s with - | Closed _ -> true + | Closed -> true | Open _ -> r = Ok ()) (* print on closed unspecified *) | Output_byte _i, Res ((Result (Unit,Exn),_), r) -> (match s with - | Closed _ -> true + | Closed -> true | Open _ -> r = Ok ()) (* print on closed unspecified *) | Output_string _s, Res ((Result (Unit,Exn),_), r) -> (match s with - | Closed _ -> true + | Closed -> true | Open _ -> r = Ok ()) (* print on closed unspecified *) | Output_bytes _b, Res ((Result (Unit,Exn),_), r) -> (match s with - | Closed _ -> true + | Closed -> true | Open _ -> r = Ok ()) (* print on closed unspecified *) | Output (b,p,l), Res ((Result (Unit,Exn),_), r) -> (match s,r with - | Closed _,_ + | Closed, _ | Open _, Ok () -> true | Open _, Error (Invalid_argument _) -> (*"output"*) let bytes_len = Bytes.length b in @@ -274,7 +274,7 @@ struct | Open _, _ -> false) | Output_substring (str,p,l), Res ((Result (Unit,Exn),_), r) -> (match s,r with - | Closed _,_ + | Closed, _ | Open _, Ok () -> true | Open _, Error (Invalid_argument _) -> (*"output_substring"*) let str_len = String.length str in @@ -284,7 +284,7 @@ struct | Set_buffered _, Res ((Unit,_), ()) -> true | Is_buffered, Res ((Bool,_),r) -> (match s with - | Closed _ -> true + | Closed -> true | Open { position = _; length = _; buffered; binary_mode = _ } -> r = buffered) | _, _ -> false end From ae8a0aa7f219c9e182e7780e573142a4c0d554de Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 11 Jan 2024 15:54:37 +0100 Subject: [PATCH 24/53] Rename prefix lin-dsl- to stm- --- src/io/stm_tests.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 4deae906..b2e41127 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -182,10 +182,10 @@ struct Open { position; length; buffered; binary_mode; } let init_sut () = - let path = Filename.temp_file "lin-dsl-" "" in + let path = Filename.temp_file "stm-" "" in (*Printf.printf "init_sut %s\n%!" path;*) let channel = Stdlib.stdout in - (*let path, channel = Filename.open_temp_file "lin-dsl-" "" in*) + (*let path, channel = Filename.open_temp_file "stm-" "" in*) { path; channel } let cleanup { path; channel } = @@ -225,7 +225,7 @@ struct | Open_text, Res ((Result (Unit,Exn),_), r) -> (match s,r with | Closed, Ok () - | Closed, Error (Sys_error _) (*"/tmp/lin-dsl-03ba23: Too many open files"*) + | Closed, Error (Sys_error _) (*"/tmp/stm-03ba23: Too many open files"*) | Open _, Ok () | Open _, Error (Sys_error _) -> true | _ -> false) From 181a99caa42e92af54d3a105cbad83989fc9a02c Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 11 Jan 2024 15:59:40 +0100 Subject: [PATCH 25/53] Document the reason for Length result/model mismatch --- src/io/stm_tests.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index b2e41127..e540e383 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -236,7 +236,7 @@ struct | Open { position; length = _; buffered = _; binary_mode = _ } -> r = Ok position) | Length, Res ((Int64,_),i) -> (match s with - | Closed -> true + | Closed -> true (* because of buffering the result and the model may disagree *) | Open { position = _; length; buffered = _; binary_mode = _ } -> i <= length) | Close, Res ((Result (Unit,Exn),_), r) -> (match s,r with From 1dbafd5e5c991a41eab4470715b704d2d13a94ee Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 11 Jan 2024 16:07:56 +0100 Subject: [PATCH 26/53] Factor out windows text-mode test --- src/io/stm_tests.ml | 15 +++++++++------ 1 file changed, 9 insertions(+), 6 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index e540e383..86664da1 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -90,6 +90,9 @@ struct let count_nls s = String.fold_right (fun c count -> if c = '\n' then 1+count else count) s 0 + let in_windows_text_mode binary_mode = + (Sys.win32 || Sys.cygwin) && not binary_mode + let next_state c s = match c,s with | Open_text, Closed -> Open { position = 0L; @@ -130,20 +133,20 @@ struct let position = Int64.succ position in let length = (* Windows text mode maps '\n' to "\r\n" *) Int64.add length - (if (Sys.win32 || Sys.cygwin) && not binary_mode && c = '\n' then 2L else 1L) in + (if in_windows_text_mode binary_mode && c = '\n' then 2L else 1L) in Open { position; length; buffered; binary_mode; } | Output_byte i, Open { position; length; buffered; binary_mode } -> let position = Int64.succ position in let length = (* Windows text mode maps '\n' to "\r\n" *) Int64.add length - (if (Sys.win32 || Sys.cygwin) && not binary_mode && (i mod 256 = 10) then 2L else 1L) in + (if in_windows_text_mode binary_mode && (i mod 256 = 10) then 2L else 1L) in Open { position; length; buffered; binary_mode; } | Output_string arg, Open { position; length; buffered; binary_mode } -> let arg_len = String.length arg in let position = Int64.add position (Int64.of_int arg_len) in let length = (* Windows text mode maps '\n' to "\r\n" *) Int64.add length - (if (Sys.win32 || Sys.cygwin) && not binary_mode + (if in_windows_text_mode binary_mode then Int64.of_int (arg_len + count_nls arg) else Int64.of_int arg_len) in Open { position; length; buffered; binary_mode; } @@ -152,7 +155,7 @@ struct let position = Int64.add position (Int64.of_int arg_len) in let length = (* Windows text mode maps '\n' to "\r\n" *) Int64.add length - (if (Sys.win32 || Sys.cygwin) && not binary_mode + (if in_windows_text_mode binary_mode then Int64.of_int (arg_len + count_nls (String.of_bytes arg)) else Int64.of_int arg_len) in Open { position; length; buffered; binary_mode; } @@ -164,7 +167,7 @@ struct let position = Int64.add position (Int64.of_int l) in let length = (* Windows text mode maps '\n' to "\r\n" *) Int64.add length - (if (Sys.win32 || Sys.cygwin) && not binary_mode + (if in_windows_text_mode binary_mode then Int64.of_int (l + count_nls String.(sub (of_bytes b) p l)) else Int64.of_int l) in Open { position; length; buffered; binary_mode; } @@ -176,7 +179,7 @@ struct let position = Int64.add position (Int64.of_int l) in let length = (* Windows text mode maps '\n' to "\r\n" *) Int64.add length - (if (Sys.win32 || Sys.cygwin) && not binary_mode + (if in_windows_text_mode binary_mode then Int64.of_int (l + count_nls String.(sub str p l)) else Int64.of_int l) in Open { position; length; buffered; binary_mode; } From 5d3b2c9f07fc3cca75490aa59039ae592eed700d Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 11 Jan 2024 16:24:23 +0100 Subject: [PATCH 27/53] Clean-up old comments --- src/io/stm_tests.ml | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 86664da1..66821e5e 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -186,15 +186,12 @@ struct let init_sut () = let path = Filename.temp_file "stm-" "" in - (*Printf.printf "init_sut %s\n%!" path;*) let channel = Stdlib.stdout in - (*let path, channel = Filename.open_temp_file "stm-" "" in*) { path; channel } let cleanup { path; channel } = if channel <> Stdlib.stdout then Out_channel.close channel; - (*Printf.printf "Removing %s\n%!" path;*) Sys.remove path let precond c s = match c,s with From 6597741750b39b986ee66094b92c64dba97079ff Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 11 Jan 2024 18:05:44 +0100 Subject: [PATCH 28/53] Wrap close_noerr in protect --- src/io/stm_tests.ml | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 66821e5e..7c79e104 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -206,7 +206,7 @@ struct | Pos -> Res (result int64 exn, protect Out_channel.pos oc) | Length -> Res (int64, Out_channel.length oc) | Close -> Res (result unit exn, protect Out_channel.close oc) - | Close_noerr -> Res (unit, Out_channel.close_noerr oc) + | Close_noerr -> Res (result unit exn, protect Out_channel.close_noerr oc) | Flush -> Res (unit, Out_channel.flush oc) | Output_char c -> Res (result unit exn, protect (Out_channel.output_char oc) c) | Output_byte i -> Res (result unit exn, protect (Out_channel.output_byte oc) i) @@ -243,10 +243,11 @@ struct | Closed, Error (Sys_error _) (*"Close exception" - unspecified *) | Open _, Ok () -> true | _ -> false) - | Close_noerr, Res ((Unit,_), r) -> + | Close_noerr, Res ((Result (Unit,Exn),_), r) -> (match s,r with - | Closed, () - | Open _, () -> true) + | Closed, Error (Sys_error _) -> false (* should not generate an error *) + | Open _, Ok () -> true + | _ -> false) | Flush, Res ((Unit,_), r) -> r = () | Output_char _c, Res ((Result (Unit,Exn),_), r) -> (match s with From 298bdea8415c34273227374a397e3f9460223756 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 11 Jan 2024 18:48:29 +0100 Subject: [PATCH 29/53] Support generating Close* cmds in state Closed --- src/io/stm_tests.ml | 22 ++++++++++++++++------ 1 file changed, 16 insertions(+), 6 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 7c79e104..d6d42c77 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -64,7 +64,12 @@ struct let bytes_gen = Gen.bytes_small in QCheck.make ~print:show_cmd (*~shrink:shrink_cmd*) (match s with - | Closed -> Gen.return Open_text (* close can trigger a fatal error *) + | Closed -> + Gen.(frequency [ (* generate only Open or Close cmds in Closed *) + 8,return Open_text; + 1,return Close; + 1,return Close_noerr; + ]) | Open _ -> Gen.(frequency [ (*1,return Open_text;*) @@ -190,13 +195,17 @@ struct { path; channel } let cleanup { path; channel } = - if channel <> Stdlib.stdout - then Out_channel.close channel; + (if channel <> Stdlib.stdout + then + try Out_channel.close channel + with Sys_error _ -> ()); Sys.remove path let precond c s = match c,s with | Open_text, Closed -> true | Open_text, Open _ -> false + | Close, Closed + | Close_noerr, Closed -> true | _, Open _ -> true | _, _ -> false @@ -205,8 +214,8 @@ struct | Seek p -> Res (unit, Out_channel.seek oc p) | Pos -> Res (result int64 exn, protect Out_channel.pos oc) | Length -> Res (int64, Out_channel.length oc) - | Close -> Res (result unit exn, protect Out_channel.close oc) - | Close_noerr -> Res (result unit exn, protect Out_channel.close_noerr oc) + | Close -> Res (result unit exn, if oc <> Stdlib.stdout then protect Out_channel.close oc else Ok ()) + | Close_noerr -> Res (result unit exn, if oc <> Stdlib.stdout then protect Out_channel.close_noerr oc else Ok ()) | Flush -> Res (unit, Out_channel.flush oc) | Output_char c -> Res (result unit exn, protect (Out_channel.output_char oc) c) | Output_byte i -> Res (result unit exn, protect (Out_channel.output_byte oc) i) @@ -240,12 +249,13 @@ struct | Open { position = _; length; buffered = _; binary_mode = _ } -> i <= length) | Close, Res ((Result (Unit,Exn),_), r) -> (match s,r with - | Closed, Error (Sys_error _) (*"Close exception" - unspecified *) + | Closed, (Ok () | Error (Sys_error _)) (*"Close exception" - unspecified *) | Open _, Ok () -> true | _ -> false) | Close_noerr, Res ((Result (Unit,Exn),_), r) -> (match s,r with | Closed, Error (Sys_error _) -> false (* should not generate an error *) + | Closed, Ok () -> true | Open _, Ok () -> true | _ -> false) | Flush, Res ((Unit,_), r) -> r = () From 497975e4274cef9c1c3af496ea8f97eccedfdaf0 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 12:22:00 +0100 Subject: [PATCH 30/53] Start in open channel to avoid Stdlib.stdout special cases --- src/io/stm_tests.ml | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index d6d42c77..193362e5 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -90,7 +90,10 @@ struct 3,return Is_buffered; ])) - let init_state = Closed + let init_state = Open { position = 0L; + length = 0L; + buffered = true; + binary_mode = false; } let count_nls s = String.fold_right (fun c count -> if c = '\n' then 1+count else count) s 0 @@ -191,14 +194,11 @@ struct let init_sut () = let path = Filename.temp_file "stm-" "" in - let channel = Stdlib.stdout in + let channel = Out_channel.open_text path in { path; channel } let cleanup { path; channel } = - (if channel <> Stdlib.stdout - then - try Out_channel.close channel - with Sys_error _ -> ()); + (try Out_channel.close channel with Sys_error _ -> ()); Sys.remove path let precond c s = match c,s with @@ -214,8 +214,8 @@ struct | Seek p -> Res (unit, Out_channel.seek oc p) | Pos -> Res (result int64 exn, protect Out_channel.pos oc) | Length -> Res (int64, Out_channel.length oc) - | Close -> Res (result unit exn, if oc <> Stdlib.stdout then protect Out_channel.close oc else Ok ()) - | Close_noerr -> Res (result unit exn, if oc <> Stdlib.stdout then protect Out_channel.close_noerr oc else Ok ()) + | Close -> Res (result unit exn, protect Out_channel.close oc) + | Close_noerr -> Res (result unit exn, protect Out_channel.close_noerr oc) | Flush -> Res (unit, Out_channel.flush oc) | Output_char c -> Res (result unit exn, protect (Out_channel.output_char oc) c) | Output_byte i -> Res (result unit exn, protect (Out_channel.output_byte oc) i) From df35b3c713edc69b4a793a0b3df5cb08a33ae5ab Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 12:31:44 +0100 Subject: [PATCH 31/53] Allow Length in Closed state --- src/io/stm_tests.ml | 16 +++++++++++----- 1 file changed, 11 insertions(+), 5 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 193362e5..8d900006 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -67,6 +67,7 @@ struct | Closed -> Gen.(frequency [ (* generate only Open or Close cmds in Closed *) 8,return Open_text; + 3,return Length; 1,return Close; 1,return Close_noerr; ]) @@ -204,6 +205,7 @@ struct let precond c s = match c,s with | Open_text, Closed -> true | Open_text, Open _ -> false + | Length, Closed | Close, Closed | Close_noerr, Closed -> true | _, Open _ -> true @@ -213,7 +215,7 @@ struct | Open_text -> Res (result unit exn, protect (fun path -> (r.channel <- Out_channel.open_text path;())) path) | Seek p -> Res (unit, Out_channel.seek oc p) | Pos -> Res (result int64 exn, protect Out_channel.pos oc) - | Length -> Res (int64, Out_channel.length oc) + | Length -> Res (result int64 exn, protect Out_channel.length oc) | Close -> Res (result unit exn, protect Out_channel.close oc) | Close_noerr -> Res (result unit exn, protect Out_channel.close_noerr oc) | Flush -> Res (unit, Out_channel.flush oc) @@ -243,10 +245,14 @@ struct (match s with | Closed -> true (*r = Error (Invalid_argument "Pos exception") - unspecified *) | Open { position; length = _; buffered = _; binary_mode = _ } -> r = Ok position) - | Length, Res ((Int64,_),i) -> - (match s with - | Closed -> true (* because of buffering the result and the model may disagree *) - | Open { position = _; length; buffered = _; binary_mode = _ } -> i <= length) + | Length, Res ((Result (Int64,Exn),_), r) -> + (match s,r with + | Closed, Error (Sys_error _) -> true (* Sys_error("Bad file descriptor") *) + | Open { position = _; + length; + buffered = _; (* because of buffering the result and the model may disagree *) + binary_mode = _ }, Ok i -> i <= length + | _ -> false) | Close, Res ((Result (Unit,Exn),_), r) -> (match s,r with | Closed, (Ok () | Error (Sys_error _)) (*"Close exception" - unspecified *) From a7b427f9addaa09b492d60562a6abd799e006efe Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 12:36:44 +0100 Subject: [PATCH 32/53] Allow Seek in Closed state --- src/io/stm_tests.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 8d900006..eb2f0bc8 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -67,6 +67,7 @@ struct | Closed -> Gen.(frequency [ (* generate only Open or Close cmds in Closed *) 8,return Open_text; + 3,map (fun i -> Seek i) int64_gen; 3,return Length; 1,return Close; 1,return Close_noerr; @@ -205,6 +206,7 @@ struct let precond c s = match c,s with | Open_text, Closed -> true | Open_text, Open _ -> false + | Seek _, Closed | Length, Closed | Close, Closed | Close_noerr, Closed -> true @@ -213,7 +215,7 @@ struct let run c ({path;channel = oc} as r) = match c with | Open_text -> Res (result unit exn, protect (fun path -> (r.channel <- Out_channel.open_text path;())) path) - | Seek p -> Res (unit, Out_channel.seek oc p) + | Seek p -> Res (result unit exn, protect (Out_channel.seek oc) p) | Pos -> Res (result int64 exn, protect Out_channel.pos oc) | Length -> Res (result int64 exn, protect Out_channel.length oc) | Close -> Res (result unit exn, protect Out_channel.close oc) @@ -240,7 +242,11 @@ struct | Open _, Ok () | Open _, Error (Sys_error _) -> true | _ -> false) - | Seek _, Res ((Unit,_), ()) -> true + | Seek _, Res ((Result (Unit,Exn),_), r) -> + (match s,r with + | Closed, Error (Sys_error _) -> true (* Sys_error("Bad file descriptor") *) + | Open _, Ok () -> true + | _ -> false) | Pos, Res ((Result (Int64,Exn),_), r) -> (match s with | Closed -> true (*r = Error (Invalid_argument "Pos exception") - unspecified *) From c6e6d049b8becaf349bfe363767f71a0e30a8e95 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 12:55:10 +0100 Subject: [PATCH 33/53] Allow Pos in Closed state --- src/io/stm_tests.ml | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index eb2f0bc8..80403f4d 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -68,6 +68,7 @@ struct Gen.(frequency [ (* generate only Open or Close cmds in Closed *) 8,return Open_text; 3,map (fun i -> Seek i) int64_gen; + 3,return Pos; 3,return Length; 1,return Close; 1,return Close_noerr; @@ -207,6 +208,7 @@ struct | Open_text, Closed -> true | Open_text, Open _ -> false | Seek _, Closed + | Pos, Closed | Length, Closed | Close, Closed | Close_noerr, Closed -> true @@ -248,9 +250,13 @@ struct | Open _, Ok () -> true | _ -> false) | Pos, Res ((Result (Int64,Exn),_), r) -> - (match s with - | Closed -> true (*r = Error (Invalid_argument "Pos exception") - unspecified *) - | Open { position; length = _; buffered = _; binary_mode = _ } -> r = Ok position) + (match s, r with + | Closed, (Ok _ | Error (Sys_error _)) -> true (* pos on closed channel unspecified *) + | Open { position; + length = _; + buffered = _; + binary_mode = _ }, Ok p -> p = position + | _ -> false) | Length, Res ((Result (Int64,Exn),_), r) -> (match s,r with | Closed, Error (Sys_error _) -> true (* Sys_error("Bad file descriptor") *) From 066025a69ee1f6036d2ca84622c45cc683e9763e Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 12:56:25 +0100 Subject: [PATCH 34/53] Allow Flush in Closed state --- src/io/stm_tests.ml | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 80403f4d..35603fd1 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -72,6 +72,7 @@ struct 3,return Length; 1,return Close; 1,return Close_noerr; + 3,return Flush; ]) | Open _ -> Gen.(frequency [ @@ -211,7 +212,8 @@ struct | Pos, Closed | Length, Closed | Close, Closed - | Close_noerr, Closed -> true + | Close_noerr, Closed + | Flush, Closed -> true | _, Open _ -> true | _, _ -> false @@ -222,7 +224,7 @@ struct | Length -> Res (result int64 exn, protect Out_channel.length oc) | Close -> Res (result unit exn, protect Out_channel.close oc) | Close_noerr -> Res (result unit exn, protect Out_channel.close_noerr oc) - | Flush -> Res (unit, Out_channel.flush oc) + | Flush -> Res (result unit exn, protect Out_channel.flush oc) | Output_char c -> Res (result unit exn, protect (Out_channel.output_char oc) c) | Output_byte i -> Res (result unit exn, protect (Out_channel.output_byte oc) i) | Output_string s -> Res (result unit exn, protect (Out_channel.output_string oc) s) @@ -276,7 +278,12 @@ struct | Closed, Ok () -> true | Open _, Ok () -> true | _ -> false) - | Flush, Res ((Unit,_), r) -> r = () + | Flush, Res ((Result (Unit,Exn),_), r) -> + (match s,r with + | Closed, Error (Sys_error _) -> false (* should not generate an error *) + | Closed, Ok () -> true + | Open _, Ok () -> true + | _ -> false) | Output_char _c, Res ((Result (Unit,Exn),_), r) -> (match s with | Closed -> true From a047e3d709d1cdbf6dae35505eff2ace224abafa Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 13:08:11 +0100 Subject: [PATCH 35/53] Allow Output_char in Closed state --- src/io/stm_tests.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 35603fd1..265cae8e 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -73,6 +73,7 @@ struct 1,return Close; 1,return Close_noerr; 3,return Flush; + 3,map (fun c -> Output_char c) char_gen; ]) | Open _ -> Gen.(frequency [ @@ -213,7 +214,8 @@ struct | Length, Closed | Close, Closed | Close_noerr, Closed - | Flush, Closed -> true + | Flush, Closed + | Output_char _, Closed -> true | _, Open _ -> true | _, _ -> false @@ -285,9 +287,10 @@ struct | Open _, Ok () -> true | _ -> false) | Output_char _c, Res ((Result (Unit,Exn),_), r) -> - (match s with - | Closed -> true - | Open _ -> r = Ok ()) (* print on closed unspecified *) + (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) + | Closed, Error (Sys_error _) -> true + | Open _, Ok () -> true + | _ -> false) | Output_byte _i, Res ((Result (Unit,Exn),_), r) -> (match s with | Closed -> true From 41be61b297c0f331ca1903fa7d3f4b7199e9db4a Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 13:30:34 +0100 Subject: [PATCH 36/53] Allow Output_byte in Closed state --- src/io/stm_tests.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 265cae8e..87fb9ff9 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -74,6 +74,7 @@ struct 1,return Close_noerr; 3,return Flush; 3,map (fun c -> Output_char c) char_gen; + 3,map (fun i -> Output_byte i) byte_gen; ]) | Open _ -> Gen.(frequency [ @@ -215,7 +216,8 @@ struct | Close, Closed | Close_noerr, Closed | Flush, Closed - | Output_char _, Closed -> true + | Output_char _, Closed + | Output_byte _, Closed -> true | _, Open _ -> true | _, _ -> false @@ -292,9 +294,10 @@ struct | Open _, Ok () -> true | _ -> false) | Output_byte _i, Res ((Result (Unit,Exn),_), r) -> - (match s with - | Closed -> true - | Open _ -> r = Ok ()) (* print on closed unspecified *) + (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) + | Closed, Error (Sys_error _) -> true + | Open _, Ok () -> true + | _ -> false) | Output_string _s, Res ((Result (Unit,Exn),_), r) -> (match s with | Closed -> true From 192a3d0157c63901f2345ab0f253331db54e4da6 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 13:32:22 +0100 Subject: [PATCH 37/53] Allow Output_string in Closed state --- src/io/stm_tests.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 87fb9ff9..588cbe8e 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -75,6 +75,7 @@ struct 3,return Flush; 3,map (fun c -> Output_char c) char_gen; 3,map (fun i -> Output_byte i) byte_gen; + 3,map (fun c -> Output_string c) string_gen; ]) | Open _ -> Gen.(frequency [ @@ -217,7 +218,8 @@ struct | Close_noerr, Closed | Flush, Closed | Output_char _, Closed - | Output_byte _, Closed -> true + | Output_byte _, Closed + | Output_string _, Closed -> true | _, Open _ -> true | _, _ -> false @@ -299,9 +301,10 @@ struct | Open _, Ok () -> true | _ -> false) | Output_string _s, Res ((Result (Unit,Exn),_), r) -> - (match s with - | Closed -> true - | Open _ -> r = Ok ()) (* print on closed unspecified *) + (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) + | Closed, Error (Sys_error _) -> true + | Open _, Ok () -> true + | _ -> false) | Output_bytes _b, Res ((Result (Unit,Exn),_), r) -> (match s with | Closed -> true From f4bfcedb9b90a065a4be36b9d75db18a06ba81a6 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 13:32:58 +0100 Subject: [PATCH 38/53] Bend the spec for Output_string in Closed state to match reality --- src/io/stm_tests.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 588cbe8e..eaa7069a 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -303,6 +303,7 @@ struct | Output_string _s, Res ((Result (Unit,Exn),_), r) -> (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) | Closed, Error (Sys_error _) -> true + | Closed, Ok () -> true (* accepting this is actually against the above spec *) | Open _, Ok () -> true | _ -> false) | Output_bytes _b, Res ((Result (Unit,Exn),_), r) -> From 474c25d1c77fb8f5608fd303bf3a43589f795e4d Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 13:35:47 +0100 Subject: [PATCH 39/53] Allow Output_bytes in Closed state --- src/io/stm_tests.ml | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index eaa7069a..444c8d93 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -76,6 +76,7 @@ struct 3,map (fun c -> Output_char c) char_gen; 3,map (fun i -> Output_byte i) byte_gen; 3,map (fun c -> Output_string c) string_gen; + 3,map (fun b -> Output_bytes b) bytes_gen; ]) | Open _ -> Gen.(frequency [ @@ -219,7 +220,8 @@ struct | Flush, Closed | Output_char _, Closed | Output_byte _, Closed - | Output_string _, Closed -> true + | Output_string _, Closed + | Output_bytes _, Closed -> true | _, Open _ -> true | _, _ -> false @@ -307,9 +309,10 @@ struct | Open _, Ok () -> true | _ -> false) | Output_bytes _b, Res ((Result (Unit,Exn),_), r) -> - (match s with - | Closed -> true - | Open _ -> r = Ok ()) (* print on closed unspecified *) + (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) + | Closed, Error (Sys_error _) -> true + | Open _, Ok () -> true + | _ -> false) | Output (b,p,l), Res ((Result (Unit,Exn),_), r) -> (match s,r with | Closed, _ From 378725bfb5c7a5f914b805f0edc1120090db6bbf Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 13:36:03 +0100 Subject: [PATCH 40/53] Bend the spec for Output_bytes in Closed state to match reality --- src/io/stm_tests.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 444c8d93..24f7ae2e 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -311,6 +311,7 @@ struct | Output_bytes _b, Res ((Result (Unit,Exn),_), r) -> (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) | Closed, Error (Sys_error _) -> true + | Closed, Ok () -> true (* accepting this is actually against the above spec *) | Open _, Ok () -> true | _ -> false) | Output (b,p,l), Res ((Result (Unit,Exn),_), r) -> From 805a634431e33db6563a1dfcf0e861d28d0f23d7 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 13:43:16 +0100 Subject: [PATCH 41/53] Allow Output in Closed state --- src/io/stm_tests.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 24f7ae2e..f92bbf41 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -77,6 +77,7 @@ struct 3,map (fun i -> Output_byte i) byte_gen; 3,map (fun c -> Output_string c) string_gen; 3,map (fun b -> Output_bytes b) bytes_gen; + 3,map3 (fun b p l -> Output (b,p,l)) bytes_gen byte_gen byte_gen; ]) | Open _ -> Gen.(frequency [ @@ -221,7 +222,8 @@ struct | Output_char _, Closed | Output_byte _, Closed | Output_string _, Closed - | Output_bytes _, Closed -> true + | Output_bytes _, Closed + | Output _, Closed -> true | _, Open _ -> true | _, _ -> false @@ -315,13 +317,13 @@ struct | Open _, Ok () -> true | _ -> false) | Output (b,p,l), Res ((Result (Unit,Exn),_), r) -> - (match s,r with - | Closed, _ + (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) + | Closed, Error (Sys_error _) -> true | Open _, Ok () -> true - | Open _, Error (Invalid_argument _) -> (*"output"*) + | (Open _|Closed), Error (Invalid_argument _) -> (*"output"*) let bytes_len = Bytes.length b in p < 0 || p >= bytes_len || l < 0 || p+l > bytes_len - | Open _, _ -> false) + | _, _ -> false) | Output_substring (str,p,l), Res ((Result (Unit,Exn),_), r) -> (match s,r with | Closed, _ From 12a3e802e13f873141066f02520c8828cab74995 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 13:43:43 +0100 Subject: [PATCH 42/53] Bend the spec for Output in Closed state to match reality --- src/io/stm_tests.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index f92bbf41..0b81f049 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -319,6 +319,7 @@ struct | Output (b,p,l), Res ((Result (Unit,Exn),_), r) -> (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) | Closed, Error (Sys_error _) -> true + | Closed, Ok () -> true (* accepting this is actually against the above spec *) | Open _, Ok () -> true | (Open _|Closed), Error (Invalid_argument _) -> (*"output"*) let bytes_len = Bytes.length b in From 41fdf0862c995a413373a5f01a999f7abcde3fb9 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 13:48:07 +0100 Subject: [PATCH 43/53] Allow Output_substring in Closed state --- src/io/stm_tests.ml | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 0b81f049..5467e1e8 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -78,6 +78,7 @@ struct 3,map (fun c -> Output_string c) string_gen; 3,map (fun b -> Output_bytes b) bytes_gen; 3,map3 (fun b p l -> Output (b,p,l)) bytes_gen byte_gen byte_gen; + 3,map3 (fun s p l -> Output_substring (s,p,l)) string_gen byte_gen byte_gen; ]) | Open _ -> Gen.(frequency [ @@ -223,7 +224,8 @@ struct | Output_byte _, Closed | Output_string _, Closed | Output_bytes _, Closed - | Output _, Closed -> true + | Output _, Closed + | Output_substring _, Closed -> true | _, Open _ -> true | _, _ -> false @@ -326,13 +328,13 @@ struct p < 0 || p >= bytes_len || l < 0 || p+l > bytes_len | _, _ -> false) | Output_substring (str,p,l), Res ((Result (Unit,Exn),_), r) -> - (match s,r with - | Closed, _ + (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) + | Closed, Error (Sys_error _) -> true | Open _, Ok () -> true - | Open _, Error (Invalid_argument _) -> (*"output_substring"*) + | (Open _|Closed), Error (Invalid_argument _) -> (*"output_substring"*) let str_len = String.length str in p < 0 || p >= str_len || l < 0 || p+l > str_len - | Open _, _ -> false) + | _, _ -> false) | Set_binary_mode _, Res ((Unit,_), ()) -> true | Set_buffered _, Res ((Unit,_), ()) -> true | Is_buffered, Res ((Bool,_),r) -> From 8e1ec3bc519c3b749166ea5bc8bcfabf1da78a31 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 13:57:03 +0100 Subject: [PATCH 44/53] Allow Set_binary_mode in Closed state --- src/io/stm_tests.ml | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 5467e1e8..973ba8b1 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -79,6 +79,7 @@ struct 3,map (fun b -> Output_bytes b) bytes_gen; 3,map3 (fun b p l -> Output (b,p,l)) bytes_gen byte_gen byte_gen; 3,map3 (fun s p l -> Output_substring (s,p,l)) string_gen byte_gen byte_gen; + 3,map (fun b -> Set_binary_mode b) Gen.bool; ]) | Open _ -> Gen.(frequency [ @@ -225,7 +226,8 @@ struct | Output_string _, Closed | Output_bytes _, Closed | Output _, Closed - | Output_substring _, Closed -> true + | Output_substring _, Closed + | Set_binary_mode _, Closed -> true | _, Open _ -> true | _, _ -> false @@ -245,8 +247,8 @@ struct | Output_substring (s,p,l) -> Res (result unit exn, protect (Out_channel.output_substring oc s p) l) | Set_binary_mode b -> if Sys.win32 || Sys.cygwin - then Res (unit, (Out_channel.flush oc; Out_channel.set_binary_mode oc b)) (* flush before changing mode *) - else Res (unit, Out_channel.set_binary_mode oc b) + then Res (result unit exn, protect (fun b -> (Out_channel.flush oc; Out_channel.set_binary_mode oc b)) b) (* flush before changing mode *) + else Res (result unit exn, protect (Out_channel.set_binary_mode oc) b) | Set_buffered b -> Res (unit, Out_channel.set_buffered oc b) | Is_buffered -> Res (bool, Out_channel.is_buffered oc) @@ -330,12 +332,17 @@ struct | Output_substring (str,p,l), Res ((Result (Unit,Exn),_), r) -> (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) | Closed, Error (Sys_error _) -> true + | Closed, Ok () -> true (* accepting this is actually against the above spec *) | Open _, Ok () -> true | (Open _|Closed), Error (Invalid_argument _) -> (*"output_substring"*) let str_len = String.length str in p < 0 || p >= str_len || l < 0 || p+l > str_len | _, _ -> false) - | Set_binary_mode _, Res ((Unit,_), ()) -> true + | Set_binary_mode _, Res ((Result (Unit,Exn),_), r) -> + (match s,r with + | Closed, (Ok () | Error (Sys_error _)) -> true (* set_binary_mode on closed channel unspecified *) + | Open _, Ok () -> true + | _, _ -> false) | Set_buffered _, Res ((Unit,_), ()) -> true | Is_buffered, Res ((Bool,_),r) -> (match s with From 1adfd60944ce958414ca36cfe9630b1aa4b36e9b Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 14:02:44 +0100 Subject: [PATCH 45/53] Allow Set_buffered in Closed state --- src/io/stm_tests.ml | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 973ba8b1..b7e6b89b 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -80,6 +80,7 @@ struct 3,map3 (fun b p l -> Output (b,p,l)) bytes_gen byte_gen byte_gen; 3,map3 (fun s p l -> Output_substring (s,p,l)) string_gen byte_gen byte_gen; 3,map (fun b -> Set_binary_mode b) Gen.bool; + 3,map (fun b -> Set_buffered b) Gen.bool; ]) | Open _ -> Gen.(frequency [ @@ -227,7 +228,8 @@ struct | Output_bytes _, Closed | Output _, Closed | Output_substring _, Closed - | Set_binary_mode _, Closed -> true + | Set_binary_mode _, Closed + | Set_buffered _, Closed -> true | _, Open _ -> true | _, _ -> false @@ -249,7 +251,7 @@ struct if Sys.win32 || Sys.cygwin then Res (result unit exn, protect (fun b -> (Out_channel.flush oc; Out_channel.set_binary_mode oc b)) b) (* flush before changing mode *) else Res (result unit exn, protect (Out_channel.set_binary_mode oc) b) - | Set_buffered b -> Res (unit, Out_channel.set_buffered oc b) + | Set_buffered b -> Res (result unit exn, protect (Out_channel.set_buffered oc) b) | Is_buffered -> Res (bool, Out_channel.is_buffered oc) let postcond c (s:state) res = match c, res with @@ -343,7 +345,11 @@ struct | Closed, (Ok () | Error (Sys_error _)) -> true (* set_binary_mode on closed channel unspecified *) | Open _, Ok () -> true | _, _ -> false) - | Set_buffered _, Res ((Unit,_), ()) -> true + | Set_buffered _, Res ((Result (Unit,Exn),_), r) -> + (match s,r with + | Closed, (Ok () | Error (Sys_error _)) -> true (* set_buffered on closed channel unspecified *) + | Open _, Ok () -> true + | _, _ -> false) | Is_buffered, Res ((Bool,_),r) -> (match s with | Closed -> true From 9500753347e9f47b3a8eb374ec468e9c6c371303 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 14:08:30 +0100 Subject: [PATCH 46/53] Allow Is_buffered in Closed state --- src/io/stm_tests.ml | 19 ++++++++++++------- 1 file changed, 12 insertions(+), 7 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index b7e6b89b..b7c38f95 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -81,6 +81,7 @@ struct 3,map3 (fun s p l -> Output_substring (s,p,l)) string_gen byte_gen byte_gen; 3,map (fun b -> Set_binary_mode b) Gen.bool; 3,map (fun b -> Set_buffered b) Gen.bool; + 3,return Is_buffered; ]) | Open _ -> Gen.(frequency [ @@ -229,9 +230,9 @@ struct | Output _, Closed | Output_substring _, Closed | Set_binary_mode _, Closed - | Set_buffered _, Closed -> true + | Set_buffered _, Closed + | Is_buffered, Closed -> true | _, Open _ -> true - | _, _ -> false let run c ({path;channel = oc} as r) = match c with | Open_text -> Res (result unit exn, protect (fun path -> (r.channel <- Out_channel.open_text path;())) path) @@ -252,7 +253,7 @@ struct then Res (result unit exn, protect (fun b -> (Out_channel.flush oc; Out_channel.set_binary_mode oc b)) b) (* flush before changing mode *) else Res (result unit exn, protect (Out_channel.set_binary_mode oc) b) | Set_buffered b -> Res (result unit exn, protect (Out_channel.set_buffered oc) b) - | Is_buffered -> Res (bool, Out_channel.is_buffered oc) + | Is_buffered -> Res (result bool exn, protect Out_channel.is_buffered oc) let postcond c (s:state) res = match c, res with | Open_text, Res ((Result (Unit,Exn),_), r) -> @@ -350,10 +351,14 @@ struct | Closed, (Ok () | Error (Sys_error _)) -> true (* set_buffered on closed channel unspecified *) | Open _, Ok () -> true | _, _ -> false) - | Is_buffered, Res ((Bool,_),r) -> - (match s with - | Closed -> true - | Open { position = _; length = _; buffered; binary_mode = _ } -> r = buffered) + | Is_buffered, Res ((Result (Bool,Exn),_), r) -> + (match s,r with + | Closed, (Ok _ | Error (Sys_error _)) -> true (* is_buffered on closed channel unspecified *) + | Open { position = _; + length = _; + buffered; + binary_mode = _ }, Ok r -> r = buffered + | _, _ -> false) | _, _ -> false end From a11d7543e734c59b2cc24e6114dce417a740b817 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 14:10:29 +0100 Subject: [PATCH 47/53] Adjust frequencies in Closed state --- src/io/stm_tests.ml | 28 ++++++++++++++-------------- 1 file changed, 14 insertions(+), 14 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index b7c38f95..896cd404 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -66,22 +66,22 @@ struct (match s with | Closed -> Gen.(frequency [ (* generate only Open or Close cmds in Closed *) - 8,return Open_text; - 3,map (fun i -> Seek i) int64_gen; - 3,return Pos; - 3,return Length; + 20,return Open_text; + 1,map (fun i -> Seek i) int64_gen; + 1,return Pos; + 1,return Length; 1,return Close; 1,return Close_noerr; - 3,return Flush; - 3,map (fun c -> Output_char c) char_gen; - 3,map (fun i -> Output_byte i) byte_gen; - 3,map (fun c -> Output_string c) string_gen; - 3,map (fun b -> Output_bytes b) bytes_gen; - 3,map3 (fun b p l -> Output (b,p,l)) bytes_gen byte_gen byte_gen; - 3,map3 (fun s p l -> Output_substring (s,p,l)) string_gen byte_gen byte_gen; - 3,map (fun b -> Set_binary_mode b) Gen.bool; - 3,map (fun b -> Set_buffered b) Gen.bool; - 3,return Is_buffered; + 1,return Flush; + 1,map (fun c -> Output_char c) char_gen; + 1,map (fun i -> Output_byte i) byte_gen; + 1,map (fun c -> Output_string c) string_gen; + 1,map (fun b -> Output_bytes b) bytes_gen; + 1,map3 (fun b p l -> Output (b,p,l)) bytes_gen byte_gen byte_gen; + 1,map3 (fun s p l -> Output_substring (s,p,l)) string_gen byte_gen byte_gen; + 1,map (fun b -> Set_binary_mode b) Gen.bool; + 1,map (fun b -> Set_buffered b) Gen.bool; + 1,return Is_buffered; ]) | Open _ -> Gen.(frequency [ From 544d564785351e145a1e735227795885c17e9785 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 14:12:22 +0100 Subject: [PATCH 48/53] Simplify precond --- src/io/stm_tests.ml | 16 +--------------- 1 file changed, 1 insertion(+), 15 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 896cd404..2475ecad 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -217,21 +217,7 @@ struct let precond c s = match c,s with | Open_text, Closed -> true | Open_text, Open _ -> false - | Seek _, Closed - | Pos, Closed - | Length, Closed - | Close, Closed - | Close_noerr, Closed - | Flush, Closed - | Output_char _, Closed - | Output_byte _, Closed - | Output_string _, Closed - | Output_bytes _, Closed - | Output _, Closed - | Output_substring _, Closed - | Set_binary_mode _, Closed - | Set_buffered _, Closed - | Is_buffered, Closed -> true + | _, Closed -> true | _, Open _ -> true let run c ({path;channel = oc} as r) = match c with From 15d62253bddb81304001d219e36085df0ff532f9 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 14:16:32 +0100 Subject: [PATCH 49/53] Adjust Open_text postcond --- src/io/stm_tests.ml | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 2475ecad..5d1c2eaa 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -243,12 +243,9 @@ struct let postcond c (s:state) res = match c, res with | Open_text, Res ((Result (Unit,Exn),_), r) -> - (match s,r with - | Closed, Ok () - | Closed, Error (Sys_error _) (*"/tmp/stm-03ba23: Too many open files"*) - | Open _, Ok () - | Open _, Error (Sys_error _) -> true - | _ -> false) + (match s,r with + | Closed, (Ok () | Error (Sys_error _)) -> true (*"/tmp/stm-03ba23: Too many open files"*) + | _ -> false) | Seek _, Res ((Result (Unit,Exn),_), r) -> (match s,r with | Closed, Error (Sys_error _) -> true (* Sys_error("Bad file descriptor") *) From 1b768307ae41c649417a6ab3f79edcfce6863c84 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 14:18:40 +0100 Subject: [PATCH 50/53] Fix indentation --- src/io/stm_tests.ml | 160 ++++++++++++++++++++++---------------------- 1 file changed, 80 insertions(+), 80 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 5d1c2eaa..61430ef7 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -248,100 +248,100 @@ struct | _ -> false) | Seek _, Res ((Result (Unit,Exn),_), r) -> (match s,r with - | Closed, Error (Sys_error _) -> true (* Sys_error("Bad file descriptor") *) - | Open _, Ok () -> true - | _ -> false) + | Closed, Error (Sys_error _) -> true (* Sys_error("Bad file descriptor") *) + | Open _, Ok () -> true + | _ -> false) | Pos, Res ((Result (Int64,Exn),_), r) -> - (match s, r with - | Closed, (Ok _ | Error (Sys_error _)) -> true (* pos on closed channel unspecified *) - | Open { position; - length = _; - buffered = _; - binary_mode = _ }, Ok p -> p = position - | _ -> false) + (match s, r with + | Closed, (Ok _ | Error (Sys_error _)) -> true (* pos on closed channel unspecified *) + | Open { position; + length = _; + buffered = _; + binary_mode = _ }, Ok p -> p = position + | _ -> false) | Length, Res ((Result (Int64,Exn),_), r) -> - (match s,r with - | Closed, Error (Sys_error _) -> true (* Sys_error("Bad file descriptor") *) - | Open { position = _; - length; - buffered = _; (* because of buffering the result and the model may disagree *) - binary_mode = _ }, Ok i -> i <= length - | _ -> false) + (match s,r with + | Closed, Error (Sys_error _) -> true (* Sys_error("Bad file descriptor") *) + | Open { position = _; + length; + buffered = _; (* because of buffering the result and the model may disagree *) + binary_mode = _ }, Ok i -> i <= length + | _ -> false) | Close, Res ((Result (Unit,Exn),_), r) -> - (match s,r with - | Closed, (Ok () | Error (Sys_error _)) (*"Close exception" - unspecified *) - | Open _, Ok () -> true - | _ -> false) + (match s,r with + | Closed, (Ok () | Error (Sys_error _)) (*"Close exception" - unspecified *) + | Open _, Ok () -> true + | _ -> false) | Close_noerr, Res ((Result (Unit,Exn),_), r) -> - (match s,r with - | Closed, Error (Sys_error _) -> false (* should not generate an error *) - | Closed, Ok () -> true - | Open _, Ok () -> true - | _ -> false) + (match s,r with + | Closed, Error (Sys_error _) -> false (* should not generate an error *) + | Closed, Ok () -> true + | Open _, Ok () -> true + | _ -> false) | Flush, Res ((Result (Unit,Exn),_), r) -> - (match s,r with - | Closed, Error (Sys_error _) -> false (* should not generate an error *) - | Closed, Ok () -> true - | Open _, Ok () -> true - | _ -> false) + (match s,r with + | Closed, Error (Sys_error _) -> false (* should not generate an error *) + | Closed, Ok () -> true + | Open _, Ok () -> true + | _ -> false) | Output_char _c, Res ((Result (Unit,Exn),_), r) -> - (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) - | Closed, Error (Sys_error _) -> true - | Open _, Ok () -> true - | _ -> false) + (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) + | Closed, Error (Sys_error _) -> true + | Open _, Ok () -> true + | _ -> false) | Output_byte _i, Res ((Result (Unit,Exn),_), r) -> - (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) - | Closed, Error (Sys_error _) -> true - | Open _, Ok () -> true - | _ -> false) + (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) + | Closed, Error (Sys_error _) -> true + | Open _, Ok () -> true + | _ -> false) | Output_string _s, Res ((Result (Unit,Exn),_), r) -> - (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) - | Closed, Error (Sys_error _) -> true - | Closed, Ok () -> true (* accepting this is actually against the above spec *) - | Open _, Ok () -> true - | _ -> false) + (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) + | Closed, Error (Sys_error _) -> true + | Closed, Ok () -> true (* accepting this is actually against the above spec *) + | Open _, Ok () -> true + | _ -> false) | Output_bytes _b, Res ((Result (Unit,Exn),_), r) -> - (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) - | Closed, Error (Sys_error _) -> true - | Closed, Ok () -> true (* accepting this is actually against the above spec *) - | Open _, Ok () -> true - | _ -> false) + (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) + | Closed, Error (Sys_error _) -> true + | Closed, Ok () -> true (* accepting this is actually against the above spec *) + | Open _, Ok () -> true + | _ -> false) | Output (b,p,l), Res ((Result (Unit,Exn),_), r) -> - (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) - | Closed, Error (Sys_error _) -> true - | Closed, Ok () -> true (* accepting this is actually against the above spec *) - | Open _, Ok () -> true - | (Open _|Closed), Error (Invalid_argument _) -> (*"output"*) - let bytes_len = Bytes.length b in - p < 0 || p >= bytes_len || l < 0 || p+l > bytes_len - | _, _ -> false) + (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) + | Closed, Error (Sys_error _) -> true + | Closed, Ok () -> true (* accepting this is actually against the above spec *) + | Open _, Ok () -> true + | (Open _|Closed), Error (Invalid_argument _) -> (*"output"*) + let bytes_len = Bytes.length b in + p < 0 || p >= bytes_len || l < 0 || p+l > bytes_len + | _, _ -> false) | Output_substring (str,p,l), Res ((Result (Unit,Exn),_), r) -> - (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) - | Closed, Error (Sys_error _) -> true - | Closed, Ok () -> true (* accepting this is actually against the above spec *) - | Open _, Ok () -> true - | (Open _|Closed), Error (Invalid_argument _) -> (*"output_substring"*) - let str_len = String.length str in - p < 0 || p >= str_len || l < 0 || p+l > str_len - | _, _ -> false) + (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) + | Closed, Error (Sys_error _) -> true + | Closed, Ok () -> true (* accepting this is actually against the above spec *) + | Open _, Ok () -> true + | (Open _|Closed), Error (Invalid_argument _) -> (*"output_substring"*) + let str_len = String.length str in + p < 0 || p >= str_len || l < 0 || p+l > str_len + | _, _ -> false) | Set_binary_mode _, Res ((Result (Unit,Exn),_), r) -> - (match s,r with - | Closed, (Ok () | Error (Sys_error _)) -> true (* set_binary_mode on closed channel unspecified *) - | Open _, Ok () -> true - | _, _ -> false) + (match s,r with + | Closed, (Ok () | Error (Sys_error _)) -> true (* set_binary_mode on closed channel unspecified *) + | Open _, Ok () -> true + | _, _ -> false) | Set_buffered _, Res ((Result (Unit,Exn),_), r) -> - (match s,r with - | Closed, (Ok () | Error (Sys_error _)) -> true (* set_buffered on closed channel unspecified *) - | Open _, Ok () -> true - | _, _ -> false) + (match s,r with + | Closed, (Ok () | Error (Sys_error _)) -> true (* set_buffered on closed channel unspecified *) + | Open _, Ok () -> true + | _, _ -> false) | Is_buffered, Res ((Result (Bool,Exn),_), r) -> - (match s,r with - | Closed, (Ok _ | Error (Sys_error _)) -> true (* is_buffered on closed channel unspecified *) - | Open { position = _; - length = _; - buffered; - binary_mode = _ }, Ok r -> r = buffered - | _, _ -> false) + (match s,r with + | Closed, (Ok _ | Error (Sys_error _)) -> true (* is_buffered on closed channel unspecified *) + | Open { position = _; + length = _; + buffered; + binary_mode = _ }, Ok r -> r = buffered + | _, _ -> false) | _, _ -> false end From bacb33e83dc39a3cd396d631de387371fab0402f Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 14:24:18 +0100 Subject: [PATCH 51/53] Sharpen the relaxed spec to only accept length 0 output w/o erroring on state Closed --- src/io/stm_tests.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 61430ef7..10f461a6 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -294,22 +294,22 @@ struct | Closed, Error (Sys_error _) -> true | Open _, Ok () -> true | _ -> false) - | Output_string _s, Res ((Result (Unit,Exn),_), r) -> + | Output_string str, Res ((Result (Unit,Exn),_), r) -> (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) | Closed, Error (Sys_error _) -> true - | Closed, Ok () -> true (* accepting this is actually against the above spec *) + | Closed, Ok () -> str = "" (* accepting this is actually against the above spec *) | Open _, Ok () -> true | _ -> false) - | Output_bytes _b, Res ((Result (Unit,Exn),_), r) -> + | Output_bytes b, Res ((Result (Unit,Exn),_), r) -> (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) | Closed, Error (Sys_error _) -> true - | Closed, Ok () -> true (* accepting this is actually against the above spec *) + | Closed, Ok () -> b = Bytes.empty (* accepting this is actually against the above spec *) | Open _, Ok () -> true | _ -> false) | Output (b,p,l), Res ((Result (Unit,Exn),_), r) -> (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) | Closed, Error (Sys_error _) -> true - | Closed, Ok () -> true (* accepting this is actually against the above spec *) + | Closed, Ok () -> l = 0 (* accepting this is actually against the above spec *) | Open _, Ok () -> true | (Open _|Closed), Error (Invalid_argument _) -> (*"output"*) let bytes_len = Bytes.length b in @@ -318,7 +318,7 @@ struct | Output_substring (str,p,l), Res ((Result (Unit,Exn),_), r) -> (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) | Closed, Error (Sys_error _) -> true - | Closed, Ok () -> true (* accepting this is actually against the above spec *) + | Closed, Ok () -> l = 0 (* accepting this is actually against the above spec *) | Open _, Ok () -> true | (Open _|Closed), Error (Invalid_argument _) -> (*"output_substring"*) let str_len = String.length str in From 2abefbd89bc8ea9e06098320f5eb57e13fe05c34 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 12 Jan 2024 14:30:59 +0100 Subject: [PATCH 52/53] Small indentation fix --- src/io/stm_tests.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index 10f461a6..a2545b95 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -349,6 +349,6 @@ module OCSTM_seq = STM_sequential.Make(OCConf) module OCSTM_dom = STM_domain.Make(OCConf) ;; QCheck_base_runner.run_tests_main [ - OCSTM_seq.agree_test ~count:1000 ~name:"STM Out_channel test sequential"; - OCSTM_dom.agree_test_par ~count:1000 ~name:"STM Out_channel test parallel"; - ] + OCSTM_seq.agree_test ~count:1000 ~name:"STM Out_channel test sequential"; + OCSTM_dom.agree_test_par ~count:1000 ~name:"STM Out_channel test parallel"; +] From 86f2ab277c22f0e15167139593137e3139ab3f13 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Mon, 22 Jan 2024 09:09:31 +0100 Subject: [PATCH 53/53] Temporarily accept Ok on a closed Out_channel --- src/io/stm_tests.ml | 24 ++++++++++++------------ 1 file changed, 12 insertions(+), 12 deletions(-) diff --git a/src/io/stm_tests.ml b/src/io/stm_tests.ml index a2545b95..bd3fb214 100644 --- a/src/io/stm_tests.ml +++ b/src/io/stm_tests.ml @@ -286,30 +286,30 @@ struct | _ -> false) | Output_char _c, Res ((Result (Unit,Exn),_), r) -> (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) - | Closed, Error (Sys_error _) -> true + | Closed, (Ok () | Error (Sys_error _)) -> true (* FIXME: temporarily accept Ok on closed channel *) | Open _, Ok () -> true | _ -> false) | Output_byte _i, Res ((Result (Unit,Exn),_), r) -> (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) - | Closed, Error (Sys_error _) -> true + | Closed, (Ok () | Error (Sys_error _)) -> true (* FIXME: temporarily accept Ok on closed channel *) | Open _, Ok () -> true | _ -> false) - | Output_string str, Res ((Result (Unit,Exn),_), r) -> + | Output_string _str, Res ((Result (Unit,Exn),_), r) -> (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) - | Closed, Error (Sys_error _) -> true - | Closed, Ok () -> str = "" (* accepting this is actually against the above spec *) + | Closed, (Ok () | Error (Sys_error _)) -> true (* FIXME: temporarily accept Ok on closed channel *) + (*| Closed, Ok () -> str = ""*) (* accepting this is actually against the above spec *) | Open _, Ok () -> true | _ -> false) - | Output_bytes b, Res ((Result (Unit,Exn),_), r) -> + | Output_bytes _b, Res ((Result (Unit,Exn),_), r) -> (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) - | Closed, Error (Sys_error _) -> true - | Closed, Ok () -> b = Bytes.empty (* accepting this is actually against the above spec *) + | Closed, (Ok () | Error (Sys_error _)) -> true (* FIXME: temporarily accept Ok on closed channel *) + (*| Closed, Ok () -> b = Bytes.empty*) (* accepting this is actually against the above spec *) | Open _, Ok () -> true | _ -> false) | Output (b,p,l), Res ((Result (Unit,Exn),_), r) -> (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) - | Closed, Error (Sys_error _) -> true - | Closed, Ok () -> l = 0 (* accepting this is actually against the above spec *) + | Closed, (Ok () | Error (Sys_error _)) -> true (* FIXME: temporarily accept Ok on closed channel *) + (*| Closed, Ok () -> l = 0*) (* accepting this is actually against the above spec *) | Open _, Ok () -> true | (Open _|Closed), Error (Invalid_argument _) -> (*"output"*) let bytes_len = Bytes.length b in @@ -317,8 +317,8 @@ struct | _, _ -> false) | Output_substring (str,p,l), Res ((Result (Unit,Exn),_), r) -> (match s,r with (* "Output functions raise a Sys_error exception when [...] applied to a closed output channel" *) - | Closed, Error (Sys_error _) -> true - | Closed, Ok () -> l = 0 (* accepting this is actually against the above spec *) + | Closed, (Ok () | Error (Sys_error _)) -> true (* FIXME: temporarily accept Ok on closed channel *) + (*| Closed, Ok () -> l = 0*) (* accepting this is actually against the above spec *) | Open _, Ok () -> true | (Open _|Closed), Error (Invalid_argument _) -> (*"output_substring"*) let str_len = String.length str in