diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs index bbf1ce13dfa..d40caefb0a8 100644 --- a/kani-compiler/src/kani_middle/transform/check_values.rs +++ b/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) diff --git a/tests/expected/valid-value-checks/slice_element.expected b/tests/expected/valid-value-checks/slice_element.expected new file mode 100644 index 00000000000..c0db8b2dcee --- /dev/null +++ b/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. diff --git a/tests/expected/valid-value-checks/slice_element.rs b/tests/expected/valid-value-checks/slice_element.rs new file mode 100644 index 00000000000..6fe511c462b --- /dev/null +++ b/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; + } +}