Add panics_if precondition to express panic-freedom

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};

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);

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);
 

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);
 

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<Self, syn::Error> {
         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)? }
             }

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

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

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