Fix size and alignment computation for intrinsics

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)

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")]

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
     }
 

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<KaniModel, FnDef>,
+}
+
+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<KaniModel, FnDef>,
+    locals: Vec<LocalDecl>,
+    changed: bool,
+}
+
+impl<'a> ReplaceIntrinsicVisitor<'a> {
+    fn new(models: &'a HashMap<KaniModel, FnDef>, locals: Vec<LocalDecl>) -> 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);
+    }
+}

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<T: ?Sized>(ptr: *const T) -> usize {
+                if let Some(size) = kani::mem::checked_size_of_raw(ptr) {
+                    size
+                } else if core::mem::size_of::<<T as Pointee>::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<T: ?Sized>(ptr: *const T) -> usize {
+                if let Some(size) = kani::mem::checked_align_of_raw(ptr) {
+                    size
+                } else if core::mem::size_of::<<T as Pointee>::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};

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

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<T: ?Sized> {
+    _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::<u64>()) {
+        if let Some(expected_size) = slice_size.checked_add(size_of::<usize>()) {
+            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::<u64>()) {
+        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) };
+    }
+}