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