From 51e77d152c2f941c1351edbd13cf8bb09abcf4d0 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Tue, 7 Mar 2023 10:48:31 +0100
Subject: [PATCH] fix: do not inherit file handles across process creation

---
 src/runtime/io.cpp       |  7 ++++++-
 src/runtime/process.cpp  | 14 +++++++++-----
 tests/lean/run/2137.lean | 18 ++++++++++++++++++
 3 files changed, 33 insertions(+), 6 deletions(-)
 create mode 100644 tests/lean/run/2137.lean

diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index 97c912c3cc..0d3bd3c0e0 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -86,7 +86,7 @@ static obj_res mk_file_not_found_error(b_obj_arg fname) {
 static lean_external_class * g_io_handle_external_class = nullptr;
 
 static void io_handle_finalizer(void * h) {
-    fclose(static_cast<FILE *>(h));
+    lean_always_assert(fclose(static_cast<FILE *>(h)) == 0);
 }
 
 static void io_handle_foreach(void * /* mod */, b_obj_arg /* fn */) {
@@ -259,6 +259,11 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_mk(b_obj_arg filename, uint8
 #ifdef LEAN_WINDOWS
     // do not translate line endings
     flags |= O_BINARY;
+    // do not inherit across process creation
+    flags |= O_NOINHERIT;
+#else
+    // do not inherit across process creation
+    flags |= O_CLOEXEC;
 #endif
     switch (mode) {
     case 0: flags |= O_RDONLY; break;  // read
diff --git a/src/runtime/process.cpp b/src/runtime/process.cpp
index fd8615b3c6..de9c0e604b 100644
--- a/src/runtime/process.cpp
+++ b/src/runtime/process.cpp
@@ -264,11 +264,15 @@ static optional<pipe> setup_stdio(stdio cfg) {
         return optional<pipe>();
     case stdio::PIPED:
         int fds[2];
-        if (::pipe(fds) == -1) {
-            throw errno;
-        } else {
-            return optional<pipe>(pipe { fds[0], fds[1] });
-        }
+#ifdef __APPLE__
+        // this is inherently racy, but there is nothing we can do on MacOS
+        if (::pipe(fds) == -1) { throw errno; }
+        if (::fcntl(fds[0], F_SETFD, FD_CLOEXEC)) { throw errno; }
+        if (::fcntl(fds[1], F_SETFD, FD_CLOEXEC)) { throw errno; }
+#else
+        if (::pipe2(fds, O_CLOEXEC) == -1) { throw errno; }
+#endif
+        return optional<pipe>(pipe { fds[0], fds[1] });
     case stdio::NUL:
         /* We should map /dev/null. */
         return optional<pipe>();
diff --git a/tests/lean/run/2137.lean b/tests/lean/run/2137.lean
new file mode 100644
index 0000000000..b039eb5ea5
--- /dev/null
+++ b/tests/lean/run/2137.lean
@@ -0,0 +1,18 @@
+def makeProc : IO Unit := do
+  let child ← IO.Process.spawn {
+    cmd := "cat"
+    args := #[]
+    stdin := .piped
+    stdout := .piped
+  }
+  IO.print (← child.stdout.getLine)
+
+def main (_ : List String) : IO UInt32 := do
+  IO.println "test"
+  makeProc
+  IO.println "done test"
+
+  for _ in [0:6] do
+    let _ ← IO.asTask makeProc
+
+  return 0