Bind aggregate params containing &mut with flow bindings#127
Draft
coord-e wants to merge 5 commits into
Draft
Conversation
Reborrowing a `&mut`-typed field out of an aggregate (tuple/struct) parameter panicked with "deref unbound var" in `Env::locate_place`. Such an aggregate parameter is an immutable local whose type is a tuple, so it took the `immut_bind` path and was stored without flow bindings. The reborrow elaboration then failed to resolve the field projection to the inner `&mut`. Detect mutable references reachable through aggregate and pointer projections via a new `Type::contains_mut` and route such parameters through the flow-decomposing `mut_bind` path, matching how a top-level `&mut` parameter is already handled. Fixes #125 https://claude.ai/code/session_01MQbByXbDZ8FxkhRra4nPfN
Follow the repo convention of pairing each ui test in pass/ and fail/. Drive the test from main so verification has a concrete assertion to check, and add the fail counterpart asserting the negated condition.
Make the 'needs decomposition' decision a separate, type-driven notion from local mutability. mut_local (reassignable/mut-borrowed) remains the box-elaboration trigger per standard Rust semantics; whether to bind with flow decomposition is now derived independently from the type. Replace Type::contains_mut with Env::type_contains_mut, which resolves enum variants through the enum definitions (with a guard against recursive enum types) so a &mut reachable through an enum is detected too, rather than relying on mut_locals' Move rule to mark the enum local mutable. Add pass/fail ui tests for reborrowing a &mut field out of an enum param. https://claude.ai/code/session_01MQbByXbDZ8FxkhRra4nPfN
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
2 participants
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.
Summary
Fixes #125.
Reborrowing a
&mut-typed field out of an aggregate (tuple/struct) parameter panicked withderef unbound varinEnv::locate_place.Root cause
An aggregate parameter like
w: (&mut i64,)is an immutable local whose type is aTuple, not directlyis_mut(). The binding logic only routes a value through the flow-decomposingmut_bindpath whenis_mut_local(local) || ty.is_mut(), so the tuple param took theimmut_bind→bind_varpath and was stored without flow bindings. WhenReborrowVisitorlater turned thecopyof the&mutfield into a reborrow of_1.0,locate_placestarted at_1, found noTupleflow binding, and the.expect("deref unbound var")fired.A top-level
&mutparameter already works becauseis_mut()is true and it takes themut_bindpath — this change generalizes that to aggregates that contain a reachable&mut.Changes
src/rty.rs: newType::contains_mut()— true if the type is, or transitively contains through tuple/struct and pointer projections, a mutable reference.src/analyze/basic_block.rs: both binding sites (bind_localand the basic-block parameter loop) usecontains_mut()instead ofis_mut(), so aggregates holding a&mutget flow-decomposed bindings. Blast radius is minimal — tuples without any&mutstill take theimmut_bindpath.tests/ui/{pass,fail}/reborrow_mut_field_of_aggregate_param.rs: paired regression test (per repo convention). Thepassasserts the value flows back correctly after reborrowing the aggregate's&mutfield; thefailasserts the negated condition and expectsUnsat.Testing
Ran the full suite locally with z3 4.13.0 (matching
.github/actions/setup-z3) and the COAR docker image: 234 passed, 0 failed, including both new tests.Note
contains_mutdoes not recurse into enum variants, since enum field types come from theEnumDefProviderrather than theTypeitself. The reported cases (tuple and struct params — structs are represented as tuples here) are covered; an enum carrying a&mutfield would be a separate follow-up.https://claude.ai/code/session_01MQbByXbDZ8FxkhRra4nPfN
Generated by Claude Code