From d095367f33d582107a3e344b9008ffabc30cadf9 Mon Sep 17 00:00:00 2001 From: Adrian Palacios <73246657+adpaco-aws@users.noreply.github.com> Date: Fri, 8 Dec 2023 14:17:47 -0500 Subject: [PATCH] Update Rust toolchain to `nightly-2023-12-08` (#2926) Updates the Rust toolchain to `nightly-2023-12-08`. The relevant changes are: * https://github.com/rust-lang/rust/pull/118324 * https://github.com/rust-lang/rust/pull/118684 --------- Co-authored-by: Celina G. Val --- .../src/codegen_cprover_gotoc/codegen/operand.rs | 6 ++++-- kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs | 9 ++++----- kani-compiler/src/kani_middle/reachability.rs | 6 +----- rust-toolchain.toml | 2 +- 4 files changed, 10 insertions(+), 13 deletions(-) diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs index d297d9d90a52..59a18348d582 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/operand.rs @@ -421,7 +421,8 @@ impl<'tcx> GotocCtx<'tcx> { } (Scalar::Ptr(ptr, _size), _) => { let res_t = self.codegen_ty(ty); - let (alloc_id, offset) = ptr.into_parts(); + let (prov, offset) = ptr.into_parts(); + let alloc_id = prov.alloc_id(); self.codegen_alloc_pointer(res_t, alloc_id, offset, span) } _ => unimplemented!(), @@ -646,7 +647,8 @@ impl<'tcx> GotocCtx<'tcx> { Size::from_bytes(self.symbol_table.machine_model().pointer_width_in_bytes()); let mut next_offset = Size::ZERO; - for &(offset, alloc_id) in alloc.provenance().ptrs().iter() { + for &(offset, prov) in alloc.provenance().ptrs().iter() { + let alloc_id = prov.alloc_id(); if offset > next_offset { let bytes = alloc.inspect_with_uninit_and_ptr_outside_interpreter( next_offset.bytes_usize()..offset.bytes_usize(), diff --git a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs index aec9d8143818..ec5756c4d09b 100644 --- a/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs +++ b/kani-compiler/src/codegen_cprover_gotoc/codegen/typ.rs @@ -332,11 +332,11 @@ impl<'tcx> GotocCtx<'tcx> { ty: Ty<'tcx>, args: ty::GenericArgsRef<'tcx>, ) -> ty::PolyFnSig<'tcx> { - let sig = args.as_coroutine().poly_sig(); + let sig = args.as_coroutine().sig(); - let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter( - sig.bound_vars().iter().chain(iter::once(ty::BoundVariableKind::Region(ty::BrEnv))), - ); + let bound_vars = self.tcx.mk_bound_variable_kinds_from_iter(iter::once( + ty::BoundVariableKind::Region(ty::BrEnv), + )); let br = ty::BoundRegion { var: ty::BoundVar::from_usize(bound_vars.len() - 1), kind: ty::BoundRegionKind::BrEnv, @@ -349,7 +349,6 @@ impl<'tcx> GotocCtx<'tcx> { let pin_args = self.tcx.mk_args(&[env_ty.into()]); let env_ty = Ty::new_adt(self.tcx, pin_adt_ref, pin_args); - let sig = sig.skip_binder(); // The `FnSig` and the `ret_ty` here is for a coroutines main // `coroutine::resume(...) -> CoroutineState` function in case we // have an ordinary coroutine, or the `Future::poll(...) -> Poll` diff --git a/kani-compiler/src/kani_middle/reachability.rs b/kani-compiler/src/kani_middle/reachability.rs index a8e7d9fe3f83..216feb66fb87 100644 --- a/kani-compiler/src/kani_middle/reachability.rs +++ b/kani-compiler/src/kani_middle/reachability.rs @@ -153,11 +153,7 @@ impl<'tcx> MonoItemsCollector<'tcx> { /// instruction looking for the items that should be included in the compilation. fn reachable_items(&mut self) { while let Some(to_visit) = self.queue.pop() { - // TODO: This should only check is_foreign_item() or even `has_body()`. - // We need https://github.com/rust-lang/rust/pull/118681 to land first. - if !self.collected.contains(&to_visit) - && !self.tcx.is_foreign_item(rustc_internal::internal(to_visit.clone()).def_id()) - { + if !self.collected.contains(&to_visit) { self.collected.insert(to_visit.clone()); let next_items = match &to_visit { MonoItem::Fn(instance) => self.visit_fn(*instance), diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 2bdb5cdf793a..6c7de32c5e63 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -2,5 +2,5 @@ # SPDX-License-Identifier: Apache-2.0 OR MIT [toolchain] -channel = "nightly-2023-12-07" +channel = "nightly-2023-12-08" components = ["llvm-tools-preview", "rustc-dev", "rust-src", "rustfmt"]