diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 8034d6df8f5d..5067d0e294c1 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -232,10 +232,10 @@ unchecked_sub | Yes | | unlikely | Yes | | unreachable | Yes | | variant_count | Yes | | -volatile_copy_memory | No | See [Notes - Concurrency](#concurrency) | -volatile_copy_nonoverlapping_memory | No | See [Notes - Concurrency](#concurrency) | +volatile_copy_memory | Partial | See [Notes - Concurrency](#concurrency) | +volatile_copy_nonoverlapping_memory | Partial | See [Notes - Concurrency](#concurrency) | volatile_load | Partial | See [Notes - Concurrency](#concurrency) | -volatile_set_memory | No | See [Notes - Concurrency](#concurrency) | +volatile_set_memory | Partial | See [Notes - Concurrency](#concurrency) | volatile_store | Partial | See [Notes - Concurrency](#concurrency) | wrapping_add | Yes | | wrapping_mul | Yes | | diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 6f6bf6bba218..0b241d840a8f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -576,11 +576,50 @@ impl GotocCtx<'_, '_> { Intrinsic::UncheckedDiv => codegen_op_with_div_overflow_check!(div), Intrinsic::UncheckedRem => codegen_op_with_div_overflow_check!(rem), Intrinsic::Unlikely => self.codegen_expr_to_place_stable(place, fargs.remove(0), loc), - Intrinsic::VolatileCopyMemory => unstable_codegen!(codegen_intrinsic_copy!(Memmove)), + // These two document their safety requirements as "consistent + // with `copy`" / "consistent with `copy_nonoverlapping`", so + // reusing `codegen_copy` checks the conditions their own docs + // state. Volatility itself constrains the optimizer (the access + // must not be elided or reordered), which Kani has no need to + // model since it performs no such optimization. + // + // One direction is worth being explicit about: the volatile + // family's docs additionally permit pointers *outside* any Rust + // allocation (the MMIO carve-out on `ptr::read_volatile`), which + // the non-volatile counterparts do not. Reusing `codegen_copy` + // therefore checks *at least* the documented UB conditions and is + // conservative rather than exact -- a legal MMIO access may be + // rejected by `--pointer-check`. That is incompleteness, never a + // missed UB, which is the safe direction for a verifier. + // + // Both intrinsics are declared as `(dst, src, count)`, but + // `codegen_copy` expects `fargs`/`farg_types` ordered as + // `[src, dst, ..]` (it does `fargs.remove(0)` for `src` followed + // by `fargs.remove(0)` for `dst`). So we swap the first two + // entries of `fargs`, and build a `farg_types` slice with the + // first two entries swapped as well, before delegating. + Intrinsic::VolatileCopyMemory => { + fargs.swap(0, 1); + let swapped_types = [farg_types[1], farg_types[0]]; + self.codegen_copy(intrinsic_str, false, fargs, &swapped_types, Some(place), loc) + } Intrinsic::VolatileCopyNonOverlappingMemory => { - unstable_codegen!(codegen_intrinsic_copy!(Memcpy)) + fargs.swap(0, 1); + let swapped_types = [farg_types[1], farg_types[0]]; + self.codegen_copy(intrinsic_str, true, fargs, &swapped_types, Some(place), loc) } Intrinsic::VolatileLoad => self.codegen_volatile_load(fargs, farg_types, place, loc), + // `volatile_set_memory(dst, val, count)` has the same argument + // order as `write_bytes(dst, val, count)` (no `dst`/`src` swap is + // needed, unlike the two copy intrinsics above), and its docs + // state its safety requirements as "consistent with + // `write_bytes`", so `codegen_write_bytes` checks the conditions + // its own docs state. The same conservative-direction caveat as + // the copy intrinsics above applies to the MMIO carve-out. + Intrinsic::VolatileSetMemory => { + assert!(self.place_ty_stable(place).kind().is_unit()); + self.codegen_write_bytes(fargs, farg_types, loc) + } Intrinsic::VolatileStore => { assert!(self.place_ty_stable(place).kind().is_unit()); self.codegen_volatile_store(fargs, farg_types, loc) diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs index 0bb42539aca9..adb96b5ffaa4 100644 --- a/kani-compiler/src/intrinsics.rs +++ b/kani-compiler/src/intrinsics.rs @@ -144,6 +144,7 @@ pub enum Intrinsic { VolatileCopyMemory, VolatileCopyNonOverlappingMemory, VolatileLoad, + VolatileSetMemory, VolatileStore, VtableSize, VtableAlign, @@ -424,6 +425,10 @@ impl Intrinsic { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => _); Self::VolatileLoad } + "volatile_set_memory" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), RigidTy::Uint(UintTy::U8), RigidTy::Uint(UintTy::Usize) => RigidTy::Tuple(_)); + Self::VolatileSetMemory + } "volatile_store" => { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => RigidTy::Tuple(_)); Self::VolatileStore diff --git a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs index a7529d4298ef..c12120fdb9f8 100644 --- a/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs +++ b/kani-compiler/src/kani_middle/points_to/points_to_analysis.rs @@ -698,6 +698,9 @@ fn is_identity_aliasing_intrinsic(intrinsic: Intrinsic) -> bool { | Intrinsic::UncheckedDiv | Intrinsic::UncheckedRem | Intrinsic::Unlikely + // Same argument shape/semantics as `WriteBytes` below (volatility is not + // an aliasing concern), so it is likewise identity-aliasing. + | Intrinsic::VolatileSetMemory | Intrinsic::VtableSize | Intrinsic::VtableAlign | Intrinsic::WrappingAdd diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs index 38c3dc93646c..7a1ab27fe3a2 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/ptr_uninit/uninit_visitor.rs @@ -336,14 +336,16 @@ impl MirVisitor for CheckUninitVisitor { position: InsertPosition::After, }); } - Intrinsic::WriteBytes => { - self.push_target(MemoryInitOp::SetSliceChunk { + // `volatile_set_memory(dst, val, count)` has the same shape and the + // same memory-initialization effect as `write_bytes(dst, val, count)`; + // volatility does not change which bytes become initialized. + Intrinsic::WriteBytes | Intrinsic::VolatileSetMemory => self + .push_target(MemoryInitOp::SetSliceChunk { operand: args[0].clone(), count: args[2].clone(), value: true, position: InsertPosition::After, - }) - } + }), intrinsic => { self.push_target(MemoryInitOp::Unsupported { reason: format!("Kani does not support reasoning about memory initialization of intrinsic `{intrinsic:?}`."), diff --git a/tests/expected/intrinsics/volatile_copy/overlapping/expected b/tests/expected/intrinsics/volatile_copy/overlapping/expected new file mode 100644 index 000000000000..9ebadf73b291 --- /dev/null +++ b/tests/expected/intrinsics/volatile_copy/overlapping/expected @@ -0,0 +1 @@ +memcpy src/dst overlap \ No newline at end of file diff --git a/tests/expected/intrinsics/volatile_copy/overlapping/main.rs b/tests/expected/intrinsics/volatile_copy/overlapping/main.rs new file mode 100644 index 000000000000..db5fb3f6927a --- /dev/null +++ b/tests/expected/intrinsics/volatile_copy/overlapping/main.rs @@ -0,0 +1,20 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that `volatile_copy_nonoverlapping_memory` fails if the `dst`/`src` +// regions overlap. +#![feature(core_intrinsics)] + +#[kani::proof] +fn test_volatile_copy_nonoverlapping_memory_with_overlap() { + let arr: [i32; 3] = [0, 1, 0]; + let src: *const i32 = arr.as_ptr(); + + unsafe { + // The call to `volatile_copy_nonoverlapping_memory` is expected to + // fail because the `src` region and the `dst` region overlap in + // `arr[1]` + let dst = src.add(1) as *mut i32; + core::intrinsics::volatile_copy_nonoverlapping_memory(dst, src, 2); + } +} diff --git a/tests/expected/intrinsics/volatile_copy/unaligned/expected b/tests/expected/intrinsics/volatile_copy/unaligned/expected new file mode 100644 index 000000000000..1c1e00c0cb0a --- /dev/null +++ b/tests/expected/intrinsics/volatile_copy/unaligned/expected @@ -0,0 +1,2 @@ +FAILURE\ +`dst` must be properly aligned \ No newline at end of file diff --git a/tests/expected/intrinsics/volatile_copy/unaligned/main.rs b/tests/expected/intrinsics/volatile_copy/unaligned/main.rs new file mode 100644 index 000000000000..765007c59ad4 --- /dev/null +++ b/tests/expected/intrinsics/volatile_copy/unaligned/main.rs @@ -0,0 +1,27 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that `volatile_copy_memory` fails when `dst` is not aligned. +// +// This specifically misaligns `dst` (and not `src`) because +// `volatile_copy_memory` is declared as `(dst, src, count)`, the reverse of +// the `(src, dst, ..)` order that `codegen_copy` expects internally, so +// codegen must swap `fargs`/`farg_types` before delegating to it. Misaligning +// `dst` while keeping `src` aligned distinguishes a correct swap (which +// reports "`dst` must be properly aligned") from a missing/backwards swap +// (which would instead misreport "`src` must be properly aligned"). +#![feature(core_intrinsics)] + +#[kani::proof] +fn test_volatile_copy_memory_unaligned_dst() { + let arr: [i32; 3] = [0, 1, 0]; + let src: *const i32 = arr.as_ptr(); + + unsafe { + // Obtain an unaligned pointer by casting into `*const i8`, adding an + // offset of 1 and casting back into `*mut i32`. + let dst_i8: *const i8 = src as *const i8; + let dst_unaligned = dst_i8.add(1) as *mut i32; + core::intrinsics::volatile_copy_memory(dst_unaligned, src, 1); + } +} diff --git a/tests/expected/intrinsics/volatile_set/out-of-bounds/expected b/tests/expected/intrinsics/volatile_set/out-of-bounds/expected new file mode 100644 index 000000000000..d69010f53d0c --- /dev/null +++ b/tests/expected/intrinsics/volatile_set/out-of-bounds/expected @@ -0,0 +1,2 @@ +FAILURE\ +memset destination region writeable \ No newline at end of file diff --git a/tests/expected/intrinsics/volatile_set/out-of-bounds/main.rs b/tests/expected/intrinsics/volatile_set/out-of-bounds/main.rs new file mode 100644 index 000000000000..8355b63076be --- /dev/null +++ b/tests/expected/intrinsics/volatile_set/out-of-bounds/main.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that `volatile_set_memory` fails if an out-of-bounds write is made. +// Mirrors the equivalent `write_bytes` test, since the two share codegen: this +// pins that reusing `codegen_write_bytes` really does carry its safety checks +// over to the volatile variant, rather than only its happy path. +#![feature(core_intrinsics)] +use std::intrinsics::volatile_set_memory; + +#[kani::proof] +fn main() { + let mut vec = vec![0u32; 4]; + unsafe { + let vec_ptr = vec.as_mut_ptr().add(4); + volatile_set_memory(vec_ptr, 0xfe, 1); + } + assert_eq!(vec, [0, 0, 0, 0]); +} diff --git a/tests/kani/Intrinsics/Volatile/copy.rs b/tests/kani/Intrinsics/Volatile/copy.rs new file mode 100644 index 000000000000..d28442fe35d8 --- /dev/null +++ b/tests/kani/Intrinsics/Volatile/copy.rs @@ -0,0 +1,57 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that `volatile_copy_memory` and `volatile_copy_nonoverlapping_memory` +// copy `count` elements from `src` to `dst`. +// +// `volatile_copy_memory` further allows the `src`/`dst` regions to overlap +// (memmove semantics), while `volatile_copy_nonoverlapping_memory` requires +// disjoint regions (memcpy semantics; the failing overlapping case is +// checked separately under +// `tests/expected/intrinsics/volatile_copy/overlapping`). Exercising the +// overlapping case here for `volatile_copy_memory` also distinguishes the +// two variants from one another: if they were accidentally coded up +// identically (e.g. both using `memcpy`), this proof would fail. +#![feature(core_intrinsics)] + +#[kani::proof] +fn test_volatile_copy_memory_simple() { + let mut expected_val = 42; + let src: *mut i32 = &mut expected_val as *mut i32; + let mut old_val = 99; + let dst: *mut i32 = &mut old_val; + unsafe { + core::intrinsics::volatile_copy_memory(dst, src, 1); + assert!(*dst == expected_val); + } +} + +#[kani::proof] +fn test_volatile_copy_memory_with_overlap() { + let arr: [i32; 3] = [0, 1, 0]; + let src: *const i32 = arr.as_ptr(); + + unsafe { + // `dst` overlaps `src` in `arr[1]`. `volatile_copy_memory` must + // still succeed here (unlike `volatile_copy_nonoverlapping_memory`). + let dst = src.add(1) as *mut i32; + core::intrinsics::volatile_copy_memory(dst, src, 2); + // The first value does not change + assert!(arr[0] == 0); + // The next values are copied from `arr[0..=1]` + assert!(arr[1] == 0); + assert!(arr[2] == 1); + } +} + +#[kani::proof] +fn test_volatile_copy_nonoverlapping_memory_simple() { + let mut expected_val = 42; + let src: *mut i32 = &mut expected_val as *mut i32; + let mut old_val = 99; + let dst: *mut i32 = &mut old_val; + unsafe { + core::intrinsics::volatile_copy_nonoverlapping_memory(dst, src, 1); + assert!(*dst == expected_val); + } +} diff --git a/tests/kani/Intrinsics/Volatile/set.rs b/tests/kani/Intrinsics/Volatile/set.rs new file mode 100644 index 000000000000..7acc1f6bde71 --- /dev/null +++ b/tests/kani/Intrinsics/Volatile/set.rs @@ -0,0 +1,27 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Check that `volatile_set_memory` fills `count` elements starting at `dst` +// with the byte value `val`. +#![feature(core_intrinsics)] + +#[kani::proof] +fn test_volatile_set_memory_simple() { + let mut arr: [u8; 4] = [0, 0, 0, 0]; + let dst: *mut u8 = arr.as_mut_ptr(); + unsafe { + core::intrinsics::volatile_set_memory(dst, 0xAB, 4); + } + assert!(arr == [0xAB, 0xAB, 0xAB, 0xAB]); +} + +#[kani::proof] +fn test_volatile_set_memory_partial() { + let mut arr: [u8; 4] = [1, 2, 3, 4]; + unsafe { + // Only fill the first two elements. + let dst: *mut u8 = arr.as_mut_ptr(); + core::intrinsics::volatile_set_memory(dst, 0, 2); + } + assert!(arr == [0, 0, 3, 4]); +}