Weaken closure parameter for FnMut closures called via FnOnce#120
Draft
coord-e wants to merge 2 commits into
Draft
Weaken closure parameter for FnMut closures called via FnOnce#120coord-e wants to merge 2 commits into
coord-e wants to merge 2 commits into
Conversation
Calling an FnMut closure through FnOnce::call_once resolves to the
closure function taking &mut {closure}, while the caller passes the
closure environment by value, which hit the unimplemented case 3 in
RustCallVisitor.
Implement case 3 by mutably borrowing the closure argument, and restore
completeness by dropping the borrow and the environment right after the
call: FnOnce::call_once consumes the closure, so dropping the
environment at the call site resolves the prophecies of its captured
mutable borrows. Without these drops the captured borrows' final values
stay unconstrained and assertions about the mutated captures cannot be
proven.
To make the environment local borrowable, reassign_local_mutabilities
now also marks the closure argument of such calls as mutable, so it is
boxed in the refinement environment.
https://claude.ai/code/session_012451PZJH2QqdqE5Zyxna5y
Instead of a separate Vec field on basic_block::Analyzer, store the extra after-terminator drops in DropPoints next to the liveness-derived sets, behind DropPoints::insert_after_terminator and an Analyzer helper. They are kept as a Vec because the locals are created during elaboration and lie outside the bitset domains sized to the original body's locals. https://claude.ai/code/session_012451PZJH2QqdqE5Zyxna5y
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.
Fixes #46 (the remaining reopened case: calling an
FnMutclosure viaFnOnce::call_once).Problem
Calling an
FnMutclosure throughFnOnce::call_onceresolves to the closure function taking&mut {closure}, while the caller's MIR passes the closure environment by value. This hit theunimplemented!()"case 3" inRustCallVisitor.The draft patch in the issue comment fixed the panic but lost completeness: after rewriting the call to pass
&mut {closure}, the environment local stays live in the caller, yet the drop-point analysis (computed on the original MIR, where the local was moved into the call) never schedules a drop for it. The prophecies of its captured mutable borrows were therefore never resolved (final = current), leaving the captures' final values unconstrained.Fix
RustCallVisitorcase 3: insert a mutable borrow of the closure environment and pass it as the argument. SinceFnOnce::call_onceconsumes the closure, schedule both the borrow and the environment local to be dropped right after the call, which resolves the prophecies of the captured mutable borrows and restores completeness.DropPoints: the scheduled drops are stored next to the liveness-derived sets, behindDropPoints::insert_after_terminatorand anAnalyzer::schedule_drop_after_terminatorhelper. They are kept as aVecbecause the locals are created during elaboration and lie outside the bitset domains sized to the original body's locals.reassign_local_mutabilities: mark the closure argument of aFnOnce::call_oncecall as mutable when the closure's kind isFnMut(implementing the TODO from the issue comment by checking the closure kind instead of the resolved signature), so the environment is boxed in the refinement environment and can be mutably borrowed.Tests
tests/ui/{pass,fail}/closure_param_weaken_3.rswith the example from the issue:assert!(result == 3 && x == 2)is now proven (the issue's draft patch could not), and the incorrect variant (x == 1) is rejected with Unsat.cargo testpasses locally (230/230 UI tests, including the pcsat/COAR-based ones), as docargo fmt --checkandcargo clippy.https://claude.ai/code/session_012451PZJH2QqdqE5Zyxna5y