Fix size and alignment computation for intrinsics (#3734)

Implement overflow checks for `size_of_val`, and panic for foreign
types.

Resolves #3616 

By submitting this pull request, I confirm that my contribution is made
under the terms of the Apache 2.0 and MIT licenses.

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,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<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 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);
+    }
+}

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/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

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<T, U: ?Sized> {
+    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:
+/// <https://github.com/rust-lang/rust/blob/7db7489f9bc2/tests/ui/repr/repr-align.rs#L11>
+#[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::<Wrapper<$t1, $t2>>();
+            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::<usize>());
+check_alignment!(check_1char_tup, (char, usize, u128), char, align_of::<u128>());
+check_alignment!(check_zst1024, (char, usize, u128), Zst1024, align_of::<Zst1024>());
+check_alignment!(check_large, u128, LargeAlign, align_of::<LargeAlign>());

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