diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index ffe404c092c9..3dccbea5837f 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs @@ -456,7 +456,7 @@ impl GotocCtx<'_> { | TyKind::RigidTy(RigidTy::Dynamic(..)) => { inner_goto_expr.member("data", &self.symbol_table) } - TyKind::RigidTy(RigidTy::Adt(..)) + TyKind::RigidTy(RigidTy::Adt(..)) | TyKind::RigidTy(RigidTy::Tuple(..)) if self.is_unsized(inner_mir_typ_internal) => { // in tests/kani/Strings/os_str_reduced.rs, we see diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 5aaba74a939a..75943b23a392 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -149,6 +149,37 @@ impl GotocHook for Assert { } } +struct SafetyCheck; +impl GotocHook for SafetyCheck { + fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool { + unreachable!("{UNEXPECTED_CALL}") + } + + fn handle( + &self, + gcx: &mut GotocCtx, + _instance: Instance, + mut fargs: Vec, + _assign_to: &Place, + target: Option, + span: Span, + ) -> Stmt { + assert_eq!(fargs.len(), 2); + let 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, + ) + } +} + struct Check; impl GotocHook for Check { fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool { @@ -619,13 +650,14 @@ impl GotocHook for LoopInvariantRegister { } pub fn fn_hooks() -> GotocHooks { - let kani_lib_hooks: [(KaniHook, Rc); 11] = [ - (KaniHook::Assert, Rc::new(Assert)), + let kani_lib_hooks = [ + (KaniHook::Assert, Rc::new(Assert) as Rc), (KaniHook::Assume, Rc::new(Assume)), (KaniHook::Panic, Rc::new(Panic)), (KaniHook::Check, Rc::new(Check)), (KaniHook::Cover, Rc::new(Cover)), (KaniHook::AnyRaw, Rc::new(Nondet)), + (KaniHook::SafetyCheck, Rc::new(SafetyCheck)), (KaniHook::IsAllocated, Rc::new(IsAllocated)), (KaniHook::PointerObject, Rc::new(PointerObject)), (KaniHook::PointerOffset, Rc::new(PointerOffset)), diff --git a/kani-compiler/src/kani_middle/abi.rs b/kani-compiler/src/kani_middle/abi.rs index 45f224ee236e..88068458a028 100644 --- a/kani-compiler/src/kani_middle/abi.rs +++ b/kani-compiler/src/kani_middle/abi.rs @@ -13,7 +13,6 @@ pub struct LayoutOf { layout: LayoutShape, } -#[allow(dead_code)] // TODO: Remove this in https://github.com/model-checking/kani/pull/3687 impl LayoutOf { /// Create the layout structure for the given type pub fn new(ty: Ty) -> LayoutOf { diff --git a/kani-compiler/src/kani_middle/intrinsics.rs b/kani-compiler/src/kani_middle/intrinsics.rs index c32ec38a3696..a3451c99e029 100644 --- a/kani-compiler/src/kani_middle/intrinsics.rs +++ b/kani-compiler/src/kani_middle/intrinsics.rs @@ -2,6 +2,9 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! This module contains a MIR pass that replaces some intrinsics by rust intrinsics models as //! well as validation logic that can only be added during monomorphization. +//! +//! TODO: Move this code to `[crate::kani_middle::transform::RustcIntrinsicsPass]` since we can do +//! proper error handling after monomorphization. use rustc_index::IndexVec; use rustc_middle::mir::{Body, Const as mirConst, ConstValue, Operand, TerminatorKind}; use rustc_middle::mir::{Local, LocalDecl}; diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 10441fd00f1e..974872f8f279 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -44,6 +44,10 @@ pub enum KaniFunction { pub enum KaniIntrinsic { #[strum(serialize = "AnyModifiesIntrinsic")] AnyModifies, + #[strum(serialize = "CheckedAlignOfIntrinsic")] + CheckedAlignOf, + #[strum(serialize = "CheckedSizeOfIntrinsic")] + CheckedSizeOf, #[strum(serialize = "IsInitializedIntrinsic")] IsInitialized, #[strum(serialize = "ValidValueIntrinsic")] @@ -55,6 +59,8 @@ pub enum KaniIntrinsic { /// Kani models are Rust functions that model some runtime behavior used by Kani instrumentation. #[derive(Debug, Copy, Clone, Eq, PartialEq, IntoStaticStr, EnumIter, EnumString, Hash)] pub enum KaniModel { + #[strum(serialize = "AlignOfDynObjectModel")] + AlignOfDynObject, #[strum(serialize = "AnyModel")] Any, #[strum(serialize = "CopyInitStateModel")] @@ -85,6 +91,10 @@ pub enum KaniModel { SetSlicePtrInitialized, #[strum(serialize = "SetStrPtrInitializedModel")] SetStrPtrInitialized, + #[strum(serialize = "SizeOfDynObjectModel")] + SizeOfDynObject, + #[strum(serialize = "SizeOfSliceObjectModel")] + SizeOfSliceObject, #[strum(serialize = "StoreArgumentModel")] StoreArgument, #[strum(serialize = "WriteAnySliceModel")] @@ -121,6 +131,8 @@ pub enum KaniHook { PointerObject, #[strum(serialize = "PointerOffsetHook")] PointerOffset, + #[strum(serialize = "SafetyCheckHook")] + SafetyCheck, #[strum(serialize = "UntrackedDerefHook")] UntrackedDeref, } diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 9c541d1e1ee4..206c0160a80d 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -8,6 +8,7 @@ //! by the transformation. use crate::args::ExtraChecks; +use crate::kani_middle::abi::LayoutOf; use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::kani_functions::{KaniFunction, KaniIntrinsic, KaniModel}; use crate::kani_middle::transform::body::{ @@ -23,11 +24,13 @@ use crate::kani_queries::QueryDb; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; use stable_mir::mir::{ - BasicBlock, BinOp, Body, ConstOperand, Mutability, Operand, Place, RETURN_LOCAL, Rvalue, - Statement, StatementKind, Terminator, TerminatorKind, UnwindAction, + AggregateKind, BasicBlock, BinOp, Body, ConstOperand, Local, Mutability, Operand, Place, + RETURN_LOCAL, Rvalue, Statement, StatementKind, Terminator, TerminatorKind, UnOp, UnwindAction, }; use stable_mir::target::MachineInfo; -use stable_mir::ty::{FnDef, MirConst, RigidTy, Ty, TyKind, UintTy}; +use stable_mir::ty::{ + AdtDef, FnDef, GenericArgKind, GenericArgs, MirConst, RigidTy, Ty, TyKind, UintTy, +}; use std::collections::HashMap; use std::fmt::Debug; use std::str::FromStr; @@ -67,6 +70,8 @@ impl TransformPass for IntrinsicGeneratorPass { attributes.fn_marker().and_then(|name| KaniIntrinsic::from_str(name.as_str()).ok()) { match kani_intrinsic { + KaniIntrinsic::CheckedAlignOf => (true, self.checked_align_of(body, instance)), + KaniIntrinsic::CheckedSizeOf => (true, self.checked_size_of(body, instance)), KaniIntrinsic::IsInitialized => (true, self.is_initialized_body(body)), KaniIntrinsic::ValidValue => (true, self.valid_value_body(body)), // This is handled in contracts pass for now. @@ -368,4 +373,255 @@ impl IntrinsicGeneratorPass { } new_body.into() } + + /// Generate the body for retrieving the size of a val starting from its raw pointer. + /// + /// The body generated will depend on the type of the pointer. + /// + /// For sized type, this will generate: + /// ```mir + /// _0: Option; + /// _1: *const T; + /// bb0: + /// _0 = Some(); + /// return + /// ``` + /// + /// For types with foreign tails, this will generate a `None` value. + /// + /// For types with trait and slice tails, gather information about the type and invoke + /// `size_of_dyn_object` and `size_of_slice_object` respectively. E.g.:: + /// ``` + /// _0: Option; + /// _1: *const T; + /// bb0: + /// _0 = size_of_dyn_object(_1, , ); + /// bb1: + /// return + /// ``` + fn checked_size_of(&mut self, body: Body, instance: Instance) -> Body { + // Get information about the pointer passed as an argument. + let ptr_arg = body.arg_locals().first().expect("Expected a pointer argument"); + let ptr_ty = ptr_arg.ty; + let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ptr_ty.kind() else { + unreachable!("Expected a pointer argument, but got {ptr_ty}") + }; + let pointee_layout = LayoutOf::new(pointee_ty); + debug!(?ptr_ty, ?pointee_layout, "checked_size_of"); + + // Get information about the return value (`Option`). + let ret_ty = body.ret_local().ty; + let TyKind::RigidTy(RigidTy::Adt(option_def, option_args)) = ret_ty.kind() else { + unreachable!("Expected `Option` as return but found `{ret_ty}`") + }; + + // Modify the body according to the type of pointer. + let mut new_body = MutableBody::from(body); + new_body.clear_body(TerminatorKind::Return); + let mut source = SourceInstruction::Terminator { bb: 0 }; + let span = source.span(new_body.blocks()); + if pointee_layout.is_sized() { + // Return Some(); + let val_op = new_body.new_uint_operand( + pointee_layout.size_of().unwrap() as _, + UintTy::Usize, + span, + ); + let ret_val = build_some(option_def, option_args, val_op); + new_body.assign_to( + Place::from(RETURN_LOCAL), + ret_val, + &mut source, + InsertPosition::Before, + ); + } else if pointee_layout.has_trait_tail() { + // Return `size_of_dyn_object::(ptr, head_size, head_align)`. + let tail_ty = pointee_layout.unsized_tail().unwrap(); + let mut instance_args = instance.args(); // This should contain `T` already. + instance_args.0.push(GenericArgKind::Type(tail_ty)); // Now push the tail type `U`. + let ptr = Operand::Copy(Place::from(Local::from(1usize))); + let head_size = + new_body.new_uint_operand(pointee_layout.size_of_head() as _, UintTy::Usize, span); + let head_align = + new_body.new_uint_operand(pointee_layout.align_of_head() as _, UintTy::Usize, span); + let operands = vec![ptr, head_size, head_align]; + self.return_model( + &mut new_body, + &mut source, + KaniModel::SizeOfDynObject, + &instance_args, + operands, + ); + } else if pointee_layout.has_slice_tail() { + // Return `size_of_slice_object::(len, elem_size, head_size, align)`. + let elem_ty = pointee_layout.unsized_tail_elem_ty().unwrap(); + let elem_layout = LayoutOf::new(elem_ty); + assert!(elem_layout.is_sized()); + + let elem_size = + new_body.new_uint_operand(elem_layout.size_of().unwrap() as _, UintTy::Usize, span); + let head_size = + new_body.new_uint_operand(pointee_layout.size_of_head() as _, UintTy::Usize, span); + let align = new_body.new_uint_operand( + pointee_layout.align_of().unwrap() as _, + UintTy::Usize, + span, + ); + let ptr = Operand::Copy(Place::from(Local::from(1usize))); + let len_local = new_body.insert_assignment( + Rvalue::UnaryOp(UnOp::PtrMetadata, ptr), + &mut source, + InsertPosition::Before, + ); + let len_op = Operand::Move(Place::from(len_local)); + let operands = vec![len_op, elem_size, head_size, align]; + self.return_model( + &mut new_body, + &mut source, + KaniModel::SizeOfSliceObject, + &instance.args(), + operands, + ); + } else { + // Cannot compute size of foreign types. Return `None`. + assert!( + pointee_layout.has_foreign_tail(), + "Expected foreign, but found `{:?}` tail instead.", + pointee_layout.unsized_tail() + ); + let ret_val = build_none(option_def, option_args); + new_body.assign_to( + Place::from(RETURN_LOCAL), + ret_val, + &mut source, + InsertPosition::Before, + ); + } + new_body.into() + } + + /// Generate the body for retrieving the alignment of the pointed to object if possible. + /// + /// The body generated will depend on the type. + /// + /// For sized type, and types with slice tails, the alignment can be computed statically, and + /// this will generate: + /// ```mir + /// _0: Option; + /// _1: *const T; + /// bb0: + /// _0 = Some(); + /// return + /// ``` + /// + /// For types with trait tail, invoke `align_of_dyn_portion`: + /// ``` + /// _0: Option; + /// _1: *const T; + /// bb0: + /// _0 = align_of_dyn_object(_1, ); + /// bb1: + /// return + /// ``` + /// + /// For types with foreign tails, this will return `None`. + fn checked_align_of(&mut self, body: Body, instance: Instance) -> Body { + // Get information about the pointer passed as an argument. + let ptr_arg = body.arg_locals().first().expect("Expected a pointer argument"); + let ptr_ty = ptr_arg.ty; + let TyKind::RigidTy(RigidTy::RawPtr(pointee_ty, _)) = ptr_ty.kind() else { + unreachable!("Expected a pointer argument, but got {ptr_ty}") + }; + let pointee_layout = LayoutOf::new(pointee_ty); + debug!(?ptr_ty, "align_of_raw"); + + // Get information about the return value (Option). + let ret_ty = body.ret_local().ty; + let TyKind::RigidTy(RigidTy::Adt(option_def, option_args)) = ret_ty.kind() else { + unreachable!("Expected `Option` as return but found `{ret_ty}`") + }; + + // Modify the body according to the type of pointer. + let mut new_body = MutableBody::from(body); + new_body.clear_body(TerminatorKind::Return); + let mut source = SourceInstruction::Terminator { bb: 0 }; + let span = source.span(new_body.blocks()); + if let Some(align) = pointee_layout.align_of() { + let val_op = new_body.new_uint_operand(align as _, UintTy::Usize, span); + let ret_val = build_some(option_def, option_args, val_op); + new_body.assign_to( + Place::from(RETURN_LOCAL), + ret_val, + &mut source, + InsertPosition::Before, + ); + } else if pointee_layout.has_trait_tail() { + // Return `align_of_dyn_object::(ptr, head_align)`. + let head_align = + new_body.new_uint_operand(pointee_layout.align_of_head() as _, UintTy::Usize, span); + let tail_ty = pointee_layout.unsized_tail().unwrap(); + let mut args = instance.args(); // This already contains `T`. + args.0.push(GenericArgKind::Type(tail_ty)); // Now push the tail type `U`. + let operands = vec![Operand::Copy(Place::from(Local::from(1usize))), head_align]; + self.return_model( + &mut new_body, + &mut source, + KaniModel::AlignOfDynObject, + &args, + operands, + ); + } else { + // Cannot compute size of foreign types. Return None! + assert!( + pointee_layout.has_foreign_tail(), + "Expected foreign, but found `{:?}` tail instead.", + pointee_layout.unsized_tail() + ); + let ret_val = build_none(option_def, option_args); + new_body.assign_to( + Place::from(RETURN_LOCAL), + ret_val, + &mut source, + InsertPosition::Before, + ); + } + new_body.into() + } + + fn return_model( + &mut self, + new_body: &mut MutableBody, + mut source: &mut SourceInstruction, + model: KaniModel, + args: &GenericArgs, + operands: Vec, + ) { + let def = self.kani_defs.get(&model.into()).unwrap(); + let size_of_dyn = Instance::resolve(*def, args).unwrap(); + new_body.insert_call( + &size_of_dyn, + &mut source, + InsertPosition::Before, + operands, + Place::from(RETURN_LOCAL), + ); + } +} + +/// Build an Rvalue `Some(val)`. +/// Since the variants of `Option` are `Some(val)` and `None`, we know we've found the `Some` variant when we find the first variant with a field. +fn build_some(option: AdtDef, args: GenericArgs, val_op: Operand) -> Rvalue { + let var_idx = option + .variants_iter() + .find_map(|var| (!var.fields().is_empty()).then_some(var.idx)) + .unwrap(); + Rvalue::Aggregate(AggregateKind::Adt(option, var_idx, args, None, None), vec![val_op]) +} + +/// Build an Rvalue `None`. +/// Since the variants of `Option` are `Some(val)` and `None`, we know we've found the `None` variant when we find the first variant without fields. +fn build_none(option: AdtDef, args: GenericArgs) -> Rvalue { + let var_idx = + option.variants_iter().find_map(|var| var.fields().is_empty().then_some(var.idx)).unwrap(); + Rvalue::Aggregate(AggregateKind::Adt(option, var_idx, args, None, None), vec![]) } diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index 75b83fd3bc76..fc47f8fec423 100644 --- a/library/kani/src/lib.rs +++ b/library/kani/src/lib.rs @@ -16,6 +16,7 @@ // Required for `rustc_diagnostic_item` and `core_intrinsics` #![allow(internal_features)] // Required for implementing memory predicates. +#![feature(layout_for_ptr)] #![feature(ptr_metadata)] #![feature(f16)] #![feature(f128)] diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index a906f3030154..551d522ba7e2 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -23,6 +23,7 @@ mod arbitrary; mod mem; mod mem_init; +mod models; pub use kani_macros::*; @@ -42,6 +43,7 @@ macro_rules! kani_lib { pub use kani_core::*; kani_core::kani_intrinsics!(core); kani_core::generate_arbitrary!(core); + kani_core::generate_models!(); pub mod mem { kani_core::kani_mem!(core); @@ -57,6 +59,7 @@ macro_rules! kani_lib { pub use kani_core::*; kani_core::kani_intrinsics!(std); kani_core::generate_arbitrary!(std); + kani_core::generate_models!(); pub mod mem { kani_core::kani_mem!(std); @@ -284,6 +287,18 @@ macro_rules! kani_intrinsics { panic!("{}", message) } + #[doc(hidden)] + #[allow(dead_code)] + #[kanitool::fn_marker = "SafetyCheckHook"] + #[inline(never)] + pub(crate) fn safety_check(cond: bool, msg: &'static str) { + #[cfg(not(feature = "concrete_playback"))] + return kani_intrinsic(); + + #[cfg(feature = "concrete_playback")] + assert!(cond, "Safety check failed: {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 ef1e277d18d0..5921b52faff2 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -44,8 +44,6 @@ macro_rules! kani_mem { ($core:tt) => { use super::kani_intrinsic; - use private::Internal; - use $core::mem::{align_of, size_of}; use $core::ptr::{DynMetadata, NonNull, Pointee}; /// Check if the pointer is valid for write access according to [crate::mem] conditions 1, 2 @@ -65,17 +63,8 @@ macro_rules! kani_mem { issue = 2690, reason = "experimental memory predicate API" )] - pub fn can_write(ptr: *mut T) -> bool - where - T: ?Sized, - ::Metadata: PtrProperties, - { - // The interface takes a mutable pointer to improve readability of the signature. - // However, using constant pointer avoid unnecessary instrumentation, and it is as powerful. - // Hence, cast to `*const T`. - let ptr: *const T = ptr; - let (thin_ptr, metadata) = ptr.to_raw_parts(); - metadata.is_ptr_aligned(thin_ptr, Internal) && is_inbounds(&metadata, thin_ptr) + pub fn can_write(ptr: *mut T) -> bool { + is_ptr_aligned(ptr) && is_inbounds(ptr) } /// Check if the pointer is valid for unaligned write access according to [crate::mem] conditions @@ -92,13 +81,9 @@ macro_rules! kani_mem { issue = 2690, reason = "experimental memory predicate API" )] - pub fn can_write_unaligned(ptr: *const T) -> bool - where - T: ?Sized, - ::Metadata: PtrProperties, - { + pub fn can_write_unaligned(ptr: *const T) -> bool { let (thin_ptr, metadata) = ptr.to_raw_parts(); - is_inbounds(&metadata, thin_ptr) + is_inbounds(ptr) } /// Checks that pointer `ptr` point to a valid value of type `T`. @@ -119,16 +104,11 @@ macro_rules! kani_mem { reason = "experimental memory predicate API" )] #[allow(clippy::not_unsafe_ptr_arg_deref)] - pub fn can_dereference(ptr: *const T) -> bool - where - T: ?Sized, - ::Metadata: PtrProperties, - { - let (thin_ptr, metadata) = ptr.to_raw_parts(); - // Need to assert `is_initialized` because non-determinism is used under the hood, so it - // does not make sense to use it inside assumption context. - metadata.is_ptr_aligned(thin_ptr, Internal) - && is_inbounds(&metadata, thin_ptr) + pub fn can_dereference(ptr: *const T) -> bool { + // Need to assert `is_initialized` because non-determinism is used under the hood, so it + // does not make sense to use it inside assumption context. + is_ptr_aligned(ptr) + && is_inbounds(ptr) && assert_is_initialized(ptr) && unsafe { has_valid_value(ptr) } } @@ -151,17 +131,11 @@ macro_rules! kani_mem { reason = "experimental memory predicate API" )] #[allow(clippy::not_unsafe_ptr_arg_deref)] - pub fn can_read_unaligned(ptr: *const T) -> bool - where - T: ?Sized, - ::Metadata: PtrProperties, - { + pub fn can_read_unaligned(ptr: *const T) -> bool { let (thin_ptr, metadata) = ptr.to_raw_parts(); // Need to assert `is_initialized` because non-determinism is used under the hood, so it // does not make sense to use it inside assumption context. - is_inbounds(&metadata, thin_ptr) - && assert_is_initialized(ptr) - && unsafe { has_valid_value(ptr) } + is_inbounds(ptr) && assert_is_initialized(ptr) && unsafe { has_valid_value(ptr) } } /// Check if two pointers points to the same allocated object, and that both pointers @@ -178,23 +152,57 @@ macro_rules! kani_mem { cbmc::same_allocation(ptr1, ptr2) } - /// Checks that `data_ptr` points to an allocation that can hold data of size calculated from `T`. + /// Compute the size of the val pointed to if it is safe to do so. + /// + /// Return `None` if an overflow would occur, or if alignment is not power of two. + /// TODO: Optimize this if T is sized. + #[kanitool::fn_marker = "CheckedSizeOfIntrinsic"] + pub fn checked_size_of_raw(ptr: *const T) -> Option { + #[cfg(not(feature = "concrete_playback"))] + return kani_intrinsic(); + + #[cfg(feature = "concrete_playback")] + if core::mem::size_of::<::Metadata>() == 0 { + // SAFETY: It is currently safe to call this with a thin pointer. + unsafe { Some(core::mem::size_of_val_raw(ptr)) } + } else { + panic!("Cannot safely compute size of `{}` at runtime", core::any::type_name::()) + } + } + + /// Compute the size of the val pointed to if safe. /// - /// This will panic if `data_ptr` points to an invalid `non_null` - fn is_inbounds(metadata: &M, data_ptr: *const ()) -> bool - where - M: PtrProperties, - T: ?Sized, - { - let sz = metadata.pointee_size(Internal); + /// Return `None` if alignment information cannot be retrieved (foreign types), or if value + /// is not power-of-two. + #[kanitool::fn_marker = "CheckedAlignOfIntrinsic"] + pub fn checked_align_of_raw(ptr: *const T) -> Option { + #[cfg(not(feature = "concrete_playback"))] + return kani_intrinsic(); + + #[cfg(feature = "concrete_playback")] + if core::mem::size_of::<::Metadata>() == 0 { + // SAFETY: It is currently safe to call this with a thin pointer. + unsafe { Some(core::mem::align_of_val_raw(ptr)) } + } else { + panic!("Cannot safely compute size of `{}` at runtime", core::any::type_name::()) + } + } + + /// Checks that `ptr` points to an allocation that can hold data of size calculated from `T`. + /// + /// This will panic if `ptr` points to an invalid `non_null` + fn is_inbounds(ptr: *const T) -> bool { + // If size overflows, then pointer cannot be inbounds. + let Some(sz) = checked_size_of_raw(ptr) else { return false }; if sz == 0 { true // ZST pointers are always valid including nullptr. - } else if data_ptr.is_null() { + } else if ptr.is_null() { false } else { // Note that this branch can't be tested in concrete execution as `is_read_ok` needs to be // stubbed. // We first assert that the data_ptr + let data_ptr = ptr as *const (); super::assert( unsafe { is_allocated(data_ptr, 0) }, "Kani does not support reasoning about pointer to unallocated memory", @@ -203,92 +211,17 @@ macro_rules! kani_mem { } } - mod private { - /// Define like this to restrict usage of PtrProperties functions outside Kani. - #[derive(Copy, Clone)] - pub struct Internal; - } - - /// Trait that allow us to extract information from pointers without de-referencing them. - #[doc(hidden)] - pub trait PtrProperties { - fn pointee_size(&self, _: Internal) -> usize; - - /// A pointer is aligned if its address is a multiple of its minimum alignment. - fn is_ptr_aligned(&self, ptr: *const (), internal: Internal) -> bool { - let min = self.min_alignment(internal); - ptr as usize % min == 0 - } - - fn min_alignment(&self, _: Internal) -> usize; - - fn dangling(&self, _: Internal) -> *const (); - } - - /// Get the information for sized types (they don't have metadata). - impl PtrProperties for () { - fn pointee_size(&self, _: Internal) -> usize { - size_of::() - } - - fn min_alignment(&self, _: Internal) -> usize { - align_of::() - } - - fn dangling(&self, _: Internal) -> *const () { - NonNull::::dangling().as_ptr() as *const _ - } - } - - /// Get the information from the str metadata. - impl PtrProperties for usize { - #[inline(always)] - fn pointee_size(&self, _: Internal) -> usize { - *self - } - - /// String slices are a UTF-8 representation of characters that have the same layout as slices - /// of type [u8]. - /// - fn min_alignment(&self, _: Internal) -> usize { - align_of::() - } - - fn dangling(&self, _: Internal) -> *const () { - NonNull::::dangling().as_ptr() as _ - } - } - - /// Get the information from the slice metadata. - impl PtrProperties<[T]> for usize { - fn pointee_size(&self, _: Internal) -> usize { - *self * size_of::() - } - - fn min_alignment(&self, _: Internal) -> usize { - align_of::() - } - - fn dangling(&self, _: Internal) -> *const () { - NonNull::::dangling().as_ptr() as _ - } - } - - /// Get the information from the vtable. - impl PtrProperties for DynMetadata - where - T: ?Sized, - { - fn pointee_size(&self, _: Internal) -> usize { - self.size_of() - } - - fn min_alignment(&self, _: Internal) -> usize { - self.align_of() - } - - fn dangling(&self, _: Internal) -> *const () { - NonNull::<&T>::dangling().as_ptr() as _ + // Return whether the pointer is aligned + #[allow(clippy::manual_is_power_of_two)] + fn is_ptr_aligned(ptr: *const T) -> bool { + // Cannot be aligned if pointer alignment cannot be computed. + let Some(align) = checked_align_of_raw(ptr) else { return false }; + if align > 0 && (align & (align - 1)) == 0 { + // Mod of power of 2 can be done with an &. + ptr as *const () as usize & (align - 1) == 0 + } else { + // Alignment is not a valid value (not a power of two). + false } } diff --git a/library/kani_core/src/models.rs b/library/kani_core/src/models.rs new file mode 100644 index 000000000000..455c8834a345 --- /dev/null +++ b/library/kani_core/src/models.rs @@ -0,0 +1,120 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Contains definitions that Kani compiler may use to model functions that are not suitable for +//! verification or functions without a body, such as intrinsics. +//! +//! Note that these are models that Kani uses by default, and they should not be user visible. +//! Thus, we separate them from stubs. +//! TODO: Move SIMD model here. + +#[macro_export] +#[allow(clippy::crate_in_macro_def)] +macro_rules! generate_models { + () => { + #[allow(dead_code)] + mod mem_models { + use core::ptr::{self, DynMetadata, Pointee}; + + /// Retrieve the size of the object pointed by the given raw pointer. + /// + /// Where `U` is a trait, and `T` is either equal to `U` or has a tail `U`. + /// + /// In cases where `T` is different than `U`, + /// `T` may have a sized portion, the head, while the unsized portion will be at its + /// tail. + /// + /// Arguments `head_size` and `head_align` represent the size and alignment of the sized + /// portion. + /// These values are known at compilation time, and they are extracted by the compiler. + /// If `T` doesn't have a sized portion, or if `T` is equal to `U`, + /// `head_size` will be set to `0`, and `head_align` will be set to 1. + /// + /// This model is used to implement `checked_size_of_raw`. + #[kanitool::fn_marker = "SizeOfDynObjectModel"] + pub(crate) fn size_of_dyn_object( + ptr: *const T, + head_size: usize, + head_align: usize, + ) -> Option + where + T: ?Sized + Pointee>, + { + let metadata = ptr::metadata(ptr); + let align = metadata.align_of().max(head_align); + if align.is_power_of_two() { + let size_dyn = metadata.size_of(); + let (total, sum_overflow) = size_dyn.overflowing_add(head_size); + // Round up size to the nearest multiple of alignment, i.e.: (size + (align - 1)) & -align + let (adjust, adjust_overflow) = total.overflowing_add(align.wrapping_sub(1)); + let adjusted_size = adjust & align.wrapping_neg(); + if sum_overflow || adjust_overflow || adjusted_size > isize::MAX as _ { + None + } else { + Some(adjusted_size) + } + } else { + None + } + } + + /// Retrieve the alignment of the object stored in the vtable. + /// + /// Where `U` is a trait, and `T` is either equal to `U` or has a tail `U`. + /// + /// In cases where `T` is different than `U`, + /// `T` may have a sized portion, the head, while the unsized portion will be at its + /// tail. + /// + /// `head_align` represents the alignment of the sized portion, + /// and its value is known at compilation time. + /// + /// If `T` doesn't have a sized portion, or if `T` is equal to `U`, + /// `head_align` will be set to 1. + /// + /// This model is used to implement `checked_aligned_of_raw`. + #[kanitool::fn_marker = "AlignOfDynObjectModel"] + pub(crate) fn align_of_dyn_object( + ptr: *const T, + head_align: usize, + ) -> Option + where + T: ?Sized + Pointee>, + { + let align = ptr::metadata(ptr).align_of().max(head_align); + align.is_power_of_two().then_some(align) + } + + /// Compute the size of a slice or object with a slice tail. + /// + /// The slice length may be a symbolic value which is computed at runtime. + /// All the other inputs are extracted and validated by Kani compiler, + /// i.e., these are well known concrete values that should be safe to use. + /// Example, align is a power-of-two and smaller than isize::MAX. + /// + /// Thus, this generate the logic to ensure the size computation does not + /// does not overflow and it is smaller than `isize::MAX`. + #[kanitool::fn_marker = "SizeOfSliceObjectModel"] + pub(crate) fn size_of_slice_object( + len: usize, + elem_size: usize, + head_size: usize, + align: usize, + ) -> Option { + let (slice_sz, mul_overflow) = elem_size.overflowing_mul(len); + let (total, sum_overflow) = slice_sz.overflowing_add(head_size); + // Round up size to the nearest multiple of alignment, i.e.: (size + (align - 1)) & -align + let (adjust, adjust_overflow) = total.overflowing_add(align.wrapping_sub(1)); + let adjusted_size = adjust & align.wrapping_neg(); + if mul_overflow + || sum_overflow + || adjust_overflow + || adjusted_size > isize::MAX as _ + { + None + } else { + Some(adjusted_size) + } + } + } + }; +} diff --git a/tests/kani/MemPredicates/adt_with_metadata.rs b/tests/kani/MemPredicates/adt_with_metadata.rs new file mode 100644 index 000000000000..aa536b26279f --- /dev/null +++ b/tests/kani/MemPredicates/adt_with_metadata.rs @@ -0,0 +1,72 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z mem-predicates +//! Check that Kani's memory predicates work for ADT with metadata. +//! TODO: Add test with packed layout and with ZST converted to dyn T. +#![feature(ptr_metadata)] + +extern crate kani; + +use kani::mem::{can_dereference, can_write}; + +#[derive(Clone, Copy, kani::Arbitrary)] +struct Wrapper { + _size: usize, + _value: T, +} + +mod valid_access { + use super::*; + use std::ptr; + #[kani::proof] + pub fn check_valid_dyn_ptr() { + let mut var: Wrapper = kani::any(); + let fat_ptr: *mut Wrapper> = &mut var as *mut _; + assert!(can_write(fat_ptr)); + } + + /// In this harness, we cast `Wrapper<[u64;4]>` to `*const [u64]` with length 5. + /// Since `Wrapper` has an extra usize, it is safe to dereference the new pointer. + #[kani::proof] + pub fn check_arbitrary_metadata_is_sound() { + let mut var: Wrapper<[u64; 4]> = kani::any(); + let fat_ptr: *mut Wrapper<[u64]> = &mut var as *mut _; + let (thin_ptr, size) = fat_ptr.to_raw_parts(); + let new_size: usize = size + 1; + let new_ptr: *const [u64] = ptr::from_raw_parts(thin_ptr, new_size); + assert!(can_dereference(new_ptr)); + } +} + +mod invalid_access { + use super::*; + use std::ptr; + #[kani::proof] + #[kani::should_panic] + pub fn check_invalid_dyn_ptr() { + unsafe fn new_dead_ptr(val: T) -> *const T { + let local = val; + &local as *const _ + } + + let raw_ptr: *const Wrapper> = + unsafe { new_dead_ptr::>(kani::any()) }; + assert!(can_dereference(raw_ptr)); + } + + /// Check that `can_dereference` correctly identifies cases where creating a pointer from raw + /// parts with an artificial size is unsafe. + #[kani::proof] + pub fn check_arbitrary_metadata() { + let mut var: Wrapper<[u64; 4]> = kani::any(); + let fat_ptr: *mut Wrapper<[u64]> = &mut var as *mut _; + let (thin_ptr, size) = fat_ptr.to_raw_parts(); + let new_size: usize = kani::any(); + let new_ptr: *const Wrapper<[u64]> = ptr::from_raw_parts(thin_ptr, new_size); + if new_size <= size { + assert!(can_dereference(new_ptr)); + } else { + assert!(!can_dereference(new_ptr)); + } + } +} diff --git a/tests/kani/MemPredicates/foreign_type.rs b/tests/kani/MemPredicates/foreign_type.rs new file mode 100644 index 000000000000..52e525c62b33 --- /dev/null +++ b/tests/kani/MemPredicates/foreign_type.rs @@ -0,0 +1,77 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// kani-flags: -Z mem-predicates -Z c-ffi +//! Check that Kani's memory predicates return that it's not safe to access pointers with foreign +//! types since it cannot compute its size. +#![feature(ptr_metadata)] +#![feature(extern_types)] + +extern crate kani; + +use kani::mem::{can_dereference, can_read_unaligned, can_write}; +use std::ffi::c_void; +use std::ptr; + +#[derive(Clone, Copy, kani::Arbitrary)] +struct Wrapper { + _size: U, + _value: T, +} + +extern "C" { + type Foreign; + type __CPROVER_size_t; + fn __CPROVER_havoc_object(p: *mut c_void); + +} + +#[kani::proof] +pub fn check_write_is_unsafe() { + let mut var: Wrapper = kani::any(); + let ptr: *mut Wrapper = &mut var as *mut _ as *mut _; + assert!(!can_write(ptr)); +} + +#[kani::proof] +pub fn check_read_is_unsafe() { + let var: usize = kani::any(); + let ptr = &var as *const _ as *const __CPROVER_size_t; + assert!(!can_dereference(ptr)); + assert!(!can_read_unaligned(ptr)); +} + +/// Kani APIs cannot tell if that's safe to write to a foreign type. +/// +/// However, foreign APIs that have knowledge of the type can still safely set new values. +#[kani::proof] +pub fn check_write_with_extern() { + let mut var = 0usize; + let ptr = &mut var as *mut _ as *mut __CPROVER_size_t; + unsafe { + __CPROVER_havoc_object(ptr as *mut c_void); + }; +} + +/// Kani APIs cannot tell if that's safe to write to a foreign type. +/// +/// However, foreign APIs that have knowledge of the type can still safely set new values, and +/// any side effect will be taken into consideration in the verification. +#[kani::proof] +#[kani::should_panic] +pub fn check_write_with_extern_side_effect() { + let mut var = 0usize; + let ptr = &mut var as *mut _ as *mut __CPROVER_size_t; + unsafe { + __CPROVER_havoc_object(ptr as *mut c_void); + }; + assert!(var == 0); +} + +/// Check that Kani can still build the foreign type using from_raw_parts. +#[kani::proof] +pub fn check_from_raw_parts() { + let mut var: Wrapper = kani::any(); + let ptr = &mut var as *mut _ as *mut (); + let fat_ptr: *mut __CPROVER_size_t = ptr::from_raw_parts_mut(ptr, ()); + assert!(!can_write(fat_ptr)); +} diff --git a/tests/kani/SizeAndAlignOfDst/fixme_unsized_foreign.rs b/tests/kani/SizeAndAlignOfDst/fixme_unsized_foreign.rs new file mode 100644 index 000000000000..64cf042969f3 --- /dev/null +++ b/tests/kani/SizeAndAlignOfDst/fixme_unsized_foreign.rs @@ -0,0 +1,48 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! Ensure we fail verification if the user tries to compute the size of a foreign item. +//! +//! Although it is currently safe to call `size_of_val` and `align_of_val` on foreign types, +//! the behavior is not well-defined. +//! +//! For now, our implementation will trigger a panic to be on the safe side. +//! +//! From : +//! > an (unstable) extern type, then this function is always safe to call, +//! > but may panic or otherwise return the wrong value, as the extern type’s layout is not known. +//! +// kani-flags: --output-format terse + +#![feature(extern_types, layout_for_ptr)] + +extern "C" { + type ExternalType; +} + +#[kani::proof] +#[kani::should_panic] +fn check_size_of_foreign() { + let tup: (u32, usize) = kani::any(); + assert_eq!(std::mem::size_of_val(&tup), 16); + + let ptr: *const (u32, ExternalType) = &tup as *const _ as *const _; + let _size = unsafe { std::mem::size_of_val_raw(ptr) }; +} + +#[kani::proof] +#[kani::should_panic] +fn check_align_of_foreign() { + let tup: (u32, usize) = kani::any(); + assert_eq!(std::mem::align_of_val(&tup), 8); + + let ptr: *const (u32, ExternalType) = &tup as *const _ as *const _; + let _align = unsafe { std::mem::align_of_val_raw(ptr) }; +} + +#[kani::proof] +fn check_foreign_layout_unknown() { + let tup: (u32, usize) = kani::any(); + let ptr: *const (u32, ExternalType) = &tup as *const _ as *const _; + assert_eq!(kani::mem::checked_align_of_raw(ptr), None); + assert_eq!(kani::mem::checked_size_of_raw(ptr), None); +} diff --git a/tests/kani/SizeAndAlignOfDst/unsized_tail.rs b/tests/kani/SizeAndAlignOfDst/unsized_tail.rs new file mode 100644 index 000000000000..efd71f5ac44f --- /dev/null +++ b/tests/kani/SizeAndAlignOfDst/unsized_tail.rs @@ -0,0 +1,115 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Ensure we compute the size correctly including padding. + +extern crate kani; + +use kani::mem::{checked_align_of_raw, checked_size_of_raw}; +use std::fmt::Debug; +use std::mem; + +#[derive(kani::Arbitrary)] +struct Pair(T, U); + +#[kani::proof] +fn check_adjusted_size_slice() { + let tup: Pair<[u8; 5], [u16; 3]> = kani::any(); + let size = std::mem::size_of_val(&tup); + + let unsized_tup: *const Pair<[u8; 5], [u16]> = &tup as *const _ as *const _; + let adjusted_size = std::mem::size_of_val(unsafe { &*unsized_tup }); + + assert_eq!(size, adjusted_size); +} + +#[kani::proof] +fn check_adjusted_size_dyn() { + const EXPECTED_SIZE: usize = size_of::>(); + let tup: Pair = kani::any(); + let size = std::mem::size_of_val(&tup); + assert_eq!(size, EXPECTED_SIZE); + + let unsized_tup: *const Pair = &tup as *const _ as *const _; + let adjusted_size = std::mem::size_of_val(unsafe { &*unsized_tup }); + assert_eq!(adjusted_size, EXPECTED_SIZE); +} + +#[kani::proof] +pub fn checked_size_of_slice_is_zero() { + let size_sized = checked_size_of_raw(&Pair((), ())); + let size_slice = checked_size_of_raw(&Pair((), [(); 2]) as &Pair<(), [()]>); + assert_eq!(size_sized, Some(0)); + assert_eq!(size_slice, Some(0)); +} + +#[kani::proof] +pub fn checked_size_of_slice_is_non_zero() { + let size_sized = checked_size_of_raw(&Pair(0u8, 19i32)); + assert_eq!(size_sized, Some(8)); + + let size_slice = checked_size_of_raw(&Pair(10u8, [1i32; 10]) as &Pair); + assert_eq!(size_slice, Some(44)); +} + +#[kani::proof] +pub fn checked_size_with_overflow() { + let original = Pair(0u8, [(); usize::MAX]); + let slice = &original as *const _ as *const Pair; + assert_eq!(checked_size_of_raw(slice), Some(1)); + + let invalid = slice as *const Pair; + assert_eq!(checked_size_of_raw(invalid), None); +} + +#[kani::proof] +pub fn checked_align_of_dyn_from_tail() { + let concrete = Pair(0u8, 19i32); + let dyn_ptr = &concrete as &Pair; + let expected = std::mem::align_of::>(); + // Check methods with concrete. + assert_eq!(checked_align_of_raw(&concrete), Some(expected)); + assert_eq!(std::mem::align_of_val(&concrete), expected); + // Check methods with dynamic. + assert_eq!(checked_align_of_raw(dyn_ptr), Some(expected)); + assert_eq!(std::mem::align_of_val(dyn_ptr), expected); +} + +#[kani::proof] +pub fn checked_align_of_dyn_from_head() { + let concrete = Pair(19i32, 10u8); + let dyn_ptr = &concrete as &Pair; + let expected = std::mem::align_of::>(); + // Check methods with concrete. + assert_eq!(checked_align_of_raw(&concrete), Some(expected)); + assert_eq!(std::mem::align_of_val(&concrete), expected); + // Check methods with dynamic. + assert_eq!(checked_align_of_raw(dyn_ptr), Some(expected)); + assert_eq!(std::mem::align_of_val(dyn_ptr), expected); +} + +#[kani::proof] +pub fn checked_align_of_slice_from_tail() { + let concrete = Pair([0u8; 5], ['a'; 7]); + let slice_ptr = &concrete as &Pair<[u8; 5], [char]>; + let expected = std::mem::align_of::>(); + // Check methods with concrete. + assert_eq!(checked_align_of_raw(&concrete), Some(expected)); + assert_eq!(std::mem::align_of_val(&concrete), expected); + // Check methods with dynamic. + assert_eq!(checked_align_of_raw(slice_ptr), Some(expected)); + assert_eq!(std::mem::align_of_val(slice_ptr), expected); +} + +#[kani::proof] +pub fn checked_align_of_slice_from_head() { + let concrete = Pair(['a'; 7], [0u8; 5]); + let slice_ptr = &concrete as &Pair<[char; 7], [u8]>; + let expected = std::mem::align_of::>(); + // Check methods with concrete. + assert_eq!(checked_align_of_raw(&concrete), Some(expected)); + assert_eq!(std::mem::align_of_val(&concrete), expected); + // Check methods with dynamic. + assert_eq!(checked_align_of_raw(slice_ptr), Some(expected)); + assert_eq!(std::mem::align_of_val(slice_ptr), expected); +} diff --git a/tests/kani/SizeAndAlignOfDst/unsized_tuple.rs b/tests/kani/SizeAndAlignOfDst/unsized_tuple.rs new file mode 100644 index 000000000000..0edae52aa0ac --- /dev/null +++ b/tests/kani/SizeAndAlignOfDst/unsized_tuple.rs @@ -0,0 +1,18 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Ensure we compute the size correctly including padding for unsized tuple. +#![feature(unsized_tuple_coercion)] + +use std::fmt::Debug; + +#[kani::proof] +fn check_adjusted_tup_size() { + let tup: (u32, [u8; 9]) = kani::any(); + let size = std::mem::size_of_val(&tup); + + let unsized_tup: *const (u32, dyn Debug) = &tup as *const _ as *const _; + let adjusted_size = std::mem::size_of_val(unsafe { &*unsized_tup }); + + assert_eq!(size, adjusted_size); +}