Fail verification if contract is vacuous

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

@@ -44,6 +44,11 @@ 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.

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

@@ -106,6 +106,39 @@ impl GotocHook for Assume {
     }
 }
 
+struct AssumeUnlessVacuous;
+impl GotocHook for AssumeUnlessVacuous {
+    fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
+        matches_function(tcx, instance.def, "KaniAssumeUnlessVacuous")
+    }
+
+    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 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,
+        )
+    }
+}
+
 struct Assert;
 impl GotocHook for Assert {
     fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
@@ -584,6 +617,7 @@ pub fn fn_hooks() -> GotocHooks {
         hooks: vec![
             Rc::new(Panic),
             Rc::new(Assume),
+            Rc::new(AssumeUnlessVacuous),
             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 ASSUME_UNLESS_VACUOUS_PROPERTY_CLASS: &'static str = "assume_unless_vacuous";
     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 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

@@ -647,6 +647,11 @@ 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
+///
+/// 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.
 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 +660,12 @@ 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::Unreachable || prop.status == CheckStatus::Success {
+                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,26 @@ 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.
+            #[inline(never)]
+            #[rustc_diagnostic_item = "KaniAssumeUnlessVacuous"]
+            #[cfg(not(feature = "concrete_playback"))]
+            #[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);
+            }
+
             /// A way to break the ownerhip rules. Only used by contracts where we can
             /// guarantee it is done safely.
             #[inline(never)]
@@ -383,7 +403,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

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

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

@@ -201,17 +201,20 @@ pub fn split_for_remembers(stmts: &[Stmt], closure_type: ClosureType) -> (&[Stmt
     let mut pos = 0;
 
     let check_str = match closure_type {
-        ClosureType::Check => "assume",
-        ClosureType::Replace => "assert",
+        ClosureType::Check => "kani::internal::assume_unless_vacuous",
+        ClosureType::Replace => "kani::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_two_idents =
-                    segments.iter().take(2).map(|sgmt| sgmt.ident.to_string()).collect::<Vec<_>>();
-
-                if first_two_idents == vec!["kani", check_str] {
+                let first_three_idents = segments
+                    .iter()
+                    .take(3)
+                    .map(|sgmt| sgmt.ident.to_string())
+                    .collect::<Vec<_>>()
+                    .join("::");
+                if first_three_idents.contains(check_str) {
                     pos += 1;
                 }
             }

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

@@ -168,7 +168,7 @@
 //!                                let mut __kani_check_div =
 //!                                    || -> u32
 //!                                        {
-//!                                            kani::assume(divisor != 0);
+//!                                            kani::internal::assume_unless_vacuous(divisor != 0);
 //!                                            let _wrapper_arg = ();
 //!                                            #[kanitool::is_contract_generated(wrapper)]
 //!                                            #[allow(dead_code, unused_variables, unused_mut)]
@@ -210,7 +210,7 @@
 //!             let mut __kani_check_div =
 //!                 || -> u32
 //!                     {
-//!                         kani::assume(divisor != 0);
+//!                         kani::internal::assume_unless_vacuous(divisor != 0);
 //!                         let _wrapper_arg = ();
 //!                         #[kanitool::is_contract_generated(wrapper)]
 //!                         #[allow(dead_code, unused_variables, unused_mut)]
@@ -310,7 +310,7 @@
 //!                                let mut __kani_check_modify =
 //!                                    ||
 //!                                        {
-//!                                            kani::assume(*ptr < 100);
+//!                                            kani::internal::assume_unless_vacuous(divisor != 0);
 //!                                            let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
 //!                                            let remember_kani_internal_92cc419d8aca576c = *ptr + 1;
 //!                                            let _wrapper_arg = (ptr as *const _,);
@@ -366,7 +366,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 _,);

tests/expected/function-contract/vacuous_requires_fail.expected

@@ -0,0 +1,5 @@
+Failed Checks: The contract's precondition (i.e., the conjunction of the #[requires(...)] clauses' bodies) is satisfiable.
+
+VERIFICATION:- FAILED
+
+Verification failed for - prove_buggy

tests/expected/function-contract/vacuous_requires_fail.rs

@@ -0,0 +1,17 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Zfunction-contracts
+
+// See https://github.com/model-checking/kani/issues/2793
+#[kani::requires(a > 5)]
+#[kani::requires(a < 4)]
+#[kani::ensures(|result| *result == a)]
+fn buggy(a: u32) -> u32 {
+    panic!("This code is never tested")
+}
+
+#[kani::proof_for_contract(buggy)]
+fn prove_buggy() {
+    let x: u32 = kani::any();
+    buggy(x);
+}

tests/expected/function-contract/valid_ptr.expected

@@ -1,10 +1,17 @@
 Checking harness pre_condition::harness_invalid_ptr...
-VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected)
+assume_unless_vacuous\
+	 - Status: FAILURE
+VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected)
 
 Checking harness pre_condition::harness_stack_ptr...
 VERIFICATION:- SUCCESSFUL
 
 Checking harness pre_condition::harness_head_ptr...
 VERIFICATION:- SUCCESSFUL
 
-Complete - 3 successfully verified harnesses, 0 failures, 3 total
+Checking harness post_condition::harness...
+assume_unless_vacuous\
+	 - Status: FAILURE
+VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected)
+
+Complete - 2 successfully verified harnesses, 2 failures, 4 total

tests/expected/function-contract/valid_ptr.rs

@@ -35,12 +35,9 @@ mod pre_condition {
     }
 }
 
-/// TODO: Enable once we fix: <https://github.com/model-checking/kani/issues/2997>
-#[cfg(not_supported)]
 mod post_condition {
-
     /// This contract should fail since we are creating a dangling pointer.
-    #[kani::ensures(kani::mem::can_dereference(result.0))]
+    #[kani::ensures(|result| kani::mem::can_dereference((*result).0))]
     unsafe fn new_invalid_ptr() -> PtrWrapper<char> {
         let var = 'c';
         PtrWrapper(&var as *const _)