From 283a7f1c44c4777fd198547ddf406409930800ce Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 18 Oct 2024 16:26:45 -0700 Subject: [PATCH] Fix issues with how we compute DST size 1. Add proper bounds check for `size_of_val` intrinsics. 2. Refactor how we compute size of the object in our mem predicates. 3. Provide user visible methods to try to retrieve the size of the object if known and valid. --- .../codegen/intrinsic.rs | 16 +- .../src/codegen_cprover_gotoc/codegen/typ.rs | 13 +- .../compiler_interface.rs | 9 +- kani-compiler/src/kani_middle/abi.rs | 193 +++++++++ kani-compiler/src/kani_middle/attributes.rs | 31 +- kani-compiler/src/kani_middle/intrinsics.rs | 3 + .../src/kani_middle/kani_functions.rs | 143 ++++++ kani-compiler/src/kani_middle/mod.rs | 7 + .../kani_middle/transform/kani_intrinsics.rs | 409 ++++++++++++++++-- .../src/kani_middle/transform/mod.rs | 9 +- .../kani_middle/transform/rustc_intrinsics.rs | 112 +++++ kani-compiler/src/kani_queries/mod.rs | 31 +- library/kani/src/lib.rs | 1 + library/kani_core/src/lib.rs | 55 ++- library/kani_core/src/mem.rs | 205 +++------ library/kani_core/src/models.rs | 75 ++++ tests/expected/intrinsics/size_of_dst.rs | 54 +++ tests/kani/MemPredicates/adt_with_metadata.rs | 66 +++ .../fixme_unsized_foreign.rs | 19 + .../SizeAndAlignOfDst/fixme_unsized_tuple.rs | 18 + tests/kani/SizeAndAlignOfDst/unsized_tail.rs | 71 +++ 21 files changed, 1334 insertions(+), 206 deletions(-) create mode 100644 kani-compiler/src/kani_middle/abi.rs create mode 100644 kani-compiler/src/kani_middle/kani_functions.rs create mode 100644 kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs create mode 100644 library/kani_core/src/models.rs create mode 100644 tests/expected/intrinsics/size_of_dst.rs create mode 100644 tests/kani/MemPredicates/adt_with_metadata.rs create mode 100644 tests/kani/SizeAndAlignOfDst/fixme_unsized_foreign.rs create mode 100644 tests/kani/SizeAndAlignOfDst/fixme_unsized_tuple.rs create mode 100644 tests/kani/SizeAndAlignOfDst/unsized_tail.rs diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index e8f566dafb15..ef0468cd6cc5 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -215,17 +215,6 @@ impl GotocCtx<'_> { }}; } - macro_rules! codegen_size_align { - ($which: ident) => {{ - let args = instance_args(&instance); - // The type `T` that we'll compute the size or alignment. - let target_ty = args.0[0].expect_ty(); - let arg = fargs.remove(0); - let size_align = self.size_and_align_of_dst(*target_ty, arg); - self.codegen_expr_to_place_stable(place, size_align.$which, loc) - }}; - } - // Most atomic intrinsics do: // 1. Perform an operation on a primary argument (e.g., addition) // 2. Return the previous value of the primary argument @@ -414,7 +403,6 @@ impl GotocCtx<'_> { Intrinsic::MaxNumF32 => codegen_simple_intrinsic!(Fmaxf), Intrinsic::MaxNumF64 => codegen_simple_intrinsic!(Fmax), Intrinsic::MinAlignOf => codegen_intrinsic_const!(), - Intrinsic::MinAlignOfVal => codegen_size_align!(align), Intrinsic::MinNumF32 => codegen_simple_intrinsic!(Fminf), Intrinsic::MinNumF64 => codegen_simple_intrinsic!(Fmin), Intrinsic::MulWithOverflow => { @@ -508,7 +496,6 @@ impl GotocCtx<'_> { loc, ), Intrinsic::SimdXor => codegen_intrinsic_binop!(bitxor), - Intrinsic::SizeOfVal => codegen_size_align!(size), Intrinsic::SqrtF32 => codegen_simple_intrinsic!(Sqrtf), Intrinsic::SqrtF64 => codegen_simple_intrinsic!(Sqrt), Intrinsic::SubWithOverflow => self.codegen_op_with_overflow( @@ -551,6 +538,9 @@ impl GotocCtx<'_> { assert!(self.place_ty_stable(place).kind().is_unit()); self.codegen_write_bytes(fargs, farg_types, loc) } + Intrinsic::SizeOfVal | Intrinsic::MinAlignOfVal => { + unreachable!("Intrinsic `{}` is handled before codegen", intrinsic_str) + } // Unimplemented Intrinsic::Unimplemented { name, issue_link } => { self.codegen_unimplemented_stmt(&name, loc, &issue_link) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index a2e52ac552c6..06233a52b833 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -1571,14 +1571,11 @@ impl<'tcx> GotocCtx<'tcx> { return None; } - let mut typ = struct_type; - while let ty::Adt(adt_def, adt_args) = typ.kind() { - assert_eq!(adt_def.variants().len(), 1, "Expected a single-variant ADT. Found {typ:?}"); - let fields = &adt_def.variants().get(VariantIdx::from_u32(0)).unwrap().fields; - let last_field = fields.last_index().expect("Trait should be the last element."); - typ = fields[last_field].ty(self.tcx, adt_args); - } - if typ.is_trait() { Some(typ) } else { None } + let ty = rustc_internal::stable(struct_type); + rustc_internal::internal( + self.tcx, + crate::kani_middle::abi::LayoutOf::new(ty).unsized_tail(), + ) } /// This function provides an iterator that traverses the data path of a receiver type. I.e.: diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 25bc0cbe8ad1..cef6aa58b9b7 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -244,10 +244,17 @@ impl CodegenBackend for GotocCodegenBackend { let ret_val = rustc_internal::run(tcx, || { super::utils::init(); - // Queries shouldn't change today once codegen starts. + // Any changes to queries from this point on is just related to caching information + // for efficiency purpose that should not outlive the stable-mir `run` scope. let queries = self.queries.lock().unwrap().clone(); + check_target(tcx.sess); check_options(tcx.sess); + if !queries.args().build_std && queries.kani_functions().is_empty() { + tcx.sess.dcx().err( + "Failed to detect Kani functions. Please check your installation is correct.", + ); + } // Codegen all items that need to be processed according to the selected reachability mode: // diff --git a/kani-compiler/src/kani_middle/abi.rs b/kani-compiler/src/kani_middle/abi.rs new file mode 100644 index 000000000000..5196b41eb746 --- /dev/null +++ b/kani-compiler/src/kani_middle/abi.rs @@ -0,0 +1,193 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! This module contains code for handling type abi information. + +use stable_mir::abi::{FieldsShape, LayoutShape}; +use stable_mir::ty::{RigidTy, Ty, TyKind, UintTy}; +use tracing::debug; + +/// A struct to encapsulate the layout information for a given type +#[derive(Clone, Debug, PartialEq, Eq)] +pub struct LayoutOf { + ty: Ty, + layout: LayoutShape, +} + +impl LayoutOf { + /// Create the layout structure for the given type + pub fn new(ty: Ty) -> LayoutOf { + LayoutOf { ty, layout: ty.layout().unwrap().shape() } + } + + /// Return whether the type is sized. + pub fn is_sized(&self) -> bool { + self.layout.is_sized() + } + + /// Return whether the type is unsized and its tail is a foreign item. + /// + /// This will also return `true` if the type is foreign. + pub fn has_foreign_tail(&self) -> bool { + self.unsized_tail() + .map_or(false, |t| matches!(t.kind(), TyKind::RigidTy(RigidTy::Foreign(_)))) + } + + /// Return whether the type is unsized and its tail is a trait object. + pub fn has_trait_tail(&self) -> bool { + self.unsized_tail().map_or(false, |t| t.kind().is_trait()) + } + + /// Return whether the type is unsized and its tail is a slice. + #[allow(dead_code)] + pub fn has_slice_tail(&self) -> bool { + self.unsized_tail().map_or(false, |tail| { + let kind = tail.kind(); + kind.is_slice() | kind.is_str() + }) + } + + /// Return the unsized tail of the type if this is an unsized type. + /// + /// For foreign types, return None. + /// For unsized types, this should return either a slice, a string slice, a dynamic type. + /// For other types, this function will return `None`. + pub fn unsized_tail(&self) -> Option { + if self.layout.is_unsized() { + match self.ty.kind().rigid().unwrap() { + RigidTy::Slice(..) | RigidTy::Dynamic(..) | RigidTy::Str => Some(self.ty), + RigidTy::Adt(..) | RigidTy::Tuple(..) => { + // Recurse the tail field type until we find the unsized tail. + self.last_field_layout().unsized_tail() + } + RigidTy::Foreign(_) => Some(self.ty), + _ => unreachable!("Expected unsized type but found `{}`", self.ty), + } + } else { + None + } + } + + /// Return the type of the elements of the array or slice at the unsized tail of this type. + /// + /// For sized types and trait unsized type, this function will return `None`. + pub fn unsized_tail_elem_ty(&self) -> Option { + self.unsized_tail().and_then(|tail| match tail.kind().rigid().unwrap() { + RigidTy::Slice(elem_ty) => Some(*elem_ty), + // String slices have the same layout as slices of u8. + // https://doc.rust-lang.org/reference/type-layout.html#str-layout + RigidTy::Str => Some(Ty::unsigned_ty(UintTy::U8)), + _ => None, + }) + } + + /// Return the size of the sized portion of this type. + /// + /// For a sized type, this function will return the size of the type. + /// For an unsized type, this function will return the size of the sized portion including + /// any padding bytes that lead to the unsized field. + /// I.e.: the size of the type, excluding the trailing unsized portion. + /// + /// For example, this function will return 2 as the sized portion of `*const (u8, [u16])`: + pub fn size_of_sized_portion(&self) -> usize { + if self.is_sized() { + self.layout.size.bytes() + } else { + match self.ty.kind().rigid().unwrap() { + RigidTy::Slice(_) | RigidTy::Str | RigidTy::Dynamic(..) | RigidTy::Foreign(..) => 0, + RigidTy::Adt(..) | RigidTy::Tuple(..) => { + let fields_sorted = self.layout.fields.fields_by_offset_order(); + let last = *fields_sorted.last().unwrap(); + let FieldsShape::Arbitrary { ref offsets } = self.layout.fields else { + unreachable!() + }; + + // We compute the size of the sized portion by taking the position of the + // last element + the sized portion of that element. + let unsized_offset_unadjusted = offsets[last].bytes(); + debug!(ty=?self.ty, ?unsized_offset_unadjusted, "size_of_sized_portion"); + unsized_offset_unadjusted + self.last_field_layout().size_of_sized_portion() + } + _ => { + unreachable!("Expected sized type, but found: `{}`", self.ty) + } + } + } + } + + /// Return the alignment of the fields that are sized. + /// + /// For a sized type, this function will return the alignment of the type. + /// + /// For an unsized type, this function will return the alignment of the sized portion. + /// The alignment of the type will be the maximum of the alignment of the sized portion + /// and the alignment of the unsized portion. + /// + /// If there's no sized portion, this function will return the minimum alignment (i.e.: 1). + pub fn align_of_sized_portion(&self) -> usize { + if self.is_sized() { + self.layout.abi_align.try_into().unwrap() + } else { + match self.ty.kind().rigid().unwrap() { + RigidTy::Slice(_) | RigidTy::Str | RigidTy::Dynamic(..) | RigidTy::Foreign(..) => 1, + RigidTy::Adt(..) | RigidTy::Tuple(..) => { + // We have to recurse and get the maximum alignment of all sized portions. + let field_layout = self.last_field_layout(); + field_layout + .align_of_sized_portion() + .max(self.layout.abi_align.try_into().unwrap()) + } + _ => { + unreachable!("Expected sized type, but found: `{}`", self.ty); + } + } + } + } + + /// Return the size of the type if it's known at compilation type. + pub fn size_of(&self) -> Option { + if self.is_sized() { Some(self.layout.size.bytes()) } else { None } + } + + /// Return the alignment of the type if it's know at compilation time. + /// + /// The alignment is known at compilation type for sized types and types with slice tail. + /// + /// Note: We assume u64 and usize are the same since Kani is only supported in 64bits machines. + /// Add a configuration in case we ever decide to port this to a 32-bits machine. + #[cfg(target_pointer_width = "64")] + pub fn align_of(&self) -> Option { + if self.is_sized() || self.has_slice_tail() { + self.layout.abi_align.try_into().ok() + } else { + None + } + } + + /// Return the layout of the last field of the type. + /// + /// This function is used to get the layout of the last field of an unsized type. + /// For example, if we have `*const (u8, [u16])`, the last field is `[u16]`. + /// This function will return the layout of `[u16]`. + /// + /// If the type is not a struct, an enum, or a tuple, with at least one field, this function + /// will panic. + fn last_field_layout(&self) -> LayoutOf { + match self.ty.kind().rigid().unwrap() { + RigidTy::Adt(adt_def, adt_args) => { + // We have to recurse and get the maximum alignment of all sized portions. + let fields = adt_def.variants_iter().next().unwrap().fields(); + let fields_sorted = self.layout.fields.fields_by_offset_order(); + let last_field_idx = *fields_sorted.last().unwrap(); + LayoutOf::new(fields[last_field_idx].ty_with_args(adt_args)) + } + RigidTy::Tuple(tys) => { + // We have to recurse and get the maximum alignment of all sized portions. + let last_ty = tys.last().expect("Expected unsized tail"); + LayoutOf::new(*last_ty) + } + _ => { + unreachable!("Expected struct, enum or tuple. Found: `{}`", self.ty); + } + } + } +} diff --git a/kani-compiler/src/kani_middle/attributes.rs b/kani-compiler/src/kani_middle/attributes.rs index 0085928a37d0..a8a51747193d 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -15,17 +15,18 @@ use rustc_middle::ty::{Instance, TyCtxt, TyKind}; use rustc_session::Session; use rustc_smir::rustc_internal; use rustc_span::{Span, Symbol}; +use stable_mir::crate_def::Attribute as AttributeStable; use stable_mir::mir::mono::Instance as InstanceStable; -use stable_mir::{CrateDef, DefId as StableDefId}; +use stable_mir::ty::FnDef; +use stable_mir::{CrateDef, DefId as StableDefId, Symbol as SymbolStable}; use std::str::FromStr; use strum_macros::{AsRefStr, EnumString}; use syn::parse::Parser; use syn::punctuated::Punctuated; -use syn::{PathSegment, TypePath}; - -use tracing::{debug, trace}; +use syn::{Expr, ExprLit, Lit, PathSegment, TypePath}; use super::resolve::{FnResolution, ResolveError, resolve_fn, resolve_fn_path}; +use tracing::{debug, trace}; #[derive(Debug, Clone, Copy, AsRefStr, EnumString, PartialEq, Eq, PartialOrd, Ord)] #[strum(serialize_all = "snake_case")] @@ -1016,6 +1017,12 @@ fn syn_attr(attr: &Attribute) -> syn::Attribute { parser.parse_str(&attr_str).unwrap().pop().unwrap() } +/// Parse a stable attribute using `syn`. +fn syn_attr_stable(attr: &AttributeStable) -> syn::Attribute { + let parser = syn::Attribute::parse_outer; + parser.parse_str(&attr.as_str()).unwrap().pop().unwrap() +} + /// Return a more user-friendly string for path by trying to remove unneeded whitespace. /// /// `quote!()` and `TokenString::to_string()` introduce unnecessary space around separators. @@ -1057,3 +1064,19 @@ fn pretty_type_path(path: &TypePath) -> String { format!("{leading}{}", segments_str(&path.path.segments)) } } + +pub(crate) fn fn_marker(def: FnDef) -> Option { + let fn_marker: [SymbolStable; 2] = ["kanitool".into(), "fn_marker".into()]; + let marker = def.attrs_by_path(&fn_marker).pop()?; + let attribute = syn_attr_stable(&marker); + let meta_name = attribute.meta.require_name_value().unwrap_or_else(|_| { + panic!("Expected name value attribute for `kanitool::fn_marker`, but found: `{:?}`", marker) + }); + let Expr::Lit(ExprLit { lit: Lit::Str(lit_str), .. }) = &meta_name.value else { + panic!( + "Expected string literal for `kanitool::fn_marker`, but found: `{:?}`", + meta_name.value + ); + }; + Some(lit_str.value()) +} 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 new file mode 100644 index 000000000000..f3e2a2748d34 --- /dev/null +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -0,0 +1,143 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +//! This module contains code for handling special functions from the Kani library. +//! +//! There are three types of functions today: +//! 1. Kani intrinsics: These are functions whose body is generated during +//! compilation time. Their body usually require some extra knowledge about the given types +//! that's only available during compilation. +//! 2. Kani models: These are functions that model a specific behavior but that cannot be used +//! directly by the user. For example, retrieving information about memory initialization. +//! Kani compiler determines when and where to use these models, but the logic itself is +//! encoded in Rust. +//! 3. Kani hooks: These are similar to intrinsics in a sense that their encoded body are +//! ignored by the compiler. +//! However, Kani compiler cannot generate their body either, and their call are replaced by +//! calling special APIs from the solver during codegen. +//! +//! Functions #1 and #2 have a `kanitool::fn_marker` attribute attached to them. +//! The marker value will contain "Intrinsic" or "Model" suffix, indicating which category they +//! fit in. +//! +//! The third today is not handled here. They are handled in +//! [crate::codegen_cprover_gotoc::overrides::hooks]. +//! +//! Note that we still need to migrate some of 1 and 2 to this new structure which are currently +//! using rustc's diagnostic infrastructure. + +use crate::kani_middle::attributes; +use stable_mir::ty::FnDef; +use std::collections::HashMap; +use std::str::FromStr; +use strum_macros::{EnumString, IntoStaticStr}; +use tracing::{debug, trace}; + +#[derive(Debug, Copy, Clone, Eq, PartialEq, Hash)] +pub enum KaniFunction { + Model(KaniModel), + Intrinsic(KaniIntrinsic), +} + +/// Kani intrinsics are functions generated by the compiler. +/// +/// These functions usually depend on information that require extra knowledge about the type +/// or extra Kani intrumentation. +#[derive(Debug, Copy, Clone, Eq, PartialEq, IntoStaticStr, EnumString, Hash)] +pub enum KaniIntrinsic { + #[strum(serialize = "ValidValueIntrinsic")] + ValidValue, + #[strum(serialize = "IsInitializedIntrinsic")] + IsInitialized, + #[strum(serialize = "SizeOfSizedIntrinsic")] + SizeOfSized, + #[strum(serialize = "SizeOfUnsizedIntrinsic")] + SizeOfUnsized, + #[strum(serialize = "AlignOfRawIntrinsic")] + AlignOfRaw, + #[strum(serialize = "SafetyCheckIntrinsic")] + SafetyCheck, +} + +/// Kani models are Rust functions that model some runtime behavior used by Kani instrumentation. +#[derive(Debug, Copy, Clone, Eq, PartialEq, IntoStaticStr, EnumString, Hash)] +pub enum KaniModel { + #[strum(serialize = "IsStrPtrInitializedModel")] + IsStrPtrInitialized, + #[strum(serialize = "IsSlicePtrInitializedModel")] + IsSlicePtrInitialized, + #[strum(serialize = "SizeOfDynPortionModel")] + SizeOfDynPortion, + #[strum(serialize = "AlignOfDynPortionModel")] + AlignOfDynPortion, + #[strum(serialize = "SizeOfValRawModel")] + SizeOfVal, + #[strum(serialize = "AlignOfValRawModel")] + AlignOfVal, +} + +impl From for KaniFunction { + fn from(value: KaniIntrinsic) -> Self { + KaniFunction::Intrinsic(value) + } +} + +impl From for KaniFunction { + fn from(value: KaniModel) -> Self { + KaniFunction::Model(value) + } +} + +impl TryFrom for KaniFunction { + type Error = (); + + fn try_from(def: FnDef) -> Result { + let value = attributes::fn_marker(def).ok_or(())?; + if let Ok(intrisic) = KaniIntrinsic::from_str(&value) { + Ok(intrisic.into()) + } else if let Ok(model) = KaniModel::from_str(&value) { + Ok(model.into()) + } else { + Err(()) + } + } +} + +/// Find all Kani functions. +/// +/// First try to find `kani` crate. If that exists, look for the items there. +/// If there's no Kani crate, look for the items in `core` since we could be using `kani_core`. +/// Note that users could have other `kani` crates, so we look in all the ones we find. +/// +/// TODO: We should check if there is no name conflict and that we found all functions. +pub fn find_kani_functions() -> HashMap { + let mut kani = stable_mir::find_crates("kani"); + if kani.is_empty() { + // In case we are using `kani_core`. + kani.extend(stable_mir::find_crates("core")); + } + kani.into_iter() + .find_map(|krate| { + let kani_funcs: HashMap<_, _> = krate + .fn_defs() + .into_iter() + .filter_map(|fn_def| { + trace!(?krate, ?fn_def, "find_kani_functions"); + KaniFunction::try_from(fn_def).ok().map(|kani_function| { + debug!(?kani_function, ?fn_def, "Found kani function"); + (kani_function, fn_def) + }) + }) + .collect(); + // All definitions should live in the same crate, so we can return the first one. + // If there are no definitions, return `None` to indicate that. + (!kani_funcs.is_empty()).then_some(kani_funcs) + }) + .unwrap_or_default() +} + +/// Ensure we have the valid definitions. +pub fn validate_kani_functions(kani_funcs: &HashMap) { + for (kani_function, fn_def) in kani_funcs { + assert_eq!(KaniFunction::try_from(*fn_def), Ok(*kani_function)); + } +} diff --git a/kani-compiler/src/kani_middle/mod.rs b/kani-compiler/src/kani_middle/mod.rs index 5fead860320c..3f4ba4099fad 100644 --- a/kani-compiler/src/kani_middle/mod.rs +++ b/kani-compiler/src/kani_middle/mod.rs @@ -26,11 +26,13 @@ use std::ops::ControlFlow; use self::attributes::KaniAttributes; +pub mod abi; pub mod analysis; pub mod attributes; pub mod codegen_units; pub mod coercion; mod intrinsics; +pub mod kani_functions; pub mod metadata; pub mod points_to; pub mod provide; @@ -119,6 +121,11 @@ pub fn check_reachable_items(tcx: TyCtxt, queries: &QueryDb, items: &[MonoItem]) tcx.dcx().abort_if_errors(); } +/// Check that Kani library is configured correctly. +/// +/// We cache the results for function definitions since it scans all functions defined in the +/// `kani` or `core` library. + /// Structure that represents the source location of a definition. /// TODO: Use `InternedString` once we move it out of the cprover_bindings. /// diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 845916af5181..185e5b813c3b 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -7,14 +7,16 @@ //! information; thus, they are implemented as a transformation pass where their body get generated //! by the transformation. -use crate::args::{Arguments, ExtraChecks}; -use crate::kani_middle::attributes::matches_diagnostic; +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::{ CheckType, InsertPosition, MutableBody, SourceInstruction, }; use crate::kani_middle::transform::check_uninit::PointeeInfo; use crate::kani_middle::transform::check_uninit::{ - PointeeLayout, get_mem_init_fn_def, mk_layout_operand, resolve_mem_init_fn, + PointeeLayout, mk_layout_operand, resolve_mem_init_fn, }; use crate::kani_middle::transform::check_values::{build_limits, ty_validity_per_offset}; use crate::kani_middle::transform::{TransformPass, TransformationType}; @@ -22,24 +24,27 @@ 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, BasicBlockIdx, BinOp, Body, ConstOperand, Local, Mutability, + Operand, Place, ProjectionElem, RETURN_LOCAL, Rvalue, Statement, StatementKind, SwitchTargets, + 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 strum_macros::AsRefStr; -use tracing::trace; +use std::str::FromStr; +use tracing::{debug, trace}; /// Generate the body for a few Kani intrinsics. #[derive(Debug)] pub struct IntrinsicGeneratorPass { - pub check_type: CheckType, - /// Used to cache FnDef lookups of injected memory initialization functions. - pub mem_init_fn_cache: HashMap<&'static str, FnDef>, + check_type: CheckType, + /// Used to cache FnDef lookups for models and Kani intrinsics. + kani_defs: HashMap, /// Used to enable intrinsics depending on the flags passed. - pub arguments: Arguments, + enable_uninit: bool, } impl TransformPass for IntrinsicGeneratorPass { @@ -47,7 +52,7 @@ impl TransformPass for IntrinsicGeneratorPass { where Self: Sized, { - TransformationType::Instrumentation + TransformationType::Stubbing } fn is_enabled(&self, _query_db: &QueryDb) -> bool @@ -61,10 +66,21 @@ impl TransformPass for IntrinsicGeneratorPass { /// 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) { trace!(function=?instance.name(), "transform"); - if matches_diagnostic(tcx, instance.def, Intrinsics::KaniValidValue.as_ref()) { - (true, self.valid_value_body(tcx, body)) - } else if matches_diagnostic(tcx, instance.def, Intrinsics::KaniIsInitialized.as_ref()) { - (true, self.is_initialized_body(tcx, body)) + let attributes = KaniAttributes::for_instance(tcx, instance); + if let Some(kani_intrinsic) = + attributes.fn_marker().and_then(|name| KaniIntrinsic::from_str(name.as_str()).ok()) + { + match kani_intrinsic { + KaniIntrinsic::IsInitialized => (true, self.is_initialized_body(tcx, body)), + KaniIntrinsic::ValidValue => (true, self.valid_value_body(tcx, body)), + KaniIntrinsic::SizeOfSized => (true, self.size_of_sized(body, instance)), + KaniIntrinsic::SizeOfUnsized => (true, self.size_of_unsized(body, instance)), + KaniIntrinsic::AlignOfRaw => (true, self.align_of_raw(body, instance)), + KaniIntrinsic::SafetyCheck => { + /* This is encoded in hooks*/ + (false, body) + } + } } else { (false, body) } @@ -72,6 +88,13 @@ impl TransformPass for IntrinsicGeneratorPass { } impl IntrinsicGeneratorPass { + pub fn new(check_type: CheckType, queries: &QueryDb) -> Self { + let enable_uninit = queries.args().ub_check.contains(&ExtraChecks::Uninit); + let kani_defs = queries.kani_functions().clone(); + debug!(?kani_defs, ?enable_uninit, "IntrinsicGeneratorPass::new"); + IntrinsicGeneratorPass { check_type, enable_uninit, kani_defs } + } + /// Generate the body for valid value. Which should be something like: /// /// ``` @@ -168,7 +191,7 @@ impl IntrinsicGeneratorPass { let mut source = SourceInstruction::Terminator { bb: 0 }; // Short-circut if uninitialized memory checks are not enabled. - if !self.arguments.ub_check.contains(&ExtraChecks::Uninit) { + if !self.enable_uninit { // Initialize return variable with True. let span = new_body.locals()[ret_var].span; let assign = StatementKind::Assign( @@ -222,11 +245,7 @@ impl IntrinsicGeneratorPass { return new_body.into(); } let is_ptr_initialized_instance = resolve_mem_init_fn( - get_mem_init_fn_def( - tcx, - "KaniIsPtrInitialized", - &mut self.mem_init_fn_cache, - ), + *self.kani_defs.get(&KaniIntrinsic::IsInitialized.into()).unwrap(), layout.len(), *pointee_info.ty(), ); @@ -256,17 +275,17 @@ impl IntrinsicGeneratorPass { } PointeeLayout::Slice { element_layout } => { // Since `str`` is a separate type, need to differentiate between [T] and str. - let (slicee_ty, diagnostic) = match pointee_info.ty().kind() { + let (slicee_ty, intrinsic) = match pointee_info.ty().kind() { TyKind::RigidTy(RigidTy::Slice(slicee_ty)) => { - (slicee_ty, "KaniIsSlicePtrInitialized") + (slicee_ty, KaniModel::IsSlicePtrInitialized.into()) } TyKind::RigidTy(RigidTy::Str) => { - (Ty::unsigned_ty(UintTy::U8), "KaniIsStrPtrInitialized") + (Ty::unsigned_ty(UintTy::U8), KaniModel::IsStrPtrInitialized.into()) } _ => unreachable!(), }; let is_ptr_initialized_instance = resolve_mem_init_fn( - get_mem_init_fn_def(tcx, diagnostic, &mut self.mem_init_fn_cache), + *self.kani_defs.get(&intrinsic).unwrap(), element_layout.len(), slicee_ty, ); @@ -362,11 +381,337 @@ impl IntrinsicGeneratorPass { } new_body.into() } + + /// Generate the body for retrieving the size of the unsized portion of a pointed to type. + /// + /// The body generated will depend on the type. + /// + /// For sized type, this will generate: + /// ```mir + /// _0: Option; + /// _1: *const T; + /// bb0: + /// _0 = Some(0); + /// return + /// ``` + /// + /// For types with trait tail, invoke `size_of_dyn_portion`: + /// ``` + /// _0: Option; + /// bb0: + /// _0 = size_of_dyn_portion(_1); + /// return + /// ``` + /// + /// For types where `::Metadata` is `usize` see [Self::size_of_slice_tail]: + fn size_of_unsized(&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, "size_of_unsized"); + + // 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() { + // There is no unsized part. return Some(0); + let val_op = new_body.new_uint_operand(0, 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() { + // Call `size_of_dyn_portion`. + let tail_ty = pointee_layout.unsized_tail().unwrap(); + let mut args = instance.args(); + args.0.push(GenericArgKind::Type(tail_ty)); + let operands = vec![Operand::Copy(Place::from(Local::from(1usize)))]; + self.return_model( + &mut new_body, + &mut source, + KaniModel::SizeOfDynPortion, + &args, + operands, + ); + } else if pointee_layout.has_slice_tail() { + // Size is Some(len x size_of::()) if no overflow happens + self.size_of_slice_tail(&mut new_body, pointee_layout, option_def, option_args); + } 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 `size_of_unsized` when the tail of `T`, i.e.: + /// ```mir + /// _0: Option; + /// _1: *const T; + /// _2: usize; // Number of elements. + /// _4: (usize, bool); + /// bb0: + /// _2 = PtrMetadata(_1); + /// _4 = CheckedMul(_2, ); + /// switchInt(_4.1) -> [0: bb1, otherwise: bb2]; + /// bb1: + /// _0 = Some(*(_4)); + /// goto bb3: + /// bb2: + /// _0 = None; + /// goto bb3: + /// bb3: + /// return + /// ``` + fn size_of_slice_tail( + &self, + new_body: &mut MutableBody, + pointee_layout: LayoutOf, + option_def: AdtDef, + option_args: GenericArgs, + ) { + let mut source = SourceInstruction::Terminator { bb: 0 }; + let span = source.span(new_body.blocks()); + + // Get metadata + let ptr_arg = Operand::Copy(Place::from(1)); + let metadata = new_body.insert_assignment( + Rvalue::UnaryOp(UnOp::PtrMetadata, ptr_arg), + &mut source, + InsertPosition::Before, + ); + + let elem_ty = pointee_layout.unsized_tail_elem_ty().unwrap(); + let elem_layout = LayoutOf::new(elem_ty); + let size_elem = + new_body.new_uint_operand(elem_layout.size_of().unwrap() as u128, UintTy::Usize, span); + + // Calculate size with overflow. + let checked_size = new_body.insert_assignment( + Rvalue::CheckedBinaryOp(BinOp::Mul, Operand::Copy(Place::from(metadata)), size_elem), + &mut source, + InsertPosition::Before, + ); + let overflow = Operand::Copy(Place { + local: checked_size, + projection: vec![ProjectionElem::Field(1, Ty::bool_ty())], + }); + + // Encode `if !overflow` branch + let if_bb: BasicBlockIdx = new_body.blocks().len(); + let else_bb: BasicBlockIdx = if_bb + 1; + let return_bb: BasicBlockIdx = else_bb + 1; + new_body.insert_terminator(&mut source, InsertPosition::Before, Terminator { + kind: TerminatorKind::SwitchInt { + discr: overflow, + targets: SwitchTargets::new(vec![(0, if_bb)], else_bb), + }, + span, + }); + + // Encode if block + let size_op = Operand::Copy(Place { + local: checked_size, + projection: vec![ProjectionElem::Field(0, Ty::usize_ty())], + }); + let size_val = build_some(option_def, option_args.clone(), size_op); + new_body.insert_stmt( + Statement { kind: StatementKind::Assign(Place::from(RETURN_LOCAL), size_val), span }, + &mut source, + InsertPosition::Before, + ); + new_body.insert_terminator(&mut source, InsertPosition::Before, Terminator { + kind: TerminatorKind::Goto { target: return_bb }, + span, + }); + + // Encode else block + let ret_val = build_none(option_def, option_args); + new_body.insert_stmt( + Statement { kind: StatementKind::Assign(Place::from(RETURN_LOCAL), ret_val), span }, + &mut source, + InsertPosition::Before, + ); + new_body.insert_terminator(&mut source, InsertPosition::Before, Terminator { + kind: TerminatorKind::Goto { target: return_bb }, + span, + }); + + assert_eq!(source.bb(), return_bb, "Unexpected return basic block"); + } + + /// Generate the body for retrieving the size of the sized portion of a type. + /// + /// ```ignore + /// _0: usize; + /// _0 = ; + /// return; + /// ``` + fn size_of_sized(&mut self, body: Body, instance: Instance) -> Body { + // Get the size of the sized portion of this type. + let Some(GenericArgKind::Type(ty)) = instance.args().0.first().cloned() else { + unreachable!("Expected target type"); + }; + let layout = LayoutOf::new(ty); + let size = layout.size_of_sized_portion(); + debug!(?ty, ?size, "size_of_sized"); + + // Assign size to the return variable. + 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()); + let size_op = new_body.new_uint_operand(size as u128, UintTy::Usize, span); + let assignment = StatementKind::Assign(Place::from(RETURN_LOCAL), Rvalue::Use(size_op)); + new_body.insert_stmt( + Statement { kind: assignment, span }, + &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; + /// _2: usize; + /// bb0: + /// _1 = ; + /// _0 = align_of_dyn_portion(_2, _1); + /// return + /// ``` + /// + /// For types with foreign tails, this will return `None`. + fn align_of_raw(&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() { + // Call `align_of_dyn_portion`. + let sized_align = pointee_layout.align_of_sized_portion(); + let sized_op = new_body.new_uint_operand(sized_align as _, UintTy::Usize, span); + let tail_ty = pointee_layout.unsized_tail().unwrap(); + let mut args = instance.args(); + args.0.push(GenericArgKind::Type(tail_ty)); + let operands = vec![Operand::Copy(Place::from(Local::from(1usize))), sized_op]; + self.return_model( + &mut new_body, + &mut source, + KaniModel::AlignOfDynPortion, + &args, + operands, + ); + } else { + // Cannot compute size of foreign types. Return None! + assert!(pointee_layout.has_foreign_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)`. +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]) } -#[derive(Debug, Copy, Clone, Eq, PartialEq, AsRefStr)] -#[strum(serialize_all = "PascalCase")] -enum Intrinsics { - KaniValidValue, - KaniIsInitialized, +/// Build an Rvalue `None`. +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/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 3f324d72c39e..6fef3d975d3e 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -33,6 +33,7 @@ use stable_mir::mir::mono::{Instance, MonoItem}; use std::collections::HashMap; use std::fmt::Debug; +use crate::kani_middle::transform::rustc_intrinsics::RustcIntrinsicsPass; pub use internal_mir::RustcInternalMir; pub(crate) mod body; @@ -43,6 +44,7 @@ mod dump_mir_pass; mod internal_mir; mod kani_intrinsics; mod loop_contracts; +mod rustc_intrinsics; mod stubs; /// Object used to retrieve a transformed instance body. @@ -86,11 +88,8 @@ impl BodyTransformation { check_type: CheckType::new_assert(tcx), mem_init_fn_cache: HashMap::new(), }); - transformer.add_pass(queries, IntrinsicGeneratorPass { - check_type, - mem_init_fn_cache: HashMap::new(), - arguments: queries.args().clone(), - }); + transformer.add_pass(queries, IntrinsicGeneratorPass::new(check_type, &queries)); + transformer.add_pass(queries, RustcIntrinsicsPass::new(&queries)); transformer.add_pass(queries, LoopContractPass::new(tcx, &unit)); transformer } diff --git a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs new file mode 100644 index 000000000000..4b304dca0463 --- /dev/null +++ b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs @@ -0,0 +1,112 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Module responsible for implementing a few Rust compiler intrinsics. +//! +//! Note that some rustc intrinsics are lowered to MIR instructions. Those can also be handled +//! here. + +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::{TransformPass, TransformationType}; +use crate::kani_queries::QueryDb; +use rustc_middle::ty::TyCtxt; +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 std::collections::HashMap; +use tracing::debug; + +/// Generate the body for a few Kani intrinsics. +#[derive(Debug)] +pub struct RustcIntrinsicsPass { + /// Used to cache FnDef lookups for intrinsics models. + models: HashMap, +} + +impl TransformPass for RustcIntrinsicsPass { + fn transformation_type() -> TransformationType + where + Self: Sized, + { + TransformationType::Stubbing + } + + fn is_enabled(&self, _query_db: &QueryDb) -> bool + where + Self: Sized, + { + true + } + + /// 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) { + debug!(function=?instance.name(), "transform"); + let mut new_body = MutableBody::from(body); + let mut visitor = ReplaceIntrinsicVisitor::new(&self.models, new_body.locals().to_vec()); + visitor.visit_body(&mut new_body); + (visitor.changed, new_body.into()) + } +} + +impl RustcIntrinsicsPass { + pub fn new(queries: &QueryDb) -> Self { + let models = queries + .kani_functions() + .iter() + .filter_map(|(func, def)| { + if let KaniFunction::Model(model) = func { Some((*model, *def)) } else { None } + }) + .collect(); + debug!(?models, "RustcIntrinsicsPass::new"); + RustcIntrinsicsPass { models } + } +} + +struct ReplaceIntrinsicVisitor<'a> { + models: &'a HashMap, + locals: Vec, + changed: bool, +} + +impl<'a> ReplaceIntrinsicVisitor<'a> { + fn new(models: &'a HashMap, locals: Vec) -> Self { + ReplaceIntrinsicVisitor { models, locals, changed: false } + } +} + +impl<'a> MutMirVisitor for ReplaceIntrinsicVisitor<'a> { + /// Replace the terminator for some intrinsics. + /// + /// Note that intrinsics must always be called directly. + fn visit_terminator(&mut self, term: &mut Terminator) { + if let TerminatorKind::Call { func, .. } = &mut term.kind { + if let TyKind::RigidTy(RigidTy::FnDef(def, args)) = + func.ty(&self.locals).unwrap().kind() + { + if def.is_intrinsic() { + let instance = Instance::resolve(def, &args).unwrap(); + let intrinsic = Intrinsic::from_instance(&instance); + debug!(?intrinsic, "handle_terminator"); + let model = match intrinsic { + Intrinsic::SizeOfVal => self.models[&KaniModel::SizeOfVal], + Intrinsic::MinAlignOfVal => self.models[&KaniModel::AlignOfVal], + // The rest is handled in hooks. + _ => { + return self.super_terminator(term); + } + }; + let new_instance = Instance::resolve(model, &args).unwrap(); + let literal = MirConst::try_new_zero_sized(new_instance.ty()).unwrap(); + let span = term.span; + let new_func = ConstOperand { span, user_ty: None, const_: literal }; + *func = Operand::Constant(new_func); + self.changed = true; + } + } + } + self.super_terminator(term); + } +} diff --git a/kani-compiler/src/kani_queries/mod.rs b/kani-compiler/src/kani_queries/mod.rs index bb28237248d3..83b636caacf1 100644 --- a/kani-compiler/src/kani_queries/mod.rs +++ b/kani-compiler/src/kani_queries/mod.rs @@ -2,9 +2,14 @@ // SPDX-License-Identifier: Apache-2.0 OR MIT //! Define the communication between KaniCompiler and the codegen implementation. -use std::sync::{Arc, Mutex}; - use crate::args::Arguments; +use crate::kani_middle::kani_functions::{ + KaniFunction, find_kani_functions, validate_kani_functions, +}; +use stable_mir::ty::FnDef; +use std::cell::OnceCell; +use std::collections::HashMap; +use std::sync::{Arc, Mutex}; /// This structure should only be used behind a synchronized reference or a snapshot. /// @@ -12,6 +17,7 @@ use crate::args::Arguments; #[derive(Debug, Default, Clone)] pub struct QueryDb { args: Option, + kani_functions: OnceCell>, } impl QueryDb { @@ -26,4 +32,25 @@ impl QueryDb { pub fn args(&self) -> &Arguments { self.args.as_ref().expect("Arguments have not been initialized") } + + /// Return a map with model and intrinsic functions defined in Kani's library. + /// + /// For `kani_core`, those definitions live in the `core` library. + /// + /// We cache these definitions to avoid doing the lookup every time it is needed. + /// The cache should be invalidated if the `stable_mir` context changes. + /// Since that doesn't occur today, we just run a sanity check to ensure all definitions + /// are still correct, and abort otherwise. + pub fn kani_functions(&self) -> &HashMap { + if let Some(kani_functions) = self.kani_functions.get() { + // Sanity check the values stored in case someone misused this API. + validate_kani_functions(kani_functions); + kani_functions + } else { + self.kani_functions.get_or_init(|| { + // Find all kani functions + find_kani_functions() + }) + } + } } diff --git a/library/kani/src/lib.rs b/library/kani/src/lib.rs index ce1eeb992121..94c805a7758a 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 ee0092554e56..e579542fe08d 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!(); kani_core::check_intrinsic!(); pub mod mem { @@ -58,7 +60,7 @@ macro_rules! kani_lib { pub use kani_core::*; kani_core::kani_intrinsics!(std); kani_core::generate_arbitrary!(std); - + kani_core::generate_models!(); kani_core::check_intrinsic! { msg="This API will be made private in future releases.", vis=pub } @@ -289,6 +291,57 @@ macro_rules! kani_intrinsics { panic!("{}", message) } + /// Retrieve the size of the sized part of the value pointed by `ptr`. + /// + /// If `T` is sized, return `size_of::()`. + /// For an unsized type, this function will return the size of the sized portion including + /// any padding bytes that lead to the unsized field. + /// I.e.: the size of the type, excluding the trailing unsized portion. + /// + /// For example, this function will return 2 as the sized portion of `*const (u8, [u16])`: + #[allow(dead_code)] + #[kanitool::fn_marker = "SizeOfSizedIntrinsic"] + #[inline(never)] + pub(crate) fn size_of_sized_portion() -> usize { + kani_intrinsic() + } + + /// Retrieve the size of the unsized part of the value pointed by `ptr`. + /// + /// If `T` is unsized, return the size of the unsized portion, if that can be safely + /// computed. Foreign types and slices that overflow will return `None`. + /// + /// For sized types, this function will return Some(0). + #[allow(dead_code)] + #[kanitool::fn_marker = "SizeOfUnsizedIntrinsic"] + #[inline(never)] + pub(crate) fn size_of_unsized_portion(_ptr: *const T) -> Option { + kani_intrinsic() + } + + /// Retrieve the alignment of raw pointer if it can be computed. + /// + /// This will return `None` if the type is foreign or contain a foreign element. + /// Note that alignment value may be incorrect. + #[allow(dead_code)] + #[kanitool::fn_marker = "AlignOfRawIntrinsic"] + #[inline(never)] + pub(crate) fn align_of_raw(_ptr: *const T) -> Option { + kani_intrinsic() + } + + #[doc(hidden)] + #[allow(dead_code)] + #[kanitool::fn_marker = "SafetyCheckIntrinsic"] + #[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 c8501e977096..4b5b13fddcd9 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,54 @@ 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 safe. + /// + /// Return `None` if an overflow would occur, or if alignment is not power of two. + /// TODO: Optimize this if T is sized. + pub fn checked_size_of_raw(ptr: *const T) -> Option { + #[cfg(not(feature = "concrete_playback"))] + { + let size_of_unsized = crate::kani::size_of_unsized_portion(ptr)?; + let sum = size_of_unsized.checked_add(crate::kani::size_of_sized_portion::())?; + let align = checked_align_of_raw(ptr)?; + // Size must be multiple of alignment. + // Since alignment is power-of-two, we can compute as (size + (align - 1)) & -align + return Some((sum.checked_add(align - 1))? & align.wrapping_neg()); + } + + #[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. + pub fn checked_align_of_raw(ptr: *const T) -> Option { + crate::kani::align_of_raw(ptr) + .and_then(|align| align.is_power_of_two().then_some(align)) + } + + /// 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 +208,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 } } @@ -312,14 +242,14 @@ macro_rules! kani_mem { /// # Safety /// /// - Users have to ensure that the pointer is aligned the pointed memory is allocated. - #[rustc_diagnostic_item = "KaniValidValue"] + #[kanitool::fn_marker = "ValidValueIntrinsic"] #[inline(never)] unsafe fn has_valid_value(_ptr: *const T) -> bool { kani_intrinsic() } /// Check whether `len * size_of::()` bytes are initialized starting from `ptr`. - #[rustc_diagnostic_item = "KaniIsInitialized"] + #[kanitool::fn_marker = "IsInitializedIntrinsic"] #[inline(never)] pub(crate) fn is_initialized(_ptr: *const T) -> bool { kani_intrinsic() @@ -363,14 +293,9 @@ macro_rules! kani_mem { /// Get the object offset of the given pointer. #[doc(hidden)] - #[crate::kani::unstable_feature( - feature = "ghost-state", - issue = 3184, - reason = "experimental ghost state/shadow memory API" - )] #[rustc_diagnostic_item = "KaniPointerOffset"] #[inline(never)] - pub fn pointer_offset(_ptr: *const T) -> usize { + pub(crate) fn pointer_offset(_ptr: *const T) -> usize { kani_intrinsic() } }; diff --git a/library/kani_core/src/models.rs b/library/kani_core/src/models.rs new file mode 100644 index 000000000000..1ace949c5132 --- /dev/null +++ b/library/kani_core/src/models.rs @@ -0,0 +1,75 @@ +// 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; thus, we keep them separate from stubs. +//! TODO: Move SIMD model here. + +#[macro_export] +#[allow(clippy::crate_in_macro_def)] +macro_rules! generate_models { + () => { + /// Model rustc intrinsics. These definitions are not visible to the crate user. + /// They are used by Kani's compiler. + #[allow(dead_code)] + mod rustc_intrinsics { + use crate::kani; + #[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) { + size + } else { + kani::safety_check(false, "failed to compute size of val"); + // Unreachable without panic. + kani::kani_intrinsic() + } + } + + #[kanitool::fn_marker = "AlignOfValRawModel"] + pub fn align_of_val_raw(ptr: *const T) -> usize { + if let Some(size) = kani::mem::checked_align_of_raw(ptr) { + size + } else { + kani::safety_check(false, "failed to compute align of val"); + // Unreachable without panic. + kani::kani_intrinsic() + } + } + } + + #[allow(dead_code)] + mod mem_models { + use core::ptr::{self, DynMetadata, Pointee}; + + /// Retrieve the size of the object stored in the vtable. + /// + /// This model is used to implement `size_of_unsized_portion` intrinsic. + /// + /// For that, `U` is a trait, and `T` is either equal to `U` or has a tail `U`. + #[kanitool::fn_marker = "SizeOfDynPortionModel"] + pub(crate) fn size_of_dyn_portion(ptr: *const T) -> Option + where + T: ?Sized + Pointee>, + { + Some(ptr::metadata(ptr).size_of()) + } + + /// Retrieve the alignment of the object stored in the vtable. + /// + /// This model is used to implement `align_of_raw` intrinsic. + /// + /// For that, `U` is a trait, and `T` is either equal to `U` or has a tail `U`. + #[kanitool::fn_marker = "AlignOfDynPortionModel"] + pub(crate) fn align_of_dyn_portion( + ptr: *const T, + sized_portion: usize, + ) -> Option + where + T: ?Sized + Pointee>, + { + Some(ptr::metadata(ptr).align_of().max(sized_portion)) + } + } + }; +} diff --git a/tests/expected/intrinsics/size_of_dst.rs b/tests/expected/intrinsics/size_of_dst.rs new file mode 100644 index 000000000000..6576fdea0450 --- /dev/null +++ b/tests/expected/intrinsics/size_of_dst.rs @@ -0,0 +1,54 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test case checks the behavior of `size_of_val_raw` for dynamically sized types. + +#![feature(layout_for_ptr)] +#![feature(ptr_metadata)] + +use std::mem::size_of_val_raw; +use std::ptr; + +#[derive(Clone, Copy, kani::Arbitrary)] +struct Wrapper { + _size: usize, + _value: T, +} + +#[cfg(ice)] +#[kani::proof] +pub fn check_size_of_adt_overflows() { + let var: Wrapper<[u64; 4]> = kani::any(); + let fat_ptr: *const Wrapper<[u64]> = &var as *const _; + 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); + #[cfg(blah)] + if let Some(slice_size) = new_size.checked_mul(size_of::()) { + if let Some(expected_size) = slice_size.checked_add(size_of::()) { + assert_eq!(unsafe { size_of_val_raw(new_ptr) }, expected_size); + } else { + // Expect UB detection + let _should_ub = unsafe { size_of_val_raw(new_ptr) }; + } + } else { + // Expect UB detection + let _should_ub = unsafe { size_of_val_raw(new_ptr) }; + } +} + +#[kani::proof] +pub fn check_size_of_overflows() { + let var: [u64; 4] = kani::any(); + let fat_ptr: *const [u64] = &var as *const _; + let (thin_ptr, size) = fat_ptr.to_raw_parts(); + let new_size: usize = kani::any(); + let new_ptr: *const [u64] = ptr::from_raw_parts(thin_ptr, new_size); + #[cfg(blah)] + if let Some(expected_size) = new_size.checked_mul(size_of::()) { + assert_eq!(unsafe { size_of_val_raw(new_ptr) }, expected_size); + } else { + // Expect UB detection + let _should_ub = unsafe { size_of_val_raw(new_ptr) }; + } +} diff --git a/tests/kani/MemPredicates/adt_with_metadata.rs b/tests/kani/MemPredicates/adt_with_metadata.rs new file mode 100644 index 000000000000..d5747a00c04d --- /dev/null +++ b/tests/kani/MemPredicates/adt_with_metadata.rs @@ -0,0 +1,66 @@ +// 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. +#![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::*; + #[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)); + } +} + +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)); + } + + #[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)); + } + } + + #[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)); + } +} diff --git a/tests/kani/SizeAndAlignOfDst/fixme_unsized_foreign.rs b/tests/kani/SizeAndAlignOfDst/fixme_unsized_foreign.rs new file mode 100644 index 000000000000..1bb639b7575f --- /dev/null +++ b/tests/kani/SizeAndAlignOfDst/fixme_unsized_foreign.rs @@ -0,0 +1,19 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT +// +//! Ensure we compute fail verification if user tries to compute the size of a foreign item. + +#![feature(extern_types, layout_for_ptr)] + +extern "C" { + type ExternalType; +} + +#[kani::proof] +#[kani::should_panic] +fn check_adjusted_tup_size() { + let tup: (u32, usize) = kani::any(); + let ptr: *const (u32, ExternalType) = &tup as *const _ as *const _; + let size = unsafe { std::mem::size_of_val_raw(ptr) }; + assert_eq!(size, 4); +} diff --git a/tests/kani/SizeAndAlignOfDst/fixme_unsized_tuple.rs b/tests/kani/SizeAndAlignOfDst/fixme_unsized_tuple.rs new file mode 100644 index 000000000000..0edae52aa0ac --- /dev/null +++ b/tests/kani/SizeAndAlignOfDst/fixme_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); +} diff --git a/tests/kani/SizeAndAlignOfDst/unsized_tail.rs b/tests/kani/SizeAndAlignOfDst/unsized_tail.rs new file mode 100644 index 000000000000..095e9e1d4cbf --- /dev/null +++ b/tests/kani/SizeAndAlignOfDst/unsized_tail.rs @@ -0,0 +1,71 @@ +// 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; + +#[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_tail() { + let align_sized = checked_align_of_raw(&Pair(0u8, 19i32)); + assert_eq!(align_sized, Some(4)); + + let align_dyn = checked_align_of_raw(&Pair(10u8, [1i32; 10]) as &Pair); + assert_eq!(align_dyn, Some(4)); +}