From c0e4e1bdb6fbcd1a4850e0ca674a19f568f0d918 Mon Sep 17 00:00:00 2001 From: "Felipe R. Monteiro" Date: Fri, 3 May 2024 15:25:17 -0400 Subject: [PATCH] Remove kani::Arbitrary from the modifies contract instrumentation (#3169) This is an additional fix for https://github.com/model-checking/kani/pull/3098. With this fix, Kani should be able to check for contracts using modifies clauses that contain references to types that doesn't implement `kani::Arbitrary`. The verification will still fail if the same contract is used as a verified stub. --------- Signed-off-by: Felipe R. Monteiro --- .../src/sysroot/contracts/check.rs | 54 +++++++++++++++---- ...simple_only_verification_modifies.expected | 1 + .../simple_only_verification_modifies.rs | 28 ++++++++++ 3 files changed, 73 insertions(+), 10 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 f18b56f934ea..516bd187ba7f 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,7 +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_args(wrapper_call_args.len(), attr.len()); + 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 @@ -124,20 +130,43 @@ 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_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_PREFIX, + ); + // 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 +175,7 @@ impl<'a> ContractConditionsHandler<'a> { attrs: vec![], })); } + self.output.extend(quote!(#[kanitool::modifies(#(#wrapper_args),*)])) } self.emit_common_header(); @@ -191,10 +221,14 @@ 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_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)] 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..4988dcb69c56 --- /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 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 +//! 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) + } +}