Skip to content

Conversation

@rajath-mk
Copy link
Contributor

Resolves #3947

Explicitly document behavior of checked_size_of_raw and is_inbounds with respect to isize::MAX to clarify safety guarantees.

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.

@rajath-mk rajath-mk requested a review from a team as a code owner March 24, 2025 22:56
@github-actions github-actions bot added the Z-EndToEndBenchCI Tag a PR to run benchmark CI label Mar 24, 2025
Copy link
Contributor

@carolynzech carolynzech left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thanks!

@carolynzech
Copy link
Contributor

For posterity: We can determine that our intrinsic implementation for checked_size_of (here) returns None if the size overflows isize::MAX by examining the models for the size of trait objects:

if sum_overflow || adjust_overflow || adjusted_size > isize::MAX as _ {
None

and slices:

|| adjusted_size > isize::MAX as _
{
None

and observing that they both return None in this case.

@rajath-mk rajath-mk self-assigned this Mar 25, 2025
@rajath-mk rajath-mk added this pull request to the merge queue Mar 25, 2025
Merged via the queue into model-checking:main with commit c0b3286 Mar 25, 2025
25 checks passed
/// - The computed size overflows.
/// - The computed size exceeds `isize::MAX`.
/// - The pointer is null (except for zero-sized types).
/// - The pointer references unallocated memory.
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This should probably also clarify that it doesn't apply for zero-sized types. Per the std::ptr docs:

For memory accesses of size zero, every pointer is valid, including the null pointer.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I created #3974 to address this

github-merge-queue bot pushed a commit that referenced this pull request Apr 2, 2025
See
#3956 (comment)

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
github-merge-queue bot pushed a commit that referenced this pull request Apr 4, 2025
Bump Kani version to 0.61.0.

Github-generated release notes:

## What's Changed
* Fix CHANGELOG of 0.60.0 by @qinheping in
#3925
* Bump tests/perf/s2n-quic from `d88faa4` to `8670e83` by @dependabot in
#3928
* Update toolchain to 2025-03-04 by @qinheping in
#3927
* Install the right toolchain for HEAD and BASE checks in
`verify-std-check.yml` by @remi-delmas-3000 in
#3920
* Automatic cargo update to 2025-03-10 by @github-actions in
#3926
* Automatic toolchain upgrade to nightly-2025-03-05 by @github-actions
in #3929
* Upgrade toolchain to nightly-2025-03-07 by @tautschnig in
#3931
* Upgrade toolchain to nightly-2025-03-12 by @tautschnig in
#3933
* Automatic toolchain upgrade to nightly-2025-03-13 by @github-actions
in #3934
* Update CBMC dependency to 6.5.0 by @tautschnig in
#3936
* Automatic toolchain upgrade to nightly-2025-03-14 by @github-actions
in #3937
* Automatic toolchain upgrade to nightly-2025-03-15 by @github-actions
in #3938
* Automatic toolchain upgrade to nightly-2025-03-16 by @github-actions
in #3939
* Automatic toolchain upgrade to nightly-2025-03-17 by @github-actions
in #3940
* Automatic cargo update to 2025-03-17 by @github-actions in
#3941
* Autoharness: Don't panic on `_` argument and add `_autoharness` suffix
to GOTO files by @carolynzech in
#3942
* Implement `f16` and `f128` cases in `codegen_float_type` by
@carolynzech in #3943
* Support function implementations of known built-ins by @tautschnig in
#3945
* Autoharness: metadata improvements and enable standard library
application by @carolynzech in
#3948
* Autoharness: `--list` option by @carolynzech in
#3952
* Add support for anonymous nested statics by @carolynzech in
#3953
* Automatic cargo update to 2025-03-24 by @github-actions in
#3954
* Bump tests/perf/s2n-quic from `8670e83` to `324cf31` by @dependabot in
#3955
* Document behavior of checked_size_of_raw and is_inbounds by @rajath-mk
in #3956
* Upgrade toolchain to 2025-03-18 by @zhassan-aws in
#3959
* Remove unstable-features from code formatting script by @zhassan-aws
in #3962
* Remove CI job to update features/verify-rust-std by @tautschnig in
#3963
* Make is_inbounds public by @rajath-mk in
#3958
* Enable Kani to work with a stable toolchain by @zhassan-aws in
#3964
* Automatic cargo update to 2025-03-31 by @github-actions in
#3966
* Add support for struct field accessing in loop contracts by
@thanhnguyen-aws in #3970
* Bump tests/perf/s2n-quic from `324cf31` to `d0aff82` by @dependabot in
#3968
* Clarify `is_inbounds` docs by @carolynzech in
#3974
* Upgrade toolchain to 2025-04-01 by @carolynzech in
#3973
* Remove remaining `--enable-unstable` mentions by @carolynzech in
#3978
* Clean up unused dependencies by @zhassan-aws in
#3981
* Automatic toolchain upgrade to nightly-2025-04-02 by @github-actions
in #3983
* Update dependencies per `cargo-outdated` by @carolynzech in
#3982
* Fix `autoharness` termination test & print metadata in alphabetical
order by @carolynzech in
#3971
* Fix cargo invocations to only use `pkg_args` where appropriate by
@carolynzech in #3984


**Full Changelog**:
kani-0.60.0...kani-0.61.0

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

Z-EndToEndBenchCI Tag a PR to run benchmark CI

Projects

None yet

Development

Successfully merging this pull request may close these issues.

Document behavior of checked_size_of_raw wrt isize::MAX

4 participants