From 6045e60bc5c598ec6b27a2729f9f10dbe8c7a8fc Mon Sep 17 00:00:00 2001 From: "Celina G. Val" Date: Mon, 15 Apr 2024 15:38:37 -0700 Subject: [PATCH] Upgrade toolchain to nightly-2024-04-15 - https://github.com/rust-lang/rust/pull/120131: Add support to `Pat` pattern type - https://github.com/rust-lang/rust/pull/122935: Rename CastKind::PointerWithExposedProvenance - https://github.com/rust-lang/rust/pull/123097: Adapt to changes to local_def_path_hash_to_def_id --- kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs | 5 +++++ kani-compiler/src/codegen_cprover_gotoc/codegen/rvalue.rs | 2 +- kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs | 8 ++++++++ kani-compiler/src/kani_middle/stubbing/annotations.rs | 2 +- kani-compiler/src/kani_middle/stubbing/transform.rs | 2 +- kani-compiler/src/kani_middle/transform/check_values.rs | 8 +++++++- rust-toolchain.toml | 2 +- 7 files changed, 24 insertions(+), 5 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/place.rs index 6b764fb63365..d24e5448c595 100644 --- 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 index 14e789930f93..008e48937819 100644 --- 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 index b5ccf1a83716..64c36dd76cfb 100644 --- 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 index 52b994ab97d2..26e508707207 100644 --- 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 index 16c46990bc6f..f101a6009907 100644 --- 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 { 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 index a620dfabb72e..d62b5807319e 100644 --- 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 index 31f9e45dd714..be42da187e10 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-03" +channel = "nightly-2024-04-15" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]