diff --git a/.github/pull_requests.toml b/.github/pull_requests.toml index 45a38b3cc2307..6c11ebfeb3691 100644 --- a/.github/pull_requests.toml +++ b/.github/pull_requests.toml @@ -12,5 +12,11 @@ members = [ "jaisnan", "patricklam", "ranjitjhala", - "carolynzech" + "carolynzech", + "robdockins", + "HuStmpHrrr", + "Eh2406", + "jswrenn", + "havelund", + "jorajeev" ] diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 6dec32c1620ec..b3c8aa3882066 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -65,3 +65,17 @@ jobs: - name: Test Kani script (In Repo Directory) working-directory: ${{github.workspace}}/head run: scripts/run-kani.sh --kani-args --harness ptr::verify::check_read_u128 --harness ptr --output-format=terse + + # Step 4: Run list on the std library and add output to job summary + - name: Run Kani List + run: head/scripts/run-kani.sh --run list --path ${{github.workspace}}/head + + - name: Add Kani List output to job summary + uses: actions/github-script@v6 + with: + script: | + const fs = require('fs'); + const kaniOutput = fs.readFileSync('${{github.workspace}}/head/kani_list.txt', 'utf8'); + await core.summary + .addRaw(kaniOutput) + .write(); \ No newline at end of file diff --git a/README.md b/README.md index 41cf22c3a7c7a..2417adde4e446 100644 --- a/README.md +++ b/README.md @@ -7,7 +7,7 @@ This repository is a fork of the official Rust programming language repository, created solely to verify the Rust standard library. It should not be used as an alternative to the official -Rust releases. The repository is tool agnostic and welcomes the addition of +Rust releases. The repository is tool agnostic and welcomes the addition of new tools. The goal is to have a verified [Rust standard library](https://doc.rust-lang.org/std/) and prove that it is safe. @@ -15,16 +15,15 @@ The goal is to have a verified [Rust standard library](https://doc.rust-lang.org 2. Creating new techniques to perform scalable verification 3. Apply techniques to verify previously unverified parts of the standard library. -## [Kani](https://github.com/model-checking/kani) +For that we are launching a contest that includes a series of challenges that focus on verifying +memory safety and a subset of undefined behaviors in the Rust standard library. +Each challenge describes the goal, the success criteria, and whether it has a financial award to be awarded upon its +successful completion. -The Kani Rust Verifier is a bit-precise model checker for Rust. -Kani verifies: -* Memory safety (e.g., null pointer dereferences) -* User-specified assertions (i.e `assert!(...)`) -* The absence of panics (eg., `unwrap()` on `None` values) -* The absence of some types of unexpected behavior (e.g., arithmetic overflows). +See [our book](https://model-checking.github.io/verify-rust-std/intro.html) for more details on the challenge rules +and the list of existing challenges. -You can find out more about Kani from the [Kani book](https://model-checking.github.io/kani/) or the [Kani repository on Github](https://github.com/model-checking/kani). +We welcome everyone to participate! ## Contact @@ -40,7 +39,7 @@ See [SECURITY](https://github.com/model-checking/kani/security/policy) for more Kani is distributed under the terms of both the MIT license and the Apache License (Version 2.0). See [LICENSE-APACHE](https://github.com/model-checking/kani/blob/main/LICENSE-APACHE) and [LICENSE-MIT](https://github.com/model-checking/kani/blob/main/LICENSE-MIT) for details. -## Rust +### Rust Rust is primarily distributed under the terms of both the MIT license and the Apache License (Version 2.0), with portions covered by various BSD-like licenses. See [the Rust repository](https://github.com/rust-lang/rust) for details. diff --git a/doc/src/SUMMARY.md b/doc/src/SUMMARY.md index ca25c36bf449a..4e15d7cacdb50 100644 --- a/doc/src/SUMMARY.md +++ b/doc/src/SUMMARY.md @@ -25,5 +25,5 @@ - [10: Memory safety of String](./challenges/0010-string.md) - [11: Safety of Methods for Numeric Primitive Types](./challenges/0011-floats-ints.md) - [12: Safety of `NonZero`](./challenges/0012-nonzero.md) - + - [13: Safety of `CStr`](./challenges/0013-cstr.md) diff --git a/doc/src/challenge_template.md b/doc/src/challenge_template.md index 50461e2a4e7c4..a39fad01050f1 100644 --- a/doc/src/challenge_template.md +++ b/doc/src/challenge_template.md @@ -3,8 +3,9 @@ - **Status:** *One of the following: \[Open | Resolved | Expired\]* - **Solution:** *Option field to point to the PR that solved this challenge.* - **Tracking Issue:** *Link to issue* -- **Start date:** *YY/MM/DD* -- **End date:** *YY/MM/DD* +- **Start date:** *YYYY/MM/DD* +- **End date:** *YYYY/MM/DD* +- **Reward:** *TBD*[^reward] ------------------- @@ -49,3 +50,4 @@ Note: All solutions to verification challenges need to satisfy the criteria esta in addition to the ones listed above. [^challenge_id]: The number of the challenge sorted by publication date. +[^reward]: Leave it as TBD when creating a new challenge. This should only be filled by the reward committee. diff --git a/doc/src/challenges/0001-core-transmutation.md b/doc/src/challenges/0001-core-transmutation.md index 2b53256b3c34e..66352a0ecb273 100644 --- a/doc/src/challenges/0001-core-transmutation.md +++ b/doc/src/challenges/0001-core-transmutation.md @@ -2,8 +2,9 @@ - **Status:** Open - **Tracking Issue:** [#19](https://github.com/model-checking/verify-rust-std/issues/19) -- **Start date:** 2024-06-12 -- **End date:** 2024-12-10 +- **Start date:** *2024/06/12* +- **End date:** *2025/04/10* +- **Reward:** *N/A* ------------------- diff --git a/doc/src/challenges/0002-intrinsics-memory.md b/doc/src/challenges/0002-intrinsics-memory.md index 185e04e5a3e2a..31c1c43225250 100644 --- a/doc/src/challenges/0002-intrinsics-memory.md +++ b/doc/src/challenges/0002-intrinsics-memory.md @@ -2,8 +2,9 @@ - **Status:** Open - **Tracking Issue:** [#16](https://github.com/model-checking/verify-rust-std/issues/16) -- **Start date:** *24/06/12* -- **End date:** *24/12/10* +- **Start date:** *2024/06/12* +- **End date:** *2025/04/10* +- **Reward:** *N/A* ------------------- diff --git a/doc/src/challenges/0003-pointer-arithmentic.md b/doc/src/challenges/0003-pointer-arithmentic.md index 5362983ffe0f3..902d3a7f55752 100644 --- a/doc/src/challenges/0003-pointer-arithmentic.md +++ b/doc/src/challenges/0003-pointer-arithmentic.md @@ -1,10 +1,10 @@ # Challenge 3: Verifying Raw Pointer Arithmetic Operations - **Status:** Open -- **Solution:** - **Tracking Issue:** [#76](https://github.com/model-checking/verify-rust-std/issues/76) -- **Start date:** 24/06/24 -- **End date:** 24/12/10 +- **Start date:** *2024/06/24* +- **End date:** *2025/04/10* +- **Reward:** *N/A* ------------------- diff --git a/doc/src/challenges/0004-btree-node.md b/doc/src/challenges/0004-btree-node.md index 835d71365292f..838d9199b400b 100644 --- a/doc/src/challenges/0004-btree-node.md +++ b/doc/src/challenges/0004-btree-node.md @@ -2,8 +2,9 @@ - **Status:** Open - **Tracking Issue:** [#77](https://github.com/model-checking/verify-rust-std/issues/77) -- **Start date:** *2024-07-01* -- **End date:** *2024-12-10* +- **Start date:** *2024/07/01* +- **End date:** *2025/04/10* +- **Reward:** *10,000 USD* ------------------- diff --git a/doc/src/challenges/0005-linked-list.md b/doc/src/challenges/0005-linked-list.md index a5c931712025a..b10d6e743cf14 100644 --- a/doc/src/challenges/0005-linked-list.md +++ b/doc/src/challenges/0005-linked-list.md @@ -2,8 +2,9 @@ - **Status:** Open - **Tracking Issue:** [#29](https://github.com/model-checking/verify-rust-std/issues/29) -- **Start date:** *24/07/01* -- **End date:** *24/12/10* +- **Start date:** *2024/07/01* +- **End date:** *2025/04/10* +- **Reward:** *5,000 USD* ------------------- @@ -23,7 +24,7 @@ The memory safety of the following public functions that iterating over the inte | Function | Location | |---------|---------| -|clearn | alloc::collections::linked_list | +|clear| alloc::collections::linked_list | |contains| alloc::collections::linked_list | |split_off| alloc::collections::linked_list | |remove| alloc::collections::linked_list | diff --git a/doc/src/challenges/0006-nonnull.md b/doc/src/challenges/0006-nonnull.md index 923e00427ad62..86cb8366a36a2 100644 --- a/doc/src/challenges/0006-nonnull.md +++ b/doc/src/challenges/0006-nonnull.md @@ -2,8 +2,9 @@ - **Status:** Open - **Tracking Issue:** [#53](https://github.com/model-checking/verify-rust-std/issues/53) -- **Start date:** *2024-08-16* -- **End date:** *2024-12-10* +- **Start date:** *2024/08/16* +- **End date:** *2025/04/10* +- **Reward:** *N/A* ------------------- diff --git a/doc/src/challenges/0007-atomic-types.md b/doc/src/challenges/0007-atomic-types.md index 69bff582f7751..eecaf24f5b37e 100644 --- a/doc/src/challenges/0007-atomic-types.md +++ b/doc/src/challenges/0007-atomic-types.md @@ -2,8 +2,9 @@ - **Status:** Open - **Tracking Issue:** [#83](https://github.com/model-checking/verify-rust-std/issues/83) -- **Start date:** *2024-10-30* -- **End date:** *2024-12-10* +- **Start date:** *2024/10/30* +- **End date:** *2025/04/10* +- **Reward:** *10,000 USD* ------------------- diff --git a/doc/src/challenges/0008-smallsort.md b/doc/src/challenges/0008-smallsort.md index c6632af9af837..1052031506517 100644 --- a/doc/src/challenges/0008-smallsort.md +++ b/doc/src/challenges/0008-smallsort.md @@ -2,8 +2,9 @@ - **Status:** Open - **Tracking Issue:** [#56](https://github.com/model-checking/verify-rust-std/issues/56) -- **Start date:** *2024-08-17* -- **End date:** *2024-12-10* +- **Start date:** *2024/08/17* +- **End date:** *2025/04/10* +- **Reward:** *10,000 USD* ------------------- diff --git a/doc/src/challenges/0009-duration.md b/doc/src/challenges/0009-duration.md index e2af60ec6c1bb..674c296b3742b 100644 --- a/doc/src/challenges/0009-duration.md +++ b/doc/src/challenges/0009-duration.md @@ -2,8 +2,9 @@ - **Status:** Open - **Tracking Issue:** [#72](https://github.com/model-checking/verify-rust-std/issues/72) -- **Start date:** *2024-08-20* -- **End date:** *2024-12-20* +- **Start date:** *2024/08/20* +- **End date:** *2025/04/10* +- **Reward:** *N/A* ------------------- diff --git a/doc/src/challenges/0010-string.md b/doc/src/challenges/0010-string.md index 4783841bee429..8d884f34a55c7 100644 --- a/doc/src/challenges/0010-string.md +++ b/doc/src/challenges/0010-string.md @@ -2,8 +2,9 @@ - **Status:** Open - **Tracking Issue:** [#61](https://github.com/model-checking/verify-rust-std/issues/61) -- **Start date:** *2024-08-19* -- **End date:** *2024-12-10* +- **Start date:** *2024/08/19* +- **End date:** *2025/04/10* +- **Reward:** *N/A* ------------------- diff --git a/doc/src/challenges/0011-floats-ints.md b/doc/src/challenges/0011-floats-ints.md index 9dde411c527ca..1a1c872b88f1f 100644 --- a/doc/src/challenges/0011-floats-ints.md +++ b/doc/src/challenges/0011-floats-ints.md @@ -3,8 +3,9 @@ - **Status:** Open - **Tracking Issue:** [#59](https://github.com/model-checking/verify-rust-std/issues/59) -- **Start date:** *2024-08-20* -- **End date:** *2024-12-10* +- **Start date:** *2024/08/20* +- **End date:** *2025/04/10* +- **Reward:** *N/A* ------------------- diff --git a/doc/src/challenges/0012-nonzero.md b/doc/src/challenges/0012-nonzero.md index 15d2abbb8eb3c..d5252cd939da7 100644 --- a/doc/src/challenges/0012-nonzero.md +++ b/doc/src/challenges/0012-nonzero.md @@ -2,8 +2,9 @@ - **Status:** Open - **Tracking Issue:** [#71](https://github.com/model-checking/verify-rust-std/issues/71) -- **Start date:** *2024-08-23* -- **End date:** *2024-12-10* +- **Start date:** *2024/08/23* +- **End date:** *2025/04/10* +- **Reward:** *N/A* ------------------- diff --git a/doc/src/challenges/0013-cstr.md b/doc/src/challenges/0013-cstr.md new file mode 100644 index 0000000000000..bb0a20808ebd2 --- /dev/null +++ b/doc/src/challenges/0013-cstr.md @@ -0,0 +1,86 @@ +# Challenge 13: Safety of `CStr` + +- **Status:** Open +- **Solution:** +- **Tracking Issue:** [#150](https://github.com/model-checking/verify-rust-std/issues/150) +- **Start date:** *2024/11/04* +- **End date:** *2025/04/10* +- **Reward:** *N/A* + +------------------- +## Goal + +Verify that `CStr` safely represents a borrowed reference to a null-terminated array of bytes sequences similar to +the C string representation. + +## Motivation + +The `CStr` structure is meant to be used to build safe wrappers of FFI functions that may leverage `CStr::as_ptr` +and the unsafe `CStr::from_ptr` constructor to provide a safe interface to other consumers. +It provides safe methods to convert `CStr` to a Rust `&str` by performing UTF-8 validation, or into an owned `CString`. + +Any issue with this structure or misusage of its unsafe methods could trigger an invalid memory access, which poses +a security risk for their users. + +## Description + +The goal of this challenge is to ensure the safety of the `CStr` struct implementation. +First, we need to specify a safety invariant that captures the essential safety properties that must be maintained. + +Next, we should verify that all the safe, public methods respect this invariant. +For example, we can check that creating a `CStr` from a byte slice with method `from_bytes_with_nul` will only yield +safe values of `CStr`. + +Finally, for unsafe methods like `from_ptr()` and `from_bytes_with_nul_unchecked`, we need to specify appropriate safety contracts. +These contracts should ensure no undefined behavior occurs within the unsafe methods themselves, +and that they maintain the overall safety invariant of `CStr` when called correctly. + +### Assumptions + +- Harnesses may be bounded. + +### Success Criteria + +1. Implement the `Invariant` trait for `CStr`. + +2. Verify that the `CStr` safety invariant holds after calling any of the following public safe methods. + +| Function | Location | +|------------------------|--------------------| +| `from_bytes_until_nul` | `core::ffi::c_str` | +| `from_bytes_with_nul` | `core::ffi::c_str` | +| `count_bytes` | `core::ffi::c_str` | +| `is_empty` | `core::ffi::c_str` | +| `to_bytes` | `core::ffi::c_str` | +| `to_bytes_with_nul` | `core::ffi::c_str` | +| `bytes` | `core::ffi::c_str` | +| `to_str` | `core::ffi::c_str` | +| `as_ptr` | `core::ffi::c_str` | + +3. Annotate and verify the safety contracts for the following unsafe functions: + +| Function | Location | +|--------------------------------|---------------------| +| `from_ptr` | `core::ffi::c_str` | +| `from_bytes_with_nul_uncheked` | `core::ffi::c_str` | +| `strlen` | `core::ffi::c_str` | + +4. Verify that the following trait implementations for the `CStr` type are safe: + + +| Trait | Implementation Location | +|-------------------------------------|-------------------------| +| `CloneToUninit` [^unsafe-fn] | `core::clone` | +| `ops::Index>` | `core::ffi::c_str` | + +[^unsafe-fn]: Unsafe functions will require safety contracts. + +All proofs must automatically ensure the absence of the following undefined behaviors [ref](https://github.com/rust-lang/reference/blob/142b2ed77d33f37a9973772bd95e6144ed9dce43/src/behavior-considered-undefined.md): + +- Accessing (loading from or storing to) a place that is dangling or based on a misaligned pointer. +- Performing a place projection that violates the requirements of in-bounds pointer arithmetic. +- Mutating immutable bytes. +- Accessing uninitialized memory. + +Note: All solutions to verification challenges need to satisfy the criteria established in the +[challenge book](../general-rules.md) in addition to the ones listed above. diff --git a/doc/src/intro.md b/doc/src/intro.md index 441d339dcf72d..47e50a97a2ae6 100644 --- a/doc/src/intro.md +++ b/doc/src/intro.md @@ -6,12 +6,22 @@ library](https://doc.rust-lang.org/std/). The goal of this is to provide automated verification that can be used to verify that a given Rust standard library implementation is safe. +Verifying the Rust libraries is difficult because: +1. Lack of a specification, +2. Lack of an existing verification mechanism in the Rust ecosystem, +3. The large size of the verification problem, +4. The unknowns of scalable verification. + +Given the magnitude and scope of the effort, we believe this should be a community owned effort. +For that, we are launching a contest that includes a series of challenges that focus on verifying +memory safety and a subset of undefined behaviors in the Rust standard library. + Efforts are largely classified in the following areas: 1. Contributing to the core mechanism of verifying the rust standard library 2. Creating new techniques to perform scalable verification 3. Apply techniques to verify previously unverified parts of the standard library. +There is a financial award tied to each challenge per its specification, which is awarded upon its successful completion. -We encourage everyone to watch this repository to be notified of any -changes. \ No newline at end of file +We encourage everyone to watch this repository to be notified of any changes. \ No newline at end of file diff --git a/doc/src/tool_template.md b/doc/src/tool_template.md index 474b1d089c6ee..c5d56b97b80d5 100644 --- a/doc/src/tool_template.md +++ b/doc/src/tool_template.md @@ -20,12 +20,12 @@ _Please list the license(s) that are used by your tool, and if to your knowledge ## Steps to Use the Tool -1. [First Step] -2. [Second Step] -3. [and so on...] +1. \[First Step\] +2. \[Second Step\] +3. \[and so on...\] ## Artifacts -_If there are noteworthy examples of using the tool to perform verificaiton, please include them in this section.Links, papers, etc._ +_If there are noteworthy examples of using the tool to perform verification, please include them in this section.Links, papers, etc._ ## CI & Versioning _Please describe how you version the tool and how it will be supported in CI pipelines._ diff --git a/library/core/src/ffi/c_str.rs b/library/core/src/ffi/c_str.rs index 93dd351b02958..2a65b2415f7d3 100644 --- a/library/core/src/ffi/c_str.rs +++ b/library/core/src/ffi/c_str.rs @@ -9,6 +9,11 @@ use crate::ptr::NonNull; use crate::slice::memchr; use crate::{fmt, intrinsics, ops, slice, str}; +use crate::ub_checks::Invariant; + +#[cfg(kani)] +use crate::kani; + // FIXME: because this is doc(inline)d, we *have* to use intra-doc links because the actual link // depends on where the item is being documented. however, since this is libcore, we can't // actually reference libstd or liballoc in intra-doc links. so, the best we can do is remove the @@ -207,6 +212,22 @@ impl fmt::Display for FromBytesWithNulError { } } +#[unstable(feature = "ub_checks", issue = "none")] +impl Invariant for &CStr { + /** + * Safety invariant of a valid CStr: + * 1. An empty CStr should have a null byte. + * 2. A valid CStr should end with a null-terminator and contains + * no intermediate null bytes. + */ + fn is_safe(&self) -> bool { + let bytes: &[c_char] = &self.inner; + let len = bytes.len(); + + !bytes.is_empty() && bytes[len - 1] == 0 && !bytes[..len-1].contains(&0) + } +} + impl CStr { /// Wraps a raw C string with a safe C string wrapper. /// @@ -833,3 +854,25 @@ impl Iterator for Bytes<'_> { #[unstable(feature = "cstr_bytes", issue = "112115")] impl FusedIterator for Bytes<'_> {} + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use super::*; + + // pub const fn from_bytes_until_nul(bytes: &[u8]) -> Result<&CStr, FromBytesUntilNulError> + #[kani::proof] + #[kani::unwind(32)] // 7.3 seconds when 16; 33.1 seconds when 32 + fn check_from_bytes_until_nul() { + const MAX_SIZE: usize = 32; + let string: [u8; MAX_SIZE] = kani::any(); + // Covers the case of a single null byte at the end, no null bytes, as + // well as intermediate null bytes + let slice = kani::slice::any_slice_of_array(&string); + + let result = CStr::from_bytes_until_nul(slice); + if let Ok(c_str) = result { + assert!(c_str.is_safe()); + } + } +} \ No newline at end of file diff --git a/library/core/src/lib.rs b/library/core/src/lib.rs index 280fda93a5494..2c813ca0cb412 100644 --- a/library/core/src/lib.rs +++ b/library/core/src/lib.rs @@ -230,6 +230,8 @@ #![feature(unboxed_closures)] #![feature(unsized_fn_params)] #![feature(with_negative_coherence)] +// Required for Kani loop contracts, which are annotated as custom stmt attributes. +#![feature(proc_macro_hygiene)] // tidy-alphabetical-end // // Target features: diff --git a/library/core/src/num/nonzero.rs b/library/core/src/num/nonzero.rs index f04c83693ef63..162c599b3468f 100644 --- a/library/core/src/num/nonzero.rs +++ b/library/core/src/num/nonzero.rs @@ -8,7 +8,9 @@ use crate::ops::{BitOr, BitOrAssign, Div, DivAssign, Neg, Rem, RemAssign}; use crate::panic::{RefUnwindSafe, UnwindSafe}; use crate::str::FromStr; use crate::{fmt, intrinsics, ptr, ub_checks}; - +use safety::{ensures, requires}; +#[cfg(kani)] +use crate::kani; /// A marker trait for primitive types which can be zero. /// /// This is an implementation detail for [NonZero]\ which may disappear or be replaced at any time. @@ -364,6 +366,27 @@ where #[rustc_const_stable(feature = "nonzero", since = "1.28.0")] #[must_use] #[inline] + // #[rustc_allow_const_fn_unstable(const_refs_to_cell)] enables byte-level + // comparisons within const functions. This is needed here to validate the + // contents of `T` by converting a pointer to a `u8` slice for our `requires` + // and `ensures` checks. + #[rustc_allow_const_fn_unstable(const_refs_to_cell)] + #[requires({ + let size = core::mem::size_of::(); + let ptr = &n as *const T as *const u8; + let slice = unsafe { core::slice::from_raw_parts(ptr, size) }; + !slice.iter().all(|&byte| byte == 0) + })] + #[ensures(|result: &Self|{ + let size = core::mem::size_of::(); + let n_ptr: *const T = &n; + let result_inner: T = result.get(); + let result_ptr: *const T = &result_inner; + let n_slice = unsafe { core::slice::from_raw_parts(n_ptr as *const u8, size) }; + let result_slice = unsafe { core::slice::from_raw_parts(result_ptr as *const u8, size) }; + + n_slice == result_slice + })] pub const unsafe fn new_unchecked(n: T) -> Self { match Self::new(n) { Some(n) => n, @@ -2159,3 +2182,36 @@ nonzero_integer! { swapped = "0x5634129078563412", reversed = "0x6a2c48091e6a2c48", } + +#[unstable(feature="kani", issue="none")] +#[cfg(kani)] +mod verify { + use super::*; + + macro_rules! nonzero_check { + ($t:ty, $nonzero_type:ty, $nonzero_check_new_unchecked_for:ident) => { + #[kani::proof_for_contract(NonZero::new_unchecked)] + pub fn $nonzero_check_new_unchecked_for() { + let x: $t = kani::any(); // Generates a symbolic value of the provided type + + unsafe { + <$nonzero_type>::new_unchecked(x); // Calls NonZero::new_unchecked for the specified NonZero type + } + } + }; + } + + // Use the macro to generate different versions of the function for multiple types + nonzero_check!(i8, core::num::NonZeroI8, nonzero_check_new_unchecked_for_i8); + nonzero_check!(i16, core::num::NonZeroI16, nonzero_check_new_unchecked_for_16); + nonzero_check!(i32, core::num::NonZeroI32, nonzero_check_new_unchecked_for_32); + nonzero_check!(i64, core::num::NonZeroI64, nonzero_check_new_unchecked_for_64); + nonzero_check!(i128, core::num::NonZeroI128, nonzero_check_new_unchecked_for_128); + nonzero_check!(isize, core::num::NonZeroIsize, nonzero_check_new_unchecked_for_isize); + nonzero_check!(u8, core::num::NonZeroU8, nonzero_check_new_unchecked_for_u8); + nonzero_check!(u16, core::num::NonZeroU16, nonzero_check_new_unchecked_for_u16); + nonzero_check!(u32, core::num::NonZeroU32, nonzero_check_new_unchecked_for_u32); + nonzero_check!(u64, core::num::NonZeroU64, nonzero_check_new_unchecked_for_u64); + nonzero_check!(u128, core::num::NonZeroU128, nonzero_check_new_unchecked_for_u128); + nonzero_check!(usize, core::num::NonZeroUsize, nonzero_check_new_unchecked_for_usize); +} diff --git a/library/core/src/ptr/const_ptr.rs b/library/core/src/ptr/const_ptr.rs index 57a7c0fc0925c..c7f762dabe3d3 100644 --- a/library/core/src/ptr/const_ptr.rs +++ b/library/core/src/ptr/const_ptr.rs @@ -3,6 +3,10 @@ use crate::cmp::Ordering::{Equal, Greater, Less}; use crate::intrinsics::const_eval_select; use crate::mem::SizedTypeProperties; use crate::slice::{self, SliceIndex}; +use safety::{ensures, requires}; + +#[cfg(kani)] +use crate::kani; impl *const T { /// Returns `true` if the pointer is null. @@ -667,6 +671,16 @@ impl *const T { #[rustc_const_stable(feature = "const_ptr_offset_from", since = "1.65.0")] #[inline] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces + #[requires( + // Ensures subtracting `origin` from `self` doesn't overflow + (self as isize).checked_sub(origin as isize).is_some() && + // Ensure the distance between `self` and `origin` is aligned to `T` + (self as isize - origin as isize) % (mem::size_of::() as isize) == 0 && + // Ensure both pointers are in the same allocation or are pointing to the same address + (self as isize == origin as isize || kani::mem::same_allocation(self, origin)) + )] + // The result should equal the distance in terms of elements of type `T` as per the documentation above + #[ensures(|result| *result == (self as isize - origin as isize) / (mem::size_of::() as isize))] pub const unsafe fn offset_from(self, origin: *const T) -> isize where T: Sized, @@ -1899,3 +1913,149 @@ impl PartialOrd for *const T { *self >= *other } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +mod verify { + use crate::kani; + use core::mem; + use kani::PointerGenerator; + + // Proof for unit size will panic as offset_from needs the pointee size to be greater then 0 + #[kani::proof_for_contract(<*const ()>::offset_from)] + #[kani::should_panic] + pub fn check_const_offset_from_unit() { + let val: () = (); + let src_ptr: *const () = &val; + let dest_ptr: *const () = &val; + unsafe { + dest_ptr.offset_from(src_ptr); + } + } + + // Array size bound for kani::any_array + const ARRAY_LEN: usize = 40; + + macro_rules! generate_offset_from_harness { + ($type: ty, $proof_name1: ident, $proof_name2: ident) => { + // Proof for a single element + #[kani::proof_for_contract(<*const $type>::offset_from)] + pub fn $proof_name1() { + const gen_size: usize = mem::size_of::<$type>(); + let mut generator1 = PointerGenerator::::new(); + let mut generator2 = PointerGenerator::::new(); + let ptr1: *const $type = generator1.any_in_bounds().ptr; + let ptr2: *const $type = if kani::any() { + generator1.any_alloc_status().ptr + } else { + generator2.any_alloc_status().ptr + }; + + unsafe { + ptr1.offset_from(ptr2); + } + } + + // Proof for large arrays + #[kani::proof_for_contract(<*const $type>::offset_from)] + pub fn $proof_name2() { + const gen_size: usize = mem::size_of::<$type>(); + let mut generator1 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let mut generator2 = PointerGenerator::<{ gen_size * ARRAY_LEN }>::new(); + let ptr1: *const $type = generator1.any_in_bounds().ptr; + let ptr2: *const $type = if kani::any() { + generator1.any_alloc_status().ptr + } else { + generator2.any_alloc_status().ptr + }; + + unsafe { + ptr1.offset_from(ptr2); + } + } + }; + } + + generate_offset_from_harness!( + u8, + check_const_offset_from_u8, + check_const_offset_from_u8_arr + ); + generate_offset_from_harness!( + u16, + check_const_offset_from_u16, + check_const_offset_from_u16_arr + ); + generate_offset_from_harness!( + u32, + check_const_offset_from_u32, + check_const_offset_from_u32_arr + ); + generate_offset_from_harness!( + u64, + check_const_offset_from_u64, + check_const_offset_from_u64_arr + ); + generate_offset_from_harness!( + u128, + check_const_offset_from_u128, + check_const_offset_from_u128_arr + ); + generate_offset_from_harness!( + usize, + check_const_offset_from_usize, + check_const_offset_from_usize_arr + ); + + generate_offset_from_harness!( + i8, + check_const_offset_from_i8, + check_const_offset_from_i8_arr + ); + generate_offset_from_harness!( + i16, + check_const_offset_from_i16, + check_const_offset_from_i16_arr + ); + generate_offset_from_harness!( + i32, + check_const_offset_from_i32, + check_const_offset_from_i32_arr + ); + generate_offset_from_harness!( + i64, + check_const_offset_from_i64, + check_const_offset_from_i64_arr + ); + generate_offset_from_harness!( + i128, + check_const_offset_from_i128, + check_const_offset_from_i128_arr + ); + generate_offset_from_harness!( + isize, + check_const_offset_from_isize, + check_const_offset_from_isize_arr + ); + + generate_offset_from_harness!( + (i8, i8), + check_const_offset_from_tuple_1, + check_const_offset_from_tuple_1_arr + ); + generate_offset_from_harness!( + (f64, bool), + check_const_offset_from_tuple_2, + check_const_offset_from_tuple_2_arr + ); + generate_offset_from_harness!( + (u32, i16, f32), + check_const_offset_from_tuple_3, + check_const_offset_from_tuple_3_arr + ); + generate_offset_from_harness!( + ((), bool, u8, u16, i32, f64, i128, usize), + check_const_offset_from_tuple_4, + check_const_offset_from_tuple_4_arr + ); +} diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 0aa306f803a70..42ea9d75896d3 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -10,9 +10,10 @@ use crate::ub_checks::assert_unsafe_precondition; use crate::{fmt, hash, intrinsics, ptr}; use safety::{ensures, requires}; - #[cfg(kani)] use crate::kani; +#[cfg(kani)] +use crate::ub_checks; /// `*mut T` but non-zero and [covariant]. /// @@ -111,6 +112,7 @@ impl NonNull { #[rustc_const_stable(feature = "const_nonnull_dangling", since = "1.36.0")] #[must_use] #[inline] + #[ensures(|result| !result.pointer.is_null() && result.pointer.is_aligned())] pub const fn dangling() -> Self { // SAFETY: ptr::dangling_mut() returns a non-null well-aligned pointer. unsafe { @@ -137,6 +139,8 @@ impl NonNull { #[must_use] #[unstable(feature = "ptr_as_uninit", issue = "75402")] #[rustc_const_unstable(feature = "ptr_as_uninit", issue = "75402")] + #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure the pointer is valid to create a reference. + #[ensures(|result: &&MaybeUninit| core::ptr::eq(*result, self.cast().as_ptr()))] // Ensure returned reference points to the correct memory location. pub const unsafe fn as_uninit_ref<'a>(self) -> &'a MaybeUninit { // SAFETY: the caller must guarantee that `self` meets all the // requirements for a reference. @@ -161,6 +165,8 @@ impl NonNull { #[must_use] #[unstable(feature = "ptr_as_uninit", issue = "75402")] #[rustc_const_unstable(feature = "ptr_as_uninit", issue = "75402")] + #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure pointer is valid to create a mutable reference. + #[ensures(|result: &&mut MaybeUninit| core::ptr::eq(*result, self.cast().as_ptr()))] // Ensure the returned reference points to the correct memory. pub const unsafe fn as_uninit_mut<'a>(self) -> &'a mut MaybeUninit { // SAFETY: the caller must guarantee that `self` meets all the // requirements for a reference. @@ -264,6 +270,7 @@ impl NonNull { #[unstable(feature = "ptr_metadata", issue = "81513")] #[rustc_const_unstable(feature = "ptr_metadata", issue = "81513")] #[inline] + #[ensures(|result| !result.pointer.is_null())] pub const fn from_raw_parts( data_pointer: NonNull<()>, metadata: ::Metadata, @@ -282,6 +289,8 @@ impl NonNull { #[must_use = "this returns the result of the operation, \ without modifying the original"] #[inline] + #[ensures(|(data_ptr, metadata)| !data_ptr.as_ptr().is_null())] + #[ensures(|(data_ptr, metadata)| self.as_ptr() as *const () == data_ptr.as_ptr() as *const ())] pub const fn to_raw_parts(self) -> (NonNull<()>, ::Metadata) { (self.cast(), super::metadata(self.as_ptr())) } @@ -294,6 +303,7 @@ impl NonNull { #[must_use] #[inline] #[stable(feature = "strict_provenance", since = "CURRENT_RUSTC_VERSION")] + #[ensures(|result| result.get() == self.as_ptr() as *const() as usize)] pub fn addr(self) -> NonZero { // SAFETY: The pointer is guaranteed by the type to be non-null, // meaning that the address will be non-zero. @@ -383,6 +393,8 @@ impl NonNull { #[rustc_const_stable(feature = "const_nonnull_as_ref", since = "1.73.0")] #[must_use] #[inline(always)] + #[requires(ub_checks::can_dereference(self.as_ptr() as *const()))] // Ensure input is convertible to a reference + #[ensures(|result: &&T| core::ptr::eq(*result, self.as_ptr()))] // Ensure returned reference matches pointer pub const unsafe fn as_ref<'a>(&self) -> &'a T { // SAFETY: the caller must guarantee that `self` meets all the // requirements for a reference. @@ -421,6 +433,9 @@ impl NonNull { #[rustc_const_stable(feature = "const_ptr_as_ref", since = "1.83.0")] #[must_use] #[inline(always)] + #[requires(ub_checks::can_dereference(self.as_ptr() as *const()))] + // verify result (a mutable reference) is still associated with the same memory address as the raw pointer stored in self + #[ensures(|result: &&mut T| core::ptr::eq(*result, self.as_ptr()))] pub const unsafe fn as_mut<'a>(&mut self) -> &'a mut T { // SAFETY: the caller must guarantee that `self` meets all the // requirements for a mutable reference. @@ -567,6 +582,11 @@ impl NonNull { #[must_use = "returns a new pointer rather than modifying its argument"] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] + #[requires(count.checked_mul(core::mem::size_of::()).is_some() + && count * core::mem::size_of::() <= isize::MAX as usize + && (self.pointer as isize).checked_add(count as isize * core::mem::size_of::() as isize).is_some() // check wrapping add + && kani::mem::same_allocation(self.pointer, self.pointer.wrapping_offset(count as isize)))] + #[ensures(|result: &NonNull| result.as_ptr() == self.as_ptr().offset(count as isize))] pub const unsafe fn add(self, count: usize) -> Self where T: Sized, @@ -645,6 +665,12 @@ impl NonNull { #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] #[cfg_attr(bootstrap, rustc_allow_const_fn_unstable(unchecked_neg))] + #[requires( + count.checked_mul(core::mem::size_of::()).is_some() && + count * core::mem::size_of::() <= isize::MAX as usize && + kani::mem::same_allocation(self.as_ptr(), self.as_ptr().wrapping_sub(count)) + )] + #[ensures(|result: &NonNull| result.as_ptr() == self.as_ptr().offset(-(count as isize)))] pub const unsafe fn sub(self, count: usize) -> Self where T: Sized, @@ -774,6 +800,11 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] + #[requires( + (kani::mem::same_allocation(self.as_ptr(), origin.as_ptr()) && + ((self.as_ptr().addr() - origin.as_ptr().addr()) % core::mem::size_of::() == 0)) + )] // Ensure both pointers meet safety conditions for offset_from + #[ensures(|result: &isize| *result == (self.as_ptr() as isize - origin.as_ptr() as isize) / core::mem::size_of::() as isize)] pub const unsafe fn offset_from(self, origin: NonNull) -> isize where T: Sized, @@ -867,6 +898,13 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[unstable(feature = "ptr_sub_ptr", issue = "95892")] #[rustc_const_unstable(feature = "const_ptr_sub_ptr", issue = "95892")] + #[requires( + self.as_ptr().addr().checked_sub(subtracted.as_ptr().addr()).is_some() && + kani::mem::same_allocation(self.as_ptr(), subtracted.as_ptr()) && + (self.as_ptr().addr()) >= (subtracted.as_ptr().addr()) && + (self.as_ptr().addr() - subtracted.as_ptr().addr()) % core::mem::size_of::() == 0 + )] + #[ensures(|result: &usize| *result == self.as_ptr().offset_from(subtracted.as_ptr()) as usize)] pub const unsafe fn sub_ptr(self, subtracted: NonNull) -> usize where T: Sized, @@ -904,6 +942,7 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] + #[requires(ub_checks::can_dereference(self.pointer))] pub const unsafe fn read(self) -> T where T: Sized, @@ -925,6 +964,7 @@ impl NonNull { #[inline] #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] + #[requires(ub_checks::can_dereference(self.pointer))] pub unsafe fn read_volatile(self) -> T where T: Sized, @@ -945,6 +985,7 @@ impl NonNull { #[cfg_attr(miri, track_caller)] // even without panics, this helps for Miri backtraces #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_stable(feature = "non_null_convenience", since = "1.80.0")] + #[requires(ub_checks::can_read_unaligned(self.pointer))] pub const unsafe fn read_unaligned(self) -> T where T: Sized, @@ -1040,6 +1081,8 @@ impl NonNull { /// [`ptr::drop_in_place`]: crate::ptr::drop_in_place() #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] + #[requires(ub_checks::can_dereference(self.as_ptr() as *const()))] // Ensure self is aligned, initialized, and valid for read + #[requires(ub_checks::can_write(self.as_ptr() as *mut()))] // Ensure self is valid for write pub unsafe fn drop_in_place(self) { // SAFETY: the caller must uphold the safety contract for `drop_in_place`. unsafe { ptr::drop_in_place(self.as_ptr()) } @@ -1131,6 +1174,9 @@ impl NonNull { /// [`ptr::replace`]: crate::ptr::replace() #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] + #[cfg_attr(kani, kani::modifies(self.as_ptr()))] + #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure self is aligned, initialized, and valid for read + #[requires(ub_checks::can_write(self.as_ptr()))] // Ensure self is valid for write pub unsafe fn replace(self, src: T) -> T where T: Sized, @@ -1149,6 +1195,9 @@ impl NonNull { #[inline(always)] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_unstable(feature = "const_swap", issue = "83163")] + #[cfg_attr(kani, kani::modifies(self.as_ptr(), with.as_ptr()))] + #[requires(ub_checks::can_dereference(self.as_ptr()) && ub_checks::can_write(self.as_ptr()))] + #[requires(ub_checks::can_dereference(with.as_ptr()) && ub_checks::can_write(with.as_ptr()))] pub const unsafe fn swap(self, with: NonNull) where T: Sized, @@ -1208,6 +1257,36 @@ impl NonNull { #[must_use] #[stable(feature = "non_null_convenience", since = "1.80.0")] #[rustc_const_unstable(feature = "const_align_offset", issue = "90962")] + #[ensures(|result| { + // Post-condition reference: https://github.com/model-checking/verify-rust-std/pull/69/files + let stride = crate::mem::size_of::(); + // ZSTs + if stride == 0 { + if self.pointer.addr() % align == 0 { + return *result == 0; + } else { + return *result == usize::MAX; + } + } + // In this case, the pointer cannot be aligned + if (align % stride == 0) && (self.pointer.addr() % stride != 0) { + return *result == usize::MAX; + } + // Checking if the answer should indeed be usize::MAX when align % stride != 0 + // requires computing gcd(a, stride), which is too expensive without + // quantifiers (https://model-checking.github.io/kani/rfc/rfcs/0010-quantifiers.html). + // This should be updated once quantifiers are available. + if (align % stride != 0 && *result == usize::MAX) { + return true; + } + // If we reach this case, either: + // - align % stride == 0 and self.pointer.addr() % stride == 0, so it is definitely possible to align the pointer + // - align % stride != 0 and result != usize::MAX, so align_offset is claiming that it's possible to align the pointer + // Check that applying the returned result does indeed produce an aligned address + let product = usize::wrapping_mul(*result, stride); + let new_addr = usize::wrapping_add(product, self.pointer.addr()); + *result != usize::MAX && new_addr % align == 0 + })] pub const fn align_offset(self, align: usize) -> usize where T: Sized, @@ -1330,6 +1409,7 @@ impl NonNull { #[must_use] #[stable(feature = "pointer_is_aligned", since = "1.79.0")] #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")] + #[ensures(|result: &bool| *result == (self.as_ptr().addr() % core::mem::align_of::() == 0))] pub const fn is_aligned(self) -> bool where T: Sized, @@ -1445,6 +1525,8 @@ impl NonNull { #[must_use] #[unstable(feature = "pointer_is_aligned_to", issue = "96284")] #[rustc_const_unstable(feature = "const_pointer_is_aligned", issue = "104203")] + #[requires(align.is_power_of_two())] + #[ensures(|result: &bool| *result == (self.as_ptr().addr() % align == 0))] // Ensure the returned value is correct based on the given alignment pub const fn is_aligned_to(self, align: usize) -> bool { self.pointer.is_aligned_to(align) } @@ -1476,6 +1558,9 @@ impl NonNull<[T]> { #[rustc_const_stable(feature = "const_slice_from_raw_parts_mut", since = "1.83.0")] #[must_use] #[inline] + #[ensures(|result| !result.pointer.is_null() + && result.pointer as *const T == data.pointer + && unsafe { result.as_ref() }.len() == len)] pub const fn slice_from_raw_parts(data: NonNull, len: usize) -> Self { // SAFETY: `data` is a `NonNull` pointer which is necessarily non-null unsafe { Self::new_unchecked(super::slice_from_raw_parts_mut(data.as_ptr(), len)) } @@ -1601,6 +1686,11 @@ impl NonNull<[T]> { #[must_use] #[unstable(feature = "ptr_as_uninit", issue = "75402")] #[rustc_const_unstable(feature = "ptr_as_uninit", issue = "75402")] + #[requires(self.as_ptr().cast::().align_offset(core::mem::align_of::()) == 0)] // Ensure the pointer is properly aligned + #[requires(self.len().checked_mul(core::mem::size_of::()).is_some() && self.len() * core::mem::size_of::() <= isize::MAX as usize)] // Ensure the slice size does not exceed isize::MAX + #[requires(kani::mem::same_allocation(self.as_ptr() as *const(), self.as_ptr().byte_add(self.len() * core::mem::size_of::()) as *const()))] // Ensure the slice is contained within a single allocation + #[ensures(|result: &&[MaybeUninit]| result.len() == self.len())] // Length check + #[ensures(|result: &&[MaybeUninit]| core::ptr::eq(result.as_ptr(), self.cast().as_ptr()))] // Ensure the memory addresses match. pub const unsafe fn as_uninit_slice<'a>(self) -> &'a [MaybeUninit] { // SAFETY: the caller must uphold the safety contract for `as_uninit_slice`. unsafe { slice::from_raw_parts(self.cast().as_ptr(), self.len()) } @@ -1666,6 +1756,11 @@ impl NonNull<[T]> { #[must_use] #[unstable(feature = "ptr_as_uninit", issue = "75402")] #[rustc_const_unstable(feature = "ptr_as_uninit", issue = "75402")] + #[requires(self.as_ptr().cast::().align_offset(core::mem::align_of::()) == 0)] // Ensure the pointer is properly aligned + #[requires(self.len().checked_mul(core::mem::size_of::()).is_some() && self.len() * core::mem::size_of::() <= isize::MAX as usize)] // Ensure the slice size does not exceed isize::MAX + #[requires(kani::mem::same_allocation(self.as_ptr() as *const(), self.as_ptr().byte_add(self.len() * core::mem::size_of::()) as *const()))] // Ensure the slice is contained within a single allocation + #[ensures(|result: &&mut [MaybeUninit]| result.len() == self.len())] // Length check + #[ensures(|result: &&mut [MaybeUninit]| core::ptr::eq(result.as_ptr(), self.cast().as_ptr()))] // Address check pub const unsafe fn as_uninit_slice_mut<'a>(self) -> &'a mut [MaybeUninit] { // SAFETY: the caller must uphold the safety contract for `as_uninit_slice_mut`. unsafe { slice::from_raw_parts_mut(self.cast().as_ptr(), self.len()) } @@ -1694,6 +1789,7 @@ impl NonNull<[T]> { /// ``` #[unstable(feature = "slice_ptr_get", issue = "74265")] #[inline] + #[requires(ub_checks::can_dereference(self.as_ptr()))] // Ensure self can be dereferenced pub unsafe fn get_unchecked_mut(self, index: I) -> NonNull where I: SliceIndex<[T]>, @@ -1811,6 +1907,29 @@ impl From<&T> for NonNull { mod verify { use super::*; use crate::ptr::null_mut; + use kani::PointerGenerator; + + trait SampleTrait { + fn get_value(&self) -> i32; + } + + struct SampleStruct { + value: i32, + } + + impl SampleTrait for SampleStruct { + fn get_value(&self) -> i32 { + self.value + } + } + + impl kani::Arbitrary for NonNull { + fn any() -> Self { + let ptr: *mut T = kani::any::() as *mut T; + kani::assume(!ptr.is_null()); + NonNull::new(ptr).expect("Non-null pointer expected") + } + } // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self #[kani::proof_for_contract(NonNull::new_unchecked)] @@ -1821,7 +1940,7 @@ mod verify { } } - // pub const unsafe fn new(ptr: *mut T) -> Option + // pub const fn new(ptr: *mut T) -> Option #[kani::proof_for_contract(NonNull::new)] pub fn non_null_check_new() { let mut x: i32 = kani::any(); @@ -1829,4 +1948,529 @@ mod verify { let maybe_null_ptr = if kani::any() { xptr as *mut i32 } else { null_mut() }; let _ = NonNull::new(maybe_null_ptr); } + + // pub const unsafe fn read(self) -> T where T: Sized + #[kani::proof_for_contract(NonNull::read)] + pub fn non_null_check_read() { + let ptr_u8: *mut u8 = &mut kani::any(); + let nonnull_ptr_u8 = NonNull::new(ptr_u8).unwrap(); + unsafe { + let result = nonnull_ptr_u8.read(); + kani::assert(*ptr_u8 == result, "read returns the correct value"); + } + + // array example + const ARR_LEN: usize = 10000; + let mut generator = PointerGenerator::::new(); + let raw_ptr: *mut i8 = generator.any_in_bounds().ptr; + let nonnull_ptr = unsafe { NonNull::new(raw_ptr).unwrap()}; + unsafe { + let result = nonnull_ptr.read(); + kani::assert( *nonnull_ptr.as_ptr() == result, "read returns the correct value"); + } + } + + // pub unsafe fn read_volatile(self) -> T where T: Sized + #[kani::proof_for_contract(NonNull::read_volatile)] + pub fn non_null_check_read_volatile() { + let ptr_u8: *mut u8 = &mut kani::any(); + let nonnull_ptr_u8 = NonNull::new(ptr_u8).unwrap(); + unsafe { + let result = nonnull_ptr_u8.read_volatile(); + kani::assert(*ptr_u8 == result, "read returns the correct value"); + } + + // array example + const ARR_LEN: usize = 10000; + let mut generator = PointerGenerator::::new(); + let raw_ptr: *mut i8 = generator.any_in_bounds().ptr; + let nonnull_ptr = unsafe { NonNull::new(raw_ptr).unwrap()}; + unsafe { + let result = nonnull_ptr.read_volatile(); + kani::assert( *nonnull_ptr.as_ptr() == result, "read returns the correct value"); + } + } + + #[repr(packed, C)] + struct Packed { + _padding: u8, + unaligned: u32, + } + + // pub const unsafe fn read_unaligned(self) -> T where T: Sized + #[kani::proof_for_contract(NonNull::read_unaligned)] + pub fn non_null_check_read_unaligned() { + // unaligned pointer + let mut generator = PointerGenerator::<10000>::new(); + let unaligned_ptr: *mut u8 = generator.any_in_bounds().ptr; + let unaligned_nonnull_ptr = NonNull::new(unaligned_ptr).unwrap(); + unsafe { + let result = unaligned_nonnull_ptr.read_unaligned(); + kani::assert( *unaligned_nonnull_ptr.as_ptr() == result, "read returns the correct value"); + } + + // read an unaligned value from a packed struct + let unaligned_value: u32 = kani::any(); + let packed = Packed { + _padding: kani::any::(), + unaligned: unaligned_value, + }; + + let unaligned_ptr = ptr::addr_of!(packed.unaligned); + let nonnull_packed_ptr = NonNull::new(unaligned_ptr as *mut u32).unwrap(); + let v = unsafe { nonnull_packed_ptr.read_unaligned() }; + assert_eq!(v, unaligned_value); + } + + // pub const unsafe fn add(self, count: usize) -> Self + #[kani::proof_for_contract(NonNull::add)] + pub fn non_null_check_add() { + const SIZE: usize = 100000; + let mut generator = PointerGenerator::<100000>::new(); + let raw_ptr: *mut i8 = generator.any_in_bounds().ptr; + let ptr = unsafe { NonNull::new(raw_ptr).unwrap()}; + // Create a non-deterministic count value + let count: usize = kani::any(); + + unsafe { + let result = ptr.add(count); + } + } + + // pub fn addr(self) -> NonZero + #[kani::proof_for_contract(NonNull::addr)] + pub fn non_null_check_addr() { + // Create NonNull pointer & get pointer address + let x = kani::any::() as *mut i32; + let Some(nonnull_xptr) = NonNull::new(x) else { return; }; + let address = nonnull_xptr.addr(); + } + + // pub fn align_offset(self, align: usize) -> usize + #[kani::proof_for_contract(NonNull::align_offset)] + pub fn non_null_check_align_offset() { + // Create NonNull pointer + let x = kani::any::() as *mut i32; + let Some(nonnull_xptr) = NonNull::new(x) else { return; }; + + // Call align_offset with valid align value + let align: usize = kani::any(); + kani::assume(align.is_power_of_two()); + nonnull_xptr.align_offset(align); + } + + // pub fn align_offset(self, align: usize) -> usize + #[kani::should_panic] + #[kani::proof_for_contract(NonNull::align_offset)] + pub fn non_null_check_align_offset_negative() { + // Create NonNull pointer + let x = kani::any::() as *mut i8; + let Some(nonnull_xptr) = NonNull::new(x) else { return; }; + + // Generate align value that is not necessarily a power of two + let invalid_align: usize = kani::any(); + + // Trigger panic + let offset = nonnull_xptr.align_offset(invalid_align); + } + + // pub const fn dangling() -> Self + #[kani::proof_for_contract(NonNull::dangling)] + pub fn non_null_check_dangling() { + // unsigned integer types + let ptr_u8 = NonNull::::dangling(); + let ptr_u16 = NonNull::::dangling(); + let ptr_u32 = NonNull::::dangling(); + let ptr_u64 = NonNull::::dangling(); + let ptr_u128 = NonNull::::dangling(); + let ptr_usize = NonNull::::dangling(); + // signed integer types + let ptr_i8 = NonNull::::dangling(); + let ptr_i16 = NonNull::::dangling(); + let ptr_i32 = NonNull::::dangling(); + let ptr_i64 = NonNull::::dangling(); + let ptr_i128 = NonNull::::dangling(); + let ptr_isize = NonNull::::dangling(); + // unit type + let ptr_unit = NonNull::<()>::dangling(); + // zero length slice from dangling unit pointer + let zero_len_slice = NonNull::slice_from_raw_parts(ptr_unit, 0); + } + + // pub const fn from_raw_parts(data_pointer: NonNull<()>, metadata: ::Metadata,) -> NonNull + #[kani::proof_for_contract(NonNull::from_raw_parts)] + #[kani::unwind(101)] + pub fn non_null_check_from_raw_parts() { + const ARR_LEN: usize = 100; + // Create a non-deterministic array and its slice + let arr: [i8; ARR_LEN] = kani::any(); + let arr_slice = kani::slice::any_slice_of_array(&arr); + // Get a raw NonNull pointer to the start of the slice + let arr_slice_raw_ptr = NonNull::new(arr_slice.as_ptr() as *mut ()).unwrap(); + // Create NonNull pointer from the start pointer and the length of the slice + let nonnull_slice = NonNull::<[i8]>::from_raw_parts(arr_slice_raw_ptr, arr_slice.len()); + // Ensure slice content is preserved, runtime at this step is proportional to ARR_LEN + unsafe { + kani::assert(arr_slice == nonnull_slice.as_ref(), "slice content must be preserve"); + } + + // zero-length dangling pointer example + let dangling_ptr = NonNull::<()>::dangling(); + let zero_length = NonNull::<[()]>::from_raw_parts(dangling_ptr, 0); + } + + #[kani::proof_for_contract(NonNull::from_raw_parts)] + pub fn non_null_check_from_raw_part_trait() { + // Create a SampleTrait object from SampleStruct + let sample_struct = SampleStruct { value: kani::any() }; + let trait_object: &dyn SampleTrait = &sample_struct; + + // Get the raw data pointer and metadata for the trait object + let trait_ptr = NonNull::new(trait_object as *const dyn SampleTrait as *mut ()).unwrap(); + // Safety: For trait objects, the metadata must come from a pointer to the same underlying erased type + let metadata = core::ptr::metadata(trait_object); + + // Create NonNull from the data pointer and metadata + let nonnull_trait_object: NonNull = NonNull::from_raw_parts(trait_ptr, metadata); + + unsafe { + // Ensure trait method and member is preserved + kani::assert( trait_object.get_value() == nonnull_trait_object.as_ref().get_value(), "trait method and member must correctly preserve"); + } + } + + // pub const fn slice_from_raw_parts(data: NonNull, len: usize) -> Self + #[kani::proof_for_contract(NonNull::slice_from_raw_parts)] + #[kani::unwind(1001)] + pub fn non_null_check_slice_from_raw_parts() { + const ARR_LEN: usize = 1000; + // Create a non-deterministic array + let mut arr: [i8; ARR_LEN] = kani::any(); + // Get a raw NonNull pointer to the start of the slice + let arr_raw_ptr = NonNull::new(arr.as_mut_ptr()).unwrap(); + // Create NonNull slice from the start pointer and ends at random slice_len + // Safety: https://doc.rust-lang.org/std/slice/fn.from_raw_parts.html + let slice_len: usize = kani::any(); + kani::assume(slice_len <= ARR_LEN); + let nonnull_slice = NonNull::<[i8]>::slice_from_raw_parts(arr_raw_ptr, slice_len); + // Ensure slice content is preserved, runtime at this step is proportional to ARR_LEN + unsafe { + kani::assert(&arr[..slice_len] == nonnull_slice.as_ref(), "slice content must be preserve"); + } + + // TODO: zero-length example blocked by kani issue [#3670](https://github.com/model-checking/kani/issues/3670) + //let dangling_ptr = NonNull::<()>::dangling(); + //let zero_length = NonNull::<[()]>::slice_from_raw_parts(dangling_ptr, 0); + } + + + // pub const fn to_raw_parts(self) -> (NonNull<()>, ::Metadata) + #[kani::proof_for_contract(NonNull::to_raw_parts)] + pub fn non_null_check_to_raw_parts() { + // Create a SampleTrait object from SampleStruct + let sample_struct = SampleStruct { value: kani::any() }; + let trait_object: &dyn SampleTrait = &sample_struct; + + // Get the raw data pointer and metadata for the trait object + let trait_ptr = NonNull::from(trait_object).cast::<()>(); //both have eq failure + //let trait_ptr = NonNull::new(trait_object as *const dyn SampleTrait as *mut ()).unwrap(); //Question: what's the difference + // Safety: For trait objects, the metadata must come from a pointer to the same underlying erased type + let metadata = core::ptr::metadata(trait_object); + + // Create NonNull from the data pointer and metadata + let nonnull_trait_object: NonNull = NonNull::from_raw_parts(trait_ptr, metadata); + let (decomposed_data_ptr, decomposed_metadata) = NonNull::to_raw_parts(nonnull_trait_object); + } + + + #[kani::proof_for_contract(NonNull::as_mut)] + pub fn non_null_check_as_mut() { + let mut x: i32 = kani::any(); + if let Some(mut ptr) = NonNull::new(&mut x as *mut i32) { + unsafe { + let result = ptr.as_mut(); + } + } + } + + #[kani::proof_for_contract(NonNull::as_ref)] + pub fn non_null_check_as_ref() { + let mut x: i32 = kani::any(); + if let Some(ptr) = NonNull::new(&mut x as *mut i32) { + unsafe { + let _ = ptr.as_ref(); + } + } + } + + #[kani::proof_for_contract(NonNull::as_uninit_mut)] + pub fn non_null_check_as_uninit_mut() { + use core::mem::MaybeUninit; + + // Create an uninitialized MaybeUninit value + let mut uninit: MaybeUninit = MaybeUninit::uninit(); + let mut ptr = NonNull::new(uninit.as_mut_ptr()).unwrap(); + + unsafe { + let _ = ptr.as_uninit_mut(); + } + } + + #[kani::proof_for_contract(NonNull::as_uninit_ref)] + pub fn non_null_check_as_uninit_ref() { + use core::mem::MaybeUninit; + + // Create an uninitialized MaybeUninit value + let mut uninit: MaybeUninit = MaybeUninit::uninit(); + let ptr = NonNull::new(uninit.as_mut_ptr()).unwrap(); + + unsafe { + let uninit_ref = ptr.as_uninit_ref(); + } + } + + #[kani::proof_for_contract(NonNull::as_uninit_slice)] + pub fn non_null_check_as_uninit_slice() { + use core::mem::MaybeUninit; + + const SIZE: usize = 100000; + let arr: [MaybeUninit; SIZE] = MaybeUninit::uninit_array(); + let slice: &[MaybeUninit] = kani::slice::any_slice_of_array(&arr); + let ptr = NonNull::slice_from_raw_parts( + NonNull::new(slice.as_ptr() as *mut MaybeUninit).unwrap(), + slice.len(), + ); + + unsafe { + let _ = ptr.as_uninit_slice(); + } + } + + #[kani::proof_for_contract(NonNull::as_uninit_slice_mut)] + pub fn non_null_check_as_uninit_slice_mut() { + use core::mem::MaybeUninit; + + const SIZE: usize = 100000; + let mut arr: [MaybeUninit; SIZE] = MaybeUninit::uninit_array(); + let slice: &[MaybeUninit] = kani::slice::any_slice_of_array(&mut arr); + let ptr = NonNull::slice_from_raw_parts( + NonNull::new(slice.as_ptr() as *mut MaybeUninit).unwrap(), + SIZE, + ); + + unsafe { + let _ = ptr.as_uninit_slice_mut(); + } + } + + #[kani::proof_for_contract(NonNull::get_unchecked_mut)] + pub fn non_null_check_get_unchecked_mut() { + const ARR_SIZE: usize = 100000; + let mut arr: [i32; ARR_SIZE] = kani::any(); + let raw_ptr = arr.as_mut_ptr(); + let ptr = NonNull::slice_from_raw_parts( + NonNull::new(raw_ptr).unwrap(), + ARR_SIZE, + ); + let lower = kani::any_where(|x| *x < ARR_SIZE); + let upper = kani::any_where(|x| *x < ARR_SIZE && *x >= lower); + unsafe { + // NOTE: The `index` parameter cannot be used in the function contracts without being moved. + // Since the `SliceIndex` trait does not guarantee that `index` implements `Clone` or `Copy`, + // it cannot be reused after being consumed in the precondition. To comply with Rust's ownership + // rules and ensure `index` is only used once, the in-bounds check is moved to the proof harness + // as a workaround. + kani::assume(ptr.as_ref().get(lower..upper).is_some()); + let _ = ptr.get_unchecked_mut(lower..upper); + } + } + + #[kani::proof_for_contract(NonNull::replace)] + pub fn non_null_check_replace() { + let mut x: i32 = kani::any(); + let mut y: i32 = kani::any(); + + let origin_ptr = NonNull::new(&mut x as *mut i32).unwrap(); + unsafe { + let captured_original = ptr::read(origin_ptr.as_ptr()); + let replaced = origin_ptr.replace(y); + let after_replace = ptr::read(origin_ptr.as_ptr()); + + assert_eq!(captured_original, replaced); + assert_eq!(after_replace, y) + } + } + + #[kani::proof_for_contract(NonNull::drop_in_place)] + pub fn non_null_check_drop_in_place() { + struct Droppable { + value: i32, + } + + impl Drop for Droppable { + fn drop(&mut self) { + } + } + + let mut droppable = Droppable { value: kani::any() }; + let ptr = NonNull::new(&mut droppable as *mut Droppable).unwrap(); + unsafe { + ptr.drop_in_place(); + } + } + + #[kani::proof_for_contract(NonNull::swap)] + pub fn non_null_check_swap() { + let mut a: i32 = kani::any(); + let mut b: i32 = kani::any(); + + let ptr_a = NonNull::new(&mut a as *mut i32).unwrap(); + let ptr_b = NonNull::new(&mut b as *mut i32).unwrap(); + + unsafe { + let old_a = ptr::read(ptr_a.as_ptr()); + let old_b = ptr::read(ptr_b.as_ptr()); + ptr_a.swap(ptr_b); + // Verify that the values have been swapped. + let new_a = ptr::read(ptr_a.as_ptr()); + let new_b = ptr::read(ptr_b.as_ptr()); + assert_eq!(old_a, new_b); + assert_eq!(old_b, new_a); + } + } + + #[kani::proof] + pub fn non_null_check_len() { + // Create a non-deterministic NonNull pointer using kani::any() + let non_null_ptr: NonNull = kani::any(); + // Create a non-deterministic size using kani::any() + let size: usize = kani::any(); + // Create a NonNull slice from the non-null pointer and size + let non_null_slice: NonNull<[i8]> = NonNull::slice_from_raw_parts(non_null_ptr, size); + + // Perform the length check + let len = non_null_slice.len(); + assert!(len == size); + } + + #[kani::proof] + pub fn non_null_check_is_empty() { + // Create a non-deterministic NonNull pointer using kani::any() + let non_null_ptr: NonNull = kani::any(); + // Create a non-deterministic size using kani::any(), constrained to zero + let size: usize = 0; + + // Create a NonNull slice from the non-null pointer and size + let non_null_slice: NonNull<[i8]> = unsafe { NonNull::slice_from_raw_parts(non_null_ptr, size) }; + + // Perform the is_empty check + let is_empty = non_null_slice.is_empty(); + assert!(is_empty); + } + + #[kani::proof_for_contract(NonNull::is_aligned)] + pub fn non_null_slice_is_aligned_check() { + // Create a non-deterministic NonNull pointer using kani::any() + let non_null_ptr: NonNull = kani::any(); + + // Perform the alignment check + let result = non_null_ptr.is_aligned(); + + } + + #[kani::proof_for_contract(NonNull::is_aligned_to)] + pub fn non_null_check_is_aligned_to() { + // Create a non-deterministic NonNull pointer using kani::any() + let non_null_ptr: NonNull = kani::any(); + + // Create a non-deterministic alignment using kani::any() + let align: usize = kani::any(); + kani::assume(align > 0); // Ensure alignment is greater than zero + + // Perform the alignment check + let result = non_null_ptr.is_aligned_to(align); + + } + + #[kani::proof] + #[kani::should_panic] // Add this if we expect a panic when the alignment is invalid + pub fn non_null_check_is_aligned_to_no_power_two() { + // Create a non-deterministic NonNull pointer using kani::any() + let non_null_ptr: NonNull = kani::any(); + + // Create a non-deterministic alignment value using kani::any() + let align: usize = kani::any(); + + // Perform the alignment check + let result = non_null_ptr.is_aligned_to(align); + } + + #[kani::proof_for_contract(NonNull::sub)] + pub fn non_null_check_sub() { + const SIZE: usize = 10000; + let mut generator = kani::PointerGenerator::::new(); + // Get a raw pointer from the generator within bounds + let raw_ptr: *mut i32 = generator.any_in_bounds().ptr; + // Create a non-null pointer from the raw pointer + let ptr = unsafe { NonNull::new(raw_ptr).unwrap() }; + // Create a non-deterministic count value + let count: usize = kani::any(); + + unsafe { + let result = ptr.sub(count); + } + } + + #[kani::proof_for_contract(NonNull::sub_ptr)] + pub fn non_null_check_sub_ptr() { + const SIZE: usize = core::mem::size_of::() * 1000; + let mut generator1 = kani::PointerGenerator::::new(); + let mut generator2 = kani::PointerGenerator::::new(); + + let ptr: *mut i32 = if kani::any() { + generator1.any_in_bounds().ptr as *mut i32 + } else { + generator2.any_in_bounds().ptr as *mut i32 + }; + + let origin: *mut i32 = if kani::any() { + generator1.any_in_bounds().ptr as *mut i32 + } else { + generator2.any_in_bounds().ptr as *mut i32 + }; + + let ptr_nonnull = unsafe { NonNull::new(ptr).unwrap() }; + let origin_nonnull = unsafe { NonNull::new(origin).unwrap() }; + + unsafe { + let distance = ptr_nonnull.sub_ptr(origin_nonnull); + } + } + + #[kani::proof_for_contract(NonNull::offset_from)] + #[kani::should_panic] + pub fn non_null_check_offset_from() { + const SIZE: usize = core::mem::size_of::() * 1000; + let mut generator1 = kani::PointerGenerator::::new(); + let mut generator2 = kani::PointerGenerator::::new(); + + let ptr: *mut i32 = if kani::any() { + generator1.any_in_bounds().ptr as *mut i32 + } else { + generator2.any_in_bounds().ptr as *mut i32 + }; + + let origin: *mut i32 = if kani::any() { + generator1.any_in_bounds().ptr as *mut i32 + } else { + generator2.any_in_bounds().ptr as *mut i32 + }; + + let ptr_nonnull = unsafe { NonNull::new(ptr).unwrap() }; + let origin_nonnull = unsafe { NonNull::new(origin).unwrap() }; + + unsafe { + let distance = ptr_nonnull.offset_from(origin_nonnull); + } + } } diff --git a/library/core/src/slice/ascii.rs b/library/core/src/slice/ascii.rs index 21e0460072fb3..0862aba322e7a 100644 --- a/library/core/src/slice/ascii.rs +++ b/library/core/src/slice/ascii.rs @@ -5,6 +5,9 @@ use core::ascii::EscapeDefault; use crate::fmt::{self, Write}; use crate::{ascii, iter, mem, ops}; +#[cfg(kani)] +use crate::kani; + #[cfg(not(test))] impl [u8] { /// Checks if all bytes in this slice are within the ASCII range. @@ -398,6 +401,10 @@ const fn is_ascii(s: &[u8]) -> bool { // Read subsequent words until the last aligned word, excluding the last // aligned word by itself to be done in tail check later, to ensure that // tail is always one `usize` at most to extra branch `byte_pos == len`. + #[safety::loop_invariant(byte_pos <= len + && byte_pos >= offset_to_aligned + && word_ptr.addr() >= start.addr() + offset_to_aligned + && byte_pos == word_ptr.addr() - start.addr())] while byte_pos < len - USIZE_SIZE { // Sanity check that the read is in bounds debug_assert!(byte_pos + USIZE_SIZE <= len); @@ -432,3 +439,28 @@ const fn is_ascii(s: &[u8]) -> bool { !contains_nonascii(last_word) } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod verify { + use super::*; + + #[kani::proof] + #[kani::unwind(8)] + pub fn check_is_ascii() { + if kani::any() { + // TODO: ARR_SIZE can be much larger with cbmc argument + // `--arrays-uf-always` + const ARR_SIZE: usize = 1000; + let mut x: [u8; ARR_SIZE] = kani::any(); + let mut xs = kani::slice::any_slice_of_array_mut(&mut x); + is_ascii(xs); + } else { + let ptr = kani::any_where::(|val| *val != 0) as *const u8; + kani::assume(ptr.is_aligned()); + unsafe{ + assert_eq!(is_ascii(crate::slice::from_raw_parts(ptr, 0)), true); + } + } + } +} diff --git a/library/core/src/str/lossy.rs b/library/core/src/str/lossy.rs index e7677c8317a9f..d6786eff487f3 100644 --- a/library/core/src/str/lossy.rs +++ b/library/core/src/str/lossy.rs @@ -4,6 +4,9 @@ use crate::fmt; use crate::fmt::{Formatter, Write}; use crate::iter::FusedIterator; +#[cfg(kani)] +use crate::kani; + impl [u8] { /// Creates an iterator over the contiguous valid UTF-8 ranges of this /// slice, and the non-UTF-8 fragments in between. @@ -204,6 +207,12 @@ impl<'a> Iterator for Utf8Chunks<'a> { let mut i = 0; let mut valid_up_to = 0; + // TODO: remove `LEN` and use `self.source.len()` directly once + // fix the issue that Kani loop contracts doesn't support `self`. + // Tracked in https://github.com/model-checking/kani/issues/3700 + #[cfg(kani)] + let LEN = self.source.len(); + #[safety::loop_invariant(i <= LEN && valid_up_to == i)] while i < self.source.len() { // SAFETY: `i < self.source.len()` per previous line. // For some reason the following are both significantly slower: @@ -296,3 +305,31 @@ impl fmt::Debug for Utf8Chunks<'_> { f.debug_struct("Utf8Chunks").field("source", &self.debug()).finish() } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod verify { + use super::*; + + #[kani::proof] + pub fn check_next() { + if kani::any() { + // TODO: ARR_SIZE can be `std::usize::MAX` with cbmc argument + // `--arrays-uf-always` + const ARR_SIZE: usize = 1000; + let mut x: [u8; ARR_SIZE] = kani::any(); + let mut xs = kani::slice::any_slice_of_array_mut(&mut x); + let mut chunks = xs.utf8_chunks(); + unsafe { + chunks.next(); + } + } else { + let ptr = kani::any_where::(|val| *val != 0) as *const u8; + kani::assume(ptr.is_aligned()); + unsafe { + let mut chunks = crate::slice::from_raw_parts(ptr, 0).utf8_chunks(); + chunks.next(); + } + } + } +} diff --git a/library/core/src/str/pattern.rs b/library/core/src/str/pattern.rs index 665c9fc67d01e..f0b767ae2d4e9 100644 --- a/library/core/src/str/pattern.rs +++ b/library/core/src/str/pattern.rs @@ -43,6 +43,12 @@ use crate::convert::TryInto as _; use crate::slice::memchr; use crate::{cmp, fmt}; +#[cfg(all(target_arch = "x86_64", any(kani, target_feature = "sse2")))] +use safety::{loop_invariant, requires}; + +#[cfg(kani)] +use crate::kani; + // Pattern /// A string pattern. @@ -1905,8 +1911,9 @@ fn simd_contains(needle: &str, haystack: &str) -> Option { /// # Safety /// /// Both slices must have the same length. -#[cfg(all(target_arch = "x86_64", target_feature = "sse2"))] // only called on x86 +#[cfg(all(target_arch = "x86_64", any(kani, target_feature = "sse2")))] // only called on x86 #[inline] +#[requires(x.len() == y.len())] unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool { debug_assert_eq!(x.len(), y.len()); // This function is adapted from @@ -1951,6 +1958,11 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool { unsafe { let (mut px, mut py) = (x.as_ptr(), y.as_ptr()); let (pxend, pyend) = (px.add(x.len() - 4), py.add(y.len() - 4)); + #[loop_invariant(crate::ub_checks::same_allocation(x.as_ptr(), px) + && crate::ub_checks::same_allocation(y.as_ptr(), py) + && px.addr() >= x.as_ptr().addr() + && py.addr() >= y.as_ptr().addr() + && px.addr() - x.as_ptr().addr() == py.addr() - y.as_ptr().addr())] while px < pxend { let vx = (px as *const u32).read_unaligned(); let vy = (py as *const u32).read_unaligned(); @@ -1965,3 +1977,50 @@ unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool { vx == vy } } + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod verify { + use super::*; + + #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86 + #[kani::proof] + #[kani::unwind(4)] + pub fn check_small_slice_eq() { + // TODO: ARR_SIZE can be `std::usize::MAX` with cbmc argument + // `--arrays-uf-always` + const ARR_SIZE: usize = 1000; + let x: [u8; ARR_SIZE] = kani::any(); + let y: [u8; ARR_SIZE] = kani::any(); + let xs = kani::slice::any_slice_of_array(&x); + let ys = kani::slice::any_slice_of_array(&y); + kani::assume(xs.len() == ys.len()); + unsafe { + small_slice_eq(xs, ys); + } + } + + /* This harness check `small_slice_eq` with dangling pointer to slice + with zero size. Kani finds safety issue of `small_slice_eq` in this + harness and hence the proof will fail. + + #[cfg(all(kani, target_arch = "x86_64"))] // only called on x86 + #[kani::proof] + #[kani::unwind(4)] + pub fn check_small_slice_eq_empty() { + let ptr_x = kani::any_where::(|val| *val != 0) as *const u8; + let ptr_y = kani::any_where::(|val| *val != 0) as *const u8; + kani::assume(ptr_x.is_aligned()); + kani::assume(ptr_y.is_aligned()); + assert_eq!( + unsafe { + small_slice_eq( + crate::slice::from_raw_parts(ptr_x, 0), + crate::slice::from_raw_parts(ptr_y, 0), + ) + }, + true + ); + } + */ +} diff --git a/library/core/src/str/validations.rs b/library/core/src/str/validations.rs index cca8ff74dda8b..f1f8a83da7d7f 100644 --- a/library/core/src/str/validations.rs +++ b/library/core/src/str/validations.rs @@ -3,6 +3,9 @@ use super::Utf8Error; use crate::mem; +#[cfg(kani)] +use crate::kani; + /// Returns the initial codepoint accumulator for the first byte. /// The first byte is special, only want bottom 5 bits for width 2, 4 bits /// for width 3, and 3 bits for width 4. @@ -132,6 +135,7 @@ pub(super) const fn run_utf8_validation(v: &[u8]) -> Result<(), Utf8Error> { let blocks_end = if len >= ascii_block_size { len - ascii_block_size + 1 } else { 0 }; let align = v.as_ptr().align_offset(usize_bytes); + #[safety::loop_invariant(index <= len + ascii_block_size)] while index < len { let old_offset = index; macro_rules! err { @@ -211,6 +215,7 @@ pub(super) const fn run_utf8_validation(v: &[u8]) -> Result<(), Utf8Error> { // until we find a word containing a non-ascii byte. if align != usize::MAX && align.wrapping_sub(index) % usize_bytes == 0 { let ptr = v.as_ptr(); + #[safety::loop_invariant(index <= blocks_end + ascii_block_size && align.wrapping_sub(index) % usize_bytes == 0)] while index < blocks_end { // SAFETY: since `align - index` and `ascii_block_size` are // multiples of `usize_bytes`, `block = ptr.add(index)` is @@ -228,6 +233,7 @@ pub(super) const fn run_utf8_validation(v: &[u8]) -> Result<(), Utf8Error> { index += ascii_block_size; } // step from the point where the wordwise loop stopped + #[safety::loop_invariant(index <= len)] while index < len && v[index] < 128 { index += 1; } @@ -271,3 +277,27 @@ pub const fn utf8_char_width(b: u8) -> usize { /// Mask of the value bits of a continuation byte. const CONT_MASK: u8 = 0b0011_1111; + +#[cfg(kani)] +#[unstable(feature = "kani", issue = "none")] +pub mod verify { + use super::*; + + #[kani::proof] + pub fn check_run_utf8_validation() { + if kani::any() { + // TODO: ARR_SIZE can be much larger with cbmc argument + // `--arrays-uf-always` + const ARR_SIZE: usize = 1000; + let mut x: [u8; ARR_SIZE] = kani::any(); + let mut xs = kani::slice::any_slice_of_array_mut(&mut x); + run_utf8_validation(xs); + } else { + let ptr = kani::any_where::(|val| *val != 0) as *const u8; + kani::assume(ptr.is_aligned()); + unsafe{ + run_utf8_validation(crate::slice::from_raw_parts(ptr, 0)); + } + } + } +} diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index 8ce27dac5d207..e32bb22c23f56 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -3,10 +3,11 @@ set -e usage() { - echo "Usage: $0 [options] [-p ] [--kani-args ]" + echo "Usage: $0 [options] [-p ] [--run ] [--kani-args ]" echo "Options:" echo " -h, --help Show this help message" echo " -p, --path Optional: Specify a path to a copy of the std library. For example, if you want to run the script from an outside directory." + echo " --run Optional: Specify whether to run 'verify-std' or 'list' command. Defaults to 'verify-std' if not specified." echo " --kani-args Optional: Arguments to pass to the command. Simply pass them in the same way you would to the Kani binary. This should be the last argument." exit 1 } @@ -14,6 +15,7 @@ usage() { # Initialize variables command_args="" path="" +run_command="verify-std" # Parse command line arguments # TODO: Improve parsing with getopts @@ -31,13 +33,23 @@ while [[ $# -gt 0 ]]; do usage fi ;; + --run) + if [[ -n $2 && ($2 == "verify-std" || $2 == "list") ]]; then + run_command=$2 + shift 2 + else + echo "Error: Invalid run command. Must be 'verify-std' or 'list'." + usage + fi + ;; --kani-args) shift command_args="$@" break ;; *) - break + echo "Error: Unknown option $1" + usage ;; esac done @@ -80,15 +92,26 @@ read_commit_from_toml() { echo "$commit" } -clone_kani_repo() { +setup_kani_repo() { local repo_url="$1" local directory="$2" local branch="$3" local commit="$4" - git clone "$repo_url" "$directory" - pushd "$directory" - git checkout "$commit" - popd + + if [[ ! -d "${directory}" ]]; then + mkdir -p "${directory}" + pushd "${directory}" > /dev/null + + git init . >& /dev/null + git remote add origin "${repo_url}" >& /dev/null + else + pushd "${directory}" > /dev/null + fi + + git fetch --depth 1 origin "$commit" --quiet + git checkout "$commit" --quiet + git submodule update --init --recursive --depth 1 --quiet + popd > /dev/null } get_current_commit() { @@ -103,17 +126,22 @@ get_current_commit() { build_kani() { local directory="$1" pushd "$directory" - os_name=$(uname -s) - - if [[ "$os_name" == "Linux" ]]; then - ./scripts/setup/ubuntu/install_deps.sh - elif [[ "$os_name" == "Darwin" ]]; then - ./scripts/setup/macos/install_deps.sh + source "kani-dependencies" + # Check if installed versions are correct. + if ./scripts/check-cbmc-version.py --major ${CBMC_MAJOR} --minor ${CBMC_MINOR} && ./scripts/check_kissat_version.sh; then + echo "Dependencies are up-to-date" else - echo "Unknown operating system" + os_name=$(uname -s) + + if [[ "$os_name" == "Linux" ]]; then + ./scripts/setup/ubuntu/install_deps.sh + elif [[ "$os_name" == "Darwin" ]]; then + ./scripts/setup/macos/install_deps.sh + else + echo "Unknown operating system" + fi fi - git submodule update --init --recursive cargo build-dev --release popd } @@ -135,11 +163,15 @@ check_binary_exists() { local expected_commit="$2" local kani_path=$(get_kani_path "$build_dir") - if [[ -f "$kani_path" ]]; then + if [[ -d "${build_dir}" ]]; then local current_commit=$(get_current_commit "$build_dir") if [[ "$current_commit" = "$expected_commit" ]]; then return 0 + else + echo "Kani repository is out of date. Rebuilding..." fi + else + echo "Kani repository not found. Creating..." fi return 1 } @@ -147,7 +179,6 @@ check_binary_exists() { main() { local build_dir="$WORK_DIR/kani_build" - local temp_dir_target=$(mktemp -d) echo "Using TOML file: $TOML_FILE" echo "Using repository URL: $REPO_URL" @@ -161,12 +192,8 @@ main() { else echo "Building Kani from commit: $commit" - # Remove old build directory if it exists - rm -rf "$build_dir" - mkdir -p "$build_dir" - # Clone repository and checkout specific commit - clone_kani_repo "$REPO_URL" "$build_dir" "$BRANCH_NAME" "$commit" + setup_kani_repo "$REPO_URL" "$build_dir" "$BRANCH_NAME" "$commit" # Build project build_kani "$build_dir" @@ -181,16 +208,21 @@ main() { echo "Running Kani command..." "$kani_path" --version - echo "Running Kani verify-std command..." - - "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates --output-format=terse $command_args + if [[ "$run_command" == "verify-std" ]]; then + echo "Running Kani verify-std command..." + "$kani_path" verify-std -Z unstable-options ./library \ + -Z function-contracts \ + -Z mem-predicates \ + -Z loop-contracts \ + --output-format=terse \ + $command_args \ + --enable-unstable \ + --cbmc-args --object-bits 12 + elif [[ "$run_command" == "list" ]]; then + echo "Running Kani list command..." + "$kani_path" list -Z list -Z function-contracts -Z mem-predicates ./library --std > $path/kani_list.txt + fi } main -cleanup() -{ - rm -rf "$temp_dir_target" -} - -trap cleanup EXIT diff --git a/tool_config/kani-version.toml b/tool_config/kani-version.toml index f75f2058e67f2..10ad4876ff0f3 100644 --- a/tool_config/kani-version.toml +++ b/tool_config/kani-version.toml @@ -2,4 +2,4 @@ # incompatible with the verify-std repo. [kani] -commit = "2565ef65767a696f1d519b42621b4e502e8970d0" +commit = "26c078e097025499baf6e360210a21989d3605e0"