From e46c47c873a9fd24f621734ac12a024ca8d41345 Mon Sep 17 00:00:00 2001 From: Qinheping Hu Date: Tue, 9 Jul 2024 12:56:16 -0500 Subject: [PATCH] Add initial tests for std function with loops --- .../loop-contracts/slice/Cargo.toml | 13 ++++ .../loop-contracts/slice/equal.expected | 1 + .../slice/memchr_naive.expected | 1 + .../loop-contracts/slice/memchr_naive.rs | 0 .../slice/partition_dedup_by.expected | 1 + .../loop-contracts/slice/repeat.expected | 1 + .../loop-contracts/slice/src/equal.rs | 25 ++++++++ .../loop-contracts/slice/src/memchr_naive.rs | 31 ++++++++++ .../slice/src/partition_dedup_by.rs | 45 ++++++++++++++ .../loop-contracts/slice/src/repeat.rs | 61 +++++++++++++++++++ .../std-checks/loop-contracts/str/Cargo.toml | 13 ++++ .../str/small_slice_eq.expected | 1 + .../loop-contracts/str/src/small_slice_eq.rs | 49 +++++++++++++++ 13 files changed, 242 insertions(+) create mode 100644 tests/std-checks/loop-contracts/slice/Cargo.toml create mode 100644 tests/std-checks/loop-contracts/slice/equal.expected create mode 100644 tests/std-checks/loop-contracts/slice/memchr_naive.expected create mode 100644 tests/std-checks/loop-contracts/slice/memchr_naive.rs create mode 100644 tests/std-checks/loop-contracts/slice/partition_dedup_by.expected create mode 100644 tests/std-checks/loop-contracts/slice/repeat.expected create mode 100644 tests/std-checks/loop-contracts/slice/src/equal.rs create mode 100644 tests/std-checks/loop-contracts/slice/src/memchr_naive.rs create mode 100644 tests/std-checks/loop-contracts/slice/src/partition_dedup_by.rs create mode 100644 tests/std-checks/loop-contracts/slice/src/repeat.rs create mode 100644 tests/std-checks/loop-contracts/str/Cargo.toml create mode 100644 tests/std-checks/loop-contracts/str/small_slice_eq.expected create mode 100644 tests/std-checks/loop-contracts/str/src/small_slice_eq.rs diff --git a/tests/std-checks/loop-contracts/slice/Cargo.toml b/tests/std-checks/loop-contracts/slice/Cargo.toml new file mode 100644 index 000000000000..39538e2ff57d --- /dev/null +++ b/tests/std-checks/loop-contracts/slice/Cargo.toml @@ -0,0 +1,13 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "verify-loop-contracts-core-slice" +version = "0.1.0" +edition = "2021" +description = "This crate contains loop contracts and harnesses for core library" + +[package.metadata.kani] +unstable = { } + +[package.metadata.kani.flags] +output-format = "terse" diff --git a/tests/std-checks/loop-contracts/slice/equal.expected b/tests/std-checks/loop-contracts/slice/equal.expected new file mode 100644 index 000000000000..01a90d50b557 --- /dev/null +++ b/tests/std-checks/loop-contracts/slice/equal.expected @@ -0,0 +1 @@ +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/std-checks/loop-contracts/slice/memchr_naive.expected b/tests/std-checks/loop-contracts/slice/memchr_naive.expected new file mode 100644 index 000000000000..01a90d50b557 --- /dev/null +++ b/tests/std-checks/loop-contracts/slice/memchr_naive.expected @@ -0,0 +1 @@ +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/std-checks/loop-contracts/slice/memchr_naive.rs b/tests/std-checks/loop-contracts/slice/memchr_naive.rs new file mode 100644 index 000000000000..e69de29bb2d1 diff --git a/tests/std-checks/loop-contracts/slice/partition_dedup_by.expected b/tests/std-checks/loop-contracts/slice/partition_dedup_by.expected new file mode 100644 index 000000000000..01a90d50b557 --- /dev/null +++ b/tests/std-checks/loop-contracts/slice/partition_dedup_by.expected @@ -0,0 +1 @@ +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/std-checks/loop-contracts/slice/repeat.expected b/tests/std-checks/loop-contracts/slice/repeat.expected new file mode 100644 index 000000000000..01a90d50b557 --- /dev/null +++ b/tests/std-checks/loop-contracts/slice/repeat.expected @@ -0,0 +1 @@ +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/std-checks/loop-contracts/slice/src/equal.rs b/tests/std-checks/loop-contracts/slice/src/equal.rs new file mode 100644 index 000000000000..5d134e57d7c1 --- /dev/null +++ b/tests/std-checks/loop-contracts/slice/src/equal.rs @@ -0,0 +1,25 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! https://github.com/rust-lang/rust/blob/7c4ac0603e9ee5295bc802c90575391288a69a8a/library/core/src/slice/cmp.rs#L58 + +fn equal(s: &[u16], other: &[u16]) -> bool { + if s.len() != other.len() { + return false; + } + + for idx in 0..s.len() { + if s[idx] != other[idx] { + return false; + } + } + + true +} + +#[kani::proof] +fn main() { + let mut a = [1; 20]; + let mut b = [1; 20]; + assert!(equal(&a, &b)); +} diff --git a/tests/std-checks/loop-contracts/slice/src/memchr_naive.rs b/tests/std-checks/loop-contracts/slice/src/memchr_naive.rs new file mode 100644 index 000000000000..1c978becf03f --- /dev/null +++ b/tests/std-checks/loop-contracts/slice/src/memchr_naive.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! https://github.com/rust-lang/rust/blob/7c4ac0603e9ee5295bc802c90575391288a69a8a/library/core/src/slice/memchr.rs#L38C10-L38C22 + +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] + +const fn memchr_naive(x: u8, text: &[u8]) -> Option { + let mut i = 0; + + // #[kani::loop_invariant(i <= text.len() && ((i == 0) || text[i-1]!= x))] + while i < text.len() { + if text[i] == x { + return Some(i); + } + + i += 1; + } + + None +} + +#[kani::proof] +fn main() { + let mut text = [1; 20]; + text[4] = 5; + let x = 5; + + assert_eq!(memchr_naive(x, &text), Some(4)); +} diff --git a/tests/std-checks/loop-contracts/slice/src/partition_dedup_by.rs b/tests/std-checks/loop-contracts/slice/src/partition_dedup_by.rs new file mode 100644 index 000000000000..0c7eb375eb38 --- /dev/null +++ b/tests/std-checks/loop-contracts/slice/src/partition_dedup_by.rs @@ -0,0 +1,45 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! https://doc.rust-lang.org/src/core/slice/mod.rs.html#3244-3346 + +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] +#![feature(ptr_sub_ptr)] + +use std::ptr; +use std::mem; +pub fn partition_dedup_by(slice: &mut [u16]) { + let len = slice.len(); + if len <= 1 { + return; + } + + let ptr = slice.as_mut_ptr(); + let mut next_read: usize = 1; + let mut next_write: usize = 1; + unsafe { + // #[kani::loop_invariant(next_read <= len && next_read >= next_write && next_write >= 1)] + while next_read < len { + let ptr_read = ptr.add(next_read); + let prev_ptr_write = ptr.add(next_write - 1); + if *ptr_read != *prev_ptr_write { + if next_read != next_write { + let ptr_write = prev_ptr_write.add(1); + mem::swap(&mut *ptr_read, &mut *ptr_write); + } + next_write += 1; + } + next_read += 1; + }; + } +} + +#[kani::proof] +#[kani::solver(kissat)] +fn main() { + let mut a = [1; 20]; + unsafe { + partition_dedup_by(&mut a); + } +} diff --git a/tests/std-checks/loop-contracts/slice/src/repeat.rs b/tests/std-checks/loop-contracts/slice/src/repeat.rs new file mode 100644 index 000000000000..6a1cd03b9c3d --- /dev/null +++ b/tests/std-checks/loop-contracts/slice/src/repeat.rs @@ -0,0 +1,61 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! https://doc.rust-lang.org/src/alloc/slice.rs.html#489 + +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] +#![feature(ptr_sub_ptr)] + +use std::ptr; +pub fn repeat(slice: &[u16], n: usize) -> Vec +{ + if n == 0 { + return Vec::new(); + } + + let capacity = slice.len().checked_mul(n).expect("capacity overflow"); + let mut buf = Vec::with_capacity(capacity); + + buf.extend(slice); + { + let mut m = n >> 1; + // #[kani::loop_invariant(1 == 1)] + while m > 0 { + unsafe { + ptr::copy_nonoverlapping( + buf.as_ptr(), + (buf.as_mut_ptr() as *mut u16).add(buf.len()), + buf.len(), + ); + let buf_len = buf.len(); + buf.set_len(buf_len * 2); + } + + m >>= 1; + }; + } + + let rem_len = capacity - buf.len(); + if rem_len > 0 { + unsafe { + ptr::copy_nonoverlapping( + buf.as_ptr(), + (buf.as_mut_ptr() as *mut u16).add(buf.len()), + rem_len, + ); + buf.set_len(capacity); + } + } + buf +} + +#[kani::proof] +#[kani::solver(kissat)] +fn main() { + let mut a = [1; 20]; + let n: usize = 30; + unsafe { + repeat(&mut a, n); + } +} diff --git a/tests/std-checks/loop-contracts/str/Cargo.toml b/tests/std-checks/loop-contracts/str/Cargo.toml new file mode 100644 index 000000000000..347603a3e2cf --- /dev/null +++ b/tests/std-checks/loop-contracts/str/Cargo.toml @@ -0,0 +1,13 @@ +# Copyright Kani Contributors +# SPDX-License-Identifier: Apache-2.0 OR MIT +[package] +name = "verify-loop-contracts-core-str" +version = "0.1.0" +edition = "2021" +description = "This crate contains loop contracts and harnesses for core library" + +[package.metadata.kani] +unstable = { } + +[package.metadata.kani.flags] +output-format = "terse" diff --git a/tests/std-checks/loop-contracts/str/small_slice_eq.expected b/tests/std-checks/loop-contracts/str/small_slice_eq.expected new file mode 100644 index 000000000000..01a90d50b557 --- /dev/null +++ b/tests/std-checks/loop-contracts/str/small_slice_eq.expected @@ -0,0 +1 @@ +Complete - 1 successfully verified harnesses, 0 failures, 1 total. diff --git a/tests/std-checks/loop-contracts/str/src/small_slice_eq.rs b/tests/std-checks/loop-contracts/str/src/small_slice_eq.rs new file mode 100644 index 000000000000..aeb1f3e1841e --- /dev/null +++ b/tests/std-checks/loop-contracts/str/src/small_slice_eq.rs @@ -0,0 +1,49 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! https://github.com/rust-lang/rust/blob/7c4ac0603e9ee5295bc802c90575391288a69a8a/library/core/src/str/pattern.rs#L1881 + +#![feature(stmt_expr_attributes)] +#![feature(proc_macro_hygiene)] +#![feature(ptr_sub_ptr)] +unsafe fn small_slice_eq(x: &[u8], y: &[u8]) -> bool { + debug_assert_eq!(x.len(), y.len()); + + if x.len() < 4 { + for (&b1, &b2) in x.iter().zip(y) { + if b1 != b2 { + return false; + } + } + return true; + } + + 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)); + // #[kani::loop_invariant( px as isize >= x.as_ptr() as isize + // && py as isize >= y.as_ptr() as isize + // && px as isize - x.as_ptr() as isize == (py as isize - y.as_ptr() as isize))] + while px < pxend { + let vx = (px as *const u32).read_unaligned(); + let vy = (py as *const u32).read_unaligned(); + if vx != vy { + return false; + } + px = px.add(4); + py = py.add(4); + } + let vx = (pxend as *const u32).read_unaligned(); + let vy = (pyend as *const u32).read_unaligned(); + vx == vy + } +} + +#[kani::proof] +fn main() { + let mut a = [1; 20]; + let mut b = [1; 20]; + unsafe { + small_slice_eq(&mut a, &mut b); + } +}