From 70725f1334e383c7c4428ab25bf8a6d3ada4a3f4 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Tue, 23 Apr 2024 19:10:49 -0400 Subject: [PATCH 1/4] Remove kani::Arbitrary from the modifies contract instrumentation Signed-off-by: Felipe R. Monteiro --- .../src/sysroot/contracts/check.rs | 37 ++++++++++++++++--- 1 file changed, 31 insertions(+), 6 deletions(-) diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index f18b56f934ea..f225a3cda184 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -60,7 +60,8 @@ impl<'a> ContractConditionsHandler<'a> { let wrapper_args = if let Some(wrapper_call_args) = inner.iter_mut().find_map(|stmt| try_as_wrapper_call_args(stmt, &wrapper_name)) { - let wrapper_args = make_wrapper_args(wrapper_call_args.len(), attr.len()); + let wrapper_args = + make_wrapper_idents(wrapper_call_args.len(), attr.len(), "_wrapper_arg_"); wrapper_call_args .extend(wrapper_args.clone().map(|a| Expr::Verbatim(quote!(#a)))); wrapper_args @@ -129,15 +130,34 @@ impl<'a> ContractConditionsHandler<'a> { /// each expression in the clause. pub fn emit_augmented_modifies_wrapper(&mut self) { if let ContractConditionsData::Modifies { attr } = &self.condition_type { - let wrapper_args = make_wrapper_args(self.annotated_fn.sig.inputs.len(), attr.len()); + let wrapper_args = make_wrapper_idents( + self.annotated_fn.sig.inputs.len(), + attr.len(), + "_wrapper_arg_", + ); + // Generate a unique type parameter identifier + let type_params = make_wrapper_idents( + self.annotated_fn.sig.inputs.len(), + attr.len(), + "WrapperArgType", + ); let sig = &mut self.annotated_fn.sig; - for arg in wrapper_args.clone() { + for (arg, arg_type) in wrapper_args.clone().zip(type_params) { + // Add the type parameter to the function signature's generic parameters list + sig.generics.params.push(syn::GenericParam::Type(syn::TypeParam { + attrs: vec![], + ident: arg_type.clone(), + colon_token: None, + bounds: Default::default(), + eq_token: None, + default: None, + })); let lifetime = syn::Lifetime { apostrophe: Span::call_site(), ident: arg.clone() }; sig.inputs.push(FnArg::Typed(syn::PatType { attrs: vec![], colon_token: Token![:](Span::call_site()), pat: Box::new(syn::Pat::Verbatim(quote!(#arg))), - ty: Box::new(syn::Type::Verbatim(quote!(&#lifetime impl kani::Arbitrary))), + ty: Box::new(syn::parse_quote! { &#arg_type }), })); sig.generics.params.push(syn::GenericParam::Lifetime(syn::LifetimeParam { lifetime, @@ -146,6 +166,7 @@ impl<'a> ContractConditionsHandler<'a> { attrs: vec![], })); } + self.output.extend(quote!(#[kanitool::modifies(#(#wrapper_args),*)])) } self.emit_common_header(); @@ -193,8 +214,12 @@ fn try_as_wrapper_call_args<'a>( /// Make `num` [`Ident`]s with the names `_wrapper_arg_{i}` with `i` starting at `low` and /// increasing by one each time. -fn make_wrapper_args(low: usize, num: usize) -> impl Iterator + Clone { - (low..).map(|i| Ident::new(&format!("_wrapper_arg_{i}"), Span::mixed_site())).take(num) +fn make_wrapper_idents( + low: usize, + num: usize, + prefix: &'static str, +) -> impl Iterator + Clone + 'static { + (low..).map(move |i| Ident::new(&format!("{}{}", prefix, i), Span::mixed_site())).take(num) } #[cfg(test)] From bb76eaf12eba6a7c3d62e8a20c2b3428b033e146 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Thu, 2 May 2024 17:29:43 -0400 Subject: [PATCH 2/4] Add regression test and improve documentation Signed-off-by: Felipe R. Monteiro --- .../src/sysroot/contracts/check.rs | 23 ++++++++++----- ...simple_only_verification_modifies.expected | 1 + .../simple_only_verification_modifies.rs | 28 +++++++++++++++++++ 3 files changed, 45 insertions(+), 7 deletions(-) create mode 100644 tests/expected/function-contract/modifies/simple_only_verification_modifies.expected create mode 100644 tests/expected/function-contract/modifies/simple_only_verification_modifies.rs diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index f225a3cda184..fe5c5a297ea4 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -13,6 +13,8 @@ use super::{ ContractConditionsData, ContractConditionsHandler, }; +const WRAPPER_ARG_PREFIX: &str = "_wrapper_arg_"; + impl<'a> ContractConditionsHandler<'a> { /// Create the body of a check function. /// @@ -60,8 +62,11 @@ impl<'a> ContractConditionsHandler<'a> { let wrapper_args = if let Some(wrapper_call_args) = inner.iter_mut().find_map(|stmt| try_as_wrapper_call_args(stmt, &wrapper_name)) { - let wrapper_args = - make_wrapper_idents(wrapper_call_args.len(), attr.len(), "_wrapper_arg_"); + let wrapper_args = make_wrapper_idents( + wrapper_call_args.len(), + attr.len(), + WRAPPER_ARG_PREFIX, + ); wrapper_call_args .extend(wrapper_args.clone().map(|a| Expr::Verbatim(quote!(#a)))); wrapper_args @@ -125,15 +130,19 @@ impl<'a> ContractConditionsHandler<'a> { /// Emit a modifies wrapper, possibly augmenting a prior, existing one. /// - /// We only augment if this clause is a `modifies` clause. In that case we - /// expand its signature with one new argument of type `&impl Arbitrary` for - /// each expression in the clause. + /// We only augment if this clause is a `modifies` clause. Before, + /// we annotated the wrapper arguments with `impl kani::Arbitrary`, + /// so Rust would infer the proper types for each argument. + /// We want to remove the restriction that these arguments must + /// implement `kani::Arbitrary` for checking. Now, we annotate each + /// argument with a generic type parameter, so the compiler can + /// continue inferring the correct types. pub fn emit_augmented_modifies_wrapper(&mut self) { if let ContractConditionsData::Modifies { attr } = &self.condition_type { let wrapper_args = make_wrapper_idents( self.annotated_fn.sig.inputs.len(), attr.len(), - "_wrapper_arg_", + WRAPPER_ARG_PREFIX, ); // Generate a unique type parameter identifier let type_params = make_wrapper_idents( @@ -212,7 +221,7 @@ fn try_as_wrapper_call_args<'a>( } } -/// Make `num` [`Ident`]s with the names `_wrapper_arg_{i}` with `i` starting at `low` and +/// Make `num` [`Ident`]s with the names `prefix{i}` with `i` starting at `low` and /// increasing by one each time. fn make_wrapper_idents( low: usize, diff --git a/tests/expected/function-contract/modifies/simple_only_verification_modifies.expected b/tests/expected/function-contract/modifies/simple_only_verification_modifies.expected new file mode 100644 index 000000000000..34c886c358cb --- /dev/null +++ b/tests/expected/function-contract/modifies/simple_only_verification_modifies.expected @@ -0,0 +1 @@ +VERIFICATION:- SUCCESSFUL diff --git a/tests/expected/function-contract/modifies/simple_only_verification_modifies.rs b/tests/expected/function-contract/modifies/simple_only_verification_modifies.rs new file mode 100644 index 000000000000..ea4b5950137f --- /dev/null +++ b/tests/expected/function-contract/modifies/simple_only_verification_modifies.rs @@ -0,0 +1,28 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +//! Check that is possible to use `modifies` clause for verifciation, but not stubbing. +//! Here, we cover the case when the modifies clause contains references to function +//! parameters of generic types. Noticed that here the type T is not annotated with +//! `kani::Arbitrary` since this is no longer a requirement if the contract is only +//! use for verification. + +pub mod contracts { + #[kani::modifies(x)] + #[kani::modifies(y)] + pub fn swap(x: &mut T, y: &mut T) { + core::mem::swap(x, y) + } +} + +mod verify { + use super::*; + + #[kani::proof_for_contract(contracts::swap)] + pub fn check_swap_primitive() { + let mut x: u8 = kani::any(); + let mut y: u8 = kani::any(); + contracts::swap(&mut x, &mut y) + } +} From 9c4fafa3c776a20a651cf55a9e072bb82a896721 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Fri, 3 May 2024 14:53:27 -0400 Subject: [PATCH 3/4] Minor suggestions Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- library/kani_macros/src/sysroot/contracts/check.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index fe5c5a297ea4..516bd187ba7f 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -228,7 +228,7 @@ fn make_wrapper_idents( num: usize, prefix: &'static str, ) -> impl Iterator + Clone + 'static { - (low..).map(move |i| Ident::new(&format!("{}{}", prefix, i), Span::mixed_site())).take(num) + (low..).map(move |i| Ident::new(&format!("{prefix}{i}"), Span::mixed_site())).take(num) } #[cfg(test)] From 4d64a4f8107432d0fdbe79b2eb0a6ce3ddc6064e Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Fri, 3 May 2024 14:53:42 -0400 Subject: [PATCH 4/4] Update tests/expected/function-contract/modifies/simple_only_verification_modifies.rs Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com> --- .../modifies/simple_only_verification_modifies.rs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/expected/function-contract/modifies/simple_only_verification_modifies.rs b/tests/expected/function-contract/modifies/simple_only_verification_modifies.rs index ea4b5950137f..4988dcb69c56 100644 --- a/tests/expected/function-contract/modifies/simple_only_verification_modifies.rs +++ b/tests/expected/function-contract/modifies/simple_only_verification_modifies.rs @@ -2,7 +2,7 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT // kani-flags: -Zfunction-contracts -//! Check that is possible to use `modifies` clause for verifciation, but not stubbing. +//! Check that is possible to use `modifies` clause for verification, but not stubbing. //! Here, we cover the case when the modifies clause contains references to function //! parameters of generic types. Noticed that here the type T is not annotated with //! `kani::Arbitrary` since this is no longer a requirement if the contract is only