Fix issues with how we compute DST size

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/overrides/hooks.rs

@@ -149,6 +149,37 @@ impl GotocHook for Assert {
     }
 }
 
+struct SafetyCheck;
+impl GotocHook for SafetyCheck {
+    fn hook_applies(&self, _tcx: TyCtxt, _instance: Instance) -> bool {
+        unreachable!("{UNEXPECTED_CALL}")
+    }
+
+    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 {
@@ -619,13 +650,14 @@ impl GotocHook for LoopInvariantRegister {
 }
 
 pub fn fn_hooks() -> GotocHooks {
-    let kani_lib_hooks: [(KaniHook, Rc<dyn GotocHook>); 11] = [
-        (KaniHook::Assert, Rc::new(Assert)),
+    let kani_lib_hooks = [
+        (KaniHook::Assert, Rc::new(Assert) as Rc<dyn GotocHook>),
         (KaniHook::Assume, Rc::new(Assume)),
         (KaniHook::Panic, Rc::new(Panic)),
         (KaniHook::Check, Rc::new(Check)),
         (KaniHook::Cover, Rc::new(Cover)),
         (KaniHook::AnyRaw, Rc::new(Nondet)),
+        (KaniHook::SafetyCheck, Rc::new(SafetyCheck)),
         (KaniHook::IsAllocated, Rc::new(IsAllocated)),
         (KaniHook::PointerObject, Rc::new(PointerObject)),
         (KaniHook::PointerOffset, Rc::new(PointerOffset)),

kani-compiler/src/kani_middle/abi.rs

@@ -13,7 +13,6 @@ pub struct LayoutOf {
     layout: LayoutShape,
 }
 
-#[allow(dead_code)] // TODO: Remove this in https://github.com/model-checking/kani/pull/3687
 impl LayoutOf {
     /// Create the layout structure for the given type
     pub fn new(ty: Ty) -> LayoutOf {

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};

kani-compiler/src/kani_middle/kani_functions.rs

@@ -44,6 +44,10 @@ pub enum KaniFunction {
 pub enum KaniIntrinsic {
     #[strum(serialize = "AnyModifiesIntrinsic")]
     AnyModifies,
+    #[strum(serialize = "CheckedAlignOfIntrinsic")]
+    CheckedAlignOf,
+    #[strum(serialize = "CheckedSizeOfIntrinsic")]
+    CheckedSizeOf,
     #[strum(serialize = "IsInitializedIntrinsic")]
     IsInitialized,
     #[strum(serialize = "ValidValueIntrinsic")]
@@ -55,6 +59,8 @@ pub enum KaniIntrinsic {
 /// Kani models are Rust functions that model some runtime behavior used by Kani instrumentation.
 #[derive(Debug, Copy, Clone, Eq, PartialEq, IntoStaticStr, EnumIter, EnumString, Hash)]
 pub enum KaniModel {
+    #[strum(serialize = "AlignOfDynObjectModel")]
+    AlignOfDynObject,
     #[strum(serialize = "AnyModel")]
     Any,
     #[strum(serialize = "CopyInitStateModel")]
@@ -85,6 +91,10 @@ pub enum KaniModel {
     SetSlicePtrInitialized,
     #[strum(serialize = "SetStrPtrInitializedModel")]
     SetStrPtrInitialized,
+    #[strum(serialize = "SizeOfDynObjectModel")]
+    SizeOfDynObject,
+    #[strum(serialize = "SizeOfSliceObjectModel")]
+    SizeOfSliceObject,
     #[strum(serialize = "StoreArgumentModel")]
     StoreArgument,
     #[strum(serialize = "WriteAnySliceModel")]
@@ -121,6 +131,8 @@ pub enum KaniHook {
     PointerObject,
     #[strum(serialize = "PointerOffsetHook")]
     PointerOffset,
+    #[strum(serialize = "SafetyCheckHook")]
+    SafetyCheck,
     #[strum(serialize = "UntrackedDerefHook")]
     UntrackedDeref,
 }