Skip to content

Add (failing) {In,Out}_channel linearization tests #13

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

Closed
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
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
29 changes: 29 additions & 0 deletions src/in_out_channel/dune
Original file line number Diff line number Diff line change
@@ -0,0 +1,29 @@
;; Linearizability tests of the stdlib Queue library

;; this prevents the tests from running on a default build
(alias
(name default)
(package multicoretests)
(deps lin_tests.exe))

(env
(_
(binaries
(../check_error_count.exe as check_error_count))))


(executable
(name lin_tests)
(modules lin_tests)
(flags (:standard -w -27))
(libraries util lin))

(rule
(alias runtest)
(package multicoretests)
(action
(progn
(with-accepted-exit-codes 1
(with-stdout-to "lin-output.txt" (run ./lin_tests.exe --no-colors --verbose)))
(cat lin-output.txt)
(run %{bin:check_error_count} "lin_tests" 1 lin-output.txt))))
129 changes: 129 additions & 0 deletions src/in_out_channel/lin_tests.ml
Original file line number Diff line number Diff line change
@@ -0,0 +1,129 @@
(* First generate a big temporary file with random contents. *)
let temp_readonly = Filename.temp_file "fuzz_stdlib" ""

let temp_readonly_size = 1_000_000

let () =
Random.self_init ();
let out = Out_channel.open_bin temp_readonly in
for _ = 1 to temp_readonly_size do
Out_channel.output_byte out @@ Random.bits () lsr 22
done;
Out_channel.close out

module In_channel_ops = struct

type t = In_channel.t (* Filename and corresponding channel *)

type cmd = Close | Read of int | BlindRead of int

let show_cmd =
let open Printf in function
| Close -> "Close"
| Read l -> sprintf "Read %d" l
| BlindRead l -> sprintf "BlindRead %d" l

let gen_cmd =
let open QCheck.Gen in
frequency
[1, return Close;
6, map (fun l -> Read l) small_nat;
6, map (fun l -> BlindRead l) small_nat;
]

type res =
| UnitRes of (unit, exn) result
| ReadRes of (string option, exn) result

let show_res =
let open Printf in function
| UnitRes (Ok ()) -> "()"
| UnitRes (Error e) -> sprintf "UnitRes exception %s" (Printexc.to_string e)
| ReadRes (Ok (Some s)) -> sprintf "\"%s\"" s
| ReadRes (Ok None) -> "None"
| ReadRes (Error e) -> sprintf "ReadRes exception %s" (Printexc.to_string e)

let init () =
In_channel.open_bin temp_readonly

let cleanup chan =
In_channel.close chan

let run cmd chan =
match cmd with
| Read l ->
begin try ReadRes (Ok (In_channel.really_input_string chan l))
with e -> ReadRes (Error e)
end
| BlindRead l ->
begin try ignore (In_channel.really_input_string chan l); UnitRes (Ok ())
with e -> UnitRes (Error e)
end
| Close ->
begin try In_channel.close chan; UnitRes (Ok ())
with e -> UnitRes (Error e)
end
end

module Out_channel_ops = struct

type t = string * Out_channel.t (* Filename and corresponding channel *)

type cmd = Flush | Close | Write of string

let show_cmd =
let open Printf in function
| Flush -> "Flush"
| Write s -> sprintf "Write %s" s
| Close -> "Close"

let gen_cmd =
let open QCheck.Gen in
frequency
[3, return Flush;
1, return Close;
6, map (fun s -> Write s) string;
]

type res = (unit, exn) result

let show_res =
let open Printf in function
| Ok () -> sprintf "()"
| Error e -> sprintf "exception %s" (Printexc.to_string e)

let init () =
let filename = Filename.temp_file "fuzz_stdlib" "" in
filename, Out_channel.open_text filename

let cleanup (filename, chan) =
Out_channel.close chan;
try Sys.remove filename with Sys_error _ -> ()

let run cmd (_,chan) =
match cmd with
| Flush ->
begin try Out_channel.flush chan; Ok ()
with e -> Error e
end
| Write s ->
begin try Out_channel.output_string chan s; Ok ()
with e -> Error e
end
| Close ->
begin try Out_channel.close chan; Ok ()
with e -> Error e
end
end

module Out_channel_lin = Lin.Make (Out_channel_ops)
module In_channel_lin = Lin.Make (In_channel_ops)

let () =
QCheck_runner.run_tests_main
[ Out_channel_lin.lin_test ~count:1000 ~name:"Out_channel" `Domain;
In_channel_lin.lin_test ~count:1000 ~name:"In_channel" `Domain;
]

let () =
Sys.remove temp_readonly