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/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/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_sized_portion(&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_sized_portion()
+                }
+                _ => {
+                    unreachable!("Expected sized type, but found: `{}`", self.ty)
+                }
+            }
+        }
+    }
+
+    /// Return the alignment of the fields that are sized.
+    ///
+    /// 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_sized_portion(&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_sized_portion()
+                        .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) => {
+                // We have to recurse and get the maximum alignment of all sized portions.
+                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) => {
+                // We have to recurse and get the maximum alignment of all sized portions.
+                let last_ty = tys.last().expect("Expected unsized tail");
+                LayoutOf::new(*last_ty)
+            }
+            _ => {
+                unreachable!("Expected struct, enum or tuple. Found: `{}`", self.ty);
+            }
+        }
+    }
+}

kani-compiler/src/kani_middle/attributes.rs

@@ -15,17 +15,18 @@ use rustc_middle::ty::{Instance, TyCtxt, TyKind};
 use rustc_session::Session;
 use rustc_smir::rustc_internal;
 use rustc_span::{Span, Symbol};
+use stable_mir::crate_def::Attribute as AttributeStable;
 use stable_mir::mir::mono::Instance as InstanceStable;
-use stable_mir::{CrateDef, DefId as StableDefId};
+use stable_mir::ty::FnDef;
+use stable_mir::{CrateDef, DefId as StableDefId, Symbol as SymbolStable};
 use std::str::FromStr;
 use strum_macros::{AsRefStr, EnumString};
 use syn::parse::Parser;
 use syn::punctuated::Punctuated;
-use syn::{PathSegment, TypePath};
-
-use tracing::{debug, trace};
+use syn::{Expr, ExprLit, Lit, PathSegment, TypePath};
 
 use super::resolve::{FnResolution, ResolveError, resolve_fn, resolve_fn_path};
+use tracing::{debug, trace};
 
 #[derive(Debug, Clone, Copy, AsRefStr, EnumString, PartialEq, Eq, PartialOrd, Ord)]
 #[strum(serialize_all = "snake_case")]
@@ -1030,6 +1031,12 @@ fn syn_attr(attr: &Attribute) -> syn::Attribute {
     parser.parse_str(&attr_str).unwrap().pop().unwrap()
 }
 
+/// Parse a stable attribute using `syn`.
+fn syn_attr_stable(attr: &AttributeStable) -> syn::Attribute {
+    let parser = syn::Attribute::parse_outer;
+    parser.parse_str(&attr.as_str()).unwrap().pop().unwrap()
+}
+
 /// Return a more user-friendly string for path by trying to remove unneeded whitespace.
 ///
 /// `quote!()` and `TokenString::to_string()` introduce unnecessary space around separators.
@@ -1071,3 +1078,19 @@ fn pretty_type_path(path: &TypePath) -> String {
         format!("{leading}{}", segments_str(&path.path.segments))
     }
 }
+
+pub(crate) fn fn_marker(def: FnDef) -> Option<String> {
+    let fn_marker: [SymbolStable; 2] = ["kanitool".into(), "fn_marker".into()];
+    let marker = def.attrs_by_path(&fn_marker).pop()?;
+    let attribute = syn_attr_stable(&marker);
+    let meta_name = attribute.meta.require_name_value().unwrap_or_else(|_| {
+        panic!("Expected name value attribute for `kanitool::fn_marker`, but found: `{:?}`", marker)
+    });
+    let Expr::Lit(ExprLit { lit: Lit::Str(lit_str), .. }) = &meta_name.value else {
+        panic!(
+            "Expected string literal for `kanitool::fn_marker`, but found: `{:?}`",
+            meta_name.value
+        );
+    };
+    Some(lit_str.value())
+}

kani-compiler/src/kani_middle/intrinsics.rs

@@ -2,6 +2,9 @@
 // SPDX-License-Identifier: Apache-2.0 OR MIT
 //! This module contains a MIR pass that replaces some intrinsics by rust intrinsics models as
 //! well as validation logic that can only be added during monomorphization.
+//!
+//! TODO: Move this code to `[crate::kani_middle::transform::RustcIntrinsicsPass]` since we can do
+//! proper error handling after monomorphization.
 use rustc_index::IndexVec;
 use rustc_middle::mir::{Body, Const as mirConst, ConstValue, Operand, TerminatorKind};
 use rustc_middle::mir::{Local, LocalDecl};