Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add Out_channel STM tests #431

Merged
merged 53 commits into from
Jan 23, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
53 commits
Select commit Hold shift + click to select a range
71083dd
Initial STM tests of Out_channel
jmid Jun 15, 2023
5e3f2e8
More Out_channel STM hacking
jmid Jun 16, 2023
72a5458
Update positions accordingly
jmid Jan 5, 2024
fc97895
Length before flushing may not be up-to-date
jmid Jan 5, 2024
46774d6
Whitespace/comment polish
jmid Jan 5, 2024
894c643
Add Seek cmd
jmid Jan 5, 2024
c3677ad
Add close_noerr cmd
jmid Jan 5, 2024
04a0f95
Add output_byte cmd
jmid Jan 5, 2024
c69ec6d
Add output_bytes cmd
jmid Jan 5, 2024
f4aede1
Add output cmd
jmid Jan 5, 2024
f89ee56
Add output_substring cmd
jmid Jan 5, 2024
a90cd18
Adjust weights
jmid Jan 5, 2024
bfa89df
Clean up next_state
jmid Jan 5, 2024
1bbef88
Remove dead code
jmid Jan 5, 2024
76ca5f7
More code clean-ups
jmid Jan 5, 2024
b67b560
Add initial is_buffered cmd
jmid Jan 5, 2024
172130a
Add set_buffered cmd
jmid Jan 5, 2024
5deb8b1
Add set_binary_mode cmd
jmid Jan 5, 2024
8799ba6
Adjust output{_char,_string,_bytes,,_substring} to reflect nl transla…
jmid Jan 5, 2024
44c16de
Adjust translation on MinGW+Cygwin to change length, not position - a…
jmid Jan 5, 2024
32fd287
Flush before changing binary mode on Windows, for output to reflect p…
jmid Jan 5, 2024
bc1bee4
Remove Lin Out_channel tests
jmid Jan 5, 2024
75447d6
Remove unused argument to Closed
jmid Jan 11, 2024
ae8a0aa
Rename prefix lin-dsl- to stm-
jmid Jan 11, 2024
181a99c
Document the reason for Length result/model mismatch
jmid Jan 11, 2024
1dbafd5
Factor out windows text-mode test
jmid Jan 11, 2024
5d3b2c9
Clean-up old comments
jmid Jan 11, 2024
6597741
Wrap close_noerr in protect
jmid Jan 11, 2024
298bdea
Support generating Close* cmds in state Closed
jmid Jan 11, 2024
497975e
Start in open channel to avoid Stdlib.stdout special cases
jmid Jan 12, 2024
df35b3c
Allow Length in Closed state
jmid Jan 12, 2024
a7b427f
Allow Seek in Closed state
jmid Jan 12, 2024
c6e6d04
Allow Pos in Closed state
jmid Jan 12, 2024
066025a
Allow Flush in Closed state
jmid Jan 12, 2024
a047e3d
Allow Output_char in Closed state
jmid Jan 12, 2024
41be61b
Allow Output_byte in Closed state
jmid Jan 12, 2024
192a3d0
Allow Output_string in Closed state
jmid Jan 12, 2024
f4bfced
Bend the spec for Output_string in Closed state to match reality
jmid Jan 12, 2024
474c25d
Allow Output_bytes in Closed state
jmid Jan 12, 2024
378725b
Bend the spec for Output_bytes in Closed state to match reality
jmid Jan 12, 2024
805a634
Allow Output in Closed state
jmid Jan 12, 2024
12a3e80
Bend the spec for Output in Closed state to match reality
jmid Jan 12, 2024
41fdf08
Allow Output_substring in Closed state
jmid Jan 12, 2024
8e1ec3b
Allow Set_binary_mode in Closed state
jmid Jan 12, 2024
1adfd60
Allow Set_buffered in Closed state
jmid Jan 12, 2024
9500753
Allow Is_buffered in Closed state
jmid Jan 12, 2024
a11d754
Adjust frequencies in Closed state
jmid Jan 12, 2024
544d564
Simplify precond
jmid Jan 12, 2024
15d6225
Adjust Open_text postcond
jmid Jan 12, 2024
1b76830
Fix indentation
jmid Jan 12, 2024
bacb33e
Sharpen the relaxed spec to only accept length 0 output w/o erroring …
jmid Jan 12, 2024
2abefbd
Small indentation fix
jmid Jan 12, 2024
86f2ab2
Temporarily accept Ok on a closed Out_channel
jmid Jan 22, 2024
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
12 changes: 9 additions & 3 deletions src/io/dune
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -37,3 +35,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))
)
16 changes: 4 additions & 12 deletions src/io/lin_tests_domain.ml
Original file line number Diff line number Diff line change
@@ -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
58 changes: 0 additions & 58 deletions src/io/lin_tests_spec_io.ml
Original file line number Diff line number Diff line change
Expand Up @@ -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
4 changes: 1 addition & 3 deletions src/io/lin_tests_thread.ml
Original file line number Diff line number Diff line change
@@ -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";
]
Loading
Loading