Fix issues with how we compute DST size

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/codegen_cprover_gotoc/codegen/place.rs

@@ -456,7 +456,7 @@ impl GotocCtx<'_> {
                     | TyKind::RigidTy(RigidTy::Dynamic(..)) => {
                         inner_goto_expr.member("data", &self.symbol_table)
                     }
-                    TyKind::RigidTy(RigidTy::Adt(..))
+                    TyKind::RigidTy(RigidTy::Adt(..)) | TyKind::RigidTy(RigidTy::Tuple(..))
                         if self.is_unsized(inner_mir_typ_internal) =>
                     {
                         // in tests/kani/Strings/os_str_reduced.rs, we see

kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs

@@ -6,6 +6,7 @@ use crate::codegen_cprover_gotoc::codegen::place::ProjectedPlace;
 use crate::codegen_cprover_gotoc::codegen::ty_stable::pointee_type_stable;
 use crate::codegen_cprover_gotoc::utils::{dynamic_fat_ptr, slice_fat_ptr};
 use crate::codegen_cprover_gotoc::{GotocCtx, VtableCtx};
+use crate::kani_middle::abi::LayoutOf;
 use crate::kani_middle::coercion::{
     CoerceUnsizedInfo, CoerceUnsizedIterator, CoercionBaseStable, extract_unsize_casting_stable,
 };
@@ -710,21 +711,32 @@ impl GotocCtx<'_> {
                         slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
                     }
                     TyKind::RigidTy(RigidTy::Adt(..)) => {
+                        let layout = LayoutOf::new(pointee_ty);
                         let pointee_goto_typ = self.codegen_ty_stable(pointee_ty);
                         let data_cast =
                             data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) });
-                        let meta = self.codegen_operand_stable(&operands[1]);
-                        if meta.typ().sizeof(&self.symbol_table) == 0 {
-                            data_cast
-                        } else {
-                            let vtable_expr = meta
-                                .member("_vtable_ptr", &self.symbol_table)
-                                .member("pointer", &self.symbol_table)
-                                .cast_to(
-                                    typ.lookup_field_type("vtable", &self.symbol_table).unwrap(),
-                                );
-                            dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table)
-                        }
+                        layout.unsized_tail().map_or(data_cast.clone(), |tail| {
+                            let meta = self.codegen_operand_stable(&operands[1]);
+                            match tail.kind().rigid().unwrap() {
+                                RigidTy::Foreign(..) => data_cast,
+                                RigidTy::Slice(..) | RigidTy::Str => {
+                                    slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
+                                }
+                                RigidTy::Dynamic(..) => {
+                                    let vtable_expr = meta
+                                        .member("_vtable_ptr", &self.symbol_table)
+                                        .member("pointer", &self.symbol_table)
+                                        .cast_to(
+                                            typ.lookup_field_type("vtable", &self.symbol_table)
+                                                .unwrap(),
+                                        );
+                                    dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table)
+                                }
+                                _ => {
+                                    unreachable!("Unexpected unsized tail: {tail:?}");
+                                }
+                            }
+                        })
                     }
                     TyKind::RigidTy(RigidTy::Dynamic(..)) => {
                         let pointee_goto_typ = self.codegen_ty_stable(pointee_ty);

kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs

@@ -1571,14 +1571,11 @@ impl<'tcx> GotocCtx<'tcx> {
             return None;
         }
 
-        let mut typ = struct_type;
-        while let ty::Adt(adt_def, adt_args) = typ.kind() {
-            assert_eq!(adt_def.variants().len(), 1, "Expected a single-variant ADT. Found {typ:?}");
-            let fields = &adt_def.variants().get(VariantIdx::from_u32(0)).unwrap().fields;
-            let last_field = fields.last_index().expect("Trait should be the last element.");
-            typ = fields[last_field].ty(self.tcx, adt_args);
-        }
-        if typ.is_trait() { Some(typ) } else { None }
+        let ty = rustc_internal::stable(struct_type);
+        rustc_internal::internal(
+            self.tcx,
+            crate::kani_middle::abi::LayoutOf::new(ty).unsized_tail(),
+        )
     }
 
     /// This function provides an iterator that traverses the data path of a receiver type. I.e.:

kani-compiler/src/codegen_cprover_gotoc/compiler_interface.rs

@@ -237,10 +237,17 @@ impl CodegenBackend for GotocCodegenBackend {
         let ret_val = rustc_internal::run(tcx, || {
             super::utils::init();
 
-            // Queries shouldn't change today once codegen starts.
+            // Any changes to queries from this point on is just related to caching information
+            // for efficiency purpose that should not outlive the stable-mir `run` scope.
             let queries = self.queries.lock().unwrap().clone();
+
             check_target(tcx.sess);
             check_options(tcx.sess);
+            if !queries.args().build_std && queries.kani_functions().is_empty() {
+                tcx.sess.dcx().err(
+                    "Failed to detect Kani functions. Please check your installation is correct.",
+                );
+            }
 
             // Codegen all items that need to be processed according to the selected reachability mode:
             //

kani-compiler/src/codegen_cprover_gotoc/overrides/hooks.rs

@@ -12,6 +12,7 @@ use crate::codegen_cprover_gotoc::GotocCtx;
 use crate::codegen_cprover_gotoc::codegen::{PropertyClass, bb_label};
 use crate::kani_middle::attributes::KaniAttributes;
 use crate::kani_middle::attributes::matches_diagnostic as matches_function;
+use crate::kani_middle::kani_functions::{KaniFunction, KaniIntrinsic};
 use crate::unwrap_or_return_codegen_unimplemented_stmt;
 use cbmc::goto_program::CIntType;
 use cbmc::goto_program::{BuiltinFn, Expr, Stmt, Type};
@@ -146,6 +147,37 @@ impl GotocHook for Assert {
     }
 }
 
+struct SafetyCheck;
+impl GotocHook for SafetyCheck {
+    fn hook_applies(&self, _tcx: TyCtxt, instance: Instance) -> bool {
+        KaniFunction::try_from(instance) == Ok(KaniFunction::Intrinsic(KaniIntrinsic::SafetyCheck))
+    }
+
+    fn handle(
+        &self,
+        gcx: &mut GotocCtx,
+        _instance: Instance,
+        mut fargs: Vec<Expr>,
+        _assign_to: &Place,
+        target: Option<BasicBlockIdx>,
+        span: Span,
+    ) -> Stmt {
+        assert_eq!(fargs.len(), 2);
+        let cond = fargs.remove(0).cast_to(Type::bool());
+        let msg = fargs.remove(0);
+        let msg = gcx.extract_const_message(&msg).unwrap();
+        let target = target.unwrap();
+        let caller_loc = gcx.codegen_caller_span_stable(span);
+        Stmt::block(
+            vec![
+                gcx.codegen_assert_assume(cond, PropertyClass::SafetyCheck, &msg, caller_loc),
+                Stmt::goto(bb_label(target), caller_loc),
+            ],
+            caller_loc,
+        )
+    }
+}
+
 struct Check;
 impl GotocHook for Check {
     fn hook_applies(&self, tcx: TyCtxt, instance: Instance) -> bool {
@@ -623,6 +655,7 @@ pub fn fn_hooks() -> GotocHooks {
             Rc::new(Assume),
             Rc::new(Assert),
             Rc::new(Check),
+            Rc::new(SafetyCheck),
             Rc::new(Cover),
             Rc::new(Nondet),
             Rc::new(IsAllocated),

kani-compiler/src/kani_middle/abi.rs

@@ -0,0 +1,193 @@
+// Copyright Kani Contributors
+// SPDX-License-Identifier: Apache-2.0 OR MIT
+//! This module contains code for handling type abi information.
+
+use stable_mir::abi::{FieldsShape, LayoutShape};
+use stable_mir::ty::{RigidTy, Ty, TyKind, UintTy};
+use tracing::debug;
+
+/// A struct to encapsulate the layout information for a given type
+#[derive(Clone, Debug, PartialEq, Eq)]
+pub struct LayoutOf {
+    ty: Ty,
+    layout: LayoutShape,
+}
+
+impl LayoutOf {
+    /// Create the layout structure for the given type
+    pub fn new(ty: Ty) -> LayoutOf {
+        LayoutOf { ty, layout: ty.layout().unwrap().shape() }
+    }
+
+    /// Return whether the type is sized.
+    pub fn is_sized(&self) -> bool {
+        self.layout.is_sized()
+    }
+
+    /// Return whether the type is unsized and its tail is a foreign item.
+    ///
+    /// This will also return `true` if the type is foreign.
+    pub fn has_foreign_tail(&self) -> bool {
+        self.unsized_tail()
+            .map_or(false, |t| matches!(t.kind(), TyKind::RigidTy(RigidTy::Foreign(_))))
+    }
+
+    /// Return whether the type is unsized and its tail is a trait object.
+    pub fn has_trait_tail(&self) -> bool {
+        self.unsized_tail().map_or(false, |t| t.kind().is_trait())
+    }
+
+    /// Return whether the type is unsized and its tail is a slice.
+    #[allow(dead_code)]
+    pub fn has_slice_tail(&self) -> bool {
+        self.unsized_tail().map_or(false, |tail| {
+            let kind = tail.kind();
+            kind.is_slice() | kind.is_str()
+        })
+    }
+
+    /// Return the unsized tail of the type if this is an unsized type.
+    ///
+    /// For foreign types, return None.
+    /// For unsized types, this should return either a slice, a string slice, a dynamic type.
+    /// For other types, this function will return `None`.
+    pub fn unsized_tail(&self) -> Option<Ty> {
+        if self.layout.is_unsized() {
+            match self.ty.kind().rigid().unwrap() {
+                RigidTy::Slice(..) | RigidTy::Dynamic(..) | RigidTy::Str => Some(self.ty),
+                RigidTy::Adt(..) | RigidTy::Tuple(..) => {
+                    // Recurse the tail field type until we find the unsized tail.
+                    self.last_field_layout().unsized_tail()
+                }
+                RigidTy::Foreign(_) => Some(self.ty),
+                _ => unreachable!("Expected unsized type but found `{}`", self.ty),
+            }
+        } else {
+            None
+        }
+    }
+
+    /// Return the type of the elements of the array or slice at the unsized tail of this type.
+    ///
+    /// For sized types and trait unsized type, this function will return `None`.
+    pub fn unsized_tail_elem_ty(&self) -> Option<Ty> {
+        self.unsized_tail().and_then(|tail| match tail.kind().rigid().unwrap() {
+            RigidTy::Slice(elem_ty) => Some(*elem_ty),
+            // String slices have the same layout as slices of u8.
+            // https://doc.rust-lang.org/reference/type-layout.html#str-layout
+            RigidTy::Str => Some(Ty::unsigned_ty(UintTy::U8)),
+            _ => None,
+        })
+    }
+
+    /// Return the size of the sized portion of this type.
+    ///
+    /// For a sized type, this function will return the size of the type.
+    /// For an unsized type, this function will return the size of the sized portion including
+    /// any padding bytes that lead to the unsized field.
+    /// I.e.: the size of the type, excluding the trailing unsized portion.
+    ///
+    /// For example, this function will return 2 as the sized portion of `*const (u8,  [u16])`:
+    pub fn size_of_head(&self) -> usize {
+        if self.is_sized() {
+            self.layout.size.bytes()
+        } else {
+            match self.ty.kind().rigid().unwrap() {
+                RigidTy::Slice(_) | RigidTy::Str | RigidTy::Dynamic(..) | RigidTy::Foreign(..) => 0,
+                RigidTy::Adt(..) | RigidTy::Tuple(..) => {
+                    let fields_sorted = self.layout.fields.fields_by_offset_order();
+                    let last = *fields_sorted.last().unwrap();
+                    let FieldsShape::Arbitrary { ref offsets } = self.layout.fields else {
+                        unreachable!()
+                    };
+
+                    // We compute the size of the sized portion by taking the position of the
+                    // last element + the sized portion of that element.
+                    let unsized_offset_unadjusted = offsets[last].bytes();
+                    debug!(ty=?self.ty, ?unsized_offset_unadjusted, "size_of_sized_portion");
+                    unsized_offset_unadjusted + self.last_field_layout().size_of_head()
+                }
+                _ => {
+                    unreachable!("Expected sized type, but found: `{}`", self.ty)
+                }
+            }
+        }
+    }
+
+    /// Return the alignment of the fields that are sized from the head of the object.
+    ///
+    /// For a sized type, this function will return the alignment of the type.
+    ///
+    /// For an unsized type, this function will return the alignment of the sized portion.
+    /// The alignment of the type will be the maximum of the alignment of the sized portion
+    /// and the alignment of the unsized portion.
+    ///
+    /// If there's no sized portion, this function will return the minimum alignment (i.e.: 1).
+    pub fn align_of_head(&self) -> usize {
+        if self.is_sized() {
+            self.layout.abi_align.try_into().unwrap()
+        } else {
+            match self.ty.kind().rigid().unwrap() {
+                RigidTy::Slice(_) | RigidTy::Str | RigidTy::Dynamic(..) | RigidTy::Foreign(..) => 1,
+                RigidTy::Adt(..) | RigidTy::Tuple(..) => {
+                    // We have to recurse and get the maximum alignment of all sized portions.
+                    let field_layout = self.last_field_layout();
+                    field_layout.align_of_head().max(self.layout.abi_align.try_into().unwrap())
+                }
+                _ => {
+                    unreachable!("Expected sized type, but found: `{}`", self.ty);
+                }
+            }
+        }
+    }
+
+    /// Return the size of the type if it's known at compilation type.
+    pub fn size_of(&self) -> Option<usize> {
+        if self.is_sized() { Some(self.layout.size.bytes()) } else { None }
+    }
+
+    /// Return the alignment of the type if it's know at compilation time.
+    ///
+    /// The alignment is known at compilation type for sized types and types with slice tail.
+    ///
+    /// Note: We assume u64 and usize are the same since Kani is only supported in 64bits machines.
+    /// Add a configuration in case we ever decide to port this to a 32-bits machine.
+    #[cfg(target_pointer_width = "64")]
+    pub fn align_of(&self) -> Option<usize> {
+        if self.is_sized() || self.has_slice_tail() {
+            self.layout.abi_align.try_into().ok()
+        } else {
+            None
+        }
+    }
+
+    /// Return the layout of the last field of the type.
+    ///
+    /// This function is used to get the layout of the last field of an unsized type.
+    /// For example, if we have `*const (u8, [u16])`, the last field is `[u16]`.
+    /// This function will return the layout of `[u16]`.
+    ///
+    /// If the type is not a struct, an enum, or a tuple, with at least one field, this function
+    /// will panic.
+    fn last_field_layout(&self) -> LayoutOf {
+        match self.ty.kind().rigid().unwrap() {
+            RigidTy::Adt(adt_def, adt_args) => {
+                let fields = adt_def.variants_iter().next().unwrap().fields();
+                let fields_sorted = self.layout.fields.fields_by_offset_order();
+                let last_field_idx = *fields_sorted.last().unwrap();
+                LayoutOf::new(fields[last_field_idx].ty_with_args(adt_args))
+            }
+            RigidTy::Tuple(tys) => {
+                // For tuples, the unsized field is currently the last declared.
+                // To be on the safe side, we still get the sorted list by offset order.
+                let fields_sorted = self.layout.fields.fields_by_offset_order();
+                let last_field_idx = *fields_sorted.last().unwrap();
+                let last_ty = tys[last_field_idx];
+                LayoutOf::new(last_ty)
+            }
+            _ => {
+                unreachable!("Expected struct, enum or tuple. Found: `{}`", self.ty);
+            }
+        }
+    }
+}