From 997a54cc55d8eea26ec021e541582280da184712 Mon Sep 17 00:00:00 2001
From: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
Date: Tue, 14 May 2024 10:51:51 -0700
Subject: [PATCH] Upgrade toolchain to 2024-04-22 (#3171)

Addresses the new `AggregateKind::RawPtr` added in
https://github.com/rust-lang/rust/pull/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 <karkhaz@amazon.com>
Co-authored-by: Michael Tautschnig <tautschn@amazon.com>
---
 .../codegen_cprover_gotoc/codegen/rvalue.rs   | 37 +++++++++++++++++++
 .../src/kani_middle/transform/check_values.rs |  1 +
 rust-toolchain.toml                           |  2 +-
 3 files changed, 39 insertions(+), 1 deletion(-)

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
index cb78163fe99b..8a9aa4821ab6 100644
--- 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
index d62b5807319e..4697c139b294 100644
--- 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
index 70848743b686..e571e9eaff4f 100644
--- 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"]