Skip to content

Commit

Permalink
Implement check for write_bytes (model-checking#3108)
Browse files Browse the repository at this point in the history
In the previous PR model-checking#3085, we did not support checks for `write_bytes`
which is added in this PR.

I am waiting for model-checking#3092 to add expected tests.
  • Loading branch information
celinval authored and zpzigi754 committed May 7, 2024
1 parent f01d3f6 commit 1d5dd96
Show file tree
Hide file tree
Showing 3 changed files with 62 additions and 1 deletion.
21 changes: 20 additions & 1 deletion kani-compiler/src/kani_middle/transform/check_values.rs
Original file line number Diff line number Diff line change
Expand Up @@ -440,7 +440,13 @@ impl<'a> MirVisitor for CheckValueVisitor<'a> {
// The write bytes intrinsic may trigger UB in safe code.
// pub unsafe fn write_bytes<T>(dst: *mut T, val: u8, count: usize)
// <https://doc.rust-lang.org/stable/core/intrinsics/fn.write_bytes.html>
// We don't support this operation yet.
// This is an over-approximation since writing an invalid value is
// not UB, only reading it will be.
assert_eq!(
args.len(),
3,
"Unexpected number of arguments for `write_bytes`"
);
let TyKind::RigidTy(RigidTy::RawPtr(target_ty, Mutability::Mut)) =
args[0].ty(self.locals).unwrap().kind()
else {
Expand All @@ -449,6 +455,19 @@ impl<'a> MirVisitor for CheckValueVisitor<'a> {
let validity = ty_validity_per_offset(&self.machine, target_ty, 0);
match validity {
Ok(ranges) if ranges.is_empty() => {}
Ok(ranges) => {
let sz = Const::try_from_uint(
target_ty.layout().unwrap().shape().size.bytes()
as u128,
UintTy::Usize,
)
.unwrap();
self.push_target(SourceOp::BytesValidity {
target_ty,
rvalue: Rvalue::Repeat(args[1].clone(), sz),
ranges,
})
}
_ => self.push_target(SourceOp::UnsupportedCheck {
check: "write_bytes".to_string(),
ty: target_ty,
Expand Down
21 changes: 21 additions & 0 deletions tests/kani/ValidValues/maybe_uninit.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
// kani-flags: -Z valid-value-checks
//! Check that Kani can identify UB when converting from a maybe uninit().

use std::mem::MaybeUninit;
use std::num::NonZeroI64;

#[kani::proof]
pub fn check_valid_zeroed() {
let maybe = MaybeUninit::zeroed();
let val: u128 = unsafe { maybe.assume_init() };
assert_eq!(val, 0);
}

#[kani::proof]
#[kani::should_panic]
pub fn check_invalid_zeroed() {
let maybe = MaybeUninit::zeroed();
let _val: NonZeroI64 = unsafe { maybe.assume_init() };
}
21 changes: 21 additions & 0 deletions tests/kani/ValidValues/write_bytes.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,21 @@
// Copyright Kani Contributors
// SPDX-License-Identifier: Apache-2.0 OR MIT
// kani-flags: -Z valid-value-checks
//! Check that Kani can identify UB when using write_bytes for initializing a variable.
#![feature(core_intrinsics)]

#[kani::proof]
#[kani::should_panic]
pub fn check_invalid_write() {
let mut val = 'a';
let ptr = &mut val as *mut char;
// Should fail given that we wrote invalid value to array of char.
unsafe { std::intrinsics::write_bytes(ptr, kani::any(), 1) };
}

#[kani::proof]
pub fn check_valid_write() {
let mut val = 10u128;
let ptr = &mut val as *mut _;
unsafe { std::intrinsics::write_bytes(ptr, kani::any(), 1) };
}

0 comments on commit 1d5dd96

Please sign in to comment.