From 5710b26f57ada249c166ce3eb6dc271c7c0e31f5 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Wed, 16 Jul 2025 11:42:16 +0000 Subject: [PATCH] Add `panics_if` precondition to express panic-freedom Implements a solution towards #3567, following up on the RFC discussion in #3893. --- library/kani/src/contracts.rs | 2 +- library/kani_macros/src/lib.rs | 24 +++++++++++++++- .../src/sysroot/contracts/assert.rs | 6 ++++ .../src/sysroot/contracts/check.rs | 6 ++++ .../src/sysroot/contracts/initialize.rs | 9 ++++-- .../kani_macros/src/sysroot/contracts/mod.rs | 28 +++++++++++++------ .../src/sysroot/contracts/replace.rs | 10 +++++++ .../FunctionContracts/promoted_constants.rs | 13 +++++++++ 8 files changed, 84 insertions(+), 14 deletions(-) diff --git a/library/kani/src/contracts.rs b/library/kani/src/contracts.rs index 2dc2bd2a4957..a0e341a92bb4 100644 --- a/library/kani/src/contracts.rs +++ b/library/kani/src/contracts.rs @@ -275,4 +275,4 @@ //! Here, the value stored in `a` is precomputed and remembered after the function //! is called, even though the contents of `a` changed during the function execution. //! -pub use super::{ensures, modifies, proof_for_contract, requires, stub_verified}; +pub use super::{ensures, modifies, panics_if, proof_for_contract, requires, stub_verified}; diff --git a/library/kani_macros/src/lib.rs b/library/kani_macros/src/lib.rs index 9ceed99d114b..3696f0c54cb0 100644 --- a/library/kani_macros/src/lib.rs +++ b/library/kani_macros/src/lib.rs @@ -356,6 +356,25 @@ pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { attr_impl::requires(attr, item) } +/// Add a panic-freedom precondition to this function. +/// +/// This is part of the function contract API, for more general information see +/// the [module-level documentation](../kani/contracts/index.html). +/// +/// The contents of the attribute is a condition over the input values to the +/// annotated function. All Rust syntax is supported, even calling other +/// functions, but the computations must be side effect free, e.g. it cannot +/// perform I/O or use mutable memory. +/// +/// Kani requires each function that uses a contract (this attribute or +/// [`requires`][macro@requires] or [`ensures`][macro@ensures]) to have at least one designated +/// [`proof_for_contract`][macro@proof_for_contract] harness for checking the +/// contract. +#[proc_macro_attribute] +pub fn panics_if(attr: TokenStream, item: TokenStream) -> TokenStream { + attr_impl::panics_if(attr, item) +} + /// Add a postcondition to this function. /// /// This is part of the function contract API, for more general information see @@ -453,7 +472,9 @@ mod sysroot { mod contracts; mod loop_contracts; - pub use contracts::{ensures, modifies, proof_for_contract, requires, stub_verified}; + pub use contracts::{ + ensures, modifies, panics_if, proof_for_contract, requires, stub_verified, + }; pub use loop_contracts::{loop_invariant, loop_modifies}; use super::*; @@ -628,6 +649,7 @@ mod regular { no_op!(unstable); no_op!(unwind); no_op!(requires); + no_op!(panics_if); no_op!(ensures); no_op!(modifies); no_op!(proof_for_contract); diff --git a/library/kani_macros/src/sysroot/contracts/assert.rs b/library/kani_macros/src/sysroot/contracts/assert.rs index fb1d0e11a31b..bda7f8c759f2 100644 --- a/library/kani_macros/src/sysroot/contracts/assert.rs +++ b/library/kani_macros/src/sysroot/contracts/assert.rs @@ -69,6 +69,12 @@ impl<'a> ContractConditionsHandler<'a> { #(#body_stmts)* }) } + ContractConditionsData::PanicsIf { attr } => { + quote!({ + kani::assert(!(#attr), concat!("Panic: ", stringify!(#attr_copy))); + #(#body_stmts)* + }) + } ContractConditionsData::Ensures { attr } => { let (remembers, ensures_clause) = build_ensures(attr); diff --git a/library/kani_macros/src/sysroot/contracts/check.rs b/library/kani_macros/src/sysroot/contracts/check.rs index c3d459f13cba..52a8337053b6 100644 --- a/library/kani_macros/src/sysroot/contracts/check.rs +++ b/library/kani_macros/src/sysroot/contracts/check.rs @@ -29,6 +29,12 @@ impl<'a> ContractConditionsHandler<'a> { #(#body_stmts)* }) } + ContractConditionsData::PanicsIf { attr } => { + quote!({ + kani::assume(!(#attr)); + #(#body_stmts)* + }) + } ContractConditionsData::Ensures { attr } => { let (remembers, ensures_clause) = build_ensures(attr); diff --git a/library/kani_macros/src/sysroot/contracts/initialize.rs b/library/kani_macros/src/sysroot/contracts/initialize.rs index ac9ab7252562..1d9cf1bfafcd 100644 --- a/library/kani_macros/src/sysroot/contracts/initialize.rs +++ b/library/kani_macros/src/sysroot/contracts/initialize.rs @@ -49,18 +49,21 @@ impl ContractFunctionState { impl<'a> ContractConditionsHandler<'a> { /// Initialize the handler. Constructs the required - /// [`ContractConditionsType`] depending on `is_requires`. + /// [`ContractConditionsType`] depending on `is_precondition`. pub fn new( - is_requires: ContractConditionsType, + condition_kind: ContractConditionsType, attr: TokenStream, annotated_fn: &'a mut ItemFn, attr_copy: TokenStream2, ) -> Result { let mut output = TokenStream2::new(); - let condition_type = match is_requires { + let condition_type = match condition_kind { ContractConditionsType::Requires => { ContractConditionsData::Requires { attr: syn::parse(attr)? } } + ContractConditionsType::PanicsIf => { + ContractConditionsData::PanicsIf { attr: syn::parse(attr)? } + } ContractConditionsType::Ensures => { ContractConditionsData::Ensures { attr: syn::parse(attr)? } } diff --git a/library/kani_macros/src/sysroot/contracts/mod.rs b/library/kani_macros/src/sysroot/contracts/mod.rs index e11b4bf2608e..b8206a70c7e5 100644 --- a/library/kani_macros/src/sysroot/contracts/mod.rs +++ b/library/kani_macros/src/sysroot/contracts/mod.rs @@ -3,14 +3,14 @@ //! Implementation of the function contracts code generation. //! -//! The most exciting part is the handling of `requires` and `ensures`, the main -//! entry point to which is [`requires_ensures_main`]. Most of the code +//! The most exciting part is the handling of `requires`, `panics_if`, and `ensures`, the main +//! entry point to which is [`pre_post_main`]. Most of the code //! generation for that is implemented on [`ContractConditionsHandler`] with //! [`ContractFunctionState`] steering the code generation. The function state //! implements a state machine in order to be able to handle multiple attributes //! on the same function correctly. //! -//! ## How the handling for `requires`, `modifies`, and `ensures` works. +//! ## How the handling for `requires`, `panics_if`, `modifies`, and `ensures` works. //! //! Our aim is to generate a "check" function that can be used to verify the //! validity of the contract and a "replace" function that can be used as a @@ -532,6 +532,10 @@ pub fn requires(attr: TokenStream, item: TokenStream) -> TokenStream { contract_main(attr, item, ContractConditionsType::Requires) } +pub fn panics_if(attr: TokenStream, item: TokenStream) -> TokenStream { + contract_main(attr, item, ContractConditionsType::PanicsIf) +} + pub fn ensures(attr: TokenStream, item: TokenStream) -> TokenStream { contract_main(attr, item, ContractConditionsType::Ensures) } @@ -616,6 +620,7 @@ struct ContractConditionsHandler<'a> { #[derive(Copy, Clone, Eq, PartialEq)] enum ContractConditionsType { Requires, + PanicsIf, Ensures, Modifies, } @@ -628,6 +633,10 @@ enum ContractConditionsData { /// The contents of the attribute. attr: Expr, }, + PanicsIf { + /// The contents of the attribute. + attr: Expr, + }, Ensures { /// The contents of the attribute. attr: ExprClosure, @@ -658,22 +667,23 @@ impl<'a> ContractConditionsHandler<'a> { } } -/// The main meat of handling requires/ensures contracts. +/// The main meat of handling requires/panics_if/ensures contracts. /// /// See the [module level documentation][self] for a description of how the code /// generation works. fn contract_main( attr: TokenStream, item: TokenStream, - is_requires: ContractConditionsType, + condition_kind: ContractConditionsType, ) -> TokenStream { let attr_copy = TokenStream2::from(attr.clone()); let mut item_fn = parse_macro_input!(item as ItemFn); let function_state = ContractFunctionState::from_attributes(&item_fn.attrs); - let handler = match ContractConditionsHandler::new(is_requires, attr, &mut item_fn, attr_copy) { - Ok(handler) => handler, - Err(e) => return e.into_compile_error().into(), - }; + let handler = + match ContractConditionsHandler::new(condition_kind, attr, &mut item_fn, attr_copy) { + Ok(handler) => handler, + Err(e) => return e.into_compile_error().into(), + }; handler.dispatch_on(function_state).into() } diff --git a/library/kani_macros/src/sysroot/contracts/replace.rs b/library/kani_macros/src/sysroot/contracts/replace.rs index 719a96dcc429..a0281005de71 100644 --- a/library/kani_macros/src/sysroot/contracts/replace.rs +++ b/library/kani_macros/src/sysroot/contracts/replace.rs @@ -92,6 +92,16 @@ impl<'a> ContractConditionsHandler<'a> { #result }) } + ContractConditionsData::PanicsIf { attr } => { + let Self { attr_copy, .. } = self; + let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); + quote!({ + kani::assert(!(#attr), concat!("Panic: ", stringify!(#attr_copy))); + #(#before)* + #(#after)* + #result + }) + } ContractConditionsData::Ensures { attr } => { let (remembers, ensures_clause) = build_ensures(attr); let result = Ident::new(INTERNAL_RESULT_IDENT, Span::call_site()); diff --git a/tests/kani/FunctionContracts/promoted_constants.rs b/tests/kani/FunctionContracts/promoted_constants.rs index 75202f1bfedd..a4f5974f2d57 100644 --- a/tests/kani/FunctionContracts/promoted_constants.rs +++ b/tests/kani/FunctionContracts/promoted_constants.rs @@ -52,3 +52,16 @@ fn check_static() { fn check_mut_static() { foo_mut_static(kani::any()); } + +/// Add a contract using a mutable static. +#[kani::requires(&foo == unsafe { &FOO_MUT })] +#[kani::panics_if(foo.0 != 1)] +pub fn foo_mut_static_with_panics_if(foo: Foo) -> Foo { + assert!(foo.0 == 1); + foo +} + +#[kani::proof_for_contract(foo_mut_static_with_panics_if)] +fn check_mut_static_with_panics_if() { + foo_mut_static_with_panics_if(kani::any()); +}