Adjust PropertyClass of assertions to identify UB

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

@@ -251,19 +251,25 @@ impl GotocCtx<'_> {
                     if *expected { r } else { Expr::not(r) }
                 };
 
-                let msg = if let AssertMessage::BoundsCheck { .. } = msg {
+                let (msg, property_class) = if let AssertMessage::BoundsCheck { .. } = msg {
                     // For bounds check the following panic message is generated at runtime:
                     // "index out of bounds: the length is {len} but the index is {index}",
                     // but CBMC only accepts static messages so we don't add values to the message.
-                    "index out of bounds: the length is less than or equal to the given index"
+                    (
+                        "index out of bounds: the length is less than or equal to the given index",
+                        PropertyClass::Assertion,
+                    )
                 } else if let AssertMessage::MisalignedPointerDereference { .. } = msg {
                     // Misaligned pointer dereference check messages is also a runtime messages.
                     // Generate a generic one here.
-                    "misaligned pointer dereference: address must be a multiple of its type's \
-                    alignment"
+                    (
+                        "misaligned pointer dereference: address must be a multiple of its type's \
+                    alignment",
+                        PropertyClass::SafetyCheck,
+                    )
                 } else {
                     // For all other assert kind we can get the static message.
-                    msg.description().unwrap()
+                    (msg.description().unwrap(), PropertyClass::Assertion)
                 };
 
                 let (msg_str, reach_stmt) =
@@ -274,7 +280,7 @@ impl GotocCtx<'_> {
                         reach_stmt,
                         self.codegen_assert_assume(
                             cond.cast_to(Type::bool()),
-                            PropertyClass::Assertion,
+                            property_class,
                             &msg_str,
                             loc,
                         ),

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

@@ -160,24 +160,25 @@ impl GotocHook for UnsupportedCheck {
         target: Option<BasicBlockIdx>,
         span: Span,
     ) -> Stmt {
-        assert_eq!(fargs.len(), 2);
+        assert_eq!(fargs.len(), 1);
         let msg = fargs.pop().unwrap();
-        let cond = fargs.pop().unwrap().cast_to(Type::bool());
         let msg = gcx.extract_const_message(&msg).unwrap();
-        let target = target.unwrap();
         let caller_loc = gcx.codegen_caller_span_stable(span);
-        Stmt::block(
-            vec![
-                gcx.codegen_assert_assume(
-                    cond,
-                    PropertyClass::UnsupportedConstruct,
-                    &msg,
-                    caller_loc,
-                ),
-                Stmt::goto(bb_label(target), caller_loc),
-            ],
-            caller_loc,
-        )
+        if let Some(target) = target {
+            Stmt::block(
+                vec![
+                    gcx.codegen_assert_assume_false(
+                        PropertyClass::UnsupportedConstruct,
+                        &msg,
+                        caller_loc,
+                    ),
+                    Stmt::goto(bb_label(target), caller_loc),
+                ],
+                caller_loc,
+            )
+        } else {
+            gcx.codegen_assert_assume_false(PropertyClass::UnsupportedConstruct, &msg, caller_loc)
+        }
     }
 }
 

library/kani_core/src/mem.rs

@@ -210,10 +210,11 @@ macro_rules! kani_mem {
                 // stubbed.
                 // We first assert that the data_ptr
                 let data_ptr = ptr as *const ();
-                super::assert(
-                    unsafe { is_allocated(data_ptr, 0) },
-                    "Kani does not support reasoning about pointer to unallocated memory",
-                );
+                if !unsafe { is_allocated(data_ptr, 0) } {
+                    crate::kani::unsupported(
+                        "Kani does not support reasoning about pointer to unallocated memory",
+                    );
+                }
                 unsafe { is_allocated(data_ptr, sz) }
             }
         }
@@ -280,11 +281,11 @@ macro_rules! kani_mem {
             pub fn same_allocation(addr1: *const (), addr2: *const ()) -> bool {
                 let obj1 = crate::kani::mem::pointer_object(addr1);
                 (obj1 == crate::kani::mem::pointer_object(addr2)) && {
-                    // TODO(3571): This should be a unsupported check
-                    crate::kani::assert(
-                        unsafe { is_allocated(addr1, 0) || is_allocated(addr2, 0) },
-                        "Kani does not support reasoning about pointer to unallocated memory",
-                    );
+                    if !unsafe { is_allocated(addr1, 0) || is_allocated(addr2, 0) } {
+                        crate::kani::unsupported(
+                            "Kani does not support reasoning about pointer to unallocated memory",
+                        );
+                    }
                     unsafe { is_allocated(addr1, 0) && is_allocated(addr2, 0) }
                 }
             }

tests/expected/MemPredicates/adt_with_metadata.expected

@@ -0,0 +1,4 @@
+Failed Checks: Kani does not support reasoning about pointer to unallocated memory
+
+Verification failed for - invalid_access::check_invalid_dyn_ptr
+Complete - 3 successfully verified harnesses, 1 failures, 4 total.

tests/kani/MemPredicates/adt_with_metadata.rs → tests/expected/MemPredicates/adt_with_metadata.rs

@@ -42,7 +42,6 @@ mod invalid_access {
     use super::*;
     use std::ptr;
     #[kani::proof]
-    #[kani::should_panic]
     pub fn check_invalid_dyn_ptr() {
         unsafe fn new_dead_ptr<T>(val: T) -> *const T {
             let local = val;

tests/expected/MemPredicates/fat_ptr_validity.expected

@@ -0,0 +1,5 @@
+Failed Checks: Kani does not support reasoning about pointer to unallocated memory
+
+Verification failed for - invalid_access::check_invalid_slice_ptr
+Verification failed for - invalid_access::check_invalid_dyn_ptr
+Complete - 4 successfully verified harnesses, 2 failures, 6 total.

tests/kani/MemPredicates/fat_ptr_validity.rs → tests/expected/MemPredicates/fat_ptr_validity.rs

@@ -38,14 +38,12 @@ mod valid_access {
 mod invalid_access {
     use super::*;
     #[kani::proof]
-    #[kani::should_panic]
     pub fn check_invalid_dyn_ptr() {
         let raw_ptr: *const dyn PartialEq<u8> = unsafe { new_dead_ptr::<u8>(0) };
         assert!(can_dereference(raw_ptr));
     }
 
     #[kani::proof]
-    #[kani::should_panic]
     pub fn check_invalid_slice_ptr() {
         let raw_ptr: *const [char] = unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) };
         assert!(can_dereference(raw_ptr));

tests/expected/MemPredicates/thin_ptr_validity.expected

@@ -0,0 +1,5 @@
+Failed Checks: Kani does not support reasoning about pointer to unallocated memory
+
+Verification failed for - invalid_access::check_invalid_array
+Verification failed for - invalid_access::check_invalid_ptr
+Complete - 3 successfully verified harnesses, 2 failures, 5 total.

tests/kani/MemPredicates/thin_ptr_validity.rs → tests/expected/MemPredicates/thin_ptr_validity.rs

@@ -32,14 +32,12 @@ mod valid_access {
 mod invalid_access {
     use super::*;
     #[kani::proof]
-    #[kani::should_panic]
     pub fn check_invalid_ptr() {
         let raw_ptr = unsafe { new_dead_ptr::<u8>(0) };
         assert!(!can_dereference(raw_ptr));
     }
 
     #[kani::proof]
-    #[kani::should_panic]
     pub fn check_invalid_array() {
         let raw_ptr = unsafe { new_dead_ptr::<[char; 2]>(['a', 'b']) };
         assert!(can_dereference(raw_ptr));

tests/expected/issue-3571/issue_3571.expected

@@ -0,0 +1,2 @@
+VERIFICATION:- FAILED (encountered failures other than panics, which were unexpected)
+Complete - 0 successfully verified harnesses, 2 failures, 2 total.

tests/expected/issue-3571/issue_3571.rs

@@ -0,0 +1,16 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+
+#[kani::proof]
+#[kani::should_panic]
+pub fn rust_ub_fails() {
+    let ptr = 0 as *const u32;
+    let _invalid_ref = unsafe { &*ptr };
+}
+
+#[kani::proof]
+#[kani::should_panic]
+pub fn rust_ub_should_fail() {
+    let ptr = 10 as *const u32;
+    let _invalid_read = unsafe { *ptr };
+}

tests/expected/uninit/multiple-instrumentations.expected

@@ -1,16 +1,16 @@
-multiple_instrumentations_different_vars.assertion.3\
+multiple_instrumentations_different_vars.assertion.1\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-multiple_instrumentations_different_vars.assertion.4\
+multiple_instrumentations_different_vars.assertion.2\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u64`"
 
-multiple_instrumentations.assertion.2\
+multiple_instrumentations.assertion.1\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"
 
-multiple_instrumentations.assertion.3\
+multiple_instrumentations.assertion.2\
 	 - Status: FAILURE\
 	 - Description: "Undefined Behavior: Reading from an uninitialized pointer of type `u128`"