From ec4860d9964569e43c5f4a4478a7740b442ef672 Mon Sep 17 00:00:00 2001 From: Lucccyo Date: Thu, 8 Sep 2022 09:17:35 +0200 Subject: [PATCH 01/33] add commands fileexists, mkdir, rmdir, readdir with version 1 of type filesys --- src/sys/dune | 22 ++++ src/sys/stm_tests.ml | 283 +++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 305 insertions(+) create mode 100644 src/sys/dune create mode 100644 src/sys/stm_tests.ml diff --git a/src/sys/dune b/src/sys/dune new file mode 100644 index 000000000..cd0123866 --- /dev/null +++ b/src/sys/dune @@ -0,0 +1,22 @@ +;; Test of the Sys library + +;; this prevents the tests from running on a default build + +(alias + (name default) + (package multicoretests) + (deps stm_tests.exe)) + +(executable + (name stm_tests) + (modules stm_tests) + (libraries STM) + (preprocess + (pps ppx_deriving.show))) + +(rule + (alias runtest) + (package multicoretests) + (deps stm_tests.exe) + (action + (run ./%{deps} --verbose))) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml new file mode 100644 index 000000000..b6aa372ae --- /dev/null +++ b/src/sys/stm_tests.ml @@ -0,0 +1,283 @@ +open QCheck +open STM + +module SConf = +struct + + type cmd = + | File_exists of string list * string + | Mkdir of string list * string * int + | Rmdir of string list * string + | Readdir of string list * string + [@@deriving show { with_path = false }] + + type filesys = + | Directory of { + perm: int; + dir_name: string; + fs_list: filesys list } + | File of { + perm: int; + file_name: string } + [@@deriving show { with_path = false }] + + type state = filesys + + type sut = unit + + let (/) = Filename.concat + + let arb_cmd _s = + let str_gen = Gen.(oneofl ["c"; "e"; "r"]) in + let name_gen = Gen.(oneofl ["aaa" ; "bbb" ; "ccc" ; "ddd" ; "eee"]) in + let path_gen = Gen.map (fun path -> "sandbox_root" :: path) (Gen.list_size (Gen.int_bound 5) name_gen) in + let perm_gen = Gen.(oneofl [0o777]) in + (* let perm_gen = Gen.map3 (fun d1 d2 d3 -> d1*100 + d2*10 + d3*1) (Gen.int_bound 7) (Gen.int_bound 7) (Gen.int_bound 7) in *) + QCheck.make ~print:show_cmd + Gen.(oneof + [ + map2 (fun path name -> File_exists (path, name)) path_gen str_gen; + map3 (fun path dir_name perm -> Mkdir (path, dir_name, perm)) path_gen str_gen perm_gen; + map2 (fun path dir_name -> Rmdir (path, dir_name)) path_gen str_gen; + map2 (fun path dir_name -> Readdir (path, dir_name)) path_gen str_gen; + ]) + + let static_path = Sys.getcwd () + + let init_state = + Directory {perm = 0o777; dir_name = "sandbox_root"; fs_list = []} + + let rec is_perm_ok (fsl: filesys list) path = + match fsl with + | [] -> true + | Directory d :: tl -> (match path with + | [] -> true + | hd_path :: tl_path -> if d.dir_name = hd_path + then if d.perm > 447 + then is_perm_ok d.fs_list tl_path + else false + else is_perm_ok tl path + ) + | File f :: tl -> (match path with + | [] -> true + | hd_path :: _tl_path -> if f.file_name = hd_path + then true + else is_perm_ok tl path + ) + + let rec mem fs path name = + match fs with + | File f -> path = [] && f.file_name = name + | Directory d -> + match path with + | [] -> name = d.dir_name + | hd :: tl -> + if hd = d.dir_name + then List.exists (fun f -> mem f tl name) d.fs_list + else false + + let is_dir_empty = function + | File _f -> false + | Directory d -> d.fs_list = [] + + let is_a_dir = function + | File _f -> false + | Directory _d -> true + + let rec is_path_empty fs path dir_name = + match fs with + | File _f -> false + | Directory d -> + match path with + | [] -> dir_name = d.dir_name && is_dir_empty (Directory d) + | hd :: tl -> + if hd = d.dir_name + then List.exists (fun f -> is_path_empty f tl dir_name) d.fs_list + else false + + let rec is_path_a_dir fs path dir_name = + match fs with + | File _f -> false + | Directory d -> + match path with + | [] -> dir_name = d.dir_name + | hd :: tl -> + if hd = d.dir_name + then List.exists (fun f -> is_path_a_dir f tl dir_name) d.fs_list + else false + + let get_name fs = + match fs with + | File f -> f.file_name + | Directory d -> d.dir_name + + let rec mkdir fs path dir_name perm = + match fs with + | File _f -> fs + | Directory d -> + match path with + | [] -> + if List.exists (fun fs -> get_name fs = dir_name) d.fs_list + then fs + else Directory {d with fs_list = (Directory {perm; dir_name; fs_list = []} :: d.fs_list)} + | hd :: [] -> + if hd = d.dir_name + then ( + if List.exists (fun fs -> get_name fs = dir_name) d.fs_list + then fs + else Directory {d with fs_list = (Directory {perm; dir_name; fs_list = []} :: d.fs_list)}) + else fs + | hd :: tl -> + if hd = d.dir_name + then Directory {d with fs_list = List.map (fun f -> mkdir f tl dir_name perm) d.fs_list} + else fs + + let rec rmdir fs path dir_name = + match fs with + | File _f -> fs + | Directory d -> + match path with + | [] -> + if not (List.exists (fun fs -> get_name fs = dir_name) d.fs_list) || not (is_dir_empty (Directory d)) + then fs + else Directory {d with fs_list = List.filter (fun f -> not (get_name f = dir_name)) d.fs_list} + | hd :: [] -> + if List.exists (fun fs -> get_name fs = dir_name && is_dir_empty fs) d.fs_list + && not (is_dir_empty (Directory d)) + && hd = d.dir_name + then Directory {d with fs_list = List.filter (fun f -> not (get_name f = dir_name)) d.fs_list} + else fs + | hd :: tl -> + if not (hd = d.dir_name) + then fs + else Directory {d with fs_list = List.map (fun f -> rmdir f tl dir_name) d.fs_list} + + let rec find_opt fs path name = + match fs with + | File _f -> None + | Directory d -> + match path with + | [] -> + if d.dir_name = name + then Some (Directory d) + else None + | hd :: tl -> + if d.dir_name = hd + then ( + let path_next = (match tl with | [] -> name | _ :: _ -> List.hd tl) in + let fs_next = List.find_opt ( + fun e -> + match e with + | File _f -> false + | Directory d -> d.dir_name = path_next) d.fs_list in + match fs_next with + | None -> None + | Some fs -> find_opt fs tl name) + else None + + let get_sub_name fs = + match fs with + | File f -> f.file_name + | Directory d -> d.dir_name + + let readdir fs path dir_name = + match find_opt fs path dir_name with + | None -> None + | Some fs -> + match fs with + | File _f -> None + | Directory d -> Some (List.map get_sub_name d.fs_list) + + let next_state c fs = + match c with + | File_exists (_path, _name) -> fs + | Mkdir (path, dir_name, perm) -> + if mem fs path dir_name + then fs + else mkdir fs path dir_name perm + | Rmdir (path, dir_name) -> + if mem fs path dir_name + then rmdir fs path dir_name + else fs + | Readdir (_path, _dir_name) -> fs + + let init_sut () = try Sys.mkdir (static_path / "sandbox_root") 0o777 with Sys_error _ -> () + + let cleanup _ = ignore (Sys.command ("rm -r -d -f " ^ (static_path / "sandbox_root"))) + + let precond _c _s = true + + let run c _file_name = match c with + | File_exists (path, name) -> Res (bool, Sys.file_exists (static_path / (List.fold_left (/) "" path) / name)) + | Mkdir (path, dir_name, perm) -> + Res (result unit exn, protect (Sys.mkdir (static_path / (List.fold_left (/) "" path) / dir_name))perm) + | Rmdir (path, dir_name) -> + Res (result unit exn, protect (Sys.rmdir) (static_path / (List.fold_left (/) "" path) / dir_name)) + | Readdir (path, dir_name) -> + Res (result (array string) exn, protect (Sys.readdir) (static_path / (List.fold_left (/) "" path) / dir_name)) + + let postcond c (fs: filesys) res = + let p path dir_name = static_path / (String.concat "/" path) / dir_name in + match c, res with + | File_exists (path, name), Res ((Bool,_),b) -> b = mem fs path name + | Mkdir (path, dir_name, _perm), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) + when s = (p path dir_name) ^ ": Permission denied" -> + not (is_perm_ok [fs] path) + | Mkdir (path, dir_name, _perm), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) + when s = (p path dir_name) ^ ": File exists" -> + mem fs path dir_name + | Mkdir (path, dir_name, _perm), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) + when s = (p path dir_name) ^ ": No such file or directory" -> + (match path with + | [] -> false + | _hd_path :: _tl_path -> + let rev = List.rev path in + not (mem fs (List.rev (List.tl rev)) (List.hd rev))) + | Mkdir (path, dir_name, _perm), Res ((Result (Unit,Exn),_), Ok ()) -> + let b = ( + match path with + | [] -> true + | _hd_path :: _tl_path -> + let rev = List.rev path in + mem fs (List.rev (List.tl rev)) (List.hd rev)) in + is_perm_ok [fs] path && not (mem fs path dir_name) && b + | Mkdir (_path, _dir_name, _perm), Res ((Result (Unit,Exn),_), _r) -> false + | Rmdir (path, dir_name), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) + when s = (p path dir_name) ^ ": No such file or directory" -> + not (mem fs path dir_name) + | Rmdir (path, dir_name), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) + when s = (p path dir_name) ^ ": Directory not empty" -> + not (is_path_empty fs path dir_name) + | Rmdir (path, dir_name), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) + when s = (p path dir_name) ^ ": Not a directory" -> + not (is_path_a_dir fs path dir_name) + | Rmdir (path, dir_name), Res ((Result (Unit,Exn),_), Ok ()) -> + mem fs path dir_name && is_path_empty fs path dir_name + | Rmdir (_path, _dir_name), Res ((Result (Unit,Exn),_), _r) -> false + | Readdir (path, dir_name), Res ((Result (Array String,Exn),_), Error (Sys_error (s) )) + when s = (p path dir_name) ^ ": No such file or directory" -> + not (mem fs path dir_name) + | Readdir (path, dir_name), Res ((Result (Array String,Exn),_), Error (Sys_error (s) )) + when s = (p path dir_name) ^ ": Not a directory" -> + not (is_path_a_dir fs path dir_name) + | Readdir (path, dir_name), Res ((Result (Array String,Exn),_), r) -> + (match r with + | Error _e -> false + | Ok a -> + let sut = List.sort (fun a b -> -(String.compare a b)) (Array.to_list a) in + (match readdir fs path dir_name with + | None -> false + | Some l -> List.sort (fun a b -> -(String.compare a b)) l = sut ) ) + | _,_ -> false +end + +module SysSTM = STM.Make(SConf) + +;; +Util.set_ci_printing () +;; +QCheck_base_runner.run_tests_main + (let count = 1000 in + [SysSTM.agree_test ~count ~name:"STM Sys test sequential"; + (* SysSTM.neg_agree_test_par ~count ~name:"STM Sys test parallel" *) +]) From 61eb2d73dd54d64cd1d904c6d6cb65362a5b2c2a Mon Sep 17 00:00:00 2001 From: Lucccyo Date: Thu, 3 Nov 2022 14:16:20 +0100 Subject: [PATCH 02/33] working version 2 of type filesys --- src/sys/stm_tests.ml | 400 ++++++++++++++++++++----------------------- 1 file changed, 190 insertions(+), 210 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index b6aa372ae..f6b954141 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -5,21 +5,17 @@ module SConf = struct type cmd = - | File_exists of string list * string + | File_exists of string list | Mkdir of string list * string * int - | Rmdir of string list * string - | Readdir of string list * string + | Rmdir of string list * string + | Readdir of string list [@@deriving show { with_path = false }] + module Map_names = Map.Make (String) + type filesys = - | Directory of { - perm: int; - dir_name: string; - fs_list: filesys list } - | File of { - perm: int; - file_name: string } - [@@deriving show { with_path = false }] + | Directory of {perm: int; fs_map: filesys Map_names.t} + | File of {perm: int} type state = filesys @@ -28,246 +24,230 @@ struct let (/) = Filename.concat let arb_cmd _s = - let str_gen = Gen.(oneofl ["c"; "e"; "r"]) in let name_gen = Gen.(oneofl ["aaa" ; "bbb" ; "ccc" ; "ddd" ; "eee"]) in - let path_gen = Gen.map (fun path -> "sandbox_root" :: path) (Gen.list_size (Gen.int_bound 5) name_gen) in + let path_gen = Gen.map (fun path -> path) (Gen.list_size (Gen.int_bound 5) name_gen) in (* can be empty *) let perm_gen = Gen.(oneofl [0o777]) in (* let perm_gen = Gen.map3 (fun d1 d2 d3 -> d1*100 + d2*10 + d3*1) (Gen.int_bound 7) (Gen.int_bound 7) (Gen.int_bound 7) in *) QCheck.make ~print:show_cmd Gen.(oneof [ - map2 (fun path name -> File_exists (path, name)) path_gen str_gen; - map3 (fun path dir_name perm -> Mkdir (path, dir_name, perm)) path_gen str_gen perm_gen; - map2 (fun path dir_name -> Rmdir (path, dir_name)) path_gen str_gen; - map2 (fun path dir_name -> Readdir (path, dir_name)) path_gen str_gen; + map (fun path -> File_exists (path)) path_gen ; + map3 (fun path new_dir_name perm -> Mkdir (path, new_dir_name, perm)) path_gen name_gen perm_gen; + map2 (fun path delete_dir_name -> Rmdir (path, delete_dir_name)) path_gen name_gen; + map (fun path -> Readdir (path)) path_gen; ]) let static_path = Sys.getcwd () - let init_state = - Directory {perm = 0o777; dir_name = "sandbox_root"; fs_list = []} - - let rec is_perm_ok (fsl: filesys list) path = - match fsl with - | [] -> true - | Directory d :: tl -> (match path with - | [] -> true - | hd_path :: tl_path -> if d.dir_name = hd_path - then if d.perm > 447 - then is_perm_ok d.fs_list tl_path - else false - else is_perm_ok tl path - ) - | File f :: tl -> (match path with - | [] -> true - | hd_path :: _tl_path -> if f.file_name = hd_path - then true - else is_perm_ok tl path - ) - - let rec mem fs path name = - match fs with - | File f -> path = [] && f.file_name = name - | Directory d -> - match path with - | [] -> name = d.dir_name - | hd :: tl -> - if hd = d.dir_name - then List.exists (fun f -> mem f tl name) d.fs_list - else false - - let is_dir_empty = function - | File _f -> false - | Directory d -> d.fs_list = [] - - let is_a_dir = function - | File _f -> false - | Directory _d -> true + let init_state = Directory {perm = 0o777; fs_map = Map_names.empty} - let rec is_path_empty fs path dir_name = - match fs with - | File _f -> false - | Directory d -> - match path with - | [] -> dir_name = d.dir_name && is_dir_empty (Directory d) - | hd :: tl -> - if hd = d.dir_name - then List.exists (fun f -> is_path_empty f tl dir_name) d.fs_list - else false - - let rec is_path_a_dir fs path dir_name = - match fs with - | File _f -> false + (* val find_opt : filesys -> string list -> filesys option *) + let rec find_opt fs path = + match fs with + | File f -> if path = [] then Some (File f) else None | Directory d -> - match path with - | [] -> dir_name = d.dir_name + (match path with + | [] -> Some (Directory d) | hd :: tl -> - if hd = d.dir_name - then List.exists (fun f -> is_path_a_dir f tl dir_name) d.fs_list - else false + (match Map_names.find_opt hd d.fs_map with + | None -> None + | Some fs -> find_opt fs tl)) - let get_name fs = - match fs with - | File f -> f.file_name - | Directory d -> d.dir_name + (* val mem : filesys -> string list -> bool *) + let mem fs path = + match find_opt fs path with + | None -> false + | Some _ -> true - let rec mkdir fs path dir_name perm = - match fs with - | File _f -> fs + (* val mkdir : filesys -> string list -> string -> int -> filesys *) + let rec mkdir fs path new_dir_name perm = + match fs with + | File _ -> fs | Directory d -> - match path with - | [] -> - if List.exists (fun fs -> get_name fs = dir_name) d.fs_list - then fs - else Directory {d with fs_list = (Directory {perm; dir_name; fs_list = []} :: d.fs_list)} - | hd :: [] -> - if hd = d.dir_name - then ( - if List.exists (fun fs -> get_name fs = dir_name) d.fs_list + (match path with + | [] -> + let new_dir = Directory {perm; fs_map = Map_names.empty} in + Directory {d with 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 sub_fs tl_path new_dir_name perm in + if nfs = sub_fs then fs - else Directory {d with fs_list = (Directory {perm; dir_name; fs_list = []} :: d.fs_list)}) - else fs - | hd :: tl -> - if hd = d.dir_name - then Directory {d with fs_list = List.map (fun f -> mkdir f tl dir_name perm) d.fs_list} - else fs - - let rec rmdir fs path dir_name = - match fs with - | File _f -> fs - | Directory d -> - match path with - | [] -> - if not (List.exists (fun fs -> get_name fs = dir_name) d.fs_list) || not (is_dir_empty (Directory d)) - then fs - else Directory {d with fs_list = List.filter (fun f -> not (get_name f = dir_name)) d.fs_list} - | hd :: [] -> - if List.exists (fun fs -> get_name fs = dir_name && is_dir_empty fs) d.fs_list - && not (is_dir_empty (Directory d)) - && hd = d.dir_name - then Directory {d with fs_list = List.filter (fun f -> not (get_name f = dir_name)) d.fs_list} - else fs - | hd :: tl -> - if not (hd = d.dir_name) - then fs - else Directory {d with fs_list = List.map (fun f -> rmdir f tl dir_name) d.fs_list} - - let rec find_opt fs path name = - match fs with - | File _f -> None - | Directory d -> - match path with - | [] -> - if d.dir_name = name - then Some (Directory d) - else None - | hd :: tl -> - if d.dir_name = hd - then ( - let path_next = (match tl with | [] -> name | _ :: _ -> List.hd tl) in - let fs_next = List.find_opt ( - fun e -> - match e with - | File _f -> false - | Directory d -> d.dir_name = path_next) d.fs_list in - match fs_next with - | None -> None - | Some fs -> find_opt fs tl name) - else None - - let get_sub_name fs = - match fs with - | File f -> f.file_name - | Directory d -> d.dir_name + 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 {d with fs_map = new_map})) - let readdir fs path dir_name = - match find_opt fs path dir_name with - | None -> None + (* val readdir : filesys -> string list -> string list option *) + let readdir fs path = + match find_opt fs path with + | None -> None | Some fs -> match fs with - | File _f -> None - | Directory d -> Some (List.map get_sub_name d.fs_list) + | File _ -> None + | Directory d -> Some (Map_names.fold (fun k _ l -> l @ [k]) d.fs_map []) + + + (* val rmdir : filesys -> string list -> string -> filesys *) + let rec rmdir fs path delete_dir_name = + match fs with + | File _ -> fs + | Directory d -> + (match path with + | [] -> + let target_fs = Map_names.find_opt delete_dir_name d.fs_map in + (match target_fs with + | None -> Directory d + | Some fs -> + (match fs with + | File _ -> Directory d + | Directory target -> + let readd_target = (Map_names.fold (fun k _ l -> l @ [k]) target.fs_map []) in + if readd_target = [] + then Directory {d with fs_map = Map_names.remove delete_dir_name d.fs_map} + else Directory d)) + | 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 sub_fs tl_path delete_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 {d with fs_map = new_map})) let next_state c fs = match c with - | File_exists (_path, _name) -> fs - | Mkdir (path, dir_name, perm) -> - if mem fs path dir_name + | File_exists (_path) -> fs + | Mkdir (path, new_dir_name, perm) -> + if mem fs (path @ [new_dir_name]) then fs - else mkdir fs path dir_name perm - | Rmdir (path, dir_name) -> - if mem fs path dir_name - then rmdir fs path dir_name + else mkdir fs path new_dir_name perm + | Rmdir (path,delete_dir_name) -> + if mem fs (path @ [delete_dir_name]) + then rmdir fs path delete_dir_name else fs - | Readdir (_path, _dir_name) -> fs + | Readdir _path -> fs let init_sut () = try Sys.mkdir (static_path / "sandbox_root") 0o777 with Sys_error _ -> () + (* ignore (Sys.command ("mkdir " ^ static_path ^ "/sandbox_root")) *) + (* creer sandbox_root + si il existe deja + il est vide = on fait rien + il est pas vide = on le rm -d et on le recree + si il existe pas = on le cree *) + (* let path = static_path ^ "/sandbox_root" in + ignore (Sys.command ("rm -rf " ^ path ^ " && mkdir " ^ path)) *) + + + + (* let err = Sys.command ("mkdir " ^ static_path ^ "/sandbox_root") in + if err = 1 + then + (Format.printf "then\n"; + ignore (Sys.command ("rm -r -d -f " ^ static_path ^ "/sandbox_root")); + ignore (Sys.command ("mkdir " ^ static_path ^ "/sandbox_root"))) + else Format.printf "else\n" *) - let cleanup _ = ignore (Sys.command ("rm -r -d -f " ^ (static_path / "sandbox_root"))) + let cleanup _ = ignore (Sys.command ("rm -r -d -f " ^ static_path ^ "/sandbox_root")) let precond _c _s = true let run c _file_name = match c with - | File_exists (path, name) -> Res (bool, Sys.file_exists (static_path / (List.fold_left (/) "" path) / name)) - | Mkdir (path, dir_name, perm) -> - Res (result unit exn, protect (Sys.mkdir (static_path / (List.fold_left (/) "" path) / dir_name))perm) - | Rmdir (path, dir_name) -> - Res (result unit exn, protect (Sys.rmdir) (static_path / (List.fold_left (/) "" path) / dir_name)) - | Readdir (path, dir_name) -> - Res (result (array string) exn, protect (Sys.readdir) (static_path / (List.fold_left (/) "" path) / dir_name)) + | File_exists (path) -> Res (bool, Sys.file_exists (static_path / "sandbox_root" / (List.fold_left (/) "" path))) + | Mkdir (path, new_dir_name, perm) -> + Res (result unit exn, protect (Sys.mkdir (static_path / "sandbox_root" / (List.fold_left (/) "" path) / new_dir_name))perm) + | Rmdir (path, delete_dir_name) -> + Res (result unit exn, protect (Sys.rmdir) (static_path / "sandbox_root" / (List.fold_left (/) "" path) / delete_dir_name)) + | Readdir (path) -> + Res (result (array string) exn, protect (Sys.readdir) (static_path / "sandbox_root" / (List.fold_left (/) "" path))) + + let cut_path p = List.rev (List.tl (List.rev p)) + let is_a_dir fs = match fs with | Directory _ -> true | File _ -> false let postcond c (fs: filesys) res = - let p path dir_name = static_path / (String.concat "/" path) / dir_name in + let p path = static_path / "sandbox_root" / (String.concat "/" path) in match c, res with - | File_exists (path, name), Res ((Bool,_),b) -> b = mem fs path name - | Mkdir (path, dir_name, _perm), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) - when s = (p path dir_name) ^ ": Permission denied" -> - not (is_perm_ok [fs] path) - | Mkdir (path, dir_name, _perm), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) - when s = (p path dir_name) ^ ": File exists" -> - mem fs path dir_name - | Mkdir (path, dir_name, _perm), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) - when s = (p path dir_name) ^ ": No such file or directory" -> - (match path with - | [] -> false - | _hd_path :: _tl_path -> - let rev = List.rev path in - not (mem fs (List.rev (List.tl rev)) (List.hd rev))) - | Mkdir (path, dir_name, _perm), Res ((Result (Unit,Exn),_), Ok ()) -> - let b = ( - match path with - | [] -> true - | _hd_path :: _tl_path -> - let rev = List.rev path in - mem fs (List.rev (List.tl rev)) (List.hd rev)) in - is_perm_ok [fs] path && not (mem fs path dir_name) && b - | Mkdir (_path, _dir_name, _perm), Res ((Result (Unit,Exn),_), _r) -> false - | Rmdir (path, dir_name), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) - when s = (p path dir_name) ^ ": No such file or directory" -> - not (mem fs path dir_name) - | Rmdir (path, dir_name), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) - when s = (p path dir_name) ^ ": Directory not empty" -> - not (is_path_empty fs path dir_name) - | Rmdir (path, dir_name), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) - when s = (p path dir_name) ^ ": Not a directory" -> - not (is_path_a_dir fs path dir_name) - | Rmdir (path, dir_name), Res ((Result (Unit,Exn),_), Ok ()) -> - mem fs path dir_name && is_path_empty fs path dir_name - | Rmdir (_path, _dir_name), Res ((Result (Unit,Exn),_), _r) -> false - | Readdir (path, dir_name), Res ((Result (Array String,Exn),_), Error (Sys_error (s) )) - when s = (p path dir_name) ^ ": No such file or directory" -> - not (mem fs path dir_name) - | Readdir (path, dir_name), Res ((Result (Array String,Exn),_), Error (Sys_error (s) )) - when s = (p path dir_name) ^ ": Not a directory" -> - not (is_path_a_dir fs path dir_name) - | Readdir (path, dir_name), Res ((Result (Array String,Exn),_), r) -> + | File_exists (path), Res ((Bool,_),b) -> b = mem fs path + | Mkdir (path, new_dir_name, _perm), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) + when s = (p (path @ [new_dir_name])) ^ ": Permission denied" -> true + | Mkdir (path, new_dir_name, _perm), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) + when s = (p (path @ [new_dir_name])) ^ ": File exists" -> + mem fs (path @ [new_dir_name]) + | Mkdir (path, new_dir_name, _perm), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) + when s = (p (path @ [new_dir_name])) ^ ": No such file or directory" -> + let b = not (mem fs path) in + b + | Mkdir (path, new_dir_name, _perm), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) + when s = (p (path @ [new_dir_name])) ^ ": Not a directory" -> + (match find_opt fs (path @ [new_dir_name]) with + | None -> false + | Some target_fs -> not (is_a_dir target_fs)) + | Mkdir (path, new_dir_name, _perm), Res ((Result (Unit,Exn),_), Ok ()) -> + let is_existing_is_a_dir = + (match find_opt fs path with + | None -> false + | Some target_fs -> is_a_dir target_fs) in + true && not (mem fs (path @ [new_dir_name])) && mem fs path && is_existing_is_a_dir + | Mkdir (_path, _new_dir_name, _perm), Res ((Result (Unit,Exn),_), _) -> false + + + + | Rmdir (path, delete_dir_name), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) + when s = (p (path @ [delete_dir_name])) ^ ": No such file or directory" -> + not (mem fs (path @ [delete_dir_name])) + + | Rmdir (path, delete_dir_name), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) + when s = (p (path @ [delete_dir_name])) ^ ": Directory not empty" -> + not (readdir fs (path @ [delete_dir_name]) = Some []) + + + | Rmdir (path, delete_dir_name), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) + when s = (p (path @ [delete_dir_name])) ^ ": Not a directory" -> + (match find_opt fs (path @ [delete_dir_name]) with + | None -> false + | Some target_fs -> not (is_a_dir target_fs)) + + + | Rmdir (path, delete_dir_name), Res ((Result (Unit,Exn),_), Ok ()) -> + let is_empty = readdir fs (path @ [delete_dir_name]) = Some [] in + let is_a_dir = + (match find_opt fs (path @ [delete_dir_name]) with + | None -> false + | Some target_fs -> is_a_dir target_fs) in + mem fs (path @ [delete_dir_name]) && is_empty && is_a_dir + + | Rmdir (_path, _delete_dir_name), Res ((Result (Unit,Exn),_), _r) -> false + + + + | Readdir (path), Res ((Result (Array String,Exn),_), Error (Sys_error (s) )) + when s = (p path) ^ ": Permission denied" -> true + | Readdir (path), Res ((Result (Array String,Exn),_), Error (Sys_error (s) )) + when s = (p path) ^ ": No such file or directory" -> + not (mem fs path) + | Readdir (path), Res ((Result (Array String,Exn),_), Error (Sys_error (s) )) + when s = (p path) ^ ": Not a directory" -> + (* not (is_a_dir fs path) *) + (match find_opt fs path with + | None -> false + | Some target_fs -> is_a_dir target_fs) + | Readdir (path), Res ((Result (Array String,Exn),_), r) -> (match r with | Error _e -> false | Ok a -> let sut = List.sort (fun a b -> -(String.compare a b)) (Array.to_list a) in - (match readdir fs path dir_name with + (match readdir fs path with | None -> false | Some l -> List.sort (fun a b -> -(String.compare a b)) l = sut ) ) + + + + | _,_ -> false end From 60af52b5f1935db1118848b798cf356d298fa15d Mon Sep 17 00:00:00 2001 From: Lucccyo Date: Thu, 10 Nov 2022 15:08:45 +0100 Subject: [PATCH 03/33] adding touch command, new interface STM_base, some cleanup --- src/sys/dune | 2 +- src/sys/stm_tests.ml | 333 +++++++++++++++++++++---------------------- 2 files changed, 160 insertions(+), 175 deletions(-) diff --git a/src/sys/dune b/src/sys/dune index cd0123866..9756f4414 100644 --- a/src/sys/dune +++ b/src/sys/dune @@ -10,7 +10,7 @@ (executable (name stm_tests) (modules stm_tests) - (libraries STM) + (libraries qcheck-stm.sequential qcheck-stm.domain) (preprocess (pps ppx_deriving.show))) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index f6b954141..fe9f45bd3 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -1,129 +1,137 @@ open QCheck -open STM +open STM_base -module SConf = +module SConf = struct - type cmd = - | File_exists of string list + | File_exists of string list | Mkdir of string list * string * int | Rmdir of string list * string - | Readdir of string list + | Readdir of string list + | Touch of string list * string * int [@@deriving show { with_path = false }] - module Map_names = Map.Make (String) + module Map_names = Map.Make (String) - type filesys = + type filesys = | Directory of {perm: int; fs_map: filesys Map_names.t} | File of {perm: int} - + type state = filesys - - type sut = unit - + + type sut = unit + let (/) = Filename.concat + + let update_map_name map_name k v = Map_names.add k v (Map_names.remove k map_name) let arb_cmd _s = let name_gen = Gen.(oneofl ["aaa" ; "bbb" ; "ccc" ; "ddd" ; "eee"]) in let path_gen = Gen.map (fun path -> path) (Gen.list_size (Gen.int_bound 5) name_gen) in (* can be empty *) let perm_gen = Gen.(oneofl [0o777]) in - (* let perm_gen = Gen.map3 (fun d1 d2 d3 -> d1*100 + d2*10 + d3*1) (Gen.int_bound 7) (Gen.int_bound 7) (Gen.int_bound 7) in *) - QCheck.make ~print:show_cmd + QCheck.make ~print:show_cmd Gen.(oneof - [ + [ map (fun path -> File_exists (path)) path_gen ; map3 (fun path new_dir_name perm -> Mkdir (path, new_dir_name, perm)) path_gen name_gen perm_gen; - map2 (fun path delete_dir_name -> Rmdir (path, delete_dir_name)) path_gen name_gen; + map2 (fun path delete_dir_name -> Rmdir (path, delete_dir_name)) path_gen name_gen; map (fun path -> Readdir (path)) path_gen; + map3 (fun path new_file_name perm -> Touch (path, new_file_name, perm)) path_gen name_gen perm_gen; ]) let static_path = Sys.getcwd () let init_state = Directory {perm = 0o777; fs_map = Map_names.empty} - (* val find_opt : filesys -> string list -> filesys option *) - let rec find_opt fs path = + let rec find_opt fs path = match fs with - | File f -> if path = [] then Some (File f) else None + | File f -> + if path = [] + then Some (File f) + 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)) - - (* val mem : filesys -> string list -> bool *) - let mem fs path = + (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 = match find_opt fs path with | None -> false | Some _ -> true - (* val mkdir : filesys -> string list -> string -> int -> filesys *) - let rec mkdir fs path new_dir_name perm = + let rec mkdir fs path new_dir_name perm = match fs with | File _ -> fs - | Directory d -> - (match path with - | [] -> + | Directory d -> + (match path with + | [] -> let new_dir = Directory {perm; fs_map = Map_names.empty} in Directory {d with fs_map = Map_names.add new_dir_name new_dir d.fs_map} - | next_in_path :: tl_path -> + | next_in_path :: tl_path -> (match Map_names.find_opt next_in_path d.fs_map with | None -> fs - | Some sub_fs -> + | Some sub_fs -> let nfs = mkdir sub_fs tl_path new_dir_name perm in if nfs = sub_fs then fs - else + 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 {d with fs_map = new_map})) - (* val readdir : filesys -> string list -> string list option *) - let readdir fs path = + let readdir fs path = match find_opt fs path with | None -> None - | Some fs -> + | Some fs -> match fs with | File _ -> None | Directory d -> Some (Map_names.fold (fun k _ l -> l @ [k]) d.fs_map []) - - (* val rmdir : filesys -> string list -> string -> filesys *) - let rec rmdir fs path delete_dir_name = + let rec rmdir fs path delete_dir_name = match fs with | File _ -> fs - | Directory d -> - (match path with - | [] -> - let target_fs = Map_names.find_opt delete_dir_name d.fs_map in - (match target_fs with - | None -> Directory d - | Some fs -> - (match fs with - | File _ -> Directory d - | Directory target -> - let readd_target = (Map_names.fold (fun k _ l -> l @ [k]) target.fs_map []) in - if readd_target = [] - then Directory {d with fs_map = Map_names.remove delete_dir_name d.fs_map} - else Directory d)) - | next_in_path :: tl_path -> + | 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 {d with 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 -> + | Some sub_fs -> let nfs = rmdir sub_fs tl_path delete_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 {d with fs_map = new_map})) + else + Directory {d with fs_map = (update_map_name d.fs_map next_in_path nfs)})) + + let rec touch fs path new_file_name perm = + match fs with + | File _ -> fs + | Directory d -> + (match path with + | [] -> + let new_file = File {perm} in + Directory {d with 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 = touch sub_fs tl_path new_file_name perm in + if nfs = sub_fs + then fs + else + Directory {d with fs_map = update_map_name d.fs_map next_in_path nfs})) - let next_state c fs = + let next_state c fs = match c with | File_exists (_path) -> fs - | Mkdir (path, new_dir_name, perm) -> + | Mkdir (path, new_dir_name, perm) -> if mem fs (path @ [new_dir_name]) then fs else mkdir fs path new_dir_name perm @@ -131,133 +139,110 @@ struct if mem fs (path @ [delete_dir_name]) then rmdir fs path delete_dir_name else fs - | Readdir _path -> fs - - let init_sut () = try Sys.mkdir (static_path / "sandbox_root") 0o777 with Sys_error _ -> () - (* ignore (Sys.command ("mkdir " ^ static_path ^ "/sandbox_root")) *) - (* creer sandbox_root - si il existe deja - il est vide = on fait rien - il est pas vide = on le rm -d et on le recree - si il existe pas = on le cree *) - (* let path = static_path ^ "/sandbox_root" in - ignore (Sys.command ("rm -rf " ^ path ^ " && mkdir " ^ path)) *) - - + | Readdir _path -> fs + | Touch (path, new_file_name, perm) -> + if mem fs (path @ [new_file_name]) + then fs + else touch fs path new_file_name perm - (* let err = Sys.command ("mkdir " ^ static_path ^ "/sandbox_root") in - if err = 1 - then - (Format.printf "then\n"; - ignore (Sys.command ("rm -r -d -f " ^ static_path ^ "/sandbox_root")); - ignore (Sys.command ("mkdir " ^ static_path ^ "/sandbox_root"))) - else Format.printf "else\n" *) + let init_sut () = ignore(Sys.command ("rm -rf " ^ (static_path / "sandbox_root") ^ " && mkdir " ^ (static_path / "sandbox_root"))) let cleanup _ = ignore (Sys.command ("rm -r -d -f " ^ static_path ^ "/sandbox_root")) - let precond _c _s = true + let precond _c _s = true - let run c _file_name = match c with - | File_exists (path) -> Res (bool, Sys.file_exists (static_path / "sandbox_root" / (List.fold_left (/) "" path))) - | Mkdir (path, new_dir_name, perm) -> - Res (result unit exn, protect (Sys.mkdir (static_path / "sandbox_root" / (List.fold_left (/) "" path) / new_dir_name))perm) - | Rmdir (path, delete_dir_name) -> - Res (result unit exn, protect (Sys.rmdir) (static_path / "sandbox_root" / (List.fold_left (/) "" path) / delete_dir_name)) - | Readdir (path) -> - Res (result (array string) exn, protect (Sys.readdir) (static_path / "sandbox_root" / (List.fold_left (/) "" path))) + let run c _file_name = + let p path = static_path / "sandbox_root" / (List.fold_left (/) "" path) in + match c with + | File_exists (path) -> Res (bool, Sys.file_exists (p path)) + | Mkdir (path, new_dir_name, perm) -> + Res (result unit exn, protect (Sys.mkdir ((p path) / new_dir_name)) perm) + | 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)) + | Touch (path, new_file_name, _perm) -> + Res (unit, ignore(Sys.command ("touch " ^ (p path) / new_file_name ^ " 2>/dev/null"))) - let cut_path p = List.rev (List.tl (List.rev p)) let is_a_dir fs = match fs with | Directory _ -> true | File _ -> false - let postcond c (fs: filesys) res = + let postcond c (fs: filesys) res = let p path = static_path / "sandbox_root" / (String.concat "/" path) in match c, res with | File_exists (path), Res ((Bool,_),b) -> b = mem fs path - | Mkdir (path, new_dir_name, _perm), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) - when s = (p (path @ [new_dir_name])) ^ ": Permission denied" -> true - | Mkdir (path, new_dir_name, _perm), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) - when s = (p (path @ [new_dir_name])) ^ ": File exists" -> - mem fs (path @ [new_dir_name]) - | Mkdir (path, new_dir_name, _perm), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) - when s = (p (path @ [new_dir_name])) ^ ": No such file or directory" -> - let b = not (mem fs path) in - b - | Mkdir (path, new_dir_name, _perm), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) - when s = (p (path @ [new_dir_name])) ^ ": Not a directory" -> - (match find_opt fs (path @ [new_dir_name]) with - | None -> false - | Some target_fs -> not (is_a_dir target_fs)) - | Mkdir (path, new_dir_name, _perm), Res ((Result (Unit,Exn),_), Ok ()) -> - let is_existing_is_a_dir = - (match find_opt fs path with - | None -> false - | Some target_fs -> is_a_dir target_fs) in - true && not (mem fs (path @ [new_dir_name])) && mem fs path && is_existing_is_a_dir - | Mkdir (_path, _new_dir_name, _perm), Res ((Result (Unit,Exn),_), _) -> false - - - - | Rmdir (path, delete_dir_name), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) - when s = (p (path @ [delete_dir_name])) ^ ": No such file or directory" -> - not (mem fs (path @ [delete_dir_name])) - - | Rmdir (path, delete_dir_name), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) - when s = (p (path @ [delete_dir_name])) ^ ": Directory not empty" -> - not (readdir fs (path @ [delete_dir_name]) = Some []) - - - | Rmdir (path, delete_dir_name), Res ((Result (Unit,Exn),_), Error (Sys_error (s) )) - when s = (p (path @ [delete_dir_name])) ^ ": Not a directory" -> - (match find_opt fs (path @ [delete_dir_name]) with - | None -> false - | Some target_fs -> not (is_a_dir target_fs)) - - - | Rmdir (path, delete_dir_name), Res ((Result (Unit,Exn),_), Ok ()) -> - let is_empty = readdir fs (path @ [delete_dir_name]) = Some [] in - let is_a_dir = - (match find_opt fs (path @ [delete_dir_name]) with - | None -> false - | Some target_fs -> is_a_dir target_fs) in - mem fs (path @ [delete_dir_name]) && is_empty && is_a_dir - - | Rmdir (_path, _delete_dir_name), Res ((Result (Unit,Exn),_), _r) -> false - - - - | Readdir (path), Res ((Result (Array String,Exn),_), Error (Sys_error (s) )) - when s = (p path) ^ ": Permission denied" -> true - | Readdir (path), Res ((Result (Array String,Exn),_), Error (Sys_error (s) )) - when s = (p path) ^ ": No such file or directory" -> - not (mem fs path) - | Readdir (path), Res ((Result (Array String,Exn),_), Error (Sys_error (s) )) - when s = (p path) ^ ": Not a directory" -> - (* not (is_a_dir fs path) *) - (match find_opt fs path with - | None -> false - | Some target_fs -> is_a_dir target_fs) - | Readdir (path), Res ((Result (Array String,Exn),_), r) -> - (match r with - | Error _e -> false - | Ok a -> - let sut = List.sort (fun a b -> -(String.compare a b)) (Array.to_list a) in - (match readdir fs path with - | None -> false - | Some l -> List.sort (fun a b -> -(String.compare a b)) l = sut ) ) - - - - + | Mkdir (path, new_dir_name, _perm), 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 fs complete_path) || + (s = (p complete_path) ^ ": No such file or directory" && not (mem fs path)) || + (s = (p complete_path) ^ ": Not a directory" && + (match find_opt fs complete_path with + | None -> true + | Some target_fs -> not (is_a_dir target_fs))) + | _ -> false) + | Ok () -> + let is_existing_is_a_dir = + (match find_opt fs path with + | None -> false + | Some target_fs -> is_a_dir target_fs) in + not (mem fs complete_path) && mem fs path && is_existing_is_a_dir) + | 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) ^ ": Directory not empty" && not (readdir fs complete_path = Some [])) || + (s = (p complete_path) ^ ": No such file or directory" && not (mem fs complete_path)) || + (s = (p complete_path) ^ ": Not a directory" && + (match find_opt fs complete_path with + | None -> true + | Some target_fs -> not (is_a_dir target_fs))) + | _ -> false) + | Ok () -> + let is_empty = readdir fs complete_path = Some [] in + let is_a_dir = + (match find_opt fs complete_path with + | None -> false + | Some target_fs -> is_a_dir target_fs) in + mem fs complete_path && is_empty && is_a_dir) + | 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 fs path)) || + (s = (p path) ^ ": Not a directory" && + (match find_opt fs path with + | None -> true + | Some target_fs -> not (is_a_dir target_fs))) + | _ -> false) + | Ok array_of_subdir -> + let sut = List.sort (fun a b -> -(String.compare a b)) (Array.to_list array_of_subdir) in + let same_result = + (match readdir fs path with + | None -> false + | Some l -> List.sort (fun a b -> -(String.compare a b)) l = sut) in + let is_a_dir = + (match find_opt fs path with + | None -> true + | Some target_fs -> is_a_dir target_fs) in + same_result && mem fs path && is_a_dir) + | Touch (_path, _new_dir_name, _perm), Res ((Unit,_),_) -> true | _,_ -> false end -module SysSTM = STM.Make(SConf) +module Sys_seq = STM_sequential.Make(SConf) +module Sys_dom = STM_domain.Make(SConf) -;; -Util.set_ci_printing () ;; QCheck_base_runner.run_tests_main (let count = 1000 in - [SysSTM.agree_test ~count ~name:"STM Sys test sequential"; - (* SysSTM.neg_agree_test_par ~count ~name:"STM Sys test parallel" *) + [Sys_seq.agree_test ~count ~name:"STM Sys test sequential"; + (* Sys_dom.neg_agree_test_par ~count ~name:"STM Sys test parallel" *) ]) From 24eeda94b8955e01cea0fb4e8fd5ee18fdf38c17 Mon Sep 17 00:00:00 2001 From: Lucccyo Date: Thu, 17 Nov 2022 19:20:11 +0100 Subject: [PATCH 04/33] add windows os support --- src/sys/stm_tests.ml | 85 ++++++++++++++++++++------------------------ 1 file changed, 39 insertions(+), 46 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index fe9f45bd3..a3b089329 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -22,7 +22,7 @@ struct type sut = unit let (/) = Filename.concat - + let update_map_name map_name k v = Map_names.add k v (Map_names.remove k map_name) let arb_cmd _s = @@ -49,7 +49,7 @@ struct if path = [] then Some (File f) else None - | Directory d -> + | Directory d -> (match path with | [] -> Some (Directory d) | hd :: tl -> @@ -57,10 +57,7 @@ struct | None -> None | Some fs -> find_opt fs tl)) - let mem fs path = - match find_opt fs path with - | None -> false - | Some _ -> true + let mem fs path = find_opt fs path <> None let rec mkdir fs path new_dir_name perm = match fs with @@ -145,14 +142,26 @@ struct then fs else touch fs path new_file_name perm - let init_sut () = ignore(Sys.command ("rm -rf " ^ (static_path / "sandbox_root") ^ " && mkdir " ^ (static_path / "sandbox_root"))) - - let cleanup _ = ignore (Sys.command ("rm -r -d -f " ^ static_path ^ "/sandbox_root")) + let init_sut () = + match Sys.os_type with + | "Unix" -> ignore (Sys.command ("rm -rf " ^ (static_path / "sandbox_root") ^ " && mkdir " ^ (static_path / "sandbox_root"))) + | "Win32" -> + ignore (Sys.command ( + "powershell -Command \"Remove-Item -Path " ^ (static_path / "sandbox_root") ^ " -Recurse -Force -ErrorAction Ignore \" + & mkdir " ^ (static_path / "sandbox_root"))) + | v -> failwith ("Sys tests not working with " ^ v) + + let cleanup _ = + match Sys.os_type with + | "Unix" -> ignore (Sys.command ("rm -rf " ^ (static_path / "sandbox_root"))) + | "Win32" -> ignore (Sys.command ("powershell -Command \"Remove-Item '" ^ (static_path / "sandbox_root") ^ "' -Recurse -Force\"")) + | v -> failwith ("Sys tests not working with " ^ v) let precond _c _s = true + let p path = (List.fold_left (/) (static_path / "sandbox_root") path) + let run c _file_name = - let p path = static_path / "sandbox_root" / (List.fold_left (/) "" path) in match c with | File_exists (path) -> Res (bool, Sys.file_exists (p path)) | Mkdir (path, new_dir_name, perm) -> @@ -162,12 +171,19 @@ struct | Readdir (path) -> Res (result (array string) exn, protect (Sys.readdir) (p path)) | Touch (path, new_file_name, _perm) -> - Res (unit, ignore(Sys.command ("touch " ^ (p path) / new_file_name ^ " 2>/dev/null"))) + (match Sys.os_type with + | "Unix" -> Res (unit, ignore(Sys.command ("touch " ^ (p path) / new_file_name ^ " 2>/dev/null"))) + | "Win32" -> Res (unit, ignore(Sys.command ("type nul >> \"" ^ (p path / new_file_name) ^ "\""))) + | v -> failwith ("Sys tests not working with " ^ v)) + + let fs_is_a_dir fs = match fs with | Directory _ -> true | File _ -> false - let is_a_dir fs = match fs with | Directory _ -> true | File _ -> false + let path_is_a_dir fs path = + match find_opt fs path with + | None -> false + | Some target_fs -> fs_is_a_dir target_fs let postcond c (fs: filesys) res = - let p path = static_path / "sandbox_root" / (String.concat "/" path) in match c, res with | File_exists (path), Res ((Bool,_),b) -> b = mem fs path | Mkdir (path, new_dir_name, _perm), Res ((Result (Unit,Exn),_), res) -> @@ -179,17 +195,9 @@ struct (s = (p complete_path) ^ ": Permission denied") || (s = (p complete_path) ^ ": File exists" && mem fs complete_path) || (s = (p complete_path) ^ ": No such file or directory" && not (mem fs path)) || - (s = (p complete_path) ^ ": Not a directory" && - (match find_opt fs complete_path with - | None -> true - | Some target_fs -> not (is_a_dir target_fs))) + (s = (p complete_path) ^ ": Not a directory" && not (path_is_a_dir fs complete_path)) | _ -> false) - | Ok () -> - let is_existing_is_a_dir = - (match find_opt fs path with - | None -> false - | Some target_fs -> is_a_dir target_fs) in - not (mem fs complete_path) && mem fs path && is_existing_is_a_dir) + | Ok () -> not (mem fs complete_path) && mem fs path && path_is_a_dir fs path) | Rmdir (path, delete_dir_name), Res ((Result (Unit,Exn),_), res) -> let complete_path = (path @ [delete_dir_name]) in (match res with @@ -198,18 +206,11 @@ struct | Sys_error s -> (s = (p complete_path) ^ ": Directory not empty" && not (readdir fs complete_path = Some [])) || (s = (p complete_path) ^ ": No such file or directory" && not (mem fs complete_path)) || - (s = (p complete_path) ^ ": Not a directory" && - (match find_opt fs complete_path with - | None -> true - | Some target_fs -> not (is_a_dir target_fs))) + (s = (p complete_path) ^ ": Not a directory" && not (path_is_a_dir fs complete_path)) | _ -> false) | Ok () -> let is_empty = readdir fs complete_path = Some [] in - let is_a_dir = - (match find_opt fs complete_path with - | None -> false - | Some target_fs -> is_a_dir target_fs) in - mem fs complete_path && is_empty && is_a_dir) + mem fs complete_path && is_empty && path_is_a_dir fs complete_path) | Readdir (path), Res ((Result (Array String,Exn),_), res) -> (match res with | Error err -> @@ -217,10 +218,7 @@ struct | Sys_error s -> (s = (p path) ^ ": Permission denied") || (s = (p path) ^ ": No such file or directory" && not (mem fs path)) || - (s = (p path) ^ ": Not a directory" && - (match find_opt fs path with - | None -> true - | Some target_fs -> not (is_a_dir target_fs))) + (s = (p path) ^ ": Not a directory" && not (path_is_a_dir fs path)) | _ -> false) | Ok array_of_subdir -> let sut = List.sort (fun a b -> -(String.compare a b)) (Array.to_list array_of_subdir) in @@ -228,11 +226,7 @@ struct (match readdir fs path with | None -> false | Some l -> List.sort (fun a b -> -(String.compare a b)) l = sut) in - let is_a_dir = - (match find_opt fs path with - | None -> true - | Some target_fs -> is_a_dir target_fs) in - same_result && mem fs path && is_a_dir) + same_result && mem fs path && path_is_a_dir fs path) | Touch (_path, _new_dir_name, _perm), Res ((Unit,_),_) -> true | _,_ -> false end @@ -241,8 +235,7 @@ module Sys_seq = STM_sequential.Make(SConf) module Sys_dom = STM_domain.Make(SConf) ;; -QCheck_base_runner.run_tests_main - (let count = 1000 in - [Sys_seq.agree_test ~count ~name:"STM Sys test sequential"; - (* Sys_dom.neg_agree_test_par ~count ~name:"STM Sys test parallel" *) -]) +QCheck_base_runner.run_tests_main [ + Sys_seq.agree_test ~count:1000 ~name:"STM Sys test sequential"; + Sys_dom.agree_test_par ~count:100 ~name:"STM Sys test parallel" + ] From fd28eef88273a983d698f25da6e632862eb6bede Mon Sep 17 00:00:00 2001 From: Lucccyo Date: Tue, 20 Dec 2022 10:05:21 +0100 Subject: [PATCH 05/33] style adjustment, make touch return an integer, dune file update --- src/sys/dune | 22 ++---- src/sys/stm_tests.ml | 167 +++++++++++++++++++++---------------------- 2 files changed, 87 insertions(+), 102 deletions(-) diff --git a/src/sys/dune b/src/sys/dune index 9756f4414..bac13a868 100644 --- a/src/sys/dune +++ b/src/sys/dune @@ -1,22 +1,10 @@ ;; Test of the Sys library -;; this prevents the tests from running on a default build - -(alias - (name default) - (package multicoretests) - (deps stm_tests.exe)) - -(executable +(test (name stm_tests) (modules stm_tests) - (libraries qcheck-stm.sequential qcheck-stm.domain) - (preprocess - (pps ppx_deriving.show))) - -(rule - (alias runtest) (package multicoretests) - (deps stm_tests.exe) - (action - (run ./%{deps} --verbose))) + (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 index a3b089329..4ead5a7fe 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -1,5 +1,5 @@ open QCheck -open STM_base +open STM module SConf = struct @@ -28,14 +28,14 @@ struct let arb_cmd _s = let name_gen = Gen.(oneofl ["aaa" ; "bbb" ; "ccc" ; "ddd" ; "eee"]) in let path_gen = Gen.map (fun path -> path) (Gen.list_size (Gen.int_bound 5) name_gen) in (* can be empty *) - let perm_gen = Gen.(oneofl [0o777]) in + let perm_gen = Gen.return 0o777 in QCheck.make ~print:show_cmd Gen.(oneof [ - map (fun path -> File_exists (path)) path_gen ; + map (fun path -> File_exists path) path_gen ; map3 (fun path new_dir_name perm -> Mkdir (path, new_dir_name, perm)) path_gen name_gen perm_gen; map2 (fun path delete_dir_name -> Rmdir (path, delete_dir_name)) path_gen name_gen; - map (fun path -> Readdir (path)) path_gen; + map (fun path -> Readdir path) path_gen; map3 (fun path new_file_name perm -> Touch (path, new_file_name, perm)) path_gen name_gen perm_gen; ]) @@ -43,25 +43,25 @@ struct let init_state = Directory {perm = 0o777; fs_map = Map_names.empty} - let rec find_opt fs path = + let rec find_opt_model fs path = match fs with | File f -> if path = [] then Some (File f) 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)) + (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 fs path = find_opt fs path <> None + let mem_model fs path = find_opt_model fs path <> None - let rec mkdir fs path new_dir_name perm = + let rec mkdir_model fs path new_dir_name perm = match fs with - | File _ -> fs + | File _ -> fs | Directory d -> (match path with | [] -> @@ -69,9 +69,9 @@ struct Directory {d with 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 + | None -> fs | Some sub_fs -> - let nfs = mkdir sub_fs tl_path new_dir_name perm in + let nfs = mkdir_model sub_fs tl_path new_dir_name perm in if nfs = sub_fs then fs else @@ -79,15 +79,15 @@ struct let new_map = Map_names.add next_in_path nfs new_map in Directory {d with fs_map = new_map})) - let readdir fs path = - match find_opt fs path with + let readdir_model fs path = + match find_opt_model fs path with | None -> None | Some fs -> - match fs with + (match fs with | File _ -> None - | Directory d -> Some (Map_names.fold (fun k _ l -> l @ [k]) d.fs_map []) + | Directory d -> Some (Map_names.fold (fun k _ l -> k::l) d.fs_map [])) - let rec rmdir fs path delete_dir_name = + let rec rmdir_model fs path delete_dir_name = match fs with | File _ -> fs | Directory d -> @@ -101,13 +101,12 @@ struct (match Map_names.find_opt next_in_path d.fs_map with | None -> fs | Some sub_fs -> - let nfs = rmdir sub_fs tl_path delete_dir_name in + let nfs = rmdir_model sub_fs tl_path delete_dir_name in if nfs = sub_fs then fs - else - Directory {d with fs_map = (update_map_name d.fs_map next_in_path nfs)})) + else Directory {d with fs_map = (update_map_name d.fs_map next_in_path nfs)})) - let rec touch fs path new_file_name perm = + let rec touch_model fs path new_file_name perm = match fs with | File _ -> fs | Directory d -> @@ -119,36 +118,32 @@ struct (match Map_names.find_opt next_in_path d.fs_map with | None -> fs | Some sub_fs -> - let nfs = touch sub_fs tl_path new_file_name perm in + let nfs = touch_model sub_fs tl_path new_file_name perm in if nfs = sub_fs then fs - else - Directory {d with fs_map = update_map_name d.fs_map next_in_path nfs})) + else Directory {d with fs_map = update_map_name d.fs_map next_in_path nfs})) let next_state c fs = match c with - | File_exists (_path) -> fs + | File_exists _path -> fs | Mkdir (path, new_dir_name, perm) -> - if mem fs (path @ [new_dir_name]) + if mem_model fs (path @ [new_dir_name]) then fs - else mkdir fs path new_dir_name perm + else mkdir_model fs path new_dir_name perm | Rmdir (path,delete_dir_name) -> - if mem fs (path @ [delete_dir_name]) - then rmdir fs 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 | Touch (path, new_file_name, perm) -> - if mem fs (path @ [new_file_name]) + if mem_model fs (path @ [new_file_name]) then fs - else touch fs path new_file_name perm + else touch_model fs path new_file_name perm let init_sut () = match Sys.os_type with - | "Unix" -> ignore (Sys.command ("rm -rf " ^ (static_path / "sandbox_root") ^ " && mkdir " ^ (static_path / "sandbox_root"))) - | "Win32" -> - ignore (Sys.command ( - "powershell -Command \"Remove-Item -Path " ^ (static_path / "sandbox_root") ^ " -Recurse -Force -ErrorAction Ignore \" - & mkdir " ^ (static_path / "sandbox_root"))) + | "Unix" -> ignore (Sys.command ("mkdir " ^ (static_path / "sandbox_root"))) + | "Win32" -> ignore (Sys.command ("mkdir " ^ (static_path / "sandbox_root"))) | v -> failwith ("Sys tests not working with " ^ v) let cleanup _ = @@ -163,71 +158,73 @@ struct let run c _file_name = match c with - | File_exists (path) -> Res (bool, Sys.file_exists (p path)) + | File_exists path -> Res (bool, Sys.file_exists (p path)) | Mkdir (path, new_dir_name, perm) -> Res (result unit exn, protect (Sys.mkdir ((p path) / new_dir_name)) perm) | Rmdir (path, delete_dir_name) -> Res (result unit exn, protect (Sys.rmdir) ((p path) / delete_dir_name)) - | Readdir (path) -> + | Readdir path -> Res (result (array string) exn, protect (Sys.readdir) (p path)) | Touch (path, new_file_name, _perm) -> - (match Sys.os_type with - | "Unix" -> Res (unit, ignore(Sys.command ("touch " ^ (p path) / new_file_name ^ " 2>/dev/null"))) - | "Win32" -> Res (unit, ignore(Sys.command ("type nul >> \"" ^ (p path / new_file_name) ^ "\""))) - | v -> failwith ("Sys tests not working with " ^ v)) + (match Sys.os_type with + | "Unix" -> Res (int, Sys.command ("touch " ^ (p path) / new_file_name ^ " 2>/dev/null")) + | "Win32" -> Res (int, Sys.command ("type nul >> \"" ^ (p path / new_file_name) ^ "\"")) + | v -> failwith ("Sys tests not working with " ^ v)) let fs_is_a_dir fs = match fs with | Directory _ -> true | File _ -> false let path_is_a_dir fs path = - match find_opt fs path with + 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 fs path + | File_exists path, Res ((Bool,_),b) -> b = mem_model fs path | Mkdir (path, new_dir_name, _perm), 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 fs complete_path) || - (s = (p complete_path) ^ ": No such file or directory" && not (mem fs path)) || - (s = (p complete_path) ^ ": Not a directory" && not (path_is_a_dir fs complete_path)) - | _ -> false) - | Ok () -> not (mem fs complete_path) && mem fs path && path_is_a_dir fs path) + | 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" && not (mem_model fs path)) || + (s = (p complete_path) ^ ": Not a directory" && not (path_is_a_dir fs complete_path)) + | _ -> 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) ^ ": Directory not empty" && not (readdir fs complete_path = Some [])) || - (s = (p complete_path) ^ ": No such file or directory" && not (mem fs complete_path)) || - (s = (p complete_path) ^ ": Not a directory" && not (path_is_a_dir fs complete_path)) - | _ -> false) - | Ok () -> - let is_empty = readdir fs complete_path = Some [] in - mem fs complete_path && is_empty && path_is_a_dir fs complete_path) - | Readdir (path), Res ((Result (Array String,Exn),_), res) -> + | Error err -> + (match err with + | Sys_error s -> + (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) ^ ": Not a directory" && not (path_is_a_dir fs complete_path)) + | _ -> 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 fs path)) || - (s = (p path) ^ ": Not a directory" && not (path_is_a_dir fs path)) - | _ -> false) - | Ok array_of_subdir -> - let sut = List.sort (fun a b -> -(String.compare a b)) (Array.to_list array_of_subdir) in - let same_result = - (match readdir fs path with - | None -> false - | Some l -> List.sort (fun a b -> -(String.compare a b)) l = sut) in - same_result && mem fs path && path_is_a_dir fs path) - | Touch (_path, _new_dir_name, _perm), Res ((Unit,_),_) -> true + | 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) ^ ": Not a directory" && not (path_is_a_dir fs path)) + | _ -> false) + | Ok array_of_subdir -> + 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))) + | Touch (path, _new_file_name, _perm), Res ((Int,_),n) -> + if n = 0 + then (mem_model fs path && path_is_a_dir fs path) + else (not (mem_model fs path) || not (path_is_a_dir fs path)) | _,_ -> false end @@ -236,6 +233,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"; - Sys_dom.agree_test_par ~count:100 ~name:"STM Sys test parallel" + Sys_seq.agree_test ~count:1000 ~name:"STM Sys test sequential"; + Sys_dom.agree_test_par ~count:200 ~name:"STM Sys test parallel" ] From 06ce34ddb3402c4a13656cbaa6a197f7746c6cc9 Mon Sep 17 00:00:00 2001 From: Lucccyo Date: Wed, 21 Dec 2022 10:42:53 +0100 Subject: [PATCH 06/33] temporary fixing mingW Windows bug --- src/sys/stm_tests.ml | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 4ead5a7fe..4358d3dcf 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -215,12 +215,16 @@ struct (s = (p path) ^ ": Not a directory" && not (path_is_a_dir fs path)) | _ -> false) | Ok array_of_subdir -> - 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))) + (* 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)))) | Touch (path, _new_file_name, _perm), Res ((Int,_),n) -> if n = 0 then (mem_model fs path && path_is_a_dir fs path) From 36bfaa2793489d1fee45633b74bf986d01f35d1f Mon Sep 17 00:00:00 2001 From: Lucccyo Date: Thu, 22 Dec 2022 11:23:36 +0100 Subject: [PATCH 07/33] separate error messages between unix and win32 --- src/sys/stm_tests.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 4358d3dcf..7530d1f9c 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -201,7 +201,9 @@ struct | Sys_error s -> (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) ^ ": Not a directory" && not (path_is_a_dir 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 []) @@ -212,7 +214,9 @@ struct | Sys_error s -> (s = (p path) ^ ": Permission denied") || (s = (p path) ^ ": No such file or directory" && not (mem_model fs path)) || - (s = (p path) ^ ": Not a directory" && not (path_is_a_dir 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 *) From 8f7442e2afc0142cf8214d5a3af112c953710dcc Mon Sep 17 00:00:00 2001 From: Lucccyo Date: Thu, 22 Dec 2022 13:20:54 +0100 Subject: [PATCH 08/33] [TRY] fix error handling from Win32 on mkdir (not a directory => no such file or directory) --- src/sys/stm_tests.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 7530d1f9c..0f8b8e3fa 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -190,7 +190,9 @@ struct (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" && not (mem_model fs path)) || - (s = (p complete_path) ^ ": Not a directory" && not (path_is_a_dir fs complete_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) -> From 0f40582731f4d405349e34316609dc0c1c9ff27a Mon Sep 17 00:00:00 2001 From: Lucccyo Date: Thu, 22 Dec 2022 16:55:58 +0100 Subject: [PATCH 09/33] modifying touch - need to know how windows manage --- src/sys/stm_tests.ml | 11 ++++++++--- 1 file changed, 8 insertions(+), 3 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 0f8b8e3fa..c67118733 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -231,10 +231,15 @@ struct | Some l -> List.sort String.compare l = List.sort String.compare (Array.to_list array_of_subdir)))) - | Touch (path, _new_file_name, _perm), Res ((Int,_),n) -> + | Touch (path, new_file_name, _perm), Res ((Int,_),n) -> + let complete_path = (path @ [new_file_name]) in if n = 0 - then (mem_model fs path && path_is_a_dir fs path) - else (not (mem_model fs path) || not (path_is_a_dir fs path)) + then ( + (* temporary : waiting to see how windows manage that *) + (mem_model fs path && path_is_a_dir fs path && not (mem_model fs complete_path)) || + mem_model fs complete_path + ) + else (not (mem_model fs path) || not (path_is_a_dir fs path)) (* the path is incorrect*) | _,_ -> false end From c7c4c01351c2673f211f4aa727577b54685b7731 Mon Sep 17 00:00:00 2001 From: Lucccyo Date: Wed, 28 Dec 2022 11:50:10 +0100 Subject: [PATCH 10/33] track windows error --- src/sys/stm_tests.ml | 16 +++++++++------- 1 file changed, 9 insertions(+), 7 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index c67118733..578bbbc89 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -233,13 +233,15 @@ struct = List.sort String.compare (Array.to_list array_of_subdir)))) | Touch (path, new_file_name, _perm), Res ((Int,_),n) -> let complete_path = (path @ [new_file_name]) in - if n = 0 - then ( - (* temporary : waiting to see how windows manage that *) - (mem_model fs path && path_is_a_dir fs path && not (mem_model fs complete_path)) || - mem_model fs complete_path - ) - else (not (mem_model fs path) || not (path_is_a_dir fs path)) (* the path is incorrect*) + if Sys.win32 + then (Format.printf "%d\n" n; true) + else + if n = 0 + then ( + (mem_model fs path && path_is_a_dir fs path && not (mem_model fs complete_path)) || + mem_model fs complete_path + ) + else (not (mem_model fs path) || not (path_is_a_dir fs path)) (* the path is incorrect*) | _,_ -> false end From c953955573cf7df2991088064f6b07eedc55919f Mon Sep 17 00:00:00 2001 From: Lucccyo Date: Wed, 28 Dec 2022 15:28:02 +0100 Subject: [PATCH 11/33] separate OS --- src/sys/stm_tests.ml | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 578bbbc89..73e22b943 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -234,7 +234,14 @@ struct | Touch (path, new_file_name, _perm), Res ((Int,_),n) -> let complete_path = (path @ [new_file_name]) in if Sys.win32 - then (Format.printf "%d\n" n; true) + then ( + if n = 0 + then ( + (mem_model fs path && path_is_a_dir fs path && not (mem_model fs complete_path)) || + mem_model fs complete_path + ) + else (not (mem_model fs path) || not (path_is_a_dir fs path)) (* the path is incorrect*) + ) else if n = 0 then ( From 192d6a2cf60e92a71af0e8dcfc99f04e661cd27c Mon Sep 17 00:00:00 2001 From: Lucccyo Date: Tue, 3 Jan 2023 10:34:13 +0100 Subject: [PATCH 12/33] make touch's postcond 'true' bc it is not a feature tested --- src/sys/stm_tests.ml | 19 +------------------ 1 file changed, 1 insertion(+), 18 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 73e22b943..78379fc96 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -231,24 +231,7 @@ struct | Some l -> List.sort String.compare l = List.sort String.compare (Array.to_list array_of_subdir)))) - | Touch (path, new_file_name, _perm), Res ((Int,_),n) -> - let complete_path = (path @ [new_file_name]) in - if Sys.win32 - then ( - if n = 0 - then ( - (mem_model fs path && path_is_a_dir fs path && not (mem_model fs complete_path)) || - mem_model fs complete_path - ) - else (not (mem_model fs path) || not (path_is_a_dir fs path)) (* the path is incorrect*) - ) - else - if n = 0 - then ( - (mem_model fs path && path_is_a_dir fs path && not (mem_model fs complete_path)) || - mem_model fs complete_path - ) - else (not (mem_model fs path) || not (path_is_a_dir fs path)) (* the path is incorrect*) + | Touch (_path, _new_file_name, _perm), Res ((Int,_),_) -> true | _,_ -> false end From e1914c53a965a3556609c19a67081479f815df9f Mon Sep 17 00:00:00 2001 From: Lucccyo Date: Tue, 3 Jan 2023 13:57:42 +0100 Subject: [PATCH 13/33] separate para tests for unix based and negative para tests for windows --- 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 78379fc96..eb49acee2 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -240,6 +240,8 @@ module Sys_dom = STM_domain.Make(SConf) ;; QCheck_base_runner.run_tests_main [ - Sys_seq.agree_test ~count:1000 ~name:"STM Sys test sequential"; - Sys_dom.agree_test_par ~count:200 ~name:"STM Sys test parallel" + Sys_seq.agree_test ~count:1000 ~name:"STM Sys test sequential"; + if Sys.win32 + then Sys_dom.neg_agree_test_par ~count:1000 ~name:"STM Sys test parallel" + else Sys_dom.agree_test_par ~count:1000 ~name:"STM Sys test parallel" ] From ac12bd4b2510706534d3bf64a7dcb6c6cc7f09f2 Mon Sep 17 00:00:00 2001 From: Lucccyo Date: Thu, 5 Jan 2023 15:47:40 +0100 Subject: [PATCH 14/33] put negative tests to Windows and MacOS machine --- src/sys/stm_tests.ml | 12 +++++++++--- 1 file changed, 9 insertions(+), 3 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index eb49acee2..13cd2da7f 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -235,13 +235,19 @@ struct | _,_ -> false end +let uname_os () = + let ic = Unix.open_process_in "uname -s" in + let os = In_channel.input_line ic in + In_channel.close 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.win32 - then Sys_dom.neg_agree_test_par ~count:1000 ~name:"STM Sys test parallel" - else Sys_dom.agree_test_par ~count:1000 ~name:"STM Sys test parallel" + 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" ] From ab83b4cd1ece0b10338dca415ca5802247d7a95f Mon Sep 17 00:00:00 2001 From: Lucccyo Date: Fri, 6 Jan 2023 12:20:21 +0100 Subject: [PATCH 15/33] update path generator, 50% to generate an existing path, 50% to generate random one --- src/sys/stm_tests.ml | 18 ++++++++++++++++-- 1 file changed, 16 insertions(+), 2 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 13cd2da7f..e9a050e48 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -25,9 +25,23 @@ struct let update_map_name map_name k v = Map_names.add k v (Map_names.remove k map_name) - let arb_cmd _s = + (* var gen_existing_path : filesys -> string list 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)] + ) + ) + + let arb_cmd s = let name_gen = Gen.(oneofl ["aaa" ; "bbb" ; "ccc" ; "ddd" ; "eee"]) in - let path_gen = Gen.map (fun path -> path) (Gen.list_size (Gen.int_bound 5) name_gen) in (* can be empty *) + let path_gen = Gen.oneof [gen_existing_path s; Gen.list_size (Gen.int_bound 5) name_gen] in (* can be empty *) let perm_gen = Gen.return 0o777 in QCheck.make ~print:show_cmd Gen.(oneof From 8b9c2675e91f04b5ebbeebff4b4fd2f22d5dd140 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Sat, 7 Jan 2023 00:12:31 +0100 Subject: [PATCH 16/33] whitespace changes --- src/sys/stm_tests.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index e9a050e48..dab22ade9 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -29,10 +29,10 @@ struct let rec gen_existing_path fs = match fs with | File _ -> Gen.return [] - | Directory d -> + | Directory d -> (match Map_names.bindings d.fs_map with | [] -> Gen.return [] - | bindings -> Gen.(oneofl bindings >>= fun (n, sub_fs) -> + | bindings -> Gen.(oneofl bindings >>= fun (n, sub_fs) -> Gen.oneof [ Gen.return [n]; Gen.map (fun l -> n::l) (gen_existing_path sub_fs)] @@ -260,8 +260,8 @@ 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" + 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" ] From 0e1a64c04923cdc55a9275383f0785bffbf22dc2 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Sat, 7 Jan 2023 00:16:16 +0100 Subject: [PATCH 17/33] attempt to clean-up Windows CI logs by silencing its stderr --- src/sys/stm_tests.ml | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index dab22ade9..35d88f3b4 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -154,6 +154,12 @@ struct then fs else touch_model fs path new_file_name perm + let sys_command_silent cmd = + let stdout,stdin,stderr = Unix.open_process_full cmd [||] in + In_channel.close stdout; + Out_channel.close stdin; + In_channel.close stderr + let init_sut () = match Sys.os_type with | "Unix" -> ignore (Sys.command ("mkdir " ^ (static_path / "sandbox_root"))) @@ -163,7 +169,7 @@ struct let cleanup _ = match Sys.os_type with | "Unix" -> ignore (Sys.command ("rm -rf " ^ (static_path / "sandbox_root"))) - | "Win32" -> ignore (Sys.command ("powershell -Command \"Remove-Item '" ^ (static_path / "sandbox_root") ^ "' -Recurse -Force\"")) + | "Win32" -> sys_command_silent ("powershell -Command \"Remove-Item '" ^ (static_path / "sandbox_root") ^ "' -Recurse -Force\"") | v -> failwith ("Sys tests not working with " ^ v) let precond _c _s = true @@ -181,8 +187,8 @@ struct Res (result (array string) exn, protect (Sys.readdir) (p path)) | Touch (path, new_file_name, _perm) -> (match Sys.os_type with - | "Unix" -> Res (int, Sys.command ("touch " ^ (p path) / new_file_name ^ " 2>/dev/null")) - | "Win32" -> Res (int, Sys.command ("type nul >> \"" ^ (p path / new_file_name) ^ "\"")) + | "Unix" -> Res (unit, ignore (Sys.command ("touch " ^ (p path) / new_file_name ^ " 2>/dev/null"))) + | "Win32" -> Res (unit, sys_command_silent ("type nul >> \"" ^ (p path / new_file_name) ^ "\"")) | v -> failwith ("Sys tests not working with " ^ v)) let fs_is_a_dir fs = match fs with | Directory _ -> true | File _ -> false @@ -245,7 +251,7 @@ struct | Some l -> List.sort String.compare l = List.sort String.compare (Array.to_list array_of_subdir)))) - | Touch (_path, _new_file_name, _perm), Res ((Int,_),_) -> true + | Touch (_path, _new_file_name, _perm), Res ((Unit,_),_) -> true | _,_ -> false end From 79054f06efacc79871e658cb38202065873442c3 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Sat, 7 Jan 2023 00:52:16 +0100 Subject: [PATCH 18/33] pass environment --- src/sys/stm_tests.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 35d88f3b4..e0d924cb5 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -154,8 +154,10 @@ struct then fs else touch_model fs path new_file_name perm + let env = Unix.environment () + let sys_command_silent cmd = - let stdout,stdin,stderr = Unix.open_process_full cmd [||] in + let stdout,stdin,stderr = Unix.open_process_full cmd env in In_channel.close stdout; Out_channel.close stdin; In_channel.close stderr From df59d779ab60e4f76a1ebc42e3d44fbffdd5a983 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Sat, 7 Jan 2023 01:19:25 +0100 Subject: [PATCH 19/33] try redirecting output instead --- src/sys/stm_tests.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index e0d924cb5..0b0a07ee4 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -153,7 +153,7 @@ struct if mem_model fs (path @ [new_file_name]) then fs else touch_model fs path new_file_name perm - +(* let env = Unix.environment () let sys_command_silent cmd = @@ -161,7 +161,7 @@ struct In_channel.close stdout; Out_channel.close stdin; In_channel.close stderr - +*) let init_sut () = match Sys.os_type with | "Unix" -> ignore (Sys.command ("mkdir " ^ (static_path / "sandbox_root"))) @@ -171,7 +171,7 @@ struct let cleanup _ = match Sys.os_type with | "Unix" -> ignore (Sys.command ("rm -rf " ^ (static_path / "sandbox_root"))) - | "Win32" -> sys_command_silent ("powershell -Command \"Remove-Item '" ^ (static_path / "sandbox_root") ^ "' -Recurse -Force\"") + | "Win32" -> ignore (Sys.command ("powershell -Command \"Remove-Item '" ^ (static_path / "sandbox_root") ^ "' -Recurse -Force\" > nul 2>&1")) | v -> failwith ("Sys tests not working with " ^ v) let precond _c _s = true @@ -190,7 +190,7 @@ struct | Touch (path, new_file_name, _perm) -> (match Sys.os_type with | "Unix" -> Res (unit, ignore (Sys.command ("touch " ^ (p path) / new_file_name ^ " 2>/dev/null"))) - | "Win32" -> Res (unit, sys_command_silent ("type nul >> \"" ^ (p path / new_file_name) ^ "\"")) + | "Win32" -> Res (unit, ignore (Sys.command ("type nul >> \"" ^ (p path / new_file_name) ^ "\" > nul 2>&1"))) | v -> failwith ("Sys tests not working with " ^ v)) let fs_is_a_dir fs = match fs with | Directory _ -> true | File _ -> false From d0e425a9e1d1f56340db935e50672332e729b1f1 Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Wed, 11 Jan 2023 10:27:57 +0100 Subject: [PATCH 20/33] Compute the sandbox root only once --- src/sys/stm_tests.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 0b0a07ee4..9b1c22043 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -53,7 +53,7 @@ struct map3 (fun path new_file_name perm -> Touch (path, new_file_name, perm)) path_gen name_gen perm_gen; ]) - let static_path = Sys.getcwd () + let sandbox_root = Sys.getcwd () / "sandbox" let init_state = Directory {perm = 0o777; fs_map = Map_names.empty} @@ -164,19 +164,19 @@ struct *) let init_sut () = match Sys.os_type with - | "Unix" -> ignore (Sys.command ("mkdir " ^ (static_path / "sandbox_root"))) - | "Win32" -> ignore (Sys.command ("mkdir " ^ (static_path / "sandbox_root"))) + | "Unix" -> ignore (Sys.command ("mkdir " ^ sandbox_root)) + | "Win32" -> ignore (Sys.command ("mkdir " ^ sandbox_root)) | v -> failwith ("Sys tests not working with " ^ v) let cleanup _ = match Sys.os_type with - | "Unix" -> ignore (Sys.command ("rm -rf " ^ (static_path / "sandbox_root"))) - | "Win32" -> ignore (Sys.command ("powershell -Command \"Remove-Item '" ^ (static_path / "sandbox_root") ^ "' -Recurse -Force\" > nul 2>&1")) + | "Unix" -> ignore (Sys.command ("rm -rf " ^ sandbox_root)) + | "Win32" -> ignore (Sys.command ("powershell -Command \"Remove-Item '" ^ sandbox_root ^ "' -Recurse -Force\" > nul 2>&1")) | v -> failwith ("Sys tests not working with " ^ v) let precond _c _s = true - let p path = (List.fold_left (/) (static_path / "sandbox_root") path) + let p path = (List.fold_left (/) sandbox_root path) let run c _file_name = match c with From 573fb27a4e63b27febae9e696ccc6d7bd5c5933b Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Wed, 11 Jan 2023 10:47:26 +0100 Subject: [PATCH 21/33] Use Map.Make.update to update the Map_names This could allow for some more sharing, when k is already mapped to v --- 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 9b1c22043..2cb19b61e 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -23,7 +23,7 @@ struct let (/) = Filename.concat - let update_map_name map_name k v = Map_names.add k v (Map_names.remove k map_name) + let update_map_name map_name k v = Map_names.update k (fun _ -> Some v) map_name (* var gen_existing_path : filesys -> string list Gen.t *) let rec gen_existing_path fs = From 8030e743fedc211333653c990498b31b2683cfd5 Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Wed, 11 Jan 2023 11:18:25 +0100 Subject: [PATCH 22/33] Use Sys.mkdir with safer permissions for the sandbox root Use Sys.mkdir instead of Sys.command "mkdir"... to create the sandbox to avoid discrepancies between OSes This also allows to set safer permissions, by restricting access to the sandbox to the user running the test --- src/sys/stm_tests.ml | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 2cb19b61e..e76591efc 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -55,7 +55,7 @@ struct let sandbox_root = Sys.getcwd () / "sandbox" - let init_state = Directory {perm = 0o777; fs_map = Map_names.empty} + let init_state = Directory {perm = 0o700; fs_map = Map_names.empty} let rec find_opt_model fs path = match fs with @@ -163,10 +163,8 @@ struct In_channel.close stderr *) let init_sut () = - match Sys.os_type with - | "Unix" -> ignore (Sys.command ("mkdir " ^ sandbox_root)) - | "Win32" -> ignore (Sys.command ("mkdir " ^ sandbox_root)) - | v -> failwith ("Sys tests not working with " ^ v) + try Sys.mkdir sandbox_root 0o700 + with Sys_error msg when msg = sandbox_root ^ ": File exists" -> () let cleanup _ = match Sys.os_type with From 9e5454ce42ce1b7be5b05570dc441a0918e5e88d Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Wed, 11 Jan 2023 11:54:54 +0100 Subject: [PATCH 23/33] Use safer removal commands Use Filename.quote to ensure that the sandbox is properly quoted before invoking Sys.command On windows, use the simple 'rd' command instead of calling powershell (which would require double-quoting, we should probably avoid that) On unix, use 'rm -r' instead of 'rm -rf' since, at the moment, '-f' should not be required --- 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 e76591efc..99bfe60fa 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -168,8 +168,8 @@ struct let cleanup _ = match Sys.os_type with - | "Unix" -> ignore (Sys.command ("rm -rf " ^ sandbox_root)) - | "Win32" -> ignore (Sys.command ("powershell -Command \"Remove-Item '" ^ sandbox_root ^ "' -Recurse -Force\" > nul 2>&1")) + | "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 From 23faa613ddc988a84b0741b51e67273bcdf955a1 Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Wed, 11 Jan 2023 12:11:47 +0100 Subject: [PATCH 24/33] Remove all permissions Since the generated permissions were always the same and that it is probably an aspect that is quite different between Unix and Windows, remove them for now --- src/sys/stm_tests.ml | 75 ++++++++++++++++++++++---------------------- 1 file changed, 37 insertions(+), 38 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 99bfe60fa..b07ab48da 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -5,17 +5,17 @@ module SConf = struct type cmd = | File_exists of string list - | Mkdir of string list * string * int + | Mkdir of string list * string | Rmdir of string list * string | Readdir of string list - | Touch of string list * string * int + | Touch of string list * string [@@deriving show { with_path = false }] module Map_names = Map.Make (String) type filesys = - | Directory of {perm: int; fs_map: filesys Map_names.t} - | File of {perm: int} + | Directory of {fs_map: filesys Map_names.t} + | File type state = filesys @@ -28,7 +28,7 @@ struct (* var gen_existing_path : filesys -> string list Gen.t *) let rec gen_existing_path fs = match fs with - | File _ -> Gen.return [] + | File -> Gen.return [] | Directory d -> (match Map_names.bindings d.fs_map with | [] -> Gen.return [] @@ -42,26 +42,25 @@ struct let arb_cmd s = let name_gen = Gen.(oneofl ["aaa" ; "bbb" ; "ccc" ; "ddd" ; "eee"]) in let path_gen = Gen.oneof [gen_existing_path s; Gen.list_size (Gen.int_bound 5) name_gen] in (* can be empty *) - let perm_gen = Gen.return 0o777 in QCheck.make ~print:show_cmd Gen.(oneof [ map (fun path -> File_exists path) path_gen ; - map3 (fun path new_dir_name perm -> Mkdir (path, new_dir_name, perm)) path_gen name_gen perm_gen; + map2 (fun path new_dir_name -> Mkdir (path, new_dir_name)) path_gen name_gen; map2 (fun path delete_dir_name -> Rmdir (path, delete_dir_name)) path_gen name_gen; map (fun path -> Readdir path) path_gen; - map3 (fun path new_file_name perm -> Touch (path, new_file_name, perm)) path_gen name_gen perm_gen; + map2 (fun path new_file_name -> Touch (path, new_file_name)) path_gen name_gen; ]) let sandbox_root = Sys.getcwd () / "sandbox" - let init_state = Directory {perm = 0o700; fs_map = Map_names.empty} + let init_state = Directory {fs_map = Map_names.empty} let rec find_opt_model fs path = match fs with - | File f -> + | File -> if path = [] - then Some (File f) + then Some fs else None | Directory d -> (match path with @@ -73,44 +72,44 @@ struct let mem_model fs path = find_opt_model fs path <> None - let rec mkdir_model fs path new_dir_name perm = + let rec mkdir_model fs path new_dir_name = match fs with - | File _ -> fs + | File -> fs | Directory d -> (match path with | [] -> - let new_dir = Directory {perm; fs_map = Map_names.empty} in - Directory {d with fs_map = Map_names.add new_dir_name new_dir d.fs_map} + 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 perm in + 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 {d with fs_map = new_map})) + 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 + | 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 + | 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 {d with fs_map = Map_names.remove delete_dir_name d.fs_map} - | None | Some (File _) | Some (Directory _) -> fs) + 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 @@ -118,41 +117,41 @@ struct let nfs = rmdir_model sub_fs tl_path delete_dir_name in if nfs = sub_fs then fs - else Directory {d with fs_map = (update_map_name d.fs_map next_in_path nfs)})) + else Directory {fs_map = (update_map_name d.fs_map next_in_path nfs)})) - let rec touch_model fs path new_file_name perm = + let rec touch_model fs path new_file_name = match fs with - | File _ -> fs + | File -> fs | Directory d -> (match path with | [] -> - let new_file = File {perm} in - Directory {d with fs_map = Map_names.add new_file_name new_file d.fs_map} + 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 = touch_model sub_fs tl_path new_file_name perm in + let nfs = touch_model sub_fs tl_path new_file_name in if nfs = sub_fs then fs - else Directory {d with fs_map = update_map_name d.fs_map next_in_path nfs})) + 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, perm) -> + | Mkdir (path, new_dir_name) -> if mem_model fs (path @ [new_dir_name]) then fs - else mkdir_model fs path new_dir_name perm + 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 - | Touch (path, new_file_name, perm) -> + | Touch (path, new_file_name) -> if mem_model fs (path @ [new_file_name]) then fs - else touch_model fs path new_file_name perm + else touch_model fs path new_file_name (* let env = Unix.environment () @@ -179,19 +178,19 @@ struct let run c _file_name = match c with | File_exists path -> Res (bool, Sys.file_exists (p path)) - | Mkdir (path, new_dir_name, perm) -> - Res (result unit exn, protect (Sys.mkdir ((p path) / new_dir_name)) perm) + | 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)) - | Touch (path, new_file_name, _perm) -> + | Touch (path, new_file_name) -> (match Sys.os_type with | "Unix" -> Res (unit, ignore (Sys.command ("touch " ^ (p path) / new_file_name ^ " 2>/dev/null"))) | "Win32" -> Res (unit, ignore (Sys.command ("type nul >> \"" ^ (p path / new_file_name) ^ "\" > nul 2>&1"))) | v -> failwith ("Sys tests not working with " ^ v)) - let fs_is_a_dir fs = match fs with | Directory _ -> true | File _ -> false + 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 @@ -201,7 +200,7 @@ struct 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, _perm), Res ((Result (Unit,Exn),_), res) -> + | Mkdir (path, new_dir_name), Res ((Result (Unit,Exn),_), res) -> let complete_path = (path @ [new_dir_name]) in (match res with | Error err -> @@ -251,7 +250,7 @@ struct | Some l -> List.sort String.compare l = List.sort String.compare (Array.to_list array_of_subdir)))) - | Touch (_path, _new_file_name, _perm), Res ((Unit,_),_) -> true + | Touch (_path, _new_file_name), Res ((Unit,_),_) -> true | _,_ -> false end From 670f395d93e1a33a8bee554b83f54e2c5eb4966a Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Thu, 12 Jan 2023 13:37:42 +0100 Subject: [PATCH 25/33] Use 'echo' to implement Touch on all OSes Change the implementation of Touch so that the behaviours are similar on Unix and Windows: by using an 'echo . > file' on all platforms, it will uniformly fail when Touch is attempted on an existing directory --- src/sys/stm_tests.ml | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index b07ab48da..4f33f7e27 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -185,10 +185,17 @@ struct | Readdir path -> Res (result (array string) exn, protect (Sys.readdir) (p path)) | Touch (path, new_file_name) -> - (match Sys.os_type with - | "Unix" -> Res (unit, ignore (Sys.command ("touch " ^ (p path) / new_file_name ^ " 2>/dev/null"))) - | "Win32" -> Res (unit, ignore (Sys.command ("type nul >> \"" ^ (p path / new_file_name) ^ "\" > nul 2>&1"))) - | v -> failwith ("Sys tests not working with " ^ v)) + let void = match Sys.os_type with + | "Unix" -> "/dev/null" + | "Win32" -> "nul" + | v -> failwith ("Sys tests not working with " ^ v) + in + (* Even if the command is called Touch, we use the actual + command echo so that we obtain the same behaviour under + unix and windows when the target is an existing directory + (rather than a regular file) *) + let cmd = Printf.sprintf "echo . > %s 2> %s" (Filename.quote (p path / new_file_name)) void in + Res (unit, ignore (Sys.command cmd)) let fs_is_a_dir fs = match fs with | Directory _ -> true | File -> false From 1f42255111ffd39dc296c2e1e599b67d48358621 Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Thu, 12 Jan 2023 13:40:39 +0100 Subject: [PATCH 26/33] Use a type `path` to clarify `cmd` signature --- src/sys/stm_tests.ml | 14 ++++++++------ 1 file changed, 8 insertions(+), 6 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 4f33f7e27..a4236b0c6 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -3,12 +3,14 @@ open STM module SConf = struct + type path = string list [@@deriving show] + type cmd = - | File_exists of string list - | Mkdir of string list * string - | Rmdir of string list * string - | Readdir of string list - | Touch of string list * string + | File_exists of path + | Mkdir of path * string + | Rmdir of path * string + | Readdir of path + | Touch of path * string [@@deriving show { with_path = false }] module Map_names = Map.Make (String) @@ -25,7 +27,7 @@ struct let update_map_name map_name k v = Map_names.update k (fun _ -> Some v) map_name - (* var gen_existing_path : filesys -> string list Gen.t *) + (* var gen_existing_path : filesys -> path Gen.t *) let rec gen_existing_path fs = match fs with | File -> Gen.return [] From cd3c5eade37458ce81214a79fe00a5d81d085c22 Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Thu, 12 Jan 2023 15:49:00 +0100 Subject: [PATCH 27/33] Convert Touch into a Mkfile Choose a better name for the command that makes a new regular file Use `Out_channel` instead of a shell command to create such a file Take into account the fact that the creation can fail in postcond, which makes Mkfile fairly similar to Mkdir --- src/sys/stm_tests.ml | 58 +++++++++++++++++++++++++++++--------------- 1 file changed, 39 insertions(+), 19 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index a4236b0c6..fced993d9 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -10,7 +10,7 @@ struct | Mkdir of path * string | Rmdir of path * string | Readdir of path - | Touch of path * string + | Mkfile of path * string [@@deriving show { with_path = false }] module Map_names = Map.Make (String) @@ -51,7 +51,7 @@ struct map2 (fun path new_dir_name -> Mkdir (path, new_dir_name)) path_gen name_gen; map2 (fun path delete_dir_name -> Rmdir (path, delete_dir_name)) path_gen name_gen; map (fun path -> Readdir path) path_gen; - map2 (fun path new_file_name -> Touch (path, new_file_name)) path_gen name_gen; + map2 (fun path new_file_name -> Mkfile (path, new_file_name)) path_gen name_gen; ]) let sandbox_root = Sys.getcwd () / "sandbox" @@ -121,7 +121,7 @@ struct then fs else Directory {fs_map = (update_map_name d.fs_map next_in_path nfs)})) - let rec touch_model fs path new_file_name = + let rec mkfile_model fs path new_file_name = match fs with | File -> fs | Directory d -> @@ -133,7 +133,7 @@ struct (match Map_names.find_opt next_in_path d.fs_map with | None -> fs | Some sub_fs -> - let nfs = touch_model sub_fs tl_path new_file_name in + 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})) @@ -150,10 +150,10 @@ struct then rmdir_model fs path delete_dir_name else fs | Readdir _path -> fs - | Touch (path, new_file_name) -> + | Mkfile (path, new_file_name) -> if mem_model fs (path @ [new_file_name]) then fs - else touch_model fs path new_file_name + else mkfile_model fs path new_file_name (* let env = Unix.environment () @@ -177,6 +177,10 @@ struct 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)) @@ -186,18 +190,8 @@ struct Res (result unit exn, protect (Sys.rmdir) ((p path) / delete_dir_name)) | Readdir path -> Res (result (array string) exn, protect (Sys.readdir) (p path)) - | Touch (path, new_file_name) -> - let void = match Sys.os_type with - | "Unix" -> "/dev/null" - | "Win32" -> "nul" - | v -> failwith ("Sys tests not working with " ^ v) - in - (* Even if the command is called Touch, we use the actual - command echo so that we obtain the same behaviour under - unix and windows when the target is an existing directory - (rather than a regular file) *) - let cmd = Printf.sprintf "echo . > %s 2> %s" (Filename.quote (p path / new_file_name)) void in - Res (unit, ignore (Sys.command cmd)) + | 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 @@ -259,7 +253,33 @@ struct | Some l -> List.sort String.compare l = List.sort String.compare (Array.to_list array_of_subdir)))) - | Touch (_path, _new_file_name), Res ((Unit,_),_) -> true + | 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 From 47e65f46dccdc532f09981eb0b49a316bf159d69 Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Fri, 13 Jan 2023 11:45:30 +0100 Subject: [PATCH 28/33] Use a relative path for the sandbox Instead of using the full absolute path, which makes the logs with counter-examples harder to read, use a simple relative path for the sandbox Change its name from `sandbox` to `_sandbox`, to follow the common usage for generated directories (such as `_build` etc.) --- 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 fced993d9..d6896bada 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -54,7 +54,7 @@ struct map2 (fun path new_file_name -> Mkfile (path, new_file_name)) path_gen name_gen; ]) - let sandbox_root = Sys.getcwd () / "sandbox" + let sandbox_root = "_sandbox" let init_state = Directory {fs_map = Map_names.empty} From 29fb75c4bf8d0912c7fb41d63b6212be38a31aaf Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Fri, 13 Jan 2023 12:22:08 +0100 Subject: [PATCH 29/33] Add other error messages spotted on Windows and macOS --- src/sys/stm_tests.ml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index d6896bada..5c481dbb7 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -211,7 +211,8 @@ struct | 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" && not (mem_model fs 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" @@ -223,6 +224,7 @@ struct | 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 *) From a4f272168bed21af44a0a727c7909ed633c59712 Mon Sep 17 00:00:00 2001 From: Samuel Hym Date: Mon, 16 Jan 2023 10:23:14 +0100 Subject: [PATCH 30/33] Reclaim all resources for the `uname` process The missing `close_process_in` did leave a zombie around for the duration of the test --- 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 5c481dbb7..07fc9932d 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -288,7 +288,7 @@ end let uname_os () = let ic = Unix.open_process_in "uname -s" in let os = In_channel.input_line ic in - In_channel.close ic; + ignore (Unix.close_process_in ic); os module Sys_seq = STM_sequential.Make(SConf) From 4d7900ed1b60e0a4ddc14270ddd7946d6aa2eeff Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Mon, 16 Jan 2023 15:11:47 +0100 Subject: [PATCH 31/33] add pair_gen for generating path and name together --- src/sys/stm_tests.ml | 29 ++++++++++++++++++++++++++--- 1 file changed, 26 insertions(+), 3 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 07fc9932d..033cf73f2 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -41,17 +41,40 @@ struct ) ) + (* 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) -> + Gen.oneof [ + Gen.return (Some ([],n)); + Gen.map (function None -> Some ([],n) + | Some (path,name) -> Some (n::path,name)) (gen_existing_pair sub_fs)] + ) + ) + let arb_cmd s = let name_gen = Gen.(oneofl ["aaa" ; "bbb" ; "ccc" ; "ddd" ; "eee"]) in let path_gen = Gen.oneof [gen_existing_path s; Gen.list_size (Gen.int_bound 5) name_gen] in (* can be empty *) + let fresh_pair_gen = Gen.(pair (list_size (int_bound 5) name_gen)) name_gen in + let pair_gen = + 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)); + ]) in QCheck.make ~print:show_cmd Gen.(oneof [ map (fun path -> File_exists path) path_gen ; - map2 (fun path new_dir_name -> Mkdir (path, new_dir_name)) path_gen name_gen; - map2 (fun path delete_dir_name -> Rmdir (path, delete_dir_name)) path_gen name_gen; + map (fun (path,new_dir_name) -> Mkdir (path, new_dir_name)) pair_gen; + map (fun (path,delete_dir_name) -> Rmdir (path, delete_dir_name)) pair_gen; map (fun path -> Readdir path) path_gen; - map2 (fun path new_file_name -> Mkfile (path, new_file_name)) path_gen name_gen; + map (fun (path,new_file_name) -> Mkfile (path, new_file_name)) pair_gen; ]) let sandbox_root = "_sandbox" From 88ccf15fd8e75cb9d842886aea9b9bc3432bdfac Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Mon, 16 Jan 2023 15:57:00 +0100 Subject: [PATCH 32/33] refactor pair_gen generator --- src/sys/stm_tests.ml | 51 ++++++++++++++++++++++---------------------- 1 file changed, 26 insertions(+), 25 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 033cf73f2..6e4b65e4a 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -47,35 +47,36 @@ struct | Directory d -> (match Map_names.bindings d.fs_map with | [] -> Gen.return None - | bindings -> Gen.(oneofl bindings >>= fun (n, sub_fs) -> - Gen.oneof [ - Gen.return (Some ([],n)); - Gen.map (function None -> Some ([],n) - | Some (path,name) -> Some (n::path,name)) (gen_existing_pair sub_fs)] - ) + | 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 arb_cmd s = - let name_gen = Gen.(oneofl ["aaa" ; "bbb" ; "ccc" ; "ddd" ; "eee"]) in - let path_gen = Gen.oneof [gen_existing_path s; Gen.list_size (Gen.int_bound 5) name_gen] in (* can be empty *) + 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 - let pair_gen = - 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)); - ]) 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 ; - map (fun (path,new_dir_name) -> Mkdir (path, new_dir_name)) pair_gen; - map (fun (path,delete_dir_name) -> Rmdir (path, delete_dir_name)) pair_gen; - map (fun path -> Readdir path) path_gen; - map (fun (path,new_file_name) -> Mkfile (path, new_file_name)) pair_gen; - ]) + 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" From f932eda4ae7c8b74ec0090d1121b84164276c501 Mon Sep 17 00:00:00 2001 From: Jan Midtgaard Date: Tue, 17 Jan 2023 17:38:42 +0100 Subject: [PATCH 33/33] remove commented out code --- src/sys/stm_tests.ml | 10 +--------- 1 file changed, 1 insertion(+), 9 deletions(-) diff --git a/src/sys/stm_tests.ml b/src/sys/stm_tests.ml index 6e4b65e4a..6a640f838 100644 --- a/src/sys/stm_tests.ml +++ b/src/sys/stm_tests.ml @@ -178,15 +178,7 @@ struct if mem_model fs (path @ [new_file_name]) then fs else mkfile_model fs path new_file_name -(* - let env = Unix.environment () - - let sys_command_silent cmd = - let stdout,stdin,stderr = Unix.open_process_full cmd env in - In_channel.close stdout; - Out_channel.close stdin; - In_channel.close stderr -*) + let init_sut () = try Sys.mkdir sandbox_root 0o700 with Sys_error msg when msg = sandbox_root ^ ": File exists" -> ()