Remove kani::Arbitrary from the modifies contract instrumentation (#3169

)

This is an additional fix for
#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 <felisous@amazon.com>

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<Item = syn::Ident> + 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<Item = syn::Ident> + Clone + 'static {
+ (low..).map(move |i| Ident::new(&format!("{prefix}{i}"), Span::mixed_site())).take(num)
 }
 
 #[cfg(test)]

tests/expected/function-contract/modifies/simple_only_verification_modifies.expected

@@ -0,0 +1 @@
+VERIFICATION:- SUCCESSFUL

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<T>(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)
+ }
+}