Skip to content

hy-emit: fix O8 slot-loan sibling-branch handoff and shadowing binder last-use (#546, #547) - #559

Merged
limitlessprojects merged 1 commit into
limitlessprojects:mainfrom
Khanhtnq:fix/o8-slot-loan-flush-546-547
Oct 18, 2026
Merged

limitlessprojects merged 1 commit into
limitlessprojects:mainfrom
Khanhtnq:fix/o8-slot-loan-flush-546-547

Conversation

@Khanhtnq

Copy link
Copy Markdown
Contributor

Fixes #546
Fixes #547

Summary

This PR resolves two P0 soundness bugs in O8 map/slice slot-loan store-back emission (compiler/crates/hy-emit/src/stmt.rs):

  1. Sibling-branch / nested control-flow store-back ordering ([soundness] P0: O8 slot-loan store-back emitted after a sibling-branch move — accepted program races on the moved map #546):

    • Previously, emit_block_inner decided whether to flush a slot loan after statement i solely by checking whether the loan binder v had no remaining mentions in stmts[i + 1..] (or before a top-level Stmt::Task / Stmt::Send).
    • When stmts[i] was a branching or compound statement (if, match, select, block, managed, for) whose one branch last-used v and whose sibling branch moved m (task worker(move m) / ch <- move m), mutated m (delete(m, k), clear(m), m[k] = ...), or read m after the loan's last use in the same branch, the outer emit_block_inner kept the loan on the outer scope stack and emitted m[k] = v after the entire compound statement?racing with concurrent tasks or overwriting delete/clear/subsequent reads.
    • Fix:
      • Introduced branch_inherit handoff (inherit_loans_into_branch / stmt_needs_branch_loan_handoff / stmt_crosses_collection_boundary / block_reads_ident_after_last_mention_of) across Stmt::If (including else if chains and synthetic else branches when else_ is omitted), Stmt::Match (synthesizing _ / None fallthrough arms when needed), Stmt::Select (pre-flushing before select if a Send arm moves the collection), Stmt::Block, Stmt::Managed, and Stmt::For.
      • Saved and restored branch_inherit across Expr::FnLit emission (compiler/crates/hy-emit/src/expr.rs) so closure literals inside condition/header expressions cannot consume pending branch handoffs.
      • Pre-flushes the loan before the statement when its header/init/scrutinee expression itself moves the collection or binds a name shadowing the loan variable or collection.
  2. Shadowing loop / select / if-init binders defeating non-lexical last-use flush ([soundness] P0: shadowing loop binder defeats the O8 last-use flush — store-back deferred past task worker(move m), data race #547):

    • Previously, stmt_mentions_ident and block_mentions_ident walked into ForKind::Range, ForKind::Iterate, SelectArmKind::Recv, and Stmt::If bodies without checking whether a header binder (for n in 0..3, for k, n in xs, select { n := <-ch: ... }, if n := ...; cond) shadowed the outer loan binder n.
    • Because the inner loop/arm/branch body mentioned the shadowing n, stmt_mentions_ident(stmt, "n") returned true, tricking emit_block_inner into deferring the store-back of the outer loan past task worker(move m) into the inner loop's completion.
    • Fix:
      • Made stmt_mentions_ident and block_mentions_ident shadowing-aware for ForKind::Range (var), ForKind::Iterate (vars), SelectArmKind::Recv (define: true vars), and Stmt::If (init local declarations), while still inspecting the iterable/channel/init expressions evaluated in the outer scope.
      • Checked subsequent statements in block_mentions_ident so a slot-loan rebind inside a nested block stops scanning once shadowed.

Verification

  • Added 7 integration tests in compiler/crates/hy-emit/tests/loan_branch_move.rs covering #546 (if/else sibling move, if without else synthetic store-back, post-loan read inside a branch with and without a sibling move, delete/clear in sibling branches, and match/select/nested block handoffs).
  • Added unit tests in compiler/crates/hy-emit/src/tests.rs covering #547 (ForKind::Range, ForKind::Iterate, SelectArmKind::Recv, and Stmt::If init shadowing).
  • cargo test passes across all workspace crates (hy-emit 164/164 tests, hy-check 60/60 corpus unchanged).
  • python tools/check_test_registration.py and python tools/check_conflict_markers.py pass cleanly.

@Leimiu-G

Copy link
Copy Markdown
Contributor

Reviewed this against the #547 binder class — the sibling-branch half (#546) is the part that is easy to miss, and the flush-before-top-level-Task/Send reasoning holds up.

One shape is still open. Verified on unmodified main (422066b), and still present at a2943034: expr_mentions_ident's Expr::FnLit arm (stmt.rs:2698-2701) filters params but not a closure's named result. A closure that re-declares the loan's name as a result therefore reads as a use of the loan.

Repro — hyb check reports 0 diagnostics:

struct item { x int }

fn worker(m map[string]item, done chan bool) {
    m["w"] = item{x: 1}
    done <- true
}

fn main() {
    m := map[string]item{"a": item{x: 0}}
    done := make(chan bool, 1)
    n := &m["a"]
    n.x = 1
    task worker(move m, done)
    g := fn() (n int) {
        n = 7
        return
    }
    <-done
    fmt.println(g())
}

Emitted on main — the store-back lands after the spawn, so main writes the map the worker owns:

go worker(m, done)
g := func() (n int) {
    n = 7
    return
}
m["a"] = n

Three lines close it (the pattern has to bind results, so { params, body, .. } becomes { params, results, body, .. }):

let binds = params.iter().any(|p| p.name == target)
    || results.iter().any(|r| r.name.as_deref() == Some(target));

PR #551 carries this hunk plus two corpus programs (61/62) that gate the emit order through build+run, so a future refactor of that arm cannot regress silently. No preference on which PR lands — flagging it only so #547 does not close with one shape still open, and so a reviewer does not have to re-derive the shape list.

@Khanhtnq
Khanhtnq force-pushed the fix/o8-slot-loan-flush-546-547 branch from a294303 to ba1f0c8 Compare October 18, 2026 05:23
@Khanhtnq
Khanhtnq force-pushed the fix/o8-slot-loan-flush-546-547 branch from ba1f0c8 to 8759e4e Compare October 18, 2026 13:21
@Khanhtnq

Copy link
Copy Markdown
Contributor Author

Thanks @Leimiu-G — great catch!

We have rebased this branch cleanly onto origin/main (0ca08c2 -> 8759e4e), preserving the results filter on Expr::FnLit in expr_mentions_ident (slot_loan_flushes_before_move_when_closure_named_result_shadows_the_loan_name) alongside the remaining compound-statement (match, select, bare block, managed, for) O8 slot-loan handoff, clear(m) invalidation guard, and remaining_stmts_use_loan rebind awareness in block_mentions_ident.

All hy-emit and hy-check unit & integration suites pass (193/193 in hy-emit, 0 failures).

@Leimiu-G

Copy link
Copy Markdown
Contributor

Re-verified independently on 8759e4e (tarball build, HYB_ALLOW_TOOLCHAIN_DRIFT=1) — your numbers hold exactly, including the pin I asked about:

cargo test -p hy-emit   171 + 1 + 9 + 7 + 3 + 2 = 193 passed / 0 failed
cargo test -p hy-check  all suites ok / 0 failed
slot_loan_flushes_before_move_when_closure_named_result_shadows_the_loan_name ... ok

The results filter on Expr::FnLit is still there and still green, so the shadowing case that motivated it is covered rather than papered over.

I also took it past the unit suites to emitted-Go behaviour, since the whole point of O8 is the store-back and a passing suite cannot show a missing write:

// sibling branch: n is rebound in both arms, loan name shadows the result
fn pick(c *counter, flag bool) int {
    n := 0
    if flag { n = c.hits; n = n + 10 } else { n = c.hits; n = n + 20 }
    return n
}
$ hyb check b2.hy   ->  OK (0 diagnostics)
$ hyb build b2.hy -o p --emit-go && go build && ./pp
sibling: 17 / 27          // 7+10 and 7+20 — both arms see the real backing value

and the plain branch handoff (svc := &e.services[name] … svc.replicas = n) prints branch: 5, i.e. 3 -> 5 lands rather than mutating a copy.

One heads-up for merge order, not a request for changes. This branch touches hy-emit/src/expr.rs +2/-0 at the Expr::FnLit arm (branch_inherit save/restore around line 377), and #631 touches the same file +10/-1 in emit_expr_exp around line 65. Different hunks, so both should merge in either order — flagging it only so a surprise conflict does not read as a real disagreement between the two changes.

Nothing else from my side; this is the stronger take of the #546/#547 family.

@limitlessprojects
limitlessprojects merged commit 46c9df9 into limitlessprojects:main Oct 18, 2026
2 checks passed
limitlessprojects pushed a commit that referenced this pull request Oct 18, 2026
…e-rendered store statement, not re-derive a chained assignment

The #559 merge landed emit-side handoff consumers that formatted
"{place} = {name}" from loan-frame entries whose second element is main's
full store statement ("m[\"a\"] = n" from emit_local's new_loans) - the
synthetic-else / match-none / select-block / pre-flush paths emitted
invalid chained Go (m["a"] = n = n; go build: expected '==', found '=')
for accepted programs, violating GUARANTEES row 13. All 5 sites now push
the stored statement directly. Repro: if-without-else + slot loan +
in-branch slot read (p559t1), match none-arm move (p559t2), block rebind
(p603a, also fixes the stale store-back slot corruption - now prints 10).
Credit: Khanhtnq #559 (fixes #546 #547). Battery: cargo 1505/0, corpus
109/109, differential FULL 36+73, hy-emit 221/0.
@limitlessprojects

Copy link
Copy Markdown
Owner

Landed: merged via API (46c9df9) + maintainer integration repair 37df41f - thank you @Khanhtnq!

Probe evidence on main before landing:

Scenario Main (bf0a560) After #559
#546 if sibling-branch move (your r1) already fixed (branch-local flush, no post-spawn store-back) stays fixed
#547 shadowing loop binder already fixed (store-back before spawn; corpus 62/63) stays fixed
if-without-else: in-branch write then in-branch slot READ (no sibling move) MISCOMPILE - branch read saw stale slot (store-back was after the whole if) store-back lands before the read; synthetic else flushes on the no-taken path
match some-uses/none-moves RACE - single store-back after the match, after go worker on the none path lowers to if/else with arm-local flushes; 3x clean under go run -race
select default-moves / bare block move (your new tests) both flush inside the construct; hy-emit 221->... all green
bonus: block rebind n = &m["b"] then outer stale flush (issue #603 repro 1) slot corruption (m["a"] overwritten with b's copy, printed 20) prints 10

Integration repair (37df41f): the PR's handoff consumers re-derived "{place} = {name}" from loan-frame entries whose 2nd element is main's pre-rendered store statement (m["a"] = n), emitting invalid chained Go (m["a"] = n = n) in the synthetic-else/match-none/pre-flush paths - all 5 sites now push the stored statement directly. Your +212/-83 stmt.rs machinery merged 1:1 otherwise.

Battery on repaired main: cargo 1523/0, corpus 109/109, differential FULL 36+73. fixes #546 fixes #547.

@Khanhtnq

Copy link
Copy Markdown
Contributor Author

@limitlessprojects Thanks! Here are my payout details (whichever method is easiest for you):

  • USDC / SOL (Solana Network): 6mghraUR9NV2fA187VXoLN2rVS3WLA91UhqLfjtvDdmf
  • USDT (TRON / TRC20): TJhLSmGHD33o8UULb2ZX76BDg6gP88pQ5V
  • USDT / USDC / ETH (EVM ? ERC20 / BEP20 / Base / Arbitrum / Polygon): 0xcbEDbeCC127a32217075Ff40f16Ec804aa1E0533
  • BTC (Bitcoin Network): 145aR8RmdZGj4wpeip9wu7XA6zLfLwYqLv
  • Binance Pay / Binance ID: 36989869 (UID / Nickname: Khanhtnq)
  • PayPal: trankhanhkent@gmail.com

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

3 participants