contract_cover

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

@@ -44,15 +44,13 @@ pub enum PropertyClass {
     ///
     /// SPECIAL BEHAVIOR: None? Possibly confusing to customers that a Rust assume is a Kani assert.
     Assume,
-    /// Same as `Assume`, but fails if the assumption would empty the search space.
-    /// E.g, imagine a previous assertion (x > 0) already exists. An assume(x < 0) would empty the search space
-    /// because there is no value of `x` for which both assertions are satisfiable.
-    /// We use this internally for contract instrumentation to ensure that preconditions do not empty the search space.
-    AssumeUnlessVacuous,
     /// See [GotocCtx::codegen_cover] below. Generally just an `assert(false)` that's not an error.
     ///
     /// 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.
     ///
@@ -155,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,10 +82,14 @@ impl GotocHook for Cover {
     }
 }
 
-struct Assume;
-impl GotocHook for Assume {
+/// 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, "KaniAssume")
+        matches_function(tcx, instance.def, "KaniContractCover")
     }
 
     fn handle(
@@ -97,19 +101,30 @@ impl GotocHook for Assume {
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
-        assert_eq!(fargs.len(), 1);
+        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 loc = gcx.codegen_span_stable(span);
+        let caller_loc = gcx.codegen_caller_span_stable(span);
 
-        Stmt::block(vec![gcx.codegen_assume(cond, loc), Stmt::goto(bb_label(target), loc)], loc)
+        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 AssumeUnlessVacuous;
-impl GotocHook for AssumeUnlessVacuous {
+struct Assume;
+impl GotocHook for Assume {
     fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
-        matches_function(tcx, instance.def, "KaniAssumeUnlessVacuous")
+        matches_function(tcx, instance.def, "KaniAssume")
     }
 
     fn handle(
@@ -121,21 +136,12 @@ impl GotocHook for AssumeUnlessVacuous {
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
-        assert_eq!(fargs.len(), 2);
+        assert_eq!(fargs.len(), 1);
         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 loc = gcx.codegen_span_stable(span);
 
-        Stmt::block(
-            vec![
-                gcx.codegen_assume(cond, loc),
-                Stmt::assert_false(PropertyClass::AssumeUnlessVacuous.as_str(), &msg, loc),
-                Stmt::goto(bb_label(target), loc),
-            ],
-            loc,
-        )
+        Stmt::block(vec![gcx.codegen_assume(cond, loc), Stmt::goto(bb_label(target), loc)], loc)
     }
 }
 
@@ -617,7 +623,7 @@ pub fn fn_hooks() -> GotocHooks {
         hooks: vec![
             Rc::new(Panic),
             Rc::new(Assume),
-            Rc::new(AssumeUnlessVacuous),
+            Rc::new(ContractCover),
             Rc::new(Assert),
             Rc::new(Check),
             Rc::new(Cover),

kani-driver/src/cbmc_output_parser.rs

@@ -95,17 +95,17 @@ pub struct PropertyId {
 }
 
 impl Property {
-    const ASSUME_UNLESS_VACUOUS_PROPERTY_CLASS: &'static str = "assume_unless_vacuous";
+    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 assume_unless_vacuous property
-    pub fn is_assume_unless_vacuous_property(&self) -> bool {
-        self.property_id.class == Self::ASSUME_UNLESS_VACUOUS_PROPERTY_CLASS
+    /// 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

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 {
@@ -648,10 +648,8 @@ fn update_results_of_code_covererage_checks(mut properties: Vec<Property>) -> Ve
 /// will be `CheckStatus::Unreachable` and not `CheckStatus::Success` since
 /// `update_properties_with_reach_status` is called beforehand
 ///
-/// We encode assume_unless_vacuous(cond) as assume(cond); assert(false).
-/// `is_assume_unless_vacuous_property` corresponds to the assert(false).
-/// If this assertion fails as expected, the assume did not empty the search space,
-/// so succeed; otherwise, fail.
+/// 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() {
@@ -660,8 +658,11 @@ 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_assume_unless_vacuous_property() {
-            if prop.status == CheckStatus::Success {
+        } 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;

library/kani_core/src/lib.rs

@@ -347,24 +347,12 @@ macro_rules! kani_intrinsics {
             }
 
             /// This function is only used for function contract instrumentation.
-            /// It is the same as assume(), but it adds an extra assert(false) afterward.
-            /// The CBMC output parser uses this assertion as a reachability check;
-            /// if the assertion is unreachable or succeeds, then we know that the assumption emptied the search space.
+            /// 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 = "KaniAssumeUnlessVacuous"]
-            #[cfg(not(feature = "concrete_playback"))]
+            #[rustc_diagnostic_item = "KaniContractCover"]
             #[doc(hidden)]
-            pub fn assume_unless_vacuous(cond: bool, msg: &'static str) {
-                let _ = cond;
-            }
-
-            #[inline(never)]
-            #[rustc_diagnostic_item = "KaniAssumeUnlessVacuous"]
-            #[cfg(feature = "concrete_playback")]
-            #[doc(hidden)]
-            pub fn assume_unless_vacuous(cond: bool, msg: &'static str) {
-                assert!(cond, "{}", msg);
-            }
+            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.

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

@@ -24,7 +24,8 @@ impl<'a> ContractConditionsHandler<'a> {
         match &self.condition_type {
             ContractConditionsData::Requires { attr } => {
                 quote!({
-                    kani::internal::assume_unless_vacuous(#attr, "The contract's precondition (i.e., the conjunction of the #[requires(...)] clauses' bodies) is satisfiable.");
+                    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/helpers.rs

@@ -201,20 +201,17 @@ pub fn split_for_remembers(stmts: &[Stmt], closure_type: ClosureType) -> (&[Stmt
     let mut pos = 0;
 
     let check_str = match closure_type {
-        ClosureType::Check => "kani::internal::assume_unless_vacuous",
-        ClosureType::Replace => "kani::assert",
+        ClosureType::Check => "assume",
+        ClosureType::Replace => "assert",
     };
 
     for stmt in stmts {
         if let Stmt::Expr(Expr::Call(ExprCall { func, .. }), _) = stmt {
             if let Expr::Path(ExprPath { path: Path { segments, .. }, .. }) = func.as_ref() {
-                let first_three_idents = segments
-                    .iter()
-                    .take(3)
-                    .map(|sgmt| sgmt.ident.to_string())
-                    .collect::<Vec<_>>()
-                    .join("::");
-                if first_three_idents.contains(check_str) {
+                let first_two_idents =
+                    segments.iter().take(2).map(|sgmt| sgmt.ident.to_string()).collect::<Vec<_>>();
+
+                if first_two_idents == vec!["kani", check_str] {
                     pos += 1;
                 }
             }

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
 //!
@@ -168,14 +172,20 @@
 //!                                let mut __kani_check_div =
 //!                                    || -> u32
 //!                                        {
-//!                                            kani::internal::assume_unless_vacuous(divisor != 0);
+//!                                            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");
@@ -210,14 +220,20 @@
 //!             let mut __kani_check_div =
 //!                 || -> u32
 //!                     {
-//!                         kani::internal::assume_unless_vacuous(divisor != 0);
+//!                         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::internal::assume_unless_vacuous(divisor != 0);
+//!                                            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");
@@ -375,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");
@@ -549,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
 }