offset_from: "the difference must fit in an isize" is a corollary · model-checking/verify-rust-std@6f80604 (original) (raw)

`@@ -761,38 +761,21 @@ impl<T: ?Sized> NonNull {

761

`///

762

`/// # Safety

763

`///

764

/// If any of the following conditions are violated, the result is Undefined

765

/// Behavior:

764

/// If any of the following conditions are violated, the result is Undefined Behavior:

766

765

`///

767

`` -

/// * Both self and origin must be either in bounds or one

768

/// byte past the end of the same [allocated object].

766

`` +

/// * self and origin must either

769

767

`///

770

/// * Both pointers must be derived from a pointer to the same object.

771

/// (See below for an example.)

768

/// * both be derived from a pointer to the same [allocated object], and the memory range between

769

/// the two pointers must be either empty or in bounds of that object. (See below for an example.)

770

/// * or both be derived from an integer literal/constant, and point to the same address.

772

771

`///

773

772

`/// * The distance between the pointers, in bytes, must be an exact multiple

774

773

`` /// of the size of T.

775

774

`///

776

`` -

/// * The distance between the pointers, in bytes, cannot overflow an isize.

777

///

778

/// * The distance being in bounds cannot rely on "wrapping around" the address space.

779

///

780

`` -

/// Rust types are never larger than isize::MAX and Rust allocations never wrap around the

781

`` -

/// address space, so two pointers within some value of any Rust type T will always satisfy

782

/// the last two conditions. The standard library also generally ensures that allocations

783

`` -

/// never reach a size where an offset is a concern. For instance, Vec and Box ensure they

784

`` -

/// never allocate more than isize::MAX bytes, so ptr_into_vec.offset_from(vec.as_ptr())

785

/// always satisfies the last two conditions.

786

///

787

/// Most platforms fundamentally can't even construct such a large allocation.

788

/// For instance, no known 64-bit platform can ever serve a request

789

/// for 2⁶³ bytes due to page-table limitations or splitting the address space.

790

/// However, some 32-bit and 16-bit platforms may successfully serve a request for

791

`` -

/// more than isize::MAX bytes with things like Physical Address

792

/// Extension. As such, memory acquired directly from allocators or memory

793

/// mapped files may be too large to handle with this function.

794

`` -

/// (Note that [offset] and [add] also have a similar limitation and hence cannot be used on

795

/// such large allocations either.)

775

/// As a consequence, the absolute distance between the pointers, in bytes, computed on

776

`` +

/// mathematical integers (without "wrapping around"), cannot overflow an isize. This is

777

/// implied by the in-bounds requirement, and the fact that no allocated object can be larger

778

`` +

/// than isize::MAX bytes.

796

779

`///

797

780

`/// The requirement for pointers to be derived from the same allocated object is primarily

798

781

`` /// needed for const-compatibility: the distance between pointers into different allocated