Upgrade toolchain to nightly-2024-04-15

- rust-lang/rust#120131: Add support to `Pat` pattern type - rust-lang/rust#122935: Rename CastKind::PointerWithExposedProvenance - rust-lang/rust#123097: Adapt to changes to local_def_path_hash_to_def_id
celinval · Apr 15, 2024 · 6045e60 · 6045e60
1 parent def3a09
commit 6045e60
Show file tree

Hide file tree

Showing 7 changed files with 24 additions and 5 deletions.
diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs
@@ -292,6 +292,11 @@ impl<'tcx> GotocCtx<'tcx> {
                             "element of {parent_ty:?} is not accessed via field projection"
                         )
                     }
+                    TyKind::RigidTy(RigidTy::Pat(..)) => {
+                        // See https://github.com/rust-lang/types-team/issues/126
+                        // for what is currently supported.
+                        unreachable!("projection inside a pattern is not supported, only transmute")
+                    }
                 }
             }
             // if we fall here, then we are handling an enum

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs
@@ -681,7 +681,7 @@ impl<'tcx> GotocCtx<'tcx> {
                 | CastKind::FnPtrToPtr
                 | CastKind::PtrToPtr
                 | CastKind::PointerExposeAddress
-                | CastKind::PointerFromExposedAddress,
+                | CastKind::PointerWithExposedProvenance,
                 e,
                 t,
             ) => self.codegen_misc_cast(e, *t),

diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs
@@ -595,6 +595,13 @@ impl<'tcx> GotocCtx<'tcx> {
                     )
                 }
             }
+            // This object has the same layout as base. For now, translate this into `(base)`.
+            // The only difference is the niche.
+            ty::Pat(base_ty, ..) => {
+                self.ensure_struct(self.ty_mangled_name(ty), self.ty_pretty_name(ty), |tcx, _| {
+                    tcx.codegen_ty_tuple_like(ty, vec![*base_ty])
+                })
+            }
             ty::Alias(..) => {
                 unreachable!("Type should've been normalized already")
             }
@@ -995,6 +1002,7 @@ impl<'tcx> GotocCtx<'tcx> {
             | ty::Int(_)
             | ty::RawPtr(_, _)
             | ty::Ref(..)
+            | ty::Pat(..)
             | ty::Tuple(_)
             | ty::Uint(_) => self.codegen_ty(pointee_type).to_pointer(),
 

diff --git a/kani-compiler/src/kani_middle/stubbing/annotations.rs b/kani-compiler/src/kani_middle/stubbing/annotations.rs
@@ -56,7 +56,7 @@ pub fn update_stub_mapping(
                         "duplicate stub mapping: {} mapped to {} and {}",
                         tcx.def_path_str(orig_id),
                         tcx.def_path_str(stub_id),
-                        tcx.def_path_str(tcx.def_path_hash_to_def_id(other, &mut || panic!()))
+                        tcx.def_path_str(tcx.def_path_hash_to_def_id(other, &()))
                     ),
                 );
             }

diff --git a/kani-compiler/src/kani_middle/stubbing/transform.rs b/kani-compiler/src/kani_middle/stubbing/transform.rs
@@ -234,7 +234,7 @@ fn deserialize_mapping(tcx: TyCtxt, val: &str) -> HashMap<DefId, DefId> {
     type Item = (u64, u64);
     let item_to_def_id = |item: Item| -> DefId {
         let hash = DefPathHash(Fingerprint::new(item.0, item.1));
-        tcx.def_path_hash_to_def_id(hash, &mut || panic!())
+        tcx.def_path_hash_to_def_id(hash, &())
     };
     let pairs: Vec<(Item, Item)> = serde_json::from_str(val).unwrap();
     let mut m = HashMap::default();

diff --git a/kani-compiler/src/kani_middle/transform/check_values.rs b/kani-compiler/src/kani_middle/transform/check_values.rs
@@ -631,7 +631,7 @@ impl<'a> MirVisitor for CheckValueVisitor<'a> {
                     ty: (rvalue.ty(self.locals).unwrap()),
                 }),
                 CastKind::PointerExposeAddress
-                | CastKind::PointerFromExposedAddress
+                | CastKind::PointerWithExposedProvenance
                 | CastKind::PointerCoercion(_)
                 | CastKind::IntToInt
                 | CastKind::FloatToInt
@@ -898,6 +898,12 @@ fn ty_validity_per_offset(
                         }
                     }
                 }
+                RigidTy::Pat(base_ty, ..) => {
+                    // This is similar to a structure with one field and with niche defined.
+                    let mut pat_validity = ty_req();
+                    pat_validity.append(&mut ty_validity_per_offset(machine_info, *base_ty, 0)?);
+                    Ok(pat_validity)
+                }
                 RigidTy::Tuple(tys) => {
                     let mut tuple_validity = vec![];
                     for idx in layout.fields.fields_by_offset_order() {

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