also remove redundant requirements from offset() · model-checking/verify-rust-std@0860a04 (original) (raw)
`@@ -390,37 +390,26 @@ impl<T: ?Sized> *const T {
`
390
390
`if self.is_null() { None } else { Some(unsafe { &*(self as *const MaybeUninit) }) }
`
391
391
`}
`
392
392
``
393
``
`-
/// Calculates the offset from a pointer.
`
``
393
`+
/// Adds an offset to a pointer.
`
394
394
`///
`
395
395
`` /// count
is in units of T; e.g., a count
of 3 represents a pointer
``
396
396
`` /// offset of 3 * size_of::<T>()
bytes.
``
397
397
`///
`
398
398
`/// # Safety
`
399
399
`///
`
400
``
`-
/// If any of the following conditions are violated, the result is Undefined
`
401
``
`-
/// Behavior:
`
402
``
`-
///
`
403
``
`-
/// * If the computed offset, in bytes, is non-zero, then both the starting and resulting
`
404
``
`-
/// pointer must be either in bounds or at the end of the same [allocated object].
`
405
``
`-
/// (If it is zero, then the function is always well-defined.)
`
406
``
`-
///
`
407
``
`` -
/// * The computed offset, in bytes, cannot overflow an isize
.
``
``
400
`+
/// If any of the following conditions are violated, the result is Undefined Behavior:
`
408
401
`///
`
409
``
`-
/// * The offset being in bounds cannot rely on "wrapping around" the address
`
410
``
`-
/// space. That is, the infinite-precision sum, in bytes must fit in a usize.
`
``
402
`` +
/// * The computed offset, count * size_of::<T>()
bytes, must not overflow isize
.
``
411
403
`///
`
412
``
`-
/// The compiler and standard library generally tries to ensure allocations
`
413
``
`` -
/// never reach a size where an offset is a concern. For instance, Vec
``
414
``
`` -
/// and Box
ensure they never allocate more than isize::MAX
bytes, so
``
415
``
`` -
/// vec.as_ptr().add(vec.len())
is always safe.
``
``
404
`` +
/// * If the computed offset is non-zero, then self
must be derived from a pointer to some
``
``
405
`` +
/// [allocated object], and the entire memory range between self
and the result must be in
``
``
406
`+
/// bounds of that allocated object. In particular, this range must not "wrap around" the edge
`
``
407
`+
/// of the address space.
`
416
408
`///
`
417
``
`-
/// Most platforms fundamentally can't even construct such an allocation.
`
418
``
`-
/// For instance, no known 64-bit platform can ever serve a request
`
419
``
`-
/// for 263 bytes due to page-table limitations or splitting the address space.
`
420
``
`-
/// However, some 32-bit and 16-bit platforms may successfully serve a request for
`
421
``
`` -
/// more than isize::MAX
bytes with things like Physical Address
``
422
``
`-
/// Extension. As such, memory acquired directly from allocators or memory
`
423
``
`-
/// mapped files may be too large to handle with this function.
`
``
409
`` +
/// Allocated objects can never be larger than isize::MAX
bytes, so if the computed offset
``
``
410
`+
/// stays in bounds of the allocated object, it is guaranteed to satisfy the first requirement.
`
``
411
`` +
/// This implies, for instance, that vec.as_ptr().add(vec.len())
(for vec: Vec<T>
) is always
``
``
412
`+
/// safe.
`
424
413
`///
`
425
414
`` /// Consider using [wrapping_offset
] instead if these constraints are
``
426
415
`/// difficult to satisfy. The only advantage of this method is that it
`
`@@ -622,7 +611,7 @@ impl<T: ?Sized> *const T {
`
622
611
`/// * The distance between the pointers, in bytes, must be an exact multiple
`
623
612
`` /// of the size of T
.
``
624
613
`///
`
625
``
`-
/// As a consequence, the absolute distance between the pointers, in bytes, computed on
`
``
614
`+
/// As a consequence, the absolute distance between the pointers, in bytes, computed on
`
626
615
`` /// mathematical integers (without "wrapping around"), cannot overflow an isize
. This is
``
627
616
`/// implied by the in-bounds requirement, and the fact that no allocated object can be larger
`
628
617
`` /// than isize::MAX
bytes.
``
`@@ -862,37 +851,26 @@ impl<T: ?Sized> *const T {
`
862
851
`}
`
863
852
`}
`
864
853
``
865
``
`` -
/// Calculates the offset from a pointer (convenience for .offset(count as isize)
).
``
``
854
`` +
/// Adds an offset to a pointer (convenience for .offset(count as isize)
).
``
866
855
`///
`
867
856
`` /// count
is in units of T; e.g., a count
of 3 represents a pointer
``
868
857
`` /// offset of 3 * size_of::<T>()
bytes.
``
869
858
`///
`
870
859
`/// # Safety
`
871
860
`///
`
872
``
`-
/// If any of the following conditions are violated, the result is Undefined
`
873
``
`-
/// Behavior:
`
874
``
`-
///
`
875
``
`-
/// * If the computed offset, in bytes, is non-zero, then both the starting and resulting
`
876
``
`-
/// pointer must be either in bounds or at the end of the same [allocated object].
`
877
``
`-
/// (If it is zero, then the function is always well-defined.)
`
878
``
`-
///
`
879
``
`` -
/// * The computed offset, in bytes, cannot overflow an isize
.
``
``
861
`+
/// If any of the following conditions are violated, the result is Undefined Behavior:
`
880
862
`///
`
881
``
`-
/// * The offset being in bounds cannot rely on "wrapping around" the address
`
882
``
`` -
/// space. That is, the infinite-precision sum must fit in a usize
.
``
``
863
`` +
/// * The computed offset, count * size_of::<T>()
bytes, must not overflow isize
.
``
883
864
`///
`
884
``
`-
/// The compiler and standard library generally tries to ensure allocations
`
885
``
`` -
/// never reach a size where an offset is a concern. For instance, Vec
``
886
``
`` -
/// and Box
ensure they never allocate more than isize::MAX
bytes, so
``
887
``
`` -
/// vec.as_ptr().add(vec.len())
is always safe.
``
``
865
`` +
/// * If the computed offset is non-zero, then self
must be derived from a pointer to some
``
``
866
`` +
/// [allocated object], and the entire memory range between self
and the result must be in
``
``
867
`+
/// bounds of that allocated object. In particular, this range must not "wrap around" the edge
`
``
868
`+
/// of the address space.
`
888
869
`///
`
889
``
`-
/// Most platforms fundamentally can't even construct such an allocation.
`
890
``
`-
/// For instance, no known 64-bit platform can ever serve a request
`
891
``
`-
/// for 263 bytes due to page-table limitations or splitting the address space.
`
892
``
`-
/// However, some 32-bit and 16-bit platforms may successfully serve a request for
`
893
``
`` -
/// more than isize::MAX
bytes with things like Physical Address
``
894
``
`-
/// Extension. As such, memory acquired directly from allocators or memory
`
895
``
`-
/// mapped files may be too large to handle with this function.
`
``
870
`` +
/// Allocated objects can never be larger than isize::MAX
bytes, so if the computed offset
``
``
871
`+
/// stays in bounds of the allocated object, it is guaranteed to satisfy the first requirement.
`
``
872
`` +
/// This implies, for instance, that vec.as_ptr().add(vec.len())
(for vec: Vec<T>
) is always
``
``
873
`+
/// safe.
`
896
874
`///
`
897
875
`` /// Consider using [wrapping_add
] instead if these constraints are
``
898
876
`/// difficult to satisfy. The only advantage of this method is that it
`
`@@ -946,38 +924,27 @@ impl<T: ?Sized> *const T {
`
946
924
`unsafe { self.cast::().add(count).with_metadata_of(self) }
`
947
925
`}
`
948
926
``
949
``
`-
/// Calculates the offset from a pointer (convenience for
`
``
927
`+
/// Subtracts an offset from a pointer (convenience for
`
950
928
`` /// .offset((count as isize).wrapping_neg())
).
``
951
929
`///
`
952
930
`` /// count
is in units of T; e.g., a count
of 3 represents a pointer
``
953
931
`` /// offset of 3 * size_of::<T>()
bytes.
``
954
932
`///
`
955
933
`/// # Safety
`
956
934
`///
`
957
``
`-
/// If any of the following conditions are violated, the result is Undefined
`
958
``
`-
/// Behavior:
`
959
``
`-
///
`
960
``
`-
/// * If the computed offset, in bytes, is non-zero, then both the starting and resulting
`
961
``
`-
/// pointer must be either in bounds or at the end of the same [allocated object].
`
962
``
`-
/// (If it is zero, then the function is always well-defined.)
`
963
``
`-
///
`
964
``
`` -
/// * The computed offset cannot exceed isize::MAX
bytes.
``
``
935
`+
/// If any of the following conditions are violated, the result is Undefined Behavior:
`
965
936
`///
`
966
``
`-
/// * The offset being in bounds cannot rely on "wrapping around" the address
`
967
``
`-
/// space. That is, the infinite-precision sum must fit in a usize.
`
``
937
`` +
/// * The computed offset, count * size_of::<T>()
bytes, must not overflow isize
.
``
968
938
`///
`
969
``
`-
/// The compiler and standard library generally tries to ensure allocations
`
970
``
`` -
/// never reach a size where an offset is a concern. For instance, Vec
``
971
``
`` -
/// and Box
ensure they never allocate more than isize::MAX
bytes, so
``
972
``
`` -
/// vec.as_ptr().add(vec.len()).sub(vec.len())
is always safe.
``
``
939
`` +
/// * If the computed offset is non-zero, then self
must be derived from a pointer to some
``
``
940
`` +
/// [allocated object], and the entire memory range between self
and the result must be in
``
``
941
`+
/// bounds of that allocated object. In particular, this range must not "wrap around" the edge
`
``
942
`+
/// of the address space.
`
973
943
`///
`
974
``
`-
/// Most platforms fundamentally can't even construct such an allocation.
`
975
``
`-
/// For instance, no known 64-bit platform can ever serve a request
`
976
``
`-
/// for 263 bytes due to page-table limitations or splitting the address space.
`
977
``
`-
/// However, some 32-bit and 16-bit platforms may successfully serve a request for
`
978
``
`` -
/// more than isize::MAX
bytes with things like Physical Address
``
979
``
`-
/// Extension. As such, memory acquired directly from allocators or memory
`
980
``
`-
/// mapped files may be too large to handle with this function.
`
``
944
`` +
/// Allocated objects can never be larger than isize::MAX
bytes, so if the computed offset
``
``
945
`+
/// stays in bounds of the allocated object, it is guaranteed to satisfy the first requirement.
`
``
946
`` +
/// This implies, for instance, that vec.as_ptr().add(vec.len())
(for vec: Vec<T>
) is always
``
``
947
`+
/// safe.
`
981
948
`///
`
982
949
`` /// Consider using [wrapping_sub
] instead if these constraints are
``
983
950
`/// difficult to satisfy. The only advantage of this method is that it
`