Check slice element reads under -Z valid-value-checks

kani-compiler/src/kani_middle/transform/check_values.rs

@@ -353,6 +353,9 @@ struct CheckValueVisitor<'a, 'b> {
     bb: BasicBlockIdx,
     /// Machine information needed to calculate Niche.
     machine: MachineInfo,
+    /// Whether the place being visited has its value read (`Copy`/`Move`), rather
+    /// than only its address taken or being written.
+    reading_value: bool,
 }
 
 impl<'a, 'b> CheckValueVisitor<'a, 'b> {
@@ -370,6 +373,7 @@ impl<'a, 'b> CheckValueVisitor<'a, 'b> {
             target: None,
             bb,
             machine: MachineInfo::target(),
+            reading_value: false,
         };
         visitor.visit_basic_block(&body.blocks()[bb]);
         visitor.target
@@ -499,6 +503,14 @@ impl MirVisitor for CheckValueVisitor<'_, '_> {
         }
     }
 
+    fn visit_operand(&mut self, operand: &Operand, location: Location) {
+        // `Copy`/`Move` read the operand's value; other uses (`&raw`, `&`, stores) don't.
+        let prev = self.reading_value;
+        self.reading_value = matches!(operand, Operand::Copy(_) | Operand::Move(_));
+        self.super_operand(operand, location);
+        self.reading_value = prev;
+    }
+
     fn visit_place(&mut self, place: &Place, ptx: PlaceContext, location: Location) {
         for (idx, elem) in place.projection.iter().enumerate() {
             let place_ref = PlaceRef { local: place.local, projection: &place.projection[..idx] };
@@ -562,9 +574,45 @@ impl MirVisitor for CheckValueVisitor<'_, '_> {
                 }
                 ProjectionElem::Downcast(_) => {}
                 ProjectionElem::OpaqueCast(_) => {}
-                ProjectionElem::Index(_)
-                | ProjectionElem::ConstantIndex { .. }
-                | ProjectionElem::Subslice { .. } => { /* safe */ }
+                ProjectionElem::Index(_) | ProjectionElem::ConstantIndex { .. } => {
+                    // A slice `[T]` has no static length, so the whole-slice deref
+                    // above checks no elements; check the one indexed element here
+                    // (a symbolic index makes CBMC cover every element, no length
+                    // loop). Sized arrays are already checked by the deref, so only
+                    // slices need this. Guard on a direct read of the whole element:
+                    // an address-of or write reads nothing, and a deeper projection
+                    // reads only a subplace.
+                    let base_ty = place_ref.ty(self.locals).unwrap();
+                    if let TyKind::RigidTy(RigidTy::Slice(elem_ty)) = base_ty.kind()
+                        && self.reading_value
+                        && place.projection.len() == idx + 1
+                    {
+                        let validity = ty_validity_per_offset(self.tcx, &self.machine, elem_ty, 0);
+                        match validity {
+                            Ok(ranges) if !ranges.is_empty() => {
+                                self.push_target(SourceOp::BytesValidity {
+                                    target_ty: elem_ty,
+                                    rvalue: Rvalue::Use(
+                                        Operand::Copy(Place {
+                                            local: place.local,
+                                            projection: place.projection[..=idx].to_vec(),
+                                        }),
+                                        WithRetag::No,
+                                    ),
+                                    ranges,
+                                })
+                            }
+                            Err(_msg) => self.push_target(SourceOp::UnsupportedCheck {
+                                check: "slice element read".to_string(),
+                                ty: elem_ty,
+                            }),
+                            _ => {}
+                        }
+                    }
+                }
+                // A subslice is still an unsized `[T]`; checking all its elements
+                // needs a runtime-length loop this pass does not have.
+                ProjectionElem::Subslice { .. } => { /* safe */ }
             }
         }
         self.super_place(place, ptx, location)

tests/expected/valid-value-checks/slice_element.expected

@@ -0,0 +1,21 @@
+Checking harness check_valid_slice_elem...
+VERIFICATION:- SUCCESSFUL
+
+Checking harness check_invalid_slice_elem_should_fail...
+Failed Checks: Undefined Behavior: Invalid value of type `bool`
+VERIFICATION:- FAILED
+
+Checking harness check_invalid_slice_elem_symbolic_should_fail...
+Failed Checks: Undefined Behavior: Invalid value of type `bool`
+VERIFICATION:- FAILED
+
+Checking harness check_raw_ref_slice_elem_no_read...
+VERIFICATION:- SUCCESSFUL
+
+Checking harness check_slice_elem_partial_read...
+VERIFICATION:- SUCCESSFUL
+
+Checking harness check_slice_elem_nested_write...
+VERIFICATION:- SUCCESSFUL
+
+Complete - 4 successfully verified harnesses, 2 failures, 6 total.

tests/expected/valid-value-checks/slice_element.rs

@@ -0,0 +1,71 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+// kani-flags: -Z valid-value-checks
+//! Regression test for https://github.com/model-checking/kani/issues/5022:
+//! reading an invalid element through a slice pointer must be reported (a slice
+//! has no static length, so the whole-slice deref checks no elements). The check
+//! fires only on a direct value read of the whole element, so forming a pointer
+//! (`&raw const`), reading a sub-element, and writing are not reported. `Index`
+//! and `ConstantIndex` share one arm, so the `Index` harnesses cover both.
+//! `black_box` keeps each read from being removed as dead code.
+
+/// Negative control: byte 2 read as a `bool` element is invalid.
+#[kani::proof]
+fn check_invalid_slice_elem_should_fail() {
+    let bytes = [2u8; 4];
+    let p = &bytes as *const [u8] as *const [bool];
+    let _ = std::hint::black_box(unsafe { (*p)[1] });
+}
+
+/// Negative control, symbolic index: only index 2 holds an invalid `bool`
+/// (byte 2); the rest are valid (byte 1). A symbolic index must still catch
+/// the one bad element, which proves the check tracks the actual index rather
+/// than a fixed position.
+#[kani::proof]
+fn check_invalid_slice_elem_symbolic_should_fail() {
+    let bytes = [1u8, 1u8, 2u8, 1u8];
+    let p = &bytes as *const [u8] as *const [bool];
+    let i: usize = kani::any();
+    kani::assume(i < 4);
+    let _ = std::hint::black_box(unsafe { (*p)[i] });
+}
+
+/// Positive control: valid `bool` elements (byte 1) at any index verify.
+#[kani::proof]
+fn check_valid_slice_elem() {
+    let bytes = [1u8; 4];
+    let p = &bytes as *const [u8] as *const [bool];
+    let i: usize = kani::any();
+    kani::assume(i < 4);
+    let _ = std::hint::black_box(unsafe { (*p)[i] });
+}
+
+/// Positive: forming a raw pointer to an element (`&raw const`) loads no `bool`,
+/// so an element that would be invalid if read must not be reported.
+#[kani::proof]
+fn check_raw_ref_slice_elem_no_read() {
+    let bytes = [2u8; 4];
+    let p = &bytes as *const [u8] as *const [bool];
+    let _ = std::hint::black_box(unsafe { &raw const (*p)[0] });
+}
+
+/// Positive: reading one `bool` of a `[bool; 2]` slice element checks only that
+/// sub-byte. Byte 0 is a valid `bool`; the unread byte 1 is invalid but must not
+/// cause a failure.
+#[kani::proof]
+fn check_slice_elem_partial_read() {
+    let bytes = [[1u8, 2u8]];
+    let p = &bytes as *const [[u8; 2]] as *const [[bool; 2]];
+    let _ = std::hint::black_box(unsafe { (*p)[0][0] });
+}
+
+/// Positive: writing one `bool` of a `[bool; 2]` slice element must not validate
+/// the element's old (invalid) contents, since a write is not UB until read.
+#[kani::proof]
+fn check_slice_elem_nested_write() {
+    let mut bytes = [[2u8, 2u8]];
+    let p = &mut bytes as *mut [[u8; 2]] as *mut [[bool; 2]];
+    unsafe {
+        (*p)[0][0] = true;
+    }
+}