Fail verification if contract is vacuous

kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs

@@ -48,6 +48,9 @@ pub enum PropertyClass {
     ///
     /// SPECIAL BEHAVIOR: "Errors" for this type of assertion just mean "reachable" not failure.
     Cover,
+    /// Same codegen as `Cover`, but failure will cause verification failure.
+    /// Used internally for contract instrumentation; see the contracts module in kani_macros for details.
+    ContractCover,
     /// The class of checks used for code coverage instrumentation. Only needed
     /// when working on coverage-related features.
     ///
@@ -150,6 +153,12 @@ impl GotocCtx<'_> {
         self.codegen_assert(cond.not(), PropertyClass::Cover, msg, loc)
     }
 
+    /// Generate a cover statement for a contract at the current location
+    pub fn codegen_contract_cover(&self, cond: Expr, msg: &str, span: SpanStable) -> Stmt {
+        let loc = self.codegen_caller_span_stable(span);
+        self.codegen_assert(cond.not(), PropertyClass::ContractCover, msg, loc)
+    }
+
     /// Generate a cover statement for code coverage reports.
     pub fn codegen_coverage(
         &self,

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -82,6 +82,45 @@ impl GotocHook for Cover {
     }
 }
 
+/// A hook for Kani's `contract_cover` function.
+/// This is only used internally for contract instrumentation.
+/// We use it to check that a contract's preconditions are satisfiable and that its postconditions are reachable.
+/// Unlike the standard `cover`, failing this check does cause verification failure.
+struct ContractCover;
+impl GotocHook for ContractCover {
+    fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
+        matches_function(tcx, instance.def, "KaniContractCover")
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        _instance: Instance,
+        mut fargs: Vec<Expr>,
+        _assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 2);
+        let cond = fargs.remove(0).cast_to(Type::bool());
+        let msg = fargs.remove(0);
+        let msg = gcx.extract_const_message(&msg).unwrap();
+        let target = target.unwrap();
+        let caller_loc = gcx.codegen_caller_span_stable(span);
+
+        let (msg, reach_stmt) = gcx.codegen_reachability_check(msg, span);
+
+        Stmt::block(
+            vec![
+                reach_stmt,
+                gcx.codegen_contract_cover(cond, &msg, span),
+                Stmt::goto(bb_label(target), caller_loc),
+            ],
+            caller_loc,
+        )
+    }
+}
+
 struct Assume;
 impl GotocHook for Assume {
     fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
@@ -594,6 +633,7 @@ pub fn fn_hooks() -> GotocHooks {
         hooks: vec![
             Rc::new(Panic),
             Rc::new(Assume),
+            Rc::new(ContractCover),
             Rc::new(Assert),
             Rc::new(Check),
             Rc::new(Cover),

kani-driver/src/cbmc_output_parser.rs

@@ -95,13 +95,19 @@ pub struct PropertyId {
 }
 
 impl Property {
+    const CONTRACT_COVER_PROPERTY_CLASS: &'static str = "contract_cover";
     const COVER_PROPERTY_CLASS: &'static str = "cover";
     const COVERAGE_PROPERTY_CLASS: &'static str = "code_coverage";
 
     pub fn property_class(&self) -> String {
         self.property_id.class.clone()
     }
 
+    /// Returns true if this is an contract_cover property
+    pub fn is_contract_cover_property(&self) -> bool {
+        self.property_id.class == Self::CONTRACT_COVER_PROPERTY_CLASS
+    }
+
     // Returns true if this is a code_coverage check
     pub fn is_code_coverage_property(&self) -> bool {
         self.property_id.class == Self::COVERAGE_PROPERTY_CLASS

kani-driver/src/cbmc_property_renderer.rs

@@ -512,7 +512,7 @@ pub fn postprocess_result(properties: Vec<Property>, extra_ptr_checks: bool) ->
 
     let updated_properties =
         update_properties_with_reach_status(properties_filtered, has_fundamental_failures);
-    let results_after_code_coverage = update_results_of_code_covererage_checks(updated_properties);
+    let results_after_code_coverage = update_results_of_code_coverage_checks(updated_properties);
     update_results_of_cover_checks(results_after_code_coverage)
 }
 
@@ -623,7 +623,7 @@ fn update_properties_with_reach_status(
 /// Note that these statuses are intermediate statuses that aren't reported to
 /// users but rather internally consumed and reported finally as `PARTIAL`, `FULL`
 /// or `NONE` based on aggregated line coverage results.
-fn update_results_of_code_covererage_checks(mut properties: Vec<Property>) -> Vec<Property> {
+fn update_results_of_code_coverage_checks(mut properties: Vec<Property>) -> Vec<Property> {
     for prop in properties.iter_mut() {
         if prop.is_code_coverage_property() {
             prop.status = match prop.status {
@@ -647,6 +647,9 @@ fn update_results_of_code_covererage_checks(mut properties: Vec<Property>) -> Ve
 /// Note that if the cover property was unreachable, its status at this point
 /// will be `CheckStatus::Unreachable` and not `CheckStatus::Success` since
 /// `update_properties_with_reach_status` is called beforehand
+///
+/// Although regular cover properties do not fail verification, contract cover properties do.
+/// If the assert(!cond) fails as expected, succeed; otherwise, fail.
 fn update_results_of_cover_checks(mut properties: Vec<Property>) -> Vec<Property> {
     for prop in properties.iter_mut() {
         if prop.is_cover_property() {
@@ -655,6 +658,15 @@ fn update_results_of_cover_checks(mut properties: Vec<Property>) -> Vec<Property
             } else if prop.status == CheckStatus::Failure {
                 prop.status = CheckStatus::Satisfied;
             }
+        } else if prop.is_contract_cover_property() {
+            if prop.status == CheckStatus::Unreachable
+                || prop.status == CheckStatus::Success
+                || prop.status == CheckStatus::Undetermined
+            {
+                prop.status = CheckStatus::Failure;
+            } else if prop.status == CheckStatus::Failure {
+                prop.status = CheckStatus::Success;
+            }
         }
     }
     properties

library/kani_core/src/lib.rs

@@ -199,7 +199,7 @@ macro_rules! kani_intrinsics {
         #[inline(never)]
         #[doc(hidden)]
         pub fn any_modifies<T>() -> T {
-            // This function should not be reacheable.
+            // This function should not be reachable.
             // Users must include `#[kani::recursion]` in any function contracts for recursive functions;
             // otherwise, this might not be properly instantiate. We mark this as unreachable to make
             // sure Kani doesn't report any false positives.
@@ -291,7 +291,7 @@ macro_rules! kani_intrinsics {
         /// function, both cause Kani to produce a warning since we don't support caller location.
         /// (see https://github.com/model-checking/kani/issues/2010).
         ///
-        /// This function is dead, since its caller is always  handled via a hook anyway,
+        /// This function is dead, since its caller is always handled via a hook anyway,
         /// so we just need to put a body that rustc does not complain about.
         /// An infinite loop works out nicely.
         fn kani_intrinsic<T>() -> T {
@@ -346,6 +346,14 @@ macro_rules! kani_intrinsics {
                 }
             }
 
+            /// This function is only used for function contract instrumentation.
+            /// It is the same as cover(), but if the cover statement is unreachable, it fails the contract harness.
+            /// See the contracts module in kani_macros for details.
+            #[inline(never)]
+            #[rustc_diagnostic_item = "KaniContractCover"]
+            #[doc(hidden)]
+            pub const fn contract_cover(_cond: bool, _msg: &'static str) {}
+
             /// A way to break the ownerhip rules. Only used by contracts where we can
             /// guarantee it is done safely.
             #[inline(never)]
@@ -383,7 +391,7 @@ macro_rules! kani_intrinsics {
             #[inline(never)]
             #[doc(hidden)]
             pub unsafe fn write_any<T: ?Sized>(_pointer: *mut T) {
-                // This function should not be reacheable.
+                // This function should not be reachable.
                 // Users must include `#[kani::recursion]` in any function contracts for recursive functions;
                 // otherwise, this might not be properly instantiate. We mark this as unreachable to make
                 // sure Kani doesn't report any false positives.

library/kani_macros/src/sysroot/contracts/check.rs

@@ -25,6 +25,7 @@ impl<'a> ContractConditionsHandler<'a> {
             ContractConditionsData::Requires { attr } => {
                 quote!({
                     kani::assume(#attr);
+                    kani::internal::contract_cover(#attr, "The contract's precondition is satisfiable.");
                     #(#body_stmts)*
                 })
             }
@@ -46,6 +47,7 @@ impl<'a> ContractConditionsHandler<'a> {
                     #(#assumes)*
                     #remembers
                     #(#rest_of_body)*
+                    kani::internal::contract_cover(#ensures_clause, "The contract's postcondition is reachable.");
                     #exec_postconditions
                     #return_expr
                 })

library/kani_macros/src/sysroot/contracts/mod.rs

@@ -58,6 +58,10 @@
 //! added before the body and postconditions after as well as injected before
 //! every `return` (see [`PostconditionInjector`]). All arguments are captured
 //! by the closure.
+//! We also inject contract_cover checks after the precondition and before the postcondition.
+//! The precondition cover checks ensure that the precondition is satisfiable; i.e.,
+//! that the precondition does not empty the search space and produce a vacuous proof.
+//! The postcondition cover checks ensure that the postcondition is reachable.
 //!
 //! ## Replace Function
 //!
@@ -169,13 +173,19 @@
 //!                                    || -> u32
 //!                                        {
 //!                                            kani::assume(divisor != 0);
+//!                                            kani::internal::contract_cover(divisor != 0, "The contract's precondition is satisfiable.");
 //!                                            let _wrapper_arg = ();
 //!                                            #[kanitool::is_contract_generated(wrapper)]
 //!                                            #[allow(dead_code, unused_variables, unused_mut)]
 //!                                            let mut __kani_modifies_div =
 //!                                                |_wrapper_arg| -> u32 { dividend / divisor };
 //!                                            let result_kani_internal: u32 =
 //!                                                __kani_modifies_div(_wrapper_arg);
+//!                                            kani::internal::contract_cover(
+//!                                                 kani::internal::apply_closure(|result: &u32|
+//!                                                     *result <= dividend,
+//!                                                     &result_kani_internal),
+//!                                                 "The contract's postcondition is reachable.");
 //!                                            kani::assert(kani::internal::apply_closure(|result: &u32|
 //!                                                        *result <= dividend, &result_kani_internal),
 //!                                                "|result : &u32| *result <= dividend");
@@ -211,13 +221,19 @@
 //!                 || -> u32
 //!                     {
 //!                         kani::assume(divisor != 0);
+//!                         kani::internal::contract_cover(divisor != 0, "The contract's precondition is satisfiable.");
 //!                         let _wrapper_arg = ();
 //!                         #[kanitool::is_contract_generated(wrapper)]
 //!                         #[allow(dead_code, unused_variables, unused_mut)]
 //!                         let mut __kani_modifies_div =
 //!                             |_wrapper_arg| -> u32 { dividend / divisor };
 //!                         let result_kani_internal: u32 =
 //!                             __kani_modifies_div(_wrapper_arg);
+//!                         kani::internal::contract_cover(
+//!                             kani::internal::apply_closure(|result: &u32|
+//!                                 *result <= dividend,
+//!                                 &result_kani_internal),
+//!                             "The contract's postcondition is reachable.");
 //!                         kani::assert(kani::internal::apply_closure(|result: &u32|
 //!                                     *result <= dividend, &result_kani_internal),
 //!                             "|result : &u32| *result <= dividend");
@@ -310,7 +326,8 @@
 //!                                let mut __kani_check_modify =
 //!                                    ||
 //!                                        {
-//!                                            kani::assume(*ptr < 100);
+//!                                            kani::assume(divisor != 0);
+//!                                            kani::internal::contract_cover(*ptr < 100, "The contract's precondition is satisfiable.");
 //!                                            let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
 //!                                            let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
 //!                                            let _wrapper_arg = (ptr as *const _,);
@@ -320,9 +337,21 @@
 //!                                                |_wrapper_arg| { *ptr += 1; };
 //!                                            let result_kani_internal: () =
 //!                                                __kani_modifies_modify(_wrapper_arg);
+//!                                            kani::internal::contract_cover(
+//!                                                kani::internal::apply_closure(|result|
+//!                                                    (remember_kani_internal_2e780b148d45b5c8) == * ptr,
+//!                                                    &result_kani_internal
+//!                                                ),
+//!                                            "The contract's postcondition is reachable.");
 //!                                            kani::assert(kani::internal::apply_closure(|result|
 //!                                                        (remember_kani_internal_92cc419d8aca576c) == *ptr,
 //!                                                    &result_kani_internal), "|result| old(*ptr + 1) == *ptr");
+//!                                            kani::internal::contract_cover(
+//!                                                kani::internal::apply_closure(|result|
+//!                                                    (remember_kani_internal_2e780b148d45b5c8) == * ptr,
+//!                                                    &result_kani_internal
+//!                                                ),
+//!                                            "The contract's postcondition is reachable.");
 //!                                            kani::assert(kani::internal::apply_closure(|result|
 //!                                                        (remember_kani_internal_92cc419d8aca576c) == *ptr,
 //!                                                    &result_kani_internal), "|result| old(*ptr + 1) == *ptr");
@@ -366,7 +395,6 @@
 //!             let mut __kani_check_modify =
 //!                 ||
 //!                     {
-//!                         kani::assume(*ptr < 100);
 //!                         let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
 //!                         let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
 //!                         let _wrapper_arg = (ptr as *const _,);
@@ -376,9 +404,19 @@
 //!                             |_wrapper_arg| { *ptr += 1; };
 //!                         let result_kani_internal: () =
 //!                             __kani_modifies_modify(_wrapper_arg);
+//!                         kani::internal::contract_cover(
+//!                            kani::internal::apply_closure(|result|
+//!                              (remember_kani_internal_2e780b148d45b5c8) == * ptr,
+//!                              &result_kani_internal
+//!                         ),
 //!                         kani::assert(kani::internal::apply_closure(|result|
 //!                                     (remember_kani_internal_92cc419d8aca576c) == *ptr,
 //!                                 &result_kani_internal), "|result| old(*ptr + 1) == *ptr");
+//!                         kani::internal::contract_cover(
+//!                            kani::internal::apply_closure(|result|
+//!                              (remember_kani_internal_2e780b148d45b5c8) == * ptr,
+//!                              &result_kani_internal
+//!                         ),
 //!                         kani::assert(kani::internal::apply_closure(|result|
 //!                                     (remember_kani_internal_92cc419d8aca576c) == *ptr,
 //!                                 &result_kani_internal), "|result| old(*ptr + 1) == *ptr");
@@ -550,5 +588,7 @@ fn contract_main(
         Err(e) => return e.into_compile_error().into(),
     };
 
-    handler.dispatch_on(function_state).into()
+    let res = handler.dispatch_on(function_state).into();
+    println!("{}", &res);
+    res
 }

tests/expected/function-contract/cover_contract/never_type.expected

@@ -0,0 +1,9 @@
+contract_cover.2\
+	 - Status: FAILURE\
+	 - Description: "The contract's postcondition is reachable."
+
+unwind.0\
+    - Status: FAILURE\
+    - Description: "unwinding assertion loop 0"
+
+VERIFICATION:- FAILED

tests/expected/function-contract/cover_contract/never_type_fixme.rs

@@ -0,0 +1,25 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// Unreachable postcondition because the function never returns.
+// Kani should fail verification because the postcondition is unreachable,
+// but currently doesn't generate the postcondition check at all
+// (although verification still fails because of the unwinding error).
+// We may need special never type detection for this case.
+
+#![feature(never_type)]
+
+#[kani::requires(true)]
+#[kani::ensures(|result: &!| true)]
+fn never_return() -> ! {
+    let x = 7;
+    loop {}
+}
+
+// Unreachable postcondition because the function never returns
+#[kani::proof_for_contract(never_return)]
+#[kani::unwind(5)]
+fn prove_never_return() {
+    never_return();
+}

tests/expected/function-contract/cover_contract/unreachable_postcondition.expected

@@ -0,0 +1,24 @@
+
+contract_cover.1\
+	 - Status: FAILURE\
+	 - Description: "The contract's postcondition is reachable."
+
+unwind.0\
+	 - Status: FAILURE\
+	 - Description: "unwinding assertion loop 0"
+
+VERIFICATION:- FAILED
+
+assertion.1\
+	 - Status: FAILURE\
+	 - Description: "panic"
+
+contract_cover.1\
+	 - Status: SUCCESS\
+	 - Description: "The contract's precondition is satisfiable."
+
+contract_cover.2\
+	 - Status: FAILURE\
+	 - Description: "The contract's postcondition is reachable."
+
+VERIFICATION:- FAILED