diff --git a/src/sys/dune b/src/sys/dune new file mode 100644 index 000000000..bac13a868 --- /dev/null +++ b/src/sys/dune @@ -0,0 +1,10 @@ +;; Test of the Sys library + +(test + (name stm_tests) + (modules stm_tests) + (package multicoretests) + (libraries qcheck-stm.sequential qcheck-stm.domain) + (preprocess (pps ppx_deriving.show)) + (action (run %{test} --verbose)) +) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml new file mode 100644 index 000000000..6a640f838 --- /dev/null +++ b/src/sys/stm_tests.ml @@ -0,0 +1,319 @@ +open QCheck +open STM + +module SConf = +struct + type path = string list [@@deriving show] + + type cmd = + | File_exists of path + | Mkdir of path * string + | Rmdir of path * string + | Readdir of path + | Mkfile of path * string + [@@deriving show { with_path = false }] + + module Map_names = Map.Make (String) + + type filesys = + | Directory of {fs_map: filesys Map_names.t} + | File + + type state = filesys + + type sut = unit + + let (/) = Filename.concat + + let update_map_name map_name k v = Map_names.update k (fun _ -> Some v) map_name + + (* var gen_existing_path : filesys -> path Gen.t *) + let rec gen_existing_path fs = + match fs with + | File -> Gen.return [] + | Directory d -> + (match Map_names.bindings d.fs_map with + | [] -> Gen.return [] + | bindings -> Gen.(oneofl bindings >>= fun (n, sub_fs) -> + Gen.oneof [ + Gen.return [n]; + Gen.map (fun l -> n::l) (gen_existing_path sub_fs)] + ) + ) + + (* var gen_existing_pair : filesys -> (path * string) option Gen.t *) + let rec gen_existing_pair fs = match fs with + | File -> Gen.return None (*failwith "no sandbox directory"*) + | Directory d -> + (match Map_names.bindings d.fs_map with + | [] -> Gen.return None + | bindings -> + Gen.(oneofl bindings >>= fun (n, sub_fs) -> + oneof [ + return (Some ([],n)); + map (function None -> Some ([],n) + | Some (path,name) -> Some (n::path,name)) (gen_existing_pair sub_fs)] + ) + ) + + let name_gen = Gen.oneofl ["aaa" ; "bbb" ; "ccc" ; "ddd" ; "eee"] + let path_gen s = Gen.(oneof [gen_existing_path s; list_size (int_bound 5) name_gen]) (* can be empty *) + let pair_gen s = + let fresh_pair_gen = Gen.(pair (list_size (int_bound 5) name_gen)) name_gen in + Gen.(oneof [ + fresh_pair_gen; + (gen_existing_pair s >>= function None -> fresh_pair_gen + | Some (p,_) -> map (fun n -> (p,n)) name_gen); + (gen_existing_pair s >>= function None -> fresh_pair_gen + | Some (p,n) -> return (p,n)); + ]) + + let arb_cmd s = + QCheck.make ~print:show_cmd + Gen.(oneof [ + map (fun path -> File_exists path) (path_gen s); + map (fun (path,new_dir_name) -> Mkdir (path, new_dir_name)) (pair_gen s); + map (fun (path,delete_dir_name) -> Rmdir (path, delete_dir_name)) (pair_gen s); + map (fun path -> Readdir path) (path_gen s); + map (fun (path,new_file_name) -> Mkfile (path, new_file_name)) (pair_gen s); + ]) + + let sandbox_root = "_sandbox" + + let init_state = Directory {fs_map = Map_names.empty} + + let rec find_opt_model fs path = + match fs with + | File -> + if path = [] + then Some fs + else None + | Directory d -> + (match path with + | [] -> Some (Directory d) + | hd :: tl -> + (match Map_names.find_opt hd d.fs_map with + | None -> None + | Some fs -> find_opt_model fs tl)) + + let mem_model fs path = find_opt_model fs path <> None + + let rec mkdir_model fs path new_dir_name = + match fs with + | File -> fs + | Directory d -> + (match path with + | [] -> + let new_dir = Directory {fs_map = Map_names.empty} in + Directory {fs_map = Map_names.add new_dir_name new_dir d.fs_map} + | next_in_path :: tl_path -> + (match Map_names.find_opt next_in_path d.fs_map with + | None -> fs + | Some sub_fs -> + let nfs = mkdir_model sub_fs tl_path new_dir_name in + if nfs = sub_fs + then fs + else + let new_map = Map_names.remove next_in_path d.fs_map in + let new_map = Map_names.add next_in_path nfs new_map in + Directory {fs_map = new_map})) + + let readdir_model fs path = + match find_opt_model fs path with + | None -> None + | Some fs -> + (match fs with + | File -> None + | Directory d -> Some (Map_names.fold (fun k _ l -> k::l) d.fs_map [])) + + let rec rmdir_model fs path delete_dir_name = + match fs with + | File -> fs + | Directory d -> + (match path with + | [] -> + (match Map_names.find_opt delete_dir_name d.fs_map with + | Some (Directory target) when Map_names.is_empty target.fs_map -> + Directory {fs_map = Map_names.remove delete_dir_name d.fs_map} + | None | Some File | Some (Directory _) -> fs) + | next_in_path :: tl_path -> + (match Map_names.find_opt next_in_path d.fs_map with + | None -> fs + | Some sub_fs -> + let nfs = rmdir_model sub_fs tl_path delete_dir_name in + if nfs = sub_fs + then fs + else Directory {fs_map = (update_map_name d.fs_map next_in_path nfs)})) + + let rec mkfile_model fs path new_file_name = + match fs with + | File -> fs + | Directory d -> + (match path with + | [] -> + let new_file = File in + Directory {fs_map = Map_names.add new_file_name new_file d.fs_map} + | next_in_path :: tl_path -> + (match Map_names.find_opt next_in_path d.fs_map with + | None -> fs + | Some sub_fs -> + let nfs = mkfile_model sub_fs tl_path new_file_name in + if nfs = sub_fs + then fs + else Directory {fs_map = update_map_name d.fs_map next_in_path nfs})) + + let next_state c fs = + match c with + | File_exists _path -> fs + | Mkdir (path, new_dir_name) -> + if mem_model fs (path @ [new_dir_name]) + then fs + else mkdir_model fs path new_dir_name + | Rmdir (path,delete_dir_name) -> + if mem_model fs (path @ [delete_dir_name]) + then rmdir_model fs path delete_dir_name + else fs + | Readdir _path -> fs + | Mkfile (path, new_file_name) -> + if mem_model fs (path @ [new_file_name]) + then fs + else mkfile_model fs path new_file_name + + let init_sut () = + try Sys.mkdir sandbox_root 0o700 + with Sys_error msg when msg = sandbox_root ^ ": File exists" -> () + + let cleanup _ = + match Sys.os_type with + | "Unix" -> ignore (Sys.command ("rm -r " ^ Filename.quote sandbox_root)) + | "Win32" -> ignore (Sys.command ("rd /s /q " ^ Filename.quote sandbox_root)) + | v -> failwith ("Sys tests not working with " ^ v) + + let precond _c _s = true + + let p path = (List.fold_left (/) sandbox_root path) + + let mkfile filepath = + let flags = [Open_wronly; Open_creat; Open_excl] in + Out_channel.with_open_gen flags 0o666 filepath (fun _ -> ()) + + let run c _file_name = + match c with + | File_exists path -> Res (bool, Sys.file_exists (p path)) + | Mkdir (path, new_dir_name) -> + Res (result unit exn, protect (Sys.mkdir ((p path) / new_dir_name)) 0o755) + | Rmdir (path, delete_dir_name) -> + Res (result unit exn, protect (Sys.rmdir) ((p path) / delete_dir_name)) + | Readdir path -> + Res (result (array string) exn, protect (Sys.readdir) (p path)) + | Mkfile (path, new_file_name) -> + Res (result unit exn, protect mkfile (p path / new_file_name)) + + let fs_is_a_dir fs = match fs with | Directory _ -> true | File -> false + + let path_is_a_dir fs path = + match find_opt_model fs path with + | None -> false + | Some target_fs -> fs_is_a_dir target_fs + + let postcond c (fs: filesys) res = + match c, res with + | File_exists path, Res ((Bool,_),b) -> b = mem_model fs path + | Mkdir (path, new_dir_name), Res ((Result (Unit,Exn),_), res) -> + let complete_path = (path @ [new_dir_name]) in + (match res with + | Error err -> + (match err with + | Sys_error s -> + (s = (p complete_path) ^ ": Permission denied") || + (s = (p complete_path) ^ ": File exists" && mem_model fs complete_path) || + ((s = (p complete_path) ^ ": No such file or directory" + || s = (p complete_path) ^ ": Invalid argument") && not (mem_model fs path)) || + if Sys.win32 && not (path_is_a_dir fs complete_path) + then s = (p complete_path) ^ ": No such file or directory" + else s = (p complete_path) ^ ": Not a directory" + | _ -> false) + | Ok () -> mem_model fs path && path_is_a_dir fs path && not (mem_model fs complete_path)) + | Rmdir (path, delete_dir_name), Res ((Result (Unit,Exn),_), res) -> + let complete_path = (path @ [delete_dir_name]) in + (match res with + | Error err -> + (match err with + | Sys_error s -> + (s = (p complete_path) ^ ": Permission denied") || + (s = (p complete_path) ^ ": Directory not empty" && not (readdir_model fs complete_path = Some [])) || + (s = (p complete_path) ^ ": No such file or directory" && not (mem_model fs complete_path)) || + if Sys.win32 && not (path_is_a_dir fs complete_path) (* if not a directory *) + then s = (p complete_path) ^ ": Invalid argument" + else s = (p complete_path) ^ ": Not a directory" + | _ -> false) + | Ok () -> + mem_model fs complete_path && path_is_a_dir fs complete_path && readdir_model fs complete_path = Some []) + | Readdir path, Res ((Result (Array String,Exn),_), res) -> + (match res with + | Error err -> + (match err with + | Sys_error s -> + (s = (p path) ^ ": Permission denied") || + (s = (p path) ^ ": No such file or directory" && not (mem_model fs path)) || + if Sys.win32 && not (path_is_a_dir fs path) (* if not a directory *) + then s = (p path) ^ ": Invalid argument" + else s = (p path) ^ ": Not a directory" + | _ -> false) + | Ok array_of_subdir -> + (* Temporary work around for mingW, see https://github.com/ocaml/ocaml/issues/11829 *) + if Sys.win32 && not (mem_model fs path) + then array_of_subdir = [||] + else + (mem_model fs path && path_is_a_dir fs path && + (match readdir_model fs path with + | None -> false + | Some l -> + List.sort String.compare l + = List.sort String.compare (Array.to_list array_of_subdir)))) + | Mkfile (path, new_file_name), Res ((Result (Unit,Exn),_),res) -> ( + let complete_path = path @ [ new_file_name ] in + let concatenated_path = p complete_path in + let match_msg err msg = err = concatenated_path ^ ": " ^ msg in + let match_msgs err = List.exists (match_msg err) in + let msgs_already_exists = ["File exists"; "Permission denied"] + (* Permission denied: seen (sometimes?) on Windows *) + and msgs_non_existent_dir = ["No such file or directory"; + "Invalid argument"; + "Permission denied"] + (* Invalid argument: seen on macOS + Permission denied: seen on Windows *) + and msg_path_not_dir = + match Sys.os_type with + | "Unix" -> "Not a directory" + | "Win32" -> "No such file or directory" + | v -> failwith ("Sys tests not working with " ^ v) + in + match res with + | Error err -> ( + match err with + | Sys_error s -> + (mem_model fs complete_path && match_msgs s msgs_already_exists) + || (not (mem_model fs path) && match_msgs s msgs_non_existent_dir) + || (not (path_is_a_dir fs path) && match_msg s msg_path_not_dir) + | _ -> false) + | Ok () -> path_is_a_dir fs path && not (mem_model fs complete_path)) + | _,_ -> false +end + +let uname_os () = + let ic = Unix.open_process_in "uname -s" in + let os = In_channel.input_line ic in + ignore (Unix.close_process_in ic); + os + +module Sys_seq = STM_sequential.Make(SConf) +module Sys_dom = STM_domain.Make(SConf) + +;; +QCheck_base_runner.run_tests_main [ + Sys_seq.agree_test ~count:1000 ~name:"STM Sys test sequential"; + if Sys.unix && uname_os () = Some "Linux" + then Sys_dom.agree_test_par ~count:200 ~name:"STM Sys test parallel" + else Sys_dom.neg_agree_test_par ~count:1000 ~name:"STM Sys test parallel" + ]