Understanding Miri and Stacked Borrows in Rust — Why One Example Is UB and the Other Isn’t

Programming

Rust’s borrow checker guarantees memory safety at compile time, but some rules—especially around raw pointers—are too subtle for the compiler alone. That’s where Miri comes in. In this post, we’ll walk through two tiny Rust programs: one that Miri accepts, and one that Miri flags as Undefined Behavior. The difference comes down to how Stacked Borrows tracks pointer permissions.

Rust’s aliasing rules are strict by design. They prevent data races, ensure exclusive access through &mut, and make raw pointer usage safe only when you uphold the rules yourself. But how do you know whether your raw pointer code is actually valid?

Enter Miri, an interpreter for Rust’s mid‑level IR (MIR) that can detect Undefined Behavior at runtime—especially UB related to aliasing and borrowing.

To understand how Miri reasons about pointers, we need to understand Stacked Borrows, the model it uses to track which references are allowed to read or write memory at any moment.

Let’s explore a simple example.

fn main() {
    let mut x = 42;
    let r1 = &mut x;
    let raw = r1 as *mut i32;
    let r2 = &mut *r1;
    *r2 = 7;
    unsafe { *raw = 13; }
    println!("{}", x); // UB
}

Lets run Miri on this code. To do this you have to install Miri first.

How to run Miri on this code

Install Miri:

rustup +nightly component add miri

Initialize Miri for your project:

cargo +nightly miri setup

Run your program under Miri:

cargo +nightly miri run

If the code is in a single file (e.g., main.rs), that’s all you need:

error: Undefined Behavior: attempting a write access using <336> at alloc149[0x0], but that tag does not exist in the borrow stack for this location
  --> src\main.rs:7:14
   |
 7 |     unsafe { *raw = 13; }
   |              ^^^^^^^^^ this error occurs as part of an access at alloc149[0x0..0x4]

What went wrong?

The key issue is the reborrow:

let r2 = &mut *r1;

This creates a new &mut with a new tag. Under Stacked Borrows, this new tag sits on top of the borrow stack. Any earlier mutable borrows—including the raw pointer derived from r1—are now inactive for mutation.

When you later write through raw, you violate the exclusivity of r2. Miri catches this instantly.

What happens in terms of Stacked Borrows

Let’s walk through the borrow stack for x:

  1. let r1 = &mut x; → r1 gets a unique tag; it is the active unique reference.
  2. let raw = r1 as *mut i32; → raw pointer gets the same tag as r1, but raw pointers do not keep the borrow alive.
  3. let r2 = &mut *r1; → This creates a new unique borrow, which pushes a new tag on top of the borrow stack. → r1 is now inactive (superseded), and so is raw.
  4. *r2 = 7; → Valid: r2 is the active unique reference.
  5. unsafe { *raw = 13; } → UB: raw uses the old tag, which is no longer allowed to write. → Miri detects that you are writing through a pointer whose borrow has been invalidated by a later &mut.

This is exactly what Stacked Borrows is designed to catch.

Now let replace this code:

fn main() {
    let mut x = 42;

    let r1 = &mut x;
    // r1: unique mutable reference, becomes the active tag for `x`

    let raw = r1 as *mut i32;
    // raw pointer inherits r1's tag, but raw pointers do NOT keep borrows alive

    let r2 = &mut *r1;
    // reborrow from r1: creates a NEW unique borrow with a NEW tag
    // this new tag is now on top of the borrow stack, invalidating r1 and raw for mutation

    *r2 = 7;
    // valid: r2 is the active unique reference

    unsafe { *raw = 13; }
    // UB under Stacked Borrows:
    // raw was created before r2, so its tag is no longer active
    // writing through raw violates the uniqueness guarantee of r2

    println!("{}", x);
    // Miri reports Undefined Behavior before this point
}

With this one:

fn main() {
    let mut x = 42;

    let r1 = &mut x;
    // r1: unique mutable reference, becomes the active tag for `x`

    *r1 = 7;
    // valid: r1 is the only active unique reference at this moment

    let raw = r1 as *mut i32;
    // raw pointer is created AFTER the last use of r1 as a mutable reference
    // raw inherits r1's tag, and no new &mut is created after this point
    // therefore raw's tag remains valid for mutation

    unsafe { *raw = 13; }
    // valid under Stacked Borrows:
    // no later &mut has superseded raw's tag, so writing through it is allowed

    println!("{}", x);
    // prints 13; no UB, Miri accepts this program
}

Why is this one okay?

The crucial difference is no new &mut is created after the raw pointer. That means:

  • raw inherits the active tag from r1
  • nothing supersedes that tag
  • writing through raw is still allowed

Miri sees no violation of aliasing rules, so the program is valid.

Code side by side

fn main() {						|	fn main() {
    let mut x = 42;				|		let mut x = 42;
    let r1 = &mut x;			|		let r1 = &mut x; // r1: unique mutable ref
    *r1 = 7						|	 	*r1 = 7;
    let raw = r1 as *mut i32;	|	 	let raw = r1 as *mut i32; // raw pointer
    let r2 = &mut *r1; /*new*/	|	 	// no new `&mut` is created after!
    *r2 = 7; 	 			    | 
    unsafe { *raw = 13; }		|		unsafe { *raw = 13; }
    println!("{}", x); /* UB */	|		println!("{}", x); // No UB
}								|	}

Also could be interesting to explore the code above with

cargo +nightly rustc -- -Zunpretty=mir > mir.log