From 46a26fd9cb65cee078928fc1543be8d846ca1080 Mon Sep 17 00:00:00 2001 From: Kasim Te <91560+kasimte@users.noreply.github.com> Date: Tue, 6 Oct 2026 11:47:14 -0400 Subject: [PATCH] Move an owned receiver into the replace closure so const fns with contracts compile The replace closure only borrows `self` (it cannot be re-bound by the kani#3667 dummy reassignments that cover the other arguments -- `self` is a keyword), so the annotated function's own scope had to drop it. For a `const fn` whose receiver type has a destructor that is rejected with E0493. Emit `let self_kani_internal = self;` at the tail of the replace body, after every borrow of `self`, so any drop lands inside the closure body instead. --- .../src/sysroot/contracts/check.rs | 9 ++++ .../kani_macros/src/sysroot/contracts/mod.rs | 1 + .../src/sysroot/contracts/replace.rs | 43 +++++++++++++++ .../const_fn_owned_receiver_fail.expected | 1 + .../const_fn_owned_receiver_fail.rs | 27 ++++++++++ .../const_fn_owned_receiver.rs | 54 +++++++++++++++++++ 6 files changed, 135 insertions(+) create mode 100644 tests/expected/function-contract/const_fn_owned_receiver_fail.expected create mode 100644 tests/expected/function-contract/const_fn_owned_receiver_fail.rs create mode 100644 tests/kani/FunctionContracts/const_fn_owned_receiver.rs diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index 73b8bfcdb6f0..365627d101b5 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -185,6 +185,15 @@ impl<'a> ContractConditionsHandler<'a> { .unwrap_or(false) } + /// Return whether the original function takes `self` by value (an owned + /// receiver), e.g. `fn into_inner(self)`. + pub fn has_owned_receiver(&self) -> bool { + let first_arg = self.annotated_fn.sig.inputs.first(); + first_arg + .map(|arg| matches!(arg, FnArg::Receiver(syn::Receiver { reference: None, .. },))) + .unwrap_or(false) + } + /// Generate argument re-definitions for arguments. /// /// This is used so Kani doesn't think that modifying a local argument value is a side effect, diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index af1c15cc53b4..c7921805db77 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -528,6 +528,7 @@ mod replace; mod shared; const INTERNAL_RESULT_IDENT: &str = "result_kani_internal"; +const INTERNAL_SELF_IDENT: &str = "self_kani_internal"; pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { contract_main(attr, item, ContractConditionsType::Requires) diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 77edf142fdcc..c44de8f9984c 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -10,6 +10,7 @@ use syn::{Block, Stmt}; use super::{ ContractConditionsData, ContractConditionsHandler, ContractMode, INTERNAL_RESULT_IDENT, + INTERNAL_SELF_IDENT, helpers::*, shared::{build_ensures, split_for_remembers, try_as_result_assign}, }; @@ -58,6 +59,10 @@ impl<'a> ContractConditionsHandler<'a> { fn split_replace(&self, mut stmts: Vec) -> (Vec, Vec) { // Pop the return result since we always re-add it. stmts.pop(); + // Likewise the owned-receiver move (when present); re-added at the tail. + if stmts.last().is_some_and(is_replace_receiver_move) { + stmts.pop(); + } let idx = stmts .iter() @@ -81,6 +86,17 @@ 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 { + // `self` cannot be re-bound like the arguments in `arg_redefinitions` + // (it is a keyword), so the replace closure would only borrow an owned + // receiver, leaving the annotated function's own scope to drop it, which + // `const fn`s whose receiver type has a destructor reject (E0493). Move + // it into the closure at the tail of the body, after every borrow of + // `self` (preconditions, remembers, modifies havocs, postconditions), so + // any drop lands outside const-checking. + let recv_move = self.has_owned_receiver().then(|| { + let self_repl = Ident::new(INTERNAL_SELF_IDENT, Span::call_site()); + quote!(let #self_repl = self;) + }); match &self.condition_type { ContractConditionsData::Requires { attr } => { let Self { attr_copy, .. } = self; @@ -91,6 +107,7 @@ impl<'a> ContractConditionsHandler<'a> { #assert_bracketed #(#before)* #(#after)* + #recv_move #result }) } @@ -107,6 +124,7 @@ impl<'a> ContractConditionsHandler<'a> { #(#rest_of_before)* #(#after)* kani::assume(#ensures_bracketed); + #recv_move #result }) } @@ -128,6 +146,7 @@ impl<'a> ContractConditionsHandler<'a> { #(#before)* #(#havoc_stmts)* #(#after)* + #recv_move #result }) } @@ -161,6 +180,30 @@ impl<'a> ContractConditionsHandler<'a> { } } +/// Is this the owned-receiver move statement (`let self_kani_internal = self;`) +/// that [`ContractConditionsHandler::expand_replace_body`] emits at the tail of a +/// replace body so the receiver drops inside the closure (see that method). +fn is_replace_receiver_move(stmt: &syn::Stmt) -> bool { + let syn::Stmt::Local(syn::Local { + pat: syn::Pat::Ident(syn::PatIdent { ident, .. }), + init: Some(syn::LocalInit { expr, diverge: None, .. }), + .. + }) = stmt + else { + return false; + }; + // Match the exact statement `expand_replace_body` emits: a bind of + // `self_kani_internal` to the bare receiver `self`, and nothing else. + ident == INTERNAL_SELF_IDENT + && matches!( + expr.as_ref(), + syn::Expr::Path(p) + if p.qself.is_none() + && p.path.segments.len() == 1 + && p.path.segments[0].ident == "self" + ) +} + /// Is this statement `let result_kani_internal : <...> = kani::any_modifies();`. fn is_replace_return_havoc(stmt: &syn::Stmt) -> bool { let Some(syn::LocalInit { diverge: None, expr: e, .. }) = try_as_result_assign(stmt) else { diff --git a/tests/expected/function-contract/const_fn_owned_receiver_fail.expected b/tests/expected/function-contract/const_fn_owned_receiver_fail.expected new file mode 100644 index 000000000000..6591cf27a8db --- /dev/null +++ b/tests/expected/function-contract/const_fn_owned_receiver_fail.expected @@ -0,0 +1 @@ +VERIFICATION:- FAILED diff --git a/tests/expected/function-contract/const_fn_owned_receiver_fail.rs b/tests/expected/function-contract/const_fn_owned_receiver_fail.rs new file mode 100644 index 000000000000..b46f2b6acc58 --- /dev/null +++ b/tests/expected/function-contract/const_fn_owned_receiver_fail.rs @@ -0,0 +1,27 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts + +//! A deliberately violated ensures on a `const fn` with an owned `Drop` +//! receiver must still fail: the receiver-move in the replace body must not +//! weaken checking. `Owned` wraps a `u32` (no `Box` deref in the ensures) so +//! the only failing check is the false postcondition itself. + +struct Owned(u32); + +impl Drop for Owned { + fn drop(&mut self) {} +} + +impl Owned { + #[kani::ensures(|result: &Owned| result.0 == old(self.0) + 1)] + const fn identity(self) -> Owned { + self + } +} + +#[kani::proof_for_contract(Owned::identity)] +fn harness() { + let v: u32 = kani::any_where(|v: &u32| *v < 100); + let _ = Owned(v).identity(); +} diff --git a/tests/kani/FunctionContracts/const_fn_owned_receiver.rs b/tests/kani/FunctionContracts/const_fn_owned_receiver.rs new file mode 100644 index 000000000000..6e36f1dac845 --- /dev/null +++ b/tests/kani/FunctionContracts/const_fn_owned_receiver.rs @@ -0,0 +1,54 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Zfunction-contracts -Zstubbing + +//! A contract on a `const fn` that takes `self` by value must compile and +//! verify when `Self` has a destructor. The replace stub used to leave `self` +//! to drop in the annotated function's own scope, which `const fn`s reject +//! (E0493); the other arguments are already covered by the #3667 reassignments. +//! +//! `Owned` has an explicit `Drop` (so it is a needs-drop receiver, like a field +//! of `Box`), but wraps a `u32` so the replace-mode harness can havoc it. The +//! body moves `self` into the return without dropping it, so it is itself +//! const-legal; the only drop of `self` previously came from the contract. + +struct Owned(u32); + +impl Drop for Owned { + fn drop(&mut self) {} +} + +impl kani::Arbitrary for Owned { + fn any() -> Self { + Owned(kani::any()) + } +} + +impl Owned { + #[kani::requires(self.0 < 100)] + #[kani::ensures(|result: &Owned| result.0 == old(self.0))] + const fn identity(self) -> Owned { + self + } +} + +/// Check mode: compiles the full contract expansion (including the replace arm +/// that previously hit E0493) and verifies the contract against the body. +#[kani::proof_for_contract(Owned::identity)] +fn check_owned_receiver_const_fn() { + let out = Owned(kani::any_where(|v: &u32| *v < 100)).identity(); + assert!(out.0 < 100); +} + +fn caller(o: Owned) -> Owned { + o.identity() +} + +/// Replace mode: stubs `identity` with its contract, exercising the replace +/// closure (with the tail receiver-move) end to end. +#[kani::proof] +#[kani::stub_verified(Owned::identity)] +fn check_owned_receiver_replace() { + let out = caller(Owned(kani::any_where(|v: &u32| *v < 100))); + assert!(out.0 < 100); +}