Add IO tests

src/io/dune

@@ -0,0 +1,37 @@
+;; Linearizability tests of the I/O operations
+
+(test
+ (name lin_tests)
+ (modules lin_tests)
+ (package multicoretests)
+ ;(flags (:standard -w -27))
+ (libraries qcheck-lin.domain)
+ ; (action (run %{test} --verbose))
+ (action (echo "Skipping src/io/%{test} from the test suite\n\n"))
+)
+
+(library
+ (name lin_tests_dsl_common_io)
+ (modules lin_tests_dsl_common)
+ (package multicoretests)
+ (libraries qcheck-lin.lin)
+)
+
+(test
+ (name lin_tests_dsl_domain)
+ (modules lin_tests_dsl_domain)
+ (package multicoretests)
+ ;(flags (:standard -w -27))
+ (libraries qcheck-lin.domain lin_tests_dsl_common_io)
+ (action (run %{test} --verbose))
+)
+
+(test
+ (name lin_tests_dsl_thread)
+ (modules lin_tests_dsl_thread)
+ (package multicoretests)
+ ;(flags (:standard -w -27))
+ (libraries qcheck-lin.thread lin_tests_dsl_common_io)
+ ; (action (run %{test} --verbose))
+ (action (echo "Skipping src/io/%{test} from the test suite\n\n"))
+)

src/io/lin_tests.ml

@@ -0,0 +1,137 @@
+(* 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;
+      ]
+
+  let shrink_cmd _ = QCheck.Iter.empty
+
+  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 equal_res = (=)
+
+  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;
+      ]
+
+  let shrink_cmd _ = QCheck.Iter.empty
+
+  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 equal_res = (=)
+
+  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_domain.Make_internal (Out_channel_ops) [@@alert "-internal"]
+module In_channel_lin = Lin_domain.Make_internal (In_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";
+    ]
+
+let () =
+  Sys.remove temp_readonly

src/io/lin_tests_dsl_common.ml

@@ -0,0 +1,88 @@
+(* ********************************************************************** *)
+(*                      Tests of in and out channels                      *)
+(* ********************************************************************** *)
+
+module ICConf : Lin.Spec = struct
+  type t = In_channel.t
+
+  let init () = In_channel.open_bin Sys.argv.(0)
+  let cleanup = In_channel.close
+
+  open Lin
+  let int,int64 = nat_small,nat64_small
+
+  let api = [
+    (* Only one t is tested, so skip stdin and opening functions *)
+    (* val_ "In_channel.stdin"               In_channel.stdin                 (t) ; *)
+    (* val_ "In_channel.open_bin"            In_channel.open_bin              (string @-> t) ; *)
+    (* val_ "In_channel.open_text"           In_channel.open_text             (string @-> t) ; *)
+    (* val_ "In_channel.open_gen"            In_channel.open_gen              (open_flag list @-> int @-> string @-> t) ; *)
+    (* val_ "In_channel.with_open_bin"       In_channel.with_open_bin         (string @-> (t @-> 'a) @-> 'a) ; *)
+    (* val_ "In_channel.with_open_text"      In_channel.with_open_text        (string @-> (t @-> 'a) @-> 'a) ; *)
+    (* val_ "In_channel.with_open_gen"       In_channel.with_open_gen         (open_flag list @-> int @-> string @-> (t @-> 'a) @-> 'a) ; *)
+
+    val_ "In_channel.seek"                In_channel.seek                  (t @-> int64 @-> returning_or_exc unit) ;
+    val_ "In_channel.pos"                 In_channel.pos                   (t @-> returning int64) ;
+    val_ "In_channel.length"              In_channel.length                (t @-> returning_or_exc int64) ;
+    val_ "In_channel.close"               In_channel.close                 (t @-> returning unit) ;
+    val_ "In_channel.close_noerr"         In_channel.close_noerr           (t @-> returning unit) ;
+    val_ "In_channel.input_char"          In_channel.input_char            (t @-> returning_or_exc (option char)) ;
+    val_ "In_channel.input_byte"          In_channel.input_byte            (t @-> returning_or_exc (option int)) ;
+    val_ "In_channel.input_line"          In_channel.input_line            (t @-> returning_or_exc (option string)) ;
+    (* bytes not yet supported by the Lin library *)
+    (* val_ "In_channel.input"               In_channel.input                 (t @-> bytes @-> int @-> int @-> returning int) ; *)
+    (* val_ "In_channel.really_input"        In_channel.really_input          (t @-> bytes @-> int @-> int @-> returning (option unit)) ; *)
+    val_ "In_channel.really_input_string" In_channel.really_input_string   (t @-> int @-> returning_or_exc (option string)) ;
+    (* input_all generates counter-examples that are impossibly long *)
+    (* val_ "In_channel.input_all"           In_channel.input_all             (t @-> returning_or_exc string) ; *)
+    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 = string * Out_channel.t
+
+  let init () = Filename.open_temp_file "lin-dsl-" ""
+  let cleanup (path, chan) =
+    Out_channel.close chan ;
+    Sys.remove path
+
+  (* turn [f: Out_channel.t -> ...] into [lift f: t -> ...] *)
+  let lift f (_, chan) = f chan
+
+  open Lin
+  let int,int64,string = nat_small,nat64_small,string_small
+  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_ "Out_channel.seek"             (lift Out_channel.seek)             (t @-> int64 @-> returning_or_exc unit) ;
+    val_ "Out_channel.pos"              (lift Out_channel.pos)              (t @-> returning_or_exc int64) ;
+    val_ "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"     Out_channel.output_bytes     (t @-> bytes @-> returning unit) ; *)
+    (* val_ "Out_channel.output"           Out_channel.output           (t @-> bytes @-> int @-> int @-> returning 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) ;
+  ]
+end

src/io/lin_tests_dsl_domain.ml

@@ -0,0 +1,14 @@
+(* ********************************************************************** *)
+(*                      Tests of in and out channels                      *)
+(* ********************************************************************** *)
+
+open Lin_tests_dsl_common_io.Lin_tests_dsl_common
+
+module IC_domain = Lin_domain.Make(ICConf)
+module OC_domain = Lin_domain.Make(OCConf)
+
+let _ =
+  QCheck_base_runner.run_tests_main [
+    IC_domain.neg_lin_test ~count:1000 ~name:"Lin DSL In_channel test with Domain";
+    OC_domain.neg_lin_test ~count:1000 ~name:"Lin DSL Out_channel test with Domain";
+  ]

src/io/lin_tests_dsl_thread.ml

@@ -0,0 +1,14 @@
+(* ********************************************************************** *)
+(*                      Tests of in and out channels                      *)
+(* ********************************************************************** *)
+
+open Lin_tests_dsl_common_io.Lin_tests_dsl_common
+
+module IC_thread = Lin_thread.Make(ICConf) [@@alert "-experimental"]
+module OC_thread = Lin_thread.Make(OCConf) [@@alert "-experimental"]
+
+let _ =
+  QCheck_base_runner.run_tests_main [
+    IC_thread.neg_lin_test ~count:1000 ~name:"Lin DSL In_channel test with Thread";
+    OC_thread.neg_lin_test ~count:1000 ~name:"Lin DSL Out_channel test with Thread";
+  ]