From fa53f26c3e397bbda836a348d4a1fd35e359a551 Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Sun, 24 Nov 2024 18:11:29 -0800 Subject: [PATCH] Fix size and alignment computation for intrinsics Implement overflow checks for `size_of_val`, and panic for foreign types. --- .../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 | 33 ++++++ .../expected/intrinsics/size_of_dst.expected | 20 ++++ tests/expected/intrinsics/size_of_dst.rs | 53 +++++++++ ..._unsized_foreign.rs => unsized_foreign.rs} | 0 8 files changed, 228 insertions(+), 13 deletions(-) create mode 100644 kani-compiler/src/kani_middle/transform/rustc_intrinsics.rs create mode 100644 tests/expected/intrinsics/size_of_dst.expected create mode 100644 tests/expected/intrinsics/size_of_dst.rs rename tests/kani/SizeAndAlignOfDst/{fixme_unsized_foreign.rs => 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 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..baa22fb7a045 --- /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 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 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/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