From c8816e4a3c3e93e8f0d1c3de9b94a8a397fcfa0c Mon Sep 17 00:00:00 2001 From: Ivo Matijasevic Date: Sat, 25 Jul 2026 22:39:58 +0200 Subject: [PATCH 1/3] Add support for volatile_copy_memory, volatile_copy_nonoverlapping_memory and volatile_set_memory Implements three of the intrinsics still unchecked on tracking issue #1163. Why the existing placeholders could not simply be un-gated ---------------------------------------------------------- The two copy intrinsics already had arms, but behind `unstable_codegen!`: Intrinsic::VolatileCopyMemory => unstable_codegen!(codegen_intrinsic_copy!(Memmove)), Intrinsic::VolatileCopyNonOverlappingMemory => { unstable_codegen!(codegen_intrinsic_copy!(Memcpy)) } `unstable_codegen!` is declared `($($tt:tt)*)` and never expands its tokens -- it unconditionally emits a codegen_unimplemented_expr. Those bodies were therefore never type-checked, and they have since rotted: codegen_intrinsic_copy! no longer exists anywhere in kani-compiler. Removing the gate alone does not compile, so both arms are rewritten rather than un-gated. `volatile_set_memory` had no Intrinsic variant at all and fell through to the unsupported catch-all. Argument order -------------- The intrinsics take the destination first: volatile_copy_memory(dst: *mut T, src: *const T, count: usize) volatile_copy_nonoverlapping_memory(dst: *mut T, src: *const T, count: usize) whereas codegen_copy consumes source first (two successive fargs.remove(0), src then dst) and indexes farg_types[0]/farg_types[1] for the src and dst alignment assertions. Both fargs and farg_types are therefore swapped before delegating. Swapping only one silently applies each alignment check to the wrong pointer -- a defect no test using two equally-aligned buffers would catch. volatile_set_memory(dst, val, count) matches write_bytes(dst, val, count), so no swap is needed there. Soundness of reusing the non-volatile codegen --------------------------------------------- Volatility constrains what the optimizer may do -- it must not elide, duplicate or reorder the access. It is not a memory-safety property: the UB conditions for these three intrinsics are exactly those of copy, copy_nonoverlapping and write_bytes. Kani performs no optimization that volatility is meant to suppress, so there is nothing additional to model. This mirrors the existing treatment of volatile_load/volatile_store. Points-to analysis ------------------ points_to_analysis.rs matches exhaustively over Intrinsic with a terminal unimplemented!() wildcard; write_bytes is protected from it via is_identity_aliasing_intrinsic. Before this change volatile_set_memory reached that pass as Intrinsic::Unimplemented, which is explicitly handled as a no-op. Introducing the new variant would have routed it to the panicking wildcard, so it is listed alongside write_bytes in the same way. The two check_uninit visitors have non-panicking fallbacks and are unchanged. Tests ----- Layout follows #1347, which added volatile_load support. tests/kani/Intrinsics/Volatile/copy.rs both copy intrinsics move the expected bytes, including an overlapping case for volatile_copy_memory (memmove semantics) that distinguishes it from the non-overlapping variant tests/kani/Intrinsics/Volatile/set.rs volatile_set_memory fills the destination, full and partial tests/expected/intrinsics/volatile_copy/overlapping/ volatile_copy_nonoverlapping_memory on overlapping ranges fails, matching the existing copy-nonoverlapping test for the non-volatile intrinsic tests/expected/intrinsics/volatile_copy/unaligned/ a misaligned pointer fails the alignment check The unaligned pair is deliberately left out: unaligned_volatile_load's gated body is a plain dereference, which does not model the unaligned access itself, and unaligned_volatile_store has no codegen at all. Those need a separate decision about how unaligned accesses should be represented. --- .../codegen/intrinsic.rs | 38 ++++++++++++- kani-compiler/src/intrinsics.rs | 5 ++ .../points_to/points_to_analysis.rs | 3 + .../volatile_copy/overlapping/expected | 1 + .../volatile_copy/overlapping/main.rs | 20 +++++++ .../volatile_copy/unaligned/expected | 2 + .../volatile_copy/unaligned/main.rs | 27 +++++++++ tests/kani/Intrinsics/Volatile/copy.rs | 57 +++++++++++++++++++ tests/kani/Intrinsics/Volatile/set.rs | 27 +++++++++ 9 files changed, 178 insertions(+), 2 deletions(-) create mode 100644 tests/expected/intrinsics/volatile_copy/overlapping/expected create mode 100644 tests/expected/intrinsics/volatile_copy/overlapping/main.rs create mode 100644 tests/expected/intrinsics/volatile_copy/unaligned/expected create mode 100644 tests/expected/intrinsics/volatile_copy/unaligned/main.rs create mode 100644 tests/kani/Intrinsics/Volatile/copy.rs create mode 100644 tests/kani/Intrinsics/Volatile/set.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 6f6bf6bba218..632cf21936e7 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -576,11 +576,45 @@ 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)), + // Volatility is an I/O-observability property (it tells the + // optimizer not to elide or reorder the access) and not a + // memory-safety property: the UB conditions for + // `volatile_copy_memory`/`volatile_copy_nonoverlapping_memory` + // are exactly those of the non-volatile `copy`/ + // `copy_nonoverlapping` intrinsics (see `codegen_copy`'s doc + // comment). Since Kani's codegen never performs the kind of + // optimization that volatility is meant to suppress, there is + // nothing extra to model, and it is sound to reuse + // `codegen_copy` as-is. + // + // 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). As with the + // copy intrinsics, volatility here is purely an + // optimizer-observability concern, so the UB conditions match + // `write_bytes` exactly and `codegen_write_bytes` can be reused + // unmodified. + 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/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/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]); +} From 97d5de2e28033a89d907f09b73e954b096d6d89a Mon Sep 17 00:00:00 2001 From: Ivo Matijasevic Date: Sun, 26 Jul 2026 18:54:06 +0200 Subject: [PATCH 2/3] Mark the three intrinsics as Partial in the feature-support table `docs/src/rust-feature-support/intrinsics.md` listed all three as `No`. They are now supported, so the table has to move. `Partial` rather than `Yes`, matching the neighbouring `volatile_load` and `volatile_store` rows and keeping the same Concurrency note. The memory-safety semantics are modelled exactly (they are those of the non-volatile counterparts), but the volatile guarantees themselves -- that the access is not elided or reordered, and really does touch memory -- are not, since Kani assumes sequential execution. Claiming `Yes` would overstate that and would disagree with how the two already-supported volatile intrinsics are documented. --- docs/src/rust-feature-support/intrinsics.md | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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 | | From 0d786973861a2f91d5da4f9f87e22589195a21d9 Mon Sep 17 00:00:00 2001 From: Ivo Matijasevic Date: Sun, 26 Jul 2026 22:47:57 +0200 Subject: [PATCH 3/3] Handle volatile_set_memory in the uninit visitor; soften the soundness comment Two review findings on the previous commit. 1. The compiler matches on `Intrinsic` in three places -- codegen, the points-to analysis, and the memory-initialization visitor -- and only the first two were updated. `volatile_set_memory` therefore fell to the visitor's catch-all and produced a spurious "Kani does not support reasoning about memory initialization" failure under -Z uninit-checks, while the codegen comment claimed it behaves exactly like `write_bytes`. It now shares that arm: same argument shape (dst, val, count), same initialization effect. 2. The comment overclaimed. "The UB conditions are exactly those of the non-volatile counterpart" is false as a generalisation: the volatile family's docs additionally permit pointers outside any Rust allocation (the MMIO carve-out on ptr::read_volatile), which the non-volatile ops do not. The modelling is still sound, but for a different reason than the comment gave -- reusing codegen_copy/codegen_write_bytes checks AT LEAST the documented UB conditions, so it is conservative rather than exact: a legal MMIO access can be rejected by --pointer-check, but real UB is never missed. The comments now say that, and anchor on what these intrinsics' own docs state ("consistent with copy_nonoverlapping" / "consistent with write_bytes") rather than on a blanket claim about volatility. Also adds tests/expected/intrinsics/volatile_set/out-of-bounds, mirroring the existing write_bytes test. The happy-path test alone did not pin that reusing codegen_write_bytes actually carries its safety checks across. --- .../codegen/intrinsic.rs | 37 +++++++++++-------- .../check_uninit/ptr_uninit/uninit_visitor.rs | 10 +++-- .../volatile_set/out-of-bounds/expected | 2 + .../volatile_set/out-of-bounds/main.rs | 19 ++++++++++ 4 files changed, 48 insertions(+), 20 deletions(-) create mode 100644 tests/expected/intrinsics/volatile_set/out-of-bounds/expected create mode 100644 tests/expected/intrinsics/volatile_set/out-of-bounds/main.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 632cf21936e7..0b241d840a8f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -576,16 +576,21 @@ 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), - // Volatility is an I/O-observability property (it tells the - // optimizer not to elide or reorder the access) and not a - // memory-safety property: the UB conditions for - // `volatile_copy_memory`/`volatile_copy_nonoverlapping_memory` - // are exactly those of the non-volatile `copy`/ - // `copy_nonoverlapping` intrinsics (see `codegen_copy`'s doc - // comment). Since Kani's codegen never performs the kind of - // optimization that volatility is meant to suppress, there is - // nothing extra to model, and it is sound to reuse - // `codegen_copy` as-is. + // 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 @@ -605,12 +610,12 @@ impl GotocCtx<'_, '_> { } 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). As with the - // copy intrinsics, volatility here is purely an - // optimizer-observability concern, so the UB conditions match - // `write_bytes` exactly and `codegen_write_bytes` can be reused - // unmodified. + // 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) 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_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]); +}