Skip to content

Implement auto strong returned references - #1728

Open
kris-gaudel wants to merge 7 commits into
flux-rs:mainfrom
kris-gaudel:kris-gaudel/auto-strong-returned
Open

Implement auto strong returned references#1728
kris-gaudel wants to merge 7 commits into
flux-rs:mainfrom
kris-gaudel:kris-gaudel/auto-strong-returned

Conversation

@kris-gaudel

Copy link
Copy Markdown
Contributor

Closes #1714

#[flux::sig(fn(x: bool[true]))]
fn assert(_x: bool) {}

#[flux::sig(fn(x: &mut usize{v: v >= 10}) -> &mut usize{v: v >= 10})]
fn returns_a_mut(x: &mut usize) -> &mut usize {
    x
}

fn reads_agree() {
    let mut blah = 10;
    let tmp = returns_a_mut(&mut blah);
    let a = *tmp;
    let b = *tmp;
    assert(a == b) // now succeeds: before, `a` and `b` were unrelated values,
                   // each only known to satisfy `{v: v >= 10}`
}

fn read_after_write() {
    let mut blah = 10;
    let tmp = returns_a_mut(&mut blah);
    *tmp = 20; // a strong update, not a weak one
    assert(*tmp == 20)
}

#[flux::sig(fn(x: &mut usize{v: v >= 10}) -> (&mut usize{v: v >= 10}, usize[0]))]
fn tag(x: &mut usize) -> (&mut usize, usize) {
    (x, 0)
}

fn through_a_tuple() {
    let mut blah = 10;
    let (r, _n) = tag(&mut blah);
    *r = 20;
    assert(*r == 20) // references nested in a returned tuple or struct too
}

kris-gaudel and others added 7 commits August 17, 2026 13:42
A `&mut T` returned by a call is invariant, so reads through it are
imprecise and every write is a weak update: two reads of `*r` aren't
known to be equal, and `*r = 20; assert(*r == 20)` fails.

Unfold such a return into a pointer to a fresh local location holding
`T`, the same way `&strg` arguments are handled by `unfold_local_ptrs`.
Reads are then precise and writes are strong updates, checked against
`T` when `fold_local_ptrs` folds the pointer back at the end of the
block.

Folding a location that other bindings still point to now has to revert
those pointers, so `fold_local_ptrs` first calls `ptrs_to_refs` to turn
each live `ptr(l)` back into the `&mut` it stands for.

Refs flux-rs#1714

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`ptrs_to_refs` handles a pointer into a *field* of the location being
folded by giving it the field's current type rather than the bound, an
arm no test covered. Exercise it with a `&mut` taken into a field of a
returned `&mut`, and check that a write through it is still caught when
the pointer is folded back.

Refs flux-rs#1714

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
The fold at the top of `check_terminator` bounds a local pointer to the
block that uses it, but it cannot cover the one edge the pointer
legitimately crosses: the edge out of the call that created it. If that
successor is a join point, `ptr(l)` reaches `join_ty` and hits a
`tracked_span_bug`; if it is an inlined exit block, the pointer reaches
`check_ret` and the bound recorded on the location is never checked.

Fold in `check_goto` for both cases, so the invariant is that a local
pointer never outlives the block it is used in.

Refs flux-rs#1714

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`fold` had no arm for `ptr(mut, l)`, so a pointer nested in a struct
reached `check_constructor`, which relates the fields with a plain
`subtyping` backed by `DummyEnv` and hits a `tracked_span_bug`. This is
reachable before `fold_local_ptrs` bounds the pointer at the terminator,
because folding the struct can happen in a statement: an unsize coercion
of a borrow of it does exactly that.

Fold the pointer as part of folding the value holding it, so a folded
type never mentions the location and `DummyEnv` stays a true statement.
`fold` has to return an `InferResult` for the subtyping this fires, and
shares `fold_local_ptr` with `fold_local_ptrs`.

Refs flux-rs#1714

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
`unfold_returned_refs` hands a returned struct back unfolded, but the
fold/unfold analysis runs on the mir and so never learns about it: it
inserts no ghost statement to fold the struct back, and the `Downcast`
escapes into any use of the value as a whole, where subtyping against
the folded type reports incompatible types.

A struct holding a `&mut` is never `Copy`, so the only reads that can
see one are a move and the return place. Fold there.

Refs flux-rs#1714

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
Converting a pointer to a local pointer location into a reference, e.g.
by an unsize coercion, blocks the location. `fold_local_ptrs` then folded
the blocked type back at the end of the block and related it to the
bound, reporting incompatible types.

The reference takes over from the pointer, so that conversion is where
the strong window closes: check the bound there and stop treating the
location as a local pointer. This also plugs a hole, since
`PtrToRefBound::Identity` never checked the bound at all, so a write
through the pointer before the coercion went unchecked.

A pointer into a *field* of the location blocks only that field and
leaves the location to be folded back as usual, so the fold unblocks
first.

Refs flux-rs#1714

Co-Authored-By: Claude Opus 5 <noreply@anthropic.com>
@nilehmann

nilehmann commented Aug 17, 2026

Copy link
Copy Markdown
Member

This PR introduces (new) unsoundness. The following is correctly rejected in main but accepted by this PR

#[flux::sig(fn(bool[true]))]
fn assert(_: bool) {}

#[flux::sig(fn(&mut usize{v: v > 0}) -> &mut usize{v: v > 0})]
fn id(x: &mut usize) -> &mut usize {
    x
}

fn bad() {
    let mut w = 1;
    let r = id(&mut w);
    let _a = [&mut *r];
    *r = 0;           
    assert(w > 0);   
}

@ranjitjhala

Copy link
Copy Markdown
Contributor

(I haven't seen the code in the PR yet) but is the unsoundness because the effect of the *r = 0 is not "back-propagated" to the w after the r expires? Is there a way to only do this auto-strong IF the returned r "expires" at the END of the caller? (Also, @nilehmann what is the let _a = [&mut *r]; doing??)

@nilehmann

Copy link
Copy Markdown
Member

I haven't reviewed the implementation, so I can't determine whether the issue is in the implementation or an existing unsoundness that's surfacing because there are more unfolds.

The let _a = [&mut *r] is triggering a ptr_to_ref on the unfolded location.

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

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Auto strong returned references

3 participants