Add regular & fixme tests for function contracts (#3371)

I'm adding a few fix-me tests that I bumped into while working on #3363.
Most of them will be fixed by #3363, except the one related to #3370.

The original PR is already quite large, so I decided to just push all of
these as fixme tests for now. This is now ready for review!

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Felipe R. Monteiro <felisous@amazon.com>
Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Co-authored-by: Carolyn Zech <cmzech@amazon.com>

Author: 4 people

tests/kani/FunctionContracts/fixme_receiver_contracts.rs

@@ -0,0 +1,147 @@
+// 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: u8 = kani::any();
+        unsafe { obj.set_val(new_val) };
+    }
+
+    #[kani::proof_for_contract(CharASCII::set_mut_ref)]
+    fn check_mut_ref() {
+        let mut obj = CharASCII::any();
+        let new_val: u8 = kani::any();
+        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: u8 = kani::any();
+        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: u8 = kani::any();
+        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: u8 = kani::any();
+        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: u8 = kani::any();
+        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: u8 = kani::any();
+        unsafe { Pin::new(Box::new(obj)).set_pin_box(new_val) };
+    }
+}

tests/kani/FunctionContracts/fn_params.rs

@@ -21,8 +21,6 @@ struct MyStruct {
 #[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),
@@ -41,8 +39,6 @@ pub fn odd_parameters_eq(
 #[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),

tests/kani/FunctionContracts/modify_slice_elem.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! Check that Kani correctly verifies 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())
+    }
+}