From 2334f2c6cb351183447fbdb950d2467fe451441c Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 11 Dec 2024 14:37:29 -0800 Subject: [PATCH] Add out of bounds check for `offset` intrinsics (#3755) Note that the `offset` intrinsics is lowered to `Rvalue::Offset`. Thus, we have to replace the entire statement. This PR does not address `ptr_offset_from` and `ptr_offset_from_unsigned`. I'll push those changes to a separate PR. Resolves #1233 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Carolyn Zech --- .../codegen_cprover_gotoc/codegen/assert.rs | 11 +- .../codegen/intrinsic.rs | 2 +- .../codegen_cprover_gotoc/codegen/rvalue.rs | 43 ++----- .../codegen_cprover_gotoc/overrides/hooks.rs | 49 ++++++-- .../src/kani_middle/kani_functions.rs | 4 + .../src/kani_middle/transform/body.rs | 5 + .../kani_middle/transform/rustc_intrinsics.rs | 117 ++++++++++++++++-- library/kani_core/src/lib.rs | 14 +++ library/kani_core/src/mem.rs | 16 ++- library/kani_core/src/models.rs | 74 +++++++++++ .../copy-unreadable-src/main.rs | 6 +- .../copy/copy-unreadable-src/main.rs | 6 +- .../fixme_offset_usize.expected | 11 ++ .../offset-bounds-check/fixme_offset_usize.rs | 31 +++++ .../out_of_bounds_ub_check.expected | 4 + .../out_of_bounds_ub_check.rs | 26 ++++ .../start_from_oob.expected | 4 + .../offset-bounds-check/start_from_oob.rs | 16 +++ tests/expected/offset-bytes-overflow/expected | 6 +- .../offset-from-bytes-overflow/expected | 6 +- .../invalid_offset_ty.expected | 1 + .../offset-invalid-args/invalid_offset_ty.rs | 16 +++ .../offset-invalid-args/non_ptr_arg.expected | 1 + .../offset-invalid-args/non_ptr_arg.rs | 15 +++ tests/expected/offset-overflow/expected | 6 +- tests/expected/offset-wraps-around/expected | 14 ++- tests/expected/offset-wraps-around/main.rs | 62 ++++++---- tests/expected/pointer-overflow/expected | 3 +- tests/expected/pointer-overflow/main.rs | 1 - .../ptr-offset-overflow-bytes/expected | 8 +- tests/expected/ptr_to_ref_cast/slice/test.rs | 2 +- tests/expected/raw_slice/expected | 3 +- tests/expected/raw_slice_c_repr/expected | 3 +- tests/expected/raw_slice_packed/expected | 3 +- .../fixme_wrap_nonzero_offset.rs | 18 +++ tests/kani/ValidValues/unaligned.rs | 37 ++++++ tests/kani/Vectors/vector_extend_bytes.rs | 3 +- 37 files changed, 529 insertions(+), 118 deletions(-) create mode 100644 tests/expected/offset-bounds-check/fixme_offset_usize.expected create mode 100644 tests/expected/offset-bounds-check/fixme_offset_usize.rs create mode 100644 tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected create mode 100644 tests/expected/offset-bounds-check/out_of_bounds_ub_check.rs create mode 100644 tests/expected/offset-bounds-check/start_from_oob.expected create mode 100644 tests/expected/offset-bounds-check/start_from_oob.rs create mode 100644 tests/expected/offset-invalid-args/invalid_offset_ty.expected create mode 100644 tests/expected/offset-invalid-args/invalid_offset_ty.rs create mode 100644 tests/expected/offset-invalid-args/non_ptr_arg.expected create mode 100644 tests/expected/offset-invalid-args/non_ptr_arg.rs create mode 100644 tests/kani/PointerOffset/fixme_wrap_nonzero_offset.rs create mode 100644 tests/kani/ValidValues/unaligned.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs index 84b20a623541..f1971f2f158e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/assert.rs @@ -38,7 +38,7 @@ pub enum PropertyClass { /// Overflow panics that can be generated by Intrisics. /// NOTE: Not all uses of this are found by rust-analyzer because of the use of macros. Try grep instead. /// - /// SPECIAL BEHAVIOR: None TODO: Why should this exist? + /// SPECIAL BEHAVIOR: Same as SafetyCheck. TODO: Replace this with `SafetyCheck`. ArithmeticOverflow, /// The Rust `assume` instrinsic is `assert`'d by Kani, and gets this property class. /// @@ -67,13 +67,13 @@ pub enum PropertyClass { /// That is, they do not depend on special instrumentation that Kani performs that wouldn't /// otherwise be observable. Assertion, - /// Another instrinsic check. + /// Another intrinsic check. /// - /// SPECIAL BEHAVIOR: None TODO: Why should this exist? + /// SPECIAL BEHAVIOR: Same as SafetyCheck. TODO: Replace this with `SafetyCheck`. ExactDiv, - /// Another instrinsic check. + /// Another intrinsic check. /// - /// SPECIAL BEHAVIOR: None TODO: Why should this exist? + /// SPECIAL BEHAVIOR: Same as SafetyCheck. TODO: Replace this with `SafetyCheck`. FiniteCheck, /// Checks added by Kani compiler to determine whether a property (e.g. /// `PropertyClass::Assertion` or `PropertyClass:Cover`) is reachable @@ -82,6 +82,7 @@ pub enum PropertyClass { /// E.g., things that trigger UB or unstable behavior. /// /// SPECIAL BEHAVIOR: Assertions that may not exist when running code normally (i.e. not under Kani) + /// This is not caught by `#[should_panic]`. SafetyCheck, /// Checks to ensure that Kani's code generation is correct. /// diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index a1daeec5f88b..654a7f2b6861 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -1015,7 +1015,7 @@ impl GotocCtx<'_> { /// /// This function handles code generation for the `arith_offset` intrinsic. /// - /// According to the documenation, the operation is always safe. + /// According to the documentation, the operation is always safe. fn codegen_arith_offset(&mut self, mut fargs: Vec, p: &Place, loc: Location) -> Stmt { let src_ptr = fargs.remove(0); let offset = fargs.remove(0); diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index f84e0a89f937..68c174ae2119 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -356,7 +356,7 @@ impl GotocCtx<'_> { fn codegen_rvalue_binary_op( &mut self, - ty: Ty, + _ty: Ty, op: &BinOp, e1: &Operand, e2: &Operand, @@ -405,42 +405,15 @@ impl GotocCtx<'_> { } // https://doc.rust-lang.org/std/primitive.pointer.html#method.offset BinOp::Offset => { + // We don't need to check for UB since we handled user calls of offset already + // via rustc_intrinsic transformation pass. + // + // This operation may still be used by other Kani instrumentation which should + // ensure safety. + // We should consider adding sanity checks if `debug_assertions` are enabled. let ce1 = self.codegen_operand_stable(e1); let ce2 = self.codegen_operand_stable(e2); - - // Check that computing `offset` in bytes would not overflow - let (offset_bytes, bytes_overflow_check) = self.count_in_bytes( - ce2.clone().cast_to(Type::ssize_t()), - pointee_type_stable(ty).unwrap(), - Type::ssize_t(), - "offset", - loc, - ); - - // Check that the computation would not overflow an `isize` which is UB: - // https://doc.rust-lang.org/std/primitive.pointer.html#method.offset - // These checks may allow a wrapping-around behavior in CBMC: - // https://github.com/model-checking/kani/issues/1150 - // Note(std): We don't check that the starting or resulting pointer stay - // within bounds of the object they point to. Doing so causes spurious - // failures due to the usage of these intrinsics in the standard library. - // See for more details. - // Note that this is one of the safety conditions for `offset`: - // - - let overflow_res = ce1.clone().cast_to(Type::ssize_t()).add_overflow(offset_bytes); - let overflow_check = self.codegen_assert_assume( - overflow_res.overflowed.not(), - PropertyClass::ArithmeticOverflow, - "attempt to compute offset which would overflow", - loc, - ); - let res = ce1.clone().plus(ce2); - Expr::statement_expression( - vec![bytes_overflow_check, overflow_check, res.as_stmt(loc)], - ce1.typ().clone(), - loc, - ) + ce1.clone().plus(ce2) } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index d228965f7633..73c887b3eeaf 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -134,15 +134,46 @@ impl GotocHook for Assert { let (msg, reach_stmt) = gcx.codegen_reachability_check(msg, span); - // Since `cond` might have side effects, assign it to a temporary - // variable so that it's evaluated once, then assert and assume it - // TODO: I don't think `cond` can have side effects, this is MIR, it's going to be temps - let (tmp, decl) = gcx.decl_temp_variable(cond.typ().clone(), Some(cond), caller_loc); Stmt::block( vec![ reach_stmt, - decl, - gcx.codegen_assert_assume(tmp, PropertyClass::Assertion, &msg, caller_loc), + gcx.codegen_assert_assume(cond, PropertyClass::Assertion, &msg, caller_loc), + Stmt::goto(bb_label(target), caller_loc), + ], + caller_loc, + ) + } +} + +struct UnsupportedCheck; +impl GotocHook for UnsupportedCheck { + fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool { + unreachable!("{UNEXPECTED_CALL}") + } + + fn handle( + &self, + gcx: &mut GotocCtx, + _instance: Instance, + mut fargs: Vec, + _assign_to: &Place, + target: Option, + span: Span, + ) -> Stmt { + assert_eq!(fargs.len(), 2); + let msg = fargs.pop().unwrap(); + let cond = fargs.pop().unwrap().cast_to(Type::bool()); + let msg = gcx.extract_const_message(&msg).unwrap(); + let target = target.unwrap(); + let caller_loc = gcx.codegen_caller_span_stable(span); + Stmt::block( + vec![ + gcx.codegen_assert_assume( + cond, + PropertyClass::UnsupportedConstruct, + &msg, + caller_loc, + ), Stmt::goto(bb_label(target), caller_loc), ], caller_loc, @@ -166,8 +197,8 @@ impl GotocHook for SafetyCheck { span: Span, ) -> Stmt { assert_eq!(fargs.len(), 2); - let cond = fargs.remove(0).cast_to(Type::bool()); - let msg = fargs.remove(0); + let msg = fargs.pop().unwrap(); + let cond = fargs.pop().unwrap().cast_to(Type::bool()); let msg = gcx.extract_const_message(&msg).unwrap(); let target = target.unwrap(); let caller_loc = gcx.codegen_caller_span_stable(span); @@ -181,6 +212,7 @@ impl GotocHook for SafetyCheck { } } +// TODO: Remove this and replace occurrences with `SanityCheck`. struct Check; impl GotocHook for Check { fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool { @@ -709,6 +741,7 @@ pub fn fn_hooks() -> GotocHooks { (KaniHook::IsAllocated, Rc::new(IsAllocated)), (KaniHook::PointerObject, Rc::new(PointerObject)), (KaniHook::PointerOffset, Rc::new(PointerOffset)), + (KaniHook::UnsupportedCheck, Rc::new(UnsupportedCheck)), (KaniHook::UntrackedDeref, Rc::new(UntrackedDeref)), (KaniHook::InitContracts, Rc::new(InitContracts)), (KaniHook::FloatToIntInRange, Rc::new(FloatToIntInRange)), diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 6a136f1a5647..38522fae837f 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -81,6 +81,8 @@ pub enum KaniModel { IsSliceChunkPtrInitialized, #[strum(serialize = "IsSlicePtrInitializedModel")] IsSlicePtrInitialized, + #[strum(serialize = "OffsetModel")] + Offset, #[strum(serialize = "RunContractModel")] RunContract, #[strum(serialize = "RunLoopContractModel")] @@ -140,6 +142,8 @@ pub enum KaniHook { PointerOffset, #[strum(serialize = "SafetyCheckHook")] SafetyCheck, + #[strum(serialize = "UnsupportedCheckHook")] + UnsupportedCheck, #[strum(serialize = "UntrackedDerefHook")] UntrackedDeref, } diff --git a/kani-compiler/src/kani_middle/transform/body.rs b/kani-compiler/src/kani_middle/transform/body.rs index 911ccf17e55f..f2072fb21fb1 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -434,6 +434,11 @@ impl MutableBody { ) { self.blocks.get_mut(source_instruction.bb()).unwrap().terminator = new_term; } + + /// Remove the given statement. + pub fn remove_stmt(&mut self, bb: BasicBlockIdx, stmt: usize) { + self.blocks[bb].statements.remove(stmt); + } } // TODO: Remove this enum, since we now only support kani's assert. diff --git a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs index 8174e8eb5e66..ad4238574d63 100644 --- a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs @@ -8,13 +8,21 @@ use crate::intrinsics::Intrinsic; use crate::kani_middle::kani_functions::{KaniFunction, KaniModel}; -use crate::kani_middle::transform::body::{MutMirVisitor, MutableBody}; +use crate::kani_middle::transform::body::{ + InsertPosition, MutMirVisitor, MutableBody, SourceInstruction, +}; use crate::kani_middle::transform::{TransformPass, TransformationType}; use crate::kani_queries::QueryDb; use rustc_middle::ty::TyCtxt; +use rustc_smir::rustc_internal; use stable_mir::mir::mono::Instance; -use stable_mir::mir::{Body, ConstOperand, LocalDecl, Operand, Terminator, TerminatorKind}; -use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind}; +use stable_mir::mir::{ + BasicBlockIdx, BinOp, Body, ConstOperand, LocalDecl, Operand, Rvalue, StatementKind, + Terminator, TerminatorKind, +}; +use stable_mir::ty::{ + FnDef, GenericArgKind, GenericArgs, IntTy, MirConst, RigidTy, Span, Ty, TyKind, UintTy, +}; use std::collections::HashMap; use tracing::debug; @@ -42,12 +50,14 @@ impl TransformPass for RustcIntrinsicsPass { /// Transform the function body by inserting checks one-by-one. /// For every unsafe dereference or a transmute operation, we check all values are valid. - fn transform(&mut self, _tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { + fn transform(&mut self, tcx: TyCtxt, body: Body, instance: Instance) -> (bool, Body) { debug!(function=?instance.name(), "transform"); let mut new_body = MutableBody::from(body); - let mut visitor = ReplaceIntrinsicVisitor::new(&self.models, new_body.locals().to_vec()); + let mut visitor = + ReplaceIntrinsicCallVisitor::new(&self.models, new_body.locals().to_vec()); visitor.visit_body(&mut new_body); - (visitor.changed, new_body.into()) + let changed = self.replace_lowered_intrinsics(tcx, &mut new_body); + (visitor.changed || changed, new_body.into()) } } @@ -63,21 +73,78 @@ impl RustcIntrinsicsPass { debug!(?models, "RustcIntrinsicsPass::new"); RustcIntrinsicsPass { models } } + + /// This function checks if we need to replace intrinsics that have been lowered. + fn replace_lowered_intrinsics(&self, tcx: TyCtxt, body: &mut MutableBody) -> bool { + // Do a reverse iteration on the instructions since we will replace Rvalues by a function + // call, which will split the basic block. + let mut changed = false; + let orig_bbs = body.blocks().len(); + for bb in (0..orig_bbs).rev() { + let num_stmts = body.blocks()[bb].statements.len(); + for stmt in (0..num_stmts).rev() { + changed |= self.replace_offset(tcx, body, bb, stmt); + } + } + changed + } + + /// Replace a lowered offset intrinsic. + fn replace_offset( + &self, + tcx: TyCtxt, + body: &mut MutableBody, + bb: BasicBlockIdx, + stmt: usize, + ) -> bool { + let statement = &body.blocks()[bb].statements[stmt]; + let StatementKind::Assign(place, rvalue) = &statement.kind else { + return false; + }; + let Rvalue::BinaryOp(BinOp::Offset, op1, op2) = rvalue else { return false }; + let mut source = SourceInstruction::Statement { idx: stmt, bb }; + + // Double check input parameters of `offset` operation. + let offset_ty = op2.ty(body.locals()).unwrap(); + let pointer_ty = op1.ty(body.locals()).unwrap(); + validate_offset(tcx, offset_ty, statement.span); + validate_raw_ptr(tcx, pointer_ty, statement.span); + tcx.dcx().abort_if_errors(); + + let pointee_ty = pointer_ty.kind().builtin_deref(true).unwrap().ty; + // The model takes the following parameters (PointeeType, PointerType, OffsetType). + let model = self.models[&KaniModel::Offset]; + let params = vec![ + GenericArgKind::Type(pointee_ty), + GenericArgKind::Type(pointer_ty), + GenericArgKind::Type(offset_ty), + ]; + let instance = Instance::resolve(model, &GenericArgs(params)).unwrap(); + body.insert_call( + &instance, + &mut source, + InsertPosition::After, + vec![op1.clone(), op2.clone()], + place.clone(), + ); + body.remove_stmt(bb, stmt); + true + } } -struct ReplaceIntrinsicVisitor<'a> { +struct ReplaceIntrinsicCallVisitor<'a> { models: &'a HashMap, locals: Vec, changed: bool, } -impl<'a> ReplaceIntrinsicVisitor<'a> { +impl<'a> ReplaceIntrinsicCallVisitor<'a> { fn new(models: &'a HashMap, locals: Vec) -> Self { - ReplaceIntrinsicVisitor { models, locals, changed: false } + ReplaceIntrinsicCallVisitor { models, locals, changed: false } } } -impl MutMirVisitor for ReplaceIntrinsicVisitor<'_> { +impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_> { /// Replace the terminator for some rustc's intrinsics. /// /// In some cases, we replace a function call to a rustc intrinsic by a call to the @@ -117,3 +184,33 @@ impl MutMirVisitor for ReplaceIntrinsicVisitor<'_> { self.super_terminator(term); } } + +/// Validate whether the offset type is valid, i.e., `isize` or `usize`. +/// +/// This will emit an error if the type is wrong but not abort. +/// Invoke `tcx.dcx().abort_if_errors()` to abort execution. +fn validate_offset(tcx: TyCtxt, offset_ty: Ty, span: Span) { + if !matches!( + offset_ty.kind(), + TyKind::RigidTy(RigidTy::Int(IntTy::Isize)) | TyKind::RigidTy(RigidTy::Uint(UintTy::Usize)) + ) { + tcx.dcx().span_err( + rustc_internal::internal(tcx, span), + format!("Expected `isize` or `usize` for offset type. Found `{offset_ty}` instead"), + ); + } +} + +/// Validate that we have a raw pointer otherwise emit an error. +/// +/// This will emit an error if the type is wrong but not abort. +/// Invoke `tcx.dcx().abort_if_errors()` to abort execution. +fn validate_raw_ptr(tcx: TyCtxt, ptr_ty: Ty, span: Span) { + let pointer_ty_kind = ptr_ty.kind(); + if !pointer_ty_kind.is_raw_ptr() { + tcx.dcx().span_err( + rustc_internal::internal(tcx, span), + format!("Expected raw pointer for pointer type. Found `{ptr_ty}` instead"), + ); + } +} diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 0a9a5b56ee9d..2d77fae0c48a 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -308,6 +308,20 @@ macro_rules! kani_intrinsics { assert!(cond, "Safety check failed: {msg}"); } + /// This should indicate that Kani does not support a certain operation. + #[doc(hidden)] + #[allow(dead_code)] + #[kanitool::fn_marker = "UnsupportedCheckHook"] + #[inline(never)] + #[allow(clippy::diverging_sub_expression)] + pub(crate) fn unsupported(msg: &'static str) -> ! { + #[cfg(not(feature = "concrete_playback"))] + return kani_intrinsic(); + + #[cfg(feature = "concrete_playback")] + unimplemented!("Unsupported Kani operation: {msg}") + } + /// An empty body that can be used to define Kani intrinsic functions. /// /// A Kani intrinsic is a function that is interpreted by Kani compiler. diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 5921b52faff2..c09d67ca51ff 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -149,7 +149,14 @@ macro_rules! kani_mem { )] #[allow(clippy::not_unsafe_ptr_arg_deref)] pub fn same_allocation(ptr1: *const T, ptr2: *const T) -> bool { - cbmc::same_allocation(ptr1, ptr2) + same_allocation_internal(ptr1, ptr2) + } + + #[allow(clippy::not_unsafe_ptr_arg_deref)] + pub(super) fn same_allocation_internal(ptr1: *const T, ptr2: *const T) -> bool { + let addr1 = ptr1 as *const (); + let addr2 = ptr2 as *const (); + cbmc::same_allocation(addr1, addr2) } /// Compute the size of the val pointed to if it is safe to do so. @@ -244,7 +251,7 @@ macro_rules! kani_mem { /// /// # Safety /// - /// - Users have to ensure that the pointer is aligned the pointed memory is allocated. + /// - Users have to ensure that the pointed to memory is allocated. #[kanitool::fn_marker = "ValidValueIntrinsic"] #[inline(never)] unsafe fn has_valid_value(_ptr: *const T) -> bool { @@ -270,11 +277,10 @@ macro_rules! kani_mem { pub(super) mod cbmc { use super::*; /// CBMC specific implementation of [super::same_allocation]. - pub fn same_allocation(ptr1: *const T, ptr2: *const T) -> bool { - let addr1 = ptr1 as *const (); - let addr2 = ptr2 as *const (); + pub fn same_allocation(addr1: *const (), addr2: *const ()) -> bool { let obj1 = crate::kani::mem::pointer_object(addr1); (obj1 == crate::kani::mem::pointer_object(addr2)) && { + // TODO(3571): This should be a unsupported check crate::kani::assert( unsafe { is_allocated(addr1, 0) || is_allocated(addr2, 0) }, "Kani does not support reasoning about pointer to unallocated memory", diff --git a/library/kani_core/src/models.rs b/library/kani_core/src/models.rs index c2be6117a7df..121be62fd499 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -16,7 +16,9 @@ macro_rules! generate_models { #[allow(dead_code)] mod rustc_intrinsics { use crate::kani; + use core::convert::TryFrom; use core::ptr::Pointee; + #[kanitool::fn_marker = "SizeOfValRawModel"] pub fn size_of_val_raw(ptr: *const T) -> usize { if let Some(size) = kani::mem::checked_size_of_raw(ptr) { @@ -42,6 +44,78 @@ macro_rules! generate_models { kani::kani_intrinsic() } } + + /// An offset model that checks UB. + #[kanitool::fn_marker = "OffsetModel"] + pub fn offset, O: ToISize>(ptr: P, offset: O) -> P { + let offset = offset.to_isize(); + let t_size = core::mem::size_of::() as isize; + if offset == 0 || t_size == 0 { + // It's always safe to perform an offset of length 0. + ptr + } else { + let (byte_offset, overflow) = offset.overflowing_mul(t_size); + kani::safety_check(!overflow, "Offset in bytes overflows isize"); + let orig_ptr = ptr.to_const_ptr(); + // NOTE: For CBMC, using the pointer addition can have unexpected behavior + // when the offset is higher than the object bits since it will wrap around. + // See for more details: https://github.com/model-checking/kani/issues/1150 + // + // However, when I tried implementing this using usize operation, we got some + // unexpected failures that still require further debugging. + // let new_ptr = orig_ptr.addr().wrapping_add_signed(byte_offset) as *const T; + let new_ptr = orig_ptr.wrapping_byte_offset(byte_offset); + kani::safety_check( + kani::mem::same_allocation_internal(orig_ptr, new_ptr), + "Offset result and original pointer must point to the same allocation", + ); + P::from_const_ptr(new_ptr) + } + } + + pub trait Ptr { + fn to_const_ptr(self) -> *const T; + fn from_const_ptr(ptr: *const T) -> Self; + } + + impl Ptr for *const T { + fn to_const_ptr(self) -> *const T { + self + } + fn from_const_ptr(ptr: *const T) -> Self { + ptr + } + } + + impl Ptr for *mut T { + fn to_const_ptr(self) -> *const T { + self + } + fn from_const_ptr(ptr: *const T) -> Self { + ptr as _ + } + } + + pub trait ToISize { + fn to_isize(self) -> isize; + } + + impl ToISize for isize { + fn to_isize(self) -> isize { + self + } + } + + impl ToISize for usize { + fn to_isize(self) -> isize { + if let Ok(val) = self.try_into() { + val + } else { + kani::safety_check(false, "Offset value overflows isize"); + unreachable!(); + } + } + } } #[allow(dead_code)] diff --git a/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs b/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs index ff2d54e7ca6b..744528b9c32a 100644 --- a/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs +++ b/tests/expected/intrinsics/copy-nonoverlapping/copy-unreadable-src/main.rs @@ -7,10 +7,10 @@ fn test_copy_nonoverlapping_invalid() { let arr: [i32; 3] = [0, 1, 0]; let src: *const i32 = arr.as_ptr(); + // Get an invalid pointer with a negative offset + let src_invalid = src.wrapping_sub(1) as *const i32; + let dst = src.wrapping_add(1) as *mut i32; unsafe { - // Get an invalid pointer with a negative offset - let src_invalid = unsafe { src.sub(1) as *const i32 }; - let dst = src.add(1) as *mut i32; core::intrinsics::copy_nonoverlapping(src_invalid, dst, 1); } } diff --git a/tests/expected/intrinsics/copy/copy-unreadable-src/main.rs b/tests/expected/intrinsics/copy/copy-unreadable-src/main.rs index 2b0e71cc16f3..202900933e00 100644 --- a/tests/expected/intrinsics/copy/copy-unreadable-src/main.rs +++ b/tests/expected/intrinsics/copy/copy-unreadable-src/main.rs @@ -7,10 +7,10 @@ fn test_copy_invalid() { let arr: [i32; 3] = [0, 1, 0]; let src: *const i32 = arr.as_ptr(); + // Get an invalid pointer with a negative offset + let src_invalid = src.wrapping_sub(1) as *const i32; + let dst = src.wrapping_add(1) as *mut i32; unsafe { - // Get an invalid pointer with a negative offset - let src_invalid = unsafe { src.sub(1) as *const i32 }; - let dst = src.add(1) as *mut i32; core::intrinsics::copy(src_invalid, dst, 1); } } diff --git a/tests/expected/offset-bounds-check/fixme_offset_usize.expected b/tests/expected/offset-bounds-check/fixme_offset_usize.expected new file mode 100644 index 000000000000..0b92595e5c61 --- /dev/null +++ b/tests/expected/offset-bounds-check/fixme_offset_usize.expected @@ -0,0 +1,11 @@ +SUMMARY:\ + ** 6 of +Failed Checks: "Expected 0 and 1 to be the only safe values for offset" +Failed Checks: Offset in bytes overflows isize +Failed Checks: Offset result and original pointer must point to the same allocation +Failed Checks: Offset value overflows isize +Failed Checks: "This should fail for delta `1`" +Failed Checks: "This should fail for delta `0`" + +Verification failed for - check_intrinsic_args +Complete - 0 successfully verified harnesses, 1 failures, 1 total. diff --git a/tests/expected/offset-bounds-check/fixme_offset_usize.rs b/tests/expected/offset-bounds-check/fixme_offset_usize.rs new file mode 100644 index 000000000000..d9e10e3483e5 --- /dev/null +++ b/tests/expected/offset-bounds-check/fixme_offset_usize.rs @@ -0,0 +1,31 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check different violations that can be triggered when providing an usize offset +//! with a type that has size > 1. + +#![feature(core_intrinsics)] +use std::intrinsics::offset; +use std::ptr::addr_of; + +/// This harness exercises different scenarios when providing unconstrained offset counter. +/// +/// We expect the following UB to be detected: +/// 1. The offset value, `delta`, itself is greater than `isize::MAX`. +/// 2. The offset in bytes, `delta * size_of::()`, is greater than `isize::MAX`. +/// 3. Offset result does not point to the same allocation as the original pointer. +/// +/// The offset operation should only succeed for delta values: +/// - `0`: The new pointer is the same as the base of the array. +/// - `1`: The new pointer points to the end of the allocation. +/// +/// FIXME: Because of CBMC wrapping behavior with pointer arithmetic, the assertion that checks +/// that `delta <= 1` currently fails. See . +#[kani::proof] +fn check_intrinsic_args() { + let array = [0u32]; + let delta: usize = kani::any(); + let new = unsafe { offset(addr_of!(array), delta) }; + assert!(delta <= 1, "Expected 0 and 1 to be the only safe values for offset"); + assert_eq!(new, &array, "This should fail for delta `1`"); + assert_ne!(new, &array, "This should fail for delta `0`"); +} diff --git a/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected b/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected new file mode 100644 index 000000000000..d8c6e135adc9 --- /dev/null +++ b/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected @@ -0,0 +1,4 @@ +Failed Checks: Offset result and original pointer must point to the same allocation +Verification failed for - check_ptr_oob + +Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/expected/offset-bounds-check/out_of_bounds_ub_check.rs b/tests/expected/offset-bounds-check/out_of_bounds_ub_check.rs new file mode 100644 index 000000000000..e6b4310269a1 --- /dev/null +++ b/tests/expected/offset-bounds-check/out_of_bounds_ub_check.rs @@ -0,0 +1,26 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check that Kani offset operations correctly detect out-of-bound access. + +/// Verification should fail because safety violation is not a regular panic. +#[kani::proof] +#[kani::should_panic] +fn check_ptr_oob() { + let array = [0]; + let base_ptr = array.as_ptr(); + // SAFETY: This is unsafe and it will trigger UB. + let oob_ptr = unsafe { base_ptr.sub(1) }; + // Just use the pointer to avoid warnings + assert_ne!(oob_ptr.addr(), base_ptr.addr()); +} + +/// Verification should succeed. +#[kani::proof] +fn check_ptr_end() { + let array = [0]; + let base_ptr = array.as_ptr(); + // Safety: This should be OK since the pointer is pointing to the end of the allocation. + let end_ptr = unsafe { base_ptr.add(1) }; + // Safety: Pointers point to the same allocation + assert_eq!(unsafe { end_ptr.offset_from(base_ptr) }, 1); +} diff --git a/tests/expected/offset-bounds-check/start_from_oob.expected b/tests/expected/offset-bounds-check/start_from_oob.expected new file mode 100644 index 000000000000..5109d3ef8a54 --- /dev/null +++ b/tests/expected/offset-bounds-check/start_from_oob.expected @@ -0,0 +1,4 @@ +Failed Checks: Offset result and original pointer must point to the same allocation +Verification failed for - check_add_to_oob + +Complete - 0 successfully verified harnesses, 1 failures, 1 total. diff --git a/tests/expected/offset-bounds-check/start_from_oob.rs b/tests/expected/offset-bounds-check/start_from_oob.rs new file mode 100644 index 000000000000..32713bbd41ee --- /dev/null +++ b/tests/expected/offset-bounds-check/start_from_oob.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check that Kani offset operations correctly detect out-of-bound access. + +/// Offset from a pointer that is out of bounds should be invalid even if it goes back to the +/// original allocation. +#[kani::proof] +fn check_add_to_oob() { + let array = [0]; + let base_ptr = array.as_ptr(); + let oob_ptr = base_ptr.wrapping_sub(1); + // SAFETY: Very unsound operation due to out-of-bounds pointer. + // This should trigger safety violation. + let back_base = unsafe { oob_ptr.add(1) }; + assert_eq!(base_ptr, back_base); +} diff --git a/tests/expected/offset-bytes-overflow/expected b/tests/expected/offset-bytes-overflow/expected index 1f13adcc7776..214bd1d0e149 100644 --- a/tests/expected/offset-bytes-overflow/expected +++ b/tests/expected/offset-bytes-overflow/expected @@ -1,2 +1,4 @@ -FAILURE\ -offset: attempt to compute number in bytes which would overflow \ No newline at end of file +Failed Checks: Offset in bytes overflows isize +Verification failed for - check_wrap_offset + +Complete - 0 successfully verified harnesses, 1 failures, 1 total. diff --git a/tests/expected/offset-from-bytes-overflow/expected b/tests/expected/offset-from-bytes-overflow/expected index bcf0242f9e9d..0cbd5aafc40c 100644 --- a/tests/expected/offset-from-bytes-overflow/expected +++ b/tests/expected/offset-from-bytes-overflow/expected @@ -1,2 +1,4 @@ -FAILURE\ -attempt to compute number in bytes which would overflow +Failed Checks: Offset in bytes overflows isize +Verification failed for - main + +Complete - 0 successfully verified harnesses, 1 failures, 1 total. diff --git a/tests/expected/offset-invalid-args/invalid_offset_ty.expected b/tests/expected/offset-invalid-args/invalid_offset_ty.expected new file mode 100644 index 000000000000..0273b7633089 --- /dev/null +++ b/tests/expected/offset-invalid-args/invalid_offset_ty.expected @@ -0,0 +1 @@ +Cannot offset by non-isize type u32 diff --git a/tests/expected/offset-invalid-args/invalid_offset_ty.rs b/tests/expected/offset-invalid-args/invalid_offset_ty.rs new file mode 100644 index 000000000000..4e3a479fe6af --- /dev/null +++ b/tests/expected/offset-invalid-args/invalid_offset_ty.rs @@ -0,0 +1,16 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check Kani output if the arguments provided to the offset intrinsic are incorrect. + +#![feature(core_intrinsics)] +use std::intrinsics::offset; +use std::ptr::addr_of; + +/// The rust compiler currently ICE. +#[kani::proof] +fn check_intrinsic_args() { + let array = [0]; + let delta: u32 = kani::any(); + let new = unsafe { offset(addr_of!(array), delta) }; + assert_ne!(new, &array) +} diff --git a/tests/expected/offset-invalid-args/non_ptr_arg.expected b/tests/expected/offset-invalid-args/non_ptr_arg.expected new file mode 100644 index 000000000000..3a89d41b5d7c --- /dev/null +++ b/tests/expected/offset-invalid-args/non_ptr_arg.expected @@ -0,0 +1 @@ +Cannot offset non-pointer type diff --git a/tests/expected/offset-invalid-args/non_ptr_arg.rs b/tests/expected/offset-invalid-args/non_ptr_arg.rs new file mode 100644 index 000000000000..b32d9f0534cf --- /dev/null +++ b/tests/expected/offset-invalid-args/non_ptr_arg.rs @@ -0,0 +1,15 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check Kani output if the arguments provided to the offset intrinsic are incorrect. + +#![feature(core_intrinsics)] +use std::intrinsics::offset; + +/// The rust compiler currently ICE. +#[kani::proof] +fn check_intrinsic_args() { + let array = [0]; + let delta: usize = kani::any(); + let new = unsafe { offset(&array, delta) }; + assert_ne!(new, &array) +} diff --git a/tests/expected/offset-overflow/expected b/tests/expected/offset-overflow/expected index 9613638bf8f9..af5ea73875ca 100644 --- a/tests/expected/offset-overflow/expected +++ b/tests/expected/offset-overflow/expected @@ -1,2 +1,4 @@ -FAILURE\ -attempt to compute offset which would overflow +Failed Checks: Offset result and original pointer must point to the same allocation +Verification failed for - test_offset_overflow + +Complete - 0 successfully verified harnesses, 1 failures, 1 total. diff --git a/tests/expected/offset-wraps-around/expected b/tests/expected/offset-wraps-around/expected index cacc000d09e5..2fedc9da1a89 100644 --- a/tests/expected/offset-wraps-around/expected +++ b/tests/expected/offset-wraps-around/expected @@ -1,2 +1,12 @@ -FAILURE\ -assertion failed: high_offset == wrapped_offset.try_into().unwrap() \ No newline at end of file +Checking harness check_wrap_around_ptr... +VERIFICATION:- SUCCESSFUL + +Checking harness harness_without_ub... +VERIFICATION:- SUCCESSFUL + +Checking harness original_harness... +Failed Checks: assertion failed: high_offset == wrapped_offset.try_into().unwrap() +VERIFICATION:- FAILED + +Verification failed for - original_harness +Complete - 2 successfully verified harnesses, 1 failures, 3 total. \ No newline at end of file diff --git a/tests/expected/offset-wraps-around/main.rs b/tests/expected/offset-wraps-around/main.rs index 3e83eacc4c2d..205ba56cb3e1 100644 --- a/tests/expected/offset-wraps-around/main.rs +++ b/tests/expected/offset-wraps-around/main.rs @@ -1,35 +1,49 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// Check that a high offset causes a "wrapping around" behavior in CBMC. +//! This test checks that Kani correctly computes the value of a wrapping_offset in cases where +//! the add operation wraps. +//! +//! Note that CBMC offset logic will wrap around the object bits, not the entire address space, when +//! computing the offset between pointers. +//! See for more details. -// This example can be really confusing. This program works fine in Rust and -// it's okay to assert that the value coming from `offset_from` is equal to -// `high_offset`. But CBMC's memory model is going to cause a "wrapping around" -// behavior in `v_wrap`, so any values that depend on it are going to show a -// strange behavior as well. use std::convert::TryInto; #[kani::proof] -fn main() { +fn original_harness() { let v: &[u128] = &[0; 10]; let v_0: *const u128 = &v[0]; let high_offset = usize::MAX / (std::mem::size_of::() * 4); - unsafe { - // Adding `high offset` to `v_0` is undefined behavior, but Kani's - // default behavior does not report it. This kind of operations - // are quite common in the standard library, and we disabled such - // checks in order to avoid spurious verification failures. - // - // Note that this instance of undefined behavior will be reported - // by `miri` and also by Kani with `--extra-pointer-checks`. - // Also, dereferencing the pointer will also be reported by Kani's - // default behavior. - let v_wrap: *const u128 = v_0.add(high_offset.try_into().unwrap()); - let wrapped_offset = v_wrap.offset_from(v_0); - // Both offsets should be the same, but because of the "wrapping around" - // behavior in CBMC, `wrapped_offset` does not equal `high_offset` - // https://github.com/model-checking/kani/issues/1150 - assert!(high_offset == wrapped_offset.try_into().unwrap()); - } + let v_wrap: *const u128 = v_0.wrapping_add(high_offset); + // FIX-ME: This should trigger UB!! + // https://github.com/model-checking/kani/issues/3756 + let wrapped_offset = unsafe { v_wrap.offset_from(v_0) }; + // Without UB detection, the offsets are the same, but CBMC pointer arithmetic + // would "wrap around" making this incorrect + // https://github.com/model-checking/kani/issues/1150 + assert!(high_offset == wrapped_offset.try_into().unwrap()); +} + +/// This harness is similar to the `original_harness`, but we replace the `offset_from` with +/// a subtraction on the pointer addresses. +#[kani::proof] +fn harness_without_ub() { + let v: &[u128] = &[0; 10]; + let v_0: *const u128 = &v[0]; + let high_offset = usize::MAX / (size_of::() * 4); + let v_wrap: *const u128 = v_0.wrapping_add(high_offset); + // The only way to compute offset of pointers out of bounds is to convert them to integers. + let wrapped_offset = (v_wrap.addr() - v_0.addr()) / size_of::(); + // Now this should work + assert_eq!(high_offset, wrapped_offset); +} + +/// Check that wrapping offset by `usize::MAX + 1` bytes will result in the same base pointer. +#[kani::proof] +fn check_wrap_around_ptr() { + let v: &[u128] = &[0; 10]; + let orig_ptr: *const u128 = &v[0]; + let new_ptr: *const u128 = orig_ptr.wrapping_byte_add(usize::MAX).wrapping_byte_add(1); + assert_eq!(orig_ptr as usize, new_ptr as usize); } diff --git a/tests/expected/pointer-overflow/expected b/tests/expected/pointer-overflow/expected index 3701d77c8bfd..89a84309199b 100644 --- a/tests/expected/pointer-overflow/expected +++ b/tests/expected/pointer-overflow/expected @@ -1,2 +1 @@ -Status: FAILURE\ -offset: attempt to compute number in bytes which would overflow +Failed Checks: Offset in bytes overflows isize diff --git a/tests/expected/pointer-overflow/main.rs b/tests/expected/pointer-overflow/main.rs index 9c8dc52bddf0..c78cf4027351 100644 --- a/tests/expected/pointer-overflow/main.rs +++ b/tests/expected/pointer-overflow/main.rs @@ -1,7 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT // -// kani-flags: --enable-unstable --extra-pointer-checks // Checks that overflows for pointer arithmetic are reported #[kani::proof] diff --git a/tests/expected/ptr-offset-overflow-bytes/expected b/tests/expected/ptr-offset-overflow-bytes/expected index ad33ce91dabb..f76a6aa699cf 100644 --- a/tests/expected/ptr-offset-overflow-bytes/expected +++ b/tests/expected/ptr-offset-overflow-bytes/expected @@ -1,5 +1,3 @@ -std::ptr::const_ptr::::offset.arithmetic_overflow\ -Status: FAILURE\ -Description: "offset: attempt to compute number in bytes which would overflow" - -VERIFICATION:- FAILED +Failed Checks: Offset in bytes overflows isize +Verification failed for - main +Complete - 0 successfully verified harnesses, 1 failures, 1 total. diff --git a/tests/expected/ptr_to_ref_cast/slice/test.rs b/tests/expected/ptr_to_ref_cast/slice/test.rs index 8526d0bf1c7f..b9e4d54546f6 100644 --- a/tests/expected/ptr_to_ref_cast/slice/test.rs +++ b/tests/expected/ptr_to_ref_cast/slice/test.rs @@ -31,6 +31,6 @@ fn check_with_byte_add_sub_pass() { let ptr = &data as *const [u8]; let offset = kani::any_where(|i| *i < 100); // This should pass since the resulting metadata is valid - let val = unsafe { &*ptr.byte_add(offset).byte_sub(offset) }; + let val = unsafe { &*ptr.wrapping_byte_add(offset).wrapping_byte_sub(offset) }; assert_eq!(val.len(), data.len()); } diff --git a/tests/expected/raw_slice/expected b/tests/expected/raw_slice/expected index 1b863417c02c..d2bd2b505ef7 100644 --- a/tests/expected/raw_slice/expected +++ b/tests/expected/raw_slice/expected @@ -62,8 +62,7 @@ Description: "assertion failed: slice.others[0] == second"\ slice.rs:96:5 in function check_naive_iterator_should_fail Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -slice.rs:100:32 in function check_naive_iterator_should_fail +Description: "Offset result and original pointer must point to the same allocation" VERIFICATION:- FAILED diff --git a/tests/expected/raw_slice_c_repr/expected b/tests/expected/raw_slice_c_repr/expected index 9271825be7cd..d0097ffc1349 100644 --- a/tests/expected/raw_slice_c_repr/expected +++ b/tests/expected/raw_slice_c_repr/expected @@ -62,8 +62,7 @@ Description: "assertion failed: slice.others[0] == second"\ in function check_naive_iterator_should_fail Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -in function check_naive_iterator_should_fail +Description: "Offset result and original pointer must point to the same allocation" VERIFICATION:- FAILED diff --git a/tests/expected/raw_slice_packed/expected b/tests/expected/raw_slice_packed/expected index 9271825be7cd..d0097ffc1349 100644 --- a/tests/expected/raw_slice_packed/expected +++ b/tests/expected/raw_slice_packed/expected @@ -62,8 +62,7 @@ Description: "assertion failed: slice.others[0] == second"\ in function check_naive_iterator_should_fail Status: FAILURE\ -Description: "dereference failure: pointer outside object bounds"\ -in function check_naive_iterator_should_fail +Description: "Offset result and original pointer must point to the same allocation" VERIFICATION:- FAILED diff --git a/tests/kani/PointerOffset/fixme_wrap_nonzero_offset.rs b/tests/kani/PointerOffset/fixme_wrap_nonzero_offset.rs new file mode 100644 index 000000000000..fdc0496ff648 --- /dev/null +++ b/tests/kani/PointerOffset/fixme_wrap_nonzero_offset.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! Testcase for issue [#1150](https://github.com/model-checking/kani/issues/1150) that shows +//! bug with wrapping offset operations in Kani. + +/// This harness shows the issue with the current implementation of wrapping offset. +/// +/// Invoking `wrapping_byte_offset` should return a pointer that is different from the original +/// pointer if the offset value is not 0. +/// See issue [#1150](https://github.com/model-checking/kani/issues/1150). +#[kani::proof] +fn fixme_incorrect_wrapping_offset() { + let ptr: *const u8 = &0u8; + let offset = kani::any_where(|v: &isize| *v != 0); + let new_ptr = ptr.wrapping_byte_offset(offset); + assert_ne!(ptr, new_ptr, "Expected new_ptr to be different than ptr"); +} diff --git a/tests/kani/ValidValues/unaligned.rs b/tests/kani/ValidValues/unaligned.rs new file mode 100644 index 000000000000..dc1d3d897211 --- /dev/null +++ b/tests/kani/ValidValues/unaligned.rs @@ -0,0 +1,37 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z valid-value-checks -Z mem-predicates +//! Check that Kani can check value validity of packed structs. + +use std::ptr::addr_of; + +#[repr(C, packed)] +#[derive(kani::Arbitrary)] +struct Packed { + byte: u8, + c: char, +} + +#[kani::proof] +pub fn check_packed_deref() { + let packed: Packed = kani::any(); + assert!(kani::mem::can_dereference(addr_of!(packed))); + assert!(kani::mem::can_dereference(addr_of!(packed.byte))); + assert!(!kani::mem::can_dereference(addr_of!(packed.c))); +} + +#[kani::proof] +pub fn check_packed_read_unaligned() { + let packed: Packed = kani::any(); + assert!(kani::mem::can_read_unaligned(addr_of!(packed))); + assert!(kani::mem::can_read_unaligned(addr_of!(packed.byte))); + assert!(kani::mem::can_read_unaligned(addr_of!(packed.c))); +} + +#[kani::proof] +pub fn check_packed_read_unaligned_invalid_value() { + const SZ: usize = size_of::(); + let val = [u8::MAX; SZ]; + let ptr = addr_of!(val) as *const Packed; + assert!(!kani::mem::can_read_unaligned(ptr)); +} diff --git a/tests/kani/Vectors/vector_extend_bytes.rs b/tests/kani/Vectors/vector_extend_bytes.rs index 2c48dcfc4653..52f68bcb3ff8 100644 --- a/tests/kani/Vectors/vector_extend_bytes.rs +++ b/tests/kani/Vectors/vector_extend_bytes.rs @@ -1,10 +1,11 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! Check that we propertly handle `Vec::extend` with a constant byte slice. +//! Check that we properly handle `Vec::extend` with a constant byte slice. //! This used to fail previously (see //! https://github.com/model-checking/kani/issues/2656). +#[kani::unwind(4)] #[kani::proof] fn check_extend_const_byte_slice() { const MY_CONSTANT: &[u8] = b"Hi";