Add regular & fixme tests for function contracts

tests/kani/FunctionContracts/fixme_fn_params.rs

@@ -0,0 +1,73 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Checks that function contracts work with different type of parameter expressions:
+//! Source: <https://doc.rust-lang.org/reference/items/functions.html>
+//!
+//! Note: See `receiver_contracts` for receiver parameters.
+// kani-flags: -Z function-contracts
+
+extern crate kani;
+use std::convert::TryFrom;
+
+/// Dummy structure to check different patterns in contract.
+#[derive(Copy, Clone, PartialEq, Eq, kani::Arbitrary)]
+struct MyStruct {
+    c: char,
+    u: u32,
+}
+
+/// Add contracts to ensure that all parameters are representing the same pair (char, u32).
+#[kani::requires(val.u == second)]
+#[kani::requires(val.u == tup_u)]
+#[kani::requires(Ok(val.c) == char::try_from(first))]
+#[kani::requires(val.c == tup_c)]
+/// We need this extra clause due to <https://github.com/model-checking/kani/issues/3370>.
+#[kani::requires(char::try_from(first).is_ok())]
+pub fn odd_parameters_eq(
+    [first, second]: [u32; 2],
+    (tup_c, tup_u): (char, u32),
+    val @ MyStruct { c: val_c, u }: MyStruct,
+) {
+    assert_eq!(tup_c, char::try_from(first).unwrap());
+    assert_eq!(tup_c, val_c);
+
+    assert_eq!(tup_u, second);
+    assert_eq!(tup_u, u);
+    assert_eq!(val, MyStruct { c: val_c, u });
+}
+
+/// Similar to the function above, but with one requirement missing.
+#[kani::requires(val.u == second)]
+#[kani::requires(val.u == tup_u)]
+#[kani::requires(Ok(val.c) == char::try_from(first))]
+// MISSING: #[kani::requires(val.c == tup_c)]
+// We need this extra clause due to <https://github.com/model-checking/kani/issues/3370>.
+#[kani::requires(char::try_from(first).is_ok())]
+pub fn odd_parameters_eq_wrong(
+    [first, second]: [u32; 2],
+    (tup_c, tup_u): (char, u32),
+    val @ MyStruct { c: val_c, u }: MyStruct,
+) {
+    assert_eq!(tup_c, char::try_from(first).unwrap());
+    assert_eq!(tup_c, val_c);
+
+    assert_eq!(tup_u, second);
+    assert_eq!(tup_u, u);
+    assert_eq!(val, MyStruct { c: val_c, u });
+}
+
+mod verify {
+    use super::*;
+    use kani::Arbitrary;
+
+    #[kani::proof_for_contract(odd_parameters_eq)]
+    fn check_params() {
+        odd_parameters_eq(kani::any(), kani::any(), kani::any())
+    }
+
+    #[kani::should_panic]
+    #[kani::proof_for_contract(odd_parameters_eq_wrong)]
+    fn check_params_wrong() {
+        odd_parameters_eq_wrong(kani::any(), kani::any(), kani::any())
+    }
+}

tests/kani/FunctionContracts/fixme_modify_slice_elem.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check that Kani correctly verify the contract that modifies slices.
+//!
+//! Note that this test used to crash while parsing the annotations.
+// kani-flags: -Zfunction-contracts
+extern crate kani;
+
+#[kani::requires(idx < slice.len())]
+#[kani::modifies(slice.as_ptr().wrapping_add(idx))]
+#[kani::ensures(|_| slice[idx] == new_val)]
+fn modify_slice(slice: &mut [u32], idx: usize, new_val: u32) {
+    *slice.get_mut(idx).unwrap() = new_val;
+}
+
+#[cfg(kani)]
+mod verify {
+    use super::modify_slice;
+
+    #[kani::proof_for_contract(modify_slice)]
+    fn check_modify_slice() {
+        let mut data = kani::vec::any_vec::<u32, 5>();
+        modify_slice(&mut data, kani::any(), kani::any())
+    }
+}

tests/kani/FunctionContracts/fixme_old_requires_order.rs

@@ -0,0 +1,18 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check that `old()` is executed after the pre-conditions, otherwise it can fail.
+//!
+//! Issue: <https://github.com/model-checking/kani/issues/3370>
+// kani-flags: -Zfunction-contracts
+
+#[kani::requires(val < i32::MAX)]
+#[kani::ensures(|result| *result == old(val + 1))]
+pub fn next(mut val: i32) -> i32 {
+    val + 1
+}
+
+#[kani::proof_for_contract(next)]
+pub fn check_next() {
+    // let _ = next(kani::any_where(|val: &i32| *val < i32::MAX));
+    let _ = next(kani::any());
+}

tests/kani/FunctionContracts/fixme_receiver_contracts.rs

@@ -0,0 +1,148 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Checks that function contracts work with different types of receivers. I.e.:
+//! - &Self (i.e. &self)
+//! - &mut Self (i.e &mut self)
+//! - Box<Self>
+//! - Rc<Self>
+//! - Arc<Self>
+//! - Pin<P> where P is one of the types above
+//! Source: <https://doc.rust-lang.org/reference/items/traits.html?highlight=receiver#object-safety>
+// compile-flags: --edition 2021
+// kani-flags: -Zfunction-contracts
+
+#![feature(rustc_attrs)]
+
+extern crate kani;
+
+use std::boxed::Box;
+use std::pin::Pin;
+use std::rc::Rc;
+use std::sync::Arc;
+
+/// Type representing a valid ASCII value going from `0..=128`.
+#[derive(Copy, Clone, PartialEq, Eq)]
+#[rustc_layout_scalar_valid_range_start(0)]
+#[rustc_layout_scalar_valid_range_end(128)]
+struct CharASCII(u8);
+
+impl kani::Arbitrary for CharASCII {
+    fn any() -> CharASCII {
+        let val = kani::any_where(|inner: &u8| *inner <= 128);
+        unsafe { CharASCII(val) }
+    }
+}
+
+/// This type contains unsafe setter functions with the same contract but different type of
+/// receivers.
+impl CharASCII {
+    #[kani::modifies(&self.0)]
+    #[kani::requires(new_val <= 128)]
+    #[kani::ensures(|_| self.0 == new_val)]
+    unsafe fn set_val(&mut self, new_val: u8) {
+        self.0 = new_val
+    }
+
+    #[kani::modifies(&self.0)]
+    #[kani::requires(new_val <= 128)]
+    #[kani::ensures(|_| self.0 == new_val)]
+    unsafe fn set_mut_ref(self: &mut Self, new_val: u8) {
+        self.0 = new_val
+    }
+
+    #[kani::modifies(&self.as_ref().0)]
+    #[kani::requires(new_val <= 128)]
+    #[kani::ensures(|_| self.as_ref().0 == new_val)]
+    unsafe fn set_box(mut self: Box<Self>, new_val: u8) {
+        self.as_mut().0 = new_val
+    }
+
+    #[kani::modifies(&self.as_ref().0)]
+    #[kani::requires(new_val <= 128)]
+    #[kani::ensures(|_| self.as_ref().0 == new_val)]
+    unsafe fn set_rc(mut self: Rc<Self>, new_val: u8) {
+        Rc::<_>::get_mut(&mut self).unwrap().0 = new_val
+    }
+
+    #[kani::modifies(&self.as_ref().0)]
+    #[kani::requires(new_val <= 128)]
+    #[kani::ensures(|_| self.as_ref().0 == new_val)]
+    unsafe fn set_arc(mut self: Arc<Self>, new_val: u8) {
+        Arc::<_>::get_mut(&mut self).unwrap().0 = new_val;
+    }
+
+    #[kani::modifies(&self.0)]
+    #[kani::requires(new_val <= 128)]
+    #[kani::ensures(|_| self.0 == new_val)]
+    unsafe fn set_pin(mut self: Pin<&mut Self>, new_val: u8) {
+        self.0 = new_val
+    }
+
+    #[kani::modifies(&self.0)]
+    #[kani::requires(new_val <= 128)]
+    #[kani::ensures(|_| self.0 == new_val)]
+    unsafe fn set_pin_box(mut self: Pin<Box<Self>>, new_val: u8) {
+        self.0 = new_val
+    }
+}
+
+mod verify {
+    use super::*;
+    use kani::Arbitrary;
+
+    #[kani::proof_for_contract(CharASCII::set_val)]
+    fn check_set_val() {
+        let mut obj = CharASCII::any();
+        let original = obj.0;
+        let new_val = kani::any_where(|new| *new != original);
+        unsafe { obj.set_val(new_val) };
+    }
+
+    #[kani::proof_for_contract(CharASCII::set_mut_ref)]
+    fn check_mut_ref() {
+        let mut obj = CharASCII::any();
+        let original = obj.0;
+        let new_val = kani::any_where(|new| *new != original);
+        unsafe { obj.set_mut_ref(new_val) };
+    }
+
+    #[kani::proof_for_contract(CharASCII::set_box)]
+    fn check_box() {
+        let obj = CharASCII::any();
+        let original = obj.0;
+        let new_val = kani::any_where(|new| *new != original);
+        unsafe { Box::new(obj).set_box(new_val) };
+    }
+
+    #[kani::proof_for_contract(CharASCII::set_rc)]
+    fn check_rc() {
+        let obj = CharASCII::any();
+        let original = obj.0;
+        let new_val = kani::any_where(|new| *new != original);
+        unsafe { Rc::new(obj).set_rc(new_val) };
+    }
+
+    #[kani::proof_for_contract(CharASCII::set_arc)]
+    fn check_arc() {
+        let obj = CharASCII::any();
+        let original = obj.0;
+        let new_val = kani::any_where(|new| *new != original);
+        unsafe { Arc::new(obj).set_arc(new_val) };
+    }
+
+    #[kani::proof_for_contract(CharASCII::set_pin)]
+    fn check_pin() {
+        let mut obj = CharASCII::any();
+        let original = obj.0;
+        let new_val = kani::any_where(|new| *new != original);
+        unsafe { Pin::new(&mut obj).set_pin(new_val) };
+    }
+
+    #[kani::proof_for_contract(CharASCII::set_pin_box)]
+    fn check_pin_box() {
+        let obj = CharASCII::any();
+        let original = obj.0;
+        let new_val = kani::any_where(|new| *new != original);
+        unsafe { Pin::new(Box::new(obj)).set_pin_box(new_val) };
+    }
+}