Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Enable contracts for const generic functions #3726

Merged
merged 11 commits into from
Nov 19, 2024
11 changes: 5 additions & 6 deletions library/kani_macros/src/sysroot/contracts/check.rs
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ 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 redefs = self.arg_redefinitions(true);
let modifies_closure =
self.modifies_closure(&self.annotated_fn.sig.output, &self.annotated_fn.block, redefs);
let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site());
Expand Down Expand Up @@ -175,14 +175,13 @@ impl<'a> ContractConditionsHandler<'a> {
/// Generate argument re-definitions for mutable arguments.
///
/// This is used so Kani doesn't think that modifying a local argument value is a side effect.
fn arg_redefinitions(&self) -> TokenStream2 {
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; ))
qinheping marked this conversation as resolved.
Show resolved Hide resolved
result.extend(quote!(let mut #ident = #ident;));
} else if !redefine_only_mut {
result.extend(quote!(let #ident = #ident;));
}
}
result
Expand Down
19 changes: 19 additions & 0 deletions library/kani_macros/src/sysroot/contracts/replace.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.arg_redefinitions(false);
qinheping marked this conversation as resolved.
Show resolved Hide resolved
match &self.condition_type {
ContractConditionsData::Requires { attr } => {
let Self { attr_copy, .. } = self;
Expand All @@ -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
})
}
Expand All @@ -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
})
}
Expand All @@ -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
})
}
Expand Down
Original file line number Diff line number Diff line change
@@ -0,0 +1,2 @@
** 1 of
Failed Checks: Check that *dst is assignable
27 changes: 27 additions & 0 deletions tests/expected/function-contract/const_generic_function.rs
Original file line number Diff line number Diff line change
@@ -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>()) };
}
Loading