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.

Sign up for GitHub

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

Lin Out_channel shrink cleanup #387

Merged
merged 11 commits into from
Sep 1, 2023
Merged

Lin Out_channel shrink cleanup #387

Show file tree
Hide file tree
Changes from 8 commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
bf61729
Disable bytes char shrinking for Lin Out_channel test
jmid Aug 15, 2023
d5ff92a
Disable string char shrinking for Lin Out_channel test
jmid Aug 15, 2023
2433827
Remove lift to reduce allocations
jmid Aug 17, 2023
ba20a6f
Adjust frequencies to reduce flush_all-triggered allocations
jmid Aug 17, 2023
6c8db20
Comment out Out_channel.flush_all to keep GC manageable
jmid Aug 30, 2023
e1a1de3
Reduce allocations when restarting check_seq_cons search
jmid Aug 28, 2023
460b97c
Steps to bring Out_channel tests in src/io/lin_tests.ml up to speed w…
jmid Aug 30, 2023
f7223d6
Swap test order to match module declaration order
jmid Aug 30, 2023
1b50d2f
Address review: cleaner call to interp_plain_ignore
jmid Aug 31, 2023
bb94d34
Add a CHANGES entry for the Lin allocation improvement
jmid Aug 31, 2023
b9509bb
Merge branch 'main' into outchannel-shrink-cleanup
jmid Aug 31, 2023
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
5 changes: 4 additions & 1 deletion lib/lin.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -47,6 +47,9 @@ struct
(* plain interpreter of a cmd list *)
let interp_plain sut cs = List.map (fun c -> (c, Spec.run c sut)) cs

(* plain interpreter ignoring the output and allocating less *)
let interp_plain_ignore sut cs = List.iter (fun c -> ignore (Spec.run c sut)) cs

let rec gen_cmds fuel =
Gen.(if fuel = 0
then return []
Expand Down Expand Up @@ -113,7 +116,7 @@ struct
||
(* rerun to get seq_sut to same cmd branching point *)
(let seq_sut' = Spec.init () in
let _ = interp_plain seq_sut' (List.rev seq_trace) in
let _ = interp_plain_ignore seq_sut' (List.rev seq_trace) in
jmid marked this conversation as resolved.
Show resolved Hide resolved
if Spec.equal_res res2 (Spec.run c2 seq_sut')
then check_seq_cons pref cs1 cs2' seq_sut' (c2::seq_trace)
else (Spec.cleanup seq_sut'; false))
Expand Down
84 changes: 54 additions & 30 deletions src/io/lin_tests.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -71,66 +71,90 @@ end

module Out_channel_ops = struct

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

type cmd = Flush | Close | Write of string
type t = Out_channel.t
let path = ref ""

type cmd =
| Seek of int64
| Close
| Flush
| Output_string of string
| Set_binary_mode of bool
| Set_buffered of bool
| Is_buffered

let show_cmd =
let open Printf in function
| Flush -> "Flush"
| Write s -> sprintf "Write %s" s
| Seek i -> sprintf "Seek %Li" i
| Close -> "Close"
| Flush -> "Flush"
| Output_string s -> sprintf "Output_string %s" s
| Set_binary_mode b -> sprintf "Set_binary_mode %s" QCheck.Print.(bool b)
| Set_buffered b -> sprintf "Set_buffered %s" QCheck.Print.(bool b)
| Is_buffered -> "Is_buffered"

let gen_cmd =
let open QCheck.Gen in
frequency
[3, return Flush;
1, return Close;
6, map (fun s -> Write s) string;
[10, map (fun i -> Seek (Int64.of_int i)) small_nat;
10, return Close;
10, return Flush;
10, map (fun s -> Output_string s) string_small;
10, map (fun b -> Set_binary_mode b) bool;
10, map (fun b -> Set_buffered b) bool;
10, return Is_buffered;
]

let shrink_cmd _ = QCheck.Iter.empty

type res = (unit, exn) result
type inner_res = Unit | Bool of bool
type res = (inner_res, exn) result

let show_res =
let open Printf in function
| Ok () -> sprintf "()"
| Error e -> sprintf "exception %s" (Printexc.to_string e)
| Ok r -> (match r with
| Unit -> sprintf "()"
| Bool b -> QCheck.Print.(bool b)
)
| Error e -> sprintf "exception %s" (Printexc.to_string e)

let equal_res = (=)

let init () =
let filename = Filename.temp_file "fuzz_stdlib" "" in
filename, Out_channel.open_text filename
let p,ch = Filename.open_temp_file "lin-dsl-" "" in
path := p;
ch

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

let run cmd (_,chan) =
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
| Seek i ->
(try Out_channel.seek chan i; Ok Unit with e -> Error e)
| Close ->
begin try Out_channel.close chan; Ok ()
with e -> Error e
end
(try Out_channel.close chan; Ok Unit with e -> Error e)
| Flush ->
(try Out_channel.flush chan; Ok Unit with e -> Error e)
| Output_string s ->
(try Out_channel.output_string chan s; Ok Unit with e -> Error e)
| Set_binary_mode b ->
(try Out_channel.set_binary_mode chan b; Ok Unit with e -> Error e)
| Set_buffered b ->
(try Out_channel.set_buffered chan b; Ok Unit with e -> Error e)
| Is_buffered ->
(try Ok (Bool (Out_channel.is_buffered chan)) with e -> Error e)

end

module Out_channel_lin = Lin_domain.Make_internal (Out_channel_ops) [@@alert "-internal"]
module In_channel_lin = Lin_domain.Make_internal (In_channel_ops) [@@alert "-internal"]
module Out_channel_lin = Lin_domain.Make_internal (Out_channel_ops) [@@alert "-internal"]

let () =
QCheck_base_runner.run_tests_main
[ Out_channel_lin.lin_test ~count:1000 ~name:"Lin Out_channel test with domains";
In_channel_lin.lin_test ~count:1000 ~name:"Lin In_channel test with domains";
[ In_channel_lin.lin_test ~count:1000 ~name:"Lin In_channel test with domains";
Out_channel_lin.lin_test ~count:1000 ~name:"Lin Out_channel test with domains";
]

let () =
Expand Down
60 changes: 36 additions & 24 deletions src/io/lin_tests_spec_io.ml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -65,18 +65,30 @@ 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 = string * Out_channel.t
type t = Out_channel.t
let path = ref ""

let init () = Filename.open_temp_file "lin-dsl-" ""
let cleanup (path, chan) =
Out_channel.close chan ;
Sys.remove path
let init () =
let p,ch = Filename.open_temp_file "lin-dsl-" "" in
path := p;
ch

(* turn [f: Out_channel.t -> ...] into [lift f: t -> ...] *)
let lift f (_, chan) = f chan
let cleanup chan =
Out_channel.close chan;
Sys.remove !path

open Lin
let int,int64,string,bytes = nat_small,nat64_small,string_small,bytes_small
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 *)

Expand All @@ -89,21 +101,21 @@ module OCConf : Lin.Spec = struct
(* 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_ "Out_channel.seek" (lift Out_channel.seek) (t @-> int64 @-> returning_or_exc unit) ;
val_freq 3 "Out_channel.pos" (lift Out_channel.pos) (t @-> returning_or_exc int64) ;
val_freq 3 "Out_channel.length" (lift Out_channel.length) (t @-> returning_or_exc int64) ;
val_ "Out_channel.close" (lift Out_channel.close) (t @-> returning_or_exc unit) ;
val_ "Out_channel.close_noerr" (lift Out_channel.close_noerr) (t @-> returning unit) ;
val_ "Out_channel.flush" (lift Out_channel.flush) (t @-> returning_or_exc unit) ;
val_ "Out_channel.flush_all" Out_channel.flush_all (unit @-> returning_or_exc unit) ;
val_ "Out_channel.output_char" (lift Out_channel.output_char) (t @-> char @-> returning_or_exc unit) ;
val_ "Out_channel.output_byte" (lift Out_channel.output_byte) (t @-> int @-> returning_or_exc unit) ;
val_ "Out_channel.output_string" (lift Out_channel.output_string) (t @-> string @-> returning_or_exc unit) ;
val_ "Out_channel.output_bytes" (lift Out_channel.output_bytes) (t @-> bytes @-> returning_or_exc unit) ;
val_ "Out_channel.output" (lift Out_channel.output) (t @-> bytes @-> int @-> int @-> returning_or_exc unit) ;
val_ "Out_channel.output_substring" (lift Out_channel.output_substring) (t @-> string @-> int @-> int @-> returning_or_exc unit) ;
val_ "Out_channel.set_binary_mode" (lift Out_channel.set_binary_mode) (t @-> bool @-> returning_or_exc unit) ;
val_ "Out_channel.set_buffered" (lift Out_channel.set_buffered) (t @-> bool @-> returning_or_exc unit) ;
val_ "Out_channel.is_buffered" (lift Out_channel.is_buffered) (t @-> returning_or_exc bool) ;
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