Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Implement check for write_bytes #3108

Merged
merged 5 commits into from
Apr 5, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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,
celinval marked this conversation as resolved.
Show resolved Hide resolved
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().
celinval marked this conversation as resolved.
Show resolved Hide resolved

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) };
}
Loading