Skip to content

Conversation

@sagjoshi
Copy link

@sagjoshi sagjoshi commented Nov 10, 2025

This PR fixes three functions in src/runtime/uv/net_addr.cpp that incorrectly called array_push() without capturing its return value, violating the Lean runtime API contract. When arrays aren't exclusively owned or need reallocation, array_push() returns a new pointer, but the code continued using the old unmodified pointer, resulting in malformed IP addresses with zero-valued octets and failed network connections. The bug was masked in typical usage because arrays were usually exclusively owned with sufficient capacity, causing in-place modification. The fix changes all three functions to capture the return value (ret = array_push(ret, lean_box(octet))), and enhanced tests now validate that all IP address octets are properly populated. DNS resolution now returns correct addresses and all network operations succeed.

Closes #11128

…ay_push() without capturing its return value, violating the Lean runtime API contract. When arrays aren't exclusively owned or need reallocation, array_push() returns a new pointer, but the code continued using the old unmodified pointer, resulting in malformed IP addresses with zero-valued octets and failed network connections. The bug was masked in typical usage because arrays were usually exclusively owned with sufficient capacity, causing in-place modification. The fix changed all three functions to capture the return value (ret = array_push(ret, lean_box(octet))), and enhanced tests now validate that all IP address octets are properly populated. DNS resolution now returns correct addresses and all network operations succeed.
@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Nov 10, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f74e21e302bb5eaa372a406649e034ae055988e0 --onto d47b474e41e4b134239ef70fa3c15778cc771bcf. You can force Mathlib CI using the force-mathlib-ci label. (2025-11-10 23:42:57)

@leanprover-bot
Copy link
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase f74e21e302bb5eaa372a406649e034ae055988e0 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-11-10 23:42:58)

@TwoFX
Copy link
Member

TwoFX commented Nov 11, 2025

The bug that this PR is supposed to fix was already fixed by #10854. The tests that this PR adds all pass on recent nightlies, and I don't think that they improve test coverage compared to what we already have, so I'll close this PR.

@TwoFX TwoFX closed this Nov 11, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

array_push return values not captured in DNS/network address functions

4 participants