Enable contracts for const generic functions

library/kani_macros/src/sysroot/contracts/bootstrap.rs

@@ -21,6 +21,8 @@ impl<'a> ContractConditionsHandler<'a> {
         let recursion_name = &self.recursion_name;
         let check_name = &self.check_name;
 
+        // redefs will be used in replace_closure.
+        self.redefs = self.arg_redefinitions(false);
         let replace_closure = self.replace_closure();
         let check_closure = self.check_closure();
         let recursion_closure = self.new_recursion_closure(&replace_closure, &check_closure);

library/kani_macros/src/sysroot/contracts/check.rs

@@ -84,9 +84,12 @@ impl<'a> ContractConditionsHandler<'a> {
         let wrapper_arg_ident = Ident::new(WRAPPER_ARG, Span::call_site());
         let return_type = return_type_to_type(&self.annotated_fn.sig.output);
         let mut_recv = self.has_mutable_receiver().then(|| quote!(core::ptr::addr_of!(self),));
-        let redefs = self.arg_redefinitions();
-        let modifies_closure =
-            self.modifies_closure(&self.annotated_fn.sig.output, &self.annotated_fn.block, redefs);
+        let redefs_mut_only = self.arg_redefinitions(true);
+        let modifies_closure = self.modifies_closure(
+            &self.annotated_fn.sig.output,
+            &self.annotated_fn.block,
+            redefs_mut_only,
+        );
         let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
         parse_quote!(
             let #wrapper_arg_ident = (#mut_recv);
@@ -172,17 +175,17 @@ impl<'a> ContractConditionsHandler<'a> {
             .unwrap_or(false)
     }
 
-    /// Generate argument re-definitions for mutable arguments.
+    /// Generate argument re-definitions for arguments.
     ///
-    /// This is used so Kani doesn't think that modifying a local argument value is a side effect.
-    fn arg_redefinitions(&self) -> TokenStream2 {
+    /// This is used so Kani doesn't think that modifying a local argument value is a side effect,
+    /// and avoid may-drop checks in const generic functions.
+    pub fn arg_redefinitions(&self, redefine_only_mut: bool) -> TokenStream2 {
         let mut result = TokenStream2::new();
         for (mutability, ident) in self.arg_bindings() {
             if mutability == MutBinding::Mut {
-                result.extend(quote!(let mut #ident = #ident;))
-            } else {
-                // This would make some replace some temporary variables from error messages.
-                //result.extend(quote!(let #ident = #ident; ))
+                result.extend(quote!(let mut #ident = #ident;));
+            } else if !redefine_only_mut {
+                result.extend(quote!(let #ident = #ident;));
             }
         }
         result

library/kani_macros/src/sysroot/contracts/initialize.rs

@@ -80,6 +80,7 @@ impl<'a> ContractConditionsHandler<'a> {
             condition_type,
             annotated_fn,
             attr_copy,
+            redefs: Default::default(),
             output,
             check_name,
             replace_name,

library/kani_macros/src/sysroot/contracts/mod.rs

@@ -475,6 +475,8 @@ struct ContractConditionsHandler<'a> {
     annotated_fn: &'a ItemFn,
     /// An unparsed, unmodified copy of `attr`, used in the error messages.
     attr_copy: TokenStream2,
+    /// Argument redefinitions.
+    redefs: TokenStream2,
     /// The stream to which we should write the generated code.
     output: TokenStream2,
     /// The name of the check closure.

library/kani_macros/src/sysroot/contracts/replace.rs

@@ -70,6 +70,7 @@ impl<'a> ContractConditionsHandler<'a> {
     /// `use_nondet_result` will only be true if this is the first time we are
     /// generating a replace function.
     fn expand_replace_body(&self, before: &[Stmt], after: &[Stmt]) -> TokenStream {
+        let redefs = &self.redefs;
         match &self.condition_type {
             ContractConditionsData::Requires { attr } => {
                 let Self { attr_copy, .. } = self;
@@ -78,6 +79,12 @@ impl<'a> ContractConditionsHandler<'a> {
                     kani::assert(#attr, stringify!(#attr_copy));
                     #(#before)*
                     #(#after)*
+
+                    // Add dummy assignments of the input variables to local variables
+                    // to avoid may drop checks in const generic functions.
+                    // https://github.com/model-checking/kani/issues/3667
+                    #redefs
+
                     #result
                 })
             }
@@ -93,6 +100,12 @@ impl<'a> ContractConditionsHandler<'a> {
                     #(#rest_of_before)*
                     #(#after)*
                     kani::assume(#ensures_clause);
+
+                    // Add dummy assignments of the input variables to local variables
+                    // to avoid may drop checks in const generic functions.
+                    // https://github.com/model-checking/kani/issues/3667
+                    #redefs
+
                     #result
                 })
             }
@@ -102,6 +115,12 @@ impl<'a> ContractConditionsHandler<'a> {
                     #(#before)*
                     #(unsafe{kani::internal::write_any(kani::internal::Pointer::assignable(kani::internal::untracked_deref(&#attr)))};)*
                     #(#after)*
+
+                    // Add dummy assignments of the input variables to local variables
+                    // to avoid may drop checks in const generic functions.
+                    // https://github.com/model-checking/kani/issues/3667
+                    #redefs
+
                     #result
                 })
             }

tests/expected/function-contract/const_generic_function.expected

@@ -0,0 +1,2 @@
+ ** 1 of
+Failed Checks: Check that *dst is assignable

tests/expected/function-contract/const_generic_function.rs

@@ -0,0 +1,27 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+//! Check that Kani contract can be applied to a constant generic function.
+//! <https://github.com/model-checking/kani/issues/3667>
+
+struct Foo<T> {
+    ptr: *const T,
+}
+
+impl<T: Sized> Foo<T> {
+    #[kani::requires(true)]
+    pub const unsafe fn bar(self, v: T)
+    where
+        T: Sized,
+    {
+        unsafe { core::ptr::write(self.ptr as *mut T, v) };
+    }
+}
+
+#[kani::proof_for_contract(Foo::bar)]
+fn check_const_generic_function() {
+    let x: u8 = kani::any();
+    let foo: Foo<u8> = Foo { ptr: &x };
+    unsafe { foo.bar(kani::any::<u8>()) };
+}