From ed7e698f38728aeb44ca63bf2489fb22cabb7998 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 4 Dec 2024 17:30:49 -0800 Subject: [PATCH 01/10] Implement bounds check on offset Still need to adjust tests --- .../codegen_cprover_gotoc/codegen/assert.rs | 11 +- .../codegen/intrinsic.rs | 2 +- .../codegen_cprover_gotoc/codegen/rvalue.rs | 43 ++----- .../codegen_cprover_gotoc/overrides/hooks.rs | 72 +++++++---- .../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 | 67 ++++++++++ .../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 +++ .../offset-invalid-args/invalid_args.expected | 1 + .../offset-invalid-args/invalid_args.rs | 15 +++ tests/expected/offset-wraps-around/main.rs | 64 +++++++--- tests/kani/ValidValues/unaligned.rs | 39 ++++++ 18 files changed, 423 insertions(+), 97 deletions(-) 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_args.expected create mode 100644 tests/expected/offset-invalid-args/invalid_args.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..82817fc6178f 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. 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 ExactDiv, - /// Another instrinsic check. + /// Another intrinsic check. /// - /// SPECIAL BEHAVIOR: None TODO: Why should this exist? + /// SPECIAL BEHAVIOR: Same as 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..3eebf1abb7ab 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -134,15 +134,10 @@ 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, @@ -150,6 +145,25 @@ impl GotocHook for Assert { } } +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, + fargs: Vec, + _assign_to: &Place, + target: Option, + span: Span, + ) -> Stmt { + check_hook(PropertyClass::UnsupportedConstruct, gcx, fargs, target, span) + } +} + struct SafetyCheck; impl GotocHook for SafetyCheck { fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool { @@ -160,24 +174,12 @@ impl GotocHook for SafetyCheck { &self, gcx: &mut GotocCtx, _instance: Instance, - mut fargs: Vec, + fargs: Vec, _assign_to: &Place, target: Option, span: Span, ) -> Stmt { - assert_eq!(fargs.len(), 2); - let cond = fargs.remove(0).cast_to(Type::bool()); - let msg = fargs.remove(0); - 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::SafetyCheck, &msg, caller_loc), - Stmt::goto(bb_label(target), caller_loc), - ], - caller_loc, - ) + check_hook(PropertyClass::SafetyCheck, gcx, fargs, target, span) } } @@ -205,10 +207,15 @@ impl GotocHook for Check { 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, - gcx.codegen_assert(cond, PropertyClass::Assertion, &msg, caller_loc), + decl, + gcx.codegen_assert(tmp, PropertyClass::Assertion, &msg, caller_loc), Stmt::goto(bb_label(target), caller_loc), ], caller_loc, @@ -709,6 +716,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)), @@ -747,3 +755,25 @@ impl GotocHooks { } } } + +fn check_hook( + prop_class: PropertyClass, + gcx: &mut GotocCtx, + mut fargs: Vec, + 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, prop_class, &msg, caller_loc), + Stmt::goto(bb_label(target), caller_loc), + ], + caller_loc, + ) +} 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..31a676f95272 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,71 @@ 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 as isize); + kani::safety_check(!overflow, "Offset in bytes overflow isize"); + let orig_ptr = ptr.to_const_ptr(); + 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 should 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 in bytes overflow isize"); + unreachable!(); + } + } + } } #[allow(dead_code)] 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..099cbdcd9f1c --- /dev/null +++ b/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected @@ -0,0 +1,4 @@ +Failed Checks: Offset result is out of bounds of initial 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..fc5fbdfb365a --- /dev/null +++ b/tests/expected/offset-bounds-check/start_from_oob.expected @@ -0,0 +1,4 @@ +Failed Checks: Offset result is out of bounds of initial 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-invalid-args/invalid_args.expected b/tests/expected/offset-invalid-args/invalid_args.expected new file mode 100644 index 000000000000..3a89d41b5d7c --- /dev/null +++ b/tests/expected/offset-invalid-args/invalid_args.expected @@ -0,0 +1 @@ +Cannot offset non-pointer type diff --git a/tests/expected/offset-invalid-args/invalid_args.rs b/tests/expected/offset-invalid-args/invalid_args.rs new file mode 100644 index 000000000000..bd5468afb9c7 --- /dev/null +++ b/tests/expected/offset-invalid-args/invalid_args.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 intrisic 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: u32 = kani::any(); + let new = unsafe { offset(&array, delta) }; + assert_ne!(new, &array) +} diff --git a/tests/expected/offset-wraps-around/main.rs b/tests/expected/offset-wraps-around/main.rs index 3e83eacc4c2d..da162cc8f1e3 100644 --- a/tests/expected/offset-wraps-around/main.rs +++ b/tests/expected/offset-wraps-around/main.rs @@ -1,35 +1,59 @@ // 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 space address when +//! computing the offset between pointers. Doing that is UB in Rust, so we should be OK +//! as long as Kani can detect UB in that case. -// 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` + let v_wrap: *const u128 = v_0.wrapping_add(high_offset); + // This should trigger UB!! + let wrapped_offset = unsafe { v_wrap.offset_from(v_0) }; + // Without UB detection, the offsets are the same, but CBMC pointer arithmetic + // would "wrapping 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); + unsafe { + 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); + } +} + +#[kani::proof] +fn check_wrap_ptr_max() { + 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); +} + +#[kani::proof] +fn check_wrap_ptr_10_bits() { + let v: &[u128] = &[0; 10]; + let orig_ptr: *const u128 = &v[0]; + let new_ptr: *const u128 = orig_ptr.wrapping_byte_add(1 << 63); + assert_ne!(orig_ptr as usize, new_ptr as usize); +} diff --git a/tests/kani/ValidValues/unaligned.rs b/tests/kani/ValidValues/unaligned.rs new file mode 100644 index 000000000000..695f74ebf1b4 --- /dev/null +++ b/tests/kani/ValidValues/unaligned.rs @@ -0,0 +1,39 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z valid-value-checks +//! 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)); + assert!(kani::mem::can_read_unaligned(unsafe { addr_of!((*ptr).byte) })); + assert!(!kani::mem::can_read_unaligned(unsafe { addr_of!((*ptr).c) })); +} From 1632b67680defe00051ee8ea27a4b0870e45ae5c Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 4 Dec 2024 18:36:01 -0800 Subject: [PATCH 02/10] Fix tests after enabling offset bound checks --- .../copy-nonoverlapping/copy-unreadable-src/main.rs | 6 +++--- .../expected/intrinsics/copy/copy-unreadable-src/main.rs | 6 +++--- .../offset-bounds-check/out_of_bounds_ub_check.expected | 2 +- .../expected/offset-bounds-check/start_from_oob.expected | 2 +- tests/expected/offset-bytes-overflow/expected | 6 ++++-- tests/expected/offset-from-bytes-overflow/expected | 6 ++++-- tests/expected/offset-overflow/expected | 6 ++++-- tests/expected/pointer-overflow/expected | 3 +-- tests/expected/pointer-overflow/main.rs | 1 - tests/expected/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 +-- tests/kani/ValidValues/unaligned.rs | 4 +--- 15 files changed, 29 insertions(+), 32 deletions(-) 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/out_of_bounds_ub_check.expected b/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected index 099cbdcd9f1c..62b518815bb0 100644 --- a/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected +++ b/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected @@ -1,4 +1,4 @@ -Failed Checks: Offset result is out of bounds of initial allocation +Failed Checks: Offset result and original pointer should 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/start_from_oob.expected b/tests/expected/offset-bounds-check/start_from_oob.expected index fc5fbdfb365a..fc766c277581 100644 --- a/tests/expected/offset-bounds-check/start_from_oob.expected +++ b/tests/expected/offset-bounds-check/start_from_oob.expected @@ -1,4 +1,4 @@ -Failed Checks: Offset result is out of bounds of initial allocation +Failed Checks: Offset result and original pointer should 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-bytes-overflow/expected b/tests/expected/offset-bytes-overflow/expected index 1f13adcc7776..8eae686f2142 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 overflow 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..51f9bfb293a0 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 overflow isize +Verification failed for - main + +Complete - 0 successfully verified harnesses, 1 failures, 1 total. diff --git a/tests/expected/offset-overflow/expected b/tests/expected/offset-overflow/expected index 9613638bf8f9..ba7d1c2fe7df 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 should 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/pointer-overflow/expected b/tests/expected/pointer-overflow/expected index 3701d77c8bfd..a6319eb7d1f1 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 overflow 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..a258cb026a1a 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 overflow 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..73a625248d51 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 should 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..eca589cdd260 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 should 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..eca589cdd260 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 should point to the same allocation" VERIFICATION:- FAILED diff --git a/tests/kani/ValidValues/unaligned.rs b/tests/kani/ValidValues/unaligned.rs index 695f74ebf1b4..dc1d3d897211 100644 --- a/tests/kani/ValidValues/unaligned.rs +++ b/tests/kani/ValidValues/unaligned.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z valid-value-checks +// kani-flags: -Z valid-value-checks -Z mem-predicates //! Check that Kani can check value validity of packed structs. use std::ptr::addr_of; @@ -34,6 +34,4 @@ pub fn check_packed_read_unaligned_invalid_value() { let val = [u8::MAX; SZ]; let ptr = addr_of!(val) as *const Packed; assert!(!kani::mem::can_read_unaligned(ptr)); - assert!(kani::mem::can_read_unaligned(unsafe { addr_of!((*ptr).byte) })); - assert!(!kani::mem::can_read_unaligned(unsafe { addr_of!((*ptr).c) })); } From 0f027cf57658eaa6d42121cc6b83b84799d4ae4e Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 4 Dec 2024 20:31:01 -0800 Subject: [PATCH 03/10] Add UB checks for `ptr_offset_from*` intrinsics Add a new model for `ptr_offset_from` and `ptr_offset_from_unsigned` intrinsics that check allocation and address order. --- .../codegen/intrinsic.rs | 84 ++----------------- .../src/kani_middle/kani_functions.rs | 4 + .../kani_middle/transform/rustc_intrinsics.rs | 2 + library/kani_core/src/models.rs | 33 ++++++++ .../offset-bounds-check/offset_from.expected | 6 ++ .../offset-bounds-check/offset_from.rs | 47 +++++++++++ .../offset-bounds-check/sub_ptr.expected | 65 ++++++++++++++ tests/expected/offset-bounds-check/sub_ptr.rs | 70 ++++++++++++++++ 8 files changed, 232 insertions(+), 79 deletions(-) create mode 100644 tests/expected/offset-bounds-check/offset_from.expected create mode 100644 tests/expected/offset-bounds-check/offset_from.rs create mode 100644 tests/expected/offset-bounds-check/sub_ptr.expected create mode 100644 tests/expected/offset-bounds-check/sub_ptr.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 654a7f2b6861..bd103fe4e45e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -7,9 +7,7 @@ use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable; use crate::codegen_cprover_gotoc::{GotocCtx, utils}; use crate::intrinsics::Intrinsic; use crate::unwrap_or_return_codegen_unimplemented_stmt; -use cbmc::goto_program::{ - ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type, -}; +use cbmc::goto_program::{BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type}; use rustc_middle::ty::TypingEnv; use rustc_middle::ty::layout::ValidityRequirement; use rustc_smir::rustc_internal; @@ -425,10 +423,6 @@ impl GotocCtx<'_> { Intrinsic::PowIF64 => codegen_simple_intrinsic!(Powi), Intrinsic::PrefAlignOf => codegen_intrinsic_const!(), Intrinsic::PtrGuaranteedCmp => self.codegen_ptr_guaranteed_cmp(fargs, place, loc), - Intrinsic::PtrOffsetFrom => self.codegen_ptr_offset_from(fargs, place, loc), - Intrinsic::PtrOffsetFromUnsigned => { - self.codegen_ptr_offset_from_unsigned(fargs, place, loc) - } Intrinsic::RawEq => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc), Intrinsic::RetagBoxToRaw => self.codegen_retag_box_to_raw(fargs, place, loc), Intrinsic::RintF32 => codegen_simple_intrinsic!(Rintf), @@ -546,7 +540,10 @@ impl GotocCtx<'_> { assert!(self.place_ty_stable(place).kind().is_unit()); self.codegen_write_bytes(fargs, farg_types, loc) } - Intrinsic::SizeOfVal | Intrinsic::MinAlignOfVal => { + Intrinsic::PtrOffsetFrom + | Intrinsic::PtrOffsetFromUnsigned + | Intrinsic::SizeOfVal + | Intrinsic::MinAlignOfVal => { unreachable!("Intrinsic `{}` is handled before codegen", intrinsic_str) } // Unimplemented @@ -1025,77 +1022,6 @@ impl GotocCtx<'_> { self.codegen_expr_to_place_stable(p, dst_ptr, loc) } - /// ptr_offset_from returns the offset between two pointers - /// - fn codegen_ptr_offset_from(&mut self, fargs: Vec, p: &Place, loc: Location) -> Stmt { - let (offset_expr, offset_overflow) = self.codegen_ptr_offset_from_expr(fargs); - - // Check that computing `offset` in bytes would not overflow an `isize` - // These checks may allow a wrapping-around behavior in CBMC: - // https://github.com/model-checking/kani/issues/1150 - let overflow_check = self.codegen_assert_assume( - offset_overflow.overflowed.not(), - PropertyClass::ArithmeticOverflow, - "attempt to compute offset in bytes which would overflow an `isize`", - loc, - ); - - let offset_expr = self.codegen_expr_to_place_stable(p, offset_expr, loc); - Stmt::block(vec![overflow_check, offset_expr], loc) - } - - /// `ptr_offset_from_unsigned` returns the offset between two pointers where the order is known. - /// The logic is similar to `ptr_offset_from` but the return value is a `usize`. - /// See for more details - fn codegen_ptr_offset_from_unsigned( - &mut self, - fargs: Vec, - p: &Place, - loc: Location, - ) -> Stmt { - let (offset_expr, offset_overflow) = self.codegen_ptr_offset_from_expr(fargs); - - // Check that computing `offset` in bytes would not overflow an `isize` - // These checks may allow a wrapping-around behavior in CBMC: - // https://github.com/model-checking/kani/issues/1150 - let overflow_check = self.codegen_assert_assume( - offset_overflow.overflowed.not(), - PropertyClass::ArithmeticOverflow, - "attempt to compute offset in bytes which would overflow an `isize`", - loc, - ); - - let non_negative_check = self.codegen_assert_assume( - offset_overflow.result.is_non_negative(), - PropertyClass::SafetyCheck, - "attempt to compute unsigned offset with negative distance", - loc, - ); - - let offset_expr = - self.codegen_expr_to_place_stable(p, offset_expr.cast_to(Type::size_t()), loc); - Stmt::block(vec![overflow_check, non_negative_check, offset_expr], loc) - } - - /// Both `ptr_offset_from` and `ptr_offset_from_unsigned` return the offset between two pointers. - /// This function implements the common logic between them. - fn codegen_ptr_offset_from_expr( - &mut self, - mut fargs: Vec, - ) -> (Expr, ArithmeticOverflowResult) { - let dst_ptr = fargs.remove(0); - let src_ptr = fargs.remove(0); - - // Compute the offset with standard substraction using `isize` - let cast_dst_ptr = dst_ptr.clone().cast_to(Type::ssize_t()); - let cast_src_ptr = src_ptr.clone().cast_to(Type::ssize_t()); - let offset_overflow = cast_dst_ptr.sub_overflow(cast_src_ptr); - - // Re-compute the offset with standard substraction (no casts this time) - let ptr_offset_expr = dst_ptr.sub(src_ptr); - (ptr_offset_expr, offset_overflow) - } - /// A transmute is a bitcast from the argument type to the return type. /// /// diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 38522fae837f..8d1ab5ef939d 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -83,6 +83,10 @@ pub enum KaniModel { IsSlicePtrInitialized, #[strum(serialize = "OffsetModel")] Offset, + #[strum(serialize = "PtrOffsetFromModel")] + PtrOffsetFrom, + #[strum(serialize = "PtrSubPtrModel")] + PtrSubPtr, #[strum(serialize = "RunContractModel")] RunContract, #[strum(serialize = "RunLoopContractModel")] diff --git a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs index ad4238574d63..79238e423e62 100644 --- a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs @@ -167,6 +167,8 @@ impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_> { let model = match intrinsic { Intrinsic::SizeOfVal => self.models[&KaniModel::SizeOfVal], Intrinsic::MinAlignOfVal => self.models[&KaniModel::AlignOfVal], + Intrinsic::PtrOffsetFrom => self.models[&KaniModel::PtrOffsetFrom], + Intrinsic::PtrOffsetFromUnsigned => self.models[&KaniModel::PtrSubPtr], // The rest is handled in codegen. _ => { return self.super_terminator(term); diff --git a/library/kani_core/src/models.rs b/library/kani_core/src/models.rs index 31a676f95272..a754efcd0f7a 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -45,6 +45,39 @@ macro_rules! generate_models { } } + #[kanitool::fn_marker = "PtrOffsetFromModel"] + pub unsafe fn ptr_offset_from(ptr1: *const T, ptr2: *const T) -> isize { + if ptr1 == ptr2 { + 0 + } else { + kani::safety_check( + kani::mem::same_allocation_internal(ptr1, ptr2), + "Offset result and original pointer should point to the same allocation", + ); + kani::safety_check( + core::mem::size_of::() > 0, + "Cannot compute offset of a ZST", + ); + // The offset must fit in isize since this represents the same allocation. + let offset_bytes = ptr1.addr().wrapping_sub(ptr2.addr()) as isize; + // We know `t_size` is a power of two, so avoid division. + let t_size = size_of::() as isize; + kani::safety_check( + offset_bytes & (t_size - 1) == 0, + "Expected the distance between the pointers, in bytes, to be a + multiple of the size of `T`", + ); + offset_bytes >> t_size.trailing_zeros() + } + } + + #[kanitool::fn_marker = "PtrSubPtrModel"] + pub unsafe fn ptr_sub_ptr(ptr1: *const T, ptr2: *const T) -> usize { + let offset = ptr_offset_from(ptr1, ptr2); + kani::safety_check(offset >= 0, "Expected non-negative distance between pointers"); + offset as usize + } + /// An offset model that checks UB. #[kanitool::fn_marker = "OffsetModel"] pub fn offset, O: ToISize>(ptr: P, offset: O) -> P { diff --git a/tests/expected/offset-bounds-check/offset_from.expected b/tests/expected/offset-bounds-check/offset_from.expected new file mode 100644 index 000000000000..d985c9a4e318 --- /dev/null +++ b/tests/expected/offset-bounds-check/offset_from.expected @@ -0,0 +1,6 @@ +Failed Checks: assertion failed: 0 < pointee_size && pointee_size <= isize::MAX as usize +Failed Checks: Offset result and original pointer should point to the same allocation + +Verification failed for - check_offset_from_diff_alloc +Verification failed for - check_offset_from_oob_ptr +Complete - 2 successfully verified harnesses, 2 failures, 4 total. diff --git a/tests/expected/offset-bounds-check/offset_from.rs b/tests/expected/offset-bounds-check/offset_from.rs new file mode 100644 index 000000000000..7ce3edcb3657 --- /dev/null +++ b/tests/expected/offset-bounds-check/offset_from.rs @@ -0,0 +1,47 @@ +// 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_offset_from_oob_ptr() { + let val = 10u128; + let ptr: *const u128 = &val; + let ptr_oob: *const u128 = ptr.wrapping_add(10); + // SAFETY: This is not safe! + let _offset = unsafe { ptr_oob.offset_from(ptr) }; +} + +#[kani::proof] +fn check_offset_from_diff_alloc() { + let val1 = 10u128; + let val2 = 0u128; + let ptr1: *const u128 = &val1; + let ptr2: *const u128 = &val2; + // SAFETY: This is not safe! + let offset = unsafe { ptr1.offset_from(ptr2) }; + assert!(offset != 0); +} + +#[kani::proof] +#[kani::should_panic] +fn check_offset_from_unit_panic() { + let val1 = kani::any(); + let val2 = kani::any(); + let ptr1: *const () = &val1 as *const _ as *const (); + let ptr2: *const () = &val2 as *const _ as *const (); + // SAFETY: This is safe but will panic... + let _offset = unsafe { ptr1.offset_from(ptr2) }; +} + +#[kani::proof] +fn check_offset_from_same_dangling() { + let val = 10u128; + let ptr: *const u128 = &val; + let ptr_oob_1: *const u128 = ptr.wrapping_add(10); + let ptr_oob_2: *const u128 = ptr.wrapping_add(5).wrapping_add(5); + // SAFETY: This is safe since the pointer is the same! + let offset = unsafe { ptr_oob_1.offset_from(ptr_oob_2) }; + assert_eq!(offset, 0); +} diff --git a/tests/expected/offset-bounds-check/sub_ptr.expected b/tests/expected/offset-bounds-check/sub_ptr.expected new file mode 100644 index 000000000000..c9ac1c983a68 --- /dev/null +++ b/tests/expected/offset-bounds-check/sub_ptr.expected @@ -0,0 +1,65 @@ +Kani Rust Verifier 0.56.0 (standalone) +Checking harness check_sub_ptr_same_dangling... + +VERIFICATION RESULT: + ** 0 of 13 failed (3 unreachable) + +VERIFICATION:- SUCCESSFUL +Verification Time: 0.03525919s + +Checking harness check_sub_ptr_unit_panic... + +VERIFICATION RESULT: + ** 1 of 12 failed (3 unreachable) +Failed Checks: assertion failed: 0 < pointee_size && pointee_size <= isize::MAX as usize + File: "/home/ANT.AMAZON.COM/celinval/.rustup/toolchains/nightly-2024-11-28-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs", line 784, in std::ptr::const_ptr::::sub_ptr + +VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected) +Verification Time: 0.032447934s + +Checking harness check_sub_ptr_negative_result... + +VERIFICATION RESULT: + ** 1 of 15 failed (1 unreachable) +Failed Checks: Expected non-negative distance between pointers + File: "/home/ANT.AMAZON.COM/celinval/workspace/kani-project/kani/library/kani/src/lib.rs", line 54, in kani::rustc_intrinsics::ptr_sub_ptr:: + +VERIFICATION:- FAILED +Verification Time: 0.05667276s + +Checking harness check_sub_ptr_diff_alloc... + +VERIFICATION RESULT: + ** 1 of 12 failed (3 unreachable) +Failed Checks: Offset result and original pointer should point to the same allocation + File: "/home/ANT.AMAZON.COM/celinval/workspace/kani-project/kani/library/kani/src/lib.rs", line 54, in kani::rustc_intrinsics::ptr_offset_from:: + +VERIFICATION:- FAILED +Verification Time: 0.037252095s + +Checking harness check_sub_ptr_oob_ptr... + +VERIFICATION RESULT: + ** 1 of 12 failed (2 unreachable) +Failed Checks: Offset result and original pointer should point to the same allocation + File: "/home/ANT.AMAZON.COM/celinval/workspace/kani-project/kani/library/kani/src/lib.rs", line 54, in kani::rustc_intrinsics::ptr_offset_from:: + +VERIFICATION:- FAILED +Verification Time: 0.040543832s + +Checking harness check_sub_ptr_self_oob... + +VERIFICATION RESULT: + ** 1 of 12 failed (2 unreachable) +Failed Checks: Offset result and original pointer should point to the same allocation + File: "/home/ANT.AMAZON.COM/celinval/workspace/kani-project/kani/library/kani/src/lib.rs", line 54, in kani::rustc_intrinsics::ptr_offset_from:: + +VERIFICATION:- FAILED +Verification Time: 0.036195125s + +Summary: +Verification failed for - check_sub_ptr_negative_result +Verification failed for - check_sub_ptr_diff_alloc +Verification failed for - check_sub_ptr_oob_ptr +Verification failed for - check_sub_ptr_self_oob +Complete - 2 successfully verified harnesses, 4 failures, 6 total. diff --git a/tests/expected/offset-bounds-check/sub_ptr.rs b/tests/expected/offset-bounds-check/sub_ptr.rs new file mode 100644 index 000000000000..7ddfa96d94f8 --- /dev/null +++ b/tests/expected/offset-bounds-check/sub_ptr.rs @@ -0,0 +1,70 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check that Kani can detect UB due to `sub_ptr` with out-of-bounds pointer or wrong order. + +#![feature(ptr_sub_ptr)] + +#[kani::proof] +fn check_sub_ptr_self_oob() { + let val = 10u128; + let ptr: *const u128 = &val; + let ptr_oob: *const u128 = ptr.wrapping_add(10); + // SAFETY: This is not safe! + let _offset = unsafe { ptr_oob.sub_ptr(ptr) }; +} + +#[kani::proof] +fn check_sub_ptr_oob_ptr() { + let val = 10u128; + let ptr: *const u128 = &val; + let ptr_oob: *const u128 = ptr.wrapping_sub(10); + // SAFETY: This is not safe! + let _offset = unsafe { ptr.sub_ptr(ptr_oob) }; +} + +#[kani::proof] +fn check_sub_ptr_diff_alloc() { + let val1 = kani::any(); + let val2 = kani::any(); + let ptr1: *const u128 = &val1; + let ptr2: *const u128 = &val2; + // SAFETY: This is not safe! + let _offset = unsafe { ptr1.sub_ptr(ptr2) }; +} + +#[kani::proof] +fn check_sub_ptr_negative_result() { + let val: [u8; 10] = kani::any(); + let ptr_first: *const _ = &val[0]; + let ptr_last: *const _ = &val[9]; + // SAFETY: This is safe! + let offset_ok = unsafe { ptr_last.sub_ptr(ptr_first) }; + + // SAFETY: This is not safe! + let offset_not_ok = unsafe { ptr_first.sub_ptr(ptr_last) }; + + // Just use the result. + assert!(offset_ok != offset_not_ok); +} + +#[kani::proof] +#[kani::should_panic] +fn check_sub_ptr_unit_panic() { + let val1 = kani::any(); + let val2 = kani::any(); + let ptr1: *const () = &val1 as *const _ as *const (); + let ptr2: *const () = &val2 as *const _ as *const (); + // SAFETY: This is safe but will panic... + let _offset = unsafe { ptr1.sub_ptr(ptr2) }; +} + +#[kani::proof] +fn check_sub_ptr_same_dangling() { + let val = 10u128; + let ptr: *const u128 = &val; + let ptr_oob_1: *const u128 = ptr.wrapping_add(10); + let ptr_oob_2: *const u128 = ptr.wrapping_add(5).wrapping_add(5); + // SAFETY: This is safe since the pointer is the same! + let offset = unsafe { ptr_oob_1.sub_ptr(ptr_oob_2) }; + assert_eq!(offset, 0); +} From e825aeedc12caf08d2211dfcc9cd7cfc357cde82 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 13 Dec 2024 10:11:06 +0000 Subject: [PATCH 04/10] Revert "Add UB checks for `ptr_offset_from*` intrinsics" This reverts commit 0f027cf57658eaa6d42121cc6b83b84799d4ae4e. --- .../codegen/intrinsic.rs | 84 +++++++++++++++++-- .../src/kani_middle/kani_functions.rs | 4 - .../kani_middle/transform/rustc_intrinsics.rs | 2 - library/kani_core/src/models.rs | 33 -------- .../offset-bounds-check/offset_from.expected | 6 -- .../offset-bounds-check/offset_from.rs | 47 ----------- .../offset-bounds-check/sub_ptr.expected | 65 -------------- tests/expected/offset-bounds-check/sub_ptr.rs | 70 ---------------- 8 files changed, 79 insertions(+), 232 deletions(-) delete mode 100644 tests/expected/offset-bounds-check/offset_from.expected delete mode 100644 tests/expected/offset-bounds-check/offset_from.rs delete mode 100644 tests/expected/offset-bounds-check/sub_ptr.expected delete mode 100644 tests/expected/offset-bounds-check/sub_ptr.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index bd103fe4e45e..654a7f2b6861 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -7,7 +7,9 @@ use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable; use crate::codegen_cprover_gotoc::{GotocCtx, utils}; use crate::intrinsics::Intrinsic; use crate::unwrap_or_return_codegen_unimplemented_stmt; -use cbmc::goto_program::{BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type}; +use cbmc::goto_program::{ + ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type, +}; use rustc_middle::ty::TypingEnv; use rustc_middle::ty::layout::ValidityRequirement; use rustc_smir::rustc_internal; @@ -423,6 +425,10 @@ impl GotocCtx<'_> { Intrinsic::PowIF64 => codegen_simple_intrinsic!(Powi), Intrinsic::PrefAlignOf => codegen_intrinsic_const!(), Intrinsic::PtrGuaranteedCmp => self.codegen_ptr_guaranteed_cmp(fargs, place, loc), + Intrinsic::PtrOffsetFrom => self.codegen_ptr_offset_from(fargs, place, loc), + Intrinsic::PtrOffsetFromUnsigned => { + self.codegen_ptr_offset_from_unsigned(fargs, place, loc) + } Intrinsic::RawEq => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc), Intrinsic::RetagBoxToRaw => self.codegen_retag_box_to_raw(fargs, place, loc), Intrinsic::RintF32 => codegen_simple_intrinsic!(Rintf), @@ -540,10 +546,7 @@ impl GotocCtx<'_> { assert!(self.place_ty_stable(place).kind().is_unit()); self.codegen_write_bytes(fargs, farg_types, loc) } - Intrinsic::PtrOffsetFrom - | Intrinsic::PtrOffsetFromUnsigned - | Intrinsic::SizeOfVal - | Intrinsic::MinAlignOfVal => { + Intrinsic::SizeOfVal | Intrinsic::MinAlignOfVal => { unreachable!("Intrinsic `{}` is handled before codegen", intrinsic_str) } // Unimplemented @@ -1022,6 +1025,77 @@ impl GotocCtx<'_> { self.codegen_expr_to_place_stable(p, dst_ptr, loc) } + /// ptr_offset_from returns the offset between two pointers + /// + fn codegen_ptr_offset_from(&mut self, fargs: Vec, p: &Place, loc: Location) -> Stmt { + let (offset_expr, offset_overflow) = self.codegen_ptr_offset_from_expr(fargs); + + // Check that computing `offset` in bytes would not overflow an `isize` + // These checks may allow a wrapping-around behavior in CBMC: + // https://github.com/model-checking/kani/issues/1150 + let overflow_check = self.codegen_assert_assume( + offset_overflow.overflowed.not(), + PropertyClass::ArithmeticOverflow, + "attempt to compute offset in bytes which would overflow an `isize`", + loc, + ); + + let offset_expr = self.codegen_expr_to_place_stable(p, offset_expr, loc); + Stmt::block(vec![overflow_check, offset_expr], loc) + } + + /// `ptr_offset_from_unsigned` returns the offset between two pointers where the order is known. + /// The logic is similar to `ptr_offset_from` but the return value is a `usize`. + /// See for more details + fn codegen_ptr_offset_from_unsigned( + &mut self, + fargs: Vec, + p: &Place, + loc: Location, + ) -> Stmt { + let (offset_expr, offset_overflow) = self.codegen_ptr_offset_from_expr(fargs); + + // Check that computing `offset` in bytes would not overflow an `isize` + // These checks may allow a wrapping-around behavior in CBMC: + // https://github.com/model-checking/kani/issues/1150 + let overflow_check = self.codegen_assert_assume( + offset_overflow.overflowed.not(), + PropertyClass::ArithmeticOverflow, + "attempt to compute offset in bytes which would overflow an `isize`", + loc, + ); + + let non_negative_check = self.codegen_assert_assume( + offset_overflow.result.is_non_negative(), + PropertyClass::SafetyCheck, + "attempt to compute unsigned offset with negative distance", + loc, + ); + + let offset_expr = + self.codegen_expr_to_place_stable(p, offset_expr.cast_to(Type::size_t()), loc); + Stmt::block(vec![overflow_check, non_negative_check, offset_expr], loc) + } + + /// Both `ptr_offset_from` and `ptr_offset_from_unsigned` return the offset between two pointers. + /// This function implements the common logic between them. + fn codegen_ptr_offset_from_expr( + &mut self, + mut fargs: Vec, + ) -> (Expr, ArithmeticOverflowResult) { + let dst_ptr = fargs.remove(0); + let src_ptr = fargs.remove(0); + + // Compute the offset with standard substraction using `isize` + let cast_dst_ptr = dst_ptr.clone().cast_to(Type::ssize_t()); + let cast_src_ptr = src_ptr.clone().cast_to(Type::ssize_t()); + let offset_overflow = cast_dst_ptr.sub_overflow(cast_src_ptr); + + // Re-compute the offset with standard substraction (no casts this time) + let ptr_offset_expr = dst_ptr.sub(src_ptr); + (ptr_offset_expr, offset_overflow) + } + /// A transmute is a bitcast from the argument type to the return type. /// /// diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 8d1ab5ef939d..38522fae837f 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -83,10 +83,6 @@ pub enum KaniModel { IsSlicePtrInitialized, #[strum(serialize = "OffsetModel")] Offset, - #[strum(serialize = "PtrOffsetFromModel")] - PtrOffsetFrom, - #[strum(serialize = "PtrSubPtrModel")] - PtrSubPtr, #[strum(serialize = "RunContractModel")] RunContract, #[strum(serialize = "RunLoopContractModel")] diff --git a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs index 79238e423e62..ad4238574d63 100644 --- a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs @@ -167,8 +167,6 @@ impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_> { let model = match intrinsic { Intrinsic::SizeOfVal => self.models[&KaniModel::SizeOfVal], Intrinsic::MinAlignOfVal => self.models[&KaniModel::AlignOfVal], - Intrinsic::PtrOffsetFrom => self.models[&KaniModel::PtrOffsetFrom], - Intrinsic::PtrOffsetFromUnsigned => self.models[&KaniModel::PtrSubPtr], // The rest is handled in codegen. _ => { return self.super_terminator(term); diff --git a/library/kani_core/src/models.rs b/library/kani_core/src/models.rs index a754efcd0f7a..31a676f95272 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -45,39 +45,6 @@ macro_rules! generate_models { } } - #[kanitool::fn_marker = "PtrOffsetFromModel"] - pub unsafe fn ptr_offset_from(ptr1: *const T, ptr2: *const T) -> isize { - if ptr1 == ptr2 { - 0 - } else { - kani::safety_check( - kani::mem::same_allocation_internal(ptr1, ptr2), - "Offset result and original pointer should point to the same allocation", - ); - kani::safety_check( - core::mem::size_of::() > 0, - "Cannot compute offset of a ZST", - ); - // The offset must fit in isize since this represents the same allocation. - let offset_bytes = ptr1.addr().wrapping_sub(ptr2.addr()) as isize; - // We know `t_size` is a power of two, so avoid division. - let t_size = size_of::() as isize; - kani::safety_check( - offset_bytes & (t_size - 1) == 0, - "Expected the distance between the pointers, in bytes, to be a - multiple of the size of `T`", - ); - offset_bytes >> t_size.trailing_zeros() - } - } - - #[kanitool::fn_marker = "PtrSubPtrModel"] - pub unsafe fn ptr_sub_ptr(ptr1: *const T, ptr2: *const T) -> usize { - let offset = ptr_offset_from(ptr1, ptr2); - kani::safety_check(offset >= 0, "Expected non-negative distance between pointers"); - offset as usize - } - /// An offset model that checks UB. #[kanitool::fn_marker = "OffsetModel"] pub fn offset, O: ToISize>(ptr: P, offset: O) -> P { diff --git a/tests/expected/offset-bounds-check/offset_from.expected b/tests/expected/offset-bounds-check/offset_from.expected deleted file mode 100644 index d985c9a4e318..000000000000 --- a/tests/expected/offset-bounds-check/offset_from.expected +++ /dev/null @@ -1,6 +0,0 @@ -Failed Checks: assertion failed: 0 < pointee_size && pointee_size <= isize::MAX as usize -Failed Checks: Offset result and original pointer should point to the same allocation - -Verification failed for - check_offset_from_diff_alloc -Verification failed for - check_offset_from_oob_ptr -Complete - 2 successfully verified harnesses, 2 failures, 4 total. diff --git a/tests/expected/offset-bounds-check/offset_from.rs b/tests/expected/offset-bounds-check/offset_from.rs deleted file mode 100644 index 7ce3edcb3657..000000000000 --- a/tests/expected/offset-bounds-check/offset_from.rs +++ /dev/null @@ -1,47 +0,0 @@ -// 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_offset_from_oob_ptr() { - let val = 10u128; - let ptr: *const u128 = &val; - let ptr_oob: *const u128 = ptr.wrapping_add(10); - // SAFETY: This is not safe! - let _offset = unsafe { ptr_oob.offset_from(ptr) }; -} - -#[kani::proof] -fn check_offset_from_diff_alloc() { - let val1 = 10u128; - let val2 = 0u128; - let ptr1: *const u128 = &val1; - let ptr2: *const u128 = &val2; - // SAFETY: This is not safe! - let offset = unsafe { ptr1.offset_from(ptr2) }; - assert!(offset != 0); -} - -#[kani::proof] -#[kani::should_panic] -fn check_offset_from_unit_panic() { - let val1 = kani::any(); - let val2 = kani::any(); - let ptr1: *const () = &val1 as *const _ as *const (); - let ptr2: *const () = &val2 as *const _ as *const (); - // SAFETY: This is safe but will panic... - let _offset = unsafe { ptr1.offset_from(ptr2) }; -} - -#[kani::proof] -fn check_offset_from_same_dangling() { - let val = 10u128; - let ptr: *const u128 = &val; - let ptr_oob_1: *const u128 = ptr.wrapping_add(10); - let ptr_oob_2: *const u128 = ptr.wrapping_add(5).wrapping_add(5); - // SAFETY: This is safe since the pointer is the same! - let offset = unsafe { ptr_oob_1.offset_from(ptr_oob_2) }; - assert_eq!(offset, 0); -} diff --git a/tests/expected/offset-bounds-check/sub_ptr.expected b/tests/expected/offset-bounds-check/sub_ptr.expected deleted file mode 100644 index c9ac1c983a68..000000000000 --- a/tests/expected/offset-bounds-check/sub_ptr.expected +++ /dev/null @@ -1,65 +0,0 @@ -Kani Rust Verifier 0.56.0 (standalone) -Checking harness check_sub_ptr_same_dangling... - -VERIFICATION RESULT: - ** 0 of 13 failed (3 unreachable) - -VERIFICATION:- SUCCESSFUL -Verification Time: 0.03525919s - -Checking harness check_sub_ptr_unit_panic... - -VERIFICATION RESULT: - ** 1 of 12 failed (3 unreachable) -Failed Checks: assertion failed: 0 < pointee_size && pointee_size <= isize::MAX as usize - File: "/home/ANT.AMAZON.COM/celinval/.rustup/toolchains/nightly-2024-11-28-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs", line 784, in std::ptr::const_ptr::::sub_ptr - -VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected) -Verification Time: 0.032447934s - -Checking harness check_sub_ptr_negative_result... - -VERIFICATION RESULT: - ** 1 of 15 failed (1 unreachable) -Failed Checks: Expected non-negative distance between pointers - File: "/home/ANT.AMAZON.COM/celinval/workspace/kani-project/kani/library/kani/src/lib.rs", line 54, in kani::rustc_intrinsics::ptr_sub_ptr:: - -VERIFICATION:- FAILED -Verification Time: 0.05667276s - -Checking harness check_sub_ptr_diff_alloc... - -VERIFICATION RESULT: - ** 1 of 12 failed (3 unreachable) -Failed Checks: Offset result and original pointer should point to the same allocation - File: "/home/ANT.AMAZON.COM/celinval/workspace/kani-project/kani/library/kani/src/lib.rs", line 54, in kani::rustc_intrinsics::ptr_offset_from:: - -VERIFICATION:- FAILED -Verification Time: 0.037252095s - -Checking harness check_sub_ptr_oob_ptr... - -VERIFICATION RESULT: - ** 1 of 12 failed (2 unreachable) -Failed Checks: Offset result and original pointer should point to the same allocation - File: "/home/ANT.AMAZON.COM/celinval/workspace/kani-project/kani/library/kani/src/lib.rs", line 54, in kani::rustc_intrinsics::ptr_offset_from:: - -VERIFICATION:- FAILED -Verification Time: 0.040543832s - -Checking harness check_sub_ptr_self_oob... - -VERIFICATION RESULT: - ** 1 of 12 failed (2 unreachable) -Failed Checks: Offset result and original pointer should point to the same allocation - File: "/home/ANT.AMAZON.COM/celinval/workspace/kani-project/kani/library/kani/src/lib.rs", line 54, in kani::rustc_intrinsics::ptr_offset_from:: - -VERIFICATION:- FAILED -Verification Time: 0.036195125s - -Summary: -Verification failed for - check_sub_ptr_negative_result -Verification failed for - check_sub_ptr_diff_alloc -Verification failed for - check_sub_ptr_oob_ptr -Verification failed for - check_sub_ptr_self_oob -Complete - 2 successfully verified harnesses, 4 failures, 6 total. diff --git a/tests/expected/offset-bounds-check/sub_ptr.rs b/tests/expected/offset-bounds-check/sub_ptr.rs deleted file mode 100644 index 7ddfa96d94f8..000000000000 --- a/tests/expected/offset-bounds-check/sub_ptr.rs +++ /dev/null @@ -1,70 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -//! Check that Kani can detect UB due to `sub_ptr` with out-of-bounds pointer or wrong order. - -#![feature(ptr_sub_ptr)] - -#[kani::proof] -fn check_sub_ptr_self_oob() { - let val = 10u128; - let ptr: *const u128 = &val; - let ptr_oob: *const u128 = ptr.wrapping_add(10); - // SAFETY: This is not safe! - let _offset = unsafe { ptr_oob.sub_ptr(ptr) }; -} - -#[kani::proof] -fn check_sub_ptr_oob_ptr() { - let val = 10u128; - let ptr: *const u128 = &val; - let ptr_oob: *const u128 = ptr.wrapping_sub(10); - // SAFETY: This is not safe! - let _offset = unsafe { ptr.sub_ptr(ptr_oob) }; -} - -#[kani::proof] -fn check_sub_ptr_diff_alloc() { - let val1 = kani::any(); - let val2 = kani::any(); - let ptr1: *const u128 = &val1; - let ptr2: *const u128 = &val2; - // SAFETY: This is not safe! - let _offset = unsafe { ptr1.sub_ptr(ptr2) }; -} - -#[kani::proof] -fn check_sub_ptr_negative_result() { - let val: [u8; 10] = kani::any(); - let ptr_first: *const _ = &val[0]; - let ptr_last: *const _ = &val[9]; - // SAFETY: This is safe! - let offset_ok = unsafe { ptr_last.sub_ptr(ptr_first) }; - - // SAFETY: This is not safe! - let offset_not_ok = unsafe { ptr_first.sub_ptr(ptr_last) }; - - // Just use the result. - assert!(offset_ok != offset_not_ok); -} - -#[kani::proof] -#[kani::should_panic] -fn check_sub_ptr_unit_panic() { - let val1 = kani::any(); - let val2 = kani::any(); - let ptr1: *const () = &val1 as *const _ as *const (); - let ptr2: *const () = &val2 as *const _ as *const (); - // SAFETY: This is safe but will panic... - let _offset = unsafe { ptr1.sub_ptr(ptr2) }; -} - -#[kani::proof] -fn check_sub_ptr_same_dangling() { - let val = 10u128; - let ptr: *const u128 = &val; - let ptr_oob_1: *const u128 = ptr.wrapping_add(10); - let ptr_oob_2: *const u128 = ptr.wrapping_add(5).wrapping_add(5); - // SAFETY: This is safe since the pointer is the same! - let offset = unsafe { ptr_oob_1.sub_ptr(ptr_oob_2) }; - assert_eq!(offset, 0); -} From dab2d6592b54e50a6eb0d171717e86bad1644548 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 13 Dec 2024 10:11:10 +0000 Subject: [PATCH 05/10] Revert "Fix tests after enabling offset bound checks" This reverts commit 1632b67680defe00051ee8ea27a4b0870e45ae5c. --- .../copy-nonoverlapping/copy-unreadable-src/main.rs | 6 +++--- .../expected/intrinsics/copy/copy-unreadable-src/main.rs | 6 +++--- .../offset-bounds-check/out_of_bounds_ub_check.expected | 2 +- .../expected/offset-bounds-check/start_from_oob.expected | 2 +- tests/expected/offset-bytes-overflow/expected | 6 ++---- tests/expected/offset-from-bytes-overflow/expected | 6 ++---- tests/expected/offset-overflow/expected | 6 ++---- tests/expected/pointer-overflow/expected | 3 ++- tests/expected/pointer-overflow/main.rs | 1 + tests/expected/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 ++- tests/kani/ValidValues/unaligned.rs | 4 +++- 15 files changed, 32 insertions(+), 29 deletions(-) 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 744528b9c32a..ff2d54e7ca6b 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 202900933e00..2b0e71cc16f3 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/out_of_bounds_ub_check.expected b/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected index 62b518815bb0..099cbdcd9f1c 100644 --- a/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected +++ b/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected @@ -1,4 +1,4 @@ -Failed Checks: Offset result and original pointer should point to the same allocation +Failed Checks: Offset result is out of bounds of initial allocation Verification failed for - check_ptr_oob Complete - 1 successfully verified harnesses, 1 failures, 2 total. diff --git a/tests/expected/offset-bounds-check/start_from_oob.expected b/tests/expected/offset-bounds-check/start_from_oob.expected index fc766c277581..fc5fbdfb365a 100644 --- a/tests/expected/offset-bounds-check/start_from_oob.expected +++ b/tests/expected/offset-bounds-check/start_from_oob.expected @@ -1,4 +1,4 @@ -Failed Checks: Offset result and original pointer should point to the same allocation +Failed Checks: Offset result is out of bounds of initial allocation Verification failed for - check_add_to_oob Complete - 0 successfully verified harnesses, 1 failures, 1 total. diff --git a/tests/expected/offset-bytes-overflow/expected b/tests/expected/offset-bytes-overflow/expected index 8eae686f2142..1f13adcc7776 100644 --- a/tests/expected/offset-bytes-overflow/expected +++ b/tests/expected/offset-bytes-overflow/expected @@ -1,4 +1,2 @@ -Failed Checks: Offset in bytes overflow isize -Verification failed for - check_wrap_offset - -Complete - 0 successfully verified harnesses, 1 failures, 1 total. +FAILURE\ +offset: attempt to compute number in bytes which would overflow \ No newline at end of file diff --git a/tests/expected/offset-from-bytes-overflow/expected b/tests/expected/offset-from-bytes-overflow/expected index 51f9bfb293a0..bcf0242f9e9d 100644 --- a/tests/expected/offset-from-bytes-overflow/expected +++ b/tests/expected/offset-from-bytes-overflow/expected @@ -1,4 +1,2 @@ -Failed Checks: Offset in bytes overflow isize -Verification failed for - main - -Complete - 0 successfully verified harnesses, 1 failures, 1 total. +FAILURE\ +attempt to compute number in bytes which would overflow diff --git a/tests/expected/offset-overflow/expected b/tests/expected/offset-overflow/expected index ba7d1c2fe7df..9613638bf8f9 100644 --- a/tests/expected/offset-overflow/expected +++ b/tests/expected/offset-overflow/expected @@ -1,4 +1,2 @@ -Failed Checks: Offset result and original pointer should point to the same allocation -Verification failed for - test_offset_overflow - -Complete - 0 successfully verified harnesses, 1 failures, 1 total. +FAILURE\ +attempt to compute offset which would overflow diff --git a/tests/expected/pointer-overflow/expected b/tests/expected/pointer-overflow/expected index a6319eb7d1f1..3701d77c8bfd 100644 --- a/tests/expected/pointer-overflow/expected +++ b/tests/expected/pointer-overflow/expected @@ -1 +1,2 @@ -Failed Checks: Offset in bytes overflow isize +Status: FAILURE\ +offset: attempt to compute number in bytes which would overflow diff --git a/tests/expected/pointer-overflow/main.rs b/tests/expected/pointer-overflow/main.rs index c78cf4027351..9c8dc52bddf0 100644 --- a/tests/expected/pointer-overflow/main.rs +++ b/tests/expected/pointer-overflow/main.rs @@ -1,6 +1,7 @@ // 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 a258cb026a1a..ad33ce91dabb 100644 --- a/tests/expected/ptr-offset-overflow-bytes/expected +++ b/tests/expected/ptr-offset-overflow-bytes/expected @@ -1,3 +1,5 @@ -Failed Checks: Offset in bytes overflow isize -Verification failed for - main -Complete - 0 successfully verified harnesses, 1 failures, 1 total. +std::ptr::const_ptr::::offset.arithmetic_overflow\ +Status: FAILURE\ +Description: "offset: attempt to compute number in bytes which would overflow" + +VERIFICATION:- FAILED diff --git a/tests/expected/ptr_to_ref_cast/slice/test.rs b/tests/expected/ptr_to_ref_cast/slice/test.rs index b9e4d54546f6..8526d0bf1c7f 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.wrapping_byte_add(offset).wrapping_byte_sub(offset) }; + let val = unsafe { &*ptr.byte_add(offset).byte_sub(offset) }; assert_eq!(val.len(), data.len()); } diff --git a/tests/expected/raw_slice/expected b/tests/expected/raw_slice/expected index 73a625248d51..1b863417c02c 100644 --- a/tests/expected/raw_slice/expected +++ b/tests/expected/raw_slice/expected @@ -62,7 +62,8 @@ Description: "assertion failed: slice.others[0] == second"\ slice.rs:96:5 in function check_naive_iterator_should_fail Status: FAILURE\ -Description: "Offset result and original pointer should point to the same allocation" +Description: "dereference failure: pointer outside object bounds"\ +slice.rs:100:32 in function check_naive_iterator_should_fail VERIFICATION:- FAILED diff --git a/tests/expected/raw_slice_c_repr/expected b/tests/expected/raw_slice_c_repr/expected index eca589cdd260..9271825be7cd 100644 --- a/tests/expected/raw_slice_c_repr/expected +++ b/tests/expected/raw_slice_c_repr/expected @@ -62,7 +62,8 @@ Description: "assertion failed: slice.others[0] == second"\ in function check_naive_iterator_should_fail Status: FAILURE\ -Description: "Offset result and original pointer should point to the same allocation" +Description: "dereference failure: pointer outside object bounds"\ +in function check_naive_iterator_should_fail VERIFICATION:- FAILED diff --git a/tests/expected/raw_slice_packed/expected b/tests/expected/raw_slice_packed/expected index eca589cdd260..9271825be7cd 100644 --- a/tests/expected/raw_slice_packed/expected +++ b/tests/expected/raw_slice_packed/expected @@ -62,7 +62,8 @@ Description: "assertion failed: slice.others[0] == second"\ in function check_naive_iterator_should_fail Status: FAILURE\ -Description: "Offset result and original pointer should point to the same allocation" +Description: "dereference failure: pointer outside object bounds"\ +in function check_naive_iterator_should_fail VERIFICATION:- FAILED diff --git a/tests/kani/ValidValues/unaligned.rs b/tests/kani/ValidValues/unaligned.rs index dc1d3d897211..695f74ebf1b4 100644 --- a/tests/kani/ValidValues/unaligned.rs +++ b/tests/kani/ValidValues/unaligned.rs @@ -1,6 +1,6 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z valid-value-checks -Z mem-predicates +// kani-flags: -Z valid-value-checks //! Check that Kani can check value validity of packed structs. use std::ptr::addr_of; @@ -34,4 +34,6 @@ pub fn check_packed_read_unaligned_invalid_value() { let val = [u8::MAX; SZ]; let ptr = addr_of!(val) as *const Packed; assert!(!kani::mem::can_read_unaligned(ptr)); + assert!(kani::mem::can_read_unaligned(unsafe { addr_of!((*ptr).byte) })); + assert!(!kani::mem::can_read_unaligned(unsafe { addr_of!((*ptr).c) })); } From 0f31a8d9300fea1a65114028acc7e24e62ebc015 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Fri, 13 Dec 2024 10:11:11 +0000 Subject: [PATCH 06/10] Revert "Implement bounds check on offset" This reverts commit ed7e698f38728aeb44ca63bf2489fb22cabb7998. --- .../codegen_cprover_gotoc/codegen/assert.rs | 11 +- .../codegen/intrinsic.rs | 2 +- .../codegen_cprover_gotoc/codegen/rvalue.rs | 43 +++++-- .../codegen_cprover_gotoc/overrides/hooks.rs | 72 ++++------- .../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 | 67 ---------- .../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 --- .../offset-invalid-args/invalid_args.expected | 1 - .../offset-invalid-args/invalid_args.rs | 15 --- tests/expected/offset-wraps-around/main.rs | 64 +++------- tests/kani/ValidValues/unaligned.rs | 39 ------ 18 files changed, 97 insertions(+), 423 deletions(-) delete mode 100644 tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected delete mode 100644 tests/expected/offset-bounds-check/out_of_bounds_ub_check.rs delete mode 100644 tests/expected/offset-bounds-check/start_from_oob.expected delete mode 100644 tests/expected/offset-bounds-check/start_from_oob.rs delete mode 100644 tests/expected/offset-invalid-args/invalid_args.expected delete mode 100644 tests/expected/offset-invalid-args/invalid_args.rs delete 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 82817fc6178f..84b20a623541 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: Same as SafetyCheck. + /// SPECIAL BEHAVIOR: None TODO: Why should this exist? 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 intrinsic check. + /// Another instrinsic check. /// - /// SPECIAL BEHAVIOR: Same as SafetyCheck + /// SPECIAL BEHAVIOR: None TODO: Why should this exist? ExactDiv, - /// Another intrinsic check. + /// Another instrinsic check. /// - /// SPECIAL BEHAVIOR: Same as SafetyCheck + /// SPECIAL BEHAVIOR: None TODO: Why should this exist? FiniteCheck, /// Checks added by Kani compiler to determine whether a property (e.g. /// `PropertyClass::Assertion` or `PropertyClass:Cover`) is reachable @@ -82,7 +82,6 @@ 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 654a7f2b6861..a1daeec5f88b 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 documentation, the operation is always safe. + /// According to the documenation, 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 68c174ae2119..f84e0a89f937 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,15 +405,42 @@ 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); - ce1.clone().plus(ce2) + + // 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, + ) } } } diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 3eebf1abb7ab..d228965f7633 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -134,10 +134,15 @@ 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, - gcx.codegen_assert_assume(cond, PropertyClass::Assertion, &msg, caller_loc), + decl, + gcx.codegen_assert_assume(tmp, PropertyClass::Assertion, &msg, caller_loc), Stmt::goto(bb_label(target), caller_loc), ], caller_loc, @@ -145,25 +150,6 @@ impl GotocHook for Assert { } } -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, - fargs: Vec, - _assign_to: &Place, - target: Option, - span: Span, - ) -> Stmt { - check_hook(PropertyClass::UnsupportedConstruct, gcx, fargs, target, span) - } -} - struct SafetyCheck; impl GotocHook for SafetyCheck { fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool { @@ -174,12 +160,24 @@ impl GotocHook for SafetyCheck { &self, gcx: &mut GotocCtx, _instance: Instance, - fargs: Vec, + mut fargs: Vec, _assign_to: &Place, target: Option, span: Span, ) -> Stmt { - check_hook(PropertyClass::SafetyCheck, gcx, fargs, target, span) + assert_eq!(fargs.len(), 2); + let cond = fargs.remove(0).cast_to(Type::bool()); + let msg = fargs.remove(0); + 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::SafetyCheck, &msg, caller_loc), + Stmt::goto(bb_label(target), caller_loc), + ], + caller_loc, + ) } } @@ -207,15 +205,10 @@ impl GotocHook for Check { 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(tmp, PropertyClass::Assertion, &msg, caller_loc), + gcx.codegen_assert(cond, PropertyClass::Assertion, &msg, caller_loc), Stmt::goto(bb_label(target), caller_loc), ], caller_loc, @@ -716,7 +709,6 @@ 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)), @@ -755,25 +747,3 @@ impl GotocHooks { } } } - -fn check_hook( - prop_class: PropertyClass, - gcx: &mut GotocCtx, - mut fargs: Vec, - 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, prop_class, &msg, caller_loc), - Stmt::goto(bb_label(target), caller_loc), - ], - caller_loc, - ) -} diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 38522fae837f..6a136f1a5647 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -81,8 +81,6 @@ pub enum KaniModel { IsSliceChunkPtrInitialized, #[strum(serialize = "IsSlicePtrInitializedModel")] IsSlicePtrInitialized, - #[strum(serialize = "OffsetModel")] - Offset, #[strum(serialize = "RunContractModel")] RunContract, #[strum(serialize = "RunLoopContractModel")] @@ -142,8 +140,6 @@ 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 f2072fb21fb1..911ccf17e55f 100644 --- a/kani-compiler/src/kani_middle/transform/body.rs +++ b/kani-compiler/src/kani_middle/transform/body.rs @@ -434,11 +434,6 @@ 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 ad4238574d63..8174e8eb5e66 100644 --- a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs @@ -8,21 +8,13 @@ use crate::intrinsics::Intrinsic; use crate::kani_middle::kani_functions::{KaniFunction, KaniModel}; -use crate::kani_middle::transform::body::{ - InsertPosition, MutMirVisitor, MutableBody, SourceInstruction, -}; +use crate::kani_middle::transform::body::{MutMirVisitor, MutableBody}; 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::{ - 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 stable_mir::mir::{Body, ConstOperand, LocalDecl, Operand, Terminator, TerminatorKind}; +use stable_mir::ty::{FnDef, MirConst, RigidTy, TyKind}; use std::collections::HashMap; use tracing::debug; @@ -50,14 +42,12 @@ 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 = - ReplaceIntrinsicCallVisitor::new(&self.models, new_body.locals().to_vec()); + let mut visitor = ReplaceIntrinsicVisitor::new(&self.models, new_body.locals().to_vec()); visitor.visit_body(&mut new_body); - let changed = self.replace_lowered_intrinsics(tcx, &mut new_body); - (visitor.changed || changed, new_body.into()) + (visitor.changed, new_body.into()) } } @@ -73,78 +63,21 @@ 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 ReplaceIntrinsicCallVisitor<'a> { +struct ReplaceIntrinsicVisitor<'a> { models: &'a HashMap, locals: Vec, changed: bool, } -impl<'a> ReplaceIntrinsicCallVisitor<'a> { +impl<'a> ReplaceIntrinsicVisitor<'a> { fn new(models: &'a HashMap, locals: Vec) -> Self { - ReplaceIntrinsicCallVisitor { models, locals, changed: false } + ReplaceIntrinsicVisitor { models, locals, changed: false } } } -impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_> { +impl MutMirVisitor for ReplaceIntrinsicVisitor<'_> { /// 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 @@ -184,33 +117,3 @@ impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_> { 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 2d77fae0c48a..0a9a5b56ee9d 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -308,20 +308,6 @@ 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 c09d67ca51ff..5921b52faff2 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -149,14 +149,7 @@ macro_rules! kani_mem { )] #[allow(clippy::not_unsafe_ptr_arg_deref)] pub fn same_allocation(ptr1: *const T, ptr2: *const T) -> bool { - 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) + cbmc::same_allocation(ptr1, ptr2) } /// Compute the size of the val pointed to if it is safe to do so. @@ -251,7 +244,7 @@ macro_rules! kani_mem { /// /// # Safety /// - /// - Users have to ensure that the pointed to memory is allocated. + /// - Users have to ensure that the pointer is aligned the pointed memory is allocated. #[kanitool::fn_marker = "ValidValueIntrinsic"] #[inline(never)] unsafe fn has_valid_value(_ptr: *const T) -> bool { @@ -277,10 +270,11 @@ macro_rules! kani_mem { pub(super) mod cbmc { use super::*; /// CBMC specific implementation of [super::same_allocation]. - pub fn same_allocation(addr1: *const (), addr2: *const ()) -> bool { + pub fn same_allocation(ptr1: *const T, ptr2: *const T) -> bool { + let addr1 = ptr1 as *const (); + let addr2 = ptr2 as *const (); 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 31a676f95272..c2be6117a7df 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -16,9 +16,7 @@ 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) { @@ -44,71 +42,6 @@ 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 as isize); - kani::safety_check(!overflow, "Offset in bytes overflow isize"); - let orig_ptr = ptr.to_const_ptr(); - 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 should 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 in bytes overflow isize"); - unreachable!(); - } - } - } } #[allow(dead_code)] 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 deleted file mode 100644 index 099cbdcd9f1c..000000000000 --- a/tests/expected/offset-bounds-check/out_of_bounds_ub_check.expected +++ /dev/null @@ -1,4 +0,0 @@ -Failed Checks: Offset result is out of bounds of initial 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 deleted file mode 100644 index e6b4310269a1..000000000000 --- a/tests/expected/offset-bounds-check/out_of_bounds_ub_check.rs +++ /dev/null @@ -1,26 +0,0 @@ -// 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 deleted file mode 100644 index fc5fbdfb365a..000000000000 --- a/tests/expected/offset-bounds-check/start_from_oob.expected +++ /dev/null @@ -1,4 +0,0 @@ -Failed Checks: Offset result is out of bounds of initial 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 deleted file mode 100644 index 32713bbd41ee..000000000000 --- a/tests/expected/offset-bounds-check/start_from_oob.rs +++ /dev/null @@ -1,16 +0,0 @@ -// 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-invalid-args/invalid_args.expected b/tests/expected/offset-invalid-args/invalid_args.expected deleted file mode 100644 index 3a89d41b5d7c..000000000000 --- a/tests/expected/offset-invalid-args/invalid_args.expected +++ /dev/null @@ -1 +0,0 @@ -Cannot offset non-pointer type diff --git a/tests/expected/offset-invalid-args/invalid_args.rs b/tests/expected/offset-invalid-args/invalid_args.rs deleted file mode 100644 index bd5468afb9c7..000000000000 --- a/tests/expected/offset-invalid-args/invalid_args.rs +++ /dev/null @@ -1,15 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -//! Check Kani output if the arguments provided to the offset intrisic 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: u32 = kani::any(); - let new = unsafe { offset(&array, delta) }; - assert_ne!(new, &array) -} diff --git a/tests/expected/offset-wraps-around/main.rs b/tests/expected/offset-wraps-around/main.rs index da162cc8f1e3..3e83eacc4c2d 100644 --- a/tests/expected/offset-wraps-around/main.rs +++ b/tests/expected/offset-wraps-around/main.rs @@ -1,59 +1,35 @@ // Copyright Kani Contributors // SPDX-License-Identifier: Apache-2.0 OR MIT -//! 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 space address when -//! computing the offset between pointers. Doing that is UB in Rust, so we should be OK -//! as long as Kani can detect UB in that case. +// Check that a high offset causes a "wrapping around" behavior in CBMC. +// 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 original_harness() { +fn main() { let v: &[u128] = &[0; 10]; let v_0: *const u128 = &v[0]; let high_offset = usize::MAX / (std::mem::size_of::() * 4); unsafe { - let v_wrap: *const u128 = v_0.wrapping_add(high_offset); - // This should trigger UB!! - let wrapped_offset = unsafe { v_wrap.offset_from(v_0) }; - // Without UB detection, the offsets are the same, but CBMC pointer arithmetic - // would "wrapping around" making this incorrect + // 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()); } } - -/// 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); - unsafe { - 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); - } -} - -#[kani::proof] -fn check_wrap_ptr_max() { - 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); -} - -#[kani::proof] -fn check_wrap_ptr_10_bits() { - let v: &[u128] = &[0; 10]; - let orig_ptr: *const u128 = &v[0]; - let new_ptr: *const u128 = orig_ptr.wrapping_byte_add(1 << 63); - assert_ne!(orig_ptr as usize, new_ptr as usize); -} diff --git a/tests/kani/ValidValues/unaligned.rs b/tests/kani/ValidValues/unaligned.rs deleted file mode 100644 index 695f74ebf1b4..000000000000 --- a/tests/kani/ValidValues/unaligned.rs +++ /dev/null @@ -1,39 +0,0 @@ -// Copyright Kani Contributors -// SPDX-License-Identifier: Apache-2.0 OR MIT -// kani-flags: -Z valid-value-checks -//! 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)); - assert!(kani::mem::can_read_unaligned(unsafe { addr_of!((*ptr).byte) })); - assert!(!kani::mem::can_read_unaligned(unsafe { addr_of!((*ptr).c) })); -} From 072303afc01599a96b04b9d7b37d3ed42a348a62 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 4 Dec 2024 20:31:01 -0800 Subject: [PATCH 07/10] Add UB checks for `ptr_offset_from*` intrinsics Add a new model for `ptr_offset_from` and `ptr_offset_from_unsigned` intrinsics that check allocation and address order. --- .../codegen/intrinsic.rs | 84 ++----------------- .../src/kani_middle/kani_functions.rs | 4 + .../kani_middle/transform/rustc_intrinsics.rs | 2 + library/kani_core/src/models.rs | 33 ++++++++ .../offset-bounds-check/offset_from.expected | 6 ++ .../offset-bounds-check/offset_from.rs | 47 +++++++++++ .../offset-bounds-check/sub_ptr.expected | 65 ++++++++++++++ tests/expected/offset-bounds-check/sub_ptr.rs | 70 ++++++++++++++++ 8 files changed, 232 insertions(+), 79 deletions(-) create mode 100644 tests/expected/offset-bounds-check/offset_from.expected create mode 100644 tests/expected/offset-bounds-check/offset_from.rs create mode 100644 tests/expected/offset-bounds-check/sub_ptr.expected create mode 100644 tests/expected/offset-bounds-check/sub_ptr.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 654a7f2b6861..bd103fe4e45e 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -7,9 +7,7 @@ use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable; use crate::codegen_cprover_gotoc::{GotocCtx, utils}; use crate::intrinsics::Intrinsic; use crate::unwrap_or_return_codegen_unimplemented_stmt; -use cbmc::goto_program::{ - ArithmeticOverflowResult, BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type, -}; +use cbmc::goto_program::{BinaryOperator, BuiltinFn, Expr, Location, Stmt, Type}; use rustc_middle::ty::TypingEnv; use rustc_middle::ty::layout::ValidityRequirement; use rustc_smir::rustc_internal; @@ -425,10 +423,6 @@ impl GotocCtx<'_> { Intrinsic::PowIF64 => codegen_simple_intrinsic!(Powi), Intrinsic::PrefAlignOf => codegen_intrinsic_const!(), Intrinsic::PtrGuaranteedCmp => self.codegen_ptr_guaranteed_cmp(fargs, place, loc), - Intrinsic::PtrOffsetFrom => self.codegen_ptr_offset_from(fargs, place, loc), - Intrinsic::PtrOffsetFromUnsigned => { - self.codegen_ptr_offset_from_unsigned(fargs, place, loc) - } Intrinsic::RawEq => self.codegen_intrinsic_raw_eq(instance, fargs, place, loc), Intrinsic::RetagBoxToRaw => self.codegen_retag_box_to_raw(fargs, place, loc), Intrinsic::RintF32 => codegen_simple_intrinsic!(Rintf), @@ -546,7 +540,10 @@ impl GotocCtx<'_> { assert!(self.place_ty_stable(place).kind().is_unit()); self.codegen_write_bytes(fargs, farg_types, loc) } - Intrinsic::SizeOfVal | Intrinsic::MinAlignOfVal => { + Intrinsic::PtrOffsetFrom + | Intrinsic::PtrOffsetFromUnsigned + | Intrinsic::SizeOfVal + | Intrinsic::MinAlignOfVal => { unreachable!("Intrinsic `{}` is handled before codegen", intrinsic_str) } // Unimplemented @@ -1025,77 +1022,6 @@ impl GotocCtx<'_> { self.codegen_expr_to_place_stable(p, dst_ptr, loc) } - /// ptr_offset_from returns the offset between two pointers - /// - fn codegen_ptr_offset_from(&mut self, fargs: Vec, p: &Place, loc: Location) -> Stmt { - let (offset_expr, offset_overflow) = self.codegen_ptr_offset_from_expr(fargs); - - // Check that computing `offset` in bytes would not overflow an `isize` - // These checks may allow a wrapping-around behavior in CBMC: - // https://github.com/model-checking/kani/issues/1150 - let overflow_check = self.codegen_assert_assume( - offset_overflow.overflowed.not(), - PropertyClass::ArithmeticOverflow, - "attempt to compute offset in bytes which would overflow an `isize`", - loc, - ); - - let offset_expr = self.codegen_expr_to_place_stable(p, offset_expr, loc); - Stmt::block(vec![overflow_check, offset_expr], loc) - } - - /// `ptr_offset_from_unsigned` returns the offset between two pointers where the order is known. - /// The logic is similar to `ptr_offset_from` but the return value is a `usize`. - /// See for more details - fn codegen_ptr_offset_from_unsigned( - &mut self, - fargs: Vec, - p: &Place, - loc: Location, - ) -> Stmt { - let (offset_expr, offset_overflow) = self.codegen_ptr_offset_from_expr(fargs); - - // Check that computing `offset` in bytes would not overflow an `isize` - // These checks may allow a wrapping-around behavior in CBMC: - // https://github.com/model-checking/kani/issues/1150 - let overflow_check = self.codegen_assert_assume( - offset_overflow.overflowed.not(), - PropertyClass::ArithmeticOverflow, - "attempt to compute offset in bytes which would overflow an `isize`", - loc, - ); - - let non_negative_check = self.codegen_assert_assume( - offset_overflow.result.is_non_negative(), - PropertyClass::SafetyCheck, - "attempt to compute unsigned offset with negative distance", - loc, - ); - - let offset_expr = - self.codegen_expr_to_place_stable(p, offset_expr.cast_to(Type::size_t()), loc); - Stmt::block(vec![overflow_check, non_negative_check, offset_expr], loc) - } - - /// Both `ptr_offset_from` and `ptr_offset_from_unsigned` return the offset between two pointers. - /// This function implements the common logic between them. - fn codegen_ptr_offset_from_expr( - &mut self, - mut fargs: Vec, - ) -> (Expr, ArithmeticOverflowResult) { - let dst_ptr = fargs.remove(0); - let src_ptr = fargs.remove(0); - - // Compute the offset with standard substraction using `isize` - let cast_dst_ptr = dst_ptr.clone().cast_to(Type::ssize_t()); - let cast_src_ptr = src_ptr.clone().cast_to(Type::ssize_t()); - let offset_overflow = cast_dst_ptr.sub_overflow(cast_src_ptr); - - // Re-compute the offset with standard substraction (no casts this time) - let ptr_offset_expr = dst_ptr.sub(src_ptr); - (ptr_offset_expr, offset_overflow) - } - /// A transmute is a bitcast from the argument type to the return type. /// /// diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 38522fae837f..8d1ab5ef939d 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -83,6 +83,10 @@ pub enum KaniModel { IsSlicePtrInitialized, #[strum(serialize = "OffsetModel")] Offset, + #[strum(serialize = "PtrOffsetFromModel")] + PtrOffsetFrom, + #[strum(serialize = "PtrSubPtrModel")] + PtrSubPtr, #[strum(serialize = "RunContractModel")] RunContract, #[strum(serialize = "RunLoopContractModel")] diff --git a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs index ad4238574d63..79238e423e62 100644 --- a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs @@ -167,6 +167,8 @@ impl MutMirVisitor for ReplaceIntrinsicCallVisitor<'_> { let model = match intrinsic { Intrinsic::SizeOfVal => self.models[&KaniModel::SizeOfVal], Intrinsic::MinAlignOfVal => self.models[&KaniModel::AlignOfVal], + Intrinsic::PtrOffsetFrom => self.models[&KaniModel::PtrOffsetFrom], + Intrinsic::PtrOffsetFromUnsigned => self.models[&KaniModel::PtrSubPtr], // The rest is handled in codegen. _ => { return self.super_terminator(term); diff --git a/library/kani_core/src/models.rs b/library/kani_core/src/models.rs index 121be62fd499..5a7debaa5f29 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -45,6 +45,39 @@ macro_rules! generate_models { } } + #[kanitool::fn_marker = "PtrOffsetFromModel"] + pub unsafe fn ptr_offset_from(ptr1: *const T, ptr2: *const T) -> isize { + if ptr1 == ptr2 { + 0 + } else { + kani::safety_check( + kani::mem::same_allocation_internal(ptr1, ptr2), + "Offset result and original pointer should point to the same allocation", + ); + kani::safety_check( + core::mem::size_of::() > 0, + "Cannot compute offset of a ZST", + ); + // The offset must fit in isize since this represents the same allocation. + let offset_bytes = ptr1.addr().wrapping_sub(ptr2.addr()) as isize; + // We know `t_size` is a power of two, so avoid division. + let t_size = size_of::() as isize; + kani::safety_check( + offset_bytes & (t_size - 1) == 0, + "Expected the distance between the pointers, in bytes, to be a + multiple of the size of `T`", + ); + offset_bytes >> t_size.trailing_zeros() + } + } + + #[kanitool::fn_marker = "PtrSubPtrModel"] + pub unsafe fn ptr_sub_ptr(ptr1: *const T, ptr2: *const T) -> usize { + let offset = ptr_offset_from(ptr1, ptr2); + kani::safety_check(offset >= 0, "Expected non-negative distance between pointers"); + offset as usize + } + /// An offset model that checks UB. #[kanitool::fn_marker = "OffsetModel"] pub fn offset, O: ToISize>(ptr: P, offset: O) -> P { diff --git a/tests/expected/offset-bounds-check/offset_from.expected b/tests/expected/offset-bounds-check/offset_from.expected new file mode 100644 index 000000000000..d985c9a4e318 --- /dev/null +++ b/tests/expected/offset-bounds-check/offset_from.expected @@ -0,0 +1,6 @@ +Failed Checks: assertion failed: 0 < pointee_size && pointee_size <= isize::MAX as usize +Failed Checks: Offset result and original pointer should point to the same allocation + +Verification failed for - check_offset_from_diff_alloc +Verification failed for - check_offset_from_oob_ptr +Complete - 2 successfully verified harnesses, 2 failures, 4 total. diff --git a/tests/expected/offset-bounds-check/offset_from.rs b/tests/expected/offset-bounds-check/offset_from.rs new file mode 100644 index 000000000000..7ce3edcb3657 --- /dev/null +++ b/tests/expected/offset-bounds-check/offset_from.rs @@ -0,0 +1,47 @@ +// 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_offset_from_oob_ptr() { + let val = 10u128; + let ptr: *const u128 = &val; + let ptr_oob: *const u128 = ptr.wrapping_add(10); + // SAFETY: This is not safe! + let _offset = unsafe { ptr_oob.offset_from(ptr) }; +} + +#[kani::proof] +fn check_offset_from_diff_alloc() { + let val1 = 10u128; + let val2 = 0u128; + let ptr1: *const u128 = &val1; + let ptr2: *const u128 = &val2; + // SAFETY: This is not safe! + let offset = unsafe { ptr1.offset_from(ptr2) }; + assert!(offset != 0); +} + +#[kani::proof] +#[kani::should_panic] +fn check_offset_from_unit_panic() { + let val1 = kani::any(); + let val2 = kani::any(); + let ptr1: *const () = &val1 as *const _ as *const (); + let ptr2: *const () = &val2 as *const _ as *const (); + // SAFETY: This is safe but will panic... + let _offset = unsafe { ptr1.offset_from(ptr2) }; +} + +#[kani::proof] +fn check_offset_from_same_dangling() { + let val = 10u128; + let ptr: *const u128 = &val; + let ptr_oob_1: *const u128 = ptr.wrapping_add(10); + let ptr_oob_2: *const u128 = ptr.wrapping_add(5).wrapping_add(5); + // SAFETY: This is safe since the pointer is the same! + let offset = unsafe { ptr_oob_1.offset_from(ptr_oob_2) }; + assert_eq!(offset, 0); +} diff --git a/tests/expected/offset-bounds-check/sub_ptr.expected b/tests/expected/offset-bounds-check/sub_ptr.expected new file mode 100644 index 000000000000..c9ac1c983a68 --- /dev/null +++ b/tests/expected/offset-bounds-check/sub_ptr.expected @@ -0,0 +1,65 @@ +Kani Rust Verifier 0.56.0 (standalone) +Checking harness check_sub_ptr_same_dangling... + +VERIFICATION RESULT: + ** 0 of 13 failed (3 unreachable) + +VERIFICATION:- SUCCESSFUL +Verification Time: 0.03525919s + +Checking harness check_sub_ptr_unit_panic... + +VERIFICATION RESULT: + ** 1 of 12 failed (3 unreachable) +Failed Checks: assertion failed: 0 < pointee_size && pointee_size <= isize::MAX as usize + File: "/home/ANT.AMAZON.COM/celinval/.rustup/toolchains/nightly-2024-11-28-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs", line 784, in std::ptr::const_ptr::::sub_ptr + +VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected) +Verification Time: 0.032447934s + +Checking harness check_sub_ptr_negative_result... + +VERIFICATION RESULT: + ** 1 of 15 failed (1 unreachable) +Failed Checks: Expected non-negative distance between pointers + File: "/home/ANT.AMAZON.COM/celinval/workspace/kani-project/kani/library/kani/src/lib.rs", line 54, in kani::rustc_intrinsics::ptr_sub_ptr:: + +VERIFICATION:- FAILED +Verification Time: 0.05667276s + +Checking harness check_sub_ptr_diff_alloc... + +VERIFICATION RESULT: + ** 1 of 12 failed (3 unreachable) +Failed Checks: Offset result and original pointer should point to the same allocation + File: "/home/ANT.AMAZON.COM/celinval/workspace/kani-project/kani/library/kani/src/lib.rs", line 54, in kani::rustc_intrinsics::ptr_offset_from:: + +VERIFICATION:- FAILED +Verification Time: 0.037252095s + +Checking harness check_sub_ptr_oob_ptr... + +VERIFICATION RESULT: + ** 1 of 12 failed (2 unreachable) +Failed Checks: Offset result and original pointer should point to the same allocation + File: "/home/ANT.AMAZON.COM/celinval/workspace/kani-project/kani/library/kani/src/lib.rs", line 54, in kani::rustc_intrinsics::ptr_offset_from:: + +VERIFICATION:- FAILED +Verification Time: 0.040543832s + +Checking harness check_sub_ptr_self_oob... + +VERIFICATION RESULT: + ** 1 of 12 failed (2 unreachable) +Failed Checks: Offset result and original pointer should point to the same allocation + File: "/home/ANT.AMAZON.COM/celinval/workspace/kani-project/kani/library/kani/src/lib.rs", line 54, in kani::rustc_intrinsics::ptr_offset_from:: + +VERIFICATION:- FAILED +Verification Time: 0.036195125s + +Summary: +Verification failed for - check_sub_ptr_negative_result +Verification failed for - check_sub_ptr_diff_alloc +Verification failed for - check_sub_ptr_oob_ptr +Verification failed for - check_sub_ptr_self_oob +Complete - 2 successfully verified harnesses, 4 failures, 6 total. diff --git a/tests/expected/offset-bounds-check/sub_ptr.rs b/tests/expected/offset-bounds-check/sub_ptr.rs new file mode 100644 index 000000000000..7ddfa96d94f8 --- /dev/null +++ b/tests/expected/offset-bounds-check/sub_ptr.rs @@ -0,0 +1,70 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Check that Kani can detect UB due to `sub_ptr` with out-of-bounds pointer or wrong order. + +#![feature(ptr_sub_ptr)] + +#[kani::proof] +fn check_sub_ptr_self_oob() { + let val = 10u128; + let ptr: *const u128 = &val; + let ptr_oob: *const u128 = ptr.wrapping_add(10); + // SAFETY: This is not safe! + let _offset = unsafe { ptr_oob.sub_ptr(ptr) }; +} + +#[kani::proof] +fn check_sub_ptr_oob_ptr() { + let val = 10u128; + let ptr: *const u128 = &val; + let ptr_oob: *const u128 = ptr.wrapping_sub(10); + // SAFETY: This is not safe! + let _offset = unsafe { ptr.sub_ptr(ptr_oob) }; +} + +#[kani::proof] +fn check_sub_ptr_diff_alloc() { + let val1 = kani::any(); + let val2 = kani::any(); + let ptr1: *const u128 = &val1; + let ptr2: *const u128 = &val2; + // SAFETY: This is not safe! + let _offset = unsafe { ptr1.sub_ptr(ptr2) }; +} + +#[kani::proof] +fn check_sub_ptr_negative_result() { + let val: [u8; 10] = kani::any(); + let ptr_first: *const _ = &val[0]; + let ptr_last: *const _ = &val[9]; + // SAFETY: This is safe! + let offset_ok = unsafe { ptr_last.sub_ptr(ptr_first) }; + + // SAFETY: This is not safe! + let offset_not_ok = unsafe { ptr_first.sub_ptr(ptr_last) }; + + // Just use the result. + assert!(offset_ok != offset_not_ok); +} + +#[kani::proof] +#[kani::should_panic] +fn check_sub_ptr_unit_panic() { + let val1 = kani::any(); + let val2 = kani::any(); + let ptr1: *const () = &val1 as *const _ as *const (); + let ptr2: *const () = &val2 as *const _ as *const (); + // SAFETY: This is safe but will panic... + let _offset = unsafe { ptr1.sub_ptr(ptr2) }; +} + +#[kani::proof] +fn check_sub_ptr_same_dangling() { + let val = 10u128; + let ptr: *const u128 = &val; + let ptr_oob_1: *const u128 = ptr.wrapping_add(10); + let ptr_oob_2: *const u128 = ptr.wrapping_add(5).wrapping_add(5); + // SAFETY: This is safe since the pointer is the same! + let offset = unsafe { ptr_oob_1.sub_ptr(ptr_oob_2) }; + assert_eq!(offset, 0); +} From e321b712f58ca6d279a26dbdb415ca63920f4cc7 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 13 Dec 2024 12:06:21 -0500 Subject: [PATCH 08/10] fix tests --- kani-driver/src/cbmc_property_renderer.rs | 1 - .../arbitrary/ptrs/pointer_inbounds.rs | 12 ++++--- .../intrinsics/offset-same-object/expected | 3 +- .../ptr_offset_from_unsigned/expected | 2 +- .../offset-bounds-check/sub_ptr.expected | 36 ------------------- tests/expected/offset-wraps-around/expected | 2 +- 6 files changed, 11 insertions(+), 45 deletions(-) diff --git a/kani-driver/src/cbmc_property_renderer.rs b/kani-driver/src/cbmc_property_renderer.rs index 5c10d08badb6..78ee9dd8ea02 100644 --- a/kani-driver/src/cbmc_property_renderer.rs +++ b/kani-driver/src/cbmc_property_renderer.rs @@ -61,7 +61,6 @@ static CBMC_ALT_DESCRIPTIONS: Lazy = Lazy::new(|| { ("NaN on /", Some("NaN on division")), ("NaN on *", Some("NaN on multiplication")), ]); - map.insert("pointer", vec![("same object violation", None)]); map.insert("pointer_arithmetic", vec![ ("pointer relation: deallocated dynamic object", None), ("pointer relation: dead object", None), diff --git a/tests/expected/arbitrary/ptrs/pointer_inbounds.rs b/tests/expected/arbitrary/ptrs/pointer_inbounds.rs index 36e4abeff48b..48746c9ed5fe 100644 --- a/tests/expected/arbitrary/ptrs/pointer_inbounds.rs +++ b/tests/expected/arbitrary/ptrs/pointer_inbounds.rs @@ -48,9 +48,13 @@ fn check_overlap() { kani::cover!(ptr_1 == ptr_2, "Same"); kani::cover!(ptr_1 == unsafe { ptr_2.byte_add(1) }, "Overlap"); - let distance = unsafe { ptr_1.offset_from(ptr_2) }; - kani::cover!(distance > 0, "Greater"); - kani::cover!(distance < 0, "Smaller"); + // offset_from is only safe if the distance between the pointers in bytes is a multiple of size_of::, + // which holds if either both ptr_1 and ptr_2 are aligned or neither are. + if ptr_1.is_aligned() == ptr_2.is_aligned() { + let distance = unsafe { ptr_1.offset_from(ptr_2) }; + kani::cover!(distance > 0, "Greater"); + kani::cover!(distance < 0, "Smaller"); - assert!(distance >= -4 && distance <= 4, "Expected a maximum distance of 4 elements"); + assert!(distance >= -4 && distance <= 4, "Expected a maximum distance of 4 elements"); + } } diff --git a/tests/expected/intrinsics/offset-same-object/expected b/tests/expected/intrinsics/offset-same-object/expected index bfb930e2bf03..0d267dddfaae 100644 --- a/tests/expected/intrinsics/offset-same-object/expected +++ b/tests/expected/intrinsics/offset-same-object/expected @@ -1,2 +1 @@ -FAILURE\ -"same object violation" \ No newline at end of file +Failed Checks: Offset result and original pointer should point to the same allocation diff --git a/tests/expected/intrinsics/ptr_offset_from_unsigned/expected b/tests/expected/intrinsics/ptr_offset_from_unsigned/expected index 8a893dea24be..9daa67d4f541 100644 --- a/tests/expected/intrinsics/ptr_offset_from_unsigned/expected +++ b/tests/expected/intrinsics/ptr_offset_from_unsigned/expected @@ -1 +1 @@ -Failed Checks: attempt to compute unsigned offset with negative distance +Failed Checks: Expected non-negative distance between pointers diff --git a/tests/expected/offset-bounds-check/sub_ptr.expected b/tests/expected/offset-bounds-check/sub_ptr.expected index c9ac1c983a68..611fe2e565c7 100644 --- a/tests/expected/offset-bounds-check/sub_ptr.expected +++ b/tests/expected/offset-bounds-check/sub_ptr.expected @@ -1,61 +1,25 @@ -Kani Rust Verifier 0.56.0 (standalone) Checking harness check_sub_ptr_same_dangling... - -VERIFICATION RESULT: - ** 0 of 13 failed (3 unreachable) - VERIFICATION:- SUCCESSFUL -Verification Time: 0.03525919s Checking harness check_sub_ptr_unit_panic... - -VERIFICATION RESULT: - ** 1 of 12 failed (3 unreachable) Failed Checks: assertion failed: 0 < pointee_size && pointee_size <= isize::MAX as usize - File: "/home/ANT.AMAZON.COM/celinval/.rustup/toolchains/nightly-2024-11-28-x86_64-unknown-linux-gnu/lib/rustlib/src/rust/library/core/src/ptr/const_ptr.rs", line 784, in std::ptr::const_ptr::::sub_ptr - VERIFICATION:- SUCCESSFUL (encountered one or more panics as expected) -Verification Time: 0.032447934s Checking harness check_sub_ptr_negative_result... - -VERIFICATION RESULT: - ** 1 of 15 failed (1 unreachable) Failed Checks: Expected non-negative distance between pointers - File: "/home/ANT.AMAZON.COM/celinval/workspace/kani-project/kani/library/kani/src/lib.rs", line 54, in kani::rustc_intrinsics::ptr_sub_ptr:: - VERIFICATION:- FAILED -Verification Time: 0.05667276s Checking harness check_sub_ptr_diff_alloc... - -VERIFICATION RESULT: - ** 1 of 12 failed (3 unreachable) Failed Checks: Offset result and original pointer should point to the same allocation - File: "/home/ANT.AMAZON.COM/celinval/workspace/kani-project/kani/library/kani/src/lib.rs", line 54, in kani::rustc_intrinsics::ptr_offset_from:: - VERIFICATION:- FAILED -Verification Time: 0.037252095s Checking harness check_sub_ptr_oob_ptr... - -VERIFICATION RESULT: - ** 1 of 12 failed (2 unreachable) Failed Checks: Offset result and original pointer should point to the same allocation - File: "/home/ANT.AMAZON.COM/celinval/workspace/kani-project/kani/library/kani/src/lib.rs", line 54, in kani::rustc_intrinsics::ptr_offset_from:: - VERIFICATION:- FAILED -Verification Time: 0.040543832s Checking harness check_sub_ptr_self_oob... - -VERIFICATION RESULT: - ** 1 of 12 failed (2 unreachable) Failed Checks: Offset result and original pointer should point to the same allocation - File: "/home/ANT.AMAZON.COM/celinval/workspace/kani-project/kani/library/kani/src/lib.rs", line 54, in kani::rustc_intrinsics::ptr_offset_from:: - VERIFICATION:- FAILED -Verification Time: 0.036195125s Summary: Verification failed for - check_sub_ptr_negative_result diff --git a/tests/expected/offset-wraps-around/expected b/tests/expected/offset-wraps-around/expected index 2fedc9da1a89..3ad0fbdad6e7 100644 --- a/tests/expected/offset-wraps-around/expected +++ b/tests/expected/offset-wraps-around/expected @@ -5,7 +5,7 @@ Checking harness harness_without_ub... VERIFICATION:- SUCCESSFUL Checking harness original_harness... -Failed Checks: assertion failed: high_offset == wrapped_offset.try_into().unwrap() +Failed Checks: Offset result and original pointer should point to the same allocation VERIFICATION:- FAILED Verification failed for - original_harness From 049c1da401911fe84803edc9140368d3a66268f5 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 13 Dec 2024 12:36:22 -0500 Subject: [PATCH 09/10] add test for distance offset_from UB --- .../arbitrary/ptrs/pointer_inbounds.rs | 2 -- .../offset-from-distance-check/expected | 3 +++ .../offset-from-distance-check/main.rs | 18 ++++++++++++++++++ 3 files changed, 21 insertions(+), 2 deletions(-) create mode 100644 tests/expected/offset-from-distance-check/expected create mode 100644 tests/expected/offset-from-distance-check/main.rs diff --git a/tests/expected/arbitrary/ptrs/pointer_inbounds.rs b/tests/expected/arbitrary/ptrs/pointer_inbounds.rs index 48746c9ed5fe..58e92703b9c0 100644 --- a/tests/expected/arbitrary/ptrs/pointer_inbounds.rs +++ b/tests/expected/arbitrary/ptrs/pointer_inbounds.rs @@ -9,8 +9,6 @@ //! Kani will detect the usage of MaybeUninit and fail the verification. extern crate kani; -use kani::PointerGenerator; - #[kani::proof] fn check_inbounds() { let mut generator = kani::pointer_generator::(); diff --git a/tests/expected/offset-from-distance-check/expected b/tests/expected/offset-from-distance-check/expected new file mode 100644 index 000000000000..d88ef6daeceb --- /dev/null +++ b/tests/expected/offset-from-distance-check/expected @@ -0,0 +1,3 @@ +Failed Checks: Expected the distance between the pointers, in bytes, to be a + multiple of the size of `T` +VERIFICATION:- FAILED \ No newline at end of file diff --git a/tests/expected/offset-from-distance-check/main.rs b/tests/expected/offset-from-distance-check/main.rs new file mode 100644 index 000000000000..2c7471fb4fe8 --- /dev/null +++ b/tests/expected/offset-from-distance-check/main.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z mem-predicates +//! Check that Kani detects UB for offset_from when the distance between the pointers is not a multiple of size_of:: +extern crate kani; + +#[kani::proof] +fn check_offset_from_distance_ub() { + let mut generator = kani::pointer_generator::(); + let ptr_1 = generator.any_in_bounds::().ptr; + let ptr_2 = generator.any_in_bounds::().ptr; + + // offset_from is only safe if the distance between the pointers in bytes is a multiple of size_of::, + // which holds if either both ptr_1 and ptr_2 are aligned or neither are. + // However, any_in_bounds makes no guarantees about alignment, so the above condition may not hold and verification should fail. + unsafe { ptr_1.offset_from(ptr_2) }; +} From b3beba3ab55e866d69c83958ac98c5af22198e04 Mon Sep 17 00:00:00 2001 From: Carolyn Zech Date: Fri, 13 Dec 2024 13:55:58 -0500 Subject: [PATCH 10/10] Add test for pointers to ZSTs Moved the ZST check above the check for the same pointer, since the function panics for all ZST pointers --- library/kani_core/src/models.rs | 8 ++++---- tests/expected/offset-from-zst/expected | 1 + tests/expected/offset-from-zst/main.rs | 18 ++++++++++++++++++ 3 files changed, 23 insertions(+), 4 deletions(-) create mode 100644 tests/expected/offset-from-zst/expected create mode 100644 tests/expected/offset-from-zst/main.rs diff --git a/library/kani_core/src/models.rs b/library/kani_core/src/models.rs index 5a7debaa5f29..cc5cce658205 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -47,6 +47,10 @@ macro_rules! generate_models { #[kanitool::fn_marker = "PtrOffsetFromModel"] pub unsafe fn ptr_offset_from(ptr1: *const T, ptr2: *const T) -> isize { + kani::safety_check( + core::mem::size_of::() > 0, + "Cannot compute offset of a ZST", + ); if ptr1 == ptr2 { 0 } else { @@ -54,10 +58,6 @@ macro_rules! generate_models { kani::mem::same_allocation_internal(ptr1, ptr2), "Offset result and original pointer should point to the same allocation", ); - kani::safety_check( - core::mem::size_of::() > 0, - "Cannot compute offset of a ZST", - ); // The offset must fit in isize since this represents the same allocation. let offset_bytes = ptr1.addr().wrapping_sub(ptr2.addr()) as isize; // We know `t_size` is a power of two, so avoid division. diff --git a/tests/expected/offset-from-zst/expected b/tests/expected/offset-from-zst/expected new file mode 100644 index 000000000000..82927d2c52cf --- /dev/null +++ b/tests/expected/offset-from-zst/expected @@ -0,0 +1 @@ +VERIFICATION:- FAILED \ No newline at end of file diff --git a/tests/expected/offset-from-zst/main.rs b/tests/expected/offset-from-zst/main.rs new file mode 100644 index 000000000000..876187c49b11 --- /dev/null +++ b/tests/expected/offset-from-zst/main.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +// kani-flags: -Z mem-predicates +//! Check that Kani detects UB for offset_from for pointers to ZSTs. +//! The pointer::offset_from method has an assertion to check for ZSTs *before* it calls the intrinsic ptr_offset_from. +//! Since we model the instrinsic, our ZST assertion comes too late, after the rustc assertion has actually failed. +//! So for now, this test does not actually test our modeling of the intrinsic, since verification fails before the intrinsic call, because of the failed rustc assertion. +//! But the Rust developers may remove the assertion in the future, in which case this test would prevent regression. +extern crate kani; + +#[kani::proof] +fn check_offset_from_zst_ub() { + let x = (); + let ptr_1 = &x as *const (); + let ptr_2 = &x as *const (); + unsafe { ptr_1.offset_from(ptr_2) }; +}