Upgrade toolchain to 2024-04-22 (#3171)

Addresses the new `AggregateKind::RawPtr` added in rust-lang/rust#123840. Resolves #3161 By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Kareem Khazem <[email protected]> Co-authored-by: Michael Tautschnig <[email protected]>
model-checking · May 14, 2024 · 997a54c · 997a54c
1 parent b34d117
commit 997a54c
Show file tree

Hide file tree

Showing 3 changed files with 39 additions and 1 deletion.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -674,6 +674,43 @@ 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]);
+                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),
         }
     }

diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/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(_, _)

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-04-21"
+channel = "nightly-2024-04-22"
 components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]