From 10904f03d14cef90de881d7512eaf754bd50dc9e Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 8 Nov 2024 10:54:04 -0600 Subject: [PATCH 1/3] Add loop contracts and harness for Utf8Chunk::next --- library/core/src/lib.rs | 1 + library/core/src/str/lossy.rs | 27 +++++++++++++++++++++++++++ scripts/run-kani.sh | 2 +- tool_config/kani-version.toml | 2 +- 4 files changed, 30 insertions(+), 2 deletions(-) diff --git a/library/core/src/lib.rs b/library/core/src/lib.rs index 280fda93a5494..7c0596768b784 100644 --- a/library/core/src/lib.rs +++ b/library/core/src/lib.rs @@ -230,6 +230,7 @@ #![feature(unboxed_closures)] #![feature(unsized_fn_params)] #![feature(with_negative_coherence)] +#![feature(proc_macro_hygiene)] // tidy-alphabetical-end // // Target features: diff --git a/library/core/src/str/lossy.rs b/library/core/src/str/lossy.rs index e7677c8317a9f..be040bab85276 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,11 @@ 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`. + #[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 +304,22 @@ 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() { + // 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(); + } + } +} 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 745bbaf8dfea5d532e4f92d7bd95be8330ef3784 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 8 Nov 2024 12:28:16 -0600 Subject: [PATCH 2/3] Add case of dangling pointers --- library/core/src/str/lossy.rs | 29 ++++++++++++++++++++--------- 1 file changed, 20 insertions(+), 9 deletions(-) diff --git a/library/core/src/str/lossy.rs b/library/core/src/str/lossy.rs index be040bab85276..e1ede32295962 100644 --- a/library/core/src/str/lossy.rs +++ b/library/core/src/str/lossy.rs @@ -301,7 +301,9 @@ impl FusedIterator for Utf8Chunks<'_> {} #[stable(feature = "utf8_chunks", since = "1.79.0")] impl fmt::Debug for Utf8Chunks<'_> { fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { - f.debug_struct("Utf8Chunks").field("source", &self.debug()).finish() + f.debug_struct("Utf8Chunks") + .field("source", &self.debug()) + .finish() } } @@ -312,14 +314,23 @@ pub mod verify { #[kani::proof] pub fn check_next() { - // 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(); + 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 7889a8988d76f5307d683f1781b6e918cd2091b8 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Fri, 8 Nov 2024 16:57:11 -0600 Subject: [PATCH 3/3] Address comments --- library/core/src/lib.rs | 1 + library/core/src/str/lossy.rs | 5 ++--- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/library/core/src/lib.rs b/library/core/src/lib.rs index 7c0596768b784..2c813ca0cb412 100644 --- a/library/core/src/lib.rs +++ b/library/core/src/lib.rs @@ -230,6 +230,7 @@ #![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 // diff --git a/library/core/src/str/lossy.rs b/library/core/src/str/lossy.rs index e1ede32295962..d6786eff487f3 100644 --- a/library/core/src/str/lossy.rs +++ b/library/core/src/str/lossy.rs @@ -209,6 +209,7 @@ impl<'a> Iterator for Utf8Chunks<'a> { 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)] @@ -301,9 +302,7 @@ impl FusedIterator for Utf8Chunks<'_> {} #[stable(feature = "utf8_chunks", since = "1.79.0")] impl fmt::Debug for Utf8Chunks<'_> { fn fmt(&self, f: &mut Formatter<'_>) -> fmt::Result { - f.debug_struct("Utf8Chunks") - .field("source", &self.debug()) - .finish() + f.debug_struct("Utf8Chunks").field("source", &self.debug()).finish() } }