fix TypeId handling

Author: thanhnguyen-aws

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

@@ -152,7 +152,7 @@ impl GotocCtx<'_> {
             .args
             .iter()
             .enumerate()
-            .filter(|&(_, arg)| (arg.mode != PassMode::Ignore))
+            .filter(|&(_, arg)| arg.mode != PassMode::Ignore)
             .map(|(idx, arg)| {
                 let arg_name = format!("{fn_name}::param_{idx}");
                 let base_name = format!("param_{idx}");

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

@@ -204,6 +204,13 @@ impl<'tcx> GotocCtx<'tcx> {
                 Some(self.codegen_const_ptr(alloc, ty, inner_ty, loc))
             }
             TyKind::RigidTy(RigidTy::Adt(adt, args)) if adt.kind().is_struct() => {
+                //Special struct that is used to handle type_id function
+                if adt.name().contains("any::TypeId") {
+                    let val = alloc.read_uint().unwrap();
+                    let u128_expr = Expr::int_constant(val, Type::unsigned_int(128));
+                    let typ = self.codegen_ty_stable(ty);
+                    return Some(u128_expr.transmute_to(typ, &self.symbol_table));
+                }
                 // Structs only have one variant.
                 let variant = adt.variants_iter().next().unwrap();
                 // There must be at least one field associated with the scalar data.
@@ -399,6 +406,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 let name = format!("{}::{alloc_id:?}", self.full_crate_name());
                 self.codegen_const_allocation(&alloc, Some(name), loc)
             }
+            GlobalAlloc::TypeId { ty: _ } => todo!(),
         };
         assert!(res_t.is_pointer() || res_t.is_transparent_type(&self.symbol_table));
         let offset_addr = base_addr

kani-compiler/src/kani_middle/reachability.rs

@@ -529,6 +529,7 @@ fn collect_alloc_items(tcx: TyCtxt, alloc_id: AllocId) -> Vec<MonoItem> {
             let vtable_id = vtable_alloc.vtable_allocation().unwrap();
             items = collect_alloc_items(tcx, vtable_id);
         }
+        GlobalAlloc::TypeId { ty: _ } => {}
     };
     items
 }

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2025-07-10"
+channel = "nightly-2025-07-11"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]