Add tests for core 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);
+    }
+}