Remove kani::Arbitrary from the modifies contract instrumentation (rust-lang#3169)

This is an additional fix for
model-checking/kani#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 <[email protected]>

Author: feliperodri

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