Stacked Borrows with raw ptr tracking vs pointer-integer-casts

[RalfJung]

In the variant of Stacked Borrows with raw pointer tracking (Cc #248; this is enabled via the -Zmiri-track-raw-pointers flag in Miri), supporting ptr-to-int casts is non-trivial. Or rather, the issue is that I think we have to make it so that pointer-to-int casts are side-effecting, i.e., they cannot be removed even if their result is unused.

Example:

fn foo(x: &mut i32, y: usize) {
   *x = 0;
   unk1();
   assert!(*x == 0); // can be optimized to 'true'
   let addr = x as *mut i32 as usize;
   if (addr == y)
     unk2(addr); // could legally cast "addr" back to a ptr and write to it
   assert!(*x == 0); // can *not* be optimized to 'true'
}

Now we do GVN integer replacement:

fn foo(x: &mut i32, y: usize) {
   *x = 0;
   unk1();
   assert!(*x == 0); // can be optimized to 'true'
   let addr = x as *mut i32 as usize;
   if (addr == y)
     unk2(y);
   assert!(*x == 0); // can *not* be optimized to 'true'
}

Now let us assume there is exactly one call site of this function (and foo is private so we know it can't be called from elsewhere, or maybe we are doing LTO), which looks like

let addr = x as *mut i32 as usize;
foo(x, addr);

This means we know that the "if" in "foo" will always evaluate to true, so we have

fn foo(x: &mut i32, y: usize) {
   *x = 0;
   unk1();
   assert!(*x == 0); // can be optimized to 'true'
   let addr = x as *mut i32 as usize;
   unk2(y);
   assert!(*x == 0); // can *not* be optimized to 'true'
}

Now we can (seemingly) optimize away the "addr" variable entirely:

fn foo(x: &mut i32, y: usize) {
   *x = 0;
   unk1();
   assert!(*x == 0); // can be optimized to 'true'
   unk2(y);
   assert!(*x == 0); // can maybe be optimized to 'true'?
}

In that last program, I can prove that with Stacked Borrows we can optimize both assertions to true. So clearly one of the optimizations along the way is wrong, and I think the problematic one is where we removed the ptr-to-int cast whose result was unused: a ptr-to-int cast has the operational side-effect of marking a memory range (or maybe a Stacked Borrows tag) as "this can now be accessed from integers", and that side-effect is relevant even if the result of the cast is unused. The result an be unused because we already know the address of x since we can have already done a cast earlier before x got its current tag.

[RalfJung]

FWIW, C's restrict has the exact same problem.

I just hope LLVM will accept this and stop optimizing away ptr-to-int casts with unused results... I am not quite sure how else to get a consistent compiler here.^^ Currently I hear proposals like "casting a restrict pointer to an integer is UB" and that makes me somewhat scared. ;)

[RalfJung]

I think this is mostly solved by Strict Provenance + "exposed"; also see my latest blog post.

[RalfJung]

Miri now implements Stacked Borrows with Strict Provenance + "exposed" -- not perfectly, but in a reasonable approximation. So I think we can consider this resolved.