Instrument validity checks for pointer to reference casts for slices …

…and str's (#3513)

As pointed out in #3498, validity checks for pointer to reference casts
(added in #3221) were not instrumented in the case of fat pointers (e.g.
array and string slices). This PR extends the instrumentation of
validity checks to handle those cases.

Resolves #3498 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

---------

Co-authored-by: Celina G. Val <celinval@amazon.com>

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<Stmt> {
+ ) -> 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

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() {

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,
  }
  }

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

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 };
+ }
+}

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.

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.
+}

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.

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());
+}

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

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());
+}

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.
 }