From 19adf79fccb4868f6854313e7589ea55813265f2 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 22 Nov 2024 13:00:37 -0800 Subject: [PATCH] Fix issues with how we compute DST size (#3687) This change fixes how we compute size of the object in our mem predicates, and provide user visible methods to try to retrieve the size of the object if known and valid (`checked_size_of_raw` and `checked_align_of_raw`. Fixes #3612 Fixes #3627 ## Call-outs To simplify this PR, I moved the following changes to their own PRs: 1. #3644 2. #3718 I also removed the fix for the intrinsics `size_of_val` and `align_of_val` from this PR, and I will create a follow up PR once this one is merged. --------- Co-authored-by: Carolyn Zech --- .../codegen_cprover_gotoc/codegen/place.rs | 2 +- .../codegen_cprover_gotoc/overrides/hooks.rs | 36 ++- kani-compiler/src/kani_middle/abi.rs | 1 - kani-compiler/src/kani_middle/intrinsics.rs | 3 + .../src/kani_middle/kani_functions.rs | 12 + .../kani_middle/transform/kani_intrinsics.rs | 262 +++++++++++++++++- library/kani/src/lib.rs | 1 + library/kani_core/src/lib.rs | 15 + library/kani_core/src/mem.rs | 197 +++++-------- library/kani_core/src/models.rs | 120 ++++++++ tests/kani/MemPredicates/adt_with_metadata.rs | 72 +++++ tests/kani/MemPredicates/foreign_type.rs | 77 +++++ .../fixme_unsized_foreign.rs | 48 ++++ tests/kani/SizeAndAlignOfDst/unsized_tail.rs | 115 ++++++++ tests/kani/SizeAndAlignOfDst/unsized_tuple.rs | 18 ++ 15 files changed, 840 insertions(+), 139 deletions(-) create mode 100644 library/kani_core/src/models.rs create mode 100644 tests/kani/MemPredicates/adt_with_metadata.rs create mode 100644 tests/kani/MemPredicates/foreign_type.rs create mode 100644 tests/kani/SizeAndAlignOfDst/fixme_unsized_foreign.rs create mode 100644 tests/kani/SizeAndAlignOfDst/unsized_tail.rs create mode 100644 tests/kani/SizeAndAlignOfDst/unsized_tuple.rs 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); +}