11open QCheck
22open STM
33
4- module SConf =
4+ module SConf =
55struct
6-
6+
77 type cmd =
8- | File_exists of string list
8+ | File_exists of string list
99 | Mkdir of string list * string * int
1010 | Rmdir of string list * string
11- | Readdir of string list
11+ | Readdir of string list
1212 | Touch of string list * string * int
1313 [@@ deriving show { with_path = false }]
1414
15- module Map_names = Map. Make (String )
15+ module Map_names = Map. Make (String )
1616
17- type filesys =
17+ type filesys =
1818 | Directory of {perm : int ; fs_map : filesys Map_names .t }
1919 | File of {perm : int }
20-
20+
2121 type state = filesys
22-
23- type sut = unit
24-
22+
23+ type sut = unit
24+
2525 let (/ ) = Filename. concat
2626
2727 let arb_cmd _s =
2828 let name_gen = Gen. (oneofl [" aaa" ; " bbb" ; " ccc" ; " ddd" ; " eee" ]) in
2929 let path_gen = Gen. map (fun path -> path) (Gen. list_size (Gen. int_bound 5 ) name_gen) in (* can be empty *)
3030 let perm_gen = Gen. (oneofl [0o777 ]) in
3131 (* 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 *)
32- QCheck. make ~print: show_cmd
32+ QCheck. make ~print: show_cmd
3333 Gen. (oneof
34- [
34+ [
3535 map (fun path -> File_exists (path)) path_gen ;
3636 map3 (fun path new_dir_name perm -> Mkdir (path, new_dir_name, perm)) path_gen name_gen perm_gen;
3737 map2 (fun path delete_dir_name -> Rmdir (path, delete_dir_name)) path_gen name_gen;
@@ -43,106 +43,106 @@ struct
4343
4444 let init_state = Directory {perm = 0o777 ; fs_map = Map_names. empty}
4545
46- let update_map_name map_name k v = Map_names. add k v (Map_names. remove k map_name)
46+ let update_map_name map_name k v = Map_names. add k v (Map_names. remove k map_name)
4747
48- let rec find_opt fs path =
48+ let rec find_opt fs path =
4949 match fs with
50- | File f ->
51- if path = []
52- then Some (File f)
50+ | File f ->
51+ if path = []
52+ then Some (File f)
5353 else None
54- | Directory d ->
55- (match path with
54+ | Directory d ->
55+ (match path with
5656 | [] -> Some (Directory d)
57- | hd :: tl ->
57+ | hd :: tl ->
5858 (match Map_names. find_opt hd d.fs_map with
5959 | None -> None
6060 | Some fs -> find_opt fs tl))
6161
62- let mem fs path =
62+ let mem fs path =
6363 match find_opt fs path with
6464 | None -> false
6565 | Some _ -> true
6666
67- let rec mkdir fs path new_dir_name perm =
67+ let rec mkdir fs path new_dir_name perm =
6868 match fs with
6969 | File _ -> fs
70- | Directory d ->
71- (match path with
72- | [] ->
70+ | Directory d ->
71+ (match path with
72+ | [] ->
7373 let new_dir = Directory {perm; fs_map = Map_names. empty} in
7474 Directory {d with fs_map = Map_names. add new_dir_name new_dir d.fs_map}
75- | next_in_path :: tl_path ->
75+ | next_in_path :: tl_path ->
7676 (match Map_names. find_opt next_in_path d.fs_map with
7777 | None -> fs
78- | Some sub_fs ->
78+ | Some sub_fs ->
7979 let nfs = mkdir sub_fs tl_path new_dir_name perm in
8080 if nfs = sub_fs
8181 then fs
82- else
82+ else
8383 let new_map = Map_names. remove next_in_path d.fs_map in
8484 let new_map = Map_names. add next_in_path nfs new_map in
8585 Directory {d with fs_map = new_map}))
8686
87- let readdir fs path =
87+ let readdir fs path =
8888 match find_opt fs path with
8989 | None -> None
90- | Some fs ->
90+ | Some fs ->
9191 match fs with
9292 | File _ -> None
9393 | Directory d -> Some (Map_names. fold (fun k _ l -> l @ [k]) d.fs_map [] )
9494
95- let rec rmdir fs path delete_dir_name =
95+ let rec rmdir fs path delete_dir_name =
9696 match fs with
9797 | File _ -> fs
98- | Directory d ->
99- (match path with
100- | [] ->
98+ | Directory d ->
99+ (match path with
100+ | [] ->
101101 (match Map_names. find_opt delete_dir_name d.fs_map with
102102 | Some (Directory target ) when Map_names. is_empty target.fs_map ->
103103 Directory {d with fs_map = Map_names. remove delete_dir_name d.fs_map}
104104 | None | Some (File _ ) | Some (Directory _ ) -> fs)
105- | next_in_path :: tl_path ->
105+ | next_in_path :: tl_path ->
106106 (match Map_names. find_opt next_in_path d.fs_map with
107107 | None -> fs
108- | Some sub_fs ->
108+ | Some sub_fs ->
109109 let nfs = rmdir sub_fs tl_path delete_dir_name in
110110 if nfs = sub_fs
111111 then fs
112- else
112+ else
113113 Directory {d with fs_map = (update_map_name d.fs_map next_in_path nfs)}))
114114
115- let rec touch fs path new_file_name perm =
115+ let rec touch fs path new_file_name perm =
116116 match fs with
117117 | File _ -> fs
118- | Directory d ->
119- (match path with
120- | [] ->
118+ | Directory d ->
119+ (match path with
120+ | [] ->
121121 let new_file = File {perm} in
122122 Directory {d with fs_map = Map_names. add new_file_name new_file d.fs_map}
123- | next_in_path :: tl_path ->
123+ | next_in_path :: tl_path ->
124124 (match Map_names. find_opt next_in_path d.fs_map with
125125 | None -> fs
126- | Some sub_fs ->
126+ | Some sub_fs ->
127127 let nfs = touch sub_fs tl_path new_file_name perm in
128128 if nfs = sub_fs
129129 then fs
130- else
130+ else
131131 Directory {d with fs_map = update_map_name d.fs_map next_in_path nfs}))
132132
133- let next_state c fs =
133+ let next_state c fs =
134134 match c with
135135 | File_exists (_path ) -> fs
136- | Mkdir (path , new_dir_name , perm ) ->
136+ | Mkdir (path , new_dir_name , perm ) ->
137137 if mem fs (path @ [new_dir_name])
138138 then fs
139139 else mkdir fs path new_dir_name perm
140140 | Rmdir (path ,delete_dir_name ) ->
141141 if mem fs (path @ [delete_dir_name])
142142 then rmdir fs path delete_dir_name
143143 else fs
144- | Readdir _path -> fs
145- | Touch (path , new_file_name , perm ) ->
144+ | Readdir _path -> fs
145+ | Touch (path , new_file_name , perm ) ->
146146 if mem fs (path @ [new_file_name])
147147 then fs
148148 else touch fs path new_file_name perm
@@ -153,62 +153,60 @@ struct
153153 (* let cleanup _ = ignore (Sys.command ("tree " ^ static_path ^ "/sandbox_root && rm -r -d -f " ^ static_path ^ "/sandbox_root")) *)
154154 let cleanup _ = ignore (Sys. command (" rm -r -d -f " ^ static_path ^ " /sandbox_root" ))
155155
156- let precond _c _s = true
156+ let precond _c _s = true
157157
158158 let run c _file_name = match c with
159159 | File_exists (path ) -> Res (bool , Sys. file_exists (static_path / " sandbox_root" / (List. fold_left (/ ) " " path)))
160- | Mkdir (path , new_dir_name , perm ) ->
160+ | Mkdir (path , new_dir_name , perm ) ->
161161 Res (result unit exn , protect (Sys. mkdir (static_path / " sandbox_root" / (List. fold_left (/ ) " " path) / new_dir_name))perm)
162- | Rmdir (path , delete_dir_name ) ->
162+ | Rmdir (path , delete_dir_name ) ->
163163 Res (result unit exn , protect (Sys. rmdir) (static_path / " sandbox_root" / (List. fold_left (/ ) " " path) / delete_dir_name))
164- | Readdir (path ) ->
164+ | Readdir (path ) ->
165165 Res (result (array string ) exn , protect (Sys. readdir) (static_path / " sandbox_root" / (List. fold_left (/ ) " " path)))
166- | Touch (path , new_file_name , _perm ) ->
166+ | Touch (path , new_file_name , _perm ) ->
167167 Res (unit , ignore(Sys. command (" touch " ^ static_path / " sandbox_root" / (List. fold_left (/ ) " " path) / new_file_name ^ " 2>/dev/null" )))
168168
169169 let is_a_dir fs = match fs with | Directory _ -> true | File _ -> false
170170
171- let postcond c (fs : filesys ) res =
171+ let postcond c (fs : filesys ) res =
172172 let p path = static_path / " sandbox_root" / (String. concat " /" path) in
173173 match c, res with
174174 | File_exists (path ), Res ((Bool,_ ),b ) -> b = mem fs path
175175 | Mkdir (path, new_dir_name, _perm), Res ((Result (Unit ,Exn ),_), Error (Sys_error (s) ))
176- when s = (p (path @ [new_dir_name])) ^ " : Permission denied" -> true
176+ when s = (p (path @ [new_dir_name])) ^ " : Permission denied" -> true
177177 | Mkdir (path, new_dir_name, _perm), Res ((Result (Unit ,Exn ),_), Error (Sys_error (s) ))
178- when s = (p (path @ [new_dir_name])) ^ " : File exists" ->
179- mem fs (path @ [new_dir_name])
178+ when s = (p (path @ [new_dir_name])) ^ " : File exists" -> mem fs (path @ [new_dir_name])
180179 | Mkdir (path, new_dir_name, _perm), Res ((Result (Unit ,Exn ),_), Error (Sys_error (s) ))
181- when s = (p (path @ [new_dir_name])) ^ " : No such file or directory" ->
182- not (mem fs path)
180+ when s = (p (path @ [new_dir_name])) ^ " : No such file or directory" -> not (mem fs path)
183181 | Mkdir (path, new_dir_name, _perm), Res ((Result (Unit ,Exn ),_), Error (Sys_error (s) ))
184182 when s = (p (path @ [new_dir_name])) ^ " : Not a directory" ->
185183 (match find_opt fs (path @ [new_dir_name]) with
186184 | None -> true
187- | Some target_fs -> not (is_a_dir target_fs))
188- | Mkdir (path , new_dir_name , _perm ), Res ((Result (Unit,Exn),_ ), Ok () ) ->
185+ | Some target_fs -> not (is_a_dir target_fs))
186+ | Mkdir (path , new_dir_name , _perm ), Res ((Result (Unit,Exn),_ ), Ok () ) ->
189187 let is_existing_is_a_dir =
190188 (match find_opt fs path with
191- | None -> false
189+ | None -> false
192190 | Some target_fs -> is_a_dir target_fs) in
193191 true && not (mem fs (path @ [new_dir_name])) && mem fs path && is_existing_is_a_dir
194192 | Mkdir (_path , _new_dir_name , _perm ), Res ((Result (Unit,Exn),_ ), _ ) -> false
195193 | Rmdir (path, delete_dir_name), Res ((Result (Unit ,Exn ),_), Error (Sys_error (s) ))
196- when s = (p (path @ [delete_dir_name])) ^ " : No such file or directory" ->
194+ when s = (p (path @ [delete_dir_name])) ^ " : No such file or directory" ->
197195 not (mem fs (path @ [delete_dir_name]))
198196 | Rmdir (path, delete_dir_name), Res ((Result (Unit ,Exn ),_), Error (Sys_error (s) ))
199197 when s = (p (path @ [delete_dir_name])) ^ " : Directory not empty" ->
200198 not (readdir fs (path @ [delete_dir_name]) = Some [] )
201199 | Rmdir (path, delete_dir_name), Res ((Result (Unit ,Exn ),_), Error (Sys_error (s) ))
202- when s = (p (path @ [delete_dir_name])) ^ " : Not a directory" ->
200+ when s = (p (path @ [delete_dir_name])) ^ " : Not a directory" ->
203201 (match find_opt fs (path @ [delete_dir_name]) with
204202 | None -> true
205203 | Some target_fs -> not (is_a_dir target_fs))
206- | Rmdir (path , delete_dir_name ), Res ((Result (Unit,Exn),_ ), Ok () ) ->
204+ | Rmdir (path , delete_dir_name ), Res ((Result (Unit,Exn),_ ), Ok () ) ->
207205 let is_empty = readdir fs (path @ [delete_dir_name]) = Some [] in
208206 let is_a_dir =
209207 (match find_opt fs (path @ [delete_dir_name]) with
210208 | None -> false
211- | Some target_fs -> is_a_dir target_fs) in
209+ | Some target_fs -> is_a_dir target_fs) in
212210 mem fs (path @ [delete_dir_name]) && is_empty && is_a_dir
213211 | Rmdir (_path , _delete_dir_name ), Res ((Result (Unit,Exn),_ ), _r ) -> false
214212 | Readdir (path), Res ((Result (Array String ,Exn ),_), Error (Sys_error (s) ))
@@ -221,10 +219,10 @@ struct
221219 (match find_opt fs path with
222220 | None -> true
223221 | Some target_fs -> not (is_a_dir target_fs))
224- | Readdir (path ), Res ((Result (Array String,Exn),_ ), r ) ->
222+ | Readdir (path ), Res ((Result (Array String,Exn),_ ), r ) ->
225223 (match r with
226224 | Error _ -> false
227- | Ok a ->
225+ | Ok a ->
228226 let sut = List. sort (fun a b -> - (String. compare a b)) (Array. to_list a) in
229227 (match readdir fs path with
230228 | None -> false
0 commit comments