Fix issues with how we compute DST size (#3687)

This change fixes how we compute size of the object in our mem
predicates, and provide user visible methods to try to retrieve the size
of the object if known and valid (`checked_size_of_raw` and
`checked_align_of_raw`.

Fixes #3612
Fixes #3627

## Call-outs

To simplify this PR, I moved the following changes to their own PRs:
1. #3644
2. #3718

I also removed the fix for the intrinsics `size_of_val` and
`align_of_val` from this PR, and I will create a follow up PR once this
one is merged.

---------

Co-authored-by: Carolyn Zech <cmzech@amazon.com>

Author: celinval

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