From 283a7f1c44c4777fd198547ddf406409930800ce Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 18 Oct 2024 16:26:45 -0700 Subject: [PATCH 1/9] 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)); +} From 24992d3243d4dbc9efc91c2320d7bfe3b15fc9bd Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Tue, 12 Nov 2024 16:09:06 -0800 Subject: [PATCH 2/9] Fix aggregate, place handle and implement safety_check --- .../codegen_cprover_gotoc/codegen/place.rs | 2 +- .../codegen_cprover_gotoc/codegen/rvalue.rs | 36 +++++++---- .../codegen_cprover_gotoc/overrides/hooks.rs | 33 ++++++++++ kani-compiler/src/kani_middle/abi.rs | 10 +-- kani-compiler/src/kani_middle/attributes.rs | 3 +- .../src/kani_middle/kani_functions.rs | 29 +++++++-- tests/kani/MemPredicates/adt_with_metadata.rs | 25 +++++--- tests/kani/MemPredicates/foreign_type.rs | 64 +++++++++++++++++++ tests/kani/SizeAndAlignOfDst/unsized_tuple.rs | 18 ++++++ 9 files changed, 184 insertions(+), 36 deletions(-) create mode 100644 tests/kani/MemPredicates/foreign_type.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/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs index 7f578940d98e..c5f2f9fd2c08 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs @@ -6,6 +6,7 @@ use crate::codegen_cprover_gotoc::codegen::place::ProjectedPlace; use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable; use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr}; use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx}; +use crate::kani_middle::abi::LayoutOf; use crate::kani_middle::coercion::{ CoerceUnsizedInfo, CoerceUnsizedIterator, CoercionBaseStable, extract_unsize_casting_stable, }; @@ -710,21 +711,32 @@ impl GotocCtx<'_> { slice_fat_ptr(typ, data_cast, meta, &self.symbol_table) } TyKind::RigidTy(RigidTy::Adt(..)) => { + let layout = LayoutOf::new(pointee_ty); let pointee_goto_typ = self.codegen_ty_stable(pointee_ty); let data_cast = data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) }); - let meta = self.codegen_operand_stable(&operands[1]); - if meta.typ().sizeof(&self.symbol_table) == 0 { - data_cast - } else { - let vtable_expr = meta - .member("_vtable_ptr", &self.symbol_table) - .member("pointer", &self.symbol_table) - .cast_to( - typ.lookup_field_type("vtable", &self.symbol_table).unwrap(), - ); - dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table) - } + layout.unsized_tail().map_or(data_cast.clone(), |tail| { + let meta = self.codegen_operand_stable(&operands[1]); + match tail.kind().rigid().unwrap() { + RigidTy::Foreign(..) => data_cast, + RigidTy::Slice(..) | RigidTy::Str => { + slice_fat_ptr(typ, data_cast, meta, &self.symbol_table) + } + RigidTy::Dynamic(..) => { + let vtable_expr = meta + .member("_vtable_ptr", &self.symbol_table) + .member("pointer", &self.symbol_table) + .cast_to( + typ.lookup_field_type("vtable", &self.symbol_table) + .unwrap(), + ); + dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table) + } + _ => { + unreachable!("Unexpected unsized tail: {tail:?}"); + } + } + }) } TyKind::RigidTy(RigidTy::Dynamic(..)) => { let pointee_goto_typ = self.codegen_ty_stable(pointee_ty); diff --git a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs index 74c39c45ed74..7a33408ef129 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs @@ -12,6 +12,7 @@ use crate::codegen_cprover_gotoc::GotocCtx; use crate::codegen_cprover_gotoc::codegen::{PropertyClass, bb_label}; use crate::kani_middle::attributes::KaniAttributes; use crate::kani_middle::attributes::matches_diagnostic as matches_function; +use crate::kani_middle::kani_functions::{KaniFunction, KaniIntrinsic}; use crate::unwrap_or_return_codegen_unimplemented_stmt; use cbmc::goto_program::CIntType; use cbmc::goto_program::{BuiltinFn, Expr, Stmt, Type}; @@ -146,6 +147,37 @@ impl GotocHook for Assert { } } +struct SafetyCheck; +impl GotocHook for SafetyCheck { + fn hook_applies(&self, _tcx: TyCtxt, instance: Instance) -> bool { + KaniFunction::try_from(instance) == Ok(KaniFunction::Intrinsic(KaniIntrinsic::SafetyCheck)) + } + + 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 { @@ -623,6 +655,7 @@ pub fn fn_hooks() -> GotocHooks { Rc::new(Assume), Rc::new(Assert), Rc::new(Check), + Rc::new(SafetyCheck), Rc::new(Cover), Rc::new(Nondet), Rc::new(IsAllocated), diff --git a/kani-compiler/src/kani_middle/abi.rs b/kani-compiler/src/kani_middle/abi.rs index 5196b41eb746..dc8a32e243bf 100644 --- a/kani-compiler/src/kani_middle/abi.rs +++ b/kani-compiler/src/kani_middle/abi.rs @@ -174,16 +174,18 @@ impl LayoutOf { 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) + // For tuples, the unsized field is currently the last declared. + // To be on the safe side, we still get the sorted list by offset order. + let fields_sorted = self.layout.fields.fields_by_offset_order(); + let last_field_idx = *fields_sorted.last().unwrap(); + let last_ty = tys[last_field_idx]; + 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 19db20e04a3c..10d2c227240f 100644 --- a/kani-compiler/src/kani_middle/attributes.rs +++ b/kani-compiler/src/kani_middle/attributes.rs @@ -17,7 +17,6 @@ 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::ty::FnDef; use stable_mir::{CrateDef, DefId as StableDefId, Symbol as SymbolStable}; use std::str::FromStr; use strum_macros::{AsRefStr, EnumString}; @@ -1079,7 +1078,7 @@ fn pretty_type_path(path: &TypePath) -> String { } } -pub(crate) fn fn_marker(def: FnDef) -> Option { +pub(crate) fn fn_marker(def: T) -> 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); diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index f3e2a2748d34..8c816b5c9e0f 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -10,22 +10,22 @@ //! 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. +//! 3. Kani hooks: These are similar to Kani intrinsics but their code generation depends +//! on some backend specific logic. From a Kani library perspective, there is no difference +//! between hooks and intrinsics. This is a compiler implementation detail. //! //! 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]. +//! We are transitioning the third category. It mostly uses rustc diagnostics. See how 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::mir::mono::Instance; use stable_mir::ty::FnDef; use std::collections::HashMap; use std::str::FromStr; @@ -41,7 +41,7 @@ pub enum KaniFunction { /// 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. +/// or extra Kani instrumentation. #[derive(Debug, Copy, Clone, Eq, PartialEq, IntoStaticStr, EnumString, Hash)] pub enum KaniIntrinsic { #[strum(serialize = "ValidValueIntrinsic")] @@ -102,6 +102,21 @@ impl TryFrom for KaniFunction { } } +impl TryFrom for KaniFunction { + type Error = (); + + fn try_from(instance: Instance) -> Result { + let value = attributes::fn_marker(instance.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. diff --git a/tests/kani/MemPredicates/adt_with_metadata.rs b/tests/kani/MemPredicates/adt_with_metadata.rs index d5747a00c04d..0bae910ef1cb 100644 --- a/tests/kani/MemPredicates/adt_with_metadata.rs +++ b/tests/kani/MemPredicates/adt_with_metadata.rs @@ -16,12 +16,25 @@ struct Wrapper { 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 { @@ -40,6 +53,8 @@ mod invalid_access { 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(); @@ -53,14 +68,4 @@ mod invalid_access { 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/MemPredicates/foreign_type.rs b/tests/kani/MemPredicates/foreign_type.rs new file mode 100644 index 000000000000..55bec34bc2c3 --- /dev/null +++ b/tests/kani/MemPredicates/foreign_type.rs @@ -0,0 +1,64 @@ +// 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 fat_ptr: *mut Wrapper = &mut var as *mut _ as *mut _; + assert!(!can_write(fat_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] +#[kani::should_panic] +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); + }; + 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/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); +} From e06eef54a323829322b12a87faa93305d2a66823 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 13 Nov 2024 12:50:45 -0800 Subject: [PATCH 3/9] Cleanup code and add more tests - Assume for now that we cannot compute foreign object size. --- kani-compiler/src/kani_middle/abi.rs | 12 +- .../src/kani_middle/kani_functions.rs | 20 +- .../kani_middle/transform/kani_intrinsics.rs | 240 ++++++------------ library/kani_core/src/lib.rs | 39 --- library/kani_core/src/mem.rs | 23 +- library/kani_core/src/models.rs | 81 +++++- .../size_and_align/unsized_foreign.rs | 41 +++ tests/kani/MemPredicates/adt_with_metadata.rs | 1 + tests/kani/MemPredicates/foreign_type.rs | 4 +- .../fixme_unsized_foreign.rs | 19 -- .../SizeAndAlignOfDst/fixme_unsized_tuple.rs | 18 -- tests/kani/SizeAndAlignOfDst/unsized_tail.rs | 54 +++- 12 files changed, 263 insertions(+), 289 deletions(-) create mode 100644 tests/expected/size_and_align/unsized_foreign.rs delete mode 100644 tests/kani/SizeAndAlignOfDst/fixme_unsized_foreign.rs delete mode 100644 tests/kani/SizeAndAlignOfDst/fixme_unsized_tuple.rs diff --git a/kani-compiler/src/kani_middle/abi.rs b/kani-compiler/src/kani_middle/abi.rs index dc8a32e243bf..55cc8a9b9807 100644 --- a/kani-compiler/src/kani_middle/abi.rs +++ b/kani-compiler/src/kani_middle/abi.rs @@ -88,7 +88,7 @@ impl LayoutOf { /// 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 { + pub fn size_of_head(&self) -> usize { if self.is_sized() { self.layout.size.bytes() } else { @@ -105,7 +105,7 @@ impl LayoutOf { // 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() + unsized_offset_unadjusted + self.last_field_layout().size_of_head() } _ => { unreachable!("Expected sized type, but found: `{}`", self.ty) @@ -114,7 +114,7 @@ impl LayoutOf { } } - /// Return the alignment of the fields that are sized. + /// Return the alignment of the fields that are sized from the head of the object. /// /// For a sized type, this function will return the alignment of the type. /// @@ -123,7 +123,7 @@ impl LayoutOf { /// 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 { + pub fn align_of_head(&self) -> usize { if self.is_sized() { self.layout.abi_align.try_into().unwrap() } else { @@ -132,9 +132,7 @@ impl LayoutOf { 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()) + field_layout.align_of_head().max(self.layout.abi_align.try_into().unwrap()) } _ => { unreachable!("Expected sized type, but found: `{}`", self.ty); diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 8c816b5c9e0f..cd0f07802f7e 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -48,12 +48,10 @@ pub enum KaniIntrinsic { ValidValue, #[strum(serialize = "IsInitializedIntrinsic")] IsInitialized, - #[strum(serialize = "SizeOfSizedIntrinsic")] - SizeOfSized, - #[strum(serialize = "SizeOfUnsizedIntrinsic")] - SizeOfUnsized, - #[strum(serialize = "AlignOfRawIntrinsic")] - AlignOfRaw, + #[strum(serialize = "CheckedAlignOfIntrinsic")] + CheckedAlignOf, + #[strum(serialize = "CheckedSizeOfIntrinsic")] + CheckedSizeOf, #[strum(serialize = "SafetyCheckIntrinsic")] SafetyCheck, } @@ -65,14 +63,16 @@ pub enum KaniModel { IsStrPtrInitialized, #[strum(serialize = "IsSlicePtrInitializedModel")] IsSlicePtrInitialized, - #[strum(serialize = "SizeOfDynPortionModel")] - SizeOfDynPortion, - #[strum(serialize = "AlignOfDynPortionModel")] - AlignOfDynPortion, #[strum(serialize = "SizeOfValRawModel")] SizeOfVal, #[strum(serialize = "AlignOfValRawModel")] AlignOfVal, + #[strum(serialize = "SizeOfDynObjectModel")] + SizeOfDynObject, + #[strum(serialize = "AlignOfDynObjectModel")] + AlignOfDynObject, + #[strum(serialize = "SizeOfSliceObjectModel")] + SizeOfSliceObject, } impl From for KaniFunction { diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 185e5b813c3b..492a61e79e0e 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -24,9 +24,8 @@ use crate::kani_queries::QueryDb; use rustc_middle::ty::TyCtxt; use stable_mir::mir::mono::Instance; use stable_mir::mir::{ - AggregateKind, BasicBlock, BasicBlockIdx, BinOp, Body, ConstOperand, Local, Mutability, - Operand, Place, ProjectionElem, RETURN_LOCAL, Rvalue, Statement, StatementKind, SwitchTargets, - Terminator, TerminatorKind, UnOp, 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::{ @@ -73,9 +72,8 @@ impl TransformPass for IntrinsicGeneratorPass { 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::CheckedAlignOf => (true, self.checked_align_of(body, instance)), + KaniIntrinsic::CheckedSizeOf => (true, self.checked_size_of(body, instance)), KaniIntrinsic::SafetyCheck => { /* This is encoded in hooks*/ (false, body) @@ -382,29 +380,32 @@ impl IntrinsicGeneratorPass { new_body.into() } - /// Generate the body for retrieving the size of the unsized portion of a pointed to type. + /// Generate the body for retrieving the size of a val starting from its raw pointer. /// - /// The body generated will depend on the type. + /// 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(0); + /// _0 = Some(); /// return /// ``` /// - /// For types with trait tail, invoke `size_of_dyn_portion`: + /// 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_portion(_1); + /// _0 = size_of_dyn_object(_1, , ); + /// bb1: /// return /// ``` - /// - /// For types where `::Metadata` is `usize` see [Self::size_of_slice_tail]: - fn size_of_unsized(&mut self, body: Body, instance: Instance) -> Body { + 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; @@ -412,9 +413,9 @@ impl IntrinsicGeneratorPass { unreachable!("Expected a pointer argument,but got {ptr_ty}") }; let pointee_layout = LayoutOf::new(pointee_ty); - debug!(?ptr_ty, ?pointee_layout, "size_of_unsized"); + debug!(?ptr_ty, ?pointee_layout, "checked_size_of"); - // Get information about the return value (Option). + // 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}`") @@ -426,8 +427,12 @@ impl IntrinsicGeneratorPass { 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); + // 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), @@ -436,23 +441,55 @@ impl IntrinsicGeneratorPass { InsertPosition::Before, ); } else if pointee_layout.has_trait_tail() { - // Call `size_of_dyn_portion`. + // Return `size_of_dyn_object::(ptr, head_size, head_align)`. 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)))]; + 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::SizeOfDynPortion, - &args, + KaniModel::SizeOfDynObject, + &instance_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); + // 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! + // Cannot compute size of foreign types. Return `None`. assert!( pointee_layout.has_foreign_tail(), "Expected foreign, but found `{:?}` tail instead.", @@ -469,133 +506,6 @@ impl IntrinsicGeneratorPass { 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. @@ -613,15 +523,15 @@ impl IntrinsicGeneratorPass { /// For types with trait tail, invoke `align_of_dyn_portion`: /// ``` /// _0: Option; - /// _2: usize; + /// _1: *const T; /// bb0: - /// _1 = ; - /// _0 = align_of_dyn_portion(_2, _1); + /// _0 = align_of_dyn_object(_1, ); + /// bb1: /// return /// ``` /// /// For types with foreign tails, this will return `None`. - fn align_of_raw(&mut self, body: Body, instance: Instance) -> Body { + 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; @@ -652,17 +562,17 @@ impl IntrinsicGeneratorPass { 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); + // 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(); - args.0.push(GenericArgKind::Type(tail_ty)); - let operands = vec![Operand::Copy(Place::from(Local::from(1usize))), sized_op]; + 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::AlignOfDynPortion, + KaniModel::AlignOfDynObject, &args, operands, ); diff --git a/library/kani_core/src/lib.rs b/library/kani_core/src/lib.rs index 3a4a021b9b61..6418adc9c764 100644 --- a/library/kani_core/src/lib.rs +++ b/library/kani_core/src/lib.rs @@ -287,45 +287,6 @@ 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"] diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index e1fba0c683a1..4947e05fe467 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -156,16 +156,10 @@ macro_rules! kani_mem { /// /// 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"))] - { - 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()); - } + return kani_intrinsic(); #[cfg(feature = "concrete_playback")] if core::mem::size_of::<::Metadata>() == 0 { @@ -180,9 +174,18 @@ macro_rules! kani_mem { /// /// 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 { - crate::kani::align_of_raw(ptr) - .and_then(|align| align.is_power_of_two().then_some(align)) + #[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`. diff --git a/library/kani_core/src/models.rs b/library/kani_core/src/models.rs index 1ace949c5132..399f8fe4e65f 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -20,7 +20,8 @@ macro_rules! generate_models { if let Some(size) = kani::mem::checked_size_of_raw(ptr) { size } else { - kani::safety_check(false, "failed to compute size of val"); + // Note that today we trigger a safety check for foreign types. + kani::safety_check(false, "failed to compute `size_of_val`"); // Unreachable without panic. kani::kani_intrinsic() } @@ -31,7 +32,8 @@ macro_rules! generate_models { if let Some(size) = kani::mem::checked_align_of_raw(ptr) { size } else { - kani::safety_check(false, "failed to compute align of val"); + // Note that today we trigger a safety check for foreign types. + kani::safety_check(false, "failed to compute `align_of_val`"); // Unreachable without panic. kani::kani_intrinsic() } @@ -42,33 +44,84 @@ macro_rules! generate_models { mod mem_models { use core::ptr::{self, DynMetadata, Pointee}; - /// Retrieve the size of the object stored in the vtable. + /// Retrieve the size of the object pointed by the given raw pointer. /// - /// This model is used to implement `size_of_unsized_portion` intrinsic. + /// Where `U` is a trait, and `T` is either equal to `U` or has a tail `U`. /// - /// 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 + /// 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>, { - Some(ptr::metadata(ptr).size_of()) + 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); + // Adjust size to be a 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. /// - /// This model is used to implement `align_of_raw` intrinsic. + /// Where `U` is a trait, and `T` is either equal to `U` or has a tail `U`. /// - /// 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( + /// This model is used to implement `checked_aligned_of_raw`. + #[kanitool::fn_marker = "AlignOfDynObjectModel"] + pub(crate) fn align_of_dyn_object( ptr: *const T, - sized_portion: usize, + head_align: usize, ) -> Option where T: ?Sized + Pointee>, { - Some(ptr::metadata(ptr).align_of().max(sized_portion)) + 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. + /// + /// Most information are extracted by the Kani compiler at compilation time, + /// except for the length of the slice. + /// Thus, alignment should be safe to use (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); + // Adjust size to be a 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/expected/size_and_align/unsized_foreign.rs b/tests/expected/size_and_align/unsized_foreign.rs new file mode 100644 index 000000000000..796b856ef988 --- /dev/null +++ b/tests/expected/size_and_align/unsized_foreign.rs @@ -0,0 +1,41 @@ +// 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, this will trigger a safety check failure. +//! +//! 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. + +#![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) }; + assert_eq!(size, 4); +} + +#[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) }; + assert_eq!(align, 4); +} diff --git a/tests/kani/MemPredicates/adt_with_metadata.rs b/tests/kani/MemPredicates/adt_with_metadata.rs index 0bae910ef1cb..aa536b26279f 100644 --- a/tests/kani/MemPredicates/adt_with_metadata.rs +++ b/tests/kani/MemPredicates/adt_with_metadata.rs @@ -2,6 +2,7 @@ // 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; diff --git a/tests/kani/MemPredicates/foreign_type.rs b/tests/kani/MemPredicates/foreign_type.rs index 55bec34bc2c3..4787f5eed8b3 100644 --- a/tests/kani/MemPredicates/foreign_type.rs +++ b/tests/kani/MemPredicates/foreign_type.rs @@ -28,8 +28,8 @@ extern "C" { #[kani::proof] pub fn check_write_is_unsafe() { let mut var: Wrapper = kani::any(); - let fat_ptr: *mut Wrapper = &mut var as *mut _ as *mut _; - assert!(!can_write(fat_ptr)); + let ptr: *mut Wrapper = &mut var as *mut _ as *mut _; + assert!(!can_write(ptr)); } #[kani::proof] diff --git a/tests/kani/SizeAndAlignOfDst/fixme_unsized_foreign.rs b/tests/kani/SizeAndAlignOfDst/fixme_unsized_foreign.rs deleted file mode 100644 index 1bb639b7575f..000000000000 --- a/tests/kani/SizeAndAlignOfDst/fixme_unsized_foreign.rs +++ /dev/null @@ -1,19 +0,0 @@ -// 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 deleted file mode 100644 index 0edae52aa0ac..000000000000 --- a/tests/kani/SizeAndAlignOfDst/fixme_unsized_tuple.rs +++ /dev/null @@ -1,18 +0,0 @@ -// 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 index 095e9e1d4cbf..efd71f5ac44f 100644 --- a/tests/kani/SizeAndAlignOfDst/unsized_tail.rs +++ b/tests/kani/SizeAndAlignOfDst/unsized_tail.rs @@ -7,6 +7,7 @@ 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); @@ -62,10 +63,53 @@ pub fn checked_size_with_overflow() { } #[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)); +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); +} - let align_dyn = checked_align_of_raw(&Pair(10u8, [1i32; 10]) as &Pair); - assert_eq!(align_dyn, Some(4)); +#[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); } From 0128e6885b7420e3727b77a3ee352b446e2edbbb Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 13 Nov 2024 13:20:58 -0800 Subject: [PATCH 4/9] Better handling of foreign types --- library/kani_core/src/mem.rs | 2 +- library/kani_core/src/models.rs | 6 +++++- .../expected/intrinsics/size_of_dst.expected | 20 +++++++++++++++++++ tests/expected/intrinsics/size_of_dst.rs | 5 ++--- .../SizeAndAlignOfDst}/unsized_foreign.rs | 19 ++++++++++++------ 5 files changed, 41 insertions(+), 11 deletions(-) create mode 100644 tests/expected/intrinsics/size_of_dst.expected rename tests/{expected/size_and_align => kani/SizeAndAlignOfDst}/unsized_foreign.rs (67%) diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 4947e05fe467..c8cf06af62c6 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -296,7 +296,7 @@ macro_rules! kani_mem { #[doc(hidden)] #[rustc_diagnostic_item = "KaniPointerOffset"] #[inline(never)] - pub(crate) fn pointer_offset(_ptr: *const T) -> usize { + pub 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 index 399f8fe4e65f..a7a9764d340a 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -15,12 +15,14 @@ macro_rules! generate_models { #[allow(dead_code)] mod rustc_intrinsics { use crate::kani; + use core::ptr::Pointee; #[kanitool::fn_marker = "SizeOfValRawModel"] pub fn size_of_val_raw(ptr: *const T) -> usize { if let Some(size) = kani::mem::checked_size_of_raw(ptr) { size + } else if core::mem::size_of::<::Metadata>() == 0 { + kani::panic("cannot compute `size_of_val` for extern types") } else { - // Note that today we trigger a safety check for foreign types. kani::safety_check(false, "failed to compute `size_of_val`"); // Unreachable without panic. kani::kani_intrinsic() @@ -31,6 +33,8 @@ macro_rules! generate_models { pub fn align_of_val_raw(ptr: *const T) -> usize { if let Some(size) = kani::mem::checked_align_of_raw(ptr) { size + } else if core::mem::size_of::<::Metadata>() == 0 { + kani::panic("cannot compute `align_of_val` for extern types") } else { // Note that today we trigger a safety check for foreign types. kani::safety_check(false, "failed to compute `align_of_val`"); diff --git a/tests/expected/intrinsics/size_of_dst.expected b/tests/expected/intrinsics/size_of_dst.expected new file mode 100644 index 000000000000..70fe457f9223 --- /dev/null +++ b/tests/expected/intrinsics/size_of_dst.expected @@ -0,0 +1,20 @@ +Checking harness check_size_of_overflows... + +safety_check\ +Status: FAILURE\ +Description: "failed to compute `size_of_val`" + +Status: SUCCESS\ +Description: "assertion failed: unsafe { size_of_val_raw(new_ptr) } == expected_size" + +Failed Checks: failed to compute `size_of_val` +VERIFICATION:- FAILED + +Checking harness check_size_of_adt_overflows... + +0 of 2 cover properties satisfied (2 unreachable) +Failed Checks: failed to compute `size_of_val` +VERIFICATION:- FAILED + +Verification failed for - check_size_of_overflows +Verification failed for - check_size_of_adt_overflows diff --git a/tests/expected/intrinsics/size_of_dst.rs b/tests/expected/intrinsics/size_of_dst.rs index 6576fdea0450..eb2b2d392477 100644 --- a/tests/expected/intrinsics/size_of_dst.rs +++ b/tests/expected/intrinsics/size_of_dst.rs @@ -15,7 +15,6 @@ struct Wrapper { _value: T, } -#[cfg(ice)] #[kani::proof] pub fn check_size_of_adt_overflows() { let var: Wrapper<[u64; 4]> = kani::any(); @@ -23,17 +22,18 @@ pub fn check_size_of_adt_overflows() { 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) }; + kani::cover!(true, "Expected unreachable"); } } else { // Expect UB detection let _should_ub = unsafe { size_of_val_raw(new_ptr) }; + kani::cover!(true, "Expected unreachable"); } } @@ -44,7 +44,6 @@ pub fn check_size_of_overflows() { 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 { diff --git a/tests/expected/size_and_align/unsized_foreign.rs b/tests/kani/SizeAndAlignOfDst/unsized_foreign.rs similarity index 67% rename from tests/expected/size_and_align/unsized_foreign.rs rename to tests/kani/SizeAndAlignOfDst/unsized_foreign.rs index 796b856ef988..64cf042969f3 100644 --- a/tests/expected/size_and_align/unsized_foreign.rs +++ b/tests/kani/SizeAndAlignOfDst/unsized_foreign.rs @@ -1,16 +1,17 @@ // 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, this will trigger a safety check failure. +//! 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)] @@ -25,8 +26,7 @@ fn check_size_of_foreign() { 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) }; - assert_eq!(size, 4); + let _size = unsafe { std::mem::size_of_val_raw(ptr) }; } #[kani::proof] @@ -36,6 +36,13 @@ fn check_align_of_foreign() { 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) }; - assert_eq!(align, 4); + 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); } From 61ea50bbf8447510ddb13930c86b35dadee01efd Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Wed, 13 Nov 2024 14:03:32 -0800 Subject: [PATCH 5/9] Fix regression failures --- .../compiler_interface.rs | 4 ++- .../src/kani_middle/kani_functions.rs | 34 +++++++++++++------ .../kani_middle/transform/check_uninit/mod.rs | 1 + .../kani_middle/transform/kani_intrinsics.rs | 2 +- library/kani_core/src/mem_init.rs | 3 ++ 5 files changed, 31 insertions(+), 13 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs index 6e07390940fe..9d5e6fe605a5 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs @@ -243,7 +243,9 @@ impl CodegenBackend for GotocCodegenBackend { check_target(tcx.sess); check_options(tcx.sess); - if !queries.args().build_std && queries.kani_functions().is_empty() { + if queries.args().reachability_analysis != ReachabilityType::None + && queries.kani_functions().is_empty() + { tcx.sess.dcx().err( "Failed to detect Kani functions. Please check your installation is correct.", ); diff --git a/kani-compiler/src/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index cd0f07802f7e..dd9331160302 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -29,8 +29,9 @@ use stable_mir::mir::mono::Instance; use stable_mir::ty::FnDef; use std::collections::HashMap; use std::str::FromStr; -use strum_macros::{EnumString, IntoStaticStr}; -use tracing::{debug, trace}; +use strum::IntoEnumIterator; +use strum_macros::{EnumIter, EnumString, IntoStaticStr}; +use tracing::debug; #[derive(Debug, Copy, Clone, Eq, PartialEq, Hash)] pub enum KaniFunction { @@ -42,7 +43,7 @@ pub enum KaniFunction { /// /// These functions usually depend on information that require extra knowledge about the type /// or extra Kani instrumentation. -#[derive(Debug, Copy, Clone, Eq, PartialEq, IntoStaticStr, EnumString, Hash)] +#[derive(Debug, Copy, Clone, Eq, PartialEq, IntoStaticStr, EnumIter, EnumString, Hash)] pub enum KaniIntrinsic { #[strum(serialize = "ValidValueIntrinsic")] ValidValue, @@ -57,8 +58,10 @@ pub enum KaniIntrinsic { } /// Kani models are Rust functions that model some runtime behavior used by Kani instrumentation. -#[derive(Debug, Copy, Clone, Eq, PartialEq, IntoStaticStr, EnumString, Hash)] +#[derive(Debug, Copy, Clone, Eq, PartialEq, IntoStaticStr, EnumIter, EnumString, Hash)] pub enum KaniModel { + #[strum(serialize = "IsPtrInitializedModel")] + IsPtrInitialized, #[strum(serialize = "IsStrPtrInitializedModel")] IsStrPtrInitialized, #[strum(serialize = "IsSlicePtrInitializedModel")] @@ -122,21 +125,19 @@ impl TryFrom for KaniFunction { /// 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() + let fns = 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) @@ -147,12 +148,23 @@ pub fn find_kani_functions() -> HashMap { // If there are no definitions, return `None` to indicate that. (!kani_funcs.is_empty()).then_some(kani_funcs) }) - .unwrap_or_default() + .unwrap_or_default(); + if cfg!(debug_assertions) { + validate_kani_functions(&fns); + } + fns } /// 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)); + let mut missing = 0u8; + for func in KaniIntrinsic::iter().map(|i| i.into()).chain(KaniModel::iter().map(|m| m.into())) { + if let Some(fn_def) = kani_funcs.get(&func) { + assert_eq!(KaniFunction::try_from(*fn_def), Ok(func), "Unexpected function marker"); + } else { + tracing::error!(?func, "Missing kani function"); + missing += 1; + } } + assert_eq!(missing, 0, "Failed to find `{missing}` Kani functions"); } diff --git a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs index 1ce21ef50669..f23ca9c8721e 100644 --- a/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs +++ b/kani-compiler/src/kani_middle/transform/check_uninit/mod.rs @@ -35,6 +35,7 @@ pub trait TargetFinder { fn find_all(self, body: &MutableBody) -> Vec; } +// TODO: Use `KaniFunctions` instead. const KANI_IS_PTR_INITIALIZED_DIAGNOSTIC: &str = "KaniIsPtrInitialized"; const KANI_SET_PTR_INITIALIZED_DIAGNOSTIC: &str = "KaniSetPtrInitialized"; const KANI_IS_SLICE_CHUNK_PTR_INITIALIZED_DIAGNOSTIC: &str = "KaniIsSliceChunkPtrInitialized"; diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 492a61e79e0e..5cc8c2d43459 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -243,7 +243,7 @@ impl IntrinsicGeneratorPass { return new_body.into(); } let is_ptr_initialized_instance = resolve_mem_init_fn( - *self.kani_defs.get(&KaniIntrinsic::IsInitialized.into()).unwrap(), + *self.kani_defs.get(&KaniModel::IsPtrInitialized.into()).unwrap(), layout.len(), *pointee_info.ty(), ); diff --git a/library/kani_core/src/mem_init.rs b/library/kani_core/src/mem_init.rs index 6475c62e31ae..ba64bb40fd5f 100644 --- a/library/kani_core/src/mem_init.rs +++ b/library/kani_core/src/mem_init.rs @@ -211,6 +211,7 @@ macro_rules! kani_mem_init { /// Get initialization state of `num_elts` items laid out according to the `layout` starting at address `ptr`. #[kanitool::disable_checks(pointer)] + #[kanitool::fn_marker = "IsPtrInitializedModel"] #[rustc_diagnostic_item = "KaniIsPtrInitialized"] fn is_ptr_initialized( ptr: *const T, @@ -275,6 +276,7 @@ macro_rules! kani_mem_init { /// Get initialization state of the slice, items of which are laid out according to the `layout` starting at address `ptr`. #[kanitool::disable_checks(pointer)] + #[kanitool::fn_marker = "IsSlicePtrInitializedModel"] #[rustc_diagnostic_item = "KaniIsSlicePtrInitialized"] fn is_slice_ptr_initialized( ptr: *const [T], @@ -306,6 +308,7 @@ macro_rules! kani_mem_init { /// Get initialization state of the string slice, items of which are laid out according to the `layout` starting at address `ptr`. #[kanitool::disable_checks(pointer)] + #[kanitool::fn_marker = "IsStrPtrInitializedModel"] #[rustc_diagnostic_item = "KaniIsStrPtrInitialized"] fn is_str_ptr_initialized( ptr: *const str, From a10a746a0055c41d9cbc21c8c1386e4dd4bef9a5 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 18 Nov 2024 13:18:16 -0800 Subject: [PATCH 6/9] Move fixes to `_of_val` to a new PR Revert changes to intrinsics and remove tests for now --- .../codegen/intrinsic.rs | 16 ++- .../src/kani_middle/kani_functions.rs | 4 - .../src/kani_middle/transform/mod.rs | 3 - .../kani_middle/transform/rustc_intrinsics.rs | 112 ------------------ library/kani_core/src/models.rs | 34 ------ .../expected/intrinsics/size_of_dst.expected | 20 ---- tests/expected/intrinsics/size_of_dst.rs | 53 --------- ...ed_foreign.rs => fixme_unsized_foreign.rs} | 0 8 files changed, 13 insertions(+), 229 deletions(-) delete mode 100644 kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs delete mode 100644 tests/expected/intrinsics/size_of_dst.expected delete mode 100644 tests/expected/intrinsics/size_of_dst.rs rename tests/kani/SizeAndAlignOfDst/{unsized_foreign.rs => fixme_unsized_foreign.rs} (100%) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 3a72fd45fa35..97b13e5f4185 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs @@ -215,6 +215,17 @@ 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 @@ -411,6 +422,7 @@ 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 => { @@ -504,6 +516,7 @@ 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( @@ -546,9 +559,6 @@ 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/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 20d0b9219b20..974872f8f279 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -61,8 +61,6 @@ pub enum KaniIntrinsic { pub enum KaniModel { #[strum(serialize = "AlignOfDynObjectModel")] AlignOfDynObject, - #[strum(serialize = "AlignOfValRawModel")] - AlignOfVal, #[strum(serialize = "AnyModel")] Any, #[strum(serialize = "CopyInitStateModel")] @@ -97,8 +95,6 @@ pub enum KaniModel { SizeOfDynObject, #[strum(serialize = "SizeOfSliceObjectModel")] SizeOfSliceObject, - #[strum(serialize = "SizeOfValRawModel")] - SizeOfVal, #[strum(serialize = "StoreArgumentModel")] StoreArgument, #[strum(serialize = "WriteAnySliceModel")] diff --git a/kani-compiler/src/kani_middle/transform/mod.rs b/kani-compiler/src/kani_middle/transform/mod.rs index 8001b1f1d359..5a02d6e725f2 100644 --- a/kani-compiler/src/kani_middle/transform/mod.rs +++ b/kani-compiler/src/kani_middle/transform/mod.rs @@ -33,7 +33,6 @@ 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; @@ -44,7 +43,6 @@ 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. @@ -90,7 +88,6 @@ impl BodyTransformation { }); transformer.add_pass(queries, IntrinsicGeneratorPass::new(check_type, &queries)); transformer.add_pass(queries, LoopContractPass::new(tcx, queries, &unit)); - transformer.add_pass(queries, RustcIntrinsicsPass::new(&queries)); transformer } diff --git a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs deleted file mode 100644 index 53832948bf6b..000000000000 --- a/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs +++ /dev/null @@ -1,112 +0,0 @@ -// 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 MutMirVisitor for ReplaceIntrinsicVisitor<'_> { - /// 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/library/kani_core/src/models.rs b/library/kani_core/src/models.rs index a7a9764d340a..b43f2e0f94e5 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -10,40 +10,6 @@ #[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; - use core::ptr::Pointee; - #[kanitool::fn_marker = "SizeOfValRawModel"] - pub fn size_of_val_raw(ptr: *const T) -> usize { - if let Some(size) = kani::mem::checked_size_of_raw(ptr) { - size - } else if core::mem::size_of::<::Metadata>() == 0 { - kani::panic("cannot compute `size_of_val` for extern types") - } 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 if core::mem::size_of::<::Metadata>() == 0 { - kani::panic("cannot compute `align_of_val` for extern types") - } else { - // Note that today we trigger a safety check for foreign types. - 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}; diff --git a/tests/expected/intrinsics/size_of_dst.expected b/tests/expected/intrinsics/size_of_dst.expected deleted file mode 100644 index 70fe457f9223..000000000000 --- a/tests/expected/intrinsics/size_of_dst.expected +++ /dev/null @@ -1,20 +0,0 @@ -Checking harness check_size_of_overflows... - -safety_check\ -Status: FAILURE\ -Description: "failed to compute `size_of_val`" - -Status: SUCCESS\ -Description: "assertion failed: unsafe { size_of_val_raw(new_ptr) } == expected_size" - -Failed Checks: failed to compute `size_of_val` -VERIFICATION:- FAILED - -Checking harness check_size_of_adt_overflows... - -0 of 2 cover properties satisfied (2 unreachable) -Failed Checks: failed to compute `size_of_val` -VERIFICATION:- FAILED - -Verification failed for - check_size_of_overflows -Verification failed for - check_size_of_adt_overflows diff --git a/tests/expected/intrinsics/size_of_dst.rs b/tests/expected/intrinsics/size_of_dst.rs deleted file mode 100644 index eb2b2d392477..000000000000 --- a/tests/expected/intrinsics/size_of_dst.rs +++ /dev/null @@ -1,53 +0,0 @@ -// 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, -} - -#[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); - 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) }; - kani::cover!(true, "Expected unreachable"); - } - } else { - // Expect UB detection - let _should_ub = unsafe { size_of_val_raw(new_ptr) }; - kani::cover!(true, "Expected unreachable"); - } -} - -#[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); - 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/SizeAndAlignOfDst/unsized_foreign.rs b/tests/kani/SizeAndAlignOfDst/fixme_unsized_foreign.rs similarity index 100% rename from tests/kani/SizeAndAlignOfDst/unsized_foreign.rs rename to tests/kani/SizeAndAlignOfDst/fixme_unsized_foreign.rs From 5c4d5b7187eaedc5d3f3d797de663c4285df4c06 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 21 Nov 2024 17:04:04 -0800 Subject: [PATCH 7/9] Apply suggestions from code review Co-authored-by: Carolyn Zech --- .../src/kani_middle/transform/kani_intrinsics.rs | 12 +++++++++--- library/kani_core/src/mem.rs | 2 +- library/kani_core/src/models.rs | 4 ++-- 3 files changed, 12 insertions(+), 6 deletions(-) diff --git a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs index 85769a17a2c9..206c0160a80d 100644 --- a/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs +++ b/kani-compiler/src/kani_middle/transform/kani_intrinsics.rs @@ -404,7 +404,7 @@ impl IntrinsicGeneratorPass { 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}") + unreachable!("Expected a pointer argument, but got {ptr_ty}") }; let pointee_layout = LayoutOf::new(pointee_ty); debug!(?ptr_ty, ?pointee_layout, "checked_size_of"); @@ -530,7 +530,7 @@ impl IntrinsicGeneratorPass { 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}") + unreachable!("Expected a pointer argument, but got {ptr_ty}") }; let pointee_layout = LayoutOf::new(pointee_ty); debug!(?ptr_ty, "align_of_raw"); @@ -572,7 +572,11 @@ impl IntrinsicGeneratorPass { ); } else { // Cannot compute size of foreign types. Return None! - assert!(pointee_layout.has_foreign_tail()); + 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), @@ -605,6 +609,7 @@ impl IntrinsicGeneratorPass { } /// 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() @@ -614,6 +619,7 @@ fn build_some(option: AdtDef, args: GenericArgs, val_op: Operand) -> Rvalue { } /// 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(); diff --git a/library/kani_core/src/mem.rs b/library/kani_core/src/mem.rs index 36a3864f6a96..5921b52faff2 100644 --- a/library/kani_core/src/mem.rs +++ b/library/kani_core/src/mem.rs @@ -152,7 +152,7 @@ macro_rules! kani_mem { cbmc::same_allocation(ptr1, ptr2) } - /// Compute the size of the val pointed to if safe. + /// 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. diff --git a/library/kani_core/src/models.rs b/library/kani_core/src/models.rs index b43f2e0f94e5..c36437bc9d48 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -33,7 +33,7 @@ macro_rules! generate_models { if align.is_power_of_two() { let size_dyn = metadata.size_of(); let (total, sum_overflow) = size_dyn.overflowing_add(head_size); - // Adjust size to be a multiple of alignment, i.e.: (size + (align - 1)) & -align + // 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 _ { @@ -80,7 +80,7 @@ macro_rules! generate_models { ) -> Option { let (slice_sz, mul_overflow) = elem_size.overflowing_mul(len); let (total, sum_overflow) = slice_sz.overflowing_add(head_size); - // Adjust size to be a multiple of alignment, i.e.: (size + (align - 1)) & -align + // 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 From 97e90482c271f268fe3ff91d5af0f2393e1f34d6 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Thu, 21 Nov 2024 17:04:20 -0800 Subject: [PATCH 8/9] Update library/kani_core/src/models.rs --- library/kani_core/src/models.rs | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/library/kani_core/src/models.rs b/library/kani_core/src/models.rs index c36437bc9d48..258c90901c00 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -65,9 +65,10 @@ macro_rules! generate_models { /// Compute the size of a slice or object with a slice tail. /// - /// Most information are extracted by the Kani compiler at compilation time, - /// except for the length of the slice. - /// Thus, alignment should be safe to use (power-of-two and smaller than isize::MAX). + /// 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`. From f3736ccf332e36f62399dc89fc04d89dbc1d7699 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Fri, 22 Nov 2024 11:41:43 -0800 Subject: [PATCH 9/9] Add more comments and split test --- library/kani_core/src/models.rs | 23 ++++++++++++++++++++++- tests/kani/MemPredicates/foreign_type.rs | 15 ++++++++++++++- 2 files changed, 36 insertions(+), 2 deletions(-) diff --git a/library/kani_core/src/models.rs b/library/kani_core/src/models.rs index 258c90901c00..455c8834a345 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -3,7 +3,8 @@ //! 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. +//! 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] @@ -18,6 +19,16 @@ macro_rules! generate_models { /// /// 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( @@ -50,6 +61,16 @@ macro_rules! generate_models { /// /// 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( diff --git a/tests/kani/MemPredicates/foreign_type.rs b/tests/kani/MemPredicates/foreign_type.rs index 4787f5eed8b3..52e525c62b33 100644 --- a/tests/kani/MemPredicates/foreign_type.rs +++ b/tests/kani/MemPredicates/foreign_type.rs @@ -44,13 +44,26 @@ pub fn check_read_is_unsafe() { /// /// However, foreign APIs that have knowledge of the type can still safely set new values. #[kani::proof] -#[kani::should_panic] 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); }