Stacked/Tree Borrows: when exactly should we retag?

One of the biggest "tuning knobs" we have in Stacked Borrows is tdefining when and where exactly retagging happens. Currently we have a rather crude 'add retags' MIR pass, which is unsatisfying for several reasons:

technically this is a MIR pass that adds UB, which is bad
the actual aliasing assumptions made by codegen are completely disconnected from these retags
while we generally insert a retag after every assignment that involves references, we avoid doing that in cases like *ptr = ... since I was worried that the assignment itself might change where that pointer points to

So, we want something nicer and more principled, I think. For MiniRust I am considering making the AssumeFullyInit statement (that was also discussed for MIR) do retagging; we'd want such statements (explicitly or implicitly) at the beginning of every function and after every local variable is initialized and probably on the return value of every callee, so that would cover a lot of it. And then maybe the only other place where we really need retags are the &/&mut operators, i.e., (re)borrowing? However, this has the unfortunate side-effect that generic code behaves slightly different from manually monomorphized code:

fn id<T>(x: T) -> T { x }
fn id_mutref<T>(x: &mut T) -> &mut T { x }

The 2nd function has a reborrow in the MIR, but the first does not.

There's also the question of what to do with 'raw retagging', which we currently (try to) insert on all reference-to-raw-ptr casts -- but here my hope is that we just won't need them at all in the future.

@nikic

If I understand @nikic's proposal here correctly, the idea there is that any time a shared reference (to a Freeze type) is stored in memory we promise to LLVM that this only exposes read-only provenance. That would mean we need to retag implicitly as part of every "typed store" -- which makes sense but is not quite how this is currently implemented in Miri: Miri uses explicit retag instructions, and something like *ptr1 = *ptr2 does not get an explicit retag.

Maybe it's time to ditch the idea of retag instructions and just make this part of typed stores (similar to resetting padding or losing provenance on integers).

@theemathas

@theemathas has some "fun" examples showing that "retag on each assignment" combined with the fact that we add extra assignments to temporaries during MIR creation leaks a lot of MIR creation details into the surface semantics in terms of whether code has UB or not -- that's definitely not great.

To properly fix this we have to define the "retag sites" entirely in terms of surface Rust, not MIR.

@icmccorm

Maybe it's time to ditch the idea of retag instructions and just make this part of typed stores (similar to resetting padding or losing provenance on integers).

FWIW, the proposal discussed in this pre-rfc for BorrowSanitizer moves us into the exact opposite direction.^^
Cc @icmccorm -- there seems to be a potential tension here between representing retags in a way that the LLVM backend can make good use of them (see rust-lang/rust#146844), and in a way that sanitizers can easily check them.

I think that it would be much easier to support a model where explicit retags only apply for &/&mut reborrows if the information in all of the remaining retags that we use today can be provided in some form by a combination of typed stores and parameter attributes. This would make it easier to support emitting retags at codegen, since much of the complexity in our prototype is only necessary to handle the cases when a retag does not directly correspond to a reborrow.

There's also the question of what to do with 'raw retagging', which we currently (try to) insert on all reference-to-raw-ptr casts -- but here my hope is that we just won't need them at all in the future.

It would be helpful for optimization if we had a way to identify casts between raw pointers and references at the LLVM IR level. I think that would be a better fit for a different mechanism than a retag, though.

I think that it would be much easier to support a model where explicit retags only apply for &/&mut reborrows if the information in all of the remaining retags that we use today can be provided in some form by a combination of typed stores and parameter attributes.

I don't know what you mean, I can't entirely parse this.

What I was referring to is that from a compiler development perspective, it would be much easier to say that when you do *x = y, where y: &T, then we do a retag of y as we store it into x. This then directly explains why we can annotate the corresponding store on the LLVM side with something like !captures !{!"address", !"read_provenance"}.

If the MIR for this store instead becomes a sequence of operations involving an explicit retag, then codegen has to be very careful to only emit the !captures !{!"address", !"read_provenance"} if the pointer we are storing has just been retagged -- we'd have to do a data-flow analysis as part of codegen! Generally it's much easier to compile a single MIR statement to one or more LLVM instructions than to pattern-match on a sequence of MIR statements that need to become a single LLVM instruction.

it would be much easier to say that when you do *x = y, where y: &T, then we do a retag of y as we store it into x. This then directly explains why we can annotate the corresponding store on the LLVM side

Would we be able to make this work in the opposite direction? That is, if we are instrumenting the LLVM IR for a Rust program, would we be able to reliably interpret typed stores as retags? That would be convenient, but I'm guessing the answer is "no", unless we added additional metadata to typed stores. And even then, function-entry retags and retags for local operands would still be missing...

From my understanding, it seems like we would still need to add explicit retags at codegen in some form to support BorrowSanitizer, even if we have typed stores in LLVM. I'm unsure of how this would work if we need to rely entirely on surface Rust though, and not MIR, to decide when we emit a retag. Do you have a plan in mind for how Miri would know when to retag without being able to infer this entirely from MIR?

TBH, I'm very interested in what happens on an untyped copy:

let (mut x, mut y) = (0, 0);
let mut x = &mut x;
let mut y = &mut y;
opaque_fn(&mut x, &mut y);
*x = 1;
*y = 1;
*x += 1;
*y += 1;

This cannot be folded to the following code, because opaque_fn could do an untyped copy of y into x or vice versa:

let (mut x, mut y) = (0, 0);
let mut x = &mut x;
let mut y = &mut y;
opaque_fn(&mut x, &mut y);
*x = 2;
*y = 2;

Which seems intuitively wrong and also a potential hazard when uniqueness is modeled at the type level.

@chorman0773

@chorman0773 Please move that discussion to #593.

@icmccorm Miri could fairly easily just do retags as part of the post-typed-copy validation. All the information is in the MIR. The question is just whether retags are encoded as separate statements or as part of other statements.

That is, if we are instrumenting the LLVM IR for a Rust program, would we be able to reliably interpret typed stores as retags?

"typed store" is a Rust concept, so I don't understand what you mean by this.

Anyway, we shouldn't derail this thread with BorrowSanitizer implementation details. This is only about when retags occur, with one option being "implicitly as part of every typed store". I probably shouldn't have pinged you here and instead brought this up in the IRLO thread. I will post a message there.

Auto merge of #154341 - RalfJung:retag-on-typed-copy, r=oli-obk

Auto merge of rust-lang#154341 - RalfJung:retag-on-typed-copy, r=oli-obk

Auto merge of #154341 - RalfJung:retag-on-typed-copy, r=oli-obk

Auto merge of rust-lang#154341 - RalfJung:retag-on-typed-copy, r=oli-obk

Auto merge of #154341 - RalfJung:retag-on-typed-copy, r=oli-obk

Navigation Menu

Repository navigation

Stacked/Tree Borrows: when exactly should we retag? #371

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Stacked/Tree Borrows: when exactly should we retag? #371

Description

Activity

RalfJung commented on Sep 29, 2025

RalfJung commented on Dec 11, 2025

RalfJung commented on Dec 11, 2025

icmccorm commented on Dec 11, 2025

RalfJung commented on Dec 11, 2025

icmccorm commented on Dec 12, 2025

chorman0773 commented on Dec 13, 2025

RalfJung commented on Dec 13, 2025

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions