Move fixes to <size|align>_of_val to a new PR

Revert changes to intrinsics and remove tests for now

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

@@ -215,6 +215,17 @@ 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
@@ -411,6 +422,7 @@ 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 => {
@@ -504,6 +516,7 @@ 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(
@@ -546,9 +559,6 @@ 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,8 +61,6 @@ pub enum KaniIntrinsic {
 pub enum KaniModel {
     #[strum(serialize = "AlignOfDynObjectModel")]
     AlignOfDynObject,
-    #[strum(serialize = "AlignOfValRawModel")]
-    AlignOfVal,
     #[strum(serialize = "AnyModel")]
     Any,
     #[strum(serialize = "CopyInitStateModel")]
@@ -97,8 +95,6 @@ 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,7 +33,6 @@ 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;
@@ -44,7 +43,6 @@ 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.
@@ -90,7 +88,6 @@ 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
     }
 

library/kani_core/src/models.rs

@@ -10,40 +10,6 @@
 #[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 {
-                    // Note that today we trigger a safety check for foreign types.
-                    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};