From 8517a0c9cca238f9cd292aabb211e0597c0bbf45 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 1 Mar 2023 09:50:19 +0100 Subject: [PATCH 01/27] Initial test of Sys.is_directory --- src/sys/stm_tests.ml | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 8738a11e8..e7aa0527d 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -7,6 +7,7 @@ struct type cmd = | File_exists of path + | Is_directory of path | Mkdir of path * string | Rmdir of path * string | Readdir of path @@ -83,6 +84,7 @@ struct QCheck.make ~print:show_cmd Gen.(oneof [ map (fun path -> File_exists path) (path_gen s); + map (fun path -> Is_directory 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); @@ -180,6 +182,7 @@ struct if mem_model fs (path @ [new_dir_name]) then fs else mkdir_model fs path new_dir_name + | Is_directory _path -> fs | Rmdir (path,delete_dir_name) -> if mem_model fs (path @ [delete_dir_name]) then rmdir_model fs path delete_dir_name @@ -212,6 +215,7 @@ struct let run c _file_name = match c with | File_exists path -> Res (bool, Sys.file_exists (p path)) + | Is_directory path -> Res (result bool exn, protect Sys.is_directory (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) -> @@ -228,9 +232,25 @@ struct | None -> false | Some target_fs -> fs_is_a_dir target_fs + let rec path_prefixes path = match path with + | [] -> [] + | [_] -> [] + | n::ns -> [n]::(List.map (fun p -> n::p) (path_prefixes ns)) + let postcond c (fs: filesys) res = match c, res with | File_exists path, Res ((Bool,_),b) -> b = mem_model fs path + | Is_directory path, Res ((Result (Bool,Exn),_),res) -> + (match res with + | Ok b -> + (match find_opt_model fs path with + | Some (Directory _) -> b = true + | Some File -> b = false + | None -> false) + | Error (Sys_error s) -> + (s = (p path) ^ ": No such file or directory" && find_opt_model fs path = None) || + (s = p path ^ ": Not a directory" && List.exists (fun pref -> Some File = find_opt_model fs pref) (path_prefixes path)) + | _ -> false) | Mkdir (path, new_dir_name), Res ((Result (Unit,Exn),_), res) -> let complete_path = (path @ [new_dir_name]) in (match res with From f135aa025b4f50a65010d28b915c47ea4784c4a9 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 1 Mar 2023 13:00:35 +0100 Subject: [PATCH 02/27] Add Sys.remove --- src/sys/stm_tests.ml | 43 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index e7aa0527d..37a5009e3 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -8,6 +8,7 @@ struct type cmd = | File_exists of path | Is_directory of path + | Remove of path * string | Mkdir of path * string | Rmdir of path * string | Readdir of path @@ -85,6 +86,7 @@ struct Gen.(oneof [ map (fun path -> File_exists path) (path_gen s); map (fun path -> Is_directory path) (path_gen s); + map (fun (path,new_dir_name) -> Remove (path, new_dir_name)) (pair_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); @@ -111,6 +113,35 @@ struct let mem_model fs path = find_opt_model fs path <> None + let rec remove_model fs path file_name = + match fs with + | File -> fs + | Directory d -> + (match path with + | [] -> + (match Map_names.find_opt file_name d.fs_map with + | None + | Some (Directory _) -> fs + | Some File -> Directory { fs_map = Map_names.remove file_name d.fs_map } + ) + | dir::dirs -> + Directory + { fs_map = Map_names.update dir (function + | None -> None + | Some File -> Some File + | Some (Directory _ as d') -> Some (remove_model d' dirs file_name)) d.fs_map + } + (* + (match Map_names.find_opt dir d.fs_map with + | None + | Some File -> fs + | Some (Directory _ as d') -> + let fs' = remove_model d' dirs file_name in + Directory { fs_map = Map_names.update dir d.fs_map } + ) +*) + ) + let rec mkdir_model fs path new_dir_name = match fs with | File -> fs @@ -182,6 +213,7 @@ struct if mem_model fs (path @ [new_dir_name]) then fs else mkdir_model fs path new_dir_name + | Remove (path, file_name) -> remove_model fs path file_name | Is_directory _path -> fs | Rmdir (path,delete_dir_name) -> if mem_model fs (path @ [delete_dir_name]) @@ -216,6 +248,7 @@ struct match c with | File_exists path -> Res (bool, Sys.file_exists (p path)) | Is_directory path -> Res (result bool exn, protect Sys.is_directory (p path)) + | Remove (path, file_name) -> Res (result unit exn, protect Sys.remove ((p path) / file_name)) | Mkdir (path, new_dir_name) -> Res (result unit exn, protect (Sys.mkdir ((p path) / new_dir_name)) 0o755) | Rmdir (path, delete_dir_name) -> @@ -251,6 +284,16 @@ struct (s = (p path) ^ ": No such file or directory" && find_opt_model fs path = None) || (s = p path ^ ": Not a directory" && List.exists (fun pref -> Some File = find_opt_model fs pref) (path_prefixes path)) | _ -> false) + | Remove (path, file_name), Res ((Result (Unit,Exn),_), res) -> + let complete_path = (path @ [file_name]) in + (match res with + | Ok () -> mem_model fs complete_path && path_is_a_dir fs path && not (path_is_a_dir fs complete_path) + | Error (Sys_error s) -> + (s = (p complete_path) ^ ": No such file or directory" && find_opt_model fs complete_path = None) || + (s = (p complete_path) ^ ": Is a directory" && path_is_a_dir fs complete_path) || + (s = (p complete_path) ^ ": Not a directory" && not (path_is_a_dir fs path)) + | Error _ -> false + ) | Mkdir (path, new_dir_name), Res ((Result (Unit,Exn),_), res) -> let complete_path = (path @ [new_dir_name]) in (match res with From 63b676cae13b729eedd5d19594f0943e4b057687 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 1 Mar 2023 23:21:55 +0100 Subject: [PATCH 03/27] add Sys.rename and refactor a bit --- src/sys/stm_tests.ml | 167 +++++++++++++++++++++++-------------------- 1 file changed, 90 insertions(+), 77 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 37a5009e3..a7d86f47e 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -9,6 +9,7 @@ struct | File_exists of path | Is_directory of path | Remove of path * string + | Rename of path * path | Mkdir of path * string | Rmdir of path * string | Readdir of path @@ -87,6 +88,7 @@ struct map (fun path -> File_exists path) (path_gen s); map (fun path -> Is_directory path) (path_gen s); map (fun (path,new_dir_name) -> Remove (path, new_dir_name)) (pair_gen s); + map2 (fun old_path new_path -> Rename (old_path, new_path)) (path_gen s) (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); @@ -113,6 +115,35 @@ struct let mem_model fs path = find_opt_model fs path <> None + let path_is_a_dir fs path = + match find_opt_model fs path with + | None + | Some File -> false + | Some (Directory _) -> true + + let path_is_a_file fs path = + match find_opt_model fs path with + | None + | Some (Directory _) -> false + | Some File -> true + + let rec path_prefixes path = match path with + | [] -> [] + | [_] -> [] + | n::ns -> [n]::(List.map (fun p -> n::p) (path_prefixes ns)) + + let separate_path path = + match List.rev path with + | [] -> None + | name::rev_path -> Some (List.rev rev_path, name) + + let rec is_true_prefix path1 path2 = match path1, path2 with + | [], [] -> false + | [], _::_ -> true + | _::_, [] -> false + | n1::p1, n2::p2 -> n1=n2 && is_true_prefix p1 p2 + + (* generic removal function *) let rec remove_model fs path file_name = match fs with | File -> fs @@ -121,46 +152,14 @@ struct | [] -> (match Map_names.find_opt file_name d.fs_map with | None - | Some (Directory _) -> fs - | Some File -> Directory { fs_map = Map_names.remove file_name d.fs_map } - ) + | Some _ -> Directory { fs_map = Map_names.remove file_name d.fs_map }) | dir::dirs -> Directory { fs_map = Map_names.update dir (function | None -> None | Some File -> Some File | Some (Directory _ as d') -> Some (remove_model d' dirs file_name)) d.fs_map - } - (* - (match Map_names.find_opt dir d.fs_map with - | None - | Some File -> fs - | Some (Directory _ as d') -> - let fs' = remove_model d' dirs file_name in - Directory { fs_map = Map_names.update dir d.fs_map } - ) -*) - ) - - 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 @@ -170,60 +169,70 @@ struct | 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 = + (* generic insertion function *) + let rec insert_model fs path new_file_name sub_tree = 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) + Directory {fs_map = Map_names.add new_file_name sub_tree 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 = 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 + let nfs = insert_model sub_fs tl_path new_file_name sub_tree in if nfs = sub_fs then fs else Directory {fs_map = update_map_name d.fs_map next_in_path nfs})) + let rename_model fs old_path new_path = + match separate_path old_path, separate_path new_path with + | None, _ + | _, None -> fs + | Some (old_path_pref, old_name), Some (new_path_pref, new_name) -> + (match find_opt_model fs new_path_pref with + | None + | Some File -> fs + | Some (Directory _) -> + (match find_opt_model fs old_path with + | None -> fs + | Some sub_fs -> + let fs' = remove_model fs old_path_pref old_name in + insert_model fs' new_path_pref new_name sub_fs)) + 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 - | Remove (path, file_name) -> remove_model fs path file_name + else insert_model fs path new_dir_name (Directory {fs_map = Map_names.empty}) + | Remove (path, file_name) -> + if find_opt_model fs (path @ [file_name]) = Some File + then remove_model fs path file_name + else fs + | Rename (old_path, new_path) -> + if is_true_prefix old_path new_path + then fs + else + (match find_opt_model fs old_path with + | None -> fs + | Some File -> + if (not (mem_model fs new_path) || path_is_a_file fs new_path) then rename_model fs old_path new_path else fs + | Some (Directory _) -> + if (not (mem_model fs new_path) || readdir_model fs new_path = Some []) then rename_model fs old_path new_path else fs) | Is_directory _path -> fs | Rmdir (path,delete_dir_name) -> - if mem_model fs (path @ [delete_dir_name]) - then rmdir_model fs path delete_dir_name + let complete_path = path @ [delete_dir_name] in + if mem_model fs complete_path && readdir_model fs complete_path = Some [] + then remove_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 + else insert_model fs path new_file_name File let init_sut () = try Sys.mkdir sandbox_root 0o700 @@ -249,6 +258,7 @@ struct | File_exists path -> Res (bool, Sys.file_exists (p path)) | Is_directory path -> Res (result bool exn, protect Sys.is_directory (p path)) | Remove (path, file_name) -> Res (result unit exn, protect Sys.remove ((p path) / file_name)) + | Rename (old_path, new_path) -> Res (result unit exn, protect (Sys.rename (p old_path)) (p new_path)) | Mkdir (path, new_dir_name) -> Res (result unit exn, protect (Sys.mkdir ((p path) / new_dir_name)) 0o755) | Rmdir (path, delete_dir_name) -> @@ -258,18 +268,6 @@ struct | 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 rec path_prefixes path = match path with - | [] -> [] - | [_] -> [] - | n::ns -> [n]::(List.map (fun p -> n::p) (path_prefixes ns)) - let postcond c (fs: filesys) res = match c, res with | File_exists path, Res ((Bool,_),b) -> b = mem_model fs path @@ -281,19 +279,34 @@ struct | Some File -> b = false | None -> false) | Error (Sys_error s) -> - (s = (p path) ^ ": No such file or directory" && find_opt_model fs path = None) || - (s = p path ^ ": Not a directory" && List.exists (fun pref -> Some File = find_opt_model fs pref) (path_prefixes path)) + (s = (p path) ^ ": No such file or directory" && not (mem_model fs path)) || + (s = p path ^ ": Not a directory" && List.exists (fun pref -> not (path_is_a_dir fs pref)) (path_prefixes path)) | _ -> false) | Remove (path, file_name), Res ((Result (Unit,Exn),_), res) -> let complete_path = (path @ [file_name]) in (match res with | Ok () -> mem_model fs complete_path && path_is_a_dir fs path && not (path_is_a_dir fs complete_path) | Error (Sys_error s) -> - (s = (p complete_path) ^ ": No such file or directory" && find_opt_model fs complete_path = None) || + (s = (p complete_path) ^ ": No such file or directory" && not (mem_model fs complete_path)) || (s = (p complete_path) ^ ": Is a directory" && path_is_a_dir fs complete_path) || (s = (p complete_path) ^ ": Not a directory" && not (path_is_a_dir fs path)) | Error _ -> false ) + | Rename (old_path, new_path), Res ((Result (Unit,Exn),_), res) -> + (match res with + | Ok () -> mem_model fs old_path + | Error (Sys_error s) -> + (s = "No such file or directory" && + not (mem_model fs old_path) || List.exists (fun pref -> not (path_is_a_dir fs pref)) (path_prefixes new_path)) || + (s = "Invalid argument" && is_true_prefix old_path new_path) || + (s = "Not a directory" && + List.exists (path_is_a_file fs) (path_prefixes old_path) || + List.exists (path_is_a_file fs) (path_prefixes new_path) || + path_is_a_dir fs old_path && mem_model fs new_path && not (path_is_a_dir fs new_path)) || + (s = "Is a directory" && path_is_a_dir fs new_path) || + (s = "Directory not empty" && + is_true_prefix new_path old_path || (path_is_a_dir fs new_path && not (readdir_model fs new_path = Some []))) + | Error _ -> false) | Mkdir (path, new_dir_name), Res ((Result (Unit,Exn),_), res) -> let complete_path = (path @ [new_dir_name]) in (match res with From d0a080442a63a7a132d13823a8fabff697e2f92b Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 2 Mar 2023 08:16:50 +0100 Subject: [PATCH 04/27] Fix Sys.remove on directory on macOS --- src/sys/stm_tests.ml | 1 + 1 file changed, 1 insertion(+) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index a7d86f47e..0579fb4ab 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -289,6 +289,7 @@ struct | Error (Sys_error s) -> (s = (p complete_path) ^ ": No such file or directory" && not (mem_model fs complete_path)) || (s = (p complete_path) ^ ": Is a directory" && path_is_a_dir fs complete_path) || + (s = (p complete_path) ^ ": Operation not permitted" && path_is_a_dir fs complete_path) || (s = (p complete_path) ^ ": Not a directory" && not (path_is_a_dir fs path)) | Error _ -> false ) From afc8dcd917ab90bbb56f52fc9e993b3edc0c6892 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Thu, 2 Mar 2023 08:20:59 +0100 Subject: [PATCH 05/27] Fix Sys.remove on directory on Windows --- src/sys/stm_tests.ml | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 0579fb4ab..b3e834f0e 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -288,8 +288,9 @@ struct | Ok () -> mem_model fs complete_path && path_is_a_dir fs path && not (path_is_a_dir fs complete_path) | Error (Sys_error s) -> (s = (p complete_path) ^ ": No such file or directory" && not (mem_model fs complete_path)) || - (s = (p complete_path) ^ ": Is a directory" && path_is_a_dir fs complete_path) || - (s = (p complete_path) ^ ": Operation not permitted" && path_is_a_dir fs complete_path) || + (s = (p complete_path) ^ ": Is a directory" && path_is_a_dir fs complete_path) || (*Linux*) + (s = (p complete_path) ^ ": Operation not permitted" && path_is_a_dir fs complete_path) || (*macOS*) + (s = (p complete_path) ^ ": Permission denied" && path_is_a_dir fs complete_path) || (*Win*) (s = (p complete_path) ^ ": Not a directory" && not (path_is_a_dir fs path)) | Error _ -> false ) From b46493f4894d354a422c4896c9903bae7989b31b Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 24 May 2023 12:05:30 +0200 Subject: [PATCH 06/27] Collect _model functions in a Model module --- src/sys/stm_tests.ml | 229 ++++++++++++++++++++++--------------------- 1 file changed, 116 insertions(+), 113 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index b3e834f0e..22955a91f 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -99,30 +99,96 @@ struct 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 + module Model = + struct + let rec find_opt 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 fs tl)) + + let mem fs path = find_opt fs path <> None + + (* generic removal function *) + let rec remove fs path file_name = + match fs with + | File -> fs + | Directory d -> + (match path with + | [] -> + (match Map_names.find_opt file_name d.fs_map with + | None + | Some _ -> Directory { fs_map = Map_names.remove file_name d.fs_map }) + | dir::dirs -> + Directory + { fs_map = Map_names.update dir (function + | None -> None + | Some File -> Some File + | Some (Directory _ as d') -> Some (remove d' dirs file_name)) d.fs_map + }) + + let readdir fs path = + match find_opt 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 [])) + + (* generic insertion function *) + let rec insert fs path new_file_name sub_tree = + match fs with + | File -> fs + | Directory d -> + (match path with + | [] -> + Directory {fs_map = Map_names.add new_file_name sub_tree 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 = insert sub_fs tl_path new_file_name sub_tree in + if nfs = sub_fs + then fs + else Directory {fs_map = update_map_name d.fs_map next_in_path nfs})) + + let separate_path path = + match List.rev path with + | [] -> None + | name::rev_path -> Some (List.rev rev_path, name) + + let rename fs old_path new_path = + match separate_path old_path, separate_path new_path with + | None, _ + | _, None -> fs + | Some (old_path_pref, old_name), Some (new_path_pref, new_name) -> + (match find_opt fs new_path_pref with + | None + | Some File -> fs + | Some (Directory _) -> + (match find_opt fs old_path with + | None -> fs + | Some sub_fs -> + let fs' = remove fs old_path_pref old_name in + insert fs' new_path_pref new_name sub_fs)) + end let path_is_a_dir fs path = - match find_opt_model fs path with + match Model.find_opt fs path with | None | Some File -> false | Some (Directory _) -> true let path_is_a_file fs path = - match find_opt_model fs path with + match Model.find_opt fs path with | None | Some (Directory _) -> false | Some File -> true @@ -132,107 +198,44 @@ struct | [_] -> [] | n::ns -> [n]::(List.map (fun p -> n::p) (path_prefixes ns)) - let separate_path path = - match List.rev path with - | [] -> None - | name::rev_path -> Some (List.rev rev_path, name) - let rec is_true_prefix path1 path2 = match path1, path2 with | [], [] -> false | [], _::_ -> true | _::_, [] -> false | n1::p1, n2::p2 -> n1=n2 && is_true_prefix p1 p2 - (* generic removal function *) - let rec remove_model fs path file_name = - match fs with - | File -> fs - | Directory d -> - (match path with - | [] -> - (match Map_names.find_opt file_name d.fs_map with - | None - | Some _ -> Directory { fs_map = Map_names.remove file_name d.fs_map }) - | dir::dirs -> - Directory - { fs_map = Map_names.update dir (function - | None -> None - | Some File -> Some File - | Some (Directory _ as d') -> Some (remove_model d' dirs file_name)) d.fs_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 [])) - - (* generic insertion function *) - let rec insert_model fs path new_file_name sub_tree = - match fs with - | File -> fs - | Directory d -> - (match path with - | [] -> - Directory {fs_map = Map_names.add new_file_name sub_tree 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 = insert_model sub_fs tl_path new_file_name sub_tree in - if nfs = sub_fs - then fs - else Directory {fs_map = update_map_name d.fs_map next_in_path nfs})) - - let rename_model fs old_path new_path = - match separate_path old_path, separate_path new_path with - | None, _ - | _, None -> fs - | Some (old_path_pref, old_name), Some (new_path_pref, new_name) -> - (match find_opt_model fs new_path_pref with - | None - | Some File -> fs - | Some (Directory _) -> - (match find_opt_model fs old_path with - | None -> fs - | Some sub_fs -> - let fs' = remove_model fs old_path_pref old_name in - insert_model fs' new_path_pref new_name sub_fs)) - 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]) + if Model.mem fs (path @ [new_dir_name]) then fs - else insert_model fs path new_dir_name (Directory {fs_map = Map_names.empty}) + else Model.insert fs path new_dir_name (Directory {fs_map = Map_names.empty}) | Remove (path, file_name) -> - if find_opt_model fs (path @ [file_name]) = Some File - then remove_model fs path file_name + if Model.find_opt fs (path @ [file_name]) = Some File + then Model.remove fs path file_name else fs | Rename (old_path, new_path) -> if is_true_prefix old_path new_path then fs else - (match find_opt_model fs old_path with + (match Model.find_opt fs old_path with | None -> fs | Some File -> - if (not (mem_model fs new_path) || path_is_a_file fs new_path) then rename_model fs old_path new_path else fs + if (not (Model.mem fs new_path) || path_is_a_file fs new_path) then Model.rename fs old_path new_path else fs | Some (Directory _) -> - if (not (mem_model fs new_path) || readdir_model fs new_path = Some []) then rename_model fs old_path new_path else fs) + if (not (Model.mem fs new_path) || Model.readdir fs new_path = Some []) then Model.rename fs old_path new_path else fs) | Is_directory _path -> fs | Rmdir (path,delete_dir_name) -> let complete_path = path @ [delete_dir_name] in - if mem_model fs complete_path && readdir_model fs complete_path = Some [] - then remove_model fs path delete_dir_name + if Model.mem fs complete_path && Model.readdir fs complete_path = Some [] + then Model.remove fs path delete_dir_name else fs | Readdir _path -> fs | Mkfile (path, new_file_name) -> - if mem_model fs (path @ [new_file_name]) + if Model.mem fs (path @ [new_file_name]) then fs - else insert_model fs path new_file_name File + else Model.insert fs path new_file_name File let init_sut () = try Sys.mkdir sandbox_root 0o700 @@ -270,24 +273,24 @@ struct let postcond c (fs: filesys) res = match c, res with - | File_exists path, Res ((Bool,_),b) -> b = mem_model fs path + | File_exists path, Res ((Bool,_),b) -> b = Model.mem fs path | Is_directory path, Res ((Result (Bool,Exn),_),res) -> (match res with | Ok b -> - (match find_opt_model fs path with + (match Model.find_opt fs path with | Some (Directory _) -> b = true | Some File -> b = false | None -> false) | Error (Sys_error s) -> - (s = (p path) ^ ": No such file or directory" && not (mem_model fs path)) || + (s = (p path) ^ ": No such file or directory" && not (Model.mem fs path)) || (s = p path ^ ": Not a directory" && List.exists (fun pref -> not (path_is_a_dir fs pref)) (path_prefixes path)) | _ -> false) | Remove (path, file_name), Res ((Result (Unit,Exn),_), res) -> let complete_path = (path @ [file_name]) in (match res with - | Ok () -> mem_model fs complete_path && path_is_a_dir fs path && not (path_is_a_dir fs complete_path) + | Ok () -> Model.mem fs complete_path && path_is_a_dir fs path && not (path_is_a_dir fs complete_path) | Error (Sys_error s) -> - (s = (p complete_path) ^ ": No such file or directory" && not (mem_model fs complete_path)) || + (s = (p complete_path) ^ ": No such file or directory" && not (Model.mem fs complete_path)) || (s = (p complete_path) ^ ": Is a directory" && path_is_a_dir fs complete_path) || (*Linux*) (s = (p complete_path) ^ ": Operation not permitted" && path_is_a_dir fs complete_path) || (*macOS*) (s = (p complete_path) ^ ": Permission denied" && path_is_a_dir fs complete_path) || (*Win*) @@ -296,18 +299,18 @@ struct ) | Rename (old_path, new_path), Res ((Result (Unit,Exn),_), res) -> (match res with - | Ok () -> mem_model fs old_path + | Ok () -> Model.mem fs old_path | Error (Sys_error s) -> (s = "No such file or directory" && - not (mem_model fs old_path) || List.exists (fun pref -> not (path_is_a_dir fs pref)) (path_prefixes new_path)) || + not (Model.mem fs old_path) || List.exists (fun pref -> not (path_is_a_dir fs pref)) (path_prefixes new_path)) || (s = "Invalid argument" && is_true_prefix old_path new_path) || (s = "Not a directory" && List.exists (path_is_a_file fs) (path_prefixes old_path) || List.exists (path_is_a_file fs) (path_prefixes new_path) || - path_is_a_dir fs old_path && mem_model fs new_path && not (path_is_a_dir fs new_path)) || + path_is_a_dir fs old_path && Model.mem fs new_path && not (path_is_a_dir fs new_path)) || (s = "Is a directory" && path_is_a_dir fs new_path) || (s = "Directory not empty" && - is_true_prefix new_path old_path || (path_is_a_dir fs new_path && not (readdir_model fs new_path = Some []))) + is_true_prefix new_path old_path || (path_is_a_dir fs new_path && not (Model.readdir fs new_path = Some []))) | Error _ -> false) | Mkdir (path, new_dir_name), Res ((Result (Unit,Exn),_), res) -> let complete_path = (path @ [new_dir_name]) in @@ -316,14 +319,14 @@ struct (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) ^ ": File exists" && Model.mem fs complete_path) || ((s = (p complete_path) ^ ": No such file or directory" - || s = (p complete_path) ^ ": Invalid argument") && not (mem_model fs path)) || + || s = (p complete_path) ^ ": Invalid argument") && not (Model.mem 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)) + | Ok () -> Model.mem fs path && path_is_a_dir fs path && not (Model.mem fs complete_path)) | Rmdir (path, delete_dir_name), Res ((Result (Unit,Exn),_), res) -> let complete_path = (path @ [delete_dir_name]) in (match res with @@ -331,32 +334,32 @@ struct (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)) || + (s = (p complete_path) ^ ": Directory not empty" && not (Model.readdir fs complete_path = Some [])) || + (s = (p complete_path) ^ ": No such file or directory" && not (Model.mem 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 []) + Model.mem fs complete_path && path_is_a_dir fs complete_path && Model.readdir 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)) || + (s = (p path) ^ ": No such file or directory" && not (Model.mem 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) + if Sys.win32 && not (Model.mem fs path) then array_of_subdir = [||] else - (mem_model fs path && path_is_a_dir fs path && - (match readdir_model fs path with + (Model.mem fs path && path_is_a_dir fs path && + (match Model.readdir fs path with | None -> false | Some l -> List.sort String.compare l @@ -384,11 +387,11 @@ struct | 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) + (Model.mem fs complete_path && match_msgs s msgs_already_exists) + || (not (Model.mem 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)) + | Ok () -> path_is_a_dir fs path && not (Model.mem fs complete_path)) | _,_ -> false end From 9934fe6f62a51c3a8cf95c7cded3087e6137e0ca Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 24 May 2023 12:09:02 +0200 Subject: [PATCH 07/27] Add new pp_cmd cases --- src/sys/stm_tests.ml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 22955a91f..707127738 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -20,6 +20,9 @@ struct let pp_path = pp_list pp_string in match x with | File_exists x -> cst1 pp_path "File_exists" par fmt x + | Is_directory x -> cst1 pp_path "Is_directory" par fmt x + | Remove (x, y) -> cst2 pp_path pp_string "Remove" par fmt x y + | Rename (x, y) -> cst2 pp_path pp_path "Rename" par fmt x y | Mkdir (x, y) -> cst2 pp_path pp_string "Mkdir" par fmt x y | Rmdir (x, y) -> cst2 pp_path pp_string "Rmdir" par fmt x y | Readdir x -> cst1 pp_path "Readdir" par fmt x From 61a9632c409816f6b1b2a862872cd3824255049e Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 24 May 2023 12:25:18 +0200 Subject: [PATCH 08/27] Factor out path_is_an_empty_dir --- src/sys/stm_tests.ml | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 707127738..33726a369 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -190,6 +190,9 @@ struct | Some File -> false | Some (Directory _) -> true + let path_is_an_empty_dir fs path = + Model.readdir fs path = Some [] + let path_is_a_file fs path = match Model.find_opt fs path with | None @@ -227,11 +230,11 @@ struct | Some File -> if (not (Model.mem fs new_path) || path_is_a_file fs new_path) then Model.rename fs old_path new_path else fs | Some (Directory _) -> - if (not (Model.mem fs new_path) || Model.readdir fs new_path = Some []) then Model.rename fs old_path new_path else fs) + if (not (Model.mem fs new_path) || path_is_an_empty_dir fs new_path) then Model.rename fs old_path new_path else fs) | Is_directory _path -> fs | Rmdir (path,delete_dir_name) -> let complete_path = path @ [delete_dir_name] in - if Model.mem fs complete_path && Model.readdir fs complete_path = Some [] + if Model.mem fs complete_path && path_is_an_empty_dir fs complete_path then Model.remove fs path delete_dir_name else fs | Readdir _path -> fs @@ -313,7 +316,7 @@ struct path_is_a_dir fs old_path && Model.mem fs new_path && not (path_is_a_dir fs new_path)) || (s = "Is a directory" && path_is_a_dir fs new_path) || (s = "Directory not empty" && - is_true_prefix new_path old_path || (path_is_a_dir fs new_path && not (Model.readdir fs new_path = Some []))) + is_true_prefix new_path old_path || (path_is_a_dir fs new_path && not (path_is_an_empty_dir fs new_path))) | Error _ -> false) | Mkdir (path, new_dir_name), Res ((Result (Unit,Exn),_), res) -> let complete_path = (path @ [new_dir_name]) in @@ -337,14 +340,14 @@ struct (match err with | Sys_error s -> (s = (p complete_path) ^ ": Permission denied") || - (s = (p complete_path) ^ ": Directory not empty" && not (Model.readdir fs complete_path = Some [])) || + (s = (p complete_path) ^ ": Directory not empty" && not (path_is_an_empty_dir fs complete_path)) || (s = (p complete_path) ^ ": No such file or directory" && not (Model.mem 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 () -> - Model.mem fs complete_path && path_is_a_dir fs complete_path && Model.readdir fs complete_path = Some []) + Model.mem fs complete_path && path_is_a_dir fs complete_path && path_is_an_empty_dir fs complete_path) | Readdir path, Res ((Result (Array String,Exn),_), res) -> (match res with | Error err -> From 7f45b8325cfaad988c1f67c1dc7e839050231e9c Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 24 May 2023 12:32:57 +0200 Subject: [PATCH 09/27] Move Model module up front --- src/sys/stm_tests.ml | 181 ++++++++++++++++++++++--------------------- 1 file changed, 91 insertions(+), 90 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 33726a369..d8af90aef 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -1,8 +1,99 @@ open QCheck open STM +module Model = +struct + module Map_names = Map.Make (String) + + type filesys = + | Directory of {fs_map: filesys Map_names.t} + | File + + let rec find_opt 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 fs tl)) + + let mem fs path = find_opt fs path <> None + + (* generic removal function *) + let rec remove fs path file_name = + match fs with + | File -> fs + | Directory d -> + (match path with + | [] -> + (match Map_names.find_opt file_name d.fs_map with + | None + | Some _ -> Directory { fs_map = Map_names.remove file_name d.fs_map }) + | dir::dirs -> + Directory + { fs_map = Map_names.update dir (function + | None -> None + | Some File -> Some File + | Some (Directory _ as d') -> Some (remove d' dirs file_name)) d.fs_map + }) + + let readdir fs path = + match find_opt 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 update_map_name map_name k v = Map_names.update k (fun _ -> Some v) map_name + + (* generic insertion function *) + let rec insert fs path new_file_name sub_tree = + match fs with + | File -> fs + | Directory d -> + (match path with + | [] -> + Directory {fs_map = Map_names.add new_file_name sub_tree 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 = insert sub_fs tl_path new_file_name sub_tree in + if nfs = sub_fs + then fs + else Directory {fs_map = update_map_name d.fs_map next_in_path nfs})) + + let separate_path path = + match List.rev path with + | [] -> None + | name::rev_path -> Some (List.rev rev_path, name) + + let rename fs old_path new_path = + match separate_path old_path, separate_path new_path with + | None, _ + | _, None -> fs + | Some (old_path_pref, old_name), Some (new_path_pref, new_name) -> + (match find_opt fs new_path_pref with + | None + | Some File -> fs + | Some (Directory _) -> + (match find_opt fs old_path with + | None -> fs + | Some sub_fs -> + let fs' = remove fs old_path_pref old_name in + insert fs' new_path_pref new_name sub_fs)) +end + module SConf = struct + include Model type path = string list type cmd = @@ -30,20 +121,12 @@ struct let show_cmd = Util.Pp.to_show pp_cmd - 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 @@ -102,88 +185,6 @@ struct let init_state = Directory {fs_map = Map_names.empty} - module Model = - struct - let rec find_opt 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 fs tl)) - - let mem fs path = find_opt fs path <> None - - (* generic removal function *) - let rec remove fs path file_name = - match fs with - | File -> fs - | Directory d -> - (match path with - | [] -> - (match Map_names.find_opt file_name d.fs_map with - | None - | Some _ -> Directory { fs_map = Map_names.remove file_name d.fs_map }) - | dir::dirs -> - Directory - { fs_map = Map_names.update dir (function - | None -> None - | Some File -> Some File - | Some (Directory _ as d') -> Some (remove d' dirs file_name)) d.fs_map - }) - - let readdir fs path = - match find_opt 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 [])) - - (* generic insertion function *) - let rec insert fs path new_file_name sub_tree = - match fs with - | File -> fs - | Directory d -> - (match path with - | [] -> - Directory {fs_map = Map_names.add new_file_name sub_tree 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 = insert sub_fs tl_path new_file_name sub_tree in - if nfs = sub_fs - then fs - else Directory {fs_map = update_map_name d.fs_map next_in_path nfs})) - - let separate_path path = - match List.rev path with - | [] -> None - | name::rev_path -> Some (List.rev rev_path, name) - - let rename fs old_path new_path = - match separate_path old_path, separate_path new_path with - | None, _ - | _, None -> fs - | Some (old_path_pref, old_name), Some (new_path_pref, new_name) -> - (match find_opt fs new_path_pref with - | None - | Some File -> fs - | Some (Directory _) -> - (match find_opt fs old_path with - | None -> fs - | Some sub_fs -> - let fs' = remove fs old_path_pref old_name in - insert fs' new_path_pref new_name sub_fs)) - end - let path_is_a_dir fs path = match Model.find_opt fs path with | None From 0baa1d81c78fa12ec53fcc73f775d13f4343eda0 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 24 May 2023 12:43:00 +0200 Subject: [PATCH 10/27] Factor out empty_dir --- src/sys/stm_tests.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index d8af90aef..b2e97e679 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -9,6 +9,8 @@ struct | Directory of {fs_map: filesys Map_names.t} | File + let empty_dir = Directory {fs_map = Map_names.empty} + let rec find_opt fs path = match fs with | File -> @@ -183,7 +185,7 @@ struct let sandbox_root = "_sandbox" - let init_state = Directory {fs_map = Map_names.empty} + let init_state = Model.empty_dir let path_is_a_dir fs path = match Model.find_opt fs path with @@ -217,7 +219,7 @@ struct | Mkdir (path, new_dir_name) -> if Model.mem fs (path @ [new_dir_name]) then fs - else Model.insert fs path new_dir_name (Directory {fs_map = Map_names.empty}) + else Model.insert fs path new_dir_name Model.empty_dir | Remove (path, file_name) -> if Model.find_opt fs (path @ [file_name]) = Some File then Model.remove fs path file_name From b794acf707eabebdf63bd4c3a70d9c13a7e2c322 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 24 May 2023 13:05:41 +0200 Subject: [PATCH 11/27] Factor out match_err --- src/sys/stm_tests.ml | 49 ++++++++++++++++++++++---------------------- 1 file changed, 25 insertions(+), 24 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index b2e97e679..7dfd0473a 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -280,6 +280,8 @@ struct | Mkfile (path, new_file_name) -> Res (result unit exn, protect mkfile (p path / new_file_name)) + let match_err err path msg = err = (p path) ^ ": " ^ msg + let postcond c (fs: filesys) res = match c, res with | File_exists path, Res ((Bool,_),b) -> b = Model.mem fs path @@ -291,19 +293,19 @@ struct | Some File -> b = false | None -> false) | Error (Sys_error s) -> - (s = (p path) ^ ": No such file or directory" && not (Model.mem fs path)) || - (s = p path ^ ": Not a directory" && List.exists (fun pref -> not (path_is_a_dir fs pref)) (path_prefixes path)) + (match_err s path "No such file or directory" && not (Model.mem fs path)) || + (match_err s path "Not a directory" && List.exists (fun pref -> not (path_is_a_dir fs pref)) (path_prefixes path)) | _ -> false) | Remove (path, file_name), Res ((Result (Unit,Exn),_), res) -> let complete_path = (path @ [file_name]) in (match res with | Ok () -> Model.mem fs complete_path && path_is_a_dir fs path && not (path_is_a_dir fs complete_path) | Error (Sys_error s) -> - (s = (p complete_path) ^ ": No such file or directory" && not (Model.mem fs complete_path)) || - (s = (p complete_path) ^ ": Is a directory" && path_is_a_dir fs complete_path) || (*Linux*) - (s = (p complete_path) ^ ": Operation not permitted" && path_is_a_dir fs complete_path) || (*macOS*) - (s = (p complete_path) ^ ": Permission denied" && path_is_a_dir fs complete_path) || (*Win*) - (s = (p complete_path) ^ ": Not a directory" && not (path_is_a_dir fs path)) + (match_err s complete_path "No such file or directory" && not (Model.mem fs complete_path)) || + (match_err s complete_path "Is a directory" && path_is_a_dir fs complete_path) || (*Linux*) + (match_err s complete_path "Operation not permitted" && path_is_a_dir fs complete_path) || (*macOS*) + (match_err s complete_path "Permission denied" && path_is_a_dir fs complete_path) || (*Win*) + (match_err s complete_path "Not a directory" && not (path_is_a_dir fs path)) | Error _ -> false ) | Rename (old_path, new_path), Res ((Result (Unit,Exn),_), res) -> @@ -327,13 +329,13 @@ struct | Error err -> (match err with | Sys_error s -> - (s = (p complete_path) ^ ": Permission denied") || - (s = (p complete_path) ^ ": File exists" && Model.mem fs complete_path) || - ((s = (p complete_path) ^ ": No such file or directory" - || s = (p complete_path) ^ ": Invalid argument") && not (Model.mem fs path)) || + (match_err s complete_path "Permission denied") || + (match_err s complete_path "File exists" && Model.mem fs complete_path) || + ((match_err s complete_path "No such file or directory" + || match_err s complete_path "Invalid argument") && not (Model.mem 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" + then match_err s complete_path "No such file or directory" + else match_err s complete_path "Not a directory" | _ -> false) | Ok () -> Model.mem fs path && path_is_a_dir fs path && not (Model.mem fs complete_path)) | Rmdir (path, delete_dir_name), Res ((Result (Unit,Exn),_), res) -> @@ -342,12 +344,12 @@ struct | Error err -> (match err with | Sys_error s -> - (s = (p complete_path) ^ ": Permission denied") || - (s = (p complete_path) ^ ": Directory not empty" && not (path_is_an_empty_dir fs complete_path)) || - (s = (p complete_path) ^ ": No such file or directory" && not (Model.mem fs complete_path)) || + (match_err s complete_path "Permission denied") || + (match_err s complete_path "Directory not empty" && not (path_is_an_empty_dir fs complete_path)) || + (match_err s complete_path "No such file or directory" && not (Model.mem 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" + then match_err s complete_path "Invalid argument" + else match_err s complete_path "Not a directory" | _ -> false) | Ok () -> Model.mem fs complete_path && path_is_a_dir fs complete_path && path_is_an_empty_dir fs complete_path) @@ -356,11 +358,11 @@ struct | Error err -> (match err with | Sys_error s -> - (s = (p path) ^ ": Permission denied") || - (s = (p path) ^ ": No such file or directory" && not (Model.mem fs path)) || + (match_err s path "Permission denied") || + (match_err s path "No such file or directory" && not (Model.mem 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" + then match_err s path "Invalid argument" + else match_err s path "Not a directory" | _ -> false) | Ok array_of_subdir -> (* Temporary work around for mingW, see https://github.com/ocaml/ocaml/issues/11829 *) @@ -375,8 +377,7 @@ struct = 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_msg err msg = match_err err complete_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 *) From 421b059bc6bac0b5df6f51e52e309bba279b8588 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 24 May 2023 13:50:42 +0200 Subject: [PATCH 12/27] Make error msg matching cases more uniform --- src/sys/stm_tests.ml | 103 +++++++++++++++++++------------------------ 1 file changed, 45 insertions(+), 58 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 7dfd0473a..1e8d6806d 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -280,7 +280,8 @@ struct | Mkfile (path, new_file_name) -> Res (result unit exn, protect mkfile (p path / new_file_name)) - let match_err err path msg = err = (p path) ^ ": " ^ msg + let match_msg err path msg = err = (p path) ^ ": " ^ msg + let match_msgs err path msgs = List.exists (match_msg err path) msgs let postcond c (fs: filesys) res = match c, res with @@ -293,19 +294,20 @@ struct | Some File -> b = false | None -> false) | Error (Sys_error s) -> - (match_err s path "No such file or directory" && not (Model.mem fs path)) || - (match_err s path "Not a directory" && List.exists (fun pref -> not (path_is_a_dir fs pref)) (path_prefixes path)) + (match_msg s path "No such file or directory" && not (Model.mem fs path)) || + (match_msg s path "Not a directory" && + List.exists (fun pref -> not (path_is_a_dir fs pref)) (path_prefixes path)) | _ -> false) | Remove (path, file_name), Res ((Result (Unit,Exn),_), res) -> - let complete_path = (path @ [file_name]) in + let full_path = (path @ [file_name]) in (match res with - | Ok () -> Model.mem fs complete_path && path_is_a_dir fs path && not (path_is_a_dir fs complete_path) + | Ok () -> Model.mem fs full_path && path_is_a_dir fs path && not (path_is_a_dir fs full_path) | Error (Sys_error s) -> - (match_err s complete_path "No such file or directory" && not (Model.mem fs complete_path)) || - (match_err s complete_path "Is a directory" && path_is_a_dir fs complete_path) || (*Linux*) - (match_err s complete_path "Operation not permitted" && path_is_a_dir fs complete_path) || (*macOS*) - (match_err s complete_path "Permission denied" && path_is_a_dir fs complete_path) || (*Win*) - (match_err s complete_path "Not a directory" && not (path_is_a_dir fs path)) + (match_msg s full_path "No such file or directory" && not (Model.mem fs full_path)) || + (match_msgs s full_path ["Is a directory"; (*Linux*) + "Operation not permitted"; (*macOS*) + "Permission denied"(*Win*)] && path_is_a_dir fs full_path) || + (match_msg s full_path "Not a directory" && not (path_is_a_dir fs path)) | Error _ -> false ) | Rename (old_path, new_path), Res ((Result (Unit,Exn),_), res) -> @@ -324,45 +326,42 @@ struct is_true_prefix new_path old_path || (path_is_a_dir fs new_path && not (path_is_an_empty_dir fs new_path))) | Error _ -> false) | Mkdir (path, new_dir_name), Res ((Result (Unit,Exn),_), res) -> - let complete_path = (path @ [new_dir_name]) in + let full_path = (path @ [new_dir_name]) in (match res with | Error err -> (match err with | Sys_error s -> - (match_err s complete_path "Permission denied") || - (match_err s complete_path "File exists" && Model.mem fs complete_path) || - ((match_err s complete_path "No such file or directory" - || match_err s complete_path "Invalid argument") && not (Model.mem fs path)) || - if Sys.win32 && not (path_is_a_dir fs complete_path) - then match_err s complete_path "No such file or directory" - else match_err s complete_path "Not a directory" + (match_msg s full_path "Permission denied") || + (match_msg s full_path "File exists" && Model.mem fs full_path) || + (match_msgs s full_path ["No such file or directory"; + "Invalid argument"] && not (Model.mem fs path)) || + (match_msgs s full_path ["Not a directory"; + "No such file or directory"(*win32*)] && not (path_is_a_dir fs full_path)) | _ -> false) - | Ok () -> Model.mem fs path && path_is_a_dir fs path && not (Model.mem fs complete_path)) + | Ok () -> Model.mem fs path && path_is_a_dir fs path && not (Model.mem fs full_path)) | Rmdir (path, delete_dir_name), Res ((Result (Unit,Exn),_), res) -> - let complete_path = (path @ [delete_dir_name]) in + let full_path = (path @ [delete_dir_name]) in (match res with | Error err -> (match err with | Sys_error s -> - (match_err s complete_path "Permission denied") || - (match_err s complete_path "Directory not empty" && not (path_is_an_empty_dir fs complete_path)) || - (match_err s complete_path "No such file or directory" && not (Model.mem fs complete_path)) || - if Sys.win32 && not (path_is_a_dir fs complete_path) (* if not a directory *) - then match_err s complete_path "Invalid argument" - else match_err s complete_path "Not a directory" + (match_msg s full_path "Permission denied") || + (match_msg s full_path "Directory not empty" && not (path_is_an_empty_dir fs full_path)) || + (match_msg s full_path "No such file or directory" && not (Model.mem fs full_path)) || + (match_msgs s full_path ["Not a directory"; + "Invalid argument"(*win32*)] && not (path_is_a_dir fs full_path)) | _ -> false) | Ok () -> - Model.mem fs complete_path && path_is_a_dir fs complete_path && path_is_an_empty_dir fs complete_path) + Model.mem fs full_path && path_is_a_dir fs full_path && path_is_an_empty_dir fs full_path) | Readdir path, Res ((Result (Array String,Exn),_), res) -> (match res with | Error err -> (match err with | Sys_error s -> - (match_err s path "Permission denied") || - (match_err s path "No such file or directory" && not (Model.mem fs path)) || - if Sys.win32 && not (path_is_a_dir fs path) (* if not a directory *) - then match_err s path "Invalid argument" - else match_err s path "Not a directory" + (match_msg s path "Permission denied") || + (match_msg s path "No such file or directory" && not (Model.mem fs path)) || + (match_msgs s path ["Not a directory"; + "Invalid argument"(*win32*)] && not (path_is_a_dir fs path)) | _ -> false) | Ok array_of_subdir -> (* Temporary work around for mingW, see https://github.com/ocaml/ocaml/issues/11829 *) @@ -370,38 +369,26 @@ struct then array_of_subdir = [||] else (Model.mem fs path && path_is_a_dir fs path && - (match Model.readdir fs path with - | None -> false - | Some l -> - List.sort String.compare l - = List.sort String.compare (Array.to_list array_of_subdir)))) + (match Model.readdir 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 match_msg err msg = match_err err complete_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 - | "Cygwin" - | "Unix" -> "Not a directory" - | "Win32" -> "No such file or directory" - | v -> failwith ("Sys tests not working with " ^ v) - in + let full_path = path @ [ new_file_name ] in match res with | Error err -> ( match err with | Sys_error s -> - (Model.mem fs complete_path && match_msgs s msgs_already_exists) - || (not (Model.mem fs path) && match_msgs s msgs_non_existent_dir) - || (not (path_is_a_dir fs path) && match_msg s msg_path_not_dir) + (match_msgs s full_path ["File exists"; + "Permission denied"] && Model.mem fs full_path) || + (match_msgs s full_path ["No such file or directory"; + "Invalid argument"; + "Permission denied"] && not (Model.mem fs path)) || + (match_msgs s full_path ["Not a directory"; + "No such file or directory"] && not (path_is_a_dir fs path)) | _ -> false) - | Ok () -> path_is_a_dir fs path && not (Model.mem fs complete_path)) + | Ok () -> path_is_a_dir fs path && not (Model.mem fs full_path)) | _,_ -> false end From 3c0907cb7907c7c64ea35962272de9b24663fab7 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 24 May 2023 14:00:59 +0200 Subject: [PATCH 13/27] More uniformity: short Ok first, match on Error (Sys_error s) --- src/sys/stm_tests.ml | 105 ++++++++++++++++++++----------------------- 1 file changed, 49 insertions(+), 56 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 1e8d6806d..89effe045 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -285,7 +285,8 @@ struct let postcond c (fs: filesys) res = match c, res with - | File_exists path, Res ((Bool,_),b) -> b = Model.mem fs path + | File_exists path, Res ((Bool,_),b) -> + b = Model.mem fs path | Is_directory path, Res ((Result (Bool,Exn),_),res) -> (match res with | Ok b -> @@ -328,67 +329,59 @@ struct | Mkdir (path, new_dir_name), Res ((Result (Unit,Exn),_), res) -> let full_path = (path @ [new_dir_name]) in (match res with - | Error err -> - (match err with - | Sys_error s -> - (match_msg s full_path "Permission denied") || - (match_msg s full_path "File exists" && Model.mem fs full_path) || - (match_msgs s full_path ["No such file or directory"; - "Invalid argument"] && not (Model.mem fs path)) || - (match_msgs s full_path ["Not a directory"; - "No such file or directory"(*win32*)] && not (path_is_a_dir fs full_path)) - | _ -> false) - | Ok () -> Model.mem fs path && path_is_a_dir fs path && not (Model.mem fs full_path)) + | Ok () -> Model.mem fs path && path_is_a_dir fs path && not (Model.mem fs full_path) + | Error (Sys_error s) -> + (match_msg s full_path "Permission denied") || + (match_msg s full_path "File exists" && Model.mem fs full_path) || + (match_msgs s full_path ["No such file or directory"; + "Invalid argument"] && not (Model.mem fs path)) || + (match_msgs s full_path ["Not a directory"; + "No such file or directory"(*win32*)] && not (path_is_a_dir fs full_path)) + | Error _ -> false) | Rmdir (path, delete_dir_name), Res ((Result (Unit,Exn),_), res) -> let full_path = (path @ [delete_dir_name]) in (match res with - | Error err -> - (match err with - | Sys_error s -> - (match_msg s full_path "Permission denied") || - (match_msg s full_path "Directory not empty" && not (path_is_an_empty_dir fs full_path)) || - (match_msg s full_path "No such file or directory" && not (Model.mem fs full_path)) || - (match_msgs s full_path ["Not a directory"; - "Invalid argument"(*win32*)] && not (path_is_a_dir fs full_path)) - | _ -> false) - | Ok () -> - Model.mem fs full_path && path_is_a_dir fs full_path && path_is_an_empty_dir fs full_path) + | Ok () -> + Model.mem fs full_path && path_is_a_dir fs full_path && path_is_an_empty_dir fs full_path + | Error (Sys_error s) -> + (match_msg s full_path "Permission denied") || + (match_msg s full_path "Directory not empty" && not (path_is_an_empty_dir fs full_path)) || + (match_msg s full_path "No such file or directory" && not (Model.mem fs full_path)) || + (match_msgs s full_path ["Not a directory"; + "Invalid argument"(*win32*)] && not (path_is_a_dir fs full_path)) + | Error _ -> false) | Readdir path, Res ((Result (Array String,Exn),_), res) -> (match res with - | Error err -> - (match err with - | Sys_error s -> - (match_msg s path "Permission denied") || - (match_msg s path "No such file or directory" && not (Model.mem fs path)) || - (match_msgs s path ["Not a directory"; - "Invalid argument"(*win32*)] && not (path_is_a_dir fs path)) - | _ -> false) - | Ok array_of_subdir -> - (* Temporary work around for mingW, see https://github.com/ocaml/ocaml/issues/11829 *) - if Sys.win32 && not (Model.mem fs path) - then array_of_subdir = [||] - else - (Model.mem fs path && path_is_a_dir fs path && - (match Model.readdir 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) -> ( + | Ok array_of_subdir -> + (* Temporary work around for mingW, see https://github.com/ocaml/ocaml/issues/11829 *) + if Sys.win32 && not (Model.mem fs path) + then array_of_subdir = [||] + else + (Model.mem fs path && path_is_a_dir fs path && + (match Model.readdir fs path with + | None -> false + | Some l -> + List.sort String.compare l + = List.sort String.compare (Array.to_list array_of_subdir))) + | Error (Sys_error s) -> + (match_msg s path "Permission denied") || + (match_msg s path "No such file or directory" && not (Model.mem fs path)) || + (match_msgs s path ["Not a directory"; + "Invalid argument"(*win32*)] && not (path_is_a_dir fs path)) + | Error _ -> false) + | Mkfile (path, new_file_name), Res ((Result (Unit,Exn),_),res) -> let full_path = path @ [ new_file_name ] in - match res with - | Error err -> ( - match err with - | Sys_error s -> - (match_msgs s full_path ["File exists"; - "Permission denied"] && Model.mem fs full_path) || - (match_msgs s full_path ["No such file or directory"; - "Invalid argument"; - "Permission denied"] && not (Model.mem fs path)) || - (match_msgs s full_path ["Not a directory"; - "No such file or directory"] && not (path_is_a_dir fs path)) - | _ -> false) - | Ok () -> path_is_a_dir fs path && not (Model.mem fs full_path)) + (match res with + | Ok () -> path_is_a_dir fs path && not (Model.mem fs full_path) + | Error (Sys_error s) -> + (match_msgs s full_path ["File exists"; + "Permission denied"] && Model.mem fs full_path) || + (match_msgs s full_path ["No such file or directory"; + "Invalid argument"; + "Permission denied"] && not (Model.mem fs path)) || + (match_msgs s full_path ["Not a directory"; + "No such file or directory"] && not (path_is_a_dir fs path)) + | Error _ -> false) | _,_ -> false end From 45faf98eb40acf7c1f202b38294979a71e8a2945 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 24 May 2023 15:36:39 +0200 Subject: [PATCH 14/27] Add workarounds for buggy MingW Sys.rename behaviour --- src/sys/stm_tests.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 89effe045..570a0ca1d 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -233,7 +233,11 @@ struct | Some File -> if (not (Model.mem fs new_path) || path_is_a_file fs new_path) then Model.rename fs old_path new_path else fs | Some (Directory _) -> - if (not (Model.mem fs new_path) || path_is_an_empty_dir fs new_path) then Model.rename fs old_path new_path else fs) + (* temporary workaround for dir-to-empty-target-dir https://github.com/ocaml/ocaml/issues/12073 *) + if Sys.win32 && path_is_an_empty_dir fs new_path then fs else + (* temporary workaround for dir-to-file https://github.com/ocaml/ocaml/issues/12073 *) + if (Sys.win32 && path_is_an_empty_dir fs new_path) || + (not (Model.mem fs new_path) || path_is_an_empty_dir fs new_path) then Model.rename fs old_path new_path else fs) | Is_directory _path -> fs | Rmdir (path,delete_dir_name) -> let complete_path = path @ [delete_dir_name] in @@ -313,8 +317,10 @@ struct ) | Rename (old_path, new_path), Res ((Result (Unit,Exn),_), res) -> (match res with - | Ok () -> Model.mem fs old_path + | Ok () -> Model.mem fs old_path (* permits dir-to-file MingW success https://github.com/ocaml/ocaml/issues/12073 *) | Error (Sys_error s) -> + (* temporary workaround for dir-to-empty-target-dir https://github.com/ocaml/ocaml/issues/12073 *) + (s = "Permission denied" && Sys.win32 && path_is_a_dir fs old_path && path_is_an_empty_dir fs new_path) || (s = "No such file or directory" && not (Model.mem fs old_path) || List.exists (fun pref -> not (path_is_a_dir fs pref)) (path_prefixes new_path)) || (s = "Invalid argument" && is_true_prefix old_path new_path) || From c5f8ef3c1d5a28426865b98bcf17831d3b1f0acb Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 24 May 2023 16:12:03 +0200 Subject: [PATCH 15/27] patch dir-to-file on MingW --- src/sys/stm_tests.ml | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 570a0ca1d..4357f23c0 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -236,8 +236,14 @@ struct (* temporary workaround for dir-to-empty-target-dir https://github.com/ocaml/ocaml/issues/12073 *) if Sys.win32 && path_is_an_empty_dir fs new_path then fs else (* temporary workaround for dir-to-file https://github.com/ocaml/ocaml/issues/12073 *) - if (Sys.win32 && path_is_an_empty_dir fs new_path) || - (not (Model.mem fs new_path) || path_is_an_empty_dir fs new_path) then Model.rename fs old_path new_path else fs) + if (Sys.win32 && path_is_file fs new_path) then + (match Model.separate_path new_path in + | None -> fs + | Some (new_path_pref, new_name) -> + let fs = remove fs new_path_pref new_name in + Model.rename fs old_path new_path) + else + if (not (Model.mem fs new_path) || path_is_an_empty_dir fs new_path) then Model.rename fs old_path new_path else fs) | Is_directory _path -> fs | Rmdir (path,delete_dir_name) -> let complete_path = path @ [delete_dir_name] in From b6802e7d2bb9614bbbabe8d78ae3a61cd0db0913 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 24 May 2023 16:21:02 +0200 Subject: [PATCH 16/27] patch file-to-dir Permission denied error on MingW --- src/sys/stm_tests.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 4357f23c0..67b522c3c 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -236,8 +236,8 @@ struct (* temporary workaround for dir-to-empty-target-dir https://github.com/ocaml/ocaml/issues/12073 *) if Sys.win32 && path_is_an_empty_dir fs new_path then fs else (* temporary workaround for dir-to-file https://github.com/ocaml/ocaml/issues/12073 *) - if (Sys.win32 && path_is_file fs new_path) then - (match Model.separate_path new_path in + if (Sys.win32 && path_is_a_file fs new_path) then + (match Model.separate_path new_path with | None -> fs | Some (new_path_pref, new_name) -> let fs = remove fs new_path_pref new_name in @@ -334,7 +334,7 @@ struct List.exists (path_is_a_file fs) (path_prefixes old_path) || List.exists (path_is_a_file fs) (path_prefixes new_path) || path_is_a_dir fs old_path && Model.mem fs new_path && not (path_is_a_dir fs new_path)) || - (s = "Is a directory" && path_is_a_dir fs new_path) || + ((s = "Is a directory" || s = "Permission denied") && path_is_a_dir fs new_path) || (s = "Directory not empty" && is_true_prefix new_path old_path || (path_is_a_dir fs new_path && not (path_is_an_empty_dir fs new_path))) | Error _ -> false) From 6c10d1fc0445ae2ef1201b3d0f7a0cf1ad60963e Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 24 May 2023 16:34:17 +0200 Subject: [PATCH 17/27] patch dir-to-dir Sys.rename MingW regression --- src/sys/stm_tests.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 67b522c3c..a941bc2a2 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -327,6 +327,8 @@ struct | Error (Sys_error s) -> (* temporary workaround for dir-to-empty-target-dir https://github.com/ocaml/ocaml/issues/12073 *) (s = "Permission denied" && Sys.win32 && path_is_a_dir fs old_path && path_is_an_empty_dir fs new_path) || + (* temporary workaround for identity regression renaming under MingW *) + (s = "No such file or directory" && Sys.win32 && old_path = new_path && path_is_an_empty_dir fs new_path) || (s = "No such file or directory" && not (Model.mem fs old_path) || List.exists (fun pref -> not (path_is_a_dir fs pref)) (path_prefixes new_path)) || (s = "Invalid argument" && is_true_prefix old_path new_path) || From e55bf4067d332b0397c5bc87d6995f72a4b8b466 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 24 May 2023 16:46:49 +0200 Subject: [PATCH 18/27] Another different Sys.rename error message --- src/sys/stm_tests.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index a941bc2a2..ad1f45305 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -331,12 +331,12 @@ struct (s = "No such file or directory" && Sys.win32 && old_path = new_path && path_is_an_empty_dir fs new_path) || (s = "No such file or directory" && not (Model.mem fs old_path) || List.exists (fun pref -> not (path_is_a_dir fs pref)) (path_prefixes new_path)) || - (s = "Invalid argument" && is_true_prefix old_path new_path) || + ((s = "Invalid argument" || s = "Permission denied"(*Win32*)) && is_true_prefix old_path new_path) || (s = "Not a directory" && List.exists (path_is_a_file fs) (path_prefixes old_path) || List.exists (path_is_a_file fs) (path_prefixes new_path) || path_is_a_dir fs old_path && Model.mem fs new_path && not (path_is_a_dir fs new_path)) || - ((s = "Is a directory" || s = "Permission denied") && path_is_a_dir fs new_path) || + ((s = "Is a directory" || s = "Permission denied"(*Win32*)) && path_is_a_dir fs new_path) || (s = "Directory not empty" && is_true_prefix new_path old_path || (path_is_a_dir fs new_path && not (path_is_an_empty_dir fs new_path))) | Error _ -> false) From 2999a355580adcf8842a3609a01076a098357596 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Wed, 24 May 2023 17:06:22 +0200 Subject: [PATCH 19/27] Remove unused Permission-denied cases --- src/sys/stm_tests.ml | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index ad1f45305..585832ec8 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -345,7 +345,6 @@ struct (match res with | Ok () -> Model.mem fs path && path_is_a_dir fs path && not (Model.mem fs full_path) | Error (Sys_error s) -> - (match_msg s full_path "Permission denied") || (match_msg s full_path "File exists" && Model.mem fs full_path) || (match_msgs s full_path ["No such file or directory"; "Invalid argument"] && not (Model.mem fs path)) || @@ -358,7 +357,6 @@ struct | Ok () -> Model.mem fs full_path && path_is_a_dir fs full_path && path_is_an_empty_dir fs full_path | Error (Sys_error s) -> - (match_msg s full_path "Permission denied") || (match_msg s full_path "Directory not empty" && not (path_is_an_empty_dir fs full_path)) || (match_msg s full_path "No such file or directory" && not (Model.mem fs full_path)) || (match_msgs s full_path ["Not a directory"; @@ -378,7 +376,6 @@ struct List.sort String.compare l = List.sort String.compare (Array.to_list array_of_subdir))) | Error (Sys_error s) -> - (match_msg s path "Permission denied") || (match_msg s path "No such file or directory" && not (Model.mem fs path)) || (match_msgs s path ["Not a directory"; "Invalid argument"(*win32*)] && not (path_is_a_dir fs path)) From bd0b7556a4cd94579cff94dacb9f50941bbaf0d4 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 19 Apr 2024 14:52:22 +0200 Subject: [PATCH 20/27] Remove reverse-engineering of error-message conditions --- src/sys/stm_tests.ml | 81 +++++++++++++++----------------------------- 1 file changed, 28 insertions(+), 53 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 585832ec8..c1734089b 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -290,9 +290,6 @@ struct | Mkfile (path, new_file_name) -> Res (result unit exn, protect mkfile (p path / new_file_name)) - let match_msg err path msg = err = (p path) ^ ": " ^ msg - let match_msgs err path msgs = List.exists (match_msg err path) msgs - let postcond c (fs: filesys) res = match c, res with | File_exists path, Res ((Bool,_),b) -> @@ -304,63 +301,49 @@ struct | Some (Directory _) -> b = true | Some File -> b = false | None -> false) - | Error (Sys_error s) -> - (match_msg s path "No such file or directory" && not (Model.mem fs path)) || - (match_msg s path "Not a directory" && - List.exists (fun pref -> not (path_is_a_dir fs pref)) (path_prefixes path)) + | Error (Sys_error _) -> not (Model.mem fs path) | _ -> false) | Remove (path, file_name), Res ((Result (Unit,Exn),_), res) -> - let full_path = (path @ [file_name]) in + let full_path = path @ [file_name] in (match res with | Ok () -> Model.mem fs full_path && path_is_a_dir fs path && not (path_is_a_dir fs full_path) - | Error (Sys_error s) -> - (match_msg s full_path "No such file or directory" && not (Model.mem fs full_path)) || - (match_msgs s full_path ["Is a directory"; (*Linux*) - "Operation not permitted"; (*macOS*) - "Permission denied"(*Win*)] && path_is_a_dir fs full_path) || - (match_msg s full_path "Not a directory" && not (path_is_a_dir fs path)) + | Error (Sys_error _) -> + (not (Model.mem fs full_path)) || path_is_a_dir fs full_path || not (path_is_a_dir fs path) | Error _ -> false ) | Rename (old_path, new_path), Res ((Result (Unit,Exn),_), res) -> (match res with | Ok () -> Model.mem fs old_path (* permits dir-to-file MingW success https://github.com/ocaml/ocaml/issues/12073 *) - | Error (Sys_error s) -> + | Error (Sys_error _) -> (* temporary workaround for dir-to-empty-target-dir https://github.com/ocaml/ocaml/issues/12073 *) - (s = "Permission denied" && Sys.win32 && path_is_a_dir fs old_path && path_is_an_empty_dir fs new_path) || + (Sys.win32 && path_is_a_dir fs old_path && path_is_an_empty_dir fs new_path) || (* temporary workaround for identity regression renaming under MingW *) - (s = "No such file or directory" && Sys.win32 && old_path = new_path && path_is_an_empty_dir fs new_path) || - (s = "No such file or directory" && - not (Model.mem fs old_path) || List.exists (fun pref -> not (path_is_a_dir fs pref)) (path_prefixes new_path)) || - ((s = "Invalid argument" || s = "Permission denied"(*Win32*)) && is_true_prefix old_path new_path) || - (s = "Not a directory" && - List.exists (path_is_a_file fs) (path_prefixes old_path) || - List.exists (path_is_a_file fs) (path_prefixes new_path) || - path_is_a_dir fs old_path && Model.mem fs new_path && not (path_is_a_dir fs new_path)) || - ((s = "Is a directory" || s = "Permission denied"(*Win32*)) && path_is_a_dir fs new_path) || - (s = "Directory not empty" && - is_true_prefix new_path old_path || (path_is_a_dir fs new_path && not (path_is_an_empty_dir fs new_path))) + (Sys.win32 && old_path = new_path && path_is_an_empty_dir fs new_path) || + (* general conditions *) + (not (Model.mem fs old_path)) || + is_true_prefix old_path new_path || (* parent-to-child *) + is_true_prefix new_path old_path || (* child-to-parent *) + (path_is_a_file fs old_path && path_is_a_dir fs new_path) || (* file-to-dir *) + (path_is_a_dir fs old_path && path_is_a_file fs new_path) || (* dir-to-file *) + (path_is_a_dir fs new_path && not (path_is_an_empty_dir fs new_path)) || (* to-non-empty-dir *) + List.exists (fun pref -> not (path_is_a_dir fs pref)) (path_prefixes new_path) (* malformed-target-path *) | Error _ -> false) | Mkdir (path, new_dir_name), Res ((Result (Unit,Exn),_), res) -> - let full_path = (path @ [new_dir_name]) in + let full_path = path @ [new_dir_name] in (match res with | Ok () -> Model.mem fs path && path_is_a_dir fs path && not (Model.mem fs full_path) - | Error (Sys_error s) -> - (match_msg s full_path "File exists" && Model.mem fs full_path) || - (match_msgs s full_path ["No such file or directory"; - "Invalid argument"] && not (Model.mem fs path)) || - (match_msgs s full_path ["Not a directory"; - "No such file or directory"(*win32*)] && not (path_is_a_dir fs full_path)) + | Error (Sys_error _) -> + Model.mem fs full_path || (not (Model.mem fs path)) || not (path_is_a_dir fs full_path) | Error _ -> false) | Rmdir (path, delete_dir_name), Res ((Result (Unit,Exn),_), res) -> - let full_path = (path @ [delete_dir_name]) in + let full_path = path @ [delete_dir_name] in (match res with | Ok () -> Model.mem fs full_path && path_is_a_dir fs full_path && path_is_an_empty_dir fs full_path - | Error (Sys_error s) -> - (match_msg s full_path "Directory not empty" && not (path_is_an_empty_dir fs full_path)) || - (match_msg s full_path "No such file or directory" && not (Model.mem fs full_path)) || - (match_msgs s full_path ["Not a directory"; - "Invalid argument"(*win32*)] && not (path_is_a_dir fs full_path)) + | Error (Sys_error _) -> + (not (Model.mem fs full_path)) || + (not (path_is_a_dir fs full_path)) || + (not (path_is_an_empty_dir fs full_path)) | Error _ -> false) | Readdir path, Res ((Result (Array String,Exn),_), res) -> (match res with @@ -375,23 +358,15 @@ struct | Some l -> List.sort String.compare l = List.sort String.compare (Array.to_list array_of_subdir))) - | Error (Sys_error s) -> - (match_msg s path "No such file or directory" && not (Model.mem fs path)) || - (match_msgs s path ["Not a directory"; - "Invalid argument"(*win32*)] && not (path_is_a_dir fs path)) + | Error (Sys_error _) -> + (not (Model.mem fs path)) || (not (path_is_a_dir fs path)) | Error _ -> false) | Mkfile (path, new_file_name), Res ((Result (Unit,Exn),_),res) -> - let full_path = path @ [ new_file_name ] in + let full_path = path @ [new_file_name] in (match res with | Ok () -> path_is_a_dir fs path && not (Model.mem fs full_path) - | Error (Sys_error s) -> - (match_msgs s full_path ["File exists"; - "Permission denied"] && Model.mem fs full_path) || - (match_msgs s full_path ["No such file or directory"; - "Invalid argument"; - "Permission denied"] && not (Model.mem fs path)) || - (match_msgs s full_path ["Not a directory"; - "No such file or directory"] && not (path_is_a_dir fs path)) + | Error (Sys_error _) -> + Model.mem fs full_path || (not (Model.mem fs path)) || (not (path_is_a_dir fs path)) | Error _ -> false) | _,_ -> false end From d2e6d167bfde4be78220ed437100ec8eda2a8a71 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 19 Apr 2024 14:52:53 +0200 Subject: [PATCH 21/27] Remove OPAM workflows --- .github/workflows/opam.yml | 51 -------------------------------------- 1 file changed, 51 deletions(-) delete mode 100644 .github/workflows/opam.yml diff --git a/.github/workflows/opam.yml b/.github/workflows/opam.yml deleted file mode 100644 index ded1b47ca..000000000 --- a/.github/workflows/opam.yml +++ /dev/null @@ -1,51 +0,0 @@ -name: OPAM installation - -concurrency: - group: ${{ github.workflow }}-${{ github.head_ref || github.run_id }} - cancel-in-progress: true - -on: - pull_request: - push: - branches: - - main - workflow_dispatch: - -jobs: - build-and-test: - env: - QCHECK_MSG_INTERVAL: '60' - - strategy: - matrix: - ocaml-compiler: - - 4.12.x - - 4.13.x - - 4.14.x - - 5.0.0 - - 5.1.0 - - 5.2.0 - - ocaml-variants.5.3.0+trunk - - runs-on: ubuntu-latest - - steps: - - name: Checkout code - uses: actions/checkout@v4 - - - name: Install OCaml compiler - uses: ocaml/setup-ocaml@v2 - with: - ocaml-compiler: ${{ matrix.ocaml-compiler }} - opam-depext: false - - - name: Test installation of the OPAM packages - run: | - opam install --with-test ./qcheck-multicoretests-util.opam ./qcheck-lin.opam ./qcheck-stm.opam - - - name: Show configuration - run: | - opam exec -- ocamlc -config - opam config list - opam exec -- dune printenv - opam list --columns=name,installed-version,repository,synopsis-or-target From fc825741fcd474a0f7f47163968b4cd777419d29 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 19 Apr 2024 14:54:43 +0200 Subject: [PATCH 22/27] REMOVE ME: run focused STM Sys tests --- dune | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/dune b/dune index d436452d8..585bbe6d6 100644 --- a/dune +++ b/dune @@ -24,8 +24,8 @@ (name ci) (package multicoretests) (deps - (alias_rec %{env:DUNE_CI_ALIAS=runtest}))) - ; (alias_rec focusedtest))) + ;(alias_rec %{env:DUNE_CI_ALIAS=runtest}) + (alias_rec focusedtest))) ; @focusedtest ; repeat a single test a couple of times @@ -36,7 +36,7 @@ ; To change the test to repeat, change the source of the `copy`: (rule - (copy src/io/lin_tests_domain.exe focusedtest.exe)) + (copy src/sys/stm_tests.exe focusedtest.exe)) (rule (alias focusedtest) @@ -49,7 +49,7 @@ (write-file hoped "") (write-file failed-runs "") (bash - "for i in `seq 20`; do echo Starting $i-th run; if ! ./focusedtest.exe -v ; then echo $i >> failed-runs; fi; done") + "for i in `seq 10`; do echo Starting $i-th run; if ! ./focusedtest.exe -v ; then echo $i >> failed-runs; fi; done") ; edit the previous line to focus on a particular seed (diff failed-runs hoped))))) @@ -64,6 +64,6 @@ (write-file hoped "") (write-file failed-runs "") (run cmd /q /c - "for %G in (1,2,3,4,5,6,7,8,9,10,11,12,13,14,15,16,17,18,19,20) do (echo Starting %G-th run && focusedtest.exe -v || echo %G >> failed-runs)") + "for %G in (1,2,3,4,5,6,7,8,9,10) do (echo Starting %G-th run && focusedtest.exe -v || echo %G >> failed-runs)") ; edit the previous line to focus on a particular seed (diff failed-runs hoped))))) From 93bfa3e879c2e8d64dea4e36d5adcca7b1a905cf Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Mon, 22 Apr 2024 13:52:59 +0200 Subject: [PATCH 23/27] Add and clean-up existing workarounds for MSVC/MinGW Sys issues --- src/sys/stm_tests.ml | 31 ++++++++++++++++++++----------- 1 file changed, 20 insertions(+), 11 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index c1734089b..4e297d0f6 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -213,6 +213,8 @@ struct | _::_, [] -> false | n1::p1, n2::p2 -> n1=n2 && is_true_prefix p1 p2 + let ocaml_version = Sys.(ocaml_release.major,ocaml_release.minor) + let next_state c fs = match c with | File_exists _path -> fs @@ -226,17 +228,24 @@ struct else fs | Rename (old_path, new_path) -> if is_true_prefix old_path new_path - then fs + then (* workaround for parent-to-empty-child-dir *) + (if Sys.win32 && ocaml_version >= (5,1) && path_is_an_empty_dir fs new_path + then + (match Model.separate_path new_path with + | None -> fs + | Some (new_path_pref, new_name) -> + remove fs new_path_pref new_name) + else fs) else (match Model.find_opt fs old_path with | None -> fs | Some File -> if (not (Model.mem fs new_path) || path_is_a_file fs new_path) then Model.rename fs old_path new_path else fs | Some (Directory _) -> - (* temporary workaround for dir-to-empty-target-dir https://github.com/ocaml/ocaml/issues/12073 *) - if Sys.win32 && path_is_an_empty_dir fs new_path then fs else - (* temporary workaround for dir-to-file https://github.com/ocaml/ocaml/issues/12073 *) - if (Sys.win32 && path_is_a_file fs new_path) then + (* workaround for dir-to-empty-target-dir https://github.com/ocaml/ocaml/issues/12073 *) + if Sys.win32 && ocaml_version <= (5,0) && path_is_an_empty_dir fs new_path then fs else + (* workaround for dir-to-file https://github.com/ocaml/ocaml/issues/12073 *) + if (Sys.win32 && ocaml_version <= (5,0) && path_is_a_file fs new_path) then (match Model.separate_path new_path with | None -> fs | Some (new_path_pref, new_name) -> @@ -315,10 +324,10 @@ struct (match res with | Ok () -> Model.mem fs old_path (* permits dir-to-file MingW success https://github.com/ocaml/ocaml/issues/12073 *) | Error (Sys_error _) -> - (* temporary workaround for dir-to-empty-target-dir https://github.com/ocaml/ocaml/issues/12073 *) - (Sys.win32 && path_is_a_dir fs old_path && path_is_an_empty_dir fs new_path) || - (* temporary workaround for identity regression renaming under MingW *) - (Sys.win32 && old_path = new_path && path_is_an_empty_dir fs new_path) || + (* workaround for dir-to-empty-target-dir https://github.com/ocaml/ocaml/issues/12073 *) + (Sys.win32 && ocaml_version <= (5,0) && path_is_a_dir fs old_path && path_is_an_empty_dir fs new_path) || + (* workaround for identity regression renaming under MingW *) + (Sys.win32 && ocaml_version <= (5,0) && old_path = new_path && path_is_an_empty_dir fs new_path) || (* general conditions *) (not (Model.mem fs old_path)) || is_true_prefix old_path new_path || (* parent-to-child *) @@ -348,8 +357,8 @@ struct | Readdir path, Res ((Result (Array String,Exn),_), res) -> (match res with | Ok array_of_subdir -> - (* Temporary work around for mingW, see https://github.com/ocaml/ocaml/issues/11829 *) - if Sys.win32 && not (Model.mem fs path) + (* workaround for non-existing readdir on MinGW https://github.com/ocaml/ocaml/issues/11829 *) + if Sys.win32 && ocaml_version <= (5,0) && not (Model.mem fs path) then array_of_subdir = [||] else (Model.mem fs path && path_is_a_dir fs path && From 7bc5c94b514c682b17ef5a8032e3b04456855ab8 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Mon, 22 Apr 2024 15:42:10 +0200 Subject: [PATCH 24/27] Remove unneeded parenthesis --- src/sys/stm_tests.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 4e297d0f6..0696ec43b 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -245,7 +245,7 @@ struct (* workaround for dir-to-empty-target-dir https://github.com/ocaml/ocaml/issues/12073 *) if Sys.win32 && ocaml_version <= (5,0) && path_is_an_empty_dir fs new_path then fs else (* workaround for dir-to-file https://github.com/ocaml/ocaml/issues/12073 *) - if (Sys.win32 && ocaml_version <= (5,0) && path_is_a_file fs new_path) then + if Sys.win32 && ocaml_version <= (5,0) && path_is_a_file fs new_path then (match Model.separate_path new_path with | None -> fs | Some (new_path_pref, new_name) -> From fe9a5e88218729af16066c3175a0439da0797759 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Mon, 22 Apr 2024 15:44:44 +0200 Subject: [PATCH 25/27] REMOVE ME: enable version test on MinGW 5.0 and 5.1 --- .github/workflows/mingw-500-bytecode.yml | 7 ++++--- .github/workflows/mingw-500.yml | 7 ++++--- .github/workflows/mingw-51x-bytecode.yml | 7 ++++--- .github/workflows/mingw-51x.yml | 7 ++++--- 4 files changed, 16 insertions(+), 12 deletions(-) diff --git a/.github/workflows/mingw-500-bytecode.yml b/.github/workflows/mingw-500-bytecode.yml index d7c2af561..eb2739786 100644 --- a/.github/workflows/mingw-500-bytecode.yml +++ b/.github/workflows/mingw-500-bytecode.yml @@ -1,9 +1,10 @@ name: MinGW bytecode 5.0.0 on: - schedule: - # Every Sunday morning, at 1:11 UTC - - cron: '11 1 * * 0' + pull_request: + push: + branches: + - main workflow_dispatch: jobs: diff --git a/.github/workflows/mingw-500.yml b/.github/workflows/mingw-500.yml index fa4280550..1342a5dd1 100644 --- a/.github/workflows/mingw-500.yml +++ b/.github/workflows/mingw-500.yml @@ -1,9 +1,10 @@ name: MinGW 5.0.0 on: - schedule: - # Every Sunday morning, at 1:11 UTC - - cron: '11 1 * * 0' + pull_request: + push: + branches: + - main workflow_dispatch: jobs: diff --git a/.github/workflows/mingw-51x-bytecode.yml b/.github/workflows/mingw-51x-bytecode.yml index bee386453..596a16b28 100644 --- a/.github/workflows/mingw-51x-bytecode.yml +++ b/.github/workflows/mingw-51x-bytecode.yml @@ -1,9 +1,10 @@ name: MinGW bytecode 5.1 on: - schedule: - # Every Sunday morning, at 2:22 UTC - - cron: '22 2 * * 0' + pull_request: + push: + branches: + - main workflow_dispatch: jobs: diff --git a/.github/workflows/mingw-51x.yml b/.github/workflows/mingw-51x.yml index ba83c6cb8..03638b722 100644 --- a/.github/workflows/mingw-51x.yml +++ b/.github/workflows/mingw-51x.yml @@ -1,9 +1,10 @@ name: MinGW 5.1 on: - schedule: - # Every Sunday morning, at 2:22 UTC - - cron: '22 2 * * 0' + pull_request: + push: + branches: + - main workflow_dispatch: jobs: From 4200c046618352f6ca5419f1937a12289e50deb2 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Tue, 23 Apr 2024 18:11:56 +0200 Subject: [PATCH 26/27] Experiment: make Sys STM test negative across all archs --- src/sys/stm_tests.ml | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 0696ec43b..05b1777ba 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -393,8 +393,6 @@ 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:2500 ~name:"STM Sys test parallel" + Sys_seq.agree_test ~count:1000 ~name:"STM Sys test sequential"; + Sys_dom.neg_agree_test_par ~count:2500 ~name:"STM Sys test parallel" ] From f8dc3b9b8fe2c6dbbc1f8a460c427cb100b83750 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Fri, 3 May 2024 13:18:17 +0200 Subject: [PATCH 27/27] Remove unused bindings, play with weights --- src/sys/stm_tests.ml | 34 +++++++++++++--------------------- 1 file changed, 13 insertions(+), 21 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 05b1777ba..c8cd096d9 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -151,9 +151,9 @@ struct | [] -> Gen.return None | bindings -> Gen.(oneofl bindings >>= fun (n, sub_fs) -> - oneof [ - return (Some ([],n)); - map (function None -> Some ([],n) + frequency [ + 2,return (Some ([],n)); + 3,map (function None -> Some ([],n) | Some (path,name) -> Some (n::path,name)) (gen_existing_pair sub_fs)] ) ) @@ -170,17 +170,17 @@ struct | Some (p,n) -> return (p,n)); ]) - let arb_cmd s = + let arb_cmd s = (* weights 3,3,3 - seed 223753993 *) QCheck.make ~print:show_cmd - Gen.(oneof [ - map (fun path -> File_exists path) (path_gen s); - map (fun path -> Is_directory path) (path_gen s); - map (fun (path,new_dir_name) -> Remove (path, new_dir_name)) (pair_gen s); - map2 (fun old_path new_path -> Rename (old_path, new_path)) (path_gen s) (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); + Gen.(frequency [ + 1,map (fun path -> File_exists path) (path_gen s); + 1,map (fun path -> Is_directory path) (path_gen s); + 1,map (fun (path,new_dir_name) -> Remove (path, new_dir_name)) (pair_gen s); + 3,map2 (fun old_path new_path -> Rename (old_path, new_path)) (path_gen s) (path_gen s); + 3,map (fun (path,new_dir_name) -> Mkdir (path, new_dir_name)) (pair_gen s); + 1,map (fun (path,delete_dir_name) -> Rmdir (path, delete_dir_name)) (pair_gen s); + 3,map (fun path -> Readdir path) (path_gen s); + 1,map (fun (path,new_file_name) -> Mkfile (path, new_file_name)) (pair_gen s); ]) let sandbox_root = "_sandbox" @@ -380,14 +380,6 @@ struct | _,_ -> false end -let run_cmd cmd = - let ic = Unix.open_process_in cmd in - let os = In_channel.input_line ic in - ignore (Unix.close_process_in ic); - os - -let uname_os () = run_cmd "uname -s" - module Sys_seq = STM_sequential.Make(SConf) module Sys_dom = STM_domain.Make(SConf)