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