diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index 72ccb95cf97b..c81d60e40d42 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -23,10 +23,12 @@ use cbmc::goto_program::{Expr, Location, Stmt, Type}; use cbmc::InternedString; use rustc_middle::mir::coverage::SourceRegion; use stable_mir::mir::{Place, ProjectionElem}; -use stable_mir::ty::{Span as SpanStable, TypeAndMut}; +use stable_mir::ty::{Span as SpanStable, Ty}; use strum_macros::{AsRefStr, EnumString}; use tracing::debug; +use super::intrinsic::SizeAlign; + /// Classifies the type of CBMC `assert`, as different assertions can have different semantics (e.g. cover) /// /// Each property class should justify its existence with a note about the special handling it recieves. @@ -333,8 +335,10 @@ impl<'tcx> GotocCtx<'tcx> { pub fn codegen_raw_ptr_deref_validity_check( &mut self, place: &Place, + place_ref: Expr, + place_ref_ty: Ty, loc: &Location, - ) -> Option { + ) -> Option<(Stmt, Stmt)> { if let Some(ProjectionElem::Deref) = place.projection.last() { // Create a place without the topmost dereference projection.ß let ptr_place = { @@ -346,41 +350,42 @@ impl<'tcx> GotocCtx<'tcx> { let ptr_place_ty = self.place_ty_stable(&ptr_place); if ptr_place_ty.kind().is_raw_ptr() { // Extract the size of the pointee. - let pointee_size = { - let TypeAndMut { ty: pointee_ty, .. } = - ptr_place_ty.kind().builtin_deref(true).unwrap(); - let pointee_ty_layout = pointee_ty.layout().unwrap(); - pointee_ty_layout.shape().size.bytes() + let SizeAlign { size: sz, align } = + self.size_and_align_of_dst(place_ref_ty, place_ref); + + // Encode __CPROVER_r_ok(ptr, size). + // First, generate a CBMC expression representing the pointer. + let ptr = { + let ptr_projection = self.codegen_place_stable(&ptr_place, *loc).unwrap(); + let place_ty = self.place_ty_stable(place); + if self.use_thin_pointer_stable(place_ty) { + ptr_projection.goto_expr().clone() + } else { + ptr_projection.goto_expr().clone().member("data", &self.symbol_table) + } }; + // Then generate an alignment check + let align_ok = + ptr.clone().cast_to(Type::size_t()).rem(align).eq(Type::size_t().zero()); + let align_check = self.codegen_assert_assume(align_ok, PropertyClass::SafetyCheck, + "misaligned pointer to reference cast: address must be a multiple of its type's \ + alignment", *loc); + // Then, generate a __CPROVER_r_ok check. + let raw_ptr_read_ok_expr = + Expr::read_ok(ptr.cast_to(Type::void_pointer()), sz.clone()) + .cast_to(Type::Bool); // __CPROVER_r_ok fails if size == 0, so need to explicitly avoid the check. - if pointee_size != 0 { - // Encode __CPROVER_r_ok(ptr, size). - // First, generate a CBMC expression representing the pointer. - let ptr = { - let ptr_projection = self.codegen_place_stable(&ptr_place, *loc).unwrap(); - let place_ty = self.place_ty_stable(place); - if self.use_thin_pointer_stable(place_ty) { - ptr_projection.goto_expr().clone() - } else { - ptr_projection.goto_expr().clone().member("data", &self.symbol_table) - } - }; - // Then, generate a __CPROVER_r_ok check. - let raw_ptr_read_ok_expr = Expr::read_ok( - ptr.cast_to(Type::void_pointer()), - Expr::int_constant(pointee_size, Type::size_t()), - ) - .cast_to(Type::Bool); - // Finally, assert that the pointer points to a valid memory location. - let raw_ptr_read_ok = self.codegen_assert( - raw_ptr_read_ok_expr, - PropertyClass::SafetyCheck, - "dereference failure: pointer invalid", - *loc, - ); - return Some(raw_ptr_read_ok); - } + let sz_typ = sz.typ().clone(); + let raw_ptr_read_ok_expr = sz.eq(sz_typ.zero()).or(raw_ptr_read_ok_expr); + // Finally, assert that the pointer points to a valid memory location. + let raw_ptr_read_ok = self.codegen_assert( + raw_ptr_read_ok_expr, + PropertyClass::SafetyCheck, + "dereference failure: pointer invalid", + *loc, + ); + return Some((align_check, raw_ptr_read_ok)); } } None diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 421d79e943c4..1b4c0174d5ed 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -18,9 +18,9 @@ use stable_mir::mir::{BasicBlockIdx, Operand, Place}; use stable_mir::ty::{GenericArgs, RigidTy, Span, Ty, TyKind, UintTy}; use tracing::debug; -struct SizeAlign { - size: Expr, - align: Expr, +pub struct SizeAlign { + pub size: Expr, + pub align: Expr, } enum VTableInfo { @@ -1291,7 +1291,7 @@ impl<'tcx> GotocCtx<'tcx> { /// This function computes the size and alignment of a dynamically-sized type. /// The implementations follows closely the SSA implementation found in /// `rustc_codegen_ssa::glue::size_and_align_of_dst`. - fn size_and_align_of_dst(&mut self, ty: Ty, arg: Expr) -> SizeAlign { + pub fn size_and_align_of_dst(&mut self, ty: Ty, arg: Expr) -> SizeAlign { let layout = self.layout_of_stable(ty); let usizet = Type::size_t(); if !layout.is_unsized() { diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index e8f1424f09a3..7abd949357ff 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -738,12 +738,23 @@ impl<'tcx> GotocCtx<'tcx> { Rvalue::Ref(_, _, p) | Rvalue::AddressOf(_, p) => { let place_ref = self.codegen_place_ref_stable(&p, loc); let place_ref_type = place_ref.typ().clone(); - match self.codegen_raw_ptr_deref_validity_check(&p, &loc) { - Some(ptr_validity_check_expr) => Expr::statement_expression( - vec![ptr_validity_check_expr, place_ref.as_stmt(loc)], - place_ref_type, - loc, - ), + match self.codegen_raw_ptr_deref_validity_check( + &p, + place_ref.clone(), + self.place_ty_stable(p), + &loc, + ) { + Some((ptr_alignment_check_expr, ptr_validity_check_expr)) => { + Expr::statement_expression( + vec![ + ptr_alignment_check_expr, + ptr_validity_check_expr, + place_ref.as_stmt(loc), + ], + place_ref_type, + loc, + ) + } None => place_ref, } } diff --git a/tests/expected/ptr_to_ref_cast/alignment/expected b/tests/expected/ptr_to_ref_cast/alignment/expected new file mode 100644 index 000000000000..c7d8f5109e21 --- /dev/null +++ b/tests/expected/ptr_to_ref_cast/alignment/expected @@ -0,0 +1,4 @@ +check_misaligned_ptr_cast_fail.safety_check\ +Status: FAILURE\ +Description: "misaligned pointer to reference cast: address must be a multiple of its type's alignment"\ +in function check_misaligned_ptr_cast_fail diff --git a/tests/expected/ptr_to_ref_cast/alignment/test.rs b/tests/expected/ptr_to_ref_cast/alignment/test.rs new file mode 100644 index 000000000000..5e0a18a79da7 --- /dev/null +++ b/tests/expected/ptr_to_ref_cast/alignment/test.rs @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test checks that Kani detects UB resulting from converting a raw +//! pointer to a reference when the pointer is not properly aligned. + +#[repr(align(4))] +#[derive(Clone, Copy)] +struct AlignedI32(i32); + +#[kani::proof] +fn check_misaligned_ptr_cast_fail() { + let data = AlignedI32(42); + let ptr = &data as *const AlignedI32; + + unsafe { + let misaligned = ptr.byte_add(1); + let x = unsafe { &*misaligned }; + } +} diff --git a/tests/expected/ptr_to_ref_cast/invalid/expected b/tests/expected/ptr_to_ref_cast/invalid/expected new file mode 100644 index 000000000000..df4b8143d2aa --- /dev/null +++ b/tests/expected/ptr_to_ref_cast/invalid/expected @@ -0,0 +1,8 @@ +MyStr::new.safety_check\ +Status: FAILURE\ +Description: "dereference failure: pointer invalid"\ +in function MyStr::new + +Verification failed for - check_size_of_val +Verification failed for - check_slice_my_str +Complete - 1 successfully verified harnesses, 2 failures, 3 total. diff --git a/tests/expected/ptr_to_ref_cast/invalid/test.rs b/tests/expected/ptr_to_ref_cast/invalid/test.rs new file mode 100644 index 000000000000..50d2c8dd05e8 --- /dev/null +++ b/tests/expected/ptr_to_ref_cast/invalid/test.rs @@ -0,0 +1,58 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test case checks the usage of slices of slices (&[&[T]]). +use std::mem::size_of_val; + +/// Structure with a raw string (i.e.: [char]). +struct MyStr { + header: u16, + data: str, +} + +impl MyStr { + /// This creates a MyStr from a byte slice. + fn new(original: &mut String) -> &mut Self { + let buf = original.get_mut(..).unwrap(); + assert!(size_of_val(buf) > 2, "This requires at least 2 bytes"); + let unsized_len = buf.len() - 2; + let ptr = std::ptr::slice_from_raw_parts_mut(buf.as_mut_ptr(), unsized_len); + unsafe { &mut *(ptr as *mut Self) } + } +} + +#[kani::proof] +fn sanity_check_my_str() { + let mut buf = String::from("123456"); + let my_str = MyStr::new(&mut buf); + my_str.header = 0; + + assert_eq!(size_of_val(my_str), 6); + assert_eq!(my_str.data.len(), 4); + assert_eq!(my_str.data.chars().nth(0), Some('3')); + assert_eq!(my_str.data.chars().nth(3), Some('6')); +} + +#[kani::proof] +fn check_slice_my_str() { + let mut buf_0 = String::from("000"); + let mut buf_1 = String::from("001"); + let my_slice = &[MyStr::new(&mut buf_0), MyStr::new(&mut buf_1)]; + assert_eq!(my_slice.len(), 2); + + assert_eq!(my_slice[0].data.len(), 1); + assert_eq!(my_slice[1].data.len(), 1); + + assert_eq!(my_slice[0].data.chars().nth(0), Some('0')); + assert_eq!(my_slice[1].data.chars().nth(0), Some('1')); +} + +#[kani::proof] +fn check_size_of_val() { + let mut buf_0 = String::from("000"); + let mut buf_1 = String::from("001"); + let my_slice = &[MyStr::new(&mut buf_0), MyStr::new(&mut buf_1)]; + assert_eq!(size_of_val(my_slice), 32); // Slice of 2 fat pointers. + assert_eq!(size_of_val(my_slice[0]), 4); // Size of a fat pointer. + assert_eq!(size_of_val(&my_slice[0].data), 1); // Size of str. +} diff --git a/tests/expected/ptr_to_ref_cast/slice/expected b/tests/expected/ptr_to_ref_cast/slice/expected new file mode 100644 index 000000000000..8a8b39f8594e --- /dev/null +++ b/tests/expected/ptr_to_ref_cast/slice/expected @@ -0,0 +1,6 @@ +Status: FAILURE\ +Description: "dereference failure: pointer invalid"\ + +Verification failed for - check_with_byte_add_fail +Verification failed for - check_with_metadata_fail +Complete - 1 successfully verified harnesses, 2 failures, 3 total. diff --git a/tests/expected/ptr_to_ref_cast/slice/test.rs b/tests/expected/ptr_to_ref_cast/slice/test.rs new file mode 100644 index 000000000000..8526d0bf1c7f --- /dev/null +++ b/tests/expected/ptr_to_ref_cast/slice/test.rs @@ -0,0 +1,36 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +#![feature(set_ptr_value)] + +//! This test checks that Kani detects UB resulting from converting a raw +//! pointer to a reference when the metadata is not valid. + +// Generate invalid fat pointer by combining the metadata. +#[kani::proof] +fn check_with_metadata_fail() { + let short = [0u32; 2]; + let long = [0u32; 10]; + let ptr = &short as *const [u32]; + // This should trigger UB since the slice is not valid for the new length. + let fake_long = unsafe { &*ptr.with_metadata_of(&long) }; + assert_eq!(fake_long.len(), long.len()); +} + +#[kani::proof] +fn check_with_byte_add_fail() { + let data = [5u8; 5]; + let ptr = &data as *const [u8]; + // This should trigger UB since the metadata does not get adjusted. + let val = unsafe { &*ptr.byte_add(1) }; + assert_eq!(val.len(), data.len()); +} + +#[kani::proof] +fn check_with_byte_add_sub_pass() { + let data = [5u8; 5]; + let ptr = &data as *const [u8]; + let offset = kani::any_where(|i| *i < 100); + // This should pass since the resulting metadata is valid + let val = unsafe { &*ptr.byte_add(offset).byte_sub(offset) }; + assert_eq!(val.len(), data.len()); +} diff --git a/tests/expected/ptr_to_ref_cast/str/expected b/tests/expected/ptr_to_ref_cast/str/expected new file mode 100644 index 000000000000..e2de069eb399 --- /dev/null +++ b/tests/expected/ptr_to_ref_cast/str/expected @@ -0,0 +1,5 @@ +Status: FAILURE\ +Description: "dereference failure: pointer invalid"\ + +VERIFICATION:- FAILED +Verification failed for - check_with_metadata_fail diff --git a/tests/expected/ptr_to_ref_cast/str/test.rs b/tests/expected/ptr_to_ref_cast/str/test.rs new file mode 100644 index 000000000000..137034e34327 --- /dev/null +++ b/tests/expected/ptr_to_ref_cast/str/test.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +#![feature(set_ptr_value)] + +//! This test checks that Kani detects UB resulting from converting a raw +//! pointer to a reference when the metadata is not valid. + +#[kani::proof] +fn check_with_metadata_fail() { + let short = "sh"; + let long = "longer"; + let ptr = short as *const str; + // This should trigger UB since the slice is not valid for the new length. + let fake_long = unsafe { &*ptr.with_metadata_of(long) }; + assert_eq!(fake_long.len(), long.len()); +} diff --git a/tests/kani/Projection/slice_slice_projection.rs b/tests/kani/Projection/slice_slice_projection.rs index 6e1cf42af4e7..6bfa62c2f6df 100644 --- a/tests/kani/Projection/slice_slice_projection.rs +++ b/tests/kani/Projection/slice_slice_projection.rs @@ -7,7 +7,8 @@ use std::mem::size_of_val; /// Structure with a raw string (i.e.: [char]). struct MyStr { - header: u16, + header_0: u8, + header_1: u8, data: str, } @@ -26,7 +27,6 @@ impl MyStr { fn sanity_check_my_str() { let mut buf = String::from("123456"); let my_str = MyStr::new(&mut buf); - my_str.header = 0; assert_eq!(size_of_val(my_str), 6); assert_eq!(my_str.data.len(), 4); @@ -54,6 +54,6 @@ fn check_size_of_val() { let mut buf_1 = String::from("001"); let my_slice = &[MyStr::new(&mut buf_0), MyStr::new(&mut buf_1)]; assert_eq!(size_of_val(my_slice), 32); // Slice of 2 fat pointers. - assert_eq!(size_of_val(my_slice[0]), 4); // Size of a fat pointer. + assert_eq!(size_of_val(my_slice[0]), 3); // Size of a fat pointer. assert_eq!(size_of_val(&my_slice[0].data), 1); // Size of str. }