Enable contracts for const generic functions (#3726)

This PR adds dummy assignments of the input variables to local variables
in contracts-replace-closure to avoid may-drop checks in const generic
functions.

Resolves #3667 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

Author: qinheping

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/replace.rs

@@ -6,7 +6,7 @@
 use proc_macro2::{Ident, Span, TokenStream};
 use quote::quote;
 use std::mem;
-use syn::Stmt;
+use syn::{Block, Stmt};
 
 use super::{
     ClosureType, ContractConditionsData, ContractConditionsHandler, INTERNAL_RESULT_IDENT,
@@ -19,7 +19,18 @@ impl<'a> ContractConditionsHandler<'a> {
     fn initial_replace_stmts(&self) -> Vec<syn::Stmt> {
         let return_type = return_type_to_type(&self.annotated_fn.sig.output);
         let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
-        vec![syn::parse_quote!(let #result : #return_type = kani::any_modifies();)]
+        // 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
+        let redefs = self.arg_redefinitions(false);
+        let redefs_block: Block = syn::parse_quote!({#redefs});
+        vec![
+            vec![syn::parse_quote!(
+                let #result : #return_type = kani::any_modifies();
+            )],
+            redefs_block.stmts,
+        ]
+        .concat()
     }
 
     /// Split an existing replace body of the form

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