Upgrade toolchain to 2024-07-19 (rust-lang#3364)

Resolves rust-lang#3358 Related upstream commits: - rust-lang@21dc49c587 ptr::metadata: avoid references to extern types
jaisnan · Jul 22, 2024 · 9f230ba · 9f230ba
1 parent 0367992
commit 9f230ba
Show file tree

Hide file tree

Showing 2 changed files with 24 additions and 6 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -703,8 +703,10 @@ impl<'tcx> GotocCtx<'tcx> {
                         if meta.typ().sizeof(&self.symbol_table) == 0 {
                             data_cast
                         } else {
-                            let vtable_expr =
-                                meta.member("_vtable_ptr", &self.symbol_table).cast_to(
+                            let vtable_expr = meta
+                                .member("_vtable_ptr", &self.symbol_table)
+                                .member("pointer", &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)
@@ -835,13 +837,29 @@ impl<'tcx> GotocCtx<'tcx> {
                             dst_goto_typ.lookup_components(&self.symbol_table).unwrap();
                         assert_eq!(dst_components.len(), 2);
                         assert_eq!(dst_components[0].name(), "_vtable_ptr");
-                        assert!(dst_components[0].typ().is_pointer());
+                        assert!(dst_components[0].typ().is_struct_like());
                         assert_eq!(dst_components[1].name(), "_phantom");
                         self.assert_is_rust_phantom_data_like(&dst_components[1].typ());
+                        // accessing pointer type of _vtable_ptr, which is wrapped in NonNull
+                        let vtable_ptr_typ = dst_goto_typ
+                            .lookup_field_type("_vtable_ptr", &self.symbol_table)
+                            .unwrap()
+                            .lookup_components(&self.symbol_table)
+                            .unwrap()[0]
+                            .typ();
                         Expr::struct_expr(
-                            dst_goto_typ,
+                            dst_goto_typ.clone(),
                             btree_string_map![
-                                ("_vtable_ptr", vtable_expr.cast_to(dst_components[0].typ())),
+                                (
+                                    "_vtable_ptr",
+                                    Expr::struct_expr_from_values(
+                                        dst_goto_typ
+                                            .lookup_field_type("_vtable_ptr", &self.symbol_table)
+                                            .unwrap(),
+                                        vec![vtable_expr.clone().cast_to(vtable_ptr_typ)],
+                                        &self.symbol_table
+                                    )
+                                ),
                                 (
                                     "_phantom",
                                     Expr::struct_expr(

diff --git a/rust-toolchain.toml b/rust-toolchain.toml
@@ -2,5 +2,5 @@
 # SPDX-License-Identifier: Apache-2.0 OR MIT
 
 [toolchain]
-channel = "nightly-2024-07-18"
+channel = "nightly-2024-07-19"
 components = ["llvm-tools", "rustc-dev", "rust-src", "rustfmt"]