Miri allows inbounds offsets outside of provenance but inside of the allocid

[CAD97]

... and it is unclear whether this is intended (inbounds only cares about the allocated object bounds) or a bug (inbounds should respect subobject provenance).

pointer::offset says

Both the starting and resulting pointer must be either in bounds or one byte past the end of the same allocated object.

Allocated object

For several operations, such as offset or field projections (expr.field), the notion of an “allocated object” becomes relevant. An allocated object is a contiguous region of memory. Common examples of allocated objects include stack-allocated variables (each variable is a separate allocated object), heap allocations (each allocation created by the global allocator is a separate allocated object), and static variables.

and ptr::read says

src must be valid for reads.

Pointer validity

The precise rules for validity are not determined yet. The guarantees that are provided at this point are very minimal:

• For a pointer to be valid, it is necessary, but not always sufficient, that the pointer be dereferenceable: the memory range of the given size starting at the pointer must all be within the bounds of a single allocated object.
• The result of casting a reference to a pointer is valid for as long as the underlying object is live and no reference (just raw pointers) is used to access the same memory.

Stronger guarantees will be provided eventually, as the aliasing rules are being determined. For more information, see the book as well as the section in the reference devoted to undefined behavior.

Example:

#![feature(raw_ref_op)]

#[allow(unused_must_use, clippy::no_effect)]
fn main() { unsafe {
    // alloc id 2200, tag 4409
    let place = [0u8; 5];

    // tag 4410 at alloc2200[0x0..0x1]
    let p = &raw const place[0];

    let q = p.offset(4); // not diagnosed ub

    // attempting a read access using <4410> at alloc2200[0x4]
    *q; // ub
} }

Tracking:

note: tracking was triggered (x5)
 --> src\main.rs:7:21
   |
 7 |         let place = [0u8; 5];
   |                     ^^^^^^^^ created stack variable allocation of 5 bytes (alignment 1 bytes) with id 2200
   |                     ^^^^^^^^ created tag 4409
   |
10 |         let p = &raw const place[0];
   |                 ^^^^^^^^^^^^^^^^^^^ created tag 4410 at alloc2200[0x0..0x1]
   |
   = note: inside `main` at src\main.rs

error: Undefined Behavior: attempting a read access using <4410> at alloc2200[0x4], but that tag does not exist in the borrow stack for this location
  --> src\main.rs:17:9
   |
17 |         *q; // ub
   |         ^^
   |         |
   |         attempting a read access using <4410> at alloc2200[0x4], but that tag does not exist in the borrow stack for this location
   |         this error occurs as part of an access at alloc2200[0x4..0x5]
   |
help: <4410> was created by a retag at offsets [0x0..0x1]
  --> src\main.rs:10:17
   |
10 |         let p = &raw const place[0];
   |                 ^^^^^^^^^^^^^^^^^^^
   = note: inside `main` at src\main.rs

trace

[2022-07-10T18:42:10Z TRACE miri::stacked_borrows] New allocation alloc2200 has base tag <4409>
[2022-07-10T18:42:10Z TRACE miri::stacked_borrows] write access with tag <4409>: alloc2200, size 1
[2022-07-10T18:42:10Z TRACE miri::stacked_borrows] read access with tag <4409>: alloc2200, size 1
[2022-07-10T18:42:10Z TRACE miri::stacked_borrows] read access with tag <4409>: alloc2200, size 1
[2022-07-10T18:42:10Z TRACE miri::stacked_borrows] write access with tag <4409>: alloc2200+0x1, size 4
[2022-07-10T18:42:10Z TRACE miri::stacked_borrows] reborrow: raw (constant) reference <4410> derived from <4409> (pointee u8): alloc2200, size 1
[2022-07-10T18:42:10Z TRACE miri::stacked_borrows] reborrow: adding item [SharedReadOnly for <4410>]
[2022-07-10T18:42:10Z TRACE miri::stacked_borrows] new_call: Assigning ID 1330
[2022-07-10T18:42:10Z TRACE miri::stacked_borrows] New allocation alloc2201 has base tag <4411>
[2022-07-10T18:42:10Z TRACE miri::stacked_borrows] reborrow: unique reference <4412> derived from <4411> (pointee *const u8): alloc2201, size 8
[2022-07-10T18:42:10Z TRACE miri::stacked_borrows] reborrow: adding item [Unique for <4412> (call 1330)]
[2022-07-10T18:42:10Z TRACE miri::stacked_borrows] write access with tag <4412>: alloc2201, size 8
[2022-07-10T18:42:10Z TRACE miri::stacked_borrows] read access with tag <4412>: alloc2201, size 8
[2022-07-10T18:42:10Z TRACE miri::stacked_borrows] read access with tag <4411>: alloc2201, size 8
[2022-07-10T18:42:10Z TRACE miri::stacked_borrows] access: disabling item [Unique for <4412> (call 1330)]
[2022-07-10T18:42:10Z TRACE miri::stacked_borrows] read access with tag <4410>: alloc2200+0x4, size 1
[2022-07-10T18:42:10Z TRACE miri::stacked_borrows] read access with tag <1>: alloc1, size 8
[2022-07-10T18:42:10Z TRACE miri::stacked_borrows] deallocation with tag <2>: alloc2, size 8
error: Undefined Behavior: attempting a read access using <4410> at alloc2200[0x4], but that tag does not exist in the borrow stack for this location

[CAD97]

Slightly cleaner trace by using intrinsic offset instead of the wrapper method

#![feature(core_intrinsics, raw_ref_op)]

use std::intrinsics::offset;

#[allow(unused_must_use, clippy::no_effect)]
fn main() {
    unsafe {
        // alloc id 2200, tag 4409
        let place = [0u8; 5];

        // tag 4410 at alloc2200[0x0..0x1]
        let p = &raw const place[0];

        let q = offset(p, 4); // not diagnosed ub

        // attempting a read access using <4410> at alloc2200[0x4]
        *q; // ub
    }
}

trace

[2022-07-10T18:49:29Z TRACE miri::stacked_borrows] New allocation alloc2200 has base tag <4409>
[2022-07-10T18:49:29Z TRACE miri::stacked_borrows] write access with tag <4409>: alloc2200, size 1
[2022-07-10T18:49:29Z TRACE miri::stacked_borrows] read access with tag <4409>: alloc2200, size 1
[2022-07-10T18:49:29Z TRACE miri::stacked_borrows] read access with tag <4409>: alloc2200, size 1
[2022-07-10T18:49:29Z TRACE miri::stacked_borrows] write access with tag <4409>: alloc2200+0x1, size 4
note: tracking was triggered
 --> src\main.rs:9:21
  |
9 |         let place = [0u8; 5];
  |                     ^^^^^^^^ created stack variable allocation of 5 bytes (alignment 1 bytes) with id 2200
  |

note: tracking was triggered
 --> src\main.rs:9:21
  |
9 |         let place = [0u8; 5];
  |                     ^^^^^^^^ created tag 4409
  |
  = note: inside `main` at src\main.rs:9:21

[2022-07-10T18:49:29Z TRACE miri::stacked_borrows] reborrow: raw (constant) reference <4410> derived from <4409> (pointee u8): alloc2200, size 1
[2022-07-10T18:49:29Z TRACE miri::stacked_borrows] reborrow: adding item [SharedReadOnly for <4410>]
note: tracking was triggered
  --> src\main.rs:12:17
   |
12 |         let p = &raw const place[0];
   |                 ^^^^^^^^^^^^^^^^^^^ created tag 4410 at alloc2200[0x0..0x1]
   |
   = note: inside `main` at src\main.rs:12:17

[2022-07-10T18:49:29Z TRACE miri::stacked_borrows] read access with tag <4410>: alloc2200+0x4, size 1
[2022-07-10T18:49:29Z TRACE miri::stacked_borrows] read access with tag <1>: alloc1, size 8
[2022-07-10T18:49:29Z TRACE miri::stacked_borrows] deallocation with tag <2>: alloc2, size 8
error: Undefined Behavior: attempting a read access using <4410> at alloc2200[0x4], but that tag does not exist in the borrow stack for this location
  --> src\main.rs:17:9
   |
17 |         *q; // ub
   |         ^^
   |         |
   |         attempting a read access using <4410> at alloc2200[0x4], but that tag does not exist in the borrow stack for this location
   |         this error occurs as part of an access at alloc2200[0x4..0x5]
   |
   = help: this indicates a potential bug in the program: it performed an invalid operation, but the Stacked Borrows rules it violated are still experimental
   = help: see https://github.com/rust-lang/unsafe-code-guidelines/blob/master/wip/stacked-borrows.md for further information
help: <4410> was created by a retag at offsets [0x0..0x1]
  --> src\main.rs:12:17
   |
12 |         let p = &raw const place[0];
   |                 ^^^^^^^^^^^^^^^^^^^
   = note: backtrace:
   = note: inside `main` at src\main.rs:17:9

[RalfJung]

... and it is unclear whether this is intended (inbounds only cares about the allocated object bounds) or a bug (inbounds should respect subobject provenance).

It is fully intended. In fact the "subobject" part of Stacked Borrows is more a case of emergent behavior than anything that was deliberately put in. And note that "subobjects" in the Stacked Borrows sense do not have to be contiguous; it is perfectly possible for a ptr to be valid for some put not all fields of a struct.

The docs are IMO pretty clear about it since they always talk about allocation boundaries, never about whether the aliasing model allows the ptr to be used here or there.

[RalfJung]

I think the docs are clear here and nobody objected to this being intentional, so I am closing this issue. If someone wants to strengthen the offset requirements to interact with the aliasing model, please write up a motivation and a proposal -- but honestly my own preference is to weaken these requirements significantly (see #350).

[chorman0773]

IMO, this issue should be subject to a T-opsem FCP on the question "is it defined behaviour to offset within the allocation entirely" prior to being closed. Otherwise, I have no objections.

[RalfJung]

"is it defined behaviour to offset within the allocation entirely"

This is documented on a stable function. I wouldn't expect us to FCP something like that. Why would we re-FCP an unsafe contract that has already been approved by libs/lang?

[Lokathor]

Since opsem can't pick a different answer without throwing a breaking change at the greater rust community there isn't much point in a full FCP.

[chorman0773]

That's fair - the only thing that gives me pause on just accepting it
as-is, though, is that it means that p.add(1) being well-defined does not
necessarily mean p.read() is well-defined, which is a potential
consistency issue for me.

Edit: Actually, wait, the consistency issue I have is the other way arround, that p.read() being defined should imply p.add(1) is defined.

[RalfJung]

p.read() being defined should imply p.add(1) is defined.

That should currently be the case (and is still the case under all proposals I am aware of).

[chorman0773]

Yeah, that isn't implicated here. The opposite one is, but is very much not the case anyways. I withdraw my concern.