diff --git a/docs/src/rust-feature-support/intrinsics.md b/docs/src/rust-feature-support/intrinsics.md index 5067d0e294c1..74b0290736a1 100644 --- a/docs/src/rust-feature-support/intrinsics.md +++ b/docs/src/rust-feature-support/intrinsics.md @@ -220,8 +220,8 @@ try | No | [#267](https://github.com/model-checking/kani/issues/267) | type_id | Yes | | type_name | Yes | | typed_swap_nonoverlapping | Yes | | -unaligned_volatile_load | No | See [Notes - Concurrency](#concurrency) | -unaligned_volatile_store | No | See [Notes - Concurrency](#concurrency) | +unaligned_volatile_load | Partial | See [Notes - Concurrency](#concurrency) | +unaligned_volatile_store | Partial | See [Notes - Concurrency](#concurrency) | unchecked_add | Yes | | unchecked_div | Yes | | unchecked_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 0b241d840a8f..c77fedd3cf6f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -254,18 +254,6 @@ impl GotocCtx<'_, '_> { }}; } - macro_rules! unstable_codegen { - ($($tt:tt)*) => {{ - let expr = self.codegen_unimplemented_expr( - &format!("'{}' intrinsic", intrinsic_str), - cbmc_ret_ty, - loc, - "https://github.com/model-checking/kani/issues/new/choose", - ); - self.codegen_expr_to_place_stable(place, expr, loc) - }}; - } - let intrinsic = Intrinsic::from_instance(&instance); match intrinsic { @@ -566,12 +554,31 @@ impl GotocCtx<'_, '_> { Intrinsic::TruncF32 => codegen_simple_intrinsic!(Truncf), Intrinsic::TruncF64 => codegen_simple_intrinsic!(Trunc), Intrinsic::TypedSwap => self.codegen_swap(fargs, farg_types, loc), + // No alignment assertion for these two, by design: tolerating a + // misaligned pointer is the entire purpose of the `unaligned_*` + // variants. CBMC models the misaligned typed access byte-precisely, + // so the plain dereference is faithful -- see the byte-wise oracle + // tests in `tests/kani/Intrinsics/Volatile/unaligned.rs`, which + // compare the loaded value against `u32::from_ne_bytes` at every + // offset -- native order, so the oracle stays byte-precise without + // assuming an endianness. Dereferenceability itself is still checked + // by `--pointer-check`, as for the aligned variants. Intrinsic::UnalignedVolatileLoad => { - unstable_codegen!(self.codegen_expr_to_place_stable( - place, - fargs.remove(0).dereference(), - loc - )) + self.codegen_expr_to_place_stable(place, fargs.remove(0).dereference(), loc) + } + Intrinsic::UnalignedVolatileStore => { + assert!(self.place_ty_stable(place).kind().is_unit()); + let dst = fargs.remove(0); + let src = fargs.remove(0); + let dst_typ = farg_types[0]; + if self.is_zst_stable(pointee_type_stable(dst_typ).unwrap()) { + // Do not dereference (and assign) a ZST -- same guard as + // `codegen_volatile_store`. A ZST pointer may legally be + // dangling-but-aligned, so this path is reachable. + Stmt::skip(loc) + } else { + dst.dereference().assign(src, loc) + } } Intrinsic::UncheckedDiv => codegen_op_with_div_overflow_check!(div), Intrinsic::UncheckedRem => codegen_op_with_div_overflow_check!(rem), diff --git a/kani-compiler/src/intrinsics.rs b/kani-compiler/src/intrinsics.rs index adb96b5ffaa4..f73685cd42f3 100644 --- a/kani-compiler/src/intrinsics.rs +++ b/kani-compiler/src/intrinsics.rs @@ -138,6 +138,7 @@ pub enum Intrinsic { TruncF64, TypedSwap, UnalignedVolatileLoad, + UnalignedVolatileStore, UncheckedDiv, UncheckedRem, Unlikely, @@ -391,6 +392,10 @@ impl Intrinsic { assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Not) => _); Self::UnalignedVolatileLoad } + "unaligned_volatile_store" => { + assert_sig_matches!(sig, RigidTy::RawPtr(_, Mutability::Mut), _ => RigidTy::Tuple(_)); + Self::UnalignedVolatileStore + } "unchecked_add" | "unchecked_mul" | "unchecked_shl" | "unchecked_shr" | "unchecked_sub" => { unreachable!("Expected intrinsic `{intrinsic_str}` to be lowered before codegen") 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 c12120fdb9f8..34cc38cd8b7c 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 @@ -290,7 +290,7 @@ impl<'tcx> Analysis<'tcx> for PointsToAnalysis<'_, 'tcx> { state.extend(&lvalue_set, &state.successors(&rvalue_set)); } // Semantically equivalent *a = b. - Intrinsic::VolatileStore => { + Intrinsic::VolatileStore | Intrinsic::UnalignedVolatileStore => { let lvalue_set = self.successors_for_deref(state, args[0].node.clone()); let rvalue_set = self.successors_for_operand(state, args[1].node.clone()); 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 7a1ab27fe3a2..7e5d604b3319 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 @@ -329,7 +329,7 @@ impl MirVisitor for CheckUninitVisitor { Intrinsic::VolatileLoad | Intrinsic::UnalignedVolatileLoad => { self.push_target(MemoryInitOp::Check { operand: args[0].clone() }); } - Intrinsic::VolatileStore => { + Intrinsic::VolatileStore | Intrinsic::UnalignedVolatileStore => { self.push_target(MemoryInitOp::Set { operand: args[0].clone(), value: true, diff --git a/tests/expected/intrinsics/unaligned_volatile/out_of_bounds/expected b/tests/expected/intrinsics/unaligned_volatile/out_of_bounds/expected new file mode 100644 index 000000000000..73c3fe902ea4 --- /dev/null +++ b/tests/expected/intrinsics/unaligned_volatile/out_of_bounds/expected @@ -0,0 +1,14 @@ +Checking harness check_unaligned_volatile_load_out_of_bounds... + +check_unaligned_volatile_load_out_of_bounds.pointer_dereference\ +Status: FAILURE\ +Description: "dereference failure: pointer outside object bounds" + +Checking harness check_unaligned_volatile_store_out_of_bounds... + +check_unaligned_volatile_store_out_of_bounds.pointer_dereference\ +Status: FAILURE\ +Description: "dereference failure: pointer outside object bounds" + +Verification failed for - check_unaligned_volatile_load_out_of_bounds +Verification failed for - check_unaligned_volatile_store_out_of_bounds diff --git a/tests/expected/intrinsics/unaligned_volatile/out_of_bounds/main.rs b/tests/expected/intrinsics/unaligned_volatile/out_of_bounds/main.rs new file mode 100644 index 000000000000..052d73868b4e --- /dev/null +++ b/tests/expected/intrinsics/unaligned_volatile/out_of_bounds/main.rs @@ -0,0 +1,35 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that an out-of-bounds access through `unaligned_volatile_load` and +// `unaligned_volatile_store` is still caught. +// +// The `unaligned_*` variants deliberately emit no alignment assertion, and they +// codegen the access as a bare dereference rather than going through place +// codegen, which is where Kani normally attaches validity assertions. That makes +// it worth pinning down that dereferenceability is nevertheless checked, by +// CBMC's `--pointer-check`. Every other test for these intrinsics uses a valid, +// in-bounds pointer, so none of them would notice if that check were absent. +// +// The pointer arithmetic here is in bounds -- `add(1)` on a four-byte array is +// well defined -- so it is the *access* that overruns the object: reading or +// writing a `u32` at byte offset 1 touches bytes 1..5 of a 4-byte allocation. +// That keeps the failure attributable to the dereference rather than to the +// offset computation. +#![feature(core_intrinsics)] + +#[kani::proof] +fn check_unaligned_volatile_load_out_of_bounds() { + let buf: [u8; 4] = [0x11, 0x22, 0x33, 0x44]; + let p = unsafe { buf.as_ptr().add(1) } as *const u32; + let v = unsafe { std::intrinsics::unaligned_volatile_load(p) }; + assert_eq!(v, v); +} + +#[kani::proof] +fn check_unaligned_volatile_store_out_of_bounds() { + let mut buf: [u8; 4] = [0u8; 4]; + let p = unsafe { buf.as_mut_ptr().add(1) } as *mut u32; + unsafe { std::intrinsics::unaligned_volatile_store(p, 0x55443322u32) }; + assert_eq!(buf[0], 0x00); +} diff --git a/tests/kani/Intrinsics/Volatile/unaligned.rs b/tests/kani/Intrinsics/Volatile/unaligned.rs new file mode 100644 index 000000000000..b3005ee8fe7a --- /dev/null +++ b/tests/kani/Intrinsics/Volatile/unaligned.rs @@ -0,0 +1,107 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +// Checks that `unaligned_volatile_load` and `unaligned_volatile_store` access +// memory byte-precisely through a deliberately misaligned pointer. +// +// These intrinsics carry no alignment requirement, so the codegen emits no +// alignment assertion for them. That makes the modelling itself the thing worth +// testing: each proof compares against a byte-wise oracle, so an implementation +// that quietly read or wrote the *aligned* word instead would be caught rather +// than silently pass. The oracle is built with `u32::from_ne_bytes` so the test +// is byte-precise without assuming an endianness: reading a `u32` at byte offset +// 1 must equal the native-order interpretation of bytes 1, 2, 3 and 4, whereas +// an alignment-assuming read from offset 0 would give the interpretation of +// bytes 0, 1, 2 and 3 -- different under either endianness. +#![feature(core_intrinsics)] + +#[kani::proof] +fn check_unaligned_volatile_load_is_byte_precise() { + let buf: [u8; 8] = [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88]; + let p = unsafe { buf.as_ptr().add(1) } as *const u32; + let v = unsafe { std::intrinsics::unaligned_volatile_load(p) }; + let expect = u32::from_ne_bytes([buf[1], buf[2], buf[3], buf[4]]); + assert_eq!(v, expect, "unaligned load must read bytes 1, 2, 3 and 4, byte-precisely"); +} + +// The store direction: write a `u32` at byte offset 1 and check the neighbouring +// bytes too, so a wrongly-aligned write shows up as a clobbered neighbour rather +// than passing silently. +#[kani::proof] +fn check_unaligned_volatile_store_is_byte_precise() { + let mut buf: [u8; 8] = [0u8; 8]; + let p = unsafe { buf.as_mut_ptr().add(1) } as *mut u32; + let val: u32 = 0x55443322; + let bytes = val.to_ne_bytes(); + unsafe { std::intrinsics::unaligned_volatile_store(p, val) }; + assert_eq!(buf[0], 0x00, "byte before the store must be untouched"); + assert_eq!(buf[1], bytes[0]); + assert_eq!(buf[2], bytes[1]); + assert_eq!(buf[3], bytes[2]); + assert_eq!(buf[4], bytes[3]); + assert_eq!(buf[5], 0x00, "byte after the store must be untouched"); +} + +// Symbolic offset: the offset is not a constant, so the result cannot be reached +// by constant folding. This is the case that would expose an alignment +// assumption hidden behind constant propagation. +#[kani::proof] +fn check_unaligned_volatile_load_symbolic_offset() { + let buf: [u8; 8] = [0x11, 0x22, 0x33, 0x44, 0x55, 0x66, 0x77, 0x88]; + let off: usize = kani::any(); + kani::assume(off <= 4); + let p = unsafe { buf.as_ptr().add(off) } as *const u32; + let v = unsafe { std::intrinsics::unaligned_volatile_load(p) }; + let expect = u32::from_ne_bytes([buf[off], buf[off + 1], buf[off + 2], buf[off + 3]]); + assert_eq!(v, expect, "unaligned load must agree with a byte-wise oracle at every offset"); +} + +// The store direction with a symbolic offset, mirroring the load above. Without +// this, byte-precision on the store side rests on a constant offset alone, which +// a correct simplifier could satisfy while the general path stayed wrong. +#[kani::proof] +fn check_unaligned_volatile_store_symbolic_offset() { + let mut buf: [u8; 8] = [0u8; 8]; + let off: usize = kani::any(); + kani::assume(off <= 4); + let p = unsafe { buf.as_mut_ptr().add(off) } as *mut u32; + let val: u32 = 0x55443322; + let bytes = val.to_ne_bytes(); + unsafe { std::intrinsics::unaligned_volatile_store(p, val) }; + // The four written bytes must land at `off`, not at the aligned word. + assert_eq!(buf[off], bytes[0], "store must begin at the requested byte offset"); + assert_eq!(buf[off + 1], bytes[1]); + assert_eq!(buf[off + 2], bytes[2]); + assert_eq!(buf[off + 3], bytes[3]); + // Everything outside that range must be untouched, so a wrongly-aligned + // write shows up as a clobbered neighbour at every offset, not just one. + let mut i = 0; + while i < 8 { + if i < off || i >= off + 4 { + assert_eq!(buf[i], 0, "bytes outside the stored range must be untouched"); + } + i += 1; + } +} + +// A ZST store: `unaligned_volatile_store::<()>` must not attempt a dereference. +// A ZST pointer may legally be dangling-but-aligned, which is why +// `codegen_volatile_store` carries the same guard. +#[kani::proof] +fn check_zst_unaligned_volatile_store() { + let mut zst = (); + let p = &mut zst as *mut (); + unsafe { std::intrinsics::unaligned_volatile_store(p, ()) }; +} + +// The case the ZST guard actually exists for: a *dangling* pointer. A ZST +// reference is allowed to be any non-null, suitably aligned address, so this is +// a pointer safe Rust can hand to the intrinsic. Nothing is dereferenced, so +// this must verify. The harness above passes a pointer to a real local, which a +// dereference would happily succeed on -- so it does not exercise the guard, +// and only this one does. +#[kani::proof] +fn check_dangling_zst_unaligned_volatile_store() { + let p = core::ptr::without_provenance_mut::<()>(core::mem::align_of::<()>()); + unsafe { std::intrinsics::unaligned_volatile_store(p, ()) }; +} diff --git a/tests/kani/VolatileIntrinsics/core_intrinsics.rs b/tests/kani/VolatileIntrinsics/core_intrinsics.rs index 3aa0e3c07b85..b1c74299ce18 100644 --- a/tests/kani/VolatileIntrinsics/core_intrinsics.rs +++ b/tests/kani/VolatileIntrinsics/core_intrinsics.rs @@ -1,6 +1,5 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-verify-fail #![feature(core_intrinsics)]