Contracts & Harnesses for non_null::sub and non_null::sub_ptr and non_null::offset_from
#93
Conversation
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
…-std into jimmy_develop
feliperodri
requested changes
Sep 27, 2024
feliperodri
changed the title
non_null::sub and non_null::sub_ptr
feliperodri
previously requested changes
Sep 27, 2024
Jimmycreative
changed the title
non_null::sub and non_null::sub_ptrnon_null::sub and non_null::sub_ptr and non_null::offset_from
zhassan-aws
reviewed
Nov 13, 2024
carolynzech
approved these changes
Nov 22, 2024
Co-authored-by: Carolyn Zech <cmzech@amazon.com>
Co-authored-by: Carolyn Zech <cmzech@amazon.com>
Co-authored-by: Carolyn Zech <cmzech@amazon.com>
carolynzech
approved these changes
Nov 22, 2024
…-std into jimmy_develop
zhassan-aws
approved these changes
Nov 26, 2024
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
auto-merge was automatically disabled
November 26, 2024 21:58
Head branch was pushed to by a user without write access
zhassan-aws
approved these changes
Nov 27, 2024
Yenyun035
pushed a commit
to rajathkotyal/verify-rust-std
that referenced
this pull request
Nov 27, 2024
… `non_null::offset_from` (model-checking#93) Towards model-checking#53 Changes added contract and harness for non_null::sub added contract and harness for non_null::sub_ptr Revalidation To revalidate the verification results, run kani verify-std -Z unstable-options "path/to/library" -Z function-contracts -Z mem-predicates --harness ptr::non_null::verify This will run both harnesses. All default checks should pass: ``` SUMMARY: ** 0 of 1622 failed VERIFICATION:- SUCCESSFUL Verification Time: 0.3814842s SUMMARY: ** 0 of 1780 failed (1 unreachable) VERIFICATION:- SUCCESSFUL Verification Time: 0.44192737s Complete - 2 successfully verified harnesses, 0 failures, 2 total. ``` The proof now only handles the array with a fixed size and uses a random element in the arr for subtraction. The element is i32 type. Is this ok for the current stage? Or maybe we need to consider other types such as i64, etc and maybe change the arr to a bigger size? --------- Co-authored-by: OwO <owo@OwOs-MacBook-Pro.local> Co-authored-by: Qinyuan Wu <qinyuanw@andrew.cmu.edu> Co-authored-by: Carolyn Zech <cmzech@amazon.com> Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Fix invariant return Add to_bytes and to_bytes_with_nul harnesses
tautschnig
pushed a commit
to tautschnig/verify-rust-std
that referenced
this pull request
Apr 29, 2025
Introduce and use specialized `//@ ignore-auxiliary` for test support files instead of using `//@ ignore-test` ### Summary Add a semantically meaningful directive for ignoring test *auxiliary* files. This is for auxiliary files that *participate* in actual tests but should not be built by `compiletest` (i.e. these files are involved through `mod xxx;` or `include!()` or `#[path = "xxx"]`, etc.). ### Motivation A specialized directive like `//@ ignore-auxiliary` makes it way easier to audit disabled tests via `//@ ignore-test`. - These support files cannot use the canonical `auxiliary/` dir because they participate in module resolution or are included, or their relative paths can be important for test intention otherwise. Follow-up to: - rust-lang#139705 - rust-lang#139783 - rust-lang#139740 See also discussions in: - [#t-compiler > Directive name for non-test aux files?](https://rust-lang.zulipchat.com/#narrow/channel/131828-t-compiler/topic/Directive.20name.20for.20non-test.20aux.20files.3F/with/512773817) - [#t-compiler > Handling disabled &model-checking#96;//@ ignore-test&model-checking#96; tests](https://rust-lang.zulipchat.com/#narrow/channel/131828-t-compiler/topic/Handling.20disabled.20.60.2F.2F.40.20ignore-test.60.20tests/with/512005974) - [#t-compiler/meetings > &model-checking#91;steering&model-checking#93; 2025-04-11 Dealing with disabled tests](https://rust-lang.zulipchat.com/#narrow/channel/238009-t-compiler.2Fmeetings/topic/.5Bsteering.5D.202025-04-11.20Dealing.20with.20disabled.20tests/with/511717981) ### Remarks on remaining unconditionally disabled tests under `tests/` After this PR, against commit 79a272c, only **14** remaining test files are disabled through `//@ ignore-test`: <details> <summary>Remaining `//@ ignore-test` files under `tests/`</summary> ``` tests/debuginfo/drop-locations.rs 4://@ ignore-test (broken, see rust-lang#128971) tests/rustdoc/macro-document-private-duplicate.rs 1://@ ignore-test (fails spuriously, see issue rust-lang#89228) tests/rustdoc/inline_cross/assoc-const-equality.rs 3://@ ignore-test (FIXME: rust-lang#125092) tests/ui/match/issue-27021.rs 7://@ ignore-test (rust-lang#54987) tests/ui/match/issue-26996.rs 7://@ ignore-test (rust-lang#54987) tests/ui/issues/issue-49298.rs 9://@ ignore-test (rust-lang#54987) tests/ui/issues/issue-59756.rs 2://@ ignore-test (rustfix needs multiple suggestions) tests/ui/precondition-checks/write.rs 5://@ ignore-test (unimplemented) tests/ui/precondition-checks/read.rs 5://@ ignore-test (unimplemented) tests/ui/precondition-checks/write_bytes.rs 5://@ ignore-test (unimplemented) tests/ui/explicit-tail-calls/drop-order.rs 2://@ ignore-test: tail calls are not implemented in rustc_codegen_ssa yet, so this causes 🧊 tests/ui/panics/panic-short-backtrace-windows-x86_64.rs 3://@ ignore-test (rust-lang#92000) tests/ui/json/json-bom-plus-crlf-multifile-aux.rs 3://@ ignore-test Not a test. Used by other tests tests/ui/traits/next-solver/object-soundness-requires-generalization.rs 2://@ ignore-test (see rust-lang#114196) ``` </details> Of these, most are either **unimplemented**, or **spurious**, or **known-broken**. The outstanding one is `tests/ui/json/json-bom-plus-crlf-multifile-aux.rs` which I did not want to touch in *this* PR -- that aux file has load-bearing BOM and carriage returns and byte offset matters. I think those test files that require special encoding / BOM probably are better off as `run-make` tests. See rust-lang#139968 for that aux file. ### Review advice - Best reviewed commit-by-commit. - The directive name diverged from the most voted `//@ auxiliary` because I think that's easy to confuse with `//@ aux-{crate,dir}`. r? compiler
github-actions bot
pushed a commit
that referenced
this pull request
Nov 30, 2025
…uarantees, r=scottmcm Make explicit that `TypeId`'s layout and size are unstable Or worded differently, explicitly remark non-stable-guarantee of `TypeId` layout and size. This PR makes no *additional* guarantees or non-guarantees, it only emphasizes that `TypeId`'s size and layout are unstable like any other `#[repr(Rust)]` types. This was discussed during [#t-compiler/meetings > [weekly] 2025-10-30 @ 💬](https://rust-lang.zulipchat.com/#narrow/channel/238009-t-compiler.2Fmeetings/topic/.5Bweekly.5D.202025-10-30/near/547949347), where the compiler team discussed a request rust-lang#148265 to have the standard library (and language) commit to `TypeId` guaranteeing a size upper bound of 16 bytes. In the meeting, the consensus was: - We were sympathetic to the use case discussed in the request PR, however we feel like this stability guarantee is premature, given that there are unresolved questions surrounding the intended purpose of `TypeId`, and concerns surrounding its collision-resistance properties rust-lang#10389 and rust-lang#129014. We would prefer not making any of such guarantee until the collision-resistance concerns are resolved. - Committing to a stability guarantee on the size upper bound now would close the door to making `TypeId` larger (even if unlikely for perf reasons). Given that we have previously broken people who asserted the size of `TypeId` is 8 bytes, it was also discussed in the meeting that we should *explicitly* note that the size and layout of `TypeId` is not a stable guarantee, and is subject to changes between Rust releases, and thus cannot be relied upon -- if breakage in people's code is due to that assumption, it will be considered a won't-fix. - So even if `#[repr(Rust)]` types have unstable size and layout, this PR makes it explicit for `TypeId` since this type can feel "special" and users can be lead into thinking its size and layout is something they can rely upon. r? `@scottmcm` (or libs/libs-api/lang)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
7 participants
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Towards #53
Changes
added contract and harness for non_null::sub
added contract and harness for non_null::sub_ptr
Revalidation
To revalidate the verification results, run kani verify-std -Z unstable-options "path/to/library" -Z function-contracts -Z mem-predicates --harness ptr::non_null::verify This will run both harnesses. All default checks should pass:
Clarifying Questions
The proof now only handles the array with a fixed size and uses a random element in the arr for subtraction. The element is i32 type. Is this ok for the current stage? Or maybe we need to consider other types such as i64, etc and maybe change the arr to a bigger size?