From 0c70dcd2db594709b39b6791004229b71c9a6d85 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 8 Nov 2024 17:04:50 -0600 Subject: [PATCH 01/25] Add loop contracts and harness for `small_slice_eq` (#122) Porting from https://github.com/model-checking/kani/blob/main/tests/expected/loop-contract/small_slice_eq.rs The cbmc argument `--object-bits 8` is needed to avoid running out of memory for the harness. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Celina G. Val --- library/core/src/lib.rs | 2 ++ library/core/src/str/pattern.rs | 61 ++++++++++++++++++++++++++++++++- scripts/run-kani.sh | 2 +- tool_config/kani-version.toml | 2 +- 4 files changed, 64 insertions(+), 3 deletions(-) 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/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/scripts/run-kani.sh b/scripts/run-kani.sh index 8ce27dac5d207..1c62a05969e34 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -183,7 +183,7 @@ main() { 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 + "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" -Z function-contracts -Z mem-predicates -Z loop-contracts --output-format=terse $command_args --enable-unstable --cbmc-args --object-bits 12 } main diff --git a/tool_config/kani-version.toml b/tool_config/kani-version.toml index f75f2058e67f2..c28d156262481 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 = "8400296f5280be4f99820129bc66447e8dff63f4" From 2cd6ce043d11bce7945b44add5138684c30e8800 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 8 Nov 2024 17:53:21 -0600 Subject: [PATCH 02/25] Add loop contracts and harness for `Utf8Chunk::next` (#158) By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- library/core/src/str/lossy.rs | 37 +++++++++++++++++++++++++++++++++++ 1 file changed, 37 insertions(+) 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(); + } + } + } +} From d1600b09b3a5275cf2772f1d0f049915e90dc6ba Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 8 Nov 2024 18:01:41 -0600 Subject: [PATCH 03/25] Add loop contracts and harness for `run_utf8_validation` (#159) Co-authored-by: Celina G. Val --- library/core/src/str/validations.rs | 30 +++++++++++++++++++++++++++++ 1 file changed, 30 insertions(+) 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)); + } + } + } +} From 576fbe46fe6e3c8983c93cabc97eaba84fa82ea7 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 8 Nov 2024 18:45:04 -0600 Subject: [PATCH 04/25] Add loop contracts and harness for `slice::is_ascii` (#157) --- library/core/src/slice/ascii.rs | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) 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); + } + } + } +} From 0ed4f75298e1210100edd9a1b258b6425442bad7 Mon Sep 17 00:00:00 2001 From: Sahithi MV <49221917+SahithiMV@users.noreply.github.com> Date: Mon, 11 Nov 2024 16:26:54 +0000 Subject: [PATCH 05/25] NonZero (new_unchecked) Proof for Contract (Init) (#109) Working on #71 (Safety of NonZero) We are looking for feedback on our proof_for_contract. We have implemented it for all the data types. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: aaluna Co-authored-by: aaluna <166172412+MooniniteErr@users.noreply.github.com> Co-authored-by: Carolyn Zech Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- library/core/src/num/nonzero.rs | 58 ++++++++++++++++++++++++++++++++- 1 file changed, 57 insertions(+), 1 deletion(-) 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); +} From 6aa2661e20a7edd7fd8fed5051425a43173a54ba Mon Sep 17 00:00:00 2001 From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> Date: Tue, 12 Nov 2024 11:15:21 -0800 Subject: [PATCH 06/25] Update Kani version (#160) Update to the version where the CBMC viewer is removed. This should resolve the issues some people are having with the `run_kani.sh` script. --- tool_config/kani-version.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tool_config/kani-version.toml b/tool_config/kani-version.toml index c28d156262481..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 = "8400296f5280be4f99820129bc66447e8dff63f4" +commit = "26c078e097025499baf6e360210a21989d3605e0" From 90d304b4df72a8cfaa4fbd075e41f1b6160fe0d3 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 13 Nov 2024 11:09:34 -0800 Subject: [PATCH 07/25] Add a new challenge to verify `CStr` (#151) Proposes a new challenge to verify the safety of `CStr` implementation. --------- Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- doc/src/SUMMARY.md | 2 +- doc/src/challenges/0013-cstr.md | 85 +++++++++++++++++++++++++++++++++ doc/src/tool_template.md | 6 +-- 3 files changed, 89 insertions(+), 4 deletions(-) create mode 100644 doc/src/challenges/0013-cstr.md 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/challenges/0013-cstr.md b/doc/src/challenges/0013-cstr.md new file mode 100644 index 0000000000000..ff6048701e50f --- /dev/null +++ b/doc/src/challenges/0013-cstr.md @@ -0,0 +1,85 @@ +# 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/01/31 + +------------------- +## 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/tool_template.md b/doc/src/tool_template.md index 474b1d089c6ee..5e7b054ed6891 100644 --- a/doc/src/tool_template.md +++ b/doc/src/tool_template.md @@ -20,9 +20,9 @@ _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._ From 83e04a0d08638c74f6e8c72d1db20406c41a8372 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Thu, 14 Nov 2024 08:37:22 -0600 Subject: [PATCH 08/25] Update pull_requests.toml (#164) @robdockins and @HuStmpHrrr will help to review PRs of adding contracts and proof harnesses. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .github/pull_requests.toml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/pull_requests.toml b/.github/pull_requests.toml index 45a38b3cc2307..7c50848653fef 100644 --- a/.github/pull_requests.toml +++ b/.github/pull_requests.toml @@ -12,5 +12,7 @@ members = [ "jaisnan", "patricklam", "ranjitjhala", - "carolynzech" + "carolynzech", + "robdockins", + "HuStmpHrrr" ] From d29f29e2770a033cf13cdb4ff43ed8a4ad56270f Mon Sep 17 00:00:00 2001 From: Qinyuan Wu <53478459+QinyuanWu@users.noreply.github.com> Date: Thu, 14 Nov 2024 06:52:47 -0800 Subject: [PATCH 09/25] Contracts & Harnesses for `add`, `addr`, and `align_offset` (#105) Towards https://github.com/model-checking/verify-rust-std/issues/53 ## Changes Three function contracts & four harnesses: - added contract and harness for `non_null::add` - added contract and harness for `non_null::addr` - added contract and harnesses for `non_null::align_offset`, including both positive and negative harness that triggers panic. The ensures clause for `align_offset` is referenced from [`align_offset`](https://github.com/model-checking/verify-rust-std/pull/69/files) in `library/core/src/ptr/mod.rs`. ## 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 all six harnesses in the module. All default checks should pass: ``` SUMMARY: ** 0 of 1556 failed VERIFICATION:- SUCCESSFUL Verification Time: 0.28004378s Complete - 6 successfully verified harnesses, 0 failures, 6 total. ``` ### :exclamation: Warning Running the above command with the default installed cargo kani will result in compilation error due to the latest merged from [PR#91](https://github.com/model-checking/verify-rust-std/pull/91). Detailed errors are commented under that PR. This issue is waiting to be resolved. ## TODO: - Use `Layout` to create dynamically sized arrays in place of fixed size array in harnesses. This approach currently has errors and is documented in [discussion](https://github.com/model-checking/verify-rust-std/discussions/104). - Verify multiple data types: these will be added in future PR. - Add `requires` clause in contract to constrain `count` to be within object memory size: there is a current [issue](https://github.com/model-checking/verify-rust-std/discussions/99) with using `ub_checks::can_write` to get the object size. A workaround is implemented in the harness. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Carolyn Zech --- library/core/src/ptr/non_null.rs | 91 +++++++++++++++++++++++++++++++- 1 file changed, 90 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 0aa306f803a70..b805c8e3b55ac 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -294,6 +294,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. @@ -567,6 +568,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, @@ -1208,6 +1214,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, @@ -1811,6 +1847,7 @@ impl From<&T> for NonNull { mod verify { use super::*; use crate::ptr::null_mut; + use kani::PointerGenerator; // pub const unsafe fn new_unchecked(ptr: *mut T) -> Self #[kani::proof_for_contract(NonNull::new_unchecked)] @@ -1821,7 +1858,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 +1866,56 @@ 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 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); + } } From 20d5a0bb9438b23ac6f3abd2f9c529c55e3deee1 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Thu, 14 Nov 2024 16:51:39 -0500 Subject: [PATCH 10/25] add @Eh2406 to reviewers list (#165) By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .github/pull_requests.toml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/pull_requests.toml b/.github/pull_requests.toml index 7c50848653fef..d5d88e0b9fca5 100644 --- a/.github/pull_requests.toml +++ b/.github/pull_requests.toml @@ -14,5 +14,6 @@ members = [ "ranjitjhala", "carolynzech", "robdockins", - "HuStmpHrrr" + "HuStmpHrrr", + "Eh2406" ] From 94a31f58f106328f17457bbcbc9f4023c6ee7164 Mon Sep 17 00:00:00 2001 From: Qinyuan Wu <53478459+QinyuanWu@users.noreply.github.com> Date: Fri, 15 Nov 2024 07:40:16 -0800 Subject: [PATCH 11/25] Contracts & Harnesses for `NonNull::read`, `NonNull::read_volatile`, `NonNull::read_unaligned` (#156) Towards #52 Contracts & Harnesses for `NonNull::read`, `NonNull::read_volatile`, `NonNull::read_unaligned` ### Discussion For the ensures clause in the contract for `NonNull::read`, I could not directly compare the value pointed by self and result due to unsized and lack of PartialEq implementation, and the comparison is currently moved to the harness. ### Verification Successful verification: ``` SUMMARY: ** 0 of 141 failed VERIFICATION:- SUCCESSFUL Verification Time: 0.1760525s Complete - 5 successfully verified harnesses, 0 failures, 5 total. ``` By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Zyad Hassan --- library/core/src/ptr/non_null.rs | 98 ++++++++++++++++++++++++++++---- 1 file changed, 88 insertions(+), 10 deletions(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index b805c8e3b55ac..0a087298893ae 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -13,6 +13,8 @@ use safety::{ensures, requires}; #[cfg(kani)] use crate::kani; +#[cfg(kani)] +use crate::ub_checks; /// `*mut T` but non-zero and [covariant]. /// @@ -568,7 +570,7 @@ 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() + #[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)))] @@ -910,6 +912,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, @@ -931,6 +934,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, @@ -951,6 +955,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, @@ -1219,9 +1224,9 @@ impl NonNull { let stride = crate::mem::size_of::(); // ZSTs if stride == 0 { - if self.pointer.addr() % align == 0 { + if self.pointer.addr() % align == 0 { return *result == 0; - } else { + } else { return *result == usize::MAX; } } @@ -1233,8 +1238,8 @@ impl NonNull { // 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 (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 @@ -1867,6 +1872,79 @@ mod verify { 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() { @@ -1875,8 +1953,8 @@ mod verify { 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(); - + let count: usize = kani::any(); + unsafe { let result = ptr.add(count); } @@ -1884,7 +1962,7 @@ mod verify { // pub fn addr(self) -> NonZero #[kani::proof_for_contract(NonNull::addr)] - pub fn non_null_check_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; }; @@ -1897,7 +1975,7 @@ mod verify { // 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()); @@ -1914,7 +1992,7 @@ mod verify { // 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); } From 922c51a1ee43668342c8bb9ececac366e513354b Mon Sep 17 00:00:00 2001 From: Daniel Tu <135958699+danielhumanmod@users.noreply.github.com> Date: Fri, 15 Nov 2024 11:45:05 -0800 Subject: [PATCH 12/25] Contracts & Harnesses for Reference Conversion APIs at std::NonNull (#116) Description: This PR introduces function contracts and proof harness for the NonNull pointer in the Rust core library. Specifically, it verifies reference conversion APIs, covering: - NonNull::as_mut<'a> - NonNull::as_ref<'a> - NonNull::as_uninit_mut<'a> - NonNull::as_uninit_ref<'a> - NonNull::as_uninit_slice<'a> - NonNull::as_uninit_slice_mut<'a> - NonNull::get_unchecked_mut Proof harness: - non_null_check_as_mut - non_null_check_as_ref - non_null_check_as_uninit_mut - non_null_check_as_as_uninit_ref - non_null_check_as_as_uninit_slice - non_null_check_as_uninit_slice_mut - non_null_check_as_get_unchecked_mut Towards https://github.com/model-checking/verify-rust-std/issues/53 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- library/core/src/ptr/non_null.rs | 124 ++++++++++++++++++++++++++++++- 1 file changed, 123 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 0a087298893ae..e6f5bff9eca60 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -139,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. @@ -163,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. @@ -386,6 +390,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. @@ -424,6 +430,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. @@ -1642,6 +1651,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()) } @@ -1707,6 +1721,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()) } @@ -1735,6 +1754,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]>, @@ -1871,7 +1891,7 @@ 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() { @@ -1996,4 +2016,106 @@ mod verify { // Trigger panic let offset = nonnull_xptr.align_offset(invalid_align); } + + #[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); + } + } } From 4db111ff2649581be7c304b24736ac4b0dbe1e95 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Tue, 19 Nov 2024 23:31:37 -0500 Subject: [PATCH 13/25] `kani list` Workflow (#146) Adds a workflow that runs `kani list` on the standard library and posts the results in a comment on the pull request. This workflow runs iff a pull request is merged, so that we have one comment at the end of a PR with the most up-to-date list results. (I considered other approaches, like running it on opening the PR or with every commit, but decided having one single comment with the final changes was best for brevity/clarity). See this [test PR](https://github.com/carolynzech/verify-rust-std/pull/10) on my fork as a demo of how it would work. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Celina G. Val --- .github/workflows/kani.yml | 14 ++++++++++++++ scripts/run-kani.sh | 33 ++++++++++++++++++++++++++++----- 2 files changed, 42 insertions(+), 5 deletions(-) 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/scripts/run-kani.sh b/scripts/run-kani.sh index 1c62a05969e34..e8f0dc42193d6 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 @@ -181,9 +193,20 @@ 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 -Z loop-contracts --output-format=terse $command_args --enable-unstable --cbmc-args --object-bits 12 + if [[ "$run_command" == "verify-std" ]]; then + 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 \ + -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 From 8f5512db864f3c568766b7f5b90d83a31320445c Mon Sep 17 00:00:00 2001 From: Daniel Tu <135958699+danielhumanmod@users.noreply.github.com> Date: Wed, 20 Nov 2024 09:15:54 -0800 Subject: [PATCH 14/25] Contracts & Harnesses for `swap`, `replace`, and `drop_in_place` (#144) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit # Description This PR introduces function contracts and proof harness for the NonNull pointer in the Rust core library. Specifically, it verifies three new APIs—`swap`, `replace`, and `drop_in_place` with Kani. These changes enhance the functionality of memory operations for NonNull pointers. # Change Overview Covered APIs: 1. NonNull::swap: Swaps the values at two mutable locations of the same type 2. NonNull::replace: Replaces the pointer's value, returning the old value 3. NonNull::drop_in_place: Executes the destructor (if any) of the pointed-to value Resolves #53 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- library/core/src/ptr/non_null.rs | 63 +++++++++++++++++++++++++++++++- 1 file changed, 62 insertions(+), 1 deletion(-) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index e6f5bff9eca60..4834c8009ec44 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -10,7 +10,6 @@ use crate::ub_checks::assert_unsafe_precondition; use crate::{fmt, hash, intrinsics, ptr}; use safety::{ensures, requires}; - #[cfg(kani)] use crate::kani; #[cfg(kani)] @@ -1060,6 +1059,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()) } @@ -1151,6 +1152,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, @@ -1169,6 +1173,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, @@ -2118,4 +2125,58 @@ mod verify { 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); + } + } } From 971befd78b5e59456280724e8c67bf1a3b43c42b Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 20 Nov 2024 11:43:45 -0800 Subject: [PATCH 15/25] Improve run-kani script to use default target (#172) Use default target folder instead of using a temporary folder. Users are still able to customize the folder using Kani argument. Avoid needless updates when Kani dependencies are already up-to-date. Fixes #170 --- scripts/run-kani.sh | 63 ++++++++++++++++++++++++++------------------- 1 file changed, 36 insertions(+), 27 deletions(-) diff --git a/scripts/run-kani.sh b/scripts/run-kani.sh index e8f0dc42193d6..e32bb22c23f56 100755 --- a/scripts/run-kani.sh +++ b/scripts/run-kani.sh @@ -92,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() { @@ -115,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 } @@ -147,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 } @@ -159,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" @@ -173,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" @@ -195,7 +210,7 @@ main() { if [[ "$run_command" == "verify-std" ]]; then echo "Running Kani verify-std command..." - "$kani_path" verify-std -Z unstable-options ./library --target-dir "$temp_dir_target" \ + "$kani_path" verify-std -Z unstable-options ./library \ -Z function-contracts \ -Z mem-predicates \ -Z loop-contracts \ @@ -211,9 +226,3 @@ main() { main -cleanup() -{ - rm -rf "$temp_dir_target" -} - -trap cleanup EXIT From a8dd9753fb7d02f9e023083bb5642f804dcb671b Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Wed, 20 Nov 2024 15:02:19 -0500 Subject: [PATCH 16/25] Add @jswrenn to reviewers list (#175) By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .github/pull_requests.toml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/.github/pull_requests.toml b/.github/pull_requests.toml index d5d88e0b9fca5..a83cebe76609e 100644 --- a/.github/pull_requests.toml +++ b/.github/pull_requests.toml @@ -15,5 +15,6 @@ members = [ "carolynzech", "robdockins", "HuStmpHrrr", - "Eh2406" + "Eh2406", + "jswrenn" ] From 406b1c196a08c69444351721a41bc73922f48c9b Mon Sep 17 00:00:00 2001 From: Bhuwan Pandit Date: Fri, 22 Nov 2024 15:27:06 +0000 Subject: [PATCH 17/25] docs(0005): typo fix in the challenge docs (#178) This PR, just fixes a typo for a function name in the challenge docs. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- doc/src/challenges/0005-linked-list.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/challenges/0005-linked-list.md b/doc/src/challenges/0005-linked-list.md index a5c931712025a..0215bbd029714 100644 --- a/doc/src/challenges/0005-linked-list.md +++ b/doc/src/challenges/0005-linked-list.md @@ -23,7 +23,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 | From e2db4357df2f596d0fe96b0ba3c9afc01c7a67f7 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 22 Nov 2024 10:21:46 -0800 Subject: [PATCH 18/25] Add reward information to the repository and challenges (#176) I also postponed the end date of all challenges, and fixed the date format. Co-authored-by: Felipe R. Monteiro --- README.md | 19 +++++++++---------- doc/src/challenge_template.md | 6 ++++-- doc/src/challenges/0001-core-transmutation.md | 5 +++-- doc/src/challenges/0002-intrinsics-memory.md | 5 +++-- .../challenges/0003-pointer-arithmentic.md | 6 +++--- doc/src/challenges/0004-btree-node.md | 5 +++-- doc/src/challenges/0005-linked-list.md | 5 +++-- doc/src/challenges/0006-nonnull.md | 5 +++-- doc/src/challenges/0007-atomic-types.md | 5 +++-- doc/src/challenges/0008-smallsort.md | 5 +++-- doc/src/challenges/0009-duration.md | 5 +++-- doc/src/challenges/0010-string.md | 5 +++-- doc/src/challenges/0011-floats-ints.md | 5 +++-- doc/src/challenges/0012-nonzero.md | 5 +++-- doc/src/challenges/0013-cstr.md | 5 +++-- doc/src/intro.md | 14 ++++++++++++-- 16 files changed, 64 insertions(+), 41 deletions(-) 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/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 0215bbd029714..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* ------------------- 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 index ff6048701e50f..bb0a20808ebd2 100644 --- a/doc/src/challenges/0013-cstr.md +++ b/doc/src/challenges/0013-cstr.md @@ -3,8 +3,9 @@ - **Status:** Open - **Solution:** - **Tracking Issue:** [#150](https://github.com/model-checking/verify-rust-std/issues/150) -- **Start date:** 2024/11/04 -- **End date:** 2025/01/31 +- **Start date:** *2024/11/04* +- **End date:** *2025/04/10* +- **Reward:** *N/A* ------------------- ## Goal 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 From 4c86400ea7d9f606c7f1da1e0943f16d1542a635 Mon Sep 17 00:00:00 2001 From: stogaru <143449212+stogaru@users.noreply.github.com> Date: Fri, 22 Nov 2024 12:23:43 -0800 Subject: [PATCH 19/25] Contract and Harnesses for `<*const T>::offset_from` (#154) Towards #76 ### Changes * Adds contracts for `<*const T>::offset_from`. * Adds harnesses for the function verifying: * All integer types * Tuples (composite types) * Unit Type * Accomplishes this using a macro. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Carolyn Zech --- library/core/src/ptr/const_ptr.rs | 160 ++++++++++++++++++++++++++++++ 1 file changed, 160 insertions(+) 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 + ); +} From b81906d2bb53c5a8c2a78ec6b1e8c99ac6177a33 Mon Sep 17 00:00:00 2001 From: Eli Gancena Date: Sat, 23 Nov 2024 17:17:22 -0400 Subject: [PATCH 20/25] Update tool_template.md (#183) Typo pr fixes typo found in verification tool template Resolves #NA By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- doc/src/tool_template.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/doc/src/tool_template.md b/doc/src/tool_template.md index 5e7b054ed6891..c5d56b97b80d5 100644 --- a/doc/src/tool_template.md +++ b/doc/src/tool_template.md @@ -25,7 +25,7 @@ _Please list the license(s) that are used by your tool, and if to your knowledge 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._ From 5e44e6e86a021633d20b610ea76574a11a7e95e7 Mon Sep 17 00:00:00 2001 From: JY <53210261+Jimmycreative@users.noreply.github.com> Date: Mon, 25 Nov 2024 08:56:41 -0800 Subject: [PATCH 21/25] Contracts & Harnesses for len, is_empty, is_aligned, and is_aligned_to (#128) Changes added contract and harness for len, is_empty, is_aligned, and is_aligned_to in the non-null library. ``` Complete - 4 successfully verified harnesses, 0 failures, 4 total. ``` --------- Co-authored-by: Carolyn Zech --- library/core/src/ptr/non_null.rs | 77 ++++++++++++++++++++++++++++++++ 1 file changed, 77 insertions(+) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 4834c8009ec44..aa224db211933 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -1387,6 +1387,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, @@ -1502,6 +1503,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) } @@ -1881,6 +1884,14 @@ mod verify { use crate::ptr::null_mut; use kani::PointerGenerator; + 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)] pub fn non_null_check_new_unchecked() { @@ -2179,4 +2190,70 @@ mod verify { 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); + } } From 07318dfc34aba23b0e04793cdcd9414629f2b774 Mon Sep 17 00:00:00 2001 From: Qinyuan Wu <53478459+QinyuanWu@users.noreply.github.com> Date: Mon, 25 Nov 2024 14:18:26 -0800 Subject: [PATCH 22/25] Contracts and harnesses for `dangling`, `from_raw_parts`, `slice_from_raw_parts`, `to_raw_parts` in NonNull (#127) Towards #53 Contracts and harnesses for `dangling`, `from_raw_parts`, `slice_from_raw_parts`, `to_raw_parts` in NonNull ### Discussion 1. `NonNull::slice_from_raw_parts`: [requested](https://github.com/model-checking/kani/issues/3693) new Kani API to compare byte by byte 2. `NonNull::to_raw_parts`: [unstable vtable comparison 'Eq'](https://github.com/model-checking/verify-rust-std/discussions/139) ### Verification Result ``` SUMMARY: ** 0 of 141 failed VERIFICATION:- SUCCESSFUL Verification Time: 0.17378491s Complete - 6 successfully verified harnesses, 0 failures, 6 total. ``` By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- library/core/src/ptr/non_null.rs | 130 +++++++++++++++++++++++++++++++ 1 file changed, 130 insertions(+) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index aa224db211933..915473ee027f0 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -112,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 { @@ -269,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, @@ -287,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())) } @@ -1536,6 +1540,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)) } @@ -1884,6 +1891,20 @@ mod verify { 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; @@ -2035,6 +2056,115 @@ mod verify { 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(); From 82da845a15dbffa36dc08f755cc0d0b4d5212b0f Mon Sep 17 00:00:00 2001 From: Yenyun035 <57857379+Yenyun035@users.noreply.github.com> Date: Mon, 25 Nov 2024 17:46:39 -0800 Subject: [PATCH 23/25] CStr Safety invariant & Harnesses for `from_bytes_until_nul` (#180) Towards #150 ### Changes * Added a `CStr` Safety Invariant * Added a harness for `from_bytes_until_nul`, the harness covers: * The input slice contains a single null byte at the end; * The input slice contains no null bytes; * The input slice contains intermediate null bytes ### Discussion * [Safety invariant implementation](https://github.com/model-checking/verify-rust-std/issues/150#issuecomment-2492853570) * [Input array generation](https://github.com/model-checking/verify-rust-std/discussions/181) ### Verification Result `./scripts/run-kani.sh --kani-args --harness ffi::c_str::verify` ``` // array size 16 Checking harness ffi::c_str::verify::check_from_bytes_until_nul... VERIFICATION RESULT: ** 0 of 140 failed (5 unreachable) VERIFICATION:- SUCCESSFUL Verification Time: 7.3023376s Complete - 1 successfully verified harnesses, 0 failures, 1 total. ``` By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- library/core/src/ffi/c_str.rs | 43 +++++++++++++++++++++++++++++++++++ 1 file changed, 43 insertions(+) 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 From 688b15bfa092fe3f56c8b71596845192a41469a9 Mon Sep 17 00:00:00 2001 From: JY <53210261+Jimmycreative@users.noreply.github.com> Date: Tue, 26 Nov 2024 20:30:26 -0800 Subject: [PATCH 24/25] Contracts & Harnesses for `non_null::sub` and `non_null::sub_ptr` and `non_null::offset_from` (#93) Towards https://github.com/model-checking/verify-rust-std/issues/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. ``` ### 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? --------- Co-authored-by: OwO Co-authored-by: Qinyuan Wu Co-authored-by: Carolyn Zech Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- library/core/src/ptr/non_null.rs | 87 ++++++++++++++++++++++++++++++++ 1 file changed, 87 insertions(+) diff --git a/library/core/src/ptr/non_null.rs b/library/core/src/ptr/non_null.rs index 915473ee027f0..42ea9d75896d3 100644 --- a/library/core/src/ptr/non_null.rs +++ b/library/core/src/ptr/non_null.rs @@ -665,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, @@ -794,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, @@ -887,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, @@ -2386,4 +2404,73 @@ mod verify { // 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); + } + } } From 716c6af923e1d2daf14aa437483a30af772c9afa Mon Sep 17 00:00:00 2001 From: rahulku Date: Wed, 27 Nov 2024 09:27:12 -0800 Subject: [PATCH 25/25] Add two more reviewers (#190) Add two more reviewers to our list. By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --- .github/pull_requests.toml | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/.github/pull_requests.toml b/.github/pull_requests.toml index a83cebe76609e..6c11ebfeb3691 100644 --- a/.github/pull_requests.toml +++ b/.github/pull_requests.toml @@ -16,5 +16,7 @@ members = [ "robdockins", "HuStmpHrrr", "Eh2406", - "jswrenn" + "jswrenn", + "havelund", + "jorajeev" ]