From 8d937a28ee7f62dff6b628435a224015ed16f971 Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Mon, 2 Jun 2025 19:21:06 +0200 Subject: [PATCH 1/6] fix windows process spawn quoting --- src/runtime/process.cpp | 38 +++++++++++++++++++++++++++++++++----- 1 file changed, 33 insertions(+), 5 deletions(-) diff --git a/src/runtime/process.cpp b/src/runtime/process.cpp index ed8d63d41c90..8290afefe715 100644 --- a/src/runtime/process.cpp +++ b/src/runtime/process.cpp @@ -190,6 +190,16 @@ static obj_res spawn(string_ref const & proc_name, array_ref const & std::string program = proc_name.to_std_string(); + // Validate program name + if (program.size() == 0 || program[program.size() - 1] == '\\') { + return io_result_mk_error(lean_mk_io_error_invalid_argument_file(proc_name.to_obj_arg(), EINVAL, mk_string("invalid process name"))); + } + for (size_t i = 0; i < program.size(); i++) { + if (program[i] == '"') { + return io_result_mk_error(lean_mk_io_error_invalid_argument_file(proc_name.to_obj_arg(), EINVAL, mk_string("invalid process name"))); + } + } + // Always escape program in cmdline, in case it contains spaces std::string command = "\""; command += program; @@ -201,14 +211,32 @@ static obj_res spawn(string_ref const & proc_name, array_ref const & // We must escape the arguments to preserving spacing and other characters, // we might need to revisit escaping here. for (auto arg : args) { - command += " \""; + bool should_quote = false; for (char const * c = arg.data(); *c != 0; c++) { - if (*c == '"') { - command += '\\'; + // check for safe characters + if ((*c < 'A' || *c > 'Z') && (*c < 'a' || *c > 'z') && (*c < '0' || *c > '9')) { + switch (*c) { + case '#': case '$': case '*': case '+': case '-': case '.': case '/': case ':': + case '?': case '@': case '_': + continue; + } + should_quote = true; + break; } - command += *c; } - command += "\""; + if (should_quote) { + command += " \""; + for (char const * c = arg.data(); *c != 0; c++) { + if (*c == '"' || *c == '\\') { + command += '\\'; + } + command += *c; + } + command += "\""; + } else { + command += " "; + command += arg.to_std_string(); + } } PROCESS_INFORMATION piProcInfo; From 476a7779b6c3f61269dc9aecbf942b88ca721f9e Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Mon, 2 Jun 2025 19:56:53 +0200 Subject: [PATCH 2/6] fix --- src/runtime/process.cpp | 33 +++++++++++++++++++++++---------- 1 file changed, 23 insertions(+), 10 deletions(-) diff --git a/src/runtime/process.cpp b/src/runtime/process.cpp index 8290afefe715..638112e8aa5d 100644 --- a/src/runtime/process.cpp +++ b/src/runtime/process.cpp @@ -211,13 +211,15 @@ static obj_res spawn(string_ref const & proc_name, array_ref const & // We must escape the arguments to preserving spacing and other characters, // we might need to revisit escaping here. for (auto arg : args) { - bool should_quote = false; + // Adapted from https://github.com/rust-lang/rust/blob/2398bd6/library/std/src/sys/args/windows.rs + bool should_quote = *arg.data() == 0; // always escape empty strings for (char const * c = arg.data(); *c != 0; c++) { - // check for safe characters + // check for safe characters (safe variant for .bat arguments) if ((*c < 'A' || *c > 'Z') && (*c < 'a' || *c > 'z') && (*c < '0' || *c > '9')) { switch (*c) { - case '#': case '$': case '*': case '+': case '-': case '.': case '/': case ':': - case '?': case '@': case '_': + case '#': case '$': case '*': case '+': + case '-': case '.': case '/': case ':': + case '?': case '@': case '_': case '\\': continue; } should_quote = true; @@ -226,16 +228,27 @@ static obj_res spawn(string_ref const & proc_name, array_ref const & } if (should_quote) { command += " \""; - for (char const * c = arg.data(); *c != 0; c++) { + } else { + command += " "; + } + // Note: Backslashes should only be escaped if they precede the closing quote or an escaped quote + size_t backslashes = 0; + for (char const * c = arg.data(); *c != 0; c++) { + if (*c == '\\') { + backslashes++; + } else { if (*c == '"' || *c == '\\') { - command += '\\'; + // append n+1 backslashes for a total of 2n+1 backslashes + command.append(backslashes + 1, '\\'); } - command += *c; + backslashes = 0; } + command += *c; + } + if (should_quote) { + // append n backslashes for a total of 2n backslashes + command.append(backslashes, '\\'); command += "\""; - } else { - command += " "; - command += arg.to_std_string(); } } From 6ff20f72dbd8f702eefa32929cf461cb6899b547 Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Tue, 3 Jun 2025 15:37:31 +0200 Subject: [PATCH 3/6] fix leaks --- src/runtime/process.cpp | 60 +++++++++++++++++++++++------------------ 1 file changed, 34 insertions(+), 26 deletions(-) diff --git a/src/runtime/process.cpp b/src/runtime/process.cpp index 638112e8aa5d..03629d74fa0c 100644 --- a/src/runtime/process.cpp +++ b/src/runtime/process.cpp @@ -138,9 +138,7 @@ static void setup_stdio(SECURITY_ATTRIBUTES * saAttr, HANDLE * theirs, object ** /* Setup stdio based on process configuration. */ switch (cfg) { case stdio::INHERIT: - lean_always_assert(DuplicateHandle(GetCurrentProcess(), *theirs, - GetCurrentProcess(), theirs, - 0, TRUE, DUPLICATE_SAME_ACCESS)); + // Use the handle from the parent process return; case stdio::PIPED: { HANDLE readh; @@ -173,30 +171,15 @@ static void setup_stdio(SECURITY_ATTRIBUTES * saAttr, HANDLE * theirs, object ** static obj_res spawn(string_ref const & proc_name, array_ref const & args, stdio stdin_mode, stdio stdout_mode, stdio stderr_mode, option_ref const & cwd, array_ref>> const & env, bool inherit_env, bool _do_setsid) { - HANDLE child_stdin = GetStdHandle(STD_INPUT_HANDLE); - HANDLE child_stdout = GetStdHandle(STD_OUTPUT_HANDLE); - HANDLE child_stderr = GetStdHandle(STD_ERROR_HANDLE); - - SECURITY_ATTRIBUTES saAttr; - - // Set the bInheritHandle flag so pipe/NUL handles are inherited. - saAttr.nLength = sizeof(SECURITY_ATTRIBUTES); - saAttr.bInheritHandle = TRUE; - saAttr.lpSecurityDescriptor = NULL; - - object * parent_stdin = box(0); setup_stdio(&saAttr, &child_stdin, &parent_stdin, true, stdin_mode); - object * parent_stdout = box(0); setup_stdio(&saAttr, &child_stdout, &parent_stdout, false, stdout_mode); - object * parent_stderr = box(0); setup_stdio(&saAttr, &child_stderr, &parent_stderr, false, stderr_mode); - std::string program = proc_name.to_std_string(); // Validate program name if (program.size() == 0 || program[program.size() - 1] == '\\') { - return io_result_mk_error(lean_mk_io_error_invalid_argument_file(proc_name.to_obj_arg(), EINVAL, mk_string("invalid process name"))); + return io_result_mk_error(lean_mk_io_error_invalid_argument_file(proc_name.to_obj_arg(), EINVAL, mk_string("Invalid process name"))); } for (size_t i = 0; i < program.size(); i++) { if (program[i] == '"') { - return io_result_mk_error(lean_mk_io_error_invalid_argument_file(proc_name.to_obj_arg(), EINVAL, mk_string("invalid process name"))); + return io_result_mk_error(lean_mk_io_error_invalid_argument_file(proc_name.to_obj_arg(), EINVAL, mk_string("Invalid process name"))); } } @@ -212,9 +195,10 @@ static obj_res spawn(string_ref const & proc_name, array_ref const & // we might need to revisit escaping here. for (auto arg : args) { // Adapted from https://github.com/rust-lang/rust/blob/2398bd6/library/std/src/sys/args/windows.rs - bool should_quote = *arg.data() == 0; // always escape empty strings + bool should_quote = false; + char last_char = '\\'; for (char const * c = arg.data(); *c != 0; c++) { - // check for safe characters (safe variant for .bat arguments) + // check for safe characters (stricter variant for .bat arguments) if ((*c < 'A' || *c > 'Z') && (*c < 'a' || *c > 'z') && (*c < '0' || *c > '9')) { switch (*c) { case '#': case '$': case '*': case '+': @@ -225,6 +209,11 @@ static obj_res spawn(string_ref const & proc_name, array_ref const & should_quote = true; break; } + last_char = *c; + } + // escape empty strings and strings with trailing backslash + if (last_char == '\\') { + should_quote = true; } if (should_quote) { command += " \""; @@ -252,6 +241,21 @@ static obj_res spawn(string_ref const & proc_name, array_ref const & } } + HANDLE child_stdin = GetStdHandle(STD_INPUT_HANDLE); + HANDLE child_stdout = GetStdHandle(STD_OUTPUT_HANDLE); + HANDLE child_stderr = GetStdHandle(STD_ERROR_HANDLE); + + SECURITY_ATTRIBUTES saAttr; + + // Set the bInheritHandle flag so pipe/NUL handles are inherited. + saAttr.nLength = sizeof(SECURITY_ATTRIBUTES); + saAttr.bInheritHandle = TRUE; + saAttr.lpSecurityDescriptor = NULL; + + object * parent_stdin = box(0); setup_stdio(&saAttr, &child_stdin, &parent_stdin, true, stdin_mode); + object * parent_stdout = box(0); setup_stdio(&saAttr, &child_stdout, &parent_stdout, false, stdout_mode); + object * parent_stderr = box(0); setup_stdio(&saAttr, &child_stderr, &parent_stderr, false, stderr_mode); + PROCESS_INFORMATION piProcInfo; STARTUPINFO siStartInfo; @@ -326,17 +330,21 @@ static obj_res spawn(string_ref const & proc_name, array_ref const & &siStartInfo, // STARTUPINFO pointer &piProcInfo); // receives PROCESS_INFORMATION + if (stdin_mode != stdio::INHERIT) CloseHandle(child_stdin); + if (stdout_mode != stdio::INHERIT) CloseHandle(child_stdout); + if (stderr_mode != stdio::INHERIT) CloseHandle(child_stderr); + if (!bSuccess) { + lean_dec(parent_stdin); + lean_dec(parent_stdout); + lean_dec(parent_stderr); + throw std::system_error(GetLastError(), std::system_category()); } // Close handle to primary thread, we don't need it. CloseHandle(piProcInfo.hThread); - if (stdin_mode == stdio::PIPED) CloseHandle(child_stdin); - if (stdout_mode == stdio::PIPED) CloseHandle(child_stdout); - if (stderr_mode == stdio::PIPED) CloseHandle(child_stderr); - object_ref r = mk_cnstr(0, parent_stdin, parent_stdout, parent_stderr, wrap_win_handle(piProcInfo.hProcess)); return lean_io_result_mk_ok(r.steal()); } From f2e5494eaf36c5d4e1e46ef8d28e0a13ac16ce07 Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Tue, 3 Jun 2025 15:46:35 +0200 Subject: [PATCH 4/6] add test --- tests/lean/run/8612.lean | 19 +++++++++++++++++++ 1 file changed, 19 insertions(+) create mode 100644 tests/lean/run/8612.lean diff --git a/tests/lean/run/8612.lean b/tests/lean/run/8612.lean new file mode 100644 index 000000000000..c6776264d1a8 --- /dev/null +++ b/tests/lean/run/8612.lean @@ -0,0 +1,19 @@ +macro "assert_eq! " t1:term ", " t2:term : doElem => + `(doElem| if $t1 != $t2 then throw (.userError s!"{repr $t1} != {repr $t2}")) + +macro "assert_failure! " e:doElem : doElem => + `(doElem| try $e; throw (.userError s!"unexpected success") catch _ => pure ()) + +def runTests : IO Unit := do + unless System.Platform.isWindows do + return + let out ← IO.Process.run { cmd := "cmd.exe", args := #["/c", "echo", "hi"] } + assert_eq! out, "hi\r\n" + assert_failure! discard <| IO.Process.run { cmd := "cmd.exe\" echo \"hi" } + assert_failure! discard <| IO.Process.run { cmd := "cmd.exe\\" } + -- creating a lot of processes should succeed and not leak file handles + for _ in [0:500] do + discard <| IO.Process.run { cmd := "cmd.exe", args := #["/c", "echo", "hi"] } + --assert_failure! discard <| IO.Process.run { cmd := "cmd.exe\" echo \"hi" } + +#eval runTests From 16dd0b55fc73ae0c3131e49d058f750d55c98b7e Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Tue, 3 Jun 2025 15:47:11 +0200 Subject: [PATCH 5/6] trigger release ci From 584e529a8d58b4bc7398a8dc44c5ad2a21012a6c Mon Sep 17 00:00:00 2001 From: Rob23oba Date: Tue, 3 Jun 2025 15:50:53 +0200 Subject: [PATCH 6/6] remove comment in test --- tests/lean/run/8612.lean | 1 - 1 file changed, 1 deletion(-) diff --git a/tests/lean/run/8612.lean b/tests/lean/run/8612.lean index c6776264d1a8..711323f9bc46 100644 --- a/tests/lean/run/8612.lean +++ b/tests/lean/run/8612.lean @@ -14,6 +14,5 @@ def runTests : IO Unit := do -- creating a lot of processes should succeed and not leak file handles for _ in [0:500] do discard <| IO.Process.run { cmd := "cmd.exe", args := #["/c", "echo", "hi"] } - --assert_failure! discard <| IO.Process.run { cmd := "cmd.exe\" echo \"hi" } #eval runTests