Upgrade toolchain to 2024-04-22

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

@@ -674,6 +674,44 @@ impl<'tcx> GotocCtx<'tcx> {
                     &self.symbol_table,
                 )
             }
+            AggregateKind::RawPtr(pointee_ty, _) => {
+                // We expect two operands: "data" and "meta"
+                assert!(operands.len() == 2);
+                let typ = self.codegen_ty_stable(res_ty);
+                let layout = self.layout_of_stable(res_ty);
+                assert!(layout.ty.is_unsafe_ptr());
+                let data = self.codegen_operand_stable(&operands[0]);
+                //dbg!(pointee_ty.kind());
+                match pointee_ty.kind() {
+                    TyKind::RigidTy(RigidTy::Slice(inner_ty)) => {
+                        let pointee_goto_typ = self.codegen_ty_stable(inner_ty);
+                        // cast data to pointer with specified type
+                        let data_cast =
+                            data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) });
+                        let meta = self.codegen_operand_stable(&operands[1]);
+                        slice_fat_ptr(typ, data_cast, meta, &self.symbol_table)
+                    }
+                    TyKind::RigidTy(RigidTy::Adt(..)) => {
+                        let pointee_goto_typ = self.codegen_ty_stable(pointee_ty);
+                        let data_cast =
+                            data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) });
+                        let meta = self.codegen_operand_stable(&operands[1]);
+                        if meta.typ().sizeof(&self.symbol_table) == 0 {
+                            data_cast
+                        } else {
+                            let vtable_expr =
+                                meta.member("vtable_ptr", &self.symbol_table).cast_to(
+                                    typ.lookup_field_type("vtable", &self.symbol_table).unwrap(),
+                                );
+                            dynamic_fat_ptr(typ, data_cast, vtable_expr, &self.symbol_table)
+                        }
+                    }
+                    _ => {
+                        let pointee_goto_typ = self.codegen_ty_stable(pointee_ty);
+                        data.cast_to(Type::Pointer { typ: Box::new(pointee_goto_typ) })
+                    }
+                }
+            }
             AggregateKind::Coroutine(_, _, _) => self.codegen_rvalue_coroutine(&operands, res_ty),
         }
     }

kani-compiler/src/kani_middle/transform/check_values.rs

@@ -678,6 +678,7 @@ impl<'a> MirVisitor for CheckValueVisitor<'a> {
                 AggregateKind::Array(_)
                 | AggregateKind::Closure(_, _)
                 | AggregateKind::Coroutine(_, _, _)
+                | AggregateKind::RawPtr(_, _)
                 | AggregateKind::Tuple => {}
             },
             Rvalue::AddressOf(_, _)

rust-toolchain.toml

@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-04-21"
+channel = "nightly-2024-04-22"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]