From 981317262df7f20564260b0a1003c854d923c36b Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 22 Jul 2024 13:15:37 -0700 Subject: [PATCH 1/7] Test contract support to parameter patterns --- tests/kani/FunctionContracts/fn_params.rs | 72 +++++++++ .../FunctionContracts/receiver_contracts.rs | 147 ++++++++++++++++++ 2 files changed, 219 insertions(+) create mode 100644 tests/kani/FunctionContracts/fn_params.rs create mode 100644 tests/kani/FunctionContracts/receiver_contracts.rs diff --git a/tests/kani/FunctionContracts/fn_params.rs b/tests/kani/FunctionContracts/fn_params.rs new file mode 100644 index 000000000000..34b9d54771d6 --- /dev/null +++ b/tests/kani/FunctionContracts/fn_params.rs @@ -0,0 +1,72 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Checks that function contracts work with different type of parameter expressions: +//! Source: +//! +//! Note: See `receiver_contracts` for receiver parameters. + +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 . +#[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 . +#[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()) + } +} diff --git a/tests/kani/FunctionContracts/receiver_contracts.rs b/tests/kani/FunctionContracts/receiver_contracts.rs new file mode 100644 index 000000000000..3a70aff37475 --- /dev/null +++ b/tests/kani/FunctionContracts/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 +//! - Rc +//! - Arc +//! - Pin

where P is one of the types above +//! Source: +// compile-flags: --edition 2021 + +#![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, 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, 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, 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>, 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) }; + } +} From aac359fdb4beb60f0f78d4b4e66d27fc6f0601f9 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 26 Jul 2024 15:02:47 -0700 Subject: [PATCH 2/7] Add fixme tests for contracts for different issues --- .../{fn_params.rs => fixme_fn_params.rs} | 1 + .../fixme_modify_slice_elem.rs | 25 +++++++++++++++++++ .../fixme_old_requires_order.rs | 18 +++++++++++++ ...ntracts.rs => fixme_receiver_contracts.rs} | 1 + 4 files changed, 45 insertions(+) rename tests/kani/FunctionContracts/{fn_params.rs => fixme_fn_params.rs} (98%) create mode 100644 tests/kani/FunctionContracts/fixme_modify_slice_elem.rs create mode 100644 tests/kani/FunctionContracts/fixme_old_requires_order.rs rename tests/kani/FunctionContracts/{receiver_contracts.rs => fixme_receiver_contracts.rs} (99%) diff --git a/tests/kani/FunctionContracts/fn_params.rs b/tests/kani/FunctionContracts/fixme_fn_params.rs similarity index 98% rename from tests/kani/FunctionContracts/fn_params.rs rename to tests/kani/FunctionContracts/fixme_fn_params.rs index 34b9d54771d6..72714bb0bd20 100644 --- a/tests/kani/FunctionContracts/fn_params.rs +++ b/tests/kani/FunctionContracts/fixme_fn_params.rs @@ -4,6 +4,7 @@ //! Source: //! //! Note: See `receiver_contracts` for receiver parameters. +// kani-flags: -Z function-contracts extern crate kani; use std::convert::TryFrom; diff --git a/tests/kani/FunctionContracts/fixme_modify_slice_elem.rs b/tests/kani/FunctionContracts/fixme_modify_slice_elem.rs new file mode 100644 index 000000000000..0efdcbdb669b --- /dev/null +++ b/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::(); + modify_slice(&mut data, kani::any(), kani::any()) + } +} diff --git a/tests/kani/FunctionContracts/fixme_old_requires_order.rs b/tests/kani/FunctionContracts/fixme_old_requires_order.rs new file mode 100644 index 000000000000..c471df44b7e8 --- /dev/null +++ b/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: +// 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()); +} diff --git a/tests/kani/FunctionContracts/receiver_contracts.rs b/tests/kani/FunctionContracts/fixme_receiver_contracts.rs similarity index 99% rename from tests/kani/FunctionContracts/receiver_contracts.rs rename to tests/kani/FunctionContracts/fixme_receiver_contracts.rs index 3a70aff37475..22f151c9b240 100644 --- a/tests/kani/FunctionContracts/receiver_contracts.rs +++ b/tests/kani/FunctionContracts/fixme_receiver_contracts.rs @@ -9,6 +9,7 @@ //! - Pin

where P is one of the types above //! Source: // compile-flags: --edition 2021 +// kani-flags: -Zfunction-contracts #![feature(rustc_attrs)] From ea918881f236e8ce8dd52d72f31f4718d5611c2f Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 13 Aug 2024 10:30:03 -0700 Subject: [PATCH 3/7] Apply suggestions from code review Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- tests/kani/FunctionContracts/fixme_old_requires_order.rs | 1 - tests/kani/FunctionContracts/fixme_receiver_contracts.rs | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/tests/kani/FunctionContracts/fixme_old_requires_order.rs b/tests/kani/FunctionContracts/fixme_old_requires_order.rs index c471df44b7e8..4a0a97075c05 100644 --- a/tests/kani/FunctionContracts/fixme_old_requires_order.rs +++ b/tests/kani/FunctionContracts/fixme_old_requires_order.rs @@ -13,6 +13,5 @@ pub fn next(mut val: i32) -> i32 { #[kani::proof_for_contract(next)] pub fn check_next() { - // let _ = next(kani::any_where(|val: &i32| *val < i32::MAX)); let _ = next(kani::any()); } diff --git a/tests/kani/FunctionContracts/fixme_receiver_contracts.rs b/tests/kani/FunctionContracts/fixme_receiver_contracts.rs index 22f151c9b240..477b1fe516f8 100644 --- a/tests/kani/FunctionContracts/fixme_receiver_contracts.rs +++ b/tests/kani/FunctionContracts/fixme_receiver_contracts.rs @@ -20,7 +20,7 @@ use std::pin::Pin; use std::rc::Rc; use std::sync::Arc; -/// Type representing a valid ASCII value going from `0..=128`. +/// 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)] From 2fd0fe45cf37c9ca3cf7932e858f28545a4670d1 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 21 Oct 2024 11:53:08 -0400 Subject: [PATCH 4/7] update tests --- charon | 1 + .../kani/FunctionContracts/fixme_fn_params.rs | 73 --------- .../fixme_old_requires_order.rs | 17 -- .../fixme_receiver_contracts copy.rs | 148 ++++++++++++++++++ .../fixme_receiver_contracts.rs | 30 ++-- tests/kani/FunctionContracts/fn_params.rs | 4 - ...ify_slice_elem.rs => modify_slice_elem.rs} | 0 7 files changed, 164 insertions(+), 109 deletions(-) create mode 160000 charon delete mode 100644 tests/kani/FunctionContracts/fixme_fn_params.rs delete mode 100644 tests/kani/FunctionContracts/fixme_old_requires_order.rs create mode 100644 tests/kani/FunctionContracts/fixme_receiver_contracts copy.rs rename tests/kani/FunctionContracts/{fixme_modify_slice_elem.rs => modify_slice_elem.rs} (100%) diff --git a/charon b/charon new file mode 160000 index 000000000000..cdc1dcde447a --- /dev/null +++ b/charon @@ -0,0 +1 @@ +Subproject commit cdc1dcde447a50cbc20336c79b21b42ac977b7fd diff --git a/tests/kani/FunctionContracts/fixme_fn_params.rs b/tests/kani/FunctionContracts/fixme_fn_params.rs deleted file mode 100644 index 72714bb0bd20..000000000000 --- a/tests/kani/FunctionContracts/fixme_fn_params.rs +++ /dev/null @@ -1,73 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -//! Checks that function contracts work with different type of parameter expressions: -//! Source: -//! -//! 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 . -#[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 . -#[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()) - } -} diff --git a/tests/kani/FunctionContracts/fixme_old_requires_order.rs b/tests/kani/FunctionContracts/fixme_old_requires_order.rs deleted file mode 100644 index 4a0a97075c05..000000000000 --- a/tests/kani/FunctionContracts/fixme_old_requires_order.rs +++ /dev/null @@ -1,17 +0,0 @@ -// 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: -// 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()); -} diff --git a/tests/kani/FunctionContracts/fixme_receiver_contracts copy.rs b/tests/kani/FunctionContracts/fixme_receiver_contracts copy.rs new file mode 100644 index 000000000000..4d84a9642783 --- /dev/null +++ b/tests/kani/FunctionContracts/fixme_receiver_contracts copy.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 +//! - Rc +//! - Arc +//! - Pin

where P is one of the types above +//! Source: +// 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, 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, 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, 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>, 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 original = obj.0; + 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) }; + } +} diff --git a/tests/kani/FunctionContracts/fixme_receiver_contracts.rs b/tests/kani/FunctionContracts/fixme_receiver_contracts.rs index 477b1fe516f8..4d84a9642783 100644 --- a/tests/kani/FunctionContracts/fixme_receiver_contracts.rs +++ b/tests/kani/FunctionContracts/fixme_receiver_contracts.rs @@ -28,7 +28,7 @@ struct CharASCII(u8); impl kani::Arbitrary for CharASCII { fn any() -> CharASCII { - let val = kani::any_where(|inner: &u8| *inner <= 128); + let val = kani::any_where(|inner: &u8| *inner < 128); unsafe { CharASCII(val) } } } @@ -37,49 +37,49 @@ impl kani::Arbitrary for CharASCII { /// receivers. impl CharASCII { #[kani::modifies(&self.0)] - #[kani::requires(new_val <= 128)] + #[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::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::requires(new_val < 128)] #[kani::ensures(|_| self.as_ref().0 == new_val)] unsafe fn set_box(mut self: Box, new_val: u8) { self.as_mut().0 = new_val } #[kani::modifies(&self.as_ref().0)] - #[kani::requires(new_val <= 128)] + #[kani::requires(new_val < 128)] #[kani::ensures(|_| self.as_ref().0 == new_val)] unsafe fn set_rc(mut self: Rc, new_val: u8) { Rc::<_>::get_mut(&mut self).unwrap().0 = new_val } #[kani::modifies(&self.as_ref().0)] - #[kani::requires(new_val <= 128)] + #[kani::requires(new_val < 128)] #[kani::ensures(|_| self.as_ref().0 == new_val)] unsafe fn set_arc(mut self: Arc, new_val: u8) { Arc::<_>::get_mut(&mut self).unwrap().0 = new_val; } #[kani::modifies(&self.0)] - #[kani::requires(new_val <= 128)] + #[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::requires(new_val < 128)] #[kani::ensures(|_| self.0 == new_val)] unsafe fn set_pin_box(mut self: Pin>, new_val: u8) { self.0 = new_val @@ -94,7 +94,7 @@ mod verify { fn check_set_val() { let mut obj = CharASCII::any(); let original = obj.0; - let new_val = kani::any_where(|new| *new != original); + let new_val: u8 = kani::any(); unsafe { obj.set_val(new_val) }; } @@ -102,7 +102,7 @@ mod verify { fn check_mut_ref() { let mut obj = CharASCII::any(); let original = obj.0; - let new_val = kani::any_where(|new| *new != original); + let new_val: u8 = kani::any(); unsafe { obj.set_mut_ref(new_val) }; } @@ -110,7 +110,7 @@ mod verify { fn check_box() { let obj = CharASCII::any(); let original = obj.0; - let new_val = kani::any_where(|new| *new != original); + let new_val: u8 = kani::any(); unsafe { Box::new(obj).set_box(new_val) }; } @@ -118,7 +118,7 @@ mod verify { fn check_rc() { let obj = CharASCII::any(); let original = obj.0; - let new_val = kani::any_where(|new| *new != original); + let new_val: u8 = kani::any(); unsafe { Rc::new(obj).set_rc(new_val) }; } @@ -126,7 +126,7 @@ mod verify { fn check_arc() { let obj = CharASCII::any(); let original = obj.0; - let new_val = kani::any_where(|new| *new != original); + let new_val: u8 = kani::any(); unsafe { Arc::new(obj).set_arc(new_val) }; } @@ -134,7 +134,7 @@ mod verify { fn check_pin() { let mut obj = CharASCII::any(); let original = obj.0; - let new_val = kani::any_where(|new| *new != original); + let new_val: u8 = kani::any(); unsafe { Pin::new(&mut obj).set_pin(new_val) }; } @@ -142,7 +142,7 @@ mod verify { fn check_pin_box() { let obj = CharASCII::any(); let original = obj.0; - let new_val = kani::any_where(|new| *new != original); + let new_val: u8 = kani::any(); unsafe { Pin::new(Box::new(obj)).set_pin_box(new_val) }; } } diff --git a/tests/kani/FunctionContracts/fn_params.rs b/tests/kani/FunctionContracts/fn_params.rs index b485ddf2b32b..42e2c52c193e 100644 --- a/tests/kani/FunctionContracts/fn_params.rs +++ b/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 . -#[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 . -#[kani::requires(char::try_from(first).is_ok())] pub fn odd_parameters_eq_wrong( [first, second]: [u32; 2], (tup_c, tup_u): (char, u32), diff --git a/tests/kani/FunctionContracts/fixme_modify_slice_elem.rs b/tests/kani/FunctionContracts/modify_slice_elem.rs similarity index 100% rename from tests/kani/FunctionContracts/fixme_modify_slice_elem.rs rename to tests/kani/FunctionContracts/modify_slice_elem.rs From 62f2855171a8238b244e9185f55675112a76e324 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 21 Oct 2024 11:57:11 -0400 Subject: [PATCH 5/7] remove charon submodule --- charon | 1 - 1 file changed, 1 deletion(-) delete mode 160000 charon diff --git a/charon b/charon deleted file mode 160000 index cdc1dcde447a..000000000000 --- a/charon +++ /dev/null @@ -1 +0,0 @@ -Subproject commit cdc1dcde447a50cbc20336c79b21b42ac977b7fd From f742cd2d8d2d348649e2a7b2b1db788ee702a339 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Mon, 21 Oct 2024 11:58:49 -0400 Subject: [PATCH 6/7] remove test copy --- charon | 1 + .../fixme_receiver_contracts copy.rs | 148 ------------------ 2 files changed, 1 insertion(+), 148 deletions(-) create mode 160000 charon delete mode 100644 tests/kani/FunctionContracts/fixme_receiver_contracts copy.rs diff --git a/charon b/charon new file mode 160000 index 000000000000..cdc1dcde447a --- /dev/null +++ b/charon @@ -0,0 +1 @@ +Subproject commit cdc1dcde447a50cbc20336c79b21b42ac977b7fd diff --git a/tests/kani/FunctionContracts/fixme_receiver_contracts copy.rs b/tests/kani/FunctionContracts/fixme_receiver_contracts copy.rs deleted file mode 100644 index 4d84a9642783..000000000000 --- a/tests/kani/FunctionContracts/fixme_receiver_contracts copy.rs +++ /dev/null @@ -1,148 +0,0 @@ -// 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 -//! - Rc -//! - Arc -//! - Pin

where P is one of the types above -//! Source: -// 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, 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, 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, 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>, 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 original = obj.0; - 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) }; - } -} From 44b282dd374125bf3fc36fc03cd6b2a1364a9f2e Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 24 Oct 2024 12:50:01 -0700 Subject: [PATCH 7/7] Apply suggestions from code review Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- tests/kani/FunctionContracts/fixme_receiver_contracts.rs | 1 - tests/kani/FunctionContracts/modify_slice_elem.rs | 2 +- 2 files changed, 1 insertion(+), 2 deletions(-) diff --git a/tests/kani/FunctionContracts/fixme_receiver_contracts.rs b/tests/kani/FunctionContracts/fixme_receiver_contracts.rs index 4d84a9642783..3a894354b868 100644 --- a/tests/kani/FunctionContracts/fixme_receiver_contracts.rs +++ b/tests/kani/FunctionContracts/fixme_receiver_contracts.rs @@ -101,7 +101,6 @@ mod verify { #[kani::proof_for_contract(CharASCII::set_mut_ref)] fn check_mut_ref() { let mut obj = CharASCII::any(); - let original = obj.0; let new_val: u8 = kani::any(); unsafe { obj.set_mut_ref(new_val) }; } diff --git a/tests/kani/FunctionContracts/modify_slice_elem.rs b/tests/kani/FunctionContracts/modify_slice_elem.rs index 0efdcbdb669b..50df13b45af3 100644 --- a/tests/kani/FunctionContracts/modify_slice_elem.rs +++ b/tests/kani/FunctionContracts/modify_slice_elem.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! Check that Kani correctly verify the contract that modifies slices. +//! 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