diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/intrinsic.rs index 97b13e5f4185..3a72fd45fa35 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 @@ -422,7 +411,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 => { @@ -516,7 +504,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( @@ -559,6 +546,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/kani_middle/kani_functions.rs b/kani-compiler/src/kani_middle/kani_functions.rs index 974872f8f279..20d0b9219b20 100644 --- a/kani-compiler/src/kani_middle/kani_functions.rs +++ b/kani-compiler/src/kani_middle/kani_functions.rs @@ -61,6 +61,8 @@ pub enum KaniIntrinsic { pub enum KaniModel { #[strum(serialize = "AlignOfDynObjectModel")] AlignOfDynObject, + #[strum(serialize = "AlignOfValRawModel")] + AlignOfVal, #[strum(serialize = "AnyModel")] Any, #[strum(serialize = "CopyInitStateModel")] @@ -95,6 +97,8 @@ 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 5a02d6e725f2..8001b1f1d359 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. @@ -88,6 +90,7 @@ 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 new file mode 100644 index 000000000000..8174e8eb5e66 --- /dev/null +++ b/kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs @@ -0,0 +1,119 @@ +// 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 rustc's intrinsics. + /// + /// In some cases, we replace a function call to a rustc intrinsic by a call to the + /// corresponding Kani intrinsic. + /// + /// Our models are usually augmented by some trait bounds, or they leverage Kani intrinsics to + /// implement the given semantics. + /// + /// Note that we only need to replace function calls since intrinsics must always be called + /// directly. I.e., no need to handle function pointers. + 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 codegen. + _ => { + 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 455c8834a345..c2be6117a7df 100644 --- a/library/kani_core/src/models.rs +++ b/library/kani_core/src/models.rs @@ -11,6 +11,39 @@ #[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 { + 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/align_of_dst.expected b/tests/expected/intrinsics/align_of_dst.expected new file mode 100644 index 000000000000..ed63dd42384c --- /dev/null +++ b/tests/expected/intrinsics/align_of_dst.expected @@ -0,0 +1,6 @@ +Checking harness check_zst1024... +Checking harness check_large... +Checking harness check_1char_tup... +Checking harness check_1zst_usize... + +Complete - 4 successfully verified harnesses, 0 failures, 4 total \ No newline at end of file diff --git a/tests/expected/intrinsics/align_of_dst.rs b/tests/expected/intrinsics/align_of_dst.rs new file mode 100644 index 000000000000..7025f35df6f4 --- /dev/null +++ b/tests/expected/intrinsics/align_of_dst.rs @@ -0,0 +1,75 @@ +// Copyright Kani Contributors +// SPDX-License-Identifier: Apache-2.0 OR MIT + +//! This test case checks the behavior of `align_of_val_raw` for dynamically sized types. + +#![feature(layout_for_ptr)] +#![feature(ptr_metadata)] + +use std::any::Any; +use std::mem::align_of; + +#[allow(unused)] +#[derive(Clone, Copy, kani::Arbitrary)] +struct Wrapper { + head: T, + dst: U, +} + +/// Create a ZST with an alignment of 1024. +#[allow(unused)] +#[repr(align(1024))] +#[derive(kani::Arbitrary)] +struct Zst1024; + +/// Create a structure with large alignment (2^29). +/// +/// This seems to be the maximum supported today: +/// +#[repr(align(536870912))] +#[derive(kani::Arbitrary)] +struct LargeAlign { + data: [usize; 100], +} + +/// Generates a harness with different type combinations and check the alignment is correct. +/// We use a constant for the original type, so it is pre-populated by the compiler. +/// +/// ## Parameters +/// - `name`: Name of the harness. +/// - `t1` / `t2`: Types used for different tail and head combinations. +/// - `expected`: The expected alignment. +macro_rules! check_alignment { + ($name:ident, $t1:ty, $t2:ty, $expected:expr) => { + #[kani::proof] + fn $name() { + const EXPECTED: usize = align_of::>(); + assert_eq!(EXPECTED, $expected); + + let var: Wrapper<$t1, $t2> = kani::any(); + let wide_ptr: &Wrapper<$t1, dyn Any> = &var as &_; + let dyn_t2_align = align_of_val(wide_ptr); + assert_eq!(dyn_t2_align, EXPECTED, "Expected same alignment as before coercion"); + + let var: Wrapper<$t2, $t1> = kani::any(); + let wide_ptr: &Wrapper<$t2, dyn Any> = &var as &_; + let dyn_t1_align = align_of_val(wide_ptr); + assert_eq!(dyn_t1_align, EXPECTED, "Expected same alignment as before coercion"); + + let var: Wrapper<$t1, [$t2; 0]> = kani::any(); + let wide_ptr: &Wrapper<$t1, [$t2]> = &var as &_; + let slice_t2_align = align_of_val(wide_ptr); + assert_eq!(slice_t2_align, EXPECTED, "Expected same alignment as before coercion"); + + let var: Wrapper<$t2, [$t1; 0]> = kani::any(); + let wide_ptr: &Wrapper<$t2, [$t1]> = &var as &_; + let slice_t1_align = align_of_val(wide_ptr); + assert_eq!(slice_t1_align, EXPECTED, "Expected same alignment as before coercion"); + } + }; +} + +check_alignment!(check_1zst_usize, usize, (), align_of::()); +check_alignment!(check_1char_tup, (char, usize, u128), char, align_of::()); +check_alignment!(check_zst1024, (char, usize, u128), Zst1024, align_of::()); +check_alignment!(check_large, u128, LargeAlign, align_of::()); 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 new file mode 100644 index 000000000000..eb2b2d392477 --- /dev/null +++ b/tests/expected/intrinsics/size_of_dst.rs @@ -0,0 +1,53 @@ +// 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/fixme_unsized_foreign.rs b/tests/kani/SizeAndAlignOfDst/unsized_foreign.rs similarity index 100% rename from tests/kani/SizeAndAlignOfDst/fixme_unsized_foreign.rs rename to tests/kani/SizeAndAlignOfDst/unsized_foreign.rs