Repository navigation
check(channel_liveness): a function body owns its capability names (fixes #4462) - #4463
Open
jorge123255 wants to merge 1 commit into
Open
jorge123255 wants to merge 1 commit into
jorge123255 wants to merge 1 commit into
Conversation
…ixes limitlessprojects#4462) `ChannelLivenessChecker` keys capabilities by the bare name (`cap_to_pipe`, `pipes_all`) and `pop_scope` promotes a body's `moved_caps` into the file-level scope, while `is_moved` scans the whole stack. So the file-level state outlived the function that produced it: a `move tx` in one function made every LATER function's own `tx` look moved. The trigger is declaration order. Helper-before-main is accepted; main-before- helper is rejected with two `HYB-E3001` — and `tx` is the name the checker's own fix-it text prints, so the rejected spelling is the natural one: fn main() { tx, rx := hy.pipe[int]() task push_three(move tx) for v in rx { fmt.println("{v}") } } fn push_three(tx hy.send_cap[int]) { // same name tx.send(i); tx.close() // rejected: "use of moved linear } // capability 'tx'" Renaming the parameter made the same program pass, which is what pointed at identity-by-name. Both orders are legal programs; only the walk order differed. `check_fn` now saves and restores the three pieces of capability state (`cap_to_pipe`, `pipes_all`, the file-level `moved_caps`) around the body, so a body starts from a clean world. Closures stay inside one function and their promotion still works — a move performed in a closure body still reaches the enclosing function. Six tests: the rejected order now accepts, the renamed control, the closure promotion that must survive, an unclosed SECOND function still rejected (E4004), a closed second function not flagged, and the constant-shape case. Three of them fail on b1627e8 (the acceptance, the closed-second, the constant), the three controls already passed. No corpus fixture: `hy.pipe` has no emit support yet, so a capability program does not reach `go build` and cannot be an ACCEPT corpus entry. Co-authored-by: OpenBot <openbot@openbot.dev>
github-actions
Bot
added
the
bot:land-candidate
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Fixes #4462.
The bug
Capabilities were identified by their bare name across the whole file:
cap_to_pipe/pipes_allare file-wide,pop_scopepromotes a body'smoved_capsinto the file-level scope, andis_movedscans the stack. Nothing reset at a function boundary, so a function inherited the moves (and closed/drained names, and pipe indices) of every function walked before it.That rejected a valid program whenever two functions both call their capability
tx— the name the checker's own fix-it prints:Declaration order alone decided the verdict: helper-above-main passed, main-above-helper failed, and renaming the parameter fixed it — both orders are legal programs.
It is not only noisy: the move also satisfies the terminal invariant, so a later function reusing a moved name loses its
HYB-E4004/E4005check.The fix
check_fnsavescap_to_pipe,pipes_alland the file-levelmoved_caps, clears them for the body, and restores them after. A body starts from a clean world; closures stay inside one body, so the promotion they rely on still works (a test pins that the closure case keeps rejecting).Six tests, three fail on
b1627e8and three are controls that already passed:E4004(guard against over-relaxing);cargo test --workspacegreen,check_corpus_censusgreen (139, unchanged).No corpus fixture:
hy.pipestill has no emit path (hyb buildfails withpackage hy is not in stdon any capability program), so an ACCEPT entry cannot build yet — worth its own issue if this surface is meant to ship.Co-authored-by: OpenBot openbot@openbot.dev