Add initial tests for std function with loops

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"

tests/std-checks/loop-contracts/slice/equal.expected

@@ -0,0 +1 @@
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.

tests/std-checks/loop-contracts/slice/memchr_naive.expected

@@ -0,0 +1 @@
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.

tests/std-checks/loop-contracts/slice/partition_dedup_by.expected

@@ -0,0 +1 @@
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.

tests/std-checks/loop-contracts/slice/repeat.expected

@@ -0,0 +1 @@
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.

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));
+}

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<usize> {
+ 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));
+}

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);
+ }
+}

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<u16>
+{
+ 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);
+ }
+}

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"

tests/std-checks/loop-contracts/str/small_slice_eq.expected

@@ -0,0 +1 @@
+Complete - 1 successfully verified harnesses, 0 failures, 1 total.

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);
+ }
+}