From 756d93871080bea886eee22604ba1a87064e1b2e Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 28 Jan 2025 13:09:24 +0000 Subject: [PATCH] Adjust PropertyClass of assertions to identify UB Anything listed as undefined behavior (UB) at https://doc.rust-lang.org/reference/behavior-considered-undefined.html must also be considered UB by Kani and should not pass under `should_fail`. In preparation of this PR, all occurrences of `PropertyClass` in the code base were audited and, where necessary, adjusted. Also, all uses of `kani::assert` were audited to confirm or adjust them. This resulted in first-time use of the `UnsupportedCheck` hook, which implied fixes to its implementation. Resolves: #3571 --- .../codegen/statement.rs | 18 +++++++---- .../codegen_cprover_gotoc/overrides/hooks.rs | 31 ++++++++++--------- library/kani_core/src/mem.rs | 19 ++++++------ .../adt_with_metadata.rs | 1 - .../fat_ptr_validity.rs | 2 -- tests/expected/issue-3571/issue_3571.expected | 2 ++ tests/expected/issue-3571/issue_3571.rs | 13 ++++++++ .../thin_ptr_validity.rs | 2 -- .../uninit/multiple-instrumentations.expected | 8 ++--- 9 files changed, 57 insertions(+), 39 deletions(-) rename tests/{kani/MemPredicates => expected}/adt_with_metadata.rs (98%) rename tests/{kani/MemPredicates => expected}/fat_ptr_validity.rs (97%) create mode 100644 tests/expected/issue-3571/issue_3571.expected create mode 100644 tests/expected/issue-3571/issue_3571.rs rename tests/{kani/MemPredicates => expected}/thin_ptr_validity.rs (96%) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs index 90635a71f2e8..ed7030f5087d 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/statement.rs +++ b/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, ), diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 73c887b3eeaf..c346b60023aa 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -160,24 +160,25 @@ impl GotocHook for UnsupportedCheck { target: Option, 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) + } } } diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index c09d67ca51ff..fb1f1463df6f 100644 --- a/library/kani_core/src/mem.rs +++ b/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) } } } diff --git a/tests/kani/MemPredicates/adt_with_metadata.rs b/tests/expected/adt_with_metadata.rs similarity index 98% rename from tests/kani/MemPredicates/adt_with_metadata.rs rename to tests/expected/adt_with_metadata.rs index aa536b26279f..9ec0a3787964 100644 --- a/tests/kani/MemPredicates/adt_with_metadata.rs +++ b/tests/expected/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(val: T) -> *const T { let local = val; diff --git a/tests/kani/MemPredicates/fat_ptr_validity.rs b/tests/expected/fat_ptr_validity.rs similarity index 97% rename from tests/kani/MemPredicates/fat_ptr_validity.rs rename to tests/expected/fat_ptr_validity.rs index c4f037f3a646..f39392b62c5c 100644 --- a/tests/kani/MemPredicates/fat_ptr_validity.rs +++ b/tests/expected/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 = unsafe { new_dead_ptr::(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)); diff --git a/tests/expected/issue-3571/issue_3571.expected b/tests/expected/issue-3571/issue_3571.expected new file mode 100644 index 000000000000..84191346398c --- /dev/null +++ b/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. diff --git a/tests/expected/issue-3571/issue_3571.rs b/tests/expected/issue-3571/issue_3571.rs new file mode 100644 index 000000000000..5fc1871f0415 --- /dev/null +++ b/tests/expected/issue-3571/issue_3571.rs @@ -0,0 +1,13 @@ +#[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 }; +} diff --git a/tests/kani/MemPredicates/thin_ptr_validity.rs b/tests/expected/thin_ptr_validity.rs similarity index 96% rename from tests/kani/MemPredicates/thin_ptr_validity.rs rename to tests/expected/thin_ptr_validity.rs index 553c5beab9f8..519a07297192 100644 --- a/tests/kani/MemPredicates/thin_ptr_validity.rs +++ b/tests/expected/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::(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)); diff --git a/tests/expected/uninit/multiple-instrumentations.expected b/tests/expected/uninit/multiple-instrumentations.expected index 153024dc692b..413314d8d72e 100644 --- a/tests/expected/uninit/multiple-instrumentations.expected +++ b/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`"