diff --git a/c_runtime/test.c b/c_runtime/test.c index 39031d517..0d342358d 100644 --- a/c_runtime/test.c +++ b/c_runtime/test.c @@ -722,19 +722,64 @@ static void io_core_assert_stop_result(BValue value, int expected, const char* m } } -static BValue io_core_spawn_poll_after_wait_poll_fn(BValue* slots, BValue opt) { - (void)slots; - assert_option_int(opt, "3", "IO/Core poll after wait should return the cached child status"); - return ___bsts_g_Bosatsu_l_Prog_l_pure(get_enum_index(opt, 0)); +static BValue io_core_spawn_stable_status_final_wait_fn(BValue* slots, BValue status) { + assert( + bsts_integer_cmp(status, slots[1]) == 0, + "IO/Core final repeated wait should return the cached child status"); + return ___bsts_g_Bosatsu_l_Prog_l_pure(status); +} + +static BValue io_core_spawn_stable_status_wait_timeout_fn(BValue* slots, BValue opt) { + if (get_variant(opt) != 1) { + printf("IO/Core wait_timeout after recorded exit should return Some(cached status)\nexpected: Some\n"); + exit(1); + } + assert( + bsts_integer_cmp(get_enum_index(opt, 0), slots[1]) == 0, + "IO/Core wait_timeout after recorded exit should return the cached child status"); + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_wait(slots[0]), + alloc_closure1(2, slots, io_core_spawn_stable_status_final_wait_fn)); +} + +static BValue io_core_spawn_stable_status_second_poll_fn(BValue* slots, BValue opt) { + if (get_variant(opt) != 1) { + printf("IO/Core repeated poll after recorded exit should return Some(cached status)\nexpected: Some\n"); + exit(1); + } + assert( + bsts_integer_cmp(get_enum_index(opt, 0), slots[1]) == 0, + "IO/Core repeated poll after recorded exit should return the cached child status"); + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_wait__timeout(slots[0], bsts_integer_from_int(0)), + alloc_closure1(2, slots, io_core_spawn_stable_status_wait_timeout_fn)); +} + +static BValue io_core_spawn_stable_status_first_poll_fn(BValue* slots, BValue opt) { + if (get_variant(opt) != 1) { + printf("IO/Core poll after recorded exit should return Some(cached status)\nexpected: Some\n"); + exit(1); + } + assert( + bsts_integer_cmp(get_enum_index(opt, 0), slots[1]) == 0, + "IO/Core poll after recorded exit should return the cached child status"); + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_poll(slots[0]), + alloc_closure1(2, slots, io_core_spawn_stable_status_second_poll_fn)); +} + +static BValue io_core_spawn_assert_stable_status(BValue process, BValue status) { + BValue slots[2] = { process, status }; + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_poll(process), + alloc_closure1(2, slots, io_core_spawn_stable_status_first_poll_fn)); } static BValue io_core_spawn_poll_after_wait_fn(BValue* slots, BValue status) { assert( bsts_integer_cmp(status, bsts_integer_from_int(3)) == 0, "IO/Core poll test wait should observe the child status"); - return ___bsts_g_Bosatsu_l_Prog_l_flat__map( - ___bsts_g_Bosatsu_l_IO_l_Core_l_poll(slots[0]), - alloc_closure1(1, slots, io_core_spawn_poll_after_wait_poll_fn)); + return io_core_spawn_assert_stable_status(slots[0], status); } static BValue io_core_spawn_poll_before_wait_fn(BValue* slots, BValue opt) { @@ -766,7 +811,7 @@ static BValue io_core_spawn_wait_timeout_wait_fn(BValue* slots, BValue status) { assert( bsts_integer_cmp(status, bsts_integer_from_int(4)) == 0, "IO/Core wait_timeout should not consume the later child status"); - return ___bsts_g_Bosatsu_l_Prog_l_pure(status); + return io_core_spawn_assert_stable_status(slots[0], status); } static BValue io_core_spawn_wait_timeout_none_fn(BValue* slots, BValue opt) { @@ -837,11 +882,10 @@ static BValue io_core_spawn_wait_timeout_zero_test_fn(BValue arg) { } static BValue io_core_spawn_stop_wait_fn(BValue* slots, BValue status) { - (void)slots; assert( bsts_integer_cmp(status, bsts_integer_from_int(0)) != 0, "IO/Core stop followed by wait should observe a non-zero stopped status"); - return ___bsts_g_Bosatsu_l_Prog_l_pure(status); + return io_core_spawn_assert_stable_status(slots[0], status); } static BValue io_core_spawn_terminate_sent_fn(BValue* slots, BValue stop_result) { @@ -905,7 +949,7 @@ static BValue io_core_spawn_already_exited_final_wait_fn(BValue* slots, BValue s stop_result, 1, "IO/Core kill after recorded exit should return AlreadyExited"); - return ___bsts_g_Bosatsu_l_IO_l_Core_l_wait(slots[0]); + return io_core_spawn_assert_stable_status(slots[0], slots[1]); } static BValue io_core_spawn_already_exited_kill_fn(BValue* slots, BValue stop_result) { @@ -915,16 +959,17 @@ static BValue io_core_spawn_already_exited_kill_fn(BValue* slots, BValue stop_re "IO/Core terminate after recorded exit should return AlreadyExited"); return ___bsts_g_Bosatsu_l_Prog_l_flat__map( ___bsts_g_Bosatsu_l_IO_l_Core_l_kill(slots[0]), - alloc_closure1(1, slots, io_core_spawn_already_exited_final_wait_fn)); + alloc_closure1(2, slots, io_core_spawn_already_exited_final_wait_fn)); } static BValue io_core_spawn_already_exited_wait_fn(BValue* slots, BValue status) { assert( bsts_integer_cmp(status, bsts_integer_from_int(0)) == 0, "IO/Core already-exited stop test should first record zero child status"); + BValue next_slots[2] = { slots[0], status }; return ___bsts_g_Bosatsu_l_Prog_l_flat__map( ___bsts_g_Bosatsu_l_IO_l_Core_l_terminate(slots[0]), - alloc_closure1(1, slots, io_core_spawn_already_exited_kill_fn)); + alloc_closure1(2, next_slots, io_core_spawn_already_exited_kill_fn)); } static BValue io_core_spawn_already_exited_process_fn(BValue spawn_result) { @@ -1287,6 +1332,179 @@ static BValue io_core_spawn_pipe_stdin_test_fn(BValue arg) { alloc_boxed_pure_fn1(io_core_spawn_pipe_stdin_write_fn)); } +static BValue io_core_spawn_low_level_pipe_owner_wait_fn(BValue* slots, BValue arg) { + (void)arg; + return ___bsts_g_Bosatsu_l_IO_l_Core_l_wait(slots[0]); +} + +static BValue io_core_spawn_low_level_pipe_owner_close_stdout_fn(BValue* slots, BValue arg) { + static const uint8_t expected[] = {'r', 'o', 'u', 'n', 'd', '\n'}; + assert_bytes_equal( + arg, + expected, + (int)sizeof(expected), + "IO/Core low-level process operations should not close or drain returned stdio pipes"); + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_close(slots[2]), + alloc_closure1(3, slots, io_core_spawn_low_level_pipe_owner_wait_fn)); +} + +static BValue io_core_spawn_low_level_pipe_owner_read_stdout_fn(BValue* slots, BValue arg) { + (void)arg; + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_read__all__bytes(slots[2], bsts_integer_from_int(16)), + alloc_closure1(3, slots, io_core_spawn_low_level_pipe_owner_close_stdout_fn)); +} + +static BValue io_core_spawn_low_level_pipe_owner_close_stdin_fn(BValue* slots, BValue arg) { + (void)arg; + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_close(slots[1]), + alloc_closure1(3, slots, io_core_spawn_low_level_pipe_owner_read_stdout_fn)); +} + +static BValue io_core_spawn_low_level_pipe_owner_write_fn(BValue* slots, BValue stop_result) { + io_core_assert_stop_result( + stop_result, + 0, + "IO/Core terminate before stdio use should return StopSent for the running child"); + static const uint8_t payload[] = {'r', 'o', 'u', 'n', 'd', '\n'}; + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_write__bytes( + slots[1], + io_core_bytes_value(payload, (int)sizeof(payload))), + alloc_closure1(3, slots, io_core_spawn_low_level_pipe_owner_close_stdin_fn)); +} + +static BValue io_core_spawn_low_level_pipe_owner_timeout_fn(BValue* slots, BValue opt) { + assert_option_none( + opt, + "IO/Core wait_timeout before stdio use should not consume or close returned pipes"); + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_terminate(slots[0]), + alloc_closure1(3, slots, io_core_spawn_low_level_pipe_owner_write_fn)); +} + +static BValue io_core_spawn_low_level_pipe_owner_poll_fn(BValue* slots, BValue opt) { + assert_option_none( + opt, + "IO/Core poll before stdio use should not consume or close returned pipes"); + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_wait__timeout(slots[0], bsts_integer_from_int(0)), + alloc_closure1(3, slots, io_core_spawn_low_level_pipe_owner_timeout_fn)); +} + +static BValue io_core_spawn_low_level_pipe_owner_ready_fn(BValue* slots, BValue ready) { + static const uint8_t expected[] = {'r', 'e', 'a', 'd', 'y', '\n'}; + assert_option_bytes_equal( + ready, + expected, + (int)sizeof(expected), + "IO/Core low-level pipe ownership test child should install its TERM trap before stop"); + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_poll(slots[0]), + alloc_closure1(3, slots, io_core_spawn_low_level_pipe_owner_poll_fn)); +} + +static BValue io_core_spawn_low_level_pipe_owner_fn(BValue spawn_result) { + BValue stdin_opt = get_struct_index(spawn_result, 1); + BValue stdout_opt = get_struct_index(spawn_result, 2); + io_core_assert_some_handle(stdin_opt, "IO/Core spawn stdin pipe should return a handle"); + io_core_assert_some_handle(stdout_opt, "IO/Core spawn stdout pipe should return a handle"); + BValue slots[3] = { + get_struct_index(spawn_result, 0), + get_enum_index(stdin_opt, 0), + get_enum_index(stdout_opt, 0)}; + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_read__bytes(slots[2], bsts_integer_from_int(6)), + alloc_closure1(3, slots, io_core_spawn_low_level_pipe_owner_ready_fn)); +} + +static BValue io_core_spawn_low_level_pipe_owner_test_fn(BValue arg) { + (void)arg; + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_spawn( + bsts_string_from_utf8_bytes_static(7, "/bin/sh"), + io_core_string_list2("-c", "trap '' TERM; printf 'ready\\n'; cat"), + alloc_struct3(io_core_stdio_pipe(), io_core_stdio_pipe(), alloc_enum0(2))), + alloc_boxed_pure_fn1(io_core_spawn_low_level_pipe_owner_fn)); +} + +static BValue io_core_spawn_low_level_pipe_owner_kill_done_fn(BValue* slots, BValue status) { + (void)slots; + assert( + bsts_integer_cmp(status, bsts_integer_from_int(0)) != 0, + "IO/Core kill before stdio close should be followed by a non-zero stopped status"); + return ___bsts_g_Bosatsu_l_Prog_l_pure(bsts_integer_from_int(0)); +} + +static BValue io_core_spawn_low_level_pipe_owner_kill_wait_fn(BValue* slots, BValue arg) { + (void)arg; + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_wait(slots[0]), + alloc_closure1(3, slots, io_core_spawn_low_level_pipe_owner_kill_done_fn)); +} + +static BValue io_core_spawn_low_level_pipe_owner_kill_close_stdout_fn(BValue* slots, BValue arg) { + (void)arg; + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_close(slots[2]), + alloc_closure1(3, slots, io_core_spawn_low_level_pipe_owner_kill_wait_fn)); +} + +static BValue io_core_spawn_low_level_pipe_owner_kill_close_stdin_fn(BValue* slots, BValue arg) { + (void)arg; + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_close(slots[1]), + alloc_closure1(3, slots, io_core_spawn_low_level_pipe_owner_kill_close_stdout_fn)); +} + +static BValue io_core_spawn_low_level_pipe_owner_kill_write_fn(BValue* slots, BValue stop_result) { + io_core_assert_stop_result( + stop_result, + 0, + "IO/Core kill before stdio close should return StopSent for the running child"); + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_write__bytes(slots[1], io_core_bytes_value(NULL, 0)), + alloc_closure1(3, slots, io_core_spawn_low_level_pipe_owner_kill_close_stdin_fn)); +} + +static BValue io_core_spawn_low_level_pipe_owner_kill_ready_fn(BValue* slots, BValue ready) { + static const uint8_t expected[] = {'r', 'e', 'a', 'd', 'y', '\n'}; + assert_option_bytes_equal( + ready, + expected, + (int)sizeof(expected), + "IO/Core low-level pipe ownership kill child should be running before stop"); + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_kill(slots[0]), + alloc_closure1(3, slots, io_core_spawn_low_level_pipe_owner_kill_write_fn)); +} + +static BValue io_core_spawn_low_level_pipe_owner_kill_fn(BValue spawn_result) { + BValue stdin_opt = get_struct_index(spawn_result, 1); + BValue stdout_opt = get_struct_index(spawn_result, 2); + io_core_assert_some_handle(stdin_opt, "IO/Core spawn stdin pipe should return a handle"); + io_core_assert_some_handle(stdout_opt, "IO/Core spawn stdout pipe should return a handle"); + BValue slots[3] = { + get_struct_index(spawn_result, 0), + get_enum_index(stdin_opt, 0), + get_enum_index(stdout_opt, 0)}; + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_read__bytes(slots[2], bsts_integer_from_int(6)), + alloc_closure1(3, slots, io_core_spawn_low_level_pipe_owner_kill_ready_fn)); +} + +static BValue io_core_spawn_low_level_pipe_owner_kill_test_fn(BValue arg) { + (void)arg; + return ___bsts_g_Bosatsu_l_Prog_l_flat__map( + ___bsts_g_Bosatsu_l_IO_l_Core_l_spawn( + bsts_string_from_utf8_bytes_static(7, "/bin/sh"), + io_core_string_list2("-c", "printf 'ready\\n'; sleep 10"), + alloc_struct3(io_core_stdio_pipe(), io_core_stdio_pipe(), alloc_enum0(2))), + alloc_boxed_pure_fn1(io_core_spawn_low_level_pipe_owner_kill_fn)); +} + static BValue io_core_spawn_existing_handle_invalid_test_fn(BValue arg) { (void)arg; return ___bsts_g_Bosatsu_l_IO_l_Core_l_spawn( @@ -3429,6 +3647,14 @@ void test_io_core_libuv_effects() { bsts_Bosatsu_Prog_run_test(alloc_boxed_pure_fn1(io_core_spawn_pipe_stdin_test_fn)), "0", "IO/Core spawn should support piped stdin"); + assert_prog_success_int( + bsts_Bosatsu_Prog_run_test(alloc_boxed_pure_fn1(io_core_spawn_low_level_pipe_owner_test_fn)), + "0", + "IO/Core low-level process operations should leave returned stdio pipes caller-owned"); + assert_prog_success_int( + bsts_Bosatsu_Prog_run_test(alloc_boxed_pure_fn1(io_core_spawn_low_level_pipe_owner_kill_test_fn)), + "0", + "IO/Core kill should leave returned stdio pipes caller-owned"); assert_prog_error_variant( bsts_Bosatsu_Prog_run_test(alloc_boxed_pure_fn1(io_core_spawn_existing_handle_invalid_test_fn)), 14, diff --git a/docs/code-plans/2376-add-cross-backend-process-stop-and-cleanup-regression-coverage.json b/docs/code-plans/2376-add-cross-backend-process-stop-and-cleanup-regression-coverage.json new file mode 100644 index 000000000..b73df7f41 --- /dev/null +++ b/docs/code-plans/2376-add-cross-backend-process-stop-and-cleanup-regression-coverage.json @@ -0,0 +1 @@ +{"current_state_markdown":"The merged dependencies have already added the public low-level process APIs (`StopResult`, `terminate`, `kill`, `poll`, `wait_timeout`) and the higher-level `with_process` helper in `test_workspace/Bosatsu/IO/Core.bosatsu`. This branch has shared JVM/Python coverage for stable status observations, timeout non-consumption, already-exited stop behavior, terminate/kill stable post-stop status, low-level pipe ownership after non-stop status operations, shared `terminate` and `kill` pipe ownership after stop, and helper-owned versus caller-owned handle cleanup. C/libuv coverage includes reusable post-recorded status assertions and focused low-level ownership regressions for `poll`, zero-duration `wait_timeout`, `terminate`, and `kill`.","flow":"small_job","issue_number":2376,"issue_title":"Add cross-backend process stop and cleanup regression coverage","problem_markdown":"Issue #2361's acceptance criteria require the cross-backend regression suite to make the low-level stdio ownership contract explicit: low-level stop/status functions must not close returned stdio handles, and callers remain responsible for closing those handles. The previous candidate proved this for non-stop status operations, for shared `kill`, and for C/libuv `terminate`/`kill`, but not for the shared JVM/Python `terminate` path because `low_level_pipe_ownership_case` wrote to stdin before `terminate(proc)`. This round moved that ownership probe after `terminate(proc)` and before explicit pipe closure.","schema_version":1,"source_design_doc_path":"docs/design/2365-specify-the-portable-process-stop-and-status-contract.md","steps":[{"assertion_tests":["Strengthened assertions for `poll` returning `None` before a bounded child exits and stable `Some(code)` after status is recorded.","Strengthened assertions for negative, zero, tiny positive, and oversized `wait_timeout` durations without consuming the later `wait` result.","Kept and corrected helper assertions for `with_process` success, non-zero child exit not invoking `on_error`, caller-domain failure precedence, already-exited cleanup, zero-grace kill escalation, returned pipe-handle closure, and caller-owned handle preservation."],"completion_notes_markdown":"Edited `test_workspace/Bosatsu/IO/ProcessWaitMain.bosatsu`. Verification in step 3 exposed that new failure-path assertions were using raw `String` errors inside a `Prog[IOError, Bool]`; this round corrected those branches to use `InvalidArgument`, including the low-level missing-stdin branch and the `with_process_use_failure_case` caller/cleanup error assertions. Pre-PR review finding F1 later showed this completed step only proved shared ownership after non-stop status operations, because it probed stdin before calling `terminate`.","description_markdown":"Update `test_workspace/Bosatsu/IO/ProcessWaitMain.bosatsu` in place so the shared process regression program explicitly covers the low-level status and helper contract for both JVM evaluation and Python generation/evaluation. Keep child commands bounded and argv-based; prefer `python3 -c ...` and existing portable commands already used by the test program. Add small local test helpers only when they reduce duplication in the invariant checks, and keep the resulting program readable enough for failures to map back to one contract clause.","invariants":["After any operation records a final child status, every later `wait`, `poll`, and `wait_timeout` observation returns the same normalized code.","`wait_timeout` returning `None` never consumes or invalidates the eventual final status.","`terminate` and `kill` return `AlreadyExited` after status has been recorded, and a stop request sent to a running child is followed by a stable non-zero final status.","Low-level `poll`, `wait_timeout`, and `wait` do not implicitly close returned stdio pipe handles.","`with_process` closes only the `SpawnResult`-owned pipe handles, stops/reaps a still-running direct child, and preserves caller-domain error precedence."],"property_tests":["Added a compact shared helper, `post_recorded_status_is_stable`, that is reused across natural zero exit, natural non-zero exit, timeout-before-wait, terminate-before-wait, and kill-before-wait cases so each case asserts convergence to one stable final status.","Added `low_level_pipe_ownership_case`, which performs low-level status operations on a process with `Pipe` stdio and verifies the returned stdin pipe remains usable until the test explicitly closes it."],"status":"completed","step_id":"1","title":"Strengthen shared JVM/Python contract coverage"},{"assertion_tests":["Strengthened C assertions for direct `terminate` and direct `kill` followed by `wait` returning a non-zero status, then stable `poll`, `wait_timeout`, and repeated `wait` observations.","Strengthened C assertions for `poll` before exit and after recorded exit, including repeated post-exit poll observations.","Strengthened C assertions for `wait_timeout` timeout followed by final `wait`, including zero/non-positive timeout behavior and stable post-exit timeout observations.","Added focused POSIX-guarded C assertions that low-level `poll`, zero-duration `wait_timeout`, `terminate`, and `kill` do not implicitly close or drain returned pipe handles by writing through a caller-owned stdin pipe after those operations."],"completion_notes_markdown":"Edited `c_runtime/test.c` only. The first focused run exposed a test wiring bug in the new already-exited closure slot count, which was fixed in the same file. `git diff --check` passed. `make -C c_runtime test_out` passed. Later ownership work added the analogous C/libuv `kill` coverage; the remaining F1 gap was only in the shared JVM/Python `terminate` case.","description_markdown":"Extend `c_runtime/test.c` near the existing IO/Core process tests so the C/libuv backend has focused coverage for the low-level contract clauses that are not covered by the shared JVM/Python test program. Keep platform-sensitive tests inside the existing non-Windows guard or equivalent guards, and avoid widening runtime implementation scope unless a test exposes a correctness bug that is small enough to fix in this PR under the 1000 LoC heuristic.","invariants":["C/libuv process status remains write-once and stable across repeated `wait`, `poll`, and `wait_timeout` observations.","C/libuv timeout requests that return `None` leave the process waitable and observable by later status operations.","C/libuv `poll`, zero-duration `wait_timeout`, `terminate`, and `kill` do not close or drain returned stdio handles.","Already-recorded process exit is reported as `AlreadyExited` for both `terminate` and `kill`."],"property_tests":["Added reusable C post-recorded status assertion helpers that check repeated `poll`, zero-duration `wait_timeout`, and repeated `wait` against one cached final status after different first observations.","Reused the stable-status helper from natural exit, timeout-before-wait, terminate-before-wait, kill-before-wait, and already-exited stop paths so the invariant is asserted consistently rather than as one-off checks."],"status":"completed","step_id":"2","title":"Mirror low-level gaps in C/libuv tests"},{"assertion_tests":["Ran `make -C c_runtime test_out`: passed/up-to-date.","Ran `sbt -batch cli/assembly` to create the local CLI assembly required by `./test_python.sh`.","Ran `./test_python.sh`: passed, including Python generation/evaluation of `ProcessWaitMain`.","Ran `scripts/test_basic.sh` after `sbt clean`: passed with CLI tests `74/74` and core JVM tests `2118/2118` with `2` ignored.","Ran `git diff --check`: passed."],"completion_notes_markdown":"Focused C verification passed with `make -C c_runtime test_out`. Initial `./test_python.sh` failed because the checkout had no CLI assembly jar. The first required-gate run exposed raw string `raise_error` calls in the new `ProcessWaitMain.bosatsu` coverage; this round fixed those directly coupled type errors by using `InvalidArgument` values. Because `EvaluationTest` embeds Bosatsu workspace files at Scala compile time via `Predef.loadFileInCompile`, stale test output still showed the old source until `sbt clean` was run. Final verification at this stage passed: `scripts/test_basic.sh` passed with CLI tests `74/74` and core JVM tests `2118/2118` with `2` ignored; `sbt -batch cli/assembly` passed; `./test_python.sh` passed; `make -C c_runtime test_out` passed/up-to-date; and `git diff --check` passed.","description_markdown":"Run the smallest useful verification loop while developing, then finish with both the focused C runtime target and the repository-required test gate. Because the branch changes cross-backend coverage, also run the existing Python flow that executes `ProcessWaitMain` after transpilation. This checkout may need `sbt cli/assembly` or the required gate to produce the `bosatsuj` assembly before `./test_python.sh` can run successfully.","invariants":["The final branch remains shippable only if `scripts/test_basic.sh` passes within the configured 2400 second timeout.","Focused backend tests should fail close to the changed coverage when a process contract regression is introduced.","The test suite must not rely on unbounded sleeps, shell-only behavior in shared JVM/Python coverage, or platform assumptions outside guarded C tests."],"property_tests":["The property-style/table-driven coverage added in steps 1 and 2 runs as part of the normal shared JVM/Python and C test entry points, not as ad hoc manual checks."],"status":"completed","step_id":"3","title":"Run focused and required verification"},{"assertion_tests":["F1 shared path now calls `terminate(proc)` before the returned stdin ownership probe, so a backend regression that closes returned pipe handles during `terminate` should fail the test.","After the post-terminate ownership probe, stdin/stdout/stderr are explicitly closed, `wait(proc)` completes, the stopped status is non-zero, and later status observations remain stable.","Moved the previous pre-terminate stdin usability probe so the terminate-specific assertion cannot pass without using a returned handle after `terminate`."],"completion_notes_markdown":"Edited `test_workspace/Bosatsu/IO/ProcessWaitMain.bosatsu` only. In `low_level_pipe_ownership_case`, `terminate(proc)` now runs after the existing pre-stop `poll` and zero-duration `wait_timeout` checks and before `stdin_write_ok`; returned stdin/stdout/stderr are still explicitly closed before reaping and stable-status assertions. No C/libuv or shared `kill` edits were needed.","description_markdown":"Address pre-PR review finding F1 by revising the existing shared low-level ownership coverage in `test_workspace/Bosatsu/IO/ProcessWaitMain.bosatsu`. In `low_level_pipe_ownership_case`, keep the existing pre-stop `poll` and zero-duration `wait_timeout` checks, but call `terminate(proc)` while returned `stdin_h`, `stdout_h`, and `stderr_h` are still open. Only after `terminate` returns should the test prove the returned stdin handle remains caller-owned by successfully using it, then explicitly close stdin/stdout/stderr, reap the child, and assert stable post-stop status. Do not duplicate the already-covered shared `kill` path or the C/libuv stop-ownership checks unless the edit exposes a directly coupled issue.","invariants":["F1: shared JVM/Python `terminate` must not close or invalidate returned `Pipe` handles; the ownership probe must happen after `terminate(proc)` and before explicit close.","Low-level `poll`, zero-duration `wait_timeout`, `terminate`, and `kill` should each have at least one regression path proving returned stdio handles remain caller-owned until explicit close.","The revised terminate ownership case must still reap the child and preserve stable post-stop status observations so it cannot leave a live child behind.","The shared JVM/Python path should remain argv-based and bounded, with no shell-specific assumptions."],"property_tests":["Revised the existing shared Bosatsu `low_level_pipe_ownership_case` rather than adding an unrelated new case: the same process checks pre-stop status observations, calls `terminate`, then probes stdin ownership before explicit close.","Kept the already-present shared `low_level_kill_pipe_ownership_case` as the sibling stop-operation ownership property for `kill`."],"status":"completed","step_id":"4","title":"Close shared terminate stdio ownership gap"},{"assertion_tests":["Ran `git diff --check`: passed.","Ran `./test_python.sh`: passed, including Python generation/evaluation of `ProcessWaitMain`.","Ran `scripts/test_basic.sh`: passed with CLI tests `74/74` and core JVM tests `2118/2118` with `2` ignored.","Did not rerun `make -C c_runtime test_out` in this round because the F1 repair touched only the shared Bosatsu test program and no C/libuv files or generated artifacts."],"completion_notes_markdown":"Verification after the F1 repair passed. `git diff --check` passed, `./test_python.sh` passed, and the configured required gate `scripts/test_basic.sh` passed within the 2400 second timeout with CLI tests `74/74` and core JVM tests `2118/2118` with `2` ignored. The only remaining worktree change is `test_workspace/Bosatsu/IO/ProcessWaitMain.bosatsu`.","description_markdown":"After step 4 changes, rerun the focused and required verification commands that cover the changed shared Bosatsu test program. Use focused checks first to catch Bosatsu typing or runtime-flow mistakes close to the edited test, then finish with the repository gate required by the issue configuration. Since C code does not need to change for F1 unless a directly coupled issue is found, the C target can be rerun as a focused regression check but should not drive unrelated scope expansion.","invariants":["The shared JVM/Python `ProcessWaitMain` coverage must pass in both JVM/basic and Python generation/evaluation flows after the terminate ownership helper is changed.","`scripts/test_basic.sh` remains the final required gate for the branch within the configured timeout.","`git diff --check` must pass after the plan and test edits.","Focused backend checks should stay aligned with changed files and should not rely on unbounded sleeps or platform assumptions."],"property_tests":["The F1 ownership property added in step 4 runs through the normal shared JVM/Python test entry points, not as a manual-only inspection."],"status":"completed","step_id":"5","title":"Re-run cross-backend verification after F1 repair"}],"summary_markdown":"Add durable regression coverage for the portable process stop/status contract and the managed cleanup helper across the supported runtime paths. The branch now also closes pre-PR review finding F1 by proving the shared JVM/Python low-level `terminate` path leaves returned stdio handles caller-owned until explicit close.","technical_debt_notes":null} diff --git a/docs/code-plans/2376-add-cross-backend-process-stop-and-cleanup-regression-coverage.md b/docs/code-plans/2376-add-cross-backend-process-stop-and-cleanup-regression-coverage.md new file mode 100644 index 000000000..7b3ceda37 --- /dev/null +++ b/docs/code-plans/2376-add-cross-backend-process-stop-and-cleanup-regression-coverage.md @@ -0,0 +1,159 @@ +# Code Plan #2376 + +> Generated from code plan JSON. +> Edit the `.json` file, not this `.md` file. + +## Metadata + +- Flow: `small_job` +- Issue: `#2376` Add cross-backend process stop and cleanup regression coverage +- Source design doc: `docs/design/2365-specify-the-portable-process-stop-and-status-contract.md` +- Pending steps: `0` +- Completed steps: `5` +- Total steps: `5` + +## Summary + +Add durable regression coverage for the portable process stop/status contract and the managed cleanup helper across the supported runtime paths. The branch now also closes pre-PR review finding F1 by proving the shared JVM/Python low-level `terminate` path leaves returned stdio handles caller-owned until explicit close. + +## Current State + +The merged dependencies have already added the public low-level process APIs (`StopResult`, `terminate`, `kill`, `poll`, `wait_timeout`) and the higher-level `with_process` helper in `test_workspace/Bosatsu/IO/Core.bosatsu`. This branch has shared JVM/Python coverage for stable status observations, timeout non-consumption, already-exited stop behavior, terminate/kill stable post-stop status, low-level pipe ownership after non-stop status operations, shared `terminate` and `kill` pipe ownership after stop, and helper-owned versus caller-owned handle cleanup. C/libuv coverage includes reusable post-recorded status assertions and focused low-level ownership regressions for `poll`, zero-duration `wait_timeout`, `terminate`, and `kill`. + +## Problem + +Issue #2361's acceptance criteria require the cross-backend regression suite to make the low-level stdio ownership contract explicit: low-level stop/status functions must not close returned stdio handles, and callers remain responsible for closing those handles. The previous candidate proved this for non-stop status operations, for shared `kill`, and for C/libuv `terminate`/`kill`, but not for the shared JVM/Python `terminate` path because `low_level_pipe_ownership_case` wrote to stdin before `terminate(proc)`. This round moved that ownership probe after `terminate(proc)` and before explicit pipe closure. + +## Steps + +1. [x] `1` Strengthen shared JVM/Python contract coverage + +Update `test_workspace/Bosatsu/IO/ProcessWaitMain.bosatsu` in place so the shared process regression program explicitly covers the low-level status and helper contract for both JVM evaluation and Python generation/evaluation. Keep child commands bounded and argv-based; prefer `python3 -c ...` and existing portable commands already used by the test program. Add small local test helpers only when they reduce duplication in the invariant checks, and keep the resulting program readable enough for failures to map back to one contract clause. + +#### Invariants + +- After any operation records a final child status, every later `wait`, `poll`, and `wait_timeout` observation returns the same normalized code. +- `wait_timeout` returning `None` never consumes or invalidates the eventual final status. +- `terminate` and `kill` return `AlreadyExited` after status has been recorded, and a stop request sent to a running child is followed by a stable non-zero final status. +- Low-level `poll`, `wait_timeout`, and `wait` do not implicitly close returned stdio pipe handles. +- `with_process` closes only the `SpawnResult`-owned pipe handles, stops/reaps a still-running direct child, and preserves caller-domain error precedence. + +#### Property Tests + +- Added a compact shared helper, `post_recorded_status_is_stable`, that is reused across natural zero exit, natural non-zero exit, timeout-before-wait, terminate-before-wait, and kill-before-wait cases so each case asserts convergence to one stable final status. +- Added `low_level_pipe_ownership_case`, which performs low-level status operations on a process with `Pipe` stdio and verifies the returned stdin pipe remains usable until the test explicitly closes it. + +#### Assertion Tests + +- Strengthened assertions for `poll` returning `None` before a bounded child exits and stable `Some(code)` after status is recorded. +- Strengthened assertions for negative, zero, tiny positive, and oversized `wait_timeout` durations without consuming the later `wait` result. +- Kept and corrected helper assertions for `with_process` success, non-zero child exit not invoking `on_error`, caller-domain failure precedence, already-exited cleanup, zero-grace kill escalation, returned pipe-handle closure, and caller-owned handle preservation. + +#### Completion Notes + +Edited `test_workspace/Bosatsu/IO/ProcessWaitMain.bosatsu`. Verification in step 3 exposed that new failure-path assertions were using raw `String` errors inside a `Prog[IOError, Bool]`; this round corrected those branches to use `InvalidArgument`, including the low-level missing-stdin branch and the `with_process_use_failure_case` caller/cleanup error assertions. Pre-PR review finding F1 later showed this completed step only proved shared ownership after non-stop status operations, because it probed stdin before calling `terminate`. + +2. [x] `2` Mirror low-level gaps in C/libuv tests + +Extend `c_runtime/test.c` near the existing IO/Core process tests so the C/libuv backend has focused coverage for the low-level contract clauses that are not covered by the shared JVM/Python test program. Keep platform-sensitive tests inside the existing non-Windows guard or equivalent guards, and avoid widening runtime implementation scope unless a test exposes a correctness bug that is small enough to fix in this PR under the 1000 LoC heuristic. + +#### Invariants + +- C/libuv process status remains write-once and stable across repeated `wait`, `poll`, and `wait_timeout` observations. +- C/libuv timeout requests that return `None` leave the process waitable and observable by later status operations. +- C/libuv `poll`, zero-duration `wait_timeout`, `terminate`, and `kill` do not close or drain returned stdio handles. +- Already-recorded process exit is reported as `AlreadyExited` for both `terminate` and `kill`. + +#### Property Tests + +- Added reusable C post-recorded status assertion helpers that check repeated `poll`, zero-duration `wait_timeout`, and repeated `wait` against one cached final status after different first observations. +- Reused the stable-status helper from natural exit, timeout-before-wait, terminate-before-wait, kill-before-wait, and already-exited stop paths so the invariant is asserted consistently rather than as one-off checks. + +#### Assertion Tests + +- Strengthened C assertions for direct `terminate` and direct `kill` followed by `wait` returning a non-zero status, then stable `poll`, `wait_timeout`, and repeated `wait` observations. +- Strengthened C assertions for `poll` before exit and after recorded exit, including repeated post-exit poll observations. +- Strengthened C assertions for `wait_timeout` timeout followed by final `wait`, including zero/non-positive timeout behavior and stable post-exit timeout observations. +- Added focused POSIX-guarded C assertions that low-level `poll`, zero-duration `wait_timeout`, `terminate`, and `kill` do not implicitly close or drain returned pipe handles by writing through a caller-owned stdin pipe after those operations. + +#### Completion Notes + +Edited `c_runtime/test.c` only. The first focused run exposed a test wiring bug in the new already-exited closure slot count, which was fixed in the same file. `git diff --check` passed. `make -C c_runtime test_out` passed. Later ownership work added the analogous C/libuv `kill` coverage; the remaining F1 gap was only in the shared JVM/Python `terminate` case. + +3. [x] `3` Run focused and required verification + +Run the smallest useful verification loop while developing, then finish with both the focused C runtime target and the repository-required test gate. Because the branch changes cross-backend coverage, also run the existing Python flow that executes `ProcessWaitMain` after transpilation. This checkout may need `sbt cli/assembly` or the required gate to produce the `bosatsuj` assembly before `./test_python.sh` can run successfully. + +#### Invariants + +- The final branch remains shippable only if `scripts/test_basic.sh` passes within the configured 2400 second timeout. +- Focused backend tests should fail close to the changed coverage when a process contract regression is introduced. +- The test suite must not rely on unbounded sleeps, shell-only behavior in shared JVM/Python coverage, or platform assumptions outside guarded C tests. + +#### Property Tests + +- The property-style/table-driven coverage added in steps 1 and 2 runs as part of the normal shared JVM/Python and C test entry points, not as ad hoc manual checks. + +#### Assertion Tests + +- Ran `make -C c_runtime test_out`: passed/up-to-date. +- Ran `sbt -batch cli/assembly` to create the local CLI assembly required by `./test_python.sh`. +- Ran `./test_python.sh`: passed, including Python generation/evaluation of `ProcessWaitMain`. +- Ran `scripts/test_basic.sh` after `sbt clean`: passed with CLI tests `74/74` and core JVM tests `2118/2118` with `2` ignored. +- Ran `git diff --check`: passed. + +#### Completion Notes + +Focused C verification passed with `make -C c_runtime test_out`. Initial `./test_python.sh` failed because the checkout had no CLI assembly jar. The first required-gate run exposed raw string `raise_error` calls in the new `ProcessWaitMain.bosatsu` coverage; this round fixed those directly coupled type errors by using `InvalidArgument` values. Because `EvaluationTest` embeds Bosatsu workspace files at Scala compile time via `Predef.loadFileInCompile`, stale test output still showed the old source until `sbt clean` was run. Final verification at this stage passed: `scripts/test_basic.sh` passed with CLI tests `74/74` and core JVM tests `2118/2118` with `2` ignored; `sbt -batch cli/assembly` passed; `./test_python.sh` passed; `make -C c_runtime test_out` passed/up-to-date; and `git diff --check` passed. + +4. [x] `4` Close shared terminate stdio ownership gap + +Address pre-PR review finding F1 by revising the existing shared low-level ownership coverage in `test_workspace/Bosatsu/IO/ProcessWaitMain.bosatsu`. In `low_level_pipe_ownership_case`, keep the existing pre-stop `poll` and zero-duration `wait_timeout` checks, but call `terminate(proc)` while returned `stdin_h`, `stdout_h`, and `stderr_h` are still open. Only after `terminate` returns should the test prove the returned stdin handle remains caller-owned by successfully using it, then explicitly close stdin/stdout/stderr, reap the child, and assert stable post-stop status. Do not duplicate the already-covered shared `kill` path or the C/libuv stop-ownership checks unless the edit exposes a directly coupled issue. + +#### Invariants + +- F1: shared JVM/Python `terminate` must not close or invalidate returned `Pipe` handles; the ownership probe must happen after `terminate(proc)` and before explicit close. +- Low-level `poll`, zero-duration `wait_timeout`, `terminate`, and `kill` should each have at least one regression path proving returned stdio handles remain caller-owned until explicit close. +- The revised terminate ownership case must still reap the child and preserve stable post-stop status observations so it cannot leave a live child behind. +- The shared JVM/Python path should remain argv-based and bounded, with no shell-specific assumptions. + +#### Property Tests + +- Revised the existing shared Bosatsu `low_level_pipe_ownership_case` rather than adding an unrelated new case: the same process checks pre-stop status observations, calls `terminate`, then probes stdin ownership before explicit close. +- Kept the already-present shared `low_level_kill_pipe_ownership_case` as the sibling stop-operation ownership property for `kill`. + +#### Assertion Tests + +- F1 shared path now calls `terminate(proc)` before the returned stdin ownership probe, so a backend regression that closes returned pipe handles during `terminate` should fail the test. +- After the post-terminate ownership probe, stdin/stdout/stderr are explicitly closed, `wait(proc)` completes, the stopped status is non-zero, and later status observations remain stable. +- Moved the previous pre-terminate stdin usability probe so the terminate-specific assertion cannot pass without using a returned handle after `terminate`. + +#### Completion Notes + +Edited `test_workspace/Bosatsu/IO/ProcessWaitMain.bosatsu` only. In `low_level_pipe_ownership_case`, `terminate(proc)` now runs after the existing pre-stop `poll` and zero-duration `wait_timeout` checks and before `stdin_write_ok`; returned stdin/stdout/stderr are still explicitly closed before reaping and stable-status assertions. No C/libuv or shared `kill` edits were needed. + +5. [x] `5` Re-run cross-backend verification after F1 repair + +After step 4 changes, rerun the focused and required verification commands that cover the changed shared Bosatsu test program. Use focused checks first to catch Bosatsu typing or runtime-flow mistakes close to the edited test, then finish with the repository gate required by the issue configuration. Since C code does not need to change for F1 unless a directly coupled issue is found, the C target can be rerun as a focused regression check but should not drive unrelated scope expansion. + +#### Invariants + +- The shared JVM/Python `ProcessWaitMain` coverage must pass in both JVM/basic and Python generation/evaluation flows after the terminate ownership helper is changed. +- `scripts/test_basic.sh` remains the final required gate for the branch within the configured timeout. +- `git diff --check` must pass after the plan and test edits. +- Focused backend checks should stay aligned with changed files and should not rely on unbounded sleeps or platform assumptions. + +#### Property Tests + +- The F1 ownership property added in step 4 runs through the normal shared JVM/Python test entry points, not as a manual-only inspection. + +#### Assertion Tests + +- Ran `git diff --check`: passed. +- Ran `./test_python.sh`: passed, including Python generation/evaluation of `ProcessWaitMain`. +- Ran `scripts/test_basic.sh`: passed with CLI tests `74/74` and core JVM tests `2118/2118` with `2` ignored. +- Did not rerun `make -C c_runtime test_out` in this round because the F1 repair touched only the shared Bosatsu test program and no C/libuv files or generated artifacts. + +#### Completion Notes + +Verification after the F1 repair passed. `git diff --check` passed, `./test_python.sh` passed, and the configured required gate `scripts/test_basic.sh` passed within the 2400 second timeout with CLI tests `74/74` and core JVM tests `2118/2118` with `2` ignored. The only remaining worktree change is `test_workspace/Bosatsu/IO/ProcessWaitMain.bosatsu`. diff --git a/test_workspace/Bosatsu/IO/ProcessWaitMain.bosatsu b/test_workspace/Bosatsu/IO/ProcessWaitMain.bosatsu index 1e26d929e..653acfbec 100644 --- a/test_workspace/Bosatsu/IO/ProcessWaitMain.bosatsu +++ b/test_workspace/Bosatsu/IO/ProcessWaitMain.bosatsu @@ -12,12 +12,14 @@ from Bosatsu/Prog import ( set, get, ) -from Bosatsu/IO/Error import IOError +from Bosatsu/IO/Error import IOError, InvalidArgument from Bosatsu/IO/Std import show_error from Bosatsu/IO/Core import ( Handle, + Process, StdioConfig, Pipe, + UseHandle, TempFile, Read, SpawnResult, @@ -38,7 +40,6 @@ from Bosatsu/IO/Core import ( poll, wait_timeout, with_process, - now_mono, ) def stop_result_eq(left: StopResult, right: StopResult) -> Bool: @@ -60,51 +61,62 @@ sleep_args: List[String] = ["-c", "import time; time.sleep(10)"] short_sleep_args: List[String] = ["-c", "import time; time.sleep(0.2)"] -def exited_stop_case() -> Prog[IOError, Bool]: +def post_recorded_status_is_stable(proc: Process, code: Int) -> Prog[IOError, Bool]: ( - SpawnResult(proc, ...) <- spawn("true", [], StdioConfig(Pipe, Pipe, Pipe)).await() - first <- wait(proc).await() + second <- wait(proc).await() poll_after <- poll(proc).await() - timeout_after <- wait_timeout(proc, duration_from_nanos(-1)).await() + zero_timeout_after <- wait_timeout(proc, duration_from_nanos(0)).await() + negative_timeout_after <- wait_timeout(proc, duration_from_nanos(-1)).await() terminated <- terminate(proc).await() killed <- kill(proc).await() - second <- wait(proc).await() + third <- wait(proc).await() pure(and( - first.eq_Int(0), + second.eq_Int(code), and( - option_code_eq(poll_after, Some(0)), + option_code_eq(poll_after, Some(code)), and( - option_code_eq(timeout_after, Some(0)), + option_code_eq(zero_timeout_after, Some(code)), and( - stop_result_eq(terminated, AlreadyExited), - and(stop_result_eq(killed, AlreadyExited), second.eq_Int(0)), + option_code_eq(negative_timeout_after, Some(code)), + and( + stop_result_eq(terminated, AlreadyExited), + and(stop_result_eq(killed, AlreadyExited), third.eq_Int(code)), + ), ), ), ), )) ) +def exited_stop_case() -> Prog[IOError, Bool]: + ( + SpawnResult(proc, ...) <- spawn("true", [], StdioConfig(Pipe, Pipe, Pipe)).await() + first <- wait(proc).await() + stable <- post_recorded_status_is_stable(proc, 0).await() + pure(and(first.eq_Int(0), stable)) + ) + def poll_timeout_case() -> Prog[IOError, Bool]: ( SpawnResult(proc, ...) <- spawn("python3", short_sleep_args, StdioConfig(Pipe, Pipe, Pipe)).await() poll_before <- poll(proc).await() + negative_timeout <- wait_timeout(proc, duration_from_nanos(-1)).await() zero_timeout <- wait_timeout(proc, duration_from_nanos(0)).await() tiny_timeout <- wait_timeout(proc, duration_from_nanos(1)).await() first <- wait(proc).await() - poll_after <- poll(proc).await() timeout_after <- wait_timeout(proc, duration_from_nanos(92233720368547758079223372036854775807)).await() - second <- wait(proc).await() + stable <- post_recorded_status_is_stable(proc, first).await() pure(and( option_code_eq(poll_before, None), and( - option_code_eq(zero_timeout, None), + option_code_eq(negative_timeout, None), and( - option_code_eq(tiny_timeout, None), + option_code_eq(zero_timeout, None), and( - first.eq_Int(0), + option_code_eq(tiny_timeout, None), and( - option_code_eq(poll_after, Some(0)), - and(option_code_eq(timeout_after, Some(0)), second.eq_Int(0)), + first.eq_Int(0), + and(option_code_eq(timeout_after, Some(0)), stable), ), ), ), @@ -117,10 +129,10 @@ def terminate_case() -> Prog[IOError, Bool]: SpawnResult(proc, ...) <- spawn("python3", sleep_args, StdioConfig(Pipe, Pipe, Pipe)).await() stopped <- terminate(proc).await() first <- wait(proc).await() - second <- wait(proc).await() + stable <- post_recorded_status_is_stable(proc, first).await() pure(and( stop_result_eq(stopped, StopSent), - and(is_nonzero(first), first.eq_Int(second)), + and(is_nonzero(first), stable), )) ) @@ -129,62 +141,102 @@ def kill_case() -> Prog[IOError, Bool]: SpawnResult(proc, ...) <- spawn("python3", sleep_args, StdioConfig(Pipe, Pipe, Pipe)).await() stopped <- kill(proc).await() first <- wait(proc).await() - second <- wait(proc).await() + stable <- post_recorded_status_is_stable(proc, first).await() pure(and( stop_result_eq(stopped, StopSent), - and(is_nonzero(first), first.eq_Int(second)), + and(is_nonzero(first), stable), )) ) -def stop_result_observed(sr: StopResult) -> Bool: - match sr: - case StopSent: True - case AlreadyExited: True - -def option_code_observed(code: Option[Int]) -> Bool: - match code: - case Some(_): True - case None: False - def stable_wait_case(cmd: String, code: Int) -> Prog[IOError, Bool]: ( SpawnResult(proc, ...) <- spawn(cmd, [], StdioConfig(Pipe, Pipe, Pipe)).await() - timeout <- now_mono.await() - polled <- ( - if False: - poll(proc) - else: - pure(None) + first <- wait(proc).await() + stable <- post_recorded_status_is_stable(proc, code).await() + pure(and(first.eq_Int(code), stable)) + ) + +def low_level_pipe_ownership_case() -> Prog[IOError, Bool]: + ( + SpawnResult(proc, stdin_h, stdout_h, stderr_h) <- spawn( + "python3", + sleep_args, + StdioConfig(Pipe, Pipe, Pipe), + ).await() + poll_before <- poll(proc).await() + timeout_before <- wait_timeout(proc, duration_from_nanos(0)).await() + stopped <- terminate(proc).await() + stdin_write_ok <- recover( + ( + _ <- (match stdin_h: + case Some(h): write_utf8(h, "") + case None: raise_error(InvalidArgument("missing stdin pipe")) + ).await() + pure(True) + ), + _ -> pure(False) ).await() - timed <- ( - if False: - wait_timeout(proc, timeout) - else: - pure(None) + _ <- (match stdin_h: + case Some(h): close(h) + case None: pure(()) ).await() - terminated <- ( - if False: - terminate(proc) - else: - pure(StopSent) + _ <- (match stdout_h: + case Some(h): close(h) + case None: pure(()) ).await() - killed <- ( - if False: - kill(proc) - else: - pure(AlreadyExited) + _ <- (match stderr_h: + case Some(h): close(h) + case None: pure(()) ).await() first <- wait(proc).await() - second <- wait(proc).await() + stable <- post_recorded_status_is_stable(proc, first).await() pure(and( - or( - option_code_observed(polled), - or( - option_code_observed(timed), - and(stop_result_observed(terminated), stop_result_observed(killed)), + option_code_eq(poll_before, None), + and( + option_code_eq(timeout_before, None), + and( + stdin_write_ok, + and(stop_result_eq(stopped, StopSent), and(is_nonzero(first), stable)), ), ), - and(first.eq_Int(code), second.eq_Int(code)), + )) + ) + +def low_level_kill_pipe_ownership_case() -> Prog[IOError, Bool]: + ( + SpawnResult(proc, stdin_h, stdout_h, stderr_h) <- spawn( + "python3", + sleep_args, + StdioConfig(Pipe, Pipe, Pipe), + ).await() + stopped <- kill(proc).await() + stdin_write_ok <- recover( + ( + _ <- (match stdin_h: + case Some(h): write_utf8(h, "") + case None: raise_error(InvalidArgument("missing stdin pipe")) + ).await() + pure(True) + ), + _ -> pure(False) + ).await() + _ <- (match stdin_h: + case Some(h): close(h) + case None: pure(()) + ).await() + _ <- (match stdout_h: + case Some(h): close(h) + case None: pure(()) + ).await() + _ <- (match stderr_h: + case Some(h): close(h) + case None: pure(()) + ).await() + first <- wait(proc).await() + stable <- post_recorded_status_is_stable(proc, first).await() + pure(and( + stop_result_eq(stopped, StopSent), + and(stdin_write_ok, and(is_nonzero(first), stable)), )) ) @@ -258,10 +310,10 @@ def with_process_use_failure_case() -> Prog[IOError, Bool]: sleep_args, StdioConfig(Pipe, Pipe, Pipe), duration_from_nanos(0), - _ -> raise_error("helper-owned error"), - _ -> raise_error("use-failed"), + _ -> raise_error(InvalidArgument("helper-owned error")), + _ -> raise_error(InvalidArgument("use-failed")), ), - err -> pure(err matches "use-failed") + err -> pure(err matches InvalidArgument("use-failed")) ) def with_process_already_exited_case() -> Prog[IOError, Bool]: @@ -326,7 +378,7 @@ def with_process_caller_owned_handle_case() -> Prog[IOError, Bool]: result <- with_process( "true", [], - StdioConfig(Pipe, Pipe, Pipe), + StdioConfig(UseHandle(handle), Pipe, Pipe), duration_from_nanos(1000000), _ -> pure(31), _ -> pure(31), @@ -349,6 +401,8 @@ run_test: Prog[IOError, Int] = poll_timeout_ok <- poll_timeout_case().await() terminate_ok <- terminate_case().await() kill_ok <- kill_case().await() + low_level_pipe_ownership_ok <- low_level_pipe_ownership_case().await() + low_level_kill_pipe_ownership_ok <- low_level_kill_pipe_ownership_case().await() with_process_success_ok <- with_process_success_case().await() with_process_nonzero_exit_ok <- with_process_nonzero_exit_case().await() with_process_use_failure_ok <- with_process_use_failure_case().await() @@ -362,7 +416,16 @@ run_test: Prog[IOError, Int] = nonzero_ok, and( exited_stop_ok, - and(poll_timeout_ok, and(terminate_ok, kill_ok)), + and( + poll_timeout_ok, + and( + terminate_ok, + and( + kill_ok, + and(low_level_pipe_ownership_ok, low_level_kill_pipe_ownership_ok), + ), + ), + ), ), ), )