fix(solver): close pipes when process creation fails
2 files changed, +25 −3
check.ml modified
| @@ -28,6 +28,19 @@ let storage folder = | ||
| 28 | 28 | require (List.sort compare (Array.to_list (Sys.readdir folder)) = ["directory"; "nested"]) |
| 29 | 29 | "failed replacement removes temporary file" |
| 30 | 30 | |
| 31 | +let transport folder = | |
| 32 | + let previous = Option.value (Sys.getenv_opt "Z3") ~default:"z3" in | |
| 33 | + let descriptors () = Array.length (Sys.readdir "/proc/self/fd") in | |
| 34 | + let before = descriptors () in | |
| 35 | + Fun.protect ~finally:(fun () -> Unix.putenv "Z3" previous) (fun () -> | |
| 36 | + Unix.putenv "Z3" (Filename.concat folder "missing"); | |
| 37 | + for _ = 1 to 32 do | |
| 38 | + let failed = try ignore (Solver.script ""); false with | |
| 39 | + | Unix.Unix_error (Unix.ENOENT, _, _) -> true in | |
| 40 | + require failed "missing solver reports process creation failure" | |
| 41 | + done); | |
| 42 | + require (descriptors () = before) "failed solver spawn closes every pipe" | |
| 43 | + | |
| 31 | 44 | let laws () = |
| 32 | 45 | let source = Layout.generate ~timeout:300000 ^ Store.read "smt/machine.smt2" ^ |
| 33 | 46 | "\n" ^ Store.read "smt/laws.smt2" in |
| @@ -173,6 +186,7 @@ let () = | ||
| 173 | 186 | let folder = Filename.concat (Filename.get_temp_dir_name ()) (Printf.sprintf "reorder%d" (Unix.getpid ())) in |
| 174 | 187 | Store.mkdir folder; |
| 175 | 188 | storage folder; |
| 189 | + transport folder; | |
| 176 | 190 | codec (); |
| 177 | 191 | laws (); |
| 178 | 192 | fixtures (); |
solver.ml modified
| @@ -18,10 +18,18 @@ let command source = | ||
| 18 | 18 | |
| 19 | 19 | let connection ~timeout ~tick action = |
| 20 | 20 | let input_read, input_write = Unix.pipe ~cloexec:true () in |
| 21 | - let output_read, output_write = Unix.pipe ~cloexec:true () in | |
| 21 | + let output_read, output_write = | |
| 22 | + try Unix.pipe ~cloexec:true () with error -> | |
| 23 | + Unix.close input_read; | |
| 24 | + Unix.close input_write; | |
| 25 | + raise error in | |
| 22 | 26 | let executable = Option.value (Sys.getenv_opt "Z3") ~default:"z3" in |
| 23 | - let pid = Unix.create_process executable [|executable; "-in"; "-smt2"|] | |
| 24 | - input_read output_write output_write in | |
| 27 | + let pid = | |
| 28 | + try Unix.create_process executable [|executable; "-in"; "-smt2"|] | |
| 29 | + input_read output_write output_write | |
| 30 | + with error -> | |
| 31 | + List.iter Unix.close [input_read; input_write; output_read; output_write]; | |
| 32 | + raise error in | |
| 25 | 33 | Unix.close input_read; |
| 26 | 34 | Unix.close output_write; |
| 27 | 35 | let input = Unix.out_channel_of_descr input_write in |